Jacques Carette JacquesCarette

JacquesCarette / Epimorphism.agda

Last active January 13, 2022 04:22 — forked from andrejbauer/Epimorphism.agda

A setoid satisfies choice if, and only if its equivalence relation is equality.

	open import Level using (Level; suc; _⊔_; Lift; lift; lower)
	open import Relation.Binary using (Setoid)
	open import Data.Product using (_×_; swap; zip; ∃; map₂; proj₁; proj₂)
	open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd)
	open import Function.Equality hiding (setoid; flip)
	open import Function using (flip) renaming (id to id→; _∘′_ to _∘→_)
	import Relation.Binary.Reasoning.Setoid as SetoidR

	module Epimorphism where