search

vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Prove !⟷₁⟷₂ in Syntax #88

Open inexxt opened 3 years ago

vikraman commented 3 years ago

The remaining TODOs can be proved using Joyal-Street propositions 1.1 and 2.1.