{-# OPTIONS --cubical-compatible #-}
module Terra.Classes.Eq where
open import Terra.Data.Equality
open import Terra.Data.Decision
open import Terra.Data.Level
open import Terra.Data.Negation

private
  variable
    ℓ : Level

-- J'ai pas besoin que ce soit un record, je peux juste utiliser l'égalité
-- décidable. J'en ai besoin, sinon les contraintes de types sont impossibles à
-- recevoir par une instance (a, b -> Decision (a ≡ b)) fonctione pas.

record Eq (A : Set ℓ) : Set ℓ where
  field
   _≟_ : (x y : A) -> Decision (x ≡ y)
  _≠_ : (x y : A) -> Decision (¬(x ≡ y))
  l ≠ r with l ≟ r
  ... | yes x = no λ f → f x
  ... | no x = yes λ x₁ → x x₁

open Eq {{...}} public