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

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₂))