proposition: Lemma Abs_θ_strength2_int: θ_Strength2_int Abs_θ.
proof: Proof. intros X Z Z'. unfold Abs_θ, Abs_H, Abs_θ_data. apply nat_trans_eq_alt. intro c. simpl. rewrite id_left. rewrite id_right. unfold Abs_θ_data_data. simpl. unfold horcomp_data; simpl. rewrite <- functor_comp. apply maponpaths. clear X. destruct Z as [Z e]; destruct Z' as [Z' e']; etrans. 2: { eapply pathsinv0. apply postcompWithBinCoproductArrow. } simpl. apply maponpaths_12. + rewrite <- assoc. assert (NN := nat_trans_ax e' _ _ (e (BinCoproductObject (CC (TerminalObject terminal) c)))). simpl in NN. match goal with |[ H1: _ = ?f·?g |- ?h · _ = _ ] => intermediate_path (h·(f·g)) end. * apply maponpaths, NN. * assert (NNN := nat_trans_ax e' _ _ (BinCoproductArrow (CC (TerminalObject terminal) (Z c)) (BinCoproductIn1 (CC (TerminalObject terminal) c)· e (BinCoproductObject (CC (TerminalObject terminal) c))) (# Z (BinCoproductIn2 (CC (TerminalObject terminal) c))))). simpl in NNN. match goal with |[ H1: _ = ?f·?g |- _ = ?h · _] => intermediate_path (h·(f·g)) end. - simpl. rewrite <- NNN. clear NNN. do 2 rewrite assoc. rewrite BinCoproductIn1Commutes. do 2 rewrite <- assoc. apply maponpaths, pathsinv0, NN. - apply idpath. + rewrite <- functor_comp. apply maponpaths. etrans. 2: { eapply pathsinv0. apply BinCoproductIn2Commutes. } apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.PrecategoryBinProduct UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.BinSumOfSignatures UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits