effectful-hott

This repository explores Homotopy Type Theory with computational effects, grounded in realizability semantics and the Effective Topos.

The project investigates how effectful computation (e.g. partiality, exceptions, state, or logging) can be integrated into HoTT while preserving constructive meaning and homotopical structure. The approach is categorical and semantic in nature, using internal languages of toposes and realizability models as foundational tools.

Contents

• proposal/
  A research proposal outlining the motivation, background, and goals of effectful HoTT via realizability.

• agda/
  Agda formalizations exploring effectful type-theoretic constructions, paths, and semantics.

• notes/ (optional)
  Informal notes, sketches, and supporting material.

Themes

• Homotopy Type Theory
• Realizability and the Effective Topos
• Computational effects and constructive semantics
• Categorical logic and internal languages
• Agda formalization

Status

This is an active research repository. The Agda code is exploratory and evolving.

License

TBD