
  0 | ||| A boundary is a pair of types, they are the object of the category of lenses
  1 | module Data.Boundary
  2 | 
  3 | %default total
  4 | 
  5 | ||| Type boundaries
  6 | public export
  7 | record Boundary where
  8 |   constructor MkB
  9 |   proj1 : Type
 10 |   proj2 : Type
 11 | 
 12 | ||| First projection of a boundary
 13 | public export
 14 | (.π1) : Boundary -> Type
 15 | (.π1) = proj1
 16 | 
 17 | ||| Second projection of a boundary
 18 | public export
 19 | (.π2) : Boundary -> Type
 20 | (.π2) = proj2
 21 | 
 22 | ||| Cartesian product of two boundaries
 23 | ||| cartesian (a , b) (c, d) = (a * c, b * d)
 24 | public export
 25 | cartesian : Boundary -> Boundary -> Boundary
 26 | cartesian a b = (MkB (a.proj1, b.proj1) (a.proj2, b.proj2))
 27 | 
 28 | ||| Build a boundary out of a single type
 29 | public export
 30 | Dup : Type -> Boundary
 31 | Dup ty = MkB ty ty
 32 | 
 33 | ||| The unit boundary is a pair of units
 34 | public export
 35 | BUnit : Boundary
 36 | BUnit = MkB Unit Unit
 37 | 
 38 | ||| Cocartesian product of boundaries
 39 | ||| cocartesian (a, b) (c, d) = (a + c, b + d)
 40 | public export
 41 | cocartesian : Boundary -> Boundary -> Boundary
 42 | cocartesian a b = MkB (Either a.proj1 b.proj1) (Either a.proj2 b.proj2)
 43 |