Definition Flat_θ_data (XZ: [C, C] ⊠ category_Ptd C): [C, C] ⟦θ_source Flat_H XZ, θ_target Flat_H XZ⟧. Proof. set (h:= nat_trans_comp (linvunitor_CAT (pr1 XZ)) ((nat_trans_id _) ⋆ (pr2 (pr2 XZ)))). set (F1' := pr1 (pr2 (left_unit_as_nat_z_iso _ _) (pr1 XZ))). set (F2' := # (post_comp_functor (pr1 XZ)) (pr2 (pr2 XZ))). set (h' := F1' · F2'). set (obsolete := nat_trans_comp (lassociator_CAT (pr1 (pr2 XZ)) (pr1 XZ) (pr1 XZ)) (h ⋆ (nat_trans_id (functor_composite (pr1 (pr2 XZ)) (pr1 XZ))))). set (F3' := rassociator_CAT (pr12 XZ) (pr1 XZ) (pr1 XZ)). set (F4' := # (pre_comp_functor (functor_compose (pr1 (pr2 XZ)) (pr1 XZ))) h'). exact (F3' · F4'). Defined.
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.