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.Hash
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Encode
open import LibraBFT.Base.PKCS
open import LibraBFT.Impl.Consensus.Types.EpochIndep

-- This module postulates a collision-resistant cryptographic hash
-- function (we call it sha256 for concreteness, but it could be any
-- collision-resistant cryptographic hash function), and defines hash
-- functions used in (an earlier version of) LibraBFT, properties
-- about it, and how Votes and Blocks are signed.

module LibraBFT.Impl.Util.Crypto where
  -- Note that this is an abstraction of a collision-resistant hash function.  It could be any such
  -- hash function, not necessarily sha256.  We just call it sha256 for "concreteness", to remind
  -- ourselves it's modeling such a function.
  postulate -- valid assumption (collision-resistant hash function)
    sha256    : BitString → Hash
    sha256-cr : ∀{x y} → sha256 x ≡ sha256 y → Collision sha256 x y ⊎ x ≡ y

  open WithCryptoHash sha256 sha256-cr

  blockInfoBSList : BlockInfo → List ByteString
  blockInfoBSList (BlockInfo∙new epoch round id) = encode epoch ∷ encode round ∷ encode id ∷ []

  hashBI : BlockInfo → HashValue
  hashBI = sha256 ∘ bs-concat ∘ blockInfoBSList

  hashBI-inj : ∀ {bi1 bi2} → hashBI bi1 ≡ hashBI bi2 → NonInjective-≡ sha256 ⊎ bi1 ≡ bi2
  hashBI-inj {bi1} {bi2} hyp with sha256-cr hyp
  ...| inj₁ col = inj₁ (_ , col)
  ...| inj₂ res with bs-concat-inj (blockInfoBSList bi1) (blockInfoBSList bi2) res
  ...| final = inj₂ (BlockInfo-η (encode-inj (proj₁ (∷-injective final)))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective final)))))
                                 (encode-inj (proj₁ (∷-injective (proj₂ (∷-injective (proj₂ (∷-injective final))))))))

  voteDataHashList : VoteData → List Hash
  voteDataHashList (VoteData∙new proposed parent) =
    hProposed ∷ hParent ∷ []
   where
    hProposed = hashBI proposed
    hParent   = hashBI parent

  hashVD : VoteData → HashValue
  hashVD = hash-concat ∘ voteDataHashList

  VoteData-≢-eid : ∀ {vd1 vd2 : VoteData}
                 → vd1 ^∙ vdProposed ∙ biEpoch ≢ vd2 ^∙ vdProposed ∙ biEpoch
                 → vd1 ≢ vd2
  VoteData-≢-eid neq = λ x → neq (cong (_^∙ vdProposed ∙ biEpoch) x)

  VoteData-hb : ∀ {vd1 vd2 : VoteData}
              → vd1 ^∙ vdProposed ∙ biEpoch ≢ vd2 ^∙ vdProposed ∙ biEpoch
              → hashVD vd1 ≡ hashVD vd2
              → NonInjective-≡ sha256
  VoteData-hb {vd1} {vd2} neq hvd≡
    with hash-concat-inj {voteDataHashList vd1} {voteDataHashList vd2} hvd≡
  ...| inj₁ hb = hb
  ...| inj₂ xxx
     with cong head xxx
  ...| yyy
     with cong tail xxx
  ...| yyy'
     with cong head (just-injective yyy')
  ...| yyy''
     with just-injective yyy | just-injective yyy''
  ...| zzz | zzz'
     with hashBI-inj {vd1 ^∙ vdProposed} {vd2 ^∙ vdProposed} zzz |
          hashBI-inj {vd1 ^∙ vdParent}   {vd2 ^∙ vdParent}   zzz'
  ...| inj₁ hb  | _         = hb
  ...| inj₂ _   | inj₁ hb   = hb
  ...| inj₂ aaa | inj₂ aaa' = ⊥-elim (VoteData-≢-eid {vd1} {vd2} neq (VoteData-η aaa aaa'))

  hashVD-inj : ∀ {vd1 vd2} → hashVD vd1 ≡ hashVD vd2 → NonInjective-≡ sha256 ⊎ vd1 ≡ vd2
  hashVD-inj {vd1} {vd2} prf
    with hash-concat-inj {voteDataHashList vd1} {voteDataHashList vd2} prf
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ vdLists≡
     with hashBI-inj (proj₁ (∷-injective vdLists≡)) | hashBI-inj (proj₁ (∷-injective (proj₂ (∷-injective vdLists≡))))
  ...| inj₁ hb    | _         = inj₁ hb
  ...| inj₂ _     | inj₁ hb   = inj₁ hb
  ...| inj₂ prop≡ | inj₂ par≡ = inj₂ (VoteData-η prop≡ par≡)

  hashLI : LedgerInfo → HashValue
  hashLI (LedgerInfo∙new commitInfo consensusDataHash) =
    hash-concat (hashBI commitInfo ∷ consensusDataHash ∷ [])

  hashLI-inj : ∀ {li1 li2} → hashLI li1 ≡ hashLI li2 → NonInjective-≡ sha256 ⊎ li1 ≡ li2
  hashLI-inj {LedgerInfo∙new ci1 cd1} {LedgerInfo∙new ci2 cd2} prf
     with hash-concat-inj {hashBI ci1 ∷ cd1 ∷ []} {hashBI ci2 ∷ cd2 ∷ []} prf
  ...| inj₁ hb      = inj₁ hb
  ...| inj₂ li1≡li2
     with ∷-injective li1≡li2
  ...| ci≡ , rest≡
     with ∷-injective rest≡
  ...| cdh≡ , _
     with hashBI-inj ci≡
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ cis≡
     = inj₂ (LedgerInfo-η cis≡ cdh≡)

  constructLI : Vote → LedgerInfo
  constructLI v = LedgerInfo∙new (₋liCommitInfo (₋vLedgerInfo v)) (hashVD (₋vVoteData v))

  hashVote : Vote → HashValue
  hashVote = hashLI ∘ constructLI

  hashVote-inj1 : ∀ {v1 v2} → hashVote v1 ≡ hashVote v2
                → NonInjective-≡ sha256 ⊎ ₋vVoteData v1 ≡ ₋vVoteData v2
  hashVote-inj1 {v1} {v2} hyp with hashLI-inj {constructLI v1} {constructLI v2} hyp
  ...| inj₁ hb = inj₁ hb
  ...| inj₂ ok = hashVD-inj {₋vVoteData v1} {₋vVoteData v2} (cong ₋liConsensusDataHash ok)

  -- A vote is always signed; as seen by the 'Unit'
  -- in the definition of Signed.
  instance
    sig-Vote : WithSig Vote
    sig-Vote = record
       { Signed         = λ _ → Unit
       ; Signed-pi      = λ _ _ _ → Unit-pi
       ; isSigned?      = λ _ → yes unit
       ; signature      = λ v _ → ₋vSignature v
       ; signableFields = encodeH ∘ hashVote
       }

  -- Captures a proof that a vote was cast by α by recording that 'verify' returns true.
  VoteSigVerifies : PK → Vote → Set
  VoteSigVerifies pk v = T (verify (signableFields ⦃ sig-Vote ⦄ v) (₋vSignature v) pk)

  Signed-pi-Blk : (b : Block)
                → (is1 is2 : (Is-just ∘ ₋bSignature) b)
                → is1 ≡ is2
  Signed-pi-Blk (Block∙new _ _ .(just _)) (just _) (just _) = cong just refl

  -- A Block might carry a signature
  instance
    sig-Block : WithSig Block
    sig-Block = record
       { Signed         = Is-just ∘ ₋bSignature
       ; Signed-pi      = Signed-pi-Blk
       ; isSigned?      = λ b → Maybe-Any-dec (λ _ → yes tt) (b ^∙ bSignature)
       ; signature      = λ { _ prf → to-witness prf }
       ; signableFields = λ b → concat (encodeH (₋bId b) ∷ encode (b ^∙ bBlockData) ∷ [])
       }

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:
-- Andreas, 2016-10-12 AIM XXIV, issue #2256

open import Common.Equality

module _ a (A : Set a) where

data ⊥ : Set where

abs : ⊥ → Set a
abs = λ()

test : (x : ⊥) → abs x ≡ A
test x = refl

-- ERROR WAS:
-- (λ ()) a A x != A of type Set a
-- when checking that the expression refl has type abs x ≡ A

