text:
------------------------------------------------------------------------
-- A coinductive definition of the expansion ordering
------------------------------------------------------------------------

-- The definition of expansion is based on the one in "Enhancements of
-- the bisimulation proof method" by Pous and Sangiorgi.

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

open import Labelled-transition-system

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

open import Equality.Propositional
open import Prelude
open import Prelude.Size

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.General
open import Equational-reasoning
open import Indexed-container using (Container; ν; ν′)
open import Relation

open LTS lts
private
  open module SB = Bisimilarity lts
    using (_∼_; _∼′_; [_]_∼_; [_]_∼′_)

private
  module General = Bisimilarity.General lts _[_]⟶̂_ _[_]⇒_ ⟶→⟶̂ ⟶→[]⇒

open General public
  using (module StepC; ⟨_,_⟩; left-to-right; right-to-left; force;
         [_]_≡_; [_]_≡′_; []≡↔;
         Extensionality; extensionality)
  renaming ( reflexive-∼ to reflexive-≳
           ; reflexive-∼′ to reflexive-≳′
           ; ≡⇒∼ to ≡⇒≳
           ; ∼:_ to ≳:_
           ; ∼′:_ to ≳′:_
           )

-- StepC is given in the following way, rather than via open public,
-- to make hyperlinks to it more informative.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = General.StepC

-- The following definitions are given explicitly, to make the code
-- easier to follow for readers of the paper.

Expansion : Size → Rel₂ ℓ Proc
Expansion = ν StepC

Expansion′ : Size → Rel₂ ℓ Proc
Expansion′ = ν′ StepC

infix 4 _≳_ _≳′_ [_]_≳_ [_]_≳′_

[_]_≳_ : Size → Proc → Proc → Type ℓ
[ i ] p ≳ q = ν StepC i (p , q)

[_]_≳′_ : Size → Proc → Proc → Type ℓ
[ i ] p ≳′ q = ν′ StepC i (p , q)

_≳_ : Proc → Proc → Type ℓ
_≳_ = [ ∞ ]_≳_

_≳′_ : Proc → Proc → Type ℓ
_≳′_ = [ ∞ ]_≳′_

private

  -- However, these definitions are definitionally equivalent to
  -- corresponding definitions in General.

  indirect-Expansion : Expansion ≡ General.Bisimilarity
  indirect-Expansion = refl

  indirect-Expansion′ : Expansion′ ≡ General.Bisimilarity′
  indirect-Expansion′ = refl

  indirect-[]≳ : [_]_≳_ ≡ General.[_]_∼_
  indirect-[]≳ = refl

  indirect-[]≳′ : [_]_≳′_ ≡ General.[_]_∼′_
  indirect-[]≳′ = refl

  indirect-≳ : _≳_ ≡ General._∼_
  indirect-≳ = refl

  indirect-≳′ : _≳′_ ≡ General._∼′_
  indirect-≳′ = refl

-- The converse relation.

infix 4 _≲_ _≲′_ [_]_≲_ [_]_≲′_

[_]_≲_ : Size → Proc → Proc → Type ℓ
[_]_≲_ i = flip [ i ]_≳_

[_]_≲′_ : Size → Proc → Proc → Type ℓ
[_]_≲′_ i = flip [ i ]_≳′_

_≲_ : Proc → Proc → Type ℓ
_≲_ = [ ∞ ]_≲_

_≲′_ : Proc → Proc → Type ℓ
_≲′_ = [ ∞ ]_≲′_

-- Combinators that can perhaps make the code a bit nicer to read.

infix -3 lr-result-⟶̂ rl-result-⇒ lr-result-⇒ rl-result-⟶̂

lr-result-⟶̂ : ∀ {i p′ q q′} μ → [ i ] p′ ≳′ q′ → q [ μ ]⟶̂ q′ →
              ∃ λ q′ → q [ μ ]⟶̂ q′ × [ i ] p′ ≳′ q′
lr-result-⟶̂ _ p′≳′q′ q⟶̂q′ = _ , q⟶̂q′ , p′≳′q′

rl-result-⇒ : ∀ {i p p′ q′} μ → p [ μ ]⇒ p′ → [ i ] p′ ≳′ q′ →
              ∃ λ p′ → p [ μ ]⇒ p′ × [ i ] p′ ≳′ q′
rl-result-⇒ _ p⇒p′ p′≳′q′ = _ , p⇒p′ , p′≳′q′

lr-result-⇒ : ∀ {i p′ q q′} μ → [ i ] p′ ≲′ q′ → q [ μ ]⇒ q′ →
              ∃ λ q′ → q [ μ ]⇒ q′ × [ i ] p′ ≲′ q′
lr-result-⇒ _ p′≲′q′ q⇒q′ = _ , q⇒q′ , p′≲′q′

rl-result-⟶̂ : ∀ {i p p′ q′} μ → p [ μ ]⟶̂ p′ → [ i ] p′ ≲′ q′ →
              ∃ λ p′ → p [ μ ]⟶̂ p′ × [ i ] p′ ≲′ q′
rl-result-⟶̂ _ p⟶̂p′ p′≲′q′ = _ , p⟶̂p′ , p′≲′q′

syntax lr-result-⟶̂ μ p′≳′q′ q⟶̂q′ = p′≳′q′ ⟵̂[ μ ] q⟶̂q′
syntax rl-result-⇒ μ p⇒p′ p′≳′q′ = p⇒p′ ⇒[ μ ] p′≳′q′
syntax lr-result-⇒ μ p′≲′q′ q⇒q′ = p′≲′q′ ⇐[ μ ] q⇒q′
syntax rl-result-⟶̂ μ p⟶̂p′ p′≲′q′ = p⟶̂p′ ⟶̂[ μ ] p′≲′q′

-- Strongly bisimilar processes are related by the expansion ordering.

mutual

  ∼⇒≳ : ∀ {i p q} → [ i ] p ∼ q → [ i ] p ≳ q
  ∼⇒≳ {i} = λ p∼q → StepC.⟨ lr p∼q , rl p∼q ⟩
    where
    lr : ∀ {p p′ q μ} →
         [ i ] p ∼ q → p [ μ ]⟶ p′ →
         ∃ λ q′ → q [ μ ]⟶̂ q′ × [ i ] p′ ≳′ q′
    lr p∼q p⟶p′ =
      let q′ , q⟶q′ , p′∼′q′ = SB.left-to-right p∼q p⟶p′
      in q′ , step q⟶q′ , ∼⇒≳′ p′∼′q′

    rl : ∀ {p q q′ μ} →
         [ i ] p ∼ q → q [ μ ]⟶ q′ →
         ∃ λ p′ → p [ μ ]⇒ p′ × [ i ] p′ ≳′ q′
    rl p∼q q⟶q′ =
      let p′ , p⟶p′ , p′∼′q′ = SB.right-to-left p∼q q⟶q′
      in p′ , ⟶→[]⇒ p⟶p′ , ∼⇒≳′ p′∼′q′

  ∼⇒≳′ : ∀ {i p q} → [ i ] p ∼′ q → [ i ] p ≳′ q
  force (∼⇒≳′ p∼′q) = ∼⇒≳ (SB.force p∼′q)

-- Expansion is a weak simulation (of three different kinds).

expansion-is-weak⇒ :
  ∀ {p p′ q} →
  p ≳ q → p ⇒ p′ →
  ∃ λ q′ → q ⇒ q′ × p′ ≳ q′
expansion-is-weak⇒ =
  is-weak⇒ StepC.left-to-right (λ p≳′q → force p≳′q) ⟶̂→⇒

expansion-is-weak[]⇒ :
  ∀ {p p′ q μ} →
  ¬ Silent μ →
  p ≳ q → p [ μ ]⇒ p′ →
  ∃ λ q′ → q [ μ ]⇒ q′ × p′ ≳ q′
expansion-is-weak[]⇒ ¬s =
  is-weak[]⇒ StepC.left-to-right (λ p≳′q → force p≳′q)
             ⟶̂→⇒ (⇒̂→[]⇒ ¬s ∘ ⟶̂→⇒̂)

expansion-is-weak⇒̂ :
  ∀ {p p′ q μ} →
  p ≳ q → p [ μ ]⇒̂ p′ →
  ∃ λ q′ → q [ μ ]⇒̂ q′ × p′ ≳ q′
expansion-is-weak⇒̂ =
  is-weak⇒̂ StepC.left-to-right (λ p≳′q → force p≳′q) ⟶̂→⇒ ⟶̂→⇒̂

-- The converse of expansion is a weak simulation (of three different
-- kinds).

converse-of-expansion-is-weak :
  ∀ {p p′ q} →
  p ≲ q → p ⇒ p′ →
  ∃ λ q′ → q ⇒ q′ × p′ ≲ q′
converse-of-expansion-is-weak =
  is-weak⇒ StepC.right-to-left (λ p≲′q → force p≲′q) []⇒→⇒

converse-of-expansion-is-weak[]⇒ :
  ∀ {p p′ q μ} →
  p ≲ q → p [ μ ]⇒ p′ →
  ∃ λ q′ → q [ μ ]⇒ q′ × p′ ≲ q′
converse-of-expansion-is-weak[]⇒ =
  is-weak[]⇒ StepC.right-to-left (λ p≲′q → force p≲′q) []⇒→⇒ id

converse-of-expansion-is-weak⇒̂ :
  ∀ {p p′ q μ} →
  p ≲ q → p [ μ ]⇒̂ p′ →
  ∃ λ q′ → q [ μ ]⇒̂ q′ × p′ ≲ q′
converse-of-expansion-is-weak⇒̂ =
  is-weak⇒̂ StepC.right-to-left (λ p≲′q → force p≲′q) []⇒→⇒ ⇒→⇒̂

mutual

  -- Expansion is transitive.
  --
  -- Note that the transitivity proof is not claimed to be fully
  -- size-preserving. For a proof showing that it cannot, in general,
  -- be size-preserving in the first argument, see
  -- Expansion.Delay-monad.size-preserving-transitivityˡ⇔uninhabited.

  transitive-≳ : ∀ {i p q r} → p ≳ q → [ i ] q ≳ r → [ i ] p ≳ r
  transitive-≳ {i} = λ p≳q q≳r → StepC.⟨ lr p≳q q≳r , rl p≳q q≳r ⟩
    where
    lr : ∀ {p p′ q r μ} →
         p ≳ q → [ i ] q ≳ r → p [ μ ]⟶ p′ →
         ∃ λ r′ → r [ μ ]⟶̂ r′ × [ i ] p′ ≳′ r′
    lr p≳q q≳r p⟶p′ with StepC.left-to-right p≳q p⟶p′
    ... | _  , done s , p′≳′q  =
      _ , done s
        , transitive-≳′ p′≳′q (record { force = λ { {_} → q≳r } })
    ... | q′ , step q⟶q′ , p′≳′q′ =
      let r′ , r⟶̂r′ , q′≳′r′ = StepC.left-to-right q≳r q⟶q′
      in r′ , r⟶̂r′ , transitive-≳′ p′≳′q′ q′≳′r′

    rl : ∀ {p q r r′ μ} →
         p ≳ q → [ i ] q ≳ r → r [ μ ]⟶ r′ →
         ∃ λ p′ → p [ μ ]⇒ p′ × [ i ] p′ ≳′ r′
    rl p≳q q≳r r⟶r′ =
      let q′ , q⇒q′ , q′≳′r′ = StepC.right-to-left q≳r r⟶r′
          p′ , p⇒̂p′ , p′≳q′  = converse-of-expansion-is-weak[]⇒ p≳q q⇒q′
      in p′ , p⇒̂p′ , transitive-≳′ (record { force = p′≳q′ }) q′≳′r′

  transitive-≳′ : ∀ {i p q r} → p ≳′ q → [ i ] q ≳′ r → [ i ] p ≳′ r
  force (transitive-≳′ p≳q q≳r) = transitive-≳ (force p≳q) (force q≳r)

-- The following variant of transitivity is fully size-preserving.

mutual

  transitive-≳∼ : ∀ {i p q r} →
                  [ i ] p ≳ q → [ i ] q ∼ r → [ i ] p ≳ r
  transitive-≳∼ {i} {p} {r = r} p≳q q∼r = StepC.⟨ lr , rl ⟩
    where
    rl : ∀ {r′ μ} → r [ μ ]⟶ r′ →
         ∃ λ p′ → p [ μ ]⇒ p′ × [ i ] p′ ≳′ r′
    rl r⟶r′ =
      let q′ , q⟶q′ , q′∼′r′ = SB.right-to-left q∼r r⟶r′
          p′ , p⇒p′ , p′≳′q′ = StepC.right-to-left p≳q q⟶q′
      in p′ , p⇒p′ , transitive-≳∼′ p′≳′q′ q′∼′r′

    lr : ∀ {p′ μ} → p [ μ ]⟶ p′ →
         ∃ λ r′ → r [ μ ]⟶̂ r′ × [ i ] p′ ≳′ r′
    lr p⟶p′ =
      let q′ , q⟶̂q′ , p′≳′q′ = StepC.left-to-right p≳q p⟶p′
          r′ , r⇒̂r′ , q′∼r′  = lemma q∼r q⟶̂q′
      in r′ , r⇒̂r′ , transitive-≳∼′ p′≳′q′ q′∼r′
      where
      lemma :
        ∀ {i p p′ q μ} →
        [ i ] p ∼ q → p [ μ ]⟶̂ p′ →
        ∃ λ q′ → q [ μ ]⟶̂ q′ × [ i ] p′ ∼′ q′
      lemma p∼q (done s)    = _ , done s
                                , record { force = λ { {_} → p∼q } }
      lemma p∼q (step p⟶p′) =
        let q′ , q⟶q′ , p′∼q′ = SB.left-to-right p∼q p⟶p′
        in q′ , ⟶→⟶̂ q⟶q′ , p′∼q′

  transitive-≳∼′ : ∀ {i p q r} →
                   [ i ] p ≳′ q → [ i ] q ∼′ r → [ i ] p ≳′ r
  force (transitive-≳∼′ p≳′q q∼′r) =
    transitive-≳∼ (force p≳′q) (SB.force q∼′r)

-- The following variant of transitivity is partially size-preserving.
--
-- For a proof showing that it cannot, in general, be size-preserving
-- in the first argument, see
-- Expansion.Delay-monad.size-preserving-transitivity-∼≳ˡ⇔uninhabited.

transitive-∼≳ : ∀ {i p q r} →
                p ∼ q → [ i ] q ≳ r → [ i ] p ≳ r
transitive-∼≳ = transitive-≳ ∘ ∼⇒≳

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

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

import      LibraBFT.Impl.OBM.Crypto              as Crypto
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.OBM.Util
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
import      Util.KVMap                            as Map
open import Util.PKCS                             hiding (verify)
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                           using (String)

module LibraBFT.Impl.Types.ValidatorVerifier where

------------------------------------------------------------------------------
calculateQuorumVotingPower : U64 -> U64
checkNumOfSignatures       : ValidatorVerifier → Map.KVMap AccountAddress Signature
                           → Either ErrLog Unit
checkVotingPower           : ValidatorVerifier → List AccountAddress → Either ErrLog Unit
getPublicKey               : ValidatorVerifier → AccountAddress → Maybe PK
getVotingPower             : ValidatorVerifier → AccountAddress → Maybe U64
sumVotingPower-ed-abs      : (List String → List String)
                           → Map.KVMap AccountAddress ValidatorConsensusInfo
                           → EitherD ErrLog U64
------------------------------------------------------------------------------

-- LBFT-OBM-DIFF : this is specific to OBM.
-- It enables specifying the number of faults allowed.
-- Assumes everyone has 1 vote
-- IMPL-DIFF : gets an alist instead of list of Author
initValidatorVerifier
  : U64 → List (Author × (SK × PK))
  → Either ErrLog ValidatorVerifier
initValidatorVerifier numFailures0 authors0 =
  checkBftAndRun numFailures0 authors0 f
 where
  f : U64 → List (Author × (SK × PK)) → ValidatorVerifier
  f numFailures authors =
    record -- ValidatorVerifier
    { _vvAddressToValidatorInfo = Map.fromList (fmap (λ (author , (_ , pk)) →
                                                       (author , ValidatorConsensusInfo∙new pk 1))
                                                    authors)
    ; _vvQuorumVotingPower      = numNodesNeededForNFailures numFailures ∸ numFailures
    ; _vvTotalVotingPower       = length authors }

new : Map.KVMap AccountAddress ValidatorConsensusInfo → EitherD ErrLog ValidatorVerifier
new addressToValidatorInfo = do
  totalVotingPower      ← sumVotingPower-ed-abs here' addressToValidatorInfo
  let quorumVotingPower = if Map.kvm-size addressToValidatorInfo == 0 then 0
                          else calculateQuorumVotingPower totalVotingPower
  pure (mkValidatorVerifier addressToValidatorInfo quorumVotingPower totalVotingPower)
 where
  here' : List String → List String
  here' t = "ValidatorVerifier" ∷ "new" ∷ t

-- This scales up the number of faults tolerated with the number of votes.
-- see TestValidatorVerifier in Haskell
calculateQuorumVotingPower totalVotingPower = (div (totalVotingPower * 2) 3) + 1

verifyIfAuthor
  : {V : Set} ⦃ _ : Crypto.CryptoHash V ⦄
  → {-Text →-} ValidatorVerifier → AccountAddress → V → Signature
  → Either ErrLog Unit
verifyIfAuthor {-msg-} self author v signature = case getPublicKey self author of λ where
  (just pk) → case Crypto.verify {-msg-} pk signature v of λ where
                (Left  e)    → Left fakeErr -- (ErrVerify e InvalidSignature)
                (Right unit) → Right unit
  nothing  → Left fakeErr -- Left (ErrVerify (msg:known) (UnknownAuthor (author^.aAuthorName)))
-- where
--  known = fmap _aAuthorName (Map.keys (self^.vvAddressToValidatorInfo))

verify
  : {V : Set} ⦃ _ : Crypto.CryptoHash V ⦄
  → ValidatorVerifier → AccountAddress → V → Signature
  → Either ErrLog Unit
verify = verifyIfAuthor -- (icSemi ["ValidatorVerifier", "verifySignature"])

verifyAggregatedStructSignature
  : {V : Set} ⦃ _ : Crypto.CryptoHash V ⦄
  → ValidatorVerifier → V → Map.KVMap AccountAddress Signature
  → Either ErrLog Unit
verifyAggregatedStructSignature self v aggregatedSignature = do
  checkNumOfSignatures self aggregatedSignature
  checkVotingPower self (Map.kvm-keys aggregatedSignature)
  forM_ (Map.kvm-toList aggregatedSignature) λ (author , signature) →
    verify self author v signature

batchVerifyAggregatedSignatures
  : {V : Set} ⦃ _ : Crypto.CryptoHash V ⦄
  → ValidatorVerifier → V → Map.KVMap AccountAddress Signature
  → Either ErrLog Unit
batchVerifyAggregatedSignatures = verifyAggregatedStructSignature

checkNumOfSignatures self aggregatedSignature =
  if-dec Map.kvm-size aggregatedSignature >? Map.kvm-size (self ^∙ vvAddressToValidatorInfo)
    then Left (ErrVerify
                 (TooManySignatures
                   (Map.kvm-size aggregatedSignature)
                   (Map.kvm-size (self ^∙ vvAddressToValidatorInfo))))
    else Right unit

checkVotingPower self authors = do
  let go : AccountAddress → U64 → Either ErrLog U64
      go a acc = case getVotingPower self a of λ where
         nothing  → Left (ErrVerify (UnknownAuthor (a ^∙ aAuthorName)))
         (just n) → Right (n + acc)
  aggregatedVotingPower ← foldrM go 0 authors
  if-dec aggregatedVotingPower <? self ^∙ vvQuorumVotingPower
    then Left (ErrVerify
               (TooLittleVotingPower aggregatedVotingPower (self ^∙ vvQuorumVotingPower)))
    else Right unit

getPublicKey self author =
  (_^∙ vciPublicKey)   <$> Map.lookup author (self ^∙ vvAddressToValidatorInfo)

getVotingPower self author =
  (_^∙ vciVotingPower) <$> Map.lookup author (self ^∙ vvAddressToValidatorInfo)

sumVotingPower : (List String → List String)
               → Map.KVMap AccountAddress ValidatorConsensusInfo
               → Either ErrLog U64
sumVotingPower here' addressToValidatorInfo =
  foldr go (Right 0) (Map.elems addressToValidatorInfo)
 where
  maxBoundU64 : U64
  maxBoundU64 = 18446744073709551615
  go : ValidatorConsensusInfo → Either ErrLog U64 → Either ErrLog U64
  go x (Right sum') =
    if-dec sum' ≤? maxBoundU64 ∸ (x ^∙ vciVotingPower)
    then Right (sum' + x ^∙ vciVotingPower)
    else Left fakeErr -- (ErrL (here' ("sum too big" ∷ [])))
  go _ (Left err) = Left err

abstract
  sumVotingPower-ed-abs f = fromEither ∘ sumVotingPower f

getOrderedAccountAddressesObmTODO : ValidatorVerifier → List AccountAddress
getOrderedAccountAddressesObmTODO self =
  -- TODO ORDER
  Map.kvm-keys (self ^∙ vvAddressToValidatorInfo)

from-ed : ValidatorSet → EitherD ErrLog ValidatorVerifier
from-ed validatorSet =
  new (foldl' go Map.empty (validatorSet ^∙ vsPayload))
 where
  go : Map.KVMap AccountAddress ValidatorConsensusInfo → ValidatorInfo
     → Map.KVMap AccountAddress ValidatorConsensusInfo
  go map0 validator =
    Map.insert (validator ^∙ viAccountAddress)
               (ValidatorConsensusInfo∙new
                 (validator ^∙ viConsensusPublicKey)
                 (validator ^∙ viConsensusVotingPower))
                map0

abstract
  from-e-abs = toEither ∘ from-ed
  from-ed-abs = from-ed

ext: agda


text:
module Alg where

open import Data.Bool
open import Data.Fin hiding (_+_ ; fold)
open import Data.List hiding (lookup ; [_] ; map)
open import Data.Nat
open import Data.Product hiding (map)
open import Data.Vec hiding (_++_)

open import Size

RankedAlphabet : ℕ → Set
RankedAlphabet = Vec ℕ

-- natural numbers = { zero_0, suc_1 }
rNat : RankedAlphabet 2
rNat = zero ∷ suc zero ∷ []

-- words over {t,f} = { eps_0, false_1, true_1 }
rBin : RankedAlphabet 3
rBin = zero ∷ suc zero ∷ suc zero ∷ []

-- binary trees = { leaf_0, branch_2 }
rBtr : RankedAlphabet 2
rBtr = zero ∷ suc (suc zero) ∷ []

module FailedAttempt where
  -- terms
  data Term {n} (ra : RankedAlphabet n) : Set where
    mk : (sym : Fin n) → (Fin (lookup ra sym) → Term ra) → Term ra

  tNat0 : Term rNat
  tNat0 = mk zero (λ ())

  tNat1 : Term rNat
  tNat1 = mk (suc zero) λ zero → tNat0

  tNat2 : Term rNat
  tNat2 = mk (suc zero) λ zero → tNat1

  -- interpretations
  nary : Set → ℕ → Set
  nary A zero = A
  nary A (suc n) = A → nary A n

  Algebra : ∀ {n} → RankedAlphabet n → Set → Set
  Algebra {n} ra A = (sym : Fin n) → nary A (lookup ra sym)

  -- I don't see how to implement this as a function
  postulate
    eval : ∀ {n} {ra : RankedAlphabet n} {A} → Term ra → Algebra ra A → A
-- end FailedAttempt

-- interpretations

nary : Set → ℕ → Set
nary A n = Vec A n → A

Algebra : ∀ {n} → RankedAlphabet n → Set → Set
Algebra {n} ra A = (sym : Fin n) → nary A (lookup ra sym)

-- natural numbers
aNat : Algebra rNat ℕ
aNat zero = λ [] → 0
aNat (suc zero) = λ{ (x ∷ []) → suc x }
aNat (suc (suc ()))

-- bitstrings
aBin : Algebra rBin (List Bool)
aBin zero = λ _ → []
aBin (suc zero) = λ x → false ∷ lookup x zero
aBin (suc (suc zero)) = λ x → true ∷ lookup x zero
aBin (suc (suc (suc ())))

-- compute value of bitstring
aBinVal : Algebra rBin ℕ
aBinVal zero = λ [] → 0
aBinVal (suc zero) = λ{ (x ∷ []) → x + x }
aBinVal (suc (suc zero)) = λ{ (x ∷ []) →  suc (x + x) }
aBinVal (suc (suc (suc ())))

-- the initial btree algebra
data BTree : Set where
  Leaf : BTree
  Branch : BTree → BTree → BTree

aBtrInitial : Algebra rBtr BTree
aBtrInitial zero = λ [] → Leaf
aBtrInitial (suc zero) = λ{ (l ∷ r ∷ []) → Branch l r }
aBtrInitial (suc (suc ()))

-- count leaves
aBtrCount : Algebra rBtr ℕ
aBtrCount zero = λ [] → 1
aBtrCount (suc zero) = λ{ (l ∷ r ∷ []) → l + r }
aBtrCount (suc (suc ()))

-- height
aBtrHeight : Algebra rBtr ℕ
aBtrHeight zero = λ [] → 0
aBtrHeight (suc zero) = λ{ (l ∷ r ∷ []) → suc (l ⊔ r) }
aBtrHeight (suc (suc ()))

-- terms (using sized types)
data Term {n} (ra : RankedAlphabet n) : {i : Size} → Set where
  mk : ∀ {i} → (sym : Fin n) → Vec (Term ra {i}) (lookup ra sym) → Term ra {↑ i}

eval : ∀ {n} {ra : RankedAlphabet n} {A} {i} → Algebra ra A → Term ra {i} → A
eval alg (mk sym subterms) = alg sym (map (eval alg) subterms)

tNat0 : Term rNat
tNat0 = mk zero []

tNat1 : Term rNat
tNat1 = mk (suc zero) [ tNat0 ]

tNat2 : Term rNat
tNat2 = mk (suc zero) [ tNat1 ]

aNatTerm : Algebra rNat (Term rNat)
aNatTerm = mk

----------------------------------------------------------------------
-- many-sorted algebra

open import Data.Unit
open import Data.Nat.GeneralisedArithmetic

Sorts = Fin

Signature : ℕ → ℕ → Set
Signature s = Vec (List (Sorts s) × Sorts s)

sNat : Signature 1 2
sNat = ([] , zero) ∷ (( zero ∷ []) , zero) ∷ []

sMon : Signature 2 6
sMon = ([] , zero) ∷ (zero ∷ [] , zero) ∷
       ([] , suc zero) ∷ (suc zero ∷ [] , suc zero) ∷ (suc zero ∷ [] , suc zero) ∷
       (zero ∷ suc zero ∷ [] , suc zero) ∷ []
-- this is:   0. S. eps. 0(). 1(). n*s.

sary : ∀ {s} → (Sorts s → Set) → List (Sorts s) → Set
sary int [] = ⊤
sary int (sort ∷ sort*) = int sort × sary int sort*

data STerm {s} {n} (sig : Signature s n) : Sorts s → Set where
  mk : (sym : Fin n) →
    let (sort* , sort) = lookup sig sym in
    sary (STerm sig) sort* →
    STerm sig sort

sNat0 : STerm sNat zero
sNat0 = mk zero tt

sNat1 : STerm sNat zero
sNat1 = mk (suc zero) (sNat0 , tt)

SAlgebra : ∀ {s n} → Signature s n → (Sorts s → Set) → Set
SAlgebra sig int = (sym : Fin _) →
    let (sort* , sort) = lookup sig sym in
    sary int sort* → int sort

asNat : SAlgebra sNat λ zero → ℕ
asNat zero = λ{ tt → 0 }
asNat (suc zero) = λ{ (x , tt) → suc x }
asNat (suc (suc ()))

asNatTerm : SAlgebra sNat (STerm sNat)
asNatTerm = mk
{- written out:
asNatTerm zero = mk zero
asNatTerm (suc zero) = mk (suc zero)
asNatTerm (suc (suc ()))
-}

asMon : SAlgebra sMon λ{ zero → ℕ ; (suc zero) → List Bool ; (suc (suc ())) }
asMon zero tt = 0
asMon (suc zero) (n , _) = suc n
asMon (suc (suc zero)) tt = []
asMon (suc (suc (suc zero))) (w , _) = true ∷ w
asMon (suc (suc (suc (suc zero)))) (w , _) = false ∷ w
asMon (suc (suc (suc (suc (suc zero))))) (n , w , _) = fold [] (_++_ w) n
asMon (suc (suc (suc (suc (suc (suc ())))))) x

max_stars_repo_name: proglang/ldlc

max_issues_repo_name: proglang/ldlc

max_forks_repo_name: proglang/ldlc


text:
{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.Core.Glue

open import Cubical.HITs.SetTruncation.Base

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

private
  variable
    ℓ : Level
    A : Type ℓ

-- lemma 6.9.1 in HoTT book
elimSetTrunc : {B : ∥ A ∥₀ → Type ℓ} →
               (Bset : (x : ∥ A ∥₀) → isSet (B x)) →
               (g : (a : A) → B (∣ a ∣₀)) →
               (x : ∥ A ∥₀) → B x
elimSetTrunc Bset g ∣ a ∣₀ = g a
elimSetTrunc {A = A} {B = B} Bset g (squash₀ x y p q i j) =
  isOfHLevel→isOfHLevelDep {n = 2} Bset  (elimSetTrunc Bset g x) (elimSetTrunc Bset g y)
    (cong (elimSetTrunc Bset g) p) (cong (elimSetTrunc Bset g) q) (squash₀ x y p q) i j

setTruncUniversal : {B : Type ℓ} → (isSet B) → (∥ A ∥₀ → B) ≃ (A → B)
setTruncUniversal Bset = isoToEquiv (iso intro elim leftInv rightInv)
  where
  intro = (λ h a → h ∣ a ∣₀)
  elim = elimSetTrunc (λ x → Bset)

  leftInv : ∀ g → intro (elim g) ≡ g
  leftInv g = refl

  rightInv : ∀ h → elim (intro h) ≡ h
  rightInv h i x = elimSetTrunc (λ x → isProp→isSet (Bset (elim (intro h) x) (h x)))
                                (λ a → refl) x i

elimSetTrunc2 : {B : ∥ A ∥₀ → ∥ A ∥₀ → Type ℓ}
                (Bset : ((x y : ∥ A ∥₀) → isSet (B x y)))
                (g : (a b : A) → B ∣ a ∣₀ ∣ b ∣₀)
                (x y : ∥ A ∥₀) → B x y
elimSetTrunc2 Bset g = elimSetTrunc (λ _ → hLevelPi 2 (λ _ → Bset _ _)) (λ a →
                       elimSetTrunc (λ _ → Bset _ _) (λ b → g a b))

elimSetTrunc3 : {B : (x y z : ∥ A ∥₀) → Type ℓ}
                (Bset : ((x y z : ∥ A ∥₀) → isSet (B x y z)))
                (g : (a b c : A) → B ∣ a ∣₀ ∣ b ∣₀ ∣ c ∣₀)
                (x y z : ∥ A ∥₀) → B x y z
elimSetTrunc3 Bset g = elimSetTrunc2 (λ _ _ → hLevelPi 2 λ _ → Bset _ _ _) (λ a b →
                       elimSetTrunc (λ _ → Bset _ _ _) (λ c → g a b c))

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
-- Andreas, 2020-06-21, issue #4769
-- Name and hiding ignored in subsequent face constraint patterns.
-- Instead, we should throw a warning.

open import Agda.Primitive.Cubical

data S : Set where
  base : S

foo : ∀ i j → Partial _ S
foo i j (i = i0) {{agdaDoesNotSeeThisName = (j = i1)}} = base

-- Expect: warning about name and "instance" flavor and argument.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
open import Prelude hiding (subst)

module Implicits.Substitutions.MetaType where

open import Implicits.Syntax.Type
open import Implicits.Syntax.MetaType

open import Data.Fin.Substitution
open import Data.Star as Star hiding (map)
open import Data.Star.Properties
open import Data.Nat.Properties.Simple
open import Data.Vec hiding ([_])

module MetaTypeTypeSubst where

  MetaSub : (ℕ → ℕ → Set) → ℕ → ℕ → ℕ → Set
  MetaSub T m ν μ = Sub (T m) ν μ

  record MetaLift (T : ℕ → ℕ → Set) : Set where
    field
      simple : ∀ {m} → Simple (T m)
      lift : ∀ {m ν} → T m ν → MetaType m ν

  module MetaTypeApp {T} (l : MetaLift T) where
    open MetaLift l

    infixl 8 _/_

    mutual
      _s/_ : ∀ {m μ ν} → MetaSimpleType m ν → MetaSub T m ν μ → MetaType m μ
      tvar x s/ σ = lift (lookup x σ)
      mvar x s/ σ = simpl (mvar x)
      (a →' b) s/ σ = simpl ((a / σ) →' (b / σ))
      tc c s/ σ = simpl (tc c)

      _/_ : ∀ {m μ ν} → MetaType m ν → MetaSub T m ν μ → MetaType m μ
      simpl x / σ = (x s/ σ)
      (a ⇒ b) / σ = (a / σ) ⇒ (b / σ)
      (∀' a)   / σ = ∀' (a / σ ↑)
        where
          open Simple simple

    module _ {m : ℕ} where
      open Application (record { _/_ = _/_ {m = m} }) public using (_/✶_)
      open Simple (simple {m})

      →'-/✶-↑✶ : ∀ k {n n' a b} (ρs : Subs (T m) n n') →
              (simpl (a →' b)) /✶ ρs ↑✶ k ≡ simpl ((a /✶ ρs ↑✶ k) →' (b /✶ ρs ↑✶ k))
      →'-/✶-↑✶ k ε        = refl
      →'-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (→'-/✶-↑✶ k ρs) refl

      ⇒-/✶-↑✶ : ∀ k {n n' a b} (ρs : Subs (T m) n n') →
              (a ⇒ b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) ⇒ (b /✶ ρs ↑✶ k)
      ⇒-/✶-↑✶ k ε        = refl
      ⇒-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (⇒-/✶-↑✶ k ρs) refl

      tc-/✶-↑✶ : ∀ k {c n n'} (ρs : Subs (T m) n n') →
              (simpl (tc c)) /✶ ρs ↑✶ k ≡ simpl (tc c)
      tc-/✶-↑✶ k ε        = refl
      tc-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tc-/✶-↑✶ k ρs) refl

      mvar-/✶-↑✶ : ∀ k {n n' c} (ρs : Subs (T m) n n') →
              (simpl (mvar c)) /✶ ρs ↑✶ k ≡ simpl (mvar c)
      mvar-/✶-↑✶ k ε        = refl
      mvar-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (mvar-/✶-↑✶ k ρs) refl

      ∀'-/✶-↑✶ : ∀ k {n n' a} (ρs : Subs (T m) n n') →
              (∀' a) /✶ ρs ↑✶ k ≡ ∀' (a /✶ ρs ↑✶ (suc k))
      ∀'-/✶-↑✶ k ε = refl
      ∀'-/✶-↑✶ k (x ◅ ρs) = cong₂ _/_ (∀'-/✶-↑✶ k ρs) refl

  Fin′ : ℕ → ℕ → Set
  Fin′ m ν = Fin ν

  module Lifted {m} {T} (lift : MetaLift T) where
    application : Application (MetaType m) (T m)
    application = record { _/_ = MetaTypeApp._/_ lift }

    open MetaLift lift public
    open Application application public
    open Simple (simple {m}) public

  varLift : MetaLift Fin′
  varLift = record {
      simple = record { var = Prelude.id ; weaken = suc }
      ; lift = (λ n → simpl (tvar n))
    }

  infixl 8 _/Var_

  _/Var_ : ∀ {m n k} → MetaType m n → Sub Fin n k → MetaType m k
  _/Var_ = MetaTypeApp._/_ varLift

  simple : ∀ {m} → Simple (MetaType m)
  simple = record { var = λ x → simpl (tvar x); weaken = λ x → x /Var VarSubst.wk }

  termLift : MetaLift MetaType
  termLift = record { simple = simple; lift = Prelude.id }

  private
    module ExpandSubst {n : ℕ} where
      app : Application (MetaType n) (MetaType n)
      app = record { _/_ = MetaTypeApp._/_ termLift }

      subst : Subst (MetaType n)
      subst = record
        { simple      = simple
        ; application = app
        }

      open Subst subst public

  open ExpandSubst public hiding (var; simple)

module MetaTypeMetaSubst where

  MetaSub : (ℕ → ℕ → Set) → ℕ → ℕ → ℕ → Set
  MetaSub T ν m m' = Sub (flip T ν) m m'

  record ExpandSimple (T : ℕ → ℕ → Set) : Set where
    field
      simple : ∀ {ν} → Simple (flip T ν)

    module _ {ν : ℕ} where
      open Simple (simple {ν}) public

  record ExpandApp (T : ℕ → ℕ → Set) : Set where
    field
      app : ∀ {ν} → Application (flip MetaType ν) (flip T ν)

    module _ {ν : ℕ} where
      open Application (app {ν}) public

  record MetaLift (T : ℕ → ℕ → Set) : Set where
    field
      exp-simple : ExpandSimple T
      lift : ∀ {m ν} → T m ν → MetaType m ν
      tpweaken : ∀ {m ν} → T m ν → T m (suc ν)

    open ExpandSimple exp-simple using (simple; _↑; weaken) renaming (var to evar)

    _↑tp : ∀ {m m' ν} → MetaSub T ν m m' → MetaSub T (suc ν) m m'
    _↑tp s = map tpweaken s

    field
      comm-weaken-tpweaken : ∀ {m ν} (a : T m ν) → weaken (tpweaken a) ≡ tpweaken (weaken a)
      tpweaken-var : ∀ {ν m} (n : Fin m) → (tpweaken {ν = ν} (evar n)) ≡ evar n

    _↑tp⋆_ : ∀ {m m' ν} → MetaSub T ν m m' → (k : ℕ) → MetaSub T (k + ν) m m'
    s ↑tp⋆ zero = s
    s ↑tp⋆ suc k = (s ↑tp⋆ k) ↑tp

  module MetaTypeApp {T} (l : MetaLift T) where
    open MetaLift l

    infixl 8 _/_

    mutual
      _s/_  : ∀ {m n ν} → MetaSimpleType m ν → MetaSub T ν m n → MetaType n ν
      tvar x s/ σ = simpl (tvar x)
      mvar x s/ σ = lift (lookup x σ)
      (a →' b) s/ σ = simpl ((a / σ) →' (b / σ))
      tc c s/ σ = simpl (tc c)

      _/_ : ∀ {m n ν} → MetaType m ν → MetaSub T ν m n → MetaType n ν
      simpl x / σ = (x s/ σ)
      (a ⇒ b) / σ = (a / σ) ⇒ (b / σ)
      (∀' a)   / σ = ∀' (a / σ ↑tp)

    open ExpandApp (record { app = record { _/_ = _/_ } }) hiding (_/_)
    open ExpandSimple exp-simple

  Fin′ : ℕ → ℕ → Set
  Fin′ m ν = Fin m

  module Lifted {T} (lift : MetaLift T) where
    open ExpandApp (record { app = record { _/_ = MetaTypeApp._/_ lift }}) public
    open MetaLift lift public
    open ExpandSimple exp-simple public

  module _ where
    private
      exp-simple : ExpandSimple Fin′
      exp-simple = record { simple = record { var = Prelude.id ; weaken = suc }}

    open ExpandSimple exp-simple

    varLift : MetaLift Fin′
    varLift = record {
        tpweaken = Prelude.id
        ; exp-simple = exp-simple
        ; lift = (λ n → simpl (mvar n))
        ; comm-weaken-tpweaken = λ s → refl
        ; tpweaken-var = λ n → refl }

  infixl 8 _/Var_

  _/Var_ : ∀ {m m' ν} → MetaType m ν → Sub Fin m m' → MetaType m' ν
  _/Var_ = MetaTypeApp._/_ varLift

  simple : ∀ {ν} → Simple (flip MetaType ν)
  simple = record { var = λ x → simpl (mvar x); weaken = λ x → x /Var VarSubst.wk }

  module _ where
    exp-simple : ExpandSimple MetaType
    exp-simple = record { simple = simple }

    open ExpandSimple exp-simple
    module MTTS = MetaTypeTypeSubst

    _↑⋆tp_ : ∀ {m m' ν} → MetaSub MetaType ν m m' → ∀ k → MetaSub MetaType (k + ν) m m'
    x ↑⋆tp zero = x
    x ↑⋆tp (suc k) = map MTTS.weaken (x ↑⋆tp k)

    _↑tp : ∀ {m m' ν} → MetaSub MetaType ν m m' → MetaSub MetaType (suc ν) m m'
    x ↑tp = x ↑⋆tp 1

    tp-weaken = MTTS.weaken

    comm-tp/var-/var : ∀ {ν ν' m m'} (a : MetaType m ν) {s : Sub Fin ν ν'} {s' : Sub Fin m m'} →
                       (a MTTS./Var s) /Var s' ≡ (a /Var s') MTTS./Var s
    comm-tp/var-/var (a ⇒ b) = cong₂ _⇒_ (comm-tp/var-/var a) (comm-tp/var-/var b)
    comm-tp/var-/var (∀' a) = cong ∀' (comm-tp/var-/var a)
    comm-tp/var-/var (simpl (tvar x)) = refl
    comm-tp/var-/var (simpl (mvar x)) = refl
    comm-tp/var-/var (simpl (a →' b)) = cong₂ (λ u v → simpl (u →' v)) (comm-tp/var-/var a)
                                          (comm-tp/var-/var b)
    comm-tp/var-/var (simpl (tc c)) = refl

    comm-weaken-tpweaken : ∀ {m ν} (a : MetaType m ν) → weaken (tp-weaken a) ≡ tp-weaken (weaken a)
    comm-weaken-tpweaken (a ⇒ b) = cong₂ _⇒_ (comm-weaken-tpweaken a) (comm-weaken-tpweaken b)
    comm-weaken-tpweaken (∀' a) = cong ∀' (comm-tp/var-/var a)
    comm-weaken-tpweaken (simpl (tvar x)) = refl
    comm-weaken-tpweaken (simpl (mvar x)) = refl
    comm-weaken-tpweaken (simpl (a →' b)) = cong₂ (λ u v → simpl (u →' v)) (comm-weaken-tpweaken a)
                                              (comm-weaken-tpweaken b)
    comm-weaken-tpweaken (simpl (tc c)) = refl

    open import Data.Vec.Properties

    termLift : MetaLift MetaType
    termLift = record {
        tpweaken = MetaTypeTypeSubst.weaken
        ; exp-simple = exp-simple
        ; lift = Prelude.id
        ; comm-weaken-tpweaken = comm-weaken-tpweaken
        ; tpweaken-var = λ n → refl}

  private
    module ExpandSubst {n : ℕ} where
      app : Application (flip MetaType n) (flip MetaType n)
      app = record { _/_ = MetaTypeApp._/_ termLift }

      subst : Subst (flip MetaType n)
      subst = record
        { simple      = simple
        ; application = app
        }

      open Subst subst public

  open ExpandSubst public hiding (var; simple)

  open-meta-k : ∀ {m ν} k → (a : MetaType m (k + suc ν)) → MetaType (suc m) (k + ν)
  open-meta-k {m} {ν} k a = (weaken a) MetaTypeTypeSubst./
      (MetaTypeTypeSubst.sub (simpl (mvar zero)) MetaTypeTypeSubst.↑⋆ k)

  open-meta : ∀ {m ν} → (a : MetaType m (suc ν)) → MetaType (suc m) ν
  open-meta a = open-meta-k zero a

  _◁m₁ : ∀ {ν m} (r : MetaType m ν) → ℕ
  _◁m₁ (a ⇒ b) = b ◁m₁
  _◁m₁ (∀' r) = 1 + r ◁m₁
  _◁m₁ (simpl x) = zero

  -- heads of metatypes
  _◁m : ∀ {ν m} (r : MetaType m ν) → (MetaType ((r ◁m₁) + m) ν)
  (a ⇒ b) ◁m = b ◁m
  ∀' r ◁m = open-meta (r ◁m)
  simpl x ◁m = simpl x

  smeta-weaken : ∀ {m ν} → MetaSimpleType m ν → MetaSimpleType (suc m) ν
  smeta-weaken (tc x) = tc x
  smeta-weaken (tvar n) = tvar n
  smeta-weaken (mvar m) = mvar (suc m)
  smeta-weaken (a →' b) = weaken a →' weaken b


text:
------------------------------------------------------------------------
-- Many properties which hold for _∼_ also hold for flip₁ _∼_
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Flip where

open import Data.Function
open import Data.Product

implies : ∀ {A} (≈ ∼ : Rel A) → ≈ ⇒ ∼ → flip₁ ≈ ⇒ flip₁ ∼
implies _ _ impl = impl

reflexive : ∀ {A} (∼ : Rel A) → Reflexive ∼ → Reflexive (flip₁ ∼)
reflexive _ refl = refl

irreflexive : ∀ {A} (≈ ∼ : Rel A) →
              Irreflexive ≈ ∼ → Irreflexive (flip₁ ≈) (flip₁ ∼)
irreflexive _ _ irrefl = irrefl

symmetric : ∀ {A} (∼ : Rel A) → Symmetric ∼ → Symmetric (flip₁ ∼)
symmetric _ sym = sym

transitive : ∀ {A} (∼ : Rel A) → Transitive ∼ → Transitive (flip₁ ∼)
transitive _ trans = flip trans

antisymmetric : ∀ {A} (≈ ≤ : Rel A) →
                Antisymmetric ≈ ≤ → Antisymmetric (flip₁ ≈) (flip₁ ≤)
antisymmetric _ _ antisym = antisym

asymmetric : ∀ {A} (< : Rel A) → Asymmetric < → Asymmetric (flip₁ <)
asymmetric _ asym = asym

respects : ∀ {A} (∼ : Rel A) P →
           Symmetric ∼ → P Respects ∼ → P Respects flip₁ ∼
respects _ _ sym resp ∼ = resp (sym ∼)

respects₂ : ∀ {A} (∼₁ ∼₂ : Rel A) →
            Symmetric ∼₂ → ∼₁ Respects₂ ∼₂ → flip₁ ∼₁ Respects₂ flip₁ ∼₂
respects₂ _ _ sym (resp₁ , resp₂) =
  ((λ {_} {_} {_} ∼ → resp₂ (sym ∼)) , λ {_} {_} {_} ∼ → resp₁ (sym ∼))

decidable : ∀ {A} (∼ : Rel A) → Decidable ∼ → Decidable (flip₁ ∼)
decidable _ dec x y = dec y x

total : ∀ {A} (∼ : Rel A) → Total ∼ → Total (flip₁ ∼)
total _ tot x y = tot y x

trichotomous : ∀ {A} (≈ < : Rel A) →
               Trichotomous ≈ < → Trichotomous (flip₁ ≈) (flip₁ <)
trichotomous _ _ compare x y = compare y x

isEquivalence : ∀ {A} {≈ : Rel A} →
                IsEquivalence ≈ → IsEquivalence (flip₁ ≈)
isEquivalence {≈ = ≈} eq = record
  { refl  = reflexive  ≈ Eq.refl
  ; sym   = symmetric  ≈ Eq.sym
  ; trans = transitive ≈ Eq.trans
  }
  where module Eq = IsEquivalence eq

setoid : Setoid → Setoid
setoid S = record
  { _≈_           = flip₁ S._≈_
  ; isEquivalence = isEquivalence S.isEquivalence
  } where module S = Setoid S

isPreorder : ∀ {A} {≈ ∼ : Rel A} →
             IsPreorder ≈ ∼ → IsPreorder (flip₁ ≈) (flip₁ ∼)
isPreorder {≈ = ≈} {∼} pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = implies ≈ ∼ Pre.reflexive
  ; trans         = transitive ∼ Pre.trans
  ; ∼-resp-≈      = respects₂ ∼ ≈ Pre.Eq.sym Pre.∼-resp-≈
  }
  where module Pre = IsPreorder pre

preorder : Preorder → Preorder
preorder P = record
  { _∼_        = flip₁ P._∼_
  ; _≈_        = flip₁ P._≈_
  ; isPreorder = isPreorder P.isPreorder
  } where module P = Preorder P

isDecEquivalence : ∀ {A} {≈ : Rel A} →
                   IsDecEquivalence ≈ → IsDecEquivalence (flip₁ ≈)
isDecEquivalence {≈ = ≈} dec = record
  { isEquivalence = isEquivalence Dec.isEquivalence
  ; _≟_           = decidable ≈ Dec._≟_
  }
  where module Dec = IsDecEquivalence dec

decSetoid : DecSetoid → DecSetoid
decSetoid S = record
  { _≈_              = flip₁ S._≈_
  ; isDecEquivalence = isDecEquivalence S.isDecEquivalence
  } where module S = DecSetoid S

isPartialOrder : ∀ {A} {≈ ≤ : Rel A} →
                 IsPartialOrder ≈ ≤ →
                 IsPartialOrder (flip₁ ≈) (flip₁ ≤)
isPartialOrder {≈ = ≈} {≤} po = record
  { isPreorder = isPreorder Po.isPreorder
  ; antisym    = antisymmetric ≈ ≤ Po.antisym
  }
  where module Po = IsPartialOrder po

poset : Poset → Poset
poset O = record
  { _≈_            = flip₁ O._≈_
  ; _≤_            = flip₁ O._≤_
  ; isPartialOrder = isPartialOrder O.isPartialOrder
  } where module O = Poset O

isStrictPartialOrder : ∀ {A} {≈ < : Rel A} →
                       IsStrictPartialOrder ≈ < →
                       IsStrictPartialOrder (flip₁ ≈) (flip₁ <)
isStrictPartialOrder {≈ = ≈} {<} spo = record
  { isEquivalence = isEquivalence Spo.isEquivalence
  ; irrefl        = irreflexive ≈ < Spo.irrefl
  ; trans         = transitive < Spo.trans
  ; <-resp-≈      = respects₂ < ≈ Spo.Eq.sym Spo.<-resp-≈
  }
  where module Spo = IsStrictPartialOrder spo

strictPartialOrder : StrictPartialOrder → StrictPartialOrder
strictPartialOrder O = record
  { _≈_                  = flip₁ O._≈_
  ; _<_                  = flip₁ O._<_
  ; isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
  } where module O = StrictPartialOrder O

isTotalOrder : ∀ {A} {≈ ≤ : Rel A} →
               IsTotalOrder ≈ ≤ →
               IsTotalOrder (flip₁ ≈) (flip₁ ≤)
isTotalOrder {≈ = ≈} {≤} to = record
  { isPartialOrder = isPartialOrder To.isPartialOrder
  ; total          = total ≤ To.total
  }
  where module To = IsTotalOrder to

totalOrder : TotalOrder → TotalOrder
totalOrder O = record
  { _≈_          = flip₁ O._≈_
  ; _≤_          = flip₁ O._≤_
  ; isTotalOrder = isTotalOrder O.isTotalOrder
  } where module O = TotalOrder O

isDecTotalOrder : ∀ {A} {≈ ≤ : Rel A} →
                  IsDecTotalOrder ≈ ≤ →
                  IsDecTotalOrder (flip₁ ≈) (flip₁ ≤)
isDecTotalOrder {≈ = ≈} {≤} dec = record
  { isTotalOrder = isTotalOrder Dec.isTotalOrder
  ; _≟_          = decidable ≈ Dec._≟_
  ; _≤?_         = decidable ≤ Dec._≤?_
  }
  where module Dec = IsDecTotalOrder dec

decTotalOrder : DecTotalOrder → DecTotalOrder
decTotalOrder O = record
  { _≈_             = flip₁ O._≈_
  ; _≤_             = flip₁ O._≤_
  ; isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
  } where module O = DecTotalOrder O

isStrictTotalOrder : ∀ {A} {≈ < : Rel A} →
                     IsStrictTotalOrder ≈ < →
                       IsStrictTotalOrder (flip₁ ≈) (flip₁ <)
isStrictTotalOrder {≈ = ≈} {<} sto = record
  { isEquivalence = isEquivalence Sto.isEquivalence
  ; trans         = transitive < Sto.trans
  ; compare       = trichotomous ≈ < Sto.compare
  ; <-resp-≈      = respects₂ < ≈ Sto.Eq.sym Sto.<-resp-≈
  }
  where module Sto = IsStrictTotalOrder sto

strictTotalOrder : StrictTotalOrder → StrictTotalOrder
strictTotalOrder O = record
  { _≈_                = flip₁ O._≈_
  ; _<_                = flip₁ O._<_
  ; isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
  } where module O = StrictTotalOrder O

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module spaceShipCell where

open import Unit
open import Data.List.Base hiding ([])
open import Data.Bool.Base
open import Data.Integer
open import Data.Product hiding (map)
open import NativeIO

open import SizedIO.Object
open import SizedIO.IOObject
open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.WxGraphicsLib
open import StateSized.GUI.ShipBitMap
open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent
open import StateSizedIO.GUI.VariableList
open import Sized.SimpleCell hiding (main; program)

VarType  = Object (cellI ℤ)

cellℤC : (z : ℤ ) → VarType
objectMethod (cellℤC z) get       = (  z  ,  cellℤC z   )
objectMethod (cellℤC z) (put z')  = (  _  ,  cellℤC z'  )

varInit : VarType
varInit = cellℤC (+ 150)

onPaint : ∀{i} → VarType → DC → Rect → IO GuiLev1Interface i VarType
onPaint c dc rect =
  let (z , c₁) = objectMethod c get                in
  do  (drawBitmap dc ship (z , (+ 150)) true)  λ _ →
  return c₁

moveSpaceShip  : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType
moveSpaceShip fra c =
  let  (z  ,  c₁)  =  objectMethod c   get
       (_  ,  c₂)  =  objectMethod c₁  (put (z + + 20))
  in   return c₂

callRepaint    : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType
callRepaint fra c = do (repaint fra) λ _ →  return c

buttonHandler : ∀{i} → Frame → List (VarType  → IO GuiLev1Interface i VarType)
buttonHandler fra = moveSpaceShip fra ∷ [ callRepaint fra ]

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  doˢ (level1C makeFrame)           λ fra →
           doˢ (level1C (makeButton fra))    λ bt →
           doˢ (level1C (addButton fra bt))  λ _ →
           doˢ (createVar varInit)           λ _ →
           doˢ (setButtonHandler bt (buttonHandler fra)) λ _ →
           doˢ (setOnPaint       fra [ onPaint  ])
           returnˢ

main : NativeIO Unit
main = start (translateLev2 program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module FFI where

open import Common.Prelude

_+'_ : Nat → Nat → Nat
zero +' y = y
suc x +' y = suc (x +' y)
{-# COMPILE GHC _+'_ = (+) :: Integer -> Integer -> Integer #-}

-- on-purpose buggy haskell implementation!
_+''_ : Nat → Nat → Nat
zero +'' y = y
suc x +'' y = suc (x +'' y)
{-# COMPILE GHC _+''_ = (-) :: Integer -> Integer -> Integer #-}

open import Common.IO
open import Common.Unit

main : IO Unit
main = printNat (10 +' 5) ,,
  printNat (30 +'' 7)

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
module Spire.IDarkwingDuck.Primitive where

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

infixr 4 _,_
infixr 5 _∷_

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

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

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

data ⊥ : Set where

elimBot : (P : ⊥ → Set)
  (v : ⊥) → P v
elimBot P ()

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

data ⊤ : Set where
  tt : ⊤

elimUnit : (P : ⊤ → Set)
  (ptt : P tt)
  (u : ⊤) → P u
elimUnit P ptt tt = ptt

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

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

elimPair : {A : Set} {B : A → Set}
  (P : Σ A B → Set)
  (ppair : (a : A) (b : B a) → P (a , b))
  (ab : Σ A B) → P ab
elimPair P ppair (a , b) = ppair a b

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

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

elimEq : {A : Set} {x : A} (P : (y : A) → x ≡ y → Set)
  (prefl : P x refl)
  (y : A) (q : x ≡ y) → P y q
elimEq P prefl x refl = prefl

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

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

elimList : {A : Set} (P : List A → Set)
  (pnil : P [])
  (pcons : (x : A) (xs : List A) → P xs → P (x ∷ xs))
  (xs : List A) → P xs
elimList P pnil pcons [] = pnil
elimList P pnil pcons (x ∷ xs) = pcons x xs (elimList P pnil pcons xs)

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

data PointsTo (A : Set) : List A → Set where
  here : ∀{x xs} → PointsTo A (x ∷ xs)
  there : ∀{x xs} → PointsTo A xs → PointsTo A (x ∷ xs)

elimPointsTo : {A : Set} (P : (xs : List A) → PointsTo A xs → Set)
  (phere : (x : A) (xs : List A) → P (x ∷ xs) here)
  (pthere : (x : A) (xs : List A) (t : PointsTo A xs) → P xs t → P (x ∷ xs) (there t))
  (xs : List A) (t : PointsTo A xs) → P xs t
elimPointsTo P phere pthere (x ∷ xs) here = phere x xs
elimPointsTo P phere pthere (x ∷ xs) (there t) = pthere x xs t (elimPointsTo P phere pthere xs t)

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

data Tel : Set₁ where
  End : Tel
  Arg IArg : (A : Set) (B : A → Tel) → Tel

elimTel : (P : Tel → Set)
  (pend : P End)
  (parg  : (A : Set) (B : A → Tel) (pb : (a : A) → P (B a)) → P (Arg A B))
  (piarg : (A : Set) (B : A → Tel) (pb : (a : A) → P (B a)) → P (IArg A B))
  (T : Tel) → P T
elimTel P pend parg piarg End = pend
elimTel P pend parg piarg (Arg A B) = parg A B (λ a → elimTel P pend parg piarg (B a))
elimTel P pend parg piarg (IArg A B) = piarg A B (λ a → elimTel P pend parg piarg (B a))

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

data Desc (I : Set) : Set₁ where
  End : (i : I) → Desc I
  Rec : (i : I) (D : Desc I) → Desc I
  Arg : (A : Set) (B : A → Desc I) → Desc I
  IArg : (A : Set) (B : A → Desc I) → Desc I

elimDesc : {I : Set} (P : Desc I → Set)
  (pend : (i : I) → P (End i))
  (prec  : (i : I) (D : Desc I) (pd : P D) → P (Rec i D))
  (parg : (A : Set) (B : A → Desc I) (pb : (a : A) → P (B a)) → P (Arg A B))
  (piarg : (A : Set) (B : A → Desc I) (pb : (a : A) → P (B a)) → P (IArg A B))
  (D : Desc I) → P D
elimDesc P pend prec parg piarg (End i) = pend i
elimDesc P pend prec parg piarg (Rec i D) = prec i D (elimDesc P pend prec parg piarg D)
elimDesc P pend prec parg piarg (Arg A B) = parg A B (λ a → elimDesc P pend prec parg piarg (B a))
elimDesc P pend prec parg piarg (IArg A B) = piarg A B (λ a → elimDesc P pend prec parg piarg (B a))

Elᴰ : {I : Set} (D : Desc I) → (I → Set) → I → Set
Elᴰ (End j) X i = j ≡ i
Elᴰ (Rec j D)  X i = Σ (X j) (λ _ → Elᴰ D X i)
Elᴰ (Arg A B)  X i = Σ A (λ a → Elᴰ (B a) X i)
Elᴰ (IArg A B) X i = Σ A (λ a → Elᴰ (B a) X i)

Hyps : {I : Set} (D : Desc I) (X : I → Set) (P : (i : I) → X i → Set) (i : I) (xs : Elᴰ D X i) → Set
Hyps (End j) X P i q = ⊤
Hyps (Rec j D)  X P i (x , xs) = Σ (P j x) (λ _ → Hyps D X P i xs)
Hyps (Arg A B)  X P i (a , b) = Hyps (B a) X P i b
Hyps (IArg A B) X P i (a , b) = Hyps (B a) X P i b

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

data μ {I : Set} (D : Desc I) (i : I) : Set where
  init : Elᴰ D (μ D) i → μ D i

ind : {I : Set} (D : Desc I)
  (M : (i : I) → μ D i → Set)
  (α : ∀ i (xs : Elᴰ D (μ D) i) (ihs : Hyps D (μ D) M i xs) → M i (init xs))
  (i : I)
  (x : μ D i)
  → M i x

prove : {I : Set} (D E : Desc I)
  (M : (i : I) → μ E i → Set)
  (α : ∀ i (xs : Elᴰ E (μ E) i) (ihs : Hyps E (μ E) M i xs) → M i (init xs))
  (i : I) (xs : Elᴰ D (μ E) i) → Hyps D (μ E) M i xs

ind D M α i (init xs) = α i xs (prove D D M α i xs)

prove (End j) E M α i q = tt
prove (Rec j D)  E M α i (x , xs) = ind E M α j x , prove D E M α i xs
prove (Arg A B)  E M α i (a , xs) = prove (B a) E M α i xs
prove (IArg A B) E M α i (a , xs) = prove (B a) E M α i xs

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

A rewrite B : Set

max_forks_repo_name: Agda-zh/agda


text:
module Category where

open import Function hiding (_∘_; id)
open import Level
open import Data.Product
open import Relation.Binary
open import Relation.Binary.Core using (_≡_)
open Setoid renaming (_≈_ to eqSetoid)

open import Basic

record Category (C₀ C₁ ℓ : Level) : Set (suc (C₀ ⊔ C₁ ⊔ ℓ)) where
  field
    Obj : Set C₀
    Homsetoid : Obj → Obj → Setoid C₁ ℓ

  Hom : Obj → Obj → Set C₁
  Hom A B = Carrier (Homsetoid A B)

  equal : {A B : Obj} → Hom A B → Hom A B → Set ℓ
  equal {A} {B} f g = eqSetoid (Homsetoid A B) f g

  field
    comp : {A B C : Obj} → Hom B C → Hom A B → Hom A C
    id : {A : Obj} → Hom A A

  field
    leftId : {A B : Obj} {f : Hom A B} → equal (comp id f) f
    rightId : {A B : Obj} {f : Hom A B} → equal (comp f id) f
    assoc : {A B C D : Obj} {f : Hom A B} {g : Hom B C} {h : Hom C D}
      → equal (comp (comp h g) f) (comp h (comp g f))
    ≈-composite : {A B C : Obj} {f g : Hom B C} {h i : Hom A B}
      → equal f g → equal h i → equal (comp f h) (comp g i)

  dom : {A B : Obj} → Hom A B → Obj
  dom {A} _ = A

  cod : {A B : Obj} → Hom A B → Obj
  cod {B} _ = B

  op : Category C₀ C₁ ℓ
  op = record
    { Obj = Obj
    ; Homsetoid = flip Homsetoid
    ; comp = flip comp
    ; id = id

    ; leftId = rightId
    ; rightId = leftId
    ; assoc = λ{A B C D} → IsEquivalence.sym (isEquivalence (Homsetoid D A)) assoc
    ; ≈-composite = flip ≈-composite
    }

open Category

infixr 9 _∘_
infixr 7 _[_∘_]
infixr 2 _≈_
infixr 2 _[_≈_]
infix 4 _[_≅_]

_[_∘_] : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
C [ f ∘ g ] = comp C f g

_∘_ : ∀{C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
_∘_ {C = C} = _[_∘_] C

_[_≈_] : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} → Rel (Hom C A B) ℓ
C [ f ≈ g ] = equal C f g

_≈_ : ∀{C₀ C₁ ℓ} {C : Category C₀ C₁ ℓ} {A B : Obj C} → Rel (Hom C A B) ℓ
_≈_ {C = C} = equal C

equiv : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} → IsEquivalence (eqSetoid (Homsetoid C A B))
equiv C {A} {B} = isEquivalence (Homsetoid C A B)

refl-hom : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} {f : Hom C A B} → C [ f ≈ f ]
refl-hom C = IsEquivalence.refl (equiv C)

sym-hom : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → C [ g ≈ f ]
sym-hom C = IsEquivalence.sym (equiv C)

trans-hom : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {A B : Obj C} {f g h : Hom C A B} → C [ f ≈ g ] → C [ g ≈ h ] → C [ f ≈ h ]
trans-hom C = IsEquivalence.trans (equiv C)

record _[_≅_] {C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) (a b : Obj C) : Set (C₀ ⊔ C₁ ⊔ ℓ) where
  field
    map-→ : Hom C a b
    map-← : Hom C b a
    proof : (C [ C [ map-→ ∘ map-← ] ≈ id C ]) × (C [ C [ map-← ∘ map-→ ] ≈ id C ])

record isomorphism {C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {a b : Obj C} (f : Hom C a b) : Set (C₀ ⊔ C₁ ⊔ ℓ) where
  field
    inverse-map : Hom C b a
    proof : (C [ C [ f ∘ inverse-map ] ≈ id C ]) × (C [ C [ inverse-map ∘ f ] ≈ id C ])

iso-≅ : ∀ {C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) {a b : Obj C} {f : Hom C a b} → isomorphism C f → C [ a ≅ b ]
iso-≅ C {f = f} iso = record {
  map-→ = f ;
  map-← = isomorphism.inverse-map iso ;
  proof = isomorphism.proof iso }

Setoids : {c₀ ℓ : Level} → Category (suc (c₀ ⊔ ℓ)) (suc (c₀ ⊔ ℓ)) (c₀ ⊔ ℓ)
Setoids {c₀} {ℓ} = record {
  Obj = Setoid c₀ ℓ;
  Homsetoid = λ A B → record { Carrier = Map.Map A B; _≈_ = Map.equality; isEquivalence = Map-Equal-Equiv A B };
  comp = Map.compose;
  id = Map.identity;
  leftId = λ {_ B} _ → refl B;
  rightId = λ {_ B} _ → refl B;
  assoc = λ {_ _ _ D} x → refl D;
  ≈-composite = λ {_ _ C f g h} x x₁ x₂ → trans C (x (Map.Map.mapping h x₂)) (Map.Map.preserveEq g (x₁ x₂)) }
  where
    Map-Equal-Equiv : (A B : Setoid _ _) → IsEquivalence Map.equality
    Map-Equal-Equiv A B = record { refl = λ _ → refl B ; sym = λ x x₁ → sym B (x x₁) ; trans = λ x x₁ x₂ → trans B (x x₂) (x₁ x₂) }

module CategoryReasoning where
  infix 1 begin⟨_⟩_
  infixr 2 _≈⟨_⟩_ _≡⟨_⟩_
  infix 3 _∎

  data IsRelatedTo[_] {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) (a b : Obj C) (x y : Hom C a b) : Set ℓ where
    relTo : C [ x ≈ y ] → IsRelatedTo[ C ] a b x y

  begin⟨_⟩_ : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) → {A B : Obj C} {f g : Hom C A B} → IsRelatedTo[ C ] A B f g → equal C f g
  begin⟨_⟩_ C {A} {B} (relTo x≈y) = x≈y

  _∎ : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} {A B : Obj C} (f : Hom C A B) → IsRelatedTo[ C ] A B f f
  _∎ {C = C} f = relTo (refl-hom C)

  _≈⟨_⟩_ : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} → {A B : Obj C} (f : Hom C A B) → {g h : Hom C A B} → equal C f g → IsRelatedTo[ C ] A B g h → IsRelatedTo[ C ] A B f h
  _≈⟨_⟩_ {C = C} f f≈g (relTo g≈h) = relTo (trans-hom C f≈g g≈h)

  _≡⟨_⟩_ : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} → {A B : Obj C} (f : Hom C A B) → {g h : Hom C A B} → f ≡ g → IsRelatedTo[ C ] A B g h → IsRelatedTo[ C ] A B f h
  _≡⟨_⟩_ {C = C} f _≡_.refl (relTo g≈h) = relTo g≈h

open CategoryReasoning public

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
module Cats.Util.Simp where

open import Data.List using (List ; [] ; _∷_)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Product using (_×_ ; _,_ ; ∃-syntax)
open import Data.Unit using (⊤)
open import Function using () renaming (_∘_ to _⊚_)
open import Level using (_⊔_) renaming (zero to lzero)
open import Relation.Binary.PropositionalEquality as ≡ using
  (_≡_ ; inspect ; [_])

open import Cats.Category.Base
open import Cats.Util.Reflection

_>>=_ = bindTC
return = returnTC

_>>_ : ∀ {a} {A : Set a} {b} {B : Set b} → TC A → TC B → TC B
ma >> mb = ma >>= λ _ → mb

module _ {lo la l≈} (C : Category lo la l≈) where

  infixr 9 _∘_

  private
    module C = Category C
    module ≈ = C.≈
    open C.≈-Reasoning

  data Tm : C.Obj → C.Obj → Set (lo ⊔ la) where
    var : ∀ {A B} → A C.⇒ B → Tm A B
    id : ∀ {A} → Tm A A
    _∘_ : ∀ {A B C} → Tm B C → Tm A B → Tm A C

  ⟦_⟧ : ∀ {A B} → Tm A B → A C.⇒ B
  ⟦ var f ⟧ = f
  ⟦ id ⟧ = C.id
  ⟦ f ∘ g ⟧ = ⟦ f ⟧ C.∘ ⟦ g ⟧

  Method : Set (lo ⊔ la)
  Method = ∀ {A B} → Tm A B → Tm A B

  Correct : Method → Set (lo ⊔ la ⊔ l≈)
  Correct f = ∀ {A B} (t : Tm A B) → ⟦ t ⟧ C.≈ ⟦ f t ⟧

  Correct→Injective : (f : Method) → Correct f → ∀ {A B} (t u : Tm A B)
    → ⟦ f t ⟧ C.≈ ⟦ f u ⟧
    → ⟦ t ⟧ C.≈ ⟦ u ⟧
  Correct→Injective f fcor t u eq
      = ≈.trans (fcor t) (≈.trans eq (≈.sym (fcor u)))

  ⊚-correct : (f g : Method) → Correct f → Correct g → Correct (f ⊚ g)
  ⊚-correct _ _ fcor gcor t = ≈.trans (gcor _) (fcor _)

  {-# TERMINATING #-}
  reassoc : Method
  reassoc (var f) = var f
  reassoc id = id
  reassoc (var f ∘ g) = var f ∘ reassoc g
  reassoc (id ∘ g) = id ∘ reassoc g
  reassoc ((f ∘ g) ∘ h) = reassoc (f ∘ g ∘ h)

  {-# TERMINATING #-}
  reassoc-correct : Correct reassoc
  reassoc-correct (var f) = C.≈.refl
  reassoc-correct id = C.≈.refl
  reassoc-correct (var f ∘ g) = C.∘-resp-r (reassoc-correct g)
  reassoc-correct (id ∘ f) = C.∘-resp-r (reassoc-correct f)
  reassoc-correct ((f ∘ g) ∘ h) = ≈.trans C.assoc (reassoc-correct (f ∘ g ∘ h))

  simpId : Method
  simpId (var x) = var x
  simpId id = id
  simpId (f ∘ g) with simpId f | simpId g
  ... | var f′  | var g′  = var f′ ∘ var g′
  ... | var f′  | id      = var f′
  ... | var f′  | g′ ∘ g″ = var f′ ∘ g′ ∘ g″
  ... | id      | g′      = g′
  ... | f′ ∘ f″ | var g′  = f′ ∘ f″ ∘ var g′
  ... | f′ ∘ f″ | id      = f′ ∘ f″
  ... | f′ ∘ f″ | g′ ∘ g″ = f′ ∘ f″ ∘ g′ ∘ g″

  simpId-correct : Correct simpId

  simpId-≡ : ∀ {A B} t {u : Tm A B} → simpId t ≡ u → ⟦ t ⟧ C.≈ ⟦ u ⟧

  simpId-correct (var x) = C.≈.refl
  simpId-correct id = C.≈.refl
  simpId-correct (f ∘ g)
    with simpId f | inspect simpId f | simpId g | inspect simpId g
  ... | var f′ | [ eq-f ] | var g′  | [ eq-g ]
      = C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)
  ... | var f′ | [ eq-f ] | id      | [ eq-g ]
      = ≈.trans (C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)) C.id-r
  ... | var f′ | [ eq-f ] | g′ ∘ g″ | [ eq-g ]
      = C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)
  ... | id | [ eq-f ] | g' | [ eq-g ]
      = ≈.trans (C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)) C.id-l
  ... | f′ ∘ f″ | [ eq-f ] | var x   | [ eq-g ]
      = ≈.trans (C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)) C.assoc
  ... | f′ ∘ f″ | [ eq-f ] | id      | [ eq-g ]
      = ≈.trans (C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)) C.id-r
  ... | f′ ∘ f″ | [ eq-f ] | g′ ∘ g″ | [ eq-g ]
      = ≈.trans (C.∘-resp (simpId-≡ f eq-f) (simpId-≡ g eq-g)) C.assoc

  simpId-≡ t eq
      = ≈.trans (simpId-correct t) (≈.reflexive (≡.cong ⟦_⟧ eq))

  simp : Method
  simp = reassoc ⊚ simpId

  simp-correct : Correct simp
  simp-correct
      = ⊚-correct reassoc simpId reassoc-correct simpId-correct

  simp-injective : ∀ {A B} (t u : Tm A B)
    → ⟦ simp t ⟧ C.≈ ⟦ simp u ⟧
    → ⟦ t ⟧ C.≈ ⟦ u ⟧
  simp-injective = Correct→Injective simp simp-correct

  simp-injective′ : ∀ {A B} (t u : Tm A B)
    → simp t ≡ simp u
    → ⟦ t ⟧ C.≈ ⟦ u ⟧
  simp-injective′ t u eq = simp-injective t u (≈.reflexive (≡.cong ⟦_⟧ eq))

reify : Term → Term
reify (def (quote Category.id)
  (argH _ ∷ argH _ ∷ argH _ ∷ argD C ∷ argH _ ∷ []))
    = con (quote id) []
reify (def (quote Category._∘_)
  (argH _ ∷ argH _ ∷ argH _ ∷ argD C ∷ argH _ ∷ argH _ ∷ argH _ ∷ argD f ∷ argD g ∷ []))
    = con (quote _∘_) (argD (reify f) ∷ argD (reify g) ∷ [])
reify t = con (quote Tm.var) (argD t ∷ [])

matchGoal : Term → TC (Term × Term)
matchGoal (def (quote Category._≈_)
  (argH _ ∷ argH _ ∷ argH _ ∷ argD C ∷ argH A ∷ argH B ∷ argD f ∷ argD g ∷ []))
    = return (reify f , reify g)
matchGoal _ = typeError (strErr "matchGoal: not an equality" ∷ [])

macro
  simp! : ∀ {lo la l≈} → Category lo la l≈ → Term → TC ⊤
  simp! C hole = do
      goal ← inferType hole
      blockOnAnyMeta goal
      (lhs , rhs) ← matchGoal goal
      C′ ← quoteTC C
      let solution
            = def (quote simp-injective′)
            ( argD C′
            ∷ argD lhs
            ∷ argD rhs
            ∷ argD (con (quote ≡.refl) [])
            ∷ [])
      unify hole solution

module Test {lo la l≈} {C : Category lo la l≈} (let module C = Category C) {A B C′ D} {f : C′ C.⇒ D} {g : B C.⇒ C′} {h : A C.⇒ B} where

  test : ((C.id C.∘ f) C.∘ g) C.∘ h C.≈ C.id C.∘ f C.∘ g C.∘ h
  test = simp! C

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-

This file contains:

- The first Eilenberg–Mac Lane type as a HIT

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.EilenbergMacLane1.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
  renaming (assoc to assoc∙)
open import Cubical.Algebra.Group.Base

private
  variable ℓ : Level

module _ (Group@(G , str) : Group ℓ) where
  open GroupStr str

  data EM₁ : Type ℓ where
    embase : EM₁
    emloop : G → embase ≡ embase
    emcomp : (g h : G)
           → PathP (λ j → embase ≡ emloop h j) (emloop g) (emloop (g · h))
    emsquash : ∀ (x y : EM₁) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s

  {- The emcomp constructor fills the square:
^
    emloop (g · h)
    [a]— — — >[c]
     ‖         ^
     ‖         | emloop h     ^
     ‖         |            j |
    [a]— — — >[b]          ∙ — >
       emloop g                i

    We use this to give another constructor-like construction:
  -}

  emloop-comp : (g h : G) → emloop (g · h) ≡ emloop g ∙ emloop h
  emloop-comp g h i = compPath-unique refl (emloop g) (emloop h)
    (emloop (g · h) , emcomp g h)
    (emloop g ∙ emloop h , compPath-filler (emloop g) (emloop h)) i .fst

  emloop-1g : emloop 1g ≡ refl
  emloop-1g =
       lUnit (emloop 1g)
    ∙∙ cong (_∙ emloop 1g) (sym (lCancel (emloop 1g)) )
    ∙∙ sym (assoc∙ _ _ _)
    ∙∙ cong (sym (emloop 1g) ∙_) (sym (emloop-comp 1g 1g) ∙ cong emloop (·IdL 1g))
    ∙∙ rCancel _

  emloop-sym : (g : G) → emloop (inv g) ≡ sym (emloop g)
  emloop-sym g =
       rUnit _
    ∙∙ cong (emloop (inv g) ∙_) (sym (rCancel (emloop g)))
    ∙∙ assoc∙ _ _ _
    ∙∙ cong (_∙ sym (emloop g)) (sym (emloop-comp (inv g) g) ∙∙ cong emloop (·InvL g) ∙∙ emloop-1g)
    ∙∙ sym (lUnit _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2

open import lib.types.PathSeq

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim

module nicolai.pseudotruncations.wconst-preparation where

{- first, we show that a weakly constant sequence for
   which we have an a₀ : A₀ is contractible.
   We proceed step-wise. -}
module wconst-init {i} {C : Sequence {i}} (wc : wconst-chain C) (a₀ : fst C O) where

  A = fst C
  f = snd C
  SC = SeqCo C

  -- first, we show that [ins] is weakly constant
  ins-wconst : (n : ℕ) → wconst (ins {C = C} n)
  ins-wconst n a₁ a₂ =
    ins n a₁           =⟨ glue n a₁ ⟩
    ins (S n) (f n a₁) =⟨ ap (ins (S n)) (wc n a₁ a₂) ⟩
    ins (S n) (f n a₂) =⟨ ! (glue n a₂) ⟩
    ins n a₂           ∎

  {- Now, we want to define what is overline(i) is the paper
     (here, we call it î-def); that is:
     any a : A n is, if moved to A ω , equal to a₀.

     It is easy to define this, but the tricky part is that
     afterwards, we need to be able to reason about it.
     The 'equational reasoning' combinators are not suitable
     at all for this.

     What we use are the 'reified equational reasoning combinators',
     which allow this sort of thing. These are in the HoTT library,
     implemented by Guillaume Brunerie [I have extended it a bit
     in order to make it useable in my situation].

     For an introduction to the concept, see the file

                   lib.types.PathSeq.

     -}

  î-def : (n : ℕ) → (a : A n) → (ins {C = C} n a) =-= (ins O a₀)
  î-def n a =
    ins n a
      =⟪ glue n a ⟫
    ins (S n) (f n a)
      =⟪ ap (ins (S n)) (wc n _ _) ⟫
    ins (S n) (lift-point C a₀ (S n))
      =⟪ ! (lift-point-= C a₀ (S n)) ⟫
    ins O a₀
      ∎∎

  {- It was easy to define î; it is more difficult to show that it satisfied
     the required coherence.
     This is the 'heptagon-proof'; we present it in
     nicolai.pseudotruncations.heptagon.agda.
  -}

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Excercises where

open import Library
open import Core/Category

SmallType : Category (mk (ℓ-suc ℓ-zero) ℓ-zero)
SmallType = record
  { Obj   = Set
  ; _⇒_   = λ (X Y : Set) → (X → Y)
  ; id    = λ (X : Set) → (λ x → x)
  ; _∘_   = λ {X Y Z : Set} (g : Y → Z) (f : X → Y) → (λ x → g (f x))
  ; idl   = ≡-refl
  ; idr   = ≡-refl
  ; assoc = ≡-refl
  }

max_stars_repo_name: gunpinyo/agda-cat

max_issues_repo_name: gunpinyo/agda-cat

max_forks_repo_name: gunpinyo/agda-cat


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

module Issue203 where

open import Common.Level

-- Should work but give unsolved metas (type of b)
data ↓ {a b} (A : Set a) : Set a where
  [_] : (x : A) → ↓ A

mutual -- avoid freezing

  -- Shouldn't instantiate the level of Σ to a
  data Σ {a b} (A : Set a) (B : A → Set b) : Set _ where
    _,_ : (x : A) (y : B x) → Σ A B

  instantiateToMax : ∀ {a b}(A : Set a)(B : A → Set b) → Set (a ⊔ b)
  instantiateToMax = Σ


text:
-- Test unquoteTC and quoteTC primitives.
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality
open import Common.Product

sum : List Nat → Nat
sum [] = 0
sum (x ∷ xs) = x + sum xs

pattern `Bool = def (quote Bool) []
pattern `true = con (quote true) []
pattern `false = con (quote false) []

infix 2 case_of_
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

macro
  ` : Term → Tactic
  ` v hole = bindTC (quoteTC v) λ e → unify hole e

  ~ : Term → Tactic
  ~ e hole = bindTC (unquoteTC e) λ v → unify hole v

  msum : Term → Tactic
  msum e hole = bindTC (unquoteTC e) λ xs → unify hole (lit (nat (sum xs)))

test₁ : Term
test₁ = ` (1 ∷ 2 ∷ 3 ∷ [])

test₂ : ~ test₁ ≡ (1 ∷ 2 ∷ 3 ∷ [])
test₂ = refl

test₃ : msum (1 ∷ 2 ∷ 3 ∷ []) ≡ 6
test₃ = refl

macro
  simp : Term → Tactic
  simp (def f (vArg x ∷ [])) hole =
    checkType (def f []) (pi (vArg `Bool) (abs "_" `Bool)) >>= λ _ →
    unquoteTC (def f (vArg `true  ∷ [])) >>= λ (t : Bool) →
    unquoteTC (def f (vArg `false ∷ [])) >>= λ (f : Bool) →
    unify hole (case (t , f) of λ
    { (true , true)   → `true
    ; (false , false) → `false
    ; (true , false)  → x
    ; (false , true)  → def (quote not) (vArg x ∷ [])
    })
  simp v _ = typeError (strErr "Can't simplify" ∷ termErr v ∷ [])

f₁ f₂ f₃ f₄ : Bool → Bool
f₁ false = false
f₁ true  = false

f₂ false = false
f₂ true  = true

f₃ false = true
f₃ true  = false

f₄ false = true
f₄ true  = true

test-f₁ : ∀ b → simp (f₁ b) ≡ false
test-f₁ b = refl

test-f₂ : ∀ b → simp (f₂ b) ≡ b
test-f₂ b = refl

test-f₃ : ∀ b → simp (f₃ b) ≡ not b
test-f₃ b = refl

test-f₄ : ∀ b → simp (f₄ b) ≡ true
test-f₄ b = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Record
open import Cubical.Algebra.Semigroup

open import Cubical.Reflection.StrictEquiv

open Iso

private
  variable
    ℓ : Level

record IsMonoid {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor ismonoid

  field
    isSemigroup : IsSemigroup _·_
    identity    : (x : A) → (x · ε ≡ x) × (ε · x ≡ x)

  open IsSemigroup isSemigroup public

  lid : (x : A) → ε · x ≡ x
  lid x = identity x .snd

  rid : (x : A) → x · ε ≡ x
  rid x = identity x .fst

record MonoidStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
  constructor monoidstr

  field
    ε        : A
    _·_      : A → A → A
    isMonoid : IsMonoid ε _·_

  infixl 7 _·_

  open IsMonoid isMonoid public

  -- semigrp : Semigroup
  -- semigrp = record { isSemigroup = isSemigroup }

  -- open Semigroup semigrp public

Monoid : Type (ℓ-suc ℓ)
Monoid = TypeWithStr _ MonoidStr

monoid : (A : Type ℓ) (ε : A) (_·_ : A → A → A) (h : IsMonoid ε _·_) → Monoid
monoid A ε _·_ h = A , monoidstr ε _·_ h

-- Easier to use constructors

makeIsMonoid : {M : Type ℓ} {ε : M} {_·_ : M → M → M}
               (is-setM : isSet M)
               (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
               (rid : (x : M) → x · ε ≡ x)
               (lid : (x : M) → ε · x ≡ x)
             → IsMonoid ε _·_
IsMonoid.isSemigroup (makeIsMonoid is-setM assoc rid lid) = issemigroup is-setM assoc
IsMonoid.identity (makeIsMonoid is-setM assoc rid lid) = λ x → rid x , lid x

makeMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             (is-setM : isSet M)
             (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
             (rid : (x : M) → x · ε ≡ x)
             (lid : (x : M) → ε · x ≡ x)
           → Monoid
makeMonoid ε _·_ is-setM assoc rid lid =
  monoid _ ε _·_ (makeIsMonoid is-setM assoc rid lid)

record MonoidEquiv (M N : Monoid {ℓ}) (e : ⟨ M ⟩ ≃ ⟨ N ⟩) : Type ℓ where

  constructor monoidiso

  private
    module M = MonoidStr (snd M)
    module N = MonoidStr (snd N)

  field
    presε : equivFun e M.ε ≡ N.ε
    isHom : (x y : ⟨ M ⟩) → equivFun e (x M.· y) ≡ equivFun e x N.· equivFun e y

module MonoidΣTheory {ℓ} where

  RawMonoidStructure : Type ℓ → Type ℓ
  RawMonoidStructure X = X × (X → X → X)

  RawMonoidEquivStr = AutoEquivStr RawMonoidStructure

  rawMonoidUnivalentStr : UnivalentStr _ RawMonoidEquivStr
  rawMonoidUnivalentStr = autoUnivalentStr RawMonoidStructure

  MonoidAxioms : (M : Type ℓ) → RawMonoidStructure M → Type ℓ
  MonoidAxioms M (e , _·_) = IsSemigroup _·_
                            × ((x : M) → (x · e ≡ x) × (e · x ≡ x))

  MonoidStructure : Type ℓ → Type ℓ
  MonoidStructure = AxiomsStructure RawMonoidStructure MonoidAxioms

  MonoidΣ : Type (ℓ-suc ℓ)
  MonoidΣ = TypeWithStr ℓ MonoidStructure

  isPropMonoidAxioms : (M : Type ℓ) (s : RawMonoidStructure M) → isProp (MonoidAxioms M s)
  isPropMonoidAxioms M (e , _·_) =
    isPropΣ (isPropIsSemigroup _·_)
            λ α → isPropΠ λ _ → isProp× (IsSemigroup.is-set α _ _) (IsSemigroup.is-set α _ _)

  MonoidEquivStr : StrEquiv MonoidStructure ℓ
  MonoidEquivStr = AxiomsEquivStr RawMonoidEquivStr MonoidAxioms

  MonoidAxiomsIsoIsMonoid : {M : Type ℓ} (s : RawMonoidStructure M)
    → Iso (MonoidAxioms M s) (IsMonoid (s .fst) (s .snd))
  fun (MonoidAxiomsIsoIsMonoid s) (x , y)        = ismonoid x y
  inv (MonoidAxiomsIsoIsMonoid s) a = (IsMonoid.isSemigroup a) , IsMonoid.identity a
  rightInv (MonoidAxiomsIsoIsMonoid s) _         = refl
  leftInv (MonoidAxiomsIsoIsMonoid s) _          = refl

  MonoidAxioms≡IsMonoid : {M : Type ℓ} (s : RawMonoidStructure M)
    → MonoidAxioms M s ≡ IsMonoid (s .fst) (s .snd)
  MonoidAxioms≡IsMonoid s = ua (strictIsoToEquiv (MonoidAxiomsIsoIsMonoid s))

  open MonoidStr

  Monoid→MonoidΣ : Monoid → MonoidΣ
  Monoid→MonoidΣ (A , M) =
    A , (ε M , _·_ M) , MonoidAxiomsIsoIsMonoid (ε M , _·_ M) .inv (isMonoid M)

  MonoidΣ→Monoid : MonoidΣ → Monoid
  MonoidΣ→Monoid (M , (ε , _·_) , isMonoidΣ) =
    monoid M ε _·_ (MonoidAxiomsIsoIsMonoid (ε , _·_) .fun isMonoidΣ)

  MonoidIsoMonoidΣ : Iso Monoid MonoidΣ
  MonoidIsoMonoidΣ =
    iso Monoid→MonoidΣ MonoidΣ→Monoid (λ _ → refl) (λ _ → refl)

  monoidUnivalentStr : UnivalentStr MonoidStructure MonoidEquivStr
  monoidUnivalentStr = axiomsUnivalentStr _ isPropMonoidAxioms rawMonoidUnivalentStr

  MonoidΣPath : (M N : MonoidΣ) → (M ≃[ MonoidEquivStr ] N) ≃ (M ≡ N)
  MonoidΣPath = SIP monoidUnivalentStr

  MonoidEquivΣ : (M N : Monoid) → Type ℓ
  MonoidEquivΣ M N = Monoid→MonoidΣ M ≃[ MonoidEquivStr ] Monoid→MonoidΣ N

  MonoidIsoΣPath : {M N : Monoid} → Iso (Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] (MonoidEquiv M N e)) (MonoidEquivΣ M N)
  fun MonoidIsoΣPath (e , monoidiso h1 h2) = (e , h1 , h2)
  inv MonoidIsoΣPath (e , h1 , h2)         = (e , monoidiso h1 h2)
  rightInv MonoidIsoΣPath _                = refl
  leftInv MonoidIsoΣPath _                 = refl

  MonoidPath : (M N : Monoid {ℓ}) → (Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] (MonoidEquiv M N e)) ≃ (M ≡ N)
  MonoidPath M N =
    Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] MonoidEquiv M N e ≃⟨ isoToEquiv MonoidIsoΣPath ⟩
    MonoidEquivΣ M N                      ≃⟨ MonoidΣPath _ _ ⟩
    Monoid→MonoidΣ M ≡ Monoid→MonoidΣ N ≃⟨ isoToEquiv (invIso (congIso MonoidIsoMonoidΣ)) ⟩
    M ≡ N ■

  RawMonoidΣ : Type (ℓ-suc ℓ)
  RawMonoidΣ = TypeWithStr ℓ RawMonoidStructure

  Monoid→RawMonoidΣ : Monoid → RawMonoidΣ
  Monoid→RawMonoidΣ (A , M) = A , (ε M) , (_·_ M)

  InducedMonoid : (M : Monoid) (N : RawMonoidΣ) (e : M .fst ≃ N .fst)
                 → RawMonoidEquivStr (Monoid→RawMonoidΣ M) N e → Monoid
  InducedMonoid M N e r =
    MonoidΣ→Monoid (inducedStructure rawMonoidUnivalentStr (Monoid→MonoidΣ M) N (e , r))

  InducedMonoidPath : (M : Monoid {ℓ}) (N : RawMonoidΣ) (e : M .fst ≃ N .fst)
                      (E : RawMonoidEquivStr (Monoid→RawMonoidΣ M) N e)
                    → M ≡ InducedMonoid M N e E
  InducedMonoidPath M N e E =
    MonoidPath M (InducedMonoid M N e E) .fst (e , monoidiso (E .fst) (E .snd))

-- We now extract the important results from the above module

isPropIsMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M) → isProp (IsMonoid ε _·_)
isPropIsMonoid ε _·_ =
  subst isProp (MonoidΣTheory.MonoidAxioms≡IsMonoid (ε , _·_))
        (MonoidΣTheory.isPropMonoidAxioms _ (ε , _·_))

MonoidPath : (M N : Monoid {ℓ}) → (Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] MonoidEquiv M N e) ≃ (M ≡ N)
MonoidPath {ℓ = ℓ} =
  SIP
    (autoUnivalentRecord
      (autoRecordSpec (MonoidStr {ℓ}) MonoidEquiv
        (fields:
          data[ ε ∣ presε ]
          data[ _·_ ∣ isHom ]
          prop[ isMonoid ∣ (λ _ → isPropIsMonoid _ _) ]))
      _ _)
  where
  open MonoidStr
  open MonoidEquiv

InducedMonoid : (M : Monoid {ℓ}) (N : MonoidΣTheory.RawMonoidΣ) (e : M .fst ≃ N .fst)
              → MonoidΣTheory.RawMonoidEquivStr (MonoidΣTheory.Monoid→RawMonoidΣ M) N e
              → Monoid
InducedMonoid = MonoidΣTheory.InducedMonoid

InducedMonoidPath : (M : Monoid {ℓ}) (N : MonoidΣTheory.RawMonoidΣ) (e : M .fst ≃ N .fst)
                    (E : MonoidΣTheory.RawMonoidEquivStr (MonoidΣTheory.Monoid→RawMonoidΣ M) N e)
                  → M ≡ InducedMonoid M N e E
InducedMonoidPath = MonoidΣTheory.InducedMonoidPath

module MonoidTheory {ℓ} (M : Monoid {ℓ}) where

  open MonoidStr (snd M)

  -- Added for its use in groups
  -- If there exists a inverse of an element it is unique
  inv-lemma : (x y z : ⟨ M ⟩) → y · x ≡ ε → x · z ≡ ε → y ≡ z
  inv-lemma x y z left-inverse right-inverse =
    y           ≡⟨ sym (rid y) ⟩
    y · ε       ≡⟨ cong (λ - → y · -) (sym right-inverse) ⟩
    y · (x · z) ≡⟨ assoc y x z ⟩
    (y · x) · z ≡⟨ cong (λ - → - · z) left-inverse ⟩
    ε · z       ≡⟨ lid z ⟩
    z ∎

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-# OPTIONS --without-K #-}
module PathStructure.Nat where

open import Equivalence
open import PathOperations
open import Types

F : ℕ → ℕ → Set
F = ind (λ _ → ℕ → Set)
  (λ _ r → ind (λ _ → Set) (λ n-1 _ → r n-1) ⊥)
  (        ind (λ _ → Set) (λ _   _ → ⊥)     ⊤)

F-lemma : ∀ n → F n n
F-lemma = ind (λ n → F n n) (λ _ f → f) _

-- Explicit arguments to prevent code littered with curly brackets.
split-path : ∀ x y → x ≡ y → F x y
split-path x _ p = tr (F x) p (F-lemma x)

merge-path : ∀ x y → F x y → x ≡ y
merge-path _ _ f = ind
  (λ x → ∀ y → F x y → x ≡ y)
  (λ x r → ind
    (λ y → F (suc x) y → suc x ≡ y)
    (λ _ _ f → ap suc (r _ f))
    0-elim)
  (ind
    (λ y → F zero y → zero ≡ y)
    (λ _ _ → 0-elim)
    (λ _ → refl))
  _ _ f

-- Lemmas.
ap-refl : ∀ {n} (p : n ≡ n) → p ≡ refl →
  ap suc p ≡ refl
ap-refl _ = J
  (λ p q _ → J (λ x y _ → suc x ≡ suc y) (λ _ → refl) _ _ p ≡ ap suc q)
  (λ _ → refl) _ refl

tr-ap : ∀ m n (f : F m n) →
    tr (F (suc m))       (ap suc (merge-path m n f)) (F-lemma (suc m))
  ≡ tr (F (suc m) ∘ suc)         (merge-path m n f)  (F-lemma (suc m))
tr-ap m n f = J
  (λ x y p → tr (F (suc x))       (ap suc p) (F-lemma (suc x))
           ≡ tr (F (suc x) ∘ suc)         p  (F-lemma (suc x)))
  (λ _ → refl)
  _ _ (merge-path m n f)

split-merge-eq : ∀ {x y} → (x ≡ y) ≃ F x y
split-merge-eq {x = x} {y = y}
  = split-path _ _
  , (merge-path _ _ , λ f → ind
      (λ x → ∀ y (f : F x y) → split-path x y (merge-path x y f) ≡ f)
      (λ x r → ind
        (λ y → (f : F (suc x) y) →
          split-path (suc x) y (merge-path (suc x) y f) ≡ f)
        (λ y _ f → tr-ap x y f · r y f)
        (λ b → 0-elim b))
      (ind
        (λ y → (f : F zero y) →
          split-path zero y (merge-path zero y f) ≡ f)
        (λ _ _ b → 0-elim b)
        (λ _ → refl))
      x y f)
  , (merge-path _ _ , J
      (λ _ _ p → merge-path _ _ (split-path _ _ p) ≡ p)
      (ind
        (λ x → merge-path x x (split-path x x refl) ≡ refl)
        (λ _ → ap-refl _)
        refl)
      _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module PiFrac.Everything where
open import PiFrac.Syntax     -- Syntax of PiFrac
open import PiFrac.Opsem      -- Abstract machine semantics of PiFrac
open import PiFrac.AuxLemmas  -- Some auxiliary lemmas about opsem for forward/backward deterministic proof
open import PiFrac.NoRepeat   -- Forward/backward deterministic lemmas and Non-repeating lemma
open import PiFrac.Invariants -- Some invariants about abstract machine semantics
open import PiFrac.Eval       -- Evaluator for PiFrac
open import PiFrac.Interp     -- Big-step intepreter for PiFrac using Maybe monad
open import PiFrac.Properties -- Properties of PiFrac
open import PiFrac.Examples   -- Examples
open import PiFrac.Category   -- PiFrac pointed category


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Delta-observational equivalence - support for equational reasoning
------------------------------------------------------------------------
module Base.Change.Equivalence.EqReasoning where

open import Relation.Binary.PropositionalEquality
open import Base.Change.Algebra
open import Level
open import Data.Unit
open import Function

open import Base.Change.Equivalence.Base public

module _ {a} {A : Set a} {{ca : ChangeAlgebra A}} {x : A} where
  ------------------------------------------------------------------------
  -- Convenient syntax for equational reasoning

  import Relation.Binary.EqReasoning as EqR

  module ≙-Reasoning where
    open EqR (≙-setoid {x = x}) public
      renaming (_≈⟨_⟩_ to _≙⟨_⟩_)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --no-qualified-instances #-}

postulate
  A : Set
  f : {{A}} → A

module M where postulate instance a : A

test : A
test = f


text:
-- P: <E[fork e]> --> <E[()]> | <e>
module Properties.StepFork where

open import Data.List
open import Data.List.All
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import ProcessSyntax
open import ProcessRun

open import Properties.Base

mkfork : ∀ {Φ Φ₁ Φ₂} → Split Φ Φ₁ Φ₂ → Expr Φ₁ TUnit → Expr (TUnit ∷ Φ₂) TUnit → Expr Φ TUnit
mkfork sp e E = letbind sp (fork e) E

mklhs : ∀ {Φ Φ₁ Φ₂} → Split Φ Φ₁ Φ₂
  → Expr Φ₁ TUnit → Expr (TUnit ∷ Φ₂) TUnit → Proc Φ
mklhs sp e E =
  exp (mkfork sp e E)

mkrhs : ∀ {Φ Φ₁ Φ₂} → Split Φ Φ₁ Φ₂
  → Expr Φ₁ TUnit → Expr (TUnit ∷ Φ₂) TUnit → Proc Φ
mkrhs sp e E =
  par sp (exp e) (exp (letbind (split-all-right _) (unit []) E))

-- weaken2-command : ∀ {G} G' G'' → Command (G' ++ G) → Command (G' ++ inactive-clone G'' ++ G)

-- obviously true, but requires a nasty inductive proof
postulate
  weaken2-ident : ∀ {G} → (cmd : Command G) → weaken2-command [] [] cmd ≡ cmd

reduction : (e : Expr [] TUnit) → (E : Expr (TUnit ∷ []) TUnit)
  →
    let lhs = (runProc [] (mklhs [] e E) (vnil []-inactive)) in
    let rhs = (runProc [] (mkrhs [] e E) (vnil []-inactive)) in
    let rhs' = one-step rhs in
    one-step lhs ≡
    (Forked , proj₁ rhs , proj₂ rhs)
reduction e E
  with ssplit-refl-left-inactive []
... | G' , ina-G' , ss-GG'
  rewrite weaken2-ident (run [] ss-[] e (vnil []-inactive) (halt []-inactive UUnit))
  = refl

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
-- Andreas, 2019-07-07, issue #3892

postulate Foo : Set
data Foo where

-- WAS: internal error

-- EXPECTED:
-- Multiple definitions of Foo. Previous definition at ...


text:
module Structure.Setoid {ℓₑ ℓₒ} where

import Lvl
open import Functional.Dependent
open import Lang.Instance
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Relator.Equivalence
open import Syntax.Function
import      Type

module _ where
  open Type

  -- An instance of `Equiv(T)` is that the type `T` has an equivalence relation which may be treated as a default one.
  -- Helps finding an instance of an equivalence relation for a type.
  record Equiv (T : Type{ℓₒ}) : Type{Lvl.𝐒(ℓₑ) Lvl.⊔ ℓₒ} where
    constructor intro

    infixl 15 _≡_ _≢_
    field
      _≡_ : T → T → Type{ℓₑ}

    field
      instance ⦃ equivalence ⦄ : Equivalence(_≡_)

    _≢_ : T → T → Type{ℓₑ}
    a ≢ b = ¬(a ≡ b)

    open Equivalence(equivalence) public

  open Equiv ⦃ ... ⦄ using (_≡_ ; _≢_) renaming (equivalence to Equiv-equivalence) public
  {-# INLINE _≡_ #-} -- TODO: Not sure if this does anything
  {-# DISPLAY Equiv._≡_ a b = a ≡ b #-} -- TODO: Not sure about this either

module _ where
  -- A set and an equivalence relation on it
  Setoid = ∃(Equiv)
  module Setoid(([∃]-intro T ⦃ equiv-T ⦄) : Setoid) where
    Type : Type.Type
    Type = T
    open Equiv(equiv-T) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module subrings where

import rings
open rings public

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

{- Subrings -}

subset-Ring :
  (l : Level) {l1 : Level} → Ring l1 → UU ((lsuc l) ⊔ l1)
subset-Ring l R = type-Ring R → UU-Prop l

is-additive-subset-Ring :
  {l l1 : Level} (R : Ring l1) (S : subset-Ring l R) → UU _
is-additive-subset-Ring R S =
  (x y : type-Ring R) →
  type-Prop (S x) → type-Prop (S y) → type-Prop (S (add-Ring R x y))

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
open import Relation.Binary.Core

module BSTree.Properties  {A : Set}
               (_≤_ : A → A → Set)
               (trans≤ : Transitive _≤_) where

open import BTree {A}
open import BSTree _≤_
open import List.Order.Simple _≤_
open import List.Order.Simple.Properties _≤_ trans≤
open import List.Sorted _≤_

lemma-*⊴-*≤ : {x : A}{t : BTree} → BSTree t → t *⊴ x → flatten t *≤ x
lemma-*⊴-*≤ slf lelf = lenx
lemma-*⊴-*≤ (snd sl sr l≤y y≤r) (lend y≤x r≤x) = lemma-++-*≤ y≤x (lemma-*⊴-*≤ sl l≤y) (lemma-*⊴-*≤ sr r≤x)

lemma-⊴*-≤* : {x : A}{t : BTree} → BSTree t → x ⊴* t → x ≤* flatten t
lemma-⊴*-≤* slf gelf = genx
lemma-⊴*-≤* (snd sl sr l≤y y≤r) (gend x≤y x≤l) = lemma-≤*-++ x≤y (lemma-⊴*-≤* sl x≤l) (lemma-⊴*-≤* sr y≤r)

lemma-bst-sorted : {t : BTree} → BSTree t → Sorted (flatten t)
lemma-bst-sorted slf = nils
lemma-bst-sorted (snd sl sr l≤x x≤r) = lemma-sorted++ (lemma-*⊴-*≤ sl l≤x) (lemma-⊴*-≤* sr x≤r) (lemma-bst-sorted sl) (lemma-bst-sorted sr)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Issue203 where

open import Imports.Level

-- shouldn't work
data Bad {a b} (A : Set a) : Set b where
  [_] : (x : A) → Bad A

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Issue395 where

foo : Set → Set₁
foo foo with Set
... | _ = Set


text:
{-# OPTIONS --without-K #-}
module sum-properties-setoid where

open import Type
import Level as L

open import Algebra
import Algebra.FunctionProperties as FP

open import Data.Zero using (𝟘)
open import Data.Bool.NP
open Data.Bool.NP.Indexed
open import Data.Fin using (Fin)
open import Data.Nat.NP
open import Data.Nat.Properties
open import Data.Product renaming (map to pmap)
open import Data.Sum
open import Data.One using (𝟙)
open import Function.NP
import Function.Inverse as Inv
open Inv using (_↔_)
open import Function.Related
open import Function.Related.TypeIsomorphisms.NP

import Function.Equality as FE
open FE using (_⟨$⟩_)

import Function.Injection as FInj

open import sum-setoid

open import Relation.Binary
open import Relation.Binary.Sum.NP
open import Relation.Binary.Product.Pointwise
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_ ; _≗_ ; _≗₂_)

module _ {A : ★} (μA : SumProp A) (f g : A → ℕ) where
    open ≡.≡-Reasoning

    sum-⊓-∸ : sum μA f ≡ sum μA (f ⊓° g) + sum μA (f ∸° g)
    sum-⊓-∸ = sum μA f                          ≡⟨ sum-ext μA (f ⟨ a≡a⊓b+a∸b ⟩° g) ⟩
              sum μA ((f ⊓° g) +° (f ∸° g))     ≡⟨ sum-hom μA (f ⊓° g) (f ∸° g) ⟩
              sum μA (f ⊓° g) + sum μA (f ∸° g) ∎

    sum-⊔-⊓ : sum μA f + sum μA g ≡ sum μA (f ⊔° g) + sum μA (f ⊓° g)
    sum-⊔-⊓ = sum μA f + sum μA g               ≡⟨ ≡.sym (sum-hom μA f g) ⟩
              sum μA (f +° g)                   ≡⟨ sum-ext μA (f ⟨ a+b≡a⊔b+a⊓b ⟩° g) ⟩
              sum μA (f ⊔° g +° f ⊓° g)         ≡⟨ sum-hom μA (f ⊔° g) (f ⊓° g) ⟩
              sum μA (f ⊔° g) + sum μA (f ⊓° g) ∎

    sum-⊔ : sum μA (f ⊔° g) ≤ sum μA f + sum μA g
    sum-⊔ = ℕ≤.trans (sum-mono μA (f ⟨ ⊔≤+ ⟩° g)) (ℕ≤.reflexive (sum-hom μA f g))

module _M2 {A : ★} (μA : SumProp A) (f g : A → Bool) where
    count-∧-not : count μA f ≡ count μA (f ∧° g) + count μA (f ∧° not° g)
    count-∧-not rewrite sum-⊓-∸ μA (toℕ ∘ f) (toℕ ∘ g)
                      | sum-ext μA (f ⟨ toℕ-⊓ ⟩° g)
                      | sum-ext μA (f ⟨ toℕ-∸ ⟩° g)
                      = ≡.refl

    count-∨-∧ : count μA f + count μA g ≡ count μA (f ∨° g) + count μA (f ∧° g)
    count-∨-∧ rewrite sum-⊔-⊓ μA (toℕ ∘ f) (toℕ ∘ g)
                    | sum-ext μA (f ⟨ toℕ-⊔ ⟩° g)
                    | sum-ext μA (f ⟨ toℕ-⊓ ⟩° g)
                    = ≡.refl

    count-∨≤+ : count μA (f ∨° g) ≤ count μA f + count μA g
    count-∨≤+ = ℕ≤.trans (ℕ≤.reflexive (sum-ext μA (≡.sym ∘ (f ⟨ toℕ-⊔ ⟩° g))))
                         (sum-⊔ μA (toℕ ∘ f) (toℕ ∘ g))

sum-ext₂ : ∀ {A B}{f g : A → B → ℕ}(μA : SumProp A)(μB : SumProp B) → f ≗₂ g → sum μA (sum μB ∘ f) ≡ sum μA (sum μB ∘ g)
sum-ext₂ μA μB f≗g = sum-ext μA (sum-ext μB ∘ f≗g)

Injective : ∀ {a b}{A : Set a}{B : Set b}(f : A → B) → Set (a L.⊔ b)
Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

Injectivoid : ∀ {A B : SEToid} → (Setoid.Carrier A → Setoid.Carrier B) → Set
Injectivoid {A}{B} f = ∀ {x y} → Setoid._≈_ B (f x) (f y) → Setoid._≈_ A x y

StableUnderInjection : ∀ {A} → SumPropoid A → Set
StableUnderInjection {A} μ = ∀ p → SumStableUnder μ (FInj.Injection.to p)

CountStableUnderInjection : ∀ {A} → SumPropoid A → Set
CountStableUnderInjection μ = ∀ p → CountStableUnder μ (FInj.Injection.to p)

{-
#-StableUnderInjection : ∀ {A}{μ : SumPropoid A} → StableUnderInjection μ
    → ∀ f p → Injective p → count μ f ≡ count μ (f ∘ p)
#-StableUnderInjection sui f p p-inj = {!sui p p-inj (toℕ ∘ f)!}
-}

sum$ : ∀ {As} → SumPropoid As → (As FE.⟶ ≡.setoid ℕ) → ℕ
sum$ μA f = sum μA (_⟨$⟩_ f)

infix 4 _≈_ -- _≈'_

record _≈_ {As Bs : SEToid}(μA : SumPropoid As)(μB : SumPropoid Bs): Set where
  constructor mk
  field
    iso : Inv.Inverse As Bs

  private
    A = Setoid.Carrier As
    B = Setoid.Carrier Bs

  from : Bs FE.⟶ As
  from = Inv.Inverse.from iso

  from$ : B → A
  from$ = _⟨$⟩_ from

  to : As FE.⟶ Bs
  to = Inv.Inverse.to iso

  to$ : A → B
  to$ = _⟨$⟩_ to

  from-inj : FInj.Injection Bs As -- Injectivoid {Bs} {As} from$
  from-inj = Inv.Inverse.injection (Inv.sym iso)

  to-inj : FInj.Injection As Bs -- Injectivoid {As} {Bs} to$
  to-inj = Inv.Inverse.injection iso

  field
    sums-ok : ∀ f → sum$ μA f ≡ sum$ μB (f FE.∘ from)

  sums-ok' : ∀ f → sum$ μB f ≡ sum$ μA (f FE.∘ to)
  sums-ok' f
             = sum$ μB f
             ≡⟨ search-extoid μB _+_ {f = f}
                  {g = f FE.∘ to FE.∘ from}
                  (λ {x}{y} x≈y → FE.cong f (SB.trans x≈y (SB.sym (Inv.Inverse.right-inverse-of iso y)))) ⟩
               sum$ μB (f FE.∘ to FE.∘ from)
             ≡⟨ ≡.sym (sums-ok (f FE.∘ to)) ⟩
               sum$ μA (f FE.∘ to)
             ∎
    where open ≡.≡-Reasoning
          module SB = Setoid Bs
          module SA = Setoid As

  StableUnder≈ : StableUnderInjection μA → StableUnderInjection μB
  StableUnder≈ μA-SUI p f
    = sum$ μB f
    ≡⟨ sums-ok' f ⟩
      sum$ μA (f FE.∘ to)
    ≡⟨ μA-SUI (from-inj FInj.∘ p FInj.∘ to-inj) (f FE.∘ to) ⟩
      sum$ μA (f FE.∘ to FE.∘ from FE.∘ FInj.Injection.to p FE.∘ to)
    ≡⟨ ≡.sym (sums-ok' (f FE.∘ to FE.∘ from FE.∘ FInj.Injection.to p)) ⟩
      sum$ μB (f FE.∘ to FE.∘ from FE.∘ FInj.Injection.to p)
    ≡⟨ search-extoid μB _+_
         {f = f FE.∘ to FE.∘ from FE.∘ FInj.Injection.to p}
         {g = f FE.∘ FInj.Injection.to p} (FE.cong f ∘ Setoid.trans Bs (Inv.Inverse.right-inverse-of iso _) ∘ FE.cong (FInj.Injection.to p)) ⟩
      sum$ μB (f FE.∘ FInj.Injection.to p)
    ∎
    where open ≡.≡-Reasoning

_≈'_ : ∀ {A B} (μA : SumProp A)(μB : SumProp B) → Set
_≈'_ = _≈_

≈-refl : ∀ {A} (μA : SumPropoid A) → μA ≈ μA
≈-refl μA = mk Inv.id (λ f → ≡.refl)

≈-id : ∀ {A} {μA : SumPropoid A} → μA ≈ μA
≈-id = ≈-refl _

≈-sym : ∀ {A B}{μA : SumPropoid A}{μB : SumPropoid B} → μA ≈ μB → μB ≈ μA
≈-sym A≈B = mk (Inv.sym iso) sums-ok'
  where open _≈_ A≈B

≈-trans : ∀ {A B C}{μA : SumPropoid A}{μB : SumPropoid B}{μC : SumPropoid C} → μA ≈ μB → μB ≈ μC → μA ≈ μC
≈-trans A≈B B≈C = mk (iso B≈C Inv.∘ iso A≈B) (λ f → ≡.trans (sums-ok A≈B f) (sums-ok B≈C (f FE.∘ from A≈B)))
  where open _≈_

infix 2 _≈∎
infixr 2 _≈⟨_⟩_

_≈∎ : ∀ {A} (μA : SumPropoid A) → μA ≈ μA
_≈∎ = ≈-refl

_≈⟨_⟩_ : ∀ {A B C} (μA : SumPropoid A){μB : SumPropoid B}{μC : SumPropoid C} → μA ≈ μB → μB ≈ μC → μA ≈ μC
_ ≈⟨ A≈B ⟩ B≈C = ≈-trans A≈B B≈C

lift-⊎ : ∀ {A B : Set} → Inv.Inverse (≡.setoid (A ⊎ B)) ((≡.setoid A) ⊎-setoid (≡.setoid B))
lift-⊎ {A} {B} =  record { to = to; from = from; inverse-of = inverse-of } where
  to : _
  to = record { _⟨$⟩_ = id; cong = cong } where
    cong : ∀ {i j} → i ≡ j → _
    cong ≡.refl = Setoid.refl (≡.setoid (A) ⊎-setoid (≡.setoid B))

  from : _
  from = record { _⟨$⟩_ = id; cong = cong } where
    cong : ∀ {i j} → ⊎ʳ 𝟘 _≡_ _≡_ i j → i ≡ j
    cong (₁∼₂ ())
    cong (₁∼₁ x∼₁y) = ≡.cong inj₁ x∼₁y
    cong (₂∼₂ x∼₂y) = ≡.cong inj₂ x∼₂y

  inverse-of : _
  inverse-of = record { left-inverse-of = left-inverse-of; right-inverse-of = right-inverse-of } where
   left-inverse-of : (_ : _) → _
   left-inverse-of  x = Setoid.refl (≡.setoid (A ⊎ B))

   right-inverse-of : (_ : _) → _
   right-inverse-of x = Setoid.refl ((≡.setoid A) ⊎-setoid (≡.setoid B))

Fin0≈𝟙 : μFinSuc zero ≈ μ𝟙
Fin0≈𝟙 = mk iso sums-ok where
  open import Relation.Binary.Sum
  iso : _
  iso = (A⊎𝟘↔A Inv.∘ Inv.id ⊎-cong Fin0↔𝟘) Inv.∘ Fin∘suc↔𝟙⊎Fin

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

𝟙+Fin : ∀ {n} → μ𝟙 +μ μFinSuc n ≈ μFinSuc (suc n)
𝟙+Fin {n} = mk iso sums-ok where
  iso : _
  iso = Inv.sym (Inv._∘_ (lift-⊎ {𝟙} {Fin (suc n)}) Fin∘suc↔𝟙⊎Fin)

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

𝟙×A≈A : ∀ {A}{μA : SumProp A} → μ𝟙 ×μ μA ≈ μA
𝟙×A≈A {A} = mk iso sums-ok where
  iso : _
  iso = ×-ICMon.identityˡ _

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

μFinPres : ∀ {m n} → m ≡ n → μFinSuc m ≈ μFinSuc n
μFinPres eq rewrite eq = ≈-refl _

_+μ-cong_ : ∀ {A B C D}{μA : SumPropoid A}{μB : SumPropoid B}{μC : SumPropoid C}{μD : SumPropoid D}
          → μA ≈ μC → μB ≈ μD → μA +μ μB ≈ μC +μ μD
A≈C +μ-cong B≈D = mk iso sums-ok where
  iso : _
  iso = (_≈_.iso A≈C) ⊎-inverse (_≈_.iso B≈D) -- (_≈_.iso A≈C) ⊎-cong (_≈_.iso B≈D)

  sums-ok : (_ : _) → _
  sums-ok f = ≡.cong₂ _+_ (_≈_.sums-ok A≈C (f FE.∘ inj₁-setoid)) -- (λ x≈y → f-resp (₁∼₁ x≈y)))
                          (_≈_.sums-ok B≈D (f FE.∘ inj₂-setoid)) -- (λ x≈y → f-resp (₂∼₂ x≈y)))

+μ-assoc : ∀ {A B C}(μA : SumPropoid A)(μB : SumPropoid B)(μC : SumPropoid C)
         → (μA +μ μB) +μ μC ≈ μA +μ (μB +μ μC)
+μ-assoc μA μB μC = mk iso sums-ok where
  iso : _
  iso = ⊎-ICMon.assoc _ _ _

  sums-ok : (_ : _) → _
  sums-ok f = ℕ°.+-assoc (sum μA (_⟨$⟩_ f ∘ inj₁ ∘ inj₁)) (sum μB (_⟨$⟩_ f ∘ inj₁ ∘ inj₂)) (sum μC (_⟨$⟩_ f ∘ inj₂))

+μ-comm : ∀ {A B}(μA : SumPropoid A)(μB : SumPropoid B)
        → μA +μ μB ≈ μB +μ μA
+μ-comm μA μB = mk iso sums-ok where
  iso : _
  iso = ⊎-ICMon.comm _ _

  sums-ok : (_ : _) → _
  sums-ok f = ℕ°.+-comm (sum$ μA (f FE.∘ inj₁-setoid)) (sum$ μB (f FE.∘ inj₂-setoid))

_×μ-cong_ :  ∀ {A B C D}{μA : SumPropoid A}{μB : SumPropoid B}{μC : SumPropoid C}{μD : SumPropoid D}
          → μA ≈ μC → μB ≈ μD → μA ×μ μB ≈ μC ×μ μD
_×μ-cong_ {A}{B}{C}{D}{μA}{μB}{μC}{μD} A≈C B≈D = mk iso sums-ok where
  open import Relation.Binary.Product.Pointwise
  iso : _
  iso = _≈_.iso A≈C ×-inverse _≈_.iso B≈D

  sums-ok : (_ : (A ×-setoid B) FE.⟶ ≡.setoid ℕ) → _
  sums-ok f = sum$ (μA ×μ μB) f
            ≡⟨ sum-ext μA (λ xa → _≈_.sums-ok B≈D (record
               { _⟨$⟩_ = λ x → f ⟨$⟩ (xa , x)
               ; cong = λ x → FE.cong f (Setoid.refl A , x) })) ⟩
              sum$ (μA ×μ μD) (f FE.∘ FE.id {A = A} ×-⟶ _≈_.from B≈D)
            ≡⟨ _≈_.sums-ok A≈C (record { _⟨$⟩_ = _; cong = λ x → search-ext μD _+_ (λ y → FE.cong f (x , Setoid.refl B)) }) ⟩
              sum$ (μC ×μ μD) (f FE.∘ Inv.Inverse.from iso)
            ∎ where open ≡.≡-Reasoning

×μ-assoc : ∀ {A B C}(μA : SumPropoid A)(μB : SumPropoid B)(μC : SumPropoid C)
         → (μA ×μ μB) ×μ μC ≈ μA ×μ (μB ×μ μC)
×μ-assoc {A}{B}{C} μA μB μC = mk iso sums-ok where
  iso : _
  iso = ×-ICMon.assoc A B C

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

×μ-comm : ∀ {A B}(μA : SumPropoid A)(μB : SumPropoid B)
        → μA ×μ μB ≈ μB ×μ μA
×μ-comm {A}{B} μA μB = mk iso sums-ok where
  iso : _
  iso = ×-ICMon.comm A B

  sums-ok : (_ : _) → _
  sums-ok f = sum-swap μA μB (curry (_⟨$⟩_ f))

×+-distrib : ∀ {A B C}(μA : SumPropoid A)(μB : SumPropoid B)(μC : SumPropoid C)
           → (μA +μ μB) ×μ μC ≈ (μA ×μ μC) +μ (μB ×μ μC)
×+-distrib {A}{B}{C} μA μB μC = mk iso sums-ok where
  iso : _
  iso = ×⊎°I.distribʳ C A B

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

+-≈ : ∀ m n → (μFinSuc m) +μ (μFinSuc n) ≈ μFinSuc (m + suc n)
+-≈ zero n    = μFinSuc zero +μ μFinSuc n
              ≈⟨ Fin0≈𝟙 +μ-cong ≈-refl (μFinSuc n) ⟩
                μ𝟙 +μ μFinSuc n
              ≈⟨ 𝟙+Fin ⟩
                μFinSuc (suc n)
              ≈∎
+-≈ (suc m) n = μFinSuc (suc m) +μ μFinSuc n
              ≈⟨ ≈-sym 𝟙+Fin +μ-cong ≈-refl (μFinSuc n) ⟩
                (μ𝟙 +μ μFinSuc m) +μ μFinSuc n
              ≈⟨ +μ-assoc μ𝟙 (μFinSuc m) (μFinSuc n) ⟩
                μ𝟙 +μ (μFinSuc m +μ μFinSuc n)
              ≈⟨ ≈-refl μ𝟙 +μ-cong +-≈ m n ⟩
                μ𝟙 +μ μFinSuc (m + suc n)
              ≈⟨ 𝟙+Fin ⟩
                μFinSuc (suc m + suc n)
              ≈∎

×-≈ : ∀ m n → μFinSuc m ×μ μFinSuc n ≈ μFinSuc (n + m * suc n)
×-≈ zero n    = μFinSuc 0 ×μ μFinSuc n
              ≈⟨ Fin0≈𝟙 ×μ-cong (≈-refl (μFinSuc n)) ⟩
                μ𝟙 ×μ μFinSuc n
              ≈⟨ 𝟙×A≈A ⟩
                μFinSuc n
              ≈⟨ μFinPres (ℕ°.+-comm 0 n) ⟩
                μFinSuc (n + 0)
              ≈∎
×-≈ (suc m) n = μFinSuc (suc m) ×μ μFinSuc n
              ≈⟨ ≈-sym 𝟙+Fin ×μ-cong ≈-refl (μFinSuc n) ⟩
                (μ𝟙 +μ μFinSuc m) ×μ μFinSuc n
              ≈⟨ ×+-distrib μ𝟙 (μFinSuc m) (μFinSuc n) ⟩
                (μ𝟙 ×μ μFinSuc n) +μ (μFinSuc m ×μ μFinSuc n)
              ≈⟨ 𝟙×A≈A {μA = μFinSuc n} +μ-cong ×-≈ m n ⟩
                μFinSuc n +μ μFinSuc (n + m * suc n)
              ≈⟨ +-≈ n (n + m * suc n) ⟩
                μFinSuc (n + suc m * suc n)
              ≈∎

open import Data.Fin using (Fin ; zero ; suc)

Finable : ∀ {A} → SumPropoid A → Set
Finable μA = Σ ℕ λ FinCard → μA ≈ μFinSuc FinCard

𝟙-Finable : Finable μ𝟙
𝟙-Finable = 0 , ≈-sym Fin0≈𝟙

Fin-Finable : ∀ {n} → Finable (μFinSuc n)
Fin-Finable {n} = n , ≈-refl (μFinSuc n)

+-Finable : ∀ {A B}(μA : SumPropoid A)(μB : SumPropoid B) → Finable μA → Finable μB → Finable (μA +μ μB)
+-Finable μA μB (|A| , A≈) (|B| , B≈) = (|A| + suc |B|) ,
  ( μA +μ μB
  ≈⟨ A≈ +μ-cong B≈ ⟩
    μFinSuc |A| +μ μFinSuc |B|
  ≈⟨ +-≈ |A| |B| ⟩
    μFinSuc (|A| + suc |B|) ≈∎)

×-Finable : ∀ {A B}(μA : SumPropoid A)(μB : SumPropoid B) → Finable μA → Finable μB → Finable (μA ×μ μB)
×-Finable μA μB (|A| , A≈) (|B| , B≈) = (|B| + |A| * suc |B|) ,
  ( μA ×μ μB
  ≈⟨ A≈ ×μ-cong B≈ ⟩
    μFinSuc |A| ×μ μFinSuc |B|
  ≈⟨ ×-≈ |A| |B| ⟩
    μFinSuc (|B| + |A| * suc |B|)
  ≈∎)

module _ where
  open import bijection-fin
  open import Data.Fin using (Fin; zero; suc)
  open import Data.Vec.NP renaming (sum to vsum)

  sumFin : ∀ n → Sum (Fin n)
  sumFin n f = vsum (tabulate f)

  sumFin-spec : ∀ n → sumFin (suc n) ≗ sum (μFinSuc n)
  sumFin-spec zero    f = ℕ°.+-comm (f zero) 0
  sumFin-spec (suc n) f = ≡.cong (_+_ (f zero)) (sumFin-spec n (f ∘ suc))

  sumFinSUI : ∀ n f p → Injective p → sumFin n f ≡ sumFin n (f ∘ p)
  sumFinSUI n f p p-inj = count-perm f p (λ _ _ → p-inj)

  μFinSUI : ∀ {n} → StableUnderInjection (μFinSuc n)
  μFinSUI {n} p f
    rewrite ≡.sym (sumFin-spec n (_⟨$⟩_ f))
          | ≡.sym (sumFin-spec n (_⟨$⟩_ (f FE.∘ FInj.Injection.to p)))
          = sumFinSUI (suc n) (_⟨$⟩_ f) (_⟨$⟩_ (FInj.Injection.to p)) (FInj.Injection.injective p)

StableIfFinable : ∀ {A} (μA : SumProp A) → Finable μA → StableUnderInjection μA
StableIfFinable μA (_ , A≈Fin)
  = _≈_.StableUnder≈ (≈-sym A≈Fin) μFinSUI

-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Common.Integer where

open import Agda.Builtin.Int public renaming (Int to Integer)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2017-02-15, issue #2462
-- Overloaded postfix projection should resolve

postulate
  A : Set

record R : Set where
  constructor mkR
  field f : A
open R

record S : Set where
  field f : R
open S

test : S → A
test s = let mkR x = s .f in x

-- Error WAS:
-- Cannot resolve overloaded projection f because it is not applied to
-- a visible argument
-- when inferring the type of .f

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module FFI.MachineWord where

import      Lvl
open import Data.Boolean
open import Numeral.Natural
open import String
open import Syntax.Number
open import Type

postulate Word64 : Type{Lvl.𝟎}
{-# BUILTIN WORD64 Word64 #-}

private
  module Primitives where
    primitive primWord64ToNat   : Word64 → ℕ
    primitive primWord64FromNat : ℕ → Word64

module Word64 where
  open Primitives renaming
    ( primWord64ToNat   to toℕ
    ; primWord64FromNat to fromℕ
    ) public

  instance
    Word64-infiniteNumeral : InfiniteNumeral(Word64)
    Word64-infiniteNumeral = InfiniteNumeral.intro fromℕ