You can encode induction impredicatively. Some minimalist theories dispense entirely with inductive/coinductive types for proof irrelevant impredicative sorts.

But in a practical theorem prover it's nice to have constructors and fields for records even if the underlying semantics are just the impredicative encoding of a fixed point operator $\mu F = \forall x. (F x \rightarrow x)\rightarrow x$.

I suspect in practice though if you just unset strict positivity for inductive proof irrelevant impredicative propositions you'll get a mess instead of the desired semantics of the fixed point operator.

But I'm not sure exactly what would go wrong.

Basically as an example in Coq

Unset Strict Positivity.
Inductive weird: SProp := weird_intro (f: weird -> weird).

"it would be nice to be like"

Definition weird := forall A: SProp, ((A -> A) -> A) -> A.

But it probably isn't and things probably break.


1 Answer 1


If you allow arbitrary fixed points you can inhabit any type.

Let $A$ be an arbitrary type. Suppose we had a type $B$ such that $B \cong B \to A$. Then by Lawvere's fixed point theorem $A$ has the fixed-point property, therefore $\mathrm{id}_A : A \to A$ has a fixed point, so $A$ is inhabited.

Should I write out more details?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.