text:
module Structure.Operator.Names where

open import Functional.Dependent
open import Function.Names
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Function.Names
open import Structure.Setoid
open import Syntax.Function
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ ℓ₁ ℓ₂ ℓ₃ ℓᵣ₂ ℓᵣ₃ ℓᵣ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑᵣ : Lvl.Level

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ where
  -- Definition of commutativity of specific elements.
  -- The binary operation swapped yields the same result.
  -- Example: For any x, (x ▫ x) always commutes.
  Commuting : (T₁ → T₁ → T₂) → T₁ → T₁ → Stmt
  Commuting(_▫_) = pointwise₂,₂(_≡_) (_▫_) (swap(_▫_))

  -- Definition of commutativity.
  -- Order of application for the operation does not matter for equality.
  -- Example: Addition of the natural numbers (_+_ : ℕ → ℕ → ℕ).
  Commutativity : (T₁ → T₁ → T₂) → Stmt
  Commutativity = ∀² ∘ Commuting

  -- Definition of an left identity element.
  -- Example: Top implies a proposition in boolean logic (⊤ →_).
  Identityₗ : (T₁ → T₂ → T₂) → T₁ → Stmt
  Identityₗ (_▫_) id = ∀{x : T₂} → (id ▫ x) ≡ x

  -- Definition of a right absorber element
  -- Also called "right neutral element" or "right annihilator"
  -- Applying the operation on this element to the right always yields itself.
  -- Example: A proposition implies top in boolean logic (_→ ⊤).
  Absorberᵣ : (T₁ → T₂ → T₂) → T₂ → Stmt
  Absorberᵣ (_▫_) null = ∀{x : T₁} → (x ▫ null) ≡ null

  ConverseAbsorberᵣ : (T₁ → T₂ → T₂) → T₂ → Stmt
  ConverseAbsorberᵣ (_▫_)(a) = ∀{x y} → (x ▫ y ≡ a) → (y ≡ a)

module _ {T₁ : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ {T₂ : Type{ℓ₂}} where
  -- Definition of an right identity element
  -- Example: Subtracting 0 for integers (_− 0).
  Identityᵣ : (T₁ → T₂ → T₁) → T₂ → Stmt
  Identityᵣ(_▫_) id = Identityₗ(swap(_▫_)) id

  -- Definition of a left absorber element
  -- Also called "left neutral element" or "left annihilator"
  -- Example: Subtraction (monus) of 0 for natural numbers (0 − ).
  Absorberₗ : (T₁ → T₂ → T₁) → T₁ → Stmt
  Absorberₗ(_▫_) null = Absorberᵣ(swap(_▫_)) null

  ConverseAbsorberₗ : (T₁ → T₂ → T₁) → T₁ → Stmt
  ConverseAbsorberₗ (_▫_)(a) = ∀{x y} → (x ▫ y ≡ a) → (x ≡ a)

module _ {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ where
  -- Definition of an identity element
  -- Example: 0 for addition of integers, 1 for multiplication of integers.
  Identity : (T → T → T) → T → Stmt
  Identity (_▫_) id = (Identityₗ (_▫_) id) ∧ (Identityᵣ (_▫_) id)

  -- Definition of idempotence.
  Idempotence : (T → T → T) → Stmt
  Idempotence (_▫_) = ∀{x : T} → (x ▫ x ≡ x)

  -- Example: 0 for addition of natural numbers, 1 for multiplication of natural numbers.
  ConverseAbsorber : (T → T → T) → T → Stmt
  ConverseAbsorber (_▫_)(a) = ∀{x y} → (x ▫ y ≡ a) → (x ≡ a)∧(y ≡ a)

  -- Example: 0 for multiplication of natural numbers.
  WeakConverseAbsorber : (T → T → T) → T → Stmt
  WeakConverseAbsorber (_▫_)(a) = ∀{x y} → (x ▫ y ≡ a) → (x ≡ a)∨(y ≡ a)

module _ {T₊ : Type{ℓ₁}} {T₋ : Type{ℓ₂}} {Tᵣ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑᵣ}(Tᵣ) ⦄ where
  -- Definition of a left inverse element.
  InverseElementₗ : (T₋ → T₊ → Tᵣ) → Tᵣ → T₊ → T₋ → Stmt
  InverseElementₗ (_▫_) id x x⁻¹ = ((x⁻¹ ▫ x) ≡ id)

  -- Definition of a right inverse element
  InverseElementᵣ : (T₊ → T₋ → Tᵣ) → Tᵣ → T₊ → T₋ → Stmt
  InverseElementᵣ (_▫_) id x x⁻¹ = ((x ▫ x⁻¹) ≡ id)

  -- Definition of a left inverse function
  InverseFunctionₗ : (T₋ → T₊ → Tᵣ) → Tᵣ → (T₊ → T₋) → Stmt
  InverseFunctionₗ (_▫_) id inv = ∀{x : T₊} → InverseElementₗ(_▫_) id x (inv x)

  -- Definition of a right inverse function
  InverseFunctionᵣ : (T₊ → T₋ → Tᵣ) → Tᵣ → (T₊ → T₋) → Stmt
  InverseFunctionᵣ (_▫_) id inv = ∀{x : T₊} → InverseElementᵣ(_▫_) id x (inv x)

module _ {T : Type{ℓ₁}} {Tᵣ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑᵣ}(Tᵣ) ⦄ where
  -- Definition of an invertible element
  InverseElement : (T → T → Tᵣ) → Tᵣ → T → T → Stmt
  InverseElement (_▫_) id x x⁻¹ = (InverseElementₗ(_▫_) id x x⁻¹) ∧ (InverseElementᵣ(_▫_) id x x⁻¹)

  -- Definition of a function which returns the inverse element of the other side of the operation
  InverseFunction : (T → T → Tᵣ) → Tᵣ → (T → T) → Stmt
  InverseFunction (_▫_) id inv = (InverseFunctionₗ (_▫_) id inv) ∧ (InverseFunctionᵣ (_▫_) id inv)

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₃}(T₃) ⦄ where
  -- Definition of right cancellation of a specific object
  -- ∀{a b : T₂} → ((x ▫ a) ≡ (x ▫ b)) → (a ≡ b)
  CancellationOnₗ : (T₁ → T₂ → T₃) → T₁ → Stmt
  CancellationOnₗ (_▫_) (x) = Injective(x ▫_)

  -- Definition of left cancellation (Injectivity for the right param)
  -- ∀{x : T₁}{a b : T₂} → ((x ▫ a) ≡ (x ▫ b)) → (a ≡ b)
  Cancellationₗ : (T₁ → T₂ → T₃) → Stmt
  Cancellationₗ (_▫_) = (∀{x : T₁} → CancellationOnₗ(_▫_)(x))

module _ {T₁ : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₃}(T₃) ⦄ where
  -- Definition of right cancellation of a specific object
  -- ∀{a b : T₁} → ((a ▫ x) ≡ (b ▫ x)) → (a ≡ b)
  CancellationOnᵣ : (T₁ → T₂ → T₃) → T₂ → Stmt
  CancellationOnᵣ (_▫_) (x) = Injective(_▫ x)

  -- Definition of right cancellation (Injectivity for the left param)
  -- ∀{x : T₂}{a b : T₁} → ((a ▫ x) ≡ (b ▫ x)) → (a ≡ b)
  Cancellationᵣ : (T₁ → T₂ → T₃) → Stmt
  Cancellationᵣ (_▫_) = (∀{x : T₂} → CancellationOnᵣ (_▫_)(x))

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ where
  -- Definition of the left inverse property
  InverseOperatorOnₗ : (T₁ → T₂ → T₃) → (T₁ → T₃ → T₂) → T₁ → T₂ → Stmt
  InverseOperatorOnₗ (_▫₁_) (_▫₂_) x y = (x ▫₂ (x ▫₁ y) ≡ y)

  InverseOperatorₗ : (T₁ → T₂ → T₃) → (T₁ → T₃ → T₂) → Stmt
  InverseOperatorₗ (_▫₁_)(_▫₂_) = ∀{x y} → InverseOperatorOnₗ(_▫₁_)(_▫₂_) x y

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ where
  -- Definition of the right inverse property
  InverseOperatorOnᵣ : (T₁ → T₂ → T₃) → (T₃ → T₂ → T₁) → T₁ → T₂ → Stmt
  InverseOperatorOnᵣ (_▫₁_) (_▫₂_) x y = ((x ▫₁ y) ▫₂ y ≡ x)

  InverseOperatorᵣ : (T₁ → T₂ → T₃) → (T₃ → T₂ → T₁) → Stmt
  InverseOperatorᵣ (_▫₁_)(_▫₂_) = ∀{x y} → InverseOperatorOnᵣ(_▫₁_)(_▫₂_) x y

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ where
  InversePropertyₗ : (T₁ → T₂ → T₂) → (T₁ → T₁) → Stmt
  InversePropertyₗ (_▫_) inv = InverseOperatorₗ(_▫_)(a ↦ b ↦ inv(a) ▫ b)

  InversePropertyᵣ : (T₂ → T₁ → T₂) → (T₁ → T₁) → Stmt
  InversePropertyᵣ (_▫_) inv = InverseOperatorᵣ(_▫_)(a ↦ b ↦ a ▫ inv(b))

---------------------------------------------------------
-- Patterns

module _ {T₁ : Type{ℓ₁}}{T₂ : Type{ℓ₂}}{T₃ : Type{ℓ₃}}{Tᵣ₂ : Type{ℓᵣ₂}}{Tᵣ₃ : Type{ℓᵣ₃}}{Tᵣ : Type{ℓᵣ}} ⦃ _ : Equiv{ℓₑᵣ}(Tᵣ) ⦄ where
  AssociativityPattern : (T₁ → T₂ → Tᵣ₃) → (Tᵣ₃ → T₃ → Tᵣ)  → (T₁ → Tᵣ₂ → Tᵣ) → (T₂ → T₃ → Tᵣ₂)→ Stmt
  AssociativityPattern (_▫₁_) (_▫₂_) (_▫₃_) (_▫₄_) =
    ∀{x : T₁}{y : T₂}{z : T₃} → ((x ▫₁ y) ▫₂ z) ≡ (x ▫₃ (y ▫₄ z))

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₃}(T₃) ⦄ where
  DistributivityPatternₗ : (T₁ → T₂ → T₃) → (T₂ → T₂ → T₂) → (T₃ → T₃ → T₃) → Stmt
  DistributivityPatternₗ (_▫₁_) (_▫₂_) (_▫₃_) =
    ∀{x : T₁} {y z : T₂} → (x ▫₁ (y ▫₂ z)) ≡ ((x ▫₁ y) ▫₃ (x ▫₁ z))

  DistributivityPatternᵣ : (T₁ → T₂ → T₃) → (T₁ → T₁ → T₁) → (T₃ → T₃ → T₃) → Stmt
  DistributivityPatternᵣ (_▫₁_) (_▫₂_) (_▫₃_) =
    ∀{x y : T₁} {z : T₂} → ((x ▫₂ y) ▫₁ z) ≡ ((x ▫₁ z) ▫₃ (y ▫₁ z))

---------------------------------------------------------
-- Derived

module _ {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ where
  -- Definition of associativity for a binary operation
  Associativity : (T → T → T) → Stmt
  Associativity (_▫_) = AssociativityPattern (_▫_) (_▫_) (_▫_) (_▫_)
  -- {x y z : T} → ((x ▫ y) ▫ z) ≡ (x ▫ (y ▫ z))

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ where
  -- Definition of compatibility for a binary operation
  Compatibility : (T₁ → T₁ → T₁) → (T₁ → T₂ → T₂) → Stmt -- TODO: https://en.wikipedia.org/wiki/Semigroup_action
  Compatibility (_▫₁_) (_▫₂_) = AssociativityPattern (_▫₁_) (_▫₂_) (_▫₂_) (_▫₂_)
  -- {x₁ x₂ : T₁}{y : T₂} → ((x₁ ▫₁ x₂) ▫₂ y) ≡ (x₁ ▫₂ (x₂ ▫₂ y))

  -- Definition of left distributivity for a binary operation
  Distributivityₗ : (T₁ → T₂ → T₂) → (T₂ → T₂ → T₂) → Stmt
  Distributivityₗ (_▫₁_) (_▫₂_) = DistributivityPatternₗ (_▫₁_) (_▫₂_) (_▫₂_)
  -- ∀{x : T₁} {y z : T₂} → (x ▫₁ (y ▫₂ z)) ≡ (x ▫₁ y) ▫₂ (x ▫₁ z)

