Upstreamed some material on displayed categories

Author: peterlefanulumsdaine

TypeTheory/ALV2/CwF_SplitTypeCat_Equiv_Cats.v

@@ -25,26 +25,6 @@ Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Maps.
 Require Import TypeTheory.ALV2.CwF_SplitTypeCat_Cats.
 Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Equivalence. (* TODO: needed for some natural transformations. *)
 
-
-(* TODO: globalise upstream? *)
-Notation "# F" := (disp_functor_on_morphisms F)
-  (at level 3) : mor_disp_scope.
-
-(* TODO: as ever, upstream when possible. *)
-Section Auxiliary.
-
-(* The following definition takes unfair advantage of the fact that  [functor_composite (functor_identity _) (functor_identity _)]
-  is judgementally(!) equal to [functor_identity _]. *)
-Definition disp_functor_id_composite
-  {C : category}
-  {CC DD EE : disp_cat C}
-  (FF : disp_functor (functor_identity _) CC DD)
-  (GG : disp_functor (functor_identity _) DD EE)
-: disp_functor (functor_identity _) CC EE
-:= disp_functor_composite FF GG.
-
-End Auxiliary.
-
 Section Fix_Context.
 
 Context {C : category}.

TypeTheory/ALV2/SplitTypeCat_ComprehensionCat.v

@@ -43,6 +43,7 @@ Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 
 Require Import TypeTheory.Auxiliary.Auxiliary.
 Require Import TypeTheory.Auxiliary.CategoryTheory.
+Require Import TypeTheory.Auxiliary.DisplayedCategories.
 Require Import TypeTheory.Auxiliary.Pullbacks.
 
 Require Import TypeTheory.ALV1.TypeCat.
@@ -55,206 +56,6 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
 Require Import UniMath.CategoryTheory.DisplayedCats.ComprehensionC.
 
