-- Renaming the universe type = Set -- Axiomatizing propositional logic infixr 4 _⇒_ infixl 5 _∨_ infixl 6 _∧_ postulate -- Type of propositions o : type -- Proposition constructors ⊤ ⊥ : o _⇒_ _∧_ _∨_ : o → o → o infix 1 _true postulate -- Judgement: A true _true : o → type -- Proof rules andI : ∀{A B : o} → A true → B true → A ∧ B true andE₁ : ∀{A B : o} → A ∧ B true → A true andE₂ : ∀{A B : o} → A ∧ B true → B true ⊤I : ⊤ true impI : ∀{A B : o} → (A true → B true) → A ⇒ B true impE : ∀{A B : o} → A ⇒ B true → A true → B true orI₁ : ∀{A B : o} → A true → A ∨ B true orI₂ : ∀{A B : o} → B true → A ∨ B true orE : ∀{A B C : o} → A ∨ B true → (A true → C true) → (B true → C true) → C true botE : ∀{C : o} → ⊥ true → C true -- a proof of commutativity of _∧_ and-comm : ∀{A B} → A ∧ B ⇒ B ∧ A true and-comm = impI λ ab → andI (andE₂ ab) (andE₁ ab) -- a proof of commutativity of _∨_ or-comm : ∀{A B} → A ∨ B ⇒ B ∨ A true or-comm = impI λ ab → orE ab (λ a → orI₂ a) (λ b → orI₁ b)