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 # -- an instance of function extensionality #unit-fun-ext : {X : Set} (f : Unit → X) → ---------------- (λ _ → f unit) ≡ f #unit-fun-ext f = primTrustMe --!!!! {- This is a safe use of primTrustMe, since function extensionality is known to be consistent. In fact quotient sets can be used to prove functional extensionality -- see funext below -- but we need this instance of it as part of the definition. -} 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) = transport B (#in ∙ #unit-fun-ext 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 -}