Safe Haskell	None
Language	GHC2024

Proarrow.Category.Equipment

Documentation

class (Bicategory kk, Bicategory (SUBCAT Tight kk), Bicategory (SUBCAT Cotight kk), WithObO2 Cotight kk, WithObO2 Tight kk) => Equipment (kk :: CAT k) where Source Comments #

Methods

withCotightAdjoint :: forall {j :: k} {k1 :: k} (f :: kk j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: kk j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #

Instances

Instances details

Equipment ADJK Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj Methods withCotightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #
Equipment PROFK Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods withCotightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #
CompactClosed k => Equipment (MonK k :: () -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods withCotightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #
(SymMonoidalAction m k, m ~ Type) => Equipment (STT' m k :: () -> () -> Type) Source Comments #	Stateful transformers. https://arxiv.org/pdf/2305.16899 definition 6 Generalized to any symmetric monoidal action.
Instance details Defined in Proarrow.Category.Equipment.Stateful Methods withCotightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' m k j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' m k j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #
Equipment kk => Equipment (COK kk :: k -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Co Methods withCotightAdjoint :: forall {j :: k} {k1 :: k} (f :: COK kk j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: COK kk j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #
Equipment kk => Equipment (OPK kk :: k -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op Methods withCotightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #
(Equipment jj, Equipment kk) => Equipment (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product Methods withCotightAdjoint :: forall {j0 :: (j, k)} {k1 :: (j, k)} (f :: PRODK jj kk j0 k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments # withTightAdjoint :: forall {j0 :: (j, k)} {k1 :: (j, k)} (f :: PRODK jj kk j0 k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #

type family TightAdjoint (p :: kk j i) :: kk i j Source Comments #

Instances

Instances details

type TightAdjoint (p :: PROFK k j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type TightAdjoint (p :: PROFK k j) = 'PK (CorepStar (UN ('PK :: (k +-> j) -> PROFK k j) p))
type TightAdjoint ('AK ps :: ADJK j i) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdjoint ('AK ps :: ADJK j i) = 'AK (TightAdj ps)
type TightAdjoint (a :: MonK k i j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type TightAdjoint (a :: MonK k i j) = Dual a :: MonK k j i
type TightAdjoint (p :: STT' m k i j) Source Comments #
Instance details Defined in Proarrow.Category.Equipment.Stateful type TightAdjoint (p :: STT' m k i j) = 'ST (WithWriter m (UN ('ST :: (k +-> k) -> STT' m k i j) p)) :: STT' m k j i
type TightAdjoint (p :: COK kk k2 j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Co type TightAdjoint (p :: COK kk k2 j) = 'CO (CotightAdjoint (UN ('CO :: kk k2 j -> COK kk k2 j) p))
type TightAdjoint (p :: OPK kk k2 j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op type TightAdjoint (p :: OPK kk k2 j) = 'OP (CotightAdjoint (UN ('OP :: kk j k2 -> OPK kk k2 j) p))
type TightAdjoint (p :: PRODK jj kk j2 k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product type TightAdjoint (p :: PRODK jj kk j2 k2) = 'PROD (TightAdjoint (PRODFST p)) (TightAdjoint (PRODSND p)) :: PRODK jj kk k2 j2

type family CotightAdjoint (p :: kk j i) :: kk i j Source Comments #

Instances

Instances details

type CotightAdjoint (p :: PROFK k j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof type CotightAdjoint (p :: PROFK k j) = 'PK (RepCostar (UN ('PK :: (k +-> j) -> PROFK k j) p))
type CotightAdjoint ('AK ps :: ADJK j i) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdjoint ('AK ps :: ADJK j i) = 'AK (CotightAdj ps)
type CotightAdjoint (a :: MonK k i j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type CotightAdjoint (a :: MonK k i j) = Dual a :: MonK k j i
type CotightAdjoint (p :: STT' m k i j) Source Comments #
Instance details Defined in Proarrow.Category.Equipment.Stateful type CotightAdjoint (p :: STT' m k i j) = 'ST (WithReader m (UN ('ST :: (k +-> k) -> STT' m k i j) p)) :: STT' m k j i
type CotightAdjoint (p :: COK kk k2 j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Co type CotightAdjoint (p :: COK kk k2 j) = 'CO (TightAdjoint (UN ('CO :: kk k2 j -> COK kk k2 j) p))
type CotightAdjoint (p :: OPK kk k2 j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Op type CotightAdjoint (p :: OPK kk k2 j) = 'OP (TightAdjoint (UN ('OP :: kk j k2 -> OPK kk k2 j) p))
type CotightAdjoint (p :: PRODK jj kk j2 k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Product type CotightAdjoint (p :: PRODK jj kk j2 k2) = 'PROD (CotightAdjoint (PRODFST p)) (CotightAdjoint (PRODSND p)) :: PRODK jj kk k2 j2

data Tight Source Comments #

Instances

Instances details

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 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 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 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 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 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 #
(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 #
type IsOb0 Tight (k2 :: k1) Source Comments #
Instance details Defined in Proarrow.Category.Equipment type IsOb0 Tight (k2 :: k1) = Any k2
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 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 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 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 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 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 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))

data Cotight 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 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 #
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 #
(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 #
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 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 #
type IsOb0 Cotight (k2 :: k1) Source Comments #
Instance details Defined in Proarrow.Category.Equipment type IsOb0 Cotight (k2 :: k1) = Any k2
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 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 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 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 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 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 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))

class (IsOb Cotight f, Ob f) => IsCotight (f :: kk i j) Source Comments #

Instances

Instances details

(IsOb Cotight f, Ob f) => IsCotight (f :: kk i j) Source Comments #
Instance details Defined in Proarrow.Category.Equipment

class (IsOb Tight f, Ob f) => IsTight (f :: kk i j) Source Comments #

Instances

Instances details

(IsOb Tight f, Ob f) => IsTight (f :: kk i j) Source Comments #
Instance details Defined in Proarrow.Category.Equipment

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

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 (IsTight f, IsCotight g, Adjunction f g) => TightPair (f :: kk c d) (g :: kk d c) Source Comments #

Instances

Instances details

(IsTight f, IsCotight g, Adjunction f g) => TightPair (f :: kk c d) (g :: kk d c) Source Comments #
Instance details Defined in Proarrow.Category.Equipment