From cd33d2e96d8155c58b9820939866beb0c97ea1dc Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 6 Nov 2014 18:54:18 -0500 Subject: [PATCH] refactor(typeof): move typeof to general_notation --- library/algebra/category/functor.lean | 3 +-- library/algebra/function.lean | 5 ----- library/general_notation.lean | 5 +++++ library/hott/path.lean | 9 +++++++++ library/hott/trunc.lean | 20 ++++++++++++++++---- 5 files changed, 31 insertions(+), 11 deletions(-) diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean index b07275ce4..aaf7eb124 100644 --- a/library/algebra/category/functor.lean +++ b/library/algebra/category/functor.lean @@ -4,8 +4,7 @@ import .basic import logic.cast -import algebra.function --remove if "typeof" is moved -open function --remove if "typeof" is moved +open function open category eq eq.ops heq inductive functor (C D : Category) : Type := diff --git a/library/algebra/function.lean b/library/algebra/function.lean index 733df0cf5..6bfdf402d 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -29,10 +29,6 @@ definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x := f x --- Yet another trick to anotate an expression with a type -definition is_typeof (A : Type) (a : A) : A := -a - precedence `∘`:60 precedence `∘'`:60 precedence `on`:1 @@ -41,7 +37,6 @@ precedence `$`:1 infixr ∘ := compose infixr ∘' := dcompose infixl on := on_fun -notation `typeof` t `:` T := is_typeof T t infixr $ := app notation f `-[` op `]-` g := combine f op g -- Trick for using any binary function as infix operator diff --git a/library/general_notation.lean b/library/general_notation.lean index ca7257d77..35e97d390 100644 --- a/library/general_notation.lean +++ b/library/general_notation.lean @@ -70,3 +70,8 @@ precedence `|`:55 reserve notation | a:55 | 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 + +notation `typeof` t `:` T := is_typeof T t diff --git a/library/hott/path.lean b/library/hott/path.lean index e52f27ed2..149eca7f0 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -23,6 +23,15 @@ notation a ≈ b := path a b notation x ≈ y `:>`:50 A:49 := @path A x y definition idp {A : Type} {a : A} := idpath a +-- unbased path induction +definition rec' {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} + (H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p := +path.rec (H a) p + +definition rec_on' {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b) + (H : Π (a : A), P a a idp) : P a b p := +path.rec (H a) p + -- Concatenation and inverse -- ------------------------- diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index 19faa2c0d..39cc28321 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -2,8 +2,8 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jeremy Avigad, Floris van Doorn -- Ported from Coq HoTT -import .path data.nat.basic data.empty data.unit -open path nat +import .path data.nat.basic data.empty data.unit data.sigma +open path nat sigma -- Truncation levels -- ----------------- @@ -45,6 +45,7 @@ trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc structure is_trunc [class] (n : trunc_index) (A : Type) := mk :: (to_internal : is_trunc_internal n A) +-- should this be notation or definitions --prefix `is_contr`:max := is_trunc -2 definition is_contr := is_trunc -2 definition is_hprop := is_trunc -1 @@ -72,8 +73,7 @@ definition path_contr [H : is_contr A] (x y : A) : x ≈ y := (contr x)⁻¹ ⬝ (contr y) definition path2_contr {A : Type₁} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q := -have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from - (λ r, path.rec_on r !concat_Vp), +have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp), K p⁻¹ ⬝ K q definition contr_paths_contr [instance] {A : Type₁} [H : is_contr A] (x y : A) : is_contr (x ≈ y) := @@ -86,6 +86,18 @@ trunc_index.rec_on n A H --in the proof the type of H is given explicitly to make it available for class inference +definition contr_basedpaths [instance] {A : Type₁} (a : A) : is_contr (Σ(x : A), a ≈ x) := +is_contr.mk (dpair a idp) (λp, sorry) + +-- Definition trunc_contr {n} {A} `{Contr A} : IsTrunc n A +-- := (@trunc_leq -2 n tt _ _). + +-- Definition trunc_hprop {n} {A} `{IsHProp A} : IsTrunc n.+1 A +-- := (@trunc_leq -1 n.+1 tt _ _). + +-- Definition trunc_hset {n} {A} `{IsHSet A} : IsTrunc n.+1.+1 A +-- := (@trunc_leq 0 n.+1.+1 tt _ _). + definition trunc_leq [instance] {A : Type₁} {m n : trunc_index} (H : m ≤ n) [H : is_trunc m A] : is_trunc n A := sorry