(* -*- mode: coq; mode: visual-line -*-  *)
(** * Connectedness *)
Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.

Require Import Extensions.
Require Import Factorization.
Require Export Modalities.Modality.        (* [Export] since the actual definitions of connectedness appear there, in the generality of a modality. *)
Require Import Modalities.Descent.
Require Import Truncations.Core Truncations.SeparatedTrunc.

(** This reduces universe variables in [conn_pointed_type] and [conn_point_elim], which refer to [Unit]. *)
Local Set Universe Minimization ToSet.

Local Open Scope path_scope.
Local Open Scope trunc_scope.

(** There is a slight controversy of indexing for connectedness — in particular, how the indexing for maps shoud relate to the indexing for types.  One may reasonably take the connectedness of a map to correspond either to that of its *fibers*, or of its *cofiber*; these differ by 1.  The traditional topological indexing uses the cofiber.  We use the fiber, as does Lurie in [HTT]; but we choose to agree with the traditional indexing on types, while Lurie agrees with it on maps.

Currently, the translation is therefore as follows:

       HoTT              Traditional       Lurie

Map    (n-1)-connected   n-connected       n-connective
Type   n-connected       n-connected       (n+1)-connective

A handy benchmark: under our indexing, the map [S1 -> 1] is 0-connected but not 1-connected, while the map [1 -> S1] is (–1)–connected but not 0-connected.


One reason for our choice is that this way, the n-truncated and n-connected maps are the modal and modally-connected maps for the n-truncation modality.  Many of the basic lemmas about connected maps are in fact true for any modality, and can be found in [Modality.v].  Thus, here we consider mainly properties that involve the interaction of connectedness at different truncation levels. *)

(** ** Truncatedness of the type of extensions *)

