Post AhoK0PJFK6PdcXiW1I by MartinEscardo@mathstodon.xyz
 (DIR) More posts by MartinEscardo@mathstodon.xyz
 (DIR) Post #AhoK0MzJxDHmQANZgW by MartinEscardo@mathstodon.xyz
       2024-05-03T22:50:06Z
       
       0 likes, 0 repeats
       
       I want a proof assistant in which category theory is built-in, rather than a library.
       
 (DIR) Post #AhoK0P54Ap4OuZ5Buy by MartinEscardo@mathstodon.xyz
       2024-05-04T18:26:08Z
       
       0 likes, 0 repeats
       
       My point, perhaps, is the following.Whenever I formalize something, I want the readers of the formalization to be able to understand what I have done by reading the code.At present, there are lots of places in TypeTopology where there is categorical reasoning, without officially invoking categories.I would like (1) the categorical reasoning to be officially recorded in the development (even though categories are not used officially), and (2) the proof assistant to support categorical reasoning in its interactive mode, as in the case of Agda.
       
 (DIR) Post #AhoK0PJFK6PdcXiW1I by MartinEscardo@mathstodon.xyz
       2024-05-04T14:19:42Z
       
       0 likes, 0 repeats
       
       I think my point is that it has been advocated in the past that category theory can be regarded as a foundation, at least for those of us who tend to think categorically. It would be nice to have a proof assistant based on category theory.
       
 (DIR) Post #AhpGcMsWbXv8QW1XgO by mc@mathstodon.xyz
       2024-05-04T08:27:06Z
       
       0 likes, 0 repeats
       
       @MartinEscardo yep I keep saying this to proof assistant salespeople lol
       
 (DIR) Post #AhpGcNa7zQnabkQMe8 by zanzi@mathstodon.xyz
       2024-05-05T19:47:32Z
       
       0 likes, 0 repeats
       
       @mc @MartinEscardo the devil is in the details!
       
 (DIR) Post #AhxYbmxdUvuVTBy2fQ by MartinEscardo@mathstodon.xyz
       2024-05-05T19:54:26Z
       
       0 likes, 0 repeats
       
       @zanzi @mc This is fine with me, if you define the devil to be (the rather kind) designers and developers of proof assistants.
       
 (DIR) Post #AhzJ55SGbfV8H9AB4y by ToucanIan@mathstodon.xyz
       2024-05-05T00:14:00Z
       
       0 likes, 0 repeats
       
       @MartinEscardo something different in mind than rzk?
       
 (DIR) Post #AhzJ56nvacQEScIzTs by MartinEscardo@mathstodon.xyz
       2024-05-05T18:27:35Z
       
       0 likes, 0 repeats
       
       @ToucanIan I want to be able to say to my proof assistant something like this."Now notice that the gadgets I am considering form a category, and that I have proved that there is a freely generated gadget over any set of generators (maybe with relations). Therefore I get a monad."At the moment, you can do that, with or without using category theory explicitly in a proof assistant, but in both cases there is a lot of required boiler plate to do that.Moreover, whether you do this with or without a library for categories, you have to repeat all this when you consider new mathematical gadgets.
       
 (DIR) Post #AhzJ57l82VmFQE0Gky by codyroux@mathstodon.xyz
       2024-05-05T18:50:33Z
       
       0 likes, 0 repeats
       
       @MartinEscardo @ToucanIan how do you want to specify "this is the free Foo"?
       
 (DIR) Post #AhzJ58asw5B40kDbQe by MartinEscardo@mathstodon.xyz
       2024-05-05T20:00:48Z
       
       0 likes, 0 repeats
       
       @codyroux @ToucanIan We have a map η : X → Free-Foo X such that every function f : X → A from X to a Foo A extends uniquely to a Foo-map f' : Free-Foo X → A along η.