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

feat(hott): replace assert by have and merge namespace equiv.ops into equiv

Browse source 
The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ
This commit is contained in:
Floris van Doorn 2016-03-03 10:48:27 -05:00 committed by Leonardo de Moura
parent 058000f61d
commit 5cacebcf86
38 changed files with 131 additions and 125 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/binary.hlean
View file

@ -104,7 +104,7 @@ namespace is_equiv
end
end is_equiv
namespace equiv
open is_equiv equiv.ops
open is_equiv
definition inv_preserve_binary {A B : Type} (f : A ≃ B)
(mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a'))
(b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') :=

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

@ -6,7 +6,7 @@ Author: Jakob von Raumer
import .iso
open iso is_equiv equiv eq is_trunc sigma equiv.ops
open iso is_equiv equiv eq is_trunc sigma
/-
A category is a precategory extended by a witness

53
hott/algebra/category/functor/yoneda.hlean
View file

@ -8,10 +8,12 @@ Yoneda embedding and Yoneda lemma
import .examples .attributes
open category eq functor prod.ops is_trunc iso is_equiv equiv category.set nat_trans lift
open category eq functor prod.ops is_trunc iso is_equiv category.set nat_trans lift
namespace yoneda
universe variables u v
variable {C : Precategory.{u v}}
/-
These attributes make sure that the fields of the category "set" reduce to the right things
However, we don't want to have them globally, because that will unfold the composition g ∘ f
@ -28,7 +30,7 @@ namespace yoneda
we use (change_fun) to make sure that (to_fun_ob (yoneda_embedding C) c) will reduce to
(hom_functor_left c) instead of (functor_curry_rev_ob (hom_functor C) c)
-/
definition yoneda_embedding [constructor] (C : Precategory) : C ⇒ cset ^c Cᵒᵖ :=
definition yoneda_embedding [constructor] (C : Precategory.{u v}) : C ⇒ cset ^c Cᵒᵖ :=
--(functor_curry_rev !hom_functor)
change_fun
(functor_curry_rev !hom_functor)
@ -39,17 +41,30 @@ namespace yoneda
notation `ɏ` := yoneda_embedding _
definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset)
definition yoneda_lemma_hom_fun [unfold_full] (c : C) (F : Cᵒᵖ ⇒ cset)
(x : trunctype.carrier (F c)) (c' : Cᵒᵖ) : to_fun_ob (ɏ c) c' ⟶ F c' :=
begin
esimp [yoneda_embedding], intro f, exact F f x
end
definition yoneda_lemma_hom_nat (c : C) (F : Cᵒᵖ ⇒ cset)
(x : trunctype.carrier (F c)) {c₁ c₂ : Cᵒᵖ} (f : c₁ ⟶ c₂)
: F f ∘ yoneda_lemma_hom_fun c F x c₁ = yoneda_lemma_hom_fun c F x c₂ ∘ to_fun_hom (ɏ c) f :=
begin
esimp [yoneda_embedding], apply eq_of_homotopy, intro f',
refine _ ⬝ ap (λy, to_fun_hom F y x) !(@id_left _ C)⁻¹,
exact ap10 !(@respect_comp Cᵒᵖ cset)⁻¹ x
end
definition yoneda_lemma_hom [constructor] (c : C) (F : Cᵒᵖ ⇒ cset)
(x : trunctype.carrier (F c)) : ɏ c ⟹ F :=
begin
fapply nat_trans.mk,
{ intro c', esimp [yoneda_embedding], intro f, exact F f x},
{ intro c' c'' f, esimp [yoneda_embedding], apply eq_of_homotopy, intro f',
refine _ ⬝ ap (λy, to_fun_hom F y x) !(@id_left _ C)⁻¹,
exact ap10 !(@respect_comp Cᵒᵖ cset)⁻¹ x}
{ exact yoneda_lemma_hom_fun c F x},
{ intro c₁ c₂ f, exact yoneda_lemma_hom_nat c F x f}
end
definition yoneda_lemma_equiv [constructor] {C : Precategory} (c : C)
definition yoneda_lemma_equiv [constructor] (c : C)
(F : Cᵒᵖ ⇒ cset) : hom (ɏ c) F ≃ lift (trunctype.carrier (to_fun_ob F c)) :=
begin
fapply equiv.MK,
@ -64,13 +79,13 @@ namespace yoneda
rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left end end},
end
definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset) :
definition yoneda_lemma (c : C) (F : Cᵒᵖ ⇒ cset) :
homset (ɏ c) F ≅ functor_lift (F c) :=
begin
apply iso_of_equiv, esimp, apply yoneda_lemma_equiv,
end
theorem yoneda_lemma_natural_ob {C : Precategory} (F : Cᵒᵖ ⇒ cset) {c c' : C} (f : c' ⟶ c)
theorem yoneda_lemma_natural_ob (F : Cᵒᵖ ⇒ cset) {c c' : C} (f : c' ⟶ c)
(η : ɏ c ⟹ F) :
to_fun_hom (functor_lift ∘f F) f (to_hom (yoneda_lemma c F) η) =
to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) :=
@ -89,7 +104,7 @@ namespace yoneda
-- attribute yoneda_lemma functor_lift Precategory_Set precategory_Set homset
-- yoneda_embedding nat_trans.compose functor_nat_trans_compose [reducible]
-- attribute tlift functor.compose [reducible]
theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ cset)
theorem yoneda_lemma_natural_functor (c : C) (F F' : Cᵒᵖ ⇒ cset)
(θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) :
(functor_lift.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) =
proof to_hom (yoneda_lemma c F') (θ ∘n η) qed :=
@ -107,20 +122,21 @@ namespace yoneda
-- proof _ qed :=
-- by reflexivity
definition fully_faithful_yoneda_embedding [instance] (C : Precategory) :
open equiv
definition fully_faithful_yoneda_embedding [instance] (C : Precategory.{u v}) :
fully_faithful (ɏ : C ⇒ cset ^c Cᵒᵖ) :=
begin
intro c c',
fapply is_equiv_of_equiv_of_homotopy,
{ symmetry, transitivity _, apply @equiv_of_iso (homset _ _),
rexact yoneda_lemma c (ɏ c'), esimp [yoneda_embedding], exact !equiv_lift⁻¹ᵉ},
exact @yoneda_lemma C c (ɏ c'), esimp [yoneda_embedding], exact !equiv_lift⁻¹ᵉ},
{ intro f, apply nat_trans_eq, intro c, apply eq_of_homotopy, intro f',
esimp [equiv.symm,equiv.trans],
esimp [yoneda_lemma,yoneda_embedding,Opposite],
rewrite [id_left,id_right]}
end
definition is_embedding_yoneda_embedding (C : Category) :
definition is_embedding_yoneda_embedding (C : Category.{u v}) :
is_embedding (ɏ : C → Cᵒᵖ ⇒ cset) :=
begin
intro c c', fapply is_equiv_of_equiv_of_homotopy,
@ -134,15 +150,18 @@ namespace yoneda
rewrite [▸*, category.category.id_left], apply id_right}
end
definition is_representable {C : Precategory} (F : Cᵒᵖ ⇒ cset) := Σ(c : C), ɏ c ≅ F
definition is_representable (F : Cᵒᵖ ⇒ cset) := Σ(c : C), ɏ c ≅ F
section
set_option apply.class_instance false
definition is_prop_representable {C : Category} (F : Cᵒᵖ ⇒ cset)
open functor.ops
definition is_prop_representable {C : Category.{u v}} (F : Cᵒᵖ ⇒ cset)
: is_prop (is_representable F) :=
begin
fapply is_trunc_equiv_closed,
{ exact proof fiber.sigma_char ɏ F qed ⬝e sigma.sigma_equiv_sigma_right (λc, !eq_equiv_iso)},
{ unfold [is_representable],
rexact fiber.sigma_char ɏ F ⬝e sigma.sigma_equiv_sigma_right
(λc, @eq_equiv_iso (cset ^c2 Cᵒᵖ) _ (hom_functor_left c) F)},
{ apply function.is_prop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding}
end
end

8
hott/algebra/category/limits/functor_preserve.hlean
View file

@ -52,7 +52,8 @@ namespace category
local attribute category.to_precategory [constructor]
definition preserves_existing_limits_yoneda_embedding_lemma [constructor] (y : cone_obj F)
definition preserves_existing_limits_yoneda_embedding_lemma [constructor]
(y : cone_obj F)
[H : is_terminal y] {G : Cᵒᵖ ⇒ cset} (η : constant_functor I G ⟹ ɏ ∘f F) :
G ⟹ hom_functor_left (cone_to_obj y) :=
begin
@ -70,15 +71,14 @@ namespace category
refine _ ⬝ ap10 (naturality (η i) f) x, rewrite [▸*, id_left]}
-- abstracting here fails
end
-- print preserves_existing_limits_yoneda_embedding_lemma_11
theorem preserves_existing_limits_yoneda_embedding (C : Precategory)
: preserves_existing_limits (yoneda_embedding C) :=
begin
intro I F H Gη, induction H with y H, induction Gη with G η, esimp at *,
have lem : Π (i : carrier I),
have lem : Π(i : carrier I),
nat_trans_hom_functor_left (natural_map (cone_to_nat y) i)
∘n preserves_existing_limits_yoneda_embedding_lemma y η = natural_map η i,
∘n @preserves_existing_limits_yoneda_embedding_lemma I C F y H G η = natural_map η i,
begin
intro i, apply nat_trans_eq, intro c, apply eq_of_homotopy, intro x,
esimp, refine !assoc ⬝ !id_right ⬝ !to_hom_limit_commute

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

@ -5,7 +5,7 @@ Authors: Floris van Doorn
-/
import types.trunc types.pi arity
open eq is_trunc pi equiv equiv.ops
open eq is_trunc pi equiv
namespace category

2
hott/algebra/hott.hlean
View file

@ -8,7 +8,7 @@ Theorems about algebra specific to HoTT
import .group arity types.pi prop_trunc types.unit .bundled
open equiv eq equiv.ops is_trunc unit
open equiv eq is_trunc unit
namespace algebra

12
hott/cubical/cube.hlean
View file

@ -8,7 +8,7 @@ Cubes
import .square
open equiv equiv.ops is_equiv sigma sigma.ops
open equiv is_equiv sigma sigma.ops
namespace eq
@ -48,7 +48,7 @@ namespace eq
definition refl2 : cube hrfl hrfl s₁₀₁ s₁₀₁ hrfl hrfl :=
by induction s₁₀₁; exact idc
definition refl3 : cube vrfl vrfl vrfl vrfl s₁₁₀ s₁₁₀ :=
by induction s₁₁₀; exact idc
@ -169,9 +169,9 @@ namespace eq
variables {a₀ a₁ : A} {p₀₀ p₀₂ p₂₀ p₂₂ : a₀ = a₁} {s₁₀ : p₀₀ = p₂₀}
{s₁₂ : p₀₂ = p₂₂} {s₀₁ : p₀₀ = p₀₂} {s₂₁ : p₂₀ = p₂₂}
(sq : square s₁₀ s₁₂ s₀₁ s₂₁)
include sq
definition ids3_cube_of_square : cube (hdeg_square s₀₁)
(hdeg_square s₂₁) (hdeg_square s₁₀) (hdeg_square s₁₂) ids ids :=
by induction p₀₀; induction sq; apply idc
@ -194,7 +194,7 @@ namespace eq
definition cube_fill110 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ lid s₁₁₂ :=
begin
induction s₀₁₁, induction s₂₁₁,
let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁)
let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁)
(eq_of_hdeg_square s₁₁₂) (eq_of_vdeg_square s₁₂₁),
apply sigma.mk,
apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
@ -206,7 +206,7 @@ namespace eq
definition cube_fill112 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ lid :=
begin
induction s₀₁₁, induction s₂₁₁,
let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁)
let fillsq := square_fill_r (eq_of_vdeg_square s₁₀₁)
(eq_of_hdeg_square s₁₁₀) (eq_of_vdeg_square s₁₂₁),
apply sigma.mk,
apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),

