style(hott/algebra/precategory): some cleanup
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
57514244b1
commit
8948926a07
8 changed files with 10 additions and 82 deletions
|
|
@ -103,10 +103,6 @@ namespace category
|
|||
apply inverse, apply naturality_iso}
|
||||
end
|
||||
|
||||
--the following error is a bug?
|
||||
-- definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) :=
|
||||
-- λ(F G : D ^c C), adjointify _ eq_of_iso_functor sorry sorry
|
||||
|
||||
definition iso_of_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η :=
|
||||
begin
|
||||
apply iso.eq_mk,
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.yoneda
|
||||
|
|
@ -69,6 +69,8 @@ structure isomorphism (C D : Precategory) :=
|
|||
|
||||
namespace category
|
||||
|
||||
-- infix `⊣`:55 := adjoint
|
||||
|
||||
infix `⋍`:25 := equivalence -- \backsimeq
|
||||
infix `≌`:25 := isomorphism -- \backcong
|
||||
--TODO: add shortcuts for Σ⋍≌▹
|
||||
|
|
|
|||
|
|
@ -139,5 +139,3 @@ namespace category
|
|||
Precategory.rec (λob c, idp) C
|
||||
|
||||
end category
|
||||
|
||||
open category
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.constructions
|
||||
|
|
@ -166,8 +166,6 @@ namespace category
|
|||
definition Precategory_functor [reducible] (D C : Precategory) : Precategory :=
|
||||
precategory.Mk (precategory_functor D C)
|
||||
|
||||
-- definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory :=
|
||||
-- Precategory_functor D C
|
||||
end
|
||||
namespace ops
|
||||
infixr `^c`:35 := Precategory_functor
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.functor
|
||||
|
|
@ -77,13 +77,6 @@ namespace functor
|
|||
apply idp
|
||||
end))))
|
||||
|
||||
-- definition functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
|
||||
-- {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂)
|
||||
-- (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f)
|
||||
-- : functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
|
||||
-- functor_mk_eq' id₁ id₂ comp₁ comp₂ idp
|
||||
-- (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c'))))
|
||||
|
||||
definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),
|
||||
(Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
|
||||
functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq))
|
||||
|
|
@ -109,7 +102,6 @@ namespace functor
|
|||
|
||||
set_option apply.class_instance false
|
||||
-- "functor C D" is equivalent to a certain sigma type
|
||||
set_option unifier.max_steps 38500
|
||||
protected definition sigma_char :
|
||||
(Σ (to_fun_ob : C → D)
|
||||
(to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b)),
|
||||
|
|
@ -123,7 +115,7 @@ namespace functor
|
|||
exact (pr₁ S.2.2), exact (pr₂ S.2.2)},
|
||||
{intro F,
|
||||
cases F with (d1, d2, d3, d4),
|
||||
exact (sigma.mk d1 (sigma.mk d2 (pair d3 (@d4))))},
|
||||
exact ⟨d1, d2, (d3, @d4)⟩},
|
||||
{intro F,
|
||||
cases F,
|
||||
apply idp},
|
||||
|
|
@ -150,11 +142,6 @@ namespace functor
|
|||
apply is_trunc_eq, apply is_trunc_succ, apply !homH},
|
||||
end
|
||||
|
||||
--STRANGE ERROR:
|
||||
-- definition functor_mk_eq'_idp {F₁ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
|
||||
-- (id₁ id₂ comp₁ comp₂) : functor_mk_eq' id₁ id₂ comp₁ comp₂ idp idp = idp :=
|
||||
-- sorry
|
||||
|
||||
definition functor_mk_eq'_idp (F : C → D) (H : Π(a b : C), hom a b → hom (F a) (F b))
|
||||
(id comp) : functor_mk_eq' id id comp comp (idpath F) (idpath H) = idp :=
|
||||
begin
|
||||
|
|
@ -166,7 +153,6 @@ namespace functor
|
|||
definition functor_eq'_idp (F : C ⇒ D) : functor_eq' idp idp = (idpath F) :=
|
||||
by (cases F; apply functor_mk_eq'_idp)
|
||||
|
||||
--TODO: do we want a similar theorem for functor_eq?
|
||||
definition functor_eq_eta' {F₁ F₂ : C ⇒ D} (p : F₁ = F₂)
|
||||
: functor_eq' (ap to_fun_ob p) (!transport_compose⁻¹ ⬝ apD to_fun_hom p) = p :=
|
||||
begin
|
||||
|
|
@ -176,36 +162,6 @@ namespace functor
|
|||
apply idp_con,
|
||||
end
|
||||
|
||||
-- definition functor_eq_eta {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
|
||||
-- (p : functor.mk ob₁ hom₁ id₁ comp₁ = functor.mk ob₂ hom₂ id₂ comp₂)
|
||||
-- : functor_mk_eq' _ _ _ _ (ap010 to_fun_ob p) _ = p :=
|
||||
-- sorry
|
||||
--set_option pp.universes true
|
||||
-- set_option pp.notation false
|
||||
-- set_option pp.implicit true
|
||||
|
||||
-- TODO: REMOVE?
|
||||
-- definition functor_mk_eq'2 {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
|
||||
-- {pob₁ pob₂ : ob₁ = ob₂} (phom₁ : pob₁ ▹ hom₁ = hom₂) (phom₂ : pob₂ ▹ hom₁ = hom₂)
|
||||
-- (r : pob₁ = pob₂) : functor_mk_eq' id₁ id₂ comp₁ comp₂ pob₁ phom₁
|
||||
-- = functor_mk_eq' id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
|
||||
-- begin
|
||||
-- cases r,
|
||||
-- apply (ap (functor_mk_eq' id₁ id₂ @comp₁ @comp₂ pob₂)),
|
||||
-- apply is_hprop.elim
|
||||
-- end
|
||||
|
||||
-- definition functor_mk_eq2 {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} {pob₁ pob₂ : ob₁ ∼ ob₂}
|
||||
-- (phom₁ : Π(a b : C) (f : hom a b), hom_of_eq (pob₁ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₁ a) = hom₂ a b f)
|
||||
-- (phom₂ : Π(a b : C) (f : hom a b), hom_of_eq (pob₂ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₂ a) = hom₂ a b f)
|
||||
-- (r : pob₁ = pob₂) : functor_mk_eq id₁ id₂ comp₁ comp₂ pob₁ phom₁
|
||||
-- = functor_mk_eq id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
|
||||
-- begin
|
||||
-- cases r,
|
||||
-- apply (ap (functor_mk_eq id₁ id₂ @comp₁ @comp₂ pob₂)),
|
||||
-- apply is_hprop.elim
|
||||
-- end
|
||||
|
||||
definition functor_eq2' {F₁ F₂ : C ⇒ D} {p₁ p₂ : to_fun_ob F₁ = to_fun_ob F₂} (q₁ q₂)
|
||||
(r : p₁ = p₂) : functor_eq' p₁ q₁ = functor_eq' p₂ q₂ :=
|
||||
by cases r; apply (ap (functor_eq' p₂)); apply is_hprop.elim
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.iso
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.nat_trans
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||||
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.precategory.yoneda
|
||||
|
|
@ -15,7 +15,6 @@ set_option pp.beta true
|
|||
namespace yoneda
|
||||
set_option class.conservative false
|
||||
|
||||
--TODO: why does this take so much steps? (giving more information than "assoc" hardly helps)
|
||||
definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C}
|
||||
(f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
|
||||
: (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
|
||||
|
|
@ -25,7 +24,6 @@ namespace yoneda
|
|||
... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _)
|
||||
... = _ : by rewrite (assoc f2 f3 f4)
|
||||
|
||||
--disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop
|
||||
definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
|
||||
functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2)
|
||||
(λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
|
||||
|
|
@ -200,7 +198,7 @@ end functor
|
|||
open functor
|
||||
|
||||
namespace yoneda
|
||||
-- or should this be defined as "yoneda_embedding Cᵒᵖ"?
|
||||
--should this be defined as "yoneda_embedding Cᵒᵖ"?
|
||||
definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
|
||||
functor_curry !hom_functor
|
||||
|
||||
|
|
@ -208,23 +206,3 @@ namespace yoneda
|
|||
functor_curry (!hom_functor ∘f !functor_prod_flip)
|
||||
|
||||
end yoneda
|
||||
|
||||
-- Coq uses unit/counit definitions as basic
|
||||
|
||||
-- open yoneda precategory.product precategory.opposite functor morphism
|
||||
-- --universe levels are given explicitly because Lean uses 6 variables otherwise
|
||||
|
||||
-- structure adjoint.{u v} [C D : Precategory.{u v}] (F : C ⇒ D) (G : D ⇒ C) : Type.{max u v} :=
|
||||
-- (nat_iso : (hom_functor D) ∘f (prod_functor (opposite_functor F) (functor.ID D)) ⟹
|
||||
-- (hom_functor C) ∘f (prod_functor (functor.ID (Cᵒᵖ)) G))
|
||||
-- (is_iso_nat_iso : is_iso nat_iso)
|
||||
|
||||
-- infix `⊣`:55 := adjoint
|
||||
|
||||
-- namespace adjoint
|
||||
-- universe variables l1 l2
|
||||
-- variables [C D : Precategory.{l1 l2}] (F : C ⇒ D) (G : D ⇒ C)
|
||||
|
||||
|
||||
|
||||
-- end adjoint
|
||||
|
|
|
|||
Loading…
Reference in a new issue