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

open import common
open import syntx

{- The sort corresponding to judgments -}

data JudgmentSort : Set where
  Ty  : JudgmentSort
  Tm  : JudgmentSort
  Ty= : JudgmentSort
  Tm= : JudgmentSort

JudgmentArityArgs = ArityArgs JudgmentSort
JudgmentArity = Arity JudgmentSort

{-
Judgments are indexed by the signature, their ambient context, the length of their local context,
and their sort.

We can see judgments as consisting of two contexts, one normal context (the ambient context) and
then one dependent context (the local context). The reason is that all typing rules occur in an
ambient context which never changes, and sometimes add new assumptions (to the local context).
Therefore we will never have to check that the ambient contexts are equal, it will be forced by the
typing.

Indexing judgments by sorts is very good to get rid of absurd cases, when giving typing rules and
that some judgments are supposed to have certain sorts.
-}

data Judgment (Σ : Signature) {m : ℕ} (Γ : Ctx Σ m) (n : ℕ) : JudgmentSort → Set where
  _⊢_       : (Δ : DepCtx Σ m n) → TyExpr Σ (m + n) → Judgment Σ Γ n Ty
  _⊢_:>_    : (Δ : DepCtx Σ m n) → TmExpr Σ (m + n) → TyExpr Σ (m + n) → Judgment Σ Γ n Tm
  _⊢_==_    : (Δ : DepCtx Σ m n) → TyExpr Σ (m + n) → TyExpr Σ (m + n) → Judgment Σ Γ n Ty=
  _⊢_==_:>_ : (Δ : DepCtx Σ m n) → TmExpr Σ (m + n) → TmExpr Σ (m + n) → TyExpr Σ (m + n)
            → Judgment Σ Γ n Tm=

{-
A derivation rule consists of a partial function taking a tuple of judgments (of the correct
arities) and returning another judgment. Moreover, a derivation rule is extendable to any other
signature the original signature maps to.

The type [DerivationRulePremises Σ Γ args] represents tuples of judgments of arities [args] (and in
signature [Σ] and with ambient context [Γ])

The type [DerivationRule Σ ar n] represents derivation rules in signature [Σ], of arity [ar] and in
scope [n]. It lives in [Set₁] because it quantifies over arbitrary signatures that [Σ] maps into.
-}

data DerivationRulePremises (Σ : Signature) {n : ℕ} (Γ : Ctx Σ n) : JudgmentArityArgs → Set where
  [] : DerivationRulePremises Σ Γ []
  _,_ : {m : ℕ} {k : JudgmentSort} {args : JudgmentArityArgs}
      → DerivationRulePremises Σ Γ args
      → Judgment Σ Γ m k
      → DerivationRulePremises Σ Γ (args , (m , k))

record DerivationRule (Σ : Signature) (ar : JudgmentArity) : Set₁ where
  field
    rule : {Σ' : Signature} {n : ℕ} → (Σ →Sig Σ') n → (Γ : Ctx Σ' n)
         → DerivationRulePremises Σ' Γ (args ar) → Partial (Judgment Σ' Γ 0 (sort ar))
open DerivationRule public

{- A derivability structure consists of a bunch of derivation rules, indexed by their arities -}

data Tag : Set where
  S T C Eq : Tag

record DerivabilityStructure (Σ : Signature) : Set₁ where
  field
    Rules : Tag → JudgmentArity → Set
    derivationRule : {t : Tag} {ar : JudgmentArity} (r : Rules t ar) → DerivationRule Σ ar
open DerivabilityStructure public

{- We can move the local context to the end of the ambient context -}

module _ {Σ : Signature} {m : ℕ} {Γ : Ctx Σ m} where

  Γ+ : {l : ℕ} (Δ : DepCtx Σ m l) → Ctx Σ (m + l)
  Γ+ ◇ = Γ
  Γ+ (Δ , A) = (Γ+ Δ , A)

  exchangeCtx : {n : ℕ} {k : JudgmentSort} → Judgment Σ Γ n k → Ctx Σ (m + n)
  exchangeCtx (Δ ⊢ A)           = Γ+ Δ
  exchangeCtx (Δ ⊢ u :> A)      = Γ+ Δ
  exchangeCtx (Δ ⊢ A == B)      = Γ+ Δ
  exchangeCtx (Δ ⊢ u == v :> A) = Γ+ Δ

  exchange : {n : ℕ} {k : JudgmentSort} → (j : Judgment Σ Γ n k) → Judgment Σ (exchangeCtx j) 0 k
  exchange (Δ ⊢ A)           = ◇ ⊢ A
  exchange (Δ ⊢ u :> A)      = ◇ ⊢ u :> A
  exchange (Δ ⊢ A == B)      = ◇ ⊢ A == B
  exchange (Δ ⊢ u == v :> A) = ◇ ⊢ u == v :> A

{-
A judgment can be derivable in one different way:
- if it has a trivial local context, then it should be obtained by applying a rule [r] from the
  derivability structure to a list of judgments [js] which are all derivable [js-der] and for which
  the rule is defined [def].

The type [DerivableArgs E js] represents the fact that all of the judgments in [js] are derivables.
The type [Derivable E j] represents the fact that the judgment [j] is derivable.
-}

data Derivable {Σ : Signature} (E : DerivabilityStructure Σ)
     : {m : ℕ} {Γ : Ctx Σ m} {k : JudgmentSort} → Judgment Σ Γ 0 k → Prop

data DerivableArgs {Σ : Signature} (E : DerivabilityStructure Σ) {m : ℕ} {Γ : Ctx Σ m}
     : {ar : JudgmentArityArgs} → DerivationRulePremises Σ Γ ar → Prop where
  []  : DerivableArgs E []
  _,_ : {n : ℕ} {k : JudgmentSort} {j : Judgment Σ Γ n k}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (exchange j)
        → DerivableArgs E (js , j)

data Derivable {Σ} E where
  apr : (t : Tag) {ar : JudgmentArity} (r : Rules E t ar) {m : ℕ} {Γ : Ctx Σ m}
        {js : DerivationRulePremises Σ Γ (args ar)}
        (js-der : DerivableArgs E js) {{def : isDefined (rule (derivationRule E r) idSig Γ js)}}
          → Derivable E (rule (derivationRule E r) idSig Γ js $ def)

{- Special cases of [_,_], used to make Agda not blow up -}

_,0Ty_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {A : TyExpr Σ m}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (◇ ⊢ A)
        → DerivableArgs E (js , ◇ ⊢ A)
djs ,0Ty dj = djs , dj

_,0Ty=_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {A B : _}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (◇ ⊢ A == B)
        → DerivableArgs E (js , ◇ ⊢ A == B)
djs ,0Ty= dj = djs , dj

_,0Tm_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {u : _} {A : _}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (◇ ⊢ u :> A)
        → DerivableArgs E (js , ◇ ⊢ u :> A)
djs ,0Tm dj = djs , dj

_,0Tm=_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {u v : _} {A : _}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (◇ ⊢ u == v :> A)
        → DerivableArgs E (js , ◇ ⊢ u == v :> A)
djs ,0Tm= dj = djs , dj

_,1Ty_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {A} {B}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (exchange ((◇ , A) ⊢ B))
        → DerivableArgs E (js , (◇ , A) ⊢ B)
djs ,1Ty dj = djs , dj

_,1Ty=_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {A} {B C}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (exchange ((◇ , A) ⊢ B == C))
        → DerivableArgs E (js , (◇ , A) ⊢ B == C)
djs ,1Ty= dj = djs , dj

_,1Tm_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {u : _} {A : _} {B : _}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (exchange ((◇ , B) ⊢ u :> A))
        → DerivableArgs E (js , (◇ , B) ⊢ u :> A)
djs ,1Tm dj = djs , dj

_,1Tm=_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {u v : _} {A : _} {B : _}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (exchange ((◇ , B) ⊢ u == v :> A))
        → DerivableArgs E (js , (◇ , B) ⊢ u == v :> A)
djs ,1Tm= dj = djs , dj

_,2Tm_ : ∀ {Σ} {E} {m} {Γ : Ctx Σ m} {u : _} {A : _} {B : _} {C : _}
        {ar : JudgmentArityArgs} {js : DerivationRulePremises Σ Γ ar}
        → DerivableArgs E js
        → Derivable E (exchange ((◇ , B , C) ⊢ u :> A))
        → DerivableArgs E (js , (◇ , B , C) ⊢ u :> A)
djs ,2Tm dj = djs , dj

infixl 4 _,0Ty_ _,0Ty=_ _,0Tm_ _,0Tm=_
         _,1Ty_ _,1Ty=_ _,1Tm_ _,1Tm=_
                        _,2Tm_

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


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

module Path where

open import Cubical.Foundations.Everything
  using ( _≡_
        ; sym
        ; refl
        ; subst
        ; transport
        ; Path
        ; PathP
        ; I
        ; i0
        ; i1
        ; funExt
        ; cong
        ; toPathP
        ; cong₂
        ; ~_
        ; _∧_
        ; _∨_
        ; hcomp
        ; transp
        ; J
        )
  renaming (_∙_ to _;_)
  public

open import Data.Empty using (¬_)
open import Level

infix 4 _≢_
_≢_ : {A : Type a} → A → A → Type a
x ≢ y = ¬ (x ≡ y)

infix 4 PathP-syntax
PathP-syntax = PathP

syntax PathP-syntax (λ i → Ty) lhs rhs = lhs ≡[ i ≔ Ty ]≡ rhs

ext: agda

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