2
hott/cubical/squareover.hlean
View file

@ -8,7 +8,7 @@ Squareovers
import .square
open eq equiv is_equiv equiv.ops
open eq equiv is_equiv
namespace eq

2
hott/hit/coeq.hlean
View file

@ -8,7 +8,7 @@ Declaration of the coequalizer
import .quotient_functor types.equiv
open quotient eq equiv equiv.ops is_trunc sigma sigma.ops
open quotient eq equiv is_trunc sigma sigma.ops
namespace coeq
section

2
hott/hit/colimit.hlean
View file

@ -7,7 +7,7 @@ Definition of general colimits and sequential colimits.
-/
/- definition of a general colimit -/
open eq nat quotient sigma equiv equiv.ops is_trunc
open eq nat quotient sigma equiv is_trunc
namespace colimit
section

2
hott/hit/pushout.hlean
View file

@ -8,7 +8,7 @@ Declaration of the pushout
import .quotient cubical.square types.sigma
open quotient eq sum equiv equiv.ops is_trunc
open quotient eq sum equiv is_trunc
namespace pushout
section

2
hott/hit/quotient.hlean
View file

@ -16,7 +16,7 @@ See also .set_quotient
import arity cubical.squareover types.arrow cubical.pathover2 types.pointed
open eq equiv sigma sigma.ops equiv.ops pi is_trunc pointed
open eq equiv sigma sigma.ops pi is_trunc pointed
namespace quotient

