Detect propositions

[sir-wabbit]

https://ncatlab.org/nlab/show/mere+proposition

Like typeclasses, they are unique but not by an ad-hoc convention, but rather by definition. Some examples: Void, Unit, A === B, A <~< B, IsCovariant[F], Inhabited[A], A => Void, Functor[F], Eq[A], and also tuples of propositions. Anything that is isomorphic to a proposition is a proposition.

We are interested not just in propositions, but in those propositions that do not have computational content (i.e. not Functor[F] or Eq[A]). They can be forcibly asserted in any part of our program, e.g. implicitly[A === A].asInstanceOf[A === B]. This allows us to replace any complicated expression returning complicated : P with a simpler expression assertP : P, assuming totality. For example, if you have an inductive proof that commutativity of natural number addition holds, you can erase the inductive part and straight up force the result.

plusIsCommutative : (a : Nat) -> (b : Nat) -> plus a b = plus b a
plusIsCommutative a b = ... -- some recursive calls
-- can be replaced to
plusIsCommutative a b = assertTrue

Every single method on Is can be replaced with unsafeForce[A, B], which just asserts the result (and with polyopt it will be a val).