-- ## Coercions
--
-- The overloading system implemented in this module is based on
-- **coercions**. A coercion is simply a function converting a type into
-- another. In object-oriented parliance, a coercion embodies an *is-a*
-- relationship.  The two types involved in a coercions are called `Source` and
-- `Target` respectively, and the coercion itself is a function `Source →
-- Target`.
--
-- Coercions are implemented as terms of type `Coercion`, which is a record
-- parameterized over the `Source` and `Target` types, with a single field for
-- the actual coercion function.  Of course, the type `Coercion X Y` is
-- isomorphic to `X → Y`, but using a record prevents possible ambiguities when
-- using coercions as implicit parameters, and potentially makes instance
-- resolution faster.
--
-- The typical scenario where coercions are used is when defining a subtype
-- relationships between types.  Although Agda has no built-in support for
-- subtypes, it is possible to achieve a reasonable level of syntactical
-- convenience with the help of some boilerplace code that specifies the
-- subtyping relation explicitly.  See `category.graph.core` for a detailed
-- example.
--
-- This module also contains some functions to help reduce the amount of
-- boilerplate needed for defining all the coercions necessary for a given type.
-- See `coerce-self` and `coerce-parent` below.
--
-- ## Methods
--
-- The strategy employed by this library to implement overloading goes as
-- follows.  Every type (denoted by `Target` in the following) defines a set of
-- "methods" that constitute its interface, and are inherited by every subtype
-- of `Target`.  Methods are divided into 2 groups:
--
-- - **static methods** are functions that take an argument `X` of a type
-- convertible to `Target`. The typical example of a static method is an
-- explicit coercion function, like `∣_∣` below, which returns the "underlying
-- set" of `X`.  Another example of static method is the `total` function for
-- graphs (see `category.graph.core`).
--
-- - **instance methods** are functions that work without requiring an explicit
-- parameter of type `Target`.  A typical example of instance method is
-- composition in a category (`_∘_`): there's no need to pass the category
-- itself when composing two morphisms.  In order to use instance methods, they
-- have to be enabled explicitly for each instance for which they are used.
-- Every type defines a special module (whose name is by convention always
-- `as-target`, where `target` is replaced with the actual lowercase name of
-- type) which allows instance methods to be enabled.  For example, to use the
-- composition operator for morphisms of a category `C`, one can write:
--
--    open as-category C
--
-- The `as-target` module itself behaves like a *static* method, so it can be
-- used to enable instance methods for any superclass of a given instance.
-- Furthermore, enabling instance methods for `Target` enables instance methods
-- for all superclasses of it in its principal inheritance path (see
-- "Inheritance Model" below).
--
-- ## Implementation
--
-- The implementation of static methods is relatively straightforward.  A static
-- method is defined as a function taking a coercion to `Target` as an instance
-- argument, and uses the coercion to convert its argument to the correct type.
--
-- As for instance methods, they are implemented as functions that take a record
-- with the full interface of `Target` (called **instance record** below) as an
-- implicit argument (see "Alternative Notations" below for details), and just
-- return the appropriate field.  This can be accomplished very easily using
-- Agda's module system.
--
-- The `as-target` module, used to enable instance methods, is defined as a
-- static method, and works simply by putting the record above into scope.
--
-- ## Alternative Notations
--
-- Some types have an interface which supports alternative notations.  For
-- example, monoids have a "default" notation (`unit` and `_*_`), and an
-- additive notation (`zero` and `_+_`).
--
-- To implement multiple notations, a `Styled` record is used as the implicit
-- parameter for instance methods.  The `Styled` record is parameterized over a
-- `style` parameter (normally `default`), and contains the interface record as
-- its only field.
--
-- The `Styled` record thus serves two purposes:
--
-- - It prevents ambiguities in the resolution of instance arguments: if an
-- interface record is in scope for reasons unrelated to the overloading system,
-- then it will not be accidentally used as the argument of an instance methods,
-- as it's not wrapped in a `Styled` record.
--
-- - It allows instance methods to specify an alternative style parameter for
-- the record in which the interface record is wrapped.  Thus, multiple
-- `as-target` module can be defined, one per supported style, that put the
-- interface record in scope wrapped in the appropriate `Styled` record.  The
-- `styled` function can be used to wrap an interface record using a given
-- style.
--
-- ## Inheritance Model
--
-- Subtyping relations can form an arbitrary directed graph, with a
-- distinguished spanning forest, whose edges we call *principal*.
--
-- Coercions are defined for every pair of connected nodes in the full graph.
-- Exactly one coercion per pair should be defined, regardless of the number of
-- paths that connect it.  Static methods are inherited automatically through
-- paths in the full DAG, since the existence of a coercion is enough for static
-- methods to propagate.
--
-- The principal subgraph is used for inheritance of instance methods.  Namely,
-- the `as-target` record enables all instance methods for the ancestors of
-- `Target` in the principal subgraph.  This is accomplished by simply
-- re-exporting the `as-target` module for the immediate parent of
-- `Target`. Extra edges coming out of `Target` can optionally be added as well
-- for convenience.

open import level
open import overloading.bundle

record Coercion {i}{j}(Source : Set i)(Target : Set j) : Set (i ⊔ j) where
  constructor coercion
  field
    coerce : Source → Target
open Coercion public

data Style : Set where default : Style

record Styled {i}(style : Style)(X : Set i) : Set i where
  field value : X

styled : ∀ {i}{X : Set i} → (s : Style) → X → Styled s X
styled s x = record { value = x }

-- Trivial coercion: any type can be coerced into itself.
coerce-self : ∀ {i} (X : Set i) → Coercion X X
coerce-self {i} _ = record
  { coerce = λ x → x }

-- Transport a coercion to a `Bundle` subtype.  See `overloading.bundle` for
-- more details on bundles.
coerce-parent : ∀ {i j k}
                {X : Set i}
                {Y : Set j}
              → ⦃ c : Coercion X Y ⦄
              → {Struct : X → Set k}
              → Coercion (Bundle Struct) Y
coerce-parent ⦃ c ⦄ = record
  { coerce = λ x → coerce c (Bundle.parent x) }

instance
  set-is-set : ∀ {i} → Coercion (Set i) (Set i)
  set-is-set {i} = coerce-self _

∣_∣ : ∀ {i j}{Source : Set i} ⦃ o : Coercion Source (Set j) ⦄
    → Source → Set j
∣_∣ ⦃ c ⦄ = coerce c

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
module Issue606 where

infixr 1 _,_

record _×_ (A B : Set) : Set where
  constructor _,_
  field fst : A
        snd : B

postulate A B C : Set

test : A × (B × C)
test = {!!} , {!!}
-- refining the second hole should give "? , ?"  (no enclosing parens!)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --no-positivity-check #-}