  -- Definition of right distributivity for a binary operation
  Distributivityᵣ : (T₂ → T₁ → T₂) → (T₂ → T₂ → T₂) → Stmt
  Distributivityᵣ (_▫₁_) (_▫₂_) = DistributivityPatternᵣ (_▫₁_) (_▫₂_) (_▫₂_)
  -- ∀{x y : T₂} {z : T₁} → ((x ▫₂ y) ▫₁ z) ≡ (x ▫₁ z) ▫₂ (y ▫₁ z)

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ where
  -- Definition of left absorption for two binary operators
  Absorptionₗ : (T₁ → T₃ → T₁) → (T₁ → T₂ → T₃) → Stmt
  Absorptionₗ (_▫₁_)(_▫₂_) = ∀{x : T₁}{y : T₂} → (x ▫₁ (x ▫₂ y) ≡ x)

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ where
  -- Definition of right absorption for two binary operators
  Absorptionᵣ : (T₃ → T₂ → T₂) → (T₁ → T₂ → T₃) → Stmt
  Absorptionᵣ (_▫₁_)(_▫₂_) = ∀{x : T₁}{y : T₂} → ((x ▫₂ y) ▫₁ y ≡ y)

---------------------------------------------------------
-- Functions (TODO: Move to Structure.Operator.Proofs)
{-
open import Relator.Equals{ℓ₁}{ℓ₂}
open import Relator.Equals.Proofs{ℓ₁}{ℓ₂}

-- Returns a commuted LHS of an equality
commuteₗ : ∀{T}{_▫_}{x y z} → ⦃ _ : Commutativity {T} {T} (_▫_) ⦄ → ((x ▫ y) ≡ z) → ((y ▫ x) ≡ z)
commuteₗ ⦃ comm ⦄ stmt = comm 🝖 stmt

-- Returns a commuted RHS of an equality
commuteᵣ : ∀{T}{_▫_}{x y z} → ⦃ _ : Commutativity {T} {T} (_▫_) ⦄ → (z ≡ (x ▫ y)) → (z ≡ (y ▫ x))
commuteᵣ ⦃ comm ⦄ stmt = stmt 🝖 comm

commuteBoth : ∀{T₁ T₂}{_▫_}{a₁ a₂ b₁ b₂} → Commutativity{T₁}{T₂}(_▫_) → (a₁ ▫ a₂ ≡ b₁ ▫ b₂) → (a₂ ▫ a₁ ≡ b₂ ▫ b₁)
commuteBoth {_}{_} {a₁} {a₂} {b₁} {b₂} commutativity (a₁▫a₂≡b₁▫b₂) =
    (symmetry ⦃ [≡]-symmetry ⦄ (commutativity {a₁} {a₂}))
    🝖' (a₁▫a₂≡b₁▫b₂)
    🝖' (commutativity {b₁} {b₂})
    where
      _🝖'_ = _🝖_ ⦃ [≡]-transitivity ⦄
      infixl 1000 _🝖'_
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
postulate
  F G : (Set → Set) → Set
  !_  : Set → Set

infix 2 F
infix 1 !_

syntax F (λ X → Y) = X , Y
syntax G (λ X → Y) = Y , X

-- This parsed when default fixity was 'unrelated', but with
-- an actual default fixity (of any strength) in place it really
-- should not.
Foo : Set
Foo = ! X , X

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
data D : Set where

record R : Set where
  constructor d
  field x : D

record R′ : Set where
  coinductive
  constructor d
  field r : R′

f : R → D
f r = let d x = r in x


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Float where

open import Agda.Builtin.Float public
open import Common.String

floatToString : Float  -> String
floatToString = primShowFloat


text:
{-# OPTIONS --no-universe-polymorphism #-}
open import Data.Product hiding (map)
open import Relation.Binary.Core hiding (Total)
open import Relation.Nullary
open import Data.Nat
import Level as L using (zero)
open import Data.List
open import Data.Unit using (⊤)
open import Data.Empty

open import DivideEtImpera
open import Equivalence
open import BagEquality
open import Lists

module Quicksort where

splitWith : {A : Set} {P Q : A → Set} → (∀ x → P x ⊕ Q x) → List A → List A × List A
splitWith _ []   = ([] , [])
splitWith decPQ (x ∷ xs) with (decPQ x)
splitWith decPQ (x ∷ xs) | (inj₁ _) = (x ∷ (proj₁ res), proj₂ res) where
                                                        res = splitWith decPQ xs
splitWith decPQ (x ∷ xs) | (inj₂ _) = (proj₁ res , x ∷ (proj₂ res)) where
                                                        res = splitWith decPQ xs

splitWithProp1 : {A : Set} {P Q : A → Set} → (decPQ : ∀ x → P x ⊕ Q x) → (xs : List A) → (z : A) → z ∈ proj₁ (splitWith decPQ xs) → P z
splitWithProp1 decPQ [] z zIn1 = ⊥-elim zIn1
splitWithProp1 decPQ (x ∷ xs) z zIn with (decPQ x)
splitWithProp1 decPQ (x ∷ xs) .x (inj₁ refl) | (inj₁ pfP) = pfP
splitWithProp1 decPQ (x ∷ xs) z  (inj₂ zIn)  | (inj₁ _  ) = splitWithProp1 decPQ xs z zIn
splitWithProp1 decPQ (x ∷ xs) z  zIn         | (inj₂ _  ) = splitWithProp1 decPQ xs z zIn

splitWithProp2 : {A : Set} {P Q : A → Set} → (decPQ : ∀ x → P x ⊕ Q x) → (xs : List A) → (z : A) → z ∈ proj₂ (splitWith decPQ xs) → Q z
splitWithProp2 decPQ [] z zIn1 = ⊥-elim zIn1
splitWithProp2 decPQ (x ∷ xs) z zIn with (decPQ x)
splitWithProp2 decPQ (x ∷ xs) .x (inj₁ refl) | (inj₂ pfQ) = pfQ
splitWithProp2 decPQ (x ∷ xs) z  (inj₂ zIn)  | (inj₂ _  ) = splitWithProp2 decPQ xs z zIn
splitWithProp2 decPQ (x ∷ xs) z  zIn         | (inj₁ _  ) = splitWithProp2 decPQ xs z zIn

×-join : {A B C : Set} → (pair : A × B) → (op : A → B → C) → C
×-join (a , b) op = op a b

splitWith-cong : {A : Set} {P Q : A → Set} → (decPQ : ∀ x → P x ⊕ Q x) → (xs : List A) → (proj₁ (splitWith decPQ xs)) ++ (proj₂ (splitWith decPQ xs)) ≈ xs
splitWith-cong _ [] z = ⊥ □↔
splitWith-cong decPQ (x ∷ xs) z with (decPQ x)
splitWith-cong decPQ (x ∷ xs) z | (inj₁ _) = let (res1 , res2) = splitWith decPQ xs
                                                   in (z ≡ x) ⊕ Any (z ≡_) (res1 ++ res2) ↔⟨ ⊕-cong ((z ≡ x) □↔) (splitWith-cong decPQ xs z) ⟩
                                                      (z ≡ x) ⊕ Any (z ≡_) xs □↔
splitWith-cong decPQ (x ∷ xs) z | (inj₂ _) = let (res1 , res2) = splitWith decPQ xs
                                                   in Any (z ≡_) (res1 ++ x ∷ res2) ↔⟨ ++-comm res1 (x ∷ res2) z ⟩
                                                      (z ≡ x) ⊕ Any (z ≡_) (res2 ++ res1) ↔⟨ ⊕-cong ((z ≡ x) □↔) (++-comm res2 res1 z) ⟩
                                                      (z ≡ x) ⊕ Any (z ≡_) (res1 ++ res2) ↔⟨ ⊕-cong ((z ≡ x) □↔) (splitWith-cong decPQ xs z) ⟩
                                                      (z ≡ x) ⊕ Any (z ≡_) xs □↔

≤′-suc : {n m : ℕ} → n ≤′ m → suc n ≤′ suc m
≤′-suc ≤′-refl = ≤′-refl
≤′-suc (≤′-step pf) = ≤′-step (≤′-suc pf)

splitWith-length1 : {A : Set} {P Q : A → Set} → (decPQ : ∀ x → P x ⊕ Q x) → (xs : List A) → length (proj₁ (splitWith decPQ xs)) ≤′ length xs
splitWith-length1 _ [] = ≤′-refl
splitWith-length1 decPQ (x ∷ xs) with (decPQ x)
splitWith-length1 decPQ (x ∷ xs) | (inj₁ _) = ≤′-suc (splitWith-length1 decPQ xs)
splitWith-length1 decPQ (x ∷ xs) | (inj₂ _) = ≤′-step (splitWith-length1 decPQ xs)

splitWith-length2 : {A : Set} {P Q : A → Set} → (decPQ : ∀ x → P x ⊕ Q x) → (xs : List A) → length (proj₂ (splitWith decPQ xs)) ≤′ length xs
splitWith-length2 _ [] = ≤′-refl
splitWith-length2 decPQ (x ∷ xs) with (decPQ x)
splitWith-length2 decPQ (x ∷ xs) | (inj₁ _) = ≤′-step (splitWith-length2 decPQ xs)
splitWith-length2 decPQ (x ∷ xs) | (inj₂ _) = ≤′-suc (splitWith-length2 decPQ xs)

qs-DecompCond : {A : Set} → Rel A L.zero → List A → (A × List A × List A) → Set
qs-DecompCond LEQ xs (piv , ys , zs) = (piv ∷ (ys ++ zs) ≈ xs) × (∀ y → y ∈ ys → LEQ y piv) × (∀ z → z ∈ zs → LEQ piv z)

qs-InputCond : {A : Set} → List A → Set
qs-InputCond x = ⊤

qs-OutputCond : {A : Set} → Rel A L.zero → List A → List A → Set
qs-OutputCond LEQ xs ys = ys ≈ xs × Ordered LEQ ys

qs-G-InputCond : {A : Set} → A → Set
qs-G-InputCond x = ⊤

qs-G-OutputCond : {A : Set} → A → A → Set
qs-G-OutputCond x y = x ≡ y

qs-CompCond : {A : Set} → (A × List A × List A) → List A → Set
qs-CompCond (piv , xs , ys) zs = xs ++ piv ∷ ys ≡ zs

qs-InductionLemma : {A : Set} → (LEQ : Rel A L.zero) → ∀{x₀ x₁ x₂ x₃ z₀ z₁ z₂ z₃} → qs-DecompCond LEQ x₀ (x₁ , x₂ , x₃ ) → qs-G-OutputCond x₁ z₁  →
                             qs-OutputCond LEQ x₂ z₂ → qs-OutputCond LEQ x₃ z₃ → qs-CompCond (z₁ , z₂ , z₃) z₀ → qs-OutputCond LEQ x₀ z₀
qs-InductionLemma LEQ {xs} {piv} {ys₁} {ys₂} {ws} {.piv} {zs₁} {zs₂} (piv∷ys₁++ys₂≈xs , ltPiv , gtPiv) refl (zs₁≈ys₁ , ord₁) (zs₂≈ys₂ , ord₂) refl
                                         = (λ x → x ∈ (zs₁ ++ piv ∷ zs₂) ↔⟨ ++-comm zs₁ (piv ∷ zs₂) x ⟩
                                                  (x ∈ ((piv ∷ zs₂) ++ zs₁)) ↔⟨ Any-++ (λ z → x ≡ z) (piv ∷ zs₂) zs₁ ⟩
                                                  ((x ≡ piv) ⊕ x ∈ zs₂) ⊕ x ∈ zs₁  ↔⟨ ↔sym ⊕-assoc  ⟩
                                                  (x ≡ piv) ⊕ (x ∈ zs₂ ⊕ x ∈ zs₁) ↔⟨ ⊕-cong ((x ≡ piv) □↔) (⊕-cong (zs₂≈ys₂ x) (zs₁≈ys₁ x)) ⟩
                                                  (x ≡ piv) ⊕ (x ∈ ys₂ ⊕ x ∈ ys₁) ↔⟨ ⊕-cong ((x ≡ piv) □↔) ⊕-comm ⟩
                                                  (x ≡ piv) ⊕ (x ∈ ys₁ ⊕ x ∈ ys₂) ↔⟨ ⊕-cong ((x ≡ piv) □↔) (↔sym (Any-++ (λ z → x ≡ z) ys₁ ys₂)) ⟩
                                                  x ∈ (piv ∷ (ys₁ ++ ys₂)) ↔⟨ piv∷ys₁++ys₂≈xs x ⟩
                                                  x ∈ xs □↔) ,
                                                       ++-Order-cong (λ x x∈zs₁ → ltPiv x (_↔_.to (zs₁≈ys₁ x) x∈zs₁)) ord₁
                                                     (cons-Order-cong (λ x x∈zs₂ → gtPiv x (_↔_.to (zs₂≈ys₂ x) x∈zs₂)) ord₂)

qs-Decomp : {A : Set} → {LEQ : Rel A L.zero} → Total LEQ → (xs : List A) → ⊤ → ¬ ListPrimitive xs → Σ (A × List A × List A)
                                                                λ y → qs-G-InputCond (proj₁ y) × (qs-InputCond (proj₁ (proj₂ y))) × (qs-InputCond (proj₂ (proj₂ y))) ×
                                                                      ((proj₁ (proj₂ y)) <l xs) × ((proj₂ (proj₂ y)) <l xs) × (qs-DecompCond LEQ xs y)
qs-Decomp total [] _ notPrim = ⊥-elim (notPrim (NilIsPrim))
qs-Decomp total (x ∷ xs) _ _ = ( x , splitWith (λ y → total y x) xs) ,  (⊤.tt , ⊤.tt , ⊤.tt , ≤′-suc (splitWith-length1 (λ y → total y x) xs) , ≤′-suc (splitWith-length2 (λ y → total y x) xs) ,
                                                                             ((λ z → (z ≡ x) ⊕ z ∈ (proj₁ (splitWith (λ y → total y x) xs) ++ proj₂ (splitWith (λ y → total y x) xs))
                                                                                ↔⟨ ⊕-cong ((z ≡ x) □↔) (splitWith-cong (λ y → total y x) xs z) ⟩
                                                                                (z ≡ x) ⊕ z ∈ xs □↔) ,
                                                                              splitWithProp1 (λ y → total y x) xs ,
                                                                              splitWithProp2 (λ y → total y x) xs))

qs-G : {A : Set} → (x : A) → ⊤ → Σ A (qs-G-OutputCond x)
qs-G x _ = (x , refl)

qs-Comp : {A : Set} → (y : A × (List A × List A)) → Σ (List A) (qs-CompCond y)
qs-Comp (piv , xs , ys) = (xs ++ piv ∷ ys , refl)

qs-DirSolve : {A : Set} → (LEQ : Rel A L.zero) → (xs : List A) → ⊤ → ListPrimitive xs → Σ (List A) (qs-OutputCond LEQ xs)
qs-DirSolve _ []      _ _    = ([] , (λ z → z ∈ [] □↔) , NilIsOrd)
qs-DirSolve _ (_ ∷ _) _ prim = ⊥-elim (consIsNotPrim prim)

quicksort : {A : Set} → {LEQ : Rel A L.zero} → Total LEQ → (xs : List A) → Σ (List A) (λ ys → ys ≈ xs × Ordered LEQ ys)
quicksort {LEQ = LEQ} total xs = makeD&C2 <l-wellFounded
                                          primDec
                                          (qs-Decomp total)
                                          qs-Comp
                                          qs-G
                                          (qs-DirSolve LEQ)
                                          (qs-InductionLemma LEQ)
                                          xs ⊤.tt

_≤_-total : Total _≤_
_≤_-total zero    n       = inj₁ z≤n
_≤_-total n       zero    = inj₂ z≤n
_≤_-total (suc n) (suc m) with (_≤_-total n m)
_≤_-total (suc n) (suc m) | (inj₁ n≤m) = inj₁ (s≤s n≤m)
_≤_-total (suc n) (suc m) | (inj₂ m≤n) = inj₂ (s≤s m≤n)

nat-quicksort = quicksort _≤_-total

max_stars_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_issues_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_forks_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda


text:
------------------------------------------------------------------------
-- Normalization of raw terms in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Syntax.Normalization where

open import Data.Context.WellFormed using (module ⊤-WellFormed)
open import Data.Fin using (Fin; zero; suc; raise; lift)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas using (module VarLemmas)
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.Maybe using (just; nothing)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using ([]; _∷_; _∷ʳ_)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Vec as Vec using ([]; _∷_)
import Data.Vec.Properties as VecProps
open import Function using (_∘_; flip)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε)
open import Relation.Binary.PropositionalEquality as P hiding ([_])

open import FOmegaInt.Reduction.Full
open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution

open Syntax

----------------------------------------------------------------------
-- Kind simplification as a relation.

infix 4 ⌊_⌋≡_

-- Kind simplification (aka erasure to shapes) as a relation.
--
-- We introduce an inductively defined relation on kinds (and shapes)
-- that precisely relates a (dependent) kind to its shape.  Proofs of
-- ⌊ j ⌋≡ k are equivalent to proofs that ⌊ j ⌋ ≡ k, as witnessed by
-- the ⌊⌋-⌊⌋≡ and ⌊⌋≡⇒⌊⌋-≡ lemmas below, but the former are easier to
-- work with in certain functions and lemmas that are defined by
-- recursion on shapes since the recursion structure then matches the
-- inductive structure of the relation.  A prime example of this is
-- η-expansion as implemented below (see the definition of η-exp in
-- the TrackSimpleKindsEtaExp module).  Most lemmas about η-expansion
-- also use the ⌊_⌋≡_ relation in a similar way.

data ⌊_⌋≡_ {T n} : Kind T n → SKind → Set where
  is-★ : ∀ {a b}                                   → ⌊ a ⋯ b ⌋≡ ★
  is-⇒ : ∀ {j₁ j₂ k₁ k₂} → ⌊ j₁ ⌋≡ k₁ → ⌊ j₂ ⌋≡ k₂ → ⌊ Π j₁ j₂ ⌋≡ k₁ ⇒ k₂

-- Kind simplification as a relation agrees with kind simplification
-- as a function.

⌊⌋-⌊⌋≡ : ∀ {T n} (k : Kind T n) → ⌊ k ⌋≡ ⌊ k ⌋
⌊⌋-⌊⌋≡ (a ⋯ b) = is-★
⌊⌋-⌊⌋≡ (Π j k) = is-⇒ (⌊⌋-⌊⌋≡ j) (⌊⌋-⌊⌋≡ k)

⌊⌋≡⇒⌊⌋-≡ : ∀ {T n k} {j : Kind T n} → ⌊ j ⌋≡ k → ⌊ j ⌋ ≡ k
⌊⌋≡⇒⌊⌋-≡ is-★                   = refl
⌊⌋≡⇒⌊⌋-≡ (is-⇒ ⌊j₁⌋=k₁ ⌊j₂⌋=k₂) =
  cong₂ _⇒_ (⌊⌋≡⇒⌊⌋-≡ ⌊j₁⌋=k₁) (⌊⌋≡⇒⌊⌋-≡ ⌊j₂⌋=k₂)

⌊⌋≡-trans : ∀ {T n m k} {j : Kind T n} {l : Kind T m} →
            ⌊ j ⌋ ≡ ⌊ l ⌋ → ⌊ l ⌋≡ k → ⌊ j ⌋≡ k
⌊⌋≡-trans ⌊j⌋≡⌊l⌋ ⌊l⌋≡k rewrite (sym (⌊⌋≡⇒⌊⌋-≡ ⌊l⌋≡k)) =
  subst (⌊ _ ⌋≡_) ⌊j⌋≡⌊l⌋ (⌊⌋-⌊⌋≡ _)

-- Kind simplification is proof-irrelevant.

⌊⌋≡-pirr : ∀ {T n k} {j : Kind T n} → (p₁ p₂ : ⌊ j ⌋≡ k) → p₁ ≡ p₂
⌊⌋≡-pirr is-★ is-★                     = refl
⌊⌋≡-pirr (is-⇒ p₁₁ p₁₂) (is-⇒ p₂₁ p₂₂) =
  cong₂ is-⇒ (⌊⌋≡-pirr p₁₁ p₂₁) (⌊⌋≡-pirr p₁₂ p₂₂)

-- A type of abstract lemma stating that kind simplification as a
-- relation commutes with substitution.

KindSimpAppLemma : ∀ {T T′} (app : Application (Kind T) T′) → Set
KindSimpAppLemma {_} {T′} app =
  ∀ {m n j k} {σ : Sub T′ m n} → ⌊ j ⌋≡ k → ⌊ j / σ ⌋≡ k
  where open Application app

-- Lemmas relating kind simplification to operations on T-kinds.

record KindSimpLemmas (T : ℕ → Set) : Set₁ where

  field lemmas : TermLikeLemmas (Kind T) Term
  open TermLikeLemmas lemmas
    using (termApplication; varApplication; weaken; weaken⋆)

  field
    ⌊⌋≡-/    : KindSimpAppLemma termApplication
    ⌊⌋≡-/Var : KindSimpAppLemma varApplication

  -- Kind simplification as a relation commutes with weakening.

  ⌊⌋≡-weaken : ∀ {n k} {j : Kind T n} → ⌊ j ⌋≡ k → ⌊ weaken j ⌋≡ k
  ⌊⌋≡-weaken ⌊j⌋≡k = ⌊⌋≡-/Var ⌊j⌋≡k

  ⌊⌋≡-weaken⋆ : ∀ m {n k} {j : Kind T n} → ⌊ j ⌋≡ k → ⌊ weaken⋆ m j ⌋≡ k
  ⌊⌋≡-weaken⋆ zero    ⌊j⌋≡k = ⌊j⌋≡k
  ⌊⌋≡-weaken⋆ (suc m) ⌊j⌋≡k = ⌊⌋≡-weaken (⌊⌋≡-weaken⋆ m ⌊j⌋≡k)

module KindSimpSubstApp {T} {l : Lift T Term} where
  open SubstApp l

  -- Kind simplification as a relation commutes with substitution.

  ⌊⌋≡-Kind/ : ∀ {m n j k} {σ : Sub T m n} → ⌊ j ⌋≡ k → ⌊ j Kind/ σ ⌋≡ k
  ⌊⌋≡-Kind/ is-★                   = is-★
  ⌊⌋≡-Kind/ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) =
    is-⇒ (⌊⌋≡-Kind/ ⌊j₁⌋≡k₁) (⌊⌋≡-Kind/ ⌊j₂⌋≡k₂)

