text:
module Typed.LTLC where

open import Prelude
open import Function
open import Level
open import Category.Monad

open import Relation.Unary.PredicateTransformer using (PT; Pt)
open import Relation.Ternary.Separation.Construct.Unit
open import Relation.Ternary.Separation.Allstar
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad.Reader
open import Relation.Ternary.Separation.Monad.Delay

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

open import Relation.Ternary.Separation.Construct.List Ty

Ctx  = List Ty
CtxT = List Ty → List Ty

infixr 20 _◂_
_◂_ : Ty → CtxT → CtxT
(x ◂ f) Γ = x ∷ f Γ

variable a b : Ty
variable ℓv  : Level
variable τ   : Set ℓv
variable Γ Γ₁ Γ₂ Γ₃ : List τ

data Exp : Ty → Ctx → Set where
  -- a base type
  tt       : ε[ Exp unit ]
  letunit  : ∀[ Exp unit ✴ Exp a ⇒ Exp a ]

  -- the λ-calculus
  lam : ∀[ (a ◂ id ⊢ Exp b) ⇒ Exp (a ⊸ b) ]
  ap  : ∀[ Exp (a ⊸ b) ✴ Exp a ⇒ Exp b ]
  var : ∀[ Just a ⇒ Exp a ]

module _ {{m : MonoidalSep 0ℓ}} where
  open MonoidalSep m using (Carrier)

  CPred : Set₁
  CPred = Carrier → Set

  mutual
    Env : Ctx → CPred
    Env = Allstar Val

    data Val : Ty → CPred where
      tt    : ε[ Val unit ]
      clos  : Exp b (a ∷ Γ) → ∀[ Env Γ ⇒ Val (a ⊸ b) ]

  module _ {i : Size} where
    open ReaderTransformer id-morph Val (Delay i) public
    open Monads.Monad reader-monad public

  M : Size → (Γ₁ Γ₂ : Ctx) → CPred → CPred
  M i = Reader {i}

  open Monads using (str; _&_; typed-str)

  mutual
    eval : ∀ {i} → Exp a Γ → ε[ M i Γ ε (Val a) ]

    eval tt = do
      return tt

    eval (letunit (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
      tt ← frame Γ≺ (►eval e₁)
      ►eval e₂

    eval (lam e) = do
      env ← ask
      return (clos e env)

    eval (ap (f ×⟨ Γ≺ ⟩ e)) = do
      clos body env ← frame Γ≺ (►eval f)
      v ×⟨ σ ⟩ env  ← ►eval e & env
      empty         ← append (v :⟨ σ ⟩: env)
      ►eval body

    eval (var refl) = do
      lookup

    ►eval : ∀ {i} → Exp a Γ → ε[ M i Γ ε (Val a) ]
    app (►eval e) E σ = later (λ where .force → app (eval e) E σ)


text:
-- Andreas, 2022-06-10, issue #5922, reported by j-towns.
-- Lack of normalization of data projections against data constructors
-- breaks termination checker applied to extended lambda gone through
-- forcing translation and reflection.

-- The workaround was to turn off the forcing translation:
-- {-# OPTIONS --no-forcing #-}

-- {-# OPTIONS -v term:20 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

data Fin : Nat → Set where
  fz : (b : Nat)         → Fin (suc b)
  fs : (b : Nat) → Fin b → Fin (suc b)

apply : {A B C : Set} (input : A) (f : A → B) (cont : B → C) → C
apply input f cont = cont (f input)

macro
  id-macro : (b : Nat) → (Fin b → Nat) → Term → TC ⊤
  id-macro b f hole =
    bindTC (quoteTC f) λ f-term →
    unify hole f-term

test : (b : Nat) → Fin b → Nat
test b = id-macro b λ where
  (fz _)   → zero
  (fs a x) → apply x (test a) suc

-- Should termination check.

-- WAS:
-- Termination checking failed for the following functions:
--   test
-- Problematic calls:
--   λ { (fz .(Agda.Builtin.Nat.suc-0 _)) → zero
--     ; (fs .(Agda.Builtin.Nat.suc-0 _) x)
--         → apply x
--           (test (Agda.Builtin.Nat.suc-0 (suc (Agda.Builtin.Nat.suc-0 b))))
--           suc
--     }
--   test (Agda.Builtin.Nat.suc-0 (suc b))
--
-- This shows data projection Agda.Builtin.Nat.suc-0 applied to data constructor
-- suc, which should be normalized away.

ext: agda


text:
module _ where

module M where
  private
    module _ (A : Set) where
      Id : Set
      Id = A

  foo : Set → Set
  foo A = Id A

open M

bar : Set → Set
bar A = Id A -- Id should not be in scope

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

   Copyright (c) 2020 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 LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.Encode
open import LibraBFT.Base.ByteString

-- This module defines Hash functions, and related properties

module LibraBFT.Hash where

 -------------------------------------------------
 -- Hash function postulates
 --
 -- We are now assuming that our 'auth' function is collision
 -- resistant. We might be able to carry the full proof in agda,
 -- but that can take place on another module.

 Hash : Set
 Hash = Σ ByteString (λ bs → length bs ≡ 4)

 hashLen-pi : ∀ {bs : ByteString} {n : ℕ } → (p1 p2 : length bs ≡ n) → p1 ≡ p2
 hashLen-pi {[]}    {.0} refl refl = refl
 hashLen-pi {h ∷ t} {.(suc (length t))} refl refl = refl

 sameBS⇒sameHash : ∀ {h1 h2 : Hash}
         → proj₁ h1 ≡ proj₁ h2
         → h1 ≡ h2
 sameBS⇒sameHash { h1a , h1b } { h2a , h2b } refl rewrite hashLen-pi {h2a} h1b h2b = refl

 _≟Hash_ : (h₁ h₂ : Hash) → Dec (h₁ ≡ h₂)
 (l , pl) ≟Hash (m , pm) with List-≡-dec (Vec-≡-dec _≟Bool_) l m
 ...| yes refl = yes (cong (_,_ l) (≡-pi pl pm))
 ...| no  abs  = no (abs ∘ ,-injectiveˡ)

 encodeH : Hash → ByteString
 encodeH (bs , _) = bs

 encodeH-inj : ∀ i j → encodeH i ≡ encodeH j → i ≡ j
 encodeH-inj (i , pi) (j , pj) refl = cong (_,_ i) (≡-pi pi pj)

 encodeH-len : ∀{h} → length (encodeH h) ≡ 4
 encodeH-len { bs , p } = p

 encodeH-len-lemma : ∀ i j → length (encodeH i) ≡ length (encodeH j)
 encodeH-len-lemma i j = trans (encodeH-len {i}) (sym (encodeH-len {j}))

 -- Which means that we can make a helper function that combines
 -- the necessary injections into one big injection
 ++b-2-inj : (h₁ h₂ : Hash){l₁ l₂ : Hash}
           → encodeH h₁ ++ encodeH l₁ ≡ encodeH h₂ ++ encodeH l₂
           → h₁ ≡ h₂ × l₁ ≡ l₂
 ++b-2-inj h₁ h₂ {l₁} {l₂} hip
   with ++-inj {m = encodeH h₁} {n = encodeH h₂} (encodeH-len-lemma h₁ h₂) hip
 ...| hh , ll = encodeH-inj h₁ h₂ hh , encodeH-inj l₁ l₂ ll

 Collision : {A B : Set}(f : A → B)(a₁ a₂ : A) → Set
 Collision f a₁ a₂ = a₁ ≢ a₂ × f a₁ ≡ f a₂

 instance
   enc-Hash : Encoder Hash
   enc-Hash = record
     { encode     = encodeH
     ; encode-inj = encodeH-inj _ _
     }

 module WithCryptoHash
   -- A Hash function maps a bytestring into a hash.
   (hash    : BitString → Hash)
   (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y) where

  -- We define the concatenation of hashes like one would expect
  hash-concat : List Hash  → Hash
  hash-concat l = hash (bs-concat (List-map encodeH l))

  -- And voila, it is either injective ot we broke the hash function!
  hash-concat-inj : ∀{l₁ l₂} → hash-concat l₁ ≡ hash-concat l₂ → NonInjective-≡ hash ⊎ l₁ ≡ l₂
  hash-concat-inj {l₁} {l₂} hyp with hash-cr hyp
  ...| inj₁ col  = inj₁ ((_ , _) , col)
  ...| inj₂ same with bs-concat-inj (List-map encodeH l₁) (List-map encodeH l₂) same
  ...| res = inj₂ (map-inj encodeH (encodeH-inj _ _) res)
    where
      map-inj : ∀{a b}{A : Set a}{B : Set b}(f : A → B)
              → (f-injective : ∀{a₁ a₂} → f a₁ ≡ f a₂ → a₁ ≡ a₂)
              → ∀{xs ys} → List-map f xs ≡ List-map f ys → xs ≡ ys
      map-inj f finj {[]} {[]} hyp = refl
      map-inj f finj {x ∷ xs} {y ∷ ys} hyp
        = cong₂ _∷_ (finj (proj₁ (∷-injective hyp)))
                    (map-inj f finj (proj₂ (∷-injective hyp)))

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 --cubical --no-import-sorts --guardedness --safe #-}

module Cubical.Codata.M.AsLimit.stream where

open import Cubical.Data.Unit

open import Cubical.Foundations.Prelude

open import Cubical.Codata.M.AsLimit.M
open import Cubical.Codata.M.AsLimit.helper
open import Cubical.Codata.M.AsLimit.Container

--------------------------------------
-- Stream definitions using M.AsLimit --
--------------------------------------

stream-S : ∀ A -> Container ℓ-zero
stream-S A = (A , (λ _ → Unit))

stream : ∀ (A : Type₀) -> Type₀
stream A = M (stream-S A)

cons : ∀ {A} -> A -> stream A -> stream A
cons x xs = in-fun (x , λ { tt -> xs } )

hd : ∀ {A} -> stream A -> A
hd {A} S = out-fun S .fst

tl : ∀ {A} -> stream A -> stream A
tl {A} S = out-fun S .snd tt

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Sized.SimpleCell where

open import Data.Product
open import Data.String.Base

open import SizedIO.Object
open import SizedIO.IOObject
open import SizedIO.ConsoleObject

open import SizedIO.Base
open import SizedIO.Console hiding (main)

open import NativeIO

open import Size

data CellMethod A : Set where
    get : CellMethod A
    put : A → CellMethod A

CellResult : ∀{A} → CellMethod A → Set
CellResult {A} get = A
CellResult (put _) = Unit

-- cellJ is the interface of the object of a simple cell
cellJ : (A : Set) → Interface
Method  (cellJ A)    =  CellMethod A
Result  (cellJ A) m  =  CellResult m

cell : {A : Set} → A → Object (cellJ A)
objectMethod (cell a) get = a , (cell a)
objectMethod (cell a) (put a') = _ , (cell a')

-- cellC is the type of consoleObjects with interface (cellJ String)
CellC : (i : Size) → Set
CellC i = ConsoleObject i (cellJ String)

-- cellO is a program for a simple cell which
-- when get is called writes "getting s" for the string s of the object
-- and when putting s writes "putting s" for the string

-- cellP is constructor for the consoleObject for interface (cellJ String)
cellP : ∀{i} (s : String) → CellC i
force (method (cellP s) get) =
  exec' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  return (s , cellP s)
force (method (cellP s) (put x)) =
  exec' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  return (_ , (cellP x))

-- Program is another program
program : String → IOConsole ∞ Unit
program arg =
  let c₀ = cellP "Start" in
  method c₀ get       >>= λ{ (s , c₁) →
  exec1 (putStrLn s)         >>
  method c₁ (put arg) >>= λ{ (_ , c₂) →
  method c₂ get       >>= λ{ (s' , c₃) →
  exec1 (putStrLn s')
  }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module functions where

open import level
open import eq

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

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

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

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

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

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

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

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

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Issue4835.ModB where

data B : Set where
  b : B -> B

max_forks_repo_name: shlevy/agda


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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Groups.Isomorphisms.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas

module Groups.Isomorphisms.Lemmas where

groupIsosCompose : {m n o r s t : _} {A : Set m} {S : Setoid {m} {r} A} {_+A_ : A → A → A} {B : Set n} {T : Setoid {n} {s} B} {_+B_ : B → B → B} {C : Set o} {U : Setoid {o} {t} C} {_+C_ : C → C → C} {G : Group S _+A_} {H : Group T _+B_} {I : Group U _+C_} {f : A → B} {g : B → C} (fHom : GroupIso G H f) (gHom : GroupIso H I g) → GroupIso G I (g ∘ f)
GroupIso.groupHom (groupIsosCompose fHom gHom) = groupHomsCompose (GroupIso.groupHom fHom) (GroupIso.groupHom gHom)
GroupIso.bij (groupIsosCompose {A = A} {S = S} {T = T} {C = C} {U = U} {f = f} {g = g} fHom gHom) = record { inj = record { injective = λ pr → (SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij fHom))) (SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij gHom)) pr) ; wellDefined = +WellDefined } ; surj = record { surjective = surj ; wellDefined = +WellDefined } }
  where
    open Setoid S renaming (_∼_ to _∼A_)
    open Setoid U renaming (_∼_ to _∼C_)
    +WellDefined : {x y : A} → (x ∼A y) → (g (f x) ∼C g (f y))
    +WellDefined = GroupHom.wellDefined (groupHomsCompose (GroupIso.groupHom fHom) (GroupIso.groupHom gHom))
    surj : {x : C} → Sg A (λ a → (g (f a) ∼C x))
    surj {x} with SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij gHom)) {x}
    surj {x} | a , prA with SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij fHom)) {a}
    ... | b , prB = b , transitive (GroupHom.wellDefined (GroupIso.groupHom gHom) prB) prA
      where
        open Equivalence (Setoid.eq U)

--groupIsoInvertible : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d}} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} → (iso : GroupIso G H f) → GroupIso H G (Invertible.inverse (bijectionImpliesInvertible (GroupIso.bijective iso)))
--GroupHom.groupHom (GroupIso.groupHom (groupIsoInvertible {G = G} {H} {f} iso)) {x} {y} = {!!}
--  where
--    open Group G renaming (_·_ to _+G_)
--    open Group H renaming (_·_ to _+H_)
--GroupHom.wellDefined (GroupIso.groupHom (groupIsoInvertible {G = G} {H} {f} iso)) {x} {y} x∼y = {!GroupHom.wellDefined x∼y!}
--GroupIso.bijective (groupIsoInvertible {G = G} {H} {f} iso) = invertibleImpliesBijection (inverseIsInvertible (bijectionImpliesInvertible (GroupIso.bijective iso)))


