From abe9461e0dc194c160d97fee23a1646097a0c264 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 24 Mar 2021 17:01:29 +0000
Subject: Prove lemma 3.5 (7).

---
 src/Cfe/Language/Indexed/Construct/Iterate.agda | 27 +++++++++++++++----------
 1 file changed, 16 insertions(+), 11 deletions(-)

(limited to 'src/Cfe/Language/Indexed/Construct')

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}
     }
 
-- 
cgit v1.2.3