Library HoTT.Basics.Logic

Set Implicit Arguments.

Require Export Basics.Notations.

Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.

Notation "A -> B" := ( (_ : A), B) : type_scope.

Propositional connectives

True is the unit type.
Inductive True : Type :=
  I : True.

False is the empty type.
Inductive False : Type :=.

not A, written ¬A, is the negation of A
Definition not (A:Type) : Type := A False.

#[export] Hint Unfold not : core.
#[export] Hint Resolve I : core.