Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
(** * An interval type implies function extensionality *)
Require Import HoTT.Basics.
Require Import HIT.Interval.
Require Import Metatheory.Core Metatheory.FunextVarieties.
(** From an interval type with definitional computation rules on the end points, we can prove function extensionality. *)
Definition funext_type_from_interval : Funext_type
:= WeakFunext_implies_Funext (NaiveFunext_implies_WeakFunext
(fun A P f g p =>
let h := fun (x:interval) (a:A) =>
interval_rec _ (f a) (g a) (p a) x
in ap h seg)).
(** Note that the converse is also true: function extensionality implies that an interval type exists, with definitional computation rules. This is illustrated in TruncImpliesFunext.v. *)