diff --git a/src/CwF.lagda.md b/src/CwF.lagda.md index 712a5ce..db57a4b 100644 --- a/src/CwF.lagda.md +++ b/src/CwF.lagda.md @@ -43,11 +43,11 @@ module CwF where ``` # 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] +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. [@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] +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. [@abd2008] -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. +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 @@ -55,7 +55,7 @@ record is-CwF {o h f : Level} (𝓒 : Precategory o h) : Type (lsuc (o ⊔ h ⊔ 𝓕 : Functor (𝓒 ^op) (Fams f) ``` -Two functions, $Ty$ and $Tm$ are defined, respectively giving the set of syntactic types, and terms in a context. +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 𝓕 @@ -67,7 +67,7 @@ Two functions, $Ty$ and $Tm$ are defined, respectively giving the set of syntact Tr Γ σ = F₀ Γ .snd σ ``` -Which support substitution in syntactic types and terms. +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 @@ -77,27 +77,39 @@ Which support substitution in syntactic types and terms. _[_] {_} {_} {A} a γ = F₁ γ .snd A a ``` -Being defined from a functor, these substitution operators play nicely with composed homs and identities. +Likewise, it follows that the substitution operators respect composition and identity. ``` - ⟦⟧-compose : {Δ Γ Θ : Ob} {γ : Hom Δ Γ} {δ : Hom Θ Δ} {A : ∣ Ty Γ ∣} + ⟦⟧-compose : {Δ Γ Θ : Ob} (γ : Hom Δ Γ) (δ : Hom Θ Δ) (A : ∣ Ty Γ ∣) → A ⟦ γ ∘ δ ⟧ ≡ A ⟦ γ ⟧ ⟦ δ ⟧ - ⟦⟧-compose {_} {_} {_} {γ} {δ} {A} i = F-∘ δ γ i .fst A + ⟦⟧-compose {_} {_} {_} γ δ A i = F-∘ δ γ i .fst A - ⟦⟧-id : {Γ : Ob} {A : ∣ Ty Γ ∣} + ⟦⟧-id : {Γ : Ob} (A : ∣ Ty Γ ∣) → A ⟦ id ⟧ ≡ A - ⟦⟧-id {Γ} {A} i = F-id i .fst 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. +Since the terms are indexed by types there will be some commonly used paths between types. ``` - []-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 + ⟦⟧-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 Γ (F-id i .fst A) ∣) (a [ id ]) a + → PathP (λ i → ⟦⟧-tr-id A i) (a [ id ]) a []-id {Γ} {A} {a} i = F-id i .snd A a ``` @@ -107,32 +119,28 @@ A CwF has a terminal object representing the empty context. terminal : Terminal 𝓒 ``` -For any context $\Gamma$ and $A \in Ty(\Gamma)$ there is a context $\Gamma,A$, extending $\Gamma$ by $A$. +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 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$ +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 syntactic term $q_{\ \Gamma;A} : Tr(\Gamma;A, A \llbracket p_{\ \Gamma;A}\rrbracket)$. +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 ⟧) ∣ ``` -It's required that the map $p$ weakened by $q$ is the identity. -``` - field - pq-id : {Γ : Ob} {A : ∣ Ty Γ ∣} → ⟨ p , q ⟩ ≡ id {Γ ; A} -``` - 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 ⟩ ≡ γ ``` @@ -140,11 +148,11 @@ Dubbing $p$ a projection is no coincidence, it projects a map out of a weakened Likewise, $q$ "projects" an object out of a weakened substitution. ``` q-∘-pathp : {Δ Γ : Ob} {γ : Hom Δ Γ} {A : ∣ Ty Γ ∣} (a : ∣ Tr Δ (A ⟦ γ ⟧) ∣) - → ∣ Tr Δ (F₁ ⟨ γ , a ⟩ .fst (F₁ p .fst A)) ∣ ≡ ∣ Tr Δ (F₁ γ .fst A) ∣ + → ∣ Tr Δ (A ⟦ p ⟧ ⟦ ⟨ γ , a ⟩ ⟧) ∣ ≡ ∣ Tr Δ (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) ∣ ∎ + ∣ 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 ⟦ γ ⟧) ∣} @@ -153,9 +161,15 @@ Likewise, $q$ "projects" an object out of a weakened substitution. a ``` -The weakening map is also required to play nice with composition. +Further motivating the use of the word projection, pairing up the two projections in a weakened map must result in the identity. ``` - ⟨⟩-∘ : {Δ Γ Θ : Ob} {γ : Hom Γ Δ} {δ : Hom Δ Θ} {A : ∣ Ty Θ ∣} {a : ∣ Tr Δ (A ⟦ δ ⟧) ∣} + 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 (λ i → ∣ Tr Γ (F-∘ γ δ (~ i) .fst A) ∣) (a [ γ ]) ⟩ + ≡ ⟨ δ ∘ γ , transport (sym (⟦⟧-tr-comp δ γ A)) (a [ γ ]) ⟩ ``` \ No newline at end of file