-Section Auxiliary.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_is_cartesian
-             {C : category}
-             {D : discrete_fibration C} {c c'}
-             (f : c' --> c) (d : D c)
-    : is_cartesian (pr2 (pr1 (unique_lift f d))).
-  Proof.
-    apply (pr2 (pr2 (fibration_from_discrete_fibration _ D _ _ f d))).
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_explicit
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c'}
-             {d : D c} {f : c' --> c} (d' : D c') (ff : d' -->[f] d)
-    : ∃! (d' : D c'), d' -->[f] d.
-  Proof.
-    exists (d' ,, ff).
-    intros X.
-    etrans. apply (pr2 (pr1 is_discrete_fibration_D _ _ f d)).
-    apply pathsinv0, (pr2 (pr1 is_discrete_fibration_D _ _ f d)).
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_explicit_eq
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c'}
-             {d : D c} {f : c' --> c} (d' : D c') (ff : d' -->[f] d)
-    : pr1 is_discrete_fibration_D _ _ f d
-      = unique_lift_explicit is_discrete_fibration_D d' ff.
-  Proof.
-    apply isapropiscontr.
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_identity
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c}
-             (d : D c)
-    : ∃! (d' : D c), d' -->[identity c] d.
-  Proof.
-    apply (unique_lift_explicit is_discrete_fibration_D d).
-    apply id_disp.
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_id
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c}
-             (d : D c)
-    : pr1 is_discrete_fibration_D _ _ (identity c) d
-      = unique_lift_identity is_discrete_fibration_D d.
-  Proof.
-    apply isapropiscontr.
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_compose
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c' c''}
-             (f : c' --> c) (g : c'' --> c')
-             (d : D c)
-    : ∃! (d'' : D c''), d'' -->[g ;; f] d.
-  Proof.
-    set (d'ff := pr1 is_discrete_fibration_D _ _ f d).
-    set (d' := pr1 (pr1 d'ff)).
-    set (ff := pr2 (pr1 d'ff)).
-    set (d''gg := pr1 is_discrete_fibration_D _ _ g d').
-    set (d'' := pr1 (pr1 d''gg)).
-    set (gg := pr2 (pr1 d''gg)).
-
-    use (unique_lift_explicit is_discrete_fibration_D d'' (gg ;; ff)%mor_disp).
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition unique_lift_comp
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c' c''}
-             (f : c' --> c) (g : c'' --> c')
-             (d : D c)
-    : pr1 is_discrete_fibration_D _ _ (g ;; f) d
-      = unique_lift_compose is_discrete_fibration_D f g d.
-  Proof.
-    apply isapropiscontr.
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition discrete_fibration_mor_weq
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c'}
-             (f : c' --> c) (d : D c) (d' : D c')
-    : (d' -->[f] d) ≃ (pr1 (pr1 (pr1 is_discrete_fibration_D c c' f d)) = d').
-  Proof.
-    set (uf := pr1 is_discrete_fibration_D c c' f d).
-    use weq_iso.
-    - intros ff. apply (maponpaths pr1 (! pr2 uf (d' ,, ff))).
-    - intros p. apply (transportf _ p (pr2 (pr1 uf))).
-    - intros ff. simpl.
-      induction (! unique_lift_explicit_eq is_discrete_fibration_D d' ff
-                : unique_lift_explicit _ d' ff = uf).
-      simpl.
-      etrans. apply maponpaths_2, maponpaths, maponpaths.
-      apply pathsinv0r.
-      apply idpath.
-    - intros ?. apply (pr2 is_discrete_fibration_D).
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition discrete_fibration_mor
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c'}
-             (f : c' --> c) (d : D c) (d' : D c')
-    : (d' -->[f] d) = (pr1 (pr1 (pr1 is_discrete_fibration_D c c' f d)) = d').
-  Proof.
-    apply univalenceweq.
-    apply discrete_fibration_mor_weq.
-  Defined.
-
-  (* TODO: move upstream? *)
-  Definition isaprop_mor_disp_of_discrete_fibration
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D) {c c'}
-             (f : c' --> c) (d : D c) (d' : D c')
-    : isaprop (d' -->[f] d).
-  Proof.
-    induction (! discrete_fibration_mor is_discrete_fibration_D f d d').
-    apply (pr2 is_discrete_fibration_D).
-  Qed.
-
-  (* TODO: move upstream? *)
-  Definition isaprop_disp_id_comp_of_discrete_fibration
-             {C : category}
-             {D : disp_cat C}
-             (is_discrete_fibration_D : is_discrete_fibration D)
-    : isaprop (disp_cat_id_comp C D).
-  Proof.
-    use isapropdirprod.
-    - apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply isaprop_mor_disp_of_discrete_fibration.
-      apply is_discrete_fibration_D.
-    - apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply isaprop_mor_disp_of_discrete_fibration.
-      apply is_discrete_fibration_D.
-  Qed.
-
-  (* TODO: move upstream? *)
-  Definition isaprop_is_discrete_fibration
-             {C : category}
-             (D : disp_cat C)
-    : isaprop (is_discrete_fibration D).
-  Proof.
-    use isapropdirprod.
-    - apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply impred_isaprop. intros ?.
-      apply isapropiscontr.
-    - apply impred_isaprop. intros ?.
-      apply isapropisaset.
-  Qed.
-             
-  (* TODO: move upstream? *)
-  Definition isaprop_is_cartesian_disp_functor
-        {C C' : category} {F : functor C C'}
-        {D : disp_cat C} {D' : disp_cat C'} {FF : disp_functor F D D'}
-    : isaprop (is_cartesian_disp_functor FF).
-  Proof.
-    apply impred_isaprop. intros c.
-    apply impred_isaprop. intros c'.
-    apply impred_isaprop. intros f.
-    apply impred_isaprop. intros d.
-    apply impred_isaprop. intros d'.
-    apply impred_isaprop. intros ff.
-    apply impred_isaprop. intros ff_is_cartesian.
-    apply isaprop_is_cartesian.
-  Qed.
-
-End Auxiliary.
-
 Section DiscreteComprehensionCatWithDefaultMor.
 
   Section From_SplitTypeCat.