Can you remove strict positivity from mere propositions?

Question

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.

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?