(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about the empty type *)

Require Import Basics.Overture Basics.Equivalences Basics.Trunc.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Set Universe Minimization ToSet.

Local Open Scope path_scope.

(** ** Unpacking *)
(** ** Eta conversion *)
(** ** Paths *)
(** ** Transport *)
(** ** Functorial action *)
(** ** Equivalences *)
(** ** Universal mapping properties *)

Global Instance contr_from_Empty@{u} {_ : Funext} (A : Empty -> Type@{u})
  : Contr@{u} (forall x:Empty, A x).
H: Funext
A: Empty -> Type
Contr (forall x : Empty, A x)
Proof.
H: Funext
A: Empty -> Type
Contr (forall x : Empty, A x)
  refine (Build_Contr@{u} _ (Empty_ind A) _).
H: Funext
A: Empty -> Type
forall y : forall e : Empty, A e, Empty_ind A = y
  intros f; apply path_forall@{Set u u}; intros x; elim x.
Defined.

Lemma Empty_rec {T : Type} (falso: Empty) : T.
T: Type
falso: Empty
T
Proof.
T: Type
falso: Empty
T case falso. Defined.

Global Instance isequiv_empty_rec@{u} `{Funext} (A : Type@{u})
  : IsEquiv@{Set u} (fun (_ : Unit) => @Empty_rec A) | 0
  := isequiv_adjointify@{Set u} _
  (fun _ => tt)
  (fun f => path_forall@{Set u u} _ _ (fun x => Empty_rec x))
  (fun x => match x with tt => idpath end).

Definition equiv_empty_rec@{u} `{Funext} (A : Type@{u})
  : Unit <~> ((Empty -> A) : Type@{u})
  := (Build_Equiv@{Set u} _ _ (fun (_ : Unit) => @Empty_rec A) _).

(** ** Behavior with respect to truncation *)

Global Instance istrunc_Empty@{} (n : trunc_index) : IsTrunc n.+1 Empty.
n: trunc_index
IsTrunc n.+1 Empty
Proof.
n: trunc_index
IsTrunc n.+1 Empty
  refine (@istrunc_leq (-1)%trunc n.+1 tt _ _).
n: trunc_index
IsHProp Empty
  apply istrunc_S.
n: trunc_index
forall x y : Empty, Contr (x = y)
  intros [].
Defined.

Global Instance isequiv_all_to_empty (T : Type) (f : T -> Empty) : IsEquiv f.
T: Type
f: T -> Empty
IsEquiv f
Proof.
T: Type
f: T -> Empty
IsEquiv f
  refine (Build_IsEquiv _ _ _ 
    (Empty_ind (fun _ => T))                (* := equiv_inf *)
    (fun fals:Empty => match fals with end) (* : f o equiv_inf == idmap *)
    (fun t:T => match (f t) with end)       (* : equiv_inf o f == idmap *)
    (_)                                     (* adjointify part *)  ).
T: Type
f: T -> Empty
forall x : T,
match
  f x as fals
  return
    (f (Empty_ind (fun _ : Empty => T) fals) = fals)
with
end =
ap f
  match
    f x
    return (Empty_ind (fun _ : Empty => T) (f x) = x)
  with
  end
  intro t.
T: Type
f: T -> Empty
t: T
match
  f t as fals
  return
    (f (Empty_ind (fun _ : Empty => T) fals) = fals)
with
end =
ap f
  match
    f t
    return (Empty_ind (fun _ : Empty => T) (f t) = t)
  with
  end 
  exact (Empty_rec (f t)).
Defined.

Definition equiv_to_empty {T : Type} (f : T -> Empty) : T <~> Empty
  := Build_Equiv T Empty f _.

(** ** Paths *)

(** We could probably prove some theorems about non-existing paths in
   [Empty], but this is really quite useless. As soon as an element
   of [Empty] is hypothesized, we can prove whatever we like with
   a simple elimination. *)