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.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: automorphism infinity-group

Bottom of Page

1 to 9 of 9

- 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 $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(X)</annotation></semantics></math>$ via $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>$ -image factorization of the name of $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>$ ?
- 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.

$<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>Y</mi><mo>:</mo><mi>Type</mi></mrow></msub><mi>IsInhab</mi><mo stretchy="false">(</mo><mi>Y</mi><mo>=</mo><mi>X</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\sum_{Y:Type} IsInhab(Y=X)</annotation></semantics></math>$ , or any variant depending on your chosen notation for IsInhab and identity/path types. E.g. $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>Y</mi><mo>:</mo><mi>Type</mi></mrow></msub><mo stretchy="false">[</mo><msub><mi>Id</mi> <mi>Type</mi></msub><mo stretchy="false">(</mo><mi>Y</mi><mo>,</mo><mi>X</mi><mo stretchy="false">)</mo><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">\sum_{Y:Type} [Id_Type(Y,X)]</annotation></semantics></math>$ would be another version.
- 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 “ $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>Y</mi><mo>:</mo><mi>Type</mi></mrow></msub><mo stretchy="false">[</mo><mi>X</mi><mo>=</mo><mi>Y</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">\sum_{Y : Type} [X = Y]</annotation></semantics></math>$ ”?
- 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.
- 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 “ $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>Y</mi><mo>:</mo><mi>Type</mi></mrow></msub><mo stretchy="false">[</mo><mi>X</mi><mo>=</mo><mi>Y</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">\sum_{Y : Type} [X = Y]</annotation></semantics></math>$ ”?

Sure, although I would probably mention that $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo stretchy="false">[</mo><mo lspace="0.11111em" rspace="0em">−</mo><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[-]</annotation></semantics></math>$ denotes the support (and, perhaps, $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo>=</mo></mrow><annotation encoding="application/x-tex">=</annotation></semantics></math>$ 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
- 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 $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mrow><mo>[</mo><msub><mo lspace="0.16667em" rspace="0.16667em">∑</mo> <mrow><mi>Y</mi><mo>:</mo><mi>Type</mi></mrow></msub><mo stretchy="false">(</mo><mi>X</mi><mo>=</mo><mi>Y</mi><mo stretchy="false">)</mo><mo>]</mo></mrow></mrow><annotation encoding="application/x-tex">\left[\sum_{Y : Type} (X = Y)\right]</annotation></semantics></math>$ . I’ve corrected the proof at infinity-image.
- 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
$<math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><msub><mi>im</mi> <mn>∞</mn></msub><mo stretchy="false">(</mo><mi>A</mi><mover><mo>→</mo><mrow><mo stretchy="false">(</mo><msub><mi>id</mi> <mi>A</mi></msub><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></mover><mi>A</mi><mo>×</mo><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>A</mi><mo>×</mo><mi>B</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex"> im_\infty(A \stackrel{(id_A, b)}{\to} A\times B) \to A \times B \to B </annotation></semantics></math>$
is equivalent to
$<math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><msub><mi>im</mi> <mn>∞</mn></msub><mo stretchy="false">(</mo><mi>A</mi><mover><mo>→</mo><mi>b</mi></mover><mi>B</mi><mo stretchy="false">)</mo><mo>→</mo><mi>B</mi><mspace width="0.16667em"/><mo>.</mo></mrow><annotation encoding="application/x-tex"> im_\infty(A \stackrel{b}{\to} B) \to B \,. </annotation></semantics></math>$
Hm…
- 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 $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo stretchy="false">(</mo><mn>1</mn><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo><mo>:</mo><mi>A</mi><mo>→</mo><mi>A</mi><mo>×</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">(1,b):A\to A\times B</annotation></semantics></math>$ is already monic, so the top composite just gives you $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>b</mi><mo>:</mo><mi>A</mi><mo>→</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">b:A\to B</annotation></semantics></math>$ rather than its image.
- 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.

1 to 9 of 9

nForum

Discussion Feed

Not signed in

Discussion Tag Cloud

nLab > Latest Changes: automorphism infinity-group