module Algebra.Equivalence
import Builtin
%default total
public export
interface Equivalence t where
  Equiv : (a, b : t) -> Type
  decEquiv : (a, b : t) -> Dec (Equiv a b)

import Algebra.Equivalence

data BooleanEquiv : (a, b : Boolean) -> Type where
  BothFalse : BooleanEquiv False False
  BothTrue  : BooleanEquiv True  True
public export
Uninhabited (BooleanEquiv False True) where
  uninhabited BothFalse impossible
  uninhabited BothTrue  impossible
public export
Uninhabited (BooleanEquiv True False) where
  uninhabited BothFalse impossible
  uninhabited BothTrue  impossible
public export
Equivalence Boolean where
  Equiv = BooleanEquiv

  decEquiv False False = Yes $ BothFalse
  decEquiv True  True  = Yes $ BothTrue
  decEquiv False True  = No  $ absurd
  decEquiv True  False = No  $ absurd

public export
decToBoolean : Dec t -> Boolean
decToBoolean (Yes _) = True
decToBoolean (No  _) = False

import Builtin

import Algebra.Equivalence

data OptionalEquiv : (a, b : Optional t) -> Type where
  BothNothing : OptionalEquiv Nothing Nothing
  BothSame : Equivalence t => {a, b : t} -> (ok : Equiv a b) -> OptionalEquiv (Some a) (Some b)
public export
Uninhabited (OptionalEquiv Nothing (Some b)) where
  uninhabited BothNothing  impossible
  uninhabited (BothSame _) impossible
public export
Uninhabited (OptionalEquiv (Some a) Nothing) where
  uninhabited BothNothing  impossible
  uninhabited (BothSame _) impossible
public export
fromNotEquiv : Equivalence t => {a, b : t} -> (ok : Not (Equiv a b)) -> Not (OptionalEquiv (Some a) (Some b))
fromNotEquiv ok BothNothing impossible
fromNotEquiv ok (BothSame ctr) = ?ctra
public export
Equivalence t => Equivalence (Optional t) where
  Equiv = OptionalEquiv
  decEquiv Nothing  Nothing  = Yes $ BothNothing
  decEquiv Nothing  (Some _) = No $ absurd
  decEquiv (Some _) Nothing  = No $ absurd
  decEquiv (Some a) (Some b) with (decEquiv a b)
    decEquiv (Some a) (Some b) | (Yes prf) = Yes $ BothSame prf
    decEquiv (Some a) (Some b) | (No ctra) = No $ fromNotEquiv ctra

	, Algebra.Equivalence