From 9c5ae69cbdf5517a191d9b3c57f6471be9702005 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Sun, 9 Oct 2022 15:57:21 +0200
Subject: [PATCH] painful pathp

---
 src/CwF/Base.lagda.md       |  4 ++--
 src/CwF/Structures.lagda.md | 35 +++++++++++++++++++++++++++++------
 2 files changed, 31 insertions(+), 8 deletions(-)

diff --git a/src/CwF/Base.lagda.md b/src/CwF/Base.lagda.md
index eeab45a..60acfdb 100644
--- a/src/CwF/Base.lagda.md
+++ b/src/CwF/Base.lagda.md
@@ -179,7 +179,7 @@ Further motivating the use of the word projection, pairing up the two projection
 
 Lastly, it is required that the weakening map behaves as expected under composition.
 ```
-    ⟨⟩-∘ : {Δ Γ Θ : Ob} {γ : Hom Γ Δ} {δ : Hom Δ Θ} {A : ∣ Ty Θ ∣} 
-           {a : ∣ Tr Δ (A ⟦ δ ⟧) ∣}
+    ⟨⟩-∘ : {Δ Γ Θ : Ob} (γ : Hom Γ Δ) (δ : Hom Δ Θ) (A : ∣ Ty Θ ∣) 
+           (a : ∣ Tr Δ (A ⟦ δ ⟧) ∣)
          → ⟨ δ , a ⟩ ∘ γ ≡ ⟨ δ ∘∘ γ , a [ γ ] ⟩
 ```
diff --git a/src/CwF/Structures.lagda.md b/src/CwF/Structures.lagda.md
index 995c9fe..9f54e52 100644
--- a/src/CwF/Structures.lagda.md
+++ b/src/CwF/Structures.lagda.md
@@ -49,19 +49,42 @@ Substitution must also be closed under all of these.
 
     There's quite a hefty pathp here...
     typeof app (transport (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣) (f [ γ ])) (x [ γ ])
-    B ⟦ ⟨ γ  ∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
-    B ⟦ ⟨ γ  ∘ p , q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
-    B ⟦ ⟨ γ  ∘ p ∘ ⟨id, x [ γ ] ⟩, q [ ⟨id, x [ γ ] ⟩ ] ⟩ ⟧
-    B ⟦ ⟨ γ  ∘ id, x [ γ ] ⟩ ⟧
+    B ⟦ ⟨ γ ∘ p , q ⟩ ⟧ ⟦ ⟨ id, x [ γ ] ⟩ ⟧
+    B ⟦ ⟨ γ ∘ p , q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
+    B ⟦ ⟨ γ ∘ p ∘ ⟨id, x [ γ ] ⟩, q [ ⟨id, x [ γ ] ⟩ ] ⟩ ⟧
+    B ⟦ ⟨ γ ∘ id, x [ γ ] ⟩ ⟧
     B ⟦ ⟨ id ∘ γ , x [ γ ] ⟩ ⟧
     B ⟦ ⟨ id, x ⟩ ⟧ ⟦ γ ⟧
     typeof app f x [ γ ]
 
-```
+    it would seem CwFs really don't want to be formalized :/
+    not enough definitional equalities...
 
+```
+  app-subst-pathp : {Δ Γ : Ob} (γ : Hom Δ Γ) {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣} 
+                      (f : ∣ Tr Γ (∏ A B) ∣) (x : ∣ Tr Γ A ∣) 
+                  → B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
+                  ≡ B ⟦ ⟨id, x ⟩ ⟧ ⟦ γ ⟧
+  app-subst-pathp {Δ} {Γ} γ {A} {B} f x =
+    B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
+      ≡˘⟨ ⟦⟧-compose ⟨ γ ∘∘ p , q ⟩ ⟨id, x [ γ ] ⟩ B ⟩
+    B ⟦ ⟨ γ ∘∘ p , q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
+      ≡⟨⟩
+    B ⟦ ⟨ γ ∘ p , transport (λ i → ⟦⟧-tr-comp γ p A (~ i)) q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
+      ≡⟨ (λ i → B ⟦ ⟨⟩-∘  ⟨id, x [ γ ] ⟩ (γ ∘ p) A (transport (λ i → ⟦⟧-tr-comp γ (p {Δ} {A ⟦ γ ⟧}) A (~ i)) q) i ⟧) ⟩
+    B ⟦ ⟨ γ ∘ p ∘∘ ⟨id, x [ γ ] ⟩ , transport (λ i → ⟦⟧-tr-comp γ (p {Δ} {A ⟦ γ ⟧}) A (~ i)) q [ ⟨id, x [ γ ] ⟩ ] ⟩ ⟧
+      ≡⟨⟩
+    B ⟦ ⟨ (γ ∘ p) ∘ ⟨id, x [ γ ] ⟩ , transport (λ i →  ⟦⟧-tr-comp (γ ∘ p) ⟨id, x [ γ ] ⟩ A (~ i))
+                                               (transport (λ j → ⟦⟧-tr-comp γ (p {Δ} {A ⟦ γ ⟧}) A (~ j)) q [ ⟨id, x [ γ ] ⟩ ]) ⟩ ⟧
+      ≡⟨ {!   !} ⟩
+    B ⟦ ⟨id, x ⟩ ⟧ ⟦ γ ⟧
+      ∎
+
+
+  field
     app-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣} 
                 (f : ∣ Tr Γ (∏ A B) ∣) (x : ∣ Tr Γ A ∣) 
-              → PathP {!   !}
+              → PathP (λ i → ∣ Tr Δ (app-subst-pathp γ f x (~ i)) ∣ )
                       (app f x [ γ ])
                       (app (transport (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣) (f [ γ ])) (x [ γ ]))
 ```