Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Since I was being asked I briefly expanded automorphism infinity-group by adding the internal version and the HoTT syntax.
Mike, what’s the best type theory syntax for the definition of $\mathbf{Aut}(X)$ via $\infty$-image factorization of the name of $X$?
$\sum_{Y:Type} IsInhab(Y=X)$, or any variant depending on your chosen notation for IsInhab and identity/path types. E.g. $\sum_{Y:Type} [Id_Type(Y,X)]$ would be another version.
Ah, thanks. I should have been able to come up with this myself.
Can we allow ourselves to write “$\sum_{Y : Type} [X = Y]$”?
I have added a general remark on this to infinity-image in a new section Syntax in homotopy type theory there.
Can we allow ourselves to write “$\sum_{Y : Type} [X = Y]$”?
Sure, although I would probably mention that $[-]$ denotes the support (and, perhaps, $=$ the intensional identity type / path type) whenever I start using this notation on a given page or in a given paper.
OOPS! I meant $\left[\sum_{Y : Type} (X = Y)\right]$. I’ve corrected the proof at infinity-image.
Hm, I was thinking that
$im_\infty(A \stackrel{(id_A, b)}{\to} A\times B) \to A \times B \to B$is equivalent to
$im_\infty(A \stackrel{b}{\to} B) \to B \,.$Hm…
That’s not even true for 0-truncated objects. In that case $(1,b):A\to A\times B$ is already monic, so the top composite just gives you $b:A\to B$ rather than its image.
Ah, sorry. Right, I am being stupid.
1 to 9 of 9