Closed aljungstrom closed 4 months ago
In #1111 I fixed the elim→Set so that its computation rules hold definitionally. This PR contains the corresponding fix for elim→Gpd. It's not used anywhere in the library yet (but I'll need it in the future), so this sould be mergeable directly.
elim→Set
elim→Gpd
In #1111 I fixed the
elim→Setso that its computation rules hold definitionally. This PR contains the corresponding fix forelim→Gpd. It's not used anywhere in the library yet (but I'll need it in the future), so this sould be mergeable directly.