(no subject)
Jul. 8th, 2017 09:11 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
jcreedLet's say you have a weak omega-category W.
Suppose X, Y are n-cells in it with the same boundary. Say X and Y are equivalent in the expected sense that there are f and g going back and forth such that fg and gf are (coinductively, in the same sense) equivalent to identities.
I think maybe the following univalence-like property is true:
Let equivalent X, Y be given. Then for all "good" sentences P(x) with one free variable x of the same type as X, Y, we have that P(X) holds iff P(Y) holds. Where "good" means you're allowed to mention some constants drawn from W, and all logical connectives including first-order quantifiers over cells in W of a given domain and codomain, but not including any notion of on-the-nose equality.
Suppose X, Y are n-cells in it with the same boundary. Say X and Y are equivalent in the expected sense that there are f and g going back and forth such that fg and gf are (coinductively, in the same sense) equivalent to identities.
I think maybe the following univalence-like property is true:
Let equivalent X, Y be given. Then for all "good" sentences P(x) with one free variable x of the same type as X, Y, we have that P(X) holds iff P(Y) holds. Where "good" means you're allowed to mention some constants drawn from W, and all logical connectives including first-order quantifiers over cells in W of a given domain and codomain, but not including any notion of on-the-nose equality.
