Agda 2 is a proof assistant developed at the Chalmers institute of technology. This is a shot of an ongoing proof related to category theory. It is taken on the LCD screen of a laptop.
{{Information |Description=Agda 2 is a proof assistant developed at the Chalmers institute of technology. This is a shot of an ongoing proof related to category theory. It is taken on the LCD screen of a laptop. |Source=self-made (http://aperturefirst.eff