# Functional Extensionality

Require Import overture pext inhab.

## Deriving functional extensionality from the existence of an interval

Section Interval.
Definition interval := inhab bool.
Let i0 : interval := tr false.
Let i1 : interval := tr true.

Lemma I_path {A : Type} (f : interval -> A) : f i0 = f i1.
Proof. congr f. exact: trP. Qed.

Program Definition path_I {A : Type} {x y : A} (p : x = y) : interval -> A :=
inhab_rec (fun b => if b then y else x) _.
Next Obligation. by destruct x0, y0. Qed.

Definition fext {A : Type} {B : A -> Type} (f g : forall x, B x) :
(forall x, f x = g x) -> f = g := fun p => I_path (fun i x => path_I (p x) i).
End Interval.

## Extensionality for products

Lemma xi_ext {A} {B C : A -> Type} (p : forall x : A, B x = C x) :
(forall x, B x) = (forall x, C x).
Proof. have: B = C by exact: fext. by move->. Qed.

Lemma xi_extP {A} {B C : A -> Prop} (p : forall x : A, B x = C x) :
(forall x, B x) = (forall x, C x).
Proof. have: B = C by exact: fext. by move->. Qed.

Lemma xi_extS {A} {B C : A -> Set} (p : forall x : A, B x = C x) :
(forall x, B x) = (forall x, C x).
Proof. have: B = C by exact: fext. by move->. Qed.

## Extensionality Tactic

Ltac fext := nointr repeat (
match goal with
[ |- ?x = ?y ] =>
(apply: fext ||
apply: xi_extP ||
apply: xi_extS ||
apply: xi_ext); intro
end).

## Propositions are closed under products

Lemma prod_is_prop A (P : A -> hprop) : is_prop (forall x, P x).
Proof. move=> p q. apply: fext => x. exact: hpropP. Qed.

Canonical Structure prod_hprop A (P : A -> hprop) :=
mk_hprop (iprod P) (@prod_is_prop A P).

Canonical Structure fun_hprop A (B : hprop) :=
mk_hprop (A -> B) (@prod_is_prop A (fun _ => B)).

## Pairs in bool -> X

Definition pairb {T} (x y : T) (b : bool) : T := if b then x else y.

Lemma pairb_fun {X Y} (f : X -> Y) x y :
f \o pairb x y = pairb (f x) (f y).
Proof. by fext=> -[]. Qed.

## Paths between Equivalences

Section EquivalencePaths.
Variables (A B : Type).
Implicit Types (f : A -> B).

Lemma is_equiv_prop f :
is_prop (is_equiv f).
Proof.
move=> [g1 h1 h2] [g2 h3 h4]. have e: g1 = g2. apply: fext => x.
by rewrite -{1}[x]h4 h1. destruct e. f_equal; exact: pi.
Qed.

Canonical Structure is_equiv_hprop f := mk_hprop (is_equiv f) (@is_equiv_prop f).

Lemma equiv_eq (f g : A <~> B) :
f = g :> (A -> B) -> f = g.
Proof.
move: f g => [f hf] [g hg] /= eqn. destruct eqn. f_equal. exact: hpropP.
Qed.
End EquivalencePaths.

## Characterization of Maps out of Truncations

Section TruncationMappingProperty.
Variables (A B : Type).

Definition constant (f : A -> B) := forall x y, f x = f y.

Program Definition inhab_map (f : inhab A -> B) : { f : A -> B | constant f } :=
exist _ (f \o tr) _.
Next Obligation. move=> x y /=. congr f. exact: trP. Qed.

Definition map_inhab (p : { f : A -> B | constant f }) : inhab A -> B :=
inhab_rec p.1 p.2.

Lemma inhab_map_sect (f : inhab A -> B) : map_inhab (inhab_map f) = f.
Proof. fext. exact: inhab_ind. Qed.

Lemma inhab_map_retr (p : { f : A -> B | constant f }) :
inhab_map (map_inhab p) = p.
Proof. exact: sig_eq. Qed.

Definition inhab_map_is_equiv : is_equiv inhab_map :=
mk_is_equiv map_inhab inhab_map_sect inhab_map_retr.

Canonical inhab_map_equiv := mk_equiv inhab_map inhab_map_is_equiv.
End TruncationMappingProperty.