Showing cs.LOShow all
2 papers · 1 filter
cs.LO2024
(Co)condition hits the Path
Tesla Zhang, Valery Isaev
We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax…
cs.LO2023
Two tricks to trivialize higher-indexed families
Tesla Zhang
The conventional general syntax of indexed families in dependent type theories follow the style of "constructors returning a special case", as in Agda, Lean, Idris, Coq, and probab…