{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2011-2015 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  polykinds
--
----------------------------------------------------------------------------

module Data.Isomorphism
  ( Iso(..)
  ) where

import Control.Category
import Data.Semigroupoid
import Data.Groupoid
import Prelude ()

data Iso k a b = Iso { forall {k} (k :: k -> k -> *) (a :: k) (b :: k). Iso k a b -> k a b
embed :: k a b, forall {k} (k :: k -> k -> *) (a :: k) (b :: k). Iso k a b -> k b a
project :: k b a }

instance Semigroupoid k => Semigroupoid (Iso k) where
  Iso k j k1
f k k1 j
g o :: forall (j :: k) (k1 :: k) (i :: k).
Iso k j k1 -> Iso k i j -> Iso k i k1
`o` Iso k i j
h k j i
i = k i k1 -> k k1 i -> Iso k i k1
forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
k a b -> k b a -> Iso k a b
Iso (k j k1
f k j k1 -> k i j -> k i k1
forall (j :: k) (k1 :: k) (i :: k). k j k1 -> k i j -> k i k1
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` k i j
h) (k j i
i k j i -> k k1 j -> k k1 i
forall (j :: k) (k1 :: k) (i :: k). k j k1 -> k i j -> k i k1
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` k k1 j
g)

instance Semigroupoid k => Groupoid (Iso k) where
  inv :: forall (a :: k) (b :: k). Iso k a b -> Iso k b a
inv (Iso k a b
f k b a
g) = k b a -> k a b -> Iso k b a
forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
k a b -> k b a -> Iso k a b
Iso k b a
g k a b
f

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