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

private
  variable
    ℓ ℓ′ : Level

data _≡_ {T : Set ℓ} : T -> T -> Set ℓ where
  refl : {x : T} -> x ≡ x

infix  _≡_


{-# BUILTIN EQUALITY _≡_ #-}

≡-elim : {A : Set ℓ} {B : A -> A -> Set ℓ′} {x y : A} -> (x ≡ y) -> ((x : A) -> B x x) -> B x y
≡-elim {x = x} refl f = f x

sym : {A : Set ℓ} {x y : A} -> x ≡ y -> y ≡ x
sym refl = refl

cong : { A : Set ℓ} -> {B : Set ℓ′} -> {x₁ x₂ : A} -> (f : A -> B) -> x₁ ≡ x₂ -> f x₁ ≡ f x₂
cong f refl = refl

_<≡>_ : {A : Set ℓ} {B : Set ℓ′} {x y : A} -> {f g : A -> B} -> f ≡ g -> x ≡ y -> f x ≡ g y
refl <≡> refl = refl

infixl  _<≡>_

pure≡ : {A : Set ℓ} (x : A) -> x ≡ x
pure≡ x = refl

_→←_ : {A : Set ℓ} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
refl →← refl = refl

infixl  _→←_

transp : {A B : Set ℓ} -> A ≡ B -> A -> B
transp refl x = x

subst : {A : Set ℓ} (B : A -> Set ℓ′) {x y : A} (eq : x ≡ y) -> B x -> B y
subst B refl x = x

case≡_of_ : {A : Set ℓ} {B : Set ℓ′}
  -> (x : A)
  -> ((y : A) -> x ≡ y -> B)
  -> B
case≡ s of f = f s refl

_∎ : {T : Set ℓ} (l : T) -> l ≡ l
_∎ v = refl

_≡⟨⟩_ : {T : Set ℓ} -> {b : T} -> (a : T) -> a ≡ b -> a ≡ b
l ≡⟨⟩ r = r

_≡⟨_⟩_ : {T : Set ℓ} ->
  {b c : T} ->
  (a : T) ->
  a ≡ b ->
  b ≡ c ->
  a ≡ c
_≡⟨_⟩_ {c = c} l j r = j →← r


infix  _∎
infixr  _≡⟨⟩_ _≡⟨_⟩_