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

Methods

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

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

Instances

Instances details

Equipment ADJK Source Github #
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 Github # withTightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Github #
Equipment PROFK Source Github #
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 Github # withTightAdjoint :: forall {j} {k1} (f :: PROFK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Github #
CompactClosed k => Equipment (MonK k :: () -> () -> Type) Source Github #
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 Github # withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Github #
SymMonoidal k => Equipment (STT' k :: () -> () -> Type) Source Github #	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' k j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Github # withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' k j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Github #
Equipment kk => Equipment (COK kk :: k -> k -> Type) Source Github #
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 Github # withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: COK kk j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Github #
Equipment kk => Equipment (OPK kk :: k -> k -> Type) Source Github #
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 Github # withTightAdjoint :: forall {j :: k} {k1 :: k} (f :: OPK kk j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Github #
(Equipment jj, Equipment kk) => Equipment (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Github #
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 Github # 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 Github #

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

Instances

Instances details

type TightAdjoint (p :: PROFK k j) Source Github #
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 Github #
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 Github #
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' k i j) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful type TightAdjoint (p :: STT' k i j) = 'ST (WithWriter (UN ('ST :: (k +-> k) -> STT' k i j) p)) :: STT' k j i
type TightAdjoint (p :: COK kk k2 j) Source Github #
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 Github #
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 j k3) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.Product type TightAdjoint (p :: PRODK jj kk j k3) = 'PROD (TightAdjoint (PRODFST p)) (TightAdjoint (PRODSND p)) :: PRODK jj kk k3 j

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

Instances

Instances details

type CotightAdjoint (p :: PROFK k j) Source Github #
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 Github #
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 Github #
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' k i j) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful type CotightAdjoint (p :: STT' k i j) = 'ST (WithReader (UN ('ST :: (k +-> k) -> STT' k i j) p)) :: STT' k j i
type CotightAdjoint (p :: COK kk k2 j) Source Github #
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 Github #
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 j k3) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.Product type CotightAdjoint (p :: PRODK jj kk j k3) = 'PROD (CotightAdjoint (PRODFST p)) (CotightAdjoint (PRODSND p)) :: PRODK jj kk k3 j

data Tight Source Github #

Instances

Instances details

