Library HoTT.Metatheory.IntervalImpliesFunext
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics.
Require Import HIT.Interval.
Require Import Metatheory.Core Metatheory.FunextVarieties.
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)).