cwfs/src/CwF.lagda.md

open import Cat.Prelude
open import Fams

module CwF where

Categories with families

This file defines a CwF, as well as type formers for pi types, sigma types, identity types and universes. Here CwFs are defined as a GAT (generalised algebraic theory), as is presented in a paper by Abel, Coquand and Dybjer. [1]

A CwF is a category \mathcal C equipped with a functor \mathcal F : \mathcal C \to \mathcal Fam, fufilling the rules of the GAT.

record CwF (o h f : Level) : Type (lsuc (o ⊔ h ⊔ f)) where
  field
    𝓒 : Precategory o h
    𝓕 : Functor 𝓒 (Fams f)

Two functions, Ty and Tm are defined, respectively giving the set of syntactic types, and terms in a context.

  open Precategory
  open Functor

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

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

[1]

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