Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Fam

Documentation

data FAM k Source Comments #

Constructors

DEP_ (x +-> k)

Instances

Instances details

CategoryOf k => FunctorForRep (Embed :: k +-> FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

fmap :: forall (a :: k) (b :: k). (a ~> b) -> ((Embed :: k +-> FAM k) @ a) ~> ((Embed :: k +-> FAM k) @ b) Source Comments #

CategoryOf k => CategoryOf (FAM k) Source Comments #

The Fam construction a.k.a. the free coproduct completion of k

Instance details

Defined in Proarrow.Category.Instance.Fam

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Fam type (~>) = Fam :: FAM k -> FAM k -> Type

CategoryOf k => HasBinaryCoproducts (FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

withObCoprod :: forall (a :: FAM k) (b :: FAM k) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Comments #

lft :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => a ~> (a || b) Source Comments #

rgt :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => b ~> (a || b) Source Comments #

(|||) :: forall (x :: FAM k) (a :: FAM k) (y :: FAM k). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Comments #

(+++) :: forall (a :: FAM k) (b :: FAM k) (x :: FAM k) (y :: FAM k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Comments #

HasBinaryProducts k => HasBinaryProducts (FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

withObProd :: forall (a :: FAM k) (b :: FAM k) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Comments #

fst :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => (a && b) ~> a Source Comments #

snd :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => (a && b) ~> b Source Comments #

(&&&) :: forall (a :: FAM k) (x :: FAM k) (y :: FAM k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments #

(***) :: forall (a :: FAM k) (b :: FAM k) (x :: FAM k) (y :: FAM k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments #

CategoryOf k => HasInitialObject (FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Fam type InitialObject = DEP VOID (Rep (Initiate :: VOID +-> k))

Methods

initiate :: forall (a :: FAM k). Ob a => (InitialObject :: FAM k) ~> a Source Comments #

HasTerminalObject k => HasTerminalObject (FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Fam type TerminalObject = DEP () (Term :: k -> () -> Type)

Methods

terminate :: forall (a :: FAM k). Ob a => a ~> (TerminalObject :: FAM k) Source Comments #

CategoryOf k => Promonad (Fam :: FAM k -> FAM k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

id :: forall (a :: FAM k). Ob a => Fam a a Source Comments #

(.) :: forall (b :: FAM k) (c :: FAM k) (a :: FAM k). Fam b c -> Fam a b -> Fam a c Source Comments #

CategoryOf k => Profunctor (Fam :: FAM k -> FAM k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

dimap :: forall (c :: FAM k) (a :: FAM k) (b :: FAM k) (d :: FAM k). (c ~> a) -> (b ~> d) -> Fam a b -> Fam c d Source Comments #

(\\) :: forall (a :: FAM k) (b :: FAM k) r. ((Ob a, Ob b) => r) -> Fam a b -> r Source Comments #

CategoryOf k => FunctorForRep (IsPresheafSub :: FAM k +-> Presheaf k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

fmap :: forall (a :: FAM k) (b :: FAM k). (a ~> b) -> ((IsPresheafSub :: FAM k +-> Presheaf k) @ a) ~> ((IsPresheafSub :: FAM k +-> Presheaf k) @ b) Source Comments #

type (Embed :: k +-> FAM k) @ (a :: k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type (Embed :: k +-> FAM k) @ (a :: k) = DEP () (Constant a :: k -> () -> Type)

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type (~>) = Fam :: FAM k -> FAM k -> Type

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type InitialObject = DEP VOID (Rep (Initiate :: VOID +-> k))

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type TerminalObject = DEP () (Term :: k -> () -> Type)

type Ob (a :: FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type Ob (a :: FAM k) = (a ~ DEP (X a) (DX a), Representable (DX a))

type (a :: FAM k) || (b :: FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type (a :: FAM k) || (b :: FAM k) = DEP (COPRODUCT (X a) (X b)) (DX a :|||: DX b)

type (a :: FAM k) && (b :: FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type (a :: FAM k) && (b :: FAM k) = DEP (X a, X b) (DX a :&&: DX b)

type (IsPresheafSub :: FAM k +-> Presheaf k) @ (DEP x dx :: FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type (IsPresheafSub :: FAM k +-> Presheaf k) @ (DEP x dx :: FAM k) = AsPresheaf dx

type UN ('DEP_ :: (x +-> k) -> FAM k) ('DEP_ dx :: FAM k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fam

type UN ('DEP_ :: (x +-> k) -> FAM k) ('DEP_ dx :: FAM k) = dx

type family X (a :: FAM k) where ... Source Comments #

Equations

X ('DEP_ dx :: FAM k) = x

type DX (a :: FAM k) = UN ('DEP_ :: (X a +-> k) -> FAM k) a Source Comments #

type DEP x (dx :: x +-> k) = 'DEP_ dx Source Comments #

data Fam (a :: FAM k) (b :: FAM k) where Source Comments #

Constructors

Fam :: forall {k} {x} {y} {dx :: x +-> k} {dy :: y +-> k} (f :: x +-> y). (Representable dx, Representable dy, Representable f) => (dx :~> (dy :.: f)) -> Fam ('DEP_ dx) ('DEP_ dy)

Instances

Instances details

CategoryOf k => Promonad (Fam :: FAM k -> FAM k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods id :: forall (a :: FAM k). Ob a => Fam a a Source Comments # (.) :: forall (b :: FAM k) (c :: FAM k) (a :: FAM k). Fam b c -> Fam a b -> Fam a c Source Comments #
CategoryOf k => Profunctor (Fam :: FAM k -> FAM k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods dimap :: forall (c :: FAM k) (a :: FAM k) (b :: FAM k) (d :: FAM k). (c ~> a) -> (b ~> d) -> Fam a b -> Fam c d Source Comments # (\\) :: forall (a :: FAM k) (b :: FAM k) r. ((Ob a, Ob b) => r) -> Fam a b -> r Source Comments #

data family Embed :: k +-> FAM k Source Comments #

Instances

Instances details

CategoryOf k => FunctorForRep (Embed :: k +-> FAM k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods fmap :: forall (a :: k) (b :: k). (a ~> b) -> ((Embed :: k +-> FAM k) @ a) ~> ((Embed :: k +-> FAM k) @ b) Source Comments #
type (Embed :: k +-> FAM k) @ (a :: k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam type (Embed :: k +-> FAM k) @ (a :: k) = DEP () (Constant a :: k -> () -> Type)

data AsPresheaf (dx :: x +-> k) (a :: k) (u :: ()) where Source Comments #

Constructors

AsPresheaf :: forall {x} {k} (dx :: x +-> k) (a :: k) (b :: x). dx a b -> AsPresheaf dx a '()

Instances

Instances details

(CategoryOf k, Profunctor dx) => Profunctor (AsPresheaf dx :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()). (c ~> a) -> (b ~> d) -> AsPresheaf dx a b -> AsPresheaf dx c d Source Comments # (\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> AsPresheaf dx a b -> r Source Comments #

data family IsPresheafSub :: FAM k +-> Presheaf k Source Comments #

Instances

Instances details

CategoryOf k => FunctorForRep (IsPresheafSub :: FAM k +-> Presheaf k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods fmap :: forall (a :: FAM k) (b :: FAM k). (a ~> b) -> ((IsPresheafSub :: FAM k +-> Presheaf k) @ a) ~> ((IsPresheafSub :: FAM k +-> Presheaf k) @ b) Source Comments #
type (IsPresheafSub :: FAM k +-> Presheaf k) @ (DEP x dx :: FAM k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam type (IsPresheafSub :: FAM k +-> Presheaf k) @ (DEP x dx :: FAM k) = AsPresheaf dx

data Term (a :: k) (b :: ()) where Source Comments #

Constructors

Term :: forall {k} (a :: k). Ob a => Term a '()

Instances

Instances details

CategoryOf k => Profunctor (Term :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()). (c ~> a) -> (b ~> d) -> Term a b -> Term c d Source Comments # (\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> Term a b -> r Source Comments #
CategoryOf k => Corepresentable (Term :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods coindex :: forall (a :: k) (b :: ()). Term a b -> ((Term :: k -> () -> Type) %% a) ~> b Source Comments # cotabulate :: forall (a :: k) (b :: ()). Ob a => (((Term :: k -> () -> Type) %% a) ~> b) -> Term a b Source Comments # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((Term :: k -> () -> Type) %% a) ~> ((Term :: k -> () -> Type) %% b) Source Comments #
HasTerminalObject k => Representable (Term :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods index :: forall (a :: k) (b :: ()). Term a b -> a ~> ((Term :: k -> () -> Type) % b) Source Comments # tabulate :: forall (b :: ()) (a :: k). Ob b => (a ~> ((Term :: k -> () -> Type) % b)) -> Term a b Source Comments # repMap :: forall (a :: ()) (b :: ()). (a ~> b) -> ((Term :: k -> () -> Type) % a) ~> ((Term :: k -> () -> Type) % b) Source Comments #
type (Term :: k -> () -> Type) %% (a :: k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam type (Term :: k -> () -> Type) %% (a :: k) = '()
type (Term :: k -> () -> Type) % '() Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam type (Term :: k -> () -> Type) % '() = TerminalObject :: k

data ((p :: x +-> k) :&&: (q :: y +-> k)) (a :: k) (b :: (x, y)) where Source Comments #

Constructors

(:&&:) :: forall {x} {k} {y} (p :: x +-> k) (a :: k) (b1 :: x) (q :: y +-> k) (c :: y). p a b1 -> q a c -> (p :&&: q) a '(b1, c)

Instances

Instances details

(Profunctor l, Profunctor r, CategoryOf k) => Profunctor (l :&&: r :: k -> (x, y) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods dimap :: forall (c :: k) (a :: k) (b :: (x, y)) (d :: (x, y)). (c ~> a) -> (b ~> d) -> (l :&&: r) a b -> (l :&&: r) c d Source Comments # (\\) :: forall (a :: k) (b :: (x, y)) r0. ((Ob a, Ob b) => r0) -> (l :&&: r) a b -> r0 Source Comments #
(Corepresentable l, Corepresentable r, CategoryOf k) => Corepresentable (l :&&: r :: k -> (x, y) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods coindex :: forall (a :: k) (b :: (x, y)). (l :&&: r) a b -> ((l :&&: r) %% a) ~> b Source Comments # cotabulate :: forall (a :: k) (b :: (x, y)). Ob a => (((l :&&: r) %% a) ~> b) -> (l :&&: r) a b Source Comments # corepMap :: forall (a :: k) (b :: k). (a ~> b) -> ((l :&&: r) %% a) ~> ((l :&&: r) %% b) Source Comments #
(Representable l, Representable r, HasBinaryProducts k) => Representable (l :&&: r :: k -> (x, y) -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam Methods index :: forall (a :: k) (b :: (x, y)). (l :&&: r) a b -> a ~> ((l :&&: r) % b) Source Comments # tabulate :: forall (b :: (x, y)) (a :: k). Ob b => (a ~> ((l :&&: r) % b)) -> (l :&&: r) a b Source Comments # repMap :: forall (a :: (x, y)) (b :: (x, y)). (a ~> b) -> ((l :&&: r) % a) ~> ((l :&&: r) % b) Source Comments #
type (l :&&: r :: k -> (x, y) -> Type) %% (a :: k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam type (l :&&: r :: k -> (x, y) -> Type) %% (a :: k) = '(l %% a, r %% a)
type (l :&&: r :: k -> (x, y) -> Type) % ('(a, b) :: (x, y)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Fam type (l :&&: r :: k -> (x, y) -> Type) % ('(a, b) :: (x, y)) = (l % a) && (r % b)

type Poly = FAM (OPPOSITE Type) Source Comments #