Merge pull request #900 from kangrongji/dep-ua

A Dependent Version of Univalence

Cubical/Foundations/Equiv/Dependent.agda

@@ -17,6 +17,7 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Transport
 
 private
   variable
@@ -166,7 +167,7 @@ fiberIso→IsoOver isom .leftInv  a = isom a .leftInv
 -- Only half-adjoint equivalence can be lifted.
 -- This is another clue that HAE is more natural than isomorphism.
 
-open isHAEquiv
+open isHAEquiv renaming (g to inv)
 
 pullbackIsoOver :
   {ℓA ℓB ℓP : Level}
@@ -222,3 +223,144 @@ equivOver→IsoOver {P = P} {Q = Q} e f equiv = w
   w .inv = isom .inv
   w .rightInv = isom .rightInv
   w .leftInv  = isom .leftInv
+
+
+-- Turn isomorphism over HAE into relative equivalence,
+-- i.e. the inverse of the previous precedure.
+
+isoToEquivOver :
+  {A : Type ℓ } {P : A → Type ℓ'' }
+  {B : Type ℓ'} {Q : B → Type ℓ'''}
+  (f : A → B) (hae : isHAEquiv f)
+  (isom' : IsoOver (isHAEquiv→Iso hae) P Q)
+  → isEquivOver {Q = Q} (isom' .fun)
+isoToEquivOver {A = A} {P} {Q = Q} f hae isom' a = isoToEquiv (fibiso a) .snd
+  where
+  isom = isHAEquiv→Iso hae
+  finv = isom .inv
+
+  fibiso : (a : A) → Iso (P a) (Q (f a))
+  fibiso a .fun = isom' .fun a
+  fibiso a .inv x = transport (λ i → P (isom .leftInv a i)) (isom' .inv (f a) x)
+  fibiso a .leftInv  x = fromPathP (isom' .leftInv _ _)
+  fibiso a .rightInv x =
+    sym (substCommSlice _ _ (isom' .fun) _ _)
+    ∙ cong (λ p → subst Q p (isom' .fun _ (isom' .inv _ x))) (hae .com a)
+    ∙ fromPathP (isom' .rightInv _ _)
+
+
+-- Half-adjoint equivalence over half-adjoint equivalence
+
+record isHAEquivOver {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'}
+  (hae : HAEquiv A B)(P : A → Type ℓ'')(Q : B → Type ℓ''')
+  (fun : mapOver (hae .fst) P Q)
+  : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓ'' ℓ''')) where
+  field
+    inv  : mapOver (hae .snd .inv) Q P
+    rinv : sectionOver (hae .snd .rinv) fun inv
+    linv : retractOver (hae .snd .linv) fun inv
+    com  : ∀ {a} b → SquareP (λ i j → Q (hae .snd .com a i j))
+      (λ i → fun _ (linv _ b i)) (rinv _ (fun _ b))
+      (refl {x = fun _ (inv _ (fun a b))}) (refl {x = fun a b})
+
+open isHAEquivOver
+
+HAEquivOver : (P : A → Type ℓ'')(Q : B → Type ℓ''')(hae : HAEquiv A B) → Type _
+HAEquivOver P Q hae = Σ[ f ∈ mapOver (hae .fst) P Q ] isHAEquivOver hae P Q f
+
+
+-- forget the coherence square to get an dependent isomorphism
+
+isHAEquivOver→isIsoOver :
+  {hae : HAEquiv A B} (hae' : HAEquivOver P Q hae)
+  → IsoOver (isHAEquiv→Iso (hae .snd)) P Q
+isHAEquivOver→isIsoOver hae' .fun = hae' .fst
+isHAEquivOver→isIsoOver hae' .inv = hae' .snd .inv
+isHAEquivOver→isIsoOver hae' .leftInv  = hae' .snd .linv
+isHAEquivOver→isIsoOver hae' .rightInv = hae' .snd .rinv
+
+
+-- A dependent version of `isoToHAEquiv`
+
+IsoOver→HAEquivOver :
+  {isom : Iso A B}
+  → (isom' : IsoOver isom P Q)
+  → isHAEquivOver (iso→HAEquiv isom) P Q (isom' .fun)
+IsoOver→HAEquivOver {A = A} {P = P} {Q = Q} {isom = isom} isom' = w
+  where
+  f = isom .fun
+  g = isom .inv
+  ε = isom .rightInv
+  η = isom .leftInv
+
+  f' = isom' .fun
+  g' = isom' .inv
+  ε' = isom' .rightInv
+  η' = isom' .leftInv
+
+  sq : _ → I → I → _
+  sq b i j =
+    hfill (λ j → λ
+      { (i = i0) → ε (f (g b)) j
+      ; (i = i1) → ε b j })
+    (inS (f (η (g b) i))) j
+
+  Hfa≡fHa : (f : A → A) (H : ∀ a → f a ≡ a) → ∀ a → H (f a) ≡ cong f (H a)
+  Hfa≡fHa f H =
+    J (λ f p → ∀ a → funExt⁻ (sym p) (f a) ≡ cong f (funExt⁻ (sym p) a))
+      (λ a → refl) (sym (funExt H))
+
+  Hfa≡fHaRefl : Hfa≡fHa (idfun _) (λ _ → refl) ≡ λ _ → refl
+  Hfa≡fHaRefl =
+    JRefl {x = idfun _}
+      (λ f p → ∀ a → funExt⁻ (sym p) (f a) ≡ cong f (funExt⁻ (sym p) a))
+      (λ a → refl)
+
+  Hfa≡fHaOver : (f : A → A) (H : ∀ a → f a ≡ a)
+    (f' : mapOver f P P) (H' : ∀ a b → PathP (λ i → P (H a i)) (f' _ b) b)
+    → ∀ a b → SquareP (λ i j →
+      P (Hfa≡fHa f H a i j)) (H' _ (f' _ b)) (λ i → f' _ (H' _ b i)) refl refl
+  Hfa≡fHaOver f H f' H' =
+   JDep {B = λ f → mapOver f P P}
+    (λ f p f' p' → ∀ a b
+      → SquareP (λ i j → P (Hfa≡fHa f (funExt⁻ (sym p)) a i j))
+          (λ i → p' (~ i) _ (f' _ b)) (λ i → f' _ (p' (~ i) _ b))
+          (refl {x = f' _ (f' _ b)}) (refl {x = f' _ b}))
+    (λ a b →
+      transport (λ t → SquareP (λ i j → P (Hfa≡fHaRefl (~ t) a i j))
+        (refl {x = b}) refl refl refl) refl)
+    (sym (funExt H)) (λ i a b → H' a b (~ i))
+
+  cube : _ → I → I → I → _
+  cube a i j k =
+    hfill (λ k → λ
+      { (i = i0) → ε (f (η a j)) k
+      ; (j = i0) → ε (f (g (f a))) k
+      ; (j = i1) → ε (f a) k})
+    (inS (f (Hfa≡fHa (λ x → g (f x)) η a (~ i) j))) k
+
+  w : isHAEquivOver _ _ _ _
+  w .inv  = isom' .inv
+  w .linv = isom' .leftInv
+  w .rinv b x i =
+    comp (λ j → Q (sq b i j))
+    (λ j → λ
+      { (i = i0) → ε' _ (f' _ (g' _ x)) j
+      ; (i = i1) → ε' _ x j })
+    (f' _ (η' _ (g' _ x) i))
+  w. com {a} b i j =
+    comp (λ k → Q (cube a i j k))
+    (λ k → λ
+      { (i = i0) → ε' _ (f' _ (η' _ b j)) k
+      ; (j = i0) → ε' _ (f' _ (g' _ (f' _ b))) k
+      ; (j = i1) → ε' _ (f' _ b) k})
+    (f' _ (Hfa≡fHaOver _ η _ η' a b (~ i) j))
+
+
+-- transform an isomorphism over some isomorphism to an isomorphism over its half-adjoint-ization
+
+IsoOverIso→IsoOverHAEquiv :
+  {isom : Iso A B} (isom' : IsoOver isom P Q)
+  → IsoOver (isHAEquiv→Iso (iso→HAEquiv isom .snd)) P Q
+IsoOverIso→IsoOverHAEquiv isom' =
+  isHAEquivOver→isIsoOver (_ , IsoOver→HAEquivOver isom')

Cubical/Foundations/Equiv/HalfAdjoint.agda

@@ -13,10 +13,7 @@ module Cubical.Foundations.Equiv.HalfAdjoint where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.Function
 open import Cubical.Foundations.GroupoidLaws
-open import Cubical.Foundations.Path
 
 private
   variable

Cubical/Foundations/Everything.agda

@@ -44,6 +44,7 @@ open import Cubical.Foundations.Structure public
 open import Cubical.Foundations.Transport public
 open import Cubical.Foundations.Univalence public
 open import Cubical.Foundations.Univalence.Universe
+open import Cubical.Foundations.Univalence.Dependent
 open import Cubical.Foundations.GroupoidLaws public
 open import Cubical.Foundations.Isomorphism public
 open import Cubical.Foundations.CartesianKanOps

Cubical/Foundations/Prelude.agda

@@ -325,6 +325,7 @@ _≡$S_ = funExtS⁻
 -- J for paths and its computation rule
 
 module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
+
   J : (p : x ≡ y) → P y p
   J p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
 
@@ -341,6 +342,17 @@ module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
 
 -- Multi-variable versions of J
 
+module _ {x : A}
+  {B : A → Type ℓ''} {b : B x}
+  (P : (y : A) (p : x ≡ y) (z : B y) (q : PathP (λ i → B (p i)) b z) → Type ℓ'')
+  (d : P _ refl _ refl) where
+
+  JDep : {y : A} (p : x ≡ y) {z : B y} (q : PathP (λ i → B (p i)) b z) → P _ p _ q
+  JDep _ q = transport (λ i → P _ _ _ (λ j → q (i ∧ j))) d
+
+  JDepRefl : JDep refl refl ≡ d
+  JDepRefl = transportRefl d
+
 module _ {x : A}
   {P : (y : A) → x ≡ y → Type ℓ'} {d : (y : A) (p : x ≡ y) → P y p}
   (Q : (y : A) (p : x ≡ y) (z : P y p) → d y p ≡ z → Type ℓ'')
@@ -359,6 +371,7 @@ module _ {x : A}
 -- A prefix operator version of J that is more suitable to be nested
 
 module _ {P : ∀ y → x ≡ y → Type ℓ'} (d : P x refl) where
+
   J>_ : ∀ y → (p : x ≡ y) → P y p
   J>_ _ p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d
 

Cubical/Foundations/Transport.agda

@@ -134,17 +134,17 @@ transportComposite : ∀ {ℓ} {A B C : Type ℓ} (p : A ≡ B) (q : B ≡ C) (x
 transportComposite = substComposite (λ D → D)
 
 -- substitution commutes with morphisms in slices
-substCommSlice : ∀ {ℓ ℓ′} {A : Type ℓ}
-                   → (B C : A → Type ℓ′)
+substCommSlice : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ}
+                   → (B : A → Type ℓ') (C : A → Type ℓ'')
                    → (F : ∀ a → B a → C a)
                    → {x y : A} (p : x ≡ y) (u : B x)
                    → subst C p (F x u) ≡ F y (subst B p u)
 substCommSlice B C F p Bx a =
   transport-fillerExt⁻ (cong C p) a (F _ (transport-fillerExt (cong B p) a Bx))
 
-constSubstCommSlice : ∀ {ℓ ℓ'} {A : Type ℓ}
+constSubstCommSlice : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ}
                    → (B : A → Type ℓ')
-                   → (C : Type ℓ')
+                   → (C : Type ℓ'')
                    → (F : ∀ a → B a → C)
                    → {x y : A} (p : x ≡ y) (u : B x)
                    →  (F x u) ≡ F y (subst B p u)

Cubical/Foundations/Univalence/Dependent.agda

@@ -0,0 +1,48 @@
+{-
+
+Dependent Version of Univalence
+
+The univalence corresponds to the dependent equivalences/isomorphisms,
+c.f. `Cubical.Foundations.Equiv.Dependent`.
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.Foundations.Univalence.Dependent where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint
+open import Cubical.Foundations.Equiv.Dependent
+open import Cubical.Foundations.Univalence
+
+private
+  variable
+    ℓ ℓ' : Level
+
+
+-- Dependent Univalence
+
+-- A quicker proof provided by @ecavallo: uaOver e F equiv = ua→ (λ a → ua (_ , equiv a))
+-- Unfortunately it gives a larger term overall.
+uaOver :
+  {A B : Type ℓ} {P : A → Type ℓ'} {Q : B → Type ℓ'}
+  (e : A ≃ B) (F : mapOver (e .fst) P Q)
+  (equiv : isEquivOver {P = P} {Q = Q} F)
+  → PathP (λ i → ua e i → Type ℓ') P Q
+uaOver {A = A} {P = P} {Q} e F equiv i x =
+  hcomp (λ j → λ
+    { (i = i0) → ua (_ , equiv x) (~ j)
+    ; (i = i1) → Q x })
+  (Q (unglue (i ∨ ~ i) x))
+
+
+-- Dependent `isoToPath`
+
+open isHAEquiv
+
+isoToPathOver :
+  {A B : Type ℓ} {P : A → Type ℓ'} {Q : B → Type ℓ'}
+  (f : A → B) (hae : isHAEquiv f)
+  (isom : IsoOver (isHAEquiv→Iso hae) P Q)
+  → PathP (λ i → ua (_ , isHAEquiv→isEquiv hae) i → Type ℓ') P Q
+isoToPathOver f hae isom = uaOver _ _ (isoToEquivOver f hae isom)