michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(hott): notation spacing and markdown files

Browse source
This commit is contained in:
Floris van Doorn 2015-10-01 15:52:28 -04:00 committed by Leonardo de Moura
parent cd48114c47
commit 115dedbd1c
26 changed files with 97 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/algebra/binary.hlean
View file

@ -47,7 +47,7 @@ namespace binary
variable {f : A → A → A}
variable H_comm : commutative f
variable H_assoc : associative f
local infixl `*` := f
local infixl * := f
theorem left_comm : left_commutative f :=
take a b c, calc
a*(b*c) = (a*b)*c : H_assoc
@ -71,7 +71,7 @@ namespace binary
variable {A : Type}
variable {f : A → A → A}
variable H_assoc : associative f
local infixl `*` := f
local infixl * := f
theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
calc
(a*b)*(c*d) = a*(b*(c*d)) : H_assoc

6
hott/algebra/category/adjoint.hlean
View file

@ -33,7 +33,7 @@ namespace category
(is_iso_counit : is_iso ε)
abbreviation inverse := @is_equivalence.G
postfix `⁻¹` := inverse
postfix ⁻¹ := inverse
--a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse
@ -55,8 +55,8 @@ namespace category
(struct : is_isomorphism to_functor)
-- infix `⊣`:55 := adjoint
infix `⋍`:25 := equivalence -- \backsimeq or \equiv
infix `≌`:25 := isomorphism -- \backcong or \iso
infix ` ⋍ `:25 := equivalence -- \backsimeq or \equiv
infix ` ≌ `:25 := isomorphism -- \backcong or \iso
definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F]
(c c' : C) : is_equiv (@(to_fun_hom F) c c') :=

6
hott/algebra/category/category.md
View file

@ -11,5 +11,7 @@ Development of Category Theory. The following files are in this folder (sorted s
* [nat_trans](nat_trans.hlean) : Natural transformations
* [strict](strict.hlean) : Strict categories
* [constructions](constructions/constructions.md) (subfolder) : basic constructions on categories and examples of categories
* [adjoint](adjoint.hlean) : Adjoint functors and Equivalences (TODO)
* [yoneda](yoneda.hlean) : Yoneda Embedding (TODO)
* [adjoint](adjoint.hlean) : Adjoint functors and Equivalences (WIP)
* [yoneda](yoneda.hlean) : Yoneda Embedding (WIP)
* [limits](limits.hlean) : Limits in a category, defined as terminal object in the cone category
* [colimits](colimits.hlean) : Colimits in a category, defined as the limit of the opposite functor

18
hott/algebra/category/constructions/constructions.md
View file

@ -3,7 +3,19 @@ algebra.category.constructions
Common categories and constructions on categories. The following files are in this folder.
* [opposite](opposite.hlean) : Opposite category
* [product](product.hlean) : Product category
* [hset](hset.hlean) : Category of sets
* [functor](functor.hlean) : Functor category
* [opposite](opposite.hlean) : Opposite category
* [hset](hset.hlean) : Category of sets
* [sum](sum.hlean) : Sum category
* [product](product.hlean) : Product category
* [comma](comma.hlean) : Comma category
* [cone](cone.hlean) : Cone category
Discrete, indiscrete or finite categories:
* [finite_cats](finite_cats.hlean) : Some finite categories, which are diagrams of common limits (the diagram for the pullback or the equalizer). Also contains a general construction of categories where you give some generators for the morphisms, with the condition that you cannot compose two of thosex
* [discrete](discrete.hlean)
* [indiscrete](indiscrete.hlean)
* [terminal](terminal.hlean)
* [initial](initial.hlean)

4
hott/algebra/category/constructions/functor.hlean
View file

@ -24,7 +24,7 @@ namespace category
definition Precategory_functor [reducible] [constructor] (D C : Precategory) : Precategory :=
precategory.Mk (precategory_functor D C)
infixr `^c`:35 := Precategory_functor
infixr ` ^c `:35 := Precategory_functor
section
/- we prove that if a natural transformation is pointwise an iso, then it is an iso -/
@ -229,7 +229,7 @@ namespace category
Category_functor D C
namespace ops
infixr `^c2`:35 := Category_functor
infixr ` ^c2 `:35 := Category_functor
end ops
namespace functor

4
hott/algebra/category/functor.hlean
View file

@ -18,7 +18,7 @@ structure functor (C D : Precategory) : Type :=
namespace functor
infixl `⇒`:25 := functor
infixl ` ⇒ `:25 := functor
variables {A B C D E : Precategory}
attribute to_fun_ob [coercion]
@ -38,7 +38,7 @@ namespace functor
G (F (g ∘ f)) = G (F g ∘ F f) : by rewrite respect_comp
... = G (F g) ∘ G (F f) : by rewrite respect_comp end)
infixr `∘f`:60 := functor.compose
infixr ` ∘f `:60 := functor.compose
protected definition id [reducible] [constructor] {C : Precategory} : functor C C :=
mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)

