Merge pull request #196 from benediktahrens/adapt-to-unimath

Adapt to changes in UniMath/UniMath

Author: benediktahrens

TypeTheory/ALV1/CwF_Defs_Equiv.v

@@ -91,7 +91,7 @@ Definition rep1_fiber_axioms {pp : mor_total (preShv C)}
 :=
   ∑ (e : ((pp : _ --> _) : nat_trans _ _ ) _ te
          = (# (Ty pp) π A)),
-    isPullback _ _ _ _ (cwf_square_comm e).
+    isPullback (cwf_square_comm e).
 
 Definition rep1_axioms {pp : mor_total (preShv C)} (Y : rep1_data pp) : UU :=
   ∏ Γ (A : Ty pp Γ : hSet), rep1_fiber_axioms A (dpr Y A) (te Y A).

TypeTheory/ALV1/CwF_SplitTypeCat_Cats_Standalone.v

@@ -109,7 +109,7 @@ Lemma term_to_section_naturality {Y} {Y'}
 Proof.
   set (t' := (term_fun_mor_TM FY : nat_trans _ _) _ t).
   set (A' := (pp Y' : nat_trans _ _) _ t').
-  set (Pb := isPullback_preShv_to_pointwise (homset_property _) (isPullback_Q_pp Y' A') Γ);
+  set (Pb := isPullback_preShv_to_pointwise (isPullback_Q_pp Y' A') Γ);
     simpl in Pb.
   apply (pullback_HSET_elements_unique Pb); clear Pb.
   - unfold yoneda_morphisms_data; cbn.
@@ -393,10 +393,10 @@ Proof.
   - apply idpath.
   - etrans. apply id_right.
     cbn. apply PullbackArrowUnique.
-    + use (PullbackArrow_PullbackPr1
-                (make_Pullback _ _ _ _ _ _ (qq_π_Pb _ f A))).
+    + 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')
@@ -423,10 +423,10 @@ Proof.
   - apply idpath.
   - etrans. apply id_right. 
     cbn. apply PullbackArrowUnique.
-    + cbn. apply (PullbackArrow_PullbackPr1 (make_Pullback _ _ _ _ _ _ _)).
+    + cbn. apply (PullbackArrow_PullbackPr1 (make_Pullback _ _)).
     + cbn. cbn in FZ. 
       etrans. apply maponpaths, @pathsinv0, FZ.
-      apply (PullbackArrow_PullbackPr2 (make_Pullback _ _ _ _ _ _ _)). 
+      apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). 
 Qed.
 
 End Rename_me.
@@ -618,13 +618,14 @@ Proof.
   repeat (apply impred_isaprop; intro). apply setproperty.
 Qed.
 
+Definition term_fun_category : category := make_category _ has_homsets_term_fun_precategory.
+
 Theorem is_univalent_term_fun_structure
-  : is_univalent term_fun_precategory.
+  : is_univalent term_fun_category.
 Proof.
-  split.
-  - apply eq_equiv_from_retraction with iso_to_id_term_fun_precategory.
-    intros. apply eq_iso. apply isaprop_term_fun_mor.
-  - apply has_homsets_term_fun_precategory. 
+  use eq_equiv_from_retraction.
+  - apply iso_to_id_term_fun_precategory.
+  - intros. apply eq_iso. apply isaprop_term_fun_mor.
 Qed.
 
 End Is_Univalent_Families_Strucs.
@@ -699,16 +700,17 @@ Proof.
   intros a b. apply isasetaprop. apply isaprop_qq_structure_mor.
 Qed.
 
+Definition qq_structure_category : category
+  := make_category _ has_homsets_qq_structure_precategory.
+
 Theorem is_univalent_qq_morphism
-  : is_univalent qq_structure_precategory.
-Proof.
-  split.
-  - intros d d'. 
-    use isweqimplimpl. 
-    + apply qq_structure_iso_to_id.
-    + apply isaset_qq_morphism_structure.
-    + apply isaprop_iso_qq_morphism_structure.
-  - apply has_homsets_qq_structure_precategory.
+  : is_univalent qq_structure_category.
+Proof.
+  intros d d'. 
+  use isweqimplimpl. 
+  + apply qq_structure_iso_to_id.
+  + apply isaset_qq_morphism_structure.
+  + apply isaprop_iso_qq_morphism_structure.
 Qed.
 
 End Is_Univalent_qq_Strucs.
@@ -722,14 +724,23 @@ Proof.
   - apply has_homsets_qq_structure_precategory. 
 Qed.
 
-Definition pr1_equiv : adj_equivalence_of_precats compat_structures_pr1_functor.
+Definition compat_structures_category : category
+  := make_category _ has_homsets_compat_structures_precategory.
+
+Definition pr1_equiv : @adj_equivalence_of_precats
+                         compat_structures_category
+                         term_fun_category
+                         compat_structures_pr1_functor.
 Proof.
   use adj_equivalence_of_precats_ff_split.
   - apply compat_structures_pr1_fully_faithful.
   - apply compat_structures_pr1_split_ess_surj.
 Defined.
 
-Definition pr2_equiv : adj_equivalence_of_precats compat_structures_pr2_functor.
+Definition pr2_equiv : @adj_equivalence_of_precats
+                         compat_structures_category
+                         qq_structure_category
+                         compat_structures_pr2_functor.
 Proof.
   use adj_equivalence_of_precats_ff_split.
   - apply compat_structures_pr2_fully_faithful.

TypeTheory/ALV1/CwF_SplitTypeCat_Defs.v

@@ -440,7 +440,7 @@ Qed.
 Definition term_fun_structure_axioms (Y : term_fun_structure_data) :=
   ∏ Γ (A : Ty X Γ), 
         ∑ (e : (pp Y : nat_trans _ _) _ (te Y A) = A [ π A ]),
-          isPullback _ _ _ _ (term_fun_str_square_comm e).
+          isPullback (term_fun_str_square_comm e).
 
 Lemma isaprop_term_fun_structure_axioms Y
   : isaprop (term_fun_structure_axioms Y).
@@ -467,12 +467,12 @@ Definition Q_pp (Y : term_fun_structure) {Γ} (A : Ty X Γ)
 
 (* TODO: rename this to [Q_pp_Pb], or [qq_π_Pb] to [isPullback_qq_π]? *)
 Definition isPullback_Q_pp (Y : term_fun_structure) {Γ} (A : Ty X Γ)
-  : isPullback _ _ _ _ (Q_pp Y A)
+  : isPullback (Q_pp Y A)
 := pr2 (pr2 Y _ _ ).
 
 (* TODO: look for places these three lemmas can be used to simplify proofs *) 
 Definition Q_pp_Pb_pointwise (Y : term_fun_structure) (Γ' Γ : C) (A : Ty X Γ)
-  := isPullback_preShv_to_pointwise (homset_property _) (isPullback_Q_pp Y A) Γ'.
+  := isPullback_preShv_to_pointwise (isPullback_Q_pp Y A) Γ'.
 
 Definition Q_pp_Pb_univprop (Y : term_fun_structure) (Γ' Γ : C) (A : Ty X Γ)
   := pullback_HSET_univprop_elements _ (Q_pp_Pb_pointwise Y Γ' Γ A).
@@ -491,7 +491,7 @@ Lemma term_to_section_aux {Y : term_fun_structure} {Γ:C} (t : Tm Y Γ)
          f ;; π _ = identity Γ
        × (Q Y A : nat_trans _ _) Γ f = t).
 Proof.
-  set (Pb := isPullback_preShv_to_pointwise (homset_property _) (isPullback_Q_pp Y A) Γ).
+  set (Pb := isPullback_preShv_to_pointwise (isPullback_Q_pp Y A) Γ).
   simpl in Pb.
   apply (pullback_HSET_univprop_elements _ Pb).
   exact (toforallpaths _ _ _ (functor_id (TY X) _) A).
@@ -557,7 +557,7 @@ Definition qq_morphism_data : UU :=
   ∑ q : ∏ {Γ Γ'} (f : C⟦Γ', Γ⟧) (A : (TY X:functor _ _ ) Γ : hSet), 
            C ⟦Γ' ◂ A [ f ], Γ ◂ A⟧, 
     (∏ Γ Γ' (f : C⟦Γ', Γ⟧) (A : (TY X:functor _ _ ) Γ : hSet), 
-        ∑ e : q f A ;; π _ = π _ ;; f , isPullback _ _ _ _ (!e)).
+        ∑ e : q f A ;; π _ = π _ ;; f , isPullback (!e)).
 
 Definition qq (Z : qq_morphism_data) {Γ Γ'} (f : C ⟦Γ', Γ⟧)
               (A : (TY X:functor _ _ ) Γ : hSet) 
@@ -571,7 +571,7 @@ Proof.
   exact (pr1 (pr2 Z _ _ f A)).
 Qed.
 
-Lemma qq_π_Pb (Z : qq_morphism_data) {Γ Γ'} (f : Γ' --> Γ) (A : _ ) : isPullback _ _ _ _ (!qq_π Z f A).
+Lemma qq_π_Pb (Z : qq_morphism_data) {Γ Γ'} (f : Γ' --> Γ) (A : _ ) : isPullback (!qq_π Z f A).
 Proof.
   exact (pr2 (pr2 Z _ _ f A)).
 Qed.

TypeTheory/ALV1/CwF_SplitTypeCat_Equivalence.v

@@ -53,7 +53,7 @@ Proof.
   etrans. apply (toforallpaths _ _ _ (!functor_comp (TM Y) _ _ ) _).
   etrans. 2: { apply (toforallpaths _ _ _ (functor_comp (TM Y) _ _ ) _). }
   apply maponpaths_2. 
-  apply (@PullbackArrow_PullbackPr2 C _ _ _ _ _ (make_Pullback _ _ _ _ _ _ _)).
+  apply (@PullbackArrow_PullbackPr2 C _ _ _ _ _ (make_Pullback _ _)).
 Qed.
 
 Definition canonical_TM_to_given : (preShv C) ⟦tm_from_qq Z, TM (pr1 Y)⟧.
@@ -142,8 +142,9 @@ Definition canonical_TM_to_given_iso
   : @iso (preShv C) (tm_from_qq Z) (TM (pr1 Y)).
 Proof.
   exists canonical_TM_to_given.
-  apply functor_iso_if_pointwise_iso. intro c.
-  apply canonical_TM_to_given_pointwise_iso.
+  apply functor_iso_if_pointwise_iso.
+  intro Γ. 
+  apply (canonical_TM_to_given_pointwise_iso).
 Defined.
 
 Definition given_TM_to_canonical_naturality
@@ -177,7 +178,7 @@ Proof.
   etrans. apply maponpaths, (pr2 Y).
   etrans. use (toforallpaths _ _ _ (!functor_comp (TM Y) _ _ )).
   etrans. apply maponpaths_2; cbn.
-    apply (PullbackArrow_PullbackPr2 (make_Pullback _ _ _ _ _ _ _)). 
+    apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). 
   apply (toforallpaths _ _ _ (functor_id (TM Y) _) _).
 Qed.
 
@@ -229,7 +230,7 @@ Proof.
       etrans. apply maponpaths, YH.
       etrans. use (toforallpaths _ _ _ (!functor_comp tm _ _ )).
       etrans. apply maponpaths_2; cbn.
-        apply (PullbackArrow_PullbackPr2 (make_Pullback _ _ _ _ _ _ _)). 
+        apply (PullbackArrow_PullbackPr2 (make_Pullback _ _)). 
       apply (toforallpaths _ _ _ (functor_id tm _) _).
 Defined.
 
@@ -266,7 +267,7 @@ Proof.
   apply funextsec; intro Γ'.
   apply funextsec; intro f.
   apply funextsec; intro A.    
-  apply (invmaponpathsweq (make_weq _ (yoneda_fully_faithful _ (homset_property _) _ _ ))).
+  apply (invmaponpathsweq (make_weq _ (yoneda_fully_faithful _ _ _ ))).
   apply pathsinv0.
   etrans. apply Yo_qq_term_Yo_of_qq.
   unfold Yo_of_qq.