module FP.Prelude.Morphism where
import FP.Prelude.Core
infixr 3 ↝
infixr 3 ⇝
infixr 7 ⌾
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