7.2 KiB

Raw Blame History

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

module CwF.Base 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 category \mathcal C is said to be a CwF if there is a contravariant functor \mathcal F : \mathcal C^{op} \to \mathcal Fam, and it fufills the laws of the GAT.

record is-CwF {o h f : _} (𝓒 : 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 context’s 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)

It is often the case that weakening maps will take a composition of morphisms, or an identity morphism, which will cause the second element to no longer have the same type definitionally. These helpers are defined to get around this with transports.

  ⟨_∘∘_,_⟩ : {Δ Γ Θ : Ob} {A : ∣ Ty Γ ∣} (γ : Hom Δ Γ)
             (δ : Hom Θ Δ) → (a : ∣ Tr Θ (A ⟦ γ ⟧ ⟦ δ ⟧) ∣ ) → Hom Θ (Γ ; A)
  ⟨_∘∘_,_⟩ {_} {_} {Θ} {A} γ δ a = ⟨ γ ∘ δ , transport (λ i → ⟦⟧-tr-comp γ δ A (~ i)) a ⟩

  ⟨id,_⟩ : {Γ : Ob} {A : ∣ Ty Γ ∣} (a : ∣ Tr Γ A ∣) → Hom Γ (Γ ; A)
  ⟨id,_⟩ {_} {A} a = ⟨ id , transport (λ i → ⟦⟧-tr-id A (~ i)) 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).

  field
    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 ⟩ ∘ γ ≡ ⟨ δ ∘∘ γ , 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

7.2 KiB Raw Blame History Unescape Escape

Categories with families

7.2 KiB

Raw Blame History