text:
module lambdasyntax where

open import Data.Nat using (ℕ)
open import Data.Bool using (Bool; true; false)
open import Data.Vec using (Vec; []; lookup)
open import Relation.Nullary
open import Data.Empty hiding (⊥)
open import Relation.Binary.PropositionalEquality

data Label : Set where
    ⊤ ⊥ ✭ : Label

data GType : Set where
    bool : Label → GType
    _⇒_  : GType → Label → GType → GType
    err  : GType

infixr 4 _∙_
infixl 6 _∨_ _∧_
data Term : Set where
    var           : ℕ → Term
    litBool       : Bool → Label → Term
    lam           : GType → Term → Label → Term
    _∧_           : Term → Term → Term
    _∨_           : Term → Term → Term
    _∙_           : Term → Term → Term
    if_then_else_ : Term → Term → Term → Term
    error         : Term

Ctx : ℕ → Set
Ctx = Vec GType

getLabel : GType → Label
getLabel (bool ℓ) = ℓ
getLabel ((g ⇒ ℓ) g₁) = ℓ
getLabel err = ✭ -- lazy propagation

setLabel : GType → Label → GType
setLabel (bool _) ℓ = bool ℓ
setLabel ((t ⇒ x) t₁) ℓ = (t ⇒ ℓ) t₁
setLabel err _ = err

-- gradual join
_~⋎~_ : (ℓ₁ ℓ₂ : Label) → Label
⊤ ~⋎~ ⊤ = ⊤
⊤ ~⋎~ ⊥ = ⊤
⊤ ~⋎~ ✭ = ⊤
⊥ ~⋎~ ⊤ = ⊤
⊥ ~⋎~ ⊥ = ⊥
⊥ ~⋎~ ✭ = ✭
✭ ~⋎~ ⊤ = ⊤
✭ ~⋎~ ⊥ = ✭
✭ ~⋎~ ✭ = ✭

-- gradual meet
_~⋏~_ : ∀ (ℓ₁ ℓ₂ : Label) → Label
⊥ ~⋏~ ✭ = ⊥
✭ ~⋏~ ⊥ = ⊥
ℓ₁ ~⋏~ ✭ = ✭
✭ ~⋏~ ℓ₂ = ✭
⊤ ~⋏~ ⊤ = ⊤
⊤ ~⋏~ ⊥ = ⊥
⊥ ~⋏~ ⊤ = ⊥
⊥ ~⋏~ ⊥ = ⊥

_:∧:_ : ∀ (t₁ t₂ : GType) → GType
_:∨:_ : ∀ (t₁ t₂ : GType) → GType
bool ℓ₁ :∧: bool ℓ₂ = bool (ℓ₁ ~⋏~ ℓ₂)
(s₁₁ ⇒ ℓ₁) s₁₂ :∧: (s₂₁ ⇒ ℓ₂) s₂₂ = ((s₁₁ :∨: s₂₁) ⇒ (ℓ₁ ~⋏~ ℓ₂)) (s₁₂ :∧: s₂₂)
_ :∧: _ = err
-- _:∨:_ : ∀ (t₁ t₂ : gtype) → gtype
bool ℓ₁ :∨: bool ℓ₂ = bool (ℓ₁ ~⋎~ ℓ₂)
(s₁₁ ⇒ ℓ₁) s₁₂ :∨: (s₂₁ ⇒ ℓ₂) s₂₂ = ((s₁₁ :∧: s₂₁) ⇒ (ℓ₁ ~⋎~ ℓ₂)) (s₁₂ :∨: s₂₂)
_ :∨: _ = err

data _≤_ : Label → Label → Set where
    ⊥≤⊤ : ⊥ ≤ ⊤
    ⊤≤⊤ : ⊤ ≤ ⊤
    ⊥≤⊥ : ⊥ ≤ ⊥
    ℓ≤✭ : ∀ {ℓ} → ℓ ≤ ✭
    ✭≤ℓ : ∀ {ℓ} → ✭ ≤ ℓ

_≤?_ : (ℓ₁ ℓ₂ : Label) → Dec (ℓ₁ ≤ ℓ₂)
⊤ ≤? ⊤ = yes ⊤≤⊤
⊤ ≤? ⊥ = no (λ ())
⊤ ≤? ✭ = yes (ℓ≤✭)
⊥ ≤? ⊤ = yes ⊥≤⊤
⊥ ≤? ⊥ = yes ⊥≤⊥
⊥ ≤? ✭ = yes (ℓ≤✭)
✭ ≤? ⊤ = yes (✭≤ℓ)
✭ ≤? ⊥ = yes (✭≤ℓ)
✭ ≤? ✭ = yes (ℓ≤✭)

data _≾_ : GType → GType → Set where
    yes : (t₁ t₂ : GType) → t₁ ≾ t₂
    no  : (t₁ t₂ : GType) → t₁ ≾ t₂

_≾?_ : (t₁ t₂ : GType) → t₁ ≾ t₂
bool ℓ ≾? bool ℓ₁ with ℓ ≤? ℓ₁
...      | yes p = yes (bool ℓ) (bool ℓ₁)
...      | no ¬p = no (bool ℓ) (bool ℓ₁)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ with t₃ ≾? t₁ | t₂ ≾? t₄ | ℓ ≤? ℓ₁
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | yes .t₃ .t₁ | (yes .t₂ .t₄) | (yes p) = yes ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)

