Skip to content

Instantly share code, notes, and snippets.

@FrozenWinters

FrozenWinters/normal.agda

Created March 28, 2022 03:58
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save FrozenWinters/933a8a8ee42903a07262eca7be16cc3c to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save FrozenWinters/933a8a8ee42903a07262eca7be16cc3c to your computer and use it in GitHub Desktop.
Download ZIP
Fragment of the proof that normal forms form a set in which I prove that type erasure is injective using a bidirectional approach to sectioning it
Raw
normal.agda
module Normal (π’ž : Contextual β„“ β„“) ⦃ π’žCCC : CCC π’ž ⦄
{X : Type β„“} (base : X β†’ Contextual.ty π’ž) where
open Contextual π’ž
open CCC π’žCCC
data Ne : (Ξ“ : ctx) (A : ty) β†’ Type β„“
data Nf : (Ξ“ : ctx) (A : ty) β†’ Type β„“
data Ne where
VN : {Ξ“ : ctx} {A : ty} β†’ IntVar Ξ“ A β†’ Ne Ξ“ A
APP : {Ξ“ : ctx} {A B : ty} β†’ Ne Ξ“ (A ⇛ B) β†’ Nf Ξ“ A β†’ Ne Ξ“ B
data Nf where
NEU : {Ξ“ : ctx} {x : X} β†’ Ne Ξ“ (base x) β†’ Nf Ξ“ (base x)
LAM : {Ξ“ : ctx} {A B : ty} β†’ Nf (Ξ“ ⊹ A) B β†’ Nf Ξ“ (A ⇛ B)
-- ... skipping stuff
module PathNormal (isDiscTy : Discrete ty) where
isSetTy = Discrete→isSet isDiscTy
open π‘‰π‘Žπ‘ŸPath ty isSetTy
data UNe : (n : β„•) β†’ Type β„“
data UNf : (n : β„•) β†’ Type β„“
data UNe where
VN : {n : β„•} β†’ Fin n β†’ UNe n
APP : {n : β„•} β†’ UNe n β†’ UNf n β†’ UNe n
data UNf where
NEU : {n : β„•} β†’ X β†’ UNe n β†’ UNf n
LAM : {n : β„•} β†’ ty β†’ UNf (S n) β†’ UNf n
eraseNe : {Ξ“ : ctx} {A : ty} β†’ Ne Ξ“ A β†’ UNe (len Ξ“)
eraseNf : {Ξ“ : ctx} {A : ty} β†’ Nf Ξ“ A β†’ UNf (len Ξ“)
eraseNe (VN v) = VN (numify v)
eraseNe (APP M N) = APP (eraseNe M) (eraseNf N)
eraseNf (NEU {x = x} M) = NEU x (eraseNe M)
eraseNf (LAM {A = A} N) = LAM A (eraseNf N)
indTy : (Ξ“ : ctx) (n : Fin (len Ξ“)) β†’ ty
indTy (Ξ“ ⊹ A) 𝑍 = A
indTy (Ξ“ ⊹ A) (𝑆 n) = indTy Ξ“ n
indVar : (Ξ“ : ctx) (n : Fin (len Ξ“)) β†’ IntVar Ξ“ (indTy Ξ“ n)
indVar (Ξ“ ⊹ A) 𝑍 = 𝑧𝑣
indVar (Ξ“ ⊹ A) (𝑆 n) = 𝑠𝑣 (indVar Ξ“ n)
compareTy : (A : ty) β†’ (B : ty) β†’ Maybe (A ≑ B)
compareTy A B with isDiscTy A B
... | yes p = just p
... | no Β¬p = nothing
checkNe : (Ξ“ : ctx) (A : ty) β†’ UNe (len Ξ“) β†’ Maybe (Ne Ξ“ A)
synthNf : (Ξ“ : ctx) β†’ UNf (len Ξ“) β†’ Maybe (Ξ£ ty (Ξ» A β†’ Nf Ξ“ A))
checkNe Ξ“ A (VN n) = do
p ← compareTy (indTy Ξ“ n) A
just (subst (Ne Ξ“) p (VN (indVar Ξ“ n)))
checkNe Ξ“ A (APP M N) = do
(B , N') ← synthNf Ξ“ N
M' ← checkNe Ξ“ (B ⇛ A) M
just (APP M' N')
synthNf Ξ“ (NEU x M) = do
M' ← checkNe Ξ“ (base x) M
just (base x , NEU M')
synthNf Ξ“ (LAM A N) = do
(B , N') ← synthNf (Ξ“ ⊹ A) N
just (A ⇛ B , LAM N')
indTyLem : {Ξ“ : ctx} {A : ty} (v : IntVar Ξ“ A) β†’ indTy Ξ“ (numify v) ≑ A
indTyLem 𝑧𝑣 = refl
indTyLem (𝑠𝑣 v) = indTyLem v
compareLem : {Ξ“ : ctx} {A : ty} (v : IntVar Ξ“ A) β†’
compareTy (indTy Ξ“ (numify v)) A ≑ just (indTyLem v)
compareLem {Ξ“} {A} v with isDiscTy (indTy Ξ“ (numify v)) A
... | yes p = λ i → just (Discrete→isSet isDiscTy (indTy Γ (numify v)) A p (indTyLem v) i)
... | no Β¬p = absurd (Β¬p (indTyLem v))
insert𝐢𝑑π‘₯ : ctx β†’ ty β†’ β„• β†’ ctx
insert𝐢𝑑π‘₯ Ξ“ A Z = Ξ“ ⊹ A
insert𝐢𝑑π‘₯ βˆ… A (S n) = βˆ… ⊹ A
insert𝐢𝑑π‘₯ (Ξ“ ⊹ B) A (S n) = insert𝐢𝑑π‘₯ Ξ“ A n ⊹ B
shiftVar : {Ξ“ : ctx} (A : ty) {B : ty} β†’ IntVar Ξ“ B β†’ (n : β„•) β†’ IntVar (insert𝐢𝑑π‘₯ Ξ“ A n) B
shiftNe : {Ξ“ : ctx} (A : ty) {B : ty} β†’ Ne Ξ“ B β†’ (n : β„•) β†’ Ne (insert𝐢𝑑π‘₯ Ξ“ A n) B
shiftNf : {Ξ“ : ctx} (A : ty) {B : ty} β†’ Nf Ξ“ B β†’ (n : β„•) β†’ Nf (insert𝐢𝑑π‘₯ Ξ“ A n) B
shiftVar A v Z = 𝑠𝑣 v
shiftVar A 𝑧𝑣 (S n) = 𝑧𝑣
shiftVar A (𝑠𝑣 v) (S n) = 𝑠𝑣 (shiftVar A v n)
shiftNe A (VN v) n = VN (shiftVar A v n)
shiftNe A (APP M N) n = APP (shiftNe A M n) (shiftNf A N n)
shiftNf A (NEU M) n = NEU (shiftNe A M n)
shiftNf A (LAM N) n = LAM (shiftNf A N (S n))
W₁Ne : {Ξ“ : ctx} (A : ty) {B : ty} β†’ Ne Ξ“ B β†’ Ne (Ξ“ ⊹ A) B
W₁Ne A M = shiftNe A M Z
transpW₁Ne : {Ξ“ : ctx} {A B₁ Bβ‚‚ : ty} (M : Ne Ξ“ B₁) (p : B₁ ≑ Bβ‚‚) β†’
subst (Ne (Ξ“ ⊹ A)) p (W₁Ne A M) ≑ W₁Ne A (subst (Ne Ξ“) p M)
transpW₁Ne {Ξ“} {A} M p =
J (Ξ» B p β†’ subst (Ne (Ξ“ ⊹ A)) p (W₁Ne A M) ≑ W₁Ne A (subst (Ne Ξ“) p M))
(transportRefl (W₁Ne A M) βˆ™ ap (W₁Ne A) (transportRefl M ⁻¹)) p
varSection : {Ξ“ : ctx} {A : ty} (v : IntVar Ξ“ A) β†’ checkNe Ξ“ A (VN (numify v)) ≑ just (VN v)
checkSection : {Ξ“ : ctx} {A : ty} (M : Ne Ξ“ A) β†’ checkNe Ξ“ A (eraseNe M) ≑ just M
synthSection : {Ξ“ : ctx} {A : ty} (N : Nf Ξ“ A) β†’ synthNf Ξ“ (eraseNf N) ≑ just (A , N)
varSection {Ξ“ ⊹ A} 𝑧𝑣 =
(compareTy A A >>= (Ξ» p β†’ just (subst (Ne (Ξ“ ⊹ A)) p (VN 𝑧𝑣))))
β‰‘βŸ¨ (Ξ» i β†’ compareLem {Ξ“ ⊹ A} 𝑧𝑣 i >>= (Ξ» p β†’ just (subst (Ne (Ξ“ ⊹ A)) p (VN 𝑧𝑣)))) ⟩
just (transport refl (VN 𝑧𝑣))
β‰‘βŸ¨ ap just (transportRefl (VN 𝑧𝑣)) ⟩
just (VN 𝑧𝑣)
∎
varSection {Ξ“ ⊹ A} {B} (𝑠𝑣 v) =
(compareTy (indTy Ξ“ (numify v)) B >>=
(Ξ» p β†’ just (subst (Ne (Ξ“ ⊹ A)) p (VN (𝑠𝑣 (indVar Ξ“ (numify v)))))))
β‰‘βŸ¨ (Ξ» i β†’ compareLem v i >>=
(Ξ» p β†’ just (subst (Ne (Ξ“ ⊹ A)) p (VN (𝑠𝑣 (indVar Ξ“ (numify v))))))) ⟩
just (subst (Ne (Ξ“ ⊹ A)) (indTyLem v) (W₁Ne A (VN (indVar Ξ“ (numify v)))))
β‰‘βŸ¨ ap just (transpW₁Ne (VN (indVar Ξ“ (numify v))) (indTyLem v)) ⟩
(just (subst (Ne Ξ“) (indTyLem v) (VN (indVar Ξ“ (numify v)))) >>= (Ξ» M β†’ just (W₁Ne A M)))
β‰‘βŸ¨ (Ξ» i β†’ compareLem v (~ i) >>=
(Ξ» p β†’ just (subst (Ne Ξ“) p (VN (indVar Ξ“ (numify v))))) >>= (Ξ» M β†’ just (W₁Ne A M))) ⟩
(compareTy (indTy Ξ“ (numify v)) B >>=
(Ξ» p β†’ just (subst (Ne Ξ“) p (VN (indVar Ξ“ (numify v))))) >>= (Ξ» M β†’ just (W₁Ne A M)))
β‰‘βŸ¨ (Ξ» i β†’ varSection v i >>= (Ξ» M β†’ just (W₁Ne A M))) ⟩
just (VN (𝑠𝑣 v))
∎
checkSection (VN v) = varSection v
checkSection (APP {Ξ“} {A} {B} M N) =
(synthNf Ξ“ (eraseNf N) >>=
(Ξ» { (A , N') β†’ checkNe Ξ“ (A ⇛ B) (eraseNe M) >>= (Ξ» M' β†’ just (Ne.APP M' N'))}))
β‰‘βŸ¨ (Ξ» i β†’ synthSection N i >>=
(Ξ» { (A , N') β†’ checkNe Ξ“ (A ⇛ B) (eraseNe M) >>= (Ξ» M' β†’ just (APP M' N'))})) ⟩
(checkNe Ξ“ (A ⇛ B) (eraseNe M) >>= (Ξ» M' β†’ just (APP M' N)))
β‰‘βŸ¨ (Ξ» i β†’ checkSection M i >>= (Ξ» M' β†’ just (APP M' N))) ⟩
just (APP M N)
∎
synthSection (NEU {x = x} M) =
ap (_>>= (Ξ» M' β†’ just (base x , NEU M'))) (checkSection M)
synthSection (LAM {Ξ“} {A} {B} N) =
ap (_>>= (Ξ» { (B , N') β†’ just ((A ⇛ B) , LAM N') })) (synthSection N)
just-invert : {A : Type ℓ₁} β†’ A β†’ Maybe A β†’ A
just-invert a (just b) = b
just-invert a nothing = a
straightenNf : {Ξ“ : ctx} {A : ty} {N₁ Nβ‚‚ : Nf Ξ“ A} {p : A ≑ A} β†’
PathP (Ξ» i β†’ Nf Ξ“ (p i)) N₁ Nβ‚‚ β†’ N₁ ≑ Nβ‚‚
straightenNf {Ξ“} {A} {N₁} {Nβ‚‚} {p} q =
transport (Ξ» i β†’ PathP (Ξ» j β†’ Nf Ξ“ (isSetTy A A p refl i j)) N₁ Nβ‚‚) q
eraseNfInj : {Ξ“ : ctx} {A : ty} (N₁ Nβ‚‚ : Nf Ξ“ A) β†’ eraseNf N₁ ≑ eraseNf Nβ‚‚ β†’ N₁ ≑ Nβ‚‚
eraseNfInj {Ξ“} {A} N₁ Nβ‚‚ p =
straightenNf
(ap (Ξ» x β†’ snd (just-invert (A , N₁) x))
(synthSection N₁ ⁻¹ βˆ™ ap (synthNf Ξ“) p βˆ™ synthSection Nβ‚‚))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment