text:
----------------------------------------------------------------------
-- This file contains constructions of new categories from existing --
-- categories.                                                      --
----------------------------------------------------------------------
module Category.CategoryCons where

open import Level
open import Data.Product

open import Setoid.Total
open import Category.Category

open SetoidFun

-- The product of two categories.
_●_ : {l₁ l₂ : Level} → (ℂ₁ : Cat {l₁}) → (ℂ₂ : Cat {l₂}) → Cat {l₁ ⊔ l₂}
ℂ₁ ● ℂ₂ = record {
            Obj = (Obj ℂ₁) × (Obj ℂ₂);
            Hom = λ A B → (Hom ℂ₁ (proj₁ A) (proj₁ B)) ●ₛ ((Hom ℂ₂ (proj₂ A) (proj₂ B)));
            comp = λ {A} {B} {C} → (comp ℂ₁) ●b (comp ℂ₂);
            id = λ {A} → (id ℂ₁) , (id ℂ₂);
            assocPf = λ {A} {B} {C} {D} {f} {g} {h} → (assocPf ℂ₁) , (assocPf ℂ₂);
            idPf = λ {A} {B} {f} → (idPf ℂ₁) , (idPf ℂ₂) }

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Data.Product renaming (_×_ to _∧_)

×-comm : {A B : Set} → (A ∧ B) → (B ∧ A)
×-comm (fst , snd) = snd , fst

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

K : {A B : Set} → A → B → A
K a b = a

app : {A B : Set} → (A → B) → A → B
app f a = f a

flip : {A B C : Set} → (A → B → C) → B → A → C
flip f b a = f a b

comp : {A B C : Set} → (A → B) → (B → C) → (A → C)
comp ab bc = λ x → bc (ab x)

S : {A B C : Set} → (A → B → C) → (A → B) → A → C
S g f = λ x → g x (f x)

proj1 : {A B : Set} → (A ∧ B) → A
proj1 (fst , snd) = fst

proj2 : {A B : Set} → (A ∧ B) → B
proj2 (fst , snd) = snd

diagonal : {A B : Set} → A → (A ∧ A)
diagonal a = a , a

commut : {A B : Set} → (A ∧ B) → (B ∧ A)
commut (fst , snd) = snd , fst

curry1 : {A B C : Set} → (A ∧ B → C) → (A → B → C)
curry1 f = λ x x₁ → f (x , x₁)

curry2 : {A B C : Set} → (A → B → C) → (A ∧ B → C)
curry2 f (fst , snd) = f fst snd

_↔_ : (A B : Set) → Set
A ↔ B = (A → B) ∧ (B → A)

currying : {A B C : Set} → (A ∧ B → C) ↔ (A → B → C)
currying = curry1 , curry2

distrib : {A B C : Set} → (A → (B ∧ C)) ↔ ((A → B) ∧ (A → C))
distrib = (λ x → (λ x₁ → proj1 (x x₁)) , λ x₁ → proj2 (x x₁)) , λ x x₁ → ((proj1 x) x₁) , ((proj2 x) x₁)

data _∨_ (A B : Set) : Set where
  left : A → A ∨ B
  right : B → A ∨ B

or-elim : {A B C : Set} → (A ∨ B) → (A → C) → (B → C) → C
or-elim (left x) = λ x₁ x₂ → x₁ x
or-elim (right x) = λ x₁ x₂ → x₂ x

or-comm : {A B : Set} → (A ∨ B) → (B ∨ A)
or-comm (left x) = right x
or-comm (right x) = left x

or-dist : {A B C : Set} → (A ∧ (B ∨ C)) → ((A ∧ B) ∨ (A ∧ C))
or-dist (fst , left x) = left (fst , x)
or-dist (fst , right x) = right (fst , x)

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

¬ : Set → Set
¬ A = A → ⊥

contr : {A B : Set} → (A → B) → (¬ B → ¬ A)
contr f = λ x x₁ → x (f x₁)

non-contr : {A : Set} → ¬ (A ∧ ¬ A)
non-contr (fst , snd) = snd fst

nni : {A : Set} → A → ¬ (¬ A)
nni a = λ x → x a

⊥-nne : ¬ (¬ ⊥) → ⊥
⊥-nne x = x ⊥-elim

¬-elim : {A B : Set} → ¬ A → A → B
¬-elim n a = ⊥-elim (n a)

nnlem : {A : Set} → ¬ (¬ (A ∨ ¬ A))
nnlem = (λ x → x (right λ y → x (left y)))

rp2 : {A : Set} → (A → ¬ A) → (¬ A → A) → ⊥
rp2 a na = nnlem (λ x → or-elim x (λ x₁ → a x₁ x₁) λ x₁ → x₁ (na x₁))

data ⊤ : Set where
  tt : ⊤

ti : {A : Set} → (⊤ → A) → A
ti f = f tt

dmnt : ¬ ⊤ → ⊥
dmnt f = f tt

dmtn : ⊥ → ¬ ⊤
dmtn = λ x x₁ → x

lem : Set₁
lem = (A : Set) → A ∨ ¬ A

nne : Set₁
nne = (A : Set) → ¬ (¬ A) → A

nne-lem : nne → lem
nne-lem x A = x (A ∨ ¬ A) nnlem

lem-nne : lem → nne
lem-nne x A y = or-elim (x A) (λ x₁ → x₁) λ x₁ → ¬-elim y x₁

_↔₁_ : (A B : Set₁) → Set₁
A ↔₁ B = (A → B) ∧ (B → A)

peirce : Set₁
peirce = (A B : Set) → ((A → B) → A) → A

lem-peirce : lem ↔₁ peirce
lem-peirce = (λ x A B x₁ → or-elim (x A) id λ x₂ → x₁ λ x₃ → ¬-elim x₂ x₃) , λ x A → x (A ∨ ¬ A) ⊥ λ x₁ → right λ x₂ → x₁ (left x₂)

nne-peirce : nne ↔₁ peirce
nne-peirce = (λ x A B x₁ → x A λ x₂ → x₂ (x₁ λ x₃ → ¬-elim x₂ x₃)) , (λ x A x₁ → x A ⊥ λ x₂ → ¬-elim x₁ x₂)

ext: agda

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
------------------------------------------------------------------------
-- Contexts, variables, context morphisms, etc.
------------------------------------------------------------------------

-- Based on Conor McBride's "Outrageous but Meaningful Coincidences:
-- Dependent type-safe syntax and evaluation".

-- The contexts and variables are parametrised by a universe.

open import Data.Universe.Indexed

module deBruijn.Context.Basics
  {i u e} (Uni : IndexedUniverse i u e) where

open IndexedUniverse Uni

open import Data.Product as Prod
open import Data.Unit
open import Function hiding (_∋_)
open import Level using (_⊔_; Lift)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

open P.≡-Reasoning

------------------------------------------------------------------------
-- Contexts and "types"

mutual

  -- Contexts.

  infixl 5 _▻_

  data Ctxt : Set (i ⊔ u ⊔ e) where
    ε   : Ctxt
    _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

  -- Semantic types: maps from environments to universe codes. The
  -- semantic types come in two flavours: indexed and unindexed
  -- (paired up with an index).

  IType : Ctxt → I → Set (u ⊔ e)
  IType Γ i = Env Γ → U i

  Type : Ctxt → Set (i ⊔ u ⊔ e)
  Type Γ = ∃ λ i → IType Γ i

  -- Extracts the index from an unindexed type.

  index : ∀ {Γ} → Type Γ → I
  index = proj₁

  -- Converts a type to an indexed type.

  indexed-type : ∀ {Γ} (σ : Type Γ) → IType Γ (index σ)
  indexed-type = proj₂

  -- Interpretation of contexts: environments.

  Env : Ctxt → Set e
  Env ε       = Lift _ ⊤
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (indexed-type σ γ)

-- Semantic values: maps from environments to universe values.

Value : (Γ : Ctxt) → Type Γ → Set _
Value Γ σ = (γ : Env Γ) → El (indexed-type σ γ)

------------------------------------------------------------------------
-- Context morphisms

-- Context morphisms or "semantic substitutions": maps from
-- environments to environments. Note the arrow's direction.

infixr 4 _⇨̂_

_⇨̂_ : Ctxt → Ctxt → Set _
Γ ⇨̂ Δ = Env Δ → Env Γ

-- The identity morphism.

îd : ∀ {Γ} → Γ ⇨̂ Γ
îd = id

-- If the context cannot be inferred the following variant can be used
-- instead.

îd[_] : ∀ Γ → Γ ⇨̂ Γ
îd[ _ ] = îd

-- Reverse composition of context morphisms.

infixl 9 _∘̂_

_∘̂_ : ∀ {Γ Δ Ε} → Γ ⇨̂ Δ → Δ ⇨̂ Ε → Γ ⇨̂ Ε
ρ̂₁ ∘̂ ρ̂₂ = ρ̂₁ ∘ ρ̂₂

-- Application of context morphisms to indexed types.

infixl 8 _/̂I_

_/̂I_ : ∀ {Γ Δ i} → IType Γ i → Γ ⇨̂ Δ → IType Δ i
σ /̂I ρ̂ = σ ∘ ρ̂

-- Application of context morphisms to types.

infixl 8 _/̂_

_/̂_ : ∀ {Γ Δ} → Type Γ → Γ ⇨̂ Δ → Type Δ
(i , σ) /̂ ρ̂ = (i , σ /̂I ρ̂)

-- Application of context morphisms to values.

infixl 8 _/̂Val_

_/̂Val_ : ∀ {Γ Δ σ} → Value Γ σ → (ρ̂ : Γ ⇨̂ Δ) → Value Δ (σ /̂ ρ̂)
v /̂Val ρ̂ = v ∘ ρ̂

-- Weakening.

ŵk : ∀ {Γ σ} → Γ ⇨̂ Γ ▻ σ
ŵk = proj₁

ŵk[_] : ∀ {Γ} σ → Γ ⇨̂ Γ ▻ σ
ŵk[ _ ] = ŵk

-- Empty context morphism.

ε̂ : ∀ {Δ} → ε ⇨̂ Δ
ε̂ = λ _ → _

ε̂[_] : ∀ Δ → ε ⇨̂ Δ
ε̂[ _ ] = ε̂

-- Extends a context morphism with another value.

infixl 5 _▻̂_ _▻̂[_]_

_▻̂_ : ∀ {Γ Δ σ} (ρ̂ : Γ ⇨̂ Δ) → Value Δ (σ /̂ ρ̂) → Γ ▻ σ ⇨̂ Δ
_▻̂_ = <_,_>

_▻̂[_]_ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) σ → Value Δ (σ /̂ ρ̂) → Γ ▻ σ ⇨̂ Δ
ρ̂ ▻̂[ _ ] v = ρ̂ ▻̂ v

-- A context morphism which only modifies the last "variable".

ŝub : ∀ {Γ σ} → Value Γ σ → Γ ▻ σ ⇨̂ Γ
ŝub v = îd ▻̂ v

-- The "tail" of a "nonempty" context morphism.

t̂ail : ∀ {Γ Δ σ} → Γ ▻ σ ⇨̂ Δ → Γ ⇨̂ Δ
t̂ail ρ̂ = ŵk ∘̂ ρ̂

-- The "head" of a "nonempty" context morphism.

ĥead : ∀ {Γ Δ σ} (ρ̂ : Γ ▻ σ ⇨̂ Δ) → Value Δ (σ /̂ t̂ail ρ̂)
ĥead ρ̂ = proj₂ ∘ ρ̂

-- Lifting.

infixl 10 _↑̂_
infix  10 _↑̂

_↑̂_ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) σ → Γ ▻ σ ⇨̂ Δ ▻ σ /̂ ρ̂
ρ̂ ↑̂ _ = Prod.map ρ̂ id

_↑̂ : ∀ {Γ Δ σ} (ρ̂ : Γ ⇨̂ Δ) → Γ ▻ σ ⇨̂ Δ ▻ σ /̂ ρ̂
ρ̂ ↑̂ = ρ̂ ↑̂ _

------------------------------------------------------------------------
-- Variables

-- Variables (de Bruijn indices).

infix 3 _∋_

data _∋_ : (Γ : Ctxt) → Type Γ → Set (i ⊔ u ⊔ e) where
  zero : ∀ {Γ σ}               → Γ ▻ σ ∋ σ /̂ ŵk
  suc  : ∀ {Γ σ τ} (x : Γ ∋ τ) → Γ ▻ σ ∋ τ /̂ ŵk

zero[_] : ∀ {Γ} σ → Γ ▻ σ ∋ σ /̂ ŵk
zero[ _ ] = zero

suc[_] : ∀ {Γ} σ {τ} → Γ ∋ τ → Γ ▻ σ ∋ τ /̂ ŵk
suc[ _ ] = suc

-- Interpretation of variables: a lookup function.

lookup : ∀ {Γ σ} → Γ ∋ σ → Value Γ σ
lookup zero    (γ , v) = v
lookup (suc x) (γ , v) = lookup x γ

-- Application of context morphisms to variables.

infixl 8 _/̂∋_

_/̂∋_ : ∀ {Γ Δ σ} → Γ ∋ σ → (ρ̂ : Γ ⇨̂ Δ) → Value Δ (σ /̂ ρ̂)
x /̂∋ ρ̂ = lookup x /̂Val ρ̂

------------------------------------------------------------------------
-- Equality

infix 4 _≅-Ctxt_ _≅-Type_ _≅-IType_ _≅-Value_ _≅-⇨̂_ _≅-∋_

-- Equality of contexts.

_≅-Ctxt_ : Ctxt → Ctxt → Set _
Γ₁ ≅-Ctxt Γ₂ = Γ₁ ≡ Γ₂

-- Equality of types.
--
-- This library uses propositional equality, including the K rule.
--
-- Two types are defined to be equal if their corresponding telescopes
-- are equal. The constructor [_] turns a type into a telescope.
--
-- At first two types (or context morphisms, or…) were defined to be
-- equal if they were equal according to the heterogeneous equality.
-- However, this led to a problem. Consider the old and new
-- definitions of /̂-cong:
--
-- Old:
--
--   /̂-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
--              {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
--            Γ₁ ≡ Γ₂ → Δ₁ ≡ Δ₂ → σ₁ ≅ σ₂ → ρ̂₁ ≅ ρ̂₂ → σ₁ /̂ ρ̂₁ ≅ σ₂ /̂ ρ̂₂
--   /̂-cong P.refl P.refl H.refl H.refl = H.refl
--
-- New:
--
--   /̂-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
--              {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
--            σ₁ ≅-Type σ₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → σ₁ /̂ ρ̂₁ ≅-Type σ₂ /̂ ρ̂₂
--   /̂-cong P.refl P.refl = P.refl
--
-- Notice that the old definition required more assumptions than the
-- new one. This meant that proofs using various congruences became
-- unnecessarily large and complicated.

record [Type] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ} : Ctxt
    σ   : Type Γ

_≅-Type_ : ∀ {Γ₁} (σ₁ : Type Γ₁)
             {Γ₂} (σ₂ : Type Γ₂) → Set _
σ₁ ≅-Type σ₂ = [ σ₁ ] ≡ [ σ₂ ]

-- If the indices are equal, then _≅-Type_ coincides with _≡_.

≅-Type-⇒-≡ : ∀ {Γ} {σ₁ σ₂ : Type Γ} →
             σ₁ ≅-Type σ₂ → σ₁ ≡ σ₂
≅-Type-⇒-≡ P.refl = P.refl

-- Certain uses of substitutivity can be removed.

drop-subst-Type : ∀ {a} {A : Set a} {x₁ x₂}
                  (f : A → Ctxt) {σ} (x₁≡x₂ : x₁ ≡ x₂) →
                  P.subst (λ x → Type (f x)) x₁≡x₂ σ ≅-Type σ
drop-subst-Type f P.refl = P.refl

-- TODO: Should functions like ≅-Type-⇒-≡ and drop-subst-Type be
-- included for all types?

record [IType] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ}   : Ctxt
    {idx} : I
    σ     : IType Γ idx

_≅-IType_ : ∀ {Γ₁ i₁} (σ₁ : IType Γ₁ i₁)
              {Γ₂ i₂} (σ₂ : IType Γ₂ i₂) → Set _
σ₁ ≅-IType σ₂ = _≡_ {A = [IType]} [ σ₁ ] [ σ₂ ]

-- If the indices are equal, then _≅-IType_ coincides with _≡_.

≅-IType-⇒-≡ : ∀ {Γ i} {σ₁ σ₂ : IType Γ i} →
              σ₁ ≅-IType σ₂ → σ₁ ≡ σ₂
≅-IType-⇒-≡ P.refl = P.refl

-- Equality of values.

record [Value] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ} : Ctxt
    {σ} : Type Γ
    v   : Value Γ σ

_≅-Value_ : ∀ {Γ₁ σ₁} (v₁ : Value Γ₁ σ₁)
              {Γ₂ σ₂} (v₂ : Value Γ₂ σ₂) → Set _
v₁ ≅-Value v₂ = _≡_ {A = [Value]} [ v₁ ] [ v₂ ]

≅-Value-⇒-≡ : ∀ {Γ σ} {v₁ v₂ : Value Γ σ} →
              v₁ ≅-Value v₂ → v₁ ≡ v₂
≅-Value-⇒-≡ P.refl = P.refl

-- Equality of context morphisms.

record [⇨̂] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ Δ} : Ctxt
    ρ̂     : Γ ⇨̂ Δ

_≅-⇨̂_ : ∀ {Γ₁ Δ₁} (ρ̂₁ : Γ₁ ⇨̂ Δ₁)
          {Γ₂ Δ₂} (ρ̂₂ : Γ₂ ⇨̂ Δ₂) → Set _
ρ̂₁ ≅-⇨̂ ρ̂₂ = _≡_ {A = [⇨̂]} [ ρ̂₁ ] [ ρ̂₂ ]

≅-⇨̂-⇒-≡ : ∀ {Γ Δ} {ρ̂₁ ρ̂₂ : Γ ⇨̂ Δ} →
          ρ̂₁ ≅-⇨̂ ρ̂₂ → ρ̂₁ ≡ ρ̂₂
≅-⇨̂-⇒-≡ P.refl = P.refl

-- Equality of variables.

record [∋] : Set (i ⊔ u ⊔ e) where
  constructor [_]
  field
    {Γ} : Ctxt
    {σ} : Type Γ
    x   : Γ ∋ σ

_≅-∋_ : ∀ {Γ₁ σ₁} (x₁ : Γ₁ ∋ σ₁)
          {Γ₂ σ₂} (x₂ : Γ₂ ∋ σ₂) → Set _
x₁ ≅-∋ x₂ = _≡_ {A = [∋]} [ x₁ ] [ x₂ ]

≅-∋-⇒-≡ : ∀ {Γ σ} {x₁ x₂ : Γ ∋ σ} →
          x₁ ≅-∋ x₂ → x₁ ≡ x₂
≅-∋-⇒-≡ P.refl = P.refl

------------------------------------------------------------------------
-- Some congruence lemmas

▻-cong : ∀ {Γ₁ Γ₂ σ₁ σ₂} → σ₁ ≅-Type σ₂ → Γ₁ ▻ σ₁ ≅-Ctxt Γ₂ ▻ σ₂
▻-cong P.refl = P.refl

indexed-type-cong :
  ∀ {Γ₁} {σ₁ : Type Γ₁}
    {Γ₂} {σ₂ : Type Γ₂} →
  σ₁ ≅-Type σ₂ → indexed-type σ₁ ≅-IType indexed-type σ₂
indexed-type-cong P.refl = P.refl

îd-cong : ∀ {Γ₁ Γ₂} → Γ₁ ≅-Ctxt Γ₂ → îd[ Γ₁ ] ≅-⇨̂ îd[ Γ₂ ]
îd-cong P.refl = P.refl

∘̂-cong : ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
           {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂} →
         ρ̂₁₁ ≅-⇨̂ ρ̂₁₂ → ρ̂₂₁ ≅-⇨̂ ρ̂₂₂ → ρ̂₁₁ ∘̂ ρ̂₂₁ ≅-⇨̂ ρ̂₁₂ ∘̂ ρ̂₂₂
∘̂-cong P.refl P.refl = P.refl

/̂I-cong : ∀ {Γ₁ Δ₁ i₁} {σ₁ : IType Γ₁ i₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
            {Γ₂ Δ₂ i₂} {σ₂ : IType Γ₂ i₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
          σ₁ ≅-IType σ₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → σ₁ /̂I ρ̂₁ ≅-IType σ₂ /̂I ρ̂₂
/̂I-cong P.refl P.refl = P.refl

/̂-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
           {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
         σ₁ ≅-Type σ₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → σ₁ /̂ ρ̂₁ ≅-Type σ₂ /̂ ρ̂₂
/̂-cong P.refl P.refl = P.refl

/̂Val-cong : ∀ {Γ₁ Δ₁ σ₁} {v₁ : Value Γ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
              {Γ₂ Δ₂ σ₂} {v₂ : Value Γ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
            v₁ ≅-Value v₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → v₁ /̂Val ρ̂₁ ≅-Value v₂ /̂Val ρ̂₂
/̂Val-cong P.refl P.refl = P.refl

ŵk-cong : ∀ {Γ₁} {σ₁ : Type Γ₁} {Γ₂} {σ₂ : Type Γ₂} →
          σ₁ ≅-Type σ₂ → ŵk[ σ₁ ] ≅-⇨̂ ŵk[ σ₂ ]
ŵk-cong P.refl = P.refl

ε̂-cong : ∀ {Δ₁ Δ₂} → Δ₁ ≅-Ctxt Δ₂ → ε̂[ Δ₁ ] ≅-⇨̂ ε̂[ Δ₂ ]
ε̂-cong P.refl = P.refl

▻̂-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {v₁ : Value Δ₁ (σ₁ /̂ ρ̂₁)}
           {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {v₂ : Value Δ₂ (σ₂ /̂ ρ̂₂)} →
         σ₁ ≅-Type σ₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → v₁ ≅-Value v₂ →
         ρ̂₁ ▻̂[ σ₁ ] v₁ ≅-⇨̂ ρ̂₂ ▻̂[ σ₂ ] v₂
▻̂-cong P.refl P.refl P.refl = P.refl

ŝub-cong : ∀ {Γ₁ σ₁} {v₁ : Value Γ₁ σ₁} {Γ₂ σ₂} {v₂ : Value Γ₂ σ₂} →
           v₁ ≅-Value v₂ → ŝub v₁ ≅-⇨̂ ŝub v₂
ŝub-cong P.refl = P.refl

t̂ail-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ▻ σ₁ ⇨̂ Δ₁}
              {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ▻ σ₂ ⇨̂ Δ₂} →
            ρ̂₁ ≅-⇨̂ ρ̂₂ → t̂ail ρ̂₁ ≅-⇨̂ t̂ail ρ̂₂
t̂ail-cong P.refl = P.refl

ĥead-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ▻ σ₁ ⇨̂ Δ₁}
              {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ▻ σ₂ ⇨̂ Δ₂} →
            ρ̂₁ ≅-⇨̂ ρ̂₂ → ĥead ρ̂₁ ≅-Value ĥead ρ̂₂
ĥead-cong P.refl = P.refl

↑̂-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {σ₁}
           {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {σ₂} →
         ρ̂₁ ≅-⇨̂ ρ̂₂ → σ₁ ≅-Type σ₂ → ρ̂₁ ↑̂ σ₁ ≅-⇨̂ ρ̂₂ ↑̂ σ₂
↑̂-cong P.refl P.refl = P.refl

zero-cong : ∀ {Γ₁} {σ₁ : Type Γ₁}
              {Γ₂} {σ₂ : Type Γ₂} →
            σ₁ ≅-Type σ₂ → zero[ σ₁ ] ≅-∋ zero[ σ₂ ]
zero-cong P.refl = P.refl

suc-cong :
  ∀ {Γ₁ σ₁ τ₁} {x₁ : Γ₁ ∋ τ₁}
    {Γ₂ σ₂ τ₂} {x₂ : Γ₂ ∋ τ₂} →
  σ₁ ≅-Type σ₂ → x₁ ≅-∋ x₂ → suc[ σ₁ ] x₁ ≅-∋ suc[ σ₂ ] x₂
suc-cong P.refl P.refl = P.refl

/̂∋-cong : ∀ {Γ₁ Δ₁ σ₁} {x₁ : Γ₁ ∋ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
            {Γ₂ Δ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} →
          x₁ ≅-∋ x₂ → ρ̂₁ ≅-⇨̂ ρ̂₂ → x₁ /̂∋ ρ̂₁ ≅-Value x₂ /̂∋ ρ̂₂
/̂∋-cong P.refl P.refl = P.refl

------------------------------------------------------------------------
-- Some properties, all of which hold definitionally

-- _/̂_ preserves the index.

index-/̂ : ∀ {Γ Δ} (σ : Type Γ) (ρ̂ : Γ ⇨̂ Δ) →
          index (σ /̂ ρ̂) ≡ index σ
index-/̂ σ ρ̂ = P.refl

-- îd and _∘̂_ form a monoid.

îd-∘̂ : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) → ρ̂ ∘̂ îd ≅-⇨̂ ρ̂
îd-∘̂ ρ̂ = P.refl

∘̂-îd : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) → îd ∘̂ ρ̂ ≅-⇨̂ ρ̂
∘̂-îd ρ̂ = P.refl

∘̂-assoc : ∀ {Γ Δ Ε Ζ} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) (ρ̂₃ : Ε ⇨̂ Ζ) →
          ρ̂₁ ∘̂ (ρ̂₂ ∘̂ ρ̂₃) ≅-⇨̂ (ρ̂₁ ∘̂ ρ̂₂) ∘̂ ρ̂₃
∘̂-assoc ρ̂₁ ρ̂₂ ρ̂₃ = P.refl

-- The lifting of the identity substitution is the identity
-- substitution.

îd-↑̂ : ∀ {Γ} (σ : Type Γ) → îd ↑̂ σ ≅-⇨̂ îd[ Γ ▻ σ ]
îd-↑̂ σ = P.refl

-- _↑̂ distributes over _∘̂_.

↑̂-distrib : ∀ {Γ Δ Ε} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) σ →
            (ρ̂₁ ∘̂ ρ̂₂) ↑̂ σ ≅-⇨̂ ρ̂₁ ↑̂ σ ∘̂ ρ̂₂ ↑̂
↑̂-distrib ρ̂₁ ρ̂₂ σ = P.refl

-- ŵk is a left inverse of ŝub.

ŵk-∘̂-ŝub : ∀ {Γ σ} (v : Value Γ σ) → ŵk ∘̂ ŝub v ≅-⇨̂ îd
ŵk-∘̂-ŝub v = P.refl

-- First weakening under the head, and then replacing the head with
-- the new head, is the same as doing nothing.

ŵk-↑̂-∘̂-ŝub : ∀ {Γ} σ → ŵk ↑̂ ∘̂ ŝub proj₂ ≅-⇨̂ îd[ Γ ▻ σ ]
ŵk-↑̂-∘̂-ŝub σ = P.refl

-- ŵk commutes with arbitrary context morphisms (modulo lifting).

∘̂-ŵk : ∀ {Γ Δ} (ρ̂ : Γ ⇨̂ Δ) σ → ρ̂ ∘̂ ŵk[ σ /̂ ρ̂ ] ≅-⇨̂ ŵk[ σ ] ∘̂ ρ̂ ↑̂
∘̂-ŵk ρ̂ σ = P.refl

-- ŝub commutes with arbitrary context morphisms (modulo lifting).

ŝub-∘̂ : ∀ {Γ Δ σ} (ρ̂ : Γ ⇨̂ Δ) (v : Value Γ σ) →
        ŝub v ∘̂ ρ̂ ≅-⇨̂ ρ̂ ↑̂ ∘̂ ŝub (v /̂Val ρ̂)
ŝub-∘̂ ρ̂ v = P.refl

-- Laws relating _▻̂_, ĥead and t̂ail.

ĥead-▻̂ : ∀ {Γ Δ σ} (ρ̂ : Γ ⇨̂ Δ) (v : Value Δ (σ /̂ ρ̂)) →
         ĥead (ρ̂ ▻̂[ σ ] v) ≅-Value v
ĥead-▻̂ ρ̂ v = P.refl

t̂ail-▻̂ : ∀ {Γ Δ σ} (ρ̂ : Γ ⇨̂ Δ) (v : Value Δ (σ /̂ ρ̂)) →
         t̂ail (ρ̂ ▻̂[ σ ] v) ≅-⇨̂ ρ̂
t̂ail-▻̂ ρ̂ v = P.refl

t̂ail-▻̂-ĥead : ∀ {Γ Δ σ} (ρ̂ : Γ ▻ σ ⇨̂ Δ) → t̂ail ρ̂ ▻̂ ĥead ρ̂ ≅-⇨̂ ρ̂
t̂ail-▻̂-ĥead ρ̂ = P.refl

-- Law relating _▻̂_ and _∘̂_.

▻̂-∘̂ : ∀ {Γ Δ Ε σ} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) (v : Value Δ (σ /̂ ρ̂₁)) →
      (ρ̂₁ ▻̂[ σ ] v) ∘̂ ρ̂₂ ≅-⇨̂ (ρ̂₁ ∘̂ ρ̂₂) ▻̂ v /̂Val ρ̂₂
▻̂-∘̂ ρ̂₁ ρ̂₂ v = P.refl

-- The identity substitution has no effect.

/̂-îd : ∀ {Γ} (σ : Type Γ) → σ /̂ îd ≅-Type σ
/̂-îd σ = P.refl

/̂Val-îd : ∀ {Γ σ} (v : Value Γ σ) → v /̂Val îd ≅-Value v
/̂Val-îd v = P.refl

-- Applying two substitutions is equivalent to applying their
-- composition.

/̂-∘̂ : ∀ {Γ Δ Ε} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) σ →
      σ /̂ ρ̂₁ ∘̂ ρ̂₂ ≅-Type σ /̂ ρ̂₁ /̂ ρ̂₂
/̂-∘̂ ρ̂₁ ρ̂₂ σ = P.refl

/̂Val-∘̂ : ∀ {Γ Δ Ε σ} (ρ̂₁ : Γ ⇨̂ Δ) (ρ̂₂ : Δ ⇨̂ Ε) (v : Value Γ σ) →
         v /̂Val ρ̂₁ ∘̂ ρ̂₂ ≅-Value v /̂Val ρ̂₁ /̂Val ρ̂₂
/̂Val-∘̂ ρ̂₁ ρ̂₂ v = P.refl

------------------------------------------------------------------------
-- More properties

-- _▻_ is injective.

▻-injective : ∀ {Γ₁ σ₁ Γ₂ σ₂} →
              Γ₁ ▻ σ₁ ≅-Ctxt Γ₂ ▻ σ₂ → Γ₁ ≅-Ctxt Γ₂ × σ₁ ≅-Type σ₂
▻-injective P.refl = P.refl , P.refl

-- Equality of variables is decidable (if they refer to the same
-- context).

infix 4 _≟-∋_

_≟-∋_ : ∀ {Γ σ₁} (x₁ : Γ ∋ σ₁) {σ₂} (x₂ : Γ ∋ σ₂) →
        Dec (x₁ ≅-∋ x₂)
zero   ≟-∋ zero   = yes P.refl
zero   ≟-∋ suc _  = no λ ()
suc _  ≟-∋ zero   = no λ ()
suc x₁ ≟-∋ suc x₂ = Dec.map′ (suc-cong P.refl) helper (x₁ ≟-∋ x₂)
  where
  helper : ∀ {Γ₁ σ₁ τ₁} {x₁ : Γ₁ ∋ τ₁}
             {Γ₂ σ₂ τ₂} {x₂ : Γ₂ ∋ τ₂} →
           suc[ σ₁ ] x₁ ≅-∋ suc[ σ₂ ] x₂ → x₁ ≅-∋ x₂
  helper P.refl = P.refl

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


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

module Agda.Builtin.IO where