text:
{-# OPTIONS --sized-types #-}
module SNat.Log where

open import Size
open import SNat
open import SNat.Order
open import SNat.Order.Properties
open import SNat.Properties
open import SNat.Sum

lemma-≅-log : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≅ n → log₂ m ≅ log₂ n
lemma-≅-log z≅z = z≅z
lemma-≅-log (s≅s z≅z) = z≅z
lemma-≅-log (s≅s (s≅s m≅n)) = s≅s (lemma-≅-log (s≅s (lemma-≅-/2 m≅n)))

mutual
  lemma-logn≤′logsn : {ι : Size}(n : SNat {ι}) → log₂ n ≤′ log₂ (succ n)
  lemma-logn≤′logsn zero = ≤′-eq z≅z
  lemma-logn≤′logsn (succ zero) = ≤′-step (≤′-eq z≅z)
  lemma-logn≤′logsn (succ (succ n)) = lemma-s≤′s (lemma-≤′-log (lemma-s≤′s (lemma-n/2≤′sn/2 n)))

  lemma-≤′-log : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤′ n → log₂ m ≤′ log₂ n
  lemma-≤′-log (≤′-eq m≅n) = ≤′-eq (lemma-≅-log m≅n)
  lemma-≤′-log (≤′-step {n = n} m≤′n) = trans≤′ (lemma-≤′-log m≤′n) (lemma-logn≤′logsn n)

lemma-1+logn≤′log2n : (n : SNat) → succ (log₂ (succ n)) ≤′ log₂ (succ n + succ n)
lemma-1+logn≤′log2n zero = refl≤′
lemma-1+logn≤′log2n (succ n) rewrite +-assoc-succ (succ (succ n)) (succ n) | +-assoc-succ n (succ n) | +-assoc-succ n n = lemma-s≤′s (lemma-≤′-log (lemma-s≤′s (lemma-n+1≤′2n+2/2 n)))

lemma-log2n≤′1+logn : (n : SNat) → log₂ (n + n) ≤′ succ (log₂ n)
lemma-log2n≤′1+logn zero = ≤′-step refl≤′
lemma-log2n≤′1+logn (succ n) rewrite +-assoc-succ (succ n) n = lemma-s≤′s (lemma-≤′-log (lemma-s≤′s (lemma-2n/2≤′n n)))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import lib.Basics
open import lib.types.Span
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.Unit
open import lib.types.Pointed

-- Cofiber is defined as a particular case of pushout

module lib.types.Cofiber where

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

  cofiber-span : Span
  cofiber-span = span Unit B A (λ _ → tt) f

  Cofiber : Type (lmax i j)
  Cofiber = Pushout cofiber-span

  cfbase' : Cofiber
  cfbase' = left tt

  cfcod' : B → Cofiber
  cfcod' b = right b

  cfglue' : (a : A) → cfbase' == cfcod' (f a)
  cfglue' a = glue a

module _ {i j} {A : Type i} {B : Type j} {f : A → B} where

  cfbase : Cofiber f
  cfbase = cfbase' f

  cfcod : B → Cofiber f
  cfcod = cfcod' f

  cfglue : (a : A) → cfbase == cfcod (f a)
  cfglue = cfglue' f

  module CofiberElim {k} {P : Cofiber f → Type k}
    (b : P cfbase) (c : (y : B) → P (cfcod y))
    (p : (x : A) → b == c (f x) [ P ↓ cfglue x ])
    = PushoutElim (λ _ → b) c p

  open CofiberElim public using () renaming (f to Cofiber-elim)

  module CofiberRec {k} {C : Type k} (b : C) (c : B → C)
    (p : (x : A) → b == c (f x))
    = PushoutRec {d = cofiber-span f} (λ _ → b) c p

  module CofiberRecType {k} (b : Type k) (c : B → Type k)
    (p : (x : A) → b ≃ c (f x))
    = PushoutRecType {d = cofiber-span f} (λ _ → b) c p

module _ {i j} {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙→ Y)) where

  ⊙cof-span : ⊙Span
  ⊙cof-span = ⊙span ⊙Unit Y X ((λ _ → tt) , idp) F

  ⊙Cof : Ptd (lmax i j)
  ⊙Cof = ⊙Pushout ⊙cof-span

  ⊙cfcod' : fst (Y ⊙→ ⊙Cof)
  ⊙cfcod' = cfcod , ap cfcod (! (snd F)) ∙ ! (cfglue (snd X))

  ⊙cfglue' : ⊙cst == ⊙cfcod' ⊙∘ F
  ⊙cfglue' = ⊙λ= cfglue (lemma cfcod (cfglue (snd X)) (snd F))
    where
    lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
      {x y : A} {z : B} (p : z == f x) (q : x == y)
      → idp == p ∙ ap f q ∙ ap f (! q) ∙ ! p
    lemma f idp idp = idp

module _ {i j} {X : Ptd i} {Y : Ptd j} {F : fst (X ⊙→ Y)} where

  ⊙cfcod : fst (Y ⊙→ ⊙Cof F)
  ⊙cfcod = ⊙cfcod' F

  ⊙cfglue : ⊙cst == ⊙cfcod ⊙∘ F
  ⊙cfglue = ⊙cfglue' F

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Logic using (_∈_)
open import Cubical.HITs.SetQuotients.Base
open import Cubical.HITs.SetQuotients.Properties
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ideal

private
  variable
    ℓ : Level

module _ (R' : Ring {ℓ}) (I : ⟨ R' ⟩  → hProp ℓ) (I-isIdeal : isIdeal R' I) where
  open Ring R' renaming (Carrier to R)
  open isIdeal I-isIdeal
  open Theory R'

  R/I : Type ℓ
  R/I = R / (λ x y → x - y ∈ I)

  private
    homogeneity : ∀ (x a b : R)
                 → (a - b ∈ I)
                 → (x + a) - (x + b) ∈ I
    homogeneity x a b p = subst (λ u → u ∈ I) (translatedDifference x a b) p

    isSetR/I : isSet R/I
    isSetR/I = squash/
    [_]/I : (a : R) → R/I
    [ a ]/I = [ a ]

    lemma : (x y a : R)
            → x - y ∈ I
            → [ x + a ]/I ≡ [ y + a ]/I
    lemma x y a x-y∈I = eq/ (x + a) (y + a) (subst (λ u → u ∈ I) calculate x-y∈I)
      where calculate : x - y ≡ (x + a) - (y + a)
            calculate =
                      x - y                 ≡⟨ translatedDifference a x y ⟩
                      ((a + x) - (a + y))   ≡⟨ cong (λ u → u - (a + y)) (+-comm _ _) ⟩
                      ((x + a) - (a + y))   ≡⟨ cong (λ u → (x + a) - u) (+-comm _ _) ⟩
                      ((x + a) - (y + a))   ∎

    pre-+/I : R → R/I → R/I
    pre-+/I x = elim
                    (λ _ → squash/)
                    (λ y → [ x + y ])
                    λ y y' diffrenceInIdeal
                      → eq/ (x + y) (x + y') (homogeneity x y y' diffrenceInIdeal)

    pre-+/I-DescendsToQuotient : (x y : R) → (x - y ∈ I)
                  → pre-+/I x ≡ pre-+/I y
    pre-+/I-DescendsToQuotient x y x-y∈I i r = pointwise-equal r i
      where
        pointwise-equal : ∀ (u : R/I)
                          → pre-+/I x u ≡ pre-+/I y u
        pointwise-equal = elimProp (λ u → isSetR/I (pre-+/I x u) (pre-+/I y u))
                                   (λ a → lemma x y a x-y∈I)

    _+/I_ : R/I → R/I → R/I
    x +/I y = (elim R/I→R/I-isSet pre-+/I pre-+/I-DescendsToQuotient x) y
      where
        R/I→R/I-isSet : R/I → isSet (R/I → R/I)
        R/I→R/I-isSet _ = isSetΠ (λ _ → squash/)

    +/I-comm : (x y : R/I) → x +/I y ≡ y +/I x
    +/I-comm = elimProp2 (λ _ _ → squash/ _ _) eq
       where eq : (x y : R) → [ x ] +/I [ y ] ≡ [ y ] +/I [ x ]
             eq x y i =  [ +-comm x y i ]

    +/I-assoc : (x y z : R/I) → x +/I (y +/I z) ≡ (x +/I y) +/I z
    +/I-assoc = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where eq : (x y z : R) → [ x ] +/I ([ y ] +/I [ z ]) ≡ ([ x ] +/I [ y ]) +/I [ z ]
            eq x y z i =  [ +-assoc x y z i ]

    0/I : R/I
    0/I = [ 0r ]

    1/I : R/I
    1/I = [ 1r ]

    -/I : R/I → R/I
    -/I = elim (λ _ → squash/) (λ x' → [ - x' ]) eq
      where
        eq : (x y : R) → (x - y ∈ I) → [ - x ] ≡ [ - y ]
        eq x y x-y∈I = eq/ (- x) (- y) (subst (λ u → u ∈ I) eq' (isIdeal.-closed I-isIdeal x-y∈I))
          where
            eq' = - (x + (- y))       ≡⟨ sym (-isDistributive _ _) ⟩
                  (- x) - (- y)       ∎

    +/I-rinv : (x : R/I) → x +/I (-/I x) ≡ 0/I
    +/I-rinv = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → [ x ] +/I (-/I [ x ]) ≡ 0/I
        eq x i = [ +-rinv x i ]

    +/I-rid : (x : R/I) → x +/I 0/I ≡ x
    +/I-rid = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → [ x ] +/I 0/I ≡ [ x ]
        eq x i = [ +-rid x i ]

    _·/I_ : R/I → R/I → R/I
    _·/I_ =
      elim (λ _ → isSetΠ (λ _ → squash/))
               (λ x → left· x)
               eq'
      where
        eq : (x y y' : R) → (y - y' ∈ I) → [ x · y ] ≡ [ x · y' ]
        eq x y y' y-y'∈I = eq/ _ _
                             (subst (λ u → u ∈ I)
                                  (x · (y - y')            ≡⟨ ·-rdist-+ _ _ _ ⟩
                                  ((x · y) + x · (- y'))   ≡⟨ cong (λ u → (x · y) + u)
                                                                   (-commutesWithRight-· x y')  ⟩
                                  (x · y) - (x · y')       ∎)
                                  (isIdeal.·-closedLeft I-isIdeal x y-y'∈I))
        left· : (x : R) → R/I → R/I
        left· x = elim (λ y → squash/)
                     (λ y → [ x · y ])
                     (eq x)
        eq' : (x x' : R) → (x - x' ∈ I) → left· x ≡ left· x'
        eq' x x' x-x'∈I i y = elimProp (λ y → squash/ (left· x y) (left· x' y))
                                       (λ y → eq′ y)
                                       y i
                              where
                                eq′ : (y : R) → left· x [ y ] ≡ left· x' [ y ]
                                eq′ y = eq/ (x · y) (x' · y)
                                            (subst (λ u → u ∈ I)
                                              ((x - x') · y         ≡⟨ ·-ldist-+ x (- x') y ⟩
                                               x · y + (- x') · y   ≡⟨ cong
                                                                         (λ u → x · y + u)
                                                                         (-commutesWithLeft-· x' y) ⟩
                                               x · y - x' · y       ∎)
                                              (isIdeal.·-closedRight I-isIdeal y x-x'∈I))

    -- more or less copy paste from '+/I' - this is preliminary anyway
    ·/I-assoc : (x y z : R/I) → x ·/I (y ·/I z) ≡ (x ·/I y) ·/I z
    ·/I-assoc = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where eq : (x y z : R) → [ x ] ·/I ([ y ] ·/I [ z ]) ≡ ([ x ] ·/I [ y ]) ·/I [ z ]
            eq x y z i =  [ ·-assoc x y z i ]

    ·/I-lid : (x : R/I) → 1/I ·/I x ≡ x
    ·/I-lid = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → 1/I ·/I [ x ] ≡ [ x ]
        eq x i = [ ·-lid x i ]

    ·/I-rid : (x : R/I) → x ·/I 1/I ≡ x
    ·/I-rid = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → [ x ] ·/I 1/I ≡ [ x ]
        eq x i = [ ·-rid x i ]

    /I-ldist : (x y z : R/I) → (x +/I y) ·/I z ≡ (x ·/I z) +/I (y ·/I z)
    /I-ldist = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where
        eq : (x y z : R) → ([ x ] +/I [ y ]) ·/I [ z ] ≡ ([ x ] ·/I [ z ]) +/I ([ y ] ·/I [ z ])
        eq x y z i = [ ·-ldist-+ x y z i ]

    /I-rdist : (x y z : R/I) → x ·/I (y +/I z) ≡ (x ·/I y) +/I (x ·/I z)
    /I-rdist = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where
        eq : (x y z : R) → [ x ] ·/I ([ y ] +/I [ z ]) ≡ ([ x ] ·/I [ y ]) +/I ([ x ] ·/I [ z ])
        eq x y z i = [ ·-rdist-+ x y z i ]

  asRing : Ring {ℓ}
  asRing = makeRing 0/I 1/I _+/I_ _·/I_ -/I isSetR/I
                    +/I-assoc +/I-rid +/I-rinv +/I-comm
                    ·/I-assoc ·/I-rid ·/I-lid /I-rdist /I-ldist

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Issue168b where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

module Membership (A : Set) where

  id : Nat → Nat
  id zero     = zero
  id (suc xs) = suc (id xs)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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 Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.PKCS

import      LibraBFT.Concrete.Properties.VotesOnce as VO

open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Consensus.RoundManager.Properties
open import LibraBFT.Impl.Handle
open import LibraBFT.Impl.Handle.Properties
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Types
open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})
open        WithSPS impl-sps-avp
open        Structural impl-sps-avp
open import LibraBFT.Impl.Properties.VotesOnce

-- This module proves the two "VotesOnce" proof obligations for our fake handler. Unlike the
-- LibraBFT.Impl.Properties.VotesOnce, which is based on unwind, this proof is done
-- inductively on the ReachableSystemState.

module LibraBFT.Impl.Properties.VotesOnceDirect where

  newVoteEpoch≡⇒Round≡ : ∀ {st : SystemState}{pid s' outs v m pk}
                       → ReachableSystemState st
                       → StepPeerState pid (msgPool st) (initialised st)
                                       (peerStates st pid) (s' , outs)
                       → v ⊂Msg m → send m ∈ outs → (sig : WithVerSig pk v)
                       → Meta-Honest-PK pk → ¬ (∈GenInfo (ver-signature sig))
                       → ¬ MsgWithSig∈ pk (ver-signature sig) (msgPool st)
                       → v ^∙ vEpoch ≡ (₋rmEC s') ^∙ rmEpoch
                       → v ^∙ vRound ≡ (₋rmEC s') ^∙ rmLastVotedRound
  newVoteEpoch≡⇒Round≡ r step@(step-msg {_ , P pm} _ pinit) v⊂m (here refl)
                       sig pkH ¬gen vnew ep≡
     with v⊂m
  ...| vote∈vm = refl
  ...| vote∈qc vs∈qc v≈rbld (inV qc∈m) rewrite cong ₋vSignature v≈rbld
       = let qc∈rm = VoteMsgQCsFromRoundManager r step pkH v⊂m (here refl) qc∈m
         in ⊥-elim (vnew (qcVotesSentB4 r pinit qc∈rm vs∈qc ¬gen))

  open PeerCanSignForPK

  peerCanSignSameS : ∀ {pid v pk s s'}
                   → PeerCanSignForPK s v pid pk
                   → s' ≡ s
                   → PeerCanSignForPK s' v pid pk
  peerCanSignSameS pcs refl = pcs

  peerCanSignEp≡ : ∀ {pid v v' pk s'}
                 → PeerCanSignForPK s' v pid pk
                 → v ^∙ vEpoch ≡ v' ^∙ vEpoch
                 → PeerCanSignForPK s' v' pid pk
  peerCanSignEp≡ (mkPCS4PK 𝓔₁ 𝓔id≡₁ 𝓔inSys₁ mbr₁ nid≡₁ pk≡₁) refl
    = (mkPCS4PK 𝓔₁ 𝓔id≡₁ 𝓔inSys₁ mbr₁ nid≡₁ pk≡₁)

  MsgWithSig⇒ValidSenderInitialised : ∀ {st v pk}
                                    → ReachableSystemState st
                                    → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                                    → ¬ (∈GenInfo (ver-signature sig))
                                    → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
                                    → ∃[ pid ] ( initialised st pid ≡ initd
                                               × PeerCanSignForPK st v pid pk )
  MsgWithSig⇒ValidSenderInitialised {st} {v} (step-s r step@(step-peer (step-honest {pid} stP))) pkH sig ¬gen msv
     with msgSameSig msv
  ...| refl
     with newMsg⊎msgSentB4 r stP pkH (msgSigned msv) ¬gen (msg⊆ msv) (msg∈pool msv)
  ...| inj₁ (m∈outs , pcsN , newV)
     with stP
  ...| step-msg _ initP
      with PerState.sameSig⇒sameVoteDataNoCol st (step-s r step) (msgSigned msv) sig (msgSameSig msv)
  ...| refl = pid , peersRemainInitialized step initP , peerCanSignEp≡ pcsN refl
  MsgWithSig⇒ValidSenderInitialised {st} {v} (step-s r step@(step-peer (step-honest stP))) pkH sig ¬gen msv
     | refl
     | inj₂ msb4
     with MsgWithSig⇒ValidSenderInitialised {v = v} r pkH sig ¬gen msb4
  ...| pid , initP , pcsPre = pid ,
                              peersRemainInitialized step initP ,
                              PeerCanSignForPK-stable r step pcsPre
  MsgWithSig⇒ValidSenderInitialised {st} {v} (step-s r step@(step-peer cheat@(step-cheat x))) pkH sig ¬gen msv
     with msgSameSig msv
  ...| refl
     with ¬cheatForgeNew cheat refl unit pkH msv ¬gen
  ...| msb4
     with MsgWithSig⇒ValidSenderInitialised {v = v} r pkH sig ¬gen msb4
  ...| pid , initP , pcsPre = pid ,
                              peersRemainInitialized step initP ,
                              PeerCanSignForPK-stable r step pcsPre

  peerCanSign-Msb4 : ∀ {pid v pk}{pre post : SystemState}
                   → ReachableSystemState pre
                   → Step pre post
                   → PeerCanSignForPK post v pid pk
                   → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                   → MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
                   → PeerCanSignForPK pre v pid pk
  peerCanSign-Msb4 r step (mkPCS4PK 𝓔₁ 𝓔id≡₁ (inGenInfo refl) mbr₁ nid≡₁ pk≡₁) pkH sig msv
    = mkPCS4PK 𝓔₁ 𝓔id≡₁ (inGenInfo refl) mbr₁ nid≡₁ pk≡₁

  peerCanSignPK-Inj :  ∀ {pid pid' pk v v'}{st : SystemState}
                    → ReachableSystemState st
                    → Meta-Honest-PK pk
                    → PeerCanSignForPK st v' pid' pk
                    → PeerCanSignForPK st v pid pk
                    → v ^∙ vEpoch ≡ v' ^∙ vEpoch
                    → pid ≡ pid'
  peerCanSignPK-Inj {pid} {pid'} r pkH pcs' pcs eid≡
     with availEpochsConsistent r pcs' pcs
  ...| refl
     with NodeId-PK-OK-injective (𝓔 pcs) (PCS4PK⇒NodeId-PK-OK pcs) (PCS4PK⇒NodeId-PK-OK pcs')
  ...| refl = refl

  msg∈pool⇒initd : ∀ {pid pk v}{st : SystemState}
                 → ReachableSystemState st
                 → PeerCanSignForPK st v pid pk
                 → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                 → ¬ (∈GenInfo (ver-signature sig))
                 → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
                 → initialised st pid ≡ initd
  msg∈pool⇒initd {pid'} {st = st} step@(step-s r (step-peer {pid} (step-honest stPeer))) pcs pkH sig ¬gen msv
     with msgSameSig msv
  ...| refl
     with newMsg⊎msgSentB4 r stPeer pkH (msgSigned msv) ¬gen (msg⊆ msv) (msg∈pool msv)
  ...| inj₁ (m∈outs , pcsN , newV)
     with sameSig⇒sameVoteData (msgSigned msv) sig (msgSameSig msv)
  ...| inj₁ hb = ⊥-elim (PerState.meta-sha256-cr st step hb)
  ...| inj₂ refl
     with stPeer
  ...| step-msg _ initP
     with pid ≟ pid'
  ...| yes refl = refl
  ...| no  pid≢ = ⊥-elim (pid≢ (peerCanSignPK-Inj step pkH pcs pcsN refl))
  msg∈pool⇒initd {pid'} (step-s r step@(step-peer {pid} (step-honest stPeer))) pcs pkH sig ¬gen msv
     | refl
     | inj₂ msb4
     with pid ≟ pid'
  ...| yes refl = refl
  ...| no  pid≢ = let pcsmsb4 = peerCanSign-Msb4 r step pcs pkH sig msb4
                  in msg∈pool⇒initd r pcsmsb4 pkH sig ¬gen msb4
  msg∈pool⇒initd {pid'} (step-s r step@(step-peer {pid} cheat@(step-cheat c))) pcs pkH sig ¬gen msv
     with msgSameSig msv
  ...| refl
     with ¬cheatForgeNew cheat refl unit pkH msv ¬gen
  ...| msb4
       = let pcsmsb4 = peerCanSign-Msb4 r step pcs pkH sig msb4
             initPre = msg∈pool⇒initd r pcsmsb4  pkH sig ¬gen msb4
         in peersRemainInitialized (step-peer cheat) initPre

  noEpochChange : ∀ {pid s' outs v pk}{st : SystemState}
                → ReachableSystemState st
                → (stP : StepPeerState pid (msgPool st) (initialised st)
                                       (peerStates st pid) (s' , outs))
                → PeerCanSignForPK st v pid pk
                → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                → ¬ ∈GenInfo (ver-signature sig)
                → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
                → (₋rmEC s') ^∙ rmEpoch ≡ (v ^∙ vEpoch)
                → (₋rmEC (peerStates st pid)) ^∙ rmEpoch ≡ (v ^∙ vEpoch)
  noEpochChange r (step-init uni) pcs pkH sig ∉gen msv eid≡
    = ⊥-elim (uninitd≢initd (trans (sym uni) (msg∈pool⇒initd r pcs pkH sig ∉gen msv)))
  noEpochChange r sm@(step-msg _ ini) pcs pkH sig ∉gen msv eid≡
    rewrite noEpochIdChangeYet r refl sm ini = eid≡

  oldVoteRound≤lvr : ∀ {pid pk v}{pre : SystemState}
                   → (r : ReachableSystemState pre)
                   → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                   → ¬ (∈GenInfo (ver-signature sig))
                   → MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
                   → PeerCanSignForPK pre v pid pk
                   → (₋rmEC (peerStates pre pid)) ^∙ rmEpoch ≡ (v ^∙ vEpoch)
                   → v ^∙ vRound ≤ (₋rmEC (peerStates pre pid)) ^∙ rmLastVotedRound
  oldVoteRound≤lvr {pid'} (step-s r step@(step-peer {pid = pid} cheat@(step-cheat c)))
                   pkH sig ¬gen msv vspk eid≡
     with ¬cheatForgeNew cheat refl unit pkH msv (¬subst ¬gen (msgSameSig msv))
  ...| msb4 rewrite cheatStepDNMPeerStates₁ {pid = pid} {pid' = pid'} cheat unit
       = let pcsmsb4 = peerCanSign-Msb4 r step vspk pkH sig msb4
         in oldVoteRound≤lvr r pkH sig ¬gen msb4 pcsmsb4 eid≡
  oldVoteRound≤lvr {pid'} step@(step-s r stP@(step-peer {pid} (step-honest stPeer)))
                   pkH sig ¬gen msv vspk eid≡
     with msgSameSig msv
  ...| refl
     with newMsg⊎msgSentB4 r stPeer pkH (msgSigned msv) ¬gen (msg⊆ msv) (msg∈pool msv)
  ...| inj₂ msb4 rewrite msgSameSig msv
     with peerCanSign-Msb4 r stP vspk pkH sig msb4
  ...| pcsmsb4
     with pid ≟ pid'
  ...| no  pid≢ = oldVoteRound≤lvr r  pkH sig ¬gen msb4 pcsmsb4 eid≡
  ...| yes refl = let  initP = msg∈pool⇒initd r pcsmsb4 pkH sig ¬gen msb4
                       ep≡   = noEpochChange r stPeer pcsmsb4 pkH sig ¬gen msb4 eid≡
                       lvr≤  = lastVoteRound-mono r refl stPeer initP (trans ep≡ (sym eid≡))
                   in ≤-trans (oldVoteRound≤lvr r pkH sig ¬gen msb4 pcsmsb4 ep≡) lvr≤
  oldVoteRound≤lvr {pid = pid'} {pre = pre}
                   step@(step-s r (step-peer {pid} (step-honest stPeer)))
                   pkH sig ¬gen msv vspk eid≡
     | refl
     | inj₁ (m∈outs , vspkN , newV)
     with sameSig⇒sameVoteData (msgSigned msv) sig (msgSameSig msv)
  ...| inj₁ hb = ⊥-elim (PerState.meta-sha256-cr pre step hb)
  ...| inj₂ refl
     with pid ≟ pid'
  ...| yes refl = ≡⇒≤ (newVoteEpoch≡⇒Round≡ r stPeer (msg⊆ msv) m∈outs (msgSigned msv)
                                            pkH ¬gen newV (sym eid≡))
  ...| no  pid≢ = ⊥-elim (pid≢ (peerCanSignPK-Inj step pkH vspk vspkN refl))

  votesOnce₁ : VO.ImplObligation₁
  votesOnce₁ {pid' = pid'} r stMsg@(step-msg {_ , P m} m∈pool psI) {v' = v'} {m' = m'}
             pkH v⊂m (here refl) sv ¬gen ¬msb vspkv v'⊂m' m'∈pool sv' ¬gen' eid≡ r≡
     with v⊂m
  ...| vote∈vm = let m'mwsb = mkMsgWithSig∈ m' v' v'⊂m' pid' m'∈pool sv' refl
                     vspkv' = peerCanSignEp≡ {v' = v'} vspkv eid≡
                     step   = step-peer (step-honest stMsg)
                     vspre' = peerCanSign-Msb4 r step vspkv' pkH sv' m'mwsb
                     rv'<rv = oldVoteRound≤lvr r pkH sv' ¬gen' m'mwsb vspre' eid≡
                 in ⊥-elim (<⇒≢ (s≤s rv'<rv) (sym r≡))
  ...| vote∈qc vs∈qc v≈rbld (inV qc∈m) rewrite cong ₋vSignature v≈rbld
     = let qc∈rm = VoteMsgQCsFromRoundManager r stMsg pkH v⊂m (here refl) qc∈m
       in ⊥-elim (¬msb (qcVotesSentB4 r psI qc∈rm vs∈qc ¬gen))

  votesOnce₂ : VO.ImplObligation₂
  votesOnce₂ {pk = pk} {st} r stMsg@(step-msg {_ , P m} m∈pool psI) pkH v⊂m m∈outs sig ¬gen vnew
             vpk v'⊂m' m'∈outs sig' ¬gen' v'new vpk' es≡ rnds≡
     with m∈outs | m'∈outs
  ...| here refl | here refl
     with v⊂m                          | v'⊂m'
  ...| vote∈vm                         | vote∈vm = refl
  ...| vote∈vm                         | vote∈qc vs∈qc' v≈rbld' (inV qc∈m')
       rewrite cong ₋vSignature v≈rbld'
       = let qc∈rm' = VoteMsgQCsFromRoundManager r stMsg pkH v'⊂m' (here refl) qc∈m'
         in ⊥-elim (v'new (qcVotesSentB4 r psI qc∈rm' vs∈qc' ¬gen'))
  ...| vote∈qc vs∈qc v≈rbld (inV qc∈m) | _
       rewrite cong ₋vSignature v≈rbld
       = let qc∈rm = VoteMsgQCsFromRoundManager r stMsg pkH v⊂m (here refl) qc∈m
         in ⊥-elim (vnew (qcVotesSentB4 r psI qc∈rm vs∈qc ¬gen))


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

open import Level
open import Function using (flip)

open import Relation.Binary hiding (_⇒_)
import Relation.Binary.PropositionalEquality as ≡
import Relation.Binary.Reasoning.Setoid as SetoidR

-- Basic definition of a |Category| with a Hom setoid.
-- Also comes with some reasoning combinators (see HomReasoning)
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  eta-equality
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    -- We add a symmetric proof of associativity so that the opposite category of the
    -- opposite category is definitionally equal to the original category. See how
    -- `op` is implemented.
    sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    -- We add a proof of "neutral" identity proof, in order to ensure the opposite of
    -- constant functor is definitionally equal to itself.
    identity² : ∀ {A} → id ∘ id {A} ≈ id {A}
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i

  module Equiv {A B : Obj} = IsEquivalence (equiv {A} {B})

  open Equiv

  dom : ∀ {A B} → (A ⇒ B) → Obj
  dom {A} _ = A

  cod : ∀ {A B} → (A ⇒ B) → Obj
  cod {B = B} _ = B

  ∘-resp-≈ˡ : ∀ {A B C} {f h : B ⇒ C} {g : A ⇒ B} → f ≈ h → f ∘ g ≈ h ∘ g
  ∘-resp-≈ˡ pf = ∘-resp-≈ pf refl

  ∘-resp-≈ʳ : ∀ {A B C} {f h : A ⇒ B} {g : B ⇒ C} → f ≈ h → g ∘ f ≈ g ∘ h
  ∘-resp-≈ʳ pf = ∘-resp-≈ refl pf

  hom-setoid : ∀ {A B} → Setoid _ _
  hom-setoid {A} {B} = record
    { Carrier       = A ⇒ B
    ; _≈_           = _≈_
    ; isEquivalence = equiv
    }

  -- Reasoning combinators.  _≈⟨_⟩_ and _≈˘⟨_⟩_ from SetoidR.
  -- Also some useful combinators for doing reasoning on _∘_ chains
  module HomReasoning {A B : Obj} where
    open SetoidR (hom-setoid {A} {B}) public
    open Equiv {A = A} {B = B} public

    infixr 4 _⟩∘⟨_ refl⟩∘⟨_
    infixl 5 _⟩∘⟨refl
    _⟩∘⟨_ : ∀ {M} {f h : M ⇒ B} {g i : A ⇒ M} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
    _⟩∘⟨_ = ∘-resp-≈

    refl⟩∘⟨_ : ∀ {M} {f : M ⇒ B} {g i : A ⇒ M} → g ≈ i → f ∘ g ≈ f ∘ i
    refl⟩∘⟨_ = Equiv.refl ⟩∘⟨_

    _⟩∘⟨refl : ∀ {M} {f h : M ⇒ B} {g : A ⇒ M} → f ≈ h → f ∘ g ≈ h ∘ g
    _⟩∘⟨refl = _⟩∘⟨ Equiv.refl

    -- convenient inline versions
    infix 2 ⟺
    infixr 3 _○_
    ⟺ : {f g : A ⇒ B} → f ≈ g → g ≈ f
    ⟺ = Equiv.sym
    _○_ : {f g h : A ⇒ B} → f ≈ g → g ≈ h → f ≈ h
    _○_ = Equiv.trans

    -- for reasoning in the Strict cases
    ≡⇒≈ : {f g : A ⇒ B} → f ≡.≡ g → f ≈ g
    ≡⇒≈ ≡.refl = Equiv.refl

    subst₂≈ : {C D : Obj} {f g : A ⇒ B} → f ≈ g → (eq₁ : A ≡.≡ C) (eq₂ : B ≡.≡ D) →
      ≡.subst₂ (_⇒_) eq₁ eq₂ f ≈ ≡.subst₂ (_⇒_) eq₁ eq₂ g
    subst₂≈ f≈g ≡.refl ≡.refl = f≈g

  -- Combinators for commutative diagram
  -- The idea is to use the combinators to write commutations in a more readable way.
  -- It starts with [_⇒_]⟨_≈_⟩, and within the third and fourth places, use _⇒⟨_⟩_ to
  -- connect morphisms with the intermediate object specified.
  module Commutation where
    infix 1 [_⇒_]⟨_≈_⟩
    [_⇒_]⟨_≈_⟩ : ∀ (A B : Obj) → A ⇒ B → A ⇒ B → Set _
    [ A ⇒ B ]⟨ f ≈ g ⟩ = f ≈ g

    infixl 2 connect
    connect : ∀ {A C : Obj} (B : Obj) → A ⇒ B → B ⇒ C → A ⇒ C
    connect B f g = g ∘ f

    syntax connect B f g = f ⇒⟨ B ⟩ g

  op : Category o ℓ e
  op = record
    { Obj       = Obj
    ; _⇒_       = flip _⇒_
    ; _≈_       = _≈_
    ; _∘_       = flip _∘_
    ; id        = id
    ; assoc     = sym-assoc
    ; sym-assoc = assoc
    ; identityˡ = identityʳ
    ; identityʳ = identityˡ
    ; identity² = identity²
    ; equiv     = equiv
    ; ∘-resp-≈  = flip ∘-resp-≈
    }

  -- Q: Should this really be defined here?
  CommutativeSquare : ∀ {A B C D} → (f : A ⇒ B) (g : A ⇒ C) (h : B ⇒ D) (i : C ⇒ D) → Set _
  CommutativeSquare f g h i = h ∘ f ≈ i ∘ g

-- Since we add extra proofs in the definition of `Category` (i.e. `sym-assoc` and
-- `identity²`), we might still want to construct a `Category` in its originally
-- easier manner. Thus, this redundant definition is here to ease the construction.
record CategoryHelper (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i

categoryHelper : ∀ {o ℓ e} → CategoryHelper o ℓ e → Category o ℓ e
categoryHelper C = record
  { Obj       = Obj
  ; _⇒_       = _⇒_
  ; _≈_       = _≈_
  ; id        = id
  ; _∘_       = _∘_
  ; assoc     = assoc
  ; sym-assoc = sym assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identityˡ
  ; equiv     = equiv
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where open CategoryHelper C
        module _ {A B} where
          open IsEquivalence (equiv {A} {B}) public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2018-04-10, issue #3662.

-- Regression in the termination checker introduced together
-- with collecting function calls also in the type signatures
-- (fix of #1556).

record T : Set₂ where
  field
    Carr : Set₁
    op   : Carr → Carr

test : T
T.Carr test   = Set
T.op   test c = Aux
  where
  postulate Aux : Set
  --  Aux : (c : T.Carr test) → Set
  --             ^^^^^^^^^^^

-- Since c as a module parameter to the where-module is parameter of Aux,
-- it contains a recursive call if we also mine type signatures for calls
-- (#1556).
--
-- We get then
--
--   test .op c --> test .Carr
--
-- which is not a decreasing call.

-- However, the call does not compose with itself, thus, with
-- Hyvernat-termination it would not give a false termination alarm.

-- Should termination check.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propositional (intensional) equality
------------------------------------------------------------------------

module Relation.Binary.PropositionalEquality where

open import Function
open import Function.Equality using (Π; _⟶_; ≡-setoid)
open import Data.Product
open import Data.Unit.Core
open import Level
open import Relation.Binary
import Relation.Binary.Indexed as I
open import Relation.Binary.Consequences
open import Relation.Binary.HeterogeneousEquality.Core as H using (_≅_)

-- Some of the definitions can be found in the following modules:

open import Relation.Binary.Core public using (_≡_; refl; _≢_)
open import Relation.Binary.PropositionalEquality.Core public

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

subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p)
         {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
           f ≡ g → (x : A) → f x ≡ g x
cong-app refl x = refl

cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
        (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
cong₂ f refl refl = refl

proof-irrelevance : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q
proof-irrelevance refl refl = refl

setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; isEquivalence = isEquivalence
  }

decSetoid : ∀ {a} {A : Set a} → Decidable (_≡_ {A = A}) → DecSetoid _ _
decSetoid dec = record
  { _≈_              = _≡_
  ; isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = dec
      }
  }

isPreorder : ∀ {a} {A : Set a} → IsPreorder {A = A} _≡_ _≡_
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  }

preorder : ∀ {a} → Set a → Preorder _ _ _
preorder A = record
  { Carrier    = A
  ; _≈_        = _≡_
  ; _∼_        = _≡_
  ; isPreorder = isPreorder
  }

------------------------------------------------------------------------
-- Pointwise equality

infix 4 _≗_

_→-setoid_ : ∀ {a b} (A : Set a) (B : Set b) → Setoid _ _
A →-setoid B = ≡-setoid A (Setoid.indexedSetoid (setoid B))

_≗_ : ∀ {a b} {A : Set a} {B : Set b} (f g : A → B) → Set _
_≗_ {A = A} {B} = Setoid._≈_ (A →-setoid B)

:→-to-Π : ∀ {a b₁ b₂} {A : Set a} {B : I.Setoid _ b₁ b₂} →
          ((x : A) → I.Setoid.Carrier B x) → Π (setoid A) B
:→-to-Π {B = B} f = record { _⟨$⟩_ = f; cong = cong′ }
  where
  open I.Setoid B using (_≈_)

  cong′ : ∀ {x y} → x ≡ y → f x ≈ f y
  cong′ refl = I.Setoid.refl B

→-to-⟶ : ∀ {a b₁ b₂} {A : Set a} {B : Setoid b₁ b₂} →
         (A → Setoid.Carrier B) → setoid A ⟶ B
→-to-⟶ = :→-to-Π

------------------------------------------------------------------------
-- The old inspect idiom

-- The old inspect idiom has been deprecated, and may be removed in
-- the future. Use inspect on steroids instead.

module Deprecated-inspect where

  -- The inspect idiom can be used when you want to pattern match on
  -- the result r of some expression e, and you also need to
  -- "remember" that r ≡ e.

  -- The inspect idiom has a problem: sometimes you can only pattern
  -- match on the p part of p with-≡ eq if you also pattern match on
  -- the eq part, and then you no longer have access to the equality.
  -- Inspect on steroids solves this problem.

  data Inspect {a} {A : Set a} (x : A) : Set a where
    _with-≡_ : (y : A) (eq : x ≡ y) → Inspect x

  inspect : ∀ {a} {A : Set a} (x : A) → Inspect x
  inspect x = x with-≡ refl

  -- Example usage:

  -- f x y with inspect (g x)
  -- f x y | c z with-≡ eq = ...

------------------------------------------------------------------------
-- Inspect on steroids

-- Inspect on steroids can be used when you want to pattern match on
-- the result r of some expression e, and you also need to "remember"
-- that r ≡ e.

data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where
  [_] : (eq : reveal x ≡ y) → Reveal x is y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)
inspect f x = [ refl ]

-- Example usage:

-- f x y with g x | inspect g x
-- f x y | c z | [ eq ] = ...

------------------------------------------------------------------------
-- Convenient syntax for equational reasoning

import Relation.Binary.EqReasoning as EqR

-- Relation.Binary.EqReasoning is more convenient to use with _≡_ if
-- the combinators take the type argument (a) as a hidden argument,
-- instead of being locked to a fixed type at module instantiation
-- time.

module ≡-Reasoning where
  module _ {a} {A : Set a} where
    open EqR (setoid A) public
      hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_)

  infixr 2 _≅⟨_⟩_

  _≅⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {y z : A} →
           x ≅ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≅⟨ x≅y ⟩ y≡z = _ ≡⟨ H.≅-to-≡ x≅y ⟩ y≡z

------------------------------------------------------------------------
-- Functional extensionality

-- If _≡_ were extensional, then the following statement could be
-- proved.

Extensionality : (a b : Level) → Set _
Extensionality a b =
  {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
  (∀ x → f x ≡ g x) → f ≡ g

-- If extensionality holds for a given universe level, then it also
-- holds for lower ones.

extensionality-for-lower-levels :
  ∀ {a₁ b₁} a₂ b₂ →
  Extensionality (a₁ ⊔ a₂) (b₁ ⊔ b₂) → Extensionality a₁ b₁
extensionality-for-lower-levels a₂ b₂ ext f≡g =
  cong (λ h → lower ∘ h ∘ lift) $
    ext (cong (lift {ℓ = b₂}) ∘ f≡g ∘ lower {ℓ = a₂})

-- Functional extensionality implies a form of extensionality for
-- Π-types.

∀-extensionality :
  ∀ {a b} →
  Extensionality a (suc b) →
  {A : Set a} (B₁ B₂ : A → Set b) →
  (∀ x → B₁ x ≡ B₂ x) → (∀ x → B₁ x) ≡ (∀ x → B₂ x)
∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂
∀-extensionality ext B .B  B₁≡B₂ | refl = refl


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

module Explore.One where

module _ {ℓ} where
    open Explore.Monad {₀} ℓ

    𝟙ᵉ : Explore ℓ 𝟙
    𝟙ᵉ = return _
    {- or
    𝟙ᵉ _ f = f _
    -}

    𝟙ⁱ : ∀ {p} → ExploreInd p 𝟙ᵉ
    𝟙ⁱ = return-ind _
    {- or
    𝟙ⁱ _ _ Pf = Pf _
    -}

module _ {ℓ₁ ℓ₂ ℓᵣ} {R : 𝟙 → 𝟙 → ★₀} {r : R _ _} where
    ⟦𝟙ᵉ⟧ : ⟦Explore⟧ {ℓ₁} {ℓ₂} ℓᵣ R 𝟙ᵉ 𝟙ᵉ
    ⟦𝟙ᵉ⟧ _ _ _∙ᵣ_ fᵣ = fᵣ r

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

open Adequacy _≡_
module _ {{_ : UA}} where
    Σᵉ𝟙-ok : ∀ {ℓ} → Adequate-Σ {ℓ} (Σᵉ 𝟙ᵉ)
    Σᵉ𝟙-ok _ = ! Σ𝟙-snd

    Πᵉ𝟙-ok : ∀ {ℓ} → Adequate-Π {ℓ} (Πᵉ 𝟙ᵉ)
    Πᵉ𝟙-ok _ = ! Π𝟙-uniq _

    𝟙ˢ-ok : Adequate-sum 𝟙ˢ
    𝟙ˢ-ok _ = ! 𝟙×-snd

    𝟙ᵖ-ok : Adequate-product 𝟙ᵖ
    𝟙ᵖ-ok _ = ! Π𝟙-uniq _

    adequate-sum𝟙     = 𝟙ˢ-ok
    adequate-product𝟙 = 𝟙ᵖ-ok

module _ {ℓ} where
    𝟙ˡ : Lookup {ℓ} 𝟙ᵉ
    𝟙ˡ = const

    𝟙ᶠ : Focus {ℓ} 𝟙ᵉ
    𝟙ᶠ = proj₂

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

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module MissingDefinition where

open import Agda.Builtin.Equality

Q : Set

data U : Set
S : Set
S = U
T : S → Set
T _ = U

V : Set
W : V → Set

private

  X : Set

module AB where

  data A : Set
  B : (a b : A) → a ≡ b

mutual

  U₂ : Set
  data T₂ : U₂ → Set
  V₂ : (u₂ : U₂) → T₂ u₂ → Set
  data W₂ (u₂ : U₂) (t₂ : T₂ u₂) : V₂ u₂ t₂ → Set

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import lib.Base

module lib.Relation {i} where

Rel : ∀ (A : Type i) j → Type (lmax i (lsucc j))
Rel A j = A → A → Type j

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

  Decidable : Type (lmax i j)
  Decidable = ∀ a₁ a₂ → Dec (rel a₁ a₂)

  is-refl : Type (lmax i j)
  is-refl = ∀ a → rel a a

  is-sym : Type (lmax i j)
  is-sym = ∀ {a b} → rel a b → rel b a

  is-trans : Type (lmax i j)
  is-trans = ∀ {a b c} → rel a b → rel b c → rel a c

  -- as equivalence relation
  -- is-equational : Type (lmax i j)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Some defined operations (multiplication by natural number and
-- exponentiation)
------------------------------------------------------------------------

open import Algebra

module Algebra.Operations (s : Semiring) where

open Semiring s hiding (zero)
open import Data.Nat using (zero; suc; ℕ)
open import Data.Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
import Relation.Binary.EqReasoning as EqR
open EqR setoid

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

-- Multiplication by natural number.

infixr 7 _×_

_×_ : ℕ → carrier → carrier
zero  × x = 0#
suc n × x = x + n × x

-- Exponentiation.

infixr 8 _^_

_^_ : carrier → ℕ → carrier
x ^ zero  = 1#
x ^ suc n = x * x ^ n

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

×-pres-≈ : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
×-pres-≈ {n} {n'} {x} {x'} n≡n' x≈x' = begin
  n  × x   ≈⟨ reflexive $ PropEq.cong (λ n → n × x) n≡n' ⟩
  n' × x   ≈⟨ ×-pres-≈ʳ n' x≈x' ⟩
  n' × x'  ∎
  where
  ×-pres-≈ʳ : ∀ n → (_×_ n) Preserves _≈_ ⟶ _≈_
  ×-pres-≈ʳ zero    x≈x' = refl
  ×-pres-≈ʳ (suc n) x≈x' = x≈x' ⟨ +-pres-≈ ⟩ ×-pres-≈ʳ n x≈x'

^-pres-≈ : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
^-pres-≈ {x} {x'} {n} {n'} x≈x' n≡n' = begin
  x  ^ n   ≈⟨ reflexive $ PropEq.cong (_^_ x) n≡n' ⟩
  x  ^ n'  ≈⟨ ^-pres-≈ˡ n' x≈x' ⟩
  x' ^ n'  ∎
  where
  ^-pres-≈ˡ : ∀ n → (λ x → x ^ n) Preserves _≈_ ⟶ _≈_
  ^-pres-≈ˡ zero    x≈x' = refl
  ^-pres-≈ˡ (suc n) x≈x' = x≈x' ⟨ *-pres-≈ ⟩ ^-pres-≈ˡ n x≈x'

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module WellFormed where

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

postulate Vec : Set -> Nat -> Set
postulate _X_ : Set -> Set -> Set
postulate zip : {A B : Set} -> (n : Nat) -> Vec A n -> Vec B n -> Vec (A X B) n

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


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

open import Examples.Sorting.Sequential.Comparable

module Examples.Sorting.Sequential.InsertionSort (M : Comparable) where

open Comparable M
open import Examples.Sorting.Sequential.Core M

open import Calf costMonoid
open import Calf.Types.Bool
open import Calf.Types.List
open import Calf.Types.Eq
open import Calf.Types.Bounded costMonoid
open import Calf.Types.BigO costMonoid

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; ∃)
open import Data.Sum using (inj₁; inj₂)
open import Function
open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s; _+_; _*_)
import Data.Nat.Properties as N
open import Data.Nat.Square

insert : cmp (Π A λ _ → Π (list A) λ _ → F (list A))
insert x []       = ret [ x ]
insert x (y ∷ ys) =
  bind (F (list A)) (x ≤ᵇ y)
    λ { false → bind (F (list A)) (insert x ys) (ret ∘ (y ∷_))
      ; true  → ret (x ∷ (y ∷ ys)) }

insert/correct : ∀ x l → Sorted l → ◯ (∃ λ l' → insert x l ≡ ret l' × SortedOf (x ∷ l) l')
insert/correct x []       []       u = [ x ] , refl , refl , [] ∷ []
insert/correct x (y ∷ ys) (h ∷ hs) u with h-cost x y
insert/correct x (y ∷ ys) (h ∷ hs) u | ⇓ b withCost q [ _ , h-eq ] rewrite eq/ref h-eq
  with ≤ᵇ-reflects-≤ u (Eq.trans (eq/ref h-eq) (step/ext (F bool) (ret b) q u)) | ≤-total x y
insert/correct x (y ∷ ys) (h ∷ hs) u | ⇓ false withCost q [ _ , _ ] | ofⁿ ¬x≤y | inj₁ x≤y = contradiction x≤y ¬x≤y
insert/correct x (y ∷ ys) (h ∷ hs) u | ⇓ false withCost q [ _ , _ ] | ofⁿ ¬x≤y | inj₂ x≤y =
  let (ys' , h-ys' , x∷ys↭ys' , sorted-ys') = insert/correct x ys hs u in
  y ∷ ys' , (
    let open ≡-Reasoning in
    begin
      step (F (list A)) q (bind (F (list A)) (insert x ys) (ret ∘ (y ∷_)))
    ≡⟨ step/ext (F (list A)) (bind (F (list A)) (insert x ys) (ret ∘ (y ∷_))) q u ⟩
      bind (F (list A)) (insert x ys) (ret ∘ (y ∷_))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e (ret ∘ (y ∷_))) h-ys' ⟩
      ret (y ∷ ys')
    ∎
  ) , (
    let open PermutationReasoning in
    begin
      x ∷ y ∷ ys
    <<⟨ refl ⟩
      y ∷ (x ∷ ys)
    <⟨ x∷ys↭ys' ⟩
      y ∷ ys'
    ∎
  ) , All-resp-↭ x∷ys↭ys' (x≤y ∷ h) ∷ sorted-ys'
insert/correct x (y ∷ ys) (h ∷ hs) u | ⇓ true withCost q [ _ , _ ] | ofʸ x≤y | _ =
  x ∷ (y ∷ ys) , step/ext (F (list A)) (ret _) q u , refl , (x≤y ∷ ≤-≤* x≤y h) ∷ (h ∷ hs)

insert/cost : cmp (Π A λ _ → Π (list A) λ _ → cost)
insert/cost x []       = zero
insert/cost x (y ∷ ys) with h-cost x y
... | ⇓ false withCost q [ q≤1 , h-eq ] = q + (insert/cost x ys + zero)
... | ⇓ true  withCost q [ q≤1 , h-eq ] = q + 0

insert/cost/closed : cmp (Π A λ _ → Π (list A) λ _ → cost)
insert/cost/closed x l = length l

insert/cost≤insert/cost/closed : ∀ x l → ◯ (insert/cost x l Nat.≤ insert/cost/closed x l)
insert/cost≤insert/cost/closed x []       u = N.≤-refl
insert/cost≤insert/cost/closed x (y ∷ ys) u with h-cost x y
... | ⇓ false withCost q [ q≤1 , h-eq ] =
  Eq.subst (λ n → (q + n) Nat.≤ (suc (length ys))) (Eq.sym (+-identityʳ (insert/cost x ys))) (
    N.≤-trans
      (+-monoˡ-≤ _ (q≤1 u))
      (s≤s (insert/cost≤insert/cost/closed x ys u))
  )
... | ⇓ true  withCost q [ q≤1 , h-eq ] =
  Eq.subst (Nat._≤ (suc (length ys))) (Eq.sym (+-identityʳ q)) (
    N.≤-trans (q≤1 u) (s≤s z≤n)
  )

insert≤insert/cost : ∀ x l → IsBounded (list A) (insert x l) (insert/cost x l)
insert≤insert/cost x []       = bound/ret
insert≤insert/cost x (y ∷ ys) with h-cost x y
... | ⇓ false withCost q [ q≤1 , h-eq ] rewrite eq/ref h-eq =
  bound/step q (insert/cost x ys + 0) (bound/bind/const (insert/cost x ys) 0 (insert≤insert/cost x ys) λ _ → bound/ret)
... | ⇓ true  withCost q [ q≤1 , h-eq ] rewrite eq/ref h-eq =
  bound/step q 0 bound/ret

insert≤insert/cost/closed : ∀ x l → IsBounded (list A) (insert x l) (insert/cost/closed x l)
insert≤insert/cost/closed x l = bound/relax (insert/cost≤insert/cost/closed x l) (insert≤insert/cost x l)

sort : cmp (Π (list A) λ _ → F (list A))
sort []       = ret []
sort (x ∷ xs) = bind (F (list A)) (sort xs) (insert x)

sort/correct : IsSort sort
sort/correct []       u = [] , refl , refl , []
sort/correct (x ∷ xs) u =
  let (xs'   , h-xs'   , xs↭xs'     , sorted-xs'  ) = sort/correct xs u in
  let (x∷xs' , h-x∷xs' , x∷xs↭x∷xs' , sorted-x∷xs') = insert/correct x xs' sorted-xs' u in
  x∷xs' , (
    let open ≡-Reasoning in
    begin
      sort (x ∷ xs)
    ≡⟨⟩
      bind (F (list A)) (sort xs) (insert x)
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e (insert x)) h-xs' ⟩
      bind (F (list A)) (ret {list A} xs') (insert x)
    ≡⟨⟩
      insert x xs'
    ≡⟨ h-x∷xs' ⟩
      ret x∷xs'
    ∎
  ) , (
    let open PermutationReasoning in
    begin
      x ∷ xs
    <⟨ xs↭xs' ⟩
      x ∷ xs'
    ↭⟨ x∷xs↭x∷xs' ⟩
      x∷xs'
    ∎
  ) , sorted-x∷xs'

sort/cost : cmp (Π (list A) λ _ → cost)
sort/cost []       = 0
sort/cost (x ∷ xs) = bind cost (sort xs) (λ xs' → sort/cost xs + insert/cost/closed x xs')

sort/cost/closed : cmp (Π (list A) λ _ → cost)
sort/cost/closed l = length l ²

sort/cost≤sort/cost/closed : ∀ l → ◯ (sort/cost l Nat.≤ sort/cost/closed l)
sort/cost≤sort/cost/closed []       u = N.≤-refl
sort/cost≤sort/cost/closed (x ∷ xs) u =
  let (xs' , ≡ , ↭ , sorted) = sort/correct xs u in
  begin
    sort/cost (x ∷ xs)
  ≡⟨⟩
    bind cost (sort xs) (λ xs' → sort/cost xs + length xs')
  ≡⟨ Eq.cong (λ e → bind cost e λ xs' → sort/cost xs + length xs') (≡) ⟩
    sort/cost xs + length xs'
  ≡˘⟨ Eq.cong (sort/cost xs +_) (↭-length ↭) ⟩
    sort/cost xs + length xs
  ≤⟨ +-monoˡ-≤ (insert/cost/closed x xs) (sort/cost≤sort/cost/closed xs u) ⟩
    sort/cost/closed xs + insert/cost/closed x xs
  ≡⟨⟩
    length xs ² + length xs
  ≤⟨ lemma/arithmetic (length xs) ⟩
    length (x ∷ xs) ²
  ≡⟨⟩
    sort/cost/closed (x ∷ xs)
  ∎
    where
      open ≤-Reasoning

      lemma/arithmetic : ∀ n → n ² + n Nat.≤ suc n ²
      lemma/arithmetic n =
        begin
          n ² + n
        ≡⟨ N.+-comm (n ²) n ⟩
          n + n ²
        ≡⟨⟩
          n + n * n
        ≤⟨ N.m≤n+m (n + n * n) (suc n) ⟩
          suc n + (n + n * n)
        ≡⟨⟩
          suc (n + (n + n * n))
        ≡˘⟨ Eq.cong (λ m → suc (n + m)) (N.*-suc n n) ⟩
          suc (n + n * suc n)
        ≡⟨⟩
          suc n ²
        ∎

sort≤sort/cost : ∀ l → IsBounded (list A) (sort l) (sort/cost l)
sort≤sort/cost []       = bound/ret
sort≤sort/cost (x ∷ xs) = bound/bind (sort/cost xs) (insert/cost/closed x) (sort≤sort/cost xs) (insert≤insert/cost/closed x)

sort≤sort/cost/closed : ∀ l → IsBounded (list A) (sort l) (sort/cost/closed l)
sort≤sort/cost/closed l = bound/relax (sort/cost≤sort/cost/closed l) (sort≤sort/cost l)

sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n ²)
sort/asymptotic = 0 ≤n⇒f[n]≤g[n]via λ l _ → sort≤sort/cost/closed l

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
postulate Name : Set
{-# BUILTIN QNAME Name #-}

data ⊤ : Set where
  tt : ⊤

data Term : Set where
  con : Name → Term → Term

data X : ⊤ → Set where
  x : {t : ⊤} → X t

data Y : Set where
  y : Y

-- this type checks
g : {t : ⊤} → Term → X t
g {t} (con nm args) = x {t}

-- this doesn't
f : {t : ⊤} → Term → X t
f {t} (con (quote Y.y) args) = x {t}
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-- offending line is above
f t = x

-- t != args of type ⊤
-- when checking that the expression x {t} has type X args


text:
{-# OPTIONS --without-K #-}
module well-typed-quoted-syntax-defs where
open import common
open import well-typed-syntax
open import well-typed-syntax-helpers
open import well-typed-syntax-context-helpers

‘ε’ : Term {Γ = ε} ‘Context’
‘ε’ = ⌜ ε ⌝c

‘□’ : Typ (ε ▻ ‘Typ’ ‘’ ‘ε’)
‘□’ = ‘Term’ ‘’₁ ‘ε’

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
module Data.Fin.Map where

open import Class.Monad
open import Data.Nat
open import Data.Fin
open import Function

DepFinMap : ∀ {a} (n : ℕ) (A : Fin n -> Set a) -> Set a
DepFinMap n A = (k : Fin n) -> A k

FinMap : ∀ {a} (n : ℕ) -> Set a -> Set a
FinMap n A = DepFinMap n (λ _ -> A)

sequenceDepFinMap : ∀ {a n A} {M : Set a -> Set a} {{_ : Monad M}}
  -> DepFinMap n (λ x -> M $ A x) -> M (DepFinMap n A)
sequenceDepFinMap {n = zero} f = return λ ()
sequenceDepFinMap {n = suc n} f = do
  f' <- sequenceDepFinMap $ f ∘ suc
  fzero <- f zero
  return λ
    { zero → fzero
    ; (suc v) → f' v}

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import Cubical.HITs.Wedge.Base public

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
postulate
  A : Set
  P : A → Set

variable
  x : A
  y : P x

data D₁ {x : A} : P x → Set where
  z : D₁ y
  s : D₁ y → D₁ y

data D₂ : {x : A} → P x → Set where
  z : D₂ y
  s : D₂ y → D₂ y


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

open import Cubical.Algebra.Ring.Base public
open import Cubical.Algebra.Ring.Properties public


text:
module _ where

data Unit : Set where
  unit : Unit

data D₁ : Set where
  c₁ : D₁

module M (_ : Set₁) where

  data D₂ : Set where
    c₂ : D₂

open M Set

f : D₁ → D₂
f c₁ = c₂

record R (A : Set) : Set where
  field a : A

open R ⦃ … ⦄ public

instance

  r₁ : R D₁
  r₁ = record { a = c₁ }

  r₂ : ⦃ r : R D₁ ⦄ → R D₂
  r₂ ⦃ r ⦄ = record { a = f (R.a r) }

postulate
  P : (A : Set) → A → Set
  g : (A : Set) (x : A) → P A x

accepted : P D₂ a
accepted = g D₂ a

rejected : P D₂ a
rejected = g _ a

-- WAS:
--   No instance of type (R D₂) was found in scope.
--   when checking that the expression a has type D₂
-- SHOULD: succeed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Properties relating Initial and Terminal Objects,
-- Product / Coproduct, Zero objects, and Kernel / Cokernel via op
module Categories.Object.Duality {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Morphism C
open import Categories.Object.Terminal op
open import Categories.Object.Initial C
open import Categories.Object.Product op
open import Categories.Object.Coproduct C

open import Categories.Object.Zero

import Categories.Object.Kernel as Kernels
import Categories.Object.Cokernel as Cokernels

private
  variable
    A B X Z : Obj
    f g k : A ⇒ B

IsInitial⇒coIsTerminal : IsInitial X → IsTerminal X
IsInitial⇒coIsTerminal is⊥ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsInitial is⊥

⊥⇒op⊤ : Initial → Terminal
⊥⇒op⊤ i = record
  { ⊤             = ⊥
  ; ⊤-is-terminal = IsInitial⇒coIsTerminal ⊥-is-initial
  }
  where open Initial i

coIsTerminal⇒IsInitial : IsTerminal X → IsInitial X
coIsTerminal⇒IsInitial is⊤ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsTerminal is⊤

op⊤⇒⊥ : Terminal → Initial
op⊤⇒⊥ t = record
  { ⊥            = ⊤
  ; ⊥-is-initial = coIsTerminal⇒IsInitial ⊤-is-terminal
  }
  where open Terminal t

Coproduct⇒coProduct : Coproduct A B → Product A B
Coproduct⇒coProduct A+B = record
  { A×B      = A+B.A+B
  ; π₁       = A+B.i₁
  ; π₂       = A+B.i₂
  ; ⟨_,_⟩    = A+B.[_,_]
  ; project₁ = A+B.inject₁
  ; project₂ = A+B.inject₂
  ; unique   = A+B.unique
  }
  where
  module A+B = Coproduct A+B

coProduct⇒Coproduct : ∀ {A B} → Product A B → Coproduct A B
coProduct⇒Coproduct A×B = record
  { A+B     = A×B.A×B
  ; i₁      = A×B.π₁
  ; i₂      = A×B.π₂
  ; [_,_]   = A×B.⟨_,_⟩
  ; inject₁ = A×B.project₁
  ; inject₂ = A×B.project₂
  ; unique  = A×B.unique
  }
  where
  module A×B = Product A×B

-- Zero objects are autodual
IsZero⇒coIsZero : IsZero C Z → IsZero op Z
IsZero⇒coIsZero is-zero = record
  { isInitial = record { ! = ! ; !-unique = !-unique }
  ; isTerminal = record { ! = ¡ ; !-unique = ¡-unique }
  }
  where
    open IsZero is-zero

coIsZero⇒IsZero : IsZero op Z → IsZero C Z
coIsZero⇒IsZero co-is-zero = record
  { isInitial = record { ! = ! ; !-unique = !-unique }
  ; isTerminal = record { ! = ¡ ; !-unique = ¡-unique }
  }
  where
    open IsZero co-is-zero

coZero⇒Zero : Zero op → Zero C
coZero⇒Zero zero = record
  { 𝟘 = 𝟘
  ; isZero = coIsZero⇒IsZero isZero
  }
  where
    open Zero zero

Zero⇒coZero : Zero C → Zero op
Zero⇒coZero zero = record
  { 𝟘 = 𝟘
  ; isZero = IsZero⇒coIsZero isZero
  }
  where
    open Zero zero

-- Tests to ensure that dualities are involutive up to definitional equality.
private
  coIsTerminal⟺IsInitial : (⊥ : IsInitial X) → coIsTerminal⇒IsInitial (IsInitial⇒coIsTerminal ⊥) ≡ ⊥
  coIsTerminal⟺IsInitial _ = ≡.refl

  IsInitial⟺coIsTerminal : (⊤ : IsTerminal X) → IsInitial⇒coIsTerminal (coIsTerminal⇒IsInitial ⊤) ≡ ⊤
  IsInitial⟺coIsTerminal _ = ≡.refl

  ⊥⟺op⊤ : (⊤ : Terminal) → ⊥⇒op⊤ (op⊤⇒⊥ ⊤) ≡ ⊤
  ⊥⟺op⊤ _ = ≡.refl

  op⊤⟺⊥ : (⊥ : Initial) → op⊤⇒⊥ (⊥⇒op⊤ ⊥) ≡ ⊥
  op⊤⟺⊥ _ = ≡.refl

  Coproduct⟺coProduct : (p : Product A B) → Coproduct⇒coProduct (coProduct⇒Coproduct p) ≡ p
  Coproduct⟺coProduct _ = ≡.refl

  coProduct⟺Coproduct : (p : Coproduct A B) → coProduct⇒Coproduct (Coproduct⇒coProduct p) ≡ p
  coProduct⟺Coproduct _ = ≡.refl

  coIsZero⟺IsZero : {zero : IsZero op Z} → IsZero⇒coIsZero (coIsZero⇒IsZero zero) ≡ zero
  coIsZero⟺IsZero = ≡.refl

  IsZero⟺coIsZero : ∀ {Z} {zero : IsZero C Z} → coIsZero⇒IsZero (IsZero⇒coIsZero zero) ≡ zero
  IsZero⟺coIsZero = ≡.refl

  coZero⟺Zero : ∀ {zero : Zero op} → Zero⇒coZero (coZero⇒Zero zero) ≡ zero
  coZero⟺Zero = ≡.refl

  Zero⟺coZero : ∀ {zero : Zero C} → coZero⇒Zero (Zero⇒coZero zero) ≡ zero
  Zero⟺coZero = ≡.refl

module _ (𝟎 : Zero C) where
  open Kernels (Zero⇒coZero 𝟎)
  open Cokernels 𝟎

  coIsKernel⇒IsCokernel : IsKernel k f → IsCokernel f k
  coIsKernel⇒IsCokernel isKernel = record
    { commute = commute
    ; universal = universal
    ; factors = factors
    ; unique = unique
    }
    where
      open IsKernel isKernel

  IsCokernel⇒coIsKernel : IsCokernel f k → IsKernel k f
  IsCokernel⇒coIsKernel isCokernel = record
    { commute = commute
    ; universal = universal
    ; factors = factors
    ; unique = unique
    }
    where
      open IsCokernel isCokernel

  coKernel⇒Cokernel : Kernel f → Cokernel f
  coKernel⇒Cokernel k = record
    { cokernel⇒ = kernel⇒
    ; isCokernel = coIsKernel⇒IsCokernel isKernel
    }
    where
      open Kernel k

  Cokernel⇒coKernel : Cokernel f → Kernel f
  Cokernel⇒coKernel k = record
    { kernel⇒ = cokernel⇒
    ; isKernel = IsCokernel⇒coIsKernel isCokernel
    }
    where
      open Cokernel k

  private
    coIsKernel⟺IsCokernel : ∀ {isKernel : IsKernel k f} → IsCokernel⇒coIsKernel (coIsKernel⇒IsCokernel isKernel) ≡ isKernel
    coIsKernel⟺IsCokernel = ≡.refl

    IsCokernel⟺coIsKernel : ∀ {isCokernel : IsCokernel f k} → coIsKernel⇒IsCokernel (IsCokernel⇒coIsKernel isCokernel) ≡ isCokernel
    IsCokernel⟺coIsKernel = ≡.refl

    coKernel⟺Cokernel : ∀ {kernel : Kernel f} → Cokernel⇒coKernel (coKernel⇒Cokernel kernel) ≡ kernel
    coKernel⟺Cokernel = ≡.refl

    Cokernel⟺coKernel : ∀ {cokernel : Cokernel f} → coKernel⇒Cokernel (Cokernel⇒coKernel cokernel) ≡ cokernel
    Cokernel⟺coKernel = ≡.refl

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:
{-# OPTIONS --safe --without-K #-}

open import Relation.Nullary.Decidable using (True; toWitness)
open import Function using (_∘_)

import Data.Product as Product
import Data.Unit as Unit
import Data.Fin as Fin
import Data.Nat as Nat
import Data.Vec as Vec
import Data.Vec.Relation.Unary.All as All

open Product using (Σ; Σ-syntax; _×_; _,_; proj₁)
open Unit using (⊤; tt)
open Nat using (ℕ; zero; suc)
open Fin using (Fin; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)

open import PiCalculus.Syntax
open Scoped
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem (Ω : Algebras) where
open Algebras Ω

infixr 4 _；_⊢_▹_
infixr 4 _；_∋[_]_；_▹_ _∋[_]_▹_ _∋[_]_
infixr 10 ν _⦅⦆_ _⟨_⟩_

private
  variable
    name : Name
    idx idx' : Idx
    n : ℕ
    i j : Fin n

data Type : Set where
  𝟙      : Type
  B[_]   : ℕ → Type
  C[_；_] : Type → (Usage idx) ² → Type
  -- P[_&_] : Type → Type → Type

-- Context of types
PreCtx : ℕ → Set
PreCtx = Vec Type

-- Context of usage indices
Idxs : ℕ → Set
Idxs = Vec Idx

-- Indexed context of usages
Ctx : ∀ {n} → Idxs n → Set
Ctx = All λ idx → (Usage idx) ²

private
  variable
    γ : PreCtx n
    idxs : Idxs n
    Γ Δ Ξ Θ : Ctx idxs
    b : ℕ
    t t' : Type
    x y z : Usage idx
    P Q : Scoped n

-- γ ∋[ i ] t is a proof that variable i in Γ has type t
data _∋[_]_ : PreCtx n → Fin n → Type → Set where
  zero : γ -, t ∋[ zero ] t
  suc : γ ∋[ i ] t → γ -,  t' ∋[ suc i ] t

-- Γ ∋[ i ] x ▹ Δ is a proof that subtracting x from variable in in Γ results in Δ
data _∋[_]_▹_ : {idxs : Idxs n} → Ctx idxs → Fin n → (Usage idx) ² → Ctx idxs → Set where

  zero : {idxs : Idxs n} {Γ : Ctx idxs} {x y z : Usage idx ²}
       → x ≔ y ∙² z
       → Γ -, x ∋[ zero {n} ] y ▹ Γ -, z

  suc : {Γ Δ : Ctx idxs} {x : (Usage idx) ² } {x' : (Usage idx') ²}
      → Γ ∋[ i ] x ▹ Δ
      → Γ -, x' ∋[ suc i ] x ▹ Δ -, x'

-- For convenience, merge together γ ∋[ i ] t and Γ ∋[ i ] x ▹ Δ
_；_∋[_]_；_▹_ : {idxs : Idxs n} → PreCtx n → Ctx idxs → Fin n → Type → (Usage idx) ² → Ctx idxs → Set
γ ； Γ ∋[ i ] t ； x ▹ Δ = (γ ∋[ i ] t) × (Γ ∋[ i ] x ▹ Δ)

-- Constructor for (zero , zero xyz) that computes z from x and y
here : {γ : PreCtx n} {idxs : Idxs n} {Γ : Ctx idxs} {x y : Usage idx ²} ⦃ check : True (∙²-computeʳ x y) ⦄
     → γ -, t ； Γ -, x ∋[ zero ] t ； y ▹ Γ -, proj₁ (toWitness check)
here ⦃ check ⦄ = let _ , x≔y∙²z = toWitness check in zero , zero x≔y∙²z

infixr 20 there_
there_ : {γ : PreCtx n} {idxs : Idxs n} {Γ Δ : Ctx idxs} {x : Usage idx ²} {x' : Usage idx' ²}
       → γ       ； Γ       ∋[     i ] t ； x ▹ Δ
       → γ -, t' ； Γ -, x' ∋[ suc i ] t ； x ▹ Δ -, x'
there_ (i , j) = suc i , suc j

-- Typing judgment γ ； Γ ⊢ P ▹ Δ where P is a well-typed process
-- under typing context γ and input and output usage contexts Γ and Δ
data _；_⊢_▹_ : {idxs : Idxs n} → PreCtx n → Ctx idxs → Scoped n → Ctx idxs → Set where

  𝟘 : γ ； Γ ⊢ 𝟘 ▹ Γ

  -- Note (μ , μ): the created channel is balanced
  ν : ∀ (t : Type) {idx' : Idx} (m : Usage idx' ²) {idx : Idx} (μ : Usage idx)
    → γ -, C[ t ； m ] ； Γ -, (μ , μ) ⊢ P            ▹ Δ -, ℓ∅
    -----------------------------------------------------
    → γ               ； Γ             ⊢ ν P ⦃ name ⦄ ▹ Δ

  _⦅⦆_ : ∀ {t : Type} {m : (Usage idx') ²}
       → γ      ； Γ       ∋[ i ] C[ t ； m ] ； ℓᵢ {idx} ▹ Ξ
       → γ -, t ； Ξ -, m  ⊢      P                      ▹ Θ -, ℓ∅
       -----------------------------------------------------------
       → γ      ； Γ       ⊢ (i ⦅⦆ P) ⦃ name ⦄           ▹ Θ

  _⟨_⟩_ : {t : Type} {m : (Usage idx') ²}
        → γ ； Γ ∋[ i ] C[ t ； m ] ； ℓₒ {idx} ▹ Δ
        → γ ； Δ ∋[ j ] t           ； m        ▹ Ξ
        → γ ； Ξ ⊢      P                       ▹ Θ
        -----------------------------------------
        → γ ； Γ ⊢      i ⟨ j ⟩ P               ▹ Θ

  _∥_ : γ ； Γ ⊢ P     ▹ Δ
      → γ ； Δ ⊢ Q     ▹ Ξ
      -------------------
      → γ ； Γ ⊢ P ∥ Q ▹ Ξ

_；[_]_⊢_▹_ : PreCtx n → (idxs : Idxs n) → Ctx idxs → Scoped n → Ctx idxs → Set
γ ；[ idxs ] Γ ⊢ P ▹ Δ = _；_⊢_▹_ {idxs = idxs} γ Γ P Δ

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
------------------------------------------------------------------------
-- A delimited continuation monad
------------------------------------------------------------------------

module Category.Monad.Continuation where

open import Category.Applicative
open import Category.Applicative.Indexed
open import Category.Monad
open import Category.Monad.Indexed
open import Category.Monad.Identity

open import Data.Function

------------------------------------------------------------------------
-- Delimited continuation monads

DContT : {I : Set} → (I → Set) → (Set → Set) → IFun I
DContT K M r₂ r₁ a = (a → M (K r₁)) → M (K r₂)

DCont : {I : Set} → (I → Set) → IFun I
DCont K = DContT K Identity

DContTIMonad : ∀ {I} (K : I → Set) {M} →
               RawMonad M → RawIMonad (DContT K M)
DContTIMonad K Mon = record
  { return = λ a k → k a
  ; _>>=_  = λ c f k → c (flip f k)
  }
  where open RawMonad Mon

DContIMonad : ∀ {I} (K : I → Set) → RawIMonad (DCont K)
DContIMonad K = DContTIMonad K IdentityMonad

------------------------------------------------------------------------
-- Delimited continuation operations

record RawIMonadDCont {I : Set} (K : I → Set)
                      (M : I → I → Set → Set) : Set₁ where
  field
    monad : RawIMonad M
    reset : ∀ {r₁ r₂ r₃} → M r₁ r₂ (K r₂) → M r₃ r₃ (K r₁)
    shift : ∀ {a r₁ r₂ r₃ r₄} →
            ((a → M r₁ r₁ (K r₂)) → M r₃ r₄ (K r₄)) → M r₃ r₂ a

  open RawIMonad monad public

DContTIMonadDCont : ∀ {I} (K : I → Set) {M} →
                    RawMonad M → RawIMonadDCont K (DContT K M)
DContTIMonadDCont K Mon = record
  { monad = DContTIMonad K Mon
  ; reset = λ e k → e return >>= k
  ; shift = λ e k → e (λ a k' → (k a) >>= k') return
  }
  where
  open RawIMonad Mon

DContIMonadDCont : ∀ {I} (K : I → Set) → RawIMonadDCont K (DCont K)
DContIMonadDCont K = DContTIMonadDCont K IdentityMonad


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

open import Basics
open import lib.Basics
open import Flat

module Axiom.C0 {@♭ i j : ULevel} (@♭ I : Type i) (@♭ R : I → Type j) where
    postulate C0 : {@♭ k : ULevel} (@♭ A : Type k)
                   (p : (index : I) → (is-equiv (λ (a : A) → λ (r : R index) → a)))
                   → A is-discrete

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
module Common.Unit where

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}
{-# COMPILED_DATA_UHC Unit __UNIT__ __UNIT__ #-}


text:
module Classical where

open import Data.Empty using (⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)

open import Negation using (¬_)

-- 排中律 → 二重否定の除去
em-→-¬¬-elim :
    (∀ {A : Set} → A ⊎ ¬ A)
    -------------------------
  → (∀ {A : Set} → ¬ ¬ A → A)
em-→-¬¬-elim a⊎¬a ¬¬a with a⊎¬a
...                      | inj₁ a  = a
...                      | inj₂ ¬a = ⊥-elim (¬¬a ¬a)

-- 排中律 → パースの法則
em-→-peirce :
    (∀ {A : Set} → A ⊎ ¬ A)
    -----------------------------------
  → (∀ {A B : Set} → ((A → B) → A) → A)
em-→-peirce a⊎¬a [a→b]→a with a⊎¬a
...                         | inj₁ a  = a
...                         | inj₂ ¬a = [a→b]→a (λ a → ⊥-elim (¬a a))

-- 排中律 → 直和としての含意
em-→-iad :
    (∀ {A : Set} → A ⊎ ¬ A)
    -------------------------------------
  → (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
em-→-iad a⊎¬a a→b with a⊎¬a
...                  | inj₁ a  = inj₂ (a→b a)
...                  | inj₂ ¬a = inj₁ ¬a

-- 排中律 → ド・モルガンの法則
em-→-demorgan :
    (∀ {A : Set} → A ⊎ ¬ A)
    ---------------------------------------
  → (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
em-→-demorgan a⊎¬a {A} {B} ¬[¬a×¬b] with a⊎¬a {A} | a⊎¬a {B}
...                                    | inj₁ a   | _        = inj₁ a
...                                    | inj₂ ¬a  | inj₁ b   = inj₂ b
...                                    | inj₂ ¬a  | inj₂ ¬b  = ⊥-elim (¬[¬a×¬b] ⟨ ¬a , ¬b ⟩)

-- 二重否定の除去 → 排中律
-- (¬¬ A → A) の A を (A ⊎ ¬ A) と見なす
-- ¬¬ (A ⊎ ¬ A) → (A ⊎ ¬ A)
¬¬-elim-→-em :
    (∀ {A : Set} → ¬ ¬ A → A)
    -------------------------
  → (∀ {A : Set} → A ⊎ ¬ A)
¬¬-elim-→-em ¬¬[a⊎¬a]→[a⊎¬a] = ¬¬[a⊎¬a]→[a⊎¬a] (λ ¬[a⊎¬a] → ¬[a⊎¬a] (inj₂ (λ a → ¬[a⊎¬a] (inj₁ a))))

-- 二重否定の除去 → パースの法則
¬¬-elim-→-peirce :
    (∀ {A : Set} → ¬ ¬ A → A)
    -----------------------------------
  → (∀ {A B : Set} → ((A → B) → A) → A)
¬¬-elim-→-peirce ¬¬a→a [a→b]→a = ¬¬a→a (λ ¬a → ¬a ([a→b]→a (λ a → ⊥-elim (¬a a))))

-- 二重否定の除去 → 直和としての含意
-- (¬¬ A → A) の A を (¬ A ⊎ B) と見なす
-- ¬¬ (¬ A ⊎ B) → (¬ A ⊎ B)
¬¬-elim-→-iad :
    (∀ {A : Set} → ¬ ¬ A → A)
    -------------------------------------
  → (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
¬¬-elim-→-iad ¬¬[¬a⊎b]→[¬a⊎b] a→b = ¬¬[¬a⊎b]→[¬a⊎b] (λ ¬[¬a⊎b] → ¬[¬a⊎b] (inj₁ (λ a → ¬[¬a⊎b] (inj₂ (a→b a)))))

-- 二重否定の除去 → ド・モルガンの法則
-- (¬¬ A → A) の A を (A ⊎ B) と見なす
-- ¬¬ (A ⊎ B) → (A ⊎ B)
¬¬-elim-→-demorgan :
    (∀ {A : Set} → ¬ ¬ A → A)
    ---------------------------------------
  → (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
¬¬-elim-→-demorgan ¬¬[a⊎b]→[a⊎b] ¬[¬a×¬b] = ¬¬[a⊎b]→[a⊎b] (λ ¬[a⊎b] → ¬[¬a×¬b] ⟨ (λ a → ¬[a⊎b] (inj₁ a)) , (λ b → ¬[a⊎b] (inj₂ b)) ⟩)

-- パースの法則 → 排中律
-- ((A → B) → A) → A) の A を (A ⊎ ¬ A) と見なす
-- ((((A ⊎ ¬ A) → B) → (A ⊎ ¬ A)) → (A ⊎ ¬ A))
peirce-→-em :
    (∀ {A B : Set} → ((A → B) → A) → A)
    -----------------------------------
  → (∀ {A : Set} → A ⊎ ¬ A)
peirce-→-em [[[a⊎¬a]→b]→[a⊎¬a]]→[a⊎¬a] = [[[a⊎¬a]→b]→[a⊎¬a]]→[a⊎¬a] (λ [a⊎¬a]→b → inj₂ (λ a → [a⊎¬a]→b (inj₁ a)))

-- パースの法則 → 二重否定の除去
-- ((A → B) → A) → A) の A を (¬¬ A → A) と見なす
-- (((¬¬ A → A) → B) → (¬¬ A → A)) → (¬¬ A → A))
peirce-→-¬¬-elim :
    (∀ {A B : Set} → ((A → B) → A) → A)
    -----------------------------------
  → (∀ {A : Set} → ¬ ¬ A → A)
peirce-→-¬¬-elim [[[¬¬a→a]→b]→[¬¬a→a]]→[¬¬a→a] = [[[¬¬a→a]→b]→[¬¬a→a]]→[¬¬a→a] (λ [¬¬a→a]→b → (λ ¬¬a → ⊥-elim (¬¬a (λ a → [¬¬a→a]→b (λ ¬¬a → a)))))

-- パースの法則 → 直和としての含意
-- ((A → B) → A) → A の A を ¬ A ⊎ B, B を ⊥ と見なす
-- (¬ (¬ A ⊎ B)) → (¬ A ⊎ B) → (¬ A ⊎ B)
peirce-→-iad :
    (∀ {A B : Set} → ((A → B) → A) → A)
    -------------------------------------
  → (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
peirce-→-iad [¬[¬a⊎b]→[¬a⊎b]]→[¬a⊎b] a→b = [¬[¬a⊎b]→[¬a⊎b]]→[¬a⊎b] (λ ¬[¬a⊎b] → inj₁ (λ a → ¬[¬a⊎b] (inj₂ (a→b a))))

-- パースの法則 → ド・モルガンの法則
-- ((A → B) → A) → A) の A を (A ⊎ B), B を ⊥ と見なす
-- (¬ (A ⊎ B) → (A ⊎ B)) → (A ⊎ B)
peirce-→-demorgan :
    (∀ {A B : Set} → ((A → B) → A) → A)
    ---------------------------------------
  → (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
peirce-→-demorgan ¬[a⊎b]→[a⊎b]→[a⊎b] ¬[¬a×¬b] = ¬[a⊎b]→[a⊎b]→[a⊎b] (λ ¬[a⊎b] → ⊥-elim (¬[¬a×¬b] ⟨ (λ a → ¬[a⊎b] (inj₁ a)) , (λ b → ¬[a⊎b] (inj₂ b)) ⟩))

-- 直和としての含意 → 排中律
-- (A → B) → ¬ A ⊎ B は B を A と見ることで排中律と同じように扱える
-- (A → A) → ¬ A ⊎ A
iad-→-em :
    (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
    -----------------------------------
  → (∀ {A : Set} → A ⊎ ¬ A)
iad-→-em [a→b]→¬a⊎b with [a→b]→¬a⊎b (λ a → a)
...                    | inj₁ ¬a              = inj₂ ¬a
...                    | inj₂ a               = inj₁ a

-- 直和としての含意 → 二重否定の除去
iad-→-¬¬-elim :
    (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
    -----------------------------------
  → (∀ {A : Set} → ¬ ¬ A → A)
iad-→-¬¬-elim [a→b]→¬a⊎b with [a→b]→¬a⊎b (λ a → a)
...                         | inj₁ ¬a              = λ ¬¬a → ⊥-elim (¬¬a ¬a)
...                         | inj₂ a               = λ ¬¬a → a

-- 直和としての含意 → パースの法則
iad-→-peirce :
    (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
    -----------------------------------
  → (∀ {A B : Set} → ((A → B) → A) → A)
iad-→-peirce [a→b]→¬a⊎b [a→b]→a with [a→b]→¬a⊎b (λ a → a)
...                                | inj₁ ¬a              = [a→b]→a (λ a → ⊥-elim (¬a a))
...                                | inj₂ a               = a

-- 直和としての含意 → ド・モルガンの法則
iad-→-demorgan :
    (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
    ---------------------------------------
  → (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
iad-→-demorgan [a→b]→¬a⊎b {A} {B} ¬[¬a×¬b] with [a→b]→¬a⊎b {A} {A} (λ a → a) | [a→b]→¬a⊎b {B} {B} (λ b → b)
...                                           | inj₁ ¬a                      | inj₁ ¬b                      = ⊥-elim (¬[¬a×¬b] ⟨ ¬a , ¬b ⟩)
...                                           | inj₂ a                       | _                            = inj₁ a
...                                           | inj₁ ¬a                      | inj₂ b                       = inj₂ b

-- ド・モルガンの法則 → 排中律
demorgan-→-em :
    (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
    ---------------------------------------
  → (∀ {A : Set} → A ⊎ ¬ A)
demorgan-→-em ¬[¬a×¬b]→a⊎b = ¬[¬a×¬b]→a⊎b (λ{ (⟨ ¬a , ¬¬a ⟩) → ¬¬a ¬a })

-- ド・モルガンの法則 → 二重否定の除去
-- (¬ (¬ A × ¬ B) → A ⊎ B) の B を A と見なす
-- ¬ (¬ A × ¬ A) → A ⊎ A
demorgan-→-¬¬-elim :
    (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
    ---------------------------------------
  → (∀ {A : Set} → ¬ ¬ A → A)
demorgan-→-¬¬-elim ¬[¬a×¬b]→a⊎b {A} ¬¬a with ¬[¬a×¬b]→a⊎b {A} {A} λ{ (⟨ ¬a , ¬b ⟩) → ¬¬a ¬a }
...                                        | inj₁ a                                           = a
...                                        | inj₂ a                                           = a

-- ド・モルガンの法則 → パースの法則
-- (¬ (¬ A × ¬ B) → A ⊎ B) の B を A と見なす
-- ¬ (¬ A × ¬ A) → A ⊎ A
demorgan-→-peirce :
    (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
    ---------------------------------------
  → (∀ {A B : Set} → ((A → B) → A) → A)
demorgan-→-peirce ¬[¬¬a×¬b]→¬a⊎b {A} {B} [a→b]→a with ¬[¬¬a×¬b]→¬a⊎b {A} {A} λ{ (⟨ ¬a , ¬b ⟩) → ¬a ([a→b]→a (λ a → ⊥-elim (¬a a))) }
...                                                 | inj₁ a                                                                         = a
...                                                 | inj₂ a                                                                         = a

-- ド・モルガンの法則 → 直和としての含意
-- (¬ (¬ A × ¬ B) → A ⊎ B) の A を ¬A と見なす
-- ¬ (¬¬ A × ¬ B) → ¬ A ⊎ B
demorgan-→-iad :
    (∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B)
    ---------------------------------------
  → (∀ {A B : Set} → (A → B) → ¬ A ⊎ B)
demorgan-→-iad ¬[¬¬a×¬b]→¬a⊎b a→b = ¬[¬¬a×¬b]→¬a⊎b (λ (⟨ ¬¬a , ¬b ⟩) → ¬¬a (λ a → ¬b (a→b a)))

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module PLRTree.Equality {A : Set} where

open import PLRTree {A}

data _≃_ : PLRTree → PLRTree → Set where
  ≃lf : leaf ≃ leaf
  ≃nd : {l r l' r' : PLRTree}
                   (x x' : A)
                   → l ≃ r
                   → l' ≃ r'
                   → l ≃ l'
                   → node perfect x l r ≃ node perfect x' l' r'

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between ring-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core

module Algebra.Morphism.RingMonomorphism
  {a b ℓ₁ ℓ₂} {R₁ : RawRing a ℓ₁} {R₂ : RawRing b ℓ₂} {⟦_⟧}
  (isRingMonomorphism : IsRingMonomorphism R₁ R₂ ⟦_⟧)
  where

open IsRingMonomorphism isRingMonomorphism
open RawRing R₁ renaming (Carrier to A; _≈_ to _≈₁_)
open RawRing R₂ renaming
  ( Carrier to B; _≈_ to _≈₂_; _+_ to _⊕_
  ; _*_ to _⊛_; 1# to 1#₂; 0# to 0#₂; -_ to ⊝_)

open import Algebra.Definitions
open import Algebra.Structures
open import Data.Product
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

------------------------------------------------------------------------
-- Re-export all properties of group and monoid monomorphisms

open import Algebra.Morphism.GroupMonomorphism
  +-isGroupMonomorphism renaming
  ( assoc to +-assoc
  ; comm to +-comm
  ; cong to +-cong
  ; idem to +-idem
  ; identity to +-identity; identityˡ to +-identityˡ; identityʳ to +-identityʳ
  ; cancel to +-cancel; cancelˡ to +-cancelˡ; cancelʳ to +-cancelʳ
  ; zero to +-zero; zeroˡ to +-zeroˡ; zeroʳ to +-zeroʳ
  ; isMagma to +-isMagma
  ; isSemigroup to +-isSemigroup
  ; isMonoid to +-isMonoid
  ; isSelectiveMagma to +-isSelectiveMagma
  ; isSemilattice to +-isSemilattice
  ; sel to +-sel
  ; isBand to +-isBand
  ; isCommutativeMonoid to +-isCommutativeMonoid
  ) public

open import Algebra.Morphism.MonoidMonomorphism
  *-isMonoidMonomorphism renaming
  ( assoc to *-assoc
  ; comm to *-comm
  ; cong to *-cong
  ; idem to *-idem
  ; identity to *-identity; identityˡ to *-identityˡ; identityʳ to *-identityʳ
  ; cancel to *-cancel; cancelˡ to *-cancelˡ; cancelʳ to *-cancelʳ
  ; zero to *-zero; zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ
  ; isMagma to *-isMagma
  ; isSemigroup to *-isSemigroup
  ; isMonoid to *-isMonoid
  ; isSelectiveMagma to *-isSelectiveMagma
  ; isSemilattice to *-isSemilattice
  ; sel to *-sel
  ; isBand to *-isBand
  ; isCommutativeMonoid to *-isCommutativeMonoid
  ) public

------------------------------------------------------------------------
-- Properties

module _ (+-isGroup : IsGroup  _≈₂_ _⊕_ 0#₂ ⊝_)
         (*-isMagma : IsMagma _≈₂_ _⊛_) where

  open IsGroup +-isGroup hiding (setoid; refl)
  open IsMagma *-isMagma renaming (∙-cong to ◦-cong)
  open SetoidReasoning setoid

  distribˡ : _DistributesOverˡ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverˡ_ _≈₁_ _*_ _+_
  distribˡ distribˡ x y z = injective (begin
    ⟦ x * (y + z) ⟧               ≈⟨ *-homo x (y + z) ⟩
    ⟦ x ⟧ ⊛ ⟦ y + z ⟧             ≈⟨ ◦-cong refl (+-homo y z) ⟩
    ⟦ x ⟧ ⊛ (⟦ y ⟧ ⊕ ⟦ z ⟧)       ≈⟨ distribˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
    ⟦ x ⟧ ⊛ ⟦ y ⟧ ⊕ ⟦ x ⟧ ⊛ ⟦ z ⟧ ≈˘⟨ ∙-cong (*-homo x y) (*-homo x z) ⟩
    ⟦ x * y ⟧ ⊕ ⟦ x * z ⟧         ≈˘⟨ +-homo (x * y) (x * z) ⟩
    ⟦ x * y + x * z ⟧ ∎)

  distribʳ : _DistributesOverʳ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverʳ_ _≈₁_ _*_ _+_
  distribʳ distribˡ x y z = injective (begin
    ⟦ (y + z) * x ⟧               ≈⟨ *-homo (y + z) x ⟩
    ⟦ y + z ⟧ ⊛ ⟦ x ⟧             ≈⟨ ◦-cong (+-homo y z) refl ⟩
    (⟦ y ⟧ ⊕ ⟦ z ⟧) ⊛ ⟦ x ⟧       ≈⟨ distribˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
    ⟦ y ⟧ ⊛ ⟦ x ⟧ ⊕ ⟦ z ⟧ ⊛ ⟦ x ⟧ ≈˘⟨ ∙-cong (*-homo y x) (*-homo z x) ⟩
    ⟦ y * x ⟧ ⊕ ⟦ z * x ⟧         ≈˘⟨ +-homo (y * x) (z * x) ⟩
    ⟦ y * x + z * x ⟧ ∎)

  distrib : _DistributesOver_ _≈₂_ _⊛_ _⊕_ → _DistributesOver_ _≈₁_ _*_ _+_
  distrib distrib = distribˡ (proj₁ distrib) , distribʳ (proj₂ distrib)

  zeroˡ : LeftZero _≈₂_ 0#₂ _⊛_ → LeftZero _≈₁_ 0# _*_
  zeroˡ zeroˡ x = injective (begin
    ⟦ 0# * x ⟧     ≈⟨ *-homo 0# x ⟩
    ⟦ 0# ⟧ ⊛ ⟦ x ⟧ ≈⟨ ◦-cong 0#-homo refl ⟩
    0#₂ ⊛ ⟦ x ⟧    ≈⟨ zeroˡ ⟦ x ⟧ ⟩
    0#₂            ≈˘⟨ 0#-homo ⟩
    ⟦ 0# ⟧         ∎)

  zeroʳ : RightZero _≈₂_ 0#₂ _⊛_ → RightZero _≈₁_ 0# _*_
  zeroʳ zeroʳ x = injective (begin
    ⟦ x * 0# ⟧     ≈⟨ *-homo x 0# ⟩
    ⟦ x ⟧ ⊛ ⟦ 0# ⟧ ≈⟨ ◦-cong refl 0#-homo ⟩
    ⟦ x ⟧ ⊛ 0#₂    ≈⟨ zeroʳ ⟦ x ⟧ ⟩
    0#₂            ≈˘⟨ 0#-homo ⟩
    ⟦ 0# ⟧         ∎)

  zero : Zero _≈₂_ 0#₂ _⊛_ → Zero _≈₁_ 0# _*_
  zero zero = zeroˡ (proj₁ zero) , zeroʳ (proj₂ zero)

isRing : IsRing _≈₂_ _⊕_ _⊛_ ⊝_ 0#₂ 1#₂ → IsRing _≈₁_ _+_ _*_ -_ 0# 1#
isRing isRing = record
  { +-isAbelianGroup = isAbelianGroup R.+-isAbelianGroup
  ; *-isMonoid       = *-isMonoid R.*-isMonoid
  ; distrib          = distrib R.+-isGroup R.*-isMagma R.distrib
  ; zero             = zero R.+-isGroup R.*-isMagma R.zero
  } where module R = IsRing isRing


text:
module builtinInModule where

module Int where

  postulate I : Set
  {-# BUILTIN INTEGER I #-}
  primitive primIntegerPlus : I -> I -> I

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-

This file contains:

- Definition of set coequalizers as performed in https://1lab.dev/Data.Set.Coequaliser.html

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.SetCoequalizer.Base where

open import Cubical.Core.Primitives

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

-- Set coequalizers as a higher inductive type
data SetCoequalizer {A : Type ℓ} {B : Type ℓ'} (f g : A → B) : Type (ℓ-max ℓ ℓ') where
  inc    : B → SetCoequalizer f g
  coeq   : (a : A) → inc (f a) ≡ inc (g a)
  squash : (x y : SetCoequalizer f g) → (p q : x ≡ y) → p ≡ q

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{- NEW TRANSLATION: notation change to avoid exponential increase in term size during translation -}

open import Preliminaries
open import Source
open import Pilot2

module Translation where

  mutual
    ⟨⟨_⟩⟩ : Tp → CTp
    ⟨⟨ unit ⟩⟩ = unit
    ⟨⟨ nat ⟩⟩ = nat
    ⟨⟨ susp A ⟩⟩ = || A ||
    ⟨⟨ A ->s B ⟩⟩ = ⟨⟨ A ⟩⟩ ->c || B ||
    ⟨⟨ A ×s B ⟩⟩ = ⟨⟨ A ⟩⟩ ×c ⟨⟨ B ⟩⟩
    ⟨⟨ list A ⟩⟩ = list ⟨⟨ A ⟩⟩
    ⟨⟨ bool ⟩⟩ = bool

    ||_|| : Tp → CTp
    || τ || = C ×c ⟨⟨ τ ⟩⟩

  ⟨⟨_⟩⟩c : Source.Ctx → Pilot2.Ctx
  ⟨⟨ [] ⟩⟩c = []
  ⟨⟨ x :: Γ ⟩⟩c = ⟨⟨ x ⟩⟩ :: ⟨⟨ Γ ⟩⟩c

  interp-Cost : ∀{Γ} → Cost → Γ Pilot2.|- C
  interp-Cost 0c = 0C
  interp-Cost 1c = 1C
  interp-Cost (m +c n) = plusC (interp-Cost m) (interp-Cost n)

  lookup : ∀{Γ τ} → τ Source.∈ Γ → ⟨⟨ τ ⟩⟩ Pilot2.∈ ⟨⟨ Γ ⟩⟩c
  lookup i0 = i0
  lookup (iS x) = iS (lookup x)

  throw-s : ∀ {Γ Γ' τ} → Pilot2.sctx Γ (τ :: Γ') → Pilot2.sctx Γ Γ'
  throw-s Θ x = Θ (iS x)

  -- translation from source expressions to complexity expressions
  ||_||e : ∀{Γ τ} → Γ Source.|- τ → ⟨⟨ Γ ⟩⟩c Pilot2.|- || τ ||
  || unit ||e = prod 0C unit
  || var x ||e = prod 0C (var (lookup x))
  || z ||e = prod 0C z
  || suc e ||e = (letc (prod (l-proj (var i0)) (s (r-proj (var i0)))) || e ||e)
  || rec e e0 e1 ||e =
    letc (l-proj (var i0) +C rec (r-proj (var i0))
      (Pilot2.wkn (1C +C || e0 ||e)) (Pilot2.subst (1C +C || e1 ||e) (Pilot2.s-extend (Pilot2.s-extend (throw-s Pilot2.ids))))) || e ||e
  || lam e ||e = prod 0C (lam || e ||e)
  || app e1 e2 ||e = letc (letc (prod (plusC (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (l-proj (app (r-proj (var (iS i0))) (r-proj (var i0)))))
                          (r-proj (app (r-proj (var (iS i0))) (r-proj (var i0))))) (Pilot2.wkn || e2 ||e)) || e1 ||e
  || prod e1 e2 ||e = letc (letc (prod (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (prod (r-proj (var (iS i0))) (r-proj (var i0)))) (Pilot2.wkn || e2 ||e)) || e1 ||e
  || delay e ||e = prod 0C || e ||e
  || force e ||e = letc (prod (plusC (l-proj (var i0)) (l-proj (r-proj (var i0)))) (r-proj (r-proj (var i0)))) || e ||e
  || split e0 e1 ||e = letc (prod (plusC (Pilot2.wkn (l-proj || e0 ||e)) (l-proj (var i0))) (r-proj (var i0))) E1
    where E1 = letc (Pilot2.subst || e1 ||e (Pilot2.lem4 (l-proj (r-proj (var i0))) (r-proj (r-proj (var i0))) Pilot2.ss Pilot2.s-extend (Pilot2.s-extend (throw-s Pilot2.ids)))) || e0 ||e
  || nil ||e = prod 0C nil
  || e ::s e₁ ||e = letc (letc (prod (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (r-proj (var (iS i0)) ::c r-proj (var i0))) (Pilot2.wkn || e₁ ||e)) || e ||e
  || listrec e e₁ e₂ ||e =
    letc (l-proj (var i0) +C listrec (r-proj (var i0))
     (Pilot2.wkn (1C +C || e₁ ||e)) (Pilot2.subst (1C +C || e₂ ||e) (Pilot2.s-extend (Pilot2.s-extend (Pilot2.s-extend (throw-s Pilot2.ids)))))) || e ||e
  || true ||e = prod 0C true
  || false ||e = prod 0C false

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Orders.Archimedean
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Fields.Orders.Total.Archimedean

module Fields.CauchyCompletion.Archimedean {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (arch : ArchimedeanField {F = F} (record { oRing = pRing })) where

open import Fields.CauchyCompletion.Group order F
open import Fields.CauchyCompletion.Ring order F
open import Fields.CauchyCompletion.Comparison order F
open import Fields.CauchyCompletion.PartiallyOrderedRing order F

CArchimedean : Archimedean (toGroup CRing CpOrderedRing)
CArchimedean x y xPos yPos = {!!}