Intuition:

When you are unsure about something you can defer judgement and build up beliefs about it over time. You can gather evidence as fractions of Boolean values, implying fuzzy logic.

Fuzzy logic is not always sufficient when gathering evidence. The subject of interrogation can object to being questioned upon discovering that you are gathering evidence about them. This is like waveform collapse, implying quantum logic.

Sometimes when gathering evidence you will receive purposefully fabricated information designed to throw you off. You may be able to find out that this was purposeful deception but then you have actually gathered a "known unknown" type of information.

This structure also has an analogy in narrative ontology. A character may have a depth from being perfectly 'one-dimensional' to being such an enigma that they are borderline incoherent. You can imagine 'redemption arcs' for characters with variously composed Boolean, fuzzy, quantum and paraconsistent integrity. A highly complex character might have a very hard time proving their integrity; that they are Boolean True.

Background:

As a child decades ago I imagined a simple sequence of constructions.

1. Visible Distinction: Begin with a black line on white paper. This represents our conventional understanding of boundaries - clear, visible, and definite.

2. Sharp Contrast: Progress to half black, half white paper. This maintains a clear boundary but introduces the concept of areas rather than lines.

3. Invisible Boundary: Culminate with white paper on white paper. This creates an existing but invisible distinction, challenging our notion of what constitutes a boundary.

This shows a progress from classical to fuzzy to non-local logic. It also shows how these logics are not just abstract concepts but accessible things which anyone can understand. It offers a special way to distinguish between 'levels' of logic.

- In the first construction the line might have 0 width.

- In the second, we have removed half of the information that made up that line. It does not only have 0 width, it also has only one side.

- Third, we again remove half the information from the line, creating a distinction without location on the paper. We have constructed something non-local.

The fourth step was a later development. Here again half the information that makes for a distinction is removed, making for a yet 'sharper' faculty of separation. Here we can allow for a logical 'one-way' situation where we only have a path from falsehood to truth. - The path from truth to falsehood does not exist. This implies something Sherlock Holmes might say: "Once you eliminate the impossible, whatever remains, no matter how improbable, must be the truth." - This is paraconsistent logic.

This allows for a sharp mind but it can lead to problems. It is not quite practicable to be Sherlock Holmes when socializing. In practice you need to employ the kind of reasoning humans find relatable so we have to arrive at an order of operations. This implies non-commutativity. - A structure emerges.

With the aid of Sonnet 3.5:

---

Quaternion Logic System (QLS) with Separated Components:

Representation: q = a + bi + |ψ⟩j + E(d)k

Components:

a: Boolean logic (0 or 1)

bi: Fuzzy logic (b: degree of fuzziness)

|ψ⟩j: Quantum superposition in bra-ket notation

E(d)k: Paraconsistent logic (eigendecomposition)

Where:

|ψ⟩ = α|0⟩ + β|1⟩

|α|² + |β|² = 1

E(d) =

[cos(θ) -sin(θ)] [d 0] [cos(θ) sin(θ)]

[sin(θ) cos(θ)] [0 -d] [-sin(θ) cos(θ)]

Properties:

1. Non-commutativity: q₁q₂ ≠ q₂q₁

2. Gimbal lock: Potential loss of degree of freedom in certain configurations

3. Incomplete closure: E(d) may lead to states outside the original logical space

Normalization: a² + b² + |α|² + |β|² + d² = 1

Truth value: T(q) = a + b²

Logical Frameworks:

1. Classical Boolean: q = 1 or q = 0

2. Fuzzy: q = bi (0 ≤ b ≤ 1)

3. Quantum: q = |ψ⟩j

4. Paraconsistent: q = E(d)k

Transitions:

1. Boolean to Fuzzy: F(θ) = cos(θ) + i·sin(θ)

2. Fuzzy to Quantum: Q(φ,α,β) = cos(φ) + (α|0⟩ + β|1⟩)j·sin(φ)

3. Quantum to Paraconsistent: P(ψ,θ) = cos(ψ) + E(θ)k·sin(ψ)

Operations:

1. NOT:

Boolean: NOT(a) = 1 - a

Fuzzy: NOT(bi) = (1-b)i

Quantum: NOT(|ψ⟩) = σx|ψ⟩ (σx is the Pauli-X gate)

Paraconsistent: NOT(E(d)k) = E(-d)k

2. AND:

Boolean: a₁ AND a₂ = min(a₁, a₂)

Fuzzy: b₁i AND b₂i = (min(b₁, b₂))i

