(* -*- mode: coq; mode: visual-line -*- *)
(** * HPropositions *)
Require Import HoTT.Basics HoTT.Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done ]
Local Open Scope path_scope.
Generalizable Variables A B.
(** ** Alternate characterization of hprops. *)
Theorem equiv_hprop_allpath `{Funext} (A : Type )
: IsHProp A <~> (forall (x y : A), x = y).H : Funext A : Type
IsHProp A <~> (forall x y : A, x = y)
Proof .H : Funext A : Type
IsHProp A <~> (forall x y : A, x = y)
rapply (equiv_iff_hprop (@path_ishprop A) (@hprop_allpath A)). H : Funext A : Type
IsHProp (forall x y : A, x = y)
apply hprop_allpath; intros f g.H : Funext A : Type f, g : forall x y : A, x = y
f = g
funext x y. H : Funext A : Type f, g : forall x y : A, x = yx, y : A
f x y = g x y
pose (C := Build_Contr A x (f x)).H : Funext A : Type f, g : forall x y : A, x = yx, y : A C := Build_Contr A x (f x) : Contr A
f x y = g x y
apply path_contr.
Defined .
Theorem equiv_hprop_inhabited_contr `{Funext} {A}
: IsHProp A <~> (A -> Contr A).H : Funext A : Type
IsHProp A <~> (A -> Contr A)
Proof .H : Funext A : Type
IsHProp A <~> (A -> Contr A)
apply (equiv_adjointify (@contr_inhabited_hprop A) (@hprop_inhabited_contr A)).H : Funext A : Type
(fun x : A -> Contr A => contr_inhabited_hprop A) ==
idmap
- H : Funext A : Type
(fun x : A -> Contr A => contr_inhabited_hprop A) ==
idmap
intro ic.H : Funext A : Type ic : A -> Contr A
contr_inhabited_hprop A = ic
by_extensionality x. H : Funext A : Type ic : A -> Contr A x : A
contr_inhabited_hprop A x = ic x
apply @path_contr.H : Funext A : Type ic : A -> Contr A x : A
Contr (Contr A)
apply contr_istrunc.H : Funext A : Type ic : A -> Contr A x : A
Contr A
exact (ic x).
- H : Funext A : Type
(fun x : IsHProp A =>
hprop_inhabited_contr A (contr_inhabited_hprop A)) ==
idmap
intro hp.H : Funext A : Type hp : IsHProp A
hprop_inhabited_contr A (contr_inhabited_hprop A) = hp
apply path_ishprop.
Defined .
(** Being an hprop is also equivalent to the diagonal being an equivalence. *)
Definition ishprop_isequiv_diag {A } `{IsEquiv _ _ (fun (a :A) => (a,a))}
: IsHProp A.A : Type H : IsEquiv (fun a : A => (a, a))
IsHProp A
Proof .A : Type H : IsEquiv (fun a : A => (a, a))
IsHProp A
apply hprop_allpath; intros x y.A : Type H : IsEquiv (fun a : A => (a, a)) x, y : A
x = y
set (d := fun (a :A) => (a,a)) in *.A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
x = y
transitivity (fst (d (d^-1 (x,y)))).A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
x = fst (d (d^-1 (x, y)))
- A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
x = fst (d (d^-1 (x, y)))
exact (ap fst (eisretr d (x,y))^).
- A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
fst (d (d^-1 (x, y))) = y
transitivity (snd (d (d^-1 (x,y)))).A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
fst (d (d^-1 (x, y))) = snd (d (d^-1 (x, y)))
+ A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
fst (d (d^-1 (x, y))) = snd (d (d^-1 (x, y)))
unfold d; reflexivity .
+ A : Type d := fun a : A => (a, a): A -> A * A H : IsEquiv d x, y : A
snd (d (d^-1 (x, y))) = y
exact (ap snd (eisretr d (x,y))).
Defined .
Global Instance isequiv_diag_ishprop {A } `{IsHProp A}
: IsEquiv (fun (a :A) => (a,a)).A : Type IsHProp0 : IsHProp A
IsEquiv (fun a : A => (a, a))
Proof .A : Type IsHProp0 : IsHProp A
IsEquiv (fun a : A => (a, a))
refine (isequiv_adjointify _ fst _ _).A : Type IsHProp0 : IsHProp A
(fun x : A * A => (fst x, fst x)) == idmap
- A : Type IsHProp0 : IsHProp A
(fun x : A * A => (fst x, fst x)) == idmap
intros [x y].A : Type IsHProp0 : IsHProp A x, y : A
(fst (x, y), fst (x, y)) = (x, y)
apply path_prod; simpl .A : Type IsHProp0 : IsHProp A x, y : A
x = x
+ A : Type IsHProp0 : IsHProp A x, y : A
x = x
reflexivity .
+ A : Type IsHProp0 : IsHProp A x, y : A
x = y
apply path_ishprop.
- A : Type IsHProp0 : IsHProp A
(fun x : A => fst (x, x)) == idmap
intros a; simpl .A : Type IsHProp0 : IsHProp A a : A
a = a
reflexivity .
Defined .
(** ** A map is an embedding as soon as its ap's have sections. *)
Definition isembedding_sect_ap {X Y } (f : X -> Y)
(s : forall x1 x2 , (f x1 = f x2) -> (x1 = x2))
(H : forall x1 x2 , (@ap X Y f x1 x2) o (s x1 x2) == idmap)
: IsEmbedding f.X, Y : Type f : X -> Y s : forall x1 x2 : X, f x1 = f x2 -> x1 = x2H : forall x1 x2 : X, ap f o s x1 x2 == idmap
IsEmbedding f
Proof .X, Y : Type f : X -> Y s : forall x1 x2 : X, f x1 = f x2 -> x1 = x2H : forall x1 x2 : X, ap f o s x1 x2 == idmap
IsEmbedding f
intros y.X, Y : Type f : X -> Y s : forall x1 x2 : X, f x1 = f x2 -> x1 = x2H : forall x1 x2 : X, ap f o s x1 x2 == idmapy : Y
IsHProp (hfiber f y)
apply hprop_allpath.X, Y : Type f : X -> Y s : forall x1 x2 : X, f x1 = f x2 -> x1 = x2H : forall x1 x2 : X, ap f o s x1 x2 == idmapy : Y
forall x y0 : hfiber f y, x = y0
intros [x1 p1] [x2 p2].X, Y : Type f : X -> Y s : forall x1 x2 : X, f x1 = f x2 -> x1 = x2H : forall x1 x2 : X, ap f o s x1 x2 == idmapy : Y x1 : X p1 : f x1 = y x2 : X p2 : f x2 = y
(x1; p1) = (x2; p2)
apply path_sigma with (s x1 x2 (p1 @ p2^)).X, Y : Type f : X -> Y s : forall x1 x2 : X, f x1 = f x2 -> x1 = x2H : forall x1 x2 : X, ap f o s x1 x2 == idmapy : Y x1 : X p1 : f x1 = y x2 : X p2 : f x2 = y
transport (fun x : X => f x = y) (s x1 x2 (p1 @ p2^))
(x1; p1).2 = (x2; p2).2
abstract (rewrite transport_paths_Fl; cbn ;
rewrite (H x1 x2 (p1 @ p2^));
rewrite inv_pp, inv_V; apply concat_pV_p).
Defined .
(** ** Alternate characterizations of contractibility. *)
Theorem equiv_contr_inhabited_hprop `{Funext} {A}
: Contr A <~> A * IsHProp A.H : Funext A : Type
Contr A <~> A * IsHProp A
Proof .H : Funext A : Type
Contr A <~> A * IsHProp A
assert (f : Contr A -> A * IsHProp A).H : Funext A : Type
Contr A -> A * IsHProp A
- H : Funext A : Type
Contr A -> A * IsHProp A
intro P.H : Funext A : Type P : Contr A
A * IsHProp A
split .H : Funext A : Type P : Contr A
A
+ H : Funext A : Type P : Contr A
A
exact (@center _ P).
+ H : Funext A : Type P : Contr A
IsHProp A
apply @istrunc_succ.H : Funext A : Type P : Contr A
Contr A
exact P.
- H : Funext A : Type f : Contr A -> A * IsHProp A
Contr A <~> A * IsHProp A
assert (g : A * IsHProp A -> Contr A).H : Funext A : Type f : Contr A -> A * IsHProp A
A * IsHProp A -> Contr A
+ H : Funext A : Type f : Contr A -> A * IsHProp A
A * IsHProp A -> Contr A
intros [a P].H : Funext A : Type f : Contr A -> A * IsHProp A a : A P : IsHProp A
Contr A
apply (@contr_inhabited_hprop _ P a).
+ H : Funext A : Type f : Contr A -> A * IsHProp A g : A * IsHProp A -> Contr A
Contr A <~> A * IsHProp A
refine (@equiv_iff_hprop _ _ _ _ f g).H : Funext A : Type f : Contr A -> A * IsHProp A g : A * IsHProp A -> Contr A
IsHProp (A * IsHProp A)
apply hprop_inhabited_contr; intro p.H : Funext A : Type f : Contr A -> A * IsHProp A g : A * IsHProp A -> Contr A p : A * IsHProp A
Contr (A * IsHProp A)
apply @contr_prod.H : Funext A : Type f : Contr A -> A * IsHProp A g : A * IsHProp A -> Contr A p : A * IsHProp A
Contr A
* H : Funext A : Type f : Contr A -> A * IsHProp A g : A * IsHProp A -> Contr A p : A * IsHProp A
Contr A
exact (g p).
* H : Funext A : Type f : Contr A -> A * IsHProp A g : A * IsHProp A -> Contr A p : A * IsHProp A
Contr (IsHProp A)
apply (@contr_inhabited_hprop _ _ (snd p)).
Defined .
Theorem equiv_contr_inhabited_allpath `{Funext} {A}
: Contr A <~> A * forall (x y : A), x = y.H : Funext A : Type
Contr A <~> A * (forall x y : A, x = y)
Proof .H : Funext A : Type
Contr A <~> A * (forall x y : A, x = y)
transitivity (A * IsHProp A).H : Funext A : Type
Contr A <~> A * IsHProp A
- H : Funext A : Type
Contr A <~> A * IsHProp A
apply equiv_contr_inhabited_hprop.
- H : Funext A : Type
A * IsHProp A <~> A * (forall x y : A, x = y)
exact (1 *E equiv_hprop_allpath _).
Defined .
(** ** Logical equivalence of hprops *)
(** Logical equivalence of hprops is not just logically equivalent to equivalence, it is equivalent to it. *)
Global Instance isequiv_equiv_iff_hprop_uncurried
`{Funext} {A B} `{IsHProp A} `{IsHProp B}
: IsEquiv (@equiv_iff_hprop_uncurried A _ B _) | 0 .H : Funext A, B : Type IsHProp0 : IsHProp A IsHProp1 : IsHProp B
IsEquiv equiv_iff_hprop_uncurried
Proof .H : Funext A, B : Type IsHProp0 : IsHProp A IsHProp1 : IsHProp B
IsEquiv equiv_iff_hprop_uncurried
pose (@istrunc_equiv).H : Funext A, B : Type IsHProp0 : IsHProp A IsHProp1 : IsHProp B i := @istrunc_equiv : Funext ->
forall (n : trunc_index)
(A B : Type ),
IsTrunc n.+1 B -> IsTrunc n.+1 (A <~> B)
IsEquiv equiv_iff_hprop_uncurried
refine (isequiv_adjointify
equiv_iff_hprop_uncurried
(fun e => (@equiv_fun _ _ e, @equiv_inv _ _ e _))
_ _);
intro ;
by apply path_ishprop.
Defined .
Definition equiv_equiv_iff_hprop
`{Funext} (A B : Type ) `{IsHProp A} `{IsHProp B}
: (A <-> B) <~> (A <~> B)
:= Build_Equiv _ _ (@equiv_iff_hprop_uncurried A _ B _) _.
(** ** Inhabited and uninhabited hprops *)
(** If an hprop is inhabited, then it is equivalent to [Unit]. *)
Lemma if_hprop_then_equiv_Unit (hprop : Type ) `{IsHProp hprop} : hprop -> hprop <~> Unit.hprop : Type IsHProp0 : IsHProp hprop
hprop -> hprop <~> Unit
Proof .hprop : Type IsHProp0 : IsHProp hprop
hprop -> hprop <~> Unit
intro p.hprop : Type IsHProp0 : IsHProp hprop p : hprop
hprop <~> Unit
apply equiv_iff_hprop.hprop : Type IsHProp0 : IsHProp hprop p : hprop
hprop -> Unit
- hprop : Type IsHProp0 : IsHProp hprop p : hprop
hprop -> Unit
exact (fun _ => tt).
- hprop : Type IsHProp0 : IsHProp hprop p : hprop
Unit -> hprop
exact (fun _ => p).
Defined .
(** If an hprop is not inhabited, then it is equivalent to [Empty]. *)
Lemma if_not_hprop_then_equiv_Empty (hprop : Type ) `{IsHProp hprop} : ~hprop -> hprop <~> Empty.hprop : Type IsHProp0 : IsHProp hprop
~ hprop -> hprop <~> Empty
Proof .hprop : Type IsHProp0 : IsHProp hprop
~ hprop -> hprop <~> Empty
intro np.hprop : Type IsHProp0 : IsHProp hprop np : ~ hprop
hprop <~> Empty
exact (Build_Equiv _ _ np _).
Defined .
(** Thus, a decidable hprop is either equivalent to [Unit] or [Empty]. *)
Definition equiv_decidable_hprop (hprop : Type )
`{IsHProp hprop} `{Decidable hprop}
: (hprop <~> Unit) + (hprop <~> Empty).hprop : Type IsHProp0 : IsHProp hprop H : Decidable hprop
(hprop <~> Unit) + (hprop <~> Empty)
Proof .hprop : Type IsHProp0 : IsHProp hprop H : Decidable hprop
(hprop <~> Unit) + (hprop <~> Empty)
destruct (dec hprop) as [x|nx].hprop : Type IsHProp0 : IsHProp hprop H : Decidable hprop x : hprop
(hprop <~> Unit) + (hprop <~> Empty)
- hprop : Type IsHProp0 : IsHProp hprop H : Decidable hprop x : hprop
(hprop <~> Unit) + (hprop <~> Empty)
exact (inl (if_hprop_then_equiv_Unit hprop x)).
- hprop : Type IsHProp0 : IsHProp hprop H : Decidable hprop nx : ~ hprop
(hprop <~> Unit) + (hprop <~> Empty)
exact (inr (if_not_hprop_then_equiv_Empty hprop nx)).
Defined .