Zulip Chat Archive

Stream: Is there code for X?

Topic: has_terminal.of_is_terminal


view this post on Zulip Adam Topaz (Mar 30 2021 at 18:34):

Do we have something which gives a docs#category_theory.limits.has_terminal instance from a term of type docs#category_theory.limits.is_terminal ?

view this post on Zulip Greg Price (Mar 30 2021 at 19:21):

Here's a rather messy solution:

import category_theory.limits.shapes.terminal

universes v u

open category_theory
open category_theory.category
open category_theory.limits

variables {C : Type u} [category.{v} C]
variables {X Y Z : C}

example (t : is_terminal X) : has_terminal C :=
{ has_limit := λ F, has_limit.mk {
    cone := { X := X, π := (by tidy)},
    is_limit := {
      lift := λ s, t.lift (as_empty_cone s.X),
      uniq' := (λ s m w,
        is_limit.uniq t (as_empty_cone s.X) m (by intros; cases j)),
    }
  }
}

view this post on Zulip Greg Price (Mar 30 2021 at 19:21):

I am surprised not to find a lemma for it, but I may be just missing it.

view this post on Zulip Markus Himmel (Mar 30 2021 at 19:57):

I also can't find it. Here's my attempt at a proof:

example {X : C} (h : is_terminal X) : has_terminal C :=
{ has_limit := λ F, have has_limit (functor.empty C), from has_limit.mk _, h⟩,
    by exactI has_limit_of_iso (functor.empty_ext (functor.empty C) _) }

view this post on Zulip Adam Topaz (Mar 30 2021 at 20:03):

I might add it to this later on: #6966


Last updated: May 07 2021 at 19:12 UTC