module Equality where

open import Agda.Builtin.Equality public
open import Level

subst :
  {ℓ ℓ' : Level}
  {A  : Set ℓ}
  (B : A → Set ℓ')
  {x y : A}
  (p : x ≡ y)
  → --------------
  B x → B y
subst B refl b = b

substcong :
  {ℓ ℓ' : Level}
  {A  : Set ℓ}
  (B : A → Set ℓ')
  {x y : A}
  (p q : x ≡ y)
  {b : B x}
  → -------------------------------------
  (_ : p ≡ q) → subst B p b ≡ subst B q b
substcong B refl refl _ = refl

subst₂ :
  {ℓ ℓ' : Level}
  {A  A' : Set ℓ}
  (B : A → A' → Set ℓ')
  {x y  : A}
  {x' y' : A'}
  (p : x ≡ y)
  (p' : x' ≡ y')
  → ------------------
  B x x' → B y y'
subst₂ _ refl refl = λ b → b

coe :
  {ℓ : Level}
  {A B : Set ℓ}
  → -----------
  A ≡ B → A → B
coe refl x = x

trans :
  {ℓ : Level}
  {A : Set ℓ}
  {x y z : A}
  (q : y ≡ z)
  (p : x ≡ y)
  → ---------
  x ≡ z
trans refl p = p

symm :
  {ℓ : Level}
  {A : Set ℓ}
  {x y : A}
  (p : x ≡ y)
  → ---------
  y ≡ x
symm refl = refl

cong :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  {B : Set ℓ'}
  (f : A → B)
  {x y : A}
  (p : x ≡ y)
  → -----------
  f x ≡ f y
cong _ refl = refl

cong₂ :
  {ℓ ℓ' : Level}
  {A A' : Set ℓ}
  {B : Set ℓ'}
  (f : A → A' → B)
  {x y  : A}
  {x' y' : A'}
  (p : x ≡ y)
  (q : x' ≡ y')
  → --------------
  f x x' ≡ f y y'
cong₂ _ refl refl = refl

cong₃ :
  {ℓ ℓ' : Level}
  {A A' A'' : Set ℓ}
  {B : Set ℓ'}
  (f : A → A' → A'' → B)
  {x y : A}
  {x' y' : A'}
  {x'' y'' : A''}
  (p : x ≡ y)
  (q : x' ≡ y')
  (r : x'' ≡ y'')
  → ---------------------
  f x x' x'' ≡ f y y' y''
cong₃ _ refl refl refl = refl

infix  [_]_≡_over_
[_]_≡_over_ :
  {ℓ ℓ' : Level}
  {A : Set ℓ}
  (B : A → Set ℓ')
  {x y : A}
  (a : B x)
  (b : B y)
  (p : x ≡ y)
  → ----------
  Set ℓ'
[ B ] a ≡ b over refl = a ≡ b