max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/hott): delete old HoTT tests

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-17 12:25:25 -07:00
parent 5e8f2add84
commit 29b35ef12d
70 changed files with 0 additions and 2647 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/shell/CMakeLists.txt
View file

@ -83,15 +83,6 @@ ENDFOREACH(T)
# COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
# ENDFOREACH(T)
# # LEAN HoTT TESTS
# file(GLOB LEANHTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.hlean")
# FOREACH(T ${LEANHTESTS})
# GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
# add_test(NAME "leanhtest_${T_NAME}"
# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
# COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
# ENDFOREACH(T)
# LEAN RUN TESTS
file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean")
FOREACH(T ${LEANRUNTESTS})
@ -129,15 +120,6 @@ FOREACH(T ${LEANT0TESTS})
COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME} "-t 10")
ENDFOREACH(T)
# # LEAN RUN HoTT TESTS
# file(GLOB LEANRUNHTESTS "${LEAN_SOURCE_DIR}/../tests/lean/hott/*.hlean")
# FOREACH(T ${LEANRUNHTESTS})
# GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
# add_test(NAME "leanhotttest_${T_NAME}"
# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/hott"
# COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
# ENDFOREACH(T)
# The new elaborator needs to populate the info_manager for the following tests
# if("${MULTI_THREAD}" MATCHES "ON")
# # LEAN INTERACTIVE TESTS

986
tests/lean/expensive/transport.lean
View file

@ -1,986 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic
namespace N1
definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b
:= eq_rec H p
theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
:= refl H
opaque_hint (hiding transport)
theorem transport_proof_irrel {A : Type} {a b : A} {P : A → Type} (p1 p2 : a = b) (H : P a) : transport p1 H = transport p2 H
:= refl (transport p1 H)
theorem transport_eq {A : Type} {a : A} {P : A → Type} (p : a = a) (H : P a) : transport p H = H
:= calc transport p H = transport (refl a) H : transport_proof_irrel p (refl a) H
... = H : transport_refl H
theorem dcongr {A : Type} {B : A → Type} {a b : A} (f : Π x, B x) (p : a = b) : transport p (f a) = f b
:= have H1 : ∀ p1 : a = a, transport p1 (f a) = f a, from
assume p1 : a = a, transport_eq p1 (f a),
eq_rec H1 p p
theorem transport_trans {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
take p, calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans1 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans2 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans3 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans4 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans5 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans6 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans7 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans8 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans9 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans10 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans11 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans12 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans13 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans14 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans15 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans16 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans17 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans18 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans19 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans20 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans21 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans22 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans23 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans24 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans25 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans26 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans27 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans28 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans29 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
take p, calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans30 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans31 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans32 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans33 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans34 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans35 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans36 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans37 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans38 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans39 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans40 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans41 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans42 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans43 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans44 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans45 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans46 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans47 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans48 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans49 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans50 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans51 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans52 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans53 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans54 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans55 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans56 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans57 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans58 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
end
namespace N2
definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b
:= eq_rec H p
theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
:= refl H
opaque_hint (hiding transport)
theorem transport_proof_irrel {A : Type} {a b : A} {P : A → Type} (p1 p2 : a = b) (H : P a) : transport p1 H = transport p2 H
:= refl (transport p1 H)
theorem transport_eq {A : Type} {a : A} {P : A → Type} (p : a = a) (H : P a) : transport p H = H
:= calc transport p H = transport (refl a) H : transport_proof_irrel p (refl a) H
... = H : transport_refl H
theorem dcongr {A : Type} {B : A → Type} {a b : A} (f : Π x, B x) (p : a = b) : transport p (f a) = f b
:= have H1 : ∀ p1 : a = a, transport p1 (f a) = f a, from
assume p1 : a = a, transport_eq p1 (f a),
eq_rec H1 p p
theorem transport_trans {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
take p, calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans1 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans2 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans3 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans4 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans5 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans6 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans7 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans8 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans9 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans10 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans11 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans12 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans13 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans14 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans15 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans16 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans17 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans18 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans19 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans20 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans21 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans22 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans23 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans24 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans25 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans26 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans27 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans28 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans29 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
take p, calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans30 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans31 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans32 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans33 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans34 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans35 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans36 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans37 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans38 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans39 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans40 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans41 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans42 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans43 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans44 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans45 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans46 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans47 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans48 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans49 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans50 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans51 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans52 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans53 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans54 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans55 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans56 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans57 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
theorem transport_trans58 {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p : b = b, transport p1 (transport p H) = transport (trans p1 p) H, from
take p : b = b,
calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
end

17
tests/lean/hott/329.hlean
View file

@ -1,17 +0,0 @@
open eq sigma
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
definition path_sigma_dpair (p : a = a') (q : p ▸ b = b') : sigma.mk a b = sigma.mk a' b' :=
eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
definition path_sigma (p : pr1 u = pr1 v) (q : p ▸ pr2 u = pr2 v) : u = v :=
begin cases u, cases v, apply path_sigma_dpair p q end
definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : p1 ▸ b = b'}
(s : idp ▸ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 :=
begin
apply (eq.rec_on s),
apply idp,
end

17
tests/lean/hott/360_2.hlean
View file

@ -1,17 +0,0 @@
open is_trunc
--structure is_contr [class] (A : Type) : Type
section
parameters {P : Π(A : Type), A → Type}
definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
definition foo2
(A : Type)
(B : A → Type)
(a : A)
(x : B a)
(H : Π (a : A), is_contr (B a)) --(H : is_contr (B a))
: P (B a) x :=
by apply my_contr
end

7
tests/lean/hott/366.hlean
View file

@ -1,7 +0,0 @@
open eq
definition foo (A : Type) : Type := Π (a : A), a = a
definition thm : Π (A : Type), foo A :=
begin
intros,
apply idp
end

121
tests/lean/hott/433.hlean
View file

@ -1,121 +0,0 @@
/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn
Ported from Coq HoTT
Theorems about pi-types (dependent function spaces)
-/
import types.sigma
open eq equiv is_equiv funext
namespace pi
universe variables l k
variables {A A' : Type.{l}} {B : A → Type.{k}} {B' : A' → Type.{k}} {C : Πa, B a → Type}
{D : Πa b, C a b → Type}
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a}
/- Paths -/
/- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ∼ g].
This equivalence, however, is just the combination of [apD10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path: -/
/- Now we show how these things compute. -/
definition apd10_path_pi (H : funext) (h : f ~ g) : apd10 (eq_of_homotopy h) ~ h :=
apd10 (right_inv apd10 h)
definition path_pi_eta (H : funext) (p : f = g) : eq_of_homotopy (apd10 p) = p :=
left_inv apd10 p
print classes
definition path_pi_idp (H : funext) : eq_of_homotopy (λx : A, refl (f x)) = refl f :=
path_pi_eta H _
/- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
definition path_equiv_homotopy (H : funext) (f g : Πx, B x) : (f = g) ≃ (f ~ g) :=
equiv.mk _ !is_equiv_apd
definition is_equiv_path_pi [instance] (H : funext) (f g : Πx, B x)
: is_equiv (@eq_of_homotopy _ _ f g) :=
is_equiv_inv apd10
definition homotopy_equiv_path (H : funext) (f g : Πx, B x) : (f ~ g) ≃ (f = g) :=
equiv.mk _ (is_equiv_path_pi H f g)
/- Transport -/
protected definition transport (p : a = a') (f : Π(b : B a), C a b)
: (transport (λa, Π(b : B a), C a b) p f)
~ (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▸ b)))) :=
eq.rec_on p (λx, idp)
/- A special case of [transport_pi] where the type [B] does not depend on [A],
and so it is just a fixed type [B]. -/
definition transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b)
: (eq.transport (λa, Π(b : A'), C a b) p f) ~ (λb, eq.transport (λa, C a b) p (f b)) :=
eq.rec_on p (λx, idp)
/- Maps on paths -/
/- The action of maps given by lambda. -/
definition ap_lambdaD (H : funext) {C : A' → Type} (p : a = a') (f : Πa b, C b) :
ap (λa b, f a b) p = eq_of_homotopy (λb, ap (λa, f a b) p) :=
begin
apply (eq.rec_on p),
apply inverse,
apply (path_pi_idp H)
end
/- Dependent paths -/
/- with more implicit arguments the conclusion of the following theorem is
(Π(b : B a), transportD B C p b (f b) = g (eq.transport B p b)) ≃
(eq.transport (λa, Π(b : B a), C a b) p f = g) -/
definition dpath_pi (H : funext) (p : a = a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
: (Π(b : B a), p ▸D (f b) = g (p ▸ b)) ≃ (p ▸ f = g) :=
eq.rec_on p (λg, homotopy_equiv_path H f g) g
section open sigma sigma.ops
/- more implicit arguments:
(Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▸ b)) ≃
(Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/
definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a = a')
(f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
(Π(b : B a), (sigma.sigma_eq p !pathover_tr) ▸ (f b) = g (p ▸ b)) ≃ (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
eq.rec_on p (λg, !equiv.refl) g
end
variables (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
p⁻¹ ▸ u
definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
/- Equivalences -/
definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
[H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]
: is_equiv (functor_pi f0 f1) :=
begin
apply (adjointify (functor_pi f0 f1) (functor_pi (f0⁻¹)
(λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
intro h, apply eq_of_homotopy,
esimp [functor_pi, function.compose], -- simplify (and unfold function_pi and function.compose)
--first subgoal
intro a', esimp,
rewrite adj,
rewrite -tr_compose,
rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
rewrite (right_inv (f1 _) _),
apply apd,
intro h,
apply eq_of_homotopy, intro a, esimp,
apply (transport_V (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)),
apply apd
end
end pi

13
tests/lean/hott/443.hlean
View file

@ -1,13 +0,0 @@
import algebra.group algebra.category
open eq sigma unit category algebra
section
parameters {P₀ : Type} [P : precategory P₀]
structure my_structure := (a : P₀) (b : P₀) (f : @hom P₀ P a b)
include P
structure another_structure (X : my_structure) := (field1 : hom (my_structure.a X) (my_structure.a X))
end

24
tests/lean/hott/443_b.hlean
View file

@ -1,24 +0,0 @@
import algebra.group algebra.category
open eq sigma unit category algebra equiv
set_option pp.implicit true
set_option pp.universes true
set_option pp.notation false
section
parameters {D₀ : Type} [C : precategory D₀]
{D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d)
(h : hom a c) (i : hom b d), Type}
include C
structure my_structure1 : Type := (vo1 : D₀) (vo2 : D₀)
check my_structure1
definition foo2 : Type := my_structure1
check foo2
end
definition foo3 : Π {D₀ : Type} [C : precategory D₀], Type :=
@my_structure1

10
tests/lean/hott/457.hlean
View file

@ -1,10 +0,0 @@
import algebra.group
open eq algebra
definition foo {A : Type} (a b c : A) (H₁ : a = c) (H₂ : c = b) : a = b :=
begin
apply concat,
apply H₁,
apply H₂,
end

8
tests/lean/hott/481.hlean
View file

@ -1,8 +0,0 @@
open equiv eq is_equiv is_trunc
definition foo {A B : Type} (f : A ≃ B) (f' : A → B)
(H' : is_equiv f') (p : to_fun f = f') : p = p :=
begin
cases p,
esimp
end

9
tests/lean/hott/488.hlean
View file

@ -1,9 +0,0 @@
constants {A B : Type} {P : B → Type} {f : A → B}
(rec_on : Π(b : B) (H : Πa, P (f a)) (H2 : Πa, H a = H a), P b)
example (b : B) (H : Πa, P (f a)) : P b :=
begin
fapply (rec_on b),
{exact H},
{clear b, apply sorry}
end

182
tests/lean/hott/531b.hlean
View file

@ -1,182 +0,0 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: init.hit
Authors: Floris van Doorn
Declaration of hits
-/
structure diagram [class] :=
(Iob : Type)
(Ihom : Type)
(ob : Iob → Type)
(dom cod : Ihom → Iob)
(hom : Π(j : Ihom), ob (dom j) → ob (cod j))
open eq diagram
-- structure col (D : diagram) :=
-- (incl : Π{i : Iob}, ob i)
-- (eq_endpoint : Π{j : Ihom} (x : ob (dom j)), ob (cod j))
-- set_option pp.universes true
-- check @diagram
-- check @col
constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w}
namespace colimit
constant inclusion : Π [D : diagram] {i : Iob}, ob i → colimit D
abbreviation ι := @inclusion
constant cglue : Π [D : diagram] (j : Ihom) (x : ob (dom j)), ι (hom j x) = ι x
/-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
(y : colimit D), P y
-- {P : my_colim f → Type} (Hinc : Π⦃n : ℕ⦄ (a : A n), P (inc f a))
-- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▸ Hinc (f a) = Hinc a) : Πaa, P aa
-- init_hit
definition comp_incl [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
{i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x :=
sorry --idp
--set_option pp.notation false
definition comp_cglue [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
{j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
--the sorry's in the statement can be removed when comp_incl is definitional
sorry --idp
protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D)
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x) : P y :=
colimit.rec Pincl Pglue y
end colimit
open colimit bool
namespace pushout
section
universe u
parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
inductive pushout_ob :=
| tl : pushout_ob
| bl : pushout_ob
| tr : pushout_ob
open pushout_ob
definition pushout_diag [reducible] : diagram :=
diagram.mk pushout_ob
bool
(λi, pushout_ob.rec_on i TL BL TR)
(λj, bool.rec_on j tl tl)
(λj, bool.rec_on j bl tr)
(λj, bool.rec_on j f g)
local notation `D` := pushout_diag
-- open bool
-- definition pushout_diag : diagram :=
-- diagram.mk pushout_ob
-- bool
-- (λi, match i with | tl := TL | tr := TR | bl := BL end)
-- (λj, match j with | tt := tl | ff := tl end)
-- (λj, match j with | tt := bl | ff := tr end)
-- (λj, match j with | tt := f | ff := g end)
definition pushout := colimit pushout_diag
local attribute pushout_diag [instance]
definition inl (x : BL) : pushout :=
@ι _ _ x
definition inr (x : TR) : pushout :=
@ι _ _ x
definition coherence (x : TL) : inl (f x) = @ι _ _ x :=
@cglue _ _ x
definition glue (x : TL) : inl (f x) = inr (g x) :=
@cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
set_option pp.notation false
set_option pp.implicit true
set_option pp.beta false
-- set_option pp.universes true
protected theorem rec {P : pushout → Type} --make def
(Pinl : Π(x : BL), P (inl x))
(Pinr : Π(x : TR), P (inr x))
(Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
(y : pushout) : P y :=
begin
fapply (@colimit.rec_on _ _ y),
{ intros [i, x], cases i,
exact (coherence x ▸ Pinl (f x)),
apply Pinl,
apply Pinr},
{ intros [j, x],
cases j,
exact idp,
change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
--(@cglue _ tt x ▸ (Pinr (g x)) = (coherence x ▸ Pinl (f x))),
apply concat;rotate 1;apply (idpath (coherence x ▸ Pinl (f x))),
apply concat;apply (ap (transport _ _));apply (idpath (Pinr (g x))),
apply tr_eq_of_eq_inv_tr,
-- rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}tr_con,
apply concat, rotate 1, apply con_tr,
rewrite -Pglue}
end
example
{P : pushout → Type}
(Pinl : Π (x : BL), P (inl x))
(Pinr : Π (x : TR), P (inr x))
(Pglue :
Π (x : TL),
@eq (P (inr (g x))) (@transport pushout (λ (x : pushout), P x) (inl (f x)) (inr (g x)) (glue x) (Pinl (f x)))
(Pinr (g x)))
(y : pushout)
(x : @ob pushout_diag (@dom pushout_diag tt)) :
@eq ((λ (x : colimit pushout_diag), P x) (@ι pushout_diag (@dom pushout_diag tt) x))
(@transport (colimit pushout_diag) (λ (x : colimit pushout_diag), P x)
(@ι pushout_diag (@cod pushout_diag tt) (@hom pushout_diag tt x))
(@ι pushout_diag (@dom pushout_diag tt) x)
(@cglue pushout_diag tt x)
(@pushout_ob.cases_on (λ (n : pushout_ob), Π (x : @ob pushout_diag n), P (@ι pushout_diag n x))
(@cod pushout_diag tt)
(λ (x : @ob pushout_diag tl),
@transport pushout (λ (x : pushout), P x) (inl (f x)) (@ι pushout_diag (@dom pushout_diag ff) x)
(coherence x)
(Pinl (f x)))
(λ (x : @ob pushout_diag bl), Pinl x)
(λ (x : @ob pushout_diag tr), Pinr x)
(@hom pushout_diag tt x)))
(@pushout_ob.cases_on (λ (n : pushout_ob), Π (x : @ob pushout_diag n), P (@ι pushout_diag n x))
(@dom pushout_diag tt)
(λ (x : @ob pushout_diag tl),
@transport pushout (λ (x : pushout), P x) (inl (f x)) (@ι pushout_diag (@dom pushout_diag ff) x)
(coherence x)
(Pinl (f x)))
(λ (x : @ob pushout_diag bl), Pinl x)
(λ (x : @ob pushout_diag tr), Pinr x)
x)
:=
begin
change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
apply sorry
end
exit

16
tests/lean/hott/580.hlean
View file

@ -1,16 +0,0 @@
section
parameters (A : Type) (a b z : A) (add : A → A → A) (le : A → A → Type₀)
local notation 0 := z
local infix + := add
local infix ≤ := le
definition add_zero (x : A) : x + 0 = x := sorry
set_option pp.universes true
definition le_add_of_nonneg_right (H : a + 0 ≤ a + b) : a ≤ a + b :=
begin
rewrite add_zero at H,
exact H
end
end

8
tests/lean/hott/599.hlean
View file

@ -1,8 +0,0 @@
structure pointed [class] (A : Type) := (point : A)
open unit pointed
definition pointed_unit [instance] [constructor] : pointed unit :=
mk star
example : point unit = point unit := by esimp

10
tests/lean/hott/610.hlean
View file

@ -1,10 +0,0 @@
import hit.quotient
attribute quotient.elim [recursor 6]
definition my_elim_on {A : Type} {R : A → A → Type} {P : Type} (x : quotient R)
(Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
begin
induction x,
exact Pc a,
exact Pp H
end

9
tests/lean/hott/611.hlean
View file

@ -1,9 +0,0 @@
open is_trunc
attribute trunc.rec [recursor]
definition my_elim {n : trunc_index} {A : Type} {P : Type}
[Pt : is_trunc n P] (H : A → P) : trunc n A → P :=
begin
intro x, induction x,
apply H, assumption
end

22
tests/lean/hott/613.hlean
View file

@ -1,22 +0,0 @@
import hit.pushout
open pushout unit bool
private definition unit_of_empty (u : empty) : unit := star
example : pushout unit_of_empty unit_of_empty → bool :=
begin
intro x, induction x using pushout.rec,
exact tt,
exact ff,
cases x
end
attribute pushout.rec [recursor]
example : pushout unit_of_empty unit_of_empty → bool :=
begin
intro x, induction x,
exact tt,
exact ff,
cases x
end

21
tests/lean/hott/614.hlean
View file

@ -1,21 +0,0 @@
import homotopy.circle
open circle eq int pi
attribute circle.rec [recursor]
protected definition my_decode {x : circle} (c : circle.code x) : base = x :=
begin
induction x,
{ revert c, exact power loop },
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
rewrite [power_con,transport_code_loop]},
end
protected definition my_decode' {x : circle} : circle.code x → base = x :=
begin
induction x,
{ exact power loop},
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
rewrite [power_con,transport_code_loop]},
end

20
tests/lean/hott/615.hlean
View file

@ -1,20 +0,0 @@
-- HoTT
import homotopy.circle
open circle eq int pi
attribute circle.rec circle.elim [recursor 4]
protected definition my_code (x : circle) : Type₀ :=
begin
induction x,
{ exact ℤ},
{ apply ua, apply equiv_succ}
end
protected definition my_decode {x : circle} : my_code x → base = x :=
begin
induction x,
{ exact power loop},
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
xrewrite [power_con, transport_code_loop]},
end

12
tests/lean/hott/619.hlean
View file

@ -1,12 +0,0 @@
-- HoTT
open is_equiv equiv eq
definition my_rec_on_ua [recursor] {A B : Type} {P : A ≃ B → Type}
(f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f :=
right_inv equiv_of_eq f ▸ H (ua f)
theorem foo {A B : Type} (f : A ≃ B) : A = B :=
begin
induction f using my_rec_on_ua,
assumption
end

1
tests/lean/hott/648.hlean
View file

@ -1 +0,0 @@
import hit.colimit hit.pushout

22
tests/lean/hott/670.hlean
View file

@ -1,22 +0,0 @@
open equiv
constants (A B : Type₀) (f : A → B) (g : B → A) (p : Πb, f (g b) = b) (q : Πa, g (f a) = a)
definition e [constructor] : A ≃ B :=
equiv.MK f g p q
example (b : B) : g (f (g b)) = g b :=
by rewrite [to_right_inv e b]
example (b : B) : g (f (g b)) = g b :=
by xrewrite [to_right_inv e b]
example (b : B) : g (f (g b)) = g b :=
by krewrite [to_right_inv e b]
example (b : B) : g (f (g b)) = g b :=
begin
note H := to_right_inv e b,
esimp at H,
rewrite H
end

11
tests/lean/hott/719.hlean
View file

@ -1,11 +0,0 @@
-- HoTT
open eq
variables {A A' : Type} {a a' : A} {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A')
definition foo : (transport _ p f) b = p ▸ (f b) := sorry
definition bar : (p ▸ f) b = transport _ p (f b) := sorry
definition bla : (p ▸ f) b = p ▸ (f b) := sorry

6
tests/lean/hott/777.hlean
View file

@ -1,6 +0,0 @@
namespace sum
definition code.{u v} {A : Type.{u}} {B : Type.{v}} : A + B → A + B → Type.{max u v}
| code (inl a) (inl a') := lift (a = a')
| code (inr b) (inr b') := lift (b = b')
| code _ _ := lift empty
end sum

6
tests/lean/hott/876.hlean
View file

@ -1,6 +0,0 @@
example : Σ(X : Type₀), X → unit :=
begin
fapply sigma.mk,
{ exact unit},
{ intro x, induction x, exact unit.star }
end

13
tests/lean/hott/892.hlean
View file

@ -1,13 +0,0 @@
open is_trunc unit
protected definition trunc.elim {n : trunc_index} {A : Type} {P : Type}
[Pt : is_trunc n P] (H : A → P) : trunc n A → P :=
trunc.rec H
attribute trunc.rec [recursor 6]
attribute trunc.elim [recursor 6]
example (x : trunc -1 unit) : unit :=
begin
induction x, exact star
end

12
tests/lean/hott/996.hlean
View file

@ -1,12 +0,0 @@
import types.pointed
open pointed
variable A : Type*
variable a : A
-- Type* is notation for the type of pointed types (types with a specified point in them)
definition ex (A : Type*) (v : Σ(x : A), x = x) : v = v :=
obtain (x : A) (p : _), from v,
rfl
print ex

16
tests/lean/hott/apply_class_issue.hlean
View file

@ -1,16 +0,0 @@
open is_trunc
section
parameters {P : Π(A : Type), A → Type}
definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
definition foo2
(A : Type)
(B : A → Type)
(a : A)
(x : B a)
(H : Π (a : A), is_contr (B a)) --(H : is_contr (B a))
: P (B a) x :=
by apply (@my_contr _ _)
end

10
tests/lean/hott/beginend2.hlean
View file

@ -1,10 +0,0 @@
open eq tactic
open eq (rec_on)
definition concat_whisker2 {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
(whisker_right a q) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right a q') :=
begin
apply (rec_on b),
apply (rec_on a),
apply ((idp_con _)⁻¹),
end

34
tests/lean/hott/bug_struct_level.hlean
View file

@ -1,34 +0,0 @@
import algebra.category
open category
section
parameter {D₀ : Type}
parameter (C : precategory D₀)
parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
attribute comp [reducible]
definition comp₁_type [reducible] : Type :=
Π ⦃a b c₁ d₁ c₂ d₂ : D₀⦄
⦃f₁ : hom a b⦄ ⦃g₁ : hom c₁ d₁⦄ ⦃h₁ : hom a c₁⦄ ⦃i₁ : hom b d₁⦄
⦃g₂ : hom c₂ d₂⦄ ⦃h₂ : hom c₁ c₂⦄ ⦃i₂ : hom d₁ d₂⦄,
(D₂ g₁ g₂ h₂ i₂) → (D₂ f₁ g₁ h₁ i₁) → (@D₂ a b c₂ d₂ f₁ g₂ (h₂ ∘ h₁) (i₂ ∘ i₁))
definition ID₁_type [reducible] : Type :=
Π ⦃a b : D₀⦄ (f : hom a b), D₂ f f (ID a) (ID b)
structure worm_precat [class] : Type :=
(comp₁ : comp₁_type)
(ID₁ : ID₁_type)
end
section
parameter {D₀ : Type}
parameter [C : precategory D₀]
parameter {D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type}
parameter [D : worm_precat C D₂]
include D
structure two_cell_ob : Type :=
(vo1 : D₀) (vo2 : D₀) (vo3 : hom vo1 vo2)
end

18
tests/lean/hott/calc_auto_trans_eq.hlean
View file

@ -1,18 +0,0 @@
constant list : Type → Type
constant R.{l} : Π {A : Type.{l}}, A → A → Type.{l}
infix `~` := R
example {A : Type} {a b c d : list nat} (H₁ : a ~ b) (H₂ : b = c) (H₃ : c = d) : a ~ d :=
calc a ~ b : H₁
... = c : H₂
... = d : H₃
example {A : Type} {a b c d : list nat} (H₁ : a = b) (H₂ : b = c) (H₃ : c ~ d) : a ~ d :=
calc a = b : H₁
... = c : H₂
... ~ d : H₃
example {A : Type} {a b c d : list nat} (H₁ : a = b) (H₂ : b ~ c) (H₃ : c = d) : a ~ d :=
calc a = b : H₁
... ~ c : H₂
... = d : H₃

19
tests/lean/hott/cases.hlean
View file

@ -1,19 +0,0 @@
open nat
inductive vec (A : Type) : nat → Type :=
| nil {} : vec A zero
| cons : Π {n}, A → vec A n → vec A (succ n)
namespace vec
variables {A B C : Type}
variables {n m : nat}
notation a :: b := cons a b
protected definition destruct (v : vec A (succ n)) {P : Π {n : nat}, vec A (succ n) → Type}
(H : Π {n : nat} (h : A) (t : vec A n), P (h :: t)) : P v :=
begin
cases v with [n', h', t'],
apply (H h' t')
end
end vec

21
tests/lean/hott/cases_eq.hlean
View file

@ -1,21 +0,0 @@
open eq
theorem trans {A : Type} {a b c : A} (h₁ : a = b) (h₂ : b = c) : a = c :=
begin
cases h₁, cases h₂, apply rfl
end
theorem symm {A : Type} {a b : A} (h₁ : a = b) : b = a :=
begin
cases h₁, apply rfl
end
theorem congr2 {A B : Type} (f : A → B) {a₁ a₂ : A} (h : a₁ = a₂) : f a₁ = f a₂ :=
begin
cases h, apply rfl
end
definition inv_pV_2 {A : Type} {x y z : A} (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ :=
begin
cases p, cases q, apply rfl
end

26
tests/lean/hott/class_loop.hlean
View file

@ -1,26 +0,0 @@
constant (A : Type₁)
constant (hom : A → A → Type₁)
constant (id' : Πa, hom a a)
structure is_iso [class] {a b : A} (f : hom a b) :=
(inverse : hom b a)
open is_iso
set_option pp.metavar_args true
set_option pp.purify_metavars false
definition inverse_id [instance] {a : A} : is_iso (id' a) :=
is_iso.mk (id' a) (id' a)
definition inverse_is_iso [instance] {a b : A} (f : hom a b) (H : is_iso f) : is_iso (@inverse a b f H) :=
is_iso.mk (inverse f) f
constant a : A
set_option trace.class_instances true
definition foo := inverse (id' a)
set_option pp.implicit true
print definition foo

46
tests/lean/hott/congr_tac.hlean
View file

@ -1,46 +0,0 @@
example (f : nat → nat → nat) (a b c : nat) : b = c → f a b = f a c :=
begin
intro bc,
congruence,
assumption
end
example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
begin
intro fg bc,
congruence,
exact fg,
exact bc
end
example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c :=
by intros; congruence; repeat assumption
inductive list (A : Type) :=
| nil {} : list A
| cons : A → list A → list A
namespace list
notation `[` a `]` := list.cons a list.nil
notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
notation h :: t := cons h t
variable {T : Type}
definition append : list T → list T → list T
| [] l := l
| (h :: s) t := h :: (append s t)
notation l₁ ++ l₂ := append l₁ l₂
end list
open list
example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
begin
intro ab,
congruence,
{congruence,
exact ab},
{congruence,
exact (eq.symm ab)}
end
example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] :=
by intros; repeat (congruence | assumption | apply eq.symm)

8
tests/lean/hott/congr_tac2.hlean
View file

@ -1,8 +0,0 @@
open nat is_trunc
example (f : Π (a b : nat), a = b → nat) (a₁ a₂ b₁ b₂ : nat) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) : a₁ = a₂ → b₁ = b₂ → f a₁ b₁ h₁ = f a₂ b₂ h₂ :=
begin
intros,
congruence,
repeat assumption
end

42
tests/lean/hott/constr_tac.hlean
View file

@ -1,42 +0,0 @@
open prod
example (a b c : Type) : a → b → c → a × b × c :=
begin
intro Ha Hb Hc,
repeat (split | assumption)
end
example (a b : Type) : a → sum a b :=
begin
intro Ha,
left,
assumption
end
example (a b : Type) : b → sum a b :=
begin
intro Ha,
right,
assumption
end
open nat
example (a : nat) : a > 0 → Σ(x : ℕ), x > 0 :=
begin
intro Ha,
existsi a,
apply Ha
end
example : nat :=
begin
constructor 1
end
example : nat :=
begin
constructor 2,
constructor 2,
constructor 1
end

16
tests/lean/hott/contra1.hlean
View file

@ -1,16 +0,0 @@
open eq
example (a b : nat) (h : empty) : a = b :=
by contradiction
example : ∀ (a b : nat), empty → a = b :=
by contradiction
example : ∀ (a b : nat), 0 = 1 :> ℕ → a = b :=
by contradiction
example : ∀ (a b : nat), id empty → a = b :=
by contradiction
example : ∀ (a b : nat), id (0 = 1 :> ℕ) → a = b :=
by contradiction

16
tests/lean/hott/contra2.hlean
View file

@ -1,16 +0,0 @@
open nat
example (q p : Type) (h₁ : p) (h₂ : ¬ p) : q :=
by contradiction
example (q p : Type) (h₁ : p) (h₂ : p → empty) : q :=
by contradiction
example (q : Type) (a b : nat) (h₁ : a + b = 0) (h₂ : ¬ a + b = 0) : q :=
by contradiction
example (q : Type) (a b : nat) (h₁ : a + b = 0) (h₂ : a + b ≠ 0) : q :=
by contradiction
example (q : Type) (a b : nat) (h₁ : a + b = 0) (h₂ : a + b = 0 → empty) : q :=
by contradiction

23
tests/lean/hott/crash1.hlean
View file

@ -1,23 +0,0 @@
import types.sigma types.prod
import algebra.binary algebra.group
open eq eq.ops
namespace algebra
variable {A : Type}
structure distrib [class] (A : Type) extends has_mul A, has_add A :=
(left_distrib : ∀a b c, mul a (add b c) = add (mul a b) (mul a c))
(right_distrib : ∀a b c, mul (add a b) c = add (mul a c) (mul b c))
structure mul_zero_class [class] (A : Type) extends has_mul A, has_zero A :=
(zero_mul : Πa, mul zero a = zero)
(mul_zero : Πa, mul a zero = zero)
structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
(zero_ne_one : zero ≠ one)
structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A,
distrib A, mul_zero_class A, zero_ne_one_class A
end algebra

14
tests/lean/hott/def_bug1.hlean
View file

@ -1,14 +0,0 @@
open eq eq.ops
variable {A : Type}
definition trans : Π {x y z : A} (p : x = y) (q : y = z), x = z
| trans (refl a) (refl a) := refl a
set_option pp.purify_locals false
definition con_inv_cancel_left : Π {x y z : A} (p : x = y) (q : x = z), p ⬝ (p⁻¹ ⬝ q) = q
| con_inv_cancel_left (refl a) (refl a) := refl (refl a)
definition inv_con_cancel_left : Π {x y z : A} (p : x = y) (q : y = z), p⁻¹ ⬝ (p ⬝ q) = q
| inv_con_cancel_left (refl a) (refl a) := refl (refl a)

18
tests/lean/hott/delta_issue2.hlean
View file

@ -1,18 +0,0 @@
open nat eq
infixr + := sum
theorem add_assoc₁ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
| a b 0 := eq.refl (nat.rec a (λ x, succ) b)
| a b (succ n) :=
calc (a + b) + (succ n) = succ ((a + b) + n) : rfl
... = succ (a + (b + n)) : ap succ (add_assoc₁ a b n)
... = a + (succ (b + n)) : rfl
... = a + (b + (succ n)) : rfl
theorem add_assoc₂ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
| a b 0 := eq.refl (nat.rec a (λ x, succ) b)
| a b (succ n) := ap succ (add_assoc₂ a b n)
theorem add_assoc₃ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
| a b nat.zero := eq.refl (nat.add a b)
| a b (succ n) := ap succ (add_assoc₃ a b n)

13
tests/lean/hott/disable_instances.hlean
View file

@ -1,13 +0,0 @@
open is_equiv
constants (A B : Type) (f : A → B)
definition H : is_equiv f := sorry
definition loop [instance] [h : is_equiv f] : is_equiv f :=
h
example (a : A) : let H' : is_equiv f := H in @(is_equiv.inv f) H' (f a) = a :=
begin
with_options [elaborator.ignore_instances true] (apply left_inv f a)
end

16
tests/lean/hott/eq1.hlean
View file

@ -1,16 +0,0 @@
open nat
inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero
| cons : Π {n}, A → vector A n → vector A (succ n)
infixr `::` := vector.cons
definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n))
| swap (a :: b :: vs) := b :: a :: vs
-- Remark: in the current approach for HoTT, the equation
-- swap (a :: b :: v) = b :: a :: v
-- holds definitionally only when the index is a closed term.
example (a b : num) (v : vector num 5) : swap (a :: b :: v) = b :: a :: v :=
rfl

9
tests/lean/hott/exfalso1.hlean
View file

@ -1,9 +0,0 @@
open nat
example (a b : nat) : a = 0 → b = 1 → a = b → a + b * b ≤ 10000 :=
begin
intro a0 b1 ab,
exfalso, state,
rewrite [a0 at ab, b1 at ab],
contradiction
end

10
tests/lean/hott/get_tac1.hlean
View file

@ -1,10 +0,0 @@
open eq
definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p :=
begin
generalize p,
eapply (eq.rec_on q),
intro p,
apply (eq.rec_on p),
apply idp
end

14
tests/lean/hott/id_tac5.hlean
View file

@ -1,14 +0,0 @@
open equiv
constant rec_on_ua {A B : Type} {P : A ≃ B → Type}
(f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f
set_option pp.universes true
set_option pp.implicit true
set_option pp.notation false
check @rec_on_ua
attribute rec_on_ua [recursor]
print [recursor] rec_on_ua

7
tests/lean/hott/ind_tac1.hlean
View file

@ -1,7 +0,0 @@
set_option pp.universes true
check @homotopy.rec_on
attribute homotopy.rec_on [recursor]
print [recursor] homotopy.rec_on

13
tests/lean/hott/ind_tac2.hlean
View file

@ -1,13 +0,0 @@
set_option pp.universes true
check @trunc.rec_on
attribute trunc.rec_on [recursor]
print [recursor] trunc.rec_on
check @quotient.rec_on
attribute quotient.rec_on [recursor]
print [recursor] quotient.rec_on

11
tests/lean/hott/ind_tac3.hlean
View file

@ -1,11 +0,0 @@
open eq
set_option pp.implicit true
set_option pp.universes true
set_option pp.notation false
check @idp_rec_on
attribute idp_rec_on [recursor]
print [recursor] idp_rec_on

6
tests/lean/hott/ind_tac4.hlean
View file

@ -1,6 +0,0 @@
import homotopy.circle
open circle
attribute circle.elim_on [recursor 2]
print [recursor] circle.elim_on

40
tests/lean/hott/inj_tac.hlean
View file

@ -1,40 +0,0 @@
open nat
inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero
| cons : Π {n}, A → vector A n → vector A (succ n)
open vector
notation a :: b := cons a b
notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
example (a b : nat) : succ a = succ b → a + 2 = b + 2 :=
begin
intro H,
injection H with p,
rewrite p
end
example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) :
a :: v = b :: w → b = a :=
begin
intro H, injection H with neqn aeqb beqw,
rewrite aeqb
end
open prod
example (A : Type) (a₁ a₂ a₃ b₁ b₂ b₃ : A) : (a₁, a₂, a₃) = (b₁, b₂, b₃) → b₁ = a₁ :=
begin
intro H, injection H with a₁b₁ a₂b₂ a₃b₃,
rewrite a₁b₁
end
example (a₁ a₂ a₃ b₁ b₂ b₃ : nat) : (a₁+2, a₂+3, a₃+1) = (b₁+2, b₂+2, b₃+2) → b₁ = a₁ × a₃ = b₃+1 :=
begin
intro H, injection H with a₁b₁ sa₂b₂ a₃sb₃,
esimp at *,
rewrite [a₁b₁, a₃sb₃], split,
repeat trivial
end

24
tests/lean/hott/inv_bug.hlean
View file

@ -1,24 +0,0 @@
open nat
open eq.ops
inductive even : nat → Type :=
| even_zero : even zero
| even_succ_of_odd : ∀ {a}, odd a → even (succ a)
with odd : nat → Type :=
| odd_succ_of_even : ∀ {a}, even a → odd (succ a)
example : even 1 → empty :=
begin
intro He1,
cases He1 with [a, Ho0],
cases Ho0
end
example : even 3 → empty :=
begin
intro He3,
cases He3 with [a, Ho2],
cases Ho2 with [a, He1],
cases He1 with [a, Ho0],
cases Ho0
end

34
tests/lean/hott/krewrite_bug.hlean
View file

@ -1,34 +0,0 @@
import algebra.category.functor
open function category eq prod prod.ops equiv is_equiv sigma sigma.ops is_trunc funext iso
open pi
namespace functor
variables {A B C D E : Precategory}
definition compose_pentagon_test (K : D ⇒ E) (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
(calc K ∘f H ∘f G ∘f F = (K ∘f H) ∘f G ∘f F : functor.assoc
... = ((K ∘f H) ∘f G) ∘f F : functor.assoc)
=
(calc K ∘f H ∘f G ∘f F = K ∘f (H ∘f G) ∘f F : ap (λx, K ∘f x) !functor.assoc
... = (K ∘f H ∘f G) ∘f F : functor.assoc
... = ((K ∘f H) ∘f G) ∘f F : ap (λx, x ∘f F) !functor.assoc) :=
begin
have lem1 : Π{F₁ F₂ : A ⇒ D} (p : F₁ = F₂) (a : A),
ap010 to_fun_ob (ap (λx, K ∘f x) p) a = ap (to_fun_ob K) (ap010 to_fun_ob p a),
by intros; cases p; esimp,
have lem2 : Π{F₁ F₂ : B ⇒ E} (p : F₁ = F₂) (a : A),
ap010 to_fun_ob (ap (λx, x ∘f F) p) a = ap010 to_fun_ob p (F a),
by intros; cases p; esimp,
apply functor_eq2,
intro a, esimp,
krewrite [ap010_con],
rewrite [+ap010_con,lem1,lem2,
ap010_assoc K H (G ∘f F) a,
ap010_assoc (K ∘f H) G F a,
ap010_assoc H G F a,
ap010_assoc K H G (F a),
ap010_assoc K (H ∘f G) F a]
end
end functor

93
tests/lean/hott/len_eq.hlean
View file

@ -1,93 +0,0 @@
import init.ua
open nat unit equiv is_trunc
inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero
| cons : Π {n}, A → vector A n → vector A (succ n)
open vector
notation a :: b := cons a b
definition const {A : Type} : Π (n : nat), A → vector A n
| zero a := nil
| (succ n) a := a :: const n a
definition head {A : Type} : Π {n : nat}, vector A (succ n) → A
| n (x :: xs) := x
theorem singlenton_vector_unit : ∀ {n : nat} (v w : vector unit n), v = w
| zero nil nil := rfl
| (succ n) (star::xs) (star::ys) :=
begin
have h₁ : xs = ys, from singlenton_vector_unit xs ys,
rewrite h₁
end
private definition f (n m : nat) (v : vector unit n) : vector unit m := const m star
theorem vn_eqv_vm (n m : nat) : vector unit n ≃ vector unit m :=
equiv.MK (f n m) (f m n)
(take v : vector unit m, singlenton_vector_unit (f n m (f m n v)) v)
(take v : vector unit n, singlenton_vector_unit (f m n (f n m v)) v)
theorem vn_eq_vm (n m : nat) : vector unit n = vector unit m :=
ua (vn_eqv_vm n m)
definition vector_inj (A : Type) := ∀ (n m : nat), vector A n = vector A m → n = m
theorem not_vector_inj : ¬ vector_inj unit :=
assume H : vector_inj unit,
have aux₁ : 0 = 1, from H 0 1 (vn_eq_vm 0 1),
lift.down (nat.no_confusion aux₁)
definition cast {A B : Type} (H : A = B) (a : A) : B :=
eq.rec_on H a
open sigma
definition heq {A B : Type} (a : A) (b : B) :=
Σ (H : A = B), cast H a = b
infix `==`:50 := heq
definition heq.type_eq {A B : Type} {a : A} {b : B} : a == b → A = B
| ⟨H, e⟩ := H
definition heq.symm : ∀ {A B : Type} {a : A} {b : B}, a == b → b == a
| A A a a ⟨eq.refl A, eq.refl a⟩ := ⟨eq.refl A, eq.refl a⟩
definition heq.trans : ∀ {A B C : Type} {a : A} {b : B} {c : C}, a == b → b == c → a == c
| A A A a a a ⟨eq.refl A, eq.refl a⟩ ⟨eq.refl A, eq.refl a⟩ := ⟨eq.refl A, eq.refl a⟩
theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
| A A (eq.refl A) a := ⟨eq.refl A, eq.refl a⟩
definition lem_eq (A : Type) : Type :=
∀ (n m : nat) (v : vector A n) (w : vector A m), v == w → n = m
theorem lem_eq_iff_vector_inj (A : Type) [inh : inhabited A] : lem_eq A ↔ vector_inj A :=
iff.intro
(assume Hl : lem_eq A,
assume n m he,
assert a : A, from default A,
assert v : vector A n, from const n a,
have e₁ : v == cast he v, from heq.symm (cast_heq he v),
Hl n m v (cast he v) e₁)
(assume Hr : vector_inj A,
assume n m v w he,
Hr n m (heq.type_eq he))
theorem lem_eq_of_not_inhabited (A : Type) [ninh : inhabited A → empty] : lem_eq A :=
take (n m : nat),
match n with
| zero :=
match m with
| zero := take v w He, rfl
| (succ m₁) :=
take (v : vector A zero) (w : vector A (succ m₁)),
empty.elim (ninh (inhabited.mk (head w)))
end
| (succ n₁) :=
take (v : vector A (succ n₁)) (w : vector A m),
empty.elim (ninh (inhabited.mk (head v)))
end

15
tests/lean/hott/noc.hlean
View file

@ -1,15 +0,0 @@
set_option pp.beta true
structure foo :=
mk :: (A : Type) (B : A → Type) (a : A) (b : B a)
namespace foo
definition foo.inj₁
{A₁ : Type} {B₁ : A₁ → Type} {a₁ : A₁} {b₁ : B₁ a₁}
{A₂ : Type} {B₂ : A₂ → Type} {a₂ : A₂} {b₂ : B₂ a₂}
(H : foo.mk A₁ B₁ a₁ b₁ = foo.mk A₂ B₂ a₂ b₂)
: A₁ = A₂
:= lift.down (foo.no_confusion H (λ e₁ e₂ e₃ e₄, e₁))
end foo

20
tests/lean/hott/noc_list.hlean
View file

@ -1,20 +0,0 @@
set_option pp.universes true
check @not
inductive list (A : Type) : Type :=
| nil {} : list A
| cons : A → list A → list A
namespace list
open lift
theorem nil_ne_cons {A : Type} (a : A) (v : list A) : nil ≠ cons a v :=
λ H, down (list.no_confusion H)
theorem cons.inj₁ {A : Type} (a₁ a₂ : A) (v₁ v₂ : list A) : cons a₁ v₁ = cons a₂ v₂ → a₁ = a₂ :=
λ H, down (list.no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₁))
theorem cons.inj₂ {A : Type} (a₁ a₂ : A) (v₁ v₂ : list A) : cons a₁ v₁ = cons a₂ v₂ → v₁ = v₂ :=
λ H, down (list.no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₂))
end list

13
tests/lean/hott/notation_with_nested_tactics.hlean
View file

@ -1,13 +0,0 @@
open is_equiv
constants (A B : Type) (f : A → B)
definition H : is_equiv f := sorry
definition loop [instance] [h : is_equiv f] : is_equiv f :=
h
notation `noinstances` t:max := by with_options [elaborator.ignore_instances true] (exact t)
example (a : A) : let H' : is_equiv f := H in @(is_equiv.inv f) H' (f a) = a :=
noinstances (left_inv f a)

36
tests/lean/hott/obtain_hott.hlean
View file

@ -1,36 +0,0 @@
open prod sigma
theorem tst2 (A B C D : Type) : (A × B) × (C × D) → C × B × A :=
assume p : (A × B) × (C × D),
obtain [a b] [c d], from p,
(c, (b, a))
theorem tst22 (A B C D : Type) : (A × B) × (C × D) → C × B × A :=
assume p,
obtain [a b] [c d], from p,
(c, (b, a))
theorem tst3 (A B C D : Type) : A × B × C × D → C × B × A :=
assume p,
obtain a b c d, from p,
(c, (b, a))
example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y :=
assume ex,
obtain x y pxy qxy qyx, from ex,
⟨x, y, pxy⟩
example (p : nat → nat → Type): (Σ x, p x x) → (Σ x y, p x y) :=
assume sig,
obtain x pxx, from sig,
⟨x, x, pxx⟩
open nat
definition even (a : nat) := Σ x, a = 2*x
example (a b : nat) (H₁ : even a) (H₂ : even b) : even (a+b) :=
obtain x (Hx : a = 2*x), from H₁,
obtain y (Hy : b = 2*y), from H₂,
⟨x+y,
calc a+b = 2*x + 2*y : by rewrite [Hx, Hy]
... = 2*(x+y) : sorry⟩

19
tests/lean/hott/rewriter1.hlean
View file

@ -1,19 +0,0 @@
import algebra.group
open algebra
constant f {A : Type} : A → A → A
theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) :=
begin
rewrite [
add_zero at {1, 3}, -- rewrite 1st and 3rd occurrences
{0 + _}add.comm] -- apply commutativity to (0 + _)
end
axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1
theorem test2 {A : Type} [s : comm_group A] (a b c : A) : f a a = 1 :=
begin
rewrite [-(mul_one a), -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences
Ax] -- use Ax as rewrite rule
end

9
tests/lean/hott/rw_binders.hlean
View file

@ -1,9 +0,0 @@
import types.eq
open eq
variables {A : Type} {a1 a2 a3 : A}
definition my_transport_eq_l (p : a1 = a2) (q : a1 = a3)
: transport (λx, x = a3) p q = p⁻¹ ⬝ q :=
begin
rewrite transport_eq_l,
end

32
tests/lean/hott/rw_eta.hlean
View file

@ -1,32 +0,0 @@
open eq is_equiv funext
constant f : nat → nat → nat
example : (λ x y : nat, f x y) = f :=
rfl
namespace hide
variables {A : Type} {B : A → Type} {C : Πa, B a → Type}
definition homotopy2 [reducible] (f g : Πa b, C a b) : Type :=
Πa b, f a b = g a b
notation f `∼2`:50 g := homotopy2 f g
definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g :=
eq_of_homotopy (λa, eq_of_homotopy (H a))
definition apD100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
λa b, apd10 (apd10 p a) b
local attribute eq_of_homotopy [reducible]
definition foo (f g : Πa b, C a b) (H : f ∼2 g) (a : A)
: apD100 (eq_of_homotopy2 H) a = H a :=
begin
esimp [apD100, eq_of_homotopy2, eq_of_homotopy],
rewrite (right_inv apd10 (λ(a : A), eq_of_homotopy (H a))),
apply (right_inv apd10)
end
end hide

50
tests/lean/hott/sig_noc.hlean
View file

@ -1,50 +0,0 @@
namespace sigma
open lift
open sigma.ops sigma
variables {A : Type} {B : A → Type}
variables {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂}
definition dpair.inj (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : Σ (e₁ : a₁ = a₂), eq.rec b₁ e₁ = b₂ :=
down (sigma.no_confusion H (λ e₁ e₂, ⟨e₁, e₂⟩))
definition dpair.inj₁ (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : a₁ = a₂ :=
(dpair.inj H).1
definition dpair.inj₂ (H : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) : eq.rec b₁ (dpair.inj₁ H) = b₂ :=
(dpair.inj H).2
end sigma
structure foo :=
mk :: (A : Type) (B : A → Type) (a : A) (b : B a)
set_option pp.implicit true
namespace foo
open lift sigma sigma.ops
universe variables l₁ l₂
variables {A₁ : Type.{l₁}} {B₁ : A₁ → Type.{l₂}} {a₁ : A₁} {b₁ : B₁ a₁}
variables {A₂ : Type.{l₁}} {B₂ : A₂ → Type.{l₂}} {a₂ : A₂} {b₂ : B₂ a₂}
definition foo.inj (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) :
Σ (e₁ : A₁ = A₂) (e₂ : eq.rec B₁ e₁ = B₂) (e₃ : eq.rec a₁ e₁ = a₂), eq.rec (eq.rec (eq.rec b₁ e₁) e₂) e₃ = b₂ :=
down (foo.no_confusion H (λ e₁ e₂ e₃ e₄, ⟨e₁, e₂, e₃, e₄⟩))
definition foo.inj₁ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : A₁ = A₂ :=
(foo.inj H).1
definition foo.inj₂ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : eq.rec B₁ (foo.inj₁ H) = B₂ :=
(foo.inj H).2.1
definition foo.inj₃ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : eq.rec a₁ (foo.inj₁ H) = a₂ :=
(foo.inj H).2.2.1
definition foo.inj₄ (H : mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂) : eq.rec (eq.rec (eq.rec b₁ (foo.inj₁ H)) (foo.inj₂ H)) (foo.inj₃ H) = b₂ :=
(foo.inj H).2.2.2
definition foo.inj_inv (e₁ : A₁ = A₂) (e₂ : eq.rec B₁ e₁ = B₂) (e₃ : eq.rec a₁ e₁ = a₂) (e₄ : eq.rec (eq.rec (eq.rec b₁ e₁) e₂) e₃ = b₂) :
mk A₁ B₁ a₁ b₁ = mk A₂ B₂ a₂ b₂ :=
eq.rec_on e₄ (eq.rec_on e₃ (eq.rec_on e₂ (eq.rec_on e₁ rfl)))
end foo

58
tests/lean/hott/subst_tac.hlean
View file

@ -1,58 +0,0 @@
open nat
example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a :=
begin
subst h₁ h₂
end
example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a :=
begin
subst B h₂
end
example (a b c : nat) (a0 : a = 0) (b1 : b = 1 + a) (ab : a = b) : empty :=
begin
subst a0,
subst b1,
contradiction
end
example (a : nat) : a = 0 → a = 1 → empty :=
begin
intro a0 a1,
subst a0,
contradiction
end
example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
begin
intro a0 b1 ab,
subst a0,
rewrite b1 at *,
state,
contradiction
end
example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
begin
intro a0 b1 ab,
subst a0, subst b1,
state,
contradiction
end
example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty :=
begin
intro a0 b1 ab,
subst a0 b1,
state,
contradiction
end
example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty :=
begin
intros,
subst a b,
state,
contradiction
end

52
tests/lean/hott/substvars1.hlean
View file

@ -1,52 +0,0 @@
open nat
example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a :=
begin
substvars
end
example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a :=
begin
substvars
end
example (a b c : nat) (a0 : a = 0) (b1 : b = 1 + a) (ab : a = b) : empty :=
begin
substvars,
contradiction
end
example (a : nat) : a = 0 → a = 1 → empty :=
begin
intro a0 a1,
substvars,
contradiction
end
example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
begin
intro a0 b1 ab,
substvars,
state,
contradiction
end
example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
begin
intro a0 b1 ab,
substvars,
contradiction
end
example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty :=
begin
intro a0 b1 ab,
substvars,
contradiction
end
example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty :=
begin
intros,
substvars,
contradiction
end

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

@ -1,18 +0,0 @@
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
reveal foo.eq
print definition foo.eq

16
tests/lean/hott/test_single.sh
View file

@ -1,16 +0,0 @@
#!/usr/bin/env bash
if [ $# -ne 2 ]; then
echo "Usage: test_single.sh [lean-executable-path] [file]"
exit 1
fi
ulimit -s 8192
LEAN=$1
export HLEAN_PATH=../../../hott:.
f=$2
echo "-- testing $f"
if "$LEAN" "$f"; then
echo "-- checked"
else
echo "failed $f"
exit 1
fi

33
tests/lean/hott/trunc_1.hlean
View file

@ -1,33 +0,0 @@
open is_trunc
namespace hide
inductive trunc (n : trunc_index) (A : Type) : Type :=
tr {} : A → trunc n A
axiom is_trunc_tr (n : trunc_index) (A : Type) : is_trunc n (trunc n A)
attribute is_trunc_tr [instance]
namespace trunc
definition trunc_rec_on {n : trunc_index} {A : Type} {P : trunc n A → Type} (aa : trunc n A)
[Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : P aa :=
trunc.rec_on aa H
definition trunc_functor1 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
begin
intro xx,
apply (trunc_rec_on xx),
intro x,
exact (tr (f x))
end
definition trunc_functor2 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
by intro xx; exact (trunc_rec_on xx (λx, (tr (f x))))
definition trunc_functor3 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
by exact (λxx, trunc_rec_on xx (λx, tr (f x)))
definition trunc_functor4 {X Y : Type} (n : trunc_index) (f : X → Y) : trunc n X → trunc n Y :=
by intro xx; apply (trunc_rec_on xx); intro x; exact (tr (f x))
end trunc
end hide

37
tests/lean/hott/unfold_test.hlean
View file

@ -1,37 +0,0 @@
import algebra.e_closure
open eq
namespace relation
section
parameters {A : Type}
(R : A → A → Type)
local abbreviation T := e_closure R
variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
parameter {R}
theorem ap_ap_e_closure_elim_h₁ {B C D : Type} {f : A → B}
{g : B → C} (h : C → D)
(e : Π⦃a a' : A⦄, R a a' → f a = f a')
{e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
(p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
: square (ap (ap h) (ap_e_closure_elim_h e p t))
(ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)
(ap_compose h g (e_closure.elim e t))⁻¹
(ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) t) :=
begin
induction t,
apply sorry,
apply sorry,
{
rewrite [▸*, ap_con (ap h)],
refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
rewrite [con_inv,inv_inv,-inv2_inv],
exact !ap_inv2 ⬝v square_inv2 v_0
},
apply sorry
end
end
end relation

21
tests/lean/hott/unfoldm.hlean
View file

@ -1,21 +0,0 @@
definition rr [constructor] {A : Type} {a : A} := eq.refl a
constants f g : Π {A : Type}, A → A
example (A : Type) (a b : A) (C : A → Type) (H : C a) (f g : C a → C a) : f = g → f (eq.rec H rr) = g H :=
begin
intros,
esimp,
state,
congruence,
assumption
end
example (A : Type) (a b : A) (C : A → Type) (H : C a) (f g : C a → C a) : f = g → f (eq.rec_on rr H) = g H :=
begin
intros,
esimp,
state,
congruence,
assumption
end