-- EXPECTED:
-- (λ ()) x != A of type Set a
-- when checking that the expression refl has type abs x ≡ A

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Equiv where

  import Prelude
  import Eq

  open Prelude
  open Eq

  data Equiv (a : Set) : Set1 where
    equiv :  (_==_  : a -> a -> Set)
          -> (refl  : (x : a) -> x == x)
          -> (sym   : (x y : a) -> x == y -> y == x)
          -> (trans : (x y z : a) -> x == y -> y == z -> x == z)
          -> Equiv a

  rel : {a : Set} -> Equiv a -> (a -> a -> Set)
  rel (equiv _==_ _ _ _) = _==_

  data Decidable {a : Set} (eq : a -> a -> Set) : Set where
    dec : ((x y : a) -> Either (eq x y) (Not (eq x y))) -> Decidable eq

  private
    boolFunctionsDecidable'
      : {a : Set}
      -> (f : a -> a -> Bool)
      -> (x y : a)
      -> (b : Bool)
      -> (b =^= f x y)
      -> Either (T' f x y) (Not (T' f x y))
    boolFunctionsDecidable' eq x y True  p = left (leibnizSubst p T unit)
    boolFunctionsDecidable' eq x y False p =
      right (not (\xy -> leibnizSubst (leibnizSym p) T xy))

  boolFunctionsDecidable
    : {a : Set} -> (f : a -> a -> Bool) -> Decidable (T' f)
  boolFunctionsDecidable f =
    dec (\x y -> boolFunctionsDecidable' f x y (f x y) leibnizRefl)

  data DecidableEquiv (a : Set) : Set1 where
    decEquiv : (eq : Equiv a) -> Decidable (rel eq) -> DecidableEquiv a

  rel' :  {a : Set} -> (eq : DecidableEquiv a) -> (a -> a -> Set)
  rel' (decEquiv eq _) = rel eq

  refl : {a : Set} -> (eq : DecidableEquiv a) -> {x : a} -> rel' eq x x
  refl (decEquiv (equiv _ refl' _ _) _) = refl' _

  sym : {a : Set} -> (eq : DecidableEquiv a) -> {x y : a}
      -> rel' eq x y -> rel' eq y x
  sym (decEquiv (equiv _ _ sym' _) _) = sym' _ _

  trans : {a : Set} -> (eq : DecidableEquiv a) -> {x y z : a}
      -> rel' eq x y -> rel' eq y z -> rel' eq x z
  trans (decEquiv (equiv _ _ _ trans') _) = trans' _ _ _

  decRel :  {a : Set} -> (eq : DecidableEquiv a) -> (x y : a)
         -> Either (rel' eq x y) (Not (rel' eq x y))
  decRel (decEquiv _ (dec f)) = f

  private

    decRelI :  {a : Set} -> (eq : a -> a -> Set) -> {x y : a}
             -> Either (eq x y) (Not (eq x y)) -> Bool
    decRelI _ (left _)  = True
    decRelI _ (right _) = False

  decRel' : {a : Set} -> DecidableEquiv a -> (a -> a -> Bool)
  decRel' eq x y = decRelI (rel' eq) (decRel eq x y)

  private
    pairEq :  {a b : Set} -> DecidableEquiv a -> DecidableEquiv b
           -> (p1 p2 : Pair a b) -> Set
    pairEq a b (pair x1 x2) (pair y1 y2) = Pair (rel' a x1 y1) (rel' b x2 y2)

    refl' :  {a b : Set} -> (da : DecidableEquiv a) -> (db : DecidableEquiv b)
          -> (x : Pair a b) -> pairEq da db x x
    refl' a b (pair x1 x2) = pair (refl a) (refl b)

    sym' :  {a b : Set} -> (da : DecidableEquiv a) -> (db : DecidableEquiv b)
         -> (x y : Pair a b) -> pairEq da db x y -> pairEq da db y x
    sym' a b (pair x1 x2) (pair y1 y2) (pair xy1 xy2) =
      pair (sym a xy1) (sym b xy2)

    trans'
      :  {a b : Set} -> (da : DecidableEquiv a) -> (db : DecidableEquiv b)
      -> (x y z : Pair a b)
      -> pairEq da db x y -> pairEq da db y z -> pairEq da db x z
    trans' a b (pair x1 x2) (pair y1 y2)
           (pair z1 z2) (pair xy1 xy2) (pair yz1 yz2) =
      pair (trans a xy1 yz1) (trans b xy2 yz2)

    dec'' :  {a b : Set} -> {da : DecidableEquiv a} -> {db : DecidableEquiv b}
          -> {x1 y1 : a} -> {x2 y2 : b}
          -> Either (rel' da x1 y1) (Not (rel' da x1 y1))
          -> Either (rel' db x2 y2) (Not (rel' db x2 y2))
          -> Either (pairEq da db (pair x1 x2) (pair y1 y2))
                    (Not (pairEq da db (pair x1 x2) (pair y1 y2)))
    dec'' (left xy1)         (left xy2)         = left (pair xy1 xy2)
    dec'' _                  (right (not nxy2)) =
      right (not (\xy -> nxy2 (snd xy)))
    dec'' (right (not nxy1)) (left _)           =
      right (not (\xy -> nxy1 (fst xy)))

    dec' :  {a b : Set} -> (da : DecidableEquiv a) -> (db : DecidableEquiv b)
         -> (x y : Pair a b) -> Either (pairEq da db x y) (Not (pairEq da db x y))
    dec' a b (pair x1 x2) (pair y1 y2) =
      dec'' {_} {_} {a} {b} (decRel a x1 y1) (decRel b x2 y2)

  pairEquiv
    :  {a b : Set} -> DecidableEquiv a -> DecidableEquiv b
    -> DecidableEquiv (Pair a b)
  pairEquiv a b = decEquiv (equiv (pairEq a b)
                                  (refl' a b) (sym' a b) (trans' a b))
                           (dec (dec' a b))


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Matrix where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                       ; +-comm to +ℕ-comm
                                       ; +-assoc to +ℕ-assoc
                                       ; ·-assoc to ·ℕ-assoc)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- Equivalence between Vec matrix and Fin function matrix

FinMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
FinMatrix A m n = FinVec (FinVec A n) m

VecMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
VecMatrix A m n = Vec (Vec A n) m

FinMatrix→VecMatrix : {m n : ℕ} → FinMatrix A m n → VecMatrix A m n
FinMatrix→VecMatrix M = FinVec→Vec (λ fm → FinVec→Vec (M fm))

VecMatrix→FinMatrix : {m n : ℕ} → VecMatrix A m n → FinMatrix A m n
VecMatrix→FinMatrix M fn fm = lookup fm (lookup fn M)

FinMatrix→VecMatrix→FinMatrix : {m n : ℕ} (M : FinMatrix A m n)
                              → VecMatrix→FinMatrix (FinMatrix→VecMatrix M) ≡ M
FinMatrix→VecMatrix→FinMatrix {m = zero} M = funExt (⊥.rec ∘ ¬Fin0)
FinMatrix→VecMatrix→FinMatrix {n = zero} M = funExt₂ (λ _ → ⊥.rec ∘ ¬Fin0)
FinMatrix→VecMatrix→FinMatrix {m = suc m} {n = suc n} M = funExt₂ goal
  where
  goal : (fm : Fin (suc m)) (fn : Fin (suc n))
       → VecMatrix→FinMatrix (_ ∷ FinMatrix→VecMatrix (M ∘ suc)) fm fn ≡ M fm fn
  goal zero zero       = refl
  goal zero (suc fn) i = FinVec→Vec→FinVec (M zero ∘ suc) i fn
  goal (suc fm) fn i   = FinMatrix→VecMatrix→FinMatrix (M ∘ suc) i fm fn

VecMatrix→FinMatrix→VecMatrix : {m n : ℕ} (M : VecMatrix A m n)
                              → FinMatrix→VecMatrix (VecMatrix→FinMatrix M) ≡ M
VecMatrix→FinMatrix→VecMatrix {m = zero} [] = refl
VecMatrix→FinMatrix→VecMatrix {m = suc m} (M ∷ MS) i =
  Vec→FinVec→Vec M i ∷ VecMatrix→FinMatrix→VecMatrix MS i

FinMatrixIsoVecMatrix : (A : Type ℓ) (m n : ℕ) → Iso (FinMatrix A m n) (VecMatrix A m n)
fun (FinMatrixIsoVecMatrix A m n)      = FinMatrix→VecMatrix
inv (FinMatrixIsoVecMatrix A m n)      = VecMatrix→FinMatrix
rightInv (FinMatrixIsoVecMatrix A m n) = VecMatrix→FinMatrix→VecMatrix
leftInv (FinMatrixIsoVecMatrix A m n)  = FinMatrix→VecMatrix→FinMatrix

FinMatrix≃VecMatrix : {m n : ℕ} → FinMatrix A m n ≃ VecMatrix A m n
FinMatrix≃VecMatrix {_} {A} {m} {n} = isoToEquiv (FinMatrixIsoVecMatrix A m n)

FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
FinMatrix≡VecMatrix _ _ _ = ua FinMatrix≃VecMatrix

-- Define abelian group structure on matrices
module FinMatrixAbGroup (G' : AbGroup ℓ) where

  open AbGroupStr (snd G') renaming ( is-set to isSetG )
  private G = ⟨ G' ⟩

  zeroFinMatrix : ∀ {m n} → FinMatrix G m n
  zeroFinMatrix _ _ = 0g

  negFinMatrix : ∀ {m n} → FinMatrix G m n → FinMatrix G m n
  negFinMatrix M i j = - M i j

  addFinMatrix : ∀ {m n} → FinMatrix G m n → FinMatrix G m n → FinMatrix G m n
  addFinMatrix M N i j = M i j + N i j

  isSetFinMatrix : ∀ {m n} → isSet (FinMatrix G m n)
  isSetFinMatrix = isSetΠ2 λ _ _ → isSetG

  addFinMatrixAssoc : ∀ {m n} → (M N K : FinMatrix G m n)
                    → addFinMatrix M (addFinMatrix N K) ≡ addFinMatrix (addFinMatrix M N) K
  addFinMatrixAssoc M N K i j k = assoc (M j k) (N j k) (K j k) i

  addFinMatrix0r : ∀ {m n} → (M : FinMatrix G m n)
                 → addFinMatrix M zeroFinMatrix ≡ M
  addFinMatrix0r M i j k = rid (M j k) i

  addFinMatrix0l : ∀ {m n} → (M : FinMatrix G m n)
                 → addFinMatrix zeroFinMatrix M ≡ M
  addFinMatrix0l M i j k = lid (M j k) i

  addFinMatrixNegMatrixr : ∀ {m n} → (M : FinMatrix G m n)
                         → addFinMatrix M (negFinMatrix M) ≡ zeroFinMatrix
  addFinMatrixNegMatrixr M i j k = invr (M j k) i

  addFinMatrixNegMatrixl : ∀ {m n} → (M : FinMatrix G m n)
                         → addFinMatrix (negFinMatrix M) M ≡ zeroFinMatrix
  addFinMatrixNegMatrixl M i j k = invl (M j k) i

  addFinMatrixComm : ∀ {m n} → (M N : FinMatrix G m n)
                   → addFinMatrix M N ≡ addFinMatrix N M
  addFinMatrixComm M N i k l = comm (M k l) (N k l) i

  FinMatrixAbGroup : (m n : ℕ) → AbGroup ℓ
  FinMatrixAbGroup m n =
    makeAbGroup {G = FinMatrix G m n} zeroFinMatrix addFinMatrix negFinMatrix
                isSetFinMatrix addFinMatrixAssoc addFinMatrix0r
                addFinMatrixNegMatrixr addFinMatrixComm

-- Define a abelian group structure on vector matrices and prove that
-- it is equal to FinMatrixAbGroup using the SIP
module _ (G' : AbGroup ℓ) where

  open AbGroupStr (snd G')
  private G = ⟨ G' ⟩
  zeroVecMatrix : ∀ {m n} → VecMatrix G m n
  zeroVecMatrix = replicate (replicate 0g)

  negVecMatrix : ∀ {m n} → VecMatrix G m n → VecMatrix G m n
  negVecMatrix = map (map (λ x → - x))

  addVec : ∀ {m} → Vec G m → Vec G m → Vec G m
  addVec [] [] = []
  addVec (x ∷ xs) (y ∷ ys) = x + y ∷ addVec xs ys

  addVecMatrix : ∀ {m n} → VecMatrix G m n → VecMatrix G m n → VecMatrix G m n
  addVecMatrix [] [] = []
  addVecMatrix (M ∷ MS) (N ∷ NS) = addVec M N ∷ addVecMatrix MS NS

  open FinMatrixAbGroup

  -- Proof that FinMatrix→VecMatrix is a group homorphism
  FinMatrix→VecMatrixHomAdd : (m n : ℕ) (M N : FinMatrix G m n)
    → FinMatrix→VecMatrix (addFinMatrix G' M N) ≡
      addVecMatrix (FinMatrix→VecMatrix M) (FinMatrix→VecMatrix N)
  FinMatrix→VecMatrixHomAdd zero n M N = refl
  FinMatrix→VecMatrixHomAdd (suc m) n M N =
    λ i → lem n (M zero) (N zero) i
        ∷ FinMatrix→VecMatrixHomAdd m n (λ i j → M (suc i) j) (λ i j → N (suc i) j) i
     where
     lem : (n : ℕ) (V W : FinVec G n)
       → FinVec→Vec (λ j → V j + W j) ≡ addVec (FinVec→Vec V) (FinVec→Vec W)
     lem zero V W = refl
     lem (suc n) V W = λ i → V zero + W zero ∷ lem n (V ∘ suc) (W ∘ suc) i

  -- Combine everything to get an induced abelian group structure of
  -- VecMatrix that is equal to the one on FinMatrix
  VecMatrixAbGroup : (m n : ℕ) → AbGroup ℓ
  VecMatrixAbGroup m n =
    InducedAbGroup (FinMatrixAbGroup G' m n) addVecMatrix
      FinMatrix≃VecMatrix (FinMatrix→VecMatrixHomAdd m n)

  FinMatrixAbGroup≡VecMatrixAbGroup : (m n : ℕ) → FinMatrixAbGroup G' m n ≡ VecMatrixAbGroup m n
  FinMatrixAbGroup≡VecMatrixAbGroup m n =
    InducedAbGroupPath (FinMatrixAbGroup G' m n) addVecMatrix
      FinMatrix≃VecMatrix (FinMatrix→VecMatrixHomAdd m n)

-- Define identity matrix and matrix multiplication for FinMatrix and
-- prove that square matrices form a ring
module _ (R' : Ring ℓ) where

  open RingStr (snd R') renaming ( is-set to isSetR )
  open RingTheory R'
  open KroneckerDelta R'
  open Sum R'
  open FinMatrixAbGroup (_ , abgroupstr _ _ _ (snd R' .RingStr.+IsAbGroup))

  private R = ⟨ R' ⟩

  oneFinMatrix : ∀ {n} → FinMatrix R n n
  oneFinMatrix i j = δ i j

  mulFinMatrix : ∀ {m1 m2 m3} → FinMatrix R m1 m2 → FinMatrix R m2 m3 → FinMatrix R m1 m3
  mulFinMatrix M N i k = ∑ λ j → M i j · N j k

  ∑Exchange : ∀ {m n} → (M : FinMatrix R m n) → ∑ (λ i → ∑ (λ j → M i j)) ≡ ∑ (λ j → ∑ (λ i → M i j))
  ∑Exchange {m = zero}  {n = n}     M = sym (∑0r n)
  ∑Exchange {m = suc m} {n = zero}  M = cong (λ x → 0r + x) (∑0r m) ∙ +Rid 0r
  ∑Exchange {m = suc m} {n = suc n} M =
     let a  = M zero zero
         L  = ∑ λ j → M zero (suc j)
         C  = ∑ λ i → M (suc i) zero
         N  = ∑ λ i → ∑ λ j → M (suc i) (suc j)
         -- N reindexed
         N' = ∑ λ j → ∑ λ i → M (suc i) (suc j)
     in a + L + ∑ (λ i → ∑ (λ j → M (suc i) j)) ≡⟨ (λ k → a + L + ∑Split (λ i → M (suc i) zero) (λ i → ∑ (λ j → M (suc i) (suc j))) k) ⟩
        a + L + (C + N)                         ≡⟨ (λ k → a + L + (C + ∑Exchange (λ i j → M (suc i) (suc j)) k)) ⟩
        a + L + (C + N')                        ≡⟨ sym (+Assoc _ _ _) ⟩
        a + (L + (C + N'))                      ≡⟨ (λ k → a + +Assoc-comm1 L C N' k) ⟩
        a + (C + (L + N'))                      ≡⟨ +Assoc _ _ _ ⟩
        a + C + (L + N')                        ≡⟨ (λ k → a + C + ∑Split (λ j → M zero (suc j)) (λ j → ∑ (λ i → M (suc i) (suc j))) (~ k)) ⟩
        a + C + ∑ (λ j → ∑ (λ i → M i (suc j))) ∎

  mulFinMatrixAssoc : ∀ {m n k l} → (M : FinMatrix R m n) → (N : FinMatrix R n k) → (K : FinMatrix R k l)
                   → mulFinMatrix M (mulFinMatrix N K) ≡ mulFinMatrix (mulFinMatrix M N) K
  mulFinMatrixAssoc M N K = funExt₂ λ i j →
    ∑ (λ k → M i k · ∑ (λ l → N k l · K l j))   ≡⟨ ∑Ext (λ k → ∑Mulrdist (M i k) (λ l → N k l · K l j)) ⟩
    ∑ (λ k → ∑ (λ l → M i k · (N k l · K l j))) ≡⟨ ∑Ext (λ k → ∑Ext (λ l → ·Assoc (M i k) (N k l) (K l j))) ⟩
    ∑ (λ k → ∑ (λ l → M i k · N k l · K l j))   ≡⟨ ∑Exchange (λ k l → M i k · N k l · K l j) ⟩
    ∑ (λ l → ∑ (λ k → M i k · N k l · K l j))   ≡⟨ ∑Ext (λ l → sym (∑Mulldist (K l j) (λ k → M i k · N k l))) ⟩
    ∑ (λ l → ∑ (λ k → M i k · N k l) · K l j)   ∎

  mulFinMatrixr1 : ∀ {m n} → (M : FinMatrix R m n) → mulFinMatrix M oneFinMatrix ≡ M
  mulFinMatrixr1 M = funExt₂ λ i j → ∑Mulr1 _ (M i) j

  mulFinMatrix1r : ∀ {m n} → (M : FinMatrix R m n) → mulFinMatrix oneFinMatrix M ≡ M
  mulFinMatrix1r M = funExt₂ λ i j → ∑Mul1r _ (λ x → M x j) i

  mulFinMatrixrDistrAddFinMatrix : ∀ {n} (M N K : FinMatrix R n n)
                                 → mulFinMatrix M (addFinMatrix N K) ≡ addFinMatrix (mulFinMatrix M N) (mulFinMatrix M K)
  mulFinMatrixrDistrAddFinMatrix M N K = funExt₂ λ i j →
    ∑ (λ k → M i k · (N k j + K k j))                 ≡⟨ ∑Ext (λ k → ·Rdist+ (M i k) (N k j) (K k j)) ⟩
    ∑ (λ k → M i k · N k j + M i k · K k j)           ≡⟨ ∑Split (λ k → M i k · N k j) (λ k → M i k · K k j) ⟩
    ∑ (λ k → M i k · N k j) + ∑ (λ k → M i k · K k j) ∎

  mulFinMatrixlDistrAddFinMatrix : ∀ {n} (M N K : FinMatrix R n n)
                                 → mulFinMatrix (addFinMatrix M N) K ≡ addFinMatrix (mulFinMatrix M K) (mulFinMatrix N K)
  mulFinMatrixlDistrAddFinMatrix M N K = funExt₂ λ i j →
    ∑ (λ k → (M i k + N i k) · K k j)                 ≡⟨ ∑Ext (λ k → ·Ldist+ (M i k) (N i k) (K k j)) ⟩
    ∑ (λ k → M i k · K k j + N i k · K k j)           ≡⟨ ∑Split (λ k → M i k · K k j) (λ k → N i k · K k j) ⟩
    ∑ (λ k → M i k · K k j) + ∑ (λ k → N i k · K k j) ∎

  FinMatrixRing : (n : ℕ) → Ring ℓ
  FinMatrixRing n =
    makeRing {R = FinMatrix R n n} zeroFinMatrix oneFinMatrix addFinMatrix
             mulFinMatrix negFinMatrix isSetFinMatrix addFinMatrixAssoc
             addFinMatrix0r addFinMatrixNegMatrixr addFinMatrixComm
             mulFinMatrixAssoc mulFinMatrixr1 mulFinMatrix1r
             mulFinMatrixrDistrAddFinMatrix mulFinMatrixlDistrAddFinMatrix

-- Generators of product of two ideals

flatten : {n m : ℕ} → FinMatrix A n m → FinVec A (n ·ℕ m)
flatten {n = zero} _ ()
flatten {n = suc n} M = M zero ++Fin flatten (M ∘ suc)

flattenElim : {P : A → Type ℓ'} {n m : ℕ} (M : FinMatrix A n m)
          → (∀ i j → P (M i j))
          → (∀ i → P (flatten M i))
flattenElim {n = zero} M PMHyp ()
flattenElim {n = suc n} {m = zero} M PMHyp ind =
  ⊥.rec (¬Fin0 (transport (λ i → Fin (0≡m·0 n (~ i))) ind))
flattenElim {n = suc n} {m = suc m} M PMHyp zero = PMHyp zero zero
flattenElim {P = P} {n = suc n} {m = suc m} M PMHyp (suc i) =
  ++FinElim {P = P} (M zero ∘ suc) (flatten (M ∘ suc)) (PMHyp zero ∘ suc)
    (flattenElim {P = P} (M ∘ suc) (PMHyp ∘ suc)) i

module ProdFin (R' : CommRing ℓ) where
 private R = fst R'
 open CommRingStr (snd R') renaming ( is-set to isSetR )
 open CommRingTheory R'
 open RingTheory (CommRing→Ring R')
 open KroneckerDelta (CommRing→Ring R')
 open Sum (CommRing→Ring R')

 toMatrix : {n m : ℕ} → FinVec R n → FinVec R m → FinMatrix R n m
 toMatrix V W i j = V i · W j

 _··Fin_ : {n m : ℕ} → FinVec R n → FinVec R m → FinVec R (n ·ℕ m)
 V ··Fin W = flatten (toMatrix V W)

 Length1··Fin : ∀ (x y : R)
              → replicateFinVec 1 (x · y) ≡ (replicateFinVec 1 x) ··Fin (replicateFinVec 1 y)
 Length1··Fin x y = sym (++FinRid (replicateFinVec 1 (x · y)) _)

 ∑Dist··Fin : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
            → (∑ U) · (∑ V) ≡ ∑ (U ··Fin V)
 ∑Dist··Fin {n = zero} U V = 0LeftAnnihilates _
 ∑Dist··Fin {n = suc n} U V =
  (U zero + ∑ (U ∘ suc)) · (∑ V) ≡⟨ ·Ldist+ _ _ _ ⟩
  U zero · (∑ V) + (∑ (U ∘ suc)) · (∑ V) ≡⟨ cong₂ (_+_) (∑Mulrdist _ V) (∑Dist··Fin (U ∘ suc) V) ⟩
  ∑ (λ j → U zero · V j) + ∑ ((U ∘ suc) ··Fin V) ≡⟨ sym (∑Split++ (λ j → U zero · V j) _) ⟩
  ∑ ((λ j → U zero · V j) ++Fin ((U ∘ suc) ··Fin V)) ∎

 ·Dist··Fin : {n m : ℕ} (α U : FinVec R n) (β V : FinVec R m)
            → ∀ j → ((λ i → α i · U i) ··Fin (λ i → β i · V i)) j ≡ (α ··Fin β) j · (U ··Fin V) j
 ·Dist··Fin {n = n} {m = m} α U β V = equivΠ e (equivHelper α U β V ) .fst
                                                λ _ → ·-commAssocSwap _ _ _ _
     where
     e = (FinProdChar.Equiv n m)
     equivHelper : {n m : ℕ} (α U : FinVec R n) (β V : FinVec R m) (a : Fin n × Fin m) →
        (α (fst a) · U (fst a) · (β (snd a) · V (snd a))
       ≡ α (fst a) · β (snd a) · (U (fst a) · V (snd a)))
      ≃ (((λ i → α i · U i) ··Fin (λ i → β i · V i)) (FinProdChar.Equiv n m .fst a)
       ≡ (α ··Fin β) (FinProdChar.Equiv n m .fst a) · (U ··Fin V) (FinProdChar.Equiv n m .fst a))
     equivHelper {n = suc n} {m = suc m} α U β V (zero , zero) = idEquiv _
     equivHelper {n = suc n} {m = suc m} α U β V (zero , suc j) = transport
      (λ 𝕚 → (α zero · U zero · (β (suc j) · V (suc j)) ≡ α zero · β (suc j) · (U zero · V (suc j)))
           ≃ (FinSumChar.++FinInl m (n ·ℕ suc m)
               (λ x → α zero · U zero · (β (suc x) · V (suc x)))
               (flatten (λ x y → α (suc x) · U (suc x) · (β y · V y))) j 𝕚
           ≡ (FinSumChar.++FinInl m (n ·ℕ suc m)
               (λ x → α zero · β (suc x)) (flatten (λ x y → α (suc x) · β y)) j 𝕚)
           · (FinSumChar.++FinInl m (n ·ℕ suc m)
               (λ x → U zero · V (suc x)) (flatten (λ x y → U (suc x) · V y)) j 𝕚)))
      (idEquiv _)
     equivHelper {n = suc n} {m = suc m} α U β V (suc i , j) = transport
      (λ 𝕚 → (α (suc i) · U (suc i) · (β j · V j) ≡ α (suc i) · β j · (U (suc i) · V j))
           ≃ (FinSumChar.++FinInr m (n ·ℕ suc m)
               (λ x → α zero · U zero · (β (suc x) · V (suc x)))
               (flatten (λ x y → α (suc x) · U (suc x) · (β y · V y)))
               (FinProdChar.Equiv n (suc m) .fst (i , j)) 𝕚
           ≡ (FinSumChar.++FinInr m (n ·ℕ suc m)
               (λ x → α zero · β (suc x)) (flatten (λ x y → α (suc x) · β y))
               (FinProdChar.Equiv n (suc m) .fst (i , j)) 𝕚)
           · (FinSumChar.++FinInr m (n ·ℕ suc m)
               (λ x → U zero · V (suc x)) (flatten (λ x y → U (suc x) · V y))
               (FinProdChar.Equiv n (suc m) .fst (i , j)) 𝕚)))
       (equivHelper (α ∘ suc) (U ∘ suc) β V _)

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
-- {-# OPTIONS -v term:30 #-}
-- 2010-10-14
module ProjectionsPreserveGuardednessTrivialExample where

open import Common.Level
open import Common.Coinduction
open import Common.Product

-- Streams

infixr 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

mutual

  repeat : {A : Set}(a : A) → Stream A
  repeat a = a ∷ proj₂ (repeat' a)

  repeat' : {A : Set}(a : A) → A × ∞ (Stream A)
  repeat' a = a , ♯ repeat a

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Testing how the pragmas are saved in the Agda interface files (using
-- the program dump-agdai interface).

-- 13 July 2012. Because for example the pragma BUILTIN is not a
-- PragmaOption it is not saved in iPragmaOptions, i.e.
--
-- iPragmaOptions = []

module NoOptionPragma where

data Bool : Set where
  true false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Level where

open import Agda.Primitive using (Level ; _⊔_ ; Setω) renaming (lzero to 0ℓ ; lsuc to ++_) public

record Lifted ℓ {aℓ} (𝕒 : Set aℓ) : Set (ℓ ⊔ aℓ) where
      constructor lift
      field lower : 𝕒

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
open import Kaleid as K using ()
open import Extract (K.kompile-funp) using (kompile)
open import ReflHelper

open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L using (List; []; _∷_)

open import Data.Fin using (Fin; zero; suc; fromℕ<)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

open import Reflection hiding (_≟_; _>>=_; return)

open import Structures
open import Function

test1-f : ℕ → ℕ
test1-f x = 1 + x

test₁ : kompile test1-f [] [] ≡ ok _
test₁ = refl

test2-f : ℕ → ℕ → ℕ
test2-f (suc x) (suc y) = suc $ test2-f x y
test2-f _ _ = 0

test₂ : kompile test2-f [] [] ≡ ok _
test₂ = refl

test3-f : (a b : ℕ) → a ≡ b → ℕ
test3-f a b _ = a ∸ b

test₃ : kompile test3-f [] [] ≡ ok _
test₃ = refl

test4-f : (x : ℕ) → x ≡ 0 → (y : ℕ) → x ≡ y → ℕ
test4-f x () (suc y) refl
test4-f x x=0 zero x=y = 0

test₄ : kompile test4-f [] [] ≡ ok _
test₄ = refl

-- _>_ is not (yet) supported, so no test₅ for now.
test5-f : (x y : ℕ) → x > y → ℕ
test5-f 0 0 ()
test5-f 0 x _ = x
test5-f (suc x) y _ = x + y

test6-f : (x y : ℕ) → ℕ
test6-f x y with x ≟ y
... | yes pf = 1
... | _ = 2

test₆ = kompile test6-f (quote _≟_ ∷ []) []

test7-f : (n : ℕ) → Fin (suc (n * n))
test7-f n = fromℕ< ≤-refl

test8-f : ℕ → ℕ
test8-f x = let a = x * x + 3 * x + 5 in a + a

test-args : (a b c d : ℕ) → ℕ
test-args a b c d = a + b + c + d

test-args2 : (a b : ℕ) → ℕ
test-args2 a b = test-args a b a b

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
module AnyRelational where
open import Data.Function
open import Data.Unit
open import Data.Empty
open import Data.Bool
open import Data.Nat
open import Data.List hiding (any)
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable renaming (map to dec-map)
open import Relation.Binary.PropositionalEquality

Pred : Set → Set₁
Pred A = A → Set

_∈_ : {A : Set} → A → Pred A → Set
a ∈ P = P a

data Even : ℕ → Set where
  zero : Even 0
  suc : {n : ℕ} → Even n → Even (suc (suc n))

6-Even : 6 ∈ Even
6-Even = suc (suc (suc zero))

data Odd : ℕ → Set where
  zero : Odd 1
  suc : {n : ℕ} → Odd n → Odd (suc (suc n))

5-Odd : 5 ∈ Odd
5-Odd = suc (suc zero)

data Any {A : Set} (P : Pred A) : List A → Set where
  here :  ∀ {x xs} → x ∈ P    → Any P (x ∷ xs)
  there : ∀ {x xs} → Any P xs → Any P (x ∷ xs)

test-any-even : Any Even (3 ∷ 6 ∷ 9 ∷ [])
test-any-even = there (here 6-Even)

test-any-odd : Any Odd (3 ∷ 5 ∷ 10 ∷ [])
test-any-odd = there (here 5-Odd)

U : {A : Set} → Pred A
U _ = ⊤

42-U : 42 ∈ U
42-U = tt

true-U : true ∈ U
true-U = tt

Universal : {A : Set} → Pred A → Set
Universal P = ∀ a → a ∈ P

U-Universal : {A : Set} → Universal {A} U
U-Universal _ = tt

_∪_ : {A : Set} → Pred A → Pred A → Pred A
P ∪ Q = λ a → P a ⊎ Q a

evenOrOdd : Universal (Even ∪ Odd)
evenOrOdd 0 = inj₁ zero
evenOrOdd 1 = inj₂ zero
evenOrOdd (suc n) with evenOrOdd n
... | inj₁ p = inj₂ (evenSucOdd p) where
  evenSucOdd : ∀ {n} → Even n → Odd (suc n)
  evenSucOdd zero = zero
  evenSucOdd (suc n) = suc (evenSucOdd n)
... | inj₂ p = inj₁ (oddSucEven p) where
  oddSucEven : ∀ {n} → Odd n → Even (suc n)
  oddSucEven zero = suc zero
  oddSucEven (suc n) = suc (oddSucEven n)

∁ : {A : Set} → Pred A → Pred A
∁ P = λ a → ¬ (P a)

_⇒_ : {A : Set} → Pred A → Pred A → Set
P ⇒ Q = ∀ {a} → P a → Q a

predOdd : ∀ {n} → Odd (suc (suc n)) → Odd n
predOdd (suc n) = n

even⇒¬odd : Even ⇒ ∁ Odd
even⇒¬odd zero = λ()
even⇒¬odd (suc e) with even⇒¬odd e
even⇒¬odd (suc e) | f = λ o → f (predOdd o)

∅ : {A : Set} → Pred A
∅ _ = ⊥

_∉_ : {A : Set} → A → Pred A → Set
a ∉ P = ¬ (a ∈ P)

42-¬∅ : 42 ∉ ∅
42-¬∅ ()

true-¬∅ : true ∉ ∅
true-¬∅ ()

Empty : {A : Set} → Pred A → Set
Empty P = ∀ a → a ∉ P

∅-Empty : {A : Set} → Empty {A} ∅
∅-Empty _ ()

∁∅-Universal : {A : Set} → Universal {A} (∁ ∅)
∁∅-Universal _ ()

∁U-Empty : {A : Set} → Empty {A} (∁ U)
∁U-Empty _ ∁U = ∁U tt

test-any-6≡ : Any ( _≡_ 6) (3 ∷ 6 ∷ 9 ∷ [])
test-any-6≡ = there (here refl)

find : ∀ {A : Set} {P : Pred A} {as : List A} →
       Any P as → ∃ (λ a → Any (_≡_ a) as × a ∈ P)
find (here p) = _ , (here refl , p)
find (there ps) = Data.Product.map id
                  (Data.Product.map there id)
                  (find ps)

-- test-any-even : Any Even (3 ∷ 6 ∷ 9 ∷ [])
-- test-any-even = there (here (suc (suc (suc zero))))

-- 6-found : proj₁ (find test-any-even) ≡ 6
-- 6-found = refl

-- 6-Even : 6 ∈ Even
-- 6-Even = proj₂ (proj₂ (find test-any-even))

-- test-any-6≡ : Any (_≡_ 6) (3 ∷ 6 ∷ 9 ∷ [])
-- test-any-6≡ = proj₁ (proj₂ (find test-any-even))

tail : ∀ {A x xs} {P : Pred A} → x ∉ P → Any P (x ∷ xs) → Any P xs
tail ¬p (here  p) = ⊥-elim (¬p p)
tail ¬p (there ps) = ps

any : {A : Set} {P : Pred A} →
      (∀ x → Dec (x ∈ P)) → (xs : List A) → Dec (Any P xs)
any f [] = no λ()
any f (x ∷ xs) with f x
any f (x ∷ xs) | yes p = yes (here p)
any f (x ∷ xs) | no ¬p = dec-map (there , tail ¬p) (any f xs)

predEven : ∀ {n} → Even (suc (suc n)) → Even n
predEven (suc n) = n

even¬Consecutive : ∀ {n} → n ∈ Even → suc n ∉ Even
even¬Consecutive zero = λ ()
even¬Consecutive (suc n) with even¬Consecutive n
... | ¬p = λ e → ¬p (predEven e)

postulate
  ¬even¬Consecutive : ∀ {n} → n ∉ Even → suc n ∈ Even

Dec-Even : ∀ n → Dec (n ∈ Even)
Dec-Even zero = yes zero
Dec-Even (suc zero) = no λ()
Dec-Even (suc n) with Dec-Even n
... | yes p = no (even¬Consecutive p)
... | no ¬p = yes (¬even¬Consecutive ¬p)

dec-any-even : Dec (Any Even (3 ∷ 6 ∷ 9 ∷ []))
dec-any-even = any Dec-Even (3 ∷ 6 ∷ 9 ∷ [])


text:
module Abstract where

data Bool : Set where
  true false : Bool

not : Bool → Bool
not true  = false
not false = true

abstract
  Answer : Set
  Answer = Bool

  yes : Answer
  yes = true

  no : Answer
  no = false

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

data Box : Set where
  [_] : Answer → Box

bad-box : Box
bad-box = [ true ]

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Examples.Run where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +)
open import Luau.Value using (nil; number)
open import Luau.Run using (run; return)
open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)

import Agda.Builtin.Equality.Rewrite
{-# REWRITE lookup-next next-emp lookup-next-emp #-}

ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
ex1 = refl

ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
ex2 = refl

ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _)
ex3 = refl


text:
-- Andreas, 2013-05-02 This ain't a bug, it is a feature.
-- {-# OPTIONS -v scope.name:10 #-}
-- {-# OPTIONS -v scope:10 #-}

module Issue836 where

module M where

  record R : Set₁ where
    field
      X : Set

open M using (R)

X : R → Set
X = R.X

-- A glimpse at the scope (showing only concrete names, though):
--   modules
--     * scope Issue836
--       private names   R --> [Issue836.M.R]
--       public  modules M --> [Issue836.M]
--     * scope Issue836.M
--       public  names   R --> [Issue836.M.R]
--               modules R --> [Issue836.M.R]
--     * scope Issue836.M.R
--       public  names   X --> [Issue836.M.R.X]

-- Nisse:
-- The open directive did not mention the /module/ R, so (I think
-- that) the code above should be rejected.

-- Andreas:
-- NO, it is a feature that projections can also be accessed via
-- the record /type/.

-- Ulf:
-- With the fix to 836 using (R) now means using (R; module R).


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

open import Agda.Primitive
open import Prelude
import GSeTT.Typed-Syntax
import Globular-TT.Syntax

{- Type theory for globular sets -}
module Globular-TT.Typed-Syntax {l}
  (index : Set l) (rule : index → GSeTT.Typed-Syntax.Ctx × (Globular-TT.Syntax.Pre-Ty index)) (eqdec-index : eqdec index)  where

  open import Globular-TT.Syntax index
  open import Globular-TT.Rules index rule
  open import Globular-TT.Eqdec-syntax index eqdec-index
  open import Globular-TT.Uniqueness-Derivations index rule eqdec-index

  Ctx : Set (lsuc l)
  Ctx = Σ Pre-Ctx (λ Γ → Γ ⊢C)

  Ty : Ctx → Set (lsuc l)
  Ty (Γ , _) = Σ Pre-Ty (λ A → Γ ⊢T A)

  Tm : ∀ (Γ : Ctx) → Ty Γ → Set (lsuc l)
  Tm (Γ , _) (A , _) = Σ Pre-Tm (λ t → Γ ⊢t t # A)

  Sub : ∀ (Δ : Ctx) (Γ : Ctx) → Set (lsuc l)
  Sub (Δ , _) (Γ , _) = Σ Pre-Sub (λ γ → Δ ⊢S γ > Γ)

  eqC : ∀ (Γ Δ : Ctx) → fst Γ == fst Δ → Γ == Δ
  eqC (Γ , Γ⊢) (.Γ , Γ⊢') idp = Σ= idp (has-all-paths-⊢C _ _)

  eqT : ∀ {Γ} (A B : Ty Γ) → fst A == fst B → A == B
  eqT (A , Γ⊢A) (.A , Γ⊢'A) idp = Σ= idp (has-all-paths-⊢T _ _)

  eqt : ∀ {Γ A} (t u : Tm Γ A) → fst t == fst u → t == u
  eqt (t , Γ⊢t:A) (.t , Γ⊢':A) idp = Σ= idp (has-all-paths-⊢t _ _)

  eqS : ∀ {Γ Δ} (γ δ : Sub Γ Δ) → fst γ == fst δ → γ == δ
  eqS (γ , Γ⊢γ:Δ) (.γ , Γ⊢'γ:Δ) idp = Σ= idp (has-all-paths-⊢S _ _)

  trS : ∀ {Γ Δ Θ : Ctx} → (p : Δ == Θ) → {γ : Sub Γ Δ} → {δ : Sub Γ Θ} → fst γ == fst δ → transport p γ == δ
  trS {Γ} {Δ} {Θ} idp {γ} {δ} x = eqS {Γ} {Θ} γ δ x

  private
    eqdec-typedTy : ∀ Γ → eqdec (Ty Γ)
    eqdec-typedTy Γ (A , Γ⊢A) (B , Γ⊢B) with eqdec-Ty A B
    ... | inl idp = inl (eqT {Γ} (A , Γ⊢A) (B , Γ⊢B) idp)
    ... | inr A≠B = inr λ p → A≠B (fst-is-inj p)

  is-set-Ty : ∀ Γ → is-set (Ty Γ)
  is-set-Ty Γ = eqdec-is-set (eqdec-typedTy Γ)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
{- Comparison view and associated lemmas -}
module TemporalOps.Common.Compare where

open import CategoryTheory.Categories
open import Relation.Binary.PropositionalEquality as ≡
open import Relation.Binary.HeterogeneousEquality as ≅
open import Data.Nat.Properties using (+-identityʳ ; +-assoc ; +-suc)
open import Data.Nat using (ℕ ; zero ; suc ; _+_) public

-- (Very verbose) comparison view
-- Like 'compare', but only distinguishes ≤ or >.
data LeqOrdering : ℕ -> ℕ -> Set where
    snd==[_+_]    : ∀ k l → LeqOrdering k           (k + l)
    fst==suc[_+_] : ∀ k l → LeqOrdering (k + suc l) k

-- Auxiliary function to compareLeq
compareLeq-suc : ∀ n k -> LeqOrdering n k -> LeqOrdering (suc n) (suc k)
compareLeq-suc n .(n + l)     snd==[ .n + l ]    = snd==[ suc n + l ]
compareLeq-suc .(k + suc l) k fst==suc[ .k + l ] = fst==suc[ suc k + l ]

compareLeq : ∀ n k -> LeqOrdering n k
compareLeq zero k          = snd==[ zero + k ]
compareLeq (suc n) zero    = fst==suc[ zero + n ]
compareLeq (suc n) (suc k) = compareLeq-suc n k (compareLeq n k)

-- Lemmas for compareLeq

-- Comparing n and (n + k) always gives snd==[ n + k ]
compare-snd : ∀ (n k : ℕ) -> compareLeq n (n + k) ≡ snd==[ n + k ]
compare-snd zero k = refl
compare-snd (suc n) k rewrite compare-snd n k = refl

-- If n ≤ n + k, then l + n  ≤ (l + n) + k
compare-snd-+ : ∀ (n k l : ℕ) -> compareLeq n (n + k) ≡ snd==[ n + k ]
             -> compareLeq (l + n) ((l + n) + k) ≡ snd==[ (l + n) + k ]
compare-snd-+ n k zero pf = pf
compare-snd-+ zero k (suc l) pf rewrite +-identityʳ l = compare-snd (suc l) k
compare-snd-+ (suc n) k (suc l) pf
    rewrite +-suc l n | compare-snd (l + n) k = refl

-- Heterogeneous version of compare-snd-+ with associativity
compare-snd-+-assoc : ∀ (n k l : ℕ) -> compareLeq n (n + k) ≡ snd==[ n + k ]
                   -> compareLeq (l + n) (l + (n + k)) ≅ snd==[ (l + n) + k ]
compare-snd-+-assoc n k l pf =
    begin
        compareLeq (l + n) (l + (n + k))
    ≅⟨ ≅.cong (λ x → compareLeq (l + n) x) (≡-to-≅ (≡.sym (+-assoc l n k))) ⟩
        compareLeq (l + n) ((l + n) + k)
    ≅⟨ ≡-to-≅ (compare-snd-+ n k l pf) ⟩
        snd==[ (l + n) + k ]
    ∎
    where
    open ≅.≅-Reasoning

-- Comparing (n + suc k and n always gives fst==suc[ n + k ]
compare-fst : ∀ (n k : ℕ) -> compareLeq (n + suc k) n ≡ fst==suc[ n + k ]
compare-fst zero k = refl
compare-fst (suc n) k rewrite compare-fst n k = refl

-- If n + suc k > n, then (l + n) + suc k  > l + n
compare-fst-+ : ∀ (n k l : ℕ) -> compareLeq (n + suc k) n ≡ fst==suc[ n + k ]
             -> compareLeq ((l + n) + suc k) (l + n) ≡ fst==suc[ (l + n) + k ]
compare-fst-+ n k zero pf = pf
compare-fst-+ zero k (suc l) pf rewrite +-identityʳ l = compare-fst (suc l) k
compare-fst-+ (suc n) k (suc l) pf
    rewrite +-suc l n | compare-fst (l + n) k = refl

-- Heterogeneous version of compare-fst-+ with associativity
compare-fst-+-assoc : ∀ (n k l : ℕ) -> compareLeq (n + suc k) n ≡ fst==suc[ n + k ]
                   -> compareLeq (l + (n + suc k)) (l + n) ≅ fst==suc[ (l + n) + k ]
compare-fst-+-assoc n k l pf =
    begin
        compareLeq (l + (n + suc k)) (l + n)
    ≅⟨ ≅.cong (λ x → compareLeq x (l + n)) (≡-to-≅ (≡.sym (+-assoc l n (suc k)))) ⟩
        compareLeq ((l + n) + suc k) (l + n)
    ≅⟨ ≡-to-≅ (compare-fst-+ n k l pf) ⟩
        fst==suc[ (l + n) + k ]
    ∎
    where
    open ≅.≅-Reasoning

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
open import Oscar.Data.Substitunction
open import Oscar.Data.Proposequality
import Oscar.Property.Setoid.Proposextensequality
open import Oscar.Class
import Oscar.Data.Constraint

module Oscar.Class.HasEquivalence.Substitunction where

module _ {𝔭} {𝔓 : Ø 𝔭} where

  open Substitunction 𝔓

  instance

    HasEquivalenceSubstitunction : ∀ {x y} → HasEquivalence (Substitunction x y) _
    HasEquivalenceSubstitunction = ∁ Proposextensequality


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.S2.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

open import Cubical.HITs.S1.Base
open import Cubical.HITs.S2.Base
open import Cubical.HITs.Susp

open import Cubical.Homotopy.Loopspace

S²ToSetElim : ∀ {ℓ} {A : S² → Type ℓ}
           → ((x : S²) → isSet (A x))
           → A base
           → (x : S²) → A x
S²ToSetElim set b base = b
S²ToSetElim set b (surf i j) =
  isOfHLevel→isOfHLevelDep 2 set b b {a0 = refl} {a1 = refl} refl refl surf i j

-- Wedge connectivity lemmas for S² (binary maps 2-groupoids)
wedgeconFunS² : ∀ {ℓ} {P : S² → S² → Type ℓ}
         → ((x y : _) → isOfHLevel 4 (P x y))
         → (l : ((x : S²) → P x base))
         → (r : (x : S²) → P base x)
         → l base ≡ r base
         → (x y : _) → P x y
wedgeconFunS² {P = P} hlev l r p base y = r y
wedgeconFunS² {P = P} hlev l r p (surf i i₁) y = help y i i₁
  where
  help : (y : S²) → SquareP (λ i j → P (surf i j) y)
                     (λ _ → r y) (λ _ → r y)
                     (λ _ → r y) λ _ → r y
  help =
    S²ToSetElim (λ _ → isOfHLevelPathP' 2 (isOfHLevelPathP' 3 (hlev _ _) _ _) _ _)
               λ w j → hcomp (λ k → λ { (j = i0) → p k
                                        ; (j = i1) → p k
                                        ; (w = i0) → p k
                                        ; (w = i1) → p k})
                              (l (surf w j))

wedgeconFunS²Id : ∀ {ℓ} {P : S² → S² → Type ℓ}
         → (h : ((x y : _) → isOfHLevel 4 (P x y)))
         → (l : ((x : S²) → P x base))
         → (r : (x : S²) → P base x)
         → (p : l base ≡ r base)
         → (x : S²) → wedgeconFunS² h l r p x base ≡ l x
wedgeconFunS²Id h l r p base = sym p
wedgeconFunS²Id h l r p (surf i j) k =
  hcomp (λ w → λ {(i = i0) → p (~ k ∧ w)
                 ; (i = i1) → p (~ k ∧ w)
                 ; (j = i0) → p (~ k ∧ w)
                 ; (j = i1) → p (~ k ∧ w)
                 ; (k = i1) → l (surf i j)})
        (l (surf i j))

S¹×S¹→S² : S¹ → S¹ → S²
S¹×S¹→S² base y = base
S¹×S¹→S² (loop i) base = base
S¹×S¹→S² (loop i) (loop j) = surf i j

invS² : S² → S²
invS² base = base
invS² (surf i j) = surf j i

S¹×S¹→S²-anticomm : (x y : S¹) → invS² (S¹×S¹→S² x y) ≡ S¹×S¹→S² y x
S¹×S¹→S²-anticomm base base = refl
S¹×S¹→S²-anticomm base (loop i) = refl
S¹×S¹→S²-anticomm (loop i) base = refl
S¹×S¹→S²-anticomm (loop i) (loop i₁) = refl

toSuspPresInvS² : (x : S²) → toSusp S²∙ (invS² x) ≡ sym (toSusp S²∙ x)
toSuspPresInvS² base =
  rCancel (merid base) ∙∙ refl ∙∙ cong sym (sym (rCancel (merid base)))
toSuspPresInvS² (surf i j) k r =
  hcomp (λ l → λ {(i = i0) → cc l k r
                 ; (i = i1) → cc l k r
                 ; (j = i0) → cc l k r
                 ; (j = i1) → cc l k r
                 ; (k = i0) → l1-fill j i r (~ l)
                 ; (k = i1) → l1-fill i j (~ r) (~ l)
                 ; (r = i0) → north
                 ; (r = i1) → north})
        (l1≡l2 k j i r)
  where
  cc : Cube {A = Susp S²} _ _ _ _ _ _
  cc = doubleCompPath-filler
        (rCancel (merid base)) refl (cong sym (sym (rCancel (merid base))))

  l1-fill : (i j k r : I) → Susp S²
  l1-fill i j k r =
    hfill (λ r →  λ {(i = i0) → rCancel (merid base) r k
                 ; (i = i1) → rCancel (merid base) r k
                 ; (j = i0) → rCancel (merid base) r k
                 ; (j = i1) → rCancel (merid base) r k
                 ; (k = i0) → north
                 ; (k = i1) → north})
          (inS (toSusp S²∙ (surf i j) k))
          r

  l1 : (Ω^ 3) (Susp∙ S²) .fst
  l1 i j k = l1-fill i j k i1

  l2 : (Ω^ 3) (Susp∙ S²) .fst
  l2 i j k = l1 j i (~ k)

  sym≡cong-sym-refl : ∀ {ℓ} {A : Type ℓ} {x : A} → sym≡cong-sym (λ _ _ → x) ≡ refl
  sym≡cong-sym-refl {x = x} = transportRefl (λ _ _ _ → x)

  l1≡l2 : l1 ≡ l2
  l1≡l2 = sym (sym≡flipSquare (λ i j → l1 j i))
        ∙ ((λ _ i j k → l1 j (~ i) k)
        ∙ λ r i j k →
          hcomp (λ l →  λ {(i = i0) → north
                 ; (i = i1) → north
                 ; (j = i0) → sym≡cong-sym-refl {x = north} r (~ l) i k
                 ; (j = i1) → sym≡cong-sym-refl {x = north} r (~ l) i k
                 ; (k = i0) → north
                 ; (k = i1) → north
                 ; (r = i0) → sym≡cong-sym (λ i k → l1 j i k) (~ l) i k
                 ; (r = i1) → l2 i j k})
                (l2 i j k))

S¹×S¹→S²-sym : (x y : S¹) → toSusp S²∙ (S¹×S¹→S² x y) ≡ sym (toSusp S²∙ (S¹×S¹→S² y x))
S¹×S¹→S²-sym x y =
  cong sym (sym (toSuspPresInvS²  (S¹×S¹→S² x y)))
  ∙ cong (sym ∘ toSusp S²∙) (S¹×S¹→S²-anticomm x y)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

-- properties of the product _※_ of Functors (so probably should be renamed?)

open import Level
open import Data.Product

open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idNI)
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Category.Product
open import Categories.Morphism
import Categories.Morphism.Reasoning as MR

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

-- variables don't work quite right, use anonymous module instead
module _ {A : Category o ℓ e} {B : Category o′ ℓ′ e′} {C : Category o″ ℓ″ e″}
         {i : Functor C A} {j : Functor C B} where

  project₁ : πˡ ∘F (i ※ j) ≃ i
  project₁ = record
    { F⇒G = ntHelper record { η = λ _ → id ; commute = λ _ → id-comm-sym }
    ; F⇐G = ntHelper record { η = λ _ → id ; commute = λ _ → id-comm-sym }
    ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ }
    }
    where open Category A; open MR.Basic A

  project₂ : πʳ ∘F (i ※ j) ≃ j
  project₂ = record
    { F⇒G = ntHelper record { η = λ _ → id ; commute = λ _ → id-comm-sym }
    ; F⇐G = ntHelper record { η = λ _ → id ; commute = λ _ → id-comm-sym }
    ; iso = λ X → record { isoˡ = identityˡ ; isoʳ = identityʳ }
    }
    where open Category B; open MR.Basic B

  unique : {h : Functor C (Product A B)} →
        πˡ ∘F h ≃ i → πʳ ∘F h ≃ j → (i ※ j) ≃ h
  unique πˡ→i πʳ→j = record
    { F⇒G = ntHelper record
      { η       = < L⇐.η , R⇐.η >
      ; commute = < L⇐.commute , R⇐.commute >
      }
    ; F⇐G = ntHelper record
      { η       = < L⇒.η , R⇒.η >
      ; commute = < L⇒.commute , R⇒.commute >
      }
    ; iso = λ X → let L = iso πˡ→i X
                      R = iso πʳ→j X in record
      { isoˡ = isoʳ L , isoʳ R
      ; isoʳ = isoˡ L , isoˡ R
      }
    }
    where
      open NaturalIsomorphism
      module L⇐ = NaturalTransformation (F⇐G πˡ→i)
      module R⇐ = NaturalTransformation (F⇐G πʳ→j)
      module L⇒ = NaturalTransformation (F⇒G πˡ→i)
      module R⇒ = NaturalTransformation (F⇒G πʳ→j)
      open Iso

-- further properties of products
module _ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) where

  private
    C×D : Category _ _ _
    C×D = Product C D
    module C×D = Category C×D
    module C = Category C
    module D = Category D

  -- TODO: write an "essentially-equal" combinator for cases such as these?
  πˡ※πʳ≃id : (πˡ ※ πʳ) ≃ idF {C = C×D}
  πˡ※πʳ≃id = record
    { F⇒G = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
    ; F⇐G = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
    ; iso = λ X → record
      { isoˡ = C.identityˡ , D.identityˡ
      ; isoʳ = C.identityʳ , D.identityʳ
      }
    }

  ※-distrib : {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ : Level} {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂}
    → (F : Functor B C) → (G : Functor B D) → (H : Functor A B)
    → ((F ∘F H) ※ (G ∘F H)) ≃ ((F ※ G) ∘F H)
  ※-distrib F G H = record
    { F⇒G = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
    ; F⇐G = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
    ; iso = λ X → record
      { isoˡ = C.identityˡ , D.identityˡ
      ; isoʳ = C.identityʳ , D.identityʳ
      }
    }

  ※-distrib₂ : {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ : Level} {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂}
    → (F : Functor B C) → (G : Functor B D)
    → ((F ∘F πˡ) ※ (G ∘F πʳ)) ≃ (F ⁂ G)
  ※-distrib₂ F G = record
    { F⇒G = ntHelper record { η = λ X → C.id , D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
    ; F⇐G = ntHelper record { η = λ X → C.id , D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
    ; iso = λ X → record { isoˡ = C.identityˡ , D.identityʳ  ; isoʳ = C.identityʳ , D.identityʳ }
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Trans where

open import Prelude

Rel : Set -> Set1
Rel A = A -> A -> Set

data [_]* {A : Set}(R : Rel A)(x : A) : A -> Set where
  ref : [ R ]* x x
  _▹_ : {y z : A} -> R x y -> [ R ]* y z -> [ R ]* x z

infixr 40 _▹_ _▹◃_

length : {A : Set}{R : Rel A}{x y : A} -> [ R ]* x y -> Nat
length ref      = zero
length (x ▹ xs) = suc (length xs)

_=[_]=>_ : {A B : Set}(R : Rel A)(i : A -> B)(S : Rel B) -> Set
R =[ i ]=> S = forall {x y} -> R x y -> S (i x) (i y)

map : {A B : Set}{R : Rel A}{S : Rel B}(i : A -> B) ->
      (R =[ i ]=> S) ->
      {x y : A} -> [ R ]* x y -> [ S ]* (i x) (i y)
map i f ref      = ref
map i f (x ▹ xs) = f x ▹ map i f xs

lem-length-map :
      {A B : Set}{R : Rel A}{S : Rel B}(i : A -> B)
      (f : R =[ i ]=> S){x y : A}(xs : [ R ]* x y) ->
      length xs ≡ length (map {S = S} i f xs)
lem-length-map i f ref      = refl
lem-length-map i f (x ▹ xs) = cong suc (lem-length-map i f xs)

_▹◃_ : {A : Set}{R : Rel A}{x y z : A} ->
       [ R ]* x y -> [ R ]* y z -> [ R ]* x z
ref      ▹◃ ys = ys
(x ▹ xs) ▹◃ ys = x ▹ (xs ▹◃ ys)

lem-length▹◃ : {A : Set}{R : Rel A}{x y z : A}
               (r₁ : [ R ]* x y)(r₂ : [ R ]* y z) ->
               length r₁ + length r₂ ≡ length (r₁ ▹◃ r₂)
lem-length▹◃ ref      ys = refl
lem-length▹◃ (x ▹ xs) ys = cong suc (lem-length▹◃ xs ys)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Coirc.Parser where
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Char
open import Data.String
open import Data.Maybe
open import Data.List hiding (_++_)
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Coirc
open import Coirc.Format

readTo-! : List Char → Maybe (String × List Char)
readTo-! [] = nothing
readTo-! ('!' ∷ xs) = just ("" , '!' ∷ xs)
readTo-! (x ∷ xs) with readTo-! xs
... | nothing = nothing
... | just (a , ys) = just ( fromList [ x ] ++ a  , ys )

readTo-sp : List Char → Maybe (String × List Char)
readTo-sp [] = nothing
readTo-sp (' ' ∷ xs) = just ("" , ' ' ∷ xs)
readTo-sp (x ∷ xs) with readTo-sp xs
... | nothing = nothing
... | just (a , ys) = just ( fromList [ x ] ++ a  , ys )

readTo-crlf : List Char → Maybe (String × List Char)
readTo-crlf [] = nothing
readTo-crlf ('\r' ∷ '\n' ∷ xs) = just ("" , '\r' ∷ '\n' ∷ xs)
readTo-crlf (x ∷ xs) with readTo-crlf xs
... | nothing = nothing
... | just (a , ys) = just ( fromList (x ∷ []) ++ a  , ys )

read : (u : U) → List Char → Maybe (El u × List Char)

read CHAR (x ∷ xs) = just (x , xs)

read (DAR n) (x ∷ xs) with Data.Nat._≟_ n (toNat x)
... | no _  = nothing
... | yes p rewrite p = just (dar x , xs)

read (DAR-RANGE n m) (x ∷ xs) with Data.Bool._≟_ true (within? x n m)
... | no _ = nothing
... | yes p rewrite p = just (dar x , xs)

read `*! xs = readTo-! xs
read `*sp xs = readTo-sp xs
read `*crlf xs = readTo-crlf xs

read _ [] = nothing

parse : (f : Format) → List Char → Maybe (⟦ f ⟧ × List Char)
parse Fail _ = nothing
parse End xs = just (tt , xs)
parse (As val) xs = just (val , xs)
parse (Base u) xs = read u xs
parse (Skip f₁ f₂) xs with parse f₁ xs
... | nothing = nothing
... | just (_ , ys) = parse f₂ ys
parse (Or f₁ f₂) xs with parse f₁ xs
... | just (a , ys) = just (inj₁ a , ys)
... | nothing with parse f₂ xs
... | just (a , ys) = just (inj₂ a , ys)
... | nothing = nothing
parse (And f₁ f₂) xs with parse f₁ xs
... | nothing = nothing
... | just (a , ys) with parse f₂ ys
... | nothing = nothing
... | just (b , zs) = just ((a , b) , zs)
parse (Use f₁ f₂) xs with parse f₁ xs
... | nothing = nothing
... | just (a , ys) with parse (f₂ a) ys
... | nothing = nothing
... | just (b , zs) = just ((a , b) , zs)

parse-Event : List Char → Maybe Event
parse-Event xs with parse Notice xs
... | just (x , _) = just x
... | nothing with parse NumericReply xs
... | just (x , _) = just x
... | nothing with parse Mode xs
... | just (x , _) = just x
... | nothing with parse Ping xs
... | just (x , _) = just x
... | nothing with parse Privmsg xs
... | just ((_ , _ , x) , _) = just x
... | nothing = nothing

private
  test : Event → String → Set
  test e s = just e ≡ parse-Event (toList (s ++ "\r\n"))

  test-Notice : test notice
    ":verne.freenode.net NOTICE * :*** Looking up your hostname..."
  test-Notice = refl

  test-NumericReply : test numeric
    ":verne.freenode.net 001 foobot-name :Welcome to the freenode Internet Relay Chat Network coalgbot"
  test-NumericReply = refl

  test-Mode : test mode
    ":coalgbot MODE coalgbot :+i"
  test-Mode = refl

  test-Ping : test ping
   "PING :verne.freenode.net"
  test-Ping = refl

  test-Privmsg : test (privmsg "amiller" "PING 3073265598")
    ":amiller!debian-tor@gateway/tor-sasl/socrates1024 PRIVMSG coalgbot :PING 3073265598"
  test-Privmsg = refl

max_stars_repo_name: larrytheliquid/coirc

max_issues_repo_name: larrytheliquid/coirc

max_forks_repo_name: larrytheliquid/coirc


text:
postulate A : Set

record R : Set where
  constructor r
  field f : A

test : R → R
test x = let r a = x
             foo : R → A
             foo x = let r a = x in a
         in r (foo (r a))


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

module Dodo.Unary.Dec where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Relation.Nullary using (Dec)
open import Relation.Unary using (Pred)

DecPred : {a ℓ : Level} {A : Set a}
  → Pred A ℓ → Set (a ⊔ ℓ)
DecPred P = ∀ x → Dec (P x)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Closures of a unary relation with respect to a strict partial order
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Unary.Closure.StrictPartialOrder
       {a r e} (P : StrictPartialOrder a e r) where

open StrictPartialOrder P renaming (_<_ to _∼_)
open import Relation.Unary using (Pred)

-- Specialising the results proven generically in `Base`.
import Relation.Unary.Closure.Base _∼_ as Base
open Base public using (□; map; Closed)

module _ {t} {T : Pred Carrier t} where

  reindex : ∀ {x y} → x ∼ y → □ T x → □ T y
  reindex = Base.reindex trans

  duplicate : ∀ {x} → □ T x → □ (□ T) x
  duplicate = Base.duplicate trans

□-closed : ∀ {t} {T : Pred Carrier t} → Closed (□ T)
□-closed = Base.□-closed trans


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Algebra.Group.Base
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

-- The following definition of GroupHom and GroupEquiv are level-wise heterogeneous.
-- This allows for example to deduce that G ≡ F from a chain of isomorphisms
-- G ≃ H ≃ F, even if H does not lie in the same level as G and F.

isGroupHom : (G : Group {ℓ}) (H : Group {ℓ'}) (f : ⟨ G ⟩ → ⟨ H ⟩) → Type _
isGroupHom G H f = (x y : ⟨ G ⟩) → f (x G.+ y) ≡ (f x H.+ f y) where
  module G = GroupStr (snd G)
  module H = GroupStr (snd H)

record GroupHom (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor grouphom

  field
    fun : ⟨ G ⟩ → ⟨ H ⟩
    isHom : isGroupHom G H fun

record GroupEquiv (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor groupequiv

  field
    eq : ⟨ G ⟩ ≃ ⟨ H ⟩
    isHom : isGroupHom G H (equivFun eq)

  hom : GroupHom G H
  hom = grouphom (equivFun eq) isHom

open GroupHom
open GroupStr

×hom : {A : Group {ℓ}} {B : Group {ℓ'}} {C : Group {ℓ''}} {D : Group {ℓ'''}}
    → GroupHom A C → GroupHom B D → GroupHom (dirProd A B) (dirProd C D)
fun (×hom mf1 mf2) = map-× (fun mf1) (fun mf2)
isHom (×hom mf1 mf2) a b = ≡-× (isHom mf1 _ _) (isHom mf2 _ _)

isInIm : (G : Group {ℓ}) (H : Group {ℓ'}) → GroupHom G H → ⟨ H ⟩ → Type (ℓ-max ℓ ℓ')
isInIm G H ϕ h = ∃[ g ∈ ⟨ G ⟩ ] ϕ .fun g ≡ h

isInKer : (G : Group {ℓ}) (H : Group {ℓ'}) → GroupHom G H → ⟨ G ⟩ → Type ℓ'
isInKer G H ϕ g = ϕ .fun g ≡ 0g (snd H)

isSurjective : (G : Group {ℓ}) (H : Group {ℓ'}) → GroupHom G H → Type (ℓ-max ℓ ℓ')
isSurjective G H ϕ = (x : ⟨ H ⟩) → isInIm G H ϕ x

isInjective : (G : Group {ℓ}) (H : Group {ℓ'}) → GroupHom G H → Type (ℓ-max ℓ ℓ')
isInjective G H ϕ = (x : ⟨ G ⟩) → isInKer G H ϕ x → x ≡ 0g (snd G)

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module combinators where

open import bool
open import bool-thms2
import closures
open import eq
open import list
open import list-thms
open import nat
open import nat-thms
open import product
open import product-thms
open import sum
open import string
open import termination

data comb : Set where
  S : comb
  K : comb
  app : comb → comb → comb

size : comb → ℕ
size S = 1
size K = 1
size (app a b) = suc (size a + size b)

data _↝_ : comb → comb → Set where
  ↝K : (a b : comb) → (app (app K a) b) ↝ a
  ↝S : (a b c : comb) → (app (app (app S a) b) c) ↝ (app (app a c) (app b c))
  ↝Cong1 : {a a' : comb} (b : comb) → a ↝ a' → (app a b) ↝ (app a' b)
  ↝Cong2 : (a : comb) {b b' : comb} → b ↝ b' → (app a b) ↝ (app a b')

Sfree : comb → 𝔹
Sfree S = ff
Sfree K = tt
Sfree (app a b) = Sfree a && Sfree b

Sfree-↝-size> : ∀{a b : comb} → Sfree a ≡ tt → a ↝ b → size a > size b ≡ tt
Sfree-↝-size> p (↝K a b) = ≤<-trans {size a} (≤+1 (size a) (size b))
                             (<+2 {size a + size b} {2})
Sfree-↝-size> () (↝S a b c)
Sfree-↝-size> p (↝Cong1{a}{a'} b u) with &&-elim{Sfree a} p
Sfree-↝-size> p (↝Cong1{a}{a'} b u) | p1 , _ = <+mono2 {size a'} (Sfree-↝-size> p1 u)
Sfree-↝-size> p (↝Cong2 a u) with &&-elim{Sfree a} p
Sfree-↝-size> p (↝Cong2 a u) | _ , p2 = <+mono1{size a} (Sfree-↝-size> p2 u)

↝-preserves-Sfree : ∀{a b : comb} → Sfree a ≡ tt → a ↝ b → Sfree b ≡ tt
↝-preserves-Sfree p (↝K a b) = fst (&&-elim p)
↝-preserves-Sfree () (↝S a b c)
↝-preserves-Sfree p (↝Cong1 b u) with &&-elim p
↝-preserves-Sfree p (↝Cong1 b u) | p1 , p2 = &&-intro (↝-preserves-Sfree p1 u) p2
↝-preserves-Sfree p (↝Cong2 a u) with &&-elim{Sfree a} p
↝-preserves-Sfree p (↝Cong2 a u) | p1 , p2 = &&-intro p1 (↝-preserves-Sfree p2 u)

Sfree-comb : Set
Sfree-comb = Σ comb (λ a → Sfree a ≡ tt)

↝-Sfree-comb : Sfree-comb → Sfree-comb → Set
↝-Sfree-comb (a , _) (b , _) = a ↝ b

size-Sfree-comb : Sfree-comb → ℕ
size-Sfree-comb (a , _) = size a

decrease-size : ∀ {x y : Sfree-comb} → ↝-Sfree-comb x y → size-Sfree-comb x > size-Sfree-comb y ≡ tt
decrease-size{a , u}{b , _} p = Sfree-↝-size> u p

open measure{A = Sfree-comb} ↝-Sfree-comb (λ x y → x > y ≡ tt) size-Sfree-comb decrease-size

measure-decreases : ∀(a : Sfree-comb) → ↓ ↝-Sfree-comb a
measure-decreases a = measure-↓ (↓-> (size-Sfree-comb a))

Sfree-terminatesh : ∀{a : comb}{p : Sfree a ≡ tt} → ↓ ↝-Sfree-comb (a , p) →  ↓ _↝_ a
Sfree-terminatesh{a}{p} (pf↓ f) = pf↓ h
  where h : {y : comb} → a ↝ y → ↓ _↝_ y
        h{y} u = Sfree-terminatesh (f {y , ↝-preserves-Sfree p u} u)

Sfree-terminates : ∀(a : comb) → Sfree a ≡ tt → ↓ _↝_ a
Sfree-terminates a p = Sfree-terminatesh (measure-decreases (a , p))

data varcomb : Set where
  S : varcomb
  K : varcomb
  app : varcomb → varcomb → varcomb
  var : (s : string) → varcomb

λ* : (s : string) → varcomb → varcomb
λ* s S = app K S
λ* s K = app K K
λ* s (app c1 c2) = app (app S (λ* s c1)) (λ* s c2)
λ* s (var s') = if (s =string s') then (app (app S K) K) else (app K (var s'))

subst : varcomb → string → varcomb → varcomb
subst c s S = S
subst c s K = K
subst c s (app c1 c2) = app (subst c s c1) (subst c s c2)
subst c s (var s') = if (s =string s') then c else var s'

data _↝vc_ : varcomb → varcomb → Set where
  ↝K : (a b : varcomb) → (app (app K a) b) ↝vc a
  ↝S : (a b c : varcomb) → (app (app (app S a) b) c) ↝vc (app (app a c) (app b c))
  ↝Cong1 : {a a' : varcomb} (b : varcomb) → a ↝vc a' → (app a b) ↝vc (app a' b)
  ↝Cong2 : (a : varcomb) {b b' : varcomb} → b ↝vc b' → (app a b) ↝vc (app a b')

-- open closures.basics _↝vc_

-- _↝vc+_ : varcomb → varcomb → Set
-- _↝vc+_ = tc

-- id↝ : ∀ (a : varcomb) → app (app (app S K) K) a ↝vc+ a
-- id↝ a = (tc-trans (tc-step (↝S K K a)) (tc-step (↝K a (app K a))))

-- trans-Cong1 : ∀{a a' : varcomb} (b : varcomb) → a ↝vc+ a' → (app a b) ↝vc+ (app a' b)
-- trans-Cong1 b (tc-trans d1 d2) = (tc-trans (trans-Cong1 b d1) (trans-Cong1 b d2))
-- trans-Cong1 b (tc-step d) = tc-step (↝Cong1 b d)

-- trans-Cong2 : ∀(a : varcomb) {b b' : varcomb} → b ↝vc+ b' → (app a b) ↝vc+ (app a b')
-- trans-Cong2 a (tc-trans d1 d2) = (tc-trans (trans-Cong2 a d1) (trans-Cong2 a d2))
-- trans-Cong2 a (tc-step d) = tc-step (↝Cong2 a d)

-- contains-var : string → varcomb → 𝔹
-- contains-var s S = ff
-- contains-var s K = ff
-- contains-var s (app c1 c2) = contains-var s c1 || contains-var s c2
-- contains-var s (var s') = s =string s'

-- λ*-binds : ∀(s : string)(v : varcomb) → contains-var s (λ* s v) ≡ ff
-- λ*-binds s S = refl
-- λ*-binds s K = refl
-- λ*-binds s (app c1 c2) rewrite λ*-binds s c1 | λ*-binds s c2 = refl
-- λ*-binds s (var s') with keep (s =string s')
-- λ*-binds s (var s') | tt , p rewrite p = refl
-- λ*-binds s (var s') | ff , p rewrite p = p

-- λ*-↝ : ∀ (v1 v2 : varcomb)(s : string) → (app (λ* s v1) v2) ↝vc+ (subst v2 s v1)
-- λ*-↝ S v2 s = tc-step (↝K S v2)
-- λ*-↝ K v2 s = tc-step (↝K K v2)
-- λ*-↝ (app c1 c2) v2 s =
--   (tc-trans (tc-step (↝S (λ* s c1) (λ* s c2) v2))
--   (tc-trans (trans-Cong1 (app (λ* s c2) v2) (λ*-↝ c1 v2 s))
--     (trans-Cong2 (subst v2 s c1) (λ*-↝ c2 v2 s))))
-- λ*-↝ (var s') v2 s with s =string s'
-- λ*-↝ (var s') v2 s | tt = id↝ v2
-- λ*-↝ (var s') v2 s | ff = tc-step (↝K (var s') v2)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a strict partial
-- order.
------------------------------------------------------------------------

-- Example uses:
--
--    u≤x : u ≤ x
--    u≤x = begin
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  <⟨ w≤x ⟩
--      x  ∎
--
--    u<x : u < x
--    u<x = begin-strict
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  <⟨ w≤x ⟩
--      x  ∎
--
--    u<e : u < e
--    u<e = begin-strict
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  <⟨ w<x ⟩
--      x  ≤⟨ x≤y ⟩
--      y  <⟨ y<z ⟩
--      z  ≡˘⟨ d≡z ⟩
--      d  ≈˘⟨ e≈d ⟩
--      e  ∎
--
--    u≈w : u ≈ w
--    u≈w = begin-equality
--      u  ≈⟨ u≈v ⟩
--      v  ≡⟨ v≡w ⟩
--      w  ∎

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

open import Relation.Binary

module Relation.Binary.Reasoning.StrictPartialOrder
  {p₁ p₂ p₃} (S : StrictPartialOrder p₁ p₂ p₃) where

open StrictPartialOrder S
import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as NonStrict

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Relation.Binary.Reasoning.Base.Triple
  (NonStrict.isPreorder₂ isStrictPartialOrder)
  trans
  <-resp-≈
  NonStrict.<⇒≤
  (NonStrict.<-≤-trans trans <-respʳ-≈)
  public


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

module Type.Cubical.Path where

open import Type
open import Type.Cubical

postulate PathP : ∀{ℓ}(P : Interval → Type{ℓ}) → P(Interval.𝟎) → P(Interval.𝟏) → Type{ℓ}
{-# BUILTIN PATHP PathP #-}

-- The type of paths.
-- Can be seen as a path between two points in the space P.
-- (A continuous function from the closed unit interval to the space).
Path : ∀{ℓ}{P : Type{ℓ}} → P → P → Type{ℓ}
Path {P = P} = PathP(\i → P)
{-# BUILTIN PATH Path #-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Monoidal.Core using (Monoidal)

-- The "four middle interchange" for monoidal categories.
--
-- Aka the "interchange law" or "exchange law" (though those terms are
-- more comonly used in the more general context of composition in
-- 2-categories).

module Categories.Category.Monoidal.Interchange
  {o ℓ e} {C : Category o ℓ e} where

open import Level using (_⊔_)
open import Data.Product using (_,_)

import Categories.Category.Monoidal.Construction.Product as MonoidalProduct
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Braided.Properties
  using (braiding-coherence; inv-Braided; inv-braiding-coherence)
open import Categories.Category.Monoidal.Properties using (module Kelly's)
import Categories.Category.Monoidal.Reasoning as MonoidalReasoning
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
import Categories.Category.Monoidal.Utilities as MonoidalUtilities
open import Categories.Category.Product using (_⁂_; assocˡ)
open import Categories.Functor using (_∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (_≃_; niHelper)
open import Categories.Morphism C using (_≅_; module ≅)
open import Categories.Morphism.IsoEquiv C using (module _≃_)
open import Categories.Morphism.Reasoning C

private module C = Category C
open C
open Commutation C

private
  variable
    W W₁ W₂ X X₁ X₂ Y Y₁ Y₂ Z Z₁ Z₂ : Obj
    f g h i : X ⇒ Y

-- An abstract definition of an interchange map with the minimal set
-- of coherence laws required to make the tensor product ⊗ of C a
-- monoidal functor.  (See also Categories.Functor.Monoidal.Tensor.)

record HasInterchange (M : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where
  open Monoidal M
  open MonoidalUtilities.Shorthands M

  -- The "four middle interchange" for tensor products.

  field swapInner : ∀ {W X Y Z} → (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)

  module swapInner {W X Y Z} = _≅_ (swapInner {W} {X} {Y} {Z})
  private
    i⇒ = swapInner.from
    i⇐ = swapInner.to

  -- Naturality and coherence laws of the interchange.

  field

    natural : i⇒ ∘ (f ⊗₁ g) ⊗₁ (h ⊗₁ i) ≈ (f ⊗₁ h) ⊗₁ (g ⊗₁ i) ∘ i⇒

    assoc : [ ((X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⇒
              (X₁ ⊗₀ (Y₁ ⊗₀ Z₁)) ⊗₀ (X₂ ⊗₀ (Y₂ ⊗₀ Z₂)) ]⟨
              i⇒ ⊗₁ id   ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⟩
              i⇒         ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ Z₁) ⊗₀ ((X₂ ⊗₀ Y₂) ⊗₀ Z₂) ⟩
              α⇒ ⊗₁ α⇒
            ≈ α⇒         ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Y₂) ⊗₀ (Z₁ ⊗₀ Z₂)) ⟩
              id ⊗₁ i⇒   ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Z₁) ⊗₀ (Y₂ ⊗₀ Z₂)) ⟩
              i⇒
            ⟩

    unitˡ : [ unit ⊗₀ (X ⊗₀ Y) ⇒ (X ⊗₀ Y) ]⟨
              λ⇐ ⊗₁ id   ⇒⟨ (unit ⊗₀ unit) ⊗₀ (X ⊗₀ Y) ⟩
              i⇒         ⇒⟨ (unit ⊗₀ X) ⊗₀ (unit ⊗₀ Y) ⟩
              λ⇒ ⊗₁ λ⇒
            ≈ λ⇒
            ⟩

    unitʳ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ (X ⊗₀ Y) ]⟨
              id ⊗₁ λ⇐   ⇒⟨ (X ⊗₀ Y) ⊗₀ (unit ⊗₀ unit) ⟩
              i⇒         ⇒⟨ (X ⊗₀ unit) ⊗₀ (Y ⊗₀ unit) ⟩
              ρ⇒ ⊗₁ ρ⇒
            ≈ ρ⇒
            ⟩

  -- The interchange is a natural isomorphism.

  naturalIso : ⊗ ∘F (⊗ ⁂ ⊗) ≃ ⊗ ∘F MonoidalProduct.⊗ M M
  naturalIso = niHelper (record
    { η       = λ _ → i⇒
    ; η⁻¹     = λ _ → i⇐
    ; commute = λ _ → natural
    ; iso     = λ _ → swapInner.iso
    })

-- Shorthands for composing and inverting isomorphisms.

open ≅ using () renaming (refl to idᵢ; sym to _⁻¹)
private
  infixr 9 _∘ᵢ_
  _∘ᵢ_ = λ {X Y Z} f g → ≅.trans {X} {Y} {Z} g f

-- Braided monoidal categories have an interchange map.

module BraidedInterchange {M : Monoidal C} (B : Braided M) where
  open MonoidalReasoning M
  open MonoidalUtilities M
  open Braided B renaming (associator to α)
  open Shorthands

  -- Shorthands for braiding.

  private
    σ : X ⊗₀ Y ≅ Y ⊗₀ X
    σ = braiding.FX≅GX
    module σ  {X Y} = _≅_ (σ {X} {Y})
    σ⇒ = σ.from
    σ⇐ = σ.to

  -- The "four middle interchange" for braided tensor products.

  swapInner : (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)
  swapInner = α ⁻¹ ∘ᵢ idᵢ ⊗ᵢ (α ∘ᵢ σ ⊗ᵢ idᵢ ∘ᵢ α ⁻¹) ∘ᵢ α

  module swapInner {W X Y Z} = _≅_ (swapInner {W} {X} {Y} {Z})
  private
    i⇒ = swapInner.from
    i⇐ = swapInner.to

  -- The interchange is a natural isomorphism.

  swapInner-natural : i⇒ ∘ (f ⊗₁ g) ⊗₁ (h ⊗₁ i) ≈ (f ⊗₁ h) ⊗₁ (g ⊗₁ i) ∘ i⇒
  swapInner-natural {f = f} {g = g} {h = h} {i = i} = begin
      (α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘ (f ⊗₁ g) ⊗₁ (h ⊗₁ i)
    ≈⟨ pullʳ (pullʳ assoc-commute-from) ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ f ⊗₁ g ⊗₁ (h ⊗₁ i) ∘ α⇒
    ≈⟨ refl⟩∘⟨ extendʳ (parallel id-comm-sym (begin
          (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ g ⊗₁ (h ⊗₁ i)
        ≈⟨ pullʳ (pullʳ assoc-commute-to) ⟩
          α⇒ ∘ σ⇒ ⊗₁ id ∘ (g ⊗₁ h) ⊗₁ i ∘ α⇐
        ≈⟨ refl⟩∘⟨ extendʳ (parallel (braiding.⇒.commute _) id-comm-sym) ⟩
          α⇒ ∘ (h ⊗₁ g) ⊗₁ i ∘ σ⇒ ⊗₁ id ∘ α⇐
        ≈⟨ extendʳ assoc-commute-from ⟩
          h ⊗₁ (g ⊗₁ i) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐
        ∎)) ⟩
      α⇐ ∘ f ⊗₁ h ⊗₁ (g ⊗₁ i) ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ extendʳ assoc-commute-to ⟩
      (f ⊗₁ h) ⊗₁ (g ⊗₁ i) ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ∎

  swapInner-naturalIsomorphism : ⊗ ∘F (⊗ ⁂ ⊗) ≃ ⊗ ∘F MonoidalProduct.⊗ M M
  swapInner-naturalIsomorphism = niHelper (record
    { η       = λ _ → i⇒
    ; η⁻¹     = λ _ → i⇐
    ; commute = λ _ → swapInner-natural
    ; iso     = λ _ → swapInner.iso
    })

  -- Another version of the interchange that associates differently.
  --
  -- Why are there two versions and what's the difference? The domain
  -- (X₁ ⊗ X₂) ⊗₀ (Y₁ ⊗ Y₂) and codomain (X₁ ⊗ Y₁) ⊗₀ (X₁ ⊗ Y₂) of the
  -- interchange map are perfectly symmetric/balanced. But in order to
  -- apply the braiding to the middle X₂ and Y₁, we need to
  -- re-associate and that breaks the symmetry. We must first
  -- re-associate the whole expression in one direction and then the
  -- larger subterm in the other. This can be done in two ways,
  -- associate to the right first, then to the left, resulting in X₁ ⊗
  -- ((Y₂ ⊗₀ X₁) ⊗ Y₂), or vice versa, resulting in (X₁ ⊗ (Y₂ ⊗₀ X₁))
  -- ⊗ Y₂. The choice is arbitrary and results in two distinct
  -- interchange maps that behave the same way (as witnessed by
  -- swapInner-coherent below).
  --
  -- Why define both? Because the proofs of some coherence laws become
  -- easier when the core of the expression is associated in one
  -- direction vs. the other. For example swapInner-unitˡ is easier to
  -- prove for the second definition, while swapInner-unitʳ is easier
  -- to prove for the first; swapInner-assoc uses both.

  swapInner′ : (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)
  swapInner′ = α ∘ᵢ (α ⁻¹ ∘ᵢ idᵢ ⊗ᵢ σ ∘ᵢ α) ⊗ᵢ idᵢ ∘ᵢ α ⁻¹

  module swapInner′ {W X Y Z} = _≅_ (swapInner′ {W} {X} {Y} {Z})
  private
    j⇒ = swapInner′.from
    j⇐ = swapInner′.to

  -- Derived coherence laws.

  swapInner-coherent : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒ (X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂) ]⟨
                         i⇒
                       ≈ j⇒
                       ⟩
  swapInner-coherent = begin
      α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      α⇐ ∘ id ⊗₁ α⇒ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      α⇐ ∘ id ⊗₁ α⇒ ∘ id ⊗₁ (σ⇒ ⊗₁ id) ∘ id ⊗₁ α⇐ ∘ α⇒
    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ conjugate-from α (idᵢ ⊗ᵢ α) (⟺ pentagon) ⟩
      α⇐ ∘ id ⊗₁ α⇒ ∘ id ⊗₁ (σ⇒ ⊗₁ id) ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐
    ≈˘⟨ pullʳ (pullʳ (extendʳ (pushˡ assoc-commute-from))) ⟩
      (α⇐ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐
    ≈⟨ pushʳ sym-assoc ⟩∘⟨refl ⟩
      ((α⇐ ∘ id ⊗₁ α⇒ ∘ α⇒) ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐
    ≈⟨ pushˡ (conjugate-from (α ⊗ᵢ idᵢ) α (assoc ○ pentagon)) ⟩∘⟨refl ⟩
      (α⇒ ∘ α⇐ ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐
    ≈˘⟨ pushʳ (pushʳ (pushˡ split₁ˡ)) ⟩
      α⇒ ∘ α⇐ ⊗₁ id ∘ (id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
    ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
      α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
    ∎

  swapInner-assoc : [ ((X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⇒
                      (X₁ ⊗₀ (Y₁ ⊗₀ Z₁)) ⊗₀ (X₂ ⊗₀ (Y₂ ⊗₀ Z₂)) ]⟨
                      i⇒ ⊗₁ id    ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⟩
                      i⇒          ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ Z₁) ⊗₀ ((X₂ ⊗₀ Y₂) ⊗₀ Z₂) ⟩
                      α⇒ ⊗₁ α⇒
                    ≈ α⇒          ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Y₂) ⊗₀ (Z₁ ⊗₀ Z₂)) ⟩
                      id ⊗₁ i⇒    ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Z₁) ⊗₀ (Y₂ ⊗₀ Z₂)) ⟩
                      i⇒
                    ⟩
  swapInner-assoc = begin
      α⇒ ⊗₁ α⇒ ∘ i⇒ ∘ i⇒ ⊗₁ id
    ≈⟨ (begin
        α⇒ ⊗₁ α⇒
      ≈⟨ serialize₂₁ ⟩
        id ⊗₁ α⇒ ∘ α⇒ ⊗₁ id
      ≈⟨ refl⟩∘⟨ switch-fromtoˡ α (switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon) ⟩
        id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ cancelˡ α.isoʳ ⟩∘⟨refl ⟩
        id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ∘ α⇐) ∘ α⇒ ∘ α⇒
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ inv-pentagon ⟩∘⟨refl ⟩
        id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ ((α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ α⇐) ∘ α⇒ ∘ α⇒
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
        id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘
        id ⊗₁ (id ⊗₁ α⇐) ∘ α⇒ ∘ α⇒
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩
        id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘
        α⇒ ∘ (id ⊗₁ id) ⊗₁ α⇐ ∘ α⇒
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
        id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒
      ∎) ⟩∘⟨refl ⟩
      (id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒) ∘
      i⇒ ∘ i⇒ ⊗₁ id
    ≈˘⟨ pullˡ (pushˡ (⊗.identity ⟩⊗⟨refl ⟩∘⟨refl)) ⟩
      ((id ⊗₁ id) ⊗₁ α⇒ ∘ α⇐) ∘
      (id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒) ∘
      (α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
      i⇒ ⊗₁ id
    ≈⟨ ⟺ assoc-commute-to ⟩∘⟨
       pullʳ (pullʳ (pushʳ (pushˡ (pushʳ (pushˡ split₂ˡ))))) ⟩
      (α⇐ ∘ id ⊗₁ (id ⊗₁ α⇒)) ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
      ((id ⊗₁ α⇐ ∘ α⇒) ∘ α⇐ ∘ id ⊗₁ α⇒) ∘
      (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
      (α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
    ≈⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ (_≅_.isoˡ (α ⁻¹ ∘ᵢ idᵢ ⊗ᵢ α))) ⟩
      α⇐ ∘ id ⊗₁ (id ⊗₁ α⇒) ∘ id ⊗₁ (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
      (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
      (α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
    ≈⟨ refl⟩∘⟨ merge₂ sym-assoc ⟩∘⟨
         pushʳ ((⟺ ⊗.identity ⟩⊗⟨refl) ⟩∘⟨refl ⟩∘⟨ split₁ˡ) ⟩
      α⇐ ∘ id ⊗₁ ((id ⊗₁ α⇒ ∘ α⇒) ∘ α⇐ ⊗₁ id ∘ α⇐) ∘
      (α⇒ ∘ (id ⊗₁ id) ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
      α⇐ ⊗₁ id ∘ (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨
         extendʳ (pushˡ (switch-fromtoʳ (α ⊗ᵢ idᵢ) (assoc ○ pentagon))) ⟩∘⟨
         extendʳ assoc-commute-from ⟩∘⟨refl ⟩
      α⇐ ∘ id ⊗₁ ((α⇒ ∘ α⇒) ∘ (α⇐ ⊗₁ id ∘ α⇐ ⊗₁ id) ∘ α⇐) ∘
      (id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ (α⇒ ∘ α⇒)) ∘ α⇐ ⊗₁ id ∘
      (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
    ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ (refl⟩∘⟨ split₁ˡ ⟩∘⟨refl) ⟩∘⟨
         pushʳ (extendʳ (switch-fromtoʳ (α ⊗ᵢ idᵢ) (assoc ○ pentagon))) ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
      id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ id ⊗₁ α⇒ ∘ α⇒ ∘
      (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ⊗₁ id
    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
      id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ id ⊗₁ α⇒ ∘ α⇒ ∘
      (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐)) ⊗₁ id ∘ α⇒ ⊗₁ id
    ≈⟨ refl⟩∘⟨ merge₂ assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ assoc) ⟩∘⟨
         refl⟩∘⟨ extendʳ assoc-commute-from ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘
      id ⊗₁ α⇒ ∘
      id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ∘ α⇒ ∘ α⇒ ⊗₁ id
    ≈⟨ refl⟩∘⟨ merge₂ (assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ assoc²')) ⟩∘⟨
         refl⟩∘⟨ switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
      id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ∘ id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒
    ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      α⇐ ∘ id ⊗₁
        (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
      id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ α⇒
    ≈⟨ refl⟩∘⟨ merge₂ assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ (assoc²' ○
        (refl⟩∘⟨ refl⟩∘⟨ assoc))) ⟩∘⟨ Equiv.refl ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘
        α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
        (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ α⇒
    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ (begin
        α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
        (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (pushˡ split₂ˡ) ⟩
        α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id) ∘ (id ⊗₁ α⇐ ∘ α⇒) ∘
        (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ assoc-commute-to ○ (refl⟩∘⟨ sym-assoc)) ⟩
        α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id ∘ (α⇐ ∘ (id ⊗₁ α⇐ ∘ α⇒)) ∘
        (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○
           (conjugate-to α (α ⊗ᵢ idᵢ) (sym-assoc ○ inv-pentagon))) ⟩∘⟨refl ⟩
        α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id ∘ (α⇒ ⊗₁ id ∘ α⇐) ∘
        (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
      ≈˘⟨ refl⟩∘⟨ split₁ Equiv.refl ⟩∘⟨
            pushʳ (refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl) ⟩
        α⇒ ∘ ((α⇐ ∘ α⇐) ∘ id ⊗₁ σ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐ ∘
        (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇐
      ≈⟨ refl⟩∘⟨ merge₁ assoc² ⟩∘⟨ extendʳ assoc-commute-to ⟩
        α⇒ ∘ (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘
        ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘ α⇐ ∘ α⇐
      ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
        α⇒ ∘ ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘
        α⇐ ∘ α⇐
      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ inv-pentagon) ⟩
        α⇒ ∘ ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘
        α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐
      ≈⟨ refl⟩∘⟨ pullˡ (⟺ split₁ˡ ○ (assoc ⟩⊗⟨refl)) ⟩
        α⇒ ∘
        ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ⊗₁ id ∘
        α⇐ ∘ id ⊗₁ α⇐
      ≈⟨ refl⟩∘⟨ (begin
          (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
        ≈⟨ pushˡ (pushʳ sym-assoc) ⟩
          (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒ ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
        ≈⟨ (refl⟩∘⟨ extendʳ (pushʳ split₁ˡ)) ⟩
          (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒) ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ (σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐
        ≈⟨ pushʳ (switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon ⟩∘⟨ pushˡ split₁ˡ) ⟩
          ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒) ∘ (id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒)) ∘
          (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ∘ α⇐
        ≈⟨ pushˡ (sym-assoc ○ (pullˡ (pullʳ assoc ⟩∘⟨refl))) ⟩
          ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇐) ∘ α⇒) ∘
          α⇒ ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ∘ α⇐
        ≈⟨ pullʳ (refl⟩∘⟨ extendʳ assoc-commute-from) ⟩
          (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇐) ∘ α⇒ ∘
          σ⇒ ⊗₁ (id ⊗₁ id) ∘ α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐
        ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ ⟺ split₂ˡ) ⟩∘⟨ refl⟩∘⟨ (refl⟩⊗⟨ ⊗.identity ⟩∘⟨
             conjugate-from (idᵢ ⊗ᵢ (α ⁻¹)) (α ⁻¹) inv-pentagon) ⟩
          (α⇐ ∘ α⇐ ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈˘⟨ extendʳ (sym-assoc ○ inv-pentagon) ⟩∘⟨refl ⟩
          (α⇐ ⊗₁ id ∘ (α⇐ ∘ id ⊗₁ α⇐) ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘
          α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈˘⟨ (refl⟩∘⟨ pushʳ split₂ˡ) ⟩∘⟨refl ⟩
          (α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ σ⇒ ∘ α⇐)) ∘
          α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈˘⟨ pushˡ ((refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨
              (sym-assoc ○ hexagon₂ ○ assoc)) ⟩∘⟨refl) ⟩
          ((α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ σ⇒)) ∘ α⇒) ∘
          σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ pushˡ (pushʳ (pushʳ split₂ˡ)) ⟩∘⟨refl ⟩
          ((α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ σ⇒ ⊗₁ id) ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ∘
          σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ pushʳ (pushˡ split₂ˡ) ⟩∘⟨refl ⟩
          (((α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ σ⇒ ⊗₁ id) ∘ id ⊗₁ α⇐) ∘
            id ⊗₁ id ⊗₁ σ⇒ ∘ α⇒) ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ ((pushˡ (pushʳ assoc-commute-to) ⟩∘⟨
             ⟺ assoc-commute-from) ○ (pullʳ sym-assoc)) ⟩∘⟨refl ⟩
          ((α⇐ ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id) ∘ ((α⇐ ∘ id ⊗₁ α⇐) ∘ α⇒) ∘
            (id ⊗₁ id) ⊗₁ σ⇒) ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ pullˡ (⟺ split₁ˡ ⟩∘⟨
             conjugate-from α (idᵢ ⊗ᵢ α ∘ᵢ α) (⟺ (assoc ○ pentagon)))
             ⟩∘⟨refl ⟩
          (((α⇐ ∘ id ⊗₁ σ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐) ∘ (id ⊗₁ id) ⊗₁ σ⇒) ∘
          σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ (pullˡ (⟺ split₁ˡ) ⟩∘⟨ ⊗.identity ⟩⊗⟨refl) ⟩∘⟨refl ⟩
          ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ id ⊗₁ σ⇒) ∘
          σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ extend² (⟺ serialize₂₁ ○ serialize₁₂) ⟩
          ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ σ⇒ ⊗₁ id) ∘
          id ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈˘⟨ pushʳ (refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity) ⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
          (((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐ ∘ σ⇒ ⊗₁ id ⊗₁ id) ∘
          (id ⊗₁ id) ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ α⇒
        ≈⟨ pushʳ assoc-commute-to ⟩∘⟨ extendʳ (⟺ assoc-commute-to) ⟩
          ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐) ∘
          α⇐ ∘ id ⊗₁ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇒
        ≈˘⟨ ((sym-assoc ○ sym-assoc) ⟩⊗⟨refl ○ split₁ˡ) ⟩∘⟨refl ⟩∘⟨
            refl⟩∘⟨ split₂ˡ ⟩
          (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐) ∘
          α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒)
        ≈˘⟨ extend² (sym-assoc ○ inv-pentagon) ⟩
          (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐ ⊗₁ id) ∘
          (α⇐ ∘ id ⊗₁ α⇐) ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒)
        ≈˘⟨ split₁ˡ ⟩∘⟨ pushʳ split₂ˡ ⟩
          ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘
          α⇐ ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒)
        ∎) ⟩⊗⟨refl ⟩∘⟨refl ⟩
        α⇒ ∘ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐ ∘
          id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒)) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐
      ≈⟨ (refl⟩∘⟨ pushˡ ((sym-assoc ⟩⊗⟨refl) ○ split₁ˡ)) ⟩
        α⇒ ∘ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐) ⊗₁ id ∘
        (id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒)) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐
      ≈⟨ (refl⟩∘⟨ split₁ˡ ⟩∘⟨ extendʳ (⟺ assoc-commute-to)) ○ pushʳ assoc ⟩
        (α⇒ ∘ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id) ⊗₁ id) ∘
        α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ id ⊗₁ α⇐
      ≈⟨ pushˡ assoc-commute-from ⟩
        ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇒ ∘
        α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ id ⊗₁ α⇐
      ≈˘⟨ refl⟩∘⟨ pullʳ (pullʳ (refl⟩∘⟨ split₂ˡ)) ⟩
        ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘
        (α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)
      ≈˘⟨ pullʳ (pullˡ (conjugate-from (α ∘ᵢ α ⊗ᵢ idᵢ) α pentagon)) ⟩
        (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇐) ∘
        id ⊗₁ α⇒ ∘ id ⊗₁ ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)
      ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩∘⟨ ⟺ split₂ˡ ⟩
        (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
        id ⊗₁ (α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐)
      ≡⟨⟩
        (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ id ⊗₁ j⇒
      ≈˘⟨ switch-fromtoʳ α (switch-fromtoˡ α (⟺ hexagon₁))
            ⟩⊗⟨refl ⟩∘⟨refl ⟩∘⟨refl ⟩
        (σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ j⇒
      ∎) ⟩∘⟨refl ⟩
      α⇐ ∘ id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ j⇒) ∘ α⇒ ∘ α⇒
    ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ id ⊗₁ j⇒ ∘ α⇒ ∘ α⇒
    ≈˘⟨ pullʳ (pullʳ (extendʳ assoc-commute-from)) ⟩
      (α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘ (id ⊗₁ id) ⊗₁ j⇒ ∘ α⇒
    ≡⟨⟩
      i⇒ ∘ (id ⊗₁ id) ⊗₁ j⇒ ∘ α⇒
    ≈⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨ ⟺ swapInner-coherent ⟩∘⟨refl ⟩
      i⇒ ∘ id ⊗₁ i⇒ ∘ α⇒
    ∎
    where inv-pentagon = λ {W X Y Z} → _≃_.to-≈ (pentagon-iso {W} {X} {Y} {Z})

  swapInner-unitˡ : [ unit ⊗₀ (X ⊗₀ Y) ⇒ (X ⊗₀ Y) ]⟨
                      λ⇐ ⊗₁ id         ⇒⟨ (unit ⊗₀ unit) ⊗₀ (X ⊗₀ Y) ⟩
                      i⇒               ⇒⟨ (unit ⊗₀ X) ⊗₀ (unit ⊗₀ Y) ⟩
                      λ⇒ ⊗₁ λ⇒
                    ≈ λ⇒
                    ⟩
  swapInner-unitˡ = begin
      λ⇒ ⊗₁ λ⇒ ∘ i⇒ ∘ λ⇐ ⊗₁ id
    ≈⟨ refl⟩∘⟨ swapInner-coherent ⟩∘⟨ (Kelly₃′ ⟩⊗⟨refl) ⟩
      λ⇒ ⊗₁ λ⇒ ∘ j⇒ ∘ ρ⇐ ⊗₁ id
    ≡⟨⟩
      λ⇒ ⊗₁ λ⇒ ∘ (α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ ρ⇐ ⊗₁ id
    ≈⟨ pullˡ (pushˡ serialize₁₂) ⟩
      (λ⇒ ⊗₁ id ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ ρ⇐ ⊗₁ id
    ≈⟨ (refl⟩∘⟨ (begin
        id ⊗₁ λ⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
      ≈⟨ pullˡ triangle ⟩
        ρ⇒ ⊗₁ id ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
      ≈˘⟨ pushˡ split₁ˡ ⟩
        (ρ⇒ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
      ≈⟨ (pullˡ Kelly₂′ ⟩⊗⟨refl ⟩∘⟨refl) ⟩
        (id ⊗₁ ρ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
      ≈˘⟨ pushˡ split₂ˡ ⟩⊗⟨refl ⟩∘⟨refl ⟩
        (id ⊗₁ (ρ⇒ ∘ σ⇒) ∘ α⇒) ⊗₁ id ∘ α⇐
      ≈⟨ (refl⟩⊗⟨ σ⁻¹-coherence ⟩∘⟨refl) ⟩⊗⟨refl ⟩∘⟨refl ⟩
        (id ⊗₁ λ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐
      ≈⟨ triangle ⟩⊗⟨refl ⟩∘⟨refl ⟩
        (ρ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐
      ≈˘⟨ assoc-commute-to ⟩
        α⇐ ∘ ρ⇒ ⊗₁ (id ⊗₁ id)
      ∎)) ⟩∘⟨refl ⟩
      (λ⇒ ⊗₁ id ∘ α⇐ ∘ ρ⇒ ⊗₁ (id ⊗₁ id)) ∘ ρ⇐ ⊗₁ id
    ≈⟨ (sym-assoc ○ (Kelly₁′ ⟩∘⟨ refl⟩⊗⟨ ⊗.identity)) ⟩∘⟨refl ⟩
      (λ⇒ ∘ ρ⇒ ⊗₁ id) ∘ ρ⇐ ⊗₁ id
    ≈⟨ cancelʳ (_≅_.isoʳ (unitorʳ ⊗ᵢ idᵢ)) ⟩
      λ⇒
    ∎
    where
      Kelly₁′       = ⟺ (switch-fromtoʳ α (Kelly's.coherence₁ M))
      Kelly₂′       = ⟺ (switch-fromtoʳ α (Kelly's.coherence₂ M))
      Kelly₃′       = _≃_.to-≈ (Kelly's.coherence-iso₃ M)
      σ⁻¹-coherence = inv-braiding-coherence (inv-Braided B)

  swapInner-unitʳ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ (X ⊗₀ Y) ]⟨
                      id ⊗₁ λ⇐         ⇒⟨ (X ⊗₀ Y) ⊗₀ (unit ⊗₀ unit) ⟩
                      i⇒               ⇒⟨ (X ⊗₀ unit) ⊗₀ (Y ⊗₀ unit) ⟩
                      ρ⇒ ⊗₁ ρ⇒
                    ≈ ρ⇒
                    ⟩
  swapInner-unitʳ = begin
      ρ⇒ ⊗₁ ρ⇒ ∘ i⇒ ∘ id ⊗₁ λ⇐
    ≡⟨⟩
      ρ⇒ ⊗₁ ρ⇒ ∘ (α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘ id ⊗₁ λ⇐
    ≈⟨ pullˡ (pushˡ serialize₂₁) ⟩
      (id ⊗₁ ρ⇒ ∘ ρ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘ id ⊗₁ λ⇐
    ≈⟨ (refl⟩∘⟨ (begin
        ρ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
      ≈˘⟨ pushˡ (switch-fromtoʳ α triangle) ⟩
        id ⊗₁ λ⇒ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
      ≈˘⟨ pushˡ split₂ˡ ⟩
        id ⊗₁ (λ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
      ≈⟨ refl⟩⊗⟨ pullˡ (Kelly's.coherence₁ M) ⟩∘⟨refl ⟩
        id ⊗₁ (λ⇒ ⊗₁ id ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
      ≈˘⟨ refl⟩⊗⟨ pushˡ split₁ˡ ⟩∘⟨refl ⟩
        id ⊗₁ ((λ⇒ ∘ σ⇒) ⊗₁ id ∘ α⇐) ∘ α⇒
      ≈⟨ refl⟩⊗⟨ (braiding-coherence B ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩
        id ⊗₁ (ρ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
      ≈˘⟨ refl⟩⊗⟨ switch-fromtoʳ α triangle ⟩∘⟨refl ⟩
        id ⊗₁ (id ⊗₁ λ⇒) ∘ α⇒
      ≈˘⟨ assoc-commute-from ⟩
        α⇒ ∘ (id ⊗₁ id) ⊗₁ λ⇒
      ∎)) ⟩∘⟨refl ⟩
      (id ⊗₁ ρ⇒ ∘ α⇒ ∘ (id ⊗₁ id) ⊗₁ λ⇒) ∘ id ⊗₁ λ⇐
    ≈⟨ (sym-assoc ○ (Kelly's.coherence₂ M ⟩∘⟨ ⊗.identity ⟩⊗⟨refl)) ⟩∘⟨refl ⟩
      (ρ⇒ ∘ id ⊗₁ λ⇒) ∘ id ⊗₁ λ⇐
    ≈⟨ cancelʳ (_≅_.isoʳ (idᵢ ⊗ᵢ unitorˡ)) ⟩
      ρ⇒
    ∎

  swapInner-braiding : [ (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ⇒ (Y ⊗₀ Z) ⊗₀ (W ⊗₀ X) ]⟨
                         i⇒         ⇒⟨ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z) ⟩
                         σ⇒ ⊗₁ σ⇒   ⇒⟨ (Y ⊗₀ W) ⊗₀ (Z ⊗₀ X) ⟩
                         i⇒
                       ≈ σ⇒
                       ⟩
  swapInner-braiding = begin
      i⇒ ∘ σ⇒ ⊗₁ σ⇒ ∘ i⇒
    ≡⟨⟩
      i⇒ ∘ σ⇒ ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ swapInner-coherent ⟩∘⟨ pushˡ serialize₁₂ ⟩
      j⇒ ∘ σ⇒ ⊗₁ id ∘ id ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈˘⟨ ((refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity) ⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl) ○ assoc ⟩
      ((α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ σ⇒ ⊗₁ (id ⊗₁ id)) ∘
      (id ⊗₁ id) ⊗₁ σ⇒ ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ pullʳ (pullʳ assoc-commute-to) ⟩∘⟨ extendʳ (⟺ assoc-commute-to) ⟩
      (α⇒ ∘ (α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐) ∘
      α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒) ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈˘⟨ (refl⟩∘⟨ pushˡ split₁ˡ) ⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      (α⇒ ∘ ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐) ∘
      α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ (refl⟩∘⟨ pullʳ (assoc ○ hexagon₁) ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨
        refl⟩∘⟨ refl⟩⊗⟨ (⟺ assoc ○ (pullˡ (assoc ○ hexagon₁))) ⟩∘⟨refl ⟩
      (α⇒ ∘ (α⇐ ∘ α⇒ ∘ σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐) ∘
      α⇐ ∘ id ⊗₁ ((α⇒ ∘ σ⇒ ∘ α⇒) ∘ α⇐) ∘ α⇒
    ≈⟨ (refl⟩∘⟨ cancelˡ α.isoˡ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨
        refl⟩∘⟨ refl⟩⊗⟨ pullʳ (cancelʳ α.isoʳ) ⟩∘⟨refl ⟩
      (α⇒ ∘ (σ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐) ∘ α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒) ∘ α⇒
    ≈⟨ extendʳ (pushʳ split₁ˡ) ⟩∘⟨ extendʳ (pushʳ split₂ˡ) ⟩
      ((α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐) ∘ (α⇐ ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒
    ≈˘⟨ extendʳ (pushʳ (pushʳ assoc)) ⟩
      (α⇒ ∘ σ⇒ ⊗₁ id) ∘ (α⇒ ⊗₁ id ∘ (α⇐ ∘ α⇐) ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒
    ≈˘⟨ refl⟩∘⟨ switch-tofromˡ (α ⊗ᵢ idᵢ)
                  (switch-tofromʳ (idᵢ ⊗ᵢ α) inv-pentagon) ⟩∘⟨refl ⟩
      (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒
    ≈⟨ pullʳ (sym-assoc ○ pullˡ hexagon₂) ⟩
      α⇒ ∘ ((α⇐ ∘ σ⇒) ∘ α⇐) ∘ α⇒
    ≈⟨ (refl⟩∘⟨ cancelʳ α.isoˡ) ⟩
      α⇒ ∘ (α⇐ ∘ σ⇒)
    ≈⟨ cancelˡ α.isoʳ ⟩
      σ⇒
    ∎
    where inv-pentagon = _≃_.to-≈ pentagon-iso

  -- Braided monoidal categories have an interchange.

  hasInterchange : HasInterchange M
  hasInterchange = record
    { swapInner  = swapInner
    ; natural    = swapInner-natural
    ; assoc      = swapInner-assoc
    ; unitˡ      = swapInner-unitˡ
    ; unitʳ      = swapInner-unitʳ
    }
  open HasInterchange hasInterchange public using (naturalIso)

-- Extra identities that hold only for symmetric monoidal categories.

module SymmetricInterchange {M : Monoidal C} (S : Symmetric M) where
  open MonoidalReasoning M
  open MonoidalUtilities M
  open Symmetric S renaming (associator to α)
  open Shorthands
  open BraidedInterchange braided public
  private
    i⇒ = swapInner.from
    i⇐ = swapInner.to
    σ⇒ = λ {X Y} → braiding.⇒.η (X , Y)
    σ⇐ = λ {X Y} → braiding.⇐.η (X , Y)

  swapInner-commutative : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒
                            (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ]⟨
                             i⇒    ⇒⟨ (X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂) ⟩
                             i⇒
                           ≈ id
                           ⟩
  swapInner-commutative = begin
      i⇒ ∘ i⇒
    ≈⟨ pullʳ (cancelInner α.isoʳ) ⟩
      α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈˘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
      α⇐ ∘ id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒
    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (∘-resp-≈ʳ sym-assoc ○ α[σ⊗1]α⁻¹.isoʳ) ⟩∘⟨refl ⟩
      α⇐ ∘ id ⊗₁ id ∘ α⇒
    ≈⟨ refl⟩∘⟨ ⊗.identity ⟩∘⟨refl ⟩
      α⇐ ∘ id ∘ α⇒
    ≈⟨ ∘-resp-≈ʳ identityˡ ○ α.isoˡ ⟩
      id
    ∎
    where module α[σ⊗1]α⁻¹ = _≅_ (α ∘ᵢ braided-iso ⊗ᵢ idᵢ ∘ᵢ α ⁻¹)

  swapInner-iso : (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)
  swapInner-iso = record
    { from = i⇒
    ; to   = i⇒
    ; iso  = record
      { isoˡ = swapInner-commutative
      ; isoʳ = swapInner-commutative
      }
    }

  swapInner-braiding′ : [ (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ⇒ (Y ⊗₀ W) ⊗₀ (Z ⊗₀ X) ]⟨
                          i⇒         ⇒⟨ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z) ⟩
                          σ⇒ ⊗₁ σ⇒
                        ≈ σ⇒         ⇒⟨ (Y ⊗₀ Z) ⊗₀ (W ⊗₀ X) ⟩
                          i⇒
                        ⟩
  swapInner-braiding′ = switch-fromtoˡ swapInner-iso swapInner-braiding

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
module Issue848 where

A : Set1
A = B module _ where
  B : Set1
  B = Set

C : Set1
C = B

D : Set1
D = E module _ where
  E : Set1
  E = Set

F : Set1
F = G module _ where
  G : Set1
  G = H module _ where
    H : Set1
    H = Set


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

open import Prelude
open import Algebra
open import Container

module Control.Monad.ListT
  {ℓ}
  (𝔽 : Container ℓ ℓ)
  (is-mon : IsMonad {ℓ} ⟦ 𝔽 ⟧ )
  where

open IsMonad is-mon

postulate
  cmap-return : (f : A → B) (x : ⟦ 𝔽 ⟧ A) →
                (cmap f x ≡ (x >>= return ∘ f))

infixr 5 _∷_
mutual
  List : Type ℓ → Type _
  List A = ⟦ 𝔽 ⟧ (Cons A)

  data Cons (A : Type ℓ) : Type ℓ where
    []  : Cons A
    _∷_ : (x : A) → (xs : List A) → Cons A

data ℭ𝔬𝔫𝔰 (A : Type ℓ) (P : List A → Type ℓ) : Type ℓ where
  [] : ℭ𝔬𝔫𝔰 A P
  _∷_⟨_⟩ : (x : A) → (xs : List A) → (P⟨xs⟩ : P xs) → ℭ𝔬𝔫𝔰 A P

module _ (P : List A → Type ℓ) where
  wrapc : ℭ𝔬𝔫𝔰 A P → Cons A
  wrapc [] = []
  wrapc (x ∷ xs ⟨ P⟨xs⟩ ⟩) = x ∷ xs

  wrap : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P) → List A
  wrap = cmap wrapc
  {-# INLINE wrap #-}

  module _ (ψ : (x : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P)) → P (wrap x)) where
    elim : (x : List A) → P x
    elimc : Cons A → ℭ𝔬𝔫𝔰 A P
    wrapc-elimc : (c : Cons A) → wrapc (elimc c) ≡ c

    wrapc-elimc []       i = []
    wrapc-elimc (x ∷ xs) i = x ∷ xs

    elimc [] = []
    elimc (x ∷ xs) = x ∷ xs ⟨ elim xs ⟩

    elim xs =
      subst
        P
        (cong (xs .fst ,_) (funExt (λ x → wrapc-elimc (xs .snd x))))
        (ψ (cmap elimc xs))

module _  (ϕ : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (const B)) → B) where
  para : List A → B
  parac : Cons A → ℭ𝔬𝔫𝔰 A (const B)

  para xs = ϕ (cmap parac xs)

  parac [] = []
  parac (x ∷ xs) = x ∷ xs ⟨ para xs ⟩

++-ϕ : List A → ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (const (List A))) → List A
++-ϕ ys xs = xs >>= λ { [] → ys ; (x ∷ _ ⟨ xs ⟩) → return (x ∷ xs) }

infixr 5 _++_
_++_ : List A → List A → List A
xs ++ ys = para (++-ϕ ys) xs

cmap-comp : (f : B → C) (g : A → B) (x : ⟦ 𝔽 ⟧ A) → cmap f (cmap g x) ≡ cmap (f ∘ g) x
cmap-comp f g x = refl

cmap-id : (x : ⟦ 𝔽 ⟧ A) → cmap id x ≡ x
cmap-id x = refl

open import Path.Reasoning

++-id : (xs : List A) → xs ++ return [] ≡ xs
++-id {A = A} = elim P ψ
  where
  P : List A → Type ℓ
  P xs = xs ++ return [] ≡ xs

  ϕ : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (const (List A))) → List A
  ϕ = ++-ϕ (return [])

  ϕ′ : ℭ𝔬𝔫𝔰 A (const (List A)) → Cons A
  ϕ′ [] = []
  ϕ′ (x ∷ xs ⟨ P⟨xs⟩ ⟩) = x ∷ P⟨xs⟩

  ϕ≡ : ∀ xs → ϕ xs ≡ (xs >>= return ∘′ ϕ′)
  ϕ≡ xs = cong (xs >>=_) (funExt (λ { [] → refl ; (x ∷ xs ⟨ P⟨xs⟩ ⟩) → refl }))

  lemma : (xs : ℭ𝔬𝔫𝔰 A P) → ϕ′ (parac ϕ (wrapc P xs)) ≡ wrapc P xs
  lemma [] = refl
  lemma (x ∷ xs ⟨ P⟨xs⟩ ⟩) = cong (x ∷_) P⟨xs⟩

  ψ : (xs : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P)) → P (wrap P xs)
  ψ xs =
    wrap P xs ++ return [] ≡⟨⟩
    para ϕ (wrap P xs) ≡⟨⟩
    ϕ (cmap (parac ϕ) (wrap P xs)) ≡⟨ ϕ≡ _ ⟩
    (cmap (parac ϕ) (wrap P xs) >>= return ∘′ ϕ′) ≡˘⟨ cmap-return ϕ′ _ ⟩
    cmap ϕ′ (cmap (parac ϕ) (wrap P xs)) ≡⟨⟩
    cmap (ϕ′ ∘ parac ϕ) (wrap P xs) ≡⟨⟩
    cmap (ϕ′ ∘ parac ϕ) (cmap (wrapc P) xs) ≡⟨⟩
    cmap (ϕ′ ∘ parac ϕ ∘ wrapc P) xs ≡⟨ cong (flip cmap xs) (funExt lemma) ⟩
    wrap P xs ∎

-- open import Cubical.Data.Sigma.Properties

-- ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
-- ++-assoc {A = A} xs ys zs = elim P ψ xs
--   where
--   P : List A → Type ℓ
--   P xs′ = (xs′ ++ ys) ++ zs ≡ xs′ ++ (ys ++ zs)
--   {-# INLINE P #-}

--   ψ : (x : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A P)) → P (wrap P x)
--   ψ xs = ΣPathTransport→PathΣ _ _ ({!refl!} , {!!})

-- _>>=′_ : List A → (A → List B) → List B
-- _>>=′_ {A = A} {B = B} xs k = para ϕ xs
--   where
--   ϕ : ⟦ 𝔽 ⟧ (ℭ𝔬𝔫𝔰 A (List B)) → List B
--   ϕ xs = xs >>= λ { [] → return [] ; (x ∷ xs) → k x ++ xs }

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- 2014-05-27 Jesper and Andreas

postulate
  A : Set
  a : A → A → A

{-# BUILTIN REWRITE a #-}

-- Expected error:

-- a  does not have the right type for a rewriting relation
-- because its type does not end in a sort, but in  A
-- when checking the pragma BUILTIN REWRITE a

max_stars_repo_name: larrytheliquid/agda


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

-- all the important stuff about NaturalTransformation are defined in .Core

open import Categories.NaturalTransformation.Core public


text:
open import Issue481PonderBase
open import Issue481PonderImportMe as as

module Issue481PonderMaster where

module M = as as as

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda