Library UniMath.CategoryTheory.ComprehensionCats.CompCatUniverse

Universe in Comprehension Categories

Let C be a comprehension category with a terminal empty context ☐. We say C has a universe if we have :

U : ty ☐, which gives rise to UΓ : ty Γ
a function el : tm UΓ ➙ ty Γ
for each s : Γ → Δ and t : tm UΔ, an isomorphism i : el (t) s ≃ el (ts)

such that i commutes with i_id and i_comp.

This definition is similar to the definition of universe in comprehension bicategories presented in "The Internal Language of Univalent Categories" by Van der Weide. A similar definition for CwFs is presented in "Principles of Dependent Type Theory" by Angiuli and Gratzer.

We also define the universe being closed type formers similar to Van der Weide. For closure under type formers, we omit the coherences of the isomorphisms in this formalisation.

References

"The Internal Languages of Univalent Categories" by Van der Weide
"Principles of Dependent Type Theory" by Angiuli and Gratzer

Contents 1. Empty Context in Comprehension Categories 2. Comprehension Category with a Universe 3. Universes being closed under type formers: Σ, unit, Π

Comprehension category with a terminal context

Definition comp_cat_with_terminal : UU := ∑ (C : comp_cat ), Terminal C.

Coercion comp_cat_with_terminal_to_comp_cat (C : comp_cat_with_terminal) : comp_cat := pr1 C.

Definition empty_context (C : comp_cat_with_terminal) : Terminal C := pr2 C.

Notation "'[]'" := (empty_context _) : comp_cat.

Definition weakened_from_empty {C: comp_cat_with_terminal} (A : comp_cat_ty ([] : C)) (Γ : C)
  : comp_cat_ty Γ
  := A [[ TerminalArrow (empty_context C) Γ ]].

Definition sub_comp_cat_univ_iso {C : comp_cat_with_terminal} {Γ Δ : C}
  (U : comp_cat_ty []) (s : Γ --> Δ)
  : z_iso (C := fiber_category _ _) ((weakened_from_empty U _) [[ s ]]) (weakened_from_empty U Γ).
Proof.
  set (T := empty_context C).
  set (tΔ := TerminalArrow T Δ : Δ --> ([] : C)).
  set (tΓ := TerminalArrow T Γ : Γ --> ([] : C)).
  assert (p : s · tΔ = tΓ) by apply TerminalArrowEq.

  refine (z_iso_comp (comp_cat_subst_ty_comp_iso U tΔ s) _).
  exact (comp_cat_subst_ty_iso U p).
Defined.

Comprehension category with a terminal context and universe

lemmas about universe data

Universe Being Closed under Sigma-Types

Section Universe_Sigma_Closure.

  Context (C : comp_cat_with_universe).
  Context (Σ : comp_cat_sigma C).

  Definition univ_sigma_form : UU :=
    ∏ (Γ : C)
      (A : comp_cat_tm (comp_cat_U Γ))
      (B : comp_cat_tm (comp_cat_U (Γ & comp_cat_el A))),
      comp_cat_tm (comp_cat_U Γ).

  Definition univ_sigma_el_iso (ΣU : univ_sigma_form) : UU :=
    ∏ (Γ : C)
      (A : comp_cat_tm (comp_cat_U _))
      (B : comp_cat_tm (comp_cat_U _)),
      @z_iso (fiber_category _ _) (comp_cat_el (ΣU Γ A B))
        ((pr1 Σ) Γ (comp_cat_el A) (comp_cat_el B)).

  Definition univ_sigma_subst_law (ΣU : univ_sigma_form) : UU :=
    ∏ (Γ Δ : C) (s : Γ --> Δ)
      (A : comp_cat_tm (comp_cat_U _))
      (B : comp_cat_tm (comp_cat_U _)),
      let e := ⌈sub_comp_cat_univ_iso _ s ⌉ in
      let As := (A [[ s ]]tm ) ↑ e in
      let el_iso := comp_cat_el_iso s A in
      let sA := comp_cat_ext_subst s (comp_cat_el A) in
      let e' := ⌈sub_comp_cat_univ_iso _ (comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA)⌉ in
      let BsA := B [[ comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA ]]tm ↑ e' in
      (ΣU Δ A B ) [[ s ]]tm ↑ e = ΣU Γ As BsA.

  Definition comp_cat_universe_closed_sigma : UU :=
    ∑ (ΣU : univ_sigma_form ),
      ∑ (eliso : univ_sigma_el_iso ΣU ),
      univ_sigma_subst_law ΣU.

  Coercion comp_cat_with_sigma_to_comp_cat (SigmaU : comp_cat_universe_closed_sigma)
    : univ_sigma_form := pr1 SigmaU.

accessors for sigma codes

  Definition comp_cat_sigma_code (SigmaU : comp_cat_universe_closed_sigma)
    {Γ : C} (A : comp_cat_tm (comp_cat_U _))
    (B : comp_cat_tm (comp_cat_U _)) :
    comp_cat_tm (comp_cat_U _)
    := (pr1 SigmaU) Γ A B.

  Definition comp_cat_sigma_el_iso (SigmaU : comp_cat_universe_closed_sigma)
    {Γ : C} (A : comp_cat_tm (comp_cat_U _))
    (B : comp_cat_tm (comp_cat_U _)):
    @z_iso (fiber_category _ _) (comp_cat_el (comp_cat_sigma_code SigmaU A B))
      ((pr1 Σ) Γ (comp_cat_el A)
         (comp_cat_el B))
    := (pr12 SigmaU ) Γ A B.

  Definition comp_cat_sigma_subst (SigmaU : comp_cat_universe_closed_sigma)
    {Γ Δ : C} (s : Γ --> Δ)
    (A : comp_cat_tm (comp_cat_U _))
    (B : comp_cat_tm (comp_cat_U _)) :
    let e := ⌈sub_comp_cat_univ_iso _ s ⌉ in
    let As := (A [[ s ]]tm ) ↑ e in
    let el_iso := comp_cat_el_iso s A in
    let sA := comp_cat_ext_subst s (comp_cat_el A) in
    let e' := ⌈sub_comp_cat_univ_iso _ (comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA)⌉ in
    let BsA := B [[ comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA ]]tm ↑ e' in
    let ΣU := (@comp_cat_sigma_code SigmaU) in
    (ΣU Δ A B ) [[ s ]]tm ↑ e = (ΣU Γ As BsA )
    := (pr22 SigmaU ) _ _ s A B.

End Universe_Sigma_Closure.

Universe Being Closed under Unit Types

Section Universe_Unit_Closure.

  Context (C : comp_cat_with_universe).

  Context (Unit : comp_cat_unit C).

  Definition univ_unit_code : UU := comp_cat_tm (comp_cat_U ([] : C)).

  Definition univ_unit_el_iso (OneU : univ_unit_code) : UU :=
    @z_iso (fiber_category _ _) (comp_cat_el OneU) ((pr1 Unit) []).

  Definition comp_cat_universe_closed_unit : UU :=
    ∑ (OneU : univ_unit_code ),
      (univ_unit_el_iso OneU ).

  Coercion unit_unit_code_from_comp_cat {UnivU : comp_cat_universe_closed_unit}
    : univ_unit_code := pr1 UnivU.

accessors for unit codes

  Definition comp_cat_unit_code (UnitU : comp_cat_universe_closed_unit)
    : comp_cat_tm (comp_cat_U []) := pr1 UnitU.

  Definition comp_cat_unit_el_iso (UnitU : comp_cat_universe_closed_unit)
    : @z_iso (fiber_category _ _)
        (comp_cat_el (comp_cat_unit_code UnitU)) ((pr1 Unit) [])
    := (pr2 UnitU).

  Section weaken_unit.

    Definition comp_cat_unit_code_weakened (UnitU : comp_cat_universe_closed_unit) (Γ : C)
      : comp_cat_tm (comp_cat_U Γ)
      := (comp_cat_unit_code UnitU [[ TerminalArrow (empty_context C) Γ ]]tm )
           ↑ ⌈comp_cat_univ_sub_iso (TerminalArrow (empty_context C) Γ)⌉.

    Definition comp_cat_unit_el_iso_w (UnitU : comp_cat_universe_closed_unit) (Γ : C) :
      @z_iso (fiber_category _ _) (comp_cat_el (comp_cat_unit_code_weakened UnitU Γ)) ((pr1 Unit) Γ).
    Proof.
      unfold comp_cat_unit_code_weakened.
      set (tΓ := TerminalArrow (empty_context C) Γ).
      refine (z_iso_comp (z_iso_inv (comp_cat_el_iso tΓ (comp_cat_unit_code UnitU))) _).
      refine (z_iso_comp (comp_cat_reindex_iso tΓ (comp_cat_unit_el_iso UnitU)) _).
      exact (comp_cat_unit_sub_iso tΓ).
    Defined.

    Proposition comp_cat_unit_subst_law (UnitU : comp_cat_universe_closed_unit) {Γ Δ : C}
      (s : Γ --> Δ) :
      ((comp_cat_unit_code_weakened UnitU Δ ) [[ s ]]tm ) ↑ ⌈comp_cat_univ_sub_iso s ⌉ =
        (comp_cat_unit_code_weakened UnitU Γ ).
    Proof.
      unfold comp_cat_unit_code_weakened.
      rewrite comp_cat_subst_coerce_tm.
      rewrite comp_cat_comp_coerce_tm.
      etrans.
      { apply maponpaths.
        refine (!_).
        apply comp_cat_id_coerce_tm.
      }
      etrans.
      {
        apply maponpaths.
        apply maponpaths_2.
        refine (!_).
        apply (@z_iso_inv_after_z_iso (fiber_category _ _) _ _ (comp_cat_subst_ty_comp_iso _ _ _)).
      }
      do 2 rewrite <- comp_cat_comp_coerce_tm.
      etrans.
      { do 3 apply maponpaths.
        refine (!_).
        apply (@comp_cat_subst_tm_comp C ).
      }
      do 2 rewrite comp_cat_comp_coerce_tm.
      assert (p :TerminalArrow (empty_context C) Γ = s · TerminalArrow (empty_context C) Δ )
        by apply TerminalArrowEq.
      etrans.
      {
        apply maponpaths.
        refine (!_).
        apply (comp_cat_subst_tm_eq _ p).
      }
      rewrite comp_cat_comp_coerce_tm.
      apply comp_cat_coerce_eq.
      set (U := comp_cat_U _).
      unfold comp_cat_univ_sub_iso.
      unfold sub_comp_cat_univ_iso.
      rewrite assoc.
      assert (H: ⌈ comp_cat_subst_ty_iso U p ⌉= ⌈ comp_cat_subst_ty_iso U (!p) ⌉⁻¹) by (induction p; apply idpath).
      rewrite H.
      unfold "⌈ _ ⌉⁻¹".
      rewrite assoc'.
      do 2 use z_iso_inv_on_right.
      rewrite assoc.
      etrans.
      { apply maponpaths_2.
        apply comp_cat_reindex_coercion_comp_witness.
      }
      etrans.
      { rewrite assoc'.
        apply maponpaths.
        refine (assoc _ _ _ @ _).
        apply maponpaths_2.
        apply (comp_cat_reindex_coercion_subst_ty_iso (C:=C)).
      }
      rewrite assoc'.
      etrans.
      { do 2 apply maponpaths.
        apply comp_cat_subst_ty_iso_comp.
      }
      etrans.
      2: { refine (!_). refine (assoc _ _ _ @ _). apply idpath. }
      rewrite assoc'.
      etrans.
      { rewrite assoc.
        apply maponpaths_2.
        refine (!_).
        apply (comp_cat_assoc'_subst_ty (C:=C)).
      }
      etrans.
      { do 2 refine (assoc' _ _ _ @ _).
        do 2 apply maponpaths.
        apply comp_cat_subst_ty_iso_comp.
      }
      rewrite !assoc.
      etrans.
      2: {
        refine (!_).
        apply maponpaths_2.
        rewrite assoc'.
        apply maponpaths.
        apply comp_cat_comp_iso_natural. }
      etrans.
      2: {
        refine (!_).
        rewrite !assoc'.
        do 2 apply maponpaths.
        apply comp_cat_subst_ty_iso_comp.
      }
      rewrite !assoc.
      apply cancel_precomposition.
      do 2 apply maponpaths.
      apply homset_property.
    Qed.

  End weaken_unit.

  Section Unit_Code_Unique_Term.

    Context (UnitU : comp_cat_universe_closed_unit).

    Definition term_unit_code (Γ : C) :
      comp_cat_tm (comp_cat_el (comp_cat_unit_code_weakened UnitU Γ)).
    Proof.
      use tpair.
      - exact ( (comp_cat_unit_tt Γ) ↑ ( ⌈ (comp_cat_unit_el_iso_w UnitU Γ) ⌉⁻¹ ) ).
      - abstract(
            cbn;
            rewrite <- assoc;
            rewrite comp_cat_comp_mor_law;
            exact (pr2 (comp_cat_unit_tt Γ))).
    Defined.

    Lemma iscontr_tm_of_iso {Γ : C} {A B : comp_cat_ty Γ}
      (HA : iscontr (comp_cat_tm A))
      (i : z_iso (C := fiber_category _ _) A B)
      : iscontr (comp_cat_tm B).
    Proof.
      set (toB := (λ u : comp_cat_tm A, u ↑ ⌈ i ⌉)).
      set (toA := (λ v : comp_cat_tm B, v ↑ ⌈ i ⌉⁻¹)).
      assert (toB_toA : ∏ v : comp_cat_tm B, toB (toA v) = v) by apply coerce_tm_after_inv.
      assert (toA_toB : ∏ u : comp_cat_tm A, toA (toB u) = u) by apply coerce_tm_inv_after.
      set (w := weq_iso toB toA toA_toB toB_toA).
      exact (iscontrweqf w HA).
    Qed.

    Lemma unique_term_unit_code :
      ∏ {Γ : C} (t : comp_cat_tm (comp_cat_el (comp_cat_unit_code_weakened UnitU Γ))),
        t = (term_unit_code Γ ).
    Proof.
      intros Γ t.
      unfold term_unit_code.
      assert (HOneΓ : iscontr (comp_cat_tm ((pr1 Unit) Γ))).
      {
        use tpair.
        - exact ( comp_cat_unit_tt Γ).
        - intro u.
          exact (comp_cat_unit_unique u).
      }
      set (HElΓ :=
             @iscontr_tm_of_iso Γ ((pr1 Unit) Γ) (comp_cat_el (comp_cat_unit_code_weakened UnitU Γ))
               HOneΓ (z_iso_inv (comp_cat_unit_el_iso_w UnitU Γ))).
      use subtypePath.
      - unfold isPredicate; intros; apply (homset_property C).
      - cbn.
        change (pr1 t = pr1 (term_unit_code Γ)).
        set (c := pr1 HElΓ).
        refine (maponpaths pr1 (_)).
        exact ((pr2 HElΓ t) @ !(pr2 HElΓ (term_unit_code Γ))).
    Qed.

  End Unit_Code_Unique_Term.

End Universe_Unit_Closure.

Universe Being Closed under Pi Types

Section Universe_Pi_Closure.

  Context (C : comp_cat_with_universe).

  Context (Π : comp_cat_pi C).

  Definition univ_pi_form : UU :=
    ∏ (Γ : C)
      (A : comp_cat_tm (comp_cat_U Γ))
      (B : comp_cat_tm (comp_cat_U (Γ & comp_cat_el A))),
      comp_cat_tm (comp_cat_U Γ).

  Definition univ_pi_el_iso (ΠU : univ_pi_form) : UU :=
    ∏ (Γ : C)
      (A : comp_cat_tm (comp_cat_U _))
      (B : comp_cat_tm (comp_cat_U _)),
      @z_iso (fiber_category _ _) (comp_cat_el (ΠU Γ A B))
        ((pr1 Π) Γ (comp_cat_el A)
           (comp_cat_el B)).

  Definition univ_pi_subst_law (ΠU : univ_pi_form) : UU :=
    ∏ (Γ Δ : C) (s : Γ --> Δ)
      (A : comp_cat_tm (comp_cat_U _))
      (B : comp_cat_tm (comp_cat_U _)),
      let e := ⌈sub_comp_cat_univ_iso _ s ⌉ in
      let As := (A [[ s ]]tm ) ↑ e in
      let el_iso := comp_cat_el_iso s A in
      let sA := comp_cat_ext_subst s (comp_cat_el A) in
      let e' := ⌈sub_comp_cat_univ_iso _ (comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA)⌉ in
      let BsA := B [[ comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA ]]tm ↑ e' in
      (ΠU Δ A B ) [[ s ]]tm ↑ e = ΠU Γ As BsA.

  Definition comp_cat_universe_closed_pi : UU :=
    ∑ (ΠU : univ_pi_form ),
      ∑ (eliso : univ_pi_el_iso ΠU ),
      (univ_pi_subst_law ΠU ).

  Coercion comp_cat_with_pi_to_comp_cat (PiU : comp_cat_universe_closed_pi)
    : univ_pi_form := pr1 PiU.

accessors for pi codes

  Definition comp_cat_pi_code (PiU : comp_cat_universe_closed_pi)
    {Γ : C} (A : comp_cat_tm (comp_cat_U _))
    (B : comp_cat_tm (comp_cat_U _)) :
    comp_cat_tm (comp_cat_U _)
    := (pr1 PiU) Γ A B.

  Definition comp_cat_pi_el_iso (PiU : comp_cat_universe_closed_pi)
    {Γ : C} (A : comp_cat_tm (comp_cat_U _))
    (B : comp_cat_tm (comp_cat_U _)):
    @z_iso (fiber_category _ _) (comp_cat_el (comp_cat_pi_code PiU A B))
      ((pr1 Π) Γ (comp_cat_el A)
         (comp_cat_el B))
    := (pr12 PiU ) Γ A B.

  Definition comp_cat_pi_subst (PiU : comp_cat_universe_closed_pi)
    {Γ Δ : C} (s : Γ --> Δ)
    (A : comp_cat_tm (comp_cat_U _))
    (B : comp_cat_tm (comp_cat_U _)) :
    let e := ⌈sub_comp_cat_univ_iso _ s ⌉ in
    let As := (A [[ s ]]tm ) ↑ e in
    let el_iso := comp_cat_el_iso s A in
    let sA := comp_cat_ext_subst s (comp_cat_el A) in
    let e' := ⌈sub_comp_cat_univ_iso _ (comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA)⌉ in
    let BsA := B [[ comp_cat_comp_mor (⌈el_iso ⌉⁻¹) · sA ]]tm ↑ e' in
    let ΣU := (@comp_cat_pi_code PiU) in
    (ΣU Δ A B ) [[ s ]]tm ↑ e = (ΣU Γ As BsA )
    := (pr22 PiU ) _ _ s A B.

End Universe_Pi_Closure.

Close Scope comp_cat.