From 94f3f88067c94d37b3d28d4db5c283d21e497963 Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 23 Jun 2022 22:14:28 +0200 Subject: [PATCH] fixed file name --- misc/llpo.html | 111 +++++++++++++++++++++++++++++++++++++++++++++++++ misc/wlpo.html | 111 ------------------------------------------------- 2 files changed, 111 insertions(+), 111 deletions(-) create mode 100644 misc/llpo.html delete mode 100644 misc/wlpo.html diff --git a/misc/llpo.html b/misc/llpo.html new file mode 100644 index 0000000..d7f1e40 --- /dev/null +++ b/misc/llpo.html @@ -0,0 +1,111 @@ + +llpo
{-# OPTIONS --safe --without-K #-}
+
+open import Agda.Primitive renaming (Set to 𝒰)
+open import Agda.Builtin.Nat renaming (Nat to ) hiding (_+_)
+open import Agda.Builtin.Bool renaming (Bool to 𝟚; false to 𝟘; true to 𝟙)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Function using (_∘_; const)
+
+{- Variables -}
+variable
+   : Level
+   : Level
+  A : 𝒰 
+  B : 𝒰 
+  C : 𝒰 
+
+{- Types -}
+
+data  : 𝒰₀ where
+
+infixr 8 ¬_
+¬_ : 𝒰   𝒰 
+¬ p = p  
+
+infixr 2 _+_
+data _+_ (A : 𝒰 ) (B : 𝒰 ) : 𝒰 (  ) where
+  inl : A  A + B
+  inr : B  A + B
+
+binary-sequence : 𝒰₀
+binary-sequence =   𝟚  
+
+all-zeros : binary-sequence  𝒰₀
+all-zeros α = (n : )  α n  𝟘
+
+has-WLPO : binary-sequence  𝒰₀
+has-WLPO α = all-zeros α + ¬ (all-zeros α)   
+
+WLPO : 𝒰₀
+WLPO = (α : binary-sequence)  has-WLPO α   
+
+at-most-one-one : binary-sequence  𝒰₀
+at-most-one-one α = (a b : )  α a  𝟙  α b  𝟙  a  b
+
+-- needed for LLPO
+dup :   
+dup 0 = 0
+dup (suc n) = suc (suc (dup n))
+
+evens :   
+evens = dup
+
+odds :   
+odds = suc  dup
+
+LLPO : 𝒰₀
+LLPO = (α : binary-sequence)  at-most-one-one α  all-zeros (α  evens) + all-zeros (α  odds)
+
+{- Eliminators -}
+⊥-elim :   A
+⊥-elim ()
+
++-elim : A + B  (A  C)  (B  C)  C
++-elim (inl a) f _ = f a
++-elim (inr b) _ g = g b
+
+-- A bit funky, but comes in handy
+𝟚-elim : (C : 𝟚  𝒰 )  (b : 𝟚)  (b  𝟘  C 𝟘)  (b  𝟙  C 𝟙)  C b
+𝟚-elim _ 𝟘 z _ = z refl
+𝟚-elim _ 𝟙 _ o = o refl
+
+{- Lemmas -}
+
+-- I think this is a bit ugly, but it works and I'm tired
+e≢o : {n m : }  ¬ (evens n  odds m)
+e≢o {zero} {zero} ()
+e≢o {zero} {suc m} ()
+e≢o {suc n} {zero} ()
+e≢o {suc n} {suc m} p = e≢o {n} {m} (ds (tr (he n) (ho m) p))
+  where
+    he : (q : )  evens (suc q)  suc (suc (evens q))
+    he _ = refl
+
+    ho : (q : )  odds (suc q)  suc (suc (odds q))
+    ho _ = refl
+
+    tr :  {a b c d : }  a  b  c  d  a  c  b  d
+    tr refl refl refl = refl
+
+    ds :  {q r : }  suc (suc q)  suc (suc r)  q  r
+    ds {zero} {zero} _ = refl
+    ds {suc q} {suc r} refl = refl
+
+
+lemma : (α : binary-sequence)  at-most-one-one α  ¬ all-zeros (α  evens)  all-zeros (α  odds)
+lemma α am11 na0e i = 𝟚-elim (_≡ 𝟘) ((α  odds) i)
+                             (const refl)
+                              p₁  ⊥-elim (na0e  j  𝟚-elim (_≡ 𝟘) ((α  evens) j)
+                                                                (const refl)
+                                                                 p₂  ⊥-elim (e≢o (am11 (evens j) (odds i) p₂ p₁))))))
+
+
+{- The main dish -}
+WLPO→LLPO : WLPO  LLPO
+WLPO→LLPO wlpo α am11 = +-elim (wlpo (α  evens))
+                              inl
+                               na0e  +-elim (wlpo (α  odds))
+                                               inr
+                                                na0o  ⊥-elim (na0o (lemma α am11 na0e))))
+
\ No newline at end of file diff --git a/misc/wlpo.html b/misc/wlpo.html deleted file mode 100644 index 35761c5..0000000 --- a/misc/wlpo.html +++ /dev/null @@ -1,111 +0,0 @@ - -wlpo
{-# OPTIONS --safe --without-K #-}
-
-open import Agda.Primitive renaming (Set to 𝒰)
-open import Agda.Builtin.Nat renaming (Nat to ) hiding (_+_)
-open import Agda.Builtin.Bool renaming (Bool to 𝟚; false to 𝟘; true to 𝟙)
-open import Agda.Builtin.Equality using (_≡_; refl)
-open import Function using (_∘_; const)
-
-{- Variables -}
-variable
-   : Level
-   : Level
-  A : 𝒰 
-  B : 𝒰 
-  C : 𝒰 
-
-{- Types -}
-
-data  : 𝒰₀ where
-
-infixr 8 ¬_
-¬_ : 𝒰   𝒰 
-¬ p = p  
-
-infixr 2 _+_
-data _+_ (A : 𝒰 ) (B : 𝒰 ) : 𝒰 (  ) where
-  inl : A  A + B
-  inr : B  A + B
-
-binary-sequence : 𝒰₀
-binary-sequence =   𝟚  
-
-all-zeros : binary-sequence  𝒰₀
-all-zeros α = (n : )  α n  𝟘
-
-has-WLPO : binary-sequence  𝒰₀
-has-WLPO α = all-zeros α + ¬ (all-zeros α)   
-
-WLPO : 𝒰₀
-WLPO = (α : binary-sequence)  has-WLPO α   
-
-at-most-one-one : binary-sequence  𝒰₀
-at-most-one-one α = (a b : )  α a  𝟙  α b  𝟙  a  b
-
--- needed for LLPO
-dup :   
-dup 0 = 0
-dup (suc n) = suc (suc (dup n))
-
-evens :   
-evens = dup
-
-odds :   
-odds = suc  dup
-
-LLPO : 𝒰₀
-LLPO = (α : binary-sequence)  at-most-one-one α  all-zeros (α  evens) + all-zeros (α  odds)
-
-{- Eliminators -}
-⊥-elim :   A
-⊥-elim ()
-
-+-elim : A + B  (A  C)  (B  C)  C
-+-elim (inl a) f _ = f a
-+-elim (inr b) _ g = g b
-
--- A bit funky, but comes in handy
-𝟚-elim : (C : 𝟚  𝒰 )  (b : 𝟚)  (b  𝟘  C 𝟘)  (b  𝟙  C 𝟙)  C b
-𝟚-elim _ 𝟘 z _ = z refl
-𝟚-elim _ 𝟙 _ o = o refl
-
-{- Lemmas -}
-
--- I think this is a bit ugly, but it works and I'm tired
-e≢o : {n m : }  ¬ (evens n  odds m)
-e≢o {zero} {zero} ()
-e≢o {zero} {suc m} ()
-e≢o {suc n} {zero} ()
-e≢o {suc n} {suc m} p = e≢o {n} {m} (ds (tr (he n) (ho m) p))
-  where
-    he : (q : )  evens (suc q)  suc (suc (evens q))
-    he _ = refl
-
-    ho : (q : )  odds (suc q)  suc (suc (odds q))
-    ho _ = refl
-
-    tr :  {a b c d : }  a  b  c  d  a  c  b  d
-    tr refl refl refl = refl
-
-    ds :  {q r : }  suc (suc q)  suc (suc r)  q  r
-    ds {zero} {zero} _ = refl
-    ds {suc q} {suc r} refl = refl
-
-
-lemma : (α : binary-sequence)  at-most-one-one α  ¬ all-zeros (α  evens)  all-zeros (α  odds)
-lemma α am11 na0e i = 𝟚-elim (_≡ 𝟘) ((α  odds) i)
-                             (const refl)
-                              p₁  ⊥-elim (na0e  j  𝟚-elim (_≡ 𝟘) ((α  evens) j)
-                                                                (const refl)
-                                                                 p₂  ⊥-elim (e≢o (am11 (evens j) (odds i) p₂ p₁))))))
-
-
-{- The main dish -}
-WLPO→LLPO : WLPO  LLPO
-WLPO→LLPO wlpo α am11 = +-elim (wlpo (α  evens))
-                              inl
-                               na0e  +-elim (wlpo (α  odds))
-                                               inr
-                                                na0o  ⊥-elim (na0o (lemma α am11 na0e))))
-
\ No newline at end of file