Loogle!

Result

Found 269 declarations mentioning CategoryTheory.Limits.IsTerminal. Of these, only the first 200 are shown.

• CategoryTheory.Limits.IsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)
• CategoryTheory.Limits.initialOpOfTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.op X)
• CategoryTheory.Limits.terminalOpOfInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.op X)
• CategoryTheory.Limits.IsInitial.op 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.op X)
• CategoryTheory.Limits.IsTerminal.op 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.op X)
• CategoryTheory.Limits.initialUnopOfTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (t : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.unop X)
• CategoryTheory.Limits.terminalUnopOfInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (t : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.unop X)
• CategoryTheory.Limits.IsInitial.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsTerminal (Opposite.unop X)
• CategoryTheory.Limits.IsTerminal.from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) (Y : C) : Y ⟶ X
• CategoryTheory.Limits.IsTerminal.ofIso 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y Z : C} (hY : CategoryTheory.Limits.IsTerminal Y) (i : Y ≅ Z) : CategoryTheory.Limits.IsTerminal Z
• CategoryTheory.Limits.IsTerminal.uniqueUpToIso 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') : T ≅ T'
• CategoryTheory.Limits.IsTerminal.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsInitial (Opposite.unop X)
• CategoryTheory.Limits.IsTerminal.equivOfIso 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : CategoryTheory.Limits.IsTerminal X ≃ CategoryTheory.Limits.IsTerminal Y
• CategoryTheory.Limits.IsTerminal.ofUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (Y ⟶ X)] : CategoryTheory.Limits.IsTerminal X
• CategoryTheory.Limits.isTerminalTop 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {α : Type u_1} [Preorder α] [OrderTop α] : CategoryTheory.Limits.IsTerminal ⊤
• CategoryTheory.Limits.coconeOfDiagramTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.IsTerminal.isSplitMono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X) (f : X ⟶ Y) : CategoryTheory.IsSplitMono f
• CategoryTheory.Limits.IsTerminal.mono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X) (f : X ⟶ Y) : CategoryTheory.Mono f
• CategoryTheory.Limits.InitialMonoClass.of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I T : C} (hI : CategoryTheory.Limits.IsInitial I) (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.isIso_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (hX : CategoryTheory.Limits.IsTerminal X) (hY : CategoryTheory.Limits.IsTerminal Y) (f : X ⟶ Y) : CategoryTheory.IsIso f
• CategoryTheory.Limits.colimitOfDiagramTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfDiagramTerminal tX F)
• CategoryTheory.Limits.IsTerminal.from_self 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : t.from X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.isLimitEquivIsTerminalOfIsEmpty 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [IsEmpty J] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsTerminal c.pt
• CategoryTheory.Limits.coconeOfDiagramTerminal_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) : (CategoryTheory.Limits.coconeOfDiagramTerminal tX F).pt = F.obj X
• CategoryTheory.Limits.IsTerminal.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X) (f g : Y ⟶ X) : f = g
• CategoryTheory.Functor.isTerminalConst 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsTerminal ((CategoryTheory.Functor.const C).obj X)
• CategoryTheory.Limits.IsTerminal.ofUniqueHom 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : (Y : C) → Y ⟶ X) (uniq : ∀ (Y : C) (m : Y ⟶ X), m = h Y) : CategoryTheory.Limits.IsTerminal X
• CategoryTheory.Limits.IsTerminal.uniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') : (hT.uniqueUpToIso hT').hom = hT'.from T
• CategoryTheory.Limits.IsTerminal.uniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') : (hT.uniqueUpToIso hT').inv = hT.from T'
• CategoryTheory.Limits.IsTerminal.comp_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsTerminal Z) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (t.from Y) = t.from X
• CategoryTheory.Limits.coneOfDiagramTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.limitOfDiagramTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfDiagramTerminal hX F)
• CategoryTheory.Limits.coneOfDiagramTerminal_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : (CategoryTheory.Limits.coneOfDiagramTerminal hX F).pt = F.obj X
• CategoryTheory.Limits.coconeOfDiagramTerminal_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.Limits.coconeOfDiagramTerminal tX F).ι.app j = F.map (tX.from j)
• CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (X : J) (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.IsIso (c.ι.app X)
• CategoryTheory.Functor.isTerminalConst_from_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor C D) (Y : C) : ((CategoryTheory.Functor.isTerminalConst C hX).from F).app Y = hX.from (F.obj Y)
• CategoryTheory.Limits.coneOfDiagramTerminal_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] (x✝ : J) : (CategoryTheory.Limits.coneOfDiagramTerminal hX F).π.app x✝ = CategoryTheory.inv (F.map (hX.from x✝))
• CategoryTheory.CostructuredArrow.mkIdTerminal 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {Y : C} {S : CategoryTheory.Functor C D} [S.Full] [S.Faithful] : CategoryTheory.Limits.IsTerminal (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (S.obj Y)))
• CategoryTheory.Over.equivalenceOfIsTerminal 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Over X ≌ T
• CategoryTheory.Over.mkIdTerminal 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} : CategoryTheory.Limits.IsTerminal (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))
• CategoryTheory.Over.equivalenceOfIsTerminal_functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).functor = CategoryTheory.Over.forget X
• CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) (Y : T) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.obj Y = CategoryTheory.Over.mk (hX.from Y)
• CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.map f = CategoryTheory.Over.homMk f ⋯
• CategoryTheory.Over.equivalenceOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y), map := fun {X_1 Y} f => CategoryTheory.Over.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Over.forget X)).obj x)) ⋯
• CategoryTheory.Over.equivalenceOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj Y).left) ⋯) ⋯
• CategoryTheory.Limits.IsTerminal.hasTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.HasTerminal C
• CategoryTheory.Limits.terminalIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.IsTerminal (⊤_ C)
• CategoryTheory.Limits.terminalIsoIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : ⊤_ C ≅ P
• CategoryTheory.Limits.isIso_ι_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsTerminal j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)
• CategoryTheory.Limits.terminalIsoIsTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : (CategoryTheory.Limits.terminalIsoIsTerminal t).hom = t.from (⊤_ C)
• CategoryTheory.Limits.terminalIsoIsTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : (CategoryTheory.Limits.terminalIsoIsTerminal t).inv = CategoryTheory.Limits.terminalIsTerminal.from P
• CategoryTheory.Limits.isIso_π_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsTerminal j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
• CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal Y) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.fst
• CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal X) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.snd
• CategoryTheory.Limits.IsZero.isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsTerminal X
• CategoryTheory.Limits.HasZeroObject.zeroIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsTerminal 0
• CategoryTheory.Limits.IsZero.isoIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsTerminal Y) : X ≅ Y
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : 0 ≅ X
• CategoryTheory.Limits.IsTerminal.isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).hom = 0
• CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).inv = 0
• CategoryTheory.Limits.IsTerminal.isTerminalObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsTerminal (G.obj X)
• CategoryTheory.Limits.IsTerminal.isTerminalOfObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G] (l : CategoryTheory.Limits.IsTerminal (G.obj X)) : CategoryTheory.Limits.IsTerminal X
• CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] : CategoryTheory.Limits.IsTerminal (G.obj (⊤_ C))
• CategoryTheory.Limits.IsTerminal.isTerminalIffObj 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G] (X : C) : CategoryTheory.Limits.IsTerminal X ≃ CategoryTheory.Limits.IsTerminal (G.obj X)
• CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.asEmptyCone X)) ≃ CategoryTheory.Limits.IsTerminal (G.obj X)
• CategoryTheory.IsFiltered.of_isTerminal 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.IsFiltered C
• CategoryTheory.Limits.IsTerminal.subsingleton_to 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} (hI : CategoryTheory.Limits.IsTerminal I) {A : C} : Subsingleton (I ⟶ A)
• CategoryTheory.Limits.IsTerminal.ofStrict 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {X Y : C} (f : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsTerminal Y
• CategoryTheory.Limits.HasStrictTerminalObjects.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] (out : ∀ {I A : C} (f : I ⟶ A) (a : CategoryTheory.Limits.IsTerminal I), CategoryTheory.IsIso f) : CategoryTheory.Limits.HasStrictTerminalObjects C
• CategoryTheory.Limits.HasStrictTerminalObjects.out 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasStrictTerminalObjects C] {I A : C} (f : I ⟶ A) : ∀ (a : CategoryTheory.Limits.IsTerminal I), CategoryTheory.IsIso f
• CategoryTheory.Limits.IsTerminal.isIso_from 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} (hI : CategoryTheory.Limits.IsTerminal I) {A : C} (f : I ⟶ A) : CategoryTheory.IsIso f
• CategoryTheory.Limits.IsTerminal.strict_hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} (hI : CategoryTheory.Limits.IsTerminal I) {A : C} (f g : I ⟶ A) : f = g
• CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] (i : J) (H : (j : J) → j ≠ i → CategoryTheory.Limits.IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F i)
• isProductOfIsTerminalIsPullback 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsTerminal Z) (H₂ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k ⋯)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k)
• isPullbackOfIsTerminalIsProduct 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : CategoryTheory.Limits.IsTerminal Z) (H₂ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k ⋯)
• isBinaryProductOfIsTerminalIsPullback 📋 Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (c : CategoryTheory.Limits.Cone F) {X : C} (hX : CategoryTheory.Limits.IsTerminal X) (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ X) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ X) (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (c.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (c.π.app { as := CategoryTheory.Limits.WalkingPair.right }) ⋯)) : CategoryTheory.Limits.IsLimit c
• CategoryTheory.IsPullback.of_is_product' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback fst snd (t.from X) (t.from Y)
• CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.IsPullback c.fst c.snd (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
• CategoryTheory.IsPullback.of_is_product 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit c) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback c.fst c.snd (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
• CommRingCat.punitIsTerminal 📋 Mathlib.Algebra.Category.Ring.Constructions
  : CategoryTheory.Limits.IsTerminal (CommRingCat.of PUnit.{u + 1})
• CommRingCat.subsingleton_of_isTerminal 📋 Mathlib.Algebra.Category.Ring.Constructions
  {X : CommRingCat} (hX : CategoryTheory.Limits.IsTerminal X) : Subsingleton ↑X
• CategoryTheory.Over.forgetMapTerminal 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Over.forget X ≅ (CategoryTheory.Over.map (hT.from X)).comp (CategoryTheory.Over.equivalenceOfIsTerminal hT).functor
• CategoryTheory.Over.forgetMapTerminal_hom_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X✝ : CategoryTheory.Over X) : (CategoryTheory.Over.forgetMapTerminal X hT).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.Over.forgetMapTerminal_inv_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X✝ : CategoryTheory.Over X) : (CategoryTheory.Over.forgetMapTerminal X hT).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.mkTerminalOfRightAdjoint 📋 Mathlib.CategoryTheory.Adjunction.Comma
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor D C) {F : CategoryTheory.Functor C D} (h : F ⊣ G) (A : D) : CategoryTheory.Limits.IsTerminal (CategoryTheory.CostructuredArrow.mk (h.counit.app A))
• CategoryTheory.Limits.Cone.isLimitEquivIsTerminal 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsTerminal c
• CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F) : hc.liftConeMorphism s = (c.isLimitEquivIsTerminal hc).from s
• CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsTerminal c) (s : CategoryTheory.Limits.Cone F) : hc.from s = (c.isLimitEquivIsTerminal.symm hc).liftConeMorphism s
• CategoryTheory.WithTerminal.starTerminal 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.IsTerminal CategoryTheory.WithTerminal.star
• CategoryTheory.WithTerminal.liftToTerminal 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D
• CategoryTheory.WithTerminal.inclLiftToTerminal 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.WithTerminal.incl.comp (CategoryTheory.WithTerminal.liftToTerminal F hZ) ≅ F
• CategoryTheory.WithTerminal.liftToTerminal_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminal F hZ).obj X = match X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z
• CategoryTheory.WithTerminal.liftToTerminalUnique 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) : G ≅ CategoryTheory.WithTerminal.liftToTerminal F hZ
• CategoryTheory.WithTerminal.inclLiftToTerminal_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (x✝ : C) : (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).inv.app x✝ = CategoryTheory.CategoryStruct.id (F.obj x✝)
• CategoryTheory.WithTerminal.inclLiftToTerminal_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (x✝ : C) : (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).hom.app x✝ = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj x✝ with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)
• CategoryTheory.WithTerminal.liftToTerminal_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) : (CategoryTheory.WithTerminal.liftToTerminal F hZ).map f = match X, Y, f with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => hZ.from (F.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
• CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).hom
• CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).inv
• CategoryTheory.Limits.Types.isTerminalPUnit 📋 Mathlib.CategoryTheory.Limits.Types.Products
  : CategoryTheory.Limits.IsTerminal PUnit.{u + 1}
