{-# LANGUAGE NoImplicitPrelude #-}

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


-- |

-- Module      : OAlg.Hom.FibredOriented

-- Description : definition of homomorphisms between fibred oriented structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- definition of homomorphisms between 'FibredOriented' structures.

module OAlg.Hom.FibredOriented
  ( -- * Disjunctive

    HomFibredOrientedDisjunctive, DualisableFibredOriented

    -- * Covariant

  , HomFibredOriented

    -- * Iso

  , toDualOpFbrOrt

    -- * Proposition

  , prpHomFbrOrt, prpHomFbrOrtDisj
  , prpDualisableFibredOrientedStk, prpDualisableFibredOrientedRt
  , prpHomDisjOpFbrOrt
  )
  where

import OAlg.Prelude

import OAlg.Category.Dualisable
import OAlg.Category.Unify
import OAlg.Category.Path

import OAlg.Structure.Oriented hiding (Path(..))
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented

import OAlg.Hom.Definition
import OAlg.Hom.Fibred
import OAlg.Hom.Oriented


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

-- HomFibredOriented -


-- | type family of homomorphisms between 'FibredOriented' structures where 'rmap' is given by

-- 'omap'.

--

-- __Property__ Let @'HomFibredOriented' __h__@, then for all @__x__@, @__y__@ and

-- @h@ in @__h x y__@ holds:

--

-- (1) @'rmap' h '.=.' 'omap' h@.

class (HomFibred h, HomOriented h, Transformable (ObjectClass h) FbrOrt)
  => HomFibredOriented h

instance HomFibredOriented h => HomFibredOriented (Path h)
instance (TransformableOrt s, TransformableFbr s, TransformableFbrOrt s)
  => HomFibredOriented (HomEmpty s)

instance HomFibredOriented h => HomFibredOriented (Inv2 h)

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

-- HomFibredOrientedDisjunctive -


-- | type family of homomorphisms between 'FibredOriented' structures where 'rmap' is given by

-- 'omapDisj'.

--

-- __Property__ Let @'HomFibredOrientedDisjunctive' __h__@, then for all @__x__@, @__y__@ and

-- @h@ in @__h x y__@ holds:

--

-- (1) @'rmap' h '.=.' 'omapDisj' h@.

class (HomFibred h, HomOrientedDisjunctive h, Transformable (ObjectClass h) FbrOrt)
  => HomFibredOrientedDisjunctive h

instance HomFibredOrientedDisjunctive h => HomFibredOrientedDisjunctive (Path h)

instance HomFibredOrientedDisjunctive h => HomFibredOriented (Variant2 Covariant h)

instance
  ( CategoryDisjunctive h
  , HomFibredOrientedDisjunctive h
  )
  => HomFibredOrientedDisjunctive (Inv2 h)

instance (TransformableFbrOrt s, HomFibredOrientedDisjunctive h)
  => HomFibredOrientedDisjunctive (Sub s h)
  
--------------------------------------------------------------------------------

-- DualisableFibredOriented -


-- | duality according to @__o__@ on 'FibredOriented'-structures.

--

-- __Property__ Let @'DualisableFibredOriented' __s o__@ then for all @__x__@ and

-- @s@ in @'Struct' __s x__@ holds:

--

-- (1) @'toDualStk' q s '.=.' 'toDualArw' q s@.

--

-- (2) @'toDualRt' q s '.=.' 'toDualOrt' q s@.

class ( DualisableFibred s o, DualisableOriented s o
      , Transformable s FbrOrt
      ) => DualisableFibredOriented s o

instance (TransformableType s, TransformableOrt s, TransformableFbrOrt s, TransformableOp s)
  => DualisableFibredOriented s Op

instance (HomFibredOriented h, DualisableFibredOriented s o)
  => HomFibredOrientedDisjunctive (HomDisj s o h)

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

-- toDualOpFbrOrt -


-- | the canonical 'Contravariant' isomorphism on 'FibredOriented' structures

-- between @__x__@ and @'Op' __x__@.

toDualOpFbrOrt :: FibredOriented x => Variant2 Contravariant (IsoO FbrOrt Op) x (Op x)
toDualOpFbrOrt :: forall x.
FibredOriented x =>
Variant2 'Contravariant (IsoO FbrOrt Op) x (Op x)
toDualOpFbrOrt = Struct FbrOrt x
-> Variant2 'Contravariant (IsoO FbrOrt Op) x (Op x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct FbrOrt x
forall s x. Structure s x => Struct s x
Struct

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

-- prpHomFbrOrt -


relHomFbrOrtStruct :: (HomFibredOriented h, Show2 h)
  => Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
relHomFbrOrtStruct :: forall (h :: * -> * -> *) x y.
(HomFibredOriented h, Show2 h) =>
Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
relHomFbrOrtStruct (Struct FbrOrt x
Struct :>: Struct FbrOrt y
Struct) h x y
h Root x
r
  = (h x y -> Root x -> Root y
forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h x y
h Root x
r Orientation (Point y) -> Orientation (Point y) -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Orientation (Point x) -> Orientation (Point y)
forall (h :: * -> * -> *) a b.
ApplicativePoint h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap h x y
h Orientation (Point x)
Root x
r) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:=h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h,String
"r"String -> String -> Parameter
:=Orientation (Point x) -> String
forall a. Show a => a -> String
show Orientation (Point x)
Root x
r]

