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 |
JacquesCarette
/ SetoidChoice.agda
Created
January 19, 2022 18:35
Variant of Andrej's code to try to understand choice and 'type like'.
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
| {-# OPTIONS --safe --without-K #-} | |
| -- Characterizations of setoids that satisfy the axiom of choice. | |
| -- | |
| -- We define four properties of a setoid A: | |
| -- | |
| -- (1) A satisfies the axiom of choice | |
| -- (2) A is projective | |
| -- (3) A is isomorphic to a type | |
| -- (4) A has canonical elements | |
| -- |