Theorems · Theorem · category theory

PFunctor.M.bisim

∀ {P : PFunctor.{uA, uB}} (R : P.M → P.M → Prop),
  (∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)) →
    ∀ (x y : P.M), R x y → x = y

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

2 results in Mathlib

Foundations

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