proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Bicategory.Op

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 :: k -> k -> 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 {k1 :: k} (i :: k) (j :: k) (a :: OPK kk i j) (b :: OPK kk i j) (c :: OPK kk j k1) (d :: OPK kk j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: k) (j :: k) (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 :: k) (j :: k) (a :: OPK kk i j). Obj a -> O (I :: OPK kk i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> a ~> O (I :: OPK kk i i) a Source Comments #

rightUnitor :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> O a (I :: OPK kk j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: k) (j :: k) (a :: OPK kk i j). Obj a -> a ~> O a (I :: OPK kk j j) Source Comments #

associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: OPK kk i j2) (b :: OPK kk j2 j1) (c :: OPK kk j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: OPK kk i j2) (b :: OPK kk j2 j1) (c :: OPK kk j1 k1). Obj a -> Obj b -> Obj 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 ('OP j2) (Lan ('OP j2) ('OP f)) Source Comments #

lanUniv :: forall (g :: OPK kk d e). Ob g => ('OP f ~> O ('OP j2) g) -> 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 (Lift ('OP j) ('OP f)) ('OP j) Source Comments #

liftUniv :: forall (g :: OPK kk e d). Ob g => ('OP f ~> O g ('OP j)) -> 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 ('OP j2) (Ran ('OP j2) ('OP f)) ~> 'OP f Source Comments #

ranUniv :: forall (g :: OPK kk d e). Ob g => (O ('OP j2) g ~> '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 (Rift ('OP j) ('OP f)) ('OP j) ~> 'OP f Source Comments #

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

Double hk vk => Double (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Double

Associated Types

data Sq (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) 
Instance details

Defined in Proarrow.Category.Double

data Sq (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) where
data Sq1 (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1) 
Instance details

Defined in Proarrow.Category.Double

data Sq1 (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1) where
  • CoSq1 :: forall {k} {h :: k} {j :: k} {i :: k} {k1 :: k} (hk :: CAT k) (vk :: CAT k) (p :: OPK hk h j) (q :: OPK hk i k1) (g :: COK vk j k1) (f :: COK vk h i). Sq1 hk vk (UN ('OP :: hk j h -> OPK hk h j) p) (UN ('OP :: hk k1 i -> OPK hk i k1) q) (UN ('CO :: vk j k1 -> COK vk j k1) g) (UN ('CO :: vk h i -> COK vk h i) f) -> Sq1 (OPK hk) (COK vk) p q f g

Methods

singleton :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1). (DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i, DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1, Ob p, Ob q, Ob f, Ob g) => Sq1 (OPK hk) (COK vk) p q f g -> Sq (OPK hk) (COK vk) (p '::: ('Nil :: Path (OPK hk) j j)) (q '::: ('Nil :: Path (OPK hk) k1 k1)) (f '::: ('Nil :: Path (COK vk) i i)) (g '::: ('Nil :: Path (COK vk) k1 k1)) Source Comments #

folded :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1). (DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i, DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1, Ob ps, Ob qs, Ob fs, Ob gs) => Sq (OPK hk) (COK vk) ps qs fs gs -> Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs) Source Comments #

object :: forall (k1 :: k). DOb (OPK hk) (COK vk) k1 => Sq (OPK hk) (COK vk) ('Nil :: Path (OPK hk) k1 k1) ('Nil :: Path (OPK hk) k1 k1) ('Nil :: Path (COK vk) k1 k1) ('Nil :: Path (COK vk) k1 k1) Source Comments #

hArr :: forall (j :: k) (k1 :: k) (ps :: Path (OPK hk) j k1) (qs :: Path (OPK hk) j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (ps ~> qs) -> Sq (OPK hk) (COK vk) ps qs ('Nil :: Path (COK vk) j j) ('Nil :: Path (COK vk) k1 k1) Source Comments #

hArr1 :: forall (j :: k) (k1 :: k) (p :: OPK hk j k1) (q :: OPK hk j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (p ~> q) -> Sq1 (OPK hk) (COK vk) p q (I :: COK vk j j) (I :: COK vk k1 k1) Source Comments #

(|||) :: forall {a1 :: k} {a2 :: k} {b1 :: k} {b2 :: k} {c1 :: k} {c2 :: k} (ps :: Path (OPK hk) a1 a2) (qs :: Path (OPK hk) b1 b2) (fs :: Path (COK vk) a1 b1) (gs :: Path (COK vk) a2 b2) (rs :: Path (OPK hk) c1 c2) (hs :: Path (COK vk) b1 c1) (is :: Path (COK vk) b2 c2). Sq (OPK hk) (COK vk) ps qs fs gs -> Sq (OPK hk) (COK vk) qs rs hs is -> Sq (OPK hk) (COK vk) ps rs (fs +++ hs) (gs +++ is) Source Comments #

vArr :: forall (j :: k) (k1 :: k) (fs :: Path (COK vk) j k1) (gs :: Path (COK vk) j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (fs ~> gs) -> Sq (OPK hk) (COK vk) ('Nil :: Path (OPK hk) j j) ('Nil :: Path (OPK hk) k1 k1) fs gs Source Comments #

vArr1 :: forall (j :: k) (k1 :: k) (f :: COK vk j k1) (g :: COK vk j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (f ~> g) -> Sq1 (OPK hk) (COK vk) (I :: OPK hk j j) (I :: OPK hk k1 k1) f g Source Comments #

(===) :: forall {h :: k} {b1 :: k} {i :: k} {b2 :: k} {j :: k} {k1 :: k} (ps :: Path (OPK hk) h b1) (qs :: Path (OPK hk) i b2) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) b1 b2) (rs :: Path (OPK hk) b1 j) (ss :: Path (OPK hk) b2 k1) (hs :: Path (COK vk) j k1). Sq (OPK hk) (COK vk) ps qs fs gs -> Sq (OPK hk) (COK vk) rs ss gs hs -> Sq (OPK hk) (COK vk) (ps +++ rs) (qs +++ ss) fs hs Source Comments #

(\\\\) :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) r. ((DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i, DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1, Ob ps, Ob qs, Ob fs, Ob gs) => r) -> Sq (OPK hk) (COK vk) ps qs fs gs -> r 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 :: k2 -> k2 -> Type) (k3 :: k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Op

type Ob0 (OPK kk :: k2 -> k2 -> Type) (k3 :: k1) = Ob0 kk k3
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 j k2) (b :: OPK kk k2 k3) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Op

type O (a :: OPK kk j k2) (b :: OPK kk k2 k3) = 'OP (O (UN ('OP :: kk k3 k2 -> OPK kk k2 k3) b) (UN ('OP :: kk k2 j -> OPK kk j k2) a))
data Sq (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Double

data Sq (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) where
data Sq1 (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Double

data Sq1 (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1) where
  • CoSq1 :: forall {k} {h :: k} {j :: k} {i :: k} {k1 :: k} (hk :: CAT k) (vk :: CAT k) (p :: OPK hk h j) (q :: OPK hk i k1) (g :: COK vk j k1) (f :: COK vk h i). Sq1 hk vk (UN ('OP :: hk j h -> OPK hk h j) p) (UN ('OP :: hk k1 i -> OPK hk i k1) q) (UN ('CO :: vk j k1 -> COK vk j k1) g) (UN ('CO :: vk h i -> COK vk h i) f) -> Sq1 (OPK hk) (COK vk) p q f g
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 #