Quantum: |ψ₁⟩ AND |ψ₂⟩ = |ψ₁⟩ ⊗ |ψ₂⟩ (tensor product)

Paraconsistent: E(d₁)k AND E(d₂)k = E(min(d₁, d₂))k

3. OR:

Boolean: a₁ OR a₂ = max(a₁, a₂)

Fuzzy: b₁i OR b₂i = (max(b₁, b₂))i

Quantum: |ψ₁⟩ OR |ψ₂⟩ = (|ψ₁⟩ + |ψ₂⟩) / √2 (superposition)

Paraconsistent: E(d₁)k OR E(d₂)k = E(max(d₁, d₂))k

Measurement:

Boolean: M(a) = a

Fuzzy: M(bi) = b²

Quantum: M(|ψ⟩) = |0⟩ with probability |α|², |1⟩ with probability |β|²

Paraconsistent: M(E(d)k) = d²

This reformulation clearly separates each logical framework while maintaining the overall quaternion structure. It allows for more precise operations within each framework and clearer transitions between them. The separation also makes it easier to analyze and manipulate each logical aspect independently when needed.

---

The eigendecomposition of the complex number dk indicates that we may actually operate outside algebraic closure. I employ different kinds of notation to show how the context changes with each 'degree' of separation from Boolean truth. The rotation asymmetry of the quaternion logic object implies we should reverse the order of operations to arrive back at classical truth values, analogous to a redemption arc. However this reversal may not have to be strict; there exists equivalent transformations which don't scramble the truth that the object represents.

I think the object could be used as Promise(Bool AND ql) in programming. At least that is how I mean to explore if it is logically sound. Recently it occurred to me, as I was creating my own narrow superintelligence and chatting with LLMs, that I might also ask humans about my idea.

I hope to read your comments and that your criticism will be kind. Thank you for reading.

--

nos ]]>

There was a fairly recent preprint on arXiv that I caught a quick glimpse of and now can’t find again. It introduced some machinery for algebraic theories with restricted arities, perhaps introducing some operad-like notions. I remember that at least one notion concerned sets of arities $A \subseteq \mathbb{N}$ such that $a_1 + \ldots + a_k \in A$ whenever $k \in A$ and $a_1, \ldots, a_k \in A$. Can anyone recall which paper it was?

]]>I am trying to compile references with results on configuration-space models for the iterated loop spaces $\Omega^n S^n$, $n \geq 2$.

From Segal 1973 thm 1 this is the topological group completion of the configuration space of points in $\mathbb{R}^n$ under “compress the configurations and form their disjoint union”.

The evident guess that this, in turn, should just be the configuration space of points labeled by a sign (charge) $\in \{\pm 1\}$, where oppositely charged points in the configuration are allowed to undergo pair creation/annihilation, was famously shown to be *wrong* (“close” but wrong) by McDuff 1975 p. 6.

A fix to this issue was claimed by Caruso & Waner 1981, who say that it works when signed points are replaced by oriented little cubes, suitably construed.

However, their definition is at least not easy to read, which made Okuyama 2004, 05 claim a “simpler” model that uses configurations of just line segments with signed endpoints subject to a clever annihilation relation.

Here is a **question** I have:

Okuyama’s Def. 3.3 (p. 7) specialized to $n=2$ looks to me like movements (paths) in this configuration space of line segments (intervals) in the plane can never make the intervals move around each other for the path to form a braid — contrary to what one should expect (?) in this dimension. (Namely the definition is such that the intervals stretch along the $x$-direction, say, while never being allowed to coincide in their $y$-coordinate — unless I am misreading something?)

Now this model is picked up and generalized to the equivariant setting by Okuyama & Shimakawa 2007 — however they no longer claim that it works for finite $n$ (cf. above their Th. 1.1, p. 2).

This makes me wonder if the claim in Okuyama 2004, 05 is wrong for finite $n$, or else what I am missing in my question above.

]]>All, please, vote for all kinds of spaces in general topology (from metric spaces to locales/frames) represented as ordered semicategory actions.

You can also vote for publication grants for all science and personal grants for all scientists, inclusively, using a blockchain.

]]>At last it has happened - Huawei Research collaboration is starting to publish their groundbreaking work on the formalization and theory of deep neural networks and deep learning. https://arxiv.org/abs/2106.14587v1 is the first published preprint (more than 100 pages already) and it references to-be-published preprints and also whole book of papers.

I can handle the theory as a beginner, but this preprint is full of musings and is not formatted in the form of theorems, lemmas and proofs. etc.