-- | validity accordint to 'HomFibredOriented'.

prpHomFbrOrt :: (HomFibredOriented h, Show2 h)
  => h x y -> Root x -> Statement
prpHomFbrOrt :: forall (h :: * -> * -> *) x y.
(HomFibredOriented h, Show2 h) =>
h x y -> Root x -> Statement
prpHomFbrOrt h x y
h Root x
r = String -> Label
Prp String
"HomFbrOrt"
  Label -> Statement -> Statement
:<=>: Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
forall (h :: * -> * -> *) x y.
(HomFibredOriented h, Show2 h) =>
Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
relHomFbrOrtStruct (Homomorphous (ObjectClass h) x y -> Homomorphous FbrOrt x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h)) h x y
h Root x
r

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

-- prpHomFbrOrtDisj -


relHomFbrOrtDisjHomomorphous :: (HomFibredOrientedDisjunctive h, Show2 h)
  => Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
relHomFbrOrtDisjHomomorphous :: forall (h :: * -> * -> *) x y.
(HomFibredOrientedDisjunctive h, Show2 h) =>
Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
relHomFbrOrtDisjHomomorphous (Struct FbrOrt x
Struct :>: Struct FbrOrt y
Struct) h x y
h Root x
r
  = (h x y -> Root x -> Root y
forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h x y
h Root x
r Orientation (Point y) -> Orientation (Point y) -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Orientation (Point x) -> Orientation (Point y)
forall (h :: * -> * -> *) x y.
(ApplicativePoint h, Disjunctive2 h) =>
h x y -> Orientation (Point x) -> Orientation (Point y)
omapDisj h x y
h Orientation (Point x)
Root x
r) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:=h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h,String
"r"String -> String -> Parameter
:=Orientation (Point x) -> String
forall a. Show a => a -> String
show Orientation (Point x)
Root x
r]


-- | validity according to 'HomFibredOrientedDisjunctive'.

prpHomFbrOrtDisj :: (HomFibredOrientedDisjunctive h, Show2 h) => h a b -> Root a -> Statement
prpHomFbrOrtDisj :: forall (h :: * -> * -> *) a b.
(HomFibredOrientedDisjunctive h, Show2 h) =>
h a b -> Root a -> Statement
prpHomFbrOrtDisj h a b
f Root a
r = String -> Label
Prp String
"HomFbrOrtDisj"
  Label -> Statement -> Statement
:<=>: Homomorphous FbrOrt a b -> h a b -> Root a -> Statement
forall (h :: * -> * -> *) x y.
(HomFibredOrientedDisjunctive h, Show2 h) =>
Homomorphous FbrOrt x y -> h x y -> Root x -> Statement
relHomFbrOrtDisjHomomorphous (Homomorphous (ObjectClass h) a b -> Homomorphous FbrOrt a b
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h a b -> Homomorphous (ObjectClass h) a b
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h a b
f)) h a b
f Root a
r

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

-- prpDualisableFibredOrientedRt -


relDualisableFibredOrientedRt :: DualisableFibredOriented s o
  => q o -> Struct s x -> Struct FbrOrt x -> Struct FbrOrt (o x) -> Root x -> Statement
