text:
------------------------------------------------------------------------
-- An up-to technique for CCS
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude hiding (step-→)

module Bisimilarity.Weak.Up-to.CCS {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

open import Bisimilarity.Weak.CCS
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
open import Indexed-container hiding (⟨_⟩)
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity.Weak CCS
open import Bisimilarity.Weak.Up-to CCS
import Labelled-transition-system.Equational-reasoning-instances CCS
  as Dummy

-- Up to (non-degenerate) context for CCS (for polyadic, coinductive
-- contexts).

Up-to-context : Trans₂ ℓ (Proc ∞)
Up-to-context R (p , q) =
  ∃ λ n →
  ∃ λ (C : Context ∞ n) →
  Non-degenerate ∞ C
    ×
  ∃ λ ps →
  ∃ λ qs →
  p ≡ C [ ps ]
    ×
  q ≡ C [ qs ]
    ×
  ∀ x → R (ps x , qs x)

-- Up to context is monotone.

up-to-context-monotone : Monotone Up-to-context
up-to-context-monotone R⊆S =
  Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $
  Σ-map id (R⊆S ∘_)

-- Up to context is size-preserving.

up-to-context-size-preserving : Size-preserving Up-to-context
up-to-context-size-preserving =
  _⇔_.from (monotone→⇔ up-to-context-monotone)
  (λ where
     (_ , C , D , ps , qs , refl , refl , ps∼qs) →

      C [ ps ]  ∼⟨ D [ ps∼qs ]-cong ⟩■
      C [ qs ])

-- Note that up to context is not compatible (assuming that Name is
-- inhabited).
--
-- This counterexample is a minor variant of one due to Pous and
-- Sangiorgi, who state that up to context is contained in a larger
-- function that is compatible for another, "one-sided" step function
-- (see Section 6.5.3 in "Enhancements of the bisimulation proof
-- method").

¬-up-to-context-compatible : Name → ¬ Compatible Up-to-context
¬-up-to-context-compatible x comp = contradiction
  where
  a = x , true

  data R₀ : Rel₂ ℓ (Proc ∞) where
    base : R₀ (τ ∙ (a ∙) , a ∙)

  R : Rel₂ ℓ (Proc ∞)
  R = R₀ ⁼

  !τa[R]!a : Up-to-context R (! τ ∙ (a ∙) , ! a ∙)
  !τa[R]!a =
      1
    , ! hole fzero
    , ! hole
    , (λ _ → τ ∙ (a ∙))
    , (λ _ → a ∙)
    , refl
    , refl
    , (λ _ → inj₁ base)

  !a[τ]⇒̂→≡ : ∀ {P} → ! a ∙ [ τ ]⇒̂ P → P ≡ ! a ∙
  !a[τ]⇒̂→≡ (non-silent ¬s _)                 = ⊥-elim $ ¬s _
  !a[τ]⇒̂→≡ (silent _ done)                   = refl
  !a[τ]⇒̂→≡ (silent _ (step {μ = μ} s !a⟶ _)) = ⊥-elim $ name≢τ (
                                                 name a  ≡⟨ !-only ·-only !a⟶ ⟩
                                                 μ       ≡⟨ silent≡τ s ⟩∎
                                                 τ       ∎)

  drop-[] : ∀ {P Q S} →
            Up-to-context R (P ∣ Q , ! S) → R (P ∣ Q , ! S)
  drop-[] (_ , hole i , _ , _ , _ , P∣Q≡Ps[i] , !S≡Qs[i] , PsRQs) =
    subst R (cong₂ _,_ (sym P∣Q≡Ps[i]) (sym !S≡Qs[i])) (PsRQs i)

  drop-[] (_ , ∅        , _ , _ , _ , () , _)
  drop-[] (_ , _ ∣ _    , _ , _ , _ , _  , () , _)
  drop-[] (_ , _ ⊕ _    , _ , _ , _ , () , _)
  drop-[] (_ , _ · _    , _ , _ , _ , () , _)
  drop-[] (_ , ⟨ν _ ⟩ _ , _ , _ , _ , () , _)
  drop-[] (_ , ! _      , _ , _ , _ , () , _)

  R⊆StepR : R ⊆ ⟦ StepC ⟧ R
  R⊆StepR (inj₁ base) = ⟨ lr , rl ⟩
    where
    lr :
      ∀ {P μ} →
      τ ∙ (a ∙) [ μ ]⟶ P →
      ∃ λ Q → a ∙ [ μ ]⇒̂ Q × R (P , Q)
    lr action =
        _
      , (a ∙  ■)
      , inj₂ refl

    rl :
      ∀ {Q μ} →
      a ∙ [ μ ]⟶ Q →
      ∃ λ P → τ ∙ (a ∙) [ μ ]⇒̂ P × R (P , Q)
    rl action =
        _
      , (τ ∙ (a ∙)  →⟨ ⟶: action ⟩
         a ∙        →⟨ ⟶: action ⟩■
         ∅)
      , inj₂ refl

  R⊆StepR {P , _} (inj₂ refl) =
    ⟨ Σ-map id (Σ-map id inj₂)         ∘ lr
    , Σ-map id (Σ-map id (inj₂ ∘ sym)) ∘ lr
    ⟩
    where
    lr : ∀ {P′ μ} →
         P [ μ ]⟶ P′ →
         ∃ λ Q′ → P [ μ ]⇒̂ Q′ × P′ ≡ Q′
    lr P⟶P′ = _ , ⟶→⇒̂ P⟶P′ , refl

  -- Note the use of compatibility in [R]⊆Step[S].

  [R]⊆Step[R] : Up-to-context R ⊆ ⟦ StepC ⟧ (Up-to-context R)
  [R]⊆Step[R] =
    Up-to-context R              ⊆⟨ up-to-context-monotone (λ {x} → R⊆StepR {x}) ⟩
    Up-to-context (⟦ StepC ⟧ R)  ⊆⟨ comp ⟩∎
    ⟦ StepC ⟧ (Up-to-context R)  ∎

  contradiction : ⊥
  contradiction =                                                       $⟨ !τa[R]!a ⟩
    Up-to-context R (! τ ∙ (a ∙) , ! a ∙)                               ↝⟨ [R]⊆Step[R] ⟩
    ⟦ StepC ⟧ (Up-to-context R) (! τ ∙ (a ∙) , ! a ∙)                   ↝⟨ (λ s → StepC.left-to-right s (replication (par-right action))) ⟩
    (∃ λ P → ! a ∙ [ τ ]⇒̂ P × Up-to-context R (! τ ∙ (a ∙) ∣ a ∙ , P))  ↝⟨ (λ { (_ , !a⟶ , hyp) →
                                                                                subst (Up-to-context R ∘ (_ ,_)) (!a[τ]⇒̂→≡ !a⟶) hyp }) ⟩
    Up-to-context R (! τ ∙ (a ∙) ∣ a ∙ , ! a ∙)                         ↝⟨ drop-[] ⟩
    R (! τ ∙ (a ∙) ∣ a ∙ , ! a ∙)                                       ↝⟨ [ (λ ()) , (λ ()) ] ⟩□
    ⊥                                                                   □

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- Andreas, 2016-11-11 issue #2301,
-- reported by stedolan and fredrikNorvallForsberg:
-- compareTelescope ignored relevance.
-- Faulty behavior probably existed since 2011.

module Issue2301 where

data Box (A : Set) : Set where
  wrap : A → Box A

weird : ∀ A → .A → Box A
weird A = wrap

-- SHOULD FAIL with error:
-- A → Box A !=< .A → Box A
-- when checking that the expression wrap has type .A → Box A

-- WAS: checked.

-- Since the first argument to wrap is not actually irrelevant,
-- this lets us write a function that discards irrelevance annotations:

make-relevant : ∀ {A} → .A → A
make-relevant a = unwrap (weird a)
  where
    unwrap : ∀ {A} → Box A → A
    unwrap (wrap a) = a

-- or proves things we shouldn't:

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

data Bool : Set where
  tt ff : Bool

absurd : {X : Set} → X
absurd {X} = different same
  where
    different : weird tt ≡ weird ff → X
    different ()

    irr-eq : ∀ {A B : Set} {x y : A} (f : .A → B) → f x ≡ f y
    irr-eq f = refl

    same : weird tt ≡ weird ff
    same = irr-eq weird

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
mutual
  _ : Set
  _ : Set → Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Dipsy.Example.CLL where

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; _∷_; [])
open import Dipsy.Polarity using (Polarity; flip) renaming (pos to +; neg to -)

mutual
  Op₀ : (r : Polarity) → Set
  Op₀ r = Op [] r
  Op₁ : (a r : Polarity) → Set
  Op₁ a r = Op (a ∷ []) r
  Op₂ : (a₁ a₂ r : Polarity) → Set
  Op₂ a₁ a₂ r = Op (a₁ ∷ a₂ ∷ []) r

  data Op : {n : ℕ} → Vec Polarity n → Polarity → Set where
    ″⊥″ : Op₀ -
    ″𝟏″ : Op₀ +
    ″⊤″ : Op₀ -
    ″𝟎″ : Op₀ +
    ″¬″ : {p : Polarity} → Op₁ (flip p) p
    ″⅋″ : Op₂ - - -
    ″⊗″ : Op₂ + + +
    ″&″ : Op₂ - - -
    ″⊕″ : Op₂ + + +

open import Dipsy.Base Op Op

pattern ⊥ = op ″⊥″ []
pattern 𝟏 = op ″𝟏″ []
pattern ⊤ = op ″⊤″ []
pattern 𝟎 = op ″𝟎″ []
pattern ¬_ A = op ″¬″ (A ∷ [])
pattern _⅋_ A B = op ″⅋″ (A ∷ B ∷ [])
pattern _⊗_ A B = op ″⊗″ (A ∷ B ∷ [])
pattern _&_ A B = op ″&″ (A ∷ B ∷ [])
pattern _⊕_ A B = op ″⊕″ (A ∷ B ∷ [])

max_stars_repo_name: wenkokke/Dipsy

max_issues_repo_name: wenkokke/dipsy

max_forks_repo_name: wenkokke/dipsy


text:
-- Andreas, 2016-09-28, solve _ <= lzero.

-- {-# OPTIONS -v tc.conv.nat:40 #-}

open import Common.Level

data C : Set₁ where
  c : Set _ → C  -- This meta should be solved to lzero.

-- ERROR WAS:
-- Failed to solve the following constraints:
--   [0] lsuc _0 =< lsuc lzero
-- REASON:
-- Non-canonical lzero in level constraint solver


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Coalgebra where

-- Co-algebras of a Functor
open import Level
open import Function using (_$_)

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; Endofunctor)

record F-Coalgebra {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) : Set (o ⊔ ℓ) where
  open Category C
  field
    A : Obj
    α : A ⇒ Functor.F₀ F A

open F-Coalgebra

-- Given a F-Coalgebra F, one can apply F to it to obtain an new 'iterated' F-Coalgebra
iterate : ∀ {o ℓ e} {C : Category o ℓ e} {F : Endofunctor C} → F-Coalgebra F → F-Coalgebra F
iterate {F = F} F-alg = record { A = Functor.F₀ F $ A F-alg ; α = Functor.F₁ F $ α F-alg }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Data.Quiver where

-- A Quiver, also known as a multidigraph, is the "underlying graph" of
-- a category. Note how a Quiver has a *setoid* of edges.

open import Level
open import Relation.Binary using (Rel; IsEquivalence; Setoid)
import Relation.Binary.Reasoning.Setoid as EqR

-- a Quiver has vertices Obj and edges _⇒_, where edges form a setoid over _≈_.
record Quiver o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  infix 4 _≈_ _⇒_

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

  setoid : {A B : Obj} → Setoid _ _
  setoid {A} {B} = record
    { Carrier       = A ⇒ B
    ; _≈_           = _≈_
    ; isEquivalence = equiv
    }

  module Equiv {A B : Obj} = IsEquivalence (equiv {A} {B})
  module EdgeReasoning {A B : Obj} = EqR (setoid {A} {B})


text:
------------------------------------------------------------------------
-- Some definitions related to Dec
------------------------------------------------------------------------

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

module Dec where

open import Logical-equivalence hiding (_∘_)
open import Prelude

private
  variable
    a   : Level
    A B : Type a

-- A map function for Dec.

Dec-map : A ⇔ B → Dec A → Dec B
Dec-map A⇔B = ⊎-map to (_∘ from)
  where
  open _⇔_ A⇔B

-- Dec preserves logical equivalences.

Dec-preserves : A ⇔ B → Dec A ⇔ Dec B
Dec-preserves A⇔B = record
  { to   = Dec-map A⇔B
  ; from = Dec-map (inverse A⇔B)
  }

-- If A and B are decided, then A × B is.

Dec-× : Dec A → Dec B → Dec (A × B)
Dec-× =
  [ (λ a → [ (λ b → yes (a , b))
           , (λ ¬b → no (¬b ∘ proj₂))
           ])
  , (λ ¬a _ → no (¬a ∘ proj₁))
  ]

-- If A and B are decided, then A ⊎ B is.

Dec-⊎ : Dec A → Dec B → Dec (A ⊎ B)
Dec-⊎ =
  [ (λ a _ → yes (inj₁ a))
  , (λ ¬a →
       [ (λ b → yes (inj₂ b))
       , (λ ¬b → no [ ¬a , ¬b ])
       ])
  ]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module System.Environment.Primitive where

open import IO.Primitive
open import Agda.Builtin.String
open import Agda.Builtin.List
open import Agda.Builtin.Unit
import Foreign.Haskell as FFI

open import System.FilePath.Posix

postulate

