511d564a55
Foundation.Meta gains an 8-constructor MetaCTerm inductive that mirrors the cubical CTerm's generic shape (ident/sym/app/lam/plam plus dedicated comp/transp arms; cubical-specific operators encode via .ident-headed .app chains). MetaArtifact picks up a .cterm arm for structure-preserving artifact content. MetaPosition gets an Option Lean.Name binder field so the dim-binder of a comp/transp can be threaded structurally instead of folded into the classifier. These additions back the cubical-bridge's Embed.lean overhaul: a real coreflection between the cubical universe (CType/CTerm/FaceFormula/ DimExpr) and the meta-mirror, with partial inverses and per-constructor round-trip theorems. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
11 lines
357 B
Text
11 lines
357 B
Text
/-
|
|
Infoductor — generic methodology / repo-organization library.
|
|
|
|
Root umbrella module. Imports each sub-library so that downstream
|
|
consumers can `import Infoductor` to bring everything into scope,
|
|
or pick specific sub-modules via fully qualified imports for
|
|
tighter compile-time graphs.
|
|
-/
|
|
|
|
import Infoductor.Foundation
|
|
import Infoductor.Test
|