HasBinaryProducts FUNK Source Github #

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 (Fst :: (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 (Snd :: (a, b) +-> b))
type (f :: SUBCAT Tight PROFK i k1) &&& (g :: SUBCAT Tight PROFK i k2)
Instance details Defined in Proarrow.Category.Bicategory.Prof type (f :: SUBCAT Tight PROFK i k1) &&& (g :: SUBCAT Tight PROFK i k2) = FUN ((UNFUN f :**: UNFUN g) :.: Rep (Diag :: i +-> (i, i)))

Methods

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

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

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

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

HasTerminalObject FUNK Source Github #

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 (Constant '()))

Methods

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

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

WithObO2 Tight ADJK Source Github #

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

WithObO2 Tight PROFK Source Github #

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

Monoidal k => WithObO2 Tight (MonK k :: () -> () -> Type) Source Github #

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

SymMonoidal k => WithObO2 Tight (STT' k :: () -> () -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

Methods

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

WithObO2 Cotight kk => WithObO2 Tight (COK kk :: s -> s -> Type) Source Github #

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

WithObO2 Cotight kk => WithObO2 Tight (OPK kk :: s -> s -> Type) Source Github #

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

Monoidal (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.CatFun type Unit = 'B () :: BI FUNK
type (j :: BI FUNK) ** (k :: BI FUNK)
Instance details Defined in Proarrow.Category.Instance.CatFun type (j :: BI FUNK) ** (k :: BI FUNK) = 'B (UN ('B :: Type -> BI FUNK) j, UN ('B :: Type -> BI FUNK) k) :: BI FUNK

Methods

withOb2 :: forall (a :: BI FUNK) (b :: BI FUNK) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: BI FUNK). Ob a => ((Unit :: BI FUNK) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: BI FUNK). Ob a => a ~> ((Unit :: BI FUNK) ** a) Source Github #

rightUnitor :: forall (a :: BI FUNK). Ob a => (a ** (Unit :: BI FUNK)) ~> a Source Github #

rightUnitorInv :: forall (a :: BI FUNK). Ob a => a ~> (a ** (Unit :: BI FUNK)) Source Github #

associator :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Methods

swap :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Closed (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Associated Types

type ('B j :: BI FUNK) ~~> ('B k :: BI FUNK)
Instance details Defined in Proarrow.Category.Instance.CatFun type ('B j :: BI FUNK) ~~> ('B k :: BI FUNK) = 'B (FUN j k) :: BI FUNK

Methods

withObExp :: forall (a :: BI FUNK) (b :: BI FUNK) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: BI FUNK) (b :: BI FUNK) (x :: BI FUNK) (y :: BI FUNK). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

Distributive (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Methods

distL :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: BI FUNK) (b :: BI FUNK) (c :: BI FUNK). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: BI FUNK). Ob a => (a ** (InitialObject :: BI FUNK)) ~> (InitialObject :: BI FUNK) Source Github #

absorbR :: forall (a :: BI FUNK). Ob a => ((InitialObject :: BI FUNK) ** a) ~> (InitialObject :: BI FUNK) Source Github #

HasBinaryCoproducts (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Associated Types

type ('B l :: BI FUNK) \|\| ('B r :: BI FUNK)
Instance details Defined in Proarrow.Category.Instance.CatFun type ('B l :: BI FUNK) \|\| ('B r :: BI FUNK) = 'B (COPRODUCT l r) :: BI FUNK

Methods

withObCoprod :: forall (a :: BI FUNK) (b :: BI FUNK) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: BI FUNK) (a :: BI FUNK) (y :: BI FUNK). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: BI FUNK) (b :: BI FUNK) (x :: BI FUNK) (y :: BI FUNK). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasInitialObject (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.CatFun type InitialObject = 'B VOID :: BI FUNK

Methods

initiate :: forall (a :: BI FUNK). Ob a => (InitialObject :: BI FUNK) ~> a Source Github #

HasBinaryProducts (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Associated Types

type (l :: BI FUNK) && (r :: BI FUNK)
Instance details Defined in Proarrow.Category.Instance.CatFun type (l :: BI FUNK) && (r :: BI FUNK) = 'B (UN ('B :: Type -> BI FUNK) l, UN ('B :: Type -> BI FUNK) r) :: BI FUNK

Methods

withObProd :: forall (a :: BI FUNK) (b :: BI FUNK) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: BI FUNK) (b :: BI FUNK). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: BI FUNK) (x :: BI FUNK) (y :: BI FUNK). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: BI FUNK) (b :: BI FUNK) (x :: BI FUNK) (y :: BI FUNK). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasTerminalObject (BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.CatFun type TerminalObject = 'B () :: BI FUNK

Methods

terminate :: forall (a :: BI FUNK). Ob a => a ~> (TerminalObject :: BI FUNK) Source Github #

(WithObO2 Tight jj, WithObO2 Tight kk) => WithObO2 Tight (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Github #

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

MonoidalProfunctor (Bi :: BI FUNK -> BI FUNK -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Methods

one :: Bi (Unit :: BI FUNK) (Unit :: BI FUNK) Source Github #

(**) :: forall (x1 :: BI FUNK) (x2 :: BI FUNK) (y1 :: BI FUNK) (y2 :: BI FUNK). Bi x1 x2 -> Bi y1 y2 -> Bi (x1 ** y1) (x2 ** y2) Source Github #

Bicategory kk => EnrichedProfunctor (BI FUNK) (Bi :: BI kk -> BI kk -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

Methods

withProObj :: forall (a :: BI kk) (b :: BI kk) r. (Ob a, Ob b) => (Ob (ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) a b) => r) -> r Source Github #

underlying :: forall (a :: BI kk) (b :: BI kk). Bi a b -> (Unit :: BI FUNK) ~> ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) a b Source Github #

enriched :: forall (a :: BI kk) (b :: BI kk). (Ob a, Ob b) => ((Unit :: BI FUNK) ~> ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) a b) -> Bi a b Source Github #

rmap :: forall (a :: BI kk) (b :: BI kk) (c :: BI kk). (Ob a, Ob b, Ob c) => (HomObj (BI FUNK) b c ** ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) a b) ~> ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) a c Source Github #

lmap :: forall (a :: BI kk) (b :: BI kk) (c :: BI kk). (Ob a, Ob b, Ob c) => (HomObj (BI FUNK) c a ** ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) a b) ~> ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) c b Source Github #