  getArgs           : IO (List String)
  getProgName       : IO String
  getExecutablePath : IO AbsolutePath
  lookupEnv         : String → IO (FFI.Maybe String)
  setEnv            : String → String → IO ⊤
  unsetEnv          : String → IO ⊤
  withArgs          : ∀ {a} {A : Set a} → List String → IO A → IO A
  withProgName      : ∀ {a} {A : Set a} → String → IO A → IO A
  getEnvironment    : IO (List (FFI.Pair String String))

{-# FOREIGN GHC import qualified System.Environment as SE                                        #-}
{-# FOREIGN GHC import Data.Text                                                                 #-}
{-# FOREIGN GHC import Data.Function                                                             #-}
{-# COMPILE GHC getArgs           = fmap (fmap pack) SE.getArgs                                  #-}
{-# COMPILE GHC getProgName       = fmap pack SE.getProgName                                     #-}
{-# COMPILE GHC getExecutablePath = SE.getExecutablePath                                         #-}
{-# COMPILE GHC lookupEnv         = fmap (fmap pack) . SE.lookupEnv . unpack                     #-}
{-# COMPILE GHC setEnv            = SE.setEnv `on` unpack                                        #-}
{-# COMPILE GHC unsetEnv          = SE.unsetEnv . unpack                                         #-}
{-# COMPILE GHC withArgs          = \ _ _ -> SE.withArgs . fmap unpack                           #-}
{-# COMPILE GHC withProgName      = \ _ _ -> SE.withProgName . unpack                            #-}
{-# COMPILE GHC getEnvironment    = fmap (fmap (\ (a, b) -> (pack a, pack b))) SE.getEnvironment #-}

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module bool-thms where

open import bool
open import eq
open import sum
open import empty
open import level

~~-elim : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim tt = refl
~~-elim ff = refl

&&-idem : ∀ {b} → b && b ≡ b
&&-idem{tt} = refl
&&-idem{ff} = refl

||-idem : ∀{b} → b || b ≡ b
||-idem{tt} = refl
||-idem{ff} = refl

||≡ff₁ : ∀ {b1 b2} → b1 || b2 ≡ ff → ff ≡ b1
||≡ff₁ {ff} p = refl
||≡ff₁ {tt} p = sym p

||≡ff₂ : ∀ {b1 b2} → b1 || b2 ≡ ff → b2 ≡ ff
||≡ff₂ {tt} ()
||≡ff₂ {ff}{tt} ()
||≡ff₂ {ff}{ff} p = refl

||-tt : ∀ (b : 𝔹) → b || tt ≡ tt
||-tt tt = refl
||-tt ff = refl

||-cong₁ : ∀ {b1 b1' b2} → b1 ≡ b1' → b1 || b2 ≡ b1' || b2
||-cong₁ refl = refl

||-cong₂ : ∀ {b1 b2 b2'} → b2 ≡ b2' → b1 || b2 ≡ b1 || b2'
||-cong₂ p rewrite p = refl

ite-same : ∀{ℓ}{A : Set ℓ} →
           ∀(b : 𝔹) (x : A) →
           (if b then x else x) ≡ x
ite-same tt x = refl
ite-same ff x = refl

ite-arg : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (f : A → B)(b : 𝔹)(x y : A) → (f (if b then x else y)) ≡ (if b then f x else f y)
ite-arg f tt x y = refl
ite-arg f ff x y = refl

𝔹-contra : ff ≡ tt → ∀{ℓ} {P : Set ℓ} → P
𝔹-contra ()

||-split : ∀ {b b' : 𝔹} → b || b' ≡ tt → b ≡ tt ⊎ b' ≡ tt
||-split{tt}{tt} p = inj₁ refl
||-split{tt}{ff} p = inj₁ refl
||-split{ff}{tt} p = inj₂ refl
||-split{ff}{ff} ()

𝔹-dec : ∀ (b : 𝔹) → b ≡ tt ⊎ b ≡ ff
𝔹-dec tt = inj₁ refl
𝔹-dec ff = inj₂ refl

&&-snd : {p1 p2 : 𝔹} → p1 && p2 ≡ tt → p2 ≡ tt
&&-snd{tt} p = p
&&-snd{ff} ()

&&-fst : {p1 p2 : 𝔹} → p1 && p2 ≡ tt → p1 ≡ tt
&&-fst{tt} p = refl
&&-fst{ff} ()

&&-combo : {p1 p2 : 𝔹} → p1 ≡ tt → p2 ≡ tt → p1 && p2 ≡ tt
&&-combo{tt} pr1 pr2 = pr2
&&-combo{ff} pr1 pr2 = 𝔹-contra pr1

&&-ff : ∀(b : 𝔹) → b && ff ≡ ff
&&-ff tt = refl
&&-ff ff = refl

ff≡tt : ff ≡ tt → ⊥ {lzero}
ff≡tt ()

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

module Data.Bits.Count where

open import Type hiding (★)
open import Data.Two hiding (_==_)
open import Data.Bits
open import Data.Bits.OperationSyntax
import Data.Bits.Search as Search
open Search.SimpleSearch
open import Data.Bits.Sum

open import Data.Bool.Properties using (not-involutive)
open import Data.Zero using (𝟘; 𝟘-elim)
import Data.Fin as Fin
open Fin using (Fin; zero; suc; #_; inject₁; inject+; raise) renaming (_+_ to _+ᶠ_)

open import Data.Maybe.NP

open import Data.Nat.NP hiding (_==_)
open import Data.Nat.Properties
import Data.Vec.NP as V
open V hiding (rewire; rewireTbl; sum) renaming (map to vmap; swap to vswap)

open import Data.Product using (_×_; _,_; uncurry; proj₁; proj₂)

open import Function.NP

import Relation.Binary.PropositionalEquality.NP as ≡
open ≡

#⟨_⟩ : ∀ {n} → (Bits n → 𝟚) → ℕ
#⟨ pred ⟩ = sum (𝟚▹ℕ ∘ pred)

-- #-ext
#-≗ : ∀ {n} (f g : Bits n → 𝟚) → f ≗ g → #⟨ f ⟩ ≡ #⟨ g ⟩
#-≗ f g f≗g = sum-≗ (𝟚▹ℕ ∘ f) (𝟚▹ℕ ∘ g) (λ x → ≡.cong 𝟚▹ℕ (f≗g x))

#-comm : ∀ {n} (pad : Bits n) (f : Bits n → 𝟚) → #⟨ f ⟩ ≡ #⟨ f ∘ _⊕_ pad ⟩
#-comm pad f = sum-comm pad (𝟚▹ℕ ∘ f)

#-bij : ∀ {n} f (g : Bits n → 𝟚) → #⟨ g ∘ eval f ⟩ ≡ #⟨ g ⟩
#-bij f g = sum-bij f (𝟚▹ℕ ∘ g)

#-⊕ : ∀ {c} (bs : Bits c) (f : Bits c → 𝟚) → #⟨ f ⟩ ≡ #⟨ f ∘ _⊕_ bs ⟩
#-⊕ = #-comm

#-const : ∀ n b → #⟨ (λ (_ : Bits n) → b) ⟩ ≡ ⟨2^ n * 𝟚▹ℕ b ⟩
#-const n b = sum-const n (𝟚▹ℕ b)

#never≡0 : ∀ n → #⟨ never n ⟩ ≡ 0
#never≡0 = sum-const0≡0

#always≡2^_ : ∀ n → #⟨ always n ⟩ ≡ 2^ n
#always≡2^ n = sum-const n 1

#-dist : ∀ {n} (f₀ f₁ : Bits n → 𝟚) → sum (λ x → 𝟚▹ℕ (f₀ x) + 𝟚▹ℕ (f₁ x)) ≡ #⟨ f₀ ⟩ + #⟨ f₁ ⟩
#-dist f₀ f₁ = sum-dist (𝟚▹ℕ ∘ f₀) (𝟚▹ℕ ∘ f₁)

#-+ : ∀ {m n} (f : Bits (m + n) → 𝟚) →
                 #⟨ f ⟩ ≡ sum {m} (λ xs → #⟨ (λ ys → f (xs ++ ys)) ⟩ )
#-+ {m} {n} f = sum-+ {m} {n} (𝟚▹ℕ ∘ f)

#-# : ∀ {m n} (f : Bits (m + n) → 𝟚) →
                          sum {m} (λ xs → #⟨ (λ ys → f (xs ++ ys)) ⟩)
                        ≡ sum {n} (λ ys → #⟨ (λ (xs : Bits m) → f (xs ++ ys)) ⟩)
#-# {m} {n} f = sum-sum {m} {n} (𝟚▹ℕ ∘ f)

#-swap : ∀ {m n} (f : Bits (m + n) → 𝟚) → #⟨ f ∘ vswap n {m} ⟩ ≡ #⟨ f ⟩
#-swap {m} {n} f = sum-swap {m} {n} (𝟚▹ℕ ∘ f)

#⟨==_⟩ : ∀ {n} (xs : Bits n) → #⟨ _==_ xs ⟩ ≡ 1
#⟨== [] ⟩ = refl
#⟨==_⟩ {suc n} (true ∷ xs)  rewrite #never≡0 n | #⟨== xs ⟩ = refl
#⟨==_⟩ {suc n} (false ∷ xs) rewrite #never≡0 n | #⟨== xs ⟩ = refl

≗-cong-# : ∀ {n} (f g : Bits n → 𝟚) → f ≗ g → #⟨ f ⟩ ≡ #⟨ g ⟩
≗-cong-# f g f≗g = sum-≗ _ _ (cong 𝟚▹ℕ ∘ f≗g)

-- #-+ : ∀ {n a b} (f : Bits (suc n) → 𝟚) → #⟨ f ∘ 0∷_ ⟩ ≡ a → #⟨ f ∘ 1∷_ ⟩ ≡ b → #⟨ f ⟩ ≡ a + b
-- #-+ f f0 f1 rewrite f0 | f1 = refl

#-take-drop : ∀ m n (f : Bits m → 𝟚) (g : Bits n → 𝟚)
                → #⟨ (f ∘ take m) |∧| (g ∘ drop m) ⟩ ≡ #⟨ f ⟩ * #⟨ g ⟩
#-take-drop zero n f g with f []
... | true rewrite ℕ°.+-comm #⟨ g ⟩ 0 = refl
... | false = #never≡0 n
#-take-drop (suc m) n f g
  rewrite ≗-cong-# ((f ∘ take (suc m)) |∧| (g ∘ drop (suc m)) ∘ 0∷_)
                   ((f ∘ 0∷_ ∘ take m) |∧| (g ∘ drop m))
                     (λ x → cong₂ (λ x y → f x ∧ g y) (take-∷ m 0' x) (drop-∷ m 0' x))
        | #-take-drop m n (f ∘ 0∷_) g
        | ≗-cong-# ((f ∘ take (suc m)) |∧| (g ∘ drop (suc m)) ∘ 1∷_)
                   ((f ∘ 1∷_ ∘ take m) |∧| (g ∘ drop m))
                     (λ x → cong₂ (λ x y → f x ∧ g y) (take-∷ m 1' x) (drop-∷ m 1' x))
        | #-take-drop m n (f ∘ 1∷_) g
          = sym (proj₂ ℕ°.distrib #⟨ g ⟩ #⟨ f ∘ 0∷_ ⟩ #⟨ f ∘ 1∷_ ⟩)

#-drop-take : ∀ m n (f : Bits n → 𝟚) (g : Bits m → 𝟚)
                  → #⟨ (f ∘ drop m) |∧| (g ∘ take m) ⟩ ≡ #⟨ f ⟩ * #⟨ g ⟩
#-drop-take m n f g =
              #⟨ (f ∘ drop m) |∧| (g ∘ take m) ⟩
            ≡⟨ ≗-cong-# ((f ∘ drop m) |∧| (g ∘ take m)) ((g ∘ take m) |∧| (f ∘ drop m)) (λ x → Bool°.+-comm (f (drop m x)) _) ⟩
              #⟨ (g ∘ take m) |∧| (f ∘ drop m) ⟩
            ≡⟨ #-take-drop m n g f ⟩
              #⟨ g ⟩ * #⟨ f ⟩
            ≡⟨ ℕ°.*-comm #⟨ g ⟩ _ ⟩
              #⟨ f ⟩ * #⟨ g ⟩
            ∎
      where open ≡-Reasoning

#-take : ∀ m n (f : Bits m → 𝟚) → #⟨ f ∘ take m {n} ⟩ ≡ 2^ n * #⟨ f ⟩
#-take m n f = #⟨ f ∘ take m {n} ⟩
             ≡⟨ #-drop-take m n (always n) f ⟩
               #⟨ always n ⟩ * #⟨ f ⟩
             ≡⟨ cong (flip _*_ #⟨ f ⟩) (#always≡2^ n) ⟩
               2^ n * #⟨ f ⟩
             ∎
      where open ≡-Reasoning

#-drop : ∀ m n (f : Bits m → 𝟚) → #⟨ f ∘ drop n ⟩ ≡ 2^ n * #⟨ f ⟩
#-drop m n f = #⟨ f ∘ drop n ⟩
             ≡⟨ #-take-drop n m (always n) f ⟩
               #⟨ always n ⟩ * #⟨ f ⟩
             ≡⟨ cong (flip _*_ #⟨ f ⟩) (#always≡2^ n) ⟩
               2^ n * #⟨ f ⟩
             ∎
      where open ≡-Reasoning

#⟨_==⟩ : ∀ {n} (xs : Bits n) → #⟨ flip _==_ xs ⟩ ≡ 1
#⟨ xs ==⟩ = trans (≗-cong-# (flip _==_ xs) (_==_ xs) (flip ==-comm xs)) #⟨== xs ⟩

#⇒ : ∀ {n} (f g : Bits n → 𝟚) → (∀ x → ✓ (f x) → ✓ (g x)) → #⟨ f ⟩ ≤ #⟨ g ⟩
#⇒ {zero} f g f⇒g with f [] | g [] | f⇒g []
... | true  | true  | _ = s≤s z≤n
... | true  | false | p = 𝟘-elim (p _)
... | false | _     | _ = z≤n
#⇒ {suc n} f g f⇒g = #⇒ (f ∘ 0∷_) (g ∘ 0∷_) (f⇒g ∘ 0∷_)
               +-mono #⇒ (f ∘ 1∷_) (g ∘ 1∷_) (f⇒g ∘ 1∷_)

#-∧-∨ᵇ : ∀ x y → 𝟚▹ℕ (x ∧ y) + 𝟚▹ℕ (x ∨ y) ≡ 𝟚▹ℕ x + 𝟚▹ℕ y
#-∧-∨ᵇ true y rewrite ℕ°.+-comm (𝟚▹ℕ y) 1 = refl
#-∧-∨ᵇ false y = refl

#-LEM : ∀ {n} → (f g : Bits n → 𝟚) → #⟨ f ⟩ ≡ #⟨ g |∧| f ⟩ + #⟨ |not| g |∧| f ⟩
#-LEM {zero} f g with g []
... | false = refl
... | true  = ℕ°.+-comm 0 #⟨ f ⟩
#-LEM {suc n} f g
  rewrite #-LEM (f ∘ 0∷_) (g ∘ 0∷_)
        | #-LEM (f ∘ 1∷_) (g ∘ 1∷_)
          = +-interchange #⟨ (g ∘ 0∷_) |∧| (f ∘ 0∷_) ⟩
                #⟨ |not| (g ∘ 0∷_) |∧| (f ∘ 0∷_) ⟩
                #⟨ (g ∘ 1∷_) |∧| (f ∘ 1∷_) ⟩
                #⟨ |not| (g ∘ 1∷_) |∧| (f ∘ 1∷_) ⟩

#-∧-snd : ∀ {n} (f g : Bits n → 𝟚) → #⟨ f |∧| g ⟩ ≤ #⟨ g ⟩
#-∧-snd {zero} f g with f [] | g []
... | false | false = z≤n
... | false | true  = z≤n
... | true  | _     = ℕ≤.reflexive refl
#-∧-snd {suc n} f g = #-∧-snd (f ∘ 0∷_) (g ∘ 0∷_)
               +-mono #-∧-snd (f ∘ 1∷_) (g ∘ 1∷_)

#-∧-fst : ∀ {n} (f g : Bits n → 𝟚) → #⟨ f |∧| g ⟩ ≤ #⟨ f ⟩
#-∧-fst f g =
          #⟨ f |∧| g ⟩
            ≡⟨ #-≗ (f |∧| g) (g |∧| f) (|∧|-comm f g) ⟩
          #⟨ g |∧| f ⟩
            ≤⟨ #-∧-snd g f ⟩
          #⟨ f ⟩ ∎
      where open ≤-Reasoning

#-∧-∨ : ∀ {n} (f g : Bits n → 𝟚) → #⟨ f |∧| g ⟩ + #⟨ f |∨| g ⟩ ≡ #⟨ f ⟩ + #⟨ g ⟩
#-∧-∨ {zero} f g = #-∧-∨ᵇ (f []) (g [])
#-∧-∨ {suc n} f g =
  trans
    (trans
      (helper #⟨ (f ∘ 0∷_) |∧| (g ∘ 0∷_) ⟩
              #⟨ (f ∘ 1∷_) |∧| (g ∘ 1∷_) ⟩
              #⟨ (f ∘ 0∷_) |∨| (g ∘ 0∷_) ⟩
                #⟨ (f ∘ 1∷_) |∨| (g ∘ 1∷_) ⟩)
      (cong₂ _+_ (#-∧-∨ (f ∘ 0∷_) (g ∘ 0∷_))
                 (#-∧-∨ (f ∘ 1∷_) (g ∘ 1∷_))))
      (helper #⟨ f ∘ 0∷_ ⟩ #⟨ g ∘ 0∷_ ⟩ #⟨ f ∘ 1∷_ ⟩ #⟨ g ∘ 1∷_ ⟩)
        where open SemiringSolver
              helper : ∀ x y z t → x + y + (z + t) ≡ x + z + (y + t)
              helper = solve 4 (λ x y z t → x :+ y :+ (z :+ t) := x :+ z :+ (y :+ t)) refl

#∨' : ∀ {n} (f g : Bits n → 𝟚) → #⟨ f |∨| g ⟩ ≤ #⟨ f ⟩ + #⟨ g ⟩
#∨' {zero} f g with f []
... | true  = s≤s z≤n
... | false = ℕ≤.refl
#∨' {suc _} f g = ℕ≤.trans (#∨' (f ∘ 0∷_) (g ∘ 0∷_) +-mono
                            #∨' (f ∘ 1∷_) (g ∘ 1∷_))
                        (ℕ≤.reflexive
                          (helper #⟨ f ∘ 0∷_ ⟩ #⟨ g ∘ 0∷_ ⟩ #⟨ f ∘ 1∷_ ⟩ #⟨ g ∘ 1∷_ ⟩))
    where open SemiringSolver
          helper : ∀ x y z t → x + y + (z + t) ≡ x + z + (y + t)
          helper = solve 4 (λ x y z t → x :+ y :+ (z :+ t) := x :+ z :+ (y :+ t)) refl

#∨ : ∀ {m n o} {f g : Bits o → 𝟚} → #⟨ f ⟩ ≤ m → #⟨ g ⟩ ≤ n → #⟨ f |∨| g ⟩ ≤ (m + n)
#∨ {m} {n} {o} {f} {g} pf pg = ℕ≤.trans (#∨' f g) (pf +-mono pg)

#∧ : ∀ {m n o} {f g : Bits o → 𝟚} → #⟨ f ⟩ ≤ m → #⟨ g ⟩ ≤ n → #⟨ f |∧| g ⟩ ≤ (m + n)
#∧ {f = f} {g} pf pg = ℕ≤.trans (#⇒ (f |∧| g) (f |∨| g) (λ x → ∧⇒∨ (f x) (g x))) (#∨ {f = f} pf pg)

#-bound : ∀ c (f : Bits c → 𝟚) → #⟨ f ⟩ ≤ 2^ c
#-bound zero    f = 𝟚≤1 (f [])
#-bound (suc c) f = #-bound c (f ∘ 0∷_) +-mono #-bound c (f ∘ 1∷_)

#-∘vnot : ∀ c (f : Bits c → 𝟚) → #⟨ f ⟩ ≡ #⟨ f ∘ vnot ⟩
#-∘vnot _ f = #-⊕ 1ⁿ f

#-∘xorᵢ : ∀ {c} (i : Fin c) (f : Bits c → 𝟚) b → #⟨ f ⟩ ≡ #⟨ f ∘ onᵢ (_xor_ b) i ⟩
#-∘xorᵢ i f b = pf
  where pad = onᵢ (_xor_ b) i 0ⁿ
        pf : #⟨ f ⟩ ≡ #⟨ f ∘ onᵢ (_xor_ b) i ⟩
        pf rewrite #-⊕ pad f = ≗-cong-# (f ∘ _⊕_ pad) (f ∘ onᵢ (_xor_ b) i) (cong (_$_ f) ∘ sym ∘ onᵢ-xor-⊕ b i)

#-∘notᵢ : ∀ {c} (i : Fin c) (f : Bits c → 𝟚) → #⟨ f ⟩ ≡ #⟨ f ∘ notᵢ i ⟩
#-∘notᵢ i f = #-∘xorᵢ i f true

#-not∘ : ∀ c (f : Bits c → 𝟚) → #⟨ f ⟩ ≡ 2^ c ∸ #⟨ not ∘ f ⟩
#-not∘ zero f with f []
... | true  = ≡.refl
... | false = ≡.refl
#-not∘ (suc c) f
  rewrite #-not∘ c (f ∘ 0∷_)
        | #-not∘ c (f ∘ 1∷_) = factor-+-∸ (#-bound c (not ∘ f ∘ 0∷_)) (#-bound c (not ∘ f ∘ 1∷_))

#-not∘′ : ∀ c (f : Bits c → 𝟚) → #⟨ not ∘ f ⟩ ≡ 2^ c ∸ #⟨ f ⟩
#-not∘′ c f = #⟨ not ∘ f ⟩
            ≡⟨ #-not∘ c (not ∘ f) ⟩
              2^ c ∸ #⟨ not ∘ not ∘ f ⟩
            ≡⟨ ≡.cong (λ g → 2^ c ∸ g) (≗-cong-# (not ∘ not ∘ f) f (not-involutive ∘ f)) ⟩
              2^ c ∸ #⟨ f ⟩
            ∎
      where open ≡-Reasoning

difference-lemma : ∀ {n}(A B F : Bits n → 𝟚)
      → #⟨ |not| F |∧| A ⟩ ≡ #⟨ |not| F |∧| B ⟩
      → dist #⟨ A ⟩ #⟨ B ⟩ ≤ #⟨ F ⟩
difference-lemma A B F A∧¬F≡B∧¬F =
  dist #⟨ A ⟩ #⟨ B ⟩
    ≡⟨ cong₂ dist (#-LEM A F) (#-LEM B F) ⟩
  dist (#⟨ F |∧| A ⟩ + #⟨ |not| F |∧| A ⟩)
       (#⟨ F |∧| B ⟩ + #⟨ |not| F |∧| B ⟩)
    ≡⟨ cong₂ dist (ℕ°.+-comm #⟨ F |∧| A ⟩ #⟨ |not| F |∧| A ⟩)
                  (ℕ°.+-comm #⟨ F |∧| B ⟩ #⟨ |not| F |∧| B ⟩) ⟩
  dist (#⟨ |not| F |∧| A ⟩ + #⟨ F |∧| A ⟩)
       (#⟨ |not| F |∧| B ⟩ + #⟨ F |∧| B ⟩)
    ≡⟨ cong₂ dist (refl {x = #⟨ |not| F |∧| A ⟩ + #⟨ F |∧| A ⟩})
                  (cong₂ _+_ (sym A∧¬F≡B∧¬F) (refl {x = #⟨ F |∧| B ⟩})) ⟩
  dist (#⟨ |not| F |∧| A ⟩ + #⟨ F |∧| A ⟩)
       (#⟨ |not| F |∧| A ⟩ + #⟨ F |∧| B ⟩)
    ≡⟨ dist-x+ #⟨ |not| F |∧| A ⟩ #⟨ F |∧| A ⟩ #⟨ F |∧| B ⟩ ⟩
  dist #⟨ F |∧| A ⟩ #⟨ F |∧| B ⟩
    ≤⟨ dist-bounded {#⟨ F |∧| A ⟩} {#⟨ F |∧| B ⟩} {#⟨ F ⟩} (#-∧-fst F A) (#-∧-fst F B) ⟩
  #⟨ F ⟩ ∎
     where open ≤-Reasoning

#⟨_⟩ᶠ : ∀ {n} → (Bits n → 𝟚) → Fin (suc (2^ n))
#⟨ pred ⟩ᶠ = countᶠ pred (allBits _)

#⟨⟩-spec : ∀ {n} (pred : Bits n → 𝟚) → #⟨ pred ⟩ ≡ Fin.toℕ #⟨ pred ⟩ᶠ
#⟨⟩-spec {zero}  pred with pred []
... | true = refl
... | false = refl
#⟨⟩-spec {suc n} pred rewrite count-++ pred (vmap 0∷_ (allBits n)) (vmap 1∷_ (allBits n))
                            | #⟨⟩-spec {n} (pred ∘ 0∷_)
                            | #⟨⟩-spec {n} (pred ∘ 1∷_)
                            | count-∘ 0∷_ pred (allBits n)
                            | count-∘ 1∷_ pred (allBits n) = refl

ext-# : ∀ {c} {f g : Bits c → 𝟚} → f ≗ g → #⟨ f ⟩ᶠ ≡ #⟨ g ⟩ᶠ
ext-# f≗g = ext-countᶠ f≗g (allBits _)

find? : ∀ {n a} {A : ★ a} → (Bits n →? A) →? A
find? = search (M?._∣_ _)

findKey : ∀ {n} → (Bits n → 𝟚) →? Bits n
findKey pred = find? (λ x → if pred x then just x else nothing)
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Pi.Interp where
open import Data.Unit
open import Data.Product
open import Data.Sum
open import Pi.Syntax
open import Pi.Opsem

-- Big-step intepreter
interp : {A B : 𝕌} → (A ↔ B) → ⟦ A ⟧ → ⟦ B ⟧
interp unite₊l (inj₂ v)         = v
interp uniti₊l v                = inj₂ v
interp swap₊   (inj₁ v)         = inj₂ v
interp swap₊   (inj₂ v)         = inj₁ v
interp assocl₊ (inj₁ v)         = inj₁ (inj₁ v)
interp assocl₊ (inj₂ (inj₁ v))  = inj₁ (inj₂ v)
interp assocl₊ (inj₂ (inj₂ v))  = inj₂ v
interp assocr₊ (inj₁ (inj₁ v))  = inj₁ v
interp assocr₊ (inj₁ (inj₂ v))  = inj₂ (inj₁ v)
interp assocr₊ (inj₂ v)         = inj₂ (inj₂ v)
interp unite⋆l (tt , v)         = v
interp uniti⋆l v                = (tt , v)
interp swap⋆   (v₁ , v₂)        = (v₂ , v₁)
interp assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
interp assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
interp dist    (inj₁ v₁ , v₃)   = inj₁ (v₁ , v₃)
interp dist    (inj₂ v₂ , v₃)   = inj₂ (v₂ , v₃)
interp factor  (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
interp factor  (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
interp id↔     v                = v
interp (c₁ ⨾ c₂) v = interp c₂ (interp c₁ v)
interp (c₁ ⊕ c₂) (inj₁ v) = inj₁ (interp c₁ v)
interp (c₁ ⊕ c₂) (inj₂ v) = inj₂ (interp c₂ v)
interp (c₁ ⊗ c₂) (v₁ , v₂) = (interp c₁ v₁ , interp c₂ v₂)


text:
module Oscar.Data.Unit where

open import Agda.Builtin.Unit public using (⊤; tt)


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

open import sum
open import equality
open import function.core
open import function.isomorphism.core
open import function.overloading
open import pointed.core
open import sets.nat.core

Ω₁ : ∀ {i} → PSet i → PSet i
Ω₁ (X , x) = ((x ≡ x) , refl)

ΩP : ∀ {i} → ℕ → PSet i → PSet _
ΩP 0 𝓧 = 𝓧
ΩP (suc n) 𝓧 = ΩP n (Ω₁ 𝓧)

Ω : ∀ {i} → ℕ → {X : Set i} → X → Set i
Ω n {X} x = proj₁ (ΩP n (X , x))

refl' : ∀ {i} n {X : Set i}(x : X) → Ω n x
refl' n {X} x = proj₂ (ΩP n (X , x))

mapΩ₁ : ∀ {i j} → {𝓧 : PSet i}{𝓨 : PSet j}
     → PMap 𝓧 𝓨 → PMap (Ω₁ 𝓧) (Ω₁ 𝓨)
mapΩ₁ (f , refl) = ap f , refl

mapΩP : ∀ {i j} n → {𝓧 : PSet i}{𝓨 : PSet j}
      → PMap 𝓧 𝓨 → PMap (ΩP n 𝓧) (ΩP n 𝓨)
mapΩP zero f = f
mapΩP (suc n) f = mapΩP n (mapΩ₁ f)

mapΩ : ∀ {i j} n → {X : Set i}{Y : Set j}(f : X → Y)
     → {x : X} → Ω n x → Ω n (f x)
mapΩ n f = proj₁ (mapΩP n (f , refl))

constP : ∀ {i j} (𝓧 : PSet i)(𝓨 : PSet j) → PMap 𝓧 𝓨
constP _ (Y , y) = (λ _ → y) , refl

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import lib.Basics
open import lib.types.PushoutFmap
open import lib.types.Span
open import lib.types.Coproduct
open import lib.types.Paths

open import Graphs.Definition
open import Coequalizers.Definition
open import Util.Coproducts

{- We show that given equivalences E ≃ E' and V ≃ V' that commute with endpoint maps
   we get an equivalence between coequalizers V / E ≃ V' / E'. This could have been
   derived from the corresponding result for pushouts in the HoTT-Agda library, but
   for reference we give the proof using univalence appearing in the paper.
-}
module Coequalizers.PreserveEquivalence where

Coeq-preserves-= : {i j : ULevel} (V : Type i) (E : Type j) (π₀ π₁ : E → V)
  (V' : Type i) (E' : Type j) (π₀' π₁' : E' → V')
  (eV : V == V') (eE : E == E') (comm₀ : coe eV ∘ π₀ == π₀' ∘ coe eE ) (comm₁ : coe eV ∘ π₁ == π₁' ∘ coe eE) →
  (Coeq (graph π₀ π₁) ≃ Coeq (graph π₀' π₁'))

Coeq-preserves-= V E π₀ π₁ .V .E .(λ x → π₀ x) .(λ x → π₁ x) idp idp idp idp = ide _

{- The easiest version of the lemma assumes that V has the same universe level as V'
   and E has the same universe level as E'. -}
Coeq-emap-same-level : {i j : ULevel} {V : Type i} {E : Type j} ⦃ gph : Graph E V ⦄
  {V' : Type i} {E' : Type j} ⦃ gph' : Graph E' V' ⦄
  (eV : V ≃ V') (eE : E ≃ E')
  (comm₀ : –> eV ∘ π₀ ∼ π₀ ∘ –> eE )
  (comm₁ : –> eV ∘ π₁ ∼ π₁ ∘ –> eE ) → (Coeq gph ≃ Coeq gph')

Coeq-emap-same-level eV eE comm₀ comm₁ = Coeq-preserves-= _ _ π₀ π₁ _ _ π₀ π₁ (ua eV) (ua eE)
  (λ= (λ e → coe-β eV _ ∙ comm₀ e ∙ ap π₀ (! (coe-β eE e))))
  (λ= (λ e → coe-β eV _ ∙ comm₁ e ∙ ap π₁ (! (coe-β eE e))))

{- We now deal with the case where all the types can have different universe levels.
   We first show that every coequalizer is equivalent to its lift to higher universe
   levels. -}
module LiftGraph {i j : ULevel} (V : Type i) (E : Type j) ⦃ gph : Graph E V ⦄ (i' j' : ULevel) where
  instance
    lift-graph : Graph (Lift {j = j'} E) (Lift {j = i'} V)
    lift-graph = graph (λ { (lift e) → lift (π₀ e)}) λ { (lift e) → lift (π₁ e)}

  Coeq-Lift-≃ : Coeq gph ≃ Coeq (lift-graph)
  Coeq-Lift-≃ = equiv f g f-g g-f
    where
      f : V / E → (Lift V) / (Lift E)
      f = Coeq-rec (c[_] ∘ lift) (λ e → quot (lift e))

      g : (Lift V) / (Lift E) → V / E
      g = Coeq-rec (λ {(lift v) → c[ v ]}) (λ {(lift e) → quot e})

      g-f : (z : V / E) → (g (f z) == z)
      g-f = Coeq-elim _ (λ v → idp) (λ e → ↓-app=idf-in (! (p e)))
        where
          p : (e : E) → ap (g ∘ f) (quot e) ∙ idp == idp ∙' (quot e)
          p e =
            ap (g ∘ f) (quot e) ∙ idp
              =⟨ ∙-unit-r _ ⟩
            ap (g ∘ f) (quot e)
              =⟨ ap-∘ g f (quot e) ⟩
            ap g (ap f (quot e))
              =⟨ ap (ap g) (Coeq-rec-β= _ _ e) ⟩
            ap g (quot (lift e))
              =⟨ Coeq-rec-β= _ _ (lift e) ⟩
            quot e
              =⟨ ! (∙'-unit-l _) ⟩
            idp ∙' (quot e)
              =∎

      f-g : (z : (Lift V) / (Lift E)) → (f (g z) == z)
      f-g = Coeq-elim _ (λ v → idp) (λ {(lift e) → ↓-app=idf-in (! (p e))})
        where
          p : (e : E) → ap (f ∘ g) (quot (lift e)) ∙ idp == idp ∙' quot (lift e)
          p e =
            ap (f ∘ g) (quot (lift e)) ∙ idp
              =⟨ ∙-unit-r _ ⟩
            ap (f ∘ g) (quot (lift e))
              =⟨ ap-∘ f g _ ⟩
            ap f (ap g (quot (lift e)))
              =⟨ ap (ap f) (Coeq-rec-β= _ _ _) ⟩
            ap f (quot e)
              =⟨ Coeq-rec-β= _ _ _ ⟩
            quot (lift e)
              =⟨ ! (∙'-unit-l _) ⟩
            idp ∙' quot (lift e)
              =∎

{- We can now derive that coequalizers preserve equivalences where
   the types can have different universe levels. -}
Coeq-emap : {i j i' j' : ULevel} {V : Type i} {E : Type j} ⦃ gph : Graph E V ⦄
  {V' : Type i'} {E' : Type j'} ⦃ gph' : Graph E' V' ⦄ →
  (eV : V ≃ V') (eE : E ≃ E')
  (comm₀ : –> eV ∘ π₀ ∼ π₀ ∘ –> eE )
  (comm₁ : –> eV ∘ π₁ ∼ π₁ ∘ –> eE ) → (Coeq gph ≃ Coeq gph')

Coeq-emap {i} {j} {i'} {j'} {V} {E} ⦃ gph ⦄ {V'} {E'} ⦃ gph' ⦄ eV eE comm₀ comm₁ =
  V / E
    ≃⟨ LEV.Coeq-Lift-≃ ⟩
  Lift V / Lift E
    ≃⟨ Coeq-emap-same-level
       (lower-equiv ⁻¹ ∘e eV ∘e lower-equiv)
       (lower-equiv ⁻¹ ∘e eE ∘e lower-equiv)
       (λ {(lift e) → ap lift (comm₀ e)})
       (λ {(lift e) → ap lift (comm₁ e)}) ⟩
  Lift V' / Lift E'
    ≃⟨ LEV'.Coeq-Lift-≃ ⁻¹ ⟩
  V' / E'
    ≃∎
  where
    module LEV = LiftGraph V E i' j'
    module LEV' = LiftGraph V' E' i j

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
{-

Normalize Integer Matrices

-}
{-# OPTIONS --safe #-}

module Cubical.Experiments.IntegerMatrix where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.Int
open import Cubical.Data.FinData
open import Cubical.Data.List

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int
  renaming (ℤ to ℤRing)

open import Cubical.Algebra.Matrix
open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.IntegerMatrix.Smith
open import Cubical.Algebra.IntegerMatrix.Diagonalization

private
  variable
    m n : ℕ

open Coefficient ℤRing

-- Get divisors directly

open isSmithNormal
open Smith
open isDiagonal
open Diag

getElemDiv : Mat m n → List ℤ
getElemDiv M = smith M .isnormal .divs .fst

getDiagDiv : Mat m n → List ℤ
getDiagDiv M = diagonalize M .isdiag .divs .fst

-- Constructing matrices

makeMat2×2 : ℤ → ℤ → ℤ → ℤ → Mat 2 2
makeMat2×2 a00 _ _ _ zero zero = a00
makeMat2×2 _ a01 _ _ zero one  = a01
makeMat2×2 _ _ a10 _ one  zero = a10
makeMat2×2 _ _ _ a11 one  one  = a11

makeMat3×3 : ℤ → ℤ → ℤ → ℤ → ℤ → ℤ → ℤ → ℤ → ℤ → Mat 3 3
makeMat3×3 a00 _ _ _ _ _ _ _ _ zero zero = a00
makeMat3×3 _ a01 _ _ _ _ _ _ _ zero one  = a01
makeMat3×3 _ _ a02 _ _ _ _ _ _ zero two  = a02
makeMat3×3 _ _ _ a10 _ _ _ _ _ one  zero = a10
makeMat3×3 _ _ _ _ a11 _ _ _ _ one  one  = a11
makeMat3×3 _ _ _ _ _ a12 _ _ _ one  two  = a12
makeMat3×3 _ _ _ _ _ _ a20 _ _ two  zero = a20
makeMat3×3 _ _ _ _ _ _ _ a21 _ two  one  = a21
makeMat3×3 _ _ _ _ _ _ _ _ a22 two  two  = a22

-- The Tests

-- One can add flag "-vprofile.interactive:10" to this file,
-- then C-c C-n to run these tests and also get the time.

-- It turns out that, "smith" is much slower than "diagonalize"
-- and it doesn't work even for simple 3×3-matrices.
-- The "diagonalize" works only for very simple 3×3-matrices.
-- One subtle point is, if one only do one-step in Smith normalization
-- and simply add the time cost in each steps,
-- the result is far less than running the whole function "smith".
-- So the recursive procedure slows down the procedure
-- for some reasons I don't fully understand.
-- Also, the performance of "smith" is very bad at certain trivial cases,
-- much worse than some non-trivial cases.

mat1 = makeMat2×2
   1  0
   0  1
-- Time: 528ms
test1  = getElemDiv mat1
-- Time: 51ms
test1' = getDiagDiv mat1

mat2 = makeMat2×2
   2  0
   0  1
-- Time: 89,437ms
-- Why so slow?
test2  = getElemDiv mat2
-- Time: 51ms
test2' = getDiagDiv mat2

mat3 = makeMat2×2
   2  1
   3  5
-- Time: 3,308ms
test3  = getElemDiv mat3
-- Time: 1,887ms
test3' = getDiagDiv mat3

mat4 = makeMat2×2
   4  2
   2  4
-- Time: 3,284ms
test4  = getElemDiv mat4
-- Time: 1,942ms
test4' = getDiagDiv mat4

mat5 = makeMat3×3
   1  0  0
   0  0  0
   0  0  0
-- Time: 9,400ms
test5  = getElemDiv mat5
-- Time: 337ms
test5' = getDiagDiv mat5

mat6 = makeMat3×3
   1  0  0
   0  1  0
   0  0  1
-- Time: ???
-- It doesn't work out already.
test6  = getElemDiv mat6
-- Time: 8,598ms
test6' = getDiagDiv mat6

mat7 = makeMat3×3
   1  1  0
   3  2  1
   2  0  1
-- Time: ???
test7  = getElemDiv mat7
-- Time: 14,149ms
test7' = getDiagDiv mat7

mat8 = makeMat3×3
   2  3  1
   2  2  3
   1  1  0
-- Time: ???
test8  = getElemDiv mat8
-- Time: ???
-- Not working either.
test8' = getDiagDiv mat8

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- Some properties related to the const function
------------------------------------------------------------------------

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

open import Equality

module Const
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude

import Bijection eq as Bijection
open Derived-definitions-and-properties eq
open import Embedding eq
open import Equivalence eq as Eq using (_≃_)
open import Fin eq
open import Function-universe eq
open import H-level eq
open import H-level.Closure eq
open import Injection eq using (Injective)
import Nat eq as Nat
open import Univalence-axiom eq

-- If A is inhabited, then the function const : B → (A → B) is
-- injective.

const-is-injective :
  ∀ {a b} →
  {A : Type a} {B : Type b} →
  A → Injective {B = A → B} const
const-is-injective x {y} {z} =
  const y ≡ const z  ↝⟨ cong (_$ x) ⟩□
  y ≡ z              □

-- Thus, if B is a set, then const is also an embedding (assuming
-- extensionality).

const-is-embedding :
  ∀ {a b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  {A : Type a} {B : Type b} →
  Is-set B →
  A → Is-embedding {B = A → B} const
const-is-embedding {a} {b} ext B-set x =
  _≃_.to (Injective≃Is-embedding
            ext B-set
            (Π-closure (lower-extensionality b a ext) 2 λ _ →
             B-set)
            const)
    (const-is-injective x)

-- However, if B is not a set, then one can construct a counterexample
-- (assuming extensionality and univalence).
--
-- This example is due to Thierry Coquand. (His proof was not
-- identical to the one below.)

const-is-not-embedding :
  ∀ {a b} →
  Extensionality (a ⊔ b) (lsuc b) →
  Univalence b →
  Univalence (# 0) →
  ¬ ({A : Type a} {B : Type (lsuc b)} →
     A → Is-embedding {B = A → B} const)
const-is-not-embedding {a} {b} ext univ univ₀ hyp =
  from-⊎ (2 Nat.≟ 4) 2≡4
  where
  ext-b : Extensionality b b
  ext-b = lower-extensionality a (lsuc b) ext

  ext-ab₊ : Extensionality a (lsuc b)
  ext-ab₊ = lower-extensionality b lzero ext

  ext₁ : Extensionality (# 0) (# 1)
  ext₁ = lower-extensionality _ (lsuc b) ext

  ext₀ : Extensionality (# 0) (# 0)
  ext₀ = lower-extensionality _ _ ext

  emb : Is-embedding {B = ↑ a (Fin 2) → Type b} const
  emb = hyp (lift true)

  2≡4 : 2 ≡ 4
  2≡4 = _⇔_.to isomorphic-same-size (
    Fin 2                                      ↝⟨ inverse $ [Fin≡Fin]↔Fin! ext₀ univ₀ 2 ⟩
    Fin 2 ≡ Fin 2                              ↔⟨ inverse $ ≡-preserves-≃ ext-b univ univ₀ (Eq.↔⇒≃ Bijection.↑↔) (Eq.↔⇒≃ Bijection.↑↔) ⟩
    ↑ b (Fin 2) ≡ ↑ b (Fin 2)                  ↔⟨ Eq.⟨ _ , emb (↑ b (Fin 2)) (↑ b (Fin 2)) ⟩ ⟩
    const (↑ b (Fin 2)) ≡ const (↑ b (Fin 2))  ↔⟨ inverse $ Eq.extensionality-isomorphism ext-ab₊ ⟩
    (↑ a (Fin 2) → ↑ b (Fin 2) ≡ ↑ b (Fin 2))  ↔⟨ →-cong ext-ab₊ (Eq.↔⇒≃ Bijection.↑↔)
                                                    (≡-preserves-≃ ext-b univ univ₀ (Eq.↔⇒≃ Bijection.↑↔) (Eq.↔⇒≃ Bijection.↑↔)) ⟩
    (Fin 2 → Fin 2 ≡ Fin 2)                    ↝⟨ ∀-cong ext₁ (λ _ → [Fin≡Fin]↔Fin! ext₀ univ₀ 2) ⟩
    (Fin 2 → Fin 2)                            ↝⟨ [Fin→Fin]↔Fin^ ext₀ 2 2 ⟩□
    Fin 4                                      □)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of membership of vectors based on propositional equality.
------------------------------------------------------------------------

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

module Data.Vec.Membership.Propositional.Properties where

open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Product as Prod using (_,_; ∃; _×_; -,_)
open import Data.Vec hiding (here; there)
open import Data.Vec.Relation.Unary.Any using (here; there)
open import Data.List.Base using ([]; _∷_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Vec.Relation.Unary.Any using (Any; here; there)
open import Data.Vec.Membership.Propositional
open import Data.List.Membership.Propositional
  using () renaming (_∈_ to _∈ₗ_)
open import Level using (Level)
open import Function using (_∘_; id)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality using (refl)

private
  variable
    a b p : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- lookup

∈-lookup : ∀ {n} i (xs : Vec A n) → lookup xs i ∈ xs
∈-lookup zero    (x ∷ xs) = here refl
∈-lookup (suc i) (x ∷ xs) = there (∈-lookup i xs)

------------------------------------------------------------------------
-- map

∈-map⁺ : (f : A → B) → ∀ {m v} {xs : Vec A m} → v ∈ xs → f v ∈ map f xs
∈-map⁺ f (here refl)  = here refl
∈-map⁺ f (there x∈xs) = there (∈-map⁺ f x∈xs)

------------------------------------------------------------------------
-- _++_

∈-++⁺ˡ : ∀ {m n v} {xs : Vec A m} {ys : Vec A n} → v ∈ xs → v ∈ xs ++ ys
∈-++⁺ˡ (here refl)  = here refl
∈-++⁺ˡ (there x∈xs) = there (∈-++⁺ˡ x∈xs)

∈-++⁺ʳ : ∀ {m n v} (xs : Vec A m) {ys : Vec A n} → v ∈ ys → v ∈ xs ++ ys
∈-++⁺ʳ []       x∈ys = x∈ys
∈-++⁺ʳ (x ∷ xs) x∈ys = there (∈-++⁺ʳ xs x∈ys)

------------------------------------------------------------------------
-- tabulate

∈-tabulate⁺ : ∀ {n} (f : Fin n → A) i → f i ∈ tabulate f
∈-tabulate⁺ f zero    = here refl
∈-tabulate⁺ f (suc i) = there (∈-tabulate⁺ (f ∘ suc) i)

------------------------------------------------------------------------
-- allFin

∈-allFin⁺ : ∀ {n} (i : Fin n) → i ∈ allFin n
∈-allFin⁺ = ∈-tabulate⁺ id

------------------------------------------------------------------------
-- allPairs

∈-allPairs⁺ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
             x ∈ xs → y ∈ ys → (x , y) ∈ allPairs xs ys
∈-allPairs⁺ {xs = x ∷ xs} (here refl)  = ∈-++⁺ˡ ∘ ∈-map⁺ (x ,_)
∈-allPairs⁺ {xs = x ∷ _}  (there x∈xs) =
  ∈-++⁺ʳ (map (x ,_) _) ∘ ∈-allPairs⁺ x∈xs

------------------------------------------------------------------------
-- toList

∈-toList⁺ : ∀ {n} {v : A} {xs : Vec A n} → v ∈ xs → v ∈ₗ toList xs
∈-toList⁺ (here refl) = here refl
∈-toList⁺ (there x∈)  = there (∈-toList⁺ x∈)

∈-toList⁻ : ∀ {n} {v : A} {xs : Vec A n} → v ∈ₗ toList xs → v ∈ xs
∈-toList⁻ {xs = x ∷ xs} (here refl)  = here refl
∈-toList⁻ {xs = x ∷ xs} (there v∈xs) = there (∈-toList⁻ v∈xs)

------------------------------------------------------------------------
-- fromList

∈-fromList⁺ : ∀ {v : A} {xs} → v ∈ₗ xs → v ∈ fromList xs
∈-fromList⁺ (here refl) = here refl
∈-fromList⁺ (there x∈)  = there (∈-fromList⁺ x∈)

∈-fromList⁻ : ∀ {v : A} {xs} → v ∈ fromList xs → v ∈ₗ xs
∈-fromList⁻ {xs = _ ∷ _} (here refl)  = here refl
∈-fromList⁻ {xs = _ ∷ _} (there v∈xs) = there (∈-fromList⁻ v∈xs)

------------------------------------------------------------------------
-- Relationship to Any

module _ {P : Pred A p} where

  fromAny : ∀ {n} {xs : Vec A n} → Any P xs → ∃ λ x → x ∈ xs × P x
  fromAny (here px) = -, here refl , px
  fromAny (there v) = Prod.map₂ (Prod.map₁ there) (fromAny v)

  toAny : ∀ {n x} {xs : Vec A n} → x ∈ xs → P x → Any P xs
  toAny (here refl) px = here px
  toAny (there v)   px = there (toAny v px)


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

module Fragment.Algebra.Free.Atoms where

open import Level using (Level; _⊔_)

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

open import Relation.Binary using (Setoid; IsEquivalence)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

private
  variable
    a ℓ : Level

module _ (A : Set a) where

  data BT (n : ℕ) : Set a where
    sta : A → BT n
    dyn : Fin n → BT n

module _ (S : Setoid a ℓ) (n : ℕ) where

  open Setoid S renaming (Carrier to A)

  data _≍_ : BT A n → BT A n → Set (a ⊔ ℓ) where
    sta : ∀ {x y} → x ≈ y → sta x ≍ sta y
    dyn : ∀ {x y} → x ≡ y → dyn x ≍ dyn y

  private

    ≍-refl : ∀ {x} → x ≍ x
    ≍-refl {sta _} = sta refl
    ≍-refl {dyn _} = dyn PE.refl

    ≍-sym : ∀ {x y} → x ≍ y → y ≍ x
    ≍-sym (sta x≈y) = sta (sym x≈y)
    ≍-sym (dyn x≡y) = dyn (PE.sym x≡y)

    ≍-trans : ∀ {x y z} → x ≍ y → y ≍ z → x ≍ z
    ≍-trans (sta x≈y) (sta y≈z) = sta (trans x≈y y≈z)
    ≍-trans (dyn x≡y) (dyn y≡z) = dyn (PE.trans x≡y y≡z)

    ≍-isEquivalence : IsEquivalence _≍_
    ≍-isEquivalence = record { refl  = ≍-refl
                             ; sym   = ≍-sym
                             ; trans = ≍-trans
                             }

  Atoms : Setoid a (a ⊔ ℓ)
  Atoms = record { Carrier       = BT (Setoid.Carrier S) n
                 ; _≈_           = _≍_
                 ; isEquivalence = ≍-isEquivalence
                 }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------
-- Validity of declarative kinding of Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Declarative.Validity where

open import Data.Fin using (zero)
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Product as Prod using (_,_; _×_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

open import FOmegaInt.Syntax
open import FOmegaInt.Kinding.Declarative

------------------------------------------------------------------------
-- Validity of declarative kinding, subkinding and subtyping

open Syntax
open Substitution hiding (subst)
open TermCtx
open Kinding
open WfCtxOps using (lookup-kd)
open KindedSubstitution
open WfSubstitutionEquality

-- An admissible rule for kinding η-expanded type operators.
Tp∈-η : ∀ {n} {Γ : Ctx n} {a j k} →
        Γ ⊢Tp a ∈ Π j k → Γ ⊢ j kd → kd j ∷ Γ ⊢ k kd →
        Γ ⊢Tp Λ j (weaken a · var zero) ∈ Π j k
Tp∈-η {k = k} a∈Πjk j-kd k-kd =
  ∈-Π-i j-kd (subst (_ ⊢Tp _ ∈_) k′[z]≡k (∈-Π-e a∈Πjk′ z∈k k-kd′ k[z]-kd)) k-kd
  where
    module KL = TermLikeLemmas termLikeLemmasKind

    j-wf    = wf-kd j-kd
    j-kd′   = kd-weaken j-wf j-kd
    k-kd′   = kd-/Var k-kd (Var∈-↑ (wf-kd j-kd′) (Var∈-wk j-wf))
    z∈k     = ∈-var zero (j-wf ∷ kd-ctx j-kd) refl
    a∈Πjk′  = Tp∈-weaken j-wf a∈Πjk
    k[z]-kd = kd-[] k-kd′ (∈-tp z∈k)
    k′[z]≡k = Kind-wk↑-sub-zero-vanishes k

mutual

  -- Validity of kinding: the kinds of well-kinded types are well-formed.
  Tp∈-valid : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ ⊢ k kd
  Tp∈-valid (∈-var x Γ-ctx Γ[x]≡kd-k) = lookup-kd x Γ-ctx Γ[x]≡kd-k
  Tp∈-valid (∈-⊥-f Γ-ctx)             = *-kd Γ-ctx
  Tp∈-valid (∈-⊤-f Γ-ctx)             = *-kd Γ-ctx
  Tp∈-valid (∈-∀-f k-kd a∈*)          = *-kd (kd-ctx k-kd)
  Tp∈-valid (∈-→-f a∈* b∈*)           = *-kd (Tp∈-ctx a∈*)
  Tp∈-valid (∈-Π-i j-kd a∈k k-kd)     = kd-Π j-kd (Tp∈-valid a∈k)
  Tp∈-valid (∈-Π-e a∈Πjk b∈j k-kd k[b]-kd) = k[b]-kd
  Tp∈-valid (∈-s-i a∈b⋯c)             = let a∈* = Tp∈-⋯-* a∈b⋯c in kd-⋯ a∈* a∈*
  Tp∈-valid (∈-⇑ a∈j j<∷k)            = proj₂ (<∷-valid j<∷k)

  -- Validity of subkinding: subkinds are well-formed.
  <∷-valid : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → Γ ⊢ j kd × Γ ⊢ k kd
  <∷-valid (<∷-⋯ a₂<:a₁∈* b₁<:b₂∈*)      =
    let a₂∈* , a₁∈* = <:-valid a₂<:a₁∈*
        b₁∈* , b₂∈* = <:-valid b₁<:b₂∈*
    in kd-⋯ a₁∈* b₁∈* , kd-⋯ a₂∈* b₂∈*
  <∷-valid (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) =
    Πj₁k₁-kd ,
    kd-Π (proj₁ (<∷-valid j₂<∷j₁)) (proj₂ (<∷-valid k₁<∷k₂))

  -- Validity of subtyping: subtypes that are related in some kind `k'
  -- inhabit `k'.
  <:-valid : ∀ {n} {Γ : Ctx n} {a b k} →
             Γ ⊢ a <: b ∈ k → Γ ⊢Tp a ∈ k × Γ ⊢Tp b ∈ k
  <:-valid (<:-refl a∈k)            = a∈k , a∈k
  <:-valid (<:-trans a<:b∈k b<:c∈k) =
    proj₁ (<:-valid a<:b∈k) , proj₂ (<:-valid b<:c∈k)
  <:-valid (<:-β₁ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) =
    ∈-Π-e (∈-Π-i j-kd a∈k k-kd) b∈j k-kd k[b]-kd , a[b]∈k[b]
    where j-kd = wf-kd-inv (wf-∷₁ (Tp∈-ctx a∈k))
  <:-valid (<:-β₂ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) =
    a[b]∈k[b] , ∈-Π-e (∈-Π-i j-kd a∈k k-kd) b∈j k-kd k[b]-kd
    where j-kd = wf-kd-inv (wf-∷₁ (Tp∈-ctx a∈k))
  <:-valid (<:-η₁ a∈Πjk) with Tp∈-valid a∈Πjk
  ... | (kd-Π j-kd k-kd) = Tp∈-η a∈Πjk j-kd k-kd , a∈Πjk
  <:-valid (<:-η₂ a∈Πjk) with Tp∈-valid a∈Πjk
  ... | (kd-Π j-kd k-kd) = a∈Πjk , Tp∈-η a∈Πjk j-kd k-kd
  <:-valid (<:-⊥ b∈c⋯d) = ∈-⊥-f (Tp∈-ctx b∈c⋯d) , Tp∈-⋯-* b∈c⋯d
  <:-valid (<:-⊤ b∈c⋯d) = Tp∈-⋯-* b∈c⋯d , ∈-⊤-f (Tp∈-ctx b∈c⋯d)
  <:-valid (<:-∀ k₂<∷k₁ a₁<:a₂∈* ∀k₁a₁∈*) =
    ∀k₁a₁∈* ,
    ∈-∀-f (proj₁ (<∷-valid k₂<∷k₁)) (proj₂ (<:-valid a₁<:a₂∈*))
  <:-valid (<:-→ a₂<:a₁∈* b₁<:b₂∈*) =
    let a₂∈* , a₁∈* = <:-valid a₂<:a₁∈*
        b₁∈* , b₂∈* = <:-valid b₁<:b₂∈*
    in ∈-→-f a₁∈* b₁∈* , ∈-→-f a₂∈* b₂∈*
  <:-valid (<:-λ a₁<:a₂∈k Λj₁a₁∈Πjk Λj₂a₂∈Πjk) = Λj₁a₁∈Πjk , Λj₂a₂∈Πjk
  <:-valid (<:-· a₁<:a₂∈Πjk b₁≃b₂∈j b₁∈j k-kd k[b₁]-kd) =
    let a₁∈Πjk , a₂∈Πjk = <:-valid a₁<:a₂∈Πjk
        b₁∈j   , b₂∈j   = ≃-valid  b₁≃b₂∈j
    in ∈-Π-e a₁∈Πjk b₁∈j k-kd k[b₁]-kd ,
       ∈-⇑ (∈-Π-e a₂∈Πjk b₂∈j k-kd (kd-[] k-kd (∈-tp b₂∈j)))
           (≅⇒<∷ (kd-[≃′] k-kd b₂∈j b₁∈j (≃-sym b₁≃b₂∈j)))
  <:-valid (<:-⟨| a∈b⋯c) with Tp∈-valid a∈b⋯c
  ... | (kd-⋯ b∈* c∈*) = b∈* , Tp∈-⋯-* a∈b⋯c
  <:-valid (<:-|⟩ a∈b⋯c) with Tp∈-valid a∈b⋯c
  ... | (kd-⋯ b∈* c∈*) = Tp∈-⋯-* a∈b⋯c , c∈*
  <:-valid (<:-⋯-i a<:b∈c⋯d) =
    let a∈c⋯d , b∈c⋯d = <:-valid a<:b∈c⋯d
        a<:b∈*        = <:-⋯-*   a<:b∈c⋯d
    in ∈-⇑ (∈-s-i a∈c⋯d) (<∷-⋯ (<:-refl (Tp∈-⋯-* a∈c⋯d)) a<:b∈*) ,
       ∈-⇑ (∈-s-i b∈c⋯d) (<∷-⋯ a<:b∈* (<:-refl (Tp∈-⋯-* b∈c⋯d)))
  <:-valid (<:-⇑ a<:b∈j j<∷k) =
    let a∈j , b∈j = <:-valid a<:b∈j
    in ∈-⇑ a∈j j<∷k , ∈-⇑ b∈j j<∷k

  -- Validity of type equality: types that are equal in some kind `k'
  -- inhabit `k'.
  ≃-valid : ∀ {n} {Γ : Ctx n} {a b k} →
            Γ ⊢ a ≃ b ∈ k → Γ ⊢Tp a ∈ k × Γ ⊢Tp b ∈ k
  ≃-valid (<:-antisym a<:b∈k b<:a∈k) = <:-valid a<:b∈k

  -- Subtypes inhabiting interval kinds are proper types.
  <:-⋯-* : ∀ {n} {Γ : Ctx n} {a b c d} → Γ ⊢ a <: b ∈ c ⋯ d → Γ ⊢ a <: b ∈ *
  <:-⋯-* a<:b∈c⋯d =
    let a∈c⋯d , b∈c⋯d = <:-valid a<:b∈c⋯d
    in <:-⇑ (<:-⋯-i a<:b∈c⋯d) (<∷-⋯ (<:-⊥ a∈c⋯d) (<:-⊤ b∈c⋯d))

-- Validity of kind equality: equal kinds are well-formed.
≅-valid : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ ⊢ j kd × Γ ⊢ k kd
≅-valid (<∷-antisym j<∷k k<∷j) = <∷-valid j<∷k

-- A corollary.
<:-valid-kd : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ∈ k → Γ ⊢ k kd
<:-valid-kd a<:b∈k = Tp∈-valid (proj₁ (<:-valid a<:b∈k))

----------------------------------------------------------------------
-- Strengthened versions of kind formation and kinding functionality.

-- Functionality of kind formation (strong version).
kd-[≃] : ∀ {n} {Γ : Ctx n} {a b j k} →
         kd j ∷ Γ ⊢ k kd → Γ ⊢ a ≃ b ∈ j → Γ ⊢ k Kind[ a ] ≅ k Kind[ b ]
kd-[≃] k-kd a≃b∈j = let a∈j , b∈j = ≃-valid a≃b∈j in kd-[≃′] k-kd a∈j b∈j a≃b∈j

-- Functionality of kinding (strong version).
Tp∈-[≃] : ∀ {n} {Γ : Ctx n} {a b c j k} →
          kd j ∷ Γ ⊢Tp a ∈ k → Γ ⊢ b ≃ c ∈ j →
          Γ ⊢ a [ b ] ≃ a [ c ] ∈ k Kind[ b ]
Tp∈-[≃] a∈k b≃c∈j = let b∈j , c∈j = ≃-valid b≃c∈j in Tp∈-[≃′] a∈k b∈j c∈j b≃c∈j

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
{-# OPTIONS --cubical #-}
module _ where

module _ where
  import Agda.Primitive
  open import Agda.Primitive.Cubical public

  postulate
    Path' : ∀ {ℓ} {A :     Set ℓ} → A    → A    → Set ℓ
    PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

  {-# BUILTIN PATH         Path'     #-}
  {-# BUILTIN PATHP        PathP     #-}

  infix 4 _≡_
  _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
  _≡_ {A = A} = PathP (λ _ → A)

  Path = _≡_

  refl : ∀ {a} {A : Set a} {x : A} → x ≡ x
  refl {x = x} = \ _ → x

testPath : ∀ {A : Set} {b a : A} (let H : Path b b; H = _) → ∀ i → H i ≡ b
testPath i = refl

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
open import Relation.Binary using (IsDecEquivalence)
open import Agda.Builtin.Equality

module UnifyMguF (FunctionName : Set) ⦃ isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName}) ⦄ where

{-
module UnifyMguF where

postulate
  FunctionName : Set
  instance isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName})
-}

open IsDecEquivalence isDecEquivalenceA using () renaming (_≟_ to _≟F_)

open import UnifyTermF FunctionName

open import Data.Product using (∃; _,_)
open import Data.Maybe using (Maybe; just; nothing)
open import Category.Monad using (RawMonad)
import Level
open RawMonad (Data.Maybe.monad {Level.zero})
open import Relation.Nullary using (Dec; yes; no)
open import Data.Nat using (ℕ; _≟_)
open import Function using (flip; _∘_)
open import Data.Vec using (Vec; []; _∷_)

record ⋆amgu (T : ℕ → Set) : Set where
  field amgu : ∀ {m} (s t : T m) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))

open ⋆amgu ⦃ … ⦄ public

mutual

  instance ⋆amguTerm : ⋆amgu Term
  ⋆amgu.amgu ⋆amguTerm leaf leaf acc = just acc
  ⋆amgu.amgu ⋆amguTerm leaf (function _ _) acc = nothing
  ⋆amgu.amgu ⋆amguTerm leaf (s' fork t') acc = nothing
  ⋆amgu.amgu ⋆amguTerm (s' fork t') leaf acc = nothing
  ⋆amgu.amgu ⋆amguTerm (s' fork t') (function _ _) acc = nothing
  ⋆amgu.amgu ⋆amguTerm (s1 fork s2) (t1 fork t2) acc =
                    amgu s2 t2 =<< amgu s1 t1 acc
  ⋆amgu.amgu ⋆amguTerm (function fn₁ ts₁) leaf acc = nothing
  ⋆amgu.amgu ⋆amguTerm (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc
   with fn₁ ≟F fn₂
  … | no _ = nothing
  … | yes _ with n₁ ≟ n₂
  … | no _ = nothing
  … | yes refl = amgu ts₁ ts₂ acc
  ⋆amgu.amgu ⋆amguTerm (function fn₁ ts₁) (_ fork _) acc = nothing
  ⋆amgu.amgu ⋆amguTerm (i x) (i y) (m , anil) = just (flexFlex x y)
  ⋆amgu.amgu ⋆amguTerm (i x) t     (m , anil) = flexRigid x t
  ⋆amgu.amgu ⋆amguTerm t     (i x) (m , anil) = flexRigid x t
  ⋆amgu.amgu ⋆amguTerm s     t  (n , σ asnoc r / z) =
           (λ σ -> σ ∃asnoc r / z) <$>
             amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)

  instance ⋆amguVecTerm : ∀ {N} → ⋆amgu (flip Vec N ∘ Term)
  ⋆amgu.amgu ⋆amguVecTerm [] [] acc = just acc
  ⋆amgu.amgu ⋆amguVecTerm (t₁ ∷ t₁s) (t₂ ∷ t₂s) acc = amgu t₁s t₂s =<< amgu t₁ t₂ acc

mgu : ∀ {m} -> (s t : Term m) -> Maybe (∃ (AList m))
mgu {m} s t = amgu s t (m , anil)


text:
open import FRP.JS.Nat using ( ℕ ; zero ; suc ; _≤_ ; _<_ ; _≟_ ; _+_ )
open import FRP.JS.Nat.Properties using ( ≤-impl-≯ ; <-impl-s≤ ; ≤≠-impl-< ; ≤-bot )
open import FRP.JS.Bool using ( Bool ; true ; false ; _∧_ )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )
open import FRP.JS.True using ( True ; contradiction ; dec ; yes ; no )

module FRP.JS.Array where

infixr 5 _∷_
infixr 4 _++i_

-- IArray A m n is offset m of a length n array with contents of type A

data IArray {α} (A : Set α) : ℕ → ℕ → Set α where
  [] : ∀ {n} → IArray A n n
  _∷_ : ∀ {m n} → (a : A) → (as : IArray A (suc m) n) → IArray A m n

data Array {α} (A : Set α) : Set α where
  array : ∀ {n} → (as : IArray A 0 n) → Array A

{-# COMPILED_JS IArray function(xs,v) {
  if ((xs.array.length) <= (xs.offset)) { return v["[]"](xs.offset); }
  else { return v["_∷_"](xs.offset,xs.array.length,xs.head(),xs.tail()); }
} #-}
{-# COMPILED_JS [] require("agda.array").iempty #-}
{-# COMPILED_JS _∷_ function(m) { return function(n) {
  return function(x) { return function(xs) { return xs.cons(x); }; };
}; } #-}
{-# COMPILED_JS Array function(as,v) {
  return v.array(as.length,require("agda.array").iarray(as));
} #-}
{-# COMPILED_JS array function(n) { return function(as) { return as.array; }; } #-}

length : ∀ {α A} → Array {α} A → ℕ
length (array {n} as) = n

{-# COMPILED_JS length function() { return function() { return function(as) { return as.length; }; }; } #-}

iarray : ∀ {α A} → (as : Array {α} A) → IArray A 0 (length as)
iarray (array as) = as

{-# COMPILED_JS iarray function() { return function() { return require("agda.array").iarray; }; } #-}

⟨⟩ : ∀ {α A} → Array {α} A
⟨⟩ = array []

{-# COMPILED_JS ⟨⟩ function() { return function() { return require("agda.array").empty; }; } #-}

ilookup : ∀ {α A m n} → IArray {α} A m n → ∀ i → {m≤i : True (m ≤ i)} → {i<n : True (i < n)} → A
ilookup {m = m} []       i {m≤i} {i<m} = contradiction (≤-impl-≯ {m} {i} m≤i i<m)
ilookup {m = m} (a ∷ as) i {m≤i} {i<n}
  with dec (m ≟ i)
... | yes m=i = a
... | no  m≠i = ilookup as i {<-impl-s≤ {m} {i} (≤≠-impl-< {m} {i} m≤i m≠i)} {i<n}

lookup : ∀ {α A} (as : Array {α} A) i → {i<#as : True (i < length as)} → A
lookup (array as) i {i<#as} = ilookup as i {≤-bot {i}} {i<#as}

{-# COMPILED_JS lookup function() { return function() { return function(as) { return function(i) { return function() {
  return require("agda.array").lookup(as,i);
}; }; }; }; } #-}

ilookup? : ∀ {α A m n} → IArray {α} A m n → ℕ → Maybe A
ilookup? []       i       = nothing
ilookup? (a ∷ as) zero    = just a
ilookup? (a ∷ as) (suc i) = ilookup? as i

lookup? : ∀ {α A} → Array {α} A → ℕ → Maybe A
lookup? (array as) i = ilookup? as i

{-# COMPILED_JS lookup? function() { return function() { return function(as) { return function(i) {
  return require("agda.box").box(require("agda.array").lookup(as,i));
}; }; }; } #-}

imap : ∀ {α β A B m n} → (A → B) → IArray {α} A m n → IArray {β} B m n
imap f [] = []
imap f (a ∷ as) = f a ∷ imap f as

map : ∀ {α β A B} → (A → B) → Array {α} A → Array {β} B
map f (array as) = array (imap f as)

{-# COMPILED_JS map function() { return function() { return function() { return function() {
  return function(f) { return function(as) { return as.map(f); }; };
}; }; }; } #-}

#filter : ∀ {α A m n} → (A → Bool) → IArray {α} A m n → ℕ → ℕ
#filter p []       l = l
#filter p (a ∷ as) l
 with p a
... | true  = #filter p as (1 + l)
... | false = #filter p as l

ifilter : ∀ {α A l m n} p as → IArray A l (#filter {α} {A} {m} {n} p as l)
ifilter p []       = []
ifilter p (a ∷ as)
 with p a
... | true  = a ∷ ifilter p as
... | false = ifilter p as

filter : ∀ {α A} → (A → Bool) → Array {α} A → Array A
filter p (array as) = array (ifilter p as)

{-# COMPILED_JS filter function() { return function() {
  return function(p) { return function(as) { return as.filter(p); }; };
}; } #-}

iall : ∀ {α A m n} → (A → Bool) → IArray {α} A m n → Bool
iall f []       = true
iall f (a ∷ as) = f a ∧ iall f as

all : ∀ {α A} → (A → Bool) → Array {α} A → Bool
all f (array as) = iall f as

{-# COMPILED_JS all function() { return function() {
  return function(f) { return function(as) { return as.every(f); }; };
}; } #-}

_≟i[_]_ : ∀ {α β A B l m n} → IArray {α} A l m → (A → B → Bool) → IArray {β} B l n → Bool
[]       ≟i[ p ] []       = true
(a ∷ as) ≟i[ p ] (b ∷ bs) = (p a b) ∧ (as ≟i[ p ] bs)
as       ≟i[ p ] bs       = false

_≟[_]_ : ∀ {α β A B} → Array {α} A → (A → B → Bool) → Array {β} B → Bool
array as ≟[ p ] array bs = as ≟i[ p ] bs

{-# COMPILED_JS _≟[_]_ function() { return function() { return function() { return function() {
  return function(as) { return function(p) { return function(bs) {
    return require("agda.array").equals(as,bs,function(a,b) { return p(a)(b); });
  }; }; };
}; }; }; } #-}

_⊆i[_]_ : ∀ {α β A B l m n} → IArray {α} A l m → (A → B → Bool) → IArray {β} B l n → Bool
[]       ⊆i[ p ] bs       = true
(a ∷ as) ⊆i[ p ] []       = false
(a ∷ as) ⊆i[ p ] (b ∷ bs) = (p a b) ∧ (as ⊆i[ p ] bs)

_⊆[_]_ : ∀ {α β A B} → Array {α} A → (A → B → Bool) → Array {β} B → Bool
array as ⊆[ p ] array bs = as ⊆i[ p ] bs

{-# COMPILED_JS _⊆[_]_ function() { return function() { return function() { return function() {
  return function(as) { return function(p) { return function(bs) {
    return require("agda.array").subseteq(as,bs,function(a,b) { return p(a)(b); });
  }; }; };
}; }; }; } #-}

igrow : ∀ {α A l m n} → IArray {α} A l n → IArray A (l + m) (n + m)
igrow []       = []
igrow (a ∷ as) = a ∷ igrow as

_++i_ : ∀ {α A l m n} → IArray {α} A l m → IArray A 0 n → IArray A l (n + m)
[]       ++i bs = igrow bs
(a ∷ as) ++i bs = a ∷ (as ++i bs)

_++_ :  ∀ {α A} → Array {α} A → Array {α} A → Array {α} A
array as ++ array bs = array (as ++i bs)

{-# COMPILED_JS _++_ function() { return function() {
  return function(as) { return function(bs) { return as.concat(bs); }; };
}; } #-}

-- Surface syntax, e.g. ⟨ 1 , 2 , 3 ⟩ : Array ℕ

infix 3 ⟨_
infixr 4 _,_
infixr 5 _⟩

data Sugar {α} (A : Set α) : Set α where
  ε : Sugar A
  _,_ : A → Sugar A → Sugar A

_⟩ : ∀ {α A} → A → Sugar {α} A
a ⟩ = (a , ε)

slength : ∀ {α A} → Sugar {α} A → ℕ → ℕ
slength ε        m = m
slength (a , as) m = slength as (1 + m)

desugar : ∀ {α A m} as → IArray A m (slength {α} {A} as m)
desugar ε        = []
desugar (a , as) = a ∷ desugar as

⟨_ : ∀ {α A} → Sugar {α} A → Array A
⟨ as = array (desugar as)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module main where

import parse
open import lib
open import huffman-types
import huffman

module parsem = parse huffman.gratr2-nt ptr
open parsem
open parsem.pnoderiv huffman.rrs huffman.huffman-rtn
open import run ptr
open noderiv {- from run.agda -}

{- imports for Huffman trees and also
   Braun trees specialized to store Huffman trees
   with lower frequency ones nearer the root -}
open import huffman-tree
import braun-tree as bt
open bt huffman-tree ht-compare

--open import braun-tree huffman-tree ht-compare

pqueue : ℕ → Set
pqueue = braun-tree

pq-empty : pqueue 0
pq-empty = bt-empty

pq-insert : ∀ {n : ℕ} → huffman-tree → pqueue n → pqueue (suc n)
pq-insert = bt-insert

pq-remove-min : ∀ {p : ℕ} → pqueue (suc p) → huffman-tree × pqueue p
pq-remove-min = bt-remove-min

data output-type : Set where
  encode-output : string → string → string → string → output-type
  decode-output : string → output-type
  error-output : string → output-type -- error message if there is an error

inc-frequency : word → trie ℕ → trie ℕ
inc-frequency w t with trie-lookup t w
inc-frequency w t | nothing = trie-insert t w 1
inc-frequency w t | just c = trie-insert t w (suc c)

compute-frequencies : words → trie ℕ → trie ℕ
compute-frequencies (WordsStart w) t = inc-frequency w t
compute-frequencies (WordsNext w ww) t = compute-frequencies ww (inc-frequency w t)

inc-frequency-nonempty : ∀(w : word)(t : trie ℕ) → trie-nonempty (inc-frequency w t) ≡ tt
inc-frequency-nonempty w t with trie-lookup t w
inc-frequency-nonempty w t | nothing = trie-insert-nonempty t w 1
inc-frequency-nonempty w t | just c = trie-insert-nonempty t w (suc c)

compute-frequencies-nonempty : ∀(ws : words)(t : trie ℕ) → trie-nonempty (compute-frequencies ws t) ≡ tt
compute-frequencies-nonempty (WordsNext w ww) t = compute-frequencies-nonempty ww (inc-frequency w t)
compute-frequencies-nonempty (WordsStart w) t = inc-frequency-nonempty w t

build-huffman-pqueue : (l : 𝕃 (string × ℕ)) → pqueue (length l)
build-huffman-pqueue [] = pq-empty
build-huffman-pqueue ((s , f) :: l) = pq-insert (ht-leaf s f) (build-huffman-pqueue l)

-- where we call this function, we have enough evidence to prove the Braun tree is nonempty
process-huffman-pqueue : ∀{n} → n =ℕ 0 ≡ ff → pqueue n → huffman-tree
process-huffman-pqueue{0} () b
process-huffman-pqueue{suc n} _ t with pq-remove-min t
process-huffman-pqueue{suc 0} _ t | h , _ = h
process-huffman-pqueue{suc (suc n)} _ _ | h , t with pq-remove-min t
process-huffman-pqueue{suc (suc n)} _ _ | h , _ | h' , t =
  process-huffman-pqueue{suc n} refl (pq-insert (ht-node ((ht-frequency h) + (ht-frequency h')) h h') t)

build-mappingh : huffman-tree → trie string → 𝕃 char → trie string
build-mappingh (ht-leaf s _) m l = trie-insert m s (𝕃char-to-string (reverse l))
build-mappingh (ht-node _ h1 h2) m l =
  build-mappingh h2 (build-mappingh h1 m ('0' :: l)) ('1' :: l)

build-mapping : huffman-tree → trie string
build-mapping h = build-mappingh h empty-trie []

encode-word : trie string → word → string
encode-word t w with trie-lookup t w
encode-word t w | nothing = "error"
encode-word t w | just s = s

encode-words : trie string → words → string
encode-words t (WordsNext w ww) = encode-word t w ^ encode-words t ww
encode-words t (WordsStart w) = encode-word t w

data code-tree : Set where
  ct-empty : code-tree
  ct-leaf : string → code-tree
  ct-node : code-tree → code-tree → code-tree

flip-digit : digit → digit
flip-digit Zero = One
flip-digit One = Zero

sub-ct : digit → code-tree → code-tree
sub-ct _ ct-empty = ct-empty
sub-ct _ (ct-leaf _) = ct-empty
sub-ct Zero (ct-node t1 t2) = t1
sub-ct One (ct-node t1 t2) = t2

ct-node-digit : digit → code-tree → code-tree → code-tree
ct-node-digit Zero t1 t2 = ct-node t1 t2
ct-node-digit One t1 t2 = ct-node t2 t1

ct-insert : code-tree → code → code-tree
ct-insert t (Code s (BvlitStart d)) =
  -- child d of the new tree is the new leaf, and the other child is the other subtree of t
  ct-node-digit d (ct-leaf s) (sub-ct (flip-digit d) t)
ct-insert t (Code s (BvlitCons d v)) =
  -- child d of the new tree is obtained recursively and the other child is the other subtree of t
  ct-node-digit d (ct-insert (sub-ct d t) (Code s v)) (sub-ct (flip-digit d) t)

make-code-tree : code-tree → codes → code-tree
make-code-tree t (CodesNext c cs) = make-code-tree (ct-insert t c) cs
make-code-tree t (CodesStart c) = ct-insert t c

decode-stringh : code-tree → code-tree → bvlit → string
decode-stringh orig n (BvlitCons d v) with sub-ct d n
decode-stringh orig n (BvlitCons d v) | ct-leaf s = s ^ " " ^ (decode-stringh orig orig v)
decode-stringh orig n (BvlitCons d v) | ct-empty = "error\n"
decode-stringh orig n (BvlitCons d v) | n' = decode-stringh orig n' v
decode-stringh orig n (BvlitStart d) with sub-ct d n
decode-stringh orig n (BvlitStart d) | ct-leaf s = s ^ "\n"
decode-stringh orig n (BvlitStart d) | _ = "error\n"

decode-string : code-tree → bvlit → string
decode-string t v = decode-stringh t t v

process-cmd : cmd → output-type
process-cmd (Encode ww) = step (compute-frequencies ww empty-trie) (compute-frequencies-nonempty ww empty-trie)
  where step : (t : trie ℕ) → trie-nonempty t ≡ tt → output-type
        step t nonempty-t =
         let s1 = trie-to-string " -> " ℕ-to-string t in
         let m = trie-mappings t in
         let wt = build-huffman-pqueue m in
         let h = process-huffman-pqueue (is-empty-ff-length (trie-mappings t) (trie-mappings-nonempty t nonempty-t)) wt in
         let s2 = ht-to-string h in
         let mp = build-mapping h in
         let s3 = trie-to-string " <- " (λ s → s) mp in
         let s4 = "! " ^ s3 ^ (encode-words mp ww) in
           encode-output s1 s2 s3 s4
process-cmd (Decode cs v) =
  let ct = make-code-tree ct-empty cs in
  let s = decode-string ct v in
    decode-output s

process-start : start → output-type
process-start (File c) = process-cmd c

process : Run → output-type
process (ParseTree (parsed-start p) :: []) = process-start p
process r = error-output ("Parsing failure (run with -" ^ "-showParsed).\n")

putStrRunIf : 𝔹 → Run → IO ⊤
putStrRunIf tt r = putStr (Run-to-string r) >> putStr "\n"
putStrRunIf ff r = return triv

doOutput : output-type → string → IO ⊤
doOutput (error-output s) basename = putStr ("Error: " ^ s ^ "\n")
doOutput (encode-output s1 s2 s3 s4) basename =
  writeFile (basename ^ "-frequencies.txt") s1 >>
  writeFile (basename ^ ".gv") s2 >>
  writeFile (basename ^ "-mapping.txt") s3 >>
  writeFile (basename ^ ".huff") s4
doOutput (decode-output s) basename = writeFile (basename ^ "-decoded.txt") s

processArgs : (showRun : 𝔹) → (showParsed : 𝔹) → 𝕃 string → IO ⊤
processArgs showRun showParsed (input-filename :: []) = (readFiniteFile input-filename) >>= processText
  where processText : string → IO ⊤
        processText x with runRtn (string-to-𝕃char x)
        processText x | s with s
        processText x | s | inj₁ cs = putStr "Characters left before failure : " >> putStr (𝕃char-to-string cs) >> putStr "\nCannot proceed to parsing.\n"
        processText x | s | inj₂ r with putStrRunIf showRun r | rewriteRun r
        processText x | s | inj₂ r | sr | r' with putStrRunIf showParsed r'
        processText x | s | inj₂ r | sr | r' | sr' = sr >> sr' >> doOutput (process r') (base-filename input-filename)

processArgs showRun showParsed ("--showRun" :: xs) = processArgs tt showParsed xs
processArgs showRun showParsed ("--showParsed" :: xs) = processArgs showRun tt xs
processArgs showRun showParsed (x :: xs) = putStr ("Unknown option " ^ x ^ "\n")
processArgs showRun showParsed [] = putStr "Please run with the name of a file to process.\n"

main : IO ⊤
main = getArgs >>= processArgs ff ff

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; sym; refl; subst; trans; cong)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness; fromWitness)
open import Function using (_∘_)

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

open Maybe using (nothing; just)
open Empty using (⊥; ⊥-elim)
open Unit using (⊤; tt)
open ℕ using (ℕ; zero; suc)
open Product using (Σ-syntax; ∃-syntax; _×_; _,_; proj₂; proj₁)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Relation.Binary.PropositionalEquality.≡-Reasoning

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

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

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

data _≔_⊗_ : Ctx idxs → Ctx idxs → Ctx idxs → Set where
  []  : [] ≔ [] ⊗ []
  _,_ : Γ ≔ Δ ⊗ Ξ → x ≔ y ∙² z → (Γ -, x) ≔ (Δ -, y) ⊗ (Ξ -, z)

ε : ∀ {idxs : Idxs n} → Ctx idxs
ε {idxs = []} = []
ε {idxs = _ -, _} = ε -, (0∙ , 0∙)

⊗-get : {idxs : Idxs n} {Γ Δ Ξ : Ctx idxs} (i : Fin n) → Γ ≔ Δ ⊗ Ξ → All.lookup i Γ ≔ All.lookup i Δ ∙² All.lookup i Ξ
⊗-get zero (Γ≔ , x≔) = x≔
⊗-get (suc i) (Γ≔ , x) = ⊗-get i Γ≔

⊗-idˡ : {idxs : Idxs n} {Γ : Ctx idxs} → Γ ≔ ε {idxs = idxs} ⊗ Γ
⊗-idˡ {Γ = []} = []
⊗-idˡ {Γ = Γ -, x} = ⊗-idˡ , ∙²-idˡ

⊗-unique : {Γ Γ' Δ Ξ  : Ctx idxs} → Γ' ≔ Δ ⊗ Ξ → Γ ≔ Δ ⊗ Ξ → Γ' ≡ Γ
⊗-unique [] [] = refl
⊗-unique (Γ'≔ , x'≔) (Γ≔ , x≔) rewrite ⊗-unique Γ'≔ Γ≔ | ∙²-unique x'≔ x≔ = refl

⊗-uniqueˡ : {Γ Δ Δ' Ξ  : Ctx idxs} → Γ ≔ Δ' ⊗ Ξ → Γ ≔ Δ ⊗ Ξ → Δ' ≡ Δ
⊗-uniqueˡ [] [] = refl
⊗-uniqueˡ (Δ'≔ , y'≔) (Δ≔ , y≔) rewrite ⊗-uniqueˡ Δ'≔ Δ≔ | ∙²-uniqueˡ y'≔ y≔ = refl

⊗-comm : {Γ Δ Ξ : Ctx idxs} → Γ ≔ Δ ⊗ Ξ → Γ ≔ Ξ ⊗ Δ
⊗-comm [] = []
⊗-comm (Γ≔ , x≔) = ⊗-comm Γ≔ , ∙²-comm x≔

⊗-assoc : {Γₘ Γₗ Γᵣ Γₗₗ Γₗᵣ : Ctx idxs}
        → Γₘ ≔ Γₗ ⊗ Γᵣ → Γₗ ≔ Γₗₗ ⊗ Γₗᵣ → Σ[ Γᵣ' ∈ Ctx idxs ] (Γₘ ≔ Γₗₗ ⊗ Γᵣ' × Γᵣ' ≔ Γₗᵣ ⊗ Γᵣ)
⊗-assoc [] [] = [] , [] , []
⊗-assoc (Γₘ≔ , xₘ≔) (Γₗ≔ , xₗ≔) with ⊗-assoc Γₘ≔ Γₗ≔ | ∙²-assoc xₘ≔ xₗ≔
... | (_ , Γₘ'≔ , Γᵣ'≔)  | (_ , xₘ'≔ , xᵣ'≔) = _ , ((Γₘ'≔ , xₘ'≔) , (Γᵣ'≔ , xᵣ'≔))

⊗-assoc⁻¹ : ∀ {x y z u v : Ctx idxs} → x ≔ y ⊗ z → z ≔ u ⊗ v → ∃[ w ] (x ≔ w ⊗ v × w ≔ y ⊗ u)
⊗-assoc⁻¹ a b = let _ , a' , b' = ⊗-assoc (⊗-comm a) (⊗-comm b) in _ , ⊗-comm a' , ⊗-comm b'

⊗-comp : {Γ Δₗ Δᵣ Δ Ξ Θ : Ctx idxs}
       → Γ ≔ Δₗ ⊗ Ξ → Ξ ≔ Δᵣ ⊗ Θ
       → Γ ≔ Δ  ⊗ Θ → Δ ≔ Δₗ ⊗ Δᵣ
⊗-comp l≔ r≔ Γ≔ with ⊗-assoc (⊗-comm l≔) (⊗-comm r≔)
⊗-comp l≔ r≔ Γ≔ | _ , Γ'≔ , R'≔ rewrite ⊗-uniqueˡ Γ≔ (⊗-comm Γ'≔) = ⊗-comm R'≔

⊗-idʳ : {Γ : Ctx idxs} → Γ ≔ Γ ⊗ ε
⊗-idʳ = ⊗-comm ⊗-idˡ

⊗-mut-cancel : ∀ {x y y' z : Ctx idxs} → x ≔ y ⊗ z → z ≔ y' ⊗ x → x ≡ z
⊗-mut-cancel [] [] = refl
⊗-mut-cancel (Γ≔ , x≔) (Ξ≔ , z≔) rewrite ⊗-mut-cancel Γ≔ Ξ≔ | ∙²-mut-cancel x≔ z≔ = refl

∋-≡Idx : {idxs : Idxs n} {i : Fin n} {Γ Δ : Ctx idxs} {x : Usage idx ²}
       → Γ ∋[ i ] x ▹ Δ → Vec.lookup idxs i ≡ idx
∋-≡Idx (zero x) = refl
∋-≡Idx (suc s) rewrite ∋-≡Idx s = refl

∋-≡Type : γ ∋[ i ] t → Vec.lookup γ i ≡ t
∋-≡Type zero = refl
∋-≡Type (suc t) rewrite ∋-≡Type t = refl

≡Type-∋ : Vec.lookup γ i ≡ t → γ ∋[ i ] t
≡Type-∋ {γ = _ -, _} {i = zero} refl = zero
≡Type-∋ {γ = _ -, _} {i = suc i} eq = suc (≡Type-∋ eq)

∋-⊗ : {Γ Ξ : Ctx idxs}
    → Γ ∋[ i ] x ▹ Ξ
    → Σ[ Δ ∈ Ctx idxs ]
      (Γ ≔ Δ ⊗ Ξ × Δ ∋[ i ] x ▹ ε {idxs = idxs})
∋-⊗ (zero x) = _ , (⊗-idˡ , x) , zero ∙²-idʳ
∋-⊗ (suc s) with ∋-⊗ s
∋-⊗ (suc s) | _ , Γ≔ , Δ≔ = _ , (Γ≔ , ∙²-idˡ) , suc Δ≔

⊗-∋ : {Γ Δ Ξ : Ctx idxs}
    → Γ ≔ Δ ⊗ Ξ
    → Δ ∋[ i ] x ▹ ε {idxs = idxs}
    → Γ ∋[ i ] x ▹ Ξ
⊗-∋ (sp , s) (zero x) rewrite ⊗-unique sp ⊗-idˡ | ∙²-unique x ∙²-idʳ = zero s
⊗-∋ (sp , s) (suc only) rewrite ∙²-unique s ∙²-idˡ = suc (⊗-∋ sp only)

∋-ℓ∅ : {idxs : Idxs n} {Γ : Ctx idxs} {i : Fin n} {idx : Idx}→ Vec.lookup idxs i ≡ idx → Γ ∋[ i ] ℓ∅ {idx} ▹ Γ
∋-ℓ∅ {Γ = _ -, _} {i = zero} refl = zero ∙²-idˡ
∋-ℓ∅ {Γ = _ -, _} {i = suc i} eq = suc (∋-ℓ∅ eq)

-- TODO: deprecate, convert to context first
∋-uniqueʳ : {i : Fin n} {idxs : Idxs n} {Γ Δ Ξ : Ctx idxs}
          → Γ ∋[ i ] x ▹ Δ → Γ ∋[ i ] x ▹ Ξ → Δ ≡ Ξ
∋-uniqueʳ (zero a) (zero b) rewrite ∙²-uniqueˡ (∙²-comm a) (∙²-comm b) = refl
∋-uniqueʳ (suc a) (suc b) rewrite ∋-uniqueʳ a b = refl

-- TODO: deprecate, convert to context first
∋-uniqueˡ : Γ ∋[ i ] x ▹ Δ → Ξ ∋[ i ] x ▹ Δ → Γ ≡ Ξ
∋-uniqueˡ (zero a) (zero b) rewrite ∙²-unique a b = refl
∋-uniqueˡ (suc a) (suc b) rewrite ∋-uniqueˡ a b = refl

∋-lookup-≡ : Γ ∋[ i ] x ▹ Δ → All.lookup i Γ ≔ x ∙² All.lookup i Δ
∋-lookup-≡ {Δ = _ -, _} (zero x) = x
∋-lookup-≡ {Δ = _ -, _} (suc s) = ∋-lookup-≡ s

∋-lookup-≢ : Γ ∋[ i ] x ▹ Δ → ∀ j → j ≢ i → All.lookup j Γ ≡ All.lookup j Δ
∋-lookup-≢ (zero x) zero j≢i = ⊥-elim (j≢i refl)
∋-lookup-≢ (suc xati) zero j≢i = refl
∋-lookup-≢ (zero x) (suc j) j≢i = refl
∋-lookup-≢ (suc xati) (suc j) j≢i = ∋-lookup-≢ xati j (j≢i ∘ cong suc)

∙²-⊗ : {Γ Δ Ξ : Ctx idxs}
     → Γ ∋[ i ] x ▹ ε → Δ ∋[ i ] y ▹ ε → Ξ ∋[ i ] z ▹ ε
     → x ≔ y ∙² z → Γ ≔ Δ ⊗ Ξ
∙²-⊗ (zero x) (zero y) (zero z) sp
  rewrite ∙²-unique x ∙²-idʳ | ∙²-unique y ∙²-idʳ | ∙²-unique z ∙²-idʳ = ⊗-idˡ , sp
∙²-⊗ (suc Γ≔) (suc Δ≔) (suc Ξ≔) sp = ∙²-⊗ Γ≔ Δ≔ Ξ≔ sp , ∙²-idˡ

diamond : {Γ Ξ Ψ : Ctx idxs}
        → i ≢ j
        → Γ ∋[ j ] x ▹ Ξ
        → Γ ∋[ i ] y ▹ Ψ
        → Σ[ Θ ∈ Ctx idxs ]
        ( Ξ ∋[ i ] y ▹ Θ
        × Ψ ∋[ j ] x ▹ Θ
        )
diamond i≢j (zero _) (zero _) = ⊥-elim (i≢j refl)
diamond i≢j (zero x) (suc ∋i) = _ , suc ∋i , zero x
diamond i≢j (suc ∋j) (zero x) = _ , zero x , suc ∋j
diamond i≢j (suc ∋j) (suc ∋i) with diamond (i≢j ∘ cong suc) ∋j ∋i
diamond i≢j (suc ∋j) (suc ∋i) | _ , ∋i' , ∋j' = _ , suc ∋i' , suc ∋j'

outer-diamond : {Γ Ξ Ψ Θ ΞΔ Δ ΨΔ : Ctx idxs}
              → i ≢ j
              → Γ ∋[ i ] x ▹ Ξ → Γ ∋[ j ] y ▹ Ψ
              → Ξ ∋[ j ] y ▹ Θ → Ψ ∋[ i ] x ▹ Θ
              → Ξ ≔ ΞΔ ⊗ Δ → Ψ ≔ ΨΔ ⊗ Δ
              → Σ[ ΘΔ ∈ Ctx idxs ] (Θ ≔ ΘΔ ⊗ Δ)
outer-diamond i≢j (zero _) (zero _) (zero _) (zero _) a b = ⊥-elim (i≢j refl)
outer-diamond i≢j (zero x₁) (suc ∋j) (suc ∈j) (zero x) (as , a) (bs , b) = _ , (bs , a)
outer-diamond i≢j (suc ∋i) (zero ∋j) (zero ∈j) (suc ∈i) (as , a) (bs , b) = _ , (as , b)
outer-diamond i≢j (suc ∋i) (suc ∋j) (suc ∈j) (suc ∈i) (as , a) (bs , b) with outer-diamond (i≢j ∘ cong suc) ∋i ∋j ∈j ∈i as bs
outer-diamond i≢j (suc ∋i) (suc ∋j) (suc ∈j) (suc ∈i) (as , a) (bs , b) | _ , s = _ , (s , a)

reverse : {Γ ΓΞ Ξ ΞΨ Ψ : Ctx idxs}
        → Γ ≔ ΓΞ ⊗ Ξ
        → Ξ ≔ ΞΨ ⊗ Ψ
        → Σ[ Θ ∈ Ctx idxs ]
        ( Γ ≔ ΞΨ ⊗ Θ
        × Θ ≔ ΓΞ ⊗ Ψ
        )
reverse Γ≔ΓΞ∙Ξ Ξ≔ΞΨ∙Ψ =
  let _ , Γ≔ΞΨ∙Θ , Θ≔Ψ∙ΓΞ = ⊗-assoc (⊗-comm Γ≔ΓΞ∙Ξ) Ξ≔ΞΨ∙Ψ in
  _ , Γ≔ΞΨ∙Θ , ⊗-comm Θ≔Ψ∙ΓΞ

boil : {Γ Ξ ΞΨ Θ Ψ ΘΨ : Ctx idxs}
     → Γ ∋[ i ] x ▹ Θ
     → Γ ∋[ i ] y ▹ Ξ
     → Ξ ≔ ΞΨ ⊗ Ψ
     → Θ ≔ ΘΨ ⊗ Ψ
     → All.lookup i ΘΨ ≡ ℓ∅
     → ∃[ z ] (x ≔ y ∙² z)
boil {i = zero} (zero a) (zero b) (_ , c) (_ , d) refl rewrite ∙²-unique d ∙²-idˡ with ∙²-assoc⁻¹ b c
boil {i = zero} (zero a) (zero b) (_ , c) (_ , d) refl | _ , e , f rewrite ∙²-uniqueˡ e a = _ , f
boil {i = suc i} (suc a) (suc b) (c , _) (d , _) eq = boil a b c d eq

split : x ≔ y ∙² z
      → Γ ∋[ i ] x ▹ Ξ
      → ∃[ Δ ] (Γ ∋[ i ] y ▹ Δ × Δ ∋[ i ] z ▹ Ξ)
split s (zero x) = let _ , x' , s' = ∙²-assoc x s in _ , zero x' , zero s'
split s (suc x) with split s x
split s (suc x) | _ , y , z = _ , suc y , suc z

split-ℓ∅ : {Γ ΓΨ Ψ ΓΘ Θ ΘΨ : Ctx idxs}
        → Γ ≔ ΓΨ ⊗ Ψ
        → Γ ≔ ΓΘ ⊗ Θ
        → Θ ≔ ΘΨ ⊗ Ψ
        → All.lookup i ΓΨ ≡ ℓ∅
        → All.lookup i ΓΘ ≡ ℓ∅ × All.lookup i ΘΨ ≡ ℓ∅
split-ℓ∅ {i = zero} (a , x) (b , y) (c , z) refl rewrite ∙²-unique x ∙²-idˡ with ∙²-mut-cancel y z
split-ℓ∅ {i = zero} (a , x) (b , y) (c , z) refl | refl = ∙²-uniqueˡ y ∙²-idˡ , ∙²-uniqueˡ z ∙²-idˡ
split-ℓ∅ {i = suc i} (a , _) (b , _) (c , _) eq = split-ℓ∅ a b c eq

⊢-⊗ : {γ : PreCtx n} {idxs : Idxs n} {Γ Ξ : Ctx idxs} → γ ； Γ ⊢ P ▹ Ξ → Σ[ Δ ∈ Ctx idxs ] (Γ ≔ Δ ⊗ Ξ)
⊢-⊗ 𝟘 = ε , ⊗-idˡ
⊢-⊗ (ν t m μ ⊢P) with ⊢-⊗ ⊢P
⊢-⊗ (ν t m μ ⊢P) | (_ -, _) , (P≔ , _) = _ , P≔
⊢-⊗ ((_ , x) ⦅⦆ ⊢P) with ⊢-⊗ ⊢P
⊢-⊗ ((_ , x) ⦅⦆ ⊢P) | (_ -, _) , (P≔ , _) =
  let _ , x≔ , _ = ∋-⊗ x
      _ , xP≔ , _ = ⊗-assoc⁻¹ x≔ P≔
   in _ , xP≔
⊢-⊗ ((_ , x) ⟨ _ , y ⟩ ⊢P) =
  let _ , x≔ , _ = ∋-⊗ x
      _ , y≔ , _ = ∋-⊗ y
      _ , P≔ = ⊢-⊗ ⊢P
      _ , xy≔ , _ = ⊗-assoc⁻¹ x≔ y≔
      _ , Pxy≔ , _ = ⊗-assoc⁻¹ xy≔ P≔
   in _ , Pxy≔
⊢-⊗ (⊢P ∥ ⊢Q) =
  let _ , P≔ = ⊢-⊗ ⊢P
      _ , Q≔ = ⊢-⊗ ⊢Q
      _ , PQ≔ , _ = ⊗-assoc⁻¹ P≔ Q≔
   in _ , PQ≔

ctx-insert : (i : Fin (suc n)) → Usage idx ² → Ctx idxs → Ctx (Vec.insert idxs i idx)
ctx-insert zero xs' Γ = Γ -, xs'
ctx-insert (suc i) xs' (Γ -, xs) = ctx-insert i xs' Γ -, xs

ctx-remove : Ctx idxs → (i : Fin (suc n)) → Ctx (Vec.remove idxs i)
ctx-remove (Γ -, _) zero = Γ
ctx-remove (Γ -, ys -, xs) (suc i) = ctx-remove (Γ -, ys) i -, xs

ctx-update : (i : Fin n) → Usage (Vec.lookup idxs i) ² → Ctx idxs → Ctx idxs
ctx-update zero m' (ms -, m) = ms -, m'
ctx-update (suc i) m' (ms -, m) = ctx-update i m' ms -, m

fromFin : {γ : PreCtx n} {idxs : Idxs n} {Γ : Ctx idxs}
        → ∀ i
        → {y z : Usage (Vec.lookup idxs i) ²}
        → All.lookup i Γ ≔ y ∙² z
        → γ ； Γ ∋[ i ] Vec.lookup γ i ； y ▹ ctx-update i z Γ
fromFin {γ = γ -, t} {Γ = Γ -, x} zero split = zero , (zero split)
fromFin {γ = γ -, t} {Γ = Γ -, x} (suc i) split = there (fromFin i split)

#_ : {γ : PreCtx n} {idxs : Idxs n} {Γ : Ctx idxs}
   → ∀ m {m<n : True (m ℕₚ.<? n)}
   → let i = Fin.fromℕ< (toWitness m<n)
     in {y : Usage (Vec.lookup idxs i) ²}
   → {check : True (∙²-computeʳ (All.lookup i Γ) y)}
   → let z , _ = toWitness check
     in γ ； Γ ∋[ i ] Vec.lookup γ i ； y ▹ ctx-update i z Γ
(# m) {m<n} {check = check} =
  let _ , split = toWitness check
  in fromFin (Fin.fromℕ< (toWitness m<n)) split

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:
module Examples where

open import Data.List using ([]; _∷_)
open import Data.Fin using () renaming (zero to fzero)

open import Relation.Binary using (Rel)

open import Level using () renaming (zero to lzero)

open import Syntax
open import Theory

module NatBool where
  data Gr : Set where
    nat : Gr
    bool : Gr

  data Func : Set where
    zero plus true false not : Func

  open PType Gr

  sorting : Func -> Sorting
  sorting zero = record { dom = Unit ; cod = ⌊ nat ⌋ }
  sorting plus = record { dom = ⌊ nat ⌋ * ⌊ nat ⌋ ; cod = ⌊ nat ⌋ }
  sorting true = record { dom = Unit ; cod = ⌊ bool ⌋ }
  sorting false = record { dom = Unit ; cod = ⌊ bool ⌋ }
  sorting not = record { dom = ⌊ bool ⌋ ; cod = ⌊ bool ⌋ }

  Sg : Signature lzero lzero
  Sg = record { Gr = Gr ; Func = Func ; sorting = sorting }

  open Term Sg

  data Ax : forall Γ A -> Rel (Γ ⊢ A) lzero where
    not-true≡false : Ax [] ⌊ bool ⌋ (func not (func true unit)) (func false unit)
    not-false≡true : Ax [] ⌊ bool ⌋ (func not (func false unit)) (func true unit)
    plus-identityˡ : Ax (⌊ nat ⌋ ∷ []) ⌊ nat ⌋
      (func plus (pair (func zero unit) var))
      var

  Th : Theory lzero lzero lzero
  Th = record { Sg = Sg ; Ax = Ax }

  open Theory.Theory Th

  import Relation.Binary.Reasoning.Setoid as S

  thm1 : forall {Γ} -> Γ ⊢ func not (func true unit) ≡ func false unit
  thm1 =
    begin
      func not (func true unit)
    ≈˘⟨ cong/func (cong/func (comm/unit _ _ _)) ⟩
      func not (func true (unit [ ! ]))
    ≈˘⟨ cong/func (comm/func _ _ _ _ _) ⟩
      func not (func true unit [ ! ])
    ≈˘⟨ comm/func _ _ _ _ _ ⟩
      func not (func true unit) [ ! ]
    ≈⟨ cong/sub refl (ax not-true≡false) ⟩
      func false unit [ ! ]
    ≈⟨ comm/func _ _ _ _ _ ⟩
      func false (unit [ ! ])
    ≈⟨ cong/func (comm/unit _ _ _) ⟩
      func false unit
    ∎
    where open S TermSetoid

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


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

module NfCBPVLaws where

open import Library hiding (_×̇_)

open import NfCBPV

-- NB: mon⁺ is a comonad coalgebra

module MonIsComonadCoalgebra where

  mon-id : ∀ (P : Ty⁺) {Γ} (a : ⟦ P ⟧⁺ Γ) → mon⁺ P a ⊆-refl ≡ a
  mon-id (base o)  x         = {!monVar-id!}
  mon-id (P₁ ×̇ P₂) (a₁ , a₂) = cong₂ _,_ (mon-id P₁ a₁) (mon-id P₂ a₂)
  mon-id (Σ̇ I Ps)  (i  ,  a) = cong (i ,_) (mon-id (Ps i) a)
  mon-id (□̇ N)     f         = funExtH (funExt (λ τ → cong f {!!})) -- ⊆-trans ⊆-refl τ ≡ τ

  -- Identity: extract ∘ mon⁺ ≡ id

  extract∘mon : ∀ (P : Ty⁺) {Γ} → extract ∘ mon⁺ P ≗ id {A = ⟦ P ⟧⁺ Γ}
  extract∘mon = mon-id

  -- Associativity: □-map (mon⁺ P) ∘ mon⁺ P ≡ duplicate ∘ mon⁺ P

  mon∘mon : ∀ (P : Ty⁺) {Γ} (a : ⟦ P ⟧⁺ Γ) {Δ} {τ : Γ ⊆ Δ} {Φ} {τ' : Δ ⊆ Φ} →
    mon⁺ P (mon⁺ P a τ) τ' ≡ mon⁺ P a (⊆-trans τ τ')
  mon∘mon (base o)  x         = {!!}  -- monVar∘monVar
  mon∘mon (P₁ ×̇ P₂) (a₁ , a₂) = cong₂ _,_ (mon∘mon P₁ a₁) (mon∘mon P₂ a₂)
  mon∘mon (Σ̇ I Ps)  (i  , a)  = cong (i ,_) (mon∘mon (Ps i) a)
  mon∘mon (□̇ N)     f         = {!!}  -- □-mon∘□-mon

  map-mon∘mon : ∀ (P : Ty⁺) {Γ} → □-map (mon⁺ P) ∘ mon⁺ P ≗ duplicate ∘ mon⁺ P {Γ}
  map-mon∘mon P a = funExtH $ funExt λ τ → funExtH $ funExt λ τ' → mon∘mon P a

module RunIsMonadAlgebra where

  -- Identity: run⁻ N ∘ return ≡ id

  -- Associativity: run⁻ N ∘ ◇-map (run⁻ N) ≡ run⁻ N ∘ join

monNe : ∀{N} → Mon (Ne N)
monNe = {!!}

monNf : ∀{N} → Mon (Nf N)
monNf = {!!}

-- ◇ preserves monotonicity
------------------------------------------------------------------------

-- This needs weakening of neutrals

◇-mon : Mon A → Mon (◇ A)
◇-mon mA (return a) τ = return (mA a τ)
◇-mon mA (bind u c) τ = bind (monNe u τ) (◇-mon mA c (refl ∷ τ)) -- need monotonicity of Ne
◇-mon mA (case x t) τ = case (monVar x τ) (λ i → ◇-mon mA (t i) (refl ∷ τ))
◇-mon mA (split x c) τ = split (monVar x τ) (◇-mon mA c (refl ∷ refl ∷ τ))

-- From ◇-mon we get □-run

□-run : Run B → Run (□ B)
□-run rB c = rB ∘ ◇-map extract ∘ ◇-mon □-mon c

-- Run for Nf?
-- Seems to need a category of renamings rather just OPE

bindNf : ∀ {N} {Γ} {P} →
         Ne (◇̇ P) Γ → Nf N (P ∷ Γ) → Nf N Γ
bindNf u (ret v) = ret (bind u v)
bindNf u (ne n)  = ne  (bind u n)
bindNf u (rec t) = rec λ i → bindNf u (t i)
bindNf u (abs t) = abs (bindNf (monNe u (_ ∷ʳ ⊆-refl)) (monNf t {!!}))
  -- The remaining goal Q ∷ P ∷ Γ ⊆ P ∷ Q ∷ Γ
  -- cannot be filled since OPEs do not support swap.

runNf : ∀{N} → ◇ (Nf N) →̇ Nf N
runNf (return j) = j
runNf (bind u c) = bindNf u (runNf c)  -- Problem!
runNf (case x t) = {!!}
runNf (split x c) = {!!}

-- Monoidal functoriality ★

module _ {A B : ISet} (mA : Mon A) (mB : Mon B) where

  zip : ⟨ ◇ A ⊙ ◇ B ⟩→̇ ◇ (A ×̂ B)
  zip cA cB = join (◇-map! (λ τ a → ◇-map! (λ τ' b → mA a τ' , b) (◇-mon mB cB τ)) cA)

-- Alternative definitions of freshᶜ

freshᶜ₀ : (Γ : Cxt) → ◇ ⟦ Γ ⟧ᶜ Γ
freshᶜ₀ [] = return []
freshᶜ₀ (P ∷ Γ) = ◇-ext $
  □-weak (◇-mon (monᶜ Γ) (freshᶜ₀ Γ)) -- BAD, use of ◇-mon
  ⋉ fresh◇
-- freshᶜ (P ∷ Γ) = ◇-ext $
--   (λ τ → ◇-mon (monᶜ Γ) (freshᶜ Γ) (⊆-trans (_ ∷ʳ ⊆-refl) τ))  -- BAD, use of ◇-mon
--   ⋉ fresh◇

freshG₀ : □ (◇ ⟦ Γ ⟧ᶜ) Γ
-- freshG₀ : (τ : Γ ⊆ Δ) → ◇ ⟦ Γ ⟧ᶜ Δ
freshG₀ [] = return []
freshG₀ (P   ∷ʳ τ) = ◇-mon (monᶜ _) (freshG₀ τ) (P ∷ʳ ⊆-refl)  -- BAD, use of ◇-mon
freshG₀ (refl ∷ τ) = ◇-ext $ (λ τ₁ → freshG₀ (⊆-trans τ (⊆-trans (_ ∷ʳ ⊆-refl) τ₁))) ⋉ fresh◇

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


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

open import FFI.Data.Either using (Either; Left; Right)
open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Luau.TypeNormalization using (normalize)

module Luau.FunctionTypes where

-- The domain of a normalized type
srcⁿ : Type → Type
srcⁿ (S ⇒ T) = S
srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
srcⁿ never = unknown
srcⁿ T = never

-- To get the domain of a type, we normalize it first We need to do
-- this, since if we try to use it on non-normalized types, we get
--
-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
-- src(never) = unknown
--
-- so src doesn't respect type equivalence.
src : Type → Type
src (S ⇒ T) = S
src T = srcⁿ(normalize T)

-- The codomain of a type
tgt : Type → Type
tgt nil = never
tgt (S ⇒ T) = T
tgt never = never
tgt unknown = unknown
tgt number = never
tgt boolean = never
tgt string = never
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
tgt (S ∩ T) = (tgt S) ∩ (tgt T)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


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

module Data.List.Kleene.Syntax where

open import Data.List hiding ([_])
open import Data.List.Kleene.Base
open import Data.Product

infixr 4 _,_
infixr 5 _]
data ListSyntax {a} (A : Set a) : Set a where
  _]  : A → ListSyntax A
  _,_ : A → ListSyntax A → ListSyntax A

infixr 4 ⋆[_ ⁺[_ [_
⋆[_ : ∀ {a} {A : Set a} → ListSyntax A → A ⋆
⋆[ x ] = ∹ x & []
⋆[ x , xs = ∹ x & (⋆[ xs)

⁺[_ : ∀ {a} {A : Set a} → ListSyntax A → A ⁺
⁺[ x ] = x & []
⁺[ x , xs = x & ∹ (⁺[ xs)

[_ : ∀ {a} {A : Set a} → ListSyntax A → List A
[ x ] = x ∷ []
[ x , xs = x ∷ ([ xs)

private
  open import Data.Nat

  _ : ℕ ⋆
  _ = ⋆[ 1 , 2 , 3 ]

  _ : ℕ ⁺
  _ = ⁺[ 1 , 2 , 3 ]

  _ : List ℕ
  _ = [ 1 , 2 , 3 ]

max_stars_repo_name: oisdk/agda-kleene-lists

max_issues_repo_name: oisdk/agda-kleene-lists

max_forks_repo_name: oisdk/agda-kleene-lists


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

module sets.int where

open import sets.int.definition public
open import sets.int.utils public
open import sets.int.core public
open import sets.int.properties public


text:
module Issue2959.M (_ : Set₁) where

record R : Set₁ where
  field
    A : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --prop #-}

postulate
  f : Prop → Prop
  P : Prop₁

x : Prop
x = f P

-- WAS:
-- Set₁ != Set
-- when checking that the expression P has type Prop

-- SHOULD BE:
-- Prop₁ != Prop
-- when checking that the expression P has type Prop

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --inversion-max-depth=10 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data ⊥ : Set where

double : Nat → Nat
double zero    = zero
double (suc n) = suc (suc (double n))

postulate
  doubleSuc : (x y : Nat) → double x ≡ suc (double y) → ⊥

diverge : ⊥
diverge = doubleSuc _ _ refl

{-
  double ?x == suc (double ?y)
    ?x := suc ?x₁
  suc (suc (double ?x₁)) == suc (double ?y)
  suc (double ?x₁) == double ?y
    ?y := suc ?y₁
  double ?x₁ == suc (double ?y₁)
  .
  .
  .
-}


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category; module Definitions)

-- Definition of the "Twisted" Functor between certain Functor Categories
module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (𝒞 : Category o ℓ e) (𝒟 : Category o′ ℓ′ e′) where

import Categories.Category.Construction.TwistedArrow as TW
open import Categories.Category.Product
open import Categories.Category.Construction.Functors
open import Categories.Functor
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)

open import Data.Product using (_,_)

private
  module C = Category 𝒞

Twist : Functor (Product C.op 𝒞) 𝒟 → Functor (TW.TwistedArrow 𝒞) 𝒟
Twist F = record
  { F₀ = λ x → F₀ (dom x , cod x)
  ; F₁ = λ f → F₁ (dom⇐ f , cod⇒ f)
  ; identity = identity
  ; homomorphism = homomorphism
  ; F-resp-≈ = F-resp-≈
  }
  where
  open Functor F
  open TW.Morphism
  open TW.Morphism⇒

Twist′ : Functor (Product C.op 𝒞) 𝒟 → Functor (Category.op (TW.TwistedArrow C.op)) 𝒟
Twist′ F = record
  { F₀ = λ x → F₀ (dom x , cod x)
  ; F₁ = λ f → F₁ (dom⇐ f , cod⇒ f)
  ; identity = identity
  ; homomorphism = homomorphism
  ; F-resp-≈ = F-resp-≈
  }
  where
  open Functor F
  open TW.Morphism
  open TW.Morphism⇒

Twisted : Functor (Functors (Product C.op 𝒞) 𝒟) (Functors (TW.TwistedArrow 𝒞) 𝒟)
Twisted = record
  { F₀ = Twist
  ; F₁ = Nat
  ; identity = D.Equiv.refl
  ; homomorphism = D.Equiv.refl
  ; F-resp-≈ = λ f≈g → f≈g
  }
  where
  open TW.Morphism
  open TW.Morphism⇒
  module D = Category 𝒟
  Nat : {F G : Functor (Product C.op 𝒞) 𝒟} → NaturalTransformation F G → NaturalTransformation (Twist F) (Twist G)
  Nat nt = ntHelper record
    { η = λ x → η nt (dom x , cod x)
    ; commute = λ f → commute nt (dom⇐ f , cod⇒ f)
    }
    where
    open NaturalTransformation

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:
module ModusPonens where

modusPonens : {P Q : Set} → (P → Q) → P → Q
modusPonens = {!!}

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
module hello-world-dep-lookup where

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; _∷_)
open import Data.Fin using (Fin; zero; suc)

variable
  A : Set
  n : ℕ

lookup : Vec A n → Fin n → A
lookup (a ∷ as) zero = a
lookup (a ∷ as) (suc i) = lookup as i

max_stars_repo_name: avieor/agda-demos

max_issues_repo_name: avieor/agda-demos

max_forks_repo_name: avieor/agda-demos