(** * Theorems about the homotopical interval. *)

Require Import Basics.Overture Basics.PathGroupoids.
Require Import Types.Paths.

Local Open Scope path_scope.


Module Export Interval.

Private Inductive interval : Type0 :=
  | zero : interval
  | one : interval.

Axiom seg : zero = one.

Definition interval_ind (P : interval -> Type)
  (a : P zero) (b : P one) (p : seg # a = b)
  : forall x:interval, P x
  := fun x => (match x return _ -> P x with
                | zero => fun _ => a
                | one  => fun _ => b
              end) p.

Axiom interval_ind_beta_seg : forall (P : interval -> Type)
  (a : P zero) (b : P one) (p : seg # a = b),
  apD (interval_ind P a b p) seg = p.

End Interval.

Definition interval_rec (P : Type) (a b : P) (p : a = b)
  : interval -> P
  := interval_ind (fun _ => P) a b (transport_const _ _ @ p).

Definition interval_rec_beta_seg (P : Type) (a b : P) (p : a = b)
  : ap (interval_rec P a b p) seg = p.
P: Type
a, b: P
p: a = b
ap (interval_rec P a b p) seg = p
Proof.
P: Type
a, b: P
p: a = b
ap (interval_rec P a b p) seg = p
  refine (cancelL (transport_const seg a) _ _ _).
P: Type
a, b: P
p: a = b
transport_const seg a @ ap (interval_rec P a b p) seg =
transport_const seg a @ p
  refine ((apD_const (interval_ind (fun _ => P) a b _) seg)^ @ _).
P: Type
a, b: P
p: a = b
apD (interval_ind (fun _ : interval => P) a b (transport_const seg a @ p))
  seg =
transport_const seg a @ p
  exact (interval_ind_beta_seg (fun _ => P) _ _ _).
Defined.

(** ** The interval is contractible. *)

Instance contr_interval : Contr interval | 0.
Contr interval
Proof.
Contr interval
  apply (Build_Contr _ zero).
forall y : interval, zero = y
  refine (interval_ind _ 1 seg _).
transport (paths zero) seg 1 = seg
  exact (transport_paths_r _ _ @ concat_1p _).
Defined.