From 29b35ef12d06ca904f7765929f3be595f950ca1d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Sep 2016 12:25:25 -0700 Subject: [PATCH] chore(tests/lean/hott): delete old HoTT tests --- src/shell/CMakeLists.txt | 18 - tests/lean/expensive/transport.lean | 986 ------------------ tests/lean/hott/329.hlean | 17 - tests/lean/hott/360_2.hlean | 17 - tests/lean/hott/366.hlean | 7 - tests/lean/hott/433.hlean | 121 --- tests/lean/hott/443.hlean | 13 - tests/lean/hott/443_b.hlean | 24 - tests/lean/hott/457.hlean | 10 - tests/lean/hott/481.hlean | 8 - tests/lean/hott/488.hlean | 9 - tests/lean/hott/531b.hlean | 182 ---- tests/lean/hott/580.hlean | 16 - tests/lean/hott/599.hlean | 8 - tests/lean/hott/610.hlean | 10 - tests/lean/hott/611.hlean | 9 - tests/lean/hott/613.hlean | 22 - tests/lean/hott/614.hlean | 21 - tests/lean/hott/615.hlean | 20 - tests/lean/hott/619.hlean | 12 - tests/lean/hott/648.hlean | 1 - tests/lean/hott/670.hlean | 22 - tests/lean/hott/719.hlean | 11 - tests/lean/hott/777.hlean | 6 - tests/lean/hott/876.hlean | 6 - tests/lean/hott/892.hlean | 13 - tests/lean/hott/996.hlean | 12 - tests/lean/hott/apply_class_issue.hlean | 16 - tests/lean/hott/beginend2.hlean | 10 - tests/lean/hott/bug_struct_level.hlean | 34 - tests/lean/hott/calc_auto_trans_eq.hlean | 18 - tests/lean/hott/cases.hlean | 19 - tests/lean/hott/cases_eq.hlean | 21 - tests/lean/hott/class_loop.hlean | 26 - tests/lean/hott/congr_tac.hlean | 46 - tests/lean/hott/congr_tac2.hlean | 8 - tests/lean/hott/constr_tac.hlean | 42 - tests/lean/hott/contra1.hlean | 16 - tests/lean/hott/contra2.hlean | 16 - tests/lean/hott/crash1.hlean | 23 - tests/lean/hott/def_bug1.hlean | 14 - tests/lean/hott/delta_issue2.hlean | 18 - tests/lean/hott/disable_instances.hlean | 13 - tests/lean/hott/eq1.hlean | 16 - tests/lean/hott/exfalso1.hlean | 9 - tests/lean/hott/get_tac1.hlean | 10 - tests/lean/hott/id_tac5.hlean | 14 - tests/lean/hott/ind_tac1.hlean | 7 - tests/lean/hott/ind_tac2.hlean | 13 - tests/lean/hott/ind_tac3.hlean | 11 - tests/lean/hott/ind_tac4.hlean | 6 - tests/lean/hott/inj_tac.hlean | 40 - tests/lean/hott/inv_bug.hlean | 24 - tests/lean/hott/krewrite_bug.hlean | 34 - tests/lean/hott/len_eq.hlean | 93 -- tests/lean/hott/noc.hlean | 15 - tests/lean/hott/noc_list.hlean | 20 - .../hott/notation_with_nested_tactics.hlean | 13 - tests/lean/hott/obtain_hott.hlean | 36 - tests/lean/hott/rewriter1.hlean | 19 - tests/lean/hott/rw_binders.hlean | 9 - tests/lean/hott/rw_eta.hlean | 32 - tests/lean/hott/sig_noc.hlean | 50 - tests/lean/hott/subst_tac.hlean | 58 -- tests/lean/hott/substvars1.hlean | 52 - tests/lean/hott/tele_eq.hlean | 18 - tests/lean/hott/test_single.sh | 16 - tests/lean/hott/trunc_1.hlean | 33 - tests/lean/hott/unfold_test.hlean | 37 - tests/lean/hott/unfoldm.hlean | 21 - 70 files changed, 2647 deletions(-) delete mode 100644 tests/lean/expensive/transport.lean delete mode 100644 tests/lean/hott/329.hlean delete mode 100644 tests/lean/hott/360_2.hlean delete mode 100644 tests/lean/hott/366.hlean delete mode 100644 tests/lean/hott/433.hlean delete mode 100644 tests/lean/hott/443.hlean delete mode 100644 tests/lean/hott/443_b.hlean delete mode 100644 tests/lean/hott/457.hlean delete mode 100644 tests/lean/hott/481.hlean delete mode 100644 tests/lean/hott/488.hlean delete mode 100644 tests/lean/hott/531b.hlean delete mode 100644 tests/lean/hott/580.hlean delete mode 100644 tests/lean/hott/599.hlean delete mode 100644 tests/lean/hott/610.hlean delete mode 100644 tests/lean/hott/611.hlean delete mode 100644 tests/lean/hott/613.hlean delete mode 100644 tests/lean/hott/614.hlean delete mode 100644 tests/lean/hott/615.hlean delete mode 100644 tests/lean/hott/619.hlean delete mode 100644 tests/lean/hott/648.hlean delete mode 100644 tests/lean/hott/670.hlean delete mode 100644 tests/lean/hott/719.hlean delete mode 100644 tests/lean/hott/777.hlean delete mode 100644 tests/lean/hott/876.hlean delete mode 100644 tests/lean/hott/892.hlean delete mode 100644 tests/lean/hott/996.hlean delete mode 100644 tests/lean/hott/apply_class_issue.hlean delete mode 100644 tests/lean/hott/beginend2.hlean delete mode 100644 tests/lean/hott/bug_struct_level.hlean delete mode 100644 tests/lean/hott/calc_auto_trans_eq.hlean delete mode 100644 tests/lean/hott/cases.hlean delete mode 100644 tests/lean/hott/cases_eq.hlean delete mode 100644 tests/lean/hott/class_loop.hlean delete mode 100644 tests/lean/hott/congr_tac.hlean delete mode 100644 tests/lean/hott/congr_tac2.hlean delete mode 100644 tests/lean/hott/constr_tac.hlean delete mode 100644 tests/lean/hott/contra1.hlean delete mode 100644 tests/lean/hott/contra2.hlean delete mode 100644 tests/lean/hott/crash1.hlean delete mode 100644 tests/lean/hott/def_bug1.hlean delete mode 100644 tests/lean/hott/delta_issue2.hlean delete mode 100644 tests/lean/hott/disable_instances.hlean delete mode 100644 tests/lean/hott/eq1.hlean delete mode 100644 tests/lean/hott/exfalso1.hlean delete mode 100644 tests/lean/hott/get_tac1.hlean delete mode 100644 tests/lean/hott/id_tac5.hlean delete mode 100644 tests/lean/hott/ind_tac1.hlean delete mode 100644 tests/lean/hott/ind_tac2.hlean delete mode 100644 tests/lean/hott/ind_tac3.hlean delete mode 100644 tests/lean/hott/ind_tac4.hlean delete mode 100644 tests/lean/hott/inj_tac.hlean delete mode 100644 tests/lean/hott/inv_bug.hlean delete mode 100644 tests/lean/hott/krewrite_bug.hlean delete mode 100644 tests/lean/hott/len_eq.hlean delete mode 100644 tests/lean/hott/noc.hlean delete mode 100644 tests/lean/hott/noc_list.hlean delete mode 100644 tests/lean/hott/notation_with_nested_tactics.hlean delete mode 100644 tests/lean/hott/obtain_hott.hlean delete mode 100644 tests/lean/hott/rewriter1.hlean delete mode 100644 tests/lean/hott/rw_binders.hlean delete mode 100644 tests/lean/hott/rw_eta.hlean delete mode 100644 tests/lean/hott/sig_noc.hlean delete mode 100644 tests/lean/hott/subst_tac.hlean delete mode 100644 tests/lean/hott/substvars1.hlean delete mode 100644 tests/lean/hott/tele_eq.hlean delete mode 100755 tests/lean/hott/test_single.sh delete mode 100644 tests/lean/hott/trunc_1.hlean delete mode 100644 tests/lean/hott/unfold_test.hlean delete mode 100644 tests/lean/hott/unfoldm.hlean diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 93049484db..00a855d8a5 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -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 diff --git a/tests/lean/expensive/transport.lean b/tests/lean/expensive/transport.lean deleted file mode 100644 index 94bb7d10a6..0000000000 --- a/tests/lean/expensive/transport.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/tests/lean/hott/329.hlean b/tests/lean/hott/329.hlean deleted file mode 100644 index 9c5b0170f9..0000000000 --- a/tests/lean/hott/329.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/360_2.hlean b/tests/lean/hott/360_2.hlean deleted file mode 100644 index 0669962f7a..0000000000 --- a/tests/lean/hott/360_2.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/366.hlean b/tests/lean/hott/366.hlean deleted file mode 100644 index 1efc92e20c..0000000000 --- a/tests/lean/hott/366.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean deleted file mode 100644 index 5cfd8ece85..0000000000 --- a/tests/lean/hott/433.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/443.hlean b/tests/lean/hott/443.hlean deleted file mode 100644 index b533b7a303..0000000000 --- a/tests/lean/hott/443.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/443_b.hlean b/tests/lean/hott/443_b.hlean deleted file mode 100644 index f8b7c77e8c..0000000000 --- a/tests/lean/hott/443_b.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/457.hlean b/tests/lean/hott/457.hlean deleted file mode 100644 index 63057da129..0000000000 --- a/tests/lean/hott/457.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/481.hlean b/tests/lean/hott/481.hlean deleted file mode 100644 index 48b156c7eb..0000000000 --- a/tests/lean/hott/481.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/488.hlean b/tests/lean/hott/488.hlean deleted file mode 100644 index d4ed79afe8..0000000000 --- a/tests/lean/hott/488.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/531b.hlean b/tests/lean/hott/531b.hlean deleted file mode 100644 index 1d85fa49bb..0000000000 --- a/tests/lean/hott/531b.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/580.hlean b/tests/lean/hott/580.hlean deleted file mode 100644 index e48e83b3a3..0000000000 --- a/tests/lean/hott/580.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/599.hlean b/tests/lean/hott/599.hlean deleted file mode 100644 index 32c3859362..0000000000 --- a/tests/lean/hott/599.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/610.hlean b/tests/lean/hott/610.hlean deleted file mode 100644 index b9525c4c8c..0000000000 --- a/tests/lean/hott/610.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/611.hlean b/tests/lean/hott/611.hlean deleted file mode 100644 index a6271b1ab7..0000000000 --- a/tests/lean/hott/611.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/613.hlean b/tests/lean/hott/613.hlean deleted file mode 100644 index 0215a7e295..0000000000 --- a/tests/lean/hott/613.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/614.hlean b/tests/lean/hott/614.hlean deleted file mode 100644 index 075fb966ad..0000000000 --- a/tests/lean/hott/614.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean deleted file mode 100644 index 021003ab5e..0000000000 --- a/tests/lean/hott/615.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/619.hlean b/tests/lean/hott/619.hlean deleted file mode 100644 index 27e8565f59..0000000000 --- a/tests/lean/hott/619.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/648.hlean b/tests/lean/hott/648.hlean deleted file mode 100644 index 2243045916..0000000000 --- a/tests/lean/hott/648.hlean +++ /dev/null @@ -1 +0,0 @@ -import hit.colimit hit.pushout diff --git a/tests/lean/hott/670.hlean b/tests/lean/hott/670.hlean deleted file mode 100644 index 6cf6c62845..0000000000 --- a/tests/lean/hott/670.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/719.hlean b/tests/lean/hott/719.hlean deleted file mode 100644 index 53ec8a4c63..0000000000 --- a/tests/lean/hott/719.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/777.hlean b/tests/lean/hott/777.hlean deleted file mode 100644 index 803afd309e..0000000000 --- a/tests/lean/hott/777.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/876.hlean b/tests/lean/hott/876.hlean deleted file mode 100644 index a42bd53684..0000000000 --- a/tests/lean/hott/876.hlean +++ /dev/null @@ -1,6 +0,0 @@ -example : Σ(X : Type₀), X → unit := -begin - fapply sigma.mk, - { exact unit}, - { intro x, induction x, exact unit.star } -end diff --git a/tests/lean/hott/892.hlean b/tests/lean/hott/892.hlean deleted file mode 100644 index 706f998901..0000000000 --- a/tests/lean/hott/892.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/996.hlean b/tests/lean/hott/996.hlean deleted file mode 100644 index 929b5f2b28..0000000000 --- a/tests/lean/hott/996.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/apply_class_issue.hlean b/tests/lean/hott/apply_class_issue.hlean deleted file mode 100644 index db6a6a09d0..0000000000 --- a/tests/lean/hott/apply_class_issue.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/beginend2.hlean b/tests/lean/hott/beginend2.hlean deleted file mode 100644 index 2a2b9b2a9b..0000000000 --- a/tests/lean/hott/beginend2.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/bug_struct_level.hlean b/tests/lean/hott/bug_struct_level.hlean deleted file mode 100644 index 5328258cae..0000000000 --- a/tests/lean/hott/bug_struct_level.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/calc_auto_trans_eq.hlean b/tests/lean/hott/calc_auto_trans_eq.hlean deleted file mode 100644 index 087a8894df..0000000000 --- a/tests/lean/hott/calc_auto_trans_eq.hlean +++ /dev/null @@ -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₃ diff --git a/tests/lean/hott/cases.hlean b/tests/lean/hott/cases.hlean deleted file mode 100644 index b60fa15db1..0000000000 --- a/tests/lean/hott/cases.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/cases_eq.hlean b/tests/lean/hott/cases_eq.hlean deleted file mode 100644 index bcd6673ecd..0000000000 --- a/tests/lean/hott/cases_eq.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/class_loop.hlean b/tests/lean/hott/class_loop.hlean deleted file mode 100644 index e0a11ce250..0000000000 --- a/tests/lean/hott/class_loop.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/congr_tac.hlean b/tests/lean/hott/congr_tac.hlean deleted file mode 100644 index af5b06da3c..0000000000 --- a/tests/lean/hott/congr_tac.hlean +++ /dev/null @@ -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) diff --git a/tests/lean/hott/congr_tac2.hlean b/tests/lean/hott/congr_tac2.hlean deleted file mode 100644 index 5ffe45173b..0000000000 --- a/tests/lean/hott/congr_tac2.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/constr_tac.hlean b/tests/lean/hott/constr_tac.hlean deleted file mode 100644 index 23a0451924..0000000000 --- a/tests/lean/hott/constr_tac.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/contra1.hlean b/tests/lean/hott/contra1.hlean deleted file mode 100644 index 3cf9260f58..0000000000 --- a/tests/lean/hott/contra1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/contra2.hlean b/tests/lean/hott/contra2.hlean deleted file mode 100644 index adfe662cea..0000000000 --- a/tests/lean/hott/contra2.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/crash1.hlean b/tests/lean/hott/crash1.hlean deleted file mode 100644 index b77a52e86c..0000000000 --- a/tests/lean/hott/crash1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/def_bug1.hlean b/tests/lean/hott/def_bug1.hlean deleted file mode 100644 index f37e9c9217..0000000000 --- a/tests/lean/hott/def_bug1.hlean +++ /dev/null @@ -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) diff --git a/tests/lean/hott/delta_issue2.hlean b/tests/lean/hott/delta_issue2.hlean deleted file mode 100644 index e4f55d1059..0000000000 --- a/tests/lean/hott/delta_issue2.hlean +++ /dev/null @@ -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) diff --git a/tests/lean/hott/disable_instances.hlean b/tests/lean/hott/disable_instances.hlean deleted file mode 100644 index 1b9c0bad42..0000000000 --- a/tests/lean/hott/disable_instances.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/eq1.hlean b/tests/lean/hott/eq1.hlean deleted file mode 100644 index e29f0cda2a..0000000000 --- a/tests/lean/hott/eq1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/exfalso1.hlean b/tests/lean/hott/exfalso1.hlean deleted file mode 100644 index 0a6df5836c..0000000000 --- a/tests/lean/hott/exfalso1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/get_tac1.hlean b/tests/lean/hott/get_tac1.hlean deleted file mode 100644 index 28a621fd83..0000000000 --- a/tests/lean/hott/get_tac1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/id_tac5.hlean b/tests/lean/hott/id_tac5.hlean deleted file mode 100644 index e23ad67e14..0000000000 --- a/tests/lean/hott/id_tac5.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/ind_tac1.hlean b/tests/lean/hott/ind_tac1.hlean deleted file mode 100644 index 9155edd929..0000000000 --- a/tests/lean/hott/ind_tac1.hlean +++ /dev/null @@ -1,7 +0,0 @@ -set_option pp.universes true - -check @homotopy.rec_on - -attribute homotopy.rec_on [recursor] - -print [recursor] homotopy.rec_on diff --git a/tests/lean/hott/ind_tac2.hlean b/tests/lean/hott/ind_tac2.hlean deleted file mode 100644 index 14f3137e66..0000000000 --- a/tests/lean/hott/ind_tac2.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/ind_tac3.hlean b/tests/lean/hott/ind_tac3.hlean deleted file mode 100644 index 40370f87d9..0000000000 --- a/tests/lean/hott/ind_tac3.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/ind_tac4.hlean b/tests/lean/hott/ind_tac4.hlean deleted file mode 100644 index 55c33a0076..0000000000 --- a/tests/lean/hott/ind_tac4.hlean +++ /dev/null @@ -1,6 +0,0 @@ -import homotopy.circle -open circle - -attribute circle.elim_on [recursor 2] - -print [recursor] circle.elim_on diff --git a/tests/lean/hott/inj_tac.hlean b/tests/lean/hott/inj_tac.hlean deleted file mode 100644 index e3e92a3a3d..0000000000 --- a/tests/lean/hott/inj_tac.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/inv_bug.hlean b/tests/lean/hott/inv_bug.hlean deleted file mode 100644 index aa0f1db177..0000000000 --- a/tests/lean/hott/inv_bug.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/krewrite_bug.hlean b/tests/lean/hott/krewrite_bug.hlean deleted file mode 100644 index e342592471..0000000000 --- a/tests/lean/hott/krewrite_bug.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/len_eq.hlean b/tests/lean/hott/len_eq.hlean deleted file mode 100644 index a3a4ea436f..0000000000 --- a/tests/lean/hott/len_eq.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/noc.hlean b/tests/lean/hott/noc.hlean deleted file mode 100644 index 50eaa5fa9d..0000000000 --- a/tests/lean/hott/noc.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/noc_list.hlean b/tests/lean/hott/noc_list.hlean deleted file mode 100644 index 8b7cc1b029..0000000000 --- a/tests/lean/hott/noc_list.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/notation_with_nested_tactics.hlean b/tests/lean/hott/notation_with_nested_tactics.hlean deleted file mode 100644 index 075b231645..0000000000 --- a/tests/lean/hott/notation_with_nested_tactics.hlean +++ /dev/null @@ -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) diff --git a/tests/lean/hott/obtain_hott.hlean b/tests/lean/hott/obtain_hott.hlean deleted file mode 100644 index 3f6c0178af..0000000000 --- a/tests/lean/hott/obtain_hott.hlean +++ /dev/null @@ -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⟩ diff --git a/tests/lean/hott/rewriter1.hlean b/tests/lean/hott/rewriter1.hlean deleted file mode 100644 index bd440b0a94..0000000000 --- a/tests/lean/hott/rewriter1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/rw_binders.hlean b/tests/lean/hott/rw_binders.hlean deleted file mode 100644 index 48052ee2a6..0000000000 --- a/tests/lean/hott/rw_binders.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/rw_eta.hlean b/tests/lean/hott/rw_eta.hlean deleted file mode 100644 index bac3a80275..0000000000 --- a/tests/lean/hott/rw_eta.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/sig_noc.hlean b/tests/lean/hott/sig_noc.hlean deleted file mode 100644 index 90c3c798e5..0000000000 --- a/tests/lean/hott/sig_noc.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/subst_tac.hlean b/tests/lean/hott/subst_tac.hlean deleted file mode 100644 index 10e0490342..0000000000 --- a/tests/lean/hott/subst_tac.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/substvars1.hlean b/tests/lean/hott/substvars1.hlean deleted file mode 100644 index 8da6f0e1b3..0000000000 --- a/tests/lean/hott/substvars1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/tele_eq.hlean b/tests/lean/hott/tele_eq.hlean deleted file mode 100644 index f38bf4b3d1..0000000000 --- a/tests/lean/hott/tele_eq.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/test_single.sh b/tests/lean/hott/test_single.sh deleted file mode 100755 index 308d3ee226..0000000000 --- a/tests/lean/hott/test_single.sh +++ /dev/null @@ -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 diff --git a/tests/lean/hott/trunc_1.hlean b/tests/lean/hott/trunc_1.hlean deleted file mode 100644 index 2a2b52a59a..0000000000 --- a/tests/lean/hott/trunc_1.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/unfold_test.hlean b/tests/lean/hott/unfold_test.hlean deleted file mode 100644 index b5e398fcf6..0000000000 --- a/tests/lean/hott/unfold_test.hlean +++ /dev/null @@ -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 diff --git a/tests/lean/hott/unfoldm.hlean b/tests/lean/hott/unfoldm.hlean deleted file mode 100644 index c9a79f7a14..0000000000 --- a/tests/lean/hott/unfoldm.hlean +++ /dev/null @@ -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