Use new style Function hierarchy everywhere. (#1895)

Author: MatthewDaggitt

CHANGELOG.md

@@ -274,8 +274,14 @@ Non-backwards compatible changes
 
 #### Removal of the old function hierarchy
 
-* The switch to the new function hierarchy is complete and the following definitions
-  now use the new definitions instead of the old ones:
+* The switch to the new function hierarchy is complete and the following modules
+  have been completely switched over to use the new definitions:
+  ```
+  Data.Sum.Function.Setoid
+  Data.Sum.Function.Propositional
+  ```
+  
+* Additionally the following proofs now use the new definitions instead of the old ones:
   * `Algebra.Lattice.Properties.BooleanAlgebra`
   * `Algebra.Properties.CommutativeMonoid.Sum`
   * `Algebra.Properties.Lattice`
@@ -1080,6 +1086,10 @@ Deprecated modules
 
 * The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties`
 
+### Deprecation of `Data.Product.Function.Dependent.Setoid.WithK`
+
+* This module has been deprecated, as none of its contents actually depended on axiom K. The contents has been moved to `Data.Product.Function.Dependent.Setoid`.
+
 Deprecated names
 ----------------
 

src/Codata/Musical/Colist.agda

@@ -25,8 +25,7 @@ open import Data.Product.Base as Prod using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Function.Base
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
+open import Function.Bundles
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Poset; Setoid; Preorder)
@@ -100,14 +99,11 @@ data _⊑_ {A : Set a} : Rel (Colist A) a where
 -- Any can be expressed using _∈_ (and vice versa).
 
 Any-∈ : ∀ {xs} → Any P xs ↔ ∃ λ x → x ∈ xs × P x
-Any-∈ {P = P} = record
-  { to         = P.→-to-⟶ to
-  ; from       = P.→-to-⟶ (λ { (x , x∈xs , p) → from x∈xs p })
-  ; inverse-of = record
-    { left-inverse-of  = from∘to
-    ; right-inverse-of = λ { (x , x∈xs , p) → to∘from x∈xs p }
-    }
-  }
+Any-∈ {P = P} = mk↔ₛ′
+  to
+  (λ { (x , x∈xs , p) → from x∈xs p })
+  (λ { (x , x∈xs , p) → to∘from x∈xs p })
+  from∘to
   where
   to : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
   to (here  p) = _ , here P.refl , p

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -18,14 +18,22 @@ open import Data.Sum.Base
 open import Data.Sum.Properties
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
 open import Function.Base
-open import Function.Equality using (_⟨$⟩_)
-open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
-import Function.Related as Related
+open import Function.Bundles
+open import Function.Properties.Inverse using (↔-refl; ↔-sym; ↔⇒↣)
+import Function.Related.Propositional as Related
 open import Function.Related.TypeIsomorphisms
+open import Level
+open import Relation.Unary using (Pred)
 import Induction.WellFounded as WF
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Construct.On as On
 
+private
+  variable
+    a p : Level
+    A : Set a
+    P : Pred A p
+
 ------------------------------------------------------------------------
 -- Some code that is used to work around Agda's syntactic guardedness
 -- checker.
@@ -34,74 +42,70 @@ private
 
   infixr 5 _∷_ _⋎_
 
-  data ColistP {a} (A : Set a) : Set a where
+  data ColistP (A : Set a) : Set a where
     []  : ColistP A
     _∷_ : A → ∞ (ColistP A) → ColistP A
     _⋎_ : ColistP A → ColistP A → ColistP A
 
-  data ColistW {a} (A : Set a) : Set a where
+  data ColistW (A : Set a) : Set a where
     []  : ColistW A
     _∷_ : A → ColistP A → ColistW A
 
-  program : ∀ {a} {A : Set a} → Colist A → ColistP A
+  program : Colist A → ColistP A
   program []       = []
   program (x ∷ xs) = x ∷ ♯ program (♭ xs)
 
   mutual
 
-    _⋎W_ : ∀ {a} {A : Set a} → ColistW A → ColistP A → ColistW A
+    _⋎W_ : ColistW A → ColistP A → ColistW A
     []       ⋎W ys = whnf ys
     (x ∷ xs) ⋎W ys = x ∷ (ys ⋎ xs)
 
-    whnf : ∀ {a} {A : Set a} → ColistP A → ColistW A
+    whnf : ColistP A → ColistW A
     whnf []        = []
     whnf (x ∷ xs)  = x ∷ ♭ xs
     whnf (xs ⋎ ys) = whnf xs ⋎W ys
 
   mutual
 
-    ⟦_⟧P : ∀ {a} {A : Set a} → ColistP A → Colist A
+    ⟦_⟧P : ColistP A → Colist A
     ⟦ xs ⟧P = ⟦ whnf xs ⟧W
 
-    ⟦_⟧W : ∀ {a} {A : Set a} → ColistW A → Colist A
+    ⟦_⟧W : ColistW A → Colist A
     ⟦ [] ⟧W     = []
     ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P
 
   mutual
 
-    ⋎-homP : ∀ {a} {A : Set a} (xs : ColistP A) {ys} →
-             ⟦ xs ⋎ ys ⟧P ≈ ⟦ xs ⟧P Colist.⋎ ⟦ ys ⟧P
+    ⋎-homP : ∀ (xs : ColistP A) {ys} → ⟦ xs ⋎ ys ⟧P ≈ ⟦ xs ⟧P Colist.⋎ ⟦ ys ⟧P
     ⋎-homP xs = ⋎-homW (whnf xs) _
 
-    ⋎-homW : ∀ {a} {A : Set a} (xs : ColistW A) ys →
-             ⟦ xs ⋎W ys ⟧W ≈ ⟦ xs ⟧W Colist.⋎ ⟦ ys ⟧P
+    ⋎-homW : ∀ (xs : ColistW A) ys → ⟦ xs ⋎W ys ⟧W ≈ ⟦ xs ⟧W Colist.⋎ ⟦ ys ⟧P
     ⋎-homW (x ∷ xs) ys = x ∷ ♯ ⋎-homP ys
     ⋎-homW []       ys = begin ⟦ ys ⟧P ∎
       where open ≈-Reasoning
 
-  ⟦program⟧P : ∀ {a} {A : Set a} (xs : Colist A) →
-               ⟦ program xs ⟧P ≈ xs
+  ⟦program⟧P : ∀ (xs : Colist A) → ⟦ program xs ⟧P ≈ xs
   ⟦program⟧P []       = []
   ⟦program⟧P (x ∷ xs) = x ∷ ♯ ⟦program⟧P (♭ xs)
 
-  Any-⋎P : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
+  Any-⋎P : ∀ xs {ys} →
            Any P ⟦ program xs ⋎ ys ⟧P ↔ (Any P xs ⊎ Any P ⟦ ys ⟧P)
   Any-⋎P {P = P} xs {ys} =
-    Any P ⟦ program xs ⋎ ys ⟧P                ↔⟨ Any-cong Inv.id (⋎-homP (program xs)) ⟩
+    Any P ⟦ program xs ⋎ ys ⟧P                ↔⟨ Any-cong ↔-refl (⋎-homP (program xs)) ⟩
     Any P (⟦ program xs ⟧P Colist.⋎ ⟦ ys ⟧P)  ↔⟨ Any-⋎ _ ⟩
-    (Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P)   ↔⟨ Any-cong Inv.id (⟦program⟧P _) ⊎-cong (_ ∎) ⟩
+    (Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P)   ↔⟨ Any-cong ↔-refl (⟦program⟧P _) ⊎-cong (_ ∎) ⟩
     (Any P xs ⊎ Any P ⟦ ys ⟧P)                ∎
     where open Related.EquationalReasoning
 
   index-Any-⋎P :
-    ∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
-    (p : Any P ⟦ program xs ⋎ ys ⟧P) →
-    index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎P xs) ⟨$⟩ p)
+    ∀ xs {ys} (p : Any P ⟦ program xs ⋎ ys ⟧P) →
+    index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎P xs) p)
   index-Any-⋎P xs p
     with       Any-resp      id  (⋎-homW (whnf (program xs)) _) p
        | index-Any-resp {f = id} (⋎-homW (whnf (program xs)) _) p
   index-Any-⋎P xs p | q | q≡p
-    with Inverse.to (Any-⋎ ⟦ program xs ⟧P) ⟨$⟩ q
+    with Inverse.to (Any-⋎ ⟦ program xs ⟧P)  q
        |       index-Any-⋎ ⟦ program xs ⟧P      q
   index-Any-⋎P xs p | q | q≡p | inj₂ r | r≤q rewrite q≡p = r≤q
   index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q
@@ -115,95 +119,90 @@ private
 
 private
 
-  merge′ : ∀ {a} {A : Set a} → Colist (A × Colist A) → ColistP A
+  merge′ : Colist (A × Colist A) → ColistP A
   merge′ []               = []
   merge′ ((x , xs) ∷ xss) = x ∷ ♯ (program xs ⋎ merge′ (♭ xss))
 
-merge : ∀ {a} {A : Set a} → Colist (A × Colist A) → Colist A
+merge : Colist (A × Colist A) → Colist A
 merge xss = ⟦ merge′ xss ⟧P
 
 ------------------------------------------------------------------------
 -- Any lemma for merge.
 
-module _ {a p} {A : Set a} {P : A → Set p} where
-
-  Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss
-  Any-merge xss = inverse (proj₁ ∘ to xss) from (proj₂ ∘ to xss) to∘from
+Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss
+Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂ ∘ to xss)
+  where
+  open P.≡-Reasoning
+
+  -- The from function.
+
+  Q = λ { (x , xs) → P x ⊎ Any P xs }
+
+  from : ∀ {xss} → Any Q xss → Any P (merge xss)
+  from (here (inj₁ p))        = here p
+  from (here (inj₂ p))        = there (Inverse.from (Any-⋎P _)  (inj₁ p))
+  from (there {x = _ , xs} p) = there (Inverse.from (Any-⋎P xs) (inj₂ (from p)))
+
+  -- The from function is injective.
+
+  from-injective : ∀ {xss} (p₁ p₂ : Any Q xss) →
+                   from p₁ ≡ from p₂ → p₁ ≡ p₂
+  from-injective (here (inj₁ p))  (here (inj₁ .p)) P.refl = P.refl
+  from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq     =
+    P.cong (here ∘ inj₂) $
+    inj₁-injective $
+    Injection.injective (↔⇒↣ (↔-sym (Any-⋎P _))) $
+    there-injective eq
+  from-injective (here (inj₂ p₁)) (there p₂) eq with
+    Injection.injective (↔⇒↣ (↔-sym (Any-⋎P _)))
+                        {x = inj₁ p₁} {y = inj₂ (from p₂)}
+                        (there-injective eq)
+  ... | ()
+  from-injective (there p₁) (here (inj₂ p₂)) eq with
+    Injection.injective (↔⇒↣ (↔-sym (Any-⋎P _)))
+                           {x = inj₂ (from p₁)} {y = inj₁ p₂}
+                           (there-injective eq)
+  ... | ()
+  from-injective (there {x = _ , xs} p₁) (there p₂) eq =
+    P.cong there $
+    from-injective p₁ p₂ $
+    inj₂-injective $
+    Injection.injective (↔⇒↣ (↔-sym (Any-⋎P xs))) $
+    there-injective eq
+  -- The to function (defined as a right inverse of from).
+
+  Input = ∃ λ xss → Any P (merge xss)
+
+  InputPred : Input → Set _
+  InputPred (xss , p) = ∃ λ (q : Any Q xss) → from q ≡ p
+
+  to : ∀ xss p → InputPred (xss , p)
+  to xss p =
+    WF.All.wfRec (On.wellFounded size <′-wellFounded) _
+                 InputPred step (xss , p)
     where
-    open P.≡-Reasoning
-
-    -- The from function.
-
-    Q = λ { (x , xs) → P x ⊎ Any P xs }
-
-    from : ∀ {xss} → Any Q xss → Any P (merge xss)
-    from (here (inj₁ p))        = here p
-    from (here (inj₂ p))        = there (Inverse.from (Any-⋎P _)  ⟨$⟩ inj₁ p)
-    from (there {x = _ , xs} p) = there (Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ (from p))
-
-    -- The from function is injective.
-
-    from-injective : ∀ {xss} (p₁ p₂ : Any Q xss) →
-                     from p₁ ≡ from p₂ → p₁ ≡ p₂
-    from-injective (here (inj₁ p))  (here (inj₁ .p)) P.refl = P.refl
-    from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq     =
-      P.cong (here ∘ inj₂) $
-      inj₁-injective $
-      Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₁ p₂} $
-      there-injective eq
-    from-injective (here (inj₂ p₁)) (there p₂) eq
-      with Inverse.injective (Inv.sym (Any-⋎P _))
-                             {x = inj₁ p₁} {y = inj₂ (from p₂)}
-                             (there-injective eq)
-    ... | ()
-    from-injective (there p₁) (here (inj₂ p₂)) eq
-      with Inverse.injective (Inv.sym (Any-⋎P _))
-                             {x = inj₂ (from p₁)} {y = inj₁ p₂}
-                             (there-injective eq)
-    ... | ()
-    from-injective (there {x = _ , xs} p₁) (there p₂) eq =
-      P.cong there $
-      from-injective p₁ p₂ $
-      inj₂-injective $
-      Inverse.injective (Inv.sym (Any-⋎P xs))
-                        {x = inj₂ (from p₁)} {y = inj₂ (from p₂)} $
-      there-injective eq
-
-    -- The to function (defined as a right inverse of from).
-
-    Input = ∃ λ xss → Any P (merge xss)
-
-    Pred : Input → Set _
-    Pred (xss , p) = ∃ λ (q : Any Q xss) → from q ≡ p
-
-    to : ∀ xss p → Pred (xss , p)
-    to = λ xss p →
-      WF.All.wfRec (On.wellFounded size <′-wellFounded) _
-                   Pred step (xss , p)
-      where
-      size : Input → ℕ
-      size (_ , p) = index p
-
-      step : ∀ p → WF.WfRec (_<′_ on size) Pred p → Pred p
-      step ([]             , ())      rec
-      step ((x , xs) ∷ xss , here  p) rec = here (inj₁ p) , P.refl
-      step ((x , xs) ∷ xss , there p) rec
-        with Inverse.to (Any-⋎P xs) ⟨$⟩ p
-           | Inverse.left-inverse-of (Any-⋎P xs) p
-           | index-Any-⋎P xs p
-      ... | inj₁ q | P.refl | _   = here (inj₂ q) , P.refl
-      ... | inj₂ q | P.refl | q≤p =
-        Prod.map there
-                 (P.cong (there ∘ _⟨$⟩_ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
-                 (rec (♭ xss , q) (s≤′s q≤p))
-
-    to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))
+    size : Input → ℕ
+    size (_ , p) = index p
+
+    step : ∀ p → WF.WfRec (_<′_ on size) InputPred p → InputPred p
+    step ([]             , ())      rec
+    step ((x , xs) ∷ xss , here  p) rec = here (inj₁ p) , P.refl
+    step ((x , xs) ∷ xss , there p) rec
+      with Inverse.to (Any-⋎P xs) p
+         | Inverse.strictlyInverseʳ (Any-⋎P xs) p
+         | index-Any-⋎P xs p
+    ... | inj₁ q | P.refl | _   = here (inj₂ q) , P.refl
+    ... | inj₂ q | P.refl | q≤p =
+      Prod.map there
+               (P.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
+               (rec (♭ xss , q) (s≤′s q≤p))
+
+  to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))
 
 -- Every member of xss is a member of merge xss, and vice versa (with
 -- equal multiplicities).
 
-∈-merge : ∀ {a} {A : Set a} {y : A} xss →
-          y ∈ merge xss ↔ ∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs)
+∈-merge : ∀ {y : A} xss → y ∈ merge xss ↔ ∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs)
 ∈-merge {y = y} xss =
   y ∈ merge xss                                           ↔⟨ Any-merge _ ⟩
   Any (λ { (x , xs) → y ≡ x ⊎ y ∈ xs }) xss               ↔⟨ Any-∈ ⟩