Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Sub

Documentation

type family IsOb tag (a :: k) Source Comments #

Instances

Instances details

type IsOb ProfRep (p :: PROFK j k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type IsOb ProfRep (p :: PROFK j k) = Representable (UN ('PK :: (j +-> k) -> PROFK j k) p)

data SUBCAT tag (kk :: CAT k) (i :: k) (j :: k) Source Comments #

Constructors

SUB (kk i j)

Instances

Instances details

HasBinaryProducts FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Fst FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Fst FUNK (a :: Type) (b :: Type) = FUN (FstCat :: a -> (a, b) -> Type)
type Snd FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Snd FUNK (a :: Type) (b :: Type) = FUN (SndCat :: b -> (a, b) -> Type)
type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) = FUN (UNFUN f :&&&: UNFUN g)

Methods

fstObj :: (Ob0 FUNK a, Ob0 FUNK b) => Obj (Fst FUNK a b) Source Comments #

sndObj :: (Ob0 FUNK a, Ob0 FUNK b) => Obj (Snd FUNK a b) Source Comments #

prodObj :: forall j a b (f :: FUNK j a) (g :: FUNK j b). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob f, Ob g) => Obj (f &&& g) Source Comments #

prodUniv :: forall j a b (h :: FUNK j (Product FUNK a b)) (k :: FUNK j (Product FUNK a b)). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob h, Ob k) => (O (Fst FUNK a b) h ~> O (Fst FUNK a b) k) -> (O (Snd FUNK a b) h ~> O (Snd FUNK a b) k) -> h ~> k Source Comments #

HasTerminalObject FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Terminate FUNK (j :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Terminate FUNK (j :: Type) = FUN (Terminate :: () -> j -> Type)

Methods

terminate :: Ob0 FUNK j => Obj (Terminate FUNK j) Source Comments #

termUniv :: forall j (f :: FUNK j (TerminalObject FUNK)) (g :: FUNK j (TerminalObject FUNK)). (Ob0 FUNK j, Ob f, Ob g) => f ~> g Source Comments #

Equipment PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

Methods

mapConjoint :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Conjoint PROFK g ~> Conjoint PROFK f Source Comments #

conjToId :: Ob0 FUNK k => Conjoint PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

conjFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Conjoint PROFK (I :: FUNK k k) Source Comments #

conjToCompose :: forall {k1} {j} {k2} (f :: FUNK j k2) (g :: FUNK k1 j). Obj f -> Obj g -> Conjoint PROFK (O f g) ~> O (Conjoint PROFK g) (Conjoint PROFK f) Source Comments #

conjFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Conjoint PROFK g) (Conjoint PROFK f) ~> Conjoint PROFK (O f g) Source Comments #

comConUnit :: forall {j} {k} (f :: FUNK j k). Obj f -> (I :: PROFK j j) ~> O (Conjoint PROFK f) (Companion PROFK f) Source Comments #

comConCounit :: forall {j} {k} (f :: FUNK j k). Obj f -> O (Companion PROFK f) (Conjoint PROFK f) ~> (I :: PROFK k k) Source Comments #

HasCompanions PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

Methods

mapCompanion :: forall {j} {k} (f :: FUNK j k) (g :: FUNK j k). (f ~> g) -> Companion PROFK f ~> Companion PROFK g Source Comments #

compToId :: Ob0 FUNK k => Companion PROFK (I :: FUNK k k) ~> (I :: PROFK k k) Source Comments #

compFromId :: Ob0 FUNK k => (I :: PROFK k k) ~> Companion PROFK (I :: FUNK k k) Source Comments #

compToCompose :: forall {i} {j} {k} (f :: FUNK j k) (g :: FUNK i j). Obj f -> Obj g -> Companion PROFK (O f g) ~> O (Companion PROFK f) (Companion PROFK g) Source Comments #

compFromCompose :: forall {j1} {j2} {k} (f :: FUNK j2 k) (g :: FUNK j1 j2). Obj f -> Obj g -> O (Companion PROFK f) (Companion PROFK g) ~> Companion PROFK (O f g) Source Comments #

HasBinaryCoproducts PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Lft PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Lft PROFK FUNK (a :: Type) (b :: Type) = FUN (LftCat :: COPRODUCT a b -> a -> Type)
type Rgt PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Rgt PROFK FUNK (a :: Type) (b :: Type) = FUN (RgtCat :: COPRODUCT a b -> b -> Type)
type CoprodV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i j1) ('SUB ('PK g) :: SUBCAT ProfRep PROFK j2 j1)
Instance details Defined in Proarrow.Category.Bicategory.Prof type CoprodV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i j1) ('SUB ('PK g) :: SUBCAT ProfRep PROFK j2 j1) = 'SUB ('PK (f :\|\|\|: g)) :: SUBCAT ProfRep PROFK (COPRODUCT i j2) j1
type CoprodH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2)
Instance details Defined in Proarrow.Category.Bicategory.Prof type CoprodH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) = 'PK (p :++: q)

Methods

lftObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Lft PROFK FUNK i j) Source Comments #

rgtObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Rgt PROFK FUNK i j) Source Comments #

coprodObj :: forall j a b (f :: FUNK a j) (g :: FUNK b j). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob f, Ob g) => Obj (CoprodV PROFK FUNK f g) Source Comments #

coprodUniv :: forall i i' (a :: PROFK i i') k' (f' :: FUNK i' k') k (p :: PROFK k k') (f :: FUNK i k) j j' (b :: PROFK j j') (g' :: FUNK j' k') (g :: FUNK j k). Sq '(a, f') '(p, f) -> Sq '(b, g') '(p, g) -> Sq '(CoprodH PROFK FUNK a b, CoprodV PROFK FUNK f' g') '(p, CoprodV PROFK FUNK f g) Source Comments #

HasBinaryProducts PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Fst PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Fst PROFK FUNK (a :: Type) (b :: Type) = FUN (FstCat :: a -> (a, b) -> Type)
type Snd PROFK FUNK (a :: Type) (b :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Snd PROFK FUNK (a :: Type) (b :: Type) = FUN (SndCat :: b -> (a, b) -> Type)
type ProdV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i1 i2) ('SUB ('PK g) :: SUBCAT ProfRep PROFK i1 j)
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProdV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i1 i2) ('SUB ('PK g) :: SUBCAT ProfRep PROFK i1 j) = 'SUB ('PK (f :&&&: g)) :: SUBCAT ProfRep PROFK i1 (i2, j)
type ProdH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2)
Instance details Defined in Proarrow.Category.Bicategory.Prof type ProdH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) = 'PK (p :**: q)

Methods

fstObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Fst PROFK FUNK i j) Source Comments #

sndObj :: (Ob0 FUNK i, Ob0 FUNK j) => Obj (Snd PROFK FUNK i j) Source Comments #

prodObj :: forall j a b (f :: FUNK j a) (g :: FUNK j b). (Ob0 FUNK j, Ob0 FUNK a, Ob0 FUNK b, Ob f, Ob g) => Obj (ProdV PROFK FUNK f g) Source Comments #

prodUniv :: forall {i} {j} k k' (p :: PROFK k k') i' (f' :: FUNK k' i') (a :: PROFK i i') (f :: FUNK k i) j' (g' :: FUNK k' j') (b :: PROFK j j') (g :: FUNK k j). Sq '(p, f') '(a, f) -> Sq '(p, g') '(b, g) -> Sq '(p, ProdV PROFK FUNK f' g') '(ProdH PROFK FUNK a b, ProdV PROFK FUNK f g) Source Comments #

HasInitialObject PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Initiate PROFK FUNK (j :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Initiate PROFK FUNK (j :: Type) = FUN (Initiate :: j -> VOID -> Type)

Methods

initiate :: Ob0 FUNK j => Obj (Initiate PROFK FUNK j) Source Comments #

initUniv :: forall i j (p :: PROFK i j). (Ob0 FUNK i, Ob0 FUNK j, Ob p) => Sq '(I :: PROFK (InitialObject PROFK FUNK) (InitialObject PROFK FUNK), Initiate PROFK FUNK j) '(p, Initiate PROFK FUNK i) Source Comments #

HasTerminalObject PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Associated Types

type Terminate PROFK FUNK (j :: Type)
Instance details Defined in Proarrow.Category.Bicategory.Prof type Terminate PROFK FUNK (j :: Type) = FUN (Terminate :: () -> j -> Type)

Methods

terminate :: Ob0 FUNK j => Obj (Terminate PROFK FUNK j) Source Comments #

termUniv :: forall i j (p :: PROFK i j). (Ob0 FUNK i, Ob0 FUNK j, Ob p) => Sq '(p, Terminate PROFK FUNK j) '(I :: PROFK (TerminalObject PROFK FUNK) (TerminalObject PROFK FUNK), Terminate PROFK FUNK i) Source Comments #

(HasColimits j k, Ob j) => HasColimits FUNK ('PK j :: PROFK a i) (k :: Kind) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

colimitObj :: forall (d :: FUNK i k). Ob d => Obj (Colimit ('PK j) d) Source Comments #

colimit :: forall (d :: FUNK i k). Ob d => O (Companion PROFK d) ('PK j) ~> Companion PROFK (Colimit ('PK j) d) Source Comments #

colimitUniv :: forall (d :: FUNK i k) (p :: FUNK a k). (Ob d, Ob p) => (O (Companion PROFK d) ('PK j) ~> Companion PROFK p) -> Colimit ('PK j) d ~> p Source Comments #

(HasLimits j k, Ob j) => HasLimits FUNK ('PK j :: PROFK i a) (k :: Kind) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

limitObj :: forall (d :: FUNK i k). Ob d => Obj (Limit ('PK j) d) Source Comments #

limit :: forall (d :: FUNK i k). Ob d => O (Companion PROFK (Limit ('PK j) d)) ('PK j) ~> Companion PROFK d Source Comments #

limitUniv :: forall (d :: FUNK i k) (p :: FUNK a k). (Ob d, Ob p) => (O (Companion PROFK p) ('PK j) ~> Companion PROFK d) -> p ~> Limit ('PK j) d Source Comments #

(Bicategory kk, forall (i :: s). Ob0 kk i => IsObI tag kk i, forall (i :: s) (j :: s) (k :: s) (a :: kk j k) (b :: kk i j). (IsOb tag a, IsOb tag b) => IsObO tag kk i j k a b) => Bicategory (SUBCAT tag kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: SUBCAT tag kk j k) (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk h i). (Ob0 (SUBCAT tag kk) h, Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob0 (SUBCAT tag 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 :: SUBCAT tag kk j k) (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk h i). (Ob0 (SUBCAT tag kk) h, Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob0 (SUBCAT tag kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

CategoryOf (kk i j) => CategoryOf (SUBCAT tag kk i j) Source Comments #

The subcategory with objects with instances of the given constraint `IsOb tag`.

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Sub type (~>) = Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type

Promonad ((~>) :: CAT (kk i j)) => Promonad (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

id :: forall (a :: SUBCAT tag kk i j). Ob a => Sub a a Source Comments #

(.) :: forall (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j). Sub b c -> Sub a b -> Sub a c Source Comments #

Profunctor ((~>) :: CAT (kk i j)) => Profunctor (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

dimap :: forall (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) (d :: SUBCAT tag kk i j). (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d Source Comments #

(\\) :: forall (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) r. ((Ob a, Ob b) => r) -> Sub a b -> r Source Comments #

type TerminalObject FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TerminalObject FUNK = ()

type Terminate FUNK (j :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Terminate FUNK (j :: Type) = FUN (Terminate :: () -> j -> Type)

type InitialObject PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type InitialObject PROFK FUNK = VOID

type TerminalObject PROFK FUNK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TerminalObject PROFK FUNK = ()

type Fst FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Fst FUNK (a :: Type) (b :: Type) = FUN (FstCat :: a -> (a, b) -> Type)

type Product FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Product FUNK (a :: Type) (b :: Type) = (a, b)

type Snd FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Snd FUNK (a :: Type) (b :: Type) = FUN (SndCat :: b -> (a, b) -> Type)

type Initiate PROFK FUNK (j :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Initiate PROFK FUNK (j :: Type) = FUN (Initiate :: j -> VOID -> Type)

type Terminate PROFK FUNK (j :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Terminate PROFK FUNK (j :: Type) = FUN (Terminate :: () -> j -> Type)

type Coproduct PROFK FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Coproduct PROFK FUNK (a :: Type) (b :: Type) = COPRODUCT a b

type Fst PROFK FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Fst PROFK FUNK (a :: Type) (b :: Type) = FUN (FstCat :: a -> (a, b) -> Type)

type Lft PROFK FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Lft PROFK FUNK (a :: Type) (b :: Type) = FUN (LftCat :: COPRODUCT a b -> a -> Type)

type Product PROFK FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Product PROFK FUNK (a :: Type) (b :: Type) = (a, b)

type Rgt PROFK FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Rgt PROFK FUNK (a :: Type) (b :: Type) = FUN (RgtCat :: COPRODUCT a b -> b -> Type)

type Snd PROFK FUNK (a :: Type) (b :: Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Snd PROFK FUNK (a :: Type) (b :: Type) = FUN (SndCat :: b -> (a, b) -> Type)

type CoprodH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type CoprodH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) = 'PK (p :++: q)

type ProdH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type ProdH PROFK FUNK ('PK p :: PROFK j1 k1) ('PK q :: PROFK j2 k2) = 'PK (p :**: q)

type CoprodV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i j1) ('SUB ('PK g) :: SUBCAT ProfRep PROFK j2 j1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type CoprodV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i j1) ('SUB ('PK g) :: SUBCAT ProfRep PROFK j2 j1) = 'SUB ('PK (f :|||: g)) :: SUBCAT ProfRep PROFK (COPRODUCT i j2) j1

type ProdV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i1 i2) ('SUB ('PK g) :: SUBCAT ProfRep PROFK i1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type ProdV PROFK FUNK ('SUB ('PK f) :: SUBCAT ProfRep PROFK i1 i2) ('SUB ('PK g) :: SUBCAT ProfRep PROFK i1 j) = 'SUB ('PK (f :&&&: g)) :: SUBCAT ProfRep PROFK i1 (i2, j)

type Colimit ('PK j :: PROFK a i) (d :: SUBCAT ProfRep PROFK i k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Colimit ('PK j :: PROFK a i) (d :: SUBCAT ProfRep PROFK i k) = FUN (Colimit j (UNFUN d))

type Limit ('PK j :: PROFK i a) (d :: SUBCAT ProfRep PROFK i k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Limit ('PK j :: PROFK i a) (d :: SUBCAT ProfRep PROFK i k) = FUN (Limit j (UNFUN d))

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

Instance details

Defined in Proarrow.Category.Bicategory.Sub

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

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type I = 'SUB (I :: kk i i) :: SUBCAT tag kk i i

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Companion PROFK (p :: SUBCAT ProfRep PROFK j k) = 'PK (UNFUN p)

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Conjoint PROFK (p :: SUBCAT ProfRep PROFK k j) = 'PK (RepCostar (UNFUN p))

type O (p :: SUBCAT tag kk j1 j2) (q :: SUBCAT tag kk i j1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type O (p :: SUBCAT tag kk j1 j2) (q :: SUBCAT tag kk i j1) = 'SUB (O (UN ('SUB :: kk j1 j2 -> SUBCAT tag kk j1 j2) p) (UN ('SUB :: kk i j1 -> SUBCAT tag kk i j1) q)) :: SUBCAT tag kk i j2

type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type (f :: SUBCAT ProfRep PROFK i1 i2) &&& (g :: SUBCAT ProfRep PROFK i1 j) = FUN (UNFUN f :&&&: UNFUN g)

type UN ('SUB :: kk i j -> SUBCAT tag kk i j) ('SUB p :: SUBCAT tag kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type UN ('SUB :: kk i j -> SUBCAT tag kk i j) ('SUB p :: SUBCAT tag kk i j) = p

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type (~>) = Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type

type Ob (a :: SUBCAT tag kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type Ob (a :: SUBCAT tag kk i j) = (Is ('SUB :: kk i j -> SUBCAT tag kk i j) a, Ob (UN ('SUB :: kk i j -> SUBCAT tag kk i j) a), IsOb tag (UN ('SUB :: kk i j -> SUBCAT tag kk i j) a))

data Sub (a :: SUBCAT ob kk i j) (b :: SUBCAT ob kk i j) where Source Comments #

Constructors

Sub :: forall {k} ob (kk :: CAT k) (i :: k) (j :: k) (a1 :: kk i j) (b1 :: kk i j). (IsOb ob a1, IsOb ob b1) => (a1 ~> b1) -> Sub ('SUB a1 :: SUBCAT ob kk i j) ('SUB b1 :: SUBCAT ob kk i j)

Instances

Instances details

Promonad ((~>) :: CAT (kk i j)) => Promonad (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub Methods id :: forall (a :: SUBCAT tag kk i j). Ob a => Sub a a Source Comments # (.) :: forall (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j). Sub b c -> Sub a b -> Sub a c Source Comments #
Profunctor ((~>) :: CAT (kk i j)) => Profunctor (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub Methods dimap :: forall (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) (d :: SUBCAT tag kk i j). (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d Source Comments # (\\) :: forall (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) r. ((Ob a, Ob b) => r) -> Sub a b -> r Source Comments #

class IsOb tag (O a b) => IsObO tag (kk :: s -> s -> Type) (i :: s) (j :: s) (k :: s) (a :: kk j k) (b :: kk i j) Source Comments #

Instances

Instances details

IsOb tag (O a b) => IsObO tag (kk :: s -> s -> Type) (i :: s) (j :: s) (k :: s) (a :: kk j k) (b :: kk i j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub

class IsOb tag (I :: kk i i) => IsObI tag (kk :: s -> s -> Type) (i :: s) Source Comments #

Instances

Instances details

IsOb tag (I :: kk i i) => IsObI tag (kk :: s -> s -> Type) (i :: s) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub