refactor(typeof): move typeof to general_notation

library/algebra/category/functor.lean

@@ -4,8 +4,7 @@
 
 import .basic
 import logic.cast
-import algebra.function --remove if "typeof" is moved
+open function
-open function --remove if "typeof" is moved
 open category eq eq.ops heq
 
 inductive functor (C D : Category) : Type :=

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

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

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
 -- -------------------------
 

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
+import .path data.nat.basic data.empty data.unit data.sigma
-open path nat
+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
+have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp),
-  (λ 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