[%] Lambek's theorem agda로 증명함

[다믜(damhiya)]

Lambek's theorem이 뭐냐?

=> https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor
(대충 카테고리 이론이랑 타입이론에서 inductive type 다룰 때 나오는 정리)

증명은 어딧냐?

=> https://github.com/damhiya/AgdaCategoryTheory/blob/master/F-algebra.agda

[+(223.62)]

개추

[++++++++(223.62)]

개추

[익명(106.102)]

천재가 되버린거냐고 오이 ㅇㅅㅇ

[다믜(damhiya)]

[Riey(rerereq)]

kime 수식기능 써먹고 있음?

[다믜(damhiya)]

ㄴㄴ 저런거는 emacs에서 제공하는걸로 입력하지

[+(223.62)]

Agda-mode는 자체 수식 입력 단축키가 있어서 필요 없을 수도?

[다믜(damhiya)]

대신 딴사람이랑 채팅으로 agda얘기 할 때 kime 수식 입력기 사용 가능

[익명(141.223)]

어우 너무 이뻐

[김민성태팬클럽회장(thecoqproofassistant)]

[미쿠쟝넘나좋아(222.98)]

ㅗㅜㅑ - dc App

[black7375(8.47)]

[익명(211.58)]

[9rum(msh01170)]

[브닌떼(172.58)]

사진, 배경, 주제 군더더기 없노