5HT

Let build a Type System for mechanical verification of BROUWER’S FIXED-POINT THEOREM IN REAL-COHESIVE HOMOTOPY TYPE THEORY https://arxiv.org/pdf/1509.07584 by Shulman

Here is proposed CCHM(HoTT)/Cohesive (Im) core: Extend if needed and produce proof therm of Brower's Fixed Point Theorem in this type theory to verify mechanically. Then we will build a specialized type checker for these purposes.

type exp =
  | EPre of Z.t | EKan of Z.t | EVar of name | EHole                                 (* cosmos *)
  | EPi of exp * (name * exp) | ELam of exp * (name * exp) | EApp of exp * exp           (* pi *)
  | ESig of exp * (name * exp) | EPair of tag * exp * exp | EFst of exp | ESnd of exp (* sigma *)
  | EId of exp | ERef of exp | EJ of exp | EField of exp * string           (* strict equality *)
  | EPathP of exp | EPLam of exp | EAppFormula of exp * exp                   (* path equality *)

5HT

Let's build a Simplicial HoTT extension to CCHM/CHM/HTS type systems targeting GAP replacement, infinity-gategorical framework like Rezk prover (Riehl, Shulman) for Simplex and Simplicial types built into type checker. Then gradually extent type inference rules for Group, Monoid, Category, Chain, Ring, Field. As eliminators I propose Face, Degeneracies, Composition, as Introduction inference rule I propose Simplicial Object with common syntax:

def <name> : <type> := П (context), conditions ⊢ <n> (elements | constraints)

def chain : Chain := П (context), conditions ⊢ n (C₀, C₁, ..., Cₙ | ∂₀, ∂₁, ..., ∂ₙ₋₁)
def simplicial : Simplicial := П (context), conditions ⊢ n (s₀, s₁, ..., sₙ | facemaps, degeneracies)
def group : Group := П (context), conditions ⊢ n (generators | relations)
def cat : Category := П (context), conditions ⊢ n (objects | morphisms | coherence)

Consider examples:

5HT

aim_spu_module.self
appldr
creserved_0
default.spp
emer_init.self
eurus_fw.bin
hdd_copy.self
isoldr
lv0
lv1.self

5HT

BDIT_FIRMWARE_PACKAGE.pkg
BDPT_FIRMWARE_PACKAGE_301R.pkg
BDPT_FIRMWARE_PACKAGE_302R.pkg
BDPT_FIRMWARE_PACKAGE_303R.pkg
BDPT_FIRMWARE_PACKAGE_304R.pkg
BDPT_FIRMWARE_PACKAGE_306R.pkg
BDPT_FIRMWARE_PACKAGE_308R.pkg
BLUETOOTH_FIRMWARE.pkg
CORE_OS_PACKAGE.pkg
MULTI_CARD_FIRMWARE.pkg

5HT

.
├── CP_Update
│   ├── Readme_CP_e.txt
│   ├── Readme_CP_j.txt
│   ├── license
│   │   ├── ps3tool_license_e.txt
│   │   └── ps3tool_license_j.txt
│   └── reftool_cp_133.bin
├── HW_doc
│   ├── Readme-RSX_Doc_e.txt

5HT

Can we build up an isomorphism between Mathematics, Thinking and Space from the Grothendieck perspective?

Introduction
Embarking on the exploration of whether we can establish an isomorphism between Mathematics, Thinking, and Space from the Grothendieck perspective is both ambitious and profoundly intriguing. To tackle this, I'll start by breaking down the key components: understanding what an isomorphism means in a mathematical context, delving into Grothendieck's contributions to mathematics, and then attempting to see how these concepts might bridge Mathematics, Thinking, and Space.

Understanding Isomorphism
In mathematics, an isomorphism is a mapping between two structures of the same type that can be reversed by an inverse mapping. It signifies a one-to-one correspondence that preserves the structure and operations within those systems. For example, in group theory, two groups are isomorphic if there's a bijective function between them that respects the group operation.

Extending this concept beyond p

5HT

Can we build up an isomorphism between Mathematics, Thinking and Space from the Grothendieck perspective?

ChatGPT said:

Developing an isomorphism between mathematics, thinking, and space from the Grothendieck perspective is a fascinating idea. Alexandre Grothendieck's mathematical philosophy often revolved around uncovering deep structural insights, focusing on relationships and transformations rather than isolated objects. This approach can inspire analogous insights into thinking and space.

Here’s a high-level roadmap for building such an isomorphism:

1. Mathematics as a Structure of Relationships 

5HT

https://www.bundesdruckerei.de/en/innovation-hub/qeaa-put-simply
https://github.com/eID4U/eIDAS-node/blob/master/EIDAS-Config-eID4U/server/eidas.xml
https://github.com/Governikus/eidas-middleware/tree/master/eidas-demo
https://eudiwalletconsortium.org/wp-content/uploads/2024/11/EWC-D3.3-PID-country-enrolment-process-definition_v1.pdf
https://eu-digital-identity-wallet.github.io/eudi-doc-architecture-and-reference-framework/1.1.0/annexes/annex-06-pid-rulebook.pdf
https://eu-digital-identity-wallet.github.io/eudi-doc-architecture-and-reference-framework/1.1.0/annexes/annex-01-initialisation-and-activation.pdf
https://walt.id/blog/p/mdl-eid-and-beyond
https://openid.github.io/OpenID4VCI/openid-4-verifiable-credential-issuance-wg-draft.html
https://www.digital-identity-wallet.eu/

5HT

maxim@TRISTELLAR:~/depot/synrc/vm/lib$ tree -L 3 .
.
├── atom
│   ├── include
│   │   ├── etest.hrl
│   │   └── ledc.hrl
│   └── src
│       ├── ahttp_client.erl
│       ├── atom.app.src
│       ├── atomvm.erl

5HT

maxim@TRISTELLAR:/mnt/d/Books$ cat books.txt
.
├── Applied Mathematics
│   ├── Algebra
│   │   ├── Artin. Algebra. Second Edition.pdf
│   │   ├── Artin. Algebra.djvu
│   │   ├── Artin. Algebra.pdf
│   │   ├── Artin. Galois Theory.pdf
│   │   └── Serre. Topics in Galois Theory.pdf
│   ├── Calculus