Lemma δ_law1_genoption : δ_law1 genopt δ_genoption. Proof. apply nat_trans_eq_alt; intro c; simpl. unfold δ_genoption_mor, BinCoproduct_of_functors_ob; simpl. rewrite id_right. apply pathsinv0, BinCoproduct_endo_is_identity. - apply BinCoproductIn1Commutes. - apply BinCoproductIn2Commutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.PointedFunctorsComposition.