  ⌊⌋≡-Kind′/ : ∀ {m n j k} {σ : Sub T m n} → ⌊ j ⌋≡ k → ⌊ j Kind′/ σ ⌋≡ k
  ⌊⌋≡-Kind′/ is-★                   = is-★
  ⌊⌋≡-Kind′/ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) =
    is-⇒ (⌊⌋≡-Kind′/ ⌊j₁⌋≡k₁) (⌊⌋≡-Kind′/ ⌊j₂⌋≡k₂)

simpLemmasKind : KindSimpLemmas Term
simpLemmasKind = record
  { lemmas   = termLikeLemmasKind
  ; ⌊⌋≡-/    = KindSimpSubstApp.⌊⌋≡-Kind/
  ; ⌊⌋≡-/Var = KindSimpSubstApp.⌊⌋≡-Kind/
  }
  where open Substitution

simpLemmasKind′ : KindSimpLemmas Elim
simpLemmasKind′ = record
  { lemmas   = termLikeLemmasKind′
  ; ⌊⌋≡-/    = KindSimpSubstApp.⌊⌋≡-Kind′/
  ; ⌊⌋≡-/Var = KindSimpSubstApp.⌊⌋≡-Kind′/
  }
  where open Substitution

module SimpHSubstLemmas where
  open KindSimpLemmas simpLemmasKind′ public

  -- Kind simplification as a relation commutes with hereditary
  -- substitution.

  ⌊⌋≡-/⟨⟩ : ∀ {m n j k l} {σ : SVSub m n} → ⌊ j ⌋≡ k → ⌊ j Kind/⟨ l ⟩ σ ⌋≡ k
  ⌊⌋≡-/⟨⟩ is-★                   = is-★
  ⌊⌋≡-/⟨⟩ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) = is-⇒ (⌊⌋≡-/⟨⟩ ⌊j₁⌋≡k₁) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)

open SimpHSubstLemmas

----------------------------------------------------------------------
-- Untyped η-expansion of neutral terms.

module TrackSimpleKindsEtaExp where
  open Substitution hiding (_↑; sub)

  -- NOTE. The definition of the function η-exp in this module is
  -- structurally recursive in the *shape* parameter k, but *not* in
  -- the kind (j : Kind Elim n) because we need to weaken the domain
  -- j₁ of the dependent kind (j = Π j₁ j₂) in the arrow case.  The
  -- additional hypothesis ⌊ j ⌋≡ k ensures that k is indeed the shape
  -- of the kind j.

  -- Kind-driven untyped η-expansion of eliminations.
  --
  -- NOTE.  We only expand neutral types since these are the only
  -- non-lambda forms of arrow kind, and thus the only ones that
  -- require expansion to reach η-long β-normal forms.

  η-exp : ∀ {n k} (j : Kind Elim n) → ⌊ j ⌋≡ k → Elim n → Elim n
  η-exp (c ⋯ d)   (is-★)                 a = a
  η-exp (Π j₁ j₂) (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) a =
    Λ∙ j₁ (η-exp j₂ ⌊j₂⌋≡k₂ a·ηz)
    where
      a·ηz = weakenElim a ⌜·⌝
               η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)

  -- A helper lemma.

  η-exp-⌊⌋≡ : ∀ {n j₁ j₂ k₁ k₂} {a : Elim n}
              (hyp₁ : ⌊ j₁ ⌋≡ k₁) (hyp₂ : ⌊ j₂ ⌋≡ k₂) → j₁ ≡ j₂ → k₁ ≡ k₂ →
              η-exp j₁ hyp₁ a ≡ η-exp j₂ hyp₂ a
  η-exp-⌊⌋≡ hyp₁ hyp₂ refl refl =
    cong (λ hyp → η-exp _ hyp _) (⌊⌋≡-pirr hyp₁ hyp₂)

  -- η-expansion commutes with renaming.

  η-exp-/Var : ∀ {m n j k} (hyp : ⌊ j ⌋≡ k) a {ρ : Sub Fin m n} →
               η-exp j hyp a Elim/Var ρ ≡
                 η-exp (j Kind′/Var ρ) (⌊⌋≡-/Var hyp) (a Elim/Var ρ)
  η-exp-/Var is-★ a = refl
  η-exp-/Var (is-⇒ {j₁} {j₂} ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) a {ρ} = begin
      η-exp _ (is-⇒ ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) a Elim/Var ρ
    ≡⟨ cong (Λ∙ (j₁ Kind′/Var ρ)) (η-exp-/Var ⌊j₂⌋≡k₂ _) ⟩
      Λ∙ (j₁ Kind′/Var ρ) (η-exp (j₂ Kind′/Var ρ V.↑) (⌊⌋≡-/Var ⌊j₂⌋≡k₂)
        ((weakenElim a ⌜·⌝
          η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)) Elim/Var
            ρ V.↑))
    ≡⟨ cong (λ c → Λ∙ (j₁ Kind′/Var ρ)
                      (η-exp (j₂ Kind′/Var ρ V.↑) (⌊⌋≡-/Var ⌊j₂⌋≡k₂) c))
            (begin
                weakenElim a ⌜·⌝
                  η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)
                    Elim/Var ρ V.↑
              ≡⟨ ⌜·⌝-/Var (weakenElim a) _ ⟩
                (weakenElim a Elim/Var ρ V.↑) ⌜·⌝
                  (η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)
                    Elim/Var ρ V.↑)
              ≡⟨ cong₂ _⌜·⌝_ (sym (EVL.wk-commutes a))
                       (η-exp-/Var (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)) ⟩
                (weakenElim (a Elim/Var ρ)) ⌜·⌝
                  (η-exp (weakenKind′ j₁ Kind′/Var ρ V.↑)
                         (⌊⌋≡-/Var (⌊⌋≡-weaken ⌊j₁⌋≡k₁))
                         ((var∙ zero) Elim/Var ρ V.↑))
              ≡⟨ cong ((weakenElim (a Elim/Var ρ)) ⌜·⌝_)
                      (η-exp-⌊⌋≡ (⌊⌋≡-/Var (⌊⌋≡-weaken ⌊j₁⌋≡k₁))
                                 (⌊⌋≡-weaken (⌊⌋≡-/Var ⌊j₁⌋≡k₁))
                                 (sym (KVL.wk-commutes j₁)) refl) ⟩
                (weakenElim (a Elim/Var ρ)) ⌜·⌝
                  (η-exp (weakenKind′ (j₁ Kind′/Var ρ))
                         (⌊⌋≡-weaken (⌊⌋≡-/Var ⌊j₁⌋≡k₁))
                         (var∙ zero))
              ∎) ⟩
      η-exp _ (is-⇒ (⌊⌋≡-/Var ⌊j₁⌋≡k₁) (⌊⌋≡-/Var ⌊j₂⌋≡k₂)) (a Elim/Var ρ)
    ∎
    where
      open ≡-Reasoning
      module V  = VarSubst
      module EL = TermLikeLemmas termLikeLemmasElim
      module KL = TermLikeLemmas termLikeLemmasKind′
      module EVL = LiftAppLemmas EL.varLiftAppLemmas
      module KVL = LiftAppLemmas KL.varLiftAppLemmas

  -- η-expansion of neutrals commutes with hereditary substitutions
  -- that miss the head of the neutral.

  η-exp-ne-Miss-/⟨⟩ : ∀ {l m n j k} x y {as} {σ : SVSub m n}
                      (hyp : ⌊ j ⌋≡ k) → Miss σ x y →
                      η-exp j hyp (var x ∙ as) /⟨ l ⟩ σ  ≡
                        η-exp (j Kind/⟨ l ⟩ σ) (⌊⌋≡-/⟨⟩ hyp)
                              (var y ∙ (as //⟨ l ⟩ σ))
  η-exp-ne-Miss-/⟨⟩ x y is-★ missP = cong (_?∙∙⟨ _ ⟩ _) (lookup-Miss missP)
  η-exp-ne-Miss-/⟨⟩ {l} x y {as} {σ} (is-⇒ {j₁} {j₂} ⌊j₁⌋≡k₁ ⌊j₂⌋≡k₂) missP =
    cong (Λ∙ (j₁ Kind/⟨ l ⟩ σ)) (begin
       η-exp j₂ ⌊j₂⌋≡k₂ ((weakenElim (var x ∙ as)) ⌜·⌝ ηz) /⟨ l ⟩ σ ↑
      ≡⟨ cong (λ x → η-exp _ ⌊j₂⌋≡k₂ (var x ∙ weakenSpine as ⌜·⌝ _) /⟨ l ⟩ σ ↑)
              (VarLemmas.lookup-wk x) ⟩
       η-exp j₂ ⌊j₂⌋≡k₂ (var (suc x) ∙ (weakenSpine as) ⌜·⌝ ηz) /⟨ l ⟩ σ ↑
      ≡⟨ η-exp-ne-Miss-/⟨⟩ (suc x) (suc y) ⌊j₂⌋≡k₂ (missP ↑) ⟩
       η-exp (j₂ Kind/⟨ l ⟩ σ ↑) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (var (suc y) ∙
         (((weakenSpine as) ∷ʳ ηz) //⟨ l ⟩ σ ↑))
      ≡⟨ cong (λ bs → η-exp _ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (var _ ∙ bs))
              (++-//⟨⟩ (weakenSpine as) (_ ∷ [])) ⟩
       η-exp (j₂ Kind/⟨ l ⟩ σ ↑) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
         (var (suc y) ∙ ((weakenSpine as) //⟨ l ⟩ σ ↑) ⌜·⌝ (ηz /⟨ l ⟩ σ ↑))
      ≡⟨ cong₂ (λ a b → η-exp (j₂ Kind/⟨ l ⟩ σ ↑) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂) (a ⌜·⌝ b))
               (cong₂ (λ x as → var x ∙ as)
                      (sym (VarLemmas.lookup-wk y)) (wk-//⟨⟩-↑⋆ 0 as))
               (η-exp-ne-Miss-/⟨⟩ zero zero (⌊⌋≡-weaken ⌊j₁⌋≡k₁) under) ⟩
       η-exp (j₂ Kind/⟨ l ⟩ σ ↑) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
         (weakenElim (var y ∙ (as //⟨ l ⟩ σ)) ⌜·⌝
           η-exp ((weakenKind′ j₁) Kind/⟨ l ⟩ σ ↑)
                 (⌊⌋≡-/⟨⟩ (⌊⌋≡-weaken ⌊j₁⌋≡k₁)) (var∙ zero))
      ≡⟨ cong (λ a → η-exp _ (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
                       (weakenElim (var y ∙ (as //⟨ l ⟩ σ)) ⌜·⌝ a))
              (η-exp-⌊⌋≡ (⌊⌋≡-/⟨⟩ (⌊⌋≡-weaken ⌊j₁⌋≡k₁))
                         (⌊⌋≡-weaken (⌊⌋≡-/⟨⟩ ⌊j₁⌋≡k₁))
                         (wk-Kind/⟨⟩-↑⋆ 0 j₁) refl) ⟩
       η-exp (j₂ Kind/⟨ l ⟩ σ ↑) (⌊⌋≡-/⟨⟩ ⌊j₂⌋≡k₂)
         ((weakenElim (var y ∙ (as //⟨ l ⟩ σ))) ⌜·⌝
           η-exp (weakenKind′ (j₁ Kind/⟨ l ⟩ σ))
                 (⌊⌋≡-weaken (⌊⌋≡-/⟨⟩ ⌊j₁⌋≡k₁)) (var∙ zero))
      ∎)
      where
        open ≡-Reasoning
        open RenamingCommutes
        ηz = η-exp (weakenKind′ j₁) (⌊⌋≡-weaken ⌊j₁⌋≡k₁) (var∙ zero)

private module TK = TrackSimpleKindsEtaExp

-- Kind-driven untyped η-expansion.

η-exp : ∀ {n} → Kind Elim n → Elim n → Elim n
η-exp k a = TK.η-exp k (⌊⌋-⌊⌋≡ k) a

module _ where
  open Substitution
  open ≡-Reasoning

  -- η-expansion commutes with renaming.

  η-exp-/Var : ∀ {m n} k a {ρ : Sub Fin m n} →
               η-exp k a Elim/Var ρ ≡ η-exp (k Kind′/Var ρ) (a Elim/Var ρ)
  η-exp-/Var k a {ρ} = begin
      η-exp k a Elim/Var ρ
    ≡⟨ TK.η-exp-/Var (⌊⌋-⌊⌋≡ k) a ⟩
      TK.η-exp (k Kind′/Var ρ) (⌊⌋≡-/Var (⌊⌋-⌊⌋≡ k)) (a Elim/Var ρ)
    ≡⟨ TK.η-exp-⌊⌋≡ (⌊⌋≡-/Var (⌊⌋-⌊⌋≡ k)) (⌊⌋-⌊⌋≡ (k Kind′/Var ρ))
                    refl (sym (⌊⌋-Kind′/Var k)) ⟩
      η-exp (k Kind′/Var ρ) (a Elim/Var ρ)
    ∎

  -- A corollary: η-expansion commutes with weakening.

  η-exp-weaken : ∀ {n} k (a : Elim n) →
                 weakenElim (η-exp k a) ≡ η-exp (weakenKind′ k) (weakenElim a)
  η-exp-weaken k a = η-exp-/Var k a

  -- η-expansion of neutrals commutes with hereditary substitutions
  -- that miss the head of the neutral.

  η-exp-ne-Miss-/⟨⟩ : ∀ {l m n} x y as k {σ : SVSub m n} → Miss σ x y →
                      η-exp k (var x ∙ as) /⟨ l ⟩ σ  ≡
                        η-exp (k Kind/⟨ l ⟩ σ) (var y ∙ (as //⟨ l ⟩ σ))
  η-exp-ne-Miss-/⟨⟩ {l} x y as k {σ} missP = begin
      η-exp k (var x ∙ as) /⟨ l ⟩ σ
    ≡⟨ TK.η-exp-ne-Miss-/⟨⟩ x y (⌊⌋-⌊⌋≡ k) missP ⟩
      TK.η-exp (k Kind/⟨ l ⟩ σ) (⌊⌋≡-/⟨⟩ (⌊⌋-⌊⌋≡ k)) (var y ∙ (as //⟨ l ⟩ σ))
    ≡⟨ TK.η-exp-⌊⌋≡ (⌊⌋≡-/⟨⟩ (⌊⌋-⌊⌋≡ k)) (⌊⌋-⌊⌋≡ (k Kind/⟨ l ⟩ σ)) refl
                    (sym (⌊⌋-Kind/⟨⟩ k)) ⟩
      η-exp (k Kind/⟨ l ⟩ σ) (var y ∙ (as //⟨ l ⟩ σ))
    ∎

----------------------------------------------------------------------
-- Untyped normalization.

open ElimCtx

-- Normalize an raw type or kind into η-long β-normal form if
-- possible.  Degenerate cases are marked "!".

mutual

  nf : ∀ {n} → Ctx n → Term n → Elim n
  nf Γ (var x) with lookup Γ x
  nf Γ (var x) | kd k = η-exp k (var∙ x)
  nf Γ (var x) | tp a = var∙ x                    -- ! a not a kind
  nf Γ ⊥       = ⊥∙
  nf Γ ⊤       = ⊤∙
  nf Γ (Π k a) = let k′ = nfKind Γ k in ∀∙ k′ (nf (kd k′ ∷ Γ) a)
  nf Γ (a ⇒ b) = (nf Γ a ⇒ nf Γ b) ∙ []
  nf Γ (Λ k a) = let k′ = nfKind Γ k in Λ∙ k′ (nf (kd k′ ∷ Γ) a)
  nf Γ (ƛ a b) = ƛ∙ ⌜ a ⌝ ⌜ b ⌝                   -- ! ƛ a b not a type
  nf Γ (a · b) = nf Γ a ↓⌜·⌝ nf Γ b
  nf Γ (a ⊡ b) = ⌜ a ⌝ ⊡∙ ⌜ b ⌝                   -- ! a ⊡ b not a type

  nfKind : ∀ {n} → Ctx n → Kind Term n → Kind Elim n
  nfKind Γ (a ⋯ b) = nf Γ a ⋯ nf Γ b
  nfKind Γ (Π j k) = let j′ = nfKind Γ j in Π j′ (nfKind (kd j′ ∷ Γ) k)

-- Normalization extended to contexts.

nfAsc : ∀ {n} → Ctx n → TermAsc n → ElimAsc n
nfAsc Γ (kd k) = kd (nfKind Γ k)
nfAsc Γ (tp a) = tp (nf Γ a)

nfCtx : ∀ {n} → TermCtx.Ctx n → Ctx n
nfCtx []      = []
nfCtx (a ∷ Γ) = let Γ′ = nfCtx Γ in nfAsc Γ′ a ∷ Γ′

nfCtxExt : ∀ {m n} → Ctx m → TermCtx.CtxExt m n → CtxExt m n
nfCtxExt Γ []      = []
nfCtxExt Γ (a ∷ Δ) = let Δ′ = nfCtxExt Γ Δ in nfAsc (Δ′ ++ Γ) a ∷ Δ′

-- Shapes are stable w.r.t. normalization.

⌊⌋-nf : ∀ {n} {Γ : Ctx n} k → ⌊ nfKind Γ k ⌋ ≡ ⌊ k ⌋
⌊⌋-nf (a ⋯ b) = refl
⌊⌋-nf (Π j k) = cong₂ _⇒_ (⌊⌋-nf j) (⌊⌋-nf k)

open SimpleCtx using (⌊_⌋Asc; kd; tp)
open ContextConversions using (⌊_⌋Ctx)

-- Simple contexts are stable w.r.t. normalization.

⌊⌋Asc-nf : ∀ {n} {Γ : Ctx n} a → ⌊ nfAsc Γ a ⌋Asc ≡ ⌊ a ⌋Asc
⌊⌋Asc-nf (kd k) = cong kd (⌊⌋-nf k)
⌊⌋Asc-nf (tp a) = refl

⌊⌋Ctx-nf : ∀ {n} (Γ : TermCtx.Ctx n) → ⌊ nfCtx Γ ⌋Ctx ≡ ⌊ Γ ⌋Ctx
⌊⌋Ctx-nf []      = refl
⌊⌋Ctx-nf (a ∷ Γ) = cong₂ _∷_ (⌊⌋Asc-nf a) (⌊⌋Ctx-nf Γ)

-- Normalization commutes with context concatenation.

nf-++ : ∀ {m n} (Δ : TermCtx.CtxExt m n) Γ →
        nfCtx (Δ ++ Γ) ≡ nfCtxExt (nfCtx Γ) Δ ++ nfCtx Γ
nf-++ []      Γ = refl
nf-++ (a ∷ Δ) Γ = cong₂ _∷_ (cong (λ Δ → nfAsc Δ a) (nf-++ Δ Γ)) (nf-++ Δ Γ)

-- A helper lemma about normalization of variables.

nf-var-kd : ∀ {n} (Γ : Ctx n) {k} x →
            lookup Γ x ≡ kd k → nf Γ (var x) ≡ η-exp k (var∙ x)
nf-var-kd Γ x Γ[x]≡kd-k with lookup Γ x
nf-var-kd Γ x refl | kd k = refl
nf-var-kd Γ x ()   | tp _

module RenamingCommutesNorm where
  open Substitution hiding (subst; varLiftAppLemmas)
  open TermLikeLemmas termLikeLemmasElimAsc
    using (varApplication; varLiftAppLemmas)
  open RenamingCommutes
  open ⊤-WellFormed weakenOps
  open ≡-Reasoning

  private
    module V  = VarSubst
    module AL = LiftAppLemmas varLiftAppLemmas

  -- Well-formed renamings.
  --
  -- A renaming `ρ' is well-formed `Δ ⊢/ ρ ∈ Γ' if it maps ascriptions
  -- from the source contxt `Γ' to the target context `Δ' in a manner
  -- that is consistent with the renaming, i.e. such that we have
  -- `Δ(ρ(x)) = Γ(x)ρ'.

  kindedVarSubst : TypedVarSubst ElimAsc _
  kindedVarSubst = record
    { _⊢_wf              = _⊢_wf
    ; typeExtension      = weakenOps
    ; typeVarApplication = varApplication
    ; wf-wf              = λ _ → ctx-wf _
    ; /-wk               = refl
    ; id-vanishes        = AL.id-vanishes
    ; /-⊙                = AL./-⊙
    }
  open TypedVarSubst kindedVarSubst renaming (lookup to /∈-lookup)

  -- Extract a "consistency" proof from a well-formed renaming, i.e. a
  -- proof that `Δ(ρ(x)) = Γ(x)ρ'.

  lookup-≡ : ∀ {m n Δ Γ} {ρ : Sub Fin m n} → Δ ⊢/Var ρ ∈ Γ → ∀ x →
             lookup Δ (Vec.lookup ρ x) ≡ lookup Γ x ElimAsc/Var ρ
  lookup-≡ {_} {_} {Δ} {Γ} {ρ} ρ∈Γ x
    with Vec.lookup ρ x | lookup Γ x ElimAsc/Var ρ | /∈-lookup ρ∈Γ x
  lookup-≡ ρ∈Γ x | y | _ | VarTyping.∈-var .y _ = refl

  mutual

    -- A helper.

    ∈-↑′ : ∀ {m n Δ Γ} {ρ : Sub Fin m n} k → Δ ⊢/Var ρ ∈ Γ →
           kd (nfKind Δ (k Kind/Var ρ)) ∷ Δ ⊢/Var ρ V.↑ ∈ (nfAsc Γ (kd k) ∷ Γ)
    ∈-↑′ k ρ∈Γ =
      subst (λ k → kd k ∷ _ ⊢/Var _ ∈ _) (nfKind-/Var k ρ∈Γ) (∈-↑ _ ρ∈Γ)

    -- Normalization commutes with renaming.

    nf-/Var : ∀ {m n Δ Γ} {ρ : Sub Fin m n} a → Δ ⊢/Var ρ ∈ Γ →
              nf Γ a Elim/Var ρ ≡ nf Δ (a /Var ρ)
    nf-/Var {_} {_} {Δ} {Γ} {ρ} (var x) ρ∈Γ
      with lookup Γ x | lookup Δ (Vec.lookup ρ x) | lookup-≡ ρ∈Γ x
    nf-/Var (var x) ρ∈Γ | kd k | _ | refl = η-exp-/Var k (var∙ x)
    nf-/Var (var x) ρ∈Γ | tp a | _ | refl = refl
    nf-/Var ⊥       ρ∈Γ = refl
    nf-/Var ⊤       ρ∈Γ = refl
    nf-/Var (Π k a) ρ∈Γ = cong₂ ∀∙ (nfKind-/Var k ρ∈Γ) (nf-/Var a (∈-↑′ k ρ∈Γ))
    nf-/Var (a ⇒ b) ρ∈Γ = cong₂ _⇒∙_ (nf-/Var a ρ∈Γ) (nf-/Var b ρ∈Γ)
    nf-/Var (Λ j a) ρ∈Γ = cong₂ Λ∙ (nfKind-/Var j ρ∈Γ) (nf-/Var a (∈-↑′ j ρ∈Γ))
    nf-/Var (ƛ a b) ρ∈Γ = cong₂ ƛ∙ (sym (⌜⌝-/Var a)) (sym (⌜⌝-/Var b))
    nf-/Var {m} {_} {Δ} {Γ} {ρ} (a · b) ρ∈Γ = begin
        (nf Γ a ↓⌜·⌝ nf Γ b) Elim/Var ρ
      ≡⟨ ↓⌜·⌝-/Var (nf Γ a) (nf Γ b) ⟩
        (nf Γ a Elim/Var ρ) ↓⌜·⌝ (nf Γ b Elim/Var ρ)
      ≡⟨ cong₂ (_↓⌜·⌝_) (nf-/Var a ρ∈Γ) (nf-/Var b ρ∈Γ) ⟩
        nf Δ (a · b /Var ρ)
      ∎
    nf-/Var (a ⊡ b) ρ∈Γ = cong₂ _⊡∙_ (sym (⌜⌝-/Var a)) (sym (⌜⌝-/Var b))

    nfKind-/Var : ∀ {m n Δ Γ} {ρ : Sub Fin m n} k → Δ ⊢/Var ρ ∈ Γ →
                  nfKind Γ k Kind′/Var ρ ≡ nfKind Δ (k Kind/Var ρ)
    nfKind-/Var (a ⋯ b) ρ∈Γ = cong₂ _⋯_ (nf-/Var a ρ∈Γ) (nf-/Var b ρ∈Γ)
    nfKind-/Var (Π j k) ρ∈Γ =
      cong₂ Π (nfKind-/Var j ρ∈Γ) (nfKind-/Var k (∈-↑′ j ρ∈Γ))

  -- Normalization of ascriptions commutes with renaming.

  nfAsc-/Var : ∀ {m n Δ Γ} {ρ : Sub Fin m n} a → Δ ⊢/Var ρ ∈ Γ →
               nfAsc Γ a ElimAsc/Var ρ ≡ nfAsc Δ (a TermAsc/Var ρ)
  nfAsc-/Var (kd k) ρ∈Γ = cong kd (nfKind-/Var k ρ∈Γ)
  nfAsc-/Var (tp a) ρ∈Γ = cong tp (nf-/Var a ρ∈Γ)

  -- Corollaries: normalization commutes with weakening.

  nf-weaken : ∀ {n} {Γ : Ctx n} a b →
              weakenElim (nf Γ b) ≡ nf (a ∷ Γ) (weaken b)
  nf-weaken a b = nf-/Var b (∈-wk _)

  nfKind-weaken : ∀ {n} {Γ : Ctx n} a k →
                  weakenKind′ (nfKind Γ k) ≡ nfKind (a ∷ Γ) (weakenKind k)
  nfKind-weaken a k = nfKind-/Var k (∈-wk _)

  nfAsc-weaken : ∀ {n} {Γ : Ctx n} a b →
                 weakenElimAsc (nfAsc Γ b) ≡ nfAsc (a ∷ Γ) (weakenTermAsc b)
  nfAsc-weaken a b = nfAsc-/Var b (∈-wk _)

open RenamingCommutesNorm

module _ where
  open Substitution hiding (sub; _↑; subst)
  open ≡-Reasoning
  open VecProps using (map-cong; map-∘)

  -- Normalization extended to single-variable substitutions

  nfSVSub : ∀ {m n} → Ctx n → SVSub m n → SVSub m n
  nfSVSub      Γ  (sub a) = sub (nf Γ (⌞ a ⌟))
  nfSVSub (_ ∷ Γ) (σ ↑)   = (nfSVSub Γ σ) ↑

  nf-Hit : ∀ {m n} Γ {σ : SVSub m n} {x a} → Hit σ x a →
           Hit (nfSVSub Γ σ) x (nf Γ ⌞ a ⌟)
  nf-Hit      Γ        here                  = here
  nf-Hit (a ∷ Γ) {σ ↑} (_↑ {x = x} {b} hitP) =
    subst (Hit (nfSVSub Γ σ ↑) (suc x))
          (trans (nf-weaken a ⌞ b ⌟) (cong (nf _) (sym (⌞⌟-/Var b))))
          (nf-Hit Γ hitP ↑)

  nf-Miss : ∀ {m n} Γ {σ : SVSub m n} {x y} → Miss σ x y → Miss (nfSVSub Γ σ) x y
  nf-Miss      Γ  over      = over
  nf-Miss (a ∷ Γ) under     = under
  nf-Miss (a ∷ Γ) (missP ↑) = (nf-Miss Γ missP) ↑

  -- Normalization commutes conversion from context to vector representation.

  nfCtx-toVec : ∀ {n} (Γ : TermCtx.Ctx n) →
                toVec (nfCtx Γ) ≡ Vec.map (nfAsc (nfCtx Γ)) (TermCtx.toVec Γ)
  nfCtx-toVec []      = refl
  nfCtx-toVec (a ∷ Γ) =
    cong₂ _∷_ (nfAsc-weaken (nfAsc (nfCtx Γ) a) a) (begin
        Vec.map weakenElimAsc (toVec (nfCtx Γ))
      ≡⟨ cong (Vec.map weakenElimAsc) (nfCtx-toVec Γ) ⟩
        Vec.map weakenElimAsc (Vec.map (nfAsc (nfCtx Γ)) (TermCtx.toVec Γ))
      ≡⟨ sym (map-∘ weakenElimAsc (nfAsc (nfCtx Γ)) (TermCtx.toVec Γ)) ⟩
        Vec.map (weakenElimAsc ∘ nfAsc (nfCtx Γ)) (TermCtx.toVec Γ)
      ≡⟨ map-cong (nfAsc-weaken (nfAsc (nfCtx Γ) a)) (TermCtx.toVec Γ) ⟩
        Vec.map (nfAsc (nfCtx (a ∷ Γ)) ∘ weakenTermAsc) (TermCtx.toVec Γ)
      ≡⟨ map-∘ (nfAsc (nfCtx (a ∷ Γ))) weakenTermAsc (TermCtx.toVec Γ) ⟩
        Vec.map (nfAsc (nfCtx (a ∷ Γ)))
                (Vec.map weakenTermAsc (TermCtx.toVec Γ))
      ∎)

  -- Normalization commutes with context lookup.

  nfCtx-lookup : ∀ {n} (Γ : TermCtx.Ctx n) x →
                 lookup (nfCtx Γ) x ≡ nfAsc (nfCtx Γ) (TermCtx.lookup Γ x)
  nfCtx-lookup Γ x = begin
      lookup (nfCtx Γ) x
    ≡⟨ cong (flip Vec.lookup x) (nfCtx-toVec Γ) ⟩
      Vec.lookup (Vec.map (nfAsc (nfCtx Γ)) (TermCtx.toVec Γ)) x
    ≡⟨ VecProps.lookup-map x _ (TermCtx.toVec Γ) ⟩
      nfAsc (nfCtx Γ) (TermCtx.lookup Γ x)
    ∎

  -- A corollary of the above (specialized for type variable lookup).

  nfCtx-lookup-kd : ∀ {n k} x (Γ : TermCtx.Ctx n) → TermCtx.lookup Γ x ≡ kd k →
                    lookup (nfCtx Γ) x ≡ kd (nfKind (nfCtx Γ) k)
  nfCtx-lookup-kd x Γ Γ[x]≡kd-k with TermCtx.lookup Γ x | nfCtx-lookup Γ x
  nfCtx-lookup-kd x Γ refl | kd k | nf-Γ[x]≡kd-nf-k = nf-Γ[x]≡kd-nf-k
  nfCtx-lookup-kd x Γ ()   | tp t | _

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
------------------------------------------------------------------------------
-- Inductive PA properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module PA.Inductive.PropertiesATP where

open import PA.Inductive.Base

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

+-rightIdentity : ∀ n → n + zero ≡ n
+-rightIdentity zero     = refl
+-rightIdentity (succ n) = prf (+-rightIdentity n)
  where postulate prf : n + zero ≡ n → succ n + zero ≡ succ n
        -- TODO (21 November 2014). See Apia issue 16
        -- {-# ATP prove prf #-}

x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)
x+Sy≡S[x+y] zero     _ = refl
x+Sy≡S[x+y] (succ m) n = prf (x+Sy≡S[x+y] m n)
  where postulate prf : m + succ n ≡ succ (m + n) →
                        succ m + succ n ≡ succ (succ m + n)
        -- TODO (21 November 2014). See Apia issue 16
        -- {-# ATP prove prf #-}

+-comm : ∀ m n → m + n ≡ n + m
+-comm zero     n = sym (+-rightIdentity n)
+-comm (succ m) n = prf (+-comm m n)
  where postulate prf : m + n ≡ n + m → succ m + n ≡ n + succ m
        -- TODO (21 November 2014). See Apia issue 16
        -- {-# ATP prove prf x+Sy≡S[x+y] #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module WithApp where

f
  : {A : Set}
  → A
  → A
f x
  with x
... | y
  = y

g
  : {A : Set}
  → A
  → A
  → A
g x y
  with x
... | _
  with y
... | _
  = x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
open import Data.Product using ( ∃ ; _×_ )
open import FRP.LTL.RSet.Core using ( RSet ; _[_,_] ; ⟦_⟧ )
open import FRP.LTL.RSet.Stateless using ( _⇒_ )
open import FRP.LTL.RSet.Globally using ( □ ; [_] )
open import FRP.LTL.Time using ( _≤_ ; ≤-refl ; _≤-trans_ )

module FRP.LTL.RSet.Causal where

infixr 2 _⊵_
infixr 3 _⋙_

-- A ⊵ B is the causal function space from A to B

_⊵_ : RSet → RSet → RSet
(A ⊵ B) t = ∀ {u} → (t ≤ u) → (A [ t , u ]) → B u

-- Categorical structure

arr : ∀ {A B} → ⟦ □ (A ⇒ B) ⇒ (A ⊵ B) ⟧
arr f s≤t σ = f s≤t (σ s≤t ≤-refl)

identity : ∀ {A} → ⟦ A ⊵ A ⟧
identity {A} = arr [( λ {u} (a : A u) → a )]

_before_ : ∀ {A s u v} → (A [ s , v ]) → (u ≤ v) → (A [ s , u ])
(σ before u≤v) s≤t t≤u = σ s≤t (t≤u ≤-trans u≤v)

_after_ : ∀ {A s t v} → (A [ s , v ]) → (s ≤ t) → (A [ t , v ])
(σ after s≤t) t≤u u≤v = σ (s≤t ≤-trans t≤u) u≤v

_$_ : ∀ {A B s u} → (A ⊵ B) s → (A [ s , u ]) → (B [ s , u ])
(f $ σ) s≤t t≤u = f s≤t (σ before t≤u)

_⋙_ : ∀ {A B C} → ⟦ (A ⊵ B) ⇒ (B ⊵ C) ⇒ (A ⊵ C) ⟧
(f ⋙ g) s≤t σ = g s≤t (f $ σ)

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module STLC.Kovacs.Embedding where

open import STLC.Syntax public
open import Category

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

-- Embeddings (OPE ; ∙ ; drop ; keep)
infix 4 _⊇_
data _⊇_ : 𝒞 → 𝒞 → Set
  where
    done  : ∅ ⊇ ∅

    wkₑ   : ∀ {Γ Γ′ A} → (η : Γ′ ⊇ Γ)
                       → Γ′ , A ⊇ Γ

    liftₑ : ∀ {Γ Γ′ A} → (η : Γ′ ⊇ Γ)
                       → Γ′ , A ⊇ Γ , A

idₑ : ∀ {Γ} → Γ ⊇ Γ
idₑ {∅}     = done
idₑ {Γ , A} = liftₑ idₑ

-- (_∘ₑ_)
_○_ : ∀ {Γ Γ′ Γ″} → Γ′ ⊇ Γ → Γ″ ⊇ Γ′ → Γ″ ⊇ Γ
η₂       ○ done     = η₂
η₂       ○ wkₑ η₁   = wkₑ (η₂ ○ η₁)
wkₑ η₂   ○ liftₑ η₁ = wkₑ (η₂ ○ η₁)
liftₑ η₂ ○ liftₑ η₁ = liftₑ (η₂ ○ η₁)

-- (idlₑ)
lid○ : ∀ {Γ Γ′} → (η : Γ′ ⊇ Γ)
                → idₑ ○ η ≡ η
lid○ done      = refl
lid○ (wkₑ η)   = wkₑ & lid○ η
lid○ (liftₑ η) = liftₑ & lid○ η

-- (idrₑ)
rid○ : ∀ {Γ Γ′} → (η : Γ′ ⊇ Γ)
                → η ○ idₑ ≡ η
rid○ done      = refl
rid○ (wkₑ η)   = wkₑ & rid○ η
rid○ (liftₑ η) = liftₑ & rid○ η

-- (assₑ)
assoc○ : ∀ {Γ Γ′ Γ″ Γ‴} → (η₁ : Γ‴ ⊇ Γ″) (η₂ : Γ″ ⊇ Γ′) (η₃ : Γ′ ⊇ Γ)
                        → (η₃ ○ η₂) ○ η₁ ≡ η₃ ○ (η₂ ○ η₁)
assoc○ done       η₂         η₃         = refl
assoc○ (wkₑ η₁)   η₂         η₃         = wkₑ & assoc○ η₁ η₂ η₃
assoc○ (liftₑ η₁) (wkₑ η₂)   η₃         = wkₑ & assoc○ η₁ η₂ η₃
assoc○ (liftₑ η₁) (liftₑ η₂) (wkₑ η₃)   = wkₑ & assoc○ η₁ η₂ η₃
assoc○ (liftₑ η₁) (liftₑ η₂) (liftₑ η₃) = liftₑ & assoc○ η₁ η₂ η₃

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

-- (∈ₑ)
getₑ : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → Γ ∋ A → Γ′ ∋ A
getₑ done      i       = i
getₑ (wkₑ η)   i       = suc (getₑ η i)
getₑ (liftₑ η) zero    = zero
getₑ (liftₑ η) (suc i) = suc (getₑ η i)

-- (∈-idₑ)
idgetₑ : ∀ {Γ A} → (i : Γ ∋ A)
                 → getₑ idₑ i ≡ i
idgetₑ zero    = refl
idgetₑ (suc i) = suc & idgetₑ i

-- (∈-∘ₑ)
get○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (i : Γ ∋ A)
                     → getₑ (η₂ ○ η₁) i ≡ (getₑ η₁ ∘ getₑ η₂) i
get○ done       done       ()
get○ (wkₑ η₁)   η₂         i       = suc & get○ η₁ η₂ i
get○ (liftₑ η₁) (wkₑ η₂)   i       = suc & get○ η₁ η₂ i
get○ (liftₑ η₁) (liftₑ η₂) zero    = refl
get○ (liftₑ η₁) (liftₑ η₂) (suc i) = suc & get○ η₁ η₂ i

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

-- (Tmₑ)
ren : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → Γ ⊢ A → Γ′ ⊢ A
ren η (𝓋 i)   = 𝓋 (getₑ η i)
ren η (ƛ M)   = ƛ (ren (liftₑ η) M)
ren η (M ∙ N) = ren η M ∙ ren η N

wk : ∀ {B Γ A} → Γ ⊢ A → Γ , B ⊢ A
wk M = ren (wkₑ idₑ) M

-- (Tm-idₑ)
idren : ∀ {Γ A} → (M : Γ ⊢ A)
                → ren idₑ M ≡ M
idren (𝓋 i)   = 𝓋 & idgetₑ i
idren (ƛ M)   = ƛ & idren M
idren (M ∙ N) = _∙_ & idren M
                    ⊗ idren N

-- (Tm-∘ₑ)
ren○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ⊇ Γ′) (η₂ : Γ′ ⊇ Γ) (M : Γ ⊢ A)
                     → ren (η₂ ○ η₁) M ≡ (ren η₁ ∘ ren η₂) M
ren○ η₁ η₂ (𝓋 i)   = 𝓋 & get○ η₁ η₂ i
ren○ η₁ η₂ (ƛ M)   = ƛ & ren○ (liftₑ η₁) (liftₑ η₂) M
ren○ η₁ η₂ (M ∙ N) = _∙_ & ren○ η₁ η₂ M
                         ⊗ ren○ η₁ η₂ N

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

𝗢𝗣𝗘 : Category 𝒞 _⊇_
𝗢𝗣𝗘 =
  record
    { idₓ    = idₑ
    ; _⋄_    = _○_
    ; lid⋄   = lid○
    ; rid⋄   = rid○
    ; assoc⋄ = assoc○
    }

getₑPsh : 𝒯 → Presheaf₀ 𝗢𝗣𝗘
getₑPsh A =
  record
    { Fₓ  = _∋ A
    ; F   = getₑ
    ; idF = fext! idgetₑ
    ; F⋄  = λ η₁ η₂ → fext! (get○ η₂ η₁)
    }

renPsh : 𝒯 → Presheaf₀ 𝗢𝗣𝗘
renPsh A =
  record
    { Fₓ  = _⊢ A
    ; F   = ren
    ; idF = fext! idren
    ; F⋄  = λ η₁ η₂ → fext! (ren○ η₂ η₁)
    }

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
module Prelude.Functor where

open import Agda.Primitive
open import Prelude.Function
open import Prelude.Equality

record Functor {a b} (F : Set a → Set b) : Set (lsuc a ⊔ b) where
  infixl 4 _<$>_ _<$_
  field
    fmap : ∀ {A B} → (A → B) → F A → F B
  _<$>_ = fmap

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ m = fmap (const x) m

open Functor {{...}} public

{-# DISPLAY Functor.fmap  _ = fmap  #-}
{-# DISPLAY Functor._<$>_ _ = _<$>_ #-}
{-# DISPLAY Functor._<$_  _ = _<$_  #-}

-- Level polymorphic functors
record Functor′ {a b} (F : ∀ {a} → Set a → Set a) : Set (lsuc (a ⊔ b)) where
  infixl 4 _<$>′_ _<$′_
  field
    fmap′ : {A : Set a} {B : Set b} → (A → B) → F A → F B
  _<$>′_ = fmap′

  _<$′_ : {A : Set a} {B : Set b} → B → F A → F B
  x <$′ m = fmap′ (const x) m

open Functor′ {{...}} public

infixr 0 flip-fmap
syntax flip-fmap a (λ x → y) = for x ← a return y
flip-fmap : ∀ {a b} {F : Set a → Set b} {{_ : Functor F}} {A B} → F A → (A → B) → F B
flip-fmap x f = fmap f x

infixr 0 caseF_of_
caseF_of_ : ∀ {a b} {F : Set a → Set b} {{_ : Functor F}} {A B} → F A → (A → B) → F B
caseF_of_ x f = fmap f x

for = caseF_of_

{-# INLINE for #-}
{-# INLINE caseF_of_ #-}

-- Congruence for _<$>_ --

infixl 4 _=$=_ _=$=′_
_=$=_ : ∀ {a b} {A B : Set a} {F : Set a → Set b} {{_ : Functor F}} {x y : F A}
          (f : A → B) → x ≡ y → (f <$> x) ≡ (f <$> y)
f =$= refl = refl

_=$=′_ : ∀ {a b} {A : Set a} {B : Set b} {F : ∀ {a} → Set a → Set a} {{_ : Functor′ F}} {x y : F A}
          (f : A → B) → x ≡ y → (f <$>′ x) ≡ (f <$>′ y)
f =$=′ refl = refl

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module Cats.Util.Logic.Classical where

open import Cats.Util.Logic.Constructive public

-- (Strong) law of the excluded middle
postulate lem : ∀ {p} (P : Set p) → P ∨ ¬ P

-- Double negation elimination
¬¬-elim : ∀ {p} {P : Set p} → ¬ ¬ P → P
¬¬-elim {P = P} ¬¬p with lem P
... | ∨-introl  p = p
... | ∨-intror ¬p = ⊥-elim (¬¬p ¬p)

-- Contrapositive
contrapositive : ∀ {p q} {P : Set p} {Q : Set q}
  → (¬ Q → ¬ P) → P → Q
contrapositive {P = P} {Q} contra p with lem Q
... | ∨-introl q = q
... | ∨-intror ¬q = ⊥-elim (contra ¬q p)

-- De Morgan's nonconstructive rule
¬∧→¬∨¬ : ∀ {p q} {P : Set p} {Q : Set q}
  → ¬ (P ∧ Q) → ¬ P ∨ ¬ Q
¬∧→¬∨¬ {P = P} {Q} ¬p∧q with lem P | lem Q
... | ∨-introl p  | ∨-introl q  = ⊥-elim (¬p∧q (p , q))
... | ∨-introl _  | ∨-intror ¬q = ∨-intror ¬q
... | ∨-intror ¬p | _           = ∨-introl ¬p

-- Negation and ∀
¬∀→∃¬ : ∀ {u p} {U : Set u} {P : U → Set p}
  → ¬ (∀ u → P u) → ∃[ u ] (¬ P u)
¬∀→∃¬ ¬∀ = ¬¬-elim (λ ¬∃¬ → ¬∀ (λ u → ¬¬-elim (λ pu → ¬∃¬ (u , pu))))

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finding the maximum/minimum values in a list
------------------------------------------------------------------------

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

open import Relation.Binary using (TotalOrder; Setoid)

module Data.List.Extrema
  {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where

import Algebra.Construct.NaturalChoice.Min as Min
import Algebra.Construct.NaturalChoice.Max as Max
open import Data.List.Base using (List; foldr)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_; lookup; map; tabulate)
open import Data.List.Membership.Propositional using (_∈_; lose)
open import Data.List.Membership.Propositional.Properties
  using (foldr-selective)
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
open import Data.List.Properties
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function using (id; flip; _on_)
open import Level using (Level)
open import Relation.Unary using (Pred)
import Relation.Binary.Construct.NonStrictToStrict as NonStrictToStrict
open import Relation.Binary.PropositionalEquality
  using (_≡_; sym; subst) renaming (refl to ≡-refl)
import Relation.Binary.Construct.On as On

------------------------------------------------------------------------------
-- Setup

open TotalOrder totalOrder renaming (Carrier to B)
open NonStrictToStrict _≈_ _≤_ using (_<_)
open import Data.List.Extrema.Core totalOrder
  renaming (⊓ᴸ to ⊓-lift; ⊔ᴸ to ⊔-lift)

private
  variable
    a p : Level
    A : Set a

------------------------------------------------------------------------------
-- Functions

argmin : (A → B) → A → List A → A
argmin f = foldr (⊓-lift f)

argmax : (A → B) → A → List A → A
argmax f = foldr (⊔-lift f)

min : B → List B → B
min = argmin id

max : B → List B → B
max = argmax id

------------------------------------------------------------------------------
-- Properties of argmin

module _ {f : A → B} where

  f[argmin]≤v⁺ : ∀ {v} ⊤ xs → (f ⊤ ≤ v) ⊎ (Any (λ x → f x ≤ v) xs) →
                f (argmin f ⊤ xs) ≤ v
  f[argmin]≤v⁺ = foldr-preservesᵒ (⊓ᴸ-presᵒ-≤v f)

  f[argmin]<v⁺ : ∀ {v} ⊤ xs → (f ⊤ < v) ⊎ (Any (λ x → f x < v) xs) →
                f (argmin f ⊤ xs) < v
  f[argmin]<v⁺ = foldr-preservesᵒ (⊓ᴸ-presᵒ-<v f)

  v≤f[argmin]⁺ : ∀ {v ⊤ xs} → v ≤ f ⊤ → All (λ x → v ≤ f x) xs →
                v ≤ f (argmin f ⊤ xs)
  v≤f[argmin]⁺ = foldr-preservesᵇ (⊓ᴸ-presᵇ-v≤ f)

  v<f[argmin]⁺ : ∀ {v ⊤ xs} → v < f ⊤ → All (λ x → v < f x) xs →
                v < f (argmin f ⊤ xs)
  v<f[argmin]⁺ = foldr-preservesᵇ (⊓ᴸ-presᵇ-v< f)

  f[argmin]≤f[⊤] : ∀ ⊤ xs → f (argmin f ⊤ xs) ≤ f ⊤
  f[argmin]≤f[⊤] ⊤ xs = f[argmin]≤v⁺ ⊤ xs (inj₁ refl)

  f[argmin]≤f[xs] : ∀ ⊤ xs → All (λ x → f (argmin f ⊤ xs) ≤ f x) xs
  f[argmin]≤f[xs] ⊤ xs = foldr-forcesᵇ (⊓ᴸ-forcesᵇ-v≤ f) ⊤ xs refl

  f[argmin]≈f[v]⁺ : ∀ {v ⊤ xs} → v ∈ xs → All (λ x → f v ≤ f x) xs → f v ≤ f ⊤ →
                    f (argmin f ⊤ xs) ≈ f v
  f[argmin]≈f[v]⁺ v∈xs fv≤fxs fv≤f⊤ = antisym
    (f[argmin]≤v⁺ _ _ (inj₂ (lose v∈xs refl)))
    (v≤f[argmin]⁺ fv≤f⊤ fv≤fxs)

argmin[xs]≤argmin[ys]⁺ : ∀ {f g : A → B} ⊤₁ {⊤₂} xs {ys : List A} →
                        (f ⊤₁ ≤ g ⊤₂) ⊎ Any (λ x → f x ≤ g ⊤₂) xs →
                        All (λ y → (f ⊤₁ ≤ g y) ⊎ Any (λ x → f x ≤ g y) xs) ys →
                        f (argmin f ⊤₁ xs) ≤ g (argmin g ⊤₂ ys)
argmin[xs]≤argmin[ys]⁺ ⊤₁ xs xs≤⊤₂ xs≤ys =
  v≤f[argmin]⁺ (f[argmin]≤v⁺ ⊤₁ _ xs≤⊤₂) (map (f[argmin]≤v⁺ ⊤₁ xs) xs≤ys)

argmin[xs]<argmin[ys]⁺ : ∀ {f g : A → B} ⊤₁ {⊤₂} xs {ys : List A} →
                        (f ⊤₁ < g ⊤₂) ⊎ Any (λ x → f x < g ⊤₂) xs →
                        All (λ y → (f ⊤₁ < g y) ⊎ Any (λ x → f x < g y) xs) ys →
                        f (argmin f ⊤₁ xs) < g (argmin g ⊤₂ ys)
argmin[xs]<argmin[ys]⁺ ⊤₁ xs xs<⊤₂ xs<ys =
  v<f[argmin]⁺ (f[argmin]<v⁺ ⊤₁ _ xs<⊤₂) (map (f[argmin]<v⁺ ⊤₁ xs) xs<ys)

argmin-sel : ∀ (f : A → B) ⊤ xs → (argmin f ⊤ xs ≡ ⊤) ⊎ (argmin f ⊤ xs ∈ xs)
argmin-sel f = foldr-selective (⊓ᴸ-sel f)

argmin-all : ∀ (f : A → B) {⊤ xs} {P : Pred A p} →
             P ⊤ → All P xs → P (argmin f ⊤ xs)
argmin-all f {⊤} {xs} {P = P}  p⊤ pxs with argmin-sel f ⊤ xs
... | inj₁ argmin≡⊤  = subst P (sym argmin≡⊤) p⊤
... | inj₂ argmin∈xs = lookup pxs argmin∈xs

------------------------------------------------------------------------------
-- Properties of argmax

module _ {f : A → B} where

  v≤f[argmax]⁺ : ∀ {v} ⊥ xs → (v ≤ f ⊥) ⊎ (Any (λ x → v ≤ f x) xs) →
                v ≤ f (argmax f ⊥ xs)
  v≤f[argmax]⁺ = foldr-preservesᵒ (⊔ᴸ-presᵒ-v≤ f)

  v<f[argmax]⁺ : ∀ {v} ⊥ xs → (v < f ⊥) ⊎ (Any (λ x → v < f x) xs) →
                v < f (argmax f ⊥ xs)
  v<f[argmax]⁺ = foldr-preservesᵒ (⊔ᴸ-presᵒ-v< f)

  f[argmax]≤v⁺ : ∀ {v ⊥ xs} → f ⊥ ≤ v → All (λ x → f x ≤ v) xs →
                f (argmax f ⊥ xs) ≤ v
  f[argmax]≤v⁺ = foldr-preservesᵇ (⊔ᴸ-presᵇ-≤v f)

  f[argmax]<v⁺ : ∀ {v ⊥ xs} → f ⊥ < v → All (λ x → f x < v) xs →
                f (argmax f ⊥ xs) < v
  f[argmax]<v⁺ = foldr-preservesᵇ (⊔ᴸ-presᵇ-<v f)

  f[⊥]≤f[argmax] : ∀ ⊥ xs → f ⊥ ≤ f (argmax f ⊥ xs)
  f[⊥]≤f[argmax] ⊥ xs = v≤f[argmax]⁺ ⊥ xs (inj₁ refl)

  f[xs]≤f[argmax] : ∀ ⊥ xs → All (λ x → f x ≤ f (argmax f ⊥ xs)) xs
  f[xs]≤f[argmax] ⊥ xs = foldr-forcesᵇ (⊔ᴸ-forcesᵇ-≤v f) ⊥ xs refl

  f[argmax]≈f[v]⁺ : ∀ {v ⊥ xs} → v ∈ xs → All (λ x → f x ≤ f v) xs → f ⊥ ≤ f v →
                    f (argmax f ⊥ xs) ≈ f v
  f[argmax]≈f[v]⁺ v∈xs fxs≤fv f⊥≤fv = antisym
    (f[argmax]≤v⁺ f⊥≤fv fxs≤fv)
    (v≤f[argmax]⁺ _ _ (inj₂ (lose v∈xs refl)))

argmax[xs]≤argmax[ys]⁺ : ∀ {f g : A → B} {⊥₁} ⊥₂ {xs : List A} ys →
                         (f ⊥₁ ≤ g ⊥₂) ⊎ Any (λ y → f ⊥₁ ≤ g y) ys →
                         All (λ x → (f x ≤ g ⊥₂) ⊎ Any (λ y → f x ≤ g y) ys) xs →
                         f (argmax f ⊥₁ xs) ≤ g (argmax g ⊥₂ ys)
argmax[xs]≤argmax[ys]⁺ ⊥₂ ys ⊥₁≤ys xs≤ys =
  f[argmax]≤v⁺ (v≤f[argmax]⁺ ⊥₂ _ ⊥₁≤ys) (map (v≤f[argmax]⁺ ⊥₂ ys) xs≤ys)

argmax[xs]<argmax[ys]⁺ : ∀ {f g : A → B} {⊥₁} ⊥₂ {xs : List A} ys →
                         (f ⊥₁ < g ⊥₂) ⊎ Any (λ y → f ⊥₁ < g y) ys →
                         All (λ x → (f x < g ⊥₂) ⊎ Any (λ y → f x < g y) ys) xs →
                         f (argmax f ⊥₁ xs) < g (argmax g ⊥₂ ys)
argmax[xs]<argmax[ys]⁺ ⊥₂ ys ⊥₁<ys xs<ys =
  f[argmax]<v⁺ (v<f[argmax]⁺ ⊥₂ _ ⊥₁<ys) (map (v<f[argmax]⁺ ⊥₂ ys) xs<ys)

argmax-sel : ∀ (f : A → B) ⊥ xs → (argmax f ⊥ xs ≡ ⊥) ⊎ (argmax f ⊥ xs ∈ xs)
argmax-sel f = foldr-selective (⊔ᴸ-sel f)

argmax-all : ∀ (f : A → B) {P : Pred A p} {⊥ xs} →
             P ⊥ → All P xs → P (argmax f ⊥ xs)
argmax-all f {P = P} {⊥} {xs} p⊥ pxs with argmax-sel f ⊥ xs
... | inj₁ argmax≡⊥  = subst P (sym argmax≡⊥) p⊥
... | inj₂ argmax∈xs = lookup pxs argmax∈xs

------------------------------------------------------------------------------
-- Properties of min

min≤v⁺ : ∀ {v} ⊤ xs → ⊤ ≤ v ⊎ Any (_≤ v) xs → min ⊤ xs ≤ v
min≤v⁺ = f[argmin]≤v⁺

min<v⁺ : ∀ {v} ⊤ xs → ⊤ < v ⊎ Any (_< v) xs → min ⊤ xs < v
min<v⁺ = f[argmin]<v⁺

v≤min⁺ : ∀ {v ⊤ xs} → v ≤ ⊤ → All (v ≤_) xs → v ≤ min ⊤ xs
v≤min⁺ = v≤f[argmin]⁺

v<min⁺ : ∀ {v ⊤ xs} → v < ⊤ → All (v <_) xs → v < min ⊤ xs
v<min⁺ = v<f[argmin]⁺

min≤⊤ : ∀ ⊤ xs → min ⊤ xs ≤ ⊤
min≤⊤ = f[argmin]≤f[⊤]

min≤xs : ∀ ⊥ xs → All (min ⊥ xs ≤_) xs
min≤xs = f[argmin]≤f[xs]

min≈v⁺ : ∀ {v ⊤ xs} → v ∈ xs → All (v ≤_) xs → v ≤ ⊤ → min ⊤ xs ≈ v
min≈v⁺ = f[argmin]≈f[v]⁺

min[xs]≤min[ys]⁺ : ∀ ⊤₁ {⊤₂} xs {ys} → (⊤₁ ≤ ⊤₂) ⊎ Any (_≤ ⊤₂) xs →
                   All (λ y → (⊤₁ ≤ y) ⊎ Any (λ x → x ≤ y) xs) ys →
                   min ⊤₁ xs ≤ min ⊤₂ ys
min[xs]≤min[ys]⁺ = argmin[xs]≤argmin[ys]⁺

min[xs]<min[ys]⁺ : ∀ ⊤₁ {⊤₂} xs {ys} → (⊤₁ < ⊤₂) ⊎ Any (_< ⊤₂) xs →
                   All (λ y → (⊤₁ < y) ⊎ Any (λ x → x < y) xs) ys →
                   min ⊤₁ xs < min ⊤₂ ys
min[xs]<min[ys]⁺ = argmin[xs]<argmin[ys]⁺

------------------------------------------------------------------------------
-- Properties of max

max≤v⁺ : ∀ {v ⊥ xs} → ⊥ ≤ v → All (_≤ v) xs → max ⊥ xs ≤ v
max≤v⁺ = f[argmax]≤v⁺

max<v⁺ : ∀ {v ⊥ xs} → ⊥ < v → All (_< v) xs → max ⊥ xs < v
max<v⁺ = f[argmax]<v⁺

v≤max⁺ : ∀ {v} ⊥ xs → v ≤ ⊥ ⊎ Any (v ≤_) xs → v ≤ max ⊥ xs
v≤max⁺ = v≤f[argmax]⁺

v<max⁺ : ∀ {v} ⊥ xs → v < ⊥ ⊎ Any (v <_) xs → v < max ⊥ xs
v<max⁺ = v<f[argmax]⁺

⊥≤max : ∀ ⊥ xs → ⊥ ≤ max ⊥ xs
⊥≤max = f[⊥]≤f[argmax]

xs≤max : ∀ ⊥ xs → All (_≤ max ⊥ xs) xs
xs≤max = f[xs]≤f[argmax]

max≈v⁺ : ∀ {v ⊤ xs} → v ∈ xs → All (_≤ v) xs → ⊤ ≤ v → max ⊤ xs ≈ v
max≈v⁺ = f[argmax]≈f[v]⁺

max[xs]≤max[ys]⁺ : ∀ {⊥₁} ⊥₂ {xs} ys → ⊥₁ ≤ ⊥₂ ⊎ Any (⊥₁ ≤_) ys →
                   All (λ x → x ≤ ⊥₂ ⊎ Any (x ≤_) ys) xs →
                   max ⊥₁ xs ≤ max ⊥₂ ys
max[xs]≤max[ys]⁺ = argmax[xs]≤argmax[ys]⁺

max[xs]<max[ys]⁺ : ∀ {⊥₁} ⊥₂ {xs} ys → ⊥₁ < ⊥₂ ⊎ Any (⊥₁ <_) ys →
                   All (λ x → x < ⊥₂ ⊎ Any (x <_) ys) xs →
                   max ⊥₁ xs < max ⊥₂ ys
max[xs]<max[ys]⁺ = argmax[xs]<argmax[ys]⁺


text:
------------------------------------------------------------------------------
-- Fair properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.ABP.Fair.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the Fair
-- predicate is also a pre-fixed point of the functional FairF, i.e.
--
-- FairF Fair ≤ Fair (see FOTC.Program.ABP.Fair).

-- See Issue https://github.com/asr/apia/issues/81 .
Fair-inA : D → Set
Fair-inA os = ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ Fair os'
{-# ATP definition Fair-inA #-}

Fair-in : ∀ {os} → ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ Fair os' →
          Fair os
Fair-in h = Fair-coind Fair-inA h' h
  where
  postulate
    h' : ∀ {os} → Fair-inA os →
         ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ Fair-inA os'
  {-# ATP prove h' #-}

head-tail-Fair : ∀ {os} → Fair os → os ≡ T ∷ tail₁ os ∨ os ≡ F ∷ tail₁ os
head-tail-Fair {os} Fos with Fair-out Fos
... | (.(T ∷ []) , os' , f*tnil , h , Fos') = prf
  where
  postulate prf : os ≡ T ∷ tail₁ os ∨ os ≡ F ∷ tail₁ os
  {-# ATP prove prf #-}

... | (.(F ∷ ft) , os' , f*tcons {ft} FTft , h , Fos') = prf
  where
  postulate prf : os ≡ T ∷ tail₁ os ∨ os ≡ F ∷ tail₁ os
  {-# ATP prove prf #-}

tail-Fair : ∀ {os} → Fair os → Fair (tail₁ os)
tail-Fair {os} Fos with Fair-out Fos
... | .(T ∷ []) , os' , f*tnil , h , Fos' = prf
  where
  postulate prf : Fair (tail₁ os)
  {-# ATP prove prf #-}
... | .(F ∷ ft) , os' , f*tcons {ft} FTft , h , Fos' = prf
  where
  postulate prf : Fair (tail₁ os)
  {-# ATP prove prf Fair-in #-}


text:
open import Agda.Primitive
open import Data.Unit
open import Data.Nat hiding (_⊔_ ; _^_)
open import Data.Integer hiding (_⊔_)
open import Data.List
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All as All
open import Data.List.Membership.Propositional
open import Data.Product
open import Data.Maybe hiding (_>>=_)
open import Data.List.Prefix
open import Data.List.Properties.Extra
open import Data.List.All.Properties.Extra
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
open import Common.Weakening

-- This file contains the definitional interpreter for STLC using
-- scopes and frames, described in Section 4 of the paper.

-- The scopes-and-frames library assumes that we are given a
-- particular scope graph, with `k` scopes.  The following module is
-- parameterized by a `k` representing the number of scopes that a
-- particular object language program has.

module STLCSF.Semantics (k : ℕ) where

-----------
-- TYPES --
-----------

data Ty : Set where
  unit : Ty
  _⇒_  : (a b : Ty) → Ty
  int  : Ty

-- The library is loaded and passed two arguments:
--
-- * `k` is the size of the scope graph for an object program
--
-- * `Ty` is the type of declarations in the scope graph

open import ScopesFrames.ScopesFrames k Ty

-- Our interpreter is parameterized by a scope graph, via the module
-- below.

module Syntax (g : Graph) where

  -- We load all the scope graph definitions in the scope graph
  -- library, by passing the object scope graph `g` as module
  -- parameter:
  open UsesGraph g

  ------------
  -- SYNTAX --
  ------------

  -- We can now define our well-typed syntax as described in the paper
  -- Section 4.2:
  data Expr (s : Scope) : Ty → Set where
    unit  : Expr s unit
    var   : ∀ {t} → (s ↦ t) → Expr s t
    ƛ     : ∀ {s' a b} → ⦃ shape : g s' ≡ ( [ a ] , [ s ] ) ⦄ → Expr s' b → Expr s (a ⇒ b)
    _·_   : ∀ {a b} → Expr s (a ⇒ b) → Expr s a → Expr s b
    num   : ℤ → Expr s int
    iop   : (ℤ → ℤ → ℤ) → (l r : Expr s int) → Expr s int

  ------------
  -- VALUES --
  ------------

  -- We can also define well-typed values as described in the paper
  -- Section 4.4:
  data Val : Ty → (Σ : HeapTy) → Set where
    unit   : ∀ {Σ} → Val unit Σ
    ⟨_,_⟩  : ∀ {Σ s s' a b}⦃ shape : g s' ≡ ( [ a ] , [ s ] ) ⦄ →
             Expr s' b → Frame s Σ → Val (a ⇒ b) Σ
    num    : ∀ {Σ} → ℤ → Val int Σ

  val-weaken : ∀ {t Σ Σ'} → Σ ⊑ Σ' → Val t Σ → Val t Σ'
  val-weaken ext ⟨ e , f ⟩ = ⟨ e , wk ext f ⟩
  val-weaken ext unit      = unit
  val-weaken ext (num z)   = num z

  -- We can now load the frames definitions of the scopes-and-frames
  -- library.  As described in Section 4.3 of the paper, our notion of
  -- frame assumes a notion of weakenable value, to be passed as
  -- module arguments to `UsesVal`:
  open UsesVal Val val-weaken renaming (getFrame to getFrame')

  -- We rename `getFrame` from the scopes-and-frames library so that
  -- we can use `getFrame` as the name of the monadic operation which
  -- returns the "current frame pointer" below.

  -----------
  -- MONAD --
  -----------

  -- These definitions correspond to Section 4.4.

  M : (s : Scope) → (HeapTy → Set) → HeapTy → Set
  M s p Σ = Frame s Σ → Heap Σ → Maybe (∃ λ Σ' → (Heap Σ' × p Σ' × Σ ⊑ Σ'))

  _>>=_       :  ∀ {s Σ}{p q : List Scope → Set} →
                 M s p Σ → (∀ {Σ'} → p Σ' → M s q Σ') → M s q Σ
  (a >>= b) f h
    with (a f h)
  ...  | nothing = nothing
  ...  | just (Σ , h' , v , ext)
       with (b v (wk ext f) h')
  ...     | nothing = nothing
  ...     | just (Σ' , h'' , v' , ext') = just (Σ' , h'' , v' , ext ⊚ ext')

  return      :  ∀ {s Σ}{p : List Scope → Set} → p Σ → M s p Σ
  return v f h = just (_ , h , v , ⊑-refl)

  getFrame    :  ∀ {s Σ} → M s (Frame s) Σ
  getFrame f = return f f

  usingFrame  :  ∀ {s s' Σ}{p : List Scope → Set} → Frame s Σ → M s p Σ → M s' p Σ
  usingFrame f a _ = a f

  timeout     :  ∀ {s Σ}{p : List Scope → Set} → M s p Σ
  timeout _ _ = nothing

  init        :  ∀ {Σ s' ds es}(s : Scope)⦃ shape : g s ≡ (ds , es) ⦄ →
                 Slots ds Σ → Links es Σ → M s' (Frame s) Σ
  init {Σ} s slots links _ h
    with (initFrame s slots links h)
  ...  | (f' , h') = just (_ , h' , f' , ∷ʳ-⊒ s Σ)

  getv        :  ∀ {s t Σ} → (s ↦ t) → M s (Val t) Σ
  getv p f h = return (getVal p f h) f h

  _^_         :  ∀ {Σ Γ}{p q : List Scope → Set} → ⦃ w : Weakenable q ⦄ →
                 M Γ p Σ → q Σ → M Γ (p ⊗ q) Σ
  (a ^ x) f h
    with (a f h)
  ...  | nothing = nothing
  ...  | just (Σ , h' , v , ext) = just (Σ , h' , (v , wk ext x) , ext)

  sₑ : ∀ {s t} → Expr s t → Scope
  sₑ {s} _ = s

  eval : ℕ → ∀ {s t Σ} → Expr s t → M s (Val t) Σ
  eval zero     _      =
    timeout
  eval (suc k) unit    =
    return unit
  eval (suc k) (var x) =
    getv x
  eval (suc k) (ƛ e)   =
    getFrame >>= λ f →
    return ⟨ e , f ⟩
  eval (suc k) (l · r) =
    eval k l >>= λ{ ⟨ e , f ⟩ →
    (eval k r ^ f) >>= λ{ (v , f) →
    init (sₑ e) (v ∷ []) (f ∷ []) >>= λ f' →
    usingFrame f' (eval k e) }}
  eval (suc k) (num z) =
    return (num z)
  eval (suc k) (iop f l r) =
    eval k l >>= λ{ (num z₁) →
    eval k r >>= λ{ (num z₂) →
    return (num (f z₁ z₂)) }}


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.SemiTensor.GeneralizesMul {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Mul struct
open import MLib.Matrix.Tensor struct
open import MLib.Matrix.SemiTensor.Core struct
open import MLib.Algebra.Operations struct

open Nat using () renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)

open import MLib.Fin.Parts.Simple

open import Data.Nat.LCM
open import Data.Nat.Divisibility

-- Semi-tensor product generalizes the usual matrix product

module _ ⦃ props : Has (1# is rightIdentity for * ∷ []) ⦄ where
  generalizes-⊗ : ∀ {m n o} (A : Matrix S m n) (B : Matrix S n o) → A ⋉ B ≃ A ⊗ B

  open _≃_

  module Zero {m o} (A : Matrix S m 0) (B : Matrix S 0 o) where
    generalizes-⊗′ : A ⋉ B ≃ A ⊗ B
    generalizes-⊗′ .m≡p = Nat.*-identityʳ m
    generalizes-⊗′ .n≡q = Nat.*-identityʳ o
    generalizes-⊗′ .equal _ _ = S.refl

  module Nonzero {m n o} (A : Matrix S m (suc n)) (B : Matrix S (suc n) o) where
    private
      t = lcm (suc n) (suc n) .proj₁
      t-lcm = lcm (suc n) (suc n) .proj₂

      open Defn t-lcm renaming (n∣t to sn∣t; t/n to t/sn; p∣t to sn∣t′; t/p to t/sn′)

      A′′-lem : A′′ A B ≃ A
      B′′-lem : B′′ A B ≃ B

    generalizes-⊗′ : A ⋉ B ≃ A ⊗ B
    generalizes-⊗′ = ⊗-cong-≃ _ _ _ _ A′′-lem B′′-lem

    private
      abstract
        lcm-n-n : ∀ {n t} → LCM n n t → t ≡ n
        lcm-n-n {n} isLcm =
          let t∣n = LCM.least isLcm (∣-refl , ∣-refl)
              n∣t = LCM.commonMultiple isLcm .proj₁
          in ∣-antisym t∣n n∣t

        quotient-n-n : ∀ {n} (p : suc n ∣ suc n) → quotient p ≡ 1
        quotient-n-n (divides q equality) = Nat.*-cancelʳ-≡ q 1 (≡.sym (≡.trans (≡.cong suc (Nat.+-identityʳ _)) equality))

        quotient-subst : ∀ {n p q} (n∣p : n ∣ p) (p≡q : p ≡ q) → quotient n∣p ≡ quotient (≡.subst (λ h → n ∣ h) p≡q n∣p)
        quotient-subst n∣p ≡.refl = ≡.refl

        t≡sn : t ≡ suc n
        t≡sn = lcm-n-n t-lcm

        t/sn≡1 : t/sn ≡ 1
        t/sn≡1 =
          begin
            t/sn ≡⟨ quotient-subst sn∣t t≡sn ⟩
            quotient (≡.subst (λ h → suc n ∣ h) t≡sn sn∣t) ≡⟨ quotient-n-n (≡.subst (λ h → suc n ∣ h) t≡sn sn∣t) ⟩
            1 ∎
          where open ≡.Reasoning

        t/sn′≡1 : t/sn′ ≡ 1
        t/sn′≡1 =
          begin
            t/sn′ ≡⟨ quotient-subst sn∣t′ t≡sn ⟩
            quotient (≡.subst (λ h → suc n ∣ h) t≡sn sn∣t′) ≡⟨ quotient-n-n (≡.subst (λ h → suc n ∣ h) t≡sn sn∣t′) ⟩
            1 ∎
          where open ≡.Reasoning

        lhs≡m : m *ℕ t/sn ≡ m
        lhs≡m =
          begin
            m *ℕ t/sn ≡⟨ ≡.cong₂ _*ℕ_ (≡.refl {x = m}) t/sn≡1 ⟩
            m *ℕ 1 ≡⟨ Nat.*-identityʳ _ ⟩
            m ∎
          where open ≡.Reasoning

        rhs≡o : o *ℕ t/sn′ ≡ o
        rhs≡o =
          begin
            o *ℕ t/sn′ ≡⟨ ≡.cong₂ _*ℕ_ (≡.refl {x = o}) t/sn′≡1 ⟩
            o *ℕ 1 ≡⟨ Nat.*-identityʳ _ ⟩
            o ∎
          where open ≡.Reasoning

      A′′-lem = ≃-trans (≡-subst-≃₂ lem₁) (≃-trans (⊠-cong (≃-refl {A = A}) (1●-cong-≃ t/sn≡1)) (⊠-identityʳ ⦃ weaken props ⦄ A))
      B′′-lem = ≃-trans (≡-subst-≃₁ lem₂) (≃-trans (⊠-cong (≃-refl {A = B}) (1●-cong-≃ t/sn′≡1)) (⊠-identityʳ ⦃ weaken props ⦄ B))

  generalizes-⊗ {n = zero} = Zero.generalizes-⊗′
  generalizes-⊗ {n = suc n} = Nonzero.generalizes-⊗′


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors with fast append
------------------------------------------------------------------------

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

module Data.DifferenceVec where

open import Data.DifferenceNat
open import Data.Vec as V using (Vec)
open import Function
import Data.Nat.Base as N

infixr 5 _∷_ _++_

DiffVec : ∀ {ℓ} → Set ℓ → Diffℕ → Set ℓ
DiffVec A m = ∀ {n} → Vec A n → Vec A (m n)

[] : ∀ {a} {A : Set a} → DiffVec A 0#
[] = λ k → k

_∷_ : ∀ {a} {A : Set a} {n} → A → DiffVec A n → DiffVec A (suc n)
x ∷ xs = λ k → V._∷_ x (xs k)

[_] : ∀ {a} {A : Set a} → A → DiffVec A 1#
[ x ] = x ∷ []

_++_ : ∀ {a} {A : Set a} {m n} →
       DiffVec A m → DiffVec A n → DiffVec A (m + n)
xs ++ ys = λ k → xs (ys k)

toVec : ∀ {a} {A : Set a} {n} → DiffVec A n → Vec A (toℕ n)
toVec xs = xs V.[]

-- fromVec xs is linear in the length of xs.

fromVec : ∀ {a} {A : Set a} {n} → Vec A n → DiffVec A (fromℕ n)
fromVec xs = λ k → xs ⟨ V._++_ ⟩ k

head : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → A
head xs = V.head (toVec xs)

tail : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → DiffVec A n
tail xs = λ k → V.tail (xs k)

take : ∀ {a} {A : Set a} m {n} →
       DiffVec A (fromℕ m + n) → DiffVec A (fromℕ m)
take N.zero    xs = []
take (N.suc m) xs = head xs ∷ take m (tail xs)

drop : ∀ {a} {A : Set a} m {n} →
       DiffVec A (fromℕ m + n) → DiffVec A n
drop N.zero    xs = xs
drop (N.suc m) xs = drop m (tail xs)


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.S2 where

open import Cubical.HITs.S2.Base public
open import Cubical.HITs.S2.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Nat where

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

_+_ : ℕ → ℕ → ℕ
zero + a = a
suc a + b = suc (a + b)

data _≡_ {A : Set} : A → A → Set where
   refl : {a : A} → a ≡ a

infix 4 _≡_

cong : {A B : Set} {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl

+-assoc : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+-assoc zero b c = refl
+-assoc (suc a) b c = cong suc (+-assoc a b c)

max_stars_repo_name: divipp/agda-intro-prezi

max_issues_repo_name: divipp/agda-intro-prezi

max_forks_repo_name: divipp/agda-intro-prezi


text:
module ModuleReexport where

open import Common.Unit
open import Common.Nat
open import Common.IO

module A (B : Set) (b : B) where
  data X : Set where
    Con1 : B -> X
    Con2 : X
  f : X -> B
  f (Con1 x) = x
  f Con2 = b

module X = A Nat 10

main = printNat (A.f Nat 10 (X.Con1 20)) ,,
  putStrLn "" ,,
  printNat (A.f Nat 10 X.Con2) ,,
  putStrLn "" ,,
  return unit


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Symmetric closures of binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Closure.Symmetric where

open import Data.Sum as Sum using (_⊎_)
open import Function using (id)
open import Relation.Binary

open Sum public using () renaming (inj₁ to fwd; inj₂ to bwd)

-- The symmetric closure of a relation.

SymClosure : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Rel A ℓ
SymClosure _∼_ a b = a ∼ b ⊎ b ∼ a

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

  -- Symmetric closures are symmetric.

  symmetric : (_∼_ : Rel A ℓ) → Symmetric (SymClosure _∼_)
  symmetric _ (fwd a∼b) = bwd a∼b
  symmetric _ (bwd b∼a) = fwd b∼a

  -- A generalised variant of map which allows the index type to change.

  gmap : ∀ {b ℓ₂} {B : Set b} {P : Rel A ℓ} {Q : Rel B ℓ₂} →
         (f : A → B) → P =[ f ]⇒ Q → SymClosure P =[ f ]⇒ SymClosure Q
  gmap _ g = Sum.map g g

  map : ∀ {ℓ₂} {P : Rel A ℓ} {Q : Rel A ℓ₂} →
        P ⇒ Q → SymClosure P ⇒ SymClosure Q
  map = gmap id


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Relation where

open import Light.Level using (Level ; Setω)
open import Light.Variable.Sets

record Kind : Setω where
      field
            iℓ : Level
            Index : Set iℓ
            ℓf : Index → Level
            Proposition : ∀ i → Set (ℓf i)

record Style (kind : Kind) : Setω where
      open Kind kind
      field
            true‐i false‐i : Index
            true : Proposition true‐i
            false : Proposition false‐i

            ¬‐index‐f : Index → Index
            ¬_ : ∀ {i} → Proposition i → Proposition (¬‐index‐f i)

            ∧‐index‐f ∨‐index‐f ⇢‐index‐f : Index → Index → Index
            _∧_ : ∀ {ia ib} → Proposition ia → Proposition ib → Proposition (∧‐index‐f ia ib)
            _∨_ : ∀ {ia ib} → Proposition ia → Proposition ib → Proposition (∨‐index‐f ia ib)
            _⇢_ : ∀ {ia ib} → Proposition ia → Proposition ib → Proposition (⇢‐index‐f ia ib)

            true‐set‐ℓf false‐set‐ℓf : Index → Level
            True : ∀ {i} → Proposition i → Set (true‐set‐ℓf i)
            False : ∀ {i} → Proposition i → Set (false‐set‐ℓf i)
            true‐is‐true : True true
            false‐is‐false : False false

record Base : Setω where
      field ⦃ kind ⦄ : Kind
      field ⦃ style ⦄ : Style kind

open Kind ⦃ ... ⦄ public
open Style ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Addition
open import Numbers.Naturals.Multiplication
open import Numbers.Naturals.Order

module Numbers.Naturals.Exponentiation where

_^N_ : ℕ → ℕ → ℕ
a ^N zero = 1
a ^N succ b = a *N (a ^N b)

exponentiationIncreases : (a b : ℕ) → (a ≡ 0) || (a ≤N a ^N (succ b))
exponentiationIncreases zero b = inl refl
exponentiationIncreases (succ a) zero = inr (inr (applyEquality succ (transitivity (additionNIsCommutative 0 a) (multiplicationNIsCommutative 1 a))))
exponentiationIncreases (succ a) (succ b) with exponentiationIncreases (succ a) b
exponentiationIncreases (succ a) (succ b) | inr (inl x) = inr (inl (canAddToOneSideOfInequality _ x))
exponentiationIncreases (succ a) (succ b) | inr (inr x) with productOne x
exponentiationIncreases (succ 0) (succ b) | inr (inr x) | inr pr rewrite pr = inr (inr refl)
exponentiationIncreases (succ (succ a)) (succ b) | inr (inr x) | inr pr rewrite pr | productWithOneRight a = inr (inl (le (succ (a +N a *N succ (succ a))) (additionNIsCommutative _ (succ (succ a)))))


text:
module Issue296 where

postulate
  Unit : Set
  IO   : Set → Set
  foo  : ((A B : Set) → Unit) → IO Unit
  bar  : (A B : Set) → Unit

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}
{-# COMPILED_TYPE Unit () #-}
{-# COMPILED bar undefined #-}

main : IO Unit
main = foo bar

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Testing nested axioms
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module NestedAxioms.A where

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

postulate
  D   : Set
  _≡_ : D → D → Set

postulate
  a b : D
  a≡b : a ≡ b
{-# ATP axiom a≡b #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- Andreas, 2016-11-02, issue #2285 raised by effectfully, found by dnkndnts

-- {-# OPTIONS -v tc.data.fits:15 #-}
-- {-# OPTIONS -v tc.conv.sort:30 #-}
-- {-# OPTIONS -v tc.meta.assign:50 #-}
-- {-# OPTIONS -v tc.meta.new:50 #-}
-- {-# OPTIONS -v tc:10 #-}
-- {-# OPTIONS -v tc.data:100 #-}

mutual
  Type = _

  data Big : Type where
    big : (∀ {α} → Set α) → Big

-- Problem WAS:
-- new sort meta _0 : .Agda.Primitive.Level
-- new meta (?0) _1 : Set _0
-- new sort meta _2 : .Agda.Primitive.Level
-- solving _0 := .Agda.Primitive.lsuc _2
-- solving _1 := Set _2
-- solving _2 := Setω

-- Big should be rejected

-- Even with Type = Setω : Setω, we do not get Hurkens through:
{-
  ⊥ : Type
  ⊥ = (A : Type) → A

  ¬_ : Type → Type
  ¬ A = A → ⊥

  -- We have some form of Type : Type
  P : Type → Type
  P A = A → Type

  U : Type
  U = (X : Type) → (P (P X) → X) → P (P X)

  test : Type
  test = P (P U) → U

{-

  -- This is not accepted:
  τ : P (P U) → U
  τ = λ (t : P (P U)) (X : Type) (f : P (P X) → X) (p : P X) → t λ x → p (f (x X f))

  σ : U → (P (P U))
  σ = λ (s : U) → s U λ t → τ t

  Δ : P U
  Δ = \y → ¬ ((p : P U) → σ y p → p (τ (σ y)))

  Ω : U
  Ω = τ \p → (x : U) → σ x p → p x

  D : Type
  D = (p : P U) → σ Ω p → p (τ (σ Ω))

  lem₁ : (p : P U) → ((x : U) → σ x p → p x) → p Ω
  lem₁ p H1 = H1 Ω \x → H1 (τ (σ x))

  lem₂ : ¬ D
  lem₂ = lem₁ Δ \x H2 H3 → H3 Δ H2 \p → H3 \y → p (τ (σ y))

  lem₃ : D
  lem₃ p = lem₁ \y → p (τ (σ y))

  loop : ⊥
  loop = lem₂ lem₃
-- -}
-- -}


text:
-- Andreas, 2019-03-18, AIM XXIX, performance regression in 2.5.4
-- The following was quick in 2.5.3

postulate
  Bool : Set
  Foo : Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Set

data FooRel
  : (x1 x1' : Bool)
    (x2 x2' : Bool)
    (x3 x3' : Bool)
    (x4 x4' : Bool)
    (x5 x5' : Bool)
    (x6 x6' : Bool)
    (x7 x7' : Bool)
    (x8 x8' : Bool)
    (x9 x9' : Bool)
  → Foo x1 x2 x3 x4 x5 x6 x7 x8 x9
  → Foo x1' x2' x3' x4' x5' x6' x7' x8' x9'
  → Set
  where
  tran
    : (x1 x1' x1'' : Bool)
      (x2 x2' x2'' : Bool)
      (x3 x3' x3'' : Bool)
      (x4 x4' x4'' : Bool)
      (x5 x5' x5'' : Bool)
      (x6 x6' x6'' : Bool)
      (x7 x7' x7'' : Bool)
      (x8 x8' x8'' : Bool)
      (x9 x9' x9'' : Bool)
      (t : Foo x1 x2 x3 x4 x5 x6 x7 x8 x9)
      (t' : Foo x1' x2' x3' x4' x5' x6' x7' x8' x9')
      (t'' : Foo x1'' x2'' x3'' x4'' x5'' x6'' x7'' x8'' x9'')
    → FooRel x1 x1' x2 x2' x3 x3' x4 x4' x5 x5' x6 x6' x7 x7' x8 x8' x9 x9' t t'
    → FooRel x1' x1'' x2' x2'' x3' x3'' x4' x4'' x5' x5'' x6' x6'' x7' x7'' x8' x8'' x9' x9'' t' t''
    → FooRel x1 x1'' x2 x2'' x3 x3'' x4 x4'' x5 x5'' x6 x6'' x7 x7'' x8 x8'' x9 x9'' t t''

foo
  : (x1 x1' : Bool)
    (x2 x2' : Bool)
    (x3 x3' : Bool)
    (x4 x4' : Bool)
    (x5 x5' : Bool)
    (x6 x6' : Bool)
    (x7 x7' : Bool)
    (x8 x8' : Bool)
    (x9 x9' : Bool)
    (t : Foo x1 x2 x3 x4 x5 x6 x7 x8 x9)
    (t' : Foo x1' x2' x3' x4' x5' x6' x7' x8' x9')
  → FooRel x1 x1' x2 x2' x3 x3' x4 x4' x5 x5' x6 x6' x7 x7' x8 x8' x9 x9' t t'
  → Set
foo x1 x1' x2 x2' x3 x3' x4 x4' x5 x5' x6 x6' x7 x7' x8 x8' x9 x9' t t' (tran .x1 x1'' .x1' .x2 x2'' .x2' .x3 x3'' .x3' .x4 x4'' .x4' .x5 x5'' .x5' .x6 x6'' .x6' .x7 x7'' .x7' .x8 x8'' .x8' .x9 x9'' .x9' .t t'' .t' xy yz) = Bool

-- Should check quickly again in 2.6.0

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.Symmetric where

open import Level

open import Categories.Category
open import Categories.Monoidal
open import Categories.Monoidal.Braided
open import Categories.Monoidal.Helpers
open import Categories.Monoidal.Braided.Helpers
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘₁_; _≡_; id)

record Symmetric {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (B : Braided M) : Set (o ⊔ ℓ ⊔ e) where
  private module C = Category C
  private module M = Monoidal M
  private module B = Braided B

  -- open C hiding (id; identityˡ; identityʳ; assoc; _≡_)
  -- open M hiding (id)
  -- open MonoidalHelperFunctors C ⊗ M.id
  -- open BraidedHelperFunctors C ⊗ M.id

  private module NI = NaturalIsomorphism B.braid

  field
    symmetry : NI.F⇒G ∘₁ NI.F⇐G ≡ id

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
open import Common.Prelude
open import Common.Reflect

id : {A : Set} → A → A
id x = x

idTerm : Term
idTerm = lam visible (def (quote id) (arg₁ ∷ arg₂ ∷ []))
  where
    arg₁ = arg (arginfo hidden relevant) (def (quote Nat) [])
    arg₂ = arg (arginfo visible relevant) (var 0 [])

-- Should fail since idTerm "λ z → id {Nat} z"
id₂ : {A : Set} → A → A
id₂ = unquote idTerm

max_stars_repo_name: larrytheliquid/agda


text:
-- Andreas, 2022-03-07, issue #5809 reported by jamestmartin
-- Regression in Agda 2.6.1.
-- Not reducing irrelevant projections lead to non-inferable elim-terms
-- and consequently to internal errors.
--
-- The fix is to treat irrelevant projections as just functions,
-- retaining their parameters, so that they remain inferable
-- even if not in normal form.

{-# OPTIONS --irrelevant-projections #-}
{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS --no-double-check #-}
-- {-# OPTIONS -v impossible:100 #-}
-- {-# OPTIONS -v tc:40 #-}

open import Agda.Builtin.Equality

record Squash {ℓ} (A : Set ℓ) : Set ℓ where
  constructor squash
  field
    .unsquash : A
open Squash

.test : ∀ {ℓ} {A : Set ℓ} (x : A) (y : Squash A) → {!!}
test x y = {!!}
  where
    help : unsquash (squash x) ≡ unsquash y
    help = refl

-- WAS: internal error.
-- Should succeed with unsolved metas.


text:
module PatternSynonymParameterisedModule where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ -> ℕ

module M (A : Set) where
  pattern sss x = suc (suc (suc x))

open M ℕ

na : ℕ
na = sss 3

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures as LedgerInfoWithSignatures
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.KVMap as Map
open import Util.Hash
open import Util.Prelude

module LibraBFT.Impl.Types.Properties.LedgerInfoWithSignatures (self : LedgerInfoWithSignatures) (vv : ValidatorVerifier) where

  -- See comments in LibraBFT.Impl.Consensus.ConsensusTypes.Properties.QuorumCert

  postulate -- TODO-2: define and prove

    Contract : Set

    contract : LedgerInfoWithSignatures.verifySignatures self vv ≡ Right unit → Contract


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

open import Agda.Primitive as Prim public
  using    (Level; _⊔_; Setω)
  renaming (lzero to zero; lsuc to suc)

open import Agda.Builtin.Sigma public
  renaming (fst to proj₁; snd to proj₂)
  hiding (module Σ)

infixr 2 _×_

variable
  a b c p q r : Level
  A B C : Set a

_×_ : ∀ (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ A λ _ → B

<_,_> : ∀ {A : Set a} {B : A → Set b} {C : ∀ {x} → B x → Set c}
        (f : (x : A) → B x) → ((x : A) → C (f x)) →
        ((x : A) → Σ (B x) C)
< f , g > x = (f x , g x)

map : ∀ {P : A → Set p} {Q : B → Set q} →
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g (x , y) = (f x , g y)

zip : ∀ {P : A → Set p} {Q : B → Set q} {R : C → Set r} →
      (_∙_ : A → B → C) →
      (∀ {x y} → P x → Q y → R (x ∙ y)) →
      Σ A P → Σ B Q → Σ C R
zip _∙_ _∘_ (a , p) (b , q) = ((a ∙ b) , (p ∘ q))

curry′ : (A × B → C) → (A → B → C)
curry′ k a b = k (a , b)

swap : A × B → B × A
swap (x , y) = (y , x)

record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  eta-equality
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Obj → Obj → Set ℓ
    _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e

    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  CommutativeSquare : ∀ {A B C D} → (f : A ⇒ B) (g : A ⇒ C) (h : B ⇒ D) (i : C ⇒ D) → Set _
  CommutativeSquare f g h i = h ∘ f ≈ i ∘ g

infix 10  _[_,_]

_[_,_] : ∀ {o ℓ e} → (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
_[_,_] = Category._⇒_

module Inner {x₁ x₂ x₃} (CC : Category x₁ x₂ x₃) where

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

  zipWith : ∀ {a b c p q r s} {A : Set a} {B : Set b} {C : Set c} {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y)
  zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
  syntax zipWith f g h = f -< h >- g

  record Functor (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    eta-equality
    private module C = Category C
    private module D = Category D

    field
      F₀ : C.Obj → D.Obj
      F₁ : ∀ {A B} (f : C [ A , B ]) → D [ F₀ A , F₀ B ]

  Product : (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
  Product C D = record
    { Obj       = C.Obj × D.Obj
    ; _⇒_       = C._⇒_ -< _×_ >- D._⇒_
    ; _≈_       = C._≈_ -< _×_ >- D._≈_
    ; _∘_       = zip C._∘_ D._∘_
    }
    where module C = Category C
          module D = Category D

  Bifunctor : Category o ℓ e → Category o′ ℓ′ e′ → Category o″ ℓ″ e″ → Set _
  Bifunctor C D E = Functor (Product C D) E

  private
    module CC = Category CC

  open CC

  infix 4 _≅_
  record _≅_ (A B : Obj) : Set (x₂) where
    field
      from : A ⇒ B
      to   : B ⇒ A

  private
    variable
      X Y Z W : Obj
      f g h : X ⇒ Y

  record Monoidal : Set (x₁ ⊔ x₂ ⊔ x₃) where
    infixr 10 _⊗₀_ _⊗₁_

    field
      ⊗  : Bifunctor CC CC CC

    module ⊗ = Functor ⊗

    open Functor ⊗

    _⊗₀_ : Obj → Obj → Obj
    _⊗₀_ = curry′ F₀

    -- this is also 'curry', but a very-dependent version
    _⊗₁_ : X ⇒ Y → Z ⇒ W → X ⊗₀ Z ⇒ Y ⊗₀ W
    f ⊗₁ g = F₁ (f , g)

    field
      associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)

    module associator {X} {Y} {Z} = _≅_ (associator {X} {Y} {Z})

    -- for exporting, it makes sense to use the above long names, but for
    -- internal consumption, the traditional (short!) categorical names are more
    -- convenient. However, they are not symmetric, even though the concepts are, so
    -- we'll use ⇒ and ⇐ arrows to indicate that
    private
      α⇒ = associator.from
      α⇐ = λ {X} {Y} {Z} → associator.to {X} {Y} {Z}

    field
      assoc-commute-from   : CommutativeSquare ((f ⊗₁ g) ⊗₁ h) α⇒ α⇒ (f ⊗₁ (g ⊗₁ h))
      assoc-commute-to     : CommutativeSquare (f ⊗₁ (g ⊗₁ h)) α⇐ α⇐ ((f ⊗₁ g) ⊗₁ h)


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

module propositional-equality where

open import Cubical.Foundations.Prelude
open import Agda.Primitive

max_stars_repo_name: guilhermehas/Equality

max_issues_repo_name: guilhermehas/Equality

max_forks_repo_name: guilhermehas/Equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties of reflexive transitive closures.
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties where

open import Function
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong; cong₂)
import Relation.Binary.Reasoning.Preorder as PreR

------------------------------------------------------------------------
-- _◅◅_

module _ {i t} {I : Set i} {T : Rel I t} where

  ◅◅-assoc : ∀ {i j k l}
             (xs : Star T i j) (ys : Star T j k) (zs : Star T k l) →
             (xs ◅◅ ys) ◅◅ zs ≡ xs ◅◅ (ys ◅◅ zs)
  ◅◅-assoc ε        ys zs = refl
  ◅◅-assoc (x ◅ xs) ys zs = cong (_◅_ x) (◅◅-assoc xs ys zs)

------------------------------------------------------------------------
-- gmap

gmap-id : ∀ {i t} {I : Set i} {T : Rel I t} {i j} (xs : Star T i j) →
          gmap id id xs ≡ xs
gmap-id ε        = refl
gmap-id (x ◅ xs) = cong (_◅_ x) (gmap-id xs)

gmap-∘ : ∀ {i t} {I : Set i} {T : Rel I t}
           {j u} {J : Set j} {U : Rel J u}
           {k v} {K : Set k} {V : Rel K v}
         (f  : J → K) (g  : U =[ f  ]⇒ V)
         (f′ : I → J) (g′ : T =[ f′ ]⇒ U)
         {i j} (xs : Star T i j) →
         (gmap {U = V} f g ∘ gmap f′ g′) xs ≡ gmap (f ∘ f′) (g ∘ g′) xs
gmap-∘ f g f′ g′ ε        = refl
gmap-∘ f g f′ g′ (x ◅ xs) = cong (_◅_ (g (g′ x))) (gmap-∘ f g f′ g′ xs)

gmap-◅◅ : ∀ {i t j u}
            {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u}
          (f : I → J) (g : T =[ f ]⇒ U)
          {i j k} (xs : Star T i j) (ys : Star T j k) →
          gmap {U = U} f g (xs ◅◅ ys) ≡ gmap f g xs ◅◅ gmap f g ys
gmap-◅◅ f g ε        ys = refl
gmap-◅◅ f g (x ◅ xs) ys = cong (_◅_ (g x)) (gmap-◅◅ f g xs ys)

gmap-cong : ∀ {i t j u}
              {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u}
            (f : I → J) (g : T =[ f ]⇒ U) (g′ : T =[ f ]⇒ U) →
            (∀ {i j} (x : T i j) → g x ≡ g′ x) →
            ∀ {i j} (xs : Star T i j) →
            gmap {U = U} f g xs ≡ gmap f g′ xs
gmap-cong f g g′ eq ε        = refl
gmap-cong f g g′ eq (x ◅ xs) = cong₂ _◅_ (eq x) (gmap-cong f g g′ eq xs)

------------------------------------------------------------------------
-- fold

fold-◅◅ : ∀ {i p} {I : Set i}
          (P : Rel I p) (_⊕_ : Transitive P) (∅ : Reflexive P) →
          (∀ {i j} (x : P i j) → (∅ ⊕ x) ≡ x) →
          (∀ {i j k l} (x : P i j) (y : P j k) (z : P k l) →
             ((x ⊕ y) ⊕ z) ≡ (x ⊕ (y ⊕ z))) →
          ∀ {i j k} (xs : Star P i j) (ys : Star P j k) →
          fold P _⊕_ ∅ (xs ◅◅ ys) ≡ (fold P _⊕_ ∅ xs ⊕ fold P _⊕_ ∅ ys)
fold-◅◅ P _⊕_ ∅ left-unit assoc ε        ys = sym (left-unit _)
fold-◅◅ P _⊕_ ∅ left-unit assoc (x ◅ xs) ys = begin
  (x ⊕  fold P _⊕_ ∅ (xs ◅◅ ys))              ≡⟨ cong (_⊕_ x) $
                                                   fold-◅◅ P _⊕_ ∅ left-unit assoc xs ys ⟩
  (x ⊕ (fold P _⊕_ ∅ xs  ⊕ fold P _⊕_ ∅ ys))  ≡⟨ sym (assoc x _ _) ⟩
  ((x ⊕ fold P _⊕_ ∅ xs) ⊕ fold P _⊕_ ∅ ys)   ∎
  where open PropEq.≡-Reasoning

------------------------------------------------------------------------
-- Relational properties

module _ {i t} {I : Set i} (T : Rel I t) where

  reflexive : _≡_ ⇒ Star T
  reflexive refl = ε

  trans : Transitive (Star T)
  trans = _◅◅_

  isPreorder : IsPreorder _≡_ (Star T)
  isPreorder = record
    { isEquivalence = PropEq.isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    }

  preorder : Preorder _ _ _
  preorder = record
    { _≈_        = _≡_
    ; _∼_        = Star T
    ; isPreorder = isPreorder
    }

------------------------------------------------------------------------
-- Preorder reasoning for Star

module StarReasoning {i t} {I : Set i} (T : Rel I t) where
  open PreR (preorder T) public
    hiding (_≈⟨_⟩_) renaming (_∼⟨_⟩_ to _⟶⋆⟨_⟩_)

  infixr 2 _⟶⟨_⟩_

  _⟶⟨_⟩_ : ∀ x {y z} → T x y → y IsRelatedTo z → x IsRelatedTo z
  x ⟶⟨ x⟶y ⟩ y⟶⋆z = x ⟶⋆⟨ x⟶y ◅ ε ⟩ y⟶⋆z


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

open import HoTT

{-
Various lemmas that will be used in cohomology.DisjointlyPointedSet.
Many of them, for example the choice lemma about coproducts, should be
put into core/.
-}

module homotopy.DisjointlyPointedSet where

module _ {i} where

  is-separable : (X : Ptd i) → Type i
  is-separable X = has-dec-onesided-eq (pt X)

  abstract
    is-separable-is-prop : {X : Ptd i}
      → is-prop (is-separable X)
    is-separable-is-prop = has-dec-onesided-eq-is-prop

  MinusPoint : (X : Ptd i) → Type i
  MinusPoint X = Σ (de⊙ X) (pt X ≠_)

  unite-pt : (X : Ptd i) → (⊤ ⊔ MinusPoint X → de⊙ X)
  unite-pt X (inl _) = pt X
  unite-pt X (inr (x , _)) = x

  has-disjoint-pt : (X : Ptd i) → Type i
  has-disjoint-pt X = is-equiv (unite-pt X)

  abstract
    separable-has-disjoint-pt : {X : Ptd i}
      → is-separable X → has-disjoint-pt X
    separable-has-disjoint-pt {X} dec =
      is-eq _ sep unite-sep sep-unite where
        sep : de⊙ X → ⊤ ⊔ (Σ (de⊙ X) (pt X ≠_))
        sep x with dec x
        sep x | inl _  = inl unit
        sep x | inr ¬p = inr (x , ¬p)

        abstract
          sep-unite : ∀ x → sep (unite-pt X x) == x
          sep-unite (inl _) with dec (pt X)
          sep-unite (inl _) | inl _  = idp
          sep-unite (inl _) | inr ¬p = ⊥-rec (¬p idp)
          sep-unite (inr (x , ¬p)) with dec x
          sep-unite (inr (x , ¬p)) | inl p   = ⊥-rec (¬p p)
          sep-unite (inr (x , ¬p)) | inr ¬p' = ap inr $ pair= idp (prop-has-all-paths ¬-is-prop ¬p' ¬p)

          unite-sep : ∀ x → unite-pt X (sep x) == x
          unite-sep x with dec x
          unite-sep x | inl p = p
          unite-sep x | inr ¬p = idp

    disjoint-pt-is-separable : {X : Ptd i}
      → has-disjoint-pt X → is-separable X
    disjoint-pt-is-separable unite-ise x with unite.g x | unite.f-g x
      where module unite = is-equiv unite-ise
    disjoint-pt-is-separable unite-ise x | inl unit       | p   = inl p
    disjoint-pt-is-separable unite-ise x | inr (y , pt≠y) | y=x = inr λ pt=x → pt≠y (pt=x ∙ ! y=x)

  separable-unite-equiv : ∀ {X}
    → is-separable X
    → (⊤ ⊔ MinusPoint X ≃ de⊙ X)
  separable-unite-equiv dX = _ , separable-has-disjoint-pt dX

module _ {i j k} n (A : Type i) (B : Type j) where
  abstract
    ⊔-has-choice-implies-inr-has-choice : has-choice n (A ⊔ B) k → has-choice n B k
    ⊔-has-choice-implies-inr-has-choice ⊔-ac W =
      transport is-equiv (λ= lemma₃)
        (snd lemma₂ ∘ise ⊔-ac W' ∘ise is-equiv-inverse (snd (Trunc-emap n lemma₁))) where
          W' : A ⊔ B → Type k
          W' (inl _) = Lift {j = k} ⊤
          W' (inr b) = W b

          lemma₁ : Π (A ⊔ B) W' ≃ Π B W
          lemma₁ = equiv to from to-from from-to where
            to : Π (A ⊔ B) W' → Π B W
            to f b = f (inr b)

            from : Π B W → Π (A ⊔ B) W'
            from f (inl a) = lift tt
            from f (inr b) = f b

            abstract
              to-from : ∀ f → to (from f) == f
              to-from f = λ= λ b → idp

              from-to : ∀ f → from (to f) == f
              from-to f = λ= λ{(inl a) → idp; (inr b) → idp}

          lemma₂ : Π (A ⊔ B) (Trunc n ∘ W') ≃ Π B (Trunc n ∘ W)
          lemma₂ = equiv to from to-from from-to where
            to : Π (A ⊔ B) (Trunc n ∘ W') → Π B (Trunc n ∘ W)
            to f b = f (inr b)

            from : Π B (Trunc n ∘ W) → Π (A ⊔ B) (Trunc n ∘ W')
            from f (inl a) = [ lift tt ]
            from f (inr b) = f b

            abstract
              to-from : ∀ f → to (from f) == f
              to-from f = λ= λ b → idp

              from-to : ∀ f → from (to f) == f
              from-to f = λ= λ{
                (inl a) → Trunc-elim
                  {P = λ t → [ lift tt ] == t}
                  (λ _ → =-preserves-level Trunc-level)
                  (λ _ → idp) (f (inl a));
                (inr b) → idp}

          lemma₃ : ∀ f → –> lemma₂ (unchoose (<– (Trunc-emap n lemma₁) f)) == unchoose f
          lemma₃ = Trunc-elim
            {P = λ f → –> lemma₂ (unchoose (<– (Trunc-emap n lemma₁) f)) == unchoose f}
            (λ _ → =-preserves-level (Π-level λ _ → Trunc-level))
            (λ f → λ= λ b → idp)

module _ {i j} n {X : Ptd i} (X-sep : has-disjoint-pt X) where
  abstract
    MinusPoint-has-choice : has-choice n (de⊙ X) j → has-choice n (MinusPoint X) j
    MinusPoint-has-choice X-ac =
      ⊔-has-choice-implies-inr-has-choice n ⊤ (MinusPoint X) $
        transport! (λ A → has-choice n A j) (ua (_ , X-sep)) X-ac

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda