    {-# 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