[Simplified (?) small⇒big⟶∞ by using the double-negation monad.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081107182008] hunk ./Semantics/Equivalence.agda 12
-open import Infinite hiding (_⇓_)
+open import Infinite hiding (_⇓_; return)
hunk ./Semantics/Equivalence.agda 15
-open import Data.Star
+open import Data.Star hiding (return)
hunk ./Semantics/Equivalence.agda 21
+open import Category.Monad
+open RawMonad ¬¬-Monad hiding (_>>_)
hunk ./Semantics/Equivalence.agda 298
-small⇒big⟶∞ (run ⌜ v ⌝)    i  (Red Val       ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
-small⇒big⟶∞ (run ⌜ v ⌝)    .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
-small⇒big⟶∞ (run (loop x)) i  ⟶∞                    ¬⇑ = Loop.lemma ⟶∞ helper
+small⇒big⟶∞ (run ⌜ v ⌝)    i  (Red Val       ◅∞ ⟶∞) = const (done↛∞ ⟶∞)
+small⇒big⟶∞ (run ⌜ v ⌝)    .U (Red (Int int) ◅∞ ⟶∞) = const (done↛∞ ⟶∞)
+small⇒big⟶∞ (run (loop x)) i  ⟶∞ = helper =<< Loop.lemma ⟶∞
hunk ./Semantics/Equivalence.agda 302
-  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> x ⟶⋆[ i ] done (nat n)) -> ⊥
-  helper (inj₁ x⟶∞)        = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Loop ∘ Seqn₁)
-  helper (inj₂ (n , x⟶⋆n)) = ¬⇑ (loop-⇑ (n , small⇒big⟶⋆ x⟶⋆n))
-small⇒big⟶∞ (run (x ⊕ y)) i ⟶∞ ¬⇑ = Add.lemma ⟶∞ helper
+  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> x ⟶⋆[ i ] done (nat n)) ->
+           ¬ ¬ loop (x ˢ⁻¹) ⇑[ i ]
+  helper (inj₁ x⟶∞)        = Loop ∘ Seqn₁ <$> small⇒big⟶∞ x i x⟶∞
+  helper (inj₂ (n , x⟶⋆n)) = return (loop-⇑ (n , small⇒big⟶⋆ x⟶⋆n))
+small⇒big⟶∞ (run (x ⊕ y)) i ⟶∞ = helper =<< Add.lemma ⟶∞
hunk ./Semantics/Equivalence.agda 308
-  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]) -> ⊥
-  helper (inj₁ x⟶∞)              = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Add₁)
-  helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Add₂ (n , small⇒big⟶⋆ x⟶⋆n))
-small⇒big⟶∞ (run (x >> y)) i ⟶∞ ¬⇑ = Seqn.lemma ⟶∞ helper
+  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]) ->
+           ¬ ¬ x ˢ⁻¹ ⊕ y ˢ⁻¹ ⇑[ i ]
+  helper (inj₁ x⟶∞)              = Add₁                        <$> small⇒big⟶∞ x i x⟶∞
+  helper (inj₂ (n , x⟶⋆n , y⟶∞)) = Add₂ (n , small⇒big⟶⋆ x⟶⋆n) <$> small⇒big⟶∞ y i y⟶∞
+small⇒big⟶∞ (run (x >> y)) i ⟶∞ = helper =<< Seqn.lemma ⟶∞
hunk ./Semantics/Equivalence.agda 314
-  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]) -> ⊥
-  helper (inj₁ x⟶∞)              = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Seqn₁)
-  helper (inj₂ (n , x⟶⋆n , y⟶∞)) = small⇒big⟶∞ y i y⟶∞ (¬⇑ ∘ Seqn₂ (n , small⇒big⟶⋆ x⟶⋆n))
-small⇒big⟶∞ (run (x catch y)) i ⟶∞ ¬⇑ = Catch.lemma ⟶∞ helper
+  helper : x ⟶∞[ i ] ⊎ ∃ (\n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]) ->
+           ¬ ¬ x ˢ⁻¹ >> y ˢ⁻¹ ⇑[ i ]
+  helper (inj₁ x⟶∞)              = Seqn₁                        <$> small⇒big⟶∞ x i x⟶∞
+  helper (inj₂ (n , x⟶⋆n , y⟶∞)) = Seqn₂ (n , small⇒big⟶⋆ x⟶⋆n) <$> small⇒big⟶∞ y i y⟶∞
+small⇒big⟶∞ (run (x catch y)) i ⟶∞ = helper =<< Catch.lemma ⟶∞
hunk ./Semantics/Equivalence.agda 320
-  helper : x ⟶∞[ i ] ⊎ (x ⟶⋆[ i ] done throw) × y ⟶∞[ B ] -> ⊥
-  helper (inj₁ x⟶∞)          = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Catch₁)
-  helper (inj₂ (x⟶⋆↯ , y⟶∞)) = small⇒big⟶∞ y B y⟶∞ (¬⇑ ∘ Catch₂ (small⇒big⟶⋆ x⟶⋆↯))
-small⇒big⟶∞ (run (block x))   i ⟶∞ ¬⇑ = small⇒big⟶∞ x B (Block.lemma   ⟶∞) (¬⇑ ∘ Block)
-small⇒big⟶∞ (run (unblock x)) i ⟶∞ ¬⇑ = small⇒big⟶∞ x U (Unblock.lemma ⟶∞) (¬⇑ ∘ Unblock)
-small⇒big⟶∞ (done v)          i ⟶∞ ¬⇑ = ⊥-elim (done↛∞ ⟶∞)
+  helper : x ⟶∞[ i ] ⊎ (x ⟶⋆[ i ] done throw) × y ⟶∞[ B ] ->
+           ¬ ¬ x ˢ⁻¹ catch y ˢ⁻¹ ⇑[ i ]
+  helper (inj₁ x⟶∞)          = Catch₁                    <$> small⇒big⟶∞ x i x⟶∞
+  helper (inj₂ (x⟶⋆↯ , y⟶∞)) = Catch₂ (small⇒big⟶⋆ x⟶⋆↯) <$> small⇒big⟶∞ y B y⟶∞
+small⇒big⟶∞ (run (block x))   i ⟶∞ = Block   <$> small⇒big⟶∞ x B (Block.lemma   ⟶∞)
+small⇒big⟶∞ (run (unblock x)) i ⟶∞ = Unblock <$> small⇒big⟶∞ x U (Unblock.lemma ⟶∞)
+small⇒big⟶∞ (done v)          i ⟶∞ = const (done↛∞ ⟶∞)