Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Op

Contents

Orphan instances

Documentation

newtype OPK (kk :: CAT k) (j :: k) (k1 :: k) Source Comments #

Constructors

OP (kk k1 j)

Instances

Instances details

Bicategory kk => Bicategory (OPK kk :: s -> s -> Type) Source Comments #

Create a dual of a bicategory by reversing the 1-cells.

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

iObj :: forall (i :: s). Ob0 (OPK kk) i => Obj (I :: OPK kk i i) Source Comments #

o :: forall {i :: s} (j :: s) (k :: s) (a :: OPK kk j k) (b :: OPK kk j k) (c :: OPK kk i j) (d :: OPK kk i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: s) (j :: s) (ps :: OPK kk i j) (qs :: OPK kk i j) r. ((Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall {i :: s} {j :: s} (a :: OPK kk i j). (Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) => O (I :: OPK kk j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: s} {j :: s} (a :: OPK kk i j). (Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) => a ~> O (I :: OPK kk j j) a Source Comments #

rightUnitor :: forall {i :: s} {j :: s} (a :: OPK kk i j). (Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) => O a (I :: OPK kk i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: s} {j :: s} (a :: OPK kk i j). (Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob a) => a ~> O a (I :: OPK kk i i) Source Comments #

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: OPK kk j k) (b :: OPK kk i j) (c :: OPK kk h i). (Ob0 (OPK kk) h, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: OPK kk j k) (b :: OPK kk i j) (c :: OPK kk h i). (Ob0 (OPK kk) h, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

LeftKanLift j2 f => LeftKanExtension ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Op type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) = 'OP (Lift j2 f)

Methods

lan :: 'OP f ~> O (Lan ('OP j2) ('OP f)) ('OP j2) Source Comments #

lanUniv :: forall (g :: OPK kk d e). Ob g => ('OP f ~> O g ('OP j2)) -> Lan ('OP j2) ('OP f) ~> g Source Comments #

LeftKanExtension j f => LeftKanLift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Op type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) = 'OP (Lan j f)

Methods

lift :: 'OP f ~> O ('OP j) (Lift ('OP j) ('OP f)) Source Comments #

liftUniv :: forall (g :: OPK kk e d). Ob g => ('OP f ~> O ('OP j) g) -> Lift ('OP j) ('OP f) ~> g Source Comments #

RightKanLift j2 f => RightKanExtension ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e)
Instance details Defined in Proarrow.Category.Bicategory.Op type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) = 'OP (Rift j2 f)

Methods

ran :: O (Ran ('OP j2) ('OP f)) ('OP j2) ~> 'OP f Source Comments #

ranUniv :: forall (g :: OPK kk d e). Ob g => (O g ('OP j2) ~> 'OP f) -> g ~> Ran ('OP j2) ('OP f) Source Comments #

RightKanExtension j f => RightKanLift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2)
Instance details Defined in Proarrow.Category.Bicategory.Op type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) = 'OP (Ran j f)

Methods

rift :: O ('OP j) (Rift ('OP j) ('OP f)) ~> 'OP f Source Comments #

riftUniv :: forall (g :: OPK kk e d). Ob g => (O ('OP j) g ~> 'OP f) -> g ~> Rift ('OP j) ('OP f) Source Comments #

Adjunction f g => Adjunction ('OP g :: OPK kk k2 j) ('OP f :: OPK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

unit :: (I :: OPK kk k2 k2) ~> O ('OP f) ('OP g) Source Comments #

counit :: O ('OP g) ('OP f) ~> (I :: OPK kk j j) Source Comments #

Bimodule s t p => Bimodule ('OP t :: OPK kk k2 k2) ('OP s :: OPK kk j j) ('OP p :: OPK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

leftAction :: O ('OP t) ('OP p) ~> 'OP p Source Comments #

rightAction :: O ('OP p) ('OP s) ~> 'OP p Source Comments #

Comonad t => Comonad ('OP t :: OPK kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

epsilon :: 'OP t ~> (I :: OPK kk a a) Source Comments #

delta :: 'OP t ~> O ('OP t) ('OP t) Source Comments #

Monad t => Monad ('OP t :: OPK kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

eta :: (I :: OPK kk a a) ~> 'OP t Source Comments #

mu :: O ('OP t) ('OP t) ~> 'OP t Source Comments #

Equipment hk vk => Equipment (COK hk :: k -> k -> Type) (OPK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapConjoint :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk j k0). (f ~> g) -> Conjoint (COK hk) g ~> Conjoint (COK hk) f Source Comments #

conjToId :: forall (k0 :: k). Ob0 (OPK vk) k0 => Conjoint (COK hk) (I :: OPK vk k k) ~> (I :: COK hk k k) Source Comments #

conjFromId :: forall (k0 :: k). Ob0 (OPK vk) k0 => (I :: COK hk k k) ~> Conjoint (COK hk) (I :: OPK vk k k) Source Comments #

conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: OPK vk j k2) (g :: OPK vk k1 j). Obj f -> Obj g -> Conjoint (COK hk) (O f g) ~> O (Conjoint (COK hk) g) (Conjoint (COK hk) f) Source Comments #

conjFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: OPK vk j2 k0) (g :: OPK vk j1 j2). Obj f -> Obj g -> O (Conjoint (COK hk) g) (Conjoint (COK hk) f) ~> Conjoint (COK hk) (O f g) Source Comments #

comConUnit :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0). Obj f -> (I :: COK hk j j) ~> O (Conjoint (COK hk) f) (Companion (COK hk) f) Source Comments #

comConCounit :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0). Obj f -> O (Companion (COK hk) f) (Conjoint (COK hk) f) ~> (I :: COK hk k k) Source Comments #

Equipment hk vk => Equipment (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapConjoint :: forall {j :: k} {k0 :: k} (f :: COK vk j k0) (g :: COK vk j k0). (f ~> g) -> Conjoint (OPK hk) g ~> Conjoint (OPK hk) f Source Comments #

conjToId :: forall (k0 :: k). Ob0 (COK vk) k0 => Conjoint (OPK hk) (I :: COK vk k k) ~> (I :: OPK hk k k) Source Comments #

conjFromId :: forall (k0 :: k). Ob0 (COK vk) k0 => (I :: OPK hk k k) ~> Conjoint (OPK hk) (I :: COK vk k k) Source Comments #

conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: COK vk j k2) (g :: COK vk k1 j). Obj f -> Obj g -> Conjoint (OPK hk) (O f g) ~> O (Conjoint (OPK hk) g) (Conjoint (OPK hk) f) Source Comments #

conjFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: COK vk j2 k0) (g :: COK vk j1 j2). Obj f -> Obj g -> O (Conjoint (OPK hk) g) (Conjoint (OPK hk) f) ~> Conjoint (OPK hk) (O f g) Source Comments #

comConUnit :: forall {j :: k} {k0 :: k} (f :: COK vk j k0). Obj f -> (I :: OPK hk j j) ~> O (Conjoint (OPK hk) f) (Companion (OPK hk) f) Source Comments #

comConCounit :: forall {j :: k} {k0 :: k} (f :: COK vk j k0). Obj f -> O (Companion (OPK hk) f) (Conjoint (OPK hk) f) ~> (I :: OPK hk k k) Source Comments #

Equipment hk vk => HasCompanions (COK hk :: k -> k -> Type) (OPK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapCompanion :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk j k0). (f ~> g) -> Companion (COK hk) f ~> Companion (COK hk) g Source Comments #

compToId :: forall (k0 :: k). Ob0 (OPK vk) k0 => Companion (COK hk) (I :: OPK vk k k) ~> (I :: COK hk k k) Source Comments #

compFromId :: forall (k0 :: k). Ob0 (OPK vk) k0 => (I :: COK hk k k) ~> Companion (COK hk) (I :: OPK vk k k) Source Comments #

compToCompose :: forall {i :: k} {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk i j). Obj f -> Obj g -> Companion (COK hk) (O f g) ~> O (Companion (COK hk) f) (Companion (COK hk) g) Source Comments #

compFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: OPK vk j2 k0) (g :: OPK vk j1 j2). Obj f -> Obj g -> O (Companion (COK hk) f) (Companion (COK hk) g) ~> Companion (COK hk) (O f g) Source Comments #