• CategoryTheory.Limits.Types.isTerminalEquivUnique 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X : Type u) : CategoryTheory.Limits.IsTerminal X ≃ Unique X
• CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X : Type u) : CategoryTheory.Limits.IsTerminal X ≃ (X ≅ PUnit.{u + 1})
• CategoryTheory.Functor.final_fromPUnit_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {c : C} (hc : CategoryTheory.Limits.IsTerminal c) : (CategoryTheory.Functor.fromPUnit c).Final
• CategoryTheory.Functor.final_of_isTerminal_colimit_comp_yoneda 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type v} [CategoryTheory.Category.{v, v} C] {D : Type u₁} [CategoryTheory.Category.{v, u₁} D] (F : CategoryTheory.Functor C D) (h : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))) : F.Final
• CategoryTheory.ObjectProperty.limitsOfShape_isEmpty_iff 📋 Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u') [CategoryTheory.Category.{v', u'} J] [IsEmpty J] (X : C) : P.limitsOfShape J X ↔ Nonempty (CategoryTheory.Limits.IsTerminal X)
• CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.SemiCartesianMonoidalCategory C] : CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• CategoryTheory.SemiCartesianMonoidalCategory.mk 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [toMonoidalCategory : CategoryTheory.MonoidalCategory C] (isTerminalTensorUnit : CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (fst : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ X) (snd : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Y) (fst_def : ∀ (X Y : C), fst X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (isTerminalTensorUnit.from Y)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom := by cat_disch) (snd_def : ∀ (X Y : C), snd X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (isTerminalTensorUnit.from X) Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom := by cat_disch) : CategoryTheory.SemiCartesianMonoidalCategory C
• CategoryTheory.Limits.Concrete.terminalOfUniqueOfReflects 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C) (h : Unique (CategoryTheory.ToType X)) : CategoryTheory.Limits.IsTerminal X
• CategoryTheory.Limits.Concrete.uniqueOfTerminalOfPreserves 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : Unique (CategoryTheory.ToType X)
• CategoryTheory.Limits.Concrete.terminalIffUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C) : CategoryTheory.Limits.IsTerminal X ≃ Unique (CategoryTheory.ToType X)
• CategoryTheory.ObjectProperty.prop_of_isTerminal 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] (X : C) (hX : CategoryTheory.Limits.IsTerminal X) : P X
• CategoryTheory.Functor.chosenTerminalIsTerminal 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.SemiCartesianMonoidalCategory C] : CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
• CategoryTheory.isConnected_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.IsConnected
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {x : C} (h : CategoryTheory.Limits.IsTerminal x) : CategoryTheory.IsConnected C
• CategoryTheory.Functor.final_const_of_isTerminal 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsFiltered C] {X : D} (hX : CategoryTheory.Limits.IsTerminal X) : ((CategoryTheory.Functor.const C).obj X).Final
• CategoryTheory.Sieve.ofArrows_eq_ofObjects 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X) {I : Type u_1} (Y : I → C) (f : (i : I) → Y i ⟶ X) : CategoryTheory.Sieve.ofArrows Y f = CategoryTheory.Sieve.ofObjects Y X
• CategoryTheory.Functor.isTerminal 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} (hF : (X : C) → CategoryTheory.Limits.IsTerminal (F.obj X)) : CategoryTheory.Limits.IsTerminal F
• CategoryTheory.Sheaf.terminal 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Sheaf J A
• CategoryTheory.Presheaf.isSheaf_of_isTerminal 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) {X : A} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Presheaf.IsSheaf J ((CategoryTheory.Functor.const Cᵒᵖ).obj X)
• CategoryTheory.Sheaf.isTerminalTerminal 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsTerminal (CategoryTheory.Sheaf.terminal J hX)
• CategoryTheory.Sheaf.terminal_obj 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Sheaf.terminal J hX).obj = (CategoryTheory.Functor.const Cᵒᵖ).obj X
• CategoryTheory.Sheaf.isTerminalOfEqTop 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (H : J = ⊤) (F : CategoryTheory.Sheaf J A) : CategoryTheory.Limits.IsTerminal F
• CategoryTheory.Sheaf.isTerminalOfBotCover 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (F : CategoryTheory.Sheaf J A) (X : C) (H : ⊥ ∈ J X) : CategoryTheory.Limits.IsTerminal (F.obj.obj (Opposite.op X))
• CategoryTheory.Sheaf.isTerminalTerminal_from_hom 📋 Mathlib.CategoryTheory.Sites.Sheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X) (G : CategoryTheory.Sheaf J A) : ((CategoryTheory.Sheaf.isTerminalTerminal J hX).from G).hom = (CategoryTheory.Functor.isTerminalConst Cᵒᵖ hX).from G.obj
• TopCat.isTerminalPUnit 📋 Mathlib.Topology.Category.TopCat.Limits.Basic
  : CategoryTheory.Limits.IsTerminal (TopCat.of PUnit.{u + 1})
