Definition creates_limits_functor_alg : creates_limits_unique disp_cat_functor_alg. Proof. unfold creates_limits_unique. intros J D L. induction L as [tmp isL]. induction tmp as [x L]. unfold creates_limit. cbn. transparent assert (FC : (cone (mapdiagram π D) (F x))). { use make_cone. - intro j. eapply compose. apply ((#F)%cat (coneOut L j )). cbn. exact (pr2 (dob D j)). - abstract ( red; intros; cbn; assert (XR := pr2 (dmor D e)); cbn in XR; etrans; [eapply pathsinv0; apply assoc |]; etrans; [apply maponpaths, (!XR) |]; etrans; [apply assoc |]; apply maponpaths_2; rewrite <- functor_comp; apply maponpaths; apply (coneOutCommutes L) ). } transparent assert (LL : (LimCone (mapdiagram π D))). { use make_LimCone. apply x. apply L. apply isL. } use tpair. - use tpair. + use tpair. * use (limArrow LL). apply FC. * abstract ( use tpair ; [ intro j; cbn; set (XR := limArrowCommutes LL _ FC); cbn in XR; apply pathsinv0; apply XR | cbn; intros i j e; apply subtypePath; [ intro; apply homset_property |]; cbn; apply (coneOutCommutes L) ]). + abstract ( intro t; cbn; use total2_paths_f; [ cbn; apply (limArrowUnique LL); induction t as [t [H1 H2]]; cbn in *; intro j; apply pathsinv0, H1 |]; apply proofirrelevance; apply isofhleveltotal2; [ apply impred_isaprop; intro; apply homset_property |]; intros; do 3 (apply impred_isaprop; intro); apply (homset_property (total_category _ )) ). - cbn. intros x' CC. set (πCC := mapcone π D CC). use unique_exists. + use tpair. * cbn. use (limArrow LL _ πCC). * set (XR := limArrowCommutes LL). cbn in XR. set (H1:= coneOutCommutes CC). simpl in H1. destruct x' as [c a]. cbn. unfold disp_cat_functor_alg in a. cbn in a. cbn in πCC. transparent assert (X : (cone (mapdiagram π D) (F c))). { use make_cone. - intro j. apply (λ f, a · f). cbn. apply (coneOut CC j). - abstract ( intros u v e; cbn; rewrite <- assoc; apply maponpaths; apply (maponpaths pr1 (coneOutCommutes CC _ _ _ )) ). } { unfold functor_alg_mor. intermediate_path (limArrow LL _ X). - apply (limArrowUnique LL). intro j. rewrite <- assoc. rewrite (limArrowCommutes LL). cbn. rewrite assoc. rewrite <- functor_comp. etrans. apply maponpaths_2. apply maponpaths. apply (limArrowCommutes LL). cbn. set (H := pr2 (coneOut CC j)). cbn in H. apply H. - apply pathsinv0. use (limArrowUnique LL). intro j. rewrite <- assoc. rewrite (limArrowCommutes LL). cbn. apply idpath. } + simpl. intro j. apply subtypePath. { intro. apply homset_property. } cbn. apply (limArrowCommutes LL). + intros. apply impred_isaprop. intro t. (apply (homset_property (total_category _ ))). + simpl. intros. apply subtypePath. { intro. apply homset_property. } apply (limArrowUnique LL). intro u. specialize (X u). apply (maponpaths pr1 X). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.