Pointwise function changes

Base/Change/Algebra.agda

@@ -145,49 +145,6 @@ syntax update′ x v dv = v ⊞₍ x ₎ dv
 diff′ = Family.diff
 syntax diff′ x u v = u ⊟₍ x ₎ v
 
--- Derivatives
--- ===========
---
--- This corresponds to Def. 2.4 in the paper.
-
-RawChange : ∀ {a b c d} {A : Set a} {B : Set b} →
-  {{CA : ChangeAlgebra c A}} →
-  {{CB : ChangeAlgebra d B}} →
-  (f : A → B) →
-  Set (a ⊔ c ⊔ d)
-RawChange f = ∀ a (da : Δ a) → Δ (f a)
-
-IsDerivative : ∀ {a b c d} {A : Set a} {B : Set b} →
-  {{CA : ChangeAlgebra c A}} →
-  {{CB : ChangeAlgebra d B}} →
-  (f : A → B) →
-  (df : RawChange f) →
-  Set (a ⊔ b ⊔ c)
-IsDerivative f df = ∀ a da → f a ⊞ df a da ≡ f (a ⊞ da)
-
--- This is a variant of IsDerivative for change algebra families.
-RawChange₍_,_₎ : ∀ {a b p q c d} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
-  {{CP : ChangeAlgebraFamily c P}} →
-  {{CQ : ChangeAlgebraFamily d Q}} →
-  (x : A) →
-  (y : B) →
-  (f : P x → Q y) → Set (c ⊔ d ⊔ p)
-RawChange₍_,_₎ x y f = ∀ px (dpx : Δ₍_₎ x px) → Δ₍_₎ y (f px)
-
-IsDerivative₍_,_₎ : ∀ {a b p q c d} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
-  {{CP : ChangeAlgebraFamily c P}} →
-  {{CQ : ChangeAlgebraFamily d Q}} →
-  (x : A) →
-  (y : B) →
-  (f : P x → Q y) →
-  (df : RawChange₍_,_₎ x y f) →
-  Set (p ⊔ q ⊔ c)
-IsDerivative₍_,_₎ {P = P} {{CP}} {{CQ}} x y f df = IsDerivative {{change-algebra₍ _ ₎}} {{change-algebra₍ _ ₎}} f df where
-  CPx = change-algebra₍_₎ {{CP}} x
-  CQy = change-algebra₍_₎ {{CQ}} y
-
--- Lemma 2.5 appears in Base.Change.Equivalence.
-
 -- Abelian Groups Induce Change Algebras
 -- =====================================
 --
@@ -253,9 +210,53 @@ module GroupChanges
 -- arguments, and provides a changeAlgebra for (A → B). The proofs
 -- are by equational reasoning using 2.1e for A and B.
 
+module _ {a} {b} {c} {d} {A : Set a} {B : Set b} {{CA : ChangeAlgebra c A}} {{CB : ChangeAlgebra d B}}
+  where
+    -- Derivatives
+    -- ===========
+    --
+    -- This corresponds to Def. 2.4 in the paper.
+
+    RawChange :
+      (f : A → B) →
+      Set (a ⊔ c ⊔ d)
+    RawChange f = ∀ a (da : Δ a) → Δ (f a)
+
+    IsDerivative :
+      (f : A → B) →
+      (df : RawChange f) →
+      Set (a ⊔ b ⊔ c)
+    IsDerivative f df = ∀ a da → f a ⊞ df a da ≡ f (a ⊞ da)
+
+module _ {a b p q c d} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q}
+       {{CP : ChangeAlgebraFamily c P}} {{CQ : ChangeAlgebraFamily d Q}}
+  where
+
+    -- This is a variant of IsDerivative for change algebra families.
+    RawChange₍_,_₎ :
+      (x : A) →
+      (y : B) →
+      (f : P x → Q y) → Set (c ⊔ d ⊔ p)
+    RawChange₍_,_₎ x y f = ∀ px (dpx : Δ₍_₎ x px) → Δ₍_₎ y (f px)
+
+    IsDerivative₍_,_₎ :
+      (x : A) →
+      (y : B) →
+      (f : P x → Q y) →
+      (df : RawChange₍_,_₎ x y f) →
+      Set (p ⊔ q ⊔ c)
+    IsDerivative₍_,_₎ x y f df = IsDerivative {{change-algebra₍ _ ₎}} {{change-algebra₍ _ ₎}} f df where
+      CPx = change-algebra₍_₎ {{CP}} x
+      CQy = change-algebra₍_₎ {{CQ}} y
+
+    -- Lemma 2.5 appears in Base.Change.Equivalence.
+
 module FunctionChanges
     {a} {b} {c} {d} (A : Set a) (B : Set b) {{CA : ChangeAlgebra c A}} {{CB : ChangeAlgebra d B}}
   where
+    Derivative : (A → B) → Set (a ⊔ b ⊔ c ⊔ d)
+    Derivative f = Σ[ f′ ∈ RawChange f ] IsDerivative f f′
+
     -- This corresponds to Definition 2.6 in the paper.
     record FunctionChange (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
       field

Base/Change/PointwiseFunctionChanges.agda

@@ -0,0 +1,91 @@
+module Base.Change.PointwiseFunctionChanges where
+
+open import Data.Product
+open import Function
+open import Relation.Binary.PropositionalEquality
+open import Postulate.Extensionality
+open import Level
+
+open import Base.Ascription
+open import Base.HetEqExtra
+open import Base.Change.Algebra
+
+-- Define an alternative change structure on functions based on pointwise changes. Both functions and changes carry a derivative with them.
+
+module AltFunctionChanges ℓ (A B : Set ℓ) {{CA : ChangeAlgebra ℓ A}} {{CB : ChangeAlgebra ℓ B}} where
+  open FunctionChanges A B {{CA}} {{CB}} using (Derivative)
+
+  RawChangeP : (f : A → B) → Set ℓ
+  RawChangeP f = (a : A) → Δ (f a)
+
+  FunBaseT : Set ℓ
+  FunBaseT = Σ[ f ∈ (A → B) ] Derivative f
+
+  _raw⊕_ : (f : A → B) → (df : RawChangeP f) → (A → B)
+  f raw⊕ df = λ a → f a ⊞ df a
+
+  _raw⊝_ : (g f : A → B) → RawChangeP f
+  g raw⊝ f = λ a → g a ⊟ f a
+
+  rawnil : (f : A → B) → RawChangeP f
+  rawnil f = λ a → nil (f a)
+
+  raw-update-nil : ∀ f → f raw⊕ (rawnil f) ≡ f
+  raw-update-nil f = ext (λ a → update-nil (f a))
+  raw-update-diff : ∀ f g → f raw⊕ (g raw⊝ f) ≡ g
+  raw-update-diff f g = ext (λ a → update-diff (g a) (f a))
+
+  Derivative-f⊕df : ∀ (f : A → B) (df : RawChangeP f) → Derivative (f raw⊕ df)
+  Derivative-f⊕df f df
+    = ( (λ a da → f (a ⊞ da) ⊞ df (a ⊞ da) ⊟ (f a ⊞ df a))
+      , (λ a da → update-diff (f (a ⊞ da) ⊞ df (a ⊞ da)) (f a ⊞ df a))
+      )
+  -- Instead of ` f (a ⊞ da) ` we could/should use` f a ⊞ f′ a da `,
+  -- but we'd need to invoke the right equivalence for the expression to typecheck.
+  -- XXX: that derivative is very non-incremental.
+  -- Alternatives:
+  -- 1. (invert df x) andThen (f' x dx) andThen (df (x ⊞ dx))
+  -- 2. include a derivative in the function change as well. That would limit the point though.
+
+  FChange₀ : (A → B) → Set ℓ
+  FChange₀ f₀ = Σ[ df ∈ RawChangeP f₀ ] Derivative (f₀ raw⊕ df)
+
+  FChange : FunBaseT → Set ℓ
+  FChange (f₀ , _f₀′) = FChange₀ f₀
+
+  _⊕_ : (f : FunBaseT) → FChange f → FunBaseT
+  (f₀ , _f₀′) ⊕ (df , f₁′) = (f₀ raw⊕ df , f₁′)
+
+  -- Lemmas to transport across the f₁ᵇ ≅ f₁ᵃ equality.
+  transport-derivative-to-equiv-base : ∀ {f₁ᵃ f₁ᵇ} (eq : f₁ᵇ ≡ f₁ᵃ) → Derivative f₁ᵃ → Derivative f₁ᵇ
+  transport-derivative-to-equiv-base refl f₁′ = f₁′
+
+  transport-base-f : ∀ {f₀ f₁} df → Derivative f₁ → (f₀ raw⊕ df ≡ f₁) → FChange₀ f₀
+  transport-base-f df f₁′ eq = df , transport-derivative-to-equiv-base eq f₁′
+  -- Implementation note: transport-base-f can't pattern match on eq because of a unification failure.
+  -- Hence we called the generalized transport-derivative-to-equiv-base, where the problem disappears.
+
+  transport-base-f-eq : ∀ {f₁ᵃ f₁ᵇ} (eq : f₁ᵇ ≡ f₁ᵃ) (f₁′ : Derivative f₁ᵃ) →
+    (f₁ᵇ , transport-derivative-to-equiv-base eq f₁′) ≡ (f₁ᵃ , f₁′)
+  transport-base-f-eq refl f₁′ = refl
+
+  f-nil : (f : FunBaseT) → FChange f
+  f-nil (f , f′) = transport-base-f (rawnil f) f′ (raw-update-nil f)
+
+  f-update-nil : ∀ fstr → (fstr ⊕ f-nil fstr) ≡ fstr
+  f-update-nil (f , f′) = transport-base-f-eq (raw-update-nil f) f′
+
+  _⊝_ : (g f : FunBaseT) → FChange f
+  _⊝_ (g , g′) (f , _f′) = transport-base-f (g raw⊝ f) g′ (raw-update-diff f g)
+
+  f-update-diff : ∀ gstr fstr → fstr ⊕ (gstr ⊝ fstr) ≡ gstr
+  f-update-diff (g , g′) (f , _f′) = transport-base-f-eq (raw-update-diff f g) g′
+
+  changeAlgebra : ChangeAlgebra ℓ FunBaseT
+  changeAlgebra = record
+                    { Change = FChange
+                    ; update = _⊕_
+                    ; diff = _⊝_
+                    ; nil = f-nil
+                    ; isChangeAlgebra = record { update-diff = f-update-diff ; update-nil = f-update-nil }
+                    }

Base/HetEqExtra.agda

@@ -0,0 +1,19 @@
+module Base.HetEqExtra where
+
+open import Relation.Binary.HeterogeneousEquality
+
+-- More dependent variant of subst₂ from Relation.Binary.HeterogeneousEquality, see e.g.
+-- http://stackoverflow.com/a/24255198/53974
+hsubst₂ : ∀ {a b p} {A : Set a} {B : A → Set b} (P : (a : A) → (B a) → Set p) →
+         ∀ {x₁ x₂ y₁ y₂} → x₁ ≅ x₂ → y₁ ≅ y₂ → P x₁ y₁ → P x₂ y₂
+hsubst₂ P refl refl p = p
+
+-- subst-removable for hsubst₂
+hsubst₂-removable : ∀ {a b p} {A : Set a} {B : A → Set b} (P : (a : A) → (B a) → Set p) →
+         ∀ {x₁ x₂ y₁ y₂} (≅₁ : x₁ ≅ x₂) (≅₂ : y₁ ≅ y₂) p → hsubst₂ P ≅₁ ≅₂ p ≅ p
+hsubst₂-removable P refl refl p = refl
+
+cong₃ : ∀ {a b c d} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c} {D : ∀ x y → C x y → Set d}
+        {x y u v z w}
+        (f : (x : A) (y : B x) → (z : C x y) → D x y z) → x ≅ y → u ≅ v → z ≅ w → f x u z ≅ f y v w
+cong₃ f refl refl refl = refl

Postulate/Extensionality.agda

@@ -11,6 +11,7 @@ module Postulate.Extensionality where
 
 
 open import Relation.Binary.PropositionalEquality
+import Relation.Binary.HeterogeneousEquality as H
 
 postulate ext : ∀ {a b} → Extensionality a b
 
@@ -25,3 +26,6 @@ ext³ : ∀
   ((a : A) (b : B a) (c : C a b) → f a b c ≡ g a b c) → f ≡ g
 
 ext³ fabc=gabc = ext (λ a → ext (λ b → ext (λ c → fabc=gabc a b c)))
+
+hext : ∀ {a b} → {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f H.≅ g
+hext f≡g = H.≡-to-≅ (ext f≡g)