module test where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe

open import Data.Nat
open import Data.Nat.Properties
open import Function
open import Algebra.Structures 

-- the primUnsafeTrustMe primitive
private
 primitive
   primUnsafeTrustMe : {A : Set}{a b : A} → a ≡ b

-- function extensionality axiom using primUnsafeTrustMe
ext : ∀ {A} {B} → {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
ext _ = primUnsafeTrustMe

-- some test code: two definitionally unequal functions
f₁ : ℕ → ℕ
f₁ = id

f₂ : ℕ → ℕ
f₂ n = 0 + n

-- a proof of equality using function extensionality
p : f₁ ≡ f₂
p = ext identityˡ
  where open IsCommutativeSemiring (isCommutativeSemiring)
        open IsCommutativeMonoid (+-isCommutativeMonoid)


-- a function to test canonicity
useP′ : {A : Set} {a b : A} → a ≡ b → ℕ
useP′ {_} {.a} {a} refl = 0

-- canonicity is ok, since the following reduces
test′ = useP′ p