relDualisableFibredOrientedRt :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibredOriented s o =>
q o
-> Struct s x
-> Struct FbrOrt x
-> Struct FbrOrt (o x)
-> Root x
-> Statement
relDualisableFibredOrientedRt q o
q Struct s x
s Struct FbrOrt x
Struct Struct FbrOrt (o x)
Struct Root x
r
  = (q o -> Struct s x -> Root x -> Root (o x)
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> Root x -> Root (o x)
toDualRt q o
q Struct s x
s Root x
r Orientation (Point (o x)) -> Orientation (Point (o x)) -> Bool
forall a. Eq a => a -> a -> Bool
== q o
-> Struct s x -> Orientation (Point x) -> Orientation (Point (o x))
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o
-> Struct s x -> Orientation (Point x) -> Orientation (Point (o x))
toDualOrt q o
q Struct s x
s Orientation (Point x)
Root x
r) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"r"String -> String -> Parameter
:=Orientation (Point x) -> String
forall a. Show a => a -> String
show Orientation (Point x)
Root x
r]

-- | validity according to 'DualisableFibredOriented'.

prpDualisableFibredOrientedRt :: DualisableFibredOriented s o
  => q o -> Struct s x -> Root x -> Statement
prpDualisableFibredOrientedRt :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibredOriented s o =>
q o -> Struct s x -> Root x -> Statement
prpDualisableFibredOrientedRt q o
q Struct s x
s Root x
r = String -> Label
Prp String
"DualisableFibredOrientedRt" Label -> Statement -> Statement
:<=>:
  q o
-> Struct s x
-> Struct FbrOrt x
-> Struct FbrOrt (o x)
-> Root x
-> Statement
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibredOriented s o =>
q o
-> Struct s x
-> Struct FbrOrt x
-> Struct FbrOrt (o x)
-> Root x
-> Statement
relDualisableFibredOrientedRt q o
q Struct s x
s (Struct s x -> Struct FbrOrt x
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct FbrOrt (o x)
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s)) Root x
r

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

-- prpDualisableFibredOrientedStk -


relDualisableFibredOrientedStk :: DualisableFibredOriented s o
  => q o -> Struct s x -> Struct FbrOrt x -> Struct FbrOrt (o x) -> x -> Statement
relDualisableFibredOrientedStk :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibredOriented s o =>
q o
-> Struct s x
-> Struct FbrOrt x
-> Struct FbrOrt (o x)
-> x
-> Statement
relDualisableFibredOrientedStk q o
q Struct s x
s Struct FbrOrt x
Struct Struct FbrOrt (o x)
Struct x
x
  = (q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s x
x o x -> o x -> Bool
forall a. Eq a => a -> a -> Bool
== q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> x -> o x
toDualArw q o
q Struct s x
s x
x) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]

-- | validity according to 'DualisableFibredOriented'.

prpDualisableFibredOrientedStk :: DualisableFibredOriented s o
  => q o -> Struct s x -> x -> Statement
prpDualisableFibredOrientedStk :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibredOriented s o =>
q o -> Struct s x -> x -> Statement
prpDualisableFibredOrientedStk q o
q Struct s x
s x
x = String -> Label
Prp String
"DualisableFibredOriented" Label -> Statement -> Statement
:<=>:
  q o
-> Struct s x
-> Struct FbrOrt x
-> Struct FbrOrt (o x)
-> x
-> Statement
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibredOriented s o =>
q o
-> Struct s x
-> Struct FbrOrt x
-> Struct FbrOrt (o x)
-> x
-> Statement
relDualisableFibredOrientedStk q o
q Struct s x
s (Struct s x -> Struct FbrOrt x
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct FbrOrt (o x)
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s)) x
x

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

-- prpHomDisjOpFbrOrt -


relHomFbrOrtDisjFbrOrtX :: (HomFibredOrientedDisjunctive h, Show2 h)
  => Homomorphous FbrOrtX x y -> h x y -> Statement
relHomFbrOrtDisjFbrOrtX :: forall (h :: * -> * -> *) x y.
(HomFibredOrientedDisjunctive h, Show2 h) =>
Homomorphous FbrOrtX x y -> h x y -> Statement
relHomFbrOrtDisjFbrOrtX (Struct FbrOrtX x
Struct :>: Struct FbrOrtX y
Struct) h x y
h
  = X (Orientation (Point x))
-> (Orientation (Point x) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Orientation (Point x))
forall x. XStandard x => X x
xStandard (h x y -> Root x -> Statement
forall (h :: * -> * -> *) a b.
(HomFibredOrientedDisjunctive h, Show2 h) =>
h a b -> Root a -> Statement
prpHomFbrOrtDisj h x y
h)

relHomDisjOpFbrOrt :: X (SomeMorphism (HomDisjEmpty FbrOrtX Op)) -> Statement
relHomDisjOpFbrOrt :: X (SomeMorphism (HomDisjEmpty FbrOrtX Op)) -> Statement
relHomDisjOpFbrOrt X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
xsh = X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
-> (SomeMorphism (HomDisjEmpty FbrOrtX Op) -> Statement)
-> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
xsh
  (\(SomeMorphism HomDisjEmpty FbrOrtX Op x y
h) -> Homomorphous FbrOrtX x y
-> HomDisjEmpty FbrOrtX Op x y -> Statement
forall (h :: * -> * -> *) x y.
(HomFibredOrientedDisjunctive h, Show2 h) =>
Homomorphous FbrOrtX x y -> h x y -> Statement
relHomFbrOrtDisjFbrOrtX (Homomorphous FbrOrtX x y -> Homomorphous FbrOrtX x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (HomDisjEmpty FbrOrtX Op x y
-> Homomorphous (ObjectClass (HomDisjEmpty FbrOrtX Op)) x y
forall x y.
HomDisj FbrOrtX Op (HomEmpty FbrOrtX) x y
-> Homomorphous (ObjectClass (HomDisjEmpty FbrOrtX Op)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous HomDisjEmpty FbrOrtX Op x y
h)) HomDisjEmpty FbrOrtX Op x y
h)

-- | validity of @'HomDisjEmpty' __FbrOrt Op__@ according to 'HomFibredOrientedDisjunctive'.

prpHomDisjOpFbrOrt :: Statement
prpHomDisjOpFbrOrt :: Statement
prpHomDisjOpFbrOrt = String -> Label
Prp String
"HomDisjOpFbrOrt" Label -> Statement -> Statement
:<=>: X (SomeMorphism (HomDisjEmpty FbrOrtX Op)) -> Statement
relHomDisjOpFbrOrt X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
xsh where
  xsh :: X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
  xsh :: X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
xsh = (SomeCmpb2 (HomDisjEmpty FbrOrtX Op)
 -> SomeMorphism (HomDisjEmpty FbrOrtX Op))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
-> X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomDisjEmpty FbrOrtX Op)
-> SomeMorphism (HomDisjEmpty FbrOrtX Op)
forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
 -> X (SomeMorphism (HomDisjEmpty FbrOrtX Op)))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
-> X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom FbrOrtX FbrOrtX Op (HomEmpty FbrOrtX)))
-> X (SomeMorphism (HomEmpty FbrOrtX))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
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 FbrOrtX FbrOrtX Op (HomEmpty FbrOrtX)))
forall s.
(s ~ FbrOrtX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoFbrOrtX X (SomeMorphism (HomEmpty FbrOrtX))
forall x. X x
XEmpty

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

-- dstFbrOrtX -


xfgFbrOrtX :: X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
xfgFbrOrtX :: X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
xfgFbrOrtX = X (SomeObjectClass (SHom FbrOrtX FbrOrtX Op (HomEmpty FbrOrtX)))
-> X (SomeMorphism (HomEmpty FbrOrtX))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
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 FbrOrtX FbrOrtX Op (HomEmpty FbrOrtX)))
forall s.
(s ~ FbrOrtX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoFbrOrtX X (SomeMorphism (HomEmpty FbrOrtX))
forall x. X x
XEmpty

dstFbrOrtX :: Int -> IO ()
dstFbrOrtX :: Int -> IO ()
dstFbrOrtX Int
n = (SomeCmpb2 (HomDisjEmpty FbrOrtX Op) -> [String])
-> Int -> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op)) -> IO ()
forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr SomeCmpb2 (HomDisjEmpty FbrOrtX Op) -> [String]
forall {c :: * -> * -> *}.
(Disjunctive2 c, Category c) =>
SomeCmpb2 c -> [String]
asp Int
n X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
xfgFbrOrtX where
  asp :: SomeCmpb2 c -> [String]
asp (SomeCmpb2 c y z
f c x y
g) = [ Variant -> String
forall a. Show a => a -> String
show (Variant -> String) -> Variant -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c x z -> Variant
forall x y. c x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
Disjunctive2 h =>
h x y -> Variant
variant2 (c y z
f c y z -> c x y -> c x z
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
g)
                        , Variant -> String
forall a. Show a => a -> String
show (Variant -> String) -> Variant -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c y z -> Variant
forall x y. c x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
Disjunctive2 h =>
h x y -> Variant
variant2 c y z
f
                        , Variant -> String
forall a. Show a => a -> String
show (Variant -> String) -> Variant -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c x y -> Variant
forall x y. c x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
Disjunctive2 h =>
h x y -> Variant
variant2 c x y
g
                        ]