Oh, really?

 Okay, we have this in Agda:

module I where

open import Data.Unit
open import Relation.Binary.PropositionalEquality

private variable
A : Set

to : (⊤ → A) → A
to f = f tt

from : A → ⊤ → A
from x _ = x

to∘from : ∀ {A} (x : A) → to (from x) ≡ x
to∘from _ = refl

from∘to : ∀ {A} (x : ⊤ → A) → from (to x) ≡ x
from∘to _ = refl

We can abstract away from computation... This makes sense for a total specification language, all computations terminate with some answer and therefore you can substitute that answer.

But it is a bit suspect, and possibly restrictive, at the same time too.

Edit: It's more than suspect but absurd.