Category.idr

Lemma

The identity lens is neutral when composed to the right.

composeIdRight : (f : a =%> b) -> f |%> identity b ≡ f
composeIdRight (fwd <! bwd) = Refl

Lemma

The identity lens is neutral when composed to the left.

composeIdLeft : (f : a =%> b) -> identity a |%> f ≡ f
composeIdLeft (fwd <! bwd) = Refl

Lemma

Composition of dependent lenses is associative.

proveAssoc : (f : a =%> b) -> (g : b =%> c) -> (h : c =%> d) ->
             f |%> (g |%> h) ≡ (f |%> g) |%> h
proveAssoc (fwd0 <! bwd0) (fwd1 <! bwd1) (fwd2 <! bwd2) = Refl

Proposition

Containers and dependent lenses form a category $\mathcal{C}ont$

Cont : Category Container
Cont = NewCat
  { objects = Container
  , morphisms = (=%>)
  , identity = (\x => identity x)
  , composition = (|%>)
  , identity_right = composeIdRight
  , identity_left = composeIdLeft
  , compose_assoc = proveAssoc
  }