Agda code to show the profunctor-based arrow definition satisfies the
arrow laws that does not involve first. The primal goal of the
implementation is for me to understand Proposition 4.2 in the
following paper:
B. Jacobs, C. Heunen, and I. Hasuo: Categorical Semantics for Arrows, JFP 19(3-4), 2009. pp. 403-438.
This repository is just for my studying purpose, and includes a lot of
reinvention of the wheel. In Category.agda, I borrowed or paraphrased
some code and ideas from the library https://github.com/agda/agda-categories.
This is the reason why this repos's LICENSE refers to "Agda Github Community", the copyright holder of the agda-categories library.