Clean up univalent universe helper a bit

- Put most of the auxiliary definitions in a named module so that they don't pollute the namespace on opening the primary module - Make isomorphisms available directly - Cleaned up the path reflection proof with a new lemma about `transportEquiv`
phijor · Jun 14, 2020 · e42a6fa · e42a6fa
1 parent e3f3740
commit e42a6fa
Show file tree

Hide file tree

Showing 2 changed files with 70 additions and 61 deletions.
diff --git a/Cubical/Foundations/Transport.agda b/Cubical/Foundations/Transport.agda
@@ -47,6 +47,19 @@ isEquivTransport {A = A} {B = B} p =
 transportEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B
 transportEquiv p = (transport p , isEquivTransport p)
 
+transpEquiv : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → ∀ i → p i ≃ B
+transpEquiv P i .fst = transp (λ j → P (i ∨ j)) i
+transpEquiv P i .snd
+  = transp (λ k → isEquiv (transp (λ j → P (i ∨ (j ∧ k))) (i ∨ ~ k)))
+      i (idIsEquiv (P i))
+
+uaTransportη : ∀ {ℓ} {A B : Type ℓ} (P : A ≡ B) → ua (transportEquiv P) ≡ P
+uaTransportη P i j
+  = Glue (P i1) λ where
+      (j = i0) → P i0 , transportEquiv P
+      (i = i1) → P j , transpEquiv P j
+      (j = i1) → P i1 , idEquiv (P i1)
+
 pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B
 pathToIso x = iso (transport x) (transport⁻ x ) ( transportTransport⁻ x) (transport⁻Transport x)
 

diff --git a/Cubical/Foundations/Univalence/Universe.agda b/Cubical/Foundations/Univalence/Universe.agda
@@ -39,74 +39,70 @@ private
   variable
     A : Type ℓ'
 
+module UU-Lemmas where
   reg : transport (λ _ → A) ≡ idfun A
   reg {A} i z = transp (λ _ → A) i z
 