module Section7 where

open import Section6 public

-- 7. Correspondence between proof trees and terms
-- ===============================================
--
-- We define a function that translates the proof trees to the corresponding untyped terms nad
-- likewise for the substitutions, we write `M ⁻` and `γ ⁻ˢ` for these operations.  The definitions
-- are:

mutual
  _⁻ : ∀ {Γ A} → Γ ⊢ A → 𝕋
  (ν x i) ⁻ = ν x
  (ƛ x M) ⁻ = ƛ x (M ⁻)
  (M ∙ N) ⁻ = (M ⁻) ∙ (N ⁻)
  (M ▶ γ) ⁻ = (M ⁻) ▶ (γ ⁻ˢ)

  _⁻ˢ : ∀ {Δ Γ} → Δ ⋙ Γ → 𝕊
  π⟨ c ⟩ ⁻ˢ        = []
  (γ ● γ′) ⁻ˢ      = (γ ⁻ˢ) ● (γ′ ⁻ˢ)
  [ γ , x ≔ M ] ⁻ˢ = [ γ ⁻ˢ , x ≔ M ⁻ ]

-- It is easy to prove that the translation of a proof tree is well-typed:

-- Lemma 12.
mutual
  lem₁₂ : ∀ {Γ A} → (M : Γ ⊢ A) → Γ ⊢ M ⁻ ∷ A
  lem₁₂ (ν x i) = ν x i
  lem₁₂ (ƛ x M) = ƛ x (lem₁₂ M)
  lem₁₂ (M ∙ N) = lem₁₂ M ∙ lem₁₂ N
  lem₁₂ (M ▶ γ) = lem₁₂ M ▶ lem₁₂ₛ γ

  lem₁₂ₛ : ∀ {Γ Γ′} → (γ : Γ′ ⋙ Γ) → Γ′ ⋙ γ ⁻ˢ ∷ Γ
  lem₁₂ₛ π⟨ c ⟩        = ↑⟨ c ⟩ refl⋙∷
  lem₁₂ₛ (γ ● γ′)      = lem₁₂ₛ γ ● lem₁₂ₛ γ′
  lem₁₂ₛ [ γ , x ≔ M ] = [ lem₁₂ₛ γ , x ≔ lem₁₂ M ]

-- In general, we may have `M ⁻ ≡ N ⁻` but `M` different from `N`.  Take for example
-- `(λ(y : B ⊃ B).z) ∙ λ(x : B).x : [ z : A ] ⊢ A` and `(λ(y : C ⊃ C).z ∙ λ(x : C).x : [ z : A ] ⊢ A`
-- which are both
-- translated into `(λ y.z) ∙ λ x.x`.  This shows that a given term can be decorated into different
-- proof trees.
--
-- We define a relation between terms and their possible decorations (and likewise for the
-- substitutions) as an inductively defined set.  (…)
--
-- The introduction rules are:  (…)

mutual
  infix 3 _𝒟_
  data _𝒟_ : ∀ {Γ A} → 𝕋 → Γ ⊢ A → Set where
    ν    : ∀ {Γ A} →
             (x : Name) (i : Γ ∋ x ∷ A) →
             ν x 𝒟 ν x i
    _∙_  : ∀ {Γ A B t₁ t₂} {M : Γ ⊢ A ⊃ B} {N : Γ ⊢ A} →
             t₁ 𝒟 M → t₂ 𝒟 N →
             t₁ ∙ t₂ 𝒟 M ∙ N
    π⟨_⟩ : ∀ {Γ Δ A t} {M : Δ ⊢ A} →
             (c : Γ ⊇ Δ) → t 𝒟 M →
             t 𝒟 M ▶ π⟨ c ⟩
    _▶_  : ∀ {Γ Δ A s t} {M : Δ ⊢ A} {γ : Γ ⋙ Δ} →
             t 𝒟 M → s 𝒟ₛ γ →
             t ▶ s 𝒟 M ▶ γ
    ƛ    : ∀ {Γ A B t} →
             (x : Name) {{_ : T (fresh x Γ)}} {M : [ Γ , x ∷ A ] ⊢ B} → t 𝒟 M →
             ƛ x t 𝒟 ƛ x M

  infix 3 _𝒟ₛ_
  data _𝒟ₛ_ : ∀ {Γ Δ} → 𝕊 → Γ ⋙ Δ → Set where
    π⟨_⟩    : ∀ {Γ Δ} →
                (c : Γ ⊇ Δ) →
                [] 𝒟ₛ π⟨ c ⟩
    [_,_≔_] : ∀ {Γ Δ A s t} {γ : Δ ⋙ Γ} {M : Δ ⊢ A} →
                s 𝒟ₛ γ → (x : Name) {{_ : T (fresh x Γ)}} → t 𝒟 M →
                [ s , x ≔ t ] 𝒟ₛ [ γ , x ≔ M ]
    ↓⟨_⟩𝒟ₛ  : ∀ {Γ Δ Θ s} {γ : Θ ⋙ Γ} →
                (c : Γ ⊇ Δ) → s 𝒟ₛ γ →
                s 𝒟ₛ ↓⟨ c ⟩ γ
    ↑⟨_⟩𝒟ₛ  : ∀ {Γ Δ Θ s} {γ : Γ ⋙ Δ} →
                (c : Θ ⊇ Γ) → s 𝒟ₛ γ →
                s 𝒟ₛ ↑⟨ c ⟩ γ
    _●_     : ∀ {Γ Δ Θ s₁ s₂} {γ₂ : Γ ⋙ Δ} {γ₁ : Θ ⋙ Γ} →
                s₂ 𝒟ₛ γ₂ → s₁ 𝒟ₛ γ₁ →
                s₂ ● s₁ 𝒟ₛ γ₂ ● γ₁

