Library HoTT.Types.Unit
Require Import Basics.Overture Basics.Equivalences.
Local Open Scope path_scope.
Local Set Universe Minimization ToSet.
Generalizable Variables A.
(* 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.
Proof.
destruct p. destruct z. reflexivity.
Defined.
Instance isequiv_path_unit (z z' : Unit) : IsEquiv (path_unit_uncurried z z') | 0.
Proof.
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) _).
intros []; destruct z, z'; reflexivity.
Defined.
Definition equiv_path_unit (z z' : Unit) : Unit <~> (z = z')
:= Build_Equiv _ _ (path_unit_uncurried z z') _.
(* The positive universal property *)
Arguments Unit_ind [A] a u : rename.
Instance isequiv_unit_ind `{Funext} (A : Unit → Type)
: IsEquiv (@Unit_ind A) | 0
:= isequiv_adjointify _
(fun f : ∀ u:Unit, A u ⇒ f tt)
(fun f : ∀ u:Unit, A u ⇒ path_forall (@Unit_ind A (f tt)) f
(fun x ⇒ match x with tt ⇒ 1 end))
(fun _ ⇒ 1).
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).
Instance isequiv_unit_name@{i j} `{Funext} (A : Type@{i})
: @IsEquiv@{i j} _ (Unit → _) (fun (a:A) ⇒ unit_name a).
Proof.
refine (isequiv_adjointify _ (fun f : Unit → _ ⇒ f tt) _ _).
- intros f; apply path_forall@{i i j}; intros x.
apply ap@{i i}, path_unit.
- intros a; reflexivity.
Defined.
(* The negative universal property *)
Definition unit_coind {A : Type} : Unit → (A → Unit)
:= fun _ _ ⇒ tt.
Instance isequiv_unit_coind `{Funext} (A : Type) : IsEquiv (@unit_coind A) | 0.
Proof.
refine (isequiv_adjointify _ (fun f ⇒ tt) _ _).
- intro f. apply path_forall; intros x; apply path_unit.
- intro x; destruct x; reflexivity.
Defined.
Definition equiv_unit_coind `{Funext} (A : Type)
: Unit <~> (A → Unit)
:= Build_Equiv _ _ (@unit_coind A) _.
(* The Unit type is contractible *)
Instance contr_unit : Contr Unit | 0 := Build_Contr _ tt (fun t : Unit ⇒ match t with tt ⇒ 1 end).
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.
:= 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.