Week 26 (06/22 - 06/28)

Two preliminaries for grasping the SOGAT → GAT translations:

• Theory of Signatures, a particular QIIT, partitioned in the following notions,

  • Four sorts (Contexts, types, terms, substitutions)
  • Substitution calculus
  • Universe (related constructors)
  • Function space with small domain
  • Identity type for elements of small types
  • Function space with metatheoretic domain

  [Some further details]

• Categories with Families: standard, historical definition, consists of

  • category $\mathcal{C}$ with terminal object $1$
  • Fam-valued presheaf, $T:{\mathcal{C}}^{\mathrm{op}}\to \mathrm{Fam}$
  • context comprehension $\Gamma \in {\mathcal{C}}_0,A\in \mathrm{Ty}(\Gamma )\mapsto \Gamma \cdot A\in {\mathcal{C}}_0$ and two projections […]

  [Some further details]