michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/lean/hott): add tele_eq example using HoTT library

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-22 09:43:16 -08:00
parent 1d79cb9c07
commit 264c88d332
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
tests/lean/hott/tele_eq.hlean Normal file
View file

@ -0,0 +1,18 @@
constant A₁ : Type
constant A₂ : A₁ → Type
constant A₃ : Π (a₁ : A₁), A₂ a₁ → Type
structure foo :=
mk :: (a₁ : A₁) (a₂ : A₂ a₁) (a₃ : A₃ a₁ a₂)
theorem foo.eq {a₁ b₁ : A₁} {a₂ : A₂ a₁} {b₂ : A₂ b₁} {a₃ : A₃ a₁ a₂} {b₃ : A₃ b₁ b₂}
(H₁ : a₁ = b₁) (H₂ : eq.rec_on H₁ a₂ = b₂) (H₃ : eq.rec_on H₂ (eq.rec_on H₁ a₃) = b₃)
: foo.mk a₁ a₂ a₃ = foo.mk b₁ b₂ b₃ :=
begin
cases H₁,
cases H₂,
cases H₃,
apply rfl
end
print definition foo.eq