(** * HPropositions *)

Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Empty Types.Unit Types.Prod Types.Paths Types.Sigma Types.Equiv.

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 = y
x, 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 = y
x, 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 : IsHProp A =>
 hprop_inhabited_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
fst (d (d^-1 (x, y))) = 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
snd (d (d^-1 (x, y))) = 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.

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 => fst (x, 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 = y
    +
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 = x2
H: 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 = x2
H: 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 = x2
H: forall x1 x2 : X, ap f o s x1 x2 == idmap
y: Y
IsHProp (hfiber f y)
  apply hprop_allpath.
X, Y: Type
f: X -> Y
s: forall x1 x2 : X, f x1 = f x2 -> x1 = x2
H: forall x1 x2 : X, ap f o s x1 x2 == idmap
y: 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 = x2
H: forall x1 x2 : X, ap f o s x1 x2 == idmap
y: 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 = x2
H: forall x1 x2 : X, ap f o s x1 x2 == idmap
y: 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
f: Contr A -> A * IsHProp A
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
IsHProp 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
g: A * IsHProp A -> Contr A
Contr A <~> A * IsHProp 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 exact (@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 (IsHProp 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) exact (@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
A * IsHProp A <~> A * (forall x y : A, x = y)
  -
H: Funext
A: Type
Contr A <~> A * IsHProp A exact 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. *)
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
Unit -> hprop
  -
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
nx: ~ 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.

(** ** Stable types and stable hprops *)

(** Recall that a type [A] is "stable" if [~~A -> A]. *)

(** When [A] is an hprop, so is [Stable A] (by [ishprop_stable_hprop]), so [Stable A * IsHProp A] is an hprop for any [A]. *)
Instance ishprop_stable_ishprop `{Funext} (A : Type) : IsHProp (Stable A * IsHProp A).
H: Funext
A: Type
IsHProp (Stable A * IsHProp A)
Proof.
H: Funext
A: Type
IsHProp (Stable A * IsHProp A)
  apply istrunc_inhabited_istrunc; intros [stable ishprop].
H: Funext
A: Type
stable: Stable A
ishprop: IsHProp A
IsHProp (Stable A * IsHProp A)
  exact _.
Defined.

(** Under function extensionality, if [A] is a stable type, then [~~A] is the propositional truncation of [A]. Here, for dependency reasons, we don't give the equivalence to [Tr (-1) A], but just show that the recursion principle holds. See Metatheory/ImpredicativeTruncation.v for a generalization to all types, and Modalities/Notnot.v for a description of the universal property of [~~A] when [A] is not assumed to be stable. *)

(** Any negation is an hprop, by [istrunc_Empty] and [istrunc_arrow]. In particular, double-negation is an hprop. *)
Definition ishprop_not_not `{Funext} {A : Type} : IsHProp (~~A) := _.

(** The recursion principle for [~~A] when [A] is stable. *)
Definition not_not_rec {A : Type} `{stable : Stable A} (P : HProp) (f : A -> P)
  : ~~A -> P.
A: Type
stable: Stable A
P: HProp
f: A -> P
~~ A -> P
Proof.
A: Type
stable: Stable A
P: HProp
f: A -> P
~~ A -> P
  intro nna.
A: Type
stable: Stable A
P: HProp
f: A -> P
nna: ~~ A
P
  exact (f (stable nna)).
Defined.

(** The unit is [not_not_unit : A -> ~~A], and the computation rule only holds propositionally. *)
Definition not_not_rec_beta {A : Type} `{Stable A} (P : HProp) (f : A -> P) (a : A)
  : not_not_rec P f (not_not_unit a) = f a
  := path_ishprop _ _.

(** The map [A -> ~~A] is an equivalence if and only if [A] is a stable hprop.  This characterizes the local types for the double-negation modality.  See Modality/Notnot.v. *)
Definition isequiv_not_not_unit_iff_stable_hprop `{Funext} A
  : IsEquiv (@not_not_unit A) <-> (Stable A * IsHProp A).
H: Funext
A: Type
IsEquiv not_not_unit <-> Stable A * IsHProp A
Proof.
H: Funext
A: Type
IsEquiv not_not_unit <-> Stable A * IsHProp A
  split.
H: Funext
A: Type
IsEquiv not_not_unit -> Stable A * IsHProp A
H: Funext
A: Type
Stable A * IsHProp A -> IsEquiv not_not_unit
  -
H: Funext
A: Type
IsEquiv not_not_unit -> Stable A * IsHProp A intros iseq.
H: Funext
A: Type
iseq: IsEquiv not_not_unit
Stable A * IsHProp A
    pose proof (eq := (Build_Equiv _ _ _ iseq)^-1%equiv); clear iseq.
H: Funext
A: Type
eq: ~~ A <~> A
Stable A * IsHProp A
    exact (stable_equiv eq _, istrunc_equiv_istrunc _ eq).
  -
H: Funext
A: Type
Stable A * IsHProp A -> IsEquiv not_not_unit intros [stable ishprop].
H: Funext
A: Type
stable: Stable A
ishprop: IsHProp A
IsEquiv not_not_unit
    rapply isequiv_iff_hprop.
H: Funext
A: Type
stable: Stable A
ishprop: IsHProp A
~~ A -> A
    exact stable.
Defined.

(** We can upgrade the previous "iff" result to an equivalence. *)
Definition equiv_isequiv_not_not_unit_stable_hprop `{Funext} (P : Type)
  : IsEquiv (@not_not_unit P) <~> (Stable P * IsHProp P)
  := equiv_iff_hprop_uncurried (isequiv_not_not_unit_iff_stable_hprop P).

(** ** A generalization of [ishprop_decpaths] *)

(** Under [Funext], [ishprop_decpaths] shows that [DecidablePaths A] is an hprop.  More generally, it's also an hprop with the first argument fixed. *)
Instance ishprop_decpaths' `{Funext} {A : Type} (x : A)
  : IsHProp (forall (y : A), Decidable (x = y)).
H: Funext
A: Type
x: A
IsHProp (forall y : A, Decidable (x = y))
Proof.
H: Funext
A: Type
x: A
IsHProp (forall y : A, Decidable (x = y))
  apply hprop_allpath; intros d d'.
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
d = d'
  (* Define [C] to be the component of [A] containing [x]. Since [x = y] is decidable, it is stable, so we can use [~~(x = y)] as an elementary form of propositional truncation. It also works to use [merely] here, but that brings in further dependencies and requires HITs. *)
  pose (C := {y : A & ~~(x = y)}).
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
d = d'
  assert (cC : Contr C).
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
Contr C
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
d = d'
  {
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
Contr C snapply (Build_Contr C (x; not_not_unit idpath)).
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
forall y : C, (x; not_not_unit 1) = y
    intros [y p].
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
y: A
p: ~~ (x = y)
(x; not_not_unit 1) = (y; p)
    srapply path_sigma_hprop; cbn.
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
y: A
p: ~~ (x = y)
x = y
    (* [d y] either solves the goal or contradicts [p]. *)
    by destruct (d y). }
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
d = d'
  funext y.
H: Funext
A: Type
x: A
d, d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d y = d' y
  generalize (d y); clear d; intros d.
H: Funext
A: Type
x: A
d': forall y : A, Decidable (x = y)
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d: Decidable (x = y)
d = d' y
  generalize (d' y); clear d'; intros d'.
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': Decidable (x = y)
d = d'
  destruct d as [d | nd]; destruct d' as [d' | nd'].
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': x = y
inl d = inl d'
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d: x = y
nd': x <> y
inl d = inr nd'
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
nd: x <> y
d': x = y
inr nd = inl d'
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
nd, nd': x <> y
inr nd = inr nd'
  -
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': x = y
inl d = inl d' apply ap.
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': x = y
d = d'
    (* [x] and [y] are "in" the component [C]: *)
    pose (xC := (x; not_not_unit idpath) : C).
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': x = y
xC:= (x; not_not_unit 1) : C: C
d = d'
    pose (yC := (y; not_not_unit d) : C).
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': x = y
xC:= (x; not_not_unit 1) : C: C
yC:= (y; not_not_unit d) : C: C
d = d'
    (* [d] and [d'] can be lifted to equalities of type [xC = yC] using [path_sigma_hprop], and so up to the computation rule for [pr1_path] (denoted "..1"), our goal is in the image of "..1". *)
    refine ((pr1_path_path_sigma_hprop xC yC d)^ @ _ @ pr1_path_path_sigma_hprop xC yC d').
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d, d': x = y
xC:= (x; not_not_unit 1) : C: C
yC:= (y; not_not_unit d) : C: C
(path_sigma_hprop xC yC d) ..1 =
(path_sigma_hprop xC yC d') ..1
    (* But since [C] is an hset, the paths in [C] are equal. *)
    apply ap, path_ishprop.
  (* The remaining cases are the same as in [ishprop_decpaths], but the last bullet is shorter since typeclass search tells us that [x <> y] is an hprop. *)
  -
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
d: x = y
nd': x <> y
inl d = inr nd' elim (nd' d).
  -
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
nd: x <> y
d': x = y
inr nd = inl d' elim (nd d').
  -
H: Funext
A: Type
x: A
C:= {y : A & ~~ (x = y)}: Type
cC: Contr C
y: A
nd, nd': x <> y
inr nd = inr nd' apply ap, path_ishprop.
Defined.