Library UniMath.Bicategories.ComprehensionCat.Universes.CatWithUniv.UniverseInCat

Universes in categories
In this file, we define the notion of universe within a category. These are Tarski-style universes, meaning that we have a map assigned to each term of the universe an actual type (instead of Russel style universes whose inhabitants are actual types). To define such universes, we first give their core ingredients. These are an object `U` and an map that assigns to each morphism into `U` a type. Concretely, this entails to
  • an object `U`
  • for all morphisms `t : Γ --> U`, a morphism `⌜ t ⌝ : El t --> Γ`
This data is given in cat_el_map.
Next we express stability under substitution of the map `El`. To state that, we use that substitution is interpreted using pullback. More specifically, we express that certain squares are pullbacks. Suppose that we have morphisms `s : Δ --> Γ` and `t : Γ --> U`. Then we have the following 
 El (s · t)         El t
     |                |
     |                |
     V                V
     Δ      ------>   Γ   -----> U
               s            t
To say that `El (s · t)` is the substitution of `El t` along `s`, we say that we have a morphism `sub_U s t : El (s · t) --> El t`, which makes the resulting square a pullback square. This is expressed in cat_el_map_stable.
The final requirement is coherence of substitution. Specifically, we say how the morphism `sub_U s t` acts on the identity and composition of substitutions. The precise definition is given in is_coherent_cat_stable_el_map. All in all, we get a notion of universe in a category with finite limits, which is given in cat_stable_el_map_coherent.
To construct a bicategory of categories with universes, we also define when functors and natural transformations preserve them. Suppose that we have a functor `F : C ⟶ D` and that `C` has a universe `U_1` and that `D` has as universe `U_2`. Then we say that `F` preserves the universe if we have
  • an isomorphism `i : F U_1 ≅ U_2`
  • for each `t : Γ --> U` in `C` we have an isomorphism `j : F (El_1 t) ≅ El_2 (F t · i)` such that the morphisms `F (El_1 t)` and `j · El_2 (F t · i)` are equal.
We also require that the functor `F` preserves the morphisms `sub_U s t : El (s · t) --> El t`. These requirements are expressed in the file `CatWithOb` (i.e., the morphism `i : F U_1 ≅ U_2`), and in the definitions functor_el_map and functor_stable_el_map. Finally, we define when a natural transformation preserves universes (see nat_trans_preserves_el). In this definition, we require that a certain diagram commutes.
Content 1. The map assigning types to terms of the universe 2. Stability 3. Coherence 4. Preservation by functors 5. Identity and compositions preserve universes 6. Functors that preserve stable universes 7. The identity and composition 8. Preservation by natural transformations
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.IdempotentsAndSplitting.Retracts.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.
Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.StructuredCategories.
Require Import UniMath.Bicategories.ComprehensionCat.Universes.CatWithUniv.CatWithOb.

Local Open Scope cat.

1. The map assigning types to terms of the universe

Definition cat_el_map
           (C : univ_cat_with_finlim_ob)
  : UU
  := ∏ (Γ : C),
     Γ --> univ_cat_universe C
     →
     ∑ (e : C), e --> Γ.

Definition cat_el_map_el
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
           {Γ : C}
           (t : Γ --> univ_cat_universe C)
  : C
  := pr1 (el Γ t).

Definition cat_el_map_mor
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
           {Γ : C}
           (t : Γ --> univ_cat_universe C)
  : cat_el_map_el el t --> Γ
  := pr2 (el Γ t).

Definition cat_el_map_slice
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
           {Γ : C}
           (t : Γ --> univ_cat_universe C)
  : C/Γ.
Show proof.
  use make_cod_fib_ob.
  - exact (cat_el_map_el el t).
  - exact (cat_el_map_mor el t).

Definition cat_el_map_el_eq
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
           {Γ : C}
           {t t' : Γ --> univ_cat_universe C}
           (p : t = t')
  : z_iso (cat_el_map_el el t) (cat_el_map_el el t').
Show proof.
  induction p.
  apply identity_z_iso.

Proposition cat_el_map_el_eq_eq
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t t' : Γ --> univ_cat_universe C}
            (p p' : t = t')
  : pr1 (cat_el_map_el_eq el p) = cat_el_map_el_eq el p'.
Show proof.
  assert (p = p') as ->.
  {
    apply homset_property.
  }
  apply idpath.

Proposition cat_el_map_el_eq_id
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t : Γ --> univ_cat_universe C}
            (p : t = t)
  : pr1 (cat_el_map_el_eq el p)
    =
    identity _.
Show proof.
  assert (p = idpath _) as ->.
  {
    apply homset_property.
  }
  apply idpath.

Proposition cat_el_map_el_eq_inv
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t t' : Γ --> univ_cat_universe C}
            (p : t = t')
  : inv_from_z_iso (cat_el_map_el_eq el p)
    =
    cat_el_map_el_eq el (!p).
Show proof.
  induction p ; cbn.
  apply idpath.

Proposition cat_el_map_el_eq_comp
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t t' t'' : Γ --> univ_cat_universe C}
            (p : t = t')
            (q : t' = t'')
  : cat_el_map_el_eq el p · cat_el_map_el_eq el q
    =
    cat_el_map_el_eq el (p @ q).
Show proof.
  induction p, q ; cbn.
  apply id_left.

Proposition cat_el_map_mor_eq
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t t' : Γ --> univ_cat_universe C}
            (p : t = t')
  : cat_el_map_el_eq el p · cat_el_map_mor el t'
    =
    cat_el_map_mor el t.
Show proof.
  induction p ; cbn.
  apply id_left.

Proposition cat_el_map_el_eq_postcomp
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t t' : Γ --> univ_cat_universe C}
            (p₁ p₂ : t = t')
            {x : C}
            {f g : x --> cat_el_map_el el t}
            (q : f = g)
  : f · cat_el_map_el_eq el p₁ = g · cat_el_map_el_eq el p₂.
Show proof.
  induction q.
  apply maponpaths.
  apply cat_el_map_el_eq_eq.

Proposition cat_el_map_el_eq_precomp
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ : C}
            {t t' : Γ --> univ_cat_universe C}
            (p₁ p₂ : t = t')
            {x : C}
            {f g : cat_el_map_el el t' --> x}
            (q : f = g)
  : cat_el_map_el_eq el p₁ · f
    =
    cat_el_map_el_eq el p₂ · g.
Show proof.
  induction q.
  apply maponpaths_2.
  apply cat_el_map_el_eq_eq.

Proposition transportf_cat_el_map_el
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ A : C}
            {f g : Γ --> univ_cat_universe C}
            (p : f = g)
            (h : cat_el_map_el el f --> A)
  : transportf
      (λ (f : Γ --> univ_cat_universe C), cat_el_map_el el f --> A)
      p
      h
    =
    cat_el_map_el_eq el (!p) · h.
Show proof.
  induction p ; cbn.
  rewrite id_left.
  apply idpath.

Proposition transportf_cat_el_map_el'
            {C : univ_cat_with_finlim_ob}
            (el : cat_el_map C)
            {Γ A : C}
            {f g : Γ --> univ_cat_universe C}
            (p : f = g)
            (h : A --> cat_el_map_el el f)
  : transportf
      (λ (f : Γ --> univ_cat_universe C), A --> cat_el_map_el el f)
      p
      h
    =
    h · cat_el_map_el_eq el p.
Show proof.
  induction p ; cbn.
  rewrite id_right.
  apply idpath.

2. Stability

Definition cat_el_map_stable
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
  : UU
  := ∏ (Γ Δ : C)
       (s : Γ --> Δ)
       (t : Δ --> univ_cat_universe C),
     ∑ (f : cat_el_map_el el (s · t) --> cat_el_map_el el t)
       (p : f · cat_el_map_mor el t
            =
            cat_el_map_mor el (s · t) · s),
     isPullback p.

Definition cat_stable_el_map
           (C : univ_cat_with_finlim_ob)
  : UU
  := ∑ (el : cat_el_map C),
     cat_el_map_stable el.

Definition make_cat_stable_el_map
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
           (H_el : cat_el_map_stable el)
  : cat_stable_el_map C
  := el ,, H_el.

Coercion cat_stable_el_map_to_el_map
         {C : univ_cat_with_finlim_ob}
         (el : cat_stable_el_map C)
  : cat_el_map C
  := pr1 el.

Definition cat_el_map_pb_mor
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
           {Γ Δ : C}
           (s : Γ --> Δ)
           (t : Δ --> univ_cat_universe C)
  : cat_el_map_el el (s · t) --> cat_el_map_el el t
  := pr1 (pr2 el Γ Δ s t).

Proposition cat_el_map_pb_mor_comm
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map C)
            {Γ Δ : C}
            (s : Γ --> Δ)
            (t : Δ --> univ_cat_universe C)
  : cat_el_map_pb_mor el s t · cat_el_map_mor el t
    =
    cat_el_map_mor el (s · t) · s.
Show proof.
  exact (pr12 (pr2 el Γ Δ s t)).

Proposition cat_el_map_pb_mor_subst_eq
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map C)
            {Γ Δ : C}
            {s s' : Γ --> Δ}
            (p : s = s')
            (t : Δ --> univ_cat_universe C)
  : cat_el_map_pb_mor el s t
    =
    cat_el_map_el_eq el (maponpaths (λ z, z · t) p)
    · cat_el_map_pb_mor el s' t.
Show proof.
  induction p ; cbn.
  rewrite id_left.
  apply idpath.

Proposition cat_el_map_pb_mor_eq
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map C)
            {Γ Δ : C}
            (s : Γ --> Δ)
            {t t' : Δ --> univ_cat_universe C}
            (p : t' = t)
            (q : s · t' = s · t)
  : cat_el_map_el_eq el q · cat_el_map_pb_mor el s t
    =
    cat_el_map_pb_mor el s t' · cat_el_map_el_eq el p.
Show proof.
  induction p.
  assert (q = idpath _) as ->.
  {
    apply homset_property.
  }
  cbn.
  rewrite id_left, id_right.
  apply idpath.

Definition cat_stable_el_map_pb
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
           {Γ Δ : C}
           (s : Γ --> Δ)
           (t : Δ --> univ_cat_universe C)
  : Pullback (cat_el_map_mor el t) s.
Show proof.
  use make_Pullback.
  - exact (cat_el_map_el el (s · t)).
  - exact (cat_el_map_pb_mor el s t).
  - exact (cat_el_map_mor el (s · t)).
  - exact (cat_el_map_pb_mor_comm el s t).
  - exact (pr22 (pr2 el Γ Δ s t)).

Proposition subst_cat_univ_tm
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map C)
            {Γ Δ : C}
            (s : Γ --> Δ)
            (a : Δ --> univ_cat_universe C)
            (t : section_of_mor (cat_el_map_mor el a))
  : section_of_mor (cat_el_map_mor el (s · a)).
Show proof.
  use make_section_of_mor.
  - use (PullbackArrow (cat_stable_el_map_pb el s a)).
    + exact (s · t).
    + apply identity.
    + abstract
        (rewrite !assoc' ;
         rewrite section_of_mor_eq ;
         rewrite id_left, id_right ;
         apply idpath).
  - abstract
      (apply (PullbackArrow_PullbackPr2 (cat_stable_el_map_pb el s a))).

Definition pb_mor_to_cat_stable_el_map_pb
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
           {Γ Δ : C}
           (s : Γ --> Δ)
           (t : Δ --> univ_cat_universe C)
  : pullbacks_univ_cat_with_finlim C _ _ _ (cat_el_map_mor el t) s
    -->
    cat_el_map_el el (s · t).
Show proof.
  use (PullbackArrow (cat_stable_el_map_pb el s t)).
  - apply PullbackPr1.
  - apply PullbackPr2.
  - abstract
      (apply PullbackSqrCommutes).

3. Coherence

Definition is_coherent_cat_stable_el_map
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
  : UU
  := (∏ (Γ : C)
        (t : Γ --> univ_cat_universe C),
      cat_el_map_pb_mor el (identity _) t
      =
      cat_el_map_el_eq el (id_left _))
     ×
     (∏ (Γ₁ Γ₂ Γ₃ : C)
        (s₁ : Γ₁ --> Γ₂)
        (s₂ : Γ₂ --> Γ₃)
        (t : Γ₃ --> univ_cat_universe C),
       cat_el_map_pb_mor el (s₁ · s₂) t
       =
       cat_el_map_el_eq el (assoc' _ _ _)
       · cat_el_map_pb_mor el s₁ (s₂ · t)
       · cat_el_map_pb_mor el s₂ t).

Proposition isaprop_is_coherent_cat_stable_el_map
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map C)
  : isaprop (is_coherent_cat_stable_el_map el).
Show proof.
  use isapropdirprod.
  - repeat (use impred ; intro).
    apply homset_property.
  - repeat (use impred ; intro).
    apply homset_property.

Definition cat_stable_el_map_coherent
           (C : univ_cat_with_finlim_ob)
  : UU
  := ∑ (el : cat_stable_el_map C),
     is_coherent_cat_stable_el_map el.

Definition make_cat_stable_el_map_coherent
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
           (H : is_coherent_cat_stable_el_map el)
  : cat_stable_el_map_coherent C
  := el ,, H.

Coercion cat_stable_el_map_coherent_to_el_map
         {C : univ_cat_with_finlim_ob}
         (el : cat_stable_el_map_coherent C)
  : cat_stable_el_map C
  := pr1 el.

Proposition cat_el_map_pb_mor_id
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map_coherent C)
            {Γ : C}
            (t : Γ --> univ_cat_universe C)
  : cat_el_map_pb_mor el (identity _) t
    =
    cat_el_map_el_eq el (id_left _).
Show proof.
  exact (pr12 el Γ t).

Proposition cat_el_map_pb_mor_id'_path
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map_coherent C)
            {Γ : C}
            {s : Γ --> Γ}
            {t : Γ --> univ_cat_universe C}
            (p : identity _ = s)
  : s · t = t.
Show proof.
  rewrite <- p.
  apply id_left.

Proposition cat_el_map_pb_mor_id'
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map_coherent C)
            {Γ : C}
            (s : Γ --> Γ)
            (t : Γ --> univ_cat_universe C)
            (p : identity _ = s)
  : cat_el_map_pb_mor el s t
    =
    cat_el_map_el_eq el (cat_el_map_pb_mor_id'_path el p).
Show proof.
  induction p.
  refine (cat_el_map_pb_mor_id el t @ _).
  apply cat_el_map_el_eq_eq.

Proposition cat_el_map_pb_mor_comp
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map_coherent C)
            {Γ₁ Γ₂ Γ₃ : C}
            (s₁ : Γ₁ --> Γ₂)
            (s₂ : Γ₂ --> Γ₃)
            (t : Γ₃ --> univ_cat_universe C)
  : cat_el_map_pb_mor el (s₁ · s₂) t
    =
    cat_el_map_el_eq el (assoc' _ _ _)
    · cat_el_map_pb_mor el s₁ (s₂ · t)
    · cat_el_map_pb_mor el s₂ t.
Show proof.
  exact (pr22 el Γ₁ Γ₂ Γ₃ s₁ s₂ t).

Proposition cat_el_map_pb_mor_comp'
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map_coherent C)
            {Γ₁ Γ₂ Γ₃ : C}
            (s₁ : Γ₁ --> Γ₂)
            (s₂ : Γ₂ --> Γ₃)
            (t : Γ₃ --> univ_cat_universe C)
  : cat_el_map_pb_mor el s₁ (s₂ · t)
    · cat_el_map_pb_mor el s₂ t
    =
    cat_el_map_el_eq el (assoc _ _ _)
    · cat_el_map_pb_mor el (s₁ · s₂) t.
Show proof.
  rewrite cat_el_map_pb_mor_comp.
  refine (!_).
  refine (assoc _ _ _ @ _).
  etrans.
  {

    apply maponpaths_2.
    refine (assoc _ _ _ @ _).
    apply maponpaths_2.
    rewrite cat_el_map_el_eq_comp.
    apply cat_el_map_el_eq_id.
  }
  rewrite id_left.
  apply idpath.

This lemma calculates the necessary transport for an equality principle
Proposition transportf_cat_el_map
            {C : univ_cat_with_finlim_ob}
            {Γ₁ Γ₂ : C}
            {el₁ el₂ : cat_el_map C}
            (p : el₁ = el₂)
            (t : Γ₂ --> univ_cat_universe C)
            (s : Γ₁ --> Γ₂)
            (f : cat_el_map_el el₁ (s · t) --> cat_el_map_el el₁ t)
  : transportf
      (λ (el : cat_el_map C), cat_el_map_el el (s · t) --> cat_el_map_el el t)
      p
      f
    =
    idtoiso (!base_paths _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ p _) (s · t)))
    · f
    · idtoiso (base_paths _ _ (toforallpaths _ _ _ (toforallpaths _ _ _ p _) t)).
Show proof.
  induction p ; cbn.
  rewrite id_left, id_right.
  apply idpath.

Proposition cat_el_map_eq_weq
            {C : univ_cat_with_finlim_ob}
            (el₁ el₂ : cat_stable_el_map_coherent C)
  : (el₁ = el₂)
    ≃
    ∑ (pq : ∏ (Γ : C)
              (t : Γ --> univ_cat_universe C),
            ∑ (p : z_iso (cat_el_map_el el₁ t) (cat_el_map_el el₂ t)),
            p · cat_el_map_mor el₂ t
            =
            cat_el_map_mor el₁ t),
    (∏ (Γ Δ : C)
       (s : Γ --> Δ)
       (t : Δ --> univ_cat_universe C),
     cat_el_map_pb_mor el₁ s t · pr1 (pq _ _)
     =
     pr1 (pq _ _) · cat_el_map_pb_mor el₂ s t).
Show proof.
  induction el₁ as [ el₁ H₁ ].
  induction el₂ as [ el₂ H₂ ].
  induction el₁ as [ el₁ r₁ ].
  induction el₂ as [ el₂ r₂ ].
  refine (_ ∘ path_sigma_hprop _ _ _ _)%weq.
  {
    apply isaprop_is_coherent_cat_stable_el_map.
  }
  refine (_ ∘ total2_paths_equiv _ _ _)%weq.
  use weqtotal2.
  - refine (_ ∘ weqtoforallpaths _ _ _)%weq.
    use weqonsecfibers.
    intro Γ.
    refine (_ ∘ weqtoforallpaths _ _ _)%weq.
    use weqonsecfibers.
    intro t ; cbn.
    refine (_ ∘ total2_paths_equiv _ _ _)%weq.
    use weqtotal2.
    + use make_weq.
      * exact (λ p, idtoiso p).
      * apply univalent_category_is_univalent.
    + intro p ; cbn ; cbn in p.
      use weqimplimpl.
      * rewrite <- idtoiso_precompose.
        intro r.
        refine (maponpaths (λ z, _ · z) (!r) @ _).
        rewrite assoc.
        refine (maponpaths (λ z, z · _) (!(pr1_idtoiso_concat _ _)) @ _).
        rewrite pathsinv0r.
        apply id_left.
      * rewrite <- idtoiso_precompose.
        intro r.
        refine (maponpaths (λ z, _ · z) (!r) @ _).
        rewrite assoc.
        refine (maponpaths (λ z, z · _) (!(pr1_idtoiso_concat _ _)) @ _).
        rewrite pathsinv0l.
        apply id_left.
      * apply homset_property.
      * apply homset_property.
  - intro p ; cbn in p.
    induction p ; cbn.
    refine (_ ∘ weqtoforallpaths _ _ _)%weq.
    use weqonsecfibers.
    intros Γ.
    refine (_ ∘ weqtoforallpaths _ _ _)%weq.
    use weqonsecfibers.
    intros Δ.
    refine (_ ∘ weqtoforallpaths _ _ _)%weq.
    use weqonsecfibers.
    intros s.
    refine (_ ∘ weqtoforallpaths _ _ _)%weq.
    use weqonsecfibers.
    intros t ; cbn.
    unfold cat_el_map_pb_mor ; cbn.
    refine (_ ∘ path_sigma_hprop _ _ _ _)%weq.
    {
      use isaproptotal2.
      {
        intro.
        apply isaprop_isPullback.
      }
      intros.
      apply homset_property.
    }
    use weqimplimpl.
    + abstract
        (intro p ;
         rewrite id_right, id_left ;
         exact p).
    + abstract
        (rewrite id_right, id_left ;
         intro p ;
         exact p).
    + apply homset_property.
    + apply homset_property.

Proposition cat_el_map_eq
            {C : univ_cat_with_finlim_ob}
            {el₁ el₂ : cat_stable_el_map_coherent C}
            (p : ∏ (Γ : C)
                   (t : Γ --> univ_cat_universe C),
                 z_iso (cat_el_map_el el₁ t) (cat_el_map_el el₂ t))
            (q : ∏ (Γ : C)
                   (t : Γ --> univ_cat_universe C),
                 p Γ t · cat_el_map_mor el₂ t
                 =
                 cat_el_map_mor el₁ t)
             (r : ∏ (Γ Δ : C)
                    (s : Γ --> Δ)
                    (t : Δ --> univ_cat_universe C),
                  cat_el_map_pb_mor el₁ s t · p _ _
                  =
                  p _ _ · cat_el_map_pb_mor el₂ s t)
  : el₁ = el₂.
Show proof.
  use (invmap (cat_el_map_eq_weq el₁ el₂)).
  exact ((λ Γ t, p Γ t ,, q Γ t) ,, r).

Section SubstIso.
  Context {C : univ_cat_with_finlim_ob}
          (el : cat_stable_el_map_coherent C)
          {Γ₁ Γ₂ : C}
          (s : z_iso Γ₁ Γ₂)
          (t : Γ₂ --> univ_cat_universe C).

  Definition cat_el_map_pb_mor_inv
    : cat_el_map_el el t --> cat_el_map_el el (s · t).
  Show proof.
    refine (cat_el_map_el_eq el _ · cat_el_map_pb_mor el (inv_from_z_iso s) (s · t)).
    abstract
      (rewrite !assoc ;
       rewrite z_iso_after_z_iso_inv ;
       rewrite id_left ;
       apply idpath).

  Arguments cat_el_map_pb_mor_inv /.

  Proposition cat_el_map_pb_mor_inv_laws
    : is_inverse_in_precat
        (cat_el_map_pb_mor el s t)
        cat_el_map_pb_mor_inv.
  Show proof.
    cbn.
    split.
    - rewrite !assoc.
      etrans.
      {
        apply maponpaths_2.
        refine (!_).
        use cat_el_map_pb_mor_eq.
        abstract
          (rewrite !assoc ;
           rewrite z_iso_inv_after_z_iso ;
           rewrite id_left ;
           apply idpath).
      }
      rewrite !assoc'.
      rewrite (cat_el_map_pb_mor_comp' el).
      refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        apply cat_el_map_el_eq_comp.
      }
      etrans.
      {
        apply maponpaths.
        use cat_el_map_pb_mor_id'.
        rewrite z_iso_inv_after_z_iso.
        apply idpath.
      }
      rewrite cat_el_map_el_eq_comp.
      apply cat_el_map_el_eq_id.
    - rewrite !assoc'.
      rewrite (cat_el_map_pb_mor_comp' el).
      refine (assoc _ _ _ @ _).
      etrans.
      {
        apply maponpaths_2.
        apply cat_el_map_el_eq_comp.
      }
      etrans.
      {
        apply maponpaths.
        use cat_el_map_pb_mor_id'.
        rewrite z_iso_after_z_iso_inv.
        apply idpath.
      }
      rewrite cat_el_map_el_eq_comp.
      apply cat_el_map_el_eq_id.

  Definition is_z_isomorphism_cat_el_map_pb_mor
    : is_z_isomorphism (cat_el_map_pb_mor el s t).
  Show proof.
    use make_is_z_isomorphism.
    - exact cat_el_map_pb_mor_inv.
    - exact cat_el_map_pb_mor_inv_laws.

  Definition cat_el_map_pb_mor_z_iso
    : z_iso (cat_el_map_el el (s · t)) (cat_el_map_el el t)
    := cat_el_map_pb_mor el s t ,, is_z_isomorphism_cat_el_map_pb_mor.
End SubstIso.

4. Preservation by functors

Definition functor_el_map
           {C₁ C₂ : univ_cat_with_finlim_ob}
           (el₁ : cat_el_map C₁)
           (el₂ : cat_el_map C₂)
           (F : functor_finlim_ob C₁ C₂)
  : UU
  := ∏ (Γ : C₁)
       (t : Γ --> univ_cat_universe C₁),
     ∑ (f : z_iso
              (F (cat_el_map_el el₁ t))
              (cat_el_map_el el₂ (#F t · functor_on_universe F))),
     #F (cat_el_map_mor el₁ t)
     =
     f
     · cat_el_map_mor el₂ (#F t · functor_on_universe F).

Proposition isaset_functor_el_map
            {C₁ C₂ : univ_cat_with_finlim_ob}
            (el₁ : cat_el_map C₁)
            (el₂ : cat_el_map C₂)
            (F : functor_finlim_ob C₁ C₂)
  : isaset (functor_el_map el₁ el₂ F).
Show proof.
  do 2 (use impred_isaset ; intro).
  use isaset_total2.
  - apply isaset_z_iso.
  - intro.
    apply isasetaprop.
    apply homset_property.

Definition functor_el_map_iso
           {C₁ C₂ : univ_cat_with_finlim_ob}
           {el₁ : cat_el_map C₁}
           {el₂ : cat_el_map C₂}
           {F : functor_finlim_ob C₁ C₂}
           (Fel : functor_el_map el₁ el₂ F)
           {Γ : C₁}
           (t : Γ --> univ_cat_universe C₁)
  : z_iso
      (F (cat_el_map_el el₁ t))
      (cat_el_map_el el₂ (#F t · functor_on_universe F))
  := pr1 (Fel Γ t).

Proposition functor_el_map_iso_eq_path
            {C₁ C₂ : univ_cat_with_finlim_ob}
            (F : functor_finlim_ob C₁ C₂)
            {Γ : C₁}
            {t₁ t₂ : Γ --> univ_cat_universe C₁}
            (p : t₁ = t₂)
  : #F t₁ · functor_on_universe F
    =
    #F t₂ · functor_on_universe F.
Show proof.
  induction p.
  apply idpath.

Proposition functor_el_map_iso_eq
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {el₁ : cat_el_map C₁}
            {el₂ : cat_el_map C₂}
            {F : functor_finlim_ob C₁ C₂}
            (Fel : functor_el_map el₁ el₂ F)
            {Γ : C₁}
            {t₁ t₂ : Γ --> univ_cat_universe C₁}
            (p : t₁ = t₂)
  : pr1 (functor_el_map_iso Fel t₂)
    =
    #F (cat_el_map_el_eq el₁ (!p))
    · functor_el_map_iso Fel t₁
    · (cat_el_map_el_eq el₂ (functor_el_map_iso_eq_path F p)).
Show proof.
  induction p ; cbn.
  rewrite functor_id.
  rewrite id_left, id_right.
  apply idpath.

Proposition functor_el_map_iso_eq_alt
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {el₁ : cat_el_map C₁}
            {el₂ : cat_el_map C₂}
            {F : functor_finlim_ob C₁ C₂}
            (Fel : functor_el_map el₁ el₂ F)
            {Γ : C₁}
            {t₁ t₂ : Γ --> univ_cat_universe C₁}
            (p : t₁ = t₂)
  : #F (cat_el_map_el_eq el₁ p)
    · pr1 (functor_el_map_iso Fel t₂)
    =
    functor_el_map_iso Fel t₁
    · (cat_el_map_el_eq el₂ (functor_el_map_iso_eq_path F p)).
Show proof.
  etrans.
  {
    apply maponpaths.
    exact (functor_el_map_iso_eq Fel p).
  }
  rewrite !assoc.
  apply maponpaths_2.
  refine (_ @ id_left _).
  apply maponpaths_2.
  rewrite <- functor_id.
  rewrite <- functor_comp.
  apply maponpaths.
  rewrite cat_el_map_el_eq_comp.
  apply cat_el_map_el_eq_id.

Proposition functor_on_cat_el_map_el_eq
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {el₁ : cat_el_map C₁}
            {el₂ : cat_el_map C₂}
            {F : functor_finlim_ob C₁ C₂}
            (Fel : functor_el_map el₁ el₂ F)
            {Γ : C₁}
            {t₁ t₂ : Γ --> univ_cat_universe C₁}
            (p : t₁ = t₂)
  : #F (cat_el_map_el_eq el₁ p)
    =
    functor_el_map_iso Fel t₁
    · cat_el_map_el_eq el₂ (functor_el_map_iso_eq_path F p)
    · inv_from_z_iso (functor_el_map_iso Fel t₂).
Show proof.
  induction p ; cbn.
  rewrite functor_id.
  rewrite id_right.
  rewrite z_iso_inv_after_z_iso.
  apply idpath.

Proposition functor_el_map_comm
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {el₁ : cat_el_map C₁}
            {el₂ : cat_el_map C₂}
            {F : functor_finlim_ob C₁ C₂}
            (Fel : functor_el_map el₁ el₂ F)
            {Γ : C₁}
            (t : Γ --> univ_cat_universe C₁)
  : #F (cat_el_map_mor el₁ t)
    =
    functor_el_map_iso Fel t
    · cat_el_map_mor el₂ (#F t · functor_on_universe F).
Show proof.
  exact (pr2 (Fel Γ t)).

Definition make_functor_el_map
           {C₁ C₂ : univ_cat_with_finlim_ob}
           {el₁ : cat_el_map C₁}
           {el₂ : cat_el_map C₂}
           {F : functor_finlim_ob C₁ C₂}
           (f : ∏ (Γ : C₁) (t : Γ --> univ_cat_universe C₁),
                z_iso
                  (F (cat_el_map_el el₁ t))
                  (cat_el_map_el el₂ (#F t · functor_on_universe F)))
           (p : ∏ (Γ : C₁) (t : Γ --> univ_cat_universe C₁),
                #F (cat_el_map_mor el₁ t)
                =
                f Γ t
                · cat_el_map_mor el₂ (#F t · functor_on_universe F))
  : functor_el_map el₁ el₂ F
  := λ Γ t, f Γ t ,, p Γ t.

5. Identity and compositions preserve universes

Definition id_functor_el_map
           {C : univ_cat_with_finlim_ob}
           (el : cat_el_map C)
  : functor_el_map el el (id₁ C).
Show proof.
  use make_functor_el_map.
  - intros Γ t.
    use make_z_iso.
    + exact (cat_el_map_el_eq el (!(id_right _))).
    + exact (cat_el_map_el_eq el (id_right _)).
    + abstract
        (split ;
         cbn ;
         rewrite cat_el_map_el_eq_comp ;
         [ rewrite pathsinv0l | rewrite pathsinv0r ] ;
         apply idpath).
  - abstract
      (intros Γ t ;
       cbn ;
       rewrite cat_el_map_mor_eq ;
       apply idpath).

Proposition comp_functor_el_map_path
            {C₁ C₂ C₃ : univ_cat_with_finlim_ob}
            (F : functor_finlim_ob C₁ C₂)
            (G : functor_finlim_ob C₂ C₃)
            {Γ : C₁}
            (t : Γ --> univ_cat_universe C₁)
  : #G(#F t · functor_on_universe F) · functor_on_universe G
    =
    #G(#F t) · (#G (functor_on_universe F) · functor_on_universe G).
Show proof.
  rewrite functor_comp.
  rewrite !assoc'.
  apply idpath.

Definition comp_functor_el_map
           {C₁ C₂ C₃ : univ_cat_with_finlim_ob}
           {F : functor_finlim_ob C₁ C₂}
           {G : functor_finlim_ob C₂ C₃}
           {el₁ : cat_el_map C₁}
           {el₂ : cat_el_map C₂}
           {el₃ : cat_el_map C₃}
           (Fel : functor_el_map el₁ el₂ F)
           (Gel : functor_el_map el₂ el₃ G)
  : functor_el_map el₁ el₃ (F · G).
Show proof.
  use make_functor_el_map.
  - intros Γ t.
    refine (z_iso_comp
              (functor_on_z_iso G (functor_el_map_iso Fel t))
              _).
    refine (z_iso_comp
              (functor_el_map_iso Gel _)
              (cat_el_map_el_eq el₃ _)).
    apply (comp_functor_el_map_path F G t).
  - abstract
      (intros Γ t ; cbn ;
       refine (maponpaths (λ z, #G z) (functor_el_map_comm Fel t) @ _) ;
       rewrite functor_comp ;
       rewrite !assoc' ;
       apply maponpaths ;
       refine (functor_el_map_comm Gel _ @ _) ;
       apply maponpaths ;
       refine (!_) ;
       apply cat_el_map_mor_eq).

Proposition comp_functor_el_map_on_tm
            {C₁ C₂ C₃ : univ_cat_with_finlim_ob}
            {F : functor_finlim_ob C₁ C₂}
            {G : functor_finlim_ob C₂ C₃}
            {el₁ : cat_el_map C₁}
            {el₂ : cat_el_map C₂}
            {el₃ : cat_el_map C₃}
            (Fel : functor_el_map el₁ el₂ F)
            (Gel : functor_el_map el₂ el₃ G)
            {Γ : C₁}
            (t : Γ --> univ_cat_universe C₁)
  : (functor_el_map_iso (comp_functor_el_map Fel Gel) t : _ --> _)
    =
    #G(functor_el_map_iso Fel t)
    · functor_el_map_iso Gel _
    · cat_el_map_el_eq el₃ (comp_functor_el_map_path F G t).
Show proof.
  apply assoc.

6. Functors that preserve stable universes

Proposition functor_stable_el_map_path
            {C₁ C₂ : univ_cat_with_finlim_ob}
            (F : functor_finlim_ob C₁ C₂)
            {Γ Δ : C₁}
            (s : Γ --> Δ)
            (t : Δ --> univ_cat_universe C₁)
  : # F (s · t) · functor_on_universe F
    =
    # F s · (# F t · functor_on_universe F).
Show proof.
  rewrite functor_comp, assoc'.
  apply idpath.

Definition functor_stable_el_map
           {C₁ C₂ : univ_cat_with_finlim_ob}
           {el₁ : cat_stable_el_map C₁}
           {el₂ : cat_stable_el_map C₂}
           {F : functor_finlim_ob C₁ C₂}
           (Fel : functor_el_map el₁ el₂ F)
  : UU
  := ∏ (Γ Δ : C₁)
       (s : Γ --> Δ)
       (t : Δ --> univ_cat_universe C₁),
     #F (cat_el_map_pb_mor el₁ s t)
     · functor_el_map_iso Fel t
     =
     functor_el_map_iso Fel _
     · cat_el_map_el_eq el₂ (functor_stable_el_map_path F s t)
     · cat_el_map_pb_mor el₂ (#F s) (# F t · functor_on_universe F).

Proposition isaprop_functor_stable_el_map
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {el₁ : cat_stable_el_map C₁}
            {el₂ : cat_stable_el_map C₂}
            {F : functor_finlim_ob C₁ C₂}
            (Fel : functor_el_map el₁ el₂ F)
  : isaprop (functor_stable_el_map Fel).
Show proof.
  repeat (use impred ; intro).
  apply homset_property.

Definition functor_preserves_el
           {C₁ C₂ : univ_cat_with_finlim_ob}
           (el₁ : cat_stable_el_map C₁)
           (el₂ : cat_stable_el_map C₂)
           (F : functor_finlim_ob C₁ C₂)
  : UU
  := ∑ (Fel : functor_el_map el₁ el₂ F),
     functor_stable_el_map Fel.

Proposition isaset_functor_preserves_el
            {C₁ C₂ : univ_cat_with_finlim_ob}
            (el₁ : cat_stable_el_map C₁)
            (el₂ : cat_stable_el_map C₂)
            (F : functor_finlim_ob C₁ C₂)
  : isaset (functor_preserves_el el₁ el₂ F).
Show proof.
  use isaset_total2.
  - apply isaset_functor_el_map.
  - intro.
    apply isasetaprop.
    apply isaprop_functor_stable_el_map.

Coercion functor_preserves_el_to_el_map
         {C₁ C₂ : univ_cat_with_finlim_ob}
         {el₁ : cat_stable_el_map C₁}
         {el₂ : cat_stable_el_map C₂}
         {F : functor_finlim_ob C₁ C₂}
         (Fel : functor_preserves_el el₁ el₂ F)
  : functor_el_map el₁ el₂ F
  := pr1 Fel.

Proposition functor_preserves_el_path
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {el₁ : cat_stable_el_map C₁}
            {el₂ : cat_stable_el_map C₂}
            {F : functor_finlim_ob C₁ C₂}
            (Fel : functor_preserves_el el₁ el₂ F)
            {Γ Δ : C₁}
            (s : Γ --> Δ)
            (t : Δ --> univ_cat_universe C₁)
  : #F (cat_el_map_pb_mor el₁ s t)
    · functor_el_map_iso Fel t
    =
    functor_el_map_iso Fel _
    · cat_el_map_el_eq el₂ (functor_stable_el_map_path F s t)
    · cat_el_map_pb_mor el₂ (#F s) (# F t · functor_on_universe F).
Show proof.
  exact (pr2 Fel Γ Δ s t).

Definition make_functor_preserves_el
           {C₁ C₂ : univ_cat_with_finlim_ob}
           {el₁ : cat_stable_el_map C₁}
           {el₂ : cat_stable_el_map C₂}
           {F : functor_finlim_ob C₁ C₂}
           (Fel : functor_el_map el₁ el₂ F)
           (Fp : functor_stable_el_map Fel)
  : functor_preserves_el el₁ el₂ F
  := Fel ,, Fp.

Definition functor_finlim_on_universe_tm
           {C₁ C₂ : univ_cat_with_finlim_ob}
           {el₁ : cat_stable_el_map_coherent C₁}
           {el₂ : cat_stable_el_map_coherent C₂}
           {F : functor_finlim_ob C₁ C₂}
           (Fel : functor_preserves_el el₁ el₂ F)
           {Γ : C₁}
           {a : Γ --> univ_cat_universe C₁}
           (t : section_of_mor (cat_el_map_mor el₁ a))
  : section_of_mor (cat_el_map_mor el₂ (#F a · functor_on_universe F)).
Show proof.
  use make_section_of_mor.
  - exact (#F t · functor_el_map_iso Fel _).
  - abstract
      (cbn ;
       unfold is_retraction ;
       rewrite !assoc' ;
       rewrite <- functor_el_map_comm ;
       rewrite <- functor_comp ;
       rewrite section_of_mor_eq ;
       apply functor_id).

7. The identity and composition

Definition id_functor_stable_el_map
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
  : functor_stable_el_map (id_functor_el_map el).
Show proof.
  intros Γ Δ s t.
  etrans.
  {
    refine (!_).
    use cat_el_map_pb_mor_eq.
    abstract
      (rewrite id_right ;
       apply idpath).
  }
  apply maponpaths_2.
  refine (_ @ !(cat_el_map_el_eq_comp _ _ _)).
  apply cat_el_map_el_eq_eq.

Definition id_functor_preserves_el
           {C : univ_cat_with_finlim_ob}
           (el : cat_stable_el_map C)
  : functor_preserves_el el el (id₁ _).
Show proof.
  use make_functor_preserves_el.
  - apply id_functor_el_map.
  - apply id_functor_stable_el_map.

Proposition id_functor_el_map_iso
            {C : univ_cat_with_finlim_ob}
            (el : cat_stable_el_map C)
            {Γ : C}
            (t : Γ --> univ_cat_universe C)
  : pr1 (functor_el_map_iso (id_functor_preserves_el el) t)
    =
    cat_el_map_el_eq el (!(id_right _)).
Show proof.
  apply idpath.

Proposition comp_functor_stable_el_map
            {C₁ C₂ C₃ : univ_cat_with_finlim_ob}
            {F : functor_finlim_ob C₁ C₂}
            {G : functor_finlim_ob C₂ C₃}
            {el₁ : cat_stable_el_map C₁}
            {el₂ : cat_stable_el_map C₂}
            {el₃ : cat_stable_el_map C₃}
            (Fel : functor_preserves_el el₁ el₂ F)
            (Gel : functor_preserves_el el₂ el₃ G)
  : functor_stable_el_map (comp_functor_el_map Fel Gel).
Show proof.
  intros Γ Δ s t.
  cbn.
  do 2 refine (assoc _ _ _ @ _).
  rewrite <- functor_comp.
  rewrite (functor_preserves_el_path Fel).
  etrans.
  {
    do 2 apply maponpaths_2.
    do 2 rewrite (functor_comp G).
    apply idpath.
  }
  rewrite !assoc'.
  apply maponpaths.
  etrans.
  {
    apply maponpaths.
    refine (assoc _ _ _ @ _).
    rewrite (functor_preserves_el_path Gel).
    apply idpath.
  }
  rewrite !assoc'.
  etrans.
  {
    do 3 apply maponpaths.
    refine (!_).
    use cat_el_map_pb_mor_eq.
    {
      apply maponpaths.
      rewrite functor_comp.
      rewrite !assoc'.
      apply idpath.
    }
  }
  do 3 refine (assoc _ _ _ @ _).
  do 2 refine (_ @ assoc' _ _ _).
  apply maponpaths_2.
  do 2 refine (assoc' _ _ _ @ _).
  refine (_ @ assoc _ _ _).
  rewrite !cat_el_map_el_eq_comp.
  refine (!_).
  etrans.
  {
    apply maponpaths_2.
    use functor_el_map_iso_eq.
    {
      exact (# F s · (# F t · functor_on_universe F)).
    }
    rewrite !assoc.
    rewrite functor_comp.
    apply idpath.
  }
  do 2 refine (assoc' _ _ _ @ _).
  rewrite cat_el_map_el_eq_comp.
  refine (assoc _ _ _ @ _ @ assoc' _ _ _).
  use cat_el_map_el_eq_postcomp.
  apply maponpaths_2.
  apply maponpaths.
  apply cat_el_map_el_eq_eq.

Definition comp_functor_preserves_el
           {C₁ C₂ C₃ : univ_cat_with_finlim_ob}
           {F : functor_finlim_ob C₁ C₂}
           {G : functor_finlim_ob C₂ C₃}
           {el₁ : cat_stable_el_map C₁}
           {el₂ : cat_stable_el_map C₂}
           {el₃ : cat_stable_el_map C₃}
           (Fel : functor_preserves_el el₁ el₂ F)
           (Gel : functor_preserves_el el₂ el₃ G)
  : functor_preserves_el el₁ el₃ (F · G).
Show proof.
  use make_functor_preserves_el.
  - exact (comp_functor_el_map Fel Gel).
  - exact (comp_functor_stable_el_map Fel Gel).

Definition comp_functor_el_map_iso
           {C₁ C₂ C₃ : univ_cat_with_finlim_ob}
           {F : functor_finlim_ob C₁ C₂}
           {G : functor_finlim_ob C₂ C₃}
           {el₁ : cat_stable_el_map C₁}
           {el₂ : cat_stable_el_map C₂}
           {el₃ : cat_stable_el_map C₃}
           (Fel : functor_preserves_el el₁ el₂ F)
           (Gel : functor_preserves_el el₂ el₃ G)
           {Γ : C₁}
           (t : Γ --> univ_cat_universe C₁)
  : pr1 (functor_el_map_iso (comp_functor_preserves_el Fel Gel) t)
    =
    #G(functor_el_map_iso Fel t)
    · functor_el_map_iso Gel _
    · cat_el_map_el_eq el₃ (comp_functor_el_map_path F G t).
Show proof.
  cbn.
  apply assoc.

8. Preservation by natural transformations

Proposition nat_trans_preserves_el_path
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {F G : functor_finlim_ob C₁ C₂}
            (τ : nat_trans_finlim_ob F G)
            {Γ : C₁}
            (t : Γ --> univ_cat_universe C₁)
  : # F t · functor_on_universe F = τ Γ · (# G t · functor_on_universe G).
Show proof.
  rewrite <- (nat_trans_universe_eq τ).
  rewrite assoc.
  rewrite (nat_trans_ax τ _ _ t).
  rewrite assoc'.
  apply idpath.

Definition nat_trans_preserves_el
           {C₁ C₂ : univ_cat_with_finlim_ob}
           {F G : functor_finlim_ob C₁ C₂}
           (τ : nat_trans_finlim_ob F G)
           {el₁ : cat_stable_el_map C₁}
           {el₂ : cat_stable_el_map C₂}
           (Fe : functor_preserves_el el₁ el₂ F)
           (Ge : functor_preserves_el el₁ el₂ G)
  : UU
  := ∏ (Γ : C₁)
       (t : Γ --> univ_cat_universe C₁),
     τ _ · functor_el_map_iso Ge t
     =
     functor_el_map_iso Fe t
     · cat_el_map_el_eq el₂ (nat_trans_preserves_el_path τ t)
     · cat_el_map_pb_mor _ (τ Γ) _.

Proposition isaprop_nat_trans_preserves_el
            {C₁ C₂ : univ_cat_with_finlim_ob}
            {F G : functor_finlim_ob C₁ C₂}
            (τ : nat_trans_finlim_ob F G)
            {el₁ : cat_stable_el_map C₁}
            {el₂ : cat_stable_el_map C₂}
            (Fe : functor_preserves_el el₁ el₂ F)
            (Ge : functor_preserves_el el₁ el₂ G)
  : isaprop (nat_trans_preserves_el τ Fe Ge).
Show proof.
  do 2 (use impred ; intro).
  apply homset_property.