Control.Category.Instances.Prod

This module defines the product of two categories.

Definitions

record Prod : (a -> b -> Type) -> (a' -> b' -> Type) -> (a, a') -> (b, b') -> Type

  The product category of two other categories.

Totality: total
Visibility: public export
Constructor: 

MkProd : cat (fst x) (fst y) -> cat' (snd x) (snd y) -> Prod cat cat' x y

Projections:

.fst : Prod cat cat' x y -> cat (fst x) (fst y)

.snd : Prod cat cat' x y -> cat' (snd x) (snd y)

Hints:

Category cat => Category cat' => Category (Prod cat cat')

Semigroupoid cat => Semigroupoid cat' => Semigroupoid (Prod cat cat')

.fst : Prod cat cat' x y -> cat (fst x) (fst y)

Totality: total
Visibility: public export

fst : Prod cat cat' x y -> cat (fst x) (fst y)

Totality: total
Visibility: public export

.snd : Prod cat cat' x y -> cat' (snd x) (snd y)

Totality: total
Visibility: public export

snd : Prod cat cat' x y -> cat' (snd x) (snd y)

Totality: total
Visibility: public export

Prod : SemigroupoidR -> SemigroupoidR -> SemigroupoidR

Totality: total
Visibility: public export

Prod : CategoryR -> CategoryR -> CategoryR

Totality: total
Visibility: public export

FunctorProd : FunctorR catF catF' -> FunctorR catG catG' -> FunctorR (Prod catF catG) (Prod catF' catG')

Totality: total
Visibility: public export