# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeSep 25th 2012

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$?

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeSep 26th 2012

$\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.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeSep 26th 2012
• (edited Sep 26th 2012)

Ah, thanks. I should have been able to come up with this myself.

Can we allow ourselves to write “$\sum_{Y : Type} [X = Y]$”?

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeSep 26th 2012
• (edited Sep 26th 2012)

I have added a general remark on this to infinity-image in a new section Syntax in homotopy type theory there.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeSep 26th 2012

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.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeSep 26th 2012

OOPS! I meant $\left[\sum_{Y : Type} (X = Y)\right]$. I’ve corrected the proof at infinity-image.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeSep 26th 2012
• (edited Sep 26th 2012)

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…

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeSep 27th 2012

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.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeSep 27th 2012
• (edited Sep 27th 2012)

Ah, sorry. Right, I am being stupid.