So - can we have some discussions about it? Some elaboration? Reformulation?

I have asked the first question in Stackexchange https://math.stackexchange.com/questions/4189699/topos-and-stacks-of-neural-networks-how-to-understand-sentence-values-in-t

But there will be more and more such questions. I hope that preprint will have next versions and I hope to read especailly forthcoming reference: [BBG20] Jean-Claude Belfiore, Daniel Bennequin, and Xavier Giraud. Logical informa-tion cells. Internal technical report, Huawei, 2020.

But DNN theory (especially used for guidance in the selection of DNN architecture and discovery of deep learning algroithms) is so hot topic, that it is impossible to wait.

Actually - this is the moment that Gates and Allen experienced some 40 years ago - trillion$ business opportunity. And huge step for civilization as well, not just in Science.

]]>Anyone have any to contribute? https://plus.google.com/+NilesJohnson/posts/P47niHmk9eU

]]>Does this article make sense?

- Juven Wang, Family Puzzle, Framing Topology, c_ =24 and 3(E8)1 Conformal Field Theories: 48/16 = 45/15 = 24/8 =3.

It has a lot of nice math, but I have trouble grasping the logic of the arguments. If they make sense, it should be possible to explain them better.

]]>Looks interesting

- Darrick Lee, Harald Oberhauser,
*Random Surfaces and Higher Algebra*[arXiv:2311.08366].

We don’t yet have a ’random surface’ entry, a concept used by Polyakov in string theory.

]]>In talking and thinking about second derivatives recently, I’ve been led towards a different point of view on higher differentials. We (or Toby, really) invented cogerm differential forms (including cojet ones) in order to make sense of an equation like

$\mathrm{d}^2f(x) = f''(x) \mathrm{d}x^2 + f'(x) \mathrm{d}^2x$with $\mathrm{d}x$ an object that’s actually being squared in a commutative algebra. But it seems to be difficult to put these objects together with $k$-forms for $k\gt 1$ in a sensible way. Moreover, they don’t seem to work so well for defining differentiability: the definition of the cogerm differential in terms of curves is an extension of directional derivatives, but it’s not so clear how to ask that a function (or form) be “differentiable” in a sense stronger than having directional derivatives.

The other point of view that I’m proposing is to use the iterated tangent bundles instead of the cojet bundles: define a $k$-form to be a function $T^k X \to \mathbb{R}$. A point of $T^k X$ includes the data of $k$ tangent vectors, so an exterior $k$-form in the usual sense can be regarded as a $k$-form in this sense. And for each $k$, such functions are still an algebra and can be composed with functions on $\mathbb{R}$, so that we still have things like $\sqrt{\mathrm{d}x^2 + \mathrm{d}y^2}$ and ${|\mathrm{d}x|}$ as 1-forms.

However, the difference is in the differentials. Now the most natural differential is one that takes a $k$-form to a $(k+1)$-form: since $T^k X$ is a manifold (at least if $X$ is smooth), we can ask that a function $\omega:T^k X \to \mathbb{R}$ be differentiable in the sense of having a linear approximation, and if so its differential is a map $T^{k+1} X \to \mathbb{R}$ that is fiberwise linear.

I think it would make the most sense to denote this differential by $\mathrm{d}\otimes \omega$, because in general it is neither symmetric nor antisymmetric. For instance, if $\omega = x \, \mathrm{d}y$ is a 1-form, then $\mathrm{d}\otimes \omega = \mathrm{d}x \otimes \mathrm{d}y + x\, \mathrm{d}^2 y$, where $\mathrm{d}x \otimes \mathrm{d}y$ is the 2-form that multiplies the $x$-component of the first underlying vector of its argument by the $y$-component of the second underlying vector, and $\mathrm{d}^2 x$ is the 2-form that takes the $x$-component of the “second-order” part of its argument (which looks in coordinates like another tangent vector, but doesn’t transform like one). However, if $f$ is a twice differentiable function, then $\mathrm{d}\otimes \mathrm{d}f$ *is* symmetric, e.g. we have

So this amounts to regarding the second differential as a bilinear form (plus the $\mathrm{d}^2x$ bit) rather than a quadratic form, which appears to be necessary in order to characterize second-differentiability.

In general, we can *symmetrize* or *antisymmetrize* $\mathrm{d}\otimes \omega$, by adding or subtracting its images under the action of the symmetric group $S_{k+1}$ on $T^{k+1} X$. The first gives a result that we might denote $\mathrm{d}\omega$; while the second restricts to the exterior derivative on exterior forms, so we may denote it $\mathrm{d}\wedge \omega$. So in this way, the symmetric and the antisymmetric differential fit into the same picture.

I think this is basically the same approach taken in the reference cited by the answer here.

]]>A couple of people are working together on relating condensed mathematics to a kind of local cohesiveness. They speak of the concept of a fractured structure/fractured topos, presumably related to fracture squares.

Their talk notes: Qi Zhu, Fractured structure on condensed spaces; Nima Rasekh, What is a topological structure?.

]]>I am preparing an entry for the *Encyclopedia of Mathematical Physics 2nd ed*:

$\,$

$\,$

Early draft now available at that link.

Will be presenting this tomorrow at a CQTS-workshop on *Homotopy Theory and Applications*.

Comments are welcome.

]]>I’ve been using the book “Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy” by David Corfield as one of my primary resources and motivations for studying HoTT and I think I have found a fundamental mistake in some of the explanations for dependent pairs.

On page 45, the author discusses a type of dates, where the dependent pair is defined as $\sum_{m : Month} d : Day(m)$ . Sample elements of the type are given: $(February, 24)$ and $(August, 5)$. It is my understanding that in type theory, every element belongs to exactly one type. This presents a problem in this treatment of dates. If we consider the element $(August, 24)$, we now have the problem that $24$ seems to belong to both types $Day(February)$ and $Day(August)$. In other words, we have $24 : Day(February)$ and $24 : Day(August)$ in the same context. To remedy this, we could split up the $Day$ elements into their respective months, as in: $(February, 24_feb)$ and $(August, 24_aug)$, where $24_feb : Day(February)$ and $24_aug : Day(August)$. But now, we have no use for the first part of each pair as the second part carries all the information. It seems to me that the type of dates can’t be treated in an elegant way as the author intended (I can think of other practical ways, but they involve $Fin$ or nested dependent pairs).

I believe the same problem occurs on page 46, in the treatment of “day and hour”. The type is written in a dependent way, as $\sum_{d : Day} d : Hour(d)$ . The given sample elements are: $(Monday, 15:00)$ and $(Saturday, 09:00)$. Again, if we consider an element such as $(Tuesday, 15:00)$, we have the problem that $15:00$ belongs to $Hour(Monday)$ *and* $Hour(Tuesday)$. The author does explain that this is a special case where the types have no genuine dependence, but it is my understanding that the type should be properly defined as $\sum_{d : Day} d : Hour$ (or the equivalent, $Day \times Hour$). This way, $15:00$ simply belongs to the type $Hour$ in both elements.

Is my thinking in all this correct?

]]>Is there an intuitive reason why complex and quaternionic Kahler structures appear at any (appropriate) dimension in Berger’s theorem but not the octonionic Kahler structure? I would have expected to see $8n$-dimensional manifolds there.

]]>Does anyone of any connections that have been made between the notions of cybernetics, autopoeitic systems, or even George Spencer Browns Laws of Form, and homotopy theory or category theory?

I suppose right now such connections might be somewhat tenuous, as the latter is pretty philosophical, and the former is pretty formal, but it seems that there are perhaps connections to be made. Especially, with the notion of the distinctions in space that Spencer-Brown talks about, ideas of homology and homotopy occur to me. Also, possible connections with David Spivak’s ontology logs and various ideas about categorical database type things. I’m also wondering if there are any connections between the aforementioned more philosophical topics and internal logic of topoi, or even topological semantics.

Any references or ideas on this would be really appreciated, it’s just kind of a shot in the dark. Perhaps the question is not well formed.

Best, Jon Beardsley

]]>There are similar notions in the boundary fields already:

* Instituion in the logics and computer science (https://en.wikipedia.org/wiki/Institution_(computer_science))

* category of First order theories and subcategory of geometrical theories as defined by Olivia Caramell (in her book https://global.oup.com/academic/product/theories-sites-toposes-9780198758914?cc=it&lang=en&, while I wonder that she mentions that there is some controversy around it http://www.oliviacaramello.com/Unification/Controversy.html)

So - are there some results or maybe it is not possible or it is not interesting to pursue building such category. I have my goals of using such category in the formalization of deep learning and I wonder what is the status of its research? ]]>

