Let's try theorem 5 from [ACMP'25].
p ↠ p ↠ (p ∙ p)
becomes, after "constructive resource semantics" encoding,
∀α₁α₂.p @ α₁ → p @ α₂ → ∃β₁β₂(α₁α₂ = β₁β₂) × p @ β₁ × p @ β₂
or, expanded out into types, let's suppose we have
Q : (W : Type) (μ : Monoid W) (p : W → Type) (α₁ α₂ : W) (x₁ : p α₁) (x₂ : p α₂)
→ (β₁ β₂ : W) × (α₁α₂ ≡ β₁β₂) × (p β₁) × (p β₂)
and suppose we have all the data to give its arguments:
(W : Type) (μ : Monoid W) (p : W → Type) (α₁ α₂ : W) (x₁ : p α₁) (x₂ : p α₂)
What we really want to show is "the only possible function of that type is the one that reassembles its arguments in the correct order", i.e. we want to prove
Q W μ p α₁ α₂ x₁ x₂ = ⟨α₁, α₂, rfl, x₁, x₂⟩
We can do this as follows:
data Bit : Type where
| b₁ : Bit
| b₂ : Bit
W' = G(_÷W).List(Bit)
μ' : Monoid(W')
μ' = { e = gel(e, 0), _*_ = gel(_*_, λab.ungel(a) @ ungel(b)), … }
p' : G(_÷W).List(Bit) → Type
p' w' = G(x÷p w').(w' ≡ α₁ × x ≡ x₁ × ungel(w') ≡ [b₁]) + (w' ≡ α₂ × x ≡ x₂ × ungel(w') ≡ [b₂])
let (β₁ β₂ : W') (e : gel(α₁ * α₂, [b₁, b₂]) ≡ β₁ * β₂) (j₁ : p' β₁) (j₂ : p' β₂) =
Q W' μ' p' (gel(α₁, [b₁])) (gel(α₂, [b₂]))
(gel(x₁, inl ⟨rfl,rfl,rfl⟩)) (gel(x₂, inr ⟨rfl,rfl,rfl⟩))
Q' : Q W μ p α₁ α₂ x₁ x₂ = ⟨α₁, α₂, rfl, x₁, x₂⟩
Q' = case (j₁, j₂) of
| (inl _, inl _) ⇒ obtain [b₁, b₂] ≡ [b₁, b₁] which is a contradiction
| (inl ⟨rfl, rfl, rfl⟩, inr ⟨rfl, rfl rfl⟩) ⇒ rfl
| (inr _, inl _) ⇒ obtain [b₁, b₂] ≡ [b₂, b₁] which is a contradiction
| (inr _, inr _) ⇒ obtain [b₁, b₂] ≡ [b₂, b₂] which is a contradiction
Now let's try to reason about
(p ⊸ p) ⊸ (p ⊸ p)
There should only be one function of this type. The "constructive resource semantics" encoding gives the type
Q : (W : Type) (μ : CommMonoid W) (p : W → Type) (α β : W)
(s : (δ : W) (m : p δ) → p (α * δ)) (z : p β) → p (α * β)
And let's assume we have some arguments:
(W : Type) (μ : CommMonoid W) (p : W → Type) (α β : W)
(s : (δ : W) (m : p δ) → p (α * δ)) (z : p β) → p (α * β)
We do the following programming:
iter 0 = z
iter (n+1) = s _ (iter n)
μ' : CommMonoid(G(_÷W).ℕ))
μ' = { e = gel(e, 0), _*_ = gel(_*_, λab.ungel(a) + ungel(b)), … }
p' : G(_÷W).ℕ → Type
p' w' = G(x÷p w').(x ≡ iter (ungel w'))
s' : (δ' : G(_÷W).ℕ)) (m' : p' δ') → p' (gel(α,1) * δ')
s' δ' m' = gel(s δ' m', rfl)
z' : p' (gel(β,0))
z' = gel(z, rfl)
Q' : Q W μ p α β s z = iter 1
Q' = ungel(
Q (G(_÷W).ℕ) μ' p' (gel(α,1)) (gel(β,0)) s' z'
)
And so we've proven that Q W μ p α β s z must be s z.