text:
module Numeral.Natural.Prime.Proofs.Representation where

import      Lvl
open import Data.Either as Either using ()
open import Data.Tuple as Tuple using ()
open import Functional
open import Function.Equals
open import Lang.Instance
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.CoordinateVector
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Prime
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Divisibility.Proofs.Product
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Relator.Equivalence.Proofs
open import Structure.Relator.Properties
open import Structure.Setoid renaming (_≡_ to _≡ₛ_ ; _≢_ to _≢ₛ_)
open import Structure.Setoid.Uniqueness
open import Syntax.Transitivity
open import Type
open import Type.Dependent

private variable a b : ℕ

record PrimePowers(f : ℕ → ℕ) : Type{Lvl.𝟎} where
  constructor intro
  field
    positive-powers : Σ ℕ (n ↦ Vector(n)(ℕ))
    zeroes-correctness : ∀{n} → Positive(f(n)) ↔ ∃(i ↦ (Σ.right positive-powers(i) ≡ n))
    prime-correctness : ∀{i} → Prime(Σ.right positive-powers(i))

  product : ℕ
  product = foldᵣ(_⋅_)(1) (map(n ↦ n ^ f(n)) (Σ.right positive-powers))

  powers-is-positive : ∀{i} → Positive(f(Σ.right positive-powers(i)))
  powers-is-positive = [↔]-to-[←] zeroes-correctness ([∃]-intro _ ⦃ [≡]-intro ⦄)

  -- postulate power-divide-product : ∀{i} → (Σ.right positive-powers i ∣ product)
  {-power-divide-product {pp}{i = 𝟎} = divides-with-[⋅]
    {b = (PrimePowers.positive-powers pp 𝟎) ^ (PrimePowers.power pp (PrimePowers.positive-powers pp 𝟎))}
    {c = foldᵣ(_⋅_)(1) (tail(map(n ↦ n ^ PrimePowers.power pp(n)) (PrimePowers.positive-powers pp)))}
    ([∨]-introₗ (divides-withᵣ-[^] ⦃ PrimePowers.powers-is-positive pp ⦄ (reflexivity(_∣_))))
  power-divide-product {pp}{i = 𝐒 i} = divides-with-[⋅]
    {b = (PrimePowers.positive-powers pp 𝟎) ^ (PrimePowers.power pp (PrimePowers.positive-powers pp 𝟎))}
    {c = foldᵣ(_⋅_)(1) (tail(map(n ↦ n ^ PrimePowers.power pp(n)) (PrimePowers.positive-powers pp)))}
    ([∨]-introᵣ {!!})
  -}

instance
  PrimePowers-equiv : Equiv(∃ PrimePowers)
  Equiv._≡_         PrimePowers-equiv = (_⊜_) on₂ [∃]-witness
  Equiv.equivalence PrimePowers-equiv = on₂-equivalence ⦃ Equiv.equivalence [⊜]-equiv ⦄

{-
-- Each positive number have a corresponding finite multiset of prime numbers such that it is equal to the product of the numbers in the multiset.
-- Examples:
--   n = (p₁ ^ n₁) ⋅ (p₂ ^ n₂) ⋅ … ⋅ (pₖ ^ nₖ)
-- Also called:
-- • Fundamental theorem of arithmetic.
-- • Canonical representation of positive integers by primes.
-- • Unique prime factorization theorem.
prime-representation : ∀{n} → ⦃ pos : Positive(n) ⦄ → ∃! ⦃ PrimePowers-equiv ⦄ (pp ↦ (n ≡ PrimePowers.product pp))
∃.witness (Tuple.left prime-representation) = {!!}
∃.proof (Tuple.left prime-representation) = {!!}
_⊜_.proof (Tuple.right (prime-representation {𝐒 n}) {pp1} {pp2} p1 p2) {p} = {!!}
-}

