[-- Attachment #1.1: Type: text/plain, Size: 3295 bytes --] Probably just for amusement only. (1) In the category of topological spaces (not up to homotopy), if X and Y are exponentiable and we topologize the space (X ≃ Y) of homeomorphisms of X and Y with the subspace topology, we get that co-derived-set (Y+1) × (X ≃ Y) ≃ (X+1 ≃ Y+1). The proof relies on classical logic. Exponentiability is only needed to make sense of (X ≃ Y) as a space, and hence we could alternatively work with compactly generated spaces, which have all exponentials, but I haven't checked the above in that case (yet). The derived set, in the sense of Cantor, is the set of limit points. Here we consider its complement, with the subspace topology, which of course is the discrete topology. When X is the same space as Y, the above specializes to co-derived-set (X+1) × Aut X ≃ Aut (X+1), where Aut X is the space of auto (homeo)morphisms of X. Hence when X is discrete, so that it is its own coderived set, the above specializes to the "factorial equation" (X+1) × Aut X ≃ Aut (X+1). But if X is perfect in the sense of Cantor (has no isolated points), then instead we get Aux X = Aut (X+1) because the coderived set of X+1 is homeomorphic to 1. (2) The above holds if we replace "space" by "homotopy type" and can be proved in HoTT/UF, *this time without appealing to classical logic* (and I doubt appealing to classical logic can simplify the argument, because the argument seems to be as simple and direct as it can be). For this, we need the following definitions in HoTT/UF: * A point x is *isolated* if the type x=y is decidable for all y:X. (Counter-example: any point of the circle.) * A type is *discrete* if all its points are isolated. (Example: natural numbers, the finite type Fin n with n elements.) * A space is *perfect* if it has no isolated points. (Example: the circle.) There is also a notion that doesn't arise above but that does arise in the proofs/constructions: * A point x is *h(omotopy)-isolated* if the type x=y is a proposition, or a subsingleton, for every point y. By local Hedberg, every isolated point is h-isolated. (3) In particular, if Fin n is the type with n elements, Fin (n+1) × Aut (Fin n) ≃ Aut (Fin (n+1)) from which we get Fin (n!) ≃ Aut (Fin n) by induction on n, as expected. (4) Although the above development uses HoTT/UF ideas crucially, only function extensionality is needed to carry out the constructions and proofs (in particular, propositional extensionality and univalence are not needed). I had fun formalizing the above ideas in Agda: https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.html and so I wanted to share it here. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 4449 bytes --] <div dir="ltr"><div>Probably just for amusement only.</div><div><br></div><div>(1) In the category of topological spaces (not up to homotopy), if X and Y are exponentiable and we topologize the space (X ≃ Y) of homeomorphisms of X and Y with the subspace topology, we get that</div><div><br></div><div> co-derived-set (Y+1) × (X ≃ Y) ≃ (X+1 ≃ Y+1).</div><div><br></div><div>The proof relies on classical logic.</div><div><br></div><div>Exponentiability is only needed to make sense of (X ≃ Y) as a space, and hence we could alternatively work with compactly generated spaces, which have all exponentials, but I haven't checked the above in that case (yet).</div><div><br></div><div>The derived set, in the sense of Cantor, is the set of limit points. Here we consider its complement, with the subspace topology, which of course is the discrete topology.</div><div><br></div><div>When X is the same space as Y, the above specializes to </div><div><br></div><div> co-derived-set (X+1) × Aut X ≃ Aut (X+1),</div><div><br></div><div>where Aut X is the space of auto (homeo)morphisms of X.</div><div><br></div><div>Hence when X is discrete, so that it is its own coderived set, the above specializes to the "factorial equation"</div><div><br></div><div> (X+1) × Aut X ≃ Aut (X+1).</div><div><br></div><div>But if X is perfect in the sense of Cantor (has no isolated points), then instead we get </div><div><br></div><div> Aux X = Aut (X+1)</div><div><br></div><div>because the coderived set of X+1 is homeomorphic to 1.</div><div><br></div><div>(2) The above holds if we replace "space" by "homotopy type" and can be proved in HoTT/UF, *this time without appealing to classical logic* (and I doubt appealing to classical logic can simplify the argument, because the argument seems to be as simple and direct as it can be).</div><div><br></div><div>For this, we need the following definitions in HoTT/UF:</div><div><br></div><div> * A point x is *isolated* if the type x=y is decidable for all y:X.</div><div> (Counter-example: any point of the circle.)</div><div><br></div><div> * A type is *discrete* if all its points are isolated.</div><div> (Example: natural numbers, the finite type Fin n with n elements.)</div><div><br></div><div> * A space is *perfect* if it has no isolated points.</div><div> (Example: the circle.)</div><div><br></div><div>There is also a notion that doesn't arise above but that does arise in the proofs/constructions:</div><div><br></div><div> * A point x is *h(omotopy)-isolated* if the type x=y is a proposition, </div><div> or a subsingleton, for every point y. </div><div><br></div><div> By local Hedberg, every isolated point is h-isolated.</div><div><br></div><div><br></div><div>(3) In particular, if Fin n is the type with n elements, </div><div><br></div><div> Fin (n+1) × Aut (Fin n) ≃ Aut (Fin (n+1))</div><div><br></div><div>from which we get</div><div><br></div><div> Fin (n!) ≃ Aut (Fin n)</div><div><br></div><div>by induction on n, as expected.</div><div><br></div><div>(4) Although the above development uses HoTT/UF ideas crucially, only function extensionality is needed to carry out the constructions and proofs (in particular, propositional extensionality and univalence are not needed).</div><div><br></div><div>I had fun formalizing the above ideas in Agda:</div><div><br></div><div> https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html</div><div> https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.html</div><div><br></div><div>and so I wanted to share it here.</div><div><br></div><div>Best,</div><div>Martin</div><div><br></div><div><br></div><div> </div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com</a>.<br />