text:
-- The Agda primitives (preloaded).

{-# OPTIONS --without-K --no-subtyping --no-import-sorts #-}

module Agda.Primitive where

------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

infixl 6 _⊔_

{-# BUILTIN TYPE Set #-}
{-# BUILTIN PROP Prop #-}
{-# BUILTIN SETOMEGA Setω #-}

-- Level is the first thing we need to define.
-- The other postulates can only be checked if built-in Level is known.

postulate
  Level : Set

-- MAlonzo compiles Level to (). This should be safe, because it is
-- not possible to pattern match on levels.

{-# BUILTIN LEVEL Level #-}

postulate
  lzero : Level
  lsuc  : (ℓ : Level) → Level
  _⊔_   : (ℓ₁ ℓ₂ : Level) → Level

{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC  lsuc  #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

max_stars_repo_name: mdimjasevic/agda

max_issues_repo_name: mdimjasevic/agda

max_forks_repo_name: mdimjasevic/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed unary relations
------------------------------------------------------------------------

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

module Relation.Unary.Indexed  where

open import Data.Product using (∃; _×_)
open import Level
open import Relation.Nullary using (¬_)

IPred : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
IPred A ℓ = ∀ {i} → A i → Set ℓ

module _ {i a} {I : Set i} {A : I → Set a} where

  _∈_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
  x ∈ P = ∀ i → P (x i)

  _∉_ : ∀ {ℓ} → (∀ i → A i) → IPred A ℓ → Set _
  t ∉ P = ¬ (t ∈ P)

ext: agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.Group
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.groups.Homomorphisms

module lib.groups.PropSubgroup where

module _ {i} (G : Group i) where

  private
    module G = Group G

  module PropSubgroup {j} (P : G.El → Type j)
    (P-level : ∀ g → has-level -1 (P g))
    (P-ident : P G.ident) (P-inv : ∀ {g} → P g → P (G.inv g))
    (P-comp : ∀ {g₁ g₂} → P g₁ → P g₂ → P (G.comp g₁ g₂)) where

    struct : GroupStructure (Σ G.El P)
    struct = record {
      ident = (G.ident , P-ident);
      inv = λ {(g , p) → (G.inv g , P-inv p)};
      comp = λ {(g₁ , p₁) (g₂ , p₂) → (G.comp g₁ g₂ , P-comp p₁ p₂)};
      unitl = λ {(g , _) →
        pair= (G.unitl g) (prop-has-all-paths-↓ (P-level _))};
      unitr = λ {(g , _) →
        pair= (G.unitr g) (prop-has-all-paths-↓ (P-level _))};
      assoc = λ {(g₁ , _) (g₂ , _) (g₃ , _) →
        pair= (G.assoc g₁ g₂ g₃) (prop-has-all-paths-↓ (P-level _))};
      invl = λ {(g , _) →
        pair= (G.invl g) (prop-has-all-paths-↓ (P-level _))};
      invr = λ {(g , _) →
        pair= (G.invr g) (prop-has-all-paths-↓ (P-level _))}}

    Subgroup : Group (lmax i j)
    Subgroup = group _ (Σ-level G.El-level (raise-level _ ∘ P-level)) struct

    inj : Subgroup →ᴳ G
    inj = record {
      f = λ {(g , _) → g};
      pres-comp = λ _ _ → idp}

    module _ {j} {H : Group j} (φ : H →ᴳ G) where

      private
        module H = Group H
        module φ = GroupHom φ

      prop-hom : Π H.El (P ∘ φ.f) → (H →ᴳ Subgroup)
      prop-hom p = record {
        f = λ g → (φ.f g , p g);
        pres-comp = λ g₁ g₂ →
          pair= (φ.pres-comp g₁ g₂) (prop-has-all-paths-↓ (P-level _))}

module _ {i} {j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where

  private
    module G = Group G
    module H = Group H
    module φ = GroupHom φ

    module Ker = PropSubgroup G (λ g → φ.f g == H.ident)
      (λ g → H.El-level _ _) φ.pres-ident
      (λ p → φ.pres-inv _ ∙ ap H.inv p ∙ group-inv-ident H)
      (λ p₁ p₂ → φ.pres-comp _ _ ∙ ap2 H.comp p₁ p₂ ∙ H.unitl _)

    module Im = PropSubgroup H (λ h → Trunc -1 (Σ G.El (λ g → φ.f g == h)))
      (λ h → Trunc-level) ([ G.ident , φ.pres-ident ])
      (Trunc-fmap (λ {(g , p) →
        (G.inv g , φ.pres-inv g ∙ ap H.inv p)}))
      (Trunc-fmap2 (λ {(g₁ , p₁) (g₂ , p₂) →
        (G.comp g₁ g₂ , φ.pres-comp g₁ g₂ ∙ ap2 H.comp p₁ p₂)}))

  open Ker public renaming
    (struct to ker-struct; Subgroup to Ker;
     inj to ker-inj; prop-hom to ker-hom)

  open Im public renaming
    (struct to im-struct; Subgroup to Im;
     inj to im-inj; prop-hom to im-out-hom)

  im-in-hom : G →ᴳ Im
  im-in-hom = record {
    f = λ g → (φ.f g , [ g , idp ]);
    pres-comp = λ g₁ g₂ →
      pair= (φ.pres-comp g₁ g₂) (prop-has-all-paths-↓ Trunc-level)}

  im-in-surj : (h : Group.El Im)
    → Trunc -1 (Σ G.El (λ g → GroupHom.f im-in-hom g == h))
  im-in-surj (_ , s) = Trunc-fmap (λ {(g , p) →
    (g , pair= p (prop-has-all-paths-↓ Trunc-level))}) s

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Naturals | Nat

type
  N : 0-ary

term
  ze   : N
  su   : N  ->  N
  nrec : N  α  (α,N).α  ->  α

theory
  (zeβ) z : α   s : (α,N).α        |> nrec (ze,       z, r m. s[r,m]) = z
  (suβ) z : α   s : (α,N).α  n : N |> nrec (su (n), z, r m. s[r,m]) = s[nrec (n, z, r m. s[r,m]), n]
-}

module Naturals.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Naturals.Signature
open import Naturals.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution Nat:Syn
open import SOAS.Metatheory.SecondOrder.Equality Nat:Syn

private
  variable
    α β γ τ : NatT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ Nat) α Γ → (𝔐 ▷ Nat) α Γ → Set where
  zeβ : ⁅ α ⁆ ⁅ α · N ⊩ α ⁆̣       ▹ ∅ ⊢     nrec ze 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩) ≋ₐ 𝔞
  suβ : ⁅ α ⁆ ⁅ α · N ⊩ α ⁆ ⁅ N ⁆̣ ▹ ∅ ⊢ nrec (su 𝔠) 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩) ≋ₐ 𝔟⟨ (nrec 𝔠 𝔞 (𝔟⟨ x₀ ◂ x₁ ⟩)) ◂ 𝔠 ⟩

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module DuplicateBuiltinBinding where

postulate Int : Set

{-# BUILTIN INTEGER Int #-}
{-# BUILTIN INTEGER Int #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module HiddenLambda where

postulate
  A : Set
  T : A -> Set

H : Set
H = {x : A} -> T x -> T x

-- H doesn't reduce when checking the body of h
h : H
h = \tx -> tx

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
import Lvl

-- TODO: Just testing how it goes with creating an axiomatic system
module Geometry.Test3 (Point : Set(Lvl.𝟎)) where

open import Functional
open import Logic.Propositional{Lvl.𝟎}
open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎} renaming (_≡_ to _≡ₚ_ ; _≢_ to _≢ₚ_)
open import Sets.PredicateSet
open import Sets.PredicateSet.Proofs
open import Structure.Relator.Equivalence{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Relator.Ordering{Lvl.𝟎}{Lvl.𝟎}

-- A line of infinite length
record Line : Set(Lvl.𝟎) where
  constructor line
  field
    a : Point
    b : Point

  field
    different : (a ≢ₚ b)

-- A circle
record Circle : Set(Lvl.𝟎) where
  constructor circle
  field
    middle : Point
    outer : Point

record Theory : Set(Lvl.𝐒(Lvl.𝐒(Lvl.𝟎))) where
  -- Symbols
  field
    -- CirclesIntersectionPoint : Circle → Circle → Point → Set(Lvl.𝟎)
    _∈ᶜ_ : Point → Circle → Stmt
    _∈ˡ_ : Point → Line → Stmt

    -- circleIntersectionPoint : (a : Circle) → (b : Circle) → ⦃ _ : CircleIntersect a b ⦄ → Point

  CircleBoundary : Circle → Point → Stmt
  CircleBoundary c p = (p ∈ᶜ c) ∧ (∀{outer a : Point} → (a ∈ᶜ circle p outer) → ⊥)

  LineIntersection : Line → Line → Point → Stmt
  LineIntersection a b p = (p ∈ˡ a) ∧ (p ∈ˡ b)

  -- Axioms
  -- field
  --   circle-boundary-eq : ∀{a b} → ((_∈ᶜ a) ≡ (_∈ᶜ b)) ↔ (CircleBoundaryPoint a ≡ᵖ CircleBoundaryPoint b)
  --   circle-either : ∀{middle outer₁ outer₂} → ((_∈ᶜ circle middle outer₁) ⊆ (_∈ᶜ circle middle outer₂)) ∨ ((_∈ᶜ circle middle outer₂) ⊆ (_∈ᶜ circle middle outer₁))
    -- circleOuterIs Circle.outer

module Theorems ⦃ _ : Theory ⦄ where
  open Theory ⦃ ... ⦄

  -- perpendicularLine : CirclesIntersectionPoint

  -- middlepoint : Line → Point
  -- middlepoint(line(a)(b)) =

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An either-or-both data type, basic type and operations
------------------------------------------------------------------------

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

module Data.These.Base where

open import Level
open import Data.Sum.Base using (_⊎_; [_,_]′)
open import Function.Base

private
  variable
    a b c d e f : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e
    F : Set f

data These {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  this  : A     → These A B
  that  :     B → These A B
  these : A → B → These A B

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

-- injection

fromSum : A ⊎ B → These A B
fromSum = [ this , that ]′

-- map

map : (f : A → B) (g : C → D) → These A C → These B D
map f g (this a)    = this (f a)
map f g (that b)    = that (g b)
map f g (these a b) = these (f a) (g b)

map₁ : (f : A → B) → These A C → These B C
map₁ f = map f id

map₂ : (g : B → C) → These A B → These A C
map₂ = map id

-- fold

fold : (A → C) → (B → C) → (A → B → C) → These A B → C
fold l r lr (this a)    = l a
fold l r lr (that b)    = r b
fold l r lr (these a b) = lr a b

foldWithDefaults : A → B → (A → B → C) → These A B → C
foldWithDefaults a b lr = fold (flip lr b) (lr a) lr

-- swap

swap : These A B → These B A
swap = fold that this (flip these)

-- align

alignWith : (These A C → E) → (These B D → F) → These A B → These C D → These E F
alignWith f g (this a)    (this c)    = this (f (these a c))
alignWith f g (this a)    (that d)    = these (f (this a)) (g (that d))
alignWith f g (this a)    (these c d) = these (f (these a c)) (g (that d))
alignWith f g (that b)    (this c)    = these (f (that c)) (g (this b))
alignWith f g (that b)    (that d)    = that (g (these b d))
alignWith f g (that b)    (these c d) = these (f (that c)) (g (these b d))
alignWith f g (these a b) (this c)    = these (f (these a c)) (g (this b))
alignWith f g (these a b) (that d)    = these (f (this a)) (g (these b d))
alignWith f g (these a b) (these c d) = these (f (these a c)) (g (these b d))

align : These A B → These C D → These (These A C) (These B D)
align = alignWith id id


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

   Copyright (c) 2020, 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 Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Concrete.System
open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})

-- This module contains placeholders for the future analog of the
-- corresponding VotesOnce property.  Defining the implementation
-- obligation and proving that it is an invariant of an implementation
-- is a substantial undertaking.  We are working first on proving the
-- simpler VotesOnce property to settle down the structural aspects
-- before tackling the harder semantic issues.
module LibraBFT.Concrete.Properties.PreferredRound where
 -- TODO-3: define the implementation obligation
 ImplObligation₁ : Set
 ImplObligation₁ = Unit

 -- Next, we prove that given the necessary obligations,
 module Proof
   (sps-corr : StepPeerState-AllValidParts)
   (Impl-PR1 : ImplObligation₁)
   where
  -- Any reachable state satisfies the PR rule for any epoch in the system.
  module _ (st : SystemState)(r : ReachableSystemState st)(𝓔 : EpochConfig) where
   -- Bring in 'unwind', 'ext-unforgeability' and friends
   open Structural sps-corr
   -- Bring in IntSystemState
   open WithSPS sps-corr
   open        PerState st r
   open        PerEpoch 𝓔
   open import LibraBFT.Concrete.Obligations.PreferredRound 𝓔 (ConcreteVoteEvidence 𝓔) as PR

   postulate  -- TODO-3: prove it
     prr : PR.Type IntSystemState

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

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

{-# BUILTIN REWRITE _≡_ #-}

record R : Set₁ where
  constructor c
  field unD : Set

open R

id : unD (c (Nat → Nat))
id x = x

postulate rew : c (Nat → Nat) ≡ c (Nat → Bool)
{-# REWRITE rew #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Data.Nat using ( ℕ ; zero ; suc )
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; _≢_ ; refl ; cong )
open import Relation.Nullary using ( ¬_ )
open import FRP.LTL.Time using
  ( Time ; _<_ ; _≤_ ; _≥_ ; ≤-refl ; _≤-trans_ ; _≤-asym_ ; _≤-total_ ; ≤-proof-irrel ; ≡-impl-≥
  ; _∸_ ; _+_ ; t≤u+t∸u ; +-unit ; +-assoc ; +-resp-≤ ; <-impl-+1≤ ; t<t+1
  ; _≤-case_ ; lt ; eq ; gt )
open import FRP.LTL.Util using ( ⊥-elim )

module FRP.LTL.Time.Bound where

infixr 2 _≼_ _≺_ _⋠_
infixr 4 _,_
infixr 5 _≼-trans_ _≼-asym_ _≼-total_ _≺-transˡ_ _≺-transʳ_ _≺-trans_

-- Time bounds, which extend Time with least and greatest elements

data Time∞ : Set where
  +∞ : Time∞
  fin : Time → Time∞

-- Order on time, generated by s ≺ t ≺ +∞ when s < t

data _≼_ : Time∞ → Time∞ → Set where
  +∞-top : ∀ {t} → (t ≼ +∞)
  ≤-impl-≼ : ∀ {t u} → (t ≤ u) → (fin t ≼ fin u)

_⋠_ : Time∞ → Time∞ → Set
s ⋠ t = ¬(s ≼ t)

_≺_ : Time∞ → Time∞ → Set
s ≺ t = (s ≼ t) × (t ⋠ s)

≼-impl-≤ : ∀ {t u} → (fin t ≼ fin u) → (t ≤ u)
≼-impl-≤ (≤-impl-≼ t≤u) = t≤u

-- Axioms for ≺

t≺+∞ : ∀ {t} → fin t ≺ +∞
t≺+∞ = (+∞-top , λ ())

<-impl-≺ : ∀ {t u} → (t < u) → (fin t ≺ fin u)
<-impl-≺ (t≤u , u≰t) = (≤-impl-≼ t≤u , λ u≼t → u≰t (≼-impl-≤ u≼t))

≺-impl-< : ∀ {t u} → (fin t ≺ fin u) → (t < u)
≺-impl-< (t≼u , u⋠t) = (≼-impl-≤ t≼u , λ u≤t → u⋠t (≤-impl-≼ u≤t))

t≺t+1 : ∀ {t} → (fin t ≺ fin (t + 1))
t≺t+1 = <-impl-≺ t<t+1

-- ≼ is a decidable total order

≼-refl : ∀ {t} → (t ≼ t)
≼-refl {+∞}     = +∞-top
≼-refl {fin t} = ≤-impl-≼ ≤-refl

_≼-trans_ : ∀ {s t u} → (s ≼ t) → (t ≼ u) → (s ≼ u)
s≼t          ≼-trans +∞-top       = +∞-top
≤-impl-≼ s≤t ≼-trans ≤-impl-≼ t≤u = ≤-impl-≼ (s≤t ≤-trans t≤u)

_≼-asym_ : ∀ {s t} → (s ≼ t) → (t ≼ s) → (s ≡ t)
+∞-top       ≼-asym +∞-top       = refl
≤-impl-≼ s≤t ≼-asym ≤-impl-≼ t≤s = cong fin (s≤t ≤-asym t≤s)

_≼-total_ : ∀ s t → (s ≼ t) ⊎ (t ≺ s)
+∞    ≼-total +∞    = inj₁ +∞-top
+∞    ≼-total fin t = inj₂ t≺+∞
fin s ≼-total +∞    = inj₁ +∞-top
fin s ≼-total fin t with s ≤-total t
... | inj₁ s≤t = inj₁ (≤-impl-≼ s≤t)
... | inj₂ t<s = inj₂ (<-impl-≺ t<s)

data _≼-Case_ (t u : Time∞) : Set where
  lt : .(t ≺ u) → (t ≼-Case u)
  eq : .(t ≡ u) → (t ≼-Case u)
  gt : .(u ≺ t) → (t ≼-Case u)

_≼-case_ : ∀ t u → (t ≼-Case u)
+∞    ≼-case +∞    = eq refl
+∞    ≼-case fin u = gt t≺+∞
fin t ≼-case +∞    = lt t≺+∞
fin t ≼-case fin u with t ≤-case u
fin t ≼-case fin u | lt t<u = lt (<-impl-≺ t<u)
fin t ≼-case fin u | eq t≡u = eq (cong fin t≡u)
fin t ≼-case fin u | gt t>u = gt (<-impl-≺ t>u)

≡-impl-≼ : ∀ {s t} → (s ≡ t) → (s ≼ t)
≡-impl-≼ refl = ≼-refl

≡-impl-≽ : ∀ {s t} → (s ≡ t) → (t ≼ s)
≡-impl-≽ refl = ≼-refl

≼-proof-irrel : ∀ {t u} → (p q : t ≼ u) → (p ≡ q)
≼-proof-irrel +∞-top          +∞-top          = refl
≼-proof-irrel (≤-impl-≼ t≤₁u) (≤-impl-≼ t≤₂u) = cong ≤-impl-≼ (≤-proof-irrel t≤₁u t≤₂u)

≺-impl-≼ : ∀ {t u} → (t ≺ u) → (t ≼ u)
≺-impl-≼ (t≼u , u⋠t) = t≼u

≺-impl-⋡ : ∀ {t u} → (t ≺ u) → (u ⋠ t)
≺-impl-⋡ (t≼u , u⋠t) = u⋠t

≺-impl-≢ : ∀ {t u} → (t ≺ u) → (t ≢ u)
≺-impl-≢ (t≼u , u⋠t) refl = u⋠t ≼-refl

_≺-transˡ_ : ∀ {t u v} → (t ≺ u) → (u ≼ v) → (t ≺ v)
(t≼u , u⋠t) ≺-transˡ u≼v = (t≼u ≼-trans u≼v , λ v≼t → u⋠t (u≼v ≼-trans v≼t))

_≺-transʳ_ : ∀ {t u v} → (t ≼ u) → (u ≺ v) → (t ≺ v)
t≼u ≺-transʳ (u≼v , v⋠u) = (t≼u ≼-trans u≼v , λ v≼t → v⋠u (v≼t ≼-trans t≼u))

_≺-trans_ : ∀ {t u v} → (t ≺ u) → (u ≺ v) → (t ≺ v)
(t≼u , u⋠t) ≺-trans (u≼v , v⋠u) = (t≼u ≼-trans u≼v , λ v≼t → v⋠u (v≼t ≼-trans t≼u))

∞≼-impl-≡∞ : ∀ {t} → (+∞ ≼ t) → (t ≡ +∞)
∞≼-impl-≡∞ +∞-top = refl

src : ∀ {s t} → .(s ≼ t) → Time∞
src {s} {t} s≼t = s

tgt : ∀ {s t} → .(s ≼ t) → Time∞
tgt {s} {t} s≼t = t

-- An induction scheme for time bounds

_+_≻_ : Time∞ → ℕ → Time∞ → Set
s + zero  ≻ u = u ≺ s
s + suc n ≻ u = ∀ {t} → (s ≺ t) → (t + n ≻ u)

data ≺-Indn (s u : Time∞) : Set where
  _,_ : ∀ n → .(s + n ≻ u) → ≺-Indn s u

≺-indn : ∀ {s u} → .(u ≺ +∞) → ≺-Indn s u
≺-indn {s}     {+∞}    u≺∞ = ⊥-elim (≺-impl-≢ u≺∞ refl)
≺-indn {+∞}    {fin u} u≺∞ = (zero , t≺+∞)
≺-indn {fin s} {fin u} u≺∞ = (suc (u ∸ s) , lemma s u (u ∸ s) t≤u+t∸u) where

  lemma : ∀ s u n → (s + n ≥ u) → (fin s + suc n ≻ fin u)
  lemma s u zero    s+0≥u   s≺t =
    (≤-impl-≼ s+0≥u ≼-trans ≡-impl-≼ (cong fin (+-unit s))) ≺-transʳ s≺t
  lemma s u (suc n) s+1+n≥u {fin t} s≺t = lemma t u n
    (s+1+n≥u ≤-trans ≡-impl-≥ (+-assoc s 1 n) ≤-trans +-resp-≤ (<-impl-+1≤ (≺-impl-< s≺t)) n)
  lemma s u (suc n) s+1+n≥u {+∞} s≺t =
    λ ∞≺v → ⊥-elim (≺-impl-⋡ ∞≺v +∞-top)

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
-- Andreas, 2019-03-28, issue #3600
--
-- Problem WAS: The size conversion checker produced invalid
-- constraints when getting stuck during checking, e.g., a <= max b a'.
-- The failing attempt of a <= b would produce constraints, which is unsound.
-- Now, we fail hard if a <= b gets stuck; this gives us a chance to succeed
-- on a <= a' instead.

{-# OPTIONS --sized-types #-}
{-# OPTIONS --show-implicit #-}

-- {-# OPTIONS -v tc.conv.size:60 -v tc.conv:10 #-}
-- {-# OPTIONS -v tc.meta.assign:10 #-}

open import Agda.Builtin.Size

data Type : (i : Size) → Set where

  _⇒_  : ∀ {i j}
       → Type i
       → Type j
       → Type (↑ (i ⊔ˢ j))

  Unit : ∀ {i} → Type (↑ i)

data Ty : ∀ {i} → Type i → Set where

  _⇒_  : ∀ {i j} {A : Type i} {B : Type j}
       → Ty A
       → Ty B
       → Ty {↑ (i ⊔ˢ j)} (A ⇒ B)

  Arr  : ∀ {i j} {A : Type i} {B : Type j}
       → Ty A
       → Ty B
       → Ty (A ⇒ B)

-- Should succeed.


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

module Data.Empty.Base where

open import Cubical.Data.Empty
  using (⊥; isProp⊥)
  public
open import Level

infix 4.5 ¬_
¬_ : Type a → Type a
¬ A = A → ⊥

⊥-elim : ⊥ → A
⊥-elim ()

max_stars_repo_name: oisdk/masters-thesis

max_issues_repo_name: oisdk/masters-thesis

max_forks_repo_name: oisdk/masters-thesis


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Class.IsEquivalence
open import Oscar.Class.Setoid
open import Oscar.Data.Proposequality

module Oscar.Property.Setoid.Proposequality where

module _ {𝔬} {𝔒 : Ø 𝔬} where

  instance

    𝓡eflexivityProposequality : Reflexivity.class Proposequality⟦ 𝔒 ⟧
    𝓡eflexivityProposequality .⋆ = !

    𝓢ymmetryProposequality : Symmetry.class Proposequality⟦ 𝔒 ⟧
    𝓢ymmetryProposequality .⋆ ∅ = !

    𝓣ransitivityProposequality : Transitivity.class Proposequality⟦ 𝔒 ⟧
    𝓣ransitivityProposequality .⋆ ∅ y∼z = y∼z

    IsEquivalenceProposequality : IsEquivalence Proposequality⟦ 𝔒 ⟧
    IsEquivalenceProposequality = ∁

module _ {𝔬} (𝔒 : Ø 𝔬) where

  SetoidProposequality : Setoid _ _
  SetoidProposequality = ∁ Proposequality⟦ 𝔒 ⟧


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

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

{-# OPTIONS --allow-unsolved-metas #-}

open import LibraBFT.Base.Types
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.NetworkMsg
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.Hash
open import Util.KVMap
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open        WithAbsVote

-- Here we have the abstraction functions that connect
-- the datatypes defined in LibraBFT.ImplFake.Consensus.Types
-- to the abstract records from LibraBFT.Abstract.Records
-- for a given EpochConfig.
--
module LibraBFT.Concrete.Records where

 ------------ properties relating the ids of (Executed)Blocks to hashes of their BlockData
 BlockHash≡ : Block → HashValue → Set
 BlockHash≡ b hv =  hashBlock b ≡ hv

 BlockId-correct : Block → Set
 BlockId-correct b = BlockHash≡ b (b ^∙ bId)

 BlockId-correct? : (b : Block) → Dec (BlockId-correct b)
 BlockId-correct? b = hashBlock b ≟Hash (b ^∙ bId)

 ExecutedBlockId-correct : ExecutedBlock → Set
 ExecutedBlockId-correct = BlockId-correct ∘ (_^∙ ebBlock)

 module WithEC (𝓔 : EpochConfig) where
   open import LibraBFT.ImplShared.Consensus.Types.EpochDep
   open WithEC 𝓔
   open import LibraBFT.Abstract.Abstract UID _≟UID_ NodeId 𝓔 ConcreteVoteEvidence as Abs hiding (bId; qcVotes; Block)
   open        EpochConfig 𝓔

   --------------------------------
   -- Abstracting Blocks and QCs --
   --------------------------------

   α-Block : Block → Abs.Block
   α-Block b with _bdBlockType (_bBlockData b)
   ...| NilBlock = record
        { bId     = _bId b
        ; bPrevQC = just (b ^∙ bBlockData ∙ bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId)
        ; bRound  = b ^∙ bBlockData ∙ bdRound
        }
   ...| Genesis = record
        { bId     = b ^∙ bId
        ; bPrevQC = nothing
        ; bRound  = b ^∙ bBlockData ∙ bdRound
        }
   ...| Proposal cmd α = record
        { bId     = b ^∙ bId
        ; bPrevQC = just (b ^∙ bBlockData ∙ bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId)
        ; bRound  = b ^∙ bBlockData ∙ bdRound
        }

   α-Block-bid≡ : (b : Block) → b ^∙ bId ≡ Abs.bId (α-Block b)
   α-Block-bid≡ b
      with _bdBlockType (_bBlockData b)
   ... | Proposal _ _ = refl
   ... | NilBlock     = refl
   ... | Genesis      = refl

   α-Block-rnd≡ : (b : Block) → b ^∙ bBlockData ∙ bdRound ≡ Abs.bRound (α-Block b)
   α-Block-rnd≡ b
      with _bdBlockType (_bBlockData b)
   ... | Proposal _ _ = refl
   ... | NilBlock     = refl
   ... | Genesis      = refl

   α-Block-prevqc≡-Prop : ∀ {b tx auth} → b ^∙ bBlockData ∙ bdBlockType ≡ Proposal tx auth
                           → Abs.bPrevQC (α-Block b) ≡ just (b ^∙ bBlockData ∙ bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId)
   α-Block-prevqc≡-Prop {b} refl = refl

   α-Block-prevqc≡-Gen  : ∀ {b} → b ^∙ bBlockData ∙ bdBlockType ≡ Genesis → Abs.bPrevQC (α-Block b) ≡ nothing
   α-Block-prevqc≡-Gen refl = refl

   α-Block-prevqc≡-Nil  : ∀ {b} → b ^∙ bBlockData ∙ bdBlockType ≡ NilBlock
                           → Abs.bPrevQC (α-Block b) ≡ just (b ^∙ bBlockData ∙ bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId)
   α-Block-prevqc≡-Nil {b} refl = refl

   α-VoteData-Block : VoteData → Abs.Block
   α-VoteData-Block vd = record
        { bId     = vd ^∙ vdProposed ∙ biId
        ; bPrevQC = just (vd ^∙ vdParent ∙ biId)
        ; bRound  = vd ^∙ vdProposed ∙ biRound
        }

   α-Vote : (qc : QuorumCert)(valid : MetaIsValidQC qc) → ∀ {as} → as ∈ qcVotes qc → Abs.Vote
   α-Vote qc v {as} as∈QC = α-ValidVote (rebuildVote qc as)
                                        (_ivvMember (All-lookup (_ivqcMetaVotesValid v) as∈QC))

   -- Abstraction of votes produce votes that carry evidence
   -- they have been cast.
   α-Vote-evidence : (qc : QuorumCert)(valid : MetaIsValidQC qc)
                   → ∀{vs} (prf : vs ∈ qcVotes qc)
                   → ConcreteVoteEvidence (α-Vote qc valid prf)
   α-Vote-evidence qc valid {as} v∈qc
     = record { _cveVote        = rebuildVote qc as
              ; _cveIsValidVote = All-lookup (_ivqcMetaVotesValid valid) v∈qc
              ; _cveIsAbs       = refl
              }

   α-QC : Σ QuorumCert MetaIsValidQC → Abs.QC
   α-QC (qc , valid) = record
     { qCertBlockId = qc ^∙ qcVoteData ∙ vdProposed ∙ biId
     ; qRound       = qc ^∙ qcVoteData ∙ vdProposed ∙ biRound
     ; qVotes       = All-reduce (α-Vote qc valid) All-self
     ; qVotes-C1    = subst IsQuorum {! !} (MetaIsValidQC._ivqcMetaIsQuorum valid)
     ; qVotes-C2    = All-reduce⁺ (α-Vote qc valid) (λ _ → refl) All-self
     ; qVotes-C3    = All-reduce⁺ (α-Vote qc valid) (λ _ → refl) All-self
     ; qVotes-C4    = All-reduce⁺ (α-Vote qc valid) (α-Vote-evidence qc valid) All-self
     }

   -- What does it mean for an (abstract) Block or QC to be represented in a NetworkMsg?
   data _α-∈NM_ : Abs.Record → NetworkMsg → Set where
     qc∈NM : ∀ {cqc nm}
           → (valid : MetaIsValidQC cqc)
           → cqc QC∈NM nm
           → Abs.Q (α-QC (cqc , valid)) α-∈NM nm
     b∈NM  : ∀ {cb pm nm}
           → nm ≡ P pm
           → pm ^∙ pmProposal ≡ cb
           → BlockId-correct cb     -- We should not consider just any message to be "InSys": an honest peer will reject a Block whose hash is incorrect.
           → Abs.B (α-Block cb) α-∈NM nm

   -- Our system model contains a message pool, which is a list of NodeId-NetworkMsg pairs.  The
   -- following relation expresses that an abstract record r is represented in a given message pool
   -- sm.
   data _α-Sent_ (r : Abs.Record) (sm : List (NodeId × NetworkMsg)) : Set where
     ws : ∀ {p nm} → getEpoch nm ≡ epoch → (p , nm) ∈ sm → r α-∈NM nm → r α-Sent sm


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

open import HoTT
open import cw.CW
open import cw.DegreeByProjection
open import cohomology.ChainComplex

module cw.cohomology.cellular.ChainComplex {i : ULevel} where

  chain-template : ∀ {n} (skel : Skeleton {i} n) {m}
    → Dec (m ≤ n) → AbGroup i
  chain-template skel (inl m≤n) = FreeAbGroup (cells-nth m≤n skel)
  chain-template skel (inr _) = Lift-abgroup {j = i} Unit-abgroup

  abstract
    boundary-nth-template : ∀ {n} (skel : Skeleton {i} n) dec
      → has-degrees-with-finite-support skel dec
      → {m : ℕ} (m≤n : m ≤ n) (Sm≤n : S m ≤ n)
      → cw-init (cw-take Sm≤n skel) == cw-take (≤-trans lteS Sm≤n) skel
      → cw-take (≤-trans lteS Sm≤n) skel == cw-take m≤n skel
      →  FreeAbGroup.grp (cells-nth Sm≤n skel)
      →ᴳ FreeAbGroup.grp (cells-nth m≤n skel)
    boundary-nth-template skel dec fin-sup m≤n Sm≤n path₀ path₁ =
         transportᴳ (λ lower-skel → FreeAbGroup.grp (cells-last lower-skel)) (path₀ ∙ path₁)
      ∘ᴳ boundary-nth Sm≤n skel dec fin-sup

  boundary-template : ∀ {n} (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → {m : ℕ} (m≤n? : Dec (m ≤ n)) (Sm≤n? : Dec (S m ≤ n))
    →  AbGroup.grp (chain-template skel Sm≤n?)
    →ᴳ AbGroup.grp (chain-template skel m≤n?)
  boundary-template skel dec fin-sup _ (inr _) = cst-hom
  boundary-template skel dec fin-sup (inr m≰n) (inl Sm≤n) = ⊥-rec $ m≰n (≤-trans lteS Sm≤n)
  boundary-template skel dec fin-sup (inl m≤n) (inl Sm≤n) =
    boundary-nth-template skel dec fin-sup m≤n Sm≤n (cw-init-take Sm≤n skel)
      (ap (λ m≤n → cw-take m≤n skel) (≤-has-all-paths (≤-trans lteS Sm≤n) m≤n))

  chain-complex : ∀ {n} (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → ChainComplex i
  chain-complex {n} skel dec fin-sup = record {M} where
    module M where
      head : AbGroup i
      head = Lift-abgroup {j = i} ℤ-abgroup

      chain : ℕ → AbGroup i
      chain m = chain-template skel (≤-dec m n)

      augment : AbGroup.grp (chain 0) →ᴳ AbGroup.grp head
      augment = FreeAbGroup-extend head λ _ → lift 1

      boundary : ∀ m → (AbGroup.grp (chain (S m)) →ᴳ AbGroup.grp (chain m))
      boundary m = boundary-template skel dec fin-sup (≤-dec m n) (≤-dec (S m) n)

  cochain-complex : ∀ {j} {n} (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → AbGroup j → CochainComplex (lmax i j)
  cochain-complex skel dec fin-sup G = complex-dualize
    (chain-complex skel dec fin-sup) G

  {- properties of coboundaries -}

  abstract
    private
      path-lemma₀ : ∀ {n} (skel : Skeleton {i} (S n)) {m} (m<n : m < n) (Sm<n : S m < n)
        →  ap (λ m≤Sn → cw-take m≤Sn skel) (≤-has-all-paths (≤-trans lteS (lteSR (inr Sm<n))) (lteSR (inr m<n)))
        == ap (λ m≤n → cw-take m≤n (cw-init skel)) (≤-has-all-paths (≤-trans lteS (inr Sm<n)) (inr m<n))
      path-lemma₀ skel m<n Sm<n =
        ap (λ m≤Sn → cw-take m≤Sn skel) (≤-has-all-paths (≤-trans lteS (lteSR (inr Sm<n))) (lteSR (inr m<n)))
          =⟨ ap (ap (λ m≤Sn → cw-take m≤Sn skel)) (contr-has-all-paths _ _) ⟩
        ap (λ m≤Sn → cw-take m≤Sn skel) (ap (lteSR ∘ inr) (<-has-all-paths (<-trans ltS Sm<n) m<n))
          =⟨ ∘-ap (λ m≤Sn → cw-take m≤Sn skel) (lteSR ∘ inr) _ ⟩
        ap (λ Sm<n → cw-take (lteSR (inr Sm<n)) skel) (<-has-all-paths (<-trans ltS Sm<n) m<n)
          =⟨ ap-∘ (λ m≤n → cw-take m≤n (cw-init skel)) inr _ ⟩
        ap (λ m≤n → cw-take m≤n (cw-init skel)) (ap inr (<-has-all-paths (<-trans ltS Sm<n) m<n))
          =⟨ ap (ap (λ m≤n → cw-take m≤n (cw-init skel))) (contr-has-all-paths _ _) ⟩
        ap (λ m≤n → cw-take m≤n (cw-init skel)) (≤-has-all-paths (≤-trans lteS (inr Sm<n)) (inr m<n))
          =∎

      path-lemma₁ : ∀ {n} (skel : Skeleton {i} (S (S n)))
        →  ap (λ n≤SSn → cw-take n≤SSn skel) (≤-has-all-paths (lteSR lteS) (lteSR lteS))
        == ap (λ n≤Sn → cw-take n≤Sn (cw-init skel)) (≤-has-all-paths lteS lteS)
      path-lemma₁ skel =
        ap (λ n≤SSn → cw-take n≤SSn skel) (≤-has-all-paths (lteSR lteS) (lteSR lteS))
          =⟨ ap (ap (λ n≤SSn → cw-take n≤SSn skel)) (contr-has-all-paths _ _) ⟩
        idp
          =⟨ ap (ap (λ n≤Sn → cw-take n≤Sn (cw-init skel))) (contr-has-all-paths _ _) ⟩
        ap (λ n≤Sn → cw-take n≤Sn (cw-init skel)) (≤-has-all-paths lteS lteS)
          =∎

      path-lemma₂ : ∀ {n} (skel : Skeleton {i} (S n))
        → ap (λ n≤Sn → cw-take n≤Sn skel) (≤-has-all-paths lteS lteS) == idp
      path-lemma₂ skel =
        ap (λ n≤Sn → cw-take n≤Sn skel) (≤-has-all-paths lteS lteS)
          =⟨ ap (ap (λ n≤Sn → cw-take n≤Sn skel)) (contr-has-all-paths _ _) ⟩
        idp
          =∎

  abstract
    boundary-template-descend-from-far : ∀ {n} (skel : Skeleton {i} (S n)) dec fin-sup {m} m<n Sm<n
      → boundary-template {n = S n} skel dec fin-sup {m} (inl (lteSR (inr m<n))) (inl (lteSR (inr Sm<n)))
        == boundary-template {n = n} (cw-init skel)
          (init-has-cells-with-dec-eq skel dec)
          (init-has-degrees-with-finite-support skel dec fin-sup)
          (inl (inr m<n)) (inl (inr Sm<n))
    boundary-template-descend-from-far skel dec fin-sup m<n Sm<n =
      ap (boundary-nth-template skel dec fin-sup (lteSR (inr m<n)) (lteSR (inr Sm<n)) (cw-init-take (lteSR (inr Sm<n)) skel))
        (path-lemma₀ skel m<n Sm<n)

    boundary-template-descend-from-two-above : ∀ {n} (skel : Skeleton {i} (S (S n))) dec fin-sup
      → boundary-template {n = S (S n)} skel dec fin-sup (inl (lteSR lteS)) (inl lteS)
        == boundary-template {n = (S n)} (cw-init skel)
          (init-has-cells-with-dec-eq skel dec)
          (init-has-degrees-with-finite-support skel dec fin-sup)
          (inl lteS) (inl lteE)
    boundary-template-descend-from-two-above skel dec fin-sup =
      ap (boundary-nth-template skel dec fin-sup (lteSR lteS) lteS idp) (path-lemma₁ skel)

    boundary-template-β : ∀ {n} (skel : Skeleton {i} (S n)) dec fin-sup
      →  boundary-template {n = S n} skel dec fin-sup (inl lteS) (inl lteE)
      == FreeAbGroup-extend
            (FreeAbGroup (cells-last (cw-init skel)))
            (boundary'-last skel dec fin-sup)
    boundary-template-β skel dec fin-sup = group-hom= $
      ap (GroupHom.f ∘ boundary-nth-template skel dec fin-sup lteS lteE idp) (path-lemma₂ skel)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Data.Maybe.Properties where

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Maybe

just-not-nothing : ∀ {ℓ}{A : Set ℓ}{x : Maybe A}{y : A} → x ≡ just y → ¬ (x ≡ nothing)
just-not-nothing refl = λ ()


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

module Data.Real.CReal where

import Prelude
import Data.Bool
import Data.String
import Data.Real.Complete
import Data.Real.Base
import Data.Nat
import Data.Integer
import Data.Rational as Rational
import Data.Interval
import Data.Real.Gauge
import Data.Show
import Data.List
import Data.Tuple

open Prelude
open Data.Real.Base
open Data.Real.Complete
open Data.Integer using (Int; pos) renaming (_-_ to _-i_; _<_ to _<i_)
open Rational hiding (fromInt)
open Data.Bool
open Data.String
open Data.Interval
open Data.Real.Gauge
open Data.Nat using (Nat)
open Data.Tuple

data CReal : Set where
  cReal : Complete Base -> CReal

approx : CReal -> Complete Base
approx (cReal f) ε = f ε

inject : Base -> CReal
inject x = cReal (unit x)

data BoundedCReal : Set where
  _∈_ : CReal -> Interval Base -> BoundedCReal

around : CReal -> Int
around (cReal f) = round (f (pos 1 % pos 2))

integerInterval : CReal -> Interval Base
integerInterval f = [ i - fromNat 1 ▻ i + fromNat 1 ]
  where
    i = Rational.fromInt (around f)

compact : CReal -> BoundedCReal
compact x = x ∈ integerInterval x

choke : BoundedCReal -> CReal
choke (cReal x ∈ [ lb ▻ ub ]) = cReal f
  where
    f : Complete Base
    f ε = ! y < lb => lb
          ! ub < y => ub
          ! otherwise y
      where
        y = x ε

compress : Complete Base -> Complete Base
compress x ε = approxBase (x ε2) ε2
  where
    ε2 = ε / fromNat 2

mapCR : (Base ==> Base) -> CReal -> CReal
mapCR f (cReal x) = cReal $ mapC f (compress x)

mapCR2 : (Base ==> Base ==> Base) -> CReal -> CReal -> CReal
mapCR2 f (cReal x) (cReal y) = cReal $ mapC2 f (compress x) (compress y)

bindR : (Base ==> Complete Base) -> CReal -> CReal
bindR f (cReal x) = cReal $ bind f (compress x)

approxRange : CReal -> Gauge -> Interval Base
approxRange x ε = [ r - ε ▻ r + ε ]
  where
    r = approx x ε

-- non-terminates for 0
proveNonZeroFrom : Gauge -> CReal -> Base
proveNonZeroFrom g r =
  ! high < fromNat 0 => high
  ! fromNat 0 < low  => low
  ! otherwise           proveNonZeroFrom (g / fromNat 2) r
  where
    i    = approxRange r g
    low  = lowerBound i
    high = upperBound i

proveNonZero : CReal -> Base
proveNonZero = proveNonZeroFrom (fromNat 1)

-- Negation

negateCts : Base ==> Base
negateCts = uniformCts id -_

realNegate : CReal -> CReal
realNegate = mapCR negateCts

-- Addition

plusBaseCts : Base -> Base ==> Base
plusBaseCts a = uniformCts id (_+_ a)

plusCts : Base ==> Base ==> Base
plusCts = uniformCts id plusBaseCts

realPlus : CReal -> CReal -> CReal
realPlus = mapCR2 plusCts

realTranslate : Base -> CReal -> CReal
realTranslate a = mapCR (plusBaseCts a)

-- Multiplication

multBaseCts : Base -> Base ==> Base
multBaseCts (pos 0 %' _) = constCts (fromNat 0)
multBaseCts a            = uniformCts μ (_*_ a)
  where
    μ = \ε -> ε / ! a !

-- First argument must be ≠ 0
multCts : Base -> Base ==> Base ==> Base
multCts maxy = uniformCts μ multBaseCts
  where
    μ = \ε -> ε / maxy

realScale : Base -> CReal -> CReal
realScale a = mapCR (multBaseCts a)

bound : Interval Base -> Base
bound [ lb ▻ ub ] = max ub (- lb)

realMultBound : BoundedCReal -> CReal -> CReal
realMultBound (x ∈ i) y = mapCR2 (multCts b) y (choke (x ∈ i))
  where
    b = bound i

realMult : CReal -> CReal -> CReal
realMult x y = realMultBound (compact x) y

-- Absolute value
absCts : Base ==> Base
absCts = uniformCts id !_!

realAbs : CReal -> CReal
realAbs = mapCR absCts

fromInt : Int -> CReal
fromInt x = inject (Rational.fromInt x)

fromRational : Rational -> CReal
fromRational = inject

-- Reciprocal

recipCts : Base -> Base ==> Base
recipCts nz = uniformCts μ f
  where
    f : Base -> Base
    f a = ! fromNat 0 ≤ nz => recip (max nz a)
          ! otherwise         recip (min a nz)

    μ = \ε -> ε * nz ^ pos 2

realRecipWitness : Base -> CReal -> CReal
realRecipWitness nz = mapCR (recipCts nz)

realRecip : CReal -> CReal
realRecip x = realRecipWitness (proveNonZero x) x

-- Exponentiation

intPowerCts : Gauge -> Int -> Base ==> Base
intPowerCts _ (pos 0) = constCts (fromNat 1)
intPowerCts maxx n = uniformCts μ (flip _^_ n)
  where
    μ = \ε -> ε / (Rational.fromInt n * maxx ^ (n -i pos 1))

realPowerIntBound : BoundedCReal -> Int -> CReal
realPowerIntBound (x ∈ i) n = mapCR (intPowerCts b n) (choke (x ∈ i))
  where
    b = bound i

realPowerInt : CReal -> Int -> CReal
realPowerInt = realPowerIntBound ∘ compact

showReal : Nat -> CReal -> String
showReal n x =
  ! len ≤' n => sign ++ "0." ++ fromList (replicate (n -' len) '0') ++ s
  ! otherwise   sign ++ i ++ "." ++ f
  where
    open Data.Nat using () renaming
              ( _^_ to _^'_
              ; div to div'; mod to mod'
              ; _==_ to _=='_; _≤_ to _≤'_
              ; _-_ to _-'_
              )
    open Data.Show
    open Data.List hiding (_++_)
    open Data.Integer using () renaming (-_ to -i_)

    k = 10 ^' n
    m = around $ realScale (fromNat k) x
    m' = if m <i pos 0 then -i m else m
    s = showInt m'

    sign = if m <i pos 0 then "-" else ""

    len = length (toList s)

    p = splitAt (len -' n) $ toList s
    i = fromList $ fst p
    f = fromList $ snd p


text:
module agda where
open import IO

main = run (putStrLn "Hello, World!")

max_stars_repo_name: thevkrant/hello-world

max_issues_repo_name: thevkrant/hello-world

max_forks_repo_name: thevkrant/hello-world


text:
module Spire.Operational where

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

data Level : Set where
  zero : Level
  suc : Level → Level

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

data Context : Set
data Type (Γ : Context) : Set
data Value (Γ : Context) : Type Γ → Set
data Neutral (Γ : Context) : Type Γ → Set

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

data Context where
  ∅ : Context
  _,_ : (Γ : Context) → Type Γ → Context

data Type Γ where
  `⊥ `⊤ `Bool : Type Γ
  `Desc `Type : (ℓ : Level) → Type Γ
  `Π `Σ : (A : Type Γ) (B : Type (Γ , A)) → Type Γ
  `μ : ∀{ℓ} → Value Γ (`Desc ℓ) → Type Γ
  `⟦_⟧ : ∀{ℓ} → Neutral Γ (`Type ℓ) → Type Γ
  `⟦_⟧ᵈ : ∀{ℓ} → Neutral Γ (`Desc ℓ) → Type Γ → Type Γ

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

⟦_⟧ : ∀{Γ ℓ} → Value Γ (`Type ℓ) →  Type Γ
⟦_⟧ᵈ : ∀{Γ ℓ} → Value Γ (`Desc ℓ) → Type Γ →  Type Γ

postulate
  wknT : ∀{Γ A} → Type Γ → Type (Γ , A)
  subT : ∀{Γ A} → Type (Γ , A) → Value Γ A → Type Γ
  subV : ∀{Γ A B} → Value (Γ , A) B → (x : Value Γ A) → Value Γ (subT B x)

data Var : (Γ : Context) (A : Type Γ) → Set where
  here : ∀{Γ A} → Var (Γ , A) (wknT A)
  there : ∀{Γ A B} → Var Γ A → Var (Γ , B) (wknT A)

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

data Value Γ where
  {- Type introduction -}
  `⊥ `⊤ `Bool `Desc `Type : ∀{ℓ} → Value Γ (`Type ℓ)
  `Π `Σ : ∀{ℓ} (A : Value Γ (`Type ℓ)) (B : Value (Γ , ⟦ A ⟧) (`Type ℓ)) → Value Γ (`Type ℓ)
  `μ : ∀{ℓ} → Value Γ (`Desc ℓ) → Value Γ (`Type ℓ)
  `⟦_⟧ : ∀{ℓ} → Value Γ (`Type ℓ) → Value Γ (`Type (suc ℓ))
  `⟦_⟧ᵈ : ∀{ℓ} → Value Γ (`Desc ℓ) → Value Γ (`Type ℓ) → Value Γ (`Type ℓ)

  {- Desc introduction -}
  `⊤ᵈ `Xᵈ : ∀{ℓ} → Value Γ (`Desc ℓ)
  `Πᵈ `Σᵈ : ∀{ℓ}
    (A : Value Γ (`Type ℓ))
    (B : Value (Γ , ⟦ A ⟧) (`Desc (suc ℓ)))
    → Value Γ (`Desc (suc ℓ))

  {- Value introduction -}
  `tt : Value Γ `⊤
  `true `false : Value Γ `Bool
  _`,_ : ∀{A B} (a : Value Γ A) (b : Value Γ (subT B a)) → Value Γ (`Σ A B)
  `λ : ∀{A B} → Value (Γ , A) B → Value Γ (`Π A B)
  `con : ∀{ℓ} {D : Value Γ (`Desc ℓ)} → Value Γ (⟦ D ⟧ᵈ (`μ D)) → Value Γ (`μ D)
  `neut : ∀{A} → Neutral Γ A → Value Γ A

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

data Neutral Γ where
  {- Value elimination -}
  `var : ∀{A} → Var Γ A → Neutral Γ A
  `if_`then_`else_ : ∀{C} (b : Neutral Γ `Bool) (c₁ c₂ : Value Γ C) → Neutral Γ C
  `elim⊥ : ∀{A} → Neutral Γ `⊥ → Neutral Γ A
  `elimBool : ∀{ℓ} (P : Value (Γ , `Bool) (`Type ℓ))
    (pt : Value Γ (subT ⟦ P ⟧ `true))
    (pf : Value Γ (subT ⟦ P ⟧ `false))
    (b : Neutral Γ `Bool) → Neutral Γ (subT ⟦ P ⟧ (`neut b))
  `proj₁ : ∀{A B} → Neutral Γ (`Σ A B) → Neutral Γ A
  `proj₂ : ∀{A B} (ab : Neutral Γ (`Σ A B)) → Neutral Γ (subT B (`neut (`proj₁ ab)))
  _`$_ : ∀{A B} (f : Neutral Γ (`Π A B)) (a : Value Γ A) → Neutral Γ (subT B a)
  `des : ∀{ℓ} {D : Value Γ (`Desc ℓ)} → Neutral Γ (`μ D) → Neutral Γ (⟦ D ⟧ᵈ (`μ D))

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

⟦ `Π A B ⟧ = `Π ⟦ A ⟧ ⟦ B ⟧
⟦ `Σ A B ⟧ = `Σ ⟦ A ⟧ ⟦ B ⟧
⟦ `⊥ ⟧ = `⊥
⟦ `⊤ ⟧ = `⊤
⟦ `Bool ⟧ = `Bool
⟦ `μ D ⟧ = `μ D
⟦ `Type {zero} ⟧ = `⊥
⟦ `Type {suc ℓ} ⟧ = `Type ℓ
⟦ `⟦ A ⟧ ⟧ = ⟦ A ⟧
⟦ `Desc {ℓ} ⟧ = `Desc ℓ
⟦ `⟦ D ⟧ᵈ X ⟧ = ⟦ D ⟧ᵈ ⟦ X ⟧
⟦ `neut A ⟧ = `⟦ A ⟧

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

⟦ `⊤ᵈ ⟧ᵈ X = `⊤
⟦ `Xᵈ ⟧ᵈ X = X
⟦ `Πᵈ A D ⟧ᵈ X = `Π ⟦ A ⟧ (⟦ D ⟧ᵈ (wknT X))
⟦ `Σᵈ A D ⟧ᵈ X = `Σ ⟦ A ⟧ (⟦ D ⟧ᵈ (wknT X))
⟦ `neut D ⟧ᵈ X = `⟦ D ⟧ᵈ X

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

elim⊥ : ∀{Γ A} → Value Γ `⊥ → Value Γ A
elim⊥ (`neut bot) = `neut (`elim⊥ bot)

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

if_then_else_ : ∀{Γ C} (b : Value Γ `Bool) (c₁ c₂ : Value Γ C) → Value Γ C
if `true then c₁ else c₂ = c₁
if `false then c₁ else c₂ = c₂
if `neut b then c₁ else c₂ = `neut (`if b `then c₁ `else c₂)

elimBool : ∀{Γ ℓ} (P : Value (Γ , `Bool) (`Type ℓ))
  (pt : Value Γ (subT ⟦ P ⟧ `true))
  (pf : Value Γ (subT ⟦ P ⟧ `false))
  (b : Value Γ `Bool)
  → Value Γ (subT ⟦ P ⟧ b)
elimBool P pt pf `true = pt
elimBool P pt pf `false = pf
elimBool P pt pf (`neut b) = `neut (`elimBool P pt pf b)

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

proj₁ : ∀{Γ A B} → Value Γ (`Σ A B) → Value Γ A
proj₁ (a `, b) = a
proj₁ (`neut ab) = `neut (`proj₁ ab)

proj₂ : ∀{Γ A B} (ab : Value Γ (`Σ A B)) → Value Γ (subT B (proj₁ ab))
proj₂ (a `, b) = b
proj₂ (`neut ab) = `neut (`proj₂ ab)

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

des : ∀{Γ ℓ} {D : Value Γ (`Desc ℓ)} → Value Γ (`μ D) → Value Γ (⟦ D ⟧ᵈ (`μ D))
des (`con x) = x
des (`neut x) = `neut (`des x)

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

_$_ : ∀{Γ A B} → Value Γ (`Π A B) → (a : Value Γ A) → Value Γ (subT B a)
`λ b $ a = subV b a
`neut f $ a = `neut (f `$ a)

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

data Term (Γ : Context) : Type Γ → Set
eval : ∀{Γ A} → Term Γ A → Value Γ A

data Term Γ where
  {- Type introduction -}
  `⊥ `⊤ `Bool `Type : ∀{ℓ} → Term Γ (`Type ℓ)
  `Π `Σ : ∀{ℓ} (A : Term Γ (`Type ℓ)) (B : Term (Γ , ⟦ eval A ⟧) (`Type ℓ)) → Term Γ (`Type ℓ)
  `μ : ∀{ℓ} → Term Γ (`Desc ℓ) → Term Γ (`Type ℓ)
  `⟦_⟧ : ∀{ℓ} → Term Γ (`Type ℓ) → Term Γ (`Type (suc ℓ))
  `⟦_⟧ᵈ : ∀{ℓ} → Term Γ (`Desc ℓ) → Term Γ (`Type ℓ) → Term Γ (`Type ℓ)

  {- Desc introduction -}
  `⊤ᵈ `Xᵈ : ∀{ℓ} → Term Γ (`Desc ℓ)
  `Πᵈ `Σᵈ : ∀{ℓ}
    (A : Term Γ (`Type ℓ))
    (D : Term (Γ , ⟦ eval A ⟧) (`Desc (suc ℓ)))
    → Term Γ (`Desc (suc ℓ))

  {- Value introduction -}
  `tt : Term Γ `⊤
  `true `false : Term Γ `Bool
  _`,_ : ∀{A B}
    (a : Term Γ A) (b : Term Γ (subT B (eval a)))
    → Term Γ (`Σ A B)
  `λ : ∀{A B}
    (b : Term (Γ , A) B)
    → Term Γ (`Π A B)
  `con : ∀{ℓ} {D : Value Γ (`Desc ℓ)} → Term Γ (⟦ D ⟧ᵈ (`μ D)) → Term Γ (`μ D)

  {- Value elimination -}
  `var : ∀{A} → Var Γ A → Term Γ A
  `if_`then_`else_ : ∀{C}
    (b : Term Γ `Bool)
    (c₁ c₂ : Term Γ C)
    → Term Γ C
  _`$_ : ∀{A B} (f : Term Γ (`Π A B)) (a : Term Γ A) → Term Γ (subT B (eval a))
  `proj₁ : ∀{A B} → Term Γ (`Σ A B) → Term Γ A
  `proj₂ : ∀{A B} (ab : Term Γ (`Σ A B)) → Term Γ (subT B (proj₁ (eval ab)))
  `elim⊥ : ∀{A} → Term Γ `⊥ → Term Γ A
  `elimBool : ∀{ℓ} (P : Term (Γ , `Bool) (`Type ℓ))
    (pt : Term Γ (subT ⟦ eval P ⟧ `true))
    (pf : Term Γ (subT ⟦ eval P ⟧ `false))
    (b : Term Γ `Bool)
    → Term Γ (subT ⟦ eval P ⟧ (eval b))
  `des : ∀{ℓ} {D : Value Γ (`Desc ℓ)} → Term Γ (`μ D) → Term Γ (⟦ D ⟧ᵈ (`μ D))

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

{- Type introduction -}
eval `⊥ = `⊥
eval `⊤ = `⊤
eval `Bool = `Bool
eval `Type = `Type
eval (`Π A B) = `Π (eval A) (eval B)
eval (`Σ A B) = `Σ (eval A) (eval B)
eval (`μ D) = `μ (eval D)
eval `⟦ A ⟧ = `⟦ eval A ⟧
eval (`⟦ D ⟧ᵈ X) = `⟦ eval D ⟧ᵈ (eval X)

{- Desc introduction -}
eval `⊤ᵈ = `⊤ᵈ
eval `Xᵈ = `Xᵈ
eval (`Πᵈ A D) = `Πᵈ (eval A) (eval D)
eval (`Σᵈ A D) = `Σᵈ (eval A) (eval D)

{- Value introduction -}
eval `tt = `tt
eval `true = `true
eval `false = `false
eval (a `, b) = eval a `, eval b
eval (`λ b) = `λ (eval b)
eval (`con x) = `con (eval x)

{- Value elimination -}
eval (`var i) = `neut (`var i)
eval (`if b `then c₁ `else c₂) = if eval b then eval c₁ else eval c₂
eval (f `$ a) = eval f $ eval a
eval (`proj₁ ab) = proj₁ (eval ab)
eval (`proj₂ ab) = proj₂ (eval ab)
eval (`elim⊥ bot) = elim⊥ (eval bot)
eval (`elimBool P pt pf b) = elimBool (eval P) (eval pt) (eval pf) (eval b)
eval (`des x) = des (eval x)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
open import Type

module Relator.Equals.Proofs.Equiv {ℓ} {T : Type{ℓ}} where

import Relator.Equals.Proofs.Equivalence

open Relator.Equals.Proofs.Equivalence.One   {T = T} public
open Relator.Equals.Proofs.Equivalence.Two   {A = T} public
open Relator.Equals.Proofs.Equivalence.Three {A = T} public
open Relator.Equals.Proofs.Equivalence.Four  {A = T} public

instance [≡]-unary-relator-instance    = [≡]-unary-relator
instance [≡]-binary-relator-instance   = [≡]-binary-relator
instance [≡]-binary-operator-instance  = [≡]-binary-operator
instance [≡]-trinary-operator-instance = [≡]-trinary-operator
instance [≡]-to-function-instance      = [≡]-to-function
instance [≡]-equiv-instance            = [≡]-equiv


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

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data Unit : Set where
  unit : Unit

Foo : Unit → Set
Foo unit = Unit

Bar : Unit → Unit → Set
Bar unit = Foo

bar : ∀ x y → Bar x y ≡ Unit
bar unit unit = refl

{-# REWRITE bar #-}

test : ∀ x y → Bar x y
test _ _ = unit

works : ∀ x → Foo x
works x = test unit x


text:
module Imports.Issue5357-C where
import Imports.Issue5357-D

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Selective.Examples.Chat where

open import Selective.ActorMonad
open import Selective.Libraries.Call
open import Prelude
  hiding (Maybe)
open import Data.Maybe as Maybe
  hiding (map)
open import Data.Maybe.Categorical as CMaybe

open import Data.List.Properties
open import Category.Monad

open import Debug
open import Data.Nat.Show using (show)

RoomName = ℕ
ClientName = ℕ

ClientInterface : InboxShape
Client-to-Room : InboxShape
Room-to-Client : InboxShape

-- =============
--  JOIN ROOM
-- =============

data JoinRoomSuccess : Set where
  JR-SUCCESS : RoomName → JoinRoomSuccess

data JoinRoomFail : Set where
  JR-FAIL : RoomName → JoinRoomFail

data JoinRoomStatus : Set where
  JRS-SUCCESS JRS-FAIL : RoomName → JoinRoomStatus

JoinRoomSuccessReply : MessageType
JoinRoomSuccessReply = ValueType UniqueTag ∷ ValueType JoinRoomSuccess ∷ [ ReferenceType Client-to-Room ]ˡ

JoinRoomFailReply : MessageType
JoinRoomFailReply = ValueType UniqueTag ∷ [ ValueType JoinRoomFail ]ˡ

JoinRoomReplyInterface : InboxShape
JoinRoomReplyInterface = JoinRoomSuccessReply ∷ JoinRoomFailReply ∷ Room-to-Client

JoinRoom : MessageType
JoinRoom = ValueType UniqueTag ∷ ReferenceType JoinRoomReplyInterface ∷ ValueType RoomName ∷ [ ValueType ClientName ]ˡ

-- =============
--  CREATE ROOM
-- =============

data CreateRoomResult : Set where
  CR-SUCCESS CR-EXISTS : RoomName → CreateRoomResult

CreateRoomReply : MessageType
CreateRoomReply = ValueType UniqueTag ∷ [ ValueType CreateRoomResult ]ˡ

CreateRoom : MessageType
CreateRoom = ValueType UniqueTag ∷ ReferenceType [ CreateRoomReply ]ˡ ∷ [ ValueType RoomName ]ˡ

-- ============
--  LIST ROOMS
-- ============

RoomList : Set
RoomList = List RoomName

ListRoomsReply : MessageType
ListRoomsReply = ValueType UniqueTag ∷ [ ValueType RoomList ]ˡ

ListRooms : MessageType
ListRooms = ValueType UniqueTag ∷ [ ReferenceType [ ListRoomsReply ]ˡ ]ˡ

-- ===
--
-- ===

Client-to-RoomManager : InboxShape
Client-to-RoomManager = JoinRoom ∷ CreateRoom ∷ [ ListRooms ]ˡ

RoomManagerInterface : InboxShape
RoomManagerInterface = Client-to-RoomManager

GetRoomManagerReply : MessageType
GetRoomManagerReply = ValueType UniqueTag ∷ [ ReferenceType RoomManagerInterface ]ˡ

GetRoomManager : MessageType
GetRoomManager = ValueType UniqueTag ∷ [ ReferenceType [ GetRoomManagerReply ]ˡ ]ˡ

RoomSupervisorInterface : InboxShape
RoomSupervisorInterface = [ GetRoomManager ]ˡ

ClientSupervisorInterface : InboxShape
ClientSupervisorInterface =
  [ ReferenceType RoomSupervisorInterface ]ˡ ∷ [ GetRoomManagerReply ]ˡ

--
--
--

record ChatMessageContent : Set where
  constructor chat-from_message:_
  field
    sender : ClientName
    message : String

ChatMessage : MessageType
ChatMessage = [ ValueType ChatMessageContent ]ˡ

LeaveRoom : MessageType
LeaveRoom = [ ValueType ClientName ]ˡ

Client-to-Room = ChatMessage ∷ [ LeaveRoom ]ˡ

Room-to-Client = [ ChatMessage ]ˡ

AddToRoom : MessageType
AddToRoom = ValueType ClientName ∷ [ ReferenceType Room-to-Client ]ˡ

RoomManager-to-Room : InboxShape
RoomManager-to-Room = [ AddToRoom ]ˡ

RoomInstanceInterface : InboxShape
RoomInstanceInterface = Client-to-Room ++ RoomManager-to-Room

ClientInterface = [ ReferenceType RoomManagerInterface ]ˡ ∷ CreateRoomReply ∷ ListRoomsReply ∷ JoinRoomReplyInterface

-- ======
--  ROOM
-- ======

ClientList : Set
ClientList = List ClientName

record RoomState : Set₁ where
  field
    clients : ClientList

cl-to-context : ClientList → TypingContext
cl-to-context = map λ _ → Room-to-Client

rs-to-context : RoomState → TypingContext
rs-to-context rs = let open RoomState
  in cl-to-context (rs .clients)

record RoomLeave (rs : ClientList) (name : ClientName) : Set₁ where
  field
    filtered : ClientList
    subs : (cl-to-context filtered) ⊆ (cl-to-context rs)

++-temp-fix : (l r : ClientList) → (x : ClientName) → (l ++ (x ∷ r)) ≡ ((l ∷ʳ x) ++ r)
++-temp-fix [] r x = refl
++-temp-fix (x₁ ∷ l) r x = cong (_∷_ x₁) (++-temp-fix l r x)

room-instance : ∀ {i} → ActorM i RoomInstanceInterface RoomState [] rs-to-context
room-instance = begin (loop (record { clients = [] }))
  where
    -- only removes first occurance...
    leave-room : (cl : ClientList) → (name : ClientName) → RoomLeave cl name
    leave-room [] name = record { filtered = [] ; subs = [] }
    leave-room (x ∷ cl) name with (x ≟ name)
    ... | (yes _) = record { filtered = cl ; subs = ⊆-suc ⊆-refl }
    ... | (no _) = let
        rl = leave-room cl name
        open RoomLeave
      in record { filtered = x ∷ rl .filtered ; subs = Z ∷ ⊆-suc (rl .subs) }
    send-to-others : ∀ {i} → (cl : ClientList) →
                     ClientName →
                     String →
                     ∞ActorM i RoomInstanceInterface ⊤₁ (cl-to-context cl) (λ _ → cl-to-context cl)
    send-to-others [] _ _ = return _
    send-to-others cl@(_ ∷ _) name message = send-loop [] cl
      where
        build-pointer : (l r : ClientList) →
                      cl-to-context r ⊢ Room-to-Client →
                      (cl-to-context (l ++ r)) ⊢ Room-to-Client
        build-pointer [] r p = p
        build-pointer (x ∷ l) r p = S (build-pointer l r p)
        recurse : ∀ {i} → (l r : ClientList) → (x : ClientName) →
                  ∞ActorM i RoomInstanceInterface ⊤₁ (cl-to-context (l ++ (x ∷ r))) (λ _ → (cl-to-context (l ++ (x ∷ r))))
        send-loop : ∀ {i} → (l r : ClientList) →
          ∞ActorM i RoomInstanceInterface ⊤₁ (cl-to-context (l ++ r)) (λ _ → cl-to-context (l ++ r))
        send-loop l [] = return _
        send-loop l (x ∷ r) with (x ≟ name)
        ... | (yes _) = recurse l r x
        ... | (no _) = let p = build-pointer l (x ∷ r) Z
          in debug ("Sending to " || show x || ": " || message) (p ![t: Z ] [ lift (chat-from name message: message) ]ᵃ ) >> recurse l r x
        recurse l r x rewrite ++-temp-fix l r x = send-loop (l ∷ʳ x) r
    handle-message : ∀ {i} → (rs : RoomState) →
                     (m : Message RoomInstanceInterface) →
                     ∞ActorM i RoomInstanceInterface RoomState (add-references (rs-to-context rs) m) rs-to-context
    -- chat message
    handle-message rs (Msg Z (chat-from client-name message: message ∷ [])) = do
      let open RoomState
      debug ("room sending " || show (pred (length (rs .clients))) ||  " messages from " || show client-name || ": " || message) (send-to-others (rs .clients) client-name message)
      (return₁ rs)
    -- leave room
    handle-message rs (Msg (S Z) (client-name ∷ [])) = do
      let
        open RoomState
        open RoomLeave
        rl = leave-room (rs .clients) client-name
      debug ("client#" || show client-name || " left the room") (strengthen (rl .subs))
      (return₁ (record { clients = rl .filtered }))
    -- add to room
    handle-message rs (Msg (S (S Z)) (client-name ∷ _ ∷ [])) = do
      let open RoomState
      return₁ (record { clients = client-name ∷ rs .clients })
    handle-message rs (Msg (S (S (S ()))) _)
    loop : ∀ {i} →
           (rs : RoomState) →
           ∞ActorM i RoomInstanceInterface RoomState (rs-to-context rs) rs-to-context
    loop state .force = begin do
      m ← debug ("ROOM LOOP") receive
      state' ← (handle-message state m)
      loop state'

-- ==============
--  ROOM MANAGER
-- ==============

record RoomManagerState : Set₁ where
  field
    rooms : RoomList

rms-to-context : RoomManagerState → TypingContext
rms-to-context rms = rl-to-context (rms .rooms)
  where
    open RoomManagerState
    rl-to-context : RoomList → TypingContext
    rl-to-context = map λ _ → RoomInstanceInterface

lookup-room : ∀ {i} → {Γ : TypingContext} →
              (rms : RoomManagerState) →
              RoomName →
              ∞ActorM i RoomManagerInterface (Maybe ((Γ ++ (rms-to-context rms)) ⊢ RoomInstanceInterface)) (Γ ++ (rms-to-context rms)) (λ _ → Γ ++ (rms-to-context rms))
lookup-room rms name =
  let open RoomManagerState
  in return₁ (loop _ (rms .rooms))
  where
    rl-to-context : RoomList → TypingContext
    rl-to-context = map λ _ → RoomInstanceInterface
    loop : (Γ : TypingContext) → (rl : RoomList) → Maybe ((Γ ++ rl-to-context rl) ⊢ RoomInstanceInterface)
    loop [] [] = nothing
    loop [] (x ∷ xs) with (x ≟ name)
    ... | (yes p) = just Z
    ... | (no _) = RawMonad._>>=_ CMaybe.monad (loop [] xs) λ p → just (S p)
    loop (x ∷ Γ) rl = RawMonad._>>=_ CMaybe.monad (loop Γ rl) (λ p → just (S p))

room-manager : ∀ {i} → ActorM i RoomManagerInterface RoomManagerState [] rms-to-context
room-manager = begin (loop (record { rooms = [] }))
  where
    handle-room-join : ∀ {i} → {Γ : TypingContext} →
                        UniqueTag →
                        RoomName →
                        ClientName →
                        (Γ ⊢ JoinRoomReplyInterface) →
                        (Maybe (Γ ⊢ RoomInstanceInterface)) →
                        ∞ActorM i RoomManagerInterface ⊤₁ Γ (λ _ → Γ)
    handle-room-join tag room-name client-name cp (just rp) = do
      cp ![t: Z ] ((lift tag) ∷ (lift (JR-SUCCESS room-name)) ∷ [ [ rp ]>: (Z ∷ [ S Z ]ᵐ) ]ᵃ)
      rp ![t: S (S Z) ] ((lift client-name) ∷ [ [ cp ]>: [ S (S Z) ]ᵐ ]ᵃ)
    handle-room-join tag room-name client-name p nothing =
      p ![t: S Z ] (lift tag ∷ [ lift (JR-FAIL room-name) ]ᵃ)
    handle-create-room : ∀ {i} →
                         (rms : RoomManagerState) →
                         UniqueTag →
                         RoomName →
                         Maybe (([ CreateRoomReply ]ˡ ∷ rms-to-context rms) ⊢ RoomInstanceInterface) →
                         ∞ActorM i RoomManagerInterface RoomManagerState ([ CreateRoomReply ]ˡ ∷ rms-to-context rms) rms-to-context
    handle-create-room rms tag name (just x) = do
      Z ![t: Z ] ((lift tag) ∷ [ lift (CR-EXISTS name) ]ᵃ)
      strengthen (⊆-suc ⊆-refl)
      return₁ rms
    handle-create-room rms tag name nothing = do
      Z ![t: Z ] ((lift tag) ∷ [ lift (CR-SUCCESS name) ]ᵃ)
      strengthen (⊆-suc ⊆-refl)
      spawn room-instance
      let
        rms' : RoomManagerState
        rms' = (record { rooms = name ∷ RoomManagerState.rooms rms })
      (return₁ rms')
    handle-message : ∀ {i} → (rms : RoomManagerState) →
                     (m : Message RoomManagerInterface) →
                     ∞ActorM i RoomManagerInterface RoomManagerState (add-references (rms-to-context rms) m) rms-to-context
    -- Jooin room
    handle-message state (Msg Z (tag ∷ _ ∷ room-name ∷ client-name ∷ [])) = do
      p ← (lookup-room state room-name)
      handle-room-join tag room-name client-name Z p
      (strengthen (⊆-suc ⊆-refl))
      (return₁ state)
    -- Create room
    handle-message state (Msg (S Z) (tag ∷ _ ∷ name ∷ [])) = do
      p ← lookup-room state name
      handle-create-room state tag name p
    -- List rooms
    handle-message state (Msg (S (S Z)) (tag ∷ _ ∷ [])) = do
      (Z ![t: Z ] ((lift tag) ∷ [(lift (RoomManagerState.rooms state) )]ᵃ))
      (strengthen (⊆-suc ⊆-refl))
      (return₁ state)
    handle-message state (Msg (S (S (S ()))) _)
    loop : ∀ {i} →
           (rms : RoomManagerState) →
           ∞ActorM i RoomManagerInterface RoomManagerState (rms-to-context rms) rms-to-context
    loop state .force = begin do
      m ← receive
      state' ← handle-message state m
      loop state'

-- =================
--  ROOM SUPERVISOR
-- =================

rs-context : TypingContext
rs-context = [ RoomManagerInterface ]ˡ

-- room-supervisor spawns the room-manager
-- and provides an interface for getting a reference to the current room-manager
-- we don't ever change that instance, but we could if we want
room-supervisor : ∀ {i} → ActorM i RoomSupervisorInterface ⊤₁ [] (λ _ → rs-context)
room-supervisor = begin do
    (spawn room-manager)
    provide-manager-instance
  where
    provide-manager-instance : ∀ {i} → ∞ActorM i RoomSupervisorInterface ⊤₁ rs-context (λ _ → rs-context)
    provide-manager-instance .force = begin do
      (Msg Z (tag ∷ _ ∷ [])) ← receive
        where (Msg (S ()) _)
      Z ![t: Z ] (lift tag ∷ [ [ S Z ]>: ⊆-refl ]ᵃ)
      (strengthen (⊆-suc ⊆-refl))
      provide-manager-instance

-- ================
--  CLIENT GENERAL
-- ================

busy-wait : ∀ {i IS Γ} → ℕ → ∞ActorM i IS ⊤₁ Γ (λ _ → Γ)
busy-wait zero = return _
busy-wait (suc n) = return tt >> busy-wait n

client-get-room-manager : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] (λ _ → [ RoomManagerInterface ]ˡ)
client-get-room-manager = do
  record { msg = Msg Z _} ← (selective-receive (λ {
    (Msg Z x₁) → true
    ; (Msg (S _) _) → false
    }))
    where
      record { msg = (Msg (S _) _) ; msg-ok = ()}
  return _

client-create-room : ∀ {i } →
                     {Γ : TypingContext} →
                     Γ ⊢ RoomManagerInterface →
                     UniqueTag →
                     RoomName →
                     ∞ActorM i ClientInterface (Lift (lsuc lzero) CreateRoomResult) Γ (λ _ → Γ)
client-create-room p tag name = do
  record { msg = (Msg (S Z) (_ ∷ cr ∷ [])) } ← (call p (S Z) tag [ lift name ]ᵃ [ S Z ]ᵐ Z)
    where
      record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () }
      record { msg = (Msg (S (S _)) _) ; msg-ok = () }
  return cr

add-if-join-success : TypingContext →
                      Lift (lsuc lzero) JoinRoomStatus →
                      TypingContext
add-if-join-success Γ (lift (JRS-SUCCESS x)) = Client-to-Room ∷ Γ
add-if-join-success Γ (lift (JRS-FAIL x)) = Γ

client-join-room : ∀ {i Γ} →
                   Γ ⊢ RoomManagerInterface →
                   UniqueTag →
                   RoomName →
                   ClientName →
                   ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus) Γ (add-if-join-success Γ)
client-join-room p tag room-name client-name = do
    self
    S p ![t: Z ] (lift tag ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ [ lift client-name ]ᵃ))
    (strengthen (⊆-suc ⊆-refl))
    m ← (selective-receive (select-join-reply tag))
    handle-message m
  where
    select-join-reply : UniqueTag → MessageFilter ClientInterface
    select-join-reply tag (Msg Z _) = false
    select-join-reply tag (Msg (S Z) _) = false
    select-join-reply tag (Msg (S (S Z)) _) = false
    select-join-reply tag (Msg (S (S (S Z))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
    select-join-reply tag (Msg (S (S (S (S Z)))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
    select-join-reply tag (Msg (S (S (S (S (S Z))))) x₁) = false
    select-join-reply tag (Msg (S (S (S (S (S (S ())))))) _)
    handle-message : ∀ {tag i Γ} → (m : SelectedMessage (select-join-reply tag)) →
                     ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus)
                       (add-selected-references Γ m) (add-if-join-success Γ)
    handle-message record { msg = (Msg Z _) ; msg-ok = () }
    handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S Z))) (_ ∷ JR-SUCCESS room-name ∷ _ ∷ [])) } = return (JRS-SUCCESS room-name)
    handle-message record { msg = (Msg (S (S (S (S Z)))) (_ ∷ JR-FAIL room-name ∷ [])) } = return (JRS-FAIL room-name)
    handle-message record { msg = (Msg (S (S (S (S (S Z))))) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) }

client-send-message : ∀ {i  Γ} →
                      Γ ⊢ Client-to-Room →
                      ClientName →
                      String →
                      ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ)
client-send-message p client-name message = p ![t: Z ] [ lift (chat-from client-name message: message) ]ᵃ

client-receive-message : ∀ {i Γ} →
                         ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) Γ (λ _ → Γ)
client-receive-message = do
    m ← (selective-receive select-message)
    handle-message m
  where
    select-message : MessageFilter ClientInterface
    select-message (Msg (S (S (S (S (S Z))))) _) = true
    select-message (Msg _ _) = false
    handle-message : ∀ {i Γ} → (m : SelectedMessage select-message) →
                     ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
    handle-message record { msg = (Msg Z _) ; msg-ok = () }
    handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S Z))) x₁) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S (S Z)))) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S (S (S Z))))) (m ∷ [])) ; msg-ok = _ } = return m
    handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) }

client-leave-room : ∀ {i Γ} →
                    Γ ⊢ Client-to-Room →
                    ClientName →
                    ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ)
client-leave-room p name = p ![t: S Z ] [ lift name ]ᵃ

debug-chat : {a : Level} {A : Set a} → ClientName → ChatMessageContent → A → A
debug-chat client-name content = let open ChatMessageContent
  in debug ("client#" || show client-name || " received \"" || content .message || "\" from client#" || show (content .sender))

-- ==========
--  CLIENT 1
-- ==========

room1-2 = 1
room2-3 = 2
room3-1 = 3
room1-2-3 = 4
name1 = 1

client1 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
client1 = begin do
  client-get-room-manager
  _ ← (client-create-room Z 0 room1-2)
  _ ← (client-create-room Z 1 room3-1)
  _ ← (client-create-room Z 2 room1-2-3)
  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room3-1 name1)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room1-2 name1)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name1)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  busy-wait 100
  (client-send-message (S Z) name1 "hi from 1 to 2")
  (client-send-message Z name1 "hi from 1 to 2-3")
  let open ChatMessageContent
  lift m1 ← client-receive-message
  lift m2 ← debug-chat name1 m1 client-receive-message
  lift m3 ← debug-chat name1 m2 client-receive-message
  debug-chat name1 m3 (client-send-message Z name1 "hi1 from 1 to 2-3")
  (client-send-message Z name1 "hi2 from 1 to 2-3")
  (client-send-message Z name1 "hi3 from 1 to 2-3")
  client-leave-room (S Z) name1
  client-leave-room (Z) name1
  (strengthen [])

-- ==========
--  CLIENT 2
-- ==========

name2 = 2

client2 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
client2 = begin do
  client-get-room-manager
  _ ← (client-create-room Z 0 room1-2)
  _ ← (client-create-room Z 1 room2-3)
  _ ← (client-create-room Z 2 room1-2-3)
  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room1-2 name2)
    where
    (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room2-3 name2)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name2)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  busy-wait 100
  debug "client2 send message" (client-send-message (S Z) name2 "hi from 2 to 3")
  debug "client2 send message" (client-send-message Z name2 "hi from 2 to 1-3")
  let open ChatMessageContent
  lift m1 ← client-receive-message
  lift m2 ← debug-chat name2 m1 client-receive-message
  lift m3 ← debug-chat name2 m2 client-receive-message
  client-leave-room (S Z) name2
  client-leave-room (Z) name2
  debug-chat name2 m3 (strengthen [])

-- ==========
--  CLIENT 3
-- ==========

name3 = 3

client3 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
client3 = begin do
  client-get-room-manager
  _ ← (client-create-room Z 0 room2-3)
  _ ← (client-create-room Z 1 room3-1)
  _ ← (client-create-room Z 2 room1-2-3)
  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room2-3 name3)
    where
    (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room3-1 name3)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name3)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  busy-wait 100
  debug "client3 send message" (client-send-message (S Z) name3 "hi from 3 to 1")
  debug "client3 send message" (client-send-message Z name3 "hi from 3 to 1-2")
  let open ChatMessageContent
  lift m1 ← client-receive-message
  lift m2 ← debug-chat name3 m1 client-receive-message
  lift m3 ← debug-chat name3 m2 client-receive-message
  debug-chat name3 m3 (client-leave-room Z name3)
  client-leave-room (S Z) name3
  client-leave-room Z name3
  (strengthen [])

-- ===================
--  CLIENT SUPERVISOR
-- ===================

cs-context : TypingContext
cs-context = RoomManagerInterface ∷ RoomSupervisorInterface ∷ []

client-supervisor : ∀ {i} → ActorM i ClientSupervisorInterface ⊤₁ [] (λ _ → cs-context)
client-supervisor = begin do
    wait-for-room-supervisor
    (get-room-manager Z 0)
    spawn-clients
  where
    wait-for-room-supervisor : ∀ {i Γ} → ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomSupervisorInterface ∷ Γ)
    wait-for-room-supervisor = do
      record { msg = Msg Z f } ← (selective-receive (λ {
        (Msg Z _) → true
        ; (Msg (S _) _) → false
        }))
        where
          record { msg = (Msg (S _) _) ; msg-ok = () }
      return _
    get-room-manager : ∀ {i Γ} →
                     Γ ⊢ RoomSupervisorInterface →
                     UniqueTag →
                      ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomManagerInterface ∷ Γ)
    get-room-manager p tag = do
      record { msg = Msg (S Z) (_ ∷  _ ∷ []) } ← (call p Z tag [] (⊆-suc ⊆-refl) Z)
        where
          record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () }
          record { msg = (Msg (S (S ())) _) }
      return _
    spawn-clients : ∀ {i} → ∞ActorM i ClientSupervisorInterface ⊤₁ cs-context (λ _ → cs-context)
    spawn-clients = do
      spawn client1
      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
      (strengthen (⊆-suc ⊆-refl))
      (spawn client2)
      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
      (strengthen (⊆-suc ⊆-refl))
      (spawn client3)
      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
      (strengthen (⊆-suc ⊆-refl))

-- chat-supervisor is the top-most actor
-- it spawns and connects the ClientRegistry to the RoomRegistry
chat-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → [])
chat-supervisor = do
    spawn room-supervisor
    spawn client-supervisor
    Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
    strengthen []

max_stars_repo_name: Zalastax/singly-typed-actors

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection utilities for ℕ
------------------------------------------------------------------------

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

module Data.Nat.Reflection where

open import Data.Nat.Base as ℕ
open import Data.Fin.Base as Fin
open import Data.List.Base using ([])
open import Reflection.Term
open import Reflection.Argument

------------------------------------------------------------------------
-- Term

toTerm : ℕ → Term
toTerm zero    = con (quote ℕ.zero) []
toTerm (suc i) = con (quote ℕ.suc)  (toTerm i ⟨∷⟩ [])

toFinTerm : ℕ → Term
toFinTerm zero    = con (quote Fin.zero) (1 ⋯⟅∷⟆ [])
toFinTerm (suc i) = con (quote Fin.suc)  (1 ⋯⟅∷⟆ toFinTerm i ⟨∷⟩ [])


text:
-- 2012-01-17 Bug found by Rob Simmons, example simplified by Nisse
-- {-# OPTIONS -v tc.proj.like:50 #-}
-- {-# OPTIONS -v tc.conv.atom:50 #-}
module Issue553b  where

data E : Set where

module M (A : Set) where

  data D : Set where
    d₁ d₂ : D

  data B : Set where
    b : D → B

  -- T must not be classified as projection-like, because of deep matching
  T : B → Set
  T (b d₁) = E
  T (b d₂) = E

  data P : B → Set where
    p : (b : B) → T b → P b

  pb : (d : D) → T (b d) → P (b d)
  pb d t = p (b d) t


text:
-- This test case was reported by Andrea Vezzosi.

{-# OPTIONS --no-guardedness #-}

open import Agda.Builtin.Size

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

data ⊥ : Set where

record T (i : Size) : Set where
  constructor con
  coinductive
  field
    force : Σ (Size< i) λ{ j → T j }

open T public

empty : ∀ i → T i → ⊥
empty i x with force x
... | j , y = empty j y

inh : T ∞
inh = λ{ .force → ∞ , inh } -- using ∞ < ∞ here

false : ⊥
false = empty ∞ inh

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

-- Some properties of 'heterogeneous' identity morphisms

module Categories.Morphism.HeterogeneousIdentity.Properties where

open import Level
open import Data.Product using (curry) renaming (_,_ to _,,_)
open import Relation.Binary.PropositionalEquality

open import Categories.Category using (Category; _[_,_]; _[_≈_])
open import Categories.Category.Product
open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Morphism.HeterogeneousIdentity

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ : Level

open Category using (Obj; id)

-- Functor identity laws lifted to heterogeneous identities.

hid-identity : (C : Category o ℓ e) (D : Category o′ ℓ′ e′)
               {F₀ : Obj C → Obj D}
               (F₁ : ∀ {A B} → C [ A , B ] → D [ F₀ A , F₀ B ]) →
               (∀ {A} → D [ F₁ (id C {A}) ≈ id D ]) →
               ∀ {A B} (p : A ≡ B) → D [ F₁ (hid C p) ≈ hid D (cong F₀ p) ]
hid-identity C D F₁ hyp refl = hyp

hid-identity₂ : (C₁ : Category o ℓ e) (C₂ : Category o′ ℓ′ e′)
                (D : Category o″ ℓ″ e″)
                {F₀ : Obj C₁ → Obj C₂ → Obj D}
                (F₁ : ∀ {A₁ A₂ B₁ B₂} → C₁ [ A₁ , B₁ ] → C₂ [ A₂ , B₂ ] →
                      D [ F₀ A₁ A₂ , F₀ B₁ B₂ ]) →
                (∀ {A₁ A₂} → D [ F₁ (id C₁ {A₁}) (id C₂ {A₂}) ≈ id D ]) →
                ∀ {A₁ A₂ B₁ B₂} (p : A₁ ≡ B₁) (q : A₂ ≡ B₂) →
                D [ F₁ (hid C₁ p) (hid C₂ q) ≈ hid D (cong₂ F₀ p q) ]
hid-identity₂ C₁ C₂ D F₁ hyp refl refl = hyp

module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
         (F : Functor C D) where
  open Category D
  open Functor F

  -- functors preserve heterogeneous identities

  F-hid : ∀ {A B} (p : A ≡ B) → F₁ (hid C p) ≈ hid D (cong F₀ p)
  F-hid = hid-identity C D F₁ identity

module _ {C₁ : Category o ℓ e} {C₂ : Category o′ ℓ′ e′}
         {D : Category o″ ℓ″ e″} (F : Bifunctor C₁ C₂ D) where
  open Category D
  open Functor F

  -- bifunctors preserve heterogeneous identities

  BF-hid : ∀ {A₁ A₂ B₁ B₂} (p : A₁ ≡ B₁) (q : A₂ ≡ B₂) →
           F₁ (hid C₁ p ,, hid C₂ q) ≈ hid D (cong₂ (curry F₀) p q)
  BF-hid = hid-identity₂ C₁ C₂ D (curry F₁) identity

module _ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) where
  open Category (Product C D)

  -- products preserve heterogeneous identities

  ×-hid : ∀ {A₁ A₂ B₁ B₂} (p : A₁ ≡ B₁) (q : A₂ ≡ B₂) →
          (hid C p ,, hid D q) ≈ hid (Product C D) (cong₂ _,,_ p q)
  ×-hid p q = BF-hid {C₁ = C} {C₂ = D} (idF ⁂ idF) p q

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module PrintFloat where
import AlonzoPrelude
import PreludeShow
import PreludeList
import PreludeString
import PreludeNat

open AlonzoPrelude
open PreludeShow
open PreludeList, hiding(_++_)
open PreludeString
open PreludeNat

typeS : Char -> Set
typeS 'f' = Float

show : (c : Char) -> (typeS c) -> String
show 'f' f = showFloat f

data Unit : Set where
  unit : Unit

data Format : Set where
  stringArg : Format
  natArg    : Format
  intArg    : Format
  floatArg  : Format
  charArg   : Format
  litChar   : Char -> Format
  badFormat : Char -> Format

data BadFormat (c:Char) : Set where

format' : List Char -> List Format
format' ('%' :: 's' :: fmt) = stringArg   :: format' fmt
format' ('%' :: 'n' :: fmt) = natArg      :: format' fmt
-- format' ('%' :: 'd' :: fmt) = intArg      :: format' fmt
format' ('%' :: 'f' :: fmt) = floatArg    :: format' fmt
format' ('%' :: 'c' :: fmt) = charArg     :: format' fmt
format' ('%' :: '%' :: fmt) = litChar '%' :: format' fmt
format' ('%' ::  c  :: fmt) = badFormat c :: format' fmt
format' (c		:: fmt) = litChar c   :: format' fmt
format'  []		= []

format : String -> List Format
format s = format' (toList s)

-- Printf1 : Format -> Set
-- Printf1 floatArg = Float

Printf' : List Format -> Set
Printf' (stringArg   :: fmt) = String  × Printf' fmt
Printf' (natArg      :: fmt) = Nat     × Printf' fmt
Printf' (intArg      :: fmt) = Int     × Printf' fmt
Printf' (floatArg    :: fmt) = Float   × Printf' fmt
Printf' (charArg     :: fmt) = Char    × Printf' fmt
Printf' (badFormat c :: fmt) = BadFormat c
Printf' (litChar _   :: fmt) = Printf' fmt
Printf'  []		     = Unit × Unit

Printf : String -> Set
Printf fmt = Printf' (format fmt)

printf' : (fmt : List Format) -> Printf' fmt -> String
printf' (stringArg   :: fmt) < s | args > = s ++ printf' fmt args
printf' (natArg      :: fmt) < n | args > = showNat n ++ printf' fmt args
printf' (intArg      :: fmt) < n | args > = showInt n ++ printf' fmt args
printf' (floatArg    :: fmt) < x | args > = showFloat x ++ printf' fmt args
printf' (charArg     :: fmt) < c | args > = showChar c ++ printf' fmt args
printf' (litChar c   :: fmt) args = fromList (c :: []) ++ printf' fmt args
printf' (badFormat _ :: fmt) ()
printf'  []		 < unit | unit >	    = ""

printf : (fmt : String) -> Printf fmt -> String
printf fmt = printf' (format fmt)

-- mainS = show 'f' 3.14
-- mainS = printf' (format "%f") < 3.14 | < unit | unit > >
mainS = printf "pi = %f" < 3.14159 | < unit | unit > >
-- mainS = fromList ( 'p' :: [] )

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

open import HoTT

module homotopy.CoHSpace where

record CoHSpaceStructure {i} (X : Ptd i) : Type i where
  constructor coHSpaceStructure
  field
    ⊙coμ : X ⊙→ X ⊙∨ X

  coμ : de⊙ X → X ∨ X
  coμ = fst ⊙coμ

  field
    ⊙unit-l : ⊙projr ⊙∘ ⊙coμ ⊙∼ ⊙idf X
    ⊙unit-r : ⊙projl ⊙∘ ⊙coμ ⊙∼ ⊙idf X

{-
module _ {i j : ULevel} {X : Ptd i} (CHSS : CoHSpaceStructure X) where

  open CoHSpaceStructure CHSS

  private
    lemma-l : ⊙projr ⊙∘ ⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j}) ⊙∘ ⊙coμ ⊙∘ ⊙lower {j = j}
           == ⊙idf _
  abstract
    lemma-l =
        ! (⊙λ= (⊙∘-assoc ⊙projr (⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j})) (⊙coμ ⊙∘ ⊙lower {j = j})))
      ∙ ap (_⊙∘ ⊙coμ ⊙∘ ⊙lower) (⊙λ= (⊙Wedge-rec-fmap ⊙cst (⊙idf _) (⊙lift {j = j}) (⊙lift {j = j})))
      ∙ ap (_⊙∘ ⊙coμ ⊙∘ ⊙lower) (! (⊙λ= (⊙Wedge-rec-post∘ (⊙lift {j = j}) ⊙cst (⊙idf _))))
      ∙ ⊙λ= (⊙∘-assoc (⊙lift {j = j}) ⊙projr (⊙coμ ⊙∘ ⊙lower {j = j}))
      ∙ ap (λ f → ⊙lift {j = j} ⊙∘ f ⊙∘ ⊙lower {j = j}) (⊙λ= ⊙unit-l)

  private
    lemma-r : ⊙projl ⊙∘ ⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j}) ⊙∘ ⊙coμ ⊙∘ ⊙lower {j = j}
           == ⊙idf _
  abstract
    lemma-r =
        ! (⊙λ= (⊙∘-assoc ⊙projl (⊙∨-fmap (⊙lift {j = j}) (⊙lift {j = j})) (⊙coμ ⊙∘ ⊙lower {j = j})))
      ∙ ap (_⊙∘ ⊙coμ ⊙∘ ⊙lower) (⊙λ= (⊙Wedge-rec-fmap (⊙idf _) ⊙cst (⊙lift {j = j}) (⊙lift {j = j})))
      ∙ ap (_⊙∘ ⊙coμ ⊙∘ ⊙lower) (! (⊙λ= (⊙Wedge-rec-post∘ (⊙lift {j = j}) (⊙idf _) ⊙cst)))
      ∙ ⊙λ= (⊙∘-assoc (⊙lift {j = j}) ⊙projl (⊙coμ ⊙∘ ⊙lower {j = j}))
      ∙ ap (λ f → ⊙lift {j = j} ⊙∘ f ⊙∘ ⊙lower {j = j}) (⊙λ= ⊙unit-r)

  Lift-co-h-space-structure : CoHSpaceStructure (⊙Lift {j = j} X)
  Lift-co-h-space-structure = record
    { ⊙coμ = ⊙∨-fmap ⊙lift ⊙lift ⊙∘ ⊙coμ ⊙∘ ⊙lower
    ; ⊙unit-l = ⊙app= lemma-l
    ; ⊙unit-r = ⊙app= lemma-r
    }
-}


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

module Data.Fin.Subset.Properties where

open import Algebra
import Algebra.Properties.BooleanAlgebra as BoolProp
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin); open Data.Fin.Fin
open import Data.Fin.Subset
open import Data.Nat using (ℕ)
open import Data.Product
open import Data.Sum as Sum
open import Data.Vec hiding (_∈_)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

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

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

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

------------------------------------------------------------------------
-- Properties involving ⊥

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

⊥⊆ : ∀ {n} {p : Subset n} → ⊥ ⊆ p
⊥⊆ x∈⊥ with ∉⊥ x∈⊥
... | ()

Empty-unique : ∀ {n} {p : Subset n} →
               Empty p → p ≡ ⊥
Empty-unique {p = []}           ¬∃∈ = P.refl
Empty-unique {p = s ∷ p}        ¬∃∈ with Empty-unique (drop-∷-Empty ¬∃∈)
Empty-unique {p = outside ∷ .⊥} ¬∃∈ | P.refl = P.refl
Empty-unique {p = inside  ∷ .⊥} ¬∃∈ | P.refl =
  ⊥-elim (¬∃∈ (zero , here))

------------------------------------------------------------------------
-- Properties involving ⊤

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

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

------------------------------------------------------------------------
-- A property involving ⁅_⁆

x∈⁅y⁆⇔x≡y : ∀ {n} {x y : Fin n} → x ∈ ⁅ y ⁆ ⇔ x ≡ y
x∈⁅y⁆⇔x≡y {x = x} {y} =
  equivalence (to y) (λ x≡y → P.subst (λ y → x ∈ ⁅ y ⁆) x≡y (x∈⁅x⁆ x))
  where

  to : ∀ {n x} (y : Fin n) → x ∈ ⁅ y ⁆ → x ≡ y
  to (suc y) (there p) = P.cong suc (to y p)
  to zero    here      = P.refl
  to zero    (there p) with ∉⊥ p
  ... | ()

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

------------------------------------------------------------------------
-- A property involving _∪_

∪⇔⊎ : ∀ {n} {p₁ p₂ : Subset n} {x} → x ∈ p₁ ∪ p₂ ⇔ (x ∈ p₁ ⊎ x ∈ p₂)
∪⇔⊎ = equivalence (to _ _) from
  where
  to : ∀ {n} (p₁ p₂ : Subset n) {x} → x ∈ p₁ ∪ p₂ → x ∈ p₁ ⊎ x ∈ p₂
  to []             []             ()
  to (inside  ∷ p₁) (s₂      ∷ p₂) here            = inj₁ here
  to (outside ∷ p₁) (inside  ∷ p₂) here            = inj₂ here
  to (s₁      ∷ p₁) (s₂      ∷ p₂) (there x∈p₁∪p₂) =
    Sum.map there there (to p₁ p₂ x∈p₁∪p₂)

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

  ⊆∪ʳ : ∀ {n} (p₁ p₂ : Subset n) → p₂ ⊆ p₁ ∪ p₂
  ⊆∪ʳ p₁ p₂ rewrite BooleanAlgebra.∨-comm (booleanAlgebra _) p₁ p₂
    = ⊆∪ˡ p₁

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

------------------------------------------------------------------------
-- _⊆_ is a partial order

-- The "natural poset" associated with the boolean algebra.

module NaturalPoset where
  private
    open module BA {n} = BoolProp (booleanAlgebra n) public
      using (poset)
    open module Po {n} = Poset (poset {n = n}) public

  -- _⊆_ is equivalent to the natural lattice order.

  orders-equivalent : ∀ {n} {p₁ p₂ : Subset n} → p₁ ⊆ p₂ ⇔ p₁ ≤ p₂
  orders-equivalent = equivalence (to _ _) (from _ _)
    where
    to : ∀ {n} (p₁ p₂ : Subset n) → p₁ ⊆ p₂ → p₁ ≤ p₂
    to []             []             p₁⊆p₂ = P.refl
    to (inside  ∷ p₁) (_       ∷ p₂) p₁⊆p₂ with p₁⊆p₂ here
    to (inside  ∷ p₁) (.inside ∷ p₂) p₁⊆p₂ | here = P.cong (_∷_ inside)  (to p₁ p₂ (drop-∷-⊆ p₁⊆p₂))
    to (outside ∷ p₁) (_       ∷ p₂) p₁⊆p₂        = P.cong (_∷_ outside) (to p₁ p₂ (drop-∷-⊆ p₁⊆p₂))

    from : ∀ {n} (p₁ p₂ : Subset n) → p₁ ≤ p₂ → p₁ ⊆ p₂
    from []             []       p₁≤p₂ x               = x
    from (.inside ∷ _)  (_ ∷ _)  p₁≤p₂ here            rewrite P.cong head p₁≤p₂ = here
    from (_       ∷ p₁) (_ ∷ p₂) p₁≤p₂ (there xs[i]=x) =
      there (from p₁ p₂ (P.cong tail p₁≤p₂) xs[i]=x)

-- _⊆_ is a partial order.

poset : ℕ → Poset _ _ _
poset n = record
  { Carrier        = Subset n
  ; _≈_            = _≡_
  ; _≤_            = _⊆_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = P.isEquivalence
      ; reflexive     = λ i≡j → from ⟨$⟩ reflexive i≡j
      ; trans         = λ x⊆y y⊆z → from ⟨$⟩ trans (to ⟨$⟩ x⊆y) (to ⟨$⟩ y⊆z)
      }
    ; antisym = λ x⊆y y⊆x → antisym (to ⟨$⟩ x⊆y) (to ⟨$⟩ y⊆x)
    }
  }
  where
  open NaturalPoset
  open module E {p₁ p₂} =
    Equivalence (orders-equivalent {n = n} {p₁ = p₁} {p₂ = p₂})


text:
{-

  - UARel given by a universe and equivalences
  - SubstRel and DUARel for the element family over the universe

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Displayed.Universe where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Displayed.Base
open import Cubical.Displayed.Subst

private
  variable
    ℓA ℓ≅A ℓB ℓ≅B ℓP : Level

𝒮-Univ : ∀ ℓ → UARel (Type ℓ) ℓ
𝒮-Univ ℓ .UARel._≅_ = _≃_
𝒮-Univ ℓ .UARel.ua _ _ = isoToEquiv (invIso univalenceIso)

𝒮ˢ-El : ∀ ℓ → SubstRel (𝒮-Univ ℓ) (λ X → X)
𝒮ˢ-El ℓ .SubstRel.act e = e
𝒮ˢ-El ℓ .SubstRel.uaˢ e a = uaβ e a

𝒮ᴰ-El : ∀ ℓ → DUARel (𝒮-Univ ℓ) (λ X → X) ℓ
𝒮ᴰ-El ℓ .DUARel._≅ᴰ⟨_⟩_  a e a' = e .fst a ≡ a'
𝒮ᴰ-El ℓ .DUARel.uaᴰ a e a' = invEquiv (ua-ungluePath-Equiv e)

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module nodcap.Show where

open import Coinduction
open import Category.Monad.State using (State; StateMonadState; module RawMonadState)
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Nat.Show as ℕS using ()
open import Data.Fin as F using (Fin; suc; zero)
open import Data.Pos as ℕ⁺
open import Data.List as L using (List; []; _∷_; length)
open import Data.List.Any as LA using (Any; here; there)
open import Data.List.Any.Properties as LAP using (++ˡ; ++ʳ)
open import Data.Product as PR using (proj₁)
open import Data.String as S using (String; _++_)
open import Data.Stream as X using (Stream; _∷_; lookup)
open import Data.Vec as V using (Vec)
open import Function using (_∘_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as I using ()
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)

open import Data.Environment
open import nodcap.Base
open import nodcap.Typing

open I.Inverse using (to; from)

showTerm : {Γ : Environment} → ⊢ Γ → String
showTerm {Γ} x = proj₁ (go bound x state)
  where
    open RawMonadState (StateMonadState (Stream String))

    names : Stream String
    names = X.map (("x" S.++_) ∘ ℕS.show) (naturals 0)
      where
        naturals : ℕ → Stream ℕ
        naturals n = n ∷ ♯ naturals (suc n)

    fresh : State (Stream String) String
    fresh = get >>= λ{(x ∷ xs) → put (♭ xs) >> return x}

    go : {Γ : Environment} (bound : {w : Type} → w ∈ Γ → String) → ⊢ Γ → State (Stream String) String
    go bound ax
      = return (boundˣ ++ "<->" ++ boundʸ)
      where
        boundˣ = bound (here P.refl)
        boundʸ = bound (there (here P.refl))
    go bound (cut {Γ} {Δ} {A} x y) = fresh >>= withFresh
      where
        withFresh : String → State (Stream String) String
        withFresh boundˣ
          = go bound₁ x >>= λ x'
          → go bound₂ y >>= λ y'
          → return ("new " ++ boundˣ ++ ".(" ++ x' ++ "|" ++ y' ++ ")")
          where
            bound₁ : {w : Type} → w ∈ A ∷ Γ → String
            bound₁ (here px) = boundˣ
            bound₁ (there i) = bound (++ˡ i)
            bound₂ : {w : Type} → w ∈ A ^ ∷ Δ → String
            bound₂ (here px) = boundˣ
            bound₂ (there i) = bound (++ʳ Γ i)
    go bound (send {Γ} {Δ} {A} {B} x y) = fresh >>= withFresh
      where
        withFresh : String → State (Stream String) String
        withFresh boundʸ
          = go bound₁ x >>= λ x'
          → go bound₂ y >>= λ y'
          → return (boundˣ ++ "[" ++ boundʸ ++ "].(" ++ x' ++ "|" ++ y' ++ ")")
          where
            boundˣ = bound (here P.refl)
            bound₁ : {w : Type} → w ∈ A ∷ Γ → String
            bound₁ (here px) = boundʸ
            bound₁ (there i) = bound (there (++ˡ i))
            bound₂ : {w : Type} → w ∈ B ∷ Δ → String
            bound₂ (here px) = bound (here P.refl)
            bound₂ (there i) = bound (there (++ʳ Γ i))
    go bound (recv {Γ} {A} {B} x) = fresh >>= withFresh
      where
        withFresh : String → State (Stream String) String
        withFresh boundʸ
          = go bound₁ x >>= λ x'
          → return (boundˣ ++ "(" ++ boundʸ ++ ")." ++ x')
          where
            boundˣ = bound (here P.refl)
            bound₁ : {w : Type} → w ∈ A ∷ B ∷ Γ → String
            bound₁ (here px) = boundʸ
            bound₁ (there (here px)) = boundˣ
            bound₁ (there (there i)) = bound (there i)
    go bound (sel₁ {Γ} {A} {B} x)
      = go bound₁ x >>= λ x'
      → return (boundˣ ++ "[inl]." ++ x')
      where
        boundˣ = bound (here P.refl)
        bound₁ : {w : Type} → w ∈ A ∷ Γ → String
        bound₁ (here px) = boundˣ
        bound₁ (there i) = bound (there i)
    go bound (sel₂ {Γ} {A} {B} x)
      = go bound₁ x >>= λ x'
      → return (boundˣ ++ "[inr]." ++ x')
      where
        boundˣ = bound (here P.refl)
        bound₁ : {w : Type} → w ∈ B ∷ Γ → String
        bound₁ (here px) = boundˣ
        bound₁ (there i) = bound (there i)
    go bound (case {Γ} {A} {B} x y)
      = go bound₁ x >>= λ x'
      → go bound₂ y >>= λ y'
      → return ("case " ++ boundˣ ++ " {" ++ x' ++ ";" ++ y' ++ "}")
      where
        boundˣ = bound (here P.refl)
        bound₁ : {w : Type} → w ∈ A ∷ Γ → String
        bound₁ (here px) = boundˣ
        bound₁ (there i) = bound (there i)
        bound₂ : {w : Type} → w ∈ B ∷ Γ → String
        bound₂ (here px) = boundˣ
        bound₂ (there i) = bound (there i)
    go bound halt
      = return (boundˣ ++ "[].0")
      where
        boundˣ = bound (here P.refl)
    go bound (wait x)
      = go (bound ∘ there) x >>= λ x'
      → return (boundˣ ++ "()." ++ x')
      where
        boundˣ = bound (here P.refl)
    go bound loop
      = return ("case " ++ boundˣ ++ " {;}")
      where
        boundˣ = bound (here P.refl)
    go bound (mk?₁ {Γ} {A} x) = fresh >>= withFresh
      where
        withFresh : String → State (Stream String) String
        withFresh boundʸ
          = go bound₁ x >>= λ x'
          → return ("?" ++ boundˣ ++ "[" ++ boundʸ ++ "]." ++ x')
          where
            boundˣ = bound (here P.refl)
            bound₁ : {w : Type} → w ∈ A ∷ Γ → String
            bound₁ (here px) = boundʸ
            bound₁ (there i) = bound (there i)
    go bound (mk!₁ {Γ} {A} x) = fresh >>= withFresh
      where
        withFresh : String → State (Stream String) String
        withFresh boundʸ
          = go bound₁ x >>= λ x'
          → return ("!" ++ boundˣ ++ "(" ++ boundʸ ++ ")." ++ x')
          where
            boundˣ = bound (here P.refl)
            bound₁ : {w : Type} → w ∈ A ∷ Γ → String
            bound₁ (here px) = boundʸ
            bound₁ (there i) = bound (there i)
    go bound (cont {Γ} {A} {m} {n} x)
      = go bound₁ x
      where
        boundˣ = bound (here P.refl)
        bound₁ : {w : Type} → w ∈ ?[ m ] A ∷ ?[ n ] A ∷ Γ → String
        bound₁ (here px) = boundˣ
        bound₁ (there (here px)) = boundˣ
        bound₁ (there (there i)) = bound (there i)
    go bound (pool {Γ} {Δ} {A} {m} {n} x y)
      = go bound₁ x >>= λ x'
      → go bound₂ y >>= λ y'
      → return ("(" ++ x' ++ "|" ++ y' ++ ")")
      where
        boundˣ = bound (here P.refl)
        bound₁ : {w : Type} → w ∈ ![ m ] A ∷ Γ → String
        bound₁ (here px) = boundˣ
        bound₁ (there i) = bound (there (++ˡ i))
        bound₂ : {w : Type} → w ∈ ![ n ] A ∷ Δ → String
        bound₂ (here px) = boundˣ
        bound₂ (there i) = bound (there (++ʳ Γ i))
    go bound (exch b x) = go (bound ∘ (to b ⟨$⟩_)) x

    bound : {w : Type} → w ∈ Γ → String
    bound i = V.lookup (toFin i) (X.take (length Γ) names)
      where
        toFin : {Γ : Environment} {w : Type} → w ∈ Γ → Fin (length Γ)
        toFin (here px) = zero
        toFin (there i) = suc (toFin i)

    state : Stream String
    state = X.drop (length Γ) names

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
-- Andreas, 2016-12-20, issue #2348

-- {-# OPTIONS -v tc.proj.like:100 #-}

{-# OPTIONS --show-implicit #-} -- NEEDED

-- something projection like

record Wrap (A : Set) : Set where
  field out : A

proj-like : {{A : Set}} {{r : Wrap A}} → A
proj-like {{r = r}} = Wrap.out r

-- display term with projection like thing

postulate
  B : Set
  b : B
  P : B → Set
  p : P b
  instance
    w : Wrap B

ok = proj-like {{B}} {{r = w}}

test : P (proj-like {{B}})
test = p  -- triggers error message

-- EXPECTED ERROR:
-- b != Wrap.out w of type B
-- when checking that the expression p has type P (proj-like {{r = w}})

max_forks_repo_name: Agda-zh/agda


text:
module Syntax.Function where

import      Lvl
open import Type
open import Syntax.Type

private variable ℓ : Lvl.Level
private variable T A B C : Type{ℓ}

infix 2 [↦] [⤠] [⤇]

-- Custom syntax for an anonymous function
-- Example:
--   f : A → A
--   f = a ↦ a
--
--   g : (A → A → A) → (A → A → A)
--   g(_▫_) = a₁ ↦ a₂ ↦ (a₁ ▫ a₂)
[↦] : T → T
[↦] x = x
syntax [↦](\x → y) = x ↦ y
{-# DISPLAY [↦] x = x #-}

-- Custom syntax for an anonymous function with an implicit argument
-- Example:
--   f : A → A
--   f = a ↦ a
[⤠] : (A → B) → ({A} → B)
[⤠] f{x} = f(x)
syntax [⤠](\x → y) = x ⤠ y
{-# DISPLAY [⤠] x = x #-}

-- Custom syntax for an anonymous function with an instance argument
[⤇] : (A → B) → (⦃ _ : A ⦄ → B)
[⤇] f ⦃ x ⦄ = f(x)
syntax [⤇](\x → y) = x ⤇ y
{-# DISPLAY [⤇] x = x #-}

-- Functions with two parameters as an infix binary operator
_⦗_⦘_ : A → (A → B → C) → B → C
a ⦗ op ⦘ b = op a b

infix  10000 _⦗_⦘_
infixl 10000 _⦗_⦘ₗ_
infixr 10000 _⦗_⦘ᵣ_

_⦗_⦘ₗ_ = _⦗_⦘_
_⦗_⦘ᵣ_ = _⦗_⦘_

{- TODO: Fix these with stuff in Lang.Function
f : {a : A} → A
f = (a ⤠ a)

g : ⦃ a₁ : A ⦄ ⦃ a₂ : A ⦄ → A
g = (a₁ ⤇ a₂ ⤇ a₁)
-}


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

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

map : ∀ {a b}{A : Set a}{B : Set b} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

reverse : ∀ {a}{A : Set a} → List A → List A
reverse {A = A} xs = reverseAcc xs []
  where
    reverseAcc : List A → List A → List A
    reverseAcc [] a = a
    reverseAcc (x ∷ xs) a = reverseAcc xs (x ∷ a)

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

infixr 5 _∷_
data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

data Ix : (d : Nat) → (s : Vec Nat d) → Set where
  []   : Ix 0 []
  _∷_  : ∀ {d s x} → Fin x → (ix : Ix d s) → Ix (suc d) (x ∷ s)

record Ar {a} (X : Set a) (d : Nat) (s : Vec Nat d) : Set a where
  constructor imap
  field sel : Ix d s → X
open Ar public

foo : Nat → Nat
foo x = 1 + x

test-ar : ∀ {n} → (a : Ar Nat 1 (n ∷ [])) → Ar Nat 1 (n ∷ [])
test-ar (imap f) = imap λ iv → foo $ foo $ f iv

-- Make sure that the telescope is also reconstructed when
-- calling getDefinition with withReconstructed.
macro
  z : Name → Term → TC ⊤
  z n hole = do
    (function (clause tel ps t ∷ [])) ←
      withReconstructed $ getDefinition n
      where _ → quoteTC "ERROR" >>= unify hole
    t ← withReconstructed
        $ inContext (reverse tel)
        $ normalise t
    quoteTC t >>= unify hole

test₁ : z test-ar
      ≡ con (quote imap) (_ ∷ _ ∷ _ ∷ _ ∷
                          arg _ (lam _ (abs "iv"
                                        (con (quote Nat.suc) _)))
                          ∷ [])
test₁ = refl

-- Make sure that getType behaves correctly under withReconstructed.
macro
  q : Name → Term → TC ⊤
  q n hole = do
    t ← withReconstructed $
        getType n
    t ← withReconstructed $
        normalise t
    quoteTC t >>= unify hole

test₂ : Term
test₂ = q test-ar


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of constructions over unary relations
------------------------------------------------------------------------

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

module Relation.Unary.Properties where

open import Data.Product using (_×_; _,_; swap; proj₁)
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Unit using (tt)
open import Relation.Binary.Core hiding (Decidable)
open import Relation.Unary
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Nullary.Negation using (¬?)
open import Function using (_$_; _∘_)

----------------------------------------------------------------------
-- The empty set

module _ {a} {A : Set a} where

  ∅? : Decidable {A = A} ∅
  ∅? _ = no λ()

  ∅-Empty : Empty {A = A} ∅
  ∅-Empty x ()

  ∁∅-Universal : Universal {A = A} (∁ ∅)
  ∁∅-Universal = λ x x∈∅ → x∈∅

----------------------------------------------------------------------
-- The universe

module _ {a} {A : Set a} where

  U? : Decidable {A = A} U
  U? _ = yes tt

  U-Universal : Universal {A = A} U
  U-Universal = λ _ → _

  ∁U-Empty : Empty {A = A} (∁ U)
  ∁U-Empty = λ x x∈∁U → x∈∁U _

----------------------------------------------------------------------
-- Subset properties

module _ {a ℓ} {A : Set a} where

  ∅-⊆ : (P : Pred A ℓ) → ∅ ⊆ P
  ∅-⊆ P ()

  ⊆-U : (P : Pred A ℓ) → P ⊆ U
  ⊆-U P _ = _

  ⊆-refl : Reflexive (_⊆_ {A = A} {ℓ})
  ⊆-refl x∈P = x∈P

  ⊆-trans : Transitive (_⊆_ {A = A} {ℓ})
  ⊆-trans P⊆Q Q⊆R x∈P = Q⊆R (P⊆Q x∈P)

  ⊂-asym : Asymmetric (_⊂_ {A = A} {ℓ})
  ⊂-asym (_ , Q⊈P) = Q⊈P ∘ proj₁

----------------------------------------------------------------------
-- Decidability properties

module _ {a} {A : Set a} where

  ∁? : ∀ {ℓ} {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
  ∁? P? x = ¬? (P? x)

  _∪?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
         Decidable P → Decidable Q → Decidable (P ∪ Q)
  _∪?_ P? Q? x = (P? x) ⊎-dec (Q? x)

  _∩?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
         Decidable P → Decidable Q → Decidable (P ∩ Q)
  _∩?_ P? Q? x = (P? x) ×-dec (Q? x)

module _ {a b} {A : Set a} {B : Set b} where

  _×?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred B ℓ₂} →
         Decidable P → Decidable Q → Decidable (P ⟨×⟩ Q)
  _×?_ P? Q? (a , b) = (P? a) ×-dec (Q? b)

  _⊙?_ : ∀ {ℓ₁ ℓ₂} {P : Pred A ℓ₁} {Q : Pred B ℓ₂} →
         Decidable P → Decidable Q → Decidable (P ⟨⊙⟩ Q)
  _⊙?_ P? Q? (a , b) = (P? a) ⊎-dec (Q? b)

  _⊎?_ : ∀ {ℓ} {P : Pred A ℓ} {Q : Pred B ℓ} →
         Decidable P → Decidable Q → Decidable (P ⟨⊎⟩ Q)
  _⊎?_ P? Q? (inj₁ a) = P? a
  _⊎?_ P? Q? (inj₂ b) = Q? b

  _~? : ∀ {ℓ} {P : Pred (A × B) ℓ} →
        Decidable P → Decidable (P ~)
  _~? P? = P? ∘ swap