Data.Boundary

A boundary is a pair of types, they are the object of the category of lenses

Definitions

record Boundary : Type

  Type boundaries

Totality: total
Visibility: public export
Constructor: 

MkB : Type -> Type -> Boundary

Projections:

.proj1 : Boundary -> Type

.proj2 : Boundary -> Type

.proj1 : Boundary -> Type

Totality: total
Visibility: public export

proj1 : Boundary -> Type

Totality: total
Visibility: public export

.proj2 : Boundary -> Type

Totality: total
Visibility: public export

proj2 : Boundary -> Type

Totality: total
Visibility: public export

.π1 : Boundary -> Type

  First projection of a boundary

Totality: total
Visibility: public export

.π2 : Boundary -> Type

  Second projection of a boundary

Totality: total
Visibility: public export

cartesian : Boundary -> Boundary -> Boundary

  Cartesian product of two boundaries
  cartesian (a , b) (c, d) = (a * c, b * d)

Totality: total
Visibility: public export

Dup : Type -> Boundary

  Build a boundary out of a single type

Totality: total
Visibility: public export

BUnit : Boundary

  The unit boundary is a pair of units

Totality: total
Visibility: public export

cocartesian : Boundary -> Boundary -> Boundary

  Cocartesian product of boundaries
  cocartesian (a, b) (c, d) = (a + c, b + d)

Totality: total
Visibility: public export