(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | yes .t₃ .t₁ | (yes .t₂ .t₄) | (no ¬p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | yes .t₃ .t₁ | (no .t₂ .t₄) | (yes p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | yes .t₃ .t₁ | (no .t₂ .t₄) | (no ¬p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | no .t₃ .t₁ | (yes .t₂ .t₄) | (yes p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | no .t₃ .t₁ | (yes .t₂ .t₄) | (no ¬p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | no .t₃ .t₁ | (no .t₂ .t₄) | (yes p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)
(t₁ ⇒ ℓ) t₂ ≾? (t₃ ⇒ ℓ₁) t₄ | no .t₃ .t₁ | (no .t₂ .t₄) | (no ¬p) = no ((t₁ ⇒ ℓ) t₂) ((t₃ ⇒ ℓ₁) t₄)

-- everything else is no
t₁ ≾? t₂ = no t₁ t₂

max_stars_repo_path: Agda/Gradual Security/lambdasyntax.agda

max_stars_repo_name: kellino/TypeSystems

max_issues_repo_path: Agda/Gradual Security/lambdasyntax.agda

max_issues_repo_name: kellino/TypeSystems

max_forks_repo_path: Agda/Gradual Security/lambdasyntax.agda

max_forks_repo_name: kellino/TypeSystems


text:
module examplesPaperJFP.StackBisim where

open import Data.Product
open import Function
open import Data.Nat.Base as N
open import Data.Vec as Vec using (Vec; []; _∷_; head; tail)

open import Relation.Binary.PropositionalEquality

open import examplesPaperJFP.StatefulObject

module _ {S : Set} {M : S → Set}  {R : (s : S)  →  (m : M s)  →  Set} {next : (s : S)  →  (m : M s)  →  R s m → S} (let

  I  = record { Stateˢ = S; Methodˢ = M; Resultˢ = R; nextˢ = next }
 ) (let
  O = Objectˢ I

    ) where
module Bisim (I : Interfaceˢ)
  (let S    = Stateˢ  I)
  (let M    = Methodˢ I)
  (let R    = Resultˢ I)
  (let next = nextˢ I)
  (let O    = Objectˢ I) where

  data  ΣR     {A : Set} {B : A → Set} (R : ∀{a} (b b′ : B a) → Set)
               :  (p p′ : Σ[ a ∈ A ] B a) → Set
        where
        eqΣ    :  ∀{a}{b b′ : B a} → R b b′ → ΣR R (a , b) (a , b′)

  record _≅_ {s : S} (o o′ : O s) : Set where
    coinductive
    field  bisimMethod  :  (m : M s) →
                           ΣR (_≅_) (objectMethod o m) (objectMethod o′ m)

  open _≅_ public

  refl≅ :  ∀{s} (o : O s) → o ≅ o
  bisimMethod (refl≅ o) m  =  let  (r , o′) =  objectMethod o m
                              in   eqΣ (refl≅ o′)

module _ {E : Set} where
  private
    I = StackInterfaceˢ E
    S = Stateˢ I
    O = Objectˢ I
  open Bisim I

  pop-after-push : ∀{n} {v : Vec E n} {e : E} →
    let  st          =  stack v
         (_ , st₁)   =  objectMethod  st   (push e)
         (e₂ , st₂)  =  objectMethod  st₁  pop

    in   (e ≡ e₂) × (st ≅ st₂)

  pop-after-push = refl , refl≅ _

  push-after-pop : ∀{n} {v : Vec E n} {e : E} →
    let  st            =  stack (e ∷ v)
         (e₁  ,  st₁)  =  objectMethod st   pop
         (_   ,  st₂)  =  objectMethod st₁  (push e₁)

    in   st ≅ st₂

  push-after-pop = refl≅ _

  tabulate  :  ∀ (n : ℕ) (f : ℕ → E) → Vec E n
  tabulate  0        f  =  []
  tabulate  (suc n)  f  =  f 0 ∷ tabulate n (f ∘ suc)

  stackF : ∀ (n : ℕ) (f : ℕ → E) → Objectˢ (StackInterfaceˢ E) n
  objectMethod  (stackF  n        f) (push e)  =  _    ,  stackF (suc n) λ
    {  0        →  e
    ;  (suc m)  →  f m    }
  objectMethod  (stackF  (suc n)  f) pop       =  f 0  ,  stackF n (f  ∘ suc)

  impl-bisim : ∀{n f} v (p : tabulate n f ≡ v) → stackF n f ≅ stack v

  bisimMethod (impl-bisim v        p) (push e) =
    eqΣ (impl-bisim (e ∷ v)  (cong (_∷_ e)  p))

  bisimMethod (impl-bisim (e ∷ v)  p) pop rewrite cong head p =
    eqΣ (impl-bisim v        (cong tail     p))

ext: agda

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module STLC.Semantics where

-- This file contains the definitional interpreter for STLC described
-- in Section 2 of the paper.

open import Data.Nat
open import Data.Integer
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.Maybe.Base hiding (_>>=_)

------------
-- SYNTAX --
------------

-- These definitions correspond to Section 2.1, except we have
-- included numbers (integers) and integer operations in the language.

data Ty : Set where
  unit : Ty
  _⇒_  : (a b : Ty) → Ty
  int  : Ty

Ctx = List Ty

-- Below, `Expr` uses `_∈_` from `Relation.Binary` in the Agda
-- Standard Library to represent typed de Bruijn indices which witness
-- the existence of an entry in the type context.

data Expr (Γ : Ctx) : Ty → Set where
  unit  : Expr Γ unit
  var   : ∀ {t} → t ∈ Γ → Expr Γ t
  ƛ     : ∀ {a b} → Expr (a ∷ Γ) b → Expr Γ (a ⇒ b)
  _·_   : ∀ {a b} → Expr Γ (a ⇒ b) → Expr Γ a → Expr Γ b
  num   : ℤ → Expr Γ int
  iop   : (ℤ → ℤ → ℤ) → (l r : Expr Γ int) → Expr Γ int

-----------------------------
-- VALUES AND ENVIRONMENTS --
-----------------------------

-- These definitions correspond to Section 2.2.
--
-- Note that the `All` type described in Section 2.2 of the paper (for
-- simplicity) does not mention universe levels, whereas the `All`
-- definition below refers to `Data.List.All` in the Agda Standard
-- Library which is defined in a universe polymorphic manner.

mutual
  data Val : Ty → Set where
    unit  : Val unit
    ⟨_,_⟩ : ∀ {Γ a b} → Expr (a ∷ Γ) b → Env Γ → Val (a ⇒ b)
    num   : ℤ → Val int

  Env : Ctx → Set
  Env Γ = All Val Γ

-- The `lookup` function described in Section 2.2 of the paper is also
-- defined in `Data.List.All` in the Agda Standard Library.

-----------
-- MONAD --
-----------

-- These definitions correspond to Section 2.3.

M : Ctx → Set → Set
M Γ a  =  Env Γ → Maybe a

_>>=_    : ∀ {Γ a b} → M Γ a → (a → M Γ b) → M Γ b
(f >>= c) E with (f E)
... | just x = c x E
... | nothing = nothing

return   : ∀ {Γ a} → a → M Γ a
return x E = just x

getEnv   : ∀ {Γ} → M Γ (Env Γ)
getEnv E = return E E

usingEnv : ∀ {Γ Γ' a} → Env Γ → M Γ a → M Γ' a
usingEnv E f _ = f E

timeout  : ∀ {Γ a} → M Γ a
timeout = λ _ → nothing

-----------------
-- INTERPRETER --
-----------------

-- These definitions correspond to Section 2.4.

eval : ℕ → ∀ {Γ t} → Expr Γ t → M Γ (Val t)
eval zero     _           =
  timeout
eval (suc k)  unit        =
  return unit
eval (suc k)  (var x)     =
  getEnv >>= λ E →
  return (All.lookup E x)
eval (suc k)  (ƛ b)       =
  getEnv >>= λ E →
  return ⟨ b , E ⟩
eval (suc k)  (l · r)     =
  eval k l >>= λ{ ⟨ e , E ⟩ →
  eval k r >>= λ v →
  usingEnv (v ∷ E) (eval k e) }
eval (suc k)  (num x)     =
  return (num x)
eval (suc k)  (iop f l r) =
  eval k l >>= λ{ (num vₗ) →
  eval k r >>= λ{ (num vᵣ) →
  return (num (f vₗ vᵣ)) }}


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

open import Categories.Adjoint
open import Categories.Category
open import Categories.Functor renaming (id to idF)

-- The crude monadicity theorem. This proof is based off of the version
-- provided in "Sheaves In Geometry and Logic" by Maclane and Moerdijk.
module Categories.Adjoint.Monadic.Crude {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
                                        {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where

open import Level
open import Function using (_$_)
open import Data.Product using (Σ-syntax; _,_)

open import Categories.Adjoint.Properties
open import Categories.Adjoint.Monadic
open import Categories.Adjoint.Monadic.Properties
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Category.Equivalence.Properties using (pointwise-iso-equivalence)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.NaturalTransformation
open import Categories.Monad

open import Categories.Diagram.Coequalizer
open import Categories.Diagram.ReflexivePair

open import Categories.Adjoint.Construction.EilenbergMoore
open import Categories.Category.Construction.EilenbergMoore
open import Categories.Category.Construction.Properties.EilenbergMoore

open import Categories.Morphism
open import Categories.Morphism.Notation
open import Categories.Morphism.Properties
import Categories.Morphism.Reasoning as MR

private
  module L = Functor L
  module R = Functor R

  module 𝒞 = Category 𝒞
  module 𝒟 = Category 𝒟

  module adjoint = Adjoint adjoint

  T : Monad 𝒞
  T = adjoint⇒monad adjoint

  𝒞ᵀ : Category _ _ _
  𝒞ᵀ = EilenbergMoore T

  Comparison : Functor 𝒟 𝒞ᵀ
  Comparison = ComparisonF adjoint

  module Comparison = Functor Comparison

  open Coequalizer

-- We could do this with limits, but this is far easier.
PreservesReflexiveCoequalizers : (F : Functor 𝒟 𝒞) → Set _
PreservesReflexiveCoequalizers F = ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → (coeq : Coequalizer 𝒟 f g) → IsCoequalizer 𝒞 (F.F₁ f) (F.F₁ g) (F.F₁ (arr coeq))
  where
    module F = Functor F

module _ {F : Functor 𝒟 𝒞} (preserves-reflexive-coeq : PreservesReflexiveCoequalizers F) where
  open Functor F

  -- Unfortunately, we need to prove that the 'coequalize' arrows are equal as a lemma
  preserves-coequalizer-unique : ∀ {A B C} {f g : 𝒟 [ A , B ]} {h : 𝒟 [ B , C ]} {eq : 𝒟 [ 𝒟 [ h ∘ f ] ≈ 𝒟 [ h ∘ g ] ]}
                                 → (reflexive-pair : ReflexivePair 𝒟 f g) → (coe : Coequalizer 𝒟 f g)
                                 →  𝒞 [ F₁ (coequalize coe eq) ≈ IsCoequalizer.coequalize (preserves-reflexive-coeq reflexive-pair coe) ([ F ]-resp-square eq) ]
  preserves-coequalizer-unique reflexive-pair coe = IsCoequalizer.unique (preserves-reflexive-coeq reflexive-pair coe) (F-resp-≈ (universal coe) ○ homomorphism)
    where
      open 𝒞.HomReasoning

-- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint.
module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where

  private
    reflexive-pair : (M : Module T) → ReflexivePair 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))
    reflexive-pair M = record
      { s = L.F₁ (adjoint.unit.η (Module.A M))
      ; isReflexivePair = record
        { sectionₗ = begin
          𝒟 [ L.F₁ (Module.action M) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈˘⟨ L.homomorphism ⟩
          L.F₁ (𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] )       ≈⟨ L.F-resp-≈ (Module.identity M) ⟩
          L.F₁ 𝒞.id                                                         ≈⟨ L.identity ⟩
          𝒟.id                                                              ∎
        ; sectionᵣ = begin
          𝒟 [ adjoint.counit.η (L.₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈⟨ adjoint.zig ⟩
          𝒟.id ∎
        }
      }
      where
        open 𝒟.HomReasoning

    -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer.
    -- We can think of this as identifying the action of the algebra lifted to a "free" structure
    -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both.
    has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))
    has-coequalizer M = has-reflexive-coequalizers (reflexive-pair M)

    module Comparison⁻¹ = Functor (Comparison⁻¹ adjoint has-coequalizer)
    module Comparison⁻¹⊣Comparison = Adjoint (Comparison⁻¹⊣Comparison adjoint has-coequalizer)

    -- We have one interesting coequalizer in 𝒞 built out of a T-module's action.
    coequalizer-action : (M : Module T) → Coequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M))))
    coequalizer-action M = record
      { arr = Module.action M
      ; isCoequalizer = record
        { equality = Module.commute M
        ; coequalize = λ {X} {h} eq → 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ]
        ; universal = λ {C} {h} {eq} → begin
          h                                                                                ≈⟨ introʳ adjoint.zag ○ 𝒞.sym-assoc ⟩
          𝒞 [ 𝒞 [ h ∘ R.F₁ (adjoint.counit.η (L.₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ pushˡ (⟺ eq) ⟩
          𝒞 [ h ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ]              ≈⟨ pushʳ (adjoint.unit.sym-commute (Module.action M)) ⟩
          𝒞 [ 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ]                                          ∎
        ; unique = λ {X} {h} {i} {eq} eq′ → begin
          i ≈⟨ introʳ (Module.identity M) ⟩
          𝒞 [ i ∘ 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ eq′) ⟩
          𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∎
        }
      }
      where
        open 𝒞.HomReasoning
        open MR 𝒞

  -- If 'R' preserves reflexive coequalizers, then the unit of the adjunction is a pointwise isomorphism
  unit-iso : PreservesReflexiveCoequalizers R → (X : Module T) → Σ[ h ∈ 𝒞ᵀ [ Comparison.F₀ (Comparison⁻¹.F₀ X) , X ] ] (Iso 𝒞ᵀ (Comparison⁻¹⊣Comparison.unit.η X) h)
  unit-iso preserves-reflexive-coeq X =
    let
        coequalizerˣ = has-coequalizer X
        coequalizerᴿˣ = ((IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair X) (has-coequalizer X))))
        coequalizer-iso = up-to-iso 𝒞 (coequalizer-action X) coequalizerᴿˣ
        module coequalizer-iso = _≅_ coequalizer-iso
        open 𝒞
        open 𝒞.HomReasoning
        open MR 𝒞
        α = record
          { arr = coequalizer-iso.to
          ; commute = begin
            coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)                                                                                ≈⟨ introʳ (R.F-resp-≈ L.identity ○ R.identity) ⟩
            (coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ 𝒞.id)                                                                                ≈⟨ pushʳ (R.F-resp-≈ (L.F-resp-≈ (⟺ coequalizer-iso.isoʳ)) ○ R.F-resp-≈ L.homomorphism ○ R.homomorphism) ⟩
            ((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ) ∘ adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to)                ≈⟨ (refl⟩∘⟨ (R.F-resp-≈ L.homomorphism ○ R.homomorphism)) ⟩∘⟨refl ⟩
            ((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘  R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈⟨ center ([ R ]-resp-square (adjoint.counit.commute _)) ⟩∘⟨refl ⟩
            ((coequalizer-iso.to ∘ (R.F₁ (arr coequalizerˣ) ∘ R.F₁ (adjoint.counit.η (L.F₀ _))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to))       ≈⟨ (refl⟩∘⟨ cancelʳ (⟺ R.homomorphism ○ R.F-resp-≈ adjoint.zig ○ R.identity)) ⟩∘⟨refl  ⟩
            (coequalizer-iso.to ∘ R.F₁ (arr coequalizerˣ)) ∘ R.F₁ (L.F₁ coequalizer-iso.to)                                                                               ≈˘⟨ universal coequalizerᴿˣ ⟩∘⟨refl ⟩
            Module.action X ∘ R.F₁ (L.F₁ coequalizer-iso.to) ∎
          }
    in α , record { isoˡ = coequalizer-iso.isoˡ ; isoʳ = coequalizer-iso.isoʳ }

  -- If 'R' preserves reflexive coequalizers and reflects isomorphisms, then the counit of the adjunction is a pointwise isomorphism.
  counit-iso : PreservesReflexiveCoequalizers R → Conservative R → (X : 𝒟.Obj) → Σ[ h ∈ 𝒟 [ X , Comparison⁻¹.F₀ (Comparison.F₀ X) ] ] Iso 𝒟 (Comparison⁻¹⊣Comparison.counit.η X) h
  counit-iso preserves-reflexive-coeq conservative X =
    let coequalizerᴿᴷˣ = IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) (has-coequalizer (Comparison.F₀ X)))
        coequalizerᴷˣ = has-coequalizer (Comparison.F₀ X)
        coequalizer-iso = up-to-iso 𝒞 coequalizerᴿᴷˣ (coequalizer-action (Comparison.F₀ X))
        module coequalizer-iso = _≅_ coequalizer-iso
        open 𝒞.HomReasoning
        open 𝒞.Equiv
    in conservative (Iso-resp-≈ 𝒞 coequalizer-iso.iso (⟺ (preserves-coequalizer-unique {R} preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) coequalizerᴷˣ)) refl)

  -- Now, for the final result. Both the unit and counit of the adjunction between the comparison functor and it's inverse are isomorphisms,
  -- so therefore they form natural isomorphism. Therfore, we have an equivalence of categories.
  crude-monadicity : PreservesReflexiveCoequalizers R → Conservative R → StrongEquivalence 𝒞ᵀ 𝒟
  crude-monadicity preserves-reflexlive-coeq conservative = record
    { F = Comparison⁻¹ adjoint has-coequalizer
    ; G = Comparison
    ; weak-inverse = pointwise-iso-equivalence (Comparison⁻¹⊣Comparison adjoint has-coequalizer)
                                               (counit-iso preserves-reflexlive-coeq conservative)
                                               (unit-iso preserves-reflexlive-coeq)
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Categories
open import Monads

module Monads.Kleisli {a b}{C : Cat {a}{b}}(M : Monad C) where

open import Library
open Cat C
open Monad M

Kl : Cat
Kl = record{
  Obj  = Obj;
  Hom  = λ X Y → Hom X (T Y);
  iden = η;
  comp = λ f g → comp (bind f) g;
  idl  = λ{X}{Y}{f} →
    proof
    comp (bind η) f
    ≅⟨ cong (λ g → comp g f) law1 ⟩
    comp iden f
    ≅⟨ idl ⟩
    f
    ∎;
  idr  = law2;
  ass  = λ{_}{_}{_}{_}{f}{g}{h} →
    proof
    comp (bind (comp (bind f) g)) h
    ≅⟨ cong (λ f → comp f h) law3 ⟩
    comp (comp (bind f) (bind g)) h
    ≅⟨ ass ⟩
    comp (bind f) (comp (bind g) h)
    ∎}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.SetoidDiscrete where

open import Data.Unit using (⊤; tt)
open import Function using (flip)
open import Level using (Lift; lift)
open import Relation.Binary using (Setoid; IsEquivalence)

open import Categories.Category.Core using (Category)
open import Categories.Category.Discrete using (DiscreteCategory)
open import Categories.Morphism using (_≅_; ≅-isEquivalence)
{-
 This is a better version of Discrete, which is more in line with
 the rest of this library, and makes a Category out of a Setoid.
 It is still 'wrong' as the equivalence is completely uninformative.
-}

Discrete : ∀ {o ℓ e} (A : Setoid o ℓ) → DiscreteCategory o ℓ e
Discrete {o} {ℓ} {e} A = record
  { category = C
  ; isDiscrete = record
    { isGroupoid = record { _⁻¹ = sym }
    }
  }
  where
    open Setoid A
    C : Category o ℓ e
    C = record
      { Obj       = Carrier
      ; _⇒_       = _≈_
      ; _≈_       = λ _ _ → Lift e ⊤
      ; id        = Setoid.refl A
      ; _∘_       = flip trans
      }


text:
-- Reported by nils.anders.danielsson, Feb 7 2014
-- The code below is accepted by Agda 2.3.2.2.

module Issue1048 where

module M (_ : Set) where

  data D : Set where
    c₁ : D
    c₂ : D → D

postulate A : Set

open M A

postulate
  ♭ : D → D
  ♯ : D → D

data S : D → Set where
  s : (d : D) → S (♭ d) → S (c₂ d)

postulate
  f : S (♭ (♯ c₁)) → S c₁

Foo : S (c₂ (♯ c₁)) → Set₁
Foo (s ._ x) with f x
... | _ = Set

-- Bug.agda:24,1-25,14
-- The constructor c₁ does not construct an element of D
-- when checking that the type (x : S (♭ (♯ c₁))) → S M.c₁ → Set₁ of
-- the generated with function is well-formed

-- Fixed.  Need to normalize constructor in checkInternal.

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.Data.Nat.Coprime where

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

open import Cubical.Data.Sigma
open import Cubical.Data.NatPlusOne

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Nat.Divisibility
open import Cubical.Data.Nat.GCD

areCoprime : ℕ × ℕ → Type₀
areCoprime (m , n) = isGCD m n 1

-- Any pair (m , n) can be converted to a coprime pair (m' , n') s.t.
--  m' ∣ m, n' ∣ n if and only if one of m or n is nonzero

module ToCoprime ((m , n) : ℕ × ℕ₊₁) where
  d   = gcd m (ℕ₊₁→ℕ n)
  d∣m = gcdIsGCD m (ℕ₊₁→ℕ n) .fst .fst
  d∣n = gcdIsGCD m (ℕ₊₁→ℕ n) .fst .snd
  gr  = gcdIsGCD m (ℕ₊₁→ℕ n) .snd

  c₁ : ℕ
  p₁ : c₁ · d ≡ m
  c₁ = ∣-untrunc d∣m .fst; p₁ = ∣-untrunc d∣m .snd

  c₂ : ℕ₊₁
  p₂ : (ℕ₊₁→ℕ c₂) · d ≡ (ℕ₊₁→ℕ n)
  c₂ = 1+ (∣s-untrunc d∣n .fst); p₂ = ∣s-untrunc d∣n .snd

  toCoprime : ℕ × ℕ₊₁
  toCoprime = (c₁ , c₂)

  private
    lem : ∀ a {b c d e} → a · b ≡ c → c · d ≡ e → a · (b · d) ≡ e
    lem a p q = ·-assoc a _ _ ∙ cong (_· _) p ∙ q

    gr' : ∀ d' → prediv d' c₁ → prediv d' (ℕ₊₁→ℕ c₂) → (d' · d) ∣ d
    gr' d' (b₁ , q₁) (b₂ , q₂) = gr (d' · d) ((∣ b₁ , lem b₁ q₁ p₁ ∣) ,
                                              (∣ b₂ , lem b₂ q₂ p₂ ∣))

  d-1 = m∣sn→z<m d∣n .fst
  q : d ≡ suc d-1
  q = sym (+-comm 1 d-1 ∙ m∣sn→z<m d∣n .snd)

  private
    -- this only works because d > 0 (<=> m > 0 or n > 0)
    d-cancelʳ : ∀ d' → (d' · d) ∣ d → d' ∣ 1
    d-cancelʳ d' div = ∣-cancelʳ d-1 (∣-trans (subst (λ x → (d' · x) ∣ x) q div)
                                              (∣-refl (sym (·-identityˡ _))))

  toCoprimeAreCoprime : areCoprime (c₁ , ℕ₊₁→ℕ c₂)
  fst toCoprimeAreCoprime = ∣-oneˡ c₁ , ∣-oneˡ (ℕ₊₁→ℕ c₂)
  snd toCoprimeAreCoprime d' (d'∣c₁ , d'∣c₂) = PropTrunc.rec isProp∣ (λ a →
                                               PropTrunc.rec isProp∣ (λ b →
                                                d-cancelʳ d' (gr' d' a b)) d'∣c₂) d'∣c₁

  toCoprime∣ : (c₁ ∣ m) × (ℕ₊₁→ℕ c₂ ∣ ℕ₊₁→ℕ n)
  toCoprime∣ = ∣ d , ·-comm d c₁ ∙ p₁ ∣ , ∣ d , ·-comm d (ℕ₊₁→ℕ c₂) ∙ p₂ ∣

  toCoprime-idem : areCoprime (m , ℕ₊₁→ℕ n) → (c₁ , c₂) ≡ (m , n)
  toCoprime-idem cp i = q₁ i , ℕ₊₁→ℕ-inj q₂ i
    where q₁ = sym (·-identityʳ c₁) ∙ cong (c₁ ·_) (sym (isGCD→gcd≡ cp)) ∙ p₁
          q₂ = sym (·-identityʳ (ℕ₊₁→ℕ c₂)) ∙ cong (ℕ₊₁→ℕ c₂ ·_) (sym (isGCD→gcd≡ cp)) ∙ p₂

open ToCoprime using (toCoprime; toCoprimeAreCoprime; toCoprime∣; toCoprime-idem) public

toCoprime-cancelʳ : ∀ ((m , n) : ℕ × ℕ₊₁) k
                    → toCoprime (m · ℕ₊₁→ℕ k , n ·₊₁ k) ≡ toCoprime (m , n)
