Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 25th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexSince 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$?

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

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex$\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.

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

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 26th 2012
   • (edited Sep 26th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAh, thanks. I should have been able to come up with this myself. Can we allow ourselves to write "$\sum_{Y : Type} [X = Y]$"?

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

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

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 26th 2012
   • (edited Sep 26th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added a general remark on this to _[[infinity-image]]_ in a new section _[Syntax in homotopy type theory](http://ncatlab.org/nlab/show/infinity-image#SyntaxInHomotopyTypeTheory)_ there.

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

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeSep 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeSep 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOOPS! I meant $\left[\sum_{Y : Type} (X = Y)\right]$. I've corrected the proof at [[infinity-image]].

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

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeSep 26th 2012
   • (edited Sep 26th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, 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...

   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…

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeSep 27th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat'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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeSep 27th 2012
   • (edited Sep 27th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAh, sorry. Right, I am being stupid.

   Ah, sorry. Right, I am being stupid.