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

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 #

(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

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