search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
748 stars 69 forks source link

Sets_Terminal is insufficiently universe-polymorphic #126

Closed nickmertin closed 1 year ago

nickmertin commented 1 year ago

With Printing Universes enabled, the full definition is as follows:

Sets_Terminal@{u} = 
{|
  Terminal.terminal_obj := {| carrier := poly_unit@{Set}; is_setoid := Unit_Setoid@{Set} |};
  Terminal.one :=
    λ x : obj[Sets@{Set Set u Set Set}],
    {| morphism := λ _ : x, ttt@{Set}; proper_morphism := Sets.Sets_Terminal_obligation_1@{u} x |};
  Terminal.one_unique :=
    λ (x : obj[Sets@{Set Set u Set Set}])
    (f
     g : x ~{ Sets@{Set Set u Set Set}
         }~> {| carrier := poly_unit@{Set}; is_setoid := Unit_Setoid@{Set} |}),
    Sets.Sets_Terminal_obligation_2@{u} x f g
|}
     : Terminal.Terminal@{u Set}
(* u |= Set < u *)

This imposes a lot of unnecessary constraints on various universes to be Set, which then quickly propagates throughout the code from wherever Sets_Terminal is used.