Safe Haskell | None |
---|---|
Language | Haskell2010 |
Proarrow.Category.Bicategory.Op
Documentation
newtype OPK (kk :: CAT k) (j :: k) (k1 :: k) Source Comments #
Constructors
OP (kk k1 j) |
Instances
Bicategory kk => Bicategory (OPK kk :: k -> k -> Type) Source Comments # | Create a dual of a bicategory by reversing the 1-cells. | ||||||||
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 # | |||||||||
LeftKanExtension j f => LeftKanLift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments # | |||||||||
RightKanLift j2 f => RightKanExtension ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments # | |||||||||
RightKanExtension j f => RightKanLift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments # | |||||||||
Double hk vk => Double (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments # | |||||||||
Defined in Proarrow.Category.Double Associated Types
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 # | |||||||||
Defined in Proarrow.Category.Bicategory.Op | |||||||||
CategoryOf (kk k2 j) => Promonad (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments # | |||||||||
CategoryOf (kk k2 j) => Profunctor (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Op | |||||||||
type Ob0 (OPK kk :: k2 -> k2 -> Type) (k3 :: k1) Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Op | |||||||||
type Lan ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments # | |||||||||
type Lift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments # | |||||||||
type Ran ('OP j2 :: OPK kk j1 d) ('OP f :: OPK kk j1 e) Source Comments # | |||||||||
type Rift ('OP j :: OPK kk d k2) ('OP f :: OPK kk e k2) Source Comments # | |||||||||
type I Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Op | |||||||||
type O (a :: OPK kk j k2) (b :: OPK kk k2 k3) Source Comments # | |||||||||
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 # | |||||||||
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 # | |||||||||
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
| |||||||||
type UN ('OP :: kk k2 j -> OPK kk j k2) ('OP k3 :: OPK kk j k2) Source Comments # | |||||||||
type (~>) Source Comments # | |||||||||
type Ob (a :: OPK kk j k2) Source Comments # | |||||||||
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
CategoryOf (kk k2 j) => Promonad (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments # | |
CategoryOf (kk k2 j) => Profunctor (Op :: OPK kk j k2 -> OPK kk j k2 -> Type) Source Comments # | |
Defined in Proarrow.Category.Bicategory.Op |