Lemma is_nat_trans_Flat_θ_data: is_nat_trans _ _ Flat_θ_data. Proof. intros XZ XZ' αβ. apply nat_trans_eq_alt. intro c. simpl. destruct XZ as [X [Z e]]; destruct XZ' as [X' [Z' e']]; destruct αβ as [α β]; simpl in *. repeat rewrite id_left. rewrite (functor_comp Z). rewrite (functor_comp X). repeat rewrite assoc. do 4 rewrite <- functor_comp. rewrite (nat_trans_ax α). repeat rewrite <- assoc. rewrite <- functor_comp. do 2 rewrite (nat_trans_ax α). do 2 apply maponpaths. repeat rewrite assoc. etrans. 2: { do 2 apply cancel_postcomposition. apply (nat_trans_ax e). } cbn. assert (β_is_pointed := ptd_mor_commutes _ β). simpl in β_is_pointed. rewrite <- (nat_trans_ax α). repeat rewrite <- assoc. apply maponpaths. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply (nat_trans_ax e). } cbn. rewrite <- assoc. rewrite β_is_pointed. 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.