feat(hott): functoriality of quotients

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

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) :=

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