From f3b2c7010f3e72ee5c2942de291d286d5156cd91 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Sat, 19 Dec 2015 18:13:02 -0500 Subject: [PATCH] feat(hott): functoriality of quotients --- hott/hit/quotient_functor.hlean | 113 ++++++++++++++++++++++++++++++++ hott/types/prod.hlean | 15 +++++ hott/types/sigma.hlean | 2 + 3 files changed, 130 insertions(+) create mode 100644 hott/hit/quotient_functor.hlean diff --git a/hott/hit/quotient_functor.hlean b/hott/hit/quotient_functor.hlean new file mode 100644 index 0000000000..9cda7fa9b9 --- /dev/null +++ b/hott/hit/quotient_functor.hlean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2015 Ulrik Buchholtz. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ulrik Buchholtz + +Functoriality of quotients and a condition for when an equivalence is induced. +-/ + +import types.sigma .quotient +open eq is_equiv equiv prod prod.ops sigma sigma.ops + +namespace quotient +section + variables {A : Type} (R : A → A → Type) + {B : Type} (Q : B → B → Type) + (f : A → B) (k : Πa a' : A, R a a' → Q (f a) (f a')) + include f k + + protected definition functor [reducible] : quotient R → quotient Q := + quotient.elim (λa, class_of Q (f a)) (λa a' r, eq_of_rel Q (k a a' r)) + + variables [F : is_equiv f] [K : Πa a', is_equiv (k a a')] + include F K + + protected definition functor_inv [reducible] : quotient Q → quotient R := + quotient.elim (λb, class_of R (f⁻¹ b)) + (λb b' q, eq_of_rel R ((k (f⁻¹ b) (f⁻¹ b'))⁻¹ + ((right_inv f b)⁻¹ ▸ (right_inv f b')⁻¹ ▸ q))) + + protected definition is_equiv [instance] + : is_equiv (quotient.functor R Q f k):= + begin + fapply adjointify _ (quotient.functor_inv R Q f k), + { intro qb, induction qb with b b b' q, + { apply ap (class_of Q), apply right_inv }, + { apply eq_pathover, rewrite [ap_id,ap_compose' (quotient.elim _ _)], + do 2 krewrite elim_eq_of_rel, rewrite (right_inv (k (f⁻¹ b) (f⁻¹ b'))), + assert H1 : pathover (λz : B × B, Q z.1 z.2) + ((right_inv f b)⁻¹ ▸ (right_inv f b')⁻¹ ▸ q) + (prod_eq (right_inv f b) (right_inv f b')) q, + { apply pathover_of_eq_tr, krewrite [prod_eq_inv,prod_eq_transport] }, + assert H2 : square + (ap (λx : (Σz : B × B, Q z.1 z.2), class_of Q x.1.1) + (sigma_eq (prod_eq (right_inv f b) (right_inv f b')) H1)) + (ap (λx : (Σz : B × B, Q z.1 z.2), class_of Q x.1.2) + (sigma_eq (prod_eq (right_inv f b) (right_inv f b')) H1)) + (eq_of_rel Q ((right_inv f b)⁻¹ ▸ (right_inv f b')⁻¹ ▸ q)) + (eq_of_rel Q q), + { exact + natural_square (λw : (Σz : B × B, Q z.1 z.2), eq_of_rel Q w.2) + (sigma_eq (prod_eq (right_inv f b) (right_inv f b')) H1) }, + krewrite (ap_compose' (class_of Q)) at H2, + krewrite (ap_compose' (λz : B × B, z.1)) at H2, + rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2, + krewrite prod.ap_pr1 at H2, krewrite prod_eq_pr1 at H2, + krewrite (ap_compose' (class_of Q) (λx : (Σz : B × B, Q z.1 z.2), x.1.2)) at H2, + krewrite (ap_compose' (λz : B × B, z.2)) at H2, + rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2, + krewrite prod.ap_pr2 at H2, krewrite prod_eq_pr2 at H2, + apply H2 } }, + { intro qa, induction qa with a a a' r, + { apply ap (class_of R), apply left_inv }, + { apply eq_pathover, rewrite [ap_id,(ap_compose' (quotient.elim _ _))], + do 2 krewrite elim_eq_of_rel, + assert H1 : pathover (λz : A × A, R z.1 z.2) + ((left_inv f a)⁻¹ ▸ (left_inv f a')⁻¹ ▸ r) + (prod_eq (left_inv f a) (left_inv f a')) r, + { apply pathover_of_eq_tr, krewrite [prod_eq_inv,prod_eq_transport] }, + assert H2 : square + (ap (λx : (Σz : A × A, R z.1 z.2), class_of R x.1.1) + (sigma_eq (prod_eq (left_inv f a) (left_inv f a')) H1)) + (ap (λx : (Σz : A × A, R z.1 z.2), class_of R x.1.2) + (sigma_eq (prod_eq (left_inv f a) (left_inv f a')) H1)) + (eq_of_rel R ((left_inv f a)⁻¹ ▸ (left_inv f a')⁻¹ ▸ r)) + (eq_of_rel R r), + { exact + natural_square (λw : (Σz : A × A, R z.1 z.2), eq_of_rel R w.2) + (sigma_eq (prod_eq (left_inv f a) (left_inv f a')) H1) }, + krewrite (ap_compose' (class_of R)) at H2, + krewrite (ap_compose' (λz : A × A, z.1)) at H2, + rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2, + krewrite prod.ap_pr1 at H2, krewrite prod_eq_pr1 at H2, + krewrite (ap_compose' (class_of R) (λx : (Σz : A × A, R z.1 z.2), x.1.2)) at H2, + krewrite (ap_compose' (λz : A × A, z.2)) at H2, + rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2, + krewrite prod.ap_pr2 at H2, krewrite prod_eq_pr2 at H2, + assert H3 : + (k (f⁻¹ (f a)) (f⁻¹ (f a')))⁻¹ + ((right_inv f (f a))⁻¹ ▸ (right_inv f (f a'))⁻¹ ▸ k a a' r) + = (left_inv f a)⁻¹ ▸ (left_inv f a')⁻¹ ▸ r, + { rewrite [adj f a,adj f a',ap_inv',ap_inv'], + rewrite [-(tr_compose _ f (left_inv f a')⁻¹ (k a a' r)), + -(tr_compose _ f (left_inv f a)⁻¹)], + rewrite [-(fn_tr_eq_tr_fn (left_inv f a')⁻¹ (λx, k a x) r), + -(fn_tr_eq_tr_fn (left_inv f a)⁻¹ + (λx, k x (f⁻¹ (f a')))), + left_inv (k _ _)] }, + rewrite H3, apply H2 } } + end +end + +section + open equiv.ops + variables {A : Type} (R : A → A → Type) + {B : Type} (Q : B → B → Type) + (f : A ≃ B) (k : Πa a' : A, R a a' ≃ Q (f a) (f a')) + include f k + + /- This could also be proved using ua, but then it wouldn't compute -/ + protected definition equiv : quotient R ≃ quotient Q := + equiv.mk (quotient.functor R Q f k) _ +end +end quotient diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index edf1c9e110..d5140792a7 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -37,6 +37,9 @@ namespace prod end ops open ops + protected definition ap_pr1 (p : u = v) : ap pr1 p = p..1 := idp + protected definition ap_pr2 (p : u = v) : ap pr2 p = p..2 := idp + definition pair_prod_eq (p : u.1 = v.1) (q : u.2 = v.2) : ((prod_eq p q)..1, (prod_eq p q)..2) = (p, q) := by induction u; induction v; esimp at *; induction p; induction q; reflexivity @@ -77,12 +80,24 @@ namespace prod definition prod_eq_equiv [constructor] (u v : A × B) : (u = v) ≃ (u.1 = v.1 × u.2 = v.2) := (equiv.mk prod_eq_unc _)⁻¹ᵉ + /- Groupoid structure -/ + definition prod_eq_inv (p : a = a') (q : b = b') : (prod_eq p q)⁻¹ = prod_eq p⁻¹ q⁻¹ := + by cases p; cases q; reflexivity + + definition prod_eq_concat (p : a = a') (p' : a' = a'') (q : b = b') (q' : b' = b'') + : prod_eq p q ⬝ prod_eq p' q' = prod_eq (p ⬝ p') (q ⬝ q') := + by cases p; cases q; cases p'; cases q'; reflexivity + /- Transport -/ definition prod_transport (p : a = a') (u : P a × Q a) : p ▸ u = (p ▸ u.1, p ▸ u.2) := by induction p; induction u; reflexivity + definition prod_eq_transport (p : a = a') (q : b = b') {R : A × B → Type} (r : R (a, b)) + : (prod_eq p q) ▸ r = p ▸ q ▸ r := + by induction p; induction q; reflexivity + /- Pathovers -/ definition etao (p : a = a') (bc : P a × Q a) : bc =[p] (p ▸ bc.1, p ▸ bc.2) := diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 8bed0f0d6d..20dceb82f5 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -69,6 +69,8 @@ namespace sigma : transport (λx, B' x.1) (sigma_eq p q) = transport B' p := by induction u; induction v; esimp at *;induction q; reflexivity + protected definition ap_pr1 (p : u = v) : ap (λx : sigma B, x.1) p = p..1 := idp + /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/ definition sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v