semantics.base.fext

Functional Extensionality

Deriving functional extensionality from the existence of an interval

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

  Lemma I_path {A : Type} (f : interval A) : f = f .
  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 , . Qed.

  Definition fext {A : Type} {B : A Type} (f g : x, B x) :
    ( 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 : x : A, B x = C x) :
  ( x, B x ) = ( x, C x ).
Proof. have: B = C by exact: fext. by move. Qed.

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

Lemma xi_extS {A} {B C : A Set} (p : x : A, B x = C x) :
  ( x, B x ) = ( 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 ( 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 [ ] [ ]. have e: = . apply: fext x.
      by rewrite -{1}[x] . 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) := 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.