text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Surjection
open import Oscar.Class.Smap
open import Oscar.Class.Transitivity

module Oscar.Class.Surjtranscommutativity where

module Surjtranscommutativity
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂) (let infix 4 _∼̇₂_ ; _∼̇₂_ = _∼̇₂_)
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  (smap : Smap.type _∼₁_ _∼₂_ surjection surjection)
  (transitivity₁ : Transitivity.type _∼₁_)
  (let infixr 9 _∙₁_
       _∙₁_ : FlipTransitivity.type _∼₁_
       _∙₁_ g f = transitivity₁ f g)
  (transitivity₂ : Transitivity.type _∼₂_)
  (let infixr 9 _∙₂_
       _∙₂_ : FlipTransitivity.type _∼₂_
       _∙₂_ g f = transitivity₂ f g)
  = ℭLASS (_∼₁_ ,, _∼₂_ ,, (λ {x y} → _∼̇₂_ {x} {y}) ,, surjection ,, (λ {x y} → smap {x} {y}) ,, (λ {x y z} → transitivity₁ {x} {y} {z}) ,, (λ {x y z} → transitivity₂ {x} {y} {z})) (∀ {x y z} (f : x ∼₁ y) (g : y ∼₁ z) → smap (g ∙₁ f) ∼̇₂ smap g ∙₂ smap f)

module Surjtranscommutativity!
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂) (let infix 4 _∼̇₂_ ; _∼̇₂_ = _∼̇₂_)
  ⦃ I1 : Surjection.class 𝔒₁ 𝔒₂ ⦄
  ⦃ I2 : Smap!.class _∼₁_ _∼₂_ ⦄
  ⦃ I3 : Transitivity.class _∼₁_ ⦄
  ⦃ I4 : Transitivity.class _∼₂_ ⦄
  = Surjtranscommutativity (_∼₁_) (_∼₂_) (λ {x y} → _∼̇₂_ {x} {y}) smap transitivity transitivity

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} {_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} {_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
  {ℓ₂} {_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂}
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  {smap : Smap.type _∼₁_ _∼₂_ surjection surjection}
  {transitivity₁ : Transitivity.type _∼₁_}
  {transitivity₂ : Transitivity.type _∼₂_}
  where
  surjtranscommutativity = Surjtranscommutativity.method _∼₁_ _∼₂_ _∼̇₂_ smap transitivity₁ transitivity₂
  ⟪∙⟫-surjtranscommutativity-syntax = surjtranscommutativity
  syntax ⟪∙⟫-surjtranscommutativity-syntax f g = g ⟪∙⟫ f

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} {_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} {_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
  {ℓ₂} {_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂}
  ⦃ _ : Surjection.class 𝔒₁ 𝔒₂ ⦄
  ⦃ _ : Smap!.class _∼₁_ _∼₂_ ⦄
  ⦃ _ : Transitivity.class _∼₁_ ⦄
  ⦃ _ : Transitivity.class _∼₂_ ⦄
  where
  surjtranscommutativity! = Surjtranscommutativity!.method _∼₁_ _∼₂_ _∼̇₂_ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ ! ⦄
  ⟪∙⟫!-surjtranscommutativity-syntax = surjtranscommutativity!
  syntax ⟪∙⟫!-surjtranscommutativity-syntax f g = g ⟪∙⟫! f

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} {_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} {_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
  {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  {smap : Smap.type _∼₁_ _∼₂_ surjection surjection}
  {transitivity₁ : Transitivity.type _∼₁_}
  {transitivity₂ : Transitivity.type _∼₂_}
  where
  surjtranscommutativity[_] = Surjtranscommutativity.method _∼₁_ _∼₂_ _∼̇₂_ smap transitivity₁ transitivity₂
  ⟪∙⟫-surjtranscommutativity[]-syntax = surjtranscommutativity[_]
  syntax ⟪∙⟫-surjtranscommutativity[]-syntax t f g = g ⟪∙⟫[ t ] f

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} {_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁}
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} {_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂}
  {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  ⦃ _ : Surjection.class 𝔒₁ 𝔒₂ ⦄
  ⦃ _ : Smap!.class _∼₁_ _∼₂_ ⦄
  ⦃ _ : Transitivity.class _∼₁_ ⦄
  ⦃ _ : Transitivity.class _∼₂_ ⦄
  where
  surjtranscommutativity![_] = Surjtranscommutativity!.method _∼₁_ _∼₂_ _∼̇₂_ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ ! ⦄
  ⟪∙⟫!-surjtranscommutativity[]-syntax = surjtranscommutativity![_]
  syntax ⟪∙⟫!-surjtranscommutativity[]-syntax t f g = g ⟪∙⟫![ t ] f


text:
record Unit : Set where
  instance
    constructor tt

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module TimeSpace where

open import Prelude as P
  hiding
    ( [_]
    ; id
    ; _∘_
    ; _***_
    )
open import Container.List
open import Pi.Util

{-
A universe of finite types.
-}
data U : Set where
  𝟘 𝟙     : U
  _⊕_ _⊗_ : U → U → U
infixr 6 _⊕_
infixr 7 _⊗_

{-
A collection of "primitive" isomorphisms.
Selection was based on accepted definitions of categorical structures.
Monoidal categories have left and right unitors, and associators;
braided monoidal categories have commutators.

While the left/right unitor pairs might be considered redundant in light of the commutative morphism,
I decided to keep them. By matching the morphisms of relevant categorical structures, we can
examine the various categorical coherence laws for time/space tradeoffs. This isn't necessary,
but I want to test the effects of the change on the structure of the proofs.
-}
data _≅_ : U → U → Set where
  -- Coproduct monoid
  ⊕λ : ∀ {A}
     → 𝟘 ⊕ A ≅ A
  ⊕ρ : ∀ {A}
     → A ⊕ 𝟘 ≅ A
  ⊕σ : ∀ {A B}
     → A ⊕ B ≅ B ⊕ A
  ⊕α : ∀ {A B C}
     → (A ⊕ B) ⊕ C ≅ A ⊕ (B ⊕ C)
  -- Product monoid
  ⊗λ : ∀ {A}
     → 𝟙 ⊗ A ≅ A
  ⊗ρ : ∀ {A}
     → A ⊗ 𝟙 ≅ A
  ⊗σ : ∀ {A B}
     → A ⊗ B ≅ B ⊗ A
  ⊗α : ∀ {A B C}
     → (A ⊗ B) ⊗ C ≅ A ⊗ (B ⊗ C)
  -- Distributivity
  δ  : ∀ {A B C}
     → A ⊗ (B ⊕ C) ≅ (A ⊗ B) ⊕ (A ⊗ C)
infix 1 _≅_
{- Naming conventions:
  *λ : left unitor     : ε ∙ x ≅ x
  *ρ : right unitor    : x ∙ ε ≅ x
  *α : associator      : (x ∙ y) ∙ z ≅ x ∙ (y ∙ z)
  *σ : braid           : x ∙ y ≅ y ∙ x
  ⊗* : multiplicative variant, (𝟙 , ⊗)
  ⊕* : additive variant,       (𝟘 , ⊕)
  δ  : distributor     : x ⊗ (y ⊕ z) ≅ (x ⊗ y) ⊕ (x ⊗ z)
-}

infixr 5 _∘_
infix 1 _⟷_
data _⟷_ : U → U → Set where
  [_] : ∀ {A B}
      → A ≅ B
      → A ⟷ B
  id : ∀ {A}
    → A ⟷ A
  _⁻¹ : ∀ {A B}
    → A ⟷ B
    → B ⟷ A
  _∘_ : ∀ {A B C}
      → B ⟷ C
      → A ⟷ B
      → A ⟷ C
  _⊗_ : ∀ {A B C D}
      → A ⟷ B
      → C ⟷ D
      → A ⊗ C ⟷ B ⊗ D
  _⊕_ : ∀ {A B C D}
      → A ⟷ B
      → C ⟷ D
      → A ⊕ C ⟷ B ⊕ D

El : U → Set
El 𝟘       = ⊥
El 𝟙       = ⊤
El (A ⊕ B) = Either (El A) (El B)
El (A ⊗ B) = El A × El B

{-
bwd/fwd relate to the unitary morphisms,
while ap/ap⁻¹ relate to arbitrary morphisms.
-}

fwd : ∀ {A B}
    → A ≅ B
    → El A → El B
bwd : ∀ {A B}
    → A ≅ B
    → El B → El A

fwd ⊕λ (left ())
fwd ⊕λ (right x)        = x
fwd ⊕ρ (left x)         = x
fwd ⊕ρ (right ())
fwd ⊕σ (left x)         = right x
fwd ⊕σ (right x)        = left x
fwd ⊕α (left (left x))  = left x
fwd ⊕α (left (right x)) = right (left x)
fwd ⊕α (right x)        = right (right x)
fwd ⊗λ (tt , x)         = x
fwd ⊗ρ (x , tt)         = x
fwd ⊗σ (x , y)          = y , x
fwd ⊗α ((x , y) , z)    = x , y , z
fwd δ (x , left y)      = left (x , y)
fwd δ (x , right y)     = right (x , y)

bwd ⊕λ x                 = right x
bwd ⊕ρ x                 = left x
bwd ⊕σ (left x)          = right x
bwd ⊕σ (right x)         = left x
bwd ⊕α (left x)          = left (left x)
bwd ⊕α (right (left x))  = left (right x)
bwd ⊕α (right (right x)) = right x
bwd ⊗λ x                 = tt , x
bwd ⊗ρ x                 = x , tt
bwd ⊗σ (x , y)           = y , x
bwd ⊗α (x , y , z)       = (x , y) , z
bwd δ (left  (x , y))    = x , left y
bwd δ (right (x , y))    = x , right y

fwd-bwd : ∀ {A B}
        → (f : A ≅ B)
        → bwd f P.∘ fwd f ≃ P.id

fwd-bwd ⊕λ (left ())
fwd-bwd ⊕λ (right x)        = P.refl
fwd-bwd ⊕ρ (left x)         = P.refl
fwd-bwd ⊕ρ (right ())
fwd-bwd ⊕σ (left x)         = P.refl
fwd-bwd ⊕σ (right x)        = P.refl
fwd-bwd ⊕α (left (left x))  = P.refl
fwd-bwd ⊕α (left (right x)) = P.refl
fwd-bwd ⊕α (right x)        = P.refl
fwd-bwd ⊗λ (tt , x)         = P.refl
fwd-bwd ⊗ρ (x , tt)         = P.refl
fwd-bwd ⊗σ (x , y)          = P.refl
fwd-bwd ⊗α ((x , y) , z)    = P.refl
fwd-bwd δ (x , left y)      = P.refl
fwd-bwd δ (x , right y)     = P.refl

bwd-fwd : ∀ {A B}
        → (f : A ≅ B)
        → fwd f P.∘ bwd f ≃ P.id
bwd-fwd ⊕λ x                 = P.refl
bwd-fwd ⊕ρ x                 = P.refl
bwd-fwd ⊕σ (left x)          = P.refl
bwd-fwd ⊕σ (right x)         = P.refl
bwd-fwd ⊕α (left x)          = P.refl
bwd-fwd ⊕α (right (left x))  = P.refl
bwd-fwd ⊕α (right (right x)) = P.refl
bwd-fwd ⊗λ x                 = P.refl
bwd-fwd ⊗ρ x                 = P.refl
bwd-fwd ⊗σ (x , y)           = P.refl
bwd-fwd ⊗α (x , y , z)       = P.refl
bwd-fwd δ (left (x , y))     = P.refl
bwd-fwd δ (right (x , y))    = P.refl

infixr 1 ap ap⁻¹

ap : ∀ {A B}
   → A ⟷ B
   → El A → El B
ap⁻¹ : ∀ {A B}
     → A ⟷ B
     → El B → El A

ap [ f ]   = fwd f
ap id      = P.id
ap (f ⁻¹)  = ap⁻¹ f
ap (g ∘ f) = ap g P.∘ ap f
ap (f ⊗ g) = ap f *** ap g
ap (f ⊕ g) = ap f +++ ap g

ap⁻¹ [ f ]   = bwd f
ap⁻¹ id      = P.id
ap⁻¹ (f ⁻¹)  = ap f
ap⁻¹ (g ∘ f) = ap⁻¹ f P.∘ ap⁻¹ g
ap⁻¹ (f ⊗ g) = ap⁻¹ f *** ap⁻¹ g
ap⁻¹ (f ⊕ g) = ap⁻¹ f +++ ap⁻¹ g

ap-inv : ∀ {A B}
       → (f : A ⟷ B)
       → ap⁻¹ f P.∘ ap f ≃ P.id
inv-ap : ∀ {A B}
       → (f : A ⟷ B)
       → ap f P.∘ ap⁻¹ f ≃ P.id

ap-inv [ f ]   x = fwd-bwd f x
ap-inv id      x = P.refl
ap-inv (f ⁻¹)  x = inv-ap f x
ap-inv (g ∘ f) x =
  ap⁻¹ f $≡ ap-inv g (ap f x)
  ⟨≡⟩ ap-inv f x
ap-inv (f ⊗ g) (x , y) = cong₂ _,_ (ap-inv f x) (ap-inv g y)
ap-inv (f ⊕ g) (left x)  = left  $≡ ap-inv f x
ap-inv (f ⊕ g) (right x) = right $≡ ap-inv g x

inv-ap [ f ]   x = bwd-fwd f x
inv-ap id      x = P.refl
inv-ap (f ⁻¹)  x = ap-inv f x
inv-ap (g ∘ f) x =
  ap g $≡ inv-ap f (ap⁻¹ g x)
  ⟨≡⟩ inv-ap g x
inv-ap (f ⊗ g) (x , y) = cong₂ _,_ (inv-ap f x) (inv-ap g y)
inv-ap (f ⊕ g) (left x)  = left  $≡ inv-ap f x
inv-ap (f ⊕ g) (right x) = right $≡ inv-ap g x

syntax fwd  f x = f ♯ x
syntax bwd  f x = f ♭ x

syntax ap   f x = f ▸ x
syntax ap⁻¹ f x = f ◂ x

{-
The size of a type A is a natural number equal to the lub to any element of A.
We can also measure the size of an individual element of A, which may differ
for elements when there are sums present in A.
-}

size : U → Nat
size 𝟘 = 0
size 𝟙 = 1
size (A ⊕ B) = max (size A) (size B)
size (A ⊗ B) = size A + size B

sizeEl : ∀ A → El A → Nat
sizeEl 𝟘       ()
sizeEl 𝟙       tt        = 1
sizeEl (A ⊕ B) (left x)  = sizeEl A x
sizeEl (A ⊕ B) (right x) = sizeEl B x
sizeEl (A ⊗ B) (x , y)   = sizeEl A x + sizeEl B y

{-
`path-length` calculates the total number of computation steps required,
according to a given valuation of the primitive isomorphisms. (see _≅_ type defn)

For any (f : A ⟷ B), the number of steps taken to transform an (x : El A) to (ap f x : El B)
depends on the value of `x`, due to the difference in steps between the two possible cases
of `path-length (f ⊕ g)`.

-}

module _ (t : ∀ {A B} → A ≅ B → El A → Nat) where
  path-length : ∀ {A B} → A ⟷ B → El A → Nat
  --| in the primitive case, we use the supplied valuation.
  path-length [ f ]             = t f
  --| `id` has unit length. Although it does no work, an abstract machine processing
  --  the morphism (f ∘ id) might still need to decompose the task into processing `f`,
  --  and processing `id`.
  path-length id      _         = 1
  --| the inverse of a morphism f takes the same number of steps to compute
  --  as does f.
  path-length (f ⁻¹)  x         = path-length f (ap⁻¹ f x)
  --| composition is sequential, and so time is added.
  path-length (g ∘ f) x         = path-length f x + path-length g (ap f x)
  --| the product tensor runs two processes in parallel, and so takes
  --  the max time of the individual processes.
  path-length (f ⊗ g) (x , y)   = max (path-length f x) (path-length g y)
  --| The coproduct tensor of two processes may take different amounts of
  --  time to run, depending on from which side of the disjoint union
  --  a particular input element is drawn.
  path-length (f ⊕ g) (left x)  = path-length f x
  path-length (f ⊕ g) (right x) = path-length g x

{-
`circuit-length` is an upper bound of `path-length`, across all possible (x : El A).
Consequently, it is independent of any particular element (x : El A).

Here, a circuit is a spatial layout of a program in two dimensions, the "width" representing
"size", or memory usage, or storage requirements of a program, and the "length" representing
the stage of execution of the program.
-}

module _ (t : ∀ {A B} → A ≅ B → Nat) where
  circuit-length : ∀ {A B} → A ⟷ B → Nat
  circuit-length [ f ]   = t f
  circuit-length id      = 1
  circuit-length (f ⁻¹)  = circuit-length f
  circuit-length (g ∘ f) = circuit-length f + circuit-length g
  circuit-length (f ⊗ g) = max (circuit-length f) (circuit-length g)
  circuit-length (f ⊕ g) = max (circuit-length f) (circuit-length g)

{-
`circuit-width` measures the maximum width of the circuit described. viz. The maximum of the widths of all cross-section types.
-}

module _ (w : ∀ {A B} → A ≅ B → Nat) where
  circuit-width : ∀ {A B} → A ⟷ B → Nat
  circuit-width [ f ]   = w f
  circuit-width {A} id  = size A
  circuit-width (f ⁻¹)  = circuit-width f
  circuit-width (g ∘ f) = max (circuit-width f) (circuit-width g)
  circuit-width (f ⊗ g) = circuit-width f + circuit-width g
  circuit-width (f ⊕ g) = max (circuit-width f) (circuit-width g)

{-
Proposition: For any morphism f : A ⟷ B, (circuit-length f) is the least upper bound of (path-length f x), for any x.
-}

Max : ∀ A → (El A → Nat) → Nat
Max 𝟘 f = 0
Max 𝟙 f = f tt
Max (A ⊕ B) f = max (Max A (f P.∘ left)) (Max B (f P.∘ right))
Max (A ⊗ B) f = Max A λ a → Max B λ b → f (a , b)

Maximum : ∀ A (f : El A → Nat) (x : El A) → f x ≤ Max A f
Maximum 𝟘 f ()
Maximum 𝟙 f tt = diff! 0
Maximum (A ⊕ B) f (left x) = prf
  where
  MA : f (left x) ≤ Max A (f P.∘ left)
  MA = Maximum A (f P.∘ left) x
  prf : f (left x) ≤ max (Max A (f P.∘ left)) (Max B (f P.∘ right))
  prf = {!!}
Maximum (A ⊕ B) f (right x) = prf
  where
  MB : f (right x) ≤ Max B (f P.∘ right)
  MB = Maximum B (f P.∘ right) x
  prf : f (right x) ≤ max (Max A (f P.∘ left)) (Max B (f P.∘ right))
  prf = {!!}
Maximum (A ⊗ B) f (x , y) = {!!}

{-
Lemma: The max of a constant function is the value of the function.
-}
MaxConst : ∀ n A → El A → Max A (λ _ → n) ≡ n
MaxConst n 𝟘 ()
MaxConst n 𝟙 tt = P.refl
MaxConst n (A ⊕ B) (left x) = {!!}
MaxConst n (A ⊕ B) (right x) = {!!}
MaxConst n (A ⊗ B) (x , y) = {!!}

module _ (t : ∀ {A B} → A ≅ B → Nat) where
  path≤circuit : ∀ {A B}
               → (f : A ⟷ B)
               → Max A (path-length (λ f _ → t f) f) ≤ circuit-length t f
  path≤circuit [ f ]   = {!!}
  path≤circuit id      = {!!}
  path≤circuit (f ⁻¹)  = {!!}
  path≤circuit (g ∘ f) = {!!}
  path≤circuit (f ⊗ g) = {!!}
  path≤circuit (f ⊕ g) = {!!}

{-
Future work:
* Continue the literature search. Much of the underpinnings of this work are speculative,
  such as the definitions of 'width' and 'length'.
* Continue the search for time/space invariants, and other properties of equivalence classes
  of morphisms.
* Derive circuit-length circuit-width explicitly as LUBs
  over element dependent metrics path-length and path-width (currently undefined).
* Find examples! The primitive objects and morphisms used here will only produce
  straight-line programs.
* c.f. lit on complexity analysis and tradeoffs re. straight-line programs.
-}

-- These are the canonical equivalences arising from the categorical structure of a symmetric monoidal category.
-- I thought they might be a good place to start looking for nonzero time/space tradeoffs.

-- Should we investigate at all toward some form of distribuitive monoidal category?

{-
∘idₗ : ∀ {A B} (f : A ⟷ B) → id ∘ f ≅ f

∘idᵣ : ∀ {A B} (f : A ⟷ B) → f ∘ id ≅ f

∘invₗ : ∀ {A B} (f : A ⟷ B)
      → f ⁻¹ ∘ f ≅ id

∘invᵣ : ∀ {A B} (f : A ⟷ B)
      → f ∘ f ⁻¹ ≅ id

∘assoc : ∀ {A B C D}
       → (f : A ⟷ B) (g : B ⟷ C) (h : C ⟷ D)
       → (h ∘ g) ∘ f ≅ h ∘ (g ∘ f)

⁻¹cong : ∀ {A B}
       → {f g : A ⟷ B} → f ≅ g
       → f ⁻¹ ≅ g ⁻¹

∘cong : ∀ {A B C}
      → {f g : A ⟷ B} → f ≅ g
      → {h i : B ⟷ C} → h ≅ i
      → h ∘ f ≅ i ∘ g

⊗cong : ∀ {A B C D}
      → {f g : A ⟷ B} → f ≅ g
      → {h i : C ⟷ D} → h ≅ i
      → f ⊗ h ≅ g ⊗ i

⊕cong : ∀ {A B C D}
      → {f g : A ⟷ B} → f ≅ g
      → {h i : C ⟷ D} → h ≅ i
      → f ⊕ h ≅ g ⊕ i

∘/⁻¹ : ∀ {A B C}
     → (f : A ⟷ B) (g : B ⟷ C)
     → (g ∘ f) ⁻¹ ≅ f ⁻¹ ∘ g ⁻¹

⊗tri : ∀ {A B}
     → (id ⊗ [ ⊗λ ]) ∘ [ ⊗α ] ≅ [ ⊗ρ ] ⊗ id ∶ (A ⊗ 𝟙) ⊗ B ⟷ A ⊗ B

⊕tri : ∀ {A B}
     → (id ⊕ [ ⊕λ ]) ∘ [ ⊕α ] ≅ [ ⊕ρ ] ⊕ id ∶ (A ⊕ 𝟘) ⊕ B ⟷ A ⊕ B

⊕pent : ∀ {A B C D}
      → [ ⊕α ] ∘ [ ⊕α ] ≅ (id ⊕ [ ⊕α ]) ∘ [ ⊕α ] ∘ ([ ⊕α ] ⊕ id) ∶ ((A ⊕ B) ⊕ C) ⊕ D ⟷ A ⊕ (B ⊕ (C ⊕ D))

⊗pent : ∀ {A B C D}
      → [ ⊗α ] ∘ [ ⊗α ] ≅ (id ⊗ [ ⊗α ]) ∘ [ ⊗α ] ∘ ([ ⊗α ] ⊗ id) ∶ ((A ⊗ B) ⊗ C) ⊗ D ⟷ A ⊗ (B ⊗ (C ⊗ D))

⊗hex : ∀ {A B C}
     → (id ⊗ [ ⊗σ ]) ∘ [ ⊗α ] ∘ ([ ⊗σ ] ⊗ id) ≅ [ ⊗α ] ∘ [ ⊗σ ] ∘ [ ⊗α ] ∶ (A ⊗ B) ⊗ C ⟷ B ⊗ (C ⊗ A)

⊕hex : ∀ {A B C}
     → (id ⊕ [ ⊕σ ]) ∘ [ ⊕α ] ∘ ([ ⊕σ ] ⊕ id) ≅ [ ⊕α ] ∘ [ ⊕σ ] ∘ [ ⊕α ] ∶ (A ⊕ B) ⊕ C ⟷ B ⊕ (C ⊕ A)

⊗hex⁻¹ : ∀ {A B C}
       → ([ ⊗σ ] ⊗ id) ∘ [ ⊗α ] ⁻¹ ∘ (id ⊗ [ ⊗σ ]) ≅ [ ⊗α ] ⁻¹ ∘ [ ⊗σ ] ∘ [ ⊗α ] ⁻¹ ∶ A ⊗ (B ⊗ C) ⟷ (C ⊗ A) ⊗ B

⊕hex⁻¹ : ∀ {A B C}
       → ([ ⊕σ ] ⊕ id) ∘ [ ⊕α ] ⁻¹ ∘ (id ⊕ [ ⊕σ ]) ≅ [ ⊕α ] ⁻¹ ∘ [ ⊕σ ] ∘ [ ⊕α ] ⁻¹ ∶ A ⊕ (B ⊕ C) ⟷ (C ⊕ A) ⊕ B
-}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Was: test/Fail/Issue493
-- Andreas, 2020-06-08, issue #4737
-- Warn instead of hard error on useless hiding.

module _ where

module M where
  postulate A B C : Set
  data D : Set where

open M using (A) hiding (B; module D)


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data Interval : Set where
  left right : Interval
  path : left ≡ right

swap : Interval → Interval
swap left = right
swap right = left
swap (path i) = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --rewriting #-}
module Issue4048 where

data _==_ {i} {A : Set i} : (x y : A) → Set i where
  refl : {a : A} → a == a
{-# BUILTIN REWRITE _==_ #-}

postulate
  Π : (A : Set) (B : A → Set) → Set
  lam : {A : Set} {B : A → Set} (b : (a : A) → B a) → Π A B
  app : {A : Set} {B : A → Set} (f : Π A B) (a : A) → B a
  Π-β : {A : Set} {B : A → Set} (b : (a : A) → B a) (a : A) → app (lam b) a == b a
  {-# REWRITE Π-β #-}

postulate
  ⊤ : Set
  tt : ⊤
  ⊤-elim : ∀ {i} (A : ⊤ → Set i) (d : A tt) (x : ⊤) → A x
  ⊤-β : ∀ {i} (A : ⊤ → Set i) (d : A tt) → ⊤-elim A d tt == d
  {-# REWRITE ⊤-β #-}

tt' : ⊤
tt' = tt

module _
  (C : (p : ⊤) → Set)
  (z : C tt)
  where

  F : (n p x : ⊤) → C p
  F n p = app (⊤-elim (λ n → (p : ⊤) → Π ⊤ (λ _ → C p))
                       (⊤-elim _ (lam (⊤-elim _ z)))
                       n p)

  F-red : F tt tt tt == z
  F-red = refl

  -- Bug?
  F-red' : F tt tt' tt == z
  F-red' = refl  -- Not accepted, even though tt' is tt by definition.


text:
module _ where

open import Common.Prelude hiding (_>>=_; _<$>_)
open import Common.Reflection

infixl 8 _<$>_
_<$>_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → TC A → TC B
f <$> m = m >>= λ x → returnTC (f x)

macro
  default : Tactic
  default hole =
    inferType hole >>= λ
    { (def (quote Nat) []) → unify hole (lit (nat 42))
    ; (def (quote Bool) []) → unify hole (con (quote false) [])
    ; (meta x _) → catchTC (blockOnMeta x) (typeError (strErr "impossible" ∷ []))
                                            -- check that the block isn't caught
    ; _ → typeError (strErr "No default" ∷ [])
    }

aNat : Nat
aNat = default

aBool : Bool
aBool = default

alsoNat : Nat

soonNat : _
soonNat = default

alsoNat = soonNat


text:
module MLib.Fin.Parts.Simple where

open import MLib.Prelude
open import MLib.Fin.Parts.Core
open import MLib.Fin.Parts
open import MLib.Fin.Parts.Nat
import MLib.Fin.Parts.Nat.Simple as PNS

open Nat using (_*_; _+_; _<_)
open Fin using (toℕ; fromℕ≤)
open Table

open PNS using (sum-replicate-*; repl)

asParts : ∀ {a b} → Fin (a * b) ↔ (Fin a × Fin b)
asParts {a} {b} = ≡.subst (λ n → Fin n ↔ (Fin a × Fin b)) (sum-replicate-* a b) (Parts.asParts (constParts a b))

fromParts : ∀ {a b} → Fin a × Fin b → Fin (a * b)
fromParts = Inverse.from asParts ⟨$⟩_

toParts : ∀ {a b} → Fin (a * b) → Fin a × Fin b
toParts = Inverse.to asParts ⟨$⟩_

fromParts³′ : ∀ {a b c} → Fin a × Fin b × Fin c → Fin (a * (b * c))
fromParts³′ {a} {b} {c} (i , j , k) = fromParts (i , fromParts (j , k))

fromParts³ : ∀ {a b c} → Fin a × Fin b × Fin c → Fin (a * b * c)
fromParts³ {a} {b} {c} (i , j , k) = fromParts (fromParts (i , j) , k)

private
  fromParts′ : ∀ {a b} → Fin a × Fin b → Fin (sum (repl a b))
  fromParts′ {a} {b} = Parts.fromParts (constParts a b)

  toParts′ : ∀ {a b} → Fin (sum (repl a b)) → Fin a × Fin b
  toParts′ {a} {b} = Parts.toParts (constParts a b)

  asParts-prop : ∀ {a b} → asParts {a} {b} ≅ Parts.asParts (constParts a b)
  asParts-prop {a} {b} = ≅.≡-subst-removable _ _ _

  abstract
    fromParts′-prop : ∀ {a b} (ij : Fin a × Fin b) → toℕ (fromParts ij) ≡ toℕ (fromParts′ ij)
    fromParts′-prop {a} {b} ij =
      ≅.≅-to-≡ (≅.icong (λ n → Fin n ↔ (Fin a × Fin b))
                         (≡.sym (sum-replicate-* a b))
                         (λ {n} (ap : Fin n ↔ (Fin a × Fin b)) → toℕ (Inverse.from ap ⟨$⟩ ij))
                         asParts-prop)

    toParts′-prop : ∀ {a b} {x : Fin (a * b)} {x′ : Fin (sum (repl a b))} → x ≅ x′ → Σ.map toℕ toℕ (toParts {a} x) ≡ Σ.map toℕ toℕ (toParts′ {a} x′)
    toParts′-prop {a} {b} {x} {x′} x≅x′ =
      ≅.≅-to-≡ (≅.icong₂
        (λ n → Fin n ↔ (Fin a × Fin b))
        (≡.sym (sum-replicate-* a b))
        (λ {n} (ap : Fin n ↔ (Fin a × Fin b)) x → Σ.map toℕ toℕ (Inverse.to ap ⟨$⟩ x))
        asParts-prop
        x≅x′)

    fromParts³′-prop : ∀ {a b c} (i : Fin a) (j : Fin b) (k : Fin c) → toℕ (fromParts³′ (i , j , k)) ≡ PNS.fromParts³′ a b c (toℕ i , toℕ j , toℕ k)
    fromParts³′-prop {a} {b} {c} i j k =
      begin
        toℕ (fromParts (i , fromParts (j , k)))                                                 ≡⟨ fromParts′-prop (i , _) ⟩
        toℕ (fromParts′ (i , fromParts (j , k)))                                                ≡⟨ Parts.fromParts-fromPartsℕ (constParts a (b * c)) i _ ⟩
        Partsℕ.fromParts (constParts a (b * c)) (toℕ i , toℕ (fromParts (j , k)))           ≡⟨ ≡.cong₂ (λ x y → Partsℕ.fromParts (constParts a x) (toℕ i , y))
                                                                                (≡.sym (sum-replicate-* b c))
                                                                                (fromParts′-prop (j , k)) ⟩
        Partsℕ.fromParts (constParts a (sum (repl b c))) (toℕ i , toℕ (fromParts′ (j , k)))  ≡⟨ ≡.sym (Parts.fromParts-fromPartsℕ (constParts a _) i _) ⟩
        toℕ (Parts.fromParts (constParts a (sum (repl b c))) (i , fromParts′ (j , k)))        ≡⟨ Parts.fromParts-fromPartsℕ (constParts a (sum (repl b c))) i _ ⟩
        PNS.fromParts a (sum (repl b c)) (toℕ i , toℕ (fromParts′ (j , k)))                  ≡⟨ ≡.cong₂ (λ x y → PNS.fromParts a x (toℕ i , y))
                                                                                (sum-replicate-* b c)
                                                                                (Parts.fromParts-fromPartsℕ (constParts b c) j k) ⟩
        PNS.fromParts a (b * c) (toℕ i , PNS.fromParts b c (toℕ j , toℕ k))               ∎
      where
      open ≡.Reasoning

    fromParts³-prop : ∀ {a b c} (i : Fin a) (j : Fin b) (k : Fin c) → toℕ (fromParts³ (i , j , k)) ≡ PNS.fromParts³ a b c (toℕ i , toℕ j , toℕ k)
    fromParts³-prop {a} {b} {c} i j k =
      begin
        toℕ (fromParts (fromParts (i , j) , k))                                                  ≡⟨ fromParts′-prop (fromParts (i , j) , k) ⟩
        toℕ (fromParts′ (fromParts (i , j) , k))                                                 ≡⟨ Parts.fromParts-fromPartsℕ (constParts (a * b) c) (fromParts (i , j)) k ⟩
        Partsℕ.fromParts (constParts (a * b) c) (toℕ (fromParts (i , j)) , toℕ k)            ≡⟨ ≡.cong₂ (λ x y → Partsℕ.fromParts (constParts x c) (y , toℕ k))
                                                                                (≡.sym (sum-replicate-* a b))
                                                                                (fromParts′-prop (i , j)) ⟩
        Partsℕ.fromParts (constParts (sum (repl a b)) c) (toℕ (fromParts′ (i , j)) , toℕ k)   ≡⟨ ≡.sym (Parts.fromParts-fromPartsℕ (constParts _ c) (fromParts′ (i , j)) k) ⟩
        toℕ (fromParts′ (fromParts′ (i , j) , k))                                                 ≡⟨ Parts.fromParts-fromPartsℕ (constParts _ c) (fromParts′ (i , j)) k ⟩
        PNS.fromParts (sum (repl a b)) c (toℕ (fromParts′ (i , j)) , toℕ k)                   ≡⟨ ≡.cong₂ (λ x y → PNS.fromParts x c (y , toℕ k))
                                                                                (sum-replicate-* a b)
                                                                                (Parts.fromParts-fromPartsℕ (constParts a b) i j) ⟩
        PNS.fromParts (a * b) c (PNS.fromParts a b (toℕ i , toℕ j) , toℕ k)                ∎
      where open ≡.Reasoning

abstract
  fromParts-assoc : ∀ {a b c} (ijk : Fin a × Fin b × Fin c) → fromParts³ ijk ≅ fromParts³′ ijk
  fromParts-assoc {a} {b} {c} (i , j , k) =
    Fin.toℕ-injective′ (begin
      toℕ (fromParts³ (i , j , k))                       ≡⟨ fromParts³-prop i j k ⟩
      PNS.fromParts³ a b c (toℕ i , toℕ j , toℕ k)   ≡⟨ ≡.sym (PNS.fromParts-assoc _ _ _ (Fin.bounded i) (Fin.bounded j) (Fin.bounded k)) ⟩
      PNS.fromParts³′ a b c (toℕ i , toℕ j , toℕ k)  ≡⟨ ≡.sym (fromParts³′-prop i j k) ⟩
      toℕ (fromParts³′ (i , j , k))                      ∎)
    (Nat.*-assoc a _ _)
    where open ≡.Reasoning

module _ (a b c : ℕ) where

  toParts³ : Fin (a * b * c) → Fin a × Fin b × Fin c
  toParts³ x =
    let ij , k = toParts x
        i , j = toParts ij
    in i , j , k

  toParts³′ : Fin (a * (b * c)) → Fin a × Fin b × Fin c
  toParts³′ i =
    let i₁ , i₂₃ = toParts i
        i₂ , i₃ = toParts i₂₃
    in i₁ , i₂ , i₃

  abstract
    fromParts³-toParts³ : ∀ i → fromParts³ (toParts³ i) ≡ i
    fromParts³-toParts³ x =
      let i , j , k = toParts³ x
          open ≡.Reasoning
      in begin
        fromParts³ (toParts³ x)          ≡⟨⟩
        fromParts (fromParts (i , j) , k)  ≡⟨ ≡.cong (fromParts ∘ (_, k)) (asParts {a} {b} .Inverse.left-inverse-of (toParts x .proj₁)) ⟩
        fromParts {a * b} (toParts x)    ≡⟨ asParts {a * b} .Inverse.left-inverse-of x ⟩
        x                                  ∎

    toParts³′-fromParts³′ : ∀ ijk → toParts³′ (fromParts³′ ijk) ≡ ijk
    toParts³′-fromParts³′ (i , j , k) =
      let i′ , j′ , k′ = toParts³′ (fromParts³′ (i , j , k))
          p , q = Σ.≡⇒≡×≡ (asParts .Inverse.right-inverse-of (i , fromParts (j , k)))
          q′ = ≡.trans (≡.cong toParts q) (asParts .Inverse.right-inverse-of (j , k))

      in Σ.≡×≡⇒≡ (p , q′)

    toParts-assoc : {i : Fin (a * b * c)} {i′ : Fin (a * (b * c))} → i ≅ i′ → toParts³ i ≡ toParts³′ i′
    toParts-assoc {i} {i′} eq =
      begin
        toParts³ i                              ≡⟨ ≡.sym (toParts³′-fromParts³′ _) ⟩
        toParts³′ (fromParts³′ (toParts³ i))  ≡⟨ ≡.cong toParts³′ lem ⟩
        toParts³′ i′                            ∎
      where
      lem : fromParts³′ (toParts³ i) ≡ i′
      lem = ≅.≅-to-≡ (
        let open ≅.Reasoning
        in begin
          fromParts³′ (toParts³ i)   ≅⟨ ≅.sym (fromParts-assoc (toParts³ i)) ⟩
          fromParts³ (toParts³ i)    ≡⟨ fromParts³-toParts³ i ⟩
          i                            ≅⟨ eq ⟩
          i′                           ∎)

      open ≡.Reasoning

    toParts³-fromParts³ : ∀ ijk → toParts³ (fromParts³ ijk) ≡ ijk
    toParts³-fromParts³ ijk =
      begin
        toParts³  (fromParts³ ijk)    ≡⟨ toParts-assoc (fromParts-assoc ijk) ⟩
        toParts³′ (fromParts³′ ijk)   ≡⟨ toParts³′-fromParts³′ ijk ⟩
        ijk                             ∎
      where open ≡.Reasoning

    fromParts³′-toParts³′ : ∀ k → fromParts³′ (toParts³′ k) ≡ k
    fromParts³′-toParts³′ k =
      let k′ = ≡.subst Fin (≡.sym (Nat.*-assoc a b c)) k
          k′≅k = ≅.≡-subst-removable Fin _ k
      in ≅.≅-to-≡ (begin
        fromParts³′ (toParts³′ k )   ≡⟨ ≡.cong fromParts³′ (≡.sym (toParts-assoc k′≅k)) ⟩
        fromParts³′ (toParts³  k′)   ≅⟨ ≅.sym (fromParts-assoc (toParts³ k′)) ⟩
        fromParts³  (toParts³  k′)   ≡⟨ fromParts³-toParts³ k′ ⟩
        k′                             ≅⟨ k′≅k ⟩
        k                              ∎)
      where open ≅.Reasoning

  asParts³ : Fin (a * b * c) ↔ (Fin a × Fin b × Fin c)
  asParts³ = record
    { to = ≡.→-to-⟶ toParts³
    ; from = ≡.→-to-⟶ fromParts³
    ; inverse-of = record
      { left-inverse-of = fromParts³-toParts³
      ; right-inverse-of = toParts³-fromParts³
      }
    }

  asParts³′ : Fin (a * (b * c)) ↔ (Fin a × Fin b × Fin c)
  asParts³′ = record
    { to = ≡.→-to-⟶ toParts³′
    ; from = ≡.→-to-⟶ fromParts³′
    ; inverse-of = record
      { left-inverse-of = fromParts³′-toParts³′
      ; right-inverse-of = toParts³′-fromParts³′
      }
    }

abstract
  toParts-1ˡ : ∀ {b} (x : Fin (1 * b)) (x′ : Fin b) → x ≅ x′ → toParts {1} x ≡ (zero , x′)
  toParts-1ˡ {b} x x′ x≅x′ =
    let i  , j = toParts {1} x
        i′ , j′ = toParts′ {1} x
        i′′ , j′′ = Partsℕ.toParts (constParts 1 b) (toℕ x)
        i≅i′ , j≅j′ = Σ.≡⇒≡×≡ (toParts′-prop {1} {x = x} {x′ = x} ≅.refl)

        i′≅i′′ , j′≅j′′ = Σ.≡⇒≡×≡ (Parts.toParts-toPartsℕ (constParts 1 b) x)
        p , q = Σ.≡⇒≡×≡ (PNS.toParts-1ˡ {b} _ (Nat.≤-trans (Fin.bounded x) (Nat.≤-reflexive (Nat.*-identityˡ _))))
        open ≡.Reasoning
    in Σ.≡×≡⇒≡
      ( Fin.toℕ-injective (begin
          toℕ i  ≡⟨ i≅i′ ⟩
          toℕ i′ ≡⟨ i′≅i′′ ⟩
          i′′    ≡⟨ p ⟩
          0      ∎)
      , Fin.toℕ-injective (begin
          toℕ j    ≡⟨ j≅j′ ⟩
          toℕ j′   ≡⟨ j′≅j′′ ⟩
          j′′      ≡⟨ q ⟩
          toℕ x    ≡⟨ ≅.≅-to-≡ (≅.icong Fin (Nat.*-identityˡ _) toℕ x≅x′) ⟩
          toℕ x′   ∎)
      )

  toParts-1ʳ : ∀ {a} (x : Fin (a * 1)) (x′ : Fin a) → x ≅ x′ → toParts x ≡ (x′ , zero)
  toParts-1ʳ {a} x x′ x≅x′ =
    let x′′ : Fin (sum (repl a 1))
        x′′ = ≡.subst Fin (≡.sym (sum-replicate-* a 1)) x

        x≅x′′ = ≅.sym (≅.≡-subst-removable Fin (≡.sym (sum-replicate-* a 1)) x)
        x′′≅x′ = ≅.trans (≅.sym x≅x′′) x≅x′
        sra≡a = ≡.trans (sum-replicate-* a 1) (Nat.*-identityʳ a)

        i , j = toParts x
        i′ , j′ = toParts′ {a} {1} x′′
        i′′ , j′′ = Partsℕ.toParts (constParts a 1) (toℕ x′′)

        i≅i′ , j≅j′ = Σ.≡⇒≡×≡ (toParts′-prop {a} {x = x} {x′ = x′′} x≅x′′)
        i′≅i′′ , j′≅j′′ = Σ.≡⇒≡×≡ (Parts.toParts-toPartsℕ (constParts a 1) x′′)

        p , q = Σ.≡⇒≡×≡ (PNS.toParts-1ʳ {a} (toℕ x′′) (Nat.≤-trans (Nat.≤-reflexive (≅.≅-to-≡ (≅.icong Fin sra≡a (suc ∘ toℕ) x′′≅x′))) (Fin.bounded x′)))

        open ≡.Reasoning
    in Σ.≡×≡⇒≡
      ( Fin.toℕ-injective (begin
          toℕ i    ≡⟨ i≅i′ ⟩
          toℕ i′   ≡⟨ i′≅i′′ ⟩
          i′′      ≡⟨ p ⟩
          toℕ x′′  ≡⟨ ≅.≅-to-≡ (≅.icong Fin sra≡a toℕ x′′≅x′) ⟩
          toℕ x′   ∎)
      , Fin.toℕ-injective (begin
          toℕ j  ≡⟨ j≅j′ ⟩
          toℕ j′ ≡⟨ j′≅j′′ ⟩
          j′′     ≡⟨ q ⟩
          0      ∎)
      )


text:
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.Equality

postulate
  A B : Set
  b : B

f : List A → Char → B
f _ 'a' = b
f [] _  = b
f _  _  = b

test : ∀ xs → f xs 'a' ≡ b
test _ = refl


text:
{-# OPTIONS --sized-types #-}
module Builtin.Size where

open import Agda.Builtin.Size public

max_stars_repo_name: UlfNorell/agda-prelude

max_issues_repo_name: UlfNorell/agda-prelude

max_forks_repo_name: UlfNorell/agda-prelude


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

------------------------------------------------------------------------
-- Re-exports of the Data.List.Kleene module, renamed to duplicate the
-- Data.List API.

module Data.List.Kleene.AsList where

import Data.List.Kleene.Base as Kleene
open import Data.List.Kleene.Base
  using
    ( []
    )
  renaming
    ( _⋆ to List
    ; foldr⋆ to foldr
    ; foldl⋆ to foldl
    ; _⋆++⋆_ to _++_
    ; map⋆ to map
    ; pure⋆ to pure
    ; _⋆<*>⋆_ to _<*>_
    ; _⋆>>=⋆_ to _>>=_
    ; mapAccumL⋆ to mapAccumL
    ; _[_]⋆ to _[_]
    ; applyUpTo⋆ to applyUpTo
    ; upTo⋆ to upTo
    ; intersperse⋆ to intersperse
    ; _⋆<|>⋆_ to _<|>_
    ; ⋆zipWith⋆ to zipWith
    ; unzipWith⋆ to unzipWith
    ; partitionSumsWith⋆ to partitionSumsWith
    ; ⋆transpose⋆ to transpose
    ; reverse⋆ to reverse
    )
  public

infixr 5 _∷_
pattern _∷_ x xs = Kleene.∹ x Kleene.& xs

scanr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → List B
scanr f b xs = Kleene.∹ Kleene.scanr⋆ f b xs

scanl : ∀ {a b} {A : Set a} {B : Set b} → (B → A → B) → B → List A → List B
scanl f b xs = Kleene.∹ Kleene.scanl⋆ f b xs

tails : ∀ {a} {A : Set a} → List A → List (List A)
tails xs = foldr (λ x xs → (Kleene.∹ x) ∷ xs) ([] ∷ []) (Kleene.tails⋆ xs)

import Data.List.Kleene.Syntax

module Syntax = Data.List.Kleene.Syntax using (_]; _,_) renaming (⋆[_ to [_)

max_stars_repo_name: oisdk/agda-kleene-lists

max_issues_repo_name: oisdk/agda-kleene-lists

max_forks_repo_name: oisdk/agda-kleene-lists


text:
-- some examples for structural order in the termination checker

module StructuralOrder where

data Nat : Set where
   zero : Nat
   succ : Nat -> Nat

-- c t > t  for any term t
-- e.g., succ (succ y) > succ y
plus : Nat -> Nat -> Nat
plus x (succ (succ y)) = succ (plus x (succ y))
plus x (succ zero) = succ x
plus x zero        = x

-- constructor names do not matter
-- c (c' t) > c'' t
-- e.g. c0 (c1 x) > c0 x
--      c0 (c0 x) > c1 x

-- Actually constructor names does matter until the non-mattering is
-- implemented properly.

{- TEMPORARILY REMOVED by Ulf since there are problems with the constructor-name ignoring
data Bin : Set where
  eps : Bin
  c0  : Bin -> Bin
  c1  : Bin -> Bin

foo : Bin -> Nat
foo eps = zero
foo (c0 eps) = zero
foo (c0 (c1 x)) = succ (foo (c0 x))
foo (c0 (c0 x)) = succ (foo (c1 x))
foo (c1 x)      = succ (foo x)
-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to ◇
------------------------------------------------------------------------

module Data.Container.Any where

open import Algebra
open import Data.Container as C
open import Data.Container.Combinator
  using (module Composition) renaming (_∘_ to _⟨∘⟩_)
open import Data.Product as Prod hiding (swap)
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Related as Related using (Related)
open import Function.Related.TypeIsomorphisms
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_; refl)
import Relation.Binary.Sigma.Pointwise as Σ

open Related.EquationalReasoning
private
  module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)

-- ◇ can be expressed using _∈_.

↔∈ : ∀ {c} (C : Container c) {X : Set c}
       {P : X → Set c} {xs : ⟦ C ⟧ X} →
     ◇ P xs ↔ (∃ λ x → x ∈ xs × P x)
↔∈ _ {P = P} {xs} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl
    ; right-inverse-of = to∘from
    }
  }
  where
  to : ◇ P xs → ∃ λ x → x ∈ xs × P x
  to (p , Px) = (proj₂ xs p , (p , refl) , Px)

  from : (∃ λ x → x ∈ xs × P x) → ◇ P xs
  from (.(proj₂ xs p) , (p , refl) , Px) = (p , Px)

  to∘from : to ∘ from ≗ id
  to∘from (.(proj₂ xs p) , (p , refl) , Px) = refl

-- ◇ is a congruence for bag and set equality and related preorders.

cong : ∀ {k c} {C : Container c}
         {X : Set c} {P₁ P₂ : X → Set c} {xs₁ xs₂ : ⟦ C ⟧ X} →
       (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
       Related k (◇ P₁ xs₁) (◇ P₂ xs₂)
cong {C = C} {P₁ = P₁} {P₂} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
  ◇ P₁ xs₁                  ↔⟨ ↔∈ C ⟩
  (∃ λ x → x ∈ xs₁ × P₁ x)  ∼⟨ Σ.cong Inv.id (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
  (∃ λ x → x ∈ xs₂ × P₂ x)  ↔⟨ sym (↔∈ C) ⟩
  ◇ P₂ xs₂                  ∎

-- Nested occurrences of ◇ can sometimes be swapped.

swap : ∀ {c} {C₁ C₂ : Container c} {X Y : Set c} {P : X → Y → Set c}
         {xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
       let ◈ : ∀ {C : Container c} {X} → ⟦ C ⟧ X → (X → Set c) → Set c
           ◈ = λ {_} {_} → flip ◇ in
       ◈ xs (◈ ys ∘ P) ↔ ◈ ys (◈ xs ∘ flip P)
swap {c} {C₁} {C₂} {P = P} {xs} {ys} =
  ◇ (λ x → ◇ (P x) ys) xs                    ↔⟨ ↔∈ C₁ ⟩
  (∃ λ x → x ∈ xs × ◇ (P x) ys)              ↔⟨ Σ.cong Inv.id (λ {x} → Inv.id ⟨ ×⊎.*-cong {ℓ = c} ⟩ ↔∈ C₂ {P = P x}) ⟩
  (∃ λ x → x ∈ xs × ∃ λ y → y ∈ ys × P x y)  ↔⟨ Σ.cong Inv.id (λ {x} → ∃∃↔∃∃ {A = x ∈ xs} (λ _ y → y ∈ ys × P x y)) ⟩
  (∃₂ λ x y → x ∈ xs × y ∈ ys × P x y)       ↔⟨ ∃∃↔∃∃ (λ x y → x ∈ xs × y ∈ ys × P x y) ⟩
  (∃₂ λ y x → x ∈ xs × y ∈ ys × P x y)       ↔⟨ Σ.cong Inv.id (λ {y} → Σ.cong Inv.id (λ {x} →
    (x ∈ xs × y ∈ ys × P x y)                     ↔⟨ sym $ ×⊎.*-assoc _ _ _ ⟩
    ((x ∈ xs × y ∈ ys) × P x y)                   ↔⟨ ×⊎.*-comm _ _ ⟨ ×⊎.*-cong {ℓ = c} ⟩ Inv.id ⟩
    ((y ∈ ys × x ∈ xs) × P x y)                   ↔⟨ ×⊎.*-assoc _ _ _ ⟩
    (y ∈ ys × x ∈ xs × P x y)                     ∎)) ⟩
  (∃₂ λ y x → y ∈ ys × x ∈ xs × P x y)       ↔⟨ Σ.cong Inv.id (λ {y} → ∃∃↔∃∃ {B = y ∈ ys} (λ x _ → x ∈ xs × P x y)) ⟩
  (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong Inv.id (λ {y} → Inv.id ⟨ ×⊎.*-cong {ℓ = c} ⟩ sym (↔∈ C₁ {P = flip P y})) ⟩
  (∃ λ y → y ∈ ys × ◇ (flip P y) xs)         ↔⟨ sym (↔∈ C₂) ⟩
  ◇ (λ y → ◇ (flip P y) xs) ys               ∎

-- Nested occurrences of ◇ can sometimes be flattened.

flatten : ∀ {c} {C₁ C₂ : Container c} {X}
          P (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
          ◇ (◇ P) xss ↔
          ◇ P (Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss)
flatten {C₁ = C₁} {C₂} {X} P xss = record
  { to         = P.→-to-⟶ t
  ; from       = P.→-to-⟶ f
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl
    ; right-inverse-of = λ _ → refl
    }
  }
  where
  open Inverse

  t : ◇ (◇ P) xss → ◇ P (from (Composition.correct C₁ C₂) ⟨$⟩ xss)
  t (p₁ , p₂ , p) = ((p₁ , p₂) , p)

  f : ◇ P (from (Composition.correct C₁ C₂) ⟨$⟩ xss) → ◇ (◇ P) xss
  f ((p₁ , p₂) , p) = (p₁ , p₂ , p)

-- Sums commute with ◇ (for a fixed instance of a given container).

◇⊎↔⊎◇ : ∀ {c} {C : Container c} {X : Set c} {xs : ⟦ C ⟧ X}
          {P Q : X → Set c} →
        ◇ (λ x → P x ⊎ Q x) xs ↔ (◇ P xs ⊎ ◇ Q xs)
◇⊎↔⊎◇ {xs = xs} {P} {Q} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
    }
  }
  where
  to : ◇ (λ x → P x ⊎ Q x) xs → ◇ P xs ⊎ ◇ Q xs
  to (pos , inj₁ p) = inj₁ (pos , p)
  to (pos , inj₂ q) = inj₂ (pos , q)

  from : ◇ P xs ⊎ ◇ Q xs → ◇ (λ x → P x ⊎ Q x) xs
  from = [ Prod.map id inj₁ , Prod.map id inj₂ ]

  from∘to : from ∘ to ≗ id
  from∘to (pos , inj₁ p) = refl
  from∘to (pos , inj₂ q) = refl

-- Products "commute" with ◇.

×◇↔◇◇× : ∀ {c} {C₁ C₂ : Container c}
           {X Y} {P : X → Set c} {Q : Y → Set c}
           {xs : ⟦ C₁ ⟧ X} {ys : ⟦ C₂ ⟧ Y} →
         ◇ (λ x → ◇ (λ y → P x × Q y) ys) xs ↔ (◇ P xs × ◇ Q ys)
×◇↔◇◇× {C₁ = C₁} {C₂} {P = P} {Q} {xs} {ys} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = λ _ → refl
    ; right-inverse-of = λ _ → refl
    }
  }
  where
  to : ◇ (λ x → ◇ (λ y → P x × Q y) ys) xs → ◇ P xs × ◇ Q ys
  to (p₁ , p₂ , p , q) = ((p₁ , p) , (p₂ , q))

  from : ◇ P xs × ◇ Q ys → ◇ (λ x → ◇ (λ y → P x × Q y) ys) xs
  from ((p₁ , p) , (p₂ , q)) = (p₁ , p₂ , p , q)

-- map can be absorbed by the predicate.

map↔∘ : ∀ {c} (C : Container c) {X Y : Set c}
        (P : Y → Set c) {xs : ⟦ C ⟧ X} (f : X → Y) →
        ◇ P (C.map f xs) ↔ ◇ (P ∘ f) xs
map↔∘ _ _ _ = Inv.id

-- Membership in a mapped container can be expressed without reference
-- to map.

∈map↔∈×≡ : ∀ {c} (C : Container c) {X Y : Set c} {f : X → Y}
             {xs : ⟦ C ⟧ X} {y} →
           y ∈ C.map f xs ↔ (∃ λ x → x ∈ xs × y ≡ f x)
∈map↔∈×≡ {c} C {f = f} {xs} {y} =
  y ∈ C.map f xs              ↔⟨ map↔∘ C (_≡_ y) f ⟩
  ◇ (λ x → y ≡ f x) xs        ↔⟨ ↔∈ C ⟩
  (∃ λ x → x ∈ xs × y ≡ f x)  ∎

-- map is a congruence for bag and set equality and related preorders.

map-cong : ∀ {k c} {C : Container c} {X Y : Set c}
             {f₁ f₂ : X → Y} {xs₁ xs₂ : ⟦ C ⟧ X} →
           f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
           C.map f₁ xs₁ ∼[ k ] C.map f₂ xs₂
map-cong {c = c} {C} {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
  x ∈ C.map f₁ xs₁        ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
  ◇ (λ y → x ≡ f₁ y) xs₁  ∼⟨ cong {xs₁ = xs₁} {xs₂ = xs₂} (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
  ◇ (λ y → x ≡ f₂ y) xs₂  ↔⟨ sym (map↔∘ C (_≡_ x) f₂) ⟩
  x ∈ C.map f₂ xs₂        ∎
  where
  helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y)
  helper y = record
    { to         = P.→-to-⟶ (λ x≡f₁y → P.trans x≡f₁y (        f₁≗f₂ y))
    ; from       = P.→-to-⟶ (λ x≡f₂y → P.trans x≡f₂y (P.sym $ f₁≗f₂ y))
    ; inverse-of = record
      { left-inverse-of  = λ _ → P.proof-irrelevance _ _
      ; right-inverse-of = λ _ → P.proof-irrelevance _ _
      }
    }

-- Uses of linear morphisms can be removed.

remove-linear :
  ∀ {c} {C₁ C₂ : Container c} {X} {xs : ⟦ C₁ ⟧ X}
  (P : X → Set c) (m : C₁ ⊸ C₂) →
  ◇ P (⟪ m ⟫⊸ xs) ↔ ◇ P xs
remove-linear {xs = xs} P m = record
  { to         = P.→-to-⟶ t
  ; from       = P.→-to-⟶ f
  ; inverse-of = record
    { left-inverse-of  = f∘t
    ; right-inverse-of = t∘f
    }
  }
  where
  open Inverse

  t : ◇ P (⟪ m ⟫⊸ xs) → ◇ P xs
  t = Prod.map (_⟨$⟩_ (to (position⊸ m))) id

  f : ◇ P xs → ◇ P (⟪ m ⟫⊸ xs)
  f = Prod.map (_⟨$⟩_ (from (position⊸ m)))
               (P.subst (P ∘ proj₂ xs)
                        (P.sym $ right-inverse-of (position⊸ m) _))

  f∘t : f ∘ t ≗ id
  f∘t (p₂ , p) = H.≅-to-≡ $
    H.cong₂ _,_ (H.≡-to-≅ $ left-inverse-of (position⊸ m) p₂)
                (H.≡-subst-removable
                  (P ∘ proj₂ xs)
                  (P.sym (right-inverse-of (position⊸ m)
                                           (to (position⊸ m) ⟨$⟩ p₂)))
                  p)

  t∘f : t ∘ f ≗ id
  t∘f (p₁ , p) = H.≅-to-≡ $
    H.cong₂ _,_ (H.≡-to-≅ $ right-inverse-of (position⊸ m) p₁)
                (H.≡-subst-removable
                  (P ∘ proj₂ xs)
                  (P.sym (right-inverse-of (position⊸ m) p₁))
                  p)

-- Linear endomorphisms are identity functions if bag equality is
-- used.

linear-identity :
  ∀ {c} {C : Container c} {X} {xs : ⟦ C ⟧ X} (m : C ⊸ C) →
  ⟪ m ⟫⊸ xs ∼[ bag ] xs
linear-identity {xs = xs} m {x} =
  x ∈ ⟪ m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m ⟩
  x ∈        xs  ∎

-- If join can be expressed using a linear morphism (in a certain
-- way), then it can be absorbed by the predicate.

join↔◇ : ∀ {c} {C₁ C₂ C₃ : Container c} {X}
         P (join′ : (C₁ ⟨∘⟩ C₂) ⊸ C₃) (xss : ⟦ C₁ ⟧ (⟦ C₂ ⟧ X)) →
         let join : ∀ {X} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ X) → ⟦ C₃ ⟧ X
             join = λ {_} → ⟪ join′ ⟫⊸ ∘
                    _⟨$⟩_ (Inverse.from (Composition.correct C₁ C₂)) in
         ◇ P (join xss) ↔ ◇ (◇ P) xss
join↔◇ {C₁ = C₁} {C₂} P join xss =
  ◇ P (⟪ join ⟫⊸ xss′)  ↔⟨ remove-linear P join ⟩
  ◇ P            xss′   ↔⟨ sym $ flatten P xss ⟩
  ◇ (◇ P) xss           ∎
  where xss′ = Inverse.from (Composition.correct C₁ C₂) ⟨$⟩ xss


text:
-- Andreas, 2019-08-20, issue #4012
-- unquoteDef and unquoteDecl should also work in abstract blocks.

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality

abstract

  data D : Set where
    c : D

  f : D
  unquoteDef f = do
    qc ← quoteTC c  -- Previously, there was a complaint here about c.
    defineFun f (clause [] [] qc ∷ [])

  unquoteDecl g = do
    ty ← quoteTC D
    _  ← declareDef (arg (arg-info visible relevant) g) ty
    qc ← quoteTC c
    defineFun g (clause [] [] qc ∷ [])

test : f ≡ g
test = refl

-- Expected error:

-- f !=< g of type D
-- when checking that the expression refl has type f ≡ g

max_forks_repo_name: shlevy/agda


text:
-- Andreas, 2019-10-21, issue #4049
-- reported and test case by andy-morris

open import Agda.Builtin.Size

data A : Size → Set
B = A

data A where
  a : ∀ i → B i

-- WAS (2.6.0): internal error in Polarity.hs

-- Should succeed.


text:
module SystemF.BigStep.Types where

open import Prelude
open import Data.List as List

-- types are indexed by the number of open tvars
infixl 10 _⇒_
data Type (n : ℕ) : Set where
  Unit : Type n
  ν    : (i : Fin n) → Type n
  _⇒_  : Type n → Type n → Type n
  ∀'   : Type (suc n) → Type n

open import Data.Fin.Substitution
open import Data.Vec hiding (_∈_; map)

module App {T} (l : Lift T Type )where

  open Lift l hiding (var)
  _/_  : ∀ {m n} → Type m → Sub T m n → Type n
  Unit / s = Unit
  ν i / s = lift (lookup i s)
  (a ⇒ b) / s = (a / s) ⇒ (b / s)
  ∀' x / s = ∀' (x / (s ↑))

  open Application (record { _/_ = _/_ }) using (_/✶_)

  open import Data.Star

  Unit-/✶-↑✶ : ∀ k {m n} (ρs : Subs T m n) → Unit /✶ ρs ↑✶ k ≡ Unit
  Unit-/✶-↑✶ k ε = refl
  Unit-/✶-↑✶ k (x ◅ ρs) = cong₂ _/_ (Unit-/✶-↑✶ k ρs) refl

  ∀-/✶-↑✶ : ∀ k {m n t} (ρs : Subs T m n) →
            ∀' t /✶ ρs ↑✶ k ≡ ∀' (t /✶ ρs ↑✶ suc k)
  ∀-/✶-↑✶ k ε        = refl
  ∀-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (∀-/✶-↑✶ k ρs) refl

  ⇒-/✶-↑✶ : ∀ k {m n t₁ t₂} (ρs : Subs T m n) →
            t₁ ⇒ t₂ /✶ ρs ↑✶ k ≡ (t₁ /✶ ρs ↑✶ k) ⇒ (t₂ /✶ ρs ↑✶ k)
  ⇒-/✶-↑✶ k ε        = refl
  ⇒-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (⇒-/✶-↑✶ k ρs) refl

tmSubst : TermSubst Type
tmSubst = record { var = ν; app = App._/_ }

open TermSubst tmSubst hiding (var; subst) public

-- typing context
Ctx : ℕ → Set
Ctx n = List (Type n)

_+tm_ : ∀ {n} → Ctx n → Type n → Ctx n
Γ +tm a = a ∷ Γ

Var : ∀ {n} → Ctx n → Type n → Set
Var Γ a = a ∈ Γ
  where
    open import Data.List.Any
    open Membership-≡

infixl 30 _ctx/_
_ctx/_ : ∀ {n m} → Ctx n → Sub Type n m → Ctx m
Γ ctx/ ρ = List.map (flip _/_ ρ) Γ

_+ty  : ∀ {n} → Ctx n → Ctx (suc n)
Γ +ty = Γ ctx/ wk

module Lemmas where

  open import Data.Fin.Substitution.Lemmas

  tyLemmas : TermLemmas Type
  tyLemmas = record
    { termSubst = tmSubst
    ; app-var   = refl
    ; /✶-↑✶     = Lemma./✶-↑✶
    }
    where
    module Lemma {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} where

      open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
      open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

      /✶-↑✶ : ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) →
              (∀ k x → ν x /✶₁ ρs₁ ↑✶₁ k ≡ ν x /✶₂ ρs₂ ↑✶₂ k) →
              ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k
      /✶-↑✶ ρs₁ ρs₂ hyp k Unit =
        begin _ ≡⟨ App.Unit-/✶-↑✶ _ k ρs₁ ⟩ Unit ≡⟨ sym $ App.Unit-/✶-↑✶ _ k ρs₂ ⟩ _ ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (ν i) = hyp k i
      /✶-↑✶ ρs₁ ρs₂ hyp k (a ⇒ b) = begin
        _ ≡⟨ App.⇒-/✶-↑✶ _ k ρs₁ ⟩
        (a /✶₁ ρs₁ ↑✶₁ k) ⇒ (b /✶₁ ρs₁ ↑✶₁ k) ≡⟨ cong₂ _⇒_ (/✶-↑✶ ρs₁ ρs₂ hyp k a)
                                                           ((/✶-↑✶ ρs₁ ρs₂ hyp k b)) ⟩
        (a /✶₂ ρs₂ ↑✶₂ k) ⇒ (b /✶₂ ρs₂ ↑✶₂ k) ≡⟨ sym $ App.⇒-/✶-↑✶ _ k ρs₂ ⟩
        _ ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (∀' x) = begin
        _ ≡⟨ App.∀-/✶-↑✶ _ k ρs₁ ⟩
          ∀' (x /✶₁ ρs₁ ↑✶₁ (suc k)) ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) x) ⟩
        ∀' (x /✶₂ ρs₂ ↑✶₂ (suc k)) ≡⟨ sym $ App.∀-/✶-↑✶ _ k ρs₂ ⟩
        _ ∎

  open TermLemmas tyLemmas public hiding (var)

module CtxLemmas where

  open import Data.List.Properties as ListProp using ()
  open import Function as Fun

  -- weakening followed by sub disappears on contexts
  ctx/-wk-sub≡id : ∀ {n} (Γ : Ctx n) a → (Γ ctx/ wk) ctx/ (sub a) ≡ Γ
  ctx/-wk-sub≡id Γ a = begin
    _ ≡⟨ sym (ListProp.map-compose Γ) ⟩
    map (λ x → x / wk / (sub a)) Γ ≡⟨ ListProp.map-cong Lemmas.wk-sub-vanishes Γ ⟩
    map Fun.id Γ ≡⟨ ListProp.map-id Γ ⟩
    _ ∎

  -- weakening commutes with other substitutions on contexts
  ctx/-wk-comm : ∀ {n m} (Γ : Ctx n) (ρ : Sub Type n m) → (Γ ctx/ ρ) ctx/ wk ≡ Γ ctx/ wk ctx/ (ρ ↑)
  ctx/-wk-comm Γ ρ = begin
    _ ≡⟨ sym $ ListProp.map-compose Γ ⟩
    map (λ x → x / ρ / wk) Γ ≡⟨ ListProp.map-cong Lemmas.wk-commutes Γ ⟩
    map (λ x → x / wk / ρ ↑) Γ ≡⟨ ListProp.map-compose Γ ⟩
    _ ∎


text:
module Tactic.Nat.Auto.Lemmas where

open import Prelude
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Container.Bag
open import Prelude.Nat.Properties

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

prod++ : (xs ys : List Nat) → productR (xs ++ ys) ≡ productR xs * productR ys
prod++ [] ys = sym (add-zero-r (productR ys))
prod++ (x ∷ xs) ys rewrite prod++ xs ys = mul-assoc x _ _

private
  shuffle₁ : ∀ a b c d → a + ((b + c) + d) ≡ b + c + (a + d)
  shuffle₁ a b c d rewrite add-assoc a (b + c) d
                         | add-commute a (b + c)
                         | add-assoc (b + c) a d
                         = refl

  shuffle₂ : ∀ a b c d → a + b + (c + d) ≡ a + c + (b + d)
  shuffle₂ a b c d rewrite add-assoc (a + b) c d
                         | sym (add-assoc a b c)
                         | add-commute b c
                         | add-assoc a c b
                         | add-assoc (a + c) b d
                         = refl

  shuffle₃ : ∀ a b c d → (a * b) * (c * d) ≡ (a * c) * (b * d)
  shuffle₃ a b c d rewrite mul-assoc (a * b) c d
                         | sym (mul-assoc a b c)
                         | mul-commute b c
                         | mul-assoc a c b
                         | mul-assoc (a * c) b d = refl

  shuffle₄ : ∀ a b c d → a * (b * c * d) ≡ b * c * (a * d)
  shuffle₄ a b c d rewrite mul-assoc a (b * c) d
                         | mul-commute a (b * c)
                         | mul-assoc (b * c) a d
                         = refl

module _ {Atom : Set} {{_ : Ord Atom}} where
  ⟨+⟩-sound : ∀ v₁ v₂ (ρ : Env Atom) → ⟦ v₁ +nf v₂ ⟧n ρ ≡ ⟦ v₁ ⟧n ρ + ⟦ v₂ ⟧n ρ
  ⟨+⟩-sound [] []               ρ = refl
  ⟨+⟩-sound [] (_ ∷ _)          ρ = refl
  ⟨+⟩-sound (t ∷ v₁)  []        ρ = sym (add-zero-r _)
  ⟨+⟩-sound ((i , t₁) ∷ v₁) ((j , t₂) ∷ v₂) ρ with compare t₁ t₂
  ... | less _ rewrite ⟨+⟩-sound v₁ ((j , t₂) ∷ v₂) ρ
                     = add-assoc (i * productR (map ρ t₁)) _ _
  ... | equal eq rewrite eq | ⟨+⟩-sound v₁ v₂ ρ
                       | mul-distr-r i j (productR (map ρ t₂))
                       = shuffle₂ (⟦ i , t₂ ⟧t ρ) (⟦ j , t₂ ⟧t ρ) _ _
  ... | greater _ rewrite ⟨+⟩-sound ((i , t₁) ∷ v₁) v₂ ρ
                        = shuffle₁ (⟦ j , t₂ ⟧t ρ) (⟦ i , t₁ ⟧t ρ) _ _

  map-merge : ∀ x y (ρ : Env Atom) → productR (map ρ (merge x y)) ≡ productR (map ρ x) * productR (map ρ y)
  map-merge [] [] ρ = refl
  map-merge [] (x ∷ xs) ρ = sym (add-zero-r (productR (ρ x ∷ map ρ xs)))
  map-merge (x ∷ xs) [] ρ = sym (mul-one-r _)
  map-merge (x ∷ xs) (y ∷ ys) ρ with x <? y
  ... | true  rewrite map-merge xs (y ∷ ys) ρ = mul-assoc (ρ x) _ _
  ... | false rewrite map-merge (x ∷ xs) ys ρ = shuffle₄ (ρ y) (ρ x) _ _

  mulTm-sound : ∀ t t′ (ρ : Env Atom) →
                  ⟦ mulTm t t′ ⟧t ρ ≡ ⟦ t ⟧t ρ * ⟦ t′ ⟧t ρ
  mulTm-sound (a , x) (b , y) ρ rewrite map-merge x y ρ
                                        = shuffle₃ a b _ _

  mulTmDistr : ∀ t v (ρ : Env Atom) → ⟦ map (mulTm t) v ⟧n ρ ≡ ⟦ t ⟧t ρ * ⟦ v ⟧n ρ
  mulTmDistr t [] ρ = sym (mul-zero-r (⟦ t ⟧t ρ))
  mulTmDistr t (t′ ∷ v) ρ =
    ⟦ mulTm t t′ ⟧t ρ + ⟦ map (mulTm t) v ⟧n ρ
      ≡⟨ cong₂ _+_ (mulTm-sound t t′ ρ) (mulTmDistr t v ρ) ⟩
    ⟦ t ⟧t ρ * ⟦ t′ ⟧t ρ + ⟦ t ⟧t ρ * ⟦ v ⟧n ρ
      ≡⟨ mul-distr-l (⟦ t ⟧t ρ) _ _ ⟩ʳ
    ⟦ t ⟧t ρ * ⟦ t′ ∷ v ⟧n ρ ∎

  sort-sound : ∀ xs ρ → ⟦ nf-sort xs ⟧n ρ ≡ ⟦ xs ⟧n ρ
  sort-sound [] ρ = refl
  sort-sound (x ∷ xs) ρ rewrite ⟨+⟩-sound [ x ] (nf-sort xs) ρ
                              | sort-sound xs ρ
                              | add-zero-r (⟦ x ⟧t ρ) = refl

  ⟨*⟩-sound : ∀ v₁ v₂ (ρ : Env Atom) → ⟦ v₁ *nf v₂ ⟧n ρ ≡ ⟦ v₁ ⟧n ρ * ⟦ v₂ ⟧n ρ
  ⟨*⟩-sound [] v₂ ρ = refl
  ⟨*⟩-sound (t ∷ v₁) v₂ ρ =
    ⟦ nf-sort (map (mulTm t) v₂) +nf (v₁ *nf v₂) ⟧n ρ
      ≡⟨ ⟨+⟩-sound (nf-sort (map (mulTm t) v₂)) (v₁ *nf v₂) ρ ⟩
    ⟦ nf-sort (map (mulTm t) v₂) ⟧n ρ + ⟦ v₁ *nf v₂ ⟧n ρ
      ≡⟨ cong (flip _+_ (⟦ v₁ *nf v₂ ⟧n ρ)) (sort-sound (map (mulTm t) v₂) ρ) ⟩
    ⟦ map (mulTm t) v₂ ⟧n ρ + ⟦ v₁ *nf v₂ ⟧n ρ
      ≡⟨ cong (_+_ (⟦ map (mulTm t) v₂ ⟧n ρ)) (⟨*⟩-sound v₁ v₂ ρ) ⟩
    ⟦ map (mulTm t) v₂ ⟧n ρ + ⟦ v₁ ⟧n ρ * ⟦ v₂ ⟧n ρ
      ≡⟨ cong (flip _+_ (⟦ v₁ ⟧n ρ * ⟦ v₂ ⟧n ρ)) (mulTmDistr t v₂ ρ) ⟩
    ⟦ t ⟧t ρ * ⟦ v₂ ⟧n ρ + ⟦ v₁ ⟧n ρ * ⟦ v₂ ⟧n ρ
      ≡⟨ mul-distr-r (⟦ t ⟧t ρ) _ _ ⟩ʳ
    ⟦ t ∷ v₁ ⟧n ρ * ⟦ v₂ ⟧n ρ ∎

  sound : ∀ e (ρ : Env Atom) → ⟦ e ⟧e ρ ≡ ⟦ norm e ⟧n ρ
  sound (var x) ρ = mul-one-r (ρ x) ʳ⟨≡⟩ add-zero-r _ ʳ⟨≡⟩ʳ add-zero-r _
  sound (lit 0) ρ = refl
  sound (lit (suc n)) ρ rewrite mul-one-r n
                              | add-commute n 1
                              = sym (add-zero-r _)
  sound (e ⟨+⟩ e₁) ρ =
    ⟦ e ⟧e ρ + ⟦ e₁ ⟧e ρ
      ≡⟨ cong₂ _+_ (sound e ρ) (sound e₁ ρ) ⟩
    ⟦ norm e ⟧n ρ + ⟦ norm e₁ ⟧n ρ
      ≡⟨ ⟨+⟩-sound (norm e) (norm e₁) ρ ⟩ʳ
    ⟦ norm e +nf norm e₁ ⟧n ρ ∎
  sound (e ⟨*⟩ e₁) ρ =
    ⟦ e ⟧e ρ * ⟦ e₁ ⟧e ρ
      ≡⟨ cong₂ _*_ (sound e ρ) (sound e₁ ρ) ⟩
    ⟦ norm e ⟧n ρ * ⟦ norm e₁ ⟧n ρ
      ≡⟨ ⟨*⟩-sound (norm e) (norm e₁) ρ ⟩ʳ
    ⟦ norm e *nf norm e₁ ⟧n ρ ∎

  module _ (ρ₁ ρ₂ : Env Atom) (eq : ∀ x → ρ₁ x ≡ ρ₂ x) where
    private
      lem-eval-env-a : ∀ a → productR (map ρ₁ a) ≡ productR (map ρ₂ a)
      lem-eval-env-a []       = refl
      lem-eval-env-a (x ∷ xs) = _*_ $≡ eq x *≡ lem-eval-env-a xs

      lem-eval-env-t : ∀ t → ⟦ t ⟧t ρ₁ ≡ ⟦ t ⟧t ρ₂
      lem-eval-env-t (k , a) = _*_ k $≡ lem-eval-env-a a

    lem-eval-env : ∀ n → ⟦ n ⟧n ρ₁ ≡ ⟦ n ⟧n ρ₂
    lem-eval-env [] = refl
    lem-eval-env (x ∷ n) = _+_ $≡ lem-eval-env-t x *≡ lem-eval-env n

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text: postulate A : Set


text:
module Rec1 where

  import Rec2

  y : ℕ
  y = x


text:
module plfa-code.Naturals where

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

{-# BUILTIN NATURAL ℕ #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

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

_ : 2 + 3 ≡ 5
_ = refl

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

_^_ : ℕ → ℕ → ℕ
n ^ zero    = suc zero
n ^ (suc m) = n * (n ^ m)

_ : 3 ^ 4 ≡ 81
_ =
  begin
    3 ^ 4
  ≡⟨⟩
    3 * (3 ^ 3)
  ≡⟨⟩
    3 * (3 * (3 ^ 2))
  ≡⟨⟩
    3 * (3 * (3 * (3 ^ 1)))
  ≡⟨⟩
    3 * (3 * (3 * (3 * (3 ^ 0))))
  ≡⟨⟩
    3 * (3 * (3 * (3 * 1)))
  ≡⟨⟩
    81
  ∎

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

_ =
  begin
     3 ∸ 2
  ≡⟨⟩
     2 ∸ 1
  ≡⟨⟩
     1 ∸ 0
  ≡⟨⟩
     1
  ∎

_ =
  begin
     2 ∸ 3
  ≡⟨⟩
     1 ∸ 2
  ≡⟨⟩
     0 ∸ 1
  ≡⟨⟩
     0
  ∎

infixl 6 _+_ _∸_
infixl 7 _*_

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil = x1 nil
inc (x0 t) = x1 t
inc (x1 t) = x0 (inc t)

_ : inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
_ = refl

_ : inc (x0 nil) ≡ x1 nil
_ = refl

_ : inc (x1 nil) ≡ x0 x1 nil
_ = refl

_ : inc (x0 x1 nil) ≡ x1 x1 nil
_ = refl

_ : inc (x1 x1 nil) ≡ x0 x0 x1 nil
_ = refl

to   : ℕ → Bin
to 0   = x0 nil
to (suc n) = inc (to n)

from : Bin → ℕ
from nil      = 0
from (x0 t)   = (from t) * 2
from (x1 t)   = (from t) * 2 + 1

_ : to 0 ≡ x0 nil
_ = refl

_ : to 1 ≡ x1 nil
_ = refl

_ : to 2 ≡ x0 x1 nil
_ = refl

_ : to 3 ≡ x1 x1 nil
_ = refl

_ : to 4 ≡ x0 x0 x1 nil
_ = refl

_ : 0 ≡ from (x0 nil)
_ = refl

_ : 1 ≡ from (x1 nil)
_ = refl

_ : 2 ≡ from (x0 x1 nil)
_ = refl

_ : 3 ≡ from (x1 x1 nil)
_ = refl

_ : 4 ≡ from (x0 x0 x1 nil)
_ = refl

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


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

module Definition.Typed.Consequences.Syntactic where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Escape
open import Definition.LogicalRelation.Fundamental
open import Definition.Typed.Consequences.Injectivity

open import Tools.Product

-- Syntactic validity of type equality.
syntacticEq : ∀ {A B Γ} → Γ ⊢ A ≡ B → Γ ⊢ A × Γ ⊢ B
syntacticEq A≡B with fundamentalEq A≡B
syntacticEq A≡B | [Γ] , [A] , [B] , [A≡B] =
  escapeᵛ [Γ] [A] , escapeᵛ [Γ] [B]

-- Syntactic validity of terms.
syntacticTerm : ∀ {t A Γ} → Γ ⊢ t ∷ A → Γ ⊢ A
syntacticTerm t with fundamentalTerm t
syntacticTerm t | [Γ] , [A] , [t] = escapeᵛ [Γ] [A]

-- Syntactic validity of term equality.
syntacticEqTerm : ∀ {t u A Γ} → Γ ⊢ t ≡ u ∷ A → Γ ⊢ A × (Γ ⊢ t ∷ A × Γ ⊢ u ∷ A)
syntacticEqTerm t≡u with fundamentalTermEq t≡u
syntacticEqTerm t≡u | [Γ] , modelsTermEq [A] [t] [u] [t≡u] =
  escapeᵛ [Γ] [A] , escapeTermᵛ [Γ] [A] [t] , escapeTermᵛ [Γ] [A] [u]

-- Syntactic validity of type reductions.
syntacticRed : ∀ {A B Γ} → Γ ⊢ A ⇒* B → Γ ⊢ A × Γ ⊢ B
syntacticRed D with fundamentalEq (subset* D)
syntacticRed D | [Γ] , [A] , [B] , [A≡B] =
  escapeᵛ [Γ] [A] , escapeᵛ [Γ] [B]

-- Syntactic validity of term reductions.
syntacticRedTerm : ∀ {t u A Γ} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ A × (Γ ⊢ t ∷ A × Γ ⊢ u ∷ A)
syntacticRedTerm d with fundamentalTermEq (subset*Term d)
syntacticRedTerm d | [Γ] , modelsTermEq [A] [t] [u] [t≡u] =
  escapeᵛ [Γ] [A] , escapeTermᵛ [Γ] [A] [t] , escapeTermᵛ [Γ] [A] [u]

-- Syntactic validity of Π-types.
syntacticΠ : ∀ {Γ F G} → Γ ⊢ Π F ▹ G → Γ ⊢ F × Γ ∙ F ⊢ G
syntacticΠ ΠFG with injectivity (refl ΠFG)
syntacticΠ ΠFG | F≡F , G≡G = proj₁ (syntacticEq F≡F) , proj₁ (syntacticEq G≡G)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

module Categories.Morphism.Universal where

open import Level
open import Categories.Category
open import Categories.Category.Construction.Comma
open import Categories.Functor
open import Categories.Object.Initial

record UniversalMorphism {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
                         (X : Category.Obj C) (F : Functor D C) : Set (e ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  X↙F : Category _ _ _
  X↙F = X ↙ F

  private
    module X↙F = Category X↙F

  field
    initial : Initial X↙F

  module initial = Initial initial
  open initial public

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:
{-# OPTIONS --without-K --safe #-}
module Util.HoTT.HLevel.Core where

open import Data.Nat using (_+_)
open import Level using (Lift ; lift ; lower)

open import Util.Prelude
open import Util.Relation.Binary.LogicalEquivalence using (_↔_ ; forth ; back)
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; Σ-≡⁻ ; Σ-≡⁺∘Σ-≡⁻ ; trans-injectiveˡ )

private
  variable
    α β γ : Level
    A B C : Set α

IsContr : Set α → Set α
IsContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

IsProp : Set α → Set α
IsProp A = (x y : A) → x ≡ y

IsProp′ : Set α → Set α
IsProp′ A = (x y : A) → IsContr (x ≡ y)

IsProp→IsProp′ : IsProp A → IsProp′ A
IsProp→IsProp′ {A = A} A-prop x y = (A-prop x y) , canon
  where
    go : (p : x ≡ y) → trans p (A-prop y y) ≡ A-prop x y
    go refl = refl

    canon : (p : x ≡ y) → A-prop x y ≡ p
    canon refl = trans-injectiveˡ (A-prop y y) (go (A-prop y y))

IsProp′→IsProp : IsProp′ A → IsProp A
IsProp′→IsProp A-prop x y = proj₁ (A-prop x y)

IsProp↔IsProp′ : IsProp A ↔ IsProp′ A
IsProp↔IsProp′ .forth = IsProp→IsProp′
IsProp↔IsProp′ .back = IsProp′→IsProp

IsSet : Set α → Set α
IsSet A = {x y : A} → IsProp (x ≡ y)

IsOfHLevel : ℕ → Set α → Set α
IsOfHLevel 0 A = IsContr A
IsOfHLevel 1 A = IsProp A
IsOfHLevel (suc (suc n)) A = {x y : A} → IsOfHLevel (suc n) (x ≡ y)

IsOfHLevel′ : ℕ → Set α → Set α
IsOfHLevel′ zero A = IsContr A
IsOfHLevel′ (suc n) A = ∀ {x y : A} → IsOfHLevel′ n (x ≡ y)

IsOfHLevel′→IsOfHLevel : ∀ n → IsOfHLevel′ n A → IsOfHLevel n A
IsOfHLevel′→IsOfHLevel zero A-contr = A-contr
IsOfHLevel′→IsOfHLevel (suc zero) A-prop = IsProp′→IsProp λ _ _ → A-prop
IsOfHLevel′→IsOfHLevel (suc (suc n)) A-level
  = IsOfHLevel′→IsOfHLevel (suc n) A-level

IsOfHLevel→IsOfHLevel′ : ∀ n → IsOfHLevel n A → IsOfHLevel′ n A
IsOfHLevel→IsOfHLevel′ zero A-contr = A-contr
IsOfHLevel→IsOfHLevel′ (suc zero) A-prop = IsProp→IsProp′ A-prop _ _
IsOfHLevel→IsOfHLevel′ (suc (suc n)) A-level
  = IsOfHLevel→IsOfHLevel′ (suc n) A-level

IsOfHLevel↔IsOfHLevel′ : ∀ n → IsOfHLevel n A ↔ IsOfHLevel′ n A
IsOfHLevel↔IsOfHLevel′ n .forth = IsOfHLevel→IsOfHLevel′ n
IsOfHLevel↔IsOfHLevel′ n .back = IsOfHLevel′→IsOfHLevel n

IsContr→IsProp : IsContr A → IsProp A
IsContr→IsProp (c , c-canon) x y = trans (sym (c-canon x)) (c-canon y)

IsOfHLevel-suc : ∀ n → IsOfHLevel n A → IsOfHLevel (suc n) A
IsOfHLevel-suc 0 A-contr = IsContr→IsProp A-contr
IsOfHLevel-suc 1 A-prop = IsOfHLevel-suc 0 (IsProp→IsProp′ A-prop _ _)
IsOfHLevel-suc (suc (suc n)) A-level-n = IsOfHLevel-suc (suc n) A-level-n

IsOfHLevel-suc-n : ∀ n m → IsOfHLevel n A → IsOfHLevel (m + n) A
IsOfHLevel-suc-n {A = A} n zero A-level = A-level
IsOfHLevel-suc-n n (suc m) A-level
  = IsOfHLevel-suc (m + n) (IsOfHLevel-suc-n n m A-level)

IsProp→IsSet : IsProp A → IsSet A
IsProp→IsSet = IsOfHLevel-suc 1

IsContr→IsSet : IsContr A → IsSet A
IsContr→IsSet = IsOfHLevel-suc-n 0 2

record HLevel α n : Set (lsuc α) where
  constructor HLevel⁺
  field
    type : Set α
    level : IsOfHLevel n type

open HLevel public

HContr : ∀ α → Set (lsuc α)
HContr α = HLevel α 0

HProp : ∀ α → Set (lsuc α)
HProp α = HLevel α 1

HSet : ∀ α → Set (lsuc α)
HSet α = HLevel α 2

HLevel-suc : ∀ {α n} → HLevel α n → HLevel α (suc n)
HLevel-suc (HLevel⁺ A A-level) = HLevel⁺ A (IsOfHLevel-suc _ A-level)

⊤-IsContr : IsContr ⊤
⊤-IsContr = _ , λ _ → refl

⊤-IsProp : IsProp ⊤
⊤-IsProp = IsOfHLevel-suc 0 ⊤-IsContr

⊥-IsProp : IsProp ⊥
⊥-IsProp ()

×-IsProp : IsProp A → IsProp B → IsProp (A × B)
×-IsProp A-prop B-prop (x , y) (x′ , y′) = cong₂ _,_ (A-prop _ _) (B-prop _ _)

Lift-IsProp : IsProp A → IsProp (Lift α A)
Lift-IsProp A-prop (lift x) (lift y) = cong lift (A-prop _ _)

⊤-HProp : HProp 0ℓ
⊤-HProp = HLevel⁺ ⊤ ⊤-IsProp

⊥-HProp : HProp 0ℓ
⊥-HProp = HLevel⁺ ⊥ ⊥-IsProp

_×-HProp_ : HProp α → HProp β → HProp (α ⊔ℓ β)
A ×-HProp B = HLevel⁺ (A .type × B .type) (×-IsProp (A .level) (B .level))

Lift-HProp : ∀ α → HProp β → HProp (α ⊔ℓ β)
Lift-HProp α (HLevel⁺ A A-prop) = HLevel⁺ (Lift α A) (Lift-IsProp A-prop)

⊤-IsSet : IsSet ⊤
⊤-IsSet = IsOfHLevel-suc 1 ⊤-IsProp

⊥-IsSet : IsSet ⊥
⊥-IsSet = IsOfHLevel-suc 1 ⊥-IsProp

Σ-IsSet : {A : Set α} {B : A → Set β}
  → IsSet A
  → (∀ a → IsSet (B a))
  → IsSet (Σ A B)
Σ-IsSet A-set B-set p q
  = trans (sym (Σ-≡⁺∘Σ-≡⁻ p))
      (sym (trans (sym (Σ-≡⁺∘Σ-≡⁻ q))
      (cong Σ-≡⁺ (Σ-≡⁺ (A-set _ _ , B-set _ _ _)))))

×-IsSet : IsSet A → IsSet B → IsSet (A × B)
×-IsSet A-set B-set = Σ-IsSet A-set (λ _ → B-set)

Lift-IsSet : IsSet A → IsSet (Lift α A)
Lift-IsSet A-set p q
  = trans (sym (Lift-≡⁺∘Lift-≡⁻ p))
      (sym (trans (sym (Lift-≡⁺∘Lift-≡⁻ q)) (cong Lift-≡⁺ (A-set _ _))))
  where
    Lift-≡⁻ : {x y : Lift α A} → x ≡ y → lower x ≡ lower y
    Lift-≡⁻ refl = refl

    Lift-≡⁺ : {x y : Lift α A} → lower x ≡ lower y → x ≡ y
    Lift-≡⁺ refl = refl

    Lift-≡⁻∘Lift-≡⁺ : {x y : Lift α A} (p : lower x ≡ lower y)
      → Lift-≡⁻ {α = α} (Lift-≡⁺ p) ≡ p
    Lift-≡⁻∘Lift-≡⁺ refl = refl

    Lift-≡⁺∘Lift-≡⁻ : {x y : Lift α A} (p : x ≡ y)
      → Lift-≡⁺ {α = α} (Lift-≡⁻ p) ≡ p
    Lift-≡⁺∘Lift-≡⁻ refl = refl

⊤-HSet : HSet 0ℓ
⊤-HSet = HLevel⁺ ⊤ ⊤-IsSet

⊥-HSet : HSet 0ℓ
⊥-HSet = HLevel⁺ ⊥ ⊥-IsSet

Σ-HSet : (A : HSet α) (B : A .type → HSet β) → HSet (α ⊔ℓ β)
Σ-HSet A B
  = HLevel⁺ (Σ (A .type) λ a → B a .type) (Σ-IsSet (A .level) (λ a → B a .level))

_×-HSet_ : HSet α → HSet β → HSet (α ⊔ℓ β)
A ×-HSet B = HLevel⁺ (A .type × B .type) (×-IsSet (A .level) (B .level))

Lift-HSet : ∀ α → HSet β → HSet (α ⊔ℓ β)
Lift-HSet α (HLevel⁺ B B-set) = HLevel⁺ (Lift α B) (Lift-IsSet B-set)

IsProp∧Pointed→IsContr : IsProp A → (a : A) → IsContr A
IsProp∧Pointed→IsContr A-prop a = a , λ b → A-prop a b

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

module Data.Binary.Subtraction where

open import Data.Binary.Definition
open import Data.Nat

double : 𝔹 → 𝔹
double 0ᵇ      = 0ᵇ
double (1ᵇ xs) = 2ᵇ double xs
double (2ᵇ xs) = 2ᵇ 1ᵇ xs

dec : 𝔹 → 𝔹
dec 0ᵇ = 0ᵇ
dec (2ᵇ xs) = 1ᵇ xs
dec (1ᵇ xs) = double xs

ones : ℕ → 𝔹 → 𝔹
ones zero    xs = xs
ones (suc n) xs = ones n (1ᵇ xs)

fromZ₁ : ℕ → 𝔹 → 𝔹
fromZ₁ n 0ᵇ      = 0ᵇ
fromZ₁ n (1ᵇ xs) = 2ᵇ ones n (double xs)
fromZ₁ n (2ᵇ xs) = 2ᵇ ones (suc n) xs

mutual
  compl₁′ : ℕ → 𝔹 → 𝔹 → 𝔹
  compl₁′ n 0ᵇ      _       = 2ᵇ ones n 0ᵇ
  compl₁′ n (1ᵇ xs) 0ᵇ      = fromZ₁ (suc n) xs
  compl₁′ n (2ᵇ xs) 0ᵇ      = 2ᵇ ones n (double xs)
  compl₁′ n (1ᵇ xs) (1ᵇ ys) = 2ᵇ ones n (compl₁′ 0 xs ys)
  compl₁′ n (1ᵇ xs) (2ᵇ ys) = compl₁′ (suc n) xs ys
  compl₁′ n (2ᵇ xs) (1ᵇ ys) = compl₂′ (suc n) xs ys
  compl₁′ n (2ᵇ xs) (2ᵇ ys) = 2ᵇ ones n (compl₁′ 0 xs ys)

  compl₂′ : ℕ → 𝔹 → 𝔹 → 𝔹
  compl₂′ n xs      0ᵇ      = fromZ₁ n xs
  compl₂′ n 0ᵇ      _       = 0ᵇ
  compl₂′ n (1ᵇ xs) (1ᵇ ys) = compl₂′ (suc n) xs ys
  compl₂′ n (1ᵇ xs) (2ᵇ ys) = 2ᵇ ones n (compl₁′ 0 xs ys)
  compl₂′ n (2ᵇ xs) (1ᵇ ys) = 2ᵇ ones n (compl₂′ 0 xs ys)
  compl₂′ n (2ᵇ xs) (2ᵇ ys) = compl₂′ (suc n) xs ys

mutual
  compl₁ : 𝔹 → 𝔹 → 𝔹
  compl₁ xs      0ᵇ      = dec xs
  compl₁ 0ᵇ      _       = 1ᵇ 0ᵇ
  compl₁ (1ᵇ xs) (1ᵇ ys) = 1ᵇ compl₁ xs ys
  compl₁ (1ᵇ xs) (2ᵇ ys) = compl₁′ zero xs ys
  compl₁ (2ᵇ xs) (1ᵇ ys) = compl₂′ zero xs ys
  compl₁ (2ᵇ xs) (2ᵇ ys) = 1ᵇ compl₁ xs ys

  compl₂ : 𝔹 → 𝔹 → 𝔹
  compl₂ 0ᵇ      _       = 0ᵇ
  compl₂ xs      0ᵇ      = xs
  compl₂ (1ᵇ xs) (1ᵇ ys) = compl₂′ zero xs ys
  compl₂ (1ᵇ xs) (2ᵇ ys) = 1ᵇ compl₁ xs ys
  compl₂ (2ᵇ xs) (1ᵇ ys) = 1ᵇ compl₂ xs ys
  compl₂ (2ᵇ xs) (2ᵇ ys) = compl₂′ zero xs ys

open import Data.Binary.Order
open import Data.Bool

infixl 6 _-_
_-_ : 𝔹 → 𝔹 → 𝔹
n - m = if n ≤ᴮ m then 0ᵇ else compl₂ n m

open import Data.Binary.Testers
open import Path using (refl)

_ : test _-_ _∸_ 30
_ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Categories.Functor.Groupoid where

open import Level

open import Categories.Category
open import Categories.Category.Groupoid using (Groupoid; IsGroupoid)
open import Categories.Functor
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

-- functor respects groupoid inverse
module _ (GC : IsGroupoid C) (GD : IsGroupoid D) (F : Functor C D) where
  private
    module C = IsGroupoid GC
    module D = IsGroupoid GD
    open Functor F
    open D
    open HomReasoning
    open MR D

  F-resp-inv : ∀ {A B} (f : A C.⇒ B) → F₁ (f C.⁻¹) ≈ (F₁ f) ⁻¹
  F-resp-inv f = begin
    F₁ (f C.⁻¹)                      ≈⟨ introˡ D.iso.isoˡ ⟩
    ((F₁ f) ⁻¹ ∘ F₁ f) ∘ F₁ (f C.⁻¹) ≈˘⟨ pushʳ homomorphism ⟩
    (F₁ f) ⁻¹ ∘ F₁ (f C.∘ f C.⁻¹)    ≈⟨ elimʳ (F-resp-≈ C.iso.isoʳ ○ identity) ⟩
    (F₁ f) ⁻¹                        ∎

-- Nevertheless, create a |GrFunctor| that is typed over Groupoid instead of Category
GrFunctor : (A B : Groupoid o ℓ e) → Set _
GrFunctor A B = Functor (category A) (category B)
  where open Groupoid


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

module Data.Probability where

open import Prelude
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Data.Bits renaming (Bits to ℚ⁺; [] to 1ℚ; 0∷_ to lℚ; 1∷_ to rℚ)
open import Data.Bits.Equatable

open import Data.Bits.Fold

euclidian : ℕ → ℕ → ℕ → ℚ⁺
euclidian n m zero    = 1ℚ
euclidian n m (suc s) =
  if n ℕ.≡ᴮ m
  then 1ℚ
  else if n ℕ.<ᴮ m
  then lℚ (euclidian n (m ℕ.∸ (1 ℕ.+ n)) s)
  else rℚ (euclidian (n ℕ.∸ (1 ℕ.+ m)) m s)

normalise-suc : ℕ → ℕ → ℚ⁺
normalise-suc n m = euclidian n m (n ℕ.+ m)

data ℙ : Type where
  ℙ⁰ : ℙ
  ℙ¹ : ℙ
  ℙ∙ : ℚ⁺ → ℙ

unEu : ℚ⁺ → ℙ
unEu 1ℚ = ℙ¹
unEu (lℚ x) = ℙ∙ x
unEu (rℚ x) = ℙ¹ -- won't happen

_/suc_ : ℕ → ℕ → ℙ
zero  /suc d = ℙ⁰
suc n /suc d = unEu (normalise-suc n d)

_/_ : ℕ → ℕ → ℙ
n / zero = ℙ⁰
n / suc d = n /suc d

zer : (ℕ × ℕ) → (ℕ × ℕ)
zer (p , q) = p , suc p ℕ.+ q

one : (ℕ × ℕ) → (ℕ × ℕ)
one (p , q) = suc p ℕ.+ q , q

norm : (ℕ × ℕ) → ℕ × ℕ
norm (x , y) = suc x , suc y

prob : ℙ → (ℕ × ℕ)
prob ℙ⁰ = 0 , 1
prob ℙ¹ = 1 , 1
prob (ℙ∙ x) = norm (zer (foldr-bits zer one (0 , 0) x))

mul″ : ℙ → ℙ → ℙ
mul″ x y =
  let xn , xd = prob x
      yn , yd = prob y
  in (xn ℕ.* yn) / (xd ℕ.* yd)

-- e = prob (5 /suc 22)

nextFrac : ℚ⁺ → ℚ⁺
nextFrac 1ℚ = lℚ 1ℚ
nextFrac (lℚ x) = rℚ x
nextFrac (rℚ x) = lℚ (nextFrac x)

open import Data.List

fracs : ℕ → List ℙ
fracs n = ℙ⁰ ∷ ℙ¹ ∷ go n 1ℚ
  where
  go : ℕ → ℚ⁺ → List ℙ
  go zero    x = []
  go (suc n) x = ℙ∙ x ∷ go n (nextFrac x)

open import Data.List.Sugar using (liftA2)

-- mul′ : ℚ⁺ → ℚ⁺ → ℚ⁺
-- mul′ 1ℚ 1ℚ = lℚ (lℚ 1ℚ)
-- mul′ 1ℚ (lℚ ys) = {!!}
-- mul′ 1ℚ (rℚ ys) = {!!}
-- mul′ (lℚ xs) 1ℚ = {!!}
-- mul′ (lℚ xs) (lℚ ys) = {!!}
-- mul′ (lℚ xs) (rℚ ys) = {!!}
-- mul′ (rℚ xs) 1ℚ = {!!}
-- mul′ (rℚ xs) (lℚ ys) = {!!}
-- mul′ (rℚ xs) (rℚ ys) = {!!}

-- mul : ℙ → ℙ → ℙ
-- mul ℙ⁰ ys = ℙ⁰
-- mul ℙ¹ ys = ys
-- mul (ℙ∙ x) ℙ⁰ = ℙ⁰
-- mul xs ℙ¹ = xs
-- mul (ℙ∙ x) (ℙ∙ y) = ℙ∙ (mul′ x y)

-- testMul : ℕ → Type
-- testMul n = liftA2 mul xs xs ≡ liftA2 mul″ xs xs
--   where
--     xs : List ℙ
--     xs = fracs n

-- _ : testMul 5
-- _ = refl


text:
{-# OPTIONS --safe #-}
module Relation.Ternary.Separation.Construct.List {a} (A : Set a) where

open import Level
open import Data.Product
open import Data.List
open import Data.List.Properties using (++-isMonoid)
open import Data.List.Relation.Ternary.Interleaving.Propositional as I public
open import Data.List.Relation.Ternary.Interleaving.Properties
open import Data.List.Relation.Binary.Equality.Propositional
open import Data.List.Relation.Binary.Permutation.Inductive

open import Relation.Binary.PropositionalEquality as P hiding ([_])
open import Relation.Unary hiding (_∈_; _⊢_)
open import Relation.Ternary.Separation

private C = List A

instance separation : RawSep C
separation = record { _⊎_≣_ = Interleaving }

-- TODO add to stdlib
interleaving-assoc : ∀ {a b ab c abc : List A} →
          Interleaving a b ab → Interleaving ab c abc →
          ∃ λ bc → Interleaving a bc abc × Interleaving b c bc
interleaving-assoc l (consʳ r)         = let _ , p , q = interleaving-assoc l r in -, consʳ p , consʳ q
interleaving-assoc (consˡ l) (consˡ r) = let _ , p , q = interleaving-assoc l r in -, consˡ p , q
interleaving-assoc (consʳ l) (consˡ r) = let _ , p , q = interleaving-assoc l r in -, consʳ p , consˡ q
interleaving-assoc [] []               = [] , [] , []

instance list-has-sep : IsSep separation
list-has-sep = record
  { ⊎-comm = I.swap
  ; ⊎-assoc = interleaving-assoc
  }

instance list-is-unital : IsUnitalSep _ _
IsUnitalSep.isSep list-is-unital               = list-has-sep
IsUnitalSep.⊎-idˡ list-is-unital               = right (≡⇒≋ P.refl)
IsUnitalSep.⊎-id⁻ˡ list-is-unital []           = refl
IsUnitalSep.⊎-id⁻ˡ list-is-unital (refl ∷ʳ px) = cong (_ ∷_) (⊎-id⁻ˡ px)

instance list-has-concat : IsConcattative separation
IsConcattative._∙_ list-has-concat = _++_
IsConcattative.⊎-∙ₗ list-has-concat {Φₑ = []} ps = ps
IsConcattative.⊎-∙ₗ list-has-concat {Φₑ = x ∷ Φₑ} ps = consˡ (⊎-∙ₗ ps)

instance list-unitalsep : UnitalSep _
list-unitalsep = record
  { isUnitalSep = list-is-unital }

instance list-resource : MonoidalSep _
list-resource = record
  { sep = separation
  ; isSep = list-has-sep
  ; isUnitalSep   = list-is-unital
  ; isConcat      = list-has-concat
  ; monoid = ++-isMonoid }

instance list-positive : IsPositive separation
list-positive = record
  { ⊎-εˡ = λ where [] → refl }


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

module quotient-groups where

import subgroups
open subgroups public

{- The left and right coset relation -}

left-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y : type-Group G) → UU (l1 ⊔ l2)
left-coset-relation G H x =
  fib ((mul-Group G x) ∘ (incl-group-Subgroup G H))

right-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y : type-Group G) → UU (l1 ⊔ l2)
right-coset-relation G H x =
  fib ((mul-Group' G x) ∘ (incl-group-Subgroup G H))

{- We show that the left coset relation is an equivalence relation -}

is-prop-left-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y : type-Group G) → is-prop (left-coset-relation G H x y)
is-prop-left-coset-relation G H x =
  is-prop-map-is-emb
    ( (mul-Group G x) ∘ (incl-group-Subgroup G H))
    ( is-emb-comp'
      ( mul-Group G x)
      ( incl-group-Subgroup G H)
      ( is-emb-is-equiv (mul-Group G x) (is-equiv-mul-Group G x))
      ( is-emb-incl-group-Subgroup G H))

is-reflexive-left-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x : type-Group G) → left-coset-relation G H x x
is-reflexive-left-coset-relation G H x =
  pair ( unit-group-Subgroup G H)
       ( right-unit-law-Group G x)

is-symmetric-left-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y : type-Group G) →
  left-coset-relation G H x y → left-coset-relation G H y x
is-symmetric-left-coset-relation G H x y (pair z p) =
  pair ( inv-group-Subgroup G H z)
       (  ap ( λ t → mul-Group G t
                      ( incl-group-Subgroup G H
                        ( inv-group-Subgroup G H z)))
             ( inv p) ∙
         ( ( is-associative-mul-Group G _ _ _) ∙
           ( ( ap (mul-Group G x) (right-inverse-law-Group G _)) ∙
             ( right-unit-law-Group G x))))

is-transitive-left-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y z : type-Group G) →
  left-coset-relation G H x y → left-coset-relation G H y z →
  left-coset-relation G H x z
is-transitive-left-coset-relation G H x y z (pair h1 p1) (pair h2 p2) =
  pair ( mul-group-Subgroup G H h1 h2)
       ( ( inv (is-associative-mul-Group G _ _ _)) ∙
         ( ( ap (λ t → mul-Group G t (incl-group-Subgroup G H h2)) p1) ∙ p2))

{- We show that the right coset relation is an equivalence relation -}

is-prop-right-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y : type-Group G) → is-prop (right-coset-relation G H x y)
is-prop-right-coset-relation G H x =
  is-prop-map-is-emb
    ( (mul-Group' G x) ∘ (incl-group-Subgroup G H))
    ( is-emb-comp'
      ( mul-Group' G x)
      ( incl-group-Subgroup G H)
      ( is-emb-is-equiv (mul-Group' G x) (is-equiv-mul-Group' G x))
      ( is-emb-incl-group-Subgroup G H))

is-reflexive-right-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x : type-Group G) → right-coset-relation G H x x
is-reflexive-right-coset-relation G H x =
  pair ( unit-group-Subgroup G H)
       ( left-unit-law-Group G x)

is-symmetric-right-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y : type-Group G) →
  right-coset-relation G H x y → right-coset-relation G H y x
is-symmetric-right-coset-relation G H x y (pair z p) =
  pair ( inv-group-Subgroup G H z)
       ( ( ap
           ( mul-Group G (incl-group-Subgroup G H (inv-group-Subgroup G H z)))
           ( inv p)) ∙
         ( ( inv (is-associative-mul-Group G _ _ _)) ∙
           ( ( ap (λ t → mul-Group G t x) (left-inverse-law-Group G _)) ∙
             ( left-unit-law-Group G x))))

is-transitive-right-coset-relation :
  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) →
  (x y z : type-Group G) →
  right-coset-relation G H x y → right-coset-relation G H y z →
  right-coset-relation G H x z
is-transitive-right-coset-relation G H x y z (pair h1 p1) (pair h2 p2) =
  pair ( mul-group-Subgroup G H h2 h1)
       ( ( is-associative-mul-Group G _ _ _) ∙
         ( ( ap (mul-Group G (incl-group-Subgroup G H h2)) p1) ∙ p2))

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
-- Andreas, May - July 2016, implementing postfix projections

module Issue1963 where

module Prod where

  record Σ (A : Set) (B : A → Set) : Set where
    field fst : A
          snd : B fst

  open Σ

  test : ∀{A} → A → Σ A λ _ → A
  test = λ where
    x .fst → x
    x .snd → x

module Stream where

  record Stream (A : Set) : Set where
    coinductive
    field head : A
          tail : Stream A

  open Stream

  repeat : ∀{A} (a : A) → Stream A
  repeat a .head = a
  repeat a. tail = repeat a

  zipWith : ∀{A B C} (f : A → B → C) (s : Stream A) (t : Stream B) → Stream C
  zipWith f s t .head = f (s .head) (t .head)
  zipWith f s t .tail = zipWith f (s .tail) (t .tail)

  module Fib (Nat : Set) (zero one : Nat) (plus : Nat → Nat → Nat) where

    {-# TERMINATING #-}
    fib : Stream Nat
    fib .head = zero
    fib .tail .head = one
    fib .tail .tail = zipWith plus fib (fib .tail)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Omniscience principles

-- https://ncatlab.org/nlab/show/principle+of+omniscience
-- http://math.fau.edu/lubarsky/Separating%20LLPO.pdf
-- https://arxiv.org/pdf/1804.05495.pdf
-- https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-revised.pdf
-- https://www.jaist.ac.jp/~t-nemoto/WMP.pdf
-- http://math.fau.edu/lubarsky/Separating%20LLPO.pdf

-- TODO
-- WKL: weak Koning's lemma
-- BE: Every real number in [0,1] has binary expansion
-- IVT: intermediate value theorem
-- BD-N
-- LLPOₙ

-- WKL <=> LLPO

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

module Constructive.Axiom where

-- agda-stdlib
open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Bool using (Bool; true; false)
open import Data.Empty using (⊥)
open import Data.Sum as Sum
open import Data.Product as Prod
open import Data.List using (List; []; _∷_; length)
open import Data.List.Relation.Binary.Prefix.Heterogeneous using (Prefix)
open import Data.Nat using (ℕ; _≤_; _<_; _+_; _*_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Function

-- agda-misc
open import Constructive.Common
open import TypeTheory.HoTT.Base using (isProp)

---------------------------------------------------------------------------
-- Axioms
-- -i indicates instance

-- Law of Excluded middle
-- LEM
EM : ∀ a → Set (lsuc a)
EM a = ∀ {A : Set a} → Dec⊎ A

-- Double negation elimination
DNE : ∀ a → Set (lsuc a)
DNE a = ∀ {A : Set a} → Stable A

-- Peirce's law
Peirce-i : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
Peirce-i A B = ((A → B) → A) → A

Peirce : ∀ a b → Set (lsuc (a ⊔ b))
Peirce a b = {A : Set a} {B : Set b} → Peirce-i A B

-- Material implication
MI-i : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
MI-i A B = (A → B) → ¬ A ⊎ B

MI : ∀ a b → Set (lsuc (a ⊔ b))
MI a b = {A : Set a} {B : Set b} → MI-i A B

-- De Morgan's laws
-- DML
DEM₁-i : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
DEM₁-i A B = ¬ (¬ A × ¬ B) → A ⊎ B

DEM₂-i : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
DEM₂-i A B = ¬ (¬ A ⊎ ¬ B) → A × B

DEM₃-i : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
DEM₃-i A B = ¬ (A × B) → ¬ A ⊎ ¬ B

DEM₁ : ∀ a b → Set (lsuc (a ⊔ b))
DEM₁ a b = {A : Set a} {B : Set b} → DEM₁-i A B

DEM₂ : ∀ a b → Set (lsuc (a ⊔ b))
DEM₂ a b = {A : Set a} {B : Set b} → DEM₂-i A B

DEM₃ : ∀ a b → Set (lsuc (a ⊔ b))
DEM₃ a b = {A : Set a} {B : Set b} → DEM₃-i A B

-- call/cc
Call/CC-i : ∀ {a} → Set a → Set a
Call/CC-i A = Peirce-i A ⊥

Call/CC : ∀ a → Set (lsuc a)
Call/CC a = ∀ {A : Set a} → Call/CC-i A

-- Gödel-Dummett logic
-- Dirk Gently's Principle (DGP)
DGP-i : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
DGP-i A B = (A → B) ⊎ (B → A)

DGP : ∀ a b → Set (lsuc (a ⊔ b))
DGP a b = {A : Set a} {B : Set b} → DGP-i A B

-- Weak excluded middle
-- https://ncatlab.org/nlab/show/weak+excluded+middle
-- WLEM WPEM
WEM-i : ∀ {a} → Set a → Set a
WEM-i A = Dec⊎ (¬ A)

WEM : ∀ a → Set (lsuc a)
WEM a = {A : Set a} → WEM-i A

-- Double-negation shift
-- if domain of P is finite this can be proved.
-- https://ncatlab.org/nlab/show/double-negation+shift
DNS-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
DNS-i P = (∀ x → ¬ ¬ P x) → ¬ ¬ (∀ x → P x)

DNS : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
DNS A p = {P : A → Set p} → DNS-i P

-- Independence-of-premise
IP : ∀ p q r → Set (lsuc (p ⊔ q ⊔ r))
IP p q r = ∀ {P : Set p} {Q : Set q} {R : Q → Set r} →
           Q → (P → Σ Q R) → (Σ Q λ x → (P → R x))

private
  toPred : ∀ {a} {A : Set a} → (A → Bool) → (A → Set)
  toPred P x = P x ≡ true

-- Searchable set
Searchable-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
Searchable-i P = DecU P → (∃ λ x₀ → P x₀ → ∀ x → P x)

Searchable : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Searchable A p = {P : A → Set p} → Searchable-i P

Searchable-Bool : ∀ {a} → Set a → Set a
Searchable-Bool A = Σ ((A → Bool) → A)
                      λ ε → (P : A → Bool) → P (ε P) ≡ true → (x : A) → P x ≡ true

-- The limited principle of omniscience
-- https://ncatlab.org/nlab/show/principle+of+omniscience
-- Omniscient type
LPO-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
LPO-i P = DecU P → ∃ P ⊎ ¬ ∃ P

LPO : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
LPO A p = {P : A → Set p} → LPO-i P

LPO-Bool-i : ∀ {a} {A : Set a} → (A → Bool) → Set a
LPO-Bool-i P = ∃ (toPred P) ⊎ ¬ ∃ (toPred P)

LPO-Bool : ∀ {a} → Set a → Set a
LPO-Bool A = (P : A → Bool) → LPO-Bool-i P

-- http://www.cs.bham.ac.uk/~mhe/papers/omniscient-2011-07-06.pdf
LPO-Bool-Alt-i : ∀ {a} {A : Set a} → (A → Bool) → Set a
LPO-Bool-Alt-i P = (∃ λ x → P x ≡ false) ⊎ (∀ x → P x ≡ true)

LPO-Bool-Alt : ∀ {a} → Set a → Set a
LPO-Bool-Alt A = (P : A → Bool) → LPO-Bool-Alt-i P

-- Weak limited principle of omniscience
-- https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-revised.pdf
-- http://math.fau.edu/lubarsky/Separating%20LLPO.pdf
-- ∀-PEM
WLPO-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
WLPO-i P = DecU P → (∀ x → P x) ⊎ ¬ (∀ x → P x)

WLPO : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
WLPO A p = {P : A → Set p} → WLPO-i P

-- Alternative form of WLPO
WLPO-Alt-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
WLPO-Alt-i P = DecU P → ¬ ∃ P ⊎ ¬ ¬ ∃ P

WLPO-Alt : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
WLPO-Alt A p = {P : A → Set p} → WLPO-Alt-i P

-- The lesser limited principle of omniscience
-- Σ⁰₁-DML
LLPO-i : ∀ {a p} {A : Set a} → (P Q : A → Set p) → Set (a ⊔ p)
LLPO-i P Q = DecU P → DecU Q → ¬ (∃ P × ∃ Q) → ¬ ∃ P ⊎ ¬ ∃ Q

LLPO : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
LLPO A p = {P Q : A → Set p} → LLPO-i P Q

LLPO-Alt-i : ∀ {a p} {A : Set a} → (P Q : A → Set p) → Set (a ⊔ p)
LLPO-Alt-i P Q = DecU P → DecU Q →
                 ¬ ¬ ((∀ x → P x) ⊎ (∀ x → Q x)) → (∀ x → P x) ⊎ (∀ x → Q x)

LLPO-Alt : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
LLPO-Alt A p = {P Q : A → Set p} → LLPO-Alt-i P Q

LLPO-Bool-i : ∀ {a} {A : Set a} → (P Q : A → Bool) → Set a
LLPO-Bool-i P Q = ¬ (∃ (toPred P) × ∃ (toPred Q)) → ¬ ∃ (toPred P) ⊎ ¬ ∃ (toPred Q)

LLPO-Bool : ∀ {a} → Set a → Set a
LLPO-Bool A = (P Q : A → Bool) → LLPO-Bool-i P Q

LLPO-ℕ : ∀ p → Set (lsuc p)
LLPO-ℕ p = {P : ℕ → Set p} → DecU P → (∀ m n → m ≢ n → P m ⊎ P n) →
           (∀ n → P (2 * n)) ⊎ (∀ n → P (1 + 2 * n))

-- Markov's principle
-- LPE
-- https://ncatlab.org/nlab/show/Markov%27s+principle
MP-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
MP-i P = DecU P → ¬ (∀ x → P x) → ∃ λ x → ¬ P x

MP : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
MP A p = {P : A → Set p} → MP-i P

-- Markov's rule
MR-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
MR-i P = DecU P → ¬ ¬ ∃ P → ∃ P

MR : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
MR A p = {P : A → Set p} → MR-i P

-- Weak Markov's principle
-- https://ncatlab.org/nlab/show/Markov%27s+principle
WMP-i : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ lsuc p)
WMP-i {p = p} {A = A} P =
  DecU P →
  ({Q : A → Set p} → DecU Q → ¬ ¬ ∃ Q ⊎ (¬ ¬ ∃ λ x → P x × ¬ Q x)) →
  ∃ P

WMP : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
WMP A p  = {P : A → Set p} → WMP-i P

WMP-Bool-i : ∀ {a} {A : Set a} → (A → Bool) → Set a
WMP-Bool-i {A = A} P =
  ((Q : A → Bool) →
    ¬ ¬ ∃ (λ x → Q x ≡ true) ⊎ (¬ ¬ ∃ λ x → P x ≡ true × Q x ≢ true)) →
  ∃ λ x → P x ≡ true

WMP-Bool : ∀ {a} (A : Set a) → Set a
WMP-Bool A = (P : A → Bool) → WMP-Bool-i P

-- Disjunctive Markov’s principle
MP⊎-i : ∀ {a p} {A : Set a} → (P Q : A → Set p) → Set (a ⊔ p)
MP⊎-i P Q = DecU P → DecU Q → ¬ (¬ ∃ P × ¬ ∃ Q) → ¬ ¬ ∃ P ⊎ ¬ ¬ ∃ Q

MP⊎ : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
MP⊎ A p = {P Q : A → Set p} → MP⊎-i P Q

MP⊎-Bool-i : ∀ {a} {A : Set a} → (P Q : A → Bool) → Set a
MP⊎-Bool-i P Q = ¬ (¬ ∃ (toPred P) × ¬ ∃ (toPred Q)) →
                 ¬ ¬ ∃ (toPred P) ⊎ ¬ ¬ ∃ (toPred Q)

MP⊎-Bool : ∀ {a} → Set a → Set a
MP⊎-Bool A = (P Q : A → Bool) → MP⊎-Bool-i P Q

MP⊎-Alt-i : ∀ {a p} {A : Set a} → (P Q : A → Set p) → Set (a ⊔ p)
MP⊎-Alt-i P Q = DecU P → DecU Q →
                ¬ ((∀ x → P x) × (∀ x → Q x)) → ¬ (∀ x → P x) ⊎ ¬ (∀ x → Q x)

MP⊎-Alt : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
MP⊎-Alt A p = {P Q : A → Set p} → MP⊎-Alt-i P Q

MP∨-i : ∀ {a p} {A : Set a} → (P Q : A → Set p) → Set (a ⊔ p)
MP∨-i P Q = DecU P → DecU Q →
            ¬ ¬ (∃ λ x → P x ⊎ Q x) → ¬ ¬ ∃ P ⊎ ¬ ¬ ∃ Q

MP∨ : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
MP∨ A p = {P Q : A → Set p} → MP∨-i P Q

-- Σ-DGP
-- Equivalent to LLPO
Σ-DGP-i : ∀ {a p} {A : Set a} (P Q : A → Set p) → Set (a ⊔ p)
Σ-DGP-i P Q = DecU P → DecU Q → DGP-i (∃ P) (∃ Q)

Σ-DGP : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Σ-DGP A p = {P Q : A → Set p} → Σ-DGP-i P Q

-- Π-DGP
Π-DGP-i : ∀ {a p} {A : Set a} (P Q : A → Set p) → Set (a ⊔ p)
Π-DGP-i P Q = DecU P → DecU Q → DGP-i (∀ x → P x) (∀ x → Q x)

Π-DGP : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Π-DGP A p = {P Q : A → Set p} → Π-DGP-i P Q

-- Σ-Π-DGP
Σ-Π-DGP-i : ∀ {a p} {A : Set a} (P Q : A → Set p) → Set (a ⊔ p)
Σ-Π-DGP-i P Q = DecU P → DecU Q → DGP-i (∃ P) (∀ x → Q x)

Σ-Π-DGP : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Σ-Π-DGP A p = {P Q : A → Set p} → Σ-Π-DGP-i P Q

-- Σ-Call/CC
Σ-Call/CC-i : ∀ {a p} {A : Set a} (P : A → Set p) → Set (a ⊔ p)
Σ-Call/CC-i P = DecU P → Call/CC-i (∃ P)

Σ-Call/CC : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Σ-Call/CC A p = {P : A → Set p} → Σ-Call/CC-i P

-- Σ-Σ-Peirce
Σ-Σ-Peirce-i : ∀ {a p} {A : Set a} (P Q : A → Set p) → Set (a ⊔ p)
Σ-Σ-Peirce-i P Q = DecU P → DecU Q → Peirce-i (∃ P) (∃ Q)

Σ-Σ-Peirce : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Σ-Σ-Peirce A p = {P Q : A → Set p} → Σ-Σ-Peirce-i P Q

-- Σ-Π-Peirce
Σ-Π-Peirce-i : ∀ {a p} {A : Set a} (P Q : A → Set p) → Set (a ⊔ p)
Σ-Π-Peirce-i P Q = DecU P → DecU Q → Peirce-i (∃ P) (∀ x → Q x)

Σ-Π-Peirce : ∀ {a} (A : Set a) p → Set (a ⊔ lsuc p)
Σ-Π-Peirce A p = {P Q : A → Set p} → Σ-Π-Peirce-i P Q

-- Kripke's Schema
KS : ∀ {a} (A : Set a) p q → Set (a ⊔ lsuc p ⊔ lsuc q)
KS A p q = ∀ (P : Set p) → Σ (A → Set q) λ Q → DecU Q × (P <=> ∃ Q)

-- Principle of Finite Possiblity
-- Principle of inverse Decision (PID)
PFP : ∀ {a} (A : Set a) p q → Set (a ⊔ lsuc p ⊔ lsuc q)
PFP A p q = {P : A → Set p} → DecU P →
            Σ (A → Set q) λ Q → DecU Q × ((∀ x → P x) <=> ∃ Q)

PFP-Bool-ℕ : Set
PFP-Bool-ℕ =
  (α : ℕ → Bool) →
  Σ (ℕ → Bool) (λ β → (∀ n → α n ≡ false) <=> ∃ λ n → β n ≡ true)

-- Weak Principle of Finite Possiblity
WPFP : ∀ {a} (A : Set a) p q → Set (a ⊔ lsuc p ⊔ lsuc q)
WPFP A p q = {P : A → Set p} → DecU P →
             Σ (A → Set q) λ Q → DecU Q × ((∀ x → P x) <=> (¬ (∀ x → Q x)))

WPFP-Bool-ℕ : Set
WPFP-Bool-ℕ =
  (α : ℕ → Bool) →
  Σ (ℕ → Bool) λ β → (∀ n → α n ≡ false) <=> (¬ (∀ n → β n ≡ false))

-- https://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html
ACLT : ∀ {a b} → Set a → Set b → ∀ p → Set (a ⊔ b ⊔ lsuc p)
ACLT A B p = {P : A → B → Set p} →
             ((x : A) → ∃ λ y → P x y) → Σ (A → B) λ f → (x : A) → P x (f x)

-- HoTT
EM⁻¹ : ∀ a → Set (lsuc a)
EM⁻¹ a = {A : Set a} → isProp A → Dec⊎ A

DNE⁻¹ : ∀ a → Set (lsuc a)
DNE⁻¹ a = {A : Set a} → isProp A → Stable A

-- WKL
takeT : ℕ → (ℕ → Bool) → List Bool
takeT ℕ.zero    α = []
takeT (ℕ.suc n) α = α 0 ∷ takeT n (λ m → α (ℕ.suc m))

-- "THE WEAK KONIG LEMMA, BROUWER’S FAN THEOREM, DE MORGAN’S LAW, AND DEPENDENT CHOICE"
2^Bool* : Set₁
2^Bool* = List Bool → Set

IsDetachable : 2^Bool* → Set
IsDetachable T = DecU T

-- closed under restrictions
IsClosed : 2^Bool* → Set
IsClosed T = ∀ u v → Prefix _≡_ v u → T u → T v

IsInfinite : 2^Bool* → Set
IsInfinite T = ∀ n → ∃ λ u → T u × n ≡ length u

IsFinite : 2^Bool* → Set
IsFinite T = ∃ λ n → ∀ u → ¬ T u × n ≡ length u

IsWellFounded : 2^Bool* → Set
IsWellFounded T = Σ (ℕ → Bool) λ α → ∃ λ n → ¬ T (takeT n α)

HasInfinitePath : 2^Bool* → Set
HasInfinitePath T = Σ (ℕ → Bool) λ α → ∀ n → T (takeT n α)

IsTree : 2^Bool* → Set
IsTree T = IsDetachable T × IsClosed T

-- Weak Kőnig Lemma
WKL : Set₁
WKL = ∀ T → IsTree T → IsInfinite T → HasInfinitePath T

-- Brouwer’s Fan Theorem
FAN : Set₁
FAN = ∀ T → IsTree T → IsWellFounded T → IsFinite T

-- BD-N
Peseudobounded : (ℕ → Set) → Set
Peseudobounded S = (s : ℕ → ℕ) → (∀ n → S (s n)) → ∃ λ N → s N < N


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Fun.Facts.Terminal where

open import Cats.Category.Base
open import Cats.Category.Constructions.Terminal using (HasTerminal)
open import Cats.Category.Fun using (_↝_ ; ≈-intro)
open import Cats.Functor using (Functor)
open import Cats.Functor.Const using (Const)

open Functor

instance
  hasTerminal : ∀ {lo la l≈ lo′ la′ l≈′}
    → {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    → {{_ : HasTerminal D}}
    → HasTerminal (C ↝ D)
  hasTerminal {C = C} {D = D} {{D⊤}} = record
    { ⊤ = Const C ⊤
    ; isTerminal = λ X → record
      { arr = record
        { component = λ c → ! (fobj X c)
        ; natural = λ {c} {d} {f} → ⇒⊤-unique _ _
        }
      ; unique = λ _ → ≈-intro (⇒⊤-unique _ _)
      }
    }
    where
      open HasTerminal D⊤

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
open import Common.Bool
open import Common.Nat

data cheesy : Bool → Set where
  chocolate : cheesy false
  cheese    : cheesy true
  bread     : ∀ x → cheesy x

foo : ∀ {x : Bool} → cheesy x → cheesy x → Bool
foo x chocolate = {!!}
foo x cheese = {!!}
foo x (bread false) = {!x!}
foo x (bread true) = {!!}


text:
module Sessions.Syntax where

open import Sessions.Syntax.Types public
open import Sessions.Syntax.Expr public
open import Sessions.Syntax.Values public


text:
module Data.Num.Bij.Convert where

open import Data.Num.Bij
open import Data.Num.Bij.Properties

open import Data.List hiding ([_])
open import Relation.Binary
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Product
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Etc

open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; sym; cong; trans)
open PropEq.≡-Reasoning
import Level

{-
-- to ℕ, instance of Conversion
instance convNat : Conversion ℕ
convNat = conversion [_]' !_!'
    where   [_]' : ℕ → Bij
            [ zero  ]' = []
            [ suc n ]' = incrB [ n ]'
            !_!' : Bij → ℕ
            ! []       !' = 0
            ! one ∷ xs !' = 1 + 2 * ! xs !'
            ! two ∷ xs !' = 2 + 2 * ! xs !'
-}

-- Digit ⇒ ℕ
D[_]ℕ : DigitB → ℕ
D[ one ]ℕ = 1
D[ two ]ℕ = 2

-- ℕ ⇔ Bij
[_]B : ℕ → Bij
[ zero  ]B = []
[ suc n ]B = incrB [ n ]B

[_]ℕ : Bij → ℕ
[ []       ]ℕ = 0
[ one ∷ xs ]ℕ = 1 + 2 * [ xs ]ℕ
[ two ∷ xs ]ℕ = 2 + 2 * [ xs ]ℕ

-- properties
[]ℕ-∷-hom : ∀ x xs → [ x ∷ xs ]ℕ ≡ D[ x ]ℕ + 2 * [ xs ]ℕ
[]ℕ-∷-hom one _ = refl
[]ℕ-∷-hom two _ = refl

[]ℕ-incrB-hom : ∀ xs → [ incrB xs ]ℕ ≡ suc [ xs ]ℕ
[]ℕ-incrB-hom [] = refl
[]ℕ-incrB-hom (one ∷ xs) = refl
[]ℕ-incrB-hom (two ∷ xs) =
    begin
        suc (2 * [ incrB xs ]ℕ)
    ≡⟨ cong (λ x → suc (2 * x)) ([]ℕ-incrB-hom xs) ⟩
        suc (suc ([ xs ]ℕ + suc ([ xs ]ℕ + 0)))
    ≡⟨ cong (λ x → suc (suc x)) (+-suc [ xs ]ℕ ([ xs ]ℕ + 0)) ⟩
        suc (suc (suc (2 * [ xs ]ℕ)))
    ∎

[]ℕ-+B-hom : ∀ xs ys → [ xs +B ys ]ℕ ≡ [ xs ]ℕ + [ ys ]ℕ
[]ℕ-+B-hom [] ys = refl
[]ℕ-+B-hom (x ∷ xs) [] = sym (+-right-identity [ x ∷ xs ]ℕ)
[]ℕ-+B-hom (one ∷ xs) (one ∷ ys) =
    begin
        2 + 2 * [ xs +B ys ]ℕ
    ≡⟨ cong (λ x → 2 + 2 * x) ([]ℕ-+B-hom xs ys) ⟩
        2 + 2 * ([ xs ]ℕ + [ ys ]ℕ)
    ≡⟨ cong (λ x → 2 + x) (distrib-left-*-+ 2 [ xs ]ℕ [ ys ]ℕ) ⟩
        2 + (2 * [ xs ]ℕ + 2 * [ ys ]ℕ)
    ≡⟨ cong suc (sym (+-suc (2 * [ xs ]ℕ) (2 * [ ys ]ℕ))) ⟩
        suc (2 * [ xs ]ℕ + suc (2 * [ ys ]ℕ))
    ∎
[]ℕ-+B-hom (one ∷ xs) (two ∷ ys) =
    begin
        1 + 2 * [ incrB (xs +B ys) ]ℕ
    ≡⟨ cong (λ x → 1 + 2 * x) ([]ℕ-incrB-hom (xs +B ys)) ⟩
        1 + 2 * (1 + [ xs +B ys ]ℕ)
    ≡⟨ cong (λ x → 1 + 2 * (1 + x)) ([]ℕ-+B-hom xs ys) ⟩
        1 + 2 * suc ([ xs ]ℕ + [ ys ]ℕ)
    ≡⟨ cong suc (+-*-suc 2 ([ xs ]ℕ + [ ys ]ℕ)) ⟩
        1 + (2 + 2 * ([ xs ]ℕ + [ ys ]ℕ))
    ≡⟨ cong (λ x → 1 + (2 + x)) (distrib-left-*-+ 2 [ xs ]ℕ [ ys ]ℕ) ⟩
        1 + (2 + 2 * [ xs ]ℕ + 2 * [ ys ]ℕ)
    ≡⟨ cong (λ x → 1 + (x + 2 * [ ys ]ℕ)) (+-comm 2 (2 * [ xs ]ℕ)) ⟩
        1 + (2 * [ xs ]ℕ + 2 + 2 * [ ys ]ℕ)
    ≡⟨ cong suc (+-assoc (2 * [ xs ]ℕ) 2 (2 * [ ys ]ℕ)) ⟩
        1 + (2 * [ xs ]ℕ + (2 + (2 * [ ys ]ℕ)))
    ∎
[]ℕ-+B-hom (two ∷ xs) (one ∷ ys) =
    begin
        suc (2 * [ incrB (xs +B ys) ]ℕ)
    ≡⟨ cong (λ x → suc (2 * x)) ([]ℕ-incrB-hom (xs +B ys)) ⟩
        suc (2 * suc [ xs +B ys ]ℕ)
    ≡⟨ cong (λ x → suc (2 * suc x)) ([]ℕ-+B-hom xs ys) ⟩
        suc (2 * suc ([ xs ]ℕ + [ ys ]ℕ))
    ≡⟨ cong suc (+-*-suc 2 ([ xs ]ℕ + [ ys ]ℕ)) ⟩
        suc (2 + 2 * ([ xs ]ℕ + [ ys ]ℕ))
    ≡⟨ cong (λ x → suc (2 + x)) (distrib-left-*-+ 2 [ xs ]ℕ [ ys ]ℕ) ⟩
        suc (2 + 2 * [ xs ]ℕ + 2 * [ ys ]ℕ)
    ≡⟨ cong (λ x → suc (suc x)) (sym (+-suc (2 * [ xs ]ℕ) (2 * [ ys ]ℕ))) ⟩
        suc (suc (2 * [ xs ]ℕ + suc (2 * [ ys ]ℕ)))
    ∎

[]ℕ-+B-hom (two ∷ xs) (two ∷ ys) =
    begin
        2 + (2 * [ incrB (xs +B ys) ]ℕ)
    ≡⟨ cong (λ x → 2 + (2 * x)) ([]ℕ-incrB-hom (xs +B ys)) ⟩
        2 + (2 * suc [ xs +B ys ]ℕ)
    ≡⟨ cong (λ x → 2 + 2 * suc x) ([]ℕ-+B-hom xs ys) ⟩
        2 + (2 * suc ([ xs ]ℕ + [ ys ]ℕ))
    ≡⟨ cong (λ x → 2 + x) (+-*-suc 2 ([ xs ]ℕ + [ ys ]ℕ)) ⟩
        2 + (2 + 2 * ([ xs ]ℕ + [ ys ]ℕ))
    ≡⟨ cong (λ x → 2 + (2 + x)) (distrib-left-*-+ 2 [ xs ]ℕ [ ys ]ℕ) ⟩
        2 + (2 + 2 * [ xs ]ℕ + 2 * [ ys ]ℕ)
    ≡⟨ cong (λ x → 2 + (x + 2 * [ ys ]ℕ)) (+-comm 2 (2 * [ xs ]ℕ)) ⟩
        2 + (2 * [ xs ]ℕ + 2 + 2 * [ ys ]ℕ)
    ≡⟨ cong (λ x → 2 + x) (+-assoc (2 * [ xs ]ℕ) 2 (2 * [ ys ]ℕ)) ⟩
        2 + (2 * [ xs ]ℕ + (2 + 2 * [ ys ]ℕ))
    ∎

[]ℕ-*2-hom : ∀ xs → [ *2 xs ]ℕ ≡ 2 * [ xs ]ℕ
[]ℕ-*2-hom [] = refl
[]ℕ-*2-hom (one ∷ xs) =
    begin
        2 + 2 * [ *2 xs ]ℕ
    ≡⟨ cong (λ x → 2 + 2 * x) ([]ℕ-*2-hom xs) ⟩
        2 + 2 * (2 * [ xs ]ℕ)
    ≡⟨ cong suc (sym (+-suc (2 * [ xs ]ℕ) (2 * [ xs ]ℕ + zero))) ⟩
        suc (2 * [ xs ]ℕ + suc (2 * [ xs ]ℕ + zero))
    ∎
[]ℕ-*2-hom (two ∷ xs) =
    begin
        2 + 2 * [ incrB (*2 xs) ]ℕ
    ≡⟨ cong (λ x → 2 + 2 * x) ([]ℕ-incrB-hom (*2 xs)) ⟩
        2 + 2 * suc [ *2 xs ]ℕ
    ≡⟨ cong (λ x → 2 + 2 * suc x) ([]ℕ-*2-hom xs) ⟩
        2 + 2 * suc (2 * [ xs ]ℕ)
    ≡⟨ cong (λ x → 2 + x) (sym (+-suc (2 * [ xs ]ℕ) (suc (2 * [ xs ]ℕ + zero)))) ⟩
        2 + (2 * [ xs ]ℕ + suc (suc (2 * [ xs ]ℕ + zero)))
    ∎

[[]B]ℕ-id : ∀ n → [ [ n ]B ]ℕ ≡ n
[[]B]ℕ-id zero = refl
[[]B]ℕ-id (suc n) =
    begin
        [ incrB [ n ]B ]ℕ
    ≡⟨ []ℕ-incrB-hom [ n ]B ⟩
        suc [ [ n ]B ]ℕ
    ≡⟨ cong suc ([[]B]ℕ-id n) ⟩
        suc n
    ∎

[]ℕ-kernal : ∀ xs → [ xs ]ℕ ≡ 0 → xs ≡ []
[]ℕ-kernal [] pf = refl
[]ℕ-kernal (one ∷ xs) pf = contradiction pf (λ ())
[]ℕ-kernal (two ∷ xs) pf = contradiction pf (λ ())

[]ℕ-surjective : ∀ (x : ℕ) → ∃ (λ y → [ y ]ℕ ≡ x)
[]ℕ-surjective n = [ n ]B , [[]B]ℕ-id n
{-
[]ℕ-injective : ∀ x y → [ x ]ℕ ≡ [ y ]ℕ → x ≡ y
[]ℕ-injective []       []       pf = refl
[]ℕ-injective []       (y ∷ ys) pf = sym ([]ℕ-kernal (y ∷ ys) (sym pf))
[]ℕ-injective (x ∷ xs) []       pf = []ℕ-kernal (x ∷ xs) pf
[]ℕ-injective (one ∷ xs) (one ∷ ys) pf =
    begin
        one ∷ xs
    ≡⟨ cong (λ x → one ∷ x) ([]ℕ-injective xs ys {!   !}) ⟩
        one ∷ ys
    ∎
    --let pf0 = trans pf (cong (λ x → 1 + 2 * x) {!   !})
    --in {!   !}
[]ℕ-injective (one ∷ xs) (two ∷ ys) pf = {!   !}
[]ℕ-injective (two ∷ xs) (y ∷ ys) pf = {!   !}
-}
{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Relation.Binary.Core

module PLRTree.Heap.Properties {A : Set}
                     (_≤_ : A → A → Set)
                     (trans≤ : Transitive _≤_) where

open import PLRTree {A}
open import PLRTree.Heap _≤_

lemma-≤-≤* : {x y : A}{t : PLRTree} → x ≤ y → y ≤* t → x ≤* t
lemma-≤-≤* {x = x} _ (lf≤* _) = lf≤* x
lemma-≤-≤* x≤y (nd≤* y≤z y≤*l y≤*r) = nd≤* (trans≤ x≤y y≤z) (lemma-≤-≤* x≤y y≤*l) (lemma-≤-≤* x≤y y≤*r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting