Coinductive types: a ν-scheme over polynomial codes, with dischargeable coinduction - #43

Merged

Russoul merged 7 commits into

mainfrom

nova-ext-codata

Aug 3, 2026

Commits on Aug 3, 2026

Coinductive types: ν at one-hole polynomial codes, with corec β and coinduction η
Russoul
committed
b84cd04
Coinductive types end to end: kernel, elaborator, corpus streams
Russoul
committed
2c5fdba
Observational stream equality in Ω; map-id and map-fusion by induction on observations
Russoul
committed
fba9e4c
Bisimilarity as the impredicative gfp in Ω; equivalence with the observational form
Russoul
committed
9858fcc
Coinduction discharges: el-nu-coind via the relator, coind proofs, bisimilarity reflects into equality
Russoul
committed
2a97021
coind at every polynomial: prop exposure by hypothesis rewriting; conat's ∞ = ∞+1
Russoul
committed
425291e
Evaluation tests: take N of a colist — finite with Z-padding, and the infinite naturals
Russoul
committed
3dd0fbe