Basic implementation of correct-by-construction bijections

Bijection.idr

module Bijection

%default total
%access public export

infixr 5 <=>

record (<=>) a p where
  constructor Biject
  ap : a -> p
  pa : p -> a
  left_inverse : (x : p) -> ap (pa x) = x
  right_inverse : (x : a) -> pa (ap x) = x

biid : a <=> a
biid = Biject id id (\_ => Refl) (\_ => Refl)

inversion_composes : (f : a -> b) -> (g : b -> a)
                   -> (h : b -> c) -> (i : c -> b)
                   -> ((x : b) -> f (g x) = x)
                   -> ((y : c) -> h (i y) = y)
                   -> (z : c)
                   -> h (f (g (i z))) = z
inversion_composes f g h i inv1 inv2 z =
  rewrite lemma in inv2 z where
    lemma : h (f (g (i z))) = h (i z)
    lemma = cong (inv1 (i z))

infix 5 =><=

(=><=) : a <=> b -> b <=> c -> a <=> c
(Biject f g p1 p2) =><= (Biject h i p3 p4) =
  Biject (h . f) (g . i) (inversion_composes f g h i p1 p3)
                         (inversion_composes i h g f p4 p2)