TypeTheory

The mathematical study of type theories, in univalent foundations

This project is maintained by UniMath

Library TypeTheory.ALV1.TypeCat


Ahrens, Lumsdaine, Voevodsky, 2015–
Contents:
  • Definition of type-categories and split type-categories
  • A few convenience lemmas

Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import TypeTheory.Auxiliary.UnicodeNotations.

Section Prelims.

Global Arguments isPullback [C a b c d] f g p1 p2 H.

End Prelims.

Type pre-categories

We define here *Type (pre-)categories*, closely based on the type-categories of Andy Pitts, Categorical Logic, 2000, Def. 6.3.3 (link). However, that definition includes two strictness conditions; we follow van den Berg and Garner, Topological and simplicial models, Def 2.2.1 (arXiv) in separating these out from the rest of the definition.
An element of type_precat, as we define it below, is thus exactly a type-category according to the definition of van den Berg and Garner; and an element of split_type_precat is a split type-category according to van den Berg and Garner, or a plain type-category in the sense of Pitts (modulo, in either case, the question of equality on objects of the category).
In order to avoid the nested sigma-types getting too deep, we split up the structure into two stages: type_precat_structure1 and type_precat_structure2.

A "preview" of the definition


Module Record_Preview.
For technical reasons, we prefer not to use record types in the development. However, a definition as a record type is much more readable — so we give that here, for documentation purposes only, wrapped in a module to keep it out of the global namespace.

Reserved Notation "C ⟨ Γ ⟩" (at level 60).
Reserved Notation "Γ ◂ A" (at level 45).
Reserved Notation "A {{ f }}" (at level 40).
Reserved Notation "'π' A" (at level 5).

Record type_precat_record : Type := {
  C : precategory ;
  ty : C -> Type where "C ⟨ Γ ⟩" := (ty Γ);
  ext : ∏ Γ, C⟨Γ⟩ -> C where "Γ ◂ A" := (ext Γ A);
  dpr : ∏ Γ (A : C⟨Γ⟩), Γ ◂ A --> Γ where "'π' A" := (dpr _ A);
  reind : ∏ Γ (A : C⟨Γ⟩) Γ' (f : Γ' --> Γ), C⟨Γ'⟩ where "A {{ f }}" := (reind _ A _ f) ;
  q : ∏ {Γ} (A : ty Γ) {Γ'} (f : Γ' --> Γ),
          (Γ' ◂ (A {{f }}) --> Γ ◂ A) ;
  dpr_q : ∏ Γ (A : C⟨Γ⟩) Γ' (f : Γ' --> Γ),
          (q A f) ;; (π A) = (π (A{{f}})) ;; f ;
  reind_pb : ∏ Γ (A : ty Γ) Γ' (f : Γ' --> Γ),
      isPullback _ _ _ _ (!dpr_q _ A _ f)
}.

Here we see the components of the definition of a type_precat. Under the names of their actual versions below, they are:
  • precat_of_type_precat1 (a coercion): the underlying pre-ategory;
  • ty_type_cat (also a coercion): for each object Γ, a type of “types over Γ”, written C Γ;
  • ext_type_cat: a context extension operation, written Γ ◂ A;
  • dpr_type_cat: dependent projections from context extensions;
  • reind_type_cat: a reindexing operation on types, written A[f] or f^*A;
  • q_type_cat: for f : Γ' → Γ, and A : C Γ, a map (Γ' ◂ f^* A) --> (Γ ◂ A) ; can be seen as the extension of a context morphism by a variable of a new type;
  • dpr_q_type_cat: reindexing commutes with dependent projections;
  • reind_pb_type_cat: the commutative square thus formed is a pullback.
One possibly surprising point is that reind_pb uses the square whose commutativity is witnessed by dpr_q itself, but by its inverse of dpr_q. The point is that dpr_q is oriented in the more computationally natural direction (q A f) ;; (π A) = (π (A{{f}})) ;; f , but at the same time, it’s more natural to think of π A{{f}} as the first projection of the pullback and q A f the second.

End Record_Preview.

For the actual definition, we use iterated ∑-types. As usual, to avoid severe performance issues with these, we have to split up the definition into several steps: type_precat_structure1 with the first few components, and type_precat_structure2 the rest.

Types, reindexing and context extension


Section Type_Precats.

Definition typecat_structure1 (C : precategory) :=
  ∑ (ty : C -> UU)
    (ext : ∏ Γ, ty Γ -> C),
      ∏ Γ (A : ty Γ) Γ' (f : Γ' --> Γ), ty Γ'.
Since the various access functions should eventually apply directly to type-categories as well as type-precategories (via coercion from the former to the latter), we drop the pre in their names.

Definition ty_typecat {CC : precategory} (C : typecat_structure1 CC) : CC -> UU
 := pr1 C.

Coercion ty_typecat : typecat_structure1 >-> Funclass.

Definition ext_typecat {CC : precategory} {C : typecat_structure1 CC}
  (Γ : CC) (A : C Γ) : CC
   := pr1 (pr2 C) Γ A.
Notation "Γ ◂ A" := (ext_typecat Γ A) (at level 45, left associativity).

Definition reind_typecat {CC : precategory} {C : typecat_structure1 CC}
  {Γ : CC} (A : C Γ) {Γ'} (f : Γ' --> Γ) : C Γ'
  := pr2 (pr2 C) Γ A Γ' f.
Notation "A {{ f }}" := (reind_typecat A f) (at level 40).

Pullback of dependent projections


Definition typecat_structure2 {CC : precategory} (C : typecat_structure1 CC) :=
  ∑ (dpr : ∏ Γ (A : C Γ), Γ◂A --> Γ)
    (q : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ), (Γ'◂A{{f}}) --> Γ◂A )
    (dpr_q : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ),
      (q _ A _ f) ;; (dpr _ A) = (dpr _ (A{{f}})) ;; f),
    ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ),
      isPullback _ _ _ _ (!dpr_q _ A _ f).

Definition typecat_structure (CC : precategory)
  := ∑ C : typecat_structure1 CC , typecat_structure2 C.

Definition typecat1_from_typecat (CC : precategory)(C : typecat_structure CC)
  : typecat_structure1 _ := pr1 C.
Coercion typecat1_from_typecat : typecat_structure >-> typecat_structure1.

Definition dpr_typecat {CC : precategory}{C : typecat_structure CC} {Γ} (A : C Γ)
  : (Γ◂A) --> Γ
:= pr1 (pr2 C) Γ A.

