From aa6801bcfc75fdbf6811cf0ac92dc5138fc3a10d Mon Sep 17 00:00:00 2001 From: depsterr Date: Fri, 7 Oct 2022 23:05:46 +0200 Subject: [PATCH] complete definition of CwF. quite ugly, needs cleaning up. --- src/CwF.lagda.md | 127 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 117 insertions(+), 10 deletions(-) diff --git a/src/CwF.lagda.md b/src/CwF.lagda.md index b089992..fe7fd45 100644 --- a/src/CwF.lagda.md +++ b/src/CwF.lagda.md @@ -18,11 +18,25 @@ references: url: http://link.springer.com/10.1007/978-3-540-78969-7_2 page: 3-13 language: en-GB +- type: book-section + id: hoffmann97 + author: + - family: Martin Hoffmann + issued: + date-parts: + - - 1997 + title: 'Syntax and semantics of dependent types' + journal: "Extensional Constructs in Intensional Type Theory" + volume: 4989 + url: https://doi.org/10.1007/978-1-4471-0963-1_2 + page: 13-54 + language: en-GB citation-style: ieee --- ``` open import Cat.Prelude +open import Cat.Diagram.Terminal open import Fams module CwF where @@ -32,26 +46,119 @@ TODO: write more about what a CwF actually is and how one should think abut it. ---> # Categories with families +A Category with families, written as CwF, is a category in which we can interpret the synax of a type theory. The objects of a CwF are contexts, and morphisms are a list of judgements, which capture the notions of substitution and weakening. For a more detailed introduction to CwFs see the introductory paper by Hoffmann. [@hoffmann97] + 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. [@abd2008] -A CwF is a category $\mathcal C$ equipped with a functor $\mathcal F : \mathcal C \to \mathcal Fam$, fufilling the rules of the GAT. +A CwF is defined as a category $\mathcal C$ equipped with a contravariant functor $\mathcal F : \mathcal C^{op} \to \mathcal Fam$, fufilling the rules of the GAT. ``` -record CwF (o h f : Level) : Type (lsuc (o ⊔ h ⊔ f)) where +record is-CwF {o h f : Level} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ f)) where field - 𝓒 : Precategory o h - 𝓕 : Functor 𝓒 (Fams f) + 𝓕 : Functor (𝓒 ^op) (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 + open Precategory 𝓒 + open Functor 𝓕 - Ty : 𝓒 .Ob → Set f - Ty Γ = 𝓕 .F₀ Γ .fst + Ty : Ob → Set f + Ty Γ = F₀ Γ .fst - Tr : (Γ : 𝓒 .Ob) → ∣ Ty Γ ∣ → Set f - Tr Γ σ = 𝓕 .F₀ Γ .snd σ + Tr : (Γ : Ob) → ∣ Ty Γ ∣ → Set f + Tr Γ σ = F₀ Γ .snd σ +``` +Which support substitution in syntactic 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 +``` + +Being defined from a functor, these substitution operators play nicely with composed homs and identities. +``` + ⟦⟧-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 +``` + +Because the type of the syntactic terms depends upon the syntactic types a path over paths is needed for stating that substitution is well behaved on terms. +``` + []-compose : {Δ Γ Θ : Ob} {γ : Hom Δ Γ} {δ : Hom Θ Δ} {A : ∣ Ty Γ ∣} {a : ∣ Tr Γ A ∣} + → PathP (λ i → ∣ Tr Θ (F-∘ δ γ i .fst A) ∣) + (a [ γ ∘ δ ]) + (a [ γ ] [ δ ]) + []-compose {_} {_} {_} {γ} {δ} {A} {a} i = F-∘ δ γ i .snd A a + + []-id : {Γ : Ob} {A : ∣ Ty Γ ∣} {a : ∣ Tr Γ A ∣} + → PathP (λ i → ∣ Tr Γ (F-id i .fst A) ∣) (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 +``` + +For every $\gamma : \Delta \to \Gamma$ and $a \in Tr(\Delta, A \llbracket \gamma \rrbracket)$ there is a weakened map $\langle \gamma , a \rangle : \Delta → \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 syntactic 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 ⟧) ∣ +``` + +The meaning of $q$ might be a bit confusing, but it's essentialy an inverse of $p$, in the sense made precise below. +``` + field + pq-id : {Γ : Ob} {A : ∣ Ty Γ ∣} → ⟨ p , q ⟩ ≡ id {Γ ; A} +``` + +There are some additional requirments placed upon $p$ and $q$ to ensure they play nice. +``` + p-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣) + → p ∘ ⟨ γ , a ⟩ ≡ γ +``` + +The condition for q, depending on the condition for p holding, needs to be expressed with a rather annoying path over path. +``` + q-∘-pathp : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣) + → ∣ Tr Δ (F₁ ⟨ γ , a ⟩ .fst (F₁ p .fst A)) ∣ ≡ ∣ Tr Δ (F₁ γ .fst A) ∣ + q-∘-pathp {Δ} {Γ} {γ} {A} a = + ∣ Tr Δ (F₁ ⟨ γ , a ⟩ .fst (F₁ p .fst A)) ∣ ≡⟨ (λ i → ∣ Tr Δ (F-∘ ⟨ γ , a ⟩ p (~ i) .fst A) ∣) ⟩ + ∣ Tr Δ (F₁ (p ∘ ⟨ γ , a ⟩) .fst A) ∣ ≡⟨ (λ i → ∣ Tr Δ (F₁ (p-∘ a i) .fst A) ∣) ⟩ + ∣ Tr Δ (F₁ γ .fst A) ∣ ∎ + + field + q-∘ : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} {a : ∣ Tr Δ (A ⟦ γ ⟧) ∣} + → PathP (λ i → q-∘-pathp a i) + (q [ ⟨ γ , a ⟩ ]) + a +``` + +The weakening map is also required to play nice with composition. +``` + ⟨⟩-∘ : {Δ Γ Θ : Ob} {γ : Hom Γ Δ} {δ : Hom Δ Θ} {A : ∣ Ty Θ ∣} {a : ∣ Tr Δ (A ⟦ δ ⟧) ∣} + → ⟨ δ , a ⟩ ∘ γ + ≡ ⟨ δ ∘ γ , transport (λ i → ∣ Tr Γ (F-∘ γ δ (~ i) .fst A) ∣) (a [ γ ]) ⟩ ``` \ No newline at end of file