(P : Type) (a b : P) (p : a = b) : finterval -> P. Proof. refine ((pr1 : { x : P & x = b } -> P) o _). apply Trm_rec. intros []. - exact (a; p). - exact (b; idpath). Defined.
Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool. Require Import Metatheory.Core Metatheory.FunextVarieties Metatheory.ImpredicativeTruncation.