toCoprime-cancelʳ (m , n) (1+ k) i =
  inj-·sm {c₁'} {d-1} {c₁} r₁ i , ℕ₊₁→ℕ-inj (inj-·sm {ℕ₊₁→ℕ c₂'} {d-1} {ℕ₊₁→ℕ c₂} r₂) i
  where open ToCoprime (m , n)
        open ToCoprime (m · suc k , n ·₊₁ (1+ k)) using ()
          renaming (c₁ to c₁'; p₁ to p₁'; c₂ to c₂'; p₂ to p₂')

        q₁ : c₁' · d · suc k ≡ m · suc k
        q₁ =   sym (·-assoc c₁' (ToCoprime.d (m , n)) (suc k))
             ∙ cong (c₁' ·_) (sym (gcd-factorʳ m (ℕ₊₁→ℕ n) (suc k)))
             ∙ p₁'
        q₂ : ℕ₊₁→ℕ c₂' · (ToCoprime.d (m , n)) · suc k ≡ ℕ₊₁→ℕ n · suc k
        q₂ =   sym (·-assoc (ℕ₊₁→ℕ c₂') (ToCoprime.d (m , n)) (suc k))
             ∙ cong (ℕ₊₁→ℕ c₂' ·_) (sym (gcd-factorʳ m (ℕ₊₁→ℕ n) (suc k)))
             ∙ p₂'

        r₁ : c₁' · suc d-1 ≡ c₁ · suc d-1
        r₁ = subst (λ z → c₁' · z ≡ c₁ · z) q (inj-·sm q₁ ∙ sym p₁)
        r₂ : ℕ₊₁→ℕ c₂' · suc d-1 ≡ ℕ₊₁→ℕ c₂ · suc d-1
        r₂ = subst (λ z → ℕ₊₁→ℕ c₂' · z ≡ ℕ₊₁→ℕ c₂ · z) q (inj-·sm q₂ ∙ sym p₂)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Issue4606 where

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

-- Test case from Andrew Pitts.
----------------------------------------------------------------------
-- Well-Founded Recursion
----------------------------------------------------------------------
data Acc {A : Set}(R : A → A → Set)(x : A) : Set where
  acc : (∀ y → R y x → Acc R y) → Acc R x

iswf : {A : Set}(R : A → A → Set) → Set
iswf R = ∀ x → Acc R x

----------------------------------------------------------------------
-- A logical contradiction
----------------------------------------------------------------------
data A : Set where
  O : A
  S : A → A
  E : ∀ x → S x ≡ x

data _<_ (x : A) : A → Set where
  <S : x < S x

O<O : O < O
O<O = primTransp (\ i →  O < E O i) i0 <S

-- Given that O < O holds, we should not be able to prove that < is
-- well-founded, but we can!
iswf< : iswf _<_
iswf< i = acc (α i)
  where
  α : ∀ x y → y < x → Acc _<_ y
 -- I don't think the following clause should pass
 -- the termination checker
  α .(S y) y <S = acc (α y)

data ⊥ : Set where

AccO→⊥ : Acc _<_ O → ⊥
AccO→⊥ (acc f) = AccO→⊥ (f O O<O)

contradiction : ⊥
contradiction = AccO→⊥ (iswf< O)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Type.Lemmas where

open import Context
open import Type.Core

open import Function
open import Data.Unit.Base
open import Relation.Binary.PropositionalEquality

foldlᶜ-▻-ε : ∀ {α} {A : Set α} -> (Θ : Con A) -> foldlᶜ _▻_ ε Θ ≡ Θ
foldlᶜ-▻-ε  ε      = refl
foldlᶜ-▻-ε (Γ ▻ σ) = cong (_▻ σ) (foldlᶜ-▻-ε Γ)

-- Same as `mapᶜ f (Γ ▻▻ Δ) ≡ mapᶜ f Γ ▻▻ mapᶜ f Δ`, but we fully inline the definitions,
-- because the REWRITE pragma requires that.
mapᶜ-▻▻
  : ∀ {α β} {A : Set α} {B : Set β} {f : A -> B} {Γ : Con A}
  -> ∀ Δ ->
      foldlᶜ (λ Ξ σ -> Ξ ▻ f σ) ε (foldlᶜ _▻_ Γ Δ)
    ≡ foldlᶜ _▻_ (foldlᶜ (λ Ξ σ -> Ξ ▻ f σ) ε Γ) (foldlᶜ (λ Ξ σ -> Ξ ▻ f σ) ε Δ)
mapᶜ-▻▻  ε      = refl
mapᶜ-▻▻ (Δ ▻ τ) = cong (_▻ _) (mapᶜ-▻▻ Δ)

keep-id : ∀ {α} {A : Set α} {Γ : Con A} {σ τ} -> (v : σ ∈ Γ ▻ τ) -> keep id v ≡ v
keep-id  vz    = refl
keep-id (vs v) = refl

keep-keep
  : ∀ {α} {A : Set α} {Γ Δ Ξ : Con A} {σ τ}
  -> (κ : Δ ⊆ Ξ) -> (ι : Γ ⊆ Δ) -> (v : σ ∈ Γ ▻ τ) -> keep κ (keep ι v) ≡ keep (κ ∘ ι) v
keep-keep κ ι  vz    = refl
keep-keep κ ι (vs v) = refl

dupl-keep-vs
  : ∀ {α} {A : Set α} {Γ Δ : Con A} {σ τ}
  -> (ι : Γ ⊆ Δ) -> (v : σ ∈ Γ ▻ τ) -> dupl (keep (vs_ ∘ ι) v) ≡ keep ι v
dupl-keep-vs ι  vz    = refl
dupl-keep-vs ι (vs v) = refl

inject-foldr-poly
  : ∀ {α β γ} {A : Set α} {B : Set β} {yᶠ yᵍ}
  -> (C : B -> Set γ)
  -> (h : ∀ {yʰ} -> C yʰ -> C yʰ -> C yʰ)
  -> (g : C yᶠ -> C yᵍ)
  -> (∀ {y z} -> h (g y) (g z) ≡ g (h y z))
  -> (f : A -> C yᶠ)
  -> (Γ : Con A)
  -> (z : C yᶠ)
  -> g (foldrᶜ (h ∘ f) z Γ) ≡ foldrᶜ (h ∘ g ∘ f) (g z) Γ
inject-foldr-poly C h g dist f  ε      y = refl
inject-foldr-poly C h g dist f (Γ ▻ x) y
  rewrite dist {f x} {y} = inject-foldr-poly C h g dist f Γ (h (f x) y)

inject-foldr-mono
  : ∀ {α β} {A : Set α} {B : Set β}
  -> (h : B -> B -> B)
  -> (g : B -> B)
  -> (∀ {y z} -> h (g y) (g z) ≡ g (h y z))
  -> (f : A -> B)
  -> (Γ : Con A)
  -> (y : B)
  -> g (foldrᶜ (h ∘ f) y Γ) ≡ foldrᶜ (h ∘ g ∘ f) (g y) Γ
inject-foldr-mono h g dist f Γ y = inject-foldr-poly {B = ⊤} _ h g dist f Γ y

keep-eq
  : ∀ {α} {A : Set α} {Θ Ξ : Con A} {σ} (ι κ : Θ ⊆ Ξ)
  -> (∀ {τ} -> (v : τ ∈ Θ)     -> renᵛ       ι  v ≡ renᵛ       κ  v)
  -> (∀ {τ} -> (v : τ ∈ Θ ▻ σ) -> renᵛ (keep ι) v ≡ renᵛ (keep κ) v)
keep-eq ι κ q  vz    = refl
keep-eq ι κ q (vs v) = cong vs_ (q v)

renᵗ-ext
  : ∀ {Θ Ξ σ} (ι κ : Θ ⊆ Ξ) (α : Θ ⊢ᵗ σ)
  -> (∀ {τ} -> (v : τ ∈ Θ) -> renᵛ ι v ≡ renᵛ κ v)
  -> renᵗ ι α ≡ renᵗ κ α
renᵗ-ext ι κ (Var v) q = cong  Var (q v)
renᵗ-ext ι κ (Lam β) q = cong Lam_ (renᵗ-ext (keep ι) (keep κ) β (keep-eq ι κ q))
renᵗ-ext ι κ (φ ∙ α) q = cong₂ _∙_ (renᵗ-ext ι κ φ q) (renᵗ-ext ι κ α q)
renᵗ-ext ι κ (α ⇒ β) q = cong₂ _⇒_ (renᵗ-ext ι κ α q) (renᵗ-ext ι κ β q)
renᵗ-ext ι κ (π σ β) q = cong (π σ) (renᵗ-ext (keep ι) (keep κ) β (keep-eq ι κ q))
renᵗ-ext ι κ (μ ψ α) q = cong₂ μ (renᵗ-ext ι κ ψ q) (renᵗ-ext ι κ α q)

renᵗ-keep-keep
  : ∀ {Θ Ξ Ω σ τ} (κ : Ξ ⊆ Ω) (ι : Θ ⊆ Ξ) (β : Θ ▻ σ ⊢ᵗ τ)
  -> renᵗ (keep κ ∘ keep ι) β ≡ renᵗ (keep (κ ∘ ι)) β
renᵗ-keep-keep κ ι β = renᵗ-ext (keep κ ∘ keep ι) (keep (κ ∘ ι)) β λ
  {  vz    -> refl
  ; (vs v) -> refl
  }

renᵗ-∘
  : ∀ {Θ Ξ Ω σ} (κ : Ξ ⊆ Ω) (ι : Θ ⊆ Ξ) (α : Θ ⊢ᵗ σ)
  -> renᵗ κ (renᵗ ι α) ≡ renᵗ (κ ∘ ι) α
renᵗ-∘ κ ι (Var v) = refl
renᵗ-∘ κ ι (Lam β) = cong Lam_ (trans (renᵗ-∘ (keep κ) (keep ι) β) (renᵗ-keep-keep κ ι β))
renᵗ-∘ κ ι (f ∙ α) = cong₂ _∙_ (renᵗ-∘ κ ι f) (renᵗ-∘ κ ι α)
renᵗ-∘ κ ι (α ⇒ β) = cong₂ _⇒_  (renᵗ-∘ κ ι α) (renᵗ-∘ κ ι β)
renᵗ-∘ κ ι (π σ β) = cong (π σ) (trans (renᵗ-∘ (keep κ) (keep ι) β) (renᵗ-keep-keep κ ι β))
renᵗ-∘ κ ι (μ ψ α) = cong₂ μ (renᵗ-∘ κ ι ψ) (renᵗ-∘ κ ι α)

renᵗ-keep-id
  : ∀ {Θ σ τ} (β : Θ ▻ σ ⊢ᵗ τ)
  -> renᵗ (keep id) β ≡ renᵗ id β
renᵗ-keep-id β = renᵗ-ext (keep id) id β λ
  {  vz    -> refl
  ; (vs v) -> refl
  }

renᵗ-id : ∀ {Θ σ} (α : Θ ⊢ᵗ σ) -> renᵗ id α ≡ α
renᵗ-id (Var v) = refl
renᵗ-id (Lam β) = cong Lam_ (trans (renᵗ-keep-id β) (renᵗ-id β))
renᵗ-id (φ ∙ α) = cong₂ _∙_ (renᵗ-id φ) (renᵗ-id α)
renᵗ-id (α ⇒ β) = cong₂ _⇒_ (renᵗ-id α) (renᵗ-id β)
renᵗ-id (π σ β) = cong (π σ) (trans (renᵗ-keep-id β) (renᵗ-id β))
renᵗ-id (μ ψ α) = cong₂ μ (renᵗ-id ψ) (renᵗ-id α)

module EnvironmentLemmas
    {α β} {A : Set α} {_◆_ : Con A -> A -> Set β}
    (environment : Environment _◆_) where
  open Environment environment

  keepᵉ-eq
    : ∀ {Θ Ξ : Con A} {σ} (ρ χ : Ξ ⊢ᵉ Θ)
    -> (∀ {τ} -> (v : τ ∈ Θ)     -> lookupᵉ v        ρ  ≡ lookupᵉ v        χ )
    -> (∀ {τ} -> (v : τ ∈ Θ ▻ σ) -> lookupᵉ v (keepᵉ ρ) ≡ lookupᵉ v (keepᵉ χ))
  keepᵉ-eq ρ χ q  vz    = refl
  keepᵉ-eq ρ χ q (vs v) = cong (renᵈ vs_) (q v)

module _ where
  open TypeEnv
  open EnvironmentLemmas environmentᵗ

  subᵗ-ext
    : ∀ {Θ Ξ σ} (ρ χ : Ξ ⊢ᵗᵉ Θ) (α : Θ ⊢ᵗ σ)
    -> (∀ {τ} -> (v : τ ∈ Θ) -> lookupᵉ v ρ ≡ lookupᵉ v χ)
    -> subᵗ ρ α ≡ subᵗ χ α
  subᵗ-ext ρ χ (Var v) q = q v
  subᵗ-ext ρ χ (Lam β) q = cong Lam_ (subᵗ-ext (keepᵉ ρ) (keepᵉ χ) β (keepᵉ-eq ρ χ q))
  subᵗ-ext ρ χ (φ ∙ α) q = cong₂ _∙_ (subᵗ-ext ρ χ φ q) (subᵗ-ext ρ χ α q)
  subᵗ-ext ρ χ (α ⇒ β) q = cong₂ _⇒_ (subᵗ-ext ρ χ α q) (subᵗ-ext ρ χ β q)
  subᵗ-ext ρ χ (π σ β) q = cong (π σ) (subᵗ-ext (keepᵉ ρ) (keepᵉ χ) β (keepᵉ-eq ρ χ q))
  subᵗ-ext ρ χ (μ ψ α) q = cong₂ μ (subᵗ-ext ρ χ ψ q) (subᵗ-ext ρ χ α q)

  subᵗ-keepᵉ-keep
    : ∀ {Θ Ξ Ω σ τ} (ρ : Ω ⊢ᵗᵉ Ξ) (ι : Θ ⊆ Ξ) (β : Θ ▻ σ ⊢ᵗ τ)
    -> subᵗ (keepᵉ ρ ∘ᵉ keep ι) β ≡ subᵗ (keepᵉ (ρ ∘ᵉ ι)) β
  subᵗ-keepᵉ-keep ρ ι β = subᵗ-ext (keepᵉ ρ ∘ᵉ keep ι) (keepᵉ (ρ ∘ᵉ ι)) β λ
    {  vz    -> refl
    ; (vs v) -> refl
    }

  subᵗ-renᵗ
    : ∀ {Θ Ξ Ω σ} (ρ : Ω ⊢ᵗᵉ Ξ) (ι : Θ ⊆ Ξ) (α : Θ ⊢ᵗ σ)
    -> subᵗ ρ (renᵗ ι α) ≡ subᵗ (ρ ∘ᵉ ι) α
  subᵗ-renᵗ ρ ι (Var v) = refl
  subᵗ-renᵗ ρ ι (Lam β) = cong Lam_ (trans (subᵗ-renᵗ (keepᵉ ρ) (keep ι) β) (subᵗ-keepᵉ-keep ρ ι β))
  subᵗ-renᵗ ρ ι (φ ∙ α) = cong₂ _∙_ (subᵗ-renᵗ ρ ι φ) (subᵗ-renᵗ ρ ι α)
  subᵗ-renᵗ ρ ι (α ⇒ β) = cong₂ _⇒_ (subᵗ-renᵗ ρ ι α) (subᵗ-renᵗ ρ ι β)
  subᵗ-renᵗ ρ ι (π σ β) = cong (π σ) (trans (subᵗ-renᵗ (keepᵉ ρ) (keep ι) β) (subᵗ-keepᵉ-keep ρ ι β))
  subᵗ-renᵗ ρ ι (μ ψ α) = cong₂ μ (subᵗ-renᵗ ρ ι ψ) (subᵗ-renᵗ ρ ι α)

  subᵗ-keepᵉ-idᵉ
    : ∀ {Θ σ τ} (β : Θ ▻ σ ⊢ᵗ τ)
    -> subᵗ (keepᵉ idᵉ) β ≡ subᵗ idᵉ β
  subᵗ-keepᵉ-idᵉ β = subᵗ-ext (keepᵉ idᵉ) idᵉ β λ
    {  vz    -> refl
    ; (vs v) -> refl
    }

  subᵗ-idᵉ
    : ∀ {Θ σ} (α : Θ ⊢ᵗ σ)
    -> subᵗ idᵉ α ≡ α
  subᵗ-idᵉ (Var v) = refl
  subᵗ-idᵉ (Lam β) = cong Lam_ (trans (subᵗ-keepᵉ-idᵉ β) (subᵗ-idᵉ β))
  subᵗ-idᵉ (φ ∙ α) = cong₂ _∙_ (subᵗ-idᵉ φ) (subᵗ-idᵉ α)
  subᵗ-idᵉ (α ⇒ β) = cong₂ _⇒_ (subᵗ-idᵉ α) (subᵗ-idᵉ β)
  subᵗ-idᵉ (π σ β) = cong (π σ) (trans (subᵗ-keepᵉ-idᵉ β) (subᵗ-idᵉ β))
  subᵗ-idᵉ (μ ψ α) = cong₂ μ (subᵗ-idᵉ ψ) (subᵗ-idᵉ α)

  subᵗ-keepᵉ-Var
    : ∀ {Θ Ξ σ τ} (ι : Θ ⊆ Ξ) (β : Θ ▻ σ ⊢ᵗ τ)
    -> subᵗ (keepᵉ (PackEnv (Var ∘ ι))) β ≡ subᵗ (PackEnv (Var ∘ keep ι)) β
  subᵗ-keepᵉ-Var ι β = subᵗ-ext (keepᵉ (PackEnv (Var ∘ ι))) (PackEnv (Var ∘ keep ι)) β λ
    {  vz    -> refl
    ; (vs v) -> refl
    }

  subᵗ-Var
    : ∀ {Θ Ξ σ} (ι : Θ ⊆ Ξ) (α : Θ ⊢ᵗ σ)
    -> subᵗ (PackEnv (Var ∘ ι)) α ≡ renᵗ ι α
  subᵗ-Var ι (Var v) = refl
  subᵗ-Var ι (Lam β) = cong Lam_ (trans (subᵗ-keepᵉ-Var ι β) (subᵗ-Var (keep ι) β))
  subᵗ-Var ι (φ ∙ α) = cong₂ _∙_ (subᵗ-Var ι φ) (subᵗ-Var ι α)
  subᵗ-Var ι (α ⇒ β) = cong₂ _⇒_ (subᵗ-Var ι α) (subᵗ-Var ι β)
  subᵗ-Var ι (π σ β) = cong (π σ) (trans (subᵗ-keepᵉ-Var ι β) (subᵗ-Var (keep ι) β))
  subᵗ-Var ι (μ ψ α) = cong₂ μ (subᵗ-Var ι ψ) (subᵗ-Var ι α)

inject-foldr-⇒-renᵗ
  : ∀ {Θ Ξ Ω} {f : Star Θ -> Star Ξ}
  -> ∀ Δ
  -> (ι : Ξ ⊆ Ω)
  -> (β : Star Ξ)
  -> renᵗ ι (conToTypeBy f Δ β) ≡ conToTypeBy (renᵗ ι ∘ f) Δ (renᵗ ι β)
inject-foldr-⇒-renᵗ Δ ι β = inject-foldr-poly Star _⇒_ (renᵗ ι) refl _ Δ β

inject-foldr-⇒-subᵗ
  : ∀ {Θ Ξ Ω} {f : Star Θ -> Star Ξ}
  -> ∀ Δ
  -> (ρ : Ω TypeEnv.⊢ᵉ Ξ)
  -> (β : Star Ξ)
  -> subᵗ ρ (conToTypeBy f Δ β) ≡ conToTypeBy (subᵗ ρ ∘ f) Δ (subᵗ ρ β)
inject-foldr-⇒-subᵗ Δ ρ β = inject-foldr-poly Star _⇒_ (subᵗ ρ) refl _ Δ β

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
module FunctionProofs where
open FunctionSet ⦃ signature ⦄

[∃]-unrelatedᵣ-[→]ᵣ-inside-[∀ₛ] : ∀{D : Domain}{P : BinaryRelator} → Proof(∀ₗ(x ↦ ∃ₗ(y ↦ (x ∈ D) ⟶ P(x)(y))) ⟷ ∀ₛ(D)(x ↦ ∃ₗ(y ↦ P(x)(y))))
[∃]-unrelatedᵣ-[→]ᵣ-inside-[∀ₛ] {D}{P} = [↔]-with-[∀] ([∃]-unrelatedᵣ-[→])

[∀ₛ∃!]-to[∀ₛ∃] : ∀{P : BinaryRelator}{D : Domain} → Proof(∀ₛ(D)(x ↦ ∃ₗ!(y ↦ P(x)(y)))) → Proof(∀ₛ(D)(x ↦ ∃ₗ(y ↦ P(x)(y))))
[∀ₛ∃!]-to[∀ₛ∃] proof =
  ([∀ₛ]-intro(\{x} → xinD ↦
    [∧].elimₗ([∀ₛ]-elim proof {x} xinD)
  ))

-- The construction of a meta-function in the meta-logic from a function in the set theory
fnset-witness : ∀{D} → (f : Domain) → ⦃ _ : Proof(Total(D)(f)) ⦄ → Function
fnset-witness f ⦃ proof ⦄ = [∃]-fn-witness ⦃ [↔].elimₗ [∃]-unrelatedᵣ-[→]ᵣ-inside-[∀ₛ] (proof) ⦄

fnset-value : ∀{D} → (f : Domain) → ⦃ proof : Proof(Total(D)(f)) ⦄ → Proof(∀ₛ(D)(x ↦ (x , fnset-witness f(x)) ∈ f))
fnset-value{D} f ⦃ proof ⦄ = [∃]-fn-proof ⦃ [↔].elimₗ [∃]-unrelatedᵣ-[→]ᵣ-inside-[∀ₛ] (proof) ⦄

fnset-proof : ∀{D} → (f : Domain) → ⦃ _ : Proof(FunctionSet(f)) ⦄ → ⦃ total : Proof(Total(D)(f)) ⦄ → Proof(∀ₛ(D)(x ↦ ∀ₗ(y ↦ (fnset-witness{D} f ⦃ total ⦄ x ≡ y) ⟷ ((x , y) ∈ f))))
fnset-proof{D} f ⦃ function ⦄ ⦃ total ⦄ =
  ([∀ₛ]-intro(\{x} → x∈D ↦
    ([∀].intro(\{y} →
      ([↔].intro
        (xy∈f ↦
          ([→].elim
            ([∀].elim([∀].elim([∀].elim function{x}) {fnset-witness f(x)}) {y})
            ([∧].intro
              ([∀ₛ]-elim(fnset-value f) {x} (x∈D))
              (xy∈f)
            )
          )
        )

        (fx≡y ↦
          [≡].elimᵣ (fx≡y) ([∀ₛ]-elim (fnset-value(f)) {x} (x∈D))
        )
      )
    ))
  ))

[→ₛₑₜ]-witness : ∀{A B} → (f : Domain) → ⦃ _ : Proof(f ∈ (A →ₛₑₜ B)) ⦄ → Function
[→ₛₑₜ]-witness f ⦃ proof ⦄ (x) =
  (fnset-witness f
    ⦃ [∧].elimᵣ([∧].elimᵣ([↔].elimᵣ
      ([∀].elim([∀].elim filter-membership))
      (proof)
    )) ⦄
    (x)
  )

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:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Dependently typed changes (Def 3.4 and 3.5, Fig. 4b and 4e)
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Denotation.Value as Value
open import Base.Change.Algebra as CA
  using (ChangeAlgebraFamily)

module Parametric.Change.Validity
    {Base : Type.Structure}
    (⟦_⟧Base : Value.Structure Base)
  where

open Type.Structure Base
open Value.Structure Base ⟦_⟧Base

open import Base.Denotation.Notation public

open import Relation.Binary.PropositionalEquality
open import Level

-- Extension Point: Change algebras for base types
Structure : Set₁
Structure = ChangeAlgebraFamily ⟦_⟧Base

module Structure {{change-algebra-base : Structure}} where
  -- change algebras

  open CA public renaming
    -- Constructors for All′
    ( [] to ∅
    ; _∷_ to _•_
    )

  change-algebra : ∀ τ → ChangeAlgebra ⟦ τ ⟧Type
  change-algebra (base ι) = change-algebra₍ ι ₎
  change-algebra (τ₁ ⇒ τ₂) = changeAlgebraFun {{change-algebra τ₁}} {{change-algebra τ₂}}

  -- We provide: change algebra for every type
  instance
    change-algebra-family : ChangeAlgebraFamily ⟦_⟧Type
    change-algebra-family = family change-algebra

  -- function changes

  module _ {τ₁ τ₂ : Type} where
    open FunctionChange {{change-algebra τ₁}} {{change-algebra τ₂}} public
      renaming
        ( correct to is-valid
        ; apply to call-change
        )

  -- We also provide: change environments (aka. environment changes).

  open ListChanges ⟦_⟧Type {{change-algebra-family}} public using () renaming
    ( changeAlgebraListChanges to environment-changes
    )

  after-env : ∀ {Γ : Context} → {ρ : ⟦ Γ ⟧} (dρ : Δ₍ Γ ₎ ρ) → ⟦ Γ ⟧
  after-env {Γ} = after₍_₎ Γ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- Various constants
------------------------------------------------------------------------

open import Atom

module Constants (atoms : χ-atoms) where

open χ-atoms atoms

c-zero : Const
c-zero = C.name 0

c-suc : Const
c-suc = C.name 1

c-nil : Const
c-nil = C.name 2

c-cons : Const
c-cons = C.name 3

c-apply : Const
c-apply = C.name 4

c-case : Const
c-case = C.name 5

c-rec : Const
c-rec = C.name 6

c-lambda : Const
c-lambda = C.name 7

c-const : Const
c-const = C.name 8

c-var : Const
c-var = C.name 9

c-branch : Const
c-branch = C.name 10

c-true : Const
c-true = C.name 11

c-false : Const
c-false = C.name 12

c-pair : Const
c-pair = C.name 13

v-equal : Var
v-equal = V.name 0

v-m : Var
v-m = V.name 1

v-n : Var
v-n = V.name 2

v-x : Var
v-x = V.name 3

v-new : Var
v-new = V.name 4

v-e : Var
v-e = V.name 5

v-subst : Var
v-subst = V.name 6

v-e₁ : Var
v-e₁ = V.name 7

v-e₂ : Var
v-e₂ = V.name 8

v-bs : Var
v-bs = V.name 9

v-y : Var
v-y = V.name 10

v-c : Var
v-c = V.name 11

v-es : Var
v-es = V.name 12

v-ys : Var
v-ys = V.name 13

v-member : Var
v-member = V.name 14

v-xs : Var
v-xs = V.name 15

v-lookup : Var
v-lookup = V.name 16

v-b : Var
v-b = V.name 17

v-c′ : Var
v-c′ = V.name 18

v-underscore : Var
v-underscore = V.name 19

v-substs : Var
v-substs = V.name 20

v-e′ : Var
v-e′ = V.name 21

v-map : Var
v-map = V.name 22

v-p : Var
v-p = V.name 23

v-eval : Var
v-eval = V.name 24

v-internal-code : Var
v-internal-code = V.name 25

v-halts : Var
v-halts = V.name 26

v-z : Var
v-z = V.name 27

v-f : Var
v-f = V.name 28

v-g : Var
v-g = V.name 29

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
open import Function using () renaming ( _∘′_ to  _∘_ )
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; refl ; sym ; cong ; cong₂ ; subst )
open import AssocFree.Util using ( subst-natural )

import AssocFree.STLambdaC.Typ

open Relation.Binary.PropositionalEquality.≡-Reasoning using ( begin_ ; _≡⟨_⟩_ ; _∎ )

module AssocFree.STLambdaC.Exp
  (TConst : Set)
  (Const : AssocFree.STLambdaC.Typ.Typ TConst → Set) where

open module Typ = AssocFree.STLambdaC.Typ TConst using
  ( Typ ; Var ; Ctxt ; const ; _⇝_
  ; [] ; [_] ; _++_ ; _∷_ ; _∈_ ; _≪_ ; _≫_ ; _⋙_ ; uniq ; singleton
  ; Case ; case ; inj₁ ; inj₂ ; inj₃ ; case-≪ ; case-≫ ; case-⋙
  ; Case₃ ; case₃ ; caseˡ ; caseʳ ; caseˡ₃ ; caseʳ₃ ; case⁻¹ ; case-iso )

-- Syntax

data Exp (Γ : Ctxt) : Typ → Set where
  const : ∀ {T} → Const T → Exp Γ T
  abs : ∀ T {U} → Exp (T ∷ Γ) U → Exp Γ (T ⇝ U)
  app : ∀ {T U} → Exp Γ (T ⇝ U) → Exp Γ T → Exp Γ U
  var : ∀ {T} → (T ∈ Γ) → Exp Γ T

-- Shorthand

var₀ : ∀ {Γ T} → Exp (T ∷ Γ) T
var₀ {Γ} {T} = var (singleton T ≪ Γ)

var₁ : ∀ {Γ T U} → Exp (U ∷ (T ∷ Γ)) T
var₁ {Γ} {T} {U} = var ([ U ] ≫ singleton T ≪ Γ)

var₂ : ∀ {Γ T U V} → Exp (V ∷ (U ∷ (T ∷ Γ))) T
var₂ {Γ} {T} {U} {V} = var ([ V ] ≫ [ U ] ≫ singleton T ≪ Γ)

-- Andreas Abel suggested defining substitution and renaming together, citing:
--
--   Conor McBride
--   Type Preserving Renaming and Substitution
--
--   Thorsten Altenkirch and Bernhard Reus
--   Monadic Presentations of Lambda Terms Using Generalized Inductive Types
--
-- http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda

-- The idea is to define two kinds, for expressions and variables,
-- such that the kind of variables is contained in the kind of
-- expressions (so admits recursion).

mutual

  data Kind : Set where
    var : Kind
    exp : ∀ {k} → IsVar k → Kind

  data IsVar : Kind → Set where
    var : IsVar var

Thing : Kind → Ctxt → Typ → Set
Thing var       Γ T = (T ∈ Γ)
Thing (exp var) Γ T = Exp Γ T

Substn : Kind → Ctxt → Ctxt → Set
Substn k Γ Δ = ∀ {T} → (T ∈ Δ) → Thing k Γ T

-- Convert between variables, things and expressions

thing : ∀ {k Γ T} → (T ∈ Γ) → Thing k Γ T
thing {var}     x = x
thing {exp var} x = var x

expr : ∀ {k Γ T} → Thing k Γ T → Exp Γ T
expr {var}     x = var x
expr {exp var} M = M

-- Extensional equivalence on substitutions (note: not assuming extensionality)

_≈_ : ∀ {k Γ Δ} → Substn k Γ Δ → Substn k Γ Δ → Set
ρ ≈ σ = ∀ {T} x → ρ {T} x ≡ σ {T} x

-- Identity substitution

id : ∀ {k} Γ → Substn k Γ Γ
id {var}     Γ x = x
id {exp var} Γ x = var x

-- Product structure of substitutions

fst : ∀ Γ Δ → Substn var (Γ ++ Δ) Γ
fst Γ Δ x = x ≪ Δ

snd : ∀ Γ Δ → Substn var (Γ ++ Δ) Δ
snd Γ Δ x = Γ ≫ x

choose : ∀ {k Γ Δ E T} → Substn k Γ Δ → Substn k Γ E → (Case T Δ E) → Thing k Γ T
choose ρ σ (inj₁ x) = ρ x
choose ρ σ (inj₂ x) = σ x

_&&&_ : ∀ {k Γ Δ E} → Substn k Γ Δ → Substn k Γ E → Substn k Γ (Δ ++ E)
(ρ &&& σ) = choose ρ σ ∘ case _ _

-- Singleton substitution

⟨_⟩ : ∀ {k Γ T} → Thing k Γ T → Substn k Γ [ T ]
⟨ M ⟩ x = subst (Thing _ _) (uniq x) M

-- Cons on substitutions

_◁_ : ∀ {k Γ Δ T} → Thing k Γ T → Substn k Γ Δ → Substn k Γ (T ∷ Δ)
M ◁ σ = ⟨ M ⟩ &&& σ

-- Applying a substitution

mutual

  substn+ : ∀ {k} B Γ Δ → Substn k Γ Δ → ∀ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ) T
  substn+ B Γ Δ σ (const c) = const c
  substn+ B Γ Δ σ (abs T M) = abs T (substn+ (T ∷ B) Γ Δ σ M)
  substn+ B Γ Δ σ (app M N) = app (substn+ B Γ Δ σ M) (substn+ B Γ Δ σ N)
  substn+ B Γ Δ σ (var x)   = expr (xsubstn+ B Γ Δ σ (case B Δ x))

  xsubstn+ : ∀ {k} B Γ Δ → Substn k Γ Δ → ∀ {T} → (Case T B Δ) → Thing k (B ++ Γ) T
  xsubstn+           B Γ Δ σ (inj₁ x) = thing (x ≪ Γ)
  xsubstn+ {var}     B Γ Δ σ (inj₂ x) = B ≫ σ x
  xsubstn+ {exp var} B Γ Δ σ (inj₂ x) = substn+ [] (B ++ Γ) Γ (snd B Γ) (σ x) -- weaken* B (σ x)

-- Shorthands

substn* : ∀ {k Γ Δ} → Substn k Γ Δ → ∀ {T} → Exp Δ T → Exp Γ T
substn* {k} {Γ} {Δ} = substn+ [] Γ Δ

substn : ∀ {Γ T U} → Exp Γ T → Exp (T ∷ Γ) U → Exp Γ U
substn {Γ} M = substn* (M ◁ id Γ)

xweaken+ : ∀ B Γ Δ {T} → (T ∈ (B ++ Δ)) → (T ∈ (B ++ Γ ++ Δ))
xweaken+ B Γ Δ x = xsubstn+ B (Γ ++ Δ) Δ (snd Γ Δ) (case B Δ x)

weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
weaken+ B Γ Δ = substn+ B (Γ ++ Δ) Δ (snd Γ Δ)

weaken* : ∀ Γ {Δ T} → Exp Δ T → Exp (Γ ++ Δ) T
weaken* Γ {Δ} = weaken+ [] Γ Δ

weakens* : ∀ {Γ Δ} E → Substn (exp var) Γ Δ → Substn (exp var) (E ++ Γ) Δ
weakens* E σ x = weaken* E (σ x)

weaken*ʳ : ∀ {Γ} Δ {T} → Exp Γ T → Exp (Γ ++ Δ) T
weaken*ʳ {Γ} Δ = weaken+ Γ Δ []

weaken : ∀ {Γ} T {U} → Exp Γ U → Exp (T ∷ Γ) U
weaken T = weaken* [ T ]

-- Composition of substitutions

_⊔_ : Kind → Kind → Kind
k ⊔ var     = k
k ⊔ exp var = exp var

_∙_ : ∀ {k l Γ Δ E} → Substn k Γ Δ → Substn l Δ E → Substn (k ⊔ l) Γ E
_∙_ {k} {var}     ρ σ = ρ ∘ σ
_∙_ {k} {exp var} ρ σ = substn* ρ ∘ σ

-- Functorial action of ++ on substitutions

par : ∀ {k Γ Δ Φ Ψ T} → Substn k Γ Φ → Substn k Δ Ψ → (Case T Φ Ψ) → Thing k (Γ ++ Δ) T
par {var}     {Γ} {Δ} ρ σ (inj₁ x) = ρ x ≪ Δ
par {var}     {Γ} {Δ} ρ σ (inj₂ x) = Γ ≫ σ x
par {exp var} {Γ} {Δ} ρ σ (inj₁ x) = weaken*ʳ Δ (ρ x)
par {exp var} {Γ} {Δ} ρ σ (inj₂ x) = weaken*  Γ (σ x)

_+++_ : ∀ {k Γ Δ Φ Ψ} → Substn k Γ Δ → Substn k Φ Ψ → Substn k (Γ ++ Φ) (Δ ++ Ψ)
(ρ +++ σ) = par ρ σ ∘ case _ _

-- Weakening a variable is a variable

weaken*-var : ∀ Γ {Δ T} (x : T ∈ Δ) →
  weaken* Γ (var x) ≡ var (Γ ≫ x)
weaken*-var Γ {Δ} x = cong (expr ∘ xsubstn+ [] (Γ ++ Δ) Δ (snd Γ Δ)) (case-≫ [] x)

weaken*ʳ-var : ∀ {Γ} Δ {T} (x : T ∈ Γ) →
  weaken*ʳ Δ (var x) ≡ var (x ≪ Δ)
weaken*ʳ-var {Γ} Δ x = cong (expr ∘ xsubstn+ Γ Δ [] (snd Δ [])) (case-≪ x [])

weaken+-var₀ : ∀ B Γ Δ {T} →
  weaken+ (T ∷ B) Γ Δ (var₀ {B ++ Δ}) ≡ var₀ {B ++ Γ ++ Δ}
weaken+-var₀ B Γ Δ {T} =
  cong (var ∘ xsubstn+ (T ∷ B) (Γ ++ Δ) Δ (snd Γ Δ)) (case-≪ (singleton T ≪ B) Δ)

-- Substitution respects extensional equality

substn+-cong : ∀ {k} B Γ Δ {σ : Substn k Γ Δ} {ρ : Substn k Γ Δ} →
  (σ ≈ ρ) → ∀ {T} M → substn+ B Γ Δ σ {T} M ≡ substn+ B Γ Δ ρ M
substn+-cong B Γ Δ σ≈ρ (const c) = refl
substn+-cong B Γ Δ σ≈ρ (abs T M) = cong (abs {B ++ Γ} T) (substn+-cong (T ∷ B) Γ Δ σ≈ρ M)
substn+-cong B Γ Δ σ≈ρ (app M N) = cong₂ app (substn+-cong B Γ Δ σ≈ρ M) (substn+-cong B Γ Δ σ≈ρ N)
substn+-cong B Γ Δ σ≈ρ (var x)   = cong expr (xsubstn+-cong B Γ Δ σ≈ρ (case B Δ x)) where

  xsubstn+-cong : ∀ {k} B Γ Δ {σ : Substn k Γ Δ} {ρ : Substn k Γ Δ} →
    (σ ≈ ρ) → ∀ {T} x → xsubstn+ B Γ Δ σ {T} x ≡ xsubstn+ B Γ Δ ρ x
  xsubstn+-cong {var}     B Γ Δ σ≈ρ (inj₁ x) = refl
  xsubstn+-cong {exp var} B Γ Δ σ≈ρ (inj₁ x) = refl
  xsubstn+-cong {var}     B Γ Δ σ≈ρ (inj₂ x) = cong (_≫_ B) (σ≈ρ x)
  xsubstn+-cong {exp var} B Γ Δ σ≈ρ (inj₂ x) = cong (substn+ [] (B ++ Γ) Γ (snd B Γ)) (σ≈ρ x)

substn*-cong : ∀ {k Γ Δ} {σ : Substn k Γ Δ} {ρ : Substn k Γ Δ} →
  (σ ≈ ρ) → ∀ {T} M → substn* σ {T} M ≡ substn* ρ M
substn*-cong {k} {Γ} {Δ} = substn+-cong [] Γ Δ

-- Identity of substitutions

xsubstn+-id : ∀ {k} B Γ {T} (x : Case T B Γ) →
  expr (xsubstn+ B Γ Γ (id {k} Γ) x) ≡ var (case⁻¹ x)
xsubstn+-id {var}     B Γ (inj₁ x) = refl
xsubstn+-id {exp var} B Γ (inj₁ x) = refl
xsubstn+-id {var}     B Γ (inj₂ x) = refl
xsubstn+-id {exp var} B Γ (inj₂ x) = weaken*-var B x

substn+-id : ∀ {k} B Γ {T} (M : Exp (B ++ Γ) T) → substn+ B Γ Γ (id {k} Γ) M ≡ M
substn+-id B Γ (const c) = refl
substn+-id B Γ (abs T M) = cong (abs {B ++ Γ} T) (substn+-id (T ∷ B) Γ M)
substn+-id B Γ (app M N) = cong₂ app (substn+-id B Γ M) (substn+-id B Γ N)
substn+-id {k} B Γ (var x)   =
  begin
    substn+ B Γ Γ (id {k} Γ) (var x)
  ≡⟨ xsubstn+-id {k} B Γ (case B Γ x) ⟩
    var (case⁻¹ (case B Γ x))
  ≡⟨ cong var (case-iso B Γ x) ⟩
    var x
  ∎

substn*-id : ∀ {k Γ T} (M : Exp Γ T) → substn* (id {k} Γ) M ≡ M
substn*-id {k} {Γ} = substn+-id [] Γ

weaken*-[] : ∀ {Γ T} (M : Exp Γ T) → weaken* [] M ≡ M
weaken*-[] M = substn*-id M

mutual

  -- Composition of substitutions

  substn+-∙ : ∀ {k l} B Γ Δ E (σ : Substn k Γ Δ) (ρ : Substn l Δ E) {T} (M : Exp (B ++ E) T) →
    (substn+ B Γ Δ σ (substn+ B Δ E ρ M) ≡ substn+ B Γ E (σ ∙ ρ) M)
  substn+-∙ B Γ Δ E ρ σ (const c) = refl
  substn+-∙ B Γ Δ E ρ σ (abs T M) = cong (abs {B ++ Γ} T) (substn+-∙ (T ∷ B) Γ Δ E ρ σ M)
  substn+-∙ B Γ Δ E ρ σ (app M N) = cong₂ app (substn+-∙ B Γ Δ E ρ σ M) (substn+-∙ B Γ Δ E ρ σ N)
  substn+-∙ B Γ Δ E ρ σ (var x)   = xsubstn+-∙ B Γ Δ E ρ σ (case B E x) where

    xsubstn+-∙ : ∀ {k l} B Γ Δ E (σ : Substn k Γ Δ) (ρ : Substn l Δ E) {T} (x : Case T B E) →
      (substn+ B Γ Δ σ (expr (xsubstn+ B Δ E ρ x)) ≡ expr (xsubstn+ B Γ E (σ ∙ ρ) x))
    xsubstn+-∙ {k}       {var}     B Γ Δ E σ ρ (inj₁ x) =
      cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
    xsubstn+-∙ {var}     {exp var} B Γ Δ E σ ρ (inj₁ x) =
      cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
    xsubstn+-∙ {exp var} {exp var} B Γ Δ E σ ρ (inj₁ x) =
      cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≪ x Δ)
    xsubstn+-∙ {var}     {var}     B Γ Δ E σ ρ (inj₂ x) =
      cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≫ B (ρ x))
    xsubstn+-∙ {exp var} {var}     B Γ Δ E σ ρ (inj₂ x) =
      cong (expr ∘ xsubstn+ B Γ Δ σ) (case-≫ B (ρ x))
    xsubstn+-∙ {var}     {exp var} B Γ Δ E σ ρ (inj₂ x) =
      begin
        substn+ B Γ Δ σ (weaken* B (ρ x))
      ≡⟨ substn+* B Γ Δ σ (weaken* B (ρ x)) ⟩
        substn* (id B +++ σ) (weaken* B (ρ x))
      ≡⟨ substn+-∙ [] (B ++ Γ) (B ++ Δ) Δ (id B +++ σ) (snd B Δ) (ρ x) ⟩
        substn* ((id B +++ σ) ∙ snd B Δ) (ρ x)
      ≡⟨ substn*-cong (λ y → cong (par (id B) σ) (case-≫ B y)) (ρ x) ⟩
        substn* (snd B Γ ∙ σ) (ρ x)
      ≡⟨ sym (substn+-∙ [] (B ++ Γ) Γ Δ (snd B Γ) σ (ρ x)) ⟩
        weaken* B (substn* σ (ρ x))
      ∎
    xsubstn+-∙ {exp var} {exp var} B Γ Δ E σ ρ (inj₂ x) =
      begin
        substn+ B Γ Δ σ (weaken* B (ρ x))
      ≡⟨ substn+* B Γ Δ σ (weaken* B (ρ x)) ⟩
        substn* (id B +++ σ) (weaken* B (ρ x))
      ≡⟨ substn+-∙ [] (B ++ Γ) (B ++ Δ) Δ (id B +++ σ) (snd B Δ) (ρ x) ⟩
        substn* ((id B +++ σ) ∙ snd B Δ) (ρ x)
      ≡⟨ substn*-cong (λ y → cong (par (id B) σ) (case-≫ B y))(ρ x) ⟩
        substn* (snd B Γ ∙ σ) (ρ x)
      ≡⟨ sym (substn+-∙ [] (B ++ Γ) Γ Δ (snd B Γ) σ (ρ x)) ⟩
        weaken* B (substn* σ (ρ x))
      ∎

  substn*-∙ : ∀ {k l Γ Δ E} (σ : Substn k Γ Δ) (ρ : Substn l Δ E) {T} (M : Exp E T) →
    (substn* σ (substn* ρ M) ≡ substn* (σ ∙ ρ) M)
  substn*-∙ {k} {l} {Γ} {Δ} {E} = substn+-∙ [] Γ Δ E

  -- Proof uses the fact that substn+ is an instance of substn*

  substn++ : ∀ {k} A B Γ Δ (σ : Substn k Γ Δ) {T} (M : Exp (A ++ B ++ Δ) T) →
    substn+ (A ++ B) Γ Δ σ M ≡ substn+ A (B ++ Γ) (B ++ Δ) (id B +++ σ) M
  substn++ A B Γ Δ σ (const c) = refl
  substn++ A B Γ Δ σ (abs T M) = cong (abs {A ++ B ++ Γ} T) (substn++ (T ∷ A) B Γ Δ σ M)
  substn++ A B Γ Δ σ (app M N) = cong₂ app (substn++ A B Γ Δ σ M) (substn++ A B Γ Δ σ N)
  substn++ A B Γ Δ σ (var x)   = cong expr (begin
      xsubstn+ (A ++ B) Γ Δ σ (case (A ++ B) Δ x)
    ≡⟨ cong (xsubstn+ (A ++ B) Γ Δ σ) (sym (caseˡ₃ A B Δ x)) ⟩
      xsubstn+ (A ++ B) Γ Δ σ (caseˡ (case₃ A B Δ x))
    ≡⟨ xsubstn++ A B Γ Δ σ (case₃ A B Δ x) ⟩
      xsubstn+ A (B ++ Γ) (B ++ Δ) (id B +++ σ) (caseʳ (case₃ A B Δ x))
    ≡⟨ cong (xsubstn+ A (B ++ Γ) (B ++ Δ) (id B +++ σ)) (caseʳ₃ A B Δ x) ⟩
      xsubstn+ A (B ++ Γ) (B ++ Δ) (id B +++ σ) (case A (B ++ Δ) x)
    ∎) where

    xsubstn++ : ∀ {k} A B Γ Δ (σ : Substn k Γ Δ) {T} (x : Case₃ T A B Δ) →
      xsubstn+ (A ++ B) Γ Δ σ (caseˡ x) ≡ xsubstn+ A (B ++ Γ) (B ++ Δ) (id B +++ σ) (caseʳ x)
    xsubstn++           A B Γ Δ σ (inj₁ x) = refl
    xsubstn++ {var}     A B Γ Δ σ (inj₂ x) = cong (λ X → A ≫ par (id B) σ X) (sym (case-≪ x Δ))
    xsubstn++ {exp var} A B Γ Δ σ (inj₂ x) =
      begin
        var (A ≫ x ≪ Γ)
      ≡⟨ sym (weaken*-var A (x ≪ Γ)) ⟩
        weaken* A (var (x ≪ Γ))
      ≡⟨ cong (weaken* A) (sym (weaken*ʳ-var Γ x)) ⟩
        weaken* A (weaken*ʳ Γ (var x))
      ≡⟨ cong (weaken* A ∘ par (id B) σ) (sym (case-≪ x Δ)) ⟩
        weaken* A ((id B +++ σ) (x ≪ Δ))
      ∎
    xsubstn++ {var}     A B Γ Δ σ (inj₃ x) = cong (λ X → A ≫ par (id B) σ X) (sym (case-≫ B x))
    xsubstn++ {exp var} A B Γ Δ σ (inj₃ x) =
      begin
        weaken* (A ++ B) (σ x)
      ≡⟨ sym (substn*-∙ (snd A (B ++ Γ)) (snd B Γ) (σ x)) ⟩
        weaken* A (weaken* B (σ x))
      ≡⟨ cong (weaken* A ∘ par (id B) σ) (sym (case-≫ B x)) ⟩
        weaken* A ((id B +++ σ) (B ≫ x))
      ∎

  substn+* : ∀ {k} B Γ Δ (σ : Substn k Γ Δ) {T} (M : Exp (B ++ Δ) T) →
    substn+ B Γ Δ σ M ≡ substn* (id B +++ σ) M
  substn+* = substn++ []

-- Weakening of weakening is weakening

weaken*-++ : ∀ A B Γ {T} (M : Exp Γ T) →
  weaken* A (weaken* B M) ≡ weaken* (A ++ B) M
weaken*-++ A B Γ = substn*-∙ (snd A (B ++ Γ)) (snd B Γ)

-- Weakening commutes with weakening

weaken*-comm : ∀ A B Γ Δ {U} (M : Exp (B ++ Δ) U) →
  weaken* A (weaken+ B Γ Δ M)
    ≡ weaken+ (A ++ B) Γ Δ (weaken* A M)
weaken*-comm A B Γ Δ M =
  begin
    weaken* A (weaken+ B Γ Δ M)
  ≡⟨ cong (substn* (snd A (B ++ Γ ++ Δ))) (substn+* B (Γ ++ Δ) Δ (snd Γ Δ) M) ⟩
    substn* (snd A (B ++ Γ ++ Δ)) (substn* (id B +++ snd Γ Δ) M)
  ≡⟨ substn*-∙ (snd A (B ++ Γ ++ Δ)) (id B +++ snd Γ Δ) M ⟩
    substn* (snd A (B ++ Γ ++ Δ) ∙ (id B +++ snd Γ Δ)) M
  ≡⟨ substn*-cong lemma₂ M ⟩
    substn* ((id (A ++ B) +++ snd Γ Δ) ∙ snd A (B ++ Δ)) M
  ≡⟨ sym (substn*-∙ (id (A ++ B) +++ snd Γ Δ) (snd A (B ++ Δ)) M) ⟩
    substn* (id (A ++ B) +++ snd Γ Δ) (substn* (snd A (B ++ Δ)) M)
  ≡⟨ sym (substn+* (A ++ B) (Γ ++ Δ) Δ (snd Γ Δ) (substn* (snd A (B ++ Δ)) M)) ⟩
    weaken+ (A ++ B) Γ Δ (weaken* A M)
  ∎ where

  lemma₁ : ∀ {T} (x : Case T B Δ) →
    snd A (B ++ Γ ++ Δ) (par (id B) (snd Γ Δ) x)
      ≡ (par (id (A ++ B)) (snd Γ Δ) (A ⋙ x))
  lemma₁ (inj₁ x) = refl
  lemma₁ (inj₂ x) = refl

  lemma₂ : (snd A (B ++ Γ ++ Δ) ∙ (id B +++ snd Γ Δ)) ≈ ((id (A ++ B) +++ snd Γ Δ) ∙ snd A (B ++ Δ))
  lemma₂ {T} x =
    begin
      snd A (B ++ Γ ++ Δ) (par (id B) (snd Γ Δ) (case B Δ x))
    ≡⟨ lemma₁ (case B Δ x) ⟩
      par (id (A ++ B)) (snd Γ Δ) (A ⋙ (case B Δ x))
    ≡⟨ cong (par (id (A ++ B)) (snd Γ Δ)) (case-⋙ A B Δ x) ⟩
      par (id (A ++ B)) (snd Γ Δ) (case (A ++ B) Δ (A ≫ x))
    ∎

weaken-comm : ∀ T B Γ Δ {U} (M : Exp (B ++ Δ) U) →
  weaken T (weaken+ B Γ Δ M)
    ≡ weaken+ (T ∷ B) Γ Δ (weaken T M)
weaken-comm T = weaken*-comm [ T ]

-- Weakening distributes through susbtn

weaken-substn : ∀ B Γ Δ {T U} (M : Exp (B ++ Δ) T) (N : Exp (T ∷ B ++ Δ) U) →
  substn (weaken+ B Γ Δ M) (weaken+ (T ∷ B) Γ Δ N)
    ≡ weaken+ B Γ Δ (substn M N)
weaken-substn B Γ Δ {T} M N = begin
    substn (weaken+ B Γ Δ M) (weaken+ (T ∷ B) Γ Δ N)
  ≡⟨ cong₂ substn (substn+* B (Γ ++ Δ) Δ (snd Γ Δ) M) (substn+* (T ∷ B) (Γ ++ Δ) Δ (snd Γ Δ) N) ⟩
    substn (substn* (id B +++ snd Γ Δ) M) (substn* (id (T ∷ B) +++ snd Γ Δ) N)
  ≡⟨ substn*-∙ (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) (id (T ∷ B) +++ snd Γ Δ) N ⟩
    substn* ((substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ∙ (id (T ∷ B) +++ snd Γ Δ)) N
  ≡⟨ substn*-cong lemma₂ N ⟩
    substn* ((id B +++ snd Γ Δ) ∙ (M ◁ id (B ++ Δ))) N
  ≡⟨ sym (substn*-∙ (id B +++ snd Γ Δ) (M ◁ id (B ++ Δ)) N) ⟩
    substn* (id B +++ snd Γ Δ) (substn M N)
  ≡⟨ sym (substn+* B (Γ ++ Δ) Δ (snd Γ Δ) (substn M N)) ⟩
    weaken+ B Γ Δ (substn M N)
  ∎ where

  lemma₁ : ∀ {S} (x : Case₃ S [ T ] B Δ) →
    (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ))
      (par (id (T ∷ B)) (snd Γ Δ) (caseˡ x))
        ≡ substn* (id B +++ snd Γ Δ)
            (choose ⟨ M ⟩ (id (B ++ Δ)) (caseʳ x))
  lemma₁ (inj₁ x) = begin
      (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) (x ≪ B ≪ Γ ≪ Δ)
    ≡⟨ cong (choose ⟨ substn* (id B +++ snd Γ Δ) M ⟩ (id (B ++ Γ ++ Δ))) (case-≪ x (B ++ Γ ++ Δ)) ⟩
      ⟨ substn* (id B +++ snd Γ Δ) M ⟩ x
    ≡⟨ subst-natural (uniq x) (substn* (id B +++ snd Γ Δ)) M ⟩
      substn* (id B +++ snd Γ Δ) (⟨ M ⟩ x)
    ∎
  lemma₁ (inj₂ x) = begin
      (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ([ T ] ≫ x ≪ Γ ≪ Δ)
    ≡⟨ cong (choose ⟨ substn* (id B +++ snd Γ Δ) M ⟩ (id (B ++ Γ ++ Δ))) (case-≫ [ T ] (x ≪ Γ ≪ Δ)) ⟩
      var (x ≪ Γ ≪ Δ)
    ≡⟨ cong (var ∘ par (id B) (snd Γ Δ)) (sym (case-≪ x Δ)) ⟩
      var ((id B +++ snd Γ Δ) (x ≪ Δ))
    ≡⟨ cong (var ∘ xsubstn+ [] (B ++ Γ ++ Δ) (B ++ Δ) (id B +++ snd Γ Δ)) (sym (case-≫ [] (x ≪ Δ))) ⟩
      substn* (id B +++ snd Γ Δ) (var (x ≪ Δ))
    ∎
  lemma₁ (inj₃ x) = begin
      (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ([ T ] ≫ B ≫ Γ ≫ x)
    ≡⟨ cong (choose ⟨ substn* (id B +++ snd Γ Δ) M ⟩ (id (B ++ Γ ++ Δ))) (case-≫ [ T ] (B ≫ Γ ≫ x)) ⟩
      var (B ≫ Γ ≫ x)
    ≡⟨ cong (var ∘ par (id B) (snd Γ Δ)) (sym (case-≫ B x)) ⟩
      var ((id B +++ snd Γ Δ) (B ≫ x))
    ≡⟨ cong (var ∘ xsubstn+ [] (B ++ Γ ++ Δ) (B ++ Δ) (id B +++ snd Γ Δ)) (sym (case-≫ [] (B ≫ x))) ⟩
      substn* (id B +++ snd Γ Δ) (var (B ≫ x))
    ∎

  lemma₂ : ((substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ∙ (id (T ∷ B) +++ snd Γ Δ))
    ≈ ((id B +++ snd Γ Δ) ∙ (M ◁ id (B ++ Δ)))
  lemma₂ {S} x = begin
      ((substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ)) ∙ (id (T ∷ B) +++ snd Γ Δ)) x
    ≡⟨ cong (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ) ∘ par (id (T ∷ B)) (snd Γ Δ))
         (sym (caseˡ₃ [ T ] B Δ x)) ⟩
      (substn* (id B +++ snd Γ Δ) M ◁ id (B ++ Γ ++ Δ))
        (par (id (T ∷ B)) (snd Γ Δ) (caseˡ (case₃ [ T ] B Δ x)))
    ≡⟨ lemma₁ (case₃ [ T ] B Δ x) ⟩
      substn* (id B +++ snd Γ Δ)
        (choose ⟨ M ⟩ (id (B ++ Δ)) (caseʳ (case₃ [ T ] B Δ x)))
    ≡⟨ cong (substn* (id B +++ snd Γ Δ) ∘ choose ⟨ M ⟩ (id (B ++ Δ)))
         (caseʳ₃ [ T ] B Δ x) ⟩
      ((id B +++ snd Γ Δ) ∙ (M ◁ id (B ++ Δ))) x
    ∎

-- Substitution into weakening discards the substitution

substn-weaken : ∀ {Γ T U} (M : Exp Γ U) (N : Exp Γ T) →
  substn N (weaken T M) ≡ M
substn-weaken {Γ} {T} M N =
  begin
    substn N (weaken T M)
  ≡⟨ substn*-∙ (N ◁ id Γ) (snd [ T ] Γ) M ⟩
    substn* ((N ◁ id Γ) ∙ snd [ T ] Γ) M
  ≡⟨ substn*-cong (λ x → cong (choose ⟨ N ⟩ (id Γ)) (case-≫ [ T ] x)) M ⟩
    substn* (id Γ) M
  ≡⟨ substn*-id M ⟩
    M
  ∎

-- Substitution + weakening respects ◁

substn*-◁ : ∀ Γ Δ E {T U} (M : Exp (T ∷ Γ) U) (N : Exp (E ++ Δ) T) (σ : Substn (exp var) Δ Γ) →
  substn* (N ◁ weakens* E σ) M
    ≡ substn N (weaken+ [ T ] E Δ (substn+ [ T ] Δ Γ σ M))
substn*-◁ Γ Δ E {T} M N σ =
  begin
    substn* (N ◁ weakens* E σ) M
  ≡⟨ substn*-cong (λ x → lemma (case [ T ] Γ x)) M ⟩
    substn* ((N ◁ id (E ++ Δ)) ∙ (id [ T ] +++ (snd E Δ ∙ σ))) M
  ≡⟨ sym (substn*-∙ (N ◁ id (E ++ Δ)) (id [ T ] +++ (snd E Δ ∙ σ)) M) ⟩
    substn N (substn* (id [ T ] +++ (snd E Δ ∙ σ)) M)
  ≡⟨ cong (substn N) (sym (substn+* [ T ] (E ++ Δ) Γ (snd E Δ ∙ σ) M)) ⟩
    substn N (substn+ [ T ] (E ++ Δ) Γ (snd E Δ ∙ σ) M)
  ≡⟨ cong (substn N) (sym (substn+-∙ [ T ] (E ++ Δ) Δ Γ (snd E Δ) σ M)) ⟩
    substn N (weaken+ [ T ] E Δ (substn+ [ T ] Δ Γ σ M))
  ∎ where

  lemma : ∀ {U} (x : Case U [ T ] Γ) →
    choose ⟨ N ⟩ (weakens* E σ) x
      ≡ substn N (par (id [ T ]) (snd E Δ ∙ σ) x)
  lemma (inj₁ x) =
    begin
      subst (Exp (E ++ Δ)) (uniq x) N
    ≡⟨ cong (choose ⟨ N ⟩ (id (E ++ Δ))) (sym (case-≪ x (E ++ Δ))) ⟩
      (N ◁ id (E ++ Δ)) (x ≪ E ≪ Δ)
    ≡⟨ sym (weaken*-[] ((N ◁ id (E ++ Δ)) (x ≪ E ≪ Δ))) ⟩
      weaken* [] ((N ◁ id (E ++ Δ)) (x ≪ E ≪ Δ))
    ≡⟨ cong (xsubstn+ [] (E ++ Δ) ([ T ] ++ E ++ Δ) (N ◁ id (E ++ Δ)))
         (sym (case-≫ [] (x ≪ E ≪ Δ))) ⟩
     substn N (var (x ≪ E ≪ Δ))
    ≡⟨ cong (substn N) (sym (weaken*ʳ-var (E ++ Δ) x)) ⟩
     substn N (weaken*ʳ (E ++ Δ) (var x))
    ∎
  lemma (inj₂ x) = sym (substn-weaken (weaken* E (σ x)) N)

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


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

open import Level using (Level)

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; foldr; zipWith; map)

open import FLA.Algebra.Structures
open import FLA.Algebra.Properties.Field

module FLA.Algebra.LinearAlgebra where

private
  variable
    ℓ : Level
    A : Set ℓ
    m n p q : ℕ

module _ {ℓ : Level} {A : Set ℓ} ⦃ F : Field A ⦄ where
  open Field F

  -- Vector addition
  _+ⱽ_ : Vec A n → Vec A n → Vec A n
  _+ⱽ_ = zipWith _+_

  -- Vector substraction
  _-ⱽ_ : Vec A n → Vec A n → Vec A n
  a -ⱽ b = a +ⱽ (map (-_) b)

  -- Vector Hadamard product
  _*ⱽ_ : Vec A n → Vec A n → Vec A n
  _*ⱽ_ = zipWith _*_

  -- Multiply vector by a constant
  _∘ⱽ_ : A → Vec A n → Vec A n
  c ∘ⱽ v = map (c *_) v

  -- Match the fixity of Haskell
  infixl  6 _+ⱽ_
  infixl  6 _-ⱽ_
  infixl  7 _*ⱽ_
  infixl 10 _∘ⱽ_

  sum : Vec A n → A
  sum = foldr _ _+_ 0ᶠ

  -- Inner product
  ⟨_,_⟩ : Vec A n → Vec A n → A
  ⟨ v₁ , v₂ ⟩ = sum (v₁ *ⱽ v₂)

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


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

module Generics.HasDesc where

open import Data.String.Base

open import Generics.Prelude hiding (lookup ; pi)
open import Generics.Telescope
open import Generics.Desc

import Generics.Accessibility as Accessibility

private
  variable
    P  : Telescope ⊤
    I  : ExTele P
    pi : ⟦ P , I ⟧xtel

record HasDesc {ℓ} (A : Indexed P I ℓ) : Setω where
  A′ : ⟦ P , I ⟧xtel → Set ℓ
  A′ = uncurry P I A

  field
    {n} : ℕ
    D   : DataDesc P I n

    names : Vec String n

    constr : ⟦ D ⟧Data A′ pi → A′ pi
    split  : A′ pi → ⟦ D ⟧Data A′ pi

    constr∘split : (x : A′ pi          ) → constr (split x) ≡  x
    split∘constr : (x : ⟦ D ⟧Data A′ pi) → split (constr x) ≡ω x

  open Accessibility A D split public

  field wf : (x : A′ pi) → Acc x

  split-injective : ∀ {pi} {x y : A′ pi} → split x ≡ω split y → x ≡ y
  split-injective {x = x} {y} sx≡sy = begin
    x                ≡⟨ sym (constr∘split x) ⟩
    constr (split x) ≡⟨ congω constr sx≡sy   ⟩
    constr (split y) ≡⟨ constr∘split y       ⟩
    y                ∎ where open ≡-Reasoning

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about subsets
------------------------------------------------------------------------

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

module Data.Fin.Subset.Properties where

open import Algebra
import Algebra.FunctionProperties as AlgebraicProperties
import Algebra.Structures as AlgebraicStructures
import Algebra.Properties.Lattice as L
import Algebra.Properties.DistributiveLattice as DL
import Algebra.Properties.BooleanAlgebra as BA
open import Data.Bool.Properties
open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Subset
open import Data.Fin.Properties using (any?; decFinSubset)
open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s; _≤_)
open import Data.Nat.Properties using (≤-step)
open import Data.Product as Product using (∃; ∄; _×_; _,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec
open import Data.Vec.Properties
open import Function using (_∘_; const; id; case_of_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; subst; isEquivalence)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Unary using (Pred; Decidable)

------------------------------------------------------------------------
-- Constructor mangling

drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p
drop-there (there x∈p) = x∈p

drop-∷-⊆ : ∀ {n s₁ s₂} {p₁ p₂ : Subset n} → s₁ ∷ p₁ ⊆ s₂ ∷ p₂ → p₁ ⊆ p₂
drop-∷-⊆ p₁s₁⊆p₂s₂ x∈p₁ = drop-there (p₁s₁⊆p₂s₂ (there x∈p₁))

------------------------------------------------------------------------
-- _∈_

infix 4 _∈?_
_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
zero  ∈? inside  ∷ p = yes here
zero  ∈? outside ∷ p = no  λ()
suc n ∈? s       ∷ p with n ∈? p
... | yes n∈p = yes (there n∈p)
... | no  n∉p = no  (n∉p ∘ drop-there)

------------------------------------------------------------------------
-- Empty

drop-∷-Empty : ∀ {n s} {p : Subset n} → Empty (s ∷ p) → Empty p
drop-∷-Empty ¬∃∈ (x , x∈p) = ¬∃∈ (suc x , there x∈p)

Empty-unique : ∀ {n} {p : Subset n} → Empty p → p ≡ ⊥
Empty-unique {_} {[]}          ¬∃∈ = refl
Empty-unique {_} {inside  ∷ p} ¬∃∈ = contradiction (zero , here) ¬∃∈
Empty-unique {_} {outside ∷ p} ¬∃∈ =
  cong (outside ∷_) (Empty-unique (drop-∷-Empty ¬∃∈))

nonempty? : ∀ {n} → Decidable (Nonempty {n})
nonempty? p = any? (_∈? p)

------------------------------------------------------------------------
-- ∣_∣

∣p∣≤n : ∀ {n} (p : Subset n) → ∣ p ∣ ≤ n
∣p∣≤n = count≤n (_≟ inside)

------------------------------------------------------------------------
-- ⊥

∉⊥ : ∀ {n} {x : Fin n} → x ∉ ⊥
∉⊥ (there p) = ∉⊥ p

⊥⊆ : ∀ {n} {p : Subset n} → ⊥ ⊆ p
⊥⊆ x∈⊥ = contradiction x∈⊥ ∉⊥

∣⊥∣≡0 : ∀ n → ∣ ⊥ {n = n} ∣ ≡ 0
∣⊥∣≡0 zero    = refl
∣⊥∣≡0 (suc n) = ∣⊥∣≡0 n

------------------------------------------------------------------------
-- ⊤

∈⊤ : ∀ {n} {x : Fin n} → x ∈ ⊤
∈⊤ {x = zero}  = here
∈⊤ {x = suc x} = there ∈⊤

⊆⊤ : ∀ {n} {p : Subset n} → p ⊆ ⊤
⊆⊤ = const ∈⊤

∣⊤∣≡n : ∀ n → ∣ ⊤ {n = n} ∣ ≡ n
∣⊤∣≡n zero    = refl
∣⊤∣≡n (suc n) = cong suc (∣⊤∣≡n n)

------------------------------------------------------------------------
-- ⁅_⁆

x∈⁅x⁆ : ∀ {n} (x : Fin n) → x ∈ ⁅ x ⁆
x∈⁅x⁆ zero    = here
x∈⁅x⁆ (suc x) = there (x∈⁅x⁆ x)

x∈⁅y⁆⇒x≡y : ∀ {n x} (y : Fin n) → x ∈ ⁅ y ⁆ → x ≡ y
x∈⁅y⁆⇒x≡y zero    here      = refl
x∈⁅y⁆⇒x≡y zero    (there p) = contradiction p ∉⊥
x∈⁅y⁆⇒x≡y (suc y) (there p) = cong suc (x∈⁅y⁆⇒x≡y y p)

x∈⁅y⁆⇔x≡y : ∀ {n} {x y : Fin n} → x ∈ ⁅ y ⁆ ⇔ x ≡ y
x∈⁅y⁆⇔x≡y {_} {x} {y} = equivalence
  (x∈⁅y⁆⇒x≡y y)
  (λ x≡y → subst (λ y → x ∈ ⁅ y ⁆) x≡y (x∈⁅x⁆ x))

∣⁅x⁆∣≡1 : ∀ {n} (i : Fin n) → ∣ ⁅ i ⁆ ∣ ≡ 1
∣⁅x⁆∣≡1 {suc n} zero    = cong suc (∣⊥∣≡0 n)
∣⁅x⁆∣≡1 {_}     (suc i) = ∣⁅x⁆∣≡1 i

------------------------------------------------------------------------
-- _⊆_

⊆-refl : ∀ {n} → Reflexive (_⊆_ {n})
⊆-refl = id

⊆-reflexive : ∀ {n} → _≡_ ⇒ (_⊆_ {n})
⊆-reflexive refl = ⊆-refl

⊆-trans : ∀ {n} → Transitive (_⊆_ {n})
⊆-trans p⊆q q⊆r x∈p = q⊆r (p⊆q x∈p)

⊆-antisym : ∀ {n} → Antisymmetric _≡_ (_⊆_ {n})
⊆-antisym {i = []}     {[]}     p⊆q q⊆p = refl
⊆-antisym {i = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y
... | inside  | inside  = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p))
... | inside  | outside = contradiction (p⊆q here) λ()
... | outside | inside  = contradiction (q⊆p here) λ()
... | outside | outside = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p))

