You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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@{SetSet u SetSet}])
(f
g : x ~{ Sets@{SetSet u SetSet}
}~> {| 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.
The text was updated successfully, but these errors were encountered:
With
Printing Universes
enabled, the full definition is as follows:This imposes a lot of unnecessary constraints on various universes to be
Set
, which then quickly propagates throughout the code from whereverSets_Terminal
is used.The text was updated successfully, but these errors were encountered: