Post #2103989

2026-04-17 23:32 UTC

I finally found a way to mechanise synthetic Tait computability in Agda where restricting along the syntactic open computes definitionally.. without relying on cubical cofibrations. It amounts to working completely within an indexed universe whose base is open-modal and fibers are closed-modal. Has this been observed before? (full code soon) cc @trebor @jonmsterling @olynch

Replies (5)

@constantine@types.pl 2026-04-20 11:20

@jonmsterling@mathstodon.xyz @olynch@mathstodon.xyz @HarrisonGrodin@mathstodon.xyz Here it is: https://github.com/kontheocharis/synthetait

Open ##2590495
@jonmsterling@mathstodon.xyz 2026-04-18 06:06

@constantine@types.pl @trebor@types.pl @olynch@mathstodon.xyz I did write this out in a draft note several years ago, but I never tried it in Agda. This is really cool!

Open ##2590496
@mevenlennonbertrand@lipn.info 2026-04-18 07:32

@constantine@types.pl Iirc @HarrisonGrodin@mathstodon.xyz was trying to do something like that in January, tagging him in case it's of interest!

Open ##2590497
@olynch@mathstodon.xyz 2026-04-18 08:50

@constantine@types.pl @trebor@types.pl @jonmsterling@mathstodon.xyz Really cool! I wish I knew more Agda so I could understand this better...

Open ##2590498
@trebor@types.pl 2026-04-20 23:21

@constantine@types.pl Can we also postulate fracture by saying every (A : Set) is isomorphic to the Sigma type over a pair of (A^○ : Tyᵇ, A^● : Tyᶠ A^○)? This should make inductive types a little easier to deal with.

Open ##2590500