⊆-min : ∀ {n} → Minimum (_⊆_ {n}) ⊥
⊆-min []       ()
⊆-min (x ∷ xs) (there v∈⊥) = there (⊆-min xs v∈⊥)

⊆-max : ∀ {n} → Maximum (_⊆_ {n}) ⊤
⊆-max []            ()
⊆-max (inside ∷ xs) here         = here
⊆-max (x      ∷ xs) (there v∈xs) = there (⊆-max xs v∈xs)

infix 4 _⊆?_
_⊆?_ : ∀ {n} → B.Decidable (_⊆_ {n = n})
[]          ⊆? []          = yes id
outside ∷ p ⊆? y ∷ q with p ⊆? q
... | yes p⊆q = yes λ { (there v∈p) → there (p⊆q v∈p)}
... | no  p⊈q = no (p⊈q ∘ drop-∷-⊆)
inside  ∷ p ⊆? outside ∷ q = no (λ p⊆q → case (p⊆q here) of λ())
inside  ∷ p ⊆? inside  ∷ q with p ⊆? q
... | yes p⊆q = yes λ { here → here ; (there v) → there (p⊆q v)}
... | no  p⊈q = no (p⊈q ∘ drop-∷-⊆)

module _ (n : ℕ) where

  ⊆-isPreorder : IsPreorder _≡_ (_⊆_ {n})
  ⊆-isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = ⊆-reflexive
    ; trans         = ⊆-trans
    }

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = record
    { isPreorder = ⊆-isPreorder
    }

  ⊆-isPartialOrder : IsPartialOrder _≡_ (_⊆_ {n})
  ⊆-isPartialOrder = record
    { isPreorder = ⊆-isPreorder
    ; antisym    = ⊆-antisym
    }

  ⊆-poset : Poset _ _ _
  ⊆-poset = record
    { isPartialOrder = ⊆-isPartialOrder
    }

p⊆q⇒∣p∣<∣q∣ : ∀ {n} {p q : Subset n} → p ⊆ q → ∣ p ∣ ≤ ∣ q ∣
p⊆q⇒∣p∣<∣q∣ {p = []}          {[]}          p⊆q = z≤n
p⊆q⇒∣p∣<∣q∣ {p = outside ∷ p} {outside ∷ q} p⊆q = p⊆q⇒∣p∣<∣q∣ (drop-∷-⊆ p⊆q)
p⊆q⇒∣p∣<∣q∣ {p = outside ∷ p} {inside  ∷ q} p⊆q = ≤-step (p⊆q⇒∣p∣<∣q∣ (drop-∷-⊆ p⊆q))
p⊆q⇒∣p∣<∣q∣ {p = inside  ∷ p} {outside ∷ q} p⊆q = contradiction (p⊆q here) λ()
p⊆q⇒∣p∣<∣q∣ {p = inside  ∷ p} {inside  ∷ q} p⊆q = s≤s (p⊆q⇒∣p∣<∣q∣ (drop-∷-⊆ p⊆q))

------------------------------------------------------------------------
-- _∩_

module _ {n : ℕ} where

  open AlgebraicProperties {A = Subset n} _≡_

  ∩-assoc : Associative _∩_
  ∩-assoc = zipWith-assoc ∧-assoc

  ∩-comm : Commutative _∩_
  ∩-comm = zipWith-comm ∧-comm

  ∩-idem : Idempotent _∩_
  ∩-idem = zipWith-idem ∧-idem

  ∩-identityˡ : LeftIdentity ⊤ _∩_
  ∩-identityˡ = zipWith-identityˡ ∧-identityˡ

  ∩-identityʳ : RightIdentity ⊤ _∩_
  ∩-identityʳ = zipWith-identityʳ ∧-identityʳ

  ∩-identity : Identity ⊤ _∩_
  ∩-identity = ∩-identityˡ , ∩-identityʳ

  ∩-zeroˡ : LeftZero ⊥ _∩_
  ∩-zeroˡ = zipWith-zeroˡ ∧-zeroˡ

  ∩-zeroʳ : RightZero ⊥ _∩_
  ∩-zeroʳ = zipWith-zeroʳ ∧-zeroʳ

  ∩-zero : Zero ⊥ _∩_
  ∩-zero = ∩-zeroˡ , ∩-zeroʳ

  ∩-inverseˡ : LeftInverse ⊥ ∁ _∩_
  ∩-inverseˡ = zipWith-inverseˡ ∧-inverseˡ

  ∩-inverseʳ : RightInverse ⊥ ∁ _∩_
  ∩-inverseʳ = zipWith-inverseʳ ∧-inverseʳ

  ∩-inverse : Inverse ⊥ ∁ _∩_
  ∩-inverse = ∩-inverseˡ , ∩-inverseʳ