• CategoryTheory.finitaryExtensive_iff_of_isTerminal 📋 Mathlib.CategoryTheory.Extensive
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] (T : C) (HT : CategoryTheory.Limits.IsTerminal T) (c₀ : CategoryTheory.Limits.BinaryCofan T T) (hc₀ : CategoryTheory.Limits.IsColimit c₀) : CategoryTheory.FinitaryExtensive C ↔ CategoryTheory.IsVanKampenColimit c₀
• CategoryTheory.GrothendieckTopology.coversTop_iff_of_isTerminal 📋 Mathlib.CategoryTheory.Sites.CoversTop.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) (hX : CategoryTheory.Limits.IsTerminal X) {I : Type u_1} (Y : I → C) : J.CoversTop Y ↔ CategoryTheory.Sieve.ofObjects Y X ∈ J X
• CategoryTheory.Limits.IsTerminal.orderTop 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : OrderTop C
• Preorder.isTerminalTop 📋 Mathlib.CategoryTheory.Limits.Preorder
  (C : Type u) [Preorder C] [OrderTop C] : CategoryTheory.Limits.IsTerminal ⊤
• TopCat.Sheaf.isTerminalOfEmpty 📋 Mathlib.Topology.Sheaves.SheafCondition.Sites
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Sheaf C X) : CategoryTheory.Limits.IsTerminal (F.obj.obj (Opposite.op ⊥))
• TopCat.Sheaf.isTerminalOfEqEmpty 📋 Mathlib.Topology.Sheaves.SheafCondition.Sites
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (F : TopCat.Sheaf C X) {U : TopologicalSpace.Opens ↑X} (h : U = ⊥) : CategoryTheory.Limits.IsTerminal (F.obj.obj (Opposite.op U))
• CategoryTheory.Limits.IsTerminal.isCardinalFiltered 📋 Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
  {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (κ : Cardinal.{w}) [Fact κ.IsRegular] : CategoryTheory.IsCardinalFiltered J κ
• CategoryTheory.MorphismProperty.Over.mkIdTerminal 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [P.ContainsIdentities] : CategoryTheory.Limits.IsTerminal (CategoryTheory.MorphismProperty.Over.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)
• SimplexCategory.isTerminalZero 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
  : CategoryTheory.Limits.IsTerminal { len := 0 }
• CategoryTheory.SimplicialObject.augmentOfIsTerminal 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.SimplicialObject.Augmented C
• CategoryTheory.SimplicialObject.augmentOfIsTerminal_right 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : (X.augmentOfIsTerminal hT).right = T
• CategoryTheory.SimplicialObject.augmentOfIsTerminal_left 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : (X.augmentOfIsTerminal hT).left = X
• CategoryTheory.SimplicialObject.augmentOfIsTerminal_hom_app 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (x✝ : SimplexCategoryᵒᵖ) : (X.augmentOfIsTerminal hT).hom.app x✝ = hT.from (X.obj x✝)
• HomotopicalAlgebra.isFibrant_iff_of_isTerminal 📋 Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [HomotopicalAlgebra.CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).RespectsIso] {X Y : C} (p : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal Y) : HomotopicalAlgebra.IsFibrant X ↔ HomotopicalAlgebra.Fibration p
• CategoryTheory.Factorisation.IsTerminal_terminal 📋 Mathlib.CategoryTheory.Category.Factorisation
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} : CategoryTheory.Limits.IsTerminal CategoryTheory.Factorisation.terminal
• AlgebraicGeometry.specZIsTerminal 📋 Mathlib.AlgebraicGeometry.Limits
  : CategoryTheory.Limits.IsTerminal (AlgebraicGeometry.Spec (CommRingCat.of ℤ))
