module quotient where
{---------------------------------------------------------------------
Alan Jeffrey, Dan Licata, Andy Pitts
13 May 2015.
This is an Agda file Tested with Agda 2.4.2.2
An implementation of quotients up to propositional identity, using an
enhanced version of Dan Licata's trick with Agda's "private" and
"postulate" declarations to define an interval type
http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
The enhancements are two-fold:
1. Use primTrustMe rather than postulates for improved
computational behaviour, inspired by Alan Jeffrey
https://groups.google.com/forum/#!topic/homotopytypetheory/hTAVT6CGbrs
2. Careful combination of thunking and private declarations to ensure
(we hope!) that the function sending an element to its equivalence
class cannot be proved to be an injection outside the scope of the
private declarations. This Yoga to avoid logical inconsistency is
adapted from Guillaume Brunerie and Dan Licata's hott-agda development
https://github.com/dlicata335/hott-agda/blob/master/lib/spaces/hithacks.agda
----------------------------------------------------------------------
Usage:
Given
- a type A : Set
- a relation R : A → A → Set
you get
- a type A / R
(of equivalence classes for the equivalence relation generated by R)
- a function _mod R : A → A / R
(mapping elements of R to propositional equalities and universal
amongst such function out of A)
- an eliminator for A / R, yielding a function
elim B f e : (z : A / R) → B z
from B : A / R → Set, f : (x : A) → B(x mod R) and a proof e that
f maps elements of R to propositional equalities.
elim B f e (x mod R) reduces to f x, because of the use of
primTrustMe rather than a postulate, and elim B f e is unique with
this property up to propositional equality.
---------------------------------------------------------------------}
open import Agda.Primitive
----------------------------------------------------------------------
module prelude where
-- Propositional equality
data _≡_ {ℓ : Level}{A : Set ℓ}(x : A) : (x' : A) → Set ℓ where
refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}
{-
We only define quotients for h-sets, so we make all types h-sets by
allowing pattern-matching-with-K and make use of uniqueness of
identity proofs
-}
uip :
{ℓ : Level}
{A : Set ℓ}
{x y : A}
(p q : x ≡ y)
→ -----------------------
(p ≡ q)
uip refl refl = refl
_∙_ :
{ℓ ℓ' : Level}
{A : Set ℓ}
{B : Set ℓ'}
(f : A → B)
{x y : A}
(p : x ≡ y)
→ -----------
f x ≡ f y
f ∙ refl = refl
transport :
{ℓ ℓ' : Level}
{A : Set ℓ}
(B : A → Set ℓ')
{x y : A}
(p : x ≡ y)
→ -----------
B x → B y
transport B refl = λ b → b
-- Heterogeneous equality over a given type equality
_≡_over_ :
{ℓ : Level}
{A B : Set ℓ}
(x : A)
(y : B)
(p : A ≡ B)
→ -----------
Set ℓ
x ≡ y over refl = x ≡ y
_over_ :
{ℓ : Level}
{A : Set ℓ}
{x y : A}
(p : x ≡ y)
(q : A ≡ A)
→ ---------
(x ≡ y over q)
p over refl = p
singleton-over :
{ℓ : Level}
{A B : Set ℓ}
(s : (x y : A) → (x ≡ y))
(p : A ≡ B)
(x : A)
(y : B)
→ -----------------
(x ≡ y over p)
singleton-over s refl = s
-- One-element type
record Unit : Set where
constructor unit
-- Booleans
data 𝔹 : Set where
true : 𝔹
false : 𝔹
-- Composition of dependent functions
infix 1 _∘_
_∘_ :
{ℓ ℓ' ℓ'' : Level}
{A : Set ℓ}
{B : A → Set ℓ'}
{C : {x : A} → B x → Set ℓ''}
(g : {x : A}(y : B x) → C y)
(f : (x : A) → B x)
→ ---------------------------
(x : A) → C (f x)
g ∘ f = λ x → g (f x)
-- end of prelude-----------------------------------------------------
open prelude
----------------------------------------------------------------------
--- primTrustMe
----------------------------------------------------------------------
primitive
primTrustMe :
{ℓ : Level}
{A : Set ℓ}
{x y : A}
→ ---------
x ≡ y
----------------------------------------------------------------------
-- Quotients up to propositional identity, via primTrustMe
----------------------------------------------------------------------
module quot {A : Set}(R : A → A → Set) where
private -- # is used to mark private definitions
record # (X : Set) : Set where
constructor #in
field
#out : X
open #
set : Set
set = # (Unit → # A)
quo : A → set
quo x = #in (λ _ → #in x)
equ :
{x y : A}
(r : R x y)
→ -----------
quo x ≡ quo y
equ r = primTrustMe --!!!!
{- This is a potentially unsafe use of primTrustMe. We have to ensure
that outside this module it is not possible to prove that quot.fun
is an injection. -}
elim :
(B : set → Set)
(f : (x : A) → B (quo x))
(_ : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
(y : set)
→ -----------------------------------------------------
B y
elim B f _ (#in g) = f (#out (g unit))
--end of module quot
----------------------------------------------------------------------
-- Notation for quotients
----------------------------------------------------------------------
--quotient set
_/_ :
(A : Set)
(R : A → A → Set)
→ ---------------
Set
A / R = quot.set {A} R
-- equivalence classes
quo :
{A : Set}
{R : A → A → Set}
→ ---------------
A → A / R
quo {R = R} = quot.quo R
syntax quo {R = R} x = x mod R
-- generating equalities
equ :
{A : Set}
{R : A → A → Set}
{x y : A}
(r : R x y)
→ -------------------
(x mod R) ≡ (y mod R)
equ {R = R} = quot.equ R
-- equivalence class eliminators
elim :
{A : Set}
{R : A → A → Set}
(B : (A / R) → Set)
(f : (x : A) → B (x mod R))
(e : {x y : A} (r : R x y) → f x ≡ f y over (B ∙ equ r))
(y : A / R)
→ ------------------------------------------------------
B y
elim {R = R} = quot.elim R
elim-simple :
{A : Set}
{R : A → A → Set}
(B : Set)
(f : A → B)
(e : {x y : A}(r : R x y) → f x ≡ f y)
→ ------------------------------------
A / R → B
elim-simple B f e =
elim (λ _ → B) f (λ r → e r over ((λ _ → B) ∙ equ r))
-- computation rule
comp :
{A : Set}
{R : A → A → Set}
(B : A / R → Set)
(f : (x : A) → B (x mod R))
(e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
(x : A)
→ -----------------------------------------------------
elim B f e (x mod R) ≡ f x
comp B f e x = refl
-- uniqueness rule
uniq :
{A : Set}
{R : A → A → Set}
(B : A / R → Set)
(f : (x : A) → B (x mod R))
(e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
(g : (y : A / R) → B y)
(p : (x : A) → g (x mod R) ≡ f x)
→ -----------------------------------------------------
(y : A / R) → g y ≡ elim B f e y
uniq B f e g p =
let
B' z = g z ≡ elim B f e z
e'{x} {y} r = singleton-over uip (B' ∙ equ r) (p x) (p y)
in elim B' p e'
----------------------------------------------------------------------
-- Example: A/≡ is isomorphic to A
----------------------------------------------------------------------
i :
{A : Set}
(z : A / _≡_)
→ -----------
A
i {A} = elim-simple A (λ x → x) (λ p → p)
j :
{A : Set}
(x : A)
→ -------
A / _≡_
j x = x mod _≡_
i∘j≡id :
{A : Set}
(x : A)
→ ---------
i (j x) ≡ x
i∘j≡id x = refl
j∘i≡id :
{A : Set}
(z : A / _≡_)
→ -----------
j (i z) ≡ z
j∘i≡id {A} =
let B = λ z → j (i z) ≡ z in elim B (λ _ → refl) e where
e : {x y : A} (r : x ≡ y) →
refl ≡ refl over ((λ z → j (i z) ≡ z) ∙ equ r)
e refl = refl
----------------------------------------------------------------------
-- Interval type as a quotient
----------------------------------------------------------------------
data Irel : (x y : 𝔹) → Set where
rel : Irel false true
I = 𝔹 / Irel
s : I
s = false mod Irel
t : I
t = true mod Irel
path : s ≡ t
path = equ {R = Irel} rel
Ielim :
{A : Set}
(x y : A)
(p : x ≡ y)
→ ---------
I → A
Ielim {A} x y p = elim-simple A f e where
f : 𝔹 → A
f true = y
f false = x
e : {b b' : 𝔹} (r : Irel b b') → f b ≡ f b'
e rel = p
----------------------------------------------------------------------
-- Function extensionality is provable, using the interval type
----------------------------------------------------------------------
funext :
{A : Set}
{B : A → Set}
(f g : (x : A) → B x)
(e : (x : A) → f x ≡ g x)
→ -----------------------
f ≡ g
funext f g e = (λ i x → Ielim (f x) (g x) (e x) i) ∙ path
----------------------------------------------------------------------
-- Universal property of quotients
----------------------------------------------------------------------
quot-comp :
{A : Set}
{R : A → A → Set}
(B : A / R → Set)
(f : (x : A) → B (x mod R))
(e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
→ -----------------------------------------------------
(elim B f e ∘ quo) ≡ f
quot-comp B f e = funext (elim B f e ∘ quo) f (λ _ → refl)
quot-uniq :
{A : Set}
{R : A → A → Set}
(B : A / R → Set)
(f : (x : A) → B (x mod R))
(e : {x y : A}(r : R x y) → f x ≡ f y over (B ∙ equ r))
(g : (y : A / R) → B y)
(p : (x : A) → g (x mod R) ≡ f x)
→ -----------------------------------------------------
g ≡ elim B f e
quot-uniq B f e g p =
let
B' = λ z → g z ≡ elim B f e z
p' = elim B' p (λ {x} {y} r →
singleton-over uip (B' ∙ equ r) (p x) (p y))
in funext g (elim B f e) p'
----------------------------------------------------------------------
-- SANITY CHECK
----------------------------------------------------------------------
{- The use of primTrustMe in the module quot implies that quo : A → A/R
cannot always be an injection. So there should be no way to define
the following function...
quo-inj :
{A : Set}
{R : A → A → Set}
(x y : A)
(p : (x mod R) ≡ (y mod R))
→ -------------------------
x ≡ y
quo-inj x y p = {!p!}
...since otherwise the use of primTrustMe has led to logical
inconsistency:
bad : false ≡ true
bad = quo-inj false true path
-}