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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |