module Haskell.Law.Equality where
open import Haskell.Prim
open import Agda.Builtin.TrustMe
_≠_ : {A : Set} → A → A → Set
_≠_ a b = a ≡ b → ⊥
infix 4 _≠_
cong : {A B : Set} → ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl
cong₂ : ∀ (f : a → b → c) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
cong₂ f refl refl = refl
sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
subst : ∀ {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y
subst P refl z = z
trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
trustMe = primTrustMe
infix 1 begin_
infixr 2 _≡⟨⟩_ step-≡ step-≡˘
infix 3 _∎
begin_ : ∀{x y : a} → x ≡ y → x ≡ y
begin_ x≡y = x≡y
_≡⟨⟩_ : ∀ (x {y} : a) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y
step-≡ : ∀ (x {y z} : a) → y ≡ z → x ≡ y → x ≡ z
step-≡ _ y≡z x≡y = trans x≡y y≡z
step-≡˘ : ∀ (x {y z} : a) → y ≡ z → y ≡ x → x ≡ z
step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z
_∎ : ∀ (x : a) → x ≡ x
_∎ _ = refl
syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
subst0 : {@0 a : Set} (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
subst0 p refl z = z
{-# COMPILE AGDA2HS subst0 transparent #-}