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

open import Categories.Category.Monoidal.Structure
  using (SymmetricMonoidalCategory)

module Categories.Functor.Monoidal.Symmetric {o o′ ℓ ℓ′ e e′}
  (C : SymmetricMonoidalCategory o ℓ e) (D : SymmetricMonoidalCategory o′ ℓ′ e′)
  where

open import Level
open import Data.Product using (_,_)

open import Categories.Category using (module Commutation)
open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)

open NaturalIsomorphism

private
  module C = SymmetricMonoidalCategory C
  module D = SymmetricMonoidalCategory D

module Lax where

  -- Lax symmetric monoidal functors.

  record IsSymmetricMonoidalFunctor (F : Functor C.U D.U)
         : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F

    field
      isMonoidal : IsMonoidalFunctor C.monoidalCategory D.monoidalCategory F

    open IsMonoidalFunctor isMonoidal public
    open D
    open Commutation D.U

    -- coherence condition

    field
      braiding-compat : ∀ {X Y} →
                        [ F₀ X ⊗₀ F₀ Y                  ⇒ F₀ (Y C.⊗₀ X) ]⟨
                          ⊗-homo.η (X , Y)              ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
                          F₁ (C.braiding.⇒.η (X , Y))
                        ≈ D.braiding.⇒.η (F₀ X , F₀ Y)  ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
                          ⊗-homo.η (Y , X)
                        ⟩

  record SymmetricMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F                   : Functor C.U D.U
      isSymmetricMonoidal : IsSymmetricMonoidalFunctor F

    open Functor F public
    open IsSymmetricMonoidalFunctor isSymmetricMonoidal public

    monoidalFunctor : MonoidalFunctor C.monoidalCategory D.monoidalCategory
    monoidalFunctor = record { F = F ; isMonoidal = isMonoidal }

module Strong where

  -- Strong symmetric monoidal functors.

  record IsSymmetricMonoidalFunctor (F : Functor C.U D.U)
         : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F

    field
      isStrongMonoidal : IsStrongMonoidalFunctor C.monoidalCategory
                                                 D.monoidalCategory F

    open IsStrongMonoidalFunctor isStrongMonoidal public
    open D
    open Commutation D.U

    -- coherence condition

    field
      braiding-compat : ∀ {X Y} →
                        [ F₀ X ⊗₀ F₀ Y                  ⇒ F₀ (Y C.⊗₀ X) ]⟨
                          ⊗-homo.⇒.η (X , Y)            ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
                          F₁ (C.braiding.⇒.η (X , Y))
                        ≈ D.braiding.⇒.η (F₀ X , F₀ Y)  ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
                          ⊗-homo.⇒.η (Y , X)
                        ⟩

    isLaxSymmetricMonoidal : Lax.IsSymmetricMonoidalFunctor F
    isLaxSymmetricMonoidal = record
      { isMonoidal      = isMonoidal
      ; braiding-compat = braiding-compat
      }

  record SymmetricMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F                   : Functor C.U D.U
      isSymmetricMonoidal : IsSymmetricMonoidalFunctor F

    open Functor F public
    open IsSymmetricMonoidalFunctor isSymmetricMonoidal public

    monoidalFunctor : StrongMonoidalFunctor C.monoidalCategory
                                            D.monoidalCategory
    monoidalFunctor = record { F = F ; isStrongMonoidal = isStrongMonoidal }

max_stars_repo_name: FintanH/agda-categories

max_issues_repo_name: andrejbauer/agda-categories

max_forks_repo_name: andrejbauer/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets
------------------------------------------------------------------------

-- Note that elements of Fin n can be seen as natural numbers in the
-- set {m | m < n}. The notation "m" in comments below refers to this
-- natural number view.

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

module Data.Fin.Base where

open import Data.Empty using (⊥-elim)
open import Data.Nat as ℕ
  using (ℕ; zero; suc; z≤n; s≤s)
open import Function using (_∘_; _on_)
open import Level using () renaming (zero to ℓ₀)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; cong)

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

-- Fin n is a type with n elements.

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

-- A conversion: toℕ "i" = i.

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

-- A Fin-indexed variant of Fin.

Fin′ : ∀ {n} → Fin n → Set
Fin′ i = Fin (toℕ i)

------------------------------------------------------------------------
-- A cast that actually computes on constructors (as opposed to subst)

cast : ∀ {m n} → .(_ : m ≡ n) → Fin m → Fin n
cast {zero}  {zero}  eq k       = k
cast {suc m} {suc n} eq zero    = zero
cast {suc m} {suc n} eq (suc k) = suc (cast (cong ℕ.pred eq) k)
cast {zero}  {suc n} ()
cast {suc m} {zero}  ()

------------------------------------------------------------------------
-- Conversions

-- toℕ is defined above.

-- fromℕ n = "n".

fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

-- fromℕ≤ {m} _ = "m".

fromℕ≤ : ∀ {m n} → m ℕ.< n → Fin n
fromℕ≤ (s≤s z≤n)       = zero
fromℕ≤ (s≤s (s≤s m≤n)) = suc (fromℕ≤ (s≤s m≤n))

-- fromℕ≤″ m _ = "m".

fromℕ≤″ : ∀ m {n} → m ℕ.<″ n → Fin n
fromℕ≤″ zero    (ℕ.less-than-or-equal refl) = zero
fromℕ≤″ (suc m) (ℕ.less-than-or-equal refl) =
  suc (fromℕ≤″ m (ℕ.less-than-or-equal refl))

-- # m = "m".

infix 10 #_

#_ : ∀ m {n} {m<n : True (suc m ℕ.≤? n)} → Fin n
#_ _ {m<n = m<n} = fromℕ≤ (toWitness m<n)

-- raise m "i" = "m + i".

raise : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
raise zero    i = i
raise (suc n) i = suc (raise n i)

-- reduce≥ "m + i" _ = "i".

reduce≥ : ∀ {m n} (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m) → Fin n
reduce≥ {zero}  i       i≥m       = i
reduce≥ {suc m} zero    ()
reduce≥ {suc m} (suc i) (s≤s i≥m) = reduce≥ i i≥m

-- inject⋆ m "i" = "i".

inject : ∀ {n} {i : Fin n} → Fin′ i → Fin n
inject {i = zero}  ()
inject {i = suc i} zero    = zero
inject {i = suc i} (suc j) = suc (inject j)

inject! : ∀ {n} {i : Fin (suc n)} → Fin′ i → Fin n
inject! {n = zero}  {i = suc ()} _
inject!             {i = zero}   ()
inject! {n = suc _} {i = suc _}  zero    = zero
inject! {n = suc _} {i = suc _}  (suc j) = suc (inject! j)

inject+ : ∀ {m} n → Fin m → Fin (m ℕ.+ n)
inject+ n zero    = zero
inject+ n (suc i) = suc (inject+ n i)

inject₁ : ∀ {m} → Fin m → Fin (suc m)
inject₁ zero    = zero
inject₁ (suc i) = suc (inject₁ i)

inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
inject≤ zero    (s≤s le) = zero
inject≤ (suc i) (s≤s le) = suc (inject≤ i le)

-- lower₁ "i" _ = "i".

lower₁ : ∀ {n} → (i : Fin (suc n)) → (n ≢ toℕ i) → Fin n
lower₁ {zero} zero ne = ⊥-elim (ne refl)
lower₁ {zero} (suc ()) _
lower₁ {suc n} zero _ = zero
lower₁ {suc n} (suc i) ne = suc (lower₁ i λ x → ne (cong suc x))

-- A strengthening injection into the minimal Fin fibre.
strengthen : ∀ {n} (i : Fin n) → Fin′ (suc i)
strengthen zero    = zero
strengthen (suc i) = suc (strengthen i)

------------------------------------------------------------------------
-- Operations

-- Folds.

fold : ∀ {t} (T : ℕ → Set t) {m} →
       (∀ {n} → T n → T (suc n)) →
       (∀ {n} → T (suc n)) →
       Fin m → T m
fold T f x zero    = x
fold T f x (suc i) = f (fold T f x i)

fold′ : ∀ {n t} (T : Fin (suc n) → Set t) →
        (∀ i → T (inject₁ i) → T (suc i)) →
        T zero →
        ∀ i → T i
fold′             T f x zero     = x
fold′ {n = zero}  T f x (suc ())
fold′ {n = suc n} T f x (suc i)  =
  f i (fold′ (T ∘ inject₁) (f ∘ inject₁) x i)

-- Lifts functions.

lift : ∀ {m n} k → (Fin m → Fin n) → Fin (k ℕ.+ m) → Fin (k ℕ.+ n)
lift zero    f i       = f i
lift (suc k) f zero    = zero
lift (suc k) f (suc i) = suc (lift k f i)

-- "i" + "j" = "i + j".

infixl 6 _+_

_+_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (toℕ i ℕ.+ n)
zero  + j = j
suc i + j = suc (i + j)

-- "i" - "j" = "i ∸ j".

infixl 6 _-_

_-_ : ∀ {m} (i : Fin m) (j : Fin′ (suc i)) → Fin (m ℕ.∸ toℕ j)
i     - zero   = i
zero  - suc ()
suc i - suc j  = i - j

-- m ℕ- "i" = "m ∸ i".

infixl 6 _ℕ-_

_ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
n     ℕ- zero   = fromℕ n
zero  ℕ- suc ()
suc n ℕ- suc i  = n ℕ- i

-- m ℕ-ℕ "i" = m ∸ i.

infixl 6 _ℕ-ℕ_

_ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
n     ℕ-ℕ zero   = n
zero  ℕ-ℕ suc ()
suc n ℕ-ℕ suc i  = n ℕ-ℕ i

-- pred "i" = "pred i".

pred : ∀ {n} → Fin n → Fin n
pred zero    = zero
pred (suc i) = inject₁ i

-- The function f(i,j) = if j>i then j-1 else j
-- This is a variant of the thick function from Conor
-- McBride's "First-order unification by structural recursion".

punchOut : ∀ {m} {i j : Fin (suc m)} → i ≢ j → Fin m
punchOut {_}     {zero}   {zero}  i≢j = ⊥-elim (i≢j refl)
punchOut {_}     {zero}   {suc j} _   = j
punchOut {zero}  {suc ()}
punchOut {suc m} {suc i}  {zero}  _   = zero
punchOut {suc m} {suc i}  {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))

-- The function f(i,j) = if j≥i then j+1 else j

punchIn : ∀ {m} → Fin (suc m) → Fin m → Fin (suc m)
punchIn zero    j       = suc j
punchIn (suc i) zero    = zero
punchIn (suc i) (suc j) = suc (punchIn i j)

------------------------------------------------------------------------
-- Order relations

infix 4 _≤_ _<_

_≤_ : ∀ {n} → Rel (Fin n) ℓ₀
_≤_ = ℕ._≤_ on toℕ

_<_ : ∀ {n} → Rel (Fin n) ℓ₀
_<_ = ℕ._<_ on toℕ

data _≺_ : ℕ → ℕ → Set where
  _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n

------------------------------------------------------------------------
-- An ordering view.

data Ordering {n : ℕ} : Fin n → Fin n → Set where
  less    : ∀ greatest (least : Fin′ greatest) →
            Ordering (inject least) greatest
  equal   : ∀ i → Ordering i i
  greater : ∀ greatest (least : Fin′ greatest) →
            Ordering greatest (inject least)

compare : ∀ {n} (i j : Fin n) → Ordering i j
compare zero    zero    = equal   zero
compare zero    (suc j) = less    (suc j) zero
compare (suc i) zero    = greater (suc i) zero
compare (suc i) (suc j) with compare i j
compare (suc .(inject least)) (suc .greatest) | less    greatest least =
  less    (suc greatest) (suc least)
compare (suc .greatest) (suc .(inject least)) | greater greatest least =
  greater (suc greatest) (suc least)
compare (suc .i)        (suc .i)              | equal i =
  equal (suc i)

ext: agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

postulate
  A : Set

data Unit : Set where
  unit : Unit

F : Unit → Set
F unit = A

postulate
  P : {A : Set} → A → Set
  Q : ∀ {x} → F x → Set
  f : ∀ {x} {y : F x} (z : Q y) → P z

variable
  x : Unit
  y : F x

g : (z : Q y) → P z
g z with f z
... | p = p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Categories.Instances.EilenbergMoore where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
open import Cubical.Foundations.Univalence

open import Cubical.Categories.Category
open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Categories.Monad.Base
open import Cubical.Categories.Instances.FunctorAlgebras
open import Cubical.Categories.Constructions.FullSubcategory
open import Cubical.Categories.Adjoint

private
  variable
    ℓC ℓC' : Level

module _ {C : Category ℓC ℓC'} (monadM : Monad C) where

  private
    M : Functor C C
    M = fst monadM

  --open Category
  private
    module C = Category C
  open Functor
  open NatTrans

  open IsMonad (snd monadM)

  record IsEMAlgebra (algA : Algebra M) : Type ℓC' where
    constructor proveEMAlgebra
    open Algebra algA
    field
      str-η : str C.∘ N-ob η carrier ≡ C.id
      str-μ : str C.∘ N-ob μ carrier ≡ str C.∘ F-hom M str

  open IsEMAlgebra