Equipment hk vk => HasCompanions (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

mapCompanion :: forall {j :: k} {k0 :: k} (f :: COK vk j k0) (g :: COK vk j k0). (f ~> g) -> Companion (OPK hk) f ~> Companion (OPK hk) g Source Comments #

compToId :: forall (k0 :: k). Ob0 (COK vk) k0 => Companion (OPK hk) (I :: COK vk k k) ~> (I :: OPK hk k k) Source Comments #

compFromId :: forall (k0 :: k). Ob0 (COK vk) k0 => (I :: OPK hk k k) ~> Companion (OPK hk) (I :: COK vk k k) Source Comments #

compToCompose :: forall {i :: k} {j :: k} {k0 :: k} (f :: COK vk j k0) (g :: COK vk i j). Obj f -> Obj g -> Companion (OPK hk) (O f g) ~> O (Companion (OPK hk) f) (Companion (OPK hk) g) Source Comments #

compFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: COK vk j2 k0) (g :: COK vk j1 j2). Obj f -> Obj g -> O (Companion (OPK hk) f) (Companion (OPK hk) g) ~> Companion (OPK hk) (O f g) Source Comments #

CategoryOf (kk k2 j) => CategoryOf (OPK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Op type (~>) = Op :: OPK kk j k2 -> OPK kk j k2 -> Type

CategoryOf (kk k2 j) => Promonad (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

id :: forall (a :: OPK kk j k2). Ob a => Op a a Source Comments #

(.) :: forall (b :: OPK kk j k2) (c :: OPK kk j k2) (a :: OPK kk j k2). Op b c -> Op a b -> Op a c Source Comments #

CategoryOf (kk k2 j) => Profunctor (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

dimap :: forall (c :: OPK kk j k2) (a :: OPK kk j k2) (b :: OPK kk j k2) (d :: OPK kk j k2). (c ~> a) -> (b ~> d) -> Op a b -> Op c d Source Comments #

(\\) :: forall (a :: OPK kk j k2) (b :: OPK kk j k2) r. ((Ob a, Ob b) => r) -> Op a b -> r Source Comments #

type Ob0 (OPK kk :: s -> s -> Type) (k2 :: k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Ob0 (OPK kk :: s -> s -> Type) (k2 :: k1) = Ob0 kk k2

type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) = 'OP (Lift j2 f)

type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) = 'OP (Lan j f)

type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) = 'OP (Rift j2 f)

type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) = 'OP (Ran j f)

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type I = 'OP (I :: kk i i)

type O (a :: OPK kk j1 k) (b :: OPK kk j2 j1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type O (a :: OPK kk j1 k) (b :: OPK kk j2 j1) = 'OP (O (UN ('OP :: kk j1 j2 -> OPK kk j2 j1) b) (UN ('OP :: kk k j1 -> OPK kk j1 k) a))

type Companion (COK hk :: k -> k -> Type) (f :: OPK vk j k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Companion (COK hk :: k -> k -> Type) (f :: OPK vk j k1) = 'CO (Conjoint hk (UN ('OP :: vk k1 j -> OPK vk j k1) f))

type Companion (OPK hk :: k1 -> k1 -> Type) (f :: COK vk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Companion (OPK hk :: k1 -> k1 -> Type) (f :: COK vk j k2) = 'OP (Conjoint hk (UN ('CO :: vk j k2 -> COK vk j k2) f))

type Conjoint (COK hk :: k -> k -> Type) (f :: OPK vk k1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Conjoint (COK hk :: k -> k -> Type) (f :: OPK vk k1 j) = 'CO (Companion hk (UN ('OP :: vk j k1 -> OPK vk k1 j) f))

type Conjoint (OPK hk :: k1 -> k1 -> Type) (f :: COK vk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Conjoint (OPK hk :: k1 -> k1 -> Type) (f :: COK vk k2 j) = 'OP (Companion hk (UN ('CO :: vk k2 j -> COK vk k2 j) f))

type UN ('OP :: kk k2 j -> OPK kk j k2) ('OP k3 :: OPK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type UN ('OP :: kk k2 j -> OPK kk j k2) ('OP k3 :: OPK kk j k2) = k3

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type (~>) = Op :: OPK kk j k2 -> OPK kk j k2 -> Type

type Ob (a :: OPK kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type Ob (a :: OPK kk j k2) = (Is ('OP :: kk k2 j -> OPK kk j k2) a, Ob (UN ('OP :: kk k2 j -> OPK kk j k2) a))

data Op (a :: OPK kk k1 j) (b :: OPK kk k1 j) where Source Comments #

Constructors

Op :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (a1 :: kk j k1) (b1 :: kk j k1). (a1 ~> b1) -> Op ('OP a1) ('OP b1)

Instances

Instances details

CategoryOf (kk k2 j) => Promonad (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods id :: forall (a :: OPK kk j k2). Ob a => Op a a Source Comments # (.) :: forall (b :: OPK kk j k2) (c :: OPK kk j k2) (a :: OPK kk j k2). Op b c -> Op a b -> Op a c Source Comments #
CategoryOf (kk k2 j) => Profunctor (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods dimap :: forall (c :: OPK kk j k2) (a :: OPK kk j k2) (b :: OPK kk j k2) (d :: OPK kk j k2). (c ~> a) -> (b ~> d) -> Op a b -> Op c d Source Comments # (\\) :: forall (a :: OPK kk j k2) (b :: OPK kk j k2) r. ((Ob a, Ob b) => r) -> Op a b -> r Source Comments #

flipSq :: forall {k1} {kk1 :: CAT k1} {k2 :: k1} {k3 :: k1} {kk2 :: CAT k1} {j :: k1} {h :: k1} (p :: kk1 k2 k3) (f :: kk2 j k3) (q :: kk1 h j) (g :: kk2 h k2). Sq '('CO p, 'OP f) '('CO q, 'OP g) -> Sq '('OP q, 'CO g) '('OP p, 'CO f) Source Comments #

flipRetroSq :: forall {k1} {kk1 :: CAT k1} {h :: k1} {j :: k1} {kk2 :: CAT k1} {k2 :: k1} {k3 :: k1} (p :: kk1 h j) (f :: kk2 h k2) (q :: kk1 k2 k3) (g :: kk2 j k3). RetroSq '('CO p, 'OP f) '('CO q, 'OP g) -> RetroSq '('OP q, 'CO g) '('OP p, 'CO f) Source Comments #

Orphan instances

Equipment hk vk => Equipment (COK hk :: k -> k -> Type) (OPK vk :: k -> k -> Type) Source Comments #
Instance details Methods mapConjoint :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk j k0). (f ~> g) -> Conjoint (COK hk) g ~> Conjoint (COK hk) f Source Comments # conjToId :: forall (k0 :: k). Ob0 (OPK vk) k0 => Conjoint (COK hk) (I :: OPK vk k k) ~> (I :: COK hk k k) Source Comments # conjFromId :: forall (k0 :: k). Ob0 (OPK vk) k0 => (I :: COK hk k k) ~> Conjoint (COK hk) (I :: OPK vk k k) Source Comments # conjToCompose :: forall {k1 :: k} {j :: k} {k2 :: k} (f :: OPK vk j k2) (g :: OPK vk k1 j). Obj f -> Obj g -> Conjoint (COK hk) (O f g) ~> O (Conjoint (COK hk) g) (Conjoint (COK hk) f) Source Comments # conjFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: OPK vk j2 k0) (g :: OPK vk j1 j2). Obj f -> Obj g -> O (Conjoint (COK hk) g) (Conjoint (COK hk) f) ~> Conjoint (COK hk) (O f g) Source Comments # comConUnit :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0). Obj f -> (I :: COK hk j j) ~> O (Conjoint (COK hk) f) (Companion (COK hk) f) Source Comments # comConCounit :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0). Obj f -> O (Companion (COK hk) f) (Conjoint (COK hk) f) ~> (I :: COK hk k k) Source Comments #
Equipment hk vk => HasCompanions (COK hk :: k -> k -> Type) (OPK vk :: k -> k -> Type) Source Comments #
Instance details Methods mapCompanion :: forall {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk j k0). (f ~> g) -> Companion (COK hk) f ~> Companion (COK hk) g Source Comments # compToId :: forall (k0 :: k). Ob0 (OPK vk) k0 => Companion (COK hk) (I :: OPK vk k k) ~> (I :: COK hk k k) Source Comments # compFromId :: forall (k0 :: k). Ob0 (OPK vk) k0 => (I :: COK hk k k) ~> Companion (COK hk) (I :: OPK vk k k) Source Comments # compToCompose :: forall {i :: k} {j :: k} {k0 :: k} (f :: OPK vk j k0) (g :: OPK vk i j). Obj f -> Obj g -> Companion (COK hk) (O f g) ~> O (Companion (COK hk) f) (Companion (COK hk) g) Source Comments # compFromCompose :: forall {j1 :: k} {j2 :: k} {k0 :: k} (f :: OPK vk j2 k0) (g :: OPK vk j1 j2). Obj f -> Obj g -> O (Companion (COK hk) f) (Companion (COK hk) g) ~> Companion (COK hk) (O f g) Source Comments #