2
hott/algebra/category/groupoid.hlean
View file

@ -1,7 +1,7 @@
/-
Copyright (c) 2014 Jakob von Raumer. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jakob von Raumer
Authors: Jakob von Raumer, Floris van Doorn
Ported from Coq HoTT
-/

6
hott/algebra/category/iso.hlean
View file

@ -31,7 +31,7 @@ namespace iso
abbreviation inverse [unfold 6] := @is_iso.inverse
abbreviation left_inverse [unfold 6] := @is_iso.left_inverse
abbreviation right_inverse [unfold 6] := @is_iso.right_inverse
postfix `⁻¹` := inverse
postfix ⁻¹ := inverse
--a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
@ -131,7 +131,7 @@ structure iso {ob : Type} [C : precategory ob] (a b : ob) :=
(to_hom : hom a b)
[struct : is_iso to_hom]
infix `≅`:50 := iso
infix ` ≅ `:50 := iso
attribute iso.struct [instance] [priority 4000]
namespace iso
@ -162,7 +162,7 @@ namespace iso
protected definition trans [constructor] ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
mk (to_hom H2 ∘ to_hom H1)
infixl `⬝i`:75 := iso.trans
infixl ` ⬝i `:75 := iso.trans
postfix [parsing-only] `⁻¹ⁱ`:(max + 1) := iso.symm
definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')

16
hott/algebra/category/nat_trans.hlean
View file

@ -13,7 +13,7 @@ structure nat_trans {C : Precategory} {D : Precategory} (F G : C ⇒ D)
namespace nat_trans
infixl `⟹`:25 := nat_trans -- \==>
infixl ` ⟹ `:25 := nat_trans -- \==>
variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E} {F'' G'' : E ⇒ B} {J : C ⇒ C}
attribute natural_map [coercion]
@ -30,7 +30,7 @@ namespace nat_trans
... = (η b ∘ θ b) ∘ F f : by rewrite assoc
end)
infixr `∘n`:60 := nat_trans.compose
infixr ` ∘n `:60 := nat_trans.compose
protected definition id [reducible] [constructor] {F : C ⇒ D} : nat_trans F F :=
mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹)
@ -130,12 +130,12 @@ namespace nat_trans
... = F (η b ∘ f) : by rewrite (naturality η f)
... = F (η b) ∘ F f : by rewrite respect_comp)
infixr `∘nf`:62 := nat_trans_functor_compose
infixr `∘fn`:62 := functor_nat_trans_compose
infixr `∘n1f`:62 := nat_trans_id_functor_compose
infixr `∘1nf`:62 := id_nat_trans_functor_compose
infixr `∘f1n`:62 := functor_id_nat_trans_compose
infixr `∘fn1`:62 := functor_nat_trans_id_compose
infixr ` ∘nf ` :62 := nat_trans_functor_compose
infixr ` ∘fn ` :62 := functor_nat_trans_compose
infixr ` ∘n1f `:62 := nat_trans_id_functor_compose
infixr ` ∘1nf `:62 := id_nat_trans_functor_compose
infixr ` ∘f1n `:62 := functor_id_nat_trans_compose
infixr ` ∘fn1 `:62 := functor_nat_trans_id_compose
definition nf_fn_eq_fn_nf_pt (η : F ⟹ G) (θ : F' ⟹ G') (c : C)
: (θ (G c)) ∘ (F' (η c)) = (G' (η c)) ∘ (θ (F c)) :=

13
hott/algebra/category/precategory.hlean
View file

