From 877bcd889e7a61c6ee651e6285e758c98742ce32 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 7 Jul 2017 20:11:47 +0100 Subject: [PATCH] eq_of_shomotopy --- homotopy/pointed_cubes.hlean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/homotopy/pointed_cubes.hlean b/homotopy/pointed_cubes.hlean index 792a95e..f38c547 100644 --- a/homotopy/pointed_cubes.hlean +++ b/homotopy/pointed_cubes.hlean @@ -139,6 +139,13 @@ begin exact ptb, end +definition ptube_v_eq_bot {A B C D : Type*} {ftop ftop' : A →* B} (htpy_top : ftop ~* ftop') {fbot fbot' : C →* D} {htpy_bot htpy_bot' : fbot ~* fbot'} (p : htpy_bot = htpy_bot') {fleft : A →* C} {fright : B →* D} (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop' fbot' fleft fright) : + ptube_v htpy_top htpy_bot psq_back psq_front → ptube_v htpy_top htpy_bot' psq_back psq_front := +begin + induction p, + exact id, +end + definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} (psq : psquare ftop fbot fleft fright) : ptube_v