
  0 | module Data.Container.Morphism.Eq
  1 | 
  2 | import public Proofs.Congruence
  3 | import public Proofs.Extensionality
  4 | 
  5 | import public Control.Relation
  6 | import public Control.Order
  7 | 
  8 | import Data.Container.Morphism
  9 | import Data.Iso
 10 | 
 11 | public export infix 0 `DepLensEq`
 12 | 
 13 | ||| Two container morphisms are equal if their mapping on shapes are equal and their
 14 | ||| mapping on positions are equal.
 15 | public export
 16 | record DepLensEq (a, b : dom =%> cod) where
 17 |   constructor MkDepLensEq
 18 |   0 eqFwd : (v : dom.req) -> a.fwd v === b.fwd v
 19 |   0 eqBwd : (v : dom.req) -> (y : cod.res (a.fwd v)) ->
 20 |           let 0 p1 : dom.res v
 21 |               p1 = a.bwd v y
 22 |               0 p2 : dom.res v
 23 |               p2 = b.bwd v (replace {p = cod.res} (eqFwd v) y)
 24 |           in p1 === p2
 25 | export
 26 | 0 depLensEqToEq : DepLensEq a b -> a === b
 27 | depLensEqToEq {a = (fwd1 <| bwd1)} {b = (fwd2 <| bwd2)} (MkDepLensEq eqFwd eqBwd) =
 28 |   cong2Dep (<|) (funExt eqFwd) (funExtDep $ \x => funExt $ \y => eqBwd x y)
 29 | 
 30 | public export
 31 | Transitive (dom =%> cod) DepLensEq where
 32 |   transitive a b = MkDepLensEq (\v => transitive (a.eqFwd v) (b.eqFwd v))
 33 |       (\v, w => transitive
 34 |            (a.eqBwd v w)
 35 |            (b.eqBwd v (replace {p = cod.res} (a.eqFwd v) w)))
 36 | 
 37 | public export
 38 | Reflexive (dom =%> cod) DepLensEq where
 39 |   reflexive = MkDepLensEq (\_ => Refl) (\_, _ => Refl)
 40 | 
 41 | public export
 42 | Preorder (dom =%> cod) DepLensEq where
 43 | 
 44 | ||| An isomorphism of container morphisms
 45 | public export
 46 | ContIso : (x, y : Container) -> Type
 47 | ContIso = GenIso Container (=%>) DepLensEq
 48 |