From 7dbd7b31f61f460bc62700bd1f9e954d18c470eb Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Thu, 6 Nov 2014 18:55:44 -0500 Subject: [PATCH] Added substitution lemma for equivalence calculations --- library/hott/axioms/ua.lean | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean index cd31e8eb8..ed91dbe52 100644 --- a/library/hott/axioms/ua.lean +++ b/library/hott/axioms/ua.lean @@ -5,6 +5,7 @@ import hott.path hott.equiv open path Equiv +--Ensure that the types compared are in the same universe universe l variables (A B : Type.{l}) @@ -16,7 +17,21 @@ definition equiv_path (H : A ≈ B) : A ≃ B := axiom ua_equiv (A B : Type) : IsEquiv (equiv_path A B) +-- Make the Equivalence given by the axiom an instance definition ua_inst [instance] {A B : Type} := (@ua_equiv A B) -definition ua {A B : Type} (H : A ≃ B) : A ≈ B := - IsEquiv.inv (@equiv_path A B) H +-- This is the version of univalence axiom we will probably use most often +definition ua {A B : Type} : A ≃ B → A ≈ B := + IsEquiv.inv (@equiv_path A B) + +-- One consequence of UA is that we can transport along equivalencies of types +namespace Equiv + + protected definition subst (P : Type → Type) {A B : Type.{l}} (H : A ≃ B) + : P A → P B := + path.transport P (ua H) + + -- We can use this for calculation evironments + calc_subst subst + +end Equiv