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

module F0 where

import Level as L
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Function using (id ; _$_ )

infixr 90 _⊗_
infixr 80 _⊕_
infixr 60 _∘_
infix  30 _⟷_

---------------------------------------------------------------------------
-- Our own version of refl that makes 'a' explicit

data _≡_ {u} {A : Set u} : (a b : A) → Set u where
  refl : (a : A) → (a ≡ a)

-- if we have no occurrences of reciprocals then we can use plain sets; for
-- consistency with the rest of the story we will explicitly add refl paths

-- pi types with no reciprocals

data B : Set where
  ONE   : B
  PLUS  : B → B → B
  TIMES : B → B → B

-- discrete groupoids

record 0-type : Set₁ where
  constructor G₀
  field
    ∣_∣ : Set
  paths : {a : ∣_∣} → (a ≡ a)
  paths {a} = refl a

open 0-type public

plus : 0-type → 0-type → 0-type
plus t₁ t₂ = G₀ (∣ t₁ ∣ ⊎ ∣ t₂ ∣)

times : 0-type → 0-type → 0-type
times t₁ t₂ = G₀ (∣ t₁ ∣ × ∣ t₂ ∣)

-- We interpret types as discrete groupoids

⟦_⟧ : B → 0-type
⟦ ONE ⟧ = G₀ ⊤
⟦ PLUS b₁ b₂ ⟧ = plus ⟦ b₁ ⟧ ⟦ b₂ ⟧
⟦ TIMES b₁ b₂ ⟧ = times ⟦ b₁ ⟧ ⟦ b₂ ⟧

-- isos

data _⟷_ : B → B → Set where
  -- +
  swap₊   : { b₁ b₂ : B } → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  -- *
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  -- congruence
  id⟷   : { b : B } → b ⟷ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _∘_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)

-- interpret isos as functors

record 0-functor (A B : 0-type) : Set where
  constructor F₀
  field
    fobj : ∣ A ∣ → ∣ B ∣
  fmor : {a b : ∣ A ∣} → (a ≡ b) → (fobj a ≡ fobj b)
  fmor {a} {.a} (refl .a) = refl (fobj a)

open 0-functor public

swap⊎ : {A B : Set} → A ⊎ B → B ⊎ A
swap⊎ (inj₁ a) = inj₂ a
swap⊎ (inj₂ b) = inj₁ b

assocl⊎ : {A B C : Set} → A ⊎ (B ⊎ C) → (A ⊎ B) ⊎ C
assocl⊎ (inj₁ x) = inj₁ (inj₁ x)
assocl⊎ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
assocl⊎ (inj₂ (inj₂ y)) = inj₂ y

assocr⊎ : {A B C : Set} → (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
assocr⊎ (inj₁ (inj₁ x)) = inj₁ x
assocr⊎ (inj₁ (inj₂ x)) = inj₂ (inj₁ x)
assocr⊎ (inj₂ y) = inj₂ (inj₂ y)

unite× : {A : Set} → ⊤ × A → A
unite× (tt , x) = x

uniti× : {A : Set} → A → ⊤ × A
uniti× x = (tt , x)

swap× : {A B : Set} → A × B → B × A
swap× (a , b) = (b , a)

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

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

dist×⊎ : {A B C : Set} → (A ⊎ B) × C → (A × C) ⊎ (B × C)
dist×⊎ (inj₁ a , c) = inj₁ (a , c)
dist×⊎ (inj₂ b , c) = inj₂ (b , c)

factor⊎× : {A B C : Set} → (A × C) ⊎ (B × C) → (A ⊎ B) × C
factor⊎× (inj₁ (a , c)) = (inj₁ a , c)
factor⊎× (inj₂ (b , c)) = (inj₂ b , c)

ev⊎ : {A B C D : Set} → (A → C) → (B → D) → A ⊎ B → C ⊎ D
ev⊎ f _ (inj₁ a) = inj₁ (f a)
ev⊎ _ g (inj₂ b) = inj₂ (g b)

ev× : {A B C D : Set} → (A → C) → (B → D) → A × B → C × D
ev× f g (a , b) = (f a , g b)

mutual
       eval : {b₁ b₂ : B} → (b₁ ⟷ b₂) → 0-functor ⟦ b₁ ⟧ ⟦ b₂ ⟧
       eval swap₊ = F₀ swap⊎
       eval assocl₊ = F₀ assocl⊎
       eval assocr₊ = F₀ assocr⊎
       eval unite⋆ = F₀ unite×
       eval uniti⋆ = F₀ uniti×
       eval swap⋆ = F₀ swap×
       eval assocl⋆ = F₀ assocl×
       eval assocr⋆ = F₀ assocr×
       eval dist = F₀ dist×⊎
       eval factor = F₀ factor⊎×
       eval id⟷ = F₀ id
       eval (sym c) = evalB c
       eval (c₁ ∘ c₂) = F₀ (λ x → fobj (eval c₂) (fobj (eval c₁) x))
       eval (c₁ ⊕ c₂) = F₀ (ev⊎ (fobj $ eval c₁) (fobj $ eval c₂))
       eval (c₁ ⊗ c₂) = F₀ (ev× (fobj $ eval c₁) (fobj $ eval c₂))

       evalB : {b₁ b₂ : B} → (b₁ ⟷ b₂) → 0-functor ⟦ b₂ ⟧ ⟦ b₁ ⟧
       evalB swap₊ = F₀ swap⊎
       evalB assocl₊ = F₀ assocr⊎
       evalB assocr₊ = F₀ assocl⊎
       evalB unite⋆ = F₀ uniti×
       evalB uniti⋆ = F₀ unite×
       evalB swap⋆ = F₀ swap×
       evalB assocl⋆ = F₀ assocr×
       evalB assocr⋆ = F₀ assocl×
       evalB dist = F₀ factor⊎×
       evalB factor = F₀ dist×⊎
       evalB id⟷ = F₀ id
       evalB (sym c) = eval c
       evalB (c₁ ∘ c₂) = F₀ (λ x → fobj (evalB c₁) (fobj (evalB c₂) x))
       evalB (c₁ ⊕ c₂) = F₀ (ev⊎ (fobj $ evalB c₁) (fobj $ evalB c₂))
       evalB (c₁ ⊗ c₂) = F₀ (ev× (fobj $ evalB c₁) (fobj $ evalB c₂))

---------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Agda.Primitive

record Order {ℓ} ℓ' (A : Set ℓ) : Set (ℓ ⊔ lsuc ℓ') where
  field
    _≤_ : A → A → Set ℓ'
open Order {{...}} public

data ℕ : Set where
  Zero : ℕ
  Succ : ℕ → ℕ

data _≤ⁿ_ : ℕ → ℕ → Set where
  Zero : ∀ {n} → Zero ≤ⁿ n
  Succ : ∀ {n₁ n₂} → n₁ ≤ⁿ n₂ → Succ n₁ ≤ⁿ Succ n₂

instance
  Order[ℕ] : Order lzero ℕ
  Order[ℕ] = record { _≤_ = _≤ⁿ_ }

subtract : ∀ (n₁ n₂ : ℕ) → n₂ ≤ n₁ → ℕ
subtract   n₁      .Zero      Zero    = n₁
subtract .(Succ _) .(Succ _) (Succ P) = subtract _ _ P

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- Monoidal natural isomorphisms between lax and strong symmetric
-- monoidal functors.
--
-- NOTE. Symmetric monoidal natural isomorphisms are really just
-- monoidal natural isomorphisms that happen to go between symmetric
-- monoidal functors.  No additional conditions are necessary.
-- Nevertheless, the definitions in this module are useful when one is
-- working in a symmetric monoidal setting.  They also help Agda's
-- type checker by bundling the (symmetric monoidal) categories and
-- functors involved.

module Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric
  where

open import Level
open import Relation.Binary using (IsEquivalence)

open import Categories.Category.Monoidal using (SymmetricMonoidalCategory)
import Categories.Functor.Monoidal.Symmetric as BMF
open import Categories.Functor.Monoidal.Properties using () renaming
  ( idF-SymmetricMonoidal to idFˡ  ; idF-StrongSymmetricMonoidal to idFˢ
  ; ∘-SymmetricMonoidal   to _∘Fˡ_ ; ∘-StrongSymmetricMonoidal   to _∘Fˢ_
  )
open import Categories.NaturalTransformation.NaturalIsomorphism as NI
  using (NaturalIsomorphism)
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal as MNI

module Lax where
  open BMF.Lax using (SymmetricMonoidalFunctor)
  open MNI.Lax using (IsMonoidalNaturalIsomorphism)
  open SymmetricMonoidalFunctor using ()
    renaming (F to UF; monoidalFunctor to MF)
  private module U = MNI.Lax

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

    -- Monoidal natural isomorphisms between lax symmetric monoidal functors.

    record SymmetricMonoidalNaturalIsomorphism
           (F G : SymmetricMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

      field
        U              : NaturalIsomorphism (UF F) (UF G)
        F⇒G-isMonoidal : IsMonoidalNaturalIsomorphism (MF F) (MF G) U

      ⌊_⌋ : U.MonoidalNaturalIsomorphism (MF F) (MF G)
      ⌊_⌋ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }

      open U.MonoidalNaturalIsomorphism ⌊_⌋ public hiding (U; F⇒G-isMonoidal)

    infix 4 _≃_

    _≃_ = SymmetricMonoidalNaturalIsomorphism

    -- "Strengthening"

    ⌈_⌉ : {F G : SymmetricMonoidalFunctor C D} →
          U.MonoidalNaturalIsomorphism (MF F) (MF G) → F ≃ G
    ⌈ α ⌉ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }
      where open U.MonoidalNaturalIsomorphism α

    open SymmetricMonoidalNaturalIsomorphism

    -- Identity and compositions

    infixr 9 _ⓘᵥ_

    id : {F : SymmetricMonoidalFunctor C D} → F ≃ F
    id = ⌈ U.id ⌉

    _ⓘᵥ_ : {F G H : SymmetricMonoidalFunctor C D} → G ≃ H → F ≃ G → F ≃ H
    α ⓘᵥ β   = ⌈ ⌊ α ⌋ U.ⓘᵥ ⌊ β ⌋ ⌉

    isEquivalence : IsEquivalence _≃_
    isEquivalence = record
      { refl  = id
      ; sym   = λ α → record
        { U              = NI.sym (U α)
        ; F⇒G-isMonoidal = F⇐G-isMonoidal α
        }
      ; trans = λ α β → β ⓘᵥ α
      }
      where

  open SymmetricMonoidalNaturalIsomorphism

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′}
           {E : SymmetricMonoidalCategory o″ ℓ″ e″} where

    infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

    _ⓘₕ_ : {F G : SymmetricMonoidalFunctor C D}
           {H I : SymmetricMonoidalFunctor D E} →
           H ≃ I → F ≃ G → (H ∘Fˡ F) ≃ (I ∘Fˡ G)
    -- NOTE: this definition is clearly equivalent to
    --
    --   α ⓘₕ β = ⌈ ⌊ α ⌋ U.ⓘₕ ⌊ β ⌋ ⌉
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ⓘₕ β = record
      { U               = C.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = C.ε-compat
        ; ⊗-homo-compat = C.⊗-homo-compat }
        }
      where module C = U.MonoidalNaturalIsomorphism (⌊ α ⌋ U.ⓘₕ ⌊ β ⌋)

    _ⓘˡ_ : {F G : SymmetricMonoidalFunctor C D}
           (H : SymmetricMonoidalFunctor D E) → F ≃ G → (H ∘Fˡ F) ≃ (H ∘Fˡ G)
    H ⓘˡ α = id {F = H} ⓘₕ α

    _ⓘʳ_ : {G H : SymmetricMonoidalFunctor D E} →
           G ≃ H → (F : SymmetricMonoidalFunctor C D) → (G ∘Fˡ F) ≃ (H ∘Fˡ F)
    α ⓘʳ F = α ⓘₕ id {F = F}

  -- Left and right unitors.

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′}
           {F : SymmetricMonoidalFunctor C D} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    unitorˡ : idFˡ D ∘Fˡ F ≃ F
    unitorˡ = record
      { U               = LU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = LU.ε-compat
        ; ⊗-homo-compat = LU.⊗-homo-compat
        }
      }
      where module LU = U.MonoidalNaturalIsomorphism (U.unitorˡ {F = MF F})

    unitorʳ : F ∘Fˡ idFˡ C ≃ F
    unitorʳ = record
      { U               = RU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = RU.ε-compat
        ; ⊗-homo-compat = RU.⊗-homo-compat
        }
      }
      where module RU = U.MonoidalNaturalIsomorphism (U.unitorʳ {F = MF F})

  -- Associator.

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
           {B : SymmetricMonoidalCategory o ℓ e}
           {C : SymmetricMonoidalCategory o′ ℓ′ e′}
           {D : SymmetricMonoidalCategory o″ ℓ″ e″}
           {E : SymmetricMonoidalCategory o‴ ℓ‴ e‴}
           {F : SymmetricMonoidalFunctor B C}
           {G : SymmetricMonoidalFunctor C D}
           {H : SymmetricMonoidalFunctor D E} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    associator : (H ∘Fˡ G) ∘Fˡ F ≃ H ∘Fˡ (G ∘Fˡ F)
    associator = record
      { U               = AU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = AU.ε-compat
        ; ⊗-homo-compat = AU.⊗-homo-compat
        }
      }
      where
        module AU =
          U.MonoidalNaturalIsomorphism (U.associator {F = MF F} {MF G} {MF H})

