hlevel of sum types (#141)

* no need for separate lift file

* clean up list

* hlevel of sum types

Cubical/Data/Everything.agda

@@ -13,4 +13,5 @@ open import Cubical.Data.Unit public
 open import Cubical.Data.Sigma public
 open import Cubical.Data.DiffInt public
 open import Cubical.Data.Group public hiding (_≃_)
-open import Cubical.Data.HomotopyGroup public
+open import Cubical.Data.HomotopyGroup public
+open import Cubical.Data.List public

Cubical/Data/List.agda

@@ -1,106 +1,5 @@
 {-# OPTIONS --cubical --safe #-}
 module Cubical.Data.List where
 
-open import Agda.Builtin.List
-open import Cubical.Core.Everything
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Prelude
-open import Cubical.Data.Empty
-open import Cubical.Data.Lift
-open import Cubical.Data.Nat
-open import Cubical.Data.Prod
-open import Cubical.Data.Unit
-
-module _ {ℓ} {A : Type ℓ} where
-
-  infixr 5 _++_
-
-  [_] : A → List A
-  [ a ] = a ∷ []
-
-  _++_ : List A → List A → List A
-  [] ++ ys = ys
-  (x ∷ xs) ++ ys = x ∷ xs ++ ys
-
-  rev : List A → List A
-  rev [] = []
-  rev (x ∷ xs) = rev xs ++ [ x ]
-
-  ++-unit-r : (xs : List A) → xs ++ [] ≡ xs
-  ++-unit-r [] = refl
-  ++-unit-r (x ∷ xs) = cong (_∷_ x) (++-unit-r xs)
-
-  ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
-  ++-assoc [] ys zs = refl
-  ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
-
-  rev-++ : (xs ys : List A) → rev (xs ++ ys) ≡ rev ys ++ rev xs
-  rev-++ [] ys = sym (++-unit-r (rev ys))
-  rev-++ (x ∷ xs) ys =
-    cong (λ zs → zs ++ [ x ]) (rev-++ xs ys)
-    ∙ ++-assoc (rev ys) (rev xs) [ x ]
-
-  rev-rev : (xs : List A) → rev (rev xs) ≡ xs
-  rev-rev [] = refl
-  rev-rev (x ∷ xs) = rev-++ (rev xs) [ x ] ∙ cong (_∷_ x) (rev-rev xs)
-
--- Path space of list type
-module ListPath {ℓ} {A : Type ℓ} where
-
-  Cover : List A → List A → Type ℓ
-  Cover [] [] = Lift Unit
-  Cover [] (_ ∷ _) = Lift ⊥
-  Cover (_ ∷ _) [] = Lift ⊥
-  Cover (x ∷ xs) (y ∷ ys) = (x ≡ y) × Cover xs ys
-
-  reflCode : ∀ xs → Cover xs xs
-  reflCode [] = lift tt
-  reflCode (_ ∷ xs) = refl , reflCode xs
-
-  encode : ∀ xs ys → (p : xs ≡ ys) → Cover xs ys
-  encode xs _ = J (λ ys _ → Cover xs ys) (reflCode xs)
-
-  encodeRefl : ∀ xs → encode xs xs refl ≡ reflCode xs
-  encodeRefl xs = JRefl (λ ys _ → Cover xs ys) (reflCode xs)
-
-  decode : ∀ xs ys → Cover xs ys → xs ≡ ys
-  decode [] [] _ = refl
-  decode [] (_ ∷ _) (lift ())
-  decode (x ∷ xs) [] (lift ())
-  decode (x ∷ xs) (y ∷ ys) (p , c) = cong₂ _∷_ p (decode xs ys c)
-
-  decodeRefl : ∀ xs → decode xs xs (reflCode xs) ≡ refl
-  decodeRefl [] = refl
-  decodeRefl (x ∷ xs) = cong (cong₂ _∷_ refl) (decodeRefl xs)
-
-  decodeEncode : ∀ xs ys → (p : xs ≡ ys) → decode xs ys (encode xs ys p) ≡ p
-  decodeEncode xs _ =
-    J (λ ys p → decode xs ys (encode xs ys p) ≡ p)
-      (cong (decode xs xs) (encodeRefl xs) ∙ decodeRefl xs)
-
-  isOfHLevelCover : (n : ℕ) (p : isOfHLevel (suc (suc n)) A)
-    (xs ys : List A) → isOfHLevel (suc n) (Cover xs ys)
-  isOfHLevelCover n p [] [] =
-    liftLevel (suc n)
-      (subst (λ m → isOfHLevel m Unit) (+-comm n 1)
-        (hLevelLift n isPropUnit))
-  isOfHLevelCover n p [] (y ∷ ys) =
-    liftLevel (suc n)
-      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
-        (hLevelLift n isProp⊥))
-  isOfHLevelCover n p (x ∷ xs) [] =
-    liftLevel (suc n)
-      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
-        (hLevelLift n isProp⊥))
-  isOfHLevelCover n p (x ∷ xs) (y ∷ ys) =
-    hLevelProd (suc n) (p x y) (isOfHLevelCover n p xs ys)
-
-
-isOfHLevelList : ∀ {ℓ} (n : ℕ) {A : Type ℓ}
-  → isOfHLevel (suc (suc n)) A → isOfHLevel (suc (suc n)) (List A)
-isOfHLevelList n ofLevel xs ys =
-  retractIsOfHLevel (suc n)
-    (ListPath.encode xs ys)
-    (ListPath.decode xs ys)
-    (ListPath.decodeEncode xs ys)
-    (ListPath.isOfHLevelCover n ofLevel xs ys)
+open import Cubical.Data.List.Base public
+open import Cubical.Data.List.Properties public