-- It is straightforward to prove Lemma 13
-- mutually with a corresponding lemma for substitutions.

-- Lemma 13.
mutual
  lem₁₃ : ∀ {Γ A} → (M : Γ ⊢ A) → M ⁻ 𝒟 M
  lem₁₃ (ν x i) = ν x i
  lem₁₃ (ƛ x M) = ƛ x (lem₁₃ M)
  lem₁₃ (M ∙ N) = lem₁₃ M ∙ lem₁₃ N
  lem₁₃ (M ▶ γ) = lem₁₃ M ▶ lem₁₃ₛ γ

  lem₁₃ₛ : ∀ {Γ Γ′} → (γ : Γ′ ⋙ Γ) → γ ⁻ˢ 𝒟ₛ γ
  lem₁₃ₛ π⟨ c ⟩        = π⟨ c ⟩
  lem₁₃ₛ (γ ● γ′)      = lem₁₃ₛ γ ● lem₁₃ₛ γ′
  lem₁₃ₛ [ γ , x ≔ M ] = [ lem₁₃ₛ γ , x ≔ lem₁₃ M ]

-- Using the discussion in Section 3.3 on how to define the monotonicity and projection
-- rules with `π⟨_⟩` we can find a proof tree that corresponds to a well-typed term:

-- Lemma 14.
postulate
  lem₁₄ : ∀ {Γ A t} → Γ ⊢ t ∷ A → Σ (Γ ⊢ A) (λ M → M ⁻ ≡ t)

-- As a direct consequence of this lemma and Lemma 13 we know that every well-typed term
-- has a decoration.

-- Lemma 15.
lem₁₅ : ∀ {Γ A t} → Γ ⊢ t ∷ A → Σ (Γ ⊢ A) (λ M → t 𝒟 M)
lem₁₅ D with lem₁₄ D
…           | (M , refl) = M , lem₁₃ M

-- As a consequence of this lemma we can now define the semantics of a well-typed term in
-- a Kripke model as the semantics of the decorated term.  In the remaining text, however, we
-- study only the correspondence between terms and proof trees since the translation to the
-- semantics is direct.
--
-- TODO: What to do about the above paragraph?
--
-- As we mentioned above a well-typed term may be decorated to several proof trees.  We
-- can however prove that if two proof trees are in η-normal form and they are decorations of
-- the same term, then the two proof trees are convertible.  We prove Lemma 16
-- together with two corresponding lemmas for proof trees in applicative normal form:

-- Lemma 16.
mutual
  postulate
    lem₁₆ : ∀ {Γ A t} {M M′ : Γ ⊢ A} {{_ : enf M}} {{_ : enf M′}} →
              t 𝒟 M → t 𝒟 M′ →
              M ≡ M′

  postulate
    lem₁₆′ : ∀ {Γ A A′ t} {M : Γ ⊢ A} {N : Γ ⊢ A′} {{_ : anf M}} {{_ : anf N}} →
               t 𝒟 M → t 𝒟 N →
               A ≡ A′

-- TODO: Uh oh. Heterogeneous equality?
-- postulate
--   lem₁₆″ : ∀ {Γ A A′ t} {M : Γ ⊢ A} {M′ : Γ ⊢ A′} {{_ : anf M}} {{_ : anf M′}} →
--              t 𝒟 M → t 𝒟 M′ →
--              M ≡ M′

  postulate
    lem₁₆″ : ∀ {Γ A t} {M M′ : Γ ⊢ A} {{_ : anf M}} {{_ : anf M′}} →
               t 𝒟 M → t 𝒟 M′ →
               M ≡ M′

-- As a consequence we get that if `nf M ⁻` and `nf N ⁻` are the same, then `M ≅ N`.

-- Corollary 2.
postulate
  cor₂ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → nf M ⁻ ≡ nf M′ ⁻ → M ≅ M′

-- Proof: By Lemma 16 and Theorem 7 we get `nf N ≡ nf M` and by Theorem 5 we get `M ≅ N`.

-- 7.1. Reduction
-- --------------
--
-- We mutually inductively define when a term is in weak head normal form (abbreviated
-- `whnf`) and in weak head applicative normal form (abbreviated `whanf`) by:

mutual
  data whnf : 𝕋 → Set where
    ƛ : ∀ {t} →
          (x : Name) → whnf t →
          whnf (ƛ x t)
    α : ∀ {t} → whanf t →
          whnf t

  data whanf : 𝕋 → Set where
    ν   : (x : Name) →
          whanf (ν x)
    _∙_ : ∀ {t u} →
          whanf t → whnf u →
          whanf (t ∙ u)

-- We inductively define a deterministic untyped one-step reduction on terms and
-- substitutions:  (…)

mutual
  infix 3 _⟶_
  data _⟶_ : 𝕋 → 𝕋 → Set where
    red₁ : ∀ {a s t x} →
             (ƛ x t ▶ s) ∙ a ⟶ t ▶ [ s , x ≔ a ]
    red₂ : ∀ {t t₁ t₂} →
             t₁ ⟶ t₂ →
             t₁ ∙ t ⟶ t₂ ∙ t
    red₃ : ∀ {s t x} →
             ν x ▶ [ s , x ≔ t ] ⟶ t
    red₄ : ∀ {s t x y} {{_ : x ≢ y}} →
             ν x ▶ [ s , y ≔ t ] ⟶ ν x ▶ s
    red₅ : ∀ {x} →
             ν x ▶ [] ⟶ ν x
    red₆ : ∀ {s₁ s₂ x} →
             s₁ ⟶ₛ s₂ →
             x ▶ s₁ ⟶ x ▶ s₂
    red₇ : ∀ {s t₁ t₂} →
             (t₁ ∙ t₂) ▶ s ⟶ (t₁ ▶ s) ∙ (t₂ ▶ s)
    red₈ : ∀ {s₁ s₂ t} →
             (t ▶ s₁) ▶ s₂ ⟶ t ▶ (s₁ ● s₂)

  infix 3 _⟶ₛ_
  data _⟶ₛ_ : 𝕊 → 𝕊 → Set where
    red₁ₛ : ∀ {s₀ s₁ t x} →
              [ s₀ , x ≔ t ] ● s₁ ⟶ₛ [ s₀ ● s₁ , x ≔ t ▶ s₁ ]
    red₂ₛ : ∀ {s₁ s₂ s₃} →
              (s₁ ● s₂) ● s₃ ⟶ₛ s₁ ● (s₂ ● s₃)
    red₃ₛ : ∀ {s} →
              [] ● s ⟶ₛ s

-- The untyped evaluation to `whnf`, `_⟹_`, is inductively defined by:

infix 3 _⟹_
data _⟹_ : 𝕋 → 𝕋 → Set where
  eval₁ : ∀ {t} {{_ : whnf t}} →
            t ⟹ t
  eval₂ : ∀ {t₁ t₂ t₃} →
            t₁ ⟶ t₂ → t₂ ⟹ t₃ →
            t₁ ⟹ t₃

-- It is easy to see that this relation is deterministic.
--
-- TODO: What to do about the above paragraph?
--
-- In order to define a deterministic reduction that gives a term on long η-normal form
-- we need to use its type.  We define this typed reduction, `_⊢_↓_∷_`, simultaneously with `_⊢_↓ₛ_∷_` which
-- η-expands the arguments in an application on `whnf`:

mutual
  infix 3 _⊢_↓_∷_
  data _⊢_↓_∷_ : 𝒞 → 𝕋 → 𝕋 → 𝒯 → Set where
    red₁ : ∀ {Γ t₀ t₂} →
             Σ 𝕋 (λ t₁ → t₀ ⟹ t₁ × Γ ⊢ t₁ ↓ₛ t₂ ∷ •) →
             Γ ⊢ t₀ ↓ t₂ ∷ •
    red₂ : ∀ {Γ A B t₁ t₂} →
             let z , φ = gensym Γ in
             let instance _ = φ in
             [ Γ , z ∷ A ] ⊢ t₁ ∙ ν z ↓ t₂ ∷ B →
             Γ ⊢ t₁ ↓ ƛ z t₂ ∷ A ⊃ B

  infix 3 _⊢_↓ₛ_∷_
  data _⊢_↓ₛ_∷_ : 𝒞 → 𝕋 → 𝕋 → 𝒯 → Set where
    red₁ₛ : ∀ {Γ A x} →
              Γ ∋ x ∷ A →
              Γ ⊢ ν x ↓ₛ ν x ∷ A
    red₂ₛ : ∀ {Γ B t₁ t₂ t₁′ t₂′} →
              Σ 𝒯 (λ A → Γ ⊢ t₁ ↓ₛ t₁′ ∷ A ⊃ B × Γ ⊢ t₂ ↓ t₂′ ∷ A) →
              Γ ⊢ t₁ ∙ t₂ ↓ₛ t₁′ ∙ t₂′ ∷ B

-- Finally we define `Γ ⊢ t ⇓ t′ ∷ A` to hold if `Γ ⊢ t [] ↓ t′ ∷ A`.

_⊢_⇓_∷_ : 𝒞 → 𝕋 → 𝕋 → 𝒯 → Set
Γ ⊢ t ⇓ t′ ∷ A = Γ ⊢ t ▶ [] ↓ t′ ∷ A

-- 7.2. Equivalence between proof trees and terms
-- ----------------------------------------------
--
-- We can prove that if `M : Γ ⊢ A`, then `Γ ⊢ M ⁻ ⇓ nf M ⁻ ∷ A`.  This we do by defining a
-- Kripke logical relation, `_ℛ_`.  (…)
--
-- When `f : Γ ⊩ •` we intuitively have that `t ℛ f` holds if `Γ ⊢ t ↓ f ⁻`.
--
-- When `f : Γ ⊩ A ⊃ B`, then `t ℛ f` holds if for all `t′` and `a : Γ ⊩ A` such that `t′ ℛ a`, we
-- have that `t ∙ t′ ℛ f ⟦∙⟧ a`.

infix 3 _ℛ_
data _ℛ_ : ∀ {Γ A} → 𝕋 → Γ ⊩ A → Set where
  𝓇• : ∀ {Δ} →
         (t : 𝕋) (f : Δ ⊩ •) →
         (∀ {Γ} →
            (c : Γ ⊇ Δ) (t′ : 𝕋) → t′ 𝒟 f ⟦g⟧⟨ c ⟩ →
            Γ ⊢ t ↓ t′ ∷ •) →
         t ℛ f
  𝓇⊃ : ∀ {Δ A B} →
         (t : 𝕋) (f : Δ ⊩ A ⊃ B) →
         (∀ {Γ} →
           (c : Γ ⊇ Δ) (a : Γ ⊩ A) (t′ : 𝕋) → Γ ⊢ t′ ∷ A → t′ ℛ a →
           t ∙ t′ ℛ f ⟦∙⟧⟨ c ⟩ a) →
         t ℛ f

-- For the substitutions we define correspondingly:

infix 3 _ℛₛ_
data _ℛₛ_ : ∀ {Γ Δ} → 𝕊 → Γ ⊩⋆ Δ → Set where
  𝓇ₛ[] : ∀ {Δ s} →
           Δ ⋙ s ∷ [] →
           s ℛₛ ([] {w = Δ})
  -- NOTE: Mistake in paper?  Changed `v : Δ ⊩ A` to `a : Γ ⊩ A`.
  rₛ≔  : ∀ {Γ Δ A s x} {{_ : T (fresh x Γ)}} {{_ : T (fresh x Δ)}} →
           Δ ⋙ s ∷ [ Γ , x ∷ A ] → (ρ : Γ ⊩⋆ Δ) (a : Γ ⊩ A) → s ℛₛ ρ → ν x ▶ s ℛ a →
           s ℛₛ [ ρ , x ≔ a ]

-- The following lemmas are straightforward to prove:

postulate
  aux₇₂₁ : ∀ {Γ A t₁ t₂} →
             (a : Γ ⊩ A) → t₁ ℛ a → t₂ ⟶ t₁ →
             t₂ ℛ a

postulate
  aux₇₂₂ : ∀ {Γ Δ s₁ s₂} →
             (ρ : Γ ⊩⋆ Δ) → Δ ⋙ s₁ ∷ Γ → s₁ ⟶ₛ s₂ → s₂ ℛₛ ρ →
             s₁ ℛₛ ρ

-- NOTE: Mistake in paper?  Changed `Occur(x, A, Γ)` to `Δ ∋ x ∷ A`.
postulate
  aux₇₂₃ : ∀ {Γ Δ A s x} →
             (ρ : Γ ⊩⋆ Δ) (i : Δ ∋ x ∷ A) → Δ ⋙ s ∷ Γ →
             ν x ▶ s ℛ lookup ρ i

postulate
  aux₇₂₄⟨_⟩ : ∀ {Γ Δ A t} →
                (c : Γ ⊇ Δ) (a : Δ ⊩ A) → t ℛ a →
                t ℛ ↑⟨ c ⟩ a

-- NOTE: Mistake in paper?  Changed `ρ ∈ Γ ⊩ Δ` to `ρ : Δ ⊩⋆ Γ`.
postulate
  aux₇₂₅⟨_⟩ : ∀ {Γ Δ Θ s} →
                (c : Θ ⊇ Δ) → Δ ⋙ s ∷ Γ → (ρ : Δ ⊩⋆ Γ) → s ℛₛ ρ →
                s ℛₛ ↑⟨ c ⟩ ρ

-- NOTE: Mistake in paper?  Changed `ρ ∈ Γ ⊩ Δ` to `ρ : Δ ⊩⋆ Γ`.
postulate
  aux₇₂₆⟨_⟩ : ∀ {Γ Δ Θ s} →
                (c : Γ ⊇ Θ) → Δ ⋙ s ∷ Γ → (ρ : Δ ⊩⋆ Γ) → s ℛₛ ρ →
                s ℛₛ ↓⟨ c ⟩ ρ

postulate
  aux₇₂₇ : ∀ {Γ Δ A s t x} →
             Γ ⊢ t ∷ A → Γ ⋙ s ∷ Δ → (ρ : Γ ⊩⋆ Δ) → s ℛₛ ρ →
             [ s , x ≔ t ] ℛₛ ρ

-- Using these lemmas we can prove by mutual induction on the proof tree of terms and
-- substitutions that:

-- NOTE: Mistake in paper?  Changed `ρ ∈ Γ ⊩ Δ` to `ρ : Δ ⊩⋆ Γ`.
postulate
  aux₇₂₈ : ∀ {Γ Δ A s t} →
             (M : Γ ⊢ A) (ρ : Δ ⊩⋆ Γ) → Δ ⋙ s ∷ Γ → t 𝒟 M → s ℛₛ ρ →
             t ▶ s ℛ ⟦ M ⟧ ρ

postulate
  aux₇₂₉ : ∀ {Γ Δ Θ s₁ s₂} →
             (γ : Γ ⋙ Θ) (ρ : Δ ⊩⋆ Γ) → Δ ⋙ s₂ ∷ Γ → s₁ 𝒟ₛ γ → s₂ ℛₛ ρ →
             s₂ ● s₁ ℛₛ ⟦ γ ⟧ₛ ρ

-- We also show, intuitively, that if `t ℛ a`, `a : Γ ⊩ A`, then `Γ ⊢ t ↓ reify a ⁻ ∷ A`
-- together with a corresponding lemma for `val`:

