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

module Type.Cubical.Quotient where

open import Functional
import      Lvl
open import Structure.Type.Identity
open import Type.Cubical
open import Type.Cubical.Path.Equality
open import Type
open import Syntax.Function

private variable ℓ ℓₗ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x y : T
private variable P : T → Type{ℓ}
private variable _▫_ : T → T → Type{ℓ}

data Quotient(_▫_ : T → T → Type{ℓ}) : Type{Lvl.of(T) Lvl.⊔ ℓ} where
  class : T → Quotient(_▫_)
  class-extensionalityₗ : (class x ≡ class y) ← (x ▫ y)

open import Type.Cubical.Path
open import Type.Cubical.Univalence
open import Type.Properties.MereProposition
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties

module _ (P : Quotient(_▫_) → Type{ℓ}) ⦃ prop-P : ∀{c} → MereProposition(P(c)) ⦄ where
  Quotient-property-pathP : ∀{x y}{px : P(x)}{py : P(y)} → (xy : x ≡ y) → PathP(\i → P(xy i)) px py
  Quotient-property-pathP {x}{y}{px}{py} xy = IdentityEliminator.elim Path-identity-eliminator (xy ↦ (∀{px}{py} → PathP(\i → P(xy i)) px py)) (\{c} → uniqueness(P(c))) {x}{y} xy {px}{py}

  class-property : (∀{a} → P(class a)) → (∀{c} → P(c))
  class-property p {class a} = p{a}
  class-property p {class-extensionalityₗ {x} {y} xy i} = Quotient-property-pathP {px = p{x}}{py = p{y}} (class-extensionalityₗ xy) i

-- TODO: Use Structuve.Function.Surjective when it is generalized to support Type.Cubical.Logic.∃. The difference is that Type.Cubical.Logic.∃ is a mere propositions while surjective uses existence defined as Σ which is not
open import Type.Cubical.Logic
class-surjective : ∀{y} → ∃(x ↦ class{_▫_ = _▫_} x ≡ y)
class-surjective{_▫_ = _▫_} = class-property(y ↦ ∃(x ↦ class{_▫_ = _▫_} x ≡ y)) (\{a} → [∃]-intro a ⦃ reflexivity(_≡_) ⦄)

-- Note: The following holds by definition: ∀{P : (A → B) → Type{ℓ}}{f}{p} → P(f) → P(Quotient-recursion f p ∘ class).
Quotient-recursion : (f : A → B) → (∀{a b} → (a ▫ b) → (f(a) ≡ f(b))) → (Quotient(_▫_) → B)
Quotient-recursion f _ (class x) = f(x)
Quotient-recursion _ p (class-extensionalityₗ xy i) = p xy i

module _ where
  open import Structure.Function
  open import Structure.Setoid

  Quotient-function : ∀{ℓₑ₁ ℓₑ₂}{equiv-A : Equiv{ℓₑ₁}(A)}{equiv-B : Equiv{ℓₑ₂}(B)} ⦃ sub : (Equiv._≡_ equiv-B) ⊆₂ Path ⦄ (f : A → B) ⦃ func : Function ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ f ⦄ → (Quotient(Equiv._≡_ equiv-A) → B)
  Quotient-function {equiv-B = equiv-B} f(x) = Quotient-recursion f (sub₂(Equiv._≡_ equiv-B)(Path) ∘ congruence₁ ⦃ _ ⦄ ⦃ _ ⦄ (f)) x

module _ ⦃ equivalence : Equivalence(_▫_) ⦄ ⦃ prop : ∀{x y} → MereProposition(x ▫ y) ⦄ where
  class-extensionalityᵣ : (class{_▫_ = _▫_} x ≡ class y) → (x ▫ y)
  class-extensionalityᵣ {x = x} {y = y} p = sub₂(_≡_)(_→ᶠ_) ⦃ Path-coercion ⦄ xx-xy (reflexivity(_▫_)) where
    xx-xy : (x ▫ x) ≡ (x ▫ y)
    xx-xy i = Quotient-recursion (x ▫_) (\ab → propositional-extensionalityₗ ([↔]-intro (swap(transitivity(_▫_)) (symmetry(_▫_) ab)) (swap(transitivity(_▫_)) ab))) (p i)

  class-extensionality : (class{_▫_ = _▫_} x ≡ class y) ↔ (x ▫ y)
  class-extensionality = [↔]-intro class-extensionalityₗ class-extensionalityᵣ

module Syntax where
  _/_ : (T : Type{ℓ}) → (T → T → Type{ℓₗ}) → Type
  _ / (_▫_) = Quotient(_▫_)

  [_] : T → (T / (_▫_))
  [_] = class

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:
-- Solver for Category

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

open import Categories.Category

module Experiment.Categories.AnotherSolver.Category
  {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Relation.Binary using (Rel)
import Function.Base as Fun

open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation renaming (id to idN)
import Categories.Morphism.Reasoning as MR
import Categories.Category.Equivalence as Eq

open Category 𝒞
open HomReasoning
open MR 𝒞

private
  variable
    A B C D E : Obj

infixr 9 _:∘_

data Expr : Rel Obj (o ⊔ ℓ) where
  :id  : Expr A A
  _:∘_ : Expr B C → Expr A B → Expr A C
  ∥_∥  : A ⇒ B → Expr A B

data NExpr : Rel Obj (o ⊔ ℓ) where
  :id  : NExpr A A
  _:∘_ : B ⇒ C → NExpr A B → NExpr A C

-- Semantics
⟦_⟧ : Expr A B → A ⇒ B
⟦ :id      ⟧ = id
⟦ e₁ :∘ e₂ ⟧ = ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧
⟦ ∥ f ∥    ⟧ = f

⟦_⟧N : NExpr A B → A ⇒ B
⟦ :id    ⟧N = id
⟦ f :∘ e ⟧N = f ∘ ⟦ e ⟧N

_∘N_ : NExpr B C → NExpr A B → NExpr A C
:id       ∘N e₂ = e₂
(f :∘ e₁) ∘N e₂ = f :∘ (e₁ ∘N e₂)

linear : NExpr A B → Expr A B
linear :id      = :id
linear (f :∘ e) = ∥ f ∥ :∘ linear e

normalise : Expr A B → NExpr A B
normalise :id        = :id
normalise (e₁ :∘ e₂) = normalise e₁ ∘N normalise e₂
normalise ∥ f ∥      = f :∘ :id

∘N-homo : (e₁ : NExpr B C) (e₂ : NExpr A B) → ⟦ e₁ ∘N e₂ ⟧N ≈ ⟦ e₁ ⟧N ∘ ⟦ e₂ ⟧N
∘N-homo :id       e₂ = sym identityˡ
∘N-homo (f :∘ e₁) e₂ = pushʳ (∘N-homo e₁ e₂)

NExpr-assoc : {f : NExpr A B} {g : NExpr B C} {h : NExpr C D} →
              ⟦ (h ∘N g) ∘N f ⟧N ≈ ⟦ h ∘N (g ∘N f) ⟧N
NExpr-assoc {f = f} {g} {:id}    = refl
NExpr-assoc {f = f} {g} {x :∘ h} = ∘-resp-≈ʳ (NExpr-assoc {f = f} {g} {h})

NExpr-identityʳ : {f : NExpr A B} → ⟦ f ∘N :id ⟧N ≈ ⟦ f ⟧N
NExpr-identityʳ {f = :id}    = refl
NExpr-identityʳ {f = x :∘ f} = ∘-resp-≈ʳ (NExpr-identityʳ {f = f})

normalise-correct : (e : Expr A B) → ⟦ normalise e ⟧N ≈ ⟦ e ⟧
normalise-correct :id        = refl
normalise-correct (e₁ :∘ e₂) = begin
  ⟦ normalise e₁ ∘N normalise e₂ ⟧N     ≈⟨ ∘N-homo (normalise e₁) (normalise e₂) ⟩
  ⟦ normalise e₁ ⟧N ∘ ⟦ normalise e₂ ⟧N ≈⟨ normalise-correct e₁ ⟩∘⟨ normalise-correct e₂ ⟩
  ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧                       ∎
normalise-correct ∥ f ∥      = identityʳ

normalise-cong : (e₁ e₂ : Expr A B) →
                 ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧ → ⟦ normalise e₁ ⟧N ≈ ⟦ normalise e₂ ⟧N
normalise-cong e₁ e₂ eq = trans (normalise-correct e₁) (trans eq (sym (normalise-correct e₂)))

normalise-inj : (e₁ e₂ : Expr A B) →
                ⟦ normalise e₁ ⟧N ≈ ⟦ normalise e₂ ⟧N → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
normalise-inj e₁ e₂ eq = trans (sym (normalise-correct e₁)) (trans eq (normalise-correct e₂))

linear-correct : (e : NExpr A B) → ⟦ linear e ⟧ ≈ ⟦ e ⟧N
linear-correct :id      = refl
linear-correct (f :∘ e) = ∘-resp-≈ʳ (linear-correct e)

Expr-category : Category o (o ⊔ ℓ) e
Expr-category = categoryHelper record
  { Obj       = Obj
  ; _⇒_       = Expr
  ; _≈_       = λ e₁ e₂ → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
  ; id        = :id
  ; _∘_       = _:∘_
  ; assoc     = assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }

NExpr-category : Category o (o ⊔ ℓ) e
NExpr-category = categoryHelper record
  { Obj       = Obj
  ; _⇒_       = NExpr
  ; _≈_       = λ e₁ e₂ → ⟦ e₁ ⟧N ≈ ⟦ e₂ ⟧N
  ; id        = :id
  ; _∘_       = _∘N_
  ; assoc     = λ {_} {_} {_} {_} {f = f} {g} {h} → NExpr-assoc {f = f} {g} {h}
  ; identityˡ = refl
  ; identityʳ = λ {_} {_} {f = f} → NExpr-identityʳ {f = f}
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = λ {_} {_} {_} {f} {h} {g} {i} f≈h g≈i →
    trans (∘N-homo f g) (trans (∘-resp-≈ f≈h g≈i) (sym (∘N-homo h i)))
  }

⟦⟧-functor : Functor Expr-category 𝒞
⟦⟧-functor = record
  { F₀           = Fun.id
  ; F₁           = ⟦_⟧
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = Fun.id
  }

⟦⟧N-functor : Functor NExpr-category 𝒞
⟦⟧N-functor = record
  { F₀           = Fun.id
  ; F₁           = ⟦_⟧N
  ; identity     = refl
  ; homomorphism = λ {_} {_} {_} {f} {g} → ∘N-homo g f
  ; F-resp-≈     = Fun.id
  }

normalise-functor : Functor Expr-category NExpr-category
normalise-functor = record
  { F₀           = Fun.id
  ; F₁           = normalise
  ; identity     = refl
  ; homomorphism = λ {_} {_} {_} {f = f} {g} → refl
  ; F-resp-≈     = λ {_} {_} {f} {g} f≈g → normalise-cong f g f≈g
  }

linear-functor : Functor NExpr-category Expr-category
linear-functor = record
  { F₀           = Fun.id
  ; F₁           = linear
  ; identity     = refl
  ; homomorphism = λ {_} {_} {_} {f} {g} → begin
    ⟦ linear (g ∘N f) ⟧         ≈⟨ linear-correct (g ∘N f) ⟩
    ⟦ g ∘N f ⟧N                 ≈⟨ ∘N-homo g f ⟩
    ⟦ g ⟧N ∘ ⟦ f ⟧N             ≈⟨ sym (linear-correct g) ⟩∘⟨ sym (linear-correct f) ⟩
    ⟦ linear g ⟧ ∘ ⟦ linear f ⟧ ∎
  ; F-resp-≈     = λ {_} {_} {f} {g} eq → begin
    ⟦ linear f ⟧ ≈⟨ linear-correct f ⟩
    ⟦ f ⟧N       ≈⟨ eq ⟩
    ⟦ g ⟧N       ≈⟨ sym (linear-correct g) ⟩
    ⟦ linear g ⟧ ∎
  }

normalise-functor-Faithful : Faithful normalise-functor
normalise-functor-Faithful = normalise-inj

linear-functor-Faithful : Faithful linear-functor
linear-functor-Faithful = λ f g x → trans (sym (linear-correct f)) (trans x (linear-correct g))

⟦⟧n-functor : Functor Expr-category 𝒞
⟦⟧n-functor = ⟦⟧N-functor ∘F normalise-functor

⟦⟧l-functor : Functor NExpr-category 𝒞
⟦⟧l-functor = ⟦⟧-functor ∘F linear-functor

normalise-natural : NaturalTransformation ⟦⟧n-functor ⟦⟧-functor
normalise-natural = ntHelper record
    { η       = λ X → id
    ; commute = λ e → begin
      id ∘ ⟦ normalise e ⟧N ≈⟨ identityˡ ⟩
      ⟦ normalise e ⟧N      ≈⟨ normalise-correct e ⟩
      ⟦ e ⟧                 ≈⟨ sym identityʳ ⟩
      ⟦ e ⟧ ∘ id           ∎
    }

linear-natural : NaturalTransformation ⟦⟧l-functor ⟦⟧N-functor
linear-natural = ntHelper record
  { η       = λ X → id
  ; commute = λ e → trans identityˡ (trans (linear-correct e) (sym identityʳ))
  }

embedExpr : Functor 𝒞 Expr-category
embedExpr = record
  { F₀           = Fun.id
  ; F₁           = ∥_∥
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = Fun.id
  }

embedNExpr : Functor 𝒞 NExpr-category
embedNExpr = record
  { F₀           = Fun.id
  ; F₁           = λ e → e :∘ :id
  ; identity     = identity²
  ; homomorphism = λ {_} {_} {_} {f} {g} → assoc
  ; F-resp-≈     = λ f≈g → trans identityʳ (trans f≈g (sym identityʳ))
  }

{-
solve : (e₁ e₂ : Expr A B) → ⟦ e₁ ⟧N ≈ ⟦ e₂ ⟧N → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
solve e₁ e₂ eq = begin
  ⟦ e₁ ⟧  ≈˘⟨ ⟦e⟧N≈⟦e⟧ e₁ ⟩
  ⟦ e₁ ⟧N ≈⟨ eq ⟩
  ⟦ e₂ ⟧N ≈⟨ ⟦e⟧N≈⟦e⟧ e₂ ⟩
  ⟦ e₂ ⟧  ∎

∥-∥ : ∀ {f : A ⇒ B} → Expr A B
∥-∥ {f = f} = ∥ f ∥
-}

ext: agda


text:
module Luau.TypeNormalization where

open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)

-- Operations on normalized types
_∪ᶠ_ : Type → Type → Type
_∪ⁿˢ_ : Type → Type → Type
_∩ⁿˢ_ : Type → Type → Type
_∪ⁿ_ : Type → Type → Type
_∩ⁿ_ : Type → Type → Type

