diff --git a/Cubical/Algebra/Group/Free.agda b/Cubical/Algebra/Group/Free.agda new file mode 100644 index 0000000000..99c26a9b41 --- /dev/null +++ b/Cubical/Algebra/Group/Free.agda @@ -0,0 +1,507 @@ +{-# OPTIONS --safe #-} + +{- + +This module introduces a way to represent elements of free groups as lists of pairs ([𝟚× A]), where A identifies generators and Bool differentiates a generator from its inverse. + + +The definition of `_⇊1g` encodes the concept of a word being equivalent to the identity element in a free group. It includes three constructors: + - The trivial case `[]` represents the identity itself. + - The `cj` constructor signifies conjugation by a generator, indicating that a word extended by a generator and its inverse is still equivalent to the identity. + - Lastly, the `_·_` constructor asserts that if two words are each equivalent to the identity, their concatenation will also be equivalent to the identity, preserving the identity property under the group operation. + +Then, a `_·_⁻¹≡ε relation`, defined as `λ xs ys → (xs ++ invLi ys) ⇊1g` captures the relationship where the concatenation of a word with the inverse of another equates to the group identity. + +By quotienting by _·_⁻¹≡ε, resulting in the List/↘↙group, a group structure on equivalence classes of lists is established. Here, concatenation acts as the group operation, hence forming the foundation for the free group constructed over A. + +Given that _·_⁻¹≡ε functions is equivalence relation, it permits the retrieval of this relationship from paths in the quotient. This feature facilitates the proof of the uniqueness of the normal form in `Cubical.HITs.FreeGroup.NormalForm`. + +In the Discrete module, the presence of decidable equality on the type of generators (A) enables the definition of groups without requiring truncation. This utility is used in `Cubical.HITs.Bouquet.Discrete` to demonstrate that a bouquet over a discrete type is an hGroupoid without truncation. + +-} + +module Cubical.Algebra.Group.Free where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Structure +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.HLevels + +open import Cubical.Data.Bool as 𝟚 hiding (_≤_) +open import Cubical.Data.Nat as ℕ hiding (_·_) +open import Cubical.Data.Nat.Order.Recursive as OR +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Sum as ⊎ +open import Cubical.Data.Sigma +open import Cubical.Data.List as Li + +open import Cubical.Relation.Nullary +open import Cubical.Relation.Binary + +open import Cubical.Functions.Involution + +open import Cubical.Algebra.Group + +open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/₂_ ; [_] to [_]/) + + + +private + variable + ℓ : Level + +[𝟚×_] : (A : Type ℓ) → Type ℓ +[𝟚×_] = List ∘ (Bool ×_) + +module NormalForm (A : Type ℓ) where + + -- Below we are defining predicate `HasRedex` over `List (Bool × A)` + -- basing it on presence of sublist - REDucible EXpression of form [(b , x) , (not b , x)] + + not₁ : (Bool × A) → (Bool × A) + not₁ = map-fst not + + not₁not₁ : ∀ x → not₁ (not₁ x) ≡ x + not₁not₁ (x , y) = cong (_, y) (notnot x) + + IsRedex : Bool × A → Bool × A → Type ℓ + IsRedex x x' = x ≡ not₁ x' + + symIsRedex : ∀ x y → IsRedex x y → IsRedex y x + symIsRedex x y p = sym (not₁not₁ _) ∙ cong not₁ (sym p) + + WillReduce : Bool → A → (xs : [𝟚× A ]) → Type ℓ + WillReduce _ _ [] = ⊥* + WillReduce b x (h ∷ _) = IsRedex (b , x) h + + HeadIsRedex : [𝟚× A ] → Type ℓ + HeadIsRedex [] = ⊥* + HeadIsRedex ((b , a) ∷ xs) = WillReduce b a xs + + HasRedex : [𝟚× A ] → Type ℓ + HasRedex [] = ⊥* + HasRedex xs@(_ ∷ xs') = HeadIsRedex xs ⊎ HasRedex xs' + + HasRedex∷ʳ : ∀ {xs} {x} → HasRedex xs → HasRedex (xs ∷ʳ x) + HasRedex∷ʳ {x₂ ∷ xs} (inr x₁) = inr (HasRedex∷ʳ x₁) + HasRedex∷ʳ {x₂ ∷ x₃ ∷ xs} (inl x₁) = inl x₁ + + HasRedex++ : ∀ xs ys → HasRedex xs → HasRedex (xs ++ ys) + HasRedex++ (x₁ ∷ xs) ys (inr x) = inr (HasRedex++ xs ys x) + HasRedex++ (x₁ ∷ x₂ ∷ xs) ys (inl x) = inl x + + ++HasRedex : ∀ xs ys → HasRedex ys → HasRedex (xs ++ ys) + ++HasRedex [] ys x = x + ++HasRedex (x₁ ∷ xs) ys x = + inr (++HasRedex xs ys x) + + -- We use absence of redexes as property of representing normalised term + + IsNormalised : [𝟚× A ] → Type ℓ + IsNormalised xs = (¬ HasRedex xs) + + isPropIsNormalised : ∀ xs → isProp (IsNormalised xs) + isPropIsNormalised xs = isProp¬ _ + + + IsNormalised[] : IsNormalised [] + IsNormalised[] = lower + + IsNormalised[x] : ∀ x → IsNormalised [ x ] + IsNormalised[x] _ = ⊎.rec lower lower + + IsNormalisedTail : ∀ xs → IsNormalised xs → IsNormalised (tail xs) + IsNormalisedTail [] n = n + IsNormalisedTail (x ∷ xs) = _∘ inr + + ¬IsRedex→IsNormalisedPair : + ∀ {x x'} → ¬ IsRedex x x' → IsNormalised (x ∷ [ x' ]) + ¬IsRedex→IsNormalisedPair {x' = x'} ¬ir = ⊎.rec ¬ir (IsNormalised[x] x') + + invLi : [𝟚× A ] → [𝟚× A ] + invLi = rev ∘ Li.map (map-fst not) + + invLi++ : ∀ xs ys → invLi (xs ++ ys) ≡ + invLi ys ++ invLi xs + invLi++ xs ys = + sym (cong rev (map++ _ xs ys)) ∙ + rev-++ (Li.map _ xs) (Li.map _ ys) + + invol-invLi : isInvolution invLi + invol-invLi xs = + sym (rev-map-comm (map-fst not) (invLi xs)) ∙ + cong (Li.map (map-fst not)) + (rev-rev (Li.map (map-fst not) xs)) + ∙ map-∘ (map-fst not) (map-fst not) xs ∙ + (λ i → Li.map (map-fst (λ x → notnot x i) ) xs) ∙ map-id xs + + HasRedexInvLi : ∀ {xs} → HasRedex xs → HasRedex (invLi xs) + HasRedexInvLi {_ ∷ []} x = x + HasRedexInvLi {x₁ ∷ x₂ ∷ xs} = ⊎.rec + (subst HasRedex (sym (++-assoc (invLi xs) _ _)) + ∘S ++HasRedex (invLi xs) (_ ∷ _) + ∘S inl ∘S cong not₁ ∘S symIsRedex _ _ ) + (HasRedex∷ʳ ∘S HasRedexInvLi) + + + IsNormalisedInvLi : ∀ {xs} → IsNormalised xs ≃ IsNormalised (invLi xs) + IsNormalisedInvLi = propBiimpl→Equiv (isPropIsNormalised _) (isPropIsNormalised _) + (_∘S subst HasRedex (invol-invLi _) ∘S HasRedexInvLi) + (_∘S HasRedexInvLi) + + HasRedexSplit++ : ∀ {xs ys} → HasRedex (xs ++ ys) → + HasRedex (take 1 (rev xs) ++ take 1 ys) ⊎ + (HasRedex xs ⊎ HasRedex ys) + HasRedexSplit++ {[]} = inr ∘ inr + HasRedexSplit++ {x ∷ []} {[]} r = ⊥.rec (IsNormalised[x] x r) + HasRedexSplit++ {x ∷ []} {x₁ ∷ ys} = ⊎.rec (inl ∘ inl) (inr ∘ inr) + HasRedexSplit++ {x ∷ x₁ ∷ xs} {ys} = + ⊎.rec (inr ∘ inl ∘ inl) + (⊎.rec (inl ∘ subst (λ zz → HasRedex (zz ++ take 1 ys)) + (w _ (subst (0 <_) (+-comm 1 _ ∙ sym (length++ (rev xs) _)) _))) + (⊎.rec (inr ∘ inl ∘ inr) (inr ∘ inr) ) ∘S HasRedexSplit++ {x₁ ∷ xs} {ys}) + where + w : ∀ xs → 0 < length xs → take 1 xs ≡ take 1 (xs ++ [ x ]) + w (x ∷ xs) _ = refl + + -- This predicate, is encoding fact that given list reduces to [], + -- meaning that if interpreted as term of free group it would be equall to 1g + + infixl 10 _⇊1g + + data _⇊1g : [𝟚× A ] → Type ℓ where + [] : [] ⇊1g + cj : ∀ x → ∀ xs → xs ⇊1g → (x ∷ (xs ∷ʳ not₁ x) ) ⇊1g + _·_ : ∀ xs ys → xs ⇊1g → ys ⇊1g → (xs ++ ys) ⇊1g + + _r·_ : ∀ {xs ys} → xs ⇊1g → ys ⇊1g → (xs ++ ys) ⇊1g + _r·_ = _·_ _ _ + + ¬⇊1g[len≡1] : ∀ xs → length xs ≡ 1 → ¬ xs ⇊1g + ¬⇊1g[len≡1] .[] x [] = znots x + ¬⇊1g[len≡1] .(_ ∷ (_ ∷ʳ _)) x (cj _ xs _) = + snotz ((+-comm 1 _ ∙ sym (length++ xs _)) ∙ injSuc x) + ¬⇊1g[len≡1] .(xs ++ ys) x ((xs · ys) x₁ x₂) = + ⊎.rec (flip (¬⇊1g[len≡1] ys) x₂ ∘ snd) + ((flip (¬⇊1g[len≡1] xs) x₁ ∘ fst)) + (m+n≡1→m≡0×n≡1⊎m≡1n≡0 {length xs} {length ys} (sym (length++ xs ys) ∙ x)) + + ⇊1gWillReduceView : ∀ b a ys → ys ⇊1g → WillReduce b a ys → + Σ ((Σ _ _⇊1g) × (Σ _ _⇊1g)) + λ ((rl , _) , (rr , _)) → + rl ++ [ b , a ] ++ rr ≡ tail ys + ⇊1gWillReduceView b a .(x ∷ (xs ∷ʳ _)) (cj x xs x₃) x₁ = + ((_ , x₃) , (_ , [])) , cong (xs ∷ʳ_) x₁ + ⇊1gWillReduceView b a .([] ++ ys) (([] · ys) x x₂) x₁ = + ⇊1gWillReduceView b a ys x₂ x₁ + ⇊1gWillReduceView b a .((_ ∷ _) ++ ys) ((xs@(_ ∷ _) · ys) x x₂) x₁ = + let (((rl , rlR) , (rr , rrR)) , p) = ⇊1gWillReduceView b a xs x x₁ + in ((_ , rlR) , (_ , (_ · _) rrR x₂)) , + sym (++-assoc rl _ _) ∙ cong (_++ ys) p + + ⇊1g⇒HasRedex : ∀ xs → 0 < length xs → xs ⇊1g → HasRedex xs + ⇊1g⇒HasRedex .(x₁ ∷ ([] ∷ʳ not₁ x₁)) x (cj x₁ [] x₂) = + inl (symIsRedex _ _ refl) + ⇊1g⇒HasRedex .(x₁ ∷ ((x₃ ∷ xs) ∷ʳ not₁ x₁)) x (cj x₁ (x₃ ∷ xs) x₂) = + inr (HasRedex∷ʳ (⇊1g⇒HasRedex _ _ x₂)) + ⇊1g⇒HasRedex .([] ++ ys) x (([] · ys) x₁ x₂) = ⇊1g⇒HasRedex _ x x₂ + ⇊1g⇒HasRedex .((x₃ ∷ xs) ++ ys) x (((x₃ ∷ xs) · ys) x₁ x₂) = + HasRedex++ _ _ (⇊1g⇒HasRedex _ _ x₁) + + isNormalised⇊1g : ∀ xs → IsNormalised xs → xs ⇊1g → xs ≡ [] + isNormalised⇊1g [] _ _ = refl + isNormalised⇊1g (x₂ ∷ xs) x x₁ = ⊥.rec (x (⇊1g⇒HasRedex _ _ x₁)) + + + ⇊1g-invLi : ∀ {xs} → xs ⇊1g → (invLi xs) ⇊1g + ⇊1g-invLi [] = [] + ⇊1g-invLi (cj x xs x₁) = + subst _⇊1g (cong (_∷ invLi (x ∷ xs)) (sym (not₁not₁ _) ) + ∙ cong (_∷ʳ _) (sym (invLi++ xs [ not₁ x ]))) (cj x _ (⇊1g-invLi x₁)) + ⇊1g-invLi ((xs · ys) x x₁) = + subst _⇊1g (sym (invLi++ xs ys)) (⇊1g-invLi x₁ r· ⇊1g-invLi x) + + ⇊1gRot : ∀ xs → xs ⇊1g → _⇊1g (rot xs) + ⇊1gRot [] x = [] + ⇊1gRot xs@(x'@(b , a) ∷ xs') x = + let (((rl , rlR) , (rr , rrR)) , p) = ⇊1gWillReduceView (not b) a xs x refl + in subst _⇊1g ((λ i → (++-assoc rl ([ not b , a ] ++ rr) + [ not₁not₁ x' i ]) (~ i)) ∙ cong (_∷ʳ x') p) + (rlR r· cj (not b , a) _ rrR) + + ⇊1g++comm : ∀ xs ys → (xs ++ ys) ⇊1g → (ys ++ xs) ⇊1g + ⇊1g++comm [] ys = subst _⇊1g (sym (++-unit-r ys)) + ⇊1g++comm (x₁ ∷ xs) ys x = + subst _⇊1g (++-assoc ys _ _) + (⇊1g++comm xs _ (subst _⇊1g (++-assoc xs _ _) (⇊1gRot _ x))) + + pop⇊1gHead : ∀ {xs} → HeadIsRedex xs → xs ⇊1g → _⇊1g (tail (tail xs)) + pop⇊1gHead x (cj x₁ [] r) = [] + pop⇊1gHead x (cj x₁ (x₂ ∷ xs) r) = + subst (_⇊1g ∘ (xs ∷ʳ_)) (symIsRedex _ _ x) (⇊1gRot _ r) + pop⇊1gHead x (([] · ys) r r₁) = pop⇊1gHead x r₁ + pop⇊1gHead x (((x₁ ∷ []) · ys) r r₁) = ⊥.rec (¬⇊1g[len≡1] [ x₁ ] refl r) + pop⇊1gHead x (((_ ∷ _ ∷ _) · ys) r r₁) = pop⇊1gHead x r r· r₁ + + ⇊1gCJ : ∀ xs ys → _⇊1g (ys ++ xs ++ invLi ys) → xs ⇊1g + ⇊1gCJ xs [] = subst _⇊1g (++-unit-r xs) + ⇊1gCJ xs (x₁ ∷ ys) x = + ⇊1gCJ xs ys (pop⇊1gHead refl + (⇊1g++comm (x₁ ∷ ys ++ xs ++ invLi ys) [ not₁ x₁ ] + (subst _⇊1g (cong (x₁ ∷_) (cong (ys ++_) (sym (++-assoc xs _ _)) + ∙ sym (++-assoc ys _ _))) x))) + + nf-uR : ∀ xs ys + → IsNormalised (invLi xs) + → IsNormalised ys + → (invLi xs ++ ys) ⇊1g → xs ≡ ys + nf-uR xs [] nXs x₁ r = sym (invol-invLi xs) ∙ cong invLi + (isNormalised⇊1g _ nXs (subst _⇊1g (++-unit-r _) r)) + nf-uR [] (x₃ ∷ ys) x x₁ x₂ = ⊥.rec (x₁ (⇊1g⇒HasRedex _ _ x₂)) + nf-uR xs@(_ ∷ _) (x₃ ∷ ys) nXs nYs r = + let ww = subst _⇊1g (cong (x₃ ∷_) (sym (++-assoc ys _ _))) + (⇊1g++comm (invLi xs) _ r) + www = subst (0 <_) + (sym (+-suc _ _) + ∙ sym (length++ (invLi xs) _)) _ + in (⊎.rec (⊎.rec (λ p → cong₂ _∷_ + (sym (not₁not₁ _) ∙ sym (symIsRedex _ _ p)) + (nf-uR (tail xs) _ (fst IsNormalisedInvLi + (invEq (IsNormalisedInvLi {xs}) nXs ∘ inr) ) (nYs ∘ inr) + (⇊1g++comm _ (invLi (tail xs)) + (pop⇊1gHead p (⇊1g++comm _ [ _ ] ww))))) + (⊥.rec ∘ IsNormalised[x] x₃) ∘S + subst HasRedex (cong ((_++ _) ∘ take 1) + (rev-rev (Li.map not₁ xs)))) + (⊥.rec ∘ ⊎.rec nXs nYs) + ∘S HasRedexSplit++ {invLi xs} + ∘S ⇊1g⇒HasRedex _ www) r + + infixr 5 _·_⁻¹≡ε + + -- We are defining this relation using record + -- to help later definitions infer implicit arguments. + -- With the help of earlier lemmas, we can prove that it is EquivRel, + -- wich lets us recover witness of this relation from path in SetQuotent + + record _·_⁻¹≡ε (xs ys : _) : Type ℓ where + constructor [_]≡ε + field + ≡ε : (xs ++ invLi ys) ⇊1g + + open _·_⁻¹≡ε public + + open BinaryRelation + open isEquivRel + + ·⁻¹≡ε-refl : isRefl _·_⁻¹≡ε + ·⁻¹≡ε-refl [] = [ [] ]≡ε + ≡ε (·⁻¹≡ε-refl (x ∷ xs)) = + subst _⇊1g (sym (++-assoc [ x ] xs (invLi (x ∷ xs)) ∙ + cong (x ∷_) (sym (++-assoc xs (invLi xs) _)))) + (cj x _ (≡ε (·⁻¹≡ε-refl xs))) + + ·⁻¹≡ε-sym : isSym _·_⁻¹≡ε + ≡ε (·⁻¹≡ε-sym a b [ p ]≡ε) = + subst _⇊1g (invLi++ a (invLi b) ∙ + cong (_++ invLi a) (invol-invLi b)) (⇊1g-invLi p) + + ·⁻¹≡ε-trans : isTrans _·_⁻¹≡ε + ≡ε (·⁻¹≡ε-trans xs ys zs [ p ]≡ε [ q ]≡ε) = + ⇊1g++comm (invLi zs) xs + (⇊1gCJ (invLi zs ++ xs) ys + (subst _⇊1g (++-assoc ys _ _ ∙ + cong (ys ++_) (sym (++-assoc (invLi zs) _ _))) (q r· p))) + + ·⁻¹≡ε-isEquivRel : isEquivRel _·_⁻¹≡ε + reflexive ·⁻¹≡ε-isEquivRel = ·⁻¹≡ε-refl + symmetric ·⁻¹≡ε-isEquivRel = ·⁻¹≡ε-sym + transitive ·⁻¹≡ε-isEquivRel = ·⁻¹≡ε-trans + + ≡→red : ∀ a b → Iso ([ a ]/ ≡ [ b ]/) ∥ a · b ⁻¹≡ε ∥₁ + ≡→red = isEquivRel→TruncIso ·⁻¹≡ε-isEquivRel + + + open Iso + + + _↘↙_ = _·_⁻¹≡ε + + List/↘↙ : Type ℓ + List/↘↙ = _ /₂ _·_⁻¹≡ε + + + -- concatenation of lists, respects `_·_⁻¹≡ε` on both sides, + -- so we can give SetQuotiening by _·_⁻¹≡ε structure of a group + -- by taking concatenation as group operation + + _↘↙++↘↙_ : ∀ {xsL xsR ysL ysR} → + xsL ↘↙ ysL → xsR ↘↙ ysR → + (xsL ++ xsR) ↘↙ (ysL ++ ysR) + ≡ε (_↘↙++↘↙_ {xsL} {xsR} {ysL} {ysR} [ p ]≡ε [ q ]≡ε) = + subst _⇊1g (sym (++-assoc xsL _ _)) + (⇊1g++comm _ xsL + (subst _⇊1g (++-assoc xsR _ _ ∙∙ + (λ i → xsR ++ ++-assoc (invLi ysR) (invLi ysL) xsL (~ i)) ∙∙ + ( λ i → ++-assoc xsR (invLi++ ysL ysR (~ i)) xsL (~ i))) + (q r· ⇊1g++comm xsL _ p))) + + List/↘↙· : List/↘↙ → List/↘↙ → List/↘↙ + List/↘↙· = SQ.rec2 squash/ (λ a b → [ a ++ b ]/) + (λ _ _ c → eq/ _ _ ∘ _↘↙++↘↙ (·⁻¹≡ε-refl c)) + (λ a _ _ → eq/ _ _ ∘ (·⁻¹≡ε-refl a) ↘↙++↘↙_ ) + + List/↘↙GroupStr : GroupStr List/↘↙ + GroupStr.1g List/↘↙GroupStr = [ [] ]/ + GroupStr._·_ List/↘↙GroupStr = List/↘↙· + GroupStr.inv List/↘↙GroupStr = + SQ.rec squash/ ([_]/ ∘ invLi) + λ xs ys → sym ∘S eq/ _ _ ∘S [_]≡ε + ∘S subst (_⇊1g ∘ (invLi ys ++_)) (sym (invol-invLi xs)) + ∘S ⇊1g++comm xs (invLi ys) ∘S ≡ε + + GroupStr.isGroup List/↘↙GroupStr = makeIsGroup squash/ + (SQ.elimProp3 (λ _ _ _ → squash/ _ _) + λ xs _ _ → cong [_]/ (sym (++-assoc xs _ _))) + (SQ.elimProp (λ _ → squash/ _ _) λ xs → cong [_]/ (++-unit-r xs)) + (SQ.elimProp (λ _ → squash/ _ _) λ _ → refl) + (SQ.elimProp (λ _ → squash/ _ _) λ xs → sym (eq/ _ _ + ([ ⇊1g-invLi (≡ε (·⁻¹≡ε-refl xs)) ]≡ε))) + (SQ.elimProp (λ _ → squash/ _ _) λ xs → eq/ _ _ [ + subst _⇊1g (cong (invLi xs ++_) (invol-invLi xs) ∙ + sym (++-unit-r _)) (≡ε (·⁻¹≡ε-refl (invLi xs))) ]≡ε) + + List/↘↙group : Group ℓ + List/↘↙group = _ , List/↘↙GroupStr + + + + module Discrete (_≟_ : Discrete A) where + + -- For discrete set of generators, we can compute normal form, + -- and proove `Iso (Σ _ IsNormalised) List/↘↙` + + isSetA = Discrete→isSet _≟_ + + isSet[𝟚×] = isOfHLevelList 0 (isSet× isSetBool isSetA) + + IsRedex? : ∀ x x' → Dec (IsRedex x x') + IsRedex? _ _ = discreteΣ 𝟚._≟_ (λ _ → _≟_) _ _ + + HeadIsRedex? : ∀ xs → Dec (HeadIsRedex xs) + HeadIsRedex? [] = no lower + HeadIsRedex? (x ∷ []) = no lower + HeadIsRedex? (x ∷ x' ∷ _) = IsRedex? x x' + + preη· : ∀ x xs → Dec (HeadIsRedex (x ∷ xs)) → [𝟚× A ] + preη· _ xs (yes _) = tail xs + preη· x xs (no _) = x ∷ xs + + preη·-N : ∀ {x xs} hir? → IsNormalised xs → IsNormalised (preη· x xs hir?) + preη·-N (yes _) = IsNormalisedTail _ + preη·-N (no ¬p) = ⊎.rec ¬p + + sec-preη· : ∀ x xs p q → IsNormalised xs → preη· (not₁ x) (preη· x xs p) q ≡ xs + sec-preη· x (x₂ ∷ xs) (yes p) (no ¬p) x₁ = + cong (_∷ xs) (sym (symIsRedex _ _ p)) + sec-preη· x (x₂ ∷ x₃ ∷ xs) (yes p) (yes p₁) x₁ = + ⊥.rec (x₁ (inl (symIsRedex _ _ p ∙ p₁))) + sec-preη· x xs (no ¬p) (no ¬p₁) x₁ = ⊥.rec (¬p₁ refl) + sec-preη· x xs (no ¬p) (yes p) _ = refl + + η· : (Bool × A) → [𝟚× A ] → [𝟚× A ] + η· x xs = preη· _ _ (HeadIsRedex? (x ∷ xs)) + + η·∷ : ∀ x xs → (HeadIsRedex (x ∷ xs) → ⊥) → η· x xs ≡ x ∷ xs + η·∷ x xs x₁ = cong (λ u → preη· x xs u) + (≡no (HeadIsRedex? (x ∷ xs)) x₁) + + nη· : (Bool × A) → Σ _ IsNormalised → Σ _ IsNormalised + fst (nη· x x₁) = η· x (fst x₁) + snd (nη· x x₁) = preη·-N (HeadIsRedex? _) (snd x₁) + + + η·iso : (Bool × A) → Iso (Σ [𝟚× A ] IsNormalised) (Σ [𝟚× A ] IsNormalised) + Iso.fun (η·iso x) = nη· x + Iso.inv (η·iso x) = nη· (not₁ x) + Iso.rightInv (η·iso x) b = + Σ≡Prop isPropIsNormalised + (funExt⁻ (cong η· (sym (not₁not₁ x)) ) (η· (not₁ x) (fst b)) + ∙ sec-preη· (not₁ x) _ (HeadIsRedex? _) (HeadIsRedex? _) (snd b)) + Iso.leftInv (η·iso x) a = + Σ≡Prop isPropIsNormalised + (sec-preη· x _ (HeadIsRedex? _) (HeadIsRedex? _) (snd a)) + + η·≃ = isoToEquiv ∘ η·iso + + normalise : ∀ xs → Σ _ λ xs' → + (xs' · xs ⁻¹≡ε) × IsNormalised xs' + normalise = Li.elim ([] , [ [] ]≡ε , lower ) + λ {x} {xs} (xs' , [ u ]≡ε , v) → + let zz : ∀ xs' uu u → (preη· x xs' uu ++ invLi (x ∷ xs)) ⇊1g + zz = + λ { xs' (no ¬p) → subst (_⇊1g ∘S (x ∷_)) (++-assoc xs' _ _) ∘ cj x _ + ; [] (yes ()) + ; (_ ∷ xs') (yes p) → + subst _⇊1g (λ i → ++-assoc xs' (invLi xs) + [ symIsRedex _ _ p i ] i) ∘ ⇊1gRot _ } + h = HeadIsRedex? _ + in _ , [ zz xs' h u ]≡ε , preη·-N h v + + IsoNF : Iso (Σ _ IsNormalised) List/↘↙ + fun IsoNF = [_]/ ∘ fst + Iso.inv IsoNF = + SQ.rec (isSetΣ isSet[𝟚×] (isProp→isSet ∘ isPropIsNormalised)) + ((λ (_ , _ , u) → _ , u) ∘ normalise) + λ _ _ → + let (a' , t , u ) = normalise _ ; (b' , t' , u') = normalise _ + in Σ≡Prop isPropIsNormalised ∘S sym + ∘S nf-uR _ _ (fst (IsNormalisedInvLi {b'}) u') u + ∘S ⇊1g++comm a' (invLi b') ∘S ≡ε + ∘S flip (·⁻¹≡ε-trans _ _ _) (·⁻¹≡ε-sym _ _ t') + ∘S ·⁻¹≡ε-trans _ _ _ t + rightInv IsoNF = SQ.elimProp (λ _ → squash/ _ _) + (eq/ _ _ ∘ fst ∘ snd ∘ normalise) + leftInv IsoNF = Σ≡Prop isPropIsNormalised ∘ uncurry + (Li.elim (λ _ → refl) λ f v → + let lem : ∀ uu → preη· _ _ uu ≡ _ ∷ _ + lem = + λ { (yes p) → ⊥.rec (v (inl (subst (WillReduce _ _) (f (v ∘ inr)) p))) + ; (no ¬p) → refl } + in lem (HeadIsRedex? _) ∙ cong (_ ∷_) (f (v ∘ inr))) + +module NF {ℓ'} {A : Type ℓ} (G : Group ℓ') (η : A → ⟨ G ⟩) where + open NormalForm A + + open GroupStr (snd G) renaming (_·_ to _·fg_) public + + η* : Bool × A → ⟨ G ⟩ + η* (b , a) = (if b then idfun _ else inv) (η a) + + fromList : [𝟚× A ] → ⟨ G ⟩ + fromList = foldr (_·fg_ ∘ η*) 1g + + record NF (g : _) : Type (ℓ-max ℓ ℓ') where + constructor _nf_,_ + field + word : [𝟚× A ] + fromListWord≡ : fromList word ≡ g + isNormalisedWord : IsNormalised word + + + fromList· : ∀ xs ys → fromList (xs ++ ys) ≡ + fromList xs ·fg fromList ys + fromList· [] _ = sym (·IdL _) + fromList· (_ ∷ xs) _ = + cong (_ ·fg_) (fromList· xs _) ∙ + ·Assoc _ _ _ + + redex-ε-η* : ∀ x x' → IsRedex x x' → η* x ·fg η* x' ≡ 1g + redex-ε-η* (false , _) (false , _) = ⊥.rec ∘ false≢true ∘ cong fst + redex-ε-η* (false , x) (true , _) q = + cong (inv (η x) ·fg_) (cong (η) (sym (cong snd q))) ∙ ·InvL (η x) + redex-ε-η* (true , x) (false , _) q = + cong (η x ·fg_) (cong (inv ∘ η) (sym (cong snd q))) ∙ ·InvR (η x) + redex-ε-η* (true , _) (true , _) = ⊥.rec ∘ true≢false ∘ cong fst diff --git a/Cubical/Data/List/Base.agda b/Cubical/Data/List/Base.agda index 0222265954..a78ac00455 100644 --- a/Cubical/Data/List/Base.agda +++ b/Cubical/Data/List/Base.agda @@ -3,8 +3,8 @@ module Cubical.Data.List.Base where open import Agda.Builtin.List public open import Cubical.Core.Everything -open import Cubical.Data.Maybe.Base as Maybe -open import Cubical.Data.Nat.Base +open import Cubical.Data.Maybe.Base as Maybe hiding (rec ; elim) +open import Cubical.Data.Nat.Base hiding (elim) module _ {ℓ} {A : Type ℓ} where @@ -50,3 +50,27 @@ module _ {ℓ} {A : Type ℓ} where foldl : ∀ {ℓ'} {B : Type ℓ'} → (B → A → B) → B → List A → B foldl f b [] = b foldl f b (x ∷ xs) = foldl f (f b x) xs + + drop : ℕ → List A → List A + drop zero xs = xs + drop (suc n) [] = [] + drop (suc n) (x ∷ xs) = drop n xs + + take : ℕ → List A → List A + take zero xs = [] + take (suc n) [] = [] + take (suc n) (x ∷ xs) = x ∷ take n xs + + elim : ∀ {ℓ'} {B : List A → Type ℓ'} + → B [] + → (∀ {a l} → B l → B (a ∷ l)) + → ∀ l → B l + elim b _ [] = b + elim {B = B} b[] b (a ∷ l) = b (elim {B = B} b[] b l ) + + rec : ∀ {ℓ'} {B : Type ℓ'} + → B + → (A → B → B) + → List A → B + rec b _ [] = b + rec b f (x ∷ xs) = f x (rec b f xs) diff --git a/Cubical/Data/List/Properties.agda b/Cubical/Data/List/Properties.agda index c44f9db1df..7b755944f5 100644 --- a/Cubical/Data/List/Properties.agda +++ b/Cubical/Data/List/Properties.agda @@ -6,13 +6,16 @@ open import Cubical.Core.Everything open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.HLevels open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism open import Cubical.Data.Empty as ⊥ open import Cubical.Data.Nat open import Cubical.Data.Sigma +open import Cubical.Data.Sum as ⊎ hiding (map) open import Cubical.Data.Unit open import Cubical.Relation.Nullary -open import Cubical.Data.List.Base +open import Cubical.Data.List.Base as List module _ {ℓ} {A : Type ℓ} where @@ -117,8 +120,11 @@ isOfHLevelList n ofLevel xs ys = private variable - ℓ : Level + ℓ ℓ' : Level A : Type ℓ + B : Type ℓ' + x y : A + xs ys : List A caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B caseList n _ [] = n @@ -132,23 +138,32 @@ private safe-tail [] = [] safe-tail (_ ∷ xs) = xs -cons-inj₁ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y +cons-inj₁ : 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₂ : 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 []) +snoc-inj₂ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y +snoc-inj₂ {xs = xs} {ys = ys} p = + cons-inj₁ ((sym (rev-++ xs _)) ∙∙ cong rev p ∙∙ (rev-++ ys _)) -¬nil≡cons : ∀ {x : A} {xs} → ¬ ([] ≡ x ∷ xs) -¬nil≡cons {A = A} p = lower (subst (caseList (List A) (Lift ⊥)) p []) +snoc-inj₁ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys +snoc-inj₁ {xs = xs} {ys = ys} p = + sym (rev-rev _) ∙∙ cong rev (cons-inj₂ ((sym (rev-++ xs _)) ∙∙ cong rev p ∙∙ (rev-++ ys _))) + ∙∙ rev-rev _ -¬snoc≡nil : ∀ {x : A} {xs} → ¬ (xs ∷ʳ x ≡ []) +¬cons≡nil : ¬ (x ∷ xs ≡ []) +¬cons≡nil {_} {A} p = lower (subst (caseList (Lift ⊥) (List A)) p []) + +¬nil≡cons : ¬ ([] ≡ x ∷ xs) +¬nil≡cons {_} {A} p = lower (subst (caseList (List A) (Lift ⊥)) p []) + +¬snoc≡nil : ¬ (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 : ¬ ([] ≡ xs ∷ʳ x) ¬nil≡snoc contra = ¬snoc≡nil (sym contra) cons≡rev-snoc : (x : A) → (xs : List A) → x ∷ rev xs ≡ rev (xs ∷ʳ x) @@ -158,7 +173,7 @@ cons≡rev-snoc x (y ∷ ys) = λ i → cons≡rev-snoc x ys i ++ y ∷ [] isContr[]≡[] : isContr (Path (List A) [] []) isContr[]≡[] = refl , ListPath.decodeEncode [] [] -isPropXs≡[] : {xs : List A} → isProp (xs ≡ []) +isPropXs≡[] : isProp (xs ≡ []) isPropXs≡[] {xs = []} = isOfHLevelSuc 0 isContr[]≡[] isPropXs≡[] {xs = x ∷ xs} = λ p _ → ⊥.rec (¬cons≡nil p) @@ -175,7 +190,161 @@ foldrCons : (xs : List A) → foldr _∷_ [] xs ≡ xs foldrCons [] = refl foldrCons (x ∷ xs) = cong (x ∷_) (foldrCons xs) -length-map : ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} → (f : A → B) → (as : List A) +length-map : (f : A → B) → (as : List A) → length (map f as) ≡ length as length-map f [] = refl length-map f (a ∷ as) = cong suc (length-map f as) + +map++ : (f : A → B) → (as bs : List A) + → map f as ++ map f bs ≡ map f (as ++ bs) +map++ f [] bs = refl +map++ f (x ∷ as) bs = cong (f x ∷_) (map++ f as bs) + +rev-map-comm : (f : A → B) → (as : List A) + → map f (rev as) ≡ rev (map f as) +rev-map-comm f [] = refl +rev-map-comm f (x ∷ as) = + sym (map++ f (rev as) _) ∙ cong (_++ [ f x ]) (rev-map-comm f as) + +length++ : (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys +length++ [] ys = refl +length++ (x ∷ xs) ys = cong suc (length++ xs ys) + +drop++ : ∀ (xs ys : List A) k → + drop (length xs + k) (xs ++ ys) ≡ drop k ys +drop++ [] ys k = refl +drop++ (x ∷ xs) ys k = drop++ xs ys k + +dropLength++ : (xs : List A) → drop (length xs) (xs ++ ys) ≡ ys +dropLength++ {ys = ys} xs = + cong (flip drop (xs ++ ys)) (sym (+-zero (length xs))) ∙ drop++ xs ys 0 + + +dropLength : (xs : List A) → drop (length xs) xs ≡ [] +dropLength xs = + cong (drop (length xs)) (sym (++-unit-r xs)) + ∙ dropLength++ xs + + +take++ : ∀ (xs ys : List A) k → take (length xs + k) (xs ++ ys) ≡ xs ++ take k ys +take++ [] ys k = refl +take++ (x ∷ xs) ys k = cong (_ ∷_) (take++ _ _ k) + + +takeLength++ : ∀ ys → take (length xs) (xs ++ ys) ≡ xs +takeLength++ {xs = xs} ys = + cong (flip take (xs ++ ys)) (sym (+-zero (length xs))) + ∙∙ take++ xs ys 0 + ∙∙ ++-unit-r xs + +takeLength : take (length xs) xs ≡ xs +takeLength = cong (take _) (sym (++-unit-r _)) ∙ takeLength++ [] + +map-∘ : ∀ {ℓA ℓB ℓC} {A : Type ℓA} {B : Type ℓB} {C : Type ℓC} + (g : B → C) (f : A → B) (as : List A) + → map g (map f as) ≡ map (λ x → g (f x)) as +map-∘ g f [] = refl +map-∘ g f (x ∷ as) = cong (_ ∷_) (map-∘ g f as) + +map-id : (as : List A) → map (λ x → x) as ≡ as +map-id [] = refl +map-id (x ∷ as) = cong (_ ∷_) (map-id as) + +length≡0→≡[] : ∀ (xs : List A) → length xs ≡ 0 → xs ≡ [] +length≡0→≡[] [] x = refl +length≡0→≡[] (x₁ ∷ xs) x = ⊥.rec (snotz x) + +init : List A → List A +init [] = [] +init (x ∷ []) = [] +init (x ∷ xs@(_ ∷ _)) = x ∷ init xs + +tail : List A → List A +tail [] = [] +tail (x ∷ xs) = xs + +init-red-lem : ∀ (x : A) xs → ¬ (xs ≡ []) → (x ∷ init xs) ≡ (init (x ∷ xs)) +init-red-lem x [] x₁ = ⊥.rec (x₁ refl) +init-red-lem x (x₂ ∷ xs) x₁ = refl + +init∷ʳ : init (xs ∷ʳ x) ≡ xs +init∷ʳ {xs = []} = refl +init∷ʳ {xs = _ ∷ []} = refl +init∷ʳ {xs = _ ∷ _ ∷ _} = cong (_ ∷_) init∷ʳ + +tail∷ʳ : tail (xs ∷ʳ y) ∷ʳ x ≡ tail (xs ∷ʳ y ∷ʳ x) +tail∷ʳ {xs = []} = refl +tail∷ʳ {xs = x ∷ xs} = refl + +init-rev-tail : rev (init xs) ≡ tail (rev xs) +init-rev-tail {xs = []} = refl +init-rev-tail {xs = x ∷ []} = refl +init-rev-tail {xs = x ∷ y ∷ xs} = + cong (_∷ʳ x) (init-rev-tail {xs = y ∷ xs}) + ∙ tail∷ʳ {xs = rev xs} + +init++ : ∀ xs → xs ++ init (x ∷ ys) ≡ init (xs ++ x ∷ ys) +init++ [] = refl +init++ (_ ∷ []) = refl +init++ (_ ∷ _ ∷ _) = cong (_ ∷_) (init++ (_ ∷ _)) + +Split++ : (xs ys xs' ys' zs : List A) → Type _ +Split++ xs ys xs' ys' zs = ((xs ++ zs ≡ xs') × (ys ≡ zs ++ ys')) + +split++ : ∀ (xs' ys' xs ys : List A) → xs' ++ ys' ≡ xs ++ ys → + Σ _ λ zs → + ((Split++ xs' ys' xs ys zs) + ⊎ (Split++ xs ys xs' ys' zs)) +split++ [] ys' xs ys x = xs , inl (refl , x) +split++ xs'@(_ ∷ _) ys' [] ys x = xs' , inr (refl , sym x) +split++ (x₁ ∷ xs') ys' (x₂ ∷ xs) ys x = + let (zs , q) = split++ xs' ys' xs ys (cons-inj₂ x) + p = cons-inj₁ x + in zs , ⊎.map (map-fst (λ q i → p i ∷ q i)) + (map-fst (λ q i → p (~ i) ∷ q i)) q + +rot : List A → List A +rot [] = [] +rot (x ∷ xs) = xs ∷ʳ x + +take[] : ∀ n → take {A = A} n [] ≡ [] +take[] zero = refl +take[] (suc n) = refl + +drop[] : ∀ n → drop {A = A} n [] ≡ [] +drop[] zero = refl +drop[] (suc n) = refl + +lookupAlways : A → List A → ℕ → A +lookupAlways a [] _ = a +lookupAlways _ (x ∷ _) zero = x +lookupAlways a (x ∷ xs) (suc k) = lookupAlways a xs k + +module List₂ where + open import Cubical.HITs.SetTruncation renaming + (rec to rec₂ ; map to map₂ ; elim to elim₂ ) + + ∥List∥₂→List∥∥₂ : ∥ List A ∥₂ → List ∥ A ∥₂ + ∥List∥₂→List∥∥₂ = rec₂ (isOfHLevelList 0 squash₂) (map ∣_∣₂) + + List∥∥₂→∥List∥₂ : List ∥ A ∥₂ → ∥ List A ∥₂ + List∥∥₂→∥List∥₂ [] = ∣ [] ∣₂ + List∥∥₂→∥List∥₂ (x ∷ xs) = + rec2 squash₂ (λ x xs → ∣ x ∷ xs ∣₂) x (List∥∥₂→∥List∥₂ xs) + + Iso∥List∥₂List∥∥₂ : Iso (List ∥ A ∥₂) ∥ List A ∥₂ + Iso.fun Iso∥List∥₂List∥∥₂ = List∥∥₂→∥List∥₂ + Iso.inv Iso∥List∥₂List∥∥₂ = ∥List∥₂→List∥∥₂ + Iso.rightInv Iso∥List∥₂List∥∥₂ = + elim₂ (isProp→isSet ∘ λ _ → squash₂ _ _) + (List.elim refl (cong (rec2 squash₂ (λ x₁ xs → ∣ x₁ ∷ xs ∣₂) ∣ _ ∣₂))) + Iso.leftInv Iso∥List∥₂List∥∥₂ = List.elim refl ((lem _ _ ∙_) ∘S cong (_ ∷_)) + where + lem = elim2 {C = λ a l' → ∥List∥₂→List∥∥₂ + (rec2 squash₂ (λ x₁ xs → ∣ x₁ ∷ xs ∣₂) a l') + ≡ a ∷ ∥List∥₂→List∥∥₂ l'} + (λ _ _ → isProp→isSet (isOfHLevelList 0 squash₂ _ _)) + λ _ _ → refl + + List-comm-∥∥₂ : ∀ {ℓ} → List {ℓ} ∘ ∥_∥₂ ≡ ∥_∥₂ ∘ List + List-comm-∥∥₂ = funExt λ A → isoToPath (Iso∥List∥₂List∥∥₂ {A = A}) diff --git a/Cubical/Data/Nat/Properties.agda b/Cubical/Data/Nat/Properties.agda index e3b3c64889..a0097e49d9 100644 --- a/Cubical/Data/Nat/Properties.agda +++ b/Cubical/Data/Nat/Properties.agda @@ -173,6 +173,12 @@ m+n≡0→m≡0×n≡0 : m + n ≡ 0 → (m ≡ 0) × (n ≡ 0) m+n≡0→m≡0×n≡0 {zero} = refl ,_ m+n≡0→m≡0×n≡0 {suc m} p = ⊥.rec (snotz p) +m+n≡1→m≡0×n≡1⊎m≡1n≡0 : m + n ≡ 1 → ((m ≡ 0) × (n ≡ 1)) ⊎ ((m ≡ 1) × (n ≡ 0)) +m+n≡1→m≡0×n≡1⊎m≡1n≡0 {zero} x = inl (refl , x) +m+n≡1→m≡0×n≡1⊎m≡1n≡0 {suc m} {n} x = + let (m≡0 , n≡0) = m+n≡0→m≡0×n≡0 (injSuc x) + in inr (cong suc m≡0 , n≡0 ) + -- Arithmetic facts about · 0≡m·0 : ∀ m → 0 ≡ m · 0 diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda index 7a1a0f53cd..a3db8125dc 100644 --- a/Cubical/Data/Sigma/Properties.agda +++ b/Cubical/Data/Sigma/Properties.agda @@ -378,6 +378,10 @@ snd (ΣPathPProp {B = B} {u = u} {v = v} pB p i) = lem i lem : PathP (λ i → B i (p i)) (snd u) (snd v) lem = toPathP (pB _ _ _) +discreteΣProp : Discrete A → ((x : A) → isProp (B x)) → Discrete (Σ A B) +discreteΣProp _≟_ isPropA _ _ = + EquivPresDec (Σ≡PropEquiv isPropA) (_ ≟ _) + ≃-× : ∀ {ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''} → A ≃ C → B ≃ D → A × B ≃ C × D ≃-× eq1 eq2 = map-× (fst eq1) (fst eq2) diff --git a/Cubical/Foundations/Function.agda b/Cubical/Foundations/Function.agda index bc37863fd4..d68fbad72a 100644 --- a/Cubical/Foundations/Function.agda +++ b/Cubical/Foundations/Function.agda @@ -9,7 +9,7 @@ open import Cubical.Foundations.Prelude private variable ℓ ℓ' ℓ'' : Level - A : Type ℓ + A A' A'' : Type ℓ B : A → Type ℓ C : (a : A) → B a → Type ℓ D : (a : A) (b : B a) → C a b → Type ℓ @@ -26,12 +26,16 @@ _$_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → ((a : A) → B a) f $ a = f a {-# INLINE _$_ #-} -infixr 9 _∘_ +infixr 9 _∘_ _∘S_ _∘_ : (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → C a (f a) g ∘ f = λ x → g (f x) {-# INLINE _∘_ #-} +_∘S_ : (A' → A'') → (A → A') → A → A'' +g ∘S f = λ x → g (f x) +{-# INLINE _∘S_ #-} + ∘-assoc : (h : {a : A} {b : B a} → (c : C a b) → D a b c) (g : {a : A} → (b : B a) → C a b) (f : (a : A) → B a) diff --git a/Cubical/Foundations/Univalence.agda b/Cubical/Foundations/Univalence.agda index 53c858608c..d6c688e421 100644 --- a/Cubical/Foundations/Univalence.agda +++ b/Cubical/Foundations/Univalence.agda @@ -69,6 +69,13 @@ module _ {A B : Type ℓ} (e : A ≃ B) {x : A} {y : B} where unquoteDef ua-ungluePath-Equiv = defStrictEquiv ua-ungluePath-Equiv ua-ungluePath ua-gluePath +ua-ungluePathExt : {A B : Type ℓ} (e : A ≃ B) → PathP (λ i → ua e i → B) (fst e) (idfun B) +ua-ungluePathExt e i = ua-unglue e i + +ua-gluePathExt : {A B : Type ℓ} (e : A ≃ B) → PathP (λ i → A → ua e i) (idfun _) (fst e) +ua-gluePathExt e i x = + ua-glue e i (λ { (i = i0) → x }) (inS (fst e x)) + -- ua-unglue and ua-glue are also definitional inverses, in a way -- strengthening the types of ua-unglue and ua-glue gives a nicer formulation of this, see below @@ -137,6 +144,14 @@ unglueEquiv : ∀ (A : Type ℓ) (φ : I) (Glue A f) ≃ A unglueEquiv A φ f = ( unglue φ , unglueIsEquiv A φ f ) +ua-unglueEquiv : ∀ {A B : Type ℓ} (e : A ≃ B) → + PathP (λ i → ua e i ≃ B) + e + (idEquiv _) +fst (ua-unglueEquiv e i) = ua-unglue e i +snd (ua-unglueEquiv e i) = + isProp→PathP (λ i → isPropIsEquiv (ua-unglue e i)) + (snd e) (idIsEquiv _) i -- The following is a formulation of univalence proposed by Martín Escardó: -- https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ @@ -194,6 +209,9 @@ pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x) uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x uaβ e x = transportRefl (equivFun e x) +~uaβ : {A B : Type ℓ} (e : A ≃ B) (x : B) → transport (sym (ua e)) x ≡ invEq e x +~uaβ e x = cong (invEq e) (transportRefl x) + uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P uaη {A = A} {B = B} P i j = Glue B {φ = φ} sides where -- Adapted from a proof by @dolio, cf. commit e42a6fa1 diff --git a/Cubical/HITs/Bouquet/Discrete.agda b/Cubical/HITs/Bouquet/Discrete.agda new file mode 100644 index 0000000000..5b9c69473e --- /dev/null +++ b/Cubical/HITs/Bouquet/Discrete.agda @@ -0,0 +1,129 @@ +{-# OPTIONS --safe #-} + +{- + +This module, uses normalization and decidable equality from `Cubical.Algebra.Group.Free` to demonstrate that Bouquet over discrete type is hGroupoid by establishing a coding between loops in the bouquet and elements of the FreeGroup represented by normalised words. + +-} + +module Cubical.HITs.Bouquet.Discrete where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Transport +open import Cubical.Foundations.HLevels + +open import Cubical.Data.Bool +open import Cubical.Data.Empty as ⊥ +open import Cubical.Data.Sigma +open import Cubical.Data.List renaming (rec to recList) +open import Cubical.Data.Sum + +open import Cubical.Relation.Nullary + + +open import Cubical.HITs.Bouquet.Base +open import Cubical.Algebra.Group.Free + + +private + variable + ℓ : Level + +module _ {A : Type ℓ} (_≟_ : Discrete A) where + + open NormalForm A + + open Discrete _≟_ + + + CodeBouquet : Bouquet A → Type ℓ + CodeBouquet base = Σ _ IsNormalised + CodeBouquet (loop a i) = ua (η·≃ (true , a)) i + + co→ : ∀ x → base ≡ x → CodeBouquet x + co→ x p = subst CodeBouquet p ([] , lower) + + co←base-step : Bool × A → Path (Bouquet A) base base + + co←base-step (b , a) = if b then (idfun _) else sym $ loop a + + co←base : [𝟚× A ] → Path (Bouquet A) base base + co←base = recList refl (flip _∙_ ∘ co←base-step) + + co← : ∀ x → CodeBouquet x → base ≡ x + co← base = co←base ∘ fst + co← (loop a i) x j = co←Sq a i j x + where + + co←Sq : (a : A) → SquareP (λ i j → ua (η·≃ (true , a)) i → Bouquet A) + (funExt (co←base ∘ fst)) + (funExt (co←base ∘ fst)) + (λ _ _ → base) + (λ i _ → loop a i) + co←Sq a = congP (λ _ → funExt) (ua→ (uncurry + (λ xs y → co←Sq' a xs y (HeadIsRedex? ((true , a) ∷ xs))))) + where + co←Sq' : (a : A) → (x : [𝟚× A ]) (y : IsNormalised x) → + ∀ u → PathP (λ i → base ≡ loop a i) + (recList (λ _ → base) (flip _∙_ ∘ co←base-step) x) + (recList (λ _ → base) (flip _∙_ ∘ co←base-step) (preη· (true , a) x u )) + co←Sq' a ((false , snd₁) ∷ xs) y (yes p) = + cong (λ x' → co←base ((false , x') ∷ xs)) (cong snd (sym p)) + ◁ symP (compPath-filler (co←base xs) (sym (loop a))) + co←Sq' a xs y (no ¬p) = compPath-filler _ _ + co←Sq' a ((true , snd₁) ∷ xs) y (yes p) = ⊥.rec (true≢false (cong fst p)) + + coSec : ∀ x → section (co← x) (co→ x) + coSec _ = J (λ x b → co← x (co→ x b) ≡ b) refl + + coRet : (x : [𝟚× A ]) (y : IsNormalised x) → + fst (subst CodeBouquet (co← base (x , y)) ([] , lower)) + ≡ x + coRet [] y = refl + coRet (x@(b , a) ∷ xs) y = + cong fst (substComposite CodeBouquet (co← base (xs , y ∘ inr)) + (co←base-step x) _) + ∙∙ + cong (fst ∘ subst CodeBouquet (co←base-step x)) + (Σ≡Prop isPropIsNormalised (coRet xs (y ∘ inr))) ∙∙ + lem b xs (y ∘ inr) ∙ η·∷ x xs (y ∘ inl) + + where + lem : ∀ b xs y → fst + (subst CodeBouquet (co←base-step (b , a)) (xs , y)) + ≡ η· (b , a) xs + lem false xs y = cong fst (~uaβ (η·≃ (true , a)) (xs , y )) + lem true xs y = cong fst (uaβ (η·≃ (true , a)) (xs , y )) + + + codeDecode : Iso (Path (Bouquet A) base base) + (Σ _ IsNormalised) + Iso.fun codeDecode p = subst CodeBouquet p ([] , lower) + Iso.inv codeDecode = co← base + Iso.rightInv codeDecode = Σ≡Prop isPropIsNormalised ∘ uncurry coRet + Iso.leftInv codeDecode = coSec base + + isSetΩBouquet : isSet (Path (Bouquet A) base base) + isSetΩBouquet = isOfHLevelRetractFromIso 2 codeDecode + (isSetΣ isSet[𝟚×] (isProp→isSet ∘ isPropIsNormalised)) + + isGroupoidBouquet : isGroupoid (Bouquet A) + isGroupoidBouquet base base = isSetΩBouquet + isGroupoidBouquet base (loop x i) = isProp→PathP + (λ i → isPropIsSet {A = Path (Bouquet A) base (loop x i)}) isSetΩBouquet isSetΩBouquet i + isGroupoidBouquet (loop x i) base = isProp→PathP + (λ i → isPropIsSet {A = Path (Bouquet A) (loop x i) base}) isSetΩBouquet isSetΩBouquet i + isGroupoidBouquet (loop x i) (loop x₁ i₁) = isSet→SquareP + (λ i i₁ → isProp→isSet (isPropIsSet {A = Path (Bouquet A) (loop x i) (loop x₁ i₁)})) + (isProp→PathP + (λ i → isPropIsSet {A = Path (Bouquet A) base (loop x₁ i)}) isSetΩBouquet isSetΩBouquet) + (isProp→PathP + (λ i → isPropIsSet {A = Path (Bouquet A) base (loop x₁ i)}) isSetΩBouquet isSetΩBouquet) + (isProp→PathP + (λ i → isPropIsSet {A = Path (Bouquet A) (loop x i) base}) isSetΩBouquet isSetΩBouquet) + (isProp→PathP + (λ i → isPropIsSet {A = Path (Bouquet A) (loop x i) base}) isSetΩBouquet isSetΩBouquet) + i i₁ diff --git a/Cubical/HITs/FreeGroup/NormalForm.agda b/Cubical/HITs/FreeGroup/NormalForm.agda new file mode 100644 index 0000000000..a4b3a87e12 --- /dev/null +++ b/Cubical/HITs/FreeGroup/NormalForm.agda @@ -0,0 +1,187 @@ +{-# OPTIONS --safe #-} + +{- + +For an arbitrary type of generators: + - `GroupIso-FG-L/↘↙` demonstrates that the free group defined as a HIT is equivalent to the definition based on quotienting lists by the appropriate relation (from `Cubical.Algebra.Group.Free`). + +The following properties are defined with the assumption that the type of the generators is an hSet. Without this assumption, they can be adapted to be stated "modulo set truncation": + + - `isPropNF` ensures the uniqueness of the normal form. + - `ηInj` establishes that the `η` constructor of FreeGroup is injective. + - `NF⇔DiscreteA` indicates that computing the normal form is feasible if and only if the type of generators is discrete. + - `discreteFreeGroup` asserts that if the generators are discrete, then the FreeGroup has decidable equality. + +-} +module Cubical.HITs.FreeGroup.NormalForm where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv + +open import Cubical.Relation.Nullary +open import Cubical.Relation.Nullary.HLevels + +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.Properties +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Free + +open import Cubical.Data.List renaming (elim to elimList) +open import Cubical.Data.Bool as 𝟚 +open import Cubical.Data.Sigma +open import Cubical.Data.Sum as ⊎ + +open import Cubical.HITs.SetQuotients renaming + (elimProp to elimProp/ ; _/_ to _/₂_ ; [_] to [_]/ ; rec to rec/) +open import Cubical.HITs.PropositionalTruncation renaming + (rec to rec₁ ; map to map₁) + + +open import Cubical.HITs.FreeGroup.Base +open import Cubical.HITs.FreeGroup.Properties renaming (rec to recFreeGroup) + +private + variable + ℓ : Level + +module _ {A : Type ℓ} where + + open NormalForm A + + open NF (freeGroupGroup A) η renaming (inv to invFG) + + FG→L/↘↙ : GroupHom (freeGroupGroup A) (_ , List/↘↙GroupStr) + FG→L/↘↙ = recFreeGroup ([_]/ ∘ [_] ∘ (true ,_)) + + module gh/ = IsGroupHom (snd (FG→L/↘↙)) + open GroupTheory (freeGroupGroup A) + + open IsGroupHom + + ⇊1g→FG≡ : ∀ a → a ⇊1g → fromList a ≡ ε + ⇊1g→FG≡ .[] [] = refl + ⇊1g→FG≡ .(x ∷ (xs ∷ʳ not₁ x)) (cj x xs x₁) = + cong (η* x ·fg_) (fromList· xs [ not₁ x ] ∙ + cong₂ _·fg_ (⇊1g→FG≡ xs x₁) (·IdR _) ∙ ·IdL _) ∙ + redex-ε-η* x (not₁ x) (symIsRedex _ _ refl) + ⇊1g→FG≡ .(xs ++ ys) ((xs · ys) x x₁) = fromList· xs ys + ∙∙ cong₂ _·fg_ (⇊1g→FG≡ _ x) (⇊1g→FG≡ _ x₁) ∙∙ ·IdL _ + + fromListInv : (xs : List (Bool × A)) → + fromList (invLi xs) ≡ invFG (fromList xs) + fromListInv [] = sym (GroupTheory.inv1g (freeGroupGroup A)) + fromListInv (x ∷ xs) = (fromList· (invLi xs) _ ∙ + cong (fromList (invLi xs) ·fg_) (w' x)) + ∙∙ cong (_·fg invFG (η* x)) (fromListInv xs) ∙∙ sym (invDistr _ _) + where + w' : ∀ x → fromList [ not₁ x ] ≡ invFG (η* x) + w' = λ { (false , a) → ·IdR _ ∙ sym (invInv _) ; (true , a) → ·IdR _ } + + fromL/ : List/↘↙ → _ + fromL/ = rec/ trunc fromList + λ a b → + _∙ (sym (fromListInv (invLi b)) + ∙ cong fromList (invol-invLi b)) ∘S invUniqueL + ∘S sym (fromList· a (invLi b)) ∙_ ∘S ⇊1g→FG≡ _ ∘S ≡ε + + section-FG-L/↘↙ : ∀ a → fst (FG→L/↘↙) (fromList a) ≡ [ a ]/ + section-FG-L/↘↙ [] = refl + section-FG-L/↘↙ (x ∷ xs) = gh/.pres· (η* x) (fromList xs) ∙ + cong (List/↘↙· (fst FG→L/↘↙ (η* x))) + (section-FG-L/↘↙ xs) ∙ w x where + w : ∀ x → List/↘↙· (fst FG→L/↘↙ (η* x)) [ xs ]/ ≡ [ x ∷ xs ]/ + w = λ { (false , a) → refl ; (true , a) → refl } + + isGroupHomFromL/ : IsGroupHom List/↘↙GroupStr fromL/ (snd (freeGroupGroup A)) + pres· isGroupHomFromL/ = elimProp2 (λ _ _ → trunc _ _) fromList· + pres1 isGroupHomFromL/ = refl + presinv isGroupHomFromL/ = elimProp/ (λ _ → trunc _ _) fromListInv + + GroupIso-FG-L/↘↙ : GroupIso (freeGroupGroup A) (List/↘↙group) + Iso.fun (fst GroupIso-FG-L/↘↙) = fst FG→L/↘↙ + Iso.inv (fst GroupIso-FG-L/↘↙) = fromL/ + Iso.rightInv (fst GroupIso-FG-L/↘↙) = + elimProp/ (λ _ → squash/ _ _) section-FG-L/↘↙ + Iso.leftInv (fst GroupIso-FG-L/↘↙) = + funExt⁻ (congS fst (freeGroupHom≡ + {f = compGroupHom FG→L/↘↙ (fromL/ , isGroupHomFromL/)} + {g = idGroupHom} (sym ∘ idr ∘ η ))) + snd GroupIso-FG-L/↘↙ = snd FG→L/↘↙ + + module _ (isSetA : isSet A) where + + private + isSet[𝟚×A] = isOfHLevelList 0 (isSet× isSetBool isSetA) + + isPropNF : ∀ g → isProp (NF g) + isPropNF = λ g → + λ (xs nf u , v) (xs' nf u' , v') → + let zz = rec₁ (isSet[𝟚×A] xs xs') + ( sym + ∘S nf-uR _ _ (fst IsNormalisedInvLi v') v + ∘S ⇊1g++comm xs (invLi xs') + ∘S ≡ε ) + (Iso.fun (≡→red xs xs') ( + isoInvInjective (fst (GroupIso-FG-L/↘↙)) + _ _ (u ∙ (sym u')))) + in λ i → zz i + nf isProp→PathP (λ i → trunc (fromList (zz i)) g) u u' i + , isProp→PathP (λ i → (isPropIsNormalised (zz i))) v v' i + + ηInj : ∀ a a' → Path (FreeGroup A) (η a) (η a') → a ≡ a' + ηInj a a' = + rec₁ (isSetA _ _) + ((λ { (inl p) i → snd (p i) + ; (inr (inl ())) ; (inr (inr ()))}) + ∘S ⇊1g⇒HasRedex _ _ ∘S ≡ε ) + ∘S Iso.fun (≡→red _ _) + ∘S isoInvInjective (fst (GroupIso-FG-L/↘↙)) + [ [ true , _ ] ]/ [ [ true , _ ] ]/ + ∘S ·IdR _ ∙∙_∙∙ sym (·IdR _) + + NF-η : ∀ a → (nfa : NF (η a)) → [ true , a ] ≡ NF.word nfa + NF-η a nfa = rec₁ (isSet[𝟚×A] _ _) (λ u → + nf-uR _ _ (IsNormalised[x] (true , a)) + (NF.isNormalisedWord nfa) (⇊1g++comm _ [ false , a ] (≡ε u))) + (Iso.fun (≡→red _ _) (isoInvInjective (fst (GroupIso-FG-L/↘↙)) + [ NF.word nfa ]/ [ [ (true , a) ] ]/ + (NF.fromListWord≡ nfa ∙ (sym (·IdR _))))) + + ΠNF⇒DiscreteA : (∀ g → NF g) → Discrete A + ΠNF⇒DiscreteA nF a a' = + let nff = nF (η a · invFG (η a')) + in rec₁ (isPropDec (isSetA _ _)) + (λ r → ⊎.rec + (yes ∘ sym ∘ cong snd) + (no ∘ ⊎.rec (λ p pp → lower (subst (WillReduce false a) + (isNormalised⇊1g _ (NF.isNormalisedWord nff) + (pop⇊1gHead (cong (true ,_) (sym pp)) r)) p)) + (const ∘ NF.isNormalisedWord nff)) + (⇊1g⇒HasRedex _ _ r)) + (map₁ (⇊1g++comm (NF.word nff) _ ∘ ≡ε) + (Iso.fun (≡→red _ _) (isoInvInjective (fst (GroupIso-FG-L/↘↙)) + [ NF.word nff ]/ [ (true , a) ∷ [ false , a' ] ]/ + (NF.fromListWord≡ nff ∙ cong (η a ·_) (sym (·IdR _)))))) + + NF⇔DiscreteA : (∀ g → NF g) ≃ Discrete A + NF⇔DiscreteA = propBiimpl→Equiv (isPropΠ isPropNF) isPropDiscrete + ΠNF⇒DiscreteA λ _≟_ g → + let e = compIso (fst (GroupIso-FG-L/↘↙)) (invIso (Discrete.IsoNF _≟_)) + (g' , n) = Iso.fun e g + in g' nf Iso.leftInv e g , n + + ≟→normalForm : Discrete A → (∀ g → NF g) + ≟→normalForm _≟_ = invEq (NF⇔DiscreteA (Discrete→isSet _≟_)) _≟_ + + discreteFreeGroup : Discrete A → Discrete (FreeGroup A) + discreteFreeGroup _≟_ = + isoPresDiscrete + (compIso + (Discrete.IsoNF _≟_) + (invIso (fst (GroupIso-FG-L/↘↙)))) + (discreteΣProp + (discreteList (discreteΣ 𝟚._≟_ λ _ → _≟_)) + isPropIsNormalised) diff --git a/Cubical/Homotopy/Group/Base.agda b/Cubical/Homotopy/Group/Base.agda index 5c856ba476..ec0c1f8f4a 100644 --- a/Cubical/Homotopy/Group/Base.agda +++ b/Cubical/Homotopy/Group/Base.agda @@ -14,6 +14,7 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.Univalence open import Cubical.Foundations.Function open import Cubical.Foundations.Transport +open import Cubical.Foundations.Structure open import Cubical.Functions.Morphism @@ -1081,3 +1082,15 @@ snd (fst (πIso e n)) = (setTruncIso (equivToIso (_ , isEquivΩ^→ (suc n) (≃∙map e) (snd (fst e))))) snd (πIso e n) = snd (πHom n (≃∙map e)) + +hGroupoidπ₁ : ∀ {ℓ} (A : hGroupoid ℓ) → ⟨ A ⟩ → Group ℓ +fst (hGroupoidπ₁ A a) = a ≡ a +1g (snd (hGroupoidπ₁ A a)) = refl +GroupStr._·_ (snd (hGroupoidπ₁ A a)) = _∙_ +inv (snd (hGroupoidπ₁ A a)) = sym +is-set (isSemigroup (isMonoid (isGroup (snd (hGroupoidπ₁ A a))))) = snd A a a +·Assoc (isSemigroup (isMonoid (isGroup (snd (hGroupoidπ₁ A a))))) = ∙assoc +·IdR (isMonoid (isGroup (snd (hGroupoidπ₁ A a)))) = sym ∘ rUnit +·IdL (isMonoid (isGroup (snd (hGroupoidπ₁ A a)))) = sym ∘ lUnit +·InvR (isGroup (snd (hGroupoidπ₁ A a))) = rCancel +·InvL (isGroup (snd (hGroupoidπ₁ A a))) = lCancel diff --git a/Cubical/Relation/Nullary/Properties.agda b/Cubical/Relation/Nullary/Properties.agda index a3e99d3c78..77535b9c88 100644 --- a/Cubical/Relation/Nullary/Properties.agda +++ b/Cubical/Relation/Nullary/Properties.agda @@ -201,3 +201,7 @@ Discrete→Separated d x y = Dec→Stable (d x y) Discrete→isSet : Discrete A → isSet A Discrete→isSet = Separated→isSet ∘ Discrete→Separated + +≡no : ∀ {A : Type ℓ} x y → Path (Dec A) x (no y) +≡no (yes p) y = ⊥.rec (y p) +≡no (no ¬p) y i = no (isProp¬ _ ¬p y i)