From aa9f32a3bd8a705c876890873aa5109d0e9397f1 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 27 Oct 2015 17:43:06 -0400 Subject: [PATCH] fix(init/equiv): make transport not an instance --- hott/init/equiv.hlean | 6 ++++-- hott/types/equiv.hlean | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 7e95aa285..29b698a03 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -41,7 +41,7 @@ namespace is_equiv protected abbreviation mk [constructor] := @is_equiv.mk' A B f -- The identity function is an equivalence. - definition is_equiv_id (A : Type) : (is_equiv (id : A → A)) := + definition is_equiv_id [instance] (A : Type) : (is_equiv (id : A → A)) := is_equiv.mk id id (λa, idp) (λa, idp) (λa, idp) -- The composition of two equivalences is, again, an equivalence. @@ -218,7 +218,7 @@ namespace is_equiv end --Transporting is an equivalence - definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A} + definition is_equiv_tr [constructor] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) := is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p) @@ -245,6 +245,8 @@ end is_equiv open is_equiv namespace eq + local attribute is_equiv_tr [instance] + definition tr_inv_fn {A : Type} {B : A → Type} {a a' : A} (p : a = a') : transport B p⁻¹ = (transport B p)⁻¹ := idp definition tr_inv {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a') : diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index cc32f070a..beec18a3b 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -23,7 +23,7 @@ namespace is_equiv right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con - ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj + ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite [adj f] ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv