Documentation
Auto
.
Lib
.
HEqExtra
Search
return to top
source
Imports
Init
Imported by
Auto
.
heq_of_cast_eq
Auto
.
HEq
.
tyEq
Auto
.
HEq
.
funext
Auto
.
congr_heq
Auto
.
congr_h_heq
Auto
.
congr₂_h_heq
Auto
.
congr_hd_heq
Auto
.
congr_arg_heq
Auto
.
congr_fun_heq
Auto
.
heq_of_eqRec_eq'
Auto
.
eq_sigma_of_heq
Auto
.
heq_of_eq_sigma
Auto
.
eqRec_heq'
Auto
.
congr_arg₂_heq
source
theorem
Auto
.
heq_of_cast_eq
{
α
β
:
Sort
u_1}
{
a
:
α
}
{
a'
:
β
}
(
e
:
α
=
β
)
:
cast
e
a
=
a'
→
a
≍
a'
source
def
Auto
.
HEq
.
tyEq
{
α
β
:
Sort
u}
(
x
:
α
)
(
y
:
β
)
(
H
:
x
≍
y
)
:
α
=
β
Equations
⋯
=
⋯
Instances For
source
def
Auto
.
HEq
.
funext
{
γ
:
Sort
u}
{
α
β
:
γ
→
Sort
v
}
(
x
:
(
u
:
γ
) →
α
u
)
(
y
:
(
u
:
γ
) →
β
u
)
(
H
:
∀ (
u
:
γ
),
x
u
≍
y
u
)
:
x
≍
y
Equations
⋯
=
⋯
Instances For
source
theorem
Auto
.
congr_heq
{
α
β
:
Sort
u_1}
{
γ
:
Sort
u_2}
{
f
:
α
→
γ
}
{
g
:
β
→
γ
}
{
x
:
α
}
{
y
:
β
}
(
h₁
:
f
≍
g
)
(
h₂
:
x
≍
y
)
:
f
x
=
g
y
source
theorem
Auto
.
congr_h_heq
{
α₁
:
Sort
u_1}
{
β₁
:
Sort
u_2}
{
α₂
:
Sort
u_1}
{
β₂
:
Sort
u_2}
{
f₁
:
α₁
→
β₁
}
{
f₂
:
α₂
→
β₂
}
{
x₁
:
α₁
}
{
x₂
:
α₂
}
(
Hβ
:
β₁
=
β₂
)
(
h₁
:
f₁
≍
f₂
)
(
h₂
:
x₁
≍
x₂
)
:
f₁
x₁
≍
f₂
x₂
source
theorem
Auto
.
congr₂_h_heq
{
α₁
:
Sort
u_1}
{
β₁
:
Sort
u_2}
{
γ₁
:
Sort
u_3}
{
α₂
:
Sort
u_1}
{
β₂
:
Sort
u_2}
{
γ₂
:
Sort
u_3}
{
f₁
:
α₁
→
β₁
→
γ₁
}
{
f₂
:
α₂
→
β₂
→
γ₂
}
{
x₁
:
α₁
}
{
x₂
:
α₂
}
{
y₁
:
β₁
}
{
y₂
:
β₂
}
(
Hγ
:
γ₁
=
γ₂
)
(
h₁
:
f₁
≍
f₂
)
(
h₂
:
x₁
≍
x₂
)
(
h₃
:
y₁
≍
y₂
)
:
f₁
x₁
y₁
≍
f₂
x₂
y₂
source
theorem
Auto
.
congr_hd_heq
{
α₁
α₂
:
Sort
u_1}
{
β₁
:
α₁
→
Sort
u
}
{
β₂
:
α₂
→
Sort
u
}
{
f₁
:
(
x
:
α₁
) →
β₁
x
}
{
f₂
:
(
x
:
α₂
) →
β₂
x
}
{
x₁
:
α₁
}
{
x₂
:
α₂
}
(
Hβ
:
β₁
≍
β₂
)
(
h₁
:
f₁
≍
f₂
)
(
h₂
:
x₁
≍
x₂
)
:
f₁
x₁
≍
f₂
x₂
source
theorem
Auto
.
congr_arg_heq
{
α
:
Sort
u_1}
{
β
:
α
→
Sort
u_2
}
(
f
:
(
a
:
α
) →
β
a
)
{
a₁
a₂
:
α
}
:
a₁
=
a₂
→
f
a₁
≍
f
a₂
source
theorem
Auto
.
congr_fun_heq
{
α
:
Sort
u_1}
{
β₁
β₂
:
α
→
Sort
u_2
}
{
f₁
:
(
a
:
α
) →
β₁
a
}
{
f₂
:
(
a
:
α
) →
β₂
a
}
{
x₁
x₂
:
α
}
(
hβ
:
β₁
=
β₂
)
(
h₁
:
f₁
≍
f₂
)
(
h₂
:
x₁
=
x₂
)
:
f₁
x₁
≍
f₂
x₂
source
theorem
Auto
.
heq_of_eqRec_eq'
{
γ
:
Sort
u_1}
{
motive
:
γ
→
Sort
u
}
{
α
β
:
γ
}
(
h₁
:
α
=
β
)
(
a
:
motive
α
)
:
a
≍
h₁
▸
a
source
theorem
Auto
.
eq_sigma_of_heq
{
α
:
Type
u_1}
{
p
:
α
→
Type
v
}
{
ty₁
ty₂
:
α
}
{
val₁
:
p
ty₁
}
{
val₂
:
p
ty₂
}
(
h₁
:
ty₁
=
ty₂
)
(
h₂
:
val₁
≍
val₂
)
:
⟨
ty₁
,
val₁
⟩
=
⟨
ty₂
,
val₂
⟩
source
theorem
Auto
.
heq_of_eq_sigma
{
α
:
Type
u_1}
{
p
:
α
→
Type
v
}
{
ty₁
ty₂
:
α
}
{
val₁
:
p
ty₁
}
{
val₂
:
p
ty₂
}
(
h
:
⟨
ty₁
,
val₁
⟩
=
⟨
ty₂
,
val₂
⟩
)
:
ty₁
=
ty₂
∧
val₁
≍
val₂
source
theorem
Auto
.
eqRec_heq'
{
α
:
Sort
u_1}
{
a'
:
α
}
{
motive
:
(
a
:
α
) →
a'
=
a
→
Sort
u
}
(
p
:
motive
a'
⋯
)
{
a
:
α
}
(
t
:
a'
=
a
)
:
t
▸
p
≍
p
source
theorem
Auto
.
congr_arg₂_heq
{
α
:
Sort
u_1}
{
β
:
α
→
Sort
u_2
}
(
γ
:
(
a
:
α
) →
β
a
→
Sort
u_3
)
(
f
:
(
a
:
α
) →
(
b
:
β
a
) →
γ
a
b
)
{
a₁
a₂
:
α
}
{
b₁
:
β
a₁
}
{
b₂
:
β
a₂
}
(
H₁
:
a₁
=
a₂
)
(
H₂
:
b₁
≍
b₂
)
:
f
a₁
b₁
≍
f
a₂
b₂