# Library Coq.Logic.PropExtensionalityFacts

Some facts and definitions about propositional and predicate extensionality
We investigate the relations between the following extensionality principles
• Proposition extensionality
• Predicate extensionality
• Propositional functional extensionality
• Provable-proposition extensionality
• Refutable-proposition extensionality
• Extensional proposition representatives
• Extensional predicate representatives
• Extensional propositional function representatives
1. Definitions
2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality
2.2 Propositional extensionality -> Provable propositional extensionality
2.3 Propositional extensionality -> Refutable propositional extensionality

Set Implicit Arguments.

# Definitions

Propositional extensionality

Local Notation PropositionalExtensionality :=
(forall A B : Prop, (A <-> B) -> A = B).

Provable-proposition extensionality

Local Notation ProvablePropositionExtensionality :=
(forall A:Prop, A -> A = True).

Refutable-proposition extensionality

Local Notation RefutablePropositionExtensionality :=
(forall A:Prop, ~A -> A = False).

Predicate extensionality

Local Notation PredicateExtensionality :=
(forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q).

Propositional functional extensionality

Local Notation PropositionalFunctionalExtensionality :=
(forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q).