• AlgebraicGeometry.specULiftZIsTerminal 📋 Mathlib.AlgebraicGeometry.Limits
  : CategoryTheory.Limits.IsTerminal (AlgebraicGeometry.Spec (CommRingCat.of (ULift.{u, 0} ℤ)))
• CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presieve 📋 Mathlib.CategoryTheory.Sites.Preserves
  {C : Type u} [CategoryTheory.Category.{v, u} C] (I : C) (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)) : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op I))
• CategoryTheory.GrothendieckTopology.Point.uniqueFiberObj 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) [CategoryTheory.LocallySmall.{w, v, u} C] (T : C) (hT : CategoryTheory.Limits.IsTerminal T) : Unique (Φ.fiber.obj T)
• CategoryTheory.GrothendieckTopology.Point.isTerminalFiberObj 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) [CategoryTheory.LocallySmall.{w, v, u} C] (T : C) (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Limits.IsTerminal (Φ.fiber.obj T)
• CategoryTheory.GrothendieckTopology.Point.subsingleton_fiber_obj 📋 Mathlib.CategoryTheory.Sites.Point.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) [CategoryTheory.LocallySmall.{w, v, u} C] {U T : C} (f : U ⟶ T) [CategoryTheory.Mono f] (hT : CategoryTheory.Limits.IsTerminal T) : Subsingleton (Φ.fiber.obj U)
• CategoryTheory.constantPresheafAdj 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Functor.const Cᵒᵖ ⊣ (CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op T)
• CategoryTheory.constantSheafAdj 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.constantSheaf J D ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)
• CategoryTheory.Sheaf.isConstant_iff_mem_essImage 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {L : CategoryTheory.Functor D (CategoryTheory.Sheaf J D)} {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (adj : L ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)) (F : CategoryTheory.Sheaf J D) : CategoryTheory.Sheaf.IsConstant J F ↔ L.essImage F
• CategoryTheory.Sheaf.isConstant_iff_of_equivalence 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {C' : Type u_3} [CategoryTheory.Category.{v_3, u_3} C'] (K : CategoryTheory.GrothendieckTopology C') [CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C') [∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] [CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) (F : CategoryTheory.Sheaf K D) : CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).inverse.obj F) ↔ CategoryTheory.Sheaf.IsConstant K F
• CategoryTheory.constantPresheafAdj_unit_app 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : D) : (CategoryTheory.constantPresheafAdj D hT).unit.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.equivCommuteConstant 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {C' : Type u_3} [CategoryTheory.Category.{v_3, u_3} C'] (K : CategoryTheory.GrothendieckTopology C') [CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C') [∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] [CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) : (CategoryTheory.constantSheaf J D).comp (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).functor ≅ CategoryTheory.constantSheaf K D
• CategoryTheory.equivCommuteConstant' 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {C' : Type u_3} [CategoryTheory.Category.{v_3, u_3} C'] (K : CategoryTheory.GrothendieckTopology C') [CategoryTheory.HasWeakSheafify K D] (G : CategoryTheory.Functor C C') [∀ (X : C'ᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) D] [CategoryTheory.Functor.IsDenseSubsite J K G] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal (G.obj T)) : CategoryTheory.constantSheaf J D ≅ (CategoryTheory.constantSheaf K D).comp (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G D).inverse
• CategoryTheory.Sheaf.isConstant_of_forget 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] [CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F
• CategoryTheory.Sheaf.isConstant_iff_forget 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full] [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)
• CategoryTheory.constantPresheafAdj_counit_app_app 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (F : CategoryTheory.Functor Cᵒᵖ D) (x✝ : Cᵒᵖ) : ((CategoryTheory.constantPresheafAdj D hT).counit.app F).app x✝ = F.map (hT.from (Opposite.unop x✝)).op
• CategoryTheory.Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D) [CategoryTheory.Sheaf.IsConstant J F] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
• CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
• CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {L : CategoryTheory.Functor D (CategoryTheory.Sheaf J D)} {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (adj : L ⊣ (CategoryTheory.sheafSections J D).obj (Opposite.op T)) [L.Faithful] [L.Full] (F : CategoryTheory.Sheaf J D) : CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso (adj.counit.app F)
• CategoryTheory.constantSheafAdj_counit_app 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : CategoryTheory.Sheaf J D) : (CategoryTheory.constantSheafAdj J D hT).counit.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf J D).map ((CategoryTheory.constantPresheafAdj D hT).counit.app X.obj)) ((CategoryTheory.sheafificationAdjunction J D).counit.app X)
• CategoryTheory.constantSheafAdj_counit_w 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasWeakSheafify J D] {B : Type u_3} [CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B) [CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [J.HasSheafCompose U] (F : CategoryTheory.Sheaf J D) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.constantCommuteCompose J U).hom.app (F.obj.obj (Opposite.op T))) ((CategoryTheory.constantSheafAdj J B hT).counit.app ((CategoryTheory.sheafCompose J U).obj F)) = (CategoryTheory.sheafCompose J U).map ((CategoryTheory.constantSheafAdj J D hT).counit.app F)
• CategoryTheory.underEquivOfIsTerminal 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Under X ≌ CategoryTheory.Discrete PUnit.{w + 1}
• CategoryTheory.underEquivOfIsTerminal_functor 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).functor = CategoryTheory.Functor.star (CategoryTheory.Under X)
• CategoryTheory.underEquivOfIsTerminal_inverse 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).inverse = CategoryTheory.Functor.fromPUnit (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))
• CategoryTheory.MorphismProperty.underEquivOfIsTerminal 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : P.Under Q X ≌ CategoryTheory.Discrete PUnit.{w + 1}
• CategoryTheory.underEquivOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.fromPUnit (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))).comp (CategoryTheory.Functor.star (CategoryTheory.Under X)))
• CategoryTheory.MorphismProperty.underEquivOfIsTerminal_functor 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).functor = CategoryTheory.Functor.star (P.Under Q X)
• CategoryTheory.MorphismProperty.underEquivOfIsTerminal_inverse 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).inverse = CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Under.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)
• CategoryTheory.underEquivOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (CategoryTheory.asIso A.hom).symm ⋯) ⋯
• CategoryTheory.MorphismProperty.underEquivOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Under.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)).comp (CategoryTheory.Functor.star (P.Under Q X)))
• CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.MorphismProperty.Under.isoMk (CategoryTheory.asIso A.hom).symm ⋯) ⋯
• Fin.isTerminalLast 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin
  (n : ℕ) : CategoryTheory.Limits.IsTerminal (Fin.last n)