Some time ago, I read an essay-like page (linked from SE) that listed perhaps a dozen structures outside of category theory (rings, vector spaces, etc), emphasizing how they were defined by rules with exceptions (like division by 0) and contrasting this with structures defined by universal rules. But I could never find the page again, despite searching nLab (and other sites) many times. Does anyone know I’m referring to? Or recognize the page I’m describing?

]]>Hello there, am an independent researcher interested in foundations of mathematics though without comprehensive mathematical background. Last year, it caught my attention that physics is formalized in richer kinds of homotopy theory in Science_Of_Logic. There is mention of universal algebra but they choose to work in a kind of synthetic homotopy theory but in my view continuing in universal algebra is more generic and could actually lead to a foundation of math. My math is bad but there could be some truth :

- A unity of opposites is between EM category on a monad and EM category on a comonad. It is subsumed by the ambient category via bireflection
- The bireflection has kleisli lifting as left adjoint inclusion and eilenberg-moore lifting as right adjoint inclusion(a crucial step yet am not so sure)
- The tower of adjoint modalities extends(by monadic decomposition) to any arbitrary ordinal as compared to the one on nlab which I believe is of length 12.
- A foremost assumption of mine is that any tower is equivalent to a fully faithful functor from kleisli category to eilenbergmoore category and that it is an equivalence( at least it is without overly-restrictive conditions). Also, dont forget it is still a tower of unity of opposites
- This now forms a 2-category with adjunctions as 0-cells, a square of adjunctions as 1-cell and transformations as 2-cells. The adjunctions in it are all tripple adjoints.
In my view, this should be formalized in enriched category theory so that every category turns out to be such a tower. The truth of this may be predicted using the idea that enriched categories are just free (co)completions and as such they are equivalent to eilenbergmoore categories, leading to my final step. 7.The 2-category above can be viewed as the category of all categories. The importance of this approach is that universal algebra is equivalent to inductive/recursive types and we can take advantage of this to inductively/recursively define the whole of mathematics and prove all its theorems in a big-bang kind of manner.

As a remark, I observe how bireflection seems to be equivalent to the physical notion of time, as defined in the nlab page, causal locality. This gives me the impression that math is inherently dynamic, that math actually exists objectively. Either way, what prevents a mathemetical theory from being real except causality ? I posted a related question on MathOverflow has there been any serious attempt at a circular foundation of mathematics. I at-least expect that the Hegelian pseudo-code can be formalized on such lines. I would appreciate it if some more advanced mathematician embarks on this or

**corrects me**. Thank you

We are finalizing this article here, if you have any comments, please drop a note:

**Twisted Cohomotopy implies M-theory anomaly cancellation**

**Abstract.** *We show that all the expected anomaly cancellations in M-theory follow from charge-quantizing the C-field in the non-abelian cohomology theory twisted Cohomotopy. Specifically, we show that such cocycles exhibit all of the following:*

*the half-integral shifted flux quantization condition,**the cancellation of the total M5-brane anomaly,**the M2-brane tadpole cancellation,**the cancellation of the $W_7$ spacetime anomaly,**the C-field integral equation of motion,**the C-field background charge.*

*Along the way, we find that the calibrated $N =1$ exceptional geometries (${Spin}(7)$, $G_2$, ${SU}(3)$, ${SU}(2)$) are all induced from the classification of twists in Cohomotopy. Finally we show that the notable factor of $1/24$ in the anomaly polynomial reflects the order of the 3rd stable homotopy group of spheres.*

Hi everyone,

I am new to the forum so pardon the possible selection of the wrong category under which to discsuss this topic. I have been studying Freyd’s algebraic theory of the reals in the past week. I have problems understanding his linear representation theorem that every scale can be embedded in a product of linear scales. To wit, I have two problems:

1) I thought that scale was linearly ordered under the relation of partial order defined by $a \multimap b = \top$. So the embedding should be trivial.

2) In the proof, he shows that the meet $y \vee x$ is strictly smaller than $\top$ in a scale that is an SDI (an algebra is an SDI “if whenever it is embedded into a product of algebras one of the coordinate maps is itself an embedding”). This I understand. But he also says that from this follows the disjonction property that $x \multimap y \vee y \multimap x = \top$ in an SDI scale. Now, I can’t see how this follows.

Thank you for your help,

Jeff.

]]>The other day on the preprint server

- Michael Freedman and Matthew Hastings in [arXiv:2304.01072, p. 1]

are:

asking readers to help invent the upper right corner of this “push out”:

$\array{ \mathclap{\text{Quantum information}} \\ \mathllap{ {}^{\text{Add tensor}} _{\text{structure}} } \Big\uparrow \\ \text{Linear algebra} &\underset{\text{Add parameters}}{\longrightarrow}& \text{Bundle theory} }$

