
  0 | module Data.Iso
  1 | 
  2 | import Control.Relation
  3 | import Control.Order
  4 | 
  5 | -- an abstract implementation of Iso for any preorder relation
  6 | public export
  7 | record GenIso (carrier : Type)
  8 |               (mor : Rel carrier)
  9 |               (rel : {0 x, y : carrier} -> Rel (mor x y))
 10 |               {auto pre : Preorder carrier mor}
 11 |               (left, right : carrier) where
 12 |   constructor MkGenIso
 13 |   to : mor left right
 14 |   from : mor right left
 15 |   0 toFrom : rel (transitive to from) Relation.reflexive
 16 |   0 fromTo : rel (transitive from to) Relation.reflexive
 17 | 
 18 | -- a special case of `GenIso` for functions and types with equality
 19 | public export
 20 | record Iso (left, right : Type) where
 21 |   constructor MkIso
 22 |   to : left -> right
 23 |   from : right -> left
 24 |   0 toFrom : (x : right) -> to (from x) = x
 25 |   0 fromTo : (x : left) -> from (to x) = x
 26 | 
 27 |