complete definition of CwF. quite ugly, needs cleaning up.

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 [ γ ]) ⟩
 ```