1
hott/hit/quotient_functor.hlean
View file

@ -104,7 +104,6 @@ section
end
section
open equiv.ops
variables {A : Type} (R : A → A → Type)
{B : Type} (Q : B → B → Type)
(f : A ≃ B) (k : Πa a' : A, R a a' ≃ Q (f a) (f a'))

1
hott/hit/trunc.hlean
View file

@ -82,7 +82,6 @@ namespace trunc
λxx, trunc.rec_on xx (λx, ap tr (p x))
section
open equiv.ops
definition trunc_equiv_trunc [constructor] (f : X ≃ Y) : trunc n X ≃ trunc n Y :=
equiv.mk _ (is_equiv_trunc_functor n f)
end

4
hott/homotopy/circle.hlean
View file

@ -10,7 +10,7 @@ import .sphere
import types.bool types.int.hott types.equiv
import algebra.homotopy_group algebra.hott .connectedness
open eq susp bool sphere_index is_equiv equiv equiv.ops is_trunc pi algebra homotopy
open eq susp bool sphere_index is_equiv equiv is_trunc pi algebra homotopy
definition circle : Type₀ := sphere 1
@ -235,7 +235,7 @@ namespace circle
preserve_binary_of_inv_preserve base_eq_base_equiv concat (@add ℤ _) decode_add p q
--the carrier of π₁(S¹) is the set-truncation of base = base.
open algebra trunc equiv.ops
open algebra trunc
definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ :=
trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv ℤ _) proof _ qed

3
hott/homotopy/connectedness.hlean
View file

@ -275,10 +275,11 @@ namespace homotopy
end
open trunc_index
-- Corollary 8.2.2
theorem is_conn_sphere [instance] (n : ℕ₋₁) : is_conn (n..-1) (sphere n) :=
begin
induction n with n IH,
{ apply is_trunc_trunc},
{ apply minus_two_conn},
{ rewrite [succ_sub_one, sphere.sphere_succ], apply is_conn_susp}
end

2
hott/homotopy/cylinder.hlean
View file

@ -8,7 +8,7 @@ Declaration of mapping cylinders
import hit.quotient
open quotient eq sum equiv equiv.ops
open quotient eq sum equiv
namespace cylinder
section

2
hott/homotopy/interval.hlean
View file

@ -7,7 +7,7 @@ Declaration of the interval
-/
import .susp types.eq types.prod cubical.square
open eq susp unit equiv equiv.ops is_trunc nat prod
open eq susp unit equiv is_trunc nat prod
definition interval : Type₀ := susp unit

4
hott/homotopy/susp.hlean
View file

@ -8,7 +8,7 @@ Declaration of suspension
import hit.pushout types.pointed cubical.square
open pushout unit eq equiv equiv.ops
open pushout unit eq equiv
definition susp (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star)
@ -220,7 +220,7 @@ namespace susp
end
definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y)
: (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* psusp_functor g :=
: (susp_adjoint_loop X Z)⁻¹ᵉ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ᵉ f ∘* psusp_functor g :=
begin
esimp [susp_adjoint_loop],
refine _ ⬝* !passoc⁻¹*,

18
hott/init/equiv.hlean
View file

@ -269,14 +269,11 @@ namespace eq
definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp
end eq
namespace equiv
namespace ops
attribute to_fun [coercion]
end ops
open equiv.ops
attribute to_is_equiv [instance]
infix ` ≃ `:25 := equiv
attribute equiv.to_is_equiv [instance]
infix ` ≃ `:25 := equiv
namespace equiv
attribute to_fun [coercion]
section
variables {A B C : Type}
@ -395,17 +392,12 @@ namespace equiv
end
namespace ops
postfix ⁻¹ := equiv.symm -- overloaded notation for inverse
end ops
infixl ` ⬝pe `:75 := equiv_of_equiv_of_eq
infixl ` ⬝ep `:75 := equiv_of_eq_of_equiv
end equiv
open equiv equiv.ops
open equiv
namespace is_equiv
definition is_equiv_of_equiv_of_homotopy [constructor] {A B : Type} (f : A ≃ B)

2
hott/init/pathover.hlean
View file

@ -9,7 +9,7 @@ Basic theorems about pathovers
prelude
import .path .equiv
open equiv is_equiv equiv.ops function
open equiv is_equiv function
variables {A A' : Type} {B B' : A → Type} {B'' : A' → Type} {C : Π⦃a⦄, B a → Type}
{a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} {p₁₃ : a = a₃}

11
hott/init/trunc.hlean
View file

@ -278,11 +278,12 @@ namespace is_trunc
theorem is_trunc_is_equiv_closed (n : ℕ₋₂) (f : A → B) [H : is_equiv f]
[HA : is_trunc n A] : is_trunc n B :=
trunc_index.rec_on n
(λA (HA : is_contr A) B f (H : is_equiv f), is_contr_is_equiv_closed f)
(λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ_intro _ _ (λ x y : B,
IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv))
A HA B f H
begin
revert A HA B f H, induction n with n IH: intros,
{ exact is_contr_is_equiv_closed f},
{ apply is_trunc_succ_intro, intro x y,
exact IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv}
end
definition is_trunc_is_equiv_closed_rev (n : ℕ₋₂) (f : A → B) [H : is_equiv f]
[HA : is_trunc n B] : is_trunc n A :=

2
hott/init/ua.hlean
View file

@ -8,7 +8,7 @@ Ported from Coq HoTT
prelude
import .equiv
open eq equiv is_equiv equiv.ops
open eq equiv is_equiv
--Ensure that the types compared are in the same universe
section

2
hott/types/arrow.hlean
View file

@ -9,7 +9,7 @@ Theorems about arrow types (function spaces)
import types.pi
open eq equiv is_equiv funext pi equiv.ops is_trunc unit
open eq equiv is_equiv funext pi is_trunc unit
namespace pi

2
hott/types/eq.hlean
View file

@ -8,7 +8,7 @@ Theorems about path types (identity types)
-/
import types.sigma
open eq sigma sigma.ops equiv is_equiv equiv.ops is_trunc
open eq sigma sigma.ops equiv is_equiv is_trunc
-- TODO: Rename transport_eq_... and pathover_eq_... to eq_transport_... and eq_pathover_...

2
hott/types/equiv.hlean
View file

@ -9,7 +9,7 @@ Theorems about the types equiv and is_equiv
import .fiber .arrow arity ..prop_trunc
open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops
open eq is_trunc sigma sigma.ops pi fiber function equiv
namespace is_equiv
variables {A B : Type} (f : A → B) [H : is_equiv f]

2
hott/types/int/hott.hlean
View file

@ -7,7 +7,7 @@ Theorems about the integers specific to HoTT
-/
import .basic types.eq arity algebra.bundled
open core eq is_equiv equiv equiv.ops algebra is_trunc
open core eq is_equiv equiv algebra is_trunc
open nat (hiding pred)
namespace int

2
hott/types/lift.hlean
View file

@ -7,7 +7,7 @@ Theorems about lift
-/
import ..function
open eq equiv equiv.ops is_equiv is_trunc pointed
open eq equiv is_equiv is_trunc pointed
namespace lift

46
hott/types/nat/div.hlean
View file

@ -168,15 +168,15 @@ begin
intro x IH,
show succ x = succ x / y * y + succ x % y, from
if H1 : succ x < y then
assert H2 : succ x / y = 0, from div_eq_zero_of_lt H1,
assert H3 : succ x % y = succ x, from mod_eq_of_lt H1,
have H2 : succ x / y = 0, from div_eq_zero_of_lt H1,
have H3 : succ x % y = succ x, from mod_eq_of_lt H1,
begin rewrite [H2, H3, zero_mul, zero_add] end
else
have H2 : y ≤ succ x, from le_of_not_gt H1,
assert H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2,
assert H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2,
have H3 : succ x / y = succ ((succ x - y) / y), from div_eq_succ_sub_div H H2,
have H4 : succ x % y = (succ x - y) % y, from mod_eq_sub_mod H H2,
have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
assert H6 : succ x - y ≤ x, from le_of_lt_succ H5,
have H6 : succ x - y ≤ x, from le_of_lt_succ H5,
(calc
succ x / y * y + succ x % y =
succ ((succ x - y) / y) * y + succ x % y : by rewrite H3
@ -213,7 +213,7 @@ by_cases_zero_pos n
assume npos : n > 0,
assume H1 : (m + i) % n = (k + i) % n,
have H2 : (m + i % n) % n = (k + i % n) % n, by rewrite [*add_mod_mod, H1],
assert H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n,
have H3 : (m + i % n + (n - i % n)) % n = (k + i % n + (n - i % n)) % n,
from add_mod_eq_add_mod_right _ H2,
begin
revert H3,
@ -301,11 +301,11 @@ theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) % k = (m * (n % k)) % k :
!mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod
protected theorem div_one (n : ℕ) : n / 1 = n :=
assert n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹,
have n / 1 * 1 + n % 1 = n, from !eq_div_mul_add_mod⁻¹,
begin rewrite [-this at {2}, mul_one, mod_one] end
protected theorem div_self {n : ℕ} (H : n > 0) : n / n = 1 :=
assert (n * 1) / (n * 1) = 1 / 1, from !nat.mul_div_mul_left H,
have (n * 1) / (n * 1) = 1 / 1, from !nat.mul_div_mul_left H,
by rewrite [nat.div_one at this, -this, *mul_one]
theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m % n = 0) : m / n * n = m :=
@ -451,11 +451,11 @@ end
lemma le_of_dvd {m n : nat} : n > 0 → m ∣ n → m ≤ n :=
assume (h₁ : n > 0) (h₂ : m ∣ n),
assert h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂,
have h₃ : n % m = 0, from mod_eq_zero_of_dvd h₂,
by_contradiction
(λ nle : ¬ m ≤ n,
have h₄ : m > n, from lt_of_not_ge nle,
assert h₅ : n % m = n, from mod_eq_of_lt h₄,
have h₅ : n % m = n, from mod_eq_of_lt h₄,
begin
rewrite h₃ at h₅, subst n,
exact absurd h₁ (lt.irrefl 0)
@ -516,7 +516,7 @@ lt_of_mul_lt_mul_right (calc
... < n * k : H)
protected theorem lt_mul_of_div_lt {m n k : ℕ} (H1 : k > 0) (H2 : m / k < n) : m < n * k :=
assert H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2),
have H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2),
have H4 : m / k * k + k ≤ n * k, by rewrite [succ_mul at H3]; apply H3,
calc
m = m / k * k + m % k : eq_div_mul_add_mod
@ -567,28 +567,28 @@ nat.strong_rec_on a
(λ a ih,
let k₁ := a / (b*c) in
let k₂ := a %(b*c) in
assert bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`,
assert k₂ < b * c, from mod_lt _ bc_pos,
assert k₂ ≤ a, from !mod_le,
have bc_pos : b*c > 0, from mul_pos `b > 0` `c > 0`,
have k₂ < b * c, from mod_lt _ bc_pos,
have k₂ ≤ a, from !mod_le,
sum.elim (eq_sum_lt_of_le this)
(suppose k₂ = a,
assert i₁ : a < b * c, by rewrite -this; assumption,
assert k₁ = 0, from div_eq_zero_of_lt i₁,
assert a / b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁,
have i₁ : a < b * c, by rewrite -this; assumption,
have k₁ = 0, from div_eq_zero_of_lt i₁,
have a / b < c, by rewrite [mul.comm at i₁]; exact nat.div_lt_of_lt_mul i₁,
begin
rewrite [`k₁ = 0`],
show (a / b) / c = 0, from div_eq_zero_of_lt `a / b < c`
end)
(suppose k₂ < a,
assert a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c),
assert a / b = k₁*c + k₂ / b, by
have a = k₁*(b*c) + k₂, from eq_div_mul_add_mod a (b*c),
have a / b = k₁*c + k₂ / b, by
rewrite [this at {1}, mul.comm b c at {2}, -mul.assoc,
add.comm, add_mul_div_self `b > 0`, add.comm],
assert e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by
have e₁ : (a / b) / c = k₁ + (k₂ / b) / c, by
rewrite [this, add.comm, add_mul_div_self `c > 0`, add.comm],
assert e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`,
assert e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`,
assert (k₂ / b) / c = 0, by rewrite [e₂, e₃],
have e₂ : (k₂ / b) / c = k₂ / (b * c), from ih k₂ `k₂ < a`,
have e₃ : k₂ / (b * c) = 0, from div_eq_zero_of_lt `k₂ < b * c`,
have (k₂ / b) / c = 0, by rewrite [e₂, e₃],
show (a / b) / c = k₁, by rewrite [e₁, this]))
protected lemma div_div_eq_div_mul (a b c : nat) : (a / b) / c = a / (b * c) :=

3
hott/types/pointed.hlean
View file

@ -7,7 +7,7 @@ Ported from Coq HoTT
-/
import arity .eq .bool .unit .sigma .nat.basic prop_trunc
open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra equiv.ops sigma.ops
open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra sigma.ops
structure pointed [class] (A : Type) :=
(point : A)
@ -97,7 +97,6 @@ namespace pointed
definition iterated_loop_space [unfold 3] (A : Type) [H : pointed A] (n : ℕ) : Type :=
Ω[n] (pointed.mk' A)
open equiv.ops
definition pType_eq {A B : Type*} (f : A ≃ B) (p : f pt = pt) : A = B :=
begin
cases A with A a, cases B with B b, esimp at *,

2
hott/types/pointed2.hlean
View file

@ -9,7 +9,7 @@ Ported from Coq HoTT
import .equiv cubical.square
open eq is_equiv equiv equiv.ops pointed is_trunc
open eq is_equiv equiv pointed is_trunc
-- structure pequiv (A B : Type*) :=
-- (to_pmap : A →* B)

2
hott/types/prod.hlean
View file

@ -7,7 +7,7 @@ Ported from Coq HoTT
Theorems about products
-/
open eq equiv is_equiv is_trunc prod prod.ops unit equiv.ops
open eq equiv is_equiv is_trunc prod prod.ops unit
variables {A A' B B' C D : Type} {P Q : A → Type}
{a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}

2
hott/types/pullback.hlean
View file

@ -7,7 +7,7 @@ Theorems about pullbacks
-/
import cubical.square
open eq equiv is_equiv function equiv.ops prod unit is_trunc sigma
open eq equiv is_equiv function prod unit is_trunc sigma
variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ : Type}
(f₁₀ : A₀₀ → A₂₀) (f₃₀ : A₂₀ → A₄₀)

39
hott/types/sum.hlean
View file

@ -8,7 +8,7 @@ Theorems about sums/coproducts/disjoint unions
import .pi .equiv logic
open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool
open lift eq is_equiv equiv prod prod.ops is_trunc sigma bool
namespace sum
universe variables u v u' v'
@ -226,9 +226,8 @@ namespace sum
end
definition unit_sum_equiv_cancel_inv (b : B) :
unit_sum_equiv_cancel_map H (unit_sum_equiv_cancel_map H⁻¹ b) = b :=
unit_sum_equiv_cancel_map H (unit_sum_equiv_cancel_map H⁻¹ᵉ b) = b :=
begin
have HH : to_fun H⁻¹ = (to_fun H)⁻¹, begin cases H, reflexivity end,
esimp[unit_sum_equiv_cancel_map], apply sum.rec,
{ intro x, cases x with u Hu, esimp, apply sum.rec,
{ intro x, exfalso, cases x with u' Hu', apply empty_of_inl_eq_inr,
@ -238,28 +237,28 @@ namespace sum
... = H⁻¹ (H (inr _)) : {Hu⁻¹}
... = inr _ : to_left_inv H },
{ intro x, cases x with b' Hb', esimp, cases sum.mem_cases (H⁻¹ (inr b)) with x x,
{ cases x with u' Hu', cases u', apply eq_of_inr_eq_inr, rewrite -HH at Hu',
calc inr b' = H (inl ⋆) : Hb'⁻¹
... = H (H⁻¹ (inr b)) : {(ap (to_fun H) Hu')⁻¹}
... = inr b : to_right_inv H (inr b) },
{ exfalso, cases x with a Ha, rewrite -HH at Ha, apply empty_of_inl_eq_inr,
{ cases x with u' Hu', cases u', apply eq_of_inr_eq_inr,
calc inr b' = H (inl ⋆) : Hb'⁻¹
... = H (H⁻¹ (inr b)) : (ap (to_fun H) Hu')⁻¹
... = inr b : to_right_inv H (inr b)},
{ exfalso, cases x with a Ha, apply empty_of_inl_eq_inr,
cases u, apply concat, apply Hu⁻¹, apply concat, rotate 1, apply !(to_right_inv H),
apply ap (to_fun H), krewrite -HH,
apply ap (to_fun H),
apply concat, rotate 1, apply Ha⁻¹, apply ap inr, esimp,
apply sum.rec, intro x, exfalso, apply empty_of_inl_eq_inr,
apply concat, exact x.2⁻¹, apply Ha,
intro x, cases x with a' Ha', esimp, apply eq_of_inr_eq_inr, apply Ha'⁻¹ ⬝ Ha } } },
{ intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ ⬝ _,
cases sum.mem_cases (to_fun H⁻¹ (inr b)) with x x,
{ cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ (inl ⋆)) with x x,
cases sum.mem_cases (to_fun H⁻¹ᵉ (inr b)) with x x,
{ cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ᵉ (inl ⋆)) with x x,
{ cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr,
calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹
... = H (inl u') : {ap H Hu'}
... = H (inl u) : {!is_prop.elim}
... = H (H⁻¹ (inr b)) : {ap H Hu⁻¹}
... = inr b : to_right_inv H (inr b) },
calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹
... = H (inl u') : ap H Hu'
... = H (inl u) : by rewrite [is_prop.elim u' u]
... = H (H⁻¹ᵉ (inr b)) : ap H Hu⁻¹
... = inr b : to_right_inv H (inr b) },
{ cases x with a Ha, exfalso, apply empty_of_inl_eq_inr,
apply concat, rotate 1, exact Hb', krewrite HH at Ha,
apply concat, rotate 1, exact Hb',
have Ha' : inl ⋆ = H (inr a), by apply !(to_right_inv H)⁻¹ ⬝ ap H Ha,
apply concat Ha', apply ap H, apply ap inr, apply sum.rec,
intro x, cases x with u' Hu', esimp, apply sum.rec,
@ -269,15 +268,15 @@ namespace sum
intro x, exfalso, cases x with a'' Ha'', apply empty_of_inl_eq_inr,
apply Hu⁻¹ ⬝ Ha'', } },
{ cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H,
rewrite -HH, apply Ha'⁻¹ } }
apply Ha'⁻¹ } }
end
definition unit_sum_equiv_cancel : A ≃ B :=
begin
fapply equiv.MK, apply unit_sum_equiv_cancel_map H,
apply unit_sum_equiv_cancel_map H⁻¹,
apply unit_sum_equiv_cancel_map H⁻¹ᵉ,
intro b, apply unit_sum_equiv_cancel_inv,
{ intro a, have H = (H⁻¹)⁻¹, from !equiv.symm_symm⁻¹, rewrite this at {2},
{ intro a, have H = (H⁻¹ᵉ)⁻¹ᵉ, from !equiv.symm_symm⁻¹, rewrite this at {2},
apply unit_sum_equiv_cancel_inv }
end

1
hott/types/trunc.hlean
View file

@ -428,7 +428,6 @@ namespace trunc
{ exact (IH _ _ _)}}}
end
open equiv.ops
definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A)
: P a :=
!trunc_equiv (f a)

6
hott/types/univ.hlean
View file

@ -10,7 +10,7 @@ Theorems about the universe
import .bool .trunc .lift .pullback
open is_trunc bool lift unit eq pi equiv equiv.ops sum sigma fiber prod pullback is_equiv sigma.ops
open is_trunc bool lift unit eq pi equiv sum sigma fiber prod pullback is_equiv sigma.ops
pointed
namespace univ
@ -117,9 +117,9 @@ namespace univ
(λb, sigma_equiv_sigma_right
(λX, !comm_equiv_nondep))
... ≃ Σb (v : ΣX, X), v.1 = fiber f b : sigma_equiv_sigma_right
(λb, !sigma_assoc_equiv⁻¹)
(λb, !sigma_assoc_equiv⁻¹ᵉ)
... ≃ Σb (Y : Type*), Y = fiber f b : sigma_equiv_sigma_right
(λb, sigma_equiv_sigma (pType.sigma_char)⁻¹
(λb, sigma_equiv_sigma (pType.sigma_char)⁻¹ᵉ
(λv, sigma.rec_on v (λx y, equiv.refl)))
... ≃ Σ(Y : Type*) b, Y = fiber f b : sigma_comm_equiv
... ≃ pullback pType.carrier (fiber f) : !pullback.sigma_char⁻¹ᵉ

1
tests/lean/extra/597a.hlean
View file

@ -1,4 +1,3 @@
open equiv
open equiv.ops
constants (A B : Type₀) (f : A ≃ B)
definition foo : A → B := f

3
tests/lean/extra/597b.hlean
View file

@ -1,4 +1,3 @@
open equiv
-- open equiv.ops
-- open equiv
constants (A B : Type₀) (f : A ≃ B)
definition foo : A → B := f -- should fail