text:
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
module Data.QuadTree.LensProofs.Valid-LensGo where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws
open import Data.Lens.Proofs.LensPostulates
open import Data.Lens.Proofs.LensComposition
open import Data.QuadTree.LensProofs.Valid-LensLeaf
open import Data.QuadTree.LensProofs.Valid-LensA
open import Data.QuadTree.LensProofs.Valid-LensBCD
open import Axiom.Extensionality.Propositional
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.SafeFunctions
open import Data.QuadTree.Implementation.PublicFunctions
open import Data.QuadTree.Implementation.DataLenses

{-
I spend close to 50 hours on this file, at the time of writing more than the rest of the lens proofs combined.
The file still looks horrible and there is very serious code duplication, but I honestly wish to never look at this file again.

In order to proof this we need some form of Extensionality
Because this is quite a complicated application of Extensionality, I did not proof it from generic Extensionality, but just postulated it seperately.
It is needed because Agda eagerly applies implicit arguments at the start of a function, which I don't want it to do
This can be used to reverse agda doing that
-}

postulate
    FunctorExtensionality :
        {t : Set} {{eqT : Eq t}} -> {deps : Nat} ->
        {la lb : Lens (VQuadrant t {S deps}) t}
        -> ({f : Set -> Set} -> {{ff : Functor f}} -> (la {f} {{ff}} ≡ lb {f} {{ff}}))
        -> (λ {f} ⦃ ff ⦄ → la {f} {{ff}}) ≡ (λ {f} ⦃ ff ⦄ → lb {f} {{ff}})

---- Lens laws for go

ValidLens-go-ViewSet :
    {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> ViewSet (go {t} loc dep {ins})
ValidLens-go-SetView :
    {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> SetView (go {t} loc dep {ins})
ValidLens-go-SetSet :
    {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> SetSet (go {t} loc dep {ins})

ValidLens-go : {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {IsTrue (isInsidePow loc dep)}
    -> ValidLens (VQuadrant t {dep}) t
ValidLens-go {t} {{eqT}} loc dep {ins} = CValidLens (go loc dep {ins}) (ValidLens-go-ViewSet loc dep {ins}) (ValidLens-go-SetView loc dep {ins}) (ValidLens-go-SetSet loc dep {ins})

ValidLens-go-ViewSet loc Z v cvq@(CVQuadrant (Leaf x) {p}) = refl
ValidLens-go-ViewSet {t} (x , y) dep@(S deps) {ins} v cvq@(CVQuadrant qd {p}) =
    ifc y < mid then (λ {{py}} ->
        ifc x < mid then (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> view g (set g v cvq))
                    -- Select only the lensA branch
                    (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifTrue (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-ViewSet (ValidLens-LensA) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) v cvq)
        ) else (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> view g (set g v cvq))
                    -- Select only the lensB branch
                    (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifFalse (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-ViewSet (ValidLens-LensB) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) v cvq)
        )
    ) else (λ {{py}} ->
        ifc x < mid then (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> view g (set g v cvq))
                    -- Select only the lensC branch
                    (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifTrue (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-ViewSet (ValidLens-LensC) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) v cvq)
        ) else (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> view g (set g v cvq))
                    -- Select only the lensD branch
                    (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifFalse (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-ViewSet (ValidLens-LensD) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) v cvq)
        )
    )
    where
        mid = pow 2 deps

ValidLens-go-SetView loc Z cvq@(CVQuadrant (Leaf x) {p}) = refl
ValidLens-go-SetView {t} (x , y) dep@(S deps) {ins} cvq@(CVQuadrant qd {p}) =
    ifc y < mid then (λ {{py}} ->
        ifc x < mid then (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g (view g cvq) cvq)
                    -- Select only the lensA branch
                    (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifTrue (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-SetView (ValidLens-LensA) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) cvq)
        ) else (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g (view g cvq) cvq)
                    -- Select only the lensB branch
                    (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifFalse (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-SetView (ValidLens-LensB) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) cvq)
        )
    ) else (λ {{py}} ->
        ifc x < mid then (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g (view g cvq) cvq)
                    -- Select only the lensC branch
                    (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifTrue (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-SetView (ValidLens-LensC) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) cvq)
        ) else (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g (view g cvq) cvq)
                    -- Select only the lensD branch
                    (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifFalse (x < mid) px))))
                -- Then use the property of composition to proof the law
                (prop-Composition-SetView (ValidLens-LensD) (ValidLens-go (mod x mid , mod y mid) deps {andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})}) cvq)
        )
    )
    where
        mid = pow 2 deps

ValidLens-go-SetSet loc Z v1 v2 cvq@(CVQuadrant (Leaf x) {p}) = refl
ValidLens-go-SetSet {t} (x , y) dep@(S deps) {ins} v1 v2 cvq@(CVQuadrant qd {p}) =
    ifc y < mid then (λ {{py}} ->
        ifc x < mid then (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 (set g v1 cvq))
                    -- Select only the lensA branch
                    (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifTrue (x < mid) px))))
                (trans
                    -- Then use the property of composition to proof the law
                    (prop-Composition-SetSet (ValidLens-LensA) (ValidLens-go (mod x mid , mod y mid) deps {modproof}) v1 v2 cvq)
                    -- Finally, cong back over the law, applying the transformation to go
                    (sym $ cong {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}}}
                        (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 cvq)
                        (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifTrue (x < mid) px)))))
        ) else (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 (set g v1 cvq))
                    -- Select only the lensB branch
                    (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifFalse (x < mid) px))))
                (trans
                    -- Then use the property of composition to proof the law
                    (prop-Composition-SetSet (ValidLens-LensB) (ValidLens-go (mod x mid , mod y mid) deps {modproof}) v1 v2 cvq)
                    -- Finally, cong back over the law, applying the transformation to go
                    (sym $ cong {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}}}
                        (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 cvq)
                        (FunctorExtensionality (trans (ifTrue (y < mid) py) (ifFalse (x < mid) px)))))
        )
    ) else (λ {{py}} ->
        ifc x < mid then (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 (set g v1 cvq))
                    -- Select only the lensC branch
                    (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifTrue (x < mid) px))))
                (trans
                    -- Then use the property of composition to proof the law
                    (prop-Composition-SetSet (ValidLens-LensC) (ValidLens-go (mod x mid , mod y mid) deps {modproof}) v1 v2 cvq)
                    -- Finally, cong back over the law, applying the transformation to go
                    (sym $ cong {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}}}
                        (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 cvq)
                        (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifTrue (x < mid) px)))))
        ) else (λ {{px}} ->
            trans
                (cong
                    -- We need to explicitly provide the x, otherwise agda gets confused
                    {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}} }
                    -- We cong over the law, applying the transformation to go
                    (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 (set g v1 cvq))
                    -- Select only the lensD branch
                    (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifFalse (x < mid) px))))
                (trans
                    -- Then use the property of composition to proof the law
                    (prop-Composition-SetSet (ValidLens-LensD) (ValidLens-go (mod x mid , mod y mid) deps {modproof}) v1 v2 cvq)
                    -- Finally, cong back over the law, applying the transformation to go
                    (sym $ cong {x = λ {f} ⦃ ff ⦄ → go (x , y) (S deps) {ins} {f} {{ff}}}
                        (λ (g : Lens (VQuadrant t {dep}) t) -> set g v2 cvq)
                        (FunctorExtensionality (trans (ifFalse (y < mid) py) (ifFalse (x < mid) px)))))
        )
    )

    where
        mid = pow 2 deps
        modproof = andCombine (modLt x mid {pow_not_zero_cv deps}) (modLt y mid {pow_not_zero_cv deps})

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
-- open import Data.List
-- open import Data.Fin

open import Agda.Builtin.Nat public
  using (Nat; zero; suc)

open import Agda.Builtin.List public
  using (List; []; _∷_)

data Fin : Nat → Set where
  fzero : {n : Nat} → Fin (suc n)
  fsuc  : {n : Nat} (i : Fin n) → Fin (suc n)

foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
foldr c n []       = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

length : ∀ {a} {A : Set a} → List A → Nat
length = foldr (λ _ → suc) 0

lookup : ∀ {a} {A : Set a} (xs : List A) → Fin (length xs) → A
lookup [] ()
lookup (x ∷ xs) fzero = x
lookup (x ∷ xs) (fsuc i) = lookup xs i

data ListD {I : Set} (T : I → Set) : List I → Set where
  nilD  : ListD T []
  consD : ∀ {x xs} → (elem : T x) → (rest : ListD T xs) → ListD T (x ∷ xs)

lookupD : {I : Set} {T : I → Set} {xs : List I} → ListD T xs → (at : Fin (length xs)) → {!lookup ? ?!}
lookupD xs at = {!!}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- A delay monad with the possibility of crashing
------------------------------------------------------------------------

module Lambda.Delay-crash where

import Equality.Propositional as E
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

import Conat E.equality-with-J as Conat
open import Function-universe E.equality-with-J hiding (_∘_)
open import Maybe E.equality-with-J as Maybe hiding (raw-monad)
open import Monad E.equality-with-J as M
  using (Raw-monad; _>>=_)

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Bisimilarity.Kind
import Delay-monad.Monad as DM
import Delay-monad.Parallel as DP
import Delay-monad.Sequential as DS
open import Delay-monad.Termination

private

  variable
    A B C     : Type
    i         : Size
    f g k x y : A

------------------------------------------------------------------------
-- Types and operations

-- The monad.

Delay-crash : Type → Size → Type
Delay-crash A i = Delay (Maybe A) i

-- A raw-monad instance. (This definition is turned into an actual
-- instance at the end of this module, to avoid problems with instance
-- resolution.)

private

  raw-monad′ : Raw-monad (λ A → Delay-crash A i)
  raw-monad′ {i = i} =
    _⇔_.to (M.⇔→raw⇔raw {F = MaybeT (λ A → Delay A i)}
              (λ _ → record { to = run; from = wrap }))
      it

  module DC {i} = Raw-monad (raw-monad′ {i = i})

-- A crashing computation.

pattern crash = now nothing

private

  -- A computation that terminates now.

  pattern return x = now (just x)

-- Sequential composition of computations.
--
-- Note that if the first argument fails to terminate, and the other
-- one crashes, then the computation fails to terminate. However, if
-- the first argument crashes, then the computation always crashes.

infixl 6 _⊛ˢ_

_⊛ˢ_ : Delay-crash (A → B) i → Delay-crash A i → Delay-crash B i
f ⊛ˢ x = f DC.>>= λ f → x DC.>>= λ x → DC.return (f x)

-- Parallel composition of computations.
--
-- Note that if the first argument fails to terminate, and the other
-- one crashes, then the computation fails to terminate. However, if
-- the first argument crashes, then the computation always crashes.

infixl 6 _⊛ᵖ_

_⊛ᵖ_ : Delay-crash (A → B) i → Delay-crash A i → Delay-crash B i
crash    ⊛ᵖ _            = crash
return f ⊛ᵖ return x     = return (f x)
return f ⊛ᵖ crash        = crash
return f ⊛ᵖ later x      = later λ { .force → return f ⊛ᵖ x .force }
later f  ⊛ᵖ later x      = later λ { .force → f .force ⊛ᵖ x .force }
later f  ⊛ᵖ x            = later λ { .force → f .force ⊛ᵖ x }

------------------------------------------------------------------------
-- Some properties

-- Bind preserves strong and weak bisimilarity and the expansion
-- relation.

infixl 5 _>>=-cong_

_>>=-cong_ :
  [ i ] x ⟨ k ⟩ y →
  (∀ z → [ i ] f z ⟨ k ⟩ g z) →
  [ i ] x DC.>>= f ⟨ k ⟩ y DC.>>= g
p >>=-cong q = p DM.>>=-cong [ (λ _ → run fail ∎) , q ]

-- Sequential composition preserves strong and weak bisimilarity and
-- the expansion relation.

infixl 6 _⊛ˢ-cong_

_⊛ˢ-cong_ :
  [ i ] f ⟨ k ⟩ g →
  [ i ] x ⟨ k ⟩ y →
  [ i ] f ⊛ˢ x ⟨ k ⟩ g ⊛ˢ y
p ⊛ˢ-cong q = p >>=-cong λ _ → q >>=-cong λ _ → now

-- Parallel composition preserves strong and weak bisimilarity and the
-- expansion relation.

infixl 6 _⊛ᵖ-cong_

_⊛ᵖ-cong_ :
  [ i ] f ⟨ k ⟩ g →
  [ i ] x ⟨ k ⟩ y →
  [ i ] f ⊛ᵖ x ⟨ k ⟩ g ⊛ᵖ y
_⊛ᵖ-cong_ = λ p q → ⊛ᵖ-cong-helper _ _ p _ _ q
  where
  crash-lemma :
    [ i ] f ⟨ other k ⟩ crash → ∀ x → [ i ] f ⊛ᵖ x ⟨ other k ⟩ crash
  crash-lemma now        x         = now
  crash-lemma (laterˡ p) (now x)   = laterˡ (crash-lemma p _)
  crash-lemma (laterˡ p) (later x) = laterˡ (crash-lemma p _)

  ⊛ᵖ-cong-helper :
    (f g : Delay-crash (A → B) ∞) → [ i ] f ⟨ k ⟩ g →
    (x y : Delay-crash A ∞) →       [ i ] x ⟨ k ⟩ y →
    [ i ] f ⊛ᵖ x ⟨ k ⟩ g ⊛ᵖ y
  ⊛ᵖ-cong-helper crash crash now = λ _ _ _ → now

  ⊛ᵖ-cong-helper (return f) .(return f) now = λ where
    (later x)  (later y)   q          → later λ { .force → now ⊛ᵖ-cong later⁻¹ q }
    crash      crash       now        → now
    (return x) .(return x) now        → now
    _          _           (laterˡ q) → laterˡ (now ⊛ᵖ-cong q)
    _          _           (laterʳ q) → laterʳ (now ⊛ᵖ-cong q)

  ⊛ᵖ-cong-helper (later f) (later g) p = λ where
    crash      crash       now        → later λ { .force → later⁻¹ p ⊛ᵖ-cong now }
    (return x) .(return x) now        → later λ { .force → later⁻¹ p ⊛ᵖ-cong now }
    (later x)  (later y)   q          → later λ { .force → later⁻¹ p ⊛ᵖ-cong later⁻¹ q }
    _          crash       (laterˡ q) → later λ { .force → later⁻¹ p ⊛ᵖ-cong q }
    _          (return y)  (laterˡ q) → later λ { .force → later⁻¹ p ⊛ᵖ-cong q }
    crash      _           (laterʳ q) → later λ { .force → later⁻¹ p ⊛ᵖ-cong q }
    (return x) _           (laterʳ q) → later λ { .force → later⁻¹ p ⊛ᵖ-cong q }

  ⊛ᵖ-cong-helper _ (return g) (laterˡ p) = λ where
    crash      crash       now        → laterˡ (p ⊛ᵖ-cong now)
    (return x) .(return x) now        → laterˡ (p ⊛ᵖ-cong now)
    (later x)  (later y)   q          → later λ { .force → p ⊛ᵖ-cong later⁻¹ q }
    _          crash       (laterˡ q) → laterˡ (p ⊛ᵖ-cong q)
    _          (return y)  (laterˡ q) → laterˡ (p ⊛ᵖ-cong q)
    crash      _           (laterʳ q) → later λ { .force → p ⊛ᵖ-cong q }
    (return x) _           (laterʳ q) → later λ { .force → p ⊛ᵖ-cong q }

  ⊛ᵖ-cong-helper (return f) _ (laterʳ p) = λ where
    crash      crash       now        → laterʳ (p ⊛ᵖ-cong now)
    (return x) .(return x) now        → laterʳ (p ⊛ᵖ-cong now)
    (later x)  (later y)   q          → later λ { .force → p ⊛ᵖ-cong later⁻¹ q }
    _          crash       (laterˡ q) → later λ { .force → p ⊛ᵖ-cong q }
    _          (return y)  (laterˡ q) → later λ { .force → p ⊛ᵖ-cong q }
    crash      _           (laterʳ q) → laterʳ (p ⊛ᵖ-cong q)
    (return x) _           (laterʳ q) → laterʳ (p ⊛ᵖ-cong q)

  ⊛ᵖ-cong-helper _ crash p@(laterˡ _) = λ _ _ _ → crash-lemma p _

  ⊛ᵖ-cong-helper crash _ p@(laterʳ _) =
    λ _ _ _ → symmetric (crash-lemma (symmetric p) _)

-- The monad laws.

left-identity :
  ∀ x (f : A → Delay-crash B ∞) →
  [ ∞ ] DC.return x DC.>>= f ∼ f x
left-identity x f =
  f x  ∎

right-identity :
  (x : Delay-crash A ∞) →
  [ ∞ ] x DC.>>= DC.return ∼ x
right-identity x =
  x DC.>>= DC.return        ∼⟨⟩
  x >>= maybe return crash  ∼⟨ (x ∎) DM.>>=-cong [ (λ _ → run fail ∎) , (λ x → run (M.return x) ∎) ] ⟩
  x >>= M.return            ∼⟨ DM.right-identity′ _ ⟩
  x                         ∎

associativity :
  (x : Delay-crash A ∞)
  (f : A → Delay-crash B ∞) (g : B → Delay-crash C ∞) →
  x DC.>>= (λ x → f x DC.>>= g) ∼ x DC.>>= f DC.>>= g
associativity x f g =
  x DC.>>= (λ x → f x DC.>>= g)                      ∼⟨⟩
  x >>= maybe (λ x → f x DC.>>= g) crash             ∼⟨ (x ∎) DM.>>=-cong [ (λ _ → run fail ∎) , (λ x → f x DC.>>= g ∎) ] ⟩
  x >>= (λ x → maybe f crash x >>= maybe g crash)    ∼⟨ DM.associativity′ x _ _ ⟩
  x >>= maybe f crash >>= maybe g crash              ∼⟨⟩
  x DC.>>= f DC.>>= g                                ∎

-- Use of _⟨$⟩_ does not affect the number of steps in the
-- computation.

steps-⟨$⟩ : Conat.[ i ] steps (f DC.⟨$⟩ x) ∼ steps x
steps-⟨$⟩ {f = f} {x = x} =
  steps (f DC.⟨$⟩ x)                                 Conat.≡⟨⟩∼
  steps (x DC.>>= DC.return ∘ f)                     Conat.≡⟨⟩∼
  steps (x >>= maybe (return ∘ f) crash)             Conat.∼⟨ steps-cong ((x ∎) DM.>>=-cong [ (λ _ → run fail ∎)
                                                                                , (λ x → return (f x) ∎)
                                                                                ]) ⟩
  steps (x >>= M.return ∘ maybe (just ∘ f) nothing)  Conat.∼⟨ DM.steps-⟨$⟩ _ ⟩
  steps x                                            Conat.∎∼

-- Sequential composition is an expansion of parallel composition.

⊛ˢ≳⊛ᵖ : [ i ] f ⊛ˢ x ≳ f ⊛ᵖ x
⊛ˢ≳⊛ᵖ {f = return f} {x = return x} = now
⊛ˢ≳⊛ᵖ {f = return f} {x = crash}    = now
⊛ˢ≳⊛ᵖ {f = return f} {x = later x}  = later λ { .force → ⊛ˢ≳⊛ᵖ }
⊛ˢ≳⊛ᵖ {f = crash}                   = now
⊛ˢ≳⊛ᵖ {f = later f}  {x = now x}    = later λ { .force → ⊛ˢ≳⊛ᵖ }
⊛ˢ≳⊛ᵖ {f = later f}  {x = later x}  = later λ { .force →
  (f .force DC.>>= λ f → later x DC.>>= λ x → DC.return (f x))  ≳⟨ ((f .force ∎) >>=-cong λ _ → laterˡ (_ ∎)) ⟩
  f .force ⊛ˢ x .force                                          ≳⟨ ⊛ˢ≳⊛ᵖ ⟩∼
  f .force ⊛ᵖ x .force                                          ∎ }

-- The computation crash is a left zero for _⊛ˢ_ and _⊛ᵖ_.

crash-⊛ˢ : [ i ] crash ⊛ˢ x ∼ (crash ⦂ Delay-crash B ∞)
crash-⊛ˢ = reflexive _

crash-⊛ᵖ : [ i ] crash ⊛ᵖ x ∼ (crash ⦂ Delay-crash B ∞)
crash-⊛ᵖ = reflexive _

-- The computation never is a left zero for _⊛ˢ_ and _⊛ᵖ_.

never-⊛ˢ :
  (x : Delay-crash A ∞) →
  [ i ] never ⊛ˢ x ∼ (never ⦂ Delay-crash B ∞)
never-⊛ˢ x = later λ { .force → never-⊛ˢ x }

never-⊛ᵖ :
  (x : Delay-crash A ∞) →
  [ i ] never ⊛ᵖ x ∼ (never ⦂ Delay-crash B ∞)
never-⊛ᵖ (now x)   = later λ { .force → never-⊛ᵖ (now x) }
never-⊛ᵖ (later x) = later λ { .force → never-⊛ᵖ _ }

-- The computation never is a right zero for _⊛ˢ_ and _⊛ᵖ_ if the left
-- computation does not crash.

⊛ˢ-never : ¬ f ≈ crash → [ i ] f ⊛ˢ never ∼ never
⊛ˢ-never {f = return _} p = later λ { .force → ⊛ˢ-never p }
⊛ˢ-never {f = later _}  p = later λ { .force → ⊛ˢ-never (p ∘ laterˡ) }
⊛ˢ-never {f = crash}    p = ⊥-elim (p (_ ∎))

⊛ᵖ-never : ¬ f ≈ crash → [ i ] f ⊛ᵖ never ∼ never
⊛ᵖ-never {f = return _} p = later λ { .force → ⊛ᵖ-never p }
⊛ᵖ-never {f = later _}  p = later λ { .force → ⊛ᵖ-never (p ∘ laterˡ) }
⊛ᵖ-never {f = crash}    p = ⊥-elim (p (_ ∎))

-- The computation crash is a right zero for _⊛ˢ_ and _⊛ᵖ_ (up to
-- expansion) if the left computation terminates.

⊛ˢ-crash : f ⇓ g → [ i ] f ⊛ˢ crash ≳ crash
⊛ˢ-crash (now {x = nothing}) = now
⊛ˢ-crash (now {x = just _})  = now
⊛ˢ-crash (laterʳ p)          = laterˡ (⊛ˢ-crash p)

⊛ᵖ-crash : f ⇓ g → [ i ] f ⊛ᵖ crash ≳ crash
⊛ᵖ-crash (now {x = nothing}) = now
⊛ᵖ-crash (now {x = just _})  = now
⊛ᵖ-crash (laterʳ p)          = laterˡ (⊛ᵖ-crash p)

-- The _⊛ᵖ_ and _⊛ˢ_ operators are not (kind of) commutative.

¬-⊛ᵖ-comm :
  ¬ (∀ {f : Delay-crash (A → B) ∞} {x} →
     f ⊛ᵖ x ≈ flip _$_ DC.⟨$⟩ x ⊛ᵖ f)
¬-⊛ᵖ-comm {A = A} {B = B} =
  (∀ {f : Delay-crash (A → B) ∞} {x} → f ⊛ᵖ x ≈ flip _$_ DC.⟨$⟩ x ⊛ᵖ f)  ↝⟨ (λ hyp → hyp {f = crash} {x = never}) ⟩
  crash ≈ flip _$_ DC.⟨$⟩ never ⊛ᵖ crash                                 ↝⟨ flip transitive-∞∼ʳ lemma ⟩
  crash ≈ never                                                          ↝⟨ now≉never ⟩□
  ⊥                                                                      □
  where
  lemma : [ i ] flip _$_ DC.⟨$⟩ never ⊛ᵖ crash ∼ never
  lemma = later λ { .force → lemma }

¬-⊛ˢ-comm :
  ¬ (∀ {f : Delay-crash (A → B) ∞} {x} →
     f ⊛ˢ x ≈ flip _$_ DC.⟨$⟩ x ⊛ˢ f)
¬-⊛ˢ-comm {A = A} {B = B} =
  (∀ {f : Delay-crash (A → B) ∞} {x} → f ⊛ˢ x ≈ flip _$_ DC.⟨$⟩ x ⊛ˢ f)  ↝⟨ (λ hyp {f x} →

      f ⊛ᵖ x                                                                   ≈⟨ symmetric (≳→ ⊛ˢ≳⊛ᵖ) ⟩
      f ⊛ˢ x                                                                   ≈⟨ hyp {f = f} {x = x} ⟩
      flip _$_ DC.⟨$⟩ x ⊛ˢ f                                                   ≳⟨ ⊛ˢ≳⊛ᵖ ⟩
      flip _$_ DC.⟨$⟩ x ⊛ᵖ f                                                   ∎) ⟩

  (∀ {f : Delay-crash (A → B) ∞} {x} → f ⊛ᵖ x ≈ flip _$_ DC.⟨$⟩ x ⊛ᵖ f)  ↝⟨ ¬-⊛ᵖ-comm ⟩□
  ⊥                                                                      □

------------------------------------------------------------------------
-- The instance declaration

-- A raw-monad instance.

instance

  raw-monad : Raw-monad (λ A → Delay-crash A i)
  raw-monad = raw-monad′

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module test where
open import Data.Sum.Base
postulate
    X : Set
    a : X
    b : X
    p : X → X → Set
    φ : (x : X) → (p x a ⊎ p x b)

example : (x : X) →


text:
{-# OPTIONS --cubical --safe --guardedness #-}

module Data.PolyP.Currying where

open import Prelude hiding (_⟨_⟩_)
open import Data.Vec.Iterated

open import Data.PolyP.Universe

Curriedⁿ : ℕ → Type₁
Curriedⁿ zero    = Type
Curriedⁿ (suc n) = Type → Curriedⁿ n

_~_ : ∀ {n} → (Params n → Type) → Curriedⁿ n
_~_ {n = zero}  f = f []
_~_ {n = suc n} f A = _~_ {n = n} (f ∘ (A ∷_))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --universe-polymorphism #-}

open import FRP.JS.Bool using ( Bool ; true ; false ; if_then_else_ ; not ; _∧_ )

module FRP.JS.True where

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

contradiction : ∀ {α} {A : Set α} → ⊥ → A
contradiction ()

True : Bool → Set
True true = ⊤
True false = ⊥

False : Bool → Set
False b = True b → ⊥

∧-intro : ∀ {a b} → True a → True b → True (a ∧ b)
∧-intro {false}         () b
∧-intro {true}  {false} tt ()
∧-intro {true}  {true}  tt tt = tt

∧-elim₁ : ∀ {a b} → True (a ∧ b) → True a
∧-elim₁ {false} ()
∧-elim₁ {true}  b  = tt

∧-elim₂ : ∀ {a b} → True (a ∧ b) → True b
∧-elim₂ {false} ()
∧-elim₂ {true}  b  = b

data Dec (b : Bool) : Set where
  yes : True b → Dec b
  no  : False b → Dec b

{-# COMPILED_JS Dec function(x,v) {
  if (x) { return v.yes(null); } else { return v.no(null); }
} #-}
{-# COMPILED_JS yes true #-}
{-# COMPILED_JS no false #-}

dec : ∀ b → Dec b
dec true  = yes tt
dec false = no contradiction

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Size where

open import Agda.Builtin.Size public
  renaming ( SizeU to SizeUniv ) --  sort SizeUniv
  using    ( Size                --  Size   : SizeUniv
           ; Size<_              --  Size<_ : Size → SizeUniv
           ; ↑_                  --  ↑_     : Size → Size
           ; ∞ )                 --  ∞      : Size


text:
{-# OPTIONS --without-K --exact-split --rewriting #-}

open import lib.Basics
open import lib.types.Truncation
open import lib.Function2
open import lib.NType2

open import Graphs.Definition
open import Coequalizers.Definition

open import Util.Misc

module Coequalizers.Misc where

module _ {i j : ULevel} {E : Type i} {V : Type j} ⦃ gph : Graph E V ⦄ where
  inh-coeq-to-vertex : ∥ V / E ∥ → ∥ V ∥
  inh-coeq-to-vertex = Trunc-rec (Coeq-rec [_] (λ _ → prop-has-all-paths _ _))

  quotient-map-is-surj : is-surj (c[_] :> (V → V / E))
  quotient-map-is-surj = Coeq-elim (λ v → ∥ hfiber c[_] v ∥) (λ v → [ v , idp ]) λ _ → prop-has-all-paths-↓

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
-- Andreas, 2016-10-09, re issue #2223

-- The front matter or module telescope of the top-level module
-- may generate level constraints that live in no module!

{-# OPTIONS -v tc.constr.add:45 #-} -- KEEP!

open import Common.Level
open import Issue2223.Setoids -- import necessary!

module _ (S : Setoid lzero lzero) (a : Setoid.Carrier S) (_ : a ⟨ Setoid._≈_ S ⟩ a) where

-- PROBLEM WAS: internal error in debug printing.
-- Should work now.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module objectsInAgdaUnsized where

open import Data.Product
open import interactiveProgramsAgdaUnsized hiding (main)
open import NativeIO
open import Data.String.Base

record Interface  :  Set₁ where
  field  Method   :  Set
         Result   :  (m : Method) → Set

open Interface public

record Object (I : Interface) : Set where
  coinductive
  field objectMethod : (m : Method I) → Result I m × Object I

open Object public

record IOObject (Iᵢₒ : IOInterface) (I : Interface) : Set where
  coinductive
  field method : (m : Method I) → IO Iᵢₒ (Result I m × IOObject Iᵢₒ I)

open IOObject public

data CellMethod A : Set where
    get  :  CellMethod A
    put  :  A → CellMethod A

CellResult             :  ∀{A} → CellMethod A → Set
CellResult   {A} get   =  A
CellResult   (put _)   =  Unit

cellI                  :  (A : Set) → Interface
Method    (cellI A)    =  CellMethod A
Result    (cellI A) m  =  CellResult m

{- A cell as an Object -}

Cell : Set → Set
Cell A = Object (cellI A)

cell : {A : Set} → A → Cell A
objectMethod (cell a) get       = a    , cell a
objectMethod (cell a) (put a')  = unit , cell a'

{- A cell as an IOObject -}

CellC : Set
CellC = IOObject ConsoleInterface (cellI String)

simpleCell : (s : String) → CellC
force (method (simpleCell s) get) =
  do' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  delay (return' (s , simpleCell s))
force (method (simpleCell s) (put x)) =
  do' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  delay (return' (_ , simpleCell x))

{-# TERMINATING #-}

program : CellC → IOConsole Unit
force (program c₁) =
  do' getLine          λ s →
  method c₁ (put s)    >>= λ{ (_  , c₂) →
  method c₂ get        >>= λ{ (s' , c₃) →
  do (putStrLn s')     λ _ →
  (program c₃)}}

main : NativeIO Unit
main = translateIOConsole (program (simpleCell "Start"))

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-
This is a rather literal translation of Martin Hötzel-Escardó's structure identity principle into cubical Agda. See
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sns

All the needed preliminary results from the lecture notes are stated and proven in this file.
It would be interesting to compare the proves with the one in Cubical.Foundations.SIP
-}

{-# OPTIONS --cubical --safe #-}
module Cubical.Experiments.EscardoSIP where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Foundations.HAEquiv
open import Cubical.Data.Sigma.Properties

private
 variable
  ℓ ℓ' ℓ'' : Level

-- We prove several useful equalities and equivalences between Σ-types all the proofs are taken from
-- Martin Hötzel-Escardó's lecture notes.

-- The next result is just a reformulation of pathSigma≡sigmaPath from Sigma.Properties.

Σ-≡-≃ : {X : Type ℓ} {A : X → Type ℓ'}
       → (σ τ : Σ X A) → ((σ ≡ τ) ≃ (Σ[ p ∈ (σ .fst) ≡ (τ .fst) ] (subst A p (σ .snd) ≡ (τ .snd))))
Σ-≡-≃ {A = A} σ τ = pathToEquiv (pathSigma≡sigmaPath σ τ)

-- This cubical proof is much shorter than in HoTT but requires that A, B live in the same universe.
Σ-cong : {X : Type ℓ} {A B : X → Type ℓ'} →
         ((x : X) → (A x ≡ B x)) → (Σ X A ≡ Σ X B)
Σ-cong {X = X} p i = Σ[ x ∈ X ] (p x i)

-- Two lemmas for the more general formulation using equivalences
NatΣ : {X : Type ℓ} {A : X → Type ℓ'} {B : X → Type ℓ''}
      → ((x : X) → (A x) → (B x)) → (Σ X A) → (Σ X B)
NatΣ τ (x , a) = (x , τ x a)

Σ-to-PathP : {X : Type ℓ} {A : X → Type ℓ'} {x : X} {a b : A x}
          → (a ≡ b) → PathP (λ i → Σ X A) (x , a) (x , b)
Σ-to-PathP {x = x} p i = (x , p i)

Σ-cong-≃ :  {X : Type ℓ} {A : X → Type ℓ'} {B : X → Type ℓ''} →
         ((x : X) → (A x ≃ B x)) → (Σ X A ≃ Σ X B)
Σ-cong-≃ {X = X} {A = A} {B = B} φ = isoToEquiv (iso (NatΣ f) (NatΣ g) NatΣ-ε NatΣ-η)
 where
  f : (x : X) → (A x) → (B x)
  f x = equivFun (φ x)

  g : (x : X) → (B x) → (A x)
  g x = equivFun (invEquiv (φ x))

  η : (x : X) → (a : A x) → (g x) ((f x) a) ≡ a
  η x = retEq (invEquiv (φ x))

  ε : (x : X) → (b : B x) → f x (g x b) ≡ b
  ε x = secEq  (invEquiv (φ x))

  NatΣ-η : (w : Σ X A) → NatΣ g (NatΣ f w) ≡ w
  NatΣ-η (x , a)  = (x , g x (f x a)) ≡⟨ Σ-to-PathP (η x a)  ⟩
                    (x , a)           ∎

  NatΣ-ε : (u : Σ X B) → NatΣ f (NatΣ g u) ≡ u
  NatΣ-ε (x , b) = (x , f x (g x b)) ≡⟨ Σ-to-PathP (ε x b) ⟩
                   (x , b)           ∎

-- The next result is stated a bit awkwardly but is rather straightforward to prove.
Σ-change-of-variable-Iso :  {X : Type ℓ} {Y : Type ℓ'} {A : Y → Type ℓ''} (f : X → Y)
                           → (isHAEquiv f) → (Iso (Σ X (A ∘ f)) (Σ Y A))
Σ-change-of-variable-Iso {ℓ = ℓ} {ℓ' = ℓ'} {X = X} {Y = Y} {A = A} f isHAEquivf = iso φ ψ φψ ψφ
  where
   g : Y → X
   g = isHAEquiv.g isHAEquivf
   ε : (x : X) → (g (f x)) ≡ x
   ε = isHAEquiv.sec isHAEquivf
   η : (y : Y) → f (g y) ≡ y
   η = isHAEquiv.ret isHAEquivf
   τ :  (x : X) → cong f (ε x) ≡ η (f x)
   τ = isHAEquiv.com isHAEquivf

   φ : (Σ X (A ∘ f)) → (Σ Y A)
   φ (x , a) = (f x , a)

   ψ : (Σ Y A) → (Σ X (A ∘ f))
   ψ (y , a) = (g y , subst A (sym (η y)) a)

   φψ : (z : (Σ Y A)) → φ (ψ z) ≡ z
   φψ (y , a) = sigmaPath→pathSigma (φ (ψ (y , a))) (y , a)
                                    (η y ,  transportTransport⁻ (λ i → A (η y i)) a)
     -- last term proves transp (λ i → A (η y i)) i0 (transp (λ i → A (η y (~ i))) i0 a) ≡ a

   ψφ : (z : (Σ X (A ∘ f))) → ψ (φ z) ≡ z
   ψφ (x , a) = sigmaPath→pathSigma (ψ (φ (x , a))) (x , a) (ε x , q)
     where
      b : A (f (g (f x)))
      b = (transp (λ i → A (η (f x) (~ i))) i0 a)

      q : transp (λ i → A (f (ε x i))) i0 (transp (λ i → A (η (f x) (~ i))) i0 a) ≡ a
      q =  transp (λ i → A (f (ε x i))) i0 b  ≡⟨ S ⟩
           transp (λ i → A (η (f x) i)) i0 b  ≡⟨ transportTransport⁻ (λ i → A (η (f x) i)) a ⟩
           a                                  ∎
       where
        S : (transp (λ i → A (f (ε x i))) i0 b)  ≡ (transp (λ i → A (η (f x) i)) i0 b)
        S = subst (λ p → (transp (λ i → A (f (ε x i))) i0 b)  ≡ (transp (λ i → A (p i)) i0 b))
                 (τ x) refl

-- Using the result above we can prove the following quite useful result.
Σ-change-of-variable-≃ : {X : Type ℓ} {Y : Type ℓ'} {A : Y → Type ℓ''} (f : X → Y)
                      → (isEquiv f) → ((Σ X (A ∘ f)) ≃ (Σ Y A))
Σ-change-of-variable-≃ f isEquivf =
                      isoToEquiv (Σ-change-of-variable-Iso f (equiv→HAEquiv (f , isEquivf) .snd))

Σ-assoc-Iso : (X : Type ℓ) (A : X → Type ℓ') (P : Σ X A → Type ℓ'')
         → (Iso (Σ (Σ X A) P) (Σ[ x ∈ X ] (Σ[ a ∈ A x ] P (x , a))))
Σ-assoc-Iso X A P = iso f g ε η
   where
    f : (Σ (Σ X A) P) → (Σ[ x ∈ X ] (Σ[ a ∈ A x ] P (x , a)))
    f ((x , a) , p) = (x , (a , p))
    g : (Σ[ x ∈ X ] (Σ[ a ∈ A x ] P (x , a))) →  (Σ (Σ X A) P)
    g (x , (a , p)) = ((x , a) , p)
    ε : section f g
    ε n = refl
    η : retract f g
    η m = refl

Σ-assoc-≃ : (X : Type ℓ) (A : X → Type ℓ') (P : Σ X A → Type ℓ'')
         → (Σ (Σ X A) P) ≃ (Σ[ x ∈ X ] (Σ[ a ∈ A x ] P (x , a)))
Σ-assoc-≃ X A P = isoToEquiv (Σ-assoc-Iso X A P)

-- A structure is a type-family S : Type ℓ → Type ℓ', i.e. for X : Type ℓ and s : S X, the pair (X , s)
-- means that X is equipped with a S-structure, which is witnessed by s.
-- An S-structure should have a notion of S-homomorphism, or rather S-isomorphism.
-- This will be implemented by a function ι
-- that gives us for any two types with S-structure (X , s) and (Y , t) a family:
--    ι (X , s) (Y , t) : (X ≃ Y) → Type ℓ''
-- Note that for any equivalence (f , e) : X ≃ Y the type  ι (X , s) (Y , t) (f , e) need not to be
-- a proposition. Indeed this type should correspond to the ways s and t can be identified
-- as S-structures. This we call a standard notion of structure.

SNS : (S : Type ℓ → Type ℓ')
     → ((A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ'')
     → Type (ℓ-max (ℓ-max(ℓ-suc ℓ) ℓ') ℓ'')
SNS  {ℓ = ℓ} S ι = ∀ {X : (Type ℓ)} (s t : S X) → ((s ≡ t) ≃ ι (X , s) (X , t) (idEquiv X))

-- Escardo's ρ can actually be  defined from this:
ρ :  {S : Type ℓ → Type ℓ'}
    → {ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ''}
    → (SNS S ι)
    → (A : Σ[ X ∈ (Type ℓ) ] (S X)) → (ι A A (idEquiv (A .fst)))
ρ θ A = equivFun (θ (A .snd) (A .snd)) refl

-- We introduce the notation a bit differently:
_≃[_]_ : {S : Type ℓ → Type ℓ'} → (Σ[ X ∈ (Type ℓ) ] (S X))
                           → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ'')
                           → (Σ[ X ∈ (Type ℓ) ] (S X))
                           → (Type (ℓ-max ℓ ℓ''))
A ≃[ ι ] B = Σ[ f ∈ ((A .fst) ≃ (B. fst)) ] (ι A B f)

Id→homEq : (S : Type ℓ → Type ℓ')
          → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ'')
          → (ρ : (A : Σ[ X ∈ (Type ℓ) ] (S X)) → ι A A (idEquiv (A .fst)))
          → (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → A ≡ B → (A ≃[ ι ] B)
Id→homEq S ι ρ A B p = J (λ y x → A ≃[ ι ] y) (idEquiv (A .fst) , ρ A) p

-- Use a PathP version of Escardó's homomorphism-lemma
hom-lemma-dep : (S : Type ℓ → Type ℓ')
               → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ'')
               → (θ : SNS S ι)
               → (A B : Σ[ X ∈ (Type ℓ) ] (S X))
               → (p : (A .fst) ≡ (B. fst))
               → (PathP (λ i → S (p i)) (A .snd) (B .snd)) ≃ (ι A B (pathToEquiv p))
hom-lemma-dep S ι θ A B p = (J P (λ s → γ s) p) (B .snd)
     where
      P = (λ y x → (s : S y) → PathP (λ i → S (x i)) (A .snd) s ≃ ι A (y , s) (pathToEquiv x))

      γ : (s : S (A .fst)) → ((A .snd) ≡ s) ≃ ι A ((A .fst) , s) (pathToEquiv refl)
      γ s = subst (λ f → ((A .snd) ≡ s) ≃ ι A ((A .fst) , s) f)  (sym pathToEquivRefl) (θ (A. snd) s)

-- Define the inverse of Id→homEq directly.
ua-lemma : (A B : Type ℓ) (e : A ≃ B) → (pathToEquiv (ua e)) ≡ e
ua-lemma A B e = EquivJ (λ b a f →  (pathToEquiv (ua f)) ≡ f)
                       (λ x → subst (λ r → pathToEquiv r ≡ idEquiv x) (sym uaIdEquiv) pathToEquivRefl)
                        B A e

homEq→Id : (S : Type ℓ → Type ℓ')
          → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ'')
          → (θ : SNS S ι)
          → (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → (A ≃[ ι ] B) → A ≡ B
homEq→Id S ι θ A B (f , φ) = ΣPathP (p , q)
        where
         p = ua f

         ψ : ι A B (pathToEquiv p)
         ψ = subst (λ g → ι A B g) (sym (ua-lemma (A .fst) (B. fst) f)) φ

         q : PathP (λ i → S (p i)) (A .snd) (B .snd)
         q = equivFun (invEquiv (hom-lemma-dep S ι θ A B p)) ψ

-- Proof of the SIP:
SIP : (S : Type ℓ → Type ℓ')
     → (ι : (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A .fst) ≃ (B .fst)) → Type ℓ'')
     → (θ : SNS S ι)
     → (A B : Σ[ X ∈ (Type ℓ) ] (S X)) → ((A ≡ B) ≃ (A ≃[ ι ] B))
SIP S ι θ A B =
            (A ≡ B)                                                                 ≃⟨ i ⟩
            (Σ[ p ∈ (A .fst) ≡ (B. fst) ] PathP (λ i → S (p i)) (A .snd) (B .snd))  ≃⟨ ii ⟩
            (Σ[ p ∈ (A .fst) ≡ (B. fst) ] (ι A B (pathToEquiv p)))                  ≃⟨ iii ⟩
            (A ≃[ ι ] B)                                                            ■
    where
     i = invEquiv Σ≡
     ii = Σ-cong-≃ (hom-lemma-dep S ι θ A B)
     iii = Σ-change-of-variable-≃ pathToEquiv (equivIsEquiv univalence)

-- A simple example: pointed types
pointed-structure : Type ℓ → Type ℓ
pointed-structure X = X

Pointed-Type : Type (ℓ-suc ℓ)
Pointed-Type {ℓ = ℓ} = Σ (Type ℓ) pointed-structure

pointed-ι : (A B : Pointed-Type) → (A .fst) ≃ (B. fst) → Type ℓ
pointed-ι (X , x) (Y , y) f = (equivFun f) x ≡ y

pointed-is-sns : SNS {ℓ = ℓ} pointed-structure pointed-ι
pointed-is-sns s t = idEquiv (s ≡ t)

pointed-type-sip : (X Y : Type ℓ) (x : X) (y : Y)
                  → (Σ[ f ∈ X ≃ Y ] (f .fst) x ≡ y) ≃ ((X , x) ≡ (Y , y))
pointed-type-sip X Y x y = invEquiv (SIP pointed-structure pointed-ι pointed-is-sns (X , x) (Y , y))

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Base where

open import Cubical.Data.Int.Base
open import Cubical.Data.Nat.Base
open import Cubical.Data.Sigma

open import Cubical.Foundations.Pointed.Base

open import Cubical.HITs.Nullification.Base
open import Cubical.HITs.SetTruncation.Base
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.S1.Base
open import Cubical.HITs.Susp.Base
open import Cubical.HITs.Truncation.Base

private
  variable
    ℓ : Level
    A : Type ℓ

--- Cohomology ---

{- EM-spaces Kₙ from Brunerie 2016 -}
coHomK : (n : ℕ) → Type₀
coHomK zero = Int
coHomK (suc n) = ∥ S₊ (suc n) ∥ (2 + suc n)

{- Cohomology -}
coHom : (n : ℕ) → Type ℓ → Type ℓ
coHom n A = ∥ (A → coHomK n) ∥₂

--- Reduced cohomology ---

coHom-pt : (n : ℕ) → coHomK n
coHom-pt 0 = 0
coHom-pt 1 = ∣ base ∣
coHom-pt (suc (suc n)) = ∣ north ∣

{- Pointed version of Kₙ  -}
coHomK-ptd : (n : ℕ) → Pointed (ℓ-zero)
coHomK-ptd n = coHomK n , coHom-pt n

{- Reduced cohomology -}
coHomRed : (n : ℕ) → (A : Pointed ℓ) → Type ℓ
coHomRed n A = ∥ A →∙ coHomK-ptd n ∥₂

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module Unsolved-meta-in-postulate where

postulate P : _


text:
{-# OPTIONS --without-K --safe #-}

module Data.Bits where

open import Level

infixr 8 0∷_ 1∷_
data Bits : Type where
  [] : Bits
  0∷_ : Bits → Bits
  1∷_ : Bits → Bits


text:
module RecordPatternMatching where

-- Sigma type.

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

_×_ : Set → Set → Set
A × B = Σ A λ _ → B

-- Curry and uncurry with pattern matching.

curry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
        ((p : Σ A B) → C p) →
        ((x : A) → (y : B x) → C (x , y))
curry f x y = f (x , y)

uncurry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
          ((x : A) → (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f (x , y) = f x y

-- We still have η-equality.

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

curry∘uncurry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
                (f : (x : A) → (y : B x) → C (x , y)) →
                (x : A) → (y : B x) →
                curry {C = C} (uncurry f) x y ≡ f x y
curry∘uncurry f x y = refl

uncurry∘curry : ∀ {A : Set} {B : A → Set} {C : Σ A B → Set} →
                (f : (p : Σ A B) → C p) →
                (p : Σ A B) →
                uncurry {C = C} (curry f) p ≡ f p
uncurry∘curry f p = refl

-- Nested pattern matching is also possible.

to : {A B C : Set} → A × (B × C) → (A × B) × C
to (x , (y , z)) = ((x , y) , z)

from : {A B C : Set} → (A × B) × C → A × (B × C)
from ((x , y) , z) = (x , (y , z))

from∘to : {A B C : Set} (p : A × (B × C)) → from (to p) ≡ p
from∘to p = refl

data Bool : Set where
  true false : Bool

data ⊥ : Set where

F : Bool → Set
F true  = Bool
F false = ⊥

foo : Σ Bool F → Bool
foo (true  , b)  = b
foo (false , ())

bar : ∀ p → F (foo p) → F (foo p)
bar (true  , true)  = λ b → b
bar (true  , false) = λ ()
bar (false , ())

baz : (Σ Bool λ _ → Σ Bool λ _ → Bool) → Bool
baz (true  , (b , c)) = b
baz (false , (b , c)) = c

lemma : ∀ p → baz (false , p) ≡ proj₂ p
lemma p = refl

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

add : ℕ × ℕ → ℕ
add (zero  , n) = n
add (suc m , n) = suc (add (m , n))

-- The code below used to trigger a bug: in one part of the code B was
-- assumed to be reduced to an application of a record type
-- constructor.

data Unit : Set where
  unit : Unit

B : Set
B = Σ Unit λ _ → Unit

C : B → Set₁
C (_ , _) = Set

-- The code below, which involves a clause with a "swapping
-- permutation", also used to trigger a bug.

data P : ⊥ → ⊥ → Set where
  p : (x y : ⊥) → P x y

Bar : (x : ⊥) → P x x → P x x → Set₁
Bar .x _ (p x .x) = Set

-- Another example which used to trigger a bug:

G : (Σ ⊥ λ x → Σ ⊥ λ y → x ≡ y) → Set₁
G (x , (.x , refl)) = Set

-- Record patterns containing dot patterns are supported.

Foo : (p₁ p₂ : B) → proj₁ p₁ ≡ proj₁ p₂ → Unit
Foo (x , y) (.x , y′) refl = unit

Foo-eval : (p : B) → Foo p p refl ≡ unit
Foo-eval _ = refl

-- Record patterns containing dot patterns as well as data type
-- patterns are also supported.

D : (p₁ p₂ : B) → proj₁ p₁ ≡ proj₁ p₂ → Set₁
D (x , y) (.x , unit) refl = Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module L.Base.Coproduct where

-- Reexport definitions
open import L.Base.Coproduct.Core public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
module #5 where

open import Level
open import Data.Product
open import Data.Bool
open import Relation.Binary.PropositionalEquality

{-
Exercise 1.5. Show that if we define A + B :≡ ∑(x:2) rec2(U, A, B, x), then we can give a definition
of indA+B for which the definitional equalities stated in §1.7 hold.
-}

rec₂ : ∀{c}{C : Set c} → C → C → Bool → C
rec₂ c₀ c₁ true = c₁
rec₂ c₀ c₁ false = c₀

ind₂ : ∀{c}(C : Bool → Set c) → C false → C true → (x : Bool) → C x
ind₂ C c₀ c₁ true = c₁
ind₂ C c₀ c₁ false = c₀

_⊎_ : ∀ {i} → Set i → Set i → Set _
A ⊎ B = Σ Bool λ b → if b then A else B

module SumTwo {a}{A B : Set a} where

  inl : A → A ⊎ B
  inl x = true , x

  inr : B → A ⊎ B
  inr y = false , y

  rec-sum₂ : ∀{a b c}{A : Set a}{B : A → Set b} → (C : Σ A B -> Set c) → (f : (x : A)(y : B x) → C (x , y)) → (s : Σ A B) → C s
  rec-sum₂ C f (x , y) = f x y

  ind-sum₂ : ∀{c}(C : A ⊎ B -> Set c) → ((x : A) → C (inl x)) → ((y : B) → C (inr y)) → (u : A ⊎ B) → C u
  ind-sum₂ C c₁ c₀ u = rec-sum₂ C (ind₂ (λ b → (z : if b then A else B) → C (b , z)) c₀ c₁) u

  ind-sum₂-β₁ : ∀{c}(C : A ⊎ B -> Set c) → (f : (x : A) → C (inl x)) → (g : (y : B) → C (inr y)) → (x : A) → ind-sum₂ C f g (inl x) ≡ f x
  ind-sum₂-β₁ C f g x = refl

  ind-sum₂-β₂ : ∀{c}(C : A ⊎ B -> Set c) → (f : (x : A) → C (inl x)) → (g : (y : B) → C (inr y)) → (x : B) → ind-sum₂ C f g (inr x) ≡ g x
  ind-sum₂-β₂ C f g x = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
{-# OPTIONS --cubical --safe #-}

module Categories.Exponential where

open import Prelude hiding (_×_)
open import Categories
open import Categories.Product

module _ {ℓ₁ ℓ₂} (C : Category ℓ₁ ℓ₂) (hasProducts : HasProducts C) where
  open Category C
  open HasProducts hasProducts

  module _ (Y Z : Ob) where
    record Exponential : Type (ℓ₁ ℓ⊔ ℓ₂) where
      field
        obj : Ob
        eval : C [ obj × Y , Z ]
        uniq : ∀ (X : Ob) (f : C [ X × Y , Z ]) →
              ∃![ f~ ] (C [ eval ∘ (f~ |×| Category.Id C) ] ≡ f)

  HasExponentials : Type (ℓ₁ ℓ⊔ ℓ₂)
  HasExponentials = ∀ X Y → Exponential X Y

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- Some negative results related to weak bisimilarity and expansion
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Delay-monad.Bisimilarity.Negative {a} {A : Type a} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Termination

------------------------------------------------------------------------
-- Lemmas stating that functions of certain types can be defined iff A
-- is uninhabited

-- The computation now x is an expansion of
-- later (record { force = now x }) for every x : A iff A is
-- uninhabited.

Now≳later-now = (x : A) → now x ≳ later (record { force = now x })

now≳later-now⇔uninhabited : Now≳later-now ⇔ ¬ A
now≳later-now⇔uninhabited = record
  { to   = Now≳later-now  ↝⟨ (λ hyp x → case hyp x of λ ()) ⟩□
           ¬ A            □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ hyp _ → hyp _ _) ⟩□
           Now≳later-now    □
  }

-- A variant of laterˡ⁻¹ for (fully defined) expansion can be defined
-- iff A is uninhabited.

Laterˡ⁻¹-≳ = ∀ {x} {y : Delay A ∞} → later x ≳ y → force x ≳ y

laterˡ⁻¹-≳⇔uninhabited : Laterˡ⁻¹-≳ ⇔ ¬ A
laterˡ⁻¹-≳⇔uninhabited = record
  { to   = Laterˡ⁻¹-≳     ↝⟨ (λ hyp _ → hyp (reflexive _)) ⟩
           Now≳later-now  ↝⟨ _⇔_.to now≳later-now⇔uninhabited ⟩□
           ¬ A            □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ hyp {_ _} _ → hyp _ _) ⟩□
           Laterˡ⁻¹-≳       □
  }

-- The following variants of transitivity can be proved iff A is
-- uninhabited.

Transitivity-≈≳≳ = {x y z : Delay A ∞} → x ≈ y → y ≳ z → x ≳ z
Transitivity-≳≈≳ = {x y z : Delay A ∞} → x ≳ y → y ≈ z → x ≳ z

transitive-≈≳≳⇔uninhabited : Transitivity-≈≳≳ ⇔ ¬ A
transitive-≈≳≳⇔uninhabited = record
  { to   = Transitivity-≈≳≳  ↝⟨ (λ trans → trans (laterʳ (reflexive _))) ⟩
           Laterˡ⁻¹-≳        ↝⟨ _⇔_.to laterˡ⁻¹-≳⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)   ↝⟨ (λ hyp {_ _ _} _ _ → hyp _ _) ⟩□
           Transitivity-≈≳≳  □
  }

transitive-≳≈≳⇔uninhabited : Transitivity-≳≈≳ ⇔ ¬ A
transitive-≳≈≳⇔uninhabited = record
  { to   = Transitivity-≳≈≳  ↝⟨ (λ trans {_ y} lx≳y → later⁻¹ {y = record { force = y }}
                                                              (trans lx≳y (laterʳ (reflexive _)))) ⟩
           Laterˡ⁻¹-≳        ↝⟨ _⇔_.to laterˡ⁻¹-≳⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)   ↝⟨ (λ hyp {_ _ _} _ _ → hyp _ _) ⟩□
           Transitivity-≳≈≳  □
  }

------------------------------------------------------------------------
-- Lemmas stating that certain size-preserving functions can be
-- defined iff A is uninhabited

-- A variant of laterˡ⁻¹ in which one occurrence of weak bisimilarity
-- is replaced by strong bisimilarity, and both arguments are
-- specialised, can be made size-preserving iff A is uninhabited.
--
-- This lemma is used to prove all other similar results below
-- (directly or indirectly), with the exception that an alternative,
-- more direct proof is also given for one of the results.

Laterˡ⁻¹-∼≈ = ∀ {i} {x : A} →
              [ i ] later (λ { .force → now x }) ∼ never →
              [ i ] now x                        ≈ never

size-preserving-laterˡ⁻¹-∼≈⇔uninhabited : Laterˡ⁻¹-∼≈ ⇔ ¬ A
size-preserving-laterˡ⁻¹-∼≈⇔uninhabited = record
  { to   = Laterˡ⁻¹-∼≈  ↝⟨ (λ laterˡ⁻¹-∼≈ x → contradiction (laterˡ⁻¹-∼≈ {_}) x ∞) ⟩□
           ¬ A          □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _} _ → trivial _ _) ⟩□
           Laterˡ⁻¹-∼≈      □
  }
  where

  module _ (laterˡ⁻¹-∼≈ : Laterˡ⁻¹-∼≈) (x : A) where

    mutual

      now≈never : ∀ {i} → [ i ] now x ≈ never
      now≈never = laterˡ⁻¹-∼≈ (later now∼never)

      now∼never : ∀ {i} → [ i ] now x ∼′ never
      force now∼never {j = j} = ⊥-elim (contradiction j)

      contradiction : Size → ⊥
      contradiction i = now≉never (now≈never {i = i})

-- A variant of Laterˡ⁻¹-∼≈ which it is sometimes easier to work with.

Laterˡ⁻¹-∼≈′ = ∀ {i} {x : A} →
               [ i ] later (record { force = now x }) ∼ never →
               [ i ] now x                            ≈ never

size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited : Laterˡ⁻¹-∼≈′ ⇔ ¬ A
size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited =
  Laterˡ⁻¹-∼≈′  ↝⟨ record { to   = _∘ transitive-∼ʳ (later λ { .force → now })
                          ; from = _∘ transitive-∼ʳ (later λ { .force → now })
                          } ⟩
  Laterˡ⁻¹-∼≈   ↝⟨ size-preserving-laterˡ⁻¹-∼≈⇔uninhabited ⟩□
  ¬ A           □

-- A variant of laterʳ⁻¹ for weak bisimilarity in which one occurrence
-- of weak bisimilarity is replaced by strong bisimilarity, and both
-- arguments are specialised, can be made size-preserving iff A is
-- uninhabited.

Laterʳ⁻¹-∼≈ = ∀ {i} {x : A} →
              [ i ] never ∼ later (record { force = now x }) →
              [ i ] never ≈ now x

size-preserving-laterʳ⁻¹-∼≈⇔uninhabited : Laterʳ⁻¹-∼≈ ⇔ ¬ A
size-preserving-laterʳ⁻¹-∼≈⇔uninhabited =
  Laterʳ⁻¹-∼≈   ↝⟨ record { to   = λ laterʳ⁻¹ → symmetric ∘ laterʳ⁻¹ ∘ symmetric
                          ; from = λ laterˡ⁻¹ → symmetric ∘ laterˡ⁻¹ ∘ symmetric
                          } ⟩
  Laterˡ⁻¹-∼≈′  ↝⟨ size-preserving-laterˡ⁻¹-∼≈′⇔uninhabited ⟩□
  ¬ A           □

-- A variant of laterʳ⁻¹ for expansion in which one occurrence of the
-- expansion relation is replaced by strong bisimilarity, and both
-- arguments are specialised, can be made size-preserving iff A is
-- uninhabited.

Laterʳ⁻¹-∼≳ = ∀ {i} {x : A} →
              [ i ] never ∼ later (record { force = now x }) →
              [ i ] never ≳ now x

size-preserving-laterʳ⁻¹-∼≳⇔uninhabited : Laterʳ⁻¹-∼≳ ⇔ ¬ A
size-preserving-laterʳ⁻¹-∼≳⇔uninhabited = record
  { to   = Laterʳ⁻¹-∼≳  ↝⟨ ≳→ ∘_ ⟩
           Laterʳ⁻¹-∼≈  ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-∼≈⇔uninhabited ⟩□
           ¬ A          □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _} _ → trivial _ _) ⟩□
           Laterʳ⁻¹-∼≳      □
  }

-- The function laterˡ⁻¹ can be made size-preserving iff A is
-- uninhabited.

Laterˡ⁻¹-≈ = ∀ {i x} {y : Delay A ∞} →
             [ i ] later x ≈ y → [ i ] force x ≈ y

size-preserving-laterˡ⁻¹-≈⇔uninhabited : Laterˡ⁻¹-≈ ⇔ ¬ A
size-preserving-laterˡ⁻¹-≈⇔uninhabited = record
  { to   = Laterˡ⁻¹-≈   ↝⟨ _∘ ∼→ ⟩
           Laterˡ⁻¹-∼≈  ↝⟨ _⇔_.to size-preserving-laterˡ⁻¹-∼≈⇔uninhabited ⟩□
           ¬ A          □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
           Laterˡ⁻¹-≈       □
  }

-- The function laterʳ⁻¹ can be made size-preserving for weak
-- bisimilarity iff A is uninhabited.

Laterʳ⁻¹-≈ = ∀ {i} {x : Delay A ∞} {y} →
             [ i ] x ≈ later y → [ i ] x ≈ force y

size-preserving-laterʳ⁻¹-≈⇔uninhabited : Laterʳ⁻¹-≈ ⇔ ¬ A
size-preserving-laterʳ⁻¹-≈⇔uninhabited =
  Laterʳ⁻¹-≈  ↝⟨ record { to   = λ laterʳ⁻¹ → symmetric ∘ laterʳ⁻¹ ∘ symmetric
                        ; from = λ laterˡ⁻¹ → symmetric ∘ laterˡ⁻¹ ∘ symmetric
                        } ⟩
  Laterˡ⁻¹-≈  ↝⟨ size-preserving-laterˡ⁻¹-≈⇔uninhabited ⟩□

  ¬ A         □

-- The function laterʳ⁻¹ can be made size-preserving for expansion iff
-- A is uninhabited.

Laterʳ⁻¹-≳ = ∀ {i} {x : Delay A ∞} {y} →
             [ i ] x ≳ later y → [ i ] x ≳ force y

size-preserving-laterʳ⁻¹-≳⇔uninhabited : Laterʳ⁻¹-≳ ⇔ ¬ A
size-preserving-laterʳ⁻¹-≳⇔uninhabited = record
  { to   = Laterʳ⁻¹-≳   ↝⟨ _∘ ∼→ ⟩
           Laterʳ⁻¹-∼≳  ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-∼≳⇔uninhabited ⟩□
           ¬ A          □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
           Laterʳ⁻¹-≳       □
  }

-- A variant of ⇓-respects-≈ in which _≈_ is replaced by _∼_ can be
-- made size-preserving in the second argument iff A is uninhabited.

⇓-Respects-∼ʳ = ∀ {i x y} {z : A} →
                x ⇓ z → [ i ] x ∼ y → Terminates i y z

size-preserving-⇓-respects-∼ʳ⇔uninhabited : ⇓-Respects-∼ʳ ⇔ ¬ A
size-preserving-⇓-respects-∼ʳ⇔uninhabited = record
  { to   = ⇓-Respects-∼ʳ  ↝⟨ (λ resp → resp (laterʳ now)) ⟩
           Laterˡ⁻¹-∼≈    ↝⟨ _⇔_.to size-preserving-laterˡ⁻¹-∼≈⇔uninhabited ⟩
           ¬ A            □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           ⇓-Respects-∼ʳ    □
  }

-- The lemma ⇓-respects-≈ can be made size-preserving in the second
-- argument iff A is uninhabited.

⇓-Respects-≈ʳ = ∀ {i x y} {z : A} →
                x ⇓ z → [ i ] x ≈ y → Terminates i y z

size-preserving-⇓-respects-≈ʳ⇔uninhabited : ⇓-Respects-≈ʳ ⇔ ¬ A
size-preserving-⇓-respects-≈ʳ⇔uninhabited = record
  { to   = ⇓-Respects-≈ʳ  ↝⟨ (λ resp x⇓z → resp x⇓z ∘ ∼→) ⟩
           ⇓-Respects-∼ʳ  ↝⟨ _⇔_.to size-preserving-⇓-respects-∼ʳ⇔uninhabited ⟩□
           ¬ A            □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           ⇓-Respects-≈ʳ    □
  }

-- There is a transitivity-like proof, taking weak bisimilarity and
-- strong bisimilarity to weak bisimilarity, that preserves the size
-- of the second argument iff A is uninhabited.

Transitivity-≈∼ʳ = ∀ {i} {x y z : Delay A ∞} →
                   x ≈ y → [ i ] y ∼ z → [ i ] x ≈ z

size-preserving-transitivity-≈∼ʳ⇔uninhabited : Transitivity-≈∼ʳ ⇔ ¬ A
size-preserving-transitivity-≈∼ʳ⇔uninhabited = record
  { to   = Transitivity-≈∼ʳ  ↝⟨ (λ trans → trans) ⟩
           ⇓-Respects-∼ʳ     ↝⟨ _⇔_.to size-preserving-⇓-respects-∼ʳ⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≈∼ʳ  □
  }

-- There is a transitivity-like proof, taking strong bisimilarity and
-- weak bisimilarity to weak bisimilarity, that preserves the size of
-- the first argument iff A is uninhabited.

Transitivity-∼≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ∼ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-∼≈ˡ⇔uninhabited : Transitivity-∼≈ˡ ⇔ ¬ A
size-preserving-transitivity-∼≈ˡ⇔uninhabited =
  Transitivity-∼≈ˡ  ↝⟨ record { to   = λ trans {_ _ _ _} p q →
                                         symmetric (trans (symmetric q) (symmetric p))
                              ; from = λ trans {_ _ _ _} p q →
                                         symmetric (trans (symmetric q) (symmetric p))
                              } ⟩
  Transitivity-≈∼ʳ  ↝⟨ size-preserving-transitivity-≈∼ʳ⇔uninhabited ⟩□

  ¬ A               □

-- There is a transitivity-like proof, taking strong bisimilarity and
-- expansion to expansion, that preserves the size of the first
-- argument iff A is uninhabited.

Transitivity-∼≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ∼ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-∼≳ˡ⇔uninhabited : Transitivity-∼≳ˡ ⇔ ¬ A
size-preserving-transitivity-∼≳ˡ⇔uninhabited = record
  { to   = Transitivity-∼≳ˡ  ↝⟨ (λ trans never∼lnx → trans never∼lnx (laterˡ now)) ⟩
           Laterʳ⁻¹-∼≳       ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-∼≳⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-∼≳ˡ  □
  }

-- There is a transitivity proof for weak bisimilarity that preserves
-- the size of the second argument iff A is uninhabited.

Transitivity-≈ʳ = ∀ {i} {x y z : Delay A ∞} →
                  x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≈ʳ⇔uninhabited : Transitivity-≈ʳ ⇔ ¬ A
size-preserving-transitivity-≈ʳ⇔uninhabited = record
  { to   = Transitivity-≈ʳ  ↝⟨ (λ trans → trans) ⟩
           ⇓-Respects-≈ʳ    ↝⟨ _⇔_.to size-preserving-⇓-respects-≈ʳ⇔uninhabited ⟩□
           ¬ A              □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≈ʳ  □
  }

-- There is a transitivity proof for weak bisimilarity that preserves
-- the size of the first argument iff A is uninhabited.

Transitivity-≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≈ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≈ˡ⇔uninhabited : Transitivity-≈ˡ ⇔ ¬ A
size-preserving-transitivity-≈ˡ⇔uninhabited =
  Transitivity-≈ˡ  ↝⟨ record { to   = λ trans {_ _ _ _} p q →
                                        symmetric (trans (symmetric q) (symmetric p))
                             ; from = λ trans {_ _ _ _} p q →
                                        symmetric (trans (symmetric q) (symmetric p))
                             } ⟩
  Transitivity-≈ʳ  ↝⟨ size-preserving-transitivity-≈ʳ⇔uninhabited ⟩□

  ¬ A              □

-- There is a transitivity proof for expansion that preserves the size
-- of the first argument iff A is uninhabited.

Transitivity-≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≳ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-≳ˡ⇔uninhabited : Transitivity-≳ˡ ⇔ ¬ A
size-preserving-transitivity-≳ˡ⇔uninhabited = record
  { to   = Transitivity-≳ˡ   ↝⟨ _∘ ∼→ ⟩
           Transitivity-∼≳ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-∼≳ˡ⇔uninhabited ⟩□
           ¬ A               □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≳ˡ  □
  }

-- There is a fully size-preserving transitivity proof for weak
-- bisimilarity iff A is uninhabited.

Transitivity-≈ = ∀ {i} {x y z : Delay A ∞} →
                 [ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≈⇔uninhabited : Transitivity-≈ ⇔ ¬ A
size-preserving-transitivity-≈⇔uninhabited = record
  { to   = Transitivity-≈   ↝⟨ (λ trans → trans) ⟩
           Transitivity-≈ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-≈ˡ⇔uninhabited ⟩
           ¬ A              □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≈   □
  }

-- The following two lemmas provide an alternative proof of one
-- direction of the previous lemma (with a small change to one of the
-- types).

-- If there is a transitivity proof for weak bisimilarity that is
-- size-preserving in both arguments, then weak bisimilarity is
-- trivial.

size-preserving-transitivity-≈→trivial :
  (∀ {i} x {y z : Delay A ∞} →
   [ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z) →
  ∀ {i} (x y : Delay A ∞) → [ i ] x ≈ y
size-preserving-transitivity-≈→trivial _≈⟨_⟩ʷ_ x y =
  (x                         ≈⟨ laterʳ (x ∎ʷ) ⟩ʷ
  (later (λ { .force → x })  ≈⟨ later (λ { .force → size-preserving-transitivity-≈→trivial _≈⟨_⟩ʷ_ x y }) ⟩ʷ
  (later (λ { .force → y })  ≈⟨ laterˡ (y ∎ʷ) ⟩ʷ
  (y                         ∎ʷ))))
  where
  _∎ʷ = reflexive

-- If there is a transitivity proof for weak bisimilarity that is
-- size-preserving in both arguments, then the carrier type A is not
-- inhabited.

size-preserving-transitivity-≈→uninhabited :
  (∀ {i} x {y z : Delay A ∞} →
   [ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z) →
  ¬ A
size-preserving-transitivity-≈→uninhabited trans x =
  now≉never (size-preserving-transitivity-≈→trivial trans (now x) never)

-- There is a fully size-preserving transitivity proof for expansion
-- iff A is uninhabited.

Transitivity-≳ = ∀ {i} {x y z : Delay A ∞} →
                 [ i ] x ≳ y → [ i ] y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-≳⇔uninhabited : Transitivity-≳ ⇔ ¬ A
size-preserving-transitivity-≳⇔uninhabited = record
  { to   = Transitivity-≳   ↝⟨ id ⟩
           Transitivity-≳ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-≳ˡ⇔uninhabited ⟩□
           ¬ A              □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≳ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≳   □
  }

-- There is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of the
-- first argument iff A is uninhabited.

Transitivity-≳≈ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ≳ y → y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈ˡ⇔uninhabited : Transitivity-≳≈ˡ ⇔ ¬ A
size-preserving-transitivity-≳≈ˡ⇔uninhabited = record
  { to   = Transitivity-≳≈ˡ  ↝⟨ _∘ ∼→ ⟩
           Transitivity-∼≈ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-∼≈ˡ⇔uninhabited ⟩
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≳≈ˡ  □
  }

-- There is a transitivity-like proof, taking expansion and weak
-- bisimilarity to weak bisimilarity, that preserves the size of both
-- arguments iff A is uninhabited.

Transitivity-≳≈ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≳ y → [ i ] y ≈ z → [ i ] x ≈ z

size-preserving-transitivity-≳≈⇔uninhabited : Transitivity-≳≈ ⇔ ¬ A
size-preserving-transitivity-≳≈⇔uninhabited = record
  { to   = Transitivity-≳≈   ↝⟨ id ⟩
           Transitivity-≳≈ˡ  ↝⟨ _⇔_.to size-preserving-transitivity-≳≈ˡ⇔uninhabited ⟩
           ¬ A               □
  ; from = ¬ A              ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)  ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≳≈  □
  }

-- There is a transitivity-like proof, taking weak bisimilarity and
-- the converse of expansion to weak bisimilarity, that preserves the
-- size of the second argument iff A is uninhabited.

Transitivity-≈≲ʳ = ∀ {i} {x y z : Delay A ∞} →
                   x ≈ y → [ i ] y ≲ z → [ i ] x ≈ z

size-preserving-transitivity-≈≲ʳ⇔uninhabited : Transitivity-≈≲ʳ ⇔ ¬ A
size-preserving-transitivity-≈≲ʳ⇔uninhabited =
  Transitivity-≈≲ʳ  ↝⟨ record { to   = λ trans x≳y y≈z → symmetric (trans (symmetric y≈z) x≳y)
                              ; from = λ trans x≈y y≲z → symmetric (trans y≲z (symmetric x≈y))
                              } ⟩
  Transitivity-≳≈ˡ  ↝⟨ size-preserving-transitivity-≳≈ˡ⇔uninhabited ⟩□
  ¬ A               □

-- There is a transitivity-like proof, taking weak bisimilarity and
-- the converse of expansion to weak bisimilarity, that preserves the
-- size of both arguments iff A is uninhabited.

Transitivity-≈≲ = ∀ {i} {x y z : Delay A ∞} →
                  [ i ] x ≈ y → [ i ] y ≲ z → [ i ] x ≈ z

size-preserving-transitivity-≈≲⇔uninhabited : Transitivity-≈≲ ⇔ ¬ A
size-preserving-transitivity-≈≲⇔uninhabited =
  Transitivity-≈≲  ↝⟨ record { to   = λ trans x≳y y≈z → symmetric (trans (symmetric y≈z) x≳y)
                             ; from = λ trans x≈y y≲z → symmetric (trans y≲z (symmetric x≈y))
                             } ⟩
  Transitivity-≳≈  ↝⟨ size-preserving-transitivity-≳≈⇔uninhabited ⟩□
  ¬ A              □

-- There is a transitivity-like proof, taking weak bisimilarity and
-- expansion to weak bisimilarity, that preserves the size of the
-- first argument iff A is uninhabited.

Transitivity-≈≳ˡ = ∀ {i} {x y z : Delay A ∞} →
                   [ i ] x ≈ y → y ≳ z → [ i ] x ≈ z

size-preserving-transitivity-≈≳ˡ⇔uninhabited : Transitivity-≈≳ˡ ⇔ ¬ A
size-preserving-transitivity-≈≳ˡ⇔uninhabited = record
  { to   = Transitivity-≈≳ˡ  ↝⟨ (λ trans x≈ly → trans x≈ly (laterˡ (reflexive _))) ⟩
           Laterʳ⁻¹-≈        ↝⟨ _⇔_.to size-preserving-laterʳ⁻¹-≈⇔uninhabited ⟩
           ¬ A               □
  ; from = ¬ A               ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)   ↝⟨ (λ trivial {_ _ _ _} _ _ → trivial _ _) ⟩□
           Transitivity-≈≳ˡ  □
  }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
module CF.Examples.Ex2 where

open import Function
open import Data.Bool
open import Data.Product
open import Data.List
open import Data.Integer
open import Data.String

open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad.Possibly

open import JVM.Contexts
open import JVM.Types
open import JVM.Transform.Assemble

open import JVM.Printer
import JVM.Printer.Jasmin as J

open import CF.Syntax as Src
open import CF.Types
open import CF.Contexts.Lexical
open import CF.Compile

-- int i = 0;
-- while(i < 10) {
--   i = i + 1
-- }
ex₂ : Src.Block void ε
ex₂ =
    Src.num (+ 0) ≔⟨ ∙-idˡ ⟩ Possibly.possibly ∼-all (
    Src.while (bop gt (var ∙⟨ ∙-idʳ ⟩ num (+ 10)) ∙⟨ overlaps ∙-idˡ ⟩
      Src.block (
        Src.asgn (refl ∙⟨ overlaps ∙-idˡ ⟩ bop add (var ∙⟨ ∙-idʳ ⟩ num (+ 1))) ⍮⟨ ∙-idʳ ⟩
        emp)
    )⍮⟨ ∙-idʳ ⟩ emp
  )

-- Which should compile to:
--
-- 0: push 0
-- 1: store 0
-- 2: load 0
-- 3: push 10
-- 4: if_icmplt 7
-- 5: push false // 0
-- 6: goto 8
-- 7: push true  // 1
-- 8: if eq 14   // 0 = false -> jump to end
-- 9: load 0
-- 10: push 1
-- 11: bop add
-- 12: store 0
-- 13: goto 2
-- 14: nop

open import IO as IO
main = IO.run (putStrLn test)
  where
    test = Show.showBytecode $ proj₂ $ exec-extractor $ extract (proj₂ $ compile ex₂)

-- Uncomment this instead of the above main to output Jasmin code.
-- You can assemble this using Jasmin so that you can run the output with java.
-- Disclaimer: the jasmin compiler pass is not verified.
-- main = IO.run (putStrLn (J.unlines $ J.Jasmin.out proc))
--   where
--   proc = procedure "ex1" (proj₂ $ compile ex₂)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Lex.Core directly.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.Relation.Lex.Core where

open import Data.List.Relation.Binary.Lex.Core public


text:
---------------------------------------------------------------------------------
-- Equality

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
infix 4 _≡_

------------------------------------------------------------------------------
-- Equality is an equivalence relation : reflexive, symmetric, and transitive.
-- Reflexivity is built-in to the definition of equality.

sym : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → y ≡ x
sym refl = refl

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y
  →     y ≡ z
    -----
  → x ≡     z
trans refl refl  =  refl

-- Equality satisfies congruence.
-- If two terms are equal, they are eual after the same function is applied to both:
cong : ∀ {A B : Set} (f : A → B) {x y : A}
  → x ≡ y
    ---------
  → f x ≡ f y
cong f refl  =  refl

-- Congruence of 2 arg functions
cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x
  → v ≡ y
    -------------
  → f u v ≡ f x y
cong₂ f refl refl  =  refl

-- Equality is a congruence in the function position of an application.
-- If two functions are equal, then applying them to the same term yields equal terms:
cong-app : ∀ {A B : Set} {f g : A → B}
  → f ≡ g
    ---------------------
  → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

-- Equality satisfies substitution.
-- If two values are equal and a predicate holds of the first then it also holds of the second:
subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    ---------
  → P x → P y
subst P refl px = px

-- Chains of equations : support equational reasoning
module ≡-Reasoning {A : Set} where

  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

open ≡-Reasoning

-- equational proof of transitivity
trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y
  → y ≡ z
    -----
  → x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
  begin
    x
  ≡⟨ x≡y ⟩
    y
  ≡⟨ y≡z ⟩
    z
  ∎

{-
Exercise trans and ≡-Reasoning (practice): TODO
Cannot use the definition of trans’ using ≡-Reasoning as the definition for trans.
WHY?
Hint: look at the definition of _≡⟨_⟩_
-}

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n  =  n
(suc m) + n  =  suc (m + n)

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

{-
Exercise ≤-Reasoning (stretch) TODO
The proof of monotonicity from Chapter Relations can be written in a more readable form
by using an analogue of our notation for ≡-Reasoning.
Define ≤-Reasoning analogously, and use it to write out an alternative proof
that addition is monotonic with regard to inequality.
Rewrite all of +-monoˡ-≤, +-monoʳ-≤, and +-mono-≤.
-}

------------------------------------------------------------------------------
-- Rewriting
-- keyword rewrite : followed by evidence of an EQUALITY
-- that equality is used to rewrite
-- - the type of the goal
-- - and of any variable in scope

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

even-comm : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm m n ev         -- even (n + m)
  rewrite +-comm n m     -- even (m + n) ; ev : even (m + n)
  = ev

--------------------------------------------------
-- Multiple rewrites each separated by a vertical bar.
+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero    n  rewrite +-identity n             =  refl
+-comm′ (suc m) n  rewrite +-suc n m | +-comm′ m n  =  refl

--------------------------------------------------
-- rewrite is shorthand for an use of WITH

even-comm′ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm′ m n ev with   m + n  | +-comm m n
...                  | .(n + m) | refl       = ev

{-
--------------------------------------------------
DOT pattern, .(n + m).
dot followed by an expression.
Used when other info forces value matched to be equal to value of expr in dot pattern.
-}

------------------------------------------------------------------------------
-- subst (instead of rewrite)

even-comm″ : ∀ (m n : ℕ)
  → even (m + n)
    ------------
  → even (n + m)
even-comm″ m n  =  subst even (+-comm m n)

{-
------------------------------------------------------------------------------
Leibniz equality

≡ def is due to Martin Löf (1975).

Older form is due to Leibniz (1686).

IDENTITY OF INDISCERNIBLES:
-  two objects are equal IFF they satisfy the same properties

Below: define Leibniz equality, and show that two terms satisfy Leibniz equality IFF
they satisfy Martin Löf equality.

x ≐ y holds if every property P that holds of x also holds of y

this def is sufficient to ensure the converse
- that every property P that holds of y also holds of x

Let x and y be objects of type A.
x ≐ y holds if for every predicate P over type A we have that P x implies P y:
_]
-}

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

{-
NOTE: write _≐_ {A} x y (instead of x ≐ y) to provide access to implicit parameter.

--------------------------------------------------
FIRST USE OF LEVELS.

Cannot assign Set the type Set (Russell’s Paradox and Girard’s Paradox).

Set is an abbreviation for Set₀

Since _≐_ def  mentions Set on right-hand side, the corresponding signature must use Set₁.

Leibniz equality is reflexive (follows by a variant of the identity function)
and transitive (by a variant of function composition)
-}
refl-≐ : ∀ {A : Set} {x : A}
  → x ≐ x
refl-≐ P Px  =  Px

trans-≐ : ∀ {A : Set} {x y z : A}
  → x ≐ y
  → y ≐ z
    -----
  → x ≐ z
trans-≐ x≐y y≐z P Px  =  y≐z P (x≐y P Px)

-- Symmetry : show that if P x implies P y for all predicates P,
-- then the implication holds the other way round as well:
sym-≐ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → y ≐ x
sym-≐ {A} {x} {y} x≐y P  =  Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx
{-
Given x ≐ y, a specific P, construct a proof that P y implies P x.
Instantiate the equality with a predicate Q such that Q z holds if P z implies P x.
The property Q x is trivial by reflexivity, and hence Q y follows from x ≐ y.
But Q y is exactly a proof of what we require, that P y implies P x.

show Martin Löf equality implies Leibniz equality, and vice versa.

if x ≡ y then need for any P to take evidence of P x to evidence of P y
which can be done since equality of x and y implies that any proof of P x is also a proof of P y:
-}

≡-implies-≐ : ∀ {A : Set} {x y : A}
  → x ≡ y
    -----
  → x ≐ y
≡-implies-≐ x≡y P  =  subst P x≡y

-- given that for any P we can take a proof of P x to a proof of P y then show x ≡ y:

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y  =  Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx
{-
proof similar to that for symmetry of Leibniz equality.
We take Q to be the predicate that holds of z if x ≡ z.
Then Q x is trivial by reflexivity of Martin Löf equality, and hence Q y follows from x ≐ y.
But Q y is exactly a proof of what we require, that x ≡ y.

(Parts adapted from
≐≃≡: Leibniz Equality is Isomorphic to Martin-Löf Identity, Parametrically,
by Andreas Abel, Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler, draft, 2017.)

------------------------------------------------------------------------------
Universe polymorphism

Not every type belongs to Set.
Set₀ : Set₁, Set₁ : Set₂, ...

≡ def at beginning is ok for comparing values of a type that belongs to Set.

How to compare two values of a type that belongs to Set ℓ for some arbitrary level ℓ?

Via universe polymorphism : definition made with respect to arbitrary level ℓ.
To use levels:
-}
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)
{-

Levels : isomorphic to natural numbers

lzero : Level
lsuc  : Level → Level

Set₀, Set₁, Set₂, and so on, are abbreviations for

Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))

_⊔_ : Level → Level → Level -- given two levels returns the largest

equality, symetry, generalised to an arbitrary level:
-}

data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl′ : x ≡′ x

sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
  → x ≡′ y
    ------
  → y ≡′ x
sym′ refl′ = refl′

{-
most defs in standard library are generalised to arbitrary levels

generalised Leibniz equality:
-}

_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y

-- generalized composition
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘ f) x  =  g (f x)

{-
Standard library

defines _≡⟨_⟩_ as step-≡, which reverses the order of the arguments.

defines a syntax macro ((automatically imported with step-≡) i, which recovers original arg order:
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module zfc where

open import Level
open import Relation.Binary
open import Relation.Nullary
open import logic

record IsZFC {n m : Level }
     (ZFSet : Set n)
     (_∋_ : ( A x : ZFSet  ) → Set m)
     (_≈_ : Rel ZFSet m)
     (∅  : ZFSet)
     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
       : Set (suc (n ⊔ suc m)) where
  field
     -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
     choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
     choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
  infixr  200 _∈_
  infixr  230 _∩_
  _∈_ : ( A B : ZFSet  ) → Set m
  A ∈ B = B ∋ A
  _∩_ : ( A B : ZFSet  ) → ZFSet
  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )

record ZFC {n m : Level } : Set (suc (n ⊔ suc m)) where
  field
     ZFSet : Set n
     _∋_ : ( A x : ZFSet  ) → Set m
     _≈_ : ( A B : ZFSet  ) → Set m
     ∅  : ZFSet
     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet
     isZFC : IsZFC ZFSet _∋_ _≈_ ∅ Select

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
{-# OPTIONS --without-K --safe #-}

{-
  Properties regarding Morphisms of a category:
  - Regular Monomorphism
  - Regular Epimorphism

  https://ncatlab.org/nlab/show/regular+epimorphism

  These are defined here rather than in Morphism, as this
  might cause import cycles (and make the dependency graph
  very odd).
-}
open import Categories.Category.Core

module Categories.Morphism.Regular {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Morphism 𝒞
open import Categories.Diagram.Equalizer 𝒞
open import Categories.Diagram.Coequalizer 𝒞

open Category 𝒞

private
  variable
    A B : Obj
    f : A ⇒ B

record RegularMono (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    { C } : Obj
    g : B ⇒ C
    h : B ⇒ C
    equalizer : IsEqualizer f h g

record RegularEpi (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    { C } : Obj
    h : C ⇒ A
    g : C ⇒ A
    coequalizer : IsCoequalizer h g f

RegularMono⇒Mono : RegularMono f → Mono f
RegularMono⇒Mono regular = IsEqualizer⇒Mono equalizer
  where
    open RegularMono regular

RegularEpi⇒Epi : RegularEpi f → Epi f
RegularEpi⇒Epi regular = IsCoequalizer⇒Epi coequalizer
  where
    open RegularEpi regular

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
module Forcing where

open import Common.IO
open import Common.Unit
open import Lib.Vec
open import Common.Nat

len : {A : Set}{n : Nat} → Vec A n → Nat
len {A} .{zero}  []             = zero
len {A} .{suc n} (_∷_ {n} x xs) = suc n

len2 : {A : Set}{n : Nat} → Vec A n → Nat
len2 [] = 0
len2 (_∷_ {n} x xs) = suc (len2 {n = n} xs)

len3 : {A : Set}{n : Nat} → Vec A n → Nat
len3 {n = zero}  []              = zero
len3 {n = suc n} (_∷_ .{n} x xs) = suc n

len4 : {A : Set}{n : Nat} → Vec A n → Nat
len4 []                 = zero
len4 (_∷_ {zero}  x xs) = suc zero
len4 (_∷_ {suc n} x xs) = suc (suc n)

main : IO Unit
main =
    printNat (len  l1) ,,
    printNat (len  l2) ,,
    printNat (len  l3) ,,

    printNat (len2 l1) ,,
    printNat (len2 l2) ,,
    printNat (len2 l3) ,,

    printNat (len3 l1) ,,
    printNat (len3 l2) ,,
    printNat (len3 l3) ,,

    printNat (len4 l1) ,,
    printNat (len4 l2) ,,
    printNat (len4 l3) ,,

    return unit
  where l1 = "a" ∷ ("b" ∷ ("c" ∷ []))
        l2 = 1 ∷ (2 ∷ (3 ∷ (4 ∷ (5 ∷ []))))
        l3 : Vec Nat zero
        l3 = []

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists, basic types and operations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.Base where

open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
open import Data.Fin using (Fin; zero; suc)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Bool.Base as Bool
  using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
open import Data.Product as Prod using (_×_; _,_)
open import Data.These as These using (These; this; that; these)
open import Function using (id; _∘_ ; _∘′_; const; flip)

open import Relation.Nullary using (yes; no)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Unary.Properties using (∁?)

------------------------------------------------------------------------
-- Types

open import Agda.Builtin.List public
  using (List; []; _∷_)

------------------------------------------------------------------------
-- Operations for transforming lists

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

mapMaybe : ∀ {a b} {A : Set a} {B : Set b} → (A → Maybe B) → List A → List B
mapMaybe p []       = []
mapMaybe p (x ∷ xs) with p x
... | just y  = y ∷ mapMaybe p xs
... | nothing =     mapMaybe p xs

module _ {a} {A : Set a} where

  infixr 5 _++_

  _++_ : List A → List A → List A
  []       ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  intersperse : A → List A → List A
  intersperse x []       = []
  intersperse x (y ∷ []) = y ∷ []
  intersperse x (y ∷ ys) = y ∷ x ∷ intersperse x ys

  intercalate : List A → List (List A) → List A
  intercalate xs []         = []
  intercalate xs (ys ∷ [])  = ys
  intercalate xs (ys ∷ yss) = ys ++ xs ++ intercalate xs yss

------------------------------------------------------------------------
-- Aligning and zipping

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  alignWith : (These A B → C) → List A → List B → List C
  alignWith f []       bs       = map (f ∘′ that) bs
  alignWith f as       []       = map (f ∘′ this) as
  alignWith f (a ∷ as) (b ∷ bs) = f (these a b) ∷ alignWith f as bs

  zipWith : (A → B → C) → List A → List B → List C
  zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
  zipWith f _        _        = []

  unalignWith : (A → These B C) → List A → List B × List C
  unalignWith f []       = [] , []
  unalignWith f (a ∷ as) with f a
  ... | this b    = Prod.map₁ (b ∷_) (unalignWith f as)
  ... | that c    = Prod.map₂ (c ∷_) (unalignWith f as)
  ... | these b c = Prod.map (b ∷_) (c ∷_) (unalignWith f as)

  unzipWith : (A → B × C) → List A → List B × List C
  unzipWith f []         = [] , []
  unzipWith f (xy ∷ xys) = Prod.zip _∷_ _∷_ (f xy) (unzipWith f xys)

  partitionSumsWith : (A → B ⊎ C) → List A → List B × List C
  partitionSumsWith f = unalignWith (These.fromSum ∘′ f)

module _ {a b} {A : Set a} {B : Set b} where

  align : List A → List B → List (These A B)
  align = alignWith id

  zip : List A → List B → List (A × B)
  zip = zipWith (_,_)

  unalign : List (These A B) → List A × List B
  unalign = unalignWith id

  unzip : List (A × B) → List A × List B
  unzip = unzipWith id

  partitionSums : List (A ⊎ B) → List A × List B
  partitionSums = partitionSumsWith id

------------------------------------------------------------------------
-- Operations for reducing lists

foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
foldr c n []       = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

foldl : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A
foldl c n []       = n
foldl c n (x ∷ xs) = foldl c (c n x) xs

concat : ∀ {a} {A : Set a} → List (List A) → List A
concat = foldr _++_ []

concatMap : ∀ {a b} {A : Set a} {B : Set b} →
            (A → List B) → List A → List B
concatMap f = concat ∘ map f

null : ∀ {a} {A : Set a} → List A → Bool
null []       = true
null (x ∷ xs) = false

and : List Bool → Bool
and = foldr _∧_ true

or : List Bool → Bool
or = foldr _∨_ false

any : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
any p = or ∘ map p

all : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
all p = and ∘ map p

sum : List ℕ → ℕ
sum = foldr _+_ 0

product : List ℕ → ℕ
product = foldr _*_ 1

length : ∀ {a} {A : Set a} → List A → ℕ
length = foldr (const suc) 0

------------------------------------------------------------------------
-- Operations for constructing lists

[_] : ∀ {a} {A : Set a} → A → List A
[ x ] = x ∷ []

fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A
fromMaybe (just x) = [ x ]
fromMaybe nothing  = []

replicate : ∀ {a} {A : Set a} → ℕ → A → List A
replicate zero    x = []
replicate (suc n) x = x ∷ replicate n x

inits : ∀ {a} {A : Set a} → List A → List (List A)
inits []       = [] ∷ []
inits (x ∷ xs) = [] ∷ map (x ∷_) (inits xs)

tails : ∀ {a} {A : Set a} → List A → List (List A)
tails []       = [] ∷ []
tails (x ∷ xs) = (x ∷ xs) ∷ tails xs

-- Scans

scanr : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → B) → B → List A → List B
scanr f e []       = e ∷ []
scanr f e (x ∷ xs) with scanr f e xs
... | []     = []                -- dead branch
... | y ∷ ys = f x y ∷ y ∷ ys

scanl : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → A) → A → List B → List A
scanl f e []       = e ∷ []
scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs

module _ {a} {A : Set a} where

-- Tabulation

  applyUpTo : (ℕ → A) → ℕ → List A
  applyUpTo f zero    = []
  applyUpTo f (suc n) = f zero ∷ applyUpTo (f ∘ suc) n

  applyDownFrom : (ℕ → A) → ℕ → List A
  applyDownFrom f zero = []
  applyDownFrom f (suc n) = f n ∷ applyDownFrom f n

  tabulate : ∀ {n} (f : Fin n → A) → List A
  tabulate {zero}  f = []
  tabulate {suc n} f = f Fin.zero ∷ tabulate (f ∘ Fin.suc)

  lookup : ∀ (xs : List A) → Fin (length xs) → A
  lookup [] ()
  lookup (x ∷ xs) Fin.zero    = x
  lookup (x ∷ xs) (Fin.suc i) = lookup xs i

-- Numerical

upTo : ℕ → List ℕ
upTo = applyUpTo id

downFrom : ℕ → List ℕ
downFrom = applyDownFrom id

allFin : ∀ n → List (Fin n)
allFin n = tabulate id

-- Other

unfold : ∀ {a b} {A : Set a} (B : ℕ → Set b)
         (f : ∀ {n} → B (suc n) → Maybe (A × B n)) →
         ∀ {n} → B n → List A
unfold B f {n = zero}  s = []
unfold B f {n = suc n} s with f s
... | nothing       = []
... | just (x , s') = x ∷ unfold B f s'

------------------------------------------------------------------------
-- Operations for deconstructing lists

-- Note that although these combinators can be useful for programming, when
-- proving it is often a better idea to manually destruct a list argument:
-- each branch of the pattern-matching will have a refined type.

module _ {a} {A : Set a} where

  uncons : List A → Maybe (A × List A)
  uncons []       = nothing
  uncons (x ∷ xs) = just (x , xs)

  head : List A → Maybe A
  head []      = nothing
  head (x ∷ _) = just x

  tail : List A → Maybe (List A)
  tail []       = nothing
  tail (_ ∷ xs) = just xs

take : ∀ {a} {A : Set a} → ℕ → List A → List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

drop : ∀ {a} {A : Set a} → ℕ → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
splitAt zero    xs       = ([] , xs)
splitAt (suc n) []       = ([] , [])
splitAt (suc n) (x ∷ xs) with splitAt n xs
... | (ys , zs) = (x ∷ ys , zs)

takeWhile : ∀ {a p} {A : Set a} {P : Pred A p} →
            Decidable P → List A → List A
takeWhile P? []       = []
takeWhile P? (x ∷ xs) with P? x
... | yes _ = x ∷ takeWhile P? xs
... | no  _ = []

dropWhile : ∀ {a p} {A : Set a} {P : Pred A p} →
            Decidable P → List A → List A
dropWhile P? []       = []
dropWhile P? (x ∷ xs) with P? x
... | yes _ = dropWhile P? xs
... | no  _ = x ∷ xs

filter : ∀ {a p} {A : Set a} {P : Pred A p} →
         Decidable P → List A → List A
filter P? [] = []
filter P? (x ∷ xs) with P? x
... | no  _ = filter P? xs
... | yes _ = x ∷ filter P? xs

partition : ∀ {a p} {A : Set a} {P : Pred A p} →
            Decidable P → List A → (List A × List A)
partition P? []       = ([] , [])
partition P? (x ∷ xs) with P? x | partition P? xs
... | yes _ | (ys , zs) = (x ∷ ys , zs)
... | no  _ | (ys , zs) = (ys , x ∷ zs)

span : ∀ {a p} {A : Set a} {P : Pred A p} →
       Decidable P → List A → (List A × List A)
span P? []       = ([] , [])
span P? (x ∷ xs) with P? x
... | yes _ = Prod.map (x ∷_) id (span P? xs)
... | no  _ = ([] , x ∷ xs)

break : ∀ {a p} {A : Set a} {P : Pred A p} →
        Decidable P → List A → (List A × List A)
break P? = span (∁? P?)

------------------------------------------------------------------------
-- Actions on single elements

module _ {a} {A : Set a} where

  infixl 5 _[_]%=_ _[_]∷=_ _─_

  _[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
  []       [ ()    ]%= f
  (x ∷ xs) [ zero  ]%= f = f x ∷ xs
  (x ∷ xs) [ suc k ]%= f = x ∷ (xs [ k ]%= f)

  _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
  xs [ k ]∷= v = xs [ k ]%= const v

  _─_ : (xs : List A) → Fin (length xs) → List A
  []       ─ ()
  (x ∷ xs) ─ zero  = xs
  (x ∷ xs) ─ suc k = x ∷ (xs ─ k)

------------------------------------------------------------------------
-- Operations for reversing lists

module _ {a} {A : Set a} where

  reverseAcc : List A → List A → List A
  reverseAcc = foldl (flip _∷_)

  reverse : List A → List A
  reverse = reverseAcc []

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
xs ∷ʳ x = xs ++ [ x ]

-- Backwards initialisation

infixl 5 _∷ʳ'_

data InitLast {a} {A : Set a} : List A → Set a where
  []    : InitLast []
  _∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)

initLast : ∀ {a} {A : Set a} → (xs : List A) → InitLast xs
initLast []               = []
initLast (x ∷ xs)         with initLast xs
initLast (x ∷ .[])        | []       = [] ∷ʳ' x
initLast (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
--
-- Note that the `boolX` functions are not given warnings as they are
-- used by other deprecated proofs throughout the library.

-- Version 0.15

gfilter = mapMaybe
{-# WARNING_ON_USAGE gfilter
"Warning: gfilter was deprecated in v0.15.
Please use mapMaybe instead."
#-}

boolFilter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
boolFilter p = mapMaybe (λ x → if p x then just x else nothing)

boolPartition : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
boolPartition p []       = ([] , [])
boolPartition p (x ∷ xs) with p x | boolPartition p xs
... | true  | (ys , zs) = (x ∷ ys , zs)
... | false | (ys , zs) = (ys , x ∷ zs)

-- Version 0.16

boolTakeWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
boolTakeWhile p []       = []
boolTakeWhile p (x ∷ xs) with p x
... | true  = x ∷ boolTakeWhile p xs
... | false = []

boolDropWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
boolDropWhile p []       = []
boolDropWhile p (x ∷ xs) with p x
... | true  = boolDropWhile p xs
... | false = x ∷ xs

boolSpan : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
boolSpan p []       = ([] , [])
boolSpan p (x ∷ xs) with p x
... | true  = Prod.map (x ∷_) id (boolSpan p xs)
... | false = ([] , x ∷ xs)

boolBreak : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
boolBreak p = boolSpan (not ∘ p)