Cubical/Data/List/Base.agda

@@ -0,0 +1,21 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.List.Base where
+
+open import Agda.Builtin.List
+open import Cubical.Core.Everything
+
+module _ {ℓ} {A : Type ℓ} where
+
+  infixr 5 _++_
+
+  [_] : A → List A
+  [ a ] = a ∷ []
+
+  _++_ : List A → List A → List A
+  [] ++ ys = ys
+  (x ∷ xs) ++ ys = x ∷ xs ++ ys
+
+  rev : List A → List A
+  rev [] = []
+  rev (x ∷ xs) = rev xs ++ [ x ]
+

Cubical/Data/List/Properties.agda

@@ -0,0 +1,93 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.List.Properties where
+
+open import Agda.Builtin.List
+open import Cubical.Core.Everything
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Empty
+open import Cubical.Data.Nat
+open import Cubical.Data.Prod
+open import Cubical.Data.Unit
+
+open import Cubical.Data.List.Base
+
+module _ {ℓ} {A : Type ℓ} where
+
+  ++-unit-r : (xs : List A) → xs ++ [] ≡ xs
+  ++-unit-r [] = refl
+  ++-unit-r (x ∷ xs) = cong (_∷_ x) (++-unit-r xs)
+
+  ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
+  ++-assoc [] ys zs = refl
+  ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
+
+  rev-++ : (xs ys : List A) → rev (xs ++ ys) ≡ rev ys ++ rev xs
+  rev-++ [] ys = sym (++-unit-r (rev ys))
+  rev-++ (x ∷ xs) ys =
+    cong (λ zs → zs ++ [ x ]) (rev-++ xs ys)
+    ∙ ++-assoc (rev ys) (rev xs) [ x ]
+
+  rev-rev : (xs : List A) → rev (rev xs) ≡ xs
+  rev-rev [] = refl
+  rev-rev (x ∷ xs) = rev-++ (rev xs) [ x ] ∙ cong (_∷_ x) (rev-rev xs)
+
+-- Path space of list type
+module ListPath {ℓ} {A : Type ℓ} where
+
+  Cover : List A → List A → Type ℓ
+  Cover [] [] = Lift Unit
+  Cover [] (_ ∷ _) = Lift ⊥
+  Cover (_ ∷ _) [] = Lift ⊥
+  Cover (x ∷ xs) (y ∷ ys) = (x ≡ y) × Cover xs ys
+
+  reflCode : ∀ xs → Cover xs xs
+  reflCode [] = lift tt
+  reflCode (_ ∷ xs) = refl , reflCode xs
+
+  encode : ∀ xs ys → (p : xs ≡ ys) → Cover xs ys
+  encode xs _ = J (λ ys _ → Cover xs ys) (reflCode xs)
+
+  encodeRefl : ∀ xs → encode xs xs refl ≡ reflCode xs
+  encodeRefl xs = JRefl (λ ys _ → Cover xs ys) (reflCode xs)
+
+  decode : ∀ xs ys → Cover xs ys → xs ≡ ys
+  decode [] [] _ = refl
+  decode [] (_ ∷ _) (lift ())
+  decode (x ∷ xs) [] (lift ())
+  decode (x ∷ xs) (y ∷ ys) (p , c) = cong₂ _∷_ p (decode xs ys c)
+
+  decodeRefl : ∀ xs → decode xs xs (reflCode xs) ≡ refl
+  decodeRefl [] = refl
+  decodeRefl (x ∷ xs) = cong (cong₂ _∷_ refl) (decodeRefl xs)
+
+  decodeEncode : ∀ xs ys → (p : xs ≡ ys) → decode xs ys (encode xs ys p) ≡ p
+  decodeEncode xs _ =
+    J (λ ys p → decode xs ys (encode xs ys p) ≡ p)
+      (cong (decode xs xs) (encodeRefl xs) ∙ decodeRefl xs)
+
+  isOfHLevelCover : (n : ℕ) (p : isOfHLevel (suc (suc n)) A)
+    (xs ys : List A) → isOfHLevel (suc n) (Cover xs ys)
+  isOfHLevelCover n p [] [] =
+    isOfHLevelLift (suc n)
+      (subst (λ m → isOfHLevel m Unit) (+-comm n 1)
+        (hLevelLift n isPropUnit))
+  isOfHLevelCover n p [] (y ∷ ys) =
+    isOfHLevelLift (suc n)
+      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
+        (hLevelLift n isProp⊥))
+  isOfHLevelCover n p (x ∷ xs) [] =
+    isOfHLevelLift (suc n)
+      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
+        (hLevelLift n isProp⊥))
+  isOfHLevelCover n p (x ∷ xs) (y ∷ ys) =
+    hLevelProd (suc n) (p x y) (isOfHLevelCover n p xs ys)
+
+isOfHLevelList : ∀ {ℓ} (n : ℕ) {A : Type ℓ}
+  → isOfHLevel (suc (suc n)) A → isOfHLevel (suc (suc n)) (List A)
+isOfHLevelList n ofLevel xs ys =
+  retractIsOfHLevel (suc n)
+    (ListPath.encode xs ys)
+    (ListPath.decode xs ys)
+    (ListPath.decodeEncode xs ys)
+    (ListPath.isOfHLevelCover n ofLevel xs ys)

