Functional extensionality from the interval in https://github.com/barras/coq/tree/hit

funext_from_interval.v

Inductive interval :=
| zero : interval
| one : interval
with paths :=
| seg : zero = one.

Definition ap A B (f : A -> B) x y (p : x = y) : f x = f y
  := match p in (_ = y) return f x = f y with
       | eq_refl => eq_refl
     end.

Definition transport_const A B x y z p
: eq_rect x (fun _ : A => B) y z p
  = y.
Proof.
  destruct p.
  reflexivity.
Defined.

Definition funext A (B : A -> Type) (f g : forall a, B a) (H : forall x, f x = g x)
: f = g
  := @ap _ _
         (fun (i : interval) x =>
            fixmatch {h} i with
              | zero => f x
              | one => g x
              | seg => eq_trans (transport_const _ _ _ _ _ _) (H x)
            end)
         _ _
         seg.

susp.v

Inductive Susp (A : Type) :=
| N : Susp A
| S : Susp A
with paths :=
| merid (x : A) : N = S.