conical terminal object

Stream: Infinity-Cosmos

[Emily Riehl]

If anyone wants a task, there are a few sorries in a new PR that I'd love to have filed

variable {C : Type u} [Category.{v} C] [SimplicialCategory C]

/-- `X` is conical terminal if the cone it induces on the empty diagram is a conical limit cone. -/
abbrev IsConicalTerminal (T : C) := IsSLimit (asEmptyCone T)

/-- A conical terminal object is also terminal.-/
def IsConicalTerminal.isTerminal {T : C} (hT : IsConicalTerminal T) : IsTerminal T := hT.isLimit

/-- The defining universal property of a conical terminal object gives an isomorphism of homs.-/
def IsConicalTerminal.sHomIso {T : C} (hT : IsConicalTerminal T) (X : C) : sHom X T ≅ ⊤_ SSet := by
  let iso : sHom X T ≅ _ := limitComparisonIso _ X hT
  sorry

/-- Transport a term of type `IsTerminal` across an isomorphism. -/
def IsConicalTerminal.ofIso {Y Z : C} (hY : IsConicalTerminal Y) (i : Y ≅ Z) :
    IsConicalTerminal Z := sorry
  -- IsLimit.ofIsoLimit hY
  --   { hom := { hom := i.hom }
  --     inv := { hom := i.inv } }

namespace HasConicalTerminal
variable [HasConicalTerminal C]

variable (C) in
noncomputable def conicalTerminal : C := conicalLimit (Functor.empty.{0} C)

def conicalTerminalIsConicalTerminal : IsConicalTerminal (conicalTerminal C) where
  isLimit := sorry
  isSLimit := sorry

[Nick Ward]

I opened a (WIP) PR at cosmos#64 that fills in the first two sorries. I will take a look at the last one today or tomorrow.

[Nick Ward]

@Emily Riehl cosmos#64 should be ready for review!

[Emily Riehl]

@Nick Ward thanks! Very happy to have this merged.

I guess the noncomputability is inevitable since it all comes down to SSet.instChosenFiniteProducts.

I'll go ahead and merge Leibniz into main and then get caught up on the homotopy category stuff.

[Nick Ward]

This is only tangentially relevant here, but mathlib4#19932 adds the eHomCongr isomorphism that was originally a part of cosmos#64.

[Dagur Asgeirsson]

I added a few small comments, otherwise lgtm

[Nick Ward]

Much appreciated @Dagur Asgeirsson!

[Emily Riehl]

Tagging @Daniel Carranza to let him know about these new defs.

[Daniel Carranza]

This seems great to know about - thank you!