type-theory

An OpenClaw skill for deep type theory competence.

"A type is a promise about the shape of a thing — a contract between what exists and what can be done with it."

What This Skill Provides

This skill equips an AI agent with comprehensive type theory knowledge and the ability to:

• Understand type theory from historical foundations (Russell, Church, Curry-Howard) through frontier research (HoTT, cubical type theory)
• Classify anything — data, concepts, propositions, programs — using type-theoretic structures
• Order and organize domains via subtyping lattices, universe hierarchies, and refinement chains
• Manipulate types: construct, combine, transform, inhabit, and prove properties
• Explain type theory to anyone, from complete beginners to working mathematicians, using calibrated metaphors, analogies, and allegories
• Translate between formal type structures and intuitive/narrative descriptions
• Apply type-theoretic thinking to practical programming, system design, and knowledge organization

Structure

type-theory/
├── SKILL.md                        # Main skill file (load this)
├── knowledge/
│   ├── foundations.md               # Lambda calculus, logic, historical origins
│   ├── type-systems.md             # Comprehensive taxonomy of type systems
│   ├── curry-howard.md             # Propositions as types, computational trilogy
│   ├── advanced.md                 # HoTT, cubical, modal, linear, effects
│   └── practical.md               # Types in real programming languages
├── metaphors/
│   ├── core-metaphors.md           # Master metaphor toolkit (shapes, machines, etc.)
│   ├── allegories.md               # Extended narrative allegories for deep concepts
│   └── analogies.md                # Cross-domain analogy tables (biology, law, music, etc.)
├── operations/
│   ├── classify.md                 # How to classify things using type theory
│   ├── order.md                    # How to order/organize using type theory
│   └── manipulate.md              # Type-level operations and transformations
└── references/
    └── bibliography.md             # Annotated reading list with learning paths

Usage

As an OpenClaw Skill

Add this to your agent's skills directory and reference it in your agent config. The SKILL.md contains a compressed knowledge base sufficient for most tasks. Supporting files provide deeper coverage when needed.

Reading the Knowledge Files

Each knowledge file is self-contained and can be read independently:

If you need...	Read...
Historical context and foundations	knowledge/foundations.md
A taxonomy of all type system features	knowledge/type-systems.md
The Curry-Howard correspondence explained	knowledge/curry-howard.md
Advanced/frontier topics (HoTT, effects, etc.)	knowledge/advanced.md
How types work in real programming languages	knowledge/practical.md

Using the Metaphor Toolkit

If your audience is...	Use...
Complete beginners	metaphors/core-metaphors.md (physical metaphors)
Programmers	metaphors/analogies.md + knowledge/practical.md
Needs a deep narrative explanation	metaphors/allegories.md
From a specific domain (biology, law, music...)	metaphors/analogies.md (domain-specific tables)

License

AGPL-3.0-or-later

Author

Kyvero Vexus Corporation (KVC)