⇑W⇓ with proofs
Use Marcell van Geest's work for defining in a neat way encoding schemes for Agda types into hardware types, and have the proofs available for round trip properties.
Use Marcell van Geest's work for defining in a neat way encoding schemes for Agda types into hardware types, and have the proofs available for round trip properties.