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 1 [_]_≡_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