From 86c375b0c4ca5aa2d106fb238a45543c3219d623 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 5 Sep 2018 15:24:07 +0200 Subject: [PATCH] make apd10_eq_of_homotopy a homotopy --- hott/homotopy/connectedness.hlean | 2 +- hott/init/funext.hlean | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index cc6c20f15..cb6c9ac78 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -99,7 +99,7 @@ namespace is_conn intro r, refine equiv.trans _ (eq_con_inv_equiv_con_eq q p (ap (λv a, v (f a)) (eq_of_homotopy r))), - rewrite [-(ap (λv a, v (f a)) (apd10_eq_of_homotopy r))], + rewrite [-(ap (λv a, v (f a)) (apd10_eq_of_homotopy_fn r))], rewrite [-(apd10_ap_precompose_dependent f (eq_of_homotopy r))], apply equiv.symm, apply eq_equiv_fn_eq (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a))) diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 4b5671d30..8ee8bc10a 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -245,9 +245,12 @@ namespace eq definition eq_of_homotopy [reducible] : f ~ g → f = g := (@apd10 A P f g)⁻¹ - definition apd10_eq_of_homotopy (p : f ~ g) : apd10 (eq_of_homotopy p) = p := + definition apd10_eq_of_homotopy_fn (p : f ~ g) : apd10 (eq_of_homotopy p) = p := right_inv apd10 p + definition apd10_eq_of_homotopy (p : f ~ g) : apd10 (eq_of_homotopy p) ~ p := + apd10 (right_inv apd10 p) + definition eq_of_homotopy_apd10 (p : f = g) : eq_of_homotopy (apd10 p) = p := left_inv apd10 p