Structural Refactoring Objectives

https://doi.org/10.5281/zenodo.20138853

https://github.com/lombardisedr-dev/PsiU-Protocol-HoTT/blob/main/README.md

The recent optimization phase was dedicated to three fundamental pillars:Homotopic Formalization: A rigorous, clean, and clear theorization at the formal level, ensuring the \(X_{n}\) hierarchy is logically transparent.Protocol Optimization: The creation of an enhanced version of the PSIU Protocol, including its full integration with YML-based verification (CI/CD) for automated auditing.Comprehensive Reporting: Detailed documentation of results and architectural modifications, providing a traceable path for peer-review and future scalability.

This report documents the definitive formal verification of the PSIU Protocol using Agda. By implementing a strict semisimplicial universe without Axiom K, we resolve the higher-dimensional coherence challenges (X3 tetrahedral level), ensuring total stability and well typedness of the system.

The development of this protocol involved a critical refactoring phase. Previous iterations contained imprecisions in the mapping of higher-order coherences between X2 and X3. These were resolved within a 24-hour sprint by rewriting the core transition formulas, leading to the current verified state.

The PSIU Protocol successfully achieves ”Crystallized” stability. The proof is automated via CI/CD and is HoTT-compliant, marking a definitive step in verified semisimplicial structures.

#HoTT #TypeTheory #UnivalentFoundations
#Agda #LeanProver

currently watching this intro to univalent foundations..

.. I'm hoping I can understand most of it ..

I'm intrigued by the idea of a more modern and "better" foundations for mathematics

https://www.youtube.com/watch?v=XIYoI5j5Flo

#maths #univalentFoundations

I enjoyed listening to this lecture, or at least the first half by Emily Riehl. About computer proof and mathematics. And scary vibe proofs and why they are nonsense

https://youtu.be/fzxW2XJS6SE?si=ZS3UQGeI4DAAiUJX

#math #hott #homtopytypetheory #univalentFoundations

Master thesis by Csanad Farkas:
"Formalisation of Display Map Categories in Univalent Foundations"

"A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. [...] The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library."

https://resolver.tudelft.nl/uuid:25ddff49-8d20-40ce-bb35-3b3f986c65ff

#Master #Thesis #Rocq #HoTT #UnivalentFoundations #UniMath

Master thesis by Arnoud van der Leer: Universal Algebra, Univalent Foundations and the Untyped λ-Calculus

"This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. [...] The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation."

https://repository.tudelft.nl/record/uuid:e6582866-9c0d-4a13-8eda-42c25e0deba4

#univalentfoundations #hott #typetheory #thesis

The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics