Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.Op

Documentation

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

Constructors

OP (kk k1 j)

Instances

Instances details

WithObO2 Tight kk => WithObO2 Cotight (OPK kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: OPK kk j k) (b :: OPK kk i j) r. (Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) => ((IsOb Cotight (O a b), Ob (O a b)) => r) -> r Source Comments #

WithObO2 Cotight kk => WithObO2 Tight (OPK kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: OPK kk j k) (b :: OPK kk i j) r. (Ob a, Ob b, IsOb Tight a, IsOb Tight b) => ((IsOb Tight (O a b), Ob (O a b)) => r) -> r Source Comments #

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

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 #

withOb2 :: forall {i :: s} {j :: s} {k :: s} (a :: OPK kk j k) (b :: OPK kk i j) r. (Ob a, Ob b, Ob0 (OPK kk) i, Ob0 (OPK kk) j, Ob0 (OPK kk) k) => (Ob (O a b) => r) -> r Source Comments #

withOb0s :: forall {j :: s} {k :: s} (a :: OPK kk j k) r. Ob a => ((Ob0 (OPK kk) j, Ob0 (OPK kk) k) => r) -> r 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 #

Equipment kk => Equipment (OPK kk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

Methods

withCotightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r 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

adj :: Adj ('OP g) ('OP f) 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 #

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 IsOb Cotight (p :: OPK kk j i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type IsOb Cotight (p :: OPK kk j i) = IsOb Tight (UN ('OP :: kk i j -> OPK kk j i) p)

type IsOb Tight (p :: OPK kk j i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type IsOb Tight (p :: OPK kk j i) = IsOb Cotight (UN ('OP :: kk i j -> OPK kk j i) p)

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 CotightAdjoint (p :: OPK kk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type CotightAdjoint (p :: OPK kk k2 j) = 'OP (TightAdjoint (UN ('OP :: kk j k2 -> OPK kk k2 j) p))

type TightAdjoint (p :: OPK kk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Op

type TightAdjoint (p :: OPK kk k2 j) = 'OP (CotightAdjoint (UN ('OP :: kk j k2 -> OPK kk k2 j) p))

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 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 #