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

feat(hott/algebra) finish functor category up to that missing sigma characterization

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-31 19:36:07 -05:00 committed by Leonardo de Moura
parent 31d1076bd7
commit 4af0a911b3
1 changed files with 24 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
hott/algebra/precategory/constructions.hlean
View file

@ -6,13 +6,13 @@
import .natural_transformation import .natural_transformation
import types.prod types.sigma import types.prod types.sigma types.pi
open eq prod eq eq.ops open eq prod eq eq.ops equiv truncation
namespace precategory namespace precategory
namespace opposite namespace opposite
section
definition opposite {ob : Type} (C : precategory ob) : precategory ob := definition opposite {ob : Type} (C : precategory ob) : precategory ob :=
mk (λ a b, hom b a) mk (λ a b, hom b a)
(λ b a, !homH) (λ b a, !homH)
@ -34,25 +34,33 @@ namespace precategory
-- take the trick they use in Coq-HoTT, and introduce a further -- take the trick they use in Coq-HoTT, and introduce a further
-- axiom in the definition of precategories that provides thee -- axiom in the definition of precategories that provides thee
-- symmetric associativity proof. -- symmetric associativity proof.
theorem op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) = C := universe variables l k
definition op_op' {ob : Type} (C : precategory.{l k} ob) : opposite (opposite C) = C :=
sorry sorry
/-begin
apply (rec_on C), intros (hom', homH', comp', ID', assoc', id_left', id_right'),
apply (ap (λassoc'', precategory.mk hom' @homH' comp' ID' assoc'' id_left' id_right')),
apply (@funext.path_pi _ _ _ _ assoc'), intro a,
apply (@funext.path_pi _ _ _ _ (@assoc' a)), intro b,
apply (@funext.path_pi _ _ _ _ (@assoc' a b)), intro c,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c)), intro d,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c d)), intro f,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c d f)), intro g,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c d f g)), intro h,
apply ap,
show @assoc ob (@opposite ob (@precategory.mk ob hom' @homH' comp' ID' assoc' id_left' id_right')) d c b a h
g
f ⁻¹ = @assoc' a b c d f g h,
begin
apply is_hset.elim,
end
end-/
theorem op_op : Opposite (Opposite C) = C := theorem op_op : Opposite (Opposite C) = C :=
(ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal (ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal
end
end opposite end opposite
/-definition type_category : precategory Type :=
mk (λa b, a → b)
(λ a b c, function.compose)
(λ a, function.id)
(λ a b c d h g f, symm (function.compose_assoc h g f))
(λ a b f, function.compose_id_left f)
(λ a b f, function.compose_id_right f)
definition Type_category : Category := Mk type_category-/
-- Note: Discrete precategory doesn't really make sense in HoTT, -- Note: Discrete precategory doesn't really make sense in HoTT,
-- We'll define a discrete _category_ later. -- We'll define a discrete _category_ later.
/-section /-section
@ -155,7 +163,7 @@ namespace precategory
variables (C D : Precategory) variables (C D : Precategory)
definition functor_category [fx : funext] : precategory (functor C D) := definition functor_category [fx : funext] : precategory (functor C D) :=
mk (λa b, natural_transformation a b) mk (λa b, natural_transformation a b)
sorry --TODO: Prove that the nat trafos between two functors are an hset (λ a b, @natural_transformation.to_hset C D a b)
(λ a b c g f, natural_transformation.compose g f) (λ a b c g f, natural_transformation.compose g f)
(λ a, natural_transformation.id) (λ a, natural_transformation.id)
(λ a b c d h g f, !natural_transformation.assoc) (λ a b c d h g f, !natural_transformation.assoc)