sheafification as a higher inductive type (HIT) — Re: [Metamath] Searching set.mm

[moz...@gmail.com]

Hi Igor,

the emdash proof assistant implements a formula-search query language
similar as the Lambdapi logical framework:
https://lambdapi.readthedocs.io/en/latest/query_language.html and I am
often amazed at whether the lack of "usability" of Metamath either is
by design or is work-in-progress...

In fact, I'd like to announce a significant further update to the
emdash proof assistant and the companion book «Functorial Type Theory:
Univalent Foundations of Mathematics»:

https://doi.org/10.5281/zenodo.21544186
https://github.com/hotdocx/emdash

- A new computational-and-internalized implementation of sheaves and
sheafification as a higher inductive type/category (HIT), affine
schemes, schemes, and the projective line.

This consolidates my earlier key insight (communicated in an Oct 4,
2024 thesis review to MAX Zeuner) to employ the "invertibility SIEVE
D_U(s)" rather than MAX Zeuner's «Univalent Foundations of
Constructive Algebraic Geometry».

- A new "usability" TypeScript elaborator for standard syntax with
binders and variables (interpreted functorially/naturally) that
compiles to two logical framework backends: TypeScript/emdash and
LambdaPi/emdash.


— Christopher


TECHNICAL APPENDIX
==================

The basic construction underneath the emdash kernel/book is the
ω-categorical directed dependent hom. For a category-valued family `E
: K ⊢ Cat`, and `x : K`, `u : E[x]`, emdash forms

```
homd_E(x,u)
: Π(y : K^op), E[y^-] ⊢_[y] (Hom_K(x,y)^op ⊢ Cat),
```

whose value at `y`, `v : E[y]`, and `f : x → y` is
`Hom_{E[y]}(E[f](u),v)`. It organizes arrows in Sigma totals:

```
Hom_{ΣE}((x,u),(y,v))
= Σ(f : x → y), Hom_{E[y]}(E[f](u),v).
```

For a category `Z`, put

```
x ↓ Z = Σ(y : Z), Hom_Z(x,y).
```

The reflexive object is `(x,id_x)`; write its canonical arrow to
`(y,p)` simply as `p`. Thus, for

```
E : (x ↓ Z) ⊢ Cat
u : E[(x,id_x)],
```

directed arrow induction has the compact form

```
Ind_x(E,u) : Π(a : x ↓ Z), E(a)

Ind_x(E,u)(y,p) = E(p)(u).
```

For `E[(y,p)] := Rep_Z(y) ⊢ Rep_Z(x)` and reflexive datum `id`, it computes
ordinary composition:

```
Ind_x(E,id)[(y,p)][z][q] ↝ q ∘ p.
```

The current TypeScript elaborator lets the same internal operations be
authored with familiar bound variables—e.g. `λ^f x. (H x) (K x)` and
displayed/natural variants—then lowers them to explicit emdash Core.
The Core is checked by TypeScript/emdash; selected judgments are also
emitted to the authoritative Lambdapi/emdash backend for conformance.

---

The first concrete directed HIT is opaque rather than defined by its
desired endomorphism type:

```
constant WalkingEnd : Cat

base : Obj(WalkingEnd)
loop : Hom_WalkingEnd(base,base).
```

Its whole recursor sends `base` to `ℕ` and `loop` to successor:

```
Code := rec_WalkingEnd(Cat_cat; ℕ,Succ)

Code[base] = ℕ
Code[loop] = Succ.
```

For a based arrow `p`, define `encode_x(p)=Code[p](0)`. In the other direction,

```
power(0) = id_base
power(n+1) = loop ∘ power(n),
```

and a spiral coherence

```
Rep_base[loop] ∘ power ⇒ power ∘ Succ
```

feeds the contextual displayed eliminator. It returns a coherent
decoder and a directed normalization cell

```
p → decode_x(encode_x(p)).
```

One-dimensionality then gives

```
power(encode_base(p)) = p
encode_base(power(n)) = n

Hom_WalkingEnd(base,base) ≃ ℕ
(underlying carriers).
```

The result is `ℕ`, not `ℤ`, because `loop` is directed and has no right inverse.

At the next hom level, Eckmann–Hilton gives

```
2End_B(x) = Hom_{Hom_B(x,x)}(id_x,id_x)

α,β : 2End_B(x)
β · α = β * α = α · β,
```

where `·` is vertical composition and `*` is horizontal composition.

---

Cat-valued profunctors are directed families

```
Prof(A,B) = A^op × B ⊢ Cat.
```

Emdash includes representables, endpoint reindexing, shaped cells,
selected tensor/co-Yoneda/internal-hom operations, and weighted
universal comparisons. For a weight `W : J ⇸ J′`, a selected
`W`-weighted colimit `C` of `F : J → A`, and an adjunction `S ⊣ R`,

```
W-Colim_A(F,C)
⇒ W-Colim_B(S ∘ F,S ∘ C).
```

This is obtained from right-adjoint preservation of weighted limits by
opposite normalization, rather than by duplicating the proof.

---

For local geometry, let `O : K^op ⊢ CommRing`, `s : O(U)`, and `p : V
→ U`. Define the invertibility sieve

```
D_U(s)(p) := Unit_{O(V)}(p^*s).
```

It is stable under every refinement of `p`. Thus the primary object is
invertibility's sieve, not a previously chosen invertibility open. A
compact
open may represent this sieve in a coherent/posetal setting, but
representability is an additional theorem.

For affine tests,

```
D_R(f)(S) = Σ(h : R → S), Unit_S(h(f)),

Hom_CommRing(R[1/f],S) ≃ D_R(f)(S)
```

for every supplied localization and test ring `S`. Moreover `D_R(fg) ≃
D_R(f) ∩ D_R(g)` pointwise, while finite unit-ideal families generate
the big Zariski topology.

For a covering sieve `R` on `U` and a Cat-valued presheaf `P`,

```
Match_P(R) = Hom(R̂,P)
Sect_P(U) = Hom(yU,P).
```

Sheafhood says that restriction from sections to matching families is
an equivalence. Direct cover completion constructs sheafification by a
categorical HIT with

```
return : P → aP
glue : Match_{aP}(R) → Sect_{aP}(U)
silent : glue ∘ restriction = id,
```

followed by a recursor and whole uniqueness:

```
Hom(aP,Y) ≃ Hom(P,Y)

a : Psh_Cat(K) ⇄ Sh_Cat(K,J) : i,
a ⊣ i.
```

The construction lives directly in ordinary categorical
semantics—actual presheaves, sieves, sites, and functors—made
computationally internal by the surrounding TypeScript or Lambdapi
logical framework. It does not require a separate modal type theory.

The affine layer connects `D(f)`, localization, intersections, finite
covers, the coordinate presheaf, and an assumption-explicit reflective
structure sheaf. A global-first binary scheme presentation retains one
ringed object, one covering sieve, two affine generators, local-ring
behavior, and inherited restrictions and overlaps. On a supplied
projective-line presentation, the actual overlap carries the Laurent
changes

```
t ↦ u⁻¹,
u ↦ t⁻¹.
```

This is a checked site-relative/projective-line capability, not yet an
atlas-first gluing theorem. Graded rings, homogeneous localization,
`Proj`, general projective space `Pⁿ`, and non-affineness remain
future work.