Lemma Abs_θ_strength2_int: θ_Strength2_int Abs_θ. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. 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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.