5HT

Ця система типів є фундаментом і алгебраїчної геометрії тому шо квантор узагальнення Pi
є нетривіальним ізоморфізмом до розшарування Fiber Bundle, використовується як
основний примітив алгебраїчної геометрії.

  type term =

I) Мова складається з 5 слів. 2 слова універсальні для всіх типізованих мов програмування.

1) Перше слово --- це "Змінна" --- інтуітивно природнє поняття, яке показує іменоване алфавітами або числами місце в програмі-реченні, що може містити інші програми-речення.

5HT

$ ./gradlew bootRun

> Task :bootRun

  .   ____          _            __ _ _
 /\\ / ___'_ __ _ _(_)_ __  __ _ \ \ \ \
( ( )\___ | '_ | '_| | '_ \/ _` | \ \ \ \
 \\/  ___)| |_)| | | | | || (_| |  ) ) ) )
  '  |____| .__|_| |_|_| |_\__, | / / / /
 =========|_|==============|___/=/_/_/_/

5HT

(* Type System *)
type exp =
  | EVar of string | ELam of exp * (string * exp) | EApp of exp * exp
  | EPi of exp * (string * exp) | ESig of exp * (string * exp) | EPair of string * exp * exp
  | EId of exp | ERef of exp 
  | EInt | EIntConst of Z.t | ERat | ERatConst of exp * exp | ERatLt of exp * exp
  | EReal | ECut of exp * exp * exp option * exp option * exp option * exp option * exp option * exp option * exp option
  | ERealLt of exp * exp | ERealEq of exp * exp | ERealOps of real_op * exp * exp
  | EIm of exp | EInf of exp | EIndIm of exp * exp
  | EDisc of exp | EHub of exp | EBase of exp | ESpoke of exp * exp | EIndDisc of exp * exp * exp * exp * exp

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