rachel/cwfs
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

painful pathp

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-10-09 15:57:21 +02:00
parent 6d3af73b9f
commit 9c5ae69cbd
2 changed files with 31 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/CwF/Base.lagda.md
View File

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

35
src/CwF/Structures.lagda.md
View File

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