(no subject)

Как известно, я в целом интересуюсь
гомотопической теорией типов
  (потому что она кодирует принцип Duck Typing'а "indistinguishable things are equal"),
направленными гомотопиями
  (потому что они естественным образом кодируют каузальную структуру и обещают прогресс в гомотопической теории типов),
эквилогическими пространствами
  (потому что категория EqL это минимальная "хорошая" категория, содержащая Top*) и
некоммутативной геометрией
  (потому что на её языке очень красиво формулируются теории поля, включая кастрированную** версию нынешней единой теории поля (см. noncommutative standard model).)

(* Судя по всемy Higher inductive type with semidecidable equality (T: Type, _≟_: (a: T, b: T) → ℧(a = b)) это в точности обсервабельное эквилогическое пространство.)
(** Эвклидова версия формулируется, а Лоренцева нет.)

В связи с успехами в первой, возник большой интерес к кубическим множествам. А оказывается, что оно всё связано в клубок. Вот что пишет Марко, наш, Грандис аж в 2004 году:
"An unexpected byproduct of a previous work on the homology of cubical sets was finding that such structures also contain models of 'virtual spaces' of interest in noncommutative geometry, namely the irrational rotation
C*-algebras or 'noncommutative tori' which cannot be realised as topological spaces. [..W]e show here how the simpler structure of an equilogical space can still express some of those 'formal quotients' of spaces; more effective results will be obtained, in a sequel, with a directed version, preordered equilogical spaces."

http://www.dima.unige.it/~grandis/Eql.pdf