-- Lemma 17.
mutual
  postulate
    lem₁₇ : ∀ {Γ A t₀ t₁} →
              Γ ⊢ t₀ ∷ A → (a : Γ ⊩ A) → t₀ ℛ a → t₁ 𝒟 reify a →
              Γ ⊢ t₀ ↓ t₁ ∷ A

  -- NOTE: Mistake in paper?  Changed `t ℛ val(f)` to `t₀ ℛ val f`.
  postulate
    aux₇₂₁₀ : ∀ {Γ A t₀} →
                Γ ⊢ t₀ ∷ A → whanf t₀ →
                (f : ∀ {Δ} → (c : Δ ⊇ Γ) → Δ ⊢ A) →
                (∀ {Δ} → (c : Δ ⊇ Γ) → Δ ⊢ t₀ ↓ₛ f c ⁻ ∷ A) →
                t₀ ℛ val f

-- The proof that the translation of proof trees reduces to the translation of its normal form
-- follows directly:

-- Theorem 8.
postulate
  thm₈ : ∀ {Γ A t} →
           (M : Γ ⊢ A) → t 𝒟 M →
           Γ ⊢ t ⇓ nf M ⁻ ∷ A

-- As a consequence we get that if two proof trees are decorations of the same term, then they
-- are convertible with each other:

-- Corollary 3.
postulate
  cor₃ : ∀ {Γ A t} →
           (M N : Γ ⊢ A) → t 𝒟 M → t 𝒟 N →
           M ≅ N

-- Proof: By Theorem 8 we get that `Γ ⊢ t ⇓ nf M ⁻ ∷ A` and `Γ ⊢ t ⇓ nf N ⁻ ∷ A`.  Since
-- the reduction is deterministic we get `nf M ⁻ ≡ nf N ⁻` and by Corollary 2 we get that
-- `M ≅ N`.

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Support.Equivalence

module Categories.Object.Indexed {o ℓ e c q} (C : Category o ℓ e) (B : Setoid c q) where

open import Categories.Support.SetoidFunctions
open Category C
open _⟶_ public using () renaming (cong to cong₀; _⟨$⟩_ to _!_)

Objoid = set→setoid Obj

Dust = B ⟶ Objoid

dust-setoid = B ⇨ Objoid

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2018-10-16, erased lambda-arguments

applyErased : {@0 A B : Set} → (@0 A → B) → @0 A → B
applyErased f x = f x

test : {A : Set} → A → A
test x = applyErased (λ y → y) x

-- Expected error:
--
-- Variable y is declared erased, so it cannot be used here
-- when checking that the expression y has type _B_7


text:
module RandomAccessList.Standard.Numeral where

open import Data.List
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Unit using (⊤)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; trans; sym; inspect)
open PropEq.≡-Reasoning

data Digit : Set where
    zero : Digit
    one  : Digit

Binary : Set
Binary = List Digit

incr : Binary → Binary
incr []          = one  ∷ []
incr (zero ∷ xs) = one  ∷ xs
incr (one  ∷ xs) = zero ∷ incr xs

⟦_⟧ : Binary → ℕ
⟦ []        ⟧ = 0
⟦ zero ∷ xs ⟧ =     2 * ⟦ xs ⟧
⟦ one  ∷ xs ⟧ = 1 + 2 * ⟦ xs ⟧

*-0-absorb : (n m : ℕ) → n ≡ 0 → m * n ≡ 0
*-0-absorb n m p =
    begin
        m * n
    ≡⟨ cong (_*_ m) p ⟩
        m * 0
    ≡⟨ *-right-zero m ⟩
        0
    ∎

decr : (xs : Binary) → ⟦ xs ⟧ ≢ 0 → Binary
decr []          p = ⊥-elim (p refl)
decr (zero ∷ xs) p = one  ∷ decr xs (contraposition (*-0-absorb ⟦ xs ⟧ 2) p)
decr (one  ∷ xs) p = zero ∷ xs

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Prelude
open import core

module ground-decidable where
  -- every type is either ground or not
  ground-decidable : (τ : typ) → (τ ground) + ((τ ground) → ⊥)
  ground-decidable b = Inl GBase
  ground-decidable ⦇·⦈ = Inr (λ ())
  ground-decidable (b ==> b) = Inr (λ ())
  ground-decidable (b ==> ⦇·⦈) = Inr (λ ())
  ground-decidable (b ==> τ' ==> τ'') = Inr (λ ())
  ground-decidable (b ==> τ₁ ⊗ τ₂) = Inr (λ ())
  ground-decidable (⦇·⦈ ==> b) = Inr (λ ())
  ground-decidable (⦇·⦈ ==> ⦇·⦈) = Inl GHole
  ground-decidable (⦇·⦈ ==> τ' ==> τ'') = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ==> b) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ==> ⦇·⦈) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ==> τ' ==> τ'') = Inr (λ ())
  ground-decidable ((τ ⊗ τ₂) ==> τ₁) = Inr (λ ())
  ground-decidable (τ ⊗ b) = Inr (λ ())
  ground-decidable (b ⊗ ⦇·⦈) = Inr (λ ())
  ground-decidable (⦇·⦈ ⊗ ⦇·⦈) = Inl GProd
  ground-decidable (⦇·⦈ ==> τ₁ ⊗ τ₂) = Inr (λ ())
  ground-decidable ((τ ⊗ τ₁) ⊗ ⦇·⦈) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ⊗ ⦇·⦈) = Inr (λ ())
  ground-decidable ((τ ==> τ₂) ==> τ₁ ⊗ τ₃) = Inr (λ ())
  ground-decidable (τ ⊗ τ₁ ==> τ₂) = Inr (λ ())
  ground-decidable (τ ⊗ τ₁ ⊗ τ₂) = Inr (λ ())

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda