Commit 2019-04-01 16:13 2f088fc1

View on Github →

feat(category_theory): working in Sort rather than Type (#824)

Estimated changes

Modified src/category_theory/adjunction.lean

Modified src/category_theory/category.lean

modified theorem category_theory.End.mul_def

modified theorem category_theory.End.one_def

modified def category_theory.large_category

modified def category_theory.small_category

Modified src/category_theory/comma.lean

modified def category_theory.over

modified def category_theory.under

Modified src/category_theory/concrete_category.lean

modified structure category_theory.bundled

modified def category_theory.forget

modified def category_theory.mk_ob

Modified src/category_theory/const.lean

Modified src/category_theory/discrete_category.lean

Modified src/category_theory/eq_to_hom.lean

Modified src/category_theory/equivalence.lean

modified structure category_theory.equivalence

Modified src/category_theory/full_subcategory.lean

modified def category_theory.induced_category

Modified src/category_theory/fully_faithful.lean

Modified src/category_theory/functor.lean

modified structure category_theory.functor

Modified src/category_theory/functor_category.lean

Modified src/category_theory/groupoid.lean

modified def category_theory.large_groupoid

modified def category_theory.small_groupoid

Modified src/category_theory/instances/monoids.lean

Created src/category_theory/instances/rel.lean

added def category_theory.rel

Modified src/category_theory/isomorphism.lean

modified structure category_theory.iso

Modified src/category_theory/limits/cones.lean

added theorem category_theory.limits.cocone.extend_ι

added theorem category_theory.limits.cone.extend_π

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/limits.lean

modified theorem category_theory.limits.colimit.map_post

modified theorem category_theory.limits.colimit.pre_post

modified def category_theory.limits.is_colimit.of_faithful

modified def category_theory.limits.is_limit.of_faithful

modified theorem category_theory.limits.limit.map_post

modified theorem category_theory.limits.limit.pre_post

Modified src/category_theory/limits/over.lean

Modified src/category_theory/limits/preserves.lean

Modified src/category_theory/natural_isomorphism.lean

Modified src/category_theory/natural_transformation.lean

modified structure category_theory.nat_trans

Modified src/category_theory/opposites.lean

modified theorem category_theory.functor.hom_obj

modified theorem category_theory.functor.hom_pairing_map

modified theorem category_theory.opposite.op_mul

modified theorem category_theory.opposite.op_one

modified theorem category_theory.opposite.unop_mul

modified theorem category_theory.opposite.unop_one

modified def category_theory.opposite

Modified src/category_theory/pempty.lean

Modified src/category_theory/products.lean

Modified src/category_theory/punit.lean

Modified src/category_theory/types.lean

modified theorem category_theory.types_comp

modified theorem category_theory.types_hom

modified theorem category_theory.types_id

Modified src/category_theory/whiskering.lean

Modified src/category_theory/yoneda.lean

modified def category_theory.coyoneda

modified def category_theory.yoneda