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

module Agda.Builtin.Unit where

record ⊤ : Set where
  instance constructor tt

{-# BUILTIN UNIT ⊤ #-}
{-# COMPILED_DATA ⊤ () () #-}

ext: agda

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
open import Agda.Primitive

data Foo : Setω where
  foo : Foo

bar : Foo → Foo
bar foo = foo

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --guarded #-}

postulate
  test : (@tick _ : _) → Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- ---------------------------------
-- this is the agda file implementing my own work on logic, viz. a relational
-- framework for logic.

-- These codes have been checked by Agda 2.6.0
-- ---------------------------------

module RL where

-- this file use agda standard library

open import Agda.Builtin.Equality
open import Relation.Nullary
open import Data.Empty
open import Data.Product

-- ---------------------------------
-- Logical Frame
-- ---------------------------------
record Frame : Set₁ where
  field
    Φ : Set -- the set of language
    bot : Φ -- contradiction
    top : Φ -- validity
    _⇌_ : Φ → Φ → Set -- ⇌ is interpreted as consistency relation
    symm : ∀ (x y : Φ) → x ⇌ y → y ⇌ x -- ⇌ is symmetric
    alre : ∀ (x : Φ) → ¬ (x ≡ bot) → x ⇌ x -- except for ⊥, ⇌ is reflexive
    ⊥-contra : ∀ (x : Φ) → ¬ (x ⇌ bot) -- ⊥ is in-⇌ with any x∈Φ
    ⊤-validi : ∀ (x : Φ) → ¬ (x ≡ bot) → (x ⇌ top) -- ⊤ ⇌ everything e.x. ⊥

substitution : {A : Frame} (x y z : Frame.Φ A) -- ∀x,y,z∈Φ.(x≡y ∧ x⇌z → y⇌z)
               → x ≡ y → Frame._⇌_ A x z → Frame._⇌_ A y z
substitution {A} x y z p q rewrite p = q

cons→non-contra : {A : Frame} (x : Frame.Φ A) -- ∀x∈Φ.(∃y∈Φ.(x⇌y) → x≠⊥)
                  → ∃[ y ] Frame._⇌_ A x y → ¬ (x ≡ Frame.bot A)
cons→non-contra {A} x (y , f) q = Frame.⊥-contra A y w
  where
  s : Frame._⇌_ A (Frame.bot A) y
  s = substitution {A} x (Frame.bot A) y q f
  w : Frame._⇌_ A y (Frame.bot A)
  w = Frame.symm A (Frame.bot A) y s

module Example₁ where

  data tf : Set where
    𝟘x 𝟙x : tf

  data _↔_ : tf → tf → Set where
    t-t : 𝟙x ↔ 𝟙x

  symm-tf : ∀ (x y : tf) → x ↔ y → y ↔ x
  symm-tf 𝟙x 𝟙x t-t = t-t

  alre-tf : ∀ (x : tf) → ¬ (x ≡ 𝟘x) → x ↔ x
  alre-tf 𝟙x _ = t-t
  alre-tf 𝟘x p = ⊥-elim (p refl)

  𝟙x-validi : ∀ (x : tf) → ¬ (x ≡ 𝟘x) → (x ↔ 𝟙x)
  𝟙x-validi 𝟙x _  = t-t
  𝟙x-validi 𝟘x ¬p = ⊥-elim (¬p refl)

  𝟘x-contra : ∀ (x : tf) → ¬ (x ↔ 𝟘x)
  𝟘x-contra x ()

  tfFrame : Frame -- the smallest possible normal frame
  tfFrame = record { Φ        = tf
                   ; bot      = 𝟘x
                   ; top      = 𝟙x
                   ; _⇌_      = _↔_
                   ; symm     = symm-tf
                   ; alre     = alre-tf
                   ; ⊥-contra = 𝟘x-contra
                   ; ⊤-validi = 𝟙x-validi }

-- ---------------------------------
-- Logical Consequence
-- ---------------------------------
record _⊢_ {A : Frame} (a b : Frame.Φ A) : Set where -- logical consequence
  field -- a⊢b ⇔ ∀x∈Φ.(x⇌a → x⇌b)
    fromCons : ∀ (x : Frame.Φ A) → Frame._⇌_ A x a → Frame._⇌_ A x b

-- ---------------------------------
-- properties of ⊢
refl-⊢ : {A : Frame} (a : Frame.Φ A) → _⊢_ {A} a a -- reflexive
refl-⊢ {A} a = record { fromCons = p }
  where
  p : ∀ (x : Frame.Φ A) → Frame._⇌_ A x a → Frame._⇌_ A x a
  p x q = q

trans-⊢ : {A : Frame} (a b c : Frame.Φ A) -- transitive
          → _⊢_ {A} a b → _⊢_ {A} b c → _⊢_ {A} a c
trans-⊢ {A} a b c p q = record { fromCons = f }
  where
  f : ∀ (x : Frame.Φ A) → Frame._⇌_ A x a → Frame._⇌_ A x c
  f x h = _⊢_.fromCons q x (_⊢_.fromCons p x h)
-- ---------------------------------

-- ---------------------------------
-- ∀x∈Φ.(⊥⊢x)
bot-cons : {A : Frame} (x : Frame.Φ A) -- ∀x∈Φ.∀y∈Φ.(y⇌⊥ → y⇌x)
           → ∀ (y : Frame.Φ A) → Frame._⇌_ A y (Frame.bot A) → Frame._⇌_ A y x
bot-cons {A} x y p = ⊥-elim (Frame.⊥-contra A y p)

bot-to-every : {A : Frame} (x : Frame.Φ A) → _⊢_ {A} (Frame.bot A) x
bot-to-every {A} x = record { fromCons = bot-cons {A} x }
-- ---------------------------------

-- ---------------------------------
-- ∀x∈Φ.(x⊢⊤)
top-cons : {A : Frame} (y x : Frame.Φ A) -- ∀y∈Φ.∀x∈Φ.(x⇌y → x⇌⊤)
            → Frame._⇌_ A x y → Frame._⇌_ A x (Frame.top A)
top-cons {A} y x p = Frame.⊤-validi A x (cons→non-contra {A} x (y , p))

top-from-every : {A : Frame} (x : Frame.Φ A) → _⊢_ {A} x (Frame.top A)
top-from-every {A} x = record { fromCons = top-cons {A} x }
-- ---------------------------------

-- ---------------------------------
-- the criteria for a Reasoning frame
-- ---------------------------------
record Reasoning (A : Frame) : Set₁ where
  field -- basically, reas says every consistent pair is testified
    reas : ∀ (x y : Frame.Φ A) → Frame._⇌_ A x y
           → ∃[ z ] ((¬ (z ≡ Frame.bot A)) × ((_⊢_ {A} z x) × (_⊢_ {A} z y)))

module Example₂ where
  open Example₁

  𝟘x⊢𝟘x : _⊢_ {tfFrame} 𝟘x 𝟘x
  𝟘x⊢𝟘x = refl-⊢ {tfFrame} 𝟘x

  𝟘x⊢𝟙x : _⊢_ {tfFrame} 𝟘x 𝟙x
  𝟘x⊢𝟙x = bot-to-every {tfFrame} 𝟙x

  𝟙x⊢𝟙x : _⊢_ {tfFrame} 𝟙x 𝟙x
  𝟙x⊢𝟙x = refl-⊢ {tfFrame} 𝟙x

  reas-tf : ∀ (x y : tf) → (x ↔ y)
            → ∃[ z ] ((¬ (z ≡ 𝟘x)) × ((_⊢_ {tfFrame} z x) × (_⊢_ {tfFrame} z y)))
  reas-tf 𝟘x _ ()
  reas-tf 𝟙x 𝟙x _ = (𝟙x , (p , (𝟙x⊢𝟙x , 𝟙x⊢𝟙x)))
    where
    p : ¬ (𝟙x ≡ 𝟘x)
    p ()

  Reasoning-tf : Reasoning tfFrame
  Reasoning-tf = record { reas = reas-tf }

max_stars_repo_path: Relational Logic/RL.agda

max_issues_repo_path: Relational Logic/RL.agda

max_forks_repo_path: Relational Logic/RL.agda


text:
module ICFPPrelude where

record ⊤ : Set where
  constructor ⟨⟩

data ⊥ : Set where

¬_ : Set → Set
¬_ A = A → ⊥

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

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

infixr 2 _∪_
data _∪_ A B : Set where
  inl : A → A ∪ B
  inr : B → A ∪ B

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

max_stars_repo_name: enlambdment/disco

max_issues_repo_name: enlambdment/disco

max_forks_repo_name: enlambdment/disco


text: data D (A : Set) : Set₁ where


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

module Data.Lift where

open import Level

record Lift {a} ℓ (A : Type a) : Type (a ℓ⊔ ℓ) where
  constructor lift
  field lower : A

open Lift public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Oscar.Category.Semigroupoid where

open import Oscar.Data.Equality
open import Oscar.Level
open import Oscar.Relation

record Semigroupoid
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔪} (_⊸_ : 𝔒 → 𝔒 → Ø 𝔪)
  : Ø 𝔬 ∙̂ 𝔪 where
  infixr 9 _∙_
  field
    _∙_ : ∀ {m n} → m ⊸ n → ∀ {l} → l ⊸ m → l ⊸ n
    ∙-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → (h ∙ g) ∙ f ≡ h ∙ g ∙ f

record Category
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔪} (_⊸_ : 𝔒 → 𝔒 → Ø 𝔪)
  : Ø 𝔬 ∙̂ 𝔪 where
  field
    semigroupoid : Semigroupoid _⊸_
  open Semigroupoid semigroupoid public

  field
    ε : ∀ {n} → n ⊸ n
    ε-left-identity : ∀ {m n} (σ : m ⊸ n) → ε ∙ σ ≡ σ
    ε-right-identity : ∀ {m n} (σ : m ⊸ n) → σ ∙ ε ≡ σ

record RCategory
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔪} {_⊸_ : 𝔒 → 𝔒 → Ø 𝔪}
  (category : Category _⊸_)
  : Ø 𝔬 ∙̂ 𝔪 where
  open Category category public hiding (semigroupoid)

module MCategory
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔪} {_⊸_ : 𝔒 → 𝔒 → Ø 𝔪}
  (category : Category _⊸_)
  where
  open Category category public hiding (semigroupoid)

-- open import Oscar.Category.Morphism
-- open import Oscar.Category.Setoid
-- open import Oscar.Level
-- open import Oscar.Relation

-- module _ {𝔬} {𝔪} {𝔮} (𝔐 : Morphism 𝔬 𝔪 𝔮) (open Morphism 𝔐) where
--   record IsSemigroupoid (_∙_ : Transitive _↦_) : Set (lsuc (𝔬 ⊔ 𝔪 ⊔ 𝔮)) where
--     field
--       extensionality : Extensional _∙_ _≞_
--       associativity : Associative _∙_ _≞_

-- open IsSemigroupoid ⦃ … ⦄ public

-- infixr 4 _,_
-- record Semigroupoid 𝔬 𝔪 𝔮 : Set (lsuc (𝔬 ⊔ 𝔪 ⊔ 𝔮))
--   where
--   constructor _,_

--   field
--     𝔐 : Morphism 𝔬 𝔪 𝔮

--   open Morphism 𝔐 public

--   infixl 7 _∙_
--   field _∙_ : Transitive _↦_

--   field ⦃ isSemigroupoid ⦄ : IsSemigroupoid 𝔐 _∙_
--   open IsSemigroupoid isSemigroupoid public


text:
open import Prelude hiding (id; Bool; _∷_; [])

module Examples.Infinite where
open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Substitutions
open import Implicits.Syntax.Type.Unification
open import Implicits.Resolution.Infinite.Resolution
open TypingRules _⊢ᵣ_
open import Data.Maybe
open import Data.List

tc-bool = 0
tc-int = 1

Bool : ∀ {n} → Type n
Bool = simpl (tc tc-bool)

Int : ∀ {n} → Type n
Int = simpl (tc tc-int)

module Ex₁ where
  Δ : ICtx zero
  Δ = (∀' (TVar zero ⇒ TVar zero)) ∷ []

  p : Δ ⊢ᵣ (Int ⇒ Int)
  p = r-iabs (r-simp (there (here refl))
    (i-tabs
      Int
        (i-iabs (r-simp (here refl) (i-simp (tc tc-int))) (i-simp (tc tc-int)))))

module Ex₂ where

  implicitly : ∀ {ν n} → Term ν n
  implicitly = Λ (ρ α (var zero))
    where
      α = TVar zero

  Implicitly : ∀ {ν n} {K : Ktx ν n} → K ⊢ implicitly ∈ (∀' (TVar zero ⇒ TVar zero))
  Implicitly = Λ (ρ (ua-simp [] All.[]) (var zero))


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

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

open import Level
open import Function using (_$_; flip)
open import Data.Product using (Σ; _,_; uncurry)

open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Properties
open import Categories.Category.Cartesian 𝒞
open import Categories.Category.Monoidal.Closed
open import Categories.Object.Product 𝒞
  hiding (repack≡id; repack∘; repack-cancel; up-to-iso; transport-by-iso)
open import Categories.Object.Exponential 𝒞 hiding (repack)
open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

private
  module 𝒞 = Category 𝒞
  open Category 𝒞
  open HomReasoning
  variable
    A B C   : Obj
    f g h i : A ⇒ B

-- Cartesian closed category
--   is a category with all products and exponentials
record CartesianClosed : Set (levelOfTerm 𝒞) where
  infixr 9 _^_
  -- an alternative notation for exponential, which emphasizes its internal hom natural
  infixr 5 _⇨_

  field
    cartesian : Cartesian
    exp       : Exponential A B

  module exp {A B} = Exponential (exp {A} {B})

  _^_ : Obj → Obj → Obj
  B ^ A = exp.B^A {A} {B}

  _⇨_ : Obj → Obj → Obj
  _⇨_ = flip _^_

  module cartesian = Cartesian cartesian

  open cartesian public

  B^A×A : ∀ B A → Product (B ^ A) A
  B^A×A B A = exp.product {A} {B}

  eval : Product.A×B (B^A×A B A) ⇒ B
  eval = exp.eval

  λg : C × A ⇒ B → C ⇒ B ^ A
  λg f = exp.λg product f

  λ-cong : f ≈ g → λg f ≈ λg g
  λ-cong eq = exp.λ-cong product eq

  _×id : (f : C ⇒ B ^ A) → C × A ⇒ [[ B^A×A B A ]]
  f ×id = [ product ⇒ exp.product ] f ×id

  β : eval ∘ λg f ×id ≈ f
  β = exp.β product

  η-exp : λg (eval ∘ f ×id) ≈ f
  η-exp = exp.η product

  λ-unique : eval ∘ f ×id ≈ g → f ≈ λg g
  λ-unique = exp.λ-unique product

  λ-unique₂ : eval ∘ f ×id ≈ eval ∘ g ×id → f ≈ g
  λ-unique₂ = exp.λ-unique′ product

  -- the annoying detail is that B^A×A is NOT the same as B ^ A × A, but they are isomorphic.
  -- make some infra so that the latter (which is more intuitive) can be used.

  B^A×A-iso : Product.A×B (B^A×A B A) ≅ B ^ A × A
  B^A×A-iso {B = B} {A = A} = record
    { from = repack exp.product product
    ; to   = repack product exp.product
    ; iso  = record
      { isoˡ = begin
        repack product exp.product ∘ repack exp.product product
          ≈⟨ [ exp.product ]⟨⟩∘ ⟩
        [ exp.product ]⟨ π₁ ∘ repack exp.product product , π₂ ∘ repack exp.product product ⟩
          ≈⟨ Product.⟨⟩-cong₂ exp.product project₁ project₂ ⟩
        [ exp.product ]⟨ [ exp.product ]π₁ , [ exp.product ]π₂ ⟩
          ≈⟨ Product.η exp.product ⟩
        id
          ∎
      ; isoʳ = begin
        repack exp.product product ∘ repack product exp.product
          ≈⟨ ⟨⟩∘ ⟩
        ⟨ [ exp.product ]π₁ ∘ repack product exp.product , [ exp.product ]π₂ ∘ repack product exp.product ⟩
          ≈⟨ ⟨⟩-cong₂ (Product.project₁ exp.product) (Product.project₂ exp.product) ⟩
        ⟨ π₁ , π₂ ⟩
          ≈⟨ η ⟩
        id
          ∎
      }
    }

  eval′ : B ^ A × A ⇒ B
  eval′ = eval ∘ to
    where open _≅_ B^A×A-iso

  λ-unique′ : eval′ ∘ (f ⁂ id) ≈ g → f ≈ λg g
  λ-unique′ eq = exp.λ-unique product (⟺ (pullʳ [ product ⇒ product ⇒ exp.product ]repack∘×) ○ eq)

  λ-unique₂′ : eval′ ∘ (f ⁂ id) ≈ eval′ ∘ (g ⁂ id) → f ≈ g
  λ-unique₂′ eq = (λ-unique′ eq) ○ ⟺ (λ-unique′ refl)

  β′ : eval′ ∘ (λg f ⁂ id) ≈ f
  β′ {f = f} = begin
    eval′ ∘ (λg f ⁂ id) ≈⟨ pullʳ [ product ⇒ product ⇒ exp.product ]repack∘× ⟩
    eval ∘ λg f ×id     ≈⟨ β ⟩
    f                   ∎

  η-exp′ : λg (eval′ ∘ (f ⁂ id)) ≈ f
  η-exp′ = sym (λ-unique′ refl)

  η-id′ : λg (eval′ {B = B} {A = A}) ≈ id
  η-id′ = sym (λ-unique′ (elimʳ (id×id product)))

  ⊤^A≅⊤ : ⊤ ^ A ≅ ⊤
  ⊤^A≅⊤ = record
    { from = !
    ; to   = λg !
    ; iso  = record
      { isoˡ = λ-unique₂ !-unique₂
      ; isoʳ = ⊤-id _
      }
    }

  A^⊤≅A : A ^ ⊤ ≅ A
  A^⊤≅A = record
    { from = let open _≅_ A×⊤≅A in eval′ ∘ to
    ; to   = let open _≅_ A×⊤≅A in λg from
    ; iso  = record
      { isoˡ = λ-unique₂′ $ begin
        eval′ ∘ ((λg π₁ ∘ eval′ ∘ ⟨ id , ! ⟩) ⁂ id)          ≈˘⟨ refl⟩∘⟨ first∘first ⟩
        eval′ ∘ ((λg π₁ ⁂ id) ∘ ((eval′ ∘ ⟨ id , ! ⟩) ⁂ id)) ≈⟨ pullˡ β′ ⟩
        π₁ ∘ ((eval′ ∘ ⟨ id , ! ⟩) ⁂ id)                     ≈⟨ helper ⟩
        eval′ ∘ (id ⁂ id)                                    ∎
      ; isoʳ = firstid ! $ begin
        ((eval′ ∘ ⟨ id , ! ⟩) ∘ λg π₁) ⁂ id                  ≈˘⟨ first∘first ⟩
        (eval′ ∘ ⟨ id , ! ⟩ ⁂ id) ∘ (λg π₁ ⁂ id)             ≈⟨ helper′ ⟩∘⟨refl ⟩
        (⟨ id , ! ⟩ ∘ eval′) ∘ (λg π₁ ⁂ id)                  ≈⟨ pullʳ β′ ⟩
        ⟨ id , ! ⟩ ∘ π₁                                      ≈⟨ ⟨⟩∘ ⟩
        ⟨ id ∘ π₁ , ! ∘ π₁ ⟩                                 ≈⟨ ⟨⟩-cong₂ identityˡ !-unique₂ ⟩
        ⟨ π₁ , π₂ ⟩                                          ≈⟨ η ⟩
        id                                                   ∎
      }
    }
    where helper = begin
            π₁ ∘ ((eval′ ∘ ⟨ id , ! ⟩) ⁂ id)                 ≈⟨ project₁ ⟩
            (eval′ ∘ ⟨ id , ! ⟩) ∘ π₁                        ≈⟨ pullʳ ⟨⟩∘ ⟩
            eval′ ∘ ⟨ id ∘ π₁ , ! ∘ π₁ ⟩                     ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ !-unique₂ ⟩
            eval′ ∘ (id ⁂ id)                                ∎
          helper′ = let open _≅_ A×⊤≅A in begin
            (eval′ ∘ ⟨ id , ! ⟩) ⁂ id                        ≈⟨ introˡ isoˡ ⟩
            (⟨ id , ! ⟩ ∘ π₁) ∘ ((eval′ ∘ ⟨ id , ! ⟩) ⁂ id)  ≈⟨ pullʳ helper ⟩
            ⟨ id , ! ⟩ ∘ (eval′ ∘ (id ⁂ id))                 ≈⟨ refl⟩∘⟨ elimʳ (id×id product) ⟩
            ⟨ id , ! ⟩ ∘ eval′                               ∎

  -- we use -⇨- to represent the bifunctor.
  -- -^- would generate a bifunctor of type Bifunctor 𝒞 𝒞.op 𝒞 which is not very typical.
  -⇨- : Bifunctor 𝒞.op 𝒞 𝒞
  -⇨- = record
    { F₀           = uncurry _⇨_
    ; F₁           = λ where
      (f , g) → λg (g ∘ eval′ ∘ second f)
    ; identity     = λ-cong (identityˡ ○ (elimʳ (id×id product))) ○ η-id′
    ; homomorphism = λ-unique₂′ helper
    ; F-resp-≈     = λ where
      (eq₁ , eq₂) → λ-cong (∘-resp-≈ eq₂ (∘-resp-≈ʳ (⁂-cong₂ refl eq₁)))
    }
    where helper : eval′ ∘ first (λg ((g ∘ f) ∘ eval′ ∘ second (h ∘ i)))
                 ≈ eval′ ∘ first (λg (g ∘ eval′ ∘ second i) ∘ λg (f ∘ eval′ ∘ second h))
          helper {g = g} {f = f} {h = h} {i = i} = begin
            eval′ ∘ first (λg ((g ∘ f) ∘ eval′ ∘ second (h ∘ i)))                         ≈⟨ β′ ⟩
            (g ∘ f) ∘ eval′ ∘ second (h ∘ i)                                              ≈˘⟨ refl⟩∘⟨ pullʳ second∘second ⟩
            (g ∘ f) ∘ (eval′ ∘ second h) ∘ second i                                       ≈˘⟨ pullˡ refl ⟩
            g ∘ f ∘ (eval′ ∘ second h) ∘ second i                                         ≈˘⟨ refl⟩∘⟨ assoc ⟩
            g ∘ (f ∘ eval′ ∘ second h) ∘ second i                                         ≈˘⟨ refl⟩∘⟨ pullˡ β′ ⟩
            g ∘ eval′ ∘ first (λg (f ∘ eval′ ∘ second h)) ∘ second i                      ≈⟨ refl⟩∘⟨ pushʳ first↔second ⟩
            g ∘ (eval′ ∘ second i) ∘ first (λg (f ∘ eval′ ∘ second h))                    ≈˘⟨ assoc ⟩
            (g ∘ eval′ ∘ second i) ∘ first (λg (f ∘ eval′ ∘ second h))                    ≈˘⟨ pullˡ β′ ⟩
            eval′ ∘ first (λg (g ∘ eval′ ∘ second i)) ∘ first (λg (f ∘ eval′ ∘ second h)) ≈⟨ refl⟩∘⟨ first∘first ⟩
            eval′ ∘ first (λg (g ∘ eval′ ∘ second i) ∘ λg (f ∘ eval′ ∘ second h))         ∎

  _⇨- : Obj → Endofunctor 𝒞
  _⇨- = appˡ -⇨-

  -⇨_ : Obj → Functor 𝒞.op 𝒞
  -⇨_ = appʳ -⇨-

  module _ where
    private
      A⇨[-×A] : Obj → Endofunctor 𝒞
      A⇨[-×A] A = A ⇨- ∘F -× A

      module A⇨[-×A] {A} = Functor (A⇨[-×A] A)

      [A⇨-]×A : Obj → Endofunctor 𝒞
      [A⇨-]×A A = -× A ∘F A ⇨-

      module [A⇨-]×A {A} = Functor ([A⇨-]×A A)

    closedMonoidal : Closed monoidal
    closedMonoidal = record
      { [-,-]   = -⇨-
      ; adjoint = λ {A} → record
        { unit   = ntHelper record
          { η       = λ _ → λg id
          ; commute = λ f → λ-unique₂′ $ begin
            eval′ ∘ first (λg id ∘ f)                     ≈˘⟨ refl⟩∘⟨ first∘first ⟩
            eval′ ∘ first (λg id) ∘ first f               ≈⟨ cancelˡ β′ ⟩
            first f                                       ≈˘⟨ cancelʳ β′ ⟩
            (first f ∘ eval′)  ∘ first (λg id)            ≈˘⟨ ∘-resp-≈ʳ (elimʳ (id×id product)) ⟩∘⟨refl ⟩
            (first f ∘ eval′ ∘ first id)  ∘ first (λg id) ≈˘⟨ pullˡ β′ ⟩
            eval′ ∘ first (A⇨[-×A].F₁ f) ∘ first (λg id)  ≈⟨ refl⟩∘⟨ first∘first ⟩
            eval′ ∘ first (A⇨[-×A].F₁ f ∘ λg id)          ∎
          }
        ; counit = ntHelper record
          { η       = λ _ → eval′
          ; commute = λ f → begin
            eval′ ∘ [A⇨-]×A.F₁ f ≈⟨ β′ ⟩
            f ∘ eval′ ∘ first id ≈⟨ refl⟩∘⟨ elimʳ (id×id product) ⟩
            f ∘ eval′            ∎
          }
        ; zig    = β′
        ; zag    = λ-unique₂′ $ begin
          eval′ ∘ first (λg (eval′ ∘ eval′ ∘ second id) ∘ λg id)
                                          ≈˘⟨ refl⟩∘⟨ first∘first ⟩
          eval′ ∘ first (λg (eval′ ∘ eval′ ∘ second id)) ∘ first (λg id)
                                          ≈⟨ pullˡ β′ ⟩
          (eval′ ∘ eval′ ∘ second id) ∘ first (λg id)
                                          ≈⟨ ∘-resp-≈ʳ (elimʳ (id×id product)) ⟩∘⟨refl ⟩
          (eval′ ∘ eval′) ∘ first (λg id) ≈⟨ cancelʳ β′ ⟩
          eval′                           ≈˘⟨ elimʳ (id×id product) ⟩
          eval′ ∘ first id                ∎
        }
      ; mate    = λ {X Y} f → record
        { commute₁ = λ-unique₂′ $ begin
          eval′ ∘ first (λg (second f ∘ eval′ ∘ second id) ∘ λg id)         ≈˘⟨ refl⟩∘⟨ first∘first ⟩
          eval′ ∘ first (λg (second f ∘ eval′ ∘ second id)) ∘ first (λg id) ≈⟨ pullˡ β′ ⟩
          (second f ∘ eval′ ∘ second id) ∘ first (λg id)                    ≈⟨ ∘-resp-≈ʳ (elimʳ (id×id product)) ⟩∘⟨refl ⟩
          (second f ∘ eval′) ∘ first (λg id)                                ≈⟨ cancelʳ β′ ⟩
          second f                                                          ≈˘⟨ cancelˡ β′ ⟩
          eval′ ∘ first (λg id) ∘ second f                                  ≈⟨ pushʳ first↔second ⟩
          (eval′ ∘ second f) ∘ first (λg id)                                ≈˘⟨ identityˡ ⟩∘⟨refl ⟩
          (id ∘ eval′ ∘ second f) ∘ first (λg id)                           ≈˘⟨ pullˡ β′ ⟩
          eval′ ∘ first (λg (id ∘ eval′ ∘ second f)) ∘ first (λg id)        ≈⟨ refl⟩∘⟨ first∘first ⟩
          eval′ ∘ first (λg (id ∘ eval′ ∘ second f) ∘ λg id)                ∎
        ; commute₂ = begin
          eval′ ∘ first (λg (id ∘ eval′ ∘ second f)) ≈⟨ β′ ⟩
          id ∘ eval′ ∘ second f                      ≈⟨ identityˡ ⟩
          eval′ ∘ second f                           ∎
        }
      }

  module closedMonoidal = Closed closedMonoidal

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
{-

        Agda Implementors' Meeting VI

                  Göteborg
             May 24 - 30, 2007

                Hello Agda!

                Ulf Norell

-}

-- Now we're getting somewhere! Inductive families of datatypes.

module Families where

-- You can import modules defined in other files.
-- More details later...
--open import Naturals

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

infixl 60 _+_
infixl 80 _*_

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

_*_ : Nat -> Nat -> Nat
zero  * m = zero
suc n * m = m + n * m

-- Think of an inductive family...
module Vec where

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

  infixr 40 _::_

  -- Some simple functions
  head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
  head (x :: _) = x  -- no need for a [] case

  -- Does the definition look familiar?
  map : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
  map f []        = []
  map f (x :: xs) = f x :: map f xs

  t1 : Vec Nat (suc (suc zero))
  t1 = map (_+_ three) (zero :: suc three :: [])
     where three = suc (suc (suc zero))

  infixr 40 _++_

  _++_ : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
  []        ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

{-

  Wait a second.. what's really going on here?

  All the indices were conveniently implicit!

-}

-- Ok. Let's make the implicit stuff explicit.
{-
module WhatsGoingOnHere? where

  open Vec using (Vec; []; _::_)
-}

  -- Now what's this funny dot thing?
  map' : {A B : Set}(n : Nat) -> (A -> B) -> Vec A n -> Vec B n
  map' .zero    f []              = []
  map' .(suc _) f (x :: xs) = f x :: map' _ f xs

  -- Basically the dot means: inside is not a pattern at all but a
  -- term whose value is uniquely determined by type checking
  -- the actual pattern.

  -- In the cases above the types of the patterns
  --   [] and (_::_ {n} x xs)
  -- forces the first argument to be zero and suc n respectively.
  -- So, that's what we write.

  -- We could spend hours talking about this, but let's move on...

-- Let's do some other interesting families.

-- The identity type.
data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

infix 30 _==_
infix 20 ¬_

-- In the presence of families we get a lot more empty types.

data Bool : Set where
  true  : Bool
  false : Bool

data False : Set where

¬_ : Set -> Set
¬ A = A -> False

_≠_ : {A : Set} -> A -> A -> Set
x ≠ y = ¬ x == y

true≠false : true == false -> False -- true ≠ false
true≠false ()

-- [The following example might have worked at AIM6, but it does not
-- work now, so I commented it out. /NAD]

-- lem : (n : Nat) -> n == suc n -> False
-- lem n ()

-- Why does this work: true == false is an empty type.

{-

  What's next?

-}

-- Actually, inductive families are sufficiently fun that
-- you'll never get bored, but there's even more fun to be had.

-- Move on to: With.agda

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
primitive
  primLevelSuc : _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module PiPointed where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product renaming (map to map×)
open import Relation.Binary.PropositionalEquality

open import Singleton
open import PlainPi

infixr 90 _#_

------------------------------------------------------------------------------
-- Pointed types and singleton types

data ∙𝕌 : Set where
  _#_ : (t : 𝕌) → (v : ⟦ t ⟧) → ∙𝕌
  _∙×ᵤ_ : ∙𝕌 → ∙𝕌 → ∙𝕌
  _∙+ᵤl_ : ∙𝕌 → ∙𝕌 → ∙𝕌
  _∙+ᵤr_ : ∙𝕌 → ∙𝕌 → ∙𝕌
  Singᵤ : ∙𝕌 → ∙𝕌

∙⟦_⟧ : ∙𝕌 → Σ[ A ∈ Set ] A
∙⟦ t # v ⟧ = ⟦ t ⟧ , v
∙⟦ T₁ ∙×ᵤ T₂ ⟧ = zip _×_ _,_ ∙⟦ T₁ ⟧ ∙⟦ T₂ ⟧
∙⟦ T₁ ∙+ᵤl T₂ ⟧ = zip _⊎_ (λ x _ → inj₁ x) ∙⟦ T₁ ⟧ ∙⟦ T₂ ⟧
∙⟦ T₁ ∙+ᵤr T₂ ⟧ = zip _⊎_ (λ _ y → inj₂ y) ∙⟦ T₁ ⟧ ∙⟦ T₂ ⟧
∙⟦ Singᵤ T ⟧ = < uncurry Singleton , (λ y → proj₂ y , refl) > ∙⟦ T ⟧

data _∙⟶_ : ∙𝕌 → ∙𝕌 → Set where
  ∙c :  {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} → (c : t₁ ⟷ t₂) →
        t₁ # v ∙⟶ t₂ # (eval c v)
  ∙id⟷ : {T : ∙𝕌} → T ∙⟶ T
  _∙⊚_ : {T₁ T₂ T₃ : ∙𝕌} → (T₁ ∙⟶ T₂) → (T₂ ∙⟶ T₃) → (T₁ ∙⟶ T₃)
  ∙Singᵤ : (T₁ T₂ : ∙𝕌) → (T₁ ∙⟶ T₂) → (Singᵤ T₁ ∙⟶ Singᵤ T₂)
  -- monad
  return : (T : ∙𝕌) → T ∙⟶ Singᵤ T
  join : (T : ∙𝕌) → Singᵤ (Singᵤ T) ∙⟶ Singᵤ T
  tensorl : (T₁ T₂ : ∙𝕌) → (Singᵤ T₁ ∙×ᵤ T₂) ∙⟶ Singᵤ (T₁ ∙×ᵤ T₂)
  tensorr : (T₁ T₂ : ∙𝕌) → (T₁ ∙×ᵤ Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙×ᵤ T₂)
  tensor : (T₁ T₂ : ∙𝕌) → (Singᵤ T₁ ∙×ᵤ Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙×ᵤ T₂)
  untensor : (T₁ T₂ : ∙𝕌) → Singᵤ (T₁ ∙×ᵤ T₂) ∙⟶ (Singᵤ T₁ ∙×ᵤ Singᵤ T₂)
  plusl : (T₁ T₂ : ∙𝕌) → (Singᵤ T₁ ∙+ᵤl T₂) ∙⟶ Singᵤ (T₁ ∙+ᵤl T₂)
  plusr : (T₁ T₂ : ∙𝕌) → (T₁ ∙+ᵤr Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙+ᵤr T₂)
  --    plus : (T₁ T₂ : ∙𝕌) → (Singᵤ T₁ ∙+ᵤl Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙+ᵤl T₂)  -- lobsided, feels wrong
  -- comonad
  extract : (T : ∙𝕌) → Singᵤ T ∙⟶ T
  duplicate : (T : ∙𝕌) → Singᵤ T ∙⟶ Singᵤ (Singᵤ T)
  cotensorl : (T₁ T₂ : ∙𝕌) → Singᵤ (T₁ ∙×ᵤ T₂) ∙⟶ (Singᵤ T₁ ∙×ᵤ T₂)
  cotensorr : (T₁ T₂ : ∙𝕌) → Singᵤ (T₁ ∙×ᵤ T₂) ∙⟶ (T₁ ∙×ᵤ Singᵤ T₂)
  coplusl : (T₁ T₂ : ∙𝕌) → Singᵤ (T₁ ∙+ᵤl T₂) ∙⟶ (Singᵤ T₁ ∙+ᵤl T₂)
  coplusr : (T₁ T₂ : ∙𝕌) → Singᵤ (T₁ ∙+ᵤr T₂) ∙⟶ (T₁ ∙+ᵤr Singᵤ T₂)

∙eval : {T₁ T₂ : ∙𝕌} → (C : T₁ ∙⟶ T₂) →
  let (t₁ , v₁) = ∙⟦ T₁ ⟧
      (t₂ , v₂) = ∙⟦ T₂ ⟧
  in Σ (t₁ → t₂) (λ f → f v₁ ≡ v₂)
∙eval ∙id⟷ = (λ x → x) , refl
∙eval (∙c c) = eval c , refl
∙eval (C₁ ∙⊚ C₂) with ∙eval C₁ | ∙eval C₂
... | (f , p) | (g , q) = (λ x → g (f x)) , trans (cong g p) q
∙eval (∙Singᵤ T₁ T₂ C) with ∙⟦ T₁ ⟧ | ∙⟦ T₂ ⟧ | ∙eval C
... | t₁ , v₁ | t₂ , .(f v₁) | f , refl = (λ {(x , refl) → f x , refl}) , refl
∙eval (return T) = (λ _ → proj₂ ∙⟦ T ⟧ , refl) , refl
∙eval (join T) = (λ { (._ , refl) → (proj₂ ∙⟦ T ⟧) , refl} ) , refl
∙eval (tensorl T₁ T₂) = (λ {_ → (proj₂ ∙⟦ T₁ ⟧ , proj₂ ∙⟦ T₂ ⟧) , refl}) , refl
∙eval (tensorr T₁ T₂) = (λ {_ → (proj₂ ∙⟦ T₁ ⟧ , proj₂ ∙⟦ T₂ ⟧) , refl}) , refl
∙eval (tensor T₁ T₂) = (λ {_ → (proj₂ ∙⟦ T₁ ⟧ , proj₂ ∙⟦ T₂ ⟧) , refl}) , refl
∙eval (untensor T₁ T₂) = (λ _ → ((proj₂ ∙⟦ T₁ ⟧ , refl) , (proj₂ ∙⟦ T₂ ⟧ , refl))) , refl
∙eval (plusl T₁ T₂) = (λ _ → inj₁ (proj₂ ∙⟦ T₁ ⟧) , refl) , refl
∙eval (plusr T₁ T₂) = (λ _ → inj₂ (proj₂ ∙⟦ T₂ ⟧) , refl) , refl
-- ∙eval (plus T₁ T₂) with ∙⟦ T₁ ⟧ | ∙⟦ T₂ ⟧
-- ... | t₁ , v₁ | t₂ , v₂ = (λ _ → inj₁ v₁ , refl) , refl
∙eval (extract T) = (λ {(w , refl) → w}) , refl
∙eval (duplicate T) = (λ {(w , refl) → (w , refl) , refl}) , refl
∙eval (cotensorl T₁ T₂) = (λ _ → ((proj₂ ∙⟦ T₁ ⟧ , refl) , proj₂ ∙⟦ T₂ ⟧)) , refl
∙eval (cotensorr T₁ T₂) = (λ _ → (proj₂ ∙⟦ T₁ ⟧ , (proj₂ ∙⟦ T₂ ⟧) , refl)) , refl
∙eval (coplusl T₁ T₂) = (λ _ → inj₁ (proj₂ ∙⟦ T₁ ⟧ , refl)) , refl
∙eval (coplusr T₁ T₂) = (λ _ → inj₂ (proj₂ ∙⟦ T₂ ⟧ , refl)) , refl

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --no-universe-polymorphism #-}
open import Induction.WellFounded as WF
open import Induction.Nat
open import Relation.Binary.Core hiding (Total)
open import Relation.Unary as U using (Decidable)
open import Relation.Nullary
open import Function using (_on_)
open import Data.Nat
import Level as L using (zero)
open import Data.List

open import BagEquality

module Lists where

infixr 8 _<l_

_<l_ : {A : Set} → Rel (List A) L.zero
_<l_ = Data.Nat._<′_ on length

<l-wellFounded : {A : Set} → Well-founded (_<l_ {A = A})
<l-wellFounded = newWf where
          module InverseOfProj = WF.Inverse-image length
          newWf = InverseOfProj.well-founded <′-well-founded

data Ordered  : {A : Set} → Rel A _ → List A → Set where
                 NilIsOrd : {A : Set} {LEQ : Rel A _} → Ordered LEQ []
                 SingleIsOrd : {A : Set} {LEQ : Rel A _} {x : A} → Ordered LEQ [ x ]
                 HeadTailOrd : {A : Set} {LEQ : Rel A _} {x y : A} {zs : List A} → LEQ x y → Ordered LEQ (y ∷ zs) → Ordered LEQ (x ∷ (y ∷ zs))

cons-Order-cong : {A : Set} → {LEQ : Rel A L.zero} → {x : A} → {ys : List A} → (∀ z → z ∈ ys → LEQ x z) → Ordered LEQ ys → Ordered LEQ (x ∷ ys)
cons-Order-cong {A} {LEQ} {y} {[]} _ _ = SingleIsOrd
cons-Order-cong {A} {LEQ} {x} {y ∷ ys} xLEQ ord-ys = HeadTailOrd (xLEQ y (inj₁ refl)) ord-ys

++-Order-cong : {A : Set} {LEQ : Rel A L.zero} → {xs ys : List A} {y : A} → (∀ z → z ∈ xs → LEQ z y) → Ordered LEQ xs → Ordered LEQ (y ∷ ys) → Ordered LEQ (xs ++ (y ∷ ys))
++-Order-cong {A} {LEQ} {[]}             {ys} {y} _        _                          ord-y∷ys = ord-y∷ys
++-Order-cong {A} {LEQ} {x ∷ []}         {ys} {y} yGEQ     _                          ord-y∷ys = HeadTailOrd (yGEQ x (inj₁ refl)) ord-y∷ys
++-Order-cong {A} {LEQ} {x₁ ∷ (x₂ ∷ xs)} {ys} {y} yGEQ (HeadTailOrd x₁LEQx₂ ord-x∷xs) ord-y∷ys = HeadTailOrd x₁LEQx₂ (++-Order-cong (λ z zIn → yGEQ z (inj₂ zIn)) ord-x∷xs ord-y∷ys)

Total : {A : Set} → Rel A L.zero → Set
Total {A} LEQ = (x y : A) → LEQ x y ⊕ LEQ y x

data ListPrimitive : {A : Set} → List A → Set where
            NilIsPrim : ∀{A} → ListPrimitive {A = A} []

consIsNotPrim : {A : Set} → {x : A} → {xs : List A} → ¬ ListPrimitive (x ∷ xs)
consIsNotPrim ()

primDec : {A : Set} → U.Decidable (ListPrimitive {A = A})
primDec []       = yes NilIsPrim
primDec (x ∷ xs) = no consIsNotPrim

data ListPrimitive2 : {A : Set} → List A → Set where
           NilIsPrim2 : ∀{A} → ListPrimitive2 {A = A} []
           SingleIsPrim2 : ∀{A} {x : A} → ListPrimitive2 (x ∷ [])

consConsIsNotPrim2 : {A : Set} → {x y : A} → {zs : List A} → ¬ ListPrimitive2 (x ∷ (y ∷ zs))
consConsIsNotPrim2 ()

prim2Dec : {A : Set} → U.Decidable (ListPrimitive2 {A = A})
prim2Dec [] = yes NilIsPrim2
prim2Dec (x ∷ []) = yes SingleIsPrim2
prim2Dec (x ∷ (y ∷ zs)) = no consConsIsNotPrim2

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

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

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


text:
module Generic.Lib.Equality.Propositional where

open import Level
open import Relation.Binary
open import Data.Empty

infix 3 _≡_ _≢_ _≗_

data _≡_ {α} {A : Set α} (x : A) : A -> Set where
  instance refl : x ≡ x

pattern lrefl = lift refl

_≢_ : ∀ {α} {A : Set α} -> A -> A -> Set
x ≢ y = x ≡ y -> ⊥

_≗_ : ∀ {α β} {A : Set α} {B : A -> Set β} -> (∀ x -> B x) -> (∀ x -> B x) -> Set α
f ≗ g = ∀ x -> f x ≡ g x

sym : ∀ {α} {A : Set α} {x y : A} -> x ≡ y -> y ≡ x
sym refl = refl

trans : ∀ {α} {A : Set α} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
trans refl refl = refl

left : ∀ {α} {A : Set α} {x y z : A} -> y ≡ x -> z ≡ x -> y ≡ z
left refl refl = refl

right : ∀ {α} {A : Set α} {x y z : A} -> x ≡ y -> x ≡ z -> y ≡ z
right refl refl = refl

subst : ∀ {α β} {A : Set α} {x y} -> (B : A -> Set β) -> x ≡ y -> B x -> B y
subst B refl z = z

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

cong₂ : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ} {x₁ x₂ y₁ y₂}
      -> (g : A -> B -> C) -> x₁ ≡ x₂ -> y₁ ≡ y₂ -> g x₁ y₁ ≡ g x₂ y₂
cong₂ g refl refl = refl

≡-Setoid : ∀ {α} -> Set α -> Setoid α zero
≡-Setoid A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; isEquivalence = record
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
  }

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module agda where
open import IO

