Theorems · Definition · category theory

PFunctor.Approx.CofixA.intro.noConfusion

{F : PFunctor.{uA, uB}} →
  {P : Sort u} →
    {n : ℕ} →
      {a : F.A} →
        {a_1 : F.B a → PFunctor.Approx.CofixA F n} →
          {n' : ℕ} →
            {a' : F.A} →
              {a'_1 : F.B a' → PFunctor.Approx.CofixA F n'} →
                n.succ = n'.succ →
                  PFunctor.Approx.CofixA.intro a a_1 ≍ PFunctor.Approx.CofixA.intro a' a'_1 →
                    (n = n' → a ≍ a' → a_1 ≍ a'_1 → P) → P

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

2 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms