Core.v

Require Import Basics Types WildCat.Core WildCat.Universe HFiber.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Modalities.Modality.
(** Users of this file almost always want to be able to write [Tr n] for both a [Modality] and a [ReflectiveSubuniverse], so they want the coercion [modality_to_reflective_subuniverse]: *)
Require Export (coercions) Modalities.Modality.

(** * Truncations of types *)

Local Open Scope path_scope.
Generalizable Variables A X n.

(** ** The definition *)

(** The definition of [Trunc n], the n-truncation of a type.

If Coq supported higher inductive types natively, we would construct this as something like:

   Inductive Trunc n (A : Type) : Type :=
   | tr : A -> Trunc n A
   | istrunc_truncation : forall (f : Sphere n.+1 -> Trunc n A)
       (x : Sphere n.+1), f x = f North.

However, while we are faking our higher-inductives anyway, we can take some shortcuts, rather than translating the definition above.  Firstly, we directly posit a “constructor” giving truncatedness, rather than rephrasing it in terms of maps of spheres.  Secondly, we omit the “computation rule” for this constructor, since it is implied by truncatedness of the result type (and, for essentially that reason, is never wanted in practice anyway).
*)

Module Export Trunc.

  Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
    tr : A -> Trunc n A.
  Arguments tr {n A} a.

  (** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
  #[export] Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
    : IsTrunc@{j} n (Trunc@{i} n A).n: trunc_index
A: Type
IsTrunc n (Trunc n A)
  Admitted.

  Definition Trunc_ind {n A}
    (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
    : (forall a, P (tr a)) -> (forall aa, P aa)
    := fun f aa => match aa with tr a => fun _ => f a end Pt.

End Trunc.

(** The non-dependent version of the eliminator. *)

Definition Trunc_rec {n A X} `{IsTrunc n X}
  : (A -> X) -> (Trunc n A -> X)
  := Trunc_ind (fun _ => X).

Definition Trunc_rec_tr n {A : Type}
  : Trunc_rec (A:=A) (tr (n:=n)) == idmap
  := Trunc_ind _ (fun a => idpath).

(** ** Tactic to remove truncations in hypotheses if possible *)

Ltac strip_truncations :=
  progress repeat
    match goal with
    | [ T : _ |- _ ]
      => revert_opaque T;
        refine (@Trunc_ind _ _ _ _ _);
        (* Ensure that we didn't generate more than one subgoal, i.e. that the goal was appropriately truncated: *)
        [];
        intro T
    end.

(** See [strip_reflections] and [strip_modalities] for generalizations to other reflective subuniverses and modalities.  We provide this version because it sometimes needs fewer universes (due to the cumulativity of [Trunc]).  However, that same cumulativity sometimes causes free universe variables.  For a hypothesis of type [Trunc@{i} X], we can use [Trunc_ind@{i j}], but sometimes Coq uses [Trunc_ind@{k j}] with [i <= k] and [k] otherwise free.  In these cases, [strip_reflections] and/or [strip_modalities] may generate fewer universe variables. *)

(** ** [Trunc] is a modality *)

Definition Tr (n : trunc_index) : Modality.n: trunc_index
Modality
Proof.n: trunc_index
Modality
  srapply (Build_Modality (fun A => IsTrunc n A)); cbn.n: trunc_index
forall T U : Type,
IsTrunc n T ->
forall f : T -> U, IsEquiv f -> IsTrunc n U
n: trunc_index
Type -> Type
n: trunc_index
forall T : Type, IsTrunc n (?Goal0 T)
n: trunc_index
forall T : Type, T -> ?Goal0 T
n: trunc_index
forall (A : Type) (B : ?Goal0 A -> Type),
(forall oa : ?Goal0 A, IsTrunc n (B oa)) ->
(forall a : A, B (?Goal2 A a)) ->
forall z : ?Goal0 A, B z
n: trunc_index
forall (A : Type) (B : ?Goal0 A -> Type)
(B_inO : forall oa : ?Goal0 A, IsTrunc n (B oa))
(f : forall a : A, B (?Goal2 A a)) (a : A),
?Goal3 A B B_inO f (?Goal2 A a) = f a
n: trunc_index
forall A : Type,
IsTrunc n A -> forall z z' : A, IsTrunc n (z = z')
  -n: trunc_index
forall T U : Type,
IsTrunc n T ->
forall f : T -> U, IsEquiv f -> IsTrunc n U intros A B ? f ?; exact (istrunc_isequiv_istrunc A f).
  -n: trunc_index
Type -> Type exact (Trunc n).
  -n: trunc_index
forall T : Type, IsTrunc n (Trunc n T) intros; apply istrunc_truncation.
  -n: trunc_index
forall T : Type, T -> Trunc n T intros A; exact tr.
  -n: trunc_index
forall (A : Type) (B : Trunc n A -> Type),
(forall oa : Trunc n A, IsTrunc n (B oa)) ->
(forall a : A, B ((fun A0 : Type => tr) A a)) ->
forall z : Trunc n A, B z intros A B ? f oa; cbn in *.n: trunc_index
A: Type
B: Trunc n A -> Type
B_inO: forall oa : Trunc n A, IsTrunc n (B oa)
f: forall a : A, B (tr a)
oa: Trunc n A
B oa
    exact (Trunc_ind B f oa).
  -n: trunc_index
forall (A : Type) (B : Trunc n A -> Type)
(B_inO : forall oa : Trunc n A, IsTrunc n (B oa))
(f : forall a : A, B ((fun A0 : Type => tr) A a))
(a : A),
(fun (A0 : Type) (B0 : Trunc n A0 -> Type)
   (B_inO0 : forall oa : Trunc n A0, IsTrunc n (B0 oa))
   (f0 : forall a0 : A0,
         B0 ((fun A1 : Type => tr) A0 a0))
   (oa : Trunc n A0) => Trunc_ind B0 f0 oa : B0 oa) A
  B B_inO f ((fun A0 : Type => tr) A a) = f a intros; reflexivity.
  -n: trunc_index
forall A : Type,
IsTrunc n A -> forall z z' : A, IsTrunc n (z = z') exact (@istrunc_paths' n).
Defined.

(** We don't usually declare modalities as coercions, but this particular one is convenient so that lemmas about (for instance) connected maps can be applied to truncation modalities without the user/reader needing to be (particularly) aware of the general notion of modality. *)
Coercion Tr : trunc_index >-> Modality.
(** However, if the coercion is not printed, then we get things like [Tr (-1) X] being printed as [(-1) X], which is terribly confusing.  So we tell Coq to always print this coercion.  This does mean that although the user can type things like [IsConnected n X], it will always be displayed back as [IsConnected (Tr n) X]. *)
Add Printing Coercion Tr.

Section TruncationModality.
  Context (n : trunc_index).

  Definition trunc_iff_isequiv_truncation (A : Type)
    : IsTrunc n A <-> IsEquiv (@tr n A)
    := inO_iff_isequiv_to_O (Tr n) A.

  #[export] Instance isequiv_tr A `{IsTrunc n A} : IsEquiv (@tr n A)
    := fst (trunc_iff_isequiv_truncation A) _.

  Definition equiv_tr (A : Type) `{IsTrunc n A}
    : A <~> Tr n A
  := Build_Equiv _ _ (@tr n A) _.

  Definition untrunc_istrunc {A : Type} `{IsTrunc n A}
    : Tr n A -> A
    := (@tr n A)^-1.

  (** ** Functoriality *)

  (** Since a modality lives on a single universe, by default if we simply define [Trunc_functor] to be [O_functor] then it would force [X] and [Y] to live in the same universe.  But since we defined [Trunc] as a cumulative inductive, if we add universe annotations we can make [Trunc_functor] more universe-polymorphic than [O_functor] is.  This is sometimes useful.  *)
  Definition Trunc_functor@{i j k | i <= k, j <= k} {X : Type@{i}} {Y : Type@{j}} (f : X -> Y)
    : Tr@{i} n X -> Tr@{j} n Y
    := O_functor@{k k k} (Tr n) f.

  #[export] Instance is0functor_Tr : Is0Functor (Tr n)
    := Build_Is0Functor _ _ _ _ (Tr n) (@Trunc_functor).

  #[export] Instance Trunc_functor_isequiv {X Y : Type}
    (f : X -> Y) `{IsEquiv _ _ f}
    : IsEquiv (Trunc_functor f)
    := isequiv_O_functor (Tr n) f.

  Definition Trunc_functor_equiv {X Y : Type} (f : X <~> Y)
    : Tr n X <~> Tr n Y
    := equiv_O_functor (Tr n) f.

  Definition Trunc_functor_compose {X Y Z} (f : X -> Y) (g : Y -> Z)
    : Trunc_functor (g o f) == Trunc_functor g o Trunc_functor f
    := O_functor_compose (Tr n) f g.

  Definition Trunc_functor_idmap (X : Type)
    : @Trunc_functor X X idmap == idmap
    := O_functor_idmap (Tr n) X.

  Definition equiv_Trunc_prod_cmp {X Y}
    : Tr n (X * Y) <~> Tr n X * Tr n Y
    := equiv_O_prod_cmp (Tr n) X Y.

  #[export] Instance is1functor_Tr : Is1Functor (Tr n).n: trunc_index
Is1Functor (Tr n)
  Proof.n: trunc_index
Is1Functor (Tr n)
    apply Build_Is1Functor.n: trunc_index
forall (a b : Type) (f g : a $-> b),
f $== g -> fmap (Tr n) f $== fmap (Tr n) g
n: trunc_index
forall a : Type, fmap (Tr n) (Id a) $== Id (Tr n a)
n: trunc_index
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap (Tr n) (g $o f) $==
fmap (Tr n) g $o fmap (Tr n) f
    -n: trunc_index
forall (a b : Type) (f g : a $-> b),
f $== g -> fmap (Tr n) f $== fmap (Tr n) g apply @O_functor_homotopy.
    -n: trunc_index
forall a : Type, fmap (Tr n) (Id a) $== Id (Tr n a) exact @Trunc_functor_idmap.
    -n: trunc_index
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap (Tr n) (g $o f) $==
fmap (Tr n) g $o fmap (Tr n) f exact @Trunc_functor_compose.
  Defined.

End TruncationModality.

(** We have to teach Coq to translate back and forth between [IsTrunc n] and [In (Tr n)]. *)
Instance inO_tr_istrunc {n : trunc_index} (A : Type) `{IsTrunc n A}
  : In (Tr n) A.n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
In (Tr n) A
Proof.n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
In (Tr n) A
  assumption.
Defined.

(** Having both of these as [Instance]s would cause infinite loops. *)
Definition istrunc_inO_tr {n : trunc_index} (A : Type) `{In (Tr n) A}
  : IsTrunc n A.n: trunc_index
A: Type
H: In (Tr n) A
IsTrunc n A
Proof.n: trunc_index
A: Type
H: In (Tr n) A
IsTrunc n A
  assumption.
Defined.

(** Instead, we make the latter an immediate instance, but with high cost (i.e. low priority) so that it doesn't override the ordinary lemmas about truncation.  Unfortunately, [Hint Immediate] doesn't allow specifying a cost, so we use [Hint Extern] instead. *)
(** Hint Immediate istrunc_inO_tr : typeclass_instances. *)
(** See https://github.com/coq/coq/issues/11697 *)
#[export]
Hint Extern 1000 (IsTrunc _ _) => simple apply istrunc_inO_tr; solve [ trivial ] : typeclass_instances.
(** This doesn't seem to be quite the same as [Hint Immediate] with a different cost either, though.  *)

(** Unfortunately, this isn't perfect; Coq still can't always find [In n] hypotheses in the context when it wants [IsTrunc].  You can always apply [istrunc_inO_tr] explicitly, but sometimes it also works to just [pose] it into the context (at the risk of causing loops in typeclass search). *)

(** We do the same for [IsTruncMap n] and [MapIn (Tr n)]. *)
Instance mapinO_tr_istruncmap {n : trunc_index} {A B : Type}
  (f : A -> B) `{IsTruncMap n A B f}
  : MapIn (Tr n) f.n: trunc_index
A, B: Type
f: A -> B
H: IsTruncMap n f
MapIn (Tr n) f
Proof.n: trunc_index
A, B: Type
f: A -> B
H: IsTruncMap n f
MapIn (Tr n) f
  assumption.
Defined.

Definition istruncmap_mapinO_tr {n : trunc_index} {A B : Type}
  (f : A -> B) `{MapIn (Tr n) _ _ f}
  : IsTruncMap n f.n: trunc_index
A, B: Type
f: A -> B
H: MapIn (Tr n) f
IsTruncMap n f
Proof.n: trunc_index
A, B: Type
f: A -> B
H: MapIn (Tr n) f
IsTruncMap n f
  assumption.
Defined.

#[export]
Hint Immediate istruncmap_mapinO_tr : typeclass_instances.

(** ** How stability and decidability interact with truncation *)

(** For [n >= -1], a stable type is logically equivalent to its [n]-truncation. (It follows that this is true for decidable types as well.) *)
Definition trunc_inhabited_iff_inhabited_stable (n : trunc_index) {A} {A_stable : Stable A}
  : Tr n.+1 A <-> A.n: trunc_index
A: Type
A_stable: Stable A
Tr n.+1 A <-> A
Proof.n: trunc_index
A: Type
A_stable: Stable A
Tr n.+1 A <-> A
  nrefine (_, tr).n: trunc_index
A: Type
A_stable: Stable A
Tr n.+1 A -> A
  intro ma.n: trunc_index
A: Type
A_stable: Stable A
ma: Tr n.+1 A
A
  apply stable; intro na.n: trunc_index
A: Type
A_stable: Stable A
ma: Tr n.+1 A
na: ~ A
Empty
  strip_truncations.n: trunc_index
A: Type
A_stable: Stable A
na: ~ A
ma: A
Empty
  exact (na ma).
Defined.

(** The most common case involves [Tr (-1)], so we give it its own name. *)
Definition merely_inhabited_iff_inhabited_stable {A} {A_stable : Stable A}
  : Tr (-1) A <-> A
  := trunc_inhabited_iff_inhabited_stable (-2).

Instance decidable_trunc_decidable (n : trunc_index) {A} {A_decidable : Decidable A}
  : Decidable (Tr n.+1 A).n: trunc_index
A: Type
A_decidable: Decidable A
Decidable (Tr n.+1 A)
Proof.n: trunc_index
A: Type
A_decidable: Decidable A
Decidable (Tr n.+1 A)
  rapply decidable_iff.n: trunc_index
A: Type
A_decidable: Decidable A
A <-> Tr n.+1 A
  symmetry; rapply trunc_inhabited_iff_inhabited_stable.
Defined.

(** ** A few special things about the (-2)-truncation *)

(** The type of contractible types is contractible. *)
Definition contr_tr_minus_two@{u su | u < su} `{Univalence}
  : Contr (Type_@{u su} (Tr (-2))).H: Univalence
Contr (Type_ (Tr (-2)))
Proof.H: Univalence
Contr (Type_ (Tr (-2)))
  apply (Build_Contr _ (exist@{su su} _ (Unit : Type@{u}) (inO_tr_istrunc _))).H: Univalence
forall y : {x : _ & In (Tr (-2)) x},
(Unit; inO_tr_istrunc Unit) = y
  intros [C ContrC].H: Univalence
C: Type
ContrC: In (Tr (-2)) C
(Unit; inO_tr_istrunc Unit) = (C; ContrC)
  apply equiv_path_sigma_hprop.H: Univalence
C: Type
ContrC: In (Tr (-2)) C
(Unit; inO_tr_istrunc Unit).1 = (C; ContrC).1
  apply path_universe_uncurried.H: Univalence
C: Type
ContrC: In (Tr (-2)) C
(Unit; inO_tr_istrunc Unit).1 <~> (C; ContrC).1
  symmetry; exact equiv_contr_unit.
Defined.

(** ** A few special things about the (-1)-truncation *)

Local Open Scope trunc_scope.

(** We define [merely A] to be an inhabitant of the universe [hProp] of hprops, rather than a type.  We can always treat it as a type because there is a coercion, but this means that if we need an element of [hProp] then we don't need a separate name for it. *)

Definition merely (A : Type@{i}) : HProp@{i} := Build_HProp (Tr (-1) A).

Definition hexists {X} (P : X -> Type) : HProp := merely (sig P).

Definition hor (P Q : Type) : HProp := merely (P + Q).

Declare Scope hprop_scope.
Notation "A \/ B" := (hor A B) : hprop_scope.

Definition himage {X Y} (f : X -> Y) := image (Tr (-1)) f.

(** ** Surjections *)

(** Surjections are the (-1)-connected maps, but they can be characterized more simply since an inhabited hprop is automatically contractible. *)
Notation IsSurjection := (IsConnMap (Tr (-1))).

Definition BuildIsSurjection {A B} (f : A -> B)
  : (forall b, merely (hfiber f b)) -> IsSurjection f.A, B: Type
f: A -> B
(forall b : B, merely (hfiber f b)) ->
IsConnMap (Tr (-1)) f
Proof.A, B: Type
f: A -> B
(forall b : B, merely (hfiber f b)) ->
IsConnMap (Tr (-1)) f
  intros H b; refine (contr_inhabited_hprop _ _).A, B: Type
f: A -> B
H: forall b : B, merely (hfiber f b)
b: B
Tr (-1) (hfiber f b)
  apply H.
Defined.

(** A family of types is pointwise merely inhabited if and only if the corresponding fibration is surjective. *)
Lemma iff_merely_issurjection {X : Type} (P : X -> Type)
  : (forall x, merely (P x)) <-> IsSurjection (pr1 : {x : X & P x} -> X).X: Type
P: X -> Type
(forall x : X, merely (P x)) <->
IsConnMap (Tr (-1)) (pr1 : {x : X & P x} -> X)
Proof.X: Type
P: X -> Type
(forall x : X, merely (P x)) <->
IsConnMap (Tr (-1)) (pr1 : {x : X & P x} -> X)
  refine (iff_compose _ (iff_forall_inO_mapinO_pr1 (Conn _) P)).X: Type
P: X -> Type
(forall x : X, merely (P x)) <->
(forall a : X, In (Conn (Tr (-1))) (P a))
  apply iff_functor_forall; intro a.X: Type
P: X -> Type
a: X
merely (P a) <-> In (Conn (Tr (-1))) (P a)
  symmetry; exact (iff_contr_hprop (Tr (-1) (P a))).
Defined.

Lemma equiv_merely_issurjection `{Funext} {X : Type} (P : X -> Type)
  : (forall x, merely (P x)) <~> IsSurjection (pr1 : {x : X & P x} -> X).H: Funext
X: Type
P: X -> Type
(forall x : X, merely (P x)) <~>
IsConnMap (Tr (-1)) (pr1 : {x : X & P x} -> X)
Proof. (* Can also be proved from equiv_forall_inO_mapinO_pr1. *)H: Funext
X: Type
P: X -> Type
(forall x : X, merely (P x)) <~>
IsConnMap (Tr (-1)) (pr1 : {x : X & P x} -> X)
  exact (equiv_iff_hprop_uncurried (iff_merely_issurjection P)).
Defined.

(** Surjections cancel on the right *)
Lemma cancelR_issurjection {A B C : Type} (f : A -> B) (g : B -> C)
      (isconn : IsSurjection (g o f))
  : IsSurjection g.A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
IsConnMap (Tr (-1)) g
Proof.A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
IsConnMap (Tr (-1)) g
  intro c.A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
IsConnected (Tr (-1)) (hfiber g c)
  rapply contr_inhabited_hprop.A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
Tr (-1) (hfiber g c)
  rapply (Trunc_functor _ (X:= (hfiber (g o f) c))).A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
hfiber (fun x : A => g (f x)) c -> hfiber g c
A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
Tr (-1) (hfiber (fun x : A => g (f x)) c)
  -A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
hfiber (fun x : A => g (f x)) c -> hfiber g c intros [a p].A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
a: A
p: g (f a) = c
hfiber g c
    exact (f a; p).
  -A, B, C: Type
f: A -> B
g: B -> C
isconn: IsConnMap (Tr (-1)) (g o f)
c: C
Tr (-1) (hfiber (fun x : A => g (f x)) c) apply center, isconn.
Defined.

(** Retractions are surjective. *)
Definition issurj_retr {X Y : Type} {r : X -> Y} (s : Y -> X) (h : forall y:Y, r (s y) = y)
  : IsSurjection r.X, Y: Type
r: X -> Y
s: Y -> X
h: forall y : Y, r (s y) = y
IsConnMap (Tr (-1)) r
Proof.X, Y: Type
r: X -> Y
s: Y -> X
h: forall y : Y, r (s y) = y
IsConnMap (Tr (-1)) r
  intro y.X, Y: Type
r: X -> Y
s: Y -> X
h: forall y : Y, r (s y) = y
y: Y
IsConnected (Tr (-1)) (hfiber r y)
  rapply contr_inhabited_hprop.X, Y: Type
r: X -> Y
s: Y -> X
h: forall y : Y, r (s y) = y
y: Y
Tr (-1) (hfiber r y)
  exact (tr (s y; h y)).
Defined.

(** ** Embeddings *)

(** For any point in the image of an embedding, the fibers are contractible. *)
Instance contr_hfiber_emb {A B} (a : A) (f : A -> B)
  `{IsEmbedding f}
  : Contr (hfiber f (f a)).A, B: Type
a: A
f: A -> B
IsEmbedding0: IsEmbedding f
Contr (hfiber f (f a))
Proof.A, B: Type
a: A
f: A -> B
IsEmbedding0: IsEmbedding f
Contr (hfiber f (f a))
  srapply contr_inhabited_hprop.A, B: Type
a: A
f: A -> B
IsEmbedding0: IsEmbedding f
hfiber f (f a) exact (a; idpath (f a)).
Defined.

(** Since embeddings are the (-1)-truncated maps, a map that is both a surjection and an embedding is an equivalence. *)
Definition isequiv_surj_emb {A B} (f : A -> B)
  `{IsSurjection f} `{IsEmbedding f}
  : IsEquiv f.A, B: Type
f: A -> B
IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding0: IsEmbedding f
IsEquiv f
Proof.A, B: Type
f: A -> B
IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding0: IsEmbedding f
IsEquiv f
  apply (@isequiv_conn_ino_map (Tr (-1))); assumption.
Defined.

(** As a corollary, it follows that if [i o f] is an equivalence and [i] is an embedding, then [f] is an equivalence. *)
Definition isequiv_isequiv_compose_embedding {X Y Z : Type}
  {f : X -> Y} (i : Y -> Z) `{IsEmbedding i}
  `{!IsEquiv (i o f)}
  : IsEquiv f.X, Y, Z: Type
f: X -> Y
i: Y -> Z
IsEmbedding0: IsEmbedding i
IsEquiv0: IsEquiv (i o f)
IsEquiv f
Proof.X, Y, Z: Type
f: X -> Y
i: Y -> Z
IsEmbedding0: IsEmbedding i
IsEquiv0: IsEquiv (i o f)
IsEquiv f
  rapply (cancelL_isequiv i).X, Y, Z: Type
f: X -> Y
i: Y -> Z
IsEmbedding0: IsEmbedding i
IsEquiv0: IsEquiv (i o f)
IsEquiv i
  refine (isequiv_surj_emb i).X, Y, Z: Type
f: X -> Y
i: Y -> Z
IsEmbedding0: IsEmbedding i
IsEquiv0: IsEquiv (i o f)
IsConnMap (Tr (-1)) i
  rapply (cancelR_issurjection f).
Defined.

(** If [X] is a set and [f : Y -> Z] is a surjection, then [- o f] is an embedding. *)
Definition isembedding_precompose_surjection_hset `{Funext} {X Y Z : Type}
  `{IsHSet X} (f : Y -> Z) `{IsSurjection f}
  : IsEmbedding (fun phi : Z -> X => phi o f).H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding (fun phi : Z -> X => phi o f)
Proof.H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
IsEmbedding (fun phi : Z -> X => phi o f)
  intros phi; apply istrunc_S.H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
phi: Y -> X
forall
(x : hfiber (fun (phi : Z -> X) (x : Y) => phi (f x))
       phi)
(y : hfiber
       (fun (phi : Z -> X) (x0 : Y) => phi (f x0)) phi),
Contr (x = y)
  intros g0 g1; cbn.H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
phi: Y -> X
g0, g1: hfiber (fun (phi : Z -> X) (x : Y) => phi (f x))
  phi
Contr (g0 = g1)
  rapply contr_inhabited_hprop.H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
phi: Y -> X
g0, g1: hfiber (fun (phi : Z -> X) (x : Y) => phi (f x))
  phi
g0 = g1
  apply path_sigma_hprop, equiv_path_arrow.H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
phi: Y -> X
g0, g1: hfiber (fun (phi : Z -> X) (x : Y) => phi (f x))
  phi
g0.1 == g1.1
  rapply conn_map_elim; intro y.H: Funext
X, Y, Z: Type
IsHSet0: IsHSet X
f: Y -> Z
IsSurjection0: IsConnMap (Tr (-1)) f
phi: Y -> X
g0, g1: hfiber (fun (phi : Z -> X) (x : Y) => phi (f x))
  phi
y: Y
g0.1 (f y) = g1.1 (f y)
  exact (ap10 (g0.2 @ g1.2^) y).
Defined.

(** We next prove that [paths : X -> (X -> Type)] is an embedding. This was proved by Escardó as Lemma 15 in "Injective types in univalent mathematics", but we give an argument similar to the proof of Theorem 2.25 of CORS. *)

(** This will be an inverse to [ap paths].  We'll want to show that it is an embedding, so we'll construct it out of pieces that are clearly equivalences, except for one step, [equiv_fun]. *)
Definition ap_paths_inverse `{Univalence} {X : Type} (x1 x2 : X)
  : paths x1 = paths x2 -> x1 = x2.H: Univalence
X: Type
x1, x2: X
paths x1 = paths x2 -> x1 = x2
Proof.H: Univalence
X: Type
x1, x2: X
paths x1 = paths x2 -> x1 = x2
  refine (_ o @equiv_ap10 _ X Type (paths x1) (paths x2)).H: Univalence
X: Type
x1, x2: X
paths x1 == paths x2 -> x1 = x2
  refine (_ o equiv_functor_forall_id (fun y => equiv_equiv_path (x1 = y) (x2 = y))).H: Univalence
X: Type
x1, x2: X
(forall a : X, x1 = a <~> x2 = a) -> x1 = x2
  refine (_ o functor_forall_id (fun y => @equiv_fun (x1 = y) (x2 = y))).H: Univalence
X: Type
x1, x2: X
(forall a : X, x1 = a -> x2 = a) -> x1 = x2
  refine (_ o (equiv_paths_ind x1 (fun y p => x2 = y))^-1%equiv).H: Univalence
X: Type
x1, x2: X
x2 = x1 -> x1 = x2
  exact (equiv_path_inverse x2 x1).
Defined.

(** A Yoneda-like embedding for path types: [paths : X -> (X -> Type)] is an embedding. *)
Definition isembedding_paths `{Univalence} {X : Type@{u}} : IsEmbedding (@paths X).H: Univalence
X: Type
IsEmbedding paths
Proof.H: Univalence
X: Type
IsEmbedding paths
  (* To show that [paths] is an embedding, it suffices to show that [ap paths : x1 = x2 -> (paths x1) = (paths x2)] is an equivalence. *)
  snapply isembedding_isequiv_ap.H: Univalence
X: Type
forall x y : X, IsEquiv (ap paths)
  intros x1 x2.H: Univalence
X: Type
x1, x2: X
IsEquiv (ap paths)
  (* And for that, it suffices to show that [i o (ap paths)] is an equivalence for a well-chosen embedding [i]. *)
  snapply (isequiv_isequiv_compose_embedding (ap_paths_inverse x1 x2)).H: Univalence
X: Type
x1, x2: X
IsEmbedding (ap_paths_inverse x1 x2)
H: Univalence
X: Type
x1, x2: X
IsEquiv (ap_paths_inverse x1 x2 o ap paths)
  - (* [ap_paths_inverse x1 x2] is an embedding since it is a composite of four equivalences and one embedding.  We can group these into three parts. *)H: Univalence
X: Type
x1, x2: X
IsEmbedding (ap_paths_inverse x1 x2)
    unfold ap_paths_inverse.H: Univalence
X: Type
x1, x2: X
IsEmbedding
  (fun x : paths x1 = paths x2 =>
   equiv_path_inverse x2 x1
     ((equiv_paths_ind x1
         (fun (y : X) (_ : x1 = y) => x2 = y))^-1%equiv
        (functor_forall_id (fun y : X => equiv_fun)
           (equiv_functor_forall_id
              (fun y : X =>
               equiv_equiv_path (x1 = y) (x2 = y))
              (equiv_ap10 (paths x1) (paths x2) x)))))
    nrefine (mapinO_compose (O:=Tr (-1)) _ (equiv_path_inverse x2 x1 oE _)).H: Univalence
X: Type
x1, x2: X
MapIn (Tr (-1))
  (fun x : paths x1 = paths x2 =>
   functor_forall_id (fun y : X => equiv_fun)
     (equiv_functor_forall_id
        (fun y : X =>
         equiv_equiv_path (x1 = y) (x2 = y))
        (equiv_ap10 (paths x1) (paths x2) x)))
H: Univalence
X: Type
x1, x2: X
MapIn (Tr (-1))
  (equiv_path_inverse x2 x1
   oE (equiv_paths_ind x1
         (fun (y : X) (_ : x1 = y) => x2 = y))^-1)
    2: exact _. (* The second part is an equivalence, so it's an embedding. *)H: Univalence
X: Type
x1, x2: X
MapIn (Tr (-1))
  (fun x : paths x1 = paths x2 =>
   functor_forall_id (fun y : X => equiv_fun)
     (equiv_functor_forall_id
        (fun y : X =>
         equiv_equiv_path (x1 = y) (x2 = y))
        (equiv_ap10 (paths x1) (paths x2) x)))
    nrefine (mapinO_compose _ (functor_forall_id _)).H: Univalence
X: Type
x1, x2: X
MapIn (Tr (-1))
  (fun x : paths x1 = paths x2 =>
   equiv_functor_forall_id
     (fun y : X => equiv_equiv_path (x1 = y) (x2 = y))
     (equiv_ap10 (paths x1) (paths x2) x))
H: Univalence
X: Type
x1, x2: X
MapIn (Tr (-1))
  (functor_forall_id (fun y : X => equiv_fun))
    1: exact _. (* The first part is an equivalence, so it's an embedding. *)H: Univalence
X: Type
x1, x2: X
MapIn (Tr (-1))
  (functor_forall_id (fun y : X => equiv_fun))
    rapply mapinO_functor_forall_id.H: Univalence
X: Type
x1, x2: X
forall a : X, MapIn (Tr (-1)) equiv_fun
    intro y.H: Univalence
X: Type
x1, x2, y: X
MapIn (Tr (-1)) equiv_fun
    exact isembedding_equiv_fun.
  - (* The composite is an equivalence because it is homotopic to the identity. *)H: Univalence
X: Type
x1, x2: X
IsEquiv (ap_paths_inverse x1 x2 o ap paths)
    simpl.H: Univalence
X: Type
x1, x2: X
IsEquiv
  (fun x : x1 = x2 =>
   ap_paths_inverse x1 x2 (ap paths x))
    srapply (isequiv_homotopic idmap).H: Univalence
X: Type
x1, x2: X
idmap ==
(fun x : x1 = x2 =>
 ap_paths_inverse x1 x2 (ap paths x))
    intros [].H: Univalence
X: Type
x1, x2: X
1 = ap_paths_inverse x1 x1 (ap paths 1)
    reflexivity.
Defined.

(** ** Iterated truncations *)

(** Compare to [O_leq_Tr] and [O_strong_leq_Tr] in SeparatedTrunc.v. *)
Definition O_leq_Tr_leq {n m : trunc_index} (Hmn : m <= n)
  : O_leq (Tr m) (Tr n).n, m: trunc_index
Hmn: m <= n
O_leq (Tr m) (Tr n)
Proof.n, m: trunc_index
Hmn: m <= n
O_leq (Tr m) (Tr n)
  intros A; rapply istrunc_leq.
Defined.

Definition Trunc_min n m X : Tr (trunc_index_min n m) X <~> Tr n (Tr m X).n, m: trunc_index
X: Type
Tr (trunc_index_min n m) X <~> Tr n (Tr m X)
Proof.n, m: trunc_index
X: Type
Tr (trunc_index_min n m) X <~> Tr n (Tr m X)
  destruct (trunc_index_min_path n m) as [p|q].n, m: trunc_index
X: Type
p: trunc_index_min n m = n
Tr (trunc_index_min n m) X <~> Tr n (Tr m X)
n, m: trunc_index
X: Type
q: trunc_index_min n m = m
Tr (trunc_index_min n m) X <~> Tr n (Tr m X)
  +n, m: trunc_index
X: Type
p: trunc_index_min n m = n
Tr (trunc_index_min n m) X <~> Tr n (Tr m X) assert (l := trunc_index_min_leq_right n m).n, m: trunc_index
X: Type
p: trunc_index_min n m = n
l: trunc_index_min n m <= m
Tr (trunc_index_min n m) X <~> Tr n (Tr m X)
    destruct p^; clear p.n, m: trunc_index
X: Type
l: n <= m
Tr n X <~> Tr n (Tr m X)
    snapply (Build_Equiv _ _ (Trunc_functor _ tr)).n, m: trunc_index
X: Type
l: n <= m
IsEquiv (Trunc_functor n tr)
    napply O_inverts_conn_map.n, m: trunc_index
X: Type
l: n <= m
IsConnMap (Tr n) tr
    rapply (conn_map_O_leq _ (Tr m)).n, m: trunc_index
X: Type
l: n <= m
O_leq (Tr n) (Tr m)
    rapply O_leq_Tr_leq.
  +n, m: trunc_index
X: Type
q: trunc_index_min n m = m
Tr (trunc_index_min n m) X <~> Tr n (Tr m X) assert (l := trunc_index_min_leq_left n m).n, m: trunc_index
X: Type
q: trunc_index_min n m = m
l: trunc_index_min n m <= n
Tr (trunc_index_min n m) X <~> Tr n (Tr m X)
    destruct q^; clear q.n, m: trunc_index
X: Type
l: m <= n
Tr m X <~> Tr n (Tr m X)
    srapply equiv_tr.n, m: trunc_index
X: Type
l: m <= n
IsTrunc n (Tr m X)
    srapply istrunc_leq.
Defined.

Definition Trunc_swap n m X : Tr n (Tr m X) <~> Tr m (Tr n X).n, m: trunc_index
X: Type
Tr n (Tr m X) <~> Tr m (Tr n X)
Proof.n, m: trunc_index
X: Type
Tr n (Tr m X) <~> Tr m (Tr n X)
  refine (Trunc_min m n _ oE equiv_transport (fun k => Tr k _) _ oE (Trunc_min n m _)^-1).n, m: trunc_index
X: Type
trunc_index_min n m = trunc_index_min m n
  apply trunc_index_min_swap.
Defined.

(** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)