(** A key lemma on the interaction between connectedness and truncatedness: suppose one is trying to extend along an n-connected map, into a k-truncated family of types (k ≥ n).  Then the space of possible extensions is (k–n–2)-truncated.

(Mnemonic for the indexing: think of the base case, where k=n; then we know we can eliminate, so the space of extensions is contractible.)

This lemma is most useful via corollaries like the wedge-inclusion, the wiggly wedge, and their n-ary generalizations. *)
Lemma istrunc_extension_along_conn `{Funext} {m n : trunc_index}
  {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
  (P : B -> Type) {HP : forall b:B, IsTrunc (m +2+ n) (P b)}
  (d : forall a:A, P (f a))
  : IsTrunc m (ExtensionAlong f P d).
H: Funext
m, n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
P: B -> Type
HP: forall b : B, IsTrunc (m +2+ n) (P b)
d: forall a : A, P (f a)
IsTrunc m (ExtensionAlong f P d)
Proof.
H: Funext
m, n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
P: B -> Type
HP: forall b : B, IsTrunc (m +2+ n) (P b)
d: forall a : A, P (f a)
IsTrunc m (ExtensionAlong f P d)
  revert P HP d.
H: Funext
m, n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
forall P : B -> Type,
(forall b : B, IsTrunc (m +2+ n) (P b)) ->
forall d : forall a : A, P (f a),
IsTrunc m (ExtensionAlong f P d) simple_induction m m' IH; intros P HP d; simpl in *.
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
P: B -> Type
HP: forall b : B, IsTrunc n (P b)
d: forall a : A, P (f a)
Contr (ExtensionAlong f P d)
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
m': trunc_index
IH: forall P : B -> Type,
(forall b : B, IsTrunc (m' +2+ n) (P b)) ->
forall d : forall a : A, P (f a),
IsTrunc m' (ExtensionAlong f P d)
P: B -> Type
HP: forall b : B, IsTrunc (m' +2+ n).+1 (P b)
d: forall a : A, P (f a)
IsTrunc m'.+1 (ExtensionAlong f P d)
  (* m = –2 *)
  -
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
P: B -> Type
HP: forall b : B, IsTrunc n (P b)
d: forall a : A, P (f a)
Contr (ExtensionAlong f P d) apply (Build_Contr _ (extension_conn_map_elim n f P d)).
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
P: B -> Type
HP: forall b : B, IsTrunc n (P b)
d: forall a : A, P (f a)
forall y : ExtensionAlong f P d,
extension_conn_map_elim (Tr n) f P d = y
    intros y.
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
P: B -> Type
HP: forall b : B, IsTrunc n (P b)
d: forall a : A, P (f a)
y: ExtensionAlong f P d
extension_conn_map_elim (Tr n) f P d = y apply (allpath_extension_conn_map n); assumption.
    (* m = S m' *)
  -
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
m': trunc_index
IH: forall P : B -> Type,
(forall b : B, IsTrunc (m' +2+ n) (P b)) ->
forall d : forall a : A, P (f a),
IsTrunc m' (ExtensionAlong f P d)
P: B -> Type
HP: forall b : B, IsTrunc (m' +2+ n).+1 (P b)
d: forall a : A, P (f a)
IsTrunc m'.+1 (ExtensionAlong f P d) apply istrunc_S.
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
m': trunc_index
IH: forall P : B -> Type,
(forall b : B, IsTrunc (m' +2+ n) (P b)) ->
forall d : forall a : A, P (f a),
IsTrunc m' (ExtensionAlong f P d)
P: B -> Type
HP: forall b : B, IsTrunc (m' +2+ n).+1 (P b)
d: forall a : A, P (f a)
forall x y : ExtensionAlong f P d, IsTrunc m' (x = y)
    intros e e'.
H: Funext
n: trunc_index
A, B: Type
f: A -> B
H0: IsConnMap (Tr n) f
m': trunc_index
IH: forall P : B -> Type,
(forall b : B, IsTrunc (m' +2+ n) (P b)) ->
forall d : forall a : A, P (f a),
IsTrunc m' (ExtensionAlong f P d)
P: B -> Type
HP: forall b : B, IsTrunc (m' +2+ n).+1 (P b)
d: forall a : A, P (f a)
e, e': ExtensionAlong f P d
IsTrunc m' (e = e') refine (istrunc_isequiv_istrunc _ (path_extension e e')).
  (* magically infers: paths in extensions = extensions into paths, which by induction is m'-truncated. *)
Defined.

(** ** Connectedness of path spaces *)

Global Instance isconnected_paths `{Univalence} {n A}
       `{IsConnected n.+1 A} (x y : A)
  : IsConnected n (x = y).
H: Univalence
n: trunc_index
A: Type
H0: IsConnected (Tr n.+1) A
x, y: A
IsConnected (Tr n) (x = y)
Proof.
H: Univalence
n: trunc_index
A: Type
H0: IsConnected (Tr n.+1) A
x, y: A
IsConnected (Tr n) (x = y)
  refine (contr_equiv' _ (equiv_path_Tr x y)^-1).
Defined.

(** ** Connectivity of pointed types *)

(** The connectivity of a pointed type and (the inclusion of) its point are intimately connected. *)

(** We can't make both of these [Instance]s, as that would result in infinite loops. *)

Global Instance conn_pointed_type@{u} {n : trunc_index} {A : Type@{u}} (a0:A)
  `{IsConnMap n _ _ (unit_name a0)}
  : IsConnected n.+1 A | 1000.
n: trunc_index
A: Type
a0: A
H: IsConnMap (Tr n) (unit_name a0)
IsConnected (Tr n.+1) A
Proof.
n: trunc_index
A: Type
a0: A
H: IsConnMap (Tr n) (unit_name a0)
IsConnected (Tr n.+1) A
  apply isconnected_conn_map_to_unit.
n: trunc_index
A: Type
a0: A
H: IsConnMap (Tr n) (unit_name a0)
IsConnMap (Tr n.+1) (const_tt A)
  apply (OO_cancelR_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
Defined.

Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type} (a0:A)
  `{IsConnected n.+1 A}
  : IsConnMap n (unit_name a0).
H: Univalence
n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr n.+1) A
IsConnMap (Tr n) (unit_name a0)
Proof.
H: Univalence
n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr n.+1) A
IsConnMap (Tr n) (unit_name a0)
  rapply (OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
H: Univalence
n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr n.+1) A
Tr n <<< Tr n.+1
  apply O_lex_leq_Tr.
Defined.

#[export] Hint Immediate conn_point_incl : typeclass_instances.

(** Note that [OO_cancelR_conn_map] and [OO_cancelL_conn_map] (Proposition 2.31 of CORS) generalize the above statements to 2/3 of a 2-out-of-3 property for connected maps, for any reflective subuniverse and its subuniverse of separated types.  If useful, we could specialize that more general form explicitly to truncations. *)

(** To prove an [n]-truncated predicate on an (n+1)-connected, pointed type, it's enough to prove it for the basepoint. *)
Definition conn_point_elim `{Univalence} (n : trunc_index) {A : pType@{u}} `{IsConnected n.+1 A}
           (P : A -> Type@{u}) `{forall a, IsTrunc n (P a)} (p0 : P (point A))
  : forall a, P a.