module _ (n : ℕ) where

  open AlgebraicStructures {A = Subset n} _≡_

  ∩-isMagma : IsMagma _∩_
  ∩-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _∩_
    }

  ∩-magma : Magma _ _
  ∩-magma = record
    { isMagma = ∩-isMagma
    }

  ∩-isSemigroup : IsSemigroup _∩_
  ∩-isSemigroup = record
    { isMagma = ∩-isMagma
    ; assoc   = ∩-assoc
    }

  ∩-semigroup : Semigroup _ _
  ∩-semigroup = record
    { isSemigroup = ∩-isSemigroup
    }

  ∩-isBand : IsBand _∩_
  ∩-isBand = record
    { isSemigroup = ∩-isSemigroup
    ; idem        = ∩-idem
    }

  ∩-band : Band _ _
  ∩-band = record
    { isBand = ∩-isBand
    }

  ∩-isSemilattice : IsSemilattice _∩_
  ∩-isSemilattice = record
    { isBand = ∩-isBand
    ; comm   = ∩-comm
    }

  ∩-semilattice : Semilattice _ _
  ∩-semilattice = record
    { isSemilattice = ∩-isSemilattice
    }

  ∩-isMonoid : IsMonoid _∩_ ⊤
  ∩-isMonoid = record
    { isSemigroup = ∩-isSemigroup
    ; identity    = ∩-identity
    }

  ∩-monoid : Monoid _ _
  ∩-monoid = record
    { isMonoid = ∩-isMonoid
    }

  ∩-isCommutativeMonoid : IsCommutativeMonoid _∩_ ⊤
  ∩-isCommutativeMonoid = record
    { isSemigroup = ∩-isSemigroup
    ; identityˡ   = ∩-identityˡ
    ; comm        = ∩-comm
    }

  ∩-commutativeMonoid : CommutativeMonoid _ _
  ∩-commutativeMonoid = record
    { isCommutativeMonoid = ∩-isCommutativeMonoid
    }

  ∩-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∩_ ⊤
  ∩-isIdempotentCommutativeMonoid = record
    { isCommutativeMonoid = ∩-isCommutativeMonoid
    ; idem                = ∩-idem
    }

  ∩-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
  ∩-idempotentCommutativeMonoid = record
    { isIdempotentCommutativeMonoid = ∩-isIdempotentCommutativeMonoid
    }

