has_terminal.of_is_terminal

Stream: Is there code for X?

[Adam Topaz]

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]

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]

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

[Markus Himmel]

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]

I might add it to this later on: #6966