Isomorphism according to Homotopy Type Theory, page 8

Iso.hs

{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
{-# LANGUAGE Haskell2010
  , TypeFamilies
  , DataKinds
  , PolyKinds
  , RankNTypes
  , TypeOperators
  , TemplateHaskell
  , GADTs
  , ScopedTypeVariables
  , NoStarIsType
  , TypeApplications
  , BlockArguments
  , LambdaCase
  , UndecidableInstances
#-}

import Data.Singletons.Prelude
import Data.Singletons.TH

-- Iso definition from HoTT page 8

-- using the fact that `exist n . P n`
-- is equivalent to `forall r . (forall n . P n -> r) -> r`
newtype a ~= b = MkIso ( forall r . (forall (f :: a ~> b)
                     . ( forall s . (forall (g :: b ~> a)
                     . Sing f -> Sing g
                    -> (forall (x :: a) . Sing x -> g @@ (f @@ x) :~: x)
                    -> (forall (y :: b) . Sing y -> f @@ (g @@ y) :~: y)
                    -> s) -> s) -> r) -> r)

infix 4 ~=

type Iso a b = a ~= b

isoRefl :: a ~= a
isoRefl = MkIso \a -> a \b -> b
  (sing @IdSym0) (sing @IdSym0) (const Refl) (const Refl)

isoSym :: a ~= b -> b ~= a
isoSym (MkIso iso) = iso \n ->
  n \f g fax fay ->
    MkIso \a -> a \b -> b g f fay fax

isoTrans :: forall a b c . a ~= b -> b ~= c -> a ~= c
isoTrans (MkIso iso) (MkIso iso') =
  iso  \n -> n \f  g  fax  fay  ->
  iso' \m -> m \f' g' fax' fay' ->
      MkIso \a -> a \b -> b
        (f' %.$$$ f )
        (g  %.$$$ g')
        (\x -> case (fax x,  fax' $ f %$ x) of (Refl, Refl) -> Refl)
        (\y -> case (fay $ g' %$ y, fay' y) of (Refl, Refl) -> Refl)
  where
    -- helper composition function that produces a singleton of a
    -- function instead of the usual (%.)
    (%.$$$) :: Sing f -> Sing g -> Sing (f .@#@$$$ g)
    (%.$$$) f g = SLambda \x -> f %$ g %$ x

-- If you want to get a function of type `a -> b`, just convince ghc that `Demote a ~ a` etc.
right :: forall a b . (SingKind a, SingKind b) => a ~= b -> Demote a -> Demote b
right (MkIso iso) = iso \n -> n \f _ _ _ -> fromSing f

left :: forall a b . (SingKind a, SingKind b) => a ~= b -> Demote b -> Demote a
left (MkIso iso) = iso \n -> n \_ g _ _ -> fromSing g

eqToIso :: a :~: b -> a ~= b
eqToIso Refl = isoRefl

-- Example usage:

singletons [d|
  data Unit = MkUnit

  unitToO :: Unit -> ()
  unitToO MkUnit = ()

  oToUnit :: () -> Unit
  oToUnit () = MkUnit
  |]

unitIsUnit :: Unit ~= ()
unitIsUnit = MkIso \a -> a \b -> b
  (sing @UnitToOSym0) (sing @OToUnitSym0) (\SMkUnit -> Refl) (\STuple0 -> Refl)

notIso :: Bool ~= Bool
notIso = MkIso \a -> a \b -> b
  (sing @NotSym0)
  (sing @NotSym0)
  \case STrue  -> Refl
        SFalse -> Refl
  \case STrue  -> Refl
        SFalse -> Refl

singletons [d|
  data Nat = Z | S Nat

  natReplicate :: Nat -> a -> [a]
  natReplicate Z     _ = []
  natReplicate (S n) x = x : natReplicate n x

  natLength :: [a] -> Nat
  natLength []     = Z
  natLength (_:xs) = S (natLength xs)
  |]

natListIso :: Nat ~= [()]
natListIso = MkIso \a -> a \b -> b
  (sing @(FlipSym1 NatReplicateSym0 @@ '())) (sing @NatLengthSym0) p q
  where
    p :: Sing x -> NatLength (NatReplicate x '()) :~: x
    p SZ = Refl
    p (SS n) | Refl <- p n = Refl
    q :: Sing y -> NatReplicate (NatLength y) '() :~: y
    q SNil = Refl
    q (SCons STuple0 xs) | Refl <- q xs = Refl