From d1b98b691918c5dacaedacc603e01bf59826591c Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 9 Apr 2015 21:41:23 -0400 Subject: [PATCH] fix(reserved_notation): make is_typeof an abbreviation --- hott/init/path.hlean | 1 + hott/init/reserved_notation.hlean | 2 +- hott/types/sigma.hlean | 2 +- library/init/reserved_notation.lean | 2 +- 4 files changed, 4 insertions(+), 3 deletions(-) diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 6b98187dc5..d1dfac72e7 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -498,6 +498,7 @@ namespace eq -- Transporting in a pulled back fibration. -- TODO: P can probably be implicit + -- rename: tr_compose definition transport_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) : transport (P ∘ f) p z = transport P (ap f p) z := eq.rec_on p idp diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index ed6198e231..2207e12f8e 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -97,7 +97,7 @@ reserve infixl `++`:65 reserve infixr `::`:65 -- Yet another trick to anotate an expression with a type -definition is_typeof (A : Type) (a : A) : A := a +abbreviation is_typeof (A : Type) (a : A) : A := a notation `typeof` t `:` T := is_typeof T t notation `(` t `:` T `)` := is_typeof T t diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 8bdaa1b11b..f71c5c9fba 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -321,7 +321,7 @@ namespace sigma section definition is_equiv_sigma_rec [instance] (C : (Σa, B a) → Type) - : is_equiv (@sigma.rec _ _ C) := + : is_equiv (sigma.rec : (Πa b, C ⟨a, b⟩) → Πab, C ab) := adjointify _ (λ g a b, g ⟨a, b⟩) (λ g, proof eq_of_homotopy (λu, destruct u (λa b, idp)) qed) (λ f, refl f) diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index d72424a811..c511cb0e63 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -94,7 +94,7 @@ reserve infixl `++`:65 reserve infixr `::`:65 -- Yet another trick to anotate an expression with a type -definition is_typeof (A : Type) (a : A) : A := a +abbreviation is_typeof (A : Type) (a : A) : A := a notation `typeof` t `:` T := is_typeof T t notation `(` t `:` T `)` := is_typeof T t