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