H: Univalence
n: trunc_index
A: pType
H0: IsConnected (Tr n.+1) A
P: A -> Type
H1: forall a : A, IsTrunc n (P a)
p0: P (point A)
forall a : A, P a
Proof.
H: Univalence
n: trunc_index
A: pType
H0: IsConnected (Tr n.+1) A
P: A -> Type
H1: forall a : A, IsTrunc n (P a)
p0: P (point A)
forall a : A, P a
  (** This follows from [conn_point_incl] and [conn_map_elim], but we give a direct proof. *)
  intro a.
H: Univalence
n: trunc_index
A: pType
H0: IsConnected (Tr n.+1) A
P: A -> Type
H1: forall a : A, IsTrunc n (P a)
p0: P (point A)
a: A
P a
  (** Since [A] is [n+1]-connected, [a0 = a] is [n]-connected, which means that [Tr n (a0 = a)] has an element. *)
  pose proof (p := center (Tr n ((point A) = a))).
H: Univalence
n: trunc_index
A: pType
H0: IsConnected (Tr n.+1) A
P: A -> Type
H1: forall a : A, IsTrunc n (P a)
p0: P (point A)
a: A
p: Tr n (point A = a)
P a
  strip_truncations.
H: Univalence
n: trunc_index
A: pType
H0: IsConnected (Tr n.+1) A
P: A -> Type
H1: forall a : A, IsTrunc n (P a)
p0: P (point A)
a: A
p: point A = a
P a
  exact (p # p0).
Defined.

(** ** Decreasing connectedness *)

(** An [n.+1]-connected type is also [n]-connected.  This obviously can't be an [Instance]! *)
Definition isconnected_pred n A `{IsConnected n.+1 A}
  : IsConnected n A.
n: trunc_index
A: Type
H: IsConnected (Tr n.+1) A
IsConnected (Tr n) A
Proof.
n: trunc_index
A: Type
H: IsConnected (Tr n.+1) A
IsConnected (Tr n) A
  apply isconnected_from_elim; intros C ? f.
n: trunc_index
A: Type
H: IsConnected (Tr n.+1) A
C: Type
H0: In (Tr n) C
f: A -> C
NullHomotopy.NullHomotopy f
  refine (isconnected_elim n.+1 C f).
Defined.

(** A [k]-connected type is [n]-connected, when [k >= n].  We constrain [k] by making it of the form [n +2+ m], which makes the induction go through smoothly. *)
Definition isconnected_pred_add n m A `{H : IsConnected (n +2+ m) A}
  : IsConnected m A.
n, m: trunc_index
A: Type
H: IsConnected (Tr (n +2+ m)) A
IsConnected (Tr m) A
Proof.
n, m: trunc_index
A: Type
H: IsConnected (Tr (n +2+ m)) A
IsConnected (Tr m) A
  induction n.
m: trunc_index
A: Type
H: IsConnected (Tr (-2 +2+ m)) A
IsConnected (Tr m) A
n, m: trunc_index
A: Type
H: IsConnected (Tr (n.+1 +2+ m)) A
IHn: IsConnected (Tr (n +2+ m)) A -> IsConnected (Tr m) A
IsConnected (Tr m) A
  1: assumption.
n, m: trunc_index
A: Type
H: IsConnected (Tr (n.+1 +2+ m)) A
IHn: IsConnected (Tr (n +2+ m)) A -> IsConnected (Tr m) A
IsConnected (Tr m) A
  apply IHn.
n, m: trunc_index
A: Type
H: IsConnected (Tr (n.+1 +2+ m)) A
IHn: IsConnected (Tr (n +2+ m)) A -> IsConnected (Tr m) A
IsConnected (Tr (n +2+ m)) A
  apply isconnected_pred.
n, m: trunc_index
A: Type
H: IsConnected (Tr (n.+1 +2+ m)) A
IHn: IsConnected (Tr (n +2+ m)) A -> IsConnected (Tr m) A
IsConnected (Tr (n +2+ m).+1) A
  assumption.
Defined.

(** A version with the order of summands swapped, which is sometimes handy, e.g. in the next two results. *)
Definition isconnected_pred_add' n m A `{H : IsConnected (m +2+ n) A}
  : IsConnected m A.
n, m: trunc_index
A: Type
H: IsConnected (Tr (m +2+ n)) A
IsConnected (Tr m) A
Proof.
n, m: trunc_index
A: Type
H: IsConnected (Tr (m +2+ n)) A
IsConnected (Tr m) A
  apply (isconnected_pred_add n m).
n, m: trunc_index
A: Type
H: IsConnected (Tr (m +2+ n)) A
IsConnected (Tr (n +2+ m)) A
  destruct (trunc_index_add_comm m n); assumption.
Defined.

(** It follows that an [n.+1]-connected type is also [-1]-connected. *)
Definition merely_isconnected n A `{IsConnected n.+1 A}
  : merely A
  := @center _ (isconnected_pred_add' n (-1) A).

(** And that an [n.+2]-connected type is [0]-connected. *)
Definition is0connected_isconnected (n : trunc_index) A `{IsConnected n.+2 A}
  : IsConnected 0 A
  := isconnected_pred_add' n 0 A.

Definition isconnmap_pred_add n m A B (f : A -> B) `{IsConnMap (n +2+ m) _ _ f}
  : IsConnMap m f.
n, m: trunc_index
A, B: Type
f: A -> B
H: IsConnMap (Tr (n +2+ m)) f
IsConnMap (Tr m) f
Proof.
n, m: trunc_index
A, B: Type
f: A -> B
H: IsConnMap (Tr (n +2+ m)) f
IsConnMap (Tr m) f
  intro b.
n, m: trunc_index
A, B: Type
f: A -> B
H: IsConnMap (Tr (n +2+ m)) f
b: B
IsConnected (Tr m) (hfiber f b)
  exact (isconnected_pred_add n m _).
Defined.

(** ** 0-connectedness *)

(** To be 0-connected is the same as to be (-1)-connected and that any two points are merely equal.  TODO: This should also be generalized to separated subuniverses (CORS Remark 2.35).  *)
Definition merely_path_is0connected `{Univalence}
           (A : Type) `{IsConnected 0 A} (x y : A)
  : merely (x = y).
H: Univalence
A: Type
H0: IsConnected (Tr 0) A
x, y: A
merely (x = y)
Proof.
H: Univalence
A: Type
H0: IsConnected (Tr 0) A
x, y: A
merely (x = y)
  (** This follows immediately from [isconnected_paths] above. *)
  rapply center.
Defined.

Definition is0connected_merely_allpath `{Univalence}
           (A : Type) `{merely A}
           (p : forall (x y:A), merely (x = y))
  : IsConnected 0 A.
H: Univalence
A: Type
merely0: merely A
p: forall x y : A, merely (x = y)
IsConnected (Tr 0) A
Proof.
H: Univalence
A: Type
merely0: merely A
p: forall x y : A, merely (x = y)
IsConnected (Tr 0) A
  strip_truncations.
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0: A
IsConnected (Tr 0) A
  apply (contr_inhabited_hprop).
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0: A
IsHProp (Tr 0 A)
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0: A
Tr 0 A
  -
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0: A
IsHProp (Tr 0 A) apply hprop_allpath; intros z w.
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0: A
z, w: Tr 0 A
z = w
    strip_truncations.
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0, w, z: A
tr z = tr w
    exact (equiv_path_Tr z w (p z w)).
  -
H: Univalence
A: Type
p: forall x y : A, merely (x = y)
merely0: A
Tr 0 A apply tr; assumption.
Defined.

(** The path component of a point [x : X] is connected. *)
Global Instance is0connected_component {X : Type} (x : X)
  : IsConnected 0 { z : X & merely (z = x) }.
X: Type
x: X
IsConnected (Tr 0) {z : X & merely (z = x)}
Proof.
X: Type
x: X
IsConnected (Tr 0) {z : X & merely (z = x)}
  apply (Build_Contr _ (tr (x; tr idpath))).
X: Type
x: X
forall y : Trunc 0 {z : X & merely (z = x)},
tr (x; tr 1) = y
  rapply Trunc_ind; intros [Z p].
X: Type
x, Z: X
p: merely (Z = x)
tr (x; tr 1) = tr (Z; p)
  strip_truncations.
X: Type
x, Z: X
p: Z = x
tr (x; tr 1) = tr (Z; tr p)
  apply (ap tr).
X: Type
x, Z: X
p: Z = x
(x; tr 1) = (Z; tr p)
  rapply path_sigma_hprop.
X: Type
x, Z: X
p: Z = x
(x; tr 1).1 = (Z; tr p).1
  exact p^.
Defined.

(** Any two points in a path component are merely equal.  This follows from [merely_path_is0connected], but this proof doesn't need univalence. *)
Definition merely_path_component {X : Type} {x : X}
  (z1 z2 : { z : X & merely (z = x) })
  : merely (z1 = z2).
X: Type
x: X
z1, z2: {z : X & merely (z = x)}
merely (z1 = z2)
Proof.
X: Type
x: X
z1, z2: {z : X & merely (z = x)}
merely (z1 = z2)
  destruct z1 as [z1 p1], z2 as [z2 p2].
X: Type
x, z1: X
p1: merely (z1 = x)
z2: X
p2: merely (z2 = x)
merely ((z1; p1) = (z2; p2))
  strip_truncations.
X: Type
x, z1, z2: X
p2: z2 = x
p1: z1 = x
merely ((z1; tr p1) = (z2; tr p2))
  apply tr.
X: Type
x, z1, z2: X
p2: z2 = x
p1: z1 = x
(z1; tr p1) = (z2; tr p2)
  apply path_sigma_hprop; cbn.
X: Type
x, z1, z2: X
p2: z2 = x
p1: z1 = x
z1 = z2
  exact (p1 @ p2^).
Defined.

(** The path component of a point [x : X] is equivalent to the image of the constant map [Unit -> X] at [x]. *)
Definition equiv_component_image_unit {X : Type} (x : X)
  : { z : X & merely (z = x) } <~> image (Tr (-1)) (unit_name x).
X: Type
x: X
{z : X & merely (z = x)} <~>
image (Tr (-1)) (unit_name x)
Proof.
X: Type
x: X
{z : X & merely (z = x)} <~>
image (Tr (-1)) (unit_name x)
  unfold image; simpl.
X: Type
x: X
{z : X & Tr (-1) (z = x)} <~>
{b : X & Tr (-1) (hfiber (unit_name x) b)}
  apply equiv_functor_sigma_id; intros z; simpl.
X: Type
x, z: X
Tr (-1) (z = x) <~> Tr (-1) (hfiber (unit_name x) z)
  apply Trunc_functor_equiv; unfold hfiber.
X: Type
x, z: X
z = x <~> {_ : Unit & x = z}
  refine ((equiv_contr_sigma _)^-1 oE _).
X: Type
x, z: X
z = x <~> x = z
  apply equiv_path_inverse.
Defined.

(** 0-connected types are indecomposable *)
Global Instance indecomposable_0connected `{Univalence}
       (X : Type) `{IsConnected 0 X}
  : Indecomposable X.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
Indecomposable X
Proof.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
Indecomposable X
  assert (IsConnected (-1) X) by refine (isconnected_pred (-1) X).
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
Indecomposable X
  constructor.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
forall (A B : Type) (f : X -> A + B),
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
~~ X
  -
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
forall (A B : Type) (f : X -> A + B),
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x)) intros A B f.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
    assert (z := center (merely X) : merely X); generalize z.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
merely X ->
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
    refine (Trunc_rec _).
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
IsHProp
  ((forall x : X, is_inl (f x)) +
   (forall x : X, is_inr (f x)))
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
X ->
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
    +
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
IsHProp
  ((forall x : X, is_inl (f x)) +
   (forall x : X, is_inr (f x))) apply ishprop_sum; try exact _.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
(forall x : X, is_inl (f x)) ->
(forall x : X, is_inr (f x)) -> Empty
      intros l r.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
l: forall x : X, is_inl (f x)
r: forall x : X, is_inr (f x)
Empty strip_truncations.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
l: forall x : X, is_inl (f x)
r: forall x : X, is_inr (f x)
z: X
Empty
      exact (not_is_inl_and_inr' (f z) (l z) (r z)).
    +
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
X ->
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x)) intros x.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
x: X
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
      remember (f x) as y eqn:p.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
x: X
y: A + B
p: f x = y
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
      destruct y as [a|b]; [ left | right ]; intros x'.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
x: X
a: A
p: f x = inl a
x': X
is_inl (f x')
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
z: merely X
x: X
b: B
p: f x = inr b
x': X
is_inr (f x')
      all:assert (q := merely_path_is0connected X x x');
        strip_truncations.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
x: X
a: A
p: f x = inl a
x': X
q: x = x'
z: X
is_inl (f x')
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
x: X
b: B
p: f x = inr b
x': X
q: x = x'
z: X
is_inr (f x')
      all:refine (transport _ (ap f q) _).
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
x: X
a: A
p: f x = inl a
x': X
q: x = x'
z: X
is_inl (f x)
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
A, B: Type
f: X -> A + B
x: X
b: B
p: f x = inr b
x': X
q: x = x'
z: X
is_inr (f x)
      all:exact (transport _ p^ tt).
  -
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
~~ X intros nx.
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
nx: ~ X
Empty
    apply (Trunc_rec (n := -1) nx).
H: Univalence
X: Type
H0: IsConnected (Tr 0) X
X0: IsConnected (Tr (-1)) X
nx: ~ X
Trunc (-1) X
    exact (center (merely X)).
Defined.

(* Truncation preserves connectedness. Note that this is for different levels. *)
Global Instance isconnected_trunc {X : Type} (n m : trunc_index) `{IsConnected n X}
  : IsConnected n (Tr m X).
X: Type
n, m: trunc_index
H: IsConnected (Tr n) X
IsConnected (Tr n) (Tr m X)
Proof.
X: Type
n, m: trunc_index
H: IsConnected (Tr n) X
IsConnected (Tr n) (Tr m X)
  unfold IsConnected.
X: Type
n, m: trunc_index
H: IsConnected (Tr n) X
Contr (Tr n (Tr m X))
  srapply (contr_equiv' _ (Trunc_swap n m X)^-1).
Defined.

Section Wedge_Incl_Conn.

(** ** Connectivity of the wedge into the product.

A very useful form of the key lemma [istrunc_extension_along_conn] is the connectivity of the wedge into the product, for a pair of pointed spaces.  In fact this can be formulated without mentioning the wedge per se (so, without requiring HIT’s), since the statement only needs to talk about maps out of the wedge.

Once again, we believe that the type of the conclusion is an hprop (though we do not prove it) — essentially because it is wrapping up an elimination principle and its corresponding computation rule — and so we make the proof of this result opaque. *)

Context `{Univalence}
  {m n : trunc_index}
  {A : Type} (a0 : A) `{IsConnected m.+1 A}
  {B : Type} (b0 : B) `{IsConnected n.+1 B}
  (P : A -> B -> Type) {HP : forall a b, IsTrunc (m +2+ n) (P a b)}
  (f_a0 : forall b:B, P a0 b)
  (f_b0 : forall a:A, P a b0)
  (f_a0b0 : f_a0 b0 = f_b0 a0).

Corollary isconn_wedge_incl
  : { f : forall a b, P a b
  & { e_a0 : forall b, f a0 b = f_a0 b
  & { e_b0 : forall a, f a b0 = f_b0 a
  & e_b0 a0 = (e_a0 b0) @ f_a0b0 }}}.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
{f : forall (a : A) (b : B), P a b &
{e_a0 : forall b : B, f a0 b = f_a0 b &
{e_b0 : forall a : A, f a b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}}
Proof.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
{f : forall (a : A) (b : B), P a b &
{e_a0 : forall b : B, f a0 b = f_a0 b &
{e_b0 : forall a : A, f a b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}}
  assert (goal_as_extension :
    ExtensionAlong (unit_name a0)
      (fun a => ExtensionAlong (unit_name b0) (P a) (unit_name (f_b0 a)))
      (unit_name (f_a0 ; (unit_name f_a0b0)))).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
ExtensionAlong (unit_name a0)
  (fun a : A =>
   ExtensionAlong (unit_name b0) (P a)
     (unit_name (f_b0 a)))
  (unit_name (f_a0; unit_name f_a0b0))
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
goal_as_extension: ExtensionAlong (unit_name a0)
  (fun a : A =>
   ExtensionAlong (unit_name b0)
     (P a) (unit_name (f_b0 a)))
  (fun x : Unit =>
   (f_a0; unit_name f_a0b0))
{f : forall (a : A) (b : B), P a b &
{e_a0 : forall b : B, f a0 b = f_a0 b &
{e_b0 : forall a : A, f a b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}}
  -
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
ExtensionAlong (unit_name a0)
  (fun a : A =>
   ExtensionAlong (unit_name b0) (P a)
     (unit_name (f_b0 a)))
  (unit_name (f_a0; unit_name f_a0b0)) apply (extension_conn_map_elim m).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
IsConnMap (Tr m) (unit_name a0)
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
forall b : A,
In (Tr m)
  (ExtensionAlong (unit_name b0) 
     (P b) (unit_name (f_b0 b)))
    +
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
IsConnMap (Tr m) (unit_name a0) apply (conn_point_incl a0).
    +
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
forall b : A,
In (Tr m)
  (ExtensionAlong (unit_name b0) (P b)
     (unit_name (f_b0 b))) intros a.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
a: A
In (Tr m)
  (ExtensionAlong (unit_name b0) (P a)
     (unit_name (f_b0 a)))
      apply (istrunc_extension_along_conn (n := n)).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
a: A
IsConnMap (Tr n) (unit_name b0)
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
a: A
forall b : B, IsTrunc (m +2+ n) (P a b)
      *
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
a: A
IsConnMap (Tr n) (unit_name b0) apply (conn_point_incl b0).
      *
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
a: A
forall b : B, IsTrunc (m +2+ n) (P a b) apply HP.
  -
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
goal_as_extension: ExtensionAlong (unit_name a0)
  (fun a : A =>
   ExtensionAlong (unit_name b0)
     (P a) (unit_name (f_b0 a)))
  (fun x : Unit =>
   (f_a0; unit_name f_a0b0))
{f : forall (a : A) (b : B), P a b &
{e_a0 : forall b : B, f a0 b = f_a0 b &
{e_b0 : forall a : A, f a b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}} destruct goal_as_extension as [f_eb name_ea_eab].
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
name_ea_eab: Unit ->
f_eb a0 = (f_a0; unit_name f_a0b0)
{f : forall (a : A) (b : B), P a b &
{e_a0 : forall b : B, f a0 b = f_a0 b &
{e_b0 : forall a : A, f a b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}}
    assert (ea_eab := name_ea_eab tt); clear name_ea_eab.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
{f : forall (a : A) (b : B), P a b &
{e_a0 : forall b : B, f a0 b = f_a0 b &
{e_b0 : forall a : A, f a b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}}
    exists (fun a => pr1 (f_eb a)).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
{e_a0 : forall b : B, (f_eb a0).1 b = f_a0 b &
{e_b0 : forall a : A, (f_eb a).1 b0 = f_b0 a &
e_b0 a0 = e_a0 b0 @ f_a0b0}}
    exists (fun b => apD10 (ea_eab ..1) b).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
{e_b0 : forall a : A, (f_eb a).1 b0 = f_b0 a &
e_b0 a0 = apD10 ea_eab ..1 b0 @ f_a0b0}
    exists (fun a => pr2 (f_eb a) tt).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
(f_eb a0).2 tt = apD10 ea_eab ..1 b0 @ f_a0b0
    (* The last component is essentially (g' ..2), wrapped in a bit of path-algebra. *)
    apply moveL_Mp.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
(apD10 ea_eab ..1 b0)^ @ (f_eb a0).2 tt = f_a0b0
    apply (concatR (apD10 (ea_eab ..2) tt)).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
(apD10 ea_eab ..1 b0)^ @ (f_eb a0).2 tt =
transport
  (fun s : forall y : B, P a0 y =>
   Unit -> s b0 = f_b0 a0) ea_eab ..1 (f_eb a0).2 tt
    set (ea := ea_eab ..1).
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
ea:= ea_eab ..1: (f_eb a0).1 = (f_a0; unit_name f_a0b0).1
(apD10 ea b0)^ @ (f_eb a0).2 tt =
transport
  (fun s : forall y : B, P a0 y =>
   Unit -> s b0 = f_b0 a0) ea (f_eb a0).2 tt generalize ea; simpl.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea_eab: f_eb a0 = (f_a0; unit_name f_a0b0)
ea:= ea_eab ..1: (f_eb a0).1 = (f_a0; unit_name f_a0b0).1
forall ea : (f_eb a0).1 = f_a0,
(apD10 ea b0)^ @ (f_eb a0).2 tt =
transport
  (fun s : forall y : B, P a0 y =>
   Unit -> s b0 = f_b0 a0) ea (f_eb a0).2 tt clear ea_eab ea.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
forall ea : (f_eb a0).1 = f_a0,
(apD10 ea b0)^ @ (f_eb a0).2 tt =
transport
  (fun s : forall y : B, P a0 y =>
   Unit -> s b0 = f_b0 a0) ea (f_eb a0).2 tt intros.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea: (f_eb a0).1 = f_a0
(apD10 ea b0)^ @ (f_eb a0).2 tt =
transport
  (fun s : forall y : B, P a0 y =>
   Unit -> s b0 = f_b0 a0) ea (f_eb a0).2 tt
    rewrite transport_arrow.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea: (f_eb a0).1 = f_a0
(apD10 ea b0)^ @ (f_eb a0).2 tt =
transport
  (fun x : forall y : B, P a0 y => x b0 = f_b0 a0) ea
  ((f_eb a0).2
     (transport (fun _ : forall y : B, P a0 y => Unit)
        ea^ tt)) rewrite transport_const.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea: (f_eb a0).1 = f_a0
(apD10 ea b0)^ @ (f_eb a0).2 tt =
transport
  (fun x : forall y : B, P a0 y => x b0 = f_b0 a0) ea
  ((f_eb a0).2 tt) rewrite transport_paths_Fl.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
f_eb: forall y : A,
ExtensionAlong (unit_name b0) 
  (P y) (unit_name (f_b0 y))
ea: (f_eb a0).1 = f_a0
(apD10 ea b0)^ @ (f_eb a0).2 tt =
(ap (fun x : forall y : B, P a0 y => x b0) ea)^ @
(f_eb a0).2 tt
    exact 1%path.
Qed.

(** It is easier to apply the above result with its components separated. *)
Definition wedge_incl_elim : forall a b, P a b
  := isconn_wedge_incl.1.

Definition wedge_incl_comp1 : forall b, wedge_incl_elim a0 b = f_a0 b
  := isconn_wedge_incl.2.1.

Definition wedge_incl_comp2 : forall a, wedge_incl_elim a b0 = f_b0 a
  := isconn_wedge_incl.2.2.1.

Definition wedge_incl_comp3
  : wedge_incl_comp2 a0 = (wedge_incl_comp1 b0) @ f_a0b0
  := isconn_wedge_incl.2.2.2.

End Wedge_Incl_Conn.

Definition wedge_incl_elim_uncurried `{Univalence}
  {m n : trunc_index}
  {A : Type} (a0 : A) `{IsConnected m.+1 A}
  {B : Type} (b0 : B) `{IsConnected n.+1 B}
  (P : A -> B -> Type) {HP : forall a b, IsTrunc (m +2+ n) (P a b)}
  (fs : {f_a0 : forall b:B, P a0 b
        & { f_b0 : forall a:A, P a b0
        & f_a0 b0 = f_b0 a0 }})
  : forall (a : A) (b : B), P a b.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
fs: {f_a0 : forall b : B, P a0 b &
{f_b0 : forall a : A, P a b0 & f_a0 b0 = f_b0 a0}}
forall (a : A) (b : B), P a b
Proof.
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
fs: {f_a0 : forall b : B, P a0 b &
{f_b0 : forall a : A, P a b0 & f_a0 b0 = f_b0 a0}}
forall (a : A) (b : B), P a b
  destruct fs as [f_a0 [f_b0 f_a0b0]].
H: Univalence
m, n: trunc_index
A: Type
a0: A
H0: IsConnected (Tr m.+1) A
B: Type
b0: B
H1: IsConnected (Tr n.+1) B
P: A -> B -> Type
HP: forall (a : A) (b : B), IsTrunc (m +2+ n) (P a b)
f_a0: forall b : B, P a0 b
f_b0: forall a : A, P a b0
f_a0b0: f_a0 b0 = f_b0 a0
forall (a : A) (b : B), P a b
  refine (wedge_incl_elim _ _ _ _ _ f_a0b0).
Defined.