{-# OPTIONS --type-in-type #-} module Proof where ⊥ : Set ⊥ = (A : Set) -> A ¬_ : Set -> Set ¬ A = A -> ⊥ pow : Set -> Set pow U = U -> Set data _==_ {A : Set} : A -> A -> Set where refl : (a : A) -> a == a symm : {A : Set} -> {a b : A} ->…