feat(library/hott): complete theorems about truncatedness of isomorphism sets
This commit is contained in:
Jakob von Raumer
Leonardo de Moura
parent
5923392395
commit
aad4592cad
4 changed files with 104 additions and 49 deletions
|
|
@ -14,17 +14,26 @@ structure category [class] (ob : Type) extends (precategory ob) :=
|
|||
(iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
|
||||
|
||||
namespace category
|
||||
variables {ob : Type} (C : category ob) {a b : ob}
|
||||
variables {ob : Type} {C : category ob} {a b : ob}
|
||||
include C
|
||||
|
||||
-- Make iso_of_path_equiv a class instance
|
||||
-- TODO: Unsafe class instance?
|
||||
instance [persistent] iso_of_path_equiv
|
||||
|
||||
definition path_of_iso {a b : ob} : (Σ (f : hom a b), is_iso f) → a ≈ b :=
|
||||
definition path_of_iso {a b : ob} : a ≅ b → a ≈ b :=
|
||||
iso_of_path⁻¹
|
||||
|
||||
definition ob_1_type : is_trunc 1 ob := sorry
|
||||
definition foo {a b : ob} :
|
||||
|
||||
definition ob_1_type : is_trunc -2 .+1 .+1 .+1 ob :=
|
||||
begin
|
||||
apply is_trunc_succ, intros (a, b),
|
||||
/-fapply trunc_equiv,
|
||||
exact (@path_of_iso ob C a b),
|
||||
apply inv_closed,
|
||||
exact sorry,-/
|
||||
end
|
||||
|
||||
end category
|
||||
|
||||
|
|
|
|||
68
library/hott/algebra/precategory/iso.lean
Normal file
68
library/hott/algebra/precategory/iso.lean
Normal file
|
|
@ -0,0 +1,68 @@
|
|||
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
import .basic .morphism hott.types.prod
|
||||
|
||||
open path precategory sigma sigma.ops equiv is_equiv function truncation
|
||||
open prod
|
||||
|
||||
namespace morphism
|
||||
variables {ob : Type} [C : precategory ob] include C
|
||||
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
|
||||
|
||||
-- "is_iso f" is equivalent to a certain sigma type
|
||||
definition sigma_equiv_of_is_iso (f : hom a b) :
|
||||
(Σ (g : hom b a), (g ∘ f ≈ id) × (f ∘ g ≈ id)) ≃ is_iso f :=
|
||||
begin
|
||||
fapply (equiv.mk),
|
||||
intro S, apply is_iso.mk,
|
||||
exact (pr₁ S.2),
|
||||
exact (pr₂ S.2),
|
||||
fapply adjointify,
|
||||
intro H, apply (is_iso.rec_on H), intros (g, η, ε),
|
||||
exact (dpair g (pair η ε)),
|
||||
intro H, apply (is_iso.rec_on H), intros (g, η, ε), apply idp,
|
||||
intro S, apply (sigma.rec_on S), intros (g, ηε),
|
||||
apply (prod.rec_on ηε), intros (η, ε), apply idp,
|
||||
end
|
||||
|
||||
-- The structure for isomorphism can be characterized up to equivalence
|
||||
-- by a sigma type.
|
||||
definition sigma_is_iso_equiv ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
|
||||
begin
|
||||
fapply (equiv.mk),
|
||||
intro S, apply isomorphic.mk, apply (S.2),
|
||||
fapply adjointify,
|
||||
intro p, apply (isomorphic.rec_on p), intros (f, H),
|
||||
exact (dpair f H),
|
||||
intro p, apply (isomorphic.rec_on p), intros (f, H), apply idp,
|
||||
intro S, apply (sigma.rec_on S), intros (f, H), apply idp,
|
||||
end
|
||||
|
||||
-- The statement "f is an isomorphism" is a mere proposition
|
||||
definition is_hprop_of_is_iso : is_hset (is_iso f) :=
|
||||
begin
|
||||
apply trunc_equiv,
|
||||
apply (equiv.to_is_equiv (!sigma_equiv_of_is_iso)),
|
||||
apply sigma_trunc,
|
||||
apply (!homH),
|
||||
intro g, apply trunc_prod,
|
||||
repeat (apply succ_is_trunc; apply trunc_succ; apply (!homH)),
|
||||
end
|
||||
|
||||
-- The type of isomorphisms between two objects is a set
|
||||
definition is_hset_iso : is_hset (a ≅ b) :=
|
||||
begin
|
||||
apply trunc_equiv,
|
||||
apply (equiv.to_is_equiv (!sigma_is_iso_equiv)),
|
||||
apply sigma_trunc,
|
||||
apply homH,
|
||||
intro f, apply is_hprop_of_is_iso,
|
||||
end
|
||||
|
||||
-- In a precategory, equal objects are isomorphic
|
||||
definition iso_of_path (p : a ≈ b) : isomorphic a b :=
|
||||
path.rec_on p (isomorphic.mk id)
|
||||
|
||||
end morphism
|
||||
|
|
@ -1,10 +1,10 @@
|
|||
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Floris van Doorn
|
||||
-- Authors: Floris van Doorn, Jakob von Raumer
|
||||
|
||||
import .basic
|
||||
import .basic hott.types.sigma
|
||||
|
||||
open path precategory sigma sigma.ops
|
||||
open path precategory sigma sigma.ops equiv is_equiv function truncation
|
||||
|
||||
namespace morphism
|
||||
variables {ob : Type} [C : precategory ob] include C
|
||||
|
|
@ -130,26 +130,22 @@ namespace morphism
|
|||
|
||||
namespace isomorphic
|
||||
|
||||
--open relation
|
||||
-- openrelation
|
||||
instance [persistent] is_iso
|
||||
|
||||
theorem refl (a : ob) : isomorphic a a :=
|
||||
definition refl (a : ob) : a ≅ a :=
|
||||
mk id
|
||||
|
||||
theorem symm ⦃a b : ob⦄ (H : isomorphic a b) : isomorphic b a :=
|
||||
definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
|
||||
mk (inverse (iso H))
|
||||
|
||||
theorem trans ⦃a b c : ob⦄ (H1 : isomorphic a b) (H2 : isomorphic b c) : isomorphic a c :=
|
||||
definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
|
||||
mk (iso H2 ∘ iso H1)
|
||||
|
||||
--theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic :=
|
||||
--is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
|
||||
end isomorphic
|
||||
|
||||
-- In a precategory, equal objects are isomorphic
|
||||
definition iso_of_path (p : a ≈ b) : isomorphic a b :=
|
||||
path.rec_on p (isomorphic.mk id)
|
||||
|
||||
inductive is_mono [class] (f : a ⟶ b) : Type :=
|
||||
mk : (∀c (g h : hom c a), f ∘ g ≈ f ∘ h → g ≈ h) → is_mono f
|
||||
inductive is_epi [class] (f : a ⟶ b) : Type :=
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ import ..trunc .prod
|
|||
open path sigma sigma.ops equiv is_equiv
|
||||
|
||||
namespace sigma
|
||||
-- remove the ₁'s (globally)
|
||||
variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
|
||||
{D : Πa b, C a b → Type}
|
||||
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
|
||||
|
|
@ -50,9 +51,9 @@ namespace sigma
|
|||
definition dpair_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
|
||||
: dpair (path_sigma p q)..1 (path_sigma p q)..2 ≈ ⟨p, q⟩ :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
generalize q, generalize p,
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply (destruct v), intros (v1, v2, p), generalize v2, --change to revert
|
||||
apply (destruct v), intros (v1, v2, p), generalize v2,
|
||||
apply (path.rec_on p), intros (v2, q),
|
||||
apply (path.rec_on q), apply idp
|
||||
end
|
||||
|
|
@ -74,7 +75,7 @@ namespace sigma
|
|||
definition transport_pr1_path_sigma {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
|
||||
: transport (λx, B' x.1) (path_sigma p q) ≈ transport B' p :=
|
||||
begin
|
||||
reverts (p, q),
|
||||
generalize q, generalize p,
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply (destruct v), intros (v1, v2, p), generalize v2,
|
||||
apply (path.rec_on p), intros (v2, q),
|
||||
|
|
@ -120,7 +121,7 @@ namespace sigma
|
|||
path_sigma_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
|
||||
≈ path_sigma_dpair p1 q1 ⬝ path_sigma_dpair p2 q2 :=
|
||||
begin
|
||||
reverts (b', p2, b'', q1, q2),
|
||||
generalize q2, generalize q1, generalize b'', generalize p2, generalize b',
|
||||
apply (path.rec_on p1), intros (b', p2),
|
||||
apply (path.rec_on p2), intros (b'', q1),
|
||||
apply (path.rec_on q1), intro q2,
|
||||
|
|
@ -132,7 +133,7 @@ namespace sigma
|
|||
path_sigma (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
|
||||
≈ path_sigma p1 q1 ⬝ path_sigma p2 q2 :=
|
||||
begin
|
||||
reverts (p1, q1, p2, q2),
|
||||
generalize q2, generalize p2, generalize q1, generalize p1,
|
||||
apply (destruct u), intros (u1, u2),
|
||||
apply (destruct v), intros (v1, v2),
|
||||
apply (destruct w), intros,
|
||||
|
|
@ -142,7 +143,7 @@ namespace sigma
|
|||
definition path_sigma_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
|
||||
path_sigma_dpair p q ≈ path_sigma_dpair p idp ⬝ path_sigma_dpair idp q :=
|
||||
begin
|
||||
reverts (b', q),
|
||||
generalize q, generalize b',
|
||||
apply (path.rec_on p), intros (b', q),
|
||||
apply (path.rec_on q), apply idp
|
||||
end
|
||||
|
|
@ -171,7 +172,7 @@ namespace sigma
|
|||
q2
|
||||
s
|
||||
-- begin
|
||||
-- reverts (q2, s),
|
||||
-- generalize s, generalize q2,
|
||||
-- apply (path.rec_on r), intros (q2, s),
|
||||
-- apply (path.rec_on s), apply idp
|
||||
-- end
|
||||
|
|
@ -180,7 +181,7 @@ namespace sigma
|
|||
/- A path between paths in a total space is commonly shown component wise. -/
|
||||
definition path_path_sigma {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
|
||||
begin
|
||||
reverts (q, r, s),
|
||||
generalize s, generalize r, generalize q,
|
||||
apply (path.rec_on p),
|
||||
apply (destruct u), intros (u1, u2, q, r, s),
|
||||
apply concat, rotate 1,
|
||||
|
|
@ -188,6 +189,7 @@ namespace sigma
|
|||
apply (path_path_sigma_path_sigma r s)
|
||||
end
|
||||
|
||||
|
||||
/- In Coq they often have to give u and v explicitly when using the following definition -/
|
||||
definition path_path_sigma_uncurried {p q : u ≈ v}
|
||||
(rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
|
||||
|
|
@ -221,7 +223,7 @@ namespace sigma
|
|||
definition transport_sigma_' {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a ≈ a')
|
||||
(bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd ≈ ⟨p ▹ bcd.1, p ▹ bcd.2.1, p ▹D2 bcd.2.2⟩ :=
|
||||
begin
|
||||
revert bcd,
|
||||
generalize bcd,
|
||||
apply (path.rec_on p), intro bcd,
|
||||
apply (destruct bcd), intros (b, cd),
|
||||
apply (destruct cd), intros (c, d),
|
||||
|
|
@ -234,35 +236,15 @@ namespace sigma
|
|||
definition functor_sigma (u : Σa, B a) : Σa', B' a' :=
|
||||
⟨f u.1, g u.1 u.2⟩
|
||||
|
||||
-- variables {A A' : Type} {B : A → Type} {B' : A' → Type} (f : A → A') (g : Πa, B a → B' (f a))
|
||||
-- (H1 : is_equiv f) (H2 : Π (a : A), is_equiv (g a)) (u' : Σ (a' : A'), B' a')
|
||||
-- (a' : A') (b' : B' a')
|
||||
-- check retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))) ≈ b'
|
||||
-- check retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b')))
|
||||
-- check (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b')))
|
||||
-- check retr f a'
|
||||
|
||||
/- Equivalences -/
|
||||
irreducible inv --function.compose
|
||||
--TODO: remove explicit arguments of IsEquiv
|
||||
|
||||
--remove explicit arguments of IsEquiv
|
||||
definition isequiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, @is_equiv (B a) (B' (f a)) (g a)]
|
||||
: is_equiv (functor_sigma f g) :=
|
||||
adjointify (functor_sigma f g)
|
||||
(functor_sigma (f⁻¹) (λ(x : A') (y : B' x),
|
||||
((g (f⁻¹ x))⁻¹ (transport B' (retr f x)⁻¹ y))))
|
||||
-- begin
|
||||
-- intro u',
|
||||
-- apply (destruct u'), intros (a', b'),
|
||||
-- apply (path_sigma (retr f a')),
|
||||
-- -- show retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))) ≈ b',
|
||||
-- -- from sorry
|
||||
-- -- exact (calc
|
||||
-- -- retr f a' ▹ g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))
|
||||
-- -- ≈ retr f a' ▹ ((retr f a')⁻¹ ▹ b') : {retr (g (f⁻¹ a')) _}
|
||||
-- -- ... ≈ b' : transport_pV)
|
||||
-- end
|
||||
proof (λu', sorry) qed
|
||||
proof (λu, sorry) qed
|
||||
/-adjointify (functor_sigma f g)
|
||||
(functor_sigma (f⁻¹) (λ(x : A') (y : B' x), ((g (f⁻¹ x))⁻¹ ((retr f x)⁻¹ ▹ y))))
|
||||
sorry-/
|
||||
sorry
|
||||
|
||||
definition equiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
|
||||
equiv.mk (functor_sigma f g) !isequiv_functor_sigma
|
||||
|
|
|
|||
Loading…
Reference in a new issue