fix(hott): make sure there are no sorry's visible
This commit is contained in:
parent
7e52c49dce
commit
a8964adb9c
6 changed files with 56 additions and 54 deletions
|
@ -11,10 +11,10 @@ open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_
|
||||||
namespace category
|
namespace category
|
||||||
variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C}
|
variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C}
|
||||||
|
|
||||||
-- do we want to have a structure "is_adjoint" and define
|
-- TODO: define a structure "adjoint" and then define
|
||||||
-- structure is_left_adjoint (F : C ⇒ D) :=
|
-- structure is_left_adjoint (F : C ⇒ D) :=
|
||||||
-- (right_adjoint : D ⇒ C) -- G
|
-- (G : D ⇒ C) -- G
|
||||||
-- (is_adjoint : adjoint F right_adjoint)
|
-- (is_adjoint : adjoint F G)
|
||||||
|
|
||||||
structure is_left_adjoint [class] (F : C ⇒ D) :=
|
structure is_left_adjoint [class] (F : C ⇒ D) :=
|
||||||
(G : D ⇒ C)
|
(G : D ⇒ C)
|
||||||
|
@ -27,13 +27,6 @@ namespace category
|
||||||
abbreviation unit := @is_left_adjoint.η
|
abbreviation unit := @is_left_adjoint.η
|
||||||
abbreviation counit := @is_left_adjoint.ε
|
abbreviation counit := @is_left_adjoint.ε
|
||||||
|
|
||||||
-- structure is_left_adjoint [class] (F : C ⇒ D) :=
|
|
||||||
-- (right_adjoint : D ⇒ C) -- G
|
|
||||||
-- (unit : functor.id ⟹ right_adjoint ∘f F) -- η
|
|
||||||
-- (counit : F ∘f right_adjoint ⟹ functor.id) -- ε
|
|
||||||
-- (H : Π(c : C), (counit (F c)) ∘ (F (unit c)) = ID (F c))
|
|
||||||
-- (K : Π(d : D), (right_adjoint (counit d)) ∘ (unit (right_adjoint d)) = ID (right_adjoint d))
|
|
||||||
|
|
||||||
structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F :=
|
structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F :=
|
||||||
mk' ::
|
mk' ::
|
||||||
(is_iso_unit : is_iso η)
|
(is_iso_unit : is_iso η)
|
||||||
|
@ -44,10 +37,6 @@ namespace category
|
||||||
--a second notation for the inverse, which is not overloaded
|
--a second notation for the inverse, which is not overloaded
|
||||||
postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse
|
postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse
|
||||||
|
|
||||||
structure equivalence (C D : Precategory) :=
|
|
||||||
(to_functor : C ⇒ D)
|
|
||||||
(struct : is_equivalence to_functor)
|
|
||||||
|
|
||||||
--TODO: review and change
|
--TODO: review and change
|
||||||
definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f'
|
definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f'
|
||||||
definition full [class] (F : C ⇒ D) := Π⦃c c' : C⦄, is_surjective (@(to_fun_hom F) c c')
|
definition full [class] (F : C ⇒ D) := Π⦃c c' : C⦄, is_surjective (@(to_fun_hom F) c c')
|
||||||
|
@ -57,6 +46,10 @@ namespace category
|
||||||
definition is_weak_equivalence [class] (F : C ⇒ D) := fully_faithful F × essentially_surjective F
|
definition is_weak_equivalence [class] (F : C ⇒ D) := fully_faithful F × essentially_surjective F
|
||||||
definition is_isomorphism [class] (F : C ⇒ D) := fully_faithful F × is_equiv (to_fun_ob F)
|
definition is_isomorphism [class] (F : C ⇒ D) := fully_faithful F × is_equiv (to_fun_ob F)
|
||||||
|
|
||||||
|
structure equivalence (C D : Precategory) :=
|
||||||
|
(to_functor : C ⇒ D)
|
||||||
|
(struct : is_equivalence to_functor)
|
||||||
|
|
||||||
structure isomorphism (C D : Precategory) :=
|
structure isomorphism (C D : Precategory) :=
|
||||||
(to_functor : C ⇒ D)
|
(to_functor : C ⇒ D)
|
||||||
(struct : is_isomorphism to_functor)
|
(struct : is_isomorphism to_functor)
|
||||||
|
@ -69,10 +62,10 @@ namespace category
|
||||||
: is_equiv (@(to_fun_hom F) c c') :=
|
: is_equiv (@(to_fun_hom F) c c') :=
|
||||||
!H
|
!H
|
||||||
|
|
||||||
definition is_iso_unit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (unit F) :=
|
definition is_iso_unit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (unit F) :=
|
||||||
!is_equivalence.is_iso_unit
|
!is_equivalence.is_iso_unit
|
||||||
|
|
||||||
definition is_iso_counit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (counit F) :=
|
definition is_iso_counit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (counit F) :=
|
||||||
!is_equivalence.is_iso_counit
|
!is_equivalence.is_iso_counit
|
||||||
|
|
||||||
-- theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
|
-- theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
|
||||||
|
@ -127,19 +120,6 @@ namespace category
|
||||||
-- rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]},
|
-- rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]},
|
||||||
-- end
|
-- end
|
||||||
|
|
||||||
section
|
|
||||||
variables (F G)
|
|
||||||
variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
|
|
||||||
include η ε
|
|
||||||
--definition inverse_of_unit_counit
|
|
||||||
|
|
||||||
definition is_equivalence.mk : is_equivalence F :=
|
|
||||||
begin
|
|
||||||
exact sorry
|
|
||||||
end
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
definition full_of_fully_faithful (H : fully_faithful F) : full F :=
|
definition full_of_fully_faithful (H : fully_faithful F) : full F :=
|
||||||
λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv))
|
λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv))
|
||||||
|
|
||||||
|
@ -155,16 +135,6 @@ namespace category
|
||||||
{ apply K}
|
{ apply K}
|
||||||
end
|
end
|
||||||
|
|
||||||
definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
|
|
||||||
: fully_faithful F :=
|
|
||||||
begin
|
|
||||||
intro c c',
|
|
||||||
fapply adjointify,
|
|
||||||
{ intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c},
|
|
||||||
{ intro g, rewrite [+respect_comp], exact sorry},
|
|
||||||
{ exact sorry},
|
|
||||||
end
|
|
||||||
|
|
||||||
definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
|
definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
|
||||||
: split_essentially_surjective F :=
|
: split_essentially_surjective F :=
|
||||||
begin
|
begin
|
||||||
|
@ -175,6 +145,32 @@ namespace category
|
||||||
|
|
||||||
/-
|
/-
|
||||||
|
|
||||||
|
definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
|
||||||
|
: fully_faithful F :=
|
||||||
|
begin
|
||||||
|
intro c c',
|
||||||
|
fapply adjointify,
|
||||||
|
{ intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c},
|
||||||
|
{ intro g, rewrite [+respect_comp,▸*],
|
||||||
|
krewrite [natural_map_inverse], xrewrite [respect_inv'],
|
||||||
|
apply inverse_comp_eq_of_eq_comp,
|
||||||
|
exact sorry /-this is basically the naturality of the counit-/ },
|
||||||
|
{ exact sorry},
|
||||||
|
end
|
||||||
|
|
||||||
|
section
|
||||||
|
variables (F G)
|
||||||
|
variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
|
||||||
|
include η ε
|
||||||
|
--definition inverse_of_unit_counit
|
||||||
|
|
||||||
|
definition is_equivalence.mk : is_equivalence F :=
|
||||||
|
begin
|
||||||
|
exact sorry
|
||||||
|
end
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
|
definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
|
||||||
sorry
|
sorry
|
||||||
|
|
||||||
|
|
|
@ -77,7 +77,9 @@ namespace category
|
||||||
|
|
||||||
local attribute componentwise_is_iso [instance]
|
local attribute componentwise_is_iso [instance]
|
||||||
|
|
||||||
|
variable {isoη}
|
||||||
definition natural_map_inverse : natural_map η⁻¹ c = (η c)⁻¹ := idp
|
definition natural_map_inverse : natural_map η⁻¹ c = (η c)⁻¹ := idp
|
||||||
|
variable [isoη]
|
||||||
|
|
||||||
definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ :=
|
definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ :=
|
||||||
calc
|
calc
|
||||||
|
|
|
@ -323,29 +323,32 @@ namespace iso
|
||||||
H⁻¹ ▸ comp_inverse_cancel_left q g
|
H⁻¹ ▸ comp_inverse_cancel_left q g
|
||||||
definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f :=
|
definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f :=
|
||||||
H⁻¹ ▸ inverse_comp_cancel_right f q
|
H⁻¹ ▸ inverse_comp_cancel_right f q
|
||||||
definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p :=
|
|
||||||
H⁻¹ ▸ inverse_comp_cancel_left q p
|
|
||||||
definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r :=
|
|
||||||
H⁻¹ ▸ comp_inverse_cancel_right r q
|
|
||||||
definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y :=
|
definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y :=
|
||||||
(comp_eq_of_eq_inverse_comp H⁻¹)⁻¹
|
(comp_eq_of_eq_inverse_comp H⁻¹)⁻¹
|
||||||
definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q :=
|
definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q :=
|
||||||
(comp_eq_of_eq_comp_inverse H⁻¹)⁻¹
|
(comp_eq_of_eq_comp_inverse H⁻¹)⁻¹
|
||||||
|
variable {Hq}
|
||||||
|
definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p :=
|
||||||
|
H⁻¹ ▸ inverse_comp_cancel_left q p
|
||||||
|
definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r :=
|
||||||
|
H⁻¹ ▸ comp_inverse_cancel_right r q
|
||||||
definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z :=
|
definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z :=
|
||||||
(inverse_comp_eq_of_eq_comp H⁻¹)⁻¹
|
(inverse_comp_eq_of_eq_comp H⁻¹)⁻¹
|
||||||
definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ :=
|
definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ :=
|
||||||
(comp_inverse_eq_of_eq_comp H⁻¹)⁻¹
|
(comp_inverse_eq_of_eq_comp H⁻¹)⁻¹
|
||||||
|
|
||||||
definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹
|
definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹
|
||||||
definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹
|
definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹
|
||||||
|
definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h :=
|
||||||
|
(eq_inverse_of_comp_eq_id' H⁻¹)⁻¹
|
||||||
|
definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h :=
|
||||||
|
(eq_inverse_of_comp_eq_id H⁻¹)⁻¹
|
||||||
|
variable [Hq]
|
||||||
definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q :=
|
definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q :=
|
||||||
eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q
|
eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q
|
||||||
definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q :=
|
definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q :=
|
||||||
eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q
|
eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q
|
||||||
definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹
|
definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹
|
||||||
definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹
|
definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹
|
||||||
definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h :=
|
|
||||||
(eq_inverse_of_comp_eq_id' H⁻¹)⁻¹
|
|
||||||
definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h :=
|
|
||||||
(eq_inverse_of_comp_eq_id H⁻¹)⁻¹
|
|
||||||
end
|
end
|
||||||
end iso
|
end iso
|
||||||
|
|
|
@ -76,7 +76,7 @@ namespace torus
|
||||||
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
|
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
|
||||||
!elim_incl1
|
!elim_incl1
|
||||||
|
|
||||||
definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
|
theorem elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
|
||||||
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1)
|
(Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1)
|
||||||
: square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
|
: square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
|
||||||
Ps
|
Ps
|
||||||
|
|
|
@ -208,13 +208,14 @@ namespace eq
|
||||||
|
|
||||||
infix ~ := homotopy
|
infix ~ := homotopy
|
||||||
|
|
||||||
protected definition homotopy.refl [refl] [reducible] (f : Πx, P x) : f ~ f :=
|
protected definition homotopy.refl [refl] [reducible] [unfold-full] (f : Πx, P x) : f ~ f :=
|
||||||
λ x, idp
|
λ x, idp
|
||||||
|
|
||||||
protected definition homotopy.symm [symm] [reducible] {f g : Πx, P x} (H : f ~ g) : g ~ f :=
|
protected definition homotopy.symm [symm] [reducible] [unfold-full] {f g : Πx, P x} (H : f ~ g)
|
||||||
|
: g ~ f :=
|
||||||
λ x, (H x)⁻¹
|
λ x, (H x)⁻¹
|
||||||
|
|
||||||
protected definition homotopy.trans [trans] [reducible] {f g h : Πx, P x}
|
protected definition homotopy.trans [trans] [reducible] [unfold-full] {f g h : Πx, P x}
|
||||||
(H1 : f ~ g) (H2 : g ~ h) : f ~ h :=
|
(H1 : f ~ g) (H2 : g ~ h) : f ~ h :=
|
||||||
λ x, H1 x ⬝ H2 x
|
λ x, H1 x ⬝ H2 x
|
||||||
|
|
||||||
|
@ -287,12 +288,12 @@ namespace eq
|
||||||
definition ap_id (p : x = y) : ap id p = p :=
|
definition ap_id (p : x = y) : ap id p = p :=
|
||||||
eq.rec_on p idp
|
eq.rec_on p idp
|
||||||
|
|
||||||
definition ap_compose (g : B → C) (f : A → B) {x y : A} (p : x = y) :
|
definition ap_compose [unfold 8] (g : B → C) (f : A → B) {x y : A} (p : x = y) :
|
||||||
ap (g ∘ f) p = ap g (ap f p) :=
|
ap (g ∘ f) p = ap g (ap f p) :=
|
||||||
eq.rec_on p idp
|
eq.rec_on p idp
|
||||||
|
|
||||||
-- Sometimes we don't have the actual function [compose].
|
-- Sometimes we don't have the actual function [compose].
|
||||||
definition ap_compose' (g : B → C) (f : A → B) {x y : A} (p : x = y) :
|
definition ap_compose' [unfold 8] (g : B → C) (f : A → B) {x y : A} (p : x = y) :
|
||||||
ap (λa, g (f a)) p = ap g (ap f p) :=
|
ap (λa, g (f a)) p = ap g (ap f p) :=
|
||||||
eq.rec_on p idp
|
eq.rec_on p idp
|
||||||
|
|
||||||
|
|
|
@ -429,7 +429,7 @@ order for the change to take effect."
|
||||||
("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵"))
|
("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵"))
|
||||||
|
|
||||||
("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜"))
|
("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜"))
|
||||||
("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿"))
|
("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) ("hom" . ("⟶"))
|
||||||
("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭"))
|
("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭"))
|
||||||
|
|
||||||
("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍"))
|
("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍"))
|
||||||
|
|
Loading…
Reference in a new issue