postulate IO : ∀ {a} → Set a → Set a
{-# BUILTIN IO IO #-}

{-# HASKELL type AgdaIO a b = IO b #-}
{-# COMPILED_TYPE IO MAlonzo.Code.Agda.Builtin.IO.AgdaIO #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
------------------------------------------------------------------------
-- Some character parsers
------------------------------------------------------------------------

-- This code also illustrates how a library can make use of another
-- library.

module RecursiveDescent.Inductive.Char where

open import Data.Unit
open import Data.Nat
open import Data.Bool
import Data.Char as C
open C using (Char; _==_)
open import Data.List
open import Data.Function hiding (_$_)

open import RecursiveDescent.Index
open import RecursiveDescent.Inductive
import RecursiveDescent.Inductive.Token
open import RecursiveDescent.Inductive.SimpleLib
import RecursiveDescent.Inductive.Lib as Lib
private
  module L = Lib Char

-- Some parameterised parsers.

private
  data NT (nt : ParserType₁) : ParserType₁ where
    lib'        : forall {i r} -> L.Nonterminal nt i r -> NT nt i r
    digit'      : NT nt _ ℕ
    number'     : NT nt _ ℕ
    whitespace' : NT nt _ ⊤

Nonterminal : ParserType₁ -> ParserType₁
Nonterminal = NT

module Combinators
         {nt} (lib : forall {i r} -> Nonterminal nt i r -> nt i r)
         where

  open L.Combinators (lib ∘₁ lib')

  digit : Parser Char nt _ ℕ
  digit = ! lib digit'

  number : Parser Char nt _ ℕ
  number = ! lib number'

  whitespace : Parser Char nt _ ⊤
  whitespace = ! lib whitespace'

  open RecursiveDescent.Inductive.Token C.decSetoid

  charLib : forall {i r} -> Nonterminal nt i r -> Parser Char nt i r
  charLib (lib' p) = library p
  charLib digit'   = 0 <$ sym '0'
                   ∣ 1 <$ sym '1'
                   ∣ 2 <$ sym '2'
                   ∣ 3 <$ sym '3'
                   ∣ 4 <$ sym '4'
                   ∣ 5 <$ sym '5'
                   ∣ 6 <$ sym '6'
                   ∣ 7 <$ sym '7'
                   ∣ 8 <$ sym '8'
                   ∣ 9 <$ sym '9'
  charLib number' = toNum <$> digit +
    where toNum = foldr (\n x -> 10 * x + n) 0 ∘ reverse
  -- whitespace recognises an incomplete but useful list of whitespace
  -- characters.
  charLib whitespace' = sat' isSpace
    where
    isSpace = \c ->
      (c == ' ') ∨ (c == '\t') ∨ (c == '\n') ∨ (c == '\r')

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- A map function for the substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Map
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Basics
open import Function using (_$_)
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

private
 module Dummy
   {t₁} {T₁ : Term-like t₁}
   {t₂} {T₂ : Term-like t₂}
   where

  open Term-like T₁ using ()
                    renaming (_⊢_ to _⊢₁_; _≅-⊢_ to _≅-⊢₁_; [_] to [_]₁)
  open Term-like T₂ using () renaming (_≅-⊢_ to _≅-⊢₂_; [_] to [_]₂)

  -- Map.

  map : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
        [ T₁ ⟶ T₂ ] ρ̂₂ → Sub T₁ ρ̂₁ → Sub T₂ (ρ̂₁ ∘̂ ρ̂₂)
  map           f ε        = ε
  map {ρ̂₂ = ρ̂₂} f (ρ₁ ▻ t) =
    P.subst (λ v → Sub T₂ (⟦ ρ₁ ⟧⇨ ∘̂ ρ̂₂ ▻̂ v))
            (≅-Value-⇒-≡ $ P.sym $ corresponds f t)
            (map f ρ₁ ▻ f · t)

  abstract

    -- An unfolding lemma.

    map-▻ :
      ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {σ}
      (f : [ T₁ ⟶ T₂ ] ρ̂₂) (ρ : Sub T₁ ρ̂₁) t →
      map f (ρ ▻⇨[ σ ] t) ≅-⇨ map f ρ ▻⇨[ σ ] f · t
    map-▻ {ρ̂₂ = ρ̂₂} f ρ t =
      drop-subst-Sub (λ v → ⟦ ρ ⟧⇨ ∘̂ ρ̂₂ ▻̂ v)
                     (≅-Value-⇒-≡ $ P.sym $ corresponds f t)

    -- A congruence lemma.

    map-cong : ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
                 {f₁ : [ T₁ ⟶ T₂ ] ρ̂₂₁} {ρ₁ : Sub T₁ ρ̂₁₁}
                 {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
                 {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂₂} {ρ₂ : Sub T₁ ρ̂₁₂} →
               f₁ ≅-⟶ f₂ → ρ₁ ≅-⇨ ρ₂ → map f₁ ρ₁ ≅-⇨ map f₂ ρ₂
    map-cong {f₁ = _ , _} {f₂ = ._ , _} {ρ₂ = ε} [ P.refl ] P.refl =
             P.refl
    map-cong {f₁ = f₁} {f₂ = f₂} {ρ₂ = ρ ▻ t} f₁≅f₂ P.refl = begin
      [ map f₁ (ρ ▻ t)    ]  ≡⟨ map-▻ f₁ ρ t ⟩
      [ map f₁ ρ ▻ f₁ · t ]  ≡⟨ ▻⇨-cong P.refl
                                        (map-cong f₁≅f₂ (P.refl {x = [ ρ ]}))
                                        (·-cong f₁≅f₂ (P.refl {x = [ t ]₁})) ⟩
      [ map f₂ ρ ▻ f₂ · t ]  ≡⟨ P.sym $ map-▻ f₂ ρ t ⟩
      [ map f₂ (ρ ▻ t)    ]  ∎

    -- Variants which only require that the functions are
    -- extensionally equal.

    map-cong-ext₁ : ∀ {Γ₁ Δ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ} {ρ̂₂₁ : Δ ⇨̂ Ε₁}
                      {f₁ : [ T₁ ⟶ T₂ ] ρ̂₂₁} {ρ₁ : Sub T₁ ρ̂₁₁}
                      {Γ₂   Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ} {ρ̂₂₂ : Δ ⇨̂ Ε₂}
                      {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂₂} {ρ₂ : Sub T₁ ρ̂₁₂} →
                    Ε₁ ≅-Ctxt Ε₂ →
                    (∀ {σ} (t : Δ ⊢₁ σ) → f₁ · t ≅-⊢₂ f₂ · t) →
                    ρ₁ ≅-⇨ ρ₂ → map f₁ ρ₁ ≅-⇨ map f₂ ρ₂
    map-cong-ext₁ {Δ = Δ} {f₁ = f₁} {f₂ = f₂} {ρ₂ = ρ}
                  Ε₁≅Ε₂ f₁≅f₂ P.refl = helper ρ
      where
      helper : ∀ {Γ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T₁ ρ̂) → map f₁ ρ ≅-⇨ map f₂ ρ
      helper ε       = ε⇨-cong Ε₁≅Ε₂
      helper (ρ ▻ t) = begin
        [ map f₁ (ρ ▻ t)    ]  ≡⟨ map-▻ f₁ ρ t ⟩
        [ map f₁ ρ ▻ f₁ · t ]  ≡⟨ ▻⇨-cong P.refl (helper ρ) (f₁≅f₂ t) ⟩
        [ map f₂ ρ ▻ f₂ · t ]  ≡⟨ P.sym $ map-▻ f₂ ρ t ⟩
        [ map f₂ (ρ ▻ t)    ]  ∎

    map-cong-ext₂ : ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
                      {f₁ : [ T₁ ⟶ T₂ ] ρ̂₂₁} {ρ₁ : Sub T₁ ρ̂₁₁}
                      {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
                      {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂₂} {ρ₂ : Sub T₁ ρ̂₁₂} →
                    Δ₁ ≅-Ctxt Δ₂ → Ε₁ ≅-Ctxt Ε₂ →
                    (∀ {σ₁ σ₂} {t₁ : Δ₁ ⊢₁ σ₁} {t₂ : Δ₂ ⊢₁ σ₂} →
                       t₁ ≅-⊢₁ t₂ → f₁ · t₁ ≅-⊢₂ f₂ · t₂) →
                    ρ₁ ≅-⇨ ρ₂ → map f₁ ρ₁ ≅-⇨ map f₂ ρ₂
    map-cong-ext₂ P.refl Ε₁≅Ε₂ f₁≅f₂ ρ₁≅ρ₂ =
      map-cong-ext₁ Ε₁≅Ε₂ (λ t → f₁≅f₂ (P.refl {x = [ t ]₁})) ρ₁≅ρ₂

    private

      -- A helper lemma.

      /∋-map-▻ :
        ∀ {Γ Δ Ε σ τ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {t} →
        (x : Γ ▻ σ ∋ τ) (f : [ T₁ ⟶ T₂ ] ρ̂₂) (ρ : Sub T₁ ρ̂₁) →
        x /∋ map f (ρ ▻ t) ≅-⊢₂ x /∋ (map f ρ ▻ f · t)
      /∋-map-▻ {t = t} x f ρ =
        /∋-cong (P.refl {x = [ x ]}) (map-▻ f ρ t)

    -- Some sort of naturality statement for _/∋_.

    /∋-map : ∀ {Γ Δ Ε σ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
             (x : Γ ∋ σ) (f : [ T₁ ⟶ T₂ ] ρ̂₂) (ρ : Sub T₁ ρ̂₁) →
             x /∋ map f ρ ≅-⊢₂ f · (x /∋ ρ)
    /∋-map (zero {σ = σ}) f (ρ ▻ t) = begin
      [ zero[ σ ] /∋ map f (ρ ▻ t)     ]₂  ≡⟨ /∋-map-▻ zero[ σ ] f ρ ⟩
      [ zero[ σ ] /∋ (map f ρ ▻ f · t) ]₂  ≡⟨ P.refl ⟩
      [ f · t                          ]₂  ∎
    /∋-map (suc {σ = σ} x) f (ρ ▻ t) = begin
      [ suc      x /∋ map f (ρ ▻ t)     ]₂  ≡⟨ /∋-map-▻ (suc x) f ρ ⟩
      [ suc[ σ ] x /∋ (map f ρ ▻ f · t) ]₂  ≡⟨ P.refl ⟩
      [ x /∋ map f ρ                    ]₂  ≡⟨ /∋-map x f ρ ⟩
      [ f · (x /∋ ρ)                    ]₂  ∎

open Dummy public

abstract

  -- Map is functorial.

  map-[id] : ∀ {t} {T : Term-like t} {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
             (ρ : Sub T ρ̂) → map ([id] {T = T}) ρ ≅-⇨ ρ
  map-[id] ε       = P.refl
  map-[id] (ρ ▻ t) = ▻⇨-cong P.refl (map-[id] ρ) P.refl

  map-[∘] :
    ∀ {t₁} {T₁ : Term-like t₁}
      {t₂} {T₂ : Term-like t₂}
      {t₃} {T₃ : Term-like t₃}
      {Γ Δ Ε Ζ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {ρ̂₃ : Ε ⇨̂ Ζ}
    (f₂ : [ T₂ ⟶ T₃ ] ρ̂₃) (f₁ : [ T₁ ⟶ T₂ ] ρ̂₂)
    (ρ : Sub T₁ ρ̂₁) →
    map (f₂ [∘] f₁) ρ ≅-⇨ map f₂ (map f₁ ρ)
  map-[∘] f₂ f₁ ε       = P.refl
  map-[∘] f₂ f₁ (ρ ▻ t) = begin
    [ map (f₂ [∘] f₁) (ρ ▻ t)           ]  ≡⟨ map-▻ (f₂ [∘] f₁) ρ t ⟩
    [ map (f₂ [∘] f₁) ρ ▻ f₂ · (f₁ · t) ]  ≡⟨ ▻⇨-cong P.refl (map-[∘] f₂ f₁ ρ) P.refl ⟩
    [ map f₂ (map f₁ ρ) ▻ f₂ · (f₁ · t) ]  ≡⟨ P.sym $ map-▻ f₂ (map f₁ ρ) (f₁ · t) ⟩
    [ map f₂ (map f₁ ρ ▻ f₁ · t)        ]  ≡⟨ map-cong (f₂ ∎-⟶) (P.sym $ map-▻ f₁ ρ t) ⟩
    [ map f₂ (map f₁ (ρ ▻ t))           ]  ∎


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

open import Level

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; Endofunctor; _∘F_) renaming (id to idF)
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (_≃_)
open import Categories.NaturalTransformation.Equivalence
open NaturalIsomorphism

record Comonad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  field
    F : Endofunctor C
    ε : NaturalTransformation F idF
    δ : NaturalTransformation F (F ∘F F)

  module F = Functor F
  module ε = NaturalTransformation ε
  module δ = NaturalTransformation δ

  open Category C
  open Functor F

  field
    assoc     : ∀ {X : Obj} → δ.η (F₀ X) ∘ δ.η X ≈ F₁ (δ.η X) ∘ δ.η X
    sym-assoc : ∀ {X : Obj} → F₁ (δ.η X) ∘ δ.η X ≈ δ.η (F₀ X) ∘ δ.η X
    identityˡ : ∀ {X : Obj} → F₁ (ε.η X) ∘ δ.η X ≈ id
    identityʳ : ∀ {X : Obj} → ε.η (F₀ X) ∘ δ.η X ≈ id

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 tc.mod.apply:80 #-}

module Issue1985 where

module Def where
  postulate A : Set

module Par (X : Set₁) where
  postulate B : Set
  open Def public

-- module Works where
--   module Ren B = Par B
--   module App = Ren Set

module Fails where
  module RenP (X : Set₁) = Par X
  module Ren = Par
  -- Like RenP, Ren should contain
  --   A : (B : Set) → Set
  --   A B = Par.A B
  -- but it incorrectly contained
  --   A : Set
  --   A = Par.A

  A₁ A₂ B₁ B₂ : Set₁ → Set
  A₁ = RenP.A
  A₂ = Ren.A
  B₁ = RenP.B
  B₂ = Ren.B

  module App = Ren Set

  A₃ B₃ : Set
  A₃ = App.A
  B₃ = App.B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Agda.Primitive

postulate
  A : Set
  F : ∀ {ℓ} (XF : Set ℓ) → Set ℓ

record R (Q : ∀ {ℓ} (XQ : Set ℓ) → Set ℓ) ℓ : Set (lsuc ℓ) where
  field
    f : {A : Set ℓ} (fa : F A) → Q A

open R

module M (X : Set₁) where
  postulate
    G : ∀ {ℓ} (XG : Set ℓ) → Set ℓ

module N (Y : Set) where
  open M Set

  variable
    z : F A

  postulate
    P     : (p : G A) → Set
    fails : P (f _ z)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Imports.StaleMetaLiteral where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

macro
  metaLit : Tactic
  metaLit hole =
    checkType unknown (def (quote Nat) []) >>= λ
    { (meta m args) →
      unify hole (lit (meta m)) >>= λ _ →
      unify (meta m args) (lit (nat 42))
    ; _ → typeError (strErr "not a meta" ∷ []) }

staleMeta : Meta
staleMeta = metaLit


text:
module Verifier where

open import Definitions
open import NatEquality using (_≟_ ; equality-disjoint)

check1 : (m n : ℕ) → Equal? m n
check1 = _≟_

check2 : (m n : ℕ) → m ≡ n → m ≢ n → ⊥
check2 = equality-disjoint

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


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

module Cubical.HITs.MappingCones.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.HITs.Pushout

open import Cubical.HITs.MappingCones.Base

private
  variable
    ℓ ℓ' ℓ'' : Level

PushoutUnit-iso-Cone : ∀ {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) → Iso (Pushout (const tt) f) (Cone f)
Iso.fun (PushoutUnit-iso-Cone f) (inl tt)   = hub
Iso.fun (PushoutUnit-iso-Cone f) (inr x)    = inj x
Iso.fun (PushoutUnit-iso-Cone f) (push x i) = spoke x i
Iso.inv (PushoutUnit-iso-Cone f) (inj x)     = inr x
Iso.inv (PushoutUnit-iso-Cone f) hub         = inl tt
Iso.inv (PushoutUnit-iso-Cone f) (spoke x i) = push x i
Iso.rightInv (PushoutUnit-iso-Cone f) (inj x)     = refl
Iso.rightInv (PushoutUnit-iso-Cone f) hub         = refl
Iso.rightInv (PushoutUnit-iso-Cone f) (spoke x i) = refl
Iso.leftInv (PushoutUnit-iso-Cone f) (inl tt)   = refl
Iso.leftInv (PushoutUnit-iso-Cone f) (inr x)    = refl
Iso.leftInv (PushoutUnit-iso-Cone f) (push x i) = refl

PushoutUnit≡Cone : ∀ {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) → Pushout (const tt) f ≡ Cone f
PushoutUnit≡Cone f = isoToPath (PushoutUnit-iso-Cone f)

ConesUnit-iso-Cone : ∀ {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) → Iso (Cones Unit (λ { tt → f })) (Cone f)
Iso.fun (ConesUnit-iso-Cone f) (inj x)        = inj x
Iso.fun (ConesUnit-iso-Cone f) (hub tt)       = hub
Iso.fun (ConesUnit-iso-Cone f) (spoke tt x i) = spoke x i
Iso.inv (ConesUnit-iso-Cone f) (inj x)     = inj x
Iso.inv (ConesUnit-iso-Cone f) hub         = hub tt
Iso.inv (ConesUnit-iso-Cone f) (spoke x i) = spoke tt x i
Iso.rightInv (ConesUnit-iso-Cone f) (inj x)     = refl
Iso.rightInv (ConesUnit-iso-Cone f) hub         = refl
Iso.rightInv (ConesUnit-iso-Cone f) (spoke x i) = refl
Iso.leftInv (ConesUnit-iso-Cone f) (inj x) = refl
Iso.leftInv (ConesUnit-iso-Cone f) (hub x) = refl
Iso.leftInv (ConesUnit-iso-Cone f) (spoke a x i) = refl

ConesUnit≡Cone : ∀ {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) → (Cones Unit (λ { tt → f })) ≡ (Cone f)
ConesUnit≡Cone f = isoToPath (ConesUnit-iso-Cone f)

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:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax PCF

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  B   : 0-ary

term
  app : α ↣ β  α  ->  β | _$_ l20
  lam : α.β  ->  α ↣ β | ƛ_ r10
  tr  : B
  fl  : B
  ze  : N
  su  : N  ->  N
  pr  : N  ->  N
  iz  : N  ->  B | 0?
  if  : B  α  α  ->  α
  fix : α.α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
  (zz)       |> iz (ze)       = tr
  (zs) n : N |> iz (su (n)) = fl
  (ps) n : N |> pr (su (n)) = n
  (ift) t f : α |> if (tr, t, f) = t
  (iff) t f : α |> if (fl, t, f) = f
  (fix) t : α.α |> fix (x.t[x]) = t[fix (x.t[x])]
-}

module PCF.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import PCF.Signature

private
  variable
    Γ Δ Π : Ctx
    α β : PCFT
    𝔛 : Familyₛ

-- Inductive term declaration
module PCF:Terms (𝔛 : Familyₛ) where

  data PCF : Familyₛ where
    var  : ℐ ⇾̣ PCF
    mvar : 𝔛 α Π → Sub PCF Π Γ → PCF α Γ

    _$_ : PCF (α ↣ β) Γ → PCF α Γ → PCF β Γ
    ƛ_  : PCF β (α ∙ Γ) → PCF (α ↣ β) Γ
    tr  : PCF B Γ
    fl  : PCF B Γ
    ze  : PCF N Γ
    su  : PCF N Γ → PCF N Γ
    pr  : PCF N Γ → PCF N Γ
    0?  : PCF N Γ → PCF B Γ
    if  : PCF B Γ → PCF α Γ → PCF α Γ → PCF α Γ
    fix : PCF α (α ∙ Γ) → PCF α Γ

  infixl 20 _$_
  infixr 10 ƛ_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  PCFᵃ : MetaAlg PCF
  PCFᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (appₒ ⋮ a , b)     → _$_ a b
      (lamₒ ⋮ a)         → ƛ_  a
      (trₒ  ⋮ _)         → tr
      (flₒ  ⋮ _)         → fl
      (zeₒ  ⋮ _)         → ze
      (suₒ  ⋮ a)         → su  a
      (prₒ  ⋮ a)         → pr  a
      (izₒ  ⋮ a)         → 0?  a
      (ifₒ  ⋮ a , b , c) → if  a b c
      (fixₒ ⋮ a)         → fix a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module PCFᵃ = MetaAlg PCFᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : PCF ⇾̣ 𝒜
    𝕊 : Sub PCF Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (_$_ a b)   = 𝑎𝑙𝑔 (appₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (ƛ_  a)     = 𝑎𝑙𝑔 (lamₒ ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞  tr         = 𝑎𝑙𝑔 (trₒ  ⋮ tt)
    𝕤𝕖𝕞  fl         = 𝑎𝑙𝑔 (flₒ  ⋮ tt)
    𝕤𝕖𝕞  ze         = 𝑎𝑙𝑔 (zeₒ  ⋮ tt)
    𝕤𝕖𝕞 (su  a)     = 𝑎𝑙𝑔 (suₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (pr  a)     = 𝑎𝑙𝑔 (prₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (0?  a)     = 𝑎𝑙𝑔 (izₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (if  a b c) = 𝑎𝑙𝑔 (ifₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)
    𝕤𝕖𝕞 (fix a)     = 𝑎𝑙𝑔 (fixₒ ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ PCFᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ PCF α Γ) → 𝕤𝕖𝕞 (PCFᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (appₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (lamₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (trₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (flₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (zeₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (suₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (prₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (izₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (ifₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (fixₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ PCF ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : PCF ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ PCFᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : PCF α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub PCF Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (_$_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (ƛ_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! tr = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! fl = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! ze = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (su a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (pr a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (0? a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (if a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (fix a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
PCF:Syn : Syntax
PCF:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = PCF:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open PCF:Terms 𝔛 in record
    { ⊥ = PCF ⋉ PCFᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax PCF:Syn public
open PCF:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands PCFᵃ public
open import SOAS.Metatheory PCF:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-  An agda file contains a single module. The module name should correspond to
    the name and path of the file. The path is relative to the project root. In
    this case the project root is the root of Agda II. Modules can be
    parameterised, but in this case we choose not to parameterise the top-level
    module.
-}

module examples.syntax.Syntax where

  -- It is recommended that the body of the top-level module is indented by a
  -- small amount, but this is not enforced in the syntax.

  -- You can have modules inside modules. The name of a sub-module isn't
  -- qualified.
  module Expressions (X : Set)(x1, x2 : X) where

    -- There are three forms of sorts. Set = Set0.
    postulate A1 : Set
	      A2 : Set3
	      A3 : Prop

    -- Independent function space.
    fun1 : X -> X
    fun1 x = x

    -- Implicit independent function space. This is mostly included for
    -- symmetry, I can't come up with an example when this would be useful.
    fun2 : {X} -> X
    fun2 {x} = x

    -- Dependent function space.
    fun3 : (A:Set) -> A -> A
    fun3 A x = x

    -- Implicit dependent function space. 'A' is implicit so we don't have to
    -- write it out in the function definition.
    fun4 : {A:Set} -> A -> A
    fun4 x = x

    -- You can also write independent functions using the dependent function
    -- space syntax. Not that you'd ever want to.
    fun5 : (_:X) -> X
    fun5 x = x

    -- Lambdas can be domain free.
    const1 : {A, B : Set} -> A -> B -> A
    const1 = \x y -> x

    -- Or completely typed.
    const2 = \{A:Set}{B:Set}(x:A)(y:B) -> x -- inferable, no type needed

    -- You cannot mix typed and untyped arguments in the same lambda.
    const3 : {A, B : Set} -> A -> B -> A
    const3 = \{A}{B} -> \(x:A)(y:B) -> x

    -- You can have wildcards in lambdas
    const4 : {A, B : Set} -> A -> B -> A
    const4 = \x _ -> x

    -- Implicit arguments can be omitted in applications.
    x = const1 x1 x2

    -- Or made explicit.
    x' = const1 {X} {X} x1 x2

    -- Infix operators can be bound by lambdas. See ComplexDeclarations for
    -- more information about infix operators.
    dup : {A:Set} -> (A -> A -> A) -> A -> A
    dup = \(+) x -> x + x

  -- The two basic declarations are function definitions and datatype
  -- declarations.
  module BasicDeclarations (X : Set) where

    -- The most common declaration is the function definition. It consists of
    -- two parts; a type signature and a set of function clauses. Type
    -- signatures have the form 'id : type', no telescopes are allowed at this
    -- point. This can be discussed.
    id : X -> X
    id x = x

    -- You can omit the type signature if the type can be inferred.
    id' = id

    -- Datatypes are introduced with the data keyword.
    data Bool : Set where
      false : Bool
      true  : Bool

    -- The parameters to the datatype (A in this case) are in scope in the
    -- types of the constructors. At the moment inductive families are not
    -- supported.
    data List (A : Set) : Set where
      nil  : List A
      (::) : A -> List A -> List A

    -- When using a constructor as a function, the parameters are hidden
    -- arguments.
    singleton : X -> List X
    singleton x = x :: nil

    singleton' : X -> List X
    singleton' x = (::) {X} x (nil {X})

    -- You can pattern match over elements of a datatype when defining
    -- functions (and only then).
    null : (A : Set) -> List A -> Bool
    null A nil	   = true
    null A (x::xs) = false

    -- Patterns can be nested (and functions can be recursive).
    and : List Bool -> Bool
    and nil	    = true
    and (true::xs)  = and xs
    and (false::xs) = false

    -- Functions can be defined in an infix style. When doing this it must be
    -- clear what name is being defined without looking at fixities. Hence we
    -- could never remove the parenthesis around x::xs in the second clause.
    (++) : List X -> List X -> List X
    nil	    ++ ys = ys
    (x::xs) ++ ys = x :: (xs ++ ys)

    -- You can also use a combination of infix and prefix.
    (@) : {A, B, C : Set} -> (B -> C) -> (A -> B) -> A -> C
    (f @ g) x = f (g x)

  -- Declarations can appear in many different contexts and not all
  -- declarations are allowed everywhere.
  module ComplexDeclarations (X : Set) where

    -- You can introduce new constants with the postulate declaration. A
    -- postulate declaration takes a list of type signatures.
    postulate A : Set
	      a : A

    -- Let's introduce some datatypes so we have something to work with. At the
    -- same time we illustrate that layout is optional.
    data Nat  : Set where { zero : Nat;   suc  : Nat -> Nat }
    data Bool : Set where { false : Bool; true : Bool }

    {- We can declare the fixity of infix symbols. The fixity is tied to a
       particular binding of a name. The binding doesn't have to be in scope
       directly (as in the example below), but it should be possible to bring
       it into scope by moving the fixity declaration further down in the
       current block (but never inside things).

       The following wouldn't be allowed:

         infixl 15 +
         mutual
	   (+) : Nat -> Nat -> Nat
	   ..

       There are three forms: infix, infixl and infixr, for non-associative,
       left associative and right associative respectively. The number is the
       precedence level.
    -}

    infixl 15 +, `plus`

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

    plus = (+)

    -- The following code is to stress test the handling of infix applications.

    infixl 10 @
    infixl 11 @@
    infixr 10 #
    infixr 11 ##
    postulate
      (@)  : Nat -> Nat -> Nat
      (#)  : Nat -> Nat -> Nat
      (@@) : Nat -> Nat -> Nat
      (##) : Nat -> Nat -> Nat

    z = zero

    test1 = z @ (z # z)
    test2 = (z @ z) # z
    test3 = z # (z @ z)
    test4 = (z # z) @ z
    test5 = z ## z # z ## z # z
    test6 = z @@ z @ z @@ z @ z
    test7 = z # z @@ z @@ z # z

    -- Mutually recursive definition are introduced using the 'mutual' keyword.
    -- A mutual block can contain function definitions, datatypes
    -- (induction-recursion) and fixity declarations.
    mutual
      even : Nat -> Bool
      even zero	    = true
      even (suc n)  = odd n

      odd : Nat -> Bool
      odd zero	    = false
      odd (suc n)   = even n

    -- If a function is declared abstract the definition of the function is not
    -- visible outside the module. For an abstract datatype the constructors
    -- are hidden. Definitions that can appear in an abstract block are:
    -- function definitions, data declarations, fixity declarations, mutual
    -- blocks, open and name space declarations (see NameSpaces).
    abstract
      data Stack : Set where
	nil  : Stack
	cons : A -> Stack -> Stack

      empty : Stack
      empty = nil

      push : A -> Stack -> Stack
      push = cons

    -- Local declarations are introduces either with a let or in a where
    -- clause. A where clause is attached to a function clause. Everything that
    -- can appear in an abstract block can appear in a local declaration, plus
    -- abstract blocks. Local functions can be recursive.
    foo : (A : Set) -> A -> A
    foo A x = let f : Local -> A
		  f (local y) = y
	      in  f (local x)
      where
	data Local : Set where
	  local : A -> Local

    -- You can declare things to be private to the current module. This means
    -- that they cannot be accessed outside the module (but they're still
    -- visible inside the module and its submodules). The only things that
    -- cannot appear in a private block are other private blocks and import
    -- statements.
    private
      bar : X -> X
      bar x = x

    -- Private declarations can go inside mutual and abstract blocks.
    mutual
      private f : Nat -> Nat
	      f zero	= zero
	      f (suc n) = g n

      g : Nat -> Nat
      g n = f n

    abstract
      Nat' : Set
      Nat' = Nat

      private h : Nat' -> Nat
	      h n = n

  -- A name space is something that contains names. You can create new
  -- name spaces and bring names from a name space into scope.
  module NameSpaces where

    -- To access definitions from a module in a different file, you have to
    -- 'import' this module. Only top-level modules (which have their own
    -- files) can be imported.

    -- If the imported module is not parameterised a name space with the same
    -- name as the module is created.
    import examples.syntax.ModuleA

    -- We can now refer to things from ModuleA using the created name
    -- space.  Note that no unqualified names were brought into scope
    -- (except, perhaps, the name of the name space). [To bring
    -- unqualified names into scope we have to use the 'open'
    -- declaration.]
    FunnyNat = examples.syntax.ModuleA.Nat

    -- If the name of an imported module clashes with a local module we might
    -- have to rename the module we are importing
    import examples.syntax.ModuleA as A
    import examples.syntax.ModuleA as A' using (Nat)

    Nat1 = A.Nat
    Nat2 = A'.Nat

    {- You can't project from a parameterised module. It has to be
       instantiated first. The only thing that happens when importing
       is that the module name 'examples.syntax.ModuleB' is brought
       into scope (and the type checker goes away and type checks this
       module).
    -}
    import examples.syntax.ModuleB

    -- To instantiate ModuleB we need something to instantiate it with.
    postulate X	   : Set
	      (==) : X -> X -> Prop
	      refl : (x : X) -> x == x

    -- To instantiate a module you create a new module and define it as the
    -- instantiation in question.
    module B = examples.syntax.ModuleB X (==) refl

    -- Now the module B contains all the names from ModuleB.
    XList = B.List
    And	  = B./\    -- qualified operators are not infix symbols

    dummyX = B.SubModule.dummy	-- submodules of ModuleB are also in scope

    -- This of course works for non-parameterised modules as well.
    module B' = B

    -- And you can create parameterised modules this way.
    module BX ((==) : X -> X -> Prop)(refl : (x : X) -> x == x) = B X (==) refl

    -- To bring names from a module into scope you use an open declaration.
    open examples.syntax.ModuleA

    two : FunnyNat
    two = eval (plus (suc zero) (suc zero))

    {- In all three declarations (import, module instantiation and open) you
       can give modifiers that affect the names which are imported. There are
       three modifiers:

	using (x1;..;xn)		only import x1,..,xn
	hiding (x1;..;xn)		import everything but x1,..,xn
	renaming (x1 to y1;..;xn to yn)	import x1,..,xn but call them y1,..,yn

      Restrictions:
	- a modifier can appear only once
	- 'using' and 'hiding' cannot appear together
	- imported names must be distinct (e.g. you cannot rename to a name
	  that is already being imported).
    -}

    -- B1 only contains True and False
    module B1 = B using (True; False)

    -- B2 contains True, False and And where And = B./\
    module B2 = B using (True; False) renaming (/\ to And)

    -- B3 contains everything from B except reflEqList and eqList, plus ===
    -- where (===) = B.eqList.
    module B3 = B hiding (reflEqList) renaming (eqList to ===)

    -- When referring to sub modules you have to be explicitly about it being
    -- a module
    module B4 = B renaming (module SubModule to Sub)

    dummy : X
    dummy = B4.Sub.dummy

  -- There are two kinds of meta variables; question marks and underscores.
  -- Question marks are used for interaction and underscores for implicit
  -- arguments.
  module MetaVariables where

    postulate X : Set
	      x : X

    -- There are two ways of writing a question mark: ? and {! ... !}
    -- The type checker will not complain about unsolved question marks (unless
    -- you claim you are done).
    incomplete : {A:Set} -> A -> A
    incomplete x = ?

    incomplete' : {A:Set} -> A -> A
    incomplete' x = {! you can put anything in here,
		       even {! nested holes !}
		    !}

    -- Underscores should always be solvable locally. Internally underscores
    -- are inserted for implicit arguments, but there are cases where you would
    -- like to write them explicitly. For instance, if you want to give one but
    -- not all implicit arguments to a function explicitly.
    underscore : ({A,B,C:Set} -> (A -> A) -> B -> C) -> X
    underscore f = f {_} {X} {_} (\y -> y) x

    -- Note that '_' is not an identifier character. The current use of
    -- underscore is not the real reason for this. The idea is rather that
    -- underscore will be used for subscripts.
    id : (A : Set) -> A -> A
    id A x = x

    x' = id_x -- this means id _ x

  -- The parser supports four types of literals. The syntax is the same as in
  -- Haskell (since that meant I could steal the lexer for them from ghc).
  module Literals where

    -- We haven't decided how to handle built-in types.
    postulate Integer : Set
	      Char    : Set
	      String  : Set
	      Float   : Set

    fortyTwo : Integer
    fortyTwo = 42

    helloWorld : String
    helloWorld = "Hello World!"

    escape : Char
    escape = '\ESC'

    pi : Float
    pi = 3.141592

  -- There are few things that the parser doesn't implement.

    {- Fancy case. I haven't been able to come up with a nice syntax for the
       fancy case statement.  The difficulty is that we should make it clear
       what arguments to the elimination rule will appear as patterns (the
       targets). Suggestions are welcome.

       Also I'm not sure that we want the fancy case. It would be better to
       have a good way of doing actual pattern matching on inductive families.
    -}

    {- Relative imports. You might want to be able to say

	import .ModuleA

       to import the module 'current.directory.ModuleA'. Easy to implement but
       I'm not sure it's that painful to write the complete name (not a problem
       in Haskell for instance). Drawbacks: it looks kind of funny and it adds
       an extra bit of syntax to remember.
    -}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module LitDistinct where

{-# BUILTIN STRING String #-}

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

data False : Set where

foo : "bar" == "baz" -> False
foo ()

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Data.List hiding ([_]) renaming (_∷_ to _∷ₗ_)
open import Data.Maybe
open import Data.Product

open import AEff
open import EffectAnnotations
open import Renamings
open import Substitutions
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary

module Preservation where

-- BINDING CONTEXTS

BCtx = List VType

-- WELL-TYPED EVALUATION CONTEXTS

data _⊢E[_]⦂_ (Γ : Ctx) : (Δ : BCtx) → CType → Set where

  [-]              : {C : CType} →
                     -------------
                     Γ ⊢E[ [] ]⦂ C

  let=_`in_        : {Δ : BCtx}
                     {X Y : VType}
                     {o : O}
                     {i : I} →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     Γ ∷ X ⊢M⦂ Y ! (o , i) →
                     ------------------------
                     Γ ⊢E[ Δ ]⦂ Y ! (o , i)

  ↑                : {Δ : BCtx}
                     {X : VType}
                     {o : O}
                     {i : I} →
                     (op : Σₛ) →
                     op ∈ₒ o →
                     Γ ⊢V⦂ ``(payload op) →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     ------------------------
                     Γ ⊢E[ Δ ]⦂ X ! (o , i)

  ↓                : {Δ : BCtx}
                     {X : VType}
                     {o : O}
                     {i : I}
                     (op : Σₛ) →
                     Γ ⊢V⦂ ``(payload op) →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     ---------------------------
                     Γ ⊢E[ Δ ]⦂ X ! op ↓ₑ (o , i)

  promise_∣_↦_`in_ : {Δ : BCtx}
                     {X Y : VType}
                     {o o' : O}
                     {i i' : I} →
                     (op : Σₛ) →
                     lkpᵢ op i ≡ just (o' , i') →
                     Γ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o' , i') →
                     Γ ∷ ⟨ X ⟩ ⊢E[ Δ ]⦂ Y ! (o , i) →
                     ------------------------------------------
                     Γ ⊢E[ X ∷ₗ Δ ]⦂ Y ! (o , i)

  coerce           : {Δ : BCtx}
                     {X : VType}
                     {o o' : O}
                     {i i' : I} →
                     o ⊑ₒ o' →
                     i ⊑ᵢ i' →
                     Γ ⊢E[ Δ ]⦂ X ! (o , i) →
                     ------------------------
                     Γ ⊢E[ Δ ]⦂ X ! (o' , i')

-- MERGING AN ORDINARY CONTEXT AND A BINDING CONTEXT

infix 30 _⋈_

_⋈_ : Ctx → BCtx → Ctx
Γ ⋈ [] = Γ
Γ ⋈ (X ∷ₗ Δ) = (Γ ∷ ⟨ X ⟩) ⋈ Δ

-- FINDING THE TYPE OF THE HOLE OF A WELL-TYPED EVALUATION CONTEXT

hole-ty-e : {Γ : Ctx} {Δ : BCtx} {C : CType} → Γ ⊢E[ Δ ]⦂ C → CType
hole-ty-e {_} {_} {C} [-] =
  C
hole-ty-e (let= E `in M) =
  hole-ty-e E
hole-ty-e (↑ op p V E) =
  hole-ty-e E
hole-ty-e (↓ op V E) =
  hole-ty-e E
hole-ty-e (promise op ∣ p ↦ M `in E) =
  hole-ty-e E
hole-ty-e (coerce p q E) =
  hole-ty-e E

-- FILLING A WELL-TYPED EVALUATION CONTEXT

{- LEMMA 3.5 -}

infix 30 _[_]

_[_] : {Γ : Ctx} {Δ : BCtx} {C : CType} → (E : Γ ⊢E[ Δ ]⦂ C) → Γ ⋈ Δ ⊢M⦂ (hole-ty-e E) → Γ ⊢M⦂ C
[-] [ M ] =
  M
(let= E `in N) [ M ] =
  let= (E [ M ]) `in N
↑ op p V E [ M ] =
  ↑ op p V (E [ M ])
↓ op V E [ M ] =
  ↓ op V (E [ M ])
(promise op ∣ p ↦ N `in E) [ M ] =
  promise op ∣ p ↦ N `in (E [ M ])
coerce p q E [ M ] =
  coerce p q (E [ M ])

-- STRENGTHENING OF GROUND VALUES WRT BOUND PROMISES

strengthen-var : {Γ : Ctx} → (Δ : BCtx) → {A : BType} → `` A ∈ Γ ⋈ Δ → `` A ∈ Γ
strengthen-var [] x = x
strengthen-var (y ∷ₗ Δ) x with strengthen-var Δ x
... | Tl p = p

strengthen-val : {Γ : Ctx} {Δ : BCtx} {A : BType} → Γ ⋈ Δ ⊢V⦂ `` A → Γ ⊢V⦂ `` A
strengthen-val {_} {Δ} (` x) =
  ` strengthen-var Δ x
strengthen-val (``_ c) =
  ``_ c

strengthen-val-[] : {Γ : Ctx}
                    {A : BType} →
                    (V : Γ ⋈ [] ⊢V⦂ `` A) →
                    --------------------
                    strengthen-val {Δ = []} V ≡ V

strengthen-val-[] (` x) =
  refl
strengthen-val-[] (``_ c) =
  refl

-- SMALL-STEP OPERATIONAL SEMANTICS FOR WELL-TYPED COMPUTATIONS
-- (ADDITIONALLY SERVES AS THE PRESERVATION THEOREM)

{- THEOREM 3.6 -}

infix 10 _↝_

data _↝_ {Γ : Ctx} : {C : CType} → Γ ⊢M⦂ C → Γ ⊢M⦂ C → Set where

  -- COMPUTATIONAL RULES

  apply           : {X : VType}
                    {C : CType} →
                    (M : Γ ∷ X ⊢M⦂ C) →
                    (V : Γ ⊢V⦂ X) →
                    ----------------------
                    (ƛ M) · V
                    ↝
                    M [ id-subst [ V ]s ]m

  let-return      : {X Y : VType}
                    {o : O}
                    {i : I} →
                    (V : Γ ⊢V⦂ X) →
                    (N : Γ ∷ X ⊢M⦂ Y ! (o , i)) →
                    -----------------------------
                    let= (return V) `in N
                    ↝
                    N [ id-subst [ V ]s ]m

  let-↑           : {X Y : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ} →
                    (p : op ∈ₒ o) →
                    (V : Γ ⊢V⦂ ``(payload op)) →
                    (M : Γ ⊢M⦂ X ! (o , i)) →
                    (N : Γ ∷ X ⊢M⦂ Y ! (o , i)) →
                    -----------------------------
                    let= (↑ op p V M) `in N
                    ↝
                    ↑ op p V (let= M `in N)

  let-promise     : {X Y Z : VType}
                    {o o' : O}
                    {i i' : I}
                    {op : Σₛ} →
                    (p : lkpᵢ op i ≡ just (o' , i')) →
                    (M₁ : Γ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o' , i')) →
                    (M₂ : Γ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i)) →
                    (N : Γ ∷ Y ⊢M⦂ Z ! (o , i)) →
                    ---------------------------------------------------------------------------
                    let= (promise op ∣ p ↦ M₁ `in M₂) `in N
                    ↝
                    (promise op ∣ p ↦ M₁ `in (let= M₂ `in (M-rename (comp-ren exchange wk₁) N)))

  letrec-unfold   : {X : VType}
                    {C D : CType}
                    (M : Γ ∷ (X ⇒ C) ∷ X ⊢M⦂ C) →
                    (N : Γ ∷ (X ⇒ C) ⊢M⦂ D) →
                    ----------------------------------------
                    (letrec M `in N)
                    ↝
                    N [ id-subst [ ƛ (letrec M-rename wk₃ M `in M-rename exchange M) ]s ]m

  promise-↑       : {X Y : VType}
                    {o o' : O}
                    {i i' : I}
                    {op op' : Σₛ} →
                    (p : lkpᵢ op i ≡ just (o' , i')) →
                    (q : op' ∈ₒ o) →
                    (V : Γ ∷ ⟨ X ⟩ ⊢V⦂ ``(payload op')) →
                    (M : Γ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i)) →
                    --------------------------------------------
                    (promise op ∣ p ↦ M `in (↑ op' q V N))
                    ↝
                    ↑ op' q (strengthen-val {Δ = X ∷ₗ []} V) (promise op ∣ p ↦ M `in N)

  ↓-return        : {X : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ} →
                    (V : Γ ⊢V⦂ ``(payload op)) →
                    (W : Γ ⊢V⦂ X) →
                    ----------------------------------------------------------------
                    ↓ {o = o} {i = i} op V (return W)
                    ↝
                    return {o = proj₁ (op ↓ₑ (o , i))} {i = proj₂ (op ↓ₑ (o , i))} W

  ↓-↑             : {X : VType}
                    {o : O}
                    {i : I}
                    {op : Σₛ}
                    {op' : Σₛ} →
                    (p : op' ∈ₒ o) →
                    (V : Γ ⊢V⦂ ``(payload op)) →
                    (W : Γ ⊢V⦂ ``(payload op')) →
                    (M : Γ ⊢M⦂ X ! (o , i)) →
                    -------------------------------
                    ↓ op V (↑ op' p W M)
                    ↝
                    ↑ op' (↓ₑ-⊑ₒ op' p) W (↓ op V M)

  ↓-promise-op    : {X Y : VType}
                    {o o' : O}
                    {i i' : I}
                    {op : Σₛ} →
                    (p : lkpᵢ op i ≡ just (o' , i')) →
                    (V : Γ ⊢V⦂ ``(payload op)) →
                    (M : Γ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i)) →
                    ---------------------------------------------------------------------------------------
                    ↓ op V (promise op ∣ p ↦ M `in N )
                    ↝
                    (let= (coerce (↓ₑ-⊑ₒ-o' {o} p) (↓ₑ-⊑ₒ-i' {o} p) (M [ id-subst [ V ]s ]m)) `in
                      ↓ op (V-rename wk₁ V) ((M-rename (comp-ren exchange wk₁) N) [ id-subst [ ` Hd ]s ]m))

  ↓-promise-op'   : {X Y : VType}
                    {o o' : O}
                    {i i' : I}
                    {op op' : Σₛ} →
                    (p : ¬ op ≡ op') →
                    (q : lkpᵢ op' i ≡ just (o' , i')) →
                    (V : Γ ⊢V⦂ ``(payload op)) →
                    (M : Γ ∷ ``(payload op') ⊢M⦂ ⟨ X ⟩ ! (o' , i')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i)) →
                    ------------------------------------------------------------------------------------------
                    ↓ op V (promise op' ∣ q ↦ M `in N )
                    ↝
                    promise_∣_↦_`in_ {o' = proj₁ (lkpᵢ-↓ₑ-neq {o = o} {i = i} p q)}
                                     {i' = proj₁ (proj₂ (lkpᵢ-↓ₑ-neq {o = o} {i = i} p q))}
                                     op'
                                     (proj₁ (proj₂ (proj₂ (lkpᵢ-↓ₑ-neq {o = o} {i = i} p q))))
                                     (coerce (proj₁ (proj₂ (proj₂ (proj₂ (lkpᵢ-↓ₑ-neq {o = o} {i = i} p q)))))
                                             (proj₂ (proj₂ (proj₂ (proj₂ (lkpᵢ-↓ₑ-neq {o = o} {i = i} p q)))))
                                             M)
                                     (↓ op (V-rename wk₁ V) N)

  await-promise   : {X : VType}
                    {C : CType} →
                    (V : Γ ⊢V⦂ X) →
                    (M : Γ ∷ X ⊢M⦂ C) →
                    --------------------
                    await ⟨ V ⟩ until M
                    ↝
                    M [ id-subst [ V ]s ]m

  -- EVALUATION CONTEXT RULE

  context         : {Δ : BCtx}
                    {C : CType} →
                    (E : Γ ⊢E[ Δ ]⦂ C) →
                    {M N : Γ ⋈ Δ ⊢M⦂ (hole-ty-e E)} →
                    M ↝ N →
                    -------------------------------
                    E [ M ] ↝ E [ N ]

  -- COERCION RULES
  -- (THE RESULT OF WORKING WITH WELL-TYPED SYNTAX AND MAKING SUBSUMPTION INTO AN EXPLICIT COERCION)

  coerce-return   : {X : VType}
                    {o o' : O}
                    {i i' : I}
                    {p : o ⊑ₒ o'}
                    {q : i ⊑ᵢ i'} →
                    (V : Γ ⊢V⦂ X) →
                    --------------------------------
                    coerce p q (return V) ↝ return V

  coerce-↑        : {X : VType}
                    {o o' : O}
                    {i i' : I}
                    {p : o ⊑ₒ o'}
                    {q : i ⊑ᵢ i'}
                    {op : Σₛ} →
                    (r : op ∈ₒ o) →
                    (V : Γ ⊢V⦂ ``(payload op)) →
                    (M : Γ ⊢M⦂ X ! (o , i)) →
                    -------------------------------
                    coerce p q (↑ op r V M)
                    ↝
                    ↑ op (p op r) V (coerce p q M)

  coerce-promise  : {X Y : VType}
                    {o o' o'' : O}
                    {i i' i'' : I}
                    {p : o ⊑ₒ o'}
                    {q : i ⊑ᵢ i'}
                    {op : Σₛ} →
                    (r : lkpᵢ op i ≡ just (o'' , i''))
                    (M : Γ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o'' , i'')) →
                    (N : Γ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i)) →
                    ------------------------------------------------------------------
                    coerce p q (promise op ∣ r ↦ M `in N)
                    ↝
                    promise_∣_↦_`in_ {o' = lkpᵢ-nextₒ q r}
                                     {i' = lkpᵢ-nextᵢ q r}
                                     op
                                     (lkpᵢ-next-eq q r)
                                     (coerce (lkpᵢ-next-⊑ₒ q r) (lkpᵢ-next-⊑ᵢ q r) M)
                                     (coerce p q N)

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


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

open import HoTT

{- Proof that if [A] and [B] are two propositions, then so is [A * B]. -}

module homotopy.PropJoinProp
  {i} {A : Type i} (pA : is-prop A)
  {j} {B : Type j} (pB : is-prop B) where

contr-left : (a : A) → is-contr (A * B)
contr-left a = left a , Pushout-elim
  (λ a' → ap left (prop-has-all-paths pA a a'))
  (λ b' → glue (a , b'))
  (λ {(a' , b') → ↓-cst=idf-in' $ ! $
    ↓-app=cst-out (apd (λ a → glue (a , b')) (prop-has-all-paths pA a a'))})

contr-right : (b : B) → is-contr (A * B)
contr-right b = right b , Pushout-elim
  (λ a' → ! (glue (a' , b)))
  (λ b' → ap right (prop-has-all-paths pB b b'))
  (λ {(a' , b') → ↓-cst=idf-in' $
    ! (glue (a' , b)) ∙ glue (a' , b')
      =⟨ ! (↓-cst=app-out' $ apd (λ b → glue (a' , b)) (prop-has-all-paths pB b b'))
        |in-ctx ! (glue (a' , b)) ∙_ ⟩
    ! (glue (a' , b)) ∙ glue (a' , b) ∙ ap right (prop-has-all-paths pB b b')
      =⟨ ! $ ∙-assoc (! (glue (a' , b))) (glue (a' , b)) (ap right (prop-has-all-paths pB b b')) ⟩
    (! (glue (a' , b)) ∙ glue (a' , b)) ∙ ap right (prop-has-all-paths pB b b')
      =⟨ !-inv-l (glue (a' , b)) |in-ctx _∙ ap right (prop-has-all-paths pB b b') ⟩
    ap right (prop-has-all-paths pB b b')
      =∎})

prop*prop-is-prop : is-prop (A * B)
prop*prop-is-prop = inhab-to-contr-is-prop $
  Pushout-rec contr-left contr-right (λ _ → prop-has-all-paths is-contr-is-prop _ _)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text: module Categories.Comonad where

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Data.Binary.Skew where

open import Prelude
open import Data.Nat
open import Data.List

𝔹 : Type
𝔹 = List ℕ

inc : 𝔹 → 𝔹
inc [] = zero ∷ []
inc (x ∷ []) = zero ∷ x ∷ []
inc (x₁ ∷ zero   ∷ xs) = suc x₁ ∷ xs
inc (x₁ ∷ suc x₂ ∷ xs) = zero ∷ x₁ ∷ x₂ ∷ xs

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero ⇑⟧ = []
⟦ suc n ⇑⟧ = inc ⟦ n ⇑⟧

skew : ℕ → ℕ
skew n = suc (n + n)

w : ℕ → ℕ → ℕ
w zero    a = a
w (suc n) a = skew (w n a)

⟦_∷_⇓⟧^ : ℕ → (ℕ → ℕ) → ℕ → ℕ
⟦ x ∷ xs ⇓⟧^ a = let a′ = w x a in a′ + xs (skew a′)

⟦_⇓⟧ : 𝔹 → ℕ
⟦ [] ⇓⟧ = zero
⟦ x ∷ xs ⇓⟧ = let a = w x 1 in a + foldr ⟦_∷_⇓⟧^ (const zero) xs a

-- open import Path.Reasoning
-- import Data.Nat.Properties as ℕ

-- inc-suc : ∀ x → ⟦ inc x ⇓⟧ ≡ suc ⟦ x ⇓⟧
-- inc-suc [] = refl
-- inc-suc (x  ∷ []) = refl
-- inc-suc (x  ∷ zero   ∷ xs) = cong suc (ℕ.+-assoc (w x 1) (w x 1) _)
-- inc-suc (x₁ ∷ suc x₂ ∷ xs) = cong suc (cong (w x₁ 1 +_) {!!})

-- 𝔹-rightInv : ∀ x → ⟦ ⟦ x ⇑⟧ ⇓⟧ ≡ x
-- 𝔹-rightInv zero = refl
-- 𝔹-rightInv (suc x) = {!!}

-- 𝔹-leftInv : ∀ x → ⟦ ⟦ x ⇓⟧ ⇑⟧ ≡ x
-- 𝔹-leftInv [] = refl
-- 𝔹-leftInv (x ∷ xs) = {!!}

-- 𝔹⇔ℕ : 𝔹 ⇔ ℕ
-- 𝔹⇔ℕ .fun = ⟦_⇓⟧
-- 𝔹⇔ℕ .inv = ⟦_⇑⟧
-- 𝔹⇔ℕ .rightInv x = {!!}
-- 𝔹⇔ℕ .leftInv = {!!}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2011-05-30
-- {-# OPTIONS -v tc.lhs.unify:50 #-}
module Issue292c where

data ⊥ : Set where

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

infix 4 _≅_

data _≅_ {A : Set} (x : A) : ∀ {B : Set} → B → Set where
  refl : x ≅ x

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

data Bool : Set where true false : Bool

data Unit1 : Set where unit1 : Unit1
data Unit2 : Set where unit2 : Unit2

D : Bool -> Set
D true  = Unit1
D false = Unit2

P : Set -> Set
P S = Σ S (\s → s ≅ unit1)

pbool : P (D true)
pbool = unit1 , refl

¬pbool2 : ¬ P (D false)
¬pbool2 ( unit2 , () )

{- expected error
unit2 ≅ unit1 should be empty, but that's not obvious to me
when checking that the clause ¬pbool2 (unit2 , ()) has type
¬ P (D false)
-}


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

syntax FOL

type
  * : 0-ary
  N : 0-ary

term
  false : * | ⊥
  or    : *  *  ->  * | _∨_ l20
  true  : * | ⊤
  and   : *  *  ->  * | _∧_ l20
  not   : *  ->  * | ¬_ r50
  eq    : N  N  ->  * | _≟_ l20
  all   : N.*  ->  * | ∀′
  ex    : N.*  ->  * | ∃′

theory
  (⊥U∨ᴸ) a |> or (false, a) = a
  (⊥U∨ᴿ) a |> or (a, false) = a
  (∨A) a b c |> or (or(a, b), c) = or (a, or(b, c))
  (∨C) a b |> or(a, b) = or(b, a)
  (⊤U∧ᴸ) a |> and (true, a) = a
  (⊤U∧ᴿ) a |> and (a, true) = a
  (∧A) a b c |> and (and(a, b), c) = and (a, and(b, c))
  (∧D∨ᴸ) a b c |> and (a, or (b, c)) = or (and(a, b), and(a, c))
  (∧D∨ᴿ) a b c |> and (or (a, b), c) = or (and(a, c), and(b, c))
  (∨B∧ᴸ) a b |> or (and (a, b), a) = a
  (∨B∧ᴿ) a b |> or (a, and (a, b)) = a
  (∧B∨ᴸ) a b |> and (or (a, b), a) = a
  (∧B∨ᴿ) a b |> and (a, or (a, b)) = a
  (⊥X∧ᴸ) a |> and (false, a) = false
  (⊥X∧ᴿ) a |> and (a, false) = false
  (¬N∨ᴸ) a |> or (not (a), a) = false
  (¬N∨ᴿ) a |> or (a, not (a)) = false
  (∧C) a b |> and(a, b) = and(b, a)
  (∨I) a |> or(a, a) = a
  (∧I) a |> and(a, a) = a
  (¬²) a |> not(not (a)) = a
  (∨D∧ᴸ) a b c |> or (a, and (b, c)) = and (or(a, b), or(a, c))
  (∨D∧ᴿ) a b c |> or (and (a, b), c) = and (or(a, c), or(b, c))
  (⊤X∨ᴸ) a |> or (true, a) = true
  (⊤X∨ᴿ) a |> or (a, true) = true
  (¬N∧ᴸ) a |> and (not (a), a) = false
  (¬N∧ᴿ) a |> and (a, not (a)) = false
  (DM∧) a b |> not (and (a, b)) = or (not(a), not(b))
  (DM∨) a b |> not (or (a, b)) = and (not(a), not(b))
  (DM∀) p : N.* |> not (all (x. p[x])) = ex  (x. not(p[x]))
  (DM∃) p : N.* |> not (ex  (x. p[x])) = all (x. not(p[x]))
  (∀D∧) p q : N.* |> all (x. and(p[x], q[x])) = and (all(x.p[x]), all(x.q[x]))
  (∃D∨) p q : N.* |> ex (x. or(p[x], q[x])) = or (ex(x.p[x]), ex(x.q[x]))
  (∧P∀ᴸ) p : *  q : N.* |> and (p, all(x.q[x])) = all (x. and(p, q[x]))
  (∧P∃ᴸ) p : *  q : N.* |> and (p, ex (x.q[x])) = ex  (x. and(p, q[x]))
  (∨P∀ᴸ) p : *  q : N.* |> or  (p, all(x.q[x])) = all (x. or (p, q[x]))
  (∨P∃ᴸ) p : *  q : N.* |> or  (p, ex (x.q[x])) = ex  (x. or (p, q[x]))
  (∧P∀ᴿ) p : N.*  q : * |> and (all(x.p[x]), q) = all (x. and(p[x], q))
  (∧P∃ᴿ) p : N.*  q : * |> and (ex (x.p[x]), q) = ex  (x. and(p[x], q))
  (∨P∀ᴿ) p : N.*  q : * |> or  (all(x.p[x]), q) = all (x. or (p[x], q))
  (∨P∃ᴿ) p : N.*  q : * |> or  (ex (x.p[x]), q) = ex  (x. or (p[x], q))
  (∀Eᴸ) p : N.*  n : N |> all (x.p[x]) = and (p[n], all(x.p[x]))
  (∃Eᴸ) p : N.*  n : N |> ex  (x.p[x]) = or  (p[n], ex (x.p[x]))
  (∀Eᴿ) p : N.*  n : N |> all (x.p[x]) = and (all(x.p[x]), p[n])
  (∃Eᴿ) p : N.*  n : N |> ex  (x.p[x]) = or  (ex (x.p[x]), p[n])
  (∃⟹) p : N.*  q : * |> imp (ex (x.p[x]), q) = all (x. imp(p[x], q))
  (∀⟹) p : N.*  q : * |> imp (all(x.p[x]), q) = ex  (x. imp(p[x], q))
-}

module FOL.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import FOL.Signature

private
  variable
    Γ Δ Π : Ctx
    α : FOLT
    𝔛 : Familyₛ

-- Inductive term declaration
module FOL:Terms (𝔛 : Familyₛ) where

  data FOL : Familyₛ where
    var  : ℐ ⇾̣ FOL
    mvar : 𝔛 α Π → Sub FOL Π Γ → FOL α Γ

    ⊥   : FOL * Γ
    _∨_ : FOL * Γ → FOL * Γ → FOL * Γ
    ⊤   : FOL * Γ
    _∧_ : FOL * Γ → FOL * Γ → FOL * Γ
    ¬_  : FOL * Γ → FOL * Γ
    _≟_ : FOL N Γ → FOL N Γ → FOL * Γ
    ∀′  : FOL * (N ∙ Γ) → FOL * Γ
    ∃′  : FOL * (N ∙ Γ) → FOL * Γ

  infixl 20 _∨_
  infixl 20 _∧_
  infixr 50 ¬_
  infixl 20 _≟_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  FOLᵃ : MetaAlg FOL
  FOLᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (falseₒ ⋮ _)     → ⊥
      (orₒ    ⋮ a , b) → _∨_ a b
      (trueₒ  ⋮ _)     → ⊤
      (andₒ   ⋮ a , b) → _∧_ a b
      (notₒ   ⋮ a)     → ¬_  a
      (eqₒ    ⋮ a , b) → _≟_ a b
      (allₒ   ⋮ a)     → ∀′  a
      (exₒ    ⋮ a)     → ∃′  a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module FOLᵃ = MetaAlg FOLᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : FOL ⇾̣ 𝒜
    𝕊 : Sub FOL Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞  ⊥        = 𝑎𝑙𝑔 (falseₒ ⋮ tt)
    𝕤𝕖𝕞 (_∨_ a b) = 𝑎𝑙𝑔 (orₒ    ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞  ⊤        = 𝑎𝑙𝑔 (trueₒ  ⋮ tt)
    𝕤𝕖𝕞 (_∧_ a b) = 𝑎𝑙𝑔 (andₒ   ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (¬_  a)   = 𝑎𝑙𝑔 (notₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (_≟_ a b) = 𝑎𝑙𝑔 (eqₒ    ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (∀′  a)   = 𝑎𝑙𝑔 (allₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (∃′  a)   = 𝑎𝑙𝑔 (exₒ    ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ FOLᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ FOL α Γ) → 𝕤𝕖𝕞 (FOLᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (falseₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (orₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (trueₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (andₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (notₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (eqₒ    ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (allₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (exₒ    ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ FOL ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : FOL ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ FOLᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : FOL α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub FOL Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! ⊥ = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_∨_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! ⊤ = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_∧_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (¬_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_≟_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (∀′ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (∃′ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
FOL:Syn : Syntax
FOL:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = FOL:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open FOL:Terms 𝔛 in record
    { ⊥ = FOL ⋉ FOLᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax FOL:Syn public
open FOL:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands FOLᵃ public
open import SOAS.Metatheory FOL:Syn public

-- Derived operations
_⟹_ : FOL 𝔛 * Γ → FOL 𝔛 * Γ → FOL 𝔛 * Γ
p ⟹ q = ¬ p ∨ q


text:
open import Agda.Builtin.Equality

data ⊥ : Set where

cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

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

data D : Set where
  c1 : D → ⊥ → D
  c2 : (⊥ → D) → D

cycle : ∀ {n} → c2 (c1 n) ≡ n → ⊥
cycle ()

d : D
d = c2 λ ()

only-one-D : (x : D) → x ≡ d
only-one-D (c2 x) = cong c2 (funExt (λ ()))

boom : ⊥
boom = cycle (only-one-D (c2 (c1 d)))


text:
open import Data.List
open import Data.List.Any
open import Data.Nat as ℕ
data capn-kind : Set where
 cKStruct : capn-kind
 ckInter  : capn-kind
open import Relation.Binary.PropositionalEquality
open Membership (setoid capn-kind)
capn-ctx = List capn-kind
data capn-τ : {Γ : capn-ctx} → Set
data capn-field : {Γ : capn-ctx} → Set
data capn-method : {Γ : capn-ctx} → Set

--While the actual capnp schema supports declaration of structs in any order / arbitrary recursion,
--I am limiting this to reference to structs-declared-so-far. This makes the model simpler, without
--removing any of the power (I think), though it would be less convenient to write code for.

data capn-τ where
  cVoid      : ∀ {Γ} → capn-τ {Γ}
  cBool      : ∀ {Γ} → capn-τ {Γ}
  cInt8      : ∀ {Γ} → capn-τ {Γ}
  cInt16     : ∀ {Γ} → capn-τ {Γ}
  cInt32     : ∀ {Γ} → capn-τ {Γ}
  cInt64     : ∀ {Γ} → capn-τ {Γ}
  cUInt8     : ∀ {Γ} → capn-τ {Γ}
  cUInt16    : ∀ {Γ} → capn-τ {Γ}
  cUInt32    : ∀ {Γ} → capn-τ {Γ}
  cUInt64    : ∀ {Γ} → capn-τ {Γ}
  cFloat32   : ∀ {Γ} → capn-τ {Γ}
  cFloat64   : ∀ {Γ} → capn-τ {Γ}
  cData      : ∀ {Γ} → capn-τ {Γ}
  cText      : ∀ {Γ} → capn-τ {Γ}
  cList      : ∀ {Γ} → capn-τ {Γ} → capn-τ {Γ}
  cStruct    : ∀ {Γ} → List (capn-field {cKStruct ∷ Γ}) → capn-τ {cKStruct ∷ Γ}
  cEnum      : ∀ {Γ} → ℕ → capn-τ {Γ}
  cVar       : ∀ {Γ k} → (k ∈ Γ) → capn-τ {Γ}
  cInterface : ∀ {Γ} → List (capn-method {ckInter ∷ Γ}) → capn-τ {ckInter ∷ Γ}

--I'm ignoring field names, because fields can be indexed by list position, which is enough for proofs
--I'm also ignoring groups, since they are just an addressing convenience
data capn-field where
  cField   : ∀ {Γ} → capn-τ {Γ} → capn-field {Γ}
  cUnion   : ∀ {Γ} → List (capn-field {Γ})→ capn-field {Γ}
  cAny     : ∀ {Γ} → capn-field {Γ}

data capn-method where
  cMeth : ∀ {Γ} → List (capn-τ {Γ}) → List (capn-τ {Γ}) → capn-method {Γ}

max_stars_repo_name: maurer/holmes

max_issues_repo_name: maurer/holmes

max_forks_repo_name: maurer/holmes