open import Logic.Classical
open import Numeral.Natural.Decidable
{-
prime-representation : ∀{n} → ⦃ pos : Positive(n) ⦄ → ∃! ⦃ PrimePowers-equiv ⦄ (pp ↦ (n ≡ PrimePowers.product([∃]-proof pp)))
prime-representation {𝐒 n} ⦃ pos ⦄ = [∧]-intro p1 (\{x}{y} → p2{x}{y}) where
  p1 : ∃(pp ↦ (𝐒(n) ≡ PrimePowers.product ([∃]-proof pp)))
  p2 : Unique(pp ↦ (𝐒(n) ≡ PrimePowers.product ([∃]-proof pp)))
  p2 {[∃]-intro x ⦃ ppx ⦄}{[∃]-intro y ⦃ ppy ⦄} px py with PrimePowers.positive-powers ppx | PrimePowers.positive-powers ppy
  p2 {[∃]-intro x ⦃ ppx ⦄} {[∃]-intro y ⦃ ppy ⦄} px py | intro 𝟎 b | intro 𝟎 d = intro {!!}
  p2 {[∃]-intro x ⦃ ppx ⦄} {[∃]-intro y ⦃ ppy ⦄} px py | intro 𝟎 b | intro (𝐒 c) d = {!!}
  p2 {[∃]-intro x ⦃ ppx ⦄} {[∃]-intro y ⦃ ppy ⦄} px py | intro (𝐒 a) b | intro 𝟎 d = {!!}
  p2 {[∃]-intro x ⦃ ppx ⦄} {[∃]-intro y ⦃ ppy ⦄} px py | intro (𝐒 a) b | intro (𝐒 c) d = {!!}
--    let xy = symmetry(_≡_) px 🝖 py
--    in intro \{p} → {!PrimePowers.power-divide-product ppx!}
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some defined operations over Rings
------------------------------------------------------------------------

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

-- This module gives the definition of _^_ which is used throughout
-- the library. It's a little different from the normal definition:
--
--   x ^ zero  = 1#
--   x ^ suc i = x * x ^ i
--
-- This is for two reasons. First, we want to avoid unnecessarily
-- multiplying by 1# if possible:
--
--     Standard definition: x ^ 2 = x * x * 1#
--     Our definition:      x ^ 2 = x * x
--
-- This speeds up typechecking and makes for much more readable
-- proofs.
--
-- Secondly, we want to associate to the left:
--
--     Standard definition: x ^ 3 = x * (x * (x * 1#))
--     Our definition:      x ^ 2 = (x * x) * x
--
-- As counterintuitive as it may seem, this also speeds up
-- typechecking.

open import Algebra

module Algebra.Operations.Ring
  {ℓ₁ ℓ₂} (ring : RawRing ℓ₁ ℓ₂)
  where

open import Data.Nat.Base as ℕ using (ℕ; suc; zero)

open RawRing ring

infixr 8 _^_+1
_^_+1 : Carrier → ℕ → Carrier
x ^ zero  +1 = x
x ^ suc n +1 = (x ^ n +1) * x

infixr 8 _^_
_^_ : Carrier → ℕ → Carrier
x ^ zero  = 1#
x ^ suc i = x ^ i +1
{-# INLINE _^_ #-}

ext: agda


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap as KVMap
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types.EpochIndep
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId

-- This module defines the types that depend on an EpochConfig,
-- but never inspect it. Consequently, we define everyting over
-- an abstract 𝓔 passed around as a module parameter.
--
-- Importantly, though, we are connecting abstract and concrete
-- votes by defining what constitutes enough "evidence" that a
-- vote was cast, which is passed around in the abstract model as
-- the variable (𝓥 : VoteEvidence); here we instantiate it to
-- 'ConcreteVoteEvidence'.
--
-- TODO-3: update types to reflect more recent version of LibraBFT.
-- This is a substantial undertaking that should probably be led by
-- someone who can access our internal implementation.
--
-- TODO-4: Make the Optics.Reflection stuff work with record
-- parameters, so we can merge all modules back into Types.  For
-- now, this is the easiest way to avoid the issue that making a
-- module inside Consensus.Types called EpochDep will break
-- mkLens (not sure why).

module LibraBFT.Impl.Consensus.Types.EpochDep (𝓔 : EpochConfig) where
  open EpochConfig 𝓔
  open WithAbsVote 𝓔

  -- A 'ConcreteVoteEvidence' is a piece of information that
  -- captures that the 'vd : AbsVoteData' in question was not /invented/
  -- but instead, comes from a concrete vote that is /valid/ (that is,
  -- signature has been checked and author belongs to this epoch).
  --
  -- Moreover, we will also store the RecordChain that leads to the vote;
  -- this requires some mutually-recursive shenanigans, so we first declare
  -- ConcreteVoteEvidence, then import the necessary modules, and then define it.
  record ConcreteVoteEvidence (vd : AbsVoteData) : Set

  open import LibraBFT.Abstract.Abstract UID _≟UID_ NodeId 𝓔 ConcreteVoteEvidence as Abs hiding (qcVotes; Vote)

  data VoteCoherence (v : Vote) (b : Abs.Block) : Set where
    initial  : v ^∙ vParentId    ≡ genesisUID
             → v ^∙ vParentRound ≡ 0
             → Abs.bPrevQC b     ≡ nothing
             → VoteCoherence v b

    ¬initial : ∀{b' q}
             → v ^∙ vParentId    ≢ genesisUID
             → v ^∙ vParentRound ≢ 0
             → v ^∙ vParentId    ≡ Abs.bId b'
             → v ^∙ vParentRound ≡ Abs.bRound b'
             → (Abs.B b') ← (Abs.Q q)
             → (Abs.Q q)  ← (Abs.B b)
             → VoteCoherence v b

  -- Estabilishing validity of a concrete vote involves checking:
  --
  --   i) Vote author belongs to the current epoch
  --  ii) Vote signature is correctly verified
  -- iii) Existence of a RecordChain up to the voted-for block.
  --  iv) Coherence of 'vdParent' field with the above record chain.
  --
  record IsValidVote (v : Vote) : Set where
    constructor IsValidVote∙new
    inductive
    field
      ₋ivvMember   : Member
      ₋ivvAuthor   : isMember? (₋vAuthor v) ≡ just ₋ivvMember
      ₋ivvSigned   : WithVerSig (getPubKey ₋ivvMember) v

      ₋ivvVDhash   : v ^∙ vLedgerInfo ∙ liConsensusDataHash ≡ hashVD (v ^∙ vVoteData)

      -- A valid vote must vote for a block that exists and is
      -- inserted in a RecordChain.
      ₋ivvBlock    : Abs.Block
      ₋ivvBlockId  : v ^∙ vProposedId ≡ Abs.bId ₋ivvBlock

      -- Moreover; we must check that the 'parent' field of the vote is coherent.
      ₋ivvCoherent : VoteCoherence v ₋ivvBlock

      -- Finally, the vote is for the correct epoch
      ₋ivvEpoch    : v ^∙ vEpoch ≡ epoch
      ₋ivvEpoch2   : v ^∙ vParent ∙ biEpoch ≡ epoch  -- Not needed?
  open IsValidVote public

  -- A valid vote can be directly mapped to an AbsVoteData. Abstraction of QCs
  -- and blocks will be given in LibraBFT.Concrete.Records, since those are
  -- more involved functions.
  α-ValidVote : (v : Vote) → Member → AbsVoteData
  α-ValidVote v mbr = AbsVoteData∙new (v ^∙ vProposed ∙ biRound)
                                      mbr
                                      (v ^∙ vProposed ∙ biId)

  -- α-ValidVote is the same for two votes that have the same vAuthor, vdProposed and vOrder
  α-ValidVote-≡ : ∀ {cv v'} {m : Member}
                → ₋vdProposed (₋vVoteData cv) ≡ ₋vdProposed (₋vVoteData v')
                → α-ValidVote cv m ≡ α-ValidVote v' m
  α-ValidVote-≡ {cv} {v'} prop≡ =
    AbsVoteData-η (cong ₋biRound prop≡) refl (cong ₋biId prop≡)

  -- Finally; evidence for some abstract vote consists of a concrete valid vote
  -- that is coherent with the abstract vote data.
  record ConcreteVoteEvidence vd where
    constructor CVE∙new
    inductive
    field
      ₋cveVote        : Vote
      ₋cveIsValidVote : IsValidVote ₋cveVote
      ₋cveIsAbs       : α-ValidVote ₋cveVote (₋ivvMember ₋cveIsValidVote) ≡ vd
  open ConcreteVoteEvidence public

  -- Gets the signature of a concrete vote evidence
  ₋cveSignature : ∀{vd} → ConcreteVoteEvidence vd → Signature
  ₋cveSignature = ₋vSignature ∘ ₋cveVote

  -- A valid quorum certificate contains a collection of valid votes, such that
  -- the members represented by those votes (which exist because the votes are valid)
  -- constitutes a quorum.
  record MetaIsValidQC (qc : QuorumCert) : Set where
    field
      ₋ivqcMetaVotesValid      : All (IsValidVote ∘ rebuildVote qc) (qcVotes qc)
      ₋ivqcMetaIsQuorum        : IsQuorum (All-reduce ₋ivvMember ₋ivqcMetaVotesValid)
  open MetaIsValidQC public

  vqcMember : (qc : QuorumCert) → MetaIsValidQC qc
             → ∀ {as} → as ∈ qcVotes qc → Member
  vqcMember qc v {α , _ , _} as∈qc with All-lookup (₋ivqcMetaVotesValid v) as∈qc
  ...| prf = ₋ivvMember prf

  -- A block tree depends on a epoch config but works regardlesss of which
  -- EpochConfig we have.
  record BlockTree : Set where
    constructor BlockTree∙new
    field
      ₋btIdToBlock               : KVMap HashValue LinkableBlock
      ₋btRootId                  : HashValue
      ₋btHighestCertifiedBlockId : HashValue
      ₋btHighestQuorumCert       : QuorumCert
      -- btHighestTimeoutCert      : Maybe TimeoutCertificate
      ₋btHighestCommitCert       : QuorumCert
      ₋btPendingVotes            : PendingVotes
      ₋btPrunedBlockIds          : List HashValue
      ₋btMaxPrunedBlocksInMem    : ℕ
      ₋btIdToQuorumCert          : KVMap HashValue (Σ QuorumCert MetaIsValidQC)
  open BlockTree public
  unquoteDecl btIdToBlock   btRootId   btHighestCertifiedBlockId   btHighestQuorumCert
              btHighestCommitCert   btPendingVotes   btPrunedBlockIds
              btMaxPrunedBlocksInMem btIdToQuorumCert = mkLens (quote BlockTree)
             (btIdToBlock ∷ btRootId ∷ btHighestCertifiedBlockId ∷ btHighestQuorumCert ∷
              btHighestCommitCert ∷ btPendingVotes ∷ btPrunedBlockIds ∷
              btMaxPrunedBlocksInMem ∷ btIdToQuorumCert ∷ [])

  record BlockStore : Set where
    constructor BlockStore∙new
    field
      ₋bsInner         : BlockTree
      -- bsStateComputer : StateComputer
      -- bsStorage       : CBPersistentStorage
  open BlockStore public
  unquoteDecl bsInner = mkLens (quote BlockStore)
             (bsInner ∷ [])

  -- These are the parts of the RoundManager that depend on an
  -- EpochConfig. We do not particularly care which EpochConfig
  -- they care about yet.
  --
  record RoundManagerWithEC : Set where
    constructor RoundManagerWithEC∙new
    field
      ₋epBlockStore   : BlockStore
  open RoundManagerWithEC public
  unquoteDecl epBlockStore = mkLens (quote RoundManagerWithEC)
    (epBlockStore ∷ [])

  lBlockTree : Lens RoundManagerWithEC BlockTree
  lBlockTree = epBlockStore ∙ bsInner

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Plain.Models where

open import Data.Nat
open import Plain.Terms

-- The (complete) Herbrand universe for Σ
U' : {n : ℕ} → (Signature n) → Set
U' Σ = GTerm Σ

open import Relation.Unary as U
open import Level

-- a (complete) Herbrand interpretation
record Interp {n : ℕ} (Σ : Signature n) : Set₁ where
  field
    Carrier : Pred (U' Σ) Level.zero
open Interp

_∩ᵢ_ : {n : ℕ} → {Σ : Signature n} → Interp Σ → Interp Σ
  → Interp Σ
i₁ ∩ᵢ i₂ = record { Carrier = (Carrier i₁) U.∩ Carrier i₂ }

_∪ᵢ_ : {n : ℕ} → {Σ : Signature n} → Interp Σ → Interp Σ
  → Interp Σ
i₁ ∪ᵢ i₂ = record { Carrier = (Carrier i₁) U.∪ Carrier i₂ }

open import Data.List as L
open import Data.List.All as LAl
open import Data.List.Any as LAn
open import Relation.Binary.Core

open Program

-- | Inductive model property
record IsIndModel {n : ℕ}
  {Σ : Signature n} (i : Interp Σ) (P : Program Σ) : Set₂ where
  field
    forwClosed :
      (bs' : List (GTerm Σ))
      → All (λ b → b ∈ Carrier i) bs'
      → (σ : GSubst Σ)
      → (a : Term Σ Var)
      → (bs : List (Term Σ Var))
      → Any (λ cl → cl ≡ (a :- bs)) (prg P)
      → (L.map (app σ) bs) ≡ bs'
      → (app σ a ∈ Carrier i)
open IsIndModel

-- | Ind Model
record IndModel {n : ℕ}
  {Σ : Signature n} (P : Program Σ) : Set₂ where
  field
    iInterp : Interp Σ
    isIndModel : IsIndModel iInterp P

open IndModel

open import Data.Product
open import Data.List.All.Properties -- using (All-map)

{-
-- | Model intersection
_∩m_ : {n : ℕ} → {Σ : Signature n} → {P : Program Σ}
  → (m₁ : IndModel P) → (m₂ : IndModel P)
  → IndModel P
_∩m_ {n} {Σ} {P} m₁ m₂ = record
  { interp = interp m₁ ∩ᵢ interp m₂
  ; isIndModel = prop-model-intersection-pair P m₁ m₂ }
-}

⋂ᵢ : {n : ℕ} → {Σ : Signature n} →
  (I : Set) → (I → Interp Σ)
  → Interp Σ
⋂ᵢ I f = record { Carrier = ⋂ I (λ i t → t ∈ Carrier (f i)) }

open import Function

prop-model-intersection : {n : ℕ} → {Σ : Signature n} →
  (P : Program Σ)
  → (I : Set) -- ^ is non-empty by what argument?
  → (mps : I → IndModel P)
  → IsIndModel ( ⋂ᵢ I (iInterp ∘ mps)) P
prop-model-intersection P I mps =
  record { forwClosed = λ bs' pbs' σ a bs pcl pbs i →
    forwClosed (isIndModel (mps i)) bs'
      (LAl.map (λ k → k i) pbs')
      σ a bs pcl pbs
    }

-- | Coinductive model
record IsCoiModel {n : ℕ}
  {Σ : Signature n} (i : Interp Σ) (P : Program Σ) : Set₂ where
  field
    backClosed :
      {a : Term Σ Var} → {bs : List (Term Σ Var)}
      → (a' : GTerm Σ)
      → a' ∈ Carrier i
      → ∃ (λ (σclsp : GSubst Σ ×
        Any (λ c → a :- bs ≡ c) (prg P))
      → app (proj₁ σclsp) a ≡ a'
      → All (λ c → c ∈ Carrier i) (L.map (app (proj₁ σclsp)) bs))
open IsCoiModel

-- | Coi Model
record CoiModel {n : ℕ}
  {Σ : Signature n} (P : Program Σ) : Set₂ where
  field
    cInterp : Interp Σ
    isCoiModel : IsCoiModel cInterp P

open CoiModel

⋃ᵢ : {n : ℕ} → {Σ : Signature n} →
  (I : Set) → (I → Interp Σ)
  → Interp Σ
⋃ᵢ I f = record { Carrier = λ x → ⋃ I (λ i t → t ∈ Carrier (f i)) x }

open import Data.Product as DP

-- | model union property
prop-model-union : {n : ℕ} → {Σ : Signature n} →
  (P : Program Σ)
  → (I : Set) -- ^ is non-empty by what argument?
  → (mps : I → CoiModel P)
  → IsCoiModel ( ⋃ᵢ I (cInterp ∘ mps)) P
prop-model-union P I mps =
  record { backClosed = λ a' x →
    DP.map (λ id → id)
           (λ x₂ x₃ → LAl.map (λ x₄ → proj₁ x , x₄) (x₂ x₃))
           (backClosed (isCoiModel (mps (proj₁ x))) a' (proj₂ x)) }

open import Data.Unit

prop-ex-ind-model : {n : ℕ} → {Σ : Signature n}
  → (P : Program Σ)
  → IndModel P
prop-ex-ind-model P = record
  { iInterp = record { Carrier = U }
  ; isIndModel = record { forwClosed = λ bs' x σ a bs x₁ x₂ → tt }
  }

open import Data.Empty

prop-ex-coi-model : {n : ℕ} → {Σ : Signature n}
  → (P : Program Σ)
  → CoiModel P
prop-ex-coi-model P = record
  { cInterp = record { Carrier = ∅ }
  ; isCoiModel = record { backClosed = λ a' () }
  }

max_stars_repo_name: frantisekfarka/lp-mod

max_issues_repo_name: frantisekfarka/lp-mod

max_forks_repo_name: frantisekfarka/lp-mod


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Data.Product using (∃; ∃-syntax; _,_)

data even : ℕ → Set
data odd  : ℕ → Set

data even where
  even-zero : even zero
  even-suc  : ∀ {n : ℕ} → odd n → even (suc n)

data odd where
  odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)

lemma : ∀ (m : ℕ) → 2 * suc m ≡ suc (suc (2 * m))
lemma m =
  begin
    2 * suc m
  ≡⟨⟩
    suc m + (suc m + zero)
  ≡⟨⟩
    suc (m + (suc (m + zero)))
  ≡⟨ cong suc (+-suc m (m + zero)) ⟩
    suc (suc (m + (m + zero)))
  ≡⟨⟩
    suc (suc (2 * m))
  ∎

∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (2 * m ≡ n)
∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + 2 * m ≡ n)

∃-even even-zero =  zero , refl
∃-even (even-suc o) with ∃-odd o
...                    | m , refl = suc m , lemma m

∃-odd  (odd-suc e)  with ∃-even e
...                    | m , refl = m , refl

∃-even′ : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ 2 * m)
∃-odd′  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + 2 * m)

∃-even′ even-zero =  zero , refl
∃-even′ (even-suc o) with ∃-odd′ o
...                     | m , eqn rewrite eqn | +-suc m (m + 0) = suc m , {!!}

∃-odd′  (odd-suc e)  with ∃-even′ e
...                     | m , eqn rewrite eqn = m , refl

data Even : ℕ → Set where
  ev0 : Even zero
  ev2 : ∀ {n} → Even n → Even (suc (suc n))

ev-ex : ∀ {n : ℕ} → Even n → ∃[ m ] (2 * m ≡ n)
ev-ex ev0 =  (zero , refl)
ev-ex (ev2 ev) with ev-ex ev
... | (m , refl) = (suc m , lemma m)


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

case_of_ : {A B : Set} → A → (A → B) → B
case x of f = f x

data D : Set where
  c : D → D

postulate
  d : D
  A : Set
  P : A → Set

record R : Set where
  no-eta-equality
  field
    f : A

  -- R : Set
  -- Rf : R → A

data Box : Set where
  box : R → Box

postulate
  f : D → Box

-- pat-lam : Box → A
-- pat-lam (box y) = R.f y

g : D → A
g x = case f x of λ
  { (box y) → R.f y
  }

postulate B : Set

p : P (g (c d))
p with B
p | z = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Definition.Typed.Decidable where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Consequences.Syntactic
open import Definition.Conversion
open import Definition.Conversion.Decidable
open import Definition.Conversion.Soundness
open import Definition.Conversion.Stability
open import Definition.Conversion.Consequences.Completeness

open import Tools.Nullary
open import Tools.Product

-- Decidability of conversion of well-formed types
dec : ∀ {A B r Γ} → Γ ⊢ A ^ r → Γ ⊢ B ^ r → Dec (Γ ⊢ A ≡ B ^ r)
dec ⊢A ⊢B =
  let ⊢Γ≡Γ = reflConEq (wf ⊢A)
  in  map soundnessConv↑ completeEq
          (decConv↑ ⊢Γ≡Γ (completeEq (refl ⊢A)) (completeEq (refl ⊢B)))

-- Decidability of conversion of well-formed terms
decTerm : ∀ {t u A r Γ} → Γ ⊢ t ∷ A ^ r → Γ ⊢ u ∷ A ^ r → Dec (Γ ⊢ t ≡ u ∷ A ^ r)
decTerm {r = [ ! , l ]} ⊢t ⊢u =
  let ⊢Γ≡Γ = reflConEq (wfTerm ⊢t)
  in  map soundnessConv↑Term completeEqTerm
          (decConv↑TermConv ⊢Γ≡Γ (refl (syntacticTerm ⊢t)) (completeEqTerm (genRefl ⊢t)) (completeEqTerm (genRefl ⊢u)))
decTerm {r = [ % , l ]} ⊢t ⊢u =
  let ⊢Γ≡Γ = reflConEq (wfTerm ⊢t)
  in  map (λ x → proj₂ (proj₂ (soundness~↑% x))) completeEqTerm
          (decConv↑TermConv ⊢Γ≡Γ (refl (syntacticTerm ⊢t)) (completeEqTerm (genRefl ⊢t)) (completeEqTerm (genRefl ⊢u)))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
open import Relation.Binary using (IsDecEquivalence)
open import Agda.Builtin.Equality

-- module UnifyMguFTerminationHunt (FunctionName : Set) ⦃ isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName}) ⦄ where

module UnifyMguFTerminationHunt where

postulate
  FunctionName : Set
  instance isDecEquivalenceA : IsDecEquivalence (_≡_ {A = FunctionName})

open IsDecEquivalence isDecEquivalenceA using () renaming (_≟_ to _≟F_)

open import UnifyTermF FunctionName

open import Data.Product using (∃; _,_)
open import Data.Maybe using (Maybe; just; nothing)
open import Category.Monad using (RawMonad)
import Level
open RawMonad (Data.Maybe.monad {Level.zero})
open import Relation.Nullary using (Dec; yes; no)

open import Data.Fin using (Fin)
open import Data.Nat using (suc)
postulate
  _◃′_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
  _for'_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) -> Fin (suc n) -> Term n

amterm : ∀ {m} (s t : Term m) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))
amterm leaf leaf acc = just acc
amterm leaf (function _ _) acc = nothing
amterm leaf (s' fork t') acc = nothing
amterm (s' fork t') leaf acc = nothing
amterm (s' fork t') (function _ _) acc = nothing
amterm (s1 fork s2) (t1 fork t2) acc = amterm s2 t2 =<< amterm s1 t1 acc {- Data.Maybe.maybe (⋆amgu.amgu ⋆amguTerm' s2 t2) nothing (⋆amgu.amgu ⋆amguTerm' s1 t1 acc) -}
amterm (function fn₁ ts₁) leaf acc = nothing
amterm (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc = nothing
amterm (function fn₁ ts₁) (_ fork _) acc = nothing
amterm (i x) (i y) (m , anil) = nothing
amterm (i x) t     (m , anil) = nothing
amterm t     (i x) (m , anil) = nothing
amterm s     t  (n , σ asnoc r / z) =
         (λ σ -> σ ∃asnoc r / z) <$>
           -- amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)
           amterm ((r for' z) ◃′ s) ((r for' z) ◃′ t) (n , σ)

-- instance ⋆amguTerm' : ⋆amgu Term
-- ⋆amguTerm' .⋆amgu.amgu leaf leaf acc = just acc
-- ⋆amguTerm' .⋆amgu.amgu leaf (function _ _) acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu leaf (s' fork t') acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu (s' fork t') leaf acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu (s' fork t') (function _ _) acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu (s1 fork s2) (t1 fork t2) acc = amgu s2 t2 =<< amgu s1 t1 acc {- Data.Maybe.maybe (⋆amgu.amgu ⋆amguTerm' s2 t2) nothing (⋆amgu.amgu ⋆amguTerm' s1 t1 acc) -}
-- ⋆amguTerm' .⋆amgu.amgu (function fn₁ ts₁) leaf acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu (function fn₁ ts₁) (_ fork _) acc = nothing
-- ⋆amguTerm' .⋆amgu.amgu (i x) (i y) (m , anil) = nothing
-- ⋆amguTerm' .⋆amgu.amgu (i x) t     (m , anil) = nothing
-- ⋆amguTerm' .⋆amgu.amgu t     (i x) (m , anil) = nothing
-- ⋆amguTerm' .⋆amgu.amgu s     t  (n , σ asnoc r / z) =
--          (λ σ -> σ ∃asnoc r / z) <$>
--            -- amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)
--            amgu ((r for z) ◃′ s) ((r for z) ◃′ t) (n , σ)

-- -- instance ⋆amguTerm' : ⋆amgu Term
-- -- ⋆amgu.amgu ⋆amguTerm' leaf leaf acc = just acc
-- -- ⋆amgu.amgu ⋆amguTerm' leaf (function _ _) acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' leaf (s' fork t') acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (s' fork t') leaf acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (s' fork t') (function _ _) acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (s1 fork s2) (t1 fork t2) acc = {!amgu s2 t2 =<< amgu s1 t1 acc!} {- Data.Maybe.maybe (⋆amgu.amgu ⋆amguTerm' s2 t2) nothing (⋆amgu.amgu ⋆amguTerm' s1 t1 acc) -}
-- -- ⋆amgu.amgu ⋆amguTerm' (function fn₁ ts₁) leaf acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (function fn₁ ts₁) (_ fork _) acc = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (i x) (i y) (m , anil) = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' (i x) t     (m , anil) = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' t     (i x) (m , anil) = nothing
-- -- ⋆amgu.amgu ⋆amguTerm' s     t  (n , σ asnoc r / z) =
-- --          (λ σ -> σ ∃asnoc r / z) <$>
-- --            -- amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)
-- --            amgu ((r for z) ◃′ s) ((r for z) ◃′ t) (n , σ)

-- -- -- mutual

-- -- --   instance ⋆amguTerm : ⋆amgu Term
-- -- --   ⋆amgu.amgu ⋆amguTerm leaf leaf acc = just acc
-- -- --   ⋆amgu.amgu ⋆amguTerm leaf (function _ _) acc = nothing
-- -- --   ⋆amgu.amgu ⋆amguTerm leaf (s' fork t') acc = nothing
-- -- --   ⋆amgu.amgu ⋆amguTerm (s' fork t') leaf acc = nothing
-- -- --   ⋆amgu.amgu ⋆amguTerm (s' fork t') (function _ _) acc = nothing
-- -- --   ⋆amgu.amgu ⋆amguTerm (s1 fork s2) (t1 fork t2) acc =
-- -- --                     amgu s2 t2 =<< amgu s1 t1 acc
-- -- --   ⋆amgu.amgu ⋆amguTerm (function fn₁ ts₁) leaf acc = nothing
-- -- --   ⋆amgu.amgu ⋆amguTerm (function fn₁ {n₁} ts₁) (function fn₂ {n₂} ts₂) acc
-- -- --    with fn₁ ≟F fn₂
-- -- --   … | no _ = nothing
-- -- --   … | yes _ with n₁ ≟ n₂
-- -- --   … | no _ = nothing
-- -- --   … | yes refl = amgu ts₁ ts₂ acc
-- -- --   ⋆amgu.amgu ⋆amguTerm (function fn₁ ts₁) (_ fork _) acc = nothing
-- -- --   ⋆amgu.amgu ⋆amguTerm (i x) (i y) (m , anil) = just (flexFlex x y)
-- -- --   ⋆amgu.amgu ⋆amguTerm (i x) t     (m , anil) = flexRigid x t
-- -- --   ⋆amgu.amgu ⋆amguTerm t     (i x) (m , anil) = flexRigid x t
-- -- --   ⋆amgu.amgu ⋆amguTerm s     t  (n , σ asnoc r / z) =
-- -- --            (λ σ -> σ ∃asnoc r / z) <$>
-- -- --              amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)

-- -- --   instance ⋆amguVecTerm : ∀ {N} → ⋆amgu (flip Vec N ∘ Term)
-- -- --   ⋆amgu.amgu ⋆amguVecTerm [] [] acc = just acc
-- -- --   ⋆amgu.amgu ⋆amguVecTerm (t₁ ∷ t₁s) (t₂ ∷ t₂s) acc = amgu t₁s t₂s =<< amgu t₁ t₂ acc

-- -- -- mgu : ∀ {m} -> (s t : Term m) -> Maybe (∃ (AList m))
-- -- -- mgu {m} s t = amgu s t (m , anil)


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

module SEquivSCPermEquiv where

open import Level        using (Level; _⊔_)
open import Data.Fin     using (Fin)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec     using (tabulate)
open import Function     using (_∘_; id)

open import Data.Vec.Properties using    (lookup∘tabulate)
open import Relation.Binary     using    (Setoid)
open import Function.Equality   using    (_⟨$⟩_; _⟶_)
                                renaming (_∘_ to _⊚_)

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)

--

open import Proofs using (_!!_; finext)
open import Equiv using (_≃_; qinv; module isqinv)
open import EquivEquiv using (_S≃_; eq; _≋_; id≋)
open import ConcretePermutation using (CPerm; cp; _∘̂_; 1C; cauchyext; SCPerm)
open import ConcretePermutationProperties using (p≡)

--

infix 4 _≃S_

------------------------------------------------------------------------------
-- The big (semantic) theorem!

-- On one side we have the setoid of permutations under ≡
-- On the other we have the setoid of equivalences under ≋
--
-- The regular equivalence ≃ relates sets. To relate the above two
-- setoids, this regular equivalence is generalized to an equivalence
-- ≃S that relates setoids each with its own equivalence relation.

record _≃S_ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} (A : Setoid ℓ₁ ℓ₂) (B : Setoid ℓ₃ ℓ₄) :
  Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  constructor equiv
  field
    f : A ⟶ B
    g : B ⟶ A
    α : ∀ {x y} → Setoid._≈_ B x y → Setoid._≈_ B ((f ⊚ g) ⟨$⟩ x) y
    β : ∀ {x y} → Setoid._≈_ A x y → Setoid._≈_ A ((g ⊚ f) ⟨$⟩ x) y

-- Big theorem

univalence : ∀ {m n} → (SCPerm m n) ≃S (Fin m S≃ Fin n)
univalence {m} {n} = equiv fwd bwd α β
  where

    fwd' : (CPerm m n) → (Fin m ≃ Fin n)
    fwd' (cp π πᵒ αp βp) =
      (λ m → πᵒ !! m) ,
      let index = (λ n → π !! n) in qinv index pf₁ pf₂
      where
        open ≡-Reasoning
        pf₁ : ∀ m → πᵒ !! (π !! m) ≡ m
        pf₁ m = begin (
          πᵒ !! (π !! m)
            ≡⟨ sym (lookup∘tabulate (λ x → πᵒ !! (π !! x)) m) ⟩
          (π ∘̂ πᵒ) !! m
            ≡⟨ cong (λ x → x !! m) αp ⟩
          1C !! m
            ≡⟨ lookup∘tabulate id m ⟩
          m ∎)
        pf₂ : ∀ m → π !! (πᵒ !! m) ≡ m
        pf₂ m = begin (
          π !! (πᵒ !! m)
            ≡⟨ sym (lookup∘tabulate (λ x → π !! (πᵒ !! x)) m) ⟩
          (πᵒ ∘̂ π) !! m
            ≡⟨ cong (λ x → x !! m) βp ⟩
          1C !! m
            ≡⟨ lookup∘tabulate id m ⟩
          m ∎)

    bwd' : (Fin m ≃ Fin n) → (CPerm m n)
    bwd' (f , qinv g α β) =
      cp (tabulate g) (tabulate f) g∘̂f≡1C f∘̂g≡1C
      where
       open ≡-Reasoning
       g∘̂f≡1C : tabulate g ∘̂ tabulate f ≡ 1C
       g∘̂f≡1C = finext (λ i → begin (
         tabulate f !! (tabulate g !! i)
           ≡⟨ lookup∘tabulate f (tabulate g !! i) ⟩
         f (tabulate g !! i)
           ≡⟨ cong f (lookup∘tabulate g i) ⟩
         f (g i)
           ≡⟨ α i ⟩
         i ∎))
       f∘̂g≡1C : tabulate f ∘̂ tabulate g ≡ 1C
       f∘̂g≡1C = finext (λ i → begin (
         tabulate g !! (tabulate f !! i)
           ≡⟨ lookup∘tabulate g (tabulate f !! i) ⟩
         g (tabulate f !! i)
           ≡⟨ cong g (lookup∘tabulate f i) ⟩
         g (f i)
           ≡⟨ β i ⟩
         i ∎))

    fwd : (SCPerm m n) ⟶ (Fin m S≃ Fin n)
    fwd = record
      { _⟨$⟩_ = fwd'
      ; cong = λ { {π} {.π} refl → id≋ }
      }

    bwd : (Fin m S≃ Fin n) ⟶ (SCPerm m n)
    bwd = record
      { _⟨$⟩_ = bwd'
      ; cong = λ eq₁≋eq₂ → p≡ (finext (_≋_.g≡ eq₁≋eq₂))
      }

    α : {eq₁ eq₂ : Fin m ≃ Fin n} → eq₁ ≋ eq₂ → (fwd ⊚ bwd ⟨$⟩ eq₁) ≋ eq₂
    α {eq₁} {eq₂} eq₁≋eq₂ =
      eq (λ x → trans (lookup∘tabulate (proj₁ eq₁) x) (_≋_.f≡ eq₁≋eq₂ x))
         (λ x → trans (lookup∘tabulate (isqinv.g (proj₂ eq₁)) x) (_≋_.g≡ eq₁≋eq₂ x))

    β : {π₁ π₂ : CPerm m n} → π₁ ≡ π₂ → (bwd ⊚ fwd ⟨$⟩ π₁) ≡ π₂
    β {π} {.π} refl = p≡ (cauchyext (CPerm.π π))

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Base

{-
    This file contains the lemma that
    a point (1 -> A) has n-connected fibers
    if A is (S n)-connected.

    The other direction will be added whenever
    it is needed.
-}

module Homotopy.PointConnected {i} (A : Set i) (a : A) where

  open import Homotopy.Connected
  open import Homotopy.Truncation
  open import Homotopy.PathTruncation

  point : unit {i} → A
  point _ = a

  abstract
    point-has-connected-fibers : ∀ {n} →
      is-connected (S n) A → has-connected-fibers n point
    point-has-connected-fibers {n} A-is-conn a₂ = center [a≡a₂]n , path
      where
        [a≡a₂]n : τ n (a ≡ a₂)
        [a≡a₂]n = connected-has-all-τ-paths A-is-conn a a₂

        center : τ n (a ≡ a₂) → τ n (hfiber point a₂)
        center = τ-extend-nondep ⦃ τ-is-truncated n _ ⦄
          (λ shift → proj $ tt , shift)

        path′ : ∀ f → proj f ≡ center [a≡a₂]n
        path′ (tt , a≡a₂) = ap center $ contr-has-all-paths
          (connected-has-connected-paths A-is-conn a a₂) (proj a≡a₂) [a≡a₂]n

        path : ∀ f → f ≡ center [a≡a₂]n
        path = τ-extend ⦃ λ _ → ≡-is-truncated n $ τ-is-truncated n _ ⦄ path′

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic structures
------------------------------------------------------------------------

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

open import Relation.Binary.Core

module Algebra.Morphism.Structures where

open import Algebra.Core
open import Algebra.Bundles
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Level using (Level; _⊔_)
import Function.Definitions as FunctionDefinitions
open import Relation.Binary.Morphism.Structures

private
  variable
    a b ℓ₁ ℓ₂ : Level

------------------------------------------------------------------------
-- Morphisms over magma-like structures
------------------------------------------------------------------------

module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) where

  open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
  open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
  open MorphismDefinitions A B _≈₂_
  open FunctionDefinitions _≈₁_ _≈₂_

  record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
      homo              : Homomorphic₂ ⟦_⟧ _∙_ _◦_

    open IsRelHomomorphism isRelHomomorphism public
      renaming (cong to ⟦⟧-cong)

  record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
      injective           : Injective ⟦_⟧

    open IsMagmaHomomorphism isMagmaHomomorphism public

    isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelMonomorphism = record
      { isHomomorphism = isRelHomomorphism
      ; injective      = injective
      }

  record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
      surjective          : Surjective ⟦_⟧

    open IsMagmaMonomorphism isMagmaMonomorphism public

    isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelIsomorphism = record
      { isMonomorphism = isRelMonomorphism
      ; surjective     = surjective
      }

------------------------------------------------------------------------
-- Morphisms over monoid-like structures
------------------------------------------------------------------------

module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) where

  open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
  open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
  open MorphismDefinitions A B _≈₂_
  open FunctionDefinitions _≈₁_ _≈₂_
  open MagmaMorphisms (RawMonoid.rawMagma M₁) (RawMonoid.rawMagma M₂)

  record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
      ε-homo              : Homomorphic₀ ⟦_⟧ ε₁ ε₂

    open IsMagmaHomomorphism isMagmaHomomorphism public

  record IsMonoidMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
      injective            : Injective ⟦_⟧

    open IsMonoidHomomorphism isMonoidHomomorphism public

    isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
    isMagmaMonomorphism = record
      { isMagmaHomomorphism = isMagmaHomomorphism
      ; injective           = injective
      }

    open IsMagmaMonomorphism isMagmaMonomorphism public
      using (isRelMonomorphism)

  record IsMonoidIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
      surjective           : Surjective ⟦_⟧

    open IsMonoidMonomorphism isMonoidMonomorphism public

    isMagmaIsomorphism : IsMagmaIsomorphism ⟦_⟧
    isMagmaIsomorphism = record
      { isMagmaMonomorphism = isMagmaMonomorphism
      ; surjective          = surjective
      }

    open IsMagmaIsomorphism isMagmaIsomorphism public
      using (isRelIsomorphism)

------------------------------------------------------------------------
-- Morphisms over group-like structures
------------------------------------------------------------------------

module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) where

  open RawGroup G₁ renaming
    (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
  open RawGroup G₂ renaming
    (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
  open MorphismDefinitions A B _≈₂_
  open FunctionDefinitions _≈₁_ _≈₂_
  open MagmaMorphisms (RawGroup.rawMagma G₁) (RawGroup.rawMagma G₂)
  open MonoidMorphisms (RawGroup.rawMonoid G₁) (RawGroup.rawMonoid G₂)

  record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
      ⁻¹-homo              : Homomorphic₁ ⟦_⟧ _⁻¹₁ _⁻¹₂

    open IsMonoidHomomorphism isMonoidHomomorphism public

  record IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
      injective           : Injective ⟦_⟧

    open IsGroupHomomorphism isGroupHomomorphism
      renaming (homo to ∙-homo) public

    isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
    isMonoidMonomorphism = record
      { isMonoidHomomorphism = isMonoidHomomorphism
      ; injective            = injective
      }

    open IsMonoidMonomorphism isMonoidMonomorphism public
      using (isRelMonomorphism)

  record IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧
      surjective          : Surjective ⟦_⟧

    open IsGroupMonomorphism isGroupMonomorphism public

    isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧
    isMonoidIsomorphism = record
      { isMonoidMonomorphism = isMonoidMonomorphism
      ; surjective           = surjective
      }

    open IsMonoidIsomorphism isMonoidIsomorphism public
      using (isRelIsomorphism)

------------------------------------------------------------------------
-- Morphisms over ring-like structures
------------------------------------------------------------------------

module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where

  open RawRing R₁ renaming
    ( Carrier to A; _≈_ to _≈₁_
    ; *-rawMonoid to *-rawMonoid₁
    ; +-rawGroup to +-rawGroup₁)

  open RawRing R₂ renaming
    ( Carrier to B; _≈_ to _≈₂_
    ; *-rawMonoid to *-rawMonoid₂
    ; +-rawGroup to +-rawGroup₂)

  module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂
  module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂

  open MorphismDefinitions A B _≈₂_
  open FunctionDefinitions _≈₁_ _≈₂_

  record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      +-isGroupHomomorphism  : +.IsGroupHomomorphism  ⟦_⟧
      *-isMonoidHomomorphism : *.IsMonoidHomomorphism ⟦_⟧

    open +.IsGroupHomomorphism +-isGroupHomomorphism renaming
      (homo to +-homo; ε-homo to 0#-homo) public

    open *.IsMonoidHomomorphism *-isMonoidHomomorphism renaming
      (homo to *-homo; ε-homo to 1#-homo) public

  record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isRingHomomorphism : IsRingHomomorphism ⟦_⟧
      injective          : Injective ⟦_⟧

    open IsRingHomomorphism isRingHomomorphism public

    +-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧
    +-isGroupMonomorphism = record
      { isGroupHomomorphism = +-isGroupHomomorphism
      ; injective           = injective
      }

    *-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧
    *-isMonoidMonomorphism = record
      { isMonoidHomomorphism = *-isMonoidHomomorphism
      ; injective            = injective
      }

    open *.IsMonoidMonomorphism *-isMonoidMonomorphism public
      using (isRelMonomorphism)

  record IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      isRingMonomorphism : IsRingMonomorphism ⟦_⟧
      surjective         : Surjective ⟦_⟧

    open IsRingMonomorphism isRingMonomorphism public

    +-isGroupIsomorphism : +.IsGroupIsomorphism ⟦_⟧
    +-isGroupIsomorphism = record
      { isGroupMonomorphism = +-isGroupMonomorphism
      ; surjective          = surjective
      }

    *-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧
    *-isMonoidIsomorphism = record
      { isMonoidMonomorphism = *-isMonoidMonomorphism
      ; surjective           = surjective
      }

    open *.IsMonoidIsomorphism *-isMonoidIsomorphism public
      using (isRelIsomorphism)

------------------------------------------------------------------------
-- Re-export contents of modules publicly

open MagmaMorphisms public
open MonoidMorphisms public
open GroupMorphisms public
open RingMorphisms public


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.SmashProduct.Base where

open import Cubical.Foundations.Prelude

-- This should be upstreamed to Basics when we develop some theory
-- about pointed types
ptType : Type₁
ptType = Σ[ A ∈ Type₀ ] A

pt : ∀ (A : ptType) → A .fst
pt A = A .snd

data Smash (A B : ptType) : Type₀ where
  basel : Smash A B
  baser : Smash A B
  proj  : (x : A .fst) → (y : B .fst) → Smash A B
  gluel : (a : A .fst) → proj a (pt B) ≡ basel
  gluer : (b : B .fst) → proj (pt A) b ≡ baser

-- Commutativity
comm : {A B : ptType} → Smash A B → Smash B A
comm basel       = baser
comm baser       = basel
comm (proj x y)  = proj y x
comm (gluel a i) = gluer a i
comm (gluer b i) = gluel b i

commK : ∀ {A B : ptType} → (x : Smash A B) → comm (comm x) ≡ x
commK basel       = refl
commK baser       = refl
commK (proj x y)  = refl
commK (gluel a x) = refl
commK (gluer b x) = refl

-- WIP below

SmashPt : (A B : ptType) → ptType
SmashPt A B = (Smash A B , basel)

-- -- A (B C) = C (B A) = C (A B) = (A B) C
-- rearrange : ∀ {A B C : ptType} → Smash A (SmashPt B C) → Smash C (SmashPt B A)
-- rearrange basel = baser
-- rearrange baser = basel
-- rearrange {B = B} {C = C} (proj x basel) = proj (C .snd) baser
-- rearrange {C = C} (proj x baser) = proj (C .snd) basel  -- ?
-- rearrange (proj x (proj y z)) = proj z (proj y x)
-- rearrange {C = C} (proj x (gluel a i)) = proj (C .snd) {!!}
-- rearrange (proj x (gluer b i)) = {!!}
-- rearrange (gluel a i) = {!!}
-- rearrange (gluer b i) = {!gluel ? i!}

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module ListThms where
open import Sec4
import Sec2

{-
  Definition of a list
-}
data List (A : Set) : Set where
  []  : List A                  -- Empty list
  _∷_ : A → List A → List A     -- Cons

infixr 4 _∷_

-- Proposition stating what is a non empty list
nelist : {A : Set} → (List A) → Prop
nelist [] = ⊥
nelist (x ∷ x₁) = ⊤

-- Head function that only works on non empty list
head : {A : Set} → (l : List A) → (p : nelist l) → A
head [] ()                      -- This can never happen
head (x ∷ _) ⋆ = x              -- This is the head of the list

-- The tail of the list only works on non empty list
tail : {A : Set} → (l : List A) → (p : nelist l) → (List A)
tail [] ()
tail (_ ∷ l) ⋆ = l

-- definition of a map
map : {A B : Set} → (A → B) → (List A) → List B
map f [] = []
map f (x ∷ l) = (f x) ∷ map f l

-- definition of fold left
fold : {A B : Set} → (A → B → B) → B → (List A) → B
fold f x [] = x
fold f x (x₁ ∷ l) = fold f (f x₁ x) l

-- reduce only works on lists of length > 0
reduce : {A : Set} → (l : List A) → (p : nelist l) → (A → A → A) → A
reduce [] ()
reduce (x ∷ l) _ f = fold f x l

-- length of a list
length : {A : Set} → (List A) → Sec2.ℕ
length [] = Sec2.Z
length (x ∷ l) = (Sec2.S Sec2.Z) Sec2.+ (length l)

-- Proposition on ≤
_<=_ : Sec2.ℕ  → Sec2.ℕ → Prop
Sec2.Z <= Sec2.Z = ⊤
Sec2.Z <= Sec2.S y = ⊤
Sec2.S x <= y = x <= y

_>=_ : Sec2.ℕ  → Sec2.ℕ → Prop
Sec2.Z >= Sec2.Z = ⊤
Sec2.Z >= Sec2.S y = ⊥
Sec2.S x >= y = x >= y

-- Indexing into the list
_!!_ : {A : Set} → ∀ (l : List A) → ∀ (i : Sec2.ℕ) → (nelist l)
                 → Exists A (λ _  → ((i >= Sec2.Z) ∧ (i <= (length l))))
([] !! i) ()
((x ∷ l) !! i) ⋆ = [ x , (and (lem1 i) (lem (x ∷ l) i))]
  where
  cong-<= : (x y : Sec2.ℕ) → (x <= y) → (x <= Sec2.S y)
  cong-<= Sec2.Z y p = ⋆
  cong-<= (Sec2.S x) Sec2.Z p = cong-<= x Sec2.Z p
  cong-<= (Sec2.S x) (Sec2.S y) p = cong-<= x (Sec2.S y) p

  lem1 : (i : Sec2.ℕ) → (i >= Sec2.Z)
  lem1 Sec2.Z = ⋆
  lem1 (Sec2.S i) = lem1 i

  lem2 : (i : Sec2.ℕ) → (i <= Sec2.Z)
  lem2 Sec2.Z = ⋆
  lem2 (Sec2.S i₁) = lem2 i₁

  lem : {A : Set} →  (l : List A) → (i : Sec2.ℕ) → (i <= (length l))
  lem [] Sec2.Z = ⋆
  lem [] (Sec2.S i) = lem2 i
  lem (x₁ ∷ l₁) i = cong-<= i (length l₁) (lem l₁ i)

data Maybe (A : Set) : Set where
  Nothing : Maybe A
  Just : A → Maybe A

index : {A : Set} → ∀ (l : List A)
                  → (nelist l)
                  → ∀ (i : Sec2.ℕ)
                  → Sec2.So ((i Sec2.≥ Sec2.Z) Sec2.& (i Sec2.< (length l)))
                  → Maybe A
index l _ i _ = index' l i (Sec2.Z)
  where
  index' : {A : Set} → ∀ (l : List A) → ∀(i : Sec2.ℕ)
                     → (c : Sec2.ℕ) → Maybe A
  index' [] i₁ c = Nothing
  index' (x₁ ∷ l₁) i₁ c with (i₁ Sec2.== c)
  index' (x₁ ∷ l₁) i₁ c | Sec2.T = Just x₁
  index' (x₁ ∷ l₁) i₁ c | Sec2.F = index' l₁ i₁ (Sec2.S c)

exx1 : Maybe Sec2.ℕ
exx1 = index (1 ∷ []) ⋆ 0 Sec2.ok

index'' : {A : Set} → ∀ (l : List A)
                  → ∀ (i : Sec2.ℕ)
                  → Sec2.So (i Sec2.< (length l))
                  → A
index'' [] Sec2.Z ()
index'' [] (Sec2.S i) ()
index'' (x ∷ l) Sec2.Z Sec2.ok = x
index'' (x ∷ l) (Sec2.S i) p = index'' l i p

-- append two lists
_++_ : {A : Set} → (l : List A) → (l' : List A) → (List A)
[] ++ l' = l'
(x ∷ l) ++ l' = (x ∷ (l ++ l'))

-- composition of two functions
_∘_ : {A B C : Set} → (A → B) → (B → C) → (A → C)
f ∘ g = λ x → (g (f x))

cong : {A : Set} → (x : A) → (l m : List A) → (l Sec2.≡ m) → (x ∷ l) Sec2.≡ (x ∷ m)
cong x l .l Sec2.refl = Sec2.refl

cong2 : {A : Set} → (l m q : List A) → (l Sec2.≡ m) → (l ++ q) Sec2.≡ (m ++ q)
cong2 l .l q Sec2.refl = Sec2.refl

thm1-map : {A B : Set} → (f : A → B) → (l : List A) → (m : List A) → (map f (l ++ m)) Sec2.≡ (map f l) ++ (map f m)
thm1-map f [] m = Sec2.refl
thm1-map f (x ∷ l) m with (f x)
thm1-map f (x ∷ l) m | p  = cong p (map f (l ++ m)) (map f l ++ map f m) (thm1-map f l m)

-- map ∘
thm2-map : {A B C : Set} → (f : A → B) → (g : B → C) → (l : List A) → (map (f ∘ g) l Sec2.≡ ((map f) ∘ (map g)) l)
thm2-map f₁ g₁ [] = Sec2.refl
thm2-map f₁ g₁ (x ∷ l) with (thm2-map f₁ g₁ l)
thm2-map f₁ g₁ (x ∷ l) | p = cong (g₁ (f₁ x)) (map (λ z → g₁ (f₁ z)) l) (map g₁ (map f₁ l)) p

-- Non empty list by construction
data NeList (A : Set) : Set where
  ^_^ : A → NeList A
  _∶_ : A → NeList A → NeList A

infixr 60 ^_^
infixr 60 _∶_

-- XXX: Prove these in Coq along with the other theorem from Mike Naha's
-- tutorial in Agda.


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

module Data.Empty.Properties where

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

isProp¬ : (A : Type a) → isProp (¬ A)
isProp¬ _ f g i x = isProp⊥ (f x) (g x) i

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Categories.Category

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

open import Level

open import Categories.Category.CartesianClosed C
open import Categories.Category.Complete.Finitely C
open import Categories.Diagram.Equalizer C
open import Categories.Diagram.SubobjectClassifier C

open Category C

record Topos : Set (levelOfTerm C) where
  field
    cartesianClosed     : CartesianClosed
    subobjectClassifier : SubobjectClassifier
    equalizer           : ∀ {A B} (f g : A ⇒ B) → Equalizer f g

  open CartesianClosed cartesianClosed public

  module subobjectClassifier = SubobjectClassifier subobjectClassifier

  finitelyComplete : FinitelyComplete
  finitelyComplete = record
    { cartesian = cartesian
    ; equalizer = equalizer
    }

  open FinitelyComplete finitelyComplete using (module equalizer; pullback) public

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------------
-- Axiomatic PA propositional equality
------------------------------------------------------------------------------

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

module PA.Axiomatic.Mendelson.Relation.Binary.PropositionalEqualityI where

open import PA.Axiomatic.Mendelson.Base

------------------------------------------------------------------------------
-- Identity properties

≈-refl : ∀ {n} → n ≈ n
≈-refl {n} = S₁ (S₅ n) (S₅ n)

≈-sym : ∀ {m n} → m ≈ n → n ≈ m
≈-sym h = S₁ h ≈-refl

≈-trans : ∀ {m n o} → m ≈ n → n ≈ o → m ≈ o
≈-trans h = S₁ (≈-sym h)

------------------------------------------------------------------------------
-- Substitution

-- Using Mendelson's axioms we cannot prove

--    a ≈ b    A(x)
--  ----------------- substitution
--         A(x)

-- where A(x) is an arbitrary propositional function, We can prove
-- substitutivity of `_≈_` for the proper functional symbols of the
-- language (`succ`, `add` and `mult`). That is, we can prove (by
-- induction)

--   succCong    : ∀ {m n} → m ≈ n → succ m ≈ succ n
--   +-rightCong : ∀ {m n p} → n ≈ p → m + n ≈ m + p
--   +-leftCong  : ∀ {m n p} → m ≈ n → m + p ≈ n + p
--   *-rightCong : ∀ {m n p} → n ≈ p → m * n ≈ m * p
--   *-leftCong  : ∀ {m n p} → m ≈ n → m * p ≈ n * p

-- The proofs of the above properties are in the `PropertiesI` module.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Lecture7 where

import Lecture6
open Lecture6 public

-- Section 7.1 Fiberwise equivalences
tot : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} → ((x : A) → B x → C x) → ( Σ A B → Σ A C)
tot f (dpair x y) = dpair x (f x y)

-- There is a function from the fibers of the induced map on total spaces, to the fibers of the fiberwise transformation
fib-ftr-fib-tot : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} → (f : (x : A) → B x → C x) → (t : Σ A C) → fib (tot f) t → fib (f (pr1 t)) (pr2 t)
fib-ftr-fib-tot f .(dpair x (f x y)) (dpair (dpair x y) refl) = dpair y refl

-- This function has a converse
fib-tot-fib-ftr : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} → (f : (x : A) → B x → C x) → (t : Σ A C) → fib (f (pr1 t)) (pr2 t) → fib (tot f) t
fib-tot-fib-ftr F (dpair a .(F a y)) (dpair y refl) = dpair (dpair a y) refl

issec-fib-tot-fib-ftr : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} → (f : (x : A) → B x → C x) → (t : Σ A C) → ((fib-ftr-fib-tot f t) ∘ (fib-tot-fib-ftr f t)) ~ id
issec-fib-tot-fib-ftr f (dpair x .(f x y)) (dpair y refl) = refl

isretr-fib-tot-fib-ftr : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} → (f : (x : A) → B x → C x) → (t : Σ A C) → ((fib-tot-fib-ftr f t) ∘ (fib-ftr-fib-tot f t)) ~ id
isretr-fib-tot-fib-ftr f .(dpair x (f x y)) (dpair (dpair x y) refl) = refl

-- We establish that the fibers of the induced map on total spaces are equivalent to the fibers of the fiberwise transformation.
is-equiv-fib-ftr-fib-tot : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} → (f : (x : A) → B x → C x) → (t : Σ A C) → is-equiv (fib-ftr-fib-tot f t)
is-equiv-fib-ftr-fib-tot f t =
  pair
    (dpair (fib-tot-fib-ftr f t) (issec-fib-tot-fib-ftr f t))
    (dpair (fib-tot-fib-ftr f t) (isretr-fib-tot-fib-ftr f t))

-- Any fiberwise equivalence induces an equivalence on total spaces
is-equiv-tot-is-equiv-ftr :
  {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} →
  (f : (x : A) → B x → C x) → ((x : A) → is-equiv (f x)) →
  is-equiv (tot f )
is-equiv-tot-is-equiv-ftr f H =
  is-equiv-is-contr-map
    (λ t → is-contr-is-equiv
      (fib-ftr-fib-tot f t)
      (is-equiv-fib-ftr-fib-tot f t)
      (is-contr-map-is-equiv (H _) (pr2 t)))

-- Convesely, any fiberwise transformation that induces an equivalence on total spaces is a fiberwise equivalence.
is-equiv-ftr-is-equiv-tot :
  {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k} →
  (f : (x : A) → B x → C x) → is-equiv (tot f) →
  (x : A) → is-equiv (f x)
is-equiv-ftr-is-equiv-tot f H x =
  is-equiv-is-contr-map
    (λ z → is-contr-is-equiv'
      (fib-ftr-fib-tot f (dpair x z))
      (is-equiv-fib-ftr-fib-tot f (dpair x z))
      (is-contr-map-is-equiv H (dpair x z)))

-- Section 7.2 The fundamental theorem

-- The general form of the fundamental theorem of identity types
id-fundamental-gen : {i j : Level} {A : UU i} {B : A → UU j} (a : A) (b : B a) → is-contr (Σ A B) → (f : (x : A) → Id a x → B x) → (x : A) → is-equiv (f x)
id-fundamental-gen {_} {_} {A} {B} a b C f x =
  is-equiv-ftr-is-equiv-tot f
    (is-equiv-is-contr _ (is-contr-total-path A a) C) x

-- The canonical form of the fundamental theorem of identity types
id-fundamental : {i j : Level} {A : UU i} {B : A → UU j} (a : A) (b : B a) →
  is-contr (Σ A B) →
  (x : A) → is-equiv (ind-Id (λ x p → B x) b x)
id-fundamental {i} {j} {A} {B} a b H =
  id-fundamental-gen a b H (ind-Id (λ x p → B x) b)

-- The converse of the fundamental theorem of identity types
id-fundamental' : {i j : Level} {A : UU i} {B : A → UU j} (a : A) (b : B a) →
  ((x : A) → is-equiv (ind-Id (λ x p → B x) b x)) → is-contr (Σ A B)
id-fundamental' {i} {j} {A} {B} a b H =
  is-contr-is-equiv'
    (tot (ind-Id (λ x p → B x) b))
    (is-equiv-tot-is-equiv-ftr _ H)
    (is-contr-total-path A a)

-- As an application we show that equivalences are embeddings.
is-emb : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-emb f = (x y : _) → is-equiv (ap f {x} {y})

is-emb-is-equiv : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → is-equiv f → is-emb f
is-emb-is-equiv {i} {j} {A} {B} f E x =
  id-fundamental-gen x refl
    (is-contr-is-equiv' (tot (λ y (p : Id (f y) (f x)) → inv p))
        (is-equiv-tot-is-equiv-ftr _ (λ y → is-equiv-inv (f y) (f x)))
      (is-contr-map-is-equiv E (f x)))
    (λ y p → ap f p)

-- Exercises

-- Exercise 7.1

tot-htpy : {i j k : Level} {A : UU i} {B : A → UU j} {C : A → UU k}
  {f g : (x : A) → B x → C x} → (H : (x : A) → f x ~ g x) → tot f ~ tot g
tot-htpy H (dpair x y) = eq-pair (dpair refl (H x y))

tot-id : {i j : Level} {A : UU i} (B : A → UU j) →
  (tot (λ x (y : B x) → y)) ~ id
tot-id B (dpair x y) = refl

tot-comp : {i j j' j'' : Level} {A : UU i} {B : A → UU j} {B' : A → UU j'} {B'' : A → UU j''} (f : (x : A) → B x → B' x) (g : (x : A) → B' x → B'' x) →
  tot (λ x → (g x) ∘ (f x)) ~ ((tot g) ∘ (tot f))
tot-comp f g (dpair x y) = refl

-- Exercise 7.7
id-fundamental-retr : {i j : Level} {A : UU i} {B : A → UU j} (a : A) →
  (i : (x : A) → B x → Id a x) → (R : (x : A) → retr (i x)) →
  (x : A) → is-equiv (i x)
id-fundamental-retr {_} {_} {A} {B} a i R =
  is-equiv-ftr-is-equiv-tot i
    (is-equiv-is-contr (tot i)
      (is-contr-retract-of (Σ _ (λ y → Id a y))
        (dpair (tot i)
          (dpair (tot λ x → pr1 (R x))
            (htpy-concat
              (tot (λ x → pr1 (R x) ∘ i x))
              (htpy-inv (tot-comp i (λ x → pr1 (R x))))
                (htpy-concat (tot (λ x → id))
                  (tot-htpy λ x → pr2 (R x))
                  (tot-id B)))))
        (is-contr-total-path _ a))
      (is-contr-total-path _ a))


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

module Luau.StrictMode.ToString where

open import Agda.Builtin.Nat using (Nat; suc)
open import FFI.Data.String using (String; _++_)
open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err)
open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
open import Luau.Type using (strict; number; boolean; string; nil)
open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Var.ToString using (varToString)
open import Luau.Type.ToString using (typeToString)
open import Luau.Syntax.ToString using (binOpToString)

tmp : Nat → String
tmp 0 = "w"
tmp 1 = "x"
tmp 2 = "y"
tmp 3 = "z"
tmp (suc (suc (suc n))) = tmp n ++ "'"

treeToString : Tree → Nat → String → String
treeToString (scalar number) n v = v ++ " is a number"
treeToString (scalar boolean) n v = v ++ " is a boolean"
treeToString (scalar string) n v = v ++ " is a string"
treeToString (scalar nil) n v = v ++ " is nil"
treeToString function n v = v ++ " is a function"
treeToString (function-ok t) n v = treeToString t n (v ++ "()")
treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ treeToString t (suc n) w where w = tmp n

subtypeWarningToString : ∀ {T U} → (T ≮: U) → String
subtypeWarningToString (witness t p q) = "\n  because provided type contains v, where " ++ treeToString t 0 "v"

warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String
warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String

warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x
warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated address " ++ addrToString a
warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U ++ subtypeWarningToString p
warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W
warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W
warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p
warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n  in function expression " ++ varToString f
warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) =  "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U ++ subtypeWarningToString p
warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n  in block " ++ varToString b
warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T ++ subtypeWarningToString p
warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U ++ subtypeWarningToString p
warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W
warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W

warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n  in function declaration " ++ varToString f
warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W
warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) =  "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U ++ subtypeWarningToString p
warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n  in local variable declaration " ++ varToString x
warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W
warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n  in return statement"

max_stars_repo_name: EtiTheSpirit/luau

max_issues_repo_name: EtiTheSpirit/luau

max_forks_repo_name: EtiTheSpirit/luau


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

module WithoutK-PatternSynonyms1 where

-- Equality defined with one index.
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

pattern r = refl

-- The --cubical-compatible option works with pattern synonyms.
K : (A : Set) (x : A) (P : x ≡ x → Set) → P refl → (p : x ≡ x ) →  P p
K A x P pr r = pr


text:
module BetterExampleOfDot where

open import Data.Nat

open import Agda.Builtin.Equality

data CannotContruct : ℕ → Set where

test : ∀ a b →
     ((a b : ℕ) → a + b ≡ b + a) →
     CannotContruct (a + b) →
     CannotContruct (b + a)
test a b theory p with  a + b  | theory a b
...                 | .(b + a) | refl = p

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneously-indexed binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Indexed.Heterogeneous where

------------------------------------------------------------------------
-- Publicly export core definitions

open import Relation.Binary.Indexed.Heterogeneous.Core public
open import Relation.Binary.Indexed.Heterogeneous.Definitions public
open import Relation.Binary.Indexed.Heterogeneous.Structures public
open import Relation.Binary.Indexed.Heterogeneous.Bundles public

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.17

REL = IREL
{-# WARNING_ON_USAGE REL
"Warning: REL was deprecated in v0.17.
Please use IREL instead."
#-}
Rel = IRel
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.17.
Please use IRel instead."
#-}
Setoid = IndexedSetoid
{-# WARNING_ON_USAGE Setoid
"Warning: Setoid was deprecated in v0.17.
Please use IndexedSetoid instead."
#-}
IsEquivalence = IsIndexedEquivalence
{-# WARNING_ON_USAGE IsEquivalence
"Warning: IsEquivalence was deprecated in v0.17.
Please use IsIndexedEquivalence instead."
#-}


text:
module Text.Greek.SBLGNT.2John where

open import Data.List
open import Text.Greek.Bible
open import Text.Greek.Script
open import Text.Greek.Script.Unicode

ΙΩΑΝΝΟΥ-Β : List (Word)
ΙΩΑΝΝΟΥ-Β =
    word (Ὁ ∷ []) "2John.1.1"
  ∷ word (π ∷ ρ ∷ ε ∷ σ ∷ β ∷ ύ ∷ τ ∷ ε ∷ ρ ∷ ο ∷ ς ∷ []) "2John.1.1"
  ∷ word (ἐ ∷ κ ∷ ∙λ ∷ ε ∷ κ ∷ τ ∷ ῇ ∷ []) "2John.1.1"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ ᾳ ∷ []) "2John.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.1"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2John.1.1"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ ο ∷ ι ∷ ς ∷ []) "2John.1.1"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῆ ∷ ς ∷ []) "2John.1.1"
  ∷ word (ο ∷ ὓ ∷ ς ∷ []) "2John.1.1"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "2John.1.1"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ ῶ ∷ []) "2John.1.1"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.1"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "2John.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.1"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2John.1.1"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "2John.1.1"
  ∷ word (μ ∷ ό ∷ ν ∷ ο ∷ ς ∷ []) "2John.1.1"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2John.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.1"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2John.1.1"
  ∷ word (ο ∷ ἱ ∷ []) "2John.1.1"
  ∷ word (ἐ ∷ γ ∷ ν ∷ ω ∷ κ ∷ ό ∷ τ ∷ ε ∷ ς ∷ []) "2John.1.1"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2John.1.1"
  ∷ word (ἀ ∷ ∙λ ∷ ή ∷ θ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2John.1.1"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2John.1.2"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2John.1.2"
  ∷ word (ἀ ∷ ∙λ ∷ ή ∷ θ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "2John.1.2"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2John.1.2"
  ∷ word (μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ σ ∷ α ∷ ν ∷ []) "2John.1.2"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.2"
  ∷ word (ἡ ∷ μ ∷ ῖ ∷ ν ∷ []) "2John.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.2"
  ∷ word (μ ∷ ε ∷ θ ∷ []) "2John.1.2"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2John.1.2"
  ∷ word (ἔ ∷ σ ∷ τ ∷ α ∷ ι ∷ []) "2John.1.2"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2John.1.2"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2John.1.2"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ α ∷ []) "2John.1.2"
  ∷ word (ἔ ∷ σ ∷ τ ∷ α ∷ ι ∷ []) "2John.1.3"
  ∷ word (μ ∷ ε ∷ θ ∷ []) "2John.1.3"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "2John.1.3"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "2John.1.3"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "2John.1.3"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "2John.1.3"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2John.1.3"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "2John.1.3"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ό ∷ ς ∷ []) "2John.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.3"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2John.1.3"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "2John.1.3"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2John.1.3"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2John.1.3"
  ∷ word (υ ∷ ἱ ∷ ο ∷ ῦ ∷ []) "2John.1.3"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2John.1.3"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ό ∷ ς ∷ []) "2John.1.3"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.3"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "2John.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.3"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "2John.1.3"
  ∷ word (Ἐ ∷ χ ∷ ά ∷ ρ ∷ η ∷ ν ∷ []) "2John.1.4"
  ∷ word (∙λ ∷ ί ∷ α ∷ ν ∷ []) "2John.1.4"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2John.1.4"
  ∷ word (ε ∷ ὕ ∷ ρ ∷ η ∷ κ ∷ α ∷ []) "2John.1.4"
  ∷ word (ἐ ∷ κ ∷ []) "2John.1.4"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "2John.1.4"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ ω ∷ ν ∷ []) "2John.1.4"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2John.1.4"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "2John.1.4"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.4"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "2John.1.4"
  ∷ word (κ ∷ α ∷ θ ∷ ὼ ∷ ς ∷ []) "2John.1.4"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ο ∷ ∙λ ∷ ὴ ∷ ν ∷ []) "2John.1.4"
  ∷ word (ἐ ∷ ∙λ ∷ ά ∷ β ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2John.1.4"
  ∷ word (π ∷ α ∷ ρ ∷ ὰ ∷ []) "2John.1.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2John.1.4"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ό ∷ ς ∷ []) "2John.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.5"
  ∷ word (ν ∷ ῦ ∷ ν ∷ []) "2John.1.5"
  ∷ word (ἐ ∷ ρ ∷ ω ∷ τ ∷ ῶ ∷ []) "2John.1.5"
  ∷ word (σ ∷ ε ∷ []) "2John.1.5"
  ∷ word (κ ∷ υ ∷ ρ ∷ ί ∷ α ∷ []) "2John.1.5"
  ∷ word (ο ∷ ὐ ∷ χ ∷ []) "2John.1.5"
  ∷ word (ὡ ∷ ς ∷ []) "2John.1.5"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ο ∷ ∙λ ∷ ὴ ∷ ν ∷ []) "2John.1.5"
  ∷ word (κ ∷ α ∷ ι ∷ ν ∷ ὴ ∷ ν ∷ []) "2John.1.5"
  ∷ word (γ ∷ ρ ∷ ά ∷ φ ∷ ω ∷ ν ∷ []) "2John.1.5"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "2John.1.5"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2John.1.5"
  ∷ word (ἣ ∷ ν ∷ []) "2John.1.5"
  ∷ word (ε ∷ ἴ ∷ χ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "2John.1.5"
  ∷ word (ἀ ∷ π ∷ []) "2John.1.5"
  ∷ word (ἀ ∷ ρ ∷ χ ∷ ῆ ∷ ς ∷ []) "2John.1.5"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2John.1.5"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ ῶ ∷ μ ∷ ε ∷ ν ∷ []) "2John.1.5"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ή ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "2John.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.6"
  ∷ word (α ∷ ὕ ∷ τ ∷ η ∷ []) "2John.1.6"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ὶ ∷ ν ∷ []) "2John.1.6"
  ∷ word (ἡ ∷ []) "2John.1.6"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ η ∷ []) "2John.1.6"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2John.1.6"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ῶ ∷ μ ∷ ε ∷ ν ∷ []) "2John.1.6"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "2John.1.6"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "2John.1.6"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ο ∷ ∙λ ∷ ὰ ∷ ς ∷ []) "2John.1.6"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2John.1.6"
  ∷ word (α ∷ ὕ ∷ τ ∷ η ∷ []) "2John.1.6"
  ∷ word (ἡ ∷ []) "2John.1.6"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ο ∷ ∙λ ∷ ή ∷ []) "2John.1.6"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2John.1.6"
  ∷ word (κ ∷ α ∷ θ ∷ ὼ ∷ ς ∷ []) "2John.1.6"
  ∷ word (ἠ ∷ κ ∷ ο ∷ ύ ∷ σ ∷ α ∷ τ ∷ ε ∷ []) "2John.1.6"
  ∷ word (ἀ ∷ π ∷ []) "2John.1.6"
  ∷ word (ἀ ∷ ρ ∷ χ ∷ ῆ ∷ ς ∷ []) "2John.1.6"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2John.1.6"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.6"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῇ ∷ []) "2John.1.6"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ῆ ∷ τ ∷ ε ∷ []) "2John.1.6"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "2John.1.7"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ο ∷ ὶ ∷ []) "2John.1.7"
  ∷ word (π ∷ ∙λ ∷ ά ∷ ν ∷ ο ∷ ι ∷ []) "2John.1.7"
  ∷ word (ἐ ∷ ξ ∷ ῆ ∷ ∙λ ∷ θ ∷ ο ∷ ν ∷ []) "2John.1.7"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2John.1.7"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2John.1.7"
  ∷ word (κ ∷ ό ∷ σ ∷ μ ∷ ο ∷ ν ∷ []) "2John.1.7"
  ∷ word (ο ∷ ἱ ∷ []) "2John.1.7"
  ∷ word (μ ∷ ὴ ∷ []) "2John.1.7"
  ∷ word (ὁ ∷ μ ∷ ο ∷ ∙λ ∷ ο ∷ γ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "2John.1.7"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ ν ∷ []) "2John.1.7"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ν ∷ []) "2John.1.7"
  ∷ word (ἐ ∷ ρ ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ν ∷ []) "2John.1.7"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.7"
  ∷ word (σ ∷ α ∷ ρ ∷ κ ∷ ί ∷ []) "2John.1.7"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ό ∷ ς ∷ []) "2John.1.7"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "2John.1.7"
  ∷ word (ὁ ∷ []) "2John.1.7"
  ∷ word (π ∷ ∙λ ∷ ά ∷ ν ∷ ο ∷ ς ∷ []) "2John.1.7"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.7"
  ∷ word (ὁ ∷ []) "2John.1.7"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ί ∷ χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ς ∷ []) "2John.1.7"
  ∷ word (β ∷ ∙λ ∷ έ ∷ π ∷ ε ∷ τ ∷ ε ∷ []) "2John.1.8"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ο ∷ ύ ∷ ς ∷ []) "2John.1.8"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2John.1.8"
  ∷ word (μ ∷ ὴ ∷ []) "2John.1.8"
  ∷ word (ἀ ∷ π ∷ ο ∷ ∙λ ∷ έ ∷ σ ∷ η ∷ τ ∷ ε ∷ []) "2John.1.8"
  ∷ word (ἃ ∷ []) "2John.1.8"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ γ ∷ α ∷ σ ∷ ά ∷ μ ∷ ε ∷ θ ∷ α ∷ []) "2John.1.8"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2John.1.8"
  ∷ word (μ ∷ ι ∷ σ ∷ θ ∷ ὸ ∷ ν ∷ []) "2John.1.8"
  ∷ word (π ∷ ∙λ ∷ ή ∷ ρ ∷ η ∷ []) "2John.1.8"
  ∷ word (ἀ ∷ π ∷ ο ∷ ∙λ ∷ ά ∷ β ∷ η ∷ τ ∷ ε ∷ []) "2John.1.8"
  ∷ word (π ∷ ᾶ ∷ ς ∷ []) "2John.1.9"
  ∷ word (ὁ ∷ []) "2John.1.9"
  ∷ word (π ∷ ρ ∷ ο ∷ ά ∷ γ ∷ ω ∷ ν ∷ []) "2John.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.9"
  ∷ word (μ ∷ ὴ ∷ []) "2John.1.9"
  ∷ word (μ ∷ έ ∷ ν ∷ ω ∷ ν ∷ []) "2John.1.9"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.9"
  ∷ word (τ ∷ ῇ ∷ []) "2John.1.9"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ χ ∷ ῇ ∷ []) "2John.1.9"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "2John.1.9"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "2John.1.9"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ν ∷ []) "2John.1.9"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2John.1.9"
  ∷ word (ἔ ∷ χ ∷ ε ∷ ι ∷ []) "2John.1.9"
  ∷ word (ὁ ∷ []) "2John.1.9"
  ∷ word (μ ∷ έ ∷ ν ∷ ω ∷ ν ∷ []) "2John.1.9"
  ∷ word (ἐ ∷ ν ∷ []) "2John.1.9"
  ∷ word (τ ∷ ῇ ∷ []) "2John.1.9"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ χ ∷ ῇ ∷ []) "2John.1.9"
  ∷ word (ο ∷ ὗ ∷ τ ∷ ο ∷ ς ∷ []) "2John.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.9"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2John.1.9"
  ∷ word (π ∷ α ∷ τ ∷ έ ∷ ρ ∷ α ∷ []) "2John.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.9"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "2John.1.9"
  ∷ word (υ ∷ ἱ ∷ ὸ ∷ ν ∷ []) "2John.1.9"
  ∷ word (ἔ ∷ χ ∷ ε ∷ ι ∷ []) "2John.1.9"
  ∷ word (ε ∷ ἴ ∷ []) "2John.1.10"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "2John.1.10"
  ∷ word (ἔ ∷ ρ ∷ χ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "2John.1.10"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2John.1.10"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2John.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.10"
  ∷ word (τ ∷ α ∷ ύ ∷ τ ∷ η ∷ ν ∷ []) "2John.1.10"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "2John.1.10"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ χ ∷ ὴ ∷ ν ∷ []) "2John.1.10"
  ∷ word (ο ∷ ὐ ∷ []) "2John.1.10"
  ∷ word (φ ∷ έ ∷ ρ ∷ ε ∷ ι ∷ []) "2John.1.10"
  ∷ word (μ ∷ ὴ ∷ []) "2John.1.10"
  ∷ word (∙λ ∷ α ∷ μ ∷ β ∷ ά ∷ ν ∷ ε ∷ τ ∷ ε ∷ []) "2John.1.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὸ ∷ ν ∷ []) "2John.1.10"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "2John.1.10"
  ∷ word (ο ∷ ἰ ∷ κ ∷ ί ∷ α ∷ ν ∷ []) "2John.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.10"
  ∷ word (χ ∷ α ∷ ί ∷ ρ ∷ ε ∷ ι ∷ ν ∷ []) "2John.1.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῷ ∷ []) "2John.1.10"
  ∷ word (μ ∷ ὴ ∷ []) "2John.1.10"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ε ∷ τ ∷ ε ∷ []) "2John.1.10"
  ∷ word (ὁ ∷ []) "2John.1.11"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ω ∷ ν ∷ []) "2John.1.11"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "2John.1.11"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῷ ∷ []) "2John.1.11"
  ∷ word (χ ∷ α ∷ ί ∷ ρ ∷ ε ∷ ι ∷ ν ∷ []) "2John.1.11"
  ∷ word (κ ∷ ο ∷ ι ∷ ν ∷ ω ∷ ν ∷ ε ∷ ῖ ∷ []) "2John.1.11"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2John.1.11"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ι ∷ ς ∷ []) "2John.1.11"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "2John.1.11"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "2John.1.11"
  ∷ word (π ∷ ο ∷ ν ∷ η ∷ ρ ∷ ο ∷ ῖ ∷ ς ∷ []) "2John.1.11"
  ∷ word (Π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2John.1.12"
  ∷ word (ἔ ∷ χ ∷ ω ∷ ν ∷ []) "2John.1.12"
  ∷ word (ὑ ∷ μ ∷ ῖ ∷ ν ∷ []) "2John.1.12"
  ∷ word (γ ∷ ρ ∷ ά ∷ φ ∷ ε ∷ ι ∷ ν ∷ []) "2John.1.12"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "2John.1.12"
  ∷ word (ἐ ∷ β ∷ ο ∷ υ ∷ ∙λ ∷ ή ∷ θ ∷ η ∷ ν ∷ []) "2John.1.12"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "2John.1.12"
  ∷ word (χ ∷ ά ∷ ρ ∷ τ ∷ ο ∷ υ ∷ []) "2John.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.12"
  ∷ word (μ ∷ έ ∷ ∙λ ∷ α ∷ ν ∷ ο ∷ ς ∷ []) "2John.1.12"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "2John.1.12"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ ζ ∷ ω ∷ []) "2John.1.12"
  ∷ word (γ ∷ ε ∷ ν ∷ έ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "2John.1.12"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2John.1.12"
  ∷ word (ὑ ∷ μ ∷ ᾶ ∷ ς ∷ []) "2John.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "2John.1.12"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ []) "2John.1.12"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "2John.1.12"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ []) "2John.1.12"
  ∷ word (∙λ ∷ α ∷ ∙λ ∷ ῆ ∷ σ ∷ α ∷ ι ∷ []) "2John.1.12"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "2John.1.12"
  ∷ word (ἡ ∷ []) "2John.1.12"
  ∷ word (χ ∷ α ∷ ρ ∷ ὰ ∷ []) "2John.1.12"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "2John.1.12"
  ∷ word (π ∷ ε ∷ π ∷ ∙λ ∷ η ∷ ρ ∷ ω ∷ μ ∷ έ ∷ ν ∷ η ∷ []) "2John.1.12"
  ∷ word (ᾖ ∷ []) "2John.1.12"
  ∷ word (Ἀ ∷ σ ∷ π ∷ ά ∷ ζ ∷ ε ∷ τ ∷ α ∷ ί ∷ []) "2John.1.13"
  ∷ word (σ ∷ ε ∷ []) "2John.1.13"
  ∷ word (τ ∷ ὰ ∷ []) "2John.1.13"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ α ∷ []) "2John.1.13"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2John.1.13"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ῆ ∷ ς ∷ []) "2John.1.13"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "2John.1.13"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "2John.1.13"
  ∷ word (ἐ ∷ κ ∷ ∙λ ∷ ε ∷ κ ∷ τ ∷ ῆ ∷ ς ∷ []) "2John.1.13"
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


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

module Cubical.HITs.FreeComMonoids where

open import Cubical.HITs.FreeComMonoids.Base public
open import Cubical.HITs.FreeComMonoids.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Data.Bits.Order.Reverse where

open import Prelude
open import Data.Bits

-- Least significant bit first

infix 4 _≲ᴮ_&_
_≲ᴮ_&_ : Bits → Bits → Bool → Bool
[]    ≲ᴮ ys    & true  = true
[]    ≲ᴮ []    & false = false
[]    ≲ᴮ 0∷ ys & false = true
[]    ≲ᴮ 1∷ ys & false = true
0∷ xs ≲ᴮ []    & s     = false
0∷ xs ≲ᴮ 0∷ ys & s     = xs ≲ᴮ ys & s
0∷ xs ≲ᴮ 1∷ ys & s     = xs ≲ᴮ ys & true
1∷ xs ≲ᴮ []    & s     = false
1∷ xs ≲ᴮ 0∷ ys & s     = xs ≲ᴮ ys & false
1∷ xs ≲ᴮ 1∷ ys & s     = xs ≲ᴮ ys & s

infix 4 _≤ᴮ_ _<ᴮ_
_≤ᴮ_ : Bits → Bits → Bool
xs ≤ᴮ ys = xs ≲ᴮ ys & true