main = run (putStrLn "Happy New Year 1396")

max_stars_repo_name: AliMD/happy-new-year

max_issues_repo_name: AliMD/happy-new-year

max_forks_repo_name: AliMD/happy-new-year


text:
module Data.QuadTree.Implementation.PublicFunctions 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.Implementation.PropDepthRelation
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.DataLenses
open import Data.QuadTree.Implementation.SafeFunctions

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic

import Data.QuadTree.Implementation.Definition
import Data.QuadTree.Implementation.ValidTypes
import Data.QuadTree.Implementation.QuadrantLenses
import Data.QuadTree.Implementation.DataLenses
import Data.QuadTree.Implementation.SafeFunctions
#-}

---- Unsafe functions (Original)

makeTree : {t : Set} {{eqT : Eq t}} -> (size : Nat × Nat) -> t -> QuadTree t
makeTree size v = qtFromSafe $ makeTreeSafe size v
{-# COMPILE AGDA2HS makeTree #-}

getLocation : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> {dep : Nat}
  -> (qt : QuadTree t)
  -> {.(IsTrue (isInsideQuadTree loc qt))}
  -> {.(IsTrue (isValid dep (treeToQuadrant qt)))} -> {.(IsTrue (dep == maxDepth qt))}
  -> t
getLocation loc qt {inside} {p} {q} = getLocationSafe loc (maxDepth qt) (qtToSafe qt {p} {q}) {inside}
{-# COMPILE AGDA2HS getLocation #-}

setLocation : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> t
  -> {dep : Nat} -> (qt : QuadTree t)
  -> {.(IsTrue (isInsideQuadTree loc qt))}
  -> {.(IsTrue (isValid dep (treeToQuadrant qt)))} -> {.(IsTrue (dep == maxDepth qt))}
  -> QuadTree t
setLocation loc v qt {inside} {p} {q} = qtFromSafe $ setLocationSafe loc (maxDepth qt) v (qtToSafe qt {p} {q}) {inside}
{-# COMPILE AGDA2HS setLocation #-}

mapLocation : {t : Set} {{eqT : Eq t}}
  -> (loc : Nat × Nat) -> (t -> t)
  -> {dep : Nat} -> (qt : QuadTree t)
  -> {.(IsTrue (isInsideQuadTree loc qt))}
  -> {.(IsTrue (isValid dep (treeToQuadrant qt)))} -> {.(IsTrue (dep == maxDepth qt))}
  -> QuadTree t
mapLocation loc f qt {inside} {p} {q} = qtFromSafe $ mapLocationSafe loc (maxDepth qt) f (qtToSafe qt {p} {q}) {inside}
{-# COMPILE AGDA2HS mapLocation #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Group.Semigroup where

open import Algebra.Category
open import Core

-- A semigroup is an associative binary function.

record SemigroupOver {a r} (A : Set a) (Eq : Equiv {r = r} A) : Set (a ⊔ r) where
  open Equiv Eq

  field
    _⋄_    : A → A → A
    ⋄-cong : ∀ {x1 x2 y1 y2} → x1 ≈ x2 → y1 ≈ y2 → x1 ⋄ y1 ≈ x2 ⋄ y2
    assoc  : ∀ x y z → (x ⋄ y) ⋄ z ≈ x ⋄ (y ⋄ z)

  semigroupoid : Semigroupoid
  semigroupoid =
    record {
      Ob = ⊤;
      Hom = λ _ _ → A;
      Eq = Eq;
      _∘_ = _⋄_;
      ∘-cong = ⋄-cong;
      assoc = assoc
    }

  open Semigroupoid semigroupoid public
    using (Epic; Monic)

record Semigroup {a r} : Set (lsuc (a ⊔ r)) where
  field
    A  : Set a
    Eq : Equiv {r = r} A
    semigroupOver : SemigroupOver A Eq

  open Equiv Eq public
  open SemigroupOver semigroupOver public

-- Commutative semigroups.

record IsComm {a r} (S : Semigroup {a} {r}) : Set (a ⊔ r) where
  open Semigroup S

  field
    comm : ∀ x y → x ⋄ y ≈ y ⋄ x

-- A semigroup morphism is a function that maps the elements of one
-- semigroup to another while preserving the compositional structure.

record SemigroupMorphism
           {sa sr ta tr}
           (S : Semigroup {sa} {sr})
           (T : Semigroup {ta} {tr})
           : Set (sa ⊔ ta ⊔ sr ⊔ tr)
       where

  private
    module S = Semigroup S
    module T = Semigroup T

  field
    map : S.A → T.A
    map-cong : ∀ {x y} → x S.≈ y → map x T.≈ map y
    ⋄-preserving : ∀ x y → map (x S.⋄ y) T.≈ map x T.⋄ map y

  semifunctor : Semifunctor S.semigroupoid T.semigroupoid
  semifunctor =
    record {
      F = λ _ → tt;
      map = map;
      map-cong = map-cong;
      ∘-preserving = ⋄-preserving
    }

-- An equivalence relation on semigroup morphisms that considers
-- semigroup morphisms to be equal iff they map every element in the
-- domain to the same element in the codomain.

SemigroupMorphismEq :
  ∀ {sa sr ta tr}
    {S : Semigroup {sa} {sr}} {T : Semigroup {ta} {tr}}
  → Equiv (SemigroupMorphism S T)
SemigroupMorphismEq {T = T} =
  record {
    _≈_ = λ F G →
            let module F = SemigroupMorphism F
                module G = SemigroupMorphism G
            in ∀ x → F.map x ≈ G.map x;
    refl = λ _ → refl;
    sym = λ x≈y x → sym (x≈y x);
    trans = λ x≈y y≈z x → trans (x≈y x) (y≈z x)
  }

  where
  module T = Semigroup T
  open Equiv T.Eq

-- The category of semigroups and semigroup morphisms.

Semigroups : ∀ {a r} → Category
Semigroups {a} {r} =
  record {
    semigroupoid = record {
      Ob = Semigroup {a} {r};
      Hom = SemigroupMorphism;
      Eq = SemigroupMorphismEq;
      _∘_ = _∘_;
      ∘-cong = λ {_} {_} {_} {F1} {F2} {G1} {G2} → ∘-cong {F1 = F1} {F2} {G1} {G2};
      assoc = assoc
    };
    id = id;
    left-id = left-right-id;
    right-id = left-right-id
  }

  where
  open module MyEquiv {S T} = Equiv (SemigroupMorphismEq {S = S} {T = T})

  _∘_ : ∀ {S T U} → SemigroupMorphism T U → SemigroupMorphism S T → SemigroupMorphism S U
  _∘_ {S} {T} {U} F G =
    record {
      map = F.map Sets.∘ G.map;
      map-cong = λ p → F.map-cong (G.map-cong p);
      ⋄-preserving = λ x y →
        U.begin
          F.map (G.map (x S.⋄ y))             U.≈[ F.map-cong (G.⋄-preserving _ _) ]
          F.map (G.map x T.⋄ G.map y)         U.≈[ F.⋄-preserving _ _ ]
          F.map (G.map x) U.⋄ F.map (G.map y)
        U.qed
    }

    where
    module S = Semigroup S
    module T = Semigroup T
    module U = Semigroup U

    module F = SemigroupMorphism F
    module G = SemigroupMorphism G

  ∘-cong :
    ∀ {S T U}
      {F1 F2 : SemigroupMorphism T U}
      {G1 G2 : SemigroupMorphism S T}
    → F1 ≈ F2 → G1 ≈ G2 → F1 ∘ G1 ≈ F2 ∘ G2
  ∘-cong {U = U} {F1} {F2} {G1} {G2} F1≈F2 G1≈G2 x =
    U.begin
      F1.map (G1.map x) U.≈[ F1.map-cong (G1≈G2 _) ]
      F1.map (G2.map x) U.≈[ F1≈F2 _ ]
      F2.map (G2.map x)
    U.qed

    where
    module U = Semigroup U

    module F1 = SemigroupMorphism F1
    module F2 = SemigroupMorphism F2
    module G1 = SemigroupMorphism G1
    module G2 = SemigroupMorphism G2

  assoc :
    ∀ {S T U V}
      (F : SemigroupMorphism U V)
      (G : SemigroupMorphism T U)
      (H : SemigroupMorphism S T)
    → (F ∘ G) ∘ H ≈ F ∘ (G ∘ H)
  assoc {V = V} _ _ _ _ = V.refl
    where
    module V = Semigroup V

  id : ∀ {S} → SemigroupMorphism S S
  id {S} =
    record {
      map = λ x → x;
      map-cong = λ x → x;
      ⋄-preserving = λ _ _ → Semigroup.refl S
    }

  left-right-id :
    ∀ {S T}
      (F : SemigroupMorphism S T)
    → F ≈ F
  left-right-id {T = T} _ _ = T.refl
    where
    module T = Semigroup T

module Semigroups {a r} = Category (Semigroups {a} {r})

-- Product semigroups

_×S_ : ∀ {sa sr ta tr} → Semigroup {sa} {sr} → Semigroup {ta} {tr} → Semigroup
S ×S T =
  record {
    A = S.A × T.A;
    Eq = record {
      _≈_ = λ { (x1 , x2) (y1 , y2) → (x1 S.≈ y1) × (x2 T.≈ y2) };
      refl = S.refl , T.refl;
      sym = λ { (p1 , p2) → S.sym p1 , T.sym p2 };
      trans = λ { (p1 , p2) (q1 , q2) → S.trans p1 q1 , T.trans p2 q2 }
    };
    semigroupOver = record {
      _⋄_ = λ { (x1 , x2) (y1 , y2) → (x1 S.⋄ y1) , (x2 T.⋄ y2) };
      ⋄-cong = λ { (p1 , p2) (q1 , q2) → S.⋄-cong p1 q1 , T.⋄-cong p2 q2 };
      assoc = λ { (x1 , x2) (y1 , y2) (z1 , z2) → S.assoc x1 y1 z1 , T.assoc x2 y2 z2 }
    }
  }

  where
  module S = Semigroup S
  module T = Semigroup T

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module Categories.Sets where

open import Library
open import Categories

Sets : ∀{l} → Cat
Sets {l} = record{
  Obj  = Set l;
  Hom  = λ X Y → X → Y;
  iden = id;
  comp = λ f g → f ∘ g;
  idl  = refl;
  idr  = refl;
  ass  = refl}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --type-in-type #-}
module Nested where

record Σ₁ (A : Set)(B : A → Set) : Set where
  constructor _,_
  field fst : A
        snd : B fst

infixr 2 _,_
record Σ (A : Set)(B : A → Set) : Set where
  field p : Σ₁ A B
  open Σ₁ p public

open Σ

data ⊤ : Set where
  tt : ⊤

∃ : {A : Set}(B : A → Set) → Set
∃ B = Σ _ B

infix 10 _≡_

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

Cat : Set
Cat =
  ∃ λ (Obj : Set) →
  ∃ λ (Hom : Obj → Obj → Set) →
  ∃ λ (id : ∀ X → Hom X X) →
  ∃ λ (_○_ : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z) →
  ∃ λ (idl : ∀ {X Y}{f : Hom X Y} → id Y ○ f ≡ f) →
  ∃ λ (idr : ∀ {X Y}{f : Hom X Y} → f ○ id X ≡ f) →
  ∃ λ (assoc : ∀ {W X Y Z}{f : Hom W X}{g : Hom X Y}{h : Hom Y Z} →
                (h ○ g) ○ f ≡ h ○ (g ○ f)) →
  ⊤

Obj : (C : Cat) → Set
Obj C = fst C

Hom : (C : Cat) → Obj C → Obj C → Set
Hom C = fst (snd C)

id : (C : Cat) → ∀ X → Hom C X X
id C = fst (snd (snd C))

comp : (C : Cat) → ∀ {X Y Z} → Hom C Y Z → Hom C X Y → Hom C X Z
comp C = fst (snd (snd (snd C)))

idl : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C (id C Y) f ≡ f
idl C = fst (snd (snd (snd (snd C))))

idr : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C f (id C X) ≡ f
idr C = fst (snd (snd (snd (snd (snd C)))))

assoc : (C : Cat) → ∀ {W X Y Z}{f : Hom C W X}{g : Hom C X Y}{h : Hom C Y Z} →
        comp C (comp C h g) f ≡ comp C h (comp C g f)
assoc C = fst (snd (snd (snd (snd (snd (snd C))))))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2018-10-29, issue #3246

-- More things are now allowed in mutual blocks.

-- @mutual@ just pushes the definition parts to the bottom.
-- Definitions exist for data, record, functions, and pattern synonyms.

{-# BUILTIN FLOAT Float #-}  -- not (yet) allowed in mutual block

mutual

  import Agda.Builtin.Bool
  open Agda.Builtin.Bool

  f : Bool
  f = g   -- pushed to bottom

  -- module M where  -- not (yet) allowed in mutual block

  module B = Agda.Builtin.Bool

  primitive
    primFloatEquality : Float → Float → Bool

  {-# INJECTIVE primFloatEquality #-}  -- certainly a lie

  open import Agda.Builtin.Equality
  {-# DISPLAY primFloatEquality x y = x ≡ y #-}

  postulate A : Set
  {-# COMPILE GHC A = type Integer #-}

  variable x : Bool

  g : Bool
  g = true  -- pushed to bottom

  {-# STATIC g #-}

  record R : Set where
    coinductive
    field foo : R

  {-# ETA R #-}

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
module Oscar.Property.Equivalence where

open import Oscar.Function
open import Oscar.Level
open import Oscar.Property.Reflexivity
open import Oscar.Property.Symmetry
open import Oscar.Property.Transitivity

record Equivalence {𝔬} {⋆ : Set 𝔬} {𝔮} (_≋_ : ⋆ → ⋆ → Set 𝔮) : Set (𝔬 ⊔ 𝔮) where
  field
    ⦃ ′reflexivity ⦄ : Reflexivity _≋_
    ⦃ ′symmetry ⦄ : Symmetry _≋_
    ⦃ ′transitivity ⦄ : Transitivity _≋_

open Equivalence ⦃ … ⦄ public

instance
  Equivalence⋆ : ∀
    {𝔬} {⋆ : Set 𝔬} {𝔮} {_≋_ : ⋆ → ⋆ → Set 𝔮}
    ⦃ _ : Reflexivity _≋_ ⦄
    ⦃ _ : Symmetry _≋_ ⦄
    ⦃ _ : Transitivity _≋_ ⦄
    → Equivalence _≋_
  Equivalence.′reflexivity Equivalence⋆ = it
  Equivalence.′symmetry Equivalence⋆ = it
  Equivalence.′transitivity Equivalence⋆ = it


text:
module Chunk where

open import Codata.Stream using (chunksOf; iterate; take)
open import Data.Nat using (ℕ; suc)
open import Data.Vec using (Vec; []; _∷_)

-- mylist 3 = [[1,2,3],[4,5,6],[7,8,9]]
myVec : (n : ℕ) → Vec (Vec ℕ n) n
myVec n = take n (chunksOf n (iterate suc 1))


text:
open import Prelude

module Implicits.Resolution.Finite.Decidable where

open import Coinduction
open import Data.Fin.Substitution
open import Data.List.Any
open Membership-≡
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.Finite.Resolution
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Equality hiding (cong)
open import Data.List.Any.Properties using (Any↔)

module M = MetaTypeMetaSubst

mutual
  {-# NO_TERMINATION_CHECK #-}
  match' : ∀ {m ν} (Δ : ICtx ν) s r∈Δ τ → (r : MetaType m ν) →
          Dec (∃ λ u → Δ & s , r∈Δ ⊢ from-meta (r M./ u) ↓ τ)
  match' Δ s r∈Δ τ (simpl x) with mgu (simpl x) τ
  match' Δ s r∈Δ τ (simpl x) | just (u , p) =
    yes (
      (asub u) ,
      subst (λ a → Δ & s , r∈Δ  ⊢ a ↓ τ) (sym $ mgu-unifies (simpl x) τ (u , p)) (i-simp τ)
    )
  match' Δ s r∈Δ τ (simpl x) | nothing = no (λ{ (proj₁ , proj₂) → {!!} })

  match' Δ s r∈Δ τ (a ⇒ b) with match' Δ s r∈Δ τ b
  match' Δ s r∈Δ τ (a ⇒ b) | no ¬p = no {!!}
  match' Δ s r∈Δ τ (a ⇒ b) | yes (u , b/u↓τ) with
    all (λ x → (r∈Δ , (from-meta (a M./ u))) ?⊬dom x) s
  match' Δ s r∈Δ τ (a ⇒ b) | yes (u , b/u↓τ) | yes p
    -- The following with clause fails to satisfy termination checking
    with let a' = from-meta (a M./ u) in resolve' Δ ((r∈Δ , a') List.∷ s) a'
  match' Δ s r∈Δ τ (a ⇒ b) | yes (u , b/u↓τ) | yes p | yes ⊢ᵣa = yes (u , i-iabs p ⊢ᵣa b/u↓τ)
  match' Δ s r∈Δ τ (a ⇒ b) | yes (u , b/u↓τ) | yes p | no ¬⊢ᵣa =
    no (λ{ (u' , i-iabs x ⊢ᵣa a⇒b↓τ) → {!¬⊢ᵣa ⊢ᵣa!} })
  match' Δ s r∈Δ τ (a ⇒ b) | yes (u , b/u↓τ) | no ¬p = no {!!}

  -- The following with clause fails to satisfy termination checking
  match' Δ s r∈Δ τ (∀' a) with match' Δ s r∈Δ τ (open-meta a)
  match' Δ s r∈Δ τ (∀' a) | yes p = yes $ lem p
    where
      lem : (∃ λ u → Δ & s , r∈Δ ⊢ (from-meta ((open-meta a) M./ u)) ↓ τ) →
          ∃ λ u' → Δ & s , r∈Δ ⊢ (from-meta (∀' a M./ u')) ↓ τ
      lem (u ∷ us , p) = us , (i-tabs (from-meta u) (subst (λ v → Δ & s , r∈Δ ⊢ v ↓ τ) (begin
            from-meta (M._/_ (open-meta a) (u ∷ us))
              ≡⟨ cong (λ v → from-meta (M._/_ (open-meta a) v)) (sym $ us↑-⊙-sub-u≡u∷us u us) ⟩
            from-meta ((open-meta a) M./ (us M.↑ M.⊙ (M.sub u)))
              ≡⟨ cong from-meta (/-⊙ (open-meta a)) ⟩
            from-meta ((open-meta a) M./ us M.↑ M./ (M.sub u))
              ≡⟨ lem' a u us ⟩
            from-meta (M._/_ a (us M.↑tp)) tp[/tp from-meta u ] ∎) p))
          where open MetaTypeMetaLemmas hiding (subst)
  match' Δ s r∈Δ τ (∀' r) | no ¬p = no {!!}

  -- match defers to match', which concerns itself with MetaTypes.
  -- If match' finds a match, we can use the fact that we have zero unification variables open here
  -- to show that we found the right thing.
  match : ∀ {ν} (Δ : ICtx ν) s r∈Δ → ∀ r τ → Dec (Δ & s , r∈Δ ⊢ r ↓ τ)
  match Δ s r∈Δ a τ with match' Δ s r∈Δ τ (to-meta {zero} a)
  match Δ s r∈Δ a τ | yes x = yes (lem x)
    where
      eq : ∀ {ν} {a : Type ν} {s} → from-meta (to-meta {zero} a M./ s) ≡ a
      eq {a = a} {s = []} = begin
          from-meta (M._/_ (to-meta {zero} a) [])
          ≡⟨ cong (λ q → from-meta q) (MetaTypeMetaLemmas.id-vanishes (to-meta {zero} a)) ⟩
          from-meta (to-meta {zero} a)
          ≡⟨ to-meta-zero-vanishes ⟩
          a ∎
      lem : ∃ (λ u → Δ & s , r∈Δ ⊢ from-meta (to-meta {zero} a M./ u) ↓ τ) →
                Δ & s , r∈Δ ⊢ a ↓ τ
      lem ([] , proj₂) = subst (λ u → Δ & s , r∈Δ ⊢ u ↓ τ) eq proj₂
  match Δ s r∈Δ a τ | no ¬p = no {!!}

  match1st : ∀ {ν} (Δ : ICtx ν) s τ  → Dec (Any (λ r → Δ & s , r ⊢ r ↓ τ) Δ)
  match1st Δ s τ = match1st' Δ Δ s τ -- any (λ r → match Δ r τ)
    where
      match1st' : ∀ {ν} (Δ ρs : ICtx ν) s → (τ : SimpleType ν) →
                  Dec (Any (λ r → Δ & s , r ⊢ r ↓ τ) ρs)
      match1st' Δ List.[] s τ = no {!!}
      match1st' Δ (x List.∷ xs) s τ with match Δ s x x τ
      match1st' Δ (x List.∷ xs) s τ | yes px = yes (here px)
      match1st' Δ (x List.∷ xs) s τ | no ¬p with match1st' Δ xs s τ
      match1st' Δ (x List.∷ xs) s τ | no ¬p | yes y = yes (there y)
      match1st' Δ (x List.∷ xs) s τ | no ¬p | no ¬q = no {!!}

  resolve' : ∀ {ν} (Δ : ICtx ν) s r → (Dec (Δ & s ⊢ᵣ r))
  resolve' Δ s (simpl x) with match1st Δ s x
  resolve' Δ s (simpl x) | yes p =
    let r , r∈Δ , r↓x = (Inverse.from Any↔) Π.⟨$⟩ p in yes (r-simp r∈Δ r↓x)
  resolve' Δ s (simpl x) | no ¬p =
    no (λ{ (r-simp x₁ x₂) → ¬p (_⟨$⟩_ (Inverse.to Any↔) (_ , (x₁ , x₂))) })
  resolve' Δ s (a ⇒ b) with resolve' (a List.∷ Δ) s b
  resolve' Δ s (a ⇒ b) | yes p = yes (r-iabs p)
  resolve' Δ s (a ⇒ b) | no ¬p = no (λ{ (r-iabs x) → ¬p x })
  resolve' Δ s (∀' r) with resolve' (ictx-weaken Δ) (stack-weaken s) r
  resolve' Δ s (∀' r) | yes p = yes (r-tabs p)
  resolve' Δ s (∀' r) | no ¬p = no λ{ (r-tabs x) → ¬p x }

  resolve : ∀ {ν} (Δ : ICtx ν) r → (Dec (Δ & List.[] ⊢ᵣ r))
  resolve Δ r = resolve' Δ List.[] r


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

-- {-# OPTIONS -v rewriting:100 #-}

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i

{-# BUILTIN REWRITE _↦_ #-}

postulate
  Unit : Set
  tt : Unit

module _ {i} (P : Unit → Set i) (tt* : P tt) where

  postulate
    Unit-elim : (x : Unit) → P x
    Unit-β : Unit-elim tt ↦ tt*
  {-# REWRITE Unit-β #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Numeral.Sign.Oper0 where

open import Numeral.Sign

-- Negation
−_ : (+|0|−) → (+|0|−)
− (➕) = (➖)
− (𝟎) = (𝟎)
− (➖) = (➕)

-- Bounded addition
_+_ : (+|0|−) → (+|0|−) → (+|0|−)
(➕) + (➕) = (➕)
(➕) + (➖) = (𝟎)
(➕) + (𝟎) = (➕)
(➖) + (➕) = (𝟎)
(➖) + (➖) = (➖)
(➖) + (𝟎) = (➖)
(𝟎) + (➕) = (➕)
(𝟎) + (➖) = (➖)
(𝟎) + (𝟎) = (𝟎)

-- Multiplication
_⨯_ : (+|0|−) → (+|0|−) → (+|0|−)
(➕) ⨯ (➕) = (➕)
(➕) ⨯ (➖) = (➖)
(➕) ⨯ (𝟎) = (𝟎)
(➖) ⨯ (➕) = (➖)
(➖) ⨯ (➖) = (➕)
(➖) ⨯ (𝟎) = (𝟎)
(𝟎) ⨯ (➕) = (𝟎)
(𝟎) ⨯ (➖) = (𝟎)
(𝟎) ⨯ (𝟎) = (𝟎)

_⋚_ : (+|0|−) → (+|0|−) → (+|0|−)
➕ ⋚ 𝟎 = ➕
➕ ⋚ ➖ = ➕
𝟎 ⋚ ➖ = ➕
➕ ⋚ ➕ = 𝟎
𝟎 ⋚ 𝟎 = 𝟎
➖ ⋚ ➖ = 𝟎
𝟎 ⋚ ➕ = ➖
➖ ⋚ ➕ = ➖
➖ ⋚ 𝟎 = ➖

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module n2o.Network.Core where

open import proto.Base
open import proto.IO

open import n2o.Network.Internal

{-# FOREIGN GHC import Network.N2O.Core #-}

postulate
    protoRun : ∀ {F : Set → Set} {A : Set} → F A → List (Proto F A) → N2O F A (Result (F A))

{-# COMPILE GHC protoRun = Network.N2O.Core.protoRun #-}


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

module Data.PolyP.Composition where

open import Function hiding (_⟨_⟩_)
open import Data.Sum
open import Data.Sigma
open import Level
open import Data.Unit
open import Data.Nat
open import Data.Vec
open import Data.Empty
open import WellFounded
open import Literals.Number
open import Data.Fin.Indexed.Literals
open import Data.Fin.Indexed.Properties
open import Data.Fin.Indexed
open import Data.Nat.Literals
open import Data.Maybe

open import Data.PolyP.Universe

infixr 9 _⊚_

_⇑_ : Fin (suc n) → Functor n → Functor (suc n)
i ⇑ (! j) = ! (insert i j)
i ⇑ (x ⊕ y) = i ⇑ x ⊕ i ⇑ y
i ⇑ (x ⊗ y) = i ⇑ x ⊗ i ⇑ y
i ⇑ μ⟨ x ⟩ = μ⟨ fs i ⇑ x ⟩
i ⇑ ⓪ = ⓪
i ⇑ ① = ①

⇓ : Functor n → Functor (suc n)
⇓ (! x) = ! (weaken x)
⇓ (x ⊕ y) = ⇓ x ⊕ ⇓ y
⇓ (x ⊗ y) = ⇓ x ⊗ ⇓ y
⇓ μ⟨ x ⟩ = μ⟨ f0 ⇑ x ⟩
⇓ ⓪ = ⓪
⇓ ① = ①

substAt : Fin (suc n) → Functor (suc n) → Functor n → Functor n
substAt i (! j)     xs = maybe xs ! (j \\ i)
substAt i (ys ⊕ zs) xs = substAt i ys xs ⊕ substAt i zs xs
substAt i (ys ⊗ zs) xs = substAt i ys xs ⊗ substAt i zs xs
substAt i μ⟨ ys ⟩   xs = μ⟨ substAt (fs i) ys (f0 ⇑ xs) ⟩
substAt i ⓪         xs = ⓪
substAt i ①         xs = ①

_⊚_ : Functor (suc n) → Functor n → Functor n
_⊚_ = substAt f0

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Data.Binary.Multiplication.Properties where

open import Prelude
open import Data.Binary.Definition
open import Data.Binary.Addition
open import Data.Binary.Addition.Properties using (+-cong)
open import Data.Binary.Multiplication
open import Data.Binary.Conversion
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Path.Reasoning
open import Data.Binary.Isomorphism

double-cong : ∀ xs → ⟦ double xs ⇓⟧ ≡ ⟦ xs ⇓⟧ ℕ.* 2
double-cong 0ᵇ i = zero
double-cong (1ᵇ xs) i = 2 ℕ.+ double-cong xs i ℕ.* 2
double-cong (2ᵇ xs) i = ⟦ 2ᵇ 1ᵇ xs ⇓⟧

double-plus : ∀ x → x ℕ.+ x ≡ x ℕ.* 2
double-plus x = cong (x ℕ.+_) (sym (ℕ.+-idʳ x)) ; ℕ.*-comm 2 x

lemma₁ : ∀ x y → x ℕ.* y ℕ.* 2 ≡ y ℕ.* 2 ℕ.* x
lemma₁ x y =
  x ℕ.* y ℕ.* 2 ≡⟨ ℕ.*-assoc x y 2 ⟩
  x ℕ.* (y ℕ.* 2) ≡⟨ ℕ.*-comm x (y ℕ.* 2) ⟩
  y ℕ.* 2 ℕ.* x ∎

lemma₂ : ∀ x y → (x ℕ.+ x ℕ.* y) ℕ.* 2 ≡ x ℕ.+ (x ℕ.+ y ℕ.* 2 ℕ.* x)
lemma₂ x y =
  (x ℕ.+ x ℕ.* y) ℕ.* 2 ≡⟨ ℕ.+-*-distrib x (x ℕ.* y) 2 ⟩
  x ℕ.* 2 ℕ.+ x ℕ.* y ℕ.* 2 ≡⟨ cong₂ ℕ._+_ (sym (double-plus x)) (lemma₁ x y) ⟩
  x ℕ.+ x ℕ.+ y ℕ.* 2 ℕ.* x ≡⟨ ℕ.+-assoc x x (y ℕ.* 2 ℕ.* x) ⟩
  x ℕ.+ (x ℕ.+ y ℕ.* 2 ℕ.* x) ∎

*-cong : ∀ xs ys → ⟦ xs * ys ⇓⟧ ≡ ⟦ xs ⇓⟧ ℕ.* ⟦ ys ⇓⟧
*-cong 0ᵇ ys = refl
*-cong (1ᵇ xs) ys =
  ⟦ ys + double (ys * xs) ⇓⟧ ≡⟨ +-cong ys (double (ys * xs)) ⟩
  ⟦ ys ⇓⟧  ℕ.+ ⟦ double (ys * xs) ⇓⟧ ≡⟨ cong (⟦ ys ⇓⟧ ℕ.+_)  (double-cong (ys * xs)) ⟩
  ⟦ ys ⇓⟧  ℕ.+ ⟦ ys * xs ⇓⟧ ℕ.* 2 ≡⟨ cong (⟦ ys ⇓⟧ ℕ.+_)  (cong (ℕ._* 2) (*-cong ys xs)) ⟩
  ⟦ ys ⇓⟧  ℕ.+ ⟦ ys ⇓⟧ ℕ.* ⟦ xs ⇓⟧ ℕ.* 2 ≡⟨ cong (⟦ ys ⇓⟧ ℕ.+_) (lemma₁ ⟦ ys ⇓⟧ ⟦ xs ⇓⟧) ⟩
  ⟦ ys ⇓⟧ ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2 ℕ.* ⟦ ys ⇓⟧ ∎
*-cong (2ᵇ xs) ys =
  ⟦ double (ys + ys * xs) ⇓⟧ ≡⟨ double-cong (ys + ys * xs) ⟩
  ⟦ ys + ys * xs ⇓⟧ ℕ.* 2 ≡⟨ cong (ℕ._* 2) (+-cong ys (ys * xs)) ⟩
  (⟦ ys ⇓⟧ ℕ.+ ⟦ ys * xs ⇓⟧) ℕ.* 2 ≡⟨ cong (ℕ._* 2) (cong (⟦ ys ⇓⟧ ℕ.+_) (*-cong ys xs)) ⟩
  (⟦ ys ⇓⟧ ℕ.+ ⟦ ys ⇓⟧ ℕ.* ⟦ xs ⇓⟧) ℕ.* 2 ≡⟨ lemma₂ ⟦ ys ⇓⟧ ⟦ xs ⇓⟧  ⟩
  ⟦ ys ⇓⟧ ℕ.+ (⟦ ys ⇓⟧ ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2 ℕ.* ⟦ ys ⇓⟧) ∎


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.Subspace
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Logic
open import Logic.Predicate
open import Logic.Predicate.Equiv
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Container.SetLike using (SetElement)
private open module SetLikeFunctionProperties{ℓ} = Structure.Container.SetLike.FunctionProperties{C = PredSet{ℓ}(V)}(_∈_)
open import Structure.Operator.Vector
open import Structure.Operator.Vector.LinearCombination ⦃ vectorSpace = vectorSpace ⦄
open import Syntax.Transitivity

private variable ℓ : Lvl.Level

-- A subspace is a subset of V such that it is a vector space under the same operators.
record Subspace (Vₛ : PredSet{ℓ}(V)) : Stmt{ℓᵥ Lvl.⊔ ℓₛ Lvl.⊔ ℓ} where
  constructor intro
  field
    ⦃ add-closure ⦄ : Vₛ closed-under₂ (_+ᵥ_)
    ⦃ mul-closure ⦄ : ∀{s} → (Vₛ closed-under₁ (s ⋅ₛᵥ_))

  _+_ : SetElement(_∈_)(Vₛ) → SetElement(_∈_)(Vₛ) → SetElement(_∈_)(Vₛ)
  _+_ = [∃]-map₂(_+ᵥ_) (Vₛ closureUnder₂ (_+ᵥ_))

  _⋅_ : S → SetElement(_∈_)(Vₛ) → SetElement(_∈_)(Vₛ)
  _⋅_ s = [∃]-map(s ⋅ₛᵥ_) (Vₛ closureUnder₁ (s ⋅ₛᵥ_))

  -- TODO: A proof of this would be easier if a similar "substructure" relation was defined on groups and fields, but I am not sure if using PredSet is the correct choice (maybe this is unprovable when using this?). Another alternative is to use a general set structure by Structure.Container.SetLike
  postulate is-vectorSpace : VectorSpace{V = SetElement(_∈_)(Vₛ)}{S = S}(_+_)(_⋅_)(_+ₛ_)(_⋅ₛ_)
  -- is-vectorSpace = {!!}

SubspaceObject : ∀{ℓ} → Stmt
SubspaceObject{ℓ} = ∃(Subspace{ℓ})


text:
module plfa-code.Relations where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym; trans)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-comm)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_)

open import plfa-code.Reasoning-legacy
open import Function

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ}
      ---------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      --------------
    → suc m ≤ suc n

infix 4 _≤_

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
     -------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    ---------
  → m ≡ zero
inv-z≤n z≤n = refl

≤-refl : ∀ {n : ℕ}
    ------
  → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    ------
  → m ≤ p
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

≤-trans′ : ∀ (m n p : ℕ)
  → m ≤ n
  → n ≤ p
    ------
  → m ≤ p
≤-trans′ zero    _       _       z≤n       _          =  z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans′ m n p m≤n n≤p)

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -------
  → m ≡ n
≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

-- when m is zero there is no instance for `n ≤ m`, the same as when n is zero

data Total (m n : ℕ) : Set where
  forward :
      m ≤ n
      ----------
    → Total m n

  flipped :
      n ≤ m
      ----------
    → Total m n

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero n = forward z≤n
≤-total (suc m) zero = flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n = forward (s≤s m≤n)
...                        | flipped n≤m = flipped (s≤s n≤m)

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n        =  forward z≤n
≤-total′ (suc m) zero     =  flipped z≤n
≤-total′ (suc m) (suc n)  =  helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n)  =  forward (s≤s m≤n)
  helper (flipped n≤m)  =  flipped (s≤s n≤m)

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    --------------
  → n + p ≤ n + q
+-monoʳ-≤ zero p q p≤q = p≤q
+-monoʳ-≤ (suc n) p q p≤q = s≤s (+-monoʳ-≤ n p q p≤q)

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    --------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n rewrite +-comm m p | +-comm n p = +-monoʳ-≤ p m n m≤n

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    --------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q = ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

---------- practice ----------
*-mono-≤ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m * p ≤ n * q
*-mono-≤ zero n p q m≤n p≤q = z≤n
*-mono-≤ (suc m) (suc n) p q m≤n p≤q = +-mono-≤ p q (m * p) (n * q) p≤q (*-mono-≤ m n p q (inv-s≤s m≤n) p≤q)
------------------------------

infix 4 _<_

data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {n : ℕ}
      -------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      --------------
    → suc m < suc n

---------- practice ----------
inv-s<s : ∀ {m n : ℕ} → suc m < suc n → m < n
inv-s<s (s<s mLTn) = mLTn

<-trans : ∀ (m n p : ℕ) → m < n → n < p → m < p
<-trans zero (suc n) (suc p) zLTsn snLTsp = z<s
<-trans (suc m) (suc n) (suc p) smLTsn snLTsp = s<s (<-trans m n p (inv-s<s smLTsn) (inv-s<s snLTsp))

data Trichotomy (m n : ℕ) : Set where
  less    : m < n → Trichotomy m n
  equal   : m ≡ n → Trichotomy m n
  greater : n < m → Trichotomy m n

<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n
<-trichotomy zero    zero     = equal refl
<-trichotomy zero    (suc n)  = less z<s
<-trichotomy (suc m) zero     = greater z<s
<-trichotomy (suc m) (suc n) with <-trichotomy m n
...                             | less    mLTn = less (s<s mLTn)
...                             | equal   refl = equal refl
...                             | greater nLTm = greater (s<s nLTm)

+-monoʳ-< : ∀ (n p q : ℕ) → p < q → n + p < n + q
+-monoʳ-< zero p q pLTq = pLTq
+-monoʳ-< (suc n) p q pLTq = s<s (+-monoʳ-< n p q pLTq)

+-monoˡ-< : ∀ (m n p : ℕ) → m < n → m + p < n + p
+-monoˡ-< m n p mLTn rewrite +-comm m p | +-comm n p = +-monoʳ-< p m n mLTn

+-mono-< : ∀ (m n p q : ℕ) → m < n → p < q → m + p < n + q
+-mono-< m n p q mLTn pLTq = <-trans (m + p) (n + p) (n + q) (+-monoˡ-< m n p mLTn) (+-monoʳ-< n p q pLTq)

≤-iff-< : ∀ (m n : ℕ) → suc m ≤ n → m < n
≤-iff-< zero    (suc n) _       = z<s
≤-iff-< (suc m) (suc n) ssm≤sn = s<s (≤-iff-< m n sm≤n)
  where
  sm≤n = inv-s≤s ssm≤sn

<-iff-≤ : ∀ (m n : ℕ) → m < n → suc m ≤ n
<-iff-≤ zero (suc n) mLTn = s≤s z≤n
<-iff-≤ (suc m) (suc n) smLTn = s≤s (<-iff-≤ m n (inv-s<s smLTn))

<→≤ : ∀ (n p : ℕ) → n < p → n ≤ p
<→≤ zero p nLTp = z≤n
<→≤ (suc n) (suc p) nLTp = s≤s (<→≤ n p (inv-s<s nLTp))

<-trans-revisited : ∀ (m n p : ℕ) → m < n → n < p → m < p
<-trans-revisited m n p mLTn nLTp = ≤-iff-< m p (inv-s≤s ssm≤sp)
  where ssm≤sp = s≤s (≤-trans (<-iff-≤ m n mLTn) (<→≤ n p nLTp))
------------------------------

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      -------------
    → even (suc n)

data odd where

  suc   : ∀ {n : ℕ}
    → even n
      ------------
    → odd (suc n)

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    -------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    ------------
  → odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

---------- practice ----------
o+o≡e : ∀ {m n : ℕ} → odd m → odd n → even (m + n)
o+o≡e (suc zero)     on = suc on
o+o≡e (suc (suc ox)) on = suc (suc (o+o≡e ox on))

open import plfa-code.Induction using (Bin; nil; x0_; x1_; inc; from; to;
                                      +1≡suc; suc-from-inc; from-to-const)

data Can : Bin → Set
data One : Bin → Set

data One where
  one  : One (x1 nil)
  x0_ : ∀ {b : Bin} → One b → One(x0 b)
  x1_ : ∀ {b : Bin} → One b → One(x1 b)

data Can where
  zero     : Can (x0 nil)
  can-one  : ∀ {b : Bin} → One b → Can b

one-inc : ∀ {x : Bin} → One x → One (inc x)
one-inc one = x0 one
one-inc (x0 x) = x1 x
one-inc (x1 x) = x0 (one-inc x)

can-inc : ∀ {x : Bin} → Can x → Can (inc x)
can-inc zero        =  can-one one
can-inc (can-one x) =  can-one (one-inc x)

one-to-n : ∀ (n : ℕ) → One (to (suc n))
one-to-n zero = one
one-to-n (suc n) = one-inc (one-to-n n)

can-to-n : ∀ (n : ℕ) → Can (to n)
can-to-n zero = zero
can-to-n (suc n) = can-one (one-to-n n)

open Data.Nat.Properties using (+-identityʳ; +-suc)

l0 : ∀ (n) → to (suc n) ≡ inc (to n)
l0 zero    = refl
l0 (suc n) = refl

2n-eq-x0 : ∀ (n) → 1 ≤ n → to (n + n) ≡ x0 (to n)
2n-eq-x0 zero ()
2n-eq-x0 (suc zero) (s≤s z≤n) = refl
2n-eq-x0 (suc (suc n)) (s≤s z≤n) =
  begin to (suc (suc n) + suc (suc n))
  ≡⟨ cong (λ x → to x) (+-suc (suc (suc n)) (suc n)) ⟩  to (suc (suc (suc n + suc n)))
  ≡⟨⟩  inc (inc (to (suc n + suc n)))
  ≡⟨ cong (λ x → (inc (inc x))) (2n-eq-x0 (suc n) (s≤s z≤n)) ⟩  inc (inc (x0 (to (suc n))))
  ≡⟨⟩  x0 (inc (to (suc n)))
  ≡⟨⟩  x0 (to (suc (suc n)))
  ∎

one-b-iff-1≤b : ∀ (b) → One b → 1 ≤ from b
one-b-iff-1≤b (x0 b) (x0 ob)
              rewrite +-identityʳ (from b)
              = +-mono-≤ 1 n 0 n (one-b-iff-1≤b b ob) z≤n
                where n = from b
one-b-iff-1≤b (x1 .nil) one     = s≤s z≤n
one-b-iff-1≤b (x1 b)    (x1 ob) = s≤s z≤n

one-tf-eq : ∀ {b} → One b → to (from b) ≡ b
one-tf-eq {_}    one    = refl
one-tf-eq {x0 b} (x0 x) =
  begin
    to (from (x0 b))
  ≡⟨⟩
    to (from b + (from b + zero))
  ≡⟨ cong (λ n → to (from b + n)) (+-identityʳ (from b)) ⟩
    to (from b + from b)
  ≡⟨ 2n-eq-x0 (from b) (one-b-iff-1≤b b x) ⟩
    x0 (to (from b))
  ≡⟨ cong x0_ (one-tf-eq x) ⟩
    x0 b
  ∎
one-tf-eq {x1 b} (x1 x) =
  begin
    to (from (x1 b))
  ≡⟨⟩
    inc (to (from b + (from b + zero)))
  ≡⟨ cong (λ n → inc (to (from b + n))) (+-identityʳ (from b)) ⟩
    inc (to (from b + from b))
  ≡⟨ cong inc (2n-eq-x0 (from b) (one-b-iff-1≤b b x)) ⟩
    inc (x0 (to (from b)))
  ≡⟨⟩
    x1 (to (from b))
  ≡⟨ cong x1_ (one-tf-eq x) ⟩
    x1 b
  ∎

can-tf-eq : ∀ {x} → Can x → to (from x) ≡ x
can-tf-eq {_}  zero        = refl
can-tf-eq {b}  (can-one x) = one-tf-eq x

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

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
------------------------------------------------------------------------
-- Pointwise equalities can be lifted
------------------------------------------------------------------------

module Stream.Pointwise where

open import Codata.Musical.Notation hiding (∞)
open import Stream
open import Stream.Equality
import Stream.Programs as Prog
open Prog hiding (lift; ⟦_⟧)
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec as Vec using (Vec; _∷_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
private
  module IsEq {A : Set} =
    IsEquivalence (Setoid.isEquivalence (Stream.setoid A))

------------------------------------------------------------------------
-- Definitions

infix  8 _∞
infixr 7 _·_
infix  6 _⟨_⟩_

-- Expressions corresponding to pointwise definitions of streams.
-- Indexed on the number of variables.

-- It is possible to generalise this type, allowing variables to
-- correspond to streams containing elements of arbitrary type, and
-- letting the function arguments of _·_ and _⟨_⟩_ be more general.
-- However, this would complicate the development, so I hesitate to do
-- so without evidence that it would be genuinely useful.

data Pointwise A n : Set where
  var   : (x : Fin n) → Pointwise A n
  _∞    : (x : A) → Pointwise A n
  _·_   : (f : A → A) (xs : Pointwise A n) → Pointwise A n
  _⟨_⟩_ : (xs : Pointwise A n)
          (_∙_ : A → A → A)
          (ys : Pointwise A n) →
          Pointwise A n

-- Stream semantics.

⟦_⟧ : ∀ {A n} → Pointwise A n → (Vec (Prog A) n → Prog A)
⟦ var x ⟧         ρ = Vec.lookup ρ x
⟦ x ∞ ⟧           ρ = x ∞
⟦ f · xs ⟧        ρ = f · ⟦ xs ⟧ ρ
⟦ xs ⟨ _∙_ ⟩ ys ⟧ ρ = ⟦ xs ⟧ ρ ⟨ _∙_ ⟩ ⟦ ys ⟧ ρ

-- Pointwise semantics.

⟪_⟫ : ∀ {A n} → Pointwise A n → (Vec A n → A)
⟪ var x ⟫         ρ = Vec.lookup ρ x
⟪ x ∞ ⟫           ρ = x
⟪ f · xs ⟫        ρ = f (⟪ xs ⟫ ρ)
⟪ xs ⟨ _∙_ ⟩ ys ⟫ ρ = ⟪ xs ⟫ ρ ∙ ⟪ ys ⟫ ρ

------------------------------------------------------------------------
-- Some lemmas used below

private

  -- lookup is natural.

  lookup-nat : ∀ {a b n} {A : Set a} {B : Set b}
               (f : A → B) (x : Fin n) ρ →
               f (Vec.lookup ρ x) ≡ Vec.lookup (Vec.map f ρ) x
  lookup-nat f zero    (x ∷ ρ) = refl
  lookup-nat f (suc i) (x ∷ ρ) = lookup-nat f i ρ

------------------------------------------------------------------------
-- The two semantics above are related via the function lift

private

  -- Lifts a pointwise function to a function on stream programs.

  lift : ∀ {A B n} →
         (Vec A n → B) → Vec (Prog A) n → Prog B
  lift f xs = f (Vec.map headP xs) ≺ ♯ lift f (Vec.map tailP xs)

  -- lift is a congruence in its first argument.

  lift-cong : ∀ {A B n} {f g : Vec A n → B} →
              (∀ ρ → f ρ ≡ g ρ) →
              ∀ ρ → lift f ρ ≊ lift g ρ
  lift-cong hyp ρ = hyp (Vec.map headP ρ) ≺
                    ♯ lift-cong hyp (Vec.map tailP ρ)

  -- unfold xs ρ is the one-step unfolding of ⟦ xs ⟧ ρ. Note the
  -- similarity to lift.

  unfold : ∀ {A n} (xs : Pointwise A n) ρ → Prog A
  unfold xs ρ = ⟪ xs ⟫ (Vec.map headP ρ) ≺♯
                ⟦ xs ⟧ (Vec.map tailP ρ)

  unfold-lemma : ∀ {A n} (xs : Pointwise A n) ρ →
                 ⟦ xs ⟧ ρ ≊ unfold xs ρ
  unfold-lemma (var x) ρ =
    Vec.lookup ρ x
      ≊⟨ ≊-η (Vec.lookup ρ x) ⟩
    headP (Vec.lookup ρ x) ≺♯ tailP (Vec.lookup ρ x)
      ≊⟨ lookup-nat headP x ρ ≺
         ♯ ≈⇒≅ (IsEq.reflexive
                  (cong Prog.⟦_⟧ (lookup-nat tailP x ρ))) ⟩
    Vec.lookup (Vec.map headP ρ) x ≺♯
    Vec.lookup (Vec.map tailP ρ) x
      ≡⟨ refl ⟩
    unfold (var x) ρ
      ∎
  unfold-lemma (x ∞)    ρ = x ∞ ∎
  unfold-lemma (f · xs) ρ =
    f · ⟦ xs ⟧ ρ
      ≊⟨ ·-cong f (⟦ xs ⟧ ρ) (unfold xs ρ) (unfold-lemma xs ρ) ⟩
    f · unfold xs ρ
      ∎
  unfold-lemma (xs ⟨ ∙ ⟩ ys) ρ =
    ⟦ xs ⟧ ρ ⟨ ∙ ⟩ ⟦ ys ⟧ ρ
      ≊⟨ ⟨ ∙ ⟩-cong (⟦ xs ⟧ ρ) (unfold xs ρ) (unfold-lemma xs ρ)
                    (⟦ ys ⟧ ρ) (unfold ys ρ) (unfold-lemma ys ρ) ⟩
    unfold xs ρ ⟨ ∙ ⟩ unfold ys ρ
      ∎

  -- The two semantics are related.

  main-lemma : ∀ {A n} (xs : Pointwise A n) →
               ∀ ρ → ⟦ xs ⟧ ρ ≊ lift ⟪ xs ⟫ ρ
  main-lemma xs ρ =
    ⟦ xs ⟧ ρ
      ≊⟨ unfold-lemma xs ρ ⟩
    unfold xs ρ
      ≡⟨ refl ⟩
    ⟪ xs ⟫ (Vec.map headP ρ) ≺♯ ⟦ xs ⟧ (Vec.map tailP ρ)
      ≊⟨ refl ≺ ♯ main-lemma xs (Vec.map tailP ρ) ⟩
    lift ⟪ xs ⟫ ρ
      ∎

------------------------------------------------------------------------
-- To prove that two streams which are defined pointwise are equal, it
-- is enough to reason about a single (arbitrary) point

-- This function is a bit awkward to use, since the user has to come
-- up with a suitable environment manually. The alternative function
-- pointwise below may be slightly easier to use.

pointwise' : ∀ {A n} (xs ys : Pointwise A n) →
             (∀ ρ → ⟪ xs ⟫ ρ ≡ ⟪ ys ⟫ ρ) →
             (∀ ρ → ⟦ xs ⟧ ρ ≊ ⟦ ys ⟧ ρ)
pointwise' xs ys hyp ρ =
  ⟦ xs ⟧ ρ
    ≊⟨ main-lemma xs ρ ⟩
  lift ⟪ xs ⟫ ρ
    ≊⟨ lift-cong hyp ρ ⟩
  lift ⟪ ys ⟫ ρ
    ≊⟨ ≅-sym (main-lemma ys ρ) ⟩
  ⟦ ys ⟧ ρ
    ∎

open import Data.Vec.N-ary

-- Applies the function to all possible variables.

app : ∀ {A} n →
      N-ary n (Pointwise A n) (Pointwise A n) → Pointwise A n
app n f = f $ⁿ Vec.map var (Vec.allFin n)

-- The type signature of this function may be a bit daunting, but once
-- n, f and g are instantiated with well-behaved concrete values the
-- remaining type evaluates nicely.

pointwise
  : ∀ {A} n (f g : N-ary n (Pointwise A n) (Pointwise A n)) →
    Eq n _≡_ (curryⁿ ⟪ app n f ⟫) (curryⁿ ⟪ app n g ⟫) →
    Eq n _≊_ (curryⁿ ⟦ app n f ⟧) (curryⁿ ⟦ app n g ⟧)
pointwise n f g hyp =
  curryⁿ-cong _≊_ ⟦ app n f ⟧ ⟦ app n g ⟧
    (pointwise' (app n f) (app n g)
      (curryⁿ-cong⁻¹ _≡_ ⟪ app n f ⟫ ⟪ app n g ⟫ hyp))

------------------------------------------------------------------------
-- Some examples

private

  example₁ : suc · 0 ∞ ≊ 1 ∞
  example₁ = pointwise 0 (suc · 0 ∞) (1 ∞) refl

  example₂ : ∀ s → suc · s ≊ 1 ∞ ⟨ _+_ ⟩ s
  example₂ = pointwise 1 (λ s → suc · s)
                         (λ s → 1 ∞ ⟨ _+_ ⟩ s)
                         (λ _ → refl)

  example₃ : ∀ s t u →
             (s ⟨ _+_ ⟩ t) ⟨ _+_ ⟩ u ≊ s ⟨ _+_ ⟩ (t ⟨ _+_ ⟩ u)
  example₃ = pointwise 3 (λ s t u → (s ⟨ _+_ ⟩ t) ⟨ _+_ ⟩ u)
                         (λ s t u →  s ⟨ _+_ ⟩ (t ⟨ _+_ ⟩ u))
                         +-assoc
    where
    open import Data.Nat.Properties

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- from http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.LocalDefinition

module Local where

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

  infixl 5 _+_
  _+_ : Nat -> Nat -> Nat
  zero + n = n
  (succ m) + n = succ (m + n)

  infixl 6 _*_
  _*_ : Nat -> Nat -> Nat
  zero * _ = zero
  (succ m) * n = n + m * n

  f : Nat
  f =  let h : Nat -> Nat
           h m = succ (succ m)
        in h zero + h (succ zero)

  t1 : Nat
  t1 = f

  h : Nat -> Nat
  h n = let add2 : Nat
            add2 = succ (succ n)

            twice : Nat -> Nat
            twice m = m * m

        in twice add2

  g : Nat -> Nat
  g n = fib n + fact n
   where fib : Nat -> Nat
         fib zero = succ zero
         fib (succ zero) = succ zero
         fib (succ (succ n)) = fib (succ n) + fib n

         fact : Nat -> Nat
         fact zero = succ zero
         fact (succ n) = succ n * fact n

  k : Nat -> Nat
  k n = let aux : Nat -> Nat
            aux m = pred (g m) + h m
        in aux (pred n)
    where pred : Nat -> Nat
          pred zero = zero
          pred (succ m) = m


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

syntax TLC | Λ

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  𝟙   : 0-ary
  _⊗_ : 2-ary | l40
  𝟘   : 0-ary
  _⊕_ : 2-ary | l30

term
  app   : α ↣ β  α  ->  β | _$_ l20
  lam   : α.β  ->  α ↣ β | ƛ_ r10
  unit  : 𝟙
  pair  : α  β  ->  α ⊗ β | ⟨_,_⟩
  fst   : α ⊗ β  ->  α
  snd   : α ⊗ β  ->  β
  abort : 𝟘  ->  α
  inl   : α  ->  α ⊕ β
  inr   : β  ->  α ⊕ β
  case  : α ⊕ β  α.γ  β.γ  ->  γ
  ze    : N
  su    : N  ->  N
  nrec  : N  α  (α,N).α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
  (𝟙η) u : 𝟙 |> u = unit
  (fβ) a : α  b : β |> fst (pair(a, b))      = a
  (sβ) a : α  b : β |> snd (pair(a, b))      = b
  (pη) p : α ⊗ β    |> pair (fst(p), snd(p)) = p
  (𝟘η) e : 𝟘  c : α |> abort(e) = c
  (lβ) a : α   f : α.γ  g : β.γ |> case (inl(a), x.f[x], y.g[y])      = f[a]
  (rβ) b : β   f : α.γ  g : β.γ |> case (inr(b), x.f[x], y.g[y])      = g[b]
  (cη) s : α ⊕ β  c : (α ⊕ β).γ |> case (s, x.c[inl(x)], y.c[inr(y)]) = c[s]
  (zeβ) z : α   s : (α,N).α        |> nrec (ze,       z, r m. s[r,m]) = z
  (suβ) z : α   s : (α,N).α  n : N |> nrec (su (n), z, r m. s[r,m]) = s[nrec (n, z, r m. s[r,m]), n]
  (ift) t f : α |> if (true,  t, f) = t
  (iff) t f : α |> if (false, t, f) = f
-}

module TLC.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import TLC.Signature
open import TLC.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution Λ:Syn
open import SOAS.Metatheory.SecondOrder.Equality Λ:Syn

private
  variable
    α β γ τ : ΛT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ Λ) α Γ → (𝔐 ▷ Λ) α Γ → Set where
  ƛβ  : ⁅ α ⊩ β ⁆ ⁅ α ⁆̣           ▹ ∅ ⊢                    (ƛ 𝔞⟨ x₀ ⟩) $ 𝔟 ≋ₐ 𝔞⟨ 𝔟 ⟩
  ƛη  : ⁅ α ↣ β ⁆̣                 ▹ ∅ ⊢                         ƛ (𝔞 $ x₀) ≋ₐ 𝔞
  𝟙η  : ⁅ 𝟙 ⁆̣                     ▹ ∅ ⊢                                  𝔞 ≋ₐ unit
  fβ  : ⁅ α ⁆ ⁅ β ⁆̣               ▹ ∅ ⊢                    fst (⟨ 𝔞 , 𝔟 ⟩) ≋ₐ 𝔞
  sβ  : ⁅ α ⁆ ⁅ β ⁆̣               ▹ ∅ ⊢                    snd (⟨ 𝔞 , 𝔟 ⟩) ≋ₐ 𝔟
  pη  : ⁅ α ⊗ β ⁆̣                 ▹ ∅ ⊢              ⟨ (fst 𝔞) , (snd 𝔞) ⟩ ≋ₐ 𝔞
  𝟘η  : ⁅ 𝟘 ⁆ ⁅ α ⁆̣               ▹ ∅ ⊢                            abort 𝔞 ≋ₐ 𝔟
  lβ  : ⁅ α ⁆ ⁅ α ⊩ γ ⁆ ⁅ β ⊩ γ ⁆̣ ▹ ∅ ⊢   case (inl 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩) ≋ₐ 𝔟⟨ 𝔞 ⟩
  rβ  : ⁅ β ⁆ ⁅ α ⊩ γ ⁆ ⁅ β ⊩ γ ⁆̣ ▹ ∅ ⊢   case (inr 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩) ≋ₐ 𝔠⟨ 𝔞 ⟩
  cη  : ⁅ α ⊕ β ⁆ ⁅ (α ⊕ β) ⊩ γ ⁆̣ ▹ ∅ ⊢ case 𝔞 (𝔟⟨ inl x₀ ⟩) (𝔟⟨ inr x₀ ⟩) ≋ₐ 𝔟⟨ 𝔞 ⟩
  zeβ : ⁅ α ⁆ ⁅ α · N ⊩ α ⁆̣       ▹ ∅ ⊢           nrec ze 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩) ≋ₐ 𝔞
  suβ : ⁅ α ⁆ ⁅ α · N ⊩ α ⁆ ⁅ N ⁆̣ ▹ ∅ ⊢       nrec (su 𝔠) 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩) ≋ₐ 𝔟⟨ (nrec 𝔠 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩)) ◂ 𝔠 ⟩

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

-- Derived equations
ift : ⁅ α ⁆ ⁅ α ⁆̣ ▹ ∅ ⊢ if true 𝔞 𝔟 ≋ 𝔞
ift = ax lβ with《 unit ◃ 𝔞 ◃ 𝔟 》
iff : ⁅ α ⁆ ⁅ α ⁆̣ ▹ ∅ ⊢ if false 𝔞 𝔟 ≋ 𝔟
iff = ax rβ with《 unit ◃ 𝔞 ◃ 𝔟 》

-- Double beta reduction
ƛβ² : ⁅ β · α ⊩ γ ⁆ ⁅ α ⁆ ⁅ β ⁆̣ ▹ ∅ ⊢ (ƛ (ƛ 𝔞⟨ x₀ ◂ x₁ ⟩)) $ 𝔟 $ 𝔠 ≋ 𝔞⟨ 𝔠 ◂ 𝔟 ⟩
ƛβ² = begin
      (ƛ (ƛ 𝔞⟨ x₀ ◂ x₁ ⟩)) $ 𝔟 $ 𝔠
  ≋⟨ cong[ ax ƛβ with《 (ƛ 𝔞⟨ x₀ ◂ x₁ ⟩) ◃ 𝔟 》 ]inside ◌ᵈ $ 𝔠 ⟩
      (ƛ 𝔞⟨ x₀ ◂ 𝔟 ⟩) $ 𝔠
  ≋⟨ ax ƛβ with《 (𝔞⟨ x₀ ◂ 𝔟 ⟩) ◃ 𝔠 》 ⟩
      𝔞⟨ 𝔠 ◂ 𝔟 ⟩
  ∎

-- Uncurrying and arithmetic
1+2 : ⁅⁆ ▹ ∅ ⊢ uncurry $ plus $ ⟨ su ze , su (su ze) ⟩ ≋ su (su (su ze))
1+2 = begin
      uncurry $ plus $ ⟨ su ze , su (su ze) ⟩
  ≋⟨ thm ƛβ² with《 x₁ $ fst x₀ $ snd x₀ ◃ plus ◃ ⟨ su ze , su (su ze) ⟩ 》 ⟩
      plus $ fst ⟨ su ze , su (su ze) ⟩ $ snd ⟨ su ze , su (su ze) ⟩
  ≋⟨ cong₂[ ax fβ with《 su ze ◃ su (su ze) 》 ][
            ax sβ with《 su ze ◃ su (su ze) 》 ]inside plus $ ◌ᵃ $ ◌ᵇ ⟩
      plus $ su ze $  su (su ze)
  ≋⟨ thm ƛβ² with《 nrec x₁ x₀ (su x₀) ◃ su ze ◃ su (su ze) 》 ⟩
      nrec (su ze) (su (su ze)) (su x₀)
  ≋⟨ ax suβ with《 su (su ze) ◃ su x₀ ◃ ze 》 ⟩
      su (nrec ze (su (su ze)) (su x₀))
  ≋⟨ cong[ ax zeβ with《 su (su ze) ◃ su x₀ 》 ]inside su ◌ᵃ ⟩
      su (su (su ze))
  ∎

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

module Light.Implementation.Data.Unit where

open import Light.Library.Data.Unit using (Library ; Dependencies)

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            record Unit : Set where constructor unit

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
-- 2018-09-05, reported by Andreas Abel
-- The new type-directed rewriting was using the wrong type for
-- constructors of parametrized datatypes.

{-# OPTIONS --rewriting #-}

module _ where

module _ (Form : Set) where

  open import Agda.Builtin.Equality
  {-# BUILTIN REWRITE _≡_ #-}

  data Cxt : Set where
    _∙_ : (Γ : Cxt) (A : Form) → Cxt

  data _≤_ : (Γ Δ : Cxt) → Set where
    id≤ : ∀{Γ} → Γ ≤ Γ
    lift : ∀{A Γ Δ} (τ : Γ ≤ Δ) → (Γ ∙ A) ≤ (Δ ∙ A)

  postulate
    lift-id≤ : ∀{Γ A} → lift id≤ ≡ id≤ {Γ ∙ A}

{-# REWRITE lift-id≤ #-}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
module Syntax.Transitivity where

import      Lvl
open import Logic
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Type

private variable ℓ₁ ℓ₂ ℓ₃ : Lvl.Level
private variable T : Type{ℓ₁}

-- The transitivity operator
infixl 1000 _🝖_
_🝖_ : ∀{_▫_ : T → T → Stmt{ℓ₂}} → ⦃ _ : Transitivity(_▫_) ⦄ → Names.Transitivity(_▫_)
_🝖_ {_▫_ = _▫_} = transitivity(_▫_)

_🝖-subₗ_ : ∀{_▫₁_ : T → T → Stmt{ℓ₂}}{_▫₂_ : T → T → Stmt{ℓ₃}} → ⦃ _ : Subtransitivityₗ(_▫₁_)(_▫₂_) ⦄ → Names.Subtransitivityₗ(_▫₁_)(_▫₂_)
_🝖-subₗ_ {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_} = subtransitivityₗ(_▫₁_)(_▫₂_)

_🝖-subᵣ_ : ∀{_▫₁_ : T → T → Stmt{ℓ₂}}{_▫₂_ : T → T → Stmt{ℓ₃}} → ⦃ _ : Subtransitivityᵣ(_▫₁_)(_▫₂_) ⦄ → Names.Subtransitivityᵣ(_▫₁_)(_▫₂_)
_🝖-subᵣ_ {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_} = subtransitivityᵣ(_▫₁_)(_▫₂_)

-- Syntax for "equational reasoning" for reflexive-transitive relation

infixr 1 _🝖[_]-[_]_
_🝖[_]-[_]_ : (x : T) → ∀{y z : T} → (_▫_ : T → T → Stmt{ℓ₂}) → ⦃ _ : Transitivity(_▫_) ⦄ → (x ▫ y) → (y ▫ z) → (x ▫ z)
_🝖[_]-[_]_ (_)(_▫_) = transitivity(_▫_)

infixr 1 _🝖[_]-[_]-sym_
_🝖[_]-[_]-sym_ : (x : T) → ∀{y z : T} → (_▫_ : T → T → Stmt{ℓ₂}) → ⦃ _ : Transitivity(_▫_) ⦄ → ⦃ _ : Symmetry(_▫_) ⦄ → (y ▫ x) → (y ▫ z) → (x ▫ z)
_🝖[_]-[_]-sym_ (_)(_▫_) yx yz = transitivity(_▫_) (symmetry(_▫_) yx) (yz)

infixr 1 _🝖[_]-[_]-sub_
_🝖[_]-[_]-sub_ : (x : T) → ∀{y z : T}{_▫₁_ : T → T → Stmt{ℓ₂}} (_▫₂_ : T → T → Stmt{ℓ₃}) → ⦃ _ : Subtransitivityₗ(_▫₁_)(_▫₂_) ⦄ → (x ▫₂ y) → (y ▫₁ z) → (x ▫₁ z)
_🝖[_]-[_]-sub_ (_) {_▫₁_ = _▫₁_} (_▫₂_) = subtransitivityₗ(_▫₁_)(_▫₂_)

infixr 1 _🝖[_]-[_]-super_
_🝖[_]-[_]-super_ : (x : T) → ∀{y z : T} (_▫₁_ : T → T → Stmt{ℓ₂}) {_▫₂_ : T → T → Stmt{ℓ₃}} → ⦃ _ : Subtransitivityᵣ(_▫₁_)(_▫₂_) ⦄ → (x ▫₁ y) → (y ▫₂ z) → (x ▫₁ z)
_🝖[_]-[_]-super_ (_) (_▫₁_) {_▫₂_ = _▫₂_} = subtransitivityᵣ(_▫₁_)(_▫₂_)

infixr 1 _🝖[_]-[]_
_🝖[_]-[]_ : (x : T) → ∀{y : T} → (_▫_ : T → T → Stmt{ℓ₂}) → (x ▫ y) → (x ▫ y)
_🝖[_]-[]_ (_)(_▫_) xy = xy

infixr 2 _🝖-semiend_🝖[_]-end-from-[_]
_🝖-semiend_🝖[_]-end-from-[_] : (x y : T) → (_▫_ : T → T → Stmt{ℓ₂}) → ⦃ _ : Transitivity(_▫_) ⦄ → (x ▫ y) → (x ▫ y)
_🝖-semiend_🝖[_]-end-from-[_] _ _ (_▫_) xy = xy

infixr 2 _🝖[_]-end
_🝖[_]-end : (x : T) → (_▫_ : T → T → Stmt{ℓ₂}) → ⦃ _ : Reflexivity(_▫_) ⦄ → (x ▫ x)
_🝖[_]-end (_)(_▫_) = reflexivity(_▫_)

-- Syntax for "equational reasoning" for reflexive-transitive relations.
-- Example:
--   import      Lvl
--   open import Logic
--   open import Structure.Relator.Properties
--   open import Type
--   postulate ℓ₁ ℓ₂ : Lvl.Level
--   postulate T : Type{ℓ₁}
--   postulate _▫_ : T → T → Stmt{ℓ₂}
--   instance postulate trans : Transitivity(_▫_)
--   instance postulate sym   : Symmetry    (_▫_)
--   instance postulate refl  : Reflexivity (_▫_)
--   postulate a b c e : T
--   d = c
--   postulate ab : (a ▫ b)
--   postulate cb : (c ▫ b)
--   postulate de : (d ▫ e)
--
--   ac : (a ▫ e)
--   ac =
--     a 🝖-[ ab ]
--     b 🝖-[ cb ]-sym
--     c 🝖-[]
--     d 🝖-[ de ]
--     e 🝖-end

infixr 1 _🝖-[_]_
_🝖-[_]_ : (x : T) → ∀{y z : T}{_▫_ : T → T → Stmt{ℓ₂}} → ⦃ _ : Transitivity(_▫_) ⦄ → (x ▫ y) → (y ▫ z) → (x ▫ z)
_🝖-[_]_ (_) {_▫_ = _▫_} = transitivity(_▫_)

infixr 1 _🝖-[_]-sym_
_🝖-[_]-sym_ : (x : T) → ∀{y z : T}{_▫_ : T → T → Stmt{ℓ₂}} → ⦃ _ : Transitivity(_▫_) ⦄ → ⦃ _ : Symmetry(_▫_) ⦄ → (y ▫ x) → (y ▫ z) → (x ▫ z)
_🝖-[_]-sym_ (_) {_▫_ = _▫_} yx yz = transitivity(_▫_) (symmetry(_▫_) yx) (yz)

infixr 1 _🝖-[_]-sub_
_🝖-[_]-sub_ : (x : T) → ∀{y z : T}{_▫₁_ : T → T → Stmt{ℓ₂}}{_▫₂_ : T → T → Stmt{ℓ₃}} → ⦃ _ : Subtransitivityₗ(_▫₁_)(_▫₂_) ⦄ → (x ▫₂ y) → (y ▫₁ z) → (x ▫₁ z)
_🝖-[_]-sub_ (_) {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_} = subtransitivityₗ(_▫₁_)(_▫₂_)

infixr 1 _🝖-[_]-super_
_🝖-[_]-super_ : (x : T) → ∀{y z : T}{_▫₁_ : T → T → Stmt{ℓ₂}}{_▫₂_ : T → T → Stmt{ℓ₃}} → ⦃ _ : Subtransitivityᵣ(_▫₁_)(_▫₂_) ⦄ → (x ▫₁ y) → (y ▫₂ z) → (x ▫₁ z)
_🝖-[_]-super_ (_) {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_} = subtransitivityᵣ(_▫₁_)(_▫₂_)

infixr 1 _🝖-[]_
_🝖-[]_ : (x : T) → ∀{y : T}{_▫_ : T → T → Stmt{ℓ₂}} → (x ▫ y) → (x ▫ y)
_🝖-[]_ (_) xy = xy

infixr 2 _🝖-semiend_🝖-end-from-[_]
_🝖-semiend_🝖-end-from-[_] : (x y : T) → ∀{_▫_ : T → T → Stmt{ℓ₂}} → ⦃ _ : Transitivity(_▫_) ⦄ → (x ▫ y) → (x ▫ y)
_🝖-semiend_🝖-end-from-[_] _ _ {_▫_ = _▫_} xy = xy

infixr 2 _🝖-end
_🝖-end : (x : T) → ∀{_▫_ : T → T → Stmt{ℓ₂}} → ⦃ _ : Reflexivity(_▫_) ⦄ → (x ▫ x)
_🝖-end x {_▫_} = reflexivity(_▫_)

-- syntax _🝖-[]_ a {b} ab = a 🝖-[ ab ]-end b


text:
module UniDB.Subst.Inst where

open import UniDB.Spec
open import UniDB.Subst.Core
open import UniDB.Subst.Pair
open import UniDB.Subst.Shifts
open import UniDB.Morph.Pair
open import UniDB.Morph.Shift
open import UniDB.Morph.Shifts
open import UniDB.Morph.Unit

-- These are two unused instances. Just to show that ApHComp is slightly
-- stronger than ApPair, but given ApRel then ApPair and ApHComp become
-- equivalent.  Unfortunately neither ApPair nor ApHComp imply ApRel but
-- both can be made stronger to do so.
module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  (X : STX) {{apTX : Ap T X}} {{apHCompTX : ApHComp T X}}
  where

  iApPair : ApPair T X
  ap-pair {{iApPair}} {Ξ} {Ζ} ξ ζ x = ap-⊡ {T} {X} {Ξ} {Ζ} {Pair Ξ Ζ} ξ ζ x

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}}
  {{apRelTX : ApRel T X}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{wkmΞ : Wkm Ξ}}
  {{lkUpTΞ : LkUp T Ξ}} {{lkWkmTΞ : LkWkm T Ξ}}
  (Ζ : MOR) {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{wkmΖ : Wkm Ζ}}
  {{lkUpTΖ : LkUp T Ζ}} {{lkWkmTΖ : LkWkm T Ζ}}
  where

  ap-wkm-rel : {γ : Dom} (δ : Dom) (x : X γ) →
    ap {T} (wkm {Ξ} δ) x ≡ ap {T} (wkm {Ζ} δ) x
  ap-wkm-rel {γ} δ = ap-rel≃ {T} lemma
    where
      lemma : [ T ] wkm {Ξ} {γ} δ ≃ wkm {Ζ} δ
      lk≃ lemma i = begin
        lk {T} (wkm {Ξ} δ) i ≡⟨ lk-wkm {T} {Ξ} δ i ⟩
        vr (wk δ i)          ≡⟨ sym (lk-wkm {T} {Ζ} δ i) ⟩
        lk {T} (wkm {Ζ} δ) i ∎

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  (X : STX) {{apTX : Ap T X}} {{apPairTX : ApPair T X}} {{apRelTX : ApRel T X}}
  where

  iApHComp : ApHComp T X
  ap-⊡ {{iApHComp}} {Ξ} {Ζ} {Θ} ξ ζ x = begin
    ap {T} {X} {Θ}        (ξ ⊡ ζ) x       ≡⟨ ap-rel≅ {T} (≃-to-≅` lem) x ⟩
    ap {T} {X} {Pair Ξ Ζ} (ξ ⊡ ζ) x       ≡⟨ ap-pair {T} ξ ζ x ⟩
    ap {T} {X} {Ζ} ζ (ap {T} {X} {Ξ} ξ x) ∎
    where
      lem : (δ : Dom) → [ T ] ((_⊡_ {Θ = Θ} ξ ζ) ↑ δ) ≃ (ξ ⊗ ζ) ↑ δ
      lk≃ (lem δ) i = begin
        lk {T} {Θ}          ((ξ ⊡ ζ) ↑ δ) i   ≡⟨ cong (λ ρ → lk {T} {Θ} ρ i) (⊡-↑ {Ξ} {Ζ} {Θ} ξ ζ δ) ⟩
        lk {T} {Θ}          (ξ ↑ δ ⊡ ζ ↑ δ) i ≡⟨ lk-⊡-ap {T} {Ξ} {Ζ} {Θ} (ξ ↑ δ) (ζ ↑ δ) i ⟩
        lk {T} {Pair Ξ Ζ} (ξ ↑ δ ⊗ ζ ↑ δ) i ≡⟨ cong (λ ρ → lk {T} {Pair Ξ Ζ} ρ i) (sym (⊡-↑ {Ξ} {Ζ} {Pair Ξ Ζ} ξ ζ δ)) ⟩
        lk {T} {Pair Ξ Ζ} ((ξ ⊗ ζ) ↑ δ) i   ∎

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  (X : STX) {{apTX : Ap T X}} {{apPairTX : ApPair T X}} {{apRelTX : ApRel T X}}
  where

  iApComp : ApComp T X
  ap-⊙ {{iApComp}} {Ξ} ξ ζ x = begin
    ap {T} (ξ ⊙ ζ) x      ≡⟨ ap-rel≅ {T} (≃-to-≅` lem) x ⟩
    ap {T} (ξ ⊗ ζ) x      ≡⟨ ap-pair {T} ξ ζ x ⟩
    ap {T} ζ (ap {T} ξ x)  ∎
    where
      lem : (δ : Dom) → [ T ] (ξ ⊙ ζ) ↑ δ ≃ (ξ ⊗ ζ) ↑ δ
      lk≃ (lem δ) i = begin
        lk ((ξ ⊙ ζ) ↑ δ) i           ≡⟨ cong (λ ρ → lk ρ i) (⊙-↑ ξ ζ δ) ⟩
        lk (ξ ↑ δ ⊙ ζ ↑ δ) i         ≡⟨ lk-⊙-ap (ξ ↑ δ) (ζ ↑ δ) i ⟩
        ap {T} (ζ ↑ δ) (lk (ξ ↑ δ) i) ≡⟨ refl ⟩
        lk (ξ ↑ δ ⊗ ζ ↑ δ) i         ≡⟨ refl ⟩ -- cong (λ ρ → lk ρ i) (sym (⊡-↑ {Ξ} {Ξ} {Pair Ξ Ξ} ξ ζ δ)) ⟩
        lk ((ξ ⊗ ζ) ↑ δ) i           ∎

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  {{apVrT : ApVr T}} {{apWkmWkTT : ApWkmWk T T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}}
  {{apWkmWkTX : ApWkmWk T X}}
  {{apPairTX : ApPair T X}} {{apRelTX : ApRel T X}}
  (Ρ : MOR) {{lkTΡ : Lk T Ρ}} {{upΡ : Up Ρ}} {{lkUpTΡ : LkUp T Ρ}}
  {{wkmΡ : Wkm Ρ}} {{lkWkmΡ : LkWkm T Ρ}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
  {{lkUpPairΞΡ : LkUp T (Pair Ξ Ρ)}}
  {{lkUpPairΞΡ : LkUp T (Pair Ρ Ξ)}}
  where

  ap-wk₁-gen : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (x : X γ₁) →
    ap {T} {X} {Ξ} (ξ ↑₁) (wk₁ x) ≡ wk₁ (ap {T} {X} {Ξ} ξ x)
  ap-wk₁-gen ξ x = begin
    ap {T} (ξ ↑₁) (wk₁ x)                ≡⟨ cong (ap {T} (ξ ↑₁)) (sym (ap-wkm-wk₁ {T} {X} {Ρ} x)) ⟩
    ap {T} (ξ ↑₁) (ap {T} (wkm {Ρ} 1) x) ≡⟨ sym (ap-pair {T} (wkm {Ρ} 1) (ξ ↑₁) x) ⟩
    ap {T} (wkm {Ρ} 1 ⊗ ξ ↑₁) x         ≡⟨ ap-rel≃ {T} lem x ⟩
    ap {T} (ξ ⊗ wkm {Ρ} 1) x            ≡⟨ ap-pair {T} ξ (wkm {Ρ} 1) x ⟩
    ap {T} (wkm {Ρ} 1) (ap {T} ξ x)      ≡⟨ ap-wkm-wk₁ {T} (ap {T} ξ x) ⟩
    wk₁ (ap {T} ξ x)
    ∎
    where
      lem : [ T ] (wkm {Ρ} 1 ⊗ ξ ↑₁) ≃ (ξ ⊗ wkm {Ρ} 1)
      lk≃ lem i = begin
        ap {T} (ξ ↑₁) (lk {T} (wkm {Ρ} 1) i) ≡⟨ cong (ap {T} (_↑₁ ξ)) (lk-wkm {T} {Ρ} 1 i) ⟩
        ap {T} (ξ ↑₁) (vr (suc i))           ≡⟨ ap-vr {T} (ξ ↑₁) (suc i) ⟩
        lk {T} (ξ ↑₁) (suc i)                ≡⟨ lk-↑₁-suc {T} ξ i ⟩
        wk₁ (lk {T} ξ i)                     ≡⟨ sym (ap-wkm-wk₁ {T} (lk {T} ξ i)) ⟩
        ap {T} (wkm {Ρ} 1) (lk {T} ξ i)      ∎

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  {{wkVrT : WkVr T}}
  {{apVrT : ApVr T}} {{apWkmWkTT : ApWkmWk T T}}
  {{apPairTT : ApPair T T}} {{apRelTT : ApRel T T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}}
  {{apWkmWkTX : ApWkmWk T X}}
  {{apPairTX : ApPair T X}} {{apRelTX : ApRel T X}}
  where

  private
    Ren : MOR
    Ren = Shift

  iApWk : ApWk T X
  ap-wk₁ {{iApWk}} {Ξ} = ap-wk₁-gen T X Ren Ξ
    where
      instance
        iLkUpRenRen : LkUp T (Pair Ren Ren)
        iLkUpRenRen = iLkUpPairRenaming T Ren Ren
        iLkUpRenΞ : LkUp T (Pair Ren Ξ)
        iLkUpRenΞ = iLkUpPairRenaming T Ren Ξ
        iLkUpΞRen : LkUp T (Pair Ξ Ren)
        iLkUpΞRen = iLkUpPairSubstitution T Ξ Ren
          (ap-wk₁-gen T T Ren Ren)

{-
module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  {{wkVrT : WkVr T}} {{apVrT : ApVr T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}}
  {{apWkmWkTX : ApWkmWk T X}} {{apIdmTX : ApIdm T X}} {{apCompTX : ApComp T X}}
  where

  private
    module _
      (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
      {{idmΞ : Idm Ξ}} {{wkmΞ : Wkm Ξ}} {{compΞ : Comp Ξ}}
      {{lkUpTΞ : LkUp T Ξ}} {{lkWkmTΞ : LkWkm T Ξ}} {{lkIdmTΞ : LkIdm T Ξ}}
      {{upIdmΞ : UpIdm Ξ}} {{upCompΞ : UpComp Ξ}} {{lkCompTΞ : LkCompAp T Ξ}}
      {{wkmHomΞ : WkmHom Ξ}}
      where

      iWkHom` : WkHom X
      wk-zero {{iWkHom`}} x = begin
        wk 0 x                                    ≡⟨ sym (ap-wkm-wk T X Ξ 0 x) ⟩
        ap T X Ξ (wkm Ξ 0) x                      ≡⟨ cong (λ ξ → ap T X Ξ ξ x) (wkm-zero Ξ) ⟩
        ap T X Ξ (idm Ξ _) x                      ≡⟨ ap-idm T X Ξ x ⟩
        x ∎
      wk-suc  {{iWkHom`}} δ x = begin
        wk (suc δ) x                              ≡⟨ sym (ap-wkm-wk T X Ξ (suc δ) x) ⟩
        ap T X Ξ (wkm Ξ (suc δ)) x                ≡⟨ cong (λ ξ → ap T X Ξ ξ x) (wkm-suc Ξ δ) ⟩
        ap T X Ξ (wkm Ξ δ ⊙ wkm Ξ 1) x            ≡⟨ ap-⊙ T X Ξ (wkm Ξ δ) (wkm Ξ 1) x ⟩
        ap T X Ξ (wkm Ξ 1) (ap T X Ξ (wkm Ξ δ) x) ≡⟨ ap-wkm-wk₁ T X Ξ (ap T X Ξ (wkm Ξ δ) x) ⟩
        wk₁ (ap T X Ξ (wkm Ξ δ) x)                ≡⟨ cong wk₁ (ap-wkm-wk T X Ξ δ x) ⟩
        wk₁ (wk δ x)                              ∎

  iWkHom : WkHom X
  iWkHom = iWkHom` Shifts
-}

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

module Issue950a where

postulate
  A : Set

record R : Set where
  field
    x : A

record S : Set where
  field
    y : A

open R

f : A
x f = ?

-- Bad error:

-- Arguments left we cannot split on. TODO: better error message
-- when checking that the clause x f = ? has type A

-- Better error:

-- Cannot eliminate type A with projection pattern x
-- when checking that the clause x f = ? has type A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module FFI.System.Exit where

open import Agda.Builtin.Int using (Int)
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)

data ExitCode : Set where
  ExitSuccess : ExitCode
  ExitFailure : Int → ExitCode

{-# FOREIGN GHC data AgdaExitCode = AgdaExitSuccess | AgdaExitFailure Integer #-}
{-# COMPILE GHC ExitCode = data AgdaExitCode (AgdaExitSuccess | AgdaExitFailure) #-}

{-# FOREIGN GHC import qualified System.Exit #-}

{-# FOREIGN GHC
toExitCode :: AgdaExitCode -> System.Exit.ExitCode
toExitCode AgdaExitSuccess = System.Exit.ExitSuccess
toExitCode (AgdaExitFailure n) = System.Exit.ExitFailure (fromIntegral n)

fromExitCode :: System.Exit.ExitCode -> AgdaExitCode
fromExitCode System.Exit.ExitSuccess = AgdaExitSuccess
fromExitCode (System.Exit.ExitFailure n) = AgdaExitFailure (fromIntegral n)
#-}

postulate
  exitWith : ExitCode → IO ⊤

{-# COMPILE GHC exitWith = System.Exit.exitWith . toExitCode #-}

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module Issue566 where

open import Common.Level using (Level; _⊔_)

data D (a : Level) (A : Set a) : Set a where
 d : D a A → D a A

P-level : (a : Level) (A : Set a) → D a A → Level
P-level a A (d x) = P-level a A x

P : (a : Level) (A : Set a) (x : D a A) → Set (P-level a A x)
P a A (d x) = P a A x

postulate
 a : Level
 E : (b : Level) → Set b → Set a → Set (a ⊔ b)
 Q : (A : Set a) → D a A → Set a
 e : (A : Set a) (x : D a A) → E (P-level a A x) (P a A x) (Q A x)
 A : Set a
 x : D a A

foo : E (P-level a A x) (P a A x) (Q A x)
foo = e _ _

-- Bug.agda:23,7-12
-- P-level a A x ⊔ a != P-level a A x ⊔ a of type Level
-- when checking that the expression e _ _ has type
-- E (P-level a A x) (P a A x) (Q A x)