module FP.Prelude.Morphism where

import FP.Prelude.Core

-- 3: arrows
infixr 3 ↝         -- (★ → ★) → (★ → ★) → ★ → ★
infixr 3 ⇝         -- ((★ → ★) → (★ → ★)) → ((★ → ★) → (★ → ★)) → (★ → ★) → ★ → ★

-- 7: composition
infixr 7 ⌾         -- (⌾) ∷ (Category t) ⇒ t b c → t a b → t a c

type m ↝ n = ∀ a. m a → n a
type t ⇝ u = ∀ m. t m ↝ u m

data a ⇄ b = Iso {isoTo ∷ a → b,isoFrom ∷ b → a}
class Isomorphic a b where isomorphic ∷ a ⇄ b

data t ↝⇄ u = Iso2 {isoTo2 ∷ t ↝ u,isoFrom2 ∷ u ↝ t}
class Isomorphic2 t u where isomorphic2 ∷ t ↝⇄ u
iso2FromIso ∷ (∀ a. t a ⇄ u a) → t ↝⇄ u
iso2FromIso f = Iso2 (isoTo f) (isoFrom f)

data v ⇝⇄ w = Iso3 {isoTo3 ∷ v ⇝ w,isoFrom3 ∷ w ⇝ v}
class Isomorphic3 v w where isomorphic3 ∷ v ⇝⇄ w

instance Isomorphic 𝕊 [ℂ] where isomorphic = Iso chars 𝕤

class Category t where {refl ∷ t a a;(⌾) ∷ t b c → t a b → t a c}
class Symmetric t where {sym ∷ t a b → t b a}

instance Category (→) where {refl = id;(⌾) = (∘)}
instance Category (⇄) where {refl = Iso id id;Iso gto gfrom ⌾ Iso fto ffrom = Iso (gto ∘ fto) (ffrom ∘ gfrom)}
instance Symmetric (⇄) where sym (Iso to from) = Iso from to
instance Category (↝⇄) where {refl = Iso2 id id;Iso2 gto gfrom ⌾ Iso2 fto ffrom = Iso2 (gto ∘ fto) (ffrom ∘ gfrom)}
instance Symmetric (↝⇄) where sym (Iso2 to from) = Iso2 from to