--- Day changed Wed Jan 24 2018
doliotomjack: The main thing missing is a nice way of specifying coinductive families like there is for inductive families.24/01 15:33
dolioInstead of explicitly talking about identity types.24/01 15:33
nkaretnikovWould it be a huge pain to go through Aluffi’s Algebra: Chapter 0 in Agda? I guess it’d require like 100 times  more effort. Or can this be simplified somehow, so I don’t need to start from scratch? Can copumpkin’s categories repo be helpful here or maybe something else?24/01 22:16
nkaretnikovI did a few chapters of Software Foundations in Coq, so I’m not new to theorem proving, but I’m still pretty much a beginner. I also did a few simple proofs in Agda. My main motivation here as a self-learner is not to bullshit myself while proving things. I attempted to solve some problems this way from a discrete mathematics course, but I quickly got overwhelmed by the number of things I needed in order to get24/01 22:26
nkaretnikovgoing. This time I’d rather stand on someone else’s shoulders.24/01 22:26
mieteknkaretnikov: you should look at https://wenkokke.github.io/sf/24/01 22:29
mieteknkaretnikov: or a book on Agda that is not a work-in-progress24/01 22:29
mieteknkaretnikov: https://dl.acm.org/citation.cfm?id=284131624/01 22:29
mieteknkaretnikov: or a book that was written for the purpose of being formalisable24/01 22:30
mieteknkaretnikov: https://www.amazon.co.uk/Type-Theory-Formal-Proof-Introduction/dp/110703650X24/01 22:30
mieteknkaretnikov: I don’t know Aluffi’s Algebra, but unless it’s constructive mathematics, you’re going to have a bad time24/01 22:30
mieteknkaretnikov: trust my 9000 half-started repos24/01 22:31
nkaretnikovI’ll check these out, but I don’t feel it really answers my question. My main motivation is to through a specific book, which I like because it’s self-contained. I just want something better than TeX.24/01 22:32
nkaretnikovYeah, I realize the amount of effort required, but still.24/01 22:33
mietekdon’t let me stop you24/01 23:35
mietekthe best way to learn is by trying and failing until you succeed24/01 23:35
mieteknkaretnikov: I’m basically doing the same thing, except it’s not about a book for me24/01 23:37
mieteknkaretnikov: feel free to join ##dependent and take up the fight24/01 23:38

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!