proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Bicategory.Sub

Documentation

type family IsOb tag (a :: kk i j) 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)
type IsOb Cotight (p :: PROFK j k) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb Cotight (p :: PROFK j k) = Corepresentable (UN ('PK :: (j +-> k) -> PROFK j k) p)
type IsOb Tight (p :: PROFK j k) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb Tight (p :: PROFK j k) = Representable (UN ('PK :: (j +-> k) -> PROFK j k) p)
type IsOb Cotight ('AK ps :: ADJK i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Cotight ('AK ps :: ADJK i j) = IsCotight ps
type IsOb Tight ('AK ps :: ADJK i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Tight ('AK ps :: ADJK i j) = IsTight ps
type IsOb Cotight ('MK a :: MonK k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type IsOb Cotight ('MK a :: MonK k i j) = ()
type IsOb Tight ('MK a :: MonK k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type IsOb Tight ('MK a :: MonK k i j) = ()
type IsOb Cotight (p :: STT' m k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type IsOb Cotight (p :: STT' m k i j) = IsReader m (UN ('ST :: (k +-> k) -> STT' m k i j) p)
type IsOb Tight (p :: STT' m k i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

type IsOb Tight (p :: STT' m k i j) = IsWriter m (UN ('ST :: (k +-> k) -> STT' m k i j) p)
type IsOb Cotight (p :: COK kk i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type IsOb Cotight (p :: COK kk i j) = IsOb Tight (UN ('CO :: kk i j -> COK kk i j) p)
type IsOb Tight (p :: COK kk i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type IsOb Tight (p :: COK kk i j) = IsOb Cotight (UN ('CO :: kk i j -> COK kk i j) p)
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 IsOb tag ('Nil :: Path kk i i) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type IsOb tag ('Nil :: Path kk i i) = ()
type IsOb tag (p '::: ps :: Path kk i1 j) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type IsOb tag (p '::: ps :: Path kk i1 j) = (IsOb tag p, IsOb tag ps)
type IsOb Cotight (p :: PRODK jj kk j2 k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Product

type IsOb Cotight (p :: PRODK jj kk j2 k2) = (IsOb Cotight (PRODFST p), IsOb Cotight (PRODSND p))
type IsOb Tight (p :: PRODK jj kk j2 k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Product

type IsOb Tight (p :: PRODK jj kk j2 k2) = (IsOb Tight (PRODFST p), IsOb Tight (PRODSND p))

type family IsOb0 tag (k :: s) Source Comments #

Instances

Instances details
type IsOb0 Cotight (k2 :: k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

type IsOb0 Cotight (k2 :: k1) = Any k2
type IsOb0 Tight (k2 :: k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment

type IsOb0 Tight (k2 :: k1) = Any k2
type IsOb0 ProfRep (k :: s) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

type IsOb0 ProfRep (k :: s) = ()

data SUBCAT tag (kk :: CAT s) (i :: s) (j :: s) 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 (Rep (FstCat :: (a, b) +-> a))
type Snd FUNK (a :: Type) (b :: Type) 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Snd FUNK (a :: Type) (b :: Type) = FUN (Rep (SndCat :: (a, b) +-> b))
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 (Rep (Terminate :: j +-> ()))

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 #

(Bicategory kk, forall (i :: s). Ob0 kk i => IsObI tag kk i, WithObO2 tag kk) => Bicategory (SUBCAT tag kk :: s -> s -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

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 #

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

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

(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) => Profunctor (Sq' :: (kk j h, SUBCAT Tight kk h i) -> (kk k i, SUBCAT Tight kk j k) -> Type) Source Comments # 
Instance details

Defined in Proarrow.Squares

Methods

dimap :: forall (c0 :: (kk j h, SUBCAT Tight kk h i)) (a :: (kk j h, SUBCAT Tight kk h i)) (b :: (kk k i, SUBCAT Tight kk j k)) (d :: (kk k i, SUBCAT Tight kk j k)). (c0 ~> a) -> (b ~> d) -> Sq' a b -> Sq' c0 d Source Comments #

(\\) :: forall (a :: (kk j h, SUBCAT Tight kk h i)) (b :: (kk k i, SUBCAT Tight kk j k)) r. ((Ob a, Ob b) => r) -> Sq' a b -> r 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 (Rep (Terminate :: j +-> ()))
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 (Rep (FstCat :: (a, b) +-> a))
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 (Rep (SndCat :: (a, b) +-> b))
type Ob0 (SUBCAT tag kk :: s2 -> s2 -> Type) (k :: s1) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Sub

type Ob0 (SUBCAT tag kk :: s2 -> s2 -> Type) (k :: s1) = (Ob0 kk k, IsOb0 tag k)
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 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), IsOb0 tag i, IsOb0 tag j)

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

Constructors

Sub :: forall {s} {i :: s} {j :: s} {ob} {kk :: CAT s} (a1 :: kk i j) (b1 :: kk i j). (IsOb ob a1, IsOb ob b1, IsOb0 ob i, IsOb0 ob j) => (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 WithObO2 tag (kk :: s -> s -> Type) where Source Comments #

Methods

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

Instances

Instances details
WithObO2 Cotight ADJK Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k) (b :: ADJK 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 Tight ADJK Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k) (b :: ADJK 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 #

WithObO2 Cotight PROFK Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withObO2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK 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 Tight PROFK Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Prof

Methods

withObO2 :: forall {i} {j} {k} (a :: PROFK j k) (b :: PROFK 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 #

Monoidal k => WithObO2 Cotight (MonK k :: () -> () -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: MonK k j k0) (b :: MonK k 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 #

Monoidal k => WithObO2 Tight (MonK k :: () -> () -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: MonK k j k0) (b :: MonK k 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 #

(MonoidalAction m k, m ~ Type) => WithObO2 Cotight (STT' m k :: () -> () -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' m k j k0) (b :: STT' m k 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 #

(MonoidalAction m k, m ~ Type) => WithObO2 Tight (STT' m k :: () -> () -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' m k j k0) (b :: STT' m k 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 #

WithObO2 Tight kk => WithObO2 Cotight (COK kk :: s -> s -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: COK kk j k) (b :: COK 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 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 (COK kk :: s -> s -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: COK kk j k) (b :: COK 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 #

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 #

WithObO2 tag kk => WithObO2 tag (Path kk :: s -> s -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

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

(WithObO2 Cotight jj, WithObO2 Cotight kk) => WithObO2 Cotight (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

withObO2 :: forall {i :: (j, k)} {j0 :: (j, k)} {k0 :: (j, k)} (a :: PRODK jj kk j0 k0) (b :: PRODK jj kk i j0) 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 Tight jj, WithObO2 Tight kk) => WithObO2 Tight (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Product

Methods

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

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

Instances

Instances details
IsOb tag (I :: kk i i) => IsObI tag (kk :: k -> k -> Type) (i :: k) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Sub