{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.Hom.Definition

-- Description : basic definitions of homomorphisms.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- basic definitions of homomorphisms.

module OAlg.Hom.Definition
  (
    -- * Disjunctive

    HomDisj(..), homDisj
  , HomDisjEmpty

    -- * Contravariant Isomorphism

  , IsoHomDisj, isoHomDisj, isoHomDisj'
  , IsoO, toDualO, toDualO'
  , ReflO, reflO


    -- * Empty

  , HomEmpty, fromHomEmpty

    -- * Id

  , HomId(..)

    -- * Hom

  , Hom, HomD
    
    -- * X

  , xscmHomDisj
  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.Dualisable
import OAlg.Category.SDuality
import OAlg.Category.Unify

import OAlg.Data.Variant

import OAlg.Structure.Oriented
import OAlg.Structure.Fibred

--------------------------------------------------------------------------------

-- HomDisj -


-- | disjunctive family of homomorphsims.

newtype HomDisj s o h x y = HomDisj (SHom s s o h x y)
  deriving (Int -> HomDisj s o h x y -> ShowS
[HomDisj s o h x y] -> ShowS
HomDisj s o h x y -> String
(Int -> HomDisj s o h x y -> ShowS)
-> (HomDisj s o h x y -> String)
-> ([HomDisj s o h x y] -> ShowS)
-> Show (HomDisj s o h x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
Int -> HomDisj s o h x y -> ShowS
forall s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
[HomDisj s o h x y] -> ShowS
forall s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
HomDisj s o h x y -> String
$cshowsPrec :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
Int -> HomDisj s o h x y -> ShowS
showsPrec :: Int -> HomDisj s o h x y -> ShowS
$cshow :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
HomDisj s o h x y -> String
show :: HomDisj s o h x y -> String
$cshowList :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
[HomDisj s o h x y] -> ShowS
showList :: [HomDisj s o h x y] -> ShowS
Show,(forall a b. HomDisj s o h a b -> String) -> Show2 (HomDisj s o h)
forall a b. HomDisj s o h a b -> String
forall s (o :: * -> *) (h :: * -> * -> *) a b.
Show2 h =>
HomDisj s o h a b -> String
forall (h :: * -> * -> *). (forall a b. h a b -> String) -> Show2 h
$cshow2 :: forall s (o :: * -> *) (h :: * -> * -> *) a b.
Show2 h =>
HomDisj s o h a b -> String
show2 :: forall a b. HomDisj s o h a b -> String
Show2,HomDisj s o h x y -> Statement
(HomDisj s o h x y -> Statement) -> Validable (HomDisj s o h x y)
forall a. (a -> Statement) -> Validable a
forall s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
HomDisj s o h x y -> Statement
$cvalid :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
HomDisj s o h x y -> Statement
valid :: HomDisj s o h x y -> Statement
Validable,(forall x y. HomDisj s o h x y -> Statement)
-> Validable2 (HomDisj s o h)
forall x y. HomDisj s o h x y -> Statement
forall s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
HomDisj s o h x y -> Statement
forall (h :: * -> * -> *).
(forall x y. h x y -> Statement) -> Validable2 h
$cvalid2 :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
HomDisj s o h x y -> Statement
valid2 :: forall x y. HomDisj s o h x y -> Statement
Validable2,HomDisj s o h x y -> Variant
(HomDisj s o h x y -> Variant) -> Disjunctive (HomDisj s o h x y)
forall x. (x -> Variant) -> Disjunctive x
forall s (o :: * -> *) (h :: * -> * -> *) x y.
HomDisj s o h x y -> Variant
$cvariant :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
HomDisj s o h x y -> Variant
variant :: HomDisj s o h x y -> Variant
Disjunctive,(forall x y. HomDisj s o h x y -> Variant)
-> Disjunctive2 (HomDisj s o h)
forall x y. HomDisj s o h x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *).
(forall (x :: k) (y :: k1). h x y -> Variant) -> Disjunctive2 h
forall s (o :: * -> *) (h :: * -> * -> *) x y.
HomDisj s o h x y -> Variant
$cvariant2 :: forall s (o :: * -> *) (h :: * -> * -> *) x y.
HomDisj s o h x y -> Variant
variant2 :: forall x y. HomDisj s o h x y -> Variant
Disjunctive2)

deriving instance (Morphism h, Eq2 h, Transformable s Typ) => Eq2 (HomDisj s o h)
deriving instance (Morphism h, Eq2 h, Transformable s Typ) => Eq (HomDisj s o h x y)

instance Morphism h => Morphism (HomDisj s o h) where
  type ObjectClass (HomDisj s o h) = s
  homomorphous :: forall x y.
HomDisj s o h x y -> Homomorphous (ObjectClass (HomDisj s o h)) x y
homomorphous (HomDisj SHom s s o h x y
h) = SHom s s o h x y -> Homomorphous (ObjectClass (SHom s s o h)) x y
forall x y.
SHom s s o h x y -> Homomorphous (ObjectClass (SHom s s o h)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous SHom s s o h x y
h

instance Morphism h => Category (HomDisj s o h) where
  cOne :: forall x.
Struct (ObjectClass (HomDisj s o h)) x -> HomDisj s o h x x
cOne = SHom s s o h x x -> HomDisj s o h x x
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj (SHom s s o h x x -> HomDisj s o h x x)
-> (Struct s x -> SHom s s o h x x)
-> Struct s x
-> HomDisj s o h x x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct s x -> SHom s s o h x x
Struct (ObjectClass (SHom s s o h)) x -> SHom s s o h x x
forall x. Struct (ObjectClass (SHom s s o h)) x -> SHom s s o h x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne 
  HomDisj SHom s s o h y z
f . :: forall y z x.
HomDisj s o h y z -> HomDisj s o h x y -> HomDisj s o h x z
. HomDisj SHom s s o h x y
g = SHom s s o h x z -> HomDisj s o h x z
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj (SHom s s o h y z
f SHom s s o h y z -> SHom s s o h x y -> SHom s s o h x z
forall y z x.
SHom s s o h y z -> SHom s s o h x y -> SHom s s o h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SHom s s o h x y
g)

instance Morphism h => CategoryDisjunctive (HomDisj s o h)


instance (Morphism h, TransformableGRefl o s) => CategoryDualisable o (HomDisj s o h) where
  cToDual :: forall x.
Struct (ObjectClass (HomDisj s o h)) x
-> Variant2 'Contravariant (HomDisj s o h) x (o x)
cToDual Struct (ObjectClass (HomDisj s o h)) x
s   = HomDisj s o h x (o x)
-> Variant2 'Contravariant (HomDisj s o h) x (o x)
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (SHom s s o h x (o x) -> HomDisj s o h x (o x)
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj SHom s s o h x (o x)
t) where Contravariant2 SHom s s o h x (o x)
t = Struct (ObjectClass (SHom s s o h)) x
-> Variant2 'Contravariant (SHom s s o h) x (o x)
forall x.
Struct (ObjectClass (SHom s s o h)) x
-> Variant2 'Contravariant (SHom s s o h) x (o x)
forall (o :: * -> *) (h :: * -> * -> *) x.
CategoryDualisable o h =>
Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
cToDual Struct (ObjectClass (SHom s s o h)) x
Struct (ObjectClass (HomDisj s o h)) x
s
  cFromDual :: forall x.
Struct (ObjectClass (HomDisj s o h)) x
-> Variant2 'Contravariant (HomDisj s o h) (o x) x
cFromDual Struct (ObjectClass (HomDisj s o h)) x
s = HomDisj s o h (o x) x
-> Variant2 'Contravariant (HomDisj s o h) (o x) x
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (SHom s s o h (o x) x -> HomDisj s o h (o x) x
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj SHom s s o h (o x) x
f) where Contravariant2 SHom s s o h (o x) x
f = Struct (ObjectClass (SHom s s o h)) x
-> Variant2 'Contravariant (SHom s s o h) (o x) x
forall x.
Struct (ObjectClass (SHom s s o h)) x
-> Variant2 'Contravariant (SHom s s o h) (o x) x
forall (o :: * -> *) (h :: * -> * -> *) x.
CategoryDualisable o h =>
Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
cFromDual Struct (ObjectClass (SHom s s o h)) x
Struct (ObjectClass (HomDisj s o h)) x
s

instance (Morphism h, ApplicativeG Id h c, DualisableG s c o Id, c ~ (->))
  => ApplicativeG Id (HomDisj s o h) c where
  amapG :: forall x y. HomDisj s o h x y -> c (Id x) (Id y)
amapG (HomDisj SHom s s o h x y
h) = SHom s s o h x y -> Id x -> Id y
forall (d :: * -> *) r s (o :: * -> *) (h :: * -> * -> *) x y.
ApplicativeG (SVal d) (SHom r s o h) (->) =>
SHom r s o h x y -> d x -> d y
smap SHom s s o h x y
h

instance (Morphism h, ApplicativeG Id h c, DualisableG s c o Id, c ~ (->))
  => FunctorialG Id (HomDisj s o h) c

instance (Morphism h, ApplicativePoint h, DualisableG s (->) o Pnt)
  => ApplicativeG Pnt (HomDisj s o h) (->) where
  amapG :: forall x y. HomDisj s o h x y -> Pnt x -> Pnt y
amapG (HomDisj SHom s s o h x y
h) = SHom s s o h x y -> Pnt x -> Pnt y
forall (d :: * -> *) r s (o :: * -> *) (h :: * -> * -> *) x y.
ApplicativeG (SVal d) (SHom r s o h) (->) =>
SHom r s o h x y -> d x -> d y
smap SHom s s o h x y
h

instance (Morphism h, ApplicativePoint h, DualisableG s (->) o Pnt)
  => FunctorialG Pnt (HomDisj s o h) (->)

instance (Morphism h, ApplicativeRoot h, DualisableG s (->) o Rt)
  => ApplicativeG Rt (HomDisj s o h) (->) where
  amapG :: forall x y. HomDisj s o h x y -> Rt x -> Rt y
amapG (HomDisj SHom s s o h x y
h) = SHom s s o h x y -> Rt x -> Rt y
forall (d :: * -> *) r s (o :: * -> *) (h :: * -> * -> *) x y.
ApplicativeG (SVal d) (SHom r s o h) (->) =>
SHom r s o h x y -> d x -> d y
smap SHom s s o h x y
h

instance (Morphism h, ApplicativeRoot h, DualisableG s (->) o Rt)
  => FunctorialG Rt (HomDisj s o h) (->)

--------------------------------------------------------------------------------

-- HomEmpty -


-- | the empty family of homomorphisms.

newtype HomEmpty s x y = HomEmpty (EntEmpty2 x y)
  deriving (Int -> HomEmpty s x y -> ShowS
[HomEmpty s x y] -> ShowS
HomEmpty s x y -> String
(Int -> HomEmpty s x y -> ShowS)
-> (HomEmpty s x y -> String)
-> ([HomEmpty s x y] -> ShowS)
-> Show (HomEmpty s x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s x y. Int -> HomEmpty s x y -> ShowS
forall s x y. [HomEmpty s x y] -> ShowS
forall s x y. HomEmpty s x y -> String
$cshowsPrec :: forall s x y. Int -> HomEmpty s x y -> ShowS
showsPrec :: Int -> HomEmpty s x y -> ShowS
$cshow :: forall s x y. HomEmpty s x y -> String
show :: HomEmpty s x y -> String
$cshowList :: forall s x y. [HomEmpty s x y] -> ShowS
showList :: [HomEmpty s x y] -> ShowS
Show, (forall a b. HomEmpty s a b -> String) -> Show2 (HomEmpty s)
forall a b. HomEmpty s a b -> String
forall s x y. HomEmpty s x y -> String
forall (h :: * -> * -> *). (forall a b. h a b -> String) -> Show2 h
$cshow2 :: forall s x y. HomEmpty s x y -> String
show2 :: forall a b. HomEmpty s a b -> String
Show2,HomEmpty s x y -> HomEmpty s x y -> Bool
(HomEmpty s x y -> HomEmpty s x y -> Bool)
-> (HomEmpty s x y -> HomEmpty s x y -> Bool)
-> Eq (HomEmpty s x y)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s x y. HomEmpty s x y -> HomEmpty s x y -> Bool
$c== :: forall s x y. HomEmpty s x y -> HomEmpty s x y -> Bool
== :: HomEmpty s x y -> HomEmpty s x y -> Bool
$c/= :: forall s x y. HomEmpty s x y -> HomEmpty s x y -> Bool
/= :: HomEmpty s x y -> HomEmpty s x y -> Bool
Eq,(forall x y. HomEmpty s x y -> HomEmpty s x y -> Bool)
-> Eq2 (HomEmpty s)
forall x y. HomEmpty s x y -> HomEmpty s x y -> Bool
forall s x y. HomEmpty s x y -> HomEmpty s x y -> Bool
forall (h :: * -> * -> *).
(forall x y. h x y -> h x y -> Bool) -> Eq2 h
$ceq2 :: forall s x y. HomEmpty s x y -> HomEmpty s x y -> Bool
eq2 :: forall x y. HomEmpty s x y -> HomEmpty s x y -> Bool
Eq2,(forall x y. HomEmpty s x y -> HomEmpty s x y -> Statement)
-> EqExt (HomEmpty s)
forall x y. HomEmpty s x y -> HomEmpty s x y -> Statement
forall s x y. HomEmpty s x y -> HomEmpty s x y -> Statement
forall (c :: * -> * -> *).
(forall x y. c x y -> c x y -> Statement) -> EqExt c
$c.=. :: forall s x y. HomEmpty s x y -> HomEmpty s x y -> Statement
.=. :: forall x y. HomEmpty s x y -> HomEmpty s x y -> Statement
EqExt,HomEmpty s x y -> Statement
(HomEmpty s x y -> Statement) -> Validable (HomEmpty s x y)
forall a. (a -> Statement) -> Validable a
forall s x y. HomEmpty s x y -> Statement
$cvalid :: forall s x y. HomEmpty s x y -> Statement
valid :: HomEmpty s x y -> Statement
Validable,(forall x y. HomEmpty s x y -> Statement)
-> Validable2 (HomEmpty s)
forall x y. HomEmpty s x y -> Statement
forall s x y. HomEmpty s x y -> Statement
forall (h :: * -> * -> *).
(forall x y. h x y -> Statement) -> Validable2 h
$cvalid2 :: forall s x y. HomEmpty s x y -> Statement
valid2 :: forall x y. HomEmpty s x y -> Statement
Validable2)

--------------------------------------------------------------------------------

-- fromHomEmpty -


-- | the empty map.

fromHomEmpty :: HomEmpty s a b -> x
fromHomEmpty :: forall s a b x. HomEmpty s a b -> x
fromHomEmpty (HomEmpty EntEmpty2 a b
e) = EntEmpty2 a b -> x
forall a b x. EntEmpty2 a b -> x
fromEmpty2 EntEmpty2 a b
e

--------------------------------------------------------------------------------

-- HomEmpty - Instances -


instance Morphism (HomEmpty s) where
  type ObjectClass (HomEmpty s) = s
  domain :: forall x y. HomEmpty s x y -> Struct (ObjectClass (HomEmpty s)) x
domain = HomEmpty s x y -> Struct s x
HomEmpty s x y -> Struct (ObjectClass (HomEmpty s)) x
forall s a b x. HomEmpty s a b -> x
fromHomEmpty
  range :: forall x y. HomEmpty s x y -> Struct (ObjectClass (HomEmpty s)) y
range  = HomEmpty s x y -> Struct s y
HomEmpty s x y -> Struct (ObjectClass (HomEmpty s)) y
forall s a b x. HomEmpty s a b -> x
fromHomEmpty

instance ApplicativeG Id (HomEmpty s) c where amapG :: forall x y. HomEmpty s x y -> c (Id x) (Id y)
amapG = HomEmpty s x y -> c (Id x) (Id y)
forall s a b x. HomEmpty s a b -> x
fromHomEmpty
instance ApplicativeG Pnt (HomEmpty s) c where amapG :: forall x y. HomEmpty s x y -> c (Pnt x) (Pnt y)
amapG = HomEmpty s x y -> c (Pnt x) (Pnt y)
forall s a b x. HomEmpty s a b -> x
fromHomEmpty
instance ApplicativeG Rt (HomEmpty s) c where amapG :: forall x y. HomEmpty s x y -> c (Rt x) (Rt y)
amapG = HomEmpty s x y -> c (Rt x) (Rt y)
forall s a b x. HomEmpty s a b -> x
fromHomEmpty

--------------------------------------------------------------------------------

-- homDisj -


-- | canonical embedding of a @h@ into 'HomDisj' as a covariant morphism.

homDisj :: (Morphism h, Transformable (ObjectClass h) s)
  => h x y -> Variant2 Covariant (HomDisj s o h) x y
homDisj :: forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj h x y
h = HomDisj s o h x y -> Variant2 'Covariant (HomDisj s o h) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (SHom s s o h x y -> HomDisj s o h x y
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj SHom s s o h x y
h') where Covariant2 SHom s s o h x y
h' = h x y -> Variant2 'Covariant (SHom s s o h) x y
forall (h :: * -> * -> *) s x y r (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (SHom r s o h) x y
sCov h x y
h

--------------------------------------------------------------------------------

-- HomDisjEmpty -


-- | 'HomDisj' for 'HomEmpty'.

type HomDisjEmpty s o = HomDisj s o (HomEmpty s)

instance TransformableGObjectClassDomain Id (HomDisj OrtX Op (HomEmpty OrtX)) EqEOrt
instance TransformableGObjectClassDomain Pnt (HomDisj OrtX Op (HomEmpty OrtX)) EqEOrt
instance TransformableObjectClass OrtX (HomDisj OrtX Op (HomEmpty OrtX))
instance Transformable s Typ => EqExt (HomDisjEmpty s Op)

--------------------------------------------------------------------------------

-- IsoHomDisj -


-- | type for contravariant isomorphism of @'HomDisj' __s o h x__ (__o x__)@.

type IsoHomDisj s o h = Inv2 (HomDisj s o h)

--------------------------------------------------------------------------------

-- isoHomDisj -


-- | contravariant isomorphism for @'HomDisj' __s o h x__ (__o x__)@.

isoHomDisj :: (Morphism h, TransformableGRefl o s)
  => Struct s x -> Variant2 Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj :: forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct s x
s = IsoHomDisj s o h x (o x)
-> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (HomDisj s o h x (o x)
-> HomDisj s o h (o x) x -> IsoHomDisj s o h x (o x)
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 HomDisj s o h x (o x)
t HomDisj s o h (o x) x
f) where
  Contravariant2 HomDisj s o h x (o x)
t = Struct (ObjectClass (HomDisj s o h)) x
-> Variant2 'Contravariant (HomDisj s o h) x (o x)
forall x.
Struct (ObjectClass (HomDisj s o h)) x
-> Variant2 'Contravariant (HomDisj s o h) x (o x)
forall (o :: * -> *) (h :: * -> * -> *) x.
CategoryDualisable o h =>
Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
cToDual Struct s x
Struct (ObjectClass (HomDisj s o h)) x
s
  Contravariant2 HomDisj s o h (o x) x
f = Struct (ObjectClass (HomDisj s o h)) x
-> Variant2 'Contravariant (HomDisj s o h) (o x) x
forall x.
Struct (ObjectClass (HomDisj s o h)) x
-> Variant2 'Contravariant (HomDisj s o h) (o x) x
forall (o :: * -> *) (h :: * -> * -> *) x.
CategoryDualisable o h =>
Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
cFromDual Struct s x
Struct (ObjectClass (HomDisj s o h)) x
s

--------------------------------------------------------------------------------

-- isoHomDisj' -


-- | contravariant isomorphism for @'HomDisj' __s o h x__ (__o x__)@ given by the proxy type.

isoHomDisj' :: (Morphism h, TransformableGRefl o s)
  => q h -> Struct s x -> Variant2 Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj' :: forall (h :: * -> * -> *) (o :: * -> *) s (q :: (* -> * -> *) -> *)
       x.
(Morphism h, TransformableGRefl o s) =>
q h
-> Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj' q h
_ = Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj

--------------------------------------------------------------------------------

-- IsoO -


-- | the type for @__o__@-isomorphisms in the category @'HomDisjEmpty' __r o__@.

type IsoO r o = Inv2 (HomDisjEmpty r o)

--------------------------------------------------------------------------------

-- toDualO -


-- | the contravariant to-dual @__o__@ isomorphism.

toDualO :: TransformableGRefl o r
  => Struct r x -> Variant2 Contravariant (IsoO r o) x (o x)
toDualO :: forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO = Struct r x
-> Variant2 'Contravariant (IsoHomDisj r o (HomEmpty r)) x (o x)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj

--------------------------------------------------------------------------------

-- toDualO' -


-- | the contravariant to-dual @__o__@ isomorphism.

toDualO' :: TransformableGRefl o r
  => q o -> Struct r x -> Variant2 Contravariant (IsoO r o) x (o x)
toDualO' :: forall (o :: * -> *) r (q :: (* -> *) -> *) x.
TransformableGRefl o r =>
q o -> Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO' q o
_ = Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO

--------------------------------------------------------------------------------

-- ReflO -


-- | the type for covariant reflections.

type ReflO r o x = Variant2 Covariant (IsoO r o) x (o (o x))

--------------------------------------------------------------------------------

-- reflO -


-- | the covariant reflection.

reflO ::
  TransformableGRefl o r
  => Struct r x -> Variant2 Covariant (IsoO r o) x (o (o x))
reflO :: forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Covariant (IsoO r o) x (o (o x))
reflO Struct r x
r = IsoO r o x (o (o x)) -> Variant2 'Covariant (IsoO r o) x (o (o x))
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (IsoO r o (o x) (o (o x))
t' IsoO r o (o x) (o (o x))
-> IsoO r o x (o x) -> IsoO r o x (o (o x))
forall y z x. IsoO r o y z -> IsoO r o x y -> IsoO r o x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. IsoO r o x (o x)
t) where
  Contravariant2 IsoO r o x (o x)
t  = Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct r x
r
  Contravariant2 IsoO r o (o x) (o (o x))
t' = Struct r (o x)
-> Variant2 'Contravariant (IsoO r o) (o x) (o (o x))
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct r x -> Struct r (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct r x
r)

--------------------------------------------------------------------------------

-- HomId -


-- | isomorphisms for mappings between @__x__@ and @'Id' __x__@ and vice versa.

data HomId s x y where
  ToId   :: (Structure s x, Structure s (Id x)) => HomId s x (Id x)
  FromId :: (Structure s x, Structure s (Id x)) => HomId s (Id x) x

deriving instance Show (HomId s x y)
instance Show2 (HomId s)

instance Morphism (HomId s) where
  type ObjectClass (HomId s) = s
  homomorphous :: forall x y. HomId s x y -> Homomorphous (ObjectClass (HomId s)) x y
homomorphous HomId s x y
ToId = Struct s x
forall s x. Structure s x => Struct s x
Struct Struct s x -> Struct s y -> Homomorphous s x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y
forall s x. Structure s x => Struct s x
Struct
  homomorphous HomId s x y
FromId = Struct s x
forall s x. Structure s x => Struct s x
Struct Struct s x -> Struct s y -> Homomorphous s x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y
forall s x. Structure s x => Struct s x
Struct

instance ApplicativeG Id (HomId s) (->) where
  amapG :: forall x y. HomId s x y -> Id x -> Id y
amapG HomId s x y
ToId Id x
x = y -> Id y
forall x. x -> Id x
Id y
Id x
x
  amapG HomId s x y
FromId (Id x
x) = x
Id y
x

instance ApplicativeG Pnt (HomId s) (->) where
  amapG :: forall x y. HomId s x y -> Pnt x -> Pnt y
amapG HomId s x y
ToId (Pnt Point x
p)   = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt Point x
Point y
p
  amapG HomId s x y
FromId (Pnt Point x
p) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt Point x
Point y
p
  
--------------------------------------------------------------------------------

-- Hom -


-- | homomorphisms parameterized over @__s__@.

type family Hom s (h :: Type -> Type -> Type) :: Constraint

--------------------------------------------------------------------------------

-- HomD -


-- | disjunctive homomorphisms parameterized over @__s__@.

type family HomD s (h :: Type -> Type -> Type) :: Constraint

--------------------------------------------------------------------------------

-- xscmHomDisj -


-- | random variable for some composable 'HomDisj'.

xscmHomDisj :: (TransformableG o s s, Morphism h, Transformable (ObjectClass h) s)
  => X (SomeObjectClass (SHom s s o h)) -> X (SomeMorphism h) -> X (SomeCmpb2 (HomDisj s o h))
xscmHomDisj :: forall (o :: * -> *) s (h :: * -> * -> *).
(TransformableG o s s, Morphism h,
 Transformable (ObjectClass h) s) =>
X (SomeObjectClass (SHom s s o h))
-> X (SomeMorphism h) -> X (SomeCmpb2 (HomDisj s o h))
xscmHomDisj X (SomeObjectClass (SHom s s o h))
xo = (SomeCmpb2 (SHom s s o h) -> SomeCmpb2 (HomDisj s o h))
-> X (SomeCmpb2 (SHom s s o h)) -> X (SomeCmpb2 (HomDisj s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(SomeCmpb2 SHom s s o h y z
f SHom s s o h x y
g) -> HomDisj s o h y z -> HomDisj s o h x y -> SomeCmpb2 (HomDisj s o h)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 (SHom s s o h y z -> HomDisj s o h y z
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj SHom s s o h y z
f) (SHom s s o h x y -> HomDisj s o h x y
forall s (o :: * -> *) (h :: * -> * -> *) x y.
SHom s s o h x y -> HomDisj s o h x y
HomDisj SHom s s o h x y
g)) (X (SomeCmpb2 (SHom s s o h)) -> X (SomeCmpb2 (HomDisj s o h)))
-> (X (SomeMorphism h) -> X (SomeCmpb2 (SHom s s o h)))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (HomDisj s o h))
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. N
-> X (SomeObjectClass (SHom s s o h))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (SHom s s o h))
forall (h :: * -> * -> *) s (o :: * -> *) r.
(Morphism h, Transformable (ObjectClass h) s,
 Transformable1 o s) =>
N
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (SHom r s o h))
xSctSomeCmpb2 N
10 X (SomeObjectClass (SHom s s o h))
xo