Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Extensions Limits.Pullback.
Require Import Modality Lex Open Closed Nullification.

Local Open Scope path_scope.


(** * The lex-modal fracture theorem *)

(** The fracture theorem for two modalities [O1] and [O2] and a type [A], when it holds, states that the naturality square

<<
 A   -->   O1 A
 |          |
 |          |
 V          V
O2 A --> O2 (O1 A)
>>

is a pullback.  This says in a certain precise sense that [A] can be recovered from its [O1]- and [O2]-reflections together with some information about how they fit together.  If we think of [O1] and [O2] as subuniverses or subtoposes, then the fracture theorem says that their "union", or more precisely their *gluing*, is the whole universe.

We will prove the fracture theorem holds under the assumptions that [O2] is lex, and that [O1]-connected types are [O2]-modal.  Note that like lex-ness, the latter is also a "large" hypothesis.  But also as with lex-ness, rather than hypothesize it polymorphically with a module type, we just hypothesize it in the obvious way and allow the polymorphism of the resulting theorem to be computed automatically.  This actually gives more precise information: the fracture theorem for a particular type [A] only depends on this hypothesis for types [B] lying in the same universe as [A].  (In fact, as we will see, it only needs the special cases of the fibers of [to O1 A], but in examples it seems no harder to verify the general case.)

It may sometimes happen that in addition, the "intersection" of [O1] and [O2] is trivial.  This is naturally expressed in the context of the fracture theorem by saying that [O2]-modal types are [O1]-connected, i.e. the converse of the second hypothesis of our fracture theorem.  When this also holds, we can show that the universe [Type] can actually be reconstructed, up to equivalence, from the universes of [O1]- and [O2]-modal types and the [O2]-reflection from the first to the second, using the "Artin gluing construction" from topos theory.  *)

  (** ** The fracture theorem *)

  Section FractureTheorem.
    Context (O1 O2 : Modality).

    Definition fracture_square (A : Type)
    : O_functor O2 (to O1 A) o to O2 A == to O2 (O1 A) o to O1 A
    := to_O_natural O2 (to O1 A).

    (** Here are the hypotheses of the fracture theorem *)
    Context `{Lex O2}.

    Definition Gluable : Type
      := forall (A : Type), IsConnected O1 A -> In O2 A.
    Context (ino2_isconnectedo1 : Gluable).

    (** The fracture theorem. *)
    Definition ispullback_fracture_square A
    : IsPullback (fracture_square A).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
IsPullback (fracture_square A)
    Proof.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
IsPullback (fracture_square A)
      apply ispullback_symm.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
IsPullback (fun a : A => (fracture_square A a)^)
      nrefine (ispullback_connmap_mapino_commsq O2 _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
Lex O2
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
O_inverts O2 (to O2 A)
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
O_inverts O2 (to O2 (O_reflector O1 A))
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
MapIn O2 (to O1 A)
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
MapIn O2 (O_functor O2 (to O1 A))
      1-3:exact _.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
MapIn O2 (to O1 A)
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
MapIn O2 (O_functor O2 (to O1 A))
      2:rapply mapinO_between_inO.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
A: Type
MapIn O2 (to O1 A)
      intros x; exact (ino2_isconnectedo1 _ _).
    Defined.

    (** ** The fracture gluing theorem *)

    (** We now also assume the converse of the second hypothesis *)
    Definition Disjoint : Type
      := forall (A : Type), In O2 A -> IsConnected O1 A.
    Context (isconnectedo1_ino2 : Disjoint).

    (** This implies that the universe decomposes into an [O1]-part, an [O2]-part, and a gluing map.  We define these pieces separately in order to make the maps transparent but the homotopies opaque. *)
    Definition fracture_glue_uncurried
    : { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }} -> Type
      := fun BCf => Pullback BCf.2.2 (to O2 BCf.1).

    Definition fracture_glue
      (B C : Type) `{HB: In O1 B} `{HC: In O2 C} (f : C -> O2 B)
    : Type
      := fracture_glue_uncurried ((B;HB);((C;HC);f)).

    Definition fracture_unglue
    : Type -> { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }}
    := fun A => ((O1 A ; O_inO A) ; ((O2 A ; O_inO A) ; O_functor O2 (to O1 A))).

    Definition fracture_unglue_isretr `{Univalence}
               (BCf : { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }})
    : fracture_unglue (fracture_glue_uncurried BCf) = BCf.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
BCf: {B : Type_ O1 & {C : Type_ O2 & C -> O2 B}}
fracture_unglue (fracture_glue_uncurried BCf) = BCf
    Proof.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
BCf: {B : Type_ O1 & {C : Type_ O2 & C -> O2 B}}
fracture_unglue (fracture_glue_uncurried BCf) = BCf
      destruct BCf as [B [C f]].
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
fracture_unglue (fracture_glue_uncurried (B; C; f)) =
(B; C; f)
      (** The first two components of our path will be applications of univalence.  We begin by observing that maps we will use are equivalences. *)
      assert (IsEquiv (O_rec ((to O2 B)^*' f))).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
IsEquiv (O_rec ((to O2 B) ^*' f))
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
fracture_unglue (fracture_glue_uncurried (B; C; f)) =
(B; C; f)
      {
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
IsEquiv (O_rec ((to O2 B) ^*' f)) apply isequiv_O_rec_O_inverts.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
O_inverts O1 ((to O2 B) ^*' f)
        apply O_inverts_conn_map, conn_map_pullback'.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
IsConnMap O1 f
        intros ob; apply isconnectedo1_ino2.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
ob: O_reflector O2 B
In O2 (hfiber f ob)
        rapply mapinO_between_inO. }
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
fracture_unglue (fracture_glue_uncurried (B; C; f)) =
(B; C; f)
      assert (IsEquiv (O_rec (f^* (to O2 B)))).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
IsEquiv (O_rec (f^* (to O2 B)))
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
fracture_unglue (fracture_glue_uncurried (B; C; f)) =
(B; C; f)
      {
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
IsEquiv (O_rec (f^* (to O2 B))) apply isequiv_O_rec_O_inverts.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
O_inverts O2 (f^* (to O2 B))
        apply O_inverts_conn_map, conn_map_pullback; exact _. }
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
fracture_unglue (fracture_glue_uncurried (B; C; f)) =
(B; C; f)
      (** Now we start building the path. *)
      simple refine (path_sigma' _ _ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
(O1 (fracture_glue_uncurried (B; C; f));
O_inO (fracture_glue_uncurried (B; C; f))) = B
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
transport
  (fun B : Type_ O1 => {C : Type_ O2 & C -> O2 B}) 
  ?p
  ((O2 (fracture_glue_uncurried (B; C; f));
   O_inO (fracture_glue_uncurried (B; C; f)));
  O_functor O2
    (to O1 (fracture_glue_uncurried (B; C; f)))) =
(C; f)
      {
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
(O1 (fracture_glue_uncurried (B; C; f));
O_inO (fracture_glue_uncurried (B; C; f))) = B apply path_TypeO; unfold ".1", ".2".
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
O1 (fracture_glue_uncurried (B; C; f)) = B.1
        exact (path_universe (O_rec ((to O2 B)^*' f))). }
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
transport
  (fun B : Type_ O1 => {C : Type_ O2 & C -> O2 B})
  (path_TypeO O1
     (O1 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) B
     (path_universe (O_rec ((to O2 B) ^*' f))
      :
      (O1 (fracture_glue_uncurried (B; C; f));
      O_inO (fracture_glue_uncurried (B; C; f))).1 =
      B.1))
  ((O2 (fracture_glue_uncurried (B; C; f));
   O_inO (fracture_glue_uncurried (B; C; f)));
  O_functor O2
    (to O1 (fracture_glue_uncurried (B; C; f)))) =
(C; f)
      refine (transport_sigma' _ _ @ _); unfold ".1", ".2".
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
((O2 (fracture_glue_uncurried (B; C; f));
 O_inO (fracture_glue_uncurried (B; C; f)));
transport
  (fun x : Type_ O1 =>
   (O2 (fracture_glue_uncurried (B; C; f));
   O_inO (fracture_glue_uncurried (B; C; f))) -> O2 x)
  (path_TypeO O1
     (O1 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) B
     (path_universe (O_rec ((to O2 B) ^*' f))))
  (O_functor O2
     (to O1 (fracture_glue_uncurried (B; C; f))))) =
(C; f)
      simple refine (path_sigma' _ _ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
(O2 (fracture_glue_uncurried (B; C; f));
O_inO (fracture_glue_uncurried (B; C; f))) = C
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
transport (fun y : Type_ O2 => y -> O2 B) 
  ?p
  (transport
     (fun x : Type_ O1 =>
      (O2 (fracture_glue_uncurried (B; C; f));
      O_inO (fracture_glue_uncurried (B; C; f))) ->
      O2 x)
     (path_TypeO O1
        (O1 (fracture_glue_uncurried (B; C; f));
        O_inO (fracture_glue_uncurried (B; C; f))) B
        (path_universe (O_rec ((to O2 B) ^*' f))))
     (O_functor O2
        (to O1 (fracture_glue_uncurried (B; C; f))))) =
f
      {
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
(O2 (fracture_glue_uncurried (B; C; f));
O_inO (fracture_glue_uncurried (B; C; f))) = C apply path_TypeO; unfold ".1", ".2".
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
O2 (fracture_glue_uncurried (B; C; f)) = C.1
        exact (path_universe (O_rec (f^* (to O2 B)))). }
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
transport (fun y : Type_ O2 => y -> O2 B)
  (path_TypeO O2
     (O2 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) C
     (path_universe (O_rec (f^* (to O2 B)))
      :
      (O2 (fracture_glue_uncurried (B; C; f));
      O_inO (fracture_glue_uncurried (B; C; f))).1 =
      C.1))
  (transport
     (fun x : Type_ O1 =>
      (O2 (fracture_glue_uncurried (B; C; f));
      O_inO (fracture_glue_uncurried (B; C; f))) ->
      O2 x)
     (path_TypeO O1
        (O1 (fracture_glue_uncurried (B; C; f));
        O_inO (fracture_glue_uncurried (B; C; f))) B
        (path_universe (O_rec ((to O2 B) ^*' f))))
     (O_functor O2
        (to O1 (fracture_glue_uncurried (B; C; f))))) =
f
      (** It remains to identify the induced function with the given [f].  We begin with some boilerplate. *)
      apply path_arrow; intros c.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport (fun y : Type_ O2 => y -> O2 B)
  (path_TypeO O2
     (O2 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) C
     (path_universe (O_rec (f^* (to O2 B)))))
  (transport
     (fun x : Type_ O1 =>
      (O2 (fracture_glue_uncurried (B; C; f));
      O_inO (fracture_glue_uncurried (B; C; f))) ->
      O2 x)
     (path_TypeO O1
        (O1 (fracture_glue_uncurried (B; C; f));
        O_inO (fracture_glue_uncurried (B; C; f))) B
        (path_universe (O_rec ((to O2 B) ^*' f))))
     (O_functor O2
        (to O1 (fracture_glue_uncurried (B; C; f)))))
  c = f c
      refine (transport_arrow_toconst _ _ _ @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport
  (fun x : Type_ O1 =>
   (O2 (fracture_glue_uncurried (B; C; f));
   O_inO (fracture_glue_uncurried (B; C; f))) -> O2 x)
  (path_TypeO O1
     (O1 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) B
     (path_universe (O_rec ((to O2 B) ^*' f))))
  (O_functor O2
     (to O1 (fracture_glue_uncurried (B; C; f))))
  (transport (TypeO_pr1 O2)
     (path_TypeO O2
        (O2 (fracture_glue_uncurried (B; C; f));
        O_inO (fracture_glue_uncurried (B; C; f))) C
        (path_universe (O_rec (f^* (to O2 B)))))^ c) =
f c
      refine (transport_arrow_fromconst
                (C := fun X:Type_ O1 => O2 X) _ _ _ @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport (fun X : Type_ O1 => O2 X)
  (path_TypeO O1
     (O1 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) B
     (path_universe (O_rec ((to O2 B) ^*' f))))
  (O_functor O2
     (to O1 (fracture_glue_uncurried (B; C; f)))
     (transport (TypeO_pr1 O2)
        (path_TypeO O2
           (O2 (fracture_glue_uncurried (B; C; f));
           O_inO (fracture_glue_uncurried (B; C; f)))
           C (path_universe (O_rec (f^* (to O2 B)))))^
        c)) = f c
      refine (transport_compose O2 (TypeO_pr1 O1) _ _ @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport O2
  (ap (TypeO_pr1 O1)
     (path_TypeO O1
        (O1 (fracture_glue_uncurried (B; C; f));
        O_inO (fracture_glue_uncurried (B; C; f))) B
        (path_universe (O_rec ((to O2 B) ^*' f)))))
  (O_functor O2
     (to O1 (fracture_glue_uncurried (B; C; f)))
     (transport (TypeO_pr1 O2)
        (path_TypeO O2
           (O2 (fracture_glue_uncurried (B; C; f));
           O_inO (fracture_glue_uncurried (B; C; f)))
           C (path_universe (O_rec (f^* (to O2 B)))))^
        c)) = f c
      refine (transport_compose idmap O2 _ _ @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (ap O2
     (ap (TypeO_pr1 O1)
        (path_TypeO O1
           (O1 (fracture_glue_uncurried (B; C; f));
           O_inO (fracture_glue_uncurried (B; C; f)))
           B (path_universe (O_rec ((to O2 B) ^*' f))))))
  (O_functor O2
     (to O1 (fracture_glue_uncurried (B; C; f)))
     (transport (TypeO_pr1 O2)
        (path_TypeO O2
           (O2 (fracture_glue_uncurried (B; C; f));
           O_inO (fracture_glue_uncurried (B; C; f)))
           C (path_universe (O_rec (f^* (to O2 B)))))^
        c)) = f c
      (** Now we have to compute through the action of [ap] and [transport] on paths in sigmas and the universe.  In applying these it helps to specify a couple of intermediate steps explicitly. *)
      transitivity (transport idmap
                     (ap O2 (path_universe (O_rec ((to O2 B)^*' f))))
                     (O_functor O2 (to O1 (Pullback f (to O2 B)))
                                ((O_rec (f^* (to O2 B)))^-1 c)));
        [ apply ap11; repeat apply ap
        | transitivity (O_functor O2 (O_rec ((to O2 B)^*' f))
                          (O_functor O2 (to O1 (Pullback f (to O2 B)))
                                     ((O_rec (f^* (to O2 B)))^-1 c))) ].
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
ap (TypeO_pr1 O1)
  (path_TypeO O1
     (O1 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) B
     (path_universe (O_rec ((to O2 B) ^*' f)))) =
path_universe (O_rec ((to O2 B) ^*' f))
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport (TypeO_pr1 O2)
  (path_TypeO O2
     (O2 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) C
     (path_universe (O_rec (f^* (to O2 B)))))^ c =
(O_rec (f^* (to O2 B)))^-1 c
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (ap O2 (path_universe (O_rec ((to O2 B) ^*' f))))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c)) =
O_functor O2 (O_rec ((to O2 B) ^*' f))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c))
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
O_functor O2 (O_rec ((to O2 B) ^*' f))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c)) = 
f c
      +
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
ap (TypeO_pr1 O1)
  (path_TypeO O1
     (O1 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) B
     (path_universe (O_rec ((to O2 B) ^*' f)))) =
path_universe (O_rec ((to O2 B) ^*' f)) exact (pr1_path_sigma_uncurried _ @ eisretr pr1 _).
      +
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport (TypeO_pr1 O2)
  (path_TypeO O2
     (O2 (fracture_glue_uncurried (B; C; f));
     O_inO (fracture_glue_uncurried (B; C; f))) C
     (path_universe (O_rec (f^* (to O2 B)))))^ c =
(O_rec (f^* (to O2 B)))^-1 c refine (transport_compose idmap (TypeO_pr1 O2)
                  (path_TypeO O2 (O2 (Pullback f (to O2 B)); _) C _)^
                  c @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (ap (TypeO_pr1 O2)
     (path_TypeO O2
        (O2 (Pullback f (to O2 B));
        O_inO (fracture_glue_uncurried (B; C; f))) C
        (path_universe (O_rec (f^* (to O2 B)))))^) c =
(O_rec (f^* (to O2 B)))^-1 c
        refine (ap (fun p => transport idmap p c) (ap_V _ _) @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (ap (TypeO_pr1 O2)
     (path_TypeO O2
        (O2 (Pullback f (to O2 B));
        O_inO (fracture_glue_uncurried (B; C; f))) C
        (path_universe (O_rec (f^* (to O2 B))))))^ c =
(O_rec (f^* (to O2 B)))^-1 c
        refine (ap (fun p => transport idmap p^ c)
                   (pr1_path_sigma_uncurried _ @ eisretr pr1 _) @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (path_universe (O_rec (f^* (to O2 B))))^ c =
(O_rec (f^* (to O2 B)))^-1 c
        exact (transport_path_universe_V _ _).
      +
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (ap O2 (path_universe (O_rec ((to O2 B) ^*' f))))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c)) =
O_functor O2 (O_rec ((to O2 B) ^*' f))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c)) refine (ap (fun p => transport idmap p _)
                   (ap_O_path_universe O2 _) @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
transport idmap
  (path_universe
     (O_functor O2 (O_rec ((to O2 B) ^*' f))))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c)) =
O_functor O2 (O_rec ((to O2 B) ^*' f))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c))
        exact (transport_path_universe _ _).
      (** Now we're down to the real point. *)
      +
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
O_functor O2 (O_rec ((to O2 B) ^*' f))
  (O_functor O2 (to O1 (Pullback f (to O2 B)))
     ((O_rec (f^* (to O2 B)))^-1 c)) = f c refine ((O_functor_compose O2 _ _ _)^ @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
O_functor O2
  (fun x : Pullback f (to O2 B) =>
   O_rec ((to O2 B) ^*' f)
     (to O1 (Pullback f (to O2 B)) x))
  ((O_rec (f^* (to O2 B)))^-1 c) = f c
        refine (O_functor_homotopy O2 _ _ (O_rec_beta _) _ @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
c: C
O_functor O2 ((to O2 B) ^*' f)
  ((O_rec (f^* (to O2 B)))^-1 c) = f c
        revert c; equiv_intro (O_rec (f^* (to O2 B))) x.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
x: O_reflector O2 (Pullback f (to O2 B))
O_functor O2 ((to O2 B) ^*' f)
  ((O_rec (f^* (to O2 B)))^-1
     (O_rec (f^* (to O2 B)) x)) =
f (O_rec (f^* (to O2 B)) x)
        refine (ap _ (eissect _ _) @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
x: O_reflector O2 (Pullback f (to O2 B))
O_functor O2 ((to O2 B) ^*' f) x =
f (O_rec (f^* (to O2 B)) x)
        revert x; apply O_indpaths; intros x.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
x: Pullback f (to O2 B)
O_functor O2 ((to O2 B) ^*' f)
  (to O2 (Pullback f (to O2 B)) x) =
f
  (O_rec (f^* (to O2 B))
     (to O2 (Pullback f (to O2 B)) x))
        refine (to_O_natural O2 _ x @ _).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
x: Pullback f (to O2 B)
to O2 B ((to O2 B) ^*' f x) =
f
  (O_rec (f^* (to O2 B))
     (to O2 (Pullback f (to O2 B)) x))
        refine (_ @ ap f (O_rec_beta _ _)^).
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
B: Type_ O1
C: Type_ O2
f: C -> O2 B
X: IsEquiv (O_rec ((to O2 B) ^*' f))
X0: IsEquiv (O_rec (f^* (to O2 B)))
x: Pullback f (to O2 B)
to O2 B ((to O2 B) ^*' f x) = f (f^* (to O2 B) x)
        destruct x as [a [b q]]; exact (q^).
    Qed.

    Definition fracture_unglue_issect `{Univalence} (A : Type)
    : fracture_glue_uncurried (fracture_unglue A) = A.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
A: Type
fracture_glue_uncurried (fracture_unglue A) = A
    Proof.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
A: Type
fracture_glue_uncurried (fracture_unglue A) = A
      apply path_universe_uncurried, equiv_inverse.
O1, O2: Modality
Lex0: Lex O2
ino2_isconnectedo1: Gluable
isconnectedo1_ino2: Disjoint
H: Univalence
A: Type
A <~> fracture_glue_uncurried (fracture_unglue A)
      exact (Build_Equiv _ _ (pullback_corec (fracture_square A))
                        (ispullback_fracture_square A)).
    Qed.

    Definition isequiv_fracture_unglue `{Univalence}
    : IsEquiv fracture_unglue
      := isequiv_adjointify
           fracture_unglue
           fracture_glue_uncurried
           fracture_unglue_isretr
           fracture_unglue_issect.

    Definition equiv_fracture_unglue `{Univalence}
    : Type <~> { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }}
      := Build_Equiv _ _ fracture_unglue isequiv_fracture_unglue.

  End FractureTheorem.

(** ** The propositional fracture theorem *)

(** An easy example of the lex-modal fracture theorem is supplied by the open and closed modalities for an hprop [U]. *)

Definition gluable_open_closed `{Funext} (U : HProp)
: Gluable (Op U) (Cl U).
H: Funext
U: HProp
Gluable (Op U) (Cl U)
Proof.
H: Funext
U: HProp
Gluable (Op U) (Cl U)
  intros A.
H: Funext
U: HProp
A: Type
IsConnected (Op U) A -> In (Cl U) A
  change (Contr (U -> A) -> (U -> Contr A)); intros ? u.
H: Funext
U: HProp
A: Type
X: Contr (U -> A)
u: U
Contr A
  apply (Build_Contr _ (center (U -> A) u)); intros a.
H: Funext
U: HProp
A: Type
X: Contr (U -> A)
u: U
a: A
center (U -> A) u = a
  exact (ap10 (path_contr _ (fun _ => a)) u).
Defined.

Definition disjoint_open_closed `{Funext} (U : HProp)
: Disjoint (Op U) (Cl U).
H: Funext
U: HProp
Disjoint (Op U) (Cl U)
Proof.
H: Funext
U: HProp
Disjoint (Op U) (Cl U)
  intros A.
H: Funext
U: HProp
A: Type
In (Cl U) A -> IsConnected (Op U) A
  change ((U -> Contr A) -> Contr (U -> A)); intros uc.
H: Funext
U: HProp
A: Type
uc: U -> Contr A
Contr (U -> A)
  apply (Build_Contr _ (fun u => let i := uc u in center A)).
H: Funext
U: HProp
A: Type
uc: U -> Contr A
forall y : U -> A,
(fun u : U => let i := uc u in center A) = y
  intros f; apply path_arrow; intros u.
H: Funext
U: HProp
A: Type
uc: U -> Contr A
f: U -> A
u: U
(let i := uc u in center A) = f u
  pose (uc u); apply path_contr.
Defined.

(** We can also prove the same thing without funext if we use the nullification versions of these modalities. *)

Definition gluable_open_closed' (U : HProp)
: Gluable (Op' U) (Cl' U).
U: HProp
Gluable (Op' U) (Cl' U)
Proof.
U: HProp
Gluable (Op' U) (Cl' U)
  intros A ? u; simpl in *.
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
ooExtendableAlong (fun _ : Empty => tt) (unit_name A)
  pose proof (contr_inhabited_hprop U u).
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
ooExtendableAlong (fun _ : Empty => tt) (unit_name A)
  assert (Contr A).
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
Contr A
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
X1: Contr A
ooExtendableAlong (fun _ : Empty => tt) (unit_name A)
  {
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
Contr A simple refine (contr_equiv (Op' U A) _).
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
Op' U A -> A
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
IsEquiv ?f
    -
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
Op' U A -> A refine (O_rec idmap).
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
In (Op' U) A
      intros []; simpl.
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
ooExtendableAlong (fun _ : U => tt) (unit_name A)
      apply ooextendable_equiv.
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
IsEquiv (fun _ : U => tt)
      exact (equiv_isequiv (@equiv_contr_contr U Unit _ _)).
    -
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
IsEquiv (O_rec idmap) refine (isequiv_adjointify _ (to (Op' U) A) _ _).
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
(fun x : A => O_rec idmap (to (Op' U) A x)) == idmap
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
(fun x : O_reflector (Op' U) A =>
 to (Op' U) A (O_rec idmap x)) == idmap
      +
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
(fun x : A => O_rec idmap (to (Op' U) A x)) == idmap intros a; apply O_rec_beta.
      +
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
(fun x : O_reflector (Op' U) A =>
 to (Op' U) A (O_rec idmap x)) == idmap apply O_indpaths; cbn.
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
(fun x : A => loc x) == (fun x : A => loc x) reflexivity. }
U: HProp
A: Type
X: IsConnected (Op' U) A
u: U
X0: Contr U
X1: Contr A
ooExtendableAlong (fun _ : Empty => tt) (unit_name A)
  apply ooextendable_contr; exact _.
Defined.

Definition disjoint_open_closed' (U : HProp)
: Disjoint (Op' U) (Cl' U).
U: HProp
Disjoint (Op' U) (Cl' U)
Proof.
U: HProp
Disjoint (Op' U) (Cl' U)
  intros A An.
U: HProp
A: Type
An: In (Cl' U) A
IsConnected (Op' U) A
  apply isconnected_from_elim; intros C Cn f.
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
NullHomotopy.NullHomotopy f
  simple refine (@local_rec _ C Cn tt _ tt ; _); simpl.
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
U -> C
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
forall x : A,
f x =
local_rec
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |}) ?Goal tt
  -
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
U -> C intros u.
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
u: U
C
    exact (f (@local_rec _ A An u Empty_rec tt)).
  -
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
forall x : A,
f x =
local_rec
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |})
  (fun u : U =>
   f
     (local_rec
        (Accessible.null_to_local_generators
           {|
             Accessible.ngen_indices := U;
             Accessible.ngen_type :=
               fun _ : U => Empty
           |}) Empty_rec tt)) tt intros a; simpl.
U: HProp
A: Type
An: In (Cl' U) A
C: Type
Cn: In (Op' U) C
f: A -> C
a: A
f a =
local_rec
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |})
  (fun u : U =>
   f
     (local_rec
        (Accessible.null_to_local_generators
           {|
             Accessible.ngen_indices := U;
             Accessible.ngen_type :=
               fun _ : U => Empty
           |}) Empty_rec tt)) tt
    refine (@local_indpaths _ C Cn tt (fun _ => f a) _ _ tt);
      intros u; simpl in *.
U: HProp
A: Type
An: Accessible.IsLocal_Internal.IsLocal
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := U;
       Accessible.ngen_type := fun _ : U => Empty
     |}) A
C: Type
Cn: Accessible.IsLocal_Internal.IsLocal
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |}) C
f: A -> C
a: A
u: U
f a =
local_rec
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |})
  (fun u : U =>
   f
     (local_rec
        (Accessible.null_to_local_generators
           {|
             Accessible.ngen_indices := U;
             Accessible.ngen_type :=
               fun _ : U => Empty
           |}) Empty_rec tt)) tt
    refine (_ @ (@local_rec_beta _ C Cn tt _ u)^).
U: HProp
A: Type
An: Accessible.IsLocal_Internal.IsLocal
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := U;
       Accessible.ngen_type := fun _ : U => Empty
     |}) A
C: Type
Cn: Accessible.IsLocal_Internal.IsLocal
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |}) C
f: A -> C
a: A
u: U
f a =
f
  (local_rec
     (Accessible.null_to_local_generators
        {|
          Accessible.ngen_indices := U;
          Accessible.ngen_type := fun _ : U => Empty
        |}) Empty_rec tt)
    apply ap.
U: HProp
A: Type
An: Accessible.IsLocal_Internal.IsLocal
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := U;
       Accessible.ngen_type := fun _ : U => Empty
     |}) A
C: Type
Cn: Accessible.IsLocal_Internal.IsLocal
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := Unit;
       Accessible.ngen_type := unit_name U
     |}) C
f: A -> C
a: A
u: U
a =
local_rec
  (Accessible.null_to_local_generators
     {|
       Accessible.ngen_indices := U;
       Accessible.ngen_type := fun _ : U => Empty
     |}) Empty_rec tt
    exact (@local_indpaths _ A An u (fun _ => a) _ (Empty_ind _) tt).
Defined.