## Stream: Is there code for X?

### Topic: has_terminal.of_is_terminal

#### 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 ?

#### 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)),
}
}
}


#### 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.

#### 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) _) }


#### 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