  isPropIsEMAlgebra : ∀ {algA} → isProp (IsEMAlgebra algA)
  isPropIsEMAlgebra {algA} isalg isalg' = cong₂ proveEMAlgebra
    (C.isSetHom _ _ (str-η isalg) (str-η isalg'))
    (C.isSetHom _ _ (str-μ isalg) (str-μ isalg'))

  EMAlgebra : Type (ℓ-max ℓC ℓC')
  EMAlgebra = Σ[ algA ∈ Algebra M ] IsEMAlgebra algA

  EMCategory : Category (ℓ-max (ℓ-max ℓC ℓC') ℓC') ℓC'
    -- cannot simplify level: --experimental-lossy-unification won't allow it.
  EMCategory = FullSubcategory (AlgebrasCategory M) IsEMAlgebra

  ForgetEM : Functor EMCategory (AlgebrasCategory M)
  ForgetEM = FullInclusion (AlgebrasCategory M) IsEMAlgebra

  ForgetEMAlgebra : Functor EMCategory C
  ForgetEMAlgebra = funcComp (ForgetAlgebra M) ForgetEM

  open Algebra
  freeEMAlgebra : C.ob → EMAlgebra
  carrier (fst (freeEMAlgebra x)) = F-ob M x
  str (fst (freeEMAlgebra x)) = N-ob μ x
  str-η (snd (freeEMAlgebra x)) = lemma
    where lemma : N-ob η (F-ob M x) C.⋆ N-ob μ x ≡ C.id
          lemma = funExt⁻ (congP (λ i → N-ob) idl-μ) x
  str-μ (snd (freeEMAlgebra x)) = lemma
    where lemma : N-ob μ (F-ob M x) C.⋆ N-ob μ x ≡ F-hom M (N-ob μ x) C.⋆ N-ob μ x
          lemma = funExt⁻ (congP (λ i → N-ob) (symP-fromGoal assoc-μ)) x

  open AlgebraHom
  FreeEMAlgebra : Functor C EMCategory
  F-ob FreeEMAlgebra x = freeEMAlgebra x
  carrierHom (F-hom FreeEMAlgebra {x} {y} φ) = F-hom M φ
  strHom (F-hom FreeEMAlgebra {x} {y} φ) = sym (N-hom μ φ)
  F-id FreeEMAlgebra = AlgebraHom≡ M (F-id M)
  F-seq FreeEMAlgebra {x} {y} {z} φ ψ = AlgebraHom≡ M (F-seq M φ ψ)

  ForgetFreeEMAlgebra : funcComp ForgetEMAlgebra FreeEMAlgebra ≡ M
  ForgetFreeEMAlgebra = Functor≡ (λ x → refl) (λ f → refl)

  emCounit : NatTrans (funcComp FreeEMAlgebra ForgetEMAlgebra) (funcId EMCategory)
  carrierHom (N-ob emCounit (algebra A α , isEMA)) = α
  strHom (N-ob emCounit (algebra A α , isEMA)) = str-μ isEMA
  N-hom emCounit {algebra A α , isEMA} {algebra B β , isEMB} (algebraHom f isalgF) =
    AlgebraHom≡ M (sym (isalgF))

  open NaturalBijection
  open _⊣_
  open _≅_

  emBijection : ∀ a emB →
    (EMCategory [ FreeEMAlgebra ⟅ a ⟆ , emB ]) ≅ (C [ a , ForgetEMAlgebra ⟅ emB ⟆ ])
  fun (emBijection a (algebra b β , isEMB)) (algebraHom f isalgF) = f C.∘ N-ob η a
  carrierHom (inv (emBijection a (algebra b β , isEMB)) f) = β C.∘ F-hom M f
  strHom (inv (emBijection a (algebra b β , isEMB)) f) =
    (N-ob μ a C.⋆ (F-hom M f C.⋆ β))
      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
    ((N-ob μ a C.⋆ F-hom M f) C.⋆ β)
      ≡⟨ cong (C._⋆ β) (sym (N-hom μ f)) ⟩
    ((F-hom M (F-hom M f) C.⋆ N-ob μ b) C.⋆ β)
      ≡⟨ C.⋆Assoc _ _ _ ⟩
    (F-hom M (F-hom M f) C.⋆ (N-ob μ b C.⋆ β))
      ≡⟨ cong (F-hom M (F-hom M f) C.⋆_) (str-μ isEMB) ⟩
    (F-hom M (F-hom M f) C.⋆ (F-hom M β C.⋆ β))
      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
    ((F-hom M (F-hom M f) C.⋆ F-hom M β) C.⋆ β)
      ≡⟨ cong (C._⋆ β) (sym (F-seq M _ _)) ⟩
    (F-hom M (F-hom M f C.⋆ β) C.⋆ β) ∎
  rightInv (emBijection a (algebra b β , isEMB)) f =
    (N-ob η a C.⋆ (F-hom M f C.⋆ β))
      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
    ((N-ob η a C.⋆ F-hom M f) C.⋆ β)
      ≡⟨ cong (C._⋆ β) (sym (N-hom η f)) ⟩
    ((f C.⋆ N-ob η b) C.⋆ β)
      ≡⟨ C.⋆Assoc _ _ _ ⟩
    (f C.⋆ (N-ob η b C.⋆ β))
      ≡⟨ cong (f C.⋆_) (str-η isEMB) ⟩
    (f C.⋆ C.id)
      ≡⟨ C.⋆IdR _ ⟩
    f ∎
  leftInv (emBijection a (algebra b β , isEMB)) (algebraHom f isalgF) = AlgebraHom≡ M (
    (F-hom M (N-ob η a C.⋆ f) C.⋆ β)
      ≡⟨ cong (C._⋆ β) (F-seq M _ _) ⟩
    ((F-hom M (N-ob η a) C.⋆ F-hom M f) C.⋆ β)
      ≡⟨ C.⋆Assoc _ _ _ ⟩
    (F-hom M (N-ob η a) C.⋆ (F-hom M f C.⋆ β))
      ≡⟨ cong (F-hom M (N-ob η a) C.⋆_) (sym isalgF) ⟩
    (F-hom M (N-ob η a) C.⋆ (N-ob μ a C.⋆ f))
      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
    ((F-hom M (N-ob η a) C.⋆ N-ob μ a) C.⋆ f)
      ≡⟨ cong (C._⋆ f) (funExt⁻ (congP (λ i → N-ob) idr-μ) a) ⟩
    (C.id C.⋆ f)
      ≡⟨ C.⋆IdL f ⟩
    f ∎
    )

  emAdjunction : FreeEMAlgebra ⊣ ForgetEMAlgebra
  adjIso emAdjunction {a} {algebra b β , isEMB} = emBijection a (algebra b β , isEMB)
  adjNatInD emAdjunction {a} {algebra b β , isEMB} {algebra c γ , isEMC}
    (algebraHom f isalgF) (algebraHom g isalgG) =
    sym (C.⋆Assoc _ _ _)
  adjNatInC emAdjunction {a} {b} {algebra c γ , isEMC} f g = AlgebraHom≡ M (
    (F-hom M (g C.⋆ f) C.⋆ γ)
      ≡⟨ cong (C._⋆ γ) (F-seq M _ _) ⟩
    ((F-hom M g C.⋆ F-hom M f) C.⋆ γ)
      ≡⟨ C.⋆Assoc _ _ _ ⟩
    (F-hom M g C.⋆ (F-hom M f C.⋆ γ)) ∎
    )

module _ {C : Category ℓC ℓC'} {monadM monadN : Monad C} (monadν : MonadHom monadM monadN) where

  open Category C
  open Functor
  open IsEMAlgebra
  open NatTrans

  private
    M N : Functor C C
    M = fst monadM
    N = fst monadN
    module M = IsMonad (snd monadM)
    module N = IsMonad (snd monadN)
    ν : NatTrans M N
    ν = fst monadν
    module ν = IsMonadHom (snd monadν)

  mapIsEMAlgebra : (algA : Algebra N) → IsEMAlgebra monadN algA → IsEMAlgebra monadM (F-ob (AlgebrasFunctor ν) algA)
  str-η (mapIsEMAlgebra (algebra a αN) isEMA) =
    N-ob M.η a ⋆ (N-ob ν a ⋆ αN)
      ≡⟨ sym (⋆Assoc _ _ _) ⟩
    (N-ob M.η a ⋆ N-ob ν a) ⋆ αN
      ≡⟨ cong (_⋆ αN) (cong (λ θ → N-ob θ a) ν.N-η) ⟩
    N-ob N.η a ⋆ αN
      ≡⟨ isEMA .str-η ⟩
    id ∎
  str-μ (mapIsEMAlgebra (algebra a αN) isEMA) =
    N-ob M.μ a ⋆ (N-ob ν a ⋆ αN)
      ≡⟨ sym (⋆Assoc _ _ _) ⟩
    (N-ob M.μ a ⋆ N-ob ν a) ⋆ αN
      ≡⟨ cong (_⋆ αN) (cong (λ θ → N-ob θ a) ν.N-μ) ⟩
    ((F-hom M (N-ob ν a) ⋆ N-ob ν (F-ob N a)) ⋆ N-ob N.μ a) ⋆ αN
      ≡⟨ ⋆Assoc _ _ _ ⟩
    (F-hom M (N-ob ν a) ⋆ N-ob ν (F-ob N a)) ⋆ (N-ob N.μ a ⋆ αN)
      ≡⟨ cong ((F-hom M (N-ob ν a) ⋆ N-ob ν (F-ob N a)) ⋆_) (isEMA .str-μ) ⟩
    (F-hom M (N-ob ν a) ⋆ N-ob ν (F-ob N a)) ⋆ (F-hom N αN ⋆ αN)
      ≡⟨ sym (⋆Assoc _ _ _) ⟩
    ((F-hom M (N-ob ν a) ⋆ N-ob ν (F-ob N a)) ⋆ F-hom N αN) ⋆ αN
      ≡⟨ cong (_⋆ αN) (⋆Assoc _ _ _) ⟩
    (F-hom M (N-ob ν a) ⋆ (N-ob ν (F-ob N a) ⋆ F-hom N αN)) ⋆ αN
      ≡⟨ cong (_⋆ αN) (cong (F-hom M (N-ob ν a) ⋆_) (sym (N-hom ν αN))) ⟩
    (F-hom M (N-ob ν a) ⋆ (F-hom M αN ⋆ N-ob ν a)) ⋆ αN
      ≡⟨ cong (_⋆ αN) (sym (⋆Assoc _ _ _)) ⟩
    ((F-hom M (N-ob ν a) ⋆ F-hom M αN) ⋆ N-ob ν a) ⋆ αN
      ≡⟨ cong (_⋆ αN) (cong (_⋆ N-ob ν a) (sym (F-seq M _ _))) ⟩
    (F-hom M (N-ob ν a ⋆ αN) ⋆ N-ob ν a) ⋆ αN
      ≡⟨ ⋆Assoc _ _ _ ⟩
    F-hom M (N-ob ν a ⋆ αN) ⋆ (N-ob ν a ⋆ αN) ∎

  EMFunctor : Functor (EMCategory monadN) (EMCategory monadM)
  EMFunctor = MapFullSubcategory
    (AlgebrasCategory N) (IsEMAlgebra monadN)
    (AlgebrasCategory M) (IsEMAlgebra monadM)
    (AlgebrasFunctor ν) mapIsEMAlgebra

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ where

open import Issue1839.A
open import Issue1839.B

X : DontPrintThis    -- should display as PrintThis
X = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Some code suggesting that types used in "programs" might not
-- necessarily be sets
------------------------------------------------------------------------

-- If lenses are only used in programs, and types used in programs are
-- always sets, then higher lenses might be pointless.

-- This module uses univalence without tracking such uses in the types
-- of functions.

{-# OPTIONS --cubical #-}

open import Equality.Path as P hiding (Is-proposition; Is-set)

module README.Not-a-set
  {e⁺} (eq : ∀ {a p} → Equality-with-paths a p e⁺) where

private
  open module D = Derived-definitions-and-properties eq
    using (Is-proposition; Is-set)

open import Equality.Path.Univalence
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
import Bijection D.equality-with-J as DB
import Bool equality-with-J as B
open import Equality.Decision-procedures equality-with-J
import Equality.Path.Isomorphisms eq as I
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
import H-level D.equality-with-J as H-level
open import H-level.Closure D.equality-with-J
open import Surjection D.equality-with-J using (_↠_)

private
  variable
    A B C : Type

------------------------------------------------------------------------
-- Dynamic types

-- Values of arbitrary type that can be turned into strings.

Printable : Type₁
Printable = ∃ λ (A : Type) → A × (A → String)

-- Printable is not a set.

¬-Printable-set : ¬ Is-set Printable
¬-Printable-set =
  Is-set Printable        ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
  P.Is-set Printable      ↝⟨ (λ h → h _ _) ⟩
  refl ≡ q                ↝⟨ cong (cong proj₁) ⟩
  refl ≡ cong proj₁ q     ↝⟨ flip trans (proj₁-Σ-≡,≡→≡ {B = λ A → A × (A → String)} {y₁ = proj₂ x} _ refl) ⟩
  refl ≡ q′               ↝⟨ cong (λ eq → subst id eq (just true)) ⟩
  just true ≡ just false  ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
  ⊥                       □
  where
  x : Printable
  x = Maybe Bool , nothing , λ _ → ""

  q′ : Maybe Bool ≡ Maybe Bool
  q′ = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)

  q : x ≡ x
  q = Σ-≡,≡→≡ q′ refl

------------------------------------------------------------------------
-- Streams

-- Streams, based on the definition given by Coutts et al. in "Stream
-- Fusion: From Lists to Streams to Nothing at All".

data Step (A S : Type) : Type where
  done  : Step A S
  yield : A → S → Step A S
  skip  : S → Step A S

Stream : Type → Type₁
Stream A = ∃ λ (S : Type) → (S → Step A S) × S

-- Stream A is not a set.

¬-Stream-set : ¬ Is-set (Stream A)
¬-Stream-set {A = A} =
  Is-set (Stream A)       ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
  P.Is-set (Stream A)     ↝⟨ (λ h → h _ _) ⟩
  refl ≡ p                ↝⟨ cong (cong proj₁) ⟩
  refl ≡ cong proj₁ p     ↝⟨ flip trans (proj₁-Σ-≡,≡→≡ {B = F} {y₁ = proj₂ t} _ refl) ⟩
  refl ≡ q                ↝⟨ cong (λ eq → subst id eq (just true)) ⟩
  just true ≡ just false  ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
  ⊥                       □
  where
  F : Type → Type
  F S = (S → Step A S) × S

  t : Stream A
  t = Maybe Bool
    , const done
    , nothing

  q : Maybe Bool ≡ Maybe Bool
  q = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)

  p : t ≡ t
  p = Σ-≡,≡→≡ q refl

-- Streams, with the added requirement that the state type must be a
-- set.

Streamˢ : Type → Type₁
Streamˢ A = ∃ λ (S : Type) → Is-set S × (S → Step A S) × S

-- Streamˢ A is not a set.

¬-Streamˢ-set : ¬ Is-set (Streamˢ A)
¬-Streamˢ-set {A = A} =
  Is-set (Streamˢ A)      ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
  P.Is-set (Streamˢ A)    ↝⟨ (λ h → h _ _) ⟩
  refl ≡ p                ↝⟨ cong (cong proj₁) ⟩
  refl ≡ cong proj₁ p     ↝⟨ flip trans (proj₁-Σ-≡,≡→≡ {B = F} {y₁ = proj₂ t} _ refl) ⟩
  refl ≡ q                ↝⟨ cong (λ eq → subst id eq (inj₂ true)) ⟩
  just true ≡ just false  ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
  ⊥                       □
  where
  F : Type → Type
  F S = Is-set S × (S → Step A S) × S

  t : Streamˢ A
  t = Maybe Bool
    , Maybe-closure 0 Bool-set
    , const done
    , nothing

  q : Maybe Bool ≡ Maybe Bool
  q = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)

  p : t ≡ t
  p =
    Σ-≡,≡→≡ q $
    cong₂ _,_
      (DB._↔_.to D.≡↔≡ (H-level-propositional I.ext 2 _ _))
      refl

------------------------------------------------------------------------
-- Some deep embeddings

-- The module is parametrised by a predicate P that satisfies some
-- properties.

module Tm-with-predicate
  (P : Type → Type)
  (P-Maybe-Bool : P (Maybe Bool))
  (P-Maybe-Bool-propositional : Is-proposition (P (Maybe Bool)))
  where

  -- A deep embedding of a simple programming language. Note the
  -- requirement that P B must hold.

  data Tm (A : Type) : Type₁ where
    literal : A → Tm A
    map     : {B : Type} → P B → Tm (B → A) → Tm B → Tm A

  -- An unfolding lemma.

  Tm≃ : Tm A ≃ (A ⊎ ∃ λ (B : Type) → P B × Tm (B → A) × Tm B)
  Tm≃ = Eq.↔→≃
    (λ where
       (literal x) → inj₁ x
       (map p f t) → inj₂ (_ , p , f , t))
    [ literal , (λ (_ , p , f , t) → map p f t) ]
    [ (λ _ → refl) , (λ _ → refl) ]
    (λ where
       (literal _) → refl
       (map _ _ _) → refl)

  -- If A is inhabited, then Tm A is not a set.

  ¬-Tm-set : A → ¬ Is-set (Tm A)
  ¬-Tm-set {A = A} a =
    Is-set (Tm A)           ↝⟨ DB._↔_.to (I.H-level↔H-level 2) ⟩
    P.Is-set (Tm A)         ↝⟨ (λ h → h _ _) ⟩
    refl ≡ p                ↝⟨ cong map-injective ⟩
    refl ≡ map-injective p  ↝⟨ flip trans lemma ⟩
    refl ≡ p₁               ↝⟨ cong (λ eq → subst id eq (just true)) ⟩
    just true ≡ just false  ↝⟨ Bool.true≢false ∘ ⊎.cancel-inj₂ ⟩□
    ⊥                       □
    where
    F : Type → Type₁
    F B = P B × Tm (B → A) × Tm B

    t : Tm A
    t = map P-Maybe-Bool (literal λ _ → a) (literal nothing)

    t′ : F (Maybe Bool)
    t′ = P-Maybe-Bool
       , literal (const a)
       , literal nothing

    p₁ : Maybe Bool ≡ Maybe Bool
    p₁ = ≃⇒≡ (F.id ⊎-cong Eq.↔⇒≃ B.swap)

    p₂ : subst F p₁ t′ ≡ t′
    p₂ =
      cong₂ _,_
        (DB._↔_.to (I.H-level↔H-level 1) P-Maybe-Bool-propositional _ _)
        (cong (_, literal nothing)
           (subst (λ B → Tm (B → A)) p₁ (literal (const a))  ≡⟨⟩
            literal (subst (λ B → B → A) p₁ (const a))       ≡⟨ (cong literal $ ⟨ext⟩ λ b → subst-→-domain id p₁ {u = b}) ⟩∎
            literal (const a)                                ∎))

    p : t ≡ t
    p = _≃_.to (Eq.≃-≡ Tm≃) $ cong inj₂ $ Σ-≡,≡→≡ p₁ p₂

    map-injective :
      {p : P B} {f : Tm (B → C)} {t : Tm B} →
      map p f t ≡ map p f t → B ≡ B
    map-injective {B = B} {p = p} {f = f} {t = t} =
      map p f t ≡ map p f t                            ↔⟨ inverse $ Eq.≃-≡ Tm≃ ⟩
      _≃_.to Tm≃ (map p f t) ≡ _≃_.to Tm≃ (map p f t)  ↔⟨⟩
      inj₂ (B , p , f , t) ≡ inj₂ (B , p , f , t)      ↔⟨ inverse Bijection.≡↔inj₂≡inj₂ ⟩
      (B , p , f , t) ≡ (B , p , f , t)                ↝⟨ cong proj₁ ⟩□
      B ≡ B                                            □

    lemma : map-injective p ≡ p₁
    lemma =
      map-injective p                                ≡⟨⟩

      cong proj₁ (⊎.cancel-inj₂
        (_≃_.from (Eq.≃-≡ Tm≃) (_≃_.to (Eq.≃-≡ Tm≃)
           (cong inj₂ (Σ-≡,≡→≡ p₁ p₂)))))            ≡⟨ cong (cong proj₁ ∘ ⊎.cancel-inj₂) $
                                                        _≃_.left-inverse-of (Eq.≃-≡ Tm≃) (cong inj₂ (Σ-≡,≡→≡ p₁ p₂)) ⟩
      cong (proj₁ {B = F})
        (⊎.cancel-inj₂ {A = ⊤ ⊎ ⊤} (cong inj₂
           (Σ-≡,≡→≡ {p₁ = _ , t′} p₁ p₂)))           ≡⟨ cong (cong (proj₁ {B = F})) $
                                                        _↔_.left-inverse-of (Bijection.≡↔inj₂≡inj₂ {A = ⊤ ⊎ ⊤}) (Σ-≡,≡→≡ {p₁ = _ , t′} _ refl) ⟩
      cong (proj₁ {B = F})
        (Σ-≡,≡→≡ {p₁ = _ , t′} p₁ p₂)                ≡⟨ proj₁-Σ-≡,≡→≡ {B = F} {y₁ = t′} _ refl ⟩∎

      p₁                                             ∎

-- A deep embedding of a simple programming language.

data Tm (A : Type) : Type₁ where
  literal : A → Tm A
  map     : {B : Type} → Tm (B → A) → Tm B → Tm A

-- If A is inhabited, then Tm A is not a set.

¬-Tm-set : A → ¬ Is-set (Tm A)
¬-Tm-set {A = A} a =
  Is-set (Tm A)    ↝⟨ H-level.respects-surjection Tm↠Tm 2 ⟩
  Is-set (T.Tm A)  ↝⟨ T.¬-Tm-set a ⟩□
  ⊥                □
  where
  module T = Tm-with-predicate (λ _ → ⊤) _ (λ _ _ → D.refl _)

  to : Tm B → T.Tm B
  to (literal x) = T.literal x
  to (map f t)   = T.map _ (to f) (to t)

  from : T.Tm B → Tm B
  from (T.literal x) = literal x
  from (T.map _ f t) = map (from f) (from t)

  to-from : (t : T.Tm B) → to (from t) D.≡ t
  to-from (T.literal x) = D.refl _
  to-from (T.map _ f t) = D.cong₂ (T.map _) (to-from f) (to-from t)

  Tm↠Tm : Tm B ↠ T.Tm B
  Tm↠Tm = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to-from
    }

-- A deep embedding of a simple programming language. Note the
-- requirement that "B" must be a set.

data Tmˢ (A : Type) : Type₁ where
  literal : A → Tmˢ A
  map     : {B : Type} → Is-set B → Tmˢ (B → A) → Tmˢ B → Tmˢ A

-- If A is inhabited, then Tmˢ A is not a set.

¬-Tmˢ-set : A → ¬ Is-set (Tmˢ A)
¬-Tmˢ-set {A = A} a =
  Is-set (Tmˢ A)   ↝⟨ H-level.respects-surjection Tmˢ↠Tm 2 ⟩
  Is-set (T.Tm A)  ↝⟨ T.¬-Tm-set a ⟩□
  ⊥                □
  where
  module T = Tm-with-predicate
    Is-set
    (Maybe-closure 0 Bool-set)
    (H-level-propositional I.ext 2)

  to : Tmˢ B → T.Tm B
  to (literal x) = T.literal x
  to (map s f t) = T.map s (to f) (to t)

  from : T.Tm B → Tmˢ B
  from (T.literal x) = literal x
  from (T.map s f t) = map s (from f) (from t)

  to-from : (t : T.Tm B) → to (from t) D.≡ t
  to-from (T.literal x) = D.refl _
  to-from (T.map s f t) = D.cong₂ (T.map s) (to-from f) (to-from t)

  Tmˢ↠Tm : Tmˢ B ↠ T.Tm B
  Tmˢ↠Tm = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to-from
    }

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the generic n-ary operations the stdlib provides
-- can be used
------------------------------------------------------------------------

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

module README.Nary where

open import Level using (Level)
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; #_; inject₁)
open import Data.List
open import Data.List.Properties
open import Data.Product using (_×_; _,_)
open import Data.Sum using (inj₁; inj₂)
open import Function
open import Relation.Nullary
open import Relation.Binary using (module Tri); open Tri
open import Relation.Binary.PropositionalEquality

private
  variable
    a b c d e : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e

------------------------------------------------------------------------
-- Introduction
------------------------------------------------------------------------

-- Function.Nary.NonDependent and Data.Product.N-ary.Heterogeneous provide
-- a generic representation of n-ary heterogeneous (non dependent) products
-- and the corresponding types of (non-dependent) n-ary functions. The
-- representation works well with inference thus allowing us to use generic
-- combinators to manipulate such functions.

open import Data.Product.Nary.NonDependent
open import Function.Nary.NonDependent
open import Relation.Nary

------------------------------------------------------------------------
-- Generalised equality-manipulating combinators
------------------------------------------------------------------------

-- By default the standard library provides users with (we are leaving out
-- the implicit arguments here):
--
-- cong   : (f : A₁      → B) → a₁ ≡ b₁           → f a₁   ≡ f b₁
-- cong₂  : (f : A₁ → A₂ → B) → a₁ ≡ b₁ → a₂ ≡ b₂ → f a₁ a₂ ≡ f b₁ b₂
--
-- and
--
-- subst  : (P : A₁      → Set p) → a₁ ≡ b₁           → P a₁    → P b₁
-- subst₂ : (P : A₁ → A₂ → Set p) → a₁ ≡ b₁ → a₂ ≡ b₂ → P a₁ a₂ → P b₁ b₂
--
-- This pattern can be generalised to any natural number `n`. Thanks to our
-- library for n-ary functions, we can write the types and implementations
-- of `congₙ` and `substₙ`.

------------------------------------------------------------------------
-- congₙ : ∀ n (f : A₁ → ⋯ → Aₙ → B) →
--         a₁ ≡ b₁ → ⋯ aₙ ≡ bₙ → f a₁ ⋯ aₙ ≡ f b₁ ⋯ bₙ

-- It may be used directly to prove something:

_ : ∀ (as bs cs : List ℕ) →
       zip (zip (as ++ []) (map id cs)) (reverse (reverse bs))
     ≡ zip (zip as cs) bs
_ = λ as bs cs → congₙ 3 (λ as bs → zip (zip as bs))
                         (++-identityʳ as)
                         (map-id cs)
                         (reverse-involutive bs)

-- Or as part of a longer derivation:

_ : ∀ m n p q → suc (m + (p * n) + (q ^ (m + n)))
              ≡ (m + 0) + (n * p) + (q ^ m * q ^ n) + 1
_ = λ m n p q → begin
    suc (m + (p * n) + (q ^ (m + n))) ≡⟨ +-comm 1 _ ⟩
    m + (p * n) + (q ^ (m + n)) + 1   ≡⟨ congₙ 3 (λ m n p → m + n + p + 1)
                                                 (+-comm 0 m)
                                                 (*-comm p n)
                                                 (^-distribˡ-+-* q m n)
                                       ⟩
    m + 0 + n * p + (q ^ m) * (q ^ n) + 1 ∎ where open ≡-Reasoning

-- Partial application of the functional argument is fine: the number of arguments
-- `congₙ` is going to take is determined by its first argument (a natural number)
-- and not by the type of the function it works on.

_ : ∀ m → (m +_) ≡ ((m + 0) +_)
_ = λ m → congₙ 1 _+_ (+-comm 0 m)

-- We don't have to work on the function's first argument either: we can just as
-- easily use `congₙ` to act on the second one by `flip`ping it. See `holeₙ` for
-- a generalisation of this idea allowing to target *any* of the function's
-- arguments and not just the first or second one.

_ : ∀ m → (_+ m) ≡ (_+ (m + 0))
_ = λ m → congₙ 1 (flip _+_) (+-comm 0 m)

------------------------------------------------------------------------
-- substₙ : (P : A₁ → ⋯ → Aₙ → Set p) →
--          a₁ ≡ b₁ → ⋯ aₙ ≡ bₙ → P a₁ ⋯ aₙ → P b₁ ⋯ bₙ

-- We can play the same type of game with subst

open import Agda.Builtin.Nat using (mod-helper)

-- Because we know from the definition `mod-helper` that this equation holds:
-- mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
-- we should be able to prove the slightly modified statement by transforming
-- all the `x + 1` into `suc x`. We can do so using `substₙ`.

_ : ∀ k m n j → mod-helper k m (n + 1) (j + 1) ≡ mod-helper (k + 1) m n j
_ = λ k m n j →
    let P sk sn sj = mod-helper k m sn sj ≡ mod-helper sk m n j
    in substₙ P (+-comm 1 k) (+-comm 1 n) (+-comm 1 j) refl

-----------------------------------------------------------------------
-- Generic programs working on n-ary products & functions
-----------------------------------------------------------------------

-----------------------------------------------------------------------
-- curryₙ   : ∀ n → (A₁ × ⋯ × Aₙ → B) → A₁ → ⋯ → Aₙ → B
-- uncurryₙ : ∀ n → (A₁ → ⋯ → Aₙ → B) → A₁ × ⋯ × Aₙ → B

-- The first thing we may want to do generically is convert between
-- curried function types and uncurried ones. We can do this by using:

-- They both work the same way so we will focus on curryₙ only here.
-- If we pass to `curryₙ` the arity of its argument then we obtain a
-- fully curried function.

curry₁ : (A × B × C × D → E) → A → B → C → D → E
curry₁ = curryₙ 4

-- Note that here we are not flattening arbitrary nestings: products have
-- to be right nested. Which means that if you have a deeply-nested product
-- then it won't be affected by the procedure.

curry₁' : (A × (B × C) × D → E) → A → (B × C) → D → E
curry₁' = curryₙ 3

-- When we are currying a function, we have no obligation to pass its exact
-- arity as the parameter: we can decide to only curry part of it like so:
-- Indeed (A₁ × ⋯ × Aₙ → B) can also be seen as (A₁ × ⋯ × (Aₖ × ⋯ × Aₙ) → B)

curry₂ : (A × B × C × D → E) → A → B → (C × D) → E
curry₂ = curryₙ 3

-----------------------------------------------------------------------
-- projₙ : ∀ n (k : Fin n) → (A₁ × ⋯ × Aₙ) → Aₖ₊₁

-- Another useful class of functions to manipulate n-ary product is a
-- generic projection function. Note the (k + 1) in the return index:
-- Fin counts from 0 up.

-- It behaves as one expects (Data.Fin's #_ comes in handy to write down
-- Fin literals):

proj₃ : (A × B × C × D × E) → C
proj₃ = projₙ 5 (# 2)

-- Of course we can once more project the "tail" of the n-ary product by
-- passing `projₙ` a natural number which is smaller than the size of the
-- n-ary product, seeing (A₁ × ⋯ × Aₙ) as (A₁ × ⋯ × (Aₖ × ⋯ × Aₙ)).

proj₃' : (A × B × C × D × E) → C × D × E
proj₃' = projₙ 3 (# 2)

-----------------------------------------------------------------------
-- insertₙ : ∀ n (k : Fin (suc n)) →
--           B → (A₁ × ⋯ Aₙ) → (A₁ × ⋯ × Aₖ × B × Aₖ₊₁ × ⋯ Aₙ)

insert₁ : C → (A × B × D × E) → (A × B × C × D × E)
insert₁ = insertₙ 4 (# 2)

insert₁' : C → (A × B × D × E) → (A × B × C × D × E)
insert₁' = insertₙ 3 (# 2)

-- Note that `insertₙ` takes a `Fin (suc n)`. Indeed in an n-ary product
-- there are (suc n) positions at which one may insert a value. We may
-- insert at the front or the back of the product:

insert-front : A → (B × C × D × E) → (A × B × C × D × E)
insert-front = insertₙ 4 (# 0)

insert-back : E → (A × B × C × D) → (A × B × C × D × E)
insert-back = insertₙ 4 (# 4)

-----------------------------------------------------------------------
-- removeₙ : ∀ n (k : Fin n) → (A₁ × ⋯ Aₙ) → (A₁ × ⋯ × Aₖ × Aₖ₊₂ × ⋯ Aₙ)

-- Dual to `insertₙ`, we may remove a value.

remove₁ : (A × B × C × D × E) → (A × B × D × E)
remove₁ = removeₙ 5 (# 2)

-- Inserting at `k` and then removing at `inject₁ k` should yield the identity

remove-insert : C → (A × B × D × E) → (A × B × D × E)
remove-insert c = removeₙ 5 (inject₁ k) ∘′ insertₙ 4 k c
    where k = # 2

-----------------------------------------------------------------------
-- updateₙ : ∀ n (k : Fin n) (f : (a : Aₖ₊₁) → B a) →
--           (p : A₁ × ⋯ Aₙ) → (A₁ × ⋯ × Aₖ × B (projₙ n k p) × Aₖ₊₂ × ⋯ Aₙ)

-- We can not only project out, insert or remove values: we can update them
-- in place. The type (and value) of the replacement at position k may depend
-- upon the current value at position k.

update₁ : (p : A × B × ℕ × C × D) → (A × B × Fin _ × C × D)
update₁ = updateₙ 5 (# 2) fromℕ

-- We can explicitly use the primed version of `updateₙ` to make it known to
-- Agda that the update function is non dependent. This type of information
-- is useful for inference: the tighter the constraints, the easier it is to
-- find a solution (if possible).

update₂ : (p : A × B × ℕ × C × D) → (A × B × List D × C × D)
update₂ = λ p → updateₙ′ 5 (# 2) (λ n → replicate n (projₙ 5 (# 4) p)) p

-----------------------------------------------------------------------
-- _%=_⊢_ : ∀ n → (C → D) → (A₁ → ⋯ Aₙ → D → B) → A₁ → ⋯ → Aₙ → C → B

-- Traditional composition (also known as the index update operator `_⊢_`
-- in `Relation.Unary`) focuses solely on the first argument of an n-ary
-- function. `_%=_⊢_` on the other hand allows us to touch any one of the
-- arguments.

-- In the following example we have a function `f : A → B` and `replicate`
-- of type `ℕ → B → List B`. We want ̀f` to act on the second argument of
-- replicate. Which we can do like so.

compose₁ : (A → B) → ℕ → A → List B
compose₁ f = 1 %= f ⊢ replicate

-- Here we spell out the equivalent explicit variable-manipulation and
-- prove the two functions equal.

compose₁' : (A → B) → ℕ → A → List B
compose₁' f n a = replicate n (f a)

compose₁-eq : compose₁ {a} {A} {b} {B} ≡ compose₁'
compose₁-eq = refl

-----------------------------------------------------------------------
-- _∷=_⊢_ : ∀ n → A → (A₁ → ⋯ Aₙ → A → B) → A₁ → ⋯ → Aₙ → B

-- Partial application usually focuses on the first argument of a function.
-- We can now partially apply a function in any of its arguments using
-- `_∷=_⊢_`. Reusing our example involving replicate: we can specialise it
-- to only output finite lists of `0`:

apply₁ : ℕ → List ℕ
apply₁ = 1 ∷= 0 ⊢ replicate

apply₁-eq : apply₁ 3 ≡ 0 ∷ 0 ∷ 0 ∷ []
apply₁-eq = refl

------------------------------------------------------------------------
-- holeₙ : ∀ n → (A → (A₁ → ⋯ Aₙ → B)) → A₁ → ⋯ → Aₙ → (A → B)

-- As we have seen earlier, `cong` acts on a function's first variable.
-- If we want to access the second one, we can use `flip`. But what about
-- the fourth one? We typically use an explicit λ-abstraction shuffling
-- variables. Not anymore.

-- Reusing mod-helper just because it takes a lot of arguments:

hole₁ : ∀ k m n j → mod-helper k (m + 1) n j ≡ mod-helper k (suc m) n j
hole₁ = λ k m n j → cong (holeₙ 2 (mod-helper k) n j) (+-comm m 1)

-----------------------------------------------------------------------
-- mapₙ : ∀ n → (B → C) → (A₁ → ⋯ Aₙ → B) → (A₁ → ⋯ → Aₙ → C)

-- (R →_) gives us the reader monad (and, a fortiori, functor). That is to
-- say that given a function (A → B) and an (R → A) we can get an (R → B)
-- This generalises to n-ary functions.

-- Reusing our `composeₙ` example: instead of applying `f` to the replicated
-- element, we can map it on the resulting list. Giving us:

map₁ : (A → B) → ℕ → A → List B
map₁ f = mapₙ 2 (map f) replicate

------------------------------------------------------------------------
-- constₙ : ∀ n → B → A₁ → ⋯ → Aₙ → B

-- `const` is basically `pure` for the reader monad discussed above. Just
-- like we can generalise the functorial action corresponding to the reader
-- functor to n-ary functions, we can do the same for `pure`.

const₁ : A → B → C → D → E → A
const₁ = constₙ 4

-- Together with `holeₙ`, this means we can make a constant function out
-- of any of the arguments. The fourth for instance:

const₂ : A → B → C → D → E → D
const₂ = holeₙ 3 (constₙ 4)

------------------------------------------------------------------------
-- Generalised quantifiers
------------------------------------------------------------------------

-- As we have seen multiple times already, one of the advantages of working
-- with non-dependent products is that they can be easily inferred. This is
-- a prime opportunity to define generic quantifiers.

-- And because n-ary relations are Set-terminated, there is no ambiguity
-- where to split between arguments & codomain. As a consequence Agda can
-- infer even `n`, the number of arguments. We can use notations which are
-- just like the ones defined in `Relation.Unary`.

------------------------------------------------------------------------
-- ∃⟨_⟩ : (A₁ → ⋯ → Aₙ → Set r) → Set _
-- ∃⟨ P ⟩ = ∃ λ a₁ → ⋯ → ∃ λ aₙ → P a₁ ⋯ aₙ

-- Returning to our favourite function taking a lot of arguments: we can
-- find a set of input for which it evaluates to 666

exist₁ : ∃⟨ (λ k m n j → mod-helper k m n j ≡ 666) ⟩
exist₁ = 19 , 793 , 3059 , 10 , refl

------------------------------------------------------------------------
-- ∀[_] : (A₁ → ⋯ → Aₙ → Set r) → Set _
-- ∀[_] P = ∀ {a₁} → ⋯ → ∀ {aₙ} → P a₁ ⋯ aₙ

all₁ : ∀[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
all₁ {a₁} {a₂} = a₁ ≟ a₂

------------------------------------------------------------------------
-- Π : (A₁ → ⋯ → Aₙ → Set r) → Set _
-- Π P = ∀ a₁ → ⋯ → ∀ aₙ → P a₁ ⋯ aₙ

all₂ : Π[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
all₂ = _≟_

------------------------------------------------------------------------
-- _⇒_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)
-- P ⇒ Q = λ a₁ → ⋯ → λ aₙ → P a₁ ⋯ aₙ → Q a₁ ⋯ aₙ

antisym : ∀[ _≤_ ⇒ _≥_ ⇒ _≡_ ]
antisym = ≤-antisym

------------------------------------------------------------------------
-- _∪_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)
-- P ∪ Q = λ a₁ → ⋯ → λ aₙ → P a₁ ⋯ aₙ ⊎ Q a₁ ⋯ aₙ

≤->-connex : Π[ _≤_ ∪ _>_ ]
≤->-connex m n with <-cmp m n
... | tri< a ¬b ¬c = inj₁ (<⇒≤ a)
... | tri≈ ¬a b ¬c = inj₁ (≤-reflexive b)
... | tri> ¬a ¬b c = inj₂ c

------------------------------------------------------------------------
-- _∩_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)
-- P ∩ Q = λ a₁ → ⋯ → λ aₙ → P a₁ ⋯ aₙ × Q a₁ ⋯ aₙ

<-inversion : ∀[ _<_ ⇒ _≤_ ∩ _≢_ ]
<-inversion m<n = <⇒≤ m<n , <⇒≢ m<n

------------------------------------------------------------------------
-- ∁ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set _)
-- ∁ P = λ a₁ → ⋯ → λ aₙ → ¬ (P a₁ ⋯ aₙ)

m<n⇒m≱n : ∀[ _>_ ⇒ ∁ _≤_ ]
m<n⇒m≱n m>n m≤n = <⇒≱ m>n m≤n


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)

-- A "canonical" presentation of cartesian closed categories.
--
-- This presentation is equivalent to the one in
-- Categories.Category.CartesianClosed but it is easier to work with
-- in some circumstances.
--
-- Here, exponentials are not defined in terms of arbitrary products,
-- but in terms of a family of "canonical" products.  Since products
-- are defined only up to isomorphism the choice of product does not
-- matter for the property of being cartesian closed, but working with
-- a fixed choice of representatives simplifies the constructions of
-- some instances of CCCs (e.g. Cats).

module Categories.Category.CartesianClosed.Canonical {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level using (levelOfTerm)
open import Function using (flip)

open import Categories.Category.Cartesian 𝒞 using (Cartesian)
import Categories.Category.CartesianClosed 𝒞 as 𝒞-CC
open import Categories.Object.Exponential 𝒞 using (Exponential)
open import Categories.Object.Product 𝒞
open import Categories.Object.Terminal 𝒞 using (Terminal)
open import Categories.Morphism.Reasoning 𝒞

private
  module 𝒞 = Category 𝒞
  open Category 𝒞
  open HomReasoning

  variable
    A B C : Obj
    f g h f₁ f₂ g₁ g₂ : A ⇒ B

-- A (canonical) cartesian closed category is a category with all
-- (canonical) products and exponentials
--
-- This presentation is equivalent to the one in
-- Categories.Category.CartesianClosed.CartesianClosed.
record CartesianClosed : Set (levelOfTerm 𝒞) where
  infixr 7 _×_
  infixr 9 _^_
  infix 10 ⟨_,_⟩

  field

    -- Canonical products

    ⊤    : Obj
    _×_  : Obj → Obj → Obj

    !     : A ⇒ ⊤
    π₁    : A × B ⇒ A
    π₂    : A × B ⇒ B
    ⟨_,_⟩ : C ⇒ A → C ⇒ B → C ⇒ A × B

    !-unique : (f : A ⇒ ⊤) → ! ≈ f

    π₁-comp  : π₁ ∘ ⟨ f , g ⟩ ≈ f
    π₂-comp  : π₂ ∘ ⟨ f , g ⟩ ≈ g

    ⟨,⟩-unique : π₁ ∘ h ≈ f → π₂ ∘ h ≈ g → ⟨ f , g ⟩ ≈ h

  -- The above defines canonical finite products, making 𝒞 cartesian.

  ⊤-terminal : Terminal
  ⊤-terminal = record { !-unique = !-unique }

  ×-product : ∀ {A B} → Product A B
  ×-product {A} {B} =
    record { project₁ = π₁-comp; project₂ = π₂-comp; unique = ⟨,⟩-unique }

  isCartesian : Cartesian
  isCartesian = record
    { terminal = ⊤-terminal
    ; products = record { product = ×-product }
    }

  module cartesian = Cartesian isCartesian
  open cartesian public
    hiding (_×_; π₁; π₂; ⟨_,_⟩)
    renaming (⟨⟩-cong₂ to ⟨,⟩-resp-≈)

  field

    -- Canonical exponentials (w.r.t. the canonical products)

    _^_   : Obj → Obj → Obj
    eval  : B ^ A × A ⇒ B
    curry : C × A ⇒ B → C ⇒ B ^ A

    eval-comp  : eval ∘ (curry f ⁂ id) ≈ f

    curry-resp-≈ : f ≈ g → curry f ≈ curry g
    curry-unique : eval ∘ (f ⁂ id) ≈ g → f ≈ curry g

  -- The above defines canonical exponentials, making 𝒞 cartesian closed.
  --
  -- NOTE: below we use "⊗" to indicate "non-canonical" products.

  ^-exponential : ∀ {A B} → Exponential A B
  ^-exponential {A} {B} = record
    { B^A      = B ^ A
    ; product  = ×-product
    ; eval     = eval
    ; λg       = λ C⊗A f → curry (f ∘ repack ×-product C⊗A)
    ; β        = λ {C} C⊗A {g} →
      begin
        eval ∘ [ C⊗A ⇒ ×-product ] curry (g ∘ repack ×-product C⊗A) ×id
      ≈˘⟨ pullʳ [ ×-product ⇒ ×-product ]×∘⟨⟩ ⟩
        (eval ∘ (curry (g ∘ repack ×-product C⊗A) ⁂ id)) ∘ repack C⊗A ×-product
      ≈⟨ eval-comp ⟩∘⟨refl ⟩
        (g ∘ repack ×-product C⊗A) ∘ repack C⊗A ×-product
      ≈⟨ cancelʳ (repack∘repack≈id ×-product C⊗A) ⟩
        g
      ∎
    ; λ-unique = λ {C} C⊗A {g} {f} hyp →
      curry-unique (begin
        eval ∘ (f ⁂ id)
      ≈˘⟨ pullʳ [ C⊗A ⇒ ×-product ]×∘⟨⟩ ⟩
        (eval ∘ [ C⊗A ⇒ ×-product ] f ×id) ∘ repack ×-product C⊗A
      ≈⟨ hyp ⟩∘⟨refl ⟩
        g ∘ repack ×-product C⊗A
      ∎)
    }

module Equivalence where
  open 𝒞-CC using () renaming (CartesianClosed to CartesianClosed′)

  -- The two presentations of CCCs are equivalent

  fromCanonical : CartesianClosed → CartesianClosed′
  fromCanonical cc = record
    { cartesian = CartesianClosed.isCartesian cc
    ; exp       = CartesianClosed.^-exponential cc
    }

  toCanonical : CartesianClosed′ → CartesianClosed
  toCanonical cc = record
    { ⊤     = ⊤
    ; _×_   = _×_
    ; !     = !
    ; π₁    = π₁
    ; π₂    = π₂
    ; ⟨_,_⟩ = ⟨_,_⟩
    ; !-unique   = !-unique
    ; π₁-comp    = project₁
    ; π₂-comp    = project₂
    ; ⟨,⟩-unique = unique
    ; _^_   = _^_
    ; eval  = eval′
    ; curry = λg
    ; eval-comp    = β′
    ; curry-resp-≈ = λ-cong
    ; curry-unique = λ-unique′
    }
    where open CartesianClosed′ cc

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level

data ⊥ : Type₀ where

⊥* : Type ℓ
⊥* = Lift ⊥

rec : {A : Type ℓ} → ⊥ → A
rec ()

elim : {A : ⊥ → Type ℓ} → (x : ⊥) → A x
elim ()

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- A memoising backend for RecursiveDescent.Hybrid
------------------------------------------------------------------------

-- Following Frost/Szydlowski and Frost/Hafiz/Callaghan (but without
-- the left recursion fix). An improvement has been made: The user
-- does not have to insert memoisation annotations manually. Instead
-- all grammar nonterminals are memoised. This is perhaps a bit less
-- flexible, but less error-prone, since there is no need to guarantee
-- that all "keys" (arguments to the memoise combinator) are unique
-- (assuming that the nonterminal equality is strong enough).

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality1
open import RecursiveDescent.Index
open import Data.Product

module RecursiveDescent.Hybrid.Memoised

  -- In order to be able to store results in a memo table (and avoid
  -- having to lift the table code to Set1) the result types have to
  -- come from the following universe:

  {Result : Set} (⟦_⟧ : Result -> Set)

  -- Nonterminals also have to be small enough:

  {NT : Index -> Result -> Set} {LargeNT : ParserType}
  (resultType : forall {i r} -> LargeNT i r -> Result)
  (resultTypeCorrect : forall {i r}
                       (x : LargeNT i r) -> ⟦ resultType x ⟧ ≡₁ r)
  (notTooLarge : forall {i r}
                 (x : LargeNT i r) -> NT i (resultType x))

  -- Furthermore nonterminals need to be ordered, so that they can be
  -- used as memo table keys:

  {_≈_ _<_ : Rel (∃₂ NT)}
  (ntOrdered : IsStrictTotalOrder _≈_ _<_)

  -- And the underlying equality needs to be strong enough:

  (indicesEqual : _≈_ =[ (\irx -> (proj₁ irx , proj₁ (proj₂ irx))) ]⇒
                  _≡_ {Index × Result})

  -- Token type:

  {Tok : Set}

  where

open import Data.Bool renaming (true to ⊤; false to ⊥)
import Data.Nat as Nat
open Nat using (ℕ; zero; suc; pred; z≤n; s≤s)
import Data.Nat.Properties as NatProp
open import Data.Function hiding (_∘′_)
import Data.Product.Record as PR
open PR using () renaming (_,_ to _◇_)
import Data.Vec  as Vec;  open Vec  using (Vec;  []; _∷_)
import Data.List as List; open List using (List; []; _∷_)
open import Data.Sum
open import Data.Maybe
open import Relation.Binary.OrderMorphism
open _⇒-Poset_
import Relation.Binary.On as On
import Relation.Binary.Props.StrictTotalOrder as STOProps
open STOProps NatProp.strictTotalOrder

import RecursiveDescent.Hybrid.Memoised.Monad as Monad
open import RecursiveDescent.Hybrid.Type renaming (return to ret)
open import Utilities

------------------------------------------------------------------------
-- Some monotone functions

MonoFun : Set
MonoFun = poset ⇒-Poset poset

suc-mono : _≤_ =[ suc ]⇒ _≤_
suc-mono (inj₁ i<j)    = inj₁ (s≤s i<j)
suc-mono (inj₂ ≡-refl) = inj₂ ≡-refl

pred-mono : _≤_ =[ pred ]⇒ _≤_
pred-mono (inj₁ (s≤s (z≤n {zero})))  = inj₂ ≡-refl
pred-mono (inj₁ (s≤s (z≤n {suc j}))) = inj₁ (s≤s z≤n)
pred-mono (inj₁ (s≤s (s≤s i<j)))     = inj₁ (s≤s i<j)
pred-mono (inj₂ ≡-refl)              = inj₂ ≡-refl

sucM : MonoFun
sucM = record
  { fun      = suc
  ; monotone = suc-mono
  }

predM : MonoFun
predM = record
  { fun      = pred
  ; monotone = pred-mono
  }

maybePredM : Empty -> MonoFun
maybePredM e = if e then idM else predM

lemma : forall e pos -> fun (maybePredM e) pos ≤ pos
lemma ⊤ pos       = refl
lemma ⊥ zero      = refl
lemma ⊥ (suc pos) = inj₁ (Poset.refl Nat.poset)

------------------------------------------------------------------------
-- Parser monad

data Key : MonoFun -> Result -> Set where
  key : forall {e c r} (nt : NT (e ◇ c) r) ->
        Key (maybePredM e) r

shuffle : ∃₂ Key -> ∃₂ NT
shuffle (._ , _ , key x) = (, , x)

_≈K_ : Rel (∃₂ Key)
_≈K_ = _≈_ on₁ shuffle

_<K_ : Rel (∃₂ Key)
_<K_ = _<_ on₁ shuffle

ordered : IsStrictTotalOrder _≈K_ _<K_
ordered = On.isStrictTotalOrder shuffle ntOrdered

funsEqual : _≈K_ =[ proj₁ ]⇒ _≡_
funsEqual {(._ , _ , key _)} {(._ , _ , key _)} eq =
  ≡-cong (maybePredM ∘ PR.proj₁ ∘ proj₁) (indicesEqual eq)

resultsEqual : _≈K_ =[ (\rfk -> proj₁ (proj₂ rfk)) ]⇒ _≡_
resultsEqual {(._ , _ , key _)} {(._ , _ , key _)} eq =
  ≡-cong proj₂ (indicesEqual eq)

open Monad
       (StrictTotalOrder.isStrictTotalOrder NatProp.strictTotalOrder)
       (Vec Tok)
       ⟦_⟧
       ordered
       (\{k₁} {k₂} -> funsEqual    {k₁} {k₂})
       (\{k₁} {k₂} -> resultsEqual {k₁} {k₂})
open PM

cast : forall {bnd f A₁ A₂} -> A₁ ≡₁ A₂ -> P bnd f A₁ -> P bnd f A₂
cast ≡₁-refl p = p

------------------------------------------------------------------------
-- Run function for the parsers

-- Some helper functions.

private

  -- Extracts the first element from the input, if any.

  eat : forall {bnd}
        (inp : Input≤ bnd) -> Maybe Tok × Input≤ (pred (position inp))
  eat {bnd} xs = helper (bounded xs) (string xs)
    where
    helper : forall {pos} ->
             pos ≤ bnd -> Vec Tok pos -> Maybe Tok × Input≤ (pred pos)
    helper _  []       = (nothing , [] isBounded∶ refl)
    helper le (c ∷ cs) = (just c  , cs isBounded∶ refl)

  -- Fails if it encounters nothing.

  fromJust : forall {bnd} -> Maybe Tok -> P bnd idM Tok
  fromJust nothing  = ∅
  fromJust (just c) = return c

-- For every successful parse the run function returns the remaining
-- string. (Since there can be several successful parses a list of
-- strings is returned.)

-- This function is structurally recursive with respect to the
-- following lexicographic measure:
--
-- 1) The upper bound of the length of the input string.
-- 2) The parser's proper left corner tree.

private

 module Dummy (g : Grammar Tok LargeNT) where

  mutual
    parse : forall n {e c r} ->
            Parser Tok LargeNT (e ◇ c) r ->
            P n (if e then idM else predM) r
    parse n       (! x)           = memoParse n x
    parse n       symbol          = fromJust =<< gmodify predM eat
    parse n       (ret x)         = return x
    parse n       fail            = ∅
    parse n       (p₁ ?>>= p₂)    = parse  n      p₁ >>= parse  n ∘′ p₂
    parse zero    (p₁ !>>= p₂)    = ∅
    parse (suc n) (p₁ !>>= p₂)    = parse (suc n) p₁ >>= parse↑ n ∘′ p₂
    parse n       (alt ⊤ _ p₁ p₂) = parse  n      p₁ ∣   parse↑ n    p₂
    parse n       (alt ⊥ ⊤ p₁ p₂) = parse↑ n      p₁ ∣   parse  n    p₂
    parse n       (alt ⊥ ⊥ p₁ p₂) = parse  n      p₁ ∣   parse  n    p₂

    parse↑ : forall n {e c r} ->
             Parser Tok LargeNT (e ◇ c) r -> P n idM r
    parse↑ n {e} p = adjustBound (lemma e) (parse n p)

    memoParse : forall n {r e c} -> LargeNT (e ◇ c) r ->
                P n (if e then idM else predM) r
    memoParse n x = cast₁ (memoise k (cast₂ (parse n (g x))))
      where
      k     = key (notTooLarge x)
      cast₁ = cast (resultTypeCorrect x)
      cast₂ = cast (≡₁-sym (resultTypeCorrect x))

-- Exported run function.

parse : forall {i r} ->
        Parser Tok LargeNT i r -> Grammar Tok LargeNT ->
        List Tok -> List (r × List Tok)
parse p g toks =
  List.map (map-× id (\xs -> Vec.toList (string xs))) $
  run (Vec.fromList toks) (Dummy.parse g _ p)

-- A variant which only returns parses which leave no remaining input.

parse-complete : forall {i r} ->
                 Parser Tok LargeNT i r -> Grammar Tok LargeNT ->
                 List Tok -> List r
parse-complete p g s =
  List.map proj₁ (List.filter (List.null ∘ proj₂) (parse p g s))

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Data.Rational where

import Data.Bool as Bool
import Data.Nat as Nat
import Data.Integer as Int

open Int renaming
            ( _*_  to _*'_
            ; _+_  to _+'_
            ; -_   to -'_
            ; _-_  to _-'_
            ; !_!  to !_!'
            ; _==_ to _=='_
            ; _≤_  to _≤'_
            ; _≥_  to _≥'_
            ; _>_  to _>'_
            ; _<_  to _<'_
            )
open Nat using (Nat; zero; suc)
open Bool

infix  40 _==_ _<_ _>_ _≤_ _≥_
infixl 60 _+_ _-_
infixl 70 _%'_ _%_ _/_ _*_
infixr 80 _^_
infix  90 -_

data Rational : Set where
  _%'_  : Int -> Int -> Rational

numerator : Rational -> Int
numerator (n %' d) = n

denominator : Rational -> Int
denominator (n %' d) = d

_%_ : Int -> Int -> Rational
neg n       % neg m = pos (suc n) % pos (suc m)
pos 0       % neg m = pos 0 %' pos 1
pos (suc n) % neg m = neg n % pos (suc m)
x           % y     = div x z %' div y z
  where
    z = gcd x y

fromInt : Int -> Rational
fromInt x = x %' pos 1

fromNat : Nat -> Rational
fromNat x = fromInt (pos x)

_+_ : Rational -> Rational -> Rational
(a %' b) + (c %' d) = (a *' d +' c *' b) % (b *' d)

-_ : Rational -> Rational
- (a %' b) = -' a %' b

_-_ : Rational -> Rational -> Rational
a - b = a + (- b)

_/_ : Rational -> Rational -> Rational
(a %' b) / (c %' d) = (a *' d) % (b *' c)

_*_ : Rational -> Rational -> Rational
(a %' b) * (c %' d) = (a *' c) % (b *' d)

recip : Rational -> Rational
recip (a %' b) = b %' a

_^_ : Rational -> Int -> Rational
q ^ neg n       = recip q ^ pos (suc n)
q ^ pos zero    = fromNat 1
q ^ pos (suc n) = q * q ^ pos n

!_! : Rational -> Rational
! a %' b ! = pos ! a !' %' pos ! b !'

round : Rational -> Int
round (a %' b) = div (a +' div b (pos 2)) b

_==_ : Rational -> Rational -> Bool
(a %' b) == (c %' d) = a *' d ==' b *' c

_<_ : Rational -> Rational -> Bool
(a %' b) < (c %' d) = a *' d <' b *' c

_>_ : Rational -> Rational -> Bool
(a %' b) > (c %' d) = a *' d >' b *' c

_≤_ : Rational -> Rational -> Bool
(a %' b) ≤ (c %' d) = a *' d ≤' b *' c

_≥_ : Rational -> Rational -> Bool
(a %' b) ≥ (c %' d) = a *' d ≥' b *' c

max : Rational -> Rational -> Rational
max a b = if a < b then b else a

min : Rational -> Rational -> Rational
min a b = if a < b then a else b

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Empty | E

type
  𝟘 : 0-ary

term
  abort : 𝟘  ->  α

theory
  (𝟘η) e : 𝟘  c : α |> abort(e) = c
-}

module Empty.Signature where

open import SOAS.Context

-- Type declaration
data ET : Set where
  𝟘 : ET

open import SOAS.Syntax.Signature ET public
open import SOAS.Syntax.Build ET public

-- Operator symbols
data Eₒ : Set where
  abortₒ : {α : ET} → Eₒ

-- Term signature
E:Sig : Signature Eₒ
E:Sig = sig λ
  { (abortₒ {α}) → (⊢₀ 𝟘) ⟼₁ α
  }

open Signature E:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Issue1245 where

postulate
  A B : Set
  [_] : A -> B

module M (_ : B) where

module N (a : A) = M [ a ]


text:
-- This file is the source Agda file
-- Edit this file not Type.hs
-- The warning below will be written to Type.hs

module PlutusCore.Generators.NEAT.Type where

-- warning to be written to Haskell file:
{-# FOREIGN AGDA2HS
{-
!!! THIS FILE IS GENERATED FROM Type.agda
!!! DO NOT EDIT THIS FILE. EDIT Type.agda
!!! AND THEN RUN agda2hs ON IT.
-}
#-}

{-# FOREIGN AGDA2HS
{-# OPTIONS_GHC -fno-warn-orphans      #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE StandaloneDeriving        #-}

import           Control.Enumerable
import           Control.Monad.Except
import           PlutusCore
import           PlutusCore.Generators.NEAT.Common

#-}

open import Relation.Binary.PropositionalEquality
open import Haskell.Prelude hiding (m)
open import PlutusCore.Generators.NEAT.Common

{-# FOREIGN AGDA2HS
newtype Neutral a = Neutral
  { unNeutral :: a
  }
#-}
-- * Enumeration

-- ** Enumerating types

data TypeBuiltinG : Set where
  TyByteStringG  : TypeBuiltinG
  TyIntegerG     : TypeBuiltinG
  TyBoolG        : TypeBuiltinG
  TyUnitG        : TypeBuiltinG
  TyStringG      : TypeBuiltinG
  TyListG        : TypeBuiltinG
  TyDataG        : TypeBuiltinG

{-# COMPILE AGDA2HS TypeBuiltinG deriving (Show, Eq, Ord) #-}

{-# FOREIGN AGDA2HS
deriveEnumerable ''TypeBuiltinG
#-}

-- NOTE: Unusually, the application case is annotated with a kind.
--       The reason is eagerness and efficiency. If we have the kind
--       information at the application site, we can check the two
--       subterms in parallel, while evaluating as little as possible.

variable
  n m o : Set

postulate Kind : Set → Set

data TypeG (n : Set) : Set where
  TyVarG : n → TypeG n
  TyFunG : TypeG n → TypeG n → TypeG n
  TyIFixG : TypeG n  → Kind ⊤ → TypeG n → TypeG n
  TyForallG : Kind ⊤ → TypeG (S n) → TypeG n
  TyBuiltinG : TypeBuiltinG → TypeG n
  TyLamG : TypeG (S n) → TypeG n
  TyAppG : TypeG n → TypeG n → Kind ⊤ → TypeG n

{-# COMPILE AGDA2HS TypeG deriving (Eq, Ord, Show) #-}

{-# FOREIGN AGDA2HS
deriving instance Ord (Kind ())

deriveEnumerable ''Kind

deriveEnumerable ''TypeG

type ClosedTypeG = TypeG Z

instance Functor TypeG where
  fmap = ren
#-}

ext : (m → n) → S m → S n
ext _ FZ     = FZ
ext f (FS x) = FS (f x)

{-# COMPILE AGDA2HS ext #-}

ren : (m → n) → TypeG m → TypeG n
ren f (TyVarG x) = TyVarG (f x)
ren f (TyFunG ty1 ty2) = TyFunG (ren f ty1) (ren f ty2)
ren f (TyIFixG ty1 k ty2) = TyIFixG (ren f ty1) k (ren f ty2)
ren f (TyForallG k ty) = TyForallG k (ren (ext f) ty)
ren _ (TyBuiltinG b) = TyBuiltinG b
ren f (TyLamG ty) = TyLamG (ren (ext f) ty)
ren f (TyAppG ty1 ty2 k) = TyAppG (ren f ty1) (ren f ty2) k

{-# COMPILE AGDA2HS ren #-}

ext-cong : {ρ ρ' : m → n} → (∀ x → ρ x ≡ ρ' x) → ∀ x → ext ρ x ≡ ext ρ' x
ext-cong p FZ     = refl
ext-cong p (FS x) = cong FS (p x)

ren-cong : {ρ ρ' : m → n} → (∀ x → ρ x ≡ ρ' x) → ∀ t → ren ρ t ≡ ren ρ' t
ren-cong p (TyVarG x)          = cong TyVarG (p x)
ren-cong p (TyFunG ty1 ty2)    = cong₂ TyFunG (ren-cong p ty1) (ren-cong p ty2)
ren-cong p (TyIFixG ty1 k ty2) =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (ren-cong p ty1) (ren-cong p ty2)
ren-cong p (TyForallG k ty)    = cong (TyForallG k) (ren-cong (ext-cong p) ty)
ren-cong p (TyBuiltinG b)      = refl
ren-cong p (TyLamG ty)         = cong TyLamG (ren-cong (ext-cong p) ty)
ren-cong p (TyAppG ty1 ty2 k)  =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (ren-cong p ty1) (ren-cong p ty2)

-- ext (map for S) satisfies the functor laws

ext-id : (x : S m) → ext id x ≡ x
ext-id FZ     = refl
ext-id (FS x) = refl

ext-comp : (x : S m)(ρ : m → n)(ρ' : n → o) → ext (ρ' ∘ ρ) x ≡ ext ρ' (ext ρ x)
ext-comp FZ     ρ ρ' = refl
ext-comp (FS x) ρ ρ' = refl

-- ren (map for TypeG) satisfies the functor laws

ren-id : (ty : TypeG m) → ren id ty ≡ ty
ren-id (TyVarG _)          = refl
ren-id (TyFunG ty1 ty2)    = cong₂ TyFunG (ren-id ty1) (ren-id ty2)
ren-id (TyIFixG ty1 k ty2) =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (ren-id ty1) (ren-id ty2)
ren-id (TyForallG k ty)    =
  cong (TyForallG k) (trans (ren-cong ext-id ty) (ren-id ty))
ren-id (TyBuiltinG _)      = refl
ren-id (TyLamG ty)         =
  cong TyLamG (trans (ren-cong ext-id ty) (ren-id ty))
ren-id (TyAppG ty1 ty2 k)  =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (ren-id ty1) (ren-id ty2)

ren-comp : (ty : TypeG m)(ρ : m → n)(ρ' : n → o)
         → ren (ρ' ∘ ρ) ty ≡ ren ρ' (ren ρ ty)
ren-comp (TyVarG x)          ρ ρ' = refl
ren-comp (TyFunG ty1 ty2)    ρ ρ' =
  cong₂ TyFunG (ren-comp ty1 ρ ρ') (ren-comp ty2 ρ ρ')
ren-comp (TyIFixG ty1 k ty2) ρ ρ' =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (ren-comp ty1 ρ ρ') (ren-comp ty2 ρ ρ')
ren-comp (TyForallG k ty)    ρ ρ' = cong
  (TyForallG k)
  (trans (ren-cong (λ x → ext-comp x ρ ρ') ty)
         (ren-comp ty (ext ρ) (ext ρ')))
ren-comp (TyBuiltinG b)      ρ ρ' = refl
ren-comp (TyLamG ty)         ρ ρ' = cong
  TyLamG
  (trans (ren-cong (λ x → ext-comp x ρ ρ') ty)
         (ren-comp ty (ext ρ) (ext ρ')))
ren-comp (TyAppG ty1 ty2 k)  ρ ρ' =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (ren-comp ty1 ρ ρ') (ren-comp ty2 ρ ρ')

-- ** Type reduction

-- |Extend type substitutions.
exts : (n → TypeG m) -> S n → TypeG (S m)
exts _ FZ     = TyVarG FZ
exts s (FS i) = ren FS (s i) -- FS <$> s i

{-# COMPILE AGDA2HS exts #-}

-- |Simultaneous substitution of type variables.
sub : (n -> TypeG m) -> TypeG n -> TypeG m
sub s (TyVarG i)             = s i
sub s (TyFunG ty1 ty2)       =
  TyFunG (sub s ty1) (sub s ty2)
sub s (TyIFixG ty1 k ty2)    =
  TyIFixG (sub s ty1) k (sub s ty2)
sub s (TyForallG k ty)       = TyForallG k (sub (exts s) ty)
sub _ (TyBuiltinG tyBuiltin) = TyBuiltinG tyBuiltin
sub s (TyLamG ty)            = TyLamG (sub (exts s) ty)
sub s (TyAppG ty1 ty2 k)     =
  TyAppG (sub s ty1) (sub s ty2) k

{-# COMPILE AGDA2HS sub #-}

{-# FOREIGN AGDA2HS
instance Monad TypeG where
  a >>= f = sub f a
--  return = pure

instance Applicative TypeG where
  (<*>) = ap
  pure = TyVarG
#-}

-- sub ((=<<) for TypeG) satisfies the monad laws

exts-cong : {σ σ' : m → TypeG n} → (∀ x → σ x ≡ σ' x)
          → ∀ x → exts σ x ≡ exts σ' x
exts-cong p FZ     = refl
exts-cong p (FS x) = cong (ren FS) (p x)

sub-cong : {σ σ' : m → TypeG n} → (∀ x → σ x ≡ σ' x)
         → ∀ ty → sub σ ty ≡ sub σ' ty
sub-cong p (TyVarG x)          = p x
sub-cong p (TyFunG ty1 ty2)    = cong₂ TyFunG (sub-cong p ty1) (sub-cong p ty2)
sub-cong p (TyIFixG ty1 k ty2) =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (sub-cong p ty1) (sub-cong p ty2)
sub-cong p (TyForallG k ty)    = cong (TyForallG k) (sub-cong (exts-cong p) ty)
sub-cong p (TyBuiltinG b)      = refl
sub-cong p (TyLamG ty)         = cong TyLamG (sub-cong (exts-cong p) ty)
sub-cong p (TyAppG ty1 ty2 k)  =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (sub-cong p ty1) (sub-cong p ty2)

exts-id : (x : S m) → exts TyVarG x ≡ TyVarG x
exts-id FZ     = refl
exts-id (FS x) = refl

sub-id : (t : TypeG m) → sub TyVarG t ≡ t
sub-id (TyVarG x)          = refl
sub-id (TyFunG ty1 ty2)    = cong₂ TyFunG (sub-id ty1) (sub-id ty2)
sub-id (TyIFixG ty1 k ty2) =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (sub-id ty1) (sub-id ty2)
sub-id (TyForallG k ty)    = cong
  (TyForallG k)
  (trans (sub-cong exts-id ty) (sub-id ty))
sub-id (TyBuiltinG b)      = refl
sub-id (TyLamG ty)         = cong
  TyLamG
  (trans (sub-cong exts-id ty) (sub-id ty))
sub-id (TyAppG ty1 ty2 k)  = cong₂
  (λ ty1 ty2 → TyAppG ty1 ty2 k)
  (sub-id ty1)
  (sub-id ty2)

exts-ext : (x : S m)(ρ : m → n)(σ : n → TypeG o)
         → exts (σ ∘ ρ) x ≡ exts σ (ext ρ x)
exts-ext FZ     σ ρ = refl
exts-ext (FS x) σ ρ = refl

sub-ren : (t : TypeG m)(ρ : m → n)(σ : n → TypeG o)
         → sub (σ ∘ ρ) t ≡ sub σ (ren ρ t)
sub-ren (TyVarG x)          ρ σ = refl
sub-ren (TyFunG ty1 ty2)    ρ σ =
  cong₂ TyFunG (sub-ren ty1 ρ σ) (sub-ren ty2 ρ σ)
sub-ren (TyIFixG ty1 k ty2) ρ σ =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (sub-ren ty1 ρ σ) (sub-ren ty2 ρ σ)

sub-ren (TyForallG k ty)    ρ σ = cong
  (TyForallG k)
  (trans (sub-cong (λ x → exts-ext x ρ σ) ty)
         (sub-ren ty (ext ρ) (exts σ)))
sub-ren (TyBuiltinG b)      ρ σ = refl
sub-ren (TyLamG ty)         ρ σ = cong
  TyLamG
  (trans (sub-cong (λ x → exts-ext x ρ σ) ty)
         (sub-ren ty (ext ρ) (exts σ)))
sub-ren (TyAppG ty1 ty2 k)  ρ σ =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (sub-ren ty1 ρ σ) (sub-ren ty2 ρ σ)

ext-exts : (x : S m)(σ : m → TypeG n)(ρ : n → o)
         → exts (ren ρ ∘ σ) x ≡ ren (ext ρ) (exts σ x)
ext-exts FZ     σ ρ = refl
ext-exts (FS x) σ ρ = trans
  (sym (ren-comp (σ x) ρ FS))
  (ren-comp (σ x) FS (ext ρ))

ren-sub : (t : TypeG m)(σ : m → TypeG n)(ρ : n → o)
         → sub (ren ρ ∘ σ) t ≡ ren ρ (sub σ t)
ren-sub (TyVarG x)          σ ρ = refl
ren-sub (TyFunG ty1 ty2)    σ ρ =
  cong₂ TyFunG (ren-sub ty1 σ ρ) (ren-sub ty2 σ ρ)
ren-sub (TyIFixG ty1 k ty2) σ ρ =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (ren-sub ty1 σ ρ) (ren-sub ty2 σ ρ)
ren-sub (TyForallG k ty)    σ ρ = cong
  (TyForallG k)
  (trans (sub-cong (λ x → ext-exts x σ ρ) ty)
         (ren-sub ty (exts σ) (ext ρ)))
ren-sub (TyBuiltinG b)      σ ρ = refl
ren-sub (TyLamG ty)         σ ρ = cong
  TyLamG
  (trans (sub-cong (λ x → ext-exts x σ ρ) ty)
         (ren-sub ty (exts σ) (ext ρ)))
ren-sub (TyAppG ty1 ty2 k)  σ ρ =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (ren-sub ty1 σ ρ) (ren-sub ty2 σ ρ)

exts-comp : (x : S m)(σ : m → TypeG n)(σ' : n → TypeG o)
         → exts (sub σ' ∘ σ) x ≡ sub (exts σ') (exts σ x)
exts-comp FZ     σ σ' = refl
exts-comp (FS x) σ σ' = trans
  (sym (ren-sub (σ x) σ' FS))
  (sub-ren (σ x) FS (exts σ'))

sub-comp : (ty : TypeG m)(σ : m → TypeG n)(σ' : n → TypeG o)
         → sub (sub σ' ∘ σ) ty ≡ sub σ' (sub σ ty)
sub-comp (TyVarG x)          σ σ' = refl
sub-comp (TyFunG ty1 ty2)    σ σ' =
  cong₂ TyFunG (sub-comp ty1 σ σ') (sub-comp ty2 σ σ')
sub-comp (TyIFixG ty1 k ty2) σ σ' =
  cong₂ (λ ty1 ty2 → TyIFixG ty1 k ty2) (sub-comp ty1 σ σ') (sub-comp ty2 σ σ')
sub-comp (TyForallG k ty)    σ σ' = cong
  (TyForallG k)
  (trans (sub-cong (λ x → exts-comp x σ σ') ty)
         (sub-comp ty (exts σ) (exts σ')))
sub-comp (TyBuiltinG b)      σ σ' = refl
sub-comp (TyLamG ty)         σ σ' = cong
  TyLamG
  (trans (sub-cong (λ x → exts-comp x σ σ') ty)
         (sub-comp ty (exts σ) (exts σ')))
sub-comp (TyAppG ty1 ty2 k)  σ σ' =
  cong₂ (λ ty1 ty2 → TyAppG ty1 ty2 k) (sub-comp ty1 σ σ') (sub-comp ty2 σ σ')

max_stars_repo_name: kk-anlm/plutus

max_issues_repo_name: kk-anlm/plutus

max_forks_repo_name: kk-anlm/plutus


text:
module Fail.MultiArgumentPatternLambda where

open import Agda.Builtin.Bool

tooManyPats : Bool → Bool → Bool
tooManyPats = λ where false false → false
                      true  true  → false
                      _     _     → true
{-# COMPILE AGDA2HS tooManyPats #-}


text:
-- Andreas, 2018-03-23: issue #3007, reported by Fabian

-- An broken identifier followed by a comment and then the end of the file
-- caused an internal error during error reporting.
--
-- Should fail without internal error.

postulate _-- This is the end of the file!


text:
module Relator.Equals.Proofs where

open import Relator.Equals
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid renaming (_≡_ to _≡ₛ_)

instance
  [≡]-reflexivity : ∀{ℓ}{A : Type{ℓ}} → Reflexivity(_≡_ {P = A})
  Reflexivity.proof([≡]-reflexivity) = constant-path

instance
  [≡]-symmetry : ∀{ℓ}{A : Type{ℓ}} → Symmetry(_≡_ {P = A})
  Symmetry.proof([≡]-symmetry) = reversed-path

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 New.NewNew where

open import New.Changes
open import New.LangChanges
open import New.Lang
open import New.Derive
open import Data.Empty

[_]τ_from_to_ : ∀ (τ : Type) → (dv : Chτ τ) → (v1 v2 : ⟦ τ ⟧Type) → Set

-- This can't be a datatype, since it wouldn't be strictly positive as it
-- appears on the left of an arrow in the function case, which then can be
-- contained in nested "fromto-validity" proofs.
sumfromto : ∀ (σ τ : Type) → (dv : SumChange2 {A = ⟦ σ ⟧Type} {B = ⟦ τ ⟧Type}) → (v1 v2 : ⟦ sum σ τ ⟧Type) → Set
sumfromto σ τ (ch₁ da) (inj₁ a1) (inj₁ a2) = [ σ ]τ da from a1 to a2
-- These fallback equations unfortunately don't hold definitionally, they're
-- split on multiple cases, so the pattern match is a mess.
--
-- To "case split" on validity, I typically copy-paste the pattern match from
-- fromto→⊕ and change the function name :-(.
sumfromto σ τ (ch₁ da) _ _ = ⊥
sumfromto σ τ (ch₂ db) (inj₂ b1) (inj₂ b2) = [ τ ]τ db from b1 to b2
sumfromto σ τ (ch₂ db) _ _ = ⊥
sumfromto σ τ (rp (inj₂ b2)) (inj₁ a1) (inj₂ b2') = b2 ≡ b2'
sumfromto σ τ (rp (inj₁ a2)) (inj₂ b1) (inj₁ a2') = a2 ≡ a2'
sumfromto σ τ (rp s) _ _ = ⊥

[ σ ⇒ τ ]τ df from f1 to f2 =
  ∀ (da : Chτ σ) (a1 a2 : ⟦ σ ⟧Type) →
  [ σ ]τ da from a1 to a2 → [ τ ]τ df a1 da from f1 a1 to f2 a2
[ int ]τ dv from v1 to v2 = v2 ≡ v1 + dv
[ pair σ τ ]τ (da , db) from (a1 , b1) to (a2 , b2) = [ σ ]τ da from a1 to a2 × [ τ ]τ db from b1 to b2
[ sum σ τ ]τ dv from v1 to v2 = sumfromto σ τ (convert dv) v1 v2

data [_]Γ_from_to_ : ∀ Γ → ChΓ Γ → (ρ1 ρ2 : ⟦ Γ ⟧Context) → Set where
  v∅ : [ ∅ ]Γ ∅ from ∅ to ∅
  _v•_ : ∀ {τ Γ dv v1 v2 dρ ρ1 ρ2} →
    (dvv : [ τ ]τ dv from v1 to v2) →
    (dρρ : [ Γ ]Γ dρ from ρ1 to ρ2) →
    [ τ • Γ ]Γ (dv • v1 • dρ) from (v1 • ρ1) to (v2 • ρ2)

⟦Γ≼ΔΓ⟧ : ∀ {Γ ρ1 ρ2 dρ} → (dρρ : [ Γ ]Γ dρ from ρ1 to ρ2) →
  ρ1 ≡ ⟦ Γ≼ΔΓ ⟧≼ dρ
⟦Γ≼ΔΓ⟧ v∅ = refl
⟦Γ≼ΔΓ⟧ (dvv v• dρρ) = cong₂ _•_ refl (⟦Γ≼ΔΓ⟧ dρρ)

fit-sound : ∀ {Γ τ} → (t : Term Γ τ) →
  ∀ {dρ ρ1 ρ2} → [ Γ ]Γ dρ from ρ1 to ρ2 →
  ⟦ t ⟧Term ρ1 ≡ ⟦ fit t ⟧Term dρ
fit-sound t dρρ = trans
  (cong ⟦ t ⟧Term (⟦Γ≼ΔΓ⟧ dρρ))
  (sym (weaken-sound t _))

-- Now relate this validity with ⊕. To know that nil and so on are valid, also
-- relate it to the other definition.

fromto→⊕ : ∀ {τ} dv v1 v2 →
  [ τ ]τ dv from v1 to v2 →
  v1 ⊕ dv ≡ v2

⊝-fromto : ∀ {τ} (v1 v2 : ⟦ τ ⟧Type) → [ τ ]τ v2 ⊝ v1 from v1 to v2
⊝-fromto {σ ⇒ τ} f1 f2 da a1 a2 daa rewrite sym (fromto→⊕ da a1 a2 daa) = ⊝-fromto (f1 a1) (f2 (a1 ⊕ da))
⊝-fromto {int} v1 v2 = sym (update-diff v2 v1)
⊝-fromto {pair σ τ} (a1 , b1) (a2 , b2) = ⊝-fromto a1 a2 , ⊝-fromto b1 b2
⊝-fromto {sum σ τ} (inj₁ a1) (inj₁ a2) = ⊝-fromto a1 a2
⊝-fromto {sum σ τ} (inj₁ a1) (inj₂ b2) = refl
⊝-fromto {sum σ τ} (inj₂ b1) (inj₁ a2) = refl
⊝-fromto {sum σ τ} (inj₂ b1) (inj₂ b2) = ⊝-fromto b1 b2

nil-fromto : ∀ {τ} (v : ⟦ τ ⟧Type) → [ τ ]τ nil v from v to v
nil-fromto v = ⊝-fromto v v

fromto→⊕ {σ ⇒ τ} df f1 f2 dff =
  ext (λ v → fromto→⊕ {τ} (df v (nil v)) (f1 v) (f2 v) (dff (nil v) v v (nil-fromto v)))
fromto→⊕ {int} dn n1 n2 refl = refl
fromto→⊕ {pair σ τ} (da , db) (a1 , b1) (a2 , b2) (daa , dbb) =
  cong₂ _,_ (fromto→⊕ _ _ _ daa) (fromto→⊕ _ _ _ dbb)
fromto→⊕ {sum σ τ} (inj₁ (inj₁ da)) (inj₁ a1) (inj₁ a2) daa rewrite fromto→⊕ da a1 a2 daa = refl
fromto→⊕ {sum σ τ} (inj₁ (inj₁ da)) (inj₁ _) (inj₂ _) ()
fromto→⊕ {sum σ τ} (inj₁ (inj₁ da)) (inj₂ _) (inj₁ _) ()
fromto→⊕ {sum σ τ} (inj₁ (inj₁ da)) (inj₂ _) (inj₂ _) ()
fromto→⊕ {sum σ τ} (inj₁ (inj₂ db)) (inj₂ b1) (inj₂ b2) dbb rewrite fromto→⊕ db b1 b2 dbb = refl
fromto→⊕ {sum σ τ} (inj₁ (inj₂ db)) (inj₁ _) (inj₁ _) ()
fromto→⊕ {sum σ τ} (inj₁ (inj₂ db)) (inj₁ _) (inj₂ _) ()
fromto→⊕ {sum σ τ} (inj₁ (inj₂ db)) (inj₂ _) (inj₁ _) ()
fromto→⊕ {sum σ τ} (inj₂ (inj₁ a2)) (inj₂ b1) (inj₁ .a2) refl = refl
fromto→⊕ {sum σ τ} (inj₂ (inj₁ a2)) (inj₁ _) (inj₁ _) ()
fromto→⊕ {sum σ τ} (inj₂ (inj₁ a2)) (inj₁ _) (inj₂ _) ()
fromto→⊕ {sum σ τ} (inj₂ (inj₁ a2)) (inj₂ _) (inj₂ _) ()
fromto→⊕ {sum σ τ} (inj₂ (inj₂ b2)) (inj₁ a1) (inj₂ .b2) refl = refl
fromto→⊕ {sum σ τ} (inj₂ (inj₂ b2)) (inj₁ _) (inj₁ _) ()
fromto→⊕ {sum σ τ} (inj₂ (inj₂ b2)) (inj₂ _) (inj₁ _) ()
fromto→⊕ {sum σ τ} (inj₂ (inj₂ b2)) (inj₂ _) (inj₂ _) ()

fromtoDeriveConst : ∀ {τ} c →
  [ τ ]τ ⟦ deriveConst c ⟧Term ∅ from ⟦ c ⟧Const to ⟦ c ⟧Const
fromtoDeriveConst (lit n) = sym (right-id-int n)
fromtoDeriveConst plus da a1 a2 daa db b1 b2 dbb rewrite daa | dbb = mn·pq=mp·nq {a1} {da} {b1} {db}
fromtoDeriveConst minus da a1 a2 daa db b1 b2 dbb rewrite daa | dbb | sym (-m·-n=-mn {b1} {db}) = mn·pq=mp·nq {a1} {da} { - b1} { - db}
fromtoDeriveConst cons da a1 a2 daa db b1 b2 dbb = daa , dbb
fromtoDeriveConst fst (da , db) (a1 , b1) (a2 , b2) (daa , dbb) = daa
fromtoDeriveConst snd (da , db) (a1 , b1) (a2 , b2) (daa , dbb) = dbb
fromtoDeriveConst linj da a1 a2 daa = daa
fromtoDeriveConst rinj db b1 b2 dbb = dbb
fromtoDeriveConst match (inj₁ (inj₁ da)) (inj₁ a1) (inj₁ a2) daa df f1 f2 dff dg g1 g2 dgg = dff da a1 a2 daa
fromtoDeriveConst match (inj₁ (inj₁ da)) (inj₁ _) (inj₂ _) ()
fromtoDeriveConst match (inj₁ (inj₁ da)) (inj₂ _) (inj₁ _) ()
fromtoDeriveConst match (inj₁ (inj₁ da)) (inj₂ _) (inj₂ _) ()
fromtoDeriveConst match (inj₁ (inj₂ db)) (inj₂ b1) (inj₂ b2) dbb df f1 f2 dff dg g1 g2 dgg = dgg db b1 b2 dbb
fromtoDeriveConst match (inj₁ (inj₂ db)) (inj₁ _) (inj₁ _) ()
fromtoDeriveConst match (inj₁ (inj₂ db)) (inj₁ _) (inj₂ _) ()
fromtoDeriveConst match (inj₁ (inj₂ db)) (inj₂ _) (inj₁ _) ()
fromtoDeriveConst match (inj₂ (inj₁ a2)) (inj₂ b1) (inj₁ .a2) refl df f1 f2 dff dg g1 g2 dgg rewrite changeMatchSem-lem2 f1 df g1 dg b1 a2 | sym (fromto→⊕ df _ _ dff) | sym (fromto→⊕ dg _ _ dgg) = ⊝-fromto (g1 b1) ((f1 ⊕ df) a2)
fromtoDeriveConst match (inj₂ (inj₁ a2)) (inj₁ _) (inj₁ _) ()
fromtoDeriveConst match (inj₂ (inj₁ a2)) (inj₁ _) (inj₂ _) ()
fromtoDeriveConst match (inj₂ (inj₁ a2)) (inj₂ _) (inj₂ _) ()
fromtoDeriveConst match (inj₂ (inj₂ b2)) (inj₁ a1) (inj₂ .b2) refl df f1 f2 dff dg g1 g2 dgg rewrite changeMatchSem-lem1 f1 df g1 dg a1 b2 | sym (fromto→⊕ df _ _ dff) | sym (fromto→⊕ dg _ _ dgg) = ⊝-fromto (f1 a1) ((g1 ⊕ dg) b2)
fromtoDeriveConst match (inj₂ (inj₂ b2)) (inj₁ _) (inj₁ _) ()
fromtoDeriveConst match (inj₂ (inj₂ b2)) (inj₂ _) (inj₁ _) ()
fromtoDeriveConst match (inj₂ (inj₂ b2)) (inj₂ _) (inj₂ _) ()

fromtoDeriveVar : ∀ {Γ τ} → (x : Var Γ τ) →
  ∀ {dρ ρ1 ρ2}  → [ Γ ]Γ dρ from ρ1 to ρ2 →
    [ τ ]τ (⟦ x ⟧ΔVar ρ1 dρ) from (⟦ x ⟧Var ρ1) to (⟦ x ⟧Var ρ2)
fromtoDeriveVar this (dvv v• dρρ) = dvv
fromtoDeriveVar (that x) (dvv v• dρρ) = fromtoDeriveVar x dρρ

fromtoDerive : ∀ {Γ} τ → (t : Term Γ τ) →
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
    [ τ ]τ (⟦ t ⟧ΔTerm ρ1 dρ) from (⟦ t ⟧Term ρ1) to (⟦ t ⟧Term ρ2)
fromtoDerive τ (const c) {dρ} {ρ1} dρρ rewrite ⟦ c ⟧ΔConst-rewrite ρ1 dρ = fromtoDeriveConst c
fromtoDerive τ (var x) dρρ = fromtoDeriveVar x dρρ
fromtoDerive τ (app {σ} s t) dρρ rewrite sym (fit-sound t dρρ) =
  let fromToF = fromtoDerive (σ ⇒ τ) s dρρ
  in let fromToB = fromtoDerive σ t dρρ in fromToF _ _ _ fromToB
fromtoDerive (σ ⇒ τ) (abs t) dρρ = λ dv v1 v2 dvv →
  fromtoDerive τ t (dvv v• dρρ)

open import Postulate.Extensionality

open ≡-Reasoning

-- If df is valid, prove (f1 ⊕ df) (a ⊕ da) ≡ f1 a ⊕ df a da.

-- This statement uses a ⊕ da instead of a2, which is not the style of this formalization but fits better with the other one.
-- Instead, WellDefinedFunChangeFromTo (without prime) fits this formalization.
WellDefinedFunChangeFromTo′ : ∀ {σ τ} (f1 : ⟦ σ ⇒ τ ⟧Type) → (df : Chτ (σ ⇒ τ)) → Set
WellDefinedFunChangeFromTo′ f1 df = ∀ da a → [ _ ]τ da from a to (a ⊕ da) → WellDefinedFunChangePoint f1 df a da

fromto→WellDefined′ : ∀ {σ τ f1 f2 df} → [ σ ⇒ τ ]τ df from f1 to f2 →
  WellDefinedFunChangeFromTo′ f1 df
fromto→WellDefined′ {f1 = f1} {f2} {df} dff da a daa =
  begin
    (f1 ⊕ df) (a ⊕ da)
  ≡⟨ cong (λ □ → □ (a ⊕ da)) (fromto→⊕ df f1 f2 dff)⟩
    f2 (a ⊕ da)
  ≡⟨ sym (fromto→⊕ _ _ _ (dff da _ _ daa)) ⟩
    f1 a ⊕ df a da
  ∎

WellDefinedFunChangeFromTo : ∀ {σ τ} (f1 : ⟦ σ ⇒ τ ⟧Type) → (df : Chτ (σ ⇒ τ)) → Set
WellDefinedFunChangeFromTo f1 df = ∀ da a1 a2 → [ _ ]τ da from a1 to a2 → WellDefinedFunChangePoint f1 df a1 da

fromto→WellDefined : ∀ {σ τ f1 f2 df} → [ σ ⇒ τ ]τ df from f1 to f2 →
  WellDefinedFunChangeFromTo f1 df
fromto→WellDefined {f1 = f1} {f2} {df} dff da a1 a2 daa =
  fromto→WellDefined′ dff da a1 daa′
  where
    daa′ : [ _ ]τ da from a1 to (a1 ⊕ da)
    daa′ rewrite fromto→⊕ da _ _ daa = daa

-- Recursive isomorphism between the two validities.
--
-- Among other things, valid→fromto proves that a validity-preserving function,
-- with validity defined via (f1 ⊕ df) (a ⊕ da) ≡ f1 a ⊕ df a da, is also valid
-- in the "fromto" sense.
--
-- We can't hope for a better statement, since we need the equation to be
-- satisfied also by returned or argument functions.

fromto→valid : ∀ {τ} →
  ∀ dv v1 v2 → [ τ ]τ dv from v1 to v2 →
  valid v1 dv
valid→fromto : ∀ {τ} v (dv : Chτ τ) → valid v dv → [ τ ]τ dv from v to (v ⊕ dv)

fromto→valid {int} = λ dv v1 v2 x → tt
fromto→valid {pair σ τ} (da , db) (a1 , b1) (a2 , b2) (daa , dbb) = (fromto→valid da _ _ daa) , (fromto→valid db _ _ dbb)
fromto→valid {σ ⇒ τ} df f1 f2 dff = λ a da ada →
  fromto→valid (df a da) (f1 a) (f2 (a ⊕ da)) (dff da a (a ⊕ da) (valid→fromto a da ada)) ,
  fromto→WellDefined′ dff da a (valid→fromto a da ada)
fromto→valid {sum σ τ} (inj₁ (inj₁ da)) (inj₁ a1) (inj₁ a2) daa = sv₁ a1 da (fromto→valid da a1 a2 daa)
fromto→valid {sum σ τ} (inj₁ (inj₁ da)) (inj₁ _) (inj₂ _) ()
fromto→valid {sum σ τ} (inj₁ (inj₁ da)) (inj₂ _) (inj₁ _) ()
fromto→valid {sum σ τ} (inj₁ (inj₁ da)) (inj₂ _) (inj₂ _) ()
fromto→valid {sum σ τ} (inj₁ (inj₂ db)) (inj₂ b1) (inj₂ b2) dbb = sv₂ b1 db (fromto→valid db b1 b2 dbb)
fromto→valid {sum σ τ} (inj₁ (inj₂ db)) (inj₁ _) (inj₁ _) ()
fromto→valid {sum σ τ} (inj₁ (inj₂ db)) (inj₁ _) (inj₂ _) ()
fromto→valid {sum σ τ} (inj₁ (inj₂ db)) (inj₂ _) (inj₁ _) ()
fromto→valid {sum σ τ} (inj₂ (inj₁ a2)) (inj₂ b1) (inj₁ .a2) refl = svrp₂ b1 a2
fromto→valid {sum σ τ} (inj₂ (inj₁ a2)) (inj₁ _) (inj₁ _) ()
fromto→valid {sum σ τ} (inj₂ (inj₁ a2)) (inj₁ _) (inj₂ _) ()
fromto→valid {sum σ τ} (inj₂ (inj₁ a2)) (inj₂ _) (inj₂ _) ()
fromto→valid {sum σ τ} (inj₂ (inj₂ b2)) (inj₁ a1) (inj₂ .b2) refl = svrp₁ a1 b2
fromto→valid {sum σ τ} (inj₂ (inj₂ b2)) (inj₁ _) (inj₁ _) ()
fromto→valid {sum σ τ} (inj₂ (inj₂ b2)) (inj₂ _) (inj₁ _) ()
fromto→valid {sum σ τ} (inj₂ (inj₂ b2)) (inj₂ _) (inj₂ _) ()

valid→fromto {int} v dv tt = refl
valid→fromto {pair σ τ} (a , b) (da , db) (ada , bdb) = valid→fromto a da ada , valid→fromto b db bdb
valid→fromto {σ ⇒ τ} f df fdf da a1 a2 daa = body
  where
    fa1da-valid :
      valid (f a1) (df a1 da) ×
      WellDefinedFunChangePoint f df a1 da
    fa1da-valid = fdf a1 da (fromto→valid da _ _ daa)
    body : [ τ ]τ df a1 da from f a1 to (f ⊕ df) a2
    body rewrite sym (fromto→⊕ da _ _ daa) | proj₂ fa1da-valid = valid→fromto (f a1) (df a1 da) (proj₁ fa1da-valid)
valid→fromto {sum σ τ} .(inj₁ a) .(inj₁ (inj₁ da)) (sv₁ a da ada) = valid→fromto a da ada
valid→fromto {sum σ τ} .(inj₂ b) .(inj₁ (inj₂ db)) (sv₂ b db bdb) = valid→fromto b db bdb
valid→fromto {sum σ τ} .(inj₁ a1) .(inj₂ (inj₂ b2)) (svrp₁ a1 b2) = refl
valid→fromto {sum σ τ} .(inj₂ b1) .(inj₂ (inj₁ a2)) (svrp₂ b1 a2) = refl

correctDeriveOplus : ∀ {Γ} τ → (t : Term Γ τ) →
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ t ⟧Term ρ1) ⊕ (⟦ t ⟧ΔTerm ρ1 dρ) ≡ (⟦ t ⟧Term ρ2)
correctDeriveOplus τ t dρρ = fromto→⊕ _ _ _ (fromtoDerive τ t dρρ)

-- Getting to the original equation 1 from PLDI'14.

open import New.LangOps

correctDeriveOplusτ : ∀ {Γ} τ → (t : Term Γ τ)
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ app₂ (oplusτo τ) (fit t) (derive t) ⟧Term dρ) ≡ (⟦ t ⟧Term ρ2)
correctDeriveOplusτ τ t {dρ = dρ} {ρ1 = ρ1} dρρ
  rewrite oplusτ-equiv _ dρ _ (⟦ fit t ⟧Term dρ) (⟦ derive t ⟧Term dρ)
  | sym (fit-sound t dρρ)
  = correctDeriveOplus τ t dρρ

deriveGivesDerivative : ∀ {Γ} σ τ → (f : Term Γ (σ ⇒ τ)) (a : Term Γ σ)→
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ app f a ⟧Term ρ1) ⊕ (⟦ app f a ⟧ΔTerm ρ1 dρ) ≡ (⟦ app f a ⟧Term ρ2)
deriveGivesDerivative σ τ f a dρρ = correctDeriveOplus τ (app f a) dρρ

deriveGivesDerivative₂ : ∀ {Γ} σ τ → (f : Term Γ (σ ⇒ τ)) (a : Term Γ σ) →
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ app₂ (oplusτo τ) (fit (app f a)) (app₂ (derive f) (fit a) (derive a)) ⟧Term dρ) ≡ (⟦ app f a ⟧Term ρ2)
deriveGivesDerivative₂ σ τ f a dρρ = correctDeriveOplusτ τ (app f a) dρρ

-- Proof of the original equation 1 from PLDI'14.
eq1 : ∀ {Γ} σ τ →
  {nilρ : ChΓ Γ} {ρ : ⟦ Γ ⟧Context} → [ Γ ]Γ nilρ from ρ to ρ →
  ∀ (f : Term Γ (σ ⇒ τ)) (a : Term Γ σ) (da : Term (ΔΓ Γ) (Δt σ)) →
  (daa : [ σ ]τ (⟦ da ⟧Term nilρ) from (⟦ a ⟧Term ρ) to (⟦ a ⟧Term ρ ⊕ ⟦ da ⟧Term nilρ)) →
    ⟦ app₂ (oplusτo τ) (fit (app f a)) (app₂ (derive f) (fit a) da) ⟧Term nilρ ≡ ⟦ app (fit f) (app₂ (oplusτo σ) (fit a) da) ⟧Term nilρ
eq1 σ τ {nilρ} {ρ} dρρ f a da daa
  rewrite
    oplusτ-equiv _ nilρ _ (⟦ fit (app f a) ⟧Term nilρ) (⟦ (app₂ (derive f) (fit a) da) ⟧Term nilρ)
  | sym (fit-sound f dρρ)
  | oplusτ-equiv _ nilρ _ (⟦ fit a ⟧Term nilρ) (⟦ da ⟧Term nilρ)
  | sym (fit-sound a dρρ)
  = fromto→⊕ (⟦ f ⟧ΔTerm ρ nilρ (⟦ a ⟧Term ρ) (⟦ da ⟧Term nilρ)) _ _
    (fromtoDerive _ f dρρ (⟦ da ⟧Term nilρ) (⟦ a ⟧Term ρ)
      (⟦ a ⟧Term ρ ⊕ ⟦ da ⟧Term nilρ) daa)

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:
module Data.ListSized.Functions where

import      Lvl
open import Data.ListSized
open import Functional
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Function
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A A₁ A₂ B B₁ B₂ Result : Type{ℓ}
private variable a b n n₁ n₂ : ℕ

-- List concatenation
_++_ : List(T)(a) → List(T)(b) → List(T)(a + b)
_++_ x y = elim _ (\{a} → const(List _ (a + _))) y (const ∘ (_⊰_)) x
infixl 1000 _++_

-- The first element of the list
head : List(T)(𝐒(n)) → T
head (x ⊰ _) = x

-- The list without its first element
tail : List(T)(𝐒(n)) → List(T)(n)
tail (_ ⊰ l) = l

tail₀ : List(T)(n) → List(T)(𝐏(n))
tail₀ ∅       = ∅
tail₀ (_ ⊰ l) = l

-- The nth element in the list
index : 𝕟(n) → List(T)(n) → T
index 𝟎      (x ⊰ _) = x
index (𝐒(n)) (_ ⊰ l) = index n l

-- The sublist with the first n elements in the list
first : (k : 𝕟₌(n)) → List(T)(n) → List(T)(𝕟-to-ℕ k)
first 𝟎      _       = ∅
first (𝐒(n)) (x ⊰ l) = x ⊰ (first n l)

-- skip : ∀{n} → (k : 𝕟₌(n)) → List(T)(n) → List(T)(n − k)
-- last : ∀{n} → (k : 𝕟₌(n)) → List(T)(n) → List(T)(𝕟-to-ℕ k)

-- Length of the list (number of elements in the list)
length : List(T)(n) → ℕ
length {n = n} _ = n

-- The list with an element repeated n times
repeat : T → (n : ℕ) → List(T)(n)
repeat _ 𝟎      = ∅
repeat x (𝐒(n)) = x ⊰ (repeat x n)

-- A list constructed from a function
fromFn : (𝕟(n) → T) → List(T)(n)
fromFn {n = 𝟎}    _ = ∅
fromFn {n = 𝐒(n)} f = f(𝟎) ⊰ fromFn {n = n} (f ∘ 𝐒)

-- The list with a list concatenated (repeated) n times
_++^_ : List(T)(n) → (k : ℕ) → List(T)(n ⋅ k)
_++^_ _ 𝟎      = ∅
_++^_ l (𝐒(k)) = l ++ (l ++^ k)

-- Applies a function to each element in the list
map : (A → B) → List(A)(n) → List(B)(n)
map f = elim _ (\{n} _ → List(_)(n)) ∅ (const ∘ (_⊰_) ∘ f)

-- Applies a binary operator to each element in the list starting with the initial element.
-- Example:
--   foldₗ(▫)(init)[]          = init
--   foldₗ(▫)(init)[a]         = init▫a
--   foldₗ(▫)(init)[a,b]       = (init▫a)▫b
--   foldₗ(▫)(init)[a,b,c,d,e] = ((((init▫a)▫b)▫c)▫d)▫e
foldₗ : (Result → T → Result) → Result → List(T)(n) → Result
foldₗ _    result ∅ = result
foldₗ(_▫_) result (elem ⊰ l) = foldₗ(_▫_) (result ▫ elem) l

-- Applies a binary operator to each element in the list starting with the initial element.
-- Example:
--   foldᵣ(▫)(init)[]          = init
--   foldᵣ(▫)(init)[a]         = a▫init
--   foldᵣ(▫)(init)[a,b]       = a▫(b▫init)
--   foldᵣ(▫)(init)[a,b,c,d,e] = a▫(b▫(c▫(d▫(e▫init))))
foldᵣ : (T → Result → Result) → Result → List(T)(n) → Result
foldᵣ(_▫_) init = elim _ _ init (const ∘ (_▫_))

-- Example:
--   reduceₗ(▫)[a]         = a
--   reduceₗ(▫)[a,b]       = a▫b
--   reduceₗ(▫)[a,b,c]     = (a▫b)▫c
--   reduceₗ(▫)[a,b,c,d,e] = (((a▫b)▫c)▫d)▫e
reduceₗ : (T → T → T) → List(T)(𝐒(n)) → T
reduceₗ(_▫_) (elem ⊰ l) = foldₗ(_▫_) elem l

-- Example:
--   reduceᵣ(▫)[a]         = a
--   reduceᵣ(▫)[a,b]       = a▫b
--   reduceᵣ(▫)[a,b,c]     = a▫(b▫c)
--   reduceᵣ(▫)[a,b,c,d,e] = a▫(b▫(c▫(d▫e)))
reduceᵣ : (T → T → T) → List(T)(𝐒(n)) → T
reduceᵣ(_▫_) (elem ⊰ l) = foldᵣ(_▫_) elem l

map₂ : (A₁ → A₂ → B) → (List(A₁)(n₁) → List(B)(n₁)) → (List(A₂)(n₂) → List(B)(n₂)) → (List(A₁)(n₁) → List(A₂)(n₂) → List(B)(max n₁ n₂))
map₂ f g₁ g₂ ∅          ∅          = ∅
map₂ f g₁ g₂ ∅          l₂@(_ ⊰ _) = g₂ l₂
map₂ f g₁ g₂ l₁@(_ ⊰ _) ∅          = g₁ l₁
map₂ f g₁ g₂ (x₁ ⊰ l₁)  (x₂ ⊰ l₂)  = f x₁ x₂ ⊰ map₂ f (tail ∘ g₁ ∘ (x₁ ⊰_)) ((tail ∘ g₂ ∘ (x₂ ⊰_))) l₁ l₂

map₂₌ : (A₁ → A₂ → B) → (List(A₁)(n) → List(A₂)(n) → List(B)(n))
map₂₌ f ∅          ∅          = ∅
map₂₌ f (x₁ ⊰ l₁)  (x₂ ⊰ l₂)  = f x₁ x₂ ⊰ map₂₌ f l₁ l₂

-- Accumulates the results of every step in `_^_` into a list.
-- Example:
--   accumulateIterate₀ 0 f(x) = []
--   accumulateIterate₀ 1 f(x) = [x]
--   accumulateIterate₀ 2 f(x) = [x , f(x)]
--   accumulateIterate₀ 3 f(x) = [x , f(x) , f(f(x))]
--   accumulateIterate₀ 4 f(x) = [x , f(x) , f(f(x)) , f(f(f(x)))]
accumulateIterate₀ : (n : ℕ) → (T → T) → (T → List(T)(n))
accumulateIterate₀ 𝟎      f(x) = ∅
accumulateIterate₀ (𝐒(n)) f(x) = x ⊰ accumulateIterate₀ n f (f(x))

-- Accumulates the results of every step in `_^_` into a list.
-- Example:
--   accumulateIterate 0 f(x) = [x]
--   accumulateIterate 1 f(x) = [x , f(x)]
--   accumulateIterate 2 f(x) = [x , f(x) , f(f(x))]
--   accumulateIterate 3 f(x) = [x , f(x) , f(f(x)) , f(f(f(x)))]
--   accumulateIterate 4 f(x) = [x , f(x) , f(f(x)) , f(f(f(x))) , f(f(f(f(x))))]
accumulateIterate : (n : ℕ) → (T → T) → (T → List(T)(𝐒(n)))
accumulateIterate n = accumulateIterate₀(𝐒(n))