Finite supports and redefined Bool.

core/lib/Base.agda

@@ -355,6 +355,7 @@ data Coprod {i j} (A : Type i) (B : Type j) : Type (lmax i j) where
   inl : A → Coprod A B
   inr : B → Coprod A B
 
+infixr 80 _⊔_
 _⊔_ = Coprod
 
 match_withl_withr_ : ∀ {i j k} {A : Type i} {B : Type j}
@@ -363,6 +364,9 @@ match_withl_withr_ : ∀ {i j k} {A : Type i} {B : Type j}
 match (inl a) withl l withr r = l a
 match (inr b) withl l withr r = r b
 
+Dec : ∀ {i} (P : Type i) → Type i
+Dec P = P ⊔ ¬ P
+
 {-
 Used in a hack to make HITs maybe consistent. This is just a parametrized unit
 type (positively)

core/lib/NType.agda

@@ -48,7 +48,7 @@ abstract
 {- Having decidable equality is stronger that being a set -}
 
 has-dec-eq : Type i → Type i
-has-dec-eq A = Dec (_==_ :> Rel A i)
+has-dec-eq A = Decidable (_==_ :> Rel A i)
 
 abstract
   dec-eq-is-set : {A : Type i} → (has-dec-eq A → is-set A)

core/lib/Relation.agda

@@ -7,6 +7,5 @@ module lib.Relation where
 Rel : ∀ {i} (A : Type i) j → Type (lmax i (lsucc j))
 Rel A j = A → A → Type j
 
-Dec : ∀ {i} {A : Type i} {j} → Rel A j → Type (lmax i j)
-Dec rel = ∀ a₁ a₂ → Coprod (rel a₁ a₂) (¬ (rel a₁ a₂))
-
+Decidable : ∀ {i} {A : Type i} {j} → Rel A j → Type (lmax i j)
+Decidable rel = ∀ a₁ a₂ → Dec (rel a₁ a₂)

core/lib/groups/FormalSum.agda

@@ -0,0 +1,185 @@
+{-# OPTIONS --without-K #-}
+
+open import lib.Basics
+open import lib.NType2
+open import lib.types.Sigma
+open import lib.types.Pi
+open import lib.types.Group
+open import lib.types.Int
+open import lib.types.List
+open import lib.types.SetQuotient
+
+module lib.groups.FormalSum {i} where
+
+PreFormalSum : Type i → Type i
+PreFormalSum A = List (ℤ × A)
+
+module _ {A : Type i} (dec : has-dec-eq A) where
+
+  coef-pre : PreFormalSum A → (A → ℤ)
+  coef-pre l a = ℤsum $ map fst $ filter (λ{(_ , a') → dec a' a}) l
+
+  -- Extensional equality
+  FormalSum-rel : Rel (PreFormalSum A) i
+  FormalSum-rel l₁ l₂ = ∀ a → coef-pre l₁ a == coef-pre l₂ a
+
+  -- The quotient
+  FormalSum : Type i
+  FormalSum = SetQuotient FormalSum-rel
+
+  -- Properties of [coef-pre]
+  coef-pre-++ : ∀ l₁ l₂ a
+    → coef-pre (l₁ ++ l₂) a == coef-pre l₁ a ℤ+ coef-pre l₂ a
+  coef-pre-++ nil              l₂ a = idp
+  coef-pre-++ ((z , a') :: l₁) l₂ a with dec a' a
+  ... | inl _ = ap (z ℤ+_) (coef-pre-++ l₁ l₂ a)
+              ∙ ! (ℤ+-assoc z (coef-pre l₁ a) (coef-pre l₂ a))
+  ... | inr _ = coef-pre-++ l₁ l₂ a
+
+  flip-pre : PreFormalSum A → PreFormalSum A
+  flip-pre = map λ{(z , a) → (ℤ~ z , a)}
+
+  coef-pre-flip-pre : ∀ l a
+    → coef-pre (flip-pre l) a == ℤ~ (coef-pre l a)
+  coef-pre-flip-pre nil a = idp
+  coef-pre-flip-pre ((z , a') :: l) a with dec a' a
+  ... | inl _ = ap (ℤ~ z ℤ+_) (coef-pre-flip-pre l a)
+              ∙ ! (ℤ~-ℤ+ z (coef-pre l a))
+  ... | inr _ = coef-pre-flip-pre l a
+
+module _ {A : Type i} {dec : has-dec-eq A} where
+
+  coef : FormalSum dec → (A → ℤ)
+  coef = SetQuot-rec (→-is-set ℤ-is-set) (coef-pre dec) λ=
+
+  -- extensionality of formal sums.
+  coef=' : ∀ fs₁ fs₂ → (∀ a → coef fs₁ a == coef fs₂ a) → fs₁ == fs₂
+  coef=' = SetQuot-elim
+    (λ _ → Π-is-set λ _ → →-is-set $ =-preserves-set SetQuotient-is-set)
+    (λ l₁ → SetQuot-elim
+      (λ _ → →-is-set $ =-preserves-set SetQuotient-is-set)
+      (λ l₂ r → quot-rel r)
+      (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuotient-is-set _ _)))
+    (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → SetQuotient-is-set _ _))
+
+  coef= : ∀ {fs₁ fs₂} → (∀ a → coef fs₁ a == coef fs₂ a) → fs₁ == fs₂
+  coef= {fs₁} {fs₂} = coef=' fs₁ fs₂
+
+  -- TODO Use abstract [FormalSum].
+
+  infixl 80 _⊞_
+  _⊞_ : FormalSum dec → FormalSum dec → FormalSum dec
+  _⊞_ = SetQuot-rec
+    (→-is-set SetQuotient-is-set)
+    (λ l₁ → SetQuot-rec SetQuotient-is-set (q[_] ∘ (l₁ ++_))
+      (λ {l₂} {l₂'} r → quot-rel λ a
+        → coef-pre-++ dec l₁ l₂ a
+        ∙ ap (coef-pre dec l₁ a ℤ+_) (r a)
+        ∙ ! (coef-pre-++ dec l₁ l₂' a)))
+    (λ {l₁} {l₁'} r → λ= $ SetQuot-elim
+      (λ _ → =-preserves-set SetQuotient-is-set)
+      (λ l₂ → quot-rel λ a
+        → coef-pre-++ dec l₁ l₂ a
+        ∙ ap (_ℤ+ coef-pre dec l₂ a) (r a)
+        ∙ ! (coef-pre-++ dec l₁' l₂ a))
+      (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _)))
+
+  coef-⊞ : ∀ fs₁ fs₂ a → coef (fs₁ ⊞ fs₂) a == coef fs₁ a ℤ+ coef fs₂ a
+  coef-⊞ = SetQuot-elim
+    (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-set ℤ-is-set)
+    (λ l₁ → SetQuot-elim
+      (λ _ → Π-is-set λ _ → =-preserves-set ℤ-is-set)
+      (λ l₂ → coef-pre-++ dec l₁ l₂)
+      (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → ℤ-is-set _ _)))
+    (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → ℤ-is-set _ _))
+
+  ⊟ : FormalSum dec → FormalSum dec
+  ⊟ = SetQuot-rec SetQuotient-is-set (q[_] ∘ flip-pre dec)
+    λ {l₁} {l₂} r → quot-rel λ a
+      → coef-pre-flip-pre dec l₁ a ∙ ap ℤ~ (r a) ∙ ! (coef-pre-flip-pre dec l₂ a)
+
+  coef-⊟ : ∀ fs a → coef (⊟ fs) a == ℤ~ (coef fs a)
+  coef-⊟ = SetQuot-elim
+    (λ _ → Π-is-set λ _ → =-preserves-set ℤ-is-set)
+    (λ l a → coef-pre-flip-pre dec l a)
+    (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → ℤ-is-set _ _))
+
+  ⊞-unit : FormalSum dec
+  ⊞-unit = q[ nil ]
+
+  coef-⊞-unit : ∀ a → coef ⊞-unit a == 0
+  coef-⊞-unit a = idp
+
+{-
+  -- Favonia: These commented-out proofs are valid, but I want to promote
+  -- the usage of [coef=].
+
+  ⊞-unit-l : ∀ fs → ⊞-unit ⊞ fs == fs
+  ⊞-unit-l = SetQuot-elim
+    (λ _ → =-preserves-set SetQuotient-is-set)
+    (λ l → idp)
+    (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _))
+
+  ⊞-unit-r : ∀ fs → fs ⊞ ⊞-unit == fs
+  ⊞-unit-r = SetQuot-elim
+    (λ _ → =-preserves-set SetQuotient-is-set)
+    (λ l → ap q[_] $ ++-nil-r l)
+    (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _))
+-}
+
+  ⊞-unit-l : ∀ fs → ⊞-unit ⊞ fs == fs
+  ⊞-unit-l fs = coef= λ a → coef-⊞ ⊞-unit fs a
+
+  ⊞-unit-r : ∀ fs → fs ⊞ ⊞-unit == fs
+  ⊞-unit-r fs = coef= λ a → coef-⊞ fs ⊞-unit a ∙ ℤ+-unit-r _
+
+  ⊞-assoc : ∀ fs₁ fs₂ fs₃ → (fs₁ ⊞ fs₂) ⊞ fs₃ == fs₁ ⊞ (fs₂ ⊞ fs₃)
+  ⊞-assoc fs₁ fs₂ fs₃ = coef= λ a →
+    coef ((fs₁ ⊞ fs₂) ⊞ fs₃) a
+      =⟨ coef-⊞ (fs₁ ⊞ fs₂) fs₃ a ⟩
+    coef (fs₁ ⊞ fs₂) a ℤ+ coef fs₃ a
+      =⟨ coef-⊞ fs₁ fs₂ a |in-ctx _ℤ+ coef fs₃ a ⟩
+    (coef fs₁ a ℤ+ coef fs₂ a) ℤ+ coef fs₃ a
+      =⟨ ℤ+-assoc (coef fs₁ a) (coef fs₂ a) (coef fs₃ a) ⟩
+    coef fs₁ a ℤ+ (coef fs₂ a ℤ+ coef fs₃ a)
+      =⟨ ! $ coef-⊞ fs₂ fs₃ a |in-ctx coef fs₁ a ℤ+_ ⟩
+    coef fs₁ a ℤ+ coef (fs₂ ⊞ fs₃) a
+      =⟨ ! $ coef-⊞ fs₁ (fs₂ ⊞ fs₃) a ⟩
+    coef (fs₁ ⊞ (fs₂ ⊞ fs₃)) a
+      ∎
+
+  ⊟-inv-r : ∀ fs → fs ⊞ (⊟ fs) == ⊞-unit
+  ⊟-inv-r fs = coef= λ a → coef-⊞ fs (⊟ fs) a
+                         ∙ ap (coef fs a ℤ+_) (coef-⊟ fs a)
+                         ∙ ℤ~-inv-r (coef fs a)
+
+  ⊟-inv-l : ∀ fs → (⊟ fs) ⊞ fs == ⊞-unit
+  ⊟-inv-l fs = coef= λ a → coef-⊞ (⊟ fs) fs a
+                         ∙ ap (_ℤ+ coef fs a) (coef-⊟ fs a)
+                         ∙ ℤ~-inv-l (coef fs a)
+
+  FormalSum-group-structure : GroupStructure (FormalSum dec)
+  FormalSum-group-structure = record
+    { ident = ⊞-unit
+    ; inv = ⊟
+    ; comp = _⊞_
+    ; unitl = ⊞-unit-l
+    ; unitr = ⊞-unit-r
+    ; assoc = ⊞-assoc
+    ; invr = ⊟-inv-r
+    ; invl = ⊟-inv-l
+    }
+
+  FormalSum-group : Group i
+  FormalSum-group = group _ SetQuotient-is-set FormalSum-group-structure
+
+  has-finite-supports : (A → ℤ) → Type i
+  has-finite-supports f = Σ (FormalSum dec) λ fs → ∀ a → f a == coef fs a
+
+  has-finite-supports-is-prop : ∀ f → is-prop (has-finite-supports f)
+  has-finite-supports-is-prop f = all-paths-is-prop
+    λ{(fs₁ , match₁) (fs₂ , match₂) → pair=
+      (coef= λ a → ! (match₁ a) ∙ match₂ a)
+      (prop-has-all-paths-↓ $ Π-is-prop λ _ → ℤ-is-set _ _)}
+
+  -- TODO Create a quotient of formal sums with finite supports

core/lib/groups/Groups.agda

@@ -11,4 +11,5 @@ open import lib.groups.GroupProduct public
 open import lib.groups.PullbackGroup public
 open import lib.groups.TruncationGroup public
 open import lib.groups.HomotopyGroup public
+open import lib.groups.FormalSum public
 

core/lib/types/Bool.agda

@@ -5,13 +5,20 @@ open import lib.types.Pointed
 
 module lib.types.Bool where
 
+{-
 data Bool : Type₀ where
   true : Bool
   false : Bool
 
 {-# BUILTIN BOOL Bool #-}
 {-# BUILTIN FALSE false #-}
 {-# BUILTIN TRUE true #-}
+-}
+
+Bool = ⊤ ⊔ ⊤
+
+pattern true = inl unit
+pattern false = inr unit
 
 ⊙Bool : Ptd₀
 ⊙Bool = ⊙[ Bool , true ]

core/lib/types/Int.agda

@@ -270,3 +270,27 @@ private
 
 ℤ-group : Group₀
 ℤ-group = group _ ℤ-is-set ℤ-group-structure
+
+-- More properties about [ℤ~]
+
+ℤ~-succ : ∀ z → ℤ~ (succ z) == pred (ℤ~ z)
+ℤ~-succ (pos 0) = idp
+ℤ~-succ (pos (S n)) = idp
+ℤ~-succ (negsucc 0) = idp
+ℤ~-succ (negsucc (S n)) = idp
+
+ℤ~-pred : ∀ z → ℤ~ (pred z) == succ (ℤ~ z)
+ℤ~-pred (pos 0) = idp
+ℤ~-pred (pos 1) = idp
+ℤ~-pred (pos (S (S n))) = idp
+ℤ~-pred (negsucc 0) = idp
+ℤ~-pred (negsucc (S n)) = idp
+
+ℤ~-ℤ+ : ∀ z₁ z₂ → ℤ~ (z₁ ℤ+ z₂) == ℤ~ z₁ ℤ+ ℤ~ z₂
+ℤ~-ℤ+ (pos 0)         z₂ = idp
+ℤ~-ℤ+ (pos 1)         z₂ = ℤ~-succ z₂
+ℤ~-ℤ+ (pos (S (S n))) z₂ =
+  ℤ~-succ (pos (S n) ℤ+ z₂) ∙ ap pred (ℤ~-ℤ+ (pos (S n)) z₂)
+ℤ~-ℤ+ (negsucc O)     z₂ = ℤ~-pred z₂
+ℤ~-ℤ+ (negsucc (S n)) z₂ =
+  ℤ~-pred (negsucc n ℤ+ z₂) ∙ ap succ (ℤ~-ℤ+ (negsucc n) z₂)

core/lib/types/List.agda

@@ -1,9 +1,15 @@
 {-# OPTIONS --without-K #-}
 
 open import lib.Base
+open import lib.NType
+open import lib.Relation
+open import lib.types.Bool
+open import lib.types.Int
 
 module lib.types.List where
 
+infixr 80 _::_
+
 data List {i} (A : Type i) : Type i where
   nil : List A
   _::_ : A → List A → List A
@@ -22,3 +28,84 @@ hlist-curry : ∀ {i j} {L : List (Type i)} {B : HList L → Type (lmax i j)}
   (f : Π (HList L) B) → hlist-curry-type {j = j} L B
 hlist-curry {L = nil} f = f nil
 hlist-curry {L = A :: _} f = λ x → hlist-curry (λ xs → f (x :: xs))
+
+infixr 80 _++_
+_++_ : ∀ {i} {A : Type i} → List A → List A → List A
+nil ++ l = l
+(x :: l₁) ++ l₂ = x :: (l₁ ++ l₂)
+
+++-nil-r : ∀ {i} {A : Type i} (l : List A) → l ++ nil == l
+++-nil-r nil      = idp
+++-nil-r (a :: l) = ap (a ::_) $ ++-nil-r l
+
+-- [any] in Haskell
+data Any {i j} {A : Type i} (P : A → Type j) : List A → Type (lmax i j) where
+  here : ∀ {a} {l} → P a → Any P (a :: l)
+  there : ∀ {a} {l} → Any P l → Any P (a :: l)
+
+infix 80 _∈_
+_∈_ : ∀ {i} {A : Type i} → A → List A → Type i
+a ∈ l = Any (_== a) l
+
+Any-dec : ∀ {i j} {A : Type i} (P : A → Type j) → (∀ a → Dec (P a)) → (∀ l → Dec (Any P l))
+Any-dec P _   nil       = inr λ{()}
+Any-dec P dec (a :: l) with dec a
+... | inl p = inl $ here p
+... | inr p⊥ with Any-dec P dec l
+...   | inl ∃p = inl $ there ∃p
+...   | inr ∃p⊥ = inr λ{(here p) → p⊥ p; (there ∃p) → ∃p⊥ ∃p}
+
+∈-dec : ∀ {i} {A : Type i} → has-dec-eq A → ∀ a l → Dec (a ∈ l)
+∈-dec dec a l = Any-dec (_== a) (λ a' → dec a' a) l
+
+Any-++-l : ∀ {i j} {A : Type i} (P : A → Type j)
+  → ∀ l₁ l₂ → Any P l₁ → Any P (l₁ ++ l₂)
+Any-++-l P _ _ (here p)   = here p
+Any-++-l P _ _ (there ∃p) = there (Any-++-l P _ _ ∃p)
+
+∈-++-l : ∀ {i} {A : Type i} (a : A) → ∀ l₁ l₂ → a ∈ l₁ → a ∈ (l₁ ++ l₂)
+∈-++-l a = Any-++-l (_== a)
+
+Any-++-r : ∀ {i j} {A : Type i} (P : A → Type j)
+  → ∀ l₁ l₂ → Any P l₂ → Any P (l₁ ++ l₂)
+Any-++-r P nil      _ ∃p = ∃p
+Any-++-r P (a :: l) _ ∃p = there (Any-++-r P l _ ∃p)
+
+∈-++-r : ∀ {i} {A : Type i} (a : A) → ∀ l₁ l₂ → a ∈ l₂ → a ∈ (l₁ ++ l₂)
+∈-++-r a = Any-++-r (_== a)
+
+Any-++ : ∀ {i j} {A : Type i} (P : A → Type j)
+  → ∀ l₁ l₂ → Any P (l₁ ++ l₂) → (Any P l₁) ⊔ (Any P l₂)
+Any-++ P nil       l₂ ∃p         = inr ∃p
+Any-++ P (a :: l₁) l₂ (here p)   = inl (here p)
+Any-++ P (a :: l₁) l₂ (there ∃p) with Any-++ P l₁ l₂ ∃p
+... | inl ∃p₁ = inl (there ∃p₁)
+... | inr ∃p₂ = inr ∃p₂
+
+∈-++ : ∀ {i} {A : Type i} (a : A) → ∀ l₁ l₂ → a ∈ (l₁ ++ l₂) → (a ∈ l₁) ⊔ (a ∈ l₂)
+∈-++ a = Any-++ (_== a)
+
+-- [map] in Haskell
+map : ∀ {i j} {A : Type i} {B : Type j} → (A → B) → (List A → List B)
+map f nil = nil
+map f (a :: l) = f a :: map f l
+
+-- [foldr] in Haskell
+foldr : ∀ {i j} {A : Type i} {B : Type j} → (A → B → B) → B → List A → B
+foldr f b nil = b
+foldr f b (a :: l) = f a (foldr f b l)
+
+-- [concat] in Haskell
+concat : ∀ {i} {A : Type i} → List (List A) → List A
+concat l = foldr _++_ nil l
+
+ℤsum = foldr _ℤ+_ 0
+
+-- [filter] in Haskell
+-- Note that [Bool] is currently defined as a coproduct.
+filter : ∀ {i j k} {A : Type i} {Keep : A → Type j} {Drop : A → Type k}
+  → ((a : A) → Keep a ⊔ Drop a) → List A → List A
+filter p nil = nil
+filter p (a :: l) with p a
+... | inl _ = a :: filter p l
+... | inr _ = filter p l

core/lib/types/Nat.agda

@@ -123,7 +123,7 @@ O≤ (S m) = inr (O<S m)
 ≤-cancel-S (inl p) = inl (ap ℕ-pred p)
 ≤-cancel-S (inr lt) = inr (<-cancel-S lt)
 
-<-dec : Dec _<_
+<-dec : Decidable _<_
 <-dec _     O     = inr (≮O _)
 <-dec O     (S m) = inl (O<S m)
 <-dec (S n) (S m) with <-dec n m