Jack Widman PhD

I just published What is a Jew? medium.com/p/what-is-a-je…

Python is like most Bar Mitzvahs. It is supposed to be the first practice of your Jewish life, but it turns out to be last. So to with Python. Sad, that so many programmers never meet a language like Haskell or Agda. Stuck in values and never to know the full beauty of types.

@quinnswm Just to be clear, I am not at all asserting that one needs to adopt HoTT as a foundation for Mathematics in order to define Group Theory as the study of those properties invariant under group ismorphism. I've always just defined it that way. But I recognize there are other ways.

@jackwidman Yes I would because set theoretically they are different and I don’t work with homotopy type theory axioms as my foundation of mathematics

I very much do not do this thank you very much

Dr. Gladys West was a mathematician whose work on satellite geodesy models paved the way for modern GPS. She was a member of AKA, an inductee in the Air Force Hall of fame, and has an elementary school named after her. She passed away yesterday at 95yo. Tell her story. 🕊️

Mathematicians say truth ≠ proof (Gödel), yet in practice we treat statements as true only once a proof exists. HoTT takes this seriously: truth is evidence. That’s why the Law of Excluded Middle isn’t automatic—it’s an extra principle, not a given. #HoTT @LawOfExcludedMiddle

Mathematics is getting too complex to scale by human proof alone. Future math will require theorem provers. That makes dependently typed languages not a niche, but the natural target: where programs, proofs, and meaning live in one system. #DependentTypes #ProofAssistants

Constructive mathematics isn’t mainly about rejecting LEM. It’s about foundations where logic and axioms form a single unified system, not two separate layers as in classical math. In HoTT, logic is built into the types themselves. #HoTT #TypeTheory

@quinnswm Do you agree that 'Group Theory is the study of properties invariant under group isomorphism?' If two groups agreed on every single property invariant under group isomorphism, would you consider them distinct groups? Only physical objects have identity independent of properties.

@jackwidman I mean I agree with that description of group theory, I disagree with treating isomorphic objects as equal

@DavidCorfield8 Quotients don’t depend only on the subgroup,they depend on how it sits inside the parent group. Univalence identifies isomorphic objects, not distinct embeddings / subobjects / structure maps. Quotients are not functorial in objects alone; they are functorial in monomorphisms.

@jackwidman "to take a single subgroup H of a group G, and embed it in G in two different ways" sounds odd to my ear whichever system one uses. A subgroup corresponds to an injective map between groups. Then we may find several such maps between H and G which are not equivalent.

To be crystal clear, regarding a former example, it is possible, in Group Theory, to take a single subgroup H of a group G, and embed it in G in two different ways, such that two different quotients are produced. So this approach won't save us from HoTT :)

Paulette Jordan just won the Democratic primary for governor in Idaho. Meaning, she's now positioned to become the first female governor of Idaho--and the first Native American governor in the US.

Perhaps there are two kinds of mathematicians: those who think, e.g. 'Group Theory is the study of properties invariant under isomorphism' and those who don't. Its kinda like Functional vs non Functional programmers. The former are invited to try out HoTT.

@ahron_maline @Tcho76521726 @JDHamkins I am trying to say we should make a concerted effort to adopt the Univalence Axiom and the general framework of Homotopy Type Theory, which would bring along with it a more constructive approach to Mathematics. This, I believe, has been a major blockage to larger experimentation

@Tcho76521726 @JDHamkins @jackwidman These statements are true, but I don't see what you're trying to say

As mathematicians, we treat isomorphic structures as equal. The problem is that set theoretical foundations, ZFC or whatnot, are not consistent with this. We need another foundation. Time to consider Homotopy Type Theory on a large scale? #hott @homotopytypetheory #foundations

@Tcho76521726 @ahron_maline @JDHamkins There are copies of Z2 in this group, but they are not identical as subobject in the categorical sense and that is why they mod out into different groups.

@ahron_maline @JDHamkins @jackwidman Clearly there's more than one isomorphic copy of Z2 in this group, seeing as you can literally quotient by different isomorphic copies and get different groups

Another approach. In group theory, a group theoretic property is one that is preserved under isomorphism. The notion of identity I am using is that if two things can't be distinguished by a property, then they are the same thing. There are no identical twins in Group Theory.

@JamesBlevins0O7 @JDHamkins There is a misconception here. Yes, there exist isomorphic subgroups H≅K of a group G, such that G/H ≇ G/K. This is true but irrelevant to my Univalence claim. Why? H and K are isomorphic as abstract groups but they are not equal as subobjects of G.

@JDHamkins @jackwidman A counter-example can be understood by 7th-grade students. Horizontal reflections and pi-rotations each generate groups of order 2, which are isomorphic. Their join gives a larger group, which includes vertical reflections. Thus, isomorphism ≠ = . ∎

@Tcho76521726 @ahron_maline @JDHamkins There is a misconception. Reestating what you said more generally, there exist isomorphic subgroups H≅K of G, such that G/H ≇ G/K. This is true but irrelevant to my Univalence claim. Why? H and K are isomorphic as abstract groups but they are not equal as subobjects of G.

@ahron_maline @JDHamkins @jackwidman There are obviously several isomorphic copies of the same group. Take D8 x Z2, quotienting by the center, which is Z2, gives V4 x Z2 but quotienting by the right index gives D8.

@ahron_maline @JDHamkins Under Univalence, its not going to a copy, its going to the same group.

@JDHamkins @jackwidman In the case of an automorphism, don't we both agree that it goes to "the same" group rather than to some new copy? So why is this more of a challenge to me than to you?