Theorems · Theorem · category theory

CompHausLike.LocallyConstant.counitApp.congr_simp

∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_3 : CategoryTheory.Limits.PreservesFiniteProducts Y],
  CompHausLike.LocallyConstant.counitApp Y = CompHausLike.LocallyConstant.counitApp Y

Defined in

Mathlib.Condensed.Discrete.LocallyConstant

Cited by

0 results in Mathlib

Foundations

Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompHausLike.HasPropCompHausLike.HasPropCompHausLike.HasExplicitFiniteCoproductsCategoryTheory.Limits.PreservesFiniteProducts