Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Fam

Documentation

data FAM k Source Github #

Constructors

DEP_ (x +-> k)

Instances

Instances details

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Fam

Associated Types

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

Methods

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

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

Instance details

Defined in Proarrow.Category.Instance.Fam

Methods

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

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

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

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

lmap :: forall (c :: FAM k) (a :: FAM k) (b :: FAM k). (c ~> a) -> Fam a b -> Fam c b Source Github #

rmap :: forall (b :: FAM k) (d :: FAM k) (a :: FAM k). (b ~> d) -> Fam a b -> Fam a d Source Github #

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Fam

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

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fam

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

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fam

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

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fam

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Fam

type (a :: FAM k) || (b :: FAM k) = DEP (COPRODUCT (X a) (X b)) (Rep (Codiag :: COPRODUCT k k +-> k) :.: (DX a :++: DX b))

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

Instance details

Defined in Proarrow.Category.Instance.Fam

type (a :: FAM k) && (b :: FAM k) = DEP (X a, X b) (Corep (Diag :: k +-> (k, k)) :.: (DX a :**: DX b))

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

Instance details

Defined in Proarrow.Category.Instance.Fam

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

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

Equations

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

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

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

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

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 Github #
Instance details Defined in Proarrow.Category.Instance.Fam Methods id :: forall (a :: FAM k). Ob a => Fam a a Source Github # (.) :: forall (b :: FAM k) (c :: FAM k) (a :: FAM k). Fam b c -> Fam a b -> Fam a c Source Github #
CategoryOf k => Profunctor (Fam :: FAM k -> FAM k -> Type) Source Github #
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 Github # lmap :: forall (c :: FAM k) (a :: FAM k) (b :: FAM k). (c ~> a) -> Fam a b -> Fam c b Source Github # rmap :: forall (b :: FAM k) (d :: FAM k) (a :: FAM k). (b ~> d) -> Fam a b -> Fam a d Source Github # (\\) :: forall (a :: FAM k) (b :: FAM k) r. ((Ob a, Ob b) => r) -> Fam a b -> r Source Github #

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

Instances

Instances details

CategoryOf k => FunctorForRep (Embed :: k +-> FAM k) Source Github #
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 Github #
type (Embed :: k +-> FAM k) @ (a :: k) Source Github #
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 Github #

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

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

lmap :: forall (c :: k) (a :: k) (b :: ()). (c ~> a) -> AsPresheaf dx a b -> AsPresheaf dx c b Source Github #

rmap :: forall (b :: ()) (d :: ()) (a :: k). (b ~> d) -> AsPresheaf dx a b -> AsPresheaf dx a d Source Github #

(\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> AsPresheaf dx a b -> r Source Github #

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

Instances

Instances details

CategoryOf k => FunctorForRep (IsPresheafSub :: FAM k +-> Presheaf k) Source Github #
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 Github #
type (IsPresheafSub :: FAM k +-> Presheaf k) @ (DEP x dx :: FAM k) Source Github #
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 Github #

Instances

Instances details

CategoryOf k => FunctorForRep (Initiate :: VOID +-> k) Source Github #
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 Github #
type (Initiate :: VOID +-> k) @ (a :: VOID) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fam type (Initiate :: VOID +-> k) @ (a :: VOID) = Any :: k

type Poly = FAM (OPPOSITE Type) Source Github #