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

open import HoTT
open import homotopy.LoopSpaceCircle
open import homotopy.PinSn
open import homotopy.SphereEndomorphism
open import homotopy.SuspAdjointLoop
open import groups.FromSusp
open import groups.Int
open import groups.Pointed
open import groups.SuspAdjointLoop
open import groups.ToOmega

module groups.SphereEndomorphism where

  ⊙SphereS-endo-group-structure : ∀ n → GroupStructure (⊙Sphere-endo (S n))
  ⊙SphereS-endo-group-structure n = Susp⊙→-group-structure (⊙Sphere n) (⊙Sphere (S n))

{-
  ⊙LiftSphereS-endo-group-structure : ∀ {i} n → GroupStructure (⊙LiftSphere-endo {i} (S n))
  ⊙LiftSphereS-endo-group-structure {i} n =
    LiftSusp⊙→-group-structure {j = i} (⊙Sphere n) (⊙Lift {j = i} (⊙Sphere (S n)))

  ⊙SphereS-endo-siso-⊙LiftSphereS-endo : ∀ {i} n →
    ⊙SphereS-endo-group-structure n ≃ᴳˢ ⊙LiftSphereS-endo-group-structure {i} n
  ⊙SphereS-endo-siso-⊙LiftSphereS-endo {i} n = ≃-to-≃ᴳˢ
    ⊙Lift-fmap-equiv
    (λ f g → ap (_⊙∘ ⊙pinch (⊙Sphere n) ⊙∘ ⊙lower {j = i}) $ ! $
      ⊙∨-rec (⊙Lift-fmap f) (⊙Lift-fmap g) ⊙∘ ⊙∨-fmap ⊙lift ⊙lift
        =⟨ ⊙λ= $ ⊙∨-rec-fmap (⊙Lift-fmap f) (⊙Lift-fmap g) ⊙lift ⊙lift ⟩
      ⊙∨-rec (⊙lift ⊙∘ f) (⊙lift ⊙∘ g)
        =⟨ ! $ ⊙λ= $ ⊙∨-rec-post∘ ⊙lift f g ⟩
      ⊙lift ⊙∘ ⊙∨-rec f g
        =∎)
-}

  Trunc-⊙SphereS-endo-group : ∀ n → Group₀
  Trunc-⊙SphereS-endo-group n = Trunc-Susp⊙→-group (⊙Sphere n) (⊙Sphere (S n))

{-
  Trunc-⊙LiftSphereS-endo-group : ∀ {i} n → Group i
  Trunc-⊙LiftSphereS-endo-group {i} n = Trunc-LiftSusp⊙→-group {j = i} (⊙Sphere n) (⊙Lift {j = i} (⊙Sphere (S n)))
-}

  Trunc-⊙SphereS-endo-⊙group : ∀ n → ⊙Group₀
  Trunc-⊙SphereS-endo-⊙group n = ⊙[ Trunc-⊙SphereS-endo-group n , [ ⊙idf _ ] ]ᴳ

{-
  Trunc-⊙LiftSphereS-endo-⊙group : ∀ {i} n → ⊙Group i
  Trunc-⊙LiftSphereS-endo-⊙group {i} n = ⊙[ Trunc-⊙LiftSphereS-endo-group {i = i} n , [ ⊙idf _ ] ]ᴳ
-}

  Trunc-⊙S¹-endo-group-iso-ℤ : Trunc-⊙SphereS-endo-group 0 ≃ᴳ ℤ-group
  Trunc-⊙S¹-endo-group-iso-ℤ =
    Trunc-⊙SphereS-endo-group 0
      ≃ᴳ⟨ Trunc-Susp⊙→-iso-Trunc-⊙→Ω ⊙Bool ⊙S¹ ⟩
    Trunc-⊙→Ω-group ⊙Bool ⊙S¹
      ≃ᴳ⟨ Trunc-⊙Bool→Ω-iso-π₁ ⊙S¹ ⟩
    πS 0 ⊙S¹
      ≃ᴳ⟨ πS-SphereS-iso-ℤ 0 ⟩
    ℤ-group
      ≃ᴳ∎

  Trunc-⊙S¹-endo-⊙group-iso-⊙ℤ : Trunc-⊙SphereS-endo-⊙group 0 ⊙≃ᴳ ℤ-⊙group
  Trunc-⊙S¹-endo-⊙group-iso-⊙ℤ = Trunc-⊙S¹-endo-group-iso-ℤ ,
    equiv-adj' ΩS¹-equiv-ℤ {a = ap (idf _) loop} {b = 1} (ap-idf loop)

  Trunc-⊙S¹-endo-⊙group-is-infinite-cyclic : is-infinite-cyclic (Trunc-⊙SphereS-endo-⊙group 0)
  Trunc-⊙S¹-endo-⊙group-is-infinite-cyclic =
    isomorphism-preserves'-infinite-cyclic Trunc-⊙S¹-endo-⊙group-iso-⊙ℤ ℤ-is-infinite-cyclic

  Trunc-⊙SphereS-endo-Susp-fmap-iso :
    ∀ n → Trunc-⊙SphereS-endo-group n ≃ᴳ Trunc-⊙SphereS-endo-group (S n)
  Trunc-⊙SphereS-endo-Susp-fmap-iso n =
    Trunc-group-fmap (Susp⊙→-Susp-fmap-shom (⊙Sphere n) (⊙Sphere (S n))) ,
    Trunc-⊙SphereS-endo-Susp-is-equiv n

  Trunc-⊙SphereS-endo-Susp-fmap-⊙iso :
    ∀ n → Trunc-⊙SphereS-endo-⊙group n ⊙≃ᴳ Trunc-⊙SphereS-endo-⊙group (S n)
  Trunc-⊙SphereS-endo-Susp-fmap-⊙iso n =
    Trunc-⊙SphereS-endo-Susp-fmap-iso n , ap [_] (⊙Susp-fmap-idf (⊙Sphere (S n)))

  Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic : ∀ n → is-infinite-cyclic (Trunc-⊙SphereS-endo-⊙group n)
  Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic O = Trunc-⊙S¹-endo-⊙group-is-infinite-cyclic
  Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic (S n) =
    isomorphism-preserves-infinite-cyclic
      (Trunc-⊙SphereS-endo-Susp-fmap-⊙iso n)
      (Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic n)

{-
  Trunc-⊙SphereS-endo-iso-Trunc-⊙LiftSphereS-endo : ∀ {i} n →
    Trunc-⊙SphereS-endo-group n ≃ᴳ Trunc-⊙LiftSphereS-endo-group {i} n
  Trunc-⊙SphereS-endo-iso-Trunc-⊙LiftSphereS-endo {i} n =
    Trunc-group-emap (⊙SphereS-endo-siso-⊙LiftSphereS-endo {i} n)

  Trunc-⊙SphereS-endo-⊙iso-Trunc-⊙LiftSphereS-endo : ∀ {i} n →
    Trunc-⊙SphereS-endo-⊙group n ⊙≃ᴳ Trunc-⊙LiftSphereS-endo-⊙group {i} n
  Trunc-⊙SphereS-endo-⊙iso-Trunc-⊙LiftSphereS-endo {i} n =
    Trunc-⊙SphereS-endo-iso-Trunc-⊙LiftSphereS-endo {i} n , idp

  Trunc-⊙LiftSphereS-endo-⊙group-is-infinite-cyclic : ∀ {i} n → is-infinite-cyclic (Trunc-⊙LiftSphereS-endo-⊙group {i} n)
  Trunc-⊙LiftSphereS-endo-⊙group-is-infinite-cyclic {i} n =
    isomorphism-preserves-infinite-cyclic
      (Trunc-⊙SphereS-endo-⊙iso-Trunc-⊙LiftSphereS-endo {i} n)
      (Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic n)
-}

  {- definition of degree -}

  Trunc-⊙SphereS-endo-degree : ∀ n → Trunc-⊙Sphere-endo (S n) → ℤ
  Trunc-⊙SphereS-endo-degree n = is-equiv.g (Trunc-⊙SphereS-endo-⊙group-is-infinite-cyclic n)

  abstract
    Trunc-⊙SphereS-endo-degree-Susp : ∀ n f
      →  Trunc-⊙SphereS-endo-degree (S n) (Trunc-fmap ⊙Susp-fmap f)
      == Trunc-⊙SphereS-endo-degree n f
    Trunc-⊙SphereS-endo-degree-Susp n f =
      ap (Trunc-⊙SphereS-endo-degree n) (GroupIso.g-f (Trunc-⊙SphereS-endo-Susp-fmap-iso n) f)

  ⊙SphereS-endo-degree : ∀ n → ⊙Sphere-endo (S n) → ℤ
  ⊙SphereS-endo-degree n = Trunc-⊙SphereS-endo-degree n ∘ [_]

  abstract
    ⊙SphereS-endo-degree-Susp : ∀ n f
      →  ⊙SphereS-endo-degree (S n) (⊙Susp-fmap f)
      == ⊙SphereS-endo-degree n f
    ⊙SphereS-endo-degree-Susp n f = Trunc-⊙SphereS-endo-degree-Susp n [ f ]

    ⊙SphereS-endo-degree-Susp' : ∀ n f
      →  ⊙SphereS-endo-degree (S n) (Susp-fmap f , idp)
      == Trunc-⊙SphereS-endo-degree n (Trunc-⊙SphereS-endo-in n [ f ])
    ⊙SphereS-endo-degree-Susp' n f =
      ⊙SphereS-endo-degree (S n) (Susp-fmap f , idp)
        =⟨ ap
            (Trunc-⊙SphereS-endo-degree (S n) ∘ Trunc-fmap (λ f → Susp-fmap f , idp))
            (! $ is-equiv.f-g (Trunc-⊙SphereS-endo-out-is-equiv n) [ f ]) ⟩
      Trunc-⊙SphereS-endo-degree (S n) (Trunc-fmap (λ f → Susp-fmap f , idp) (Trunc-fmap fst (Trunc-⊙SphereS-endo-in n [ f ])))
        =⟨ ap (Trunc-⊙SphereS-endo-degree (S n))
            (Trunc-fmap-∘ (λ f → Susp-fmap f , idp) fst (Trunc-⊙SphereS-endo-in n [ f ])) ⟩
      Trunc-⊙SphereS-endo-degree (S n) (Trunc-fmap ⊙Susp-fmap (Trunc-⊙SphereS-endo-in n [ f ]))
        =⟨ Trunc-⊙SphereS-endo-degree-Susp n (Trunc-⊙SphereS-endo-in n [ f ]) ⟩
      Trunc-⊙SphereS-endo-degree n (Trunc-⊙SphereS-endo-in n [ f ])
        =∎

    ⊙SphereS-endo-degree-base-indep : ∀ n {f g}
      → fst f ∼ fst g
      → ⊙SphereS-endo-degree n f == ⊙SphereS-endo-degree n g
    ⊙SphereS-endo-degree-base-indep n {f} {g} f∼g =
      ! (⊙SphereS-endo-degree-Susp n f)
      ∙ ap (λ f → ⊙SphereS-endo-degree (S n) (Susp-fmap f , idp)) (λ= f∼g)
      ∙ ⊙SphereS-endo-degree-Susp n g

{-
  Trunc-⊙LiftSphereS-endo-degree : ∀ {i} n → Trunc-⊙LiftSphere-endo {i} (S n) → ℤ
  Trunc-⊙LiftSphereS-endo-degree {i} n = is-equiv.g (Trunc-⊙LiftSphereS-endo-⊙group-is-infinite-cyclic {i} n)

  abstract
    Trunc-⊙LiftSphereS-endo-degree-Susp : ∀ {i} n f
      →  Trunc-⊙LiftSphereS-endo-degree {i} (S n) (Trunc-fmap (λ f → ⊙Lift-fmap (⊙Susp-fmap (⊙lower ⊙∘ f ⊙∘ ⊙lift))) f)
      == Trunc-⊙LiftSphereS-endo-degree {i} n f
    Trunc-⊙LiftSphereS-endo-degree-Susp {i} n =
      Trunc-elim
        {{λ _ → =-preserves-level ℤ-is-set}}
        (λ f → ⊙SphereS-endo-degree-Susp n (⊙lower ⊙∘ f ⊙∘ ⊙lift))

  ⊙LiftSphereS-endo-degree : ∀ {i} n → ⊙LiftSphere-endo {i} (S n) → ℤ
  ⊙LiftSphereS-endo-degree {i} n = Trunc-⊙LiftSphereS-endo-degree {i} n ∘ [_]

  abstract
    ⊙LiftSphereS-endo-degree-Susp : ∀ {i} n f
      →  ⊙LiftSphereS-endo-degree {i} (S n) (⊙Lift-fmap (⊙Susp-fmap (⊙lower ⊙∘ f ⊙∘ ⊙lift)))
      == ⊙LiftSphereS-endo-degree {i} n f
    ⊙LiftSphereS-endo-degree-Susp {i} n f =
      Trunc-⊙LiftSphereS-endo-degree-Susp {i} n [ f ]

    ⊙LiftSphereS-endo-degree-base-indep : ∀ {i} n {f g}
      → fst f ∼ fst g
      → ⊙LiftSphereS-endo-degree {i} n f == ⊙LiftSphereS-endo-degree {i} n g
    ⊙LiftSphereS-endo-degree-base-indep {i} n {f} {g} f∼g =
      ! (⊙LiftSphereS-endo-degree-Susp {i} n f)
      ∙ ap (λ f → ⊙LiftSphereS-endo-degree {i} (S n) (⊙Lift-fmap (Susp-fmap (lower ∘ f ∘ lift) , idp))) (λ= f∼g)
      ∙ ⊙LiftSphereS-endo-degree-Susp {i} n g
-}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Properties.AbelianGroup
         {g₁ g₂} (G : AbelianGroup g₁ g₂) where

import Algebra.Properties.Group as GP
open import Data.Product
open import Function
import Relation.Binary.EqReasoning as EqR

open AbelianGroup G
open EqR setoid

open GP group public

private
  lemma : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
  lemma x y = begin
    x ∙ y ∙ x ⁻¹    ≈⟨ comm _ _ ⟨ ∙-cong ⟩ refl ⟩
    y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩
    y ∙ (x ∙ x ⁻¹)  ≈⟨ refl ⟨ ∙-cong ⟩ proj₂ inverse _ ⟩
    y ∙ ε           ≈⟨ proj₂ identity _ ⟩
    y               ∎

⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
⁻¹-∙-comm x y = begin
  x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩
  y ⁻¹ ∙ x ⁻¹                         ≈⟨ sym $ lem ⟨ ∙-cong ⟩ refl ⟩
  x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma _ _ ⟩
  y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹               ≈⟨ lemma _ _ ⟩
  (x ∙ y) ⁻¹                          ∎
  where
  lem = begin
    x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹)  ≈⟨ sym $ assoc _ _ _ ⟩
    x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹  ≈⟨ sym $ assoc _ _ _ ⟨ ∙-cong ⟩ refl ⟩
    x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹    ≈⟨ proj₂ inverse _ ⟨ ∙-cong ⟩ refl ⟩
    ε ∙ y ⁻¹                     ≈⟨ proj₁ identity _ ⟩
    y ⁻¹                         ∎

ext: agda


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 LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block              as Block
import      LibraBFT.Impl.Consensus.ConsensusTypes.TimeoutCertificate as TimeoutCertificate
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Hash
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                               using (String)

module LibraBFT.Impl.Consensus.ConsensusTypes.ProposalMsg where

verifyWellFormed : ProposalMsg → Either ErrLog Unit
verifyWellFormed self = do
  lcheck (not (Block.isNilBlock (self ^∙ pmProposal)))
         (here' ("Proposal for a NIL block" ∷ []))
  withErrCtx' ("Failed to verify ProposalMsg's block" ∷ [])
              (Block.verifyWellFormed (self ^∙ pmProposal))
  lcheck (self ^∙ pmProposal ∙ bRound >? 0)
         (here' ("Proposal for has round <= 0" ∷ []))
  lcheck (self ^∙ pmProposal ∙ bEpoch == self ^∙ pmSyncInfo ∙ siEpoch)
         (here' ("ProposalMsg has different epoch than SyncInfo" ∷ [])) -- lsSI (self ^∙ pmSyncInfo)

  lcheck (self ^∙ pmProposal ∙ bParentId == self ^∙ pmSyncInfo ∙ siHighestQuorumCert ∙ qcCertifiedBlock ∙ biId)
         (here' ( "Proposal SyncInfo HQC CertifiedBlock id not eq to block parent id" ∷ []))
               -- lsSI (self ^∙ pmSyncInfo)
  let previousRound = self ^∙ pmProposal ∙ bRound ∸ 1 -- NOTE: monus usage
  let highestCertifiedRound =
        max (self ^∙ pmProposal ∙ bQuorumCert ∙ qcCertifiedBlock ∙ biRound)
            (maybe 0 (_^∙ tcRound) (self ^∙ pmSyncInfo ∙ siHighestTimeoutCert))
  lcheck (previousRound == highestCertifiedRound)
         (here' ("Proposal does not have a certified round" ∷ []))
               -- lsMTC (self ^∙ pmSyncInfo ∙ siHighestTimeoutCert)
  lcheck (is-just (self ^∙ pmProposal ∙ bAuthor))
         (here' ("Proposal does not have an author" ∷ []))
  -- LBFT-DIFF : this check used to live in EventProcessor ∙ processProposedBlockM
  -- TODO: is it needed?
  -- Safety invariant: For any valid proposed block
  -- , its parent block == the block pointed to by its QC.
  lcheck (self ^∙ pmProposal ∙ bParentId == self ^∙ pmProposal ∙ bQuorumCert ∙ qcCertifiedBlock ∙ biId)
         (here' ("parent id /= qcCB" ∷ [])) -- show (self ^∙ pmProposal)
 where
  here' : List String → List String
  here' t = "ProposalMsg" ∷ "verifyWellFormed" {-∷ lsPM self-} ∷ t

verify : ProposalMsg → ValidatorVerifier → Either ErrLog Unit
verify self validator = do
  Block.validateSignature    (self ^∙ pmProposal)                        validator
  TimeoutCertificate.verify' (self ^∙ pmSyncInfo ∙ siHighestTimeoutCert) validator
  verifyWellFormed self


text:
module Issue2487 where

open import Issue2487.b

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module nodcap.Base where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺ using (ℕ⁺; suc; _+_)
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.List.Any using (Any; here; there)
open import Data.List.Any.Membership.Propositional using (_∈_; _∼[_]_; bag)
open import Data.Product using (_×_; _,_; uncurry; map)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (id; _$_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- Types.

data Type : Set where
  𝟏 : Type
  ⊥ : Type
  𝟎 : Type
  ⊤ : Type
  _⊗_ : (A B : Type) → Type
  _⅋_ : (A B : Type) → Type
  _⊕_ : (A B : Type) → Type
  _&_ : (A B : Type) → Type
  ![_]_ : (n : ℕ⁺) (A : Type) → Type
  ?[_]_ : (n : ℕ⁺) (A : Type) → Type

-- Duality.

_^ : Type → Type
𝟏 ^ = ⊥
⊥ ^ = 𝟏
𝟎 ^ = ⊤
⊤ ^ = 𝟎
(A ⊗ B) ^ = (A ^) ⅋ (B ^)
(A ⅋ B) ^ = (A ^) ⊗ (B ^)
(A ⊕ B) ^ = (A ^) & (B ^)
(A & B) ^ = (A ^) ⊕ (B ^)
(![ n ] A) ^ = ?[ n ] (A ^)
(?[ n ] A) ^ = ![ n ] (A ^)

^-inv : (A : Type) → A ^ ^ ≡ A
^-inv 𝟏 = P.refl
^-inv ⊥ = P.refl
^-inv 𝟎 = P.refl
^-inv ⊤ = P.refl
^-inv (A ⊗ B) = P.cong₂ _⊗_ (^-inv A) (^-inv B)
^-inv (A ⅋ B) = P.cong₂ _⅋_ (^-inv A) (^-inv B)
^-inv (A ⊕ B) = P.cong₂ _⊕_ (^-inv A) (^-inv B)
^-inv (A & B) = P.cong₂ _&_ (^-inv A) (^-inv B)
^-inv (![ n ] A) = P.cong ![ n ]_ (^-inv A)
^-inv (?[ n ] A) = P.cong ?[ n ]_ (^-inv A)

-- Lollipop.

_⊸_ : (A B : Type) → Type
A ⊸ B = (A ^) ⅋ B

-- Polarity.

data Pos : (A : Type) → Set where
  𝟎 : Pos 𝟎
  𝟏 : Pos 𝟏
  _⊗_ : (A B : Type) → Pos (A ⊗ B)
  _⊕_ : (A B : Type) → Pos (A ⊕ B)
  ![_]_ : (n : ℕ⁺) (A : Type) → Pos (![ n ] A)

data Neg : (A : Type) → Set where
  ⊥ : Neg ⊥
  ⊤ : Neg ⊤
  _⅋_ : (A B : Type) → Neg (A ⅋ B)
  _&_ : (A B : Type) → Neg (A & B)
  ?[_]_ : (n : ℕ⁺) (A : Type) → Neg (?[ n ] A)

pol? : (A : Type) → Pos A ⊎ Neg A
pol? 𝟏 = inj₁ 𝟏
pol? ⊥ = inj₂ ⊥
pol? 𝟎 = inj₁ 𝟎
pol? ⊤ = inj₂ ⊤
pol? (A ⊗ B) = inj₁ (A ⊗ B)
pol? (A ⅋ B) = inj₂ (A ⅋ B)
pol? (A ⊕ B) = inj₁ (A ⊕ B)
pol? (A & B) = inj₂ (A & B)
pol? (![ n ] A) = inj₁ (![ n ] A)
pol? (?[ n ] A) = inj₂ (?[ n ] A)

^-posneg : {A : Type} (P : Pos A) → Neg (A ^)
^-posneg 𝟎 = ⊤
^-posneg 𝟏 = ⊥
^-posneg (A ⊗ B) = (A ^) ⅋ (B ^)
^-posneg (A ⊕ B) = (A ^) & (B ^)
^-posneg (![ n ] A) = ?[ n ] (A ^)

^-negpos : {A : Type} (N : Neg A) → Pos (A ^)
^-negpos ⊥ = 𝟏
^-negpos ⊤ = 𝟎
^-negpos (A ⅋ B) = (A ^) ⊗ (B ^)
^-negpos (A & B) = (A ^) ⊕ (B ^)
^-negpos (?[ n ] A) = ![ n ] (A ^)

-- Environments.

Environment : Set
Environment = List Type

-- Injectivity.

private
  infix 10 _≈_

  _≈_ : Type → Type → Set
  A ≈ B = A ≡ B

⊗-inj : {A B C D : Type} → A ⊗ B ≈ C ⊗ D → A ≈ C × B ≈ D
⊗-inj P.refl = P.refl , P.refl

⅋-inj : {A B C D : Type} → A ⅋ B ≈ C ⅋ D → A ≈ C × B ≈ D
⅋-inj P.refl = P.refl , P.refl

⊕-inj : {A B C D : Type} → A ⊕ B ≈ C ⊕ D → A ≈ C × B ≈ D
⊕-inj P.refl = P.refl , P.refl

&-inj : {A B C D : Type} → A & B ≈ C & D → A ≈ C × B ≈ D
&-inj P.refl = P.refl , P.refl

!-inj : {A B : Type} {m n : ℕ⁺} → ![ m ] A ≈ ![ n ] B → m ≡ n × A ≈ B
!-inj P.refl = P.refl , P.refl

?-inj : {A B : Type} {m n : ℕ⁺} → ?[ m ] A ≈ ?[ n ] B → m ≡ n × A ≈ B
?-inj P.refl = P.refl , P.refl

-- This is one of those proofs for which I wish Agda had tactics.

^-inj : {A B : Type} → A ^ ≈ B ^ → A ≈ B
^-inj {A = 𝟏}        {B = 𝟏}         p = P.refl
^-inj {A = 𝟏}        {B = ⊥}         ()
^-inj {A = 𝟏}        {B = 𝟎}         ()
^-inj {A = 𝟏}        {B = ⊤}         ()
^-inj {A = 𝟏}        {B = C ⊗ D}     ()
^-inj {A = 𝟏}        {B = C ⅋ D}     ()
^-inj {A = 𝟏}        {B = C ⊕ D}     ()
^-inj {A = 𝟏}        {B = C & D}     ()
^-inj {A = 𝟏}        {B = ![ n ] C}  ()
^-inj {A = 𝟏}        {B = ?[ n ] C}  ()
^-inj {A = ⊥}        {B = 𝟏}         ()
^-inj {A = ⊥}        {B = ⊥}         p = P.refl
^-inj {A = ⊥}        {B = 𝟎}         ()
^-inj {A = ⊥}        {B = ⊤}         ()
^-inj {A = ⊥}        {B = C ⊗ D}     ()
^-inj {A = ⊥}        {B = C ⅋ D}     ()
^-inj {A = ⊥}        {B = C ⊕ D}     ()
^-inj {A = ⊥}        {B = C & D}     ()
^-inj {A = ⊥}        {B = ![ n ] C}  ()
^-inj {A = ⊥}        {B = ?[ n ] C}  ()
^-inj {A = 𝟎}        {B = 𝟏}         ()
^-inj {A = 𝟎}        {B = ⊥}         ()
^-inj {A = 𝟎}        {B = 𝟎}         p = P.refl
^-inj {A = 𝟎}        {B = ⊤}         ()
^-inj {A = 𝟎}        {B = C ⊗ D}     ()
^-inj {A = 𝟎}        {B = C ⅋ D}     ()
^-inj {A = 𝟎}        {B = C ⊕ D}     ()
^-inj {A = 𝟎}        {B = C & D}     ()
^-inj {A = 𝟎}        {B = ![ n ] C}  ()
^-inj {A = 𝟎}        {B = ?[ n ] C}  ()
^-inj {A = ⊤}        {B = 𝟏}         ()
^-inj {A = ⊤}        {B = ⊥}         ()
^-inj {A = ⊤}        {B = 𝟎}         ()
^-inj {A = ⊤}        {B = ⊤}         p = P.refl
^-inj {A = ⊤}        {B = C ⊗ D}     ()
^-inj {A = ⊤}        {B = C ⅋ D}     ()
^-inj {A = ⊤}        {B = C ⊕ D}     ()
^-inj {A = ⊤}        {B = C & D}     ()
^-inj {A = ⊤}        {B = ![ n ] C}  ()
^-inj {A = ⊤}        {B = ?[ n ] C}  ()
^-inj {A = A ⊗ B}    {B = 𝟏}         ()
^-inj {A = A ⊗ B}    {B = ⊥}         ()
^-inj {A = A ⊗ B}    {B = 𝟎}         ()
^-inj {A = A ⊗ B}    {B = ⊤}         ()
^-inj {A = A ⊗ B}    {B = C ⊗ D}     p = uncurry (P.cong₂ _⊗_) (map ^-inj ^-inj (⅋-inj p))
^-inj {A = A ⊗ B}    {B = C ⅋ D}     ()
^-inj {A = A ⊗ B}    {B = C ⊕ D}     ()
^-inj {A = A ⊗ B}    {B = C & D}     ()
^-inj {A = A ⊗ B}    {B = ![ n ] C}  ()
^-inj {A = A ⊗ B}    {B = ?[ n ] C}  ()
^-inj {A = A ⅋ B}    {B = 𝟏}         ()
^-inj {A = A ⅋ B}    {B = ⊥}         ()
^-inj {A = A ⅋ B}    {B = 𝟎}         ()
^-inj {A = A ⅋ B}    {B = ⊤}         ()
^-inj {A = A ⅋ B}    {B = C ⊗ D}     ()
^-inj {A = A ⅋ B}    {B = C ⅋ D}     p = uncurry (P.cong₂ _⅋_) (map ^-inj ^-inj (⊗-inj p))
^-inj {A = A ⅋ B}    {B = C ⊕ D}     ()
^-inj {A = A ⅋ B}    {B = C & D}     ()
^-inj {A = A ⅋ B}    {B = ![ n ] C}  ()
^-inj {A = A ⅋ B}    {B = ?[ n ] C}  ()
^-inj {A = A ⊕ B}    {B = 𝟏}         ()
^-inj {A = A ⊕ B}    {B = ⊥}         ()
^-inj {A = A ⊕ B}    {B = 𝟎}         ()
^-inj {A = A ⊕ B}    {B = ⊤}         ()
^-inj {A = A ⊕ B}    {B = C ⊗ D}     ()
^-inj {A = A ⊕ B}    {B = C ⅋ D}     ()
^-inj {A = A ⊕ B}    {B = C ⊕ D}     p = uncurry (P.cong₂ _⊕_) (map ^-inj ^-inj (&-inj p))
^-inj {A = A ⊕ B}    {B = C & D}     ()
^-inj {A = A ⊕ B}    {B = ![ n ] C}  ()
^-inj {A = A ⊕ B}    {B = ?[ n ] C}  ()
^-inj {A = A & B}    {B = 𝟏}         ()
^-inj {A = A & B}    {B = ⊥}         ()
^-inj {A = A & B}    {B = 𝟎}         ()
^-inj {A = A & B}    {B = ⊤}         ()
^-inj {A = A & B}    {B = C ⊗ D}     ()
^-inj {A = A & B}    {B = C ⅋ D}     ()
^-inj {A = A & B}    {B = C ⊕ D}     ()
^-inj {A = A & B}    {B = C & D}     p = uncurry (P.cong₂ _&_) (map ^-inj ^-inj (⊕-inj p))
^-inj {A = A & B}    {B = ![ n ] C}  ()
^-inj {A = A & B}    {B = ?[ n ] C}  ()
^-inj {A = ![ m ] A} {B = 𝟏}         ()
^-inj {A = ![ m ] A} {B = ⊥}         ()
^-inj {A = ![ m ] A} {B = 𝟎}         ()
^-inj {A = ![ m ] A} {B = ⊤}         ()
^-inj {A = ![ m ] A} {B = C ⊗ D}     ()
^-inj {A = ![ m ] A} {B = C ⅋ D}     ()
^-inj {A = ![ m ] A} {B = C ⊕ D}     ()
^-inj {A = ![ m ] A} {B = C & D}     ()
^-inj {A = ![ m ] A} {B = ![ n ] C}  p = uncurry (P.cong₂ ![_]_) (map id ^-inj (?-inj p))
^-inj {A = ![ m ] A} {B = ?[ n ] C}  ()
^-inj {A = ?[ m ] A} {B = 𝟏}         ()
^-inj {A = ?[ m ] A} {B = ⊥}         ()
^-inj {A = ?[ m ] A} {B = 𝟎}         ()
^-inj {A = ?[ m ] A} {B = ⊤}         ()
^-inj {A = ?[ m ] A} {B = C ⊗ D}     ()
^-inj {A = ?[ m ] A} {B = C ⅋ D}     ()
^-inj {A = ?[ m ] A} {B = C ⊕ D}     ()
^-inj {A = ?[ m ] A} {B = C & D}     ()
^-inj {A = ?[ m ] A} {B = ![ n ] C}  ()
^-inj {A = ?[ m ] A} {B = ?[ n ] C}  p = uncurry (P.cong₂ ?[_]_) (map id ^-inj (!-inj p))

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Sigma

{- Some miscellaneous lemmas for types with decidable equality. -}
module Util.DecEq where

×-has-dec-eq : {i j : ULevel} {A : Type i} {B : Type j} → (has-dec-eq A) → (has-dec-eq B) →
  (has-dec-eq (A × B))

×-has-dec-eq Adec Bdec (a , b) (a' , b') =
  ⊔-rec (⊔-rec (λ p q → inl (pair×= q p)) (λ f _ → inr (λ p → f (ap snd p))) (Bdec b b'))
        (λ f → inr (λ p → f (ap fst p))) (Adec a a')

equiv-preserves-dec-eq : {i j : ULevel} {A : Type i} {B : Type j} → (A ≃ B) → (has-dec-eq B) →
  has-dec-eq A

equiv-preserves-dec-eq e Adec a a' = ⊔-rec (λ p → inl (–>-is-inj e a a' p))
  (λ f → inr (λ p → f (ap (–> e) p))) (Adec (–> e a) (–> e a'))

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
module Category.Core where

open import Level
open import Data.Product
-- open import Relation.Binary as B using ()
open import Relation.Binary as B using ()
open import Relation.Binary.Indexed
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)

record IsMorphism   {𝒸 ℓ : Level}
                    {Object : Set 𝒸}
                    {Carrier : (Object × Object) → Set 𝒸}
                    (_≈_ : Rel Carrier ℓ)
                    (_∘_ : ∀ {a b c} → Carrier (b , c) → Carrier (a , b) → Carrier (a , c))
                    (id : (a : Object) → Carrier (a , a))
                    : Set (suc (𝒸 ⊔ ℓ)) where
    _⇒_ = curry Carrier
    field
        assoc : ∀ {a b c d : Object}
            → (f : a ⇒ b) → (g : b ⇒ c) → (h : c ⇒ d)
            → ((h ∘ g) ∘ f) ≈ (h ∘ (g ∘ f))
        left-identity : ∀ {a b : Object}
            → (f : a ⇒ b)
            → (id b ∘ f) ≈ f
        right-identity : ∀ {a b : Object}
            → (f : a ⇒ b)
            → (f ∘ id a) ≈ f
        cong : ∀ {a b c a' b' c' : Object}
            {x : Carrier (b , c)} {y : Carrier (b' , c')}
            {u : Carrier (a , b)} {v : Carrier (a' , b')}
            → x ≈ y → u ≈ v → (x ∘ u) ≈ (y ∘ v)

record MorphismStructure (𝒸 ℓ : Level) (Object : Set 𝒸) : Set (suc (𝒸 ⊔ ℓ)) where
    infixr 9 _∘_
    infix 4 _≈_
    field
        Carrier : (Object × Object) → Set 𝒸
        _≈_ : Rel Carrier ℓ
        isEquivalence : IsEquivalence Carrier _≈_

    setoid : Setoid (Object × Object) _ _
    setoid = record { isEquivalence = isEquivalence }

    -- Arrows
    _⇒_ : Object → Object → Set 𝒸
    _⇒_ = curry Carrier

    field
        _∘_ : ∀ {a b c : Object}
            → b ⇒ c
            → a ⇒ b
            → a ⇒ c
        id : (a : Object) → a ⇒ a
        isMorphism : IsMorphism _≈_ _∘_ id

record Category (𝒸 ℓ : Level) : Set (suc (𝒸 ⊔ ℓ)) where

    field
        Objects : B.Setoid 𝒸 ℓ

    Object : Set 𝒸
    Object = B.Setoid.Carrier Objects

    _≈o_ : Object → Object → Set ℓ
    _≈o_ = B.Setoid._≈_ Objects

    field
        Morphisms : MorphismStructure 𝒸 ℓ Object

    open MorphismStructure Morphisms public

    hom[-,_] : Object → Set 𝒸
    hom[-, b ] = Σ[ a ∈ Object ] a ⇒ b

    -- hom[_,_] : Object → Object → Set 𝒸
    -- hom[ a , b ] = a ⇒ b

record IsFunctor {𝒸₀ ℓ₀ 𝒸₁ ℓ₁ : Level}
    {C : Category 𝒸₀ ℓ₀} {D : Category 𝒸₁ ℓ₁}
    (mapObject : Category.Object C → Category.Object D)
    (mapMorphism : ∀ {a b}
            → (Category._⇒_ C) a             b
            → (Category._⇒_ D) (mapObject a) (mapObject b))
    : Set (𝒸₀ ⊔ ℓ₀ ⊔ 𝒸₁ ⊔ ℓ₁) where

    module C = Category C
    open Category D

    field
        preserve-id : (a : C.Object)
            → mapMorphism (C.id a) ≈ id (mapObject a)
        preserve-∘ : {a b c : C.Object} (f : a C.⇒ b) (g : b C.⇒ c)
            → mapMorphism (C._∘_ g f) ≈ mapMorphism g ∘ mapMorphism f

record Functor {𝒸₀ ℓ₀ 𝒸₁ ℓ₁ : Level}
    (C : Category 𝒸₀ ℓ₀) (D : Category 𝒸₁ ℓ₁) : Set (𝒸₀ ⊔ ℓ₀ ⊔ 𝒸₁ ⊔ ℓ₁) where
    module C = Category C
    module D = Category D
    field
        mapObject : C.Object → D.Object
        mapMorphism : ∀ {a b} → a C.⇒ b → mapObject a D.⇒ mapObject b
        isFunctor : IsFunctor {𝒸₀} {ℓ₀} {𝒸₁} {ℓ₁} {C} {D} mapObject mapMorphism

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Monads on indexed sets (predicates)
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

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

module Category.Monad.Predicate where

open import Category.Applicative.Indexed
open import Category.Monad
open import Category.Monad.Indexed
open import Data.Unit
open import Data.Product
open import Function
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)

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

record RawPMonad {i ℓ} {I : Set i} (M : Pt I (i ⊔ ℓ)) :
                 Set (suc i ⊔ suc ℓ) where

  infixl 1 _?>=_ _?>_ _>?>_
  infixr 1 _=<?_ _<?<_

  -- ``Demonic'' operations (the opponent chooses the state).

  field
    return? : ∀ {P} → P ⊆ M P
    _=<?_   : ∀ {P Q} → P ⊆ M Q → M P ⊆ M Q

  _?>=_ : ∀ {P Q} → M P ⊆ const (P ⊆ M Q) ⇒ M Q
  m ?>= f = f =<? m

  _?>=′_ : ∀ {P Q} → M P ⊆ const (∀ j → {_ : P j} → j ∈ M Q) ⇒ M Q
  m ?>=′ f = m ?>= λ {j} p → f j {p}

  _?>_ : ∀ {P Q} → M P ⊆ const (∀ {j} → j ∈ M Q) ⇒ M Q
  m₁ ?> m₂ = m₁ ?>= λ _ → m₂

  join? : ∀ {P} → M (M P) ⊆ M P
  join? m = m ?>= id

  _>?>_ : {P Q R : _} → P ⊆ M Q → Q ⊆ M R → P ⊆ M R
  f >?> g = _=<?_ g ∘ f

  _<?<_ : ∀ {P Q R} → Q ⊆ M R → P ⊆ M Q → P ⊆ M R
  g <?< f = f >?> g

  -- ``Angelic'' operations (the player knows the state).

  rawIMonad : RawIMonad (λ i j A → i ∈ M (const A ∩ ｛ j ｝))
  rawIMonad = record
    { return = λ x → return? (x , refl)
    ; _>>=_  = λ m k → m ?>= λ { {._} (x , refl) → k x }
    }

  open RawIMonad rawIMonad public


text:
module CoinductiveCK where

open import Data.Product
open import Data.Sum
open import Data.Empty
open import Data.Nat
open import Data.Bool using (Bool; if_then_else_; true; false)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; subst)
open PropEq.≡-Reasoning
open import Relation.Nullary
open import Relation.Nullary.Negation using (¬∃⟶∀¬; Excluded-Middle)
open import Function using (_$_; _∘_)
open import Relation.Binary.Core using (IsEquivalence) renaming (Rel to RelL)
open import Level as L using () renaming (_⊔_ to _⊔L_)

-- to be classical, we need the law of excluded middle
-- the following defns. were adapted from:
-- http://stackoverflow.com/questions/36669072/law-of-excluded-middle-in-agda

postulate LEM : ∀ {ℓ} (A : Set ℓ) → Dec A

¬¬A⇒A : ∀ {ℓ} {A : Set ℓ} → ¬ (¬ A) → A
¬¬A⇒A {_} {A} ¬¬p with LEM A
... | yes p = p
... | no ¬p = ⊥-elim (¬¬p ¬p)

¬∀⟶∃¬ :  ∀ {ℓ ℓ'} {A : Set ℓ} {B : A → Set ℓ'} → ¬ (∀ a → B a) → ∃ λ a → ¬ (B a)
¬∀⟶∃¬ {A = A} {B} ¬∀ with LEM (∃ λ a → ¬ B a)
... | (yes p) = p
... | (no ¬p) = ⊥-elim $ ¬∀ (¬¬A⇒A ∘ ¬∃⟶∀¬ ¬p)

postulate State : Set

Event : ∀ {ℓ} → Set (L.suc ℓ)
Event {ℓ} = State → Set ℓ

_∧_ : ∀ {ℓ ℓ'} → Event {ℓ} → Event {ℓ'} → Event
e1 ∧ e2 = λ w → e1 w × e2 w

_∨_ : ∀ {ℓ ℓ'} → Event {ℓ} → Event {ℓ'} → Event
e1 ∨ e2 = λ w → e1 w ⊎ e2 w

_⟶_ : ∀ {ℓ ℓ'} → Event {ℓ} → Event {ℓ'} → Event
e1 ⟶ e2 = λ w → e1 w → e2 w

_⇒_ : ∀ {ℓ ℓ'} → Event {ℓ} → Event {ℓ'} → Set _
e1 ⇒ e2 = ∀ w → e1 w → e2 w

~_ : ∀ {ℓ} → Event {ℓ} → Event
~ e = λ w → e w → ⊥

All : ∀ {ℓ} → Event {ℓ} → Set _
All e = ∀ w → e w

⇒All⟶ : ∀ {ℓ ℓ'} (e1 : Event {ℓ}) (e2 : Event {ℓ'}) → e1 ⇒ e2 → All (e1 ⟶ e2)
⇒All⟶ e1 e2 e1⇒e2 w e1w = e1⇒e2 w e1w

mapE : ∀ {ℓ ℓ' ℓ''} {X : Set ℓ} → (Event {ℓ'} → Event {ℓ''}) → (X → Event) → X → Event {ℓ''}
mapE K E = λ n → K (E n)

_⊂_ : ∀ {ℓ ℓ' ℓ''} {X : Set ℓ} → (X → Event {ℓ'}) → Event {ℓ''} → Set (ℓ ⊔L ℓ' ⊔L ℓ'')
_⊂_ {X = X} E e = ∀ w → (∀ (x : X) → E x w) → e w

⇒Trans : ∀ {ℓ ℓ' ℓ''} {e1 : Event {ℓ}} {e2 : Event {ℓ'}} {e3 : Event {ℓ''}} → e1 ⇒ e2 → e2 ⇒ e3 → e1 ⇒ e3
⇒Trans e1⇒e2 e2⇒e3 w e1w = e2⇒e3 w (e1⇒e2 w e1w)

⊂Trans : ∀ {ℓ ℓ' ℓ'' ℓ'''} {X : Set ℓ} {E : X → Event {ℓ'}} {e1 : Event {ℓ''}} {e2 : Event {ℓ'''}} →
  E ⊂ e1 → e1 ⇒ e2 → E ⊂ e2
⊂Trans E⊂e1 e1⇒e2 w ∀xExw = e1⇒e2 w (E⊂e1 w ∀xExw)

-- Definition of preservation of semantic implication.
Sem⊂ : ∀ {ℓ ℓ' ℓ''} → (Event {ℓ'} → Event {ℓ''}) → Set (L.suc (ℓ ⊔L ℓ') ⊔L ℓ'')
Sem⊂ {ℓ} {ℓ'} {ℓ''} K = ∀ {X : Set ℓ} {E : X → Event {ℓ'}} {e : Event {ℓ'}} → _⊂_ {ℓ} {ℓ'} {ℓ'} E e → (mapE K E) ⊂ K e

-- Knowledge Operators
record KOp {ℓ ℓ'} (K : Event {ℓ} → Event {ℓ}) : Set (L.suc (ℓ ⊔L ℓ')) where
  field
    axiomN : ∀ {e} → All e → All (K e)
    axiomK : ∀ {e1 e2} → K (e1 ⟶ e2) ⇒ (K e1 ⟶ K e2)
    axiomT : ∀ {e} → K e ⇒ e
    axiom4 : ∀ {e} → K e ⇒ K (K e)
    axiom5 : ∀ {e} → (~ K e) ⇒ K (~ K e)
    -- Infinitary deduction
    axiomInf : Sem⊂ {ℓ'} K

-- axiomN follows from axiomInf, using the empty family
emptyFam : ∀ {ℓ} → ⊥ → Event {ℓ}
emptyFam ()

All_emptyFam : ∀ {ℓ ℓ'} (e : Event {ℓ}) → All e → (emptyFam {ℓ'}) ⊂ e
All_emptyFam e Alle w ∀xExw = Alle w

emptyFam_All : ∀ {ℓ ℓ'} (e : Event {ℓ}) → (emptyFam {ℓ'}) ⊂ e → All e
emptyFam_All e emptyFam⊂e w = emptyFam⊂e w (λ x → ⊥-elim x)

infN : ∀ {ℓ ℓ'} → (K : Event {ℓ} → Event {ℓ'}) → Sem⊂ K → ∀ e → All e → All (K e)
infN {ℓ} K Sem⊂K e Alle = emptyFam_All (K e) aux
  where
    aux : (emptyFam {ℓ}) ⊂ (K e)
    aux w _ = Sem⊂K (All_emptyFam e Alle) w (λ x → ⊥-elim x)

-- Similarly, axiomK follows from axiomInf using a family with two members:
-- A "modus ponens" family.
mpFam : ∀ {ℓ ℓ'} (e1 : Event {ℓ ⊔L ℓ'}) (e2 : Event {ℓ'}) → Bool → Event {ℓ ⊔L ℓ'}
mpFam e1 e2 = λ b → if b then (e1 ⟶ e2) else e1

infK : ∀ {ℓ} → (K : Event {ℓ} → Event {ℓ}) → Sem⊂ K →
  ∀ (e1 : Event {ℓ}) (e2 : Event {ℓ}) → K (e1 ⟶ e2) ⇒ (K e1 ⟶ K e2)
infK {ℓ} K Sem⊂K e1 e2 w Ke1⟶e2w Ke1w = Sem⊂K {E = mpFam {ℓ} e1 e2} aux₁ w aux₂
  where
    aux₁ : mpFam {ℓ} e1 e2 ⊂ e2
    aux₁ w ∀x⦃e1⟶e2,e1⦄xw = ∀x⦃e1⟶e2,e1⦄xw true (∀x⦃e1⟶e2,e1⦄xw false)

    aux₂ : (x : Bool) → mapE K (mpFam {ℓ} e1 e2) x w
    aux₂ true = Ke1⟶e2w
    aux₂ false = Ke1w

natK : ∀ {ℓ ℓ'} {X : Set ℓ'} {K : Event {ℓ} → Event {ℓ}} → KOp {ℓ} {ℓ'} K →
  ∀ {E : X → Event} {e} → E ⊂ e → (mapE K E) ⊂ (K e)
natK KOpK E⊂e = KOp.axiomInf KOpK E⊂e

K⇒ : ∀ {ℓ ℓ'} {K : Event {ℓ} → Event {ℓ}} → KOp {ℓ} {ℓ'} K →
  ∀ {e1 e2} → e1 ⇒ e2 → (K e1) ⇒ (K e2)
K⇒ KOpK {e1} {e2} e1⇒e2 w Ke1w = KOp.axiomK KOpK {e1} {e2} w (KOp.axiomN KOpK e1⇒e2 w) Ke1w

~e⇒K~Ke : ∀ {ℓ ℓ'} {K : Event {ℓ} → Event {ℓ}} → KOp {ℓ} {ℓ'} K →
  ∀ {e} → (~ e) ⇒ K (~ K e)
~e⇒K~Ke KOpK {e} w ~ew = KOp.axiom5 KOpK w (λ Kew → ~ew (KOp.axiomT KOpK {e} w Kew))

-- COINDUCTIVE DEFINITION OF COMMON KNOWLEDGE
postulate Agent : Set
postulate an_agent : Agent

postulate 𝕂 : ∀ {ℓ} → Agent → Event {ℓ} → Event {ℓ}
postulate 𝕂KOp : ∀ {ℓ ℓ'} a → KOp {ℓ} {ℓ'} (𝕂 a)

𝕂⇒ : ∀ {ℓ} {e1 : Event {ℓ}} {e2 : Event {ℓ}} {i : Agent} → e1 ⇒ e2 → 𝕂 i e1 ⇒ 𝕂 i e2
𝕂⇒ {ℓ} {e1} {e2} {i} e1⇒e2 w 𝕂ie1w =
  KOp.axiomK (𝕂KOp {ℓ} {ℓ} i) {e1} {e2} w (KOp.axiomN (𝕂KOp {ℓ} {ℓ} i) e1⇒e2 w) 𝕂ie1w

-- Everybody Knows
EK : ∀ {ℓ ℓ'} {K : Agent → Event {ℓ} → Event {ℓ'}} → Event → Event
EK {ℓ} {ℓ'} {K} e = λ w → ∀ {i : Agent} → K i e w

E𝕂 : ∀ {ℓ} → Event {ℓ} → Event {ℓ}
E𝕂 = EK {K = 𝕂}

-- Common Knowledge
-- Coinductive Definition

record cCK {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} (e : Event {ℓ}) (w : State) : Set ℓ where
  coinductive
  field
    intro : (EK {ℓ} {ℓ} {K} e ∧ cCK {ℓ} {K} (EK {ℓ} {ℓ} {K} e)) w

cC𝕂 : ∀ {ℓ} → Event {ℓ} → Event {ℓ}
cC𝕂 = cCK {K = 𝕂}

cCK⇒EK : ∀ {ℓ} {e : Event {ℓ}} {K : Agent → Event {ℓ} → Event {ℓ}} →
  cCK {K = K} e ⇒ EK {K = K} e
cCK⇒EK w cCKe = proj₁ (cCK.intro cCKe)

cCK⇒cCKEK : ∀ {ℓ} {e : Event {ℓ}} {K : Agent → Event {ℓ} → Event {ℓ}} →
  cCK {K = K} e ⇒ cCK {K = K} (EK {K = K} e)
cCK⇒cCKEK w cCKe = proj₂ (cCK.intro cCKe)

-- knowledge operator properties of E𝕂
E𝕂axiomInf : ∀ {ℓ ℓ'} → Sem⊂ {ℓ'} (E𝕂 {ℓ})
E𝕂axiomInf {X = X} {E} {e} E⊂e w ∀xEKExw {i} =
  KOp.axiomInf (𝕂KOp i) {X} {E} {e} E⊂e w (λ x → ∀xEKExw x)

E𝕂axiomN : ∀ {ℓ} {e : Event {ℓ}} →
  All e → All (E𝕂 e)
E𝕂axiomN {ℓ} Alle w {i} = KOp.axiomN (𝕂KOp {ℓ} {ℓ} i) Alle w

E𝕂axiomK : ∀ {ℓ} {e1 e2 : Event {ℓ}} →
  E𝕂 (e1 ⟶ e2) ⇒ (E𝕂 e1 ⟶ E𝕂 e2)
E𝕂axiomK {ℓ} {e1 = e1} {e2} w E𝕂e1⟶e2w E𝕂e1w {i} =
  KOp.axiomK (𝕂KOp {ℓ} {ℓ} i) {e1} w E𝕂e1⟶e2w E𝕂e1w

E𝕂axiomT : ∀ {ℓ} {e : Event {ℓ}} → E𝕂 e ⇒ e
E𝕂axiomT {ℓ} w E𝕂ew = KOp.axiomT (𝕂KOp {ℓ} {ℓ} an_agent) w E𝕂ew

E𝕂⇒ : ∀ {ℓ} {e1 e2 : Event {ℓ}} → e1 ⇒ e2 → E𝕂 e1 ⇒ E𝕂 e2
E𝕂⇒ e1⇒e2 w E𝕂e1w = 𝕂⇒ e1⇒e2 w E𝕂e1w

-- EK_axiom4 doesn't hold - if it did, (EK e) would imply (EK (EK e)),
-- and applying this ad infinitum would imply (cCK e)

E𝕂cC𝕂 : ∀ {ℓ} {e : Event {ℓ}} → e ⇒ E𝕂 e → e ⇒ cC𝕂 e
cCK.intro (E𝕂cC𝕂 {e} e⇒E𝕂e w ew) = e⇒E𝕂e w ew , E𝕂cC𝕂 (E𝕂⇒ e⇒E𝕂e) w (e⇒E𝕂e w ew)

~K⇒~EK : ∀ {ℓ} {e : Event {ℓ}} {K : Agent → Event {ℓ} → Event {ℓ}} {a} →
  (~ K a e) ⇒ (~ EK {K = K} e)
~K⇒~EK w ~Kae EKew = ~Kae EKew

𝕂~𝕂⇒𝕂~E𝕂 : ∀ {ℓ} {e : Event {ℓ}} {a} → 𝕂 a (~ 𝕂 a e) ⇒ 𝕂 a (~ E𝕂 e)
𝕂~𝕂⇒𝕂~E𝕂 = 𝕂⇒ (~K⇒~EK {K = 𝕂})

~e⇒E𝕂~E𝕂 : ∀ {ℓ} {e : Event {ℓ}} → (~ e) ⇒ E𝕂 (~ E𝕂 e)
~e⇒E𝕂~E𝕂 {ℓ} w ~ew {i} = 𝕂~𝕂⇒𝕂~E𝕂 w (~e⇒K~Ke (𝕂KOp {ℓ} {ℓ} i) w ~ew)

-- cCK equivalent of recursive EK

recEK : ∀ {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} → Event {ℓ} → ℕ → Event {ℓ}
recEK {K = K} e zero = EK {K = K} e
recEK {K = K} e (suc n) = EK {K = K} (recEK {K = K} e n)

recE𝕂 : ∀ {ℓ} → Event {ℓ} → ℕ → Event {ℓ}
recE𝕂 = recEK {K = 𝕂}

recEK-EK≡EK-recEK : ∀ {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} (e : Event {ℓ}) n →
  recEK {K = K} (EK {K = K} e) n ≡ EK {K = K} (recEK {K = K} e n)
recEK-EK≡EK-recEK _ zero = refl
recEK-EK≡EK-recEK {K = K} e (suc n) = cong (EK {K = K}) (recEK-EK≡EK-recEK {K = K} e n)

cCK⇒recEK : ∀ {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} (e : Event {ℓ}) n →
  cCK {K = K} e ⇒ recEK {K = K} e n
cCK⇒recEK e zero w cCKew {i} = proj₁ (cCK.intro cCKew)
cCK⇒recEK {K = K} e (suc n) =
  ⇒Trans {e2 = cCK {K = K} (EK {K = K} e)} cCK⇒cCKEK
    (⇒Trans {e2 = recEK {K = K} (EK {K = K} e) n} ih aux)
  where
    ih : cCK {K = K} (EK {K = K} e) ⇒ recEK {K = K} (EK {K = K} e) n
    ih = cCK⇒recEK (EK {K = K} e) n

    aux : recEK {K = K} (EK {K = K} e) n ⇒ recEK {K = K} e (suc n)
    aux rewrite recEK-EK≡EK-recEK {K = K} e n = λ w EKrecEKenw {i} → EKrecEKenw

recEK⊂cCK : ∀ {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} (e : Event {ℓ}) →
  (recEK {K = K} e) ⊂ (cCK {K = K} e)
cCK.intro (recEK⊂cCK {K = K} e w ∀xrecEKexw) =
  ∀xrecEKexw zero , ih w (λ n → subst (λ P → P) (aux n) (∀xrecEKexw (suc n)))
  where
    ih : (recEK {K = K} (EK {K = K} e)) ⊂ (cCK {K = K} (EK {K = K} e))
    ih = recEK⊂cCK (EK {K = K} e)

    aux : ∀ n → (EK {K = K} (recEK {K = K} e n)) w ≡ (recEK {K = K} (EK {K = K} e) n) w
    aux n = cong (λ P → P w) {EK {K = K} (recEK {K = K} e n)} {recEK {K = K} (EK {K = K} e) n}
      (sym (recEK-EK≡EK-recEK e n))

-- knowledge operator properties of cCK

E𝕂cC𝕂⇒cC𝕂E𝕂 : ∀ {ℓ} (e : Event {ℓ}) → E𝕂 (cC𝕂 e) ⇒ cC𝕂 (E𝕂 e)
E𝕂cC𝕂⇒cC𝕂E𝕂 e w E𝕂cC𝕂ew = cCK⇒cCKEK w (E𝕂axiomT w E𝕂cC𝕂ew)

cCKEK⇒EKcCK : ∀ {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} {KOpK : ∀ a -> KOp {ℓ} {L.zero} (K a)} (e : Event {ℓ}) →
  cCK {K = K} (EK {K = K} e) ⇒ EK {K = K} (cCK {K = K} e)
cCKEK⇒EKcCK {K = K} {KOpK} e w cCKEKew {i} =
  natK {X = ℕ} (KOpK i) (recEK⊂cCK e) w
    (λ n → aux n w (subst (λ P → P w)
      {recEK {K = K} (EK {K = K} e) n}
      {EK {K = K} (recEK {K = K} e n)}
      (recEK-EK≡EK-recEK e n)
      (cCK⇒recEK (EK {K = K} e) n w cCKEKew)))
  where
    aux : ∀ n → EK {K = K} (recEK {K = K} e n) ⇒ mapE (K i) (recEK {K = K} e) n
    aux n w EKrecEKen = EKrecEKen

cCK⇒EKcCK : ∀ {ℓ} {K : Agent → Event {ℓ} → Event {ℓ}} (KOpK : ∀ a -> KOp {ℓ} {L.zero} (K a)) (e : Event {ℓ}) →
  cCK {K = K} e ⇒ EK {K = K} (cCK {K = K} e)
cCK⇒EKcCK {K = K} KOpK e = ⇒Trans {e2 = cCK {K = K} (EK {K = K} e)} cCK⇒cCKEK (cCKEK⇒EKcCK {K = K} {KOpK} e)

E𝕂recE𝕂 : ∀ {ℓ} (e1 e2 : Event {ℓ}) n → e1 ⇒ E𝕂 e2 → recE𝕂 e1 n ⇒ recE𝕂 e2 (suc n)
E𝕂recE𝕂 e1 e2 zero    e1⇒E𝕂e2 w recE𝕂e1nw {i} = E𝕂⇒ {e1 = e1} e1⇒E𝕂e2 w recE𝕂e1nw
E𝕂recE𝕂 e1 e2 (suc n) e1⇒E𝕂e2 w recE𝕂e1nw {i} = E𝕂⇒ {e1 = recEK e1 n} ih w recE𝕂e1nw
  where
    ih : recE𝕂 e1 n ⇒ recE𝕂 e2 (suc n)
    ih = E𝕂recE𝕂 e1 e2 n e1⇒E𝕂e2

cC𝕂⇒recE𝕂cC𝕂 : ∀ {ℓ} (e : Event {ℓ}) n → cC𝕂 e ⇒ recE𝕂 (cC𝕂 e) n
cC𝕂⇒recE𝕂cC𝕂 e zero = cCK⇒EKcCK 𝕂KOp e
cC𝕂⇒recE𝕂cC𝕂 e (suc n) = ⇒Trans {e2 = E𝕂 (cC𝕂 e)} (cCK⇒EKcCK 𝕂KOp e) ih
  where
    ih : E𝕂 (cC𝕂 e) ⇒ E𝕂 (recE𝕂 (cC𝕂 e) n)
    ih = E𝕂⇒ (cC𝕂⇒recE𝕂cC𝕂 e n)

cC𝕂axiomInf : ∀ {ℓ ℓ'} → Sem⊂ {ℓ} {ℓ'} {ℓ'} cC𝕂
cCK.intro (cC𝕂axiomInf {X = X} {E} {e} E⊂e w mapEcC𝕂E) =
  E𝕂axiomInf {X = X} {E} E⊂e w (λ x → cCK⇒EK w (mapEcC𝕂E x)) ,
  cC𝕂axiomInf {E = λ x → E𝕂 (E x)} (E𝕂axiomInf {X = X} {E} E⊂e) w (λ x → cCK⇒cCKEK w (mapEcC𝕂E x))

cC𝕂axiom4 : ∀ {ℓ} {e : Event {ℓ}} → cC𝕂 e ⇒ cC𝕂 (cC𝕂 e)
cC𝕂axiom4 {e = e} w cC𝕂e = recEK⊂cCK (cC𝕂 e) w ((λ n → cC𝕂⇒recE𝕂cC𝕂 e n w cC𝕂e))

cC𝕂axiomN : ∀ {ℓ} {e : Event {ℓ}} → All e → All (cC𝕂 e)
cC𝕂axiomN {e = e} = infN cC𝕂 cC𝕂axiomInf e

cC𝕂axiomT : ∀ {ℓ} {e : Event {ℓ}} → cC𝕂 e ⇒ e
cC𝕂axiomT w cC𝕂ew = E𝕂axiomT w (proj₁ (cCK.intro cC𝕂ew))

cC𝕂axiomK : ∀ {ℓ} {e1 e2 : Event {ℓ}} → cC𝕂 (e1 ⟶ e2) ⇒ (cC𝕂 e1 ⟶ cC𝕂 e2)
cC𝕂axiomK {_} {e1} {e2} = infK cC𝕂 cC𝕂axiomInf e1 e2

~cC𝕂⇒E𝕂~cC𝕂 : ∀ {ℓ} {e : Event {ℓ}} → (~ cC𝕂 e) ⇒ E𝕂 (~ cC𝕂 e)
~cC𝕂⇒E𝕂~cC𝕂 {e = e} w ~cC𝕂ew = cut (λ ∀nrecE𝕂enw → ~cC𝕂ew (recEK⊂cCK e w ∀nrecE𝕂enw))
  where
    cut : (¬(∀ n → recE𝕂 e n w)) → E𝕂 (~ cC𝕂 e) w
    cut ¬∀nrecE𝕂enw = E𝕂⇒ {e1 = ~ recE𝕂 e (suc n)}
      (λ w ~recE𝕂eSn cC𝕂ew → ~recE𝕂eSn (cCK⇒recEK e (suc n) w cC𝕂ew))
      w
      (~e⇒E𝕂~E𝕂 w ¬recE𝕂enw)
      where
        neg : ∃ (λ n → ¬ (recE𝕂 e n w))
        neg = ¬∀⟶∃¬ ¬∀nrecE𝕂enw

        n = proj₁ neg
        ¬recE𝕂enw = proj₂ neg

cC𝕂axiom5 : ∀ {ℓ} {e : Event {ℓ}} → (~ cC𝕂 e) ⇒ cC𝕂 (~ cC𝕂 e)
cC𝕂axiom5 = E𝕂cC𝕂 ~cC𝕂⇒E𝕂~cC𝕂

cC𝕂KOp : ∀ {ℓ ℓ'} → KOp {ℓ} {ℓ'} cC𝕂
cC𝕂KOp = record {
    axiomN = cC𝕂axiomN
  ; axiomK = cC𝕂axiomK
  ; axiomT = cC𝕂axiomT
  ; axiom4 = cC𝕂axiom4
  ; axiom5 = cC𝕂axiom5
  ; axiomInf = cC𝕂axiomInf
  }

-- Equivalence Relations

RelToK : ∀ {ℓ ℓ'} → RelL State ℓ → Event {ℓ'} → Event {ℓ ⊔L ℓ'}
RelToK R e w = ∀ v → R w v → e v

KtoRel : ∀ {ℓ} → (Event → Event {ℓ}) → RelL State (L.suc ℓ)
KtoRel K w v = ∀ e → K e w → K e v

-- Proof that RelToK on an equivalence relation yields a K satisfying S5 *)

axiomN' : ∀ {ℓ ℓ'} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ {e : Event {ℓ'}} → All e → All ((RelToK R) e)
axiomN' _ _ Alle _ v _ = Alle v

axiomK' : ∀ {ℓ ℓ' ℓ''} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ {e1 : Event {ℓ'}} {e2 : Event {ℓ''}} → (RelToK R) (e1 ⟶ e2) ⇒ ((RelToK R) e1 ⟶ (RelToK R) e2)
axiomK' R _ {e1} {e2} w Ke1⟶e2 Ke1w = λ v Rwv → Ke1⟶e2 v Rwv (Ke1w v Rwv)

axiomT' : ∀ {ℓ ℓ'} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ {e : Event {ℓ'}} → (RelToK R) e ⇒ e
axiomT' R IsEqR {e} w Kew = Kew w (IsEquivalence.refl IsEqR)

axiom4' : ∀ {ℓ ℓ'} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ {e : Event {ℓ'}} → (RelToK R) e ⇒ (RelToK R) ((RelToK R) e)
axiom4' R IsEqR {e} w Kew v Rwv u Rvu = Kew u (IsEquivalence.trans IsEqR Rwv Rvu)

axiom5' : ∀ {ℓ ℓ'} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ {e : Event {ℓ'}} → (~ (RelToK R) e) ⇒ (RelToK R) (~ ((RelToK R) e))
axiom5' R IsEqR {e} w ~Kew v Rwv Kev =
  ~Kew (λ u Rwu → Kev u (IsEquivalence.trans IsEqR (IsEquivalence.sym IsEqR Rwv) Rwu))

axiomInf' : ∀ {ℓ ℓ'} → (R : RelL State ℓ) → IsEquivalence R → Sem⊂ {ℓ'} {ℓ} (RelToK R)
axiomInf' R IsEqR E⊂e w ∀x v Rwv = E⊂e v (λ x → ∀x x v Rwv)

KOpRelToK : ∀ {ℓ ℓ'} → (R : RelL State ℓ) → IsEquivalence R → KOp {ℓ} {ℓ'} (RelToK R)
KOpRelToK R IsEqR = record {
    axiomN = axiomN' R IsEqR
  ; axiomK = axiomK' R IsEqR
  ; axiomT = axiomT' R IsEqR
  ; axiom4 = axiom4' R IsEqR
  ; axiom5 = axiom5' R IsEqR
  ; axiomInf = axiomInf' R IsEqR
  }

-- Proof that K_to_Rel on a K satisfying S5 yields an equivalence relation

eqRefl' : ∀ {ℓ ℓ'} → (K : Event {ℓ} → Event) → KOp {ℓ} {ℓ'} K →
  ∀ {w : State} → (KtoRel K) w w
eqRefl' K KopK = λ e Kew → Kew

eqSym' : ∀ {ℓ ℓ'} → (K : Event {ℓ} → Event) → KOp {ℓ} {ℓ'} K →
  ∀ {w v : State} → (KtoRel K) w v → (KtoRel K) v w
eqSym' K KOpK {w} {v} Rwv e Kev = ¬¬A⇒A (λ ¬Kew →
  KOp.axiomT KOpK {~ K e} v (Rwv (~ K e) (KOp.axiom5 KOpK {e} w ¬Kew)) Kev)

eqTrans' : ∀ {ℓ ℓ'} → (K : Event {ℓ} → Event) → KOp {ℓ} {ℓ'} K →
  ∀ {w v u : State} →  (KtoRel K) w v → (KtoRel K) v u → (KtoRel K) w u
eqTrans' K _ {w} {v} {u} Rwv Rvu e Kew = Rvu e (Rwv e Kew)

EqRelKtoRel : ∀ {ℓ ℓ'} → (K : Event {ℓ} → Event) → KOp {ℓ} {ℓ'} K → IsEquivalence (KtoRel K)
EqRelKtoRel K KOpK = record { refl = eqRefl' K KOpK ; sym = eqSym' K KOpK ; trans = eqTrans' K KOpK }

-- The two transformations are an isomorphism

EqRelKIso1 : ∀ {ℓ ℓ'} → {K : Event → Event {ℓ}} → KOp {ℓ} {ℓ'} K →
    ∀ (e : Event {ℓ}) → (K e) ⇒ (RelToK (KtoRel K) e)
EqRelKIso1 {K = K} KOpK e w Kew v Rwv = KOp.axiomT KOpK v (Rwv e Kew)

data Indexed {ℓ ℓ'} (K : Event {ℓ} → Event {ℓ'}) (w : State) : Set (L.suc (ℓ ⊔L ℓ')) where
  index : ∀ (e : Event) → K e w → Indexed K w

KFam : ∀ {ℓ} {K : Event {ℓ} → Event {ℓ}} {w : State} → Indexed K w → Event {ℓ}
KFam {K = K} (index e Kew) = K e

Rew→KFam⊂e : ∀ {ℓ} → {K : Event → Event {ℓ}} →
  ∀ (e : Event {ℓ}) w → RelToK (KtoRel K) e w → (KFam {K = K} {w}) ⊂ e
Rew→KFam⊂e {ℓ} {K} e w R2K-K2Rew v ∀xKFamxv =
  R2K-K2Rew v (λ e' Ke'w → ∀xKFamxv (index e' Ke'w))

EqRelKIso2 : ∀ {ℓ} → {K : Event → Event {ℓ}} → KOp {ℓ} {L.suc ℓ} K →
    ∀ (e : Event {ℓ}) → (RelToK (KtoRel K) e) ⇒ (K e)
EqRelKIso2 {ℓ} {K} KOpK e w R2K-K2Rew = KOp.axiomInf KOpK aux w aux₁
  where
    aux : _⊂_ {L.suc ℓ} {ℓ} {ℓ} (KFam {ℓ} {K} {w}) e
    aux = Rew→KFam⊂e e w R2K-K2Rew

    aux₁ : (x : Indexed K w) → K (KFam x) w
    aux₁ (index e Kew) = KOp.axiom4 KOpK w Kew

KeqRelIso1 : ∀ {ℓ} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ w v → R w v → KtoRel {ℓ} (RelToK R) w v
KeqRelIso1 R IsEqR w v Rwv e R2Kew u Rvu = R2Kew u (IsEquivalence.trans IsEqR Rwv Rvu)

KeqRelIso2 : ∀ {ℓ} → (R : RelL State ℓ) → IsEquivalence R →
  ∀ w v → KtoRel {ℓ} (RelToK R) w v → R w v
KeqRelIso2 R IsEqR w v K2R-R2Kwv = K2R-R2Kwv (R w) (λ v₁ z → z) v (IsEquivalence.refl IsEqR)

-- RELATIONAL DEFINITION OF COMMON KNOWLEDGE

postulate 𝕂R : ∀ {ℓ} → Agent → RelL State ℓ
postulate IsEq𝕂R : ∀ {ℓ} a → IsEquivalence (𝕂R {ℓ} a)

𝕂ᵣ : ∀ {ℓ} (i : Agent) → Event {ℓ} → Event {ℓ}
𝕂ᵣ {ℓ} i = RelToK (𝕂R {ℓ} i)

𝕂ᵣKOp : ∀ {ℓ ℓ'} i -> KOp {ℓ} {ℓ'} (𝕂ᵣ i)
𝕂ᵣKOp i = KOpRelToK (𝕂R i) (IsEq𝕂R i)

𝕂ᵣe→e : ∀ {ℓ} i (e : Event {ℓ}) w → 𝕂ᵣ i e w → e w
𝕂ᵣe→e i e w 𝕂ᵣiew = 𝕂ᵣiew w (IsEquivalence.refl (IsEq𝕂R i))

𝕂ᵣe→𝕂ᵣ𝕂ᵣe : ∀ {ℓ} i (e : Event {ℓ}) w → 𝕂ᵣ i e w → 𝕂ᵣ i (𝕂ᵣ i e) w
𝕂ᵣe→𝕂ᵣ𝕂ᵣe i e w 𝕂ᵣiew v 𝕂Riwv u 𝕂Rivu =
  𝕂ᵣiew u (IsEquivalence.trans (IsEq𝕂R i) 𝕂Riwv 𝕂Rivu)

E𝕂ᵣ : ∀ {ℓ} → Event {ℓ} → Event {ℓ}
E𝕂ᵣ = EK {K = 𝕂ᵣ}

cC𝕂ᵣ : ∀ {ℓ} → Event {ℓ} → Event {ℓ}
cC𝕂ᵣ = cCK {K = 𝕂ᵣ}

cC𝕂ᵣ→E𝕂ᵣcC𝕂ᵣ : ∀ {ℓ} {e : Event {ℓ}} {w : State} → cC𝕂ᵣ e w -> E𝕂ᵣ (cC𝕂ᵣ e) w
cC𝕂ᵣ→E𝕂ᵣcC𝕂ᵣ {ℓ} {e} {w} = cCK⇒EKcCK {K = 𝕂ᵣ} 𝕂ᵣKOp e w

data C𝕂R {ℓ} : RelL State ℓ where
  base : ∀ i w v -> 𝕂R {ℓ} i w v -> C𝕂R w v
  trans : ∀ {w v u} -> C𝕂R {ℓ} w v -> C𝕂R {ℓ} v u -> C𝕂R {ℓ} w u

C𝕂Rrefl : ∀ {ℓ} → Relation.Binary.Core.Reflexive (C𝕂R {ℓ})
C𝕂Rrefl {x = w} = base an_agent w w (IsEquivalence.refl (IsEq𝕂R an_agent))

C𝕂Rsym : ∀ {ℓ} → Relation.Binary.Core.Symmetric (C𝕂R {ℓ})
C𝕂Rsym (base i w v 𝕂Riwv) = base i v w (IsEquivalence.sym (IsEq𝕂R i) 𝕂Riwv)
C𝕂Rsym (trans C𝕂Rwv C𝕂Rvu) = trans (C𝕂Rsym C𝕂Rvu) (C𝕂Rsym C𝕂Rwv)

EqRelC𝕂R : ∀ {ℓ} → IsEquivalence (C𝕂R {ℓ})
EqRelC𝕂R = record { refl = C𝕂Rrefl ; sym = C𝕂Rsym ; trans = trans }

C𝕂ᵣ : ∀ {ℓ} → Event {ℓ} → Event {ℓ}
C𝕂ᵣ {ℓ} = RelToK (C𝕂R {ℓ})

C𝕂ᵣ→E𝕂ᵣ : ∀ {ℓ} {e : Event {ℓ}} {w : State} → C𝕂ᵣ e w -> E𝕂ᵣ e w
C𝕂ᵣ→E𝕂ᵣ {_} {e} {w} C𝕂ᵣew {i} v 𝕂Riwv = C𝕂ᵣew v (base i w v 𝕂Riwv)

C𝕂ᵣ→E𝕂ᵣC𝕂ᵣ : ∀ {ℓ} {e : Event {ℓ}} {w : State} → C𝕂ᵣ e w -> E𝕂ᵣ (C𝕂ᵣ e) w
C𝕂ᵣ→E𝕂ᵣC𝕂ᵣ {_} {e} {w} C𝕂ᵣew {i} v 𝕂Riwv u C𝕂Rvu =
  C𝕂ᵣew u (trans (base i w v 𝕂Riwv) C𝕂Rvu)

C𝕂ᵣ→C𝕂ᵣE𝕂ᵣ : ∀ {ℓ} {e : Event {ℓ}} {w : State} → C𝕂ᵣ e w -> C𝕂ᵣ (E𝕂ᵣ e) w
C𝕂ᵣ→C𝕂ᵣE𝕂ᵣ {_} {e} {w} C𝕂ᵣew v C𝕂Rwv {i} u 𝕂Rivu =
  C𝕂ᵣew u (trans C𝕂Rwv (base i v u 𝕂Rivu))

C𝕂ᵣ→cC𝕂ᵣ : ∀ {ℓ} {e : Event {ℓ}} {w : State} → C𝕂ᵣ e w -> cC𝕂ᵣ e w
cCK.intro (C𝕂ᵣ→cC𝕂ᵣ {ℓ} {e} {w} C𝕂ᵣew) = C𝕂ᵣ→E𝕂ᵣ C𝕂ᵣew , C𝕂ᵣ→cC𝕂ᵣ (C𝕂ᵣ→C𝕂ᵣE𝕂ᵣ C𝕂ᵣew)

C𝕂transport : ∀ {ℓ} {e : Event {ℓ}} {w v : State} → cC𝕂ᵣ e w -> C𝕂R {ℓ} w v -> cC𝕂ᵣ e v
C𝕂transport {_} {e} cC𝕂ᵣew (base i w v 𝕂Riwv) = record { intro =
    proj₁ (cCK.intro (proj₂ (cCK.intro cC𝕂ᵣew))) v 𝕂Riwv ,
    aux v 𝕂Riwv
  }
  where
    aux : E𝕂ᵣ (cC𝕂ᵣ (E𝕂ᵣ e)) w
    aux = cC𝕂ᵣ→E𝕂ᵣcC𝕂ᵣ (record { intro = cCK.intro (proj₂ (cCK.intro cC𝕂ᵣew)) })
C𝕂transport cC𝕂ᵣew (trans C𝕂Rwv C𝕂Rvu) =
  C𝕂transport (C𝕂transport cC𝕂ᵣew C𝕂Rwv) C𝕂Rvu

cC𝕂ᵣ→C𝕂ᵣ : ∀ {ℓ} {e : Event {ℓ}} {w : State} → cC𝕂ᵣ e w -> C𝕂ᵣ e w
cC𝕂ᵣ→C𝕂ᵣ {ℓ} {e} cC𝕂ᵣew v (base i w .v x) = proj₁ (cCK.intro cC𝕂ᵣew) v x
cC𝕂ᵣ→C𝕂ᵣ {ℓ} {e} {w} cC𝕂ᵣew v (trans {v = v'} C𝕂Rwv' C𝕂Rv'v) =
  cC𝕂ᵣ→C𝕂ᵣ (C𝕂transport cC𝕂ᵣew C𝕂Rwv') v C𝕂Rv'v

max_stars_repo_name: goodlyrottenapple/coinductiveCK

max_issues_repo_name: goodlyrottenapple/coinductiveCK

max_forks_repo_name: goodlyrottenapple/coinductiveCK


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.HITs.Pushout.Base
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

_⋁_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ')
_⋁_ (A , ptA) (B , ptB) = Pushout {A = Unit} {B = A} {C = B} (λ _ → ptA) (λ _ → ptB)

-- Pointed versions
_⋁∙ₗ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋁∙ₗ B = (A ⋁ B) , (inl (snd A))

_⋁∙ᵣ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋁∙ᵣ B = (A ⋁ B) , (inr (snd B))

-- Wedge sums of functions
_∨→_ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
      → (f : A →∙ C) (g : B →∙ C)
      → A ⋁ B → fst C
(f ∨→ g) (inl x) = fst f x
(f ∨→ g) (inr x) = fst g x
(f ∨→ g) (push a i₁) = (snd f ∙ sym (snd g)) i₁

-- Pointed version
∨→∙ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
   → (f : A →∙ C) (g : B →∙ C) → ((A ⋁∙ₗ B) →∙ C)
fst (∨→∙ {A = A} f g) = f ∨→ g
snd (∨→∙ {A = A} f g) = snd f

-- Wedge sum of Units is contractible
isContr-Unit⋁Unit : isContr ((Unit , tt) ⋁ (Unit , tt))
fst isContr-Unit⋁Unit = inl tt
snd isContr-Unit⋁Unit (inl tt) = refl
snd isContr-Unit⋁Unit (inr tt) = push tt
snd isContr-Unit⋁Unit (push tt i) j = push tt (i ∧ j)

⋁↪ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
      → A ⋁ B → typ A × typ B
⋁↪ {B = B} (inl x) = x , pt B
⋁↪ {A = A} (inr x) = pt A , x
⋁↪ {A = A} {B = B} (push a i) = pt A , pt B


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.Int where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Int
  renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

open GroupStr

ℤGroup : Group₀
fst ℤGroup = ℤ
1g (snd ℤGroup) = 0
_·_ (snd ℤGroup) = _+ℤ_
inv (snd ℤGroup) = -ℤ_
isGroup (snd ℤGroup) = isGroupℤ
  where
  abstract
    isGroupℤ : IsGroup (pos 0) (_+ℤ_) (-ℤ_)
    isGroupℤ = makeIsGroup isSetℤ
                           +Assoc (λ _ → refl) (+Comm 0)
                           -Cancel -Cancel'

ℤHom : (n : ℤ) → GroupHom ℤGroup ℤGroup
fst (ℤHom n) x = n ·ℤ x
snd (ℤHom n) =
  makeIsGroupHom λ x y → ·DistR+ n x y

negEquivℤ : GroupEquiv ℤGroup ℤGroup
fst negEquivℤ =
  isoToEquiv
    (iso (GroupStr.inv (snd ℤGroup))
         (GroupStr.inv (snd ℤGroup))
         (GroupTheory.invInv ℤGroup)
         (GroupTheory.invInv ℤGroup))
snd negEquivℤ =
  makeIsGroupHom -Dist+

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Homogeneous`.

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

module Relation.Binary.Indexed.Homogeneous.Core where

open import Level using (Level; _⊔_)
open import Data.Product using (_×_)
open import Relation.Binary as B using (REL; Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.Indexed.Heterogeneous as I
open import Relation.Unary.Indexed using (IPred)

private
  variable
    a b c ℓ : Level
    I : Set c

------------------------------------------------------------------------
-- Homegeneously indexed binary relations

-- Heterogeneous types

IREL : (I → Set a) → (I → Set b) → (ℓ : Level) → Set _
IREL A B ℓ = ∀ {i} → REL (A i) (B i) ℓ

-- Homogeneous types

IRel : (I → Set a) → (ℓ : Level) → Set _
IRel A = IREL A A

------------------------------------------------------------------------
-- Lifting to non-indexed binary relations

-- Ideally this should be in: `Construct.Lift` but we want this relation
-- to be exported by the various structures & bundles.

Lift : (A : I → Set a) → IRel A ℓ → Rel (∀ i → A i) _
Lift _ _∼_ x y = ∀ i → x i ∼ y i

------------------------------------------------------------------------
-- Conversion between homogeneous and heterogeneously indexed relations

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

  OverPath : ∀ {ℓ} → IREL A B ℓ → ∀ {i j} → i ≡ j → REL (A i) (B j) ℓ
  OverPath _∼_ refl = _∼_

  toHetIndexed : ∀ {ℓ} → IREL A B ℓ → I.IREL A B (i ⊔ ℓ)
  toHetIndexed _∼_ {i} {j} x y = (p : i ≡ j) → OverPath _∼_ p x y

  fromHetIndexed : ∀ {ℓ} → I.IREL A B ℓ → IREL A B ℓ
  fromHetIndexed _∼_ = _∼_


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Agda.Builtin.Nat
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Fin

open import Relation.Binary

module SingleSorted.AlgebraicTheory where

  open import SingleSorted.Context public

  Arity : Set
  Arity = Context

  arg : Arity → Set
  arg = var

  -- an algebraic signature
  record Signature : Set₁ where
    field
      oper : Set -- operations
      oper-arity : oper → Arity -- the arity of an operation

    -- terms over a signature in a context of a given sort
    data Term (Γ : Context) : Set where
      tm-var : var Γ → Term Γ
      tm-oper : ∀ (f : oper) → (arg (oper-arity f) → Term Γ) → Term Γ

    -- Substitutions (definitions - some useful properties are in another file)
    _⇒s_ : ∀ (Γ Δ : Context) → Set
    Γ ⇒s Δ = var Δ → Term Γ

    infix  4 _⇒s_

    -- identity substitution
    id-s : ∀ {Γ : Context} → Γ ⇒s Γ
    id-s = tm-var

    -- the action of a substitution on a term (contravariant)
    _[_]s : ∀ {Γ Δ : Context} → Term Δ → Γ ⇒s Δ → Term Γ
    (tm-var x) [ σ ]s = σ x
    (tm-oper f x) [ σ ]s = tm-oper f (λ i → x i [ σ ]s)

    infixr 6 _[_]s

    -- composition of substitutions
    _∘s_ : ∀ {Γ Δ Θ : Context} → Δ ⇒s Θ → Γ ⇒s Δ → Γ ⇒s Θ
    (σ ∘s ρ) x = σ x [ ρ ]s

    infixl 7 _∘s_

    -- Axioms are equations in context
    record Equation  : Set where
      field
        eq-ctx : Context
        eq-lhs : Term eq-ctx
        eq-rhs : Term eq-ctx

  -- Theory
  -- an equational theory is a family of equations over a given sort
  record Theory ℓ (Σ : Signature) : Set (lsuc ℓ) where
    open Signature Σ public

    field
      ax : Set ℓ -- the axiom names
      ax-eq : ax → Equation -- the axioms

    ax-ctx : ax → Context
    ax-ctx ε = Equation.eq-ctx (ax-eq ε)

    ax-lhs : ∀ (ε : ax) → Term (ax-ctx ε)
    ax-lhs ε = Equation.eq-lhs (ax-eq ε)

    ax-rhs : ∀ (ε : ax) → Term (ax-ctx ε)
    ax-rhs ε = Equation.eq-rhs (ax-eq ε)

    infix 4 _⊢_≈_

    -- equality of terms
    data _⊢_≈_ : (Γ : Context) → Term Γ → Term Γ → Set (lsuc ℓ) where
      -- general rules
      eq-refl : ∀ {Γ} {t : Term Γ} → Γ ⊢ t ≈ t
      eq-symm : ∀ {Γ} {s t : Term Γ} → Γ ⊢ s ≈ t → Γ ⊢ t ≈ s
      eq-tran : ∀ {Γ} {s t u : Term Γ} → Γ ⊢ s ≈ t → Γ ⊢ t ≈ u → Γ ⊢ s ≈ u
      -- congruence rule
      eq-congr : ∀ {Γ} {f : oper} {xs ys : arg (oper-arity f) → Term Γ} →
                 (∀ i → Γ ⊢ xs i ≈ ys i) → Γ ⊢ tm-oper f xs ≈ tm-oper f ys
      -- equational axiom
      eq-axiom : ∀ (ε : ax) {Γ : Context} (σ : Γ ⇒s (ax-ctx ε)) →
                 Γ ⊢ ax-lhs ε [ σ ]s ≈ ax-rhs ε [ σ ]s

    ≡-⊢-≈ : {Γ : Context} {s t : Term Γ} → s ≡ t → Γ ⊢ s ≈ t
    ≡-⊢-≈ refl = eq-refl

    -- the action of the identity substitution is the identity
    id-action : ∀ {Γ : Context} {a : Term Γ} → (Γ ⊢ a ≈ (a [ id-s ]s))
    id-action {a = tm-var a} = eq-refl
    id-action {a = tm-oper f x} = eq-congr (λ i → id-action {a = x i})

    eq-axiom-id : ∀ (ε : ax) → ax-ctx ε ⊢ ax-lhs ε ≈ ax-rhs ε
    eq-axiom-id ε = eq-tran id-action (eq-tran (eq-axiom ε id-s) (eq-symm id-action))

    eq-setoid : ∀ (Γ : Context) → Setoid lzero (lsuc ℓ)
    eq-setoid Γ =
      record
        { Carrier = Term Γ
        ;  _≈_ = λ s t → (Γ ⊢ s ≈ t)
        ; isEquivalence =
            record
              { refl = eq-refl
              ; sym = eq-symm
              ; trans = eq-tran
           }
        }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module +-swap where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; _+_)

open import Induction′ using (+-assoc; +-comm)

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
  begin
    m + (n + p)
  ≡⟨ sym (+-assoc m n p) ⟩
    (m + n) + p
  ≡⟨ cong (_+ p) (+-comm m n) ⟩
    (n + m) + p
  ≡⟨ +-assoc n m p ⟩
    n + (m + p)
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------------
-- Testing nested axioms
------------------------------------------------------------------------------

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

{-

Processing this file should be generate a TPTP file with the following
axioms

fof(..., axiom, ( a = b )).
fof(..., axiom, ( b = c )).
fof(..., axiom, ( c = d )).
-}

module NestedAxioms.C where

open import NestedAxioms.A
open import NestedAxioms.B

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

postulate
  d : D
  c≡d : c ≡ d
{-# ATP axiom c≡d #-}

postulate foo : d ≡ a
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

module Categories.Category.Instance.Cartesians where

open import Level

open import Categories.Category
open import Categories.Category.Helper
open import Categories.Category.Cartesian.Structure
open import Categories.Functor.Cartesian
open import Categories.Functor.Cartesian.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism

module _ o ℓ e where

  Cartesians : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
  Cartesians = categoryHelper record
    { Obj       = CartesianCategory o ℓ e
    ; _⇒_       = CartesianF
    ; _≈_       = λ F G → CF.F F ≃ CF.F G
    ; id        = idF-CartesianF _
    ; _∘_       = ∘-CartesianF
    ; assoc     = λ {_ _ _ _ F G H} → associator (CF.F F) (CF.F G) (CF.F H)
    ; identityˡ = unitorˡ
    ; identityʳ = unitorʳ
    ; equiv     = record
      { refl  = ≃.refl
      ; sym   = ≃.sym
      ; trans = ≃.trans
      }
    ; ∘-resp-≈  = _ⓘₕ_
    }
    where module CF = CartesianF

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

module Data.Nat.DivMod where

open import Data.Nat.Base
open import Agda.Builtin.Nat as Nat
open import Data.Bool

nonZero : ℕ → Bool
nonZero (suc _) = true
nonZero zero    = false

infixl 8 _÷_
_÷_ : (n m : ℕ) → { m≢0 : T (nonZero m) } → ℕ
_÷_ n (suc m) = Nat.div-helper 0 m n m

rem : (n m : ℕ) → { m≢0 : T (nonZero m) } → ℕ
rem n (suc m) = Nat.mod-helper 0 m n m

even : ℕ → Bool
even n = rem n 2 Nat.== 0

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Almost commutative rings
------------------------------------------------------------------------

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

module Tactic.RingSolver.Core.AlmostCommutativeRing where

open import Level
open import Relation.Binary
open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Structures using (IsCommutativeSemiring)
open import Algebra.Definitions
open import Algebra.Bundles using (RawRing; CommutativeRing; CommutativeSemiring)
import Algebra.Morphism as Morphism
open import Function
open import Level
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)

record IsAlmostCommutativeRing
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
         (_+_ _*_ : A → A → A) (-_ : A → A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
    -‿cong                : -_ Preserves _≈_ ⟶ _≈_
    -‿*-distribˡ          : ∀ x y → ((- x) * y)     ≈ (- (x * y))
    -‿+-comm              : ∀ x y → ((- x) + (- y)) ≈ (- (x + y))

  open IsCommutativeSemiring isCommutativeSemiring public

import Algebra.Operations.Ring as Exp

record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  infixr 8 _^_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ
    _+_                     : Op₂ Carrier
    _*_                     : Op₂ Carrier
    -_                      : Op₁ Carrier
    0#                      : Carrier
    0≟_                     : (x : Carrier) → Maybe (0# ≈ x)
    1#                      : Carrier
    isAlmostCommutativeRing :
      IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsAlmostCommutativeRing isAlmostCommutativeRing hiding (refl) public
  open import Data.Nat.Base as ℕ using (ℕ)

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring = record
    { isCommutativeSemiring = isCommutativeSemiring
    }

  open CommutativeSemiring commutativeSemiring public
    using ( +-semigroup; +-monoid; +-commutativeMonoid
          ; *-semigroup; *-monoid; *-commutativeMonoid
          ; semiring
          )

  rawRing : RawRing _ _
  rawRing = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

  _^_ : Carrier → ℕ → Carrier
  _^_ = Exp._^_ rawRing
  {-# NOINLINE _^_ #-}

  refl : ∀ {x} → x ≈ x
  refl = IsAlmostCommutativeRing.refl isAlmostCommutativeRing

record _-Raw-AlmostCommutative⟶_
         {r₁ r₂ r₃ r₄}
         (From : RawRing r₁ r₂)
         (To : AlmostCommutativeRing r₃ r₄) : Set (r₁ ⊔ r₂ ⊔ r₃ ⊔ r₄) where
  private
    module F = RawRing From
    module T = AlmostCommutativeRing To
  open Morphism.Definitions F.Carrier T.Carrier T._≈_
  field
    ⟦_⟧    : Morphism
    +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
    *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
    -‿homo : Homomorphic₁ ⟦_⟧ F.-_  T.-_
    0-homo : Homomorphic₀ ⟦_⟧ F.0#  T.0#
    1-homo : Homomorphic₀ ⟦_⟧ F.1#  T.1#

-raw-almostCommutative⟶
  : ∀ {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) →
    AlmostCommutativeRing.rawRing R -Raw-AlmostCommutative⟶ R
-raw-almostCommutative⟶ R = record
  { ⟦_⟧    = id
  ; +-homo = λ _ _ → refl
  ; *-homo = λ _ _ → refl
  ; -‿homo = λ _ → refl
  ; 0-homo = refl
  ; 1-homo = refl
  }
  where open AlmostCommutativeRing R

-- A homomorphism induces a notion of equivalence on the raw ring.

Induced-equivalence :
  ∀ {c₁ c₂ c₃ ℓ} {Coeff : RawRing c₁ c₂} {R : AlmostCommutativeRing c₃ ℓ} →
  Coeff -Raw-AlmostCommutative⟶ R → Rel (RawRing.Carrier Coeff) ℓ
Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧
  where
  open AlmostCommutativeRing R
  open _-Raw-AlmostCommutative⟶_ morphism

------------------------------------------------------------------------
-- Conversions

-- Commutative rings are almost commutative rings.

fromCommutativeRing : ∀ {r₁ r₂} (CR : CommutativeRing r₁ r₂) →
                      (open CommutativeRing CR) →
                      (∀ x → Maybe (0# ≈ x)) →
                      AlmostCommutativeRing _ _
fromCommutativeRing CR 0≟_ = record
  { isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = -‿cong
      ; -‿*-distribˡ          = -‿*-distribˡ
      ; -‿+-comm              = ⁻¹-∙-comm
      }
  ; 0≟_ = 0≟_
  }
  where
  open CommutativeRing CR
  open import Algebra.Properties.Ring ring
  open import Algebra.Properties.AbelianGroup +-abelianGroup

fromCommutativeSemiring : ∀ {r₁ r₂} (CS : CommutativeSemiring r₁ r₂)
                          (open CommutativeSemiring CS) →
                          (∀ x → Maybe (0# ≈ x)) →
                          AlmostCommutativeRing _ _
fromCommutativeSemiring CS 0≟_ = record
  { -_                      = id
  ; isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = id
      ; -‿*-distribˡ          = λ _ _ → refl
      ; -‿+-comm              = λ _ _ → refl
      }
  ; 0≟_ = 0≟_
  }
  where open CommutativeSemiring CS


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( Finite )

module Web.Semantic.DL.Category.Object {Σ : Signature} where

infixr 4 _,_

data Object (S T : TBox Σ) : Set₁ where
  _,_ : ∀ X → (X ∈ Finite × ABox Σ X) → Object S T

IN : ∀ {S T} → Object S T → Set
IN (X , X∈Fin , A) = X

fin : ∀ {S T} → (A : Object S T) → (IN A ∈ Finite)
fin (X , X∈Fin , A) = X∈Fin

iface : ∀ {S T} → (A : Object S T) → (ABox Σ (IN A))
iface (X , X∈Fin , A) = A

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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 LibraBFT.Prelude
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Concrete.System.Parameters

-- This module collects the implementation obligations for our (fake/simple, for now)
-- "implementation" into the structure required by Concrete.Properties.
open import LibraBFT.Impl.Properties.Aux
import      LibraBFT.Impl.Properties.VotesOnce   as VO
import      LibraBFT.Impl.Properties.LockedRound as LR
open import LibraBFT.Concrete.Obligations
open import LibraBFT.Concrete.System impl-sps-avp

module LibraBFT.Impl.Properties where
  theImplObligations : ImplObligations
  theImplObligations = record { sps-cor = impl-sps-avp
                              ; vo₁     = VO.vo₁
                              ; vo₂     = VO.vo₂
                              ; lr₁     = LR.lr₁ }

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


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

module Type.Cubical.Logic where

open import Functional
import      Logic.Propositional as Logic
import      Logic.Predicate     as Logic
import      Lvl
open import Type
open import Type.Cubical.Path.Equality
open import Type.Cubical.HTrunc₁
open import Type.Properties.Homotopy
open import Type.Properties.MereProposition
open import Structure.Relator
open import Syntax.Function

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A B C Obj : Type{ℓ}
private variable Pred : Obj → Type{ℓ}

open import Logic.Propositional public using
  ( _∧_ ; [∧]-intro ; [∧]-elimₗ ; [∧]-elimᵣ
  ; _←_ ; [←]-intro ; [←]-elim
  ; _↔_ ; [↔]-intro ; [↔]-elimₗ ; [↔]-elimᵣ ; [↔]-to-[←] ; [↔]-to-[→]
  ; ¬_  ; [¬]-intro ; [¬]-elim
  ; ⊥   ; [⊥]-elim
  ; ⊤   ; [⊤]-intro
  )

_∨_ : Type{ℓ₁} → Type{ℓ₂} → Type
_∨_ = HTrunc₁ ∘₂ (Logic._∨_)

[∨]-introₗ : A → (A ∨ B)
[∨]-introₗ = trunc ∘ Logic.[∨]-introₗ

[∨]-introᵣ : B → (A ∨ B)
[∨]-introᵣ = trunc ∘ Logic.[∨]-introᵣ

[∨]-elim : ⦃ prop-C : MereProposition(C) ⦄ → (A → C) → (B → C) → (A ∨ B) → C
[∨]-elim = HTrunc₁-function ∘₂ Logic.[∨]-elim

instance
  [∨]-prop : MereProposition(A ∨ B)
  [∨]-prop = HTrunc₁-prop

∃ : (Obj → Type{ℓ}) → Type
∃ = HTrunc₁ ∘ Logic.∃

[∃]-intro : (witness : Obj) → ⦃ proof : Pred(witness) ⦄ → ∃(Pred)
[∃]-intro witness = trunc(Logic.[∃]-intro witness)

[∃]-elim : ⦃ prop-A : MereProposition(A) ⦄ → (∀{x : Obj} → Pred(x) → A) → ∃(Pred) → A
[∃]-elim = HTrunc₁-function ∘ Logic.[∃]-elim

instance
  [∃]-prop : MereProposition(∃ Pred)
  [∃]-prop = HTrunc₁-prop

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --type-in-type #-}
module dyn.fib where
open import prelude
open import functors
open import prelude.Stream using (take)
open import prelude.io
open import dyn

fib : Dyn
fib =  (plus   ⊠⊠⊠ delay ℕ) ⟫
    λ  (   f    ,     f₋  ) → f₋ , λ (.tt)
    → ((f₋ , f) ,     f   )
    where plus = fun→dyn (uncurry _ℕ+_)

main : IO ⊤
main = printStream (run fib auto (1 , 1))

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
open import Categories.Category
import Categories.Functor as Fun
open import Categories.Monad
open import Categories.Object.BinaryCoproducts

import Categories.Normalise as Nm

module Categories.Monad.Coproduct {o ℓ e} (C : Category o ℓ e) (coprod : BinCoproducts C) where

open Category C
open Equiv

open BinCoproducts C coprod

module Internal where
  module +Reasoning = Nm.+Reasoning C coprod

  {- ----------------------------------------------------------------------------
     Functoriality of left
  ---------------------------------------------------------------------------- -}

  .left-id : ∀ {X Y} → left id ≡ id {X ∐ Y}
  left-id {X} {Y} = by computation {↑ X ⊎ ↑ Y} (#left #id) #id
    where
    open +Reasoning

  .left-∘ : ∀ {X Y Z W} {f : X ⇒ Y} {g : Y ⇒ Z} → left {C = W} (g ∘ f) ≡ left g ∘ left f
  left-∘ {X} {Y} {Z} {W} {f = f} {g} =
    by computation {↑ X ⊎ ↑ W}
         (#left (↑↑ g #∘ ↑↑ f))
         (#left (↑↑ g) #∘ #left (↑↑ f))
    where
    open +Reasoning

  .left-resp-≡ : ∀ {x y z} → {f g : x ⇒ y} → f ≡ g → left {C = z} f ≡ left {C = z} g
  left-resp-≡ {f = f} {g} p =
    begin
      [ i₁ ∘ f , i₂ ∘ id ]
    ↓⟨ []-cong₂ (∘-resp-≡ʳ p) refl ⟩
      [ i₁ ∘ g , i₂ ∘ id ]
    ∎
    where
    open HomReasoning

  {- ----------------------------------------------------------------------------
     Functoriality of right
  ---------------------------------------------------------------------------- -}

  .right-id : ∀ {X Y} → right id ≡ id {X ∐ Y}
  right-id {X} {Y} = by computation {↑ X ⊎ ↑ Y} (#right #id) #id
    where
    open +Reasoning

  .right-∘ : ∀ {X Y Z W} {f : X ⇒ Y} {g : Y ⇒ Z} → right {A = W} (g ∘ f) ≡ right g ∘ right f
  right-∘ {X} {W = W} {f = f} {g} = by computation {↑ W ⊎ ↑ X}
                                       (#right (↑↑ g #∘ ↑↑ f))
                                       (#right (↑↑ g) #∘ #right (↑↑ f))
    where
    open +Reasoning

  .right-resp-≡ : ∀ {x y z} → {f g : x ⇒ y} → f ≡ g → right {A = z} f ≡ right {A = z} g
  right-resp-≡ {f = f} {g} p =
    begin
      [ i₁ ∘ id , i₂ ∘ f ]
    ↓⟨ []-cong₂ refl (∘-resp-≡ʳ p) ⟩
      [ i₁ ∘ id , i₂ ∘ g ]
    ∎
    where
    open HomReasoning

  {- ----------------------------------------------------------------------------
     Left/Right functors
  ---------------------------------------------------------------------------- -}

  Left : Obj → Fun.Functor C C
  Left A =
   record
    { F₀ = λ X → X ∐ A
    ; F₁ = left
    ; identity = left-id
    ; homomorphism = left-∘
    ; F-resp-≡ = left-resp-≡
    }

  Right : Obj → Fun.Functor C C
  Right A =
   record
    { F₀ = _∐_ A
    ; F₁ = right
    ; identity = right-id
    ; homomorphism = right-∘
    ; F-resp-≡ = right-resp-≡
    }

private module I = Internal

{- ----------------------------------------------------------------------------
     Left/Right monads
---------------------------------------------------------------------------- -}

Left : Obj -> Monad C
Left c =
  record
    { F = I.Left c
    ; η = unit
    ; μ = join
    ; assoc = (λ {x} → by computation {#Left (#Left (#Left (↑ x)))}
                            (#join #∘ #left #join)
                            (#join #∘ #join))
    ; identityˡ = λ {x} → by computation {#Left (↑ x)} (#join #∘ #left #i₁) #id
    ; identityʳ = λ {x} → by computation {#Left (↑ x)} (#join #∘ #i₁) #id
    }
  module Left where
    open I.+Reasoning

    #Left = λ x → x ⊎ ↑ c

    unit = record { η = λ X → i₁
                  ; commute = λ {X} {Y} f → by computation {↑ X} {#Left (↑ Y)}
                                    (#i₁ #∘ ↑↑ f) (#left (↑↑ f) #∘ #i₁)
                  }

    #join : ∀ {A} -> Term (#Left (#Left A)) (#Left A)
    #join = #[ #id , #i₂ ]

    join = record { η = λ X → [ id , i₂ ]
                  ; commute = λ {X} {Y} f → by computation {#Left (#Left (↑ X))}
                              (#join #∘ #left (#left (↑↑ f)))
                              (#left (↑↑ f) #∘ #join)
                  }

Right : Obj -> Monad C
Right c =
  record
    { F = I.Right c
    ; η = unit
    ; μ = join
    ; assoc = (λ {x} → by computation {#Right (#Right (#Right (↑ x)))}
                            (#join #∘ #right #join)
                            (#join #∘ #join))
    ; identityˡ = λ {x} → by computation {#Right (↑ x)} (#join #∘ #right #i₂) #id
    ; identityʳ = λ {x} → by computation {#Right (↑ x)} (#join #∘ #i₂) #id
    }
  module Right where
    open I.+Reasoning

    #Right = λ x → ↑ c ⊎ x

    unit = record { η = λ X → i₂
                  ; commute = λ {X} {Y} f → by computation {↑ X} {#Right (↑ Y)}
                                    (#i₂ #∘ ↑↑ f) (#right (↑↑ f) #∘ #i₂)
                  }

    #join : ∀ {A} -> Term (#Right (#Right A)) (#Right A)
    #join = #[ #i₁ , #id ]

    join = record { η = λ X → [ i₁ , id ]
                  ; commute = λ {X} {Y} f → by computation {#Right (#Right (↑ X))}
                              (#join #∘ #right (#right (↑↑ f)))
                              (#right (↑↑ f) #∘ #join)
                  }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Level
open import Function using () renaming (_∘_ to _∙_)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂; zip; map; <_,_>; swap)

open import Categories.Utils.Product
open import Categories.Category using (Category)
open import Categories.Category.Groupoid using (IsGroupoid)
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation.Core
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl)
import Categories.Morphism as Morphism

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level
    o₁ ℓ₁ e₁ o′₁ ℓ′₁ e′₁ o₂ ℓ₂ e₂ o′₂ ℓ′₂ e′₂ : Level

    C C₁ C₂ D D₁ D₂ : Category o ℓ e

Product : (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Product C D = record
  { Obj       = C.Obj × D.Obj
  ; _⇒_       = C._⇒_ -< _×_ >- D._⇒_
  ; _≈_       = C._≈_ -< _×_ >- D._≈_
  ; _∘_       = zip C._∘_ D._∘_
  ; id        = C.id , D.id
  ; assoc     = C.assoc , D.assoc
  ; sym-assoc = C.sym-assoc , D.sym-assoc
  ; identityˡ = C.identityˡ , D.identityˡ
  ; identityʳ = C.identityʳ , D.identityʳ
  ; identity² = C.identity² , D.identity²
  ; equiv     = record
    { refl  = C.Equiv.refl , D.Equiv.refl
    ; sym   = map C.Equiv.sym D.Equiv.sym
    ; trans = zip C.Equiv.trans D.Equiv.trans
    }
  ; ∘-resp-≈  = zip C.∘-resp-≈ D.∘-resp-≈
  }
  where module C = Category C
        module D = Category D

-- product of functors sharing the same domain
infixr 2 _※_
_※_ : ∀ (F : Functor C D₁) → (G : Functor C D₂) → Functor C (Product D₁ D₂)
F ※ G = record
  { F₀           = < F.F₀ , G.F₀ >
  ; F₁           = < F.F₁ , G.F₁ >
  ; identity     = F.identity , G.identity
  ; homomorphism = F.homomorphism , G.homomorphism
  ; F-resp-≈     = < F.F-resp-≈ , G.F-resp-≈ >
  }
  where module F = Functor F
        module G = Functor G

-- general product of functors
infixr 2 _⁂_
_⁂_ : ∀ (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) → Functor (Product C₁ C₂) (Product D₁ D₂)
F ⁂ G = record
  { F₀           = map F.F₀ G.F₀
  ; F₁           = map F.F₁ G.F₁
  ; identity     = F.identity , G.identity
  ; homomorphism = F.homomorphism , G.homomorphism
  ; F-resp-≈     = map F.F-resp-≈ G.F-resp-≈
  }
  where module F = Functor F
        module G = Functor G

-- Natural Transformations respect the ⁂ product
infixr 5 _⁂ⁿ_
_⁂ⁿ_ : ∀ {C₁ : Category o₁ ℓ₁ e₁} {D₁ : Category o′₁ ℓ′₁ e′₁}
         {C₂ : Category o₂ ℓ₂ e₂} {D₂ : Category o′₂ ℓ′₂ e′₂}
         {F₁ G₁ : Functor C₁ D₁} {F₂ G₂ : Functor C₂ D₂}
         (α : NaturalTransformation F₁ G₁) (β : NaturalTransformation F₂ G₂) →
         NaturalTransformation (F₁ ⁂ F₂) (G₁ ⁂ G₂)
α ⁂ⁿ β = ntHelper record
  { η       = map⁎′ α.η β.η
  ; commute = map⁎′ α.commute β.commute
  }
  where module α = NaturalTransformation α
        module β = NaturalTransformation β

-- Natural Transformations respect the ※ product as well
infixr 5 _※ⁿ_
_※ⁿ_ : ∀ {D₁ : Category o ℓ e} {D₂ : Category o′ ℓ′ e′}
         {F₁ G₁ : Functor C D₁} {F₂ G₂ : Functor C D₂}
         (α : NaturalTransformation F₁ G₁) →
         (β : NaturalTransformation F₂ G₂) →
         NaturalTransformation (F₁ ※ F₂) (G₁ ※ G₂)
α ※ⁿ β = ntHelper record
  { η       = < α.η , β.η >
  ; commute = < α.commute , β.commute >
  }
  where module α = NaturalTransformation α
        module β = NaturalTransformation β

-- Natural Isomorphisms too
infixr 5 _⁂ⁿⁱ_
_⁂ⁿⁱ_ : ∀ {C₁ : Category o₁ ℓ₁ e₁} {D₁ : Category o′₁ ℓ′₁ e′₁}
          {C₂ : Category o₂ ℓ₂ e₂} {D₂ : Category o′₂ ℓ′₂ e′₂}
          {F₁ G₁ : Functor C₁ D₁} {F₂ G₂ : Functor C₂ D₂}
          (α : NaturalIsomorphism F₁ G₁) (β : NaturalIsomorphism F₂ G₂) →
          NaturalIsomorphism (F₁ ⁂ F₂) (G₁ ⁂ G₂)
α ⁂ⁿⁱ β = record
  { F⇒G = α.F⇒G ⁂ⁿ β.F⇒G
  ; F⇐G = α.F⇐G ⁂ⁿ β.F⇐G
  ; iso = λ where
    (X , Y) → record
      { isoˡ = isoˡ (α.iso X) , isoˡ (β.iso Y)
      ; isoʳ = isoʳ (α.iso X) , isoʳ (β.iso Y)
      }
  }
  where module α = NaturalIsomorphism α
        module β = NaturalIsomorphism β
        open Morphism.Iso

-- Natural Isomorphisms too
infixr 5 _※ⁿⁱ_
_※ⁿⁱ_ : ∀ {D₁ : Category o ℓ e} {D₂ : Category o′ ℓ′ e′}
          {F₁ G₁ : Functor C D₁} {F₂ G₂ : Functor C D₂}
          (α : NaturalIsomorphism F₁ G₁) →
          (β : NaturalIsomorphism F₂ G₂) →
          NaturalIsomorphism (F₁ ※ F₂) (G₁ ※ G₂)
α ※ⁿⁱ β = record
  { F⇒G = α.F⇒G ※ⁿ β.F⇒G
  ; F⇐G = α.F⇐G ※ⁿ β.F⇐G
  ; iso = λ X → record
    { isoˡ = isoˡ (α.iso X) , isoˡ (β.iso X)
    ; isoʳ = isoʳ (α.iso X) , isoʳ (β.iso X)
    }
  }
  where module α = NaturalIsomorphism α
        module β = NaturalIsomorphism β
        open Morphism.Iso

module _ (C₁ : Category o ℓ e) (C₂ : Category o′ ℓ′ e′) (C₃ : Category o″ ℓ″ e″) where

  private
    module C₁ = Category C₁
    module C₂ = Category C₂
    module C₃ = Category C₃

  assocˡ : Functor (Product (Product C₁ C₂) C₃) (Product C₁ (Product C₂ C₃))
  assocˡ = record
    { F₀           = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
    ; F₁           = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
    ; identity     = C₁.Equiv.refl , C₂.Equiv.refl , C₃.Equiv.refl
    ; homomorphism = C₁.Equiv.refl , C₂.Equiv.refl , C₃.Equiv.refl
    ; F-resp-≈     = < proj₁ ∙ proj₁ , < proj₂ ∙ proj₁ , proj₂ > >
    }

  assocʳ : Functor (Product C₁ (Product C₂ C₃)) (Product (Product C₁ C₂) C₃)
  assocʳ = record
    { F₀           = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
    ; F₁           = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
    ; identity     = (C₁.Equiv.refl , C₂.Equiv.refl) , C₃.Equiv.refl
    ; homomorphism = (C₁.Equiv.refl , C₂.Equiv.refl) , C₃.Equiv.refl
    ; F-resp-≈     = < < proj₁ , proj₁ ∙ proj₂ > , proj₂ ∙ proj₂ >
    }

module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} where

  private
    module C = Category C
    module D = Category D

  πˡ : Functor (Product C D) C
  πˡ = record
    { F₀           = proj₁
    ; F₁           = proj₁
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = proj₁
    }
    where open C.Equiv using (refl)

  πʳ : Functor (Product C D) D
  πʳ = record
    { F₀           = proj₂
    ; F₁           = proj₂
    ; identity     = refl
    ; homomorphism = refl
    ; F-resp-≈     = proj₂
    }
    where open D.Equiv using (refl)

  Swap : Functor (Product C D) (Product D C)
  Swap = record
    { F₀           = swap
    ; F₁           = swap
    ; identity     = D.Equiv.refl , C.Equiv.refl
    ; homomorphism = D.Equiv.refl , C.Equiv.refl
    ; F-resp-≈     = swap
    }

-- Groupoid Product
Groupoid-× : {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂}
        → IsGroupoid C → IsGroupoid D → IsGroupoid (Product C D)
Groupoid-× c₁ c₂ = record
    { _⁻¹ = map (IsGroupoid._⁻¹ c₁) (IsGroupoid._⁻¹ c₂)
    ; iso = record { isoˡ = Iso.isoˡ i₁ , Iso.isoˡ i₂
                   ; isoʳ = Iso.isoʳ i₁ , Iso.isoʳ i₂
                   }
    }
  where
  open Morphism
  i₁ = IsGroupoid.iso c₁
  i₂ = IsGroupoid.iso c₂

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import HoTT
open import homotopy.HSpace
open import homotopy.EilenbergMacLane1 using (EM₁-level₁)

module homotopy.EM1HSpace where

module EM₁HSpace {i} (G : AbGroup i) where

  private
    module G = AbGroup G

    emloop-commutes : (g g' : G.El) → emloop g ∙ emloop g' == emloop g' ∙ emloop g
    emloop-commutes g g' =
      emloop g ∙ emloop g'
        =⟨ ! (emloop-comp' G.grp g g') ⟩
      emloop (G.comp g g')
        =⟨ ap (emloop' G.grp) (G.comm g g') ⟩
      emloop (G.comp g' g)
        =⟨ emloop-comp' G.grp g' g ⟩
      emloop g' ∙ emloop g =∎

  mult-loop : G.El → (x : EM₁ G.grp) → x == x
  mult-loop g = EM₁-set-elim
    {P = λ x → x == x}
    {{λ x → has-level-apply (EM₁-level₁ G.grp) x x}}
    (emloop g)
    (λ g' → ↓-idf=idf-in' (emloop-commutes g g' ∙ ∙=∙' (emloop g') (emloop g)))

  private
    EM₁-endo-Ω-group : Group i
    EM₁-endo-Ω-group = Ω^S-group 0 ⊙[ (EM₁ G.grp → EM₁ G.grp) , (λ x → x) ]

    mult-hom : GroupHom G.grp EM₁-endo-Ω-group
    mult-hom = record {f = λ= ∘ mult-loop; pres-comp = pres-comp}
      where
      abstract
        pres-comp' : (g₁ g₂ : G.El) (x : EM₁ G.grp) →
          mult-loop (G.comp g₁ g₂) x == mult-loop g₁ x ∙ mult-loop g₂ x
        pres-comp' g₁ g₂ =
          EM₁-prop-elim
            {P = λ x → mult-loop (G.comp g₁ g₂) x == mult-loop g₁ x ∙ mult-loop g₂ x}
            {{λ x → has-level-apply (has-level-apply (EM₁-level₁ G.grp) _ _) _ _}}
            (emloop-comp g₁ g₂)

        pres-comp : (g₁ g₂ : G.El)
          → λ= (mult-loop (G.comp g₁ g₂)) ==
            Group.comp EM₁-endo-Ω-group (λ= (mult-loop g₁)) (λ= (mult-loop g₂))
        pres-comp g₁ g₂ =
          ap λ= (λ= (pres-comp' g₁ g₂)) ∙
          =ₛ-out (λ=-∙ (mult-loop g₁) (mult-loop g₂))

    module MultRec = EM₁Level₁Rec {G = G.grp} {C = EM₁ G.grp → EM₁ G.grp} (λ x → x) mult-hom

  abstract
    mult : EM₁ G.grp → EM₁ G.grp → EM₁ G.grp
    mult = MultRec.f

    mult-embase-β : mult embase ↦ (λ x → x)
    mult-embase-β = MultRec.embase-β
    {-# REWRITE mult-embase-β #-}

    mult-emloop-β : ∀ g y → ap (λ x → mult x y) (emloop g) == mult-loop g y
    mult-emloop-β g y =
      ap (λ x → mult x y) (emloop g)
        =⟨ ap-∘ (λ f → f y) mult (emloop g) ⟩
      app= (ap mult (emloop g)) y
        =⟨ ap (λ w → app= w y) (MultRec.emloop-β g) ⟩
      app= (λ= (mult-loop g)) y
        =⟨ app=-β (mult-loop g) y ⟩
      mult-loop g y =∎

  H-⊙EM₁ : HSpaceStructure (⊙EM₁ G.grp)
  H-⊙EM₁ = from-alt-h-space $ record { μ = mult; unit-l = unit-l; unit-r = unit-r; coh = coh }
    where
    unit-l : (x : EM₁ G.grp) → mult embase x == x
    unit-l x = idp

    unit-r : (x : EM₁ G.grp) → mult x embase == x
    unit-r = EM₁-set-elim
      {P = λ x → mult x embase == x}
      {{λ x → has-level-apply (EM₁-level₁ G.grp) (mult x embase) x}}
      idp
      (λ g → ↓-app=idf-in $
         idp ∙' emloop g
           =⟨ ∙'-unit-l (emloop g) ⟩
         emloop g
           =⟨ ! (mult-emloop-β g embase) ⟩
         ap (λ z → mult z embase) (emloop g)
           =⟨ ! (∙-unit-r (ap (λ z → mult z embase) (emloop g))) ⟩
         ap (λ z → mult z embase) (emloop g) ∙ idp ∎)

    coh : unit-l embase == unit-r embase
    coh = idp

  open HSpaceStructure H-⊙EM₁

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module InstanceArgumentsConstraintsModule where

data Bool : Set where
  true false : Bool

module M (A1 A2 B C : Set) (a1 : A1) (a2 : A2) where

  record Class (R : Bool → Set) : Set where
    field f : (t : Bool) → R t

  open Class {{...}} public

  instance
    class1 : Class (λ _ → A1)
    class1 = record { f = λ _ → a1 }

    class2 : Class (λ _ → A2)
    class2 = record { f = λ _ → a2 }

module N (A1 A2 B C : Set) (a1 : A1) (a2 : A2) where

  postulate someF : A1 → C

  open M A1 A2 B C a1 a2

  test : C
  test = someF (f true)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Properties of homogeneous binary relations
------------------------------------------------------------------------

module Relation.Binary where

open import Data.Product
open import Data.Sum
open import Data.Function
import Relation.Binary.PropositionalEquality.Core as PropEq
open import Relation.Binary.Consequences
open import Relation.Binary.Core as Core using (_≡_)

------------------------------------------------------------------------
-- Simple properties and equivalence relations

open Core public hiding (_≡_; refl; _≢_)

------------------------------------------------------------------------
-- Preorders

record IsPreorder {a : Set}
                  (_≈_ : Rel a) -- The underlying equality.
                  (_∼_ : Rel a) -- The relation.
                  : Set where
  field
    isEquivalence : IsEquivalence _≈_
    -- Reflexivity is expressed in terms of an underlying equality:
    reflexive     : _≈_ ⇒ _∼_
    trans         : Transitive _∼_
    ∼-resp-≈      : _∼_ Respects₂ _≈_

  module Eq = IsEquivalence isEquivalence

  refl : Reflexive _∼_
  refl = reflexive Eq.refl

record Preorder : Set₁ where
  infix 4 _≈_ _∼_
  field
    carrier    : Set
    _≈_        : Rel carrier  -- The underlying equality.
    _∼_        : Rel carrier  -- The relation.
    isPreorder : IsPreorder _≈_ _∼_

  open IsPreorder isPreorder public

------------------------------------------------------------------------
-- Setoids

-- Equivalence relations are defined in Relation.Binary.Core.

record Setoid : Set₁ where
  infix 4 _≈_
  field
    carrier       : Set
    _≈_           : Rel carrier
    isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public

  isPreorder : IsPreorder _≡_ _≈_
  isPreorder = record
    { isEquivalence = PropEq.isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    ; ∼-resp-≈      = PropEq.resp₂ _≈_
    }

  preorder : Preorder
  preorder = record { isPreorder = isPreorder }

------------------------------------------------------------------------
-- Decidable equivalence relations

record IsDecEquivalence {a : Set} (_≈_ : Rel a) : Set where
  field
    isEquivalence : IsEquivalence _≈_
    _≟_           : Decidable _≈_

  open IsEquivalence isEquivalence public

record DecSetoid : Set₁ where
  infix 4 _≈_
  field
    carrier          : Set
    _≈_              : Rel carrier
    isDecEquivalence : IsDecEquivalence _≈_

  open IsDecEquivalence isDecEquivalence public

  setoid : Setoid
  setoid = record { isEquivalence = isEquivalence }

  open Setoid setoid public using (preorder)

------------------------------------------------------------------------
-- Partial orders

record IsPartialOrder {a : Set} (_≈_ _≤_ : Rel a) : Set where
  field
    isPreorder : IsPreorder _≈_ _≤_
    antisym    : Antisymmetric _≈_ _≤_

  open IsPreorder isPreorder public
         renaming (∼-resp-≈ to ≤-resp-≈)

record Poset : Set₁ where
  infix 4 _≈_ _≤_
  field
    carrier        : Set
    _≈_            : Rel carrier
    _≤_            : Rel carrier
    isPartialOrder : IsPartialOrder _≈_ _≤_

  open IsPartialOrder isPartialOrder public

  preorder : Preorder
  preorder = record { isPreorder = isPreorder }

------------------------------------------------------------------------
-- Strict partial orders

record IsStrictPartialOrder {a : Set} (_≈_ _<_ : Rel a) : Set where
  field
    isEquivalence : IsEquivalence _≈_
    irrefl        : Irreflexive _≈_ _<_
    trans         : Transitive _<_
    <-resp-≈      : _<_ Respects₂ _≈_

  module Eq = IsEquivalence isEquivalence

record StrictPartialOrder : Set₁ where
  infix 4 _≈_ _<_
  field
    carrier              : Set
    _≈_                  : Rel carrier
    _<_                  : Rel carrier
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_

  open IsStrictPartialOrder isStrictPartialOrder public

------------------------------------------------------------------------
-- Total orders

record IsTotalOrder {a : Set} (_≈_ _≤_ : Rel a) : Set where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    total          : Total _≤_

  open IsPartialOrder isPartialOrder public

record TotalOrder : Set₁ where
  infix 4 _≈_ _≤_
  field
    carrier      : Set
    _≈_          : Rel carrier
    _≤_          : Rel carrier
    isTotalOrder : IsTotalOrder _≈_ _≤_

  open IsTotalOrder isTotalOrder public

  poset : Poset
  poset = record { isPartialOrder = isPartialOrder }

  open Poset poset public using (preorder)

------------------------------------------------------------------------
-- Decidable total orders

record IsDecTotalOrder {a : Set} (_≈_ _≤_ : Rel a) : Set where
  field
    isTotalOrder : IsTotalOrder _≈_ _≤_
    _≟_          : Decidable _≈_
    _≤?_         : Decidable _≤_

  private
    module TO = IsTotalOrder isTotalOrder
  open TO public hiding (module Eq)

  module Eq where

    isDecEquivalence : IsDecEquivalence _≈_
    isDecEquivalence = record
      { isEquivalence = TO.isEquivalence
      ; _≟_           = _≟_
      }

    open IsDecEquivalence isDecEquivalence public

record DecTotalOrder : Set₁ where
  infix 4 _≈_ _≤_
  field
    carrier         : Set
    _≈_             : Rel carrier
    _≤_             : Rel carrier
    isDecTotalOrder : IsDecTotalOrder _≈_ _≤_

  private
    module DTO = IsDecTotalOrder isDecTotalOrder
  open DTO public hiding (module Eq)

  totalOrder : TotalOrder
  totalOrder = record { isTotalOrder = isTotalOrder }

  open TotalOrder totalOrder public using (poset; preorder)

  module Eq where

    decSetoid : DecSetoid
    decSetoid = record { isDecEquivalence = DTO.Eq.isDecEquivalence }

    open DecSetoid decSetoid public

------------------------------------------------------------------------
-- Strict total orders

-- Note that these orders are decidable (see compare).

record IsStrictTotalOrder {a : Set} (_≈_ _<_ : Rel a) : Set where
  field
    isEquivalence : IsEquivalence _≈_
    trans         : Transitive _<_
    compare       : Trichotomous _≈_ _<_
    <-resp-≈      : _<_ Respects₂ _≈_

  _≟_ : Decidable _≈_
  _≟_ = tri⟶dec≈ compare

  isDecEquivalence : IsDecEquivalence _≈_
  isDecEquivalence = record
    { isEquivalence = isEquivalence
    ; _≟_           = _≟_
    }

  module Eq = IsDecEquivalence isDecEquivalence

  isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
  isStrictPartialOrder = record
    { isEquivalence = isEquivalence
    ; irrefl        = tri⟶irr <-resp-≈ Eq.sym compare
    ; trans         = trans
    ; <-resp-≈      = <-resp-≈
    }

  open IsStrictPartialOrder isStrictPartialOrder using (irrefl)

record StrictTotalOrder : Set₁ where
  infix 4 _≈_ _<_
  field
    carrier            : Set
    _≈_                : Rel carrier
    _<_                : Rel carrier
    isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_

  open IsStrictTotalOrder isStrictTotalOrder public
    hiding (module Eq)

  strictPartialOrder : StrictPartialOrder
  strictPartialOrder =
    record { isStrictPartialOrder = isStrictPartialOrder }

  decSetoid : DecSetoid
  decSetoid = record { isDecEquivalence = isDecEquivalence }

  module Eq = DecSetoid decSetoid

max_issues_repo_name: larrytheliquid/Lemmachine