Skip to content

Instantly share code, notes, and snippets.

View JacquesCarette's full-sized avatar

Jacques Carette JacquesCarette

View GitHub Profile
@JacquesCarette
JacquesCarette / SetoidChoice.agda
Created January 19, 2022 18:35
Variant of Andrej's code to try to understand choice and 'type like'.
{-# 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
--
@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