module Eq where

open import Data.Fin
open import Data.Fin.Props


data Foo : Set where
  a b c : Foo

open import Data.Product
open import Relation.Binary.PropositionalEquality
I^-1 : (n : Fin 3) -> Foo
I^-1 zero = a 
I^-1 (suc zero) = b 
I^-1 (suc (suc zero)) = c 
I^-1 (suc (suc (suc ())))
I' : (x : Foo) -> Σ (Fin 3) \ n -> I^-1 n ≡ x
I' a = zero , refl
I' b = suc zero , refl
I' c = suc (suc zero) , refl

I : Foo -> Fin 3
I x = proj₁ (I' x)

I-inj : ∀ {x y} -> I x ≡ I y -> x ≡ y
I-inj eq = trans (sym (proj₂ (I' _))) (trans (cong I^-1 eq) (proj₂ (I' _)))
open import Relation.Nullary
open import Relation.Nullary.Decidable

dec : (x y : Foo) -> Dec (x ≡ y)
dec x y with (I x) ≟ (I y)
dec x y | yes p = yes (I-inj p)
dec x y | no ¬p = no (λ x' → ¬p (cong I x'))