Definition q_typecat {CC : precategory} {C : typecat_structure CC} {Γ} (A : C Γ) {Γ'} (f : Γ' --> Γ)
  : (Γ' ◂ A{{f}}) --> (Γ ◂ A)
:=
  pr1 (pr2 (pr2 C)) _ A _ f.

Definition dpr_q_typecat {CC : precategory} {C : typecat_structure CC} {Γ} (A : C Γ) {Γ'} (f : Γ' --> Γ)
  : (q_typecat A f) ;; (dpr_typecat A) = (dpr_typecat (A{{f}})) ;; f
:=
  pr1 (pr2 (pr2 (pr2 C))) _ A _ f.

Definition reind_pb_typecat {CC : precategory} {C : typecat_structure CC} {Γ} (A : C Γ) {Γ'} (f : Γ' --> Γ)
  : isPullback _ _ _ _ (!dpr_q_typecat A f)
:=
  pr2 (pr2 (pr2 (pr2 C))) _ A _ f.

Type-saturation


Definition is_type_saturated_typecat {CC : precategory} (C : typecat_structure CC) : UU
  := ∏ Γ, isincl (λ A : C Γ, tpair (λ X, X --> Γ) (Γ ◂ A) (dpr_typecat A)).

Splitness

A type-precategory C is split if each collection of types C Γ is a set, reindexing is strictly functorial, and the q maps satisfy the evident functoriality axioms
Definition is_split_typecat {CC : precategory} (C : typecat_structure CC)
  := (∏ Γ:CC, isaset (C Γ))
     × (∑ (reind_id : ∏ Γ (A : C Γ), A {{identity Γ}} = A),
         ∏ Γ (A : C Γ), q_typecat A (identity Γ)
                        = idtoiso (maponpaths (fun b => Γ◂b) (reind_id Γ A)))
     × (∑ (reind_comp : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'),
                         A {{g;;f}} = A{{f}}{{g}}),
          ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'),
            q_typecat A (g ;; f)
            = idtoiso (maponpaths (fun b => Γ''◂b) (reind_comp _ A _ f _ g))
               ;; q_typecat (A{{f}}) g
               ;; q_typecat A f).

Lemma isaprop_is_split_typecat (CC : precategory) (hs : has_homsets CC)
       (C : typecat_structure CC) : isaprop (is_split_typecat C).
Proof.
  repeat (apply isofhleveltotal2; intros).
  - apply impred; intro; apply isapropisaset.
  - repeat (apply impred; intro). apply x.
  - repeat (apply impred; intro). apply hs.
  - repeat (apply impred; intro). apply x.
  - intros.
    repeat (apply impred; intro).
    apply hs.
Qed.

Definition split_typecat_structure (CC : precategory) : UU
  := ∑ C : typecat_structure CC, is_split_typecat C.

Coercion typecat_from_split (CC : precategory) (C : split_typecat_structure CC)
  : typecat_structure _
  := pr1 C.

Coercion is_split_from_split_typecat (CC : precategory) (C : split_typecat_structure CC)
  : is_split_typecat C
  := pr2 C.

Definition reind_comp_typecat {CC : precategory} {C : typecat_structure CC}
           (H : is_split_typecat C)
  : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'),
      A {{g;;f}} = A{{f}}{{g}}
  := pr1 (pr2 (pr2 H)).

Definition q_q_typecat {CC : precategory} {C : split_typecat_structure CC}
  : ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'),
            q_typecat A (g ;; f)
            = idtoiso (maponpaths (fun b => Γ''◂b) (reind_comp_typecat C _ A _ f _ g))
               ;; q_typecat (A{{f}}) g
               ;; q_typecat A f
  := pr2 (pr2 (pr2 (pr2 C))).


Section access_functions.

Context {CC : precategory} {C : typecat_structure CC} (T : is_split_typecat C).

Definition isaset_types_typecat : ∏ Γ:CC, isaset (C Γ) := pr1 T.

Definition reind_id_type_typecat : ∏ Γ (A : C Γ), A {{identity Γ}} = A := pr1 (pr1 (pr2 T)).

Definition reind_id_term_typecat :
  ∏ Γ (A : C Γ), q_typecat A (identity Γ)
                        = idtoiso (maponpaths (fun b => Γ◂b) (reind_id_type_typecat Γ A)) :=
 pr2 (pr1 (pr2 T)).

Definition reind_comp_type_typecat :
  ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'), A {{g;;f}} = A{{f}}{{g}}
 := pr1 (pr2 (pr2 T)).

Definition reind_comp_term_typecat :
   ∏ Γ (A : C Γ) Γ' (f : Γ' --> Γ) Γ'' (g : Γ'' --> Γ'),
            q_typecat A (g ;; f)
            = idtoiso (maponpaths (fun b => Γ''◂b) (reind_comp_type_typecat _ A _ f _ g))
               ;; q_typecat (A{{f}}) g
               ;; q_typecat A f
 := pr2 (pr2 (pr2 T)).

End access_functions.

End Type_Precats.

Notation "Γ ◂ A" := (ext_typecat Γ A) (at level 45, left associativity).
Notation "A {{ f }}" := (reind_typecat A f) (at level 40).

Lemmas about type-(pre)categories


Section lemmas.

Variable CC : precategory.
Variable C : split_typecat_structure CC.
Variable hs : has_homsets CC.

Lemma transportf_dpr_typecat (Γ : CC)
  (A B : C Γ)
  (f : Γ --> Γ ◂ A)
  (p : A = B) :
   transportf (λ B : C Γ, Γ --> Γ ◂ B) p f;; dpr_typecat B =
   f;; dpr_typecat A.
Proof.
  induction p.
  apply idpath.
Defined.

Lemma idtoiso_dpr_typecat (Γ : CC)
  (A B : C Γ)
  (p : A = B) :
   idtoiso (maponpaths (λ B : C Γ, Γ ◂ B) p);; dpr_typecat B =
   dpr_typecat A.
Proof.
  induction p.
  apply id_left.
Defined.

Lemma transportf_reind_typecat (Γ Γ' : CC) (A A' : C Γ') (e : A = A') t :
  transportf (λ B, Γ --> Γ' ◂ B) e t = transportf (λ Δ, Γ --> Δ) (maponpaths _ e) t.
Proof.
  induction e.
  apply idpath.
Defined.

Lemma transportf_reind_typecat' (Γ Γ' : CC) (A : C Γ) (i i' : Γ' --> Γ) (e : i = i') t :
   transportf (λ i0 : Γ' --> Γ, Γ' --> Γ' ◂ reind_typecat A i0) e t =
   transportf (λ B : C Γ', Γ' --> Γ' ◂ B) (maponpaths _ e) t.
Proof.
  induction e.
  apply idpath.
Defined.

End lemmas.