@@ -12,7 +12,7 @@ module Data.So
1212||| If you find yourself using `So` for something other than primitive types,
1313||| it may be appropriate to define a type of evidence for the property that you
1414||| care about instead.
15−data So : Bool -> Type where
15+data So : Bool -> Type where
1616 Oh : So True
1717
1818implementation Uninhabited (So False) where
@@ -23,4 +23,14 @@ choose : (b : Bool) -> Either (So b) (So (not b))
2323choose True = Left Oh
2424choose False = Right Oh
2525
26+||| Absurd when you have proof that both `b` and `not b` is true.
27+export
28+soAbsurd : So b -> So (not b) -> Void
29+soAbsurd sb snb with (sb)
30+ | Oh = uninhabited snb
31+
32+||| Transmission between usage of value-level `not` and type-level `Not`.
33+export
34+soNotToNotSo : So (not b) -> Not (So b)
35+soNotToNotSo = flip soAbsurd
2636