{-# OPTIONS --safe --without-K #-}
  module ag-93PB where

  open import MLTT.Spartan
  open import MLTT.List
  open import UF.Equiv
  open import UF.Univalence

polynomial解釋成型別時

  ⟦_⟧ : Poly → 𝓤₀ ̇ → 𝓤₀ ̇
  ⟦ 𝟘ᵖ    ⟧ X = 𝟘
  ⟦ 𝟙ᵖ    ⟧ X = 𝟙
  ⟦ var   ⟧ X = X
  ⟦ p ⊕ q ⟧ X = ⟦ p ⟧ X + ⟦ q ⟧ X
  ⟦ p ⊗ q ⟧ X = ⟦ p ⟧ X × ⟦ q ⟧ X

Figure 4 的前六行但排除 $\partial_x(y \setminus x)$

  ∂ : Poly → Poly
  ∂ 𝟘ᵖ      = 𝟘ᵖ
  ∂ 𝟙ᵖ      = 𝟘ᵖ
  ∂ var     = 𝟙ᵖ
  ∂ (p ⊕ q) = ∂ p ⊕ ∂ q
  ∂ (p ⊗ q) = (∂ p ⊗ q) ⊕ (p ⊗ ∂ q)

我們先看案例 $\text{btree}\ X = 1 + X^2$

  B : Poly
  B = 𝟙ᵖ ⊕ (var ⊗ var)

  _ : ∂ B ＝ 𝟘ᵖ ⊕ ((𝟙ᵖ ⊗ var) ⊕ (var ⊗ 𝟙ᵖ))
  _ = refl

  ∂B-≃ : {X : 𝓤₀ ̇ } → ⟦ ∂ B ⟧ X ≃ (X + X)
  ∂B-≃ = qinveq to (from , from-to , to-from)
    where
    to : {X : 𝓤₀ ̇ } → ⟦ ∂ B ⟧ X → X + X
    to (inl ())
    to (inr (inl (⋆ , x))) = inl x
    to (inr (inr (x , ⋆))) = inr x

    from : {X : 𝓤₀ ̇ } → X + X → ⟦ ∂ B ⟧ X
    from (inl x) = inr (inl (⋆ , x))
    from (inr x) = inr (inr (x , ⋆))

    from-to : {X : 𝓤₀ ̇ } → (c : ⟦ ∂ B ⟧ X) → from (to c) ＝ c
    from-to (inl ())
    from-to (inr (inl (⋆ , x))) = refl
    from-to (inr (inr (x , ⋆))) = refl

    to-from : {X : 𝓤₀ ̇ } → (v : X + X) → to (from v) ＝ v
    to-from (inl x) = refl
    to-from (inr x) = refl

  ∂B-＝ : is-univalent 𝓤₀ → (X : 𝓤₀ ̇ ) → ⟦ ∂ B ⟧ X ＝ (X + X)
  ∂B-＝ ua X = eqtoid ua _ _ ∂B-≃

給一個 one-hole context Γ : ⟦ ∂ p ⟧ X 跟一個元素 x : X，把 x 塞進洞裡重建出完整的 ⟦ p ⟧ X。

  _⋖_ : (p : Poly) {X : 𝓤₀ ̇ } → ⟦ ∂ p ⟧ X → X → ⟦ p ⟧ X
  _⋖_ 𝟘ᵖ ()
  _⋖_ 𝟙ᵖ ()
  (var ⋖ ⋆)                x = x
  ((p ⊕ q) ⋖ inl Γ)        x = inl ((p ⋖ Γ) x)
  ((p ⊕ q) ⋖ inr Γ)        x = inr ((q ⋖ Γ) x)
  ((p ⊗ q) ⋖ inl (Γ , qv)) x = (p ⋖ Γ) x , qv
  ((p ⊗ q) ⋖ inr (pv , Γ)) x = pv , (q ⋖ Γ) x
  infixl  _⋖_