HoTT
Unify `BAut X` with `Type_ O`?
BAut X is defined to be { Z : Type & merely (Z = X) }.
When O : Type -> Type is a Subuniverse (so its values are hprops), Type_ O is defined to be { Z : Type & O Z } (roughly).
If we fix X and define O Z to be merely (Z = X), then the two coincide. Except that O Z is in a larger universe than Z, which isn't allowed by the definition of Subuniverse.
Would it be worth it to add another universe variable to Subuniverse saying where the hprops live? They would infiltrate a lot of other code. But many facts are true for both BAut X and Type_ O, so they could be proved only once. This came up in practice, since Type_ O is the object classifier for fibrations with fiber in O, but one can't use that to study fibrations whose fiber is merely equal to X.
Maybe there are other situations in which one would like to consider a Subuniverse where the predicate lands in a different universe? Or maybe this is rare enough that we should just keep Type_ O and BAut X separate? Or maybe there can be Subuniverse' and Type_' that allow this flexibility, but are not used in the Modalities code?
I meant to mention that as an option as well. It might be a fair bit of work adjusting all of the existing BAut proofs. Any idea whether things would generally become simpler or more complicated? It looks like essentially all results about BAut already assume Univalence, so the change wouldn't force use to use more Univalence (and might let us reduce it?)
No, I don't really have a guess. Probably it would make some things more complicated but others less complicated, and I don't have a guess about which would predominate. It would be worth a try to find out, I think.
I agree that it would probably be worth trying to change the definition of BAut to use equivalences and see how it goes.
About adding an extra universe variable to Subuniverse, I just noticed that FactorizationSystem has two extra universe variables for the two predicates on the universe, so there is a precedent for allowing this flexibility.
Actually, the extra universe variables j and k for FactorizationSystem are constrained to be <= i, so this doesn't really give any extra flexibility that I can see. It looks to me like both FactorizationSystem and Factorization might make sense with just a single universe variable, but I haven't thought about this carefully.
I am also interested in BAut at the moment. I want to define symmetric groups for some group theory that I am doing. I noticed that BAut has quite a few universes:
BAut@{u u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 u17 u18} : Type -> Type
If we define BAut X to be { Z : Type & merely (Z <~> X) } then proving connectedness requires univalence, so any statement about BAut X as an oo-group will use it. So this can only increase usage of univalence for such things.
In practice I'm finding it satisfactory that Type_ O and BAut X (with the definition using paths) are easy to prove equivalent, using the fact that Type_ O unifies with the definition of BAut X above.
Isn't Univalence used almost everywhere already? So I'm not sure that it matters too much whether we need Univalence to prove connectivity. I'm more curious whether various proofs become easier or harder overall. And I'm still wondering about just allowing the hprop's in the definition of subuniverse to be in another universe...
Looking at your PR, I see the point you are making. BAut is later redefined to be classifying_space (Aut X), and with the proposed definition, we would need univalence just to define Aut X as an ooGroup. I agree that this doesn't seem like the best approach.