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