_<ᴮ_ : Bits → Bits → Bool
xs <ᴮ ys = xs ≲ᴮ ys & false

infix 4 _≤_ _<_
_≤_ : Bits → Bits → Type
xs ≤ ys = T (xs ≤ᴮ ys)

_<_ : Bits → Bits → Type
xs < ys = T (xs <ᴮ ys)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module LanguageConstructs where

open import Haskell.Prelude

{-# FOREIGN AGDA2HS {-# LANGUAGE LambdaCase #-} #-}

--------------------------------------------------
-- Lists

oneTwoThree : List Int
oneTwoThree = 1 ∷ 2 ∷ 3 ∷ []
{-# COMPILE AGDA2HS oneTwoThree #-}

exactlyTwo : List a → Maybe (a × a)
exactlyTwo (x ∷ y ∷ []) = Just (x , y)
exactlyTwo _            = Nothing
{-# COMPILE AGDA2HS exactlyTwo #-}

--------------------------------------------------
-- If-then-else

ifThenElse : Int → String
ifThenElse n = if n >= 10 then "big" else "small"
{-# COMPILE AGDA2HS ifThenElse #-}

--------------------------------------------------
-- Case

maybeToList : Maybe a → List a
maybeToList = λ where Nothing  → []
                      (Just x) → x ∷ []
{-# COMPILE AGDA2HS maybeToList #-}

mhead : List a → Maybe a
mhead xs = case xs of λ where
  []      → Nothing
  (x ∷ _) → Just x
{-# COMPILE AGDA2HS mhead #-}

-- Applied to lambda
plus5minus5 : Int → Int
plus5minus5 n = case n + 5 of λ m → m - 5
{-# COMPILE AGDA2HS plus5minus5 #-}

-- Applied to non-lambda
len : List a → Int
len xs = case xs of length
{-# COMPILE AGDA2HS len #-}

-- Underapplied
applyToFalse : (Bool → a) → a
applyToFalse = case false of_
{-# COMPILE AGDA2HS applyToFalse #-}

caseOf : a → (a → b) → b
caseOf = case_of_
{-# COMPILE AGDA2HS caseOf #-}

--------------------------------------------------
-- Enums

enum₁ : List Int
enum₁ = enumFromTo 5 10
{-# COMPILE AGDA2HS enum₁ #-}

enum₂ : List Integer
enum₂ = enumFromThenTo 10 20 100
{-# COMPILE AGDA2HS enum₂ #-}

enum₃ : List Bool
enum₃ = enumFrom false
{-# COMPILE AGDA2HS enum₃ #-}

enum₄ : List Ordering
enum₄ = enumFromThen LT EQ
{-# COMPILE AGDA2HS enum₄ #-}

underappliedEnum : List Int → List (List Int)
underappliedEnum = map (enumFromTo 1)
{-# COMPILE AGDA2HS underappliedEnum #-}


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

open import lib.Base

module lib.Coinduction where

infix 1000 ♯_

postulate  -- Coinduction
  ∞  : ∀ {i} (A : Type i) → Type i
  ♯_ : ∀ {i} {A : Type i} → A → ∞ A
  ♭  : ∀ {i} {A : Type i} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
open import Agda.Builtin.Bool

record ⊤ : Set where constructor tt
data   ⊥ : Set where

record Σ (A : Set) (B : A → Set) : Set where
  field
    fst : A
    snd : B fst
open Σ

T : Bool → Set
T false = ⊥
T true  = ⊤

Foo : Bool → Set
Foo false = Bool → Bool
Foo true  = Σ Bool T

foo : (x : Bool) → Foo x
foo false x    = x
foo true  .fst = true
foo true  .snd = tt

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Category.Vect
  {k ℓᵏ} (K : Field k ℓᵏ)
  {a ℓ}
  where

open import Relation.Binary using (Setoid)
open import Algebra.Linear.Structures.Bundles
open import Algebra.Linear.Morphism.Bundles K
open import Categories.Category

open LinearMap

id : ∀ {V : VectorSpace K a ℓ} -> LinearMap V V
id {V = V} = record
  { ⟦_⟧ = λ u -> u
  ; isLinearMap = record
   { isAbelianGroupMorphism = record
     { gp-homo = record
       { mn-homo = record
         { sm-homo = record
           { ⟦⟧-cong = λ r -> r
           ; ∙-homo = λ x y → VectorSpace.refl V }
         ; ε-homo = VectorSpace.refl V } } }
   ; ∙-homo = λ c u → VectorSpace.refl V } }

_∘_ : ∀ {U V W : VectorSpace K a ℓ} -> LinearMap V W -> LinearMap U V -> LinearMap U W
_∘_ {U = U} {V} {W} f g = record
  { ⟦_⟧ = λ u → f ⟪$⟫ g ⟪$⟫ u
  ; isLinearMap = record
    { isAbelianGroupMorphism = record
      { gp-homo = record
        { mn-homo = record
          { sm-homo = record
            { ⟦⟧-cong = λ r → ⟦⟧-cong f (⟦⟧-cong g r)
            ; ∙-homo = λ u v → VectorSpace.trans W (⟦⟧-cong f (+-homo g u v)) (+-homo f (g ⟪$⟫ u) (g ⟪$⟫ v))
            }
          ; ε-homo = VectorSpace.trans W (⟦⟧-cong f (0#-homo g)) (0#-homo f)
          }
        }
      }
    ; ∙-homo = λ c u → VectorSpace.trans W (⟦⟧-cong f (∙-homo g c u)) (∙-homo f c (g ⟪$⟫ u))
    }
  }

private
  module Assoc
    {U V W X : VectorSpace K a ℓ}
    {f : LinearMap U V} {g : LinearMap V W} {h : LinearMap W X}
    where

    open Setoid (linearMap-setoid U X)
    open import Relation.Binary.EqReasoning (linearMap-setoid U X)

    right : ((h ∘ g) ∘ f) ≈ (h ∘ (g ∘ f))
    right r = ⟦⟧-cong h (⟦⟧-cong g (⟦⟧-cong f r))

    left : (h ∘ (g ∘ f)) ≈ ((h ∘ g) ∘ f)
    left r = ⟦⟧-cong h (⟦⟧-cong g (⟦⟧-cong f r))

Vect : Category _ _ _
Vect = record
  { Obj = VectorSpace K a ℓ
  ; _⇒_ = λ V W → LinearMap V W
  ; _≈_ = λ {V} {W} -> Setoid._≈_ (linearMap-setoid V W)
  ; id = id
  ; _∘_ = _∘_
  ; assoc =  λ {U} {V} {W} {X} {f} {g} {h} -> Assoc.right {U} {V} {W} {X} {f} {g} {h}
  ; sym-assoc = λ {U} {V} {W} {X} {f} {g} {h} -> Assoc.left {U} {V} {W} {X} {f} {g} {h}
  ; identityˡ = λ {U} {V} {f} -> ⟦⟧-cong f
  ; identityʳ = λ {U} {V} {f} → ⟦⟧-cong f
  ; equiv = λ {V} {W} -> Setoid.isEquivalence (linearMap-setoid V W)
  ; ∘-resp-≈ = λ {U} {V} {W} {f} {h} {g} {i} rf rg rx →
    VectorSpace.trans W (rf (⟦⟧-cong g rx)) (⟦⟧-cong h (rg (VectorSpace.refl U)))
  }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
-- Andreas, 2017-07-11, issue #2637, reported by nad.
--
-- This error was triggered by a meta m in a constraint UnBlock m
-- which is solved to infinity by the size solver.

-- The constraint printer did not expect such a situation
-- and crashed when printing the UnBlock constraint.

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

module _ (Z : Set) where

open import Common.Size
open import Common.Product

postulate
  map    : (A B C : Set) → (A → C) → A × B → C × B
  I      : Set
  P      : I → Set
  Q      : Size → I → Set
  f      : I → I
  lemma₁ : (R : I → Set) → (∀ x → R (f x) → R x) → ∀ x → R x → R (f x)
  lemma₂ : ∀ i x → Q i (f x) → Q i x

works : ∀ i x → Q i (f x) × P x → Q i (f (f x)) × P x
works i x = map
  (Q i (f x))
  (P x)
  (Q i (f (f x)))
  (lemma₁ (Q i) (λ y → lemma₂ i y) (f x))

-- Replacing any underscore by its solution or parts of its solution
-- makes the internal error disappear.

lemma₃ : ∀ i x → Q i (f x) × P x → Q i (f (f x)) × P x
lemma₃ i x = map
  (Q _ _)
  (P x)
  (Q _ (f (f x)))
  (lemma₁ _ (λ y → lemma₂ _ _) _)


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

open import Algebra

module Magma.Properties
  {a ℓ} (M : Magma a ℓ) where

open Magma M


text:
module RationalUtils where

open import Algebra
import Algebra.Morphism.RingMonomorphism as RingMonomorphisms
open import Data.Rational
open import Data.Rational.Properties
open import Data.Nat using (z≤n; s≤s)
open import Data.Integer using (+≤+; +<+; +_; -[1+_])
open import Data.Product using (_×_; _,_)
open import Data.Sum
open import Function.Base using (_∘_; _∘′_)
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)

open import Vehicle.Data.Tensor

open ≤-Reasoning

private
  variable
    p q : ℚ

private
  module +-*-Monomorphism = RingMonomorphisms toℚᵘ-isRingMonomorphism-+-*

------------------------------------------------------------------------
-- Things to work out how to put in standard library

2ℚ = + 2 / 1
3ℚ = + 3 / 1

≰⇒≥ : _≰_ ⇒ _≥_
≰⇒≥ = <⇒≤ ∘′ ≰⇒>

p≤0⇒∣p∣≡-p : p ≤ 0ℚ → ∣ p ∣ ≡ - p
p≤0⇒∣p∣≡-p {mkℚ +[1+ n ] _ _} p≤0 = contradiction (nonPositive p≤0) λ()
p≤0⇒∣p∣≡-p {mkℚ +0       _ _} _   = refl
p≤0⇒∣p∣≡-p {mkℚ -[1+ n ] _ _} _   = refl

neg-involutive : Involutive _≡_ (-_)
neg-involutive (mkℚ +[1+ n ] _ _) = refl
neg-involutive (mkℚ +0       _ _) = refl
neg-involutive (mkℚ -[1+ n ] _ _) = refl

p≤∣p∣ : ∀ p → p ≤ ∣ p ∣
p≤∣p∣ p with 0ℚ ≤? p
... | yes 0≤p = ≤-reflexive (sym (0≤p⇒∣p∣≡p 0≤p))
... | no  0≰p = ≤-trans (≰⇒≥ 0≰p) (0≤∣p∣ p)

-p≤∣p∣ : ∀ p → - p ≤ ∣ p ∣
-p≤∣p∣ p with 0ℚ ≤? p
... | yes 0≤p = ≤-trans (neg-antimono-≤ 0≤p) (0≤∣p∣ p)
... | no  0≰p = ≤-reflexive (sym (p≤0⇒∣p∣≡-p (≰⇒≥ 0≰p)))

-p≤q⇒-q≤p : - p ≤ q → - q ≤ p
-p≤q⇒-q≤p {p} {q} = subst (- q ≤_) (neg-involutive p) ∘ neg-antimono-≤

p≤-q⇒q≤-p : p ≤ - q → q ≤ - p
p≤-q⇒q≤-p {p} {q} = subst (_≤ - p) (neg-involutive q) ∘ neg-antimono-≤

-p<q⇒-q<p : - p < q → - q < p
-p<q⇒-q<p {p} {q} = subst (- q <_) (neg-involutive p) ∘ neg-antimono-<

p<-q⇒q<-p : p < - q → q < - p
p<-q⇒q<-p {p} {q} = subst (_< - p) (neg-involutive q) ∘ neg-antimono-<

postulate p-[p+q]≡q : ∀ p q → p - (p + q) ≡ q

postulate p+q-p≡q : ∀ p q → p + q - p ≡ q

postulate p-q+q≡p : ∀ p q → p - q + q ≡ p

postulate *-monoʳ-≤ : ∀ r → Positive r → (r *_) Preserves _≤_ ⟶ _≤_

postulate p<r-q⇒p+q<r : ∀ p q r → p < r - q → p + q < r

∣p∣≤q⇒-q≤p≤q : ∀ p → ∣ p ∣ ≤ q → - q ≤ p × p ≤ q
∣p∣≤q⇒-q≤p≤q p ∣p∣≤q =
  -p≤q⇒-q≤p (≤-trans (-p≤∣p∣ p) ∣p∣≤q)
  , ≤-trans (p≤∣p∣ p) ∣p∣≤q

-p≤q≤p⇒∣q∣≤p : - p ≤ q → q ≤ p → ∣ q ∣ ≤ p
-p≤q≤p⇒∣q∣≤p {p} {q} -q≤p q≤p with ∣p∣≡p∨∣p∣≡-p q
... | inj₁ ∣q∣≡q  = subst (_≤ p) (sym ∣q∣≡q) q≤p
... | inj₂ ∣q∣≡-q = subst (_≤ p) (sym ∣q∣≡-q) (-p≤q⇒-q≤p -q≤p)

∣p∣<q⇒-q<p<q : ∀ p → ∣ p ∣ < q → - q < p × p < q
∣p∣<q⇒-q<p<q p ∣p∣<q =
  -p<q⇒-q<p (≤-<-trans (-p≤∣p∣ p) ∣p∣<q)
  , ≤-<-trans (p≤∣p∣ p) ∣p∣<q

-p<q<p⇒∣q∣<p : - p < q → q < p → ∣ q ∣ < p
-p<q<p⇒∣q∣<p {p} {q} -p<q q<p with ∣p∣≡p∨∣p∣≡-p q
... | inj₁ ∣q∣≡q  = subst (_< p) (sym ∣q∣≡q) q<p
... | inj₂ ∣q∣≡-q = subst (_< p) (sym ∣q∣≡-q) (-p<q⇒-q<p -p<q)

p+q-q≡p : ∀ p q → p + q - q ≡ p
p+q-q≡p p q = begin-equality
  p + q - q   ≡⟨ +-assoc p q (- q) ⟩
  p + (q - q) ≡⟨ cong (λ v → p + v) (+-inverseʳ q) ⟩
  p + 0ℚ      ≡⟨ +-identityʳ p ⟩
  p           ∎

+-isCommutativeSemigroup : IsCommutativeSemigroup _≡_ _+_
+-isCommutativeSemigroup = isCommutativeSemigroup
  where open IsCommutativeMonoid +-0-isCommutativeMonoid

+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
  { isCommutativeSemigroup = +-isCommutativeSemigroup
  }

2*p≡p+p : ∀ p → 2ℚ * p ≡ p + p
2*p≡p+p p = begin-equality
  2ℚ * p          ≡⟨⟩
  (1ℚ + 1ℚ) * p   ≡⟨ *-distribʳ-+ p 1ℚ 1ℚ ⟩
  1ℚ * p + 1ℚ * p ≡⟨ cong₂ _+_ (*-identityˡ p) (*-identityˡ p) ⟩
  p + p           ∎

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module _ where

open import Common.Prelude
open import Common.String

record IsString {a} (A : Set a) : Set a where
  field
    fromString : String → A

open IsString {{...}} public
{-# BUILTIN FROMSTRING fromString #-}

instance
  StringIsString : IsString String
  StringIsString = record { fromString = λ s → s }

  ListIsString : IsString (List Char)
  ListIsString = record { fromString = stringToList }

foo : List Char
foo = "foo"

open import Common.Equality

thm : "foo" ≡ 'f' ∷ 'o' ∷ 'o' ∷ []
thm = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module maybe-thms where

open import eq
open import level
open import maybe
open import product
open import sum

maybe-dec : ∀ {ℓ}{A : Set ℓ}(x : maybe A) → x ≡ nothing ∨ Σ A (λ a → x ≡ just a)
maybe-dec nothing = inj₁ refl
maybe-dec (just a) = inj₂ (a , refl)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
open import SOAS.Metatheory.Syntax

-- Unit law of metasubstitution
module SOAS.Metatheory.SecondOrder.Unit {T : Set}(Syn : Syntax {T}) where

open Syntax Syn

open import SOAS.Metatheory.FreeMonoid Syn

open import SOAS.Metatheory.SecondOrder.Metasubstitution Syn

open import SOAS.Families.Core {T}
open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Construction.Structure as Structure
open import SOAS.ContextMaps.Combinators
open import SOAS.ContextMaps.CategoryOfRenamings {T}
import SOAS.Abstract.Coalgebra {T} as →□
open →□.Sorted
open →□.Unsorted using (⊤ᵇ) renaming (Coalg to UCoalg ; Coalg⇒ to UCoalg⇒)
import SOAS.Abstract.Box {T} as □ ; open □.Sorted
open import SOAS.Abstract.Monoid
open import SOAS.Abstract.ExpStrength

open import SOAS.Coalgebraic.Monoid

open import SOAS.Metatheory Syn
open import SOAS.Metatheory.Monoid ⅀F ⅀:Str
open import SOAS.ContextMaps.Properties

open Theory

private
  variable
    Γ Δ Π : Ctx
    α β : T
    𝔛 𝔜 ℨ : Familyₛ

-- Metasubstitution unit is a coalgebra homomorphisem from ⊤
ms-unitᵇ⇒ : UCoalg⇒ ⊤ᵇ [ 𝔛 ⊸ (𝕋ᵇ 𝔛) ]ᵇ (λ _ → ms-unit)
ms-unitᵇ⇒ {𝔛} = record
  { ⟨r⟩ = λ{ {Γ = Γ}{Δ}{ρ} → iext (dext λ {Π} 𝔪 → sym (begin
        𝕣𝕖𝕟 𝔛 (ms-unit 𝔪) (Π ∔∣ ρ)
    ≡⟨ Renaming.𝕥⟨𝕞⟩ 𝔛 ⟩
        𝕞𝕧𝕒𝕣 𝔛 𝔪 (λ p → 𝕣𝕖𝕟 𝔛 (𝕧𝕒𝕣 𝔛 (inl Π p)) (Π ∔∣ ρ))
    ≡⟨ 𝕞≈₂ 𝔛 (λ v → Renaming.𝕥⟨𝕧⟩ 𝔛) ⟩
        𝕞𝕧𝕒𝕣 𝔛 𝔪 (λ v → 𝕧𝕒𝕣 𝔛 ((Π ∔∣ ρ) (inl Π v)))
    ≡⟨ 𝕞≈₂ 𝔛 (λ v → cong (𝕧𝕒𝕣 𝔛) (∔.+₁∘i₁ {f = id′ᵣ Π}{g = ρ})) ⟩
        𝕞𝕧𝕒𝕣 𝔛 𝔪 (λ v → 𝕧𝕒𝕣 𝔛 (∔.i₁ v))
    ∎))}
  } where open ≡-Reasoning

-- Right unit of metasubstitution
□msub-runitᵃ⇒ : MetaAlg⇒  𝔛 (𝕋ᵃ 𝔛) (□ᵃ 𝔛 (𝕋ᵃ 𝔛)) λ t ρ → □msub t ρ ms-unit
□msub-runitᵃ⇒ {𝔛} = record
  { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → dext λ ρ → begin
        □msub (𝕒𝕝𝕘 𝔛 t) ρ ms-unit
    ≡⟨ cong (λ - → - ms-unit) □MS.𝕥⟨𝕒⟩ ⟩
        𝕒𝕝𝕘 𝔛 (□estr [ 𝔛 ⊸ 𝕋ᵇ 𝔛 ]ᵇ (𝕋 𝔛) (⅀₁ □msub t) ρ ms-unit)
    ≡⟨ cong (𝕒𝕝𝕘 𝔛) (estr-unit′ ms-unitᵇ⇒) ⟩
        𝕒𝕝𝕘 𝔛 (⅀₁ (λ e′ → e′ ms-unit) (str ℐᴮ ⟅ 𝔛 ⇨ 𝕋 𝔛 ⟆ (⅀₁ □msub t) ρ))
    ≡˘⟨ cong (𝕒𝕝𝕘 𝔛) (str-nat₂ ((λ e′ → e′ ms-unit)) (⅀₁ □msub t) ρ) ⟩
        𝕒𝕝𝕘 𝔛 (str ℐᴮ (𝕋 𝔛) (⅀₁ (λ { h′ ς → h′ ς ms-unit }) (⅀₁ □msub t)) ρ)
    ≡˘⟨ congr ⅀.homomorphism (λ - → 𝕒𝕝𝕘 𝔛 (str ℐᴮ (𝕋 𝔛) - ρ)) ⟩
        𝕒𝕝𝕘 𝔛 (str ℐᴮ (𝕋 𝔛) (⅀₁ (λ{ t ρ → □msub t ρ ms-unit}) t) ρ)
    ∎ }
  ; ⟨𝑣𝑎𝑟⟩ = λ{ {v = v} → dext λ ρ → cong (λ - → - ms-unit) □MS.𝕥⟨𝕧⟩}
  ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{ε} → dext λ ρ → begin
        □msub (𝕞𝕧𝕒𝕣 𝔛 𝔪 ε) ρ ms-unit
    ≡⟨ cong (λ - → - ms-unit) □MS.𝕥⟨𝕞⟩ ⟩
        𝕤𝕦𝕓 𝔛 (ms-unit 𝔪) (copair (𝕋 𝔛) (λ v → □msub (ε v) ρ ms-unit) (𝕧𝕒𝕣 𝔛))
    ≡⟨ Substitution.𝕥⟨𝕞⟩ 𝔛 ⟩
        𝕞𝕧𝕒𝕣 𝔛 𝔪 (λ v → 𝕤𝕦𝕓 𝔛 (𝕧𝕒𝕣 𝔛 (∔.i₁ v)) (copair (𝕋 𝔛) (λ v → □msub (ε v) ρ ms-unit) (𝕧𝕒𝕣 𝔛)))
    ≡⟨ 𝕞≈₂ 𝔛 (λ v → begin
              𝕤𝕦𝕓 𝔛 (𝕧𝕒𝕣 𝔛 (∔.i₁ v)) (copair (𝕋 𝔛) (λ 𝔫 → □msub (ε 𝔫) ρ ms-unit) (𝕧𝕒𝕣 𝔛))
          ≡⟨ Mon.lunit (𝕋ᵐ 𝔛) ⟩
              copair (𝕋 𝔛) (λ 𝔫 → □msub (ε 𝔫) ρ ms-unit) (𝕧𝕒𝕣 𝔛) (∔.i₁ v)
          ≡⟨ copair∘i₁ (𝕋 𝔛) v ⟩
              □msub (ε v) ρ ms-unit
          ∎) ⟩
        𝕞𝕧𝕒𝕣 𝔛 𝔪 (λ v → □msub (ε v) ρ ms-unit)
    ∎ }
  } where open ≡-Reasoning

□msub-runit : (t : 𝕋 𝔛 α Γ)(ρ : Γ ↝ Δ)
           → □msub t ρ ms-unit ≡ 𝕣𝕖𝕟 𝔛 t ρ
□msub-runit {𝔛} t ρ = sym (cong (λ - → - ρ) (Renaming.𝕤𝕖𝕞! 𝔛 □msub-runitᵃ⇒ t))

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module RandomAccessList.Zeroless.Properties where

open import BuildingBlock
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf; split)
open import RandomAccessList.Zeroless.Core
open import RandomAccessList.Zeroless.Core.Properties
open import RandomAccessList.Zeroless

open import Data.Unit using (tt)
open import Data.Nat
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple
open import Data.Product as Prod

open import Function
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (False; True; fromWitnessFalse; fromWitness)
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning

tailₙ-suc : ∀ {n A} → (xs : 1-2-RAL A n) → (p : ⟦ xs ⟧ ≢ 0)
           → suc ⟦ tailₙ xs p ⟧ₙ ≡ ⟦ xs ⟧ₙ
tailₙ-suc {n} {A}    [] p = contradiction (⟦[]⟧≡0 ([] {A} {n}) refl) p
tailₙ-suc (x     1∷ xs) p with ⟦ xs ⟧ ≟ 0
tailₙ-suc {n} (x 1∷ xs) p | yes q =
    begin
        suc 0
    ≡⟨ cong suc (sym (*-right-zero 0)) ⟩
        suc (2 * 0)
    ≡⟨ cong (λ w → suc (2 * w)) (sym (no-zero-divisor (2 * 2 ^ n) ⟦ xs ⟧ₙ (m^n≢0 2 (suc n) (λ ())) q)) ⟩
        suc (2 * ⟦ xs ⟧ₙ)
    ∎
tailₙ-suc (x     1∷ xs) p | no ¬q =
    begin
        3 + 2 * ⟦ tailₙ xs ¬q ⟧ₙ
    ≡⟨ cong suc (sym (+-*-suc 2 ⟦ tailₙ xs ¬q ⟧ₙ)) ⟩
        1 + 2 * suc ⟦ tailₙ xs ¬q ⟧ₙ
    ≡⟨ cong (λ w → 1 + 2 * w) (tailₙ-suc xs ¬q) ⟩
        1 + (2 * ⟦ xs ⟧ₙ)
    ∎
tailₙ-suc (x , y 2∷ xs) p = refl

tail-suc : ∀ {A} → (xs : 1-2-RAL A 0) → (p : ⟦ xs ⟧ ≢ 0)
         → suc ⟦ tail xs p ⟧ ≡ ⟦ xs ⟧
tail-suc {A}        [] p = contradiction (⟦[]⟧≡0 ([] {A} {0}) refl) p
tail-suc (x     1∷ xs) p with ⟦ xs ⟧ ≟ 0
tail-suc (x     1∷ xs) p | yes q = cong (λ w → suc (w + 0)) (sym q)
tail-suc (x     1∷ xs) p | no ¬q =
    begin
        3 + 2 * ⟦ tailₙ xs ¬q ⟧ₙ + 0
    ≡⟨ cong (λ w → 1 + w + 0) (sym (+-*-suc 2 ⟦ tailₙ xs ¬q ⟧ₙ)) ⟩
        1 + 2 * suc ⟦ tailₙ xs ¬q ⟧ₙ + 0
    ≡⟨ cong (λ w → 1 + 2 * w + 0) (tailₙ-suc xs ¬q) ⟩
        1 + 2 * ⟦ xs ⟧ₙ + 0
    ∎
tail-suc (x , y 2∷ xs) p = refl

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

module HITs.PropositionalTruncation where

open import Cubical.HITs.PropositionalTruncation
  using (squash; ∥_∥; ∣_∣)
  renaming (recPropTrunc to rec; recPropTrunc→Set to rec→set)
  public


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

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

open import Util.Prelude
------------------------------------------------------------------------------
open import Agda.Builtin.Float

module LibraBFT.Impl.OBM.Rust.RustTypes where

-- TODO-2 : reasoning about integer overflow

F64 : Set
F64 = Float -- This is 'Double' in Haskell.  In Agda, 'Float' is represented as a Haskell 'Double'.

U64 : Set
U64 = ℕ

U128 : Set
U128 = ℕ

Usize : Set
Usize = ℕ

postulate -- TODO-1: VecDeque, vdNew
  VecDeque : Set
  vdNew : VecDeque


text:
-- Andreas, 2014-07-02 Documenting the ETA pragma

open import Common.Equality

mutual
  data Colist (A : Set) : Set where
    [] : Colist A
    _∷_ : A → ∞Colist A → Colist A

  record ∞Colist (A : Set) : Set where
    eta-equality
    coinductive
    constructor delay
    field       force : Colist A

open ∞Colist

-- By default, recursive records do not have eta,
-- but it can be turned on by force.
-- In case of colists, it is ok, since there is no
-- infinite eta-expansion (unlike for streams).

test : {A : Set} (x : ∞Colist A) → x ≡ delay (force x)
test x = refl


text:
record Foo : Set where
  cppattern                     -- Typo here
  no-eta-equality

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2016-12-30, issue #1886, reported by nad

-- {-# OPTIONS -v tc.data:40 -v scope.data.def:40 -v tc.decl:10 #-}

data D (X : Set) : Set

data D (X : Set Set) where

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- The "terminates" relation
------------------------------------------------------------------------

open import Atom

module Termination (atoms : χ-atoms) where

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

open import Chi           atoms
open import Deterministic atoms
open import Propositional atoms

-- Terminates e means that e terminates with a value.

Terminates : Exp → Type
Terminates p = ∃ λ v → p ⇓ v

-- This relation is propositional.

Terminates-propositional :
  ∀ {e} →
  Is-proposition (Terminates e)
Terminates-propositional (_ , e₁) (_ , e₂) =
  Σ-≡,≡→≡ (⇓-deterministic e₁ e₂)
          (⇓-propositional _ _)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi