Definition hat_functor_preserves_binproducts (t : sort) (c : propcoproducts_commute_binproducts C BP (λ p, CC p (isasetaprop (pr2 p)))) : preserves_binproduct (hat_functor sort Hsort C CC t). Proof. intros x y p p1 p2 p_prod. use (isBinProduct_is_objectwise _ BP). intro F. simpl. assert (ts_pr : isaprop (t = F)). { apply Hsort_set. } use make_isBinProduct'. { apply BP. } use tpair. - use make_is_z_isomorphism. + refine (_ · pr1 (c (_,,ts_pr) x y) · _). ++ use BinProductOfArrows ; use CoproductOfArrows ; intro ; apply identity. ++ use CoproductOfArrows. exact (λ _, BinProductOfArrows _ (make_BinProduct _ _ _ _ _ _ p_prod) (BP x y) (identity _) (identity _)). + split. * etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, assoc. etrans. 1: do 2 apply maponpaths_2 ; apply postcompWithBinProductArrow. transparent assert (ii : (is_z_isomorphism (CoproductOfArrows (t = F) C (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, BP x y)) (CC (t = F) (Hsort t F) (λ _ : t = F, p)) (λ _ : t = F, BinProductOfArrows C (make_BinProduct C x y p p1 p2 p_prod) (BP x y) (identity x) (identity y))))). { apply CoproductOfArrowsIsos. intro. exact (BinProductOfArrows_is_z_iso (BP x y) (make_BinProduct C x y p p1 p2 p_prod) (identity _) (identity _) (identity_is_z_iso _) (identity_is_z_iso _)). } apply (z_iso_inv_to_right _ _ _ _ (_,,ii)). etrans. 2: apply pathsinv0, id_left. apply pathsinv0. apply (z_iso_inv_on_left _ _ _ _ (_ ,, c ((t = F),, ts_pr) x y)). etrans. 2: apply pathsinv0, precompWithBinProductArrow. use BinProductArrowUnique. -- etrans. 1: apply BinProductPr1Commutes. simpl. unfold inv_from_z_iso. simpl. etrans. 1: apply precompWithCoproductArrow. etrans. 2: apply pathsinv0, precompWithCoproductArrow. use CoproductArrowUnique. intro. etrans. 1: apply (CoproductInCommutes _ _ _ (CC (t = F) (Hsort t F) (λ _ : t = F, p))). etrans. 2: apply assoc'. etrans. 2: apply maponpaths_2, pathsinv0, BinProductPr1Commutes. apply assoc. -- etrans. 1: apply BinProductPr2Commutes. simpl. unfold inv_from_z_iso. simpl. etrans. 1: apply precompWithCoproductArrow. etrans. 2: apply pathsinv0, precompWithCoproductArrow. use CoproductArrowUnique. intro. etrans. 1: apply (CoproductInCommutes _ _ _ (CC (t = F) (Hsort t F) (λ _ : t = F, p))). etrans. 2: apply assoc'. etrans. 2: apply maponpaths_2, pathsinv0, BinProductPr2Commutes. apply assoc. * transparent assert (ii : (is_z_isomorphism (BinProductOfArrows C (BP (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, x)) (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, y))) (BP (CC (t = F) (Hsort t F) (λ _ : t = F, x)) (CC (t = F) (Hsort t F) (λ _ : t = F, y))) (CoproductOfArrows (t = F) C (CC (t = F) (Hsort t F) (λ _ : t = F, x)) (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, x)) (λ _ : t = F, identity x)) (CoproductOfArrows (t = F) C (CC (t = F) (Hsort t F) (λ _ : t = F, y)) (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, y)) (λ _ : t = F, identity y))))). { apply BinProductOfArrows_is_z_iso ; (apply CoproductOfArrowsIsos ; intro ; apply identity_is_z_iso). } rewrite ! assoc'. apply pathsinv0. apply (z_iso_inv_to_left _ _ _ ((_,,ii))). etrans. 1: apply id_right. apply (z_iso_inv_to_left _ _ _ (z_iso_inv (_ ,, c ((t = F),, ts_pr) x y))). etrans. 1: apply postcompWithBinProductArrow. etrans. 2: apply pathsinv0, precompWithBinProductArrow. use BinProductArrowUnique. -- etrans. 1: apply BinProductPr1Commutes. etrans. 1: apply precompWithCoproductArrow. etrans. 2: apply pathsinv0, precompWithCoproductArrow. use CoproductArrowUnique. intro. etrans. 1: apply (CoproductInCommutes _ _ _ (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, BP x y))). etrans. 1: apply maponpaths, id_left. unfold BinProductOfArrows. etrans. 2: apply assoc'. apply maponpaths_2. etrans. 2: apply pathsinv0, (BinProductPr1Commutes _ _ _ ((make_BinProduct C x y p p1 p2 p_prod))). apply pathsinv0, id_right. -- etrans. 1: apply BinProductPr2Commutes. etrans. 1: apply precompWithCoproductArrow. etrans. 2: apply pathsinv0, precompWithCoproductArrow. use CoproductArrowUnique. intro. etrans. 1: apply (CoproductInCommutes _ _ _ (CC (t = F) (isasetaprop (pr2 ((t = F),, ts_pr))) (λ _ : t = F, BP x y))). etrans. 1: apply maponpaths, id_left. unfold BinProductOfArrows. etrans. 2: apply assoc'. apply maponpaths_2. etrans. 2: apply pathsinv0, (BinProductPr2Commutes _ _ _ ((make_BinProduct C x y p p1 p2 p_prod))). apply pathsinv0, id_right. - split. + etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply precompWithCoproductArrow. } transparent assert (i : (is_z_isomorphism (BinProductOfArrows C (BP (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, x)) (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, y))) (BP (CC (t = F) (Hsort t F) (λ _ : t = F, x)) (CC (t = F) (Hsort t F) (λ _ : t = F, y))) (CoproductOfArrows (t = F) C (CC (t = F) (Hsort t F) (λ _ : t = F, x)) (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, x)) (λ _ : t = F, identity x)) (CoproductOfArrows (t = F) C (CC (t = F) (Hsort t F) (λ _ : t = F, y)) (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, y)) (λ _ : t = F, identity y))))). { use BinProductOfArrows_is_z_iso ; (use CoproductOfArrowsIsos ; intro ; apply identity_is_z_iso). } apply pathsinv0. etrans. 2: apply assoc. use (z_iso_inv_to_left _ _ _ (_,,i)). etrans. 1: apply BinProductPr1Commutes. use (z_iso_inv_to_left _ _ _ (z_iso_inv (_,,(c ((t = F),, ts_pr) x y)))). etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, BinProductPr1Commutes. use CoproductArrowUnique. intro. etrans. 1: apply assoc. etrans. 1: { apply maponpaths_2. apply (CoproductInCommutes _ _ _ ((CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, BP x y)))). } etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (CoproductInCommutes _ _ _ (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, x))). } etrans. 2: apply assoc'. etrans. 2: { apply maponpaths_2, pathsinv0. apply (BinProductPr1Commutes _ _ _ (make_BinProduct C x y p p1 p2 p_prod)). } apply assoc. + etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply precompWithCoproductArrow. } transparent assert (i : (is_z_isomorphism (BinProductOfArrows C (BP (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, x)) (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, y))) (BP (CC (t = F) (Hsort t F) (λ _ : t = F, x)) (CC (t = F) (Hsort t F) (λ _ : t = F, y))) (CoproductOfArrows (t = F) C (CC (t = F) (Hsort t F) (λ _ : t = F, x)) (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, x)) (λ _ : t = F, identity x)) (CoproductOfArrows (t = F) C (CC (t = F) (Hsort t F) (λ _ : t = F, y)) (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, y)) (λ _ : t = F, identity y))))). { use BinProductOfArrows_is_z_iso ; (use CoproductOfArrowsIsos ; intro ; apply identity_is_z_iso). } apply pathsinv0. etrans. 2: apply assoc. use (z_iso_inv_to_left _ _ _ (_,,i)). etrans. 1: apply BinProductPr2Commutes. use (z_iso_inv_to_left _ _ _ (z_iso_inv (_,,(c ((t = F),, ts_pr) x y)))). etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, BinProductPr2Commutes. use CoproductArrowUnique. intro. etrans. 1: apply assoc. etrans. 1: { apply maponpaths_2. apply (CoproductInCommutes _ _ _ ((CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, BP x y)))). } etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (CoproductInCommutes _ _ _ (CC (t = F) (isasetaprop ts_pr) (λ _ : t = F, y))). } etrans. 2: apply assoc'. etrans. 2: { apply maponpaths_2, pathsinv0. apply (BinProductPr2Commutes _ _ _ (make_BinProduct C x y p p1 p2 p_prod)). } apply assoc. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas. Require Import UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts. Require Import UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor. Require Import UniMath.CategoryTheory.Limits.Preservation.