Set Quotients
Table of Contents
1 Set quotients
module Lib.SetQuotients where
This file defines set quotients, i.e., types quotiented by an equivalence relation to a set, and show that the equality when quotienting is effective; that is, that equality on a set quotient corresponds to the equivalence relation it is quotiented from. This file mostly follows the HoTT book, §6.10.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Lib.EquivalenceRelations import Lib.Image import Lib.Prop.Levels import Lib.Prop.Set
1.2 Specification
For any set B, a map is a set quotient whenever precomposing with the quotient yields an equivalence: (A → B) ≅ (Σf: A → BΠx,y: AR(a, b) → f(a) = f(b)).
precomp-Set-quotient (A : U) (R : Eq-Rel A) (B X : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (g : Set/hom B X) : reflecting-map-Eq-Rel A R (Set/type X) = ( λx. g (reflecting-map-Eq-Rel/map A R (Set/type B) f x), λx y r. ap ( Set/type B) ( Set/type X) g ( reflecting-map-Eq-Rel/map A R (Set/type B) f x) ( reflecting-map-Eq-Rel/map A R (Set/type B) f y) ( reflecting-map-Eq-Rel/reflects-Eq A R (Set/type B) f x y r))
A map is a set quotient whenever its precomposition is an equivalence.
is-set-quotient (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) : U = (X : UU-Set) → is-equiv (Set/hom B X) (reflecting-map-Eq-Rel A R (Set/type X)) (precomp-Set-quotient A R B X f)
1.3 Definition
A set quotient is a type, quotiented by a relation R (that is, if R(a, b) then q(a) = q(b)) such that the final type is a set.
data Set-quotient (A : U) (R : Eq-Rel A) : U = Set-quotient/q (a : A) | Set-quotient/eq (a b : A) (r : Eq-Rel/type A R a b) <i> [(i=0) → Set-quotient/q a, (i=1) → Set-quotient/q b] | Set-quotient/squash (x y : Set-quotient A R) (p q : Path (Set-quotient A R) x y) <i j> [(i=0) → p j, (i=1) → q j, (j=0) → x, (j=1) → y]
As expected, quotienting respects the equivalence relation.
Set-quotient/respects-relation (A : U) (R : Eq-Rel A) (x y : A) : Eq-Rel/type A R x y → Path (Set-quotient A R) (Set-quotient/q x) (Set-quotient/q y) = λr i. Set-quotient/eq x y r i
And it is a set.
Set-quotient/is-set (A : U) (R : Eq-Rel A) : is-set (Set-quotient A R) = λx y p q i j. Set-quotient/squash x y p q i j Set-quotient/Set (A : U) (R : Eq-Rel A) : UU-Set = ( Set-quotient A R, Set-quotient/is-set A R)
1.4 Induction principle
Of course, it has an induction principle.
ind-Set-quotient (A : U) (R : Eq-Rel A) (P : Set-quotient A R → UU-Set) (f : (x : A) → Set/type (P (Set-quotient/q x))) (feq : (x y : A) → (r : Eq-Rel/type A R x y) → PathP (i. Set/type (P (Set-quotient/eq x y r i))) (f x) (f y)) : (x : Set-quotient A R) → Set/type (P x) = split Set-quotient/q a → f a Set-quotient/eq x y r i → feq x y r i Set-quotient/squash x y p q i j → square/dependent-fill ( Set-quotient A R) P x y p q ( λi' j'. Set-quotient/squash x y p q i' j') ( ind-Set-quotient A R P f feq x) ( ind-Set-quotient A R P f feq y) ( λk. ind-Set-quotient A R P f feq (p k)) ( λk. ind-Set-quotient A R P f feq (q k)) i j
And a recursion principle.
rec-Set-quotient (A : U) (R : Eq-Rel A) (B : UU-Set) (f : A → Set/type B) (feq : (x y : A) → Eq-Rel/type A R x y → Path (Set/type B) (f x) (f y)) : (x : Set-quotient A R) → Set/type B = ind-Set-quotient A R ( λ_. B) f feq
1.5 Using propositions
There's a (slightly simpler) induction principle if the goal is a proposition.
PathO-to-PathP (A : U) (x y : A) (p : Path A x y) (B : A → U) (u : B x) (v : B y) : (PathO A x y p B u v) → PathP (i. B (p i)) u v = Equiv/inv-map ( PathP (i. B (p i)) u v) ( PathO A x y p B u v) ( path-to-equiv ( PathP (i. B (p i)) u v) ( PathO A x y p B u v) ( PathP-eq-PathO A x y p B u v)) ind-Set-quotient/Prop (A : U) (R : Eq-Rel A) (P : Set-quotient A R → UU-Prop) (f : (x : A) → Prop/type (P (Set-quotient/q x))) : (x : Set-quotient A R) → Prop/type (P x) = split Set-quotient/q a → f a Set-quotient/eq x y r i → PathO-to-PathP ( Set-quotient A R) ( Set-quotient/q x) ( Set-quotient/q y) ( Set-quotient/respects-relation A R x y r) ( λz. Prop/type (P z)) ( f x) ( f y) ( Prop/is-prop ( P (Set-quotient/q y)) ( tr (Set-quotient A R) (Set-quotient/q x) (Set-quotient/q y) (Set-quotient/respects-relation A R x y r) (λz. Prop/type (P z)) (f x)) ( f y)) i Set-quotient/squash x y p q i j → square/dependent-fill ( Set-quotient A R) ( λz. Prop/Set (P z)) x y p q ( λi' j'. Set-quotient/squash x y p q i' j') ( ind-Set-quotient/Prop A R P f x) ( ind-Set-quotient/Prop A R P f y) ( λk. ind-Set-quotient/Prop A R P f (p k)) ( λk. ind-Set-quotient/Prop A R P f (q k)) i j
And thus, there's also a slightly simpler recursor.
rec-Set-quotient/Prop (A : U) (R : Eq-Rel A) (B : UU-Prop) (f : A → Prop/type B) : (x : Set-quotient A R) → Prop/type B = ind-Set-quotient/Prop A R (λ_. B) f
1.6 Surjectivity
The quotient of a type by an equivalence relation is obviously surjective.
quotienting-is-surj (A : U) (R : Eq-Rel A) : is-surj A (Set-quotient A R) (λa. Set-quotient/q a) = ind-Set-quotient/Prop A R ( λx. Prop-trunc/Prop (Fib A (Set-quotient A R) (λa. Set-quotient/q a) x)) ( λx. Prop-trunc/unit (x, refl (Set-quotient A R) (Set-quotient/q x)))
1.7 Set quotient is a set quotient
Set-quotient/relation (A : U) (R : Eq-Rel A) : reflecting-map-Eq-Rel A R (Set-quotient A R) = ( (λx. Set-quotient/q x), Set-quotient/respects-relation A R) Set-quotient/is-set-quotient/map (A : U) (R : Eq-Rel A) (B : UU-Set) : (Set-quotient A R → Set/type B) → (reflecting-map-Eq-Rel A R (Set/type B)) = precomp-Set-quotient A R ( Set-quotient/Set A R) B ( Set-quotient/relation A R) Set-quotient/is-set-quotient/inv-map (A : U) (R : Eq-Rel A) (B : UU-Set) : (reflecting-map-Eq-Rel A R (Set/type B)) → (Set-quotient A R → Set/type B) = λt. rec-Set-quotient A R B t.1 t.2 Set-quotient/is-set-quotient/right-htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (t : reflecting-map-Eq-Rel A R (Set/type B)) : Path (reflecting-map-Eq-Rel A R (Set/type B)) (Set-quotient/is-set-quotient/map A R B (Set-quotient/is-set-quotient/inv-map A R B t)) t = refl (reflecting-map-Eq-Rel A R (Set/type B)) t Set-quotient/is-set-quotient/left-htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (f : Set-quotient A R → Set/type B) : Path (Set-quotient A R → Set/type B) (Set-quotient/is-set-quotient/inv-map A R B (Set-quotient/is-set-quotient/map A R B f)) f = λi x. rec-Prop-trunc ( Fib A (Set-quotient A R) (λz. Set-quotient/q z) x) ( Set/eq/Prop B ( Set-quotient/is-set-quotient/inv-map A R B (Set-quotient/is-set-quotient/map A R B f) x) ( f x)) ( λt. comp ( Set/type B) ( Set-quotient/is-set-quotient/inv-map A R B (Set-quotient/is-set-quotient/map A R B f) x) ( f (Set-quotient/q t.1)) ( ap (Set-quotient A R) (Set/type B) (λz. Set-quotient/is-set-quotient/inv-map A R B (Set-quotient/is-set-quotient/map A R B f) z) x (Set-quotient/q t.1) t.2) ( f x) ( ap (Set-quotient A R) (Set/type B) f (Set-quotient/q t.1) x (inv (Set-quotient A R) x (Set-quotient/q t.1) t.2))) ( quotienting-is-surj A R x) i
Then, we can conclude on it being an equivalence.
Set-quotient/is-set-quotient (A : U) (R : Eq-Rel A) : is-set-quotient A R (Set-quotient/Set A R) (Set-quotient/relation A R) = λB. has-inverse/is-equiv ( Set-quotient A R → Set/type B) ( reflecting-map-Eq-Rel A R (Set/type B)) ( Set-quotient/is-set-quotient/map A R B) ( Set-quotient/is-set-quotient/inv-map A R B, ( Set-quotient/is-set-quotient/right-htpy A R B, Set-quotient/is-set-quotient/left-htpy A R B))
1.8 Effective on equivalence relations
The equality on set quotient is equivalent to the relation. To show this, we first define an auxiliary relation by double induction on the set quotient. We define R'(q(x), q(y)) by R(x, y).
is-set-quotient/is-effective/rel-eq (A : U) (R : Eq-Rel A) (x y z : A) (r1 : Eq-Rel/type A R y z) : Path UU-Prop (Eq-Rel/Relation A R x y) (Eq-Rel/Relation A R x z) = UU-Prop/eq/map ( Eq-Rel/Relation A R x y) ( Eq-Rel/Relation A R x z) ( equiv-to-path ( Eq-Rel/type A R x y) ( Eq-Rel/type A R x z) ( Prop/Equiv ( Eq-Rel/Relation A R x y) ( Eq-Rel/Relation A R x z) ( λrxy. Eq-Rel/is-transitive A R x y z rxy r1) ( λrxz. Eq-Rel/is-transitive A R x z y rxz ( Eq-Rel/is-symmetric A R y z r1)))) is-set-quotient/is-effective/rel-eq'' (A : U) (R : Eq-Rel A) (x y : A) (r : Eq-Rel/type A R x y) (z : A) : Path UU-Prop (Eq-Rel/Relation A R x z) (Eq-Rel/Relation A R y z) = UU-Prop/eq/map ( Eq-Rel/Relation A R x z) ( Eq-Rel/Relation A R y z) ( equiv-to-path ( Eq-Rel/type A R x z) ( Eq-Rel/type A R y z) ( Prop/Equiv ( Eq-Rel/Relation A R x z) ( Eq-Rel/Relation A R y z) ( λrxz. Eq-Rel/is-symmetric A R z y ( Eq-Rel/is-transitive A R z x y ( Eq-Rel/is-symmetric A R x z rxz) r)) ( λryz. Eq-Rel/is-symmetric A R z x ( Eq-Rel/is-transitive A R z y x ( Eq-Rel/is-symmetric A R y z ryz) ( Eq-Rel/is-symmetric A R x y r))))) lock UU-Prop/is-set has-inverse/is-equiv UU-Prop/eq/map is-set-quotient/is-effective/rel-aux' (A : U) (R : Eq-Rel A) (y : Set-quotient A R) (x : A) : UU-Prop = rec-Set-quotient A R UU-Prop/Set ( λy'. Eq-Rel/Relation A R x y') ( is-set-quotient/is-effective/rel-eq A R x) y is-set-quotient/is-effective/rel-eq' (A : U) (R : Eq-Rel A) (y : Set-quotient A R) (a b : A) (r : Eq-Rel/type A R a b) : Path UU-Prop (is-set-quotient/is-effective/rel-aux' A R y a) (is-set-quotient/is-effective/rel-aux' A R y b) = ind-Set-quotient/Prop A R ( λz. Set/eq/Prop UU-Prop/Set ( is-set-quotient/is-effective/rel-aux' A R z a) ( is-set-quotient/is-effective/rel-aux' A R z b)) ( is-set-quotient/is-effective/rel-eq'' A R a b r) y is-set-quotient/is-effective/rel-aux (A : U) (R : Eq-Rel A) (x y : Set-quotient A R) : UU-Prop = rec-Set-quotient A R UU-Prop/Set ( is-set-quotient/is-effective/rel-aux' A R y) ( is-set-quotient/is-effective/rel-eq' A R y) x
Of course, R' is reflexive.
is-set-quotient/is-effective/refl (A : U) (R : Eq-Rel A) (x : Set-quotient A R) : (Prop/type (is-set-quotient/is-effective/rel-aux A R x x)) = ind-Set-quotient/Prop A R ( λx'. is-set-quotient/is-effective/rel-aux A R x' x') ( Eq-Rel/is-reflexive A R) x
Then, as R'(q(x), q(y)) is a proposition, it suffices to show that there's a back-and-forth map to the equality on the set quotient for them to be equivalent. The map from path to relation is trivial by reflexivity.
is-set-quotient/is-effective/map (A : U) (R : Eq-Rel A) (x y : Set-quotient A R) : Path (Set-quotient A R) x y → (Prop/type (is-set-quotient/is-effective/rel-aux A R x y)) = J ( Set-quotient A R) x ( λz _. Prop/type (is-set-quotient/is-effective/rel-aux A R x z)) ( is-set-quotient/is-effective/refl A R x) y
On the other hand, we show that if R'(x, y) then there are x', y' s.t. R(q(x'), q(y')). Thus, there is a path between q(x') and q(y') and so between x and y.
is-set-quotient/is-effective/R (A : U) (R : Eq-Rel A) (a b : Set-quotient A R) (x y : A) (p : Path (Set-quotient A R) a (Set-quotient/q x)) (q : Path (Set-quotient A R) b (Set-quotient/q y)) (r : Prop/type (is-set-quotient/is-effective/rel-aux A R a b)) : Prop/type (is-set-quotient/is-effective/rel-aux A R (Set-quotient/q x) (Set-quotient/q y)) = tr ( Set-quotient A R) a ( Set-quotient/q x) p ( λz. Prop/type (is-set-quotient/is-effective/rel-aux A R z (Set-quotient/q y))) ( tr ( Set-quotient A R) b ( Set-quotient/q y) q ( λz. Prop/type (is-set-quotient/is-effective/rel-aux A R a z)) r) is-set-quotient/is-effective/eq' (A : U) (R : Eq-Rel A) (a b : Set-quotient A R) (x y : A) (p : Path (Set-quotient A R) a (Set-quotient/q x)) (q : Path (Set-quotient A R) b (Set-quotient/q y)) (r : Prop/type (is-set-quotient/is-effective/rel-aux A R a b)) : Path (Set-quotient A R) (Set-quotient/q x) (Set-quotient/q y) = λi. Set-quotient/eq x y ( is-set-quotient/is-effective/R A R a b x y p q r) i is-set-quotient/is-effective/eq (A : U) (R : Eq-Rel A) (a b : Set-quotient A R) (x y : A) (p : Path (Set-quotient A R) a (Set-quotient/q x)) (q : Path (Set-quotient A R) b (Set-quotient/q y)) (r : Prop/type (is-set-quotient/is-effective/rel-aux A R a b)) : Path (Set-quotient A R) a b = tr ( Set-quotient A R) ( Set-quotient/q x) a ( inv (Set-quotient A R) a (Set-quotient/q x) p) ( λz. Path (Set-quotient A R) z b) ( tr ( Set-quotient A R) ( Set-quotient/q y) b ( inv (Set-quotient A R) b (Set-quotient/q y) q) ( λz. Path (Set-quotient A R) (Set-quotient/q x) z) ( is-set-quotient/is-effective/eq' A R a b x y p q r)) is-set-quotient/is-effective/inv-map (A : U) (R : Eq-Rel A) (x y : Set-quotient A R) (r : Prop/type (is-set-quotient/is-effective/rel-aux A R x y)) : Path (Set-quotient A R) x y = rec-Prop-trunc ( Fib A (Set-quotient A R) (λa. Set-quotient/q a) x) ( Set/eq/Prop (Set-quotient/Set A R) x y) ( λt. rec-Prop-trunc ( Fib A (Set-quotient A R) (λa. Set-quotient/q a) y) ( Set/eq/Prop (Set-quotient/Set A R) x y) ( λu. is-set-quotient/is-effective/eq A R x y t.1 u.1 t.2 u.2 r) ( quotienting-is-surj A R y)) ( quotienting-is-surj A R x)
And thus, there is an equivalence between R(x, y) and q(x) = q(y).
is-set-quotient/is-effective (A : U) (R : Eq-Rel A) (x y : A) : Equiv (Path (Set-quotient A R) (Set-quotient/q x) (Set-quotient/q y)) (Eq-Rel/type A R x y) = Prop/Equiv ( Set/eq/Prop (Set-quotient/Set A R) (Set-quotient/q x) (Set-quotient/q y)) ( Eq-Rel/Relation A R x y) ( is-set-quotient/is-effective/map A R (Set-quotient/q x) (Set-quotient/q y)) ( is-set-quotient/is-effective/inv-map A R (Set-quotient/q x) (Set-quotient/q y)) is-set-quotient/is-effective' (A : U) (R : Eq-Rel A) (x y : A) : Equiv (Eq-Rel/type A R x y) (Path (Set-quotient A R) (Set-quotient/q x) (Set-quotient/q y)) = Prop/Equiv ( Eq-Rel/Relation A R x y) ( Set/eq/Prop (Set-quotient/Set A R) (Set-quotient/q x) (Set-quotient/q y)) ( is-set-quotient/is-effective/inv-map A R (Set-quotient/q x) (Set-quotient/q y)) ( is-set-quotient/is-effective/map A R (Set-quotient/q x) (Set-quotient/q y))
We do not forget to unlock the things that take time to compute.
unlock UU-Prop/is-set has-inverse/is-equiv UU-Prop/eq/map
1.9 Uniqueness principle
We show that whenever a pair (f : A → B, g : R(x, y) → f x = f y) is a set quotient, then any map that extends f is unique. To see this, we use the im/inclusion and im/q functions. First, we show that for any x, y such that R(x, y), im/q q x = im/q q y. Indeed, im/inclusion (im/q q x) = q x = q y = im/inclusion (im/q q y), and im/inclusion is injective.
is-set-quotient/is-surj/identifying-q (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (x y : A) (r : Eq-Rel/type A R x y) : Path (im A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f)) (im/q A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f) x) (im/q A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f) y) = let g : A → Set/type B = (reflecting-map-Eq-Rel/map A R (Set/type B) f) in im/is-injective A ( Set/type B) g ( im/q A (Set/type B) g x) ( im/q A (Set/type B) g y) ( comp-n ( Set/type B) three-Nat ( im/inclusion A (Set/type B) g (im/q A (Set/type B) g x)) ( g x) ( im/htpy A (Set/type B) g x) ( g y) ( reflecting-map-Eq-Rel/reflects-Eq A R (Set/type B) f x y r) ( im/inclusion A (Set/type B) g (im/q A (Set/type B) g y)) ( im/htpy' A (Set/type B) g y))
As im(q) is a set and f a set quotient, we get an extension of qq along q.
is-set-quotient/is-surj/map (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (is-set-quotient-f : is-set-quotient A R B f) : Set/type B → im A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f) = let q : A → Set/type B = reflecting-map-Eq-Rel/map A R (Set/type B) f in is-equiv/inv-map ( Set/type B → im A (Set/type B) q) ( reflecting-map-Eq-Rel A R (Set/type (im/Set A B q))) ( precomp-Set-quotient A R B (im/Set A B q) f) ( is-set-quotient-f (im/Set A B q)) ( im/q A (Set/type B) q, is-set-quotient/is-surj/identifying-q A R B f)
We can show that the composition of this map with image inclusion is actually qq.
lock is-prop/is-set is-set-quotient/is-surj/htpy (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (H : is-set-quotient A R B f) : Htpy' A (im A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f)) (λx. is-set-quotient/is-surj/map A R B f H (reflecting-map-Eq-Rel/map A R (Set/type B) f x)) (im/q A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f)) = let q : A → Set/type B = reflecting-map-Eq-Rel/map A R (Set/type B) f in htpy-eq' A ( im A (Set/type B) q) ( λx. is-set-quotient/is-surj/map A R B f H (q x)) ( im/q A (Set/type B) q) ( λi. ( ( is-equiv/inv-right-htpy ( Set/type B → im A (Set/type B) q) ( reflecting-map-Eq-Rel A R (Set/type (im/Set A B q))) ( precomp-Set-quotient A R B (im/Set A B q) f) ( H (im/Set A B q)) ( im/q A (Set/type B) q, is-set-quotient/is-surj/identifying-q A R B f)) i).1)
As such, the composition of the inclusion with the map and q is q.
is-set-quotient/is-surj/htpy2 (A : U) (R : Eq-Rel A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R (Set/type B)) (H : is-set-quotient A R B f) (x : A) : Path (Set/type B) (im/inclusion A (Set/type B) (reflecting-map-Eq-Rel/map A R (Set/type B) f) (is-set-quotient/is-surj/map A R B f H (reflecting-map-Eq-Rel/map A R (Set/type B) f x))) (reflecting-map-Eq-Rel/map A R (Set/type B) f x) = let q : A → Set/type B = reflecting-map-Eq-Rel/map A R (Set/type B) f in comp ( Set/type B) ( im/inclusion A ( Set/type B) q ( is-set-quotient/is-surj/map A R B f H (q x))) ( im/inclusion A ( Set/type B) q ( im/q A (Set/type B) q x)) ( ap (im A (Set/type B) q) (Set/type B) (im/inclusion A (Set/type B) q) (is-set-quotient/is-surj/map A R B f H (q x)) (im/q A (Set/type B) q x) ( is-set-quotient/is-surj/htpy A R B f H x)) ( q x) ( im/htpy A (Set/type B) q x)
We can conclude that q is surjective.
-- is-set-quotient/is-surj (A : U) (R : Relation-Prop A) (B : UU-Set) (f : reflecting-map-Eq-Rel A R B) (H : is-set-quotient A R B f) -- : is-surj A (Set/type B) (reflecting-map-Eq-Rel A R B f) = -- let q : A → Set/type B = (reflecting-map-Eq-Rel A R B f) in