Dynamic intermediates WIP; continuing in literate-execution

.gitignore

@@ -9,6 +9,14 @@
 *.out
 *.fdb_latexmk
 *.fls
+*.loc
+*.soc
 *.pdf
 *.zip
 *.DS_Store
+*.fdb_latexmk
+*.fls
+
+# Claude Code local state (memory, transcripts, and git worktrees it manages)
+/.claude/
+agda/_build/

Makefile

@@ -1,9 +1,10 @@
-.PHONY: main notes clean submit arXiv # otherwise confused by folders with the same name
+.PHONY: main notes mu-types clean submit arXiv # otherwise confused by folders with the same name
 
 default: main
 
 main: main.pdf
 notes: notes.pdf
+mu-types: mu-types.pdf
 
 # -out2dir unsupported on default Mac installation
 LATEXMK_OPTS:=-output-format=pdf -outdir=_latex
@@ -18,6 +19,15 @@ main.pdf: main.tex $(MAIN_DEPS)
 	cp _latex/main.pdf .
 	@! grep -qE "LaTeX Warning: There were undefined references\.|natbib Warning: There were undefined citations\." _latex/main.log
 
+MU_TYPES_DEPS:=$(wildcard mu-types/*.tex) $(wildcard fig/*.tex) macros.tex bib.bib
+
+mu-types.pdf: mu-types.tex $(MU_TYPES_DEPS)
+	latexmk $(LATEXMK_OPTS) mu-types
+	cd _latex && bibtex mu-types
+	latexmk $(LATEXMK_OPTS) -g mu-types
+	cp _latex/mu-types.pdf .
+	@! grep -qE "LaTeX Warning: There were undefined references\.|natbib Warning: There were undefined citations\." _latex/mu-types.log
+
 NOTES_DEPS:=$(wildcard notes/*.tex) $(wildcard fig/*.tex) macros.tex bib.bib
 
 notes.pdf: notes.tex $(NOTES_DEPS)
@@ -66,3 +76,4 @@ clean:
 	rm -f suppl-submit.zip
 	rm -f arXiv.zip
 	rm -f notes.pdf
+	rm -f mu-types.pdf

agda/src/approx-numbers.agda

@@ -17,7 +17,7 @@ open import categories using (HasTerminal; Category)
 
 import fam
 
-open import Data.Rational using (ℚ; _≤_; _⊔_; _⊓_; _+_; _-_; 0ℚ; -_; Positive; _*_; _÷_; NonZero)
+open import Data.Rational using (ℚ; _≤_; _⊔_; _⊓_; _+_; _-_; 0ℚ; 1ℚ; -_; Positive; _*_; _÷_; NonZero)
 open import Data.Rational.Properties
   using (
     ≤-refl; ≤-trans; ⊓-glb; ⊔-lub; p⊓q≤p; p⊓q≤q; +-mono-≤; module ≤-Reasoning; +-comm; ≤-reflexive; +-assoc;
@@ -335,6 +335,20 @@ module Galois where
   zero-mor .famf .transf _ ._⇒g_.left⊣right {tt} {< x >} .proj₂ _ = x .l≤q , x .q≤u
   zero-mor .famf .natural e .right-eq .eqfun _ = (liftS ≤-refl , liftS ≤-refl) , liftS ≤-refl , liftS ≤-refl
 
+  one-mor : Fam.Mor 𝟙 ℚ-intv
+  one-mor .idxf .prop-setoid._⇒_.func _ = 1ℚ
+  one-mor .idxf .prop-setoid._⇒_.func-resp-≈ _ = liftS ≡-refl
+  one-mor .famf .transf _ ._⇒g_.right ._=>_.fun _ =
+    < record { lower = 1ℚ ; upper = 1ℚ ; l≤q = liftS ≤-refl ; q≤u = liftS ≤-refl } >
+  one-mor .famf .transf _ ._⇒g_.right ._=>_.mono _ = liftS ≤-refl , liftS ≤-refl
+  one-mor .famf .transf _ ._⇒g_.left ._=>_.fun _ = tt
+  one-mor .famf .transf _ ._⇒g_.left ._=>_.mono _ = tt
+  one-mor .famf .transf _ ._⇒g_.left⊣right {tt} {y} .proj₁ _ = tt
+  one-mor .famf .transf _ ._⇒g_.left⊣right {tt} {bottom} .proj₂ _ = tt
+  one-mor .famf .transf _ ._⇒g_.left⊣right {tt} {< x >} .proj₂ _ = x .l≤q , x .q≤u
+  one-mor .famf .natural e .right-eq .eqfun _ = (liftS ≤-refl , liftS ≤-refl) , liftS ≤-refl , liftS ≤-refl
+  one-mor .famf .natural e .left-eq .eqfun _ = tt , tt
+
 ------------------------------------------------------------------------------
 -- Conjugate (forward) interpretation
 module Conjugate where
@@ -628,6 +642,24 @@ module Conjugate where
   zero-mor .famf .natural e ._≃c_.left-eq ._≃J_.eqfunc ._≃m_.eqfun bottom = tt , tt
   zero-mor .famf .natural e ._≃c_.left-eq ._≃J_.eqfunc ._≃m_.eqfun < x > = tt , tt
 
+  one-mor : Fam.Mor 𝟙 ℚ-intv
+  one-mor .idxf .prop-setoid._⇒_.func _ = 1ℚ
+  one-mor .idxf .prop-setoid._⇒_.func-resp-≈ _ = liftS ≡-refl
+  one-mor .famf .transf _ ._⇒c_.right ._=>J_.func ._=>_.fun tt = bottom
+  one-mor .famf .transf _ ._⇒c_.right ._=>J_.func ._=>_.mono {tt} {tt} _ = tt
+  one-mor .famf .transf _ ._⇒c_.right ._=>J_.∨-preserving = tt
+  one-mor .famf .transf _ ._⇒c_.right ._=>J_.⊥-preserving = tt
+  one-mor .famf .transf _ ._⇒c_.left ._=>J_.func ._=>_.fun _ = tt
+  one-mor .famf .transf _ ._⇒c_.left ._=>J_.func ._=>_.mono _ = tt
+  one-mor .famf .transf _ ._⇒c_.left ._=>J_.∨-preserving = tt
+  one-mor .famf .transf _ ._⇒c_.left ._=>J_.⊥-preserving = tt
+  one-mor .famf .transf _ ._⇒c_.conjugate .proj₁ _ = tt
+  one-mor .famf .transf _ ._⇒c_.conjugate {x = tt} {y = bottom} .proj₂ _ = tt
+  one-mor .famf .transf _ ._⇒c_.conjugate {x = tt} {y = < _ >} .proj₂ _ = tt
+  one-mor .famf .natural e ._≃c_.right-eq ._≃J_.eqfunc ._≃m_.eqfun tt = tt , tt
+  one-mor .famf .natural e ._≃c_.left-eq ._≃J_.eqfunc ._≃m_.eqfun bottom = tt , tt
+  one-mor .famf .natural e ._≃c_.left-eq ._≃J_.eqfunc ._≃m_.eqfun < x > = tt , tt
+
   add-mor : Fam.Mor (ℚ-intv ⊗ ℚ-intv) ℚ-intv
   add-mor .idxf .prop-setoid._⇒_.func (q₁ , q₂) = q₁ + q₂
   add-mor .idxf .prop-setoid._⇒_.func-resp-≈ (liftS ≡-refl , liftS ≡-refl) = liftS ≡-refl

agda/src/cartesian-monoidal.agda

@@ -33,7 +33,7 @@ _×m_ = prod-m
 ×m-comp : ∀ {x₁ x₂ y₁ y₂ z₁ z₂}
           (f₁ : y₁ ⇒ z₁) (f₂ : y₂ ⇒ z₂) (g₁ : x₁ ⇒ y₁) (g₂ : x₂ ⇒ y₂) →
           ((f₁ ∘ g₁) ×m (f₂ ∘ g₂)) ≈ ((f₁ ×m f₂) ∘ (g₁ ×m g₂))
-×m-comp = pair-functorial
+×m-comp = prod-m-comp
 
 -- Associativity
 ×-assoc : ∀ {x y z} → ((x × y) × z) ⇒ (x × (y × z))