Impredicative Prop

[amp12]

Would it be possible to have a "--prop-in-prop" option that collapses the Prop_ hierarchy and makes Prop into an impredicative (but hopefully still consistent) universe of proof-irrelevant propositions?

[jespercockx]

Currently Agda's termination check assumes predicativity so such an option would not be consistent:

{-# OPTIONS --prop --type-in-type #-}

data ⊥ : Prop where

data Bad : Prop where
  b : ((P : Prop) → P → P) → Bad

bad : Bad
bad = b (λ P p → p)

no-bad : Bad → ⊥
no-bad (b x) = no-bad (x Bad bad)

very-bad : ⊥
very-bad = no-bad bad

So first we would have to patch the termination checker.

[jespercockx]

It seems this could now be implemented easily, thanks to a change by @plt-amy to the termination checker for --prop: #6639 (comment)

[andreasabel]

We could have --impredicative-prop disable --syntax-based-termination, because type-based termination does not have the inconsistency issue with impredicativity.

We would have to go through the constraint solver to look for predicativity assumptions. At least the comment here would have to change:

agda/src/full/Agda/TypeChecking/Conversion.hs

Lines 2024 to 2038 in 15342bf

	-- If @Prop l == funSort s1 s2@, then @s2@ must be of the
	-- form @Prop l2@, and @s1@ can be one of @Set l1@, Prop
	-- l1@, or @SizeUniv@.
	Prop l -> do
	l2 <- forceUniv UProp s2
	leqLevel l2 l
	s1b <- reduceB s1
	let s1 = ignoreBlocking s1b
	blocker = getBlocker s1b
	case funSort' s1 (Prop l2) of
	-- If the work we did makes the @funSort@ compute,
	-- continue working.
	Right s -> equalSort (Prop l) s
	-- Otherwise: postpone
	Left _ -> patternViolation blocker

We need to relax the fitsIn check for Prop.