module Strong where
  open BMF.Strong using (SymmetricMonoidalFunctor)
  open MNI.Strong using (IsMonoidalNaturalIsomorphism)
  open SymmetricMonoidalFunctor using () renaming
    ( F                         to UF
    ; monoidalFunctor           to MF
    ; laxSymmetricMonoidalFunctor to laxBMF
    )
  private module U = MNI.Strong

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

    -- Monoidal natural isomorphisms between strong symmetric monoidal functors.

    record SymmetricMonoidalNaturalIsomorphism
           (F G : SymmetricMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

      field
        U              : NaturalIsomorphism (UF F) (UF G)
        F⇒G-isMonoidal : IsMonoidalNaturalIsomorphism (MF F) (MF G) U

      ⌊_⌋ : U.MonoidalNaturalIsomorphism (MF F) (MF G)
      ⌊_⌋ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }

      laxBNI : Lax.SymmetricMonoidalNaturalIsomorphism (laxBMF F) (laxBMF G)
      laxBNI = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }

      open Lax.SymmetricMonoidalNaturalIsomorphism laxBNI public
        hiding (U; F⇒G-isMonoidal; ⌊_⌋)

    infix 4 _≃_

    _≃_ = SymmetricMonoidalNaturalIsomorphism

    -- "Strengthening"

    ⌈_⌉ : {F G : SymmetricMonoidalFunctor C D} →
          U.MonoidalNaturalIsomorphism (MF F) (MF G) → F ≃ G
    ⌈ α ⌉ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }
      where open U.MonoidalNaturalIsomorphism α

    open SymmetricMonoidalNaturalIsomorphism

    -- Identity and compositions

    infixr 9 _ⓘᵥ_

    id : {F : SymmetricMonoidalFunctor C D} → F ≃ F
    id = ⌈ U.id ⌉

    _ⓘᵥ_ : {F G H : SymmetricMonoidalFunctor C D} → G ≃ H → F ≃ G → F ≃ H
    α ⓘᵥ β   = ⌈ ⌊ α ⌋ U.ⓘᵥ ⌊ β ⌋ ⌉

    isEquivalence : IsEquivalence _≃_
    isEquivalence = record
      { refl  = id
      ; sym   = λ α → record
        { U              = NI.sym (U α)
        ; F⇒G-isMonoidal = F⇐G-isMonoidal α
        }
      ; trans = λ α β → β ⓘᵥ α
      }
      where

  open SymmetricMonoidalNaturalIsomorphism

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′}
           {E : SymmetricMonoidalCategory o″ ℓ″ e″} where

    infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

    _ⓘₕ_ : {F G : SymmetricMonoidalFunctor C D}
           {H I : SymmetricMonoidalFunctor D E} →
           H ≃ I → F ≃ G → (H ∘Fˢ F) ≃ (I ∘Fˢ G)
    -- NOTE: this definition is clearly equivalent to
    --
    --   α ⓘₕ β = ⌈ ⌊ α ⌋ U.ⓘₕ ⌊ β ⌋ ⌉
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ⓘₕ β = record
      { U               = C.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = C.ε-compat
        ; ⊗-homo-compat = C.⊗-homo-compat }
        }
      where module C = U.MonoidalNaturalIsomorphism (⌊ α ⌋ U.ⓘₕ ⌊ β ⌋)

    _ⓘˡ_ : {F G : SymmetricMonoidalFunctor C D}
           (H : SymmetricMonoidalFunctor D E) → F ≃ G → (H ∘Fˢ F) ≃ (H ∘Fˢ G)
    H ⓘˡ α = id {F = H} ⓘₕ α

    _ⓘʳ_ : {G H : SymmetricMonoidalFunctor D E} →
           G ≃ H → (F : SymmetricMonoidalFunctor C D) → (G ∘Fˢ F) ≃ (H ∘Fˢ F)
    α ⓘʳ F = α ⓘₕ id {F = F}

  -- Left and right unitors.

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′}
           {F : SymmetricMonoidalFunctor C D} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    unitorˡ : idFˢ D ∘Fˢ F ≃ F
    unitorˡ = record
      { U               = LU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = LU.ε-compat
        ; ⊗-homo-compat = LU.⊗-homo-compat
        }
      }
      where module LU = U.MonoidalNaturalIsomorphism (U.unitorˡ {F = MF F})

    unitorʳ : F ∘Fˢ idFˢ C ≃ F
    unitorʳ = record
      { U               = RU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = RU.ε-compat
        ; ⊗-homo-compat = RU.⊗-homo-compat
        }
      }
      where module RU = U.MonoidalNaturalIsomorphism (U.unitorʳ {F = MF F})

  -- Associator.

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
           {B : SymmetricMonoidalCategory o ℓ e}
           {C : SymmetricMonoidalCategory o′ ℓ′ e′}
           {D : SymmetricMonoidalCategory o″ ℓ″ e″}
           {E : SymmetricMonoidalCategory o‴ ℓ‴ e‴}
           {F : SymmetricMonoidalFunctor B C}
           {G : SymmetricMonoidalFunctor C D}
           {H : SymmetricMonoidalFunctor D E} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    associator : (H ∘Fˢ G) ∘Fˢ F ≃ H ∘Fˢ (G ∘Fˢ F)
    associator = record
      { U               = AU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = AU.ε-compat
        ; ⊗-homo-compat = AU.⊗-homo-compat
        }
      }
      where
        module AU =
          U.MonoidalNaturalIsomorphism (U.associator {F = MF F} {MF G} {MF H})


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

open import HoTT

module homotopy.S1SuspensionS0 where

{- To -}

module To = S¹Rec (north Bool) (merid _ true ∙ ! (merid _ false))

to : S¹ → Suspension Bool
to = To.f

{- From -}

from-merid : Bool → base == base
from-merid true = loop
from-merid false = idp

module From = SuspensionRec Bool base base from-merid

from : Suspension Bool → S¹
from = From.f

{- ToFrom and FromTo -}

