From 8abb1b5601fabf5e7560d08faa6e633e60663e0a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 29 Apr 2021 20:58:04 +0100
Subject: Finally prove that e [ μ e / zero ] ≈ μ e.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Complete proof of generator.
---
 src/Cfe/Function/Power.agda | 37 -------------------------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 src/Cfe/Function/Power.agda

(limited to 'src/Cfe/Function/Power.agda')

diff --git a/src/Cfe/Function/Power.agda b/src/Cfe/Function/Power.agda
deleted file mode 100644
index da3b335..0000000
--- a/src/Cfe/Function/Power.agda
+++ /dev/null
@@ -1,37 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Cfe.Function.Power where
-
-open import Data.Nat using (ℕ)
-open import Data.Product using (∃-syntax; _×_)
-open import Function using (id; _∘_)
-open import Level using (Level; _⊔_)
-open import Relation.Binary using (Rel; REL)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_)
-
-private
-  variable
-    a : Level
-    A : Set a
-
-infix 10 _^_
-
-------------------------------------------------------------------------
--- Definition
-
-_^_ : (A → A) → ℕ → A → A
-f ^ ℕ.zero = id
-f ^ ℕ.suc n = f ∘ f ^ n
-
-------------------------------------------------------------------------
--- Properties
-
-f∼g⇒fⁿ∼gⁿ :
-  ∀ {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) {f g 0A 0B} →
-  0A ∼ 0B → (∀ {x y} → x ∼ y → f x ∼ g y) → ∀ n → (f ^ n) 0A ∼ (g ^ n) 0B
-f∼g⇒fⁿ∼gⁿ _ refl ext    ℕ.zero = refl
-f∼g⇒fⁿ∼gⁿ ∼ refl ext (ℕ.suc n) = ext (f∼g⇒fⁿ∼gⁿ ∼ refl ext n)
-
-fⁿf≡fⁿ⁺¹ : ∀ (f : A → A) n → (f ^ n) ∘ f ≡ f ^ (ℕ.suc n)
-fⁿf≡fⁿ⁺¹ f    ℕ.zero = _≡_.refl
-fⁿf≡fⁿ⁺¹ f (ℕ.suc n) = cong (f ∘_) (fⁿf≡fⁿ⁺¹ f n)
-- 
cgit v1.2.3