Replacing (strict) positivity with monotonicity on propositions

Question

When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to \mathsf D$, where $F(\mathsf D)$ is the type of the constructor argument, and it can contain $\mathsf D$ itself. Then the positivity restriction basically states that the proof assistant needs to see that $F$ is a functor $\mathsf{Type} \to \mathsf{Type}$⁽¹⁾. This is crucial because otherwise the induction principle wouldn't make sense: $$\forall (P : \mathsf D \to \mathsf{Prop}).\left(\forall (\vec x : F(\mathsf D)). \mathtt{fmap}_{F} P \, (\vec x) \to P(\mathsf c\, \vec x)\right) \to \forall x. P(x)$$ where $\mathtt{fmap}_F$ is the map on the morphisms associated with the functor $F$. The proof checker, based on the consideration above, implements some syntactic criteria to ensure functorality, which become known as positivity. On the other hand, the "strictly positive" criterion, as I view it, is added to avoid size issues similar to that of set theory.

This has led me to wonder if such a criterion can be relaxed on propositions. In languages having definitionally irrelevant (or related weaker notions of) propositions, the propositions can be roughly viewed as a subsingleton, i.e. a subset of the singleton. This avoids all the size issues. Also, the functorality condition degenerates because of the irrelevance. So perhaps for inductive propositions, we can allow $F : \mathsf{Prop} \to \mathsf{Prop}$ to simply be monotonic. So if the proof checker can deduce (from some syntactic criteria, or by a user supplied proof) that $F(p) \to F(q)$ whenever $p \to q$, then it should allow this inductive definition. In proof assistants embracing classical logic (at least in $\mathsf{Prop}$), this can be much more powerful. The proof checker might just run a small SAT solver to see if the definition is monotonic.

The question is: does this leads to anything interesting (including possible paradoxes when combined with other features in the type theory)? Pointers to existing literature are also welcome.

(1) : Let's ignore universe levels for now. $\mathsf{Type, Prop}$ are just suggestive notations.

Answer 1

Impredicative strict Prop supports initial F-algebras for all F : Prop → Prop functors. In Coq:

Require Import Coq.Unicode.Utf8.

Record Functor : Type := mkFunctor
  {ob : SProp → SProp; hom : ∀ (A B : SProp), (A → B) → ob A → ob B}.

Record Alg (F : Functor) : Type := mkAlg
  {carrier : SProp; phi : F.(ob) carrier → carrier}.

Arguments mkAlg {F}.
Arguments carrier {F}.
Arguments phi {F}.

Definition InitAlg (F : Functor) : Alg F :=
  mkAlg (∀ (P : SProp), (F.(ob) P → P) → P)
        (λ fx P c, c (F.(hom) _ _ (λ g, g P c) fx)).

Definition InitAlgInit (F : Functor)(A : Alg F) (x : (InitAlg F).(carrier)) : A.(carrier) :=
  x (A.(carrier)) (A.(phi)).

As you mentioned, all equations can be omitted here because of the irrelevance, and there's no need to consider "dependent" elimination. For ordinary Prop, we would need an axiom of irrelevance to do the same. Impredicativity is generally required, else ∀ (P : SProp), (F.(ob) P → P) → P) doesn't fit in SProp.

I couldn't come up with examples of interesting applications of non-strictly positive SProp-s, maybe someone else here can.

Answer 2

Can't you just use an impredicative encoding of inductive datatypes?

Definition W {A} (B: A → SProp): SProp := ∀ (Q: SProp), (∀ tag, (B tag → Q) → Q) → Q.
Definition sup {A} {B: A → SProp} (tag: A) (f: B tag → W B): W B :=
  λ _ p, p tag (λ b, f b _ p).
Definition W_sind (A: Type) (B: A → SProp) (P: W B → SProp)
           (f: ∀ tag field, (∀ b : B tag, P (field b)) → P (sup tag field)) (w: W B): P w :=
  w (P w) (λ tag field, f tag _ (λ b, field b)).

I ape strict positivity here but I'm not quite sure why just using any old functor shouldn't work.