module _ {i}  {A : Type i} where
  ∙idp∙ : {x y z : A} (p : x == y) (q : y == z) → p ∙ idp ∙ q == p ∙ q
  ∙idp∙ idp idp = idp
  p∙!q∙q : {x y z : A} (p : x == y) (q : z == y) → p ∙ ( ! q ∙ q)  == p
  p∙!q∙q idp idp = idp
  !-∙∙ :  {x y z w : A} (p : x == y) (q : y == z) (r : x == w) →  ! (p ∙ q) ∙ r == (! q ∙ ! p ) ∙ r
  !-∙∙ idp idp idp = idp
  !-coh : {x y : A} {p p' : x == y} → p == p' → ! p == ! p'
  !-coh idp = idp
  add-idp-r : {x y : A} → (p : x == y) → p == p ∙ idp
  add-idp-r idp = idp

ap-coh : ∀ {i j} {A : Type i} {B : Type j} {x y : A} → (f : A → B) → {p p' : x == y} → p == p' → ap f p == ap f p'
ap-coh f idp = idp
_∋_ : ∀ {i} (A : Type i) → A → A
A ∋ x = x

mt : north Bool == south Bool
mt = merid Bool true

mf : north Bool == south Bool
mf = merid Bool false

to-from-merid-t' :  ( ! (ap to (ap from mt))) ∙ idp ∙ mt ==  mf
to-from-merid-t' =  ! (ap to (ap from mt)) ∙ idp ∙ mt         =⟨ ∙idp∙ ( ! (ap to (ap from mt)))  mt  ⟩
                    ! (ap to (ap from mt)) ∙ mt               =⟨ (!-coh (ap-coh to (From.glue-β true))) ∙ᵣ mt ⟩
                    ! (ap to loop) ∙ mt                       =⟨ (!-coh (To.loop-β)) ∙ᵣ mt ⟩
                    (! (mt ∙ ! mf)) ∙ mt                      =⟨ !-∙∙ mt (! mf) mt ⟩
                    ((! (! mf)) ∙ ! mt) ∙ mt                  =⟨ ((!-! mf) ∙ᵣ (! mt)) ∙ᵣ mt ⟩
                    (mf ∙ ! mt) ∙ mt                          =⟨ ∙-assoc mf (! mt) mt  ⟩
                    mf ∙ (! mt ∙ mt)                          =⟨ p∙!q∙q mf mt ⟩
                    mf ∎

to-from-merid-f' :  ( ! (ap to (ap from mf))) ∙ idp ∙ mf ==  mf
to-from-merid-f' =  ! (ap to (ap from mf)) ∙ idp ∙ mf        =⟨ ∙idp∙ ( ! (ap to (ap from mf))) mf ⟩
                    ! (ap to (ap from mf)) ∙ mf              =⟨ (!-coh (ap-coh to (From.glue-β false))) ∙ᵣ mf ⟩
                    mf ∎

-- to-from-merid' : (b : Bool) → ( ! (ap to (ap from (merid Bool b)))) ∙ idp ∙ mf ==  (merid Bool b)
-- to-from-merid' false = to-from-merid-f'
-- to-from-merid' true = to-from-merid-t'

to-from : (x : Suspension Bool) → to (from x) == x
to-from = ToFrom.f
  where
    Q : Suspension Bool → Set lzero
    Q x = to (from x) == x

    n : to (from (north Bool)) == north Bool
    n = idp

    s : to (from (south Bool)) == south Bool
    s = mf

    lemma : {x y : Suspension Bool} → (q : x == y) → (α : to (from x) == x) → transport Q q α == (! (ap to (ap from q))) ∙ α ∙ q
    lemma idp α = add-idp-r α

    p : (b : Bool) → n == s [ Q ↓ merid Bool b ]
    p true = from-transp Q mt ((lemma mt n) ∙ to-from-merid-t')
    p false = from-transp Q mf ((lemma mf n) ∙ to-from-merid-f')

    module ToFrom = SuspensionElim Bool {P = Q} n s p

from-to-loop' : (! (ap from (ap to loop))) ∙ idp ∙ loop == idp
from-to-loop' = ! (ap from (ap to loop)) ∙ idp ∙ loop         =⟨ ∙idp∙ (! (ap from (ap to loop)))  loop  ⟩
                ! (ap from (ap to loop)) ∙ loop               =⟨ (!-coh (ap-coh from To.loop-β)) ∙ᵣ loop ⟩
                ! (ap from (mt ∙ ! mf)) ∙ loop                =⟨ (!-coh (ap-∙ from mt (! mf))) ∙ᵣ loop  ⟩
                (! ((ap from mt) ∙ (ap from (! mf)))) ∙ loop  =⟨ (!-coh ( (From.glue-β true) ∙ᵣ (ap from (! mf)))) ∙ᵣ loop  ⟩
                ! (loop ∙ (ap from (! mf))) ∙ loop            =⟨ !-coh (loop ∙ₗ ap-! from mf) ∙ᵣ loop ⟩
                ! (loop ∙ ! (ap from mf)) ∙ loop              =⟨ !-coh (loop ∙ₗ (!-coh (From.glue-β false))) ∙ᵣ loop ⟩
                ! (loop ∙ ! idp) ∙ loop                       =⟨ !-∙∙ loop (! idp) loop ⟩
                (! loop) ∙ loop                               =⟨ !-inv-l loop ⟩
                idp ∎

from-to : (x : S¹) → from (to x) == x
from-to = FromTo.f
  where
    Q : S¹ → Type lzero
    Q x = from (to x) == x

    b : Q base
    b = idp

    lemma : {x y : S¹} → (q : x == y) → (α : from (to x) == x) → transport Q q α == (! (ap from (ap to q))) ∙ α ∙ q
    lemma idp α = add-idp-r α

    l : b == b [ Q ↓ loop ]
    l = from-transp Q loop ((lemma loop b) ∙ from-to-loop')

    module FromTo = S¹Elim {P = Q} b l

e : S¹ ≃ Suspension Bool
e = equiv to from to-from from-to

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: UlrikBuchholtz/HoTT-Agda

max_forks_repo_name: UlrikBuchholtz/HoTT-Agda


text:
module Prelude.Bytes where

open import Prelude.Bool
open import Prelude.Decidable
open import Prelude.Equality
open import Prelude.Equality.Unsafe

{-# FOREIGN GHC import qualified Data.ByteString as B #-}

postulate
  Bytes : Set
{-# COMPILE GHC Bytes = type B.ByteString #-}

private
  module Internal where
    postulate
      empty : Bytes
      append : Bytes → Bytes → Bytes
    {-# COMPILE GHC empty  = B.empty #-}
    {-# COMPILE GHC append = B.append #-}

-- Eq --

private
  postulate eqBytes : Bytes → Bytes → Bool
  {-# COMPILE GHC eqBytes = (==) #-}

instance
  EqBytes : Eq Bytes
  _==_ {{EqBytes}} x y with eqBytes x y
  ... | true = yes unsafeEqual
  ... | false = no unsafeNotEqual

-- Monoid --

instance
  open import Prelude.Monoid
  MonoidBytes : Monoid Bytes
  mempty {{MonoidBytes}} = Internal.empty
  _<>_   {{MonoidBytes}} = Internal.append

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
open import Prelude

open import Relation.Binary.PropositionalEquality
open import RW.Language.RTerm using (Name)
open import RW.Strategy.PropEq
open import RW.RW (≡-strat ∷ [])

open import Data.Nat.Properties.Simple
  using (+-comm; +-right-identity; +-assoc)

module PropEqTest where

    ++-assoc : ∀{a}{A : Set a}(xs ys zs : List A) →
               (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
    ++-assoc [] ys zs       = refl
    ++-assoc (x ∷ xs) ys zs = tactic (by (quote ++-assoc))

    open ≡-Reasoning

    ++-assocH : ∀{a}{A : Set a}(xs ys zs : List A) →
                (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
    ++-assocH [] ys zs =
              begin
                ([] ++ ys) ++ zs
              ≡⟨ refl ⟩
                ys ++ zs
              ≡⟨ refl ⟩
                [] ++ (ys ++ zs)
              ∎
    ++-assocH {A = A} (x ∷ xs) ys zs =
              begin
                ((x ∷ xs) ++ ys) ++ zs
              ≡⟨ refl ⟩
                x ∷ (xs ++ ys) ++ zs
              ≡⟨ refl ⟩
                x ∷ ((xs ++ ys) ++ zs)
              ≡⟨ (tactic (by (quote ++-assocH))) ⟩
                x ∷ (xs ++ (ys ++ zs))
              ≡⟨ refl ⟩
                (x ∷ xs) ++ (ys ++ zs)
              ∎

    []-++-neutral : ∀{a}{A : Set a}(xs : List A)
                  → xs ++ [] ≡ xs
    []-++-neutral [] = refl
    []-++-neutral (x ∷ xs) = tactic (by (quote []-++-neutral))

    test1 : (x y : ℕ) → (x + y) + 0 ≡ y + (x + 0)
    test1 x y
      = begin
        (x + y) + 0
      ≡⟨ (tactic (by+ acts)) ⟩
        x + y
      ≡⟨ (tactic (by+ acts)) ⟩
        y + x
      ≡⟨ (tactic (by+ acts)) ⟩
        (y + x) + 0
      ≡⟨ (tactic (by+ acts)) ⟩
        y + (x + 0)
      ∎
      where
        acts : List Name
        acts = quote +-right-identity ∷ quote +-assoc ∷ quote +-comm ∷ []

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
module split where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n; _≤?_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)

open import lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_]; All; Decidable)

-- リストのマージ
-- xs と ys を使って zs を組み立てる
data merge {A : Set} : (xs ys zs : List A) → Set where
  [] :
      --------------
      merge [] [] []

  left-∷ : ∀ {x xs ys zs}
    → merge xs ys zs
      --------------------------
    → merge (x ∷ xs) ys (x ∷ zs)

  right-∷ : ∀ {y xs ys zs}
    → merge xs ys zs
      --------------------------
    → merge xs (y ∷ ys) (y ∷ zs)

_ : merge [ 1 , 4 ] [ 2 , 3 ] [ 1 , 2 , 3 , 4 ]
_ = left-∷ (right-∷ (right-∷ (left-∷ [])))

-- リストの分割
-- 述語Pが成り立つ場合はxs、そうでない場合はysとして分割する (scalaでいうpartition)
split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
  → ∃[ xs ] ∃[ ys ] (merge xs ys zs × All P xs × All (¬_ ∘ P) ys)
split P? []                                                                 = ⟨ [] ,     ⟨ [] ,     ⟨ [] ,        ⟨ [] ,       [] ⟩ ⟩ ⟩ ⟩
split P? (z ∷ zs) with P? z   | split P? zs
...                  | yes Pz | ⟨ xs , ⟨ ys , ⟨ m , ⟨ Pxs , ¬Pys  ⟩  ⟩  ⟩ ⟩ = ⟨ z ∷ xs , ⟨ ys ,     ⟨ left-∷ m ,  ⟨ Pz ∷ Pxs , ¬Pys ⟩ ⟩ ⟩ ⟩
...                  | no ¬Pz | ⟨ xs , ⟨ ys , ⟨ m , ⟨ Pxs , ¬Pys  ⟩  ⟩  ⟩ ⟩ = ⟨ xs ,     ⟨ z ∷ ys , ⟨ right-∷ m , ⟨ Pxs ,      ¬Pz ∷ ¬Pys ⟩ ⟩ ⟩ ⟩

-- 0と等しい1以上の自然数は存在しない
¬z≡n : ∀ {n : ℕ} → ¬ (zero ≡ suc n)
¬z≡n ()

-- m = n が成り立たなければ (m + 1) = (n + 1) も成り立たない
¬s≡s : ∀ {m n : ℕ} → ¬ (m ≡ n) → ¬ (suc m ≡ suc n)
¬s≡s ¬m≡n refl = ¬m≡n refl

-- decidableを使った、2つの自然数が等しいかどうか判定する関数
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero  ≡ℕ? zero                = yes refl
zero  ≡ℕ? suc n               = no ¬z≡n
suc m ≡ℕ? zero                = no (λ ())
suc m ≡ℕ? suc n with m ≡ℕ? n
...                | yes refl = yes refl
...                | no ¬m≡n  = no (¬s≡s ¬m≡n)

-- テスト
-- リストの要素を3とそれ以外とに分ける
_ : split (_≡ℕ? 3) [ 3 , 0 , 3 , 1 ]
  ≡ ⟨ [ 3 , 3 ] , ⟨ [ 0 , 1 ] , ⟨ (left-∷ (right-∷ (left-∷ (right-∷ [])))) , ⟨ refl ∷ refl ∷ [] , ¬z≡n ∷ (¬s≡s ¬z≡n) ∷ [] ⟩ ⟩ ⟩ ⟩
_ = refl

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------
-- A proof of univalence for an arbitrary "equality with J"
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

import Equality.Path as P

module Equality.Path.Isomorphisms.Univalence
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

import Equality.Path.Univalence as PU
open import Prelude

open import Equivalence equality-with-J
open import Univalence-axiom equality-with-J
open import Equality.Path.Isomorphisms eq

private
  variable
    ℓ : Level

-- Univalence.

univ : Univalence ℓ
univ = _≃_.from Univalence≃Univalence PU.univ

-- A variant of univ that does not compute at compile-time.

abstract

  abstract-univ : Univalence ℓ
  abstract-univ = univ

-- Propositional extensionality.

prop-ext : Propositional-extensionality ℓ
prop-ext =
  _≃_.from
    (Propositional-extensionality-is-univalence-for-propositions ext)
    (λ _ _ → univ)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

-- Let's have a closer look at the module system

module Modules where

{-

  Importing and opening modules

-}

-- You can import a module defined in a different file.
import Nat

-- This will bring the module into scope and allows you to
-- access its contents using qualified names.
plusTwo : Nat.Nat -> Nat.Nat
plusTwo n = Nat._+_ n 2

-- To bring everything from a module into scope you can open
-- the module.
open Nat

z : Nat
z = zero

-- There's also a short-hand to import and open at the same time
open import Bool

_&&_ : Bool -> Bool -> Bool
x && y = if x then y else false

-- Sometimes it's nice to be able to control what is brought
-- into scope when you open a module. There are three modifiers
-- that affect this: using, hiding and renaming.

module DifferentWaysOfOpeningNat where

  -- nothing but Nat
  open Nat using (Nat)

  -- everything but zero
  open Nat hiding (zero)

  -- everything, but zero and suc under different names
  open Nat renaming (zero to ZZ; suc to S_S)

  two : Nat
  two = S S zero S S

  -- you can combine using or hiding with renaming, but not using
  -- with hiding (for obvious reasons).

-- To re-export something opened use the public modifier.
module A where
  open Nat public using (Nat)

N = A.Nat -- now Nat is a visible name in module A

{-

  Parameterised modules

-}

-- A very useful feature is parameterised modules.

data Vec (A : Set) : Nat -> Set where
  []   : Vec A 0
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

infixr 40 _::_

module Sort {A : Set}(_≤_ : A -> A -> Bool) where

  insert : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
  insert x [] = x :: []
  insert x (y :: ys) = if x ≤ y
                       then x :: y :: ys
                       else y :: insert x ys

  sort : {n : Nat} -> Vec A n -> Vec A n
  sort []        = []
  sort (x :: xs) = insert x (sort xs)

_≤_ : Nat -> Nat -> Bool
zero  ≤ m     = true
suc n ≤ zero  = false
suc n ≤ suc m = n ≤ m

-- When used directly, functions from parameterised modules
-- take the parameters as extra arguments.
test = Sort.sort _≤_ (6 :: 2 :: 0 :: 4 :: [])

-- But, you can also apply the entire module to its arguments.
-- Let's open the new module while we're at it.
open module SortNat = Sort _≤_

test' = sort (3 :: 2 :: 4 :: 0 :: [])

{-

  Local definitions

-}

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

subst : {A : Set}(C : A -> Set){x y : A} -> x == y -> C x -> C y
subst C refl cx = cx

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

lem₁ : (n : Nat) -> n + 0 == n
lem₁ zero    = refl
lem₁ (suc n) = cong suc (lem₁ n)

lem₂ : (n m : Nat) -> n + suc m == suc n + m
lem₂ n  zero   = refl
lem₂ n (suc m) = cong suc (lem₂ n m)

{-

  What's next?

-}

-- The final thing on the agenda is records.

-- Move on to: Records.agda


text:
-- The point of this test is to check that we don't create needlessly
-- large anonymous modules when we open a module application.

{-# OPTIONS -vscope.mod.inst:10 -vtc.section.apply:20 #-}

module Optimised-open where

postulate A : Set

module M₁ (A : Set) where
  postulate
    P : A → Set
    X : Set

-- There is no point in creating a module containing X here.
open M₁ A using (P)

postulate
  a : A
  p : P a

module M₂ where

  -- Or here.
  open M₁ A public using () renaming (P to P′)

  postulate
    p′ : P′ a

open M₂

-- Make sure that we get a type error.
postulate
  x : P P


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

module Categories.Category.Instance.Quivers where

-- The Category of Quivers

open import Level using (Level; suc; _⊔_)
open import Relation.Binary.PropositionalEquality.Core using (refl)
open import Data.Quiver using (Quiver)
open import Data.Quiver.Morphism using (Morphism; id; _∘_; _≃_; ≃-Equivalence; ≃-resp-∘)

open import Categories.Category.Core using (Category)

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

Quivers : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Quivers o ℓ e = record
  { Obj       = Quiver o ℓ e
  ; _⇒_       = Morphism
  ; _≈_       = _≃_
  ; id        = id
  ; _∘_       = _∘_
  ; assoc     = λ {_ _ _ G} → record { F₀≡ = refl ; F₁≡ = Equiv.refl G }
  ; sym-assoc = λ {_ _ _ G} → record { F₀≡ = refl ; F₁≡ = Equiv.refl G }
  ; identityˡ = λ {_ G}     → record { F₀≡ = refl ; F₁≡ = Equiv.refl G }
  ; identityʳ = λ {_ G}     → record { F₀≡ = refl ; F₁≡ = Equiv.refl G }
  ; identity² = λ {G}       → record { F₀≡ = refl ; F₁≡ = Equiv.refl G }
  ; equiv     = ≃-Equivalence
  ; ∘-resp-≈  = ≃-resp-∘
  }
  where open Quiver using (module Equiv)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2018-10-16, runtime erasure

id : (@0 A : Set) (@0 x : A) → A
id A x = x

-- Expected error:
--
-- Variable x is declared erased, so it cannot be used here
-- when checking that the expression x has type A


text:
module Numeral.Natural.Induction{ℓ} where

open import Logic
open import Logic.Propositional
open import Functional
open import Numeral.Natural

-- The induction proof method on natural numbers
-- TODO: There seems to be a problem making i implicit with unsolved metas.
-- TODO: Maybe rename to elim because this is the elimination rule for ℕ
ℕ-elim : ∀{T : ℕ → Stmt{ℓ}} → T(𝟎) → ((i : ℕ) → T(i) → T(𝐒(i))) → ((n : ℕ) → T(n))
ℕ-elim {T} base step 𝟎      = base
ℕ-elim {T} base step (𝐒(n)) = step n (ℕ-elim {T} base step n)

[ℕ]-induction : ∀{φ : ℕ → Stmt{ℓ}} → φ(𝟎) → (∀(i : ℕ) → φ(i) → φ(𝐒(i))) → (∀{n} → φ(n))
[ℕ]-induction {φ} base step {n} = ℕ-elim {φ} base step n

[ℕ]-inductionᵢ : ∀{φ : ℕ → Stmt{ℓ}} → φ(𝟎) → (∀{i : ℕ} → φ(i) → φ(𝐒(i))) → (∀{n} → φ(n))
[ℕ]-inductionᵢ {φ} base step = [ℕ]-induction {φ} base (i ↦ step{i})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Common.PredicateBasedContext where

open import Common.Predicate public

-- Predicate-based context membership.

module _ {U : Set} where
  infix 3 _∈_
  _∈_ : U → Pred (Cx U)
  A ∈ Γ = Any (_≡ A) Γ

  infix 3 _∉_
  _∉_ : U → Pred (Cx U)
  A ∉ Γ = Not (A ∈ Γ)

  lookup : ∀ {Γ P} → All P Γ → (∀ {A} → A ∈ Γ → P A)
  -- Alternatively:
  -- lookup : ∀ {Γ P} → All P Γ → (_∈ Γ) ⊆ᴾ P
  lookup ∅       ()
  lookup (γ , a) (top refl) = a
  lookup (γ , a) (pop i)    = lookup γ i

  tabulate : ∀ {Γ P} → (∀ {A} → A ∈ Γ → P A) → All P Γ
  -- Alternatively:
  -- tabulate : ∀ {Γ P} → (_∈ Γ) ⊆ᴾ P → All P Γ
  tabulate {∅}     f = ∅
  tabulate {Γ , A} f = tabulate (f ∘ pop) , f (top refl)

  bot∈ : ∀ {A} → A ∉ ∅
  bot∈ ()

  [_]ᴵˣ : ∀ {A Γ} → A ∈ Γ → ℕ
  [ top refl ]ᴵˣ = zero
  [ pop i ]ᴵˣ    = suc [ i ]ᴵˣ

  i₀ : ∀ {A Γ} → A ∈ Γ , A
  i₀ = top refl

  i₁ : ∀ {A B Γ} → A ∈ Γ , A , B
  i₁ = pop i₀

  i₂ : ∀ {A B C Γ} → A ∈ Γ , A , B , C
  i₂ = pop i₁

-- Predicate-based context inclusion.

module _ {U : Set} where
  -- NOTE: This is similar to Ren from Conor’s fish-and-chips development.
  infix 3 _⊆_
  _⊆_ : Cx U → Pred (Cx U)
  Γ ⊆ Γ′ = ∀ {A} → A ∈ Γ → A ∈ Γ′
  -- Alternatively:
  -- Γ ⊆ Γ′ = (_∈ Γ) ⊆ᴾ (_∈ Γ′)

  infix 3 _⊈_
  _⊈_ : Cx U → Pred (Cx U)
  Γ ⊈ Γ′ = Not (Γ ⊆ Γ′)

  skip⊆ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
  skip⊆ η = pop ∘ η

  -- NOTE: This is similar to wkr from Conor’s fish-and-chips development.
  keep⊆ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A
  keep⊆ η (top refl) = top refl
  keep⊆ η (pop i)    = pop (η i)

  refl⊆ : ∀ {Γ} → Γ ⊆ Γ
  refl⊆ {Γ} = refl⊆ᴾ {P = _∈ Γ}

  trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
  trans⊆ {Γ} η η′ = trans⊆ᴾ {P = _∈ Γ} η η′

  unskip⊆ : ∀ {A Γ Γ′} → Γ , A ⊆ Γ′ → Γ ⊆ Γ′
  unskip⊆ η = η ∘ pop

  -- NOTE: This doesn’t seem possible.
  -- unkeep⊆ : ∀ {A Γ Γ′} → Γ , A ⊆ Γ′ , A → Γ ⊆ Γ′

  weak⊆ : ∀ {A Γ} → Γ ⊆ Γ , A
  weak⊆ = pop

  bot⊆ : ∀ {Γ} → ∅  ⊆ Γ
  bot⊆ ()

-- Predicate-based context equality.

module _ {U : Set} where
  infix 3 _⫗_
  _⫗_ : Cx U → Pred (Cx U)
  Γ ⫗ Γ′ = (Γ ⊆ Γ′) × (Γ′ ⊆ Γ)

  infix 3 _⫘_
  _⫘_ : Cx U → Pred (Cx U)
  Γ ⫘ Γ′ = Not (Γ ⫗ Γ′)

  refl⫗ : ∀ {Γ} → Γ ⫗ Γ
  refl⫗ {Γ} = refl⫗ᴾ {P = _∈ Γ}

  trans⫗ : ∀ {Γ Γ′ Γ″} → Γ ⫗ Γ′ → Γ′ ⫗ Γ″ → Γ ⫗ Γ″
  trans⫗ {Γ} σ σ′ = trans⫗ᴾ {P = _∈ Γ} σ σ′

  sym⫗ : ∀ {Γ Γ′} → Γ ⫗ Γ′ → Γ′ ⫗ Γ
  sym⫗ {Γ} σ = sym⫗ᴾ {P = _∈ Γ} σ

  antisym⊆ : ∀ {Γ Γ′} → ((Γ ⊆ Γ′) × (Γ′ ⊆ Γ)) ≡ (Γ ⫗ Γ′)
  antisym⊆ {Γ} = antisym⊆ᴾ {P = _∈ Γ}

-- Monotonicity with respect to predicate-based context inclusion.

module _ {U : Set} where
  mono∈ : ∀ {A : U} {Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
  mono∈ η i = η i

  reflmono∈ : ∀ {A Γ} → (i : A ∈ Γ) → i ≡ mono∈ refl⊆ i
  reflmono∈ i = refl

  transmono∈ : ∀ {A Γ Γ′ Γ″} → (η : Γ ⊆ Γ′) (η′ : Γ′ ⊆ Γ″) (i : A ∈ Γ)
               → mono∈ η′ (mono∈ η i) ≡ mono∈ (trans⊆ η η′) i
  transmono∈ η η′ i = refl

-- Predicate-based context concatenation.

module _ {U : Set} where
  _⧺_ : Cx U → Cx U → Cx U
  Γ ⧺ ∅        = Γ
  Γ ⧺ (Γ′ , A) = (Γ ⧺ Γ′) , A

  id⧺₁ : ∀ {Γ} → Γ ⧺ ∅ ≡ Γ
  id⧺₁ = refl

  id⧺₂ : ∀ {Γ} → ∅  ⧺ Γ ≡ Γ
  id⧺₂ {∅}     = refl
  id⧺₂ {Γ , A} = cong² _,_ id⧺₂ refl

  weak⊆⧺₁ : ∀ {Γ} Γ′ → Γ ⊆ Γ ⧺ Γ′
  weak⊆⧺₁ ∅        = refl⊆
  weak⊆⧺₁ (Γ′ , A) = skip⊆ (weak⊆⧺₁ Γ′)

  weak⊆⧺₂ : ∀ {Γ Γ′} → Γ′ ⊆ Γ ⧺ Γ′
  weak⊆⧺₂ {Γ} {∅}      = bot⊆
  weak⊆⧺₂ {Γ} {Γ′ , A} = keep⊆ weak⊆⧺₂

-- Predicate-based context thinning.

module _ {U : Set} where
  _-_ : ∀ {A} → (Γ : Cx U) → A ∈ Γ → Cx U
  ∅       - ()
  (Γ , A) - top refl = Γ
  (Γ , B) - pop i    = (Γ - i) , B

  thin⊆ : ∀ {A Γ} → (i : A ∈ Γ) → Γ - i ⊆ Γ
  thin⊆ (top refl) = pop
  thin⊆ (pop i)    = keep⊆ (thin⊆ i)

-- Decidable predicate-based context membership equality.

module _ {U : Set} where
  data _=∈_ {A : U} {Γ} (i : A ∈ Γ) : ∀ {C} → Pred (C ∈ Γ) where
    same : i =∈ i
    diff : ∀ {C} → (j : C ∈ Γ - i) → i =∈ mono∈ (thin⊆ i) j

  _≟∈_ : ∀ {A C Γ} → (i : A ∈ Γ) (j : C ∈ Γ) → i =∈ j
  top refl ≟∈ top refl = same
  top refl ≟∈ pop j    = diff j
  pop i    ≟∈ top refl = diff (top refl)
  pop i    ≟∈ pop j    with i ≟∈ j
  pop i ≟∈ pop .i      | same = same
  pop i ≟∈ pop ._      | diff j = diff (pop j)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
open import ExtractSac as ES using ()
open import Extract (ES.kompile-fun)

open import Data.Nat as N using (ℕ; zero; suc; _≤_; _≥_; _<_; s≤s; z≤n)
import      Data.Nat.DivMod as N
open import Data.Nat.Properties as N
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
import      Data.Vec.Properties as V
open import Data.Fin using (Fin; zero; suc; #_)
open import Data.Product as Prod using (Σ; _,_; curry; uncurry) renaming (_×_ to _⊗_)

open import Relation.Binary.PropositionalEquality

open import Reflection

open import Structures
open import Function

open import Array.Base
open import Array.Properties

open import APL2

open import Agda.Builtin.Float

v→a : ∀ {a}{X : Set a}{n} → Vec X n → Ar X 1 (n ∷ [])
v→a s = imap (λ iv → V.lookup s $ ix-lookup iv zero )

a→v : ∀ {a}{X : Set a}{s} → Ar X 1 (s ∷ []) → Vec X s
a→v (imap x) = V.tabulate λ i → x (i ∷ [])

-- blog←{⍺×⍵×1-⍵}
blog : ∀ {n s} → Ar Float n s → Ar Float n s → Ar Float n s
blog α ω = α ×ᵣ ω ×ᵣ 1.0 -ᵣ ω

test-blog = a→v $ blog (v→a $ 3.0 ∷ 4.0 ∷ []) (v→a $ 5.0 ∷ 6.0 ∷ [])

kblog = kompile blog [] []
test₃₆ : kblog ≡ ok _
test₃₆ = refl

-- backbias←{+/,⍵}
backbias : ∀ {n s} → Ar Float n s → Scal Float
backbias ω = --(▾_ ∘₂ _+ᵣ_) / , ω
             _+ᵣ′_ / , ω
  where
    --_+ᵣ′_ : Float → Float → Float
    --a +ᵣ′ b = ▾ (a +ᵣ b)

    _+ᵣ′_ = primFloatPlus

kbackbias = kompile backbias (quote prod ∷ []) (quote prod ∷ quote off→idx ∷ quote reduce-custom.reduce-1d ∷ [])
--test₃₇ : kbackbias ≡ ok _
--test₃₇ = refl

-- logistic←{÷1+*-⍵}
logistic : ∀ {n s} → Ar Float n s → Ar Float n s
logistic ω = ÷ᵣ 1.0 +ᵣ *ᵣ -ᵣ ω

klogistic = kompile logistic [] []
test₃₈ : klogistic ≡ ok _
test₃₈ = refl

-- meansqerr←{÷∘2+/,(⍺-⍵)*2}
meansqerr : ∀ {n s} → Ar Float n s → Ar Float n s → Scal Float
meansqerr α ω = _÷ᵣ 2.0 $ _+ᵣ′_ / , (α +ᵣ ω) ×ᵣ (α -ᵣ ω)
  where
    _+ᵣ′_ = primFloatPlus

kmeansqerr = kompile meansqerr (quote prod ∷ []) (quote prod ∷ quote off→idx ∷ quote reduce-custom.reduce-1d ∷ [])
test₃₉ : klogistic ≡ ok _
test₃₉ = refl

-- backavgpool←{2⌿2/⍵÷4}⍤2
backavgpool : ∀ {s} → Ar Float 2 s → Ar Float 2 $ ▾ (2 × s)
backavgpool {s = _ ∷ _ ∷ []} ω = 2 /ᵣ′ 2 ⌿ᵣ ω ×ᵣ 4.0
  where
    infixr 20 _/ᵣ′_
    _/ᵣ′_ = _/ᵣ_ {s = _ ∷ []}

kbackavgpool = kompile backavgpool [] []
test₄₀ : kbackavgpool ≡ ok _
test₄₀ = refl

-- Something that could go in Stdlib.
≡⇒≤ : ∀ {a b} → a ≡ b → a N.≤ b
≡⇒≤ refl = ≤-refl

-- This should be perfectly generaliseable --- instead of 2
-- we can use any m>0
a<b⇒k<2⇒a*2+k<b*2 : ∀ {a b k} → a N.< b → k N.< 2 → a N.* 2 N.+ k N.< b N.* 2
a<b⇒k<2⇒a*2+k<b*2 {a} {b} {zero} a<b k<2
                  rewrite (+-identityʳ (a N.* 2))
                        | (*-comm a 2)
                        | (*-comm b 2) = *-monoʳ-< 1 a<b
a<b⇒k<2⇒a*2+k<b*2 {a} {b} {suc zero} a<b k<2 = ≤-trans (N.s≤s (≡⇒≤ (+-comm _ 1)))
                                                        (*-monoˡ-≤ 2 a<b)
a<b⇒k<2⇒a*2+k<b*2 {a} {b} {suc (suc k)} a<b (N.s≤s (N.s≤s ()))

A<B⇒K<2⇒A*2+K<B*2 : ∀ {n s}{a b k : Ar ℕ n s} → a <a b → k <a (cst 2) → ((a × 2) + k) <a (b × 2)
A<B⇒K<2⇒A*2+K<B*2 {a = imap a} {imap b} {imap k} a<b k<2 = λ iv → a<b⇒k<2⇒a*2+k<b*2 (a<b iv) (k<2 iv)

avgpool : ∀ {s}
        → Ar Float 2 $ ▾ (s × 2)
        → Ar Float 2 s
avgpool {s} (imap p) = imap body
  where
    body : _ → _
    body iv = ▾ (_÷ᵣ 4.0 $ _+ᵣ′_ / , f ̈ ι [2,2])
      where
         [2,2] = cst {s = 2 ∷ []} 2
         f : _ → _
         f (i , pf) = let ix , ix<s = ix→a iv in
                      p $ a→ix ((ix × 2) + i) (s × 2) $ A<B⇒K<2⇒A*2+K<B*2 ix<s pf
         _+ᵣ′_ = primFloatPlus

kavgpool = kompile avgpool [] []

open import ReflHelper
fin-id : ∀ {n} → Fin n → Fin n
fin-id x = x

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
module Structure.Relator.Ordering.Proofs where

import      Lvl
open import Functional
open import Lang.Instance
open import Logic
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

private variable ℓ : Lvl.Level
private variable A B : Type{ℓ}
private variable _≤_ _≤₁_ _≤₂_ : A → A → Stmt{ℓ}
private variable f : A → B
private variable x : A

module _ ⦃ trans : Transitivity{T = B}(_≤_) ⦄ where
  open Strict.Properties

  -- TODO: Agda bug 20200523 does not allow instance arg
  accessibleₗ-image-by-trans : Accessibleₗ{T = B}(_≤_)(f(x)) → Accessibleₗ((_≤_) on₂ f)(x)
  accessibleₗ-image-by-trans {f = f} {y} (intro ⦃ acc ⦄) = intro ⦃ \{x} ⦃ xy ⦄ → intro ⦃ \{a} ⦃ ax ⦄ → accessibleₗ-image-by-trans (acc {f(a)} ⦃ transitivity(_≤_) ax xy ⦄ ) ⦄ ⦄

  wellfounded-image-by-trans : ∀{f : A → B} → ⦃ _ : WellFounded{T = B}(_≤_) ⦄ → WellFounded((_≤_) on₂ f)
  wellfounded-image-by-trans = accessibleₗ-image-by-trans infer

module _ ⦃ refl : Reflexivity{T = B}(_≤_) ⦄ where
  open Strict.Properties

  accessibleₗ-image-by-refl : ⦃ _ : Accessibleₗ{T = B}(_≤_)(f(x)) ⦄ → Accessibleₗ((_≤_) on₂ f)(x)
  accessibleₗ-image-by-refl {f = f} {y} ⦃ intro ⦃ acc ⦄ ⦄ = accessibleₗ-image-by-refl ⦃ acc{f(y)} ⦃ reflexivity(_≤_) ⦄ ⦄

  wellfounded-image-by-refl : ∀{f : A → B} → ⦃ _ : WellFounded{T = B}(_≤_) ⦄ → WellFounded((_≤_) on₂ f)
  wellfounded-image-by-refl = accessibleₗ-image-by-refl

module _ ⦃ sub : (_≤₁_) ⊆₂ (_≤₂_) ⦄ where
  open Strict.Properties

  accessibleₗ-sub₂ : ⦃ _ : Accessibleₗ(_≤₂_)(x) ⦄ → Accessibleₗ(_≤₁_)(x)
  accessibleₗ-sub₂ {x = y} ⦃ intro ⦃ acc ⦄ ⦄ = intro ⦃ \{x} ⦃ xy ⦄ → accessibleₗ-sub₂ ⦃ acc{x} ⦃ sub₂(_≤₁_)(_≤₂_) xy ⦄ ⦄ ⦄

  wellfounded-sub₂ : ⦃ _ : WellFounded(_≤₂_) ⦄ → WellFounded(_≤₁_)
  wellfounded-sub₂ = accessibleₗ-sub₂


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.DirProd

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsAbGroup {G : Type ℓ}
                 (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where

  constructor isabgroup

  field
    isGroup : IsGroup 0g _+_ -_
    +Comm    : (x y : G) → x + y ≡ y + x

  open IsGroup isGroup public
    renaming
      ( ·Assoc      to +Assoc
      ; ·IdL        to +IdL
      ; ·IdR        to +IdR
      ; ·InvL       to +InvL
      ; ·InvR       to +InvR)

  infixl 6 _-_

  -- Useful notation for additive groups
  _-_ : G → G → G
  x - y = x + (- y)

unquoteDecl IsAbGroupIsoΣ = declareRecordIsoΣ IsAbGroupIsoΣ (quote IsAbGroup)

record AbGroupStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor abgroupstr

  field
    0g        : A
    _+_       : A → A → A
    -_        : A → A
    isAbGroup : IsAbGroup 0g _+_ -_

  infixr 7 _+_
  infix  8 -_

  open IsAbGroup isAbGroup public

AbGroup : ∀ ℓ → Type (ℓ-suc ℓ)
AbGroup ℓ = TypeWithStr ℓ AbGroupStr

module _ {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
         (is-setG : isSet G)
         (+Assoc   : (x y z : G) → x + (y + z) ≡ (x + y) + z)
         (+IdR     : (x : G) → x + 0g ≡ x)
         (+InvR    : (x : G) → x + (- x) ≡ 0g)
         (+Comm    : (x y : G) → x + y ≡ y + x)
  where

  makeIsAbGroup : IsAbGroup 0g _+_ -_
  makeIsAbGroup .IsAbGroup.isGroup =
    makeIsGroup is-setG +Assoc +IdR
                (λ x → +Comm _ _ ∙ +IdR x)
                +InvR
                (λ x → +Comm _ _ ∙ +InvR x)
  makeIsAbGroup .IsAbGroup.+Comm = +Comm

module _ {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
         (is-setG : isSet G)
         (+Assoc  : (x y z : G) → x + (y + z) ≡ (x + y) + z)
         (+IdR    : (x : G) → x + 0g ≡ x)
         (+InvR   : (x : G) → x + (- x) ≡ 0g)
         (+Comm   : (x y : G) → x + y ≡ y + x)
  where

  makeAbGroup : AbGroup ℓ
  makeAbGroup .fst = G
  makeAbGroup .snd .AbGroupStr.0g = 0g
  makeAbGroup .snd .AbGroupStr._+_ = _+_
  makeAbGroup .snd .AbGroupStr.-_ = -_
  makeAbGroup .snd .AbGroupStr.isAbGroup = makeIsAbGroup is-setG +Assoc +IdR +InvR +Comm

open GroupStr
open AbGroupStr
open IsAbGroup

AbGroupStr→GroupStr : {G : Type ℓ} → AbGroupStr G → GroupStr G
AbGroupStr→GroupStr A .1g = A .0g
AbGroupStr→GroupStr A ._·_ = A ._+_
AbGroupStr→GroupStr A .inv = A .-_
AbGroupStr→GroupStr A .isGroup = A .isAbGroup .isGroup

AbGroup→Group : AbGroup ℓ → Group ℓ
fst (AbGroup→Group A) = fst A
snd (AbGroup→Group A) = AbGroupStr→GroupStr (snd A)

Group→AbGroup : (G : Group ℓ) → ((x y : fst G) → _·_ (snd G) x y ≡ _·_ (snd G) y x) → AbGroup ℓ
fst (Group→AbGroup G +Comm) = fst G
AbGroupStr.0g (snd (Group→AbGroup G +Comm)) = 1g (snd G)
AbGroupStr._+_ (snd (Group→AbGroup G +Comm)) = _·_ (snd G)
AbGroupStr.- snd (Group→AbGroup G +Comm) = inv (snd G)
IsAbGroup.isGroup (AbGroupStr.isAbGroup (snd (Group→AbGroup G +Comm))) = isGroup (snd G)
IsAbGroup.+Comm (AbGroupStr.isAbGroup (snd (Group→AbGroup G +Comm))) = +Comm

module _ ((G , abgroupstr _ _ _ GisGroup) : AbGroup ℓ) where
  AbGroup→CommMonoid : CommMonoid ℓ
  AbGroup→CommMonoid .fst = G
  AbGroup→CommMonoid .snd .CommMonoidStr.ε = _
  AbGroup→CommMonoid .snd .CommMonoidStr._·_ = _
  AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.isMonoid = IsAbGroup.isMonoid GisGroup
  AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.·Comm = IsAbGroup.+Comm GisGroup

isSetAbGroup : (A : AbGroup ℓ) → isSet ⟨ A ⟩
isSetAbGroup A = isSetGroup (AbGroup→Group A)

AbGroupHom : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H)

AbGroupIso : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
AbGroupIso G H = GroupIso (AbGroup→Group G) (AbGroup→Group H)

IsAbGroupEquiv : {A : Type ℓ} {B : Type ℓ'}
  (G : AbGroupStr A) (e : A ≃ B) (H : AbGroupStr B) → Type (ℓ-max ℓ ℓ')
IsAbGroupEquiv G e H = IsGroupHom (AbGroupStr→GroupStr G) (e .fst) (AbGroupStr→GroupStr H)

AbGroupEquiv : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
AbGroupEquiv G H = Σ[ e ∈ (G .fst ≃ H .fst) ] IsAbGroupEquiv (G .snd) e (H .snd)

isPropIsAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
                → isProp (IsAbGroup 0g _+_ (-_))
isPropIsAbGroup 0g _+_ -_ =
  isOfHLevelRetractFromIso 1 IsAbGroupIsoΣ
    (isPropΣ (isPropIsGroup 0g _+_ (-_))
             (λ grp → isPropΠ2 (λ _ _ → grp .is-set _ _)))
  where
  open IsGroup

𝒮ᴰ-AbGroup : DUARel (𝒮-Univ ℓ) AbGroupStr ℓ
𝒮ᴰ-AbGroup =
  𝒮ᴰ-Record (𝒮-Univ _) IsAbGroupEquiv
    (fields:
      data[ _+_ ∣ autoDUARel _ _ ∣ pres· ]
      data[ 0g ∣ autoDUARel _ _ ∣ pres1 ]
      data[ -_ ∣ autoDUARel _ _ ∣ presinv ]
      prop[ isAbGroup ∣ (λ _ _ → isPropIsAbGroup _ _ _) ])
  where
  open AbGroupStr
  open IsGroupHom

-- Extract the characterization of equality of groups
AbGroupPath : (G H : AbGroup ℓ) → (AbGroupEquiv G H) ≃ (G ≡ H)
AbGroupPath = ∫ 𝒮ᴰ-AbGroup .UARel.ua

-- The module below defines an abelian group induced from an
-- equivalence between an abelian group G and a type A which preserves
-- the full raw group structure from G to A. This version is useful
-- when proving that some type equivalent to an abelian group is an
-- abelian group while also specifying the binary operation, unit and
-- inverse. For an example of this see Algebra.Matrix
module _ (G : AbGroup ℓ) {A : Type ℓ}
  (m : A → A → A)
  (u : A)
  (inverse : A → A)
  (e : ⟨ G ⟩ ≃ A)
  (p+ : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
  (pu : e .fst (G .snd .0g) ≡ u)
  (pinv : ∀ x → e .fst (G .snd .-_ x) ≡ inverse (e .fst x))
  where

  private
    module G = AbGroupStr (G .snd)

    BaseΣ : Type (ℓ-suc ℓ)
    BaseΣ = Σ[ B ∈ Type ℓ ] (B → B → B) × B × (B → B)

    FamilyΣ : BaseΣ → Type ℓ
    FamilyΣ (B , m , u , i) = IsAbGroup u m i

    inducedΣ : FamilyΣ (A , m , u , inverse)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel BaseΣ) (e , p+ , pu , pinv))
        G.isAbGroup

  InducedAbGroup : AbGroup ℓ
  InducedAbGroup .fst = A
  InducedAbGroup .snd ._+_ = m
  InducedAbGroup .snd .0g = u
  InducedAbGroup .snd .-_ = inverse
  InducedAbGroup .snd .isAbGroup = inducedΣ

  InducedAbGroupEquiv : AbGroupEquiv G InducedAbGroup
  fst InducedAbGroupEquiv = e
  snd InducedAbGroupEquiv = makeIsGroupHom p+

  InducedAbGroupPath : G ≡ InducedAbGroup
  InducedAbGroupPath = AbGroupPath _ _ .fst InducedAbGroupEquiv

-- The module below defines an abelian group induced from an
-- equivalence which preserves the binary operation (i.e. a group
-- isomorphism). This version is useful when proving that some type
-- equivalent to an abelian group G is an abelian group when one
-- doesn't care about what the unit and inverse are. When using this
-- version the unit and inverse will both be defined by transporting
-- over the unit and inverse from G to A.
module _ (G : AbGroup ℓ) {A : Type ℓ}
  (m : A → A → A)
  (e : ⟨ G ⟩ ≃ A)
  (p· : ∀ x y → e .fst (G .snd ._+_ x y) ≡ m (e .fst x) (e .fst y))
  where

  private
    module G = AbGroupStr (G .snd)

    FamilyΣ : Σ[ B ∈ Type ℓ ] (B → B → B) → Type ℓ
    FamilyΣ (B , n) = Σ[ e ∈ B ] Σ[ i ∈ (B → B) ] IsAbGroup e n i

    inducedΣ : FamilyΣ (A , m)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel (Σ[ B ∈ Type ℓ ] (B → B → B))) (e , p·))
        (G.0g , G.-_ , G.isAbGroup)

  InducedAbGroupFromPres· : AbGroup ℓ
  InducedAbGroupFromPres· .fst = A
  InducedAbGroupFromPres· .snd ._+_ = m
  InducedAbGroupFromPres· .snd .0g = inducedΣ .fst
  InducedAbGroupFromPres· .snd .-_ = inducedΣ .snd .fst
  InducedAbGroupFromPres· .snd .isAbGroup = inducedΣ .snd .snd

  InducedAbGroupEquivFromPres· : AbGroupEquiv G InducedAbGroupFromPres·
  fst InducedAbGroupEquivFromPres· = e
  snd InducedAbGroupEquivFromPres· = makeIsGroupHom p·

  InducedAbGroupPathFromPres· : G ≡ InducedAbGroupFromPres·
  InducedAbGroupPathFromPres· = AbGroupPath _ _ .fst InducedAbGroupEquivFromPres·

dirProdAb : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
dirProdAb A B =
  Group→AbGroup (DirProd (AbGroup→Group A) (AbGroup→Group B))
                 λ p q → ΣPathP (+Comm (isAbGroup (snd A)) _ _
                                , +Comm (isAbGroup (snd B)) _ _)

trivialAbGroup : ∀ {ℓ} → AbGroup ℓ
fst trivialAbGroup = Unit*
0g (snd trivialAbGroup) = tt*
_+_ (snd trivialAbGroup) _ _ = tt*
(- snd trivialAbGroup) _ = tt*
isAbGroup (snd trivialAbGroup) = makeIsAbGroup
                                 (isProp→isSet isPropUnit*)
                                 (λ _ _ _ → refl)
                                 (λ _ → refl)
                                 (λ _ → refl)
                                 (λ _ _ → refl)

-- useful lemma
-- duplicate propeerties => this file should be split !
move4 : ∀ {ℓ} {A : Type ℓ} (x y z w : A) (_+_ : A → A → A)
       → ((x y z : A) → x + (y + z) ≡ (x + y) + z)
       → ((x y : A) → x + y ≡ y + x)
      → (x + y) + (z + w) ≡ ((x + z) + (y + w))
move4 x y z w _+_ assoc +Comm =
     sym (assoc x y (z + w))
  ∙∙ cong (x +_) (assoc y z w ∙∙ cong (_+ w) (+Comm y z) ∙∙ sym (assoc z y w))
  ∙∙ assoc x z (y + w)

---- The type of homomorphisms A → B is an AbGroup if B is -----
module _ {ℓ ℓ' : Level} (AGr : Group ℓ) (BGr : AbGroup ℓ') where
  private
    strA = snd AGr
    strB = snd BGr

    _* = AbGroup→Group

    A = fst AGr
    B = fst BGr
    open IsGroupHom

    open AbGroupStr strB
      renaming (_+_ to _+B_ ; -_ to -B_ ; 0g to 0B
              ; +IdR to +IdRB ; +IdL to +IdLB
              ; +Assoc to +AssocB ; +Comm to +CommB
              ; +InvR to +InvRB ; +InvL to +InvLB)
    open GroupStr strA
      renaming (_·_ to _∙A_ ; inv to -A_
                ; 1g to 1A ; ·IdR to ·IdRA)

  trivGroupHom : GroupHom AGr (BGr *)
  fst trivGroupHom x = 0B
  snd trivGroupHom = makeIsGroupHom λ _ _ → sym (+IdRB 0B)

  compHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
  fst (compHom f g) x = fst f x +B fst g x
  snd (compHom f g) =
      makeIsGroupHom λ x y
      → cong₂ _+B_ (pres· (snd f) x y) (pres· (snd g) x y)
      ∙ move4 (fst f x) (fst f y) (fst g x) (fst g y)
              _+B_ +AssocB +CommB

  invHom : GroupHom AGr (BGr *) → GroupHom AGr (BGr *)
  fst (invHom (f , p)) x = -B f x
  snd (invHom (f , p)) =
    makeIsGroupHom
      λ x y → cong -B_ (pres· p x y)
            ∙∙ GroupTheory.invDistr (BGr *) (f x) (f y)
            ∙∙ +CommB _ _

  open AbGroupStr

  HomGroup : AbGroup (ℓ-max ℓ ℓ')
  fst HomGroup = GroupHom AGr (BGr *)
  0g (snd HomGroup) = trivGroupHom
  _+_ (snd HomGroup) = compHom
  - snd HomGroup = invHom
  isAbGroup (snd HomGroup) =
    makeIsAbGroup
    isSetGroupHom
    (λ { (f , p) (g , q) (h , r) → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                                             (funExt λ x → +AssocB _ _ _) })
    (λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +IdRB _)})
    ((λ { (f , p) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ y → +InvRB _)}))
    (λ { (f , p) (g , q) → Σ≡Prop (λ _ → isPropIsGroupHom _ _) (funExt λ x → +CommB _ _)})

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Dependently typed changes with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Change.Validity where

open import Nehemiah.Syntax.Type
open import Nehemiah.Denotation.Value

import Parametric.Change.Validity ⟦_⟧Base as Validity

open import Nehemiah.Change.Type
open import Nehemiah.Change.Value

open import Data.Integer
open import Structure.Bag.Nehemiah
open import Base.Change.Algebra

open import Level

change-algebra-base : ∀ ι → ChangeAlgebra ⟦ ι ⟧Base
change-algebra-base base-int = GroupChanges.changeAlgebraGroup _ {{abelian-int}}
change-algebra-base base-bag = GroupChanges.changeAlgebraGroup _ {{abelian-bag}}

instance
  change-algebra-base-family : ChangeAlgebraFamily ⟦_⟧Base
  change-algebra-base-family = family change-algebra-base

open Validity.Structure {{change-algebra-base-family}} public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
open import Oscar.Prelude
open import Oscar.Data.𝟘

module Oscar.Data.Proposequality where

module _ where

  data Proposequality {𝔬} {𝔒 : Ø 𝔬} (𝓞 : 𝔒) : 𝔒 → Ø₀ where
    instance ∅ : Proposequality 𝓞 𝓞

  {-# BUILTIN EQUALITY Proposequality #-}

  Proposequality⟦_⟧ : ∀ {𝔬} (𝔒 : Ø 𝔬) → 𝔒 → 𝔒 → Ø₀
  Proposequality⟦ _ ⟧ = Proposequality

  [Proposequality] : ∀ {𝔬} {𝔒 : Ø 𝔬} → {x y : 𝔒} → Ø₀
  [Proposequality] {x = x} {y = y} = Proposequality x y

module _ where

  infix 4 _≡_
  _≡_ = Proposequality

-- transport : ∀ {a b} {A : Set a} (B : A → Set b) {x y} → x ≡ y → B x → B y
-- transport _ ∅ = ¡

-- transport₂ : ∀ {a b c} {A : Set a} {B : Set b} (C : A → B → Set c) {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → C x₁ y₁ → C x₂ y₂
-- transport₂ _ ∅ ∅ = ¡

module _ where

  Proposantiequality : ∀ {𝔬} {𝔒 : Ø 𝔬} → 𝔒 → 𝔒 → Ø₀
  Proposantiequality x y = Proposequality x y → 𝟘

  Proposantiequality⟦_⟧ : ∀ {𝔬} (𝔒 : Ø 𝔬) → 𝔒 → 𝔒 → Ø₀
  Proposantiequality⟦ _ ⟧ = Proposantiequality

  infix 4 _≢_
  _≢_ = Proposantiequality

module _ where

  Proposextensequality : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} → ((𝓞 : 𝔒) → 𝔓 𝓞) → ((𝓞 : 𝔒) → 𝔓 𝓞) → Ø 𝔬
  Proposextensequality 𝓟₁ 𝓟₂ = ∀ 𝓞 → Proposequality (𝓟₁ 𝓞) (𝓟₂ 𝓞)

  Proposextensequality⟦_⟧ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) → ((𝓞 : 𝔒) → 𝔓 𝓞) → ((𝓞 : 𝔒) → 𝔓 𝓞) → Ø 𝔬
  Proposextensequality⟦ _ ⟧ = Proposextensequality

  Proposextensequality[_/_] : ∀ {𝔬} (𝔒 : Ø 𝔬) {𝔭} (𝔓 : 𝔒 → Ø 𝔭) → ((𝓞 : 𝔒) → 𝔓 𝓞) → ((𝓞 : 𝔒) → 𝔓 𝓞) → Ø 𝔬
  Proposextensequality[ _ / _ ] = Proposextensequality

module _ where

  infix 4 _≡̇_
  _≡̇_ = Proposextensequality

  infix 4 ≡̇⟦⟧-syntax
  ≡̇⟦⟧-syntax = Proposextensequality⟦_⟧
  syntax ≡̇⟦⟧-syntax t x y = x ≡̇⟦ t ⟧ y


text:
-- Andreas, 2016-02-09, should not record sections have all hidden parameters?

module _ (A : Set) where

  record R : Set where
    postulate
      P : (a : A) → Set

  -- Records have some magic to make record parameters hidden
  -- in record section.
  -- This leads to an error in @checkInternal@.
  -- Should the parent parameters alse be hidden in the record section?

  record Fails (a : A) : Set where

    T = (w p : R.P _ a) → Set -- well-formed

    f : R.P _ a → Set
    f p with p
    ... | _ = A

-- ERROR:
-- Expected a hidden argument, but found a visible argument
-- when checking that the type (w p : R.P _ a) → Set of the generated
-- with function is well-formed

-- Should succeed.


text:
-- Category of sets and functions

module Control.Category.SetsAndFunctions where

open import Level using (zero; suc; _⊔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Data.Product

open import Axiom.FunctionExtensionality

open import Control.Category
open import Control.Category.Product

-- Category SET

Functions : Set → Set → Setoid _ _
Functions A B = setoid (A → B)

setIsCategory : IsCategory Functions
setIsCategory = record
  { ops = record
    { id  = λ x → x
    ; _⟫_ = λ f g x → g (f x)
    }
  ; laws = record
    { id-first = refl
    ; id-last  = refl
    ; ∘-assoc  = λ f → refl
    ; ∘-cong   = λ{ refl refl → refl }
    }
  }

SET : Category _ _ _
SET = record { Hom = Functions; isCategory = setIsCategory }

{-
timesProductStructure : (A B : Set) → ProductStructure SET A B
timesProductStructure A B = record
  { A×B = A × B
  ; fst = proj₁
  ; snd = proj₂
  }

⟨_,_⟩ :  {A B C : Set} (f : C → A) (g : C → B) → C → A × B
⟨ f , g ⟩ = λ x → f x , g x

pairIsPair : {A B C : Set} (f : C → A) (g : C → B) →
  IsPair (timesProductStructure A B) f g ⟨ f , g ⟩
pairIsPair f g = record
  { β-fst = refl
  ; β-snd = refl
  }

open IsPair

pairPair : {A B C : Set} (f : C → A) (g : C → B) →
  Pair (timesProductStructure A B) f g
pairPair f g = record
  { ⟨f,g⟩  = ⟨ f , g ⟩
  ; isPair = pairIsPair f g
  ; unique =  λ p → fun-ext (λ x → cong₂ (λ f g → f x , g x) (β-fst p) (β-snd p))
  }

timesIsProduct : (A B : Set) → Product SET A B
timesIsProduct A B = record
  { productStructure = timesProductStructure A B
  ; isProduct = record { pair = pairPair }
  }

-- -}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
------------------------------------------------------------------------
-- A lemma
------------------------------------------------------------------------

open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph using (acyclic)

module Mixfix.Acyclic.Lemma
         (g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
         where

open import Data.List using ([]; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; foldl; _⁺∷ʳ_)
open import Data.Product using (uncurry)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)

open PrecedenceCorrect acyclic g
open import Mixfix.Fixity

-- A generalisation of Mixfix.Acyclic.Grammar.Prec.appˡ.

appˡ : ∀ {p} → Outer p left → List⁺ (Outer p left → ExprIn p left) →
       ExprIn p left
appˡ e fs = foldl (λ e f → f (similar e)) (λ f → f e) fs

appˡ-∷ʳ : ∀ {p} (e : Outer p left) fs f →
          appˡ e (fs ⁺∷ʳ f) ≡ f (similar (appˡ e fs))
appˡ-∷ʳ e (f′ ∷ fs) = helper e f′ fs
  where
  helper : ∀ {p} (e : Outer p left) f′ fs f →
           appˡ e ((f′ ∷ fs) ⁺∷ʳ f) ≡ f (similar (appˡ e (f′ ∷ fs)))
  helper e f′ []        f = refl
  helper e f′ (f″ ∷ fs) f = helper (similar (f′ e)) f″ fs f

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --copatterns --sized-types #-}

open import Function
open import Data.Unit as Unit renaming (tt to ∗)
open import Data.List as List

TyCtx = List ⊤

data TyVar : (Γ : TyCtx) → Set where
  zero : ∀{Γ}                          → TyVar (∗ ∷ Γ)
  succ : ∀{Γ} → (x : TyVar Γ) → TyVar (∗ ∷ Γ)

data Type (Γ : TyCtx) : Set where
  unit :                                     Type Γ
  var  : (x : TyVar Γ)                     → Type Γ
  _⊕_  : (t₁ : Type Γ)       (t₂ : Type Γ) → Type Γ
  μ    : (t : Type (_ ∷ Γ))                → Type Γ
  _⊗_  : (t₁ : Type Γ)       (t₂ : Type Γ) → Type Γ
  _⇒_  : (t₁ : Type [])      (t₂ : Type Γ) → Type Γ
  ν    : (t : Type (_ ∷ Γ))                → Type Γ

-- | Variable renaming in types
_▹_ : (Γ Δ : TyCtx) → Set
Γ ▹ Δ = TyVar Γ → TyVar Δ

{-
rename : {Γ Δ : TyCtx} → (ρ : Γ ▹ Δ) → Type Γ → Type Δ
rename         ρ unit      = unit
rename         ρ (var x)   = var (ρ ∗ x)
rename         ρ (t₁ ⊕ t₂) = rename ρ t₁ ⊕ rename ρ t₂
rename {Γ} {Δ} ρ (μ t)     = μ (rename ρ' t)
  where
    ρ' : (∗ ∷ Γ) ▹ (∗ ∷ Δ)
    ρ' = ?
    -- ρ' = id {[ ∗ ]} ⧻ ρ
rename         ρ (t₁ ⊗ t₂) = rename ρ t₁ ⊗ rename ρ t₂
rename         ρ (t₁ ⇒ t₂) = t₁ ⇒ rename ρ t₂
rename {Γ} {Δ} ρ (ν t)     = ν (rename ρ' t)
  where
    ρ' : (∗ ∷ Γ) ▹ (∗ ∷ Δ)
    ρ' = ?
--    ρ' = ctx-id {[ ∗ ]} ⧻ ρ

-------------------------
---- Generating structure on contexts (derived from renaming)

weaken : {Γ : TyCtx} (Δ : TyCtx) → Type Γ -> Type (Δ ++ Γ)
weaken {Γ} Δ = rename {Γ} {Δ ++ Γ} ?

exchange : (Γ Δ : TyCtx) → Type (Γ ++ Δ) -> Type (Δ ++ Γ)
exchange Γ Δ = rename [ i₂ {Δ} {Γ} , i₁ {Δ} {Γ} ]

contract : {Γ : TyCtx} → Type (Γ ∐ Γ) -> Type Γ
contract = rename [ ctx-id , ctx-id ]

-}

Subst : TyCtx → TyCtx → Set
Subst Γ Δ = TyVar Γ → Type Δ

update : ∀{Γ Δ : TyCtx} → Subst Γ Δ → Type Δ → (Subst (∗ ∷ Γ) Δ)
update σ a zero        = a
update σ _ (succ x) = σ x

lift : ∀{Γ Δ} → Subst Γ Δ → Subst (∗ ∷ Γ) (∗ ∷ Δ)
lift σ zero = {!!}
lift σ (succ x) = {!!}

-- | Simultaneous substitution
subst : {Γ Δ : TyCtx} → (σ : Subst Γ Δ) → Type Γ → Type Δ
subst         σ unit      = unit
subst         σ (var x)   = σ x
subst         σ (t₁ ⊕ t₂) = subst σ t₁ ⊕ subst σ t₂
subst {Γ} {Δ} σ (μ t)     = μ (subst (lift σ) t)
subst         σ (t₁ ⊗ t₂) = subst σ t₁ ⊗ subst σ t₂
subst         σ (t₁ ⇒ t₂) = t₁ ⇒ subst σ t₂
subst {Γ} {Δ} σ (ν t)     = ν (subst (lift σ) t)

data Term : Set where

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Fold where

open import Prelude

myfold : {ac b : Set} -> (ac -> b -> ac) -> ac -> List b -> ac
#ifdef strict
myfold = foldl!
#else
myfold = foldl
#endif

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
------------------------------------------------------------------------
-- The double-negation monad
------------------------------------------------------------------------

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

open import Equality

module Double-negation
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Equivalence eq hiding (id; _∘_)
open import Excluded-middle eq
open import H-level eq
open import H-level.Closure eq
open import Monad eq

-- The double-negation monad, defined using a wrapper type to make
-- instance resolution easier.

infix 3 ¬¬_

record ¬¬_ {a} (A : Type a) : Type a where
  constructor wrap
  field
    run : ¬ ¬ A

open ¬¬_ public

-- An extra universe-polymorphic variant of map.

map′ :
  ∀ {a b} {@0 A : Type a} {@0 B : Type b} →
  (A → B) → ¬¬ A → ¬¬ B
run (map′ f ¬¬a) = λ ¬b → run ¬¬a (λ a → ¬b (f a))

-- Instances.

instance

  double-negation-monad : ∀ {ℓ} → Raw-monad (λ (A : Type ℓ) → ¬¬ A)
  run (Raw-monad.return double-negation-monad x)   = _$ x
  run (Raw-monad._>>=_  double-negation-monad x f) =
    join (map′ (run ∘ f) x)
    where
    join : ∀ {a} {A : Type a} → ¬¬ ¬ A → ¬ A
    join ¬¬¬a = λ a → run ¬¬¬a (λ ¬a → ¬a a)

private

  proof-irrelevant : ∀ {a} {A : Type a} {x y : ¬¬ A} →
                     Extensionality a lzero → x ≡ y
  proof-irrelevant ext =
    cong wrap $ apply-ext ext λ _ → ⊥-propositional _ _

monad : ∀ {ℓ} →
        Extensionality ℓ lzero →
        Monad (λ (A : Type ℓ) → ¬¬ A)
Monad.raw-monad      (monad _)         = double-negation-monad
Monad.left-identity  (monad ext) _ _   = proof-irrelevant ext
Monad.right-identity (monad ext) _     = proof-irrelevant ext
Monad.associativity  (monad ext) _ _ _ = proof-irrelevant ext

-- The following variant of excluded middle is provable.

excluded-middle : ∀ {a} {@0 A : Type a} → ¬¬ Dec A
run excluded-middle ¬[a⊎¬a] = ¬[a⊎¬a] (no λ a → ¬[a⊎¬a] (yes a))

-- The following variant of Peirce's law is provable.

call/cc : ∀ {a w} {@0 A : Type a} {Whatever : Type w} →
          ((A → Whatever) → ¬¬ A) → ¬¬ A
run (call/cc hyp) ¬a = run (hyp (λ a → ⊥-elim (¬a a))) ¬a

-- If one can prove that the empty type is inhabited in the
-- double-negation monad, then the empty type is inhabited.

¬¬¬⊥ : ∀ {ℓ} → ¬ (¬¬ (⊥ {ℓ = ℓ}))
¬¬¬⊥ ¬¬⊥ = run ¬¬⊥ ⊥-elim

-- If the double-negation of a negation can be proved, then the
-- negation itself can be proved.

¬¬¬→¬ : ∀ {a} {A : Type a} → ¬¬ ¬ A → ¬ A
¬¬¬→¬ ¬¬¬a = λ a → ¬¬¬⊥ (¬¬¬a >>= λ ¬a → ⊥-elim (¬a a))

------------------------------------------------------------------------
-- Excluded middle and double-negation elimination

-- Double-negation elimination (roughly as stated in the HoTT book).

Double-negation-elimination : (ℓ : Level) → Type (lsuc ℓ)
Double-negation-elimination p =
  {P : Type p} → Is-proposition P → ¬¬ P → P

-- Double-negation elimination is propositional (assuming
-- extensionality).

Double-negation-elimination-propositional :
  ∀ {ℓ} →
  Extensionality (lsuc ℓ) ℓ →
  Is-proposition (Double-negation-elimination ℓ)
Double-negation-elimination-propositional ext =
  implicit-Π-closure ext 1 λ _ →
  Π-closure (lower-extensionality _ lzero ext) 1 λ P-prop →
  Π-closure (lower-extensionality _ lzero ext) 1 λ _ →
  P-prop

-- Excluded middle implies double-negation elimination.

Excluded-middle→Double-negation-elimination :
  ∀ {ℓ} → Excluded-middle ℓ → Double-negation-elimination ℓ
Excluded-middle→Double-negation-elimination em P-prop ¬¬p =
  [ id , ⊥-elim ∘ run ¬¬p ] (em P-prop)

-- Excluded middle is pointwise equivalent to double-negation
-- elimination (assuming extensionality).

Excluded-middle≃Double-negation-elimination :
  ∀ {ℓ} →
  Extensionality (lsuc ℓ) (lsuc ℓ) →
  Excluded-middle ℓ ≃ Double-negation-elimination ℓ
Excluded-middle≃Double-negation-elimination ext =
  _↔_.to (⇔↔≃ ext
              (Excluded-middle-propositional
                 (lower-extensionality lzero _ ext))
              (Double-negation-elimination-propositional
                 (lower-extensionality lzero _ ext)))
    (record
       { to   = Excluded-middle→Double-negation-elimination
       ; from = λ dne P-prop →
                  dne (Dec-closure-propositional
                         (lower-extensionality _ _ ext) P-prop)
                      excluded-middle
       })


text:
-- {-# OPTIONS -v tc.lhs.unify:100 #-}
module Issue811 where

module ParamIndex where
  -- Report by stevan:
  -- When case-splitting, I think dots end up at the wrong places,
  -- consider:

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

  -- If you case-split on p in:
  dot : ∀ {A}(x : A)(y : A) → x ≡ y → Set
  dot x y p = {!p!}

  {- You get:
  dot′ : ∀ {A}(x y : A) → x ≡ y → Set
  dot′ .y y refl = {!!}

  -- This seems the wrong way around to me, because we say that the first
  -- argument has to be something, namely y, before that something has
  -- been introduced.

  -- If I'd do the case-splitting manually, I would write:
  dot″ : ∀ {A}(x y : A) → x ≡ y → Set
  dot″ x .x refl = {!!}
  -}

  -- Andreas, 2013-03-05 This is indeed what you get now, since
  -- Agda now prefers the more left variables.

  -- Unfortunately, this leads to bad behavior in this case:
  dot1 : ∀ {A}{x : A}(y : A) → x ≡ y → Set
  dot1 y p = {!p!}

  -- This one works nicely
  dot2 : ∀ {A}(x : A){y : A} → x ≡ y → Set
  dot2 x p = {!p!}

module AllIndices where

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

  dot : ∀ {A}(x : A)(y : A) → x ≡ y → Set
  dot x y p = {!p!}

  -- Same problem here:
  dot1 : ∀ {A}{x : A}(y : A) → x ≡ y → Set
  dot1 y p = {!p!}

  dot2 : ∀ {A}(x : A){y : A} → x ≡ y → Set
  dot2 x p = {!p!}

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module plfa-code.Lists where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
open import Level using (Level)
open import plfa-code.Isomorphism using (_≃_; _⇔_)

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 5 _∷_

_ : List ℕ
_ = 0 ∷ 1 ∷ 2 ∷ []

data List′ : Set → Set where
  []′  : ∀ {A : Set} → List′ A
  _∷′_ : ∀ {A : Set} → A → List′ A → List′ A

_ : List ℕ
_ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ})))

{-# BUILTIN LIST List #-}

pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

infixr 5 _++_

_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys  =  ys
(x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)

_ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ]
_ = -- refl
  begin
    0 ∷ 1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ []
  ≡⟨⟩
    0 ∷ (1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    0 ∷ 1 ∷ (2 ∷ [] ++ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    0 ∷ 1 ∷ 2 ∷ ([] ++ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []
  ∎

++-assoc : ∀ {A : Set} (xs ys zs : List A)
  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs = -- refl
  begin
    ([] ++ ys) ++ zs
  ≡⟨⟩
    ys ++ zs
  ≡⟨⟩
    [] ++ (ys ++ zs)
  ∎
++-assoc (x ∷ xs) ys zs = -- cong (_∷_ x) (++-assoc xs ys zs)
  begin
    (x ∷ xs ++ ys) ++ zs
  ≡⟨⟩
    x ∷ (xs ++ ys) ++ zs
  ≡⟨⟩
    x ∷ ((xs ++ ys) ++ zs)
  ≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩
    x ∷ (xs ++ (ys ++ zs))
  ≡⟨⟩
    x ∷ xs ++ (ys ++ zs)
  ∎

++-identityˡ : ∀ {A : Set} (xs : List A) → [] ++ xs ≡ xs
++-identityˡ xs = -- refl
  begin
    [] ++ xs
  ≡⟨⟩
    xs
  ∎

++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-identityʳ [] = -- refl
  begin
    [] ++ []
  ≡⟨⟩
    []
  ∎
++-identityʳ (x ∷ xs) = -- cong (_∷_ x) (++-identityʳ xs)
  begin
   (x ∷ xs) ++ []
  ≡⟨⟩
    x ∷ (xs ++ [])
  ≡⟨ cong (x ∷_) (++-identityʳ xs) ⟩
   x ∷ xs
  ∎

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

_ : length [ 0 , 1 , 2 ] ≡ 3
_ = -- refl
  begin
    length (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    suc (length (1 ∷ 2 ∷ []))
  ≡⟨⟩
    suc (suc (length (2 ∷ [])))
  ≡⟨⟩
    suc (suc (suc (length {ℕ} [])))
  ≡⟨⟩
    suc (suc (suc zero))
  ∎

length-++ : ∀ {A : Set} (xs ys : List A)
  → length (xs ++ ys) ≡ length xs + length ys
length-++ {A} [] ys = -- refl
  begin
    length ([] ++ ys)
  ≡⟨⟩
    length ys
  ≡⟨⟩
    length {A} [] + length ys
  ∎
length-++ {A} (x ∷ xs) ys = -- cong suc (length-++ xs ys)
  begin
    length ((x ∷ xs) ++ ys)
  ≡⟨⟩
    suc (length (xs ++ ys))
  ≡⟨ cong suc (length-++ xs ys) ⟩
    suc (length xs + length ys)
  ≡⟨⟩
    length (x ∷ xs) + length ys
  ∎

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

_ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ =
  begin
    reverse (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    reverse (1 ∷ 2 ∷ []) ++ [ 0 ]
  ≡⟨⟩
    (reverse (2 ∷ []) ++ [ 1 ]) ++ [ 0 ]
  ≡⟨⟩
    ((reverse [] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
  ≡⟨⟩
    (([] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
  ≡⟨⟩
    (([] ++ 2 ∷ []) ++ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    (2 ∷ [] ++ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    2 ∷ ([] ++ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    (2 ∷ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    2 ∷ (1 ∷ [] ++ 0 ∷ [])
  ≡⟨⟩
    2 ∷ 1 ∷ ([] ++ 0 ∷ [])
  ≡⟨⟩
    2 ∷ 1 ∷ 0 ∷ []
  ≡⟨⟩
    [ 2 , 1 , 0 ]
  ∎

---------- practice ----------
reverse-++-commute : ∀ {A : Set} {xs ys : List A}
  → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-commute {_} {[]} {[]} = refl
reverse-++-commute {_} {[]} {y ∷ ys} = sym (++-identityʳ (reverse ys ++ [ y ]))
reverse-++-commute {_} {x ∷ xs} {ys} =
  begin
    reverse ((x ∷ xs) ++ ys)
  ≡⟨⟩
    reverse (x ∷ (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-commute {_} {xs} {ys}) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ reverse xs ++ [ x ]
  ≡⟨ cong (reverse ys ++_) (sym refl) ⟩
    reverse ys ++ reverse ([ x ] ++ xs)
  ≡⟨⟩
    reverse ys ++ reverse (x ∷ xs)
  ∎

reverse-involutive : ∀ {A : Set} {xs : List A}
  → reverse (reverse xs) ≡ xs
reverse-involutive {_} {[]} = refl
reverse-involutive {_} {x ∷ xs} =
  begin
    reverse (reverse (x ∷ xs))
  ≡⟨⟩
    reverse (reverse xs ++ [ x ])
  ≡⟨ reverse-++-commute {_} {reverse xs} {[ x ]} ⟩
    reverse [ x ] ++ reverse (reverse xs)
  ≡⟨ cong (reverse [ x ] ++_) reverse-involutive ⟩
    [ x ] ++ xs
  ≡⟨⟩
    x ∷ xs
  ∎

------------------------------

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

shunt-reverse : ∀ {A : Set} (xs ys : List A)
  → shunt xs ys ≡ (reverse xs) ++ ys
shunt-reverse [] ys = -- refl
  begin
    shunt [] ys
  ≡⟨⟩
    reverse [] ++ ys
  ∎
shunt-reverse (x ∷ xs) ys =
  begin
    shunt (x ∷ xs) ys
  ≡⟨⟩
    shunt xs (x ∷ ys)
  ≡⟨ shunt-reverse xs (x ∷ ys) ⟩
    reverse xs ++ (x ∷ ys)
  ≡⟨⟩
    reverse xs ++ ([ x ] ++ ys)
  ≡⟨ sym (++-assoc (reverse xs) [ x ] ys) ⟩
    (reverse xs ++ [ x ]) ++ ys
  ≡⟨⟩
    reverse (x ∷ xs) ++ ys
  ∎

reverse′ : ∀ {A : Set} → List A → List A
reverse′ xs = shunt xs []

reverses : ∀ {A : Set} (xs : List A)
  → reverse′ xs ≡ reverse xs
reverses xs =
  begin
    reverse′ xs
  ≡⟨⟩
    shunt xs []
  ≡⟨ shunt-reverse xs [] ⟩
    reverse xs ++ []
  ≡⟨ ++-identityʳ (reverse xs) ⟩
    reverse xs
  ∎

_ : reverse′ [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ =
  begin
    reverse′ (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    shunt (0 ∷ 1 ∷ 2 ∷ []) []
  ≡⟨⟩
    shunt (1 ∷ 2 ∷ []) (0 ∷ [])
  ≡⟨⟩
    shunt (2 ∷ []) (1 ∷ 0 ∷ [])
  ≡⟨⟩
    shunt [] (2 ∷ 1 ∷ 0 ∷ [])
  ≡⟨⟩
    2 ∷ 1 ∷ 0 ∷ []
  ∎

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

_ : map suc [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
_ =
  begin
    map suc (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    suc 0 ∷ map suc (1 ∷ 2 ∷ [])
  ≡⟨⟩
    suc 0 ∷ suc 1 ∷ map suc (2 ∷ [])
  ≡⟨⟩
    suc 0 ∷ suc 1 ∷ suc 2 ∷ map suc []
  ≡⟨⟩
    suc 0 ∷ suc 1 ∷ suc 2 ∷ []
  ≡⟨⟩
    1 ∷ 2 ∷ 3 ∷ []
  ∎

sucs : List ℕ → List ℕ
sucs = map suc

_ : sucs [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
_ =
  begin
    sucs [ 0 , 1 , 2 ]
  ≡⟨⟩
    map suc [ 0 , 1 , 2 ]
  ≡⟨⟩
    [ 1 , 2 , 3 ]
  ∎
---------- practice ----------
open plfa-code.Isomorphism using (extensionality)

map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
  → map (g ∘ f) ≡ map g ∘ map f
map-compose {A} {B} {C} {f} {g} = extensionality hf
  where
  hf : (xs : List A) → map (g ∘ f) xs ≡ map g (map f xs)
  hf [] = refl
  hf (x ∷ xs) = cong ((g (f x)) ∷_) (hf xs)

map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
  →  map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-commute {A} {B} {f} {[]} {ys} = refl
map-++-commute {A} {B} {f} {x ∷ xs} {ys} =
  cong ((f x) ∷_) (map-++-commute {_} {_} {f} {xs} {ys})

data Tree (A B : Set) : Set where
  leaf : A → Tree A B
  node : Tree A B → B → Tree A B → Tree A B

map-Tree : ∀ {A B C D : Set}
  → (A → C) → (B → D) → Tree A B → Tree C D
map-Tree f g (leaf a) = leaf (f a)
map-Tree f g (node tree b tree₁) = node (map-Tree f g tree) (g b) (map-Tree f g tree₁)

------------------------------

foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr _⊗_ e       []  =  e
foldr _⊗_ e (x ∷ xs)  =  x ⊗ (foldr _⊗_ e xs)

_ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
_ =
  begin
    foldr _+_ 0 (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    1 + foldr _+_ 0 (2 ∷ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    1 + (2 + foldr _+_ 0 (3 ∷ 4 ∷ []))
  ≡⟨⟩
    1 + (2 + (3 + foldr _+_ 0 (4 ∷ [])))
  ≡⟨⟩
    1 + (2 + (3 + (4 + foldr _+_ 0 [])))
  ≡⟨⟩
    1 + (2 + (3 + (4 + 0)))
  ∎

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

_ : sum [ 1 , 2 , 3 , 4 ] ≡ 10
_ =
  begin
    sum [ 1 , 2 , 3 , 4 ]
  ≡⟨⟩
    foldr _+_ 0 [ 1 , 2 , 3 , 4 ]
  ≡⟨⟩
    10
  ∎

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

_ : product [ 1 , 2 , 3 , 4 ] ≡ 24
_ = refl

foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
  foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
foldr-++ _⊗_ e []       ys = refl
foldr-++ _⊗_ e (x ∷ xs) ys = cong (x ⊗_) (foldr-++ _⊗_ e xs ys)

map-is-foldr : ∀ {A B : Set} {f : A → B} →
  map f ≡ foldr (λ x xs → f x ∷ xs) []
map-is-foldr {A} {_} {f} = extensionality hf
  where
  hf : (l : List A) → map f l ≡ foldr (λ x xs → f x ∷ xs) [] l
  hf [] = refl
  hf (x ∷ xs) = cong (f x ∷_) (hf xs)

fold-Tree : ∀ {A B C : Set}
  → (A → C) → (C → B → C → C) → Tree A B → C
fold-Tree f g (leaf a)            = f a
fold-Tree f g (node tree b tree₁) = g (fold-Tree f g tree) b (fold-Tree f g tree₁)

downFrom : ℕ → List ℕ
downFrom zero     =  []
downFrom (suc n)  =  n ∷ downFrom n

_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
_ = refl

open Data.Nat.Properties using
  (*-distribʳ-+; *-distribʳ-∸; m∸n+n≡m; m≤m+n;
   +-comm; *-comm; +-identityʳ; *-identityˡ)
open Eq using (cong₂)

2n≡n+n : ∀ n → 2 * n ≡ n + n
2n≡n+n zero = refl
2n≡n+n (suc n) = cong (λ x → suc (n + suc x)) (+-identityʳ n)

n≤n*n : ∀ n → n ≤ n * n
n≤n*n zero    = z≤n
n≤n*n (suc n) = s≤s (m≤m+n n (n * suc n))

sum-downFrom : ∀ (n : ℕ)
  → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom zero    = refl
sum-downFrom (suc n) =
  begin
    sum (downFrom (suc n)) * 2
  ≡⟨⟩
    (n + sum (downFrom n)) * 2
  ≡⟨ *-distribʳ-+ 2 n (sum (downFrom n)) ⟩
    n * 2 + sum (downFrom n) * 2
  ≡⟨ cong (n * 2 +_) (sum-downFrom n) ⟩
    n * 2 + n * (n ∸ 1)
  ≡⟨ cong₂ _+_ (*-comm n 2) (*-comm n (n ∸ 1)) ⟩
    2 * n + (n ∸ 1) * n
  ≡⟨ cong (2 * n +_) (*-distribʳ-∸ n n 1) ⟩
    2 * n + (n * n ∸ 1 * n)
  ≡⟨ cong₂ (λ a b → a + (n * n ∸ b)) (2n≡n+n n) (*-identityˡ n) ⟩
    n + n + (n * n ∸ n)
  ≡⟨ +-comm (n + n) (n * n ∸ n) ⟩
    n * n ∸ n + (n + n)
  ≡⟨ sym (+-assoc (n * n ∸ n) n n) ⟩
    n * n ∸ n + n + n
  ≡⟨ cong (_+ n) (m∸n+n≡m (n≤n*n n)) ⟩
    n * n + n
  ≡⟨ +-comm (n * n) n ⟩
    n + n * n
  ≡⟨⟩
    (suc n) * (suc n ∸ 1)
  ∎

------------------------------

record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where
  field
    assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
    identityˡ : ∀ (x : A) → e ⊗ x ≡ x
    identityʳ : ∀ (x : A) → x ⊗ e ≡ x

open IsMonoid

+-monoid : IsMonoid _+_ 0
+-monoid =
  record
    { assoc = +-assoc
    ; identityˡ = +-identityˡ
    ; identityʳ = +-identityʳ
    }

*-monoid : IsMonoid _*_ 1
*-monoid =
  record
    { assoc = *-assoc
    ; identityˡ = *-identityˡ
    ; identityʳ = *-identityʳ
    }

++-monoid : ∀ {A : Set} → IsMonoid {List A} _++_ []
++-monoid =
  record
    { assoc = ++-assoc
    ; identityˡ = ++-identityˡ
    ; identityʳ = ++-identityʳ
    }

foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs : List A) (y : A) → foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ y
foldr-monoid _⊗_ e ⊗-monoid [] y = -- sym (identityˡ ⊗-monoid y)
  begin
    foldr _⊗_ y []
  ≡⟨⟩
    y
  ≡⟨ sym (identityˡ ⊗-monoid y) ⟩
    (e ⊗ y)
  ≡⟨⟩
    foldr _⊗_ e [] ⊗ y
  ∎
foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
  begin
    foldr _⊗_ y (x ∷ xs)
  ≡⟨⟩
    x ⊗ (foldr _⊗_ y xs)
  ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e ⊗-monoid xs y) ⟩
    x ⊗ ((foldr _⊗_ e xs) ⊗ y)
  ≡⟨ sym (assoc ⊗-monoid x (foldr _⊗_ e xs) y) ⟩
    (x ⊗ (foldr _⊗_ e xs)) ⊗ y
  ∎

foldr-monoid-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs ys : List A) → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
  begin
    foldr _⊗_ e (xs ++ ys)
  ≡⟨ foldr-++ _⊗_ e xs ys ⟩
    foldr _⊗_ (foldr _⊗_ e ys) xs
  ≡⟨ foldr-monoid _⊗_ e monoid-⊗ xs (foldr _⊗_ e ys) ⟩
    foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
  ∎

---------- practice ----------
foldl : ∀ {A B : Set} → (B → A → B) → B → List A → B
foldl _⊗_ e       []  =  e
foldl _⊗_ e (x ∷ xs)  =  foldl _⊗_ (e ⊗ x) xs

foldl-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs : List A) (y : A) → foldl _⊗_ y xs ≡ y ⊗ foldl _⊗_ e xs
foldl-monoid _⊗_ e ⊗-monoid []       y = sym (identityʳ ⊗-monoid y)
foldl-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
  begin
    foldl _⊗_ y (x ∷ xs)
  ≡⟨⟩
    foldl _⊗_ (y ⊗ x) xs
  ≡⟨ foldl-monoid _⊗_ e ⊗-monoid xs (y ⊗ x) ⟩
    (y ⊗ x) ⊗ (foldl _⊗_ e xs)
  ≡⟨ assoc ⊗-monoid y x (foldl _⊗_ e xs) ⟩
    y ⊗ (x ⊗ foldl _⊗_ e xs)
  ≡⟨ sym (cong (y ⊗_) (foldl-monoid _⊗_ e ⊗-monoid xs x)) ⟩
    y ⊗ (foldl _⊗_ x xs)
  ≡⟨ sym (cong (λ z → y ⊗ foldl _⊗_ z xs) (identityˡ ⊗-monoid x)) ⟩
    y ⊗ (foldl _⊗_ (e ⊗ x) xs)
  ≡⟨⟩
    y ⊗ foldl _⊗_ e (x ∷ xs)
  ∎

foldr-monoid-foldl : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs : List A) → foldr _⊗_ e xs ≡ foldl _⊗_ e xs
foldr-monoid-foldl _⊗_ e ⊗-monoid []       = refl
foldr-monoid-foldl _⊗_ e ⊗-monoid (x ∷ xs) =
  begin
    foldr _⊗_ e (x ∷ xs)
  ≡⟨⟩
    (x ⊗ foldr _⊗_ e xs)
  ≡⟨ cong (x ⊗_) (foldr-monoid-foldl _⊗_ e ⊗-monoid xs) ⟩
    (x ⊗ foldl _⊗_ e xs)
  ≡⟨ sym (foldl-monoid _⊗_ e ⊗-monoid xs x) ⟩
    foldl _⊗_ x xs
  ≡⟨ cong (λ a → foldl _⊗_ a xs) (sym (identityˡ ⊗-monoid x)) ⟩
    foldl _⊗_ (e ⊗ x) xs
  ≡⟨⟩
    foldl _⊗_ e (x ∷ xs)
  ∎

------------------------------

data All {A : Set} (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)

_ : All (_≤ 2) [ 0 , 1 , 2 ]
_ = z≤n ∷ s≤s z≤n ∷ s≤s (s≤s z≤n) ∷ []

data Any {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} → P x → Any P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)

_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∉ xs = ¬ (x ∈ xs)

_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
_ = here refl

_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
_ = there (there (here refl))

not-in : 3 ∉ [ 0 , 0 , 0 , 2 ]
not-in (here ())
not-in (there (here ()))
not-in (there (there (here ())))
not-in (there (there (there (here ()))))
not-in (there (there (there (there ()))))

All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
  All P (xs ++ ys) ⇔ (All P xs × All P ys)
All-++-⇔ xs ys =
  record
    { to   = to xs ys
    ; from = from xs ys
    }
  where

  to : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
    All P (xs ++ ys) → (All P xs × All P ys)
  to [] ys Pys = ⟨ [] , Pys ⟩
  to (x ∷ xs) ys (Px ∷ Pxs++ys) with to xs ys Pxs++ys
  ... | ⟨ Pxs , Pys ⟩ = ⟨ Px ∷ Pxs , Pys ⟩

  from : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
    All P xs × All P ys → All P (xs ++ ys)
  from [] ys ⟨ [] , Pys ⟩ = Pys
  from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩ = Px ∷ (from xs ys ⟨ Pxs , Pys ⟩)

---------- practice ----------
open import Data.Sum using (_⊎_; inj₁; inj₂)
open Data.Product using (proj₁; proj₂)
open import Data.Empty using (⊥-elim)

Any-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
  Any P (xs ++ ys) ⇔ (Any P xs ⊎ Any P ys)
Any-++-⇔ {A} {P} xs ys =
  record
  { to   = to xs ys
  ; from = from xs ys
  }
  where
  to : ∀ (xs ys : List A) →
    Any P (xs ++ ys) → Any P xs ⊎ Any P ys
  to []       ys Pys = inj₂ Pys
  to (x ∷ xs) ys (here Px)       = inj₁ (here Px)
  to (x ∷ xs) ys (there ∃Pxs++ys) with to xs ys ∃Pxs++ys
  ...                                | inj₁ ∃Pxs = inj₁ (there ∃Pxs)
  ...                                | inj₂ ∃Pys = inj₂ ∃Pys
  from : ∀ (xs ys : List A) →
    Any P xs ⊎ Any P ys → Any P (xs ++ ys)
  from [] ys (inj₂ ∃Pys) = ∃Pys
  from (x ∷ xs) ys (inj₁ (here Px))    = here Px
  from (x ∷ xs) ys (inj₁ (there ∃Pxs)) = there (from xs ys (inj₁ ∃Pxs))
  from (x ∷ xs) ys (inj₂ ∃Pys)         = there (from xs ys (inj₂ ∃Pys))

All-++-≃ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
  All P (xs ++ ys) ≃ (All P xs × All P ys)
All-++-≃ {A} {P} xs ys =
  record
  { to      = to      xs ys
  ; from    = from    xs ys
  ; from∘to = from∘to xs ys
  ; to∘from = to∘from xs ys
  }
  where
  to : ∀ (xs ys : List A) → All P (xs ++ ys) → (All P xs × All P ys)
  to xs ys = _⇔_.to (All-++-⇔ xs ys)

  from : ∀ (xs ys : List A) → All P xs × All P ys → All P (xs ++ ys)
  from xs ys = _⇔_.from (All-++-⇔ xs ys)

  from∘to : ∀ (xs ys : List A) (Pxs++ys : All P (xs ++ ys))
    → from xs ys (to xs ys Pxs++ys) ≡ Pxs++ys
  from∘to [] ys Pxs++ys = refl
  from∘to (x ∷ xs) ys (Px ∷ Pxs++ys) = -- cong (Px ∷_) (from∘to xs ys Pxs++ys)
    begin
      from (x ∷ xs) ys (to (x ∷ xs) ys (Px ∷ Pxs++ys))
    ≡⟨⟩
      from (x ∷ xs) ys ⟨ Px ∷ proj₁ t , proj₂ t ⟩
    ≡⟨⟩
      Px ∷ from xs ys ⟨ proj₁ t , proj₂ t ⟩
    ≡⟨⟩
      Px ∷ from xs ys (to xs ys Pxs++ys)
    ≡⟨ cong (Px ∷_) (from∘to xs ys Pxs++ys) ⟩
      Px ∷ Pxs++ys
    ∎
    where t = to xs ys Pxs++ys

  to∘from : ∀ (xs ys : List A) (Pxs×Pys : All P xs × All P ys)
    → to xs ys (from xs ys Pxs×Pys) ≡ Pxs×Pys
  to∘from [] ys ⟨ [] , Pys ⟩ = refl
  to∘from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩ =
  -- cong (λ k → ⟨ Px ∷ (proj₁ k) , proj₂ k ⟩) (to∘from xs ys ⟨ Pxs , Pys ⟩)
    begin
      to (x ∷ xs) ys (from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩)
    ≡⟨⟩
      to (x ∷ xs) ys (Px ∷ (from xs ys ⟨ Pxs , Pys ⟩))
    ≡⟨⟩
      ⟨ Px ∷ (proj₁ tf) , (proj₂ tf) ⟩
    ≡⟨ cong (λ k → ⟨ Px ∷ (proj₁ k) , proj₂ k ⟩) (to∘from xs ys ⟨ Pxs , Pys ⟩) ⟩
      ⟨ Px ∷ (proj₁ ⟨ Pxs , Pys ⟩) , (proj₂ ⟨ Pxs , Pys ⟩) ⟩
    ≡⟨⟩
      ⟨ Px ∷ Pxs , Pys ⟩
    ∎
    where tf = (to xs ys (from xs ys ⟨ Pxs , Pys ⟩))

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

¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
  → (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
¬Any≃All¬ {A} P xs =
  record
  { to      = to xs
  ; from    = from xs
  ; from∘to = from∘to xs
  ; to∘from = to∘from xs
  }
  where
  to : (xs : List A) → (¬_ ∘′ Any P) xs → All (¬_ ∘′ P) xs
  to []       ¬Any = []
  to (x ∷ xs) ¬Any = (λ Px → ¬Any (here Px)) ∷ to xs (λ Pxs → ¬Any (there Pxs))
  from : (xs : List A) → All (¬_ ∘′ P) xs → (¬_ ∘′ Any P) xs
  from (x ∷ xs) (¬Px ∷ All¬) (here Px) = ¬Px Px
  from (x ∷ xs) (¬Px ∷ All¬) (there AnyP) = from xs All¬ AnyP

  from∘to : (xs : List A) → ∀ (¬Any) → from xs (to xs ¬Any) ≡ ¬Any
  from∘to xs ¬Any = extensionality λ AnyP → ⊥-elim (¬Any AnyP)

  to∘from : (xs : List A) → ∀ (All¬) → to xs (from xs All¬) ≡ All¬
  to∘from [] [] = refl
  to∘from (x ∷ xs) (¬Px ∷ ¬Pxs) = cong (¬Px ∷_) (to∘from xs ¬Pxs)

-- ¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
--  → (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
-- doesn't hold, because we couldn't use
-- ((¬_ ∘′ All P) xs) to construct a (Any (¬_ ∘′ P) xs)

------------------------------

all : ∀ {A : Set} → (A → Bool) → List A → Bool
all p  =  foldr _∧_ true ∘ map p

Decidable : ∀ {A : Set} → (A → Set) → Set
Decidable {A} P  =  ∀ (x : A) → Dec (P x)

All? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P)
All? P? []                                 = yes []
All? P? (x ∷ xs) with P? x   | All? P? xs
...                 | yes Px | yes p₁      = yes (Px ∷ p₁)
...                 | no ¬Px | _           = no λ{ (Px ∷ Pxs) → ¬Px Px}
...                 | _      | no ¬Pxs     = no λ{ (Px ∷ Pxs) → ¬Pxs Pxs}

---------- practice ----------
any : ∀ {A : Set} → (A → Bool) → List A → Bool
any p  =  foldr _∨_ false ∘ map p

Any? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (Any P)
Any? P? [] = no (λ ())
Any? P? (x ∷ xs) with P? x   | Any? P? xs
Any? P? (x ∷ xs)    | yes Px | _        = yes (here Px)
Any? P? (x ∷ xs)    | _      | yes ∃Pxs = yes (there ∃Pxs)
Any? P? (x ∷ xs)    | no ¬Px | no ¬∃Pxs = no λ{ (here Px) → ¬Px Px
                                              ; (there ∃Px) → ¬∃Pxs ∃Px
                                              }

open import plfa-code.Quantifiers using (∀-extensionality)

-- the implicit argument x is too difficult to deal with ..
-- so I replace it with explicit

All-∀ : ∀ {A : Set} {P : A → Set} (xs : List A) →
  All P xs ≃ (∀ (x) → x ∈ xs → P x)
All-∀ {A} {P} xs =
  record
  { to      = to xs
  ; from    = from xs
  ; from∘to = from∘to xs
  ; to∘from = to∘from xs
  }
  where
  to : ∀ (xs : List A) → All P xs → (∀ (x) → x ∈ xs → P x)
  to (x₁ ∷ xs) (Px₁ ∷  _ ) .x₁ (here refl)  = Px₁
  to (x₁ ∷ xs) ( _  ∷ Pxs) x   (there x∈xs) = to xs Pxs x x∈xs

  from : ∀ (xs : List A) → (∀ (x) → x ∈ xs → P x) → All P xs
  from []       f = []
  from (x ∷ xs) f = f x (here refl) ∷ from xs (λ x₁ → (f x₁) ∘ there)

  from∘to : ∀ (xs : List A) → (Pxs : All P xs) → from xs (to xs Pxs) ≡ Pxs
  from∘to []       []         = refl
  from∘to (x ∷ xs) (Px ∷ Pxs) = cong (Px ∷_) (from∘to xs Pxs)

  to∘from : ∀ (xs : List A) → ∀ (f) → to xs (from xs f) ≡ f
  to∘from [] f = ∀-extensionality (to [] []) f
    (λ x → ∀-extensionality (to [] [] x) (f x) λ ())
  to∘from (x ∷ xs) f = ∀-extensionality (to (x ∷ xs) (from (x ∷ xs) f)) f
    (λ x₁ → ∀-extensionality (to (x ∷ xs) (from (x ∷ xs) f) x₁) (f x₁)
      λ{ (here refl) → refl
       ; (there x₁∈xs) → cong (λ g → g x₁ x₁∈xs)
                (to∘from xs (λ x₂ → (f x₂) ∘ there))
       }
    )

-- Emmmm..., "∃[ x ∈ xs ] P x" is not a valid type, I guess its real
-- meaning is like below

Any-∃ : {A : Set} {P : A → Set} (xs : List A) →
  Any P xs ≃ ∃[ x ] (x ∈ xs × P x)
Any-∃ {A} {P} xs =
  record
  { to      = to xs
  ; from    = from xs
  ; from∘to = from∘to xs
  ; to∘from = to∘from xs
  }
  where
  to : ∀ (xs : List A) → Any P xs → ∃[ x ] (x ∈ xs × P x)
  to (x ∷ xs) (here Px)         = ⟨ x , ⟨ here refl , Px ⟩ ⟩
  to (x ∷ xs) (there AnyP) with to xs AnyP
  ... | ⟨ x₁ , ⟨ x₁∈xs , Px ⟩ ⟩ = ⟨ x₁ , ⟨ there x₁∈xs , Px ⟩ ⟩

  from : ∀ (xs : List A) → ∃[ x ] (x ∈ xs × P x) → Any P xs
  from (x ∷ xs) ⟨ .x , ⟨ here refl   , Px  ⟩ ⟩ = here Px
  from (x ∷ xs) ⟨ x₁ , ⟨ there x₁∈xs , Px₁ ⟩ ⟩ = there (from xs ⟨ x₁ , ⟨ x₁∈xs , Px₁ ⟩ ⟩)

  from∘to : ∀ (xs : List A) → (AnyP : Any P xs)
    → from xs (to xs AnyP) ≡ AnyP
  from∘to (x ∷ xs) (here x₁)    = refl
  from∘to (x ∷ xs) (there AnyP) = cong there (from∘to xs AnyP)

  to∘from : ∀ (xs : List A) → ∀ ∃Pxs → to xs (from xs ∃Pxs) ≡ ∃Pxs
  to∘from (x ∷ xs) ⟨ .x , ⟨ here refl   , Px  ⟩ ⟩ = refl
  to∘from (x ∷ xs) ⟨ x₁ , ⟨ there x₁∈xs , Px₁ ⟩ ⟩
    = cong (λ a → ⟨ proj₁ a , ⟨ there (proj₁ (proj₂ a)) , proj₂ (proj₂ a) ⟩ ⟩)
           (to∘from xs ⟨ x₁ , ⟨ x₁∈xs , Px₁ ⟩ ⟩)

filter? : ∀ {A : Set} {P : A → Set}
  → (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
filter? P? [] = ⟨ [] , [] ⟩
filter? P? (x ∷ xs) with P? x   | filter? P? xs
...                    | yes Px | ⟨ ys , Pys ⟩  = ⟨ (x ∷ ys) , (Px ∷ Pys) ⟩
...                    | no ¬Px | ∃ys-Pys       = ∃ys-Pys

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code