Cubical/Data/Nat/Properties.agda

@@ -7,7 +7,6 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Nat.Base
 open import Cubical.Data.Empty
-open import Cubical.Data.Sum
 open import Cubical.Data.Prod.Base
 
 open import Cubical.Relation.Nullary

Cubical/Data/Sum.agda

@@ -2,3 +2,4 @@
 module Cubical.Data.Sum where
 
 open import Cubical.Data.Sum.Base public
+open import Cubical.Data.Sum.Properties public

Cubical/Data/Sum/Properties.agda

@@ -0,0 +1,70 @@
+{-# OPTIONS --cubical --safe #-}
+module Cubical.Data.Sum.Properties where
+
+open import Cubical.Core.Everything
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Empty
+open import Cubical.Data.Nat
+
+open import Cubical.Data.Sum.Base
+
+-- Path space of sum type
+module SumPath {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
+
+  Cover : A ⊎ B → A ⊎ B → Type (ℓ-max ℓ ℓ')
+  Cover (inl a) (inl a') = Lift {j = ℓ-max ℓ ℓ'} (a ≡ a')
+  Cover (inl _) (inr _) = Lift ⊥
+  Cover (inr _) (inl _) = Lift ⊥
+  Cover (inr b) (inr b') = Lift {j = ℓ-max ℓ ℓ'} (b ≡ b')
+
+  reflCode : (c : A ⊎ B) → Cover c c
+  reflCode (inl a) = lift refl
+  reflCode (inr b) = lift refl
+
+  encode : ∀ c c' → c ≡ c' → Cover c c'
+  encode c _ = J (λ c' _ → Cover c c') (reflCode c)
+
+  encodeRefl : ∀ c → encode c c refl ≡ reflCode c
+  encodeRefl c = JRefl (λ c' _ → Cover c c') (reflCode c)
+
+  decode : ∀ c c' → Cover c c' → c ≡ c'
+  decode (inl a) (inl a') (lift p) = cong inl p
+  decode (inl a) (inr b') ()
+  decode (inr b) (inl a') ()
+  decode (inr b) (inr b') (lift q) = cong inr q
+
+  decodeRefl : ∀ c → decode c c (reflCode c) ≡ refl
+  decodeRefl (inl a) = refl
+  decodeRefl (inr b) = refl
+
+  decodeEncode : ∀ c c' → (p : c ≡ c') → decode c c' (encode c c' p) ≡ p
+  decodeEncode c _ =
+    J (λ c' p → decode c c' (encode c c' p) ≡ p)
+      (cong (decode c c) (encodeRefl c) ∙ decodeRefl c)
+
+  isOfHLevelCover : (n : ℕ)
+    → isOfHLevel (suc (suc n)) A
+    → isOfHLevel (suc (suc n)) B
+    → ∀ c c' → isOfHLevel (suc n) (Cover c c')
+  isOfHLevelCover n p q (inl a) (inl a') = isOfHLevelLift (suc n) (p a a')
+  isOfHLevelCover n p q (inl a) (inr b') =
+    isOfHLevelLift (suc n)
+    (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
+      (hLevelLift n isProp⊥))
+  isOfHLevelCover n p q (inr b) (inl a') =
+    isOfHLevelLift (suc n)
+      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
+        (hLevelLift n isProp⊥))
+  isOfHLevelCover n p q (inr b) (inr b') = isOfHLevelLift (suc n) (q b b')
+
+isOfHLevelSum : ∀ {ℓ ℓ'} (n : ℕ) {A : Type ℓ} {B : Type ℓ'}
+  → isOfHLevel (suc (suc n)) A
+  → isOfHLevel (suc (suc n)) B
+  → isOfHLevel (suc (suc n)) (A ⊎ B)
+isOfHLevelSum n lA lB c c' =
+  retractIsOfHLevel (suc n)
+    (SumPath.encode c c')
+    (SumPath.decode c c')
+    (SumPath.decodeEncode c c')
+    (SumPath.isOfHLevelCover n lA lB c c')

Cubical/Foundations/HLevels.agda

@@ -276,3 +276,6 @@ isContrPartial→isContr {A = A} extend law
             u : Partial φ A
             u = λ { (i = i0) → ex ; (i = i1) → y }
             v = extend φ u
+
+isOfHLevelLift : ∀ {ℓ ℓ'} (n : ℕ) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A)
+isOfHLevelLift n = retractIsOfHLevel n lower lift λ _ → refl