@ -33,11 +33,11 @@ namespace category
attribute precategory [multiple-instances]
attribute precategory.is_hset_hom [instance]
infixr `∘` := precategory.comp
infixr ∘ := precategory.comp
-- input ⟶ using \--> (this is a different arrow than \-> (→))
infixl [parsing-only] `⟶`:25 := precategory.hom
infixl [parsing-only] ` ⟶ `:25 := precategory.hom
namespace hom
infixl `⟶`:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
infixl ` ⟶ `:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
end hom
abbreviation hom [unfold 2] := @precategory.hom
@ -85,8 +85,8 @@ namespace category
end basic_lemmas
section squares
parameters {ob : Type} [C : precategory ob]
local infixl `⟶`:25 := @precategory.hom ob C
local infixr `∘` := @precategory.comp ob C _ _ _
local infixl ` ⟶ `:25 := @precategory.hom ob C
local infixr ∘ := @precategory.comp ob C _ _ _
definition compose_squares {xa xb xc ya yb yc : ob}
{xg : xb ⟶ xc} {xf : xa ⟶ xb} {yg : yb ⟶ yc} {yf : ya ⟶ yb}
{wa : xa ⟶ ya} {wb : xb ⟶ yb} {wc : xc ⟶ yc}
@ -149,10 +149,9 @@ namespace category
attribute Precategory.struct [instance] [priority 10000] [coercion]
-- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
-- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
notation g `∘[`:60 C:0 `]`:0 f:60 :=
notation g ` ∘[`:60 C:0 `] `:0 f:60 :=
@comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
-- TODO: make this left associative
-- TODO: change this notation?
definition Precategory.eta (C : Precategory) : Precategory.mk C C = C :=
Precategory.rec (λob c, idp) C

2
hott/algebra/e_closure.hlean
View file

@ -18,7 +18,7 @@ inductive e_closure {A : Type} (R : A → A → Type) : A → A → Type :=
| trans : Π{a a' a''} (r : e_closure R a a') (r' : e_closure R a' a''), e_closure R a a''
namespace e_closure
infix `⬝r`:75 := e_closure.trans
infix ` ⬝r `:75 := e_closure.trans
postfix `⁻¹ʳ`:(max+10) := e_closure.symm
notation `[`:max a `]`:0 := e_closure.of_rel a
abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := refl R a

2
hott/algebra/field.hlean
View file

@ -26,7 +26,7 @@ section division_ring
include s
definition divide (a b : A) : A := a * b⁻¹
infix `/` := divide
infix / := divide
-- only in this file
local attribute divide [reducible]

14
hott/algebra/group.hlean
View file

@ -34,12 +34,12 @@ structure has_inv [class] (A : Type) :=
structure has_neg [class] (A : Type) :=
(neg : A → A)
infixl `*` := has_mul.mul
infixl `+` := has_add.add
postfix `⁻¹` := has_inv.inv
prefix `-` := has_neg.neg
notation 1 := !has_one.one
notation 0 := !has_zero.zero
infixl * := has_mul.mul
infixl + := has_add.add
postfix ⁻¹ := has_inv.inv
prefix - := has_neg.neg
notation 1 := !has_one.one
notation 0 := !has_zero.zero
--a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹ᵍ`:std.prec.max_plus := has_inv.inv
@ -387,7 +387,7 @@ section add_group
-- TODO: derive corresponding facts for div in a field
definition sub [reducible] (a b : A) : A := a + -b
infix `-` := sub
infix - := sub
theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl

6
hott/algebra/order.hlean
View file

@ -29,9 +29,9 @@ structure has_le.{l} [class] (A : Type.{l}) : Type.{l+1} :=
structure has_lt [class] (A : Type) :=
(lt : A → A → Type₀)
infixl `<=` := has_le.le
infixl `≤` := has_le.le
infixl `<` := has_lt.lt
infixl <= := has_le.le
infixl ≤ := has_le.le
infixl < := has_lt.lt
definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a
notation a ≥ b := has_le.ge a b

4
hott/init/bool.hlean
View file

@ -16,12 +16,12 @@ namespace bool
definition bor (a b : bool) :=
bool.rec_on a (bool.rec_on b ff tt) tt
notation a || b := bor a b
infix || := bor
definition band (a b : bool) :=
bool.rec_on a ff (bool.rec_on b ff tt)
notation a && b := band a b
infix && := band
definition bnot (a : bool) :=
bool.rec_on a tt ff

6
hott/init/equiv.hlean
View file

@ -30,7 +30,7 @@ structure equiv (A B : Type) :=
namespace is_equiv
/- Some instances and closure properties of equivalences -/
postfix `⁻¹` := inv
postfix ⁻¹ := inv
/- a second notation for the inverse, which is not overloaded -/
postfix [parsing-only] `⁻¹ᶠ`:std.prec.max_plus := inv
@ -261,7 +261,7 @@ namespace equiv
open equiv.ops
attribute to_is_equiv [instance]
infix `≃`:25 := equiv
infix ` ≃ `:25 := equiv
section
variables {A B C : Type}
@ -358,7 +358,7 @@ namespace equiv
namespace ops
postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
postfix ⁻¹ := equiv.symm -- overloaded notation for inverse
end ops
end equiv

12
hott/init/function.hlean
View file

@ -53,15 +53,11 @@ definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C :=
definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) :=
λ f p, match p with (a, b) := f a b end
precedence `∘'`:60
precedence `on`:1
precedence `$`:1
infixr ∘ := compose
infixr ∘' := dcompose
infixl on := on_fun
infixr $ := app
infixr ` ∘ ` := compose
infixr ` ∘' `:60 := dcompose
infixl ` on `:1 := on_fun
infixr ` $ `:1 := app
notation f ` -[` op `]- ` g := combine f op g
end function

16
hott/init/logic.hlean
View file

@ -10,7 +10,7 @@ import init.reserved_notation
/- not -/
definition not [reducible] (a : Type) := a → empty
prefix `¬` := not
prefix ¬ := not
definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b :=
empty.rec (λ e, b) (H₂ H₁)
@ -36,7 +36,7 @@ assume Hb : b, absurd (assume Ha : a, Hb) H
/- eq -/
notation a = b := eq a b
infix = := eq
definition rfl {A : Type} {a : A} := eq.refl a
namespace eq
@ -52,9 +52,9 @@ namespace eq
subst H (refl a)
namespace ops
notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
notation H1 ⬝ H2 := trans H1 H2
notation H1 ▸ H2 := subst H1 H2
postfix ⁻¹ := symm --input with \sy or \-1 or \inv
infixl ⬝ := trans
infixr ▸ := subst
end ops
end eq
@ -94,7 +94,7 @@ end lift
/- ne -/
definition ne {A : Type} (a b : A) := ¬(a = b)
notation a ≠ b := ne a b
infix ≠ := ne
namespace ne
open eq.ops
@ -132,8 +132,8 @@ end
definition iff (a b : Type) := prod (a → b) (b → a)
notation a <-> b := iff a b
notation a ↔ b := iff a b
infix <-> := iff
infix ↔ := iff
namespace iff
variables {a b c : Type}

10
hott/init/path.hlean
View file

@ -559,7 +559,7 @@ namespace eq
definition inverse2 [unfold 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ :=
eq.rec_on h idp
infixl `◾`:75 := concat2
infixl ` ◾ `:75 := concat2
postfix [parsing-only] `⁻²`:(max+10) := inverse2 --this notation is abusive, should we use it?
/- Whiskering -/
@ -584,11 +584,11 @@ namespace eq
whisker_right h idp = h :=
eq.rec_on h (eq.rec_on p idp)
definition whisker_right_idp_left (p : x = y) (q : y = z) :
definition whisker_right_idp_left [unfold-full] (p : x = y) (q : y = z) :
whisker_right idp q = idp :> (p ⬝ q = p ⬝ q) :=
idp
definition whisker_left_idp_right (p : x = y) (q : y = z) :
definition whisker_left_idp_right [unfold-full] (p : x = y) (q : y = z) :
whisker_left p idp = idp :> (p ⬝ q = p ⬝ q) :=
idp
@ -596,11 +596,11 @@ namespace eq
(idp_con p) ⁻¹ ⬝ whisker_left idp h ⬝ idp_con q = h :=
eq.rec_on h (eq.rec_on p idp)
definition con2_idp {p q : x = y} (h : p = q) :
definition con2_idp [unfold-full] {p q : x = y} (h : p = q) :
h ◾ idp = whisker_right h idp :> (p ⬝ idp = q ⬝ idp) :=
idp
definition idp_con2 {p q : x = y} (h : p = q) :
definition idp_con2 [unfold-full] {p q : x = y} (h : p = q) :
idp ◾ h = whisker_left idp h :> (idp ⬝ p = idp ⬝ q) :=
idp

2
hott/init/reserved_notation.hlean
View file

@ -33,7 +33,7 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (
/- Logical operations and relations -/
reserve prefix `¬`:40
reserve prefix ` ~ `:40
reserve prefix `~`:40
reserve infixr ` ∧ `:35
reserve infixr ` /\ `:35
reserve infixr ` \/ `:30

6
hott/init/trunc.hlean
View file

@ -26,8 +26,8 @@ namespace is_trunc
notation for trunc_index is -2, -1, 0, 1, ...
from 0 and up this comes from a coercion from num to trunc_index (via nat)
-/
postfix `.+1`:(max+1) := trunc_index.succ
postfix `.+2`:(max+1) := λn, (n .+1 .+1)
postfix ` .+1`:(max+1) := trunc_index.succ
postfix ` .+2`:(max+1) := λn, (n .+1 .+1)
notation `-2` := trunc_index.minus_two
notation `-1` := -2.+1 -- ISSUE: -1 gets printed as -2.+1
export [coercions] nat
@ -56,7 +56,7 @@ namespace is_trunc
definition sub_two [reducible] (n : nat) : trunc_index :=
nat.rec_on n -2 (λ n k, k.+1)
postfix `.-2`:(max+1) := sub_two
postfix ` .-2`:(max+1) := sub_two
/- truncated types -/

2
hott/types/nat/basic.hlean
View file

@ -15,7 +15,7 @@ namespace nat
definition addl (x y : ℕ) : ℕ :=
nat.rec y (λ n r, succ r) x
infix `⊕`:65 := addl
infix ` ⊕ `:65 := addl
definition addl_succ_right (n m : ℕ) : n ⊕ succ m = succ (n ⊕ m) :=
nat.rec_on n

12
hott/types/pointed.hlean
View file

@ -74,7 +74,7 @@ namespace pointed
nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A
prefix `Ω`:(max+5) := Loop_space
notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space n A
notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A
definition refln [constructor] {A : Type*} {n : ℕ} : Ω[n] A := pt
@ -117,7 +117,7 @@ namespace pointed
abbreviation respect_pt [unfold 3] := @pmap.resp_pt
notation `map₊` := pmap
infix `→*`:30 := pmap
infix ` →* `:30 := pmap
attribute pmap.map [coercion]
variables {A B C D : Type*} {f g h : A →* B}
@ -137,13 +137,13 @@ namespace pointed
definition pcompose [constructor] (g : B →* C) (f : A →* B) : A →* C :=
pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g)
infixr `∘*`:60 := pcompose
infixr ` ∘* `:60 := pcompose
structure phomotopy (f g : A →* B) :=
(homotopy : f ~ g)
(homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f)
infix `~*`:50 := phomotopy
infix ` ~* `:50 := phomotopy
abbreviation to_homotopy_pt [unfold 5] := @phomotopy.homotopy_pt
abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a :=
phomotopy.homotopy p
@ -262,7 +262,7 @@ namespace pointed
induction p', esimp, apply inv_con_cancel_left}
end
infix `⬝*`:75 := phomotopy.trans
infix ` ⬝* `:75 := phomotopy.trans
postfix `⁻¹*`:(max+1) := phomotopy.symm
definition eq_of_phomotopy (p : f ~* g) : f = g :=
@ -295,7 +295,7 @@ namespace pointed
(to_pmap : A →* B)
(is_equiv_to_pmap : is_equiv to_pmap)
infix `≃*`:25 := pequiv
infix ` ≃* `:25 := pequiv
attribute pequiv.to_pmap [coercion]
attribute pequiv.is_equiv_to_pmap [instance]

8
hott/types/types.md
View file

@ -12,14 +12,16 @@ Types (not necessarily HoTT-related):
* [sum](sum.hlean)
* [pi](pi.hlean)
* [arrow](arrow.hlean)
* [W](W.hlean): W-types (not loaded by default)
* [arrow_2](arrow_2.hlean): alternative development of properties of arrows
* [W](W.hlean): W-types (not loaded by default)
* [lift](lift.hlean)
HoTT types
* [eq](eq.hlean): show that functions related to the identity type are equivalences
* [pointed](pointed.hlean)
* [pointed](pointed.hlean): pointed types, maps, homotopies, and equivalences
* [fiber](fiber.hlean)
* [equiv](equiv.hlean)
* [trunc](trunc.hlean): truncation levels, n-Types, truncation
* [pullback](pullback.hlean)
* [univ](univ.hlean)

1
hott/types/univ.hlean
View file

@ -47,7 +47,6 @@ namespace univ
assume H : is_hset Type,
absurd (is_trunc_is_embedding_closed lift star) not_is_hset_type0
--set_option pp.notation false
definition not_double_negation_elimination0 : ¬Π(A : Type₀), ¬¬A → A :=
begin
intro f,

2
library/init/reserved_notation.lean
View file

@ -33,7 +33,7 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (
/- Logical operations and relations -/
reserve prefix `¬`:40
reserve prefix ` ~ `:40
reserve prefix `~`:40
reserve infixr ` ∧ `:35
reserve infixr ` /\ `:35
reserve infixr ` \/ `:30