• CategoryTheory.Sheaf.H.equiv₀ 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (F : CategoryTheory.Sheaf J AddCommGrpCat) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : F.H 0 ≃+ ↑(F.obj.obj (Opposite.op T))
• CategoryTheory.Sheaf.H.equiv₀_naturality 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) {F G : CategoryTheory.Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : F.H 0) : (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op T))) ((CategoryTheory.Sheaf.H.equiv₀ F hT) x) = (CategoryTheory.Sheaf.H.equiv₀ G hT) ((CategoryTheory.Sheaf.H.map f 0) x)
• CategoryTheory.Sheaf.H.equiv₀_symm_naturality 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) {F G : CategoryTheory.Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : ↑(F.obj.obj (Opposite.op T))) : (CategoryTheory.Sheaf.H.map f 0) ((CategoryTheory.Sheaf.H.equiv₀ F hT).symm x) = (CategoryTheory.Sheaf.H.equiv₀ G hT).symm ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op T))) x)
• SSet.quasicategory_of_hasLiftingProperty 📋 Mathlib.AlgebraicTopology.Quasicategory.Basic
  (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) (h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)) : S.Quasicategory
• SSet.Quasicategory.hasLiftingProperty 📋 Mathlib.AlgebraicTopology.Quasicategory.Basic
  (S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) (hn : i < Fin.last n) : CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)
• SSet.quasicategory_iff_hasLiftingProperty 📋 Mathlib.AlgebraicTopology.Quasicategory.Basic
  (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) : S.Quasicategory ↔ ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)
• SSet.quasicategory_of_from_innerFibrations 📋 Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
  (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) (h : SSet.innerFibrations (t.from S)) : S.Quasicategory
• SSet.Quasicategory.from_innerFibrations 📋 Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
  (S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) : SSet.innerFibrations (t.from S)
• SSet.quasicategory_iff_of_isTerminal 📋 Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
  {X Y : SSet} (p : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal Y) : X.Quasicategory ↔ SSet.InnerFibration p
• CategoryTheory.Cat.chosenTerminalIsTerminal 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
  : CategoryTheory.Limits.IsTerminal CategoryTheory.Cat.chosenTerminal
• SSet.stdSimplex.isTerminalObj₀ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
  : CategoryTheory.Limits.IsTerminal (SSet.stdSimplex.obj { len := 0 })
• CategoryTheory.Cat.isTerminalDiscretePUnit 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u_1 + 1}))
• CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  {T : Type u} [CategoryTheory.Category.{v, u} T] [Unique T] [CategoryTheory.IsDiscrete T] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T)
• CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  {T : Type u} [CategoryTheory.Category.{u, u} T] (hT : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T)) : CategoryTheory.Cat.of T ≅ CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u + 1})
• SSet.isTerminalHoFunctorDeltaZero 📋 Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
  : CategoryTheory.Limits.IsTerminal (SSet.hoFunctor.obj (SSet.stdSimplex.obj { len := 0 }))
