{-# 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.Relation.Nullary 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) private variable ℓ : Level A : Type ℓ caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B caseList n _ [] = n caseList _ c (_ ∷ _) = c safe-head : A → List A → A safe-head x [] = x safe-head _ (x ∷ _) = x safe-tail : List A → List A safe-tail [] = [] safe-tail (_ ∷ xs) = xs cons-inj₁ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y cons-inj₁ {x = x} p = cong (safe-head x) p cons-inj₂ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → xs ≡ ys cons-inj₂ = cong safe-tail ¬cons≡nil : ∀ {x : A} {xs} → ¬ (x ∷ xs ≡ []) ¬cons≡nil {A = A} p = lower (subst (caseList (Lift ⊥) (List A)) p []) ¬nil≡cons : ∀ {x : A} {xs} → ¬ ([] ≡ x ∷ xs) ¬nil≡cons {A = A} p = lower (subst (caseList (List A) (Lift ⊥)) p []) ¬snoc≡nil : ∀ {x : A} {xs} → ¬ (xs ∷ʳ x ≡ []) ¬snoc≡nil {xs = []} contra = ¬cons≡nil contra ¬snoc≡nil {xs = x ∷ xs} contra = ¬cons≡nil contra ¬nil≡snoc : ∀ {x : A} {xs} → ¬ ([] ≡ xs ∷ʳ x) ¬nil≡snoc contra = ¬snoc≡nil (sym contra) cons≡rev-snoc : (x : A) → (xs : List A) → x ∷ rev xs ≡ rev (xs ∷ʳ x) cons≡rev-snoc _ [] = refl cons≡rev-snoc x (y ∷ ys) = λ i → cons≡rev-snoc x ys i ++ y ∷ [] nil≡nil-isContr : isContr (Path (List A) [] []) nil≡nil-isContr = refl , ListPath.decodeEncode [] [] list≡nil-isProp : {xs : List A} → isProp (xs ≡ []) list≡nil-isProp {xs = []} = hLevelSuc 0 _ nil≡nil-isContr list≡nil-isProp {xs = x ∷ xs} = λ p _ → ⊥-elim (¬cons≡nil p) discreteList : Discrete A → Discrete (List A) discreteList eqA [] [] = yes refl discreteList eqA [] (y ∷ ys) = no ¬nil≡cons discreteList eqA (x ∷ xs) [] = no ¬cons≡nil discreteList eqA (x ∷ xs) (y ∷ ys) with eqA x y | discreteList eqA xs ys ... | yes p | yes q = yes (λ i → p i ∷ q i) ... | yes _ | no ¬q = no (λ p → ¬q (cons-inj₂ p)) ... | no ¬p | _ = no (λ q → ¬p (cons-inj₁ q))