text:
module CompleteSemantics.Iemhoff where

open import Syntax public

-- Introspective brilliant Kripke models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    World   : Set
    _≤_     : World → World → Set
    refl≤   : ∀ {w} → w ≤ w
    trans≤  : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″
    _R_     : World → World → Set
    reflR   : ∀ {w} → w R w
    transR  : ∀ {w w′ w″} → w R w′ → w′ R w″ → w R w″
    _⊩ᵅ_   : World → Atom → Set
    mono⊩ᵅ : ∀ {w w′ P} → w ≤ w′ → w ⊩ᵅ P → w′ ⊩ᵅ P

  -- Introspection.
  field
    peek : World → Context

  _R⨾≤_ : World → World → Set
  _R⨾≤_ = _R_ ⨾ _≤_

  -- Brilliance.
  field
    R⨾≤→R : ∀ {w v′} → w R⨾≤ v′ → w R v′

  -- Vindication, as a consequence of brilliance.
  ≤→R : ∀ {w v′} → w ≤ v′ → w R v′
  ≤→R {w} ψ = R⨾≤→R (w , (reflR , ψ))

open Model {{…}} public

-- Forcing in a particular world of a particular model.

module _ {{_ : Model}} where
  mutual
    infix 3 _⊪_
    _⊪_ : World → Type → Set
    w ⊪ α P    = w ⊩ᵅ P
    w ⊪ A ⇒ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
    w ⊪ □ A    = ∀ {v′} → w R v′ → ∅ ⁏ π₂ (peek v′) ⊢ A ∧ v′ ⊩ A
    w ⊪ A ⩕ B  = w ⊩ A ∧ w ⊩ B
    w ⊪ ⫪     = ⊤
    w ⊪ ⫫     = ⊥
    w ⊪ A ⩖ B  = w ⊩ A ∨ w ⊩ B

    infix 3 _⊩_
    _⊩_ : World → Type → Set
    w ⊩ A = ∀ {C w′} → w ≤ w′ →
             (∀ {w″} → w′ ≤ w″ → w″ ⊪ A → peek w″ ⊢ⁿᶠ C) →
             peek w′ ⊢ⁿᶠ C

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Stack Type → Set
  w ⊩⋆ ∅     = ⊤
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ ∧ w ⊩ A

-- Monotonicity of forcing with respect to constructive accessibility.

module _ {{_ : Model}} where
  mutual
    mono⊪ : ∀ {A w w′} → w ≤ w′ → w ⊪ A → w′ ⊪ A
    mono⊪ {α P}    ψ s       = mono⊩ᵅ ψ s
    mono⊪ {A ⇒ B} ψ f       = λ ψ′ a → f (trans≤ ψ ψ′) a
    mono⊪ {□ A}    ψ f       = λ ρ → f (transR (≤→R ψ) ρ)
    mono⊪ {A ⩕ B}  ψ (a , b) = mono⊩ {A} ψ a , mono⊩ {B} ψ b
    mono⊪ {⫪}     ψ ∙       = ∙
    mono⊪ {⫫}     ψ ()
    mono⊪ {A ⩖ B}  ψ (ι₁ a)  = ι₁ (mono⊩ {A} ψ a)
    mono⊪ {A ⩖ B}  ψ (ι₂ b)  = ι₂ (mono⊩ {B} ψ b)

    mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
    mono⊩ ψ a = λ ψ′ κ → a (trans≤ ψ ψ′) κ

  mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     ψ ∙       = ∙
  mono⊩⋆ {Ξ , A} ψ (ξ , s) = mono⊩⋆ {Ξ} ψ ξ , mono⊩ {A} ψ s

-- Continuation-passing equipment.

module _ {{_ : Model}} where
  return : ∀ {A w} → w ⊪ A → w ⊩ A
  return {A} a = λ ψ κ → κ refl≤ (mono⊪ {A} ψ a)

  bind : ∀ {A B w} → w ⊩ A →
         (∀ {w′} → w ≤ w′ → w′ ⊪ A → w′ ⊩ B) →
         w ⊩ B
  bind a κ = λ ψ κ′ → a ψ
               λ ψ′ a′ → κ (trans≤ ψ ψ′) a′ refl≤
                 λ ψ″ a″ → κ′ (trans≤ ψ′ ψ″) a″

-- Additional equipment.

module _ {{_ : Model}} where
  lookup : ∀ {Ξ A w} → A ∈ Ξ → w ⊩⋆ Ξ → w ⊩ A
  lookup top     (ξ , s) = s
  lookup (pop i) (ξ , s) = lookup i ξ

-- Forcing in all worlds of all models, or semantic entailment.

infix 3 _⊨_
_⊨_ : Context → Type → Set₁
Γ ⁏ Δ ⊨ A = ∀ {{_ : Model}} {w} →
             w ⊩⋆ Γ →
             (∀ {v′} → w R v′ → ∅ ⁏ π₂ (peek v′) ⊢⋆ Δ) →
             (∀ {v′} → w R v′ → v′ ⊩⋆ Δ) →
             w ⊩ A

-- Soundness of the semantics with respect to the syntax.

reflect : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊨ A
reflect (var i)                  γ τ δ = lookup i γ
reflect (mvar i)                 γ τ δ = lookup i (δ reflR)
reflect (lam {A} {B} d)          γ τ δ = return {A ⇒ B}
                                           λ ψ a → reflect d (mono⊩⋆ ψ γ , a)
                                                              (λ ρ → τ (transR (≤→R ψ) ρ))
                                                              (λ ρ → δ (transR (≤→R ψ) ρ))
reflect (app {A} {B} d e)        γ τ δ = bind {A ⇒ B} {B} (reflect d γ τ δ)
                                           λ ψ f → f refl≤ (mono⊩ {A} ψ (reflect e γ τ δ))
reflect (box {A} d)              γ τ δ = return {□ A}
                                           λ ρ → graft⊢ ∙ (τ ρ) d ,
                                                  reflect d ∙
                                                            (λ ρ′ → τ (transR ρ ρ′))
                                                            (λ ρ′ → δ (transR ρ ρ′))
reflect (unbox {A} {C} d e)      γ τ δ = bind {□ A} {C} (reflect d γ τ δ)
                                           λ ψ s → reflect e (mono⊩⋆ ψ γ)
                                                              (λ ρ → τ (transR (≤→R ψ) ρ) , π₁ (s ρ))
                                                              (λ ρ → δ (transR (≤→R ψ) ρ) , π₂ (s ρ))
reflect (pair {A} {B} d e)       γ τ δ = return {A ⩕ B} (reflect d γ τ δ , reflect e γ τ δ)
reflect (fst {A} {B} d)          γ τ δ = bind {A ⩕ B} {A} (reflect d γ τ δ)
                                           λ { ψ (a , b) → a }
reflect (snd {A} {B} d)          γ τ δ = bind {A ⩕ B} {B} (reflect d γ τ δ)
                                           λ { ψ (a , b) → b }
reflect unit                     γ τ δ = return {⫪} ∙
reflect (boom {C} d)             γ τ δ = bind {⫫} {C} (reflect d γ τ δ)
                                           λ ψ → elim⊥
reflect (left {A} {B} d)         γ τ δ = return {A ⩖ B} (ι₁ (reflect d γ τ δ))
reflect (right {A} {B} d)        γ τ δ = return {A ⩖ B} (ι₂ (reflect d γ τ δ))
reflect (case {A} {B} {C} d e f) γ τ δ = bind {A ⩖ B} {C} (reflect d γ τ δ)
                                           λ { ψ (ι₁ a) → reflect e (mono⊩⋆ ψ γ , a)
                                                                     (λ ρ → τ (transR (≤→R ψ) ρ))
                                                                     (λ ρ → δ (transR (≤→R ψ) ρ))
                                             ; ψ (ι₂ b) → reflect f (mono⊩⋆ ψ γ , b)
                                                                     (λ ρ → τ (transR (≤→R ψ) ρ))
                                                                     (λ ρ → δ (transR (≤→R ψ) ρ))
                                             }

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { World   = Context
      ; _≤_     = _⊆²_
      ; refl≤   = refl⊆²
      ; trans≤  = trans⊆²
      ; _R_     = λ { (_ ⁏ Δ) (_ ⁏ Δ′) → Δ ⊆ Δ′ }
      ; reflR   = refl⊆
      ; transR  = trans⊆
      ; _⊩ᵅ_   = λ { (Γ ⁏ Δ) P → Γ ⁏ Δ ⊢ⁿᵉ α P }
      ; mono⊩ᵅ = mono⊢ⁿᵉ
      ; peek    = id
      ; R⨾≤→R  = λ { (_ , (ρ , (_ , ρ′))) → trans⊆ ρ ρ′ }
      }

-- Soundness and completeness of the canonical model with respect to the syntax.

mutual
  reflectᶜ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊩ A
  reflectᶜ {α P}    d = return {α P} d
  reflectᶜ {A ⇒ B} d = return {A ⇒ B}
                          λ ψ a → reflectᶜ (appⁿᵉ (mono⊢ⁿᵉ ψ d) (reifyᶜ a))
  reflectᶜ {□ A}    d = λ ψ κ → neⁿᶠ (unboxⁿᵉ (mono⊢ⁿᵉ ψ d)
                                               (κ (refl⊆ , weak⊆)
                                                  λ ρ′ → mono⊢ (bot , ρ′) mv₀ ,
                                                          reflectᶜ (mono⊢ⁿᵉ (bot , ρ′) mv₀ⁿᵉ)))
  reflectᶜ {A ⩕ B}  d = return {A ⩕ B} (reflectᶜ (fstⁿᵉ d) , reflectᶜ (sndⁿᵉ d))
  reflectᶜ {⫪}     d = return {⫪} ∙
  reflectᶜ {⫫}     d = λ ψ κ → neⁿᶠ (boomⁿᵉ (mono⊢ⁿᵉ ψ d))
  reflectᶜ {A ⩖ B}  d = λ ψ κ → neⁿᶠ (caseⁿᵉ (mono⊢ⁿᵉ ψ d)
                                              (κ (weak⊆ , refl⊆) (ι₁ (reflectᶜ v₀ⁿᵉ)))
                                              (κ (weak⊆ , refl⊆) (ι₂ (reflectᶜ v₀ⁿᵉ))))

  reifyᶜ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊩ A → Γ ⁏ Δ ⊢ⁿᶠ A
  reifyᶜ {α P}    κ = κ refl⊆²
                        λ ψ s → neⁿᶠ s
  reifyᶜ {A ⇒ B} κ = κ refl⊆²
                        λ ψ f → lamⁿᶠ (reifyᶜ (f (weak⊆ , refl⊆) (reflectᶜ v₀ⁿᵉ)))
  reifyᶜ {□ A}    κ = κ refl⊆²
                        λ ψ f → boxⁿᶠ (π₁ (f {∅ ⁏ _} refl⊆))
  reifyᶜ {A ⩕ B}  κ = κ refl⊆²
                        λ { ψ (a , b) → pairⁿᶠ (reifyᶜ a) (reifyᶜ b) }
  reifyᶜ {⫪}     κ = κ refl⊆²
                        λ { ψ ∙ → unitⁿᶠ }
  reifyᶜ {⫫}     κ = κ refl⊆²
                        λ ψ ()
  reifyᶜ {A ⩖ B}  κ = κ refl⊆²
                        λ { ψ (ι₁ a) → leftⁿᶠ (reifyᶜ a)
                          ; ψ (ι₂ b) → rightⁿᶠ (reifyᶜ b)
                          }

-- Reflexivity of simultaneous forcing.

refl⊩⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊩⋆ Γ
refl⊩⋆ {∅}     = ∙
refl⊩⋆ {Γ , A} = mono⊩⋆ (weak⊆ , refl⊆) refl⊩⋆ , reflectᶜ v₀ⁿᵉ

mrefl⊩⋆ : ∀ {Δ Γ} → Γ ⁏ Δ ⊩⋆ Δ
mrefl⊩⋆ {∅}     = ∙
mrefl⊩⋆ {Δ , A} = mono⊩⋆ (refl⊆ , weak⊆) mrefl⊩⋆ , reflectᶜ mv₀ⁿᵉ

-- Completeness of the semantics with respect to the syntax.

reify : ∀ {Γ Δ A} → Γ ⁏ Δ ⊨ A → Γ ⁏ Δ ⊢ⁿᶠ A
reify s = reifyᶜ (s refl⊩⋆ (λ ρ → mono⊢⋆ (refl⊆ , ρ) mrefl⊢⋆)
                            (λ ρ → mono⊩⋆ (refl⊆ , ρ) mrefl⊩⋆))

-- Normalisation by evaluation.

nbe : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ A
nbe = reify ∘ reflect


text:
module sum-thms where

open import eq
open import sum
open import list
open import product

inj₁-inj : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{x : A}{x'} → inj₁{ℓ}{ℓ'}{A}{B} x ≡ inj₁ x' → x ≡ x'
inj₁-inj refl = refl

ext: agda

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


text:
module MultiSorted.Context {s} (Sort : Set s)  where

-- An attempt to define more structured context
-- that directly support the cartesian structure

data Context : Set s where
  ctx-empty : Context
  ctx-slot : Sort → Context
  ctx-concat : Context → Context → Context

-- the variables in a context
data var : Context → Set where
  var-var  : ∀ {A} → var (ctx-slot A)
  var-inl  : ∀ {Γ Δ} → var Γ → var (ctx-concat Γ Δ)
  var-inr  : ∀ {Γ Δ} → var Δ → var (ctx-concat Γ Δ)

sort-of : ∀ (Γ : Context) → var Γ → Sort
sort-of (ctx-slot A) _ = A
sort-of (ctx-concat Γ Δ) (var-inl x) = sort-of Γ x
sort-of (ctx-concat Γ Δ) (var-inr x) = sort-of Δ x

-- It is absurd to have a variable in the empty context
ctx-empty-absurd : ∀ {ℓ} {P : var ctx-empty → Set ℓ} (x : var ctx-empty) → P x
ctx-empty-absurd ()

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

open import Agda.Primitive

record LiftP {ℓ ℓ'}(A : Prop ℓ) : Prop (ℓ ⊔ ℓ') where
  constructor liftP
  field
    unliftP : A
open LiftP public

