For Id, is there actually a type Psi such that Psi <~> (Id[Psi] ⇒ A)?
Does this Haskell code answer your question?
data Fix f = MakeFix (f (Fix f)) data Id x = MakeId x data PrePsi a x = MakePrePsi (Id x -> a) type Psi a = Fix (PrePsi a)
The two directions of isomorphism:
forward :: Psi a -> (Id (Psi a) -> a) forward (MakeFix (MakePrePsi x)) = x backward :: (Id (Psi a) -> a) -> Psi a backward x = MakeFix (MakePrePsi x)
Isn’t that where the Y combinator comes in?
Not sure. Fix is a type-level Y combinator, while loeb is a value-level Y combinator.
(I wish we were working with a proof that didn’t invoke this external lemma)
I think that’s not possible. Löb’s theorem requires the diagonal lemma.
Does this Haskell code answer your question?
The two directions of isomorphism:
Not sure. Fix is a type-level Y combinator, while loeb is a value-level Y combinator.
I think that’s not possible. Löb’s theorem requires the diagonal lemma.