Merge pull request #4 from m-lindgren/presheaves-coq8.16

Cleanup the previous commits a bit.

TypeTheory/Auxiliary/SetsAndPresheaves.v

@@ -119,22 +119,11 @@ Proof.
   apply (toforallpaths (is_natural_yoneda_iso_inv _ F _ _ f)).
 Qed.
 
-
-Lemma yy_comp_nat_trans_type {C : category}
-      (F F' : preShv C) (p : _ ⟦F, F'⟧)
-      A (v : F $p A)
-  : UU.
-Proof.
-  refine (_ = _).
-  - exact (yy v ;; p).
-  - exact (yy (p $nt v)).
-Defined.
-
 Lemma yy_comp_nat_trans {C : category}
-      (F F' : preShv C) (p : _ ⟦F, F'⟧)
-      A (v : F $p A)
-  : yy_comp_nat_trans_type F F' p A v.
-  (* : yy v ;; p = yy (p $nt v). *)
+      (F F' : preShv C) (p : preShv C ⟦F, F'⟧)
+      (A : C^op)
+      (v : F $p A)
+  : (@yy C F A) v · p = (@yy C F' A) (p $nt v).
 Proof.
   apply nat_trans_eq.
   - apply homset_property.

TypeTheory/CwF/CwF_def.v

@@ -72,7 +72,7 @@ Definition cwf_tm_of_ty {Γ : C} (A : Ty Γ : hSet) : UU
 Lemma cwf_square_comm {Γ} {A}
   {ΓA : C} {π : ΓA --> Γ}
   {t : Tm ΓA : hSet} (e : pp $nt t = # Ty π A)
-  : (# (yoneda C) π ;; (@yy C Ty Γ) A) = ((@yy C Tm ΓA) t ;; pp).
+  : #Yo π ;; (@yy C Ty Γ) A = (@yy C Tm ΓA) t ;; pp.
 Proof.
   apply pathsinv0.
   etrans. 2: { apply yy_natural. }
@@ -112,7 +112,7 @@ Context {C : category} (pp : mor_total (preShv C)).
 Lemma cwf_square_comm_converse {Γ : C} {A : Ty pp Γ : hSet}
     {ΓA : C} {π : ΓA --> Γ}
     {t : Tm pp ΓA : hSet}
-    (e : (# (yoneda C) π ;; (@yy C (@Ty C pp) Γ) A)%mor = ((@yy C (@Tm C pp) ΓA) t ;; pp))
+    (e : #Yo π ;; (@yy C (Ty pp) Γ) A = (@yy C (Tm pp) ΓA) t ;; pp)
   : pp $nt t = # (Ty pp) π A.
 Proof.
   etrans.
@@ -245,11 +245,7 @@ Context (pp : mor_total (preShv C)).
 (* TODO: there is considerable redundancy between this and [cwf_fiber_representation_weq] above; in particular, the same reassociation is used. Try to consolidate? *)
 Definition weq_cwf_fiber_representation_fpullback {Γ : C} (A : Ty pp Γ : hSet)
   : cwf_fiber_representation pp A
-      ≃
-      @fpullback C [C^op, SET] (yoneda C)
-      (@target (preShv C) pp)
-      (@source (preShv C) pp)
-      pp Γ ((@yy C (@Ty C pp) Γ) A).
+      ≃ fpullback (yoneda C) pp ((@yy C (Ty pp) Γ) A).
 Proof.
   unfold cwf_fiber_representation, fpullback.
   (* reassociate the RHS to match the LHS:

TypeTheory/CwF_TypeCat/CwF_SplitTypeCat_Defs.v

@@ -415,10 +415,8 @@ Definition pp Y : TM Y --> TY X := pr1 (pr2 Y).
 Definition te Y {Γ:C} A : Tm Y (Γ ◂ A)
   := pr2 (pr2 Y) Γ A.
 
-Definition Q Y {Γ:C} (A:Ty X Γ) : Yo (Γ ◂ A) --> TM Y.
-Proof.
-  exact(yy (te Y A)).
-Defined.
+Definition Q Y {Γ:C} (A:Ty X Γ) : Yo (Γ ◂ A) --> TM Y
+  := (@yy C (TM Y) (Γ ◂ A)) (te Y A).
 
 Lemma comp_ext_compare_Q Y Γ (A A' : Ty X Γ) (e : A = A') : 
   #Yo (Δ e) ;; Q Y A' = Q Y A . 
@@ -433,7 +431,7 @@ Qed.
 Lemma term_fun_str_square_comm {Y : term_fun_structure_data}
     {Γ : C} {A : Ty X Γ}
     (e : (pp Y) $nt (te Y A) = A [ π A ])
-  : (# (yoneda C) (@π C X Γ A) ;; (@yy C (@TY C X) Γ) A) = (@Q Y Γ A ;; pp Y).
+  : (#Yo (π A) ;; (@yy C (TY X) Γ) A) = (Q Y A ;; pp Y).
 Proof.
   apply pathsinv0.
   etrans. 2: { apply yy_natural. }
@@ -466,10 +464,8 @@ Definition pp_te (Y : term_fun_structure) {Γ} (A : Ty X Γ)
 := pr1 (pr2 Y _ A).
 
 Definition Q_pp (Y : term_fun_structure) {Γ} (A : Ty X Γ)
-  : (# (yoneda C) (@π C X Γ A) ;; (@yy C (@TY C X) Γ) A) = (@Q Y Γ A ;; pp Y).
-Proof.
-  exact(term_fun_str_square_comm (pp_te Y A)).
-Defined.
+  : (#Yo (π A) ;; (@yy C (TY X) Γ) A) = (Q Y A ;; pp Y)
+  := term_fun_str_square_comm (pp_te Y A).
 
 (* TODO: rename this to [Q_pp_Pb], or [qq_π_Pb] to [isPullback_qq_π]? *)
 Definition isPullback_Q_pp (Y : term_fun_structure) {Γ} (A : Ty X Γ)

TypeTheory/TypeConstructions/CwF_SplitTypeCat_TypeEquiv.v

@@ -86,23 +86,19 @@ Proof.
 Qed.
 
 Lemma Subproof_γ {Γ : C} {A : Ty Γ : hSet} (a : CwF_tm A)
-  : (@identity (preShv C) ((yoneda C) Γ) ;; (@yy C Ty Γ) A) = ((@yy C Tm Γ) a ;; pp).
+  : identity (Yo Γ) ;; (@yy C Ty Γ) A = ((@yy C Tm Γ) a ;; pp).
 Proof.
   apply pathsinv0, (pathscomp0(yy_comp_nat_trans Tm Ty pp Γ a)) ,pathsinv0,
   (pathscomp0(@id_left _  (Yo Γ) Ty  (yy A))) ,
   (maponpaths yy (!(pr2 a))).
 Qed.
 
-Definition γ {Γ : C} {A : Ty Γ : hSet} (a : CwF_tm A) : (preShv C)⟦Yo Γ,Yo (Γ.:A)⟧.
-Proof.
-  apply ((CwF_Pullback A) (Yo Γ) (identity _) (yy a) (Subproof_γ a)).
-Defined.
+Definition γ {Γ : C} {A : Ty Γ : hSet} (a : CwF_tm A) : (preShv C)⟦Yo Γ,Yo (Γ.:A)⟧
+  := pr11 ((CwF_Pullback A) (Yo Γ) (identity _) (@yy C Tm Γ a) (Subproof_γ a)).
 
 Definition DepTypesType {Γ : C} {A : Ty Γ : hSet} (B : Ty(Γ.:A) : hSet) (a : CwF_tm A)
-  : Ty Γ : hSet.
-Proof.
-  exact((γ a;;yy B : nat_trans _ _)  Γ (identity Γ)).
-Defined.
+  : Ty Γ : hSet
+  := (γ a ;; (@yy C Ty (Γ.: A)) B : nat_trans _ _)  Γ (identity Γ).
 
 (** Unit Types *)
 Section Unit.

TypeTheory/TypeConstructions/CwF_Structure_Display.v

@@ -254,7 +254,7 @@ Proof.
 Qed.
 
 Lemma qq_yoneda_commutes {Γ Δ : C} (A : Ty Γ : hSet) (f : C^op ⟦Γ,Δ⟧)
-  : (@qq_yoneda Γ Δ A f ;; (@yy C Tm (Γ .: A)) (@te Γ A)) = (@yy C Tm (Δ .: # Ty f A)) (@te Δ (# Ty f A)).
+  : (qq_yoneda A f ;; (@yy C Tm (Γ .: A)) (te A)) = (@yy C Tm (Δ .: # Ty f A)) (te (# Ty f A)).
 Proof.
   apply (PullbackArrow_PullbackPr2 (CwF_Pullback A)).
 Qed.
@@ -298,20 +298,18 @@ Qed.
 Section Familly_Of_Types.
 (** Famillies of types in a Category with famillies**)
 Lemma Subproof_γ {Γ : C} {A : Ty Γ : hSet} (a : tm A)
-  : (@identity (preShv C) ((yoneda C) Γ) ;; (@yy C Ty Γ) A) =
+  : (identity (Yo Γ) ;; (@yy C Ty Γ) A) =
       ((@yy C Tm Γ) a ;; pp).
 Proof.
   apply pathsinv0, (pathscomp0(yy_comp_nat_trans Tm Ty pp Γ a)) ,pathsinv0,
   (pathscomp0(id_left _ )), ((maponpaths yy) (!(pr2 a))).
 Qed.
 
-Definition γ {Γ : C} {A : Ty Γ : hSet} (a : tm A) : (preShv C)⟦Yo Γ,Yo (Γ.:A)⟧.
-Proof.
-  exact(map_into_Pb (CwF_isPullback A) (identity _) (yy a) (Subproof_γ a)).
-Defined.
+Definition γ {Γ : C} {A : Ty Γ : hSet} (a : tm A) : (preShv C)⟦Yo Γ,Yo (Γ.:A)⟧
+  := (map_into_Pb (CwF_isPullback A) (identity _) (@yy C Tm Γ a) (Subproof_γ a)).
 
 Lemma  γ_pull {Γ : C} (A : Ty Γ : hSet) (a : tm A)
-  : (@γ Γ A a ;; (@yy C Tm (Γ .: A)) (@te Γ A)) = (@yy C Tm Γ) a.
+  : (γ a ;; (@yy C Tm (Γ .: A)) (te A)) = (@yy C Tm Γ) a.
 Proof.
   apply Pb_map_commutes_2.
 Qed.
@@ -352,10 +350,10 @@ Proof.
 Qed.
 
 Lemma γPullback1 {Γ : C} (A : Ty Γ : hSet)
-  : (@γ (Γ .: A) (# Ty (@pi Γ A) A) (@te Γ A) ;;
-     # (yoneda C : C ⟶ preShv C) (@qq_term Γ (Γ .: A) A (@pi Γ A)) ;; (@yy C Tm (Γ .: A)) (@te Γ A))
-    =
-      (@identity [C^op, SET] (yoneda C (Γ .: A)) ;; (@yy C Tm (Γ .: A)) (@te Γ A)).
+  : γ (te A)
+     ;; #Yo (qq_term A (pi A))
+     ;; (@yy C Tm (Γ .: A)) (te A)
+    = identity _ ;; (@yy C Tm (Γ .: A)) (te A).
 Proof.
   rewrite id_left.
   rewrite (qq_yoneda_compatibility A (pi A)), <- assoc.
@@ -420,20 +418,15 @@ Proof.
 Qed.
 
 Definition DepTypesType {Γ : C} {A : Ty Γ : hSet}
-  (B : Ty(Γ.:A) : hSet)
-  (a : tm A)
-  : Ty Γ : hSet.
-Proof.
-  exact((γ a;;yy B : nat_trans _ _) Γ (identity Γ)).
-Defined.
+  (B : Ty(Γ.:A) : hSet) (a : tm A)
+  : Ty Γ : hSet
+  := (γ a ;; (@yy C Ty (Γ .: A) B) : nat_trans _ _) Γ (identity Γ).
 
 Definition DepTypesElem_pr1 {Γ : C} {A : Ty Γ : hSet} {B : Ty(Γ.:A) : hSet}
   (b : tm B)
   (a : tm A)
-  : Tm Γ : hSet.
-Proof.
-  exact((γ a;;yy b : nat_trans _ _) Γ (identity Γ)).
-Defined.
+  : Tm Γ : hSet
+  := (γ a ;; (@yy C Tm (Γ .: A) b) : nat_trans _ _) Γ (identity Γ).
 
 Lemma DepTypesComp {Γ : C} { A : Ty Γ : hSet} {B : Ty(Γ.:A) : hSet}
 (b : tm B) (a : tm A)