Leibnizian.idr

data Equal: (a : k) -> (b : k) -> Type where
  MkEqual : ({f : k -> Type} -> f a -> f b) -> Equal a b

subst : {f : k -> Type} -> Equal a b -> f a -> f b
subst (MkEqual ab) fa = ab fa

refl' : Equal a a
refl' = MkEqual id

sym' : Equal a b -> Equal b a
sym' ab = subst {f=\x => Equal x a} ab refl'

rewrite' : (f : k1 -> k2) -> Equal a b -> Equal (f a) (f b)
rewrite' f ab = subst {f=\x => Equal (f a) (f x)} ab refl'

toEq : Equal a b -> a = b
toEq ab = subst {f=\x => a = x} ab Refl

fromEq : a = b -> Equal a b
fromEq Refl = refl'

plus_0 : (n : Nat) -> Equal n (plus n Z)
plus_0 Z = refl'
plus_0 (S k) = rewrite' (\x => S x) (plus_0 k)

plus_commutes : (n : Nat) -> (m : Nat) -> Equal (n + m) (m + n)
plus_commutes Z m = plus_0 m
plus_commutes (S k) m = ?case2