julesh on Nostr: I just implemented function types in Aptwe, aka the monoidal closed structure of ...

I just implemented function types in Aptwe, aka the monoidal closed structure of lenses. Here's the interpreter cases corresponding to hom introduction and elimination, which correspond to the bidirectional semantics of (linear) lambda abstraction and function application
https://github.com/CyberCat-Institute/Aptwe/blob/main/src/Interpreter/Terms.idr