slightly less confusing text

src/CwF.lagda.md

@@ -41,9 +41,6 @@ open import Fams
 
 module CwF where
 ```
-<!---
-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]
@@ -128,19 +125,19 @@ For every context $\Gamma$ and $A ∈ Ty(\Gamma)$ there is a projection map $p_{
     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.
+It's required that the map $p$ weakened by $q$ is the identity.
 ```
   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.
+Dubbing $p$ a projection is no coincidence, it projects a map out of a weakened map.
 ```
     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.
+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) ∣