$\,$

In reply, we want to say that this pushout is “*parameterized quantum information theory*” exhibited by the category VectBund of vector bundles equipped with its external tensor product of vector bundles, the 1-categorical semantics for dependent linear type theory which exhibits it as a classically controlled quantum language. (K-theory would come in only as a second step of group completion…)

To make this precise, at least in the case that the parameters form discrete sets, we want to say that there is a pushout diagram of the following form, in a suitable ambient (2,1)-category:

$\array{ \big( Vect, \otimes \big) &\longrightarrow& \big( Vect_{Set} , \sqcup , \boxtimes \big) \\ \big\uparrow && \big\uparrow \\ Vect &\longrightarrow& \big( Vect_{Set}, \sqcup \big) }$In order to make sense of this diagram and to see that it is indeed a pushout, we need an ambient (2,1)-category inside which we have 1. categories, 2. monoidal categories, 3. co-cartesian cateories and 4. distributive monoidal categories, so that functors may go from categories with some number of monoidal structures to categories with at least these monoidal structures, maybe more.

Take that (2,1)-category to be the (2,1)-Grothendieck construction on the evident square of forgetful functors.

$\mathbf{C} \;\; \colon \;\; \array{ (1,0) &\longrightarrow& (1,1) \\ \big\uparrow && \big\uparrow \\ (0,0) &\longrightarrow& (1,0) } \;\;\;\; \mapsto \;\;\;\; \array{ MonCat &\longleftarrow& DistMonCat \\ \big\downarrow && \big\downarrow \\ Cat &\longleftarrow& CoCartCat }$Here in $\int \mathbf{C}$ the above square is a pushout, as desired. I think.

Have made a first note about this at *VectBund* in a new section *Amalgamation of monoidal and parameter structures*. For the moment this is a little experimental, will try to polish this up.

Alain Connes brought out a book containing a dialogue with psychoanalyst Patrick Gauthier-Lafaye called À l’ombre de Grothendieck et de Lacan. Developing Lacan’s ’The unconscious is structured like a language’, the thesis of the book is

The unconscious is structured like a topos.

I found the book very light on details. Attention is given to the idea of a classifying topos for a geometric theory encoding what Lacan calls the fundamental fantasy.

Surprisingly, there’s nothing on the dynamics of therapy, which in this story ought to correspond to modifying the topos/refining the theory. That got me wondering outside of anything psychoanalytic how to get the classifying topos concept to relate to Aufhebung, level of a topos, etc. Whenever we have some resolution of an opposition, should we be able to describe it via theory extension? This from Aufhebung suggests so

We can think of the inclusion of the sheaf category of a lower level into the higher sheaf category as an

analyticrelation between the concepts involved: when viewed as a relation between the geometric theories classified by the respective subtoposes an inclusion relation corresponds indeed to an unpacking of the richer theory of the smaller subtopos e.g. the subtopos corresponding to the theory of local rings is included in the topos corresponding to the theory of rings which on the conceptual side is spelled out asa local ring is a ring, or, the concept ’local ring’ implies the concept ’ring’. So the passage from subtopos to including supratopos corresponds to an unfolding of the concepts implied in the subtopos concept.

So if $\empty\dashv \ast$ corresponds to the inconsistent geometric theory. what should we say for $\flat\dashv \sharp$?

]]>I am reading https://www.cambridge.org/core/books/abs/new-spaces-in-mathematics/homotopy-type-theory-the-logic-of-space/D13957048F50112B531698F6FB6269EB and thinking about this.

Of course, any individual effort in the mathematics that uses categorical tools and any research in category theory, is one step of doing this program already. But I just wanted to know about references that consider this as large scale, intentional and systematic effort? ]]>

From the other side there is relation/duality between algebra and geometry https://ncatlab.org/nlab/show/duality+between+algebra+and+geometry but it can not be complete if this duality does not extends to the algebra that would correspond to the higher order logic.

I am just trying to put all this in order - can higher algebra be of help for the algebraization of HOL. Yes or No? If no, then what to do with this gap (no algebra - geometry duality for HOL-level expressions)?

It would be nice to establish this Rosetta stone:

computing/type theories <-> algebra <-> categories <-> geometry <-> physics

for the HOL as well.

If there is some nice text about this I wold be thankful to know about it and read it. Maybe Jacob Lurie is working on this currently. No new papers from him for the past few years. ]]>