A derivation of function extensionality from the interval in Coq using private inductives

funext_from_interval.v

Module Import Interval.
  Unset Elimination Schemes.
  (** An [interval] is the quotient of [bool] under the trivial
      relation, that [true = false].  Based on the real interval, we
      call the left endpoint [zero], the right endpoint [one], and the
      proof of equality [seg : zero = one]. *)
  Private Inductive interval := zero | one.
  Axiom seg : zero = one.

  (** The eliminator for the interval says that if you send [zero]
      somewhere, and you send [one] somewhere, and the places you send
      them are equal, then you can eliminate the interval.  A
      dependent version needs [transport] to align the types, but we
      only need the non-dependent version here.  We use a trick to
      make sure that [Coq] does not remove the proof of equality;
      understanding the type is more important than understanding the
      body. *)
  Definition interval_rect_nd (P : Type) (z o : P) (s : z = o) (i : interval) : P
    := match i with
       | zero => fun _ => z
       | one => fun _ => o
       end s.
End Interval.

Section funext.
  Context {A} {B : A -> Type}
          (f g : forall a : A, B a)
          (h : forall a, f a = g a).
  
  (** The proof of funext involves two steps: first we construct a
      function, then we use [f_equal] to prove funext. *)
  (** The function is of type [interval -> forall a, B a], and is
      *judgmentally* [f] on [zero] and *judgmentally [g] on [one].  It is
      possible to do this with only a propositional computation rule, but
      we don't do that here. *)
  Let f_or_g : interval -> forall a, B a
    := fun i a
       => interval_rect_nd (B a) (f a) (g a) (h a) i.

  (** Since we created this as a function out of the interval, we have
      that it is equal when applied to [zero] or applied to [one]. *)
  Let f_or_g_equal : f_or_g zero = f_or_g one := f_equal f_or_g seg.
  (** By judgmental computation, we can prove [f = g]. *)
  Definition funext : f = g := f_or_g_equal.
End funext.

(** An enlightening challenge is to try to do this proof using the
    impredicative / Church encoding of the interval, and show that
    this is not sufficient to prove funext without axioms. *)

(** Hint: The impredicative encoding of the interval type is: *)
Definition interval := forall (P : Type) (z o : P) (s : z = o), P.
(** The definitions of [zero : interval], [one : interval], and [seg :
    zero = one] are left as an exercise to the reader. *)