text:
module prelude.list where
open import Data.Nat renaming (zero to z; suc to s)
open import Data.Fin as Fin using (Fin)
import Data.Fin as Fin renaming (zero to z; suc to s)
open import Agda.Builtin.Sigma
open import Data.Product
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
open import Data.Empty
open import Function

Vect : ∀ {ℓ} → ℕ → Set ℓ → Set ℓ
Vect n t = Fin n → t
List : ∀ {ℓ} → Set ℓ → Set ℓ
List t = Σ[ n ∈ ℕ ] Vect n t
len : ∀ {ℓ} {a : Set ℓ} → List a → ℕ
len = fst
head : ∀ {ℓ} {a : Set ℓ} → (as : List a) → (len as ≢ z) → a
head (z , as) n≢0 = ⊥-elim (n≢0 refl)
head (s n , as) _ = as Fin.z
tail : ∀ {ℓ} {a : Set ℓ} → (as : List a) → (len as ≢ z) → List a
tail (z , as) n≢0 = ⊥-elim (n≢0 refl)
tail (s n , as) _ = n , (as ∘ Fin.inject₁)

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


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

module Categories.Category.Instance.Properties.Setoids.Extensive where

open import Level
open import Data.Product using (Σ; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_)
open import Function.Equality using (Π)
open import Relation.Binary using (Setoid; Rel)
open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Instance.Setoids
open import Categories.Category.Extensive
open import Categories.Category.Cocartesian
open import Categories.Diagram.Pullback
open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical
open import Categories.Category.Monoidal.Instance.Setoids
open import Data.Sum.Relation.Binary.Pointwise
open import Data.Unit.Polymorphic using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum.Base using ([_,_]′; _⊎_)
open import Function.Equality as SΠ renaming (id to ⟶-id)
open import Data.Product using (∃)

open import Relation.Binary.PropositionalEquality using (_≡_; [_]; inspect)

open Π

module _ ℓ where
  private
    S = Setoids ℓ ℓ
    module S = Category S

  open Pullback

  Setoids-Extensive : (ℓ : Level) → Extensive (Setoids ℓ ℓ)
  Setoids-Extensive ℓ = record
     { cocartesian = record { initial = initial ; coproducts = coproducts }
     ; pullback₁ = λ f → pullback ℓ ℓ f i₁
     ; pullback₂ = λ f → pullback ℓ ℓ f i₂
     ; pullback-of-cp-is-cp = λ {C A B} f → record
          { [_,_] = λ g h → record
              { _⟨$⟩_ = copair-$ f g h
              ; cong = λ {z z′} → copair-cong f g h z z′
              }
          ; inject₁ = λ {X g h z} eq →
               trans (isEquivalence {ℓ} X) (copair-inject₁ f g h z) (cong g eq)
          ; inject₂ = λ {X g h z} eq →
               trans (isEquivalence {ℓ} X) (copair-inject₂ f g h z) (cong h eq)
          ; unique = λ {X u g h} feq₁ feq₂ {z z′} eq →
               trans (isEquivalence {ℓ} X) (copair-unique f g h u z (λ {z} → feq₁ {z}) (λ {z} → feq₂ {z})) (cong u eq)
          }
     ; pullback₁-is-mono = λ _ _ eq x≈y → drop-inj₁ (eq x≈y)
     ; pullback₂-is-mono = λ _ _ eq x≈y → drop-inj₂ (eq x≈y)
     ; disjoint = λ {A B} → record
          { commute = λ { {()} _}
          ; universal = λ {C f g} eq → record
             { _⟨$⟩_ = λ z → conflict A B (f ⟨$⟩ z) (g ⟨$⟩ z) (eq (refl (isEquivalence {ℓ} C)))
             ; cong = λ z → tt
             }
          ; unique = λ _ _ _ → tt
          ; p₁∘universal≈h₁ = λ {C h₁ h₂ eq x y} x≈y → conflict A B (h₁ ⟨$⟩ x) (h₂ ⟨$⟩ y) (eq x≈y)
          ; p₂∘universal≈h₂ = λ {C h₁ h₂ eq x y} x≈y → conflict A B (h₁ ⟨$⟩ x) (h₂ ⟨$⟩ y) (eq x≈y)
          }
     }
       where
         open Cocartesian (Setoids-Cocartesian {ℓ} {ℓ})
         open Relation.Binary.IsEquivalence
         open import Data.Sum using (inj₁; inj₂)
         open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence)

         -- must be in the standard library. Maybe it is?
         conflict : ∀ {ℓ ℓ' ℓ''} (X Y : Setoid ℓ ℓ') {Z : Set ℓ''}
           (x : ∣ X ∣) (y : ∣ Y ∣) → [ ⊎-setoid X Y ][ inj₁ x ≈ inj₂ y ] → Z
         conflict X Y x y ()

         module Diagram {A B C X : Setoid ℓ ℓ} (f : C ⟶ ⊎-setoid A B)
           (g : P (pullback ℓ ℓ f i₁) ⟶ X) (h : P (pullback ℓ ℓ f i₂) ⟶ X) where

           private
             A⊎B = ⊎-setoid A B
             A′ = P (pullback ℓ ℓ f i₁)
             B′ = P (pullback ℓ ℓ f i₂)

             refl-A = refl (isEquivalence A)
             refl-B = refl (isEquivalence B)
             refl-C = refl (isEquivalence C)
             refl-A⊎B = refl (isEquivalence A⊎B)

             reflexive-A⊎B = reflexive (isEquivalence A⊎B)

             sym-A = sym (isEquivalence A)
             sym-B = sym (isEquivalence B)
             sym-C = sym (isEquivalence C)
             sym-X = sym (isEquivalence X)
             sym-A⊎B = sym (isEquivalence A⊎B)

             trans-X = trans (isEquivalence X)
             trans-A⊎B = trans (isEquivalence A⊎B)

           -- copairing of g : A′ → X and h : B′ → X, resulting in C → X
           copair-$ : ∣ C ∣ → ∣ X ∣
           copair-$ z with (f ⟨$⟩ z) | inspect (f ⟨$⟩_) z
           ... | inj₁ x | [ eq ] = g ⟨$⟩ record { elem₁ = z ; elem₂ = x ; commute = reflexive-A⊎B eq }
           ... | inj₂ y | [ eq ] = h ⟨$⟩ record { elem₁ = z ; elem₂ = y ; commute = reflexive-A⊎B eq }

           -- somewhat roundabout way to expand the definition of copair-$ z if f ⟨$⟩ z ≈ inj₁ x,
           -- in order to circumwent the pitfalls of the with-abstraction
           copair-$-i₁ : (x : ∣ A ∣) (z : ∣ C ∣) → (eq : [ A⊎B ][ f ⟨$⟩ z ≈ inj₁ x ]) →
             ∃ (λ v → [ X ][ copair-$ z ≈ g ⟨$⟩ v ] ×
                        [ C ][ FiberProduct.elem₁ v ≈ z ] ×
                        [ A ][ FiberProduct.elem₂ v ≈ x ])
           copair-$-i₁ x z eq with (f ⟨$⟩ z) | inspect (f ⟨$⟩_) z
           ... | inj₁ x′ | [ eq′ ] =
             record { elem₁ = z ; elem₂ =  x′ ; commute = reflexive-A⊎B eq′}
             , cong g (refl-C , refl-A)
             , refl-C
             , drop-inj₁ eq

           -- same for f ⟨$⟩ z ≈ inj₂ y
           copair-$-i₂ : (y : ∣ B ∣) (z : ∣ C ∣) → (eq : [ A⊎B ][ f ⟨$⟩ z ≈ inj₂ y ]) →
             ∃ (λ v → [ X ][ copair-$ z ≈ h ⟨$⟩ v ] × [ C ][ FiberProduct.elem₁ v ≈ z ] × [ B ][ FiberProduct.elem₂ v ≈ y ])
           copair-$-i₂ y z eq with (f ⟨$⟩ z) | inspect (f ⟨$⟩_) z
           ... | inj₂ y′ | [ eq′ ] =
             record { elem₁ = z ; elem₂ =  y′ ; commute = reflexive-A⊎B eq′}
             , cong h (refl-C , refl-B)
             , refl-C
             , drop-inj₂ eq

           case-f⟨$⟩z : (z : ∣ C ∣) → (∃ λ x → [ A⊎B ][ f ⟨$⟩ z ≈ inj₁ x ]) ⊎ (∃ λ y → [ A⊎B ][ f ⟨$⟩ z ≈ inj₂ y ])
           case-f⟨$⟩z z with (f ⟨$⟩ z)
           ... | inj₁ x = inj₁ (x , refl-A⊎B)
           ... | inj₂ y = inj₂ (y , refl-A⊎B)

           copair-cong : (z z′ : ∣ C ∣) → (z≈z′ : [ C ][ z ≈ z′ ]) → [ X ][ copair-$ z ≈ copair-$ z′ ]
           copair-cong z z′ z≈z′ with (f ⟨$⟩ z) | inspect (_⟨$⟩_ f) z | (f ⟨$⟩ z′) | inspect (_⟨$⟩_ f) z′
           ... | inj₁ x | [ eq ] | inj₁ x′ | [ eq′ ] = cong g
             (z≈z′ , drop-inj₁ (trans-A⊎B (sym-A⊎B (reflexive-A⊎B eq)) (trans-A⊎B (cong f z≈z′) (reflexive-A⊎B eq′))))
           ... | inj₁ x | [ eq ] | inj₂ y  | [ eq′ ] = conflict A B x y
             (trans-A⊎B (sym-A⊎B (reflexive-A⊎B eq)) (trans-A⊎B (cong f z≈z′) (reflexive-A⊎B eq′)))
           ... | inj₂ y | [ eq ] | inj₁ x  | [ eq′ ] = conflict A B x y
             (trans-A⊎B (sym-A⊎B (reflexive-A⊎B eq′)) (trans-A⊎B (cong f (sym-C z≈z′)) (reflexive-A⊎B eq)))
           ... | inj₂ y | [ eq ] | inj₂ y′ | [ eq′ ] = cong h (z≈z′ , drop-inj₂
             (trans-A⊎B (sym-A⊎B (reflexive-A⊎B eq)) (trans-A⊎B (cong f z≈z′) (reflexive-A⊎B eq′))))

           copair-inject₁ : (z : FiberProduct f i₁) → [ X ][ copair-$ (FiberProduct.elem₁ z) ≈ g ⟨$⟩ z ]
           copair-inject₁ record { elem₁ = z ; elem₂ = x ; commute = eq } with case-f⟨$⟩z z
           ... | inj₁ _  with copair-$-i₁ x z eq
           ... | _ , eq₁ , eq₂ , eq₃ = trans-X eq₁ (cong g (eq₂ , eq₃))
           copair-inject₁ record { elem₁ = z ; elem₂ = x ; commute = eq } | inj₂ (y , eq′) =
             conflict A B x y (trans-A⊎B (sym-A⊎B eq) eq′)

           copair-inject₂ : (z : FiberProduct f i₂) → [ X ][ copair-$ (FiberProduct.elem₁ z) ≈ h ⟨$⟩ z ]
           copair-inject₂ record { elem₁ = z ; elem₂ = y ; commute = eq } with case-f⟨$⟩z z
           ... | inj₂ _  with copair-$-i₂ y z eq
           ... | _ , eq₁ , eq₂ , eq₃ = trans-X eq₁ (cong h (eq₂ , eq₃))
           copair-inject₂ record { elem₁ = z ; elem₂ = y ; commute = eq } | inj₁ (x , eq′) =
             conflict A B x y (trans-A⊎B (sym-A⊎B eq′) eq)

           copair-unique : (u : C ⟶ X) (z : ∣ C ∣) →
             [ A′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
             [ B′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
             [ X ][ copair-$ z ≈ u ⟨$⟩ z ]
           copair-unique u z feq₁ feq₂ with case-f⟨$⟩z z
           ... | inj₁ (x , eq) with copair-$-i₁ x z eq
           ... | z′ , eq₁ , eq₂ , _ = trans-X eq₁ (trans-X (sym-X (feq₁{z′} (refl-C , refl-A))) (cong u eq₂))
           copair-unique u z feq₁ feq₂ | inj₂ (y , eq) with copair-$-i₂ y z eq
           ... | z′ , eq₁ , eq₂ , _ = trans-X eq₁ (trans-X (sym-X (feq₂{z′} (refl-C , refl-B))) (cong u eq₂))

         open Diagram

ext: agda

max_stars_repo_name: sergey-goncharov/agda-categories

max_issues_repo_name: sergey-goncharov/agda-categories

max_forks_repo_name: sergey-goncharov/agda-categories


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

module Erased-cubical where

-- Modules that use --cubical can be imported.

open import Erased-cubical.Cubical-again

-- Code from such modules that was originally defined in modules using
-- --without-K or --erased-cubical can be used without restrictions.

_ : {A : Set} → A → ∥ A ∥
_ = ∣_∣

_ : D
_ = c

-- Matching on an erased constructor that was defined in a module that
-- uses --cubical is fine, and makes it possible to use erased
-- definitions in the right-hand side.

f : D′ → D′
f c′ = c′

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Finitude.Properties where
open import Data.Fin as Fin using (Fin; #_ )
open import Data.Fin.Properties hiding (decSetoid)
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary renaming (Decidable to Dec₂) hiding (Irrelevant)
open import Relation.Binary.PropositionalEquality as P hiding (decSetoid; isEquivalence)
open import Data.Finitude
open import Function.Equality as F using (_⟨$⟩_)
open import Function.Inverse as Inv using (Inverse)
open import Data.Nat as ℕ hiding (_≟_)
import Level

finitude→≡ : ∀ {n m} → Finitude (P.setoid (Fin n)) m → n ≡ m
finitude→≡ fin = ⇒Fin∼Fin fin
  where
    open import Data.Fin.PigeonHole

dec-≈ : ∀ {a ℓ n}{S : Setoid a ℓ} → Finitude S n → Dec₂ (Setoid._≈_ S)
dec-≈ {S = S} fin x y with (Inverse.to fin ⟨$⟩ x) ≟ (Inverse.to fin ⟨$⟩ y)
dec-≈ {S = S} fin x y | yes fx≡fy = yes (Inverse.injective fin fx≡fy)
dec-≈ {S = S} fin x y | no fx≢fy = no (λ x≈y → fx≢fy (F.cong (Inverse.to fin) x≈y))

decSetoid : ∀ {a ℓ n}{S : Setoid a ℓ} → Finitude S n → DecSetoid a ℓ
decSetoid {S = S} fin = record {
          isDecEquivalence = record {
            _≟_ = dec-≈ fin
          ; isEquivalence = isEquivalence
          }
          }
          where open Setoid S

same-size↔  : ∀ {n a₁ a₂ ℓ₁ ℓ₂}{A₁ : Setoid a₁ ℓ₁}{A₂ : Setoid a₂ ℓ₂} → Finitude A₁ n → Finitude A₂ n → Inverse A₁ A₂
same-size↔ fin₁ fin₂ = Inv.sym fin₂ Inv.∘  fin₁

size-unique : ∀ {a ℓ} {A : Setoid a ℓ} {n m} → Finitude A n → Finitude A m → n ≡ m
size-unique finN finM = finitude→≡ (finM Inv.∘ Inv.sym finN)

{-
open import Data.Empty
open import Data.Unit

Irr : ∀ {a ℓ}(S : Setoid a ℓ) → Set (a Level.⊔ ℓ)
Irr S = ∀ x y → x ≈ y
  where
    open Setoid S

⊥-Irr : Irrelevant ⊥
⊥-Irr = λ ()

⊤-Irr : Irrelevant ⊤
⊤-Irr = λ _ _ → P.refl

Irr-finitude : ∀ {a ℓ n}{S : Set a} → Irrelevant S → Finitude (P.setoid S) n → n ℕ.≤ 1
Irr-finitude {n = ℕ.zero} irr fin = z≤n
Irr-finitude {n = ℕ.suc ℕ.zero} irr fin = s≤s z≤n
Irr-finitude {n = ℕ.suc (ℕ.suc n)}{S} irr fin = ⊥-elim contra
   where
     open Setoid S
     x₀ = Inverse.from fin ⟨$⟩ # 0
     x₁ = Inverse.from fin ⟨$⟩ # 1

     contra : ⊥
     contra with Inverse.injective (Inv.sym fin) (irr x₀ x₁)
     ... | ()
-}

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
-- Andreas, 2016-10-03, re issue #2231
-- Testing whether the musical coinduction works fine in abstract blocks

{-# OPTIONS --guardedness #-}

module AbstractCoinduction where

{-# BUILTIN INFINITY ∞_  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

infixr 5 _≺_

abstract

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

  data Stream (A : Set) : Set where
    _≺_ : (x : A) (xs : ∞ (Stream A)) -> Stream A

  head : ∀ {A} -> Stream A -> A
  head (x ≺ xs) = x

  tail : ∀ {A} -> Stream A -> Stream A
  tail (x ≺ xs) = ♭ xs

  ------------------------------------------------------------------------
  -- Stream programs

  infix  8 _∞
  infixr 5 _⋎_
  infix  4 ↓_

  mutual

    data Stream′ (A : Set) : Set1 where
      _≺_ : (x : A) (xs : ∞ (StreamProg A)) -> Stream′ A

    data StreamProg (A : Set) : Set1 where
      ↓_  : (xs : Stream′ A) -> StreamProg A
      _∞'  : (x : A) -> StreamProg A
      _⋎'_ : (xs ys : StreamProg A) -> StreamProg A

  _∞ : ∀ {A : Set} (x : A) -> StreamProg A
  _∞ = _∞'

  _⋎_ : ∀ {A : Set} (xs ys : StreamProg A) -> StreamProg A
  _⋎_ = _⋎'_

  head′ : ∀ {A} → Stream′ A → A
  head′ (x ≺ xs) = x

  tail′ : ∀ {A} → Stream′ A → StreamProg A
  tail′ (x ≺ xs) = ♭ xs

  P⇒′ : ∀ {A} -> StreamProg A -> Stream′ A
  P⇒′ (↓ xs)    = xs
  P⇒′ (x ∞')     = x ≺ ♯ (x ∞)
  P⇒′ (xs ⋎' ys) with P⇒′ xs
  P⇒′ (xs ⋎' ys) | xs′ = head′ xs′ ≺ ♯ (ys ⋎ tail′ xs′)

  mutual

    ′⇒ : ∀ {A} -> Stream′ A -> Stream A
    ′⇒ (x ≺ xs) = x ≺ ♯ P⇒ (♭ xs)

    P⇒ : ∀ {A} -> StreamProg A -> Stream A
    P⇒ xs = ′⇒ (P⇒′ xs)

  ------------------------------------------------------------------------
  -- Stream equality

  infix 4 _≡_ _≈_ _≊_

  data _≡_ {a : Set} (x : a) : a -> Set where
    ≡-refl : x ≡ x

  data _≈_ {A} (xs ys : Stream A) : Set where
    _≺_ : (x≡ : head xs ≡ head ys) (xs≈ : ∞ (tail xs ≈ tail ys)) ->
          xs ≈ ys

  _≊_ : ∀ {A} (xs ys : StreamProg A) -> Set
  xs ≊ ys = P⇒ xs ≈ P⇒ ys

  foo : ∀ {A : Set} (x : A) -> x ∞ ⋎ x ∞ ≊ x ∞
  foo x = ≡-refl ≺ ♯ foo x

  -- The first goal has goal type
  --   head (′⇒ (x ≺ x ∞ ⋎ x ∞)) ≡ head (′⇒ (x ≺ x ∞)).
  -- The normal form of the left-hand side is x, and the normal form of
  -- the right-hand side is x (both according to Agda), but ≡-refl is
  -- not accepted by the type checker:
  --   x != head (′⇒ (P⇒′ (x ∞))) of type .A
  --   when checking that the expression ≡-refl has type
  --   (head (P⇒ (x ∞ ⋎ x ∞)) ≡ head (P⇒ (x ∞)))

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
module HasVacuousDischarge where

open import OscarPrelude
open import HasNegation
open import HasSubstantiveDischarge

record HasVacuousDischarge (A : Set) : Set₁
 where
  field
    ⦃ hasNegation ⦄ : HasNegation A
    ⦃ hasSubstantiveDischarge ⦄ : HasSubstantiveDischarge A A

  ◁_ : List A → Set
  ◁ +s = ∃ λ (s : A) → +s ≽ s × +s ≽ ~ s

  ⋪_ : List A → Set
  ⋪_ = ¬_ ∘ ◁_

open HasVacuousDischarge ⦃ … ⦄ public

{-# DISPLAY HasVacuousDischarge.◁_ _ = ◁_ #-}
{-# DISPLAY HasVacuousDischarge.⋪_ _ = ⋪_ #-}


text:
------------------------------------------------------------------------
-- A simplification of Hinze.Section3
------------------------------------------------------------------------

module Hinze.Simplified.Section3 where

open import Stream.Programs
open import Stream.Equality
open import Stream.Pointwise
open import Hinze.Simplified.Section2-4
open import Hinze.Lemmas

open import Codata.Musical.Notation hiding (∞)
open import Data.Product
open import Data.Bool
open import Data.Vec hiding (_⋎_)
open import Data.Nat renaming (suc to 1+)
import Data.Nat.Properties as Nat
import Relation.Binary.PropositionalEquality as P
open import Algebra.Structures
private
  module CS = IsCommutativeSemiring Nat.+-*-isCommutativeSemiring

------------------------------------------------------------------------
-- Abbreviations

2^ : ℕ → ℕ
2^ n = 2 ^ n

2*2^ : ℕ → ℕ
2*2^ n = 2 * 2 ^ n

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

pot : Prog Bool
pot = true ≺ ♯ (pot ⋎ false ∞)

msb : Prog ℕ
msb = 1 ≺ ♯ (2* · msb ⋎ 2* · msb)

ones′ : Prog ℕ
ones′ = 1 ≺ ♯ (ones′ ⋎ 1+ · ones′)

ones : Prog ℕ
ones = 0 ≺♯ ones′

carry : Prog ℕ
carry = 0 ≺ ♯ (1+ · carry ⋎ 0 ∞)

carry-folded : carry ≊ 0 ∞ ⋎ 1+ · carry
carry-folded = carry ∎

turn-length : ℕ → ℕ
turn-length 0      = 0
turn-length (1+ n) = ℓ + 1+ ℓ
  where ℓ = turn-length n

turn : (n : ℕ) → Vec ℕ (turn-length n)
turn 0      = []
turn (1+ n) = turn n ++ [ n ] ++ turn n

tree : ℕ → Prog ℕ
tree n = n ≺ ♯ (turn n ≺≺ tree (1+ n))

frac : Prog ℕ
frac = 0 ≺ ♯ (frac ⋎ 1+ · nat)

frac-folded : frac ≊ nat ⋎ frac
frac-folded = frac ∎

god : Prog ℕ
god = 1+2* · frac

------------------------------------------------------------------------
-- Laws and properties

carry-god-nat : 2^ · carry ⟨ _*_ ⟩ god ≊ tailP nat
carry-god-nat =
  2^ · carry ⟨ _*_ ⟩ god
                                 ≊⟨ ⟨ _*_ ⟩-cong (2^ · carry) (1 ∞ ⋎ 2* · 2^ · carry) lemma
                                                 god (1+2* · nat ⋎ god) (≅-sym (⋎-map 1+2* nat frac)) ⟩
  (1 ∞ ⋎ 2* · 2^ · carry)
         ⟨ _*_ ⟩
    (1+2* · nat ⋎ god)
                                 ≊⟨ ≅-sym (abide-law _*_ (1 ∞) (1+2* · nat) (2* · 2^ · carry) god) ⟩
    1 ∞ ⟨ _*_ ⟩ 1+2* · nat
              ⋎
  2* · 2^ · carry ⟨ _*_ ⟩ god
                                 ≊⟨ ⋎-cong (1 ∞ ⟨ _*_ ⟩ 1+2* · nat) (1+2* · nat)
                                           (pointwise 1 (λ s → 1 ∞ ⟨ _*_ ⟩ s) (λ s → s)
                                                        (λ n → proj₁ CS.*-identity n) (1+2* · nat))
                                           (2* · 2^ · carry ⟨ _*_ ⟩ god) (2* · (2^ · carry ⟨ _*_ ⟩ god))
                                           (pointwise 2 (λ s t → 2* · s ⟨ _*_ ⟩ t)
                                                        (λ s t → 2* · (s ⟨ _*_ ⟩ t))
                                                        (CS.*-assoc 2) (2^ · carry) god) ⟩
           1+2* · nat
               ⋎
  2* · (2^ · carry ⟨ _*_ ⟩ god)
                                 ≊⟨ P.refl ≺ coih ⟩
  1+2* · nat ⋎ 2* · tailP nat
                                 ≊⟨ ≅-sym (tailP-cong nat (2* · nat ⋎ 1+2* · nat) nat-lemma₂) ⟩
  tailP nat
                                 ∎
  where
  coih = ♯ ⋎-cong (2* · (2^ · carry ⟨ _*_ ⟩ god)) (2* · tailP nat)
                  (·-cong 2* (2^ · carry ⟨ _*_ ⟩ god) (tailP nat)
                          carry-god-nat)
                  (tailP (1+2* · nat)) (tailP (1+2* · nat)) (tailP (1+2* · nat) ∎)

  lemma =
    2^ · carry
                                ≡⟨ P.refl ⟩
    2^ · (0 ∞ ⋎ 1+ · carry)
                                ≊⟨ ≅-sym (⋎-map 2^ (0 ∞) (1+ · carry)) ⟩
    2^ · 0 ∞ ⋎ 2^ · 1+ · carry
                                ≊⟨ ⋎-cong (2^ · 0 ∞) (1 ∞)
                                          (pointwise 0 (2^ · 0 ∞) (1 ∞) P.refl)
                                          (2^ · 1+ · carry) (2* · 2^ · carry)
                                          (pointwise 1 (λ s → 2^ · 1+ · s)
                                                       (λ s → 2* · 2^ · s)
                                                       (λ _ → P.refl) carry) ⟩
    (1 ∞ ⋎ 2* · 2^ · carry)
                                ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module Luau.Syntax.FromJSON where

open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /)
open import Luau.Type.FromJSON using (typeFromJSON)

open import Agda.Builtin.List using (List; _∷_; [])

open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
open import FFI.Data.Bool using (true; false)
open import FFI.Data.Either using (Either; Left; Right)
open import FFI.Data.Maybe using (Maybe; nothing; just)
open import FFI.Data.Scientific using (toFloat)
open import FFI.Data.String using (String; _++_)
open import FFI.Data.Vector using (head; tail; null; empty)

args = fromString "args"
body = fromString "body"
func = fromString "func"
lokal = fromString "local"
list = fromString "list"
name = fromString "name"
type = fromString "type"
value = fromString "value"
values = fromString "values"
vars = fromString "vars"
op = fromString "op"
left = fromString "left"
right = fromString "right"

data Lookup : Set where
  _,_ : String → Value → Lookup
  nil : Lookup

lookupIn : List String → Object → Lookup
lookupIn [] obj = nil
lookupIn (key ∷ keys) obj with lookup (fromString key) obj
lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj
lookupIn (key ∷ keys) obj | just value = (key , value)

binOpFromJSON : Value → Either String BinaryOperator
binOpFromString : String → Either String BinaryOperator
varDecFromJSON : Value → Either String (VarDec maybe)
varDecFromObject : Object → Either String (VarDec maybe)
exprFromJSON : Value → Either String (Expr maybe)
exprFromObject : Object → Either String (Expr maybe)
statFromJSON : Value → Either String (Stat maybe)
statFromObject : Object → Either String (Stat maybe)
blockFromJSON : Value → Either String (Block maybe)
blockFromArray : Array → Either String (Block maybe)

binOpFromJSON (string s) = binOpFromString s
binOpFromJSON val = Left "Binary operator not a string"

binOpFromString "Add" = Right +
binOpFromString "Sub" = Right -
binOpFromString "Mul" = Right *
binOpFromString "Div" = Right /
binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")

varDecFromJSON (object arg) = varDecFromObject arg
varDecFromJSON val = Left "VarDec not an object"

varDecFromObject obj with lookup name obj | lookup type obj
varDecFromObject obj | just (string name) | nothing = Right (var name)
varDecFromObject obj | just (string name) | just Value.null = Right (var name)
varDecFromObject obj | just (string name) | just tyValue with typeFromJSON tyValue
varDecFromObject obj | just (string name) | just tyValue | Right ty = Right (var name ∈ ty)
varDecFromObject obj | just (string name) | just tyValue | Left err = Left err
varDecFromObject obj | just _ | _ = Left "AstLocal name is not a string"
varDecFromObject obj | nothing | _ = Left "AstLocal missing name"

exprFromJSON (object obj) = exprFromObject obj
exprFromJSON val = Left "AstExpr not an object"

exprFromObject obj with lookup type obj
exprFromObject obj | just (string "AstExprCall") with lookup func obj | lookup args obj
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) with head arr
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 with exprFromJSON value | exprFromJSON value2
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | Right fun | Right arg = Right (fun $ arg)
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | Left err | _ = Left err
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | just value2 | _ | Left err = Left err
exprFromObject obj | just (string "AstExprCall") | just value | just (array arr) | nothing = Left ("AstExprCall empty args")
exprFromObject obj | just (string "AstExprCall") | just value | just _ = Left ("AstExprCall args not an array")
exprFromObject obj | just (string "AstExprCall") | nothing | _  = Left ("AstExprCall missing func")
exprFromObject obj | just (string "AstExprCall") | _ | nothing  = Left ("AstExprCall missing args")
exprFromObject obj | just (string "AstExprConstantNil") = Right nil
exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue with head arr | blockFromJSON blockValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B with varDecFromJSON argValue
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Right arg = Right (function "" ⟨ arg ⟩ is B end)
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | just argValue | Right B | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | nothing | Right B = Left "Unsupported AstExprFunction empty args"
exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just blockValue | _ | Left err = Left err
exprFromObject obj | just (string "AstExprFunction") | just _ | just _ = Left "AstExprFunction args not an array"
exprFromObject obj | just (string "AstExprFunction") | nothing | _ = Left "AstExprFunction missing args"
exprFromObject obj | just (string "AstExprFunction") | _ | nothing = Left "AstExprFunction missing body"
exprFromObject obj | just (string "AstExprLocal") with lookup lokal obj
exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′))
exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r with binOpFromJSON o | exprFromJSON l | exprFromJSON r
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Right o′ | Right l′ | Right r′ = Right (binexp l′ o′ r′)
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Left err | _ | _ = Left err
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | Left err | _ = Left err
exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | _ | Left err = Left err
exprFromObject obj | just (string "AstExprBinary") | nothing | _ | _ = Left "Missing 'op' in AstExprBinary"
exprFromObject obj | just (string "AstExprBinary") | _ | nothing | _ = Left "Missing 'left' in AstExprBinary"
exprFromObject obj | just (string "AstExprBinary") | _ | _ | nothing = Left "Missing 'right' in AstExprBinary"
exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
exprFromObject obj | just _ = Left "AstExpr type not a string"
exprFromObject obj | nothing = Left "AstExpr missing type"

{-# NON_TERMINATING #-}
statFromJSON (object obj) = statFromObject obj
statFromJSON _ = Left "AstStat not an object"

statFromObject obj with lookup type obj
statFromObject obj | just(string "AstStatLocal") with lookup vars obj | lookup values obj
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) with head(arr1) | head(arr2)
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) with varDecFromJSON(x) | exprFromJSON(value)
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) | Right x′ | Right M = Right (local x′ ← M)
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) | Left err | _ = Left err
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | just(value) | _ | Left err = Left err
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(x) | nothing = Left "AstStatLocal empty values"
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | nothing | _ = Left "AstStatLocal empty vars"
statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(_) = Left "AstStatLocal values not an array"
statFromObject obj | just(string "AstStatLocal") | just(_) | just(_) = Left "AstStatLocal vars not an array"
statFromObject obj | just(string "AstStatLocal") | just(_) | nothing = Left "AstStatLocal missing values"
statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLocal missing vars"
statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value with varDecFromJSON fnName | exprFromJSON value
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Right fnVar | Right (function "" ⟨ x ⟩ is B end) = Right (function (Luau.Syntax.name fnVar) ⟨ x ⟩ is B end)
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | Left err | _ = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just fnName | just value | _ | Left err = Left err
statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
statFromObject obj | just(string "AstStatLocalFunction") | nothing | _ = Left "AstStatFunction missing name"
statFromObject obj | just(string "AstStatLocalFunction") | _ | nothing = Left "AstStatFunction missing func"
statFromObject obj | just(string "AstStatReturn") with lookup list obj
statFromObject obj | just(string "AstStatReturn") | just(array arr) with head arr
statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value with exprFromJSON value
statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value | Right M = Right (return M)
statFromObject obj | just(string "AstStatReturn") | just(array arr) | just value | Left err = Left err
statFromObject obj | just(string "AstStatReturn") | just(array arr) | nothing = Left "AstStatReturn empty list"
statFromObject obj | just(string "AstStatReturn") | just(_) = Left "AstStatReturn list not an array"
statFromObject obj | just(string "AstStatReturn") | nothing = Left "AstStatReturn missing list"
statFromObject obj | just (string ty) = Left ("TODO: Unsupported AstStat " ++ ty)
statFromObject obj | just _ = Left "AstStat type not a string"
statFromObject obj | nothing = Left "AstStat missing type"

blockFromJSON (array arr) = blockFromArray arr
blockFromJSON (object obj) with lookup type obj | lookup body obj
blockFromJSON (object obj) | just (string "AstStatBlock") | just value = blockFromJSON value
blockFromJSON (object obj) | just (string "AstStatBlock") | nothing = Left "AstStatBlock missing body"
blockFromJSON (object obj) | just (string ty) | _ = Left ("Unsupported AstBlock " ++ ty)
blockFromJSON (object obj) | just _ | _ = Left "AstStatBlock type not a string"
blockFromJSON (object obj) | nothing | _ = Left "AstStatBlock missing type"
blockFromJSON _ = Left "AstBlock not an array or AstStatBlock object"

blockFromArray arr with head arr
blockFromArray arr | nothing = Right done
blockFromArray arr | just value with statFromJSON value
blockFromArray arr | just value | Left err = Left err
blockFromArray arr | just value | Right S with blockFromArray(tail arr)
blockFromArray arr | just value | Right S | Left err = Left (err)
blockFromArray arr | just value | Right S | Right B  = Right (S ∙ B)


text:
------------------------------------------------------------------------
-- Some properties imply others
------------------------------------------------------------------------

module Relation.Binary.Consequences where

open import Relation.Binary.Core hiding (refl)
open import Relation.Nullary.Core
open import Relation.Binary.PropositionalEquality.Core
open import Data.Function
open import Data.Sum
open import Data.Product
open import Data.Empty

-- Some of the definitions can be found in the following module:

open import Relation.Binary.Consequences.Core public

trans∧irr⟶asym :
  ∀ {a} → {≈ < : Rel a} →
  Reflexive ≈ →
  Transitive < → Irreflexive ≈ < → Asymmetric <
trans∧irr⟶asym refl trans irrefl = λ x<y y<x →
  irrefl refl (trans x<y y<x)

irr∧antisym⟶asym :
  ∀ {a} → {≈ < : Rel a} →
  Irreflexive ≈ < → Antisymmetric ≈ < → Asymmetric <
irr∧antisym⟶asym irrefl antisym = λ x<y y<x →
  irrefl (antisym x<y y<x) x<y

asym⟶antisym :
  ∀ {a} → {≈ < : Rel a} →
  Asymmetric < → Antisymmetric ≈ <
asym⟶antisym asym x<y y<x = ⊥-elim (asym x<y y<x)

asym⟶irr :
  ∀ {a} → {≈ < : Rel a} →
  < Respects₂ ≈ → Symmetric ≈ →
  Asymmetric < → Irreflexive ≈ <
asym⟶irr {< = _<_} resp sym asym {x} {y} x≈y x<y = asym x<y y<x
  where
  y<y : y < y
  y<y = proj₂ resp x≈y x<y
  y<x : y < x
  y<x = proj₁ resp (sym x≈y) y<y

total⟶refl :
  ∀ {a} → {≈ ∼ : Rel a} →
  ∼ Respects₂ ≈ → Symmetric ≈ →
  Total ∼ → ≈ ⇒ ∼
total⟶refl {≈ = ≈} {∼ = ∼} resp sym total = refl
  where
  refl : ≈ ⇒ ∼
  refl {x} {y} x≈y with total x y
  ...              | inj₁ x∼y = x∼y
  ...              | inj₂ y∼x =
    proj₁ resp x≈y (proj₂ resp (sym x≈y) y∼x)

total+dec⟶dec :
  ∀ {a} → {≈ ≤ : Rel a} →
  ≈ ⇒ ≤ → Antisymmetric ≈ ≤ →
  Total ≤ → Decidable ≈ → Decidable ≤
total+dec⟶dec {≈ = ≈} {≤ = ≤} refl antisym total _≟_ = dec
  where
  dec : Decidable ≤
  dec x y with total x y
  ... | inj₁ x≤y = yes x≤y
  ... | inj₂ y≤x with x ≟ y
  ...   | yes  x≈y = yes (refl x≈y)
  ...   | no  ¬x≈y = no (λ x≤y → ¬x≈y (antisym x≤y y≤x))

tri⟶asym :
  ∀ {a} → {≈ < : Rel a} →
  Trichotomous ≈ < → Asymmetric <
tri⟶asym tri {x} {y} x<y x>y with tri x y
... | tri< _   _ x≯y = x≯y x>y
... | tri≈ _   _ x≯y = x≯y x>y
... | tri> x≮y _ _   = x≮y x<y

tri⟶irr :
  ∀ {a} → {≈ < : Rel a} →
  < Respects₂ ≈ → Symmetric ≈ →
  Trichotomous ≈ < → Irreflexive ≈ <
tri⟶irr resp sym tri = asym⟶irr resp sym (tri⟶asym tri)

tri⟶dec≈ :
  ∀ {a} → {≈ < : Rel a} →
  Trichotomous ≈ < → Decidable ≈
tri⟶dec≈ compare x y with compare x y
... | tri< _ x≉y _ = no  x≉y
... | tri≈ _ x≈y _ = yes x≈y
... | tri> _ x≉y _ = no  x≉y

tri⟶dec< :
  ∀ {a} → {≈ < : Rel a} →
  Trichotomous ≈ < → Decidable <
tri⟶dec< compare x y with compare x y
... | tri< x<y _ _ = yes x<y
... | tri≈ x≮y _ _ = no  x≮y
... | tri> x≮y _ _ = no  x≮y

subst⟶cong :
  {≈ : ∀ {a} → Rel a} →
  (∀ {a} → Reflexive {a} ≈) →
  (∀ {a} → Substitutive {a} ≈) →
  Congruential ≈
subst⟶cong {≈ = _≈_} refl subst f {x} x≈y =
  subst (λ y → f x ≈ f y) x≈y refl

cong+trans⟶cong₂ :
  {≈ : ∀ {a} → Rel a} →
  Congruential  ≈ → (∀ {a} → Transitive {a} ≈) →
  Congruential₂ ≈
cong+trans⟶cong₂ cong trans f {x = x} {v = v} x≈y u≈v =
  cong (f x) u≈v ⟨ trans ⟩ cong (flip f v) x≈y

map-NonEmpty : ∀ {I} {P Q : Rel I} →
               P ⇒ Q → NonEmpty P → NonEmpty Q
map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2019-08-07, issue #3966
--
-- Precise error location for unification problem during coverage checking.

{-# OPTIONS --cubical-compatible #-}

module _ {A : Set} where

open import Common.Equality
open import Common.List

data _⊆_ : (xs ys : List A) → Set where
  _∷ʳ_ : ∀ {xs ys} → ∀ y → _⊆_ xs ys → _⊆_ xs (y ∷ ys)
  _∷_  : ∀ {x xs y ys} → x ≡ y → _⊆_ xs ys → _⊆_ (x ∷ xs) (y ∷ ys)

⊆-trans : ∀{xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
⊆-trans rs        (y ∷ʳ ss) = y ∷ʳ ⊆-trans  rs ss
⊆-trans (y ∷ʳ rs) (s ∷ ss)  = _ ∷ʳ ⊆-trans  rs ss
⊆-trans (r ∷ rs)  (s ∷ ss)  = trans r s ∷ ⊆-trans rs ss

-- Provoke a unification error during coverage checking:

test : ∀ {x} {xs ys zs : List A} {τ : (x ∷ xs) ⊆ zs} {σ : ys ⊆ zs}
       us (ρ : us ⊆ zs) (τ' : (x ∷ xs) ⊆ us) (σ' : ys ⊆ us)
       (σ'∘ρ≡σ : ⊆-trans σ' ρ ≡ σ)
       → Set₁

test {τ = z ∷ʳ τ} {σ = z ∷ʳ σ} (y ∷ us) (.z ∷ʳ ρ) (y ∷ʳ τ') (refl ∷ σ') refl = Set
test {σ = z ∷ʳ σ} _ (refl ∷ ρ) _ (refl ∷ σ') ()
test {τ = z   ∷ʳ τ} {σ = refl ∷ σ} (y ∷ us) ρ (y ∷ʳ τ') (refl ∷ σ') σ'∘ρ≡σ = Set
test {τ = refl ∷ τ} {σ = z   ∷ʳ σ} (y ∷ us) ρ (y ∷ʳ τ') (refl ∷ σ') σ'∘ρ≡σ = Set
test {τ = refl ∷ τ} {σ = refl ∷ σ} (y ∷ us) ρ (y ∷ʳ τ') (refl ∷ σ') σ'∘ρ≡σ = Set

test (x ∷ us) ρ (refl ∷ τ') (x ∷ʳ σ') refl = Set  -- ONLY this LHS should be highlighted!
test (x ∷ us) ρ (refl ∷ τ') (refl ∷ σ') σ'∘ρ≡σ = Set
test (y ∷ us) ρ (y ∷ʳ τ') (refl ∷ σ') σ'∘ρ≡σ =  Set

-- Expected error location: 34,1-43

-- I'm not sure if there should be a case for the constructor refl,
-- because I get stuck when trying to solve the following unification
-- problems (inferred index ≟ expected index):
--   ⊆-trans (x ∷ʳ σ') ρ ≟ refl ∷ σ
-- when checking the definition of test


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

module Agda.Builtin.Word where

open import Agda.Builtin.Nat

postulate Word64 : Set
{-# BUILTIN WORD64 Word64 #-}

primitive
  primWord64ToNat   : Word64 → Nat
  primWord64FromNat : Nat → Word64

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

open import Relation.Nullary.Decidable using (toWitness; fromWitness)
open import Relation.Nullary using (yes; no)
open import Function using (_∘_)

import Data.Empty as Empty
import Data.Product as Product
import Data.Product.Properties as Productₚ
import Data.Unit as Unit
import Data.Nat.Base as Nat
import Data.Vec.Base as Vec
import Data.Vec.Properties as Vecₚ
import Data.Fin.Base as Fin
import Data.Vec.Relation.Unary.All as All

open Empty using (⊥-elim)
open Unit using (tt)
open Nat using (ℕ; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Product using (_×_; _,_; proj₁; proj₂)

import PiCalculus.Syntax
open PiCalculus.Syntax.Scoped
open import PiCalculus.Semantics
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Framing (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω

private
  variable
    n : ℕ
    i j : Fin n
    idx : Idx
    idxs : Idxs n
    γ : PreCtx n
    t : Type
    x y z : Usage idx
    Γ Θ Δ Ξ : Ctx idxs
    P Q : Scoped n

∋-frame : {idxs : Idxs n} {Γ Θ Δ Ξ Ψ : Ctx idxs} {x : Usage idx ²}
        → Γ ≔ Δ ⊗ Θ → Ξ ≔ Δ ⊗ Ψ
        → Γ ∋[ i ] x ▹ Θ
        → Ξ ∋[ i ] x ▹ Ψ

∋-frame (Γ≔ , x≔) (Ξ≔ , x'≔) (zero xyz)
  rewrite ⊗-uniqueˡ Γ≔ ⊗-idˡ | ⊗-unique Ξ≔ ⊗-idˡ
  | ∙²-uniqueˡ x≔ xyz = zero x'≔
∋-frame (Γ≔ , x≔) (Ξ≔ , x'≔) (suc x)
  rewrite ∙²-uniqueˡ x≔ ∙²-idˡ | ∙²-unique x'≔ ∙²-idˡ
  = suc (∋-frame Γ≔ Ξ≔ x)

⊢-frame : {γ : PreCtx n} {idxs : Idxs n} {Γ Δ Θ Ξ Ψ : Ctx idxs}
        → Γ ≔ Δ ⊗ Θ → Ξ ≔ Δ ⊗ Ψ
        → γ ； Γ ⊢ P ▹ Θ
        → γ ； Ξ ⊢ P ▹ Ψ

⊢-frame Γ≔ Ξ≔ 𝟘 rewrite ⊗-uniqueˡ Γ≔ ⊗-idˡ | ⊗-unique Ξ≔ ⊗-idˡ = 𝟘
⊢-frame Γ≔ Ξ≔ (ν t m μ ⊢P)
  = ν t m μ (⊢-frame {Δ = _ -, (μ , μ)} (Γ≔ , ∙²-idʳ) (Ξ≔ , ∙²-idʳ) ⊢P)
⊢-frame Γ≔ Ξ≔ ((t , ∋i) ⦅⦆ ⊢P) with ∋-⊗ ∋i | ⊢-⊗ ⊢P
⊢-frame Γ≔ Ξ≔ ((t , ∋i) ⦅⦆ ⊢P) | _ , i≔ , _ | (_ -, _) , (P≔ , x≔) =
  let iP≔           = ⊗-comp i≔ P≔ Γ≔
      _ , i'≔ , P'≔ = ⊗-assoc Ξ≔ iP≔
   in (t , ∋-frame i≔ i'≔ ∋i) ⦅⦆ ⊢-frame (P≔ , x≔) (P'≔ , x≔) ⊢P
⊢-frame Γ≔ Ξ≔ ((ti , ∋i) ⟨ tj , ∋j ⟩ ⊢P) with ∋-⊗ ∋i | ∋-⊗ ∋j | ⊢-⊗ ⊢P
⊢-frame Γ≔ Ξ≔ ((ti , ∋i) ⟨ tj , ∋j ⟩ ⊢P) | _ , i≔ , _ | _ , j≔ , _ | _ , P≔ =
  let _ , ij≔ , _    = ⊗-assoc⁻¹ i≔ j≔
      [ij]P≔         = ⊗-comp ij≔ P≔ Γ≔
      _ , ij'≔ , P'≔ = ⊗-assoc Ξ≔ [ij]P≔
      ij≔            = ⊗-comp i≔ j≔ ij≔
      _ , i'≔ , j'≔  = ⊗-assoc ij'≔ ij≔
   in (ti , ∋-frame i≔ i'≔ ∋i) ⟨ tj , ∋-frame j≔ j'≔ ∋j ⟩ ⊢-frame P≔ P'≔ ⊢P
⊢-frame Γ≔ Ξ≔ (⊢P ∥ ⊢Q) with ⊢-⊗ ⊢P | ⊢-⊗ ⊢Q
⊢-frame Γ≔ Ξ≔ (⊢P ∥ ⊢Q) | _ , P≔ | _ , Q≔ =
  let PQ≔           = ⊗-comp P≔ Q≔ Γ≔
      _ , P'≔ , Q'≔ = ⊗-assoc Ξ≔ PQ≔
   in ⊢-frame P≔ P'≔ ⊢P ∥ ⊢-frame Q≔ Q'≔ ⊢Q

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-# OPTIONS --without-K #-}
module hott.loop.level where

open import sets.nat.core
open import hott.loop.core
open import hott.level.core

Ω-level : ∀ {i n}{X : Set i}(m : ℕ){x : X}
        → h (m + n) X → h n (Ω m x)
Ω-level zero hX = hX
Ω-level (suc m) hX = Ω-level m (hX _ _)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

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

module Data.Fin where

open import Data.Nat as Nat
  using (ℕ; zero; suc; z≤n; s≤s)
  renaming ( _+_ to _N+_; _∸_ to _N∸_
           ; _≤_ to _N≤_; _≥_ to _N≥_; _<_ to _N<_; _≤?_ to _N≤?_)
open import Function
import Level
open import Relation.Nullary.Decidable
open import Relation.Binary

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

-- Fin n is a type with n elements.

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

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

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

-- A Fin-indexed variant of Fin.

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

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

-- toℕ is defined above.

-- fromℕ n = "n".

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

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

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

-- # m = "m".

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

-- raise m "n" = "m + n".

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

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

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

-- inject⋆ m "n" = "n".

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

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

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

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

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

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

-- Folds.

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

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

-- Lifts functions.

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

-- "m" + "n" = "m + n".

infixl 6 _+_

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

-- "m" - "n" = "m ∸ n".

infixl 6 _-_

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

-- m ℕ- "n" = "m ∸ n".

infixl 6 _ℕ-_

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

-- m ℕ-ℕ "n" = m ∸ n.

infixl 6 _ℕ-ℕ_

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

-- pred "n" = "pred n".

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

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

infix 4 _≤_ _<_

_≤_ : ∀ {n} → Rel (Fin n) Level.zero
_≤_ = _N≤_ on toℕ

_<_ : ∀ {n} → Rel (Fin n) Level.zero
_<_ = _N<_ on toℕ

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

-- An ordering view.

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

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


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

open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

variable
  k l m n : Nat

postulate
  max : Nat → Nat → Nat
  max-0l : max 0 n ≡ n
  max-0r : max m 0 ≡ m
  max-diag : max m m ≡ m
  max-ss : max (suc m) (suc n) ≡ suc (max m n)
  max-assoc : max (max k l) m ≡ max k (max l m)

{-# REWRITE max-0l #-}
{-# REWRITE max-0r #-}
{-# REWRITE max-diag #-}
{-# REWRITE max-ss #-}
--{-# REWRITE max-assoc #-} -- not confluent!

postulate
  _+_ : Nat → Nat → Nat
  plus-0l : 0 + n ≡ n
  plus-0r : m + 0 ≡ m
  plus-suc-l : (suc m) + n ≡ suc (m + n)
  plus-suc-r : m + (suc n) ≡ suc (m + n)
  plus-assoc : (k + l) + m ≡ k + (l + m)

{-# REWRITE plus-0l #-}
{-# REWRITE plus-0r #-}
{-# REWRITE plus-suc-l #-}
{-# REWRITE plus-suc-r #-}
{-# REWRITE plus-assoc #-}

postulate
  _*_ : Nat → Nat → Nat
  mult-0l : 0 * n ≡ 0
  mult-0r : m * 0 ≡ 0
  mult-suc-l : (suc m) * n ≡ n + (m * n)
  mult-suc-r : m * (suc n) ≡ (m * n) + m
  plus-mult-distr-l : k * (l + m) ≡ (k * l) + (k * m)
  plus-mult-distr-r : (k + l) * m ≡ (k * m) + (l * m)
  mult-assoc : (k * l) * m ≡ k * (l * m)

{-# REWRITE mult-0l #-}
{-# REWRITE mult-0r #-}
{-# REWRITE mult-suc-l #-}
{-# REWRITE mult-suc-r #-} -- requires rule plus-assoc!
--{-# REWRITE plus-mult-distr-l #-}
--{-# REWRITE plus-mult-distr-r #-}
--{-# REWRITE mult-assoc #-}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


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

module AgdaFeatureInstanceResolutionViaConstraint where

postulate A : Set
postulate y : A

Appy : (A → Set) → Set
Appy H = H y

record Foo (T : Set) : Set where field foo : T

open Foo ⦃ … ⦄ public

postulate
  S : A → Set

record Failing : Set where
  no-eta-equality

  postulate
    instance FooInstance : {R : A → Set} → Foo (Appy R)

  works1 : Appy S
  works1 = foo ⦃ FooInstance {R = S} ⦄

  fails2 : Appy S
  fails2 = foo ⦃ FooInstance {R = {!!}} ⦄
  {-
    [21] (_R_11 y) =< (S y) : Set
    _12 := λ → Foo.foo FooInstance [blocked by problem 21]
  -}

  fails3 : Appy S
  fails3 = foo

record Succeeds : Set where
  no-eta-equality

  record Bar (B : A → Set) : Set where
    no-eta-equality

  postulate
    instance BarInstance : Bar S
    instance FooInstance : {R : A → Set} ⦃ _ : Bar R ⦄ → Foo (Appy R)

  works1 : Appy S
  works1 = foo ⦃ FooInstance {R = S} ⦄

  works2 : Appy S
  works2 = foo ⦃ FooInstance {R = {!!}} ⦄

  works3 : Appy S
  works3 = foo


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

-- Construction of M-types from
-- https://arxiv.org/pdf/1504.02949.pdf
-- "Non-wellfounded trees in Homotopy Type Theory"
-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti

module Cubical.Codata.M.AsLimit.M.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv using (_≃_)
open import Cubical.Foundations.Function using (_∘_)

open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Data.Nat.Algebra

open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sum

open import Cubical.Codata.M.AsLimit.helper
open import Cubical.Codata.M.AsLimit.Container

open import Cubical.Codata.M.AsLimit.Coalg.Base

open Iso

private
  limit-collapse : ∀ {ℓ} {S : Container ℓ} (X : ℕ → Type ℓ) (l : (n : ℕ) → X n → X (suc n)) → (x₀ : X 0) → ∀ (n : ℕ) → X n
  limit-collapse X l x₀ 0 = x₀
  limit-collapse {S = S} X l x₀ (suc n) = l n (limit-collapse {S = S} X l x₀ n)

lemma11-Iso :
  ∀ {ℓ} {S : Container ℓ} (X : ℕ → Type ℓ) (l : (n : ℕ) → X n → X (suc n))
  → Iso (Σ[ x ∈ ((n : ℕ) → X n)] ((n : ℕ) → x (suc n) ≡ l n (x n)))
         (X 0)
fun (lemma11-Iso X l) (x , y) = x 0
inv (lemma11-Iso {S = S} X l) x₀ = limit-collapse {S = S} X l x₀ , (λ n → refl {x = limit-collapse {S = S} X l x₀ (suc n)})
rightInv (lemma11-Iso X l) _ = refl
leftInv (lemma11-Iso {ℓ = ℓ} {S = S} X l) (x , y) i =
  let temp = χ-prop (x 0) (fst (inv (lemma11-Iso {S = S} X l) (fun (lemma11-Iso {S = S} X l) (x , y))) , refl , (λ n → refl {x = limit-collapse {S = S} X l (x 0) (suc n)})) (x , refl , y)
  in temp i .fst , proj₂ (temp i .snd)
  where
    open AlgebraPropositionality
    open NatSection

    X-fiber-over-ℕ : (x₀ : X 0) -> NatFiber NatAlgebraℕ ℓ
    X-fiber-over-ℕ x₀ = record { Fiber = X ; fib-zero = x₀ ; fib-suc = λ {n : ℕ} xₙ → l n xₙ }

    X-section : (x₀ : X 0) → (z : Σ[ x ∈ ((n : ℕ) → X n)] (x 0 ≡ x₀) × (∀ n → (x (suc n)) ≡ l n (x n))) -> NatSection (X-fiber-over-ℕ x₀)
    X-section = λ x₀ z → record { section = fst z ; sec-comm-zero = proj₁ (snd z) ; sec-comm-suc = proj₂ (snd z) }

    Z-is-Section : (x₀ : X 0) →
      Iso (Σ[ x ∈ ((n : ℕ) → X n)] (x 0 ≡ x₀) × (∀ n → (x (suc n)) ≡ l n (x n)))
          (NatSection (X-fiber-over-ℕ x₀))
    fun (Z-is-Section x₀) (x , (z , y)) = record { section = x ; sec-comm-zero = z ; sec-comm-suc = y }
    inv (Z-is-Section x₀) x = NatSection.section x , (sec-comm-zero x , sec-comm-suc x)
    rightInv (Z-is-Section x₀) _ = refl
    leftInv (Z-is-Section x₀) (x , (z , y)) = refl

    -- S≡T
    χ-prop' : (x₀ : X 0) → isProp (NatSection (X-fiber-over-ℕ x₀))
    χ-prop' x₀ a b = SectionProp.S≡T isNatInductiveℕ (X-section x₀ (inv (Z-is-Section x₀) a)) (X-section x₀ (inv (Z-is-Section x₀) b))

    χ-prop : (x₀ : X 0) → isProp (Σ[ x ∈ ((n : ℕ) → X n) ] (x 0 ≡ x₀) × (∀ n → (x (suc n)) ≡ l n (x n)))
    χ-prop x₀ = subst isProp (sym (isoToPath (Z-is-Section x₀))) (χ-prop' x₀)

-----------------------------------------------------
-- Shifting the limit of a chain is an equivalence --
-----------------------------------------------------

-- Shift is equivalence (12) and (13) in the proof of Theorem 7
-- https://arxiv.org/pdf/1504.02949.pdf
-- "Non-wellfounded trees in Homotopy Type Theory"
-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti

-- TODO: This definition is inefficient, it should be updated to use some cubical features!
shift-iso : ∀ {ℓ} (S : Container ℓ) -> Iso (P₀ S (M S)) (M S)
shift-iso S@(A , B) =
  P₀ S (M S)
    Iso⟨ Σ-cong-iso-snd
         (λ x → iso (λ f → (λ n z → f z .fst n) , λ n i a → f a .snd n i)
                    (λ (u , q) z → (λ n → u n z) , λ n i → q n i z)
                    (λ _ → refl)
                    (λ _ → refl)) ⟩
  (Σ[ a ∈ A ] (Σ[ u ∈ ((n : ℕ) → B a → X (sequence S) n) ] ((n : ℕ) → π (sequence S) ∘ (u (suc n)) ≡ u n)))
    Iso⟨ invIso α-iso-step-5-Iso ⟩
  (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A) ] ((n : ℕ) → a (suc n) ≡ a n)) ]
        Σ[ u ∈ ((n : ℕ) → B (a .fst n) → X (sequence S) n) ]
           ((n : ℕ) → PathP (λ x → B (a .snd n x) → X (sequence S) n)
                               (π (sequence S) ∘ u (suc n))
                               (u n)))
    Iso⟨ α-iso-step-1-4-Iso-lem-12 ⟩
  M S ∎Iso
    where
      α-iso-step-5-Iso-helper0 :
        ∀ (a : (ℕ -> A))
        → (p : (n : ℕ) → a (suc n) ≡ a n)
        → (n : ℕ)
        → a n ≡ a 0
      α-iso-step-5-Iso-helper0 a p 0 = refl
      α-iso-step-5-Iso-helper0 a p (suc n) = p n ∙ α-iso-step-5-Iso-helper0 a p n

      α-iso-step-5-Iso-helper1-Iso :
        ∀ (a : ℕ -> A)
        → (p : (n : ℕ) → a (suc n) ≡ a n)
        → (u : (n : ℕ) → B (a n) → Wₙ S n)
        → (n : ℕ)
        → (PathP (λ x → B (p n x) → Wₙ S n) (πₙ S ∘ u (suc n)) (u n)) ≡
             (πₙ S ∘ (subst (\k -> B k → Wₙ S (suc n)) (α-iso-step-5-Iso-helper0 a p (suc n))) (u (suc n))
         ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n))
      α-iso-step-5-Iso-helper1-Iso  a p u n =
        PathP (λ x → B (p n x) → Wₙ S n) (πₙ S ∘ u (suc n)) (u n)
          ≡⟨ PathP≡Path (λ x → B (p n x) → Wₙ S n) (πₙ S ∘ u (suc n)) (u n) ⟩
        subst (λ k → B k → Wₙ S n) (p n) (πₙ S ∘ u (suc n)) ≡ (u n)
          ≡⟨ (λ i → transp (λ j → B (α-iso-step-5-Iso-helper0 a p n (i ∧ j)) → Wₙ S n) (~ i) (subst (λ k → B k → Wₙ S n) (p n) (πₙ S ∘ u (suc n)))
                  ≡ transp (λ j → B (α-iso-step-5-Iso-helper0 a p n (i ∧ j)) → Wₙ S n) (~ i) (u n)) ⟩
        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (subst (λ k → B k → Wₙ S n) (p n) (πₙ S ∘ u (suc n))) ≡
        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)
          ≡⟨ (λ i → sym (substComposite (λ k → B k → Wₙ S n) (p n) (α-iso-step-5-Iso-helper0 a p n) (πₙ S ∘ u (suc n))) i
                  ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)) ⟩
        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p (suc n)) (πₙ S ∘ u (suc n)) ≡
        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)
          ≡⟨ (λ i → substCommSlice (λ k → B k → Wₙ S (suc n)) (λ k → B k → Wₙ S n)
                                   (λ a x x₁ → (πₙ S) (x x₁))
                                   (α-iso-step-5-Iso-helper0 a p (suc n)) (u (suc n)) i
                  ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)) ⟩
        πₙ S ∘ subst (λ k → B k → Wₙ S (suc n)) (α-iso-step-5-Iso-helper0 a p (suc n)) (u (suc n))
          ≡
        subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n) ∎

      α-iso-step-5-Iso :
        Iso
          (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A) ] ((n : ℕ) → a (suc n) ≡ a n)) ]
            Σ[ u ∈ ((n : ℕ) → B (a .fst n) → X (sequence S) n) ]
              ((n : ℕ) → PathP (λ x → B (a .snd n x) → X (sequence S) n)
                                  (π (sequence S) ∘ u (suc n))
                                  (u n)))
            (Σ[ a ∈ A ] (Σ[ u ∈ ((n : ℕ) → B a → X (sequence S) n) ] ((n : ℕ) → π (sequence S) ∘ (u (suc n)) ≡ u n)))
      α-iso-step-5-Iso =
        Σ-cong-iso (lemma11-Iso {S = S} (λ _ → A) (λ _ x → x)) (λ a,p →
          Σ-cong-iso (pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → cong (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 (a,p .fst) (a,p .snd) n)))) λ u →
                              pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → α-iso-step-5-Iso-helper1-Iso (a,p .fst) (a,p .snd) u n)))

      α-iso-step-1-4-Iso-lem-12 :
        Iso (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A)] ((n : ℕ) → a (suc n) ≡ a n)) ]
                  (Σ[ u ∈ ((n : ℕ) → B (a .fst n) → X (sequence S) n) ]
                      ((n : ℕ) → PathP (λ x → B (a .snd n x) → X (sequence S) n)
                                          (π (sequence S) ∘ u (suc n))
                                          (u n))))
            (limit-of-chain (sequence S))
      fun α-iso-step-1-4-Iso-lem-12 (a , b) = (λ { 0 → lift tt ; (suc n) → (a .fst n) , (b .fst n)}) , λ { 0 → refl {x = lift tt} ; (suc m) i → a .snd m i , b .snd m i }
      inv α-iso-step-1-4-Iso-lem-12 x = ((λ n → (x .fst) (suc n) .fst) , λ n i → (x .snd) (suc n) i .fst) , (λ n → (x .fst) (suc n) .snd) , λ n i → (x .snd) (suc n) i .snd
      fst (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = lift tt
      fst (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = refl i
      snd (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = refl
      snd (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = c (suc n)
      leftInv α-iso-step-1-4-Iso-lem-12 (a , b) = refl

shift : ∀ {ℓ} (S : Container ℓ) -> P₀ S (M S) ≡ M S
shift S = isoToPath (shift-iso S) -- lemma 13 & lemma 12

-- Transporting along shift

in-fun : ∀ {ℓ} {S : Container ℓ} -> P₀ S (M S) -> M S
in-fun {S = S} = fun (shift-iso S)

out-fun : ∀ {ℓ} {S : Container ℓ} -> M S -> P₀ S (M S)
out-fun {S = S} = inv (shift-iso S)

-- Property of functions into M-types

lift-to-M : ∀ {ℓ} {A : Type ℓ} {S : Container ℓ}
  → (x : (n : ℕ) -> A → X (sequence S) n)
  → ((n : ℕ) → (a : A) →  π (sequence S) (x (suc n) a) ≡ x n a)
  ---------------
  → (A → M S)
lift-to-M x p a = (λ n → x n a) , λ n i → p n a i

lift-direct-M : ∀ {ℓ} {S : Container ℓ}
  → (x : (n : ℕ) → X (sequence S) n)
  → ((n : ℕ) →  π (sequence S) (x (suc n)) ≡ x n)
  ---------------
  → M S
lift-direct-M x p = x , p

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:
{-# OPTIONS --without-K #-}
module lob where
open import common
open import well-typed-syntax
open import well-typed-quoted-syntax
open import well-typed-syntax-interpreter-full

module inner (‘X’ : Typ ε) (‘f’ : Term {Γ = ε ▻ (‘□’ ‘’ ⌜ ‘X’ ⌝T)} (W ‘X’)) where
  X : Set _
  X = Typε⇓ ‘X’

  f'' : (x : Typε⇓ (‘□’ ‘’ ⌜ ‘X’ ⌝T)) → Typε▻⇓ {‘□’ ‘’ ⌜ ‘X’ ⌝T} (W ‘X’) x
  f'' = Termε▻⇓ ‘f’

  {-f : □ ‘X’ → X
  f □‘X’ = un▻-Typε▻⇓ (Termε▻⇓ ‘f’ helper)
    where helper : {!.well-typed-syntax-interpreter.Typ⇓
                     (transfer-Typ (‘□’ ‘’ ⌜ ‘X’ ⌝T))
                     .well-typed-syntax-interpreter-full.Contextε⇓!}
          helper = {!!}-}

  dummy : Typ ε
  dummy = ‘Context’

  cast : (Γv : Σ Context Typ) → Typ (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)
  cast (Γ , v) = context-pick-if {P = Typ} {Γ} (W dummy) v

  Hf : (h : Σ Context Typ) → Typ ε
  Hf h = (cast h ‘’ quote-sigma h ‘→'’ ‘X’)

  qh : Term {Γ = (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)} (W (‘Typ’ ‘’ ‘ε’))
  qh = f' w‘‘’’ x
    where
      f' : Term (W (‘Typ’ ‘’ ⌜ ε ▻ ‘Σ’ ‘Context’ ‘Typ’ ⌝c))
      f' = w→ ‘cast’ ‘'’ₐ ‘VAR₀’

      x : Term (W (‘Term’ ‘’₁ ⌜ ε ⌝c ‘’ ⌜ ‘Σ’ ‘Context’ ‘Typ’ ⌝T))
      x = (w→ ‘quote-sigma’ ‘'’ₐ ‘VAR₀’)

  h2 : Typ (ε ▻ ‘Σ’ ‘Context’ ‘Typ’)
  h2 = (W1 ‘□’ ‘’ (qh w‘‘→'’’ w ⌜ ‘X’ ⌝T))

  h : Σ Context Typ
  h = ((ε ▻ ‘Σ’ ‘Context’ ‘Typ’) , h2)

  H0 : Typ ε
  H0 = Hf h

  H : Set
  H = Term {Γ = ε} H0

  ‘H0’ : □ (‘Typ’ ‘’ ⌜ ε ⌝c)
  ‘H0’ = ⌜ H0 ⌝T

  ‘H’ : Typ ε
  ‘H’ = ‘□’ ‘’ ‘H0’

  H0' : Typ ε
  H0' = ‘H’ ‘→'’ ‘X’

  H' : Set
  H' = Term {Γ = ε} H0'

  ‘H0'’ : □ (‘Typ’ ‘’ ⌜ ε ⌝c)
  ‘H0'’ = ⌜ H0' ⌝T

  ‘H'’ : Typ ε
  ‘H'’ = ‘□’ ‘’ ‘H0'’

  toH-helper-helper : ∀ {k} → h2 ≡ k
    → □ (h2 ‘’ quote-sigma h ‘→'’ ‘□’ ‘’ ⌜ h2 ‘’ quote-sigma h ‘→'’ ‘X’ ⌝T)
    → □ (k ‘’ quote-sigma h ‘→'’ ‘□’ ‘’ ⌜ k ‘’ quote-sigma h ‘→'’ ‘X’ ⌝T)
  toH-helper-helper p x = transport (λ k → □ (k ‘’ quote-sigma h ‘→'’ ‘□’ ‘’ ⌜ k ‘’ quote-sigma h ‘→'’ ‘X’ ⌝T)) p x

  toH-helper : □ (cast h ‘’ quote-sigma h ‘→'’ ‘H’)
  toH-helper = toH-helper-helper
    {k = context-pick-if {P = Typ} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} (W dummy) h2}
    (sym (context-pick-if-refl {P = Typ} {W dummy} {h2}))
    (S₀₀W1'→ ((‘‘→'’’→w‘‘→'’’ ‘∘’ ‘‘fcomp-nd’’ ‘'’ₐ (‘s←←’ ‘‘∘’’ ‘cast-refl’ ‘‘∘’’ ⌜→'⌝ ‘'’ₐ ⌜ ‘λ∙’ ‘VAR₀’ ⌝t)) ‘∘’ ⌜←'⌝))

  ‘toH’ : □ (‘H'’ ‘→'’ ‘H’)
  ‘toH’ = ⌜→'⌝ ‘∘’ ‘‘fcomp-nd’’ ‘'’ₐ (⌜→'⌝ ‘'’ₐ ⌜ toH-helper ⌝t) ‘∘’ ⌜←'⌝

  toH : H' → H
  toH h' = toH-helper ‘∘’ h'

  fromH-helper-helper : ∀ {k} → h2 ≡ k
    → □ (‘□’ ‘’ ⌜ h2 ‘’ quote-sigma h ‘→'’ ‘X’ ⌝T ‘→'’ h2 ‘’ quote-sigma h)
    → □ (‘□’ ‘’ ⌜ k ‘’ quote-sigma h ‘→'’ ‘X’ ⌝T ‘→'’ k ‘’ quote-sigma h)
  fromH-helper-helper p x = transport (λ k → □ (‘□’ ‘’ ⌜ k ‘’ quote-sigma h ‘→'’ ‘X’ ⌝T ‘→'’ k ‘’ quote-sigma h)) p x

  fromH-helper : □ (‘H’ ‘→'’ cast h ‘’ quote-sigma h)
  fromH-helper = fromH-helper-helper
    {k = context-pick-if {P = Typ} {ε ▻ ‘Σ’ ‘Context’ ‘Typ’} (W dummy) h2}
    (sym (context-pick-if-refl {P = Typ} {W dummy} {h2}))
    (S₀₀W1'← (⌜→'⌝ ‘∘’ ‘‘fcomp-nd’’ ‘'’ₐ (⌜→'⌝ ‘'’ₐ ⌜ ‘λ∙’ ‘VAR₀’ ⌝t ‘‘∘’’ ‘cast-refl'’ ‘‘∘’’ ‘s→→’) ‘∘’ w‘‘→'’’→‘‘→'’’))
  {--}
  ‘fromH’ : □ (‘H’ ‘→'’ ‘H'’)
  ‘fromH’ = ⌜→'⌝ ‘∘’ ‘‘fcomp-nd’’ ‘'’ₐ (⌜→'⌝ ‘'’ₐ ⌜ fromH-helper ⌝t) ‘∘’ ⌜←'⌝

  fromH : H → H'
  fromH h' = fromH-helper ‘∘’ h'

  lob : □ ‘X’
  lob = fromH h' ‘'’ₐ ⌜ h' ⌝t
    where
      f' : Term {ε ▻ ‘□’ ‘’ ‘H0’} (W (‘□’ ‘’ (⌜ ‘□’ ‘’ ‘H0’ ⌝T ‘‘→'’’ ⌜ ‘X’ ⌝T)))
      f' = Conv0 {‘H0’} {‘X’} (SW1W (w∀ ‘fromH’ ‘’ₐ ‘VAR₀’))

      x : Term {ε ▻ ‘□’ ‘’ ‘H0’} (W (‘□’ ‘’ ⌜ ‘H’ ⌝T))
      x = w→ ‘quote-term’ ‘'’ₐ ‘VAR₀’

      h' : H
      h' = toH (‘λ∙’ (w→ (‘λ∙’ ‘f’) ‘'’ₐ (w→→ ‘tApp-nd’ ‘'’ₐ f' ‘'’ₐ x)))

lob : {‘X’ : Typ ε} → □ ((‘□’ ‘’ ⌜ ‘X’ ⌝T) ‘→'’ ‘X’) → □ ‘X’
lob {‘X’} ‘f’ = inner.lob ‘X’ (un‘λ∙’ ‘f’)

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
{-# OPTIONS --without-K #-}
open import Types

module J {a c} {A : Set a} (C : (x y : A) → x ≡ y → Set c) where

open import GroupoidStructure
open import PathOperations
open import PathStructure.Sigma
open import Transport

γ : {x y : A} (p : x ≡ y) →
  Id (Σ A λ y → x ≡ y) (x , refl) (y , p)
γ p = merge-path (p , tr-post _ p refl · id·p _)

justification : {x y : A} (p : x ≡ y) → C x x refl → C x y p
justification p = tr (λ z → C _ (π₁ z) (π₂ z)) (γ p)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
{-# OPTIONS --without-K #-}
module Model.RGraph where

open import Cats.Category
open import Relation.Binary using (IsEquivalence)

open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.Prelude hiding (id) renaming (_∘_ to _∘F_)
open import Util.Relation.Binary.PropositionalEquality

infixr 0 _⇒_
infix 4 _≈_
infixr 9 _∘_

record RGraph : Set₁ where
  no-eta-equality
  field
    ObjHSet : HSet 0ℓ

  open HLevel ObjHSet public using () renaming
    ( type to Obj
    ; level to Obj-IsSet
    )

  field
    eqHProp : Obj → Obj → HProp 0ℓ

  private
    module M₀ x y = HLevel (eqHProp x y)
    module M₁ {x} {y} = HLevel (eqHProp x y)

  open M₀ public using () renaming
    ( type to eq )
  open M₁ public using () renaming
    ( level to eq-IsProp )

  field
    eq-refl : ∀ x → eq x x

open RGraph public

private
  variable Γ Δ Ψ : RGraph

record _⇒_ (Γ Δ : RGraph) : Set where
  no-eta-equality
  field
    fobj : Γ .Obj → Δ .Obj
    feq : ∀ {x y} → Γ .eq x y → Δ .eq (fobj x) (fobj y)

open _⇒_ public

private
  variable f g h i : Γ ⇒ Δ

⇒Canon : (Γ Δ : RGraph) → Set
⇒Canon Γ Δ
  = Σ[ fobj ∈ (Γ .Obj → Δ .Obj) ]
      (∀ {x y} → Γ .eq x y → Δ .eq (fobj x) (fobj y))

⇒≅⇒Canon : (Γ ⇒ Δ) ≅ (⇒Canon Γ Δ)
⇒≅⇒Canon = record
  { forth = λ f → f .fobj , f .feq
  ; isIso = record
    { back = λ f → record { fobj = proj₁ f ; feq = proj₂ f }
    ; back∘forth = λ where
        record { fobj = fobj ; feq = feq } → refl
    ; forth∘back = λ f → refl
    }
  }

⇒Canon-IsSet : ∀ Γ Δ → IsSet (⇒Canon Γ Δ)
⇒Canon-IsSet Γ Δ
  = Σ-IsSet
      (→-IsSet (Δ .Obj-IsSet))
      (λ _ → ∀∙-IsSet (λ _ → ∀∙-IsSet λ _ → →-IsSet (IsProp→IsSet (Δ .eq-IsProp))))

⇒-IsSet : IsSet (Γ ⇒ Δ)
⇒-IsSet {Γ} {Δ} = ≅-pres-IsOfHLevel 2 (≅-sym ⇒≅⇒Canon) (⇒Canon-IsSet Γ Δ)

record _≈_ (f g : Γ ⇒ Δ) : Set where
  no-eta-equality
  constructor ≈⁺
  field
    ≈⁻ : ∀ x → f .fobj x ≡ g .fobj x

open _≈_ public

≈→≡Canon : ∀ {Γ Δ} {f g : Γ ⇒ Δ}
  → f ≈ g
  → ⇒≅⇒Canon .forth f ≡ ⇒≅⇒Canon .forth g
≈→≡Canon {Δ = Δ} {f} {g} (≈⁺ f≈g) = Σ-≡⁺
  ( funext f≈g
  , funext∙ (funext∙ (funext λ x≈y → Δ .eq-IsProp _ _))
  )

≈→≡ : f ≈ g → f ≡ g
≈→≡ f≈g = ≅-Injective ⇒≅⇒Canon (≈→≡Canon f≈g)

≈-isEquivalence : ∀ Γ Δ → IsEquivalence (_≈_ {Γ} {Δ})
≈-isEquivalence Γ Δ = record
  { refl = ≈⁺ (λ x → refl)
  ; sym = λ f≈g → ≈⁺ (λ x → sym (f≈g .≈⁻ x))
  ; trans = λ f≈g g≈h → ≈⁺ (λ x → trans (f≈g .≈⁻ x) (g≈h .≈⁻ x))
  }

private
  open module M₀ {Γ} {Δ}
    = IsEquivalence (≈-isEquivalence Γ Δ) public using () renaming
    ( refl to ≈-refl
    ; sym to ≈-sym
    ; trans to ≈-trans
    ; reflexive to ≈-reflexive )

id : ∀ {Γ} → Γ ⇒ Γ
id = record { fobj = λ x → x ; feq = λ x → x }

_∘_ : ∀ {Γ Δ Ψ} → Δ ⇒ Ψ → Γ ⇒ Δ → Γ ⇒ Ψ
f ∘ g = record
  { fobj = f .fobj ∘F g .fobj
  ; feq = f .feq ∘F g .feq
  }

RGraphs : Category (lsuc 0ℓ) 0ℓ 0ℓ
RGraphs = record
  { Obj = RGraph
  ; _⇒_ = _⇒_
  ; _≈_ = _≈_
  ; id = id
  ; _∘_ = _∘_
  ; equiv = ≈-isEquivalence _ _
  ; ∘-resp = λ {Γ Δ Ψ f g h i} f≈g h≈i
      → ≈⁺ (λ x → trans (f≈g .≈⁻ _) (cong (g .fobj) (h≈i .≈⁻ x)))
  ; id-r = ≈⁺ (λ x → refl)
  ; id-l = ≈⁺ (λ x → refl)
  ; assoc = ≈⁺ (λ x → refl)
  }

module RGraphs = Category RGraphs

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A data structure which keeps track of an upper bound on the number
-- of elements /not/ in a given list
------------------------------------------------------------------------

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

open import Level using (0ℓ)
open import Relation.Binary

module Data.List.Countdown (D : DecSetoid 0ℓ 0ℓ) where

open import Data.Empty
open import Data.Fin using (Fin; zero; suc; punchOut)
open import Data.Fin.Properties
  using (suc-injective; punchOut-injective)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Injection
  using (Injection; module Injection)
open import Data.List hiding (lookup)
open import Data.List.Relation.Unary.Any as Any using (here; there)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product
open import Data.Sum
open import Data.Sum.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; cong)
open PropEq.≡-Reasoning

private
  open module D = DecSetoid D
    hiding (refl) renaming (Carrier to Elem)
  open import Data.List.Membership.Setoid D.setoid

------------------------------------------------------------------------
-- Helper functions

private

  -- The /first/ occurrence of x in xs.

  first-occurrence : ∀ {xs} x → x ∈ xs → x ∈ xs
  first-occurrence x (here x≈y)           = here x≈y
  first-occurrence x (there {x = y} x∈xs) with x ≟ y
  ... | yes x≈y = here x≈y
  ... | no  _   = there $ first-occurrence x x∈xs

  -- The index of the first occurrence of x in xs.

  first-index : ∀ {xs} x → x ∈ xs → Fin (length xs)
  first-index x x∈xs = Any.index $ first-occurrence x x∈xs

  -- first-index preserves equality of its first argument.

  first-index-cong : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
                     x₁ ≈ x₂ → first-index x₁ x₁∈xs ≡ first-index x₂ x₂∈xs
  first-index-cong {x₁} {x₂} x₁∈xs x₂∈xs x₁≈x₂ = helper x₁∈xs x₂∈xs
    where
    helper : ∀ {xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
             first-index x₁ x₁∈xs ≡ first-index x₂ x₂∈xs
    helper (here x₁≈x) (here x₂≈x)           = refl
    helper (here x₁≈x) (there {x = x} x₂∈xs) with x₂ ≟ x
    ... | yes x₂≈x = refl
    ... | no  x₂≉x = ⊥-elim (x₂≉x (trans (sym x₁≈x₂) x₁≈x))
    helper (there {x = x} x₁∈xs) (here x₂≈x) with x₁ ≟ x
    ... | yes x₁≈x = refl
    ... | no  x₁≉x = ⊥-elim (x₁≉x (trans x₁≈x₂ x₂≈x))
    helper (there {x = x} x₁∈xs) (there x₂∈xs) with x₁ ≟ x | x₂ ≟ x
    ... | yes x₁≈x | yes x₂≈x = refl
    ... | yes x₁≈x | no  x₂≉x = ⊥-elim (x₂≉x (trans (sym x₁≈x₂) x₁≈x))
    ... | no  x₁≉x | yes x₂≈x = ⊥-elim (x₁≉x (trans x₁≈x₂ x₂≈x))
    ... | no  x₁≉x | no  x₂≉x = cong suc $ helper x₁∈xs x₂∈xs

  -- first-index is injective in its first argument.

  first-index-injective
    : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
      first-index x₁ x₁∈xs ≡ first-index x₂ x₂∈xs → x₁ ≈ x₂
  first-index-injective {x₁} {x₂} = helper
    where
    helper : ∀ {xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
             first-index x₁ x₁∈xs ≡ first-index x₂ x₂∈xs → x₁ ≈ x₂
    helper (here x₁≈x) (here x₂≈x)             _  = trans x₁≈x (sym x₂≈x)
    helper (here x₁≈x) (there {x = x} x₂∈xs)   _  with x₂ ≟ x
    helper (here x₁≈x) (there {x = x} x₂∈xs)   _  | yes x₂≈x = trans x₁≈x (sym x₂≈x)
    helper (here x₁≈x) (there {x = x} x₂∈xs)   () | no  x₂≉x
    helper (there {x = x} x₁∈xs) (here x₂≈x)   _  with x₁ ≟ x
    helper (there {x = x} x₁∈xs) (here x₂≈x)   _  | yes x₁≈x = trans x₁≈x (sym x₂≈x)
    helper (there {x = x} x₁∈xs) (here x₂≈x)   () | no  x₁≉x
    helper (there {x = x} x₁∈xs) (there x₂∈xs) _  with x₁ ≟ x | x₂ ≟ x
    helper (there {x = x} x₁∈xs) (there x₂∈xs) _  | yes x₁≈x | yes x₂≈x = trans x₁≈x (sym x₂≈x)
    helper (there {x = x} x₁∈xs) (there x₂∈xs) () | yes x₁≈x | no  x₂≉x
    helper (there {x = x} x₁∈xs) (there x₂∈xs) () | no  x₁≉x | yes x₂≈x
    helper (there {x = x} x₁∈xs) (there x₂∈xs) eq | no  x₁≉x | no  x₂≉x =
      helper x₁∈xs x₂∈xs (suc-injective eq)

------------------------------------------------------------------------
-- The countdown data structure

-- If counted ⊕ n is inhabited then there are at most n values of type
-- Elem which are not members of counted (up to _≈_). You can read the
-- symbol _⊕_ as partitioning Elem into two parts: counted and
-- uncounted.

infix 4 _⊕_

record _⊕_ (counted : List Elem) (n : ℕ) : Set where
  field
    -- An element can be of two kinds:
    -- ⑴ It is provably in counted.
    -- ⑵ It is one of at most n elements which may or may not be in
    --   counted. The "at most n" part is guaranteed by the field
    --   "injective".

    kind      : ∀ x → x ∈ counted ⊎ Fin n
    injective : ∀ {x y i} → kind x ≡ inj₂ i → kind y ≡ inj₂ i → x ≈ y

-- A countdown can be initialised by proving that Elem is finite.

empty : ∀ {n} → Injection D.setoid (PropEq.setoid (Fin n)) → [] ⊕ n
empty inj =
  record { kind      = inj₂ ∘ _⟨$⟩_ to
         ; injective = λ {x} {y} {i} eq₁ eq₂ → injective (begin
             to ⟨$⟩ x  ≡⟨ inj₂-injective eq₁ ⟩
             i         ≡⟨ PropEq.sym $ inj₂-injective eq₂ ⟩
             to ⟨$⟩ y  ∎)
         }
  where open Injection inj

-- A countdown can also be initialised by proving that Elem is finite.

emptyFromList : (counted : List Elem) → (∀ x → x ∈ counted) →
                [] ⊕ length counted
emptyFromList counted complete = empty record
  { to = record
    { _⟨$⟩_ = λ x → first-index x (complete x)
    ; cong  = first-index-cong (complete _) (complete _)
    }
  ; injective = first-index-injective (complete _) (complete _)
  }

-- Finds out if an element has been counted yet.

lookup : ∀ {counted n} → counted ⊕ n → ∀ x → Dec (x ∈ counted)
lookup {counted} _ x = Any.any (_≟_ x) counted

-- When no element remains to be counted all elements have been
-- counted.

lookup! : ∀ {counted} → counted ⊕ zero → ∀ x → x ∈ counted
lookup! counted⊕0 x with _⊕_.kind counted⊕0 x
... | inj₁ x∈counted = x∈counted
... | inj₂ ()

private

  -- A variant of lookup!.

  lookup‼ : ∀ {m counted} →
            counted ⊕ m → ∀ x → x ∉ counted → ∃ λ n → m ≡ suc n
  lookup‼ {suc m} counted⊕n x x∉counted = (m , refl)
  lookup‼ {zero}  counted⊕n x x∉counted =
    ⊥-elim (x∉counted $ lookup! counted⊕n x)

-- Counts a previously uncounted element.

insert : ∀ {counted n} →
         counted ⊕ suc n → ∀ x → x ∉ counted → x ∷ counted ⊕ n
insert {counted} {n} counted⊕1+n x x∉counted =
  record { kind = kind′; injective = inj }
  where
  open _⊕_ counted⊕1+n

  helper : ∀ x y i {j} →
           kind x ≡ inj₂ i → kind y ≡ inj₂ j → i ≡ j → x ≈ y
  helper _ _ _ eq₁ eq₂ refl = injective eq₁ eq₂

  kind′ : ∀ y → y ∈ x ∷ counted ⊎ Fin n
  kind′  y with y ≟ x | kind x | kind y | helper x y
  kind′  y | yes y≈x | _              | _              | _   = inj₁ (here y≈x)
  kind′  y | _       | inj₁ x∈counted | _              | _   = ⊥-elim (x∉counted x∈counted)
  kind′  y | _       | _              | inj₁ y∈counted | _   = inj₁ (there y∈counted)
  kind′  y | no  y≉x | inj₂ i         | inj₂ j         | hlp =
    inj₂ (punchOut (y≉x ∘ sym ∘ hlp _ refl refl))

  inj : ∀ {y z i} → kind′ y ≡ inj₂ i → kind′ z ≡ inj₂ i → y ≈ z
  inj {y} {z} eq₁ eq₂ with y ≟ x | z ≟ x | kind x | kind y | kind z
                         | helper x y | helper x z | helper y z
  inj ()  _   | yes _ | _     | _              | _      | _      | _ | _ | _
  inj _   ()  | _     | yes _ | _              | _      | _      | _ | _ | _
  inj _   _   | no  _ | no  _ | inj₁ x∈counted | _      | _      | _ | _ | _ = ⊥-elim (x∉counted x∈counted)
  inj ()  _   | no  _ | no  _ | inj₂ _         | inj₁ _ | _      | _ | _ | _
  inj _   ()  | no  _ | no  _ | inj₂ _         | _      | inj₁ _ | _ | _ | _
  inj eq₁ eq₂ | no  _ | no  _ | inj₂ i         | inj₂ _ | inj₂ _ | _ | _ | hlp =
    hlp _ refl refl $
      punchOut-injective {i = i} _ _ $
        (PropEq.trans (inj₂-injective eq₁) (PropEq.sym (inj₂-injective eq₂)))

-- Counts an element if it has not already been counted.

lookupOrInsert : ∀ {counted m} →
                 counted ⊕ m →
                 ∀ x → x ∈ counted ⊎
                       ∃ λ n → m ≡ suc n × x ∷ counted ⊕ n
lookupOrInsert counted⊕n x with lookup counted⊕n x
... | yes x∈counted = inj₁ x∈counted
... | no  x∉counted with lookup‼ counted⊕n x x∉counted
...   | (n , refl) = inj₂ (n , refl , insert counted⊕n x x∉counted)


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

--  Restriction Functor
module Categories.Functor.Restriction where

open import Level using (Level; _⊔_)

open import Categories.Category using (Category; _[_,_]; _[_≈_])
open import Categories.Category.Restriction using (Restriction)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level
    C : Category o ℓ e
    D : Category o′ ℓ′ e′
    E : Category o″ ℓ″ e″

record RestrictionF {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (RC : Restriction C) (RD : Restriction D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module C = Category C using (Obj)
    module RC = Restriction RC
    module RD = Restriction RD
  field
    Func : Functor C D
  open Functor Func using (F₁)
  field
    F-resp-↓ : {A B : C.Obj} → (f : C [ A , B ]) → D [ F₁ (f RC.↓) ≈ (F₁ f) RD.↓ ]

id : {RC : Restriction C} → RestrictionF RC RC
id {C = C} = record { Func = idF ; F-resp-↓ = λ f → Category.Equiv.refl C }

_∘R_ : {RC : Restriction C} {RD : Restriction D} {RE : Restriction E} → RestrictionF RD RE → RestrictionF RC RD → RestrictionF RC RE
_∘R_ {C = C} {E = E} {RC} {RD} {RE} F G = record
  { Func = Func F ∘F Func G
  ; F-resp-↓ = resp
  }
  where
    open RestrictionF
    open Category E using (_≈_; module HomReasoning)
    open HomReasoning
    module F = Functor (Func F)
    module G = Functor (Func G)
    module RC = Restriction RC
    module RD = Restriction RD
    module RE = Restriction RE
    resp : ∀ {A B : Category.Obj C} → (f : C [ A , B ]) → F.₁ (G.₁ (f RC.↓)) ≈ F.₁ (G.₁ f) RE.↓
    resp f = begin
       F.₁ (G.₁ (f RC.↓)) ≈⟨ F.F-resp-≈ (F-resp-↓ G f) ⟩
       F.₁ ((G.₁ f) RD.↓) ≈⟨ F-resp-↓ F _ ⟩
       F.₁ (G.₁ f) RE.↓ ∎

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS -v treeless.opt:20 #-}

module _ where

open import Common.Prelude
open import Common.Equality

data Dec {a} (A : Set a) : Set a where
  yes : A → Dec A
  no  : (A → ⊥) → Dec A

decEq₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} {f : A → B → C} →
           (∀ {x y z w} → f x y ≡ f z w → x ≡ z) →
           (∀ {x y z w} → f x y ≡ f z w → y ≡ w) →
           ∀ {x y z w} → Dec (x ≡ y) → Dec (z ≡ w) → Dec (f x z ≡ f y w)
decEq₂ f-inj₁ f-inj₂ (no neq)    _         = no λ eq → neq (f-inj₁ eq)
decEq₂ f-inj₁ f-inj₂  _         (no neq)   = no λ eq → neq (f-inj₂ eq)
decEq₂ f-inj₁ f-inj₂ (yes refl) (yes refl) = yes refl

main : IO Unit
main = putStrLn ""

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
-- Andreas, 2020-06-16, issue #4752
-- Disallow @-patterns in pattern synonyms.
--
-- Agda 2.5.2 implemented @-patterns and accidentially
-- allowed them in pattern synonyms.
-- However they just lead to a panic when used.

data Nat : Set where
  suc : Nat → Nat

pattern ss x = suc x@(suc _)

-- EXPECTED:
--
-- @-patterns are not allowed in pattern synonyms
-- when scope checking the declaration
--   pattern ss x = suc x@(suc _)

test : Nat → Set
test (ss x) = test x

-- WAS (from 2.5.2):
--
-- Panic: unbound variable x
-- when checking that the expression x has type Nat


text:
{-# OPTIONS --sized-types #-}

module SizedTypesRigidVarClash where

open import Common.Size renaming (↑_ to _^)

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

inc : {i j : Size} -> Nat {i} -> Nat {j ^}
inc x = suc x


text:
module StateSizedIO.GUI.WxGraphicsLib where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Size renaming (Size to AgdaSize)

open import Data.Bool.Base
open import Data.List.Base
open import Data.Nat

open import Function
open import Data.Integer

open import NativeIO

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

data GuiLev1Command  : Set where
  makeFrame          : GuiLev1Command
  setChildredLayout  : Frame   → ℕ → ℕ → ℕ → ℕ → GuiLev1Command
  makeButton         : Frame   → GuiLev1Command
  setAttribButton    : Button  → WxColor → GuiLev1Command
  addButton          : Frame   → Button → GuiLev1Command
  deleteButton       : Button → GuiLev1Command
  drawBitmap         : DC      → Bitmap → Point → Bool → GuiLev1Command
  repaint            : Frame   → GuiLev1Command
  bitmapGetWidth     : Bitmap  → GuiLev1Command
  putStrLn           : String  → GuiLev1Command

GuiLev1Response : GuiLev1Command → Set
GuiLev1Response makeFrame           = Frame
GuiLev1Response (makeButton _)      = Button
GuiLev1Response (bitmapGetWidth _)  = ℤ
GuiLev1Response _                   = Unit

GuiLev1Interface : IOInterface
Command   GuiLev1Interface = GuiLev1Command
Response  GuiLev1Interface = GuiLev1Response

GuiLev2State : Set₁
GuiLev2State = VarList

data GuiLev2Command (s :  GuiLev2State) : Set₁ where
  level1C           : GuiLev1Command → GuiLev2Command s
  createVar         : {A : Set} → A → GuiLev2Command s
  setButtonHandler  : Button → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → GuiLev2Command s
  setTimer          : Frame → ℤ → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → GuiLev2Command s
  setKeyHandler     : Button
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → List (prod s → IO GuiLev1Interface ∞ (prod s))
                      → GuiLev2Command s
  setOnPaint        : Frame
                     → List (prod s → DC → Rect → IO GuiLev1Interface ∞ (prod s))
                     → GuiLev2Command s

GuiLev2Response : (s : GuiLev2State) → GuiLev2Command s → Set
GuiLev2Response _ (level1C c)         = GuiLev1Response c
GuiLev2Response _ (createVar {A} a)   = Var A
GuiLev2Response _ (setTimer fra x p)  = Timer
GuiLev2Response _ _                   = Unit

GuiLev2Next : (s : GuiLev2State) → (c : GuiLev2Command s)
              → GuiLev2Response s c
              → GuiLev2State
GuiLev2Next s (createVar {A} a) var = addVar A var s
GuiLev2Next s _  _                  = s

GuiLev2Interface : IOInterfaceˢ
Stateˢ     GuiLev2Interface = GuiLev2State
Commandˢ   GuiLev2Interface = GuiLev2Command
Responseˢ  GuiLev2Interface = GuiLev2Response
nextˢ      GuiLev2Interface = GuiLev2Next

translateLev1Local : (c : GuiLev1Command) → NativeIO (GuiLev1Response c)
translateLev1Local makeFrame              = nativeNewFrame "dummy title"
translateLev1Local (setChildredLayout win a b c d) = nativeSetChildredLayout win a b c d
translateLev1Local (makeButton fra)       = nativeMakeButton fra "dummy button label"
translateLev1Local (deleteButton bt)      = nativeDeleteButton bt
translateLev1Local (addButton fra bt)     = nativeAddButton fra bt
translateLev1Local (setAttribButton bt col) = nativeSetColorButton bt col
translateLev1Local (drawBitmap dc bm p b) = nativeDrawBitmap dc bm p b
translateLev1Local (repaint fra)          = nativeRepaint fra
translateLev1Local (bitmapGetWidth b)     = nativeBitmapGetWidth b
translateLev1Local (putStrLn s)           = nativePutStrLn s

translateLev1 : {A : Set} → IO GuiLev1Interface ∞ A → NativeIO A
translateLev1 = translateIO translateLev1Local

translateLev1List : {A : Set} → List (IO GuiLev1Interface ∞ A) → List (NativeIO A)
translateLev1List l = map translateLev1 l

translateLev2Local : (s : GuiLev2State)
                          → (c : GuiLev2Command s)
                          → NativeIO (GuiLev2Response s c)
translateLev2Local s (level1C c) = translateLev1Local c

translateLev2Local s (createVar {A} a)   = nativeNewVar {A} a
translateLev2Local s (setButtonHandler bt proglist)
    = nativeSetButtonHandler bt
            (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglist))

translateLev2Local s (setTimer fra interv proglist)
    = nativeSetTimer fra interv (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglist))

translateLev2Local s (setKeyHandler bt proglistRight proglistLeft proglistUp proglistDown)
    =  nativeSetKeyHandler bt
           (λ key -> case (showKey key) of λ
                 { "Right" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistRight))
                 ; "Left" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistLeft))
                 ; "Up" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistUp))
                 ; "Down" → (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglistDown))
                 ; _  → nativeReturn unit
                 } )

translateLev2Local s (setOnPaint fra proglist)
    = nativeSetOnPaint fra (λ dc rect → (dispatchList s
         (map (λ prog aa → translateLev1 (prog aa dc rect)) proglist)))

translateLev2 : {s : GuiLev2State} → {A : Set}
                     → IOˢ GuiLev2Interface ∞ (λ _ → A) s → NativeIO A
translateLev2 = translateIOˢ {I = GuiLev2Interface} translateLev2Local

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda