text:
module LocalChoice where

open import IO using (run; putStrLn; mapM′; _>>_)
open import Coinduction using (♯_)
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺ using (ℕ⁺; suc)
open import Data.String using (String)
open import Data.List using (List; []; _∷_; map)
open import Data.Colist using (fromList)
open import Function using (_$_; _∘_)

open import Data.Environment
open import nodcap.Base
open import nodcap.Typing
open import nodcap.LocalChoice
open import nodcap.Norm
open import nodcap.Show renaming (showTerm to show)
open import nodcap.NF.Show renaming (showTerm to showNF)

Bit : Type
Bit = 𝟏 ⊕ 𝟏

bit₁ bit₂ : ⊢ Bit ∷ []
bit₁ = sel₁ halt
bit₂ = sel₂ halt

randomBit : ⊢ Bit ∷ []
randomBit = bit₁ or bit₂

main = run (mapM′ putStrLn (fromList strs))
  where
    strs = "Process:"
         ∷ show randomBit
         ∷ "Result:"
         ∷ map showNF (nfND randomBit)

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

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
module SN where

open import Library
open import Syntax
open import RenamingAndSubstitution

-- Reduction

data _↦_ {Γ} : ∀{a} (t t' : Tm Γ a) → Set where
  β    : ∀{a b} {t : Tm (Γ , a) b} {u} → app (abs t) u ↦ sub0 t u
  abs  : ∀{a b} {t t' : Tm (Γ , a) b} (r : t ↦ t') → abs t ↦ abs t'
  appl : ∀{a b} {t t' : Tm Γ (a ⇒ b)} {u} (r : t ↦ t') → app t u ↦ app t' u
  appr : ∀{a b} {t : Tm Γ (a ⇒ b)} {u u'} (r : u ↦ u') → app t u ↦ app t u'

ren↦ : ∀{Γ Δ a} (ρ : Ren Γ Δ) {t t' : Tm Δ a} (r : t ↦ t') → ren ρ t ↦ ren ρ t'
-- ren↦ {Γ} {Δ} {a} ρ {t} {t'} r = {!r!}
ren↦ {Γ} {Δ} ρ β = {!!}
ren↦ {Γ} {Δ} ρ (abs r) = abs (ren↦ (liftr ρ) r)
ren↦ {Γ} {Δ} ρ (appl r) = {!!}
ren↦ {Γ} {Δ} ρ (appr r) = {!!}

ren↦inv : ∀{Γ Δ a} (ρ : Ren Γ Δ) (t : Tm Δ a) {t' : Tm Γ a} (r : ren ρ t ↦ t') →
  ∃ λ (u : Tm Δ a) → (t ↦ u) × (t' ≡ ren ρ u)
ren↦inv ρ (var x) ()
ren↦inv ρ (app (abs t) t₁) β = sub0 t t₁ , β , {!refl!}
ren↦inv ρ (abs t) (abs r) with ren↦inv (liftr ρ) t r
ren↦inv ρ (abs t) (abs r) | u , r' , e = abs u , abs r' , cong abs e
ren↦inv ρ (app t t₁) (appl r) with ren↦inv ρ t r
ren↦inv ρ (app t t₁) (appl r) | u , r' , refl = app u t₁ , appl r' , refl
ren↦inv ρ (app t t₁) (appr r) with ren↦inv ρ t₁ r
... | u , r' , refl = app t u , appr r' , refl

-- Strongly normalizing terms

data SN {Γ : Cxt} {a : Ty} (t : Tm Γ a) : Set where
  sn : (∀ t' (r : t ↦ t') → SN t') → SN t

-- SN is closed under renaming

renSN : ∀{Γ Δ a} (ρ : Ren Γ Δ) {t : Tm Δ a} (s : SN t) → SN (ren ρ t)
renSN ρ (sn f) = sn λ _ r → case ren↦inv ρ _ r of
  λ{ (t'' , r' , refl) → renSN ρ (f t'' r') }

-- Strong head reduction (weak head reduction that preserves SN under expansion)

data _s↦_ {Γ} : ∀{a} (t t' : Tm Γ a) → Set where
  β    : ∀{a b} {t : Tm (Γ , a) b} {u} (s : SN u) → app (abs t) u s↦ sub0 t u
  appl : ∀{a b} {t t' : Tm Γ (a ⇒ b)} {u} (r : t s↦ t') → app t u s↦ app t' u

-- Strong head reduction is closed under renaming

rens↦ : ∀{Γ Δ a} (ρ : Ren Γ Δ) {t t' : Tm Δ a} (r : t s↦ t') → ren ρ t s↦ ren ρ t'
rens↦ ρ (β s) = {!β!}
  -- Need lemma:
  --   app (abs (ren (liftr ρ) .t)) (ren ρ .u) s↦
  --     ren ρ (sub (subId , .u) .t)rens↦ ρ (appl r) = appl (rens↦ ρ r)

-- SN is closed under strong head expansion

s↦SN : ∀{Γ a}{t t' : Tm Γ a} (r : t s↦ t') (s : SN t') → SN t
-- s↦SN r s = sn λ t' → λ{ β → {!!} ; (abs r') → {!!} ; (appl r') → {!!} ; (appr r') → {!!}}
s↦SN (β s')   s = sn (λ t' → λ{ β → s ; (appl (abs r)) → {!!} ; (appr r) → {!!}})
s↦SN (appl r) s = {!!}

-- Reducibility: Kripke logical predicate

Red : (a : Ty) {Γ : Cxt} (t : Tm Γ a) → Set
Red ★       {Γ} t = SN t
Red (a ⇒ b) {Γ} t = ∀{Γ'}(ρ : Ren Γ' Γ) u (s : Red a u) → Red b (app (ren ρ t) u)

-- Reducibility is closed under renaming

renRed : ∀{Γ Δ a} (ρ : Ren Γ Δ) {t : Tm Δ a} (p : Red a t) → Red a (ren ρ t)
renRed {Γ} {Δ} {★}     ρ {t} p = renSN ρ p
renRed {Γ} {Δ} {a ⇒ b} ρ {t} p = λ ρ₁ u s →
  subst (λ z → Red b (app z u)) (rencomp ρ₁ ρ t)
    (p (renComp ρ₁ ρ) u s)

-- Reducibility is closed under strong head expansion

expRed : ∀{Γ a} {t t' : Tm Γ a} (r : t s↦ t') (p : Red a t') → Red a t
expRed {Γ} {★}     {t} {t'} r p       = s↦SN r p
expRed {Γ} {a ⇒ b} {t} {t'} r p ρ u s = expRed (appl {!!}) (p ρ u s)

ext: agda

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
{-# OPTIONS --two-level --cubical-compatible #-}

open import Agda.Primitive

data D₁ : SSet → SSet (lsuc lzero) where
  c : (@0 A : SSet) → A → D₁ A

data D₂ : Set → SSet (lsuc lzero) where
  c : (@0 A : Set) → A → D₂ A


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import Haskell.Modules.RWS.RustAnyHow
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-0 as ECP-LBFT-OBM-Diff-0
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Storage.DiemDB.DiemDB                     as DiemDB
import      LibraBFT.Impl.Types.EpochChangeProof                    as EpochChangeProof
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                            using (String)

module LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-1 where

------------------------------------------------------------------------------

postulate -- TODO-1 : nub (remove duplicates)
  nub : ∀ {A : Set} → List A → List A

------------------------------------------------------------------------------

amIMemberOfCurrentEpoch : Author → List Author → Bool
amIMemberOfCurrentEpochM : LBFT Bool

------------------------------------------------------------------------------

e_SyncManager_insertQuorumCertM_commit : LedgerInfoWithSignatures → LBFT (Either ErrLog Unit)
e_SyncManager_insertQuorumCertM_commit liws =
  ifD (not ECP-LBFT-OBM-Diff-0.enabled)
  then (do
    rcvrs ← use (lRoundManager ∙ rmObmAllAuthors)
    --act (BroadcastEpochChangeProof (EpochChangeProof∙new (liws ∷ []) false) rcvrs) -- TODO-1
    ok unit)
  else do
    {-
    LBFT-OBM-DIFF
    A SyncInfo is sent BEFORE an EpochChangeProof.
    Only sent to members of current epoch (not the one the EpochChangeProof will transition to).

    This is needed since the highest committed QC from the initial committer/leader of
    the EPOCHCHANGE transaction needs to be given to followers so they will also
    commit the EPOCHCHANGE transaction.

    Note: This is similar to how the QC is carried in a ProposalMsg.
    -}
    rcvrs    ← use (lRoundManager ∙ rmObmAllAuthors)
    syncInfo ← SyncInfo∙new <$> use (lBlockStore ∙ bsHighestQuorumCert)
                            <*> use (lBlockStore ∙ bsHighestCommitCert)
                            <*> use (lBlockStore ∙ bsHighestTimeoutCert)
    act (BroadcastSyncInfo syncInfo rcvrs)

    -- LBFT-OBM-DIFF : PUSH: when sending an ECP when committing an epoch change,
    -- send all epoch ending ledger info (not just the current one)
    -- so the receiver will be up-to-date.
    -- TODO : optimize: let receiver PULL its gaps.
    db ← use (lBlockStore ∙ bsStorage ∙ msObmDiemDB)
    maybeSD (liws ^∙ liwsLedgerInfo ∙ liNextEpochState) (bail fakeErr {-"liNextEpochState" ∷ "Nothing" ∷ []-}) $ λ es → do
      let newRcvrs = es ^∙ esVerifier ∙ vvObmAuthors
          allRcvrs = nub (rcvrs ++ newRcvrs)
      eitherS (DiemDB.getEpochEndingLedgerInfos db ({-Epoch-} 1) (liws ^∙ liwsEpoch + 1))
              bail
              (λ (liwss , b) -> do
                  -- act (BroadcastEpochChangeProof lEC (EpochChangeProof.new liwss b) allRcvrs) -- TODO-1
                  ok unit)
 where
  here' : List String → List String
  here' t = "e_SyncManager_InsertQuorumCertM_commit" ∷ t

------------------------------------------------------------------------------

e_RoundState_processLocalTimeoutM : Epoch → Round → LBFT Bool
e_RoundState_processLocalTimeoutM e r =
  ifD not ECP-LBFT-OBM-Diff-0.enabled
  then yes'
  else
    -- LBFT-OBM-DIFF : do not broadcast timeouts if not member of epoch
    ifMD amIMemberOfCurrentEpochM
         yes'
         (do
           logInfo fakeInfo -- ["not a member of Epoch", "ignoring timeout", lsE e, lsR r]
           pure false)
 where
  yes' : LBFT Bool
  yes' = do
    logInfo fakeInfo -- InfoRoundTimeout e r
    pure true

------------------------------------------------------------------------------
-- TODO-1 : use EitherD
e_EpochManager_doECP_waitForRlec : EpochManager → EpochChangeProof → Either ErrLog Bool
e_EpochManager_doECP_waitForRlec self ecp =
  if not ECP-LBFT-OBM-Diff-0.enabled
  then pure true
  else do
    rm ← self ^∙ emObmRoundManager
    e  ← self ^∙ emEpoch
    maybeS (rm ^∙ rmObmMe)
           (Left fakeErr {-["e_EpochManager_doECP_waitForRlec", "rmObmMe", "Nothing"]-})
           $ λ me → let m = amIMemberOfCurrentEpoch me (rm ^∙ rmObmAllAuthors)
                     in pure (m ∧ (EpochChangeProof.obmLastEpoch ecp == e))

------------------------------------------------------------------------------

module e_EpochManager_startNewEpoch where
  VariantFor : ∀ {ℓ} EL → EL-func {ℓ} EL
  VariantFor EL =
    EpochManager → EpochChangeProof
    → EL ErrLog EpochManager

  step₀ : VariantFor EitherD
  step₀ self ecp =
    ifD not ECP-LBFT-OBM-Diff-0.enabled
    then pure self
    else do
      -- LBFT-OBM-DIFF: store all the epoch ending LedgerInfos sent in ECP
      -- (to avoid gaps -- from when a node is not a member).
      db ← (foldM) (\db l → DiemDB.saveTransactions db (just l))
                    (self ^∙ emStorage ∙ msObmDiemDB)
                    (ecp ^∙ ecpLedgerInfoWithSigs)
      pure (self & emStorage ∙ msObmDiemDB ∙~ db)

e_EpochManager_startNewEpoch      : e_EpochManager_startNewEpoch.VariantFor Either
e_EpochManager_startNewEpoch em   = toEither ∘ e_EpochManager_startNewEpoch.step₀ em

e_EpochManager_startNewEpoch-D    : e_EpochManager_startNewEpoch.VariantFor EitherD
e_EpochManager_startNewEpoch-D em = fromEither ∘ e_EpochManager_startNewEpoch em

------------------------------------------------------------------------------
-- TODO-1 : use EitherD
e_EpochManager_checkEpc : EpochManager → EpochChangeProof → Either ErrLog Unit
e_EpochManager_checkEpc self ecp =
  if (not ECP-LBFT-OBM-Diff-0.enabled)
  then checkEpcNot
  else checkEpcEnable
 where
  here' : List String → List String

  checkEpcNot : Either ErrLog Unit
  checkEpcNot = case EpochChangeProof.epoch ecp of λ where
    (Left e) → Left (withErrCtx (here' []) e)
    (Right msgEpoch) → do
      e ← self ^∙ emEpoch
      if msgEpoch == e
        then pure unit
        else Left fakeErr
              --(ErrInfo (lEC, InfoL (here ["unexpected epoch proof", lsE msgEpoch, lsE e])))

  -- LBFT-OBM-DIFF : ignore it if it doesn't help
  checkEpcEnable : Either ErrLog Unit
  checkEpcEnable = do
    epoch ← self ^∙ emEpoch
    if-dec (EpochChangeProof.obmLastEpoch ecp <? epoch)
      then Left fakeErr
          --(ErrInfo (lEC, InfoL (here [ "ecp last", lsE (EpochChangeProof.obmLastEpoch ecp)
          --                           , "< ours"  , lsE epoch ])))
      else pure unit

  here' t = "e_EpochManager_checkEpc" ∷ t

------------------------------------------------------------------------------
-- TODO-1 : use EitherD
e_EpochManager_processMessage_ISyncInfo : EpochManager → SyncInfo → Either ErrLog Unit
e_EpochManager_processMessage_ISyncInfo self si = do
  e ← self ^∙ emEpoch
  grd‖ not ECP-LBFT-OBM-Diff-0.enabled ≔ pure unit
     ‖ si ^∙ siEpoch == e              ≔ pure unit
     ‖ otherwise≔
       Left fakeErr
             -- ["si epoch", lsE (si^.siEpoch), "/=", "ours", lsE e]

------------------------------------------------------------------------------

amIMemberOfCurrentEpochM =
  use (lRoundManager ∙ rmObmMe) >>= λ where
    nothing → do
      logErr fakeErr -- no identity
      pure false
    (just me) →
      amIMemberOfCurrentEpoch <$> pure me <*> use (lRoundManager ∙ rmObmAllAuthors)

amIMemberOfCurrentEpoch = elem


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Sum.Base where

open import Cubical.Relation.Nullary

open import Cubical.Core.Everything

private
  variable
    ℓ ℓ' : Level
    A B C D : Type ℓ

data _⊎_ (A : Type ℓ)(B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

rec : {C : Type ℓ} → (A → C) → (B → C) → A ⊎ B → C
rec f _ (inl x) = f x
rec _ g (inr y) = g y

elim : {C : A ⊎ B → Type ℓ} →  ((a : A) → C (inl a)) → ((b : B) → C (inr b))
       → (x : A ⊎ B) → C x
elim f _ (inl x) = f x
elim _ g (inr y) = g y

map : (A → C) → (B → D) → A ⊎ B → C ⊎ D
map f _ (inl x) = inl (f x)
map _ g (inr y) = inr (g y)

_⊎?_ : {P Q : Type ℓ} → Dec P → Dec Q → Dec (P ⊎ Q)
P? ⊎? Q? with P? | Q?
... | yes p | _ = yes (inl p)
... | no _  | yes q = yes (inr q)
... | no ¬p | no ¬q  = no λ
  { (inl p) → ¬p p
  ; (inr q) → ¬q q
  }

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:
-- Generated by src/templates/TemplatesCompiler
module templates where
open import cedille-types
{-# FOREIGN GHC import qualified Templates #-}

-- src/templates/Mendler.ced
postulate
  templateMendler : start
{-# COMPILE GHC templateMendler = Templates.templateMendler #-}

-- src/templates/MendlerSimple.ced
postulate
  templateMendlerSimple : start
{-# COMPILE GHC templateMendlerSimple = Templates.templateMendlerSimple #-}

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


text:
module Relation.Ternary.Separation.Monad.Reader where

open import Level
open import Function using (_∘_; case_of_)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (PT)
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Allstar

open import Data.Product
open import Data.List hiding (concat; lookup)
open import Data.Unit

private
  variable
    ℓv : Level
    A  : Set ℓv
    Γ Γ₁ Γ₂ Γ₃ : List A

{- Something not unlike a indexed relative monad transformer in a bicartesian closed category -}
module ReaderTransformer {ℓ}
  -- types
  {T : Set ℓ}
  -- runtime resource
  {C : Set ℓ} {{rc : RawSep C}} {u} {{sc : IsUnitalSep rc u}} {{cc : IsConcattative rc}}
  --
  {B : Set ℓ} {{rb : RawSep B}}
  (j : Morphism C B) {{sb : IsUnitalSep rb (Morphism.j j u)}}
  (V : T → Pred C ℓ) -- values
  (M : PT C B ℓ ℓ)
  {{monad : Monads.Monad {{jm = j}} ⊤ ℓ (λ _ _ → M) }}
  where

  open Morphism j hiding (j) public
  open Monads {{jm = j}} using (Monad; str; typed-str)
  open import Relation.Ternary.Separation.Construct.List T

  module _ where
    open Monad monad

    variable
      P Q R : Pred C ℓ

    Reader : ∀ (Γ₁ Γ₂ : List T) (P : Pred C ℓ) → Pred B ℓ
    Reader Γ₁ Γ₂ P = J (Allstar V Γ₁) ─✴ M (P ✴ Allstar V Γ₂)

    instance
      reader-monad : Monad (List T) _ Reader
      app (Monad.return reader-monad px) (inj e) s = return px &⟨ s ⟩ e
      app (app (Monad.bind reader-monad f) mp σ₁) env σ₂ =
        let _ , σ₃ , σ₄ = ⊎-assoc σ₁ σ₂ in
        app (bind (wand λ where
          (px ×⟨ σ₅ ⟩ env') σ₆ →
            let _ , τ₁ , τ₂ = ⊎-unassoc σ₆ (j-⊎ σ₅) in
            app (app f px τ₁) (inj env') τ₂)) (app mp env σ₄) σ₃

    frame : Γ₁ ⊎ Γ₃ ≣ Γ₂ → ∀[ Reader Γ₁ ε P ⇒ Reader Γ₂ Γ₃ P ]
    app (frame sep c) (inj env) σ = do
      let E₁ ×⟨ σ₁ ⟩ E₂ = repartition sep env
      let Φ , σ₂ , σ₃   = ⊎-unassoc σ (j-⊎ σ₁)
      (v ×⟨ σ₄ ⟩ nil) ×⟨ σ₅ ⟩ E₃ ← app c (inj E₁) σ₂ &⟨ Allstar _ _ ∥ σ₃ ⟩ E₂
      case ⊎-id⁻ʳ σ₄ of λ where
        refl → return (v ×⟨ σ₅ ⟩ E₃)

    ask : ε[ Reader Γ ε (Allstar V Γ) ]
    app ask (inj env) σ with ⊎-id⁻ˡ σ
    ... | refl = return (env ×⟨ ⊎-idʳ ⟩ nil)

    prepend : ∀[ Allstar V Γ₁ ⇒ⱼ Reader Γ₂ (Γ₁ ∙ Γ₂) Emp ]
    app (prepend env₁) (inj env₂) s with j-⊎⁻ s
    ... | _ , refl , s' = return (empty ×⟨ ⊎-idˡ ⟩ (concat (env₁ ×⟨ s' ⟩ env₂)))

    append : ∀[ Allstar V Γ₁ ⇒ⱼ Reader Γ₂ (Γ₂ ∙ Γ₁) Emp ]
    app (append env₁) (inj env₂) s with j-⊎⁻ s
    ... | _ , refl , s' = return (empty ×⟨ ⊎-idˡ ⟩ (concat (✴-swap (env₁ ×⟨ s' ⟩ env₂))))

    liftM : ∀[ M P ⇒ Reader Γ Γ P ]
    app (liftM mp) (inj env) σ = do
      mp &⟨ σ ⟩ env

    runReader : ∀[ Allstar V Γ ⇒ⱼ Reader Γ ε P ─✴ M P ]
    app (runReader env) mp σ = do
      px ×⟨ σ ⟩ nil ← app mp (inj env) (⊎-comm σ)
      case ⊎-id⁻ʳ σ of λ where
        refl → return px

  module _ where
    open Monad reader-monad

    lookup : ∀ {a} → ε[ Reader [ a ] [] (V a) ]
    lookup = do
      v :⟨ σ ⟩: nil ← ask
      case ⊎-id⁻ʳ σ of λ where
        refl → return v

module ReaderMonad {ℓ}
  -- types
  {T : Set ℓ}
  -- runtime resource
  {C : Set ℓ} {{rc : RawSep C}} {u} {{sc : IsUnitalSep rc u}} {{cc : IsConcattative rc}}
  -- values
  (V : T → Pred C ℓ)
  where

  open import Relation.Ternary.Separation.Monad.Identity
  open ReaderTransformer id-morph V Identity.Id {{ monad = Identity.id-monad }} public


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

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym; cong)
open import Relation.Nullary using (_because_; ofʸ; ofⁿ)

open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat.Base
open import Data.Bool.Base using (false; true)
open import Data.Product using (_×_; _,_; ∃-syntax)

import Data.Fin as Fin
import Data.Nat.Properties as ℕₚ
import Data.Fin.Properties as Finₚ

open Fin using (Fin ; zero ; suc; #_)

open import PiCalculus.Syntax
open Scoped

module PiCalculus.Semantics where

  private
    variable
      name namex namey : Name
      n : ℕ
      P P' Q R : Scoped n
      x y : Fin n

  Unused : ∀ {n} → Fin n → Scoped n → Set
  Unused i 𝟘 = ⊤
  Unused i (ν P) = Unused (suc i) P
  Unused i (P ∥ Q) = Unused i P × Unused i Q
  Unused i (x ⦅⦆ P) = i ≢ x × Unused (suc i) P
  Unused i (x ⟨ y ⟩ P) = i ≢ x × i ≢ y × Unused i P

  lift : (i : Fin (suc n)) → Scoped n → Scoped (suc n)
  lift i 𝟘 = 𝟘
  lift i (ν P) = ν (lift (suc i) P)
  lift i (P ∥ Q) = lift i P ∥ lift i Q
  lift i (x ⦅⦆ P) = Fin.punchIn i x ⦅⦆ lift (suc i) P
  lift i (x ⟨ y ⟩ P) = Fin.punchIn i x ⟨ Fin.punchIn i y ⟩ lift i P

  lower : (i : Fin (suc n)) (P : Scoped (suc n)) → Unused i P → Scoped n
  lower i 𝟘 uP = 𝟘
  lower i (ν P) uP = ν (lower (suc i) P uP)
  lower i (P ∥ Q) (uP , uQ) = lower i P uP ∥ lower i Q uQ
  lower i (x ⦅⦆ P) (i≢x , uP) = Fin.punchOut i≢x ⦅⦆ lower (suc i) P uP
  lower i (x ⟨ y ⟩ P) (i≢x , (i≢y , uP)) = Fin.punchOut i≢x ⟨ Fin.punchOut i≢y ⟩ lower i P uP

  notMax : (i : Fin n) (x : Fin (suc n)) → Fin.inject₁ i ≡ x → n ≢ Fin.toℕ x
  notMax i x p n≡x = Finₚ.toℕ-inject₁-≢ i (trans n≡x (sym (cong Fin.toℕ p)))

  exchangeFin : Fin n → Fin (suc n) → Fin (suc n)
  exchangeFin i x with Fin.inject₁ i Fin.≟ x
  exchangeFin i x | true because ofʸ p = suc (Fin.lower₁ x (notMax i x p))
  exchangeFin i x | false because _ with (suc i) Fin.≟ x
  exchangeFin i x | false because _ | true because _ = Fin.inject₁ i
  exchangeFin i x | false because _ | false because _ = x

  exchange : Fin n → Scoped (suc n) → Scoped (suc n)
  exchange i 𝟘 = 𝟘
  exchange i (ν P) = ν (exchange (suc i) P)
  exchange i (P ∥ Q) = exchange i P ∥ exchange i Q
  exchange i (x ⦅⦆ P)  = exchangeFin i x ⦅⦆ exchange (suc i) P
  exchange i (x ⟨ y ⟩ P)  = exchangeFin i x ⟨ exchangeFin i y ⟩ exchange i P

  infixl 10 _≈_
  data _≈_ : Scoped n → Scoped n → Set where
    comp-assoc : P ∥ (Q ∥ R) ≈ (P ∥ Q) ∥ R

    comp-symm : P ∥ Q ≈ Q ∥ P

    comp-end : P ∥ 𝟘 ≈ P

    scope-end : _≈_ {n} (ν 𝟘 ⦃ name ⦄) 𝟘

    scope-ext : (u : Unused zero P)
              → ν (P ∥ Q) ⦃ name ⦄ ≈ lower zero P u ∥ (ν Q) ⦃ name ⦄

    scope-scope-comm : ν (ν P ⦃ namey ⦄) ⦃ namex ⦄ ≈ ν (ν (exchange zero P) ⦃ namex ⦄) ⦃ namey ⦄

  data RecTree : Set where
    zero : RecTree
    one : RecTree → RecTree
    two : RecTree → RecTree → RecTree

  private
    variable
      r p : RecTree

  -- TODO: change names as per paper
  infixl 5 _≅⟨_⟩_
  data _≅⟨_⟩_ : Scoped n → RecTree → Scoped n → Set where
    stop_ : P ≈ Q → P ≅⟨ zero ⟩ Q

    -- Equivalence relation
    cong-refl  : P ≅⟨ zero ⟩ P
    cong-symm_ : P ≅⟨ r ⟩ Q → Q ≅⟨ one r ⟩ P
    cong-trans : P ≅⟨ r ⟩ Q → Q ≅⟨ p ⟩ R → P ≅⟨ two r p ⟩ R

    -- Congruent relation
    ν-cong_      : P ≅⟨ r ⟩ P' → ν P ⦃ name ⦄      ≅⟨ one r ⟩ ν P' ⦃ name ⦄
    comp-cong_   : P ≅⟨ r ⟩ P' → P ∥ Q             ≅⟨ one r ⟩ P' ∥ Q
    input-cong_  : P ≅⟨ r ⟩ P' → (x ⦅⦆ P) ⦃ name ⦄ ≅⟨ one r ⟩ (x ⦅⦆ P') ⦃ name ⦄
    output-cong_ : P ≅⟨ r ⟩ P' → x ⟨ y ⟩ P         ≅⟨ one r ⟩ x ⟨ y ⟩ P'

  _≅_ : Scoped n → Scoped n → Set
  P ≅ Q = ∃[ r ] (P ≅⟨ r ⟩ Q)

  _[_↦_]' : Fin n → Fin n → Fin n → Fin n
  x [ i ↦ j ]' with i Finₚ.≟ x
  x [ i ↦ j ]' | true because _ = j
  x [ i ↦ j ]' | false because _ = x

  _[_↦_] : Scoped n → (i j : Fin n) → Scoped n
  𝟘           [ i ↦ j ] = 𝟘
  (ν P)       [ i ↦ j ] = ν (P [ suc i ↦ suc j ])
  (P ∥ Q)     [ i ↦ j ] = (P [ i ↦ j ]) ∥ (Q [ i ↦ j ])
  (x ⦅⦆ P)    [ i ↦ j ] = (x [ i ↦ j ]') ⦅⦆ (P [ suc i ↦ suc j ])
  (x ⟨ y ⟩ P) [ i ↦ j ] = (x [ i ↦ j ]') ⟨ y [ i ↦ j ]' ⟩ (P [ i ↦ j ])

  substFin-unused : ∀ {i j} (x : Fin (suc n)) → i ≢ j → i ≢ x [ i ↦ j ]'
  substFin-unused {i = i} x i≢j  with i Finₚ.≟ x
  substFin-unused {i = i} x i≢j | true because _ = i≢j
  substFin-unused {i = i} x i≢j | false because ofⁿ ¬p = ¬p

  subst-unused : {i j : Fin (suc n)}
               → i ≢ j
               → (P : Scoped (suc n))
               → Unused i (P [ i ↦ j ])
  subst-unused i≢j 𝟘 = tt
  subst-unused i≢j (ν P) = subst-unused (λ i≡j → i≢j (Finₚ.suc-injective i≡j)) P
  subst-unused i≢j (P ∥ Q) = subst-unused i≢j P , subst-unused i≢j Q
  subst-unused i≢j (x ⦅⦆ P) = substFin-unused x i≢j , subst-unused (λ i≡j → i≢j (Finₚ.suc-injective i≡j)) P
  subst-unused i≢j (x ⟨ y ⟩ P) = substFin-unused x i≢j , substFin-unused y i≢j , subst-unused i≢j P

  data Channel : ℕ → Set where
    internal : ∀ {n}         → Channel n
    external : ∀ {n} → Fin n → Channel n

  dec : Channel (suc n) → Channel n
  dec internal = internal
  dec (external zero) = internal
  dec (external (suc i)) = external i

  maybe : ∀ {a} {A : Set a} → A → (Fin n → A) → Channel n → A
  maybe b f internal = b
  maybe b f (external x) = f x

  infixl 5 _=[_]⇒_
  data _=[_]⇒_ : Scoped n → Channel n → Scoped n → Set where

    comm : {P : Scoped (1 + n)} {Q : Scoped n} {i j : Fin n}
         → let uP' = subst-unused (λ ()) P
         in ((i ⦅⦆ P) ⦃ name ⦄) ∥ (i ⟨ j ⟩ Q) =[ external i ]⇒ lower zero (P [ zero ↦ suc j ]) uP' ∥ Q

    par_ : ∀ {c} {P P' Q : Scoped n}
         → P =[ c ]⇒ P'
         → P ∥ Q =[ c ]⇒ P' ∥ Q

    res_ : ∀ {c} {P Q : Scoped (1 + n)}
         → P =[ c ]⇒ Q
         → ν P ⦃ name ⦄ =[ dec c ]⇒ ν Q ⦃ name ⦄

    struct : ∀ {c} {P P' Q' Q : Scoped n}
           → P ≅⟨ r ⟩ P'
           → P' =[ c ]⇒ Q'
           → Q' ≅⟨ r ⟩ Q
           → P =[ c ]⇒ Q

  _⇒_ : Scoped n → Scoped n → Set
  P ⇒ Q = ∃[ c ] (P =[ c ]⇒ Q)

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
module datatypes where

open import bool public
open import bool-to-string public
open import char public
open import integer public
open import list public
open import list-to-string public
open import level public
open import maybe public
open import nat public
open import nat-division public
open import nat-to-string public
open import nat-log public
open import product public
open import string public
open import sum public
open import tree public
open import trie public
open import unit public
open import vector public

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2014-05-03 Test case by Andrea Vezzosi

data Two : Set where
  a b : Two

-- This example of varying arity crashed Epic before.
f : Two → {eq : Two} → Two
f a   {x} = a
f b       = b

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}

postulate
  return  : ∀ {A} → A → IO A

{-# COMPILED_EPIC return (u1 : Unit, a : Any) -> Any = ioreturn(a) #-}

main : IO Two
main = return a

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --type-in-type #-}
module poly0 where
open import prelude
open import functors
open import poly.core public

variable
  A B C X Y : ∫
  I A⁺ B⁺ C⁺ X⁺ Y⁺ : Set
  A⁻ : A⁺ → Set
  B⁻ : B⁺ → Set
  C⁻ : C⁺ → Set
  X⁻ : X⁺ → Set
  Y⁻ : Y⁺ → Set

∃⊤ ∃⊥ ⊤∫ ∫∫ : Set → ∫
∃⊤ a = a , λ _ → ⊤
∃⊥ a = a , λ _ → ⊥
⊤∫ a = ⊤ , λ _ → a
∫∫ a = a , λ _ → a
𝒴 𝟘 : ∫
𝒴 = ⊤ , λ _ → ⊤
𝟘  = ⊥ , λ _ → ⊥

module _ {A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫} where
  infixl 5 _★_
  -- infix notatjon for get
  _★_ : A⁺ → (l : ∫[ A , B ]) → B⁺
  σa ★ l = get l σa
  infixr 4 _#_←_
  -- Infix notatjon for set
  _#_←_ : (a⁺ : A⁺) → (A↝B : ∫[ A , B ]) → B⁻ (a⁺ ★ A↝B) → A⁻ a⁺
  a⁺ # l ← b⁻ = π₂ (l a⁺) b⁻
  _↕_ : (get : A⁺ → B⁺) → (set : (a⁺ : A⁺) → B⁻ (get a⁺) → A⁻ a⁺) → ∫[ A , B ]
  g ↕ s = λ a⁺ → (g a⁺) , (s a⁺)

module _ {A@(A⁺ , A⁻) C@(C⁺ , C⁻) : ∫} (l : ∫[ A , C ]) where
    -- vertical and cartesian factorization
    Factor : Σ[ B ∈ ∫ ] (∫[ A , B ]) × (∫[ B , C ])
    Factor = (A⁺ , C⁻ ∘ get l)
           , id ↕ set l
           , get l ↕ λ _ → id

module lenses (f : A⁺ → B⁺) where
    constant : ∫[ ∃⊥ A⁺ , ∃⊥ B⁺ ]
    emitter  : ∫[ ∃⊤ A⁺ , ∃⊤ B⁺ ]
    sensor   : ∫[ ⊤∫ B⁺ , ⊤∫ A⁺ ]
    constant a⁺ = f a⁺ , id
    emitter  a⁺ = f a⁺ , λ _ → tt
    sensor   _  = tt   , f
open lenses public
enclose : ((a⁺ : A⁺) → B⁻ a⁺) → ∫[ (A⁺ , B⁻) , 𝒴 ]
enclose f a⁺ = tt , λ _ → f a⁺
auto : ∫[ ∃⊤ A⁺ , 𝒴 ]
auto = enclose λ _ → tt

{-
lift∫ : (f : Set → Set) → ∫ → ∫
lift∫ f (A⁺ , A⁻) = A⁺ , f ∘ A⁻

liftLens : ∀ {A B} (f : Set → Set) → ∫[ A , B ] → ∫[ lift∫ f A , lift∫ f B ]
liftLens f l a⁺ with l a⁺
... | b⁺ , setb = b⁺ , φ setb
-}

{-
module lift_comonad (f : Set → Set) {A : ∫} ⦃ f_monad : Monad f ⦄ where
    extract : lift∫ f A ↝ A
    extract a⁺ = a⁺ , η f_monad
    -- id ↕ λ _ → η
    duplicate : lift∫ f A ↝ lift∫ f (lift∫ f A)
    duplicate a⁺ = a⁺ , μ
    -}

module poly-ops where
  infixl 6 _⊗_
  infixl 5 _⊕_
  _⊕_ _⊗_ _⊠_ _⊚_ : ∫ → ∫ → ∫
  (A⁺ , A⁻) ⊕ (B⁺ , B⁻) = (A⁺ ⊎ B⁺) , (A⁻ ⨄ B⁻) -- coproduct
  (A⁺ , A⁻) ⊗ (B⁺ , B⁻) = (A⁺ × B⁺) , (A⁻ ⨃ B⁻) -- product
  (A⁺ , A⁻) ⊠ (B⁺ , B⁻) = (A⁺ × B⁺) , (A⁻ ⨉ B⁻) -- juxtapose
  (A⁺ , A⁻) ⊚ (B⁺ , B⁻) = (Σ[ a⁺ ∈ A⁺ ](A⁻ a⁺ → B⁺)) -- compose
                        , λ (_ , bs) → ∃ (B⁻ ∘ bs)

  -- N-ary
  Σ⊕ : (I → ∫) → ∫
  Σ⊕ {I = I} A = Σ I (π₁ ∘ A) , λ (i , a⁺) → π₂ (A i) a⁺
  Π⊗ : (I → ∫) → ∫
  Π⊗ {I = I} a = ((i : I) → π₁ (a i))
               , λ a⁺ → Σ[ i ∈ I ](π₂ (a i) (a⁺ i))
  Π⊠ : (I → ∫) → ∫
  Π⊠ {I = I} a = ((i : I) → π₁ (a i))
               , (λ a⁺ → (i : I) -> π₂ (a i) (a⁺ i))
  _ᵒ_ : ∫ → ℕ → ∫
  _ ᵒ ℕz = 𝒴
  a ᵒ ℕs n = a ⊚ (a ᵒ n)
open poly-ops public

module lens-ops where
  _⟦+⟧_ : ∀ {a b x y} → ∫[ a , b ] → ∫[ x , y ] → ∫[ a ⊕ x , b ⊕ y ] -- coproduct
  _⟦|⟧_ : ∀ {a b x  } → ∫[ a , x ] → ∫[ b , x ] → ∫[ a ⊕ b ,     x ] -- copair
  _⟦⊗⟧_ : ∀ {a b x y} → ∫[ a , b ] → ∫[ x , y ] → ∫[ a ⊗ x , b ⊗ y ] -- product
  _⟦×⟧_ : ∀ {x a b  } → ∫[ x , a ] → ∫[ x , b ] → ∫[ x     , a ⊗ b ] -- pair
  _⟦⊠⟧_ : ∀ {a b x y} → ∫[ a , b ] → ∫[ x , y ] → ∫[ a ⊠ x , b ⊠ y ] -- juxtaposition
  _⟦⊚⟧_ : ∀ {a b x y} → ∫[ a , b ] → ∫[ x , y ] → ∫[ a ⊚ x , b ⊚ y ] -- composition

  (a↝b ⟦+⟧ x↝y) = λ{(Σ₁ a⁺) → let b⁺ , setb = a↝b a⁺ in Σ₁ b⁺  , setb
                   ;(Σ₂ x⁺) → let y⁺ , sety = x↝y x⁺ in Σ₂ y⁺  , sety}

  (a↝x ⟦|⟧ b↝x) = λ{(Σ₁ a⁺) → a↝x a⁺
                   ;(Σ₂ b⁺) → b↝x b⁺}

  (a↝b ⟦⊗⟧ x↝y) (a⁺ , x⁺) with a↝b a⁺ | x↝y x⁺
  ... | b⁺ , setb | y⁺ , sety = (b⁺ , y⁺)
                  , λ{(Σ₁ b⁻) → Σ₁ (setb b⁻)
                     ;(Σ₂ y⁻) → Σ₂ (sety y⁻)}

  _⟦×⟧_ x↝a x↝b x⁺ with x↝a x⁺ | x↝b x⁺
  ... | a⁺ , seta | b⁺ , setb = (a⁺ , b⁺) , λ{(Σ₁ a⁻) → seta a⁻
                                             ;(Σ₂ b⁻) → setb b⁻}

  _⟦⊠⟧_ a↝b x↝y (a⁺ , x⁺) = ((a⁺ ★ a↝b) , (x⁺ ★ x↝y))
            , λ (b⁻ , y⁻) → (a⁺ # a↝b ← b⁻) , (x⁺ # x↝y ← y⁻)

  (a↝b ⟦⊚⟧ x↝y) (a⁺ , a⁻→x⁺) with a↝b a⁺
  ... | b⁺ , setb = (b⁺ , get x↝y ∘ a⁻→x⁺ ∘ setb)
                  , λ (b⁻ , y⁻) → let a⁻ = setb b⁻
                                  in a⁻ , (a⁻→x⁺ a⁻ # x↝y ← y⁻)

  -- N-ary
  Π⟦⊠⟧ : {as bs : I → ∫}
        → ((i : I) → (∫[ as i , bs i ]))
        → ∫[ Π⊠ as , Π⊠ bs ]
  Π⟦⊠⟧ ls as⁺ = (λ i → as⁺ i ★ ls i)
          , (λ dbs i → as⁺ i # ls i ← dbs i)
  _⟦ᵒ⟧_ : ∫[ A , B ] → (n : ℕ) → ∫[ A ᵒ n , B ᵒ n ]
  _⟦ᵒ⟧_ {a} {b} l = go where
    go : (n : ℕ) → ∫[ a ᵒ n , b ᵒ n ]
    go ℕz    = 𝒾 {x = 𝒴}
    go (ℕs n) = l ⟦⊚⟧ (go n)
open lens-ops public

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
module Prelude.Monad where

open import Agda.Primitive
open import Prelude.Function
open import Prelude.Functor
open import Prelude.Unit
open import Prelude.Applicative

open import Prelude.Monad.Indexed {I = ⊤} as Indexed

Monad : ∀ {a b} (M : Set a → Set b) → Set (lsuc a ⊔ b)
Monad M = Indexed.IMonad (λ _ _ → M)

Monad′ : ∀ {a b} (M : ∀ {a} → Set a → Set a) → Set (lsuc (a ⊔ b))
Monad′ {a} {b} M = Indexed.IMonad′ {a = a} {b = b} (λ _ _ → M)

open Indexed public hiding (IMonad; IMonad′)

monadAp : ∀ {a b} {A B : Set a} {M : Set a → Set b}
            {{_ : Functor M}} →
            (M (A → B) → ((A → B) → M B) → M B) →
            M (A → B) → M A → M B
monadAp _>>=_ mf mx = mf >>= λ f → fmap f mx

monadAp′ : ∀ {a b} {A : Set a} {B : Set b} {M : ∀ {a} → Set a → Set a}
             {{_ : Functor′ {a} {b} M}} →
            (M (A → B) → ((A → B) → M B) → M B) →
            M (A → B) → M A → M B
monadAp′ _>>=_ mf mx = mf >>= λ f → fmap′ f mx

infixr 0 caseM_of_
caseM_of_ = _>>=_

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --without-K #-}
open import Type
open import Type.Identities
open import Level.NP
open import Explore.Core
open import Explore.Properties
open import Explore.Explorable
open import Data.Zero
open import Function.NP
open import Function.Extensionality
open import Data.Product
open import Relation.Binary.PropositionalEquality.NP using (_≡_; refl; _∙_; !_)
open import HoTT
open Equivalences

import Explore.Monad
open import Explore.Isomorphism

module Explore.Zero where

module _ {ℓ} where
    𝟘ᵉ : Explore ℓ 𝟘
    𝟘ᵉ = empty-explore
    {- or
    𝟘ᵉ ε _ _ = ε
    -}

    𝟘ⁱ : ∀ {p} → ExploreInd p 𝟘ᵉ
    𝟘ⁱ = empty-explore-ind
    {- or
    𝟘ⁱ _ Pε _ _ = Pε
    -}

module _ {ℓ₁ ℓ₂ ℓᵣ} {R : 𝟘 → 𝟘 → ★₀} where
    ⟦𝟘ᵉ⟧ : ⟦Explore⟧ {ℓ₁} {ℓ₂} ℓᵣ R 𝟘ᵉ 𝟘ᵉ
    ⟦𝟘ᵉ⟧ _ εᵣ _ _ = εᵣ

module 𝟘ⁱ = FromExploreInd 𝟘ⁱ
open 𝟘ⁱ public using ()
  renaming (sum to 𝟘ˢ
           ;product to 𝟘ᵖ
           ;reify to 𝟘ʳ
           ;unfocus to 𝟘ᵘ
           )

module _ {ℓ} where

    𝟘ˡ : Lookup {ℓ} 𝟘ᵉ
    𝟘ˡ _ ()

    𝟘ᶠ : Focus {ℓ} 𝟘ᵉ
    𝟘ᶠ ((), _)

    module _ {{_ : UA}} where
        Σᵉ𝟘-ok : Adequate-Σ {ℓ} (Σᵉ 𝟘ᵉ)
        Σᵉ𝟘-ok _ = ! Σ𝟘-lift∘fst

    module _ {{_ : UA}}{{_ : FunExt}} where
        Πᵉ𝟘-ok : Adequate-Π {ℓ} (Πᵉ 𝟘ᵉ)
        Πᵉ𝟘-ok _ = ! Π𝟘-uniq _

open Adequacy _≡_
module _ {{_ : UA}} where
    𝟘ˢ-ok : Adequate-sum 𝟘ˢ
    𝟘ˢ-ok _ = Fin0≡𝟘 ∙ ! Σ𝟘-fst

    adequate-sum𝟘     = 𝟘ˢ-ok

module _ {{_ : UA}}{{_ : FunExt}} where
    𝟘ᵖ-ok : Adequate-product 𝟘ᵖ
    𝟘ᵖ-ok _ = Fin1≡𝟙 ∙ ! (Π𝟘-uniq₀ _)

    adequate-product𝟘 = 𝟘ᵖ-ok

explore𝟘          = 𝟘ᵉ
explore𝟘-ind      = 𝟘ⁱ
lookup𝟘           = 𝟘ˡ
reify𝟘            = 𝟘ʳ
focus𝟘            = 𝟘ᶠ
unfocus𝟘          = 𝟘ᵘ
sum𝟘              = 𝟘ˢ
product𝟘          = 𝟘ᵖ

Lift𝟘ᵉ : ∀ {m} → Explore m (Lift 𝟘)
Lift𝟘ᵉ = explore-iso (≃-sym Lift≃id) 𝟘ᵉ

ΣᵉLift𝟘-ok : ∀ {{_ : UA}}{{_ : FunExt}}{m} → Adequate-Σ {m} (Σᵉ Lift𝟘ᵉ)
ΣᵉLift𝟘-ok = Σ-iso-ok (≃-sym Lift≃id) {Aᵉ = 𝟘ᵉ} Σᵉ𝟘-ok

-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conat Literals
------------------------------------------------------------------------

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

module Codata.Cofin.Literals where

open import Data.Nat
open import Agda.Builtin.FromNat
open import Codata.Conat
open import Codata.Conat.Properties
open import Codata.Cofin
open import Relation.Nullary.Decidable

number : ∀ n → Number (Cofin n)
number n = record
  { Constraint = λ k → True (suc k ℕ≤? n)
  ; fromNat    = λ n {{p}} → fromℕ< (toWitness p)
  }


text:
open import Data.Product

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

open import EffectAnnotations

module Types where

-- BASE AND GROUND TYPES

postulate BType : Set -- set of base types

postulate dec-bty : (B B' : BType) → Dec (B ≡ B')

GType = BType

-- VALUE AND COMPUTATION TYPES

mutual

  data VType : Set where
    ``  : GType → VType
    _⇒_ : VType → CType → VType
    ⟨_⟩ : VType → VType

  data CType : Set where
    _!_ : VType → O × I → CType

infix 30 _⇒_
infix 30 _!_

-- PROCESS TYPES

data PTypeShape : Set where
  _!_ : VType → I → PTypeShape
  _∥_ : PTypeShape → PTypeShape → PTypeShape

data PType : O → Set where

  _‼_,_ : (X : VType) →
          (o : O) →
          (i : I) →
          ---------------
          PType o

  _∥_   : {o o' : O} →
          (PP : PType o) →
          (QQ : PType o') →
          ---------------------------
          PType (o ∪ₒ o')

-- ACTION OF INTERRUPTS ON PROCESS TYPES

_↓ₚₚ_ : (op : Σₛ) → {o : O} →
        PType o → Σ[ o' ∈ O ] PType o'
op ↓ₚₚ (X ‼ o , i) with op ↓ₑ (o , i)
... | (o' , i') =
  o' , (X ‼ o' , i')
op ↓ₚₚ (PP ∥ QQ) with op ↓ₚₚ PP | op ↓ₚₚ QQ
... | (o'' , PP') | (o''' , QQ') =
  (o'' ∪ₒ o''') , (PP' ∥ QQ')

_↓ₚ_ : (op : Σₛ) → {o : O} →
       (PP : PType o) → PType (proj₁ (op ↓ₚₚ PP))

op ↓ₚ PP = proj₂ (op ↓ₚₚ PP)

-- ACTION OF INTERRUPTS ON PROCESS TYPES PRESERVES SIGNAL ANNOTATIONS

{- LEMMA 4.1 -}

↓ₚₚ-⊑ₒ : {op : Σₛ}
        {o : O} →
        (PP : PType o) →
        ----------------------
        o ⊑ₒ proj₁ (op ↓ₚₚ PP)

↓ₚₚ-⊑ₒ (X ‼ o , i) =
  ↓ₑ-⊑ₒ
↓ₚₚ-⊑ₒ (PP ∥ QQ) =
  ∪ₒ-fun (↓ₚₚ-⊑ₒ PP) (↓ₚₚ-⊑ₒ QQ)

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


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

open import Categories.Category

module Categories.Diagram.Coequalizer {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning

open import Level

private
  variable
    A B : Obj
    h i : A ⇒ B

record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    {obj} : Obj
    arr   : B ⇒ obj

    equality   : arr ∘ f ≈ arr ∘ g
    coequalize : h ∘ f ≈ h ∘ g → obj ⇒ cod h
    universal  : ∀ {eq : h ∘ f ≈ h ∘ g} → h ≈ coequalize eq ∘ arr
    unique     : ∀ {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

module F2a where

open import Agda.Prim
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

open import Paths
open import Evaluator

------------------------------------------------------------------------------
--
-- General structure and idea
--
-- We have pointed types (Paths.agda)
-- We have paths between pointed types (Paths.agda)
-- We have functions between pointed types (that use ≡ to make sure the
--   basepoint is respected) (F2a.agda)
-- Then we use univalence to connect these two independently developed
--   notions (F2a.agda)
-- Because our paths are richer than just refl and our functions are
--   more restricted than arbitrary functions, and in fact because our
--   path constructors are sound and complete for the class of functions
--   we consider, we hope to _prove_ univalence
--
------------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Equivalences between raw functions and types
-- This is generalized below to pointed types

-- Two functions are ∼ is they map each argument to related results

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

-- quasi-inverses

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ∘ g) ∼ id
    β : (g ∘ f) ∼ id

idqinv : ∀ {ℓ} → {A : Set ℓ} → qinv {ℓ} {ℓ} {A} {A} id
idqinv = record {
           g = id ;
           α = λ b → refl ;
           β = λ a → refl
         }

-- equivalences

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f ∘ g) ∼ id
    h : B → A
    β : (h ∘ f) ∼ id

equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) isequiv

idequiv : ∀ {ℓ} {A : Set ℓ} → A ≃ A
idequiv = (id , equiv₁ idqinv)

-- Function extensionality

{--
happly : ∀ {ℓ} {A B : Set ℓ} {f g : A → B} → (Path f g) → (f ∼ g)
happly {ℓ} {A} {B} {f} {g} p =
  (pathInd
    (λ _ → f ∼ g) -- f ∼ g
    (λ {AA} a x → {!!}) {!!}
    {!!} {!!} {!!} {!!} {!!} {!!}
    {!!} {!!} (λ a b x → {!cong (evalB p) (eval-resp-• (p))!})
    {!!} {!!} {!!} {!!} {!!} {!!}
    (λ a x → {!!}) (λ p₁ q x x₁ x₂ → x x₂)
    (λ p₁ q x x₁ x₂ → x x₂) (λ p₁ q x x₁ x₂ → x x₂) (λ p₁ q x x₁ x₂ → x₁ x₂))
  {A → B} {A → B} {f} {g} p

postulate
  funextP : {A B : Set} {f g : A → B} →
            isequiv {A = Path f g} {B = f ∼ g} happly

funext : {A B : Set} {f g : A → B} → (f ∼ g) → (Path f g)
funext = isequiv.g funextP

-- Universes; univalence

idtoeqv : {A B : Set} → (Path A B) → (A ≃ B)
idtoeqv {A} {B} p = {!!}
{--
  (pathInd
    (λ {S₁} {S₂} {A} {B} p → {!!})
    {!!} {!!}
    {!!} {!!} {!!} {!!} {!!} {!!}
    {!!} {!!} {!!}
    {!!} {!!} {!!} {!!} {!!} {!!}
    {!!} {!!} {!!} {!!} {!!})
  {Set} {Set} {A} {B} p
--}

postulate
  univalence : {ℓ : Level} {A B : Set ℓ} → (Path A B) ≃ (A ≃ B)

--}

path2fun : {ℓ : Level} {A B : Set ℓ} → (Path A B) → (A ≃ B)
path2fun p = ( {!!} , {!!})

------------------------------------------------------------------------------
-- Functions and equivalences between pointed types

-- Univalence as a postulate for now but hopefully we can actually prove it
-- since the pi-combinators are sound and complete for isomorphisms between
-- finite types

--postulate
--  univalence• : {ℓ : Level} {A• B• : Set• {ℓ}} → (Path A• B•) ≃• (A• ≃• B•)

{--
record isequiv• {ℓ} {A B : Set} {A• B• : Set• {ℓ}} (f• : A• →• B•) :
  Set (lsuc ℓ) where
  constructor mkisequiv•
  field
    equi : isequiv (fun f•)
    path' : Path (• A•) (• B•)

_≈•_ : ∀ {ℓ} {A B : Set} (A• B• : Set• {ℓ}) → Set (lsuc ℓ)
_≈•_ {_} {A} {B} A• B• = Σ (A• →• B•) (isequiv• {_} {A} {B})
--}

------------------------------------------------------------------------------
-- Univalence for pointed types

eval• :  {ℓ : Level} {A• B• : Set• {ℓ}} → A• ⇛ B• → (A• →• B•)
eval• c = record { fun = eval c ; resp• = eval-resp-• c }

evalB• :  {ℓ : Level} {A• B• : Set• {ℓ}} → A• ⇛ B• → (B• →• A•)
evalB• c = record { fun = evalB c ; resp• = evalB-resp-• c }

-- This is at the wrong level... We need to define equivalences ≃ between
-- pointed sets too...

{--
path2iso : {ℓ : Level} {A• B• : Set• {ℓ}} → A• ⇛ B• → ∣ A• ∣ ≃ ∣ B• ∣
path2iso {ℓ} {a} {b} p = (eval p ,
  mkisequiv (evalB p) (λ x → {!!}) (evalB p) (λ x → {!eval∘evalB p!}))
--}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
postulate
  A : Set
  P : A → Set
  a : A

  T    : Set → Set
  proj : (X : Set) → T X → X
  t    : T (∀ {x} → P x)

-- Checking target types first would prematurely solve the underscore
-- with `P a` instead of the correct `∀ {x} → P x`
fail : P a
fail = proj _ t

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- First generalizes the idea that an element is the first in a list to
-- satisfy a predicate.
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.First {a} {A : Set a} where

open import Level using (_⊔_)
open import Data.Empty
open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.Product as Prod using (∃; -,_; _,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Function
open import Relation.Unary
open import Relation.Nullary

-----------------------------------------------------------------------
-- Basic type.

module _ {p q} (P : Pred A p) (Q : Pred A q) where

  data First : Pred (List A) (a ⊔ p ⊔ q) where
    [_] : ∀ {x xs} → Q x            → First (x ∷ xs)
    _∷_ : ∀ {x xs} → P x → First xs → First (x ∷ xs)

  data FirstView : Pred (List A) (a ⊔ p ⊔ q) where
    _++_∷_ : ∀ {xs y} → All P xs → Q y → ∀ ys → FirstView (xs List.++ y ∷ ys)

------------------------------------------------------------------------
-- map

module _ {p q r s} {P : Pred A p} {Q : Pred A q} {R : Pred A r} {S : Pred A s} where

  map : P ⊆ R → Q ⊆ S → First P Q ⊆ First R S
  map p⇒r q⇒r [ qx ]      = [ q⇒r qx ]
  map p⇒r q⇒r (px ∷ pqxs) = p⇒r px ∷ map p⇒r q⇒r pqxs

module _ {p q r} {P : Pred A p} {Q : Pred A q} {R : Pred A r} where

  map₁ : P ⊆ R → First P Q ⊆ First R Q
  map₁ p⇒r = map p⇒r id

  map₂ : Q ⊆ R → First P Q ⊆ First P R
  map₂ = map id

  refine : P ⊆ Q ∪ R → First P Q ⊆ First R Q
  refine f [ qx ]      = [ qx ]
  refine f (px ∷ pqxs) with f px
  ... | inj₁ qx = [ qx ]
  ... | inj₂ rx = rx ∷ refine f pqxs

module _ {p q} {P : Pred A p} {Q : Pred A q} where

------------------------------------------------------------------------
-- Operations

  empty : ¬ First P Q []
  empty ()

  tail : ∀ {x xs} → ¬ Q x → First P Q (x ∷ xs) → First P Q xs
  tail ¬qx [ qx ]      = ⊥-elim (¬qx qx)
  tail ¬qx (px ∷ pqxs) = pqxs

  index : First P Q ⊆ (Fin ∘′ List.length)
  index [ qx ]     = zero
  index (_ ∷ pqxs) = suc (index pqxs)

  index-satisfied : ∀ {xs} (pqxs : First P Q xs) → Q (List.lookup xs (index pqxs))
  index-satisfied [ qx ]     = qx
  index-satisfied (_ ∷ pqxs) = index-satisfied pqxs

  satisfied : ∀ {xs} → First P Q xs → ∃ Q
  satisfied pqxs = -, index-satisfied pqxs

  satisfiable : Satisfiable Q → Satisfiable (First P Q)
  satisfiable (x , qx) = List.[ x ] , [ qx ]

------------------------------------------------------------------------
-- Decidability results

  first : Π[ P ∪ Q ] → Π[ First P Q ∪ All P ]
  first p⊎q []       = inj₂ []
  first p⊎q (x ∷ xs) with p⊎q x
  ... | inj₁ px = Sum.map (px ∷_) (px ∷_) (first p⊎q xs)
  ... | inj₂ qx = inj₁ [ qx ]

------------------------------------------------------------------------
-- Relationship with Any

module _ {q} {Q : Pred A q} where

  fromAny : Any Q ⊆ First U Q
  fromAny (here qx)   = [ qx ]
  fromAny (there any) = _ ∷ fromAny any

  toAny : ∀ {p} {P : Pred A p} → First P Q ⊆ Any Q
  toAny [ qx ]     = here qx
  toAny (_ ∷ pqxs) = there (toAny pqxs)


text:
-- {-# OPTIONS -v tc.meta.assign:15 #-}
-- Ulf, 2011-10-04
-- I still don't quite believe in irrelevant levels. In part because I just proved ⊥:

module IrrelevantLevelHurkens where

open import Imports.Level

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

data Irr .(i : Level)(A : Set i) : Set where
  irr : Irr i A

data Unit : Set where
  unit : Unit

unirr : ∀ .i (A : Set i) → Irr i A → Unit
unirr i A irr = unit

↓_  : ∀ .{i} → Set i → Set
foo : ∀ .{i}{A : Set i}(x : Irr i A) → unirr i A x ≡ unirr zero (↓ A) _
↓ A    = _
foo xs = refl
{- Andreas, 2011-10-04 Irrelevant Levels do not harmonize with solving

type of meta = .{.i : Level} (A : Set .i) → Set
solving _39 := λ {.i} A → A
term _38 xs := xs
passed occursCheck
type of meta = ..{i : Level} {A : Set i} (x : Irr .(i) A) →
               Irr .(zero) (↓ A)
solving _38 := λ {i} {A} x → x

The solutions x and A for the two holes do not type check, if entered manually.
The solver would need to re-type-check to make sure solutions are correct.
For now, just do not supply --experimental-irrelevance flag.
-}

⊥′ : Set
⊥′ = ↓ ((A : Set) → A)

¬_ : Set → Set
¬ A = A → ⊥′

P : Set → Set
P A = ↓ (A → Set)

U : Set
U = ↓ ((X : Set) → (P (P X) → X) → P (P X))

τ : P (P U) → U
τ t = λ X f p → t λ x → p (f (x X f))

σ : U → P (P U)
σ s pu = s U (λ t → τ t) pu

Δ : P U
Δ = λ y → ¬ ((p : P U) → σ y p → p (τ (σ y)))

Ω : U
Ω X t px = τ (λ p → (x : U) → σ x p → p x) X t px

D : Set
D = (p : P U) → σ Ω p → p (τ (σ Ω))

lem₁ : (p : P U) → ((x : U) → σ x p → p x) → p Ω
lem₁ p H1 = H1 Ω λ x → H1 (τ (σ x))

lem₂ : ¬ D
lem₂ d A = lem₁ Δ (λ x H2 H3 → H3 Δ H2 λ p → H3 λ y → p (τ (σ y))) d A

lem₃ : D
lem₃ p = lem₁ λ y → p (τ (σ y))

loop : ⊥′
loop = λ A → lem₂ lem₃ A

data ⊥ : Set where

false : ⊥
false = loop ⊥

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
------------------------------------------------------------------------------
-- Streams properties
------------------------------------------------------------------------------

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

module FOTC.Data.Stream.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Conat
open import FOTC.Data.Conat.Equality.Type
open import FOTC.Data.List
open import FOTC.Data.Stream

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Stream predicate is also a pre-fixed point of the functional
-- StreamF, i.e.
--
-- StreamF Stream ≤ Stream (see FOTC.Data.Stream.Type).

-- See Issue https://github.com/asr/apia/issues/81 .
Stream-inA : D → Set
Stream-inA xs = ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream xs'
{-# ATP definition Stream-inA #-}

Stream-in : ∀ {xs} →
            ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream xs' →
            Stream xs
Stream-in h = Stream-coind Stream-inA h' h
  where
  postulate h' : ∀ {xs} → Stream-inA xs →
                 ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Stream-inA xs'
  {-# ATP prove h' #-}

-- See Issue https://github.com/asr/apia/issues/81 .
zeros-StreamA : D → Set
zeros-StreamA xs = xs ≡ zeros
{-# ATP definition zeros-StreamA #-}

zeros-Stream : Stream zeros
zeros-Stream = Stream-coind zeros-StreamA h refl
  where
  postulate h : ∀ {xs} → zeros-StreamA xs →
                ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ zeros-StreamA xs'
  {-# ATP prove h #-}

-- See Issue https://github.com/asr/apia/issues/81 .
ones-StreamA : D → Set
ones-StreamA xs = xs ≡ ones
{-# ATP definition ones-StreamA #-}

ones-Stream : Stream ones
ones-Stream = Stream-coind ones-StreamA h refl
  where
  postulate h : ∀ {xs} → ones-StreamA xs →
                ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ ones-StreamA xs'
  {-# ATP prove h #-}

postulate ∷-Stream : ∀ {x xs} → Stream (x ∷ xs) → Stream xs
{-# ATP prove ∷-Stream #-}

-- Adapted from (Sander 1992, p. 59).

-- See Issue https://github.com/asr/apia/issues/81 .
streamLengthR : D → D → Set
streamLengthR m n = ∃[ xs ] Stream xs ∧ m ≡ length xs ∧ n ≡ ∞
{-# ATP definition streamLengthR #-}

streamLength : ∀ {xs} → Stream xs → length xs ≈ ∞
streamLength {xs} Sxs = ≈-coind streamLengthR h₁ h₂
  where
  postulate
    h₁ : ∀ {m n} → streamLengthR m n →
         m ≡ zero ∧ n ≡ zero
           ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ streamLengthR m' n')
  {-# ATP prove h₁ #-}

  postulate h₂ : streamLengthR (length xs) ∞
  {-# ATP prove h₂ #-}

------------------------------------------------------------------------------
-- References
--
-- Sander, Herbert P. (1992). A Logic of Functional Programs with an
-- Application to Concurrency. PhD thesis. Department of Computer
-- Sciences: Chalmers University of Technology and University of
-- Gothenburg.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Agda.Primitive public using (lzero)

{-# BUILTIN LEVELZERO lzero #-}


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

open import Relation.Binary

module Algorithms.List.Sort.Common
  {c l₁ l₂} (DTO : DecTotalOrder c l₁ l₂)
  where

-- agda-stdlib
open import Data.List
import Data.List.Relation.Binary.Equality.Setoid as ListSetoidEquality
open import Data.List.Relation.Unary.AllPairs
open import Data.List.Relation.Unary.Linked
import Data.List.Relation.Unary.Linked.Properties as Linkedₚ

-- agda-misc
open import Experiment.ListRelationProperties using (Linked-resp-≋)

open DecTotalOrder DTO
open ListSetoidEquality Eq.setoid

Sorted : List Carrier → Set _
Sorted = Linked _≤_

toAllPairs : ∀ {xs} → Sorted xs → AllPairs _≤_ xs
toAllPairs = Linkedₚ.Linked⇒AllPairs trans

Sorted-resp-≋ : ∀ {xs ys} → xs ≋ ys → Sorted xs → Sorted ys
Sorted-resp-≋ = Linked-resp-≋ Eq.setoid ≤-resp-≈


text:
------------------------------------------------------------------------------
-- First-order logic base
------------------------------------------------------------------------------

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

module FOL.Base where

infix  2 ⋀
infixr 1 _⇒_
infixr 0 _⇔_

------------------------------------------------------------------------------
-- First-order logic (without equality).
open import Common.FOL.FOL public

------------------------------------------------------------------------------
-- We added extra symbols for the implication, the biconditional and
-- the universal quantification (see module Common.FOL.FOL).

-- The implication data type.
data _⇒_ (A B : Set) : Set where
  fun : (A → B) → A ⇒ B

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

-- Biconditional.
_⇔_ : Set → Set → Set
A ⇔ B = (A ⇒ B) ∧ (B ⇒ A)

-- The universal quantifier type on D.
data  ⋀ (A : D → Set) : Set where
  dfun : ((t : D) → A t) → ⋀ A

-- Sugar syntax for the universal quantifier.
syntax ⋀ (λ x → e) = ⋀[ x ] e

dapp : {A : D → Set}(t : D) → ⋀ A → A t
dapp t (dfun f) = f t

------------------------------------------------------------------------------
-- In first-order logic it is assumed that the universe of discourse
-- is non-empty.
postulate D≢∅ : D

------------------------------------------------------------------------------
-- The ATPs work in classical logic, therefore we add the principle of
-- the exclude middle for prove some non-intuitionistic theorems. Note
-- that we do not need to add the postulate as an ATP axiom.

-- The principle of the excluded middle.
postulate pem : ∀ {A} → A ∨ ¬ A


text:
module Thesis.RelateToValidity where

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

open import Thesis.Changes
open import Thesis.Lang

module _ {A : Set} {{CA : ChangeStructure A}} where
  fromto→valid fromto→valid-2 : ∀ da (a1 a2 : A) (daa : ch da from a1 to a2) → valid a1 da
  fromto→valid da a1 a2 daa rewrite fromto→⊕ da a1 _ daa = daa
  fromto→valid-2 da a1 a2 daa = subst (ch da from a1 to_) (sym (fromto→⊕ da a1 a2 daa)) daa

  -- The "inverse" is so trivial to not be worth calling, hence commented out:
  -- valid→fromto : ∀ da (a : A) → (valid a da) → ch da from a to (a ⊕ da)
  -- valid→fromto _ _ daa = daa

module _
  {A : Set} {B : Set} {{CA : ChangeStructure A}} {{CB : ChangeStructure B}} where

  WellDefinedFunChangePoint : ∀ (f : A → B) → (df : Ch (A → B)) → ∀ a da → Set
  WellDefinedFunChangePoint f df a da = (f ⊕ df) (a ⊕ da) ≡ f a ⊕ df a da

  WellDefinedFunChangeFromTo′ : ∀ (f1 : A → B) → (df : Ch (A → B)) → Set
  WellDefinedFunChangeFromTo′ f1 df = ∀ da a → valid a da → WellDefinedFunChangePoint f1 df a da

  open ≡-Reasoning
  open import Function

  fromto-incrementalization : ∀ {f1 f2 : A → B} {df} → ch df from f1 to f2 →
    ∀ {da a} → valid a da →
    f1 a ⊕ df a da ≡ f2 (a ⊕ da)
  fromto-incrementalization {f1 = f1} {f2} {df} dff {da} {a} daa = fromto→⊕ _ _ _ (dff da a _ daa)

  fromto→valid-fun : ∀ {f1 f2 : A → B} {df : Ch (A → B)} → ch df from f1 to f2 → ∀ {a da} (daa : valid a da) → valid (f1 a) (df a da)
  fromto→valid-fun {f1} {f2} {df} dff {a} {da} daa = fromto→valid (df a da) (f1 a) _ (dff da a _ daa)

  fromto→WellDefined′ : ∀ {f1 f2 df} → ch df from f1 to f2 →
    WellDefinedFunChangeFromTo′ f1 df
  fromto→WellDefined′ {f1 = f1} {f2} {df} dff da a daa =
    begin
      (f1 ⊕ df) (a ⊕ da)
    ≡⟨ cong (_$ (a ⊕ da)) (fromto→⊕ df f1 f2 dff)⟩
      f2 (a ⊕ da)
    ≡⟨ sym (fromto-incrementalization dff daa) ⟩
      f1 a ⊕ df a da
    ∎

  -- Δ f is similar to function changes in PLDI'14, but PLDI'14 function changes
  -- need not be defined on invalid changes; instead, if (df, dff) : Δ f, then
  -- df is a function change that is also defined on invalid changes.
  --
  -- Next we define fΔ. It is closer to the PLDI'14 definition of function
  -- changes; but it is not defined recursively, so it still produces new-style
  -- function changes.
  --
  -- Hence this is sort of bigger than Δ f, though not really.
  fΔ : (A → B) → Set
  fΔ f = (a : A) → Δ₁ a → Δ₁ (f a)

  -- We can indeed map Δ f into fΔ f, via valid-functions-map-Δ. If this mapping
  -- were an injection, we could say that fΔ f is bigger than Δ f. But we'd need
  -- first to quotient Δ f to turn valid-functions-map-Δ into an injection:
  --
  -- 1. We need to quotient Δ f by extensional equivalence of functions.
  --    Luckily, we can just postulate it.
  --
  -- 2. We need to quotient Δ f by identifying functions that only differ by
  --    behavior on invalid changes; such functions can't be distinguished after
  --    being injected into fΔ f.
  valid-functions-map-Δ : ∀ (f : A → B) (df : Δ₁ f) → fΔ f
  valid-functions-map-Δ f (df , dff) a (da , daa) = df a da , valid-res
    where
      valid-res : ch df a da from f a to (f a ⊕ df a da)
      valid-res rewrite sym (fromto→WellDefined′ dff da a daa) = dff da a (a ⊕ da) daa

  -- Two alternative proofs
  fromto-functions-map-Δ-1 fromto-functions-map-Δ-2 : ∀ (f1 f2 : A → B) (df : Ch (A → B)) → ch df from f1 to f2 → fΔ f1
  fromto-functions-map-Δ-1 f1 f2 df dff a (da , daa) = valid-functions-map-Δ f1 (df , fromto→valid df f1 f2 dff) a (da , daa)

  fromto-functions-map-Δ-2 f1 f2 df dff a (da , daa) = df a da , fromto→valid-fun dff daa

open import Thesis.LangChanges

fromto→WellDefined′Lang : ∀ {σ τ f1 f2 df} → [ σ ⇒ τ ]τ df from f1 to f2 →
  WellDefinedFunChangeFromTo′ f1 df
fromto→WellDefined′Lang {f1 = f1} {f2} {df} dff da a daa =
  fromto→WellDefined′ dff da a daa

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Issue553a where

data D : Set where
  d₁ d₂ : D

data E : Set where

module M (A : Set) where

  data B : Set where
    b : D → B

  T : B → Set
  T (b d₁) = E
  T (b d₂) = E

open M E

g : (d : D) → T (b d) → D
g d t with d₁
g d t | d′ = d′  -- Unsolved meta-variable, no constraints.


text:
module Data.Tuple.Raise where

open import Data.Tuple.Raiseᵣ public

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:
------------------------------------------------------------------------
-- Some counterexamples
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Bisimilarity.Up-to.Counterexamples where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Fin equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import Surjection equality-with-J using (_↠_)

open import Indexed-container using (Container; ν; ⟦_⟧; force)
open import Labelled-transition-system
import Up-to

import Bisimilarity
import Bisimilarity.Classical
open import Bisimilarity.Comparison
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Step
import Bisimilarity.Up-to
open import Equational-reasoning
open import Relation

private

  -- A combination of some parametrised modules.

  module Combination {ℓ} (lts : LTS ℓ) where

    open Bisimilarity lts public
    open Bisimilarity.Classical lts public using (Progression)
    open Bisimilarity.Up-to lts public
    open LTS lts public hiding (_[_]⟶_)

    private
      module S =
        Bisimilarity.Step lts (LTS._[_]⟶_ lts) (LTS._[_]⟶_ lts)

    open S public using (Step; Step↔StepC) hiding (module Step)

    module Step where
      open S public using (⟨_,_⟩)
      open S.Step public

-- There is a size-preserving relation transformer that is neither
-- monotone nor extensive.

∃size-preserving×¬[monotone⊎extensive] :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ∃ λ (F : Trans₂ (# 0) Proc) →
      Size-preserving F × ¬ (Monotone F ⊎ Extensive F)
∃size-preserving×¬[monotone⊎extensive] =
  one-loop , F , F-pres , [ ¬-F-mono , ¬-F-extensive ]
  where
  open Combination one-loop

  F : Trans₂ (# 0) Proc
  F R = ¬_ ∘ R

  ¬-F-mono : ¬ Monotone F
  ¬-F-mono =
    Monotone F                                                   ↝⟨ (λ mono → mono {_}) ⟩
    ((λ _ → ⊥) ⊆ (λ _ → ↑ _ ⊤) → F (λ _ → ⊥) ⊆ F (λ _ → ↑ _ ⊤))  ↔⟨⟩
    ((λ _ → ⊥) ⊆ (λ _ → ↑ _ ⊤) → (λ _ → ¬ ⊥) ⊆ (λ _ → ¬ ↑ _ ⊤))  ↝⟨ _$ _ ⟩
    (λ _ → ¬ ⊥) ⊆ (λ _ → ¬ ↑ _ ⊤)                                ↝⟨ (λ hyp → hyp {tt}) ⟩
    (¬ ⊥ → ¬ ↑ _ ⊤)                                              ↝⟨ _$ ⊥-elim ⟩
    ¬ ↑ _ ⊤                                                      ↝⟨ _$ _ ⟩□
    ⊥                                                            □

  ¬-F-extensive : ¬ Extensive F
  ¬-F-extensive =
    Extensive F        ↝⟨ (λ hyp → hyp _) ⟩
    (↑ _ ⊤ → ¬ ↑ _ ⊤)  ↝⟨ (_$ _) ∘ (_$ _) ⟩□
    ⊥                  □

  total : ∀ {i x y} → [ i ] x ∼ y
  total = reflexive

  F-pres : Size-preserving F
  F-pres _ _ = total

-- A slight strengthening of the previous result, with a somewhat more
-- complicated proof: There are (at least two) size-preserving
-- relation transformers that are neither monotone nor extensive.

∃-2-size-preserving×¬[monotone⊎extensive] :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ∃ λ (F : Trans₂ (# 0) Proc) →
  ∃ λ (G : Trans₂ (# 0) Proc) →
    Size-preserving F × ¬ (Monotone F ⊎ Extensive F) ×
    Size-preserving G × ¬ (Monotone G ⊎ Extensive G) ×
    F ≢ G
∃-2-size-preserving×¬[monotone⊎extensive] =
    lts
  , F ⊤ , F ⊥
  , F-pres , [ ¬-F-mono , ¬-F-extensive ]
  , F-pres , [ ¬-F-mono , ¬-F-extensive ]
  , F⊤≢F⊥
  where
  lts : LTS lzero
  lts = record
    { Proc      = Bool
    ; Label     = ⊥
    ; _[_]⟶_    = λ _ ()
    ; is-silent = λ ()
    }

  open Combination lts

  F : Type → Trans₂ (# 0) Bool
  F A R p@(true  , false) = R p × A
  F A R p@(false , true)  = R p
  F A R p                 = ¬ R p

  ¬-F-mono : ∀ {A} → ¬ Monotone (F A)
  ¬-F-mono {A} =
    Monotone (F A)                                                   ↝⟨ (λ mono → mono {_}) ⟩
    ((λ _ → ⊥) ⊆ (λ _ → ↑ _ ⊤) → F A (λ _ → ⊥) ⊆ F A (λ _ → ↑ _ ⊤))  ↝⟨ (λ hyp {p} → hyp _ {p}) ⟩
    F A (λ _ → ⊥) ⊆ F A (λ _ → ↑ _ ⊤)                                ↝⟨ (λ hyp → hyp {true , true}) ⟩
    (¬ ⊥ → ¬ ↑ _ ⊤)                                                  ↝⟨ _$ ⊥-elim ⟩
    ¬ ↑ _ ⊤                                                          ↝⟨ _$ _ ⟩□
    ⊥                                                                □

  ¬-F-extensive : ∀ {A} → ¬ Extensive (F A)
  ¬-F-extensive {A} =
    Extensive (F A)    ↝⟨ (λ hyp → hyp (λ _ → ↑ _ ⊤) {true , true}) ⟩
    (↑ _ ⊤ → ¬ ↑ _ ⊤)  ↝⟨ (_$ _) ∘ (_$ _) ⟩□
    ⊥                  □

  F-pres : ∀ {A} → Size-preserving (F A)
  F-pres R⊆∼i {true  , false} = R⊆∼i ∘ proj₁
  F-pres R⊆∼i {false , true}  = R⊆∼i
  F-pres _    {true  , true}  = λ _ → true ■
  F-pres _    {false , false} = λ _ → false ■

  F⊤≢F⊥ : F ⊤ ≢ F ⊥
  F⊤≢F⊥ =
    F ⊤ ≡ F ⊥                                                       ↝⟨ subst (λ F → F (λ _ → ⊤) (true , false)) ⟩
    (F ⊤  (λ _ → ⊤) (true , false) → F ⊥ (λ _ → ⊤) (true , false))  ↔⟨⟩
    (⊤ × ⊤ → ⊤ × ⊥)                                                 ↝⟨ proj₂ ∘ (_$ _) ⟩□
    ⊥                                                               □

-- There is a container C such that there are (at least two) relation
-- transformers satisfying λ F → ∀ {i} → F (ν C i) ⊆ ν C i that are
-- not up-to techniques with respect to C.

∃special-case-of-size-preserving×¬up-to :
  ∃ λ (I : Type) →
  ∃ λ (C : Container I I) →
  ∃ λ (F : Trans (# 0) I) →
  ∃ λ (G : Trans (# 0) I) →
    (∀ {i} → F (ν C i) ⊆ ν C i) × ¬ Up-to.Up-to-technique C F ×
    (∀ {i} → G (ν C i) ⊆ ν C i) × ¬ Up-to.Up-to-technique C G ×
    F ≢ G
∃special-case-of-size-preserving×¬up-to =
    (Proc × Proc)
  , StepC
  , G ⊤ , G ⊥
  , bisimilarity-pre-fixpoint
  , ¬-up-to
  , bisimilarity-pre-fixpoint
  , ¬-up-to
  , G⊤≢G⊥
  where

  data Proc : Type where
    p q r : Proc

  data _⟶_ : Proc → Proc → Type where
    p : p ⟶ p
    q : q ⟶ r

  lts = record
    { Proc      = Proc
    ; Label     = ⊤
    ; _[_]⟶_    = λ p _ q → p ⟶ q
    ; is-silent = λ _ → false
    }

  open Combination lts hiding (Proc)

  G : Type → Trans₂ (# 0) Proc
  G A R x = R (r , r) → ¬ R (p , r) → R x × A

  p≁r : ∀ {i} → ¬ Bisimilarity i (p , r)
  p≁r hyp with left-to-right hyp p
  ... | _ , () , _

  bisimilarity-pre-fixpoint :
    ∀ {A i} → G A (Bisimilarity i) ⊆ Bisimilarity i
  bisimilarity-pre-fixpoint hyp = proj₁ (hyp reflexive p≁r)

  data S : Rel₂ (# 0) Proc where
    pq : S (p , q)

  S⊆StepGS : ∀ {A} → S ⊆ Step (G A S)
  Step.left-to-right (S⊆StepGS pq) p = r , q , λ ()
  Step.right-to-left (S⊆StepGS pq) q = p , p , λ ()

  p≁q : ¬ Bisimilarity ∞ (p , q)
  p≁q hyp with left-to-right hyp p
  ... | r , q , p∼r = p≁r (force p∼r)

  ¬-up-to : ∀ {A} → ¬ Up-to-technique (G A)
  ¬-up-to {A} =
    Up-to-technique (G A)                         ↝⟨ (λ up-to → up-to) ⟩
    (S ⊆ ⟦ StepC ⟧ (G A S) → S ⊆ Bisimilarity ∞)  ↝⟨ (λ hyp below → hyp (Step↔StepC _ ∘ below)) ⟩
    (S ⊆ Step (G A S) → S ⊆ Bisimilarity ∞)       ↝⟨ _$ S⊆StepGS ⟩
    S ⊆ Bisimilarity ∞                            ↝⟨ _$ pq ⟩
    Bisimilarity ∞ (p , q)                        ↝⟨ p≁q ⟩□
    ⊥                                             □

  G⊤≢G⊥ : G ⊤ ≢ G ⊥
  G⊤≢G⊥ =
    G ⊤ ≡ G ⊥                                                    ↝⟨ subst (λ G → G (uncurry _≡_) (q , q)) ⟩
    (G ⊤ (uncurry _≡_) (q , q) → G ⊥ (uncurry _≡_) (q , q))      ↔⟨⟩
    ((r ≡ r → p ≢ r → q ≡ q × ⊤) → (r ≡ r → p ≢ r → q ≡ q × ⊥))  ↝⟨ _$ (λ _ _ → refl , _) ⟩
    (r ≡ r → p ≢ r → q ≡ q × ⊥)                                  ↝⟨ proj₂ ∘ (_$ λ ()) ∘ (_$ refl) ⟩□
    ⊥                                                            □

-- There is a container C such that there are (at least two) relation
-- transformers satisfying λ F → ∀ {i} → F (ν C i) ⊆ ν C i that are
-- not size-preserving with respect to C.

∃special-case-of-size-preserving×¬size-preserving :
  ∃ λ (I : Type) →
  ∃ λ (C : Container I I) →
  ∃ λ (F : Trans (# 0) I) →
  ∃ λ (G : Trans (# 0) I) →
    (∀ {i} → F (ν C i) ⊆ ν C i) × ¬ Up-to.Size-preserving C F ×
    (∀ {i} → G (ν C i) ⊆ ν C i) × ¬ Up-to.Size-preserving C G ×
    F ≢ G
∃special-case-of-size-preserving×¬size-preserving =
  Σ-map id (Σ-map id (Σ-map id (Σ-map id (Σ-map id
    (Σ-map (_∘ Up-to.size-preserving→up-to _) (Σ-map id
       (Σ-map (_∘ Up-to.size-preserving→up-to _) id)))))))
    ∃special-case-of-size-preserving×¬up-to

-- There is a monotone, extensive and size-preserving relation
-- transformer that is not compatible.

∃monotone×extensive×size-preserving×¬compatible :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ∃ λ (F : Trans₂ (# 0) Proc) →
    Monotone F × Extensive F × Size-preserving F × ¬ Compatible F
∃monotone×extensive×size-preserving×¬compatible =
    one-transition
  , F
  , mono
  , extensive
  , pres
  , ¬comp

  where

  -- An LTS with two distinct processes and one transition from one to
  -- the other.

  one-transition : LTS lzero
  one-transition = record
    { Proc      = Bool
    ; Label     = ⊤
    ; _[_]⟶_    = λ x _ y → T (x ∧ not y)
    ; is-silent = λ _ → false
    }

  open Combination one-transition

  -- A relation transformer.

  F : Trans₂ (# 0) Proc
  F R (true , true) = R (false , false) ⊎ R (true , true)
  F R               = R

  -- F is monotone.

  mono : Monotone F
  mono R⊆S {true  , true}  = ⊎-map R⊆S R⊆S
  mono R⊆S {true  , false} = R⊆S
  mono R⊆S {false , true}  = R⊆S
  mono R⊆S {false , false} = R⊆S

  -- F is extensive.

  extensive : Extensive F
  extensive R {true  , true}  = inj₂
  extensive R {true  , false} = id
  extensive R {false , true}  = id
  extensive R {false , false} = id

  -- Bisimilarity of size i is a pre-fixpoint of F.

  pre : ∀ {i} → F (Bisimilarity i) ⊆ Bisimilarity i
  pre {x = true  , true}  = λ _ → true ■
  pre {x = true  , false} = id
  pre {x = false , true}  = id
  pre {x = false , false} = id

  -- F is size-preserving.

  pres : Size-preserving F
  pres = _⇔_.from (monotone→⇔ mono) (λ {_ x} → pre {x = x})

  -- A relation.

  R : Rel₂ (# 0) Proc
  R _ = ⊥

  -- A lemma.

  StepRff : Step R (false , false)
  Step.left-to-right StepRff ()
  Step.right-to-left StepRff ()

  -- F is not compatible.

  ¬comp : ¬ Compatible F
  ¬comp =
    Compatible F                                                     ↝⟨ (λ comp {x} → comp {x = x}) ⟩

    F (⟦ StepC ⟧ R) ⊆ ⟦ StepC ⟧ (F R)                                ↝⟨ (λ le → le {true , true}) ⟩

    (F (⟦ StepC ⟧ R) (true , true) → ⟦ StepC ⟧ (F R) (true , true))  ↔⟨⟩

    (⟦ StepC ⟧ R (false , false) ⊎ ⟦ StepC ⟧ R (true , true) →
     ⟦ StepC ⟧ (F R) (true , true))                                  ↝⟨ _$ inj₁ (_⇔_.to (Step↔StepC _) StepRff) ⟩

    ⟦ StepC ⟧ (F R) (true , true)                                    ↝⟨ (λ step → StepC.left-to-right {p = true} {q = true} step {p′ = false} _ ) ⟩

    (∃ λ y → T (not y) × F R (false , y))                            ↔⟨⟩

    (∃ λ y → T (not y) × ⊥)                                          ↝⟨ proj₂ ∘ proj₂ ⟩□

    ⊥                                                                □

-- An LTS used in a couple of lemmas below, along with some
-- properties.

module PQR where

  -- An LTS with two sets of processes, three "to the left", and three
  -- "to the right".

  Side : Type
  Side = Bool

  pattern left  = true
  pattern right = false

  data Process : Type where
    p q r : Side → Process

  data Label : Type where
    pq pr : Label
    qq rr : Side → Label

  infix 4 _[_]⟶_

  data _[_]⟶_ : Process → Label → Process → Type where
    pq : ∀ {s} → p s [ pq ]⟶ q s
    pr : ∀ {s} → p s [ pr ]⟶ r s
    qq : ∀ {s} → q s [ qq s ]⟶ q s
    rr : ∀ {s} → r s [ rr s ]⟶ r s

  lts : LTS lzero
  lts = record
    { Proc      = Process
    ; Label     = Label
    ; _[_]⟶_    = _[_]⟶_
    ; is-silent = λ _ → false
    }

  open Combination lts public hiding (Label)

  -- Two relation transformers: F and G both add (at most) one pair to
  -- the underlying relation.

  data F (R : Rel₂ (# 0) Proc) : Rel₂ (# 0) Proc where
    qq  : F R (q left , q right)
    [_] : ∀ {x} → R x → F R x

  data G (R : Rel₂ (# 0) Proc) : Rel₂ (# 0) Proc where
    rr  : G R (r left , r right)
    [_] : ∀ {x} → R x → G R x

  -- A relation that adds one pair to reflexivity.

  data S : Rel₂ (# 0) Proc where
    pp   : S (p left , p right)
    refl : ∀ {x} → S (x , x)

  -- S progresses to F (G S).

  S-prog : Progression S (F (G S))
  S-prog pp   = Step.⟨ (λ where
                          pq → _ , pq , qq
                          pr → _ , pr , [ rr ])
                     , (λ where
                          pq → _ , pq , qq
                          pr → _ , pr , [ rr ])
                     ⟩
  S-prog refl = Step.⟨ (λ where
                          pq → _ , pq , [ [ refl ] ]
                          pr → _ , pr , [ [ refl ] ]
                          qq → _ , qq , [ [ refl ] ]
                          rr → _ , rr , [ [ refl ] ])
                     , (λ where
                          pq → _ , pq , [ [ refl ] ]
                          pr → _ , pr , [ [ refl ] ]
                          qq → _ , qq , [ [ refl ] ]
                          rr → _ , rr , [ [ refl ] ])
                     ⟩

  S-prog′ : S ⊆ ⟦ StepC ⟧ (F (G S))
  S-prog′ Sx = _⇔_.to (Step↔StepC _) (S-prog Sx)

  -- The two processes q left and q right are not bisimilar.

  q≁q : ¬ q left ∼ q right
  q≁q =
    q left ∼ q right                                ↝⟨ (λ rel → StepC.left-to-right rel qq) ⟩
    (∃ λ y → q right [ qq left ]⟶ y × q left ∼′ y)  ↝⟨ (λ { (_ , () , _) }) ⟩□
    ⊥                                               □

  -- The two processes r left and r right are not bisimilar.

  r≁r : ¬ r left ∼ r right
  r≁r =
    r left ∼ r right                                ↝⟨ (λ rel → StepC.left-to-right rel rr) ⟩
    (∃ λ y → r right [ rr left ]⟶ y × r left ∼′ y)  ↝⟨ (λ { (_ , () , _) }) ⟩□
    ⊥                                               □

  -- F ∘ G is not an up-to technique.

  ¬-F∘G-up-to : ¬ Up-to-technique (F ∘ G)
  ¬-F∘G-up-to =
    Up-to-technique (F ∘ G)                    ↝⟨ (λ up-to → up-to S-prog′) ⟩
    S ⊆ Bisimilarity ∞                         ↝⟨ (λ le → le pp) ⟩
    p left ∼ p right                           ↝⟨ (λ rel → StepC.left-to-right rel pq) ⟩
    (∃ λ y → p right [ pq ]⟶ y × q left ∼′ y)  ↝⟨ (λ { (.(q right) , pq , rel) → rel }) ⟩
    q left ∼′ q right                          ↝⟨ (λ rel → q≁q (force rel)) ⟩
    ⊥                                          □

  -- F is not equal to G.

  F≢G : F ≢ G
  F≢G =
    F ≡ G                                                              ↝⟨ subst (λ F → F (λ _ → ⊥) (q left , q right)) ⟩
    (F (λ _ → ⊥) (q left , q right) → G (λ _ → ⊥) (q left , q right))  ↝⟨ _$ qq ⟩
    G (λ _ → ⊥) (q left , q right)                                     ↝⟨ (λ { [ () ] }) ⟩□
    ⊥                                                                  □

  module F-lemmas where

    -- F is monotone.

    mono : Monotone F
    mono R⊆S qq      = qq
    mono R⊆S [ Rxy ] = [ R⊆S Rxy ]

    -- F is extensive.

    ext : Extensive F
    ext = λ _ → [_]

    -- F is not size-preserving.

    ¬-pres : ¬ Size-preserving F
    ¬-pres =
      Size-preserving F                    ↝⟨ (λ pres → _⇔_.to (monotone→⇔ mono) pres) ⟩
      F (Bisimilarity ∞) ⊆ Bisimilarity ∞  ↝⟨ _$ qq ⟩
      q left ∼ q right                     ↝⟨ q≁q ⟩□
      ⊥                                    □

    -- F is an up-to technique.

    module _ {R} (R-prog′ : R ⊆ ⟦ StepC ⟧ (F R)) where

      R-prog : Progression R (F R)
      R-prog Rx = _⇔_.from (Step↔StepC _) (R-prog′ Rx)

      ¬rr : ∀ {s} → ¬ R (r s , r (not s))
      ¬rr rel with Progression.left-to-right R-prog rel rr
      ¬rr {true}  _ | _ , () , _
      ¬rr {false} _ | _ , () , _

      ¬qq : ∀ {s} → ¬ R (q s , q (not s))
      ¬qq rel with Progression.left-to-right R-prog rel qq
      ¬qq {true}  _ | _ , () , _
      ¬qq {false} _ | _ , () , _

      ¬pp : ∀ {s} → ¬ R (p s , p (not s))
      ¬pp rel with Progression.left-to-right R-prog rel pr
      ... | .(r _) , pr , [ rel′ ] = ¬rr rel′

      ¬pq : ∀ {s₁ s₂} → ¬ R (p s₁ , q s₂)
      ¬pq rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬qp : ∀ {s₁ s₂} → ¬ R (q s₁ , p s₂)
      ¬qp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬pr : ∀ {s₁ s₂} → ¬ R (p s₁ , r s₂)
      ¬pr rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬rp : ∀ {s₁ s₂} → ¬ R (r s₁ , p s₂)
      ¬rp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬qr : ∀ {s₁ s₂} → ¬ R (q s₁ , r s₂)
      ¬qr rel with Progression.right-to-left R-prog rel rr
      ... | _ , () , _

      ¬rq : ∀ {s₁ s₂} → ¬ R (r s₁ , q s₂)
      ¬rq rel with Progression.left-to-right R-prog rel rr
      ... | _ , () , _

      up-to : R ⊆ Bisimilarity ∞
      up-to {p left  , p left}  rel = reflexive
      up-to {p left  , p right} rel = ⊥-elim (¬pp rel)
      up-to {p right , p left}  rel = ⊥-elim (¬pp rel)
      up-to {p right , p right} rel = reflexive
      up-to {p _     , q _}     rel = ⊥-elim (¬pq rel)
      up-to {p _     , r _}     rel = ⊥-elim (¬pr rel)
      up-to {q _     , p _}     rel = ⊥-elim (¬qp rel)
      up-to {q left  , q left}  rel = reflexive
      up-to {q left  , q right} rel = ⊥-elim (¬qq rel)
      up-to {q right , q left}  rel = ⊥-elim (¬qq rel)
      up-to {q right , q right} rel = reflexive
      up-to {q _     , r _}     rel = ⊥-elim (¬qr rel)
      up-to {r _     , p _}     rel = ⊥-elim (¬rp rel)
      up-to {r _     , q _}     rel = ⊥-elim (¬rq rel)
      up-to {r left  , r left}  rel = reflexive
      up-to {r left  , r right} rel = ⊥-elim (¬rr rel)
      up-to {r right , r left}  rel = ⊥-elim (¬rr rel)
      up-to {r right , r right} rel = reflexive

  module G-lemmas where

    -- G is monotone.

    mono : Monotone G
    mono R⊆S rr      = rr
    mono R⊆S [ Rxy ] = [ R⊆S Rxy ]

    -- G is extensive.

    ext : Extensive G
    ext = λ _ → [_]

    -- G is not size-preserving.

    ¬-pres : ¬ Size-preserving G
    ¬-pres =
      Size-preserving G                    ↝⟨ (λ pres → _⇔_.to (monotone→⇔ mono) pres) ⟩
      G (Bisimilarity ∞) ⊆ Bisimilarity ∞  ↝⟨ _$ rr ⟩
      r left ∼ r right                     ↝⟨ r≁r ⟩□
      ⊥                                    □

    -- G is an up-to technique.

    module _ {R} (R-prog′ : R ⊆ ⟦ StepC ⟧ (G R)) where

      R-prog : Progression R (G R)
      R-prog Rx = _⇔_.from (Step↔StepC _) (R-prog′ Rx)

      ¬rr : ∀ {s} → ¬ R (r s , r (not s))
      ¬rr rel with Progression.left-to-right R-prog rel rr
      ¬rr {true}  _ | _ , () , _
      ¬rr {false} _ | _ , () , _

      ¬qq : ∀ {s} → ¬ R (q s , q (not s))
      ¬qq rel with Progression.left-to-right R-prog rel qq
      ¬qq {true}  _ | _ , () , _
      ¬qq {false} _ | _ , () , _

      ¬pp : ∀ {s} → ¬ R (p s , p (not s))
      ¬pp rel with Progression.left-to-right R-prog rel pq
      ... | .(q _) , pq , [ rel′ ] = ¬qq rel′

      ¬pq : ∀ {s₁ s₂} → ¬ R (p s₁ , q s₂)
      ¬pq rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬qp : ∀ {s₁ s₂} → ¬ R (q s₁ , p s₂)
      ¬qp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬pr : ∀ {s₁ s₂} → ¬ R (p s₁ , r s₂)
      ¬pr rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬rp : ∀ {s₁ s₂} → ¬ R (r s₁ , p s₂)
      ¬rp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬qr : ∀ {s₁ s₂} → ¬ R (q s₁ , r s₂)
      ¬qr rel with Progression.right-to-left R-prog rel rr
      ... | _ , () , _

      ¬rq : ∀ {s₁ s₂} → ¬ R (r s₁ , q s₂)
      ¬rq rel with Progression.left-to-right R-prog rel rr
      ... | _ , () , _

      up-to : R ⊆ Bisimilarity ∞
      up-to {p left  , p left}  rel = reflexive
      up-to {p left  , p right} rel = ⊥-elim (¬pp rel)
      up-to {p right , p left}  rel = ⊥-elim (¬pp rel)
      up-to {p right , p right} rel = reflexive
      up-to {p _     , q _}     rel = ⊥-elim (¬pq rel)
      up-to {p _     , r _}     rel = ⊥-elim (¬pr rel)
      up-to {q _     , p _}     rel = ⊥-elim (¬qp rel)
      up-to {q left  , q left}  rel = reflexive
      up-to {q left  , q right} rel = ⊥-elim (¬qq rel)
      up-to {q right , q left}  rel = ⊥-elim (¬qq rel)
      up-to {q right , q right} rel = reflexive
      up-to {q _     , r _}     rel = ⊥-elim (¬qr rel)
      up-to {r _     , p _}     rel = ⊥-elim (¬rp rel)
      up-to {r _     , q _}     rel = ⊥-elim (¬rq rel)
      up-to {r left  , r left}  rel = reflexive
      up-to {r left  , r right} rel = ⊥-elim (¬rr rel)
      up-to {r right , r left}  rel = ⊥-elim (¬rr rel)
      up-to {r right , r right} rel = reflexive

-- There are monotone and extensive up-to techniques F and G such
-- that F ∘ G is not an up-to-technique.
--
-- Pous and Sangiorgi discuss another instance of this property in
-- Section 6.5.4 of "Enhancements of the bisimulation proof method".

∃[monotone×extensive×up-to]²×¬∘-up-to :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ∃ λ (F : Trans₂ (# 0) Proc) →
  ∃ λ (G : Trans₂ (# 0) Proc) →
    Monotone F × Extensive F × Up-to-technique F ×
    Monotone G × Extensive G × Up-to-technique G ×
    ¬ Up-to-technique (F ∘ G)
∃[monotone×extensive×up-to]²×¬∘-up-to =
    lts
  , F
  , G
  , F-lemmas.mono
  , F-lemmas.ext
  , F-lemmas.up-to
  , G-lemmas.mono
  , G-lemmas.ext
  , G-lemmas.up-to
  , ¬-F∘G-up-to
  where
  open PQR

-- It is not the case that every monotone and extensive up-to
-- technique is size-preserving.

¬monotone×extensive×up-to→size-preserving :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ¬ (∀ {F} → Monotone F → Extensive F → Up-to-technique F →
             Size-preserving F)
¬monotone×extensive×up-to→size-preserving =
    lts
  , λ up-to→pres →
      ¬-F∘G-up-to $
      size-preserving→up-to $
      ∘-closure (up-to→pres F-lemmas.mono F-lemmas.ext F-lemmas.up-to)
                (up-to→pres G-lemmas.mono G-lemmas.ext G-lemmas.up-to)
  where
  open PQR

-- Up-to-technique is not closed under composition, not even for
-- monotone and extensive relation transformers.

¬-∘-closure :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ¬ ({F G : Trans₂ (# 0) Proc} →
     Monotone F → Extensive F →
     Monotone G → Extensive G →
     Up-to-technique F →
     Up-to-technique G →
     Up-to-technique (F ∘ G))
¬-∘-closure =
    lts
  , λ ∘-closure →
        ¬-F∘G-up-to (∘-closure F-lemmas.mono F-lemmas.ext
                               G-lemmas.mono G-lemmas.ext
                               F-lemmas.up-to G-lemmas.up-to)
  where
  open PQR

-- There are (at least two) monotone and extensive up-to techniques
-- that are not size-preserving.

∃monotone×extensive×up-to×¬size-preserving :
  ∃ λ (lts : LTS lzero) →
  let open Combination lts in
  ∃ λ (F : Trans₂ (# 0) Proc) →
  ∃ λ (G : Trans₂ (# 0) Proc) →
    Monotone F × Extensive F × Up-to-technique F × ¬ Size-preserving F ×
    Monotone G × Extensive G × Up-to-technique G × ¬ Size-preserving G ×
    F ≢ G
∃monotone×extensive×up-to×¬size-preserving =
    lts
  , F , G
  , F-lemmas.mono
  , F-lemmas.ext
  , F-lemmas.up-to
  , F-lemmas.¬-pres
  , G-lemmas.mono
  , G-lemmas.ext
  , G-lemmas.up-to
  , G-lemmas.¬-pres
  , F≢G
  where
  open PQR

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Classes where

record Plus {a} (A : Set a) : Set a where
  field
    _+_ : A → A → A

  infixl 6 _+_

open Plus {{...}} public

record Times {a} (A : Set a) : Set a where
  field
    {{plus}} : Plus A
    _*_ : A → A → A

  infixl 7 _*_

open Times {{...}} public

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


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

open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Sets.EquivalenceRelations
open import Rings.IntegralDomains.Definition

module Rings.IntegralDomains.Lemmas {m n : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open Setoid S
open Equivalence eq
open Ring R

cancelIntDom : {a b c : A} → (a * b) ∼ (a * c) → ((a ∼ (Ring.0R R)) → False) → (b ∼ c)
cancelIntDom {a} {b} {c} ab=ac a!=0 = transferToRight (Ring.additiveGroup R) t3
  where
    t1 : (a * b) + Group.inverse (Ring.additiveGroup R) (a * c) ∼ Ring.0R R
    t1 = transferToRight'' (Ring.additiveGroup R) ab=ac
    t2 : a * (b + Group.inverse (Ring.additiveGroup R) c) ∼ Ring.0R R
    t2 = transitive (transitive (Ring.*DistributesOver+ R) (Group.+WellDefined (Ring.additiveGroup R) reflexive (transferToRight' (Ring.additiveGroup R) (transitive (symmetric (Ring.*DistributesOver+ R)) (transitive (Ring.*WellDefined R reflexive (Group.invLeft (Ring.additiveGroup R))) (Ring.timesZero R)))))) t1
    t3 : (b + Group.inverse (Ring.additiveGroup R) c) ∼ Ring.0R R
    t3 = IntegralDomain.intDom I t2 a!=0

cancelIntDom' : {a b c : A} → (a * c) ∼ (b * c) → (c ∼ Ring.0R R → False) → a ∼ b
cancelIntDom' pr n = cancelIntDom (transitive *Commutative (transitive pr *Commutative)) n


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Reexport Data.List.All from the standard library.
--
-- At one point, we reinvented Data.List.All from the Agda
-- standard library, under the name dependent list. We later
-- replaced our reinvention by this adapter module that just
-- exports the standard library's version with partly different
-- names.
------------------------------------------------------------------------

module Base.Data.DependentList where

open import Data.List.All public
  using
    ( head
    ; tail
    ; map
    ; tabulate
    )
  renaming
    ( All to DependentList
    ; _∷_ to _•_
    ; [] to ∅
    )

-- Maps a binary function over two dependent lists.
-- Should this be in the Agda standard library?
zipWith : ∀ {a p q r} {A : Set a} {P : A → Set p} {Q : A → Set q} {R : A → Set r} →
  (f : {a : A} → P a → Q a → R a) →
  ∀ {xs} → DependentList P xs → DependentList Q xs → DependentList R xs
zipWith f ∅ ∅ = ∅
zipWith f (p • ps) (q • qs) = f p q • zipWith f ps qs


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Free.Properties (Σ : Signature) where

open import Level using (Level)
open import Function using (_∘_)

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Free.Base Σ
open import Fragment.Algebra.Free.Evaluation Σ
open import Fragment.Algebra.Free.Monad Σ
open import Fragment.Algebra.Homomorphism Σ
open import Fragment.Algebra.Quotient Σ

open import Fragment.Setoid.Morphism as M
  hiding (∣_∣; ∣_∣-cong; id; _≗_)

open import Data.Fin using (Fin)
open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Vec.Properties using (map-∘)
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
  using (Pointwise; Pointwise-≡⇒≡; []; _∷_)

import Relation.Binary.Reasoning.Setoid as Reasoning
open import Relation.Binary using (Setoid; Rel; IsEquivalence)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

private
  variable
    a b c ℓ₁ ℓ₂ ℓ₃ : Level

module _
  {A : Algebra {a} {ℓ₁}}
  (h : Free ∥ A ∥/≈ ⟿ A)
  (inj : ∣ h ∣⃗ · unit M.≗ M.id)
  where

  open Setoid ∥ A ∥/≈
  open Reasoning ∥ A ∥/≈

  mutual
    map-∣eval∣-universal : ∀ {n} {xs : Vec (Term ∥ A ∥) n}
                            → Pointwise (≈[ A ]) (map ∣ h ∣ xs)
                                                 (map ∣ eval A ∣ xs)
    map-∣eval∣-universal {_} {[]}     = []
    map-∣eval∣-universal {_} {x ∷ xs} =
      eval-universal {x} ∷ map-∣eval∣-universal {_} {xs}

    eval-universal : h ≗ eval A
    eval-universal {atom x}    = inj
    eval-universal {term f xs} = begin
        ∣ h ∣ (term f xs)
      ≈⟨ sym (∣ h ∣-hom f xs) ⟩
        A ⟦ f ⟧ (map ∣ h ∣ xs)
      ≈⟨ (A ⟦ f ⟧-cong) map-∣eval∣-universal ⟩
        A ⟦ f ⟧ (map ∣ eval A ∣ xs)
      ≈⟨ ∣ eval A ∣-hom f xs ⟩
        ∣ eval A ∣ (term f xs)
      ∎

module _
  {A : Setoid a ℓ₁}
  {B : Setoid b ℓ₂}
  (f : A ↝ Herbrand B)
  where

  bind-unitₗ : ∣ bind f ∣⃗ · unit M.≗ f
  bind-unitₗ = Setoid.refl (Herbrand B)

module _ {A : Setoid a ℓ₁} where

  open Setoid ∥ Free A ∥/≈
  open Reasoning ∥ Free A ∥/≈

  mutual
    map-∣bind∣-unitʳ : ∀ {n} → {xs : Vec ∥ Free A ∥ n}
                       → Pointwise ≈[ Free A ] (map ∣ bind {B = A} unit ∣ xs) xs
    map-∣bind∣-unitʳ {xs = []}     = []
    map-∣bind∣-unitʳ {xs = x ∷ xs} = bind-unitʳ ∷ map-∣bind∣-unitʳ

    bind-unitʳ : bind {B = A} unit ≗ id
    bind-unitʳ {atom _}    = Setoid.refl (Herbrand A)
    bind-unitʳ {term f xs} = begin
        ∣ bind {B = A} unit ∣ (term f xs)
      ≈⟨ sym (∣ bind unit ∣-hom f xs) ⟩
        term f (map ∣ bind {B = A} unit ∣ xs)
      ≈⟨ term map-∣bind∣-unitʳ ⟩
        term f xs
      ∎

module _
  {A : Setoid a ℓ₁}
  {B : Setoid b ℓ₂}
  {C : Setoid c ℓ₃}
  (g : B ↝ Herbrand C)
  (f : A ↝ Herbrand B)
  where

  open Setoid ∥ Free C ∥/≈
  open Reasoning ∥ Free C ∥/≈

  mutual
    map-∣bind∣-assoc : ∀ {n} → {xs : Vec ∥ Free A ∥ n}
                       → Pointwise (≈[ Free C ])
                                   (map (∣ bind g ∣ ∘ ∣ bind f ∣) xs)
                                   (map ∣ bind (∣ bind g ∣⃗ · f) ∣ xs)
    map-∣bind∣-assoc {xs = []}     = []
    map-∣bind∣-assoc {xs = x ∷ xs} = bind-assoc {x} ∷ map-∣bind∣-assoc

    bind-assoc : bind g ⊙ bind f ≗ bind (∣ bind g ∣⃗ · f)
    bind-assoc {atom _}     = refl
    bind-assoc {term op xs} = begin
        ∣ bind g ∣ (∣ bind f ∣ (term op xs))
      ≈⟨ sym (∣ bind g ∣-cong (∣ bind f ∣-hom op xs)) ⟩
        ∣ bind g ∣ (term op (map ∣ bind f ∣ xs))
      ≈⟨ sym (∣ bind g ∣-hom op (map ∣ bind f ∣ xs)) ⟩
        term op (map ∣ bind g ∣ (map ∣ bind f ∣ xs))
      ≈⟨ sym (term (PW.map reflexive (PW.≡⇒Pointwise-≡ (map-∘ ∣ bind g ∣ ∣ bind f ∣ xs)))) ⟩
        term op (map (∣ bind g ∣ ∘ ∣ bind f ∣) xs)
      ≈⟨ term map-∣bind∣-assoc ⟩
        term op (map ∣ bind (∣ bind g ∣⃗ · f) ∣ xs)
      ≈⟨ ∣ bind (∣ bind g ∣⃗ · f) ∣-hom op xs ⟩
        ∣ bind (∣ bind g ∣⃗ · f) ∣ (term op xs)
      ∎

fmap-id : ∀ {A : Setoid a ℓ₁} → fmap M.id ≗ id
fmap-id {A = A} = bind-unitʳ {A = A}

module _ {n}
  (A : Algebra {a} {ℓ₁})
  (θ : Env A n)
  where

  IsInstantiation : F n ⟿ A → Set _
  IsInstantiation f = ∀ x → ∣ f ∣ (atom (dyn x)) ≡ θ x

  inst-isInstantiation : IsInstantiation (inst A θ)
  inst-isInstantiation x = PE.refl

  mutual
    map-∣inst∣-universal : ∀ {h m} → IsInstantiation h
                           → {xs : Vec ∥ F n ∥ m}
                           → Pointwise ≈[ A ] (map ∣ h ∣ xs)
                                              (map ∣ inst A θ ∣ xs)
    map-∣inst∣-universal p {xs = []}             = []
    map-∣inst∣-universal {h = h} p {xs = x ∷ xs} =
      inst-universal {h = h} p ∷ map-∣inst∣-universal {h = h} p

    inst-universal : ∀ {h} → IsInstantiation h → h ≗ (inst A θ)
    inst-universal {h} p {x = atom (dyn x)} = Setoid.reflexive ∥ A ∥/≈ (p x)
    inst-universal {h} p {x = term f xs}    = begin
        ∣ h ∣ (term f xs)
      ≈⟨ Setoid.sym ∥ A ∥/≈ (∣ h ∣-hom f xs) ⟩
        A ⟦ f ⟧ (map ∣ h ∣ xs)
      ≈⟨ (A ⟦ f ⟧-cong) (map-∣inst∣-universal {h = h} p {xs = xs}) ⟩
        A ⟦ f ⟧ (map ∣ inst A θ ∣ xs)
      ≈⟨ ∣ inst A θ ∣-hom f xs ⟩
        ∣ inst A θ ∣ (term f xs)
      ∎
      where open Reasoning ∥ A ∥/≈

  module _
    {B : Algebra {b} {ℓ₂}}
    (h : A ⟿ B)
    where

    mutual
      map-∣inst∣-assoc : ∀ {m} {xs : Vec ∥ F n ∥ m}
                       → Pointwise ≈[ B ]
                                   (map ∣ h ⊙ inst A θ ∣ xs)
                                   (map ∣ inst B (∣ h ∣ ∘ θ) ∣ xs)
      map-∣inst∣-assoc {xs = []}     = []
      map-∣inst∣-assoc {xs = x ∷ xs} = inst-assoc {x = x} ∷ map-∣inst∣-assoc

      inst-assoc : h ⊙ inst A θ ≗ inst B (∣ h ∣ ∘ θ)
      inst-assoc {atom (dyn _)} = Setoid.refl ∥ B ∥/≈
      inst-assoc {term f xs}    = begin
          ∣ h ⊙ inst A θ ∣ (term f xs)
        ≈⟨ sym (∣ h ⊙ inst A θ ∣-hom f xs) ⟩
          B ⟦ f ⟧ (map ∣ h ⊙ inst A θ ∣ xs)
        ≈⟨ (B ⟦ f ⟧-cong) map-∣inst∣-assoc ⟩
          B ⟦ f ⟧ (map ∣ inst B (∣ h ∣ ∘ θ) ∣ xs)
        ≈⟨ ∣ inst B (∣ h ∣ ∘ θ) ∣-hom f xs ⟩
          ∣ inst B (∣ h ∣ ∘ θ) ∣ (term f xs)
        ∎
        where open Setoid ∥ B ∥/≈
              open Reasoning ∥ B ∥/≈

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --copatterns #-}

module Issue906 where

{- Globular types as a coinductive record -}
record Glob : Set1 where
  coinductive
  field
    Ob : Set
    Hom : (a b : Ob) → Glob
open Glob public

record Unit : Set where

data _==_ {A : Set} (a : A) : A → Set where
  refl : a == a

{- The terminal globular type -}
Unit-glob : Glob
Ob Unit-glob = Unit
Hom Unit-glob _ _ = Unit-glob

{- The tower of identity types -}
Id-glob : (A : Set) → Glob
Ob (Id-glob A) = A
Hom (Id-glob A) a b = Id-glob (a == b)

-- should termination check

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where

variable
  A  : Set
  x  : A
  n  : Nat
  xs : Vec A n

postulate
  IsHead : A → Vec A (suc n) → Set

-- The `n` should be generalized over since the generalizable n in the type of xs
-- is solved with suc n.
foo : IsHead {n = _} x xs → Nat
foo h = 0

check-foo : {A : Set} {x : A} {n : Nat} {xs : Vec A (suc n)} → IsHead x xs → Nat
check-foo = foo

-- Should work also if the meta is created in an extended context
bar : (X : Set) → IsHead x xs → Nat
bar X h = 0

check-bar : {A : Set} {x : A} {n : Nat} {xs : Vec A (suc n)} → (X : Set) → IsHead x xs → Nat
check-bar = bar


text:
module Pi-.Interp where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Pi-.Syntax
open import Pi-.Opsem
open import Pi-.Eval

{-# TERMINATING #-}
mutual
  interp : {A B : 𝕌} → (A ↔ B) → Val A B → Val B A
  -- Forward
  interp unite₊l (inj₂ y ⃗)        = y ⃗
  interp uniti₊l (v ⃗)             = inj₂ v ⃗
  interp swap₊   (inj₁ x ⃗)        = inj₂ x ⃗
  interp swap₊   (inj₂ y ⃗)        = inj₁ y ⃗
  interp assocl₊ (inj₁ x ⃗)        = inj₁ (inj₁ x) ⃗
  interp assocl₊ (inj₂ (inj₁ y) ⃗) = inj₁ (inj₂ y) ⃗
  interp assocl₊ (inj₂ (inj₂ z) ⃗) = inj₂ z ⃗
  interp assocr₊ (inj₁ (inj₁ x) ⃗) = inj₁ x ⃗
  interp assocr₊ (inj₁ (inj₂ y) ⃗) = inj₂ (inj₁ y) ⃗
  interp assocr₊ (inj₂ z ⃗)        = inj₂ (inj₂ z) ⃗
  interp unite⋆l ((tt , v) ⃗)      = v ⃗
  interp uniti⋆l (v ⃗)             = (tt , v) ⃗
  interp swap⋆   ((x , y) ⃗)       = (y , x) ⃗
  interp assocl⋆ ((x , (y , z)) ⃗) = ((x , y) , z) ⃗
  interp assocr⋆ (((x , y) , z) ⃗) = (x , y , z) ⃗
  interp dist    ((inj₁ x , z) ⃗)  = inj₁ (x , z) ⃗
  interp dist    ((inj₂ y , z) ⃗)  = inj₂ (y , z) ⃗
  interp factor  (inj₁ (x , z) ⃗)  = (inj₁ x , z) ⃗
  interp factor  (inj₂ (y , z) ⃗)  = (inj₂ y , z) ⃗
  interp id↔     (v ⃗)             = v ⃗
  interp (c₁ ⨾ c₂) (v ⃗) with interp c₁ (v ⃗)
  interp (c₁ ⨾ c₂) (v ⃗) | (v' ⃖) = v' ⃖
  interp (c₁ ⨾ c₂) (v ⃗) | (v' ⃗) = c₁ ⨾[ v' ⃗]⨾ c₂
  interp (c₁ ⊕ c₂) (inj₁ x ⃗) with interp c₁ (x ⃗)
  interp (c₁ ⊕ c₂) (inj₁ x ⃗) | (x' ⃗) = inj₁ x' ⃗
  interp (c₁ ⊕ c₂) (inj₁ x ⃗) | (x' ⃖) = inj₁ x' ⃖
  interp (c₁ ⊕ c₂) (inj₂ y ⃗) with interp c₂ (y ⃗)
  interp (c₁ ⊕ c₂) (inj₂ y ⃗) | (y' ⃗) = inj₂ y' ⃗
  interp (c₁ ⊕ c₂) (inj₂ y ⃗) | (y' ⃖) = inj₂ y' ⃖
  interp (c₁ ⊗ c₂) ((x , y) ⃗) with interp c₁ (x ⃗)
  interp (c₁ ⊗ c₂) ((x , y) ⃗) | (x' ⃖) = (x' , y) ⃖
  interp (c₁ ⊗ c₂) ((x , y) ⃗) | (x' ⃗) with interp c₂ (y ⃗)
  interp (c₁ ⊗ c₂) ((x , y) ⃗) | (x' ⃗) | (y' ⃗) = (x' , y') ⃗
  interp (c₁ ⊗ c₂) ((x , y) ⃗) | (x' ⃗) | (y' ⃖) = (x , y') ⃖
  interp ε₊ (inj₁ v ⃗)     = inj₂ (- v) ⃖
  interp ε₊ (inj₂ (- v) ⃗) = inj₁ v ⃖
  -- Backward
  interp unite₊l (v ⃖)             = inj₂ v ⃖
  interp uniti₊l (inj₂ v ⃖)        = v ⃖
  interp swap₊   (inj₁ x ⃖)        = inj₂ x ⃖
  interp swap₊   (inj₂ y ⃖)        = inj₁ y ⃖
  interp assocl₊ (inj₁ (inj₁ x) ⃖) = inj₁ x ⃖
  interp assocl₊ (inj₁ (inj₂ y) ⃖) = inj₂ (inj₁ y) ⃖
  interp assocl₊ (inj₂ z ⃖)        = inj₂ (inj₂ z) ⃖
  interp assocr₊ (inj₁ x ⃖)        = inj₁ (inj₁ x) ⃖
  interp assocr₊ (inj₂ (inj₁ y) ⃖) = inj₁ (inj₂ y) ⃖
  interp assocr₊ (inj₂ (inj₂ z) ⃖) = inj₂ z ⃖
  interp unite⋆l (v ⃖)             = (tt , v) ⃖
  interp uniti⋆l ((tt , v) ⃖)      = v ⃖
  interp swap⋆   ((x , y) ⃖)       = (y , x) ⃖
  interp assocl⋆ (((x , y) , z) ⃖) = (x , (y , z)) ⃖
  interp assocr⋆ ((x , (y , z)) ⃖) = ((x , y) , z) ⃖
  interp dist    (inj₁ (x , z) ⃖)  = (inj₁ x , z) ⃖
  interp dist    (inj₂ (y , z) ⃖)  = (inj₂ y , z) ⃖
  interp factor  ((inj₁ x , z) ⃖)  = inj₁ (x , z) ⃖
  interp factor  ((inj₂ y , z) ⃖)  = inj₂ (y , z) ⃖
  interp id↔ (v ⃖) = v ⃖
  interp (c₁ ⨾ c₂) (v ⃖) with interp c₂ (v ⃖)
  interp (c₁ ⨾ c₂) (v ⃖) | v' ⃗ = v' ⃗
  interp (c₁ ⨾ c₂) (v ⃖) | v' ⃖ = c₁ ⨾[ v' ⃖]⨾ c₂
  interp (c₁ ⊕ c₂) (inj₁ x ⃖) with interp c₁ (x ⃖)
  interp (c₁ ⊕ c₂) (inj₁ x ⃖) | (x' ⃖) = inj₁ x' ⃖
  interp (c₁ ⊕ c₂) (inj₁ x ⃖) | (x' ⃗) = inj₁ x' ⃗
  interp (c₁ ⊕ c₂) (inj₂ y ⃖) with interp c₂ (y ⃖)
  interp (c₁ ⊕ c₂) (inj₂ y ⃖) | (y' ⃖) = inj₂ y' ⃖
  interp (c₁ ⊕ c₂) (inj₂ y ⃖) | (y' ⃗) = inj₂ y' ⃗
  interp (c₁ ⊗ c₂) ((x , y) ⃖) with interp c₂ (y ⃖)
  interp (c₁ ⊗ c₂) ((x , y) ⃖) | (y' ⃗) = (x , y') ⃗
  interp (c₁ ⊗ c₂) ((x , y) ⃖) | (y' ⃖) with interp c₁ (x ⃖)
  interp (c₁ ⊗ c₂) ((x , y) ⃖) | (y' ⃖) | (x' ⃖) = (x' , y') ⃖
  interp (c₁ ⊗ c₂) ((x , y) ⃖) | (y' ⃖) | (x' ⃗) = (x' , y) ⃗
  interp η₊ (inj₁ v ⃖)     = inj₂ (- v) ⃗
  interp η₊ (inj₂ (- v) ⃖) = inj₁ v ⃗

  _⨾[_⃗]⨾_ : ∀ {A B C} → (A ↔ B) → ⟦ B ⟧ → (B ↔ C) → Val C A
  c₁ ⨾[ b ⃗]⨾ c₂ with interp c₂ (b ⃗)
  c₁ ⨾[ b ⃗]⨾ c₂ | c ⃗ = c ⃗
  c₁ ⨾[ b ⃗]⨾ c₂ | b' ⃖ = c₁ ⨾[ b' ⃖]⨾ c₂

  _⨾[_⃖]⨾_ : ∀ {A B C} → (A ↔ B) → ⟦ B ⟧ → (B ↔ C) → Val C A
  c₁ ⨾[ b ⃖]⨾ c₂ with interp c₁ (b ⃖)
  c₁ ⨾[ b ⃖]⨾ c₂ | a ⃖ = a ⃖
  c₁ ⨾[ b ⃖]⨾ c₂ | b' ⃗ = c₁ ⨾[ b' ⃗]⨾ c₂


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

module Dodo.Unary where

open import Dodo.Unary.Dec public
open import Dodo.Unary.Disjoint public
open import Dodo.Unary.Empty public
open import Dodo.Unary.Equality public
open import Dodo.Unary.Intersection public
open import Dodo.Unary.Union public
open import Dodo.Unary.Unique public
open import Dodo.Unary.XOpt public

open ⊆₁-Reasoning public
open ⇔₁-Reasoning public

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
module Properties.Dec where

open import Properties.Contradiction using (¬)

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

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


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

-- 2014-05-27 Jesper and Andreas

postulate
  A B : Set
  R   : A → B → Set

{-# BUILTIN REWRITE R #-}

-- Expected error:
-- R  does not have the right type for a rewriting relation
-- because the types of the last two arguments are different
-- when checking the pragma BUILTIN REWRITE R


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

open import HoTT
open import homotopy.JoinComm
open import homotopy.JoinAssocCubical

module homotopy.JoinSusp where

module _ {i} (A : Type i) where

  private

      module Into = JoinRec {A = Bool} {B = A}
        {C = Susp A}
        (Bool-rec north south)
        (λ _ → south)
        (λ {true a → merid a;
            false a → idp})

      into = Into.f

      module Out = SuspRec {C = Bool * A}
        (left true)
        (left false)
        (λ a → jglue true a ∙ ! (jglue false a))

      out = Out.f

      into-out : ∀ σ → into (out σ) == σ
      into-out = Susp-elim
        idp
        idp
        (λ a → ↓-∘=idf-from-square into out $ vert-degen-square $
           ap (ap into) (Out.merid-β a)
           ∙ ap-∙ into (jglue true a) (! (jglue false a))
           ∙ (Into.glue-β true a
              ∙2 (ap-! into (jglue false a)
                  ∙ ap ! (Into.glue-β false a)))
           ∙ ∙-unit-r _)

      out-into : ∀ j → out (into j) == j
      out-into = Join-elim
        (Bool-elim idp idp)
        (λ a → jglue false a)
        (λ{true a → ↓-∘=idf-from-square out into $
              (ap (ap out) (Into.glue-β true a) ∙ Out.merid-β a)
              ∙v⊡ (vid-square {p = jglue true a}
                    ⊡h rt-square (jglue false a))
              ⊡v∙ ∙-unit-r _;
           false a → ↓-∘=idf-from-square out into $
             ap (ap out) (Into.glue-β false a) ∙v⊡ connection})

  *-Bool-l : Bool * A ≃ Susp A
  *-Bool-l = equiv into out into-out out-into

module _ {i} (X : Ptd i) where

  ⊙*-Bool-l : ⊙Bool ⊙* X ⊙≃ ⊙Susp X
  ⊙*-Bool-l = ≃-to-⊙≃ (*-Bool-l (de⊙ X)) idp

module _ {i j} (A : Type i) (B : Type j) where

  *-Susp-l : Susp A * B ≃ Susp (A * B)
  *-Susp-l = *-Bool-l (A * B) ∘e *-assoc Bool A B ∘e *-emap (*-Bool-l A) (ide B) ⁻¹

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙*-Susp-l : ⊙Susp X ⊙* Y ⊙≃ ⊙Susp (X ⊙* Y)
  ⊙*-Susp-l = ≃-to-⊙≃ (*-Susp-l (de⊙ X) (de⊙ Y)) idp

module _ {i} where

  ⊙*-Sphere-l : (m : ℕ) (X : Ptd i) → ⊙Sphere m ⊙* X ⊙≃ ⊙Susp^ (S m) X
  ⊙*-Sphere-l O X = ⊙*-Bool-l X
  ⊙*-Sphere-l (S m) X = ⊙Susp-emap (⊙*-Sphere-l m X) ⊙∘e ⊙*-Susp-l (⊙Sphere m) X

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda