cwfs/src/CwF.lagda.md

open import Cat.Prelude
open import Cat.Diagram.Terminal
open import Fams

module CwF where

Categories with families

A Category with families, a CwF, is a category in which we can interpret the synax of a type theory. The objects of a CwF are contexts and the morphisms are a list of judgements. The morphisms, being lists of judgements, are able to describe substitution and weakening. For a more detailed introduction to CwFs see the introductory paper by Hoffmann. [1]

This file defines a CwF, without any particular type formers. Here CwFs are thought of as GATs (generalised algebraic theories), as is presented in a paper by Abel, Coquand and Dybjer. [2]

A CwF is defined as a precategory \mathcal C equipped with a contravariant functor \mathcal F : \mathcal C^{op} \to \mathcal Fam, fufilling the properties listed below.

record is-CwF {o h f : Level} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) where
  field
    𝓕 : Functor (𝓒 ^op) (Fams f)

Two functions, Ty and Tm are defined in terms of \mathcal F, giving a contexts set of syntactic types, and terms respectively.

  open Precategory 𝓒
  open Functor 𝓕

  Ty : Ob → Set f
  Ty Γ = F₀ Γ .fst 

  Tr : (Γ : Ob) → ∣ Ty Γ ∣ → Set f
  Tr Γ σ = F₀ Γ .snd σ

From functoriality of \mathcal F it can be derived that these support substitution in both types and terms.

  _⟦_⟧ : {Δ Γ : Ob} → ∣ Ty Γ ∣ → Hom Δ Γ → ∣ Ty Δ ∣
  A ⟦ γ ⟧ = F₁ γ .fst A

  _[_] : {Δ Γ : Ob} {A : ∣ Ty Γ ∣} (a : ∣ Tr Γ A ∣)
         (γ : Hom Δ Γ) → ∣ Tr Δ (A ⟦ γ ⟧) ∣
  _[_] {_} {_} {A} a γ = F₁ γ .snd A a

Likewise, it follows that the substitution operators respect composition and identity.

  ⟦⟧-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
             → A ⟦ γ ∘ δ ⟧ ≡ A ⟦ γ ⟧ ⟦ δ ⟧
  ⟦⟧-compose {_} {_} {_} γ δ A i = F-∘ δ γ i .fst A

  ⟦⟧-id : {Γ : Ob} (A : ∣ Ty Γ ∣)
        → A ⟦ id ⟧ ≡ A
  ⟦⟧-id {Γ} A i = F-id i .fst A

Since the terms are indexed by types there will be some commonly used paths between types.

  ⟦⟧-tr-comp : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣)
             → ∣ Tr Θ (A ⟦ γ ∘ δ ⟧) ∣ ≡ ∣ Tr Θ (A ⟦ γ ⟧ ⟦ δ ⟧) ∣
  ⟦⟧-tr-comp {_} {_} {Θ} γ δ A i = ∣ Tr Θ (⟦⟧-compose γ δ A i) ∣

  ⟦⟧-tr-id : {Γ : Ob} (A : ∣ Ty Γ ∣)
           → ∣ Tr Γ (A ⟦ id ⟧) ∣ ≡ ∣ Tr Γ A ∣
  ⟦⟧-tr-id  {Γ} A i = ∣ Tr Γ (⟦⟧-id A i) ∣

Using the paths defined above, composition and identity laws for terms can be stated and proven.

  []-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣) 
               {a : ∣ Tr Γ A ∣}
               → PathP (λ i → ⟦⟧-tr-comp γ δ A i) 
                       (a [ γ ∘ δ ])
                       (a [ γ ] [ δ ])
  []-compose {_} {_} {_} γ δ A {a} i = F-∘ δ γ i .snd A a

  []-id : {Γ : Ob} {A : ∣ Ty Γ ∣} {a : ∣ Tr Γ A ∣}
          → PathP (λ i → ⟦⟧-tr-id A i) (a [ id ]) a
  []-id {Γ} {A} {a} i = F-id i .snd A a

A CwF has a terminal object representing the empty context.

  field
    terminal : Terminal 𝓒

For any context \Gamma and A \in Ty(\Gamma) there is a context \Gamma;A, extending \Gamma by A.

    _;_ : (Γ : Ob) → ∣ Ty Γ ∣ → Ob

Thus contexts can be built by repeatedly extending the empty context.

For any list of judgements between \Delta and \Gamma, there should be a weakened version from \Delta to \Gamma;A.

    ⟨_,_⟩ : {Γ Δ : Ob} {A : ∣ Ty Γ ∣} (γ : Hom Δ Γ) (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣ )
          → Hom Δ (Γ ; A)

For every context \Gamma and A ∈ Ty(\Gamma) there is a projection map p_{\ \Gamma;A} : \Gamma;A → \Gamma and a term q_{\ \Gamma;A} : Tr(\Gamma;A, A \llbracket p_{\ \Gamma;A}\rrbracket).

    p : {Γ : Ob} {A : ∣ Ty Γ ∣} → Hom (Γ ; A) Γ
    q : {Γ : Ob} {A : ∣ Ty Γ ∣} → ∣ Tr (Γ ; A) (A ⟦ p ⟧) ∣

Dubbing p a projection is no coincidence, it projects a map out of a weakened map.

  field
    p-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣)
        → p ∘ ⟨ γ , a ⟩ ≡ γ

Likewise, q “projects” an object out of a weakened substitution.

  q-∘-pathp : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣) 
            → ∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡ ∣ Tr Δ (A ⟦ γ ⟧) ∣
  q-∘-pathp {Δ} {Γ} {γ} {A} a =
    ∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡˘⟨ ⟦⟧-tr-comp p ⟨ γ , a ⟩ A ⟩
    ∣ Tr Δ (A ⟦ p ∘ ⟨ γ , a ⟩ ⟧)   ∣ ≡⟨ (λ i → ∣ Tr Δ (A ⟦ p-∘ a i ⟧) ∣) ⟩
    ∣ Tr Δ (A ⟦ γ ⟧)               ∣ ∎
              
  field
    q-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} {a : ∣ Tr Δ (A ⟦ γ ⟧) ∣} 
        → PathP (λ i → q-∘-pathp a i) 
                (q [ ⟨ γ , a ⟩ ]) 
                a

Further motivating the use of the word projection, pairing up the two projections in a weakened map must result in the identity.

    pq-id : {Γ : Ob} {A : ∣ Ty Γ ∣} → ⟨ p , q ⟩ ≡ id {Γ ; A}

Lastly, it is required that the weakening map behaves as expected under composition.

    ⟨⟩-∘ : {Δ Γ Θ : Ob} {γ : Hom Γ Δ} {δ : Hom Δ Θ} {A : ∣ Ty Θ ∣} 
           {a : ∣ Tr Δ (A ⟦ δ ⟧) ∣}
         → ⟨ δ , a ⟩ ∘ γ 
         ≡ ⟨ δ ∘ γ , transport (sym (⟦⟧-tr-comp δ γ A)) (a [ γ ]) ⟩

[1]

Martin Hoffmann, “Syntax and semantics of dependent types,” vol. 4989. pp. 13–54, 1997. Available: https://doi.org/10.1007/978-1-4471-0963-1_2

[2]

Andreas Abel, Thierry Coquand, and Peter Dybjer, “On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory,” vol. 4989, pp. 3–13, 2008, Available: http://link.springer.com/10.1007/978-3-540-78969-7_2