module Kindly.Iso where

--------------------------------------------------------------------------------

import Control.Category (Category (..))
import Data.Kind (Type)
import Kindly.Class (Cat)

--------------------------------------------------------------------------------

-- | An invertible mapping between 'a' and 'b' in category 'cat'.
--
-- === Laws
--
-- @
-- 'fwd' '.' 'bwd' ≡ 'id'
-- 'bwd' '.' 'fwd' ≡ 'id'
-- @
data Iso cat a b = Iso {forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
Iso cat a b -> cat a b
fwd :: a `cat` b, forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
Iso cat a b -> cat b a
bwd :: b `cat` a}

instance (Category cat) => Category (Iso cat) where
  id :: (Category cat) => Iso cat a a
  id :: forall (a :: k). Category cat => Iso cat a a
id = cat a a -> cat a a -> Iso cat a a
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
cat a b -> cat b a -> Iso cat a b
Iso cat a a
forall (a :: k). cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id cat a a
forall (a :: k). cat a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

  (.) :: Iso cat b c -> Iso cat a b -> Iso cat a c
  Iso cat b c
fwd cat c b
bwd . :: forall (b :: k) (c :: k) (a :: k).
Iso cat b c -> Iso cat a b -> Iso cat a c
. Iso cat a b
fwd' cat b a
bwd' = cat a c -> cat c a -> Iso cat a c
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k).
cat a b -> cat b a -> Iso cat a b
Iso (cat b c
fwd cat b c -> cat a b -> cat a c
forall (b :: k) (c :: k) (a :: k). cat b c -> cat a b -> cat a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. cat a b
fwd') (cat b a
bwd' cat b a -> cat c b -> cat c a
forall (b :: k) (c :: k) (a :: k). cat b c -> cat a b -> cat a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. cat c b
bwd)

type (<->) :: Cat Type
type (<->) = Iso (->)