Proof of funext from the interval.

funext_interval.v

Require Import HoTT.

Axiom Interval : Type.
Axioms zero one : Interval.
Axiom seg : zero = one.
Axiom Interval_rect_nodep : forall P
                                   (Pzero Pone : P)
                                   (H : Pzero = Pone),
                              Interval -> P.

Axiom Inverval_rect_nodep_compute_zero
: (fun P Pzero Pone H => Interval_rect_nodep P Pzero Pone H zero)
  = (fun P Pzero Pone H => Pzero).

Axiom Inverval_rect_nodep_compute_one
: (fun P Pzero Pone H => Interval_rect_nodep P Pzero Pone H one)
  = (fun P Pzero Pone H => Pone).

Definition funext_path_forall A (P : A -> Type)
           (f g : forall x, P x)
           (H : forall x, f x = g x)
: f = g.
  pose (fun (i : Interval) (x : A)
        => Interval_rect_nodep _
                               (f x)
                               (g x)
                               (H x)
                               i) as h.
  pose (ap h seg).
  transitivity (h zero); [ symmetry
                         | transitivity (h one);
                           [ assumption
                           | symmetry ] ];
  subst h;
  simpl in *.
  - change ((fun x => (fun P (Pzero Pone : P) (H : Pzero = Pone)
                       => Interval_rect_nodep P Pzero Pone H zero)
                        (P x) (f x) (g x) (H x))
            = f).
    rewrite Inverval_rect_nodep_compute_zero.
    reflexivity.
  - change (g
            = (fun x => (fun P (Pzero Pone : P) (H : Pzero = Pone)
                         => Interval_rect_nodep P Pzero Pone H one)
                          (P x) (f x) (g x) (H x))).
    rewrite Inverval_rect_nodep_compute_one.
    reflexivity.
Defined.