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

Require Import Basics.Overture Basics.Equivalences.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Local Open Scope path_scope.

Local Set Universe Minimization ToSet.

Generalizable Variables A.

(** ** Eta conversion *)

Definition eta_unit (z : Unit) : tt = z
  := match z with tt => 1 end.

(** ** Paths *)

(* This is all kind of ridiculous, but it fits the pattern. *)

Definition path_unit_uncurried (z z' : Unit) : Unit -> z = z'
  := fun _ => match z, z' with tt, tt => 1 end.

Definition path_unit (z z' : Unit) : z = z'
  := path_unit_uncurried z z' tt.

Definition eta_path_unit {z z' : Unit} (p : z = z') :
  path_unit z z' = p.
z, z': Unit
p: z = z'
path_unit z z' = p
Proof.
z, z': Unit
p: z = z'
path_unit z z' = p
  destruct p.
z: Unit
path_unit z z = 1 destruct z.
path_unit tt tt = 1 reflexivity.
Defined.

Global Instance isequiv_path_unit (z z' : Unit) : IsEquiv (path_unit_uncurried z z') | 0.
z, z': Unit
IsEquiv (path_unit_uncurried z z')
Proof.
z, z': Unit
IsEquiv (path_unit_uncurried z z')
  refine (Build_IsEquiv _ _ (path_unit_uncurried z z') (fun _ => tt)
    (fun p:z=z' =>
      match p in (_ = z') return (path_unit_uncurried z z' tt = p) with
        | idpath => match z as z return (path_unit_uncurried z z tt = 1) with
                    | tt => 1
                  end
      end)
    (fun x => match x with tt => 1 end) _).
z, z': Unit
forall x : Unit,
match
  path_unit_uncurried z z' x as p in (_ = z')
  return (path_unit_uncurried z z' tt = p)
with
| 1 =>
    match
      z return (path_unit_uncurried z z tt = 1)
    with
    | tt => 1
    end
end =
ap (path_unit_uncurried z z')
  match x as x0 return (tt = x0) with
  | tt => 1
  end
  intros []; destruct z, z'; reflexivity.
Defined.

Definition equiv_path_unit (z z' : Unit) : Unit <~> (z = z')
  := Build_Equiv _ _ (path_unit_uncurried z z') _.

(** ** Transport *)

(** Is a special case of transporting in a constant fibration. *)

(** ** Universal mapping properties *)

(* The positive universal property *)
Arguments Unit_ind [A] a u : rename.

Global Instance isequiv_unit_ind `{Funext} (A : Unit -> Type)
: IsEquiv (@Unit_ind A) | 0
  := isequiv_adjointify _
  (fun f : forall u:Unit, A u => f tt)
  (fun f : forall u:Unit, A u => path_forall (@Unit_ind A (f tt)) f
                                             (fun x => match x with tt => 1 end))
  (fun _ => 1).

Global Instance isequiv_unit_rec `{Funext} (A : Type)
: IsEquiv (@Unit_ind (fun _ => A)) | 0
  := isequiv_unit_ind (fun _ => A).

#[local]
Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.

Definition equiv_unit_rec `{Funext} (A : Type)
  : A <~> (Unit -> A)
  := (Build_Equiv _ _ (@Unit_ind (fun _ => A)) _).

(* For various reasons, it is typically more convenient to define functions out of the unit as constant maps, rather than [Unit_ind]. *)
Notation unit_name x := (fun (_ : Unit) => x).

Global Instance isequiv_unit_name@{i j} `{Funext} (A : Type@{i})
: @IsEquiv@{i j} _ (Unit -> _) (fun (a:A) => unit_name a).
H: Funext
A: Type
IsEquiv (fun a : A => unit_name a)
Proof.
H: Funext
A: Type
IsEquiv (fun a : A => unit_name a)
  refine (isequiv_adjointify _ (fun f : Unit -> _ => f tt) _ _).
H: Funext
A: Type
(fun x : Unit -> A => unit_name (x tt)) == idmap
H: Funext
A: Type
idmap == idmap
  -
H: Funext
A: Type
(fun x : Unit -> A => unit_name (x tt)) == idmap intros f; apply path_forall@{i i j}; intros x.
H: Funext
A: Type
f: Unit -> A
x: Unit
f tt = f x
    apply ap@{i i}, path_unit.
  -
H: Funext
A: Type
idmap == idmap intros a; reflexivity.
Defined.

(* The negative universal property *)
Definition unit_coind {A : Type} : Unit -> (A -> Unit)
  := fun _ _ => tt.

Global Instance isequiv_unit_coind `{Funext} (A : Type) : IsEquiv (@unit_coind A) | 0.
H: Funext
A: Type
IsEquiv unit_coind
Proof.
H: Funext
A: Type
IsEquiv unit_coind
  refine (isequiv_adjointify _ (fun f => tt) _ _).
H: Funext
A: Type
(fun _ : A -> Unit => unit_coind tt) == idmap
H: Funext
A: Type
unit_name tt == idmap
  -
H: Funext
A: Type
(fun _ : A -> Unit => unit_coind tt) == idmap intro f.
H: Funext
A: Type
f: A -> Unit
unit_coind tt = f apply path_forall; intros x; apply path_unit.
  -
H: Funext
A: Type
unit_name tt == idmap intro x; destruct x; reflexivity.
Defined.

Definition equiv_unit_coind `{Funext} (A : Type)
  : Unit <~> (A -> Unit)
  := Build_Equiv _ _ (@unit_coind A) _.

(** ** Truncation *)

(* The Unit type is contractible *)
Global Instance contr_unit : Contr Unit | 0 := Build_Contr _ tt (fun t : Unit => match t with tt => 1 end).

(** ** Equivalences *)

(** A contractible type is equivalent to [Unit]. *)
Definition equiv_contr_unit `{Contr A} : A <~> Unit
  := equiv_contr_contr.

(* Conversely, a type equivalent to [Unit] is contractible. We don't make this an instance because Coq would have to guess the equivalence.  And when it has a map in mind, it would try to use [isequiv_contr_contr], which would cause a cycle. *)
Definition contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A
  := contr_equiv' Unit f^-1%equiv.

(** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when [const tt] is used in a context that doesn't have [Universe Minimization ToSet] as this file does. If we ever set that globally, then we could get rid of this and remove some imports of this file. *)
Definition const_tt (A : Type) := @const A Unit tt.