From 6b939d93435e14736c7670ebf41fe4cc2d58141e Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Wed, 7 Feb 2024 13:32:39 +0100 Subject: [PATCH] Update references to category packages --- TypeTheory/Auxiliary/CategoryTheory.v | 62 ++--- TypeTheory/Auxiliary/CategoryTheoryImports.v | 6 +- TypeTheory/Auxiliary/Pullbacks.v | 12 +- TypeTheory/Auxiliary/SetsAndPresheaves.v | 36 +-- TypeTheory/Csystems/lC0systems.v | 192 +++++++------- TypeTheory/Csystems/lCsystems.v | 130 +++++----- TypeTheory/Cubical/FillFromComp.v | 8 +- TypeTheory/CwDM/CompCat_of_CwDM.v | 20 +- TypeTheory/CwDM/DispCat_of_CwDM.v | 24 +- .../CwF_SplitTypeCat_Cats_Standalone.v | 116 ++++----- .../CwF_SplitTypeCat_Univalent_Cats.v | 60 ++--- TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v | 30 +-- TypeTheory/Initiality/SyntacticCategory.v | 40 +-- TypeTheory/Instances/Presheaves.v | 10 +- TypeTheory/OtherDefs/CwF_1.v | 224 ++++++++--------- TypeTheory/OtherDefs/CwF_Dybjer.v | 4 +- TypeTheory/OtherDefs/CwF_Pitts.v | 234 +++++++++--------- TypeTheory/OtherDefs/CwF_Pitts_completion.v | 18 +- TypeTheory/OtherDefs/CwF_Pitts_natural.v | 40 +-- TypeTheory/OtherDefs/CwF_Pitts_to_CwF_1.v | 16 +- TypeTheory/OtherDefs/CwF_Pitts_to_DM.v | 8 +- TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat.v | 20 +- .../OtherDefs/CwF_Pitts_to_TypeCat_to_DM.v | 8 +- TypeTheory/OtherDefs/DM.v | 18 +- TypeTheory/OtherDefs/DM_to_TypeCat.v | 14 +- TypeTheory/OtherDefs/TypeCat_to_CwF_Pitts.v | 34 +-- TypeTheory/OtherDefs/TypeCat_to_DM.v | 12 +- TypeTheory/RelUniv/RelUniv_Cat.v | 36 +-- TypeTheory/RelUniv/RelUniv_Cat_Simple.v | 8 +- TypeTheory/TypeCat/Contextual.v | 26 +- TypeTheory/TypeCat/TypeCat.v | 50 ++-- 31 files changed, 758 insertions(+), 758 deletions(-) diff --git a/TypeTheory/Auxiliary/CategoryTheory.v b/TypeTheory/Auxiliary/CategoryTheory.v index 67ad91d6..61173c9c 100644 --- a/TypeTheory/Auxiliary/CategoryTheory.v +++ b/TypeTheory/Auxiliary/CategoryTheory.v @@ -8,9 +8,9 @@ Require Import UniMath.CategoryTheory.DisplayedCats.ComprehensionC. (* a few libraries need to be reloaded after “All”, to claim precedence on overloaded names *) -Require Import UniMath.CategoryTheory.limits.graphs.limits. -Require Import UniMath.CategoryTheory.limits.graphs.terminal. -Require Import UniMath.CategoryTheory.limits.graphs.initial. +Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. +Require Import UniMath.CategoryTheory.Limits.Graphs.Terminal. +Require Import UniMath.CategoryTheory.Limits.Graphs.Initial. Require Import TypeTheory.Auxiliary.Auxiliary. @@ -37,7 +37,7 @@ Open Scope cat. (* TODO: check more thoroughly if this is provided in the library; if so, use the library version, otherwise move this upstream. Cf. also https://github.com/UniMath/UniMath/issues/279 *) Lemma inv_from_z_iso_from_is_z_iso {D: precategory} {a b : D} (f: a --> b) (g : b --> a) (H : is_inverse_in_precat f g) -: inv_from_z_iso (f ,, (g ,, H)) +: inv_from_z_iso (f ,, (g ,, H)) = g. Proof. apply idpath. @@ -57,7 +57,7 @@ Proof. apply idpath. Defined. -Lemma forall_isotid (A : category) (a_is : is_univalent A) +Lemma forall_isotid (A : category) (a_is : is_univalent A) (a a' : A) (P : z_iso a a' -> UU) : (∏ e, P (idtoiso e)) → ∏ i, P i. Proof. @@ -66,7 +66,7 @@ Proof. apply H. Defined. -Lemma transportf_isotoid_functor +Lemma transportf_isotoid_functor (A X : category) (H : is_univalent A) (K : functor A X) (a a' : A) (p : z_iso a a') (b : X) (f : K a --> b) : @@ -89,8 +89,8 @@ Lemma idtoiso_transportf_family_of_morphisms (D : precategory) (F : ∏ a, B a -> D) (d d' : D) (deq : d = d') (R : ∏ a (b : B a), D⟦ F a b, d⟧) - -: transportf (λ x, ∏ a b, D⟦ F a b, x⟧) deq R + +: transportf (λ x, ∏ a b, D⟦ F a b, x⟧) deq R = λ a b, R a b ;; idtoiso deq. Proof. @@ -127,9 +127,9 @@ Proof. intros; induction p. apply pathsinv0, id_left. Defined. -Lemma idtoiso_postcompose_idtoiso_pre {C : precategory} {a b c : C} +Lemma idtoiso_postcompose_idtoiso_pre {C : precategory} {a b c : C} (g : a --> b) (f : a --> c) - (p : b = c) + (p : b = c) : g = f ;; idtoiso (!p) -> g ;; idtoiso p = f. Proof. induction p. simpl. @@ -199,7 +199,7 @@ Coercion nat_trans_from_nat_z_iso : nat_z_iso >-> nat_trans. (** * Properties of functors *) Definition split_ess_surj {A B : precategory} - (F : functor A B) + (F : functor A B) := ∏ b : B, ∑ a : A, z_iso (F a) b. Definition split_full {C D : precategory} (F : functor C D) : UU @@ -238,7 +238,7 @@ Qed. Definition ff_on_z_isos {C D : precategory} (F : functor C D) : UU := ∏ c c', isweq (@functor_on_z_iso _ _ F c c'). -Lemma fully_faithful_impl_ff_on_isos {C D : category} (F : functor C D) +Lemma fully_faithful_impl_ff_on_isos {C D : category} (F : functor C D) : fully_faithful F -> ff_on_z_isos F. Proof. intros Fff c c'. @@ -357,13 +357,13 @@ Qed. Definition G_ff_split : functor _ _ := ( _ ,, G_ff_split_ax). -Definition is_nat_trans_ε_ff_split : +Definition is_nat_trans_ε_ff_split : is_nat_trans (functor_composite_data G_ff_split_data F) (functor_identity_data B) (λ b : B, pr2 (Fses b)). Proof. intros b b' g; etrans; [ apply maponpaths_2 ; use homotweqinvweq |]; - repeat rewrite <- assoc; + repeat rewrite <- assoc; apply maponpaths; rewrite z_iso_after_z_iso_inv; apply id_right. @@ -378,7 +378,7 @@ Proof. - apply is_nat_trans_ε_ff_split. Defined. -Lemma is_nat_trans_η_ff_split : +Lemma is_nat_trans_η_ff_split : is_nat_trans (functor_identity_data A) (functor_composite_data F G_ff_split_data) (λ a : A, Finv (inv_from_z_iso (pr2 (Fses (F ((functor_identity A) a)))))). @@ -406,18 +406,18 @@ Proof. - intro a. apply Finv. apply (inv_from_z_iso (pr2 (Fses _ ))). - - apply is_nat_trans_η_ff_split. + - apply is_nat_trans_η_ff_split. Defined. - -Lemma form_adjunction_ff_split + +Lemma form_adjunction_ff_split : form_adjunction F G_ff_split η_ff_split ε_ff_split. simpl. split. * intro a. - cbn. - etrans. apply maponpaths_2. use homotweqinvweq. + cbn. + etrans. apply maponpaths_2. use homotweqinvweq. apply z_iso_after_z_iso_inv. * intro b. - cbn. + cbn. apply (invmaponpathsweq (make_weq _ (Fff _ _ ))). cbn. rewrite functor_comp. @@ -435,13 +435,13 @@ Proof. use tpair. - exists G_ff_split. use tpair. - + exists η_ff_split. - exact ε_ff_split. - + apply form_adjunction_ff_split. + + exists η_ff_split. + exact ε_ff_split. + + apply form_adjunction_ff_split. - split; cbn. - + intro a. + + intro a. use (fully_faithful_reflects_iso_proof _ _ _ Fff _ _ (make_z_iso' _ _ )). - apply is_z_iso_inv_from_z_iso. + apply is_z_iso_inv_from_z_iso. + intro b. apply pr2. Defined. @@ -498,7 +498,7 @@ Defined. Lemma inv_from_z_iso_z_iso_from_fully_faithful_reflection {C D : precategory} (F : functor C D) (HF : fully_faithful F) (a b : C) (i : z_iso (F a) (F b)) : inv_from_z_iso - (iso_from_fully_faithful_reflection HF i) = + (iso_from_fully_faithful_reflection HF i) = iso_from_fully_faithful_reflection HF (z_iso_inv_from_z_iso i). Proof. apply idpath. @@ -520,7 +520,7 @@ Defined. Lemma z_iso_from_z_iso_with_postcomp (D E E' : category) (F G : functor D E) (H : functor E E') - (Hff : fully_faithful H) : + (Hff : fully_faithful H) : z_iso (C:=[D, E']) (functor_composite F H) (functor_composite G H) -> z_iso (C:=[D, E]) F G. @@ -610,7 +610,7 @@ End Limits. (** * Sections of maps *) -(* TODO: currently, sections are independently developed in many places in [TypeTheory]. Try to unify the treatments of them here? Also unify with ad hoc material on sections in [UniMath.CategoryTheory.limits.pullbacks]: [pb_of_section], [section_from_diagonal], etc.*) +(* TODO: currently, sections are independently developed in many places in [TypeTheory]. Try to unify the treatments of them here? Also unify with ad hoc material on sections in [UniMath.CategoryTheory.Limits.Pullbacks]: [pb_of_section], [section_from_diagonal], etc.*) Section Sections. Definition section {C : precategory} {X Y : C} (f : X --> Y) @@ -657,7 +657,7 @@ Coercion structure_of_comprehension_cat (C : comprehension_cat) := pr2 C. (** * Unorganised lemmas *) -(* Lemmas that probably belong in one of the sections above, but haven’t been sorted into them yet. Mainly a temporary holding pen for lemmas being upstreamed from other files. TODO: empty this bin frequently (but keep it here for re-use). *) +(* Lemmas that probably belong in one of the sections above, but haven’t been sorted into them yet. Mainly a temporary holding pen for lemmas being upstreamed from other files. TODO: empty this bin frequently (but keep it here for re-use). *) Section Unorganised. End Unorganised. @@ -677,7 +677,7 @@ End Unorganised. - [adj_equivalence_of_cats] changes to either [is_adj_equiv] or [adj_equiv_structure] - (possible also [_of_cats], but this seems reasonably implicit since it’s on a functor) + (possible also [_of_cats], but this seems reasonably implicit since it’s on a functor) - [equivalence_of_cats] changes to [adj_equiv_of_cats] - lemmas about them are renamed as consistently as possible, following these. diff --git a/TypeTheory/Auxiliary/CategoryTheoryImports.v b/TypeTheory/Auxiliary/CategoryTheoryImports.v index 85cd3897..3d2134c8 100644 --- a/TypeTheory/Auxiliary/CategoryTheoryImports.v +++ b/TypeTheory/Auxiliary/CategoryTheoryImports.v @@ -6,7 +6,7 @@ (** A wrapper, re-exporting the modules from [UniMath] that we frequently use, to reduce clutter in imports. *) -Require Export UniMath.CategoryTheory.limits.pullbacks. +Require Export UniMath.CategoryTheory.Limits.Pullbacks. Require Export UniMath.Foundations.Propositions. Require Export UniMath.CategoryTheory.Core.Prelude. Require Export UniMath.CategoryTheory.opp_precat. @@ -16,8 +16,8 @@ Require Export UniMath.CategoryTheory.Equivalences.Core. Require Export UniMath.CategoryTheory.precomp_fully_faithful. (* Require Export UniMath.CategoryTheory.rezk_completion. *) Require Export UniMath.CategoryTheory.yoneda. -Require Export UniMath.CategoryTheory.categories.HSET.Core. -Require Export UniMath.CategoryTheory.categories.HSET.Univalence. +Require Export UniMath.CategoryTheory.Categories.HSET.Core. +Require Export UniMath.CategoryTheory.Categories.HSET.Univalence. Require Export UniMath.CategoryTheory.Presheaf. Require Export UniMath.CategoryTheory.catiso. Require Export UniMath.CategoryTheory.ArrowCategory. diff --git a/TypeTheory/Auxiliary/Pullbacks.v b/TypeTheory/Auxiliary/Pullbacks.v index 44bc3d8f..8e76b862 100644 --- a/TypeTheory/Auxiliary/Pullbacks.v +++ b/TypeTheory/Auxiliary/Pullbacks.v @@ -4,7 +4,7 @@ Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. (* a few libraries need to be reloaded after “All”, to claim precedence on overloaded names *) -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -175,7 +175,7 @@ Lemma isPullback_transfer_z_iso {C : category} -> isPullback H'. Proof. intros Hpb. - apply (make_isPullback _ ). + apply (make_isPullback _ ). intros X h k H''. simple refine (tpair _ _ _ ). - simple refine (tpair _ _ _ ). @@ -299,7 +299,7 @@ Proof. simpl in *. destruct Cone as [p [h k]]; destruct Cone' as [p' [h' k']]; - simpl in *. + simpl in *. unfold from_Pullback_to_Pullback; rewrite PullbackArrow_PullbackPr2, PullbackArrow_PullbackPr1. apply idpath. @@ -315,14 +315,14 @@ Section Pullback_Unique_Up_To_Iso. g | | k | | c----d - j + j and pb square a' b' c d, and h iso - + task: construct iso from a to a' *) - + Variable CC : category. Variables A B C D A' B' : CC. Variables (f : A --> B) (g : A --> C) (k : B --> D) (j : C --> D) diff --git a/TypeTheory/Auxiliary/SetsAndPresheaves.v b/TypeTheory/Auxiliary/SetsAndPresheaves.v index 7fedfd6c..9749ca7b 100644 --- a/TypeTheory/Auxiliary/SetsAndPresheaves.v +++ b/TypeTheory/Auxiliary/SetsAndPresheaves.v @@ -5,11 +5,11 @@ Require Import UniMath.Combinatorics.StandardFiniteSets. (* a few libraries need to be reloaded after “All”, to claim precedence on overloaded names *) -Require Import UniMath.CategoryTheory.limits.graphs.limits. -Require Import UniMath.CategoryTheory.limits.graphs.pullbacks. -Require Import UniMath.CategoryTheory.limits.pullbacks. -Require Import UniMath.CategoryTheory.categories.HSET.Limits. -Require Import UniMath.CategoryTheory.categories.HSET.Univalence. +Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. +Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. +Require Import UniMath.CategoryTheory.Categories.HSET.Limits. +Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -23,13 +23,13 @@ Arguments nat_trans_comp {_ _ _ _ _} _ _. Definition preShv C := functor_univalent_category C^op HSET_univalent_category. (* Note: just like notation "PreShv" upstream, but univalent. TODO: unify these? *) -(* Notations for working with presheaves and natural transformations given as objects of [preShv C], since applying them directly requires type-casts before the coercions to [Funclass] trigger. *) +(* Notations for working with presheaves and natural transformations given as objects of [preShv C], since applying them directly requires type-casts before the coercions to [Funclass] trigger. *) Notation "#p F" := (functor_on_morphisms (F : functor _ _)) (at level 3) : cat. -Notation "P $p c" +Notation "P $p c" := (((P : preShv _) : functor _ _) c : hSet) (at level 65) : cat. -Notation "α $nt x" +Notation "α $nt x" := (((α : preShv _ ⟦_ , _ ⟧) : nat_trans _ _) _ x) (at level 65) : cat. (* The combinations of type-casts here are chosen as they’re what seems to work for as many given types as possible *) @@ -111,8 +111,8 @@ Proof. apply yoneda_weq. Defined. -Lemma yy_natural {C : category} - (F : preShv C) (c : C) (A : F $p c) +Lemma yy_natural {C : category} + (F : preShv C) (c : C) (A : F $p c) (c' : C) (f : C⟦c', c⟧) : (@yy C F c') (#p F f A) = # (yoneda C) f · (@yy C F c) A. Proof. @@ -127,7 +127,7 @@ Lemma yy_comp_nat_trans {C : category} Proof. apply nat_trans_eq. - apply homset_property. - - intro c. simpl. + - intro c. simpl. apply funextsec. intro f. cbn. apply nat_trans_ax_pshf. Qed. @@ -177,12 +177,12 @@ Proof. refine (H_uniqueness (h x) (k x) _ (_,,_) (_,,_)); try split; revert x; apply toforallpaths; assumption. - - use tpair. + - use tpair. + intros x. refine (pr1 (H_existence (h x) (k x) _)). apply (toforallpaths ehk). + simpl. split; apply funextsec; intro x. - * apply (pr1 (pr2 (H_existence _ _ _))). + * apply (pr1 (pr2 (H_existence _ _ _))). * apply (pr2 (pr2 (H_existence _ _ _))). Qed. @@ -225,7 +225,7 @@ Lemma pullback_HSET_elements_unique {P A B C : HSET} (e1 : p1 ab = p1 ab') (e2 : p2 ab = p2 ab') : ab = ab'. Proof. - set (temp := proofirrelevancecontr + set (temp := proofirrelevancecontr (pullback_HSET_univprop_elements _ pb (p1 ab') (p2 ab') (toforallpaths ep ab'))). refine (maponpaths pr1 (temp (ab,, _) (ab',, _))). @@ -262,23 +262,23 @@ Proof. transparent assert (XH : (∏ a : C^op, LimCone - (@colimits.diagram_pointwise C^op HSET + (@Colimits.diagram_pointwise C^op HSET pullback_graph XT1 a))). { intro. apply LimConeHSET. } specialize (XR XH). - specialize (XR W). + specialize (XR W). set (XT := PullbCone _ _ _ _ p1 p2 e). specialize (XR XT). transparent assert (XTT : (isLimCone XT1 W XT)). { apply @equiv_isPullback_1. exact pb. } - specialize (XR XTT c). + specialize (XR XTT c). intros S h k H. specialize (XR S). simpl in XR. transparent assert (HC - : (cone (@colimits.diagram_pointwise C^op HSET + : (cone (@Colimits.diagram_pointwise C^op HSET pullback_graph (pullback_diagram (preShv C) f g) c) S)). { use make_cone. apply three_rec_dep; cbn. diff --git a/TypeTheory/Csystems/lC0systems.v b/TypeTheory/Csystems/lC0systems.v index 3437b44a..6f9c68d9 100644 --- a/TypeTheory/Csystems/lC0systems.v +++ b/TypeTheory/Csystems/lC0systems.v @@ -1,6 +1,6 @@ -(** ** lC0-systems +(** ** lC0-systems -by Vladimir Voevodsky, started Dec. 4, 2014, continued Jan. 22, 2015, Feb. 11, 2015 +by Vladimir Voevodsky, started Dec. 4, 2014, continued Jan. 22, 2015, Feb. 11, 2015 We refer below to the paper "Subsystems and regular quotients of C-systems" by V. Voevodsky as "Csubsystems". @@ -14,8 +14,8 @@ Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import TypeTheory.Auxiliary.Auxiliary. -Require Import TypeTheory.Auxiliary.CategoryTheory. -Require Import UniMath.CategoryTheory.limits.terminal. +Require Import TypeTheory.Auxiliary.CategoryTheory. +Require Import UniMath.CategoryTheory.Limits.Terminal. Require Export TypeTheory.Csystems.hSet_ltowers. @@ -279,19 +279,19 @@ Definition mor_from { C : precategory_ob_mor } ( X : C ) := ∑ A : C, X --> A. (* compare with UniMath.CategoryTheory.coslicecat.coslicecat_ob *) Definition mor_from_pr2 { C : precategory_ob_mor } ( X : C ): - forall f : mor_from X, precategory_morphisms X ( pr1 f ) := pr2. + forall f : mor_from X, precategory_morphisms X ( pr1 f ) := pr2. Coercion mor_from_pr2 : mor_from >-> precategory_morphisms. (* compare with UniMath.CategoryTheory.coslicecat.coslicecat_ob_morphism *) Definition mor_from_constr { C : precategory_ob_mor } { X A : C } ( f : X --> A ): - mor_from X := tpair _ _ f. + mor_from X := tpair _ _ f. Definition mor_to { C : precategory_ob_mor } ( X : C ) := ∑ A : C, A --> X. (* compare with UniMath.CategoryTheory.slicecat.slicecat_ob *) Definition mor_to_pr2 { C : precategory_ob_mor } ( X : C ) - : ∏ f : mor_to X , precategory_morphisms ( pr1 f ) X := pr2. + : ∏ f : mor_to X , precategory_morphisms ( pr1 f ) X := pr2. Coercion mor_to_pr2 : mor_to >-> precategory_morphisms. (* compare with UniMath.CategoryTheory.slicecat.slicecat_ob_morphism *) @@ -335,7 +335,7 @@ Qed. (* Definition isaset_ob ( C : setcategory ): isaset C := pr1 ( pr2 C ). -Definition isaset_mor ( C : setcategory ): has_homsets C := pr2 ( pr2 C ). +Definition isaset_mor ( C : setcategory ): has_homsets C := pr2 ( pr2 C ). *) @@ -343,7 +343,7 @@ Definition isaset_mor ( C : setcategory ): has_homsets C := pr2 ( pr2 C ). The following sequence of definitions is a formalization of Definition 2.1 in Csubsystems *) -(** **** The carrier of an lC0-system +(** **** The carrier of an lC0-system as a set precategory whose objects form a pointed hSet-ltower with the additional structure of the canonical projections pX : X --> ft X . *) @@ -354,7 +354,7 @@ the canonical projections pX : X --> ft X . *) Definition ltower_precat : UU - := ∑ C : setcategory, ltower_str C. + := ∑ C : setcategory, ltower_str C. Definition ltower_precat_to_ltower ( CC : ltower_precat ) : hSet_ltower @@ -371,9 +371,9 @@ Coercion ltower_precat_pr1 Definition ltower_precat_and_p : UU := ∑ CC : ltower_precat, ∏ X : CC, X --> ft X. -Definition ltower_precat_and_p_pr1: ltower_precat_and_p -> ltower_precat := pr1. -Coercion ltower_precat_and_p_pr1: ltower_precat_and_p >-> ltower_precat. - +Definition ltower_precat_and_p_pr1: ltower_precat_and_p -> ltower_precat := pr1. +Coercion ltower_precat_and_p_pr1: ltower_precat_and_p >-> ltower_precat. + Definition pX { CC : ltower_precat_and_p } ( X : CC ): X --> ft X := pr2 CC X. @@ -382,12 +382,12 @@ Definition pX { CC : ltower_precat_and_p } ( X : CC ): X --> ft X := pr2 CC X. (** **** Some constructions *) Definition pnX { CC : ltower_precat_and_p } ( n : nat ) ( X : CC ) - : X --> ftn n X. + : X --> ftn n X. Proof. induction n as [ | n IHn ]. - - exact ( identity X ). + - exact ( identity X ). - destruct n as [ | n ]. - + exact ( pX X ). + + exact ( pX X ). + exact ( IHn · pX ( ftn ( S n ) X ) ). Defined. @@ -403,7 +403,7 @@ Coercion sec_pnX_to_mor { CC : ltower_precat_and_p } ( n : nat ) ( X : CC ) Definition sec_pnX_eq { CC : ltower_precat_and_p } { n : nat } { X : CC } ( s : sec_pnX n X ) : s · pnX n X = identity ( ftn n X ) := pr2 s. - + Notation sec_pX := (sec_pnX 1). Notation sec_pX_eq := (@sec_pnX_eq _ 1 _ ). @@ -506,7 +506,7 @@ Qed. Definition Ob_tilde_over_to_mor_to { CC : ltower_precat_and_p } ( X : CC ) ( r : Ob_tilde_over X ): mor_to X := mor_to_constr ( pr1 r ). -Coercion Ob_tilde_over_to_mor_to: Ob_tilde_over >-> mor_to. +Coercion Ob_tilde_over_to_mor_to: Ob_tilde_over >-> mor_to. Definition Ob_tilde_over_to_mor_from { CC : ltower_precat_and_p } ( X : CC ) ( r : Ob_tilde_over X ): @@ -531,16 +531,16 @@ Coercion pltower_precat_and_p_pr1 : pltower_precat_and_p >-> ltower_precat_and_p. Definition pltower_precat_and_p_to_pltower: pltower_precat_and_p -> pltower := - fun X => pltower_constr ( pr2 X ). + fun X => pltower_constr ( pr2 X ). Coercion pltower_precat_and_p_to_pltower: pltower_precat_and_p >-> pltower. (** **** l-C0-system data *) -Definition q_data_type ( CC : ltower_precat_and_p ) := - forall ( X Y : CC ) ( gt0 : ll X > 0 ) ( f : Y --> ft X ), mor_to X. -Identity Coercion from_q_data_type: q_data_type >-> Funclass. +Definition q_data_type ( CC : ltower_precat_and_p ) := + forall ( X Y : CC ) ( gt0 : ll X > 0 ) ( f : Y --> ft X ), mor_to X. +Identity Coercion from_q_data_type: q_data_type >-> Funclass. Definition lC0system_data := ∑ CC : pltower_precat_and_p, q_data_type CC. @@ -558,10 +558,10 @@ Definition dom { CC : lC0system_data } { X : CC } := pr1 f. -Definition q_of_f { CC : lC0system_data } +Definition q_of_f { CC : lC0system_data } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> ft X ) : mor_to X - := pr2 CC _ _ gt0 f . + := pr2 CC _ _ gt0 f . Definition f_star { CC : lC0system_data } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> ft X ) @@ -582,9 +582,9 @@ Definition mor_to_star { CC : lC0system_data } { X : CC } ( gt0 : ll X > 0 ) -(** **** Properties on l-C0-system data +(** **** Properties on l-C0-system data -that later become axioms of an lC0-system. The numbering of the conditions below is according to +that later become axioms of an lC0-system. The numbering of the conditions below is according to the Csubsystems paper. The conditions 1-3 are consequences of the definition of a pointed l-tower (pltower) *) @@ -617,7 +617,7 @@ Definition C0ax5b_z_iso_inv { CC : lC0system_data } ( ax5b : C0ax5b_type CC ) (** The description of properties continues *) Definition C0ax5c_type { CC : lC0system_data } ( ax5b : C0ax5b_type CC ) - := ∏ ( X Y : CC ) ( gt0 : ll X > 0 ) ( f : Y --> ft X ), + := ∏ ( X Y : CC ) ( gt0 : ll X > 0 ) ( f : Y --> ft X ), pX ( f_star gt0 f ) · ( ( C0ax5b_z_iso ax5b gt0 f ) · f ) = ( q_of_f gt0 f ) · ( pX X ). @@ -625,7 +625,7 @@ Definition C0ax6_type ( CC : lC0system_data ) := ∏ ( X : CC ) ( gt0 : ll X > 0 ), q_of_f gt0 ( identity ( ft X ) ) = mor_to_constr (identity X). -Definition C0ax7_type { CC : lC0system_data } +Definition C0ax7_type { CC : lC0system_data } ( ax5a : C0ax5a_type CC ) ( ax5b : C0ax5b_type CC ) := ∏ ( X Y Z : CC ) ( gt0 : ll X > 0 ) ( f : Y --> ft X ) ( g : Z --> ft(f_star gt0 f) ), mor_to_constr ( ( q_of_f ( ax5a _ _ gt0 f ) g ) · ( q_of_f gt0 f ) ) = @@ -640,7 +640,7 @@ Definition lC0system := ∑ CC : lC0system_data, ( C0ax4_type CC ) × ( ∑ axs : ( C0ax5a_type CC ) × - ( ∑ ax5b : C0ax5b_type CC, C0ax5c_type ax5b ), + ( ∑ ax5b : C0ax5b_type CC, C0ax5c_type ax5b ), ( C0ax6_type CC ) × ( C0ax7_type ( pr1 axs ) ( pr1 ( pr2 axs ) ) ) ). @@ -651,7 +651,7 @@ Coercion lC0system_pr1: lC0system >-> lC0system_data. Definition C0_has_homsets ( CC : lC0system ) : has_homsets CC := pr2 ( pr1 ( pr2 CC ) ) . *) -Definition C0ax4 ( CC : lC0system ): C0ax4_type CC := pr1 ( pr2 CC ). +Definition C0ax4 ( CC : lC0system ): C0ax4_type CC := pr1 ( pr2 CC ). Definition C0ax5a { CC : lC0system } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> ft X ) : ll ( f_star gt0 f ) > 0 @@ -661,7 +661,7 @@ Definition C0ax5b { CC : lC0system } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> : ft ( f_star gt0 f ) = Y := pr1 ( pr2 ( pr1 ( pr2 ( pr2 CC )))) X Y gt0 f. -Notation ft_f_star := C0ax5b. +Notation ft_f_star := C0ax5b. Definition C0eiso { CC : lC0system } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> ft X ) : z_iso (ft(f_star gt0 f)) Y @@ -677,7 +677,7 @@ Definition C0ax5c { CC : lC0system } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> ft X ) : pX ( f_star gt0 f ) · ( ( C0eiso gt0 f ) · f ) = ( q_of_f gt0 f ) · ( pX X ) - := pr2 ( pr2 ( pr1 ( pr2 ( pr2 CC )))) X Y gt0 f. + := pr2 ( pr2 ( pr1 ( pr2 ( pr2 CC )))) X Y gt0 f. Definition C0ax6 { CC : lC0system } { X : CC } ( gt0 : ll X > 0 ) @@ -706,7 +706,7 @@ Lemma ll_f_star { CC : lC0system } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y --> f Proof. assert ( gt0': ll ( f_star gt0 f ) > 0 ) by apply C0ax5a. etrans. { apply pathsinv0. apply ( S_ll_ft gt0' ). } - do 2 apply maponpaths. apply C0ax5b. + do 2 apply maponpaths. apply C0ax5b. Defined. @@ -714,16 +714,16 @@ Lemma isover_f_star { CC : lC0system } { X Y : CC } ( gt0 : ll X > 0 ) ( f : Y - : isover ( f_star gt0 f ) Y. Proof. set ( eq := C0ax5b gt0 f ). - unfold isover. + unfold isover. assert ( eq1 : ll ( f_star gt0 f ) - ll Y = 1 ). { etrans. { apply maponpaths_2. apply ll_f_star. } apply plusminusnmm. } apply pathsinv0. etrans. { apply maponpaths_2. apply eq1. } - exact eq. + exact eq. Defined. - + (** *** Operations qn, fn_star and f_star_of_s and fn_star_of_s *) @@ -738,23 +738,23 @@ Definition qn { CC : lC0system_data } { A X : CC } ( fun X => idfun _ ) ( fun X gt0 => q_of_mor_to gt0 ) ( fun X Y f g => funcomp g f ) - X A isov f. + X A isov f. -(* Definition qn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) +(* Definition qn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) : mor_to X . Proof. - intros until n . + intros until n . induction n as [ | n IHn ] . - intros . - change _ with ( X = A ) in eq . - apply ( mor_to_constr ( f ;; id_to_mor ( ! eq ) ) ) . + intros . + change _ with ( X = A ) in eq . + apply ( mor_to_constr ( f ;; id_to_mor ( ! eq ) ) ) . intros . set ( int := ftn_ft n X : ftn n ( ft X ) = ftn ( 1 + n ) X ) . - set ( gt0 := natgehgthtrans _ _ _ gtn ( natgthsn0 _ ) ) . - apply ( q_of_f gt0 ( IHn ( ft X ) ( ll_ft_gtn gtn ) ( int @ eq ) ) ) . + set ( gt0 := natgehgthtrans _ _ _ gtn ( natgthsn0 _ ) ) . + apply ( q_of_f gt0 ( IHn ( ft X ) ( ll_ft_gtn gtn ) ( int @ eq ) ) ) . Defined. *) @@ -771,22 +771,22 @@ Definition fn_star { CC : lC0system_data } { X A : CC } (* Lemma qn_equals_qn { CC : lC0system_data } ( is : isaset CC ) { Y A : CC } ( f : Y --> A ) - { n1 n2 : nat } ( eqn : n1 = n2 ) + { n1 n2 : nat } ( eqn : n1 = n2 ) { X : CC } ( gtn1 : ll X >= n1 ) ( gtn2 : ll X >= n2 ) ( eq1 : ftn n1 X = A ) ( eq2 : ftn n2 X = A ) : qn f n1 gtn1 eq1 = qn f n2 gtn2 eq2 . Proof. - intros until n2 . - intro eqn . + intros until n2 . + intro eqn . rewrite eqn . - intros until gtn2 . - assert ( eq : gtn1 = gtn2 ) . apply ( proofirrelevance _ ( pr2 ( _ >= _ ) ) ) . - rewrite eq . - intros eq1 eq2 . + intros until gtn2 . + assert ( eq : gtn1 = gtn2 ) . apply ( proofirrelevance _ ( pr2 ( _ >= _ ) ) ) . + rewrite eq . + intros eq1 eq2 . assert ( eq' : eq1 = eq2 ) . - apply is . - rewrite eq' . + apply is . + rewrite eq' . apply idpath . Defined. *) @@ -807,7 +807,7 @@ Opaque q_XX. Lemma q_isab { CC : lC0system_data } { X A : CC } ( f : mor_to A ) ( isab : isabove X A ) - : qn f isab = q_of_mor_to ( isabove_gt0 isab ) ( qn f ( isover_ft' isab ) ). + : qn f isab = q_of_mor_to ( isabove_gt0 isab ) ( qn f ( isover_ft' isab ) ). Proof. set ( int := isover_ind_isab ( fun X Y : CC => mor_to Y -> mor_to X ) ( fun X => idfun _ ) @@ -822,14 +822,14 @@ Opaque q_isab. Lemma q_X_ftX { CC : lC0system_data } { X : CC } ( f : mor_to ( ft X ) ) ( gt0 : ll X > 0 ) : qn f ( isover_X_ftX X ) = q_of_mor_to gt0 f. Proof. - unfold qn. + unfold qn. apply ( maponpaths ( fun g => g f ) ). use isover_ind_X_ftX. - intros X0 gt1. - apply idpath. + intros X0 gt1. + apply idpath. Defined. -Opaque q_X_ftX. +Opaque q_X_ftX. @@ -837,17 +837,17 @@ Lemma f_star_XX { CC : lC0system_data } { X : CC } ( f : mor_to X ) ( isov : iso : fn_star f isov = dom f. Proof. apply ( maponpaths dom ). - apply q_XX. + apply q_XX. Defined. Opaque f_star_XX. -Lemma f_star_isab { CC : lC0system_data } { X A : CC } +Lemma f_star_isab { CC : lC0system_data } { X A : CC } ( f : mor_to A ) ( isab : isabove X A ) - : fn_star f isab = f_star ( isabove_gt0 isab ) ( qn f ( isover_ft' isab ) ). + : fn_star f isab = f_star ( isabove_gt0 isab ) ( qn f ( isover_ft' isab ) ). Proof. apply ( maponpaths dom ). - apply q_isab. + apply q_isab. Defined. Opaque f_star_isab. @@ -856,13 +856,13 @@ Opaque f_star_isab. Lemma f_star_X_ftX { CC : lC0system_data } { X : CC } ( f : mor_to ( ft X ) ) ( gt0 : ll X > 0 ) : fn_star f ( isover_X_ftX X ) = f_star gt0 f. Proof. - apply ( maponpaths dom ). + apply ( maponpaths dom ). apply q_X_ftX. Defined. -(* Definition qsn_strict { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) +(* Definition qsn_strict { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtsn : ll X >= S n ) ( eq : ftn (S n) X = A ) : qn f ( S n ) gtsn eq = q_of_f (natgehgthtrans _ _ _ gtsn ( natgthsn0 _ )) @@ -873,7 +873,7 @@ Definition qsn_new_eq { T : ltower } { A X : T } { n m : nat } ( eq : ftn n X = A ) ( eqnat : n = S m ) : ftn ( S m ) X = A . Proof . intros . - apply ( ( maponpaths ( fun i => ftn i X ) ( ! eqnat ) ) @ eq ) . + apply ( ( maponpaths ( fun i => ftn i X ) ( ! eqnat ) ) @ eq ) . Defined. @@ -887,7 +887,7 @@ Proof. Defined. -Lemma qn_to_qsm { CC : lC0system } { Y A : CC } ( f : Y --> A ) { n : nat } +Lemma qn_to_qsm { CC : lC0system } { Y A : CC } ( f : Y --> A ) { n : nat } { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) { m : nat } ( eqnat : n = S m ) : qn f n gtn eq = @@ -895,7 +895,7 @@ Lemma qn_to_qsm { CC : lC0system } { Y A : CC } ( f : Y --> A ) { n : nat } Proof. intros . apply qn_equals_qn . - + apply C0_isaset_Ob . apply eqnat . @@ -904,7 +904,7 @@ Defined. -Definition fsn_strict { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Definition fsn_strict { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtsn : ll X >= S n ) ( eq : ftn ( S n ) X = A ) : fn_star f ( S n ) gtsn eq = f_star (natgehgthtrans _ _ _ gtsn ( natgthsn0 _ )) @@ -912,18 +912,18 @@ Definition fsn_strict { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : idpath _ . -Definition fn_star_to_fsm_star { CC : lC0system } { Y A : CC } ( f : Y --> A ) { n : nat } +Definition fn_star_to_fsm_star { CC : lC0system } { Y A : CC } ( f : Y --> A ) { n : nat } { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) { m : nat } ( eqnat : n = S m ) : fn_star f n gtn eq = fn_star f ( S m ) ( qsn_new_gtn gtn eqnat ) ( qsn_new_eq eq eqnat ) := - maponpaths pr1 ( qn_to_qsm _ _ _ _ ) . + maponpaths pr1 ( qn_to_qsm _ _ _ _ ) . *) Lemma ll_fn_star { CC : lC0system } { A X : CC } ( f : mor_to A ) ( isov : isover X A ) - : ll ( fn_star f isov ) + ll A = ll ( dom f ) + ll X. + : ll ( fn_star f isov ) + ll A = ll ( dom f ) + ll X. Proof. set ( P := fun ( X0 Y0 : CC ) ( isov0 : isover X0 Y0 ) => forall ( f0 : mor_to Y0 ), ll ( fn_star f0 isov0 ) + ll Y0 = ll ( dom f0 ) + ll X0 ). @@ -931,47 +931,47 @@ Proof. { intro. unfold P. intro. - apply maponpaths_2. apply maponpaths. apply f_star_XX. + apply maponpaths_2. apply maponpaths. apply f_star_XX. } - assert ( Pft : forall X0 ( gt0 : ll X0 > 0 ), P X0 ( ft X0 ) ( isover_X_ftX X0 ) ). + assert ( Pft : forall X0 ( gt0 : ll X0 > 0 ), P X0 ( ft X0 ) ( isover_X_ftX X0 ) ). { intros. unfold P. intro f0. etrans. { apply maponpaths_2. etrans. { apply maponpaths. apply ( f_star_X_ftX f0 gt0 ). } etrans. { apply ( ll_f_star gt0 f0 ). } - apply ( natpluscomm 1 _ ). + apply ( natpluscomm 1 _ ). } etrans. apply natplusassoc. apply ( maponpaths ( fun x => ll (dom f0) + x ) ). - apply S_ll_ft. + apply S_ll_ft. apply gt0. } assert ( Pcomp : forall ( X Y : CC ), ( forall isov1, P X ( ft X ) isov1 ) -> ( forall isov2, P ( ft X ) Y isov2 ) -> - forall ( isab : isabove X Y ), P X Y isab ). - { intros X0 Y0 F0 G0 isab. - unfold P. + forall ( isab : isabove X Y ), P X Y isab ). + { intros X0 Y0 F0 G0 isab. + unfold P. intro f0. etrans. { apply maponpaths_2. etrans. { apply maponpaths, f_star_isab. } apply ll_f_star. } assert ( eq := G0 (isover_ft' isab) ). { unfold P in eq. - change (pr1 (qn f0 (isover_ft' isab))) with ( fn_star f0 (isover_ft' isab) ). + change (pr1 (qn f0 (isover_ft' isab))) with ( fn_star f0 (isover_ft' isab) ). rewrite natplusassoc. - rewrite ( eq f0 ). + rewrite ( eq f0 ). rewrite ( natpluscomm ( ll ( dom f0 ) ) ). rewrite <- natplusassoc. - rewrite S_ll_ft. - - apply natpluscomm. - - apply ( isabove_gt0 isab ). + rewrite S_ll_ft. + - apply natpluscomm. + - apply ( isabove_gt0 isab ). } } - apply ( isover_strong_ind_int P P0 Pft Pcomp _ _ _ isov _ ). + apply ( isover_strong_ind_int P P0 Pft Pcomp _ _ _ isov _ ). Defined. - + Lemma isover_fn_star { CC : lC0system } { X A : CC } ( f : mor_to A ) ( isov : isover X A ): isover ( fn_star f isov ) ( dom f ). @@ -981,31 +981,31 @@ Proof. assert ( P0 : forall X0 , P X0 X0 ( isover_XX X0 ) ). { intro. unfold P. - intro. + intro. rewrite f_star_XX. apply isover_XX. } - assert ( Pft : forall X0 ( gt0 : ll X0 > 0 ) , P X0 ( ft X0 ) ( isover_X_ftX X0 ) ). + assert ( Pft : forall X0 ( gt0 : ll X0 > 0 ) , P X0 ( ft X0 ) ( isover_X_ftX X0 ) ). { intros. unfold P. intro f0. rewrite ( f_star_X_ftX f0 gt0 ). - apply isover_f_star. - } + apply isover_f_star. + } assert ( Pcomp : forall ( X Y : CC ), ( forall isov1, P X ( ft X ) isov1 ) -> ( forall isov2, P ( ft X ) Y isov2 ) -> - forall ( isab : isabove X Y ), P X Y isab ). - { intros X0 Y0 F0 G0 isab. - unfold P. - intro f0. + forall ( isab : isabove X Y ), P X Y isab ). + { intros X0 Y0 F0 G0 isab. + unfold P. + intro f0. rewrite f_star_isab. use isover_trans. - - apply ( dom (qn f0 (isover_ft' isab)) ). + - apply ( dom (qn f0 (isover_ft' isab)) ). - apply isover_f_star. - - apply G0. + - apply G0. } - apply ( isover_strong_ind_int P P0 Pft Pcomp _ _ _ isov _ ). + apply ( isover_strong_ind_int P P0 Pft Pcomp _ _ _ isov _ ). Defined. diff --git a/TypeTheory/Csystems/lCsystems.v b/TypeTheory/Csystems/lCsystems.v index 044efa96..93e9f328 100644 --- a/TypeTheory/Csystems/lCsystems.v +++ b/TypeTheory/Csystems/lCsystems.v @@ -8,7 +8,7 @@ by V. Voevodsky as "Csubsystems". The definition of an lC-system given below does not require that the types of objects or morphisms of the underlying precategory form a set. It also does not require the -properties of the identity morphisms but does require associativity. +properties of the identity morphisms but does require associativity. The section Pullbacks (in particular Lemma q_of_f_is_pullback and @@ -24,14 +24,14 @@ Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. Require Export TypeTheory.Csystems.lC0systems. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.MoreFoundations.PartA. (** *** The l-C-systems *) -(** **** l-C-system data *) +(** **** l-C-system data *) Definition sf_type ( CC : lC0system_data ) := forall ( Y X : CC ) ( gt0 : ll X > 0 ) ( f : Y --> X ), sec_pX ( f_star gt0 ( ftf f ) ). @@ -39,7 +39,7 @@ Definition sf_type ( CC : lC0system_data ) := Definition lCsystem_data := ∑ CC : lC0system_data, sf_type CC. Definition lCsystem_data_constr { CC : lC0system_data } - ( sf0 : sf_type CC ) : lCsystem_data := tpair _ _ sf0 . + ( sf0 : sf_type CC ) : lCsystem_data := tpair _ _ sf0 . Definition lCsystem_data_pr1 : lCsystem_data -> lC0system_data := pr1. Coercion lCsystem_data_pr1 : lCsystem_data >-> lC0system_data. @@ -123,22 +123,22 @@ Proof. assert ( int2 : f_star gt0 ( ( ftf f ) · ( ( C0eiso gt0 g ) · g ) ) = f_star gt0 ( f · ( ( pX _ ) · ( ( C0eiso gt0 g ) · g ) ) ) ). { unfold ftf. - rewrite <- assoc. + rewrite <- assoc. apply idpath. } assert ( int3 : f_star gt0 ( f · ( ( pX _ ) · ( ( C0eiso gt0 g ) · g ) ) ) = f_star gt0 ( f · ( ( q_of_f gt0 g ) · ( pX U ) ) ) ). { unfold ftf. rewrite C0ax5c. - apply idpath. + apply idpath. } assert ( int4 : f_star gt0 ( f · ( ( q_of_f gt0 g ) · ( pX U ) ) ) = f_star gt0 (ftf (f · q_of_f gt0 g)) ). { unfold ftf. rewrite assoc. - apply idpath. + apply idpath. } - exact ( ( int1 @ int2 ) @ ( int3 @ int4 ) ). + exact ( ( int1 @ int2 ) @ ( int3 @ int4 ) ). Defined. @@ -165,7 +165,7 @@ Definition lCsystem_to_lCsystem_data ( CC : lCsystem ): lCsystem_data := Coercion lCsystem_to_lCsystem_data : lCsystem >-> lCsystem_data. Definition sf { CC : lCsystem } { Y X : CC } ( gt0 : ll X > 0 ) ( f : Y --> X ): - sec_pX ( f_star gt0 ( ftf f ) ) := ( pr1 ( pr2 CC ) ) Y X gt0 f. + sec_pX ( f_star gt0 ( ftf f ) ) := ( pr1 ( pr2 CC ) ) Y X gt0 f. Definition sf_ax1 { CC : lCsystem } { Y X : CC } ( gt0 : ll X > 0 ) ( f : Y --> X ): ( C0eiso gt0 ( ftf f ) ) · f = ( sf gt0 f ) · ( q_of_f gt0 ( ftf f ) ) := @@ -183,97 +183,97 @@ Definition sf_ax2 { CC : lCsystem } { Y Y' U : CC } ( gt0 : ll U > 0 ) (** **** Operation f_star_of_s *) Definition f_star_of_s { CC : lCsystem } { Y X : CC } ( f : Y --> ft X ) - ( gt0 : ll X > 0 ) ( s : sec_pX X ): sec_pX ( f_star gt0 f ). + ( gt0 : ll X > 0 ) ( s : sec_pX X ): sec_pX ( f_star gt0 f ). Proof. set ( int := sf gt0 ( f · s ) ). assert ( inteq : ftf ( f · s ) = f ). - { unfold ftf. + { unfold ftf. rewrite <- assoc. set ( eq := sec_pX_eq s : (s · pX X)= _). change ( f · (s · pX X ) = f ). rewrite eq. - apply id_right. + apply id_right. } - rewrite inteq in int. - exact int. + rewrite inteq in int. + exact int. Defined. - + (** **** Operation fsn_star_of_s *) Definition fsn_star_of_s { CC : lCsystem } { A X : CC } ( f : mor_to A ) - ( isab : isabove X A ) ( r : sec_pX X ) : sec_pX ( fn_star f isab ). + ( isab : isabove X A ) ( r : sec_pX X ) : sec_pX ( fn_star f isab ). Proof. rewrite f_star_isab. - apply f_star_of_s. + apply f_star_of_s. exact r. Defined. - + (* - + (** *** Operations qn, fn_star and f_star_of_s and fn_star_of_s *) (** **** Operations qn and fn_star *) -Definition qn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Definition qn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) : mor_to X . Proof. - intros until n . + intros until n . induction n as [ | n IHn ] . - intros . - change _ with ( X = A ) in eq . - apply ( mor_to_constr ( f ;; id_to_mor ( ! eq ) ) ) . + intros . + change _ with ( X = A ) in eq . + apply ( mor_to_constr ( f ;; id_to_mor ( ! eq ) ) ) . intros . set ( int := ftn_ft n X : ftn n ( ft X ) = ftn ( 1 + n ) X ) . - set ( gt0 := natgehgthtrans _ _ _ gtn ( natgthsn0 _ ) ) . - apply ( q_of_f gt0 ( IHn ( ft X ) ( ll_ft_gtn gtn ) ( int @ eq ) ) ) . + set ( gt0 := natgehgthtrans _ _ _ gtn ( natgthsn0 _ ) ) . + apply ( q_of_f gt0 ( IHn ( ft X ) ( ll_ft_gtn gtn ) ( int @ eq ) ) ) . Defined. Lemma qn_equals_qn { CC : lC0system_data } ( is : isaset CC ) { Y A : CC } ( f : Y --> A ) - { n1 n2 : nat } ( eqn : n1 = n2 ) + { n1 n2 : nat } ( eqn : n1 = n2 ) { X : CC } ( gtn1 : ll X >= n1 ) ( gtn2 : ll X >= n2 ) ( eq1 : ftn n1 X = A ) ( eq2 : ftn n2 X = A ) : qn f n1 gtn1 eq1 = qn f n2 gtn2 eq2 . Proof. - intros until n2 . - intro eqn . + intros until n2 . + intro eqn . rewrite eqn . - intros until gtn2 . - assert ( eq : gtn1 = gtn2 ) . apply ( proofirrelevance _ ( pr2 ( _ >= _ ) ) ) . - rewrite eq . - intros eq1 eq2 . + intros until gtn2 . + assert ( eq : gtn1 = gtn2 ) . apply ( proofirrelevance _ ( pr2 ( _ >= _ ) ) ) . + rewrite eq . + intros eq1 eq2 . assert ( eq' : eq1 = eq2 ) . - apply is . - rewrite eq' . + apply is . + rewrite eq' . apply idpath . Defined. - -Definition qsn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) + +Definition qsn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtsn : ll X >= S n ) ( eq : ftn (S n) X = A ) : qn f ( S n ) gtsn eq = q_of_f (natgehgthtrans _ _ _ gtsn ( natgthsn0 _ )) ( qn f n ( ll_ft_gtn gtsn ) ( ( ftn_ft n X ) @ eq ) ) := - idpath _ . + idpath _ . -Definition fn_star { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Definition fn_star { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) : CC := pr1 ( qn f n gtn eq ) . -Definition fsn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Definition fsn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtsn : ll X >= S n ) ( eq : ftn ( S n ) X = A ) : fn_star f ( S n ) gtsn eq = f_star (natgehgthtrans _ _ _ gtsn ( natgthsn0 _ )) @@ -282,78 +282,78 @@ Definition fsn { CC : lC0system_data } { Y A : CC } ( f : Y --> A ) ( n : nat ) -Lemma ll_fn_star { CC : lC0system } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Lemma ll_fn_star { CC : lC0system } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) : - ll ( fn_star f n gtn eq ) = ll Y + n . + ll ( fn_star f n gtn eq ) = ll Y + n . Proof. intros until n . induction n as [ | n IHn ] . intros . rewrite natplusr0 . apply idpath . - intros . + intros . change ( ll ( fn_star _ _ _ _ ) ) with ( ll ( f_star (natgehgthtrans _ _ _ gtn ( natgthsn0 _ )) - ( qn f n ( ll_ft_gtn gtn ) ( ( ftn_ft n X ) @ eq ) ) ) ) . + ( qn f n ( ll_ft_gtn gtn ) ( ( ftn_ft n X ) @ eq ) ) ) ) . rewrite ll_f_star . unfold fn_star in IHn . rewrite IHn . - apply ( ! ( natplusnsm ( ll Y ) n ) ) . + apply ( ! ( natplusnsm ( ll Y ) n ) ) . Defined. -Lemma isover_fn_star { CC : lC0system } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Lemma isover_fn_star { CC : lC0system } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtn : ll X >= n ) ( eq : ftn n X = A ) : isover ( fn_star f n gtn eq ) Y . Proof. intros until n . induction n as [ | n IHn ] . - intros . apply isover_XX . + intros . apply isover_XX . intros . - refine ( isover_trans ( isover_X_ftX _ ) _ ) . + refine ( isover_trans ( isover_X_ftX _ ) _ ) . change (fn_star f (S n) gtn eq) with ( f_star (natgehgthtrans _ _ _ gtn ( natgthsn0 _ )) ( qn f n ( ll_ft_gtn gtn ) ( ( ftn_ft n X ) @ eq ) ) ) . rewrite ft_f_star . - apply IHn . + apply IHn . Defined. - + (** **** Operation f_star_of_s *) Definition f_star_of_s { CC : lCsystem } { Y X : CC } ( f : Y --> ft X ) ( gt0 : ll X > 0 ) ( r : sec_pX X ) : - sec_pX ( f_star gt0 f ) . + sec_pX ( f_star gt0 f ) . Proof . - intros . - assert ( int := sf gt0 ( f ;; r ) ) . - assert ( inteq : ftf ( f ;; r ) = f ) . - unfold ftf . + intros . + assert ( int := sf gt0 ( f ;; r ) ) . + assert ( inteq : ftf ( f ;; r ) = f ) . + unfold ftf . rewrite <- assoc. - set ( eq := sec_pX_eq r : (r;; pX X)= _) . - change ( f ;; (r ;; pX X ) = f ) . + set ( eq := sec_pX_eq r : (r;; pX X)= _) . + change ( f ;; (r ;; pX X ) = f ) . rewrite eq . - apply id_right . + apply id_right . - rewrite inteq in int . - apply int . + rewrite inteq in int . + apply int . Defined. - + (** **** Operation fsn_start_of_s *) -Definition fsn_star_of_s { CC : lCsystem } { Y A : CC } ( f : Y --> A ) ( n : nat ) +Definition fsn_star_of_s { CC : lCsystem } { Y A : CC } ( f : Y --> A ) ( n : nat ) { X : CC } ( gtsn : ll X >= 1 + n ) ( eq : ftn ( 1 + n ) X = A ) ( r : sec_pX X ) : - sec_pX ( fn_star f ( 1 + n ) gtsn eq ) . + sec_pX ( fn_star f ( 1 + n ) gtsn eq ) . Proof . intros. set ( int := ftn_ft n X : ftn n ( ft X ) = ftn ( 1 + n ) X ) . set ( gt0 := natgehgthtrans _ _ _ gtsn ( natgthsn0 _ ) ) . - set ( qnint := qn f n ( ll_ft_gtn gtsn ) ( int @ eq ) : mor_to ( ft X ) ) . + set ( qnint := qn f n ( ll_ft_gtn gtsn ) ( int @ eq ) : mor_to ( ft X ) ) . change ( fn_star f ( 1 + n ) gtsn eq ) with ( f_star gt0 qnint ) . - apply ( f_star_of_s qnint gt0 r ) . + apply ( f_star_of_s qnint gt0 r ) . Defined. diff --git a/TypeTheory/Cubical/FillFromComp.v b/TypeTheory/Cubical/FillFromComp.v index 031505a4..94c58d12 100644 --- a/TypeTheory/Cubical/FillFromComp.v +++ b/TypeTheory/Cubical/FillFromComp.v @@ -86,11 +86,11 @@ Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. -Require Export UniMath.CategoryTheory.categories.HSET.Core. +Require Export UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.whiskering. -Require Import UniMath.CategoryTheory.limits.pullbacks. -Require Import UniMath.CategoryTheory.limits.binproducts. -Require Import UniMath.CategoryTheory.limits.terminal. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. +Require Import UniMath.CategoryTheory.Limits.BinProducts. +Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.LatticeObject. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.ElementsOp. diff --git a/TypeTheory/CwDM/CompCat_of_CwDM.v b/TypeTheory/CwDM/CompCat_of_CwDM.v index af1b67c2..8f6d3346 100644 --- a/TypeTheory/CwDM/CompCat_of_CwDM.v +++ b/TypeTheory/CwDM/CompCat_of_CwDM.v @@ -3,7 +3,7 @@ Definition of the displayed category of display maps over a category [C] -Given a category with display maps [C], we define a displayed +Given a category with display maps [C], we define a displayed category over [C]. Objects over [c:C] are display maps into [c]. *) @@ -11,7 +11,7 @@ category over [C]. Objects over [c:C] are display maps into [c]. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -39,7 +39,7 @@ Proof. use tpair. + intros x d. cbn in *. exact (pr1 d). - + cbn. intros x y xx yy f ff. + + cbn. intros x y xx yy f ff. exact ff. Defined. @@ -65,7 +65,7 @@ Lemma is_cartesian_comprehension_of_dm_structure Proof. use cartesian_functor_from_cleaving. - apply is_fibration_DM_disp. - - intros c c' f d. + - intros c c' f d. apply isPullback_cartesian_in_cod_disp. apply isPullback_of_dm_sub_pb. Qed. @@ -77,11 +77,11 @@ Definition total_comprehension_of_dm_structure (** This commutativity is an instance of a general lemma about comprehension categories once we have produced [comp_cat_of_dm] below *) -Lemma comprehension_of_dm_structure_triangle_commutes +Lemma comprehension_of_dm_structure_triangle_commutes : functor_composite total_comprehension_of_dm_structure (pr1_category _) - = pr1_category _ . -Proof. - apply functor_eq. + = pr1_category _ . +Proof. + apply functor_eq. - apply homset_property. - apply idpath. Qed. @@ -90,9 +90,9 @@ Definition comp_cat_of_dm : comprehension_cat_structure C. Proof. use tpair. - apply DM_disp. apply H. - - use tpair. + - use tpair. + apply is_fibration_DM_disp. - + use tpair. + + use tpair. * apply comprehension_of_dm_structure. * apply is_cartesian_comprehension_of_dm_structure. Defined. diff --git a/TypeTheory/CwDM/DispCat_of_CwDM.v b/TypeTheory/CwDM/DispCat_of_CwDM.v index f0ab8794..61efce70 100644 --- a/TypeTheory/CwDM/DispCat_of_CwDM.v +++ b/TypeTheory/CwDM/DispCat_of_CwDM.v @@ -3,7 +3,7 @@ Definition of the displayed category of display maps over a category [C] -Given a category with display maps [C], we define a displayed +Given a category with display maps [C], we define a displayed category over [C]. Objects over [c:C] are display maps into [c]. *) @@ -11,7 +11,7 @@ category over [C]. Objects over [c:C] are display maps into [c]. Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -25,12 +25,12 @@ Require Import TypeTheory.OtherDefs.DM. (** ** Displayed category induced by a display map category The total category associated to this displayed category is going to be isomorphic to -the subcategory of the arrow category where objects are display maps -(instead of all morphisms) +the subcategory of the arrow category where objects are display maps +(instead of all morphisms) *) -(* TODO: we could define the concept of a full displayed subcategory +(* TODO: we could define the concept of a full displayed subcategory The predicate on objects here would be induced by the predicate [H : DM] on arrows of [C]. *) @@ -47,7 +47,7 @@ Context (D : dm_sub_struct CC). Definition DM_disp_ob_mor : disp_cat_ob_mor CC. Proof. exists (fun Γ => DM_over D Γ). - simpl; intros Γ Δ p q f. + simpl; intros Γ Δ p q f. exact (∑ ff : ob_from_DM_over p --> ob_from_DM_over q, ff ;; q = p ;; f). Defined. @@ -77,21 +77,21 @@ Definition DM_disp_data : disp_cat_data CC Lemma DM_disp_axioms : disp_cat_axioms CC DM_disp_data. Proof. repeat apply tpair; intros; try apply homset_property. - - (* id_left_disp *) + - (* id_left_disp *) apply subtypePath. { intro. apply homset_property. } etrans. apply id_left. apply pathsinv0. etrans. use (pr1_transportf (CC⟦_,_⟧)). use transportf_const'. - - (* id_right_disp *) + - (* id_right_disp *) apply subtypePath. { intro. apply homset_property. } etrans. apply id_right. apply pathsinv0. etrans. use (pr1_transportf (CC⟦_,_⟧)). use transportf_const'. - - (* assoc_disp *) + - (* assoc_disp *) apply subtypePath. { intro. apply homset_property. } etrans. apply assoc. @@ -116,7 +116,7 @@ Definition pullback_is_cartesian Proof. intros Hpb Δ g q hh. eapply iscontrweqf. - 2: { + 2: { use Hpb. + exact (ob_from_DM_over q). + exact (pr1 hh). @@ -127,7 +127,7 @@ Proof. 2: { apply weqtotal2asstol. } apply weq_subtypes_iff. - intro. apply isapropdirprod; apply homset_property. - - intro. apply (isofhleveltotal2 1). + - intro. apply (isofhleveltotal2 1). + apply homset_property. + intros. apply homsets_disp. - intros gg; split; intros H. @@ -142,7 +142,7 @@ Qed. End Displayed_Cat_of_Class_of_Maps. -(* Even for a fibration, we don’t need a full displayed cat structure: just that we have pullbacks, not the closure under iso or the fact that the [DM] predicate is a prop. +(* Even for a fibration, we don’t need a full displayed cat structure: just that we have pullbacks, not the closure under iso or the fact that the [DM] predicate is a prop. TODO: maybe factor out this dependency — name the separate conditions on classes of maps, and state just the hypotheses as needed. *) diff --git a/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Cats_Standalone.v b/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Cats_Standalone.v index 47d7be5a..bee2f5c8 100644 --- a/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Cats_Standalone.v +++ b/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Cats_Standalone.v @@ -54,12 +54,12 @@ Variable X : obj_ext_structure C. (** * category of term-structures *) Section Term_Fun_Structure_Precat. -Definition term_fun_mor - (Y Y' : term_fun_structure C X) +Definition term_fun_mor + (Y Y' : term_fun_structure C X) : UU := ∑ FF_TM : TM Y --> TM Y', - FF_TM ;; pp Y' = pp Y - × + FF_TM ;; pp Y' = pp Y + × ∏ {Γ:C} {A : Ty X Γ}, FF_TM $nt (te Y A) = te Y' _. @@ -69,7 +69,7 @@ Definition term_fun_mor_TM {Y Y'} (FF : term_fun_mor Y Y') := pr1 FF. Definition term_fun_mor_pp {Y Y'} (FF : term_fun_mor Y Y') - : term_fun_mor_TM FF ;; pp Y' = pp Y + : term_fun_mor_TM FF ;; pp Y' = pp Y := pr1 (pr2 FF). Definition term_fun_mor_te {Y Y'} (FF : term_fun_mor Y Y') @@ -99,7 +99,7 @@ Proof. - intros x; apply isapropdirprod. + apply homset_property. + repeat (apply impred_isaprop; intro). apply setproperty. - - apply nat_trans_eq. apply has_homsets_HSET. + - apply nat_trans_eq. apply has_homsets_HSET. intros Γ. apply funextsec. unfold homot. apply e_TM. Qed. @@ -109,7 +109,7 @@ Lemma term_to_section_naturality {Y} {Y'} {FY : term_fun_mor Y Y'} {Γ : C} (t : Tm Y Γ) (A := pp Y $nt t) : pr1 (term_to_section (term_fun_mor_TM FY $nt t)) - = pr1 (term_to_section t) + = pr1 (term_to_section t) ;; Δ (!nat_trans_eq_pointwise_pshf (term_fun_mor_pp FY) _). Proof. set (t' := term_fun_mor_TM FY $nt t). @@ -123,7 +123,7 @@ Proof. etrans. apply @pathsinv0, assoc. apply maponpaths. apply comp_ext_compare_π. - - etrans. apply term_to_section_recover. + - etrans. apply term_to_section_recover. apply pathsinv0. etrans. apply Q_comp_ext_compare. etrans. @@ -152,7 +152,7 @@ Proof. Qed. -Definition term_fun_ob_mor : precategory_ob_mor. +Definition term_fun_ob_mor : precategory_ob_mor. Proof. exists (term_fun_structure C X). exact @term_fun_mor. @@ -163,7 +163,7 @@ Proof. apply tpair. - intros Y. simpl; unfold term_fun_mor. exists (identity _). apply tpair. - + apply id_left. + + apply id_left. + intros Γ A. apply idpath. - intros Y0 Y1 Y2 FF GG. exists (term_fun_mor_TM FF ;; term_fun_mor_TM GG). apply tpair. @@ -175,7 +175,7 @@ Proof. apply term_fun_mor_te. Defined. -Definition term_fun_data : precategory_data +Definition term_fun_data : precategory_data := (_ ,, term_fun_id_comp). Definition term_fun_axioms : is_precategory term_fun_data. @@ -183,10 +183,10 @@ Proof. use make_is_precategory_one_assoc; intros; apply isaprop_term_fun_mor. Qed. -Definition term_fun_precategory : precategory +Definition term_fun_precategory : precategory := (_ ,, term_fun_axioms). -Lemma has_homsets_term_fun_precat +Lemma has_homsets_term_fun_precat : has_homsets term_fun_precategory. Proof. intros a b. apply isaset_total2. @@ -215,7 +215,7 @@ Lemma isaprop_qq_structure_mor (Z Z' : qq_structure_ob_mor) : isaprop (Z --> Z'). Proof. - repeat (apply impred_isaprop; intro). apply homset_property. + repeat (apply impred_isaprop; intro). apply homset_property. Qed. Definition qq_structure_id_comp : precategory_id_comp qq_structure_ob_mor. @@ -228,7 +228,7 @@ Proof. etrans. apply FF. apply GG. Qed. -Definition qq_structure_data : precategory_data +Definition qq_structure_data : precategory_data := (_ ,, qq_structure_id_comp). Definition qq_structure_axioms : is_precategory qq_structure_data. @@ -252,7 +252,7 @@ Definition strucs_compat_ob_mor : precategory_ob_mor. Proof. use tpair. - - exact (∑ YZ : (term_fun_precategory × qq_structure_precategory), + - exact (∑ YZ : (term_fun_precategory × qq_structure_precategory), iscompatible_term_qq (pr1 YZ) (pr2 YZ)). - intros YZ YZ'. exact ((pr1 (pr1 YZ)) --> (pr1 (pr1 YZ')) @@ -262,14 +262,14 @@ Defined. Definition strucs_compat_id_comp : precategory_id_comp strucs_compat_ob_mor. Proof. - split. + split. - intro; split; apply identity. - - intros a b c f g. split. - eapply @compose. apply (pr1 f). apply (pr1 g). - eapply @compose. apply (pr2 f). apply (pr2 g). + - intros a b c f g. split. + eapply @compose. apply (pr1 f). apply (pr1 g). + eapply @compose. apply (pr2 f). apply (pr2 g). Defined. -Definition strucs_compat_data : precategory_data +Definition strucs_compat_data : precategory_data := ( _ ,, strucs_compat_id_comp). Definition strucs_compat_axioms : is_precategory strucs_compat_data. @@ -281,7 +281,7 @@ Proof. Qed. Definition compat_structures_precategory - : precategory + : precategory := ( _ ,, strucs_compat_axioms). (* should this be the name of the compatible pairs category? *) @@ -327,15 +327,15 @@ Proof. apply iscompatible_qq_from_term. Defined. -Lemma qq_from_term_mor +Lemma qq_from_term_mor {Y : term_fun_precategory} {Y'} (FY : Y --> Y') {Z : qq_structure_precategory} {Z'} (W : iscompatible_term_qq Y Z) (W' : iscompatible_term_qq Y' Z') - : Z --> Z'. + : Z --> Z'. Proof. intros Γ' Γ f A. - cbn in W, W', FY. unfold iscompatible_term_qq in *. + cbn in W, W', FY. unfold iscompatible_term_qq in *. unfold term_fun_mor in FY. apply (Q_pp_Pb_unique Y'); simpl; unfold yoneda_morphisms_data. - etrans. apply qq_π. @@ -348,7 +348,7 @@ Proof. Qed. -Lemma qq_from_term_mor_unique +Lemma qq_from_term_mor_unique {Y : term_fun_precategory} {Y'} (FY : Y --> Y') {Z : qq_structure_precategory} {Z'} (W : iscompatible_term_qq Y Z) @@ -400,7 +400,7 @@ Proof. + set (XX := (make_Pullback _ (qq_π_Pb (pr1 Z) f A))). apply (PullbackArrow_PullbackPr1 XX). + cbn; cbn in FZ. etrans. apply maponpaths, @pathsinv0, FZ. - apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). + apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). Qed. Lemma tm_from_qq_mor_TM {Z Z' : qq_structure_precategory} (FZ : Z --> Z') @@ -425,17 +425,17 @@ Proof. cbn. use tm_from_qq_eq. - apply idpath. - - etrans. apply id_right. + - etrans. apply id_right. cbn. apply PullbackArrowUnique. + cbn. apply (PullbackArrow_PullbackPr1 (make_Pullback _ _)). - + cbn. cbn in FZ. + + cbn. cbn in FZ. etrans. apply maponpaths, @pathsinv0, FZ. - apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). + apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). Qed. End Rename_me. -Definition term_from_qq_mor_TM +Definition term_from_qq_mor_TM {Z : qq_structure_precategory} {Z'} (FZ : Z --> Z') {Y : term_fun_precategory} {Y'} (W : iscompatible_term_qq Y Z) @@ -471,7 +471,7 @@ Proof. apply (canonical_TM_to_given_te _ _ (_,,_)). Qed. -Lemma term_from_qq_mor_unique +Lemma term_from_qq_mor_unique {Z : qq_structure_precategory} {Z'} (FZ : Z --> Z') {Y : term_fun_precategory} {Y'} (W : iscompatible_term_qq Y Z) @@ -506,7 +506,7 @@ Proof. - intros. cbn. destruct x as [f q]. cbn. apply maponpaths. apply proofirrelevance. - use (qq_from_term_mor_unique f); assumption. + use (qq_from_term_mor_unique f); assumption. - intros y. cbn. apply idpath. Qed. @@ -543,7 +543,7 @@ Section Is_Univalent_Families_Strucs. Definition iso_to_TM_eq (Y Y' : term_fun_precategory) - : z_iso Y Y' + : z_iso Y Y' -> TM (Y : term_fun_structure _ X) = TM (Y' : term_fun_structure _ X). Proof. intro i. @@ -556,7 +556,7 @@ Proof. + exact (maponpaths term_fun_mor_TM (z_iso_after_z_iso_inv i)). Defined. -Lemma prewhisker_iso_to_TM_eq +Lemma prewhisker_iso_to_TM_eq {Y Y' : term_fun_precategory} (FG : z_iso Y Y') {P : preShv C} (α : TM (Y : term_fun_structure _ X) --> P) @@ -568,7 +568,7 @@ Proof. apply inv_from_z_iso_from_is_z_iso. Qed. -Lemma postwhisker_iso_to_TM_eq +Lemma postwhisker_iso_to_TM_eq {Y Y' : term_fun_precategory} (FG : z_iso Y Y') {P : preShv C} (α : P --> TM (Y : term_fun_structure _ X)) @@ -578,7 +578,7 @@ Proof. use postwhisker_isotoid. Qed. -Lemma idtoiso_iso_to_TM_eq +Lemma idtoiso_iso_to_TM_eq {Y Y' : term_fun_precategory} (FG : z_iso Y Y') : (idtoiso (iso_to_TM_eq _ _ FG) : _ --> _) @@ -597,7 +597,7 @@ Proof. rewrite transportf_dirprod. apply dirprodeq. - etrans. apply prewhisker_iso_to_TM_eq. - apply term_fun_mor_pp. + apply term_fun_mor_pp. - etrans. use transportf_forall. apply funextsec; intros Γ. etrans. use transportf_forall. @@ -636,7 +636,7 @@ End Is_Univalent_Families_Strucs. Section Is_Univalent_qq_Strucs. -Lemma isaset_qq_morphism_structure (x : obj_ext_structure C) +Lemma isaset_qq_morphism_structure (x : obj_ext_structure C) : isaset (qq_morphism_structure x). Proof. apply (isofhleveltotal2 2). @@ -648,7 +648,7 @@ Proof. * apply hlevelntosn. apply homset_property. * intro. apply hlevelntosn. - apply pullbacks.isaprop_isPullback. + apply Pullbacks.isaprop_isPullback. - intro d. unfold qq_morphism_axioms. apply isofhleveldirprod. + do 2 (apply impred; intro). @@ -669,7 +669,7 @@ Definition qq_structure_category : category := make_category _ has_homsets_qq_structure_precategory. -Lemma isaprop_iso_qq_morphism_structure +Lemma isaprop_iso_qq_morphism_structure (d d' : qq_structure_category) : isaprop (z_iso d d'). Proof. @@ -679,21 +679,21 @@ Proof. - intro. apply isaprop_is_z_isomorphism. Qed. -Lemma qq_structure_eq +Lemma qq_structure_eq (x : obj_ext_structure C) (d d' : qq_morphism_structure x) - (H : ∏ (Γ Γ' : C) (f : Γ' --> Γ) (A : Ty x Γ), + (H : ∏ (Γ Γ' : C) (f : Γ' --> Γ) (A : Ty x Γ), qq d f A = qq d' f A) : d = d'. Proof. apply subtypePath. { intro. apply isaprop_qq_morphism_axioms. } apply subtypePath. - { intro. do 4 (apply impred; intro). + { intro. do 4 (apply impred; intro). apply isofhleveltotal2. + apply homset_property. - + intro. apply pullbacks.isaprop_isPullback. - } + + intro. apply Pullbacks.isaprop_isPullback. + } do 4 (apply funextsec; intro). apply H. Defined. @@ -702,17 +702,17 @@ Definition qq_structure_iso_to_id (d d' : qq_structure_precategory) : z_iso d d' → d = d'. Proof. - intro H. + intro H. apply qq_structure_eq. intros Γ Γ' f A. use (pr1 H). -Defined. +Defined. Theorem is_univalent_qq_morphism : is_univalent qq_structure_category. Proof. - intros d d'. - use isweqimplimpl. + intros d d'. + use isweqimplimpl. + apply qq_structure_iso_to_id. + apply isaset_qq_morphism_structure. + apply isaprop_iso_qq_morphism_structure. @@ -720,13 +720,13 @@ Qed. End Is_Univalent_qq_Strucs. -Lemma has_homsets_compat_structures_precategory +Lemma has_homsets_compat_structures_precategory : has_homsets compat_structures_precategory. Proof. - intros a b. - apply isasetdirprod. + intros a b. + apply isasetdirprod. - apply has_homsets_term_fun_precategory. - - apply has_homsets_qq_structure_precategory. + - apply has_homsets_qq_structure_precategory. Qed. Definition compat_structures_category : category @@ -757,11 +757,11 @@ Proof. use adj_equivalence_of_cats_inv. Defined. -Definition equiv_of_structures : adj_equivalence_of_cats _ - := @comp_adj_equivalence_of_cats _ _ _ _ _ +Definition equiv_of_structures : adj_equivalence_of_cats _ + := @comp_adj_equivalence_of_cats _ _ _ _ _ pr1_equiv_inv pr2_equiv. -Definition equiv_of_types_of_structures +Definition equiv_of_types_of_structures : term_fun_precategory ≃ qq_structure_precategory. Proof. use (weq_on_objects_from_adj_equiv_of_cats _ _ @@ -772,7 +772,7 @@ Proof. Defined. -Lemma equiv_of_types_equal_direct_constr +Lemma equiv_of_types_equal_direct_constr : equiv_of_types_of_structures ~ weq_term_qq X. Proof. intro Y. diff --git a/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Univalent_Cats.v b/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Univalent_Cats.v index 88f532a5..9ba68fb3 100644 --- a/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Univalent_Cats.v +++ b/TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Univalent_Cats.v @@ -65,8 +65,8 @@ Section Is_Univalent_Obj_Ext_Disp. -> X -->[identity_z_iso TY] X'. Proof. intros I Γ A. - exists (pr1 (I Γ A)). - apply pathsinv0, (pr2 (I Γ A)). + exists (pr1 (I Γ A)). + apply pathsinv0, (pr2 (I Γ A)). Defined. Lemma is_iso_slice_isos_to_obj_ext_map {TY : PreShv C} {X X' : obj_ext_disp TY} @@ -78,12 +78,12 @@ Section Is_Univalent_Obj_Ext_Disp. - use obj_ext_mor_disp_transportb_eq_gen. + cbn; intros; apply idpath. + cbn; intros. - etrans. { apply id_right. } + etrans. { apply id_right. } exact (maponpaths pr1 (z_iso_after_z_iso_inv (I Γ A))). - use obj_ext_mor_disp_transportb_eq_gen. + cbn; intros; apply idpath. + cbn; intros. - etrans. { apply id_right. } + etrans. { apply id_right. } exact (maponpaths pr1 (z_iso_inv_after_z_iso (I Γ A))). Qed. @@ -101,7 +101,7 @@ Section Is_Univalent_Obj_Ext_Disp. -> (∏ Γ A, slice_cat C Γ ⟦ X Γ A , X' Γ A ⟧). Proof. intros I Γ A. - exists (pr1 (I Γ A)). + exists (pr1 (I Γ A)). apply pathsinv0, (pr2 (I Γ A)). Defined. @@ -118,13 +118,13 @@ Section Is_Univalent_Obj_Ext_Disp. etrans. { apply I_V. } etrans. { use obj_ext_mor_disp_transportb. } etrans. { apply id_left. } - apply comp_ext_compare_id_general. + apply comp_ext_compare_id_general. - set (V_I := z_iso_disp_after_inv_mor I). apply (maponpaths (fun f => obj_ext_mor_disp_φ f A)) in V_I. etrans. { apply V_I. } etrans. { use obj_ext_mor_disp_transportb. } etrans. { apply id_left. } - apply comp_ext_compare_id_general. + apply comp_ext_compare_id_general. Qed. Lemma isweq_slice_isos_obj_ext_iso {TY : PreShv C} (X X' : obj_ext_disp TY) @@ -132,7 +132,7 @@ Section Is_Univalent_Obj_Ext_Disp. Proof. use gradth. - intros I Γ A; use tpair. - apply (obj_ext_map_to_slice_maps I). + apply (obj_ext_map_to_slice_maps I). apply is_iso_obj_ext_iso_to_slice_maps. - intros I. apply funextsec; intros Γ. @@ -158,8 +158,8 @@ Section Is_Univalent_Obj_Ext_Disp. : X = X' ≃ z_iso_disp (identity_z_iso TY) X X'. Proof. apply (@weqcomp _ (forall Γ A, X Γ A = X' Γ A)). - { refine (weqcomp _ _). { apply weqtoforallpaths. } - apply weqonsecfibers; intros Γ. + { refine (weqcomp _ _). { apply weqtoforallpaths. } + apply weqonsecfibers; intros Γ. apply weqtoforallpaths. } eapply weqcomp. @@ -169,7 +169,7 @@ Section Is_Univalent_Obj_Ext_Disp. } apply weq_slice_isos_obj_ext_iso. Defined. - + Lemma is_univalent_obj_ext_fibers : is_univalent_in_fibers (@obj_ext_disp C). Proof. unfold is_univalent_in_fibers. @@ -186,7 +186,7 @@ Section Is_Univalent_Obj_Ext_Disp. apply is_univalent_disp_from_fibers, is_univalent_obj_ext_fibers. Defined. - + Theorem is_univalent_obj_ext : is_univalent (obj_ext_cat C). Proof. apply is_univalent_total_category. @@ -216,7 +216,7 @@ Proof. apply transportf_term_fun_mor_TM. Defined. -Lemma prewhisker_iso_disp_to_TM_eq +Lemma prewhisker_iso_disp_to_TM_eq {X} {Y Y' : term_fun_disp_cat C X} (FG : z_iso_disp (identity_z_iso X) Y Y') {P : preShv C} (α : TM (Y : term_fun_structure _ X) --> P) @@ -228,7 +228,7 @@ Proof. apply inv_from_z_iso_from_is_z_iso. Qed. -Lemma postwhisker_iso_disp_to_TM_eq +Lemma postwhisker_iso_disp_to_TM_eq {X} {Y Y' : term_fun_disp_cat C X} (FG : z_iso_disp (identity_z_iso X) Y Y') {P : preShv C} (α : P --> TM (Y : term_fun_structure _ X)) @@ -238,7 +238,7 @@ Proof. apply postwhisker_isotoid. Qed. -Lemma idtoiso_iso_disp_to_TM_eq +Lemma idtoiso_iso_disp_to_TM_eq {X} {Y Y' : term_fun_disp_cat C X} (FG : z_iso_disp (identity_z_iso X) Y Y') : (idtoiso (iso_disp_to_TM_eq _ _ _ FG) : _ --> _) @@ -286,7 +286,7 @@ End Is_Univalent_Families_Strucs. Section Is_Univalent_qq_Strucs. -Lemma isaset_qq_morphism_structure (x : obj_ext_structure C) +Lemma isaset_qq_morphism_structure (x : obj_ext_structure C) : isaset (qq_morphism_structure x). Proof. apply (isofhleveltotal2 2). @@ -298,7 +298,7 @@ Proof. * apply hlevelntosn. apply homset_property. * intro. apply hlevelntosn. - apply pullbacks.isaprop_isPullback. + apply Pullbacks.isaprop_isPullback. - intro d. unfold qq_morphism_axioms. apply isofhleveldirprod. + do 2 (apply impred; intro). @@ -309,7 +309,7 @@ Proof. apply homset_property. Qed. -Lemma isaprop_iso_disp_qq_morphism_structure +Lemma isaprop_iso_disp_qq_morphism_structure (x : obj_ext_cat C) (d d' : (qq_structure_disp_cat C) x) : isaprop (z_iso_disp (identity_z_iso x) d d'). @@ -320,21 +320,21 @@ Proof. - intro. apply isaprop_is_z_iso_disp. Qed. -Lemma qq_structure_eq +Lemma qq_structure_eq (x : obj_ext_cat C) (d d' : qq_morphism_structure x) - (H : ∏ (Γ Γ' : C) (f : Γ' --> Γ) (A : TY x $p Γ), + (H : ∏ (Γ Γ' : C) (f : Γ' --> Γ) (A : TY x $p Γ), qq d f A = qq d' f A) : d = d'. Proof. apply subtypePath. { intro. apply isaprop_qq_morphism_axioms. } apply subtypePath. - { intro. do 4 (apply impred; intro). + { intro. do 4 (apply impred; intro). apply isofhleveltotal2. + apply homset_property. - + intro. apply pullbacks.isaprop_isPullback. - } + + intro. apply Pullbacks.isaprop_isPullback. + } do 4 (apply funextsec; intro). apply H. Defined. @@ -344,7 +344,7 @@ Definition qq_structure_iso_disp_to_id (d d' : (qq_structure_disp_cat C) x) : z_iso_disp (identity_z_iso x) d d' → d = d'. Proof. - intro H. + intro H. apply qq_structure_eq. intros Γ Γ' f A. assert (XR := pr1 H); clear H. @@ -352,19 +352,19 @@ Proof. rewrite id_right in XR. rewrite id_left in XR. etrans. apply XR. - match goal with [|- Δ ?ee ;; _ = _ ] => set (e := ee) end. + match goal with [|- Δ ?ee ;; _ = _ ] => set (e := ee) end. simpl in e; unfold identity in e; simpl in e. assert (X : e = idpath _ ). { apply setproperty. } rewrite X. apply id_left. -Defined. - +Defined. + Theorem is_univalent_qq_morphism : is_univalent_disp (qq_structure_disp_cat C). Proof. apply is_univalent_disp_from_fibers. - intros x d d'. - use isweqimplimpl. + intros x d d'. + use isweqimplimpl. - apply qq_structure_iso_disp_to_id. - apply isaset_qq_morphism_structure. - apply isaprop_iso_disp_qq_morphism_structure. @@ -423,7 +423,7 @@ Section Is_Univalent_Total_Cats. - apply @is_univalent_obj_ext; auto. - apply is_univalent_term_fun_structure. Defined. - + Theorem is_univalent_sty'_structure_precat : is_univalent (sty'_structure_precat C). Proof. diff --git a/TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v b/TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v index 6d358478..aa21299c 100644 --- a/TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v +++ b/TypeTheory/CwF_TypeCat/TypeCat_Reassoc.v @@ -1,5 +1,5 @@ -(** +(** Ahrens, Lumsdaine, Voevodsky, 2015– @@ -18,8 +18,8 @@ The equivalence is a bit more involved than one might hope; it proceeds in two m Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. -Require Import UniMath.CategoryTheory.limits.pullbacks. -Require Import UniMath.CategoryTheory.categories.HSET.All. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. +Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.opp_precat. Require Import TypeTheory.Auxiliary.Auxiliary. @@ -46,7 +46,7 @@ Context (T_q_id : ∏ ty ext dpr reind, (T_q_etc ty ext dpr reind) -> (T_reind_id ty reind) -> UU) (T_reind_comp : ∏ ty, T_reind ty -> UU) - (T_q_comp : ∏ ty ext dpr reind, + (T_q_comp : ∏ ty ext dpr reind, (T_q_etc ty ext dpr reind) -> (T_reind_comp ty reind) -> UU). Arguments T_dpr [_] _. @@ -96,7 +96,7 @@ Definition obj_ext_struct Definition gen_q_mor_data (X : obj_ext_struct) (ext := pr1 (pr2 X)) (dpr := pr2 (pr2 X)) - (reind := pr2 (pr1 (pr1 X))) + (reind := pr2 (pr1 (pr1 X))) := T_q_etc dpr reind. Definition gen_q_mor_axs {X : obj_ext_struct} (q_etc : gen_q_mor_data X) @@ -154,10 +154,10 @@ Defined. Theorem weq_reassoc_direct : split_struct ≃ reassoc_split_struct. Proof. use (weq_iso l_to_r_reassoc_direct r_to_l_reassoc_direct). - - intros [[[ty [ext reind]] [dpr q_etc]] + - intros [[[ty [ext reind]] [dpr q_etc]] [set [[reind_id q_id] [reind_comp q_comp]]]]. apply idpath. - - intros [[[[[ty set] reind] [reind_id reind_comp]] [ext dpr]] + - intros [[[[[ty set] reind] [reind_id reind_comp]] [ext dpr]] [q_etc [q_id q_comp]]]. apply idpath. Defined. @@ -168,7 +168,7 @@ Section Fix_Category. Context {CC : category}. -(** ** Equivalence between split type-cat structures and their structurally-abstracted version +(** ** Equivalence between split type-cat structures and their structurally-abstracted version This is in fact a judgemental equality; but recognising this in practice is rather slow, so we explicitly declare the equivalence [weq_standalone_structural] between them. *) @@ -183,7 +183,7 @@ Definition T_dpr Definition T_reind := (λ ty, ∏ (Γ : CC) (A : ty Γ) (Γ' : CC), (Γ' --> Γ) -> ty Γ'). Definition T_q_etc - := (λ ty ext (dpr : T_dpr ty ext) (reind : T_reind ty), + := (λ ty ext (dpr : T_dpr ty ext) (reind : T_reind ty), ∑ (q : ∏ (Γ:CC) (A : ty Γ) Γ' (f : Γ' --> Γ), (ext Γ' (reind _ A _ f)) --> (ext Γ A)) (dpr_q : ∏ Γ (A : ty Γ) Γ' (f : Γ' --> Γ), @@ -263,7 +263,7 @@ Defined. End Split_Type_Cat_as_Structural. -(** ** Equivalence between the structural and object-extension versions +(** ** Equivalence between the structural and object-extension versions Here we build up an equivalence [weq_structural_regrouped] between (RHS) the regrouped object-extension structure definition of split type-category structures, and (LHS) the structurally-abstracted definition, with the types of components taken from the standalone definition, but re-ordered and re-grouped to match (RHS). @@ -290,15 +290,15 @@ Definition weq_structural_pshf_axioms Proof. apply weqdirprodf. - cbn. unfold bandfmap, weqforalltototal, maponsec. - cbn. unfold totaltoforall, T_reind_id, functor_idax. + cbn. unfold totaltoforall, T_reind_id, functor_idax. apply weqonsecfibers; intro Γ. apply weqfunextsec. - cbn. unfold bandfmap, weqforalltototal, maponsec. - cbn. unfold totaltoforall, T_reind_comp, functor_compax. + cbn. unfold totaltoforall, T_reind_comp, functor_compax. apply weqonsecfibers; intro Γ. eapply weqcomp. apply weq_exchange_args. apply weqonsecfibers; intro Γ'. - eapply weqcomp. + eapply weqcomp. apply weqonsecfibers; intro A. apply weq_exchange_args. eapply weqcomp. apply weq_exchange_args. apply weqonsecfibers; intro Γ''. @@ -379,7 +379,7 @@ Definition weq_structural_regrouped T_set T_reind_id T_q_id T_reind_comp T_q_comp ≃ split_typecat'_structure CC. Proof. - use weqbandf. apply weq_structural_obj_ext. intro X. + use weqbandf. apply weq_structural_obj_ext. intro X. use weqbandf. apply weq_structural_q_mor_data. intros q_etc. unfold qq_morphism_axioms. cbn. unfold bandfmap, weqforalltototal, maponsec. cbn. @@ -393,7 +393,7 @@ Proof. - apply weqonsecfibers; intro Γ. eapply weqcomp. apply weq_exchange_args. apply weqonsecfibers; intro Γ'. - eapply weqcomp. + eapply weqcomp. apply weqonsecfibers; intro A. apply weq_exchange_args. eapply weqcomp. apply weq_exchange_args. apply weqonsecfibers; intro Γ''. diff --git a/TypeTheory/Initiality/SyntacticCategory.v b/TypeTheory/Initiality/SyntacticCategory.v index 512f218c..0108237e 100644 --- a/TypeTheory/Initiality/SyntacticCategory.v +++ b/TypeTheory/Initiality/SyntacticCategory.v @@ -4,8 +4,8 @@ As a matter of organisation: all concrete lemmas involving derivations should li Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. -Require Import UniMath.CategoryTheory.limits.pullbacks. -Require Import UniMath.CategoryTheory.limits.graphs.terminal. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. +Require Import UniMath.CategoryTheory.Limits.Graphs.Terminal. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -207,7 +207,7 @@ Section Contexts_Modulo_Equality. apply hinhpr. exact tt. Defined. - + Definition derivable_cxteq_hrel {n} : hrel (wellformed_context_of_length n) := fun Γ Δ => ∥ derivation_flat_cxteq Γ Δ ∥. @@ -383,7 +383,7 @@ Section Context_Maps. Lemma raw_mapeq_for_some_rep {ΓΓ ΔΔ : context_mod_eq} (f g : raw_context_map ΓΓ ΔΔ) - + : (∃ (Γ:context_representative ΓΓ) (Δ:context_representative ΔΔ), ∥ [! |- f ::: Γ ---> Δ !] × [! |- g ::: Γ ---> Δ !] @@ -458,11 +458,11 @@ Section Context_Map_Operations. [ apply isapropishinh | intros Δ; unsquash from Δ (map_derivable f Γ Δ) (map_derivable g Δ Θ) - as d_Δ d_f d_g; apply hinhpr; + as d_Δ d_f d_g; apply hinhpr; eauto using (derive_comp d_f) ]). - (* respecting equality in [f] *) abstract ( intros f f' g e_f Γ Θ; cbn; - apply (take_context_representative ΔΔ); + apply (take_context_representative ΔΔ); [ apply isapropishinh | intros Δ; unsquash from Γ (e_f Γ Δ) (map_derivable f Γ Δ) @@ -622,7 +622,7 @@ Section Syntactic_Types. intros H Γ. unsquash H as [Γ' d_A]. unsquash from Γ Γ' (cxteq_context_representatives Γ Γ') as d_Γ d_Γ' e_Γ. - apply hinhpr, (derive_ty_conv_cxteq Γ'); + apply hinhpr, (derive_ty_conv_cxteq Γ'); eauto using derive_flat_cxteq_sym, derive_flat_cxt_from_strat. Qed. @@ -741,7 +741,7 @@ Section Split_Typecat. exact (derive_dB_next_context_map d_Γ d_A). Defined. - Local Definition qmor_raw + Local Definition qmor_raw {ΓΓ : context_mod_eq} (AA : type_mod_eq ΓΓ) {ΓΓ' : context_mod_eq} (f : raw_context_map ΓΓ' ΓΓ) : raw_context_map (S ΓΓ') (S ΓΓ). @@ -796,7 +796,7 @@ Section Split_Typecat. try refine (derive_weaken_raw_context_map _ _ _ d_f); auto using derive_flat_cxt_from_strat, (@derive_flat_cxteq_refl Γ'). + refine (derive_weaken_raw_context_map _ _ _ d_g); - auto using derive_flat_cxt_from_strat. + auto using derive_flat_cxt_from_strat. + refine (derive_weaken_raw_context_mapeq _ _ _ _ _ d_fg); auto using derive_flat_cxt_from_strat. Qed. @@ -822,12 +822,12 @@ Section Split_Typecat. revert ff; use setquotunivprop'. { intros; apply isasetsetquot. } intros f. simpl. apply iscompsetquotpr. - use mapeq_from_path. + use mapeq_from_path. intros i; simpl. apply rename_as_subst_tm. Qed. - Local Definition reind_pb_raw + Local Definition reind_pb_raw {ΓΓ ΓΓ' ΔΔ: context_mod_eq} (g : raw_context_map ΔΔ ΓΓ') (h : raw_context_map ΔΔ (S ΓΓ)) : raw_context_map ΔΔ (S ΓΓ'). @@ -866,7 +866,7 @@ Section Split_Typecat. refine (derive_extend_context_map d_g _); simpl. assert (d_dpr_h : [! |- comp_raw_context h (dB_next_context_map Γ) ::: Δ ---> Γ !]). - { refine (derive_comp d_h _). + { refine (derive_comp d_h _). use derive_dB_next_context_map; auto using derive_flat_cxt_from_strat. } assert (d_g_f : [! |- comp_raw_context g f ::: Δ ---> Γ !]). { exact (derive_comp d_g d_f). } @@ -884,7 +884,7 @@ Section Split_Typecat. (* TODO: [reind_pb_eq], analogous to [qmor_eq] *) - Local Definition reind_pb + Local Definition reind_pb {ΓΓ : context_mod_eq} (AA : type_mod_eq ΓΓ) {ΓΓ' : context_mod_eq} (ff : map_mod_eq ΓΓ' ΓΓ) : @isPullback syntactic_category _ _ _ _ @@ -952,17 +952,17 @@ Section Split_Typecat. + simpl. admit. (* This should be provable once we know how to do the above admit *) Admitted. (* [is_split_syntactic_typecat_structure]: seems a bit harder than one might expect. *) - + Definition syntactic_typecat : split_typecat := ((syntactic_category,, syntactic_typecat_structure),, is_split_syntactic_typecat_structure). - + End Split_Typecat. Section Contextuality. (* TODO: Should some of these lemmas be upstreamed? *) - + Local Definition empty_context : syntactic_typecat. Proof. exists 0. @@ -981,7 +981,7 @@ Section Contextuality. use make_isTerminal. intros x. use tpair. - - apply setquotpr. + - apply setquotpr. use tpair. + apply raw_context_map_0. + simpl. @@ -1006,7 +1006,7 @@ Section Contextuality. exists (pr11 G). apply (hinhfun pr1 (pr2 G)). Defined. - + Lemma syntactic_typecat_is_contextual : is_contextual syntactic_typecat. Proof. exists empty_context, isTerminal_empty_context. @@ -1026,7 +1026,7 @@ Section Contextuality. + simpl in *. admit. + admit. - Admitted. (* [syntactic_typecat_is_contextual]. Self-contained, proof-irrelevant. *) + Admitted. (* [syntactic_typecat_is_contextual]. Self-contained, proof-irrelevant. *) Definition syntactic_contextual_cat : contextual_cat := (syntactic_typecat,, syntactic_typecat_is_contextual). @@ -1110,7 +1110,7 @@ Section Misc. exists (∥ [! Γ |- a ::: A !] ∥). apply tm_expr_as_term. Defined. - + Lemma tm_transportf_tm_expr_as_term_gen {n} (Γ : wellformed_context_of_length n) {A : ty_expr n} (isd_A : ∥ [! Γ |- A !] ∥) diff --git a/TypeTheory/Instances/Presheaves.v b/TypeTheory/Instances/Presheaves.v index 20d8e012..42ff177d 100644 --- a/TypeTheory/Instances/Presheaves.v +++ b/TypeTheory/Instances/Presheaves.v @@ -105,7 +105,7 @@ Require Import UniMath.MoreFoundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import UniMath.CategoryTheory.RightKanExtension. -Require Import UniMath.CategoryTheory.categories.HSET.Limits. +Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.ElementsOp. Require Import TypeTheory.Auxiliary.Auxiliary. @@ -692,8 +692,8 @@ Proof. apply total2_neg_to_neg_forall. exists (constant_functor _ SET unitset). apply total2_neg_to_neg_forall. exists (constant_functor _ SET boolset). apply total2_neg_to_neg_forall. exists (constant_functor _ SET boolset). - eapply negf. { - eapply (isofhlevelweqf 1). + eapply negf. { + eapply (isofhlevelweqf 1). exists idtoiso. apply is_univalent_functor_category, is_univalent_HSET. } @@ -701,11 +701,11 @@ Proof. apply total2_neg_to_neg_forall. exists (identity_z_iso _). apply total2_neg_to_neg_forall. use tpair. { use constant_nat_z_iso. exists negb. - refine (MonoEpiIso.hset_equiv_is_z_iso boolset boolset negb_weq). } + refine (MonoEpiIso.hset_equiv_is_z_iso boolset boolset negb_weq). } simpl. eapply negf. { apply (maponpaths pr1). } simpl. eapply negf. { refine (maponpaths _). - refine (fun (α : nat_trans _ _) => α _). + refine (fun (α : nat_trans _ _) => α _). exists c. apply tt. } simpl. eapply negf. { apply (maponpaths (fun f => f true)). } simpl. exact nopathstruetofalse. diff --git a/TypeTheory/OtherDefs/CwF_1.v b/TypeTheory/OtherDefs/CwF_1.v index c62bd3e7..4dd55447 100644 --- a/TypeTheory/OtherDefs/CwF_1.v +++ b/TypeTheory/OtherDefs/CwF_1.v @@ -9,16 +9,16 @@ - Proof that reindexing forms a pullback The definition is based on Pitts, *Nominal Presentations of the Cubical Sets - Model of Type Theory*, Def. 3.1: + Model of Type Theory*, Def. 3.1: http://www.cl.cam.ac.uk/~amp12/papers/nompcs/nompcs.pdf (page=9) - This file is very similar to [TypeTheory.OtherDefs.CwF_Pitts]; the main difference is that here the functor of types is bundled into an actual functor, whereas in [CwF_Pitts], it is split up componentwise. + This file is very similar to [TypeTheory.OtherDefs.CwF_Pitts]; the main difference is that here the functor of types is bundled into an actual functor, whereas in [CwF_Pitts], it is split up componentwise. *) Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -44,35 +44,35 @@ Record cwf_record : Type := { Ty : functor C HSET where "C ⟨ Γ ⟩" := (Ty Γ) ; term : ∏ Γ : C, pr1hSet (Ty Γ) → UU where "C ⟨ Γ ⊢ A ⟩" := (term Γ A) ; (* rtype : ∏ {Γ Γ' : C} (A : pr1hSet (Ty Γ)) (γ : Γ' --> Γ), pr1hSetC⟨Γ'⟩ where "A [[ γ ]]" := (rtype A γ) ; *) - rterm : ∏ {Γ Γ' : C} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), + rterm : ∏ {Γ Γ' : C} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ A[[γ]]⟩ where "a ⟦ γ ⟧" := (rterm a γ) ; reindx_type_id : ∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A ; - reindx_type_comp : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), - A [[γ';;γ]] - = + reindx_type_comp : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), + A [[γ';;γ]] + = A[[γ]][[γ']] ; - reindx_term_id : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), - a⟦identity Γ⟧ + reindx_term_id : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), + a⟦identity Γ⟧ = transportf (λ B, C⟨Γ ⊢ B⟩) (! (reindx_type_id _ _)) a ; reindx_term_comp : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩), - a⟦γ';;γ⟧ + a⟦γ';;γ⟧ = transportf (λ B, C⟨Γ'' ⊢ B⟩) (!(reindx_type_comp _ _ _ )) (a⟦γ⟧⟦γ'⟧) ; comp_obj : ∏ Γ (A : C⟨Γ⟩), C where "Γ ∙ A" := (comp_obj Γ A) ; proj_mor : ∏ Γ (A : C⟨Γ⟩), Γ ∙ A --> Γ where "'π' A" := (proj_mor _ A) ; gen_element : ∏ Γ (A : C⟨Γ⟩), C⟨Γ∙A ⊢ A[[π _ ]]⟩ where "'ν' A" := (gen_element _ A) ; - pairing : ∏ Γ (A : C⟨Γ⟩) Γ' (γ : Γ' --> Γ)(a : C⟨Γ'⊢ A[[γ]]⟩), Γ' --> Γ∙A + pairing : ∏ Γ (A : C⟨Γ⟩) Γ' (γ : Γ' --> Γ)(a : C⟨Γ'⊢ A[[γ]]⟩), Γ' --> Γ∙A where "γ ♯ a" := (pairing _ _ _ γ a) ; - cwf_law_1 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩), - (γ ♯ a) ;; (π _) - = + cwf_law_1 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩), + (γ ♯ a) ;; (π _) + = γ ; cwf_law_2 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩), transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) (cwf_law_1 Γ A Γ' γ a) (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _ )(γ ♯ a) _ ) ((ν A) ⟦γ ♯ a⟧)) - = + = a }. *) @@ -83,9 +83,9 @@ End Record_Preview. (* Note: in the end, we define not pre-cwfs but cwfs, assuming an underlying _category_ with homsets. But for the “data” stages of the definition, we just take an underlying precategory. *) -(** - A [cwf] comes with types, written [C⟨Γ⟩], - and terms [C⟨Γ ⊢ A⟩] +(** + A [cwf] comes with types, written [C⟨Γ⟩], + and terms [C⟨Γ ⊢ A⟩] *) @@ -112,11 +112,11 @@ Proof. apply (# (pr1 C) γ A). Defined. -Definition reindx_structure {CC : precategory}(C : tt_structure CC) := +Definition reindx_structure {CC : precategory}(C : tt_structure CC) := (* ∑ (rtype : ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩), *) ∏ (Γ Γ' : CC) (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢rtype A γ⟩. -Definition tt_reindx_struct (CC : precategory) : UU +Definition tt_reindx_struct (CC : precategory) : UU := ∑ C : tt_structure CC, reindx_structure C. @@ -124,17 +124,17 @@ Coercion tt_from_tt_reindx CC (C : tt_reindx_struct CC) : tt_structure _ := pr1 Coercion reindx_from_tt_reindx CC (C : tt_reindx_struct CC) : reindx_structure _ := pr2 C. (* -Definition rtype {CC : precategory}{C : tt_reindx_struct CC} - : ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩ -:= +Definition rtype {CC : precategory}{C : tt_reindx_struct CC} + : ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩ +:= pr1 (pr2 C). *) Notation "A [[ γ ]]" := (rtype A γ) (at level 40). -Definition rterm {CC : precategory}{C : tt_reindx_struct CC} - : ∏ {Γ Γ' : CC} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ A [[γ]] ⟩ -:= +Definition rterm {CC : precategory}{C : tt_reindx_struct CC} + : ∏ {Γ Γ' : CC} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ A [[γ]] ⟩ +:= (pr2 C). Notation "a ⟦ γ ⟧" := (rterm a γ) (at level 40). @@ -144,7 +144,7 @@ Notation "a ⟦ γ ⟧" := (rterm a γ) (at level 40). (** Reindexing for types *) Definition reindx_laws_type {CC : precategory}(C : tt_reindx_struct CC) : UU := (∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A) × - (∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), A [[γ';;γ]] = A[[γ]][[γ']]). + (∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), A [[γ';;γ]] = A[[γ]][[γ']]). Definition reindx_laws_type_proof {CC : precategory} (C : tt_reindx_struct CC) : reindx_laws_type C. @@ -154,158 +154,158 @@ Proof. - do 5 intro. apply toforallpaths, (functor_comp (pr1 (pr1 C))). Defined. -(** Reindexing for terms needs transport along reindexing for types *) -Definition reindx_laws_terms {CC : precategory} (C : tt_reindx_struct CC) +(** Reindexing for terms needs transport along reindexing for types *) +Definition reindx_laws_terms {CC : precategory} (C : tt_reindx_struct CC) := let T:=reindx_laws_type_proof C in - (∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = + (∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = transportf (λ B, C⟨Γ ⊢ B⟩) (!pr1 T _ _) a) × (∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), - a⟦γ';;γ⟧ = + a⟦γ';;γ⟧ = transportf (λ B, C⟨Γ'' ⊢ B⟩) (!pr2 T _ _ _ _ _ _ ) (a⟦γ⟧⟦γ'⟧)). - + (** Package of reindexing for types and terms *) (* Note: in fact the reindexing laws for types are already packaged into the functor structure, so [reindx_laws] is just an alias for [reindx_laws_terms], given for consistency with other versions of CwF’s. TODO: is this useful/necessary? *) -Definition reindx_laws {CC : precategory} (C : tt_reindx_struct CC) : UU := +Definition reindx_laws {CC : precategory} (C : tt_reindx_struct CC) : UU := reindx_laws_terms C. - -Definition reindx_type_id {CC : precategory} {C : tt_reindx_struct CC} - : ∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A -:= + +Definition reindx_type_id {CC : precategory} {C : tt_reindx_struct CC} + : ∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A +:= (pr1 (reindx_laws_type_proof C)). -Definition reindx_type_comp {CC : precategory} {C : tt_reindx_struct CC} +Definition reindx_type_comp {CC : precategory} {C : tt_reindx_struct CC} (* (T : reindx_laws C) *) - {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) + {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) : A [[γ';;γ]] = A[[γ]][[γ']] := pr2 (reindx_laws_type_proof C) _ _ _ _ _ _ . Definition reindx_term_id {CC : precategory} {C : tt_reindx_struct CC} - (T : reindx_laws C) - : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = - transportf (λ B, C⟨Γ ⊢ B⟩) (! (reindx_type_id _ _ ) ) a + (T : reindx_laws C) + : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = + transportf (λ B, C⟨Γ ⊢ B⟩) (! (reindx_type_id _ _ ) ) a := pr1 T. Definition reindx_term_comp {CC : precategory} {C : tt_reindx_struct CC} - (T : reindx_laws C) + (T : reindx_laws C) : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩), - a⟦γ';;γ⟧ = - transportf (λ B, C⟨Γ'' ⊢ B⟩) (! (reindx_type_comp _ _ _ ) ) (a⟦γ⟧⟦γ'⟧) -:= + a⟦γ';;γ⟧ = + transportf (λ B, C⟨Γ'' ⊢ B⟩) (! (reindx_type_comp _ _ _ ) ) (a⟦γ⟧⟦γ'⟧) +:= (pr2 T). - + (** * Comprehension structure *) (** ** Comprehension object and projection *) -Definition comp_1_struct {CC : precategory} (C : tt_reindx_struct CC) : UU +Definition comp_1_struct {CC : precategory} (C : tt_reindx_struct CC) : UU := ∏ Γ (A : C⟨Γ⟩), ∑ ΓA, ΓA --> Γ. -Definition tt_reindx_comp_1_struct (CC : precategory) : UU - := +Definition tt_reindx_comp_1_struct (CC : precategory) : UU + := ∑ C : tt_reindx_struct CC, comp_1_struct C. -Coercion tt_reindx_from_tt_reindx_comp_1 (CC : precategory) (C : tt_reindx_comp_1_struct CC) +Coercion tt_reindx_from_tt_reindx_comp_1 (CC : precategory) (C : tt_reindx_comp_1_struct CC) : tt_reindx_struct _ := pr1 C. -Definition comp_obj {CC : precategory} {C : tt_reindx_comp_1_struct CC} (Γ : CC) (A : C⟨Γ⟩) - : CC +Definition comp_obj {CC : precategory} {C : tt_reindx_comp_1_struct CC} (Γ : CC) (A : C⟨Γ⟩) + : CC := (pr1 (pr2 C Γ A)). Notation "Γ ∙ A" := (comp_obj Γ A) (at level 35). (* \. in Adga mode *) Definition proj_mor {CC : precategory} {C : tt_reindx_comp_1_struct CC} - {Γ : CC} (A : C⟨Γ⟩) - : Γ ∙ A --> Γ + {Γ : CC} (A : C⟨Γ⟩) + : Γ ∙ A --> Γ := (pr2 (pr2 C Γ A)). Notation "'π' A" := (proj_mor A) (at level 20). (** ** Generic element and pairing *) Definition comp_2_struct {CC : precategory} (C : tt_reindx_comp_1_struct CC) : UU -:= - ∏ Γ (A : C⟨Γ⟩), - C⟨(Γ∙A) ⊢ (A [[π A]]) ⟩ × +:= + ∏ Γ (A : C⟨Γ⟩), + C⟨(Γ∙A) ⊢ (A [[π A]]) ⟩ × (∏ Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩), Γ' --> Γ∙A). -Definition tt_reindx_type_struct (CC : precategory) : UU +Definition tt_reindx_type_struct (CC : precategory) : UU := ∑ C : tt_reindx_comp_1_struct CC, comp_2_struct C. -Coercion tt_reindx_comp_1_from_tt_reindx_comp (CC : precategory) (C : tt_reindx_type_struct CC) +Coercion tt_reindx_comp_1_from_tt_reindx_comp (CC : precategory) (C : tt_reindx_type_struct CC) : tt_reindx_comp_1_struct _ := pr1 C. -Definition gen_elem {CC : precategory} {C : tt_reindx_type_struct CC} - {Γ : CC} (A : C⟨Γ⟩) - : C⟨Γ∙A ⊢ A[[π _ ]]⟩ - := +Definition gen_elem {CC : precategory} {C : tt_reindx_type_struct CC} + {Γ : CC} (A : C⟨Γ⟩) + : C⟨Γ∙A ⊢ A[[π _ ]]⟩ + := pr1 (pr2 C Γ A). Notation "'ν' A" := (gen_elem A) (at level 15). -Definition pairing {CC : precategory} {C : tt_reindx_type_struct CC} - {Γ : CC} {A : C⟨Γ⟩} {Γ'} (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩) - : Γ' --> Γ∙A +Definition pairing {CC : precategory} {C : tt_reindx_type_struct CC} + {Γ : CC} {A : C⟨Γ⟩} {Γ'} (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩) + : Γ' --> Γ∙A := pr2 (pr2 C Γ A) Γ' γ a. Notation "γ ♯ a" := (pairing γ a) (at level 25). (* \# in Adga mode *) - + (** ** Laws satisfied by the comprehension structure *) -Definition comp_laws_1_2 {CC : precategory} {C : tt_reindx_type_struct CC} - (L : reindx_laws C) : UU := +Definition comp_laws_1_2 {CC : precategory} {C : tt_reindx_type_struct CC} + (L : reindx_laws C) : UU := ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩), ∑ h : (γ ♯ a) ;; (π _ ) = γ, - transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) h + transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) h (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _ )(γ ♯ a) _ ) ((ν _ ) ⟦γ ♯ a⟧)) = a. Definition comp_law_3 {CC : precategory} {C : tt_reindx_type_struct CC} - (L : reindx_laws C) : UU -:= + (L : reindx_laws C) : UU +:= ∏ Γ (A : C ⟨Γ⟩) Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (a : C⟨Γ'⊢ A[[γ]]⟩), - γ' ;; (γ ♯ a) - = + γ' ;; (γ ♯ a) + = (γ' ;; γ) ♯ (transportf (λ B, C⟨Γ''⊢ B⟩) (!reindx_type_comp γ γ' _ ) (a⟦γ'⟧)). Definition comp_law_4 {CC : precategory} {C : tt_reindx_type_struct CC} (L : reindx_laws C) : UU := - ∏ Γ (A : C⟨Γ⟩), π A ♯ ν A = identity _ . + ∏ Γ (A : C⟨Γ⟩), π A ♯ ν A = identity _ . (* Note: the restriction now from categories to precategories is deliberate — we are insisting that cwf’s have hom-sets. *) -Definition cwf_laws {CC : category} (C : tt_reindx_type_struct CC) +Definition cwf_laws {CC : category} (C : tt_reindx_type_struct CC) := (∑ T : reindx_laws C, (comp_laws_1_2 T × comp_law_3 T × comp_law_4 T)) × - (∏ Γ (A : C⟨Γ⟩), isaset (C⟨Γ⊢ A⟩)). + (∏ Γ (A : C⟨Γ⟩), isaset (C⟨Γ⊢ A⟩)). (** * Definition of category with families *) -(** A category with families [cwf] is +(** A category with families [cwf] is - a category - - with type-and-term structure - - with reindexing + - with type-and-term structure + - with reindexing - with comprehension structure - satisfying the comprehension laws - where types and terms are hsets *) -Definition cwf_struct (CC : category) : UU +Definition cwf_struct (CC : category) : UU := ∑ C : tt_reindx_type_struct CC, cwf_laws C. (** * Various access functions to the components *) -(** Also a few generalizations are proved, providing variants with - generalized proofs of identity of types, terms (which form hsets) +(** Also a few generalizations are proved, providing variants with + generalized proofs of identity of types, terms (which form hsets) *) Coercion cwf_data_from_cwf_struct (CC : category) (C : cwf_struct CC) @@ -331,20 +331,20 @@ Definition cwf_terms_isaset {CC : category} (C : cwf_struct CC) : ∏ Γ A, isa := (pr2 (pr2 C)). -Definition cwf_law_1 {CC : category} (C : cwf_struct CC) +Definition cwf_law_1 {CC : category} (C : cwf_struct CC) Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩) : (γ ♯ a) ;; (π _) = γ := pr1 (pr1 (cwf_comp_laws C) Γ A Γ' γ a). -Definition cwf_law_2 {CC : category} (C : cwf_struct CC) +Definition cwf_law_2 {CC : category} (C : cwf_struct CC) Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩) : transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) (cwf_law_1 C Γ A Γ' γ a) - (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _)(γ ♯ a) _ ) + (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _)(γ ♯ a) _ ) ((ν A) ⟦γ ♯ a⟧)) = a := pr2 ((pr1 (cwf_comp_laws C)) Γ A Γ' γ a). -Definition cwf_law_2_gen {CC : category} (C : cwf_struct CC) +Definition cwf_law_2_gen {CC : category} (C : cwf_struct CC) Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩) : ∏ (p : (A [[π A]]) [[γ ♯ a]] = A [[γ ♯ a;; π A]]) (p0 : γ ♯ a;; π A = γ), transportf (λ ι : Γ' --> Γ, C ⟨ Γ' ⊢ A [[ι]] ⟩) p0 @@ -352,18 +352,18 @@ Definition cwf_law_2_gen {CC : category} (C : cwf_struct CC) Proof. intros p p'. etrans; [ | apply cwf_law_2]. - match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p' = p1) end. + match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p' = p1) end. { apply homset_property. } rewrite T; clear T. apply maponpaths. match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p = p1) end. { apply (cwf_types_isaset C). } rewrite T; apply idpath. -Qed. +Qed. Definition cwf_law_3 {CC : category} (C : cwf_struct CC) : comp_law_3 C := pr1 (pr2 (cwf_comp_laws C)). -Definition cwf_law_3_gen {CC : category} (C : cwf_struct CC) +Definition cwf_law_3_gen {CC : category} (C : cwf_struct CC) (Γ : CC) (A : C ⟨ Γ ⟩) (Γ' Γ'' : CC) (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (a : C ⟨ Γ' ⊢ A [[γ]] ⟩) (p : (A [[γ]]) [[γ']] = A [[γ';; γ]]): γ';; γ ♯ a = @@ -402,7 +402,7 @@ Proof. repeat (apply isofhleveldirprod). do 2 imp. apply isapropisaset. Qed. - + (** * Lemmas about CwFs, in particular that reindexing forms pullback *) @@ -413,7 +413,7 @@ Context `{C : cwf_struct CC}. Lemma map_to_comp_as_pair_cwf {Γ} {A : C⟨Γ⟩} {Γ'} (f : Γ' --> Γ∙A) : (f ;; π A) ♯ (transportb _ (reindx_type_comp _ _ _) ((gen_elem A)⟦f⟧)) - = + = f. Proof. sym. @@ -439,16 +439,16 @@ Defined. Lemma pairing_mapeq {Γ} {A : C⟨Γ⟩} {Γ'} (f f' : Γ' --> Γ) (e : f = f') (a : C ⟨ Γ' ⊢ A [[f]] ⟩) : f ♯ a - = + = f' ♯ (transportf (fun B => C⟨Γ' ⊢ B⟩ ) (maponpaths _ e) a). Proof. destruct e. apply idpath. Qed. -Lemma pairing_mapeq_gen {Γ} {Γ'} (f f' : Γ' --> Γ) {A : C⟨Γ⟩} (a : C ⟨ Γ' ⊢ A [[f]] ⟩) +Lemma pairing_mapeq_gen {Γ} {Γ'} (f f' : Γ' --> Γ) {A : C⟨Γ⟩} (a : C ⟨ Γ' ⊢ A [[f]] ⟩) (e : f = f') (p : A [[f]] = A [[f']]) : f ♯ a - = + = f' ♯ (transportf (fun B => C⟨Γ' ⊢ B⟩ ) p a). Proof. assert (T : p = (maponpaths _ e)). @@ -480,7 +480,7 @@ Proof. Qed. (* A slightly odd statement, but very often useful. - + TODO: consider naming! TODO: try to use in proofs, instead of [transport_f_f] *) Lemma term_typeeq_transport_lemma {Γ} {A A' A'': C ⟨ Γ ⟩} (e : A = A'') (e' : A' = A'') @@ -507,7 +507,7 @@ Proof. eapply pathscomp0. apply maponpaths, (reindx_term_comp C). rew_trans_@. - apply term_typeeq_transport_lemma_2. + apply term_typeeq_transport_lemma_2. apply idpath. Qed. @@ -516,7 +516,7 @@ Definition cwf_law_2' Γ (A : C ⟨ Γ ⟩) Γ' (γ : Γ' --> Γ) (a : C ⟨ Γ' : (ν A) ⟦γ ♯ a⟧ = transportf _ (reindx_type_comp _ _ _) (transportb _ (maponpaths (fun g => A[[g]]) (cwf_law_1 _ _ _ _ _ _)) - a). + a). Proof. eapply pathscomp0. 2: { apply maponpaths, maponpaths. exact (cwf_law_2 _ _ _ _ γ a). } @@ -547,7 +547,7 @@ Proof. apply gen_elem. Defined. -Definition dpr_q_cwf +Definition dpr_q_cwf {Γ} (A : C ⟨ Γ ⟩) {Γ'} (f : Γ' --> Γ) : (q_cwf A f) ;; (π A) = (π (A[[f]])) ;; f. @@ -574,13 +574,13 @@ Proof. apply idpath. Qed. -(** The biggest work is in showing that the square of dependent projections/reindexings is a pullback. +(** The biggest work is in showing that the square of dependent projections/reindexings is a pullback. -We split this up into several lemmas: +We split this up into several lemmas: -- construction of the pullback pairing function; -- proof that projections applied to the pairing recover the original maps; -- and proof that the pairing map is the unique such map. +- construction of the pullback pairing function; +- proof that projections applied to the pairing recover the original maps; +- and proof that the pairing map is the unique such map. *) @@ -607,7 +607,7 @@ Proof. 2: { apply map_to_comp_as_pair_cwf. } etrans. apply cwf_law_3. - assert ((k ♯ (dpr_q_pbpairing_cwf_aux A f h k H)) ;; (π (A [[f]]) ;; f) + assert ((k ♯ (dpr_q_pbpairing_cwf_aux A f h k H)) ;; (π (A [[f]]) ;; f) = h ;; π A) as e1. eapply pathscomp0. apply assoc. refine (_ @ !H). @@ -657,7 +657,7 @@ Proof. eapply (maponpaths (fun t => t ⟦hk⟧)). apply rterm_univ. eapply pathscomp0. - apply maponpaths, maponpaths. + apply maponpaths, maponpaths. eapply pathscomp0. symmetry. apply rterm_typeeq. apply maponpaths. @@ -675,7 +675,7 @@ Proof. eapply pathscomp0. apply transport_f_f. eapply pathscomp0. 2: { symmetry. apply transportf_rtype_mapeq. } - repeat apply term_typeeq_transport_lemma. + repeat apply term_typeeq_transport_lemma. apply term_typeeq_transport_lemma_2. apply idpath. Qed. @@ -688,13 +688,13 @@ Definition dpr_q_pbpairing_cwf_unique (hk ;; q_cwf A f = h) × (hk ;; π (A[[f]]) = k)) : t = dpr_q_pbpairing_cwf A f h k H. Proof. - destruct t as [hk [e2 e1] ]. - unshelve refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _ + destruct t as [hk [e2 e1] ]. + unshelve refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _ (dpr_q_pbpairing_cwf_mapunique A f H hk e2 e1) _). unshelve refine (total2_paths_f _ _); apply homset_property. Qed. -Lemma is_pullback_reindx_cwf : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) +Lemma is_pullback_reindx_cwf : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) (f : Γ' --> Γ), isPullback (dpr_q_cwf A f). Proof. @@ -704,5 +704,5 @@ Proof. exists (dpr_q_pbpairing_cwf _ _ h k H). apply dpr_q_pbpairing_cwf_unique. Defined. - + End CwF_lemmas. diff --git a/TypeTheory/OtherDefs/CwF_Dybjer.v b/TypeTheory/OtherDefs/CwF_Dybjer.v index 3362d8df..d09cb059 100644 --- a/TypeTheory/OtherDefs/CwF_Dybjer.v +++ b/TypeTheory/OtherDefs/CwF_Dybjer.v @@ -10,7 +10,7 @@ *) Require Import UniMath.Foundations.Sets. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.opp_precat. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -46,7 +46,7 @@ Record precwf_record : Type := { iscontr (∑ (θ : Δ --> Γ ∙ A), ∑ (e : θ ;; π A = γ), pr2 (# T θ) _ (q _ A) - = + = transportf (fun f => pr1 ((T Δ)₂ (pr1 f A))) (functor_comp T _ _ ) (transportb (fun f => pr1 ((T Δ)₂ (pr1 (# T f) A))) e diff --git a/TypeTheory/OtherDefs/CwF_Pitts.v b/TypeTheory/OtherDefs/CwF_Pitts.v index 05c7043b..cfc2e36b 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts.v +++ b/TypeTheory/OtherDefs/CwF_Pitts.v @@ -9,16 +9,16 @@ - Proof that reindexing forms a pullback The definition is based on Pitts, *Nominal Presentations of the Cubical Sets - Model of Type Theory*, Def. 3.1: + Model of Type Theory*, Def. 3.1: http://www.cl.cam.ac.uk/~amp12/papers/nompcs/nompcs.pdf (page=9) - This file is very similar to [TypeTheory.OtherDefs.CwF_1]; the main difference is that here the functor of types is split up into its separate components, whereas there it is bundled into an actual functor. + This file is very similar to [TypeTheory.OtherDefs.CwF_1]; the main difference is that here the functor of types is split up into its separate components, whereas there it is bundled into an actual functor. *) Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. @@ -43,35 +43,35 @@ Record cwf_record : Type := { type : C → UU where "C ⟨ Γ ⟩" := (type Γ) ; term : ∏ Γ : C, C⟨Γ⟩ → UU where "C ⟨ Γ ⊢ A ⟩" := (term Γ A) ; rtype : ∏ {Γ Γ' : C} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩ where "A {{ γ }}" := (rtype A γ) ; - rterm : ∏ {Γ Γ' : C} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), + rterm : ∏ {Γ Γ' : C} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ (A{{γ}})⟩ where "a ⟦ γ ⟧" := (rterm a γ) ; reindx_type_id : ∏ Γ (A : C⟨Γ⟩), A {{identity Γ}} = A ; - reindx_type_comp : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), - A {{γ';;γ}} - = + reindx_type_comp : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), + A {{γ';;γ}} + = A{{γ}}{{γ'}} ; - reindx_term_id : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), - a⟦identity Γ⟧ + reindx_term_id : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), + a⟦identity Γ⟧ = transportf (λ B, C⟨Γ ⊢ B⟩) (! (reindx_type_id _ _)) a ; reindx_term_comp : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩), - a⟦γ';;γ⟧ + a⟦γ';;γ⟧ = transportf (λ B, C⟨Γ'' ⊢ B⟩) (!(reindx_type_comp _ _ _ )) (a⟦γ⟧⟦γ'⟧) ; comp_obj : ∏ Γ (A : C⟨Γ⟩), C where "Γ ∙ A" := (comp_obj Γ A) ; proj_mor : ∏ Γ (A : C⟨Γ⟩), Γ ∙ A --> Γ where "'π' A" := (proj_mor _ A) ; gen_element : ∏ Γ (A : C⟨Γ⟩), C⟨Γ∙A ⊢ A{{π _ }}⟩ where "'ν' A" := (gen_element _ A) ; - pairing : ∏ Γ (A : C⟨Γ⟩) Γ' (γ : Γ' --> Γ)(a : C⟨Γ'⊢ A{{γ}}⟩), Γ' --> Γ∙A + pairing : ∏ Γ (A : C⟨Γ⟩) Γ' (γ : Γ' --> Γ)(a : C⟨Γ'⊢ A{{γ}}⟩), Γ' --> Γ∙A where "γ ♯ a" := (pairing _ _ _ γ a) ; - cwf_law_1 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩), - (γ ♯ a) ;; (π _) - = + cwf_law_1 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩), + (γ ♯ a) ;; (π _) + = γ ; cwf_law_2 : ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩), transportf (λ ι, C⟨Γ'⊢ A {{ι}}⟩) (cwf_law_1 Γ A Γ' γ a) (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _ )(γ ♯ a) _ ) ((ν A) ⟦γ ♯ a⟧)) - = + = a }. @@ -79,9 +79,9 @@ End Record_Preview. (** * Type and terms of a [CwF] *) -(** - A [tt_category] comes with a types, written [C⟨Γ⟩], - and terms [C⟨Γ ⊢ A⟩] +(** + A [tt_category] comes with a types, written [C⟨Γ⟩], + and terms [C⟨Γ ⊢ A⟩] *) Definition tt_structure (C : category) := @@ -100,11 +100,11 @@ Notation "C ⟨ Γ ⊢ A ⟩" := (term C Γ A) (at level 60). (** * Reindexing of types [A{{γ]] and terms [a⟦γ⟧] along a morphism [γ : Γ' --> Γ] *) -Definition reindx_structure {CC : category}(C : tt_structure CC) := +Definition reindx_structure {CC : category}(C : tt_structure CC) := ∑ (rtype : ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩), ∏ (Γ Γ' : CC) (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢rtype A γ⟩. -Definition tt_reindx_struct (CC : category) : UU +Definition tt_reindx_struct (CC : category) : UU := ∑ C : tt_structure CC, reindx_structure C. @@ -112,16 +112,16 @@ Coercion tt_from_tt_reindx CC (C : tt_reindx_struct CC) : tt_structure _ := pr1 Coercion reindx_from_tt_reindx CC (C : tt_reindx_struct CC) : reindx_structure _ := pr2 C. -Definition rtype {CC : category}{C : tt_reindx_struct CC} - : ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩ -:= +Definition rtype {CC : category}{C : tt_reindx_struct CC} + : ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩ +:= pr1 (pr2 C). Notation "A {{ γ }}" := (rtype A γ) (at level 30). -Definition rterm {CC : category}{C : tt_reindx_struct CC} - : ∏ {Γ Γ' : CC} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ A {{γ}} ⟩ -:= +Definition rterm {CC : category}{C : tt_reindx_struct CC} + : ∏ {Γ Γ' : CC} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ A {{γ}} ⟩ +:= pr2 (pr2 C). Notation "a ⟦ γ ⟧" := (rterm a γ) (at level 40). @@ -131,160 +131,160 @@ Notation "a ⟦ γ ⟧" := (rterm a γ) (at level 40). (** Reindexing for types *) Definition reindx_laws_type {CC : category}(C : tt_reindx_struct CC) : UU := (∏ Γ (A : C⟨Γ⟩), A {{identity Γ}} = A) × - (∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), A {{γ';;γ}} = A{{γ}}{{γ'}}). + (∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), A {{γ';;γ}} = A{{γ}}{{γ'}}). -(** Reindexing for terms needs transport along reindexing for types *) -Definition reindx_laws_terms {CC : category} {C : tt_reindx_struct CC} +(** Reindexing for terms needs transport along reindexing for types *) +Definition reindx_laws_terms {CC : category} {C : tt_reindx_struct CC} (T : reindx_laws_type C) := - (∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = + (∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = transportf (λ B, C⟨Γ ⊢ B⟩) (!pr1 T _ _) a) × (∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), - a⟦γ';;γ⟧ = + a⟦γ';;γ⟧ = transportf (λ B, C⟨Γ'' ⊢ B⟩) (!pr2 T _ _ _ _ _ _ ) (a⟦γ⟧⟦γ'⟧)). - + (** Package of reindexing for types and terms *) -Definition reindx_laws {CC : category} (C : tt_reindx_struct CC) : UU := +Definition reindx_laws {CC : category} (C : tt_reindx_struct CC) : UU := ∑ T : reindx_laws_type C, reindx_laws_terms T. - -Definition reindx_type_id {CC : category} {C : tt_reindx_struct CC} + +Definition reindx_type_id {CC : category} {C : tt_reindx_struct CC} (T : reindx_laws C) - : ∏ Γ (A : C⟨Γ⟩), A {{identity Γ}} = A -:= + : ∏ Γ (A : C⟨Γ⟩), A {{identity Γ}} = A +:= pr1 (pr1 T). -Definition reindx_type_comp {CC : category} {C : tt_reindx_struct CC} - (T : reindx_laws C) - {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) - : A {{γ';;γ}} = A{{γ}}{{γ'}} +Definition reindx_type_comp {CC : category} {C : tt_reindx_struct CC} + (T : reindx_laws C) + {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) + : A {{γ';;γ}} = A{{γ}}{{γ'}} := pr2 (pr1 T) _ _ _ _ _ _ . Definition reindx_term_id {CC : category} {C : tt_reindx_struct CC} - (T : reindx_laws C) - : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = - transportf (λ B, C⟨Γ ⊢ B⟩) (!pr1 (pr1 T) _ _) a + (T : reindx_laws C) + : ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ = + transportf (λ B, C⟨Γ ⊢ B⟩) (!pr1 (pr1 T) _ _) a := pr1 (pr2 T). Definition reindx_term_comp {CC : category} {C : tt_reindx_struct CC} - (T : reindx_laws C) + (T : reindx_laws C) : ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩), - a⟦γ';;γ⟧ = - transportf (λ B, C⟨Γ'' ⊢ B⟩) (!pr2 (pr1 T) _ _ _ _ _ _ ) (a⟦γ⟧⟦γ'⟧) -:= + a⟦γ';;γ⟧ = + transportf (λ B, C⟨Γ'' ⊢ B⟩) (!pr2 (pr1 T) _ _ _ _ _ _ ) (a⟦γ⟧⟦γ'⟧) +:= pr2 (pr2 T). - + (** * Comprehension structure *) (** ** Comprehension object and projection *) -Definition comp_1_struct {CC : category} (C : tt_reindx_struct CC) : UU +Definition comp_1_struct {CC : category} (C : tt_reindx_struct CC) : UU := ∏ Γ (A : C⟨Γ⟩), ∑ ΓA, ΓA --> Γ. -Definition tt_reindx_comp_1_struct (CC : category) : UU - := +Definition tt_reindx_comp_1_struct (CC : category) : UU + := ∑ C : tt_reindx_struct CC, comp_1_struct C. -Coercion tt_reindx_from_tt_reindx_comp_1 (CC : category) (C : tt_reindx_comp_1_struct CC) +Coercion tt_reindx_from_tt_reindx_comp_1 (CC : category) (C : tt_reindx_comp_1_struct CC) : tt_reindx_struct _ := pr1 C. -Definition comp_obj {CC : category} {C : tt_reindx_comp_1_struct CC} (Γ : CC) (A : C⟨Γ⟩) - : CC +Definition comp_obj {CC : category} {C : tt_reindx_comp_1_struct CC} (Γ : CC) (A : C⟨Γ⟩) + : CC := (pr1 (pr2 C Γ A)). Notation "Γ ∙ A" := (comp_obj Γ A) (at level 35). (* \. in Adga mode *) Definition proj_mor {CC : category} {C : tt_reindx_comp_1_struct CC} - {Γ : CC} (A : C⟨Γ⟩) - : Γ ∙ A --> Γ + {Γ : CC} (A : C⟨Γ⟩) + : Γ ∙ A --> Γ := (pr2 (pr2 C Γ A)). Notation "'π' A" := (proj_mor A) (at level 20). (** ** Generic element and pairing *) Definition comp_2_struct {CC : category} (C : tt_reindx_comp_1_struct CC) : UU -:= - ∏ Γ (A : C⟨Γ⟩), - C⟨(Γ∙A) ⊢ (A {{π A}}) ⟩ × +:= + ∏ Γ (A : C⟨Γ⟩), + C⟨(Γ∙A) ⊢ (A {{π A}}) ⟩ × (∏ Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢A{{γ}}⟩), Γ' --> Γ∙A). -Definition tt_reindx_type_struct (CC : category) : UU +Definition tt_reindx_type_struct (CC : category) : UU := ∑ C : tt_reindx_comp_1_struct CC, comp_2_struct C. -Coercion tt_reindx_comp_1_from_tt_reindx_comp (CC : category) (C : tt_reindx_type_struct CC) +Coercion tt_reindx_comp_1_from_tt_reindx_comp (CC : category) (C : tt_reindx_type_struct CC) : tt_reindx_comp_1_struct _ := pr1 C. -Definition gen_elem {CC : category} {C : tt_reindx_type_struct CC} - {Γ : CC} (A : C⟨Γ⟩) - : C⟨Γ∙A ⊢ A{{π _ }}⟩ - := +Definition gen_elem {CC : category} {C : tt_reindx_type_struct CC} + {Γ : CC} (A : C⟨Γ⟩) + : C⟨Γ∙A ⊢ A{{π _ }}⟩ + := pr1 (pr2 C Γ A). Notation "'ν' A" := (gen_elem A) (at level 15). -Definition pairing {CC : category} {C : tt_reindx_type_struct CC} - {Γ : CC} {A : C⟨Γ⟩} {Γ'} (γ : Γ' --> Γ) (a : C⟨Γ'⊢A{{γ}}⟩) - : Γ' --> Γ∙A +Definition pairing {CC : category} {C : tt_reindx_type_struct CC} + {Γ : CC} {A : C⟨Γ⟩} {Γ'} (γ : Γ' --> Γ) (a : C⟨Γ'⊢A{{γ}}⟩) + : Γ' --> Γ∙A := pr2 (pr2 C Γ A) Γ' γ a. Notation "γ ♯ a" := (pairing γ a) (at level 25). (* \# in Adga mode *) - + (** ** Laws satisfied by the comprehension structure *) -Definition comp_laws_1_2 {CC : category} {C : tt_reindx_type_struct CC} - (L : reindx_laws C) : UU := +Definition comp_laws_1_2 {CC : category} {C : tt_reindx_type_struct CC} + (L : reindx_laws C) : UU := ∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩), ∑ h : (γ ♯ a) ;; (π _ ) = γ, - transportf (λ ι, C⟨Γ'⊢ A {{ι}}⟩) h + transportf (λ ι, C⟨Γ'⊢ A {{ι}}⟩) h (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp L (π _ )(γ ♯ a) _ ) ((ν _ ) ⟦γ ♯ a⟧)) = a. Definition comp_law_3 {CC : category} {C : tt_reindx_type_struct CC} - (L : reindx_laws C) : UU -:= + (L : reindx_laws C) : UU +:= ∏ Γ (A : C ⟨Γ⟩) Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (a : C⟨Γ'⊢ A{{γ}}⟩), - γ' ;; (γ ♯ a) - = + γ' ;; (γ ♯ a) + = (γ' ;; γ) ♯ (transportf (λ B, C⟨Γ''⊢ B⟩) (!reindx_type_comp L γ γ' _ ) (a⟦γ'⟧)). Definition comp_law_4 {CC : category} {C : tt_reindx_type_struct CC} (L : reindx_laws C) : UU := - ∏ Γ (A : C⟨Γ⟩), π A ♯ ν A = identity _ . + ∏ Γ (A : C⟨Γ⟩), π A ♯ ν A = identity _ . -Definition cwf_laws {CC : category} (C : tt_reindx_type_struct CC) +Definition cwf_laws {CC : category} (C : tt_reindx_type_struct CC) := (∑ T : reindx_laws C, (comp_laws_1_2 T × comp_law_3 T × comp_law_4 T)) × (∏ Γ, isaset (C⟨Γ⟩)) - × ∏ Γ (A : C⟨Γ⟩), isaset (C⟨Γ⊢ A⟩). + × ∏ Γ (A : C⟨Γ⟩), isaset (C⟨Γ⊢ A⟩). (** * Definition of category with families *) -(** A category with families [cwf] is +(** A category with families [cwf] is - a category - - with type-and-term structure - - with reindexing + - with type-and-term structure + - with reindexing - with comprehension structure - satisfying the comprehension laws - where types and terms are hsets *) -Definition cwf_struct (CC : category) : UU +Definition cwf_struct (CC : category) : UU := ∑ C : tt_reindx_type_struct CC, cwf_laws C. (** * Various access functions to the components *) -(** Also a few generalizations are proved, providing variants with - generalized proofs of identity of types, terms (which form hsets) +(** Also a few generalizations are proved, providing variants with + generalized proofs of identity of types, terms (which form hsets) *) Coercion cwf_data_from_cwf_struct (CC : category) (C : cwf_struct CC) : _ CC := pr1 C. @@ -307,20 +307,20 @@ Definition cwf_terms_isaset {CC : category} (C : cwf_struct CC) : ∏ Γ A, isa := pr2 (pr2 (pr2 C)). -Definition cwf_law_1 {CC : category} (C : cwf_struct CC) +Definition cwf_law_1 {CC : category} (C : cwf_struct CC) Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩) : (γ ♯ a) ;; (π _) = γ := pr1 (pr1 (cwf_comp_laws C) Γ A Γ' γ a). -Definition cwf_law_2 {CC : category} (C : cwf_struct CC) +Definition cwf_law_2 {CC : category} (C : cwf_struct CC) Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩) : transportf (λ ι, C⟨Γ'⊢ A {{ι}}⟩) (cwf_law_1 C Γ A Γ' γ a) - (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp C (π _)(γ ♯ a) _ ) + (transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp C (π _)(γ ♯ a) _ ) ((ν A) ⟦γ ♯ a⟧)) = a := pr2 ((pr1 (cwf_comp_laws C)) Γ A Γ' γ a). -Definition cwf_law_2_gen {CC : category} (C : cwf_struct CC) +Definition cwf_law_2_gen {CC : category} (C : cwf_struct CC) Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A{{γ}}⟩) : ∏ (p : (A {{π A}}) {{γ ♯ a}} = A {{γ ♯ a;; π A}}) (p0 : γ ♯ a;; π A = γ), transportf (λ ι : Γ' --> Γ, C ⟨ Γ' ⊢ A {{ι}} ⟩) p0 @@ -328,18 +328,18 @@ Definition cwf_law_2_gen {CC : category} (C : cwf_struct CC) Proof. intros p p'. etrans; [ | apply cwf_law_2]. - match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p' = p1) end. + match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p' = p1) end. { apply homset_property. } rewrite T; clear T. apply maponpaths. match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p = p1) end. { apply (cwf_types_isaset C). } rewrite T; apply idpath. -Qed. +Qed. Definition cwf_law_3 {CC : category} (C : cwf_struct CC) : comp_law_3 C := pr1 (pr2 (cwf_comp_laws C)). -Definition cwf_law_3_gen {CC : category} (C : cwf_struct CC) +Definition cwf_law_3_gen {CC : category} (C : cwf_struct CC) (Γ : CC) (A : C ⟨ Γ ⟩) (Γ' Γ'' : CC) (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (a : C ⟨ Γ' ⊢ A {{γ}} ⟩) (p : (A {{γ}}) {{γ'}} = A {{γ';; γ}}): γ';; γ ♯ a = @@ -377,7 +377,7 @@ Proof. do 6 imp. apply (cwf_types_isaset X). } * intros. - { + { apply isofhleveltotal2. - do 3 imp. apply (cwf_terms_isaset X). @@ -400,7 +400,7 @@ Proof. + do 1 imp. apply isapropisaset. + do 2 imp. apply isapropisaset. Qed. - + (** * Lemmas about CwFs, in particular that reindexing forms pullback *) Section CwF_lemmas. @@ -410,7 +410,7 @@ Context `{C : cwf_struct CC}. Lemma map_to_comp_as_pair_cwf {Γ} {A : C⟨Γ⟩} {Γ'} (f : Γ' --> Γ∙A) : (f ;; π A) ♯ (transportb _ (reindx_type_comp C _ _ _) ((gen_elem A)⟦f⟧)) - = + = f. Proof. sym. @@ -436,16 +436,16 @@ Defined. Lemma pairing_mapeq {Γ} {A : C⟨Γ⟩} {Γ'} (f f' : Γ' --> Γ) (e : f = f') (a : C ⟨ Γ' ⊢ A {{f}} ⟩) : f ♯ a - = + = f' ♯ (transportf (fun B => C⟨Γ' ⊢ B⟩ ) (maponpaths _ e) a). Proof. destruct e. apply idpath. Qed. -Lemma pairing_mapeq_gen {Γ} {Γ'} (f f' : Γ' --> Γ) {A : C⟨Γ⟩} (a : C ⟨ Γ' ⊢ A {{f}} ⟩) +Lemma pairing_mapeq_gen {Γ} {Γ'} (f f' : Γ' --> Γ) {A : C⟨Γ⟩} (a : C ⟨ Γ' ⊢ A {{f}} ⟩) (e : f = f') (p : A {{f}} = A {{f'}}) : f ♯ a - = + = f' ♯ (transportf (fun B => C⟨Γ' ⊢ B⟩ ) p a). Proof. assert (T : p = (maponpaths _ e)). @@ -477,7 +477,7 @@ Proof. Qed. (* A slightly odd statement, but very often useful. - + TODO: consider naming! TODO: try to use in proofs, instead of [transport_f_f] *) Lemma term_typeeq_transport_lemma {Γ} {A A' A'': C ⟨ Γ ⟩} (e : A = A'') (e' : A' = A'') @@ -504,7 +504,7 @@ Proof. eapply pathscomp0. apply maponpaths, (reindx_term_comp C). rew_trans_@. - apply term_typeeq_transport_lemma_2. + apply term_typeeq_transport_lemma_2. apply idpath. Qed. @@ -513,14 +513,14 @@ Definition cwf_law_2' Γ (A : C ⟨ Γ ⟩) Γ' (γ : Γ' --> Γ) (a : C ⟨ Γ' : (ν A) ⟦γ ♯ a⟧ = transportf _ (reindx_type_comp C _ _ _) (transportb _ (maponpaths (fun g => A{{g}}) (cwf_law_1 _ _ _ _ _ _)) - a). + a). Proof. eapply pathscomp0. 2: { apply maponpaths, maponpaths. exact (cwf_law_2 _ _ _ _ γ a). } apply pathsinv0. rew_trans_@. etrans. apply maponpaths, transportf_rtype_mapeq. - rew_trans_@. + rew_trans_@. (* TODO: try simplyfying with [term_typeeq_transport_lemma] *) refine (@maponpaths _ _ (fun e => transportf _ e _) _ (idpath _) _). apply cwf_types_isaset. @@ -544,7 +544,7 @@ Proof. apply gen_elem. Defined. -Definition dpr_q_cwf +Definition dpr_q_cwf {Γ} (A : C ⟨ Γ ⟩) {Γ'} (f : Γ' --> Γ) : (q_cwf A f) ;; (π A) = (π (A{{f}})) ;; f. @@ -571,13 +571,13 @@ Proof. apply idpath. Qed. -(** The biggest work is in showing that the square of dependent projections/reindexings is a pullback. +(** The biggest work is in showing that the square of dependent projections/reindexings is a pullback. -We split this up into several lemmas: +We split this up into several lemmas: -- construction of the pullback pairing function; -- proof that projections applied to the pairing recover the original maps; -- and proof that the pairing map is the unique such map. +- construction of the pullback pairing function; +- proof that projections applied to the pairing recover the original maps; +- and proof that the pairing map is the unique such map. *) @@ -604,7 +604,7 @@ Proof. 2: { apply map_to_comp_as_pair_cwf. } etrans. { apply cwf_law_3. } - assert ((k ♯ (dpr_q_pbpairing_cwf_aux A f h k H)) ;; (π (A {{f}}) ;; f) + assert ((k ♯ (dpr_q_pbpairing_cwf_aux A f h k H)) ;; (π (A {{f}}) ;; f) = h ;; π A) as e1. eapply pathscomp0. apply assoc. refine (_ @ !H). @@ -651,11 +651,11 @@ Proof. apply (pairing_mapeq _ _ e1 _). simpl. apply maponpaths. eapply pathscomp0. - apply maponpaths, maponpaths. + apply maponpaths, maponpaths. apply (@maponpaths (C ⟨ Γ' ∙ (A{{f}}) ⊢ A{{f}}{{π (A{{f}})}} ⟩) _ (fun t => t ⟦hk⟧)). apply rterm_univ. eapply pathscomp0. - apply maponpaths, maponpaths. + apply maponpaths, maponpaths. eapply pathscomp0. symmetry. apply rterm_typeeq. apply maponpaths. @@ -673,7 +673,7 @@ Proof. eapply pathscomp0. apply transport_f_f. eapply pathscomp0. 2: { symmetry. apply transportf_rtype_mapeq. } - repeat apply term_typeeq_transport_lemma. + repeat apply term_typeeq_transport_lemma. apply term_typeeq_transport_lemma_2. apply idpath. Qed. @@ -686,13 +686,13 @@ Definition dpr_q_pbpairing_cwf_unique (hk ;; q_cwf A f = h) × (hk ;; π (A{{f}}) = k)) : t = dpr_q_pbpairing_cwf A f h k H. Proof. - destruct t as [hk [e2 e1]]. - refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _ + destruct t as [hk [e2 e1]]. + refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _ (dpr_q_pbpairing_cwf_mapunique A f H hk e2 e1) _). unshelve refine (total2_paths_f _ _); apply homset_property. Qed. -Lemma is_pullback_reindx_cwf : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) +Lemma is_pullback_reindx_cwf : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC) (f : Γ' --> Γ), isPullback (dpr_q_cwf A f). Proof. @@ -702,5 +702,5 @@ Proof. exists (dpr_q_pbpairing_cwf _ _ h k H). apply dpr_q_pbpairing_cwf_unique. Defined. - + End CwF_lemmas. diff --git a/TypeTheory/OtherDefs/CwF_Pitts_completion.v b/TypeTheory/OtherDefs/CwF_Pitts_completion.v index 33b9f0c8..06334a7f 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_completion.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_completion.v @@ -11,8 +11,8 @@ Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.rezk_completion. Require Import UniMath.CategoryTheory.opp_precat. -Require Import UniMath.CategoryTheory.categories.HSET.Core. -Require Import UniMath.CategoryTheory.categories.HSET.Univalence. +Require Import UniMath.CategoryTheory.Categories.HSET.Core. +Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -24,8 +24,8 @@ Local Arguments iso: clear implicits. (** How to get a functor from RC(C) to D when having one from C to D **) -Definition Rezk_functor (C : category) (D : univalent_category) - (F : functor C D) +Definition Rezk_functor (C : category) (D : univalent_category) + (F : functor C D) : functor (Rezk_completion C) D. Proof. set (H:=Rezk_eta_Universal_Property C D (pr2 D)). @@ -45,18 +45,18 @@ Context (CC : category) (C : cwf_struct CC). We thus obtain a "type" functor on RC(C) by univ property **) -Definition type_hSet (Γ : CC) : hSet := make_hSet (C⟨Γ⟩) (cwf_types_isaset _ _ ). +Definition type_hSet (Γ : CC) : hSet := make_hSet (C⟨Γ⟩) (cwf_types_isaset _ _ ). Definition type_functor_data : functor_data CC (opp_precat HSET). Proof. exists type_hSet. intros Γ Γ' γ A. exact (rtype A γ). Defined. - + Definition type_is_functor : is_functor type_functor_data. Proof. split; intros; simpl. - - intros Γ. apply funextfun; intro A. apply reindx_type_id. + - intros Γ. apply funextfun; intro A. apply reindx_type_id. apply reindx_laws_from_cwf_struct. - intros Γ Γ' Γ'' f g. apply funextfun; intro A. apply reindx_type_comp. @@ -66,11 +66,11 @@ Qed. Definition type_functor : functor _ _ := tpair _ _ type_is_functor. Definition RC_type_functor : functor (Rezk_completion CC) (opp_precat HSET). -Proof. +Proof. apply (Rezk_functor CC (op_unicat HSET_univalent_category)). apply type_functor. Defined. - + (** ** The "term" part of a CwF **) (** The "term" part is a functor from the category of elements of "type" into (the opposite of) sets. diff --git a/TypeTheory/OtherDefs/CwF_Pitts_natural.v b/TypeTheory/OtherDefs/CwF_Pitts_natural.v index 9e9b6826..567be067 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_natural.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_natural.v @@ -9,7 +9,7 @@ - Proof that reindexing forms a pullback The definition is based on Pitts, *Nominal Presentations of the Cubical Sets - Model of Type Theory*, Def. 3.1: + Model of Type Theory*, Def. 3.1: http://www.cl.cam.ac.uk/~amp12/papers/nompcs/nompcs.pdf (page=9) *) @@ -18,8 +18,8 @@ Require Import UniMath.Foundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import UniMath.CategoryTheory.FunctorCategory. -Require Import UniMath.CategoryTheory.categories.HSET.All. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Categories.HSET.All. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. Require Import TypeTheory.Auxiliary.SetsAndPresheaves. @@ -29,7 +29,7 @@ Local Open Scope precat. (** * A "preview" of the definition *) Module Preview. - + Variable C : category. Variable Ty Tm: [C^op, HSET]. (* functor C^op HSET. *) Variable p : _ ⟦Tm, Ty⟧. (* needs to be written as mor in a precat *) @@ -57,7 +57,7 @@ Variable comp_comm : yoTm _ (q Γ A) ;; p = #(yoneda _ ) (pi Γ A) ;; yoTy _ A. -Variable ispullback_comp_comm : +Variable ispullback_comp_comm : forall Γ (A : Ty $p Γ), isPullback (comp_comm Γ A). @@ -77,49 +77,49 @@ Definition p (X : tt_structure) : _ ⟦Tm X, Ty X⟧ := pr2 X. Definition comp_structure (X : tt_structure) : UU := forall Γ (A : Ty X $p Γ), - ∑ (comp : C) (pi : _ ⟦comp, Γ⟧), + ∑ (comp : C) (pi : _ ⟦comp, Γ⟧), Tm X $p comp. -Definition comp {X : tt_structure} (Y : comp_structure X) : +Definition comp {X : tt_structure} (Y : comp_structure X) : forall (Γ : C) (A : Ty X $p Γ), C := fun Γ A => pr1 (Y Γ A). -Definition pi {X : tt_structure} (Y : comp_structure X) : +Definition pi {X : tt_structure} (Y : comp_structure X) : forall (Γ : C) (A : Ty X $p Γ), comp _ Γ A --> Γ := fun Γ A => pr1 (pr2 (Y Γ A)). -Definition q {X : tt_structure} (Y : comp_structure X) : - forall (Γ : C) (A : Ty X $p Γ), Tm X $p (comp Y Γ A) +Definition q {X : tt_structure} (Y : comp_structure X) : + forall (Γ : C) (A : Ty X $p Γ), Tm X $p (comp Y Γ A) := fun Γ A => pr2 (pr2 (Y Γ A)). Definition pullback_structure {X : tt_structure} (Y : comp_structure X) : UU := forall Γ (A : Ty X $p Γ), - ∑ H : - invmap (yoneda_weq C _ (Tm X)) (q Y Γ A) ;; p X + ∑ H : + invmap (yoneda_weq C _ (Tm X)) (q Y Γ A) ;; p X = - #(yoneda _ ) (pi Y Γ A) ;; invmap (yoneda_weq _ _ (Ty X)) A , + #(yoneda _ ) (pi Y Γ A) ;; invmap (yoneda_weq _ _ (Ty X)) A , isPullback(C:=[(C^op), SET]) H. -Definition comp_comm {X : tt_structure } {Y : comp_structure X} (Z : pullback_structure Y) +Definition comp_comm {X : tt_structure } {Y : comp_structure X} (Z : pullback_structure Y) : forall Γ (A : Ty X $p Γ), - invmap (yoneda_weq _ _ (Tm X)) (q Y Γ A) ;; p X + invmap (yoneda_weq _ _ (Tm X)) (q Y Γ A) ;; p X = #(yoneda _ ) (pi Y Γ A) ;; invmap (yoneda_weq _ _ (Ty X)) A := fun Γ A => pr1 (Z Γ A). -Definition is_Pullback_comp {X : tt_structure } {Y : comp_structure X} (Z : pullback_structure Y) +Definition is_Pullback_comp {X : tt_structure } {Y : comp_structure X} (Z : pullback_structure Y) : forall Γ (A : Ty X $p Γ), isPullback(C:=[(C^op), SET]) (comp_comm Z _ _ ) := fun Γ A => pr2 (Z Γ A). -Definition is_natural_CwF : UU +Definition is_natural_CwF : UU := ∑ (X : tt_structure) (Y : comp_structure X), pullback_structure Y. Coercion tt_structure_from_is_natural_CwF (X : is_natural_CwF) : tt_structure := pr1 X. -Coercion comp_structure_from_is_natural_CwF (X : is_natural_CwF) : +Coercion comp_structure_from_is_natural_CwF (X : is_natural_CwF) : comp_structure (tt_structure_from_is_natural_CwF X) := pr1 (pr2 X). -Coercion pullback_structure_from_is_natural_CwF (X : is_natural_CwF) : +Coercion pullback_structure_from_is_natural_CwF (X : is_natural_CwF) : pullback_structure (comp_structure_from_is_natural_CwF X) := pr2 (pr2 X). - + End definition. diff --git a/TypeTheory/OtherDefs/CwF_Pitts_to_CwF_1.v b/TypeTheory/OtherDefs/CwF_Pitts_to_CwF_1.v index 9e018ddc..09bcee50 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_to_CwF_1.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_to_CwF_1.v @@ -9,13 +9,13 @@ - Proof that reindexing forms a pullback The definition is based on Pitts, *Nominal Presentations of the Cubical Sets - Model of Type Theory*, Def. 3.1: + Model of Type Theory*, Def. 3.1: http://www.cl.cam.ac.uk/~amp12/papers/nompcs/nompcs.pdf (page=9) *) Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -27,11 +27,11 @@ Require Import TypeTheory.OtherDefs.CwF_1. Local Open Scope precat. Section fix_a_precategory. - + Variable C : category. Section CwF_1_from_CwF. - + Variable CC : CwF_Pitts.cwf_struct C. Definition type_functor : functor C^op HSET. @@ -55,7 +55,7 @@ Section fix_a_precategory. Defined. Definition CwF_1_data_from_CwF : CwF_1.tt_reindx_type_struct C. - Proof. + Proof. use tpair; [use tpair; [use tpair; [use tpair|]|]|]. - apply type_functor. - simpl. intros Γ A. apply (CwF_Pitts.term CC Γ A). @@ -116,7 +116,7 @@ Section fix_a_precategory. simpl in *. apply CwF_Pitts.cwf_law_4. Defined. - + Definition CwF_1_from_CwF : CwF_1.cwf_struct C. Proof. exists CwF_1_data_from_CwF. @@ -188,7 +188,7 @@ Section fix_a_precategory. simpl in A. apply CwF_1.cwf_law_4. Defined. - + Definition CwF_from_CwF_1 : CwF_Pitts.cwf_struct C. Proof. exists CwF_data_from_CwF_1. @@ -197,7 +197,7 @@ Section fix_a_precategory. End CwF_from_CwF_1. - + Lemma CwF_1_to_CwF_to_CwF_1 (CC : CwF_1.cwf_struct C) : CwF_1_from_CwF (CwF_from_CwF_1 CC) = CC. Proof. diff --git a/TypeTheory/OtherDefs/CwF_Pitts_to_DM.v b/TypeTheory/OtherDefs/CwF_Pitts_to_DM.v index 56f558f7..e4f5d842 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_to_DM.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_to_DM.v @@ -1,5 +1,5 @@ -(** +(** Ahrens, Lumsdaine, Voevodsky, 2015 @@ -13,7 +13,7 @@ Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. @@ -26,7 +26,7 @@ Require Import TypeTheory.OtherDefs.CwF_Pitts. Require Import TypeTheory.OtherDefs.DM. (* Locally override the notation [ γ ♯ a ], at a higher level, - to get more informative bracketing when pairing meets composition. *) + to get more informative bracketing when pairing meets composition. *) Local Notation "γ ## a" := (pairing γ a) (at level 75). (** * Category with DM from Category with families @@ -97,7 +97,7 @@ Proof. - unshelve refine (make_Pullback _ _). 5: use postcomp_pb_with_z_iso. 7: eapply is_pullback_reindx_cwf. - + eassumption. + + eassumption. + sym. assumption. - simpl. apply hinhpr. diff --git a/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat.v b/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat.v index f134caea..1bb87ad0 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat.v @@ -1,6 +1,6 @@ -(** - +(** + Ahrens, Lumsdaine, Voevodsky, 2015 Contents: @@ -11,7 +11,7 @@ Contents: *) -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. @@ -24,7 +24,7 @@ Require Import TypeTheory.TypeCat.TypeCat. Require Import TypeTheory.OtherDefs.CwF_Pitts. (* Locally override the notation [ γ ♯ a ], at a higher level, - to get more informative bracketing when pairing meets composition. *) + to get more informative bracketing when pairing meets composition. *) Local Notation "γ ## a" := (pairing γ a) (at level 75). (** * Type-cat from cat with Families *) @@ -44,7 +44,7 @@ Definition type_cat1_of_cwf : typecat_structure1 CC. Proof. unfold typecat_structure1. exists (type C). - exists (comp_obj ). + exists (comp_obj ). exact (fun Γ a Γ' f => a{{f}}). Defined. @@ -69,12 +69,12 @@ Definition issplit_type_cat_of_cwf : is_split_typecat type_cat_of_cwf. Proof. unfold is_split_typecat. - repeat split. + repeat split. - (* Types over each object form a set *) apply cwf_types_isaset. - (* Reindexing along identities *) exists (reindx_type_id C). - intros Γ A. + intros Γ A. unfold q_typecat; simpl. unfold q_cwf. eapply pathscomp0. 2: { apply id_left. } eapply pathscomp0. 2: apply maponpaths_2. @@ -91,15 +91,15 @@ Proof. - (* Reindexing along composites *) exists (fun Γ A Γ' f Γ'' g => reindx_type_comp C f g A). intros Γ A Γ' f Γ'' g. - unfold q_typecat. simpl. + unfold q_typecat. simpl. eapply pathscomp0. 2: { apply id_left. } rewrite 2 assoc. unfold ext_typecat. simpl. rewrite <- cwf_law_4. rewrite pairing_transport. - unfold q_cwf. + unfold q_cwf. rewrite cwf_law_3. - match goal with [|- pairing ?b _ = pairing ?e _ ] => + match goal with [|- pairing ?b _ = pairing ?e _ ] => set (X := b); set (X' := e) end. etrans. + refine (pairing_mapeq _ X' _ _ ). diff --git a/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat_to_DM.v b/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat_to_DM.v index 1ac8615b..3fc96c1a 100644 --- a/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat_to_DM.v +++ b/TypeTheory/OtherDefs/CwF_Pitts_to_TypeCat_to_DM.v @@ -1,6 +1,6 @@ -(** - +(** + Ahrens, Lumsdaine, Voevodsky, 2015 Contents: @@ -13,7 +13,7 @@ Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.TypeCat.TypeCat. Require Import TypeTheory.OtherDefs.CwF_Pitts. @@ -38,5 +38,5 @@ Section compare_maps. apply X. - intros. apply X. Defined. - + End compare_maps. diff --git a/TypeTheory/OtherDefs/DM.v b/TypeTheory/OtherDefs/DM.v index f7701b72..271f1564 100644 --- a/TypeTheory/OtherDefs/DM.v +++ b/TypeTheory/OtherDefs/DM.v @@ -16,7 +16,7 @@ Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -31,7 +31,7 @@ Reserved Notation "γ ⋆ f" (at level 25). -(** these are approximations of the access functions implemented at the end of the file +(** these are approximations of the access functions implemented at the end of the file one difference is that actually DM is defined as the sigma type of another type @@ -103,7 +103,7 @@ Coercion arrow_from_DM {C : precategory} (H : dm_sub_struct C)(Δ Γ : C) (δ : Definition dm_sub_closed_under_iso {CC : precategory} (C : dm_sub_struct CC) : UU := ∏ Δ Γ (γ : DM C Δ Γ), - ∏ Δ' (δ : Δ' --> Γ), + ∏ Δ' (δ : Δ' --> Γ), ∏ (h : z_iso Δ Δ'), h ;; δ = γ → DM_type C δ. @@ -118,7 +118,7 @@ Definition dm_sub_closed_under_iso {CC : precategory} (C : dm_sub_struct CC) | | | | γ ∈ DM |____f_____|Γ' - Δ + Δ ]] @@ -143,7 +143,7 @@ Definition pb_ob_of_DM {CC : category} {C : dm_sub_pb CC} Notation "γ ⋆ f" := (pb_ob_of_DM γ f) (at level 45, format "γ ⋆ f"). (* written "\st" in Agda input mode *) - + Definition pb_mor_of_DM {CC : category} {C : dm_sub_pb CC} {Δ Γ} (γ : DM C Δ Γ) {Γ'} (f : Γ' --> Γ) : (γ⋆f) --> Γ'. @@ -160,7 +160,7 @@ Defined. Definition sqr_comm_of_dm_sub_pb {CC : category} {C : dm_sub_pb CC} {Δ Γ} (γ : DM C Δ Γ) {Γ'} (f : Γ' --> Γ) -: _ ;; _ = _ ;; _ +: _ ;; _ = _ ;; _ := PullbackSqrCommutes (pr1 (pr2 C _ _ γ _ f )). Definition isPullback_of_dm_sub_pb {CC : category} {C : dm_sub_pb CC} @@ -186,13 +186,13 @@ Definition pb_DM_of_DM {CC} {C : dm_sub_pb CC} {Δ Γ} (γ : DM C Δ Γ) {Γ'} : DM C (γ⋆f) Γ'. Proof. exists (pb_mor_of_DM γ f). - apply (pr2 (pr2 C _ _ γ _ f)). + apply (pr2 (pr2 C _ _ γ _ f)). Defined. Definition pb_DM_over_of_DM_over {CC} {C : dm_sub_pb CC} {Γ} (γ : DM_over C Γ) {Γ'} (f : Γ' --> Γ) : DM_over C Γ'. Proof. - eapply DM_over_from_DM. + eapply DM_over_from_DM. refine (pb_DM_of_DM γ f). Defined. @@ -204,7 +204,7 @@ Defined. Definition sqr_comm_of_DM {CC : category} {C : DM_structure CC} {Δ Γ} (γ : DM C Δ Γ) {Γ'} (f : Γ' --> Γ) : pb_arrow_of_arrow _ _ ;; γ = pb_DM_of_DM γ f ;; f. -Proof. +Proof. apply sqr_comm_of_dm_sub_pb. Defined. diff --git a/TypeTheory/OtherDefs/DM_to_TypeCat.v b/TypeTheory/OtherDefs/DM_to_TypeCat.v index 3def0ee9..1ae4b293 100644 --- a/TypeTheory/OtherDefs/DM_to_TypeCat.v +++ b/TypeTheory/OtherDefs/DM_to_TypeCat.v @@ -1,15 +1,15 @@ -(** - +(** + Ahrens, Lumsdaine, Voevodsky, 2015 Contents: - Definition of a Comprehension precategory from a precategory with Display maps - + *) -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import TypeTheory.TypeCat.TypeCat. @@ -91,8 +91,8 @@ Proof. rewrite X. apply isinclpr1. intros. apply (pr2 (pr2 C)). -Qed. - +Qed. + (* this seems to require (at least!) that the objects of the underlying category form a set *) (* Lemma is_split_type_cat_from_DM : is_split_type_cat type_cat_struct_from_DM. @@ -103,5 +103,5 @@ Proof. refine (tpair _ _ _ ). + unfold reind_type_cat; simpl. *) - + End DM_to_TypeCat. diff --git a/TypeTheory/OtherDefs/TypeCat_to_CwF_Pitts.v b/TypeTheory/OtherDefs/TypeCat_to_CwF_Pitts.v index d68fed66..aafbcaf3 100644 --- a/TypeTheory/OtherDefs/TypeCat_to_CwF_Pitts.v +++ b/TypeTheory/OtherDefs/TypeCat_to_CwF_Pitts.v @@ -1,6 +1,6 @@ (** - + Ahrens, Lumsdaine, Voevodsky, 2015 Contents: @@ -11,7 +11,7 @@ Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -20,14 +20,14 @@ Require Import TypeTheory.Auxiliary.Pullbacks. Require Import TypeTheory.TypeCat.TypeCat. Require Import TypeTheory.OtherDefs.CwF_Pitts. -(** * CwF structure from split type-category structure on a category +(** * CwF structure from split type-category structure on a category Every split-Comp-cat gives rise to a category with families. Since the components of the CwF structure are highly successively dependent, we construct most of them individually, before putting them together in [cwf_of_type_cat]. *) -Section CwF_of_Comp. +Section CwF_of_Comp. Context (CC : category) (C : split_typecat_structure CC). @@ -40,7 +40,7 @@ Proof. unfold tt_structure. exists (ty_typecat C). intros Γ A. - exact (∑ f : Γ --> Γ ◂ A, f ;; dpr_typecat _ = identity _ ). + exact (∑ f : Γ --> Γ ◂ A, f ;; dpr_typecat _ = identity _ ). Defined. (* A handy lemma for calculations with terms of reindexed types. @@ -97,7 +97,7 @@ Proof. apply (@reind_comp_typecat C_sptc). Defined. (* needs to be transparent for comp_law_3 at least *) -Lemma reindx_term_id_typecat +Lemma reindx_term_id_typecat (Γ : CC) (A : tt_reindx_from_typecat ⟨ Γ ⟩) (a : tt_reindx_from_typecat ⟨ Γ ⊢ A ⟩) : @@ -125,7 +125,7 @@ Proof. Qed. -Lemma reindx_term_comp_typecat +Lemma reindx_term_comp_typecat (Γ Γ' Γ'' : CC) (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') @@ -135,7 +135,7 @@ Lemma reindx_term_comp_typecat a ⟦ γ';; γ ⟧ = transportf (λ B : C Γ'', ∑ f : Γ'' --> Γ'' ◂ B, f;; dpr_typecat B = identity Γ'') - (! @reind_comp_typecat C_sptc Γ A Γ' γ Γ'' γ') + (! @reind_comp_typecat C_sptc Γ A Γ' γ Γ'' γ') ((a ⟦ γ ⟧) ⟦ γ' ⟧). Proof. intros. @@ -167,7 +167,7 @@ Qed. Definition reindx_laws_terms_of_typecat : reindx_laws_terms reindx_laws_type_of_typecat. Proof. split. - - apply reindx_term_id_typecat. + - apply reindx_term_id_typecat. - intros. apply reindx_term_comp_typecat. Qed. @@ -199,7 +199,7 @@ Proof. - unfold tt_reindx_comp_1_of_typecat in *. simpl in *. + unshelve refine (tpair _ _ _ ). - * { unfold comp_obj. simpl. + * { unfold comp_obj. simpl. eapply map_into_Pb. - apply reind_pb_typecat. - apply maponpaths_2. @@ -260,7 +260,7 @@ Proof. etrans. 2: { eapply maponpaths, pathsinv0, Pb_map_commutes_2. } etrans. 2: { apply pathsinv0, id_right. } cbn. etrans. { apply assoc'. } - etrans. { apply maponpaths, pathsinv0. + etrans. { apply maponpaths, pathsinv0. eapply z_iso_inv_on_right. etrans. 2: { apply assoc'. } apply (@q_comp_typecat C_sptc). } @@ -315,9 +315,9 @@ Proof. rewrite (@q_comp_typecat ((CC,,pr1 C),,pr2 C)). match goal with |[ |- _ ;; ?B' ;; ?C' = _ ] => set (B:=B'); set (D:=C') end. simpl in *. - match goal with |[ |- @map_into_Pb _ _ _ _ _ _ ?B' ?C' ?D' ?E' ?F' ?G' ?Y' ?Z' ?W' ;; _ ;; _ = _ ] => + match goal with |[ |- @map_into_Pb _ _ _ _ _ _ ?B' ?C' ?D' ?E' ?F' ?G' ?Y' ?Z' ?W' ;; _ ;; _ = _ ] => set (f':=B'); set (g:=C'); set (h:=D'); set (k:=E') end. - match goal with |[ |- @map_into_Pb _ _ _ _ _ _ _ _ _ _ ?F' ?G' ?Y' ?Z' _ ;; _ ;; _ = _ ] => + match goal with |[ |- @map_into_Pb _ _ _ _ _ _ _ _ _ _ ?F' ?G' ?Y' ?Z' _ ;; _ ;; _ = _ ] => set (x:=F'); set (y:=G'); set (Y:=Y'); set (Z:=Z') end. @@ -330,7 +330,7 @@ Proof. rewrite <- idtoiso_concat_pr. etrans. apply maponpaths_2. apply maponpaths_2. apply maponpaths. - apply idtoiso_eq_idpath. + apply idtoiso_eq_idpath. { rewrite <- maponpathscomp0. apply maponpaths_eq_idpath. simpl. @@ -355,8 +355,8 @@ Proof. repeat split. - exists reindx_laws_of_typecat. repeat split. - + apply comp_laws_1_2_of_typecat. - + apply comp_law_3_of_typecat. + + apply comp_laws_1_2_of_typecat. + + apply comp_law_3_of_typecat. + apply comp_law_4_of_typecat. - apply (@isaset_types_typecat C_sptc). - simpl. @@ -373,6 +373,6 @@ Proof. exists tt_reindx_type_struct_of_typecat. exact cwf_laws_of_typecat. Defined. - + End CwF_of_Comp. diff --git a/TypeTheory/OtherDefs/TypeCat_to_DM.v b/TypeTheory/OtherDefs/TypeCat_to_DM.v index a9a37da7..5fea6c2a 100644 --- a/TypeTheory/OtherDefs/TypeCat_to_DM.v +++ b/TypeTheory/OtherDefs/TypeCat_to_DM.v @@ -1,5 +1,5 @@ -(** - +(** + Ahrens, Lumsdaine, Voevodsky, 2015 Contents: @@ -8,7 +8,7 @@ (assumption of saturatedness needed for pullbacks forming hprop) *) -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -22,7 +22,7 @@ Require Import TypeTheory.OtherDefs.DM. Section TypeCat_to_DM. Variable CC : category. -Variable H : is_univalent CC. +Variable H : is_univalent CC. Variable C : typecat_structure CC. Definition iso_to_dpr {Γ Γ'} (γ : Γ --> Γ') : UU @@ -82,7 +82,7 @@ Proof. - unshelve refine (make_Pullback _ _). 5: use postcomp_pb_with_z_iso. 7: eapply is_symmetric_isPullback, reind_pb_typecat. - + eassumption. + + eassumption. + sym. assumption. - simpl. apply hinhpr. @@ -104,5 +104,5 @@ Proof. exists dm_sub_closed_under_iso_of_TypeCat. intros. apply isapropishinh. Defined. - + End TypeCat_to_DM. diff --git a/TypeTheory/RelUniv/RelUniv_Cat.v b/TypeTheory/RelUniv/RelUniv_Cat.v index 9f5b97c7..20373ce5 100644 --- a/TypeTheory/RelUniv/RelUniv_Cat.v +++ b/TypeTheory/RelUniv/RelUniv_Cat.v @@ -4,7 +4,7 @@ Part of the [TypeTheory] library (Ahrens, Lumsdaine, Voevodsky, 2015–present). *) -(** +(** This module defines two categories of relative J-universe structures: - [reluniv_cat] — with "simple" (or naive) morphisms (simple commutative squares); - [reluniv_with_ϕ_cat] — with "full" morphisms (with explicit ϕ component and corresponding axioms). @@ -30,7 +30,7 @@ Require Import UniMath.MoreFoundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -95,7 +95,7 @@ Section RelUniv_ϕ_Cat. (X : C) (f : J X --> U u1) : UU := Xf u1 X f --> Xf u2 X (f ;; F_U mor). - + Definition has_reluniv_mor_axiom_ϕ_π {u1 u2 : relative_universe J} (mor : relative_universe_mor u1 u2) @@ -103,7 +103,7 @@ Section RelUniv_ϕ_Cat. (ϕ : reluniv_mor_ϕ_data mor X f) : UU := ϕ ;; π u2 X (F_U mor ∘ f) = π u1 X f. - + Definition has_reluniv_mor_axiom_ϕ_Q {u1 u2 : relative_universe J} (mor : relative_universe_mor u1 u2) @@ -383,7 +383,7 @@ Section RelUniv_ϕ_Cat. etrans. use transportf_forall. apply funextsec. intros f. use total2_paths_f. + etrans. - + set (A := relative_universe_mor u1 u2). set (B := λ (a : A), reluniv_mor_ϕ_data a X f). set (P := λ (a : A) (b : B a), @@ -399,7 +399,7 @@ Section RelUniv_ϕ_Cat. ). etrans. apply pathsinv0, idtoiso_postcompose. - + apply pathsinv0. etrans. apply pathsinv0, e_ϕ. apply maponpaths. @@ -490,7 +490,7 @@ Section RelUniv_ϕ_Cat. etrans. apply maponpaths, pathsinv0, idtoiso_concat_pr. etrans. apply assoc'. etrans. apply maponpaths, pathsinv0, idtoiso_concat_pr. - + etrans. 2: apply id_right. apply maponpaths. apply idtoiso_eq_idpath. @@ -557,7 +557,7 @@ Section RelUniv_ϕ_Cat. = k (f;g;h) ; idtoiso ; idtoiso ; compat *) - + (* Step 4: get rid of idtoiso on the left of k *) etrans. apply maponpaths, assoc'. etrans. apply maponpaths, assoc'. @@ -566,24 +566,24 @@ Section RelUniv_ϕ_Cat. etrans. apply maponpaths_2, idtoiso_eq_idpath. apply pathsinv0r. etrans. apply id_left. - + (* Oversimplified version of the equation: k (f;g;h) ; (idtoiso ; idtoiso) = k (f;g;h) ; idtoiso ; idtoiso ; compat *) - + (* Step 5: get rid of k *) apply maponpaths. - + (* Oversimplified version of the equation: idtoiso ; idtoiso = idtoiso ; idtoiso ; compat *) - + (* Step 6: reduce equality of idtoiso to equality of paths *) etrans. apply pathsinv0, idtoiso_concat_pr. etrans. 2: { apply maponpaths, idtoiso_concat_pr. } @@ -644,11 +644,11 @@ Section Comm_Squares. (* TODO: perhaps it would be better to unify this with the displayed arrow category. *) Context {C : precategory}. - + Definition comm_square {c c' : C} (f : c --> c') {d d' : C} (g : d --> d') - := ∑ (hk : c --> d × c' --> d'), (pr1 hk ;; g = f ;; pr2 hk). + := ∑ (hk : c --> d × c' --> d'), (pr1 hk ;; g = f ;; pr2 hk). Definition dom_comm_square {c c' : C} {f : c --> c'} @@ -674,23 +674,23 @@ End Comm_Squares. Section Functor_Squares. (* Start by defining “pre-functor-squares”, with no commutativity, - so that we can have a single pair of access functions [dom_functor], + so that we can have a single pair of access functions [dom_functor], [cod_functor] which can (via coercions) be used for lax-, colax-, and pseudo-commutative squares alike. *) -Definition pre_functor_square +Definition pre_functor_square {C D : precategory} (J : C ⟶ D) {C' D' : precategory} (J' : C' ⟶ D') : UU := (functor C C' × functor D D'). -Definition dom_functor +Definition dom_functor {C D : precategory} {J : C ⟶ D} {C' D' : precategory} {J' : C' ⟶ D'} : pre_functor_square J J' -> C ⟶ C' := pr1. -Definition cod_functor +Definition cod_functor {C D : precategory} {J : C ⟶ D} {C' D' : precategory} {J' : C' ⟶ D'} : pre_functor_square J J' -> D ⟶ D' diff --git a/TypeTheory/RelUniv/RelUniv_Cat_Simple.v b/TypeTheory/RelUniv/RelUniv_Cat_Simple.v index 8b9f575f..237f9e41 100644 --- a/TypeTheory/RelUniv/RelUniv_Cat_Simple.v +++ b/TypeTheory/RelUniv/RelUniv_Cat_Simple.v @@ -4,7 +4,7 @@ Part of the [TypeTheory] library (Ahrens, Lumsdaine, Voevodsky, 2015–present). *) -(** +(** This module defines two categories of relative J-universe structures: - [reluniv_cat] — with "simple" (or naive) morphisms (simple commutative squares); - [reluniv_with_ϕ_cat] — with "full" morphisms (with explicit ϕ component and corresponding axioms). @@ -28,7 +28,7 @@ Require Import UniMath.MoreFoundations.All. Require Import TypeTheory.Auxiliary.CategoryTheoryImports. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. @@ -389,7 +389,7 @@ Section RelUniv_Functor. Definition weak_from_reluniv_is_functor : is_functor weak_from_reluniv_functor_data := (weak_from_reluniv_functor_idax ,, weak_from_reluniv_functor_compax). - + Definition weak_from_reluniv_functor : functor (reluniv_cat J) (weak_reluniv_cat J) := make_functor weak_from_reluniv_functor_data @@ -434,7 +434,7 @@ Section RelUniv_Functor. : catiso (reluniv_cat J) (weak_reluniv_cat J) := (weak_from_reluniv_functor ,, weak_from_reluniv_functor_is_catiso Ccat J_ff). - + Definition reluniv_cat_is_univalent (Ccat : is_univalent C) (J_ff : fully_faithful J) (Dcat : is_univalent D) diff --git a/TypeTheory/TypeCat/Contextual.v b/TypeTheory/TypeCat/Contextual.v index e018ae3b..fcf9cc54 100644 --- a/TypeTheory/TypeCat/Contextual.v +++ b/TypeTheory/TypeCat/Contextual.v @@ -4,8 +4,8 @@ Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. -Require Import UniMath.CategoryTheory.limits.graphs.limits. -Require Import UniMath.CategoryTheory.limits.graphs.terminal. +Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. +Require Import UniMath.CategoryTheory.Limits.Graphs.Terminal. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -23,7 +23,7 @@ Section Extensions. Proof. destruct n as [ | n']. - exists unit. intros e; exact Γ. - - set (E_R := extension_aux C Γ n'). + - set (E_R := extension_aux C Γ n'). exists (∑ (E : pr1 E_R), C (pr2 E_R E)). intros AA_B. exact (ext_typecat _ (pr2 AA_B)). Defined. @@ -73,7 +73,7 @@ Section Extensions. Definition ext_extension {C:typecat} (Γ:C) (AA : extension Γ) : C - := ext_extension_of_length Γ AA. + := ext_extension_of_length Γ AA. Arguments ext_extension : simpl nomatch. Fixpoint dpr_extension {C:typecat} {n:nat} {Γ:C} @@ -104,13 +104,13 @@ Section Extensions. Qed. (* To define concatenation of extensions, we also need to mutually define some comparison between the extension by the concatenation (Γ + (AA + BB)) and the two-stage extension ((Γ + AA) + BB). - + This comparison could be given as an equality; however we avoid taking that as primary, to minimise use of equality on objects, and instead give it just as the morphism required, and show afterwards that it’s an equality. *) Definition concat_extension_aux {C : typecat} {Γ:C} {n} (AA : extension_of_length n Γ) {m} (BB : extension_of_length m (ext_extension Γ AA)) : ∑ (AABB : extension_of_length (m+n) Γ), - ext_extension Γ AABB --> ext_extension _ BB. + ext_extension Γ AABB --> ext_extension _ BB. Proof. induction m as [ | m' IH]; simpl. - (* m = 0, BB empty *) @@ -134,12 +134,12 @@ Section Extensions. {m} (BB : extension_of_length m (ext_extension Γ AA)) : extension_of_length (m+n) Γ := pr1 (concat_extension_aux AA BB). - + Definition compare_concat_extension {C : typecat} {Γ:C} {n} (AA : extension_of_length n Γ) {m} (BB : extension_of_length m (ext_extension Γ AA)) : ext_extension Γ (concat_extension AA BB) - --> ext_extension (ext_extension Γ AA) BB + --> ext_extension (ext_extension Γ AA) BB := pr2 (concat_extension_aux AA BB). Definition path_ext_typecat {C : split_typecat} @@ -173,12 +173,12 @@ Section Extensions. Proof. induction m as [ | m' IH]; simpl. - (* m = 0, BB empty *) - use tpair; apply idpath. + use tpair; apply idpath. - (* m = S m', BB = BB';;B *) set (B := extension_last BB); set (BB' := extension_rest BB) in *. destruct (IH BB') as [e1 e2]; clear IH. unfold ext_extension, ext_extension_of_length; simpl. - use tpair. + use tpair. + use path_ext_typecat. * exact e1. * apply maponpaths, e2. @@ -194,12 +194,12 @@ Section Extensions. : ext_extension Γ (concat_extension AA BB) = (ext_extension _ BB). Proof. exact (pr1 (ext_concat_extension_aux AA BB)). - Defined. + Defined. End Extensions. Section Contextual_Cats. -(** A split type-category is _contextual_ if it has some base object, such that every object arises uniquely as an extension of this base object. +(** A split type-category is _contextual_ if it has some base object, such that every object arises uniquely as an extension of this base object. Note that such a base object is necessarily unique: see [isaprop_is_contextual]. *) @@ -262,7 +262,7 @@ Note that such a base object is necessarily unique: see [isaprop_is_contextual]. := ∑ C : split_typecat, is_contextual C. Coercion pr1_contextual_cat := pr1 : contextual_cat -> split_typecat. - Coercion pr2_contextual_cat := pr2 + Coercion pr2_contextual_cat := pr2 : forall C : contextual_cat, is_contextual C. Lemma isaset_ob_contextual_cat {C : contextual_cat} diff --git a/TypeTheory/TypeCat/TypeCat.v b/TypeTheory/TypeCat/TypeCat.v index 952673cc..ca051705 100644 --- a/TypeTheory/TypeCat/TypeCat.v +++ b/TypeTheory/TypeCat/TypeCat.v @@ -1,5 +1,5 @@ -(** +(** Ahrens, Lumsdaine, Voevodsky, 2015– @@ -14,7 +14,7 @@ Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. -Require Import UniMath.CategoryTheory.limits.pullbacks. +Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import TypeTheory.Auxiliary.Auxiliary. Require Import TypeTheory.Auxiliary.CategoryTheory. @@ -23,22 +23,22 @@ Require Import TypeTheory.Auxiliary.CategoryTheory. We define here *Type (pre-)categories*, closely based on the _type-categories_ of Andy Pitts, _Categorical Logic_, 2000, Def. 6.3.3 #(link).# -However, that definition includes two _strictness conditions_; -we follow van den Berg and Garner, _Topological and simplicial models_, Def 2.2.1 #(arXiv)# +However, that definition includes two _strictness conditions_; +we follow van den Berg and Garner, _Topological and simplicial models_, Def 2.2.1 #(arXiv)# in separating these out from the rest of the definition. - An element of [typecat], as we define it below, is thus exactly a type-category according -to the definition of van den Berg and Garner (except with an underlying _precategory_, i.e. hom-types not assumed sets); and an element of [split_typecat] is a split type-category + An element of [typecat], as we define it below, is thus exactly a type-category according +to the definition of van den Berg and Garner (except with an underlying _precategory_, i.e. hom-types not assumed sets); and an element of [split_typecat] is a split type-category according to van den Berg and Garner, or a plain type-category in the sense of Pitts. - In order to avoid the nested sigma-types getting too deep, + In order to avoid the nested sigma-types getting too deep, we split up the structure into two stages: [typecat_structure1] and [typecat_structure2]. *) (** * A "preview" of the definition *) Module Record_Preview. (** For technical reasons, we prefer not to use record types in the development. -However, a definition as a record type is much more readable — so we give that here, +However, a definition as a record type is much more readable — so we give that here, for documentation purposes only, wrapped in a module to keep it out of the global namespace. *) @@ -52,11 +52,11 @@ Record type_precat_record : Type := { ty : C -> Type where "C ⟨ Γ ⟩" := (ty Γ); ext : ∏ Γ, C⟨Γ⟩ -> C where "Γ ◂ A" := (ext Γ A); dpr : ∏ Γ (A : C⟨Γ⟩), Γ ◂ A --> Γ where "'π' A" := (dpr _ A); - reind : ∏ Γ (A : C⟨Γ⟩) Γ' (f : Γ' --> Γ), C⟨Γ'⟩ + reind : ∏ Γ (A : C⟨Γ⟩) Γ' (f : Γ' --> Γ), C⟨Γ'⟩ where "A {{ f }}" := (reind _ A _ f); q : ∏ {Γ} (A : ty Γ) {Γ'} (f : Γ' --> Γ), (Γ' ◂ (A {{f }}) --> Γ ◂ A) ; - dpr_q : ∏ Γ (A : C⟨Γ⟩) Γ' (f : Γ' --> Γ), + dpr_q : ∏ Γ (A : C⟨Γ⟩) Γ' (f : Γ' --> Γ), (q A f) ;; (π A) = (π (A{{f}})) ;; f ; reind_pb : ∏ Γ (A : ty Γ) Γ' (f : Γ' --> Γ), isPullback (!dpr_q _ A _ f) @@ -67,20 +67,20 @@ Record type_precat_record : Type := { - [precat_of_type_precat1] (a coercion): the underlying pre-ategory; - [ty_type_cat] (also a coercion): for each object [Γ], a type of “types over [Γ]”, written [C Γ]; - [ext_type_cat]: a context extension operation, written [Γ ◂ A]; -- [dpr_type_cat]: dependent projections from context extensions; +- [dpr_type_cat]: dependent projections from context extensions; - [reind_type_cat]: a reindexing operation on types, written [A[f]] or [f^*A]; - [q_type_cat]: for [f : Γ' → Γ], and [A : C Γ], a map [ (Γ' ◂ f^* A) --> (Γ ◂ A) ]; can be seen as the extension of a context morphism by a variable of a new type; - [dpr_q_type_cat]: reindexing commutes with dependent projections; -- [reind_pb_type_cat]: the commutative square thus formed is a pullback. +- [reind_pb_type_cat]: the commutative square thus formed is a pullback. One possibly surprising point is that [reind_pb] uses the square whose commutativity is witnessed by [dpr_q] itself, but by its inverse of [dpr_q]. The point is that [dpr_q] is oriented in the more computationally natural direction [(q A f) ;; (π A) = (π (A{{f}})) ;; f ], but at the same time, it’s more natural to think of [π A{{f}}] as the first projection of the pullback and [q A f] the second. *) End Record_Preview. -(** For the actual definition, we use iterated ∑-types. -As usual, to avoid severe performance issues with these, -we have to split up the definition into several steps: +(** For the actual definition, we use iterated ∑-types. +As usual, to avoid severe performance issues with these, +we have to split up the definition into several steps: [type_precat_structure1] with the first few components, and [type_precat_structure2] the rest. *) @@ -101,12 +101,12 @@ Coercion precat_from_type_precat1 : type_precat1 >-> precategory. (** Since the various access functions should eventually apply directly to type-categories as well as type-precategories (via coercion from the former to the latter), we drop the [pre] in their names. *) -Definition ty_typecat {CC : precategory} (C : typecat_structure1 CC) : CC -> UU +Definition ty_typecat {CC : precategory} (C : typecat_structure1 CC) : CC -> UU := pr1 C. Coercion ty_typecat : typecat_structure1 >-> Funclass. -Definition ext_typecat {CC : precategory} {C : typecat_structure1 CC} +Definition ext_typecat {CC : precategory} {C : typecat_structure1 CC} (Γ : CC) (A : C Γ) : CC := pr1 (pr2 C) Γ A. Notation "Γ ◂ A" := (ext_typecat Γ A) (at level 40, left associativity). @@ -127,16 +127,16 @@ Notation "A {{ f }}" := (reind_typecat A f) (at level 30). Definition typecat_structure2 {CC : category} (C : typecat_structure1 CC) := ∑ (dpr : ∏ Γ (A : C Γ), Γ◂A --> Γ) (q : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ), (Γ'◂A{{f}}) --> Γ◂A ) - (dpr_q : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ), + (dpr_q : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ), (q _ A _ f) ;; (dpr _ A) = (dpr _ (A{{f}})) ;; f), ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ), isPullback (!dpr_q _ A _ f). (* TODO: change name [dpr_q] to [q_dpr] throughout, now that composition is diagrammatic order? *) -Definition typecat_structure (CC : category) +Definition typecat_structure (CC : category) := ∑ C : typecat_structure1 CC , typecat_structure2 C. -Definition typecat1_from_typecat (CC : category)(C : typecat_structure CC) +Definition typecat1_from_typecat (CC : category)(C : typecat_structure CC) : typecat_structure1 _ := pr1 C. Coercion typecat1_from_typecat : typecat_structure >-> typecat_structure1. @@ -147,7 +147,7 @@ Definition dpr_typecat {CC : category} Definition q_typecat {CC : category} {C : typecat_structure CC} {Γ} (A : C Γ) {Γ'} (f : Γ' --> Γ) - : (Γ' ◂ A{{f}}) --> (Γ ◂ A) + : (Γ' ◂ A{{f}}) --> (Γ ◂ A) := pr1 (pr2 (pr2 C)) _ A _ f. @@ -172,7 +172,7 @@ Definition is_type_saturated_typecat {CC : category} (** * Splitness *) -(** A type-precategory [C] is _split_ if it is a category (i.e. has hom-sets); each collection of types [C Γ] is a set, reindexing is strictly functorial; and the [q] maps satisfy the evident functoriality axioms *) +(** A type-precategory [C] is _split_ if it is a category (i.e. has hom-sets); each collection of types [C Γ] is a set, reindexing is strictly functorial; and the [q] maps satisfy the evident functoriality axioms *) Definition is_split_typecat {CC : category} (C : typecat_structure CC) := (∏ Γ:CC, isaset (C Γ)) × (∑ (reind_id : ∏ Γ (A : C Γ), A {{identity Γ}} = A), @@ -253,7 +253,7 @@ Definition q_q_typecat = idtoiso (maponpaths _ (!reind_comp_typecat A f g)) ;; q_typecat A (g ;; f). Proof. - intros. apply z_iso_inv_to_left, pathsinv0. + intros. apply z_iso_inv_to_left, pathsinv0. etrans. { apply q_comp_typecat. } repeat rewrite <- assoc; apply maponpaths_2. generalize (reind_comp_typecat A f g). @@ -280,7 +280,7 @@ Context {CC : category} {C : typecat_structure CC}. Lemma transportf_dpr_typecat {Γ : CC} {A B : C Γ} (p : A = B) - (f : Γ --> Γ ◂ A) + (f : Γ --> Γ ◂ A) : transportf (λ B : C Γ, Γ --> Γ ◂ B) p f;; dpr_typecat B = f ;; dpr_typecat A. Proof. @@ -293,7 +293,7 @@ Lemma idtoiso_dpr_typecat {Γ : CC} {A B : C Γ} (p : A = B) = dpr_typecat A. Proof. induction p. - apply id_left. + apply id_left. Defined. Lemma idtoiso_q_typecat