2015-02-26 18:19:54 +00:00
|
|
|
/-
|
|
|
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
|
|
|
|
|
Module: algebra.category.constructions
|
|
|
|
|
Authors: Floris van Doorn
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
|
|
import .basic algebra.precategory.constructions
|
|
|
|
|
|
|
|
|
|
open eq prod eq eq.ops equiv is_trunc funext pi category.ops morphism category
|
|
|
|
|
|
|
|
|
|
namespace category
|
|
|
|
|
|
|
|
|
|
section hset
|
2015-02-28 00:50:06 +00:00
|
|
|
definition is_univalent_hset (a b : Precategory_hset) : is_equiv (@iso_of_eq _ _ a b) :=
|
2015-02-26 18:19:54 +00:00
|
|
|
sorry
|
|
|
|
|
|
|
|
|
|
definition category_hset [reducible] [instance] : category hset :=
|
2015-02-28 00:50:06 +00:00
|
|
|
category.mk' hset precategory_hset is_univalent_hset
|
2015-02-26 18:19:54 +00:00
|
|
|
|
|
|
|
|
definition Category_hset [reducible] : Category :=
|
|
|
|
|
Category.mk hset category_hset
|
|
|
|
|
|
2015-02-27 05:45:21 +00:00
|
|
|
definition isomorphic_hset_eq_equiv (a b : Category_hset) : (a ≅ b) = (a ≃ b) := sorry
|
2015-02-26 18:19:54 +00:00
|
|
|
|
|
|
|
|
end hset
|
|
|
|
|
namespace ops
|
|
|
|
|
abbreviation set := Category_hset
|
|
|
|
|
end ops
|
|
|
|
|
|
|
|
|
|
end category
|