-nu : ∀ x y → x ≡ y → El x ≃ El y
-nu x y p = transportEquiv (cong El p)
-
-cong-un-te
-  : ∀ x y (p : El x ≡ El y)
-  → cong El (un x y (transportEquiv p)) ≡ p
-cong-un-te x y p
-  = isInjectiveTransport (
-      transport (cong El (un x y (transportEquiv p)))
-        ≡⟨ cong transport (comp _) ⟩
-      transport (ua (transportEquiv p))
-        ≡[ i ]⟨ (λ z → uaβ (transportEquiv p) z i) ⟩
-      transport p ∎)
-
-
-nu-un : ∀ x y (e : El x ≃ El y) → nu x y (un x y e) ≡ e
-nu-un x y e
-  = equivEq (nu x y (un x y e)) e λ i z
-      → (cong (λ p → transport p z) (comp e) ∙ uaβ e z) i
-
-El-un-equiv : ∀ x i → El (un x x (idEquiv _) i) ≃ El x
-El-un-equiv x i = λ where
-    .fst → transp (λ j → p j) (i ∨ ~ i)
-    .snd → transp (λ j → isEquiv (transp (λ k → p (j ∧ k)) (~ j ∨ i ∨ ~ i)))
-              (i ∨ ~ i) (idIsEquiv T)
-  where
-  T = El (un x x (idEquiv _) i)
-  p : T ≡ El x
-  p j = (comp (idEquiv _) ∙ uaIdEquiv {A = El x}) j i
-
-un-refl : ∀ x → un x x (idEquiv (El x)) ≡ refl
-un-refl x i j
-  = hcomp (λ k → λ where
-        (i = i0) → un x x (idEquiv (El x)) j
-        (i = i1) → un x x (idEquiv (El x)) (j ∨ k)
-        (j = i0) → un x x (idEquiv (El x)) (~ i ∨ k)
-        (j = i1) → x)
-      (un (un x x (idEquiv (El x)) (~ i)) x (El-un-equiv x (~ i)) j)
-
-nu-refl : ∀ x → nu x x refl ≡ idEquiv (El x)
-nu-refl x = equivEq (nu x x refl) (idEquiv (El x)) reg
-
-un-nu : ∀ x y (p : x ≡ y) → un x y (nu x y p) ≡ p
-un-nu x y p
-  = J (λ z q → un x z (nu x z q) ≡ q) (cong (un x x) (nu-refl x) ∙ un-refl x) p
+  nu : ∀ x y → x ≡ y → El x ≃ El y
+  nu x y p = transportEquiv (cong El p)
+
+  cong-un-te
+    : ∀ x y (p : El x ≡ El y)
+    → cong El (un x y (transportEquiv p)) ≡ p
+  cong-un-te x y p
+    = comp (transportEquiv p) ∙ uaTransportη p
+
+  nu-un : ∀ x y (e : El x ≃ El y) → nu x y (un x y e) ≡ e
+  nu-un x y e
+    = equivEq (nu x y (un x y e)) e λ i z
+        → (cong (λ p → transport p z) (comp e) ∙ uaβ e z) i
+
+  El-un-equiv : ∀ x i → El (un x x (idEquiv _) i) ≃ El x
+  El-un-equiv x i = λ where
+      .fst → transp (λ j → p j) (i ∨ ~ i)
+      .snd → transp (λ j → isEquiv (transp (λ k → p (j ∧ k)) (~ j ∨ i ∨ ~ i)))
+                (i ∨ ~ i) (idIsEquiv T)
+    where
+    T = El (un x x (idEquiv _) i)
+    p : T ≡ El x
+    p j = (comp (idEquiv _) ∙ uaIdEquiv {A = El x}) j i
+
+  un-refl : ∀ x → un x x (idEquiv (El x)) ≡ refl
+  un-refl x i j
+    = hcomp (λ k → λ where
+          (i = i0) → un x x (idEquiv (El x)) j
+          (i = i1) → un x x (idEquiv (El x)) (j ∨ k)
+          (j = i0) → un x x (idEquiv (El x)) (~ i ∨ k)
+          (j = i1) → x)
+        (un (un x x (idEquiv (El x)) (~ i)) x (El-un-equiv x (~ i)) j)
+
+  nu-refl : ∀ x → nu x x refl ≡ idEquiv (El x)
+  nu-refl x = equivEq (nu x x refl) (idEquiv (El x)) reg
+
+  un-nu : ∀ x y (p : x ≡ y) → un x y (nu x y p) ≡ p
+  un-nu x y p
+    = J (λ z q → un x z (nu x z q) ≡ q) (cong (un x x) (nu-refl x) ∙ un-refl x) p
+
+open UU-Lemmas
+open Iso
+
+equivIso : ∀ s t → Iso (s ≡ t) (El s ≃ El t)
+equivIso s t .fun = nu s t
+equivIso s t .inv = un s t
+equivIso s t .rightInv = nu-un s t
+equivIso s t .leftInv = un-nu s t
+
+pathIso : ∀ s t → Iso (s ≡ t) (El s ≡ El t)
+pathIso s t .fun = cong El
+pathIso s t .inv = un s t ∘ transportEquiv
+pathIso s t .rightInv = cong-un-te s t
+pathIso s t .leftInv = un-nu s t
 
 minivalence : ∀{s t} → (s ≡ t) ≃ (El s ≃ El t)
-minivalence {s} {t} = isoToEquiv mini
-  where
-  open Iso
-  mini : Iso (s ≡ t) (El s ≃ El t)
-  mini .fun = nu s t
-  mini .inv = un s t
-  mini .rightInv = nu-un s t
-  mini .leftInv = un-nu s t
+minivalence {s} {t} = isoToEquiv (equivIso s t)
 
 path-reflection : ∀{s t} → (s ≡ t) ≃ (El s ≡ El t)
-path-reflection {s} {t} = isoToEquiv reflect
-  where
-  open Iso
-  reflect : Iso (s ≡ t) (El s ≡ El t)
-  reflect .fun = cong El
-  reflect .inv = un s t ∘ transportEquiv
-  reflect .rightInv = cong-un-te s t
-  reflect .leftInv = un-nu s t
+path-reflection {s} {t} = isoToEquiv (pathIso s t)
 
 isEmbeddingEl : isEmbedding El
 isEmbeddingEl s t = snd path-reflection