proarrow
Safe HaskellNone
LanguageGHC2024

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 () (Rep (Constant a))
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 () (Rep (Constant a))

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 family Initiate :: VOID +-> k Source Comments #

Instances

Instances details
CategoryOf k => FunctorForRep (Initiate :: VOID +-> k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

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

type (Initiate :: VOID +-> k) @ (a :: VOID) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

type (Initiate :: VOID +-> k) @ (a :: VOID) = Any :: k

data family LftCat :: j +-> COPRODUCT j k Source Comments #

Instances

Instances details
(CategoryOf j, CategoryOf k) => FunctorForRep (LftCat :: j +-> COPRODUCT j k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

fmap :: forall (a :: j) (b :: j). (a ~> b) -> ((LftCat :: j +-> COPRODUCT j k) @ a) ~> ((LftCat :: j +-> COPRODUCT j k) @ b) Source Comments #

type (LftCat :: j +-> COPRODUCT j k) @ (a :: j) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

type (LftCat :: j +-> COPRODUCT j k) @ (a :: j) = 'L a :: COPRODUCT j k

data family RgtCat :: k +-> COPRODUCT j k Source Comments #

Instances

Instances details
(CategoryOf j, CategoryOf k) => FunctorForRep (RgtCat :: k +-> COPRODUCT j k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

fmap :: forall (a :: k) (b :: k). (a ~> b) -> ((RgtCat :: k +-> COPRODUCT j k) @ a) ~> ((RgtCat :: k +-> COPRODUCT j k) @ b) Source Comments #

type (RgtCat :: k +-> COPRODUCT j k) @ (a :: k) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

type (RgtCat :: k +-> COPRODUCT j k) @ (a :: k) = 'R a :: COPRODUCT j k

data ((p :: i +-> k) :|||: (q :: j +-> k)) (a :: k) (b :: COPRODUCT i j) where Source Comments #

Constructors

InjLP :: forall {i} {k} {j} (p :: i +-> k) (a :: k) (b1 :: i) (q :: j +-> k). p a b1 -> (p :|||: q) a ('L b1 :: COPRODUCT i j) 
InjRP :: forall {j} {k} {i} (q :: j +-> k) (a :: k) (b1 :: j) (p :: i +-> k). q a b1 -> (p :|||: q) a ('R b1 :: COPRODUCT i j) 

Instances

Instances details
(Profunctor p, Profunctor q) => Profunctor (p :|||: q :: k -> COPRODUCT i j -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

dimap :: forall (c :: k) (a :: k) (b :: COPRODUCT i j) (d :: COPRODUCT i j). (c ~> a) -> (b ~> d) -> (p :|||: q) a b -> (p :|||: q) c d Source Comments #

(\\) :: forall (a :: k) (b :: COPRODUCT i j) r. ((Ob a, Ob b) => r) -> (p :|||: q) a b -> r Source Comments #

(Representable p, Representable q) => Representable (p :|||: q :: k -> COPRODUCT i j -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

index :: forall (a :: k) (b :: COPRODUCT i j). (p :|||: q) a b -> a ~> ((p :|||: q) % b) Source Comments #

tabulate :: forall (b :: COPRODUCT i j) (a :: k). Ob b => (a ~> ((p :|||: q) % b)) -> (p :|||: q) a b Source Comments #

repMap :: forall (a :: COPRODUCT i j) (b :: COPRODUCT i j). (a ~> b) -> ((p :|||: q) % a) ~> ((p :|||: q) % b) Source Comments #

type (p :|||: q :: k -> COPRODUCT i j -> Type) % ('L a :: COPRODUCT i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

type (p :|||: q :: k -> COPRODUCT i j -> Type) % ('L a :: COPRODUCT i j) = p % a
type (p :|||: q :: k -> COPRODUCT i j -> Type) % ('R a :: COPRODUCT i j) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

type (p :|||: q :: k -> COPRODUCT i j -> Type) % ('R a :: COPRODUCT i j) = q % a

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) % (ab :: (x, y)) Source Comments # 
Instance details

Defined in Proarrow.Category.Instance.Fam

type (l :&&: r :: k -> (x, y) -> Type) % (ab :: (x, y)) = (l % Fst ab) && (r % Snd ab)

type Poly = FAM (OPPOSITE Type) Source Comments #