p∩q⊆p : ∀ {n} (p q : Subset n) → p ∩ q ⊆ p
p∩q⊆p []            []           x∈p∩q        = x∈p∩q
p∩q⊆p (inside  ∷ p) (inside ∷ q) here         = here
p∩q⊆p (inside  ∷ p) (_      ∷ q) (there ∈p∩q) = there (p∩q⊆p p q ∈p∩q)
p∩q⊆p (outside ∷ p) (_      ∷ q) (there ∈p∩q) = there (p∩q⊆p p q ∈p∩q)

p∩q⊆q : ∀ {n} (p q : Subset n) → p ∩ q ⊆ q
p∩q⊆q p q rewrite ∩-comm p q = p∩q⊆p q p

x∈p∩q⁺ : ∀ {n} {p q : Subset n} {x} → x ∈ p × x ∈ q → x ∈ p ∩ q
x∈p∩q⁺ (here      , here)      = here
x∈p∩q⁺ (there x∈p , there x∈q) = there (x∈p∩q⁺ (x∈p , x∈q))

x∈p∩q⁻ : ∀ {n} (p q : Subset n) {x} → x ∈ p ∩ q → x ∈ p × x ∈ q
x∈p∩q⁻ []           []           ()
x∈p∩q⁻ (inside ∷ p) (inside ∷ q) here          = here , here
x∈p∩q⁻ (s      ∷ p) (t      ∷ q) (there x∈p∩q) =
  Product.map there there (x∈p∩q⁻ p q x∈p∩q)

∩⇔× : ∀ {n} {p q : Subset n} {x} → x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q)
∩⇔× = equivalence (x∈p∩q⁻ _ _) x∈p∩q⁺

------------------------------------------------------------------------
-- _∪_

module _ {n : ℕ} where

  open AlgebraicProperties {A = Subset n} _≡_

  ∪-assoc : Associative _∪_
  ∪-assoc = zipWith-assoc ∨-assoc

  ∪-comm : Commutative _∪_
  ∪-comm = zipWith-comm ∨-comm

  ∪-idem : Idempotent _∪_
  ∪-idem = zipWith-idem ∨-idem

  ∪-identityˡ : LeftIdentity ⊥ _∪_
  ∪-identityˡ = zipWith-identityˡ ∨-identityˡ

  ∪-identityʳ : RightIdentity ⊥ _∪_
  ∪-identityʳ = zipWith-identityʳ ∨-identityʳ

  ∪-identity : Identity ⊥ _∪_
  ∪-identity = ∪-identityˡ , ∪-identityʳ

  ∪-zeroˡ : LeftZero ⊤ _∪_
  ∪-zeroˡ = zipWith-zeroˡ ∨-zeroˡ

  ∪-zeroʳ : RightZero ⊤ _∪_
  ∪-zeroʳ = zipWith-zeroʳ ∨-zeroʳ

  ∪-zero : Zero ⊤ _∪_
  ∪-zero = ∪-zeroˡ , ∪-zeroʳ

  ∪-inverseˡ : LeftInverse ⊤ ∁ _∪_
  ∪-inverseˡ = zipWith-inverseˡ ∨-inverseˡ

  ∪-inverseʳ : RightInverse ⊤ ∁ _∪_
  ∪-inverseʳ = zipWith-inverseʳ ∨-inverseʳ

  ∪-inverse : Inverse ⊤ ∁ _∪_
  ∪-inverse = ∪-inverseˡ , ∪-inverseʳ

  ∪-distribˡ-∩ : _∪_ DistributesOverˡ _∩_
  ∪-distribˡ-∩ = zipWith-distribˡ ∨-distribˡ-∧

  ∪-distribʳ-∩ : _∪_ DistributesOverʳ _∩_
  ∪-distribʳ-∩ = zipWith-distribʳ ∨-distribʳ-∧

  ∪-distrib-∩ : _∪_ DistributesOver _∩_
  ∪-distrib-∩ = ∪-distribˡ-∩ , ∪-distribʳ-∩

  ∩-distribˡ-∪ : _∩_ DistributesOverˡ _∪_
  ∩-distribˡ-∪ = zipWith-distribˡ ∧-distribˡ-∨

  ∩-distribʳ-∪ : _∩_ DistributesOverʳ _∪_
  ∩-distribʳ-∪ = zipWith-distribʳ ∧-distribʳ-∨

  ∩-distrib-∪ : _∩_ DistributesOver _∪_
  ∩-distrib-∪ = ∩-distribˡ-∪ , ∩-distribʳ-∪

  ∪-abs-∩ : _∪_ Absorbs _∩_
  ∪-abs-∩ = zipWith-absorbs ∨-abs-∧

  ∩-abs-∪ : _∩_ Absorbs _∪_
  ∩-abs-∪ = zipWith-absorbs ∧-abs-∨

module _ (n : ℕ) where

  open AlgebraicStructures {A = Subset n} _≡_

  ∪-isMagma : IsMagma _∪_
  ∪-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _∪_
    }

  ∪-magma : Magma _ _
  ∪-magma = record
    { isMagma = ∪-isMagma
    }

  ∪-isSemigroup : IsSemigroup _∪_
  ∪-isSemigroup = record
    { isMagma = ∪-isMagma
    ; assoc   = ∪-assoc
    }

  ∪-semigroup : Semigroup _ _
  ∪-semigroup = record
    { isSemigroup = ∪-isSemigroup
    }

  ∪-isBand : IsBand _∪_
  ∪-isBand = record
    { isSemigroup = ∪-isSemigroup
    ; idem        = ∪-idem
    }

  ∪-band : Band _ _
  ∪-band = record
    { isBand = ∪-isBand
    }

  ∪-isSemilattice : IsSemilattice _∪_
  ∪-isSemilattice = record
    { isBand = ∪-isBand
    ; comm   = ∪-comm
    }

  ∪-semilattice : Semilattice _ _
  ∪-semilattice = record
    { isSemilattice = ∪-isSemilattice
    }

  ∪-isMonoid : IsMonoid _∪_ ⊥
  ∪-isMonoid = record
    { isSemigroup = ∪-isSemigroup
    ; identity    = ∪-identity
    }

  ∪-monoid : Monoid _ _
  ∪-monoid = record
    { isMonoid = ∪-isMonoid
    }

  ∪-isCommutativeMonoid : IsCommutativeMonoid _∪_ ⊥
  ∪-isCommutativeMonoid = record
    { isSemigroup = ∪-isSemigroup
    ; identityˡ   = ∪-identityˡ
    ; comm        = ∪-comm
    }

  ∪-commutativeMonoid : CommutativeMonoid _ _
  ∪-commutativeMonoid = record
    { isCommutativeMonoid = ∪-isCommutativeMonoid
    }

  ∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∪_ ⊥
  ∪-isIdempotentCommutativeMonoid = record
    { isCommutativeMonoid = ∪-isCommutativeMonoid
    ; idem                = ∪-idem
    }

  ∪-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
  ∪-idempotentCommutativeMonoid = record
    { isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid
    }

  ∪-∩-isLattice : IsLattice _∪_ _∩_
  ∪-∩-isLattice = record
    { isEquivalence = isEquivalence
    ; ∨-comm        = ∪-comm
    ; ∨-assoc       = ∪-assoc
    ; ∨-cong        = cong₂ _∪_
    ; ∧-comm        = ∩-comm
    ; ∧-assoc       = ∩-assoc
    ; ∧-cong        = cong₂ _∩_
    ; absorptive    = ∪-abs-∩ , ∩-abs-∪
    }

  ∪-∩-lattice : Lattice _ _
  ∪-∩-lattice = record
    { isLattice = ∪-∩-isLattice
    }

  ∪-∩-isDistributiveLattice : IsDistributiveLattice _∪_ _∩_
  ∪-∩-isDistributiveLattice = record
    { isLattice    = ∪-∩-isLattice
    ; ∨-∧-distribʳ = ∪-distribʳ-∩
    }

  ∪-∩-distributiveLattice : DistributiveLattice _ _
  ∪-∩-distributiveLattice = record
    { isDistributiveLattice = ∪-∩-isDistributiveLattice
    }

  ∪-∩-isBooleanAlgebra : IsBooleanAlgebra _∪_ _∩_ ∁ ⊤ ⊥
  ∪-∩-isBooleanAlgebra = record
    { isDistributiveLattice = ∪-∩-isDistributiveLattice
    ; ∨-complementʳ         = ∪-inverseʳ
    ; ∧-complementʳ         = ∩-inverseʳ
    ; ¬-cong                = cong ∁
    }

  ∪-∩-booleanAlgebra : BooleanAlgebra _ _
  ∪-∩-booleanAlgebra = record
    { isBooleanAlgebra = ∪-∩-isBooleanAlgebra
    }

  ∩-∪-isLattice : IsLattice _∩_ _∪_
  ∩-∪-isLattice = L.∧-∨-isLattice ∪-∩-lattice

  ∩-∪-lattice : Lattice _ _
  ∩-∪-lattice = L.∧-∨-lattice ∪-∩-lattice

  ∩-∪-isDistributiveLattice : IsDistributiveLattice _∩_ _∪_
  ∩-∪-isDistributiveLattice = DL.∧-∨-isDistributiveLattice ∪-∩-distributiveLattice

  ∩-∪-distributiveLattice : DistributiveLattice _ _
  ∩-∪-distributiveLattice = DL.∧-∨-distributiveLattice ∪-∩-distributiveLattice

  ∩-∪-isBooleanAlgebra : IsBooleanAlgebra _∩_ _∪_ ∁ ⊥ ⊤
  ∩-∪-isBooleanAlgebra = BA.∧-∨-isBooleanAlgebra ∪-∩-booleanAlgebra

  ∩-∪-booleanAlgebra : BooleanAlgebra _ _
  ∩-∪-booleanAlgebra = BA.∧-∨-booleanAlgebra ∪-∩-booleanAlgebra

