working with equivalences is very slow

[jdchristensen]

This started as a discussion in #1472.

Working with equivalences has been very slow lately. Here's a test script that shows the issue and works with multiple versions of the library. When things are good, the Time command gives 11s on my machine. When they are bad, it gives 98s. Good and bad commits are shown below.

Require Import HoTT.

Local Open Scope trunc_scope.
Local Open Scope mc_mult_scope.

Definition test (X : pType) `{IsTrunc 1 X}
  : { bloop' : Pi1 X -> loops X &
                   forall x y : Pi1 X, bloop' (x * y) = bloop' x @ bloop' y }.
Proof.
    exists (equiv_tr 0 _)^-1%equiv.
    Time simpl.

Things are bad with this commit:

commit 6468b5b3db01d73bf73436b24752f34d54d32dda (HEAD)
Merge: 96d42444c0 d3f7d7fdee
Author: Ali Caglayan <alizter@gmail.com>
Date:   Mon Apr 12 20:07:34 2021 +0200

    Merge pull request #1446 from Alizter/eisadj

    Removed eisadj_other + some optimizations

Things are good two days earlier:

commit 6982fbfdbd163aafb1692efcc78024787f9cf921
Merge: 6d0c7ac116 d89dbb62b3
Author: Ali Caglayan <alizter@gmail.com>
Date:   Sat Apr 10 17:00:08 2021 +0200

    Merge pull request #1436 from Alizter/predgroup

    Predicate subgroups

[jdchristensen]

Even 11s seems long for this kind of thing. Would it help to rethink how the data for an equivalence f is defined? Since we often use isequiv_adjointify, that needs to be unfolded in order to get the inverse function. What if we instead provided the inverse function g, and then called a function like isequiv_adjointify to produce the rest of the data for isequiv? Then we could avoid needing to unfold that function in many situations. The operation of taking an inverse would swap the two functions f and g, and apply a function that transforms the half-adjoint data for f,g to the half-adjoint data for g,f. Again, in many cases that function would not need to be unfolded.

Maybe this would entail changing IsEquiv f to a record with two fields, one the inverse function g and the other another record which packages up the rest of the data needed for a half-adjoint equivalence. We could still have accessor functions like eissect, so the library wouldn't need to change.

[JasonGross]

Perhaps we should first try making the coherence data actually opaque for isequiv_adjointify. https://github.com/HoTT/HoTT/blob/72afece390894bb5201e7d0ab98acd52d3c125fc/theories/Basics/Equivalences.v#L144-L154 has a Qed at the end, but in fact for Let a Qed is the same as a Defined, so we should either wrap the proof in abstract or replace Let with Lemma. Or even make it a Definition and add Opaque or simpl never. As it is currently we're inlining the adjointification data a lot.

I don't think that reorganizing the data a bit is going to help much; we will still end up with large arguments to opaque proofs that do not simplify.

[JasonGross]

The issue here is not in equivalences, though, it's that you're blowing up on modalities and reflective subuniverse definitions (cc @mikeshulman ). If you do Opaque Tr, then simpl returns instantly giving you forall x y : Tr 0 (point X = point X), O_rec idmap (x * y) = O_rec idmap x @ O_rec idmap y. If you then issue Transparent Tr. cbv [Tr]. Set Printing All., you get

this enormous term

```coq 1 subgoal (ID 106) X : pType H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) (pointed_type X) ============================ forall x y : rsu_reflector (modality_to_reflective_subuniverse (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))), @paths (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@O_rec (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@istrunc_paths (pointed_type X) (trunc_S (trunc_S minus_two)) H (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (Build_Reflects (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun (Q : Type) (Q_inO : In (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) Q) => @extendable_to_OO (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (modality_reflectsD (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun _ : @O_reflector (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) => Q) (fun _ : @O_reflector (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) => Q_inO))) (fun x0 : @paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) => x0) (@sg_op (rsu_reflector (modality_to_reflective_subuniverse (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun x0 y0 : rsu_reflector (modality_to_reflective_subuniverse (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) => @Trunc_ind (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (fun _ : Trunc (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) => rsu_reflector (modality_to_reflective_subuniverse (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun _ : Trunc (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) => istrunc_truncation (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun y1 : @paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) => @Trunc_ind (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (fun _ : Trunc (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) => rsu_reflector (modality_to_reflective_subuniverse (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun _ : Trunc (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) => istrunc_truncation (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun x1 : @paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) => @tr (trunc_S (trunc_S minus_two)) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@concat (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) x1 y1)) x0) y0) x y)) (@concat (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) (@O_rec (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@istrunc_paths (pointed_type X) (trunc_S (trunc_S minus_two)) H (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (Build_Reflects (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun (Q : Type) (Q_inO : In (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) Q) => @extendable_to_OO (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (modality_reflectsD (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun _ : @O_reflector (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) => Q) (fun _ : @O_reflector (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) => Q_inO))) (fun x0 : @paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) => x0) x) (@O_rec (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (@istrunc_paths (pointed_type X) (trunc_S (trunc_S minus_two)) H (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (Build_Reflects (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun (Q : Type) (Q_inO : In (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) Q) => @extendable_to_OO (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (modality_reflectsD (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) (fun _ : @O_reflector (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) => Q) (fun _ : @O_reflector (modality_subuniv (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z'))) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X))) (modality_prereflects (Build_Modality (IsTrunc (trunc_S (trunc_S minus_two))) (fun (H0 : Funext) (T : Type) => @ishprop_istrunc H0 (trunc_S (trunc_S minus_two)) T) (fun (A B : Type) (X0 : IsTrunc (trunc_S (trunc_S minus_two)) A) (f : forall _ : A, B) (X1 : @IsEquiv A B f) => @istrunc_isequiv_istrunc A B f (trunc_S (trunc_S minus_two)) X0 X1) (Trunc (trunc_S (trunc_S minus_two))) (fun T : Type => istrunc_truncation (trunc_S (trunc_S minus_two)) T) (fun A : Type => @tr (trunc_S (trunc_S minus_two)) A) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (B_inO : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (oa : Trunc (trunc_S (trunc_S minus_two)) A) => @Trunc_ind (trunc_S (trunc_S minus_two)) A B B_inO f oa) (fun (A : Type) (B : forall _ : Trunc (trunc_S (trunc_S minus_two)) A, Type) (_ : forall oa : Trunc (trunc_S (trunc_S minus_two)) A, IsTrunc (trunc_S (trunc_S minus_two)) (B oa)) (f : forall a : A, B (@tr (trunc_S (trunc_S minus_two)) A a)) (a : A) => @idpath (B (@tr (trunc_S (trunc_S minus_two)) A a)) (f a)) (fun (A : Type) (A_inO : IsTrunc (trunc_S (trunc_S minus_two)) A) (z z' : A) => @istrunc_paths A (trunc_S (trunc_S minus_two)) (@istrunc_succ (trunc_S (trunc_S minus_two)) A A_inO) z z')) (@paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)))) => Q_inO))) (fun x0 : @paths (pointed_type X) (@point (pointed_type X) (ispointed_type X)) (@point (pointed_type X) (ispointed_type X)) => x0) y)) ```

Where are you hoping for things to simplify down to here?

[JasonGross]

Btw, the way that I tracked this down was to Set Printing All., take all of the identifiers in the goal, mark them all as Opaque, and then do binary search on this list to find the minimal set of identifiers that needed to be opaque to make simpl fast. Then I would manually unfold whichever identifiers I thought should be unfolded, and repeat the process.

[JasonGross]

And then the next issue you have is O_rec, which for whatever reason simpl is slow with. If you issue either Arguments O_rec / . or cbv [O_rec] after Opaque Tr. simpl. Transparent Tr., then simpl is again instantaneous. In fact, if you issue Arguments O_rec / . at the beginning, then simpl is instantaneous and reduces your goal to

  forall x y : Tr 0 (point X = point X),
  Trunc_ind (fun _ : Trunc 0 (point X = point X) => point X = point X) idmap (x * y) =
  Trunc_ind (fun _ : Trunc 0 (point X = point X) => point X = point X) idmap x @
  Trunc_ind (fun _ : Trunc 0 (point X = point X) => point X = point X) idmap y

[Alizter]

I just noticed that marking eisadj as opaque seems to have done nothing. I guess it requires a Global.

[jdchristensen]

@JasonGross Thanks for analyzing this so carefully! It seems that there are two separate issues here. One having to do with changes to eisadj that were introduced around Apr 10-12, and can probably be fixed by making it Opaque. The other might have to do with Tr, but I don't fully understand what's going on there, or what the right solution is. The idea of changing isadjoint' might also be helpful too.

I'm happy with either concise form of the goal that you showed. E.g. what simpl gives if you wait long enough is:

  forall x y : Tr 0 (point X = point X),
  O_rec idmap (x * y) = O_rec idmap x @ O_rec idmap y

[JasonGross]

If what you are looking for is forall x y : Tr 0 (point X = point X), O_rec idmap (x * y) = O_rec idmap x @ O_rec idmap y, then perhaps what you want is Arguments Tr : simpl never. and Arguments sg_op : simpl never.. Then simpl is still slow, but cbn is instantaneous and gives this compact form.

[JasonGross]

Furthermore, if you then issue cbv [O_rec Tr], then cbn is again instantaneous and gives the Trunc_ind version.

[JasonGross]

If you do

  exists (equiv_tr 0 _)^-1%equiv.
  Arguments Tr : simpl never.
  Arguments sg_op : simpl never.
  cbn.
  cbv [O_rec].
  cbn.

then you get

  forall x y : Tr 0 (point X = point X),
  (fst (extendable_to_OO (fun _ : O_reflector (modality_subuniv (Tr 0)) (point X = point X) => point X = point X) 1%nat) idmap).1
    (x * y) =
  (fst (extendable_to_OO (fun _ : O_reflector (modality_subuniv (Tr 0)) (point X = point X) => point X = point X) 1%nat) idmap).1 x 
@
  (fst (extendable_to_OO (fun _ : O_reflector (modality_subuniv (Tr 0)) (point X = point X) => point X = point X) 1%nat) idmap).1 y  

So it seems to me the issue here is just that you should not unfold Tr unless you are also planning to unfold O_rec.

[jdchristensen]

I can't say what's best overall, just that even with the fix to eisadj, some things seem unnecessarily slow.

BTW, when you wrote "So it seems to me the issue here is just that you should not unfold Tr unless you are also planning to unfold O_rec." did you mean to reverse "Tr" and "O_rec" in that sentence?

I'm also confused about the fact simpl never doesn't prevent simpl from unfolding Tr, but after googling I see that it is a known, long-standing issue.

[JasonGross]

BTW, when you wrote "So it seems to me the issue here is just that you should not unfold Tr unless you are also planning to unfold O_rec." did you mean to reverse "Tr" and "O_rec" in that sentence?

No. If you issue Arguments Tr : simpl never. or Opaque Tr. then cbn is fast. If you want to unfold Tr you can instead issue Arguments O_rec / . to indicate that O_rec should be unfolded early, and then cbn is still fast and will unfold both Tr and O_rec. Furthermore, there is no issue with issuing both of these commands, whence cbn will (quickly) unfold O_rec without unfolding Tr. So it is perfectly fine to unfold O_rec without unfolding Tr, but cbn is slow if you tell it to unfold Tr without unfolding O_rec.

I'm also confused about the fact simpl never doesn't prevent simpl from unfolding Tr, but after googling I see that it is a known, long-standing issue.

Indeed, this is one of the ways cbn is supposed to be more well-behaved than simpl.

[jdchristensen]

The is_adjoint' issue was nicely spotted and speeds some things up.

Any opinions about whether we should make Tr opaque or make O_rec unfold more easily? I think we should try one of the two (but not both, since doing both leads to an ugly term). Based on #1477, the former sounds easier, but I can imagine situations in which this might not be ideal.

[Alizter]

@jdchristensen There was only a problem in one place and that was BAut/Rigid.v I believe. The rest of the library didn't care about making Tr opaque.

[Alizter]

IIRC there are a few places in the library where we haven't used isequiv_adjointify on purpose, due to their being a cleaner proof of the traingle. Here is an example in MappingCylinder.v:

https://github.com/HoTT/HoTT/blob/36ed41c8e7f523ddf357f18c1003cafcf13bf2b9/theories/Colimits/MappingCylinder.v#L74-L95