(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 Github #

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

lmap :: 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)). (c0 ~> a) -> Sq' a b -> Sq' c0 b Source Github #

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

(\\) :: 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 Github #

type TerminalObject FUNK Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type TerminalObject FUNK = ()

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type Terminate FUNK (j :: Type) = FUN (Rep (Constant '()))

type IsOb0 Tight (k2 :: k1) Source Github #

Instance details

Defined in Proarrow.Category.Equipment

type IsOb0 Tight (k2 :: k1) = Any k2

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

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

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

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

Instance details

Defined in Proarrow.Category.Bicategory.Prof

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

type IsOb Tight (p :: PROFK j k) Source Github #

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

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Tight ('AK ps :: ADJK i j) = IsTight ps

type IsOb Tight (p :: STT' k i j) Source Github #

Instance details

Defined in Proarrow.Category.Equipment.Stateful

type IsOb Tight (p :: STT' k i j) = IsWriter (UN ('ST :: (k +-> k) -> STT' k i j) p)

type IsOb Tight ('MK a :: MonK k i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type IsOb Tight ('MK a :: MonK k i j) = ()

type IsOb Tight (p :: COK kk i j) Source Github #

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

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 (f :: SUBCAT Tight PROFK i k1) &&& (g :: SUBCAT Tight PROFK i k2) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.Prof

type (f :: SUBCAT Tight PROFK i k1) &&& (g :: SUBCAT Tight PROFK i k2) = FUN ((UNFUN f :**: UNFUN g) :.: Rep (Diag :: i +-> (i, i)))

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type Unit = 'B () :: BI FUNK

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type InitialObject = 'B VOID :: BI FUNK

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type TerminalObject = 'B () :: BI FUNK

type (j :: BI FUNK) ** (k :: BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type (j :: BI FUNK) ** (k :: BI FUNK) = 'B (UN ('B :: Type -> BI FUNK) j, UN ('B :: Type -> BI FUNK) k) :: BI FUNK

type (l :: BI FUNK) && (r :: BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type (l :: BI FUNK) && (r :: BI FUNK) = 'B (UN ('B :: Type -> BI FUNK) l, UN ('B :: Type -> BI FUNK) r) :: BI FUNK

type ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) ('B j :: BI kk) ('B k :: BI kk) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type ProObj (BI FUNK) (Bi :: BI kk -> BI kk -> Type) ('B j :: BI kk) ('B k :: BI kk) = 'B (kk j k) :: BI FUNK

type IsOb Tight (p :: PRODK jj kk j k3) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.Product

type IsOb Tight (p :: PRODK jj kk j k3) = (IsOb Tight (PRODFST p), IsOb Tight (PRODSND p))

type ('B j :: BI FUNK) ~~> ('B k :: BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type ('B j :: BI FUNK) ~~> ('B k :: BI FUNK) = 'B (FUN j k) :: BI FUNK

type ('B l :: BI FUNK) || ('B r :: BI FUNK) Source Github #

Instance details

Defined in Proarrow.Category.Instance.CatFun

type ('B l :: BI FUNK) || ('B r :: BI FUNK) = 'B (COPRODUCT l r) :: BI FUNK

data Cotight Source Github #

Instances

Instances details

WithObO2 Cotight ADJK Source Github #
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 Github #
WithObO2 Cotight PROFK Source Github #
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 Github #
Monoidal k => WithObO2 Cotight (MonK k :: () -> () -> Type) Source Github #
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 Github #
SymMonoidal k => WithObO2 Cotight (STT' k :: () -> () -> Type) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful Methods withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' k j k0) (b :: STT' 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 Github #
WithObO2 Tight kk => WithObO2 Cotight (COK kk :: s -> s -> Type) Source Github #
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 Github #
WithObO2 Tight kk => WithObO2 Cotight (OPK kk :: s -> s -> Type) Source Github #
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 Github #
(WithObO2 Cotight jj, WithObO2 Cotight kk) => WithObO2 Cotight (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Github #
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 Github #
type IsOb0 Cotight (k2 :: k1) Source Github #
Instance details Defined in Proarrow.Category.Equipment type IsOb0 Cotight (k2 :: k1) = Any k2
type IsOb Cotight (p :: PROFK j k) Source Github #
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 Github #
Instance details Defined in Proarrow.Category.Bicategory.Adj type IsOb Cotight ('AK ps :: ADJK i j) = IsCotight ps
type IsOb Cotight (p :: STT' k i j) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful type IsOb Cotight (p :: STT' k i j) = IsReader (UN ('ST :: (k +-> k) -> STT' k i j) p)
type IsOb Cotight ('MK a :: MonK k i j) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type IsOb Cotight ('MK a :: MonK k i j) = ()
type IsOb Cotight (p :: COK kk i j) Source Github #
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 Github #
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 j k3) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.Product type IsOb Cotight (p :: PRODK jj kk j k3) = (IsOb Cotight (PRODFST p), IsOb Cotight (PRODSND p))

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

Instances

Instances details

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

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

Instances

Instances details

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

type family IsOb tag (a :: kk i j) Source Github #

Instances

Instances details

type IsOb Cotight (p :: PROFK j k) Source Github #
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 Github #
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 Github #
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 Github #
Instance details Defined in Proarrow.Category.Bicategory.Adj type IsOb Tight ('AK ps :: ADJK i j) = IsTight ps
type IsOb Cotight (p :: STT' k i j) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful type IsOb Cotight (p :: STT' k i j) = IsReader (UN ('ST :: (k +-> k) -> STT' k i j) p)
type IsOb Tight (p :: STT' k i j) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful type IsOb Tight (p :: STT' k i j) = IsWriter (UN ('ST :: (k +-> k) -> STT' k i j) p)
type IsOb Cotight ('MK a :: MonK k i j) Source Github #
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 Github #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type IsOb Tight ('MK a :: MonK k i j) = ()
type IsOb Cotight (p :: COK kk i j) Source Github #
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 Github #
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 Github #
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 Github #
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 Github #
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 Github #
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 j k3) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.Product type IsOb Cotight (p :: PRODK jj kk j k3) = (IsOb Cotight (PRODFST p), IsOb Cotight (PRODSND p))
type IsOb Tight (p :: PRODK jj kk j k3) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.Product type IsOb Tight (p :: PRODK jj kk j k3) = (IsOb Tight (PRODFST p), IsOb Tight (PRODSND p))

class WithObO2 tag (kk :: s -> s -> Type) where Source Github #

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

Instances

Instances details

WithObO2 Cotight ADJK Source Github #
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 Github #
WithObO2 Tight ADJK Source Github #
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 Github #
WithObO2 Cotight PROFK Source Github #
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 Github #
WithObO2 Tight PROFK Source Github #
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 Github #
Monoidal k => WithObO2 Cotight (MonK k :: () -> () -> Type) Source Github #
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 Github #
SymMonoidal k => WithObO2 Cotight (STT' k :: () -> () -> Type) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful Methods withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' k j k0) (b :: STT' 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 Github #
Monoidal k => WithObO2 Tight (MonK k :: () -> () -> Type) Source Github #
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 Github #
SymMonoidal k => WithObO2 Tight (STT' k :: () -> () -> Type) Source Github #
Instance details Defined in Proarrow.Category.Equipment.Stateful Methods withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: STT' k j k0) (b :: STT' 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 Github #
WithObO2 Tight kk => WithObO2 Cotight (COK kk :: s -> s -> Type) Source Github #
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 Github #
WithObO2 Tight kk => WithObO2 Cotight (OPK kk :: s -> s -> Type) Source Github #
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 Github #
WithObO2 Cotight kk => WithObO2 Tight (COK kk :: s -> s -> Type) Source Github #
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 Github #
WithObO2 Cotight kk => WithObO2 Tight (OPK kk :: s -> s -> Type) Source Github #
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 Github #
WithObO2 tag kk => WithObO2 tag (Path kk :: s -> s -> Type) Source Github #
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 Github #
(WithObO2 Cotight jj, WithObO2 Cotight kk) => WithObO2 Cotight (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Github #
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 Github #
(WithObO2 Tight jj, WithObO2 Tight kk) => WithObO2 Tight (PRODK jj kk :: (j, k) -> (j, k) -> Type) Source Github #
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 Github #

class (IsTight f, IsCotight g, Adjunction f g) => TightPair (f :: kk c d) (g :: kk d c) Source Github #

Instances

Instances details

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