module UVMHS.Core.Classes.Morphism where

import UVMHS.Core.Init

infixr 1 →⁻,→⁼,⇄,⇄⁻,⇄⁼
infixl 7 ⊚

type (m ∷ ★ → ★) →⁻ (n ∷ ★ → ★) = ∀ a. m a → n a
type (t ∷ (★ → ★) → ★ → ★) →⁼ (u ∷ (★ → ★) → ★ → ★) = ∀ m. t m →⁻ u m

class a ⇄ b | a → b where
  isoto ∷ a → b
  isofr ∷ b → a
data Iso a b = Iso 
  { forall a b. Iso a b -> a -> b
ito ∷ a → b
  , forall a b. Iso a b -> b -> a
ifr ∷ b → a
  }

toiso ∷ (a ⇄ b) ⇒ Iso a b 
toiso :: forall a b. (a ⇄ b) => Iso a b
toiso = (a -> b) -> (b -> a) -> Iso a b
forall a b. (a -> b) -> (b -> a) -> Iso a b
Iso a -> b
forall a b. (a ⇄ b) => a -> b
isoto b -> a
forall a b. (a ⇄ b) => b -> a
isofr

friso ∷ (a ⇄ b) ⇒ Iso b a
friso :: forall a b. (a ⇄ b) => Iso b a
friso = (b -> a) -> (a -> b) -> Iso b a
forall a b. (a -> b) -> (b -> a) -> Iso a b
Iso b -> a
forall a b. (a ⇄ b) => b -> a
isofr a -> b
forall a b. (a ⇄ b) => a -> b
isoto

class t ⇄⁻ u | t → u where
  isoto2 ∷ t →⁻ u
  isofr2 ∷ u →⁻ t
data Iso2 t u = Iso2 
  { forall (t :: * -> *) (u :: * -> *). Iso2 t u -> t →⁻ u
ito2 ∷ t →⁻ u
  , forall (t :: * -> *) (u :: * -> *). Iso2 t u -> u →⁻ t
ifr2 ∷ u →⁻ t
  }

toiso2 ∷ (t ⇄⁻ u) ⇒ Iso2 t u
toiso2 :: forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => Iso2 t u
toiso2 = (t →⁻ u) -> (u →⁻ t) -> Iso2 t u
forall (t :: * -> *) (u :: * -> *).
(t →⁻ u) -> (u →⁻ t) -> Iso2 t u
Iso2 t a -> u a
t →⁻ u
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 u a -> t a
u →⁻ t
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2

friso2 ∷ (t ⇄⁻ u) ⇒ Iso2 u t
friso2 :: forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => Iso2 u t
friso2 = (u →⁻ t) -> (t →⁻ u) -> Iso2 u t
forall (t :: * -> *) (u :: * -> *).
(t →⁻ u) -> (u →⁻ t) -> Iso2 t u
Iso2 u a -> t a
u →⁻ t
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 t a -> u a
t →⁻ u
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2

class v ⇄⁼ w | v → w where
  isoto3 ∷ v →⁼ w
  isofr3 ∷ w →⁼ v
data Iso3 v w = Iso3
  { forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
Iso3 v w -> v →⁼ w
ito3 ∷ v →⁼ w
  , forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
Iso3 v w -> w →⁼ v
ifr3 ∷ w →⁼ v
  }

toiso3 ∷ (v ⇄⁼ w) ⇒ Iso3 v w
toiso3 :: forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
Iso3 v w
toiso3 = (v →⁼ w) -> (w →⁼ v) -> Iso3 v w
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v →⁼ w) -> (w →⁼ v) -> Iso3 v w
Iso3 v m a -> w m a
v →⁼ w
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3 w m a -> v m a
w →⁼ v
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3

friso3 ∷ (v ⇄⁼ w) ⇒ Iso3 w v
friso3 :: forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
Iso3 w v
friso3 = (w →⁼ v) -> (v →⁼ w) -> Iso3 w v
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v →⁼ w) -> (w →⁼ v) -> Iso3 v w
Iso3 w m a -> v m a
w →⁼ v
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
w →⁼ v
isofr3 v m a -> w m a
v →⁼ w
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v ⇄⁼ w) =>
v →⁼ w
isoto3

class Reflexive t where refl ∷ t a a
class Transitive t where (⊚) ∷ t b c → t a b → t a c
class (Reflexive t,Transitive t) ⇒ Category t
class Symmetric t where {sym ∷ t a b → t b a}

instance Reflexive (→) where 
  refl :: forall a. a -> a
refl = a -> a
forall a. a -> a
id
instance Transitive (→) where 
  ⊚ :: forall b c a. (b -> c) -> (a -> b) -> a -> c
(⊚) = (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(∘)
instance Category (→)

instance Reflexive Iso where 
  refl :: forall a. Iso a a
refl = (a -> a) -> (a -> a) -> Iso a a
forall a b. (a -> b) -> (b -> a) -> Iso a b
Iso a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id
instance Transitive Iso where
  Iso b -> c
gto c -> b
gfrom ⊚ :: forall b c a. Iso b c -> Iso a b -> Iso a c
⊚ Iso a -> b
fto b -> a
ffrom = (a -> c) -> (c -> a) -> Iso a c
forall a b. (a -> b) -> (b -> a) -> Iso a b
Iso (b -> c
gto (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
fto) (b -> a
ffrom (b -> a) -> (c -> b) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ c -> b
gfrom)
instance Symmetric Iso where 
  sym :: forall a b. Iso a b -> Iso b a
sym (Iso a -> b
to b -> a
from) = (b -> a) -> (a -> b) -> Iso b a
forall a b. (a -> b) -> (b -> a) -> Iso a b
Iso b -> a
from a -> b
to
instance Category Iso
instance Reflexive Iso2 where 
  refl :: forall (a :: * -> *). Iso2 a a
refl = (a →⁻ a) -> (a →⁻ a) -> Iso2 a a
forall (t :: * -> *) (u :: * -> *).
(t →⁻ u) -> (u →⁻ t) -> Iso2 t u
Iso2 a a -> a a
forall a. a -> a
a →⁻ a
id a a -> a a
forall a. a -> a
a →⁻ a
id
instance Transitive Iso2 where 
  Iso2 b →⁻ c
gto c →⁻ b
gfrom ⊚ :: forall (b :: * -> *) (c :: * -> *) (a :: * -> *).
Iso2 b c -> Iso2 a b -> Iso2 a c
⊚ Iso2 a →⁻ b
fto b →⁻ a
ffrom = (a →⁻ c) -> (c →⁻ a) -> Iso2 a c
forall (t :: * -> *) (u :: * -> *).
(t →⁻ u) -> (u →⁻ t) -> Iso2 t u
Iso2 (b a -> c a
b →⁻ c
gto (b a -> c a) -> (a a -> b a) -> a a -> c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a a -> b a
a →⁻ b
fto) (b a -> a a
b →⁻ a
ffrom (b a -> a a) -> (c a -> b a) -> c a -> a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ c a -> b a
c →⁻ b
gfrom)
instance Symmetric Iso2 where 
  sym :: forall (a :: * -> *) (b :: * -> *). Iso2 a b -> Iso2 b a
sym (Iso2 a →⁻ b
to b →⁻ a
from) = (b →⁻ a) -> (a →⁻ b) -> Iso2 b a
forall (t :: * -> *) (u :: * -> *).
(t →⁻ u) -> (u →⁻ t) -> Iso2 t u
Iso2 b a -> a a
b →⁻ a
from a a -> b a
a →⁻ b
to
instance Category Iso2
instance Reflexive Iso3 where 
  refl :: forall (a :: (* -> *) -> * -> *). Iso3 a a
refl = (a →⁼ a) -> (a →⁼ a) -> Iso3 a a
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v →⁼ w) -> (w →⁼ v) -> Iso3 v w
Iso3 a m a -> a m a
forall a. a -> a
a →⁼ a
id a m a -> a m a
forall a. a -> a
a →⁼ a
id
instance Transitive Iso3 where 
  Iso3 b →⁼ c
gto c →⁼ b
gfrom ⊚ :: forall (b :: (* -> *) -> * -> *) (c :: (* -> *) -> * -> *)
       (a :: (* -> *) -> * -> *).
Iso3 b c -> Iso3 a b -> Iso3 a c
⊚ Iso3 a →⁼ b
fto b →⁼ a
ffrom = (a →⁼ c) -> (c →⁼ a) -> Iso3 a c
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v →⁼ w) -> (w →⁼ v) -> Iso3 v w
Iso3 (b m a -> c m a
b →⁼ c
gto (b m a -> c m a) -> (a m a -> b m a) -> a m a -> c m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a m a -> b m a
a →⁼ b
fto) (b m a -> a m a
b →⁼ a
ffrom (b m a -> a m a) -> (c m a -> b m a) -> c m a -> a m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ c m a -> b m a
c →⁼ b
gfrom)
instance Symmetric Iso3 where 
  sym :: forall (a :: (* -> *) -> * -> *) (b :: (* -> *) -> * -> *).
Iso3 a b -> Iso3 b a
sym (Iso3 a →⁼ b
to b →⁼ a
from) = (b →⁼ a) -> (a →⁼ b) -> Iso3 b a
forall (v :: (* -> *) -> * -> *) (w :: (* -> *) -> * -> *).
(v →⁼ w) -> (w →⁼ v) -> Iso3 v w
Iso3 b m a -> a m a
b →⁼ a
from a m a -> b m a
a →⁼ b
to
instance Category Iso3