English
Fix F α is defined as the quotient of all W-structures (q.P.W α) by the W-equivalence relation; it is a functor with one fewer parameter than F.
Русский
Fix F α задаётся как фактор-множество всех W-структур (q.P.W α) по отношению эквивалентности W; это функтор с наименьшим количеством параметров.
LaTeX
$$$\mathrm{Fix} F \alpha = \operatorname{Quot} (wSetoid \alpha) (q.P.W \alpha)$$$
Lean4
/-- Least fixed point of functor F. The result is a functor with one fewer parameters
than the input. For `F a b c` a ternary functor, `Fix F` is a binary functor such that
```lean
Fix F a b = F a b (Fix F a b)
```
-/
def Fix {n : ℕ} (F : TypeVec (n + 1) → Type*) [q : MvQPF F] (α : TypeVec n) :=
Quotient (wSetoid α : Setoid (q.P.W α))
