Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Friday, 13-Dec-2024 05:30:24 JST julesh

   After 5 hours sleep and a 6 hour meeting, on the flight home I apparently have invented coterms while thinking about pattern matching 🤷♀️

   • Embed this notice
     Boarders (boarders@mathstodon.xyz)'s status on Friday, 13-Dec-2024 05:39:09 JST Boarders

     in reply to

     @julesh is that different than terms of a codata type (type that you interact with as codomains)?

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Friday, 13-Dec-2024 05:43:52 JST julesh

     in reply to

     • Boarders

     @boarders I think it's a different thing, but it wouldn't surprise me much if they're closely related

   • Embed this notice
     Zanzi @ Monoidal Cafe (zanzi@mathstodon.xyz)'s status on Friday, 13-Dec-2024 05:44:59 JST Zanzi @ Monoidal Cafe

     in reply to

     • Boarders

     @julesh @boarders they are, once you have terms + coterms for both data and codata, you get an involutive duality between them. thats what im working on for Jermaine right now