-- Union of function types
(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
F ∪ᶠ (G₁ ∩ G₂) = (F ∪ᶠ G₁) ∩ (F ∪ᶠ G₂)
(R ⇒ S) ∪ᶠ (T ⇒ U) = (R ∩ⁿ T) ⇒ (S ∪ⁿ U)
F ∪ᶠ G = F ∪ G

-- Union of normalized types
S ∪ⁿ (T₁ ∪ T₂) = (S ∪ⁿ T₁) ∪ T₂
S ∪ⁿ unknown = unknown
S ∪ⁿ never = S
never ∪ⁿ T = T
unknown ∪ⁿ T = unknown
(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
F ∪ⁿ G = F ∪ᶠ G

-- Intersection of normalized types
S ∩ⁿ (T₁ ∪ T₂) = (S ∩ⁿ T₁) ∪ⁿˢ (S ∩ⁿˢ T₂)
S ∩ⁿ unknown = S
S ∩ⁿ never = never
(S₁ ∪ S₂) ∩ⁿ G = (S₁ ∩ⁿ G)
unknown ∩ⁿ G = G
never ∩ⁿ G = never
F ∩ⁿ G = F ∩ G

-- Intersection of normalized types with a scalar
(S₁ ∪ nil) ∩ⁿˢ nil = nil
(S₁ ∪ boolean) ∩ⁿˢ boolean = boolean
(S₁ ∪ number) ∩ⁿˢ number = number
(S₁ ∪ string) ∩ⁿˢ string = string
(S₁ ∪ S₂) ∩ⁿˢ T = S₁ ∩ⁿˢ T
unknown ∩ⁿˢ T = T
F ∩ⁿˢ T = never

-- Union of normalized types with an optional scalar
S ∪ⁿˢ never = S
unknown ∪ⁿˢ T = unknown
(S₁ ∪ nil) ∪ⁿˢ nil = S₁ ∪ nil
(S₁ ∪ boolean) ∪ⁿˢ boolean = S₁ ∪ boolean
(S₁ ∪ number) ∪ⁿˢ number = S₁ ∪ number
(S₁ ∪ string) ∪ⁿˢ string = S₁ ∪ string
(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₂
F ∪ⁿˢ T = F ∪ T

-- Normalize!
normalize : Type → Type
normalize nil = never ∪ nil
normalize (S ⇒ T) = (normalize S ⇒ normalize T)
normalize never = never
normalize unknown = unknown
normalize boolean = never ∪ boolean
normalize number = never ∪ number
normalize string = never ∪ string
normalize (S ∪ T) = normalize S ∪ⁿ normalize T
normalize (S ∩ T) = normalize S ∩ⁿ normalize T

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


text:
-- Andreas, 2013-10-21
-- There was a bug in Rules/Builtin such that NATEQUALS' equations
-- would be checked at type Nat instead of Bool.
-- This bug surfaced only because of today's refactoring in Conversion,
-- because then I got a strange unsolved constraint  true == true : Nat.

module NatEquals where

import Common.Level

data Bool : Set where
  true false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

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

{-# BUILTIN NATURAL Nat #-}

infix 40 _=?=_

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

{-# BUILTIN NATEQUALS _=?=_ #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.List.Sugar where

open import Data.List.Base
open import Prelude

[_] : A → List A
[ x ] = x ∷ []

pure : A → List A
pure = [_]

_>>=_ : List A → (A → List B) → List B
_>>=_ = flip concatMap

_>>_ : List A → List B → List B
xs >> ys = xs >>= const ys

_<*>_ : List (A → B) → List A → List B
fs <*> xs = do
  f ← fs
  x ← xs
  [ f x ]

guard : Bool → List ⊤
guard false = []
guard true  = [ tt ]

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

module Data.Dyck.Payload where

open import Prelude
open import Data.Nat using (_+_)
open import Data.Vec.Iterated using (Vec; _∷_; []; foldlN; head)

private
  variable
    n : ℕ

--------------------------------------------------------------------------------
-- Binary trees: definition and associated functions
--------------------------------------------------------------------------------

infixl 6 _*_
data Tree (A : Type a) : Type a where
  [_] : A → Tree A
  _*_ : Tree A → Tree A → Tree A

--------------------------------------------------------------------------------
-- Dyckrams: definition and associated functions
--------------------------------------------------------------------------------

infixr 5 ⟨_!_ ⟩_
data Dyck (A : Type a) : ℕ → Type a where
  ⟩⋆   : Dyck A 1
  ⟨_!_ : A → Dyck A (1 + n) → Dyck A n
  ⟩_   : Dyck A (1 + n) → Dyck A (2 + n)

--------------------------------------------------------------------------------
-- Conversion from a Dyck to a Tree
--------------------------------------------------------------------------------

dyck→tree⊙ : Dyck A n → Vec (Tree A) n → Tree A
dyck→tree⊙ ⟩⋆         (v ∷ [])       = v
dyck→tree⊙ (⟨ v ! is) st             = dyck→tree⊙ is ([ v ] ∷ st)
dyck→tree⊙ (⟩     is) (t₁ ∷ t₂ ∷ st) = dyck→tree⊙ is (t₂ * t₁ ∷ st)

dyck→tree : Dyck A zero → Tree A
dyck→tree ds = dyck→tree⊙ ds []

--------------------------------------------------------------------------------
-- Conversion from a Tree to a Dyck
--------------------------------------------------------------------------------

tree→dyck⊙ : Tree A → Dyck A (suc n) → Dyck A n
tree→dyck⊙ [ x ]     = ⟨ x !_
tree→dyck⊙ (xs * ys) = tree→dyck⊙ xs ∘ tree→dyck⊙ ys ∘ ⟩_

tree→dyck : Tree A → Dyck A zero
tree→dyck tr = tree→dyck⊙ tr ⟩⋆

--------------------------------------------------------------------------------
-- Proof of isomorphism
--------------------------------------------------------------------------------

tree→dyck→tree⊙ :  {is : Dyck A (1 + n)} {st : Vec (Tree A) n} (e : Tree A) →
  dyck→tree⊙ (tree→dyck⊙ e is) st ≡ dyck→tree⊙ is (e ∷ st)
tree→dyck→tree⊙ [ x ]     = refl
tree→dyck→tree⊙ (xs * ys) = tree→dyck→tree⊙ xs ; tree→dyck→tree⊙ ys

dyck→tree→dyck⊙ :  {st : Vec (Tree A) n} (is : Dyck A n) →
 tree→dyck (dyck→tree⊙ is st) ≡ foldlN (Dyck A) tree→dyck⊙ is st
dyck→tree→dyck⊙  ⟩⋆        = refl
dyck→tree→dyck⊙ (⟨ v ! is) = dyck→tree→dyck⊙ is
dyck→tree→dyck⊙ (⟩     is) = dyck→tree→dyck⊙ is

dyck-iso : Dyck A zero ⇔ Tree A
dyck-iso .fun = dyck→tree
dyck-iso .inv = tree→dyck
dyck-iso .rightInv = tree→dyck→tree⊙
dyck-iso .leftInv  = dyck→tree→dyck⊙

_ : tree→dyck (([ 1 ] * ([ 2 ] * [ 3 ])) * [ 4 ]) ≡ ⟨ 1 ! ⟨ 2 ! ⟨ 3 ! ⟩ ⟩ ⟨ 4 ! ⟩ ⟩⋆
_ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2019-11-08, issue #4154 reported by Yashmine Sharoda.

-- Warn if a `renaming` clause clashes with an exported name
-- (that is not mentioned in a `using` clause).

module _ where

module M where
  postulate
    A B : Set

-- These produce warnings (#4154):

module N = M renaming (A to B)
open M renaming (A to B)

-- These produce errors (see also #3057)
-- as they produce ambiguous exports:

Test = B
TestN = N.B
module L = M using (B) renaming (A to B)


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

module Issue2442-postulate where

postulate

  A : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module FT-Nat where

open import Data.Empty
open import Data.Unit
open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Sum renaming (map to _⊎→_)
open import Data.Product
import Data.Fin as F
open import Data.Vec
import Data.List as L
open import Function renaming (_∘_ to _○_)

open import FT
open import SimpleHoTT using (refl; pathInd; _≡_; ap)
open import Equivalences
open import TypeEquivalences using (path⊎)
open import Path2Equiv
open import LeftCancellation

------------------------------------------------------------------
-- Finite Types and the natural numbers are intimately related.
--
-- Basically, this is because both of them are models of
-- unital semirings, and the natural numbers are the initial object
-- in the category of unital semirings.  In this case, things are
-- deeper still, and so we record many of these facts here.
--
-- And, of course, as Pi records the proof-theory of semirings in
-- a fairly explicit manner, we can use all this to link up
-- normalization of natural-numbers expressions and Pi-based paths.

toℕ : FT → ℕ
toℕ ZERO = zero
toℕ ONE = suc zero
toℕ (PLUS b₀ b₁) = (toℕ b₀) + (toℕ b₁)
toℕ (TIMES b₀ b₁) = (toℕ b₀) * (toℕ b₁)

fromℕ : ℕ → FT
fromℕ zero = ZERO
fromℕ (suc n) = PLUS ONE (fromℕ n)

toℕ∘fromℕ : toℕ ○ fromℕ ∼ id
toℕ∘fromℕ zero = refl zero
toℕ∘fromℕ (suc n) =
  pathInd
    (λ {x} {y} _ → suc x ≡ suc y)
    (λ m → refl (suc m))
    (toℕ∘fromℕ n)

assocr : {m : ℕ} (n : ℕ) → (PLUS (fromℕ n) (fromℕ m)) ⇛ fromℕ (n + m)
assocr zero = unite₊⇛
assocr (suc n) = assocr₊⇛ ◎ (id⇛ ⊕ (assocr n))

distr : (n₀ : ℕ) {n₁ : ℕ} → TIMES (fromℕ n₀) (fromℕ n₁) ⇛ fromℕ (n₀ * n₁)
distr zero = distz⇛
distr (suc n) {m} = dist⇛ ◎ (unite⋆⇛ ⊕ distr n) ◎ assocr m

-- normalize a finite type to (1 + (1 + (1 + ... + (1 + 0) ... )))
-- a bunch of ones ending with zero with left biased + in between

normalize : FT → FT
normalize = fromℕ ○ toℕ

normal : (b : FT) → b ⇛ normalize b
normal ZERO = id⇛
normal ONE = uniti₊⇛ ◎ swap₊⇛
normal (PLUS b₀ b₁) = (normal b₀ ⊕ normal b₁) ◎ assocr (toℕ b₀)
normal (TIMES b₀ b₁) = (normal b₀ ⊗ normal b₁) ◎ distr (toℕ b₀)

normalizeC : {B : FT} → ⟦ normalize B ⟧ ≃ ⟦ B ⟧
normalizeC {B} = path2equiv (sym⇛ (normal B))

mapNorm :  {B₁ B₂ : FT} → (⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧) → ⟦ normalize B₁ ⟧ ≃ ⟦ normalize B₂ ⟧
mapNorm {B₁} {B₂} eq = trans≃ (trans≃ (normalizeC {B₁}) eq) (sym≃ (normalizeC {B₂}))

⟦_⟧ℕ : ℕ → Set
⟦ zero ⟧ℕ = ⊥
⟦ suc n ⟧ℕ = ⊤ ⊎ ⟦ n ⟧ℕ

ℕrespects⟦⟧ : {n : ℕ} → ⟦ fromℕ n ⟧ ≃ ⟦ n ⟧ℕ
ℕrespects⟦⟧ {zero} = id≃
ℕrespects⟦⟧ {suc n} = path⊎ id≃ (ℕrespects⟦⟧ {n})

------------------------------------------------------------------------------
-- Understanding the syntactic structure of pi combinators with respect
-- to normalization

data FTNF : Set where
  Z : FTNF
  S : FTNF → FTNF

fromℕNF : ℕ → FTNF
fromℕNF zero = Z
fromℕNF (suc n) = S (fromℕNF n)

normalizeNF : FT → FTNF
normalizeNF = fromℕNF ○ toℕ

data FTN : FT → Set where
  normalized : (b : FT) → FTN (normalize b)

-- in both the following two functions we are missing fundamental information
-- about how a type relates to its normal form...

{--
normalize⇛ : {b₁ b₂ : FT} → (b₁ ⇛ b₂) → (normalize b₁ ⇛ normalize b₂)
normalize⇛ unite₊⇛ = id⇛
normalize⇛ uniti₊⇛ = id⇛
normalize⇛ swap₊⇛ = {!!}
normalize⇛ assocl₊⇛ = {!!}
normalize⇛ assocr₊⇛ = {!!}
normalize⇛ unite⋆⇛ = {!!}
normalize⇛ uniti⋆⇛ = {!!}
normalize⇛ swap⋆⇛ = {!!}
normalize⇛ assocl⋆⇛ = {!!}
normalize⇛ assocr⋆⇛ = {!!}
normalize⇛ distz⇛ = id⇛
normalize⇛ factorz⇛ = id⇛
normalize⇛ dist⇛ = {!!}
normalize⇛ factor⇛ = {!!}
normalize⇛ id⇛ = id⇛
normalize⇛ (sym⇛ c) = sym⇛ (normalize⇛ c)
normalize⇛ (c₁ ◎ c₂) = normalize⇛ c₁ ◎ normalize⇛ c₂
normalize⇛ (c ⊕ c₁) = {!!}
normalize⇛ (c ⊗ c₁) = {!!}
--}

{--
swapii+1 : {b : FT} → (i : ℕ) → (b ⇛ b)
swapii+1 {PLUS ONE (PLUS ONE b)} 0 =
  (assocl₊⇛ {ONE} {ONE} {b}) ◎ (swap₊⇛ ⊕ id⇛) ◎ (assocr₊⇛ {ONE} {ONE} {b})
swapii+1 {PLUS ONE b} (suc n) = id⇛ ⊕ swapii+1 n
swapii+1 _ = {!!}
--}
------------------------------------------------------------------------------

-- needs LeftCancellation

liftℕ : (n₁ n₂ : ℕ) → ⟦ n₁ ⟧ℕ ≃ ⟦ n₂ ⟧ℕ → (fromℕ n₁) ≡ (fromℕ n₂)
liftℕ zero zero eq = refl ZERO
liftℕ zero (suc n₂) (_ , mkisequiv g α h β) with h (inj₁ tt)
liftℕ zero (suc n₂) (_ , mkisequiv g α h β) | ()
liftℕ (suc n₁) zero (f , _) with f (inj₁ tt)
liftℕ (suc n₁) zero (f , _) | ()
liftℕ (suc n₁) (suc n₂) eq = ap (λ x → PLUS ONE x) (liftℕ n₁ n₂ (left-cancel-⊤ eq))

liftNormal : {B₁ B₂ : FT} →  ⟦ normalize B₁ ⟧ ≃ ⟦ normalize B₂ ⟧ → (normalize B₁) ≡ (normalize B₂)
liftNormal {B₁} {B₂} eq =
  liftℕ (toℕ B₁) (toℕ B₂)
    (⟦ toℕ B₁ ⟧ℕ ≃⟨ sym≃ (ℕrespects⟦⟧ {toℕ B₁}) ⟩ ⟦ normalize B₁ ⟧ ≃⟨ eq ⟩ ⟦ normalize B₂ ⟧ ≃⟨ ℕrespects⟦⟧ {toℕ B₂} ⟩ id≃)

sameNorm : {B₁ B₂ : FT} → (⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧) → (normalize B₁) ≡ (normalize B₂)
sameNorm {B₁} {B₂} eq = liftNormal {B₁} {B₂} (mapNorm eq)

bridge : {B₁ B₂ : FT} → (⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧) → (normalize B₁) ⇛ (normalize B₂)
bridge eq =
  pathInd
    (λ {B₃} {B₄} _ → B₃ ⇛ B₄)
    (λ _ → id⇛)
    (sameNorm eq)

{--

Not used

exf : ⊤ ⊎ ℕ → ℕ
exf (inj₁ tt) = 0
exf (inj₂ n) = suc n

exg : ℕ → ⊤ ⊎ ℕ
exg 0 = inj₁ tt
exg (suc n) = inj₂ n

exα : exf ○ exg ∼ id
exα 0 = refl 0
exα (suc n) = refl (suc n)

exβ : exg ○ exf ∼ id
exβ (inj₁ tt) = refl (inj₁ tt)
exβ (inj₂ n) = refl (inj₂ n)

ex : (⊤ ⊎ ℕ) ≃ ℕ
ex = (exf , equiv₁ (mkqinv exg exα exβ))

exf2 : (⊤ ⊎ (⊤ ⊎ ℕ)) → (⊤ ⊎ ℕ)
exf2 (inj₁ tt) = inj₂ 0
exf2 (inj₂ (inj₁ tt)) = inj₂ 1
exf2 (inj₂ (inj₂ 0)) = inj₁ tt
exf2 (inj₂ (inj₂ (suc n))) = inj₂ (suc (suc n))

exg2 : (⊤ ⊎ ℕ) → (⊤ ⊎ (⊤ ⊎ ℕ))
exg2 (inj₁ tt) = inj₂ (inj₂ 0)
exg2 (inj₂ 0) = inj₁ tt
exg2 (inj₂ 1) = inj₂ (inj₁ tt)
exg2 (inj₂ (suc (suc n))) = inj₂ (inj₂ (suc n))

exα2 : exf2 ○ exg2 ∼ id
exα2 (inj₁ tt) = refl (inj₁ tt)
exα2 (inj₂ 0) = refl (inj₂ 0)
exα2 (inj₂ 1) = refl (inj₂ 1)
exα2 (inj₂ (suc (suc n))) = refl (inj₂ (suc (suc n)))

exβ2 : exg2 ○ exf2 ∼ id
exβ2 (inj₁ tt) = refl (inj₁ tt)
exβ2 (inj₂ (inj₁ tt)) = refl (inj₂ (inj₁ tt))
exβ2 (inj₂ (inj₂ 0)) = refl (inj₂ (inj₂ 0))
exβ2 (inj₂ (inj₂ (suc n))) = refl (inj₂ (inj₂ (suc n)))

ex2 : (⊤ ⊎ (⊤ ⊎ ℕ)) ≃ (⊤ ⊎ ℕ)
ex2 = (exf2 , equiv₁ (mkqinv exg2 exα2 exβ2))

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Andreas, 2016-12-31, re issue #1976
-- Allow projection pattern disambiguation by parameters

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

postulate
  A B : Set

module M (_ : Set) where

  record R : Set₂ where
    field
      F : Set₁

  open R public

module Succeeds where
  open M _
  open M B

  test : M.R B
  F test = Set

module ShouldFail where
  open M A
  open M _

  test : M.R B
  F test = Set  -- should fail

module Fails where
  open M _
  open M A

  test : M.R B
  F test = Set

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module 747Connectives where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)

-- Copied from 747Isomorphism.

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃  -- This has been added, not in PLFA
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

-- You may copy over the various reasoning modules if you wish.

-- End of code from 747Isomorphism.

-- Logical AND is Cartesian product.

data _×_ (A : Set) (B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

-- Destructors (eliminators) for ×.

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A

proj₁ A×B = {!!}

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B

proj₂ A×B = {!!}

-- An easier (equivalent) construction using records.

record _×′_ (A B : Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

-- Eta-equivalence relates constructors and destructors.

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× A×B = {!!}

-- Bool (Booleans), a type with exactly two members.

infixr 2 _×_
data Bool : Set where
  true  : Bool
  false : Bool

-- A type with three members (useful for examples).

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

-- Bool × Tri has six members.
-- Here is a function counting them.

×-count : Bool × Tri → ℕ
×-count ⟨ true  , aa ⟩  =  1
×-count ⟨ true  , bb ⟩  =  2
×-count ⟨ true  , cc ⟩  =  3
×-count ⟨ false , aa ⟩  =  4
×-count ⟨ false , bb ⟩  =  5
×-count ⟨ false , cc ⟩  =  6

-- Cartesian product is commutative and associative up to isomorphism.

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm = {!!}

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc = {!!}

-- 747/PLFA exercise: IffIsoIfOnlyIf (1 point)
-- Show A ⇔ B is isomorphic to (A → B) × (B → A).

iff-iso-if-onlyif : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
iff-iso-if-onlyif = {!!}

-- Logical True is a type with one member (unit)

data ⊤ : Set where

  tt :
    --
    ⊤

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ w = {!!}

⊤-count : ⊤ → ℕ
⊤-count tt = 1

-- Unit is the left and right identity of product.

⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
⊤-identityˡ = {!!}

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
⊤-identityʳ = {!!}

-- Logical OR (disjunction) is sum (disjoint union).

data _⊎_ : Set → Set → Set where

  inj₁ : ∀ {A B : Set}
    → A
      -----
    → A ⊎ B

  inj₂ : ∀ {A B : Set}
    → B
      -----
    → A ⊎ B

-- One way to eliminate a sum.

case-⊎ : ∀ {A B C : Set}
  → (A → C)
  → (B → C)
  → A ⊎ B
    -----------
  → C
case-⊎ f g s = {!!}

-- We typically use pattern-matching to eliminate sums.

-- Eta equivalence for sums.

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ w = {!!}

-- A generalization.

uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
  case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h w = {!!}

infix 1 _⊎_

-- Bool ⊎ Tri has five members

⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true)   =  1
⊎-count (inj₁ false)  =  2
⊎-count (inj₂ aa)     =  3
⊎-count (inj₂ bb)     =  4
⊎-count (inj₂ cc)     =  5

-- 747/PLFA exercise: SumCommIso (1 point)
-- Sum is commutative up to isomorphism.

⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
⊎-comm = {!!}

-- 747/PLFA exercise: SumAssocIso (1 point)
-- Sum is associative up to isomorphism.

⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc = {!!}

-- Logical False is the empty type ("bottom", "empty").

data ⊥ : Set where
  -- no clauses!

-- Ex falso quodlibet "from falsehood, anything follows".

⊥-elim : ∀ {A : Set}
  → ⊥
    --
  → A

⊥-elim w = {!!}

uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h w = {!!}

⊥-count : ⊥ → ℕ
⊥-count w = {!!}

-- 747/PLFA exercise: EmptyLeftIdSumIso (1 point)
-- Empty is the left unit of sum up to isomorphism.

⊎-identityˡ : ∀ {A : Set} → ⊥ ⊎ A ≃ A
⊎-identityˡ = {!!}

-- 747/PLFA exercise: EmptyRightIdSumIso (1 point)
-- Empty is the right unit of sum up to isomorphism.

⊎-identityʳ : ∀ {A : Set} → A ⊎ ⊥ ≃ A
⊎-identityʳ = {!!}

-- Logical implication (if-then) is... the function type constructor!
-- Eliminating an if-then (modus ponens) is function application.

→-elim : ∀ {A B : Set}
  → (A → B)
  → A
    -------
  → B

→-elim L M = L M

-- This works because eta-reduction for → is built in.

η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl

-- The function space A → B is sometimes called the exponential Bᴬ.
-- Bool → Tri has 3² or 9 members.

→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
...          | aa     | aa      =   1
...          | aa     | bb      =   2
...          | aa     | cc      =   3
...          | bb     | aa      =   4
...          | bb     | bb      =   5
...          | bb     | cc      =   6
...          | cc     | aa      =   7
...          | cc     | bb      =   8
...          | cc     | cc      =   9

-- In math,   (p ^ n) ^ m = p ^ (n * m).
-- For types, (A ^ B) ^ C ≃ A ^ (B × C).

-- In a language where functions take multiple parameters,
-- this is called "currying".

currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying = {!!}

-- In math,   p ^ (n + m) = (p ^ n) * (p ^ m).
-- For types, (A ⊎ B → C) ≃ ((A → C) × (B → C)).

→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ = {!!}

-- In math,   (p * n) ^ m = (p ^ m) * (n ^ m).
-- For types, (A → B × C) ≃ (A → B) × (A → C).

→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× = {!!}

-- More distributive laws.

×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ = {!!}

⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× = {!!}

-- Think of a counterexample to show the above isn't an isomorphism.

-- 747/PLFA exercise: ImpProdRightDist (1 point)

×-distrib-→ : ∀ {A B C : Set} → (C → (A × B)) ≃ (C → A) × (C → B)
×-distrib-→ = {!!}

-- 747/PLFA exercise: ImpSumLeftDist (1 point)

⊎-distrib-→ : ∀ {A B C : Set} → ((A ⊎ B) → C) ≃ (A → C) × (B → C)
⊎-distrib-→ = {!!}

-- PLFA exercise: a weak distributive law.
-- ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
-- ⊎-weak-× A⊎B×C = {!!}
-- State and prove the strong law, and explain the relationship.

-- 747/PLFA exercise: SumOfProdImpProdOfSum (1 point)
-- A disjunct of conjuncts implies a conjunct of disjuncts.

⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎ A×B⊎C×D = {!!}

-- PLFA exercise: Is the converse true? If so, prove it; if not, give a counterexample.

-- See PLFA for a number of slight differences with the standard library.

-- Unicode introduced in this chapter:

{-

  ×  U+00D7  MULTIPLICATION SIGN (\x)
  ⊎  U+228E  MULTISET UNION (\u+)
  ⊤  U+22A4  DOWN TACK (\top)
  ⊥  U+22A5  UP TACK (\bot)
  η  U+03B7  GREEK SMALL LETTER ETA (\eta)
  ₁  U+2081  SUBSCRIPT ONE (\_1)
  ₂  U+2082  SUBSCRIPT TWO (\_2)
  ⇔  U+21D4  LEFT RIGHT DOUBLE ARROW (\<=>, \iff, \lr=)

-}

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

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

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


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.HITs.DunceCap.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.S1 using (S¹; base)
import Cubical.HITs.S1 as S¹

open import Cubical.HITs.MappingCones

-- definition of the dunce cap as a HIT

data Dunce : Type₀ where
  base : Dunce
  loop : base ≡ base
  surf : PathP (λ i → loop i ≡ loop i) loop refl

-- definition of the dunce cap as a mapping cone

dunceMap : S¹ → S¹
dunceMap base        = base
dunceMap (S¹.loop i) = (S¹.loop ⁻¹ ∙∙ S¹.loop ∙∙ S¹.loop) i

DunceCone : Type₀
DunceCone = Cone dunceMap

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module agda where
open import IO

main = run (putStrLn "Fuck You Github")

max_stars_repo_name: ozcanyarimdunya/FuckYouGithub

max_issues_repo_name: ozcanyarimdunya/FuckYouGithub

max_forks_repo_name: ozcanyarimdunya/FuckYouGithub


text:
module MLib.Fin.Parts.Nat.Simple where

open import MLib.Prelude
open import MLib.Fin.Parts.Core
open import MLib.Fin.Parts.Nat

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

repl : ∀ n → ℕ → Table ℕ n
repl _ = replicate

-- abstract
-- TODO: why does this break reduction later?
sum-replicate-* : ∀ m n → sum (repl m n) ≡ m * n
sum-replicate-* zero _ = ≡.refl
sum-replicate-* (suc m) _ = ≡.cong₂ _+_ ≡.refl (sum-replicate-* m _)

fromParts : ∀ a b → ℕ × ℕ → ℕ
fromParts a b = Partsℕ.fromParts (constParts a b)

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

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

open ≡.Reasoning

abstract
  fromParts′-a-irrel : ∀ a k b i j → i < a → j < b → fromParts a b (i , j) ≡ fromParts (a + k) b (i , j)
  fromParts′-a-irrel a k b zero j p q = ≡.refl
  fromParts′-a-irrel (suc a) k b (suc i) j (Nat.s≤s p) q = ≡.cong₂ _+_ ≡.refl (fromParts′-a-irrel a k b i j p q)

  fromParts′-0 : ∀ a b i → i < a → fromParts a b (i , 0) ≡ i * b
  fromParts′-0 zero b i ()
  fromParts′-0 (suc a) b zero (Nat.s≤s p) = ≡.refl
  fromParts′-0 (suc a) b (suc i) (Nat.s≤s p) = ≡.cong₂ _+_ ≡.refl (fromParts′-0 a b i p)

  lem′ : ∀ m a b i j → (m * b) + fromParts a b (i , j) ≡ fromParts (m + a) b (m + i , j)
  lem′ zero a b i j = ≡.refl
  lem′ (suc m) a b i j =
    begin
      b + m * b + fromParts a b (i , j)   ≡⟨ Nat.+-assoc b _ _ ⟩
      b + (m * b + fromParts a b (i , j)) ≡⟨ ≡.cong₂ _+_ ≡.refl (lem′ m a b i j) ⟩
      b + fromParts (m + a) b (m + i , j) ∎

  lem : ∀ a b c i k → i < a → fromParts a (b * c) (i , k) ≡ fromParts (a * b) c (i * b , k)
  lem zero b c i k ()
  lem (suc a) b c zero k p = ≡.refl
  lem (suc a) b c (suc i) k (Nat.s≤s p) =
    begin
      (b * c) + fromParts a (b * c) (i , k)      ≡⟨ ≡.cong₂ _+_ ≡.refl (lem a b c i k p) ⟩
      (b * c) + fromParts (a * b) c (i * b , k)  ≡⟨ lem′ b (a * b) c (i * b) k ⟩
      fromParts (suc a * b) c (suc i * b , k)    ∎

  fromParts-assoc :
    ∀ {a b c} i j k → i < a → j < b → k < c →
    fromParts³′ a b c (i , j , k) ≡ fromParts³ a b c (i , j , k)
  fromParts-assoc {a} {b} {c} zero zero k p q r = ≡.refl
  fromParts-assoc {suc a} {suc b} {c} zero (suc j) k (Nat.s≤s p) (Nat.s≤s q) r =
    begin
      fromParts³′ (suc a) (suc b) c (0 , suc j , k)   ≡⟨⟩
      fromParts (suc b) c (suc j , k)                 ≡⟨⟩
      c + fromParts b c (j , k)                       ≡⟨ ≡.cong₂ _+_ ≡.refl (fromParts′-a-irrel b (a * suc b) c j k q r) ⟩
      c + fromParts (b + a * suc b) c (j , k)         ≡⟨⟩
      fromParts (suc (b + a * suc b)) c (suc j , k)   ≡⟨⟩
      fromParts (suc a * suc b) c (suc j , k)         ≡⟨⟩
      fromParts³ (suc a) (suc b) c (0 , suc j , k)    ∎
  fromParts-assoc {zero} {b} {c} (suc i) j k () q r
  fromParts-assoc {suc a} {b} {c} (suc i) zero k (Nat.s≤s p) q r =
    begin
      fromParts³′ (suc a) b c (suc i , 0 , k)   ≡⟨⟩
      fromParts (suc a) (b * c) (suc i , k)   ≡⟨ lem (suc a) b c (suc i) k (Nat.s≤s p) ⟩
      fromParts (suc a * b) c (suc i * b , k) ≡⟨ ≡.cong (λ h → fromParts (suc a * b) c (b + h , k)) (≡.sym (fromParts′-0 a b i p)) ⟩
      fromParts (suc a * b) c (b + fromParts a b (i , 0) , k) ≡⟨⟩
      fromParts (suc a * b) c (fromParts (suc a) b (suc i , 0) , k) ≡⟨⟩
      fromParts³ (suc a) b c (suc i , 0 , k)  ∎
  fromParts-assoc {suc a} {zero} {c} (suc i) (suc j) k p () r
  fromParts-assoc {suc a} {suc b} {c} (suc i) (suc j) k (Nat.s≤s p) q r =
    let sb = suc b
        sj = suc j
    in begin
      fromParts³′ (suc a) sb c (suc i , sj , k)                          ≡⟨⟩
      fromParts (suc a) (sb * c) (suc i , fromParts sb c (sj , k))       ≡⟨⟩
      sb * c + fromParts a (sb * c) (i , c + fromParts b c (j , k))      ≡⟨⟩
      sb * c + fromParts³′  a sb c (i , sj , k)                          ≡⟨ ≡.cong₂ _+_ ≡.refl (fromParts-assoc i sj k p q r) ⟩
      sb * c + fromParts³ a sb c (i , sj , k)                            ≡⟨⟩
      sb * c + fromParts (a * sb) c (fromParts a sb (i , sj) , k)        ≡⟨ Nat.+-assoc c _ _ ⟩
      c + (b * c + fromParts (a * sb) c (fromParts a sb (i , sj) , k))   ≡⟨ ≡.cong₂ _+_ ≡.refl (lem′ b (a * sb) c _ k) ⟩
      c + fromParts (b + a * sb) c (b + fromParts a sb (i , sj) , k)     ≡⟨⟩
      fromParts (suc a * sb) c (fromParts (suc a) sb (suc i , sj) , k)   ≡⟨⟩
      fromParts³ (suc a) sb c (suc i , sj , k) ∎

abstract
  toParts-1ˡ : ∀ {b} i → i < b → Partsℕ.toParts (constParts 1 b) i ≡ (0 , i)
  toParts-1ˡ {b} i p with Impl.compare′ i b
  toParts-1ˡ {.(suc (i + k))} i p | Impl.less .i k = ≡.refl
  toParts-1ˡ {.m} .(m + k) p | Impl.gte m k = ⊥-elim (Nat.m+n≮m m k p)

  toParts-1ʳ : ∀ {a} i → i < a → Partsℕ.toParts (constParts a 1) i ≡ (i , 0)
  toParts-1ʳ {zero} _ ()
  toParts-1ʳ {suc a} zero p = ≡.refl
  toParts-1ʳ {suc a} (suc i) (Nat.s≤s p) with Σ.≡⇒≡×≡ (toParts-1ʳ {a} i p)
  toParts-1ʳ {suc a} (suc i) (Nat.s≤s p) | q , r with Impl.compare′ i 0
  toParts-1ʳ {suc a} (suc i) (Nat.s≤s p) | q , r | Impl.gte .0 .i = Σ.≡×≡⇒≡ (≡.cong suc q , r)


text:
module RandomAccessList.Zeroless.Core where

open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)

open import Data.Nat
open import Data.Nat.Etc

--  parameterized by the level of the least significant digit
data 1-2-RAL (A : Set) : ℕ → Set where
    []     : ∀ {n}                                                               → 1-2-RAL A n
    _1∷_   : ∀ {n} → BinaryLeafTree A n                      → 1-2-RAL A (suc n) → 1-2-RAL A n
    _,_2∷_ : ∀ {n} → BinaryLeafTree A n → BinaryLeafTree A n → 1-2-RAL A (suc n) → 1-2-RAL A n

infixr 2 _1∷_
infixr 2 _,_2∷_
--------------------------------------------------------------------------------
-- to ℕ

⟦_⟧ₙ : ∀ {A n} → 1-2-RAL A n → ℕ
⟦          [] ⟧ₙ = 0
⟦ x     1∷ xs ⟧ₙ = 1 + 2 * ⟦ xs ⟧ₙ
⟦ x , y 2∷ xs ⟧ₙ = 2 + 2 * ⟦ xs ⟧ₙ

⟦_⟧ : ∀ {n A} → 1-2-RAL A n → ℕ
⟦_⟧ {n} xs = 2 ^ n * ⟦ xs ⟧ₙ

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------
-- Second-order abstract syntax
--
-- Formalisation of second-order abstract syntax with variable binding.
------------------------------------------------------------------------

module Everything where

-- Public exports of modules and definitions used throughout the library.
import SOAS.Common

-- Abstract categorical definitions of carrier categories with extra structure,
-- and associated free constructions.
import SOAS.Construction.Free
import SOAS.Construction.Structure

-- Skew monoidal and closed structure
import SOAS.Construction.Skew.SkewClosed

-- Add sorting to categories, and prove that various categorical
-- structure (CCC, monoidal, etc.) are preserved.
import SOAS.Sorting

-- Definition of simple contexts as lists of sorts.
import SOAS.Context

-- The sorted family of variables and generalised context maps
import SOAS.Variable

-- | Context maps as renamings, substitutions and category morphisms

-- Context map combinators
import SOAS.ContextMaps.Combinators

-- Category of contexts and renamings
import SOAS.ContextMaps.CategoryOfRenamings

-- Inductive context maps
import SOAS.ContextMaps.Inductive

-- Common properties of context maps
import SOAS.ContextMaps.Properties

-- | Families

-- Definition of the category of sorted families
import SOAS.Families.Core

-- Isomorphism between sorted families
import SOAS.Families.Isomorphism

-- Bi-Cartesian closed and linear monoidal closed structure of families
import SOAS.Families.BCCC
import SOAS.Families.Linear

-- Context extension endofunctor
import SOAS.Families.Delta

-- Inductive construction of families
import SOAS.Families.Build

-- | Abstract constructions

-- Box modality
import SOAS.Abstract.Box

-- □-coalgebra on families - renaming structure
import SOAS.Abstract.Coalgebra

-- Internal hom of families
import SOAS.Abstract.Hom

-- Closed monoid in families - substitution structure
import SOAS.Abstract.Monoid

-- Exponential strength
import SOAS.Abstract.ExpStrength

-- | Constructions built upon coalgebras

-- Coalgebraic maps 𝒳 ⇾ 〖𝒫 , 𝒴〗
import SOAS.Coalgebraic.Map

-- Lifting and strength
import SOAS.Coalgebraic.Lift
import SOAS.Coalgebraic.Strength

-- Monoids compatible with coalgebra structure
import SOAS.Coalgebraic.Monoid

-- | Metatheory for a second-order binding signature

-- Binding algebras
import SOAS.Metatheory.Algebra

-- Algebras with variables and metavariables
import SOAS.Metatheory.MetaAlgebra

-- Signature monoids
import SOAS.Metatheory.Monoid

-- Initial-algebra semantics
import SOAS.Metatheory.Semantics

-- Parametrised interpretations
import SOAS.Metatheory.Traversal

-- Renaming structure by initiality
import SOAS.Metatheory.Renaming

-- Coalgebraic maps by initiality
import SOAS.Metatheory.Coalgebraic

-- Substitution structure by initiality
import SOAS.Metatheory.Substitution

-- Free monoid structure
import SOAS.Metatheory.FreeMonoid

-- Syntactic structure
import SOAS.Metatheory.Syntax

-- | Second-order structure

-- Metasubstitution
import SOAS.Metatheory.SecondOrder.Metasubstitution

-- Unit of metasubstitution
import SOAS.Metatheory.SecondOrder.Unit

-- Equational theory
import SOAS.Metatheory.SecondOrder.Equality

-- | Term syntax of a second-order signature

-- Argument representation
import SOAS.Syntax.Arguments

-- Second-order binding signature
import SOAS.Syntax.Signature

-- Shorthand notation
import SOAS.Syntax.Shorthands

-- Signature construction
import SOAS.Syntax.Build

-- First-order term syntax
import SOAS.Syntax.Term


text:
open import Coinduction using ( ∞ ; ♭ ; ♯_ )
open import Data.Empty using ( ⊥ )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
open import Data.Product using ( ∃ ; _×_ ; _,_ ; ,_ )
open import Data.Strict using ( Strict ; ! )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Data.Unit using ( ⊤ ; tt )
open import System.IO.Transducers.Session
  using ( Session ; I ; Σ ; _∼_ ; ∼-sym ; Γ ; _/_ ; IsΣ ; IsΣ-≡ ; ⟨_⟩ ; _&_ ; ¿ ; _+_  )
  renaming ( unit₁ to ∼-unit₁ ; unit₂ to ∼-unit₂ ; assoc to ∼-assoc )
open import System.IO.Transducers.Trace using ( _≤_ ; _⊑_ ; Trace ; [] ; _∷_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Nullary using ( Dec ; yes ; no )

module System.IO.Transducers.Lazy where

-- S ⇛ T is the type of transducers whose inputs
-- are traces through S, and whose output are traces through T.

-- Note that input is coinductive, but output is inductive,
-- which guarantees that transducers will map finite traces
-- to finite traces.

-- The name transducer comes from automata theory -- these
-- are essentially I/O automata, or strategies in a two-player
-- game without the move alternation restriction.

-- In this module, we give definitions for lazy transducers,
-- there is a separate module for stict transducers.

infixr 4 _⇒_ _≃_ _≲_
infixr 6 _⟫_
infixr 8 _[&]_ _⟨&⟩_ _⟨+⟩_ _⟨¿⟩_

-- Lazy transducers, which may perform output before input.

data _⇒_ : (S T : Session) → Set₁ where
  inp : ∀ {T A V F} → ∞ ((a : A) → (♭ F a ⇒ T)) → (Σ V F ⇒ T)
  out : ∀ {S B W G} → (b : B) → (S ⇒ ♭ G b) → (S ⇒ Σ W G)
  done : ∀ {S} → (S ⇒ S)

-- Semantically, we only need done at type I,
-- we have it at all types just for efficiency.

data _⤇_ : (S T : Session) → Set₁ where
  inp : ∀ {T A V F} → ∞ ((a : A) → (♭ F a ⤇ T)) → (Σ V F ⤇ T)
  out : ∀ {S B W G} → (b : B) → (S ⤇ ♭ G b) → (S ⤇ Σ W G)
  done : (I ⤇ I)

ι : ∀ {S T} → (S ⤇ T) → (S ⇒ T)
ι (inp P)   = inp (♯ λ a → ι (♭ P a))
ι (out b P) = out b (ι P)
ι done      = done

ι⁻¹ : ∀ {S T} → (S ⇒ T) → (S ⤇ T)
ι⁻¹ (inp P)        = inp (♯ λ a → ι⁻¹ (♭ P a))
ι⁻¹ (out b P)      = out b (ι⁻¹ P)
ι⁻¹ (done {I})     = done
ι⁻¹ (done {Σ V F}) = inp (♯ λ a → out a (ι⁻¹ done))

-- Helper functions to build transducers in terms of Γ and _/_

out' : ∀ {S T} b → (S ⇒ T / b) → (S ⇒ T)
out' {S} {I}     () P
out' {S} {Σ W G} b  P = out b P

-- Helper function to output a whole trace.

out* : ∀ {S T U} → (T ≤ U) → (S ⇒ T) → (S ⇒ U)
out* []       P = P
out* (b ∷ bs) P = out* bs (out' b P)

-- Semantics as a function from partial traces to partial traces

⟦_⟧ : ∀ {S T} → (S ⇒ T) → (Trace S) → (Trace T)
⟦ inp P   ⟧ []       = []
⟦ inp P   ⟧ (a ∷ as) = ⟦ ♭ P a ⟧ as
⟦ out b P ⟧ as       = b ∷ ⟦ P ⟧ as
⟦ done    ⟧ as       = as

-- Extensional equivalence on trace functions

_≃_ : ∀ {S T} → (f g : Trace S → Trace T) → Set
f ≃ g = ∀ as → f as ≡ g as

-- Improvement order on trace functions

_≲_ : ∀ {S T} → (f g : Trace S → Trace T) → Set₁
f ≲ g = ∀ as → f as ⊑ g as

-- Equivalent sessions give rise to a transducer

equiv : ∀ {S T} → (S ∼ T) → (S ⇒ T)
equiv I       = done
equiv (Σ V F) = inp (♯ λ a → out a (equiv (♭ F a)))

-- Transducers form a category with composition given by
-- parallel (data flow) composition.  This is defined by the
-- usual expansion laws for parallel composition, together with
-- the unit law for done.  Since composition is deterministic,
-- we prioritize output over input.

_⟫_ : ∀ {S T U} → (S ⇒ T) → (T ⇒ U) → (S ⇒ U)
done    ⟫ Q       = Q
P       ⟫ done    = P
P       ⟫ out b Q = out b (P ⟫ Q)
out b P ⟫ inp Q   = P ⟫ ♭ Q b
inp P   ⟫ Q       = inp (♯ λ a → ♭ P a ⟫ Q)

-- The category has monoidal structure given by &, with
-- action on morphisms:

_[&]_ : ∀ {S T U V} → (S ⇒ T) → (U ⇒ V) → ((S & U) ⇒ (T & V))
inp {I} P    [&] out c Q = out c (inp P [&] Q)
inp P        [&] Q       = inp (♯ λ a → ♭ P a [&] Q)
out b P      [&] Q       = out b (P [&] Q)
done {I}     [&] Q       = Q
done {Σ V F} [&] Q       = inp (♯ λ a → out a (done {♭ F a} [&] Q))

-- Units for &

unit₁ : ∀ {S} → (I & S) ⇒ S
unit₁ = equiv ∼-unit₁

unit₁⁻¹ : ∀ {S} → S ⇒ (I & S)
unit₁⁻¹ = equiv (∼-sym ∼-unit₁)

unit₂ : ∀ {S} → (S & I) ⇒ S
unit₂ = equiv ∼-unit₂

unit₂⁻¹ : ∀ {S} → S ⇒ (S & I)
unit₂⁻¹ = equiv (∼-sym ∼-unit₂)

-- Associativity of &

assoc : ∀ {S T U} → (S & (T & U)) ⇒ ((S & T) & U)
assoc {S} = equiv (∼-assoc {S})

assoc⁻¹ : ∀ {S T U} → ((S & T) & U) ⇒ (S & (T & U))
assoc⁻¹ {S} = equiv (∼-sym (∼-assoc {S}))

-- Projections

discard : ∀ {S} → (S ⇒ I)
discard {I}     = done
discard {Σ V F} = inp (♯ λ a → discard)

π₁ : ∀ {S T} → (S & T ⇒ S)
π₁ {I}     = discard
π₁ {Σ V F} = inp (♯ λ a → out a π₁)

π₂ : ∀ {S T} → (S & T ⇒ T)
π₂ {I}     = done
π₂ {Σ V F} = inp (♯ λ a → π₂ {♭ F a})

-- The category is almost cartesian, at the cost of
-- buffering.  WARNING.  BUFFERING.  This is bad.  Do not do this.

-- The "almost" is due to a failure of the projection properties:
-- P ⟨&⟩ Q ⟫ π₂ is not equivalent to Q, since Q may do output immediately,
-- and P ⟨&⟩ Q ⟫ π₂ can only output after it has consumed all its input.
-- Similarly π₁ ⟨&⟩ π₂ is not equivalent to done, as π₂'s output will
-- be bufferred.

-- This implementation uses output buffering, hopefully output
-- is usually smaller than input.

buffer : ∀ {S T U V} → (S ⇒ T) → (S ⇒ U) → (U ≤ V) → (S ⇒ T & V)
buffer (inp P)        (inp Q)   cs = inp (♯ λ a → buffer (♭ P a) (♭ Q a) cs)
buffer (inp P)        (out c Q) cs = buffer (inp P) Q (c ∷ cs)
buffer (inp P)        done      cs = inp (♯ λ c → buffer (♭ P c) done (c ∷ cs))
buffer (out b P)      Q         cs = out b (buffer P Q cs)
buffer (done {I})     Q         cs = out* cs Q
buffer (done {Σ V F}) (inp Q)   cs = inp (♯ λ a → out a (buffer done (♭ Q a) cs))
buffer (done {Σ V F}) (out c Q) cs = buffer done Q (c ∷ cs)
buffer (done {Σ V F}) done      cs = inp (♯ λ c → out c (buffer done done (c ∷ cs)))

_⟨&⟩_ : ∀ {S T U} → (S ⇒ T) → (S ⇒ U) → (S ⇒ T & U)
P ⟨&⟩ Q = buffer P Q []

-- If you want input buffering, you can implement it using copy and _[&]_.

copy : ∀ {S} → (S ⇒ (S & S))
copy = done ⟨&⟩ done

-- Braiding structure

swap'' : ∀ {T U} → (I ≤ U) → T ⇒ (T & U)
swap'' {I}     cs = out* cs done
swap'' {Σ W G} cs = inp (♯ λ b → out b (swap'' cs))

swap' : ∀ {S T} {isΣ : IsΣ T} {U} → (S ≤ U) → (S & T) ⇒ (T & U)
swap' {I}             cs = swap'' cs
swap' {Σ V F} {Σ W G} cs = inp (♯ λ c → swap' (c ∷ cs))
swap' {Σ V F} {I}  {} cs

swap : ∀ {S T} → ((S & T) ⇒ (T & S))
swap {I}     {T}     = unit₂⁻¹
swap {Σ V F} {I}     = unit₂
swap {Σ V F} {Σ W G} = swap' {Σ V F} []

-- Choice

ι₁ : ∀ {S T} → (S ⇒ S + T)
ι₁ = out true done

ι₂ : ∀ {S T} → (T ⇒ S + T)
ι₂ = out false done

choice : ∀ {S T U} → (S ⇒ U) → (T ⇒ U) → ∀ b → ((if b then S else T) ⇒ U)
choice P Q true  = P
choice P Q false = Q

_[+]_ : ∀ {S T U V} → (S ⇒ U) → (T ⇒ V) → ((S + T) ⇒ (U + V))
P [+] Q = inp (♯ choice (out true P) (out false Q))

_⟨+⟩_ : ∀ {S T U} {isΣ : IsΣ U} → (S ⇒ U) → (T ⇒ U) → ((S + T) ⇒ U)
_⟨+⟩_ {S} {T} {Σ X H} P Q = inp (♯ choice P Q)
_⟨+⟩_ {S} {T} {I}  {} P Q

-- Options.

some : ∀ {S} → (S ⇒ ¿ S)
some = ι₁

none : ∀ {S} → (I ⇒ ¿ S)
none = ι₂

[¿] : ∀ {S T} → (S ⇒ T) → (¿ S ⇒ ¿ T)
[¿] P = P [+] done

_⟨¿⟩_ : ∀ {S T} {isΣ : IsΣ T} → (S ⇒ T) → (I ⇒ T) → (¿ S ⇒ T)
_⟨¿⟩_ {S} {T} {isΣ} = _⟨+⟩_ {S} {I} {T} {isΣ}

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

module Definition.Conversion.Weakening where

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Conversion

import Tools.PropositionalEquality as PE

mutual
  -- Weakening of algorithmic equality of neutrals.
  wk~↑! : ∀ {ρ t u A Γ Δ l} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
      → Γ ⊢ t ~ u ↑! A ^ l
      → Δ ⊢ U.wk ρ t ~ U.wk ρ u ↑! U.wk ρ A ^ l
  wk~↑! {ρ} [ρ] ⊢Δ (var-refl x₁ x≡y) = var-refl (wkTerm [ρ] ⊢Δ x₁) (PE.cong (wkVar ρ) x≡y)
  wk~↑! ρ ⊢Δ (app-cong {rF = !} {G = G} t~u x) =
    PE.subst (λ x → _ ⊢ _ ~ _ ↑! x ^ _) (PE.sym (wk-β G))
             (app-cong (wk~↓! ρ ⊢Δ t~u) (wkConv↑Term ρ ⊢Δ x))
  wk~↑! ρ ⊢Δ (app-cong {rF = %} {G = G} t~u x) =
    PE.subst (λ x → _ ⊢ _ ~ _ ↑! x ^ _) (PE.sym (wk-β G))
             (app-cong (wk~↓! ρ ⊢Δ t~u) (wk~↑% ρ ⊢Δ x))
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (natrec-cong {k} {l} {h} {g} {a₀} {b₀} {F} {G} {ll} x x₁ x₂ t~u) =
    PE.subst (λ x → _ ⊢ U.wk ρ (natrec _ F a₀ h k) ~ _ ↑! x ^ _) (PE.sym (wk-β F))
             (natrec-cong (wkConv↑ (lift [ρ]) (⊢Δ ∙ (univ (ℕⱼ ⊢Δ))) x)
                          (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x ^ _) (wk-β F)
                                    (wkConv↑Term [ρ] ⊢Δ x₁))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ h [conv↑] U.wk ρ g ∷ x ^ ι ll)
                                    (wk-β-natrec _ F ! _) (wkConv↑Term [ρ] ⊢Δ x₂))
                          (wk~↓! [ρ] ⊢Δ t~u))
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Emptyrec-cong {k} {l} {F} {G} x t~u) =
    Emptyrec-cong (wkConv↑ [ρ] ⊢Δ x) (wk~↑% [ρ] ⊢Δ t~u)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-cong X x x₁) = Id-cong (wk~↓! [ρ] ⊢Δ X) (wkConv↑Term [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-ℕ x x₁) = Id-ℕ (wk~↓! [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-ℕ0 x) = Id-ℕ0 (wk~↓! [ρ] ⊢Δ x)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-ℕS x x₁) = Id-ℕS (wkConv↑Term [ρ] ⊢Δ x) (wk~↓! [ρ] ⊢Δ x₁)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-U x x₁) = Id-U (wk~↓! [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-Uℕ x) = Id-Uℕ (wk~↓! [ρ] ⊢Δ x)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (Id-UΠ x x₁) = Id-UΠ (wkConv↑Term [ρ] ⊢Δ x) (wk~↓! [ρ] ⊢Δ x₁)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-cong X x x₁ x₂ x₃) =
    cast-cong (wk~↓! [ρ] ⊢Δ X) (wkConv↑Term [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂) (wkTerm [ρ] ⊢Δ x₃)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-ℕ X x x₁ x₂) =
    cast-ℕ (wk~↓! [ρ] ⊢Δ X) (wkConv↑Term [ρ] ⊢Δ x) (wkTerm [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-ℕℕ X x x₁) =
    cast-ℕℕ (wk~↓! [ρ] ⊢Δ X) (wkTerm [ρ] ⊢Δ x) (wkTerm [ρ] ⊢Δ x₁)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-Π x X x₁ x₂ x₃) =
    cast-Π (wkConv↑Term [ρ] ⊢Δ x) (wk~↓! [ρ] ⊢Δ X) (wkConv↑Term [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂) (wkTerm [ρ] ⊢Δ x₃)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-Πℕ x x₁ x₂ x₃) =
    cast-Πℕ (wkConv↑Term [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂) (wkTerm [ρ] ⊢Δ x₃)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-ℕΠ x x₁ x₂ x₃) =
    cast-ℕΠ (wkConv↑Term [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂) (wkTerm [ρ] ⊢Δ x₃)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-ΠΠ%! x x₁ x₂ x₃ x₄) =
    cast-ΠΠ%! (wkConv↑Term [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁) (wkConv↑Term [ρ] ⊢Δ x₂) (wkTerm [ρ] ⊢Δ x₃) (wkTerm [ρ] ⊢Δ x₄)
  wk~↑! {ρ} {Δ = Δ} [ρ] ⊢Δ (cast-ΠΠ!% x x₁ x₂ x₃ x₄) =
    cast-ΠΠ!% (wkConv↑Term [ρ] ⊢Δ x) (wkConv↑Term [ρ] ⊢Δ x₁) (wkConv↑Term [ρ] ⊢Δ x₂) (wkTerm [ρ] ⊢Δ x₃) (wkTerm [ρ] ⊢Δ x₄)

  wk~↑% : ∀ {ρ t u A Γ Δ l } ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
        → Γ ⊢ t ~ u ↑% A ^ l
        → Δ ⊢ U.wk ρ t ~ U.wk ρ u ↑% U.wk ρ A ^ l
  wk~↑% [ρ] ⊢Δ (%~↑ ⊢k ⊢l) =
    %~↑ (wkTerm [ρ] ⊢Δ ⊢k) (wkTerm [ρ] ⊢Δ ⊢l)

  wk~↑ : ∀ {ρ t u A rA lA Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
      → Γ ⊢ t ~ u ↑ A ^ [ rA , lA ]
      → Δ ⊢ U.wk ρ t ~ U.wk ρ u ↑ U.wk ρ A ^ [ rA , lA ]
  wk~↑ [ρ] ⊢Δ (~↑! x) = ~↑! (wk~↑! [ρ] ⊢Δ x)
  wk~↑ [ρ] ⊢Δ (~↑% x) = ~↑% (wk~↑% [ρ] ⊢Δ x)

  -- Weakening of algorithmic equality of neutrals in WHNF.
  wk~↓! : ∀ {ρ t u A Γ Δ l} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
      → Γ ⊢ t ~ u ↓! A ^ l
      → Δ ⊢ U.wk ρ t ~ U.wk ρ u ↓! U.wk ρ A ^ l
  wk~↓! {ρ} [ρ] ⊢Δ ([~] A₁ D whnfA k~l) =
    [~] (U.wk ρ A₁) (wkRed* [ρ] ⊢Δ D) (wkWhnf ρ whnfA) (wk~↑! [ρ] ⊢Δ k~l)

  -- Weakening of algorithmic equality of types.
  wkConv↑ : ∀ {ρ A B rA Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
          → Γ ⊢ A [conv↑] B ^ rA
          → Δ ⊢ U.wk ρ A [conv↑] U.wk ρ B ^ rA
  wkConv↑ {ρ} [ρ] ⊢Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    [↑] (U.wk ρ A′) (U.wk ρ B′) (wkRed* [ρ] ⊢Δ D) (wkRed* [ρ] ⊢Δ D′)
        (wkWhnf ρ whnfA′) (wkWhnf ρ whnfB′) (wkConv↓ [ρ] ⊢Δ A′<>B′)

  -- Weakening of algorithmic equality of types in WHNF.
  wkConv↓ : ∀ {ρ A B rA Γ Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
         → Γ ⊢ A [conv↓] B ^ rA
         → Δ ⊢ U.wk ρ A [conv↓] U.wk ρ B ^ rA
  wkConv↓ ρ ⊢Δ (U-refl eqr x) = U-refl eqr ⊢Δ
  wkConv↓ ρ ⊢Δ (univ x) = univ (wkConv↓Term ρ ⊢Δ x)

  -- Weakening of algorithmic equality of terms.
  wkConv↑Term : ∀ {ρ t u A Γ Δ l} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
             → Γ ⊢ t [conv↑] u ∷ A ^ l
             → Δ ⊢ U.wk ρ t [conv↑] U.wk ρ u ∷ U.wk ρ A ^ l
  wkConv↑Term {ρ} [ρ] ⊢Δ ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    [↑]ₜ (U.wk ρ B) (U.wk ρ t′) (U.wk ρ u′)
         (wkRed* [ρ] ⊢Δ D) (wkRed*Term [ρ] ⊢Δ d) (wkRed*Term [ρ] ⊢Δ d′)
         (wkWhnf ρ whnfB) (wkWhnf ρ whnft′) (wkWhnf ρ whnfu′)
         (wkConv↓Term [ρ] ⊢Δ t<>u)

  -- Weakening of algorithmic equality of terms in WHNF.
  wkConv↓Term : ∀ {ρ t u A Γ Δ l} ([ρ] : ρ ∷ Δ ⊆ Γ) → ⊢ Δ
             → Γ ⊢ t [conv↓] u ∷ A ^ l
             → Δ ⊢ U.wk ρ t [conv↓] U.wk ρ u ∷ U.wk ρ A ^ l
  wkConv↓Term ρ ⊢Δ (U-refl eqr x) = U-refl eqr ⊢Δ
  wkConv↓Term ρ ⊢Δ (ne x) = ne (wk~↓! ρ ⊢Δ x)
  wkConv↓Term ρ ⊢Δ (ℕ-ins x) =
    ℕ-ins (wk~↓! ρ ⊢Δ x)
  -- wkConv↓Term ρ ⊢Δ (Empty-ins x) =
  --   Empty-ins (wk~↓% ρ ⊢Δ x)
  wkConv↓Term {ρ} [ρ] ⊢Δ (ne-ins t u x x₁) =
    ne-ins (wkTerm [ρ] ⊢Δ t) (wkTerm [ρ] ⊢Δ u) (wkNeutral ρ x) (wk~↓! [ρ] ⊢Δ x₁)
  wkConv↓Term ρ ⊢Δ (zero-refl x) = zero-refl ⊢Δ
  wkConv↓Term ρ ⊢Δ (suc-cong t<>u) = suc-cong (wkConv↑Term ρ ⊢Δ t<>u)
  wkConv↓Term {ρ} {Δ = Δ} [ρ] ⊢Δ (η-eq {F = F} {G = G} {rF = rF} {lF = lF} {lG = lG} l< l<' x x₁ x₂ y y₁ t<>u) =
    let ⊢ρF = wk [ρ] ⊢Δ x
    in  η-eq l< l<' ⊢ρF (wkTerm [ρ] ⊢Δ x₁) (wkTerm [ρ] ⊢Δ x₂)
             (wkFunction ρ y) (wkFunction ρ y₁)
             (PE.subst₃ (λ x y z → Δ ∙ U.wk ρ F ^ [ rF , ι lF ] ⊢ x [conv↑] y ∷ z ^ ι lG)
                        (PE.cong₃ _∘_^_ (PE.sym (wk1-wk≡lift-wk1 _ _)) PE.refl PE.refl)
                        (PE.cong₃ _∘_^_ (PE.sym (wk1-wk≡lift-wk1 _ _)) PE.refl PE.refl)
                        PE.refl
                        (wkConv↑Term (lift [ρ]) (⊢Δ ∙ ⊢ρF) t<>u))
  wkConv↓Term ρ ⊢Δ (ℕ-refl x) = ℕ-refl ⊢Δ
  wkConv↓Term ρ ⊢Δ (Empty-refl x _) = Empty-refl x ⊢Δ
  wkConv↓Term ρ ⊢Δ (Π-cong eql eqr eqlF eqlG l< l<'   x A<>B A<>B₁) =
    let ⊢ρF = wk ρ ⊢Δ x
    in  Π-cong eql eqr eqlF eqlG l< l<' ⊢ρF (wkConv↑Term ρ ⊢Δ A<>B) (wkConv↑Term (lift ρ) (⊢Δ ∙ ⊢ρF) A<>B₁)
  wkConv↓Term ρ ⊢Δ (∃-cong eql x A<>B A<>B₁) =
    let ⊢ρF = wk ρ ⊢Δ x
    in  ∃-cong eql ⊢ρF (wkConv↑Term ρ ⊢Δ A<>B) (wkConv↑Term (lift ρ) (⊢Δ ∙ ⊢ρF) A<>B₁)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

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

---- Lens laws for go

ValidLens-AtLocation-ViewSet :
    {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> ViewSet (atLocation {t} loc dep {ins})
ValidLens-AtLocation-ViewSet (x , y) dep {ins} v s = trans refl (prop-Composition-ViewSet (ValidLens-WrappedTree) (ValidLens-go (x , y) dep {ins}) v s)

ValidLens-AtLocation-SetView :
    {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> SetView (atLocation {t} loc dep {ins})
ValidLens-AtLocation-SetView (x , y) dep {ins} s = trans refl (prop-Composition-SetView (ValidLens-WrappedTree) (ValidLens-go (x , y) dep {ins}) s)

ValidLens-AtLocation-SetSet :
    {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> SetSet (atLocation {t} loc dep {ins})
ValidLens-AtLocation-SetSet (x , y) dep {ins} v1 v2 s = trans refl (prop-Composition-SetSet (ValidLens-WrappedTree) (ValidLens-go (x , y) dep {ins}) v1 v2 s)

ValidLens-AtLocation : {t : Set} {{eqT : Eq t}}
    -> (loc : Nat × Nat) -> (dep : Nat)
    -> {ins : IsTrue (isInsidePow loc dep)}
    -> ValidLens (VQuadTree t {dep}) t
ValidLens-AtLocation {t} {{eqT}} (x , y) dep {ins} = CValidLens (atLocation (x , y) dep {ins}) (ValidLens-AtLocation-ViewSet (x , y) dep {ins}) (ValidLens-AtLocation-SetView (x , y) dep {ins}) (ValidLens-AtLocation-SetSet (x , y) dep {ins})

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
open import Relation.Binary using (Rel)
open import Algebra.Bundles using (CommutativeRing)
open import Algebra.Module.Morphism.Structures
open import Algebra.Module.Normed using (NormedModule)

module Algebra.Module.Limit
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR using () renaming (Carrier to X))
  {rel} {_≤_ : Rel X rel}
  {ma ℓma} (MA : NormedModule CR _≤_ ma ℓma)
  {mb ℓmb} (MB : NormedModule CR _≤_ mb ℓmb)
  where

open import Data.Product using (Σ-syntax; ∃-syntax; _×_; proj₁)

open CommutativeRing CR
open import Algebra.Module.Morphism.Module using (⊸-normed)
private
  module MA = NormedModule MA
  module MB = NormedModule MB
  module MA⊸MB = NormedModule (⊸-normed MA MB)

open NormedModule MA using () renaming
  ( Carrierᴹ to Carrierᴬ
  ; _+ᴹ_ to _+ᴬ_
  ; _-ᴹ_ to _-ᴬ_
  ; ∥_∥ to ∥_∥ᴬ
  ; ⟨_,_⟩ to ⟨_,_⟩ᴬ
  )

open NormedModule MB using () renaming
  ( Carrierᴹ to Carrierᴮ
  ; _+ᴹ_ to _+ᴮ_
  ; _-ᴹ_ to _-ᴮ_
  ; ∥_∥ to ∥_∥ᴮ
  ; ⟨_,_⟩ to ⟨_,_⟩ᴮ
  )

open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ using (_<_)

Limit-syntax : (L : Carrierᴮ) (f : Carrierᴬ → Carrierᴮ) (c : Carrierᴬ) → Set _
Limit-syntax L f c =
  ∀ ε → 0# < ε → ∃[ δ ]
    ∀ x →
      let d = ⟨ c , x ⟩ᴬ
      in (0# < d) × (d < δ) → ⟨ f x , L ⟩ᴮ < ε

syntax Limit-syntax L (λ x → f) c = f ⟶ L As x ⟶ c

Limit-syntax-0 : (L : Carrierᴮ) (f : Carrierᴬ → Carrierᴮ) → Set _
Limit-syntax-0 L f =
  ∀ ε → 0# < ε → ∃[ δ ]
    ∀ x →
      let d = ∥ x ∥ᴬ
      in (0# < d) × (d < δ) → ⟨ f x , L ⟩ᴮ < ε

syntax Limit-syntax-0 L (λ x → f) = f ⟶ L As x ⟶0

Limit-syntax-0-0 : (f : Carrierᴬ → Carrierᴮ) → Set _
Limit-syntax-0-0 f =
  ∀ ε → 0# < ε → ∃[ δ ]
    ∀ x →
      let d = ∥ x ∥ᴬ
      in (0# < d) × (d < δ) → ∥ f x ∥ᴮ < ε

syntax Limit-syntax-0-0 (λ x → f) = f ⟶0 As x ⟶0

_Approximates_At_
  : (δf : MA⊸MB.Carrierᴹ)
  → (f : Carrierᴬ → Carrierᴮ)
  → (x : Carrierᴬ)
  → Set _
δf Approximates f At x = (f (x +ᴬ dx) -ᴮ (f x +ᴮ proj₁ δf dx)) ⟶0 As dx ⟶0

_Differentiates_
  : (δf : Carrierᴬ → MA⊸MB.Carrierᴹ)
  → (f : Carrierᴬ → Carrierᴮ)
  → Set _
δf Differentiates f = ∀ x → (f (x +ᴬ dx) -ᴮ (f x +ᴮ proj₁ (δf x) dx)) ⟶0 As dx ⟶0

D[_,_]_~_ : (f : Carrierᴬ → Carrierᴮ) (df : Carrierᴬ → MA⊸MB.Carrierᴹ) → Set _
D[_,_]_~_ f df = df Differentiates f

_DifferentiableAt_ : (f : Carrierᴬ → Carrierᴮ) (x : Carrierᴬ) → Set _
f DifferentiableAt x = ∃[ δf ] δf Approximates f At x

Differentiable : (f : Carrierᴬ → Carrierᴮ) → Set _
Differentiable f = ∀ x → f DifferentiableAt x

D[_,_][_,_] : (f : Carrierᴬ → Carrierᴮ) (x : Carrierᴬ) → Set _
D[_,_][_,_] f x = f DifferentiableAt x

-- [_,_]~[_~_]_
--   : (δf : Carrierᴬ → Carrierᴮ)
--   → (f : Carrierᴬ → Carrierᴮ)
--   → (x : Carrierᴬ)
--   → Set _
-- [_,_][_~_]_ df f x = {! df Approximates f At x  !}

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
open import FRP.JS.Geolocation.Angle using ( Angle ) renaming ( toString to toString° )
open import FRP.JS.String using ( String ; _++_ )

module FRP.JS.Geolocation.Coords where

-- Not including the optional fields yet.

record Coords : Set where
  field
    latitude : Angle
    longitude : Angle

open Coords public

toString : Coords → String
toString c = toString° (latitude c) ++ "," ++ toString° (longitude c)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-dependent product combinators for setoid equality preserving
-- functions
------------------------------------------------------------------------

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

module Data.Product.Function.NonDependent.Setoid where

open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Relation.Binary
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; _↣_; module Injection)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)

------------------------------------------------------------------------
-- Combinators for equality preserving functions

module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where

  _×-⟶_ : (A ⟶ B) → (C ⟶ D) → (A ×ₛ C) ⟶ (B ×ₛ D)
  _×-⟶_ f g = record
    { _⟨$⟩_ = fg
    ; cong  = fg-cong
    }
    where
    open Setoid (A ×ₛ C) using () renaming (_≈_ to _≈AC_)
    open Setoid (B ×ₛ D) using () renaming (_≈_ to _≈BD_)

    fg = map (f ⟨$⟩_) (g ⟨$⟩_)

    fg-cong : _≈AC_ =[ fg ]⇒ _≈BD_
    fg-cong (_∼₁_ , _∼₂_) = (F.cong f _∼₁_ , F.cong g _∼₂_)

module _ {a₁ a₂ b₁ b₂ c₁ c₂}
         {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} {C : Setoid c₁ c₂}
         where

  <_,_>ₛ : (A ⟶ B) → (A ⟶ C) → A ⟶ (B ×ₛ C)
  < f , g >ₛ = record
    { _⟨$⟩_ = < f ⟨$⟩_ , g ⟨$⟩_ >
    ; cong = < F.cong f , F.cong g >
    }

module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} where

  proj₁ₛ : (A ×ₛ B) ⟶ A
  proj₁ₛ = record { _⟨$⟩_ = proj₁ ; cong = proj₁ }

  proj₂ₛ : (A ×ₛ B) ⟶ B
  proj₂ₛ = record { _⟨$⟩_ = proj₂ ; cong = proj₂ }

  swapₛ : (A ×ₛ B) ⟶ (B ×ₛ A)
  swapₛ = < proj₂ₛ , proj₁ₛ >ₛ

------------------------------------------------------------------------
-- Combinators for more complex function types

module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where

  _×-equivalence_ : Equivalence A B → Equivalence C D →
                    Equivalence (A ×ₛ C) (B ×ₛ D)
  _×-equivalence_ A⇔B C⇔D = record
    { to   = to   A⇔B ×-⟶ to   C⇔D
    ; from = from A⇔B ×-⟶ from C⇔D
    } where open Equivalence

  _×-injection_ : Injection A B → Injection C D →
                  Injection (A ×ₛ C) (B ×ₛ D)
  A↣B ×-injection C↣D = record
    { to        = to A↣B ×-⟶ to C↣D
    ; injective = map (injective A↣B) (injective C↣D)
    } where open Injection

  _×-left-inverse_ : LeftInverse A B → LeftInverse C D →
                     LeftInverse (A ×ₛ C) (B ×ₛ D)
  A↞B ×-left-inverse C↞D = record
    { to              = Equivalence.to eq
    ; from            = Equivalence.from eq
    ; left-inverse-of = left
    }
    where
    open LeftInverse
    eq = LeftInverse.equivalence A↞B ×-equivalence
         LeftInverse.equivalence C↞D

    left : Equivalence.from eq LeftInverseOf Equivalence.to eq
    left (x , y) = (left-inverse-of A↞B x , left-inverse-of C↞D y)

module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
  {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
  {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
  where

  _×-surjection_ : Surjection A B → Surjection C D →
                   Surjection (A ×ₛ C) (B ×ₛ D)
  A↠B ×-surjection C↠D = record
    { to         = LeftInverse.from inv
    ; surjective = record
      { from             = LeftInverse.to inv
      ; right-inverse-of = LeftInverse.left-inverse-of inv
      }
    }
    where
    open Surjection
    inv = right-inverse A↠B ×-left-inverse right-inverse C↠D

  _×-inverse_ : Inverse A B → Inverse C D →
                Inverse (A ×ₛ C) (B ×ₛ D)
  A↔B ×-inverse C↔D = record
    { to         = Surjection.to   surj
    ; from       = Surjection.from surj
    ; inverse-of = record
      { left-inverse-of  = LeftInverse.left-inverse-of inv
      ; right-inverse-of = Surjection.right-inverse-of surj
      }
    }
    where
    open Inverse
    surj = Inverse.surjection   A↔B ×-surjection
           Inverse.surjection   C↔D
    inv  = Inverse.left-inverse A↔B ×-left-inverse
           Inverse.left-inverse C↔D


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

open import Agda.Builtin.Equality
postulate
  A : Set
  B : A → Set

data H (@0 A : Set) : Set where
  con : (@0 x : A) →  H A

data G : Set where
  con : (@0 x : A) → (@0 b : B x) → G

data D : Set where
  con : (@0 x : A) → B x → D


text:
module Graph (Node : Set) where

open import Basics

data Edge : Set where
  edge : Node -> Node -> Edge

Graph : Set
Graph = List Edge

Step : Graph -> Node -> Node -> Set
Step G x y = Elem (edge x y) G

infixr 40 _<>_

data Path (G : Graph) : Node -> Node -> Set where
  nul  : forall {x}     -> Path G x x
  _<>_ : forall {x y z} -> Step G x y -> Path G y z -> Path G x z


text:
module Golden.Insertion where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Bool

insert : Nat -> List Nat -> List Nat
insert a [] = a ∷ []
insert x (a ∷ b) with x < a
... | true = x ∷ a ∷ b
... | false = a ∷ (insert x b)

lst : List Nat
lst = 2 ∷ []

slst : List Nat
slst = insert 3 lst

atDef : ∀ {a : Set} → a → List a -> Nat -> a
atDef def (x ∷ l) zero = x
atDef def (x ∷ l) (suc ix) = atDef def l ix
atDef def _ _ = def

l0 : Nat
l0 = atDef 0 slst 0

l1 : Nat
l1 = atDef 0 slst 1

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


text:
module Spire.Examples.Standard where

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

data ℕ : Set where
  zero : ℕ
  suc : (n : ℕ) → ℕ

data Vec (A : Set) : ℕ → Set where
  nil : Vec A zero
  cons : (n : ℕ) (a : A) (xs : Vec A n) → Vec A (suc n)

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

elimℕ : (P : ℕ → Set)
  (pzero : P zero)
  (psuc : (m : ℕ) → P m → P (suc m))
  (n : ℕ)
  → P n
elimℕ P pzero psuc zero = pzero
elimℕ P pzero psuc (suc n) = psuc n (elimℕ P pzero psuc n)

elimVec : (A : Set) (P : (n : ℕ) → Vec A n → Set)
  (pnil : P zero nil)
  (pcons : (n : ℕ) (a : A) (xs : Vec A n) → P n xs → P (suc n) (cons n a xs))
  (n : ℕ)
  (xs : Vec A n)
  → P n xs
elimVec A P pnil pcons .zero nil = pnil
elimVec A P pnil pcons .(suc n) (cons n a xs) = pcons n a xs (elimVec A P pnil pcons n xs)

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

module PatternMatching where

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

  mult : ℕ → ℕ → ℕ
  mult zero n = zero
  mult (suc m) n = add n (mult m n)

  append : (A : Set) (m : ℕ) (xs : Vec A m) (n : ℕ) (ys : Vec A n) → Vec A (add m n)
  append A .zero nil n ys = ys
  append A .(suc m) (cons m x xs) n ys = cons (add m n) x (append A m xs n ys)

  concat : (A : Set) (m n : ℕ) (xss : Vec (Vec A m) n) → Vec A (mult n m)
  concat A m .zero nil = nil
  concat A m .(suc n) (cons n xs xss) = append A m xs (mult n m) (concat A m n xss)

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

module Eliminator where

  add : ℕ → ℕ → ℕ
  add = elimℕ (λ _ → ℕ → ℕ)
    (λ n → n)
    (λ m ih n → suc (ih n))

  mult : ℕ → ℕ → ℕ
  mult = elimℕ (λ _ → ℕ → ℕ)
    (λ n → zero)
    (λ m ih n → add n (ih n))

  append : (A : Set) (m : ℕ) (xs : Vec A m) (n : ℕ) (ys : Vec A n) → Vec A (add m n)
  append A = elimVec A (λ m xs → (n : ℕ) (ys : Vec A n) → Vec A (add m n))
    (λ n ys → ys)
    (λ m x xs ih n ys → cons (add m n) x (ih n ys))

  concat : (A : Set) (m n : ℕ) (xss : Vec (Vec A m) n) → Vec A (mult n m)
  concat A m = elimVec (Vec A m) (λ n xss → Vec A (mult n m))
    nil
    (λ n xs xss ih → append A m xs (mult n m) ih)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


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

open import Functions.Definition
open import Functions.Lemmas
open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Sets.FinSet.Definition

module Sets.FinSet.Lemmas where

fneSymmetric : {n : ℕ} → {a b : FinSet (succ n)} → FinNotEquals a b → FinNotEquals b a
fneSymmetric {.1} {.a1} {.b1} (fne2 a1 b1 (inl x)) = fne2 b1 a1 (inr x)
fneSymmetric {.1} {.a1} {.b1} (fne2 a1 b1 (inr x)) = fne2 b1 a1 (inl x)
fneSymmetric {.(succ (succ _))} {.fzero} {b} (fneN .fzero b (inl (inl (refl ,, snd)))) = fneN b fzero (inl (inr (snd ,, refl)))
fneSymmetric {.(succ (succ _))} {a} {.fzero} (fneN a .fzero (inl (inr (fst ,, refl)))) = fneN fzero a (inl (inl (refl ,, fst)))
fneSymmetric {.(succ (succ _))} {a} {b} (fneN a b (inr ((fst ,, snd) , record { one = o ; two = p ; three = q }))) = fneN b a (inr ((snd ,, fst) , record { one = p ; two = o ; three = fneSymmetric q }))

private
  underlyingProof : {l m : _} {L : Set l} {pr : L → Set m} → (a : Sg L pr) → pr (underlying a)
  underlyingProof (a , b) = b

finSetNotEquals : {n : ℕ} → {a b : FinSet (succ n)} → (a ≡ b → False) → FinNotEquals {n} a b
finSetNotEquals {zero} {fzero} {fzero} pr = exFalso (pr refl)
finSetNotEquals {zero} {fzero} {fsucc ()} pr
finSetNotEquals {zero} {fsucc ()} {b} pr
finSetNotEquals {succ zero} {fzero} {fzero} pr = exFalso (pr refl)
finSetNotEquals {succ zero} {fzero} {fsucc fzero} pr = fne2 fzero (fsucc fzero) (inl (refl ,, refl))
finSetNotEquals {succ zero} {fzero} {fsucc (fsucc ())} pr
finSetNotEquals {succ zero} {fsucc fzero} {fzero} pr = fne2 (fsucc fzero) fzero (inr (refl ,, refl))
finSetNotEquals {succ zero} {fsucc fzero} {fsucc fzero} pr = exFalso (pr refl)
finSetNotEquals {succ zero} {fsucc fzero} {fsucc (fsucc ())} pr
finSetNotEquals {succ zero} {fsucc (fsucc ())}
finSetNotEquals {succ (succ n)} {fzero} {fzero} pr = exFalso (pr refl)
finSetNotEquals {succ (succ n)} {fzero} {fsucc b} pr = fneN fzero (fsucc b) (inl (inl (refl ,, (b , refl))))
finSetNotEquals {succ (succ n)} {fsucc a} {fzero} pr = fneN (fsucc a) fzero (inl (inr ((a , refl) ,, refl)))
finSetNotEquals {succ (succ n)} {fsucc a} {fsucc b} pr = fneN (fsucc a) (fsucc b) (inr ans)
  where
    q : a ≡ b → False
    q refl = pr refl
    t : FinNotEquals {succ n} a b
    t = finSetNotEquals {succ n} {a} {b} q
    ans : Sg (FinSet (succ (succ n)) && FinSet (succ (succ n))) (λ x → (fsucc a ≡ fsucc (_&&_.fst x)) & fsucc b ≡ fsucc (_&&_.snd x) & FinNotEquals (_&&_.fst x) (_&&_.snd x))
    ans with t
    ans | fne2 .fzero .(fsucc fzero) (inl (refl ,, refl)) = (a ,, b) , record { one = refl ; two = refl ; three = fne2 fzero (fsucc fzero) (inl (refl ,, refl)) }
    ans | fne2 .(fsucc fzero) .fzero (inr (refl ,, refl)) = (a ,, b) , record { one = refl ; two = refl ; three = fne2 (fsucc fzero) fzero (inr (refl ,, refl)) }
    ans | fneN a b _ = (a ,, b) , record { one = refl ; two = refl ; three = t }

fzeroNotFsucc : {n : ℕ} → {a : _} → fzero ≡ fsucc {succ n} a → False
fzeroNotFsucc ()

finSetNotEqualsSame : {n : ℕ} → {a : FinSet (succ n)} → FinNotEquals a a → False
finSetNotEqualsSame {.1} {fzero} (fne2 .fzero .fzero (inl (fst ,, ())))
finSetNotEqualsSame {.1} {fzero} (fne2 .fzero .fzero (inr (fst ,, ())))
finSetNotEqualsSame {.(succ (succ _))} {fzero} (fneN .fzero .fzero (inl (inl (refl ,, (a , ())))))
finSetNotEqualsSame {.(succ (succ _))} {fzero} (fneN .fzero .fzero (inl (inr ((a , ()) ,, refl))))
finSetNotEqualsSame {.(succ (succ _))} {fzero} (fneN .fzero .fzero (inr ((fst ,, snd) , record { one = () ; two = p ; three = q })))
finSetNotEqualsSame {.1} {fsucc a} (fne2 .(fsucc a) .(fsucc a) (inl (() ,, snd)))
finSetNotEqualsSame {.1} {fsucc a} (fne2 .(fsucc a) .(fsucc a) (inr (() ,, snd)))
finSetNotEqualsSame {.(succ (succ _))} {fsucc a} (fneN .(fsucc a) .(fsucc a) (inl (inl (() ,, snd))))
finSetNotEqualsSame {.(succ (succ _))} {fsucc a} (fneN .(fsucc a) .(fsucc a) (inl (inr (fst ,, ()))))
finSetNotEqualsSame {.(succ (succ _))} {fsucc a} (fneN .(fsucc a) .(fsucc a) (inr ((.a ,, .a) , record { one = refl ; two = refl ; three = q }))) = finSetNotEqualsSame q

finNotEqualsFsucc : {n : ℕ} → {a b : FinSet (succ n)} → FinNotEquals (fsucc a) (fsucc b) → FinNotEquals a b
finNotEqualsFsucc {.0} {a} {b} (fne2 .(fsucc a) .(fsucc b) (inl (() ,, snd)))
finNotEqualsFsucc {.0} {a} {b} (fne2 .(fsucc a) .(fsucc b) (inr (() ,, snd)))
finNotEqualsFsucc {n} {a} {b} (fneN .(fsucc a) .(fsucc b) (inl (inl (() ,, snd))))
finNotEqualsFsucc {n} {a} {b} (fneN .(fsucc a) .(fsucc b) (inl (inr (fst ,, ()))))
finNotEqualsFsucc {n} {a} {b} (fneN .(fsucc a) .(fsucc b) (inr ((fst ,, snd) , prf))) = identityOfIndiscernablesRight FinNotEquals ans (equalityCommutative b=snd)
  where
    a=fst : a ≡ fst
    a=fst = fsuccInjective (_&_&_.one prf)
    b=snd : b ≡ snd
    b=snd = fsuccInjective (_&_&_.two prf)
    ans : FinNotEquals a snd
    ans = identityOfIndiscernablesLeft FinNotEquals (_&_&_.three prf) (equalityCommutative a=fst)

finSetNotEquals' : {n : ℕ} → {a b : FinSet (succ n)} → FinNotEquals a b → (a ≡ b → False)
finSetNotEquals' {n} {a} {.a} fne refl = finSetNotEqualsSame fne

finset0Empty : FinSet zero → False
finset0Empty ()

finset1OnlyOne : (a b : FinSet 1) → a ≡ b
finset1OnlyOne fzero fzero = refl
finset1OnlyOne fzero (fsucc ())
finset1OnlyOne (fsucc ()) b

intoSmaller : {n m : ℕ} → .(n <N m) → (FinSet n → FinSet m)
intoSmaller {zero} {m} n<m = t
  where
    t : FinSet 0 → FinSet m
    t ()
intoSmaller {succ n} {zero} ()
intoSmaller {succ n} {succ m} n<m with intoSmaller (canRemoveSuccFrom<N n<m)
intoSmaller {succ n} {succ m} n<m | prev = t
  where
    t : FinSet (succ n) → FinSet (succ m)
    t fzero = fzero
    t (fsucc arg) = fsucc (prev arg)

intoSmallerInj : {n m : ℕ} → (n<m : n <N m) → Injection (intoSmaller n<m)
intoSmallerInj {zero} {zero} (le x ())
intoSmallerInj {zero} {succ m} n<m = inj
  where
    t : FinSet 0 → FinSet (succ m)
    t ()
    inj : {x y : FinSet zero} → intoSmaller (succIsPositive m) x ≡ intoSmaller (succIsPositive m) y → x ≡ y
    inj {()} {y}
intoSmallerInj {succ n} {zero} ()
intoSmallerInj {succ n} {succ m} n<m with intoSmallerInj (canRemoveSuccFrom<N n<m)
intoSmallerInj {succ n} {succ m} n<m | prevInj = inj
  where
    inj : Injection (intoSmaller n<m)
    inj {fzero} {fzero} pr = refl
    inj {fzero} {fsucc y} ()
    inj {fsucc x} {fzero} ()
    inj {fsucc x} {fsucc y} pr = applyEquality fsucc (prevInj (fsuccInjective pr))

toNat : {n : ℕ} → (a : FinSet n) → ℕ
toNat {.(succ _)} fzero = 0
toNat {.(succ _)} (fsucc a) = succ (toNat a)

toNatSmaller : {n : ℕ} → (a : FinSet n) → toNat a <N n
toNatSmaller {zero} ()
toNatSmaller {succ n} fzero = succIsPositive n
toNatSmaller {succ n} (fsucc a) = succPreservesInequality (toNatSmaller a)

ofNat : {n : ℕ} → (m : ℕ) → .(m <N n) → FinSet n
ofNat {zero} zero ()
ofNat {succ n} zero m<n = fzero
ofNat {zero} (succ m) ()
ofNat {succ n} (succ m) m<n = fsucc (ofNat {n} m (canRemoveSuccFrom<N m<n))

ofNatInjective : {n : ℕ} → (x y : ℕ) → .(pr : x <N n) → .(pr2 : y <N n) → ofNat x pr ≡ ofNat y pr2 → x ≡ y
ofNatInjective {zero} zero zero () y<n pr
ofNatInjective {zero} zero (succ y) () y<n pr
ofNatInjective {zero} (succ x) zero x<n () pr
ofNatInjective {zero} (succ x) (succ y) () y<n pr
ofNatInjective {succ n} zero zero x<n y<n pr = refl
ofNatInjective {succ n} zero (succ y) x<n y<n ()
ofNatInjective {succ n} (succ x) zero x<n y<n ()
ofNatInjective {succ n} (succ x) (succ y) x<n y<n pr = applyEquality succ (ofNatInjective x y (canRemoveSuccFrom<N x<n) (canRemoveSuccFrom<N y<n) (fsuccInjective pr))

toNatInjective : {n : ℕ} → (x y : FinSet n) → toNat x ≡ toNat y → x ≡ y
toNatInjective fzero fzero pr = refl
toNatInjective (fsucc x) (fsucc y) pr = applyEquality fsucc (toNatInjective x y (succInjective pr))

toNatOfNat : {n : ℕ} → (a : ℕ) → (a<n : a <N n) → toNat (ofNat a a<n) ≡ a
toNatOfNat {zero} zero (le x ())
toNatOfNat {zero} (succ a) (le x ())
toNatOfNat {succ n} zero a<n = refl
toNatOfNat {succ n} (succ a) a<n = applyEquality succ (toNatOfNat a (canRemoveSuccFrom<N a<n))

intoSmallerLemm : {n m : ℕ} → {n<m : n <N (succ m)} → {m<sm : m <N succ m} → (b : FinSet n) → intoSmaller n<m b ≡ ofNat m m<sm → False
intoSmallerLemm {.(succ _)} {m} {n<m} fzero pr with intoSmaller (canRemoveSuccFrom<N n<m)
intoSmallerLemm {.(succ _)} {zero} {n<m} fzero refl | bl = zeroNeverGreater (canRemoveSuccFrom<N n<m)
intoSmallerLemm {.(succ _)} {succ m} {n<m} fzero () | bl
intoSmallerLemm {.(succ _)} {m} {n<m} (fsucc b) pr with inspect (intoSmaller (canRemoveSuccFrom<N n<m))
intoSmallerLemm {.(succ _)} {zero} {n<m} (fsucc b) pr | bl with≡ _ = zeroNeverGreater (canRemoveSuccFrom<N n<m)
intoSmallerLemm {.(succ _)} {succ m} {n<m} {m<sm} (fsucc b) pr | bl with≡ p = intoSmallerLemm {n<m = canRemoveSuccFrom<N n<m} {m<sm = canRemoveSuccFrom<N m<sm} b (fsuccInjective pr)

intoSmallerNotSurj : {n m : ℕ} → {n<m : n <N m} → Surjection (intoSmaller n<m) → False
intoSmallerNotSurj {n} {zero} {le x ()} property
intoSmallerNotSurj {zero} {succ zero} {n<m} property with property fzero
... | () , _
intoSmallerNotSurj {succ n} {succ zero} {n<m} property = zeroNeverGreater (canRemoveSuccFrom<N n<m)
intoSmallerNotSurj {0} {succ (succ m)} {n<m} property with property fzero
... | () , _
intoSmallerNotSurj {succ n} {succ (succ m)} {n<m} property = problem
  where
    notHit : FinSet (succ (succ m))
    notHit = ofNat (succ m) (le zero refl)
    hitting : Sg (FinSet (succ n)) (λ i → intoSmaller n<m i ≡ notHit)
    hitting = property notHit
    problem : False
    problem with hitting
    ... | a , pr = intoSmallerLemm {succ n} {succ m} {n<m} {le 0 refl} a pr

finsetDecidableEquality : {n : ℕ} → (x y : FinSet n) → (x ≡ y) || ((x ≡ y) → False)
finsetDecidableEquality fzero fzero = inl refl
finsetDecidableEquality fzero (fsucc y) = inr λ ()
finsetDecidableEquality (fsucc x) fzero = inr λ ()
finsetDecidableEquality (fsucc x) (fsucc y) with finsetDecidableEquality x y
finsetDecidableEquality (fsucc x) (fsucc y) | inl pr rewrite pr = inl refl
finsetDecidableEquality (fsucc x) (fsucc y) | inr pr = inr (λ f → pr (fsuccInjective f))

subInjection : {n : ℕ} → {f : FinSet (succ (succ n)) → FinSet (succ (succ n))} → Injection f → (FinSet (succ n) → FinSet (succ n))
subInjection {n} {f} inj x with inspect (f (fsucc x))
subInjection {f = f} inj x | fzero with≡ _ with inspect (f fzero)
subInjection {f = f} inj x | fzero with≡ pr | fzero with≡ pr2 = exFalso (fzeroNotFsucc (inj (transitivity pr2 (equalityCommutative pr))))
subInjection {f = f} inj x | fzero with≡ _ | fsucc bl with≡ _ = bl
subInjection {f = f} inj x | fsucc bl with≡ _ = bl

subInjIsInjective : {n : ℕ} → {f : FinSet (succ (succ n)) → FinSet (succ (succ n))} → (inj : Injection f) → Injection (subInjection inj)
subInjIsInjective {f = f} inj {x} {y} pr with inspect (f (fsucc x))
subInjIsInjective {f = f} inj {x} {y} pr | fzero with≡ _ with inspect (f (fzero))
subInjIsInjective {f = f} inj {x} {y} pr | fzero with≡ pr1 | fzero with≡ pr2 = exFalso (fzeroNotFsucc (inj (transitivity pr2 (equalityCommutative pr1))))
subInjIsInjective {f = f} inj {x} {y} pr | fzero with≡ pr1 | fsucc bl with≡ _ with inspect (f (fsucc y))
subInjIsInjective {f = f} inj {x} {y} pr | fzero with≡ pr1 | fsucc bl with≡ _ | fzero with≡ x₁ with inspect (f (fzero))
subInjIsInjective {f = f} inj {x} {y} pr | fzero with≡ pr1 | fsucc bl with≡ _ | fzero with≡ x1 | fzero with≡ x2 = exFalso (fzeroNotFsucc (inj (transitivity x2 (equalityCommutative x1))))
subInjIsInjective {f = f} inj {x} {y} refl | fzero with≡ pr1 | fsucc .bl2 with≡ _ | fzero with≡ x1 | fsucc bl2 with≡ _ = fsuccInjective (inj (transitivity pr1 (equalityCommutative x1)))
subInjIsInjective {f = f} inj {x} {y} refl | fzero with≡ pr1 | fsucc .bl2 with≡ pr2 | fsucc bl2 with≡ pr3 = exFalso (fzeroNotFsucc (inj (transitivity pr2 (equalityCommutative pr3))))
subInjIsInjective {f = f} inj {x} {y} pr | fsucc bl with≡ _ with inspect (f (fsucc y))
subInjIsInjective {f = f} inj {x} {y} pr | fsucc bl with≡ _ | fzero with≡ x₁ with inspect (f fzero)
subInjIsInjective {f = f} inj {x} {y} pr | fsucc bl with≡ _ | fzero with≡ x1 | fzero with≡ x2 = exFalso (fzeroNotFsucc (inj (transitivity x2 (equalityCommutative x1))))
subInjIsInjective {f = f} inj {x} {y} refl | fsucc .bl2 with≡ x1 | fzero with≡ x₁ | fsucc bl2 with≡ x2 = exFalso (fzeroNotFsucc (inj (transitivity x2 (equalityCommutative x1))))
subInjIsInjective {f = f} inj {x} {y} refl | fsucc .y1 with≡ pr1 | fsucc y1 with≡ pr2 = fsuccInjective (inj (transitivity pr1 (equalityCommutative pr2)))

onepointBij : (f : FinSet 1 → FinSet 1) → Bijection f
Bijection.inj (onepointBij f) {x} {y} _ = finset1OnlyOne x y
Bijection.surj (onepointBij f) fzero with inspect (f fzero)
... | fzero with≡ pr = fzero , pr
... | fsucc () with≡ _
Bijection.surj (onepointBij f) (fsucc ())

nopointBij : (f : FinSet 0 → FinSet 0) → Bijection f
Bijection.inj (nopointBij f) {()}
Bijection.surj (nopointBij f) ()

private
  flip : {n : ℕ} → (f : FinSet (succ n) → FinSet (succ n)) → FinSet (succ n) → FinSet (succ n)
  flip {n} f fzero = f fzero
  flip {n} f (fsucc a) with inspect (f fzero)
  flip {n} f (fsucc a) | fzero with≡ x = fsucc a
  flip {n} f (fsucc a) | fsucc y with≡ x with finsetDecidableEquality a y
  flip {n} f (fsucc a) | fsucc y with≡ x | inl a=y = fzero
  flip {n} f (fsucc a) | fsucc y with≡ x | inr a!=y = fsucc a

  flipSwapsF0 : {n : ℕ} → {f : FinSet (succ n) → FinSet (succ n)} → (flip f (f fzero)) ≡ fzero
  flipSwapsF0 {zero} {f} with inspect (f fzero)
  flipSwapsF0 {zero} {f} | fzero with≡ x rewrite x = x
  flipSwapsF0 {zero} {f} | fsucc () with≡ x
  flipSwapsF0 {succ n} {f = f} with inspect (f fzero)
  flipSwapsF0 {succ n} {f = f} | fzero with≡ pr rewrite pr = pr
  flipSwapsF0 {succ n} {f = f} | fsucc b with≡ pr rewrite pr = ans
    where
      ans : flip f (fsucc b) ≡ fzero
      ans with inspect (f fzero)
      ans | fzero with≡ x = exFalso (fzeroNotFsucc (transitivity (equalityCommutative x) pr))
      ans | fsucc y with≡ x with finsetDecidableEquality b y
      ans | fsucc y with≡ x | inl b=y = refl
      ans | fsucc y with≡ x | inr b!=y = exFalso (b!=y (fsuccInjective (transitivity (equalityCommutative pr) x)))

  flipSwapsZero : {n : ℕ} → {f : FinSet (succ n) → FinSet (succ n)} → (flip f fzero) ≡ f fzero
  flipSwapsZero {n} {f} = refl

  flipMaintainsEverythingElse : {n : ℕ} → {f : FinSet (succ n) → FinSet (succ n)} → (x : FinSet n) → ((fsucc x ≡ f fzero) → False) → flip f (fsucc x) ≡ fsucc x
  flipMaintainsEverythingElse {n} {f} x x!=f0 with inspect (f fzero)
  flipMaintainsEverythingElse {n} {f} x x!=f0 | fzero with≡ pr = refl
  flipMaintainsEverythingElse {n} {f} x x!=f0 | fsucc bl with≡ pr with finsetDecidableEquality x bl
  flipMaintainsEverythingElse {n} {f} x x!=f0 | fsucc bl with≡ pr | inl x=bl = exFalso (x!=f0 (transitivity (applyEquality fsucc x=bl) (equalityCommutative pr)))
  flipMaintainsEverythingElse {n} {f} x x!=f0 | fsucc bl with≡ pr | inr x!=bl = refl

  bijFlip : {n : ℕ} → {f : FinSet (succ n) → FinSet (succ n)} → Bijection (flip f)
  bijFlip {zero} {f} = onepointBij (flip f)
  Bijection.inj (bijFlip {succ n} {f}) {fzero} {fzero} flx=fly = refl
  Bijection.inj (bijFlip {succ n} {f}) {fzero} {fsucc y} flx=fly with inspect (f fzero)
  Bijection.inj (bijFlip {succ n} {f}) {fzero} {fsucc y} flx=fly | fzero with≡ x rewrite x = exFalso (fzeroNotFsucc flx=fly)
  Bijection.inj (bijFlip {succ n} {f}) {fzero} {fsucc y} flx=fly | fsucc f0 with≡ x with finsetDecidableEquality y f0
  Bijection.inj (bijFlip {succ n} {f}) {fzero} {fsucc y} flx=fly | fsucc f0 with≡ x | inl x₁ = exFalso (fzeroNotFsucc (transitivity (equalityCommutative flx=fly) x))
  Bijection.inj (bijFlip {succ n} {f}) {fzero} {fsucc y} flx=fly | fsucc f0 with≡ x | inr pr = exFalso (pr (fsuccInjective (transitivity (equalityCommutative flx=fly) x)))
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fzero} flx=fly with inspect (f fzero)
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fzero} flx=fly | fzero with≡ pr = transitivity flx=fly pr
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fzero} flx=fly | fsucc f0 with≡ x₁ with finsetDecidableEquality x f0
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fzero} flx=fly | fsucc f0 with≡ pr | inl x₂ = exFalso (fzeroNotFsucc (transitivity flx=fly pr))
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fzero} flx=fly | fsucc f0 with≡ x1 | inr x!=f0 = exFalso (x!=f0 (fsuccInjective (transitivity flx=fly x1)))
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly with inspect (f fzero)
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly | fzero with≡ x₁ = flx=fly
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly | fsucc f0 with≡ x₁ with finsetDecidableEquality y f0
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly | fsucc f0 with≡ x₁ | inl y=f0 with finsetDecidableEquality x f0
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly | fsucc f0 with≡ x₁ | inl y=f0 | inl x=f0 = applyEquality fsucc (transitivity x=f0 (equalityCommutative y=f0))
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} () | fsucc f0 with≡ x₁ | inl y=f0 | inr x!=f0
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly | fsucc f0 with≡ x₁ | inr y!=f0 with finsetDecidableEquality x f0
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} () | fsucc f0 with≡ x₁ | inr y!=f0 | inl x=f0
  Bijection.inj (bijFlip {succ n} {f}) {fsucc x} {fsucc y} flx=fly | fsucc f0 with≡ x₁ | inr y!=f0 | inr x!=f0 = flx=fly
  Bijection.surj (bijFlip {succ n} {f}) fzero = f fzero , flipSwapsF0 {f = f}
  Bijection.surj (bijFlip {succ n} {f}) (fsucc b) with inspect (f fzero)
  Bijection.surj (bijFlip {succ n} {f}) (fsucc b) | fzero with≡ x = fsucc b , flipMaintainsEverythingElse {f = f} b λ pr → fzeroNotFsucc (transitivity (equalityCommutative x) (equalityCommutative pr))
  Bijection.surj (bijFlip {succ n} {f}) (fsucc b) | fsucc y with≡ x with finsetDecidableEquality y b
  Bijection.surj (bijFlip {succ n} {f}) (fsucc b) | fsucc y with≡ x | inl y=b = fzero , transitivity x (applyEquality fsucc y=b)
  Bijection.surj (bijFlip {succ n} {f}) (fsucc b) | fsucc y with≡ x | inr y!=b = fsucc b , flipMaintainsEverythingElse {f = f} b λ pr → y!=b (fsuccInjective (transitivity (equalityCommutative x) (equalityCommutative pr)))

injectionIsBijectionFinset : {n : ℕ} → {f : FinSet n → FinSet n} → Injection f → Bijection f
injectionIsBijectionFinset {zero} {f} inj = record { inj = inj ; surj = λ () }
injectionIsBijectionFinset {succ zero} {f} inj = record { inj = inj ; surj = ans }
  where
    ans : (b : FinSet (succ zero)) → Sg (FinSet (succ zero)) (λ a → f a ≡ b)
    ans fzero with inspect (f fzero)
    ans fzero | fzero with≡ x = fzero , x
    ans fzero | fsucc () with≡ x
    ans (fsucc ())
injectionIsBijectionFinset {succ (succ n)} {f} inj with injectionIsBijectionFinset {succ n} (subInjIsInjective inj)
... | sb = ans
  where
    subSurj : Surjection (subInjection inj)
    subSurj = Bijection.surj sb

    tweakedF : FinSet (succ (succ n)) → FinSet (succ (succ n))
    tweakedF fzero = fzero
    tweakedF (fsucc x) = fsucc (subInjection inj x)

    tweakedBij : Bijection tweakedF
    Bijection.inj tweakedBij {fzero} {fzero} f'x=f'y = refl
    Bijection.inj tweakedBij {fzero} {fsucc y} ()
    Bijection.inj tweakedBij {fsucc x} {fzero} ()
    Bijection.inj tweakedBij {fsucc x} {fsucc y} f'x=f'y = applyEquality fsucc ((subInjIsInjective inj) (fsuccInjective f'x=f'y))
    Bijection.surj tweakedBij fzero = fzero , refl
    Bijection.surj tweakedBij (fsucc b) with subSurj b
    ... | ans , prop = fsucc ans , applyEquality fsucc prop

    compBij : Bijection (λ i → flip f (tweakedF i))
    compBij = bijectionComp tweakedBij bijFlip

    undoTweakMakesF : {x : FinSet (succ (succ n))} → flip f (tweakedF x) ≡ f x
    undoTweakMakesF {fzero} = refl
    undoTweakMakesF {fsucc x} with inspect (f fzero)
    undoTweakMakesF {fsucc x} | fzero with≡ x₁ with inspect (f (fsucc x))
    undoTweakMakesF {fsucc x} | fzero with≡ x₁ | fzero with≡ x₂ with inspect (f fzero)
    undoTweakMakesF {fsucc x} | fzero with≡ x₁ | fzero with≡ x2 | fzero with≡ x3 = exFalso (fzeroNotFsucc (inj (transitivity x3 (equalityCommutative x2))))
    undoTweakMakesF {fsucc x} | fzero with≡ x1 | fzero with≡ x2 | fsucc y with≡ x3 = exFalso (fzeroNotFsucc (inj (transitivity x1 (equalityCommutative x2))))
    undoTweakMakesF {fsucc x} | fzero with≡ x1 | fsucc y with≡ x2 = equalityCommutative x2
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ with inspect (f (fsucc x))
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ | fzero with≡ x₂ with inspect (f fzero)
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ | fzero with≡ x2 | fzero with≡ x3 = exFalso (fzeroNotFsucc (inj (transitivity x3 (equalityCommutative x2))))
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ | fzero with≡ x₂ | fsucc pr with≡ x₃ with finsetDecidableEquality pr y
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ | fzero with≡ x2 | fsucc pr with≡ x₃ | inl x₄ = equalityCommutative x2
    undoTweakMakesF {fsucc x} | fsucc y with≡ x1 | fzero with≡ x₂ | fsucc pr with≡ x3 | inr pr!=y = exFalso (pr!=y (fsuccInjective (transitivity (equalityCommutative x3) x1)))
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ | fsucc thi with≡ x₂ with finsetDecidableEquality thi y
    undoTweakMakesF {fsucc x} | fsucc .thi with≡ x1 | fsucc thi with≡ x2 | inl refl = exFalso false
      where
        p : f fzero ≡ f (fsucc x)
        p = transitivity x1 (equalityCommutative x2)
        q : fzero ≡ fsucc x
        q = inj p
        false : False
        false = fzeroNotFsucc q
    undoTweakMakesF {fsucc x} | fsucc y with≡ x₁ | fsucc thi with≡ x2 | inr thi!=y = equalityCommutative x2

    ans : Bijection f
    ans = bijectionPreservedUnderExtensionalEq compBij undoTweakMakesF

pigeonhole : {n m : ℕ} → (m <N n) → {f : FinSet n → FinSet m} → Injection f → False
pigeonhole {zero} {zero} () {f} property
pigeonhole {zero} {succ m} () {f} property
pigeonhole {succ n} {zero} m<n {f} property = finset0Empty (f fzero)
pigeonhole {succ zero} {succ m} m<n {f} property with canRemoveSuccFrom<N m<n
pigeonhole {succ zero} {succ m} m<n {f} property | le x ()
pigeonhole {succ (succ n)} {succ zero} m<n {f} property = fzeroNotFsucc (property (transitivity f0 (equalityCommutative f1)))
  where
    f0 : f (fzero) ≡ fzero
    f0 with inspect (f fzero)
    ... | fzero with≡ x = x
    ... | fsucc () with≡ _
    f1 : f (fsucc fzero) ≡ fzero
    f1 with inspect (f (fsucc fzero))
    ... | fzero with≡ x = x
    ... | fsucc () with≡ _
pigeonhole {succ (succ n)} {succ (succ m)} m<n {f} injF = intoSmallerNotSurj {_}{_} {m<n} surj
  where
    inj : Injection ((intoSmaller m<n) ∘ f)
    inj = injComp injF (intoSmallerInj m<n)
    bij : Bijection ((intoSmaller m<n) ∘ f)
    bij = injectionIsBijectionFinset inj
    surj : Surjection (intoSmaller m<n)
    surj = compSurjLeftSurj (Bijection.surj bij)

--surjectionIsBijectionFinset : {n : ℕ} → {f : FinSet n → FinSet n} → Surjection f → Bijection f
--surjectionIsBijectionFinset {zero} {f} surj = nopointBij f
--surjectionIsBijectionFinset {succ zero} {f} surj = onepointBij f
--surjectionIsBijectionFinset {succ (succ n)} {f} record { property = property } = {!!}

ofNatToNat : {n : ℕ} → (a : FinSet n) → ofNat (toNat a) (toNatSmaller a) ≡ a
ofNatToNat {zero} ()
ofNatToNat {succ n} fzero = refl
ofNatToNat {succ n} (fsucc a) = applyEquality fsucc (ofNatToNat a)


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

module C1.LEM where
  open import Basics
  open import Bool
  open import LEM
  open import NotNot
  open import Flat
  open import Sharp
  open import C1.Base

  open import lib.NType2

  -- UNFINISHED due to ♯-ptwise problems
  ♯-prop-is-¬¬ : ∀ {i}(P : PropT i) (p : (P holds) is-codiscrete) → (P holds) ≃ ((not (not P)) holds)
  ♯-prop-is-¬¬ P p =
    iff-to-≃ {P = P} {Q = not (not P)}
      -- ⇒
         continue
      -- ⇐
         (not (not P) holds
           –⟨ lemma ⟩→
         ♯ (P holds)
           –⟨ un♯ p ⟩→
         P holds
           →∎)
    where
      postulate lemma : not (not P) holds → ♯ (P holds)
      -- The problem here is that ♯-ptwise won't rewrite to ♯ (P holds)
      -- So, we can't run the right proof.
      -- I'm not sure why though...

  nbhd-is-infinitesimal : ∀ {i} {A : hSet i} (a : ∈ A) → (nbhd a) is-infinitesimal
  nbhd-is-infinitesimal {A = (A , p)} a =
    has-level-in (((a , refl≈)^♯) ,
      (λ b' → ♯-=-retract $
                let♯ b ^♯:= b' in♯
                  (♯-=-compare
                    (<– (♯-prop-is-¬¬ (♯ₙ $ (a , refl≈) ==ₚ b)
                    (♯-is-codiscrete ((a , refl≈) == b)))
                    {!snd b!})) ^♯
                in-family (λ b' → ((a , refl≈)^♯) == b')))

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
------------------------------------------------------------------------
-- Products implemented using records
------------------------------------------------------------------------

-- It it ever becomes convenient to pattern match on records I might
-- make this the default implementation of products.

module Data.Product.Record where

open import Data.Function

infixr 4 _,_
infixr 2 _×_ _-×-_ _-,-_

------------------------------------------------------------------------
-- Definition

record Σ (a : Set) (b : a → Set) : Set where
  field
    proj₁ : a
    proj₂ : b proj₁

open Σ public

_×_ : (a b : Set) → Set
a × b = Σ a (λ _ → b)

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

_,_ : ∀ {a b} → (x : a) → b x → Σ a b
(x , y) = record {proj₁ = x; proj₂ = y}

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

map : ∀ {A B P Q} →
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g = < f ∘ proj₁ , g ∘ proj₂ >

swap : ∀ {a b} → a × b → b × a
swap = < proj₂ , proj₁ >

_-×-_ : ∀ {a b} → (a → b → Set) → (a → b → Set) → (a → b → Set)
f -×- g = f -[ _×_ ]₁- g

_-,-_ : ∀ {a b c d} → (a → b → c) → (a → b → d) → (a → b → c × d)
f -,- g = f -[ _,_ ]- g

curry : {a : Set} {b : a → Set} {c : Σ a b → Set} →
        ((p : Σ a b) → c p) →
        ((x : a) → (y : b x) → c (x , y))
curry f x y = f (x , y)

uncurry : {a : Set} {b : a → Set} {c : Σ a b → Set} →
          ((x : a) → (y : b x) → c (x , y)) →
          ((p : Σ a b) → c p)
uncurry f p = f (proj₁ p) (proj₂ p)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Usage examples of the categorical view of the Sum type
------------------------------------------------------------------------

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

module Data.Sum.Categorical.Examples where

open import Level
open import Data.Sum
import Data.Sum.Categorical.Left as Sumₗ
open import Category.Functor
open import Category.Monad

-- Note that these examples are simple unit tests, because the type
-- checker verifies them.

private
  module Examplesₗ {a b} {A : Set a} {B : Set b} where

    open import Agda.Builtin.Equality
    open import Function
    module Sₗ = Sumₗ A b

    open RawFunctor Sₗ.functor

    -- This type to the right of ⊎ needs to be a "lifted" version of (B : Set b)
    -- that lives in the universe (Set (a ⊔ b)).
    fmapId : (x : A ⊎ (Lift a B)) → (id <$> x) ≡ x
    fmapId (inj₁ x) = refl
    fmapId (inj₂ y) = refl

    open RawMonad   Sₗ.monad

    -- Now, let's show that "return" is a unit for >>=. We use Lift in exactly
    -- the same way as above. The data (x : B) then needs to be "lifted" to
    -- this new type (Lift B).
    returnUnitL : ∀ {x : B} {f : Lift a B → A ⊎ (Lift a B)}
                  → ((return (lift x)) >>= f) ≡ f (lift x)
    returnUnitL = refl

    returnUnitR : (x : A ⊎ (Lift a B)) → (x >>= return) ≡ x
    returnUnitR (inj₁ _) = refl
    returnUnitR (inj₂ _) = refl

    -- And another (limited version of a) monad law...
    bindCompose : ∀ {f g : Lift a B → A ⊎ (Lift a B)}
                → (x : A ⊎ (Lift a B))
                → ((x >>= f) >>= g) ≡ (x >>= (λ y → (f y >>= g)))
    bindCompose (inj₁ x) = refl
    bindCompose (inj₂ y) = refl


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

module Data.Empty.Base where

open import Level

data ⊥ : Type where

infix 4.5 ¬_
¬_ : Type a → Type a
¬ A = A → ⊥

⊥-elim : ⊥ → A
⊥-elim ()

max_issues_repo_name: oisdk/agda-playground