(* -*- mode: coq; mode: visual-line -*- *)

(** * Theorems about trunctions *)

Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Metatheory.Core Metatheory.FunextVarieties.

(** ** We can construct an interval type as [Trunc -1 Bool] *)

Local Definition interval := Trunc (-1) Bool.

Local Definition interval_rec (P : Type) (a b : P) (p : a = b)
: interval -> P.
P: Type
a, b: P
p: a = b
interval -> P
Proof.
P: Type
a, b: P
p: a = b
interval -> P
  unfold interval; intro x.
P: Type
a, b: P
p: a = b
x: Trunc (-1) Bool
P
  cut { pt : P | pt = b }.
P: Type
a, b: P
p: a = b
x: Trunc (-1) Bool
{pt : P & pt = b} -> P
P: Type
a, b: P
p: a = b
x: Trunc (-1) Bool
{pt : P & pt = b}
  {
P: Type
a, b: P
p: a = b
x: Trunc (-1) Bool
{pt : P & pt = b} -> P apply pr1. }
P: Type
a, b: P
p: a = b
x: Trunc (-1) Bool
{pt : P & pt = b}
  {
P: Type
a, b: P
p: a = b
x: Trunc (-1) Bool
{pt : P & pt = b} strip_truncations.
P: Type
a, b: P
p: a = b
x: Bool
{pt : P & pt = b}
    refine (if x then a else b; _).
P: Type
a, b: P
p: a = b
x: Bool
(if x then a else b) = b
    destruct x; (reflexivity || assumption). }
Defined.

Local Definition seg : tr true = tr false :> interval
  := path_ishprop _ _.

(** ** From an interval type, and thus from truncations, we can prove function extensionality. *)

Definition funext_type_from_trunc : 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)).