From 7f77246bb0012ae918c4a9d3b91a3bd76562b223 Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Thu, 19 Sep 2024 06:47:49 +0200 Subject: [PATCH] Adapt to che renamings of the UniMath rezk completion files --- TypeTheory/Articles/ALV_2017.v | 20 +++--- TypeTheory/Articles/ALV_2018.v | 10 +-- TypeTheory/Auxiliary/CategoryTheoryImports.v | 2 +- TypeTheory/CwF/CwF_def.v | 66 ++++++++++---------- TypeTheory/CwF/RepMaps.v | 22 +++---- TypeTheory/OtherDefs/CwF_Pitts_completion.v | 2 +- TypeTheory/RelUniv/RelUnivTransfer.v | 48 +++++++------- TypeTheory/RelUniv/RelUnivYonedaCompletion.v | 8 +-- 8 files changed, 89 insertions(+), 89 deletions(-) diff --git a/TypeTheory/Articles/ALV_2017.v b/TypeTheory/Articles/ALV_2017.v index 95b0b3e3..9762b0c5 100644 --- a/TypeTheory/Articles/ALV_2017.v +++ b/TypeTheory/Articles/ALV_2017.v @@ -6,7 +6,7 @@ (** -This file accompanies the article _Categorical structures for type theory in univalent foundations_, Ahrens, Lumsdaine, Voevodsky, 2017, Logical Methods in Computer Science 14(3), https://arxiv.org/abs/1705.04310, +This file accompanies the article _Categorical structures for type theory in univalent foundations_, Ahrens, Lumsdaine, Voevodsky, 2017, Logical Methods in Computer Science 14(3), https://arxiv.org/abs/1705.04310, https://doi.org/10.23638/LMCS-14(3:18)2018 This file should contain _no substantial formalisation_, and should not be imported. Its aim is to provide an index from the results of the article ALV 2017 to their locations in the actual formalisation, so that they remain easily available and checkable for readers of the article, even as the library continues to evolve. @@ -15,7 +15,7 @@ This file should contain _no substantial formalisation_, and should not be impor Require Import UniMath.Foundations.Sets. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -53,14 +53,14 @@ Defined. (** ** Compatible [qq] from term structure and vice versa *) -Definition compatible_qq_from_term {C : category} +Definition compatible_qq_from_term {C : category} {X : obj_ext_structure C} (Y : term_fun_structure C X) : compatible_qq_morphism_structure Y. Proof. apply compatible_qq_from_term. Defined. -Definition compatible_term_from_qq {C : category} +Definition compatible_term_from_qq {C : category} {X : obj_ext_structure C} (Z : qq_morphism_structure X) : compatible_term_structure Z. Proof. @@ -90,11 +90,11 @@ Defined. (** * Map from [cwf_structure C] to [rep_map C] *) -(** and proof that the map is an equivalence when [C] is univalent *) +(** and proof that the map is an equivalence when [C] is univalent *) Definition from_cwf_to_rep (C : category) - : cwf_structure C → rep_map C. -Proof. + : cwf_structure C → rep_map C. +Proof. exact (from_cwf_to_rep_map C). Defined. @@ -111,7 +111,7 @@ Defined. Definition transfer_cwf_weak_equivalence {C D : category} (F : C ⟶ D) : fully_faithful F → essentially_surjective F - → is_univalent D → + → is_univalent D → cwf_structure C → cwf_structure D. Proof. apply transfer_cwf_weak_equiv. @@ -119,8 +119,8 @@ Defined. (** * Transfer of [rep_map]s along weak equivalences *) -Definition transfer_rep_map_weak_equivalence {C D : category} - (F : C ⟶ D) +Definition transfer_rep_map_weak_equivalence {C D : category} + (F : C ⟶ D) : fully_faithful F → essentially_surjective F → rep_map C ≃ rep_map D. Proof. apply transfer_rep_map_weak_equiv. diff --git a/TypeTheory/Articles/ALV_2018.v b/TypeTheory/Articles/ALV_2018.v index 410668b3..772375d2 100644 --- a/TypeTheory/Articles/ALV_2018.v +++ b/TypeTheory/Articles/ALV_2018.v @@ -12,7 +12,7 @@ This file is intended to accompany a sequel article to ALV-2017, currently in (d Require Import UniMath.Foundations.Sets. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -82,10 +82,10 @@ Admitted. (** * Map from [cwf_structure C] to [rep_map C] *) -(** and proof that the map is an equivalence when [C] is univalent *) +(** and proof that the map is an equivalence when [C] is univalent *) Definition functor_cwf_to_rep (C : category) - : cwf_structure_cat C ⟶ rep_map_cat C. + : cwf_structure_cat C ⟶ rep_map_cat C. Admitted. Proposition fully_faithful_cwf_to_rep (C : category) @@ -100,7 +100,7 @@ Admitted. Definition transfer_cwf_weak_equivalence {C D : category} (F : C ⟶ D) : fully_faithful F → essentially_surjective F - → is_univalent D → + → is_univalent D → cwf_structure_cat C ⟶ cwf_structure_cat D. Admitted. (* TODO: perhaps show functorial in F also. *) @@ -108,7 +108,7 @@ Admitted. (** * Transfer of [rep_map]s along weak equivalences *) Definition transfer_rep_map_weak_equivalence - {C D : category} (F : C ⟶ D) + {C D : category} (F : C ⟶ D) : fully_faithful F → essentially_surjective F → equivalence_of_cats (rep_map_cat C) (rep_map_cat D). Admitted. diff --git a/TypeTheory/Auxiliary/CategoryTheoryImports.v b/TypeTheory/Auxiliary/CategoryTheoryImports.v index 3d2134c8..cc50824f 100644 --- a/TypeTheory/Auxiliary/CategoryTheoryImports.v +++ b/TypeTheory/Auxiliary/CategoryTheoryImports.v @@ -14,7 +14,7 @@ Require Export UniMath.CategoryTheory.whiskering. Require Export UniMath.CategoryTheory.Adjunctions.Core. Require Export UniMath.CategoryTheory.Equivalences.Core. Require Export UniMath.CategoryTheory.precomp_fully_faithful. -(* Require Export UniMath.CategoryTheory.rezk_completion. *) +(* Require Export UniMath.CategoryTheory.RezkCompletions.Construction. *) Require Export UniMath.CategoryTheory.yoneda. Require Export UniMath.CategoryTheory.Categories.HSET.Core. Require Export UniMath.CategoryTheory.Categories.HSET.Univalence. diff --git a/TypeTheory/CwF/CwF_def.v b/TypeTheory/CwF/CwF_def.v index b3ea634d..c3e49067 100644 --- a/TypeTheory/CwF/CwF_def.v +++ b/TypeTheory/CwF/CwF_def.v @@ -17,7 +17,7 @@ Contents: Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -28,7 +28,7 @@ Require Import TypeTheory.RelUniv.RelativeUniverses. Require Import TypeTheory.RelUniv.Transport_along_Equivs. Require Import TypeTheory.RelUniv.RelUnivYonedaCompletion. -(** * Definition of a CwF +(** * Definition of a CwF A (Fiore-style) CwF consists of: @@ -50,7 +50,7 @@ Section Fix_Category. Context {C : category}. -(** ** Representations of maps of presheaves +(** ** Representations of maps of presheaves A *representation* of a map Tm —p—> Ty of presheaves consists of data illustrating that “every fibre of _p_ is representable”; that is, giving for each (A : Ty Γ), some object and map (π A) : Γ.A Γ, along with a term (te A) over A which is “universal”, in that it represents the fiber of p over A. *) @@ -81,11 +81,11 @@ Proof. Qed. Definition cwf_fiber_representation {Γ : C} (A : Ty Γ : hSet) : UU - := ∑ (ΓAπ : map_into Γ) (te : cwf_tm_of_ty (# Ty (pr2 ΓAπ) A)), + := ∑ (ΓAπ : map_into Γ) (te : cwf_tm_of_ty (# Ty (pr2 ΓAπ) A)), isPullback (cwf_square_comm (pr2 te)). (* See below for an alternative version [cwf_fiber_representation'], separated into data + axioms *) -Definition cwf_representation : UU +Definition cwf_representation : UU := ∏ Γ (A : Ty Γ : hSet), cwf_fiber_representation A. End Representation. @@ -141,7 +141,7 @@ Definition cwf_fiber_rep_data {Γ:C} (A : Ty pp Γ : hSet) : UU := ∑ (ΓA : C), C ⟦ΓA, Γ⟧ × (Tm pp ΓA : hSet). Definition cwf_fiber_rep_ax {Γ:C} {A : Ty pp Γ : hSet} - (ΓAπt : cwf_fiber_rep_data A) : UU + (ΓAπt : cwf_fiber_rep_data A) : UU := ∑ (H : pp $nt (pr2 (pr2 ΓAπt)) = #(Ty pp) (pr1 (pr2 ΓAπt)) A), isPullback (cwf_square_comm H). @@ -149,20 +149,20 @@ Definition cwf_fiber_rep_ax {Γ:C} {A : Ty pp Γ : hSet} Definition cwf_fiber_representation' {Γ:C} (A : Ty pp Γ : hSet) : UU := ∑ ΓAπt : cwf_fiber_rep_data A, cwf_fiber_rep_ax ΓAπt. -Definition cwf_fiber_representation_weq {Γ:C} (A : Ty pp Γ : hSet) +Definition cwf_fiber_representation_weq {Γ:C} (A : Ty pp Γ : hSet) : cwf_fiber_representation pp A ≃ cwf_fiber_representation' A. Proof. unfold cwf_fiber_representation, cwf_fiber_representation'. eapply weqcomp. (* (ΓA,π), ((v,e),P) *) eapply weqfibtototal. intro x. apply weqtotal2asstor. simpl. (* (ΓA,π), (v, (e,P)) *) - eapply weqcomp; [eapply invweq; apply weqtotal2asstol |]; simpl. + eapply weqcomp; [eapply invweq; apply weqtotal2asstol |]; simpl. apply invweq. eapply weqcomp. apply weqtotal2asstor. cbn. apply weqfibtototal. intro ΓA. apply weqtotal2asstor. -Defined. +Defined. End Representation_Regrouping. @@ -175,8 +175,8 @@ Proof. intros isC. apply invproofirrelevance. intros x x'. apply subtypePath. - { intro t. - apply isofhleveltotal2. + { intro t. + apply isofhleveltotal2. - apply setproperty. - intro. apply isaprop_isPullback. } @@ -194,8 +194,8 @@ Proof. cbn. etrans. { apply yoneda_postcompose. } etrans. { - refine (toforallpaths _ (identity _)). - refine (toforallpaths _ _). + refine (toforallpaths _ (identity _)). + refine (toforallpaths _ _). apply maponpaths, (PullbackArrow_PullbackPr1 (make_Pullback _ (pr22 x))). } @@ -283,7 +283,7 @@ Lemma weq_cwf_representation_rel_universe_structure : cwf_representation pp ≃ rel_universe_structure Yo pp. Proof. apply weqonsecfibers. intro Γ. - (* convert the type argument under [yy] *) + (* convert the type argument under [yy] *) eapply weqcomp. 2: { eapply invweq. refine (weqonsecbase _ _). apply yy. @@ -294,7 +294,7 @@ Defined. End Representation_FComprehension. -Definition weq_cwf_structure_RelUnivYo +Definition weq_cwf_structure_RelUnivYo : cwf_structure C ≃ @relative_universe C _ Yo. Proof. apply weqfibtototal. @@ -337,7 +337,7 @@ Qed. Definition transfer_cwf_weak_equiv {C D : category} (F : C ⟶ D) (F_ff : fully_faithful F) (F_es : essentially_surjective F) - (Dcat : is_univalent D) + (Dcat : is_univalent D) : cwf_structure C → cwf_structure D. Proof. intro CC. @@ -351,11 +351,11 @@ Defined. Section CwF_Ftransport_recover. -Context {C D : category} +Context {C D : category} (F : C ⟶ D) - (F_ff : fully_faithful F) + (F_ff : fully_faithful F) (F_es : essentially_surjective F) - (Dcat : is_univalent D) + (Dcat : is_univalent D) (T : cwf_structure C). Let DD : univalent_category := (D,,Dcat). @@ -371,34 +371,34 @@ Let pp' : _ ⟦ TM' , TY' ⟧ := pr1 T'. Let ηη : functor (preShv D) (preShv C) := pre_composition_functor C^op D^op _ (functor_opp F). -Let isweq_Fcomp : isweq (pr1 (pr1 (Fop_precomp F))) := -adj_equiv_of_cats_is_weq_of_objects - _ _ +Let isweq_Fcomp : isweq (pr1 (pr1 (Fop_precomp F))) := +adj_equiv_of_cats_is_weq_of_objects + _ _ (is_univalent_functor_category _ _ is_univalent_HSET ) (is_univalent_functor_category _ _ is_univalent_HSET ) - _ + _ (equiv_Fcomp F F_ff F_es). -Lemma Tm_transfer_recover : +Lemma Tm_transfer_recover : TM = ηη TM'. Proof. assert (XT := homotweqinvweq (make_weq _ isweq_Fcomp) TM). apply pathsinv0. apply XT. -Defined. +Defined. -Lemma Ty_transfer_recover : +Lemma Ty_transfer_recover : TY = ηη TY'. Proof. assert (XT := homotweqinvweq (make_weq _ isweq_Fcomp) TY). apply pathsinv0. apply XT. -Defined. +Defined. Let Fopequiv : adj_equivalence_of_cats _ := equiv_Fcomp F F_ff F_es. -Definition pp'_eta : +Definition pp'_eta : preShv C ⟦ ηη TM' , ηη TY' ⟧. Proof. apply (# ηη pp'). @@ -452,7 +452,7 @@ Let pp' : _ ⟦ TM' , TY' ⟧ := pr1 T'. Let ηη : functor (preShv RC) (preShv C) := pre_composition_functor C^op RC^op _ (functor_opp (Rezk_eta C)). -Lemma Tm_Rezk_completion_recover : +Lemma Tm_Rezk_completion_recover : (* Tm = functor_composite (functor_opp (Rezk_eta C _ )) Tm'.*) TM = ηη TM'. Proof. @@ -460,9 +460,9 @@ Proof. assert (XT := homotweqinvweq XR TM). apply pathsinv0. apply XT. -Defined. +Defined. -Lemma Ty_Rezk_completion_recover : +Lemma Ty_Rezk_completion_recover : (* Ty = functor_composite (functor_opp (Rezk_eta C _ )) Ty'. *) TY = ηη TY'. Proof. @@ -470,7 +470,7 @@ Proof. assert (XT := homotweqinvweq XR TY). apply pathsinv0. apply XT. -Defined. +Defined. Let RCequiv : adj_equivalence_of_cats _ := Rezk_op_adj_equiv C @@ -481,7 +481,7 @@ Proof. apply functor_category_has_homsets. Defined. -Definition RC_pp'_eta : +Definition RC_pp'_eta : preShv C ⟦ ηη TM' , ηη TY' ⟧. Proof. apply (# ηη pp'). diff --git a/TypeTheory/CwF/RepMaps.v b/TypeTheory/CwF/RepMaps.v index c5babae8..5fb8fe4c 100644 --- a/TypeTheory/CwF/RepMaps.v +++ b/TypeTheory/CwF/RepMaps.v @@ -17,7 +17,7 @@ Contents: Require Import UniMath.Foundations.Sets. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -31,7 +31,7 @@ Require Import TypeTheory.RelUniv.Transport_along_Equivs. (** * Definition of a representable map of presheaves -A representable map of presheaves consists of +A representable map of presheaves consists of - a base category C; - a morphism Tm —p—> Ty of presheaves on C; @@ -41,10 +41,10 @@ A representable map of presheaves consists of Section Fix_Category. -(** Representations of maps of presheaves +(** Representations of maps of presheaves -A *representation* of a map Tm —p—> Ty of presheaves consists of data exhibiting, - for each (A : Ty Γ), the fiber of p over A as represented by some object Γ.A over Γ. +A *representation* of a map Tm —p—> Ty of presheaves consists of data exhibiting, + for each (A : Ty Γ), the fiber of p over A as represented by some object Γ.A over Γ. *) @@ -68,7 +68,7 @@ Proof. apply propproperty. Qed. -Definition rep_map : UU +Definition rep_map : UU := ∑ pp : mor_total (preShv C), is_representable pp. (** * Map from cwfs to representable maps of presheaves *) @@ -95,7 +95,7 @@ Defined. an equivalence if [C] is univalent. *) -Definition weq_cwf_rep_map : +Definition weq_cwf_rep_map : is_univalent C -> cwf_structure C ≃ rep_map. Proof. intro H. @@ -108,8 +108,8 @@ Proof. apply H. Defined. -(** Perhaps not obviously, the equivalence [weq_cwf_rep_map] is - pointwise definitionally equal to the map [from_cwf_to_rep_map] +(** Perhaps not obviously, the equivalence [weq_cwf_rep_map] is + pointwise definitionally equal to the map [from_cwf_to_rep_map] defined by hand. *) @@ -187,9 +187,9 @@ Defined. >>> *) -Lemma cwf_repmap_diagram (C : category) (X : cwf_structure C) +Lemma cwf_repmap_diagram (C : category) (X : cwf_structure C) : from_cwf_to_rep_map _ (Rezk_on_cwf_structures X) - = + = Rezk_on_rep_map _ (from_cwf_to_rep_map _ X). Proof. apply subtypePath. diff --git a/TypeTheory/OtherDefs/CwF_Pitts_completion.v b/TypeTheory/OtherDefs/CwF_Pitts_completion.v index 06334a7f..aa48098d 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_completion.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_completion.v @@ -9,7 +9,7 @@ Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. diff --git a/TypeTheory/RelUniv/RelUnivTransfer.v b/TypeTheory/RelUniv/RelUnivTransfer.v index bdcc967d..f91e8ed2 100644 --- a/TypeTheory/RelUniv/RelUnivTransfer.v +++ b/TypeTheory/RelUniv/RelUnivTransfer.v @@ -21,7 +21,7 @@ TODO: Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -494,7 +494,7 @@ Section RelUniv_Transfer. etrans. apply maponpaths_2, id_right. etrans. apply pathsinv0, functor_comp. apply maponpaths. - + etrans. apply assoc. etrans. apply maponpaths_2, z_iso_after_z_iso_inv. apply id_left. @@ -813,7 +813,7 @@ Section WeakRelUniv_Transfer. apply is_z_iso_from_is_iso. apply weak_relu_square_nat_trans_is_nat_iso. Defined. - + Definition weak_relu_square_commutes (C'_univ : is_univalent C') : nat_z_iso @@ -838,27 +838,27 @@ Section WeakRelUniv_Transfer. Defined. Definition reluniv_functor_with_ess_surj_issurjective_AC - (C'_univ : is_univalent C') - (AC : AxiomOfChoice.AxiomOfChoice) - (obC_isaset : isaset C) - : issurjective (reluniv_functor_with_ess_surj - _ _ _ _ J J' - R S α α_is_iso - S_pb C'_univ ff_J' S_full R_es - ). - Proof. - set (W := (weak_from_reluniv_functor J' - ,, weak_from_reluniv_functor_is_catiso J' C'_univ ff_J') - : catiso _ _). - use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)). - use (transportf (λ F, issurjective (pr11 F)) - (! weak_relu_square_commutes_identity C'_univ)). - use issurjcomp. - - apply weak_from_reluniv_functor_issurjective. - apply AC. - apply obC_isaset. - - apply issurjectiveweq. - apply (catiso_ob_weq (_,,weak_reluniv_functor_is_catiso)). + (C'_univ : is_univalent C') + (AC : AxiomOfChoice.AxiomOfChoice) + (obC_isaset : isaset C) + : issurjective (reluniv_functor_with_ess_surj + _ _ _ _ J J' + R S α α_is_iso + S_pb C'_univ ff_J' S_full R_es + ). + Proof. + set (W := (weak_from_reluniv_functor J' + ,, weak_from_reluniv_functor_is_catiso J' C'_univ ff_J') + : catiso _ _). + use (Core.issurjective_postcomp_with_weq _ (catiso_ob_weq W)). + use (transportf (λ F, issurjective (pr11 F)) + (! weak_relu_square_commutes_identity C'_univ)). + use issurjcomp. + - apply weak_from_reluniv_functor_issurjective. + apply AC. + apply obC_isaset. + - apply issurjectiveweq. + apply (catiso_ob_weq (_,,weak_reluniv_functor_is_catiso)). Defined. End WeakRelUniv_Transfer. diff --git a/TypeTheory/RelUniv/RelUnivYonedaCompletion.v b/TypeTheory/RelUniv/RelUnivYonedaCompletion.v index 20fa4069..9259134f 100644 --- a/TypeTheory/RelUniv/RelUnivYonedaCompletion.v +++ b/TypeTheory/RelUniv/RelUnivYonedaCompletion.v @@ -7,7 +7,7 @@ (** This file provides the result: given a universe in [preShv C] relative to the Yoneda embedding [ Yo : C -> preShv C ], this transfers to a similar relative universe in [ preShv (RC C) ]. i.e. on the Rezk-completion of [C]. *) Require Import UniMath.Foundations.Sets. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.rezk_completion. +Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -48,8 +48,8 @@ Proof. apply is_univalent_HSET. Defined. -Definition Rezk_on_WeakRelUnivYo : - weak_relative_universe (yoneda C) +Definition Rezk_on_WeakRelUnivYo : + weak_relative_universe (yoneda C) ≃ weak_relative_universe (yoneda RC). Proof. use (Transfer_of_WeakRelUnivYoneda (Rezk_eta C)). @@ -60,4 +60,4 @@ Defined. End fix_category. -(* *) +(* *)