Prove lemma 3.5 (7).

2 files changed, 23 insertions, 12 deletions

diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 5ed031b..1a37326 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -8,10 +8,11 @@ module Cfe.Language.Indexed.Construct.Iterate
 
 open Setoid over using () renaming (Carrier to C)
 
+open import Algebra
 open import Cfe.Language over as L
 open import Cfe.Language.Indexed.Homogeneous over
 open import Data.List
-open import Data.Nat as ℕ hiding (_⊔_; _≤_)
+open import Data.Nat as ℕ hiding (_⊔_; _≤_; _^_)
 open import Data.Product as Product
 open import Function
 open import Level hiding (Lift) renaming (suc to lsuc)
@@ -20,11 +21,13 @@ open import Relation.Binary.PropositionalEquality as ≡
 
 open IndexedLanguage
 
-iter : ∀ {a} {A : Set a} → (A → A) → ℕ → A → A
-iter f ℕ.zero = id
-iter f (ℕ.suc n) = f ∘ iter f n
+infix 9 _^_
 
-f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f (iter f n x) ≡ iter f n (f x)
+_^_ : ∀ {a} {A : Set a} → Op₁ A → ℕ → Op₁ A
+f ^ zero = id
+f ^ (suc n) = f ∘ (f ^ n)
+
+f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f ((f ^ n) x) ≡ (f ^ n) (f x)
 f-fn-x≡fn-f-x f ℕ.zero x = refl
 f-fn-x≡fn-f-x f (suc n) x = ≡.cong f (f-fn-x≡fn-f-x f n x)
 
@@ -32,9 +35,10 @@ module _
   {a aℓ} (A : B.Setoid a aℓ)
   where
 
-  module A = B.Setoid A
+  private
+    module A = B.Setoid A
 
-  f≈g⇒fn≈gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≈ y → f x A.≈ g y) → ∀ n x → iter f n x A.≈ iter g n x
+  f≈g⇒fn≈gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≈ y → f x A.≈ g y) → ∀ n x → (f ^ n) x A.≈ (g ^ n) x
   f≈g⇒fn≈gn f≈g ℕ.zero x = A.refl
   f≈g⇒fn≈gn f≈g (suc n) x = f≈g (f≈g⇒fn≈gn f≈g n x)
 
@@ -42,10 +46,11 @@ module _
   {a aℓ₁ aℓ₂} (A : B.Poset a aℓ₁ aℓ₂)
   where
 
-  module A′ = B.Poset A
+  private
+    module A = B.Poset A
 
-  f≤g⇒fn≤gn : {f g : A′.Carrier → A′.Carrier} → (∀ {x y} → x A′.≤ y → f x A′.≤ g y) → ∀ n x → iter f n x A′.≤ iter g n x
-  f≤g⇒fn≤gn f≤g ℕ.zero x = A′.refl
+  f≤g⇒fn≤gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≤ y → f x A.≤ g y) → ∀ n x → (f ^ n) x A.≤ (g ^ n) x
+  f≤g⇒fn≤gn f≤g ℕ.zero x = A.refl
   f≤g⇒fn≤gn f≤g (suc n) x = f≤g (f≤g⇒fn≤gn f≤g n x)
 
 module _
@@ -56,7 +61,7 @@ module _
     { Carrierᵢ = ℕ
     ; _≈ᵢ_ = ≡._≡_
     ; isEquivalenceᵢ = ≡.isEquivalence
-    ; F = λ n → iter f n (Lift a ∅)
+    ; F = λ n → (f ^ n) (Lift a ∅)
     ; cong = λ {≡.refl → ≈-refl}
     }
 
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index b2630ce..756877c 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -13,7 +13,7 @@ open import Cfe.Language.Base over
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Function
-open import Level
+open import Level hiding (Lift)
 
 ≈-refl : ∀ {a} → Reflexive (_≈_ {a})
 ≈-refl {x = A} = record
@@ -94,3 +94,9 @@ setoid a = record { isEquivalence = ≈-isEquivalence {a} }
 
 poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
 poset a = record { isPartialOrder = ≤-isPartialOrder a }
+
+lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
+lift-cong b L = record
+  { f = lower
+  ; f⁻¹ = lift
+  }