p⊆p∪q : ∀ {n p} (q : Subset n) → p ⊆ p ∪ q
p⊆p∪q []      ()
p⊆p∪q (s ∷ q) here        = here
p⊆p∪q (s ∷ q) (there x∈p) = there (p⊆p∪q q x∈p)

q⊆p∪q : ∀ {n} (p q : Subset n) → q ⊆ p ∪ q
q⊆p∪q p q rewrite ∪-comm p q = p⊆p∪q p

x∈p∪q⁻ :  ∀ {n} (p q : Subset n) {x} → x ∈ p ∪ q → x ∈ p ⊎ x ∈ q
x∈p∪q⁻ []            []            ()
x∈p∪q⁻ (inside  ∷ p) (t       ∷ q) here          = inj₁ here
x∈p∪q⁻ (outside ∷ p) (inside  ∷ q) here          = inj₂ here
x∈p∪q⁻ (s       ∷ p) (t       ∷ q) (there x∈p∪q) =
  Sum.map there there (x∈p∪q⁻ p q x∈p∪q)

x∈p∪q⁺ : ∀ {n} {p q : Subset n} {x} → x ∈ p ⊎ x ∈ q → x ∈ p ∪ q
x∈p∪q⁺ (inj₁ x∈p) = p⊆p∪q _   x∈p
x∈p∪q⁺ (inj₂ x∈q) = q⊆p∪q _ _ x∈q

∪⇔⊎ : ∀ {n} {p q : Subset n} {x} → x ∈ p ∪ q ⇔ (x ∈ p ⊎ x ∈ q)
∪⇔⊎ = equivalence (x∈p∪q⁻ _ _) x∈p∪q⁺

------------------------------------------------------------------------
-- Lift

Lift? : ∀ {n p} {P : Pred (Fin n) p} → Decidable P → Decidable (Lift P)
Lift? P? p = decFinSubset (_∈? p) (λ {x} _ → P? x)

------------------------------------------------------------------------
-- Other

anySubset? : ∀ {n} {P : Subset n → Set} → Decidable P → Dec (∃ P)
anySubset? {zero}  P? with P? []
... | yes P[] = yes (_ , P[])
... | no ¬P[] = no (λ {([] , P[]) → ¬P[] P[]})
anySubset? {suc n} P? with anySubset? (P? ∘ (inside ∷_))
... | yes (_ , Pp) = yes (_ , Pp)
... | no  ¬Pp      with anySubset? (P? ∘ (outside ∷_))
...   | yes (_ , Pp) = yes (_ , Pp)
...   | no ¬Pp'      = no λ
  { (inside  ∷ p , Pp)  → ¬Pp  (_ , Pp)
  ; (outside ∷ p , Pp') → ¬Pp' (_ , Pp')
  }


text:
module Haskell.Prim.Functor where

open import Haskell.Prim
open import Haskell.Prim.Either
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Tuple

--------------------------------------------------
-- Functor

record Functor (f : Set → Set) : Set₁ where
  field
    fmap : (a → b) → f a → f b

  infixl 1 _<&>_
  infixl 4 _<$>_ _<$_ _$>_

  _<$>_ : (a → b) → f a → f b
  _<$>_ = fmap

  _<&>_ : f a → (a → b) → f b
  m <&> f = fmap f m

  _<$_ : a → f b → f a
  x <$ m = fmap (const x) m

  _$>_ : f a → b → f b
  m $> x = x <$ m

  void : f a → f (Tuple [])
  void = [] <$_

open Functor ⦃ ... ⦄ public

instance
  iFunctorList : Functor List
  iFunctorList .fmap = map

  iFunctorMaybe : Functor Maybe
  iFunctorMaybe .fmap f Nothing  = Nothing
  iFunctorMaybe .fmap f (Just x) = Just (f x)

  iFunctorEither : Functor (Either a)
  iFunctorEither .fmap f (Left  x) = Left x
  iFunctorEither .fmap f (Right y) = Right (f y)

  iFunctorFun : Functor (λ b → a → b)
  iFunctorFun .fmap = _∘_

  iFunctorTuple₂ : Functor (a ×_)
  iFunctorTuple₂ .fmap f (x , y) = x , f y

  iFunctorTuple₃ : Functor (a × b ×_)
  iFunctorTuple₃ .fmap f (x , y , z) = x , y , f z

  iFunctorTuple₄ : Functor (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
  iFunctorTuple₄ .fmap f (x ∷ y ∷ z ∷ w ∷ []) = x ∷ y ∷ z ∷ f w ∷ []


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

open import lib.Base

module test.succeed.Test0 where

module _ where

  private
    data #I : Type₀ where
      #zero : #I
      #one : #I

  I : Type₀
  I = #I

  zero : I
  zero = #zero

  one : I
  one = #one

  postulate
    seg : zero == one

  I-elim : ∀ {i} {P : I → Type i} (zero* : P zero) (one* : P one)
           (seg* : zero* == one* [ P ↓ seg ]) → Π I P
  I-elim zero* one* seg* #zero = zero*
  I-elim zero* one* seg* #one = one*

  postulate
    I-seg-β : ∀ {i} {P : I → Type i} (zero* : P zero) (one* : P one)
              (seg* : zero* == one* [ P ↓ seg ])
              → apd (I-elim zero* one* seg*) seg == seg*

test : ∀ {i} {P : I → Type i} (zero* : P zero) (one* : P one)
           (seg* : zero* == one* [ P ↓ seg ]) →
       (I-elim zero* one* seg*) zero == zero*
test zero* one* seg* = idp

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

data FALSE : Set where

CONTRADICTION : ∀ {A : Set} → FALSE → A
CONTRADICTION ()

record TRUE : Set where
{-# BUILTIN UNIT TRUE #-}

data Bool : Set where
  false true : Bool
{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

data Nat : Set where
  zero : Nat
  suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)
{-# BUILTIN NATPLUS _+_ #-}

_-_ : Nat → Nat → Nat
n     - zero  = n
zero  - suc m = zero
suc n - suc m = n - m
{-# BUILTIN NATMINUS _-_ #-}

_*_ : Nat → Nat → Nat
zero  * m = zero
suc n * m = (n * m) + m
{-# BUILTIN NATTIMES _*_ #-}

_==_ : Nat → Nat → Bool
zero  == zero  = true
suc n == suc m = n == m
_     == _     = false
{-# BUILTIN NATEQUALS _==_ #-}

postulate String : Set
{-# BUILTIN STRING String #-}

primitive
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool

_+++_ = primStringAppend
_===_ = primStringEquality

data List(A : Set) : Set where
  nil : List(A)
  _::_ : A → List(A) → List(A)
{-# BUILTIN LIST List  #-}

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REWRITE _≡_ #-}

cong : ∀ {a} {X Y : Set a} {x y : X} (f : X → Y) → (x ≡ y) → (f x ≡ f y)
cong f refl = refl

_≢_ :  ∀ {a} {A : Set a} → A → A → Set a
(x ≢ y) = (x ≡ y) → FALSE

data Dec(A : Set) : Set where
  yes : A → Dec(A)
  no : (A → FALSE) → Dec(A)

primitive
  primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y

primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
primTrustMe {x = x} {y} = primEraseEquality unsafePrimTrustMe where
   postulate unsafePrimTrustMe : x ≡ y

_≟String_ : (s t : String) → Dec(s ≡ t)
(s ≟String t) with primStringEquality s t
(s ≟String t) | true = yes primTrustMe
(s ≟String t) | false = no unsafeNo where
  postulate unsafeNo : s ≢ t

_≟Nat_ : (m n : Nat) → Dec(m ≡ n)
(m ≟Nat n) with m == n
(m ≟Nat n) | true = yes primTrustMe
(m ≟Nat n) | false = no unsafeNo where
  postulate unsafeNo : m ≢ n

data _≤_ : Nat → Nat → Set where
  zero : ∀ {x} → zero ≤ x
  suc : ∀ {x y} → (x ≤ y) → (suc x ≤ suc y)

_≤?_ : (x y : Nat) → Dec(x ≤ y)
zero ≤? y = yes zero
suc x ≤? zero = no (λ ())
suc x ≤? suc y with (x ≤? y)
... | yes p = yes (suc p)
... | no  p = no  (λ { (suc q) → p q })

_<_ : Nat → Nat → Set
m < n = (n ≤ m) → FALSE

asym : ∀ {m n} → (m ≤ n) → (n ≤ m) → (m ≡ n)
asym zero zero = refl
asym (suc p) (suc q) with asym p q
asym (suc p) (suc q) | refl = refl

if : ∀ {X Y : Set} → Dec(X) → Y → Y → Y
if (yes p) x y = x
if (no  p) x y = y

+zero : ∀ {m} → (m + zero) ≡ m
+zero {zero} = refl
+zero {suc m} = cong suc +zero

+suc : ∀ {m n} → (m + suc n) ≡ suc (m + n)
+suc {zero} = refl
+suc {suc m} = cong suc +suc

{-# REWRITE +zero +suc #-}

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


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

import Data.List as List
import Data.List.Properties
open import Data.Nat using (ℕ)
import Data.Product as Product
import Data.Vec as Vec
import Data.Vec.Properties
open import Function using (id; λ-; _$-)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category.Discrete using (Discrete)
open import Categories.Category.Instance.Sets
open import Categories.Functor using (Endofunctor)
open import Categories.Functor.Bifunctor using (Bifunctor; appʳ)

List : ∀ {o} → Endofunctor (Sets o)
List = record
  { F₀ = List.List
  ; F₁ = List.map
  ; identity = map-id $-
  ; homomorphism = map-compose $-
  ; F-resp-≈ = λ f≈g → map-cong (λ- f≈g) $-
  }
  where
    open Data.List.Properties

Vec′ : ∀ {o} → Bifunctor (Sets o) (Discrete ℕ) (Sets o)
Vec′ = record
  { F₀ = Product.uncurry Vec.Vec
  ; F₁ = λ { (f , refl) → Vec.map f }
  ; identity = map-id $-
  ; homomorphism = λ { {_} {_} {_} {f , refl} {g , refl} → map-∘ g f _}
  ; F-resp-≈ = λ { {_} {_} {_} {_ , refl} (g , refl) → map-cong (λ- g) _}
  }
  where
    open Product using (_,_)
    open Data.Vec.Properties

Vec : ∀ {o} → ℕ → Endofunctor (Sets o)
Vec = appʳ Vec′


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties {{eqrel : EqRelSet}} where

open import Definition.LogicalRelation.Properties.Reflexivity public
open import Definition.LogicalRelation.Properties.Symmetry public
open import Definition.LogicalRelation.Properties.Transitivity public
open import Definition.LogicalRelation.Properties.Conversion public
open import Definition.LogicalRelation.Properties.Escape public
open import Definition.LogicalRelation.Properties.Universe public
open import Definition.LogicalRelation.Properties.Neutral public
open import Definition.LogicalRelation.Properties.Reduction public
open import Definition.LogicalRelation.Properties.Successor public
open import Definition.LogicalRelation.Properties.MaybeEmb public

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Theory

module cohomology.Unit {i} (CT : CohomologyTheory i) where

open CohomologyTheory CT

private
  ⊙LU = ⊙Lift {j = i} ⊙Unit

  G : fst (⊙CEl O (⊙Cof (⊙idf _)) ⊙→ ⊙CEl O ⊙LU)
  G = CF O (⊙cfcod (⊙idf _))

  Cof-Unit-is-Unit : ⊙Cof (⊙idf ⊙LU) == ⊙LU
  Cof-Unit-is-Unit = ⊙ua e idp
    where e = equiv (λ _ → lift unit)
                    (λ _ → cfbase (idf _))
                    (λ _ → idp)
                    (Cofiber-elim (idf _)
                       {P = λ c → cfbase (idf _) == c}
                       idp
                       (λ _ → cfglue (idf _) (lift unit))
                       (λ _ → ↓-cst=idf-in idp))

  cfcod-is-idf : Path {A = Σ (Ptd i) (λ X → fst (⊙LU ⊙→ X))}
                      (⊙Cof (⊙idf _) , ⊙cfcod (⊙idf _))
                      (⊙LU , ⊙idf _)
  cfcod-is-idf =
    pair= Cof-Unit-is-Unit
          (prop-has-all-paths-↓ (⊙→-level (Lift-level Unit-is-prop)))

  C₀-Unit-is-contr : is-contr (CEl O ⊙LU)
  C₀-Unit-is-contr =
    (Cid O ⊙LU , λ x → lemma₂ x ∙ app= (ap GroupHom.f (CF-ident O)) x)
    where
    lemma₁ : (x : CEl O (⊙Cof (⊙idf _))) → Cid O ⊙LU == fst G x
    lemma₁ x = ! (itok (C-exact O (⊙idf _)) (fst G x) [ x , idp ])
               ∙ app= (ap GroupHom.f (CF-ident O)) (fst G x)

    lemma₂ : (x : CEl O ⊙LU) → Cid O ⊙LU == fst (CF O (⊙idf _)) x
    lemma₂ = transport
      {A = Σ (Ptd i) (λ X → fst (⊙LU ⊙→ X))}
      (λ {(X , H) → (c : CEl O X) → Cid O ⊙LU == fst (CF O H) c})
      cfcod-is-idf
      lemma₁

  Unit-is-Susp-Unit : ⊙LU == ⊙Susp ⊙LU
  Unit-is-Susp-Unit = ⊙ua
    (equiv (λ _ → north _)
           (λ _ → lift unit)
           (Suspension-elim _
             {P = λ s → north _ == s}
             idp
             (merid _ (lift unit))
             (λ _ → ↓-cst=idf-in idp))
           (λ _ → idp))
    idp

C-Unit-is-trivial : (n : ℤ) → C n ⊙LU == LiftUnit-Group
C-Unit-is-trivial O =
  contr-is-0ᴳ _ C₀-Unit-is-contr
C-Unit-is-trivial (pos O) =
  ap (C (pos O)) Unit-is-Susp-Unit ∙ C-Susp O ⊙LU
  ∙ (contr-is-0ᴳ _ C₀-Unit-is-contr)
C-Unit-is-trivial (pos (S m)) =
  ap (C (pos (S m))) Unit-is-Susp-Unit ∙ C-Susp (pos m) ⊙LU
  ∙ C-Unit-is-trivial (pos m)
C-Unit-is-trivial (neg O) =
  ! (C-Susp (neg O) ⊙LU) ∙ ! (ap (C O) Unit-is-Susp-Unit)
  ∙ (contr-is-0ᴳ _ C₀-Unit-is-contr)
C-Unit-is-trivial (neg (S m)) =
  ! (C-Susp (neg (S m)) ⊙LU) ∙ ! (ap (C (neg m)) Unit-is-Susp-Unit)
  ∙ C-Unit-is-trivial (neg m)

C-Unit-is-contr : (n : ℤ) → is-contr (CEl n ⊙LU)
C-Unit-is-contr n =
  transport (is-contr ∘ Group.El) (! (C-Unit-is-trivial n))
            (Lift-level Unit-is-contr)

C-Unit-is-prop : (n : ℤ) → is-prop (CEl n ⊙LU)
C-Unit-is-prop n =
  transport (is-prop ∘ Group.El) (! (C-Unit-is-trivial n))
            (Lift-level Unit-is-prop)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda