5HT

Parameter Point : Set.(* Define congruence of segments, written as AB ≡ CD *)
Parameter Cong : Point -> Point -> Point -> Point -> Prop.
Notation "A B ≡ C D" := (Cong A B C D) (at level 70).(* Define betweenness: B is between A and C, written A-B-C *)
Parameter Bet : Point -> Point -> Point -> Prop.
Notation "A - B - C" := (Bet A B C) (at level 70).(* Define perpendicularity: line AB ⊥ CD *)
Parameter Perp : Point -> Point -> Point -> Point -> Prop.
Notation "A B ⊥ C D" := (Perp A B C D) (at level 70).(* Congruence is an equivalence relation *)
Axiom Cong_refl : forall A B, A B ≡ A B.
Axiom Cong_sym : forall A B C D, A B ≡ C D -> C D ≡ A B.
Axiom Cong_trans : forall A B C D E F, A B ≡ C D -> C D ≡ E F -> A B ≡ E F.(* Identity axiom for congruence *)

5HT

Volume VIII: Consciousness
==========================

Kuhn arrays all the theories on a linear spectrum, simplistically and roughly,
from the most physical on the left (at the beginning) to the least physical
on the right (near the end).

* Physicalism
* Non-Reductive Physicalism
* Integrated Information Theory

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