
  0 | module Data.Container.Category
  1 | 
  2 | import public Data.Category
  3 | import public Data.Container
  4 | import public Data.Container.Morphism
  5 | import public Data.Container.Morphism.Eq
  6 | 
  7 | import Proofs.Extensionality
  8 | 
  9 | ---------------------------------------------------------------------------------------------------
 10 | -- Containers form a category                                                                    --
 11 | ---------------------------------------------------------------------------------------------------
 12 | 
 13 | -- Composition respects identity on the right
 14 | composeIdRight : (f : a =%> b) -> f ⨾ Morphism.identity = f
 15 | composeIdRight (fwd <| bwd) = Refl
 16 | 
 17 | -- Composition respects identity on the left
 18 | composeIdLeft : (f : a =%> b) -> Morphism.identity ⨾ f = f
 19 | composeIdLeft (fwd <| bwd) = Refl
 20 | 
 21 | -- Composition is associative
 22 | proveAssoc : (f : a =%> b) -> (g : b =%> c) -> (h : c =%> d) ->
 23 |              f ⨾ (g ⨾ h) = (f ⨾ g) ⨾ h
 24 | proveAssoc (fwd0 <| bwd0) (fwd1 <| bwd1) (fwd2 <| bwd2) = Refl
 25 | 
 26 | -- The category of containers with dependent lenses as morphisms
 27 | public export
 28 | Cont : Category Container
 29 | Cont = MkCategory
 30 |   (=%>)
 31 |   (\_ => Morphism.identity)
 32 |   (⨾)
 33 |   composeIdRight
 34 |   composeIdLeft
 35 |   proveAssoc
 36 | 
 37 |