• SSet.Truncated.HomotopyCategory.isTerminal 📋 Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
  (X : SSet.Truncated 2) [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 }))] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of X.HomotopyCategory)
• CategoryTheory.Functor.PullbackObjObj.ofIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))] (h : CategoryTheory.Limits.IsTerminal Y₃) : G.PullbackObjObj f₁ f₃
• CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))] (h : CategoryTheory.Limits.IsTerminal Y₃) : (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).pt = (G.obj (Opposite.op X₁)).obj X₃
• CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))] (h : CategoryTheory.Limits.IsTerminal Y₃) : (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).fst = CategoryTheory.CategoryStruct.id ((G.obj (Opposite.op X₁)).obj X₃)
• CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))] (h : CategoryTheory.Limits.IsTerminal Y₃) : (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).π = (G.map f₁.op).app X₃
• CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))] (h : CategoryTheory.Limits.IsTerminal Y₃) : (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).snd = (CategoryTheory.Limits.IsTerminal.isTerminalObj (G.obj (Opposite.op Y₁)) Y₃ h).from ((G.obj (Opposite.op X₁)).obj X₃)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (X □ CategoryTheory.Arrow.mk (i.to T)) ≅ X
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (X □ CategoryTheory.Arrow.mk (t.from I)) ≅ X
• CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C} : (Opposite.op X ⋔ CategoryTheory.Arrow.mk (t.from W)) ≅ CategoryTheory.Arrow.mk ((CategoryTheory.MonoidalClosed.pre X.hom).app W)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).inv.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).inv.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).hom.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).hom
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).hom.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).hom
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).hom.left = CategoryTheory.CategoryStruct.comp ⋯.isoPushout.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).hom)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c