unliftP' : {ℓ ℓ' ℓ'' : Level} {A : Prop ℓ}{B : Set ℓ''}(f : A → B) → LiftP {ℓ}{ℓ'} A → B
unliftP' f (liftP x) = f x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts #-}
module Cubical.Codata.Everything where

open import Cubical.Codata.EverythingSafe public

--- Modules making assumptions that might be incompatible with other
--  flags or make use of potentially unsafe features.

-- Assumes --guardedness
open import Cubical.Codata.Stream public

open import Cubical.Codata.Conat public

open import Cubical.Codata.M public

-- Also uses {-# TERMINATING #-}.
open import Cubical.Codata.M.Bisimilarity public

{-
-- Alternative M type implemetation, based on
-- https://arxiv.org/pdf/1504.02949.pdf
-- "Non-wellfounded trees in Homotopy Type Theory"
-- Benedikt Ahrens, Paolo Capriotti, Régis Spadotti
-}

open import Cubical.Codata.M.AsLimit.M
open import Cubical.Codata.M.AsLimit.Coalg
open import Cubical.Codata.M.AsLimit.helper
open import Cubical.Codata.M.AsLimit.Container
open import Cubical.Codata.M.AsLimit.itree
open import Cubical.Codata.M.AsLimit.stream

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: module Automaton.Pushdown where

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 Naturals where

open import Library
open import Categories
open import Functors

open Fun

record NatT {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(F G : Fun C D) :
  Set (a ⊔ b ⊔ c ⊔ d) where
  constructor natural
  open Cat
  field cmp : ∀ {X} → Hom D (OMap F X) (OMap G X)
        nat : ∀{X Y}{f : Hom C X Y} →
              comp D (HMap G f) cmp ≅ comp D cmp (HMap F f)

NatTEq : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{F G : Fun C D}
         {α β : NatT F G} →
         (λ {X} → NatT.cmp α {X}) ≅ (λ {X} → NatT.cmp β {X}) →
         α ≅ β
NatTEq {α = natural cmp _} {natural .cmp _} refl =
  cong (natural cmp) (iext λ _ → iext λ _ → iext λ _ → ir _ _)

idNat : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{F : Fun C D} → NatT F F
idNat {D = D}{F} = let open Cat D in record {
  cmp = iden;
  nat = λ{X}{Y}{f} →
    proof
    comp (HMap F f) iden
    ≅⟨ idr ⟩
    HMap F f
    ≅⟨ sym idl ⟩
    comp iden (HMap F f) ∎}

compNat : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{F G H : Fun C D} →
          NatT G H → NatT F G → NatT F H
compNat {D = D}{F}{G}{H} α β = let open Cat D; open NatT in record {
  cmp = comp (cmp α) (cmp β);
  nat = λ{X}{Y}{f} →
    proof
    comp (HMap H f) (comp (cmp α) (cmp β))
    ≅⟨ sym ass ⟩
    comp (comp (HMap H f) (cmp α)) (cmp β)
    ≅⟨ cong (λ f₁ → comp f₁ (cmp β)) (nat α) ⟩
    comp (comp (cmp α) (HMap G f)) (cmp β)
    ≅⟨ ass ⟩
    comp (cmp α) (comp (HMap G f) (cmp β))
    ≅⟨ cong (comp (cmp α)) (nat β) ⟩
    comp (cmp α) (comp (cmp β) (HMap F f))
    ≅⟨ sym ass ⟩
    comp (comp (cmp α) (cmp β)) (HMap F f)
    ∎}

idlNat : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{F G : Fun C D}
         {α : NatT F G} → compNat idNat α ≅ α
idlNat {D = D} = NatTEq (iext λ _ → Cat.idl D)

idrNat : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{F G : Fun C D}
         {α : NatT F G} → compNat α idNat ≅ α
idrNat {D = D} = NatTEq (iext λ _ → Cat.idr D)

assNat : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{E F G H : Fun C D}
         {α : NatT G H}{β : NatT F G}{η : NatT E F} →
         compNat (compNat α β) η ≅ compNat α (compNat β η)
assNat {D = D} = NatTEq (iext λ _ → Cat.ass D)

-- Natural isomorphism

record Iso {l m}(C : Cat {l}{m}){A B}(f : Cat.Hom C A B) : Set (l ⊔ m)
  where
  constructor iso
  open Cat C
  field inv  : Hom B A
        rinv : comp f inv ≅ iden {B}
        linv : comp inv f ≅ iden {A}

record NatI {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(F G : Fun C D) :
  Set (a ⊔ b ⊔ c ⊔ d) where
  constructor natural
  open Cat
  field cmp : ∀ {X} → Hom D (OMap F X) (OMap G X)
        cmpI : ∀{X} -> Iso D (cmp {X})
        nat : ∀{X Y}{f : Hom C X Y} →
              comp D (HMap G f) cmp ≅ comp D cmp (HMap F f)

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module PushProdPull where

open import Categories.Category
open import Categories.Category.Cartesian.Bundle
open import Categories.Category.CartesianClosed.Canonical
open import Categories.Category.Core
open import Categories.Category.Product
open import Categories.Diagram.Pullback
open import Categories.Diagram.Pushout
open import Categories.Functor
open import Categories.Functor.Bifunctor
open import Data.Product
open import Function using (const)
open import Level
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

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

data t : Set where
 ⊤ : t

!-unique-lemma : ∀ (x : t) → ⊤ ≡ x
!-unique-lemma ⊤ = refl

arrow : Category (suc zero) zero zero
arrow = record
  { Obj = Σ (Set × Set) (λ x → proj₁ x → proj₂ x)
  ; _⇒_ = arr
  ; _≈_ = _≡_
  ; id = (λ z → z) , λ z → z
  ; _∘_ = λ {A} {B} {C} f g → comp {A} {B} {C} f g
  ; assoc = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = λ {refl refl → refl}
  }
  where
  arr : Rel (Σ (Set × Set) (λ x → proj₁ x → proj₂ x)) zero
  arr ((a , b) , x1) ((c , d) , y1) = (a → c) × (b → d)
  comp : {A B C : Σ (Set × Set) (λ x → proj₁ x → proj₂ x)} → arr B C → arr A B → arr A C
  comp {A} {B} {C} (f0 , f1) (g0 , g1) = (λ x → f0 (g0 x)) , λ x → f1 (g1 x)

open Category arrow

SetC : Category (suc zero) zero zero
SetC =
 record
  { Obj = Set
  ; _⇒_ = λ x y → x → y
  ; _≈_ = _≡_
  ; id = λ x → x
  ; _∘_ = λ f g a → f (g a)
  ; assoc = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = λ {refl refl → refl}
  }

pushout-prod : (f g : Obj) → Obj
pushout-prod ((A0 , A1) , f) ((B0 , B1) , g) = {!   !}
-- Pushout SetC f×1 1×g
--  where
--  f×1 : A0 × B0 → A1 × B0
--  f×1 (a , b) = f a , b
--  1×g : A0 × B0 → A0 × B1
--  1×g (a , b) = a , g b

pullback-hom : (f g : Obj) → Obj
pullback-hom ((A0 , A1) , f) ((B0 , B1) , g) = {!   !}
-- Pullback SetC [f,1] [1,g]
--  where
--  [f,1] : (A1 → B1) → A0 → B1
--  [f,1] u = λ x → u (f x)
--  [1,g] : (A0 → B0) → A0 → B1
--  [1,g] u = λ x → g (u x)

pp-is-functor : Endobifunctor arrow
pp-is-functor =
 record
  { F₀ = F0
  ; F₁ = {!   !}
  ; identity = {!   !}
  ; homomorphism = {!   !}
  ; F-resp-≈ = {!   !}
  }
  where
  F0 : Category.Obj (Categories.Category.Product.Product arrow arrow) → Obj
  F0 x = pullback-hom (proj₁ x) (proj₂ x)
  F1 : {A B : Obj × Obj} → Product arrow arrow Categories.Category.[ A , B ] → arrow Categories.Category.[ F0 A , F0 B ]
  F1 {((A0 , A1) , a) , ((B0 , B1) , b)} {((C0 , C1) , c) , ((D0 , D1) , d)} ((u , v) , s , t) = {!   !}

max_stars_repo_name: tetrapharmakon/agda-categories

max_issues_repo_name: tetrapharmakon/agda-categories

max_forks_repo_name: tetrapharmakon/agda-categories


text:
module Esterel.Lang.Properties where

open import Esterel.Lang
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Nullary using (¬_ ; Dec ; yes ; no)
open import Esterel.Environment
open import Esterel.Variable.Signal as Signal
open import Esterel.Variable.Shared as SharedVar
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Context.Properties

open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.Nat
  using (ℕ ; zero ; suc) renaming (_⊔_ to _⊔ℕ_)
open import Data.MoreNatProp
  using (⊔-sym)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Data.List
open import Data.Maybe
open import Data.List.Any
open import Data.List.All
open import Data.OrderedListMap
open import Function using (_$_)

import Data.OrderedListMap(Signal)(Signal.unwrap)(Signal.Status) as SigOMap
import Data.OrderedListMap(SharedVar)(SharedVar.unwrap)(SharedVar.Status × ℕ) as ShrOMap

open ≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)

open EvaluationContext1
open _≐_⟦_⟧e
open Context1
open _≐_⟦_⟧c

data halted : Term → Set where
  hnothin :           halted nothin
  hexit   : (n : ℕ) → halted (exit n)

data paused : Term → Set where
  ppause   :                     paused pause
  pseq     : ∀{p q} → paused p → paused (p >> q)
  ploopˢ   : ∀{p q} → paused p → paused (loopˢ p q)
  ppar     : ∀{p q} → paused p → paused q → paused (p ∥ q)
  psuspend : ∀{p S} → paused p → paused (suspend p S)
  ptrap    : ∀{p}   → paused p → paused (trap p)

data done : Term → Set where
  dhalted : ∀{p} → (p/halted : halted p) → done p
  dpaused : ∀{p} → (p/paused : paused p) → done p

data complete-θ : Env → Set where
  θcomplete : ∀{θ} →
                (∀ S → (S∈ : isSig∈ S θ) → ((sig-stats{S} θ S∈ ≡ Signal.absent) ⊎ (sig-stats{S} θ S∈ ≡ Signal.present))) →
                (∀ s → (s∈ : isShr∈ s θ) → (shr-stats{s} θ s∈ ≡ SharedVar.ready)) →
                ---------------
                complete-θ θ

data complete : Term → Set where
  codone : ∀{p} → done p → complete p
  coenv : ∀{θ A p} → complete-θ θ → done p → complete (ρ⟨ θ , A ⟩· p)

-- Halted and paused programs are disjoint
halted-paused-disjoint : ∀{p} → halted p → paused p → ⊥
halted-paused-disjoint hnothin   ()
halted-paused-disjoint (hexit _) ()

↓_ : ∀ {p} → halted p → Term
↓ hnothin = nothin
↓ hexit zero = nothin
↓ hexit (suc n) = exit n

↓-well-behaved : ∀ p -> (haltedp : halted p) -> halted (↓ haltedp)
↓-well-behaved .nothin hnothin = hnothin
↓-well-behaved .(exit 0) (hexit zero) = hnothin
↓-well-behaved .(exit (suc n)) (hexit (suc n)) = hexit n

A-max : Ctrl → Ctrl → Ctrl
A-max GO   GO   = GO
A-max GO   WAIT = GO
A-max WAIT GO   = GO
A-max WAIT WAIT = WAIT

value-max : ∀{p q} → done p → done q → (halted p ⊎ halted q) →  Term
value-max {q = q} (dhalted hnothin)   done-q              h⊎h = q
value-max {p = p} done-p              (dhalted hnothin)   h⊎h = p
value-max         (dhalted (hexit n)) (dhalted (hexit m)) h⊎h = exit (n ⊔ℕ m)
value-max         (dhalted (hexit n)) (dpaused _)         h⊎h = exit n
value-max         (dpaused _)         (dhalted (hexit m)) h⊎h = exit m
value-max         (dpaused paused-p)  (dpaused paused-q)  (inj₁ halted-p) =
  ⊥-elim (halted-paused-disjoint halted-p paused-p)
value-max         (dpaused paused-p)  (dpaused paused-q)  (inj₂ halted-q) =
  ⊥-elim (halted-paused-disjoint halted-q paused-q)

value-max-unique : ∀{p q d1 d2 d3 d4 ij1 ij2} → value-max{p}{q} d1 d2 ij1 ≡ value-max{p}{q} d3 d4 ij2
value-max-unique {d1 = dhalted hnothin}   {d2}                {dhalted hnothin}    {d4}                 {ij1} {ij2} = refl
value-max-unique {d1 = dhalted (hexit n)} {dhalted hnothin}   {dhalted (hexit .n)} {dhalted hnothin}    {ij1} {ij2} = refl
value-max-unique {d1 = dpaused p/paused}  {dhalted hnothin}   {dpaused p/paused'}  {dhalted hnothin}    {ij1} {ij2} = refl
value-max-unique {d1 = dhalted (hexit n)} {dhalted (hexit m)} {dhalted (hexit .n)} {dhalted (hexit .m)} {ij1} {ij2} = refl
value-max-unique {d1 = dhalted (hexit n)} {dpaused q/paused}  {dhalted (hexit .n)} {dpaused q/paused'}  {ij1} {ij2} = refl
value-max-unique {d1 = dpaused p/paused}  {dhalted (hexit n)} {dpaused p/paused'}  {dhalted (hexit .n)} {ij1} {ij2} = refl
value-max-unique {d1 = dpaused p/paused}  {dpaused q/paused}  {dpaused p/paused'}  {dpaused q/paused'} {inj₁ p/halted} {ij2} =
  ⊥-elim (halted-paused-disjoint p/halted p/paused')
value-max-unique {d1 = dpaused p/paused} {dpaused q/paused}   {dpaused p/paused'}  {dpaused q/paused'} {inj₂ q/halted} {ij2} =
  ⊥-elim (halted-paused-disjoint q/halted q/paused')
value-max-unique {d1 = dhalted p/halted} {d2} {dpaused p/paused'} {d4} {ij1} {ij2} =
  ⊥-elim (halted-paused-disjoint p/halted p/paused')
value-max-unique {d1 = dpaused p/paused} {d2} {dhalted p/halted'} {d4} {ij1} {ij2} =
  ⊥-elim (halted-paused-disjoint p/halted' p/paused)
value-max-unique {d1 = d1} {dhalted q/halted} {d3} {dpaused q/paused} {ij1} {ij2} =
  ⊥-elim (halted-paused-disjoint q/halted q/paused)
value-max-unique {d1 = d1} {dpaused q/paused}  {d3} {dhalted q/halted} {ij1} {ij2} =
  ⊥-elim (halted-paused-disjoint q/halted q/paused)

value-max-sym : ∀ {p q} ->
  (donep : done p) ->
  (haltedq : halted q) ->
  value-max donep (dhalted haltedq) (inj₂ haltedq) ≡
  value-max (dhalted haltedq) donep (inj₁ haltedq)
value-max-sym (dhalted hnothin) hnothin = refl
value-max-sym (dhalted hnothin) (hexit n) = refl
value-max-sym (dhalted (hexit n)) hnothin = refl
value-max-sym (dhalted (hexit n)) (hexit m)
  rewrite ⊔-sym n m = refl
value-max-sym (dpaused p/paused) hnothin = refl
value-max-sym (dpaused p/paused) (hexit n) = refl

value-max-done : ∀ {p q} →
  (p/done : done p) →
  (q/done : done q) →
  (p/halted⊎q/halted : halted p ⊎ halted q) →
  done (value-max p/done q/done p/halted⊎q/halted)
value-max-done (dhalted hnothin)   q/done              ⟨p⊎q⟩/halted = q/done
value-max-done (dhalted (hexit n)) (dhalted hnothin)   ⟨p⊎q⟩/halted = dhalted (hexit n)
value-max-done (dhalted (hexit n)) (dhalted (hexit m)) ⟨p⊎q⟩/halted = dhalted (hexit (n ⊔ℕ m))
value-max-done (dhalted (hexit n)) (dpaused q/paused)  ⟨p⊎q⟩/halted = dhalted (hexit n)
value-max-done (dpaused p/paused)  (dhalted hnothin)   ⟨p⊎q⟩/halted = dpaused p/paused
value-max-done (dpaused p/paused)  (dhalted (hexit m)) ⟨p⊎q⟩/halted = dhalted (hexit m)
value-max-done (dpaused p/paused)  (dpaused q/paused)  (inj₁ p/halted) =
  ⊥-elim (halted-paused-disjoint p/halted p/paused)
value-max-done (dpaused p/paused)  (dpaused q/paused)  (inj₂ q/halted) =
  ⊥-elim (halted-paused-disjoint q/halted q/paused)

{-
Properties relating halted, paused, done programs and the contexts. There's no way to
decompose halted programs, so the result must remain halted. The decomposition of paused
programs under the evaluation context must result in paused programs.

    halted-⟦⟧c : ∀{p p' C} → halted p → p ≐ C ⟦ p' ⟧c → halted p'
    paused-⟦⟧e : ∀{p p' E} → paused p → p ≐ E ⟦ p' ⟧e → paused p'
-}
halted-⟦⟧c : ∀{p p' C} → halted p → p ≐ C ⟦ p' ⟧c → halted p'
halted-⟦⟧c hnothin dchole = hnothin
halted-⟦⟧c (hexit n) dchole = hexit n

-- In fact, the only valid case would be E ≡ [] and p ≡ p'
halted-⟦⟧e : ∀{p p' E} → halted p → p ≐ E ⟦ p' ⟧e → halted p'
halted-⟦⟧e p/halted p≐E⟦p'⟧ = halted-⟦⟧c p/halted (⟦⟧e-to-⟦⟧c p≐E⟦p'⟧)

paused-⟦⟧e : ∀{p p' E} → paused p → p ≐ E ⟦ p' ⟧e → paused p'
paused-⟦⟧e ppause dehole = ppause
paused-⟦⟧e (pseq paused) dehole = pseq paused
paused-⟦⟧e (pseq paused) (deseq d) = paused-⟦⟧e paused d
paused-⟦⟧e (ploopˢ paused) dehole = ploopˢ paused
paused-⟦⟧e (ploopˢ paused) (deloopˢ d) = paused-⟦⟧e paused d
paused-⟦⟧e (ppar paused₁ paused₂) dehole = ppar paused₁ paused₂
paused-⟦⟧e (ppar paused₁ paused₂) (depar₁ d) = paused-⟦⟧e paused₁ d
paused-⟦⟧e (ppar paused₁ paused₂) (depar₂ d) = paused-⟦⟧e paused₂ d
paused-⟦⟧e (psuspend paused) dehole = psuspend paused
paused-⟦⟧e (psuspend paused) (desuspend d) = paused-⟦⟧e paused d
paused-⟦⟧e (ptrap paused) dehole = ptrap paused
paused-⟦⟧e (ptrap paused) (detrap d) = paused-⟦⟧e paused d

done-⟦⟧e : ∀ {p p' E} → done p → p ≐ E ⟦ p' ⟧e → done p'
done-⟦⟧e (dhalted p/halted) p≐E⟦p'⟧ = dhalted (halted-⟦⟧e p/halted p≐E⟦p'⟧)
done-⟦⟧e (dpaused p/paused) p≐E⟦p'⟧ = dpaused (paused-⟦⟧e p/paused p≐E⟦p'⟧)

halted-dec : ∀ p -> Dec (halted p)
halted-dec nothin = yes hnothin
halted-dec pause = no (λ ())
halted-dec (signl S p) = no (λ ())
halted-dec (present S ∣⇒ p ∣⇒ p₁) = no (λ ())
halted-dec (emit S) = no (λ ())
halted-dec (p ∥ q) = no (λ ())
halted-dec (loop p) = no (λ ())
halted-dec (loopˢ p q) = no (λ ())
halted-dec (p >> q) = no (λ ())
halted-dec (suspend p S) = no (λ ())
halted-dec (trap p) = no (λ ())
halted-dec (exit x) = yes (hexit x)
halted-dec (shared s ≔ e in: p) = no (λ ())
halted-dec (s ⇐ e) = no (λ ())
halted-dec (var x ≔ e in: p) = no (λ ())
halted-dec (x ≔ e) = no (λ ())
halted-dec (if x ∣⇒ p ∣⇒ q) = no (λ ())
halted-dec (ρ⟨ θ , A ⟩· p) = no (λ ())

paused-dec : ∀ p -> Dec (paused p)
paused-dec nothin = no (λ ())
paused-dec pause = yes ppause
paused-dec (signl S p) = no (λ ())
paused-dec (present S ∣⇒ p ∣⇒ p₁) = no (λ ())
paused-dec (emit S) = no (λ ())
paused-dec (p ∥ q) with paused-dec p | paused-dec q
paused-dec (p ∥ q) | yes pausedp | yes pausedq = yes (ppar pausedp pausedq)
paused-dec (p ∥ q) | _ | no ¬pausedq = no (λ { (ppar _ pausedq) → ¬pausedq pausedq } )
paused-dec (p ∥ q) | no ¬pausedp | _ = no (λ { (ppar pausedp _) → ¬pausedp pausedp } )
paused-dec (loop p) = no (λ ())
paused-dec (loopˢ p q) with paused-dec p
paused-dec (loopˢ p q) | yes pausedp = yes (ploopˢ pausedp)
paused-dec (loopˢ p q) | no ¬pausedp = no (λ { (ploopˢ pausedp) → ¬pausedp pausedp })
paused-dec (p >> q) with paused-dec p
paused-dec (p >> q) | yes pausedp = yes (pseq pausedp)
paused-dec (p >> q) | no ¬pausedp = no (λ { (pseq pausedp) → ¬pausedp pausedp })
paused-dec (suspend p S) with paused-dec p
paused-dec (suspend p S) | yes pausedp = yes (psuspend pausedp)
paused-dec (suspend p S) | no ¬pausedp = no (λ { (psuspend pausedp) → ¬pausedp pausedp })
paused-dec (trap p) with paused-dec p
paused-dec (trap p) | yes pasuedp = yes (ptrap pasuedp)
paused-dec (trap p) | no ¬pausedp = no (λ { (ptrap pausedp) → ¬pausedp pausedp })
paused-dec (exit x) = no (λ ())
paused-dec (shared s ≔ e in: p) = no (λ ())
paused-dec (s ⇐ e) = no (λ ())
paused-dec (var x ≔ e in: p) = no (λ ())
paused-dec (x ≔ e) = no (λ ())
paused-dec (if x ∣⇒ p ∣⇒ q) = no (λ ())
paused-dec (ρ⟨ θ , A ⟩· p) = no (λ ())

done-dec : ∀ p → Dec (done p)
done-dec p with halted-dec p
done-dec p | yes halted-p = yes (dhalted halted-p)
done-dec p | no ¬halted-p with paused-dec p
done-dec p | no _ | yes paused-p = yes (dpaused paused-p)
done-dec p | no ¬halted-p | (no ¬paused-p) = no
  (λ { (dhalted p/halted) → ¬halted-p p/halted ;
       (dpaused p/paused) → ¬paused-p p/paused})

signal-absent-or-present : Signal.Status → Set
signal-absent-or-present S = S ≡ Signal.absent ⊎ S ≡ Signal.present

signal-absent-or-present-dec : Decidable signal-absent-or-present
signal-absent-or-present-dec present = yes (inj₂ refl)
signal-absent-or-present-dec absent = yes (inj₁ refl)
signal-absent-or-present-dec unknown = no (λ { (inj₁ ()) ; (inj₂ ())})

signals-all-absent-or-present-dec :
  (Ss :  SigMap.Map Signal.Status) ->
        Dec (∀ S → (S∈ : (SigMap.∈Dom S Ss)) →
              (signal-absent-or-present (SigMap.lookup{k = S} Ss S∈)))
signals-all-absent-or-present-dec m
   with SigOMap.andmap{_}{signal-absent-or-present} signal-absent-or-present-dec m
signals-all-absent-or-present-dec m | yes p = yes (λ S → p (Signal.unwrap S))
signals-all-absent-or-present-dec m | no ¬p = no (λ z → ¬p (λ n → z (n ₛ)))

var-is-ready : SharedVar.Status × ℕ → Set
var-is-ready p = (proj₁ p) ≡ SharedVar.ready

var-is-ready-dec : Decidable var-is-ready
var-is-ready-dec (ready , _) = yes refl
var-is-ready-dec (new , _) = no (λ ())
var-is-ready-dec (old , _) = no (λ ())

vars-all-ready-dec :
  (ss : ShrMap.Map (SharedVar.Status × ℕ)) ->
   Dec (∀ s → (s∈ : ShrMap.∈Dom s ss) →
        var-is-ready (ShrMap.lookup{k = s} ss s∈))
vars-all-ready-dec ss with ShrOMap.andmap{_}{var-is-ready} var-is-ready-dec ss
vars-all-ready-dec ss | yes p = yes (λ s → p (SharedVar.unwrap s))
vars-all-ready-dec ss | no ¬p = no (λ z → ¬p (λ n → z (n ₛₕ)))

complete-θ-dec : ∀ θ → Dec (complete-θ θ)
complete-θ-dec (Θ sigs shr _) with signals-all-absent-or-present-dec sigs
complete-θ-dec (Θ sigs shrs _) | yes p with vars-all-ready-dec shrs
complete-θ-dec (Θ sigs shrs _) | yes p₁ | yes p₂ = yes (θcomplete p₁ p₂)
complete-θ-dec (Θ sigs shrs _) | yes _ | no ¬p = no (λ { (θcomplete _ x) → ¬p x } )
complete-θ-dec (Θ sigs shrs _) | no ¬p = no (λ { (θcomplete x _) → ¬p x } )

complete-dec : ∀ p → Dec (complete p)
complete-dec p with done-dec p
complete-dec p | yes donep = yes (codone donep)
complete-dec nothin | no ¬donep = no (λ _ → ¬donep (dhalted hnothin))
complete-dec pause | no ¬donep = no (λ _ → ¬donep (dpaused ppause))
complete-dec (signl S p) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (present S ∣⇒ p ∣⇒ p₁) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (emit S) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (p ∥ p₁) | no ¬donep =  no (λ { (codone x) → ¬donep x } )
complete-dec (loop p) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (loopˢ p q) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (p >> p₁) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (suspend p S) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (trap p) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (exit x) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (shared s ≔ e in: p) | no ¬donep = no (λ { (codone x) → ¬donep x } )
complete-dec (s ⇐ e) | no ¬donep =  no (λ { (codone x) → ¬donep x } )
complete-dec (var x ≔ e in: p) | no ¬donep =  no (λ { (codone x) → ¬donep x } )
complete-dec (x ≔ e) | no ¬donep =  no (λ { (codone x) → ¬donep x } )
complete-dec (if x ∣⇒ p ∣⇒ p₁) | no ¬donep =  no (λ { (codone x) → ¬donep x } )
complete-dec (ρ⟨ θ , A ⟩· p) | _ with done-dec p
complete-dec (ρ⟨ θ , A ⟩· p) | _ | yes donep with complete-θ-dec θ
complete-dec (ρ⟨ θ , A ⟩· p) | _ | yes donep | (yes complete-θ) = yes (coenv complete-θ donep)
complete-dec (ρ⟨ θ , A ⟩· p) | _ | yes donep | (no ¬complete-θ) = no
   (λ { (codone (dhalted ())) ;
        (codone (dpaused ())) ;
        (coenv complete-θ _) → ¬complete-θ complete-θ })
complete-dec (ρ⟨ θ , A ⟩· p) | _ | no ¬donep = no
  (λ { (codone (dhalted ())) ;
       (codone (dpaused ())) ;
       (coenv _ donep) → ¬donep donep })

A-max-GO-≡-left : ∀ A → A-max GO A ≡ GO
A-max-GO-≡-left GO =  refl
A-max-GO-≡-left WAIT = refl

A-max-GO-≡-right : ∀ A → A-max A GO ≡ GO
A-max-GO-≡-right GO = refl
A-max-GO-≡-right WAIT = refl

A-max-comm : ∀ A1 A2 → A-max A1 A2 ≡ A-max A2 A1
A-max-comm GO GO = refl
A-max-comm GO WAIT = refl
A-max-comm WAIT GO = refl
A-max-comm WAIT WAIT = refl

A-max-assoc : ∀ A1 A2 A3 → (A-max A1 $ A-max A2 A3) ≡ A-max (A-max A1 A2) A3
A-max-assoc GO GO GO = refl
A-max-assoc GO GO WAIT = refl
A-max-assoc GO WAIT GO = refl
A-max-assoc GO WAIT WAIT = refl
A-max-assoc WAIT GO GO = refl
A-max-assoc WAIT GO WAIT = refl
A-max-assoc WAIT WAIT GO = refl
A-max-assoc WAIT WAIT WAIT = refl

A-max-swap : ∀ A1 A2 A3
             → (A-max (A-max A1 A2) A3) ≡ (A-max (A-max A1 A3) A2)
A-max-swap A1 A2 A3 = begin
                        (A-max (A-max A1 A2) A3) ≡⟨ sym (A-max-assoc A1 A2 A3) ⟩
                        (A-max A1 $ A-max A2 A3) ≡⟨ sym (cong (A-max A1) (A-max-comm A3 A2)) ⟩
                        (A-max A1 $ A-max A3 A2) ≡⟨ A-max-assoc A1 A3 A2 ⟩
                        (A-max (A-max A1 A3) A2) ∎

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- Safe modules that use --erased-cubical and --guardedness
------------------------------------------------------------------------

{-# OPTIONS --safe --erased-cubical --guardedness #-}

module README.Safe.Cubical.Erased.Guardedness where

-- M-types for indexed containers, defined coinductively (in Cubical
-- Agda).

import Container.Indexed.Variant.M.Codata
import Container.Indexed.M.Codata

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module OpenModule where

module A where
  postulate X : Set

-- Both open import and open module applies the directives
-- to the "open" rather than to the module.
open import Nat   hiding (zero) renaming (Nat to N)
open module B = A renaming (X to Y)

Test : Set
Test = Y → B.X → N → Nat.Nat

zero : N
zero = Nat.zero

-- If the module isn't opened the directives are applied to
-- the module.
import Nat as N renaming (Nat to N)
module C = A    renaming (X to Z)

Test₂ : Set
Test₂ = N.N → C.Z


text:
-- The category of contexts and renamings
module SOAS.ContextMaps.CategoryOfRenamings {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.ContextMaps.Combinators (ℐ {T})

open import Categories.Functor.Bifunctor
open import Categories.Object.Initial
open import Categories.Object.Coproduct
open import Categories.Category.Cocartesian

import Categories.Morphism

-- The category of contexts and renamings, defined as the Lawvere theory
-- associated with the clone of variables. In elementary terms it has
-- contexts Γ, Δ as objects, and renamings Γ ↝ Δ ≜ Γ ~[ ℐ → ℐ ]↝ Δ as arrows.
𝔽 : Category 0ℓ 0ℓ 0ℓ
𝔽 = categoryHelper (record
  { Obj = Ctx
  ; _⇒_ = _↝_
  ; _≈_ = λ {Γ} ρ₁ ρ₂ → ∀{α : T}{v : ℐ α Γ} → ρ₁ v ≡ ρ₂ v
  ; id = λ x → x
  ; _∘_ = λ ϱ ρ v → ϱ (ρ v)
  ; assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; equiv = record { refl = refl ; sym = λ p → sym p ; trans = λ p q → trans p q }
  ; ∘-resp-≈ = λ{ {f = ρ₁} p₁ p₂ → trans (cong ρ₁ p₂) p₁ }
  })

module 𝔽 = Category 𝔽 using (op) renaming ( _∘_      to _∘ᵣ_
                                          ; _≈_      to _≈ᵣ_
                                          ; id       to idᵣ
                                          ; ∘-resp-≈ to ∘-resp-≈ᵣ )
open 𝔽 public

id′ᵣ : (Γ : Ctx) → Γ ↝ Γ
id′ᵣ Γ = idᵣ {Γ}

-- Category of context is co-Cartesian, given by the empty initial context and
-- context concatenation as the monoidal product.
𝔽:Cocartesian : Cocartesian 𝔽
𝔽:Cocartesian = record
  { initial = record
    { ⊥ = ∅
    ; ⊥-is-initial = record { ! = λ{()} ; !-unique = λ{ f {_} {()}} }
    }
  ; coproducts = record { coproduct = λ {Γ}{Δ} → record
    { A+B = Γ ∔ Δ
    ; i₁ = expandʳ Δ
    ; i₂ = expandˡ Γ
    ; [_,_] = copair
    ; inject₁ = λ{ {Θ}{ρ}{ϱ} → i₁-commute ρ ϱ _ }
    ; inject₂ = λ{ {Θ}{ρ}{ϱ} → i₂-commute ρ ϱ _ }
    ; unique = λ{ p₁ p₂ → unique {Γ}{Δ} _ _ _ p₁ p₂ _ }
    } }
  }
  where

  in₁ : (Γ Δ : Ctx) → Γ ↝ Γ ∔ Δ
  in₁ (α ∙ Γ) Δ new     = new
  in₁ (α ∙ Γ) Δ (old v) = old (in₁ Γ Δ v)

  in₂ : (Γ Δ : Ctx) → Δ ↝ Γ ∔ Δ
  in₂ ∅       Δ v = v
  in₂ (α ∙ Γ) Δ v = old (in₂ Γ Δ v)

  i₁-commute : {Γ Δ Θ : Ctx}{α : T}(ρ : Γ ↝ Θ)(ϱ : Δ ↝ Θ)(v : ℐ α Γ)
             → copair ρ ϱ (expandʳ Δ v) ≡ ρ v
  i₁-commute ρ ϱ new = refl
  i₁-commute ρ ϱ (old v) = i₁-commute (ρ ∘ old) ϱ v

  i₂-commute : {Γ Δ Θ : Ctx}{α : T}(ρ : Γ ↝ Θ)(ϱ : Δ ↝ Θ)(v : ℐ α Δ)
             → copair ρ ϱ (expandˡ Γ v) ≡ ϱ v
  i₂-commute {∅} ρ ϱ v = refl
  i₂-commute {α ∙ Γ} ρ ϱ v = i₂-commute (ρ ∘ old) ϱ v

  unique : {Γ Δ Θ : Ctx}{α : T}(ρ : Γ ↝ Θ)(ϱ : Δ ↝ Θ)(π : Γ ∔ Δ ↝ Θ)
         → (π ∘ᵣ expandʳ Δ ≈ᵣ ρ)
         → (π ∘ᵣ expandˡ Γ ≈ᵣ ϱ)
         → (v : ℐ α (Γ ∔ Δ)) → copair ρ ϱ v ≡ π v
  unique {∅} ρ ϱ π p₁ p₂ v = sym p₂
  unique {α ∙ Γ} ρ ϱ π p₁ p₂ new = sym p₁
  unique {α ∙ Γ} ρ ϱ π p₁ p₂ (old v) = unique (ρ ∘ old) ϱ (π ∘ old) p₁ p₂ v

module 𝔽:Co = Cocartesian 𝔽:Cocartesian
module ∔ = BinaryCoproducts (Cocartesian.coproducts 𝔽:Cocartesian)

-- | Special operations coming from the coproduct structure

-- Concatenation is a bifunctor
∔:Bifunctor : Bifunctor 𝔽 𝔽 𝔽
∔:Bifunctor = 𝔽:Co.-+-

-- Left context concatenation functor Γ ∔ (-) : 𝔽 ⟶ 𝔽, for any context Γ
_∔F- : Ctx → Functor 𝔽 𝔽
Γ ∔F- = Γ ∔.+-

-- Right context concatenation functor (-) ∔ Δ : 𝔽 ⟶ 𝔽, for any context Δ
-∔F_ : Ctx → Functor 𝔽 𝔽
-∔F Δ  = ∔.-+ Δ

-- Functorial mapping and injections
_∣∔∣_ : {Γ₁ Γ₂ Δ₁ Δ₂ : Ctx}(ρ : Γ₁ ↝ Γ₂)(ϱ : Δ₁ ↝ Δ₂) → (Γ₁ ∔ Δ₁) ↝ (Γ₂ ∔ Δ₂)
_∣∔∣_ = ∔._+₁_

_∣∔_ : {Γ₁ Γ₂ : Ctx}(ρ : Γ₁ ↝ Γ₂)(Δ : Ctx) → (Γ₁ ∔ Δ) ↝ (Γ₂ ∔ Δ)
ρ ∣∔ Δ = ρ ∣∔∣ id′ᵣ Δ

_∔∣_ : {Δ₁ Δ₂ : Ctx}(Γ : Ctx)(ϱ : Δ₁ ↝ Δ₂) → (Γ ∔ Δ₁) ↝ (Γ ∔ Δ₂)
Γ ∔∣ ϱ =  id′ᵣ Γ ∣∔∣ ϱ

inl  : (Γ {Δ} : Ctx) → Γ ↝ Γ ∔ Δ
inl Γ {Δ} v = ∔.i₁ {Γ}{Δ} v

inr  : (Γ {Δ} : Ctx) → Δ ↝ Γ ∔ Δ
inr Γ {Δ} v = ∔.i₂ {Γ}{Δ} v

-- Left context concatenation represents weakening a variable in Γ by an
-- arbitrary new context Θ to get a variable in context (Θ ∔ Γ).
module Concatˡ Γ = Functor (Γ ∔F-)
    using () renaming ( F₁           to _∔ᵣ_
                      ; identity     to ∔identity
                      ; homomorphism to ∔homomorphism
                      ; F-resp-≈     to ∔F-resp-≈)
open Concatˡ public

-- Context extension represents weakening by a single type, and it's a special
-- case of context concatenation with a singleton context.
module Ext τ = Functor (⌊ τ ⌋ ∔F-)
    using () renaming ( F₁           to _∙ᵣ_
                      ; identity     to ∙identity
                      ; homomorphism to ∙homomorphism
                      ; F-resp-≈     to ∙F-resp-≈)
open Ext public

-- The two coincide (since add is a special case of copair)
-- but not definitionally: ∙ᵣ is the parallel sum of id : ⌊ τ ⌋ ↝ ⌊ τ ⌋ and ρ : Γ ↝ Δ
-- (i.e. the copairing of expandʳ ⌊ τ ⌋ Δ  : ⌊ τ ⌋ ↝ τ ∙ Δ and old ∘ ρ :  Γ ↝ τ ∙ Δ)
-- while liftᵣ is the copairing of new : ⌊ τ ⌋ ↝ τ ∙ Δ and old ∘ ρ :  Γ ↝ τ ∙ Δ
∙ᵣ-as-add : {α τ : T}{Γ Δ : Ctx} → (ρ : Γ ↝ Δ)(v : ℐ α (τ ∙ Γ))
        → add new (old ∘ ρ) v ≡ (τ ∙ᵣ ρ) v
∙ᵣ-as-add ρ new = refl
∙ᵣ-as-add ρ (old v) = refl

-- Making this a definitional equality simplifies things significantly

-- Right context concatenation is possible but rarely needed.
module Concatʳ Δ =  Functor (-∔F Δ )


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.Support.SetoidPi where

open import Level
open import Function as Fun using (_on_)
open import Relation.Binary as B using () renaming (_=[_]⇒_ to _=[_]⇒₀_; _⇒_ to _⊆_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Relation.Binary.HeterogeneousEquality using (_≅_) renaming (refl to ≅-refl)
open import Relation.Binary.Indexed.Heterogeneous as I using (_=[_]⇒_)
open import Categories.Support.Equivalence
open import Categories.Support.SetoidFunctions as SF using (_⟶_) renaming (_⟨$⟩_ to _⟨$⟩₀_; cong to cong₀)
open Setoid using () renaming (Carrier to Carrier₀; _≈_ to _[_≈_])

_⟶[_,_] : ∀ {cf ℓf} (From : Setoid cf ℓf) (ct ℓt : Level) → Set (cf ⊔ ℓf ⊔ suc (ct ⊔ ℓt))
From ⟶[ ct , ℓt ] = From ⟶ set→setoid (Setoid ct ℓt)

------------------------------------------------------------------------
-- Indexed binary relations
------------------------------------------------------------------------

record IndexedSetoid {i iℓ} (I : Set i) (_∼_ : B.Rel I iℓ) c ℓ : Set (suc (i ⊔ iℓ ⊔ c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : I → Set c
    _≈_           : I.IRel Carrier ℓ
    .isEquivalence : I.IsIndexedEquivalence Carrier _≈_
    -- NOTE one more field, see resp below

  -- no irrelevant opens ☹
  -- .open I.IsEquivalence isEquivalence public
  private
    module E = I.IsIndexedEquivalence
  .refl : I.Reflexive Carrier _≈_
  refl = E.refl isEquivalence
  .sym : I.Symmetric Carrier _≈_
  sym = E.sym isEquivalence
  .trans : I.Transitive Carrier _≈_
  trans = E.trans isEquivalence

  .reflexive : ∀ {i} → _≡_ ⊆ (_≈_ {i})
  reflexive = E.reflexive isEquivalence

  -- conversion to regular setoids by evaluating at an index
  _at_ : I → Setoid c ℓ
  _at_ i = record
    { Carrier = Carrier i
    ; _≈_ = _≈_
    ; isEquivalence = record
      { refl = E.refl isEquivalence
      ; sym = E.sym isEquivalence
      ; trans = E.trans isEquivalence
      }
    }

  -- XXX ideally i should redo the resp stuff and promotion and everything
  -- with the proper setoid of setoids under equivalence, but first i didn't
  -- make it yet and second OH MY GOD                         ─xplat
  Resp-Type = _∼_ =[ _at_ ]⇒₀ _≡_ {A = Setoid c ℓ}
  field
    .resp          : Resp-Type

resp-per : ∀ {c ℓ} {C₁ C₂ : Set c} {_≈₁_ : B.Rel C₁ ℓ} {_≈₂_ : B.Rel C₂ ℓ} {equiv₁ : B.IsEquivalence _≈₁_} {equiv₂ : B.IsEquivalence _≈₂_} → C₁ ≡ C₂ → _≈₁_ ≅ _≈₂_ → _≡_ {A = Setoid c ℓ} record {Carrier = C₁; _≈_ = _≈₁_; isEquivalence = equiv₁} record {Carrier = C₂; _≈_ = _≈₂_; isEquivalence = equiv₂}
resp-per _≡_.refl ≅-refl = _≡_.refl

.resp-per′ : ∀ {c ℓ} (S T : Setoid c ℓ) → (Carrier₀ S ≡ Carrier₀ T) → (Setoid._≈_ S ≅ Setoid._≈_ T) → S ≡ T
resp-per′ S T = resp-per {equiv₁ = Setoid.isEquivalence S} {equiv₂ = Setoid.isEquivalence T}

open IndexedSetoid using (_at_)

weaken : ∀ {c ℓ} → Setoid c ℓ → ∀ {i iℓ} {I : Set i} {_∼_ : B.Rel I iℓ} → IndexedSetoid I _∼_ c ℓ
weaken S {I = I} {_∼_} = record
  { Carrier = Fun.const S.Carrier
  ; _≈_ = S._≈_
  ; isEquivalence = record { refl = S.refl; sym = S.sym; trans = S.trans }
  ; resp = Fun.const _≡_.refl
  }
  where module S = Setoid S

{-
-- this definition is unusable because agda spins in circles trying to infer
-- ct and ℓt before it will extract any information from f's type, but f's
-- type is the only thing it can infer them from... test is below ☹
_[$]_ : ∀ {cf ℓf ct ℓt} {From : Setoid cf ℓf} → (From ⟶[ ct , ℓt ]) → Carrier From → Set ct
f [$] x = Carrier (f ⟨$⟩₀ x)

.test : ∀ {cf ℓf ct ℓt} {From : Setoid cf ℓf} (To : From ⟶[ ct , ℓt ]) (x : Carrier From) → (_[$]_ {ct = ct}{ℓt = ℓt} To x) → Set ℓt
test = {!!}
-}

-- i think this approach would work beautifully with regular setoids, but
-- with irrelevant setoids the type of cong can't depend on localize
--                                                          ─ xplat

-- .localize : ∀ {cf ℓf ct ℓt} {From : Setoid cf ℓf} (To : From ⟶[ ct , ℓt ]) {x y : Carrier₀ From} → From [ x ≈ y ] → B.REL (Carrier₀ (To ⟨$⟩₀ x)) (Carrier₀ (To ⟨$⟩₀ y)) ℓt
-- localize To {x} x≈y with To ⟨$⟩₀ x | cong₀ To x≈y
-- localize To x≈y | ._ | _≡_.refl = Setoid._≈_ (To ⟨$⟩₀ _)

-- ... so it's on to yet another annoying heterogeneous equality type
module SetoidHetero {cf ℓf} (From : Setoid cf ℓf) (ct ℓt : Level) (To : From ⟶[ ct , ℓt ]) where
  I = Carrier₀ From
  To$ = _⟨$⟩₀_ To
  To$C = Fun._∘_ Carrier₀ (_⟨$⟩₀_ To)

  localize′ : ∀ {S T : Setoid ct ℓt} → (S ≡ T) → B.REL (Carrier₀ S) (Carrier₀ T) ℓt
  -- localize′ {S} {T} S≡T
  localize′ {S} _≡_.refl = Setoid._≈_ S

  localize : ∀ {x y : I} → (To$ x ≡ To$ y) → B.REL (To$C x) (To$C y) ℓt
  localize {x} {y} To$x≡To$y with To$ y
  localize {x} _≡_.refl | ._ = Setoid._≈_ (To$ x)

  data _≈∗_ {S T : Setoid ct ℓt} (x : Carrier₀ S) : (y : Carrier₀ T) → Set (suc (ct ⊔ ℓt)) where
    locally : (S≡T : S ≡ T)
      {y : Carrier₀ T} (x≈y : localize′ S≡T x y) →
      _≈∗_ {S} {T} x y

  _≈⋆_ : {iˣ iʸ : I} → B.REL (To$C iˣ) (To$C iʸ) (suc (ct ⊔ ℓt))
  _≈⋆_ {iˣ} {iʸ} = _≈∗_ {To$ iˣ} {To$ iʸ}

asIndexed : ∀ {cf ℓf} ct ℓt {From : Setoid cf ℓf} → (From ⟶[ ct , ℓt ]) → IndexedSetoid (Carrier₀ From) (Setoid._≈_ From) ct (suc (ct ⊔ ℓt))
asIndexed ct ℓt {From} To = record
  { Carrier = To$C
  ; _≈_ = _≈⋆_
  ; isEquivalence = record
    { refl = my-refl
    ; sym = my-sym
    ; trans = my-trans
    }
  ; resp = λ {i j} i∼j → resp-per′ (fake-at i) (fake-at j) (resp-helper i∼j) (resp-helper₂ i∼j)
  }
  where
  open SetoidHetero _ ct ℓt To

  .my-refl : I.Reflexive To$C _≈⋆_
  my-refl {i} {x} = locally {To$ i} _≡_.refl ((Setoid.refl (To$ i)))

  .sym-helper : ∀ i j (To$i≡To$j : To$ i ≡ To$ j) (x : To$C i) (y : To$C j) (x≈y : localize′ To$i≡To$j x y) → localize′ (PE.sym To$i≡To$j) y x
  sym-helper i j To$i≡To$j x y with To$ j
  sym-helper i j _≡_.refl x y | ._ = Setoid.sym (To$ i)

  .my-sym : I.Symmetric To$C _≈⋆_
  my-sym {i} {j} {x} {y} (locally To$i≡To$j x≈y) = locally (PE.sym To$i≡To$j) (sym-helper i j To$i≡To$j x y x≈y)

  .trans-helper : ∀ i j k (To$i≡To$j : To$ i ≡ To$ j) (To$j≡To$k : To$ j ≡ To$ k) (x : To$C i) (y : To$C j) (z : To$C k) (x≈y : localize′ To$i≡To$j x y) (y≈z : localize′ To$j≡To$k y z) → localize′ (PE.trans To$i≡To$j To$j≡To$k) x z
  trans-helper i j k To$i≡To$j To$j≡To$k x y z with To$ j | To$ k
  trans-helper i j k _≡_.refl _≡_.refl x y z | ._ | ._ = Setoid.trans (To$ i)

  .my-trans : I.Transitive To$C _≈⋆_
  my-trans (locally To$i≡To$j x≈y) (locally To$j≡To$k y≈z) = locally (PE.trans To$i≡To$j To$j≡To$k) (trans-helper _ _ _ To$i≡To$j To$j≡To$k _ _ _ x≈y y≈z)

  .resp-helper : ∀ {i j} → From [ i ≈ j ] → To$C i ≡ To$C j
  resp-helper i∼j = PE.cong Carrier₀ (cong₀ To i∼j)

  .resp-helper₃ : (S T : Setoid ct ℓt) → S ≡ T → _≈∗_ {S} {S} ≅ _≈∗_ {T} {T}
  resp-helper₃ S .S _≡_.refl = ≅-refl

  .resp-helper₂ : ∀ {i j} → From [ i ≈ j ] → _≈⋆_ {i} {i} ≅ _≈⋆_ {j} {j}
  resp-helper₂ {i} {j} i∼j = resp-helper₃ (To$ i) (To$ j) (cong₀ To i∼j)

  fake-at : ∀ i → Setoid ct (suc (ct ⊔ ℓt))
  fake-at i = record
    { Carrier = To$C i
    ; _≈_ = _≈⋆_ {i} {i}
    ; isEquivalence = record
      { refl = my-refl
      ; sym = my-sym
      ; trans = my-trans
      }
    }

------------------------------------------------------------------------
-- Functions which preserve equality

record Π {f₁ f₂ t₁ t₂}
         (From : Setoid f₁ f₂)
         (To : IndexedSetoid (Carrier₀ From) (Setoid._≈_ From) t₁ t₂) :
         Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  open I using (_=[_]⇒_)
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : (x : Carrier₀ From) → IndexedSetoid.Carrier To x
    .cong : Setoid._≈_ From =[ _⟨$⟩_ ]⇒ IndexedSetoid._≈_ To

open Π public

Π′ : ∀ {cf ℓf} (ct ℓt : Level) (From : Setoid cf ℓf) (To : From ⟶[ ct , ℓt ]) → Set (cf ⊔ ℓf ⊔ suc (ct ⊔ ℓt))
Π′ ct ℓt From To = Π From (asIndexed ct ℓt To)

-- Pis that 'just happen' to be independent, instead of being necessarily so.

infixr 0 _⟶Π_

_⟶Π_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Set _
From ⟶Π To = Π From (weaken To)

-- Identity and composition.

id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶Π A
id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }

infixr 9 _∙′_

_∙′_ : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
        {b₁ b₂} {B : Setoid b₁ b₂}
        {c₁ c₂} {C : Setoid c₁ c₂} →
      B ⟶Π C → A ⟶Π B → A ⟶Π C
f ∙′ g = record
  { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
  ; cong  = Fun._∘_ (cong  f) (cong  g)
  }

infixr 9 _[_○_]

-- XXX this shouldn't need B, but it can't be inferred from f's type
_[_○_] : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
           {b₁ b₂} (B : Setoid b₁ b₂)
           {c₁ c₂} (C : IndexedSetoid _ (Setoid._≈_ B) c₁ c₂) →
         (A ⟶Π B) → IndexedSetoid _ _ c₁ c₂
B [ C ○ f ] = record
  { Carrier = Fun._∘_ C.Carrier (_⟨$⟩_ f)
  ; _≈_ = C._≈_
  ; isEquivalence = record { refl = C.refl; sym = C.sym; trans = C.trans }
  ; resp = Fun._∘_ C.resp (cong f)
  }
  where module C = IndexedSetoid C

-- PROPER.  well, halfway.
infixr 9 _∙_

_∙_ : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
        {b₁ b₂} {B : Setoid b₁ b₂}
        {c₁ c₂} {C : IndexedSetoid _ _ c₁ c₂} →
      (f : Π B C) → (g : A ⟶Π B) → Π A (B [ C ○ g ])
f ∙ g = record
  { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
  ; cong  = Fun._∘_ (cong  f) (cong  g)
  }

-- Constant equality-preserving function.

const : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
          {b₁ b₂} {B : Setoid b₁ b₂} →
        Carrier₀ B → A ⟶Π B
const {B = B} b = record
  { _⟨$⟩_ = Fun.const b
  ; cong  = Fun.const (Setoid.refl B)
  }

------------------------------------------------------------------------
-- Function setoids

-- Dependent.

setoid : ∀ {f₁ f₂ t₁ t₂}
         (From : Setoid f₁ f₂) →
         IndexedSetoid (Carrier₀ From) (Setoid._≈_ From) t₁ t₂ →
         Setoid _ _
setoid From To = record
  { Carrier       = Π From To
  ; _≈_           = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
  ; isEquivalence = record
    { refl  = λ {f} → cong f
    ; sym   = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
    ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
    }
  }
  where
  open module From = Setoid      From using () renaming (_≈_ to _≈₁_)
  open module To = IndexedSetoid To   using () renaming (_≈_ to _≈₂_)

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 #-}

-- This module provides the basic expression type for polynomials.

module Polynomial.Expr where

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

infixl 6 _⊕_
infixl 7 _⊗_
infixr 8 _⊛_
data Expr  {ℓ} (A : Set ℓ) (n : ℕ) : Set ℓ where
  Κ   : A → Expr A n
  Ι   : Fin n → Expr A n
  _⊕_ : Expr A n → Expr A n → Expr A n
  _⊗_ : Expr A n → Expr A n → Expr A n
  _⊛_ : Expr A n → ℕ → Expr A n
  ⊝_  : Expr A n → Expr A n

open import Polynomial.Parameters

module Eval {c r₁ r₂ r₃} (homo : Homomorphism c r₁ r₂ r₃) where
  open Homomorphism homo
  open import Polynomial.Exponentiation rawRing

  open import Data.Vec as Vec using (Vec)

  ⟦_⟧ : ∀ {n} → Expr Raw.Carrier n → Vec Carrier n → Carrier
  ⟦ Κ x ⟧ ρ = ⟦ x ⟧ᵣ
  ⟦ Ι x ⟧ ρ = Vec.lookup ρ x
  ⟦ x ⊕ y ⟧ ρ = ⟦ x ⟧ ρ + ⟦ y ⟧ ρ
  ⟦ x ⊗ y ⟧ ρ = ⟦ x ⟧ ρ * ⟦ y ⟧ ρ
  ⟦ ⊝ x ⟧ ρ = - ⟦ x ⟧ ρ
  ⟦ x ⊛ i ⟧ ρ = ⟦ x ⟧ ρ ^ i

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
-- 2012-09-25 Andreas, reported by Nicolas Pouillard
{-# OPTIONS --sized-types #-}
module Issue700 where

import Common.Level
open import Common.Size

postulate
  Size< : Size → Set
{-# BUILTIN SIZELT Size< #-}

postulate
  A : Set

data T (i : Size) : Set where
  c : (j : Size< i) → T j → T _

bug : ∀ i → T i → A
bug i (c j x) = bug j x

{- WAS: de Bruijn index out of scope

Issue700.bug is projection like in argument 1 for type Issue700.T
Translated clause:
  delta = (j : Size< @0) (x : T j)
  perm  = x0,x1 -> x0,x1
  ps    = [r(ConP Issue700.T.c Nothing [r(VarP "j"),r(VarP "x")])]
  body  = Bind (Abs "h1" Bind (Abs "h2" Body (Def Issue700.bug [r(Var 1 []),r(Var 0 [])])))
  body  = [h1 h2] bug h1 h2
-}

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- {-# OPTIONS -v term:30 #-}
{-# OPTIONS --copatterns #-}
module ColistMutual where

mutual

  data CoList (A : Set) : Set where
    []  : CoList A
    _∷_ : (x : A)(xs : ∞CoList A) → CoList A

  record ∞CoList (A : Set) : Set where
    coinductive
    field out : CoList A

open ∞CoList

mutual

  repeat : {A : Set}(a : A) → CoList A
  repeat a = a ∷ ∞repeat a

  ∞repeat : {A : Set}(a : A) → ∞CoList A
  out (∞repeat a) = repeat a

-- example by Thorsten and Nisse, PAR 2010

data Tree : Set where
  node : CoList Tree → Tree

mutual

  bad : Tree
  bad = node (node [] ∷ bads)

  bads : ∞CoList Tree
  out bads = bad ∷ bads
  -- should not termination check

CRASH -- TODO fix termination checker

{-
data Bool : Set where
  true false : Bool

mutual

  shape : Tree → Bool
  shape (node []) = false
  shape (node (_ ∷ l)) = shapes (out l)

  shapes : CoList Tree → Bool
  shapes [] = false
  shapes (t ∷ _) = shape t

-- shape/shapes may not termination check
-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Saturated sets.

module SAT3 where

open import Library
open import Terms
open import Substitution
open import Reduction
open import SN
open import SN.AntiRename

-- Kripke predicates on well-typed terms.

TmSet : (a : Ty) → Set₁
TmSet a = {Γ : Cxt} (t : Tm Γ a) → Set

_⊆_ : ∀{a} (𝑨 𝑨′ : TmSet a) → Set
𝑨 ⊆ 𝑨′ = ∀{Γ}{t : Tm Γ _} → 𝑨 t → 𝑨′ t

-- Closure by strong head expansion

Closed : ∀ {a} (𝑨 : TmSet a) → Set
Closed 𝑨 = ∀{Γ}{t t' : Tm Γ _} → t ⟨ _ ⟩⇒ t' → 𝑨 t' → 𝑨 t

data Cl {a} (𝑨 : TmSet a) {Γ} (t : Tm Γ a) : Set where
  emb : 𝑨 t                             → Cl 𝑨 t
  exp : ∀{t'} → t ⟨ _ ⟩⇒ t' → Cl 𝑨 t' → Cl 𝑨 t

-- Function space.

_[→]_ : ∀{a b} → TmSet a → TmSet b → TmSet (a →̂ b)
(𝓐 [→] 𝓑) {Γ} t = ∀{Δ} (ρ : Δ ≤ Γ) → {u : Tm Δ _} → 𝓐 u → 𝓑 (app (rename ρ t) u)

-- Saturated term sets.

record IsSAT {a} (𝑨 : TmSet a) : Set where
  -- constructor isSat
  field
    satSNe  : SNe ⊆ 𝑨
    satSN   : 𝑨 ⊆ SN
    satExp  : Closed 𝑨
    satRename : ∀ {Γ Δ} → (ρ : Ren Γ Δ) → ∀ {t} → 𝑨 t → 𝑨 (subst ρ t)
--open IsSAT

record SAT (a : Ty) : Set₁ where
  -- constructor sat
  field
    satSet  : TmSet a
    satProp : IsSAT satSet

  open IsSAT satProp public
open SAT public

-- Elementhood for saturated sets.
-- We use a record to instead of just application to help Agda's unifier.
record _∈_ {a Γ} (t : Tm Γ a) (𝓐 : SAT a) : Set where
  constructor ↿_
  field       ⇃_ : satSet 𝓐 t
open _∈_ public

-- Variables inhabit saturated sets.

⟦var⟧ : ∀{a} (𝓐 : SAT a) {Γ} (x : Var Γ a) → var x ∈ 𝓐
⟦var⟧ 𝓐 x = ↿ (satSNe 𝓐 (var x))

-- Smallest semantic type.

⟦⊥⟧ : SAT base
⟦⊥⟧ = record
  { satSet  = SN
  ; satProp = record
    { satSNe    = ne
    ; satSN     = id
    ; satExp    = exp
    ; satRename = renameSN
    }
  }

-- Semantic function type.

_⟦→⟧_ : ∀ {a b} (𝓐 : SAT a) (𝓑 : SAT b) → SAT (a →̂ b)
𝓐 ⟦→⟧ 𝓑 = record
  { satSet  = 𝑪
  ; satProp = record
    { satSNe = CSNe
    ; satSN  = CSN
    ; satExp = CExp
    ; satRename = λ ρ {t} 𝒕 ρ₁ {u} 𝒖 → ≡.subst (λ t₁ → 𝑩 (app t₁ u)) (subst-∙ ρ₁ ρ t) (𝒕 (λ x₂ → ρ₁ (ρ x₂)) 𝒖)
    }
  }
  where
    module 𝓐 = SAT 𝓐
    module 𝓑 = SAT 𝓑
    𝑨 = 𝓐.satSet
    𝑩 = 𝓑.satSet
    𝑪 : TmSet (_ →̂ _)
    𝑪 t = (𝑨 [→] 𝑩) t

    CSNe : SNe ⊆ 𝑪
    CSNe 𝒏 ρ 𝒖 = 𝓑.satSNe (sneApp (renameSNe ρ 𝒏) (𝓐.satSN 𝒖))

    CSN : 𝑪 ⊆ SN
    CSN 𝒕 = unRenameSN (prop→Ind suc ≡.refl) (absVarSN (𝓑.satSN (𝒕 _ (𝓐.satSNe (var v₀)))))

    CExp : ∀{Γ}{t t' : Tm Γ _} → t ⟨ _ ⟩⇒ t' → 𝑪 t' → 𝑪 t
    CExp t⇒ 𝒕 ρ 𝒖 = 𝓑.satExp ((cong (appl _) (appl _) (subst⇒ (renSN ρ) t⇒))) (𝒕 ρ 𝒖)

-- Lemma: If 𝓐, 𝓑 ∈ SAT and t[u] ∈ 𝓑 for all a ∈ 𝓐, then λt ∈ 𝓐 ⟦→⟧ 𝓑

⟦abs⟧ : ∀{a b}{𝓐 : SAT a}{𝓑 : SAT b}{Γ}{t : Tm (a ∷ Γ) b} →
    (∀ {Δ} (ρ : Δ ≤ Γ) {u : Tm Δ a} →
      u ∈ 𝓐 → (subst0 u (subst (lifts ρ) t)) ∈ 𝓑 ) → abs t ∈ (𝓐 ⟦→⟧ 𝓑)
(⇃ ⟦abs⟧ {𝓐 = 𝓐}{𝓑 = 𝓑} 𝒕) ρ 𝒖 =
  SAT.satExp 𝓑 (β (SAT.satSN 𝓐 𝒖)) (⇃ 𝒕 ρ (↿ 𝒖))

-- Lemma: If 𝓐, 𝓑 ∈ SAT and t ∈ 𝓐 ⟦→⟧ 𝓑 and u ∈ 𝓐, then app t u ∈ 𝓑

⟦app⟧ : ∀ {a b} {𝓐 : SAT a} {𝓑 : SAT b} {Γ} {t : Tm Γ (a →̂ b)} {u : Tm Γ a} →
        t ∈ (𝓐 ⟦→⟧ 𝓑) → u ∈ 𝓐 → app t u ∈ 𝓑
⟦app⟧ {𝓑 = 𝓑} {u = u} (↿ 𝒕) (↿ 𝒖) = ≡.subst (λ t → app t u ∈ 𝓑) renId (↿ 𝒕 _ 𝒖)

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
{-

Some basic utilities for reflection

-}
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Reflection.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.List.Base
open import Cubical.Data.Nat.Base

import Agda.Builtin.Reflection as R
open import Agda.Builtin.String

_>>=_ = R.bindTC
_<|>_ = R.catchTC

_$_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → A → B
f $ a = f a

_>>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → R.TC A → R.TC B → R.TC B
f >> g = f >>= λ _ → g

infixl 4 _>>=_ _>>_ _<|>_
infixr 3 _$_

liftTC : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → R.TC A → R.TC B
liftTC f ta = ta >>= λ a → R.returnTC (f a)

v : ℕ → R.Term
v n = R.var n []

pattern varg t = R.arg (R.arg-info R.visible R.relevant) t
pattern harg t = R.arg (R.arg-info R.hidden R.relevant) t
pattern _v∷_ a l = varg a ∷ l
pattern _h∷_ a l = harg a ∷ l

infixr 5 _v∷_ _h∷_

vlam : String → R.Term → R.Term
vlam str t = R.lam R.visible (R.abs str t)

newMeta = R.checkType R.unknown

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- Andreas, 2013-11-08
module Issue532 where

module M (A : Set) where
  postulate
    ax : A
    P  : A → Set

record R (A : Set) : Set where
  open M A public
  field
    f : P ax
open R

-- Error WAS:
-- Not a valid let-declaration
-- when scope checking let open M A public in (f : P ax) → Set₀

S : {A : Set} → R A → Set
S r = P r (ax r)

-- Works now.


text:
{-# OPTIONS --type-in-type #-}  -- yes, there will be some cheating in this lecture

module Lec4Done where

open import Lec1Done
open import Lec2Done
open import Lec3Done

-- the identity functor (the identity action on objects and arrows)
ID : {C : Category} -> C => C
ID = id~> where open Category CATEGORY

-- composition of functors (composition of actions on objects and arrows)
_>F>_ : {C D E : Category} -> (C => D) -> (D => E) -> (C => E)
F >F> G = F >~> G where open Category CATEGORY

-- EXAMPLES

data Maybe (X : Set) : Set where
  yes : (x : X) -> Maybe X
  no  : Maybe X

maybe : {X Y : Set} -> (X -> Y) -> Maybe X -> Maybe Y
maybe f (yes x) = yes (f x)
maybe f no      = no

MAYBE : SET => SET
MAYBE = record
  { F-Obj = Maybe
  ; F-map = maybe
  ; F-map-id~> = extensionality \ { (yes x) -> refl (yes x) ; no -> refl no }
  ; F-map->~> = \ f g -> extensionality \ { (yes x) -> refl (yes (g (f x))) ; no -> refl no }
  }

module MAYBE-CAT where
  open Category SET
  open _=>_ MAYBE
  joinMaybe : {X : Set} -> Maybe (Maybe X) -> Maybe X
  joinMaybe no            = no        -- goes wrong sooner
  joinMaybe (yes mx)      = mx        -- maybe goes wrong later
  MAYBE-CAT : Category
  MAYBE-CAT = record
                { Obj = Set
                ; _~>_ = \ S T -> S -> Maybe T
                ; id~>  = yes
                ; _>~>_ = \ f g -> f >~> maybe g >~> joinMaybe
                ; law-id~>>~> = \ f -> extensionality \ x -> help1 (f x)
                ; law->~>id~> = \ f -> extensionality \ x -> help2 (f x)
                ; law->~>>~>  = \ f g h -> extensionality \ x -> help3 g h (f x)
                } where
    help1 : {T : Set} (w : Maybe T) -> joinMaybe (yes w) == w
    help1 mx = refl mx
    help2 : {T : Set} (w : Maybe T) -> joinMaybe (maybe yes w) == w
    help2 (yes x) = refl (yes x)
    help2 no = refl no
    help3 : {R S T : Set} (g : R -> Maybe S) (h : S -> Maybe T)
          (w : Maybe R) ->
        joinMaybe (maybe h (joinMaybe (maybe g w))) ==
        joinMaybe (maybe (\ x -> joinMaybe (maybe h (g x))) w)
    help3 g h (yes x) with g x
    help3 g h (yes x) | yes y = refl (h y)
    help3 g h (yes x) | no = refl no
    help3 g h no = refl no

module NATURAL-TRANSFORMATION {C D : Category} where
  open Category
  open _=>_

  record _~~>_ (F G : C => D) : Set where
    field
      -- one operation
      xform : {X : Obj C} -> _~>_ D (F-Obj F X) (F-Obj G X)
      -- one law
      xform-natural : {X Y : Obj C}(f : _~>_ C X Y) ->
                      _>~>_ D (F-map F f) (xform {Y})
                      ==
                      _>~>_ D (xform {X}) (F-map G f)

module MAYBE-GADGETS where
  open NATURAL-TRANSFORMATION {SET}{SET}
  open Category SET
  open _=>_ MAYBE
  open _~~>_

  unitMaybe : ID ~~> MAYBE
  unitMaybe = record
    { xform = yes
    ; xform-natural = \ f -> refl (f >~> yes)
    }

  multMaybe : (MAYBE >F> MAYBE) ~~> MAYBE
  multMaybe = record
    { xform = MAYBE-CAT.joinMaybe
    ; xform-natural = \ f -> extensionality \
       { (yes (yes x)) -> refl (yes (f x))
       ; (yes no) -> refl no
       ; no -> refl no }
    }

  law1 : {X : Set} -> (xform unitMaybe >~> xform multMaybe) == id~> {Maybe X}
  law1 = extensionality \ { (yes x) -> refl (yes x) ; no -> refl no }

  law2 : {X : Set} -> (F-map (xform unitMaybe) >~> xform multMaybe) == id~> {Maybe X}
  law2 = extensionality \ { (yes x) -> refl (yes x) ; no -> refl no }

  law3 : {X : Set} -> (xform multMaybe >~> xform multMaybe)
                   == (F-map (xform multMaybe) >~> xform multMaybe {X})
  law3 = extensionality \ { (yes (yes mx)) -> refl mx ; (yes no) -> refl no ; no -> refl no }

  MAYBE-CAT2 : Category
  MAYBE-CAT2 = record
    { Obj = Set
    ; _~>_ = \ S T -> S -> Maybe T
    ; id~> = xform unitMaybe
    ; _>~>_ = \ f g -> f >~> F-map g >~> xform multMaybe
    ; law-id~>>~> = \ f ->
        xform unitMaybe >~> F-map f >~> xform multMaybe
          =< law->~>>~> (xform unitMaybe) (F-map f) (xform multMaybe) ]=
        (xform unitMaybe >~> F-map f) >~> xform multMaybe
          =< refl (_>~> xform multMaybe) =$= xform-natural unitMaybe f ]=
        (f >~> xform unitMaybe) >~> xform multMaybe
          =[ law->~>>~> f (xform unitMaybe) (xform multMaybe) >=
        f >~> (xform unitMaybe >~> xform multMaybe)
          =[ refl (f >~>_) =$= law1 >=
        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]
    ; law->~>id~> = \ f ->
        f >~> (F-map (xform unitMaybe) >~> xform multMaybe)
          =[ refl (f >~>_) =$= law2 >=
        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]
    ; law->~>>~> = \ f g h ->
        (f >~> (F-map g >~> xform multMaybe)) >~> (F-map h >~> xform multMaybe)
          =[ law->~>>~> f (F-map g >~> xform multMaybe) (F-map h >~> xform multMaybe) >=
        f >~> (F-map g >~> xform multMaybe) >~> (F-map h >~> xform multMaybe)
          =[ refl (f >~>_) =$= (
            (F-map g >~> xform multMaybe) >~> (F-map h >~> xform multMaybe)
              =[ law->~>>~> (F-map g) (xform multMaybe) (F-map h >~> xform multMaybe) >=
            F-map g >~> (xform multMaybe >~> (F-map h >~> xform multMaybe))
              =[ refl (F-map g >~>_) =$= (
                xform multMaybe >~> (F-map h >~> xform multMaybe)
                  =< law->~>>~> (xform multMaybe) (F-map h) (xform multMaybe) ]=
                (xform multMaybe >~> F-map h) >~> xform multMaybe
                  =< refl (_>~> xform multMaybe) =$= xform-natural multMaybe h ]=
                (F-map (F-map h) >~> xform multMaybe) >~> xform multMaybe
                  =[ law->~>>~> (F-map (F-map h)) (xform multMaybe) (xform multMaybe) >=
                F-map (F-map h) >~> (xform multMaybe >~> xform multMaybe)
                  =[ refl (F-map (F-map h) >~>_) =$= law3 >=
                F-map (F-map h) >~> (F-map (xform multMaybe) >~> xform multMaybe)
                  =< law->~>>~> (F-map (F-map h)) (F-map (xform multMaybe)) (xform multMaybe) ]=
                (F-map (F-map h) >~> F-map (xform multMaybe)) >~> xform multMaybe
                  =< refl (_>~> xform multMaybe) =$= F-map->~> (F-map h) (xform multMaybe) ]=
                (F-map (F-map h >~> xform multMaybe) >~> xform multMaybe) [QED]
              ) >=
            F-map g >~> (F-map (F-map h >~> xform multMaybe) >~> xform multMaybe)
              =< law->~>>~> (F-map g) (F-map (F-map h >~> xform multMaybe)) (xform multMaybe) ]=
            (F-map g >~> F-map (F-map h >~> xform multMaybe)) >~> xform multMaybe
              =< refl (_>~> xform multMaybe) =$= F-map->~> g (F-map h >~> xform multMaybe) ]=
            (F-map (g >~> F-map h >~> xform multMaybe) >~> xform multMaybe) [QED]
          ) >=
        (f >~> F-map (g >~> F-map h >~> xform multMaybe) >~> xform multMaybe) [QED]
    }

module MONAD {C : Category}(M : C => C) where
  open NATURAL-TRANSFORMATION {C}{C}
  open Category C
  open _=>_ M
  open _~~>_

  record Monad : Set where
    field
      unit :        ID ~~> M
      mult : (M >F> M) ~~> M

      unitMult : {X : Obj} -> (xform unit >~> xform mult) == id~> {F-Obj X}
      multUnit : {X : Obj} -> (F-map (xform unit) >~> xform mult) == id~> {F-Obj X}
      multMult : {X : Obj} -> (xform mult >~> xform mult) == (F-map (xform mult) >~> xform mult {X})

    KLEISLI : Category
    KLEISLI = record
      { Obj = Obj
      ; _~>_ = \ S T -> S ~> F-Obj T
      ; id~>  = xform unit
      ; _>~>_ = \ f g -> f >~> F-map g >~> xform mult
      ; law-id~>>~> = \ f ->
        xform unit >~> F-map f >~> xform mult
          =< law->~>>~> (xform unit) (F-map f) (xform mult) ]=
        (xform unit >~> F-map f) >~> xform mult
          =< refl (_>~> xform mult) =$= xform-natural unit f ]=
        (f >~> xform unit) >~> xform mult
          =[ law->~>>~> f (xform unit) (xform mult) >=
        f >~> (xform unit >~> xform mult)
          =[ refl (f >~>_) =$= unitMult >=
        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]
      ; law->~>id~> = \ f ->
        f >~> (F-map (xform unit) >~> xform mult)
          =[ refl (f >~>_) =$= multUnit >=
        f >~> id~>
          =[ law->~>id~> f >=
        f [QED]
      ; law->~>>~> = \ f g h ->
        (f >~> (F-map g >~> xform mult)) >~> (F-map h >~> xform mult)
          =[ law->~>>~> f (F-map g >~> xform mult) (F-map h >~> xform mult) >=
        f >~> (F-map g >~> xform mult) >~> (F-map h >~> xform mult)
          =[ refl (f >~>_) =$= (
            (F-map g >~> xform mult) >~> (F-map h >~> xform mult)
              =[ law->~>>~> (F-map g) (xform mult) (F-map h >~> xform mult) >=
            F-map g >~> (xform mult >~> (F-map h >~> xform mult))
              =[ refl (F-map g >~>_) =$= (
                xform mult >~> (F-map h >~> xform mult)
                  =< law->~>>~> (xform mult) (F-map h) (xform mult) ]=
                (xform mult >~> F-map h) >~> xform mult
                  =< refl (_>~> xform mult) =$= xform-natural mult h ]=
                (F-map (F-map h) >~> xform mult) >~> xform mult
                  =[ law->~>>~> (F-map (F-map h)) (xform mult) (xform mult) >=
                F-map (F-map h) >~> (xform mult >~> xform mult)
                  =[ refl (F-map (F-map h) >~>_) =$= multMult >=
                F-map (F-map h) >~> (F-map (xform mult) >~> xform mult)
                  =< law->~>>~> (F-map (F-map h)) (F-map (xform mult)) (xform mult) ]=
                (F-map (F-map h) >~> F-map (xform mult)) >~> xform mult
                  =< refl (_>~> xform mult) =$= F-map->~> (F-map h) (xform mult) ]=
                (F-map (F-map h >~> xform mult) >~> xform mult) [QED]
              ) >=
            F-map g >~> (F-map (F-map h >~> xform mult) >~> xform mult)
              =< law->~>>~> (F-map g) (F-map (F-map h >~> xform mult)) (xform mult) ]=
            (F-map g >~> F-map (F-map h >~> xform mult)) >~> xform mult
              =< refl (_>~> xform mult) =$= F-map->~> g (F-map h >~> xform mult) ]=
            (F-map (g >~> F-map h >~> xform mult) >~> xform mult) [QED]
          ) >=
        (f >~> F-map (g >~> F-map h >~> xform mult) >~> xform mult) [QED]
      }

data List (X : Set) : Set where
  []   : List X
  _,-_ : (x : X)(xs : List X) -> List X

list : {X Y : Set} -> (X -> Y) -> List X -> List Y
list f []         = []
list f (x ,- xs)  = f x ,- list f xs

LIST : SET => SET
LIST = record
  { F-Obj = List
  ; F-map = list
  ; F-map-id~> = extensionality listId
  ; F-map->~> = \ f g -> extensionality (listCp f g)
  } where
  open Category SET
  listId : {T : Set}(xs : List T) -> list id xs == xs
  listId []        = refl []
  listId (x ,- xs) = refl (_,-_ x) =$= listId xs
  listCp : {R S T : Set} (f : R -> S) (g : S -> T) (xs : List R) →
           list (f >~> g) xs == (list f >~> list g) xs
  listCp f g [] = refl []
  listCp f g (x ,- xs) = refl (_,-_ (g (f x))) =$= listCp f g xs

data Two : Set where tt ff : Two

data BitProcess (X : Set) : Set where  -- in what way is X used?
  stop : (x : X) -> BitProcess X                       -- stop with value x
  send : (b : Two)(k : BitProcess X) -> BitProcess X   -- send b, continue as k
  recv : (kt kf : BitProcess X) -> BitProcess X        -- receive bit, continue as
                                                       --   kt if tt, kf if ff

bpRun : forall {X} ->  BitProcess X   -- a process to run
                   ->  List Two       -- a list of bits waiting to be input
                   ->  List Two       -- the list of bits output
                    *  Maybe          -- and, if we don't run out of input
                       (  X           -- the resulting value
                       *  List Two    -- and the unused input
                       )
bpRun (stop x)     bs                      = []         , yes (x , bs)
bpRun (send b k)   bs with bpRun k bs
bpRun (send b k)   bs | os , yes (x , is)  = (b ,- os)  , yes (x , is)
bpRun (send b k)   bs | os , no            = os         , no
bpRun (recv kt kf) []                      = []         , no
bpRun (recv kt kf) (tt ,- bs)              = bpRun kt bs
bpRun (recv kt kf) (ff ,- bs)              = bpRun kf bs

bitProcess : {X Y : Set} -> (X -> Y) -> BitProcess X -> BitProcess Y
bitProcess f (stop x) = stop (f x)
bitProcess f (send b k) = send b (bitProcess f k)
bitProcess f (recv kt kf) = recv (bitProcess f kt) (bitProcess f kf)

BITPROCESS : SET => SET  -- actions on *values* lift to processes
BITPROCESS = record
  { F-Obj = BitProcess
  ; F-map = bitProcess
  ; F-map-id~> = extensionality helpId
  ; F-map->~> = \ f g -> extensionality (helpCp f g)
  } where
  open Category SET
  helpId : {T : Set} (p : BitProcess T) -> bitProcess id p == p
  helpId (stop x) = refl (stop x)
  helpId (send b k) rewrite helpId k = refl (send b k)
  helpId (recv kt kf) rewrite helpId kt | helpId kf = refl (recv kt kf)
  helpCp : {R S T : Set} (f : R -> S)(g : S -> T) (p : BitProcess R) →
         bitProcess (f >~> g) p == (bitProcess f >~> bitProcess g) p
  helpCp f g (stop x) = refl (stop (g (f x)))
  helpCp f g (send b k) rewrite helpCp f g k = refl (send b (bitProcess g (bitProcess f k)))
  helpCp f g (recv kt kf) rewrite helpCp f g kt | helpCp f g kf
    = refl (recv (bitProcess g (bitProcess f kt)) (bitProcess g (bitProcess f kf)))

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
data Bool : Set where
  true false : Bool

{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE true #-}  -- hmm, no

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Sum
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

module acasXu-temp-output where

InputVector : Set
InputVector = Tensor ℚ (5 ∷ [])

distanceToIntruder : ∀ {_x0 : Set} {{_x1 : HasNatLits _x0}} → _x0
distanceToIntruder = 0

angleToIntruder : ∀ {_x4 : Set} {{_x5 : HasNatLits _x4}} → _x4
angleToIntruder = 1

intruderHeading : ∀ {_x8 : Set} {{_x9 : HasNatLits _x8}} → _x8
intruderHeading = 2

speed : ∀ {_x12 : Set} {{_x13 : HasNatLits _x12}} → _x12
speed = 3

intruderSpeed : ∀ {_x16 : Set} {{_x17 : HasNatLits _x16}} → _x16
intruderSpeed = 4

OutputVector : Set
OutputVector = Tensor ℚ (5 ∷ [])

clearOfConflict : ∀ {_x20 : Set} {{_x21 : HasNatLits _x20}} → _x20
clearOfConflict = 0

weakLeft : ∀ {_x24 : Set} {{_x25 : HasNatLits _x24}} → _x24
weakLeft = 1

weakRight : ∀ {_x28 : Set} {{_x29 : HasNatLits _x28}} → _x28
weakRight = 2

strongLeft : ∀ {_x32 : Set} {{_x33 : HasNatLits _x32}} → _x32
strongLeft = 3

strongRight : ∀ {_x36 : Set} {{_x37 : HasNatLits _x36}} → _x36
strongRight = 4

postulate acasXu : InputVector → OutputVector

pi : ℚ
pi = ℤ.+ 392699 ℚ./ 125000

Advises : Fin 5 → (InputVector → Set)
Advises i x = ∀ (j : Fin 5) → i ≢ j → acasXu x i ℚ.< acasXu x j

IntruderDistantAndSlower : InputVector → Set
IntruderDistantAndSlower x = x distanceToIntruder ℚ.≥ ℤ.+ 55947691 ℚ./ 1000 × (x speed ℚ.≥ ℤ.+ 1145 ℚ./ 1 × x intruderSpeed ℚ.≤ ℤ.+ 60 ℚ./ 1)

abstract
  property1 : ∀ (x : Tensor ℚ (5 ∷ [])) → IntruderDistantAndSlower x → acasXu x clearOfConflict ℚ.≤ ℤ.+ 1500 ℚ./ 1
  property1 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  property2 : ∀ (x : Tensor ℚ (5 ∷ [])) → IntruderDistantAndSlower x → ∃ λ (j : Fin 5) → acasXu x j ℚ.> acasXu x clearOfConflict
  property2 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

DirectlyAhead : InputVector → Set
DirectlyAhead x = (ℤ.+ 1500 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 1800 ℚ./ 1) × (ℚ.- (ℤ.+ 3 ℚ./ 50) ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ ℤ.+ 3 ℚ./ 50)

MovingTowards : InputVector → Set
MovingTowards x = x intruderHeading ℚ.≥ ℤ.+ 31 ℚ./ 10 × (x speed ℚ.≥ ℤ.+ 980 ℚ./ 1 × x intruderSpeed ℚ.≥ ℤ.+ 960 ℚ./ 1)

abstract
  property3 : ∀ (x : Tensor ℚ (5 ∷ [])) → DirectlyAhead x × MovingTowards x → ¬ Advises clearOfConflict x
  property3 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

MovingAway : InputVector → Set
MovingAway x = x intruderHeading ≡ ℤ.+ 0 ℚ./ 1 × (ℤ.+ 1000 ℚ./ 1 ℚ.≤ x speed × (ℤ.+ 700 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 800 ℚ./ 1))

abstract
  property4 : ∀ (x : Tensor ℚ (5 ∷ [])) → DirectlyAhead x × MovingAway x → ¬ Advises clearOfConflict x
  property4 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

NearAndApproachingFromLeft : InputVector → Set
NearAndApproachingFromLeft x = (ℤ.+ 250 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 400 ℚ./ 1) × ((ℤ.+ 1 ℚ./ 5 ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ ℤ.+ 2 ℚ./ 5) × ((ℚ.- pi ℚ.≤ x intruderHeading × x intruderHeading ℚ.≤ ℚ.- pi ℚ.+ ℤ.+ 1 ℚ./ 200) × ((ℤ.+ 100 ℚ./ 1 ℚ.≤ x speed × x speed ℚ.≤ ℤ.+ 400 ℚ./ 1) × (ℤ.+ 0 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 400 ℚ./ 1))))

abstract
  property5 : ∀ (x : Tensor ℚ (5 ∷ [])) → NearAndApproachingFromLeft x → Advises strongRight x
  property5 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

IntruderFarAway : InputVector → Set
IntruderFarAway x = (ℤ.+ 12000 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 62000 ℚ./ 1) × ((ℚ.- pi ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ ℚ.- (ℤ.+ 7 ℚ./ 10) ⊎ ℤ.+ 7 ℚ./ 10 ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ pi) × ((ℚ.- pi ℚ.≤ x intruderHeading × x intruderHeading ℚ.≤ ℚ.- pi ℚ.+ ℤ.+ 1 ℚ./ 200) × ((ℤ.+ 100 ℚ./ 1 ℚ.≤ x speed × x speed ℚ.≤ ℤ.+ 1200 ℚ./ 1) × (ℤ.+ 0 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 1200 ℚ./ 1))))

abstract
  property6 : ∀ (x : Tensor ℚ (5 ∷ [])) → IntruderFarAway x → Advises clearOfConflict x
  property6 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

LargeVerticalSeparation : InputVector → Set
LargeVerticalSeparation x = (ℤ.+ 0 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 60760 ℚ./ 1) × ((ℚ.- pi ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ pi) × ((ℚ.- pi ℚ.≤ x intruderHeading × x intruderHeading ℚ.≤ pi) × ((ℤ.+ 100 ℚ./ 1 ℚ.≤ x speed × x speed ℚ.≤ ℤ.+ 1200 ℚ./ 1) × (ℤ.+ 0 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 1200 ℚ./ 1))))

abstract
  property7 : ∀ (x : Tensor ℚ (5 ∷ [])) → LargeVerticalSeparation x → ¬ Advises strongLeft x × ¬ Advises strongRight x
  property7 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

LargeVerticalSeparationAndPreviousWeakLeft : InputVector → Set
LargeVerticalSeparationAndPreviousWeakLeft x = (ℤ.+ 0 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 60760 ℚ./ 1) × ((ℚ.- pi ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ ℚ.- (ℤ.+ 3 ℚ./ 4) ℚ.* pi) × ((ℚ.- (ℤ.+ 1 ℚ./ 10) ℚ.≤ x intruderHeading × x intruderHeading ℚ.≤ ℤ.+ 1 ℚ./ 10) × ((ℤ.+ 600 ℚ./ 1 ℚ.≤ x speed × x speed ℚ.≤ ℤ.+ 1200 ℚ./ 1) × (ℤ.+ 600 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 1200 ℚ./ 1))))

abstract
  property8 : ∀ (x : Tensor ℚ (5 ∷ [])) → LargeVerticalSeparationAndPreviousWeakLeft x → Advises clearOfConflict x ⊎ Advises weakLeft x
  property8 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

PreviousWeakRightAndNearbyIntruder : InputVector → Set
PreviousWeakRightAndNearbyIntruder x = (ℤ.+ 2000 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 7000 ℚ./ 1) × ((ℚ.- (ℤ.+ 2 ℚ./ 5) ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ ℚ.- (ℤ.+ 7 ℚ./ 50)) × ((ℚ.- pi ℚ.≤ x intruderHeading × x intruderHeading ℚ.≤ ℚ.- pi ℚ.+ ℤ.+ 1 ℚ./ 100) × ((ℤ.+ 100 ℚ./ 1 ℚ.≤ x speed × x speed ℚ.≤ ℤ.+ 150 ℚ./ 1) × (ℤ.+ 0 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 150 ℚ./ 1))))

abstract
  property9 : ∀ (x : Tensor ℚ (5 ∷ [])) → PreviousWeakRightAndNearbyIntruder x → Advises strongLeft x
  property9 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

IntruderFarAway2 : InputVector → Set
IntruderFarAway2 x = (ℤ.+ 36000 ℚ./ 1 ℚ.≤ x distanceToIntruder × x distanceToIntruder ℚ.≤ ℤ.+ 60760 ℚ./ 1) × ((ℤ.+ 7 ℚ./ 10 ℚ.≤ x angleToIntruder × x angleToIntruder ℚ.≤ pi) × ((ℚ.- pi ℚ.≤ x intruderHeading × x intruderHeading ℚ.≤ ℚ.- pi ℚ.+ ℤ.+ 1 ℚ./ 100) × ((ℤ.+ 900 ℚ./ 1 ℚ.≤ x speed × x speed ℚ.≤ ℤ.+ 1200 ℚ./ 1) × (ℤ.+ 600 ℚ./ 1 ℚ.≤ x intruderSpeed × x intruderSpeed ℚ.≤ ℤ.+ 1200 ℚ./ 1))))

abstract
  property10 : ∀ (x : Tensor ℚ (5 ∷ [])) → IntruderFarAway2 x → Advises clearOfConflict x
  property10 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
------------------------------------------------------------------------------
-- Colist properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Colist.PropertiesI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Colist

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Colist predicate is also a pre-fixed point of the functional
-- ColistF, i.e.
--
-- ColistF Colist ≤ Colist (see FOTC.Data.Colist.Type).
Colist-in :
  ∀ {xs} →
  xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Colist xs') →
  Colist xs
Colist-in h = Colist-coind A h' h
  where
  A : D → Set
  A xs =   xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Colist xs')

  h' : ∀ {xs} → A xs → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs')
  h' (inj₁ xs≡[])                    = inj₁ xs≡[]
  h' (inj₂ (x' , xs' , prf , Clxs')) = inj₂ (x' , xs' , prf , Colist-out Clxs')

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module _ where

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

module M (n : Nat) (m : Nat) where

  foo : n ≡ 0 → Nat
  foo refl = 0
    module M' where
      bar : Nat
      bar = m

  bad : Nat
  bad = M'.bar -- internal error Monad.Signature:882


text:
module OldBasicILP.Syntax.Translation where

open import Common.Context public

import OldBasicILP.Syntax.ClosedHilbertSequential as CHS
import OldBasicILP.Syntax.ClosedHilbert as CH

-- Translation from closed Hilbert-style sequential to closed Hilbert-style.

mutual
  chsᵀ→chᵀ : CHS.Ty → CH.Ty
  chsᵀ→chᵀ (CHS.α P)   = CH.α P
  chsᵀ→chᵀ (A CHS.▻ B) = chsᵀ→chᵀ A CH.▻ chsᵀ→chᵀ B
  chsᵀ→chᵀ (p CHS.⦂ A) = chsᴾ→chᴾ p CH.⦂ chsᵀ→chᵀ A
  chsᵀ→chᵀ (A CHS.∧ B) = chsᵀ→chᵀ A CH.∧ chsᵀ→chᵀ B
  chsᵀ→chᵀ CHS.⊤      = CH.⊤

  chsᴾ→chᴾ : ∀ {Ξ A} → CHS.Proof Ξ A → CH.Proof (chsᵀ→chᵀ A)
  chsᴾ→chᴾ CHS.[ d ] = CH.[ chsᴰ→ch d top ]

  chsᴰ→ch : ∀ {Ξ A} → CHS.⊢ᴰ Ξ → A ∈ Ξ → CH.⊢ (chsᵀ→chᵀ A)
  chsᴰ→ch (CHS.mp i j d) top     = CH.app (chsᴰ→ch d i) (chsᴰ→ch d j)
  chsᴰ→ch (CHS.ci d)     top     = CH.ci
  chsᴰ→ch (CHS.ck d)     top     = CH.ck
  chsᴰ→ch (CHS.cs d)     top     = CH.cs
  chsᴰ→ch (CHS.nec `d d) top     = CH.box (chsᴰ→ch `d top)
  chsᴰ→ch (CHS.cdist {Ξ} {A} {B} {`Ξ₁} {`Ξ₂} {`d₁} {`d₂} d) top = oops {A} {B} {`Ξ₁} {`Ξ₂} {`d₁} {`d₂}
  chsᴰ→ch (CHS.cup d)    top     = CH.cup
  chsᴰ→ch (CHS.cdown d)  top     = CH.cdown
  chsᴰ→ch (CHS.cpair d)  top     = CH.cpair
  chsᴰ→ch (CHS.cfst d)   top     = CH.cfst
  chsᴰ→ch (CHS.csnd d)   top     = CH.csnd
  chsᴰ→ch (CHS.unit d)   top     = CH.unit
  chsᴰ→ch (CHS.mp i j d) (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.ci d)     (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.ck d)     (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cs d)     (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.nec `d d) (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cdist d)  (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cup d)    (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cdown d)  (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cpair d)  (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.cfst d)   (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.csnd d)   (pop k) = chsᴰ→ch d k
  chsᴰ→ch (CHS.unit d)   (pop k) = chsᴰ→ch d k

  -- FIXME: I can’t even postulate this.
  -- postulate
  --   ᴬlem₁ : ∀ {Ξ₁ Ξ₂ A B} {d₁ : CHS.⊢ᴰ Ξ₁ , A CHS.▻ B} {d₂ : CHS.⊢ᴰ Ξ₂ , A}
  --           → chsᴰ→ch (CHS.appᴰ d₁ d₂) ≡ CH.app (chsᴰ→ch d₁ top) (chsᴰ→ch d₂ top)

  postulate
    oops : ∀ {A B Ξ₁ Ξ₂} {d₁ : CHS.⊢ᴰ Ξ₁ , A CHS.▻ B} {d₂ : CHS.⊢ᴰ Ξ₂ , A}
           → CH.⊢ chsᴾ→chᴾ CHS.[ d₁ ] CH.⦂ (chsᵀ→chᵀ A CH.▻ chsᵀ→chᵀ B) CH.▻
                    chsᴾ→chᴾ CHS.[ d₂ ] CH.⦂ chsᵀ→chᵀ A CH.▻
                    chsᴾ→chᴾ CHS.[ CHS.appᴰ d₁ d₂ ] CH.⦂ chsᵀ→chᵀ B

  chs→ch : ∀ {A} → CHS.⊢ A → CH.⊢ (chsᵀ→chᵀ A)
  chs→ch (Ξ , d) = chsᴰ→ch d top

-- Translation from closed Hilbert-style to closed Hilbert-style sequential.

mutual
  chᵀ→chsᵀ : CH.Ty → CHS.Ty
  chᵀ→chsᵀ (CH.α P)   = CHS.α P
  chᵀ→chsᵀ (A CH.▻ B) = chᵀ→chsᵀ A CHS.▻ chᵀ→chsᵀ B
  chᵀ→chsᵀ (p CH.⦂ A) with chᴾ→chsᴾ p
  chᵀ→chsᵀ (p CH.⦂ A) | (Ξ , p′) = p′ CHS.⦂ chᵀ→chsᵀ A
  chᵀ→chsᵀ (A CH.∧ B) = chᵀ→chsᵀ A CHS.∧ chᵀ→chsᵀ B
  chᵀ→chsᵀ CH.⊤      = CHS.⊤

  chᴾ→chsᴾ : ∀ {A} → CH.Proof A → ∃ (λ Ξ → CHS.Proof Ξ (chᵀ→chsᵀ A))
  chᴾ→chsᴾ CH.[ d ] with ch→chs d
  chᴾ→chsᴾ CH.[ d ] | (Ξ , d′) = Ξ , CHS.[ d′ ]

  ch→chs : ∀ {A} → CH.⊢ A → CHS.⊢ (chᵀ→chsᵀ A)
  ch→chs (CH.app d₁ d₂) = CHS.app (ch→chs d₁) (ch→chs d₂)
  ch→chs CH.ci          = ∅ , CHS.ci CHS.nil
  ch→chs CH.ck          = ∅ , CHS.ck CHS.nil
  ch→chs CH.cs          = ∅ , CHS.cs CHS.nil
  ch→chs (CH.box d)     = CHS.box (ch→chs d)
  ch→chs CH.cdist       = ∅ , CHS.cdist CHS.nil
  ch→chs CH.cup         = ∅ , CHS.cup CHS.nil
  ch→chs CH.cdown       = ∅ , CHS.cdown CHS.nil
  ch→chs CH.cpair       = ∅ , CHS.cpair CHS.nil
  ch→chs CH.cfst        = ∅ , CHS.cfst CHS.nil
  ch→chs CH.csnd        = ∅ , CHS.csnd CHS.nil
  ch→chs CH.unit        = ∅ , CHS.unit CHS.nil

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- No top-level module

f : Set₁
f = Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.Setoid directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.Vec.Relation.Equality.Setoid
  {a ℓ} (S : Setoid a ℓ) where

open import Data.Vec.Relation.Binary.Equality.Setoid S public


text:
useful-lemma : ∀ {a} {A : Set a} → A
useful-lemma = useful-lemma


text:
------------------------------------------------------------------------
-- Very stable booleans
------------------------------------------------------------------------

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

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the very stable booleans uses path
-- equality, but the supplied notion of equality is used for other
-- things.

import Equality.Path as P

module Bool.Very-stable
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

import Equality.Path.Univalence as PU
open import Prelude as Bool hiding (true; false)

open import Bijection equality-with-J using (_↔_)
import Bijection P.equality-with-J as PB
open import Equality.Decision-procedures equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Erased.Cubical eq as Erased
import Erased.Cubical P.equality-with-paths as PE
open import Function-universe equality-with-J hiding (_∘_)
open import Injection equality-with-J using (Injective)

private
  variable
    a p          : Level
    A            : Type a
    P            : A → Type p
    b f r r-[] t : A

------------------------------------------------------------------------
-- Very stable booleans

-- Very stable booleans.
--
-- This type uses a construction due to Thierry Coquand and Fabian
-- Ruch. I think this construction is a variant of a construction due
-- to Rijke, Shulman and Spitters (see "Modalities in Homotopy Type
-- Theory").

data B̃ool : Type where
  true false : B̃ool
  stable     : Erased B̃ool → B̃ool
  stable-[]ᴾ : (b : B̃ool) → stable [ b ] P.≡ b

-- The constructor stable is a left inverse of [_].

stable-[] : (b : B̃ool) → stable [ b ] ≡ b
stable-[] = _↔_.from ≡↔≡ ∘ stable-[]ᴾ

-- B̃ool is very stable.

Very-stable-B̃ool : Very-stable B̃ool
Very-stable-B̃ool = Stable→Left-inverse→Very-stable stable stable-[]

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

elimᴾ :
  (P : B̃ool → Type p) →
  P true →
  P false →
  (r : ∀ b → Erased (P (erased b)) → P (stable b)) →
  (∀ b (p : P b) →
   P.[ (λ i → P (stable-[]ᴾ b i)) ] r [ b ] [ p ] ≡ p) →
  ∀ b → P b
elimᴾ P t f r r-[] = λ where
  true             → t
  false            → f
  (stable b)       → r b [ elimᴾ P t f r r-[] (erased b) ]
  (stable-[]ᴾ b i) → r-[] b (elimᴾ P t f r r-[] b) i

-- A non-dependent eliminator, expressed using paths.

recᴾ :
  A → A →
  (r : Erased B̃ool → Erased A → A) →
  (∀ b p → r [ b ] [ p ] P.≡ p) →
  B̃ool → A
recᴾ = elimᴾ _

-- A dependent eliminator, expressed using equality.

elim :
  (P : B̃ool → Type p) →
  P true →
  P false →
  (r : ∀ b → Erased (P (erased b)) → P (stable b)) →
  (∀ b (p : P b) → subst P (stable-[] b) (r [ b ] [ p ]) ≡ p) →
  ∀ b → P b
elim P t f r r-[] = elimᴾ P t f r (λ b p → subst≡→[]≡ (r-[] b p))

-- A "computation" rule.

elim-stable-[] :
  dcong (elim P t f r r-[]) (stable-[] b) ≡
  r-[] b (elim P t f r r-[] b)
elim-stable-[] = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator, expressed using equality.

rec :
  A → A →
  (r : Erased B̃ool → Erased A → A) →
  (∀ b p → r [ b ] [ p ] ≡ p) →
  B̃ool → A
rec t f r r-[] = recᴾ t f r (λ b p → _↔_.to ≡↔≡ (r-[] b p))

-- A "computation" rule.

rec-stable-[] :
  cong (rec t f r r-[]) (stable-[] b) ≡
  r-[] b (rec t f r r-[] b)
rec-stable-[] = cong-≡↔≡ (refl _)

-- A dependent eliminator that can be used when eliminating into very
-- stable type families.

elim-Very-stable :
  (P : B̃ool → Type p) →
  P true →
  P false →
  (∀ b → Very-stable (P b)) →
  ∀ b → P b
elim-Very-stable P t f s =
  elim P t f
    (λ b →
       Erased (P (erased b))  ↝⟨ Erased.map (subst P (

           erased b                ≡⟨ sym $ stable-[] (erased b) ⟩∎
           stable b                ∎)) ⟩

       Erased (P (stable b))  ↝⟨ Very-stable→Stable 0 (s (stable b)) ⟩□

       P (stable b)           □)
    (λ b p →
       Very-stable→Stable 1 (Very-stable→Very-stable-≡ 0 (s b)) _ _
         [ subst P (stable-[] b)
             (_≃_.from Eq.⟨ _ , s (stable [ b ]) ⟩
                [ subst P (sym $ stable-[] b) p ])                ≡⟨ cong (subst P (stable-[] b)) $ sym $
                                                                     _≃_.left-inverse-unique Eq.⟨ _ , s (stable [ b ]) ⟩ erased refl _ ⟩
           subst P (stable-[] b)
             (erased [ subst P (sym $ stable-[] b) p ])           ≡⟨⟩

           subst P (stable-[] b) (subst P (sym $ stable-[] b) p)  ≡⟨ subst-subst-sym _ _ _ ⟩∎

           p                                                      ∎
         ])

-- A non-dependent eliminator that can be used when eliminating into
-- very stable type families.

rec-Very-stable : A → A → Very-stable A → B̃ool → A
rec-Very-stable t f s = elim-Very-stable _ t f (λ _ → s)

------------------------------------------------------------------------
-- Some properties

private
 module Dummy where

  -- A function mapping very stable booleans to types: true is mapped
  -- to the unit type and false to the empty type.

  private

    T̃′ : B̃ool → Σ Type Very-stable
    T̃′ = rec-Very-stable
      (⊤ , Very-stable-⊤)
      (⊥ , Very-stable-⊥)
      (Very-stable-∃-Very-stable ext univ)

  T̃ : B̃ool → Type
  T̃ = proj₁ ∘ T̃′

  -- Some computation rules that hold by definition.

  _ : T̃ true ≡ ⊤
  _ = refl _

  _ : T̃ false ≡ ⊥
  _ = refl _

  -- The output of T̃ is very stable.

  Very-stable-T̃ : ∀ b → Very-stable (T̃ b)
  Very-stable-T̃ = proj₂ ∘ T̃′

  -- The values true and false are not equal.

  true≢false : true ≢ false
  true≢false =
    true ≡ false      ↝⟨ cong T̃ ⟩
    T̃ true ≡ T̃ false  ↔⟨⟩
    ⊤ ≡ ⊥             ↝⟨ (λ eq → ≡⇒↝ _ eq _) ⟩□
    ⊥                 □

module Alternative-T̃ where

  -- A direct implementation of T̃.

  private

    T̃′ : B̃ool → Σ Type PE.Very-stable

  T̃ : B̃ool → Type
  T̃ b = proj₁ (T̃′ b)

  Very-stable-T̃ : ∀ b → PE.Very-stable (T̃ b)
  Very-stable-T̃ b = proj₂ (T̃′ b)

  T̃′ true             = ⊤ , PE.Very-stable-⊤
  T̃′ false            = ⊥ , PE.Very-stable-⊥
  T̃′ (stable [ b ])   = PE.Erased (T̃ b) , PE.Very-stable-Erased
  T̃′ (stable-[]ᴾ b i) = lemma₁ i , lemma₂ i
    where
    lemma₁ : PE.Erased (T̃ b) P.≡ T̃ b
    lemma₁ = PU.≃⇒≡ (PE.Very-stable→Stable 0 (Very-stable-T̃ b))

    lemma₂ :
      P.[ (λ i → PE.Very-stable (lemma₁ i)) ]
        PE.Very-stable-Erased ≡ Very-stable-T̃ b
    lemma₂ =
      P.heterogeneous-irrelevance₀
        (PE.Very-stable-propositional P.ext)

  -- Some computation rules that hold by definition.

  _ : T̃ true ≡ ⊤
  _ = refl _

  _ : T̃ false ≡ ⊥
  _ = refl _

  _ : T̃ (stable [ b ]) ≡ PE.Erased (T̃ b)
  _ = refl _

open Dummy public

-- A function from booleans to very stable booleans.

from-Bool : Bool → B̃ool
from-Bool = if_then true else false

-- The function from-Bool is injective.
--
-- This lemma was suggested by Mike Shulman.

from-Bool-injective : Injective from-Bool
from-Bool-injective {x = Bool.true}  {y = Bool.true}  = λ _ → refl _
from-Bool-injective {x = Bool.true}  {y = Bool.false} = ⊥-elim ∘ true≢false
from-Bool-injective {x = Bool.false} {y = Bool.true}  = ⊥-elim ∘ true≢false ∘ sym
from-Bool-injective {x = Bool.false} {y = Bool.false} = λ _ → refl _

-- B̃ool is equivalent to Erased Bool.
--
-- This lemma was suggested by Mike Shulman.

B̃ool≃Erased-Bool : B̃ool ≃ Erased Bool
B̃ool≃Erased-Bool = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = λ b →
        Very-stable→Stable 0
          (Very-stable→Very-stable-≡ 0 Very-stable-Erased _ _)
          [ to (from b)                           ≡⟨⟩
            to (stable [ from-Bool (erased b) ])  ≡⟨ cong to (stable-[] _) ⟩
            to (from-Bool (erased b))             ≡⟨ lemma (erased b) ⟩
            [ erased b ]                          ≡⟨⟩
            b                                     ∎
          ]
    }
  ; left-inverse-of = elim-Very-stable
      _
      (stable-[] true)
      (stable-[] false)
      (λ _ → Very-stable→Very-stable-≡ 0 Very-stable-B̃ool _ _)
  })
  where
  to = rec-Very-stable [ Bool.true ] [ Bool.false ] Very-stable-Erased

  from = stable ∘ Erased.map from-Bool

  lemma : ∀ b → to (from-Bool b) ≡ [ b ]
  lemma Bool.true  = refl _
  lemma Bool.false = refl _

------------------------------------------------------------------------
-- An example

private

  -- At the time of writing it is unclear if there is a reasonable way
  -- to compile very stable booleans. The constructors true and false
  -- are distinct, and it is reasonable to think that a compiler will
  -- compile them in different ways. Now consider the following two
  -- very stable booleans:

  b₁ : B̃ool
  b₁ = stable [ true ]

  b₂ : B̃ool
  b₂ = stable [ false ]

  -- The first one is equal to true, and the second one is equal to
  -- false:

  _ : b₁ ≡ true
  _ = stable-[] true

  _ : b₂ ≡ false
  _ = stable-[] false

  -- However, unlike the constructors true and false, b₁ and b₂ should
  -- be compiled in the same way, because the argument to [_] is
  -- erased.

  -- One question, raised by Andrea Vezzosi, is whether it is possible
  -- to write a program that gives /observably/ different results
  -- (after erasure) for true and false. If this is the case, then the
  -- erasure mechanism is not well-behaved.


text:
import Nat
open   Nat using (Nat)

module TopLevelImport (n : Nat) where

  it : Nat
  it = n


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Equiv.Reasoning where

open import Cubical.Foundations.Prelude using (refl; sym)

open import Cubical.Relation.Binary

-- Properties of equivalence

≃-reflexive : Reflexive _≃_
≃-reflexive = ?