text:
------------------------------------------------------------------------
-- A small definition of a dependently typed language, using the
-- technique from McBride's "Outrageous but Meaningful Coincidences"
------------------------------------------------------------------------

-- Inlining saves a lot of memory. Test with +RTS -M100M
-- The inlining of zero and suc in raw-category at the end is the most
-- important.

{-# OPTIONS --type-in-type #-}

module _ where

open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma

------------------------------------------------------------------------
-- Prelude

data ⊥ : Set where

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

data Either (A B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

uncurry : {A : Set} {B : A → Set} {C : Σ A B → Set} →
          ((x : A) (y : B x) → C (x , y)) →
          ((p : Σ A B) → C p)
uncurry f p = f (fst p) (snd p)

infixr 2 _×_
_×_ : Set → Set → Set
_×_ A B = Σ A (λ _ → B)

------------------------------------------------------------------------
-- A universe

data U : Set

El : U → Set

data U where
  set   : U
  el    : Set → U
  sigma : (a : U) → (El a → U) → U
  pi    : (a : U) → (El a → U) → U

El set         = Set
El (el A)      = A
El (sigma a b) = Σ (El a) (λ x → El (b x))
El (pi a b)    = (x : El a) → El (b x)

-- Abbreviations.

fun : U → U → U
fun a b = pi a (λ _ → b)

times : U → U → U
times a b = sigma a (λ _ → b)

-- -- Example.

------------------------------------------------------------------------
-- Contexts

-- Contexts.

data Ctxt : Set

-- Types.

Ty : Ctxt → Set

-- Environments.

Env : Ctxt → Set

data Ctxt where
  empty : Ctxt
  snoc  : (G : Ctxt) → Ty G → Ctxt

Ty G = Env G → U

Env empty      = ⊤
Env (snoc G s) = Σ (Env G) (λ g → El (s g))

-- Variables (deBruijn indices).

Var : ∀ G → Ty G → Set
Var empty      t = ⊥
Var (snoc G s) t =
  Either ((λ g → s (fst g)) ≡ t)
         (Σ _ (λ u → (λ g → u (fst g)) ≡ t × Var G u))

zero : ∀ {G s} → Var (snoc G s) (λ g → s (fst g))
zero = left refl

suc : ∀ {G s t} → (x : Var G t) → Var (snoc G s) (λ g → t (fst g))
suc x = right (_ , refl , x)

-- A lookup function.

lookup : ∀ G (s : Ty G) → Var G s → (g : Env G) → El (s g)
lookup empty      _ absurd     _ = ⊥-elim absurd
lookup (snoc vs v) _ (left refl) g = snd g
lookup (snoc vs v) t (right (_ , refl , x))  g = lookup _ _ x (fst g)

------------------------------------------------------------------------
-- A language

-- Syntax for types.

data Type (G : Ctxt) (s : Ty G) : Set

-- Terms.

data Term (G : Ctxt) (s : Ty G) : Set

-- The semantics of a term.

eval : ∀ {G s} → Term G s → (g : Env G) → El (s g)

data Type G s where
  set''   : s ≡ (λ _ → set) → Type G s
  el''    : (x : Term G (λ _ → set)) →
            (λ g → el (eval {s = λ _ → set} x g)) ≡ s →
            Type G s
  sigma'' : {t : _} {u : _} →
            Type G t →
            Type (snoc G t) u →
            (λ g → sigma (t g) (λ v → u (g , v))) ≡ s →
            Type G s
  pi''    : {t : _} {u : _} →
            Type G t →
            Type (snoc G t) u →
            (λ g → pi (t g) (λ v → u (g , v))) ≡ s →
            Type G s

data Term G s where
  var   : Var G s → Term G s
  lam'' : {t : _} {u : _} →
          Term (snoc G t) (uncurry u) →
          (λ g → pi (t g) (λ v → u g v)) ≡ s →
          Term G s
  app'' : {t : _} {u : (g : Env G) → El (t g) → U} →
          Term G (λ g → pi (t g) (λ v → u g v)) →
          (t2 : Term G t) →
          (λ g → u g (eval t2 g)) ≡ s →
          Term G s

eval (var x)            g = lookup _ _ x g
eval (lam'' t refl)     g = λ v → eval t (g , v)
eval (app'' t1 t2 refl) g = eval t1 g (eval t2 g)

-- Abbreviations.

set' : {G : Ctxt} → Type G (λ _ → set)
set' = set'' refl

el' : {G : Ctxt}
      (x : Term G (λ _ → set)) →
      Type G (λ g → el (eval {G} {λ _ → set} x g))
el' x = el'' x refl

sigma' : {G : Ctxt} {t : Env G → U} {u : Env (snoc G t) → U} →
         Type G t →
         Type (snoc G t) u →
         Type G (λ g → sigma (t g) (λ v → u (g , v)))
sigma' s t = sigma'' s t refl

pi' : {G : _} {t : _} {u : _} →
      Type G t →
      Type (snoc G t) u →
      Type G (λ g → pi (t g) (λ v → u (g , v)))
pi' s t = pi'' s t refl

lam : {G : _} {t : _} {u : _} →
      Term (snoc G t) (uncurry u) →
      Term G (λ g → pi (t g) (λ v → u g v))
lam t = lam'' t refl

app : {G : _} {t : _} {u : (g : Env G) → El (t g) → U} →
      Term G (λ g → pi (t g) (λ v → u g v)) →
      (t2 : Term G t) →
      Term G (λ g → u g (eval t2 g))
app t1 t2 = app'' t1 t2 refl

-- Example.

raw-categoryU : U
raw-categoryU =
  sigma set (λ obj →
  sigma (fun (el obj) (fun (el obj) set)) (λ hom →
  times
    (pi (el obj) (λ x → el (hom x x)))
    (pi (el obj) (λ x → el (hom x x)))))

raw-category : Type empty (λ _ → raw-categoryU)
raw-category =
     -- Objects.
   sigma' set'
     -- Morphisms.
  (sigma' (pi' (el' (var zero)) (pi' (el' (var (suc zero))) set'))
     -- Identity.
  (sigma' (pi' (el' (var (suc zero)))
               (el' (app (app (var (suc zero)) (var zero)) (var zero))))
          (pi' (el' (var (suc (suc zero))))
               (el' (app (app (var (suc (suc zero))) (var zero)) (var zero))))))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Semigroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto

open Iso

private
  variable
    ℓ : Level

-- Semigroups as a record, inspired by the Agda standard library:
--
--  https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Bundles.agda#L48
--  https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L50
--
-- Note that as we are using Path for all equations the IsMagma record
-- would only contain isSet A if we had it.
record IsSemigroup {A : Type ℓ} (_·_ : A → A → A) : Type ℓ where

  -- TODO: add no-eta-equality for efficiency? This breaks some proofs later

  constructor issemigroup
  field
    is-set : isSet A
    assoc  : (x y z : A) → x · (y · z) ≡ (x · y) · z

record Semigroup : Type (ℓ-suc ℓ) where

  constructor semigroup

  field
    Carrier     : Type ℓ
    _·_         : Carrier → Carrier → Carrier
    isSemigroup : IsSemigroup _·_

  infixl 7 _·_

  open IsSemigroup isSemigroup public

-- Extractor for the carrier type
⟨_⟩ : Semigroup → Type ℓ
⟨_⟩ = Semigroup.Carrier

record SemigroupEquiv (M N : Semigroup {ℓ}) : Type ℓ where

  constructor semigroupequiv

  -- Shorter qualified names
  private
    module M = Semigroup M
    module N = Semigroup N

  field
    e     : ⟨ M ⟩ ≃ ⟨ N ⟩
    isHom : (x y : ⟨ M ⟩) → equivFun e (x M.· y) ≡ equivFun e x N.· equivFun e y

-- Develop some theory about Semigroups using various general results
-- that are stated using Σ-types. For this we define Semigroup as a
-- nested Σ-type, prove that it's equivalent to the above record
-- definition and then transport results along this equivalence.
module SemigroupΣTheory {ℓ} where

  RawSemigroupStructure : Type ℓ → Type ℓ
  RawSemigroupStructure X = X → X → X

  RawSemigroupEquivStr = AutoEquivStr RawSemigroupStructure

  rawSemigroupUnivalentStr : UnivalentStr _ RawSemigroupEquivStr
  rawSemigroupUnivalentStr = autoUnivalentStr RawSemigroupStructure

  SemigroupAxioms : (A : Type ℓ) → RawSemigroupStructure A → Type ℓ
  SemigroupAxioms A _·_ = isSet A
                        × ((x y z : A) → x · (y · z) ≡ (x · y) · z)

  SemigroupStructure : Type ℓ → Type ℓ
  SemigroupStructure = AxiomsStructure RawSemigroupStructure SemigroupAxioms

  SemigroupΣ : Type (ℓ-suc ℓ)
  SemigroupΣ = TypeWithStr ℓ SemigroupStructure

  isPropSemigroupAxioms : (A : Type ℓ) (_·_ : RawSemigroupStructure A)
                        → isProp (SemigroupAxioms A _·_)
  isPropSemigroupAxioms _ _ = isPropΣ isPropIsSet λ isSetA → isPropΠ3 λ _ _ _ → isSetA _ _

  SemigroupEquivStr : StrEquiv SemigroupStructure ℓ
  SemigroupEquivStr = AxiomsEquivStr RawSemigroupEquivStr SemigroupAxioms

  SemigroupAxiomsIsoIsSemigroup : {A : Type ℓ} (_·_ : RawSemigroupStructure A)
                                → Iso (SemigroupAxioms A _·_) (IsSemigroup _·_)
  fun (SemigroupAxiomsIsoIsSemigroup s) (x , y)           = issemigroup x y
  inv (SemigroupAxiomsIsoIsSemigroup s) (issemigroup x y) = (x , y)
  rightInv (SemigroupAxiomsIsoIsSemigroup s) _            = refl
  leftInv (SemigroupAxiomsIsoIsSemigroup s) _             = refl

  SemigroupAxioms≡IsSemigroup : {A : Type ℓ} (_·_ : RawSemigroupStructure A)
                              → SemigroupAxioms _ _·_ ≡ IsSemigroup _·_
  SemigroupAxioms≡IsSemigroup s = isoToPath (SemigroupAxiomsIsoIsSemigroup s)

  Semigroup→SemigroupΣ : Semigroup → SemigroupΣ
  Semigroup→SemigroupΣ (semigroup A _·_ isSemigroup) =
    A , _·_ , SemigroupAxiomsIsoIsSemigroup _ .inv isSemigroup

  SemigroupΣ→Semigroup : SemigroupΣ → Semigroup
  SemigroupΣ→Semigroup (A , _·_ , isSemigroupΣ) =
    semigroup A _·_ (SemigroupAxiomsIsoIsSemigroup _ .fun isSemigroupΣ)

  SemigroupIsoSemigroupΣ : Iso Semigroup SemigroupΣ
  SemigroupIsoSemigroupΣ =
    iso Semigroup→SemigroupΣ SemigroupΣ→Semigroup (λ _ → refl) (λ _ → refl)

  semigroupUnivalentStr : UnivalentStr SemigroupStructure SemigroupEquivStr
  semigroupUnivalentStr = axiomsUnivalentStr _ isPropSemigroupAxioms rawSemigroupUnivalentStr

  SemigroupΣPath : (M N : SemigroupΣ) → (M ≃[ SemigroupEquivStr ] N) ≃ (M ≡ N)
  SemigroupΣPath = SIP semigroupUnivalentStr

  SemigroupEquivΣ : (M N : Semigroup) → Type ℓ
  SemigroupEquivΣ M N = Semigroup→SemigroupΣ M ≃[ SemigroupEquivStr ] Semigroup→SemigroupΣ N

  SemigroupIsoΣPath : {M N : Semigroup} → Iso (SemigroupEquiv M N) (SemigroupEquivΣ M N)
  fun SemigroupIsoΣPath (semigroupequiv e h) = (e , h)
  inv SemigroupIsoΣPath (e , h)            = semigroupequiv e h
  rightInv SemigroupIsoΣPath _             = refl
  leftInv SemigroupIsoΣPath _              = refl

  SemigroupPath : (M N : Semigroup) → (SemigroupEquiv M N) ≃ (M ≡ N)
  SemigroupPath M N =
    SemigroupEquiv M N                                ≃⟨ isoToEquiv SemigroupIsoΣPath ⟩
    SemigroupEquivΣ M N                               ≃⟨ SemigroupΣPath _ _ ⟩
    Semigroup→SemigroupΣ M ≡ Semigroup→SemigroupΣ N ≃⟨ isoToEquiv (invIso (congIso SemigroupIsoSemigroupΣ)) ⟩
    M ≡ N ■

-- We now extract the important results from the above module

isPropIsSemigroup : {A : Type ℓ} (_·_ : A → A → A) → isProp (IsSemigroup _·_)
isPropIsSemigroup _·_ =
  subst isProp (SemigroupΣTheory.SemigroupAxioms≡IsSemigroup _·_)
        (SemigroupΣTheory.isPropSemigroupAxioms _ _·_)

SemigroupPath : (M N : Semigroup {ℓ}) → (SemigroupEquiv M N) ≃ (M ≡ N)
SemigroupPath = SemigroupΣTheory.SemigroupPath

-- To rename the fields when using a Semigroup use for example the following:
--
-- open Semigroup M renaming ( Carrier to M ; _·_ to _·M_ )

ext: agda

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --without-K #-}
open import Function.Related.TypeIsomorphisms.NP
open import Function.Inverse.NP
open import Data.Maybe.NP
open import Data.Nat

open import Explore.Type
open import Explore.Explorable
open import Explore.Sum

module Explore.Explorable.Maybe where

μMaybe : ∀ {A} → Explorable A → Explorable (Maybe A)
μMaybe μA = μ-iso (sym Maybe↔𝟙⊎) (μ𝟙 ⊎-μ μA)

μMaybe^ : ∀ {A} n → Explorable A → Explorable (Maybe^ n A)
μMaybe^ zero    μA = μA
μMaybe^ (suc n) μA = μMaybe (μMaybe^ n μA)

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


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

open import Relation.Binary.Core

module Loop.Definitions
  {a ℓ} {A : Set a}   -- The underlying set
  (_≈_ : Rel A ℓ)     -- The underlying equality
  where

open import Algebra.Core
open import Data.Product

LeftBol : Op₂ A → Set _
LeftBol _∙_ = ∀ x y z → (x ∙ (y ∙ (x ∙ z))) ≈ ((x ∙ (y ∙ z)) ∙ z )

RightBol : Op₂ A → Set _
RightBol _∙_ = ∀ x y z → (((z ∙ x) ∙ y) ∙ x) ≈ (z ∙ ((x ∙ y) ∙ x))

MoufangIdentity₁ : Op₂ A → Set _
MoufangIdentity₁  _∙_  = ∀ x y z → (z ∙ (x ∙ (z ∙ y))) ≈ (((z ∙ x) ∙ z) ∙ y)

MoufangIdentity₂ : Op₂ A → Set _
MoufangIdentity₂ _∙_ = ∀ x y z → (x ∙ (z ∙ (y ∙ z))) ≈ (((x ∙ z) ∙ y) ∙ z)

MoufangIdentity₃ : Op₂ A → Set _
MoufangIdentity₃ _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ ((z ∙ (x ∙ y)) ∙ z)

MoufangIdentity₄ : Op₂ A → Set _
MoufangIdentity₄ _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ (z ∙ ((x ∙ y) ∙ z))


text:
module UninstantiatedDotPattern where

f : Set -> Set -> Set
f .X X = X

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Opposite where

-- some properties of the opposite category.
-- XXX these should probably go somewhere else, but everywhere i think of
-- has other problems. ☹

open import Categories.Category
open import Categories.Functor
open import Categories.FunctorCategory
open import Categories.NaturalTransformation
open import Categories.Morphisms renaming (_≅_ to _[_≅_])

opⁱ : ∀ {o ℓ e} {C : Category o ℓ e} {A B} → C [ A ≅ B ] → Category.op C [ B ≅ A ]
opⁱ {C = C} A≅B = record
  { f = A≅B.f
  ; g = A≅B.g
  ; iso = record { isoˡ = A≅B.isoʳ; isoʳ = A≅B.isoˡ }
  }
  where
  module A≅B = Categories.Morphisms._≅_ A≅B

opF : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂} ->
    (Functor (Category.op (Functors (Category.op A) (Category.op B))) (Functors A B))
opF {A = A} {B} = record {
                    F₀ = Functor.op;
                    F₁ = NaturalTransformation.op;
                    identity = Category.Equiv.refl B;
                    homomorphism = Category.Equiv.refl B;
                    F-resp-≡ = λ x → x }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Categories.Category

-- a zero object is both terminal and initial.
module Categories.Object.Zero {o ℓ e} (C : Category o ℓ e) where

open import Level using (_⊔_)

open import Categories.Object.Terminal C
open import Categories.Object.Initial C

open Category C

record Zero : Set (o ⊔ ℓ ⊔ e) where
 field
   zero : Obj
   !    : ∀ {A} → zero ⇒ A
   ¡    : ∀ {A} → A ⇒ zero

 field
   !-unique : ∀ {A} (f : zero ⇒ A) → ! ≈ f
   ¡-unique : ∀ {A} (f : A ⇒ zero) → ¡ ≈ f

 initial : Initial
 initial = record
   { ⊥        = zero
   ; !        = !
   ; !-unique = !-unique
   }

 terminal : Terminal
 terminal = record
   { ⊤        = zero
   ; !        = ¡
   ; !-unique = ¡-unique
   }

 module initial  = Initial initial
 module terminal = Terminal terminal

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( Finite )

module Web.Semantic.DL.Category.Object {Σ : Signature} where

infixr 4 _,_
{-
This Object represents a Knowledge Base (schema + facts) with constraints.
It is defined over two TBoxes on the same Signature Σ
  S is the standard TBox - i.e. a schema
  T is the consTraint TBox - constraints on the facts A below
It is built from
  A is a  set of ABox facts over a finite set of variables

see "Integrity Constraints for Linked Data"
and especially the reference from there to Definition 1 p11 of
"Bridging the Gap between OWL and Relational Databases"
by Boris Motik, Ian Horrocks and Ulrike Sattler
-}
data Object (S T : TBox Σ) : Set₁ where
  _,_ : ∀ X → (X ∈ Finite × ABox Σ X) → Object S T

-- Interface Names, the nodes that can be used by other ABoxes
IN : ∀ {S T} → Object S T → Set
IN (X , X∈Fin , A) = X

-- the proof that X is finite
fin : ∀ {S T} → (A : Object S T) → (IN A ∈ Finite)
fin (X , X∈Fin , A) = X∈Fin

{- An ABox thought of as an interface
 (language from  "§3 Initial Interpretation" of
 "Integrity Constraints for Linked Data" )
The idea is that an ABox either creates nodes
that can be used by others or it uses nodes from
other ABoxes, and so it provides an interface to others  -}
iface : ∀ {S T} → (A : Object S T) → (ABox Σ (IN A))
iface (X , X∈Fin , A) = A

max_stars_repo_name: bblfish/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module sn-calculus-compatconf.pot where

open import can-function-preserve
  using (canₖ-monotonic ; canₛ-monotonic ; canₛₕ-monotonic)

open import sn-calculus
open import utility renaming (_U̬_ to _∪_)
open import context-properties
  using (->pot-view)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
  using (Can ; Canₛ ; Canₛₕ ; Canₖ ; Canθ ; Canθₛ ; Canθₛₕ ; Canθₖ)
open import Esterel.Lang.CanFunction.Properties
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Context.Properties
  using (unplugc)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning)
open import Data.Bool
  using (Bool ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _∷_ ; [] ; _++_)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function using (_∘_ ; id ; _∋_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ->pot-view

open Context1
open _≐_⟦_⟧c

{-
       (p)
  ρθ. C⟦pin⟧   -- sn⟶₁ ->    ρθ' C⟦pin⟧
 (ρθ) C⟦pin⟧   -- sn⟶₁ ->   (ρθ) C⟦qin⟧
-}
1-steplρ-pot-lemma : ∀{C θ p pin qin θ' BV FV A} →
  {ρθpsn⟶₁ρθ'p  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θ' , A ⟩· p} →

  ->pot-view  ρθpsn⟶₁ρθ'p  refl refl →

  CorrectBinding pin BV FV →
  p ≐ C ⟦ pin ⟧c →
  pin sn⟶₁ qin →

  ρ⟨ θ , A ⟩· C ⟦ qin ⟧c   sn⟶₁  ρ⟨ θ' , A ⟩· C ⟦ qin ⟧c

1-steplρ-pot-lemma {C} {θ} {_} {pin} {qin}
  {ρθpsn⟶₁ρθ'p = .(rabsence {S = S} S∈ θS≡unknown S∉can-p-θ)}
  (vabsence S S∈ θS≡unknown S∉can-p-θ)
  cb p≐C⟦pin⟧ pinsn⟶₁qin with sym (unplugc p≐C⟦pin⟧)
... | refl
  = rabsence {S = S} S∈ θS≡unknown
      (λ S∈can-q-θ →
        S∉can-p-θ
          (canθₛ-plug 0 (Env.sig θ) C pin qin
            (λ θ* → canₛ-monotonic θ* _ _ cb pinsn⟶₁qin ∘ _ₛ)
            (λ θ* → canₖ-monotonic θ* _ _ cb pinsn⟶₁qin)
            Env.[]env (Signal.unwrap S) S∈can-q-θ))

1-steplρ-pot-lemma {C} {θ} {_} {pin} {qin}
  {ρθpsn⟶₁ρθ'p = .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)}
  (vreadyness {θ = .θ} s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  cb p≐C⟦pin⟧ pinsn⟶₁qin with sym (unplugc p≐C⟦pin⟧)
... | refl
  = rreadyness {s = s} s∈ θs≡old⊎θs≡new
      (λ s∈can-q-θ →
        s∉can-p-θ
          (canθₛₕ-plug 0 (Env.sig θ) C pin qin
            (λ θ* → canₛₕ-monotonic θ* _ _ cb pinsn⟶₁qin ∘ _ₛₕ)
            (λ θ* → canₖ-monotonic θ* _ _ cb pinsn⟶₁qin)
            (λ θ* → canₛ-monotonic θ* _ _ cb pinsn⟶₁qin ∘ _ₛ)
            Env.[]env (SharedVar.unwrap s)
            s∈can-q-θ))

-- Wrapper around 1-steplρ-pot-lemma.
1-steplρ-pot : ∀{p q θ θ' BV FV A} →
  {ρθpsn⟶₁ρθ'p  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θ' , A ⟩· p} →
  CorrectBinding (ρ⟨ θ , A ⟩· p) BV FV →

  ->pot-view  ρθpsn⟶₁ρθ'p  refl refl →
  p sn⟶ q →

  (ρ⟨ θ' , A ⟩· p  sn⟶*  ρ⟨ θ' , A ⟩· q  ×
   ρ⟨ θ  , A ⟩· q  sn⟶*  ρ⟨ θ' , A ⟩· q)

1-steplρ-pot cb@(CBρ cb') pot psn⟶q@(rcontext _ p≐C⟦pin⟧ pinsn⟶₁qin) =
  sn⟶*-inclusion (rcontext _ (dcenv p≐C⟦pin⟧) pinsn⟶₁qin) ,′
  sn⟶*-inclusion
    (sn⟶-inclusion
      (1-steplρ-pot-lemma pot
        (proj₂ (binding-extractc' cb' p≐C⟦pin⟧))
        p≐C⟦pin⟧ pinsn⟶₁qin))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category.Base
open import Cubical.Categories.Monoidal.Base
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Functor.Base renaming (𝟙⟨_⟩ to idfunctor)
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Categories.NaturalTransformation.Properties

module Cubical.Categories.Instances.Functors.Endo {ℓC ℓC'} (C : Category ℓC ℓC') where

  open Category
  open NatTrans
  open Functor
  open StrictMonStr
  open TensorStr

  EndofunctorCategory : Category (ℓ-max ℓC ℓC') (ℓ-max ℓC ℓC')
  EndofunctorCategory = FUNCTOR C C

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS -v impossible:10 #-}

module ImpossibleVerbose where

-- The only way to trigger an __IMPOSSIBLE__ that isn't a bug.
{-# IMPOSSIBLE This message should be debug-printed with option '-v impossible:10'. #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module nodcap.NF.CutND where

open import Algebra
open import Category.Monad
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺
open import Data.List as L using (List; []; _∷_; _++_; map)
open import Data.List.Any as LA using (Any; here; there)
open import Data.List.Any.BagAndSetEquality as B
open import Data.Product as PR using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; _∘_; flip)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as I using ()
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)

open import Data.Environment
open import nodcap.Base
open import nodcap.NF.Typing
open import nodcap.NF.Contract
open import nodcap.NF.Expand
open import nodcap.NF.Cut

open I.Inverse using (to; from)
private
  open module LM {ℓ} = RawMonadPlus (L.monadPlus {ℓ})
private module ++ {a} {A : Set a} = Monoid (L.monoid A)

{-# TERMINATING #-}
-- Theorem:
--   Nondeterministic cut elimination.
mutual
  cutND : {Γ Δ : Environment} {A : Type} →

    ⊢ⁿᶠ A ∷ Γ → ⊢ⁿᶠ A ^ ∷ Δ →
    ---------------------
    List (⊢ⁿᶠ Γ ++ Δ)

  cutND {_} {Δ} {A = 𝟏} halt (wait y)
    = return y
  cutND {Γ} {_} {A = ⊥} (wait x) halt
    = return
    $ P.subst ⊢ⁿᶠ_ (P.sym (proj₂ ++.identity Γ)) x
  cutND {_} {Θ} {A = A ⊗ B} (send {Γ} {Δ} x y) (recv z)
    = return
    ∘ P.subst ⊢ⁿᶠ_ (P.sym (++.assoc Γ Δ Θ))
    ∘ exch (swp [] Γ Δ)
    =<< cutND y
    ∘ exch (fwd [] Γ)
    =<< cutND x z
  cutND {Θ} {_} {A = A ⅋ B} (recv x) (send {Γ} {Δ} y z)
    = return
    ∘ P.subst ⊢ⁿᶠ_ (++.assoc Θ Γ Δ)
    =<< flip cutND z
    =<< cutND x y
  cutND {Γ} {Δ} {A = A ⊕ B} (sel₁ x) (case y z)
    = cutND x y
  cutND {Γ} {Δ} {A = A ⊕ B} (sel₂ x) (case y z)
    = cutND x z
  cutND {Γ} {Δ} {A = A & B} (case x y) (sel₁ z)
    = cutND x z
  cutND {Γ} {Δ} {A = A & B} (case x y) (sel₂ z)
    = cutND y z
  cutND {Γ} {Δ} {A = ![ n ] A} x y
    = all (replicate⁺ n (A ^)) >>= return ∘ withPerm ∘ proj₂
    where
      withPerm : {Θ : Environment} → replicate⁺ n (A ^) ∼[ bag ] Θ → ⊢ⁿᶠ Γ ++ Δ
      withPerm {Θ} b
        = cut x
        $ contract
        $ exch (B.++-cong (P.subst (_ ∼[ bag ]_) (all-replicate⁺ n (I.sym b)) b) I.id)
        $ expand y
  cutND {Γ} {Δ} {A = ?[ n ] A} x y
    = all (replicate⁺ n A) >>= return ∘ withPerm ∘ proj₂
    where
      withPerm : {Θ : Environment} → replicate⁺ n A ∼[ bag ] Θ → ⊢ⁿᶠ Γ ++ Δ
      withPerm {Θ} b
        = exch (swp₂ Γ)
        $ cut y
        $ P.subst (λ A → ⊢ⁿᶠ ?[ n ] A ∷ Γ) (P.sym (^-inv A))
        $ contract
        $ exch (B.++-cong (P.subst (_ ∼[ bag ]_) (all-replicate⁺ n (I.sym b)) b) I.id)
        $ expand x
  cutND {Γ} {Δ} {A} (exch b x) y
    = return
    ∘ exch (B.++-cong {ys₁ = Δ} (del-from b (here P.refl)) I.id)
    =<< cutNDIn (from b ⟨$⟩ here P.refl) (here P.refl) x y
  cutND {Γ} {Δ} {A} x (exch b y)
    = return
    ∘ exch (B.++-cong {xs₁ = Γ} I.id (del-from b (here P.refl)))
    =<< cutNDIn (here P.refl) (from b ⟨$⟩ here P.refl) x y

  cutNDIn : {Γ Δ : Environment} {A : Type} (i : A ∈ Γ) (j : A ^ ∈ Δ) →

    ⊢ⁿᶠ Γ → ⊢ⁿᶠ Δ →
    -----------------------
    List (⊢ⁿᶠ Γ - i ++ Δ - j)

  cutNDIn (here P.refl) (here P.refl) x y = cutND x y

  cutNDIn {_} {Θ} (there i) j (send {Γ} {Δ} x y) z
    with split Γ i
  ... | inj₁ (k , p) rewrite p
      = return
      ∘ P.subst ⊢ⁿᶠ_ (P.sym (++.assoc (_ ∷ Γ - k) Δ (Θ - j)))
      ∘  exch (swp₃ (_ ∷ Γ - k) Δ)
      ∘  P.subst ⊢ⁿᶠ_ (++.assoc (_ ∷ Γ - k) (Θ - j) Δ)
      ∘ flip send y
      =<< cutNDIn (there k) j x z
  ... | inj₂ (k , p) rewrite p
      = return
      ∘ P.subst ⊢ⁿᶠ_ (P.sym (++.assoc (_ ∷ Γ) (Δ - k) (Θ - j)))
      ∘ send x
      =<< cutNDIn (there k) j y z
  cutNDIn (there i) j (recv x) y
    = return
    ∘ recv
    =<< cutNDIn (there (there i)) j x y
  cutNDIn (there i) j (sel₁ x) y
    = return
    ∘ sel₁
    =<< cutNDIn (there i) j x y
  cutNDIn (there i) j (sel₂ x) y
    = return
    ∘ sel₂
    =<< cutNDIn (there i) j x y
  cutNDIn (there i) j (case x y) z
    = cutNDIn (there i) j x z >>= λ xz
    → cutNDIn (there i) j y z >>= λ yz
    → return
    $ case xz yz
  cutNDIn (there ()) j halt y
  cutNDIn (there i) j (wait x) y
    = return
    ∘ wait
    =<< cutNDIn i j x y
  cutNDIn (there i) j loop y
    = return
    $ loop
  cutNDIn {Γ} {Δ} (there i) j (mk?₁ x) y
    = return
    ∘ mk?₁
    =<< cutNDIn (there i) j x y
  cutNDIn {Γ} {Δ} (there i) j (mk!₁ x) y
    = return
    ∘ mk!₁
    =<< cutNDIn (there i) j x y
  cutNDIn {Γ} {Δ} (there i) j (cont x) y
    = return
    ∘ cont
    =<< cutNDIn (there (there i)) j x y
  cutNDIn {_} {Θ} (there i) j (pool {Γ} {Δ} x y) z
    with split Γ i
  ... | inj₁ (k , p) rewrite p
      = return
      ∘ P.subst ⊢ⁿᶠ_ (P.sym (++.assoc (_ ∷ Γ - k) Δ (Θ - j)))
      ∘ exch (swp₃ (_ ∷ Γ - k) Δ)
      ∘ P.subst ⊢ⁿᶠ_ (++.assoc (_ ∷ Γ - k) (Θ - j) Δ)
      ∘ flip pool y
      =<< cutNDIn (there k) j x z
  ... | inj₂ (k , p) rewrite p
      = return
      ∘ P.subst ⊢ⁿᶠ_ (P.sym (++.assoc (_ ∷ Γ) (Δ - k) (Θ - j)))
      ∘ pool x
      =<< cutNDIn (there k) j y z

  cutNDIn {Θ} {_} i (there j) x (send {Γ} {Δ} y z)
    with split Γ j
  ... | inj₁ (k , p) rewrite p
      = return
      ∘ exch (bwd [] (Θ - i))
      ∘ P.subst ⊢ⁿᶠ_ (++.assoc (_ ∷ Θ - i) (Γ - k) Δ)
      ∘ flip send z
      ∘ exch (fwd [] (Θ - i))
      =<< cutNDIn i (there k) x y
  ... | inj₂ (k , p) rewrite p
      = return
      ∘ exch (swp [] (Θ - i) (_ ∷ Γ))
      ∘ send y
      ∘ exch (fwd [] (Θ - i))
      =<< cutNDIn i (there k) x z
  cutNDIn {Γ} i (there j) x (recv {Δ} y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ recv
    ∘ exch (swp [] (_ ∷ _ ∷ []) (Γ - i))
    =<< cutNDIn i (there (there j)) x y
  cutNDIn {Γ} {Δ} i (there j) x (sel₁ y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ sel₁
    ∘ exch (fwd [] (Γ - i))
    =<< cutNDIn i (there j) x y
  cutNDIn {Γ} {Δ} i (there j) x (sel₂ y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ sel₂
    ∘ exch (fwd [] (Γ - i))
    =<< cutNDIn i (there j) x y
  cutNDIn {Γ} {Δ} i (there j) x (case y z)
    = cutNDIn i (there j) x y >>= λ xy
    → cutNDIn i (there j) x z >>= λ xz
    → return
    $ exch (bwd [] (Γ - i))
    $ case
    ( exch (fwd [] (Γ - i)) xy )
    ( exch (fwd [] (Γ - i)) xz )
  cutNDIn {Γ} i (there ()) x halt
  cutNDIn {Γ} {Δ} i (there j) x (wait y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ wait
    =<< cutNDIn i j x y
  cutNDIn {Γ} {Δ} i (there j) x loop
    = return
    ∘ exch (bwd [] (Γ - i))
    $ loop
  cutNDIn {Γ} {Δ} i (there j) x (mk?₁ y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ mk?₁
    ∘ exch (fwd [] (Γ - i))
    =<< cutNDIn i (there j) x y
  cutNDIn {Γ} {Δ} i (there j) x (mk!₁ y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ mk!₁
    ∘ exch (fwd [] (Γ - i))
    =<< cutNDIn i (there j) x y
  cutNDIn {Γ} {Δ} i (there j) x (cont y)
    = return
    ∘ exch (bwd [] (Γ - i))
    ∘ cont
    ∘ exch (swp [] (_ ∷ _ ∷ []) (Γ - i))
    =<< cutNDIn i (there (there j)) x y
  cutNDIn {Θ} {_} i (there j) x (pool {Γ} {Δ} y z)
    with split Γ j
  ... | inj₁ (k , p) rewrite p
      = return
      ∘ exch (bwd [] (Θ - i))
      ∘ P.subst ⊢ⁿᶠ_ (++.assoc (_ ∷ Θ - i) (Γ - k) Δ)
      ∘ flip pool z
      ∘ exch (fwd [] (Θ - i))
      =<< cutNDIn i (there k) x y
  ... | inj₂ (k , p) rewrite p
      = return
      ∘ exch (swp [] (Θ - i) (_ ∷ Γ))
      ∘ pool y
      ∘ exch (fwd [] (Θ - i))
      =<< cutNDIn i (there k) x z

  cutNDIn {Γ} {Δ} i j (exch b x) y
    = return
    ∘ exch (B.++-cong {ys₁ = Δ - j} (del-from b i ) I.id)
    =<< cutNDIn (from b ⟨$⟩ i) j x y
  cutNDIn {Γ} {Δ} i j x (exch b y)
    = return
    ∘ exch (B.++-cong {xs₁ = Γ - i} I.id (del-from b j))
    =<< cutNDIn i (from b ⟨$⟩ j) x y

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
module OlderBasicILP.Indirect.Hilbert.Nested where

open import OlderBasicILP.Indirect public

-- Derivations, as Hilbert-style combinator trees.

mutual
  data Tm : Set where
    VAR   : ℕ → Tm
    APP   : Tm → Tm → Tm
    CI    : Tm
    CK    : Tm
    CS    : Tm
    BOX   : Tm → Tm
    CDIST : Tm
    CUP   : Tm
    CDOWN : Tm
    CPAIR : Tm
    CFST  : Tm
    CSND  : Tm
    UNIT  : Tm

  infix 3 _⊢_
  data _⊢_ (Γ : Cx (Ty Tm)) : Ty Tm → Set where
    var   : ∀ {A}       → A ∈ Γ → Γ ⊢ A
    app   : ∀ {A B}     → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
    ci    : ∀ {A}       → Γ ⊢ A ▻ A
    ck    : ∀ {A B}     → Γ ⊢ A ▻ B ▻ A
    cs    : ∀ {A B C}   → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
    box   : ∀ {A}       → (t : ∅ ⊢ A) → Γ ⊢ [ t ] ⦂ A
    cdist : ∀ {A B T U} → Γ ⊢ T ⦂ (A ▻ B) ▻ U ⦂ A ▻ APP T U ⦂ B
    cup   : ∀ {A T}     → Γ ⊢ T ⦂ A ▻ BOX T ⦂ T ⦂ A
    cdown : ∀ {A T}     → Γ ⊢ T ⦂ A ▻ A
    cpair : ∀ {A B}     → Γ ⊢ A ▻ B ▻ A ∧ B
    cfst  : ∀ {A B}     → Γ ⊢ A ∧ B ▻ A
    csnd  : ∀ {A B}     → Γ ⊢ A ∧ B ▻ B
    unit  : Γ ⊢ ⊤

  [_] : ∀ {A Γ} → Γ ⊢ A → Tm
  [ var i ]   = VAR [ i ]ⁱ
  [ app t u ] = APP [ t ] [ u ]
  [ ci ]      = CI
  [ ck ]      = CK
  [ cs ]      = CS
  [ box t ]   = BOX [ t ]
  [ cdist ]   = CDIST
  [ cup ]     = CUP
  [ cdown ]   = CDOWN
  [ cpair ]   = CPAIR
  [ cfst ]    = CFST
  [ csnd ]    = CSND
  [ unit ]    = UNIT

infix 3 _⊢⋆_
_⊢⋆_ : Cx (Ty Tm) → Cx (Ty Tm) → Set
Γ ⊢⋆ ∅     = 𝟙
Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (var i)   = var (mono∈ η i)
mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η ci        = ci
mono⊢ η ck        = ck
mono⊢ η cs        = cs
mono⊢ η (box t)   = box t
mono⊢ η cdist     = cdist
mono⊢ η cup       = cup
mono⊢ η cdown     = cdown
mono⊢ η cpair     = cpair
mono⊢ η cfst      = cfst
mono⊢ η csnd      = csnd
mono⊢ η unit      = unit

mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
mono⊢⋆ {∅}     η ∙        = ∙
mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

V₀ : Tm
V₀ = VAR 0

V₁ : Tm
V₁ = VAR 1

V₂ : Tm
V₂ = VAR 2

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → (Γ , A) , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → ((Γ , A) , B) , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem.

LAM : Tm → Tm
LAM (VAR zero)    = CI
LAM (VAR (suc i)) = APP CK (VAR i)
LAM (APP T U)     = APP (APP CS (LAM T)) (LAM U)
LAM CI            = APP CK CI
LAM CK            = APP CK CK
LAM CS            = APP CK CS
LAM (BOX T)       = APP CK (BOX T)
LAM CDIST         = APP CK CDIST
LAM CUP           = APP CK CUP
LAM CDOWN         = APP CK CDOWN
LAM CPAIR         = APP CK CPAIR
LAM CFST          = APP CK CFST
LAM CSND          = APP CK CSND
LAM UNIT          = APP CK UNIT

lam : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ▻ B
lam (var top)     = ci
lam (var (pop i)) = app ck (var i)
lam (app t u)     = app (app cs (lam t)) (lam u)
lam ci            = app ck ci
lam ck            = app ck ck
lam cs            = app ck cs
lam (box t)       = app ck (box t)
lam cdist         = app ck cdist
lam cup           = app ck cup
lam cdown         = app ck cdown
lam cpair         = app ck cpair
lam cfst          = app ck cfst
lam csnd          = app ck csnd
lam unit          = app ck unit

-- Detachment theorem.

DET : Tm → Tm
DET T = APP T V₀

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

-- Cut and multicut.

CUT : Tm → Tm → Tm
CUT T U = APP (LAM U) T

MULTICUT : Cx Tm → Tm → Tm
MULTICUT ∅        U = U
MULTICUT (TS , T) U = APP (MULTICUT TS (LAM U)) T

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

CCONT : Tm
CCONT = LAM (LAM (APP (APP V₁ V₀) V₀))

CONT : Tm → Tm
CONT T = DET (APP CCONT (LAM (LAM T)))

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

CEXCH : Tm
CEXCH = LAM (LAM (LAM (APP (APP V₂ V₀) V₁)))

EXCH : Tm → Tm
EXCH T = DET (DET (APP CEXCH (LAM (LAM T))))

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

CCOMP : Tm
CCOMP = LAM (LAM (LAM (APP V₂ (APP V₁ V₀))))

COMP : Tm → Tm → Tm
COMP T U = DET (APP (APP CCOMP (LAM T)) (LAM U))

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

DIST : Tm → Tm → Tm
DIST T U = APP (APP CDIST T) U

UP : Tm → Tm
UP T = APP CUP T

DOWN : Tm → Tm
DOWN T = APP CDOWN T

DISTUP : Tm → Tm → Tm
DISTUP T U = DIST T (UP U)

UNBOX : Tm → Tm → Tm
UNBOX T U = APP (LAM U) T

MULTIBOX : Cx Tm → Tm → Tm
MULTIBOX ∅        U = BOX U
MULTIBOX (TS , T) U = DISTUP (MULTIBOX TS (LAM U)) T

dist : ∀ {A B T U Γ} → Γ ⊢ T ⦂ (A ▻ B) → Γ ⊢ U ⦂ A → Γ ⊢ (APP T U) ⦂ B
dist t u = app (app cdist t) u

up : ∀ {A T Γ} → Γ ⊢ T ⦂ A → Γ ⊢ BOX T ⦂ T ⦂ A
up t = app cup t

down : ∀ {A T Γ} → Γ ⊢ T ⦂ A → Γ ⊢ A
down t = app cdown t

distup : ∀ {A B T U Γ} → Γ ⊢ T ⦂ (U ⦂ A ▻ B)
         → Γ ⊢ U ⦂ A → Γ ⊢ APP T (BOX U) ⦂ B
distup t u = dist t (up u)

unbox : ∀ {A C T U Γ} → Γ ⊢ T ⦂ A → Γ , T ⦂ A ⊢ U ⦂ C → Γ ⊢ U ⦂ C
unbox t u = app (lam u) t

-- FIXME ↓ FIXME ↓ FIXME -----------------------------------------------------
--
-- Do we need reduction on term representations?
--
-- Goal: Γ ⊢ [ u ] ⦂ A
-- Have: Γ ⊢ APP [ lam u ] (BOX S) ⦂ A

distup′ : ∀ {A B T U Γ} → Γ ⊢ LAM T ⦂ (U ⦂ A ▻ B) → Γ ⊢ U ⦂ A
          → Γ ⊢ APP (LAM T) (BOX U) ⦂ B
distup′ t u = dist t (up u)

-- multibox : ∀ {n A Γ} {SS : VCx Tm n} {Ξ : VCx (Ty Tm) n}
--            → Γ ⊢⋆ SS ⦂⋆ Ξ → (u : SS ⦂⋆ Ξ ⊢ A)
--            → Γ ⊢ [ u ] ⦂ A
-- multibox {SS = ∅}      {∅}     ∙        u = box u
-- multibox {SS = SS , S} {Ξ , B} (ts , t) u = {!distup (multibox ts (lam u)) t!}

-- FIXME ↑ FIXME ↑ FIXME -----------------------------------------------------

PAIR : Tm → Tm → Tm
PAIR T U = APP (APP CPAIR T) U

FST : Tm → Tm
FST T = APP CFST T

SND : Tm → Tm
SND T = APP CSND T

pair : ∀ {A B Γ} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ A
fst t = app cfst t

snd : ∀ {A B Γ} → Γ ⊢ A ∧ B → Γ ⊢ B
snd t = app csnd t

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Support for reflection
------------------------------------------------------------------------

module Reflection where

open import Data.Bool as Bool using (Bool); open Bool.Bool
open import Data.List using (List); open Data.List.List
open import Data.Nat using (ℕ) renaming (_≟_ to _≟-ℕ_)
open import Data.Nat.Show renaming (show to showNat)
open import Data.Float using (Float) renaming (_≟_ to _≟f_; show to showFloat)
open import Data.Char using (Char) renaming (_≟_ to _≟c_; show to showChar)
open import Data.String using (String) renaming (_≟_ to _≟s_; show to showString)
open import Data.Product
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe
open import Relation.Nullary
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product

------------------------------------------------------------------------
-- Names

-- Names.

postulate Name : Set

{-# BUILTIN QNAME Name #-}

private
  primitive
    primQNameEquality : Name → Name → Bool

-- Equality of names is decidable.

infix 4 _==_ _≟-Name_

private

  _==_ : Name → Name → Bool
  _==_ = primQNameEquality

_≟-Name_ : Decidable {A = Name} _≡_
s₁ ≟-Name s₂ with s₁ == s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- Names can be shown.

private
  primitive
    primShowQName : Name → String

showName : Name → String
showName = primShowQName

------------------------------------------------------------------------
-- Terms

-- Is the argument visible (explicit), hidden (implicit), or an
-- instance argument?

data Visibility : Set where
  visible hidden instance′ : Visibility

{-# BUILTIN HIDING   Visibility #-}
{-# BUILTIN VISIBLE  visible    #-}
{-# BUILTIN HIDDEN   hidden     #-}
{-# BUILTIN INSTANCE instance′  #-}

-- Arguments can be relevant or irrelevant.

data Relevance : Set where
  relevant irrelevant : Relevance

{-# BUILTIN RELEVANCE  Relevance  #-}
{-# BUILTIN RELEVANT   relevant   #-}
{-# BUILTIN IRRELEVANT irrelevant #-}

-- Arguments.

data Arg-info : Set where
  arg-info : (v : Visibility) (r : Relevance) → Arg-info

visibility : Arg-info → Visibility
visibility (arg-info v _) = v

relevance : Arg-info → Relevance
relevance (arg-info _ r) = r

data Arg (A : Set) : Set where
  arg : (i : Arg-info) (x : A) → Arg A

{-# BUILTIN ARGINFO    Arg-info #-}
{-# BUILTIN ARGARGINFO arg-info #-}
{-# BUILTIN ARG        Arg      #-}
{-# BUILTIN ARGARG     arg      #-}

-- Literals.

data Literal : Set where
  nat    : ℕ → Literal
  float  : Float → Literal
  char   : Char → Literal
  string : String → Literal
  name   : Name → Literal

{-# BUILTIN AGDALITERAL   Literal #-}
{-# BUILTIN AGDALITNAT    nat     #-}
{-# BUILTIN AGDALITFLOAT  float   #-}
{-# BUILTIN AGDALITCHAR   char    #-}
{-# BUILTIN AGDALITSTRING string  #-}
{-# BUILTIN AGDALITQNAME  name    #-}

-- Terms.

mutual
  data Term : Set where
    -- Variable applied to arguments.
    var     : (x : ℕ) (args : List (Arg Term)) → Term
    -- Constructor applied to arguments.
    con     : (c : Name) (args : List (Arg Term)) → Term
    -- Identifier applied to arguments.
    def     : (f : Name) (args : List (Arg Term)) → Term
    -- Different kinds of λ-abstraction.
    lam     : (v : Visibility) (t : Term) → Term
    -- Pattern matching λ-abstraction.
    pat-lam : (cs : List Clause) (args : List (Arg Term)) → Term
    -- Pi-type.
    pi      : (t₁ : Arg Type) (t₂ : Type) → Term
    -- A sort.
    sort    : Sort → Term
    -- A literal.
    lit     : Literal → Term
    -- Anything else.
    unknown : Term

  data Type : Set where
    el : (s : Sort) (t : Term) → Type

  data Sort : Set where
    -- A Set of a given (possibly neutral) level.
    set     : (t : Term) → Sort
    -- A Set of a given concrete level.
    lit     : (n : ℕ) → Sort
    -- Anything else.
    unknown : Sort

  data Pattern : Set where
    con    : Name → List (Arg Pattern) → Pattern
    dot    : Pattern
    var    : Pattern
    lit    : Literal → Pattern
    proj   : Name → Pattern
    absurd : Pattern

  data Clause : Set where
    clause        : List (Arg Pattern) → Term → Clause
    absurd-clause : List (Arg Pattern) → Clause

{-# BUILTIN AGDASORT    Sort    #-}
{-# BUILTIN AGDATYPE    Type    #-}
{-# BUILTIN AGDATERM    Term    #-}
{-# BUILTIN AGDAPATTERN Pattern #-}
{-# BUILTIN AGDACLAUSE  Clause  #-}

{-# BUILTIN AGDATERMVAR         var     #-}
{-# BUILTIN AGDATERMCON         con     #-}
{-# BUILTIN AGDATERMDEF         def     #-}
{-# BUILTIN AGDATERMLAM         lam     #-}
{-# BUILTIN AGDATERMEXTLAM      pat-lam #-}
{-# BUILTIN AGDATERMPI          pi      #-}
{-# BUILTIN AGDATERMSORT        sort    #-}
{-# BUILTIN AGDATERMLIT         lit     #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
{-# BUILTIN AGDATYPEEL          el      #-}
{-# BUILTIN AGDASORTSET         set     #-}
{-# BUILTIN AGDASORTLIT         lit     #-}
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}

{-# BUILTIN AGDAPATCON    con    #-}
{-# BUILTIN AGDAPATDOT    dot    #-}
{-# BUILTIN AGDAPATVAR    var    #-}
{-# BUILTIN AGDAPATLIT    lit    #-}
{-# BUILTIN AGDAPATPROJ   proj   #-}
{-# BUILTIN AGDAPATABSURD absurd #-}

{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}

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

-- Function definition.
data FunctionDef : Set where
  fun-def : Type → List Clause → FunctionDef

{-# BUILTIN AGDAFUNDEF    FunctionDef #-}
{-# BUILTIN AGDAFUNDEFCON fun-def     #-}

postulate
  -- Data type definition.
  Data-type : Set
  -- Record type definition.
  Record    : Set

{-# BUILTIN AGDADATADEF   Data-type #-}
{-# BUILTIN AGDARECORDDEF Record    #-}

-- Definitions.

data Definition : Set where
  function     : FunctionDef  → Definition
  data-type    : Data-type → Definition
  record′      : Record    → Definition
  constructor′ : Definition
  axiom        : Definition
  primitive′   : Definition

{-# BUILTIN AGDADEFINITION                Definition   #-}
{-# BUILTIN AGDADEFINITIONFUNDEF          function     #-}
{-# BUILTIN AGDADEFINITIONDATADEF         data-type    #-}
{-# BUILTIN AGDADEFINITIONRECORDDEF       record′      #-}
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR constructor′ #-}
{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom        #-}
{-# BUILTIN AGDADEFINITIONPRIMITIVE       primitive′   #-}

showLiteral : Literal → String
showLiteral (nat x)    = showNat x
showLiteral (float x)  = showFloat x
showLiteral (char x)   = showChar x
showLiteral (string x) = showString x
showLiteral (name x)   = showName x

private
  primitive
    primQNameType        : Name → Type
    primQNameDefinition  : Name → Definition
    primDataConstructors : Data-type → List Name

-- The type of the thing with the given name.

type : Name → Type
type = primQNameType

-- The definition of the thing with the given name.

definition : Name → Definition
definition = primQNameDefinition

-- The constructors of the given data type.

constructors : Data-type → List Name
constructors = primDataConstructors

------------------------------------------------------------------------
-- Term equality is decidable

-- Boring helper functions.

private

  cong₂′ : ∀ {A B C : Set} (f : A → B → C) {x y u v} →
          x ≡ y × u ≡ v → f x u ≡ f y v
  cong₂′ f = uncurry (cong₂ f)

  cong₃′ : ∀ {A B C D : Set} (f : A → B → C → D) {x y u v r s} →
           x ≡ y × u ≡ v × r ≡ s → f x u r ≡ f y v s
  cong₃′ f (refl , refl , refl) = refl

  arg₁ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → i ≡ i′
  arg₁ refl = refl

  arg₂ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → x ≡ x′
  arg₂ refl = refl

  arg-info₁ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′
  arg-info₁ refl = refl

  arg-info₂ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → r ≡ r′
  arg-info₂ refl = refl

  cons₁ : ∀ {A : Set} {x y} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → x ≡ y
  cons₁ refl = refl

  cons₂ : ∀ {A : Set} {x y} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
  cons₂ refl = refl

  var₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′
  var₁ refl = refl

  var₂ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → args ≡ args′
  var₂ refl = refl

  con₁ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → c ≡ c′
  con₁ refl = refl

  con₂ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → args ≡ args′
  con₂ refl = refl

  def₁ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → f ≡ f′
  def₁ refl = refl

  def₂ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → args ≡ args′
  def₂ refl = refl

  lam₁ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′
  lam₁ refl = refl

  lam₂ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → t ≡ t′
  lam₂ refl = refl

  pat-lam₁ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → cs ≡ cs′
  pat-lam₁ refl = refl

  pat-lam₂ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → args ≡ args′
  pat-lam₂ refl = refl

  pi₁ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₁ ≡ t₁′
  pi₁ refl = refl

  pi₂ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₂ ≡ t₂′
  pi₂ refl = refl

  sort₁ : ∀ {x y} → sort x ≡ sort y → x ≡ y
  sort₁ refl = refl

  lit₁ : ∀ {x y} → Term.lit x ≡ lit y → x ≡ y
  lit₁ refl = refl

  pcon₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′
  pcon₁ refl = refl

  pcon₂ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → args ≡ args′
  pcon₂ refl = refl

  plit₁ : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
  plit₁ refl = refl

  pproj₁ : ∀ {x y} → proj x ≡ proj y → x ≡ y
  pproj₁ refl = refl

  set₁ : ∀ {x y} → set x ≡ set y → x ≡ y
  set₁ refl = refl

  slit₁ : ∀ {x y} → Sort.lit x ≡ lit y → x ≡ y
  slit₁ refl = refl

  el₁ : ∀ {s s′ t t′} → el s t ≡ el s′ t′ → s ≡ s′
  el₁ refl = refl

  el₂ : ∀ {s s′ t t′} → el s t ≡ el s′ t′ → t ≡ t′
  el₂ refl = refl

  nat₁ : ∀ {x y} → nat x ≡ nat y → x ≡ y
  nat₁ refl = refl

  float₁ : ∀ {x y} → float x ≡ float y → x ≡ y
  float₁ refl = refl

  char₁ : ∀ {x y} → char x ≡ char y → x ≡ y
  char₁ refl = refl

  string₁ : ∀ {x y} → string x ≡ string y → x ≡ y
  string₁ refl = refl

  name₁ : ∀ {x y} → name x ≡ name y → x ≡ y
  name₁ refl = refl

  clause₁ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′
  clause₁ refl = refl

  clause₂ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → b ≡ b′
  clause₂ refl = refl

  absurd-clause₁ : ∀ {ps ps′} → absurd-clause ps ≡ absurd-clause ps′ → ps ≡ ps′
  absurd-clause₁ refl = refl

_≟-Visibility_ : Decidable (_≡_ {A = Visibility})
visible   ≟-Visibility visible   = yes refl
hidden    ≟-Visibility hidden    = yes refl
instance′ ≟-Visibility instance′ = yes refl
visible   ≟-Visibility hidden    = no λ()
visible   ≟-Visibility instance′ = no λ()
hidden    ≟-Visibility visible   = no λ()
hidden    ≟-Visibility instance′ = no λ()
instance′ ≟-Visibility visible   = no λ()
instance′ ≟-Visibility hidden    = no λ()

_≟-Relevance_ : Decidable (_≡_ {A = Relevance})
relevant   ≟-Relevance relevant   = yes refl
irrelevant ≟-Relevance irrelevant = yes refl
relevant   ≟-Relevance irrelevant = no λ()
irrelevant ≟-Relevance relevant   = no λ()

_≟-Arg-info_ : Decidable (_≡_ {A = Arg-info})
arg-info v r ≟-Arg-info arg-info v′ r′ =
  Dec.map′ (cong₂′ arg-info)
           < arg-info₁ , arg-info₂ >
           (v ≟-Visibility v′ ×-dec r ≟-Relevance r′)

_≟-Lit_ : Decidable (_≡_ {A = Literal})
nat x ≟-Lit nat x₁ = Dec.map′ (cong nat) nat₁ (x ≟-ℕ x₁)
nat x ≟-Lit float x₁ = no (λ ())
nat x ≟-Lit char x₁ = no (λ ())
nat x ≟-Lit string x₁ = no (λ ())
nat x ≟-Lit name x₁ = no (λ ())
float x ≟-Lit nat x₁ = no (λ ())
float x ≟-Lit float x₁ = Dec.map′ (cong float) float₁ (x ≟f x₁)
float x ≟-Lit char x₁ = no (λ ())
float x ≟-Lit string x₁ = no (λ ())
float x ≟-Lit name x₁ = no (λ ())
char x ≟-Lit nat x₁ = no (λ ())
char x ≟-Lit float x₁ = no (λ ())
char x ≟-Lit char x₁ = Dec.map′ (cong char) char₁ (x ≟c x₁)
char x ≟-Lit string x₁ = no (λ ())
char x ≟-Lit name x₁ = no (λ ())
string x ≟-Lit nat x₁ = no (λ ())
string x ≟-Lit float x₁ = no (λ ())
string x ≟-Lit char x₁ = no (λ ())
string x ≟-Lit string x₁ = Dec.map′ (cong string) string₁ (x ≟s x₁)
string x ≟-Lit name x₁ = no (λ ())
name x ≟-Lit nat x₁ = no (λ ())
name x ≟-Lit float x₁ = no (λ ())
name x ≟-Lit char x₁ = no (λ ())
name x ≟-Lit string x₁ = no (λ ())
name x ≟-Lit name x₁ = Dec.map′ (cong name) name₁ (x ≟-Name x₁)

mutual
  infix 4 _≟_ _≟-Args_ _≟-ArgType_

  _≟-ArgTerm_ : Decidable (_≡_ {A = Arg Term})
  arg i a ≟-ArgTerm arg i′ a′ =
    Dec.map′ (cong₂′ arg)
             < arg₁ , arg₂ >
             (i ≟-Arg-info i′ ×-dec a ≟ a′)

  _≟-ArgType_ : Decidable (_≡_ {A = Arg Type})
  arg i a ≟-ArgType arg i′ a′ =
    Dec.map′ (cong₂′ arg)
             < arg₁ , arg₂ >
             (i ≟-Arg-info i′ ×-dec a ≟-Type a′)

  _≟-ArgPattern_ : Decidable (_≡_ {A = Arg Pattern})
  arg i a ≟-ArgPattern arg i′ a′ =
    Dec.map′ (cong₂′ arg)
             < arg₁ , arg₂ >
             (i ≟-Arg-info i′ ×-dec a ≟-Pattern a′)

  _≟-Args_ : Decidable (_≡_ {A = List (Arg Term)})
  []       ≟-Args []       = yes refl
  (x ∷ xs) ≟-Args (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-ArgTerm y ×-dec xs ≟-Args ys)
  []       ≟-Args (_ ∷ _)  = no λ()
  (_ ∷ _)  ≟-Args []       = no λ()

  _≟-Clause_ : Decidable (_≡_ {A = Clause})
  clause ps b ≟-Clause clause ps′ b′ = Dec.map′ (cong₂′ clause) < clause₁ , clause₂ > (ps ≟-ArgPatterns ps′ ×-dec b ≟ b′)
  absurd-clause ps ≟-Clause absurd-clause ps′ = Dec.map′ (cong absurd-clause) absurd-clause₁ (ps ≟-ArgPatterns ps′)
  clause _ _      ≟-Clause absurd-clause _ = no λ()
  absurd-clause _ ≟-Clause clause _ _      = no λ()

  _≟-Clauses_ : Decidable (_≡_ {A = List Clause})
  []       ≟-Clauses []       = yes refl
  (x ∷ xs) ≟-Clauses (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-Clause y ×-dec xs ≟-Clauses ys)
  []       ≟-Clauses (_ ∷ _)  = no λ()
  (_ ∷ _)  ≟-Clauses []       = no λ()

  _≟-Pattern_ : Decidable (_≡_ {A = Pattern})
  con c ps ≟-Pattern con c′ ps′ = Dec.map′ (cong₂′ con) < pcon₁ , pcon₂ > (c ≟-Name c′ ×-dec ps ≟-ArgPatterns ps′)
  con x x₁ ≟-Pattern dot = no (λ ())
  con x x₁ ≟-Pattern var = no (λ ())
  con x x₁ ≟-Pattern lit x₂ = no (λ ())
  con x x₁ ≟-Pattern proj x₂ = no (λ ())
  con x x₁ ≟-Pattern absurd = no (λ ())
  dot ≟-Pattern con x x₁ = no (λ ())
  dot ≟-Pattern dot = yes refl
  dot ≟-Pattern var = no (λ ())
  dot ≟-Pattern lit x = no (λ ())
  dot ≟-Pattern proj x = no (λ ())
  dot ≟-Pattern absurd = no (λ ())
  var ≟-Pattern con x x₁ = no (λ ())
  var ≟-Pattern dot = no (λ ())
  var ≟-Pattern var = yes refl
  var ≟-Pattern lit x = no (λ ())
  var ≟-Pattern proj x = no (λ ())
  var ≟-Pattern absurd = no (λ ())
  lit x ≟-Pattern con x₁ x₂ = no (λ ())
  lit x ≟-Pattern dot = no (λ ())
  lit x ≟-Pattern var = no (λ ())
  lit l ≟-Pattern lit l′ = Dec.map′ (cong lit) plit₁ (l ≟-Lit l′)
  lit x ≟-Pattern proj x₁ = no (λ ())
  lit x ≟-Pattern absurd = no (λ ())
  proj x ≟-Pattern con x₁ x₂ = no (λ ())
  proj x ≟-Pattern dot = no (λ ())
  proj x ≟-Pattern var = no (λ ())
  proj x ≟-Pattern lit x₁ = no (λ ())
  proj x ≟-Pattern proj x₁ = Dec.map′ (cong proj) pproj₁ (x ≟-Name x₁)
  proj x ≟-Pattern absurd = no (λ ())
  absurd ≟-Pattern con x x₁ = no (λ ())
  absurd ≟-Pattern dot = no (λ ())
  absurd ≟-Pattern var = no (λ ())
  absurd ≟-Pattern lit x = no (λ ())
  absurd ≟-Pattern proj x = no (λ ())
  absurd ≟-Pattern absurd = yes refl

  _≟-ArgPatterns_ : Decidable (_≡_ {A = List (Arg Pattern)})
  []       ≟-ArgPatterns []       = yes refl
  (x ∷ xs) ≟-ArgPatterns (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-ArgPattern y ×-dec xs ≟-ArgPatterns ys)
  []       ≟-ArgPatterns (_ ∷ _)  = no λ()
  (_ ∷ _)  ≟-ArgPatterns []       = no λ()

  _≟_ : Decidable (_≡_ {A = Term})
  var x args ≟ var x′ args′ = Dec.map′ (cong₂′ var) < var₁ , var₂ > (x ≟-ℕ x′          ×-dec args ≟-Args args′)
  con c args ≟ con c′ args′ = Dec.map′ (cong₂′ con) < con₁ , con₂ > (c ≟-Name c′       ×-dec args ≟-Args args′)
  def f args ≟ def f′ args′ = Dec.map′ (cong₂′ def) < def₁ , def₂ > (f ≟-Name f′       ×-dec args ≟-Args args′)
  lam v t    ≟ lam v′ t′    = Dec.map′ (cong₂′ lam) < lam₁ , lam₂ > (v ≟-Visibility v′ ×-dec t ≟ t′)
  pat-lam cs args ≟ pat-lam cs′ args′ =
                              Dec.map′ (cong₂′ pat-lam) < pat-lam₁ , pat-lam₂ > (cs ≟-Clauses cs′ ×-dec args ≟-Args args′)
  pi t₁ t₂   ≟ pi t₁′ t₂′   = Dec.map′ (cong₂′ pi)  < pi₁  , pi₂  > (t₁ ≟-ArgType t₁′  ×-dec t₂ ≟-Type t₂′)
  sort s     ≟ sort s′      = Dec.map′ (cong sort)  sort₁           (s ≟-Sort s′)
  lit l      ≟ lit l′       = Dec.map′ (cong lit)   lit₁           (l ≟-Lit l′)
  unknown    ≟ unknown      = yes refl

  var x args ≟ con c args′ = no λ()
  var x args ≟ def f args′ = no λ()
  var x args ≟ lam v t     = no λ()
  var x args ≟ pi t₁ t₂    = no λ()
  var x args ≟ sort _      = no λ()
  var x args ≟ lit _      = no λ()
  var x args ≟ unknown     = no λ()
  con c args ≟ var x args′ = no λ()
  con c args ≟ def f args′ = no λ()
  con c args ≟ lam v t     = no λ()
  con c args ≟ pi t₁ t₂    = no λ()
  con c args ≟ sort _      = no λ()
  con c args ≟ lit _      = no λ()
  con c args ≟ unknown     = no λ()
  def f args ≟ var x args′ = no λ()
  def f args ≟ con c args′ = no λ()
  def f args ≟ lam v t     = no λ()
  def f args ≟ pi t₁ t₂    = no λ()
  def f args ≟ sort _      = no λ()
  def f args ≟ lit _      = no λ()
  def f args ≟ unknown     = no λ()
  lam v t    ≟ var x args  = no λ()
  lam v t    ≟ con c args  = no λ()
  lam v t    ≟ def f args  = no λ()
  lam v t    ≟ pi t₁ t₂    = no λ()
  lam v t    ≟ sort _      = no λ()
  lam v t    ≟ lit _      = no λ()
  lam v t    ≟ unknown     = no λ()
  pi t₁ t₂   ≟ var x args  = no λ()
  pi t₁ t₂   ≟ con c args  = no λ()
  pi t₁ t₂   ≟ def f args  = no λ()
  pi t₁ t₂   ≟ lam v t     = no λ()
  pi t₁ t₂   ≟ sort _      = no λ()
  pi t₁ t₂   ≟ lit _      = no λ()
  pi t₁ t₂   ≟ unknown     = no λ()
  sort _     ≟ var x args  = no λ()
  sort _     ≟ con c args  = no λ()
  sort _     ≟ def f args  = no λ()
  sort _     ≟ lam v t     = no λ()
  sort _     ≟ pi t₁ t₂    = no λ()
  sort _     ≟ lit _       = no λ()
  sort _     ≟ unknown     = no λ()
  lit _     ≟ var x args  = no λ()
  lit _     ≟ con c args  = no λ()
  lit _     ≟ def f args  = no λ()
  lit _     ≟ lam v t     = no λ()
  lit _     ≟ pi t₁ t₂    = no λ()
  lit _     ≟ sort _      = no λ()
  lit _     ≟ unknown     = no λ()
  unknown    ≟ var x args  = no λ()
  unknown    ≟ con c args  = no λ()
  unknown    ≟ def f args  = no λ()
  unknown    ≟ lam v t     = no λ()
  unknown    ≟ pi t₁ t₂    = no λ()
  unknown    ≟ sort _      = no λ()
  unknown    ≟ lit _       = no λ()
  pat-lam _ _ ≟ var x args  = no λ()
  pat-lam _ _ ≟ con c args  = no λ()
  pat-lam _ _ ≟ def f args  = no λ()
  pat-lam _ _ ≟ lam v t     = no λ()
  pat-lam _ _ ≟ pi t₁ t₂    = no λ()
  pat-lam _ _ ≟ sort _      = no λ()
  pat-lam _ _ ≟ lit _       = no λ()
  pat-lam _ _ ≟ unknown     = no λ()
  var x args  ≟ pat-lam _ _ = no λ()
  con c args  ≟ pat-lam _ _ = no λ()
  def f args  ≟ pat-lam _ _ = no λ()
  lam v t     ≟ pat-lam _ _ = no λ()
  pi t₁ t₂    ≟ pat-lam _ _ = no λ()
  sort _      ≟ pat-lam _ _ = no λ()
  lit _       ≟ pat-lam _ _ = no λ()
  unknown     ≟ pat-lam _ _ = no λ()

  _≟-Type_ : Decidable (_≡_ {A = Type})
  el s t ≟-Type el s′ t′ = Dec.map′ (cong₂′ el) < el₁ , el₂ > (s ≟-Sort s′ ×-dec t ≟ t′)

  _≟-Sort_ : Decidable (_≡_ {A = Sort})
  set t   ≟-Sort set t′  = Dec.map′ (cong set) set₁ (t ≟ t′)
  lit n   ≟-Sort lit n′  = Dec.map′ (cong lit) slit₁ (n ≟-ℕ n′)
  unknown ≟-Sort unknown = yes refl
  set _   ≟-Sort lit _   = no λ()
  set _   ≟-Sort unknown = no λ()
  lit _   ≟-Sort set _   = no λ()
  lit _   ≟-Sort unknown = no λ()
  unknown ≟-Sort set _   = no λ()
  unknown ≟-Sort lit _   = no λ()


text:
module Issue313 where

postulate
  QName : Set

{-# BUILTIN QNAME QName #-}

postulate
  X   : Set
  _+_ : QName → QName → Set

foo : Set
foo = quote X + quote X


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Simple combinators working solely on and with functions
------------------------------------------------------------------------

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

module Function where

open import Level
open import Strict

infixr 9 _∘_ _∘′_
infixl 8 _ˢ_
infixl 1 _on_
infixl 1 _⟨_⟩_
infixr -1 _$_ _$′_ _$!_ _$!′_
infixr 0 _-[_]-_
infixl 0 _|>_ _|>′_ _∋_

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

-- Unary functions on a given set.

Fun₁ : ∀ {i} → Set i → Set i
Fun₁ A = A → A

-- Binary functions on a given set.

Fun₂ : ∀ {i} → Set i → Set i
Fun₂ A = A → A → A

------------------------------------------------------------------------
-- Functions

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         (B → C) → (A → B) → (A → C)
f ∘′ g = _∘_ f g

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

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x = λ _ → x

-- The S combinator. (Written infix as in Conor McBride's paper
-- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax
-- and evaluation".)

_ˢ_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} →
      ((x : A) (y : B x) → C x y) →
      (g : (x : A) → B x) →
      ((x : A) → C x (g x))
f ˢ g = λ x → f x (g x)

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

-- Note that _$_ is right associative, like in Haskell. If you want a
-- left associative infix application operator, use
-- Category.Functor._<$>_, available from
-- Category.Monad.Identity.IdentityMonad.

_$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
      ((x : A) → B x) → ((x : A) → B x)
f $ x = f x

_$′_ : ∀ {a b} {A : Set a} {B : Set b} →
       (A → B) → (A → B)
_$′_ = _$_

-- Strict (call-by-value) application

_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} →
       ((x : A) → B x) → ((x : A) → B x)
_$!_ = flip force

_$!′_ : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B) → (A → B)
_$!′_ = _$!_

-- flipped application aka pipe-forward

_|>_ : ∀ {a b} {A : Set a} {B : A → Set b} →
       (a : A) → (∀ a → B a) → B a
_|>_ = flip _$_

_|>′_ : ∀ {a b} {A : Set a} {B : Set b} →
        A → (A → B) → B
_|>′_ = _|>_

_⟨_⟩_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
        A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y

_on_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       (B → B → C) → (A → B) → (A → A → C)
_*_ on f = λ x y → f x * f y

_-[_]-_ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c}
            {D : Set d} {E : Set e} →
          (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
f -[ _*_ ]- g = λ x y → f x y * g x y

-- In Agda you cannot annotate every subexpression with a type
-- signature. This function can be used instead.

_∋_ : ∀ {a} (A : Set a) → A → A
A ∋ x = x

-- Conversely it is sometimes useful to be able to extract the
-- type of a given expression:

typeOf : ∀ {a} {A : Set a} → A → Set a
typeOf {A = A} _ = A

-- Case expressions (to be used with pattern-matching lambdas, see
-- README.Case).

infix 0 case_return_of_ case_of_

case_return_of_ :
  ∀ {a b} {A : Set a}
  (x : A) (B : A → Set b) → ((x : A) → B x) → B x
case x return B of f = f x

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = case x return _ of f


text:
{-# OPTIONS --universe-polymorphism #-}
open import Common.Prelude
  renaming (Nat to ℕ; module Nat to ℕ)
   using (zero; suc; _+_; _∸_; List; []; _∷_; Bool; true; false)
open import Common.Level
open import Common.Reflection

module TermSplicing where

module Library where
  data Box {a} (A : Set a) : Set a where
    box : A → Box A

  record ⊤ : Set where
    constructor tt

  infixr 5 _×_
  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      proj₁ : A
      proj₂ : B

  [_] : ∀ {A : Set} → A → List A
  [ x ] = x ∷ []

  replicate : ∀ {A : Set} → ℕ → A → List A
  replicate zero x = []
  replicate (suc n) x = x ∷ replicate n x

  foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
  foldr c n []       = n
  foldr c n (x ∷ xs) = c x (foldr c n xs)

  foldl : ∀ {A B : Set} → (A → B → A) → A → List B → A
  foldl c n []       = n
  foldl c n (x ∷ xs) = foldl c (c n x) xs

  reverse : ∀ {A : Set} → List A → List A
  reverse = foldl (λ rev x → x ∷ rev) []

  length : ∀ {A : Set} → List A → ℕ
  length = foldr (λ _ → suc) 0

  data Maybe (A : Set) : Set where
    nothing : Maybe A
    just    : A → Maybe A

  mapMaybe : ∀ {A B : Set} → (A → B) → Maybe A → Maybe B
  mapMaybe f (just x) = just (f x)
  mapMaybe f nothing  = nothing

  when : ∀ {A} → Bool → Maybe A → Maybe A
  when true  x = x
  when false _ = nothing

  infix 6 _≡_

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

  _→⟨_⟩_ : ∀ (A : Set) (n : ℕ) (B : Set) → Set
  A →⟨ zero  ⟩ B = B
  A →⟨ suc n ⟩ B = A → A →⟨ n ⟩ B

open Library

module ReflectLibrary where
  lamᵛ : Term → Term
  lamᵛ t = lam visible (abs "_" t)

  lamʰ : Term → Term
  lamʰ t = lam hidden (abs "_" t)

  argᵛʳ : ∀{a} {A : Set a} → A → Arg A
  argᵛʳ = arg (argInfo visible relevant)

  argʰʳ : ∀{a} {A : Set a} → A → Arg A
  argʰʳ = arg (argInfo hidden relevant)

  app` : (Args → Term) → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  app` f = go [] where
    go : List (Arg Term) → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
    go args []             = f (reverse args)
    go args (i ∷ hs) = λ t → go (arg i t ∷ args) hs

  con` : QName → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  con` x = app` (con x)

  def` : QName → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  def` x = app` (def x)

  var` : ℕ → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  var` x = app` (var x)

  coe : ∀ {A : Set} {z : A} n → (Term →⟨ length (replicate n z) ⟩ Term) → Term →⟨ n ⟩ Term
  coe zero    t = t
  coe (suc n) f = λ t → coe n (f t)

  con`ⁿʳ : QName → (n : ℕ) → Term →⟨ n ⟩ Term
  con`ⁿʳ x n = coe n (app` (con x) (replicate n (argInfo visible relevant)))

  def`ⁿʳ : QName → (n : ℕ) → Term →⟨ n ⟩ Term
  def`ⁿʳ x n = coe n (app` (def x) (replicate n (argInfo visible relevant)))

  var`ⁿʳ : ℕ → (n : ℕ) → Term →⟨ n ⟩ Term
  var`ⁿʳ x n = coe n (app` (var x) (replicate n (argInfo visible relevant)))

  sort₀ : Sort
  sort₀ = lit 0

  sort₁ : Sort
  sort₁ = lit 1

  `Set₀ : Term
  `Set₀ = sort sort₀

  unArg : ∀ {a} {A : Set a} → Arg A → A
  unArg (arg _ a) = a

  `Level : Term
  `Level = def (quote Level) []

  ℕ→Level : ℕ → Level
  ℕ→Level zero    = lzero
  ℕ→Level (suc n) = lsuc (ℕ→Level n)

  -- Can't match on Levels anymore
--   Level→ℕ : Level → ℕ
--   Level→ℕ zero    = zero
--   Level→ℕ (suc n) = suc (Level→ℕ n)

  setLevel : Level → Sort
  setLevel ℓ = lit 0 -- (Level→ℕ ℓ)

  _==_ : QName → QName → Bool
  _==_ = primQNameEquality

  decodeSort : Sort → Maybe Level
  decodeSort (set (con c [])) = when (quote lzero == c) (just lzero)
  decodeSort (set (con c (arg (argInfo visible relevant) s ∷ [])))
    = when (quote lsuc == c) (mapMaybe lsuc (decodeSort (set s)))
  decodeSort (set (sort s)) = decodeSort s
  decodeSort (set _) = nothing
  decodeSort (lit n) = just (ℕ→Level n)
  decodeSort (prop _) = nothing
  decodeSort (propLit _) = nothing
  decodeSort (inf _) = nothing
  decodeSort unknown = nothing

  _`⊔`_ : Sort → Sort → Sort
  s₁ `⊔` s₂ with decodeSort s₁ | decodeSort s₂
  ...          | just n₁       | just n₂        = setLevel (n₁ ⊔ n₂)
  ...          | _             | _              = set (def (quote _⊔_) (argᵛʳ (sort s₁) ∷ argᵛʳ (sort s₂) ∷ []))

  Π : Arg Type → Type → Type
  Π t u = pi t (abs "_" u)

  Πᵛʳ : Type → Type → Type
  Πᵛʳ t u = Π (vArg t) u

  Πʰʳ : Type → Type → Type
  Πʰʳ t u = Π (hArg t) u

open ReflectLibrary

`ℕ : Term
`ℕ = def (quote ℕ) []

`ℕOk : (unquote (give `ℕ)) ≡ ℕ
`ℕOk = refl

idℕ : ℕ → ℕ
idℕ = unquote (give (lamᵛ (var 0 [])))

id : (A : Set) → A → A
id = unquote (give (lamᵛ (lamᵛ (var 0 []))))

idBox : Box ({A : Set} → A → A)
idBox = box (unquote (give (lamᵛ (var 0 []))))

-- builds a pair
_`,_ : Term → Term → Term
_`,_ = con`ⁿʳ (quote _,_) 2

`tt : Term
`tt = con (quote tt) []

tuple : List Term → Term
tuple = foldr _`,_ `tt

`refl : Term
`refl = con (quote refl) []

`zero : Term
`zero = con (quote ℕ.zero) []

`[] : Term
`[] = con (quote []) []

_`∷_ : (`x `xs : Term) → Term
_`∷_ = con`ⁿʳ (quote _∷_) 2

`abs : (`s `body : Term) → Term
`abs = con`ⁿʳ (quote abs) 2

`var : (`n `args : Term) → Term
`var = con`ⁿʳ (quote Term.var) 2

`lam : (`hiding `body : Term) → Term
`lam = con`ⁿʳ (quote lam) 2

`lit : Term → Term
`lit = con`ⁿʳ (quote Term.lit) 1

`string : Term → Term
`string = con`ⁿʳ (quote string) 1

`visible : Term
`visible = con (quote visible) []

`hidden : Term
`hidden = con (quote hidden) []

`[_`] : Term → Term
`[ x `] = x `∷ `[]

quotedTwice : Term
quotedTwice = `lam `visible (`abs (lit (string "_")) (`var `zero `[]))

unquoteTwice₂ : ℕ → ℕ
unquoteTwice₂ = unquote (give (unquote (give quotedTwice)))

unquoteTwice : ℕ → ℕ
unquoteTwice x = unquote (give (unquote (give (`var `zero `[]))))

id₂ : {A : Set} → A → A
id₂ = unquote (give (lamᵛ (var 0 [])))

id₃ : {A : Set} → A → A
id₃ x = unquote (give (var 0 []))

module Id {A : Set} (x : A) where
  x′ : A
  x′ = unquote (give (var 0 []))

k`ℕ : ℕ → Term
k`ℕ zero    = `ℕ
k`ℕ (suc n) = unquote (give (def (quote k`ℕ) [ argᵛʳ (var 0 []) ])) -- k`ℕ n

test : id ≡ (λ A (x : A) → x)
     × unquote (give `Set₀)                      ≡ Set
     × unquote (give `ℕ)                        ≡ ℕ
     × unquote (give (lamᵛ (var 0 [])))          ≡ (λ (x : Set) → x)
     × id                                        ≡ (λ A (x : A) → x)
     × unquote (give `tt)                        ≡ tt
     × (λ {A} → Id.x′ {A})                ≡ (λ {A : Set} (x : A) → x)
     × unquote (give (pi (vArg `Set₀) (abs "_" `Set₀)))  ≡ (Set → Set)
     × unquoteTwice                        ≡ (λ (x : ℕ) → x)
     × unquote (give (k`ℕ 42))                    ≡ ℕ
     × unquote (give (lit (nat 15)))              ≡ 15
     × unquote (give (lit (float 3.1415)))        ≡ 3.1415
     × unquote (give (lit (string "foo")))        ≡ "foo"
     × unquote (give (lit (char 'X')))            ≡ 'X'
     × unquote (give (lit (qname (quote ℕ))))      ≡ quote ℕ
     × ⊤
test = unquote (give (tuple (replicate n `refl))) where n = 15

Πⁿ : ℕ → Type → Type
Πⁿ zero    t = t
Πⁿ (suc n) t = Π (argʰʳ `Set₀) (Πⁿ n t)

ƛⁿ : Hiding → ℕ → Term → Term
ƛⁿ h zero    t = t
ƛⁿ h (suc n) t = lam h (abs "_" (ƛⁿ h n t))

-- projᵢ : Proj i n
-- projᵢ = proj i n
-- Projᵢ = {A₁ ... Ai ... An : Set} → A₁ → ... → Aᵢ → ... → An → Aᵢ
-- projᵢ = λ {A₁ ... Ai ... An} x₁ ... xᵢ ... xn → xᵢ

Proj : (i n : ℕ) → Term
Proj i n = Πⁿ n (go n) where
  n∸1 = n ∸ 1
  go : ℕ → Type
  go zero    = var ((n + n) ∸ i) []
  go (suc m) = Π (argᵛʳ (var n∸1 [])) (go m)

proj : (i n : ℕ) → Term
proj i n = ƛⁿ visible n (var (n ∸ i) [])

projFull : (i n : ℕ) → Term
projFull i n = ƛⁿ hidden n (proj i n)

ℕ→ℕ : Set
ℕ→ℕ = unquote (give (Π (argᵛʳ `ℕ) `ℕ))

ℕ→ℕOk : ℕ→ℕ ≡ (ℕ → ℕ)
ℕ→ℕOk = refl

``∀A→A : Type
``∀A→A = Πᵛʳ `Set₀ (var 0 [])

∀A→A : Set₁
∀A→A = unquote (give ``∀A→A)

Proj₁¹ : Set₁
Proj₁¹ = unquote (give (Proj 1 1))

Proj₁² : Set₁
Proj₁² = unquote (give (Proj 1 2))

Proj₂² : Set₁
Proj₂² = unquote (give (Proj 2 2))

proj₃⁵ : unquote (give (Proj 3 5))
proj₃⁵ _ _ x _ _ = x

proj₃⁵′ : Box (unquote (give (Proj 3 5)))
proj₃⁵′ = box (unquote (give (proj 3 5)))

proj₂⁷ : unquote (give (Proj 2 7))
proj₂⁷ = unquote (give (proj 2 7))

test-proj : proj₃⁵′                ≡ box (λ _ _ x _ _ → x)
          × Proj₁¹                 ≡ ({A : Set} → A → A)
          × Proj₁²                 ≡ ({A₁ A₂ : Set} → A₁ → A₂ → A₁)
          × Proj₂²                 ≡ ({A₁ A₂ : Set} → A₁ → A₂ → A₂)
          × unquote (give (Proj 3 5))     ≡ ({A₁ A₂ A₃ A₄ A₅ : Set} → A₁ → A₂ → A₃ → A₄ → A₅ → A₃)
          × unquote (give (projFull 1 1)) ≡ (λ {A : Set} (x : A) → x)
          × unquote (give (projFull 1 2)) ≡ (λ {A₁ A₂ : Set} (x₁ : A₁) (x₂ : A₂) → x₁)
          × unquote (give (projFull 2 2)) ≡ (λ {A₁ A₂ : Set} (x₁ : A₁) (x₂ : A₂) → x₂)
          × ∀A→A                   ≡ (∀ (A : Set) → A)
          × ⊤
test-proj = unquote (give (tuple (replicate n `refl))) where n = 9

module Test where
  data Squash (A : Set) : Set where
    squash : unquote (give (Π (arg (argInfo visible irrelevant) (var 0 []))
                              (def (quote Squash) (argᵛʳ (var 1 []) ∷ []))))

data Squash (A : Set) : Set where
  squash : .A → Squash A

`Squash : Term → Term
`Squash = def`ⁿʳ (quote Squash) 1

squash-type : Type
squash-type = Π (arg (argInfo visible irrelevant) (var 0 [])) (`Squash (var 1 []))

test-squash : ∀ {A} → (.A → Squash A) ≡ unquote (give squash-type)
test-squash = refl

`∀ℓ→Setℓ : Type
`∀ℓ→Setℓ = Πᵛʳ `Level (sort (set (var 0 [])))


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

open import lib.Basics
open import lib.NType
open import lib.types.Cospan
open import lib.types.Pointed
open import lib.types.Sigma

module lib.types.Pullback where

module _ {i j k} (D : Cospan {i} {j} {k}) where

  open Cospan D

  record Pullback : Type (lmax i (lmax j k)) where
    constructor pullback
    field
      a : A
      b : B
      h : f a == g b

  pullback= : {a a' : A} (p : a == a') {b b' : B} (q : b == b')
    {h : f a == g b} {h' : f a' == g b'} (r : h ∙ ap g q == ap f p ∙ h')
    → pullback a b h == pullback a' b' h'
  pullback= idp idp r =
    ap (pullback _ _) (! (∙-unit-r _) ∙ r)

  pullback-aβ : {a a' : A} (p : a == a') {b b' : B} (q : b == b')
    {h : f a == g b} {h' : f a' == g b'} (r : h ∙ ap g q == ap f p ∙ h')
    → ap Pullback.a (pullback= p q {h = h} {h' = h'} r) == p
  pullback-aβ idp idp r =
    ap Pullback.a (ap (pullback _ _) (! (∙-unit-r _) ∙ r))
      =⟨ ∘-ap Pullback.a (pullback _ _) _ ⟩
    ap (λ _ → _) (! (∙-unit-r _) ∙ r)
      =⟨ ap-cst _ _ ⟩
    idp =∎

  pullback-bβ : {a a' : A} (p : a == a') {b b' : B} (q : b == b')
    {h : f a == g b} {h' : f a' == g b'} (r : h ∙ ap g q == ap f p ∙ h')
    → ap Pullback.b (pullback= p q {h = h} {h' = h'} r) == q
  pullback-bβ idp idp r =
    ap Pullback.b (ap (pullback _ _) (! (∙-unit-r _) ∙ r))
      =⟨ ∘-ap Pullback.b (pullback _ _) _ ⟩
    ap (λ _ → _) (! (∙-unit-r _) ∙ r)
      =⟨ ap-cst _ _ ⟩
    idp =∎

module _ {i j k} (D : ⊙Cospan {i} {j} {k}) where

  ⊙Pullback : Ptd (lmax i (lmax j k))
  ⊙Pullback =
    ⊙[ Pullback (⊙cospan-out D) ,
       pullback (pt X) (pt Y) (snd f ∙ ! (snd g)) ]
    where open ⊙Cospan D

module _ {i j k} (D : Cospan {i} {j} {k}) where
  open Cospan D

  pullback-decomp-equiv : Pullback D ≃ Σ (A × B) (λ {(a , b) → f a == g b})
  pullback-decomp-equiv = equiv
    (λ {(pullback a b h) → ((a , b) , h)})
    (λ {((a , b) , h) → pullback a b h})
    (λ _ → idp)
    (λ _ → idp)

module _ {i j k} (n : ℕ₋₂) {D : Cospan {i} {j} {k}} where
  open Cospan D

  pullback-level : has-level n A → has-level n B → has-level n C
    → has-level n (Pullback D)
  pullback-level pA pB pC =
    equiv-preserves-level ((pullback-decomp-equiv D)⁻¹) $
      Σ-level (×-level pA pB) (λ _ → =-preserves-level pC)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

module Data.Empty where

open import Data.Empty.Base public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --without-K #-}
module tactic where

open import Type
open import Search.Type
open import Search.Searchable
open import Search.Searchable.Product

open import Data.One
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality.NP

module _ {R S} (sum-R : Sum R)(sum-R-ext : SumExt sum-R)(sum-S : Sum S) where
  su-× : ∀ {f : R → R}{g : S → S} → SumStableUnder sum-R f → SumStableUnder sum-S g
       → SumStableUnder (sum-R ×-sum sum-S) (map f g)
  su-× {f}{g} su-f su-g F
    = (sum-R ×-sum sum-S) F
    ≡⟨ sum-R-ext (λ x → su-g (λ y → F ( x , y))) ⟩
      (sum-R ×-sum sum-S) (F ∘ map id g)
    ≡⟨ su-f (λ x → sum-S (λ y → F (map id g (x , y)))) ⟩
      (sum-R ×-sum sum-S) (F ∘ map f g)
    ∎ where open ≡-Reasoning

module _ {R}(sum-R : Sum R) where
  su-id : SumStableUnder sum-R id
  su-id f = refl

  su-∘ : ∀ {f g} → SumStableUnder sum-R f → SumStableUnder sum-R g → SumStableUnder sum-R (f ∘ g)
  su-∘ {f} su-f su-g F = trans (su-f F) (su-g (F ∘ f))

module with-sum {R R' S'}(sum-R : Sum R)(sum-R' : Sum R')(sum-S' : Sum S')(sum-R'-ext : SumExt sum-R')
           (h : R' → R')(su-h : SumStableUnder sum-R' h)
           (to : R' → S' → R)(sum-same : ∀ f → sum-R f ≡ sum-R' (λ r' → sum-S' (f ∘ to r'))) where

  principle : ∀ {f g} → (∀ r' → sum-S' (f ∘ to r') ≡ sum-S' (g ∘ to (h r'))) → sum-R f ≡ sum-R g
  principle {f}{g} prf
    = sum-R f
    ≡⟨ sum-same f ⟩
      sum-R' (λ r' → sum-S' (λ s' → f (to r' s')))
    ≡⟨ sum-R'-ext (λ r' → prf r') ⟩
      sum-R' (λ r' → sum-S' (λ s' → g (to (h r') s')))
    ≡⟨ sym (su-h (λ r' → sum-S' (λ s' → g (to r' s')))) ⟩
      sum-R' (λ r' → sum-S' (λ s' → g (to r' s')))
    ≡⟨ sym (sum-same g) ⟩
      sum-R g
    ∎
    where open ≡-Reasoning

import Function.Inverse.NP as Inv
open Inv using (_↔_) renaming (_$₁_ to to ; _$₂_ to from)

module with-iso {R R' S' : Set}(iso : R ↔ (R' × S'))(h : R' ↔ R') where

  open import Function.Related
  open import Data.Fin using (Fin)

  open import Function.Related.TypeIsomorphisms.NP

  principle : ∀ {f g} → (∀ r' → Σ S' (Fin ∘ f ∘ curry (from iso) r')
                              ↔ Σ S' (Fin ∘ g ∘ curry (from iso) (to h r')))
            → Σ R (Fin ∘ f) ↔ Σ R (Fin ∘ g)
  principle {f} {g} prf
    = Σ R (Fin ∘ f)
    ↔⟨ first-iso iso ⟩
      Σ (R' × S') (Fin ∘ f ∘ from iso)
    ↔⟨ Σ-assoc ⟩
      Σ R' (λ r' → Σ S' (λ s' → Fin (f (from iso (r' , s')))))
    ↔⟨ second-iso prf ⟩
      Σ R' (λ r' → Σ S' (λ s' → Fin (g (from iso (to h r' , s')))))
    ↔⟨ Inv.sym (first-iso (Inv.sym h)) ⟩
      Σ R' (λ r' → Σ S' (λ s' → Fin (g (from iso (r' , s')))))
    ↔⟨ Inv.sym Σ-assoc ⟩
      Σ (R' × S') (Fin ∘ g ∘ from iso)
    ↔⟨ Inv.sym (first-iso iso) ⟩
      Σ R (Fin ∘ g)
    ∎ where open EquationalReasoning

  module _ (sum-R : Sum R)(sum-S' : Sum S')(sum-R-adq : AdequateSum sum-R)(sum-S'-adq : AdequateSum sum-S') where
    cool : ∀ {f g} → (∀ r' → sum-S' (f ∘ curry (from iso) r')
                           ≡ sum-S' (g ∘ curry (from iso) (to h r')))
         → sum-R f ≡ sum-R g
    cool {f} {g} prf = Fin-injective (Inv.sym (sum-R-adq g)
                               Inv.∘ principle lemma
                               Inv.∘ sum-R-adq f)

     where
        open EquationalReasoning
        lemma : (_ : _) → _
        lemma r' = Σ S' (Fin ∘ f ∘ curry (from iso) r')
                 ↔⟨ Inv.sym (sum-S'-adq (f ∘ curry (from iso) r')) ⟩
                   Fin (sum-S' (f ∘ curry (from iso) r'))
                 ↔⟨ Fin-cong (prf r') ⟩
                   Fin (sum-S' (g ∘ curry (from iso) (to h r')))
                 ↔⟨ sum-S'-adq (g ∘ curry (from iso) (to h r')) ⟩
                   Σ S' (Fin ∘ g ∘ curry (from iso) (to h r'))
                 ∎


text:
-- ByteStrings where we track statically if they're lazy or strict
-- Note that lazy and strict bytestrings have the same semantics
-- in Agda, as all computation is guaranteed to terminate.
-- They may, however, have quite different performance characteristics.

open import Data.Bool using ( Bool )
open import Data.Nat using ( ℕ )
open import Data.Natural using ( Natural ; % )
open import Data.Product using ( _×_ ; _,_ )
open import Data.Word using ( Byte )
open import Data.String using ( String )
open import Data.ByteString.Primitive

module Data.ByteString where

open Data.ByteString.Primitive public using ( mkStrict ; mkLazy )

data Style : Set where
  lazy strict : Style

ByteString : Style → Set
ByteString strict = ByteStringStrict
ByteString lazy   = ByteStringLazy

ε : {s : Style} → (ByteString s)
ε {lazy}   = emptyLazy
ε {strict} = emptyStrict

_∙_ : {s : Style} → (ByteString s) → (ByteString s) → (ByteString s)
_∙_ {lazy}   = appendLazy
_∙_ {strict} = appendStrict

_◁_ : {s : Style} → Byte → (ByteString s) → (ByteString s)
_◁_ {lazy}   = consLazy
_◁_ {strict} = consStrict

_▷_ : {s : Style} → (ByteString s) → Byte → (ByteString s)
_▷_ {lazy}   = snocLazy
_▷_ {strict} = snocStrict

length : {s : Style} → (ByteString s) → Natural
length {lazy}   = lengthLazy
length {strict} = lengthStrict

size : {s : Style} → (ByteString s) → ℕ
size bs = %(length bs)

null : {s : Style} → (ByteString s) → Bool
null {lazy}   = nullLazy
null {strict} = nullStrict

span : {s : Style} → (Byte → Bool) → (ByteString s) → (ByteString s × ByteString s)
span {lazy}   φ bs with spanLazy φ bs
span {lazy}   φ bs | bs² = (lazy₁ bs² , lazy₂ bs²)
span {strict} φ bs with spanStrict φ bs
span {strict} φ bs | bs² = (strict₁ bs² , strict₂ bs²)

break : {s : Style} → (Byte → Bool) → (ByteString s) → (ByteString s × ByteString s)
break {lazy}   φ bs with breakLazy φ bs
break {lazy}   φ bs | bs² = (lazy₁ bs² , lazy₂ bs²)
break {strict} φ bs with breakStrict φ bs
break {strict} φ bs | bs² = (strict₁ bs² , strict₂ bs²)

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module BasicConcreteImplementations where

open import AbstractInterfaces public

-- Process identifiers.

instance
  ⟨P⟩ : IsProc
  ⟨P⟩ = record
          { Proc    = ℕ
          ; _≡ₚ?_   = _≡?_
          ; _<ₚ_    = _<_
          ; trans<ₚ = trans<
          ; tri<ₚ   = tri<
          }

-- Process clocks, message timestamps, and event timestamps.

instance
  ⟨T⟩ : IsTime
  ⟨T⟩ = record
          { Time      = ℕ
          ; _≡ₜ?_     = _≡?_
          ; _<ₜ_      = _<_
          ; trans<ₜ   = trans<
          ; tri<ₜ     = tri<
          ; irrefl<ₜ  = irrefl<
          ; sucₜ      = suc
          ; _⊔ₜ_      = _⊔_
          ; n<s[n⊔m]ₜ = n<s[n⊔m]
          }

-- Messages.

data BasicMsg : (Pᵢ Pⱼ : Proc) (Tₘ : Time) → Set where

instance
  ⟨M⟩ : IsMsg
  ⟨M⟩ = record
          { Msg = BasicMsg
          }

-- Events within one process.

data BasicEvent : Proc → Time → Set where
  send : ∀ {Cᵢ Pᵢ Pⱼ Tₘ} {{_ : Tₘ ≡ sucₜ Cᵢ}} →
         Msg Pᵢ Pⱼ Tₘ → BasicEvent Pᵢ Tₘ

  recv : ∀ {Cⱼ Pᵢ Pⱼ Tₘ Tⱼ} {{_ : Tⱼ ≡ sucₜ (Tₘ ⊔ₜ Cⱼ)}} →
         Msg Pᵢ Pⱼ Tₘ → BasicEvent Pⱼ Tⱼ

instance
  ⟨E⟩ : IsEvent
  ⟨E⟩ = record
          { Event   = BasicEvent
          ; isSendₑ = λ {Cᵢ} m a → a ≡ send {Cᵢ} m
          ; isRecvₑ = λ {Cⱼ} m a → a ≡ recv {Cⱼ} m
          ; absurdₑ = λ { {{refl}} (refl , ()) }
          }

max_stars_repo_name: mietek/lamport-timestamps

max_issues_repo_name: mietek/lamport-timestamps

max_forks_repo_name: mietek/lamport-timestamps


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import Sets.EquivalenceRelations

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Setoids.Orders.Total.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {c : _} {_<_ : A → A → Set c} {P : SetoidPartialOrder S _<_} (T : SetoidTotalOrder P) where

open SetoidTotalOrder T
open SetoidPartialOrder P
open Setoid S
open Equivalence eq

maxInequalitiesR : {a b c : A} → (a < b) → (a < c) → (a < max b c)
maxInequalitiesR {a} {b} {c} a<b a<c with totality b c
... | inl (inl x) = a<c
... | inl (inr x) = a<b
... | inr x = a<c

minInequalitiesR : {a b c : A} → (a < b) → (a < c) → (a < min b c)
minInequalitiesR {a} {b} {c} a<b a<c with totality b c
... | inl (inl x) = a<b
... | inl (inr x) = a<c
... | inr x = a<b

maxInequalitiesL : {a b c : A} → (a < c) → (b < c) → (max a b < c)
maxInequalitiesL {a} {b} {c} a<b a<c with totality a b
... | inl (inl x) = a<c
... | inl (inr x) = a<b
... | inr x = a<c

minInequalitiesL : {a b c : A} → (a < c) → (b < c) → (min a b < c)
minInequalitiesL {a} {b} {c} a<b a<c with totality a b
... | inl (inl x) = a<b
... | inl (inr x) = a<c
... | inr x = a<b

minLessL : (a b : A) → min a b <= a
minLessL a b with totality a b
... | inl (inl x) = inr reflexive
... | inl (inr x) = inl x
... | inr x = inr reflexive

minLessR : (a b : A) → min a b <= b
minLessR a b with totality a b
... | inl (inl x) = inl x
... | inl (inr x) = inr reflexive
... | inr x = inr x

maxGreaterL : (a b : A) → a <= max a b
maxGreaterL a b with totality a b
... | inl (inl x) = inl x
... | inl (inr x) = inr reflexive
... | inr x = inr x

maxGreaterR : (a b : A) → b <= max a b
maxGreaterR a b with totality a b
... | inl (inl x) = inr reflexive
... | inl (inr x) = inl x
... | inr x = inr reflexive


text:
-- {-# OPTIONS -v tc.lhs.shadow:30 #-}

module PatternShadowsConstructor3 where

data Bool : Set where
  true false : Bool

module A where

  data B : Set where
    x : B

  data C : Set where
    c : B → C

open A using (C; c)

T : Bool → Set
T true = C → C
T false = Bool

f : (b : Bool) → T b
f true (c x) = x
f false = true


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

open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.Commutes {i} (d : Span^2 {i}) where

open Span^2 d
open M using (Pushout^2)

open To d
open From d

open import homotopy.3x3.FromTo
open import homotopy.3x3.ToFrom

abstract
  theorem : Pushout^2 d ≃ Pushout^2 (transpose d)
  theorem = equiv to from (to-from d) (from-to d)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Data.ListSized.Proofs where

import      Lvl
open import Data.ListSized
open import Data.ListSized.Functions
open import Functional
open import Function.Equals
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Function
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A A₁ A₂ B B₁ B₂ C C₁ C₂ Result : Type{ℓ}
private variable a b n n₁ n₂ : ℕ
private variable f : B → C
private variable g : A → B
private variable l l₁ l₂ : List(T)(n)
private variable x : T

map-id : (map{A = A}{n = n} id ⊜ id)
_⊜_.proof map-id {∅}     = reflexivity(_≡_)
_⊜_.proof map-id {x ⊰ l} = congruence₂ᵣ(_⊰_)(_) (_⊜_.proof map-id {l})

map-[∘] : (map{n = n} (f ∘ g) ⊜ (map f) ∘ (map g))
_⊜_.proof map-[∘] {∅}     = reflexivity(_≡_)
_⊜_.proof map-[∘] {x ⊰ l} = congruence₂ᵣ(_⊰_)(_) (_⊜_.proof map-[∘] {l})

map-[++] : map f(l₁ ++ l₂) ≡ map f(l₁) ++ map f(l₂)
map-[++] {l₁ = ∅}       = reflexivity(_≡_)
map-[++] {l₁ = x₁ ⊰ l₁} = congruence₂ᵣ(_⊰_)(_) (map-[++] {l₁ = l₁})

map-repeat : map f(repeat x n) ≡ repeat (f(x)) n
map-repeat {n = 𝟎}   = reflexivity(_≡_)
map-repeat {n = 𝐒 n} = congruence₂ᵣ(_⊰_)(_) (map-repeat {n = n})

[+][++]-repeat : repeat x (n₁ + n₂) ≡ repeat x n₁ ++ repeat x n₂
[+][++]-repeat {n₁ = 𝟎}    = reflexivity(_≡_)
[+][++]-repeat {n₁ = 𝐒 n₁} = congruence₂ᵣ(_⊰_)(_) ([+][++]-repeat {n₁ = n₁})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module functions where

open import level
open import eq
open import product

{- Note that the Agda standard library has an interesting generalization
   of the following basic composition operator, with more dependent typing. -}

_∘_ : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''} →
      (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

∘-assoc : ∀{ℓ ℓ' ℓ'' ℓ'''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{D : Set ℓ'''}
           (f : C → D)(g : B → C)(h : A → B) → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
∘-assoc f g h = refl

id : ∀{ℓ}{A : Set ℓ} → A → A
id x = x

∘-id : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(f : A → B) → f ∘ id ≡ f
∘-id f = refl

id-∘ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(f : A → B) → id ∘ f ≡ f
id-∘ f = refl

extensionality : {ℓ₁ ℓ₂ : Level} → Set (lsuc ℓ₁ ⊔ lsuc ℓ₂)
extensionality {ℓ₁}{ℓ₂} = ∀{A : Set ℓ₁}{B : Set ℓ₂}{f g : A → B} → (∀{a : A} → f a ≡ g a) → f ≡ g

record Iso {ℓ₁ ℓ₂ : Level} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
 constructor isIso
 field
   l-inv : A → B
   r-inv : B → A
   l-cancel : r-inv ∘ l-inv ≡ id
   r-cancel : l-inv ∘ r-inv ≡ id

curry : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃} → ((A × B) → C) → (A → B → C)
curry f x y = f (x , y)

uncurry : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃} → (A → B → C) → ((A × B) → C)
uncurry f (x , y) = f x y

compose-cong : ∀{ℓ}{A : Set ℓ}{B : Set ℓ}{C : Set ℓ}{f f' : A → B}{g g' : B → C} → f ≡ f' → g ≡ g' → g ∘ f ≡ g' ∘ f'
compose-cong refl refl = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 06-universes where

import 05-identity-types
open 05-identity-types public

-- Section 6.3 Pointed types

-- Definition 6.3.1

UU-pt : (i : Level) → UU (lsuc i)
UU-pt i = Σ (UU i) (λ X → X)

type-UU-pt : {i : Level} → UU-pt i → UU i
type-UU-pt = pr1

pt-UU-pt : {i : Level} (A : UU-pt i) → type-UU-pt A
pt-UU-pt = pr2

-- Definition 6.3.2

_→*_ : {i j : Level} → UU-pt i → UU-pt j → UU-pt (i ⊔ j)
A →* B =
  pair
    ( Σ (type-UU-pt A → type-UU-pt B) (λ f → Id (f (pt-UU-pt A)) (pt-UU-pt B)))
    ( pair
      ( const (type-UU-pt A) (type-UU-pt B) (pt-UU-pt B))
      ( refl))

-- Definition 6.3.3

Ω : {i : Level} → UU-pt i → UU-pt i
Ω A = pair (Id (pt-UU-pt A) (pt-UU-pt A)) refl

-- Definition 6.3.4

iterated-loop-space : {i : Level} → ℕ → UU-pt i → UU-pt i
iterated-loop-space zero-ℕ A = A
iterated-loop-space (succ-ℕ n) A = Ω (iterated-loop-space n A)

-- Section 6.4 Families and relations on the natural numbers

-- Definition 6.4.1

Fin : ℕ → UU lzero
Fin zero-ℕ = empty
Fin (succ-ℕ n) = coprod (Fin n) unit

-- Definition 6.4.2

-- Observational equality on the natural numbers

Eq-ℕ : ℕ → (ℕ → UU lzero)
Eq-ℕ zero-ℕ zero-ℕ = 𝟙
Eq-ℕ zero-ℕ (succ-ℕ n) = 𝟘
Eq-ℕ (succ-ℕ m) zero-ℕ = 𝟘
Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n

-- Lemma 6.4.3

refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
refl-Eq-ℕ zero-ℕ = star
refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n

succ-relation-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) → ℕ → ℕ → UU i
succ-relation-ℕ R m n = R (succ-ℕ m) (succ-ℕ n)

succ-reflexivity-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) →
  (n : ℕ) → succ-relation-ℕ R n n
succ-reflexivity-ℕ R ρ n = ρ (succ-ℕ n)

{- In the book we suggest that first the order of the variables should be
   swapped, in order to make the inductive hypothesis stronger. Agda's pattern
   matching mechanism allows us to bypass this step and give a more direct
   construction. -}

least-reflexive-Eq-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) →
  (m n : ℕ) → Eq-ℕ m n → R m n
least-reflexive-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
least-reflexive-Eq-ℕ R ρ zero-ℕ (succ-ℕ n) ()
least-reflexive-Eq-ℕ R ρ (succ-ℕ m) zero-ℕ ()
least-reflexive-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  least-reflexive-Eq-ℕ (succ-relation-ℕ R) (succ-reflexivity-ℕ R ρ) m n e

-- Exercises

-- Exercise 6.1

{- In this exercise we were asked to show that the observational equality on ℕ
   is an equivalence relation. -}

symmetric-Eq-ℕ : (m n : ℕ) → Eq-ℕ m n → Eq-ℕ n m
symmetric-Eq-ℕ zero-ℕ zero-ℕ star = star
symmetric-Eq-ℕ (succ-ℕ m) (succ-ℕ n) t = symmetric-Eq-ℕ m n t

transitive-Eq-ℕ : (l m n : ℕ) → Eq-ℕ l m → Eq-ℕ m n → Eq-ℕ l n
transitive-Eq-ℕ zero-ℕ zero-ℕ zero-ℕ p q = star
transitive-Eq-ℕ (succ-ℕ l) (succ-ℕ m) (succ-ℕ n) p q =
  transitive-Eq-ℕ l m n p q

-- Exercise 6.2

{- In this exercise we were asked to show that any function on the natural
   numbers preserves observational equality. The quick solution uses the fact
   that observational equality is the least reflexive relation. -}

preserve_Eq-ℕ : (f : ℕ → ℕ) (n m : ℕ) → (Eq-ℕ n m) → (Eq-ℕ (f n) (f m))
preserve_Eq-ℕ f =
  least-reflexive-Eq-ℕ
    ( λ x y → Eq-ℕ (f x) (f y))
    ( λ x → refl-Eq-ℕ (f x))

-- Exercise 6.3

{- In this exercise we were asked to construct the relations ≤ and < on the
   natural numbers, and show basic properties about them. -}

-- Exercise 6.3(a)

-- The definition of ≤

leq-ℕ : ℕ → ℕ → UU lzero
leq-ℕ zero-ℕ m = unit
leq-ℕ (succ-ℕ n) zero-ℕ = empty
leq-ℕ (succ-ℕ n) (succ-ℕ m) = leq-ℕ n m

_≤_ = leq-ℕ

leq-zero-ℕ :
  (n : ℕ) → leq-ℕ zero-ℕ n
leq-zero-ℕ n = star

-- The definition of <

le-ℕ : ℕ → ℕ → UU lzero
le-ℕ m zero-ℕ = empty
le-ℕ zero-ℕ (succ-ℕ m) = unit
le-ℕ (succ-ℕ n) (succ-ℕ m) = le-ℕ n m

_<_ = le-ℕ

reflexive-leq-ℕ : (n : ℕ) → n ≤ n
reflexive-leq-ℕ zero-ℕ = star
reflexive-leq-ℕ (succ-ℕ n) = reflexive-leq-ℕ n

anti-reflexive-le-ℕ : (n : ℕ) → ¬ (n < n)
anti-reflexive-le-ℕ zero-ℕ = ind-empty
anti-reflexive-le-ℕ (succ-ℕ n) = anti-reflexive-le-ℕ n

transitive-leq-ℕ :
  (n m l : ℕ) → (n ≤ m) → (m ≤ l) → (n ≤ l)
transitive-leq-ℕ zero-ℕ m l p q = star
transitive-leq-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-leq-ℕ n m l p q

transitive-le-ℕ : (n m l : ℕ) → (le-ℕ n m) → (le-ℕ m l) → (le-ℕ n l)
transitive-le-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ l) p q = star
transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-le-ℕ n m l p q

succ-leq-ℕ : (n : ℕ) → leq-ℕ n (succ-ℕ n)
succ-leq-ℕ zero-ℕ = star
succ-leq-ℕ (succ-ℕ n) = succ-leq-ℕ n

succ-le-ℕ : (n : ℕ) → le-ℕ n (succ-ℕ n)
succ-le-ℕ zero-ℕ = star
succ-le-ℕ (succ-ℕ n) = succ-le-ℕ n

anti-symmetric-leq-ℕ : (m n : ℕ) → leq-ℕ m n → leq-ℕ n m → Id m n
anti-symmetric-leq-ℕ zero-ℕ zero-ℕ p q = refl
anti-symmetric-leq-ℕ (succ-ℕ m) (succ-ℕ n) p q =
  ap succ-ℕ (anti-symmetric-leq-ℕ m n p q)

anti-symmetric-le-ℕ : (m n : ℕ) → le-ℕ m n → le-ℕ n m → Id m n
anti-symmetric-le-ℕ (succ-ℕ m) (succ-ℕ n) p q =
  ap succ-ℕ (anti-symmetric-le-ℕ m n p q)

-- Exercise 6.5

{- In this exercise we were asked to construct observational equality on the
   booleans. This construction is analogous to, but simpler than, the
   construction of observational equality on the natural numbers. -}

Eq-𝟚 : bool → bool → UU lzero
Eq-𝟚 true true = unit
Eq-𝟚 true false = empty
Eq-𝟚 false true = empty
Eq-𝟚 false false = unit

reflexive-Eq-𝟚 : (x : bool) → Eq-𝟚 x x
reflexive-Eq-𝟚 true = star
reflexive-Eq-𝟚 false = star

least-reflexive-Eq-𝟚 : {i : Level}
  (R : bool → bool → UU i) (ρ : (x : bool) → R x x)
  (x y : bool) → Eq-𝟚 x y → R x y
least-reflexive-Eq-𝟚 R ρ true true p = ρ true
least-reflexive-Eq-𝟚 R ρ true false p = ind-empty p
least-reflexive-Eq-𝟚 R ρ false true p = ind-empty p
least-reflexive-Eq-𝟚 R ρ false false p = ρ false

-- Exercise 6.6

{- In this exercise we were asked to define the relations ≤ and < on the
   integers. As a criterion of correctness, we were then also asked to show
   that the type of all integers l satisfying k ≤ l satisfy the induction
   principle of the natural numbers. -}

diff-ℤ : ℤ → ℤ → ℤ
diff-ℤ k l = add-ℤ (neg-ℤ k) l

is-non-negative-ℤ : ℤ → UU lzero
is-non-negative-ℤ (inl x) = empty
is-non-negative-ℤ (inr k) = unit

leq-ℤ : ℤ → ℤ → UU lzero
leq-ℤ k l = is-non-negative-ℤ (diff-ℤ k l)

reflexive-leq-ℤ : (k : ℤ) → leq-ℤ k k
reflexive-leq-ℤ k =
  tr is-non-negative-ℤ (inv (left-inverse-law-add-ℤ k)) star

is-non-negative-succ-ℤ :
  (k : ℤ) → is-non-negative-ℤ k → is-non-negative-ℤ (succ-ℤ k)
is-non-negative-succ-ℤ (inr (inl star)) p = star
is-non-negative-succ-ℤ (inr (inr x)) p = star

is-non-negative-add-ℤ :
  (k l : ℤ) →
  is-non-negative-ℤ k → is-non-negative-ℤ l → is-non-negative-ℤ (add-ℤ k l)
is-non-negative-add-ℤ (inr (inl star)) (inr (inl star)) p q = star
is-non-negative-add-ℤ (inr (inl star)) (inr (inr n)) p q = star
is-non-negative-add-ℤ (inr (inr zero-ℕ)) (inr (inl star)) p q = star
is-non-negative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inl star)) star star =
  is-non-negative-succ-ℤ
    ( add-ℤ (inr (inr n)) (inr (inl star)))
    ( is-non-negative-add-ℤ (inr (inr n)) (inr (inl star)) star star)
is-non-negative-add-ℤ (inr (inr zero-ℕ)) (inr (inr m)) star star = star
is-non-negative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inr m)) star star =
  is-non-negative-succ-ℤ
    ( add-ℤ (inr (inr n)) (inr (inr m)))
    ( is-non-negative-add-ℤ (inr (inr n)) (inr (inr m)) star star)

triangle-diff-ℤ :
  (k l m : ℤ) → Id (add-ℤ (diff-ℤ k l) (diff-ℤ l m)) (diff-ℤ k m)
triangle-diff-ℤ k l m =
  ( associative-add-ℤ (neg-ℤ k) l (diff-ℤ l m)) ∙
  ( ap
    ( add-ℤ (neg-ℤ k))
    ( ( inv (associative-add-ℤ l (neg-ℤ l) m)) ∙
      ( ( ap (λ x → add-ℤ x m) (right-inverse-law-add-ℤ l)) ∙
        ( left-unit-law-add-ℤ m))))

transitive-leq-ℤ : (k l m : ℤ) → leq-ℤ k l → leq-ℤ l m → leq-ℤ k m
transitive-leq-ℤ k l m p q =
  tr is-non-negative-ℤ
    ( triangle-diff-ℤ k l m)
    ( is-non-negative-add-ℤ
      ( add-ℤ (neg-ℤ k) l)
      ( add-ℤ (neg-ℤ l) m)
      ( p)
      ( q))

succ-leq-ℤ : (k : ℤ) → leq-ℤ k (succ-ℤ k)
succ-leq-ℤ k =
  tr is-non-negative-ℤ
    ( inv
      ( ( right-successor-law-add-ℤ (neg-ℤ k) k) ∙
        ( ap succ-ℤ (left-inverse-law-add-ℤ k))))
    ( star)

leq-ℤ-succ-leq-ℤ : (k l : ℤ) → leq-ℤ k l → leq-ℤ k (succ-ℤ l)
leq-ℤ-succ-leq-ℤ k l p = transitive-leq-ℤ k l (succ-ℤ l) p (succ-leq-ℤ l)

is-positive-ℤ : ℤ → UU lzero
is-positive-ℤ k = is-non-negative-ℤ (pred-ℤ k)

le-ℤ : ℤ → ℤ → UU lzero
le-ℤ (inl zero-ℕ) (inl x) = empty
le-ℤ (inl zero-ℕ) (inr y) = unit
le-ℤ (inl (succ-ℕ x)) (inl zero-ℕ) = unit
le-ℤ (inl (succ-ℕ x)) (inl (succ-ℕ y)) = le-ℤ (inl x) (inl y)
le-ℤ (inl (succ-ℕ x)) (inr y) = unit
le-ℤ (inr x) (inl y) = empty
le-ℤ (inr (inl star)) (inr (inl star)) = empty
le-ℤ (inr (inl star)) (inr (inr x)) = unit
le-ℤ (inr (inr x)) (inr (inl star)) = empty
le-ℤ (inr (inr zero-ℕ)) (inr (inr zero-ℕ)) = empty
le-ℤ (inr (inr zero-ℕ)) (inr (inr (succ-ℕ y))) = unit
le-ℤ (inr (inr (succ-ℕ x))) (inr (inr zero-ℕ)) = empty
le-ℤ (inr (inr (succ-ℕ x))) (inr (inr (succ-ℕ y))) =
  le-ℤ (inr (inr x)) (inr (inr y))

-- Extra material

-- We show that ℕ is an ordered semi-ring

leq-eq-ℕ : {m m' n n' : ℕ} → Id m m' → Id n n' → leq-ℕ m n → leq-ℕ m' n'
leq-eq-ℕ refl refl = id

left-law-leq-add-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ m k) (add-ℕ n k)
left-law-leq-add-ℕ zero-ℕ m n = id
left-law-leq-add-ℕ (succ-ℕ k) m n H = left-law-leq-add-ℕ k m n H

right-law-leq-add-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ k m) (add-ℕ k n)
right-law-leq-add-ℕ k m n H =
  leq-eq-ℕ
    ( commutative-add-ℕ m k)
    ( commutative-add-ℕ n k)
    ( left-law-leq-add-ℕ k m n H)

preserves-leq-add-ℕ :
  {m m' n n' : ℕ} → leq-ℕ m m' → leq-ℕ n n' → leq-ℕ (add-ℕ m n) (add-ℕ m' n')
preserves-leq-add-ℕ {m} {m'} {n} {n'} H K =
  transitive-leq-ℕ
    ( add-ℕ m n)
    ( add-ℕ m' n)
    ( add-ℕ m' n')
    ( left-law-leq-add-ℕ n m m' H)
    ( right-law-leq-add-ℕ m' n n' K)

right-law-leq-mul-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ k m) (mul-ℕ k n)
right-law-leq-mul-ℕ zero-ℕ m n H = star
right-law-leq-mul-ℕ (succ-ℕ k) m n H = {!!}

{-
  preserves-leq-add-ℕ
    { m = mul-ℕ k m}
    { m' = mul-ℕ k n}
    ( right-law-leq-mul-ℕ k m n H) H

left-law-leq-mul-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ m k) (mul-ℕ n k)
left-law-leq-mul-ℕ k m n H =
  leq-eq-ℕ
    ( commutative-mul-ℕ k m)
    ( commutative-mul-ℕ k n)
    ( right-law-leq-mul-ℕ k m n H)

-- We show that ℤ is an ordered ring

{-
leq-add-ℤ : (m k l : ℤ) → leq-ℤ k l → leq-ℤ (add-ℤ m k) (add-ℤ m l)
leq-add-ℤ (inl zero-ℕ) k l H = {!!}
leq-add-ℤ (inl (succ-ℕ x)) k l H = {!!}
leq-add-ℤ (inr m) k l H = {!!}
-}

-- Section 5.5 Identity systems

succ-fam-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i) →
  (m n : ℕ) → Eq-ℕ m n → UU i
succ-fam-Eq-ℕ R m n e = R (succ-ℕ m) (succ-ℕ n) e

succ-refl-fam-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  (ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  (n : ℕ) → (succ-fam-Eq-ℕ R n n (refl-Eq-ℕ n))
succ-refl-fam-Eq-ℕ R ρ n = ρ (succ-ℕ n)

path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( m n : ℕ) (e : Eq-ℕ m n) → R m n e
path-ind-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
path-ind-Eq-ℕ R ρ zero-ℕ (succ-ℕ n) ()
path-ind-Eq-ℕ R ρ (succ-ℕ m) zero-ℕ ()
path-ind-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  path-ind-Eq-ℕ (succ-fam-Eq-ℕ R) (succ-refl-fam-Eq-ℕ R ρ) m n e

comp-path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( n : ℕ) → Id (path-ind-Eq-ℕ R ρ n n (refl-Eq-ℕ n)) (ρ n)
comp-path-ind-Eq-ℕ R ρ zero-ℕ = refl
comp-path-ind-Eq-ℕ R ρ (succ-ℕ n) =
  comp-path-ind-Eq-ℕ (succ-fam-Eq-ℕ R) (succ-refl-fam-Eq-ℕ R ρ) n
-}

{-
-- Graphs
Gph : (i : Level) → UU (lsuc i)
Gph i = Σ (UU i) (λ X → (X → X → (UU i)))

-- Reflexive graphs
rGph : (i : Level) →  UU (lsuc i)
rGph i = Σ (UU i) (λ X → Σ (X → X → (UU i)) (λ R → (x : X) → R x x))
-}

-- Exercise 3.7

{- With the construction of the divisibility relation we open the door to basic
   number theory. -}

divides : (d n : ℕ) → UU lzero
divides d n = Σ ℕ (λ m → Eq-ℕ (mul-ℕ d m) n)

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module PatternSynonymMutualBlock where

data D : Set where
  c : D

mutual
  pattern p = c

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda