From fe4b21669a25079a0699654291522486eafe9226 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 27 Apr 2020 02:30:19 +0300 Subject: [PATCH 01/18] Construct type category from a comprehension category --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 141 ++++++++++++++++++++- 1 file changed, 138 insertions(+), 3 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 8a821cd8..57ba517f 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -483,6 +483,136 @@ Section TypeCat_Disp_Functor. End TypeCat_Disp_Functor. +(* TODO: move upstream *) +Definition comprehension_cat := ∑ (C : category), (comprehension_cat_structure C). + +Section ComprehensionCat_TypeCat. + Context {C : category}. + Context (CC : comprehension_cat_structure C). + + Let D := pr1 CC : disp_cat C. + Let cleaving_D := pr1 (pr2 CC) : cleaving D. + Let comprehension_functor + := pr1 (pr2 (pr2 CC)) + : disp_functor _ D (disp_codomain C). + Let comprehension_functor_is_cartesian + := pr2 (pr2 (pr2 CC)) + : is_cartesian_disp_functor comprehension_functor. + + Definition ty_from_comprehension_cat : C → UU + := ob_disp D. + + Definition ext_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + : C + := pr1 (comprehension_functor Γ A). + + Definition reind_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + (Γ' : C) (f : Γ' --> Γ) + : ty_from_comprehension_cat Γ' + := pr1 (cleaving_D Γ Γ' f A). + + Definition typecat1_from_comprehension_cat + : typecat_structure1 C. + Proof. + repeat use tpair. + - exact ty_from_comprehension_cat. + - exact ext_from_comprehension_cat. + - exact reind_from_comprehension_cat. + Defined. + + Definition dpr_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + : ext_from_comprehension_cat Γ A --> Γ + := pr2 (comprehension_functor Γ A). + + Definition typecat_obj_ext_structure_from_comprehension_cat + : typecat_obj_ext_structure C + := (typecat1_from_comprehension_cat ,, dpr_from_comprehension_cat). + + Definition q_square_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + (Γ' : C) (f : Γ' --> Γ) + : comprehension_functor Γ' (reind_from_comprehension_cat _ A _ f) + -->[ f ] comprehension_functor Γ A + := disp_functor_on_morphisms comprehension_functor + (pr1 (pr2 (cleaving_D Γ Γ' f A))). + + Definition q_square_from_comprehension_cat_is_cartesian + (Γ : C) (A : ty_from_comprehension_cat Γ) + (Γ' : C) (f : Γ' --> Γ) + : is_cartesian (q_square_from_comprehension_cat _ A _ f). + Proof. + apply comprehension_functor_is_cartesian. + apply cartesian_lift_is_cartesian. + Defined. + + Definition q_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + (Γ' : C) (f : Γ' --> Γ) + : ext_from_comprehension_cat + Γ' (reind_from_comprehension_cat Γ A Γ' f) + --> ext_from_comprehension_cat Γ A + := pr1 (q_square_from_comprehension_cat _ A _ f). + + Definition dpr_q_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + (Γ' : C) (f : Γ' --> Γ) + : q_from_comprehension_cat _ A _ f ;; dpr_from_comprehension_cat _ A + = dpr_from_comprehension_cat _ (reind_from_comprehension_cat _ A _ f) ;; f + := pr2 (q_square_from_comprehension_cat _ A _ f). + + Definition pullback_from_comprehension_cat + (Γ : C) (A : ty_from_comprehension_cat Γ) + (Γ' : C) (f : Γ' --> Γ) + : isPullback _ _ _ _ (!dpr_q_from_comprehension_cat _ A _ f). + Proof. + intros Δ g k H. + eapply iscontrweqf. + 2: { + use (q_square_from_comprehension_cat_is_cartesian _ A _ f). + - exact Γ'. + - exact (identity _). + - apply (Δ,, g). + - use tpair. + + apply k. + + etrans. apply pathsinv0, H. + apply pathsinv0, maponpaths, id_left. + } + apply invweq. + eapply weqcomp. + 2: apply weqtotal2asstol. + apply weq_subtypes_iff. + - intro. apply isapropdirprod; apply homset_property. + - intro. apply (isofhleveltotal2 1). + + apply homset_property. + + intros. apply homsets_disp. + - intros gg; split; intros H'. + + use tpair. + * etrans. apply (pr1 H'). + apply pathsinv0, id_right. + * apply subtypePath. + intro; apply homset_property. + exact (pr2 H'). + + split. + * etrans. apply (pr1 H'). apply id_right. + * etrans. apply (maponpaths pr1 (pr2 H')). apply idpath. + Defined. + + Definition typecat_structure_from_comprehension_cat + : typecat_structure C. + Proof. + exists typecat1_from_comprehension_cat. + repeat use tpair. + - exact dpr_from_comprehension_cat. + - exact q_from_comprehension_cat. + - exact dpr_q_from_comprehension_cat. + - exact pullback_from_comprehension_cat. + Defined. + +End ComprehensionCat_TypeCat. + Section TypeCat_ComprehensionCat. Definition typecat_to_comprehension_cat_structure @@ -496,9 +626,6 @@ Section TypeCat_ComprehensionCat. apply typecat_disp_functor_is_cartesian. Defined. - (* TODO: move upstream *) - Definition comprehension_cat := ∑ (C : category), (comprehension_cat_structure C). - Definition typecat_to_comprehension_cat : typecat → comprehension_cat. Proof. @@ -507,4 +634,12 @@ Section TypeCat_ComprehensionCat. apply (typecat_to_comprehension_cat_structure (pr2 TC)). Defined. + Definition typecat_from_comprehension_cat + : comprehension_cat → typecat. + Proof. + intros CC. + exists (pr1 CC). + apply (typecat_structure_from_comprehension_cat (pr2 CC)). + Defined. + End TypeCat_ComprehensionCat. From 834ae0b6e7a4cc7cf571c2f33f98d437cd8c944d Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 27 Apr 2020 03:25:52 +0300 Subject: [PATCH 02/18] Sketch a proof of equivalence for typecat and comprehension_cat --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 34 ++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 57ba517f..93946735 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -486,6 +486,9 @@ End TypeCat_Disp_Functor. (* TODO: move upstream *) Definition comprehension_cat := ∑ (C : category), (comprehension_cat_structure C). +Coercion category_of_comprehension_cat (C : comprehension_cat) := pr1 C. +Coercion structure_of_comprehension_cat (C : comprehension_cat) := pr2 C. + Section ComprehensionCat_TypeCat. Context {C : category}. Context (CC : comprehension_cat_structure C). @@ -641,5 +644,36 @@ Section TypeCat_ComprehensionCat. exists (pr1 CC). apply (typecat_structure_from_comprehension_cat (pr2 CC)). Defined. + + Definition fully_faithful_comprehension_cat_structure + {C : category} (CC : comprehension_cat_structure C) + := disp_functor_ff (pr1 (pr2 (pr2 CC))). + + Definition typecat_comprehension_cat_structure_weq + {C : category} + : typecat_structure C ≃ ∑ CC : comprehension_cat_structure C, fully_faithful_comprehension_cat_structure CC. + Proof. + use weq_iso. + - intros TC. + exact (typecat_to_comprehension_cat_structure TC ,, typecat_disp_functor_ff TC). + - intros CC. apply (typecat_structure_from_comprehension_cat (pr1 CC)). + - intros TC. + repeat use total2_paths_f. + + apply idpath. + + apply idpath. + + apply idpath. + + apply idpath. + + apply idpath. + + apply idpath. + + apply funextsec. intros Γ. + apply funextsec. intros A. + apply funextsec. intros Γ'. + apply funextsec. intros f. + apply isaprop_isPullback. + - intros ff_CC. + repeat use total2_paths_f. + + apply idpath. + + (* STUCK: need to think, this might be impossible *) (* apply idpath. *) + Abort. End TypeCat_ComprehensionCat. From 770feed0bfd1a6171e089bc626c9fe637231691a Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 30 Apr 2020 00:53:36 +0300 Subject: [PATCH 03/18] Save work-in-progress --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 295 +++++++++++++++++++++ 1 file changed, 295 insertions(+) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 93946735..bcd4b076 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -62,6 +62,92 @@ Section Auxiliary. apply idpath. Defined. + Definition disp_ff_functor_to_on_objects + {C : category} + (D' : disp_cat C) + : UU + := ∑ (obd : C → UU) + , ∏ (Γ : C), obd Γ → D' Γ. + + Definition disp_ff_functor_to_on_morphisms + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : UU + := ∑ (mord : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (id_comp_d : disp_cat_id_comp C (_ ,, mord)) + (axioms_d : disp_cat_axioms C (_,, id_comp_d)) + (functor_mord : + ∏ x y (xx : ((_,,axioms_d) : disp_cat C) x) (yy : pr1 D y) (f : x --> y), + (xx -->[f] yy) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) + (functor_axioms_d : @disp_functor_axioms + C C (functor_identity _) + (_,,axioms_d) D' + (pr2 D ,, functor_mord)) + , disp_functor_ff ((_ ,, functor_axioms_d) + : disp_functor (functor_identity C) + (_ ,, axioms_d) D'). + + Definition disp_ff_functor_to + {C : category} (D' : disp_cat C) + : UU + := ∑ (D : disp_ff_functor_to_on_objects D'), disp_ff_functor_to_on_morphisms D. + + Definition source_disp_cat_of_disp_ff_functor + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to D') + : disp_cat C. + Proof. + set (axioms_d := pr1 (pr2 (pr2 (pr2 D)))). + exact (_ ,, axioms_d). + Defined. + + Definition disp_functor_of_disp_ff_functor + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to D') + : disp_functor (functor_identity _) (source_disp_cat_of_disp_ff_functor D) D'. + Proof. + set (functor_axioms_d := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))). + exact (_ ,, functor_axioms_d). + Defined. + + Definition disp_ff_functor_is_ff + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to D') + : disp_functor_ff (disp_functor_of_disp_ff_functor D) + := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))). + + Lemma isaprop_disp_source_functor_on_morphisms + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : isaprop (disp_ff_functor_to_on_morphisms D). + Proof. + intros X Y. + use tpair. + - use total2_paths_f. + + apply funextsec. intros Γ. + apply funextsec. intros Γ'. + apply funextsec. intros A. + apply funextsec. intros B. + apply funextsec. intros f. + set (wX := (_ ,, disp_ff_functor_is_ff (D,,X) Γ Γ' A B f)). + set (wY := (_ ,, disp_ff_functor_is_ff (D,,Y) Γ Γ' A B f)). + apply univalenceweq. (* FIXME: is this correct application? *) + apply (weqcomp wX (invweq wY)). + + use total2_paths_f. + * use dirprod_paths. + -- apply funextsec. intros Γ. + apply funextsec. intros A. + set (Fid_axiom_X := pr1 (pr2 (disp_functor_of_disp_ff_functor (D,,X))) Γ A). + set (Fid_axiom_Y := pr1 (pr2 (disp_functor_of_disp_ff_functor (D,,Y))) Γ A). + (* TODO: work in progress *) + (* + maponpaths (Fid_axiom_X @ !Fid_axiom_Y). + set (wX := (_ ,, disp_ff_functor_is_ff (D,,X) Γ Γ A A (identity _))). + set (wY := (_ ,, disp_ff_functor_is_ff (D,,Y) Γ Γ A A (identity _))). + apply univalenceweq. + *) + Abort. + End Auxiliary. Section TypeCat_ObjExt. @@ -649,6 +735,215 @@ Section TypeCat_ComprehensionCat. {C : category} (CC : comprehension_cat_structure C) := disp_functor_ff (pr1 (pr2 (pr2 CC))). + Print disp_cat_ob_mor. + + Print cleaving. + Check cartesian_lift. + + Definition ff_comprehension_cat_structure (C : category) : UU + := ∑ (obd : C → UU) + (functor_on_obd : ∏ (Γ : C), obd Γ → disp_codomain C Γ) + (cleaving_on_obd : ∏ (Γ Γ' : C) (f : Γ' --> Γ) (A : obd Γ), + ∑ (A' : obd Γ') + (ff : functor_on_obd _ A' -->[f] functor_on_obd _ A), + is_cartesian ff) + , unit. + + Definition ff_comprehension_cat_structure_has_morphisms (C : category) + (ff_CC : ff_comprehension_cat_structure C) + : UU + := ∑ (mord : ∏ (Γ Γ' : C), (pr1 ff_CC Γ) → (pr1 ff_CC Γ') → (Γ --> Γ') → UU) + (id_comp_d : disp_cat_id_comp C (_ ,, mord)) + (axioms_d : disp_cat_axioms C (_,, id_comp_d)) + (functor_mord : + ∏ x y (xx : ((_,,axioms_d) : disp_cat C) x) (yy : pr1 ff_CC y) (f : x --> y), + (xx -->[f] yy) -> (pr1 (pr2 ff_CC) _ xx -->[ f ] pr1 (pr2 ff_CC) _ yy)) + (functor_axioms_d : @disp_functor_axioms + C C (functor_identity _) + (_,,axioms_d) (disp_codomain C) + (pr1 (pr2 ff_CC) ,, functor_mord)) + (ff : disp_functor_ff ((_ ,, functor_axioms_d) + : disp_functor (functor_identity C) + (_ ,, axioms_d) (disp_codomain C))) + , unit. + + Definition isaprop_ff_comprehension_cat_structure_has_morphisms {C : category} + (ff_CC : ff_comprehension_cat_structure C) + : isaprop (ff_comprehension_cat_structure_has_morphisms C ff_CC). + Proof. + intros X Y. + use tpair. + - use total2_paths_f. + + + Defined. + + Definition ff_comprehension_cat_structure_disp_cat {C : category} + : ff_comprehension_cat_structure C → disp_cat C. + Proof. + intros ff_CC. + set (obd := pr1 ff_CC). + set (functor_on_obd := pr1 (pr2 ff_CC)). + set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). + use tpair. + - use tpair. + + exists obd. + intros Γ Δ A B f. + exact (functor_on_obd _ A -->[f] functor_on_obd _ B). + + use tpair. + * intros Γ A. + apply id_disp. + * intros Γ Γ' Γ'' A A' A'' f g. + apply comp_disp. + - repeat use make_dirprod. + + intros ? ? ? ? ? ?. apply id_left_disp. + + intros ? ? ? ? ? ?. apply id_right_disp. + + intros ? ? ? ? ? ? ? ? ? ? ? ? ? ?. apply assoc_disp. + + intros ? ? ? ? ? ?. apply homsets_disp. + Defined. + + Definition ff_comprehension_cat_structure_disp_functor {C : category} + (ff_CC : ff_comprehension_cat_structure C) + : disp_functor (functor_identity _) + (ff_comprehension_cat_structure_disp_cat ff_CC) + (disp_codomain C). + Proof. + set (obd := pr1 ff_CC). + set (functor_on_obd := pr1 (pr2 ff_CC)). + set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). + repeat use tpair. + - exact functor_on_obd. + - intros ? ? ? ? ?. apply idfun. + - intros ? ?. apply idpath. + - intros ? ? ? ? ? ? ? ? ? ?. apply idpath. + Defined. + + Definition ff_comprehension_cat_structure_disp_functor_is_ff {C : category} + (ff_CC : ff_comprehension_cat_structure C) + : disp_functor_ff (ff_comprehension_cat_structure_disp_functor ff_CC). + Proof. + set (obd := pr1 ff_CC). + set (functor_on_obd := pr1 (pr2 ff_CC)). + set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). + unfold disp_functor_ff. + intros Γ Γ' A A' f. + use isweq_iso. + - apply idfun. + - intros k. apply idpath. + - intros k. apply idpath. + Defined. + + Definition ff_comprehension_cat_structure_cleaving {C : category} + (ff_CC : ff_comprehension_cat_structure C) + : cleaving (ff_comprehension_cat_structure_disp_cat ff_CC). + Proof. + intros Γ Γ' f A. + set (obd := pr1 ff_CC). + set (functor_on_obd := pr1 (pr2 ff_CC)). + set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). + set (ff := cleaving_on_obd Γ Γ' f A). + use tpair. + - apply (pr1 ff). + - use tpair. + + apply (pr1 (pr2 ff)). + + intros Δ g B k. + use iscontrweqf. + 3: { + use (pr2 (pr2 ff)). + - exact Δ. + - exact g. + - exact (functor_on_obd Δ B). + - exact k. + } + apply idweq. + Defined. + + Definition ff_comprehension_cat_structure_disp_functor_is_cartesian {C : category} + (ff_CC : ff_comprehension_cat_structure C) + : is_cartesian_disp_functor (ff_comprehension_cat_structure_disp_functor ff_CC). + Proof. + use cartesian_functor_from_cleaving. + - apply (ff_comprehension_cat_structure_cleaving ff_CC). + - intros Γ Γ' f A. + set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). + set (ff := cleaving_on_obd Γ Γ' f A). + apply (pr2 (pr2 ff)). + Defined. + + Definition ff_comprehension_cat_structure_to_comprehension_cat_structure + {C : category} + : ff_comprehension_cat_structure C + → ∑ (CC : comprehension_cat_structure C), + fully_faithful_comprehension_cat_structure CC. + Proof. + intros ff_CC. + use tpair. + - use tpair. + + apply (ff_comprehension_cat_structure_disp_cat ff_CC). + + use tpair. + * apply (ff_comprehension_cat_structure_cleaving ff_CC). + * use tpair. + -- apply (ff_comprehension_cat_structure_disp_functor ff_CC). + -- apply (ff_comprehension_cat_structure_disp_functor_is_cartesian ff_CC). + - apply (ff_comprehension_cat_structure_disp_functor_is_ff ff_CC). + Defined. + + Definition ff_comprehension_cat_structure_from_comprehension_cat_structure + {C : category} + : (∑ (CC : comprehension_cat_structure C), + fully_faithful_comprehension_cat_structure CC) + → ff_comprehension_cat_structure C. + Proof. + intros CC. + use tpair. + - apply (ob_disp (pr1 (pr1 CC))). + - use tpair. + + intros Γ A. apply (disp_functor_on_objects (pr1 (pr2 (pr2 (pr1 CC)))) A). + + use tpair. + * intros Γ Γ' f A. + set (ff := pr1 (pr2 (pr1 CC)) Γ Γ' f A). + exists (pr1 ff). + use tpair. + -- use (disp_functor_on_morphisms (pr1 (pr2 (pr2 (pr1 CC))))). + apply (pr1 (pr2 ff)). + -- use (pr2 (pr2 (pr2 (pr1 CC)))). + apply (pr2 (pr2 ff)). + * apply tt. + Defined. + + + Definition ff_comprehension_cat_structure_weq (C : category) + : ff_comprehension_cat_structure C + ≃ ∑ (CC : comprehension_cat_structure C), + fully_faithful_comprehension_cat_structure CC. + Proof. + Search weq. + use weq_iso. + - apply ff_comprehension_cat_structure_to_comprehension_cat_structure. + - apply ff_comprehension_cat_structure_from_comprehension_cat_structure. + - intros ff_CC. + repeat use total2_paths_f. + + apply idpath. + + apply idpath. + + apply funextsec. intros ?. + apply funextsec. intros ?. + apply funextsec. intros ?. + apply funextsec. intros ?. + use total2_paths_f. + * apply idpath. + * use total2_paths_f. + -- apply idpath. + -- apply isaprop_is_cartesian. + + apply isapropunit. + - intros CC. + repeat use total2_paths_f. + + apply idpath. + + apply idpath. + Defined. + + Definition ff_comprehension_cat_structure_weq + {C : category} + : ∑ CC : comprehension_cat_structure C, fully_faithful_comprehension_cat_structure CC. + Definition typecat_comprehension_cat_structure_weq {C : category} : typecat_structure C ≃ ∑ CC : comprehension_cat_structure C, fully_faithful_comprehension_cat_structure CC. From 275df5c22b6323fc28cdbc4b2ca756e8937904e1 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 30 Apr 2020 01:03:49 +0300 Subject: [PATCH 04/18] Restructure ff_comprehension_cat in preparation to use more general disp_ff_functor_to --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 242 ++------------------- 1 file changed, 20 insertions(+), 222 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index bcd4b076..885ed838 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -110,6 +110,8 @@ Section Auxiliary. exact (_ ,, functor_axioms_d). Defined. + Coercion disp_functor_of_disp_ff_functor : disp_ff_functor_to >-> disp_functor. + Definition disp_ff_functor_is_ff {C : category} {D' : disp_cat C} (D : disp_ff_functor_to D') @@ -740,235 +742,31 @@ Section TypeCat_ComprehensionCat. Print cleaving. Check cartesian_lift. - Definition ff_comprehension_cat_structure (C : category) : UU - := ∑ (obd : C → UU) - (functor_on_obd : ∏ (Γ : C), obd Γ → disp_codomain C Γ) - (cleaving_on_obd : ∏ (Γ Γ' : C) (f : Γ' --> Γ) (A : obd Γ), - ∑ (A' : obd Γ') - (ff : functor_on_obd _ A' -->[f] functor_on_obd _ A), - is_cartesian ff) - , unit. - - Definition ff_comprehension_cat_structure_has_morphisms (C : category) - (ff_CC : ff_comprehension_cat_structure C) - : UU - := ∑ (mord : ∏ (Γ Γ' : C), (pr1 ff_CC Γ) → (pr1 ff_CC Γ') → (Γ --> Γ') → UU) - (id_comp_d : disp_cat_id_comp C (_ ,, mord)) - (axioms_d : disp_cat_axioms C (_,, id_comp_d)) - (functor_mord : - ∏ x y (xx : ((_,,axioms_d) : disp_cat C) x) (yy : pr1 ff_CC y) (f : x --> y), - (xx -->[f] yy) -> (pr1 (pr2 ff_CC) _ xx -->[ f ] pr1 (pr2 ff_CC) _ yy)) - (functor_axioms_d : @disp_functor_axioms - C C (functor_identity _) - (_,,axioms_d) (disp_codomain C) - (pr1 (pr2 ff_CC) ,, functor_mord)) - (ff : disp_functor_ff ((_ ,, functor_axioms_d) - : disp_functor (functor_identity C) - (_ ,, axioms_d) (disp_codomain C))) - , unit. - - Definition isaprop_ff_comprehension_cat_structure_has_morphisms {C : category} - (ff_CC : ff_comprehension_cat_structure C) - : isaprop (ff_comprehension_cat_structure_has_morphisms C ff_CC). - Proof. - intros X Y. - use tpair. - - use total2_paths_f. - + - Defined. - - Definition ff_comprehension_cat_structure_disp_cat {C : category} - : ff_comprehension_cat_structure C → disp_cat C. - Proof. - intros ff_CC. - set (obd := pr1 ff_CC). - set (functor_on_obd := pr1 (pr2 ff_CC)). - set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). - use tpair. - - use tpair. - + exists obd. - intros Γ Δ A B f. - exact (functor_on_obd _ A -->[f] functor_on_obd _ B). - + use tpair. - * intros Γ A. - apply id_disp. - * intros Γ Γ' Γ'' A A' A'' f g. - apply comp_disp. - - repeat use make_dirprod. - + intros ? ? ? ? ? ?. apply id_left_disp. - + intros ? ? ? ? ? ?. apply id_right_disp. - + intros ? ? ? ? ? ? ? ? ? ? ? ? ? ?. apply assoc_disp. - + intros ? ? ? ? ? ?. apply homsets_disp. - Defined. - - Definition ff_comprehension_cat_structure_disp_functor {C : category} - (ff_CC : ff_comprehension_cat_structure C) - : disp_functor (functor_identity _) - (ff_comprehension_cat_structure_disp_cat ff_CC) - (disp_codomain C). - Proof. - set (obd := pr1 ff_CC). - set (functor_on_obd := pr1 (pr2 ff_CC)). - set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). - repeat use tpair. - - exact functor_on_obd. - - intros ? ? ? ? ?. apply idfun. - - intros ? ?. apply idpath. - - intros ? ? ? ? ? ? ? ? ? ?. apply idpath. - Defined. - - Definition ff_comprehension_cat_structure_disp_functor_is_ff {C : category} - (ff_CC : ff_comprehension_cat_structure C) - : disp_functor_ff (ff_comprehension_cat_structure_disp_functor ff_CC). - Proof. - set (obd := pr1 ff_CC). - set (functor_on_obd := pr1 (pr2 ff_CC)). - set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). - unfold disp_functor_ff. - intros Γ Γ' A A' f. - use isweq_iso. - - apply idfun. - - intros k. apply idpath. - - intros k. apply idpath. - Defined. - - Definition ff_comprehension_cat_structure_cleaving {C : category} - (ff_CC : ff_comprehension_cat_structure C) - : cleaving (ff_comprehension_cat_structure_disp_cat ff_CC). + Definition typecat_obj_ext_structure_disp_ff_functor_to_codomain_weq + (C : category) + : typecat_obj_ext_structure C ≃ disp_ff_functor_to (disp_codomain C). Proof. - intros Γ Γ' f A. - set (obd := pr1 ff_CC). - set (functor_on_obd := pr1 (pr2 ff_CC)). - set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). - set (ff := cleaving_on_obd Γ Γ' f A). - use tpair. - - apply (pr1 ff). - - use tpair. - + apply (pr1 (pr2 ff)). - + intros Δ g B k. - use iscontrweqf. - 3: { - use (pr2 (pr2 ff)). - - exact Δ. - - exact g. - - exact (functor_on_obd Δ B). - - exact k. - } - apply idweq. - Defined. - - Definition ff_comprehension_cat_structure_disp_functor_is_cartesian {C : category} - (ff_CC : ff_comprehension_cat_structure C) - : is_cartesian_disp_functor (ff_comprehension_cat_structure_disp_functor ff_CC). - Proof. - use cartesian_functor_from_cleaving. - - apply (ff_comprehension_cat_structure_cleaving ff_CC). - - intros Γ Γ' f A. - set (cleaving_on_obd := pr1 (pr2 (pr2 ff_CC))). - set (ff := cleaving_on_obd Γ Γ' f A). - apply (pr2 (pr2 ff)). - Defined. - - Definition ff_comprehension_cat_structure_to_comprehension_cat_structure - {C : category} - : ff_comprehension_cat_structure C - → ∑ (CC : comprehension_cat_structure C), - fully_faithful_comprehension_cat_structure CC. - Proof. - intros ff_CC. - use tpair. - - use tpair. - + apply (ff_comprehension_cat_structure_disp_cat ff_CC). - + use tpair. - * apply (ff_comprehension_cat_structure_cleaving ff_CC). - * use tpair. - -- apply (ff_comprehension_cat_structure_disp_functor ff_CC). - -- apply (ff_comprehension_cat_structure_disp_functor_is_cartesian ff_CC). - - apply (ff_comprehension_cat_structure_disp_functor_is_ff ff_CC). - Defined. - - Definition ff_comprehension_cat_structure_from_comprehension_cat_structure - {C : category} - : (∑ (CC : comprehension_cat_structure C), - fully_faithful_comprehension_cat_structure CC) - → ff_comprehension_cat_structure C. - Proof. - intros CC. - use tpair. - - apply (ob_disp (pr1 (pr1 CC))). - - use tpair. - + intros Γ A. apply (disp_functor_on_objects (pr1 (pr2 (pr2 (pr1 CC)))) A). - + use tpair. - * intros Γ Γ' f A. - set (ff := pr1 (pr2 (pr1 CC)) Γ Γ' f A). - exists (pr1 ff). - use tpair. - -- use (disp_functor_on_morphisms (pr1 (pr2 (pr2 (pr1 CC))))). - apply (pr1 (pr2 ff)). - -- use (pr2 (pr2 (pr2 (pr1 CC)))). - apply (pr2 (pr2 ff)). - * apply tt. - Defined. + (* TODO *) + Abort. + Definition ff_comprehension_cat_structure (C : category) : UU + := ∑ (F : disp_ff_functor_to (disp_codomain C)), + cleaving (source_disp_cat_of_disp_ff_functor F) + × is_cartesian_disp_functor F. - Definition ff_comprehension_cat_structure_weq (C : category) - : ff_comprehension_cat_structure C - ≃ ∑ (CC : comprehension_cat_structure C), - fully_faithful_comprehension_cat_structure CC. + Definition typecat_ff_comprehension_cat_structure_weq (C : category) + : typecat_structure C ≃ ff_comprehension_cat_structure C. Proof. - Search weq. - use weq_iso. - - apply ff_comprehension_cat_structure_to_comprehension_cat_structure. - - apply ff_comprehension_cat_structure_from_comprehension_cat_structure. - - intros ff_CC. - repeat use total2_paths_f. - + apply idpath. - + apply idpath. - + apply funextsec. intros ?. - apply funextsec. intros ?. - apply funextsec. intros ?. - apply funextsec. intros ?. - use total2_paths_f. - * apply idpath. - * use total2_paths_f. - -- apply idpath. - -- apply isaprop_is_cartesian. - + apply isapropunit. - - intros CC. - repeat use total2_paths_f. - + apply idpath. - + apply idpath. - Defined. + (* TODO *) + Abort. - Definition ff_comprehension_cat_structure_weq - {C : category} - : ∑ CC : comprehension_cat_structure C, fully_faithful_comprehension_cat_structure CC. + Definition ff_comprehension_cat : UU + := ∑ (C : category), ff_comprehension_cat_structure C. - Definition typecat_comprehension_cat_structure_weq - {C : category} - : typecat_structure C ≃ ∑ CC : comprehension_cat_structure C, fully_faithful_comprehension_cat_structure CC. + Definition typecat_ff_comprehension_cat_weq (C : category) + : typecat ≃ ff_comprehension_cat. Proof. - use weq_iso. - - intros TC. - exact (typecat_to_comprehension_cat_structure TC ,, typecat_disp_functor_ff TC). - - intros CC. apply (typecat_structure_from_comprehension_cat (pr1 CC)). - - intros TC. - repeat use total2_paths_f. - + apply idpath. - + apply idpath. - + apply idpath. - + apply idpath. - + apply idpath. - + apply idpath. - + apply funextsec. intros Γ. - apply funextsec. intros A. - apply funextsec. intros Γ'. - apply funextsec. intros f. - apply isaprop_isPullback. - - intros ff_CC. - repeat use total2_paths_f. - + apply idpath. - + (* STUCK: need to think, this might be impossible *) (* apply idpath. *) + (* TODO *) Abort. End TypeCat_ComprehensionCat. From 9de1cf5aaad5ea2599c0f00dfb7ec69fbc4db473 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 6 May 2020 06:34:24 +0300 Subject: [PATCH 05/18] WIP --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 63 ++++++++++++++++++++-- 1 file changed, 60 insertions(+), 3 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 885ed838..af4112ad 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -69,12 +69,12 @@ Section Auxiliary. := ∑ (obd : C → UU) , ∏ (Γ : C), obd Γ → D' Γ. - Definition disp_ff_functor_to_on_morphisms + Definition disp_ff_functor_to_on_morphisms' {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') + (mord : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) : UU - := ∑ (mord : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - (id_comp_d : disp_cat_id_comp C (_ ,, mord)) + := ∑ (id_comp_d : disp_cat_id_comp C (_ ,, mord)) (axioms_d : disp_cat_axioms C (_,, id_comp_d)) (functor_mord : ∏ x y (xx : ((_,,axioms_d) : disp_cat C) x) (yy : pr1 D y) (f : x --> y), @@ -87,6 +87,13 @@ Section Auxiliary. : disp_functor (functor_identity C) (_ ,, axioms_d) D'). + Definition disp_ff_functor_to_on_morphisms + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : UU + := ∑ (mord : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + , disp_ff_functor_to_on_morphisms' D mord. + Definition disp_ff_functor_to {C : category} (D' : disp_cat C) : UU @@ -118,6 +125,41 @@ Section Auxiliary. : disp_functor_ff (disp_functor_of_disp_ff_functor D) := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))). + Definition disp_ff_functor_mor_eq + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (m1 m2 : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (e_mor : m1 = m2) + (X : disp_ff_functor_to_on_morphisms' D m1) + (Y : disp_ff_functor_to_on_morphisms' D m2) + : transportf _ e_mor X = Y. + Proof. + induction e_mor. + etrans. apply idpath_transportf. + use total2_paths_f. + - use dirprod_paths. + + apply funextsec. intros Γ. + apply funextsec. intros A. + + set (id_disp_X := pr1 (pr1 X) Γ A). + set (id_disp_Y := pr1 (pr1 Y) Γ A). + + (* STUCK *) + + (* + apply funextsec. intros Γ. + apply funextsec. intros A. + set (id_disp_1 := pr1 id_comp_d1). + set (id_disp_2 := pr1 id_comp_d2). + set (e1 := pr1 axioms_d1 Γ Γ _ A A (id_disp_2 Γ A)). + set (e2 := pr1 (dirprod_pr2 axioms_d2) Γ Γ _ A A (id_disp_1 Γ A)). + unfold id_disp, id_disp_1, id_disp_2 in *. + simpl in *. + Check (!e1 @ e2). + *) + Abort. + + Lemma isaprop_disp_source_functor_on_morphisms {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') @@ -139,8 +181,23 @@ Section Auxiliary. * use dirprod_paths. -- apply funextsec. intros Γ. apply funextsec. intros A. + set (Fid_axiom_X := pr1 (pr2 (disp_functor_of_disp_ff_functor (D,,X))) Γ A). set (Fid_axiom_Y := pr1 (pr2 (disp_functor_of_disp_ff_functor (D,,Y))) Γ A). + + set (id_disp_X := pr1 (pr1 (pr2 X))). + set (id_disp_Y := pr1 (pr1 (pr2 Y))). + + (* + + Check (pr1 (pr1 (pr2 (pr2 X))) Γ Γ _ A A (id_disp_Y Γ A)). + set (Did_axiom_X := + + simpl in *. + Check Fid_axiom_Y. + Check Fid_axiom_X @ !Fid_axiom_Y. + Search weq. + *) (* TODO: work in progress *) (* maponpaths (Fid_axiom_X @ !Fid_axiom_Y). From 26b8c6b4628963934fdf1a7b70413407d33ce2fe Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 6 May 2020 21:35:37 +0300 Subject: [PATCH 06/18] Add proof that disp_ff_functor_on_morphisms is contractible --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 319 +++++++++++++-------- 1 file changed, 199 insertions(+), 120 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index af4112ad..7420b2cb 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -69,143 +69,222 @@ Section Auxiliary. := ∑ (obd : C → UU) , ∏ (Γ : C), obd Γ → D' Γ. - Definition disp_ff_functor_to_on_morphisms' - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mord : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - : UU - := ∑ (id_comp_d : disp_cat_id_comp C (_ ,, mord)) - (axioms_d : disp_cat_axioms C (_,, id_comp_d)) - (functor_mord : - ∏ x y (xx : ((_,,axioms_d) : disp_cat C) x) (yy : pr1 D y) (f : x --> y), - (xx -->[f] yy) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) - (functor_axioms_d : @disp_functor_axioms - C C (functor_identity _) - (_,,axioms_d) D' - (pr2 D ,, functor_mord)) - , disp_functor_ff ((_ ,, functor_axioms_d) - : disp_functor (functor_identity C) - (_ ,, axioms_d) D'). - - Definition disp_ff_functor_to_on_morphisms - {C : category} {D' : disp_cat C} + Check weqtotaltoforall. + + Lemma weqtotaltoforall3 {X : UU} + (P1 : X → UU) + (P2 : ∏ x : X, P1 x → UU) + (P3 : ∏ (x : X) (y : P1 x), P2 x y → UU) + : (∑ (p1 : ∏ x : X, P1 x) (p2 : ∏ x : X, P2 x (p1 x)), ∏ x : X, P3 x (p1 x) (p2 x)) + ≃ (∏ x : X, ∑ (p1 : P1 x) (p2 : P2 x p1), P3 x p1 p2). + Proof. + eapply weqcomp. + apply (weqtotal2asstol + (λ p1, ∏ x : X, P2 x (p1 x)) + (λ p12, ∏ x : X, P3 x (pr1 p12 x) (pr2 p12 x)) + ). + eapply weqcomp. + use weqtotal2. 3: apply weqtotaltoforall. + - exact (λ p12, ∏ x : X, P3 x (pr1 (p12 x)) (pr2 (p12 x))). + - intros x. apply idweq. + + - eapply weqcomp. + apply (weqtotaltoforall + (λ x : X, ∑ y : P1 x, P2 x y) + (λ (x : X) p12, P3 x (pr1 p12) (pr2 p12)) + ). + apply weqonsecfibers. + intros x. + apply weqtotal2asstor. + Defined. + + Definition disp_ff_functor_on_morphisms_sop + {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') : UU - := ∑ (mord : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - , disp_ff_functor_to_on_morphisms' D mord. + := ∑ (mord : ∏ Γ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (functor_mord : ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord _ _ A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + , ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord Γ Γ' A A' f). - Definition disp_ff_functor_to - {C : category} (D' : disp_cat C) + Definition disp_ff_functor_on_morphisms_pos + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') : UU - := ∑ (D : disp_ff_functor_to_on_objects D'), disp_ff_functor_to_on_morphisms D. + := ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ'), + ∑ (mord : UU), mord ≃ (pr2 D _ A -->[ f ] pr2 D _ A'). - Definition source_disp_cat_of_disp_ff_functor + Definition disp_ff_functor_on_morphisms_sop_pos_weq {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to D') - : disp_cat C. + (D : disp_ff_functor_to_on_objects D') + : disp_ff_functor_on_morphisms_sop D ≃ disp_ff_functor_on_morphisms_pos D. Proof. - set (axioms_d := pr1 (pr2 (pr2 (pr2 D)))). - exact (_ ,, axioms_d). + eapply weqcomp. + apply (weqtotaltoforall3 + (λ Γ, ∏ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (λ Γ mord, ∏ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord _ A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ Γ mord functor_mord, + ∏ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord Γ' A A' f))). + apply weqonsecfibers. intros Γ. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (λ Γ' mord, ∏ (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ Γ' mord functor_mord, + ∏ (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord A A' f))). + apply weqonsecfibers. intros Γ'. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ A, (pr1 D Γ') → (Γ --> Γ') → UU) + (λ A mord, ∏ (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ A mord functor_mord, + ∏ (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord A' f))). + apply weqonsecfibers. intros A. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ A', (Γ --> Γ') → UU) + (λ A' mord, ∏ (f : Γ --> Γ') + , (mord f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ A' mord functor_mord, + ∏ (f : Γ --> Γ') + , isweq (functor_mord f))). + apply weqonsecfibers. intros A'. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ f, UU) + (λ f mord, mord -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ f mord functor_mord, isweq functor_mord)). + apply idweq. Defined. - Definition disp_functor_of_disp_ff_functor + Definition disp_ff_functor_on_morphisms_pos_iscontr {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to D') - : disp_functor (functor_identity _) (source_disp_cat_of_disp_ff_functor D) D'. + (D : disp_ff_functor_to_on_objects D') + : iscontr (disp_ff_functor_on_morphisms_pos D). Proof. - set (functor_axioms_d := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))). - exact (_ ,, functor_axioms_d). + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros f. + use (@iscontrweqf (∑ mord : UU, mord = pr2 D Γ A -->[f] pr2 D Γ' A')). + - use (weqtotal2 (idweq _)). intros mord. apply univalenceweq. + - apply iscontrcoconustot. Defined. - Coercion disp_functor_of_disp_ff_functor : disp_ff_functor_to >-> disp_functor. - - Definition disp_ff_functor_is_ff - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to D') - : disp_functor_ff (disp_functor_of_disp_ff_functor D) - := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))). - - Definition disp_ff_functor_mor_eq + Definition disp_ff_functor_on_morphisms_pos_isaprop {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') - (m1 m2 : ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - (e_mor : m1 = m2) - (X : disp_ff_functor_to_on_morphisms' D m1) - (Y : disp_ff_functor_to_on_morphisms' D m2) - : transportf _ e_mor X = Y. + : isaprop (disp_ff_functor_on_morphisms_pos D). Proof. - induction e_mor. - etrans. apply idpath_transportf. - use total2_paths_f. - - use dirprod_paths. - + apply funextsec. intros Γ. - apply funextsec. intros A. - - set (id_disp_X := pr1 (pr1 X) Γ A). - set (id_disp_Y := pr1 (pr1 Y) Γ A). - - (* STUCK *) - - (* - apply funextsec. intros Γ. - apply funextsec. intros A. - set (id_disp_1 := pr1 id_comp_d1). - set (id_disp_2 := pr1 id_comp_d2). - set (e1 := pr1 axioms_d1 Γ Γ _ A A (id_disp_2 Γ A)). - set (e2 := pr1 (dirprod_pr2 axioms_d2) Γ Γ _ A A (id_disp_1 Γ A)). - unfold id_disp, id_disp_1, id_disp_2 in *. - simpl in *. - Check (!e1 @ e2). - *) - Abort. - + apply isapropifcontr, disp_ff_functor_on_morphisms_pos_iscontr. + Defined. - Lemma isaprop_disp_source_functor_on_morphisms - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : isaprop (disp_ff_functor_to_on_morphisms D). - Proof. - intros X Y. - use tpair. - - use total2_paths_f. - + apply funextsec. intros Γ. - apply funextsec. intros Γ'. - apply funextsec. intros A. - apply funextsec. intros B. - apply funextsec. intros f. - set (wX := (_ ,, disp_ff_functor_is_ff (D,,X) Γ Γ' A B f)). - set (wY := (_ ,, disp_ff_functor_is_ff (D,,Y) Γ Γ' A B f)). - apply univalenceweq. (* FIXME: is this correct application? *) - apply (weqcomp wX (invweq wY)). - + use total2_paths_f. - * use dirprod_paths. - -- apply funextsec. intros Γ. - apply funextsec. intros A. - - set (Fid_axiom_X := pr1 (pr2 (disp_functor_of_disp_ff_functor (D,,X))) Γ A). - set (Fid_axiom_Y := pr1 (pr2 (disp_functor_of_disp_ff_functor (D,,Y))) Γ A). - - set (id_disp_X := pr1 (pr1 (pr2 X))). - set (id_disp_Y := pr1 (pr1 (pr2 Y))). - - (* - - Check (pr1 (pr1 (pr2 (pr2 X))) Γ Γ _ A A (id_disp_Y Γ A)). - set (Did_axiom_X := - - simpl in *. - Check Fid_axiom_Y. - Check Fid_axiom_X @ !Fid_axiom_Y. - Search weq. - *) - (* TODO: work in progress *) - (* - maponpaths (Fid_axiom_X @ !Fid_axiom_Y). - set (wX := (_ ,, disp_ff_functor_is_ff (D,,X) Γ Γ A A (identity _))). - set (wY := (_ ,, disp_ff_functor_is_ff (D,,Y) Γ Γ A A (identity _))). - apply univalenceweq. - *) - Abort. + (* Types for parts of a fully faithful functor that rely on morphisms *) + Section disp_ff_functor_to_on_morphisms. + + Context {C : category} {D' : disp_cat C}. + Context (D : disp_ff_functor_to_on_objects D'). + + Definition disp_ff_functor_source_mor : UU + := ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU. + + Definition disp_ff_functor_source_id_comp + (mord : disp_ff_functor_source_mor) : UU + := disp_cat_id_comp C (pr1 D,, mord). + + Definition disp_ff_functor_source_axioms + (mord : disp_ff_functor_source_mor) + (id_comp_d : disp_ff_functor_source_id_comp mord) + : UU + := disp_cat_axioms C ((pr1 D ,, mord) ,, id_comp_d). + + Definition disp_ff_functor_on_morphisms + (mord : disp_ff_functor_source_mor) + : UU + := ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y) + , (mord _ _ xx yy f) -> (pr2 D _ xx -->[ f ] pr2 D _ yy). + + Definition disp_ff_functor_axioms + (mord : disp_ff_functor_source_mor) + (id_comp_d : disp_ff_functor_source_id_comp mord) + (axioms_d : disp_ff_functor_source_axioms mord id_comp_d) + (functor_mord : disp_ff_functor_on_morphisms mord) + : UU + := @disp_functor_axioms + C C (functor_identity _) + (((pr1 D ,, mord) ,, id_comp_d) ,, axioms_d) D' + (pr2 D ,, functor_mord). + + Definition disp_ff_functor_ff + (mord : disp_ff_functor_source_mor) + (functor_mord : disp_ff_functor_on_morphisms mord) + : UU + := ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord Γ Γ' A A' f). + + Definition disp_ff_functor_to_on_morphisms' + (mord : disp_ff_functor_source_mor) + : UU + := ∑ (id_comp_d : disp_ff_functor_source_id_comp mord) + (axioms_d : disp_ff_functor_source_axioms mord id_comp_d) + (functor_mord : disp_ff_functor_on_morphisms mord) + (functor_axioms_d : disp_ff_functor_axioms mord id_comp_d axioms_d functor_mord) + , disp_ff_functor_ff mord functor_mord. + + Definition disp_ff_functor_to_on_morphisms + : UU + := ∑ (mord : disp_ff_functor_source_mor) + , disp_ff_functor_to_on_morphisms' mord. + + End disp_ff_functor_to_on_morphisms. + + Definition disp_ff_functor_to + {C : category} (D' : disp_cat C) + : UU + := ∑ (D : disp_ff_functor_to_on_objects D'), disp_ff_functor_to_on_morphisms D. + + (* Accessors for parts of a fully faithful functor that rely on morphisms *) + Section disp_ff_functor_accessors. + + Definition source_disp_cat_of_disp_ff_functor + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to D') + : disp_cat C. + Proof. + set (axioms_d := pr1 (pr2 (pr2 (pr2 D)))). + exact (((pr1 (pr1 D),, _),, _) ,, axioms_d). + Defined. + + Definition disp_functor_of_disp_ff_functor + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to D') + : disp_functor (functor_identity _) (source_disp_cat_of_disp_ff_functor D) D'. + Proof. + set (functor_axioms_d := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))). + exact ((pr2 (pr1 D) ,, _) ,, functor_axioms_d). + Defined. + + Coercion disp_functor_of_disp_ff_functor : disp_ff_functor_to >-> disp_functor. + + Definition disp_ff_functor_is_ff + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to D') + : disp_functor_ff (disp_functor_of_disp_ff_functor D) + := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))). + + End disp_ff_functor_accessors. End Auxiliary. From 5bd500c2e807449f137d5ebfaecf4c433ff33290 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 6 May 2020 22:54:23 +0300 Subject: [PATCH 07/18] Add proof that disp_ff_functor_on_morphisms_id is contractible --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 53 ++++++++++++++++++---- 1 file changed, 44 insertions(+), 9 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 7420b2cb..7672c7f2 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -62,15 +62,7 @@ Section Auxiliary. apply idpath. Defined. - Definition disp_ff_functor_to_on_objects - {C : category} - (D' : disp_cat C) - : UU - := ∑ (obd : C → UU) - , ∏ (Γ : C), obd Γ → D' Γ. - - Check weqtotaltoforall. - + (* TODO: move upstream? *) Lemma weqtotaltoforall3 {X : UU} (P1 : X → UU) (P2 : ∏ x : X, P1 x → UU) @@ -98,6 +90,15 @@ Section Auxiliary. apply weqtotal2asstor. Defined. + Definition disp_ff_functor_to_on_objects + {C : category} + (D' : disp_cat C) + : UU + := ∑ (obd : C → UU) + , ∏ (Γ : C), obd Γ → D' Γ. + + Check weqtotaltoforall. + Definition disp_ff_functor_on_morphisms_sop {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') @@ -191,6 +192,40 @@ Section Auxiliary. apply isapropifcontr, disp_ff_functor_on_morphisms_pos_iscontr. Defined. + Definition disp_ff_functor_on_morphisms_id_pos + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (mor_weq : disp_ff_functor_on_morphisms_pos D) + : UU + := ∏ (Γ : C) (A : pr1 D Γ), + ∑ (mor_id : pr1 (mor_weq Γ Γ A A (identity Γ))), + pr1 (pr2 (mor_weq Γ Γ A A (identity Γ))) mor_id + = transportb (mor_disp (pr2 D Γ A) (pr2 D Γ A)) + (functor_id (functor_identity C) Γ) (id_disp (pr2 D Γ A)). + + Definition disp_ff_functor_on_morphisms_id_pos_iscontr + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (mor_weq : disp_ff_functor_on_morphisms_pos D) + (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) + : iscontr (disp_ff_functor_on_morphisms_id_pos D mor_weq). + Proof. + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros A. + set (mord := pr1 (mor_weq Γ Γ A A (identity Γ))). + set (mord_weq := pr2 (mor_weq Γ Γ A A (identity Γ))). + use (@iscontrweqf (∑ mor_id : mord, mor_id = invweq mord_weq + (transportb (mor_disp (pr2 D Γ A) (pr2 D Γ A)) + (functor_id (functor_identity C) Γ) (id_disp (pr2 D Γ A))))). + - use (weqtotal2 (idweq _)). intros mor_id. simpl. + use weq_iso. + + intros p. apply (maponpaths mord_weq p @ homotweqinvweq mord_weq _). + + intros p. apply (! homotinvweqweq mord_weq _ @ maponpaths (invmap mord_weq) p). + + intros p. apply mor_isaset. + + intros p. apply (@homsets_disp _ D'). + - apply iscontrcoconustot. + Defined. + (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. From 27fd08a4d89e8d8caad7252222548b1c1f309935 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Wed, 6 May 2020 23:14:48 +0300 Subject: [PATCH 08/18] Add proof that disp_ff_functor_on_morphisms_comp is contractible --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 47 ++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 7672c7f2..890d55e9 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -226,6 +226,53 @@ Section Auxiliary. - apply iscontrcoconustot. Defined. + Definition disp_ff_functor_on_morphisms_comp_pos + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (mor_weq : disp_ff_functor_on_morphisms_pos D) + : UU + := ∏ (Γ Γ' Γ'' : C) + (A : pr1 D Γ) (A' : pr1 D Γ') (A'' : pr1 D Γ'') + (f : Γ --> Γ') (g : Γ' --> Γ'') + (ff : pr1 (mor_weq Γ Γ' A A' f)) + (gg : pr1 (mor_weq Γ' Γ'' A' A'' g)), + ∑ (mor_comp : pr1 (mor_weq Γ Γ'' A A'' (f ;; g))), + pr2 (mor_weq Γ Γ'' A A'' (f ;; g)) mor_comp + = transportb _ (functor_comp (functor_identity C) f g) + (comp_disp (pr2 (mor_weq _ _ _ _ _) ff) (pr2 (mor_weq _ _ _ _ _) gg)). + + Definition disp_ff_functor_on_morphisms_comp_pos_iscontr + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (mor_weq : disp_ff_functor_on_morphisms_pos D) + (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) + : iscontr (disp_ff_functor_on_morphisms_comp_pos D mor_weq). + Proof. + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros Γ''. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros A''. + apply impred_iscontr. intros f. + apply impred_iscontr. intros g. + apply impred_iscontr. intros ff. + apply impred_iscontr. intros gg. + set (mord := pr1 (mor_weq Γ Γ'' A A'' (f ;; g))). + set (mord_weq := pr2 (mor_weq Γ Γ'' A A'' (f ;; g))). + use (@iscontrweqf (∑ mor_comp : mord, + mor_comp + = invweq mord_weq (transportb _ (functor_comp (functor_identity C) f g) + (comp_disp (pr2 (mor_weq _ _ _ _ _) ff) (pr2 (mor_weq _ _ _ _ _) gg))))). + - use (weqtotal2 (idweq _)). intros mor_id. simpl. + use weq_iso. + + intros p. apply (maponpaths mord_weq p @ homotweqinvweq mord_weq _). + + intros p. apply (! homotinvweqweq mord_weq _ @ maponpaths (invmap mord_weq) p). + + intros p. apply mor_isaset. + + intros p. apply (@homsets_disp _ D'). + - apply iscontrcoconustot. + Defined. + (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. From f753eb0a7d0b8403dde142fac0619503074db851 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 00:07:00 +0300 Subject: [PATCH 09/18] Prove disp_ff_functor_on_morphisms_idcomp_pos_iscontr --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 69 ++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 890d55e9..de0563fc 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -90,6 +90,20 @@ Section Auxiliary. apply weqtotal2asstor. Defined. + (* TODO: move upstream? *) + Lemma iscontr_total2 + {X : UU} {P : X → UU} + : iscontr X → (∏ x : X, iscontr (P x)) → iscontr (∑ (x : X), P x). + Proof. + intros X_contr P_contr. + use tpair. + - exists (pr1 X_contr). apply P_contr. + - intros xp. + use total2_paths_f. + + apply X_contr. + + apply P_contr. + Defined. + Definition disp_ff_functor_to_on_objects {C : category} (D' : disp_cat C) @@ -273,6 +287,61 @@ Section Auxiliary. - apply iscontrcoconustot. Defined. + Definition disp_ff_functor_source_mor_isaset + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (mor_weq : disp_ff_functor_on_morphisms_pos D) + : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f)). + Proof. + intros Γ Γ' f A A'. + set (w := pr2 (mor_weq Γ Γ' A A' f)). + use (isofhlevelweqf 2 (invweq w)). + apply (@homsets_disp _ D'). + Defined. + + Definition disp_ff_functor_source_mor_isaset_iscontr + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + (mor_weq : disp_ff_functor_on_morphisms_pos D) + : iscontr (∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))). + Proof. + apply iscontraprop1. + - apply impred_isaprop. intros Γ. + apply impred_isaprop. intros Γ'. + apply impred_isaprop. intros A. + apply impred_isaprop. intros A'. + apply impred_isaprop. intros f. + apply isapropisaset. + - apply disp_ff_functor_source_mor_isaset. + Defined. + + Definition disp_ff_functor_on_morphisms_idcomp_pos + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : UU + := ∑ (mor_weq : disp_ff_functor_on_morphisms_pos D) + (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) + (mor_id : disp_ff_functor_on_morphisms_id_pos D mor_weq) + , disp_ff_functor_on_morphisms_comp_pos D mor_weq. + + Definition disp_ff_functor_on_morphisms_idcomp_pos_iscontr + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : iscontr (disp_ff_functor_on_morphisms_idcomp_pos D). + Proof. + apply iscontr_total2. + - apply disp_ff_functor_on_morphisms_pos_iscontr. + - intros mor_weq. apply iscontr_total2. + + apply disp_ff_functor_source_mor_isaset_iscontr. + + intros mor_isaset. + apply iscontr_total2. + * apply disp_ff_functor_on_morphisms_id_pos_iscontr. + apply mor_isaset. + * intros ?. + apply disp_ff_functor_on_morphisms_comp_pos_iscontr. + apply mor_isaset. + Defined. + (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. From da5227459ca3127a4cf545e7241f7e8bbf547244 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 01:35:54 +0300 Subject: [PATCH 10/18] Add disp_ff_functor_on_morphisms_idcomp_sop_pos_weq (direct equivalence proof) --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 71 +++++++++++++++++++--- 1 file changed, 64 insertions(+), 7 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index de0563fc..e85fad03 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -111,8 +111,6 @@ Section Auxiliary. := ∑ (obd : C → UU) , ∏ (Γ : C), obd Γ → D' Γ. - Check weqtotaltoforall. - Definition disp_ff_functor_on_morphisms_sop {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') @@ -342,6 +340,70 @@ Section Auxiliary. apply mor_isaset. Defined. + Definition disp_ff_functor_on_morphisms_idcomp_sop + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + := ∑ (mor_disp : ∏ {x y : C}, (x --> y) -> pr1 D x -> pr1 D y -> UU) + (id_disp' : ∏ {x : C} (xx : pr1 D x), mor_disp (identity x) xx xx) + (comp_disp' : ∏ {x y z : C} {f : x --> y} {g : y --> z} + {xx : pr1 D x} {yy : pr1 D y} {zz : pr1 D z}, + mor_disp f xx yy -> mor_disp g yy zz -> mor_disp (f ;; g) xx zz) + (homsets_disp : ∏ {x y} {f : x --> y} {xx} {yy}, isaset (mor_disp f xx yy)) + (Fmor : ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), + (mor_disp f xx yy) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) + (Fid : ∏ x (xx : pr1 D x), + Fmor _ _ _ _ _ (id_disp' xx) = transportb _ (functor_id (functor_identity C) x) (id_disp (pr2 D _ xx))) + (Fcomp : ∏ x y z (xx : pr1 D x) yy zz (f : x --> y) (g : y --> z) + (ff : mor_disp f xx yy) (gg : mor_disp g yy zz), + Fmor _ _ _ _ _ (comp_disp' ff gg) + = transportb _ (functor_comp (functor_identity _) f g) (comp_disp (Fmor _ _ _ _ _ ff) (Fmor _ _ _ _ _ gg))) + , ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), + isweq (fun ff : mor_disp f xx yy => Fmor _ _ _ _ _ ff). + + Definition disp_ff_functor_on_morphisms_idcomp_sop_pos_weq + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : disp_ff_functor_on_morphisms_idcomp_sop D ≃ disp_ff_functor_on_morphisms_idcomp_pos D. + Proof. + use weq_iso. + + - intros sop. + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + + exists (λ x y xx yy f, mor_disp x y f xx yy ,, Fmor x y xx yy f,, Fff x y xx yy f). + exists homsets_disp'. + exists (λ x xx, (id_disp' x xx ,, Fid x xx)). + exact (λ x y z xx yy zz f g ff gg, (comp_disp' x y z f g xx yy zz ff gg ,, Fcomp x y z xx yy zz f g ff gg)). + + - intros pos. + set (mor_disp := λ x y f xx yy, pr1 (pr1 pos x y xx yy f)). + set (Fmor := λ x y xx yy f, pr1 (pr2 (pr1 pos x y xx yy f))). + set (Fff := λ x y xx yy f, pr2 (pr2 (pr1 pos x y xx yy f))). + set (homsets_disp' := pr1 (pr2 pos)). + set (id_disp' := λ x xx, pr1 (pr1 (pr2 (pr2 pos)) x xx)). + set (Fid := λ x xx, pr2 (pr1 (pr2 (pr2 pos)) x xx)). + set (comp_disp' := λ x y z f g xx yy zz ff gg, pr1 (pr2 (pr2 (pr2 pos)) x y z xx yy zz f g ff gg)). + set (Fcomp := λ x y z xx yy zz f g ff gg, pr2 (pr2 (pr2 (pr2 pos)) x y z xx yy zz f g ff gg)). + + exists mor_disp. + exists id_disp'. + exists comp_disp'. + exists homsets_disp'. + exists Fmor. + exists Fid. + exists Fcomp. + exact Fff. + - intros ?. apply idpath. + - intros ?. apply idpath. + Defined. + (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. @@ -1024,11 +1086,6 @@ Section TypeCat_ComprehensionCat. {C : category} (CC : comprehension_cat_structure C) := disp_functor_ff (pr1 (pr2 (pr2 CC))). - Print disp_cat_ob_mor. - - Print cleaving. - Check cartesian_lift. - Definition typecat_obj_ext_structure_disp_ff_functor_to_codomain_weq (C : category) : typecat_obj_ext_structure C ≃ disp_ff_functor_to (disp_codomain C). From 5af5e1e5f4e2152444a3f4c6612d1efe062a6cd0 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 02:50:50 +0300 Subject: [PATCH 11/18] Add iscontr proofs for left and right identity axioms --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 151 +++++++++++++++++++-- 1 file changed, 142 insertions(+), 9 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index e85fad03..721639fc 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -343,22 +343,22 @@ Section Auxiliary. Definition disp_ff_functor_on_morphisms_idcomp_sop {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') - := ∑ (mor_disp : ∏ {x y : C}, (x --> y) -> pr1 D x -> pr1 D y -> UU) - (id_disp' : ∏ {x : C} (xx : pr1 D x), mor_disp (identity x) xx xx) + := ∑ (mor_disp : ∏ {x y : C}, pr1 D x -> pr1 D y -> (x --> y) -> UU) + (id_disp' : ∏ {x : C} (xx : pr1 D x), mor_disp xx xx (identity x)) (comp_disp' : ∏ {x y z : C} {f : x --> y} {g : y --> z} {xx : pr1 D x} {yy : pr1 D y} {zz : pr1 D z}, - mor_disp f xx yy -> mor_disp g yy zz -> mor_disp (f ;; g) xx zz) - (homsets_disp : ∏ {x y} {f : x --> y} {xx} {yy}, isaset (mor_disp f xx yy)) + mor_disp xx yy f -> mor_disp yy zz g -> mor_disp xx zz (f ;; g)) + (homsets_disp : ∏ {x y} {f : x --> y} {xx} {yy}, isaset (mor_disp xx yy f)) (Fmor : ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), - (mor_disp f xx yy) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) + (mor_disp xx yy f) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) (Fid : ∏ x (xx : pr1 D x), Fmor _ _ _ _ _ (id_disp' xx) = transportb _ (functor_id (functor_identity C) x) (id_disp (pr2 D _ xx))) (Fcomp : ∏ x y z (xx : pr1 D x) yy zz (f : x --> y) (g : y --> z) - (ff : mor_disp f xx yy) (gg : mor_disp g yy zz), + (ff : mor_disp xx yy f) (gg : mor_disp yy zz g), Fmor _ _ _ _ _ (comp_disp' ff gg) = transportb _ (functor_comp (functor_identity _) f g) (comp_disp (Fmor _ _ _ _ _ ff) (Fmor _ _ _ _ _ gg))) , ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), - isweq (fun ff : mor_disp f xx yy => Fmor _ _ _ _ _ ff). + isweq (fun ff : mor_disp xx yy f => Fmor _ _ _ _ _ ff). Definition disp_ff_functor_on_morphisms_idcomp_sop_pos_weq {C : category} {D' : disp_cat C} @@ -377,13 +377,13 @@ Section Auxiliary. set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - exists (λ x y xx yy f, mor_disp x y f xx yy ,, Fmor x y xx yy f,, Fff x y xx yy f). + exists (λ x y xx yy f, mor_disp x y xx yy f ,, Fmor x y xx yy f,, Fff x y xx yy f). exists homsets_disp'. exists (λ x xx, (id_disp' x xx ,, Fid x xx)). exact (λ x y z xx yy zz f g ff gg, (comp_disp' x y z f g xx yy zz ff gg ,, Fcomp x y z xx yy zz f g ff gg)). - intros pos. - set (mor_disp := λ x y f xx yy, pr1 (pr1 pos x y xx yy f)). + set (mor_disp := λ x y xx yy f, pr1 (pr1 pos x y xx yy f)). set (Fmor := λ x y xx yy f, pr1 (pr2 (pr1 pos x y xx yy f))). set (Fff := λ x y xx yy f, pr2 (pr2 (pr1 pos x y xx yy f))). set (homsets_disp' := pr1 (pr2 pos)). @@ -404,6 +404,139 @@ Section Auxiliary. - intros ?. apply idpath. Defined. + Definition source_disp_cat_data_of_disp_ff_functor_on_morphisms_idcomp_sop + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : disp_ff_functor_on_morphisms_idcomp_sop D → disp_cat_data C. + Proof. + intros sop. + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + + use tpair. + - exists (pr1 D). apply mor_disp. + - exact (id_disp' , comp_disp'). + Defined. + + Definition disp_ff_functor_sop + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : UU + := ∑ (mor_idcomp : disp_ff_functor_on_morphisms_idcomp_sop D), + disp_cat_axioms _ (source_disp_cat_data_of_disp_ff_functor_on_morphisms_idcomp_sop + D mor_idcomp). + + Lemma idpath_transportb + {X : UU} (P : X → UU) + (x : X) (p : P x) + : transportb P (idpath x) p = p. + Proof. + apply idpath. + Defined. + + Lemma homot_invweq_transportb_weq + (Z : UU) + (z z' : Z) + (X Y : Z → UU) + (e : z = z') + (w : ∏ z : Z, X z ≃ Y z) + (x : X z') + : invmap (w z) (transportb Y e (w z' x)) = transportb X e x. + Proof. + induction e. + etrans. apply maponpaths, idpath_transportb. + apply homotinvweqweq. + Defined. + + Definition disp_ff_functor_sop_iscontr + {C : category} {D' : disp_cat C} + (D : disp_ff_functor_to_on_objects D') + : iscontr (disp_ff_functor_sop D). + Proof. + apply iscontr_total2. + - apply (iscontrweqb (disp_ff_functor_on_morphisms_idcomp_sop_pos_weq _)). + apply disp_ff_functor_on_morphisms_idcomp_pos_iscontr. + - intros sop. + apply iscontr_total2. + + + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros f. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros ff. + apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (w := λ g, (Fmor _ _ A A' g,, Fff _ _ _ _ _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w _)). + etrans. apply maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths, maponpaths_2. apply Fid. + etrans. apply maponpaths, maponpaths. apply id_left_disp. + etrans. apply maponpaths. apply transport_b_b. simpl. + apply homot_invweq_transportb_weq. + + + intros ?. + apply iscontr_total2. + + * apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros f. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros ff. + apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (w := λ g, (Fmor _ _ A A' g,, Fff _ _ _ _ _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w _)). + etrans. apply maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths, maponpaths. apply Fid. + etrans. apply maponpaths, maponpaths. apply id_right_disp. + etrans. apply maponpaths. apply transport_b_b. simpl. + apply homot_invweq_transportb_weq. + + * intros ?. apply iscontr_total2. + + -- apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros Γ''. + apply impred_iscontr. intros Γ'''. + apply impred_iscontr. intros f. + apply impred_iscontr. intros g. + apply impred_iscontr. intros h. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros A''. + apply impred_iscontr. intros A'''. + apply impred_iscontr. intros ff. + apply impred_iscontr. intros gg. + apply impred_iscontr. intros hh. + apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (w := λ g, (Fmor _ _ A A''' g,, Fff _ _ _ _ _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w _)). + etrans. apply maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths, maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths. apply assoc_disp. + etrans. apply maponpaths. apply transport_b_b. simpl. + (* WORK IN PROGRESS *) + Abort. + (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. From 8182e528139a70c783df0aeb9a16c6cfe76e1b22 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 03:25:16 +0300 Subject: [PATCH 12/18] Complete proof for source displayed cat axioms (iscontr) --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 32 ++++++++++++++++++++-- 1 file changed, 29 insertions(+), 3 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 721639fc..0eac4ada 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -449,6 +449,19 @@ Section Auxiliary. apply homotinvweqweq. Defined. + Lemma homot_invweq_transportb + (Z : UU) + (z z' : Z) + (X Y : Z → UU) + (e : z = z') + (w : ∏ z : Z, X z ≃ Y z) + (y : Y z') + : invmap (w z) (transportb Y e y) = transportb X e (invmap (w z') y). + Proof. + induction e. + apply idpath. + Defined. + Definition disp_ff_functor_sop_iscontr {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') @@ -529,13 +542,26 @@ Section Auxiliary. set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). set (w := λ g, (Fmor _ _ A A''' g,, Fff _ _ _ _ _)). - etrans. apply pathsinv0. apply (homotinvweqweq (w _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w (f ;; (g ;; h)))). etrans. apply maponpaths. apply Fcomp. etrans. apply maponpaths, maponpaths, maponpaths. apply Fcomp. etrans. apply maponpaths, maponpaths. apply assoc_disp. - etrans. apply maponpaths. apply transport_b_b. simpl. + etrans. apply maponpaths. apply transport_b_b. (* WORK IN PROGRESS *) - Abort. + etrans. apply maponpaths, maponpaths, maponpaths_2, pathsinv0, Fcomp. + etrans. apply maponpaths, maponpaths, pathsinv0, Fcomp. + apply homot_invweq_transportb_weq. + -- intros ?. + set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). + apply iscontraprop1. + ++ apply impred_isaprop. intros Γ. + apply impred_isaprop. intros Γ'. + apply impred_isaprop. intros f. + apply impred_isaprop. intros A. + apply impred_isaprop. intros A'. + apply isapropisaset. + ++ apply homsets_disp'. + Defined. (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. From 98e3d4f93a4e9acbb64186150e0c5e3d042b9d32 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 03:53:21 +0300 Subject: [PATCH 13/18] Show that disp_ff_functor_sop is equivalent to usual definition of fully faithful displayed functor --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 133 +++++++++++++++------ 1 file changed, 95 insertions(+), 38 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 0eac4ada..9d080a7c 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -104,6 +104,30 @@ Section Auxiliary. + apply P_contr. Defined. + (* TODO: move upstream? *) + Lemma idpath_transportb + {X : UU} (P : X → UU) + (x : X) (p : P x) + : transportb P (idpath x) p = p. + Proof. + apply idpath. + Defined. + + (* TODO: move upstream? *) + Lemma homot_invweq_transportb_weq + (Z : UU) + (z z' : Z) + (X Y : Z → UU) + (e : z = z') + (w : ∏ z : Z, X z ≃ Y z) + (x : X z') + : invmap (w z) (transportb Y e (w z' x)) = transportb X e x. + Proof. + induction e. + etrans. apply maponpaths, idpath_transportb. + apply homotinvweqweq. + Defined. + Definition disp_ff_functor_to_on_objects {C : category} (D' : disp_cat C) @@ -419,7 +443,7 @@ Section Auxiliary. - exact (id_disp' , comp_disp'). Defined. - Definition disp_ff_functor_sop + Definition disp_ff_functor_mor_sop {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') : UU @@ -427,45 +451,10 @@ Section Auxiliary. disp_cat_axioms _ (source_disp_cat_data_of_disp_ff_functor_on_morphisms_idcomp_sop D mor_idcomp). - Lemma idpath_transportb - {X : UU} (P : X → UU) - (x : X) (p : P x) - : transportb P (idpath x) p = p. - Proof. - apply idpath. - Defined. - - Lemma homot_invweq_transportb_weq - (Z : UU) - (z z' : Z) - (X Y : Z → UU) - (e : z = z') - (w : ∏ z : Z, X z ≃ Y z) - (x : X z') - : invmap (w z) (transportb Y e (w z' x)) = transportb X e x. - Proof. - induction e. - etrans. apply maponpaths, idpath_transportb. - apply homotinvweqweq. - Defined. - - Lemma homot_invweq_transportb - (Z : UU) - (z z' : Z) - (X Y : Z → UU) - (e : z = z') - (w : ∏ z : Z, X z ≃ Y z) - (y : Y z') - : invmap (w z) (transportb Y e y) = transportb X e (invmap (w z') y). - Proof. - induction e. - apply idpath. - Defined. - - Definition disp_ff_functor_sop_iscontr + Definition disp_ff_functor_mor_sop_iscontr {C : category} {D' : disp_cat C} (D : disp_ff_functor_to_on_objects D') - : iscontr (disp_ff_functor_sop D). + : iscontr (disp_ff_functor_mor_sop D). Proof. apply iscontr_total2. - apply (iscontrweqb (disp_ff_functor_on_morphisms_idcomp_sop_pos_weq _)). @@ -563,6 +552,74 @@ Section Auxiliary. ++ apply homsets_disp'. Defined. + Definition disp_ff_functor_sop + {C : category} (D' : disp_cat C) + : UU + := ∑ (D : disp_ff_functor_to_on_objects D'), + disp_ff_functor_mor_sop D. + + Definition disp_ff_functor_sop_eq + {C : category} (D' : disp_cat C) + (X Y : disp_ff_functor_sop D') + (e : pr1 X = pr1 Y) + : X = Y. + Proof. + use total2_paths_f. + - apply e. + - apply isapropifcontr. + apply disp_ff_functor_mor_sop_iscontr. + Defined. + + Definition disp_ff_functor_sop_disp_functor_ff_weq + {C : category} {D' : disp_cat C} + : disp_ff_functor_sop D' ≃ + ∑ (D : disp_cat C) (F : disp_functor (functor_identity _) D D'), disp_functor_ff F. + Proof. + use weq_iso. + + - intros Fsop. + set (sop := pr1 (pr2 Fsop)). + + set (ob_disp := pr1 (pr1 Fsop)). + set (Fob := pr2 (pr1 Fsop)). + set (axioms_d := pr2 (pr2 Fsop)). + + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + + exists (((ob_disp ,, mor_disp) ,, (id_disp' , comp_disp')) ,, axioms_d). + exists ((Fob,,Fmor),,(Fid,Fcomp)). + exact Fff. + + - intros F. + + set (ob_disp := pr1 (pr1 (pr1 (pr1 F)))). + set (mor_disp := pr2 (pr1 (pr1 (pr1 F)))). + set (id_disp' := pr1 (pr2 (pr1 (pr1 F)))). + set (comp_disp' := pr2 (pr2 (pr1 (pr1 F)))). + set (axioms_d := pr2 (pr1 F)). + set (homsets_disp' := pr2 (pr2 (pr2 axioms_d))). + + set (Fob := pr1 (pr1 (pr1 (pr2 F)))). + set (Fmor := pr2 (pr1 (pr1 (pr2 F)))). + set (Fid := pr1 (pr2 (pr1 (pr2 F)))). + set (Fcomp := pr2 (pr2 (pr1 (pr2 F)))). + set (Fff := pr2 (pr2 F)). + + exists (ob_disp ,, Fob). + exists (mor_disp ,, id_disp' ,, comp_disp' ,, homsets_disp' ,, Fmor ,, Fid ,, Fcomp ,, Fff). + exact axioms_d. + + - intros ?. apply disp_ff_functor_sop_eq. apply idpath. + - intros ?. apply idpath. + Defined. + (* Types for parts of a fully faithful functor that rely on morphisms *) Section disp_ff_functor_to_on_morphisms. From 9050d1da261ecdf00e2607c12e860ede3292721f Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 04:25:51 +0300 Subject: [PATCH 14/18] Add accessors and coercion for disp_ff_functor_sop: --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 186 ++++++++------------- 1 file changed, 70 insertions(+), 116 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 9d080a7c..790c2052 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -558,6 +558,50 @@ Section Auxiliary. := ∑ (D : disp_ff_functor_to_on_objects D'), disp_ff_functor_mor_sop D. + Definition source_disp_cat_of_disp_ff_functor_sop + {C : category} {D' : disp_cat C} + (Fsop : disp_ff_functor_sop D') + : disp_cat C. + Proof. + set (sop := pr1 (pr2 Fsop)). + + set (ob_disp := pr1 (pr1 Fsop)). + set (axioms_d := pr2 (pr2 Fsop)). + + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + + exact (((ob_disp ,, mor_disp) ,, (id_disp' , comp_disp')) ,, axioms_d). + Defined. + + Definition disp_functor_of_disp_ff_functor_sop + {C : category} {D' : disp_cat C} + (Fsop : disp_ff_functor_sop D') + : disp_functor (functor_identity C) (source_disp_cat_of_disp_ff_functor_sop Fsop) D'. + Proof. + set (sop := pr1 (pr2 Fsop)). + + set (Fob := pr2 (pr1 Fsop)). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + + exact ((Fob,,Fmor),,(Fid,Fcomp)). + Defined. + + Coercion disp_functor_of_disp_ff_functor_sop : disp_ff_functor_sop >-> disp_functor. + + Definition disp_functor_of_disp_ff_functor_sop_is_ff + {C : category} {D' : disp_cat C} + (Fsop : disp_ff_functor_sop D') + : disp_functor_ff (disp_functor_of_disp_ff_functor_sop Fsop). + Proof. + set (sop := pr1 (pr2 Fsop)). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + exact Fff. + Defined. + Definition disp_ff_functor_sop_eq {C : category} (D' : disp_cat C) (X Y : disp_ff_functor_sop D') @@ -578,24 +622,9 @@ Section Auxiliary. use weq_iso. - intros Fsop. - set (sop := pr1 (pr2 Fsop)). - - set (ob_disp := pr1 (pr1 Fsop)). - set (Fob := pr2 (pr1 Fsop)). - set (axioms_d := pr2 (pr2 Fsop)). - - set (mor_disp := pr1 sop). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). - set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). - set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). - set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - - exists (((ob_disp ,, mor_disp) ,, (id_disp' , comp_disp')) ,, axioms_d). - exists ((Fob,,Fmor),,(Fid,Fcomp)). - exact Fff. + exists (source_disp_cat_of_disp_ff_functor_sop Fsop). + exists (disp_functor_of_disp_ff_functor_sop Fsop). + apply disp_functor_of_disp_ff_functor_sop_is_ff. - intros F. @@ -620,100 +649,14 @@ Section Auxiliary. - intros ?. apply idpath. Defined. - (* Types for parts of a fully faithful functor that rely on morphisms *) - Section disp_ff_functor_to_on_morphisms. - - Context {C : category} {D' : disp_cat C}. - Context (D : disp_ff_functor_to_on_objects D'). - - Definition disp_ff_functor_source_mor : UU - := ∏ (Γ Γ' : C), (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU. - - Definition disp_ff_functor_source_id_comp - (mord : disp_ff_functor_source_mor) : UU - := disp_cat_id_comp C (pr1 D,, mord). - - Definition disp_ff_functor_source_axioms - (mord : disp_ff_functor_source_mor) - (id_comp_d : disp_ff_functor_source_id_comp mord) - : UU - := disp_cat_axioms C ((pr1 D ,, mord) ,, id_comp_d). - - Definition disp_ff_functor_on_morphisms - (mord : disp_ff_functor_source_mor) - : UU - := ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y) - , (mord _ _ xx yy f) -> (pr2 D _ xx -->[ f ] pr2 D _ yy). - - Definition disp_ff_functor_axioms - (mord : disp_ff_functor_source_mor) - (id_comp_d : disp_ff_functor_source_id_comp mord) - (axioms_d : disp_ff_functor_source_axioms mord id_comp_d) - (functor_mord : disp_ff_functor_on_morphisms mord) - : UU - := @disp_functor_axioms - C C (functor_identity _) - (((pr1 D ,, mord) ,, id_comp_d) ,, axioms_d) D' - (pr2 D ,, functor_mord). - - Definition disp_ff_functor_ff - (mord : disp_ff_functor_source_mor) - (functor_mord : disp_ff_functor_on_morphisms mord) - : UU - := ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , isweq (functor_mord Γ Γ' A A' f). - - Definition disp_ff_functor_to_on_morphisms' - (mord : disp_ff_functor_source_mor) - : UU - := ∑ (id_comp_d : disp_ff_functor_source_id_comp mord) - (axioms_d : disp_ff_functor_source_axioms mord id_comp_d) - (functor_mord : disp_ff_functor_on_morphisms mord) - (functor_axioms_d : disp_ff_functor_axioms mord id_comp_d axioms_d functor_mord) - , disp_ff_functor_ff mord functor_mord. - - Definition disp_ff_functor_to_on_morphisms - : UU - := ∑ (mord : disp_ff_functor_source_mor) - , disp_ff_functor_to_on_morphisms' mord. - - End disp_ff_functor_to_on_morphisms. - - Definition disp_ff_functor_to - {C : category} (D' : disp_cat C) - : UU - := ∑ (D : disp_ff_functor_to_on_objects D'), disp_ff_functor_to_on_morphisms D. - - (* Accessors for parts of a fully faithful functor that rely on morphisms *) - Section disp_ff_functor_accessors. - - Definition source_disp_cat_of_disp_ff_functor - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to D') - : disp_cat C. - Proof. - set (axioms_d := pr1 (pr2 (pr2 (pr2 D)))). - exact (((pr1 (pr1 D),, _),, _) ,, axioms_d). - Defined. - - Definition disp_functor_of_disp_ff_functor - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to D') - : disp_functor (functor_identity _) (source_disp_cat_of_disp_ff_functor D) D'. - Proof. - set (functor_axioms_d := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 D)))))). - exact ((pr2 (pr1 D) ,, _) ,, functor_axioms_d). - Defined. - - Coercion disp_functor_of_disp_ff_functor : disp_ff_functor_to >-> disp_functor. - - Definition disp_ff_functor_is_ff - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to D') - : disp_functor_ff (disp_functor_of_disp_ff_functor D) - := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 D))))). - - End disp_ff_functor_accessors. + Definition disp_ff_functor_sop_disp_ff_functor_to_on_objects_weq + {C : category} {D' : disp_cat C} + : disp_ff_functor_to_on_objects D' ≃ disp_ff_functor_sop D'. + Proof. + apply invweq, weqpr1. + intros D. + apply disp_ff_functor_mor_sop_iscontr. + Defined. End Auxiliary. @@ -1304,14 +1247,25 @@ Section TypeCat_ComprehensionCat. Definition typecat_obj_ext_structure_disp_ff_functor_to_codomain_weq (C : category) - : typecat_obj_ext_structure C ≃ disp_ff_functor_to (disp_codomain C). + : typecat_obj_ext_structure C ≃ disp_ff_functor_to_on_objects (disp_codomain C). Proof. - (* TODO *) + use weq_iso. + - intros tc. + exists (pr1 (pr1 tc)). + intros Γ A. + exists (Γ ◂ A). + apply (pr2 tc). + - intros F. + use tpair. + + exists (pr1 F). + use tpair. + * intros Γ A. + exact (pr1 (pr2 F Γ A)). Abort. Definition ff_comprehension_cat_structure (C : category) : UU - := ∑ (F : disp_ff_functor_to (disp_codomain C)), - cleaving (source_disp_cat_of_disp_ff_functor F) + := ∑ (F : disp_ff_functor_sop (disp_codomain C)), + cleaving (source_disp_cat_of_disp_ff_functor_sop F) × is_cartesian_disp_functor F. Definition typecat_ff_comprehension_cat_structure_weq (C : category) From dee0d33b1b8d7de51f50622dd6d478a91d57afb4 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 04:50:06 +0300 Subject: [PATCH 15/18] Show that typecat_obj_ext_structure is equivalent to disp_ff_functor_on_objects --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 81 +++++++++++++--------- 1 file changed, 48 insertions(+), 33 deletions(-) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 790c2052..ad194fe0 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -1,4 +1,4 @@ -(** +(* [TypeTheory.ALV2.TypeCat_ComprehensionCat] Part of the [TypeTheory] library (Ahrens, Lumsdaine, Voevodsky, 2015–present). @@ -670,21 +670,28 @@ Section TypeCat_ObjExt. * - projection morphism [dpr_typecat_obj_ext]: Γ ◂ A --> Γ. *) Definition typecat_obj_ext_structure (C : precategory) - := ∑ TC : typecat_structure1 C, - ∏ Γ (A : TC Γ), Γ ◂ A --> Γ. + := ∑ (Ty : C → UU) + (ext : ∏ (Γ : C), Ty Γ → C) + (* dpr : *), ∏ Γ (A : Ty Γ), ext Γ A --> Γ. + + Definition Ty_obj_ext (C : precategory) + (TC : typecat_obj_ext_structure C) + : C → UU + := pr1 TC. + + Coercion Ty_obj_ext : typecat_obj_ext_structure >-> Funclass. - Definition typecat1_from_typecat_obj_ext (C : precategory) - (TC : typecat_obj_ext_structure C) - : typecat_structure1 _ := pr1 TC. - Coercion typecat1_from_typecat_obj_ext : typecat_obj_ext_structure >-> typecat_structure1. + Definition obj_ext_typecat {C : precategory} {TC : typecat_obj_ext_structure C} + (Γ : C) (A : TC Γ) : C + := pr1 (pr2 TC) Γ A. Definition dpr_typecat_obj_ext {C : precategory} - {TC : typecat_obj_ext_structure C} {Γ} (A : TC Γ) - : (Γ ◂ A) --> Γ - := pr2 TC Γ A. + {TC : typecat_obj_ext_structure C} {Γ} (A : pr1 TC Γ) + : obj_ext_typecat Γ A --> Γ + := pr2 (pr2 TC) Γ A. Definition typecat_obj_ext_from_typecat (C : precategory) (TC : typecat_structure C) - : typecat_obj_ext_structure _ := (pr1 TC ,, @dpr_typecat _ TC). + : typecat_obj_ext_structure _ := (_ ,, _ ,, @dpr_typecat _ TC). Coercion typecat_obj_ext_from_typecat : typecat_structure >-> typecat_obj_ext_structure. End TypeCat_ObjExt. @@ -698,7 +705,7 @@ Section TypeCat_Comp_Ext_Compare. Definition typecat_comp_ext_compare {Γ : C} {A B : TC Γ} - : (A = B) → Γ ◂ A --> Γ ◂ B. + : (A = B) → obj_ext_typecat Γ A --> obj_ext_typecat Γ B. Proof. intros p. induction p. apply identity. @@ -707,14 +714,14 @@ Section TypeCat_Comp_Ext_Compare. Definition typecat_idtoiso_dpr {Γ : C} {A B : TC Γ} (p : A = B) - : idtoiso (maponpaths (λ B, Γ ◂ B) p) ;; π B = π A. + : idtoiso (maponpaths (λ B, obj_ext_typecat Γ B) p) ;; π B = π A. Proof. induction p. apply id_left. Defined. Definition typecat_iso_triangle {Γ : C} (A B : TC Γ) - := ∑ (i : iso (Γ ◂ A) (Γ ◂ B)), + := ∑ (i : iso (obj_ext_typecat Γ A) (obj_ext_typecat Γ B)), i ;; π B = π A. Definition typecat_iso_triangle_swap @@ -756,7 +763,7 @@ Section TypeCat_Disp. use tpair. - apply TC. - intros Γ' Γ A' A f. - exact (∑ ff : Γ' ◂ A' --> Γ ◂ A, + exact (∑ ff : obj_ext_typecat Γ' A' --> obj_ext_typecat Γ A, ff ;; π A = π A' ;; f). Defined. @@ -833,11 +840,11 @@ Section TypeCat_Disp. : typecat_iso_triangle _ A B → @iso_disp C (typecat_disp TC) _ _ (identity_iso Γ) A B. Proof. intros tr. - set (i := pr1 (pr1 tr) : C ⟦ Γ ◂ A, Γ ◂ B ⟧ ). + set (i := pr1 (pr1 tr) : C ⟦ obj_ext_typecat Γ A, obj_ext_typecat Γ B ⟧ ). set (iB_A := pr2 tr : i ;; π B = π A). set (tr' := typecat_iso_triangle_swap TC tr). - set (inv_i := pr1 (pr1 tr') : C ⟦ Γ ◂ B, Γ ◂ A ⟧). + set (inv_i := pr1 (pr1 tr') : C ⟦ obj_ext_typecat Γ B, obj_ext_typecat Γ A ⟧). set (inv_iA_B := pr2 tr' : inv_i ;; π A = π B). set (i_inv_i := iso_inv_after_iso (pr1 tr) : i ;; inv_i = identity _). @@ -852,13 +859,13 @@ Section TypeCat_Disp. 2: apply homset_property. etrans. apply inv_i_i. apply pathsinv0. - etrans. apply (pr1_transportb (λ _ (_ : C ⟦ Γ ◂ B, Γ ◂ B ⟧), _)). + etrans. apply (pr1_transportb (λ _ (_ : C ⟦ obj_ext_typecat Γ B, obj_ext_typecat Γ B ⟧), _)). apply (maponpaths (λ f, f _) (transportb_const _ _)). - use total2_paths_f. 2: apply homset_property. etrans. apply i_inv_i. apply pathsinv0. - etrans. apply (pr1_transportb (λ _ (_ : C ⟦ Γ ◂ A, Γ ◂ A ⟧), _)). + etrans. apply (pr1_transportb (λ _ (_ : C ⟦ obj_ext_typecat Γ A, obj_ext_typecat Γ A ⟧), _)). apply (maponpaths (λ f, f _) (transportb_const _ _)). Defined. @@ -867,9 +874,9 @@ Section TypeCat_Disp. : @iso_disp C (typecat_disp TC) _ _ (identity_iso Γ) A B → typecat_iso_triangle _ A B. Proof. intros tr. - set (i := pr1 (pr1 tr) : C ⟦ Γ ◂ A, Γ ◂ B ⟧ ). + set (i := pr1 (pr1 tr) : C ⟦ obj_ext_typecat Γ A, obj_ext_typecat Γ B ⟧ ). set (iB_A := pr2 (pr1 tr) : i ;; π B = π A ;; identity _). - set (inv_i := pr1 (pr1 (pr2 tr)) : C ⟦ Γ ◂ B, Γ ◂ A ⟧). + set (inv_i := pr1 (pr1 (pr2 tr)) : C ⟦ obj_ext_typecat Γ B, obj_ext_typecat Γ A ⟧). set (inv_iA_B := pr2 (pr1 (pr2 tr)) : inv_i ;; π A = π B ;; identity _). set (inv_i_i := maponpaths pr1 (pr1 (pr2 (pr2 tr))) : _). @@ -882,11 +889,11 @@ Section TypeCat_Disp. + apply inv_i. + etrans. apply i_inv_i. etrans. - use (pr1_transportb (λ _ (_ : C ⟦ Γ ◂ A, Γ ◂ A ⟧), _)). + use (pr1_transportb (λ _ (_ : C ⟦ obj_ext_typecat Γ A, obj_ext_typecat Γ A ⟧), _)). simpl. apply (maponpaths (λ f, f _) (transportb_const _ _)). + etrans. apply inv_i_i. etrans. - use (pr1_transportb (λ _ (_ : C ⟦ Γ ◂ B, Γ ◂ B ⟧), _)). + use (pr1_transportb (λ _ (_ : C ⟦ obj_ext_typecat Γ B, obj_ext_typecat Γ B ⟧), _)). simpl. apply (maponpaths (λ f, f _) (transportb_const _ _)). - etrans. apply iB_A. apply id_right. Defined. @@ -998,7 +1005,7 @@ Section TypeCat_Disp_Functor. (typecat_disp TC) (disp_codomain C). Proof. use tpair. - - intros Γ A. exists (Γ ◂ A). apply dpr_typecat_obj_ext. + - intros Γ A. exists (obj_ext_typecat Γ A). apply dpr_typecat_obj_ext. - intros Γ' Γ A' A f ff. apply ff. Defined. @@ -1127,8 +1134,13 @@ Section ComprehensionCat_TypeCat. := pr2 (comprehension_functor Γ A). Definition typecat_obj_ext_structure_from_comprehension_cat - : typecat_obj_ext_structure C - := (typecat1_from_comprehension_cat ,, dpr_from_comprehension_cat). + : typecat_obj_ext_structure C. + Proof. + repeat use tpair. + - exact ty_from_comprehension_cat. + - exact ext_from_comprehension_cat. + - exact dpr_from_comprehension_cat. + Defined. Definition q_square_from_comprehension_cat (Γ : C) (A : ty_from_comprehension_cat Γ) @@ -1251,17 +1263,20 @@ Section TypeCat_ComprehensionCat. Proof. use weq_iso. - intros tc. - exists (pr1 (pr1 tc)). + exists (pr1 tc). intros Γ A. - exists (Γ ◂ A). + exists (obj_ext_typecat Γ A). apply (pr2 tc). - intros F. + exists (pr1 F). use tpair. - + exists (pr1 F). - use tpair. - * intros Γ A. - exact (pr1 (pr2 F Γ A)). - Abort. + + intros Γ A. + exact (pr1 (pr2 F Γ A)). + + intros Γ A. + exact (pr2 (pr2 F Γ A)). + - intros ?. apply idpath. + - intros ?. apply idpath. + Defined. Definition ff_comprehension_cat_structure (C : category) : UU := ∑ (F : disp_ff_functor_sop (disp_codomain C)), From 02c2ab3817b837b63b040a579ecf948f2d65ca2f Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 04:54:53 +0300 Subject: [PATCH 16/18] Show that typecat_obj_ext_structure is equivalent to usual definition of fully faithful displayed functor to codomain --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index ad194fe0..34b491f5 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -1278,6 +1278,18 @@ Section TypeCat_ComprehensionCat. - intros ?. apply idpath. Defined. + Definition typecat_obj_ext_structure_ff_disp_functor_to_codomain_weq + (C : category) + : typecat_obj_ext_structure C ≃ + ∑ (D : disp_cat C) + (F : disp_functor (functor_identity _) D (disp_codomain C)) + , disp_functor_ff F. + Proof. + eapply weqcomp. apply typecat_obj_ext_structure_disp_ff_functor_to_codomain_weq. + eapply weqcomp. apply disp_ff_functor_sop_disp_ff_functor_to_on_objects_weq. + apply disp_ff_functor_sop_disp_functor_ff_weq. + Defined. + Definition ff_comprehension_cat_structure (C : category) : UU := ∑ (F : disp_ff_functor_sop (disp_codomain C)), cleaving (source_disp_cat_of_disp_ff_functor_sop F) From e1e3a2ea3315f830561e0eb2ec2c536fc5dd011a Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 12:49:36 +0300 Subject: [PATCH 17/18] Add typecat_structure' that is equivalent to typecat_structure --- TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 33 ++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 34b491f5..6d34688f 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -1290,6 +1290,39 @@ Section TypeCat_ComprehensionCat. apply disp_ff_functor_sop_disp_functor_ff_weq. Defined. + Definition typecat_structure' (C : category) : UU + := ∑ (TC : typecat_obj_ext_structure C) + (reind : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), TC Γ') + (q : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), (obj_ext_typecat Γ' (reind _ A _ f)) --> obj_ext_typecat Γ A ) + (dpr_q : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), + (q _ A _ f) ;; (dpr_typecat_obj_ext A) = (dpr_typecat_obj_ext (reind _ A _ f)) ;; f), + ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), + isPullback _ _ _ _ (!dpr_q _ A _ f). + + Definition typecat_structure_typecat_structure'_weq + (C : category) + : typecat_structure C ≃ typecat_structure' C. + Proof. + eapply weqcomp. apply weqtotal2asstor. + apply invweq. + eapply weqcomp. apply weqtotal2asstor. + apply (weqtotal2 (idweq _)). intros Ty. + + eapply weqcomp. apply weqtotal2asstor. + apply invweq. eapply weqcomp. apply weqtotal2asstor. + apply (weqtotal2 (idweq _)). intros ext. + + eapply weqcomp. unfold typecat_structure2. simpl. + apply (@WeakEquivalences.weqtotal2comm + _ _ + (λ reind dpr, + ∑ (q : ∏ Γ (A : Ty Γ) Γ' (f : Γ' --> Γ), (ext Γ' (reind _ A _ f)) --> ext Γ A ) + (dpr_q : ∏ Γ (A : Ty Γ) Γ' (f : Γ' --> Γ), + (q _ A _ f) ;; (dpr _ A) = (dpr _ (reind _ A _ f)) ;; f), + _)). + apply idweq. + Defined. + Definition ff_comprehension_cat_structure (C : category) : UU := ∑ (F : disp_ff_functor_sop (disp_codomain C)), cleaving (source_disp_cat_of_disp_ff_functor_sop F) From 268192a438e13299f2becce111c7aff7f11958c3 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Thu, 7 May 2020 18:57:45 +0300 Subject: [PATCH 18/18] Factor out FullyFaithfulDispFunctor module --- TypeTheory/ALV2/.package/files | 1 + TypeTheory/ALV2/FullyFaithfulDispFunctor.v | 662 +++++++++++++++++++++ TypeTheory/ALV2/TypeCat_ComprehensionCat.v | 643 ++------------------ 3 files changed, 697 insertions(+), 609 deletions(-) create mode 100644 TypeTheory/ALV2/FullyFaithfulDispFunctor.v diff --git a/TypeTheory/ALV2/.package/files b/TypeTheory/ALV2/.package/files index 046cf238..11a61f5c 100644 --- a/TypeTheory/ALV2/.package/files +++ b/TypeTheory/ALV2/.package/files @@ -12,3 +12,4 @@ RelUniv_Cat_Iso.v RelUniv_Cat_Yo_CwF_Iso.v RelUnivTransfer.v TypeCat_ComprehensionCat.v +FullyFaithfulDispFunctor.v diff --git a/TypeTheory/ALV2/FullyFaithfulDispFunctor.v b/TypeTheory/ALV2/FullyFaithfulDispFunctor.v new file mode 100644 index 00000000..938ecb45 --- /dev/null +++ b/TypeTheory/ALV2/FullyFaithfulDispFunctor.v @@ -0,0 +1,662 @@ +(* + [TypeTheory.ALV2.FullyFaithfulDispFunctor] + + Part of the [TypeTheory] library (Ahrens, Lumsdaine, Voevodsky, 2015–present). +*) + +(** + +Fully faithful displayed functors over identity functor on C +with fixed target displayed categories are completely determined +my their action on objects. + +Specifically we have an equivalence [ff_disp_functor_weq] between +[ff_disp_functor] (an alias for [ff_disp_functor_on_objects]) +and [ff_disp_functor_explicit] (which is a combination of +a source displayed category over C and a fully faithful functor +over identity functor on C from said category into D'). + +Main definitions: + +- [ff_disp_functor] (same as [ff_disp_functor_on_objects]) — + definition of fully faithful functor without (contractible) morphisms; +- [ff_disp_functor_explicit] — combination of a source displayed category + over C and a fully faithful displayed functor (over identity functor on C) + into D'; +- [ff_disp_functor_weq] — equivalence of the two definitions; + +Accessors for [ff_disp_functor]: + +- [source_disp_cat_from_ff_disp_functor] — source displayed category; +- [disp_functor_from_ff_disp_functor] — displayed functor (also acts as coercion); +- [disp_functor_from_ff_disp_functor_is_ff] — proof that extracted functor is fully faithful; + +*) + +Require Import UniMath.MoreFoundations.PartA. +Require Import TypeTheory.Auxiliary.CategoryTheoryImports. + +Require Import TypeTheory.Auxiliary.Auxiliary. +Require Import UniMath.CategoryTheory.DisplayedCats.Core. + +Section Auxiliary. + + (* TODO: move upstream? *) + Lemma weqtotaltoforall3 {X : UU} + (P1 : X → UU) + (P2 : ∏ x : X, P1 x → UU) + (P3 : ∏ (x : X) (y : P1 x), P2 x y → UU) + : (∑ (p1 : ∏ x : X, P1 x) (p2 : ∏ x : X, P2 x (p1 x)), ∏ x : X, P3 x (p1 x) (p2 x)) + ≃ (∏ x : X, ∑ (p1 : P1 x) (p2 : P2 x p1), P3 x p1 p2). + Proof. + eapply weqcomp. + apply (weqtotal2asstol + (λ p1, ∏ x : X, P2 x (p1 x)) + (λ p12, ∏ x : X, P3 x (pr1 p12 x) (pr2 p12 x)) + ). + eapply weqcomp. + use weqtotal2. 3: apply weqtotaltoforall. + - exact (λ p12, ∏ x : X, P3 x (pr1 (p12 x)) (pr2 (p12 x))). + - intros x. apply idweq. + + - eapply weqcomp. + apply (weqtotaltoforall + (λ x : X, ∑ y : P1 x, P2 x y) + (λ (x : X) p12, P3 x (pr1 p12) (pr2 p12)) + ). + apply weqonsecfibers. + intros x. + apply weqtotal2asstor. + Defined. + + (* TODO: move upstream? *) + Lemma iscontr_total2 + {X : UU} {P : X → UU} + : iscontr X → (∏ x : X, iscontr (P x)) → iscontr (∑ (x : X), P x). + Proof. + intros X_contr P_contr. + use tpair. + - exists (pr1 X_contr). apply P_contr. + - intros xp. + use total2_paths_f. + + apply X_contr. + + apply P_contr. + Defined. + + (* TODO: move upstream? *) + Lemma idpath_transportb + {X : UU} (P : X → UU) + (x : X) (p : P x) + : transportb P (idpath x) p = p. + Proof. + apply idpath. + Defined. + + (* TODO: move upstream? *) + Lemma homot_invweq_transportb_weq + (Z : UU) + (z z' : Z) + (X Y : Z → UU) + (e : z = z') + (w : ∏ z : Z, X z ≃ Y z) + (x : X z') + : invmap (w z) (transportb Y e (w z' x)) = transportb X e x. + Proof. + induction e. + etrans. apply maponpaths, idpath_transportb. + apply homotinvweqweq. + Defined. + +End Auxiliary. + +Section FullyFaithfulDispFunctor. + + (* Fully faithful displayed functor (over identity functor on C) into D' + * is completely determined by its action on objects: + * + * - type family of displayed objects (for the source displayed category) over objects in C + * - mapping of said displayed objects to displayed objects in D' over C. + * *) + Definition ff_disp_functor_on_objects {C : category} + (D' : disp_cat C) + : UU + := ∑ (ob_disp : C → UU) + (* Fob *), ∏ (Γ : C), ob_disp Γ → D' Γ. + + Section FullyFaithfulFunctorOnMorphisms. + + Context {C : category} {D' : disp_cat C}. + Context (D : ff_disp_functor_on_objects D'). + + Definition ff_disp_functor_on_morphisms_sop : UU + := ∑ (mord : ∏ Γ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (functor_mord : ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord _ _ A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + , ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord Γ Γ' A A' f). + + Definition ff_disp_functor_on_morphisms_pos : UU + := ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ'), + ∑ (mord : UU), mord ≃ (pr2 D _ A -->[ f ] pr2 D _ A'). + + Definition ff_disp_functor_on_morphisms_sop_pos_weq + : ff_disp_functor_on_morphisms_sop ≃ ff_disp_functor_on_morphisms_pos. + Proof. + eapply weqcomp. + apply (weqtotaltoforall3 + (λ Γ, ∏ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (λ Γ mord, ∏ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord _ A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ Γ mord functor_mord, + ∏ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord Γ' A A' f))). + apply weqonsecfibers. intros Γ. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) + (λ Γ' mord, ∏ (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ Γ' mord functor_mord, + ∏ (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord A A' f))). + apply weqonsecfibers. intros Γ'. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ A, (pr1 D Γ') → (Γ --> Γ') → UU) + (λ A mord, ∏ (A' : pr1 D Γ') (f : Γ --> Γ') + , (mord A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ A mord functor_mord, + ∏ (A' : pr1 D Γ') (f : Γ --> Γ') + , isweq (functor_mord A' f))). + apply weqonsecfibers. intros A. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ A', (Γ --> Γ') → UU) + (λ A' mord, ∏ (f : Γ --> Γ') + , (mord f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ A' mord functor_mord, + ∏ (f : Γ --> Γ') + , isweq (functor_mord f))). + apply weqonsecfibers. intros A'. + + eapply weqcomp. + apply (weqtotaltoforall3 + (λ f, UU) + (λ f mord, mord -> (pr2 D _ A -->[ f ] pr2 D _ A')) + (λ f mord functor_mord, isweq functor_mord)). + apply idweq. + Defined. + + Definition ff_disp_functor_on_morphisms_pos_iscontr + : iscontr ff_disp_functor_on_morphisms_pos. + Proof. + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros f. + use (@iscontrweqf (∑ mord : UU, mord = pr2 D Γ A -->[f] pr2 D Γ' A')). + - use (weqtotal2 (idweq _)). intros mord. apply univalenceweq. + - apply iscontrcoconustot. + Defined. + + Definition ff_disp_functor_on_morphisms_pos_isaprop + : isaprop ff_disp_functor_on_morphisms_pos. + Proof. + apply isapropifcontr, ff_disp_functor_on_morphisms_pos_iscontr. + Defined. + + Definition ff_disp_functor_on_morphisms_id_pos + (mor_weq : ff_disp_functor_on_morphisms_pos) + : UU + := ∏ (Γ : C) (A : pr1 D Γ), + ∑ (mor_id : pr1 (mor_weq Γ Γ A A (identity Γ))), + pr1 (pr2 (mor_weq Γ Γ A A (identity Γ))) mor_id + = transportb (mor_disp (pr2 D Γ A) (pr2 D Γ A)) + (functor_id (functor_identity C) Γ) (id_disp (pr2 D Γ A)). + + Definition ff_disp_functor_on_morphisms_id_pos_iscontr + (mor_weq : ff_disp_functor_on_morphisms_pos) + (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) + : iscontr (ff_disp_functor_on_morphisms_id_pos mor_weq). + Proof. + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros A. + set (mord := pr1 (mor_weq Γ Γ A A (identity Γ))). + set (mord_weq := pr2 (mor_weq Γ Γ A A (identity Γ))). + use (@iscontrweqf (∑ mor_id : mord, mor_id = invweq mord_weq + (transportb (mor_disp (pr2 D Γ A) (pr2 D Γ A)) + (functor_id (functor_identity C) Γ) (id_disp (pr2 D Γ A))))). + - use (weqtotal2 (idweq _)). intros mor_id. simpl. + use weq_iso. + + intros p. apply (maponpaths mord_weq p @ homotweqinvweq mord_weq _). + + intros p. apply (! homotinvweqweq mord_weq _ @ maponpaths (invmap mord_weq) p). + + intros p. apply mor_isaset. + + intros p. apply (@homsets_disp _ D'). + - apply iscontrcoconustot. + Defined. + + Definition ff_disp_functor_on_morphisms_comp_pos + (mor_weq : ff_disp_functor_on_morphisms_pos) + : UU + := ∏ (Γ Γ' Γ'' : C) + (A : pr1 D Γ) (A' : pr1 D Γ') (A'' : pr1 D Γ'') + (f : Γ --> Γ') (g : Γ' --> Γ'') + (ff : pr1 (mor_weq Γ Γ' A A' f)) + (gg : pr1 (mor_weq Γ' Γ'' A' A'' g)), + ∑ (mor_comp : pr1 (mor_weq Γ Γ'' A A'' (f ;; g))), + pr2 (mor_weq Γ Γ'' A A'' (f ;; g)) mor_comp + = transportb _ (functor_comp (functor_identity C) f g) + (comp_disp (pr2 (mor_weq _ _ _ _ _) ff) (pr2 (mor_weq _ _ _ _ _) gg)). + + Definition ff_disp_functor_on_morphisms_comp_pos_iscontr + (mor_weq : ff_disp_functor_on_morphisms_pos) + (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) + : iscontr (ff_disp_functor_on_morphisms_comp_pos mor_weq). + Proof. + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros Γ''. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros A''. + apply impred_iscontr. intros f. + apply impred_iscontr. intros g. + apply impred_iscontr. intros ff. + apply impred_iscontr. intros gg. + set (mord := pr1 (mor_weq Γ Γ'' A A'' (f ;; g))). + set (mord_weq := pr2 (mor_weq Γ Γ'' A A'' (f ;; g))). + use (@iscontrweqf (∑ mor_comp : mord, + mor_comp + = invweq mord_weq (transportb _ (functor_comp (functor_identity C) f g) + (comp_disp (pr2 (mor_weq _ _ _ _ _) ff) (pr2 (mor_weq _ _ _ _ _) gg))))). + - use (weqtotal2 (idweq _)). intros mor_id. simpl. + use weq_iso. + + intros p. apply (maponpaths mord_weq p @ homotweqinvweq mord_weq _). + + intros p. apply (! homotinvweqweq mord_weq _ @ maponpaths (invmap mord_weq) p). + + intros p. apply mor_isaset. + + intros p. apply (@homsets_disp _ D'). + - apply iscontrcoconustot. + Defined. + + Definition ff_disp_functor_source_mor_isaset + (mor_weq : ff_disp_functor_on_morphisms_pos) + : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f)). + Proof. + intros Γ Γ' f A A'. + set (w := pr2 (mor_weq Γ Γ' A A' f)). + use (isofhlevelweqf 2 (invweq w)). + apply (@homsets_disp _ D'). + Defined. + + Definition ff_disp_functor_source_mor_isaset_iscontr + (mor_weq : ff_disp_functor_on_morphisms_pos) + : iscontr (∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))). + Proof. + apply iscontraprop1. + - apply impred_isaprop. intros Γ. + apply impred_isaprop. intros Γ'. + apply impred_isaprop. intros A. + apply impred_isaprop. intros A'. + apply impred_isaprop. intros f. + apply isapropisaset. + - apply ff_disp_functor_source_mor_isaset. + Defined. + + Definition ff_disp_functor_on_morphisms_idcomp_pos : UU + := ∑ (mor_weq : ff_disp_functor_on_morphisms_pos) + (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) + (mor_id : ff_disp_functor_on_morphisms_id_pos mor_weq) + , ff_disp_functor_on_morphisms_comp_pos mor_weq. + + Definition ff_disp_functor_on_morphisms_idcomp_pos_iscontr + : iscontr ff_disp_functor_on_morphisms_idcomp_pos. + Proof. + apply iscontr_total2. + - apply ff_disp_functor_on_morphisms_pos_iscontr. + - intros mor_weq. apply iscontr_total2. + + apply ff_disp_functor_source_mor_isaset_iscontr. + + intros mor_isaset. + apply iscontr_total2. + * apply ff_disp_functor_on_morphisms_id_pos_iscontr. + apply mor_isaset. + * intros ?. + apply ff_disp_functor_on_morphisms_comp_pos_iscontr. + apply mor_isaset. + Defined. + + Definition ff_disp_functor_on_morphisms_idcomp_sop + := ∑ (mor_disp : ∏ {x y : C}, pr1 D x -> pr1 D y -> (x --> y) -> UU) + (id_disp' : ∏ {x : C} (xx : pr1 D x), mor_disp xx xx (identity x)) + (comp_disp' : ∏ {x y z : C} {f : x --> y} {g : y --> z} + {xx : pr1 D x} {yy : pr1 D y} {zz : pr1 D z}, + mor_disp xx yy f -> mor_disp yy zz g -> mor_disp xx zz (f ;; g)) + (homsets_disp : ∏ {x y} {f : x --> y} {xx} {yy}, isaset (mor_disp xx yy f)) + (Fmor : ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), + (mor_disp xx yy f) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) + (Fid : ∏ x (xx : pr1 D x), + Fmor _ _ _ _ _ (id_disp' xx) = transportb _ (functor_id (functor_identity C) x) (id_disp (pr2 D _ xx))) + (Fcomp : ∏ x y z (xx : pr1 D x) yy zz (f : x --> y) (g : y --> z) + (ff : mor_disp xx yy f) (gg : mor_disp yy zz g), + Fmor _ _ _ _ _ (comp_disp' ff gg) + = transportb _ (functor_comp (functor_identity _) f g) (comp_disp (Fmor _ _ _ _ _ ff) (Fmor _ _ _ _ _ gg))) + , ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), + isweq (fun ff : mor_disp xx yy f => Fmor _ _ _ _ _ ff). + + Definition ff_disp_functor_on_morphisms_idcomp_sop_pos_weq + : ff_disp_functor_on_morphisms_idcomp_sop ≃ ff_disp_functor_on_morphisms_idcomp_pos. + Proof. + use weq_iso. + + - intros sop. + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + + exists (λ x y xx yy f, mor_disp x y xx yy f ,, Fmor x y xx yy f,, Fff x y xx yy f). + exists homsets_disp'. + exists (λ x xx, (id_disp' x xx ,, Fid x xx)). + exact (λ x y z xx yy zz f g ff gg, (comp_disp' x y z f g xx yy zz ff gg ,, Fcomp x y z xx yy zz f g ff gg)). + + - intros pos. + set (mor_disp := λ x y xx yy f, pr1 (pr1 pos x y xx yy f)). + set (Fmor := λ x y xx yy f, pr1 (pr2 (pr1 pos x y xx yy f))). + set (Fff := λ x y xx yy f, pr2 (pr2 (pr1 pos x y xx yy f))). + set (homsets_disp' := pr1 (pr2 pos)). + set (id_disp' := λ x xx, pr1 (pr1 (pr2 (pr2 pos)) x xx)). + set (Fid := λ x xx, pr2 (pr1 (pr2 (pr2 pos)) x xx)). + set (comp_disp' := λ x y z f g xx yy zz ff gg, pr1 (pr2 (pr2 (pr2 pos)) x y z xx yy zz f g ff gg)). + set (Fcomp := λ x y z xx yy zz f g ff gg, pr2 (pr2 (pr2 (pr2 pos)) x y z xx yy zz f g ff gg)). + + exists mor_disp. + exists id_disp'. + exists comp_disp'. + exists homsets_disp'. + exists Fmor. + exists Fid. + exists Fcomp. + exact Fff. + - intros ?. apply idpath. + - intros ?. apply idpath. + Defined. + + Definition source_disp_cat_data_of_ff_disp_functor_on_morphisms_idcomp_sop + : ff_disp_functor_on_morphisms_idcomp_sop → disp_cat_data C. + Proof. + intros sop. + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + + use tpair. + - exists (pr1 D). apply mor_disp. + - exact (id_disp' , comp_disp'). + Defined. + + Definition ff_disp_functor_mor_sop : UU + := ∑ (mor_idcomp : ff_disp_functor_on_morphisms_idcomp_sop), + disp_cat_axioms _ (source_disp_cat_data_of_ff_disp_functor_on_morphisms_idcomp_sop + mor_idcomp). + + Definition ff_disp_functor_mor_sop_iscontr + : iscontr ff_disp_functor_mor_sop. + Proof. + apply iscontr_total2. + - apply (iscontrweqb ff_disp_functor_on_morphisms_idcomp_sop_pos_weq). + apply ff_disp_functor_on_morphisms_idcomp_pos_iscontr. + - intros sop. + apply iscontr_total2. + + + apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros f. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros ff. + apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (w := λ g, (Fmor _ _ A A' g,, Fff _ _ _ _ _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w _)). + etrans. apply maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths, maponpaths_2. apply Fid. + etrans. apply maponpaths, maponpaths. apply id_left_disp. + etrans. apply maponpaths. apply transport_b_b. simpl. + apply homot_invweq_transportb_weq. + + + intros ?. + apply iscontr_total2. + + * apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros f. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros ff. + apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (w := λ g, (Fmor _ _ A A' g,, Fff _ _ _ _ _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w _)). + etrans. apply maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths, maponpaths. apply Fid. + etrans. apply maponpaths, maponpaths. apply id_right_disp. + etrans. apply maponpaths. apply transport_b_b. simpl. + apply homot_invweq_transportb_weq. + + * intros ?. apply iscontr_total2. + + -- apply impred_iscontr. intros Γ. + apply impred_iscontr. intros Γ'. + apply impred_iscontr. intros Γ''. + apply impred_iscontr. intros Γ'''. + apply impred_iscontr. intros f. + apply impred_iscontr. intros g. + apply impred_iscontr. intros h. + apply impred_iscontr. intros A. + apply impred_iscontr. intros A'. + apply impred_iscontr. intros A''. + apply impred_iscontr. intros A'''. + apply impred_iscontr. intros ff. + apply impred_iscontr. intros gg. + apply impred_iscontr. intros hh. + apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + set (w := λ g, (Fmor _ _ A A''' g,, Fff _ _ _ _ _)). + etrans. apply pathsinv0. apply (homotinvweqweq (w (f ;; (g ;; h)))). + etrans. apply maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths, maponpaths. apply Fcomp. + etrans. apply maponpaths, maponpaths. apply assoc_disp. + etrans. apply maponpaths. apply transport_b_b. + (* WORK IN PROGRESS *) + etrans. apply maponpaths, maponpaths, maponpaths_2, pathsinv0, Fcomp. + etrans. apply maponpaths, maponpaths, pathsinv0, Fcomp. + apply homot_invweq_transportb_weq. + -- intros ?. + set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). + apply iscontraprop1. + ++ apply impred_isaprop. intros Γ. + apply impred_isaprop. intros Γ'. + apply impred_isaprop. intros f. + apply impred_isaprop. intros A. + apply impred_isaprop. intros A'. + apply isapropisaset. + ++ apply homsets_disp'. + Defined. + + End FullyFaithfulFunctorOnMorphisms. + + Section FullyFaithfulFunctorWithMorphisms. + + (* Fully faithful displayed functor (over identity functor on C) into D' + * (equipped with contractible action on morphisms). *) + Definition ff_disp_functor_with_morphisms + {C : category} (D' : disp_cat C) + : UU + := ∑ (D : ff_disp_functor_on_objects D'), ff_disp_functor_mor_sop D. + + (* Source displayed category over C + * extracted from a fully faithful displayed functor (over identity functor on C) *) + Definition source_disp_cat_from_ff_disp_functor_with_morphisms + {C : category} {D' : disp_cat C} + (Fsop : ff_disp_functor_with_morphisms D') + : disp_cat C. + Proof. + set (sop := pr1 (pr2 Fsop)). + + set (ob_disp := pr1 (pr1 Fsop)). + set (axioms_d := pr2 (pr2 Fsop)). + + set (mor_disp := pr1 sop). + set (id_disp' := pr1 (pr2 sop)). + set (comp_disp' := pr1 (pr2 (pr2 sop))). + + exact (((ob_disp ,, mor_disp) ,, (id_disp' , comp_disp')) ,, axioms_d). + Defined. + + Definition disp_functor_from_ff_disp_functor_with_morphisms + {C : category} {D' : disp_cat C} + (Fsop : ff_disp_functor_with_morphisms D') + : disp_functor (functor_identity C) (source_disp_cat_from_ff_disp_functor_with_morphisms Fsop) D'. + Proof. + set (sop := pr1 (pr2 Fsop)). + + set (Fob := pr2 (pr1 Fsop)). + set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). + set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). + set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + + exact ((Fob,,Fmor),,(Fid,Fcomp)). + Defined. + + Coercion disp_functor_from_ff_disp_functor_with_morphisms + : ff_disp_functor_with_morphisms >-> disp_functor. + + Definition disp_functor_from_ff_disp_functor_with_morphisms_is_ff + {C : category} {D' : disp_cat C} + (Fsop : ff_disp_functor_with_morphisms D') + : disp_functor_ff (disp_functor_from_ff_disp_functor_with_morphisms Fsop). + Proof. + set (sop := pr1 (pr2 Fsop)). + set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). + exact Fff. + Defined. + + Definition ff_disp_functor_with_morphisms_eq + {C : category} (D' : disp_cat C) + (X Y : ff_disp_functor_with_morphisms D') + (e : pr1 X = pr1 Y) + : X = Y. + Proof. + use total2_paths_f. + - apply e. + - apply isapropifcontr. + apply ff_disp_functor_mor_sop_iscontr. + Defined. + + Definition ff_disp_functor_explicit + {C : category} (D' : disp_cat C) + : UU + := ∑ (D : disp_cat C) (F : disp_functor (functor_identity _) D D'), disp_functor_ff F. + + Definition ff_disp_functor_with_morphisms_weq + {C : category} {D' : disp_cat C} + : ff_disp_functor_with_morphisms D' ≃ ff_disp_functor_explicit D'. + Proof. + use weq_iso. + + - intros Fsop. + exists (source_disp_cat_from_ff_disp_functor_with_morphisms Fsop). + exists (disp_functor_from_ff_disp_functor_with_morphisms Fsop). + apply disp_functor_from_ff_disp_functor_with_morphisms_is_ff. + + - intros F. + + set (ob_disp := pr1 (pr1 (pr1 (pr1 F)))). + set (mor_disp := pr2 (pr1 (pr1 (pr1 F)))). + set (id_disp' := pr1 (pr2 (pr1 (pr1 F)))). + set (comp_disp' := pr2 (pr2 (pr1 (pr1 F)))). + set (axioms_d := pr2 (pr1 F)). + set (homsets_disp' := pr2 (pr2 (pr2 axioms_d))). + + set (Fob := pr1 (pr1 (pr1 (pr2 F)))). + set (Fmor := pr2 (pr1 (pr1 (pr2 F)))). + set (Fid := pr1 (pr2 (pr1 (pr2 F)))). + set (Fcomp := pr2 (pr2 (pr1 (pr2 F)))). + set (Fff := pr2 (pr2 F)). + + exists (ob_disp ,, Fob). + exists (mor_disp ,, id_disp' ,, comp_disp' ,, homsets_disp' ,, Fmor ,, Fid ,, Fcomp ,, Fff). + exact axioms_d. + + - intros ?. apply ff_disp_functor_with_morphisms_eq. apply idpath. + - intros ?. apply idpath. + Defined. + + Definition ff_disp_functor_on_objects_ff_disp_functor_with_morphisms_weq + {C : category} {D' : disp_cat C} + : ff_disp_functor_on_objects D' ≃ ff_disp_functor_with_morphisms D'. + Proof. + apply invweq, weqpr1. + intros D. + apply ff_disp_functor_mor_sop_iscontr. + Defined. + + End FullyFaithfulFunctorWithMorphisms. + + (* Fully faithful displayed functor (over identity functor on C) into D'. *) + Definition ff_disp_functor + {C : category} (D' : disp_cat C) + : UU + := ff_disp_functor_on_objects D'. + + Definition ff_disp_functor_weq + {C : category} {D' : disp_cat C} + : ff_disp_functor D' ≃ ff_disp_functor_explicit D'. + Proof. + eapply weqcomp. apply ff_disp_functor_on_objects_ff_disp_functor_with_morphisms_weq. + apply ff_disp_functor_with_morphisms_weq. + Defined. + + Definition source_disp_cat_from_ff_disp_functor + {C : category} {D' : disp_cat C} + (F : ff_disp_functor D') + : disp_cat C + := pr1 (ff_disp_functor_weq F). + + Definition disp_functor_from_ff_disp_functor + {C : category} {D' : disp_cat C} + (F : ff_disp_functor D') + : disp_functor (functor_identity C) (source_disp_cat_from_ff_disp_functor F) D' + := pr1 (pr2 (ff_disp_functor_weq F)). + + Coercion disp_functor_from_ff_disp_functor : ff_disp_functor >-> disp_functor. + + Definition disp_functor_from_ff_disp_functor_is_ff + {C : category} {D' : disp_cat C} + (F : ff_disp_functor D') + : disp_functor_ff F + := pr2 (pr2 (ff_disp_functor_weq F)). + +End FullyFaithfulDispFunctor. diff --git a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v index 6d34688f..24270e69 100644 --- a/TypeTheory/ALV2/TypeCat_ComprehensionCat.v +++ b/TypeTheory/ALV2/TypeCat_ComprehensionCat.v @@ -28,6 +28,8 @@ Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.ALV1.TypeCat. +Require Import TypeTheory.ALV2.FullyFaithfulDispFunctor. + Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. @@ -62,602 +64,6 @@ Section Auxiliary. apply idpath. Defined. - (* TODO: move upstream? *) - Lemma weqtotaltoforall3 {X : UU} - (P1 : X → UU) - (P2 : ∏ x : X, P1 x → UU) - (P3 : ∏ (x : X) (y : P1 x), P2 x y → UU) - : (∑ (p1 : ∏ x : X, P1 x) (p2 : ∏ x : X, P2 x (p1 x)), ∏ x : X, P3 x (p1 x) (p2 x)) - ≃ (∏ x : X, ∑ (p1 : P1 x) (p2 : P2 x p1), P3 x p1 p2). - Proof. - eapply weqcomp. - apply (weqtotal2asstol - (λ p1, ∏ x : X, P2 x (p1 x)) - (λ p12, ∏ x : X, P3 x (pr1 p12 x) (pr2 p12 x)) - ). - eapply weqcomp. - use weqtotal2. 3: apply weqtotaltoforall. - - exact (λ p12, ∏ x : X, P3 x (pr1 (p12 x)) (pr2 (p12 x))). - - intros x. apply idweq. - - - eapply weqcomp. - apply (weqtotaltoforall - (λ x : X, ∑ y : P1 x, P2 x y) - (λ (x : X) p12, P3 x (pr1 p12) (pr2 p12)) - ). - apply weqonsecfibers. - intros x. - apply weqtotal2asstor. - Defined. - - (* TODO: move upstream? *) - Lemma iscontr_total2 - {X : UU} {P : X → UU} - : iscontr X → (∏ x : X, iscontr (P x)) → iscontr (∑ (x : X), P x). - Proof. - intros X_contr P_contr. - use tpair. - - exists (pr1 X_contr). apply P_contr. - - intros xp. - use total2_paths_f. - + apply X_contr. - + apply P_contr. - Defined. - - (* TODO: move upstream? *) - Lemma idpath_transportb - {X : UU} (P : X → UU) - (x : X) (p : P x) - : transportb P (idpath x) p = p. - Proof. - apply idpath. - Defined. - - (* TODO: move upstream? *) - Lemma homot_invweq_transportb_weq - (Z : UU) - (z z' : Z) - (X Y : Z → UU) - (e : z = z') - (w : ∏ z : Z, X z ≃ Y z) - (x : X z') - : invmap (w z) (transportb Y e (w z' x)) = transportb X e x. - Proof. - induction e. - etrans. apply maponpaths, idpath_transportb. - apply homotinvweqweq. - Defined. - - Definition disp_ff_functor_to_on_objects - {C : category} - (D' : disp_cat C) - : UU - := ∑ (obd : C → UU) - , ∏ (Γ : C), obd Γ → D' Γ. - - Definition disp_ff_functor_on_morphisms_sop - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : UU - := ∑ (mord : ∏ Γ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - (functor_mord : ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , (mord _ _ A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) - , ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , isweq (functor_mord Γ Γ' A A' f). - - Definition disp_ff_functor_on_morphisms_pos - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : UU - := ∏ Γ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ'), - ∑ (mord : UU), mord ≃ (pr2 D _ A -->[ f ] pr2 D _ A'). - - Definition disp_ff_functor_on_morphisms_sop_pos_weq - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : disp_ff_functor_on_morphisms_sop D ≃ disp_ff_functor_on_morphisms_pos D. - Proof. - eapply weqcomp. - apply (weqtotaltoforall3 - (λ Γ, ∏ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - (λ Γ mord, ∏ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , (mord _ A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) - (λ Γ mord functor_mord, - ∏ Γ' (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , isweq (functor_mord Γ' A A' f))). - apply weqonsecfibers. intros Γ. - - eapply weqcomp. - apply (weqtotaltoforall3 - (λ Γ', (pr1 D Γ) → (pr1 D Γ') → (Γ --> Γ') → UU) - (λ Γ' mord, ∏ (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , (mord A A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) - (λ Γ' mord functor_mord, - ∏ (A : pr1 D Γ) (A' : pr1 D Γ') (f : Γ --> Γ') - , isweq (functor_mord A A' f))). - apply weqonsecfibers. intros Γ'. - - eapply weqcomp. - apply (weqtotaltoforall3 - (λ A, (pr1 D Γ') → (Γ --> Γ') → UU) - (λ A mord, ∏ (A' : pr1 D Γ') (f : Γ --> Γ') - , (mord A' f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) - (λ A mord functor_mord, - ∏ (A' : pr1 D Γ') (f : Γ --> Γ') - , isweq (functor_mord A' f))). - apply weqonsecfibers. intros A. - - eapply weqcomp. - apply (weqtotaltoforall3 - (λ A', (Γ --> Γ') → UU) - (λ A' mord, ∏ (f : Γ --> Γ') - , (mord f) -> (pr2 D _ A -->[ f ] pr2 D _ A')) - (λ A' mord functor_mord, - ∏ (f : Γ --> Γ') - , isweq (functor_mord f))). - apply weqonsecfibers. intros A'. - - eapply weqcomp. - apply (weqtotaltoforall3 - (λ f, UU) - (λ f mord, mord -> (pr2 D _ A -->[ f ] pr2 D _ A')) - (λ f mord functor_mord, isweq functor_mord)). - apply idweq. - Defined. - - Definition disp_ff_functor_on_morphisms_pos_iscontr - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : iscontr (disp_ff_functor_on_morphisms_pos D). - Proof. - apply impred_iscontr. intros Γ. - apply impred_iscontr. intros Γ'. - apply impred_iscontr. intros A. - apply impred_iscontr. intros A'. - apply impred_iscontr. intros f. - use (@iscontrweqf (∑ mord : UU, mord = pr2 D Γ A -->[f] pr2 D Γ' A')). - - use (weqtotal2 (idweq _)). intros mord. apply univalenceweq. - - apply iscontrcoconustot. - Defined. - - Definition disp_ff_functor_on_morphisms_pos_isaprop - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : isaprop (disp_ff_functor_on_morphisms_pos D). - Proof. - apply isapropifcontr, disp_ff_functor_on_morphisms_pos_iscontr. - Defined. - - Definition disp_ff_functor_on_morphisms_id_pos - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mor_weq : disp_ff_functor_on_morphisms_pos D) - : UU - := ∏ (Γ : C) (A : pr1 D Γ), - ∑ (mor_id : pr1 (mor_weq Γ Γ A A (identity Γ))), - pr1 (pr2 (mor_weq Γ Γ A A (identity Γ))) mor_id - = transportb (mor_disp (pr2 D Γ A) (pr2 D Γ A)) - (functor_id (functor_identity C) Γ) (id_disp (pr2 D Γ A)). - - Definition disp_ff_functor_on_morphisms_id_pos_iscontr - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mor_weq : disp_ff_functor_on_morphisms_pos D) - (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) - : iscontr (disp_ff_functor_on_morphisms_id_pos D mor_weq). - Proof. - apply impred_iscontr. intros Γ. - apply impred_iscontr. intros A. - set (mord := pr1 (mor_weq Γ Γ A A (identity Γ))). - set (mord_weq := pr2 (mor_weq Γ Γ A A (identity Γ))). - use (@iscontrweqf (∑ mor_id : mord, mor_id = invweq mord_weq - (transportb (mor_disp (pr2 D Γ A) (pr2 D Γ A)) - (functor_id (functor_identity C) Γ) (id_disp (pr2 D Γ A))))). - - use (weqtotal2 (idweq _)). intros mor_id. simpl. - use weq_iso. - + intros p. apply (maponpaths mord_weq p @ homotweqinvweq mord_weq _). - + intros p. apply (! homotinvweqweq mord_weq _ @ maponpaths (invmap mord_weq) p). - + intros p. apply mor_isaset. - + intros p. apply (@homsets_disp _ D'). - - apply iscontrcoconustot. - Defined. - - Definition disp_ff_functor_on_morphisms_comp_pos - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mor_weq : disp_ff_functor_on_morphisms_pos D) - : UU - := ∏ (Γ Γ' Γ'' : C) - (A : pr1 D Γ) (A' : pr1 D Γ') (A'' : pr1 D Γ'') - (f : Γ --> Γ') (g : Γ' --> Γ'') - (ff : pr1 (mor_weq Γ Γ' A A' f)) - (gg : pr1 (mor_weq Γ' Γ'' A' A'' g)), - ∑ (mor_comp : pr1 (mor_weq Γ Γ'' A A'' (f ;; g))), - pr2 (mor_weq Γ Γ'' A A'' (f ;; g)) mor_comp - = transportb _ (functor_comp (functor_identity C) f g) - (comp_disp (pr2 (mor_weq _ _ _ _ _) ff) (pr2 (mor_weq _ _ _ _ _) gg)). - - Definition disp_ff_functor_on_morphisms_comp_pos_iscontr - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mor_weq : disp_ff_functor_on_morphisms_pos D) - (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) - : iscontr (disp_ff_functor_on_morphisms_comp_pos D mor_weq). - Proof. - apply impred_iscontr. intros Γ. - apply impred_iscontr. intros Γ'. - apply impred_iscontr. intros Γ''. - apply impred_iscontr. intros A. - apply impred_iscontr. intros A'. - apply impred_iscontr. intros A''. - apply impred_iscontr. intros f. - apply impred_iscontr. intros g. - apply impred_iscontr. intros ff. - apply impred_iscontr. intros gg. - set (mord := pr1 (mor_weq Γ Γ'' A A'' (f ;; g))). - set (mord_weq := pr2 (mor_weq Γ Γ'' A A'' (f ;; g))). - use (@iscontrweqf (∑ mor_comp : mord, - mor_comp - = invweq mord_weq (transportb _ (functor_comp (functor_identity C) f g) - (comp_disp (pr2 (mor_weq _ _ _ _ _) ff) (pr2 (mor_weq _ _ _ _ _) gg))))). - - use (weqtotal2 (idweq _)). intros mor_id. simpl. - use weq_iso. - + intros p. apply (maponpaths mord_weq p @ homotweqinvweq mord_weq _). - + intros p. apply (! homotinvweqweq mord_weq _ @ maponpaths (invmap mord_weq) p). - + intros p. apply mor_isaset. - + intros p. apply (@homsets_disp _ D'). - - apply iscontrcoconustot. - Defined. - - Definition disp_ff_functor_source_mor_isaset - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mor_weq : disp_ff_functor_on_morphisms_pos D) - : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f)). - Proof. - intros Γ Γ' f A A'. - set (w := pr2 (mor_weq Γ Γ' A A' f)). - use (isofhlevelweqf 2 (invweq w)). - apply (@homsets_disp _ D'). - Defined. - - Definition disp_ff_functor_source_mor_isaset_iscontr - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - (mor_weq : disp_ff_functor_on_morphisms_pos D) - : iscontr (∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))). - Proof. - apply iscontraprop1. - - apply impred_isaprop. intros Γ. - apply impred_isaprop. intros Γ'. - apply impred_isaprop. intros A. - apply impred_isaprop. intros A'. - apply impred_isaprop. intros f. - apply isapropisaset. - - apply disp_ff_functor_source_mor_isaset. - Defined. - - Definition disp_ff_functor_on_morphisms_idcomp_pos - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : UU - := ∑ (mor_weq : disp_ff_functor_on_morphisms_pos D) - (mor_isaset : ∏ Γ Γ' f (A : pr1 D Γ) (A' : pr1 D Γ'), isaset (pr1 (mor_weq _ _ A A' f))) - (mor_id : disp_ff_functor_on_morphisms_id_pos D mor_weq) - , disp_ff_functor_on_morphisms_comp_pos D mor_weq. - - Definition disp_ff_functor_on_morphisms_idcomp_pos_iscontr - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : iscontr (disp_ff_functor_on_morphisms_idcomp_pos D). - Proof. - apply iscontr_total2. - - apply disp_ff_functor_on_morphisms_pos_iscontr. - - intros mor_weq. apply iscontr_total2. - + apply disp_ff_functor_source_mor_isaset_iscontr. - + intros mor_isaset. - apply iscontr_total2. - * apply disp_ff_functor_on_morphisms_id_pos_iscontr. - apply mor_isaset. - * intros ?. - apply disp_ff_functor_on_morphisms_comp_pos_iscontr. - apply mor_isaset. - Defined. - - Definition disp_ff_functor_on_morphisms_idcomp_sop - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - := ∑ (mor_disp : ∏ {x y : C}, pr1 D x -> pr1 D y -> (x --> y) -> UU) - (id_disp' : ∏ {x : C} (xx : pr1 D x), mor_disp xx xx (identity x)) - (comp_disp' : ∏ {x y z : C} {f : x --> y} {g : y --> z} - {xx : pr1 D x} {yy : pr1 D y} {zz : pr1 D z}, - mor_disp xx yy f -> mor_disp yy zz g -> mor_disp xx zz (f ;; g)) - (homsets_disp : ∏ {x y} {f : x --> y} {xx} {yy}, isaset (mor_disp xx yy f)) - (Fmor : ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), - (mor_disp xx yy f) -> (pr2 D _ xx -->[ f ] pr2 D _ yy)) - (Fid : ∏ x (xx : pr1 D x), - Fmor _ _ _ _ _ (id_disp' xx) = transportb _ (functor_id (functor_identity C) x) (id_disp (pr2 D _ xx))) - (Fcomp : ∏ x y z (xx : pr1 D x) yy zz (f : x --> y) (g : y --> z) - (ff : mor_disp xx yy f) (gg : mor_disp yy zz g), - Fmor _ _ _ _ _ (comp_disp' ff gg) - = transportb _ (functor_comp (functor_identity _) f g) (comp_disp (Fmor _ _ _ _ _ ff) (Fmor _ _ _ _ _ gg))) - , ∏ x y (xx : pr1 D x) (yy : pr1 D y) (f : x --> y), - isweq (fun ff : mor_disp xx yy f => Fmor _ _ _ _ _ ff). - - Definition disp_ff_functor_on_morphisms_idcomp_sop_pos_weq - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : disp_ff_functor_on_morphisms_idcomp_sop D ≃ disp_ff_functor_on_morphisms_idcomp_pos D. - Proof. - use weq_iso. - - - intros sop. - set (mor_disp := pr1 sop). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). - set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). - set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). - set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - - exists (λ x y xx yy f, mor_disp x y xx yy f ,, Fmor x y xx yy f,, Fff x y xx yy f). - exists homsets_disp'. - exists (λ x xx, (id_disp' x xx ,, Fid x xx)). - exact (λ x y z xx yy zz f g ff gg, (comp_disp' x y z f g xx yy zz ff gg ,, Fcomp x y z xx yy zz f g ff gg)). - - - intros pos. - set (mor_disp := λ x y xx yy f, pr1 (pr1 pos x y xx yy f)). - set (Fmor := λ x y xx yy f, pr1 (pr2 (pr1 pos x y xx yy f))). - set (Fff := λ x y xx yy f, pr2 (pr2 (pr1 pos x y xx yy f))). - set (homsets_disp' := pr1 (pr2 pos)). - set (id_disp' := λ x xx, pr1 (pr1 (pr2 (pr2 pos)) x xx)). - set (Fid := λ x xx, pr2 (pr1 (pr2 (pr2 pos)) x xx)). - set (comp_disp' := λ x y z f g xx yy zz ff gg, pr1 (pr2 (pr2 (pr2 pos)) x y z xx yy zz f g ff gg)). - set (Fcomp := λ x y z xx yy zz f g ff gg, pr2 (pr2 (pr2 (pr2 pos)) x y z xx yy zz f g ff gg)). - - exists mor_disp. - exists id_disp'. - exists comp_disp'. - exists homsets_disp'. - exists Fmor. - exists Fid. - exists Fcomp. - exact Fff. - - intros ?. apply idpath. - - intros ?. apply idpath. - Defined. - - Definition source_disp_cat_data_of_disp_ff_functor_on_morphisms_idcomp_sop - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : disp_ff_functor_on_morphisms_idcomp_sop D → disp_cat_data C. - Proof. - intros sop. - set (mor_disp := pr1 sop). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - - use tpair. - - exists (pr1 D). apply mor_disp. - - exact (id_disp' , comp_disp'). - Defined. - - Definition disp_ff_functor_mor_sop - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : UU - := ∑ (mor_idcomp : disp_ff_functor_on_morphisms_idcomp_sop D), - disp_cat_axioms _ (source_disp_cat_data_of_disp_ff_functor_on_morphisms_idcomp_sop - D mor_idcomp). - - Definition disp_ff_functor_mor_sop_iscontr - {C : category} {D' : disp_cat C} - (D : disp_ff_functor_to_on_objects D') - : iscontr (disp_ff_functor_mor_sop D). - Proof. - apply iscontr_total2. - - apply (iscontrweqb (disp_ff_functor_on_morphisms_idcomp_sop_pos_weq _)). - apply disp_ff_functor_on_morphisms_idcomp_pos_iscontr. - - intros sop. - apply iscontr_total2. - - + apply impred_iscontr. intros Γ. - apply impred_iscontr. intros Γ'. - apply impred_iscontr. intros f. - apply impred_iscontr. intros A. - apply impred_iscontr. intros A'. - apply impred_iscontr. intros ff. - apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). - set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). - set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (w := λ g, (Fmor _ _ A A' g,, Fff _ _ _ _ _)). - etrans. apply pathsinv0. apply (homotinvweqweq (w _)). - etrans. apply maponpaths. apply Fcomp. - etrans. apply maponpaths, maponpaths, maponpaths_2. apply Fid. - etrans. apply maponpaths, maponpaths. apply id_left_disp. - etrans. apply maponpaths. apply transport_b_b. simpl. - apply homot_invweq_transportb_weq. - - + intros ?. - apply iscontr_total2. - - * apply impred_iscontr. intros Γ. - apply impred_iscontr. intros Γ'. - apply impred_iscontr. intros f. - apply impred_iscontr. intros A. - apply impred_iscontr. intros A'. - apply impred_iscontr. intros ff. - apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). - set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). - set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (w := λ g, (Fmor _ _ A A' g,, Fff _ _ _ _ _)). - etrans. apply pathsinv0. apply (homotinvweqweq (w _)). - etrans. apply maponpaths. apply Fcomp. - etrans. apply maponpaths, maponpaths, maponpaths. apply Fid. - etrans. apply maponpaths, maponpaths. apply id_right_disp. - etrans. apply maponpaths. apply transport_b_b. simpl. - apply homot_invweq_transportb_weq. - - * intros ?. apply iscontr_total2. - - -- apply impred_iscontr. intros Γ. - apply impred_iscontr. intros Γ'. - apply impred_iscontr. intros Γ''. - apply impred_iscontr. intros Γ'''. - apply impred_iscontr. intros f. - apply impred_iscontr. intros g. - apply impred_iscontr. intros h. - apply impred_iscontr. intros A. - apply impred_iscontr. intros A'. - apply impred_iscontr. intros A''. - apply impred_iscontr. intros A'''. - apply impred_iscontr. intros ff. - apply impred_iscontr. intros gg. - apply impred_iscontr. intros hh. - apply iscontraprop1. apply (pr1 (pr2 (pr2 (pr2 sop)))). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). - set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). - set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - set (w := λ g, (Fmor _ _ A A''' g,, Fff _ _ _ _ _)). - etrans. apply pathsinv0. apply (homotinvweqweq (w (f ;; (g ;; h)))). - etrans. apply maponpaths. apply Fcomp. - etrans. apply maponpaths, maponpaths, maponpaths. apply Fcomp. - etrans. apply maponpaths, maponpaths. apply assoc_disp. - etrans. apply maponpaths. apply transport_b_b. - (* WORK IN PROGRESS *) - etrans. apply maponpaths, maponpaths, maponpaths_2, pathsinv0, Fcomp. - etrans. apply maponpaths, maponpaths, pathsinv0, Fcomp. - apply homot_invweq_transportb_weq. - -- intros ?. - set (homsets_disp' := pr1 (pr2 (pr2 (pr2 sop)))). - apply iscontraprop1. - ++ apply impred_isaprop. intros Γ. - apply impred_isaprop. intros Γ'. - apply impred_isaprop. intros f. - apply impred_isaprop. intros A. - apply impred_isaprop. intros A'. - apply isapropisaset. - ++ apply homsets_disp'. - Defined. - - Definition disp_ff_functor_sop - {C : category} (D' : disp_cat C) - : UU - := ∑ (D : disp_ff_functor_to_on_objects D'), - disp_ff_functor_mor_sop D. - - Definition source_disp_cat_of_disp_ff_functor_sop - {C : category} {D' : disp_cat C} - (Fsop : disp_ff_functor_sop D') - : disp_cat C. - Proof. - set (sop := pr1 (pr2 Fsop)). - - set (ob_disp := pr1 (pr1 Fsop)). - set (axioms_d := pr2 (pr2 Fsop)). - - set (mor_disp := pr1 sop). - set (id_disp' := pr1 (pr2 sop)). - set (comp_disp' := pr1 (pr2 (pr2 sop))). - - exact (((ob_disp ,, mor_disp) ,, (id_disp' , comp_disp')) ,, axioms_d). - Defined. - - Definition disp_functor_of_disp_ff_functor_sop - {C : category} {D' : disp_cat C} - (Fsop : disp_ff_functor_sop D') - : disp_functor (functor_identity C) (source_disp_cat_of_disp_ff_functor_sop Fsop) D'. - Proof. - set (sop := pr1 (pr2 Fsop)). - - set (Fob := pr2 (pr1 Fsop)). - set (Fmor := pr1 (pr2 (pr2 (pr2 (pr2 sop))))). - set (Fid := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 sop)))))). - set (Fcomp := pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - - exact ((Fob,,Fmor),,(Fid,Fcomp)). - Defined. - - Coercion disp_functor_of_disp_ff_functor_sop : disp_ff_functor_sop >-> disp_functor. - - Definition disp_functor_of_disp_ff_functor_sop_is_ff - {C : category} {D' : disp_cat C} - (Fsop : disp_ff_functor_sop D') - : disp_functor_ff (disp_functor_of_disp_ff_functor_sop Fsop). - Proof. - set (sop := pr1 (pr2 Fsop)). - set (Fff := pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 sop))))))). - exact Fff. - Defined. - - Definition disp_ff_functor_sop_eq - {C : category} (D' : disp_cat C) - (X Y : disp_ff_functor_sop D') - (e : pr1 X = pr1 Y) - : X = Y. - Proof. - use total2_paths_f. - - apply e. - - apply isapropifcontr. - apply disp_ff_functor_mor_sop_iscontr. - Defined. - - Definition disp_ff_functor_sop_disp_functor_ff_weq - {C : category} {D' : disp_cat C} - : disp_ff_functor_sop D' ≃ - ∑ (D : disp_cat C) (F : disp_functor (functor_identity _) D D'), disp_functor_ff F. - Proof. - use weq_iso. - - - intros Fsop. - exists (source_disp_cat_of_disp_ff_functor_sop Fsop). - exists (disp_functor_of_disp_ff_functor_sop Fsop). - apply disp_functor_of_disp_ff_functor_sop_is_ff. - - - intros F. - - set (ob_disp := pr1 (pr1 (pr1 (pr1 F)))). - set (mor_disp := pr2 (pr1 (pr1 (pr1 F)))). - set (id_disp' := pr1 (pr2 (pr1 (pr1 F)))). - set (comp_disp' := pr2 (pr2 (pr1 (pr1 F)))). - set (axioms_d := pr2 (pr1 F)). - set (homsets_disp' := pr2 (pr2 (pr2 axioms_d))). - - set (Fob := pr1 (pr1 (pr1 (pr2 F)))). - set (Fmor := pr2 (pr1 (pr1 (pr2 F)))). - set (Fid := pr1 (pr2 (pr1 (pr2 F)))). - set (Fcomp := pr2 (pr2 (pr1 (pr2 F)))). - set (Fff := pr2 (pr2 F)). - - exists (ob_disp ,, Fob). - exists (mor_disp ,, id_disp' ,, comp_disp' ,, homsets_disp' ,, Fmor ,, Fid ,, Fcomp ,, Fff). - exact axioms_d. - - - intros ?. apply disp_ff_functor_sop_eq. apply idpath. - - intros ?. apply idpath. - Defined. - - Definition disp_ff_functor_sop_disp_ff_functor_to_on_objects_weq - {C : category} {D' : disp_cat C} - : disp_ff_functor_to_on_objects D' ≃ disp_ff_functor_sop D'. - Proof. - apply invweq, weqpr1. - intros D. - apply disp_ff_functor_mor_sop_iscontr. - Defined. - End Auxiliary. Section TypeCat_ObjExt. @@ -1259,7 +665,7 @@ Section TypeCat_ComprehensionCat. Definition typecat_obj_ext_structure_disp_ff_functor_to_codomain_weq (C : category) - : typecat_obj_ext_structure C ≃ disp_ff_functor_to_on_objects (disp_codomain C). + : typecat_obj_ext_structure C ≃ ff_disp_functor (disp_codomain C). Proof. use weq_iso. - intros tc. @@ -1280,25 +686,26 @@ Section TypeCat_ComprehensionCat. Definition typecat_obj_ext_structure_ff_disp_functor_to_codomain_weq (C : category) - : typecat_obj_ext_structure C ≃ - ∑ (D : disp_cat C) - (F : disp_functor (functor_identity _) D (disp_codomain C)) - , disp_functor_ff F. + : typecat_obj_ext_structure C ≃ ff_disp_functor_explicit (disp_codomain C). Proof. eapply weqcomp. apply typecat_obj_ext_structure_disp_ff_functor_to_codomain_weq. - eapply weqcomp. apply disp_ff_functor_sop_disp_ff_functor_to_on_objects_weq. - apply disp_ff_functor_sop_disp_functor_ff_weq. + apply ff_disp_functor_weq. Defined. - Definition typecat_structure' (C : category) : UU - := ∑ (TC : typecat_obj_ext_structure C) - (reind : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), TC Γ') + Definition typecat_structure2' {C : category} + (TC : typecat_obj_ext_structure C) + : UU + := ∑ (reind : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), TC Γ') (q : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), (obj_ext_typecat Γ' (reind _ A _ f)) --> obj_ext_typecat Γ A ) (dpr_q : ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), (q _ A _ f) ;; (dpr_typecat_obj_ext A) = (dpr_typecat_obj_ext (reind _ A _ f)) ;; f), ∏ Γ (A : TC Γ) Γ' (f : Γ' --> Γ), isPullback _ _ _ _ (!dpr_q _ A _ f). + Definition typecat_structure' (C : category) : UU + := ∑ (TC : typecat_obj_ext_structure C), + typecat_structure2' TC. + Definition typecat_structure_typecat_structure'_weq (C : category) : typecat_structure C ≃ typecat_structure' C. @@ -1324,9 +731,27 @@ Section TypeCat_ComprehensionCat. Defined. Definition ff_comprehension_cat_structure (C : category) : UU - := ∑ (F : disp_ff_functor_sop (disp_codomain C)), - cleaving (source_disp_cat_of_disp_ff_functor_sop F) - × is_cartesian_disp_functor F. + := ∑ (F : ∑ (D : disp_cat C) + (F : disp_functor (functor_identity _) D (disp_codomain C)) + , disp_functor_ff F), + cleaving (pr1 F) × is_cartesian_disp_functor (pr1 (pr2 F)). + + Definition typecat_structure2'_cleaving_weq + {C : category} (TC : typecat_obj_ext_structure C) + : typecat_structure2' TC ≃ + (cleaving (pr1 (typecat_obj_ext_structure_ff_disp_functor_to_codomain_weq _ TC)) + × is_cartesian_disp_functor (pr1 (pr2 (typecat_obj_ext_structure_ff_disp_functor_to_codomain_weq _ TC)))). + Proof. + Abort. + + Definition typecat_structure'_ff_comprehension_cat_structure_weq + (C : category) + : typecat_structure' C ≃ ff_comprehension_cat_structure C. + Proof. + use weqtotal2. + - apply typecat_obj_ext_structure_ff_disp_functor_to_codomain_weq. + - intros TC. simpl. + Abort. Definition typecat_ff_comprehension_cat_structure_weq (C : category) : typecat_structure C ≃ ff_comprehension_cat_structure C.