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

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Abstract.Types -- TODO-2: remove this, see comment below

open import LibraBFT.Yasm.AvailableEpochs using (AvailableEpochs) renaming (lookup'' to EC-lookup)
import LibraBFT.Yasm.AvailableEpochs as AE

open import LibraBFT.Yasm.Base

-- This module defines a model of a distributed system, parameterized by
-- SystemParameters, which establishes various application-dependent types,
-- handlers, etc.  The model supports a set of peers executing handlers in
-- response to messages received; these handlers can update the peer's
-- local state and/or send additional messages.  The model also enables
-- "cheat" steps, which can send arbitrary messages, except that they are
-- constrained to prevent a cheat step from introducing a new signature for
-- an "honest" public key.  The module also contains some structures for
-- proving properties of executions of the modeled system.

module LibraBFT.Yasm.System (parms : SystemParameters) where
 open SystemParameters parms

 -- TODO-2: The System model currently depends on a specific EpochConfig
 -- type, which is imported from LibraBFT-specific types.  However, the
 -- system model should be entirely application-independent.  Therefore, we
 -- should factor EpochConfig out of Yasm, and have the SystemParameters
 -- include an EpochConfig type and a way to query whether a given peer is
 -- a member of the represented epoch, and if so, with what associated PK.
 open EpochConfig

 PeerId : Set -- TODO-2: When we factor EpochConfig out of here (see
              -- comment above), PeerId will be a parameter to
              -- SystemParameters; for now, it's NodeId to make it
              -- compatible with everything else.
 PeerId = NodeId

 SenderMsgPair : Set
 SenderMsgPair = PeerId × Msg

 SentMessages : Set
 SentMessages = List SenderMsgPair

 -- The model supports sending messages that contain some fields that are
 -- /not/ covered by the message's signature.  Therefore, given a message
 -- with a verifiable signature, it is possible for a propositionally
 -- different message that verifies against the same signature to have been
 -- sent before, which is captured by the following definition.
 record MsgWithSig∈ (pk : PK)(sig : Signature)(pool : SentMessages) : Set where
   constructor mkMsgWithSig∈
   field
     msgWhole   : Msg
     msgPart    : Part
     msg⊆       : msgPart ⊂Msg msgWhole
     msgSender  : PeerId
     msg∈pool   : (msgSender , msgWhole) ∈ pool
     msgSigned  : WithVerSig pk msgPart
     msgSameSig : ver-signature msgSigned ≡ sig
 open MsgWithSig∈ public

 postulate  -- TODO-1: prove it
   MsgWithSig∈? : ∀ {pk} {sig} {pool} → Dec (MsgWithSig∈ pk sig pool)

 MsgWithSig∈-++ʳ : ∀{pk sig pool ms} → MsgWithSig∈ pk sig pool → MsgWithSig∈ pk sig (ms ++ pool)
 MsgWithSig∈-++ʳ {ms = pre} msig = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = Any-++ʳ pre (msg∈pool msig)
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 MsgWithSig∈-++ˡ : ∀{pk sig pool ms} → MsgWithSig∈ pk sig ms → MsgWithSig∈ pk sig (ms ++ pool)
 MsgWithSig∈-++ˡ {ms = pre} msig = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = Any-++ˡ (msg∈pool msig)
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 MsgWithSig∈-transp : ∀{pk sig pool pool'}
                    → (mws : MsgWithSig∈ pk sig pool)
                    → (msgSender mws , msgWhole mws) ∈ pool'
                    → MsgWithSig∈ pk sig pool'
 MsgWithSig∈-transp msig ∈pool' = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = ∈pool'
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 -- * Forbidding the Forging of Signatures
 --
 -- Whenever our reasoning must involve digital signatures, it is standard
 -- to talk about EUF-CMA resistant signature schemes. Informally, this captures
 -- signatures schemes that cannot be compromised by certain adversaries.
 -- Formally, it means that for any probabilistic-polynomial-time adversary 𝓐,
 -- and some security parameter k:
 --
 --      Pr[ EUF-CMA(k) ] ≤ ε(k) for ε a negigible function.
 --
 -- EUF-CMA is defined as:
 --
 -- EUF-CMA(k):                           |  O(m):
 --   L        ← ∅                        |    σ ← Sign(sk , m)
 --   (pk, sk) ← Gen(k)                   |    L ← L ∪ { m }
 --   (m , σ)  ← 𝓐ᴼ(pk)                   |    return σ
 --   return (Verify(pk, m, σ) ∧ m ∉ L)   |
 --
 -- This says that 𝓐 cannot create a message that has /not yet been signed/ and
 -- forge a signature for it. The list 'L' keeps track of the messages that 𝓐
 -- asked to be signed by the oracle.
 --
 -- Because the probability of the adversary to win the EUF-CMA(k) game
 -- approaches 0 as k increases; it is reasonable to assume that winning
 -- the game is /impossible/ for realistic security parameters.
 --
 -- EUF-CMA security is incorporated into our model by constraining messages
 -- sent by a cheat step to ensure that for every verifiably signed part of
 -- such a message, if there is a signature on the part, then it is either for
 -- a dishonest public key (in which cases it's secret key may have been leaked),
 -- or a message has been sent with the same signature before (in which case the
 -- signature is simply being "replayed" from a previous message).
 --
 -- Dishonest (or "cheat") messages are those that are not the result of
 -- a /handle/ or /init/ call, but rather are the result of a /cheat/ step.
 --
 -- A part of a cheat message can contain a verifiable signature only if it
 -- is for a dishonest public key, or a message with the same signature has
 -- been sent before (a cheater can "reuse" an honest signature sent
 -- before; it just can't produce a new one).  Note that this constraint
 -- precludes a peer sending a message that contains a new verifiable
 -- signature for an honest PK, even if the PK is the peer's own PK for
 -- some epoch (implying that the peer possesses the associated secret
 -- key).  In other words, a peer that is honest for a given epoch (by
 -- virtue of being a member of that epoch and being assigned an honest PK
 -- for the epoch), cannot send a message for that epoch using a cheat
 -- step.
 CheatPartConstraint : SentMessages → Part → Set
 CheatPartConstraint pool m = ∀{pk} → (ver : WithVerSig pk m)
                                    → Meta-Dishonest-PK pk
                                    ⊎ MsgWithSig∈ pk (ver-signature ver) pool

 -- The only constraints on messages sent by cheat steps are that:
 -- * the sender is not an honest member in the epoch of any part of the message
 -- * the signature on any part of the message satisfies CheatCanSign, meaning
 --   that it is not a new signature for an honest public key
 CheatMsgConstraint : SentMessages → Msg → Set
 CheatMsgConstraint pool m = ∀{part} → part ⊂Msg m → CheatPartConstraint pool part

 -- * The System State
 --
 -- A system consists in a partial map from PeerId to PeerState, a pool
 -- of sent messages and a number of available epochs.
 record SystemState (e : ℕ) : Set₁ where
   field
     peerStates  : Map PeerId PeerState
     msgPool     : SentMessages          -- All messages ever sent
     availEpochs : AvailableEpochs e
 open SystemState public

 initialState : SystemState 0
 initialState = record
   { peerStates  = Map-empty
   ; msgPool     = []
   ; availEpochs = []
   }

 -- Convenience function for appending an epoch to the system state
 pushEpoch : ∀{e} → EpochConfigFor e → SystemState e → SystemState (suc e)
 pushEpoch 𝓔 st = record
   { peerStates  = peerStates st
   ; msgPool     = msgPool st
   ; availEpochs = AE.append 𝓔 (availEpochs st)
   }

 -- * Small Step Semantics
 --
 -- The small step semantics are divided into three datatypes:
 --
 -- i)   StepPeerState executes a step through init or handle
 -- ii)  StepPeer executes a step through StepPeerState or cheat
 -- iii) Step transitions the system state by a StepPeer or by
 --      bringing a new epoch into existence

 -- The pre and post states of Honest peers are related iff
 data StepPeerState {e}(pid : PeerId)(𝓔s : AvailableEpochs e)(pool : SentMessages)
          : Maybe PeerState → PeerState → List Msg → Set where
   -- The peer receives an "initialization package"; for now, this consists
   -- of the actual EpochConfig for the epoch being initialized.  Later, we
   -- may move to a more general scheme, enabled by assuming a function
   -- 'render : InitPackage -> EpochConfig'.
   step-init : ∀{ms s' out}(ix : Fin e)
             → (s' , out) ≡ init pid (AE.lookup' 𝓔s ix) ms
             → StepPeerState pid 𝓔s pool ms s' out

   -- The peer processes a message in the pool
   step-msg  : ∀{m ms s s' out}
             → m ∈ pool
             → ms ≡ just s → (s' , out) ≡ handle pid (proj₂ m) s
             → StepPeerState pid 𝓔s pool ms s' out

 -- The pre-state of the suplied PeerId is related to the post-state and list of output messages iff:
 data StepPeer {e}(pre : SystemState e) : PeerId → Maybe PeerState → List Msg → Set where
   -- it can be obtained by a handle or init call.
   step-honest : ∀{pid st outs}
               → StepPeerState pid (availEpochs pre) (msgPool pre) (Map-lookup pid (peerStates pre)) st outs
               → StepPeer pre pid (just st) outs

   -- or the peer decides to cheat.  CheatMsgConstraint ensures it cannot
   -- forge signatures by honest peers.  Cheat steps do not modify peer
   -- state: these are maintained exclusively by the implementation
   -- handlers.
   step-cheat  : ∀{pid}
               → (fm : SentMessages → Maybe PeerState → Msg)
               → let m = fm (msgPool pre) (Map-lookup pid (peerStates pre))
                  in CheatMsgConstraint (msgPool pre) m
                   → StepPeer pre pid (Map-lookup pid (peerStates pre)) (m ∷ [])

 isCheat : ∀ {e pre pid ms outs} → StepPeer {e} pre pid ms outs → Set
 isCheat (step-honest _)  = ⊥
 isCheat (step-cheat _ _) = Unit

 -- Computes the post-sysstate for a given step-peer.
 StepPeer-post : ∀{e pid st' outs}{pre : SystemState e}
               → StepPeer pre pid st' outs → SystemState e
 StepPeer-post {e} {pid} {st'} {outs} {pre} _ = record pre
   { peerStates = Map-set pid st' (peerStates pre)
   ; msgPool    = List-map (pid ,_) outs ++ msgPool pre
   }

 data Step : ∀{e e'} → SystemState e → SystemState e' → Set₁ where
   step-epoch : ∀{e}{pre : SystemState e}
              → (𝓔 : EpochConfigFor e)
              -- TODO-3: Eventually, we'll condition this step to only be
              -- valid when peers on the previous epoch have agreed that 𝓔
              -- is the new one.  → ∃EnoughValidCommitMsgsFor pre 𝓔
              → Step pre (pushEpoch 𝓔 pre)

   step-peer : ∀{e pid st' outs}{pre : SystemState e}
             → (pstep : StepPeer pre pid st' outs)
             → Step pre (StepPeer-post pstep)

 postulate -- TODO-1: prove it
   msgs-stable : ∀ {e e'} {pre : SystemState e} {post : SystemState e'} {m}
               → (theStep : Step pre post)
               → m ∈ msgPool pre
               → m ∈ msgPool post

 postulate -- not used yet, but some proofs could probably be cleaned up using this,
           -- e.g., prevVoteRnd≤-pred-step in Impl.VotesOnce
   sendMessages-target : ∀ {m : SenderMsgPair} {sm : SentMessages} {ml : List SenderMsgPair}
                       → ¬ (m ∈ sm)
                       → m ∈ (ml ++ sm)
                       → m ∈ ml

 step-epoch-does-not-send : ∀ {e} (pre : SystemState e) (𝓔 : EpochConfigFor e)
                            → msgPool (pushEpoch 𝓔 pre) ≡ msgPool pre
 step-epoch-does-not-send _ _ = refl

 -- * Reflexive-Transitive Closure

 data Step* : ∀{e e'} → SystemState e → SystemState e' → Set₁ where
   step-0 : ∀{e}{pre : SystemState e}
          → Step* pre pre

   step-s : ∀{e e' e''}{fst : SystemState e}{pre : SystemState e'}{post : SystemState e''}
          → Step* fst pre
          → Step pre post
          → Step* fst post

 ReachableSystemState : ∀{e} → SystemState e → Set₁
 ReachableSystemState = Step* initialState

 Step*-mono : ∀{e e'}{st : SystemState e}{st' : SystemState e'}
            → Step* st st' → e ≤ e'
 Step*-mono step-0 = ≤-refl
 Step*-mono (step-s tr (step-peer _)) = Step*-mono tr
 Step*-mono (step-s tr (step-epoch _)) = ≤-step (Step*-mono tr)

 MsgWithSig∈-Step* : ∀{e e' sig pk}{st : SystemState e}{st' : SystemState e'}
                   → Step* st st'
                   → MsgWithSig∈ pk sig (msgPool st)
                   → MsgWithSig∈ pk sig (msgPool st')
 MsgWithSig∈-Step* step-0        msig = msig
 MsgWithSig∈-Step* (step-s tr (step-epoch _)) msig
   = MsgWithSig∈-Step* tr msig
 MsgWithSig∈-Step* (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-++ʳ (MsgWithSig∈-Step* tr msig)

 MsgWithSig∈-Step*-part : ∀{e e' sig pk}{st : SystemState e}{st' : SystemState e'}
                        → (tr   : Step* st st')
                        → (msig : MsgWithSig∈ pk sig (msgPool st))
                        → msgPart msig ≡ msgPart (MsgWithSig∈-Step* tr msig)
 MsgWithSig∈-Step*-part step-0        msig = refl
 MsgWithSig∈-Step*-part (step-s tr (step-epoch _)) msig
   = MsgWithSig∈-Step*-part tr msig
 MsgWithSig∈-Step*-part (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-Step*-part tr msig

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

 -- Type synonym to express a relation over system states;
 SystemStateRel : (∀{e e'} → SystemState e → SystemState e' → Set₁) → Set₂
 SystemStateRel P = ∀{e e'}{st : SystemState e}{st' : SystemState e'} → P st st' → Set₁

 -- Just like Data.List.Any maps a predicate over elements to a predicate over lists,
 -- Any-step maps a relation over steps to a relation over steps in a trace.
 data Any-Step (P : SystemStateRel Step) : SystemStateRel Step* where
  step-here  : ∀{e e' e''}{fst : SystemState e}{pre : SystemState e'}{post : SystemState e''}
             → (cont : Step* fst pre)
             → {this : Step pre post}(prf  : P this)
             → Any-Step P (step-s cont this)

  step-there : ∀{e e' e''}{fst : SystemState e}{pre : SystemState e'}{post : SystemState e''}
             → {cont : Step* fst pre}
             → {this : Step pre post}
             → (prf  : Any-Step P cont)
             → Any-Step P (step-s cont this)

 Any-Step-elim
   : ∀{e₀ e₁}{st₀ : SystemState e₀}{st₁ : SystemState e₁}{P : SystemStateRel Step}{Q : Set₁}
   → {r : Step* st₀ st₁}
   → (P⇒Q : ∀{d d'}{s : SystemState d}{s' : SystemState d'}{st : Step s s'}
          → P st → Step* s' st₁ → Q)
   → Any-Step P r → Q
 Any-Step-elim P⇒Q (step-here cont prf)
   = P⇒Q prf step-0
 Any-Step-elim P⇒Q (step-there {this = this} f)
   = Any-Step-elim (λ p s → P⇒Q p (step-s s this)) f

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

 module _ (P : ∀{e} → SystemState e → Set) where

   Step*-Step-fold : (∀{e}{st : SystemState e}
                        → ReachableSystemState st
                        → (𝓔 : EpochConfigFor e)
                        → P st
                        → P (pushEpoch 𝓔 st))
                   → (∀{e pid st' outs}{st : SystemState e}
                        → ReachableSystemState st
                        → (pstep : StepPeer st pid st' outs)
                        → P st
                        → P (StepPeer-post pstep))
                   → P initialState
                   → ∀{e}{st : SystemState e}
                   → (tr : ReachableSystemState st) → P st
   Step*-Step-fold fe fs p₀ step-0 = p₀
   Step*-Step-fold fe fs p₀ (step-s tr (step-epoch 𝓔)) = fe tr 𝓔 (Step*-Step-fold fe fs p₀ tr)
   Step*-Step-fold fe fs p₀ (step-s tr (step-peer p)) = fs tr p (Step*-Step-fold fe fs p₀ tr)


text:
module lists where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
open import Level using (Level)
-- open import plfa.part1.Isomorphism using (_≃_; _⇔_)

-- 同型 (isomorphism)
infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
-- open _≃_

-- 同値 (equivalence)
record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

-- Lists

-- リスト
infixr 5 _∷_
data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

_ : List ℕ
_ = 0 ∷ 1 ∷ 2 ∷ []

data List′ : Set → Set where
  []′  : ∀ {A : Set} → List′ A
  _∷′_ : ∀ {A : Set} → A → List′ A → List′ A

_ : List ℕ
_ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ})))

-- List syntax

-- リストの便利記法
pattern [_] z = z ∷ []
pattern [_,_] y z = y ∷ z ∷ []
pattern [_,_,_] x y z = x ∷ y ∷ z ∷ []
pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []
pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []

-- Append

-- リストの結合
infixr 5 _++_
_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

_ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ]
_ =
  begin
    0 ∷ 1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ []
  ≡⟨⟩
    0 ∷ (1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    0 ∷ 1 ∷ (2 ∷ [] ++ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    0 ∷ 1 ∷ 2 ∷ ([] ++ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []
  ∎

-- Reasoning about append

-- リストの結合法則
++-assoc : ∀ {A : Set} (xs ys zs : List A)
  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs =
  begin
    ([] ++ ys) ++ zs
  ≡⟨⟩
    ys ++ zs
  ≡⟨⟩
    [] ++ (ys ++ zs)
  ∎
++-assoc (x ∷ xs) ys zs =
  begin
    (x ∷ xs ++ ys) ++ zs
  ≡⟨⟩
    x ∷ (xs ++ ys) ++ zs
  ≡⟨⟩
    x ∷ ((xs ++ ys) ++ zs)
  ≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩
    x ∷ (xs ++ (ys ++ zs))
  ≡⟨⟩
    x ∷ xs ++ (ys ++ zs)
  ∎

-- 空のリストが左単位元であることの証明
++-identityˡ : ∀ {A : Set} (xs : List A) → [] ++ xs ≡ xs
++-identityˡ xs =
  begin
    [] ++ xs
  ≡⟨⟩
    xs
  ∎

-- 空のリストが右単位元であることの証明
++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-identityʳ [] =
  begin
    [] ++ []
  ≡⟨⟩
    []
  ∎
++-identityʳ (x ∷ xs) =
  begin
    (x ∷ xs) ++ []
  ≡⟨⟩
    x ∷ (xs ++ [])
  ≡⟨ cong (x ∷_) (++-identityʳ xs) ⟩
    x ∷ xs
  ∎

-- Length

-- リスト長を返す関数
length : ∀ {A : Set} → List A → ℕ
length []       = zero
length (x ∷ xs) = suc (length xs)

_ : length [ 0 , 1 , 2 ] ≡ 3
_ =
  begin
    length (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    suc (length (1 ∷ 2 ∷ []))
  ≡⟨⟩
    suc (suc (length (2 ∷ [])))
  ≡⟨⟩
    suc (suc (suc (length {ℕ} [])))
  ≡⟨⟩
    suc (suc (suc zero))
  ∎

-- Reasoning about length

-- lengthの分配性の証明
length-++ : ∀ {A : Set} (xs ys : List A)
  → length (xs ++ ys) ≡ length xs + length ys
length-++ {A} [] ys =
  begin
    length ([] ++ ys)
  ≡⟨⟩
    length ys
  ≡⟨⟩
    length {A} [] + length ys
  ∎
length-++ (x ∷ xs) ys =
  begin
    length ((x ∷ xs) ++ ys)
  ≡⟨⟩
    suc (length (xs ++ ys))
  ≡⟨ cong suc (length-++ xs ys) ⟩
    suc (length xs + length ys)
  ≡⟨⟩
    length (x ∷ xs) + length ys
  ∎

-- Reverse

-- 逆順のリストを返す関数
reverse : ∀ {A : Set} → List A → List A
reverse []       = []
reverse (x ∷ xs) = reverse xs ++ [ x ]

_ : reverse [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ =
  begin
    reverse (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    reverse (1 ∷ 2 ∷ []) ++ [ 0 ]
  ≡⟨⟩
    (reverse (2 ∷ []) ++ [ 1 ]) ++ [ 0 ]
  ≡⟨⟩
    ((reverse [] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
  ≡⟨⟩
    (([] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
  ≡⟨⟩
    (([] ++ 2 ∷ []) ++ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    (2 ∷ [] ++ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    2 ∷ ([] ++ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    (2 ∷ 1 ∷ []) ++ 0 ∷ []
  ≡⟨⟩
    2 ∷ (1 ∷ [] ++ 0 ∷ [])
  ≡⟨⟩
    2 ∷ 1 ∷ ([] ++ 0 ∷ [])
  ≡⟨⟩
    2 ∷ 1 ∷ 0 ∷ []
  ≡⟨⟩
    [ 2 , 1 , 0 ]
  ∎

-- Faster reverse

shunt : ∀ {A : Set} → List A → List A → List A
shunt []       ys  =  ys
shunt (x ∷ xs) ys  =  shunt xs (x ∷ ys)

shunt-reverse : ∀ {A : Set} (xs ys : List A)
  → shunt xs ys ≡ reverse xs ++ ys
shunt-reverse [] ys =
  begin
    shunt [] ys
  ≡⟨⟩
    ys
  ≡⟨⟩
    reverse [] ++ ys
  ∎
shunt-reverse (x ∷ xs) ys =
  begin
    shunt (x ∷ xs) ys
  ≡⟨⟩
    shunt xs (x ∷ ys)
  ≡⟨ shunt-reverse xs (x ∷ ys) ⟩
    reverse xs ++ (x ∷ ys)
  ≡⟨⟩
    reverse xs ++ ([ x ] ++ ys)
  ≡⟨ sym (++-assoc (reverse xs) [ x ] ys) ⟩
    (reverse xs ++ [ x ]) ++ ys
  ≡⟨⟩
    reverse (x ∷ xs) ++ ys
  ∎

reverse′ : ∀ {A : Set} → List A → List A
reverse′ xs = shunt xs []

reverses : ∀ {A : Set} (xs : List A)
  → reverse′ xs ≡ reverse xs
reverses xs =
  begin
    reverse′ xs
  ≡⟨⟩
    shunt xs []
  ≡⟨ shunt-reverse xs [] ⟩
    reverse xs ++ []
  ≡⟨ ++-identityʳ (reverse xs) ⟩
    reverse xs
  ∎

_ : reverse′ [ 0 , 1 , 2 ] ≡ [ 2 , 1 , 0 ]
_ =
  begin
    reverse′ (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    shunt (0 ∷ 1 ∷ 2 ∷ []) []
  ≡⟨⟩
    shunt (1 ∷ 2 ∷ []) (0 ∷ [])
  ≡⟨⟩
    shunt (2 ∷ []) (1 ∷ 0 ∷ [])
  ≡⟨⟩
    shunt [] (2 ∷ 1 ∷ 0 ∷ [])
  ≡⟨⟩
    2 ∷ 1 ∷ 0 ∷ []
  ∎

-- Map

map : ∀ {A B : Set} → (A → B) → List A → List B
map f []        =  []
map f (x ∷ xs)  =  f x ∷ map f xs

_ : map suc [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
_ =
  begin
    map suc (0 ∷ 1 ∷ 2 ∷ [])
  ≡⟨⟩
    suc 0 ∷ map suc (1 ∷ 2 ∷ [])
  ≡⟨⟩
    suc 0 ∷ suc 1 ∷ map suc (2 ∷ [])
  ≡⟨⟩
    suc 0 ∷ suc 1 ∷ suc 2 ∷ map suc []
  ≡⟨⟩
    suc 0 ∷ suc 1 ∷ suc 2 ∷ []
  ≡⟨⟩
    1 ∷ 2 ∷ 3 ∷ []
  ∎

sucs : List ℕ → List ℕ
sucs = map suc

_ : sucs [ 0 , 1 , 2 ] ≡ [ 1 , 2 , 3 ]
_ =
  begin
    sucs [ 0 , 1 , 2 ]
  ≡⟨⟩
    map suc [ 0 , 1 , 2 ]
  ≡⟨⟩
    [ 1 , 2 , 3 ]
  ∎

-- 右畳み込み
foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr _⊗_ e []        =  e
foldr _⊗_ e (x ∷ xs)  =  x ⊗ foldr _⊗_ e xs

_ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
_ =
  begin
    foldr _+_ 0 (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    1 + foldr _+_ 0 (2 ∷ 3 ∷ 4 ∷ [])
  ≡⟨⟩
    1 + (2 + foldr _+_ 0 (3 ∷ 4 ∷ []))
  ≡⟨⟩
    1 + (2 + (3 + foldr _+_ 0 (4 ∷ [])))
  ≡⟨⟩
    1 + (2 + (3 + (4 + foldr _+_ 0 [])))
  ≡⟨⟩
    1 + (2 + (3 + (4 + 0)))
  ∎

-- リストの要素の和
sum : List ℕ → ℕ
sum = foldr _+_ 0

_ : sum [ 1 , 2 , 3 , 4 ] ≡ 10
_ =
  begin
    sum [ 1 , 2 , 3 , 4 ]
  ≡⟨⟩
    foldr _+_ 0 [ 1 , 2 , 3 , 4 ]
  ≡⟨⟩
    10
  ∎

-- Monoids

record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where
  field
    assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
    identityˡ : ∀ (x : A) → e ⊗ x ≡ x
    identityʳ : ∀ (x : A) → x ⊗ e ≡ x

open IsMonoid

+-monoid : IsMonoid _+_ 0
+-monoid =
  record
    { assoc = +-assoc
    ; identityˡ = +-identityˡ
    ; identityʳ = +-identityʳ
    }

*-monoid : IsMonoid _*_ 1
*-monoid =
  record
    { assoc = *-assoc
    ; identityˡ = *-identityˡ
    ; identityʳ = *-identityʳ
    }

++-monoid : ∀ {A : Set} → IsMonoid {List A} _++_ []
++-monoid =
  record
    { assoc = ++-assoc
    ; identityˡ = ++-identityˡ
    ; identityʳ = ++-identityʳ
    }

foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs : List A) (y : A) → foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ y
foldr-monoid _⊗_ e ⊗-monoid [] y =
  begin
    foldr _⊗_ y []
  ≡⟨⟩
    y
  ≡⟨ sym (identityˡ ⊗-monoid y) ⟩
    (e ⊗ y)
  ≡⟨⟩
    foldr _⊗_ e [] ⊗ y
  ∎
foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
  begin
    foldr _⊗_ y (x ∷ xs)
  ≡⟨⟩
    x ⊗ (foldr _⊗_ y xs)
  ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e ⊗-monoid xs y) ⟩
    x ⊗ (foldr _⊗_ e xs ⊗ y)
  ≡⟨ sym (assoc ⊗-monoid x (foldr _⊗_ e xs) y) ⟩
    (x ⊗ foldr _⊗_ e xs) ⊗ y
  ≡⟨⟩
    foldr _⊗_ e (x ∷ xs) ⊗ y
  ∎

postulate
  foldr-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) (xs ys : List A) →
    foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs

foldr-monoid-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs ys : List A) → foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
  begin
    foldr _⊗_ e (xs ++ ys)
  ≡⟨ foldr-++ _⊗_ e xs ys ⟩
    foldr _⊗_ (foldr _⊗_ e ys) xs
  ≡⟨ foldr-monoid _⊗_ e monoid-⊗ xs (foldr _⊗_ e ys) ⟩
    foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
  ∎

-- All

data All {A : Set} (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x : A} {xs : List A} → P x → All P xs → All P (x ∷ xs)

_ : All (_≤ 2) [ 0 , 1 , 2 ]
_ = z≤n ∷ s≤s z≤n ∷ s≤s (s≤s z≤n) ∷ []

-- Any

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

infix 4 _∈_ _∉_

_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

_∉_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∉ xs = ¬ (x ∈ xs)

_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
_ = here refl

_ : 0 ∈ [ 0 , 1 , 0 , 2 ]
_ = there (there (here refl))

not-in : 3 ∉ [ 0 , 1 , 0 , 2 ]
not-in (here ())
not-in (there (here ()))
not-in (there (there (here ())))
not-in (there (there (there (here ()))))
not-in (there (there (there (there ()))))

-- All and append

All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
  All P (xs ++ ys) ⇔ (All P xs × All P ys)
All-++-⇔ xs ys =
  record
    { to       =  to xs ys
    ; from     =  from xs ys
    }
  where
    to : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
      All P (xs ++ ys) → (All P xs × All P ys)
    to [] ys Pys = ⟨ [] , Pys ⟩
    to (x ∷ xs) ys (Px ∷ Pxs++ys) with to xs ys Pxs++ys
    ... | ⟨ Pxs , Pys ⟩ = ⟨ Px ∷ Pxs , Pys ⟩

    from : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
      All P xs × All P ys → All P (xs ++ ys)
    from [] ys ⟨ [] , Pys ⟩ = Pys
    from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩ =  Px ∷ from xs ys ⟨ Pxs , Pys ⟩

-- Decidability of All

all : ∀ {A : Set} → (A → Bool) → List A → Bool
all p = foldr _∧_ true ∘ map p

Decidable : ∀ {A : Set} → (A → Set) → Set
Decidable {A} P = ∀ (x : A) → Dec (P x)

All? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P)
All? P? []                                = yes []
All? P? (x ∷ xs) with P? x   | All? P? xs
...                 | yes Px | yes Pxs    = yes (Px ∷ Pxs)
...                 | no ¬Px | _          = no λ{ (Px ∷ Pxs) → ¬Px Px   }
...                 | _      | no ¬Pxs    = no λ{ (Px ∷ Pxs) → ¬Pxs Pxs }

ext: agda

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.IntConstruction where

open import Level

open import Data.Fin
open import Data.Product

open import Categories.Category
open import Categories.Product
open import Categories.Monoidal
open import Categories.Functor hiding (id; _∘_; identityʳ; assoc)
open import Categories.Monoidal.Braided
open import Categories.Monoidal.Helpers
open import Categories.Monoidal.Braided.Helpers
open import Categories.Monoidal.Symmetric
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation hiding (id)
open import Categories.Monoidal.Traced

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

record Polarized {o o' : Level} (A : Set o) (B : Set o') : Set (o ⊔ o') where
  constructor ±
  field
    pos : A
    neg : B

IntC : ∀ {o ℓ e}
       {C : Category o ℓ e} {M : Monoidal C} {B : Braided M} {S : Symmetric B} →
       (T : Traced S) → Category o ℓ e
IntC {o} {ℓ} {e} {C} {M} {B} {S} T = record {
    Obj = Polarized C.Obj C.Obj
  ; _⇒_ = λ { (± A+ A-) (± B+ B-) → C [ F.⊗ₒ (A+ , B-) , F.⊗ₒ (B+ , A-) ]}
  ; _≡_ = C._≡_
  ; _∘_ = λ { {(± A+ A-)} {(± B+ B-)} {(± C+ C-)} g f →
            T.trace { B- } {F.⊗ₒ (A+ , C-)} {F.⊗ₒ (C+ , A-)}
              (ηassoc⇐ (ternary C C+ A- B-) C.∘
               F.⊗ₘ (C.id , ηbraid (binary C B- A-)) C.∘
               ηassoc⇒ (ternary C C+ B- A-) C.∘
               F.⊗ₘ (g , C.id) C.∘
               ηassoc⇐ (ternary C B+ C- A-) C.∘
               F.⊗ₘ (C.id , ηbraid (binary C A- C-)) C.∘
               ηassoc⇒ (ternary C B+ A- C-) C.∘
               F.⊗ₘ (f , C.id) C.∘
               ηassoc⇐ (ternary C A+ B- C-) C.∘
               F.⊗ₘ (C.id , ηbraid (binary C C- B-)) C.∘
               ηassoc⇒ (ternary C A+ C- B-))}
  ; id = F.⊗ₘ (C.id , C.id)
  ; assoc = λ { {(± A+ A-)} {(± B+ B-)} {(± C+ C-)} {(± D+ D-)} {f} {g} {h} →
            {!!} }
  ; identityˡ = λ { {(± A+ A-)} {(± B+ B-)} {f} →
                (begin
                  {!!}
                ↓⟨ {!!} ⟩
                  f ∎) }
  ; identityʳ = λ { {(± A+ A-)} {(± B+ B-)} {f} →
                {!!} }
  ; equiv = C.equiv
  ; ∘-resp-≡ = λ { {(± A+ A-)} {(± B+ B-)} {(± C+ C-)} {f} {h} {g} {i} f≡h g≡i →
               {!!} }
  }
  where
    module C = Category C
    open C.HomReasoning
    module M = Monoidal M renaming (id to 𝟙)
    module F = Functor M.⊗ renaming (F₀ to ⊗ₒ; F₁ to ⊗ₘ)
    module B = Braided B
    module S = Symmetric S
    module T = Traced T
    module NIassoc = NaturalIsomorphism M.assoc
    open NaturalTransformation NIassoc.F⇒G renaming (η to ηassoc⇒)
    open NaturalTransformation NIassoc.F⇐G renaming (η to ηassoc⇐)
    module NIbraid = NaturalIsomorphism B.braid
    open NaturalTransformation NIbraid.F⇒G renaming (η to ηbraid)

IntConstruction : ∀ {o ℓ e}
  {C : Category o ℓ e} {M : Monoidal C} {B : Braided M} {S : Symmetric B} →
  (T : Traced S) →
  Σ[ IntC ∈ Category o ℓ e ]
  Σ[ MIntC ∈ Monoidal IntC ]
  Σ[ BIntC ∈ Braided MIntC ]
  Σ[ SIntC ∈ Symmetric BIntC ]
  Traced SIntC
IntConstruction = {!!}

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
module Reright where
  open import Prelude
  open import Tactic.Reflection.Reright
  open import Agda.Builtin.Reflection -- for better pretty-printing of error messages

  -- 'reright' presents the user with changed context variabes, to mimic that done by 'rewrite'.
  simple-reright-test₁ : (A B : Set) (F : Set → Set) → F A → A ≡ B → B → A
  simple-reright-test₁ A B F FA A≡B b = reright A≡B $ λ (FB : F B) → b

  -- the target of the reright (in this case x≡y₁) is excluded from the changed context variables
  simple-reright-test₂ : {a : Level} {A : Set a} {x y : A} (x≡y₁ : x ≡ y) (x≡y₂ : x ≡ y) → y ≡ x
  simple-reright-test₂ {y = y} x≡y₁ x≡y₂ = reright x≡y₁ λ (x≡y₂' : y ≡ y) → refl

  -- the visibility of context variables remains the same in their changed state
  simple-reright-test₃ : {a : Level} {A : Set a} {x y : A} (x≡y₁ : x ≡ y) (x≡y₂ : x ≡ y) {x≡y₃ : x ≡ y} → y ≡ x
  simple-reright-test₃ {y = y} x≡y₁ x≡y₂ {x≡y₃} = reright x≡y₁ λ (x≡y₂' : y ≡ y) {x≡y₃' : y ≡ y} → refl

  -- for some reason, when the first changed variable is hidden, it's impossible to bring it into scope
  {- FAILS - results in unsolved metas
    problematic-visibility : {a : Level} {A : Set a} {x y : A} (x≡y₁ : x ≡ y) {x≡y₃ : x ≡ y} → y ≡ x
    problematic-visibility {y = y} x≡y₁ {x≡y₃} = reright x≡y₁ λ {x≡y₃' : y ≡ y} → refl
  -}

  module Test₁ where
    postulate
      Set≡Set : Set ≡ Set
      A₀ : Set
      A₁ : A₀ → Set
      A₂ : (a₀ : A₀) → A₁ a₀ → Set
      A₃ : (a₀ : A₀) → (a₁ : A₁ a₀) → A₂ a₀ a₁ → Set
      B₀ : Set
      B₁ : B₀ → Set
      B₂ : (b₀ : B₀) → B₁ b₀ → Set
      B₃ : (b₀ : B₀) → (b₁ : B₁ b₀) → B₂ b₀ b₁ → Set
      A₀≡B₀ : A₀ ≡ B₀
      F : Set → Set
      C : (α : Level) (β : Level) → Set α → Set β
      𝑨₀¹ : A₀
      𝑨₀² : A₀
      𝑨₀¹≡𝑨₀² : 𝑨₀¹ ≡ 𝑨₀²
      𝑨₂𝑨₀²⋆ : (a₁𝑨₀² : A₁ 𝑨₀²) → A₂ 𝑨₀² a₁𝑨₀²
      𝑩₀ : B₀
      K₀ : A₀ → Set

    test₀ : (b₀¹ b₀² : B₀) (b₀¹≡b₀² : b₀¹ ≡ b₀²) → Set
    test₀ b₀¹ b₀² b₀¹≡b₀² with b₀¹≡b₀²
    test₀ b₀¹ b₀² b₀¹≡b₀² | b₀¹≡b₀²-with = let b₀¹≡b₀²-let = b₀¹≡b₀²-with in reright b₀¹≡b₀²-let {!!}

    test₁ : ∀ (a₀ : A₀) → a₀ ≡ a₀
    test₁ a₀ = id (reright A₀≡B₀ {!!})

    test₂ : A₀ → B₀
    test₂ a₀ = reright A₀≡B₀ (λ b₀ → 𝑩₀)

    test₃ : A₀ → B₀
    test₃ a₀ = reright Set≡Set (reright A₀≡B₀ (λ b₀ → 𝑩₀))

    test₄ : A₀ → B₀
    test₄ a₀ = reright Set≡Set (reright A₀≡B₀ (λ b₀ → reright A₀≡B₀ {!!}))

    test₅ : A₀ → B₀
    test₅ a₀ = reright Set≡Set 𝑩₀

    test₆ : A₀ → B₀
    test₆ a₀ = reright Set≡Set $ reright A₀≡B₀ $ {!!}

    test₇ : ∀ {α : Level}
            (a₀ : A₀)
            {β : Level}
            (X Y : Set (α ⊔ β))
            → X ≡ Y
            → Y ≡ X
    test₇ {α} a₀ {β} X Y X≡Y = id (reright X≡Y {!!})

    test₈ : (a₁𝑨₀¹ : A₁ 𝑨₀¹) → A₂ 𝑨₀¹ a₁𝑨₀¹
    test₈ a₁𝑨₀¹ = reright 𝑨₀¹≡𝑨₀² (λ a₁𝑨₀² → {!!})

    test₉ : (a₀¹ : A₀) (a₀² : A₀) (a₀¹≡a₀²-1 : a₀¹ ≡ a₀²) (a₁a₀¹ : A₁ a₀¹) (X : Set) (Y : Set) (a₀¹≡a₀²-2 : a₀¹ ≡ a₀²) → F (A₂ a₀¹ a₁a₀¹) → F (A₁ a₀¹) ≡ A₂ a₀¹ a₁a₀¹
    test₉ a₀¹ a₀² a₀¹≡a₀²-1 a₁a₀¹ X Y a₀¹≡a₀²-2 = reright a₀¹≡a₀²-1 {!!}

    module _ (A₂⋆ : (a₀ : A₀) (a₁a₀ : A₁ a₀) → A₂ a₀ a₁a₀) where
      test₁₀ : (a₀ : A₀) (a₁a₀¹ : A₁ a₀) (a₁a₀² : A₁ a₀) (a₁a₀¹≡a₁a₀² : a₁a₀¹ ≡ a₁a₀²) → A₂ a₀ a₁a₀¹
      test₁₀ a₀ a₁a₀¹ a₁a₀² a₁a₀¹≡a₁a₀² = reright a₁a₀¹≡a₁a₀² {!!}

    test₁₁ : (a₀¹ : A₀) (a₀² : A₀) (FA₁a₀¹≡FA₁a₀² : F (A₁ a₀¹) ≡ F (A₁ a₀²)) → F (A₁ a₀¹) → F (A₁ a₀¹) ≡ F (F (A₁ a₀¹))
    test₁₁ a₀¹ a₀² FA₁a₀¹≡FA₁a₀² = reright FA₁a₀¹≡FA₁a₀² {!!}

    test₁₂ : (a₀¹ : A₀) (a₀² : A₀) (FA₁a₀¹≡FA₁a₀² : F (A₁ a₀¹) ≡ F (A₁ a₀²)) → F (A₁ a₀¹) → F (A₁ a₀¹) ≡ F (F (A₁ a₀¹))
    test₁₂ a₀¹ a₀² FA₁a₀¹≡FA₁a₀² FA₁a₀¹ = reright FA₁a₀¹≡FA₁a₀² {!!}

    test₁₃ : (β : Level)
             (a₀¹ : A₀)
             (χ : Level)
             (a₀² : A₀)
             (CA₁a₀¹≡CA₁a₀² : C lzero (β ⊔ χ) (A₁ a₀¹) ≡ C lzero (β ⊔ χ) (A₁ a₀²)) →
             C lzero (β ⊔ χ) (A₁ a₀¹)
             → Nat → Σ _ λ γ → C lzero (β ⊔ χ) (A₁ a₀¹) ≡ C γ (β ⊔ χ) (C lzero γ (A₁ a₀¹))
    test₁₃ β a₀¹ χ a₀² CA₁a₀¹≡CA₁a₀² CA₁a₀¹ = reright CA₁a₀¹≡CA₁a₀² {!!}

    test₁₄ : (a₀ : A₀) (FFA₁a₀≡FA₁a₀ : F (F (A₁ a₀)) ≡ F (A₁ a₀)) → F (F (F (F (A₁ a₀))))
    test₁₄ a₀ FFA₁a₀≡FA₁a₀ = reright FFA₁a₀≡FA₁a₀ (reright FFA₁a₀≡FA₁a₀ (reright FFA₁a₀≡FA₁a₀ {!!}))

    test₁₅ : (a₀ : A₀) (FA₁a₀≡FFA₁a₀ : F (A₁ a₀) ≡ F (F (A₁ a₀))) → F (F (A₁ a₀))
    test₁₅ a₀ FA₁a₀≡FFA₁a₀ = reright FA₁a₀≡FFA₁a₀ (reright FA₁a₀≡FFA₁a₀ {!!})

    test₁₆ : (l : A₀ → Level → Level)
             (β : Level)
             (a₀² : A₀)
             (a₀¹ : A₀)
             (CA₁a₀¹≡CA₁a₀² : C lzero (l a₀¹ β) (A₁ a₀¹) ≡ C lzero (l a₀¹ β) (A₁ a₀²))
             → C lzero (l a₀¹ β) (A₁ a₀¹)
             → Σ _ λ γ → C lzero (l a₀¹ β) (A₁ a₀¹) ≡ C γ (l a₀¹ β) (C lzero γ (A₁ a₀¹))
    test₁₆ l β a₀² a₀¹ CA₁a₀¹≡CA₁a₀² CA₁a₀¹ = reright CA₁a₀¹≡CA₁a₀² {!!}

    test₁₇ : (a₀¹ : A₀)
             (a₀² : A₀)
             (K₀a₀¹ : K₀ a₀¹)
             (a₀¹≡a₀² : a₀¹ ≡ a₀²)
           → Set
    test₁₇ a₀¹ a₀² K₀a₀¹ a₀¹≡a₀² = reright a₀¹≡a₀² {!!}

    test₁₈ : (a₀¹ : A₀)
             (a₀² : A₀)
             (k₀a₀¹ : K₀ a₀¹)
             (FK₀a₀¹ : F (K₀ a₀¹))
             (K₀a₀¹≡K₀a₀² : K₀ a₀¹ ≡ K₀ a₀²)
           → F (F (K₀ a₀¹)) ≡ F (K₀ a₀²)
    test₁₈ a₀¹ a₀² k₀a₀¹ FK₀a₀¹ K₀a₀¹≡K₀a₀² = reright K₀a₀¹≡K₀a₀² {!!}

    test₁₉ : ∀ {a₀¹ : A₀}
               {a₀² : A₀}
               {a₁a₀²-1 a₁a₀²-2 a₁a₀²-3 : A₁ a₀²}
               {a₁a₀²-2=a₁a₀²-3 : A₂ a₀² a₁a₀²-2 ≡ A₂ a₀² a₁a₀²-3}
               (R : ∀ (a₀²' : A₀) → A₂ a₀² a₁a₀²-1 ≡ A₂ a₀² a₁a₀²-2)
               (X : A₂ a₀² a₁a₀²-2 ≡ A₂ a₀² a₁a₀²-3)
               {ignore : Set}
             → A₂ a₀² a₁a₀²-1 ≡ A₂ a₀² a₁a₀²-3
    test₁₉ {a₀¹} {a₀²} {a₁a₀²-1} {a₁a₀²-2} {a₁a₀²-3} {a₁a₀²-2=a₁a₀²-3} R X = reright (R a₀¹) {!!}

    {- FAILS (correctly, though perhaps without the most comprehensible of error messages)
      test₂₀' : (f₁ : A₀) (f₂ : A₀) (A₀f₁≡A₀f₂ : A₁ f₁ ≡ A₁ f₂) (g₁ : A₁ f₁) → A₂ f₁ g₁
      test₂₀' f₁ f₂ A₀f₁≡A₀f₂ g₁ rewrite A₀f₁≡A₀f₂ = {!!}

      test₂₀ : (f₁ : A₀) (f₂ : A₀) (A₀f₁≡A₀f₂ : A₁ f₁ ≡ A₁ f₂) (g₁ : A₁ f₁) → A₂ f₁ g₁
      test₂₀ f₁ f₂ A₀f₁≡A₀f₂ g₁ = reright A₀f₁≡A₀f₂ {!!}
    -}

    test₂₀ : ∀ {a b : Level} {A : Set a} {x y : A} (x≡y : x ≡ y) → Set
    test₂₀ x≡y = reright x≡y {!!}

    test₂₁ : ∀ {a b : Level} {A : Set a} {x y : A} (B : Set b) (x≡y : x ≡ y) → Set
    test₂₁ B x≡y = reright x≡y {!!}

    test₂₂ : ∀ {a : Level} {A : Set a} {B : Set} {x : B} {y : B} (x≡y : x ≡ y) → Set
    test₂₂ x≡y = reright x≡y {!!}

    module _ (l : Level) where
      postulate P : Set

      test₂₃ : (p : P)
               (A : Set)
               (x y : A)
               (x≡y : x ≡ y)
               → Set
      test₂₃ _ _ _ _ x≡y = reright x≡y ?

  module Test₂ where
    record Map
             {K : Set}
             (V : K → Set)
             (Carrier : Nat → Set) {{isDecEquivalence/K : Eq K}} {{isDecEquivalence/V : (k : K) → Eq (V k)}} : Set₁ where
      field
        ∅ : Carrier 0
        _∉_ : ∀ {s} → K → Carrier s → Set
        ∅-is-empty : ∀ {𝑘} {∅ : Carrier 0} → 𝑘 ∉ ∅

      _∈_ : ∀ {s} → K → Carrier s → Set
      _∈_ k m = ¬ k ∉ m

      field
        get : ∀ {k : K} {s} {m : Carrier s} → k ∈ m → V k
        put : ∀ {k₀ : K} (v₀ : V k₀) {s₁} {m₁ : Carrier s₁} → k₀ ∉ m₁ → Σ _ λ (m₀ : Carrier (suc s₁)) → Σ _ λ (k₀∈m₀ : k₀ ∈ m₀) → get k₀∈m₀ ≡ v₀

    postulate
      A : Set

    V : A → Set
    V = λ _ → Nat

    postulate
      M : Nat → Set
      isDecEquivalence/A : Eq A
      isDecEquivalence/V : (a : A) → Eq (V a)

    postulate
      m : Map V M {{isDecEquivalence/A}} {{isDecEquivalence/V}}

    open Map m

    test₁ : (v : Nat) (k : A)
      → (k∈putkv∅ : k ∈ (fst $ put {k₀ = k} v {m₁ = ∅} ∅-is-empty))
      → Set
    test₁ v k k∈putkv∅ = let p = (put {k₀ = k} v {m₁ = ∅} ∅-is-empty) in let r = sym (snd $ snd p) in reright r {!!}

{- expected.out
?0 : b₀² ≡ b₀² → Set
?1 : (b : B₀) → b ≡ b
?2 : B₀ → B₀
?3 : B₀ → B₀
?4 : Y ≡ Y
?5 : A₂ 𝑨₀² a₁𝑨₀²
?6 : (a₁ : A₁ a₀²) → a₀² ≡ a₀² → F (A₂ a₀² a₁) → F (A₁ a₀²) ≡ A₂ a₀² a₁
?7 : A₂ a₀ a₁a₀²
?8 : F (A₁ a₀²) → F (A₁ a₀²) ≡ F (F (A₁ a₀²))
?9 : F (A₁ a₀²) → F (A₁ a₀²) ≡ F (F (A₁ a₀²))
?10 : C lzero (χ ⊔ β) (A₁ a₀²) →
Nat →
Σ Level
(λ γ → C lzero (χ ⊔ β) (A₁ a₀²) ≡ C γ (χ ⊔ β) (C lzero γ (A₁ a₀¹)))
?11 : F (A₁ a₀)
?12 : F (F (F (F (A₁ a₀))))
?13 : C lzero (l a₀¹ β) (A₁ a₀²) →
Σ Level
(λ γ →
   C lzero (l a₀¹ β) (A₁ a₀²) ≡ C γ (l a₀¹ β) (C lzero γ (A₁ a₀¹)))
?14 : K₀ a₀² → Set
?15 : K₀ a₀² → F (K₀ a₀²) → F (F (K₀ a₀²)) ≡ F (K₀ a₀²)
?16 : (A₀ → A₂ a₀² a₁a₀²-2 ≡ A₂ a₀² a₁a₀²-2) →
A₂ a₀² a₁a₀²-2 ≡ A₂ a₀² a₁a₀²-3
?17 : Set
?18 : Set
?19 : Set
?20 : Set
?21 : (k ∉ fst (put (get (fst (snd (put v ∅-is-empty)))) ∅-is-empty) →
 ⊥) →
Set
-}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists made up entirely of unique elements (setoid equality)
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid)

module Data.List.Relation.Unary.Unique.Setoid {a ℓ} (S : Setoid a ℓ) where

open Setoid S renaming (Carrier to A)

open import Data.List.Base
import Data.List.Relation.Unary.AllPairs as AllPairsM
open import Level using (_⊔_)
open import Relation.Unary using (Pred)
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- Definition

private

  Distinct : Rel A ℓ
  Distinct x y = ¬ (x ≈ y)

open import Data.List.Relation.Unary.AllPairs.Core Distinct
     renaming (AllPairs to Unique)
     public

open import Data.List.Relation.Unary.AllPairs {R = Distinct}
     using (head; tail)
     public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Equality over lists using propositional equality
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where

open import Data.List
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Publically re-export everything from setoid equality

open SetoidEquality (setoid A) public

------------------------------------------------------------------------
-- ≋ is propositional

≋⇒≡ : _≋_ ⇒ _≡_
≋⇒≡ []             = refl
≋⇒≡ (refl ∷ xs≈ys) = cong (_ ∷_) (≋⇒≡ xs≈ys)

≡⇒≋ : _≡_ ⇒ _≋_
≡⇒≋ refl = ≋-refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Unary.Any.Properties directly.
------------------------------------------------------------------------

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

module Data.List.Relation.BagAndSetEquality where

open import Data.List.Relation.Binary.BagAndSetEquality public


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

open import HoTT
open import homotopy.RibbonCover

module experimental.CoverClassification2 {i} (X : Ptd i)
  (A-conn : is-connected 0 (de⊙ X)) where

  private
    A = de⊙ X
    a = pt X

  open Cover
  open import homotopy.CoverClassification X A-conn

  {-
      Universality of the covering generated by the fundamental group itself.
  -}

  -- FIXME What's the established terminology for this?
  canonical-gset : Gset (πS 0 X) i
  canonical-gset = record
    { El = a =₀ a
    ; El-level = Trunc-level
    ; gset-struct = record
      { act = _∙₀_
      ; unit-r = ∙₀-unit-r
      ; assoc = ∙₀-assoc
      }
    }

  -- FIXME What's the established terminology for this?
  canonical-cover : Cover A i
  canonical-cover = gset-to-cover canonical-gset

{-
  private
    module CanonicalIsUniversal where
      open covering canonical-covering
      open gset canonical-gset

      center′ : ∀ a → Σ A fiber
      center′ a = (a , trace {gs = act} refl₀ refl₀)

      center : τ ⟨1⟩ (Σ A fiber)
      center = proj center′

      private
        -- An ugly lemma for this development only
        trans-fiber≡cst-proj-Σ-eq : ∀ {i} (P : Set i) (Q : P → Set i)
          (a : P) (c : Σ P Q) {b₁ b₂} (p : b₁ ≡ b₂) (q : a ≡ π₁ c)
          (r : transport Q q b₁ ≡ π₂ c)
          → transport (λ r → (a , r) ≡₀ c) p (proj $ Σ-eq q r)
          ≡ proj (Σ-eq q (ap (transport Q q) (! p) ∘ r))
        trans-fiber≡cst-proj-Σ-eq P Q a c refl q r = refl

      abstract
        path-trace-fiber : ∀ {a₂} y (p : a ≡ a₂)
          → transport fiber (! p ∘ ! y) (trace (proj y) (proj p))
          ≡ trace refl₀ refl₀
        path-trace-fiber y refl =
          transport fiber (! y) (trace (proj y) refl₀)
            ≡⟨ trans-trace act (! y) (proj y) refl₀ ⟩
          trace (proj y) (proj $ ! y)
            ≡⟨ paste refl₀ (proj y) (proj $ ! y) ⟩
          trace refl₀ (proj $ y ∘ ! y)
            ≡⟨ ap (trace refl₀ ◯ proj) $ opposite-right-inverse y ⟩∎
          trace refl₀ refl₀
            ∎

      path-trace : ∀ {a₂} y p → (a₂ , trace {act = act} y p) ≡₀ center′
      path-trace {a₂} =
        π₀-extend ⦃ λ y → Π-is-set λ p → π₀-is-set ((a₂ , trace y p) ≡ center′) ⦄
          (λ y → π₀-extend ⦃ λ p → π₀-is-set ((a₂ , trace (proj y) p) ≡ center′) ⦄
            (λ p → proj $ Σ-eq (! p ∘ ! y) (path-trace-fiber y p)))

      abstract
        path-paste′ : ∀ {a₂} y loop p
          → transport (λ r → (a₂ , r) ≡₀ center′) (paste (proj y) (proj loop) (proj p))
              (path-trace (proj $ y ∘ loop) (proj p))
          ≡ path-trace (proj y) (proj $ loop ∘ p)
        path-paste′ y loop refl =
          transport (λ r → (a , r) ≡₀ center′) (paste (proj y) (proj loop) refl₀)
            (proj $ Σ-eq (! (y ∘ loop)) (path-trace-fiber (y ∘ loop) refl))
              ≡⟨ trans-fiber≡cst-proj-Σ-eq A fiber a center′
                    (paste (proj y) (proj loop) refl₀)
                    (! (y ∘ loop)) (path-trace-fiber (y ∘ loop) refl) ⟩
          proj (Σ-eq (! (y ∘ loop)) _)
              ≡⟨ ap proj $
                  ap2 (λ p q → Σ-eq p q)
                    (! (y ∘ loop)
                      ≡⟨ opposite-concat y loop ⟩
                    ! loop ∘ ! y
                      ≡⟨ ap (λ x → ! x ∘ ! y) $ ! $ refl-right-unit loop ⟩∎
                    ! (loop ∘ refl) ∘ ! y
                      ∎)
                    (prop-has-all-paths (ribbon-is-set a _ _) _ _) ⟩∎
          proj (Σ-eq (! (loop ∘ refl) ∘ ! y) (path-trace-fiber y (loop ∘ refl)))
              ∎

      abstract
        path-paste : ∀ {a₂} y loop p
          → transport (λ r → (a₂ , r) ≡₀ center′) (paste y loop p)
              (path-trace (y ∘₀ loop) p)
          ≡ path-trace y (loop ∘₀ p)
        path-paste {a₂} =
          π₀-extend ⦃ λ y → Π-is-set λ loop → Π-is-set λ p → ≡-is-set $ π₀-is-set _ ⦄
            (λ y → π₀-extend ⦃ λ loop → Π-is-set λ p → ≡-is-set $ π₀-is-set _ ⦄
              (λ loop → π₀-extend ⦃ λ p → ≡-is-set $ π₀-is-set _ ⦄
                (λ p → path-paste′ y loop p)))

      path′ : (y : Σ A fiber) → proj {n = ⟨1⟩} y ≡ center
      path′ y = τ-path-equiv-path-τ-S {n = ⟨0⟩} ☆
        ribbon-rec {act = act} (π₁ y)
          (λ r → (π₁ y , r) ≡₀ center′)
          ⦃ λ r → π₀-is-set ((π₁ y , r) ≡ center′) ⦄
          path-trace
          path-paste
          (π₂ y)

      path : (y : τ ⟨1⟩ (Σ A fiber)) → y ≡ center
      path = τ-extend {n = ⟨1⟩} ⦃ λ _ → ≡-is-truncated ⟨1⟩ $ τ-is-truncated ⟨1⟩ _ ⦄ path′

  canonical-covering-is-universal : is-universal canonical-covering
  canonical-covering-is-universal = Universality.center , Universality.path

  -- The other direction:  If a covering is universal, then the fiber
  -- is equivalent to the fundamental group.
  module _ (cov : covering) (cov-is-universal : is-universal cov) where
    open covering cov
    open action (covering⇒action cov)

    -- We need a point!
    module GiveMeAPoint (center : fiber a) where

      -- Goal: fiber a <-> fundamental group

      fiber-a⇒fg : fiber a → a ≡₀ a
      fiber-a⇒fg y = ap₀ π₁ $ connected-has-all-τ-paths
        cov-is-universal (a , center) (a , y)

      fg⇒fiber-a : a ≡₀ a → fiber a
      fg⇒fiber-a = tracing cov center

      fg⇒fiber-a⇒fg : ∀ p → fiber-a⇒fg (fg⇒fiber-a p) ≡ p
      fg⇒fiber-a⇒fg = π₀-extend ⦃ λ _ → ≡-is-set $ π₀-is-set _ ⦄ λ p →
        ap₀ π₁ (connected-has-all-τ-paths
          cov-is-universal (a , center) (a , transport fiber p center))
            ≡⟨ ap (ap₀ π₁)
                  $ ! $ π₂ (connected-has-connected-paths cov-is-universal _ _)
                           (proj $ Σ-eq p refl) ⟩
        ap₀ π₁ (proj $ Σ-eq p refl)
            ≡⟨ ap proj $ base-path-Σ-eq p refl ⟩∎
        proj p
            ∎

      fiber-a⇒fg⇒fiber-a : ∀ y → fg⇒fiber-a (fiber-a⇒fg y) ≡ y
      fiber-a⇒fg⇒fiber-a y = π₀-extend
        ⦃ λ p → ≡-is-set {x = tracing cov center (ap₀ π₁ p)} {y = y}
                  $ fiber-is-set a ⦄
        (λ p →
          transport fiber (base-path p) center
            ≡⟨ trans-base-path p ⟩∎
          y
            ∎)
        (connected-has-all-τ-paths cov-is-universal (a , center) (a , y))

      fiber-a≃fg : fiber a ≃ (a ≡₀ a)
      fiber-a≃fg = fiber-a⇒fg , iso-is-eq _ fg⇒fiber-a
        fg⇒fiber-a⇒fg fiber-a⇒fg⇒fiber-a

    -- This is the best we can obtain, because there is no continuous
    -- choice of the center.
    [center] : [ fiber a ]
    [center] = τ-extend-nondep
      ⦃ prop-is-gpd []-is-prop ⦄
      (λ y → []-extend-nondep
        ⦃ []-is-prop ⦄
        (proj ◯ λ p → transport fiber p (π₂ y))
        (connected-has-all-τ-paths A⋆-is-conn (π₁ y) a))
      (π₁ cov-is-universal)

    -- [ isomorphism between the fiber and the fundamental group ]
    -- This is the best we can obtain, because there is no continuous
    -- choice of the center.
    [fiber-a≃fg] : [ fiber a ≃ (a ≡₀ a) ]
    [fiber-a≃fg] = []-extend-nondep ⦃ []-is-prop ⦄
      (proj ◯ GiveMeAPoint.fiber-a≃fg) [center]

-}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Andreas, 2015-02-07

postulate
  X Y : Set
  fix : (X → X) → X
  g   : Y → X → X
  y   : Y
  P   : X → Set
  yes : (f : X → X) → P (f (fix f))

test : P (g y (fix (g y)))
test with g y
test | f = yes f

-- should be able to abstract (g y) twice
-- and succeed

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Categories.Category
open import Categories.Functor

module Categories.Diagram.Limit.Properties
       {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′}  where

open import Categories.Diagram.Cone.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; module ≃)
open import Categories.Morphism.Reasoning C
open import Categories.Morphism C

import Categories.Category.Construction.Cones as Con
import Categories.Diagram.Limit as Lim

private
  module J = Category J
  module C = Category C

  open C
  variable
    X Y Z : Obj
    f g h : X ⇒ Y

open HomReasoning

-- natural isomorphisms respects limits
module _ {F G : Functor J C} (F≃G : F ≃ G) where
  private
    module F  = Functor F
    module G  = Functor G
    module LF = Lim F
    module LG = Lim G
    open NaturalIsomorphism F≃G

  ≃-resp-lim : LF.Limit → LG.Limit
  ≃-resp-lim L = record
    { terminal = record
      { ⊤        = record
        { apex = record
          { ψ       = λ j → ⇒.η j ∘ proj j
          ; commute = λ {X Y} f → begin
            G.F₁ f ∘ ⇒.η X ∘ proj X   ≈⟨ pullˡ (⇒.sym-commute f) ⟩
            (⇒.η Y ∘ F.F₁ f) ∘ proj X ≈⟨ pullʳ (limit-commute f) ⟩
            ⇒.η Y ∘ proj Y            ∎
          }
        }
      ; ⊤-is-terminal = record
        { !        = λ {A} → record
          { arr     = rep (nat-map-Cone F⇐G A)
          ; commute = λ {j} → assoc ○ ⟺ (switch-tofromˡ (record { iso = iso j }) (⟺ commute))
          }
        ; !-unique = λ {K} f →
          let module f = Con.Cone⇒ G f
          in terminal.!-unique record
            { arr     = f.arr
            ; commute = λ {j} → switch-fromtoˡ (record { iso = iso j }) (sym-assoc ○ f.commute)
            }
        }
      }
    }
    where open LF.Limit L

  ≃⇒Cone⇒ : ∀ (Lf : LF.Limit) (Lg : LG.Limit) → Con.Cones G [ LG.Limit.limit (≃-resp-lim Lf) , LG.Limit.limit Lg ]
  ≃⇒Cone⇒ Lf Lg = rep-cone (LG.Limit.limit (≃-resp-lim Lf))
    where open LG.Limit Lg

≃⇒lim≅ : ∀ {F G : Functor J C} (F≃G : F ≃ G) (Lf : Lim.Limit F) (Lg : Lim.Limit G) → Lim.Limit.apex Lf ≅ Lim.Limit.apex Lg
≃⇒lim≅ {F = F} {G} F≃G Lf Lg = record
  { from = arr (≃⇒Cone⇒ F≃G Lf Lg)
  ; to   = arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)
  ; iso  = record
    { isoˡ = Lf.terminal.⊤-id record
      { commute = λ {j} → begin
        Lf.proj j ∘ arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf) ∘ arr (≃⇒Cone⇒ F≃G Lf Lg) ≈⟨ pullˡ (⇒-commute (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)) ⟩
        (⇐.η j ∘ Lg.proj j) ∘ arr (≃⇒Cone⇒ F≃G Lf Lg)                         ≈⟨ pullʳ (⇒-commute (≃⇒Cone⇒ F≃G Lf Lg)) ⟩
        ⇐.η j ∘ ⇒.η j ∘ Lf.proj j                                             ≈⟨ cancelˡ (iso.isoˡ j) ⟩
        Lf.proj j                                                             ∎
      }
    ; isoʳ = Lg.terminal.⊤-id record
      { commute = λ {j} → begin
        Lg.proj j ∘ arr (≃⇒Cone⇒ F≃G Lf Lg) ∘ arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf) ≈⟨ pullˡ (⇒-commute (≃⇒Cone⇒ F≃G Lf Lg)) ⟩
        (⇒.η j ∘ Lf.proj j) ∘ arr (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)                 ≈⟨ pullʳ (⇒-commute (≃⇒Cone⇒ (≃.sym F≃G) Lg Lf)) ⟩
        ⇒.η j ∘ ⇐.η j ∘ Lg.proj j                                             ≈⟨ cancelˡ (iso.isoʳ j) ⟩
        Lg.proj j                                                             ∎
      }
    }
  }
  where open Con.Cone⇒ renaming (commute to ⇒-commute)
        module Lf = Lim.Limit Lf
        module Lg = Lim.Limit Lg
        open NaturalIsomorphism F≃G

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:
open import lib
open import sum

module grammar (form : Set)(_eq_ : form → form → 𝔹)(drop-form : (x y : form) → x ≡ y → x eq y ≡ tt)(rise-form : (x y : form) → x eq y ≡ tt → x ≡ y) where

infix 7 _⇒_

data production : Set where
  _⇒_ : form → 𝕃 (form ⊎ char) → production

record grammar {numprods : ℕ} : Set where
  constructor  _,_
  field
    start : form
    prods : 𝕍 production numprods

open grammar

splice : ℕ → 𝕃 (form ⊎ char) → form → 𝕃 (form ⊎ char) → 𝕃 (form ⊎ char)
splice x [] _ _ = []
splice 0 ((inj₁ s) :: ss) s' ss' with s eq s'
... | tt = ss' ++ ss
... | ff = (inj₁ s) :: ss
splice 0 (x :: ss) s' ss' = x :: ss
splice (suc n) (s :: ss) s' ss' = s :: splice n ss s' ss'

𝕃inj₂ : ∀{ℓ ℓ'}{B : Set ℓ}{A : Set ℓ'} → 𝕃 A → 𝕃 (B ⊎ A)
𝕃inj₂ (x :: xs) = (inj₂ x) :: 𝕃inj₂ xs
𝕃inj₂ [] = []

𝕃inj₁ : ∀{ℓ ℓ'}{B : Set ℓ}{A : Set ℓ'} → 𝕃 A → 𝕃 (A ⊎ B)
𝕃inj₁ (x :: xs) = (inj₁ x) :: 𝕃inj₁ xs
𝕃inj₁ [] = []

data derivation{numprods : ℕ} {g : grammar{numprods}} : 𝕃 (form ⊎ char) → 𝕃 char → Set where
  end : {ss : 𝕃 char} → derivation (𝕃inj₂ ss) ss
  step : ∀ {ss1 ss1' : 𝕃 (form ⊎ char)}{ss2 : 𝕃 char}{s : form}{ss : 𝕃 (form ⊎ char)} →
           (m n : ℕ) → (p : n < numprods ≡ tt) →
           nth𝕍 n p (prods g) ≡ (s ⇒ ss) →
           m < length ss1 ≡ tt →
           splice m ss1 s ss ≡ ss1' →
           derivation {g = g} ss1' ss2 →
           derivation ss1 ss2

splice-concat : ∀{l1 l2 target final : 𝕃 (form ⊎ char)}{n : ℕ}{slice : form} → splice n l1 slice target ≡ final → splice (n + (length l2)) (l2 ++ l1) slice target ≡ l2 ++ final
splice-concat{l2 = []}{n = n} pr rewrite +0 n = pr
splice-concat{l1}{x :: xs}{n = n} pr rewrite +suc n (length xs) | splice-concat{l1}{l2 = xs} pr = refl

_=form⊎char_ : (x y : form ⊎ char) → 𝔹
_=form⊎char_ = =⊎ _eq_ _=char_

form⊎char-drop : (x y : form ⊎ char) → x ≡ y → x =form⊎char y ≡ tt
form⊎char-drop = ≡⊎-to-= _eq_ _=char_ drop-form ≡char-to-=

form⊎char-rise : (x y : form ⊎ char) → x =form⊎char y ≡ tt → x ≡ y
form⊎char-rise = =⊎-to-≡ _eq_ _=char_ rise-form =char-to-≡

splice-concat2 : ∀{l1 l2 target final : 𝕃 (form ⊎ char)}{n : ℕ}{slice : form} → splice n l1 slice target ≡ final → n < length l1 ≡ tt → splice n (l1 ++ l2) slice target ≡ final ++ l2
splice-concat2{[]}{n = n} pr1 pr2 rewrite <-0 n = 𝔹-contra pr2
splice-concat2{inj₁ x :: xs}{l2}{target}{n = 0}{slice} pr1 pr2 with x eq slice
...| tt rewrite (sym pr1) | ++[] target | ++-assoc target xs l2 = refl
...| ff rewrite (sym pr1) = refl
splice-concat2{inj₂ x :: xs}{l2}{target}{n = 0}{slice} pr1 pr2 rewrite (sym pr1) = refl
splice-concat2{x :: xs}{l2}{target}{[]}{suc n} pr1 pr2 with pr1
...| ()
splice-concat2{x :: xs}{l2}{target}{f :: fs}{suc n}{slice} pr1 pr2 with =𝕃-from-≡ _=form⊎char_ form⊎char-drop pr1
...| s1 rewrite splice-concat2{xs}{l2}{target}{fs}{n}{slice} (≡𝕃-from-={l1 = splice n xs slice target}{fs} _=form⊎char_ form⊎char-rise (&&-snd{x =form⊎char f} s1)) pr2 | form⊎char-rise x f (&&-fst{x =form⊎char f} s1) = refl

length+ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → length (l1 ++ l2) ≡ length l1 + length l2
length+ [] l2 = refl
length+ (x :: xs) l2 rewrite length+ xs l2 = refl

<-h1 : ∀{x y a : ℕ} → x < y ≡ tt → x + a < y + a ≡ tt
<-h1{x}{y}{0} p rewrite +0 x | +0 y = p
<-h1{x}{y}{suc n} p rewrite +suc y n | +suc x n = <-h1{x}{y}{n} p

<-h2 : ∀{a x y : ℕ} → a < x ≡ tt → a < x + y ≡ tt
<-h2{a}{x}{0} p rewrite +0 x = p
<-h2{a}{x}{suc y} p rewrite +suc x y with <-h2{a}{x}{y} p | <-suc (x + y)
...| pr1 | pr2 = <-trans{a}{x + y}{suc (x + y)} pr1 pr2

length𝕃inj₂ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (l : 𝕃 A) → length (𝕃inj₂{B = B} l) ≡ length l
length𝕃inj₂{B = B} (x :: xs) rewrite length𝕃inj₂{B = B} xs = refl
length𝕃inj₂ [] = refl

𝕃inj₂++ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (l1 l2 : 𝕃 A) → 𝕃inj₂{B = B} (l1 ++ l2) ≡ 𝕃inj₂ l1 ++ 𝕃inj₂ l2
𝕃inj₂++ [] l2 = refl
𝕃inj₂++{B = B} (x :: xs) l2 rewrite 𝕃inj₂++{B = B} xs l2 = refl

infixr 10 _deriv++_

_deriv++_ : {l2 l4 : 𝕃 char}{l1 l3 : 𝕃 (form ⊎ char)}{n : ℕ}{gr : grammar{n}} → derivation{g = gr} l1 l2 → derivation{g = gr} l3 l4 → derivation{g = gr} (l1 ++ l3) (l2 ++ l4)
_deriv++_{l2}{l4} end end rewrite sym (𝕃inj₂++{B = form} l2 l4) = end
_deriv++_{l2}{l4}{l1}{l3} f (step{ss1' = ss1'}{s = s}{ss} a b pr1 pr2 pr3 pr4 next) with <-h1{a}{length l3}{length l1} pr3
...| pr5 rewrite +comm (length l3) (length l1) | (sym (length+ l1 l3)) =  step{ss1 = l1 ++ l3}{l1 ++ ss1'}{l2 ++ l4} (a + (length l1)) b pr1 pr2 pr5 (splice-concat{l3}{l1} pr4) (_deriv++_ f next)
_deriv++_{l2}{l4}{l1} (step{ss1' = ss1'}{s = s}{ss} a b pr1 pr2 pr3 pr4 next) end with <-h2{a}{length l1}{length (𝕃inj₂{B = form} l4)} pr3
...| pr5 rewrite sym (length+ l1 (𝕃inj₂ l4)) = step{ss1 = l1 ++ 𝕃inj₂ l4}{ss1' ++ 𝕃inj₂ l4}{l2 ++ l4} a b pr1 pr2 pr5 (splice-concat2{l1}{𝕃inj₂ l4} pr4 pr3) (_deriv++_ next end)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Issue203 where

open import Common.Level

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

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Eq.KleeneTheory where

open import Prelude
open import T
open import Eq.Defs
open import Eq.LogicalTheory
open import Eq.KleeneTheoryEarly public

-- Harper says that Kleene equality is "evidently reflexive",
-- but this requires/implies termination!
-- We pick it directly from the consistency and reflexivity of
-- logical equivalence.
-- We could also prove it using halting, which we could prove from
-- either our HT result or from reflexivity of logical equivalence.
-- This is a bit simpler.
kleene-refl : Reflexive KleeneEq
kleene-refl {e} = ological-consistent (ological-refl e)

-- For kicks, we'll prove halting for closed nats.
nats-halt : (n : TNat) → THalts n
nats-halt n with kleene-refl {n}
... | kleeneq _ val E1 _ = halts E1 val

kleene-is-equivalence : IsEquivalence KleeneEq
kleene-is-equivalence = record { refl_ = kleene-refl
                               ; sym_ = kleene-sym
                               ; trans_ = kleene-trans }

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


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

module Dodo.Binary.Irreflexive where

-- Stdlib imports
open import Level using (Level)
open import Relation.Binary using (Rel; Irreflexive)
-- Local imports
open import Dodo.Binary.Equality

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {≈ : Rel A ℓ₁} {P : Rel A ℓ₂} {Q : Rel A ℓ₃} where

  irreflexive-⊆₂ : Irreflexive ≈ Q → P ⊆₂ Q → Irreflexive ≈ P
  irreflexive-⊆₂ irreflexiveQ P⊆Q x≈y Pxy = irreflexiveQ x≈y (⊆₂-apply P⊆Q Pxy)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
-- Andreas, 2017-01-20, issue #1817 is fixed

open import Agda.Builtin.Size
open import Agda.Builtin.Nat renaming (Nat to ℕ)

-- Function

_$_ : ∀{a b}{A : Set a}{B : Set b} →(A → B) → A →  B
f $ x = f x

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

-- Size

data SizeLt (i : Size) : Set where
  size : (j : Size< i) → SizeLt i

getSize : ∀{i} → SizeLt i → Size
getSize (size j) = j

-- List

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

for : ∀{A B} (xs : List A) (f : A → B) → List B
for [] f = []
for (x ∷ xs) f = f x ∷ for xs f

-- BT

data Var : (n : ℕ) → Set where
  vz : ∀{n} → Var (suc n)
  vs : ∀{n} → (x : Var n) → Var (suc n)

mutual
  record BT (i : Size) (n : ℕ) : Set where
    inductive; constructor Λ
    field nabs : ℕ
          var  : Var (nabs + n)
          args : List (BT' i (nabs + n))

  record BT' (i : Size) (n : ℕ) : Set where
    coinductive; constructor delay
    field force : ∀{j : SizeLt i} → BT (getSize j) n

open BT'

-- Renaming

data Ope : (n m : ℕ) → Set where
  id   : ∀{n} → Ope n n
  weak : ∀{n m} (ρ : Ope n m) → Ope (1 + n) m
  lift : ∀{n m} (ρ : Ope n m) → Ope (1 + n) (1 + m)

lifts : ∀ k {n m} (ρ : Ope n m) → Ope (k + n) (k + m)
lifts 0       ρ = ρ
lifts (suc k) ρ = lift (lifts k ρ)

renVar : ∀{n m} (ρ : Ope n m) (x : Var m) → Var n
renVar id       x      = x
renVar (weak ρ) x      = vs (renVar ρ x)
renVar (lift ρ) vz     = vz
renVar (lift ρ) (vs x) = vs (renVar ρ x)

ren  : ∀{i n m} (ρ : Ope n m) (t : BT i m) → BT i n
ren {i} ρ₀ (Λ n x ts) = Λ n (renVar ρ x) $ for ts \ t → delay
   \{ {size j} → ren {j} ρ $ force t {size j} }
  where ρ = lifts n ρ₀


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax CTLC | ΛC

type
  N   : 0-ary
  _↣_ : 2-ary | r30
  ¬_  : 1-ary | r30

term
  app    : α ↣ β  α  ->  β | _$_ l20
  lam    : α.β  ->  α ↣ β | ƛ_ r10
  throw  : α  ¬ α  ->  β
  callcc : ¬ α.α  ->  α

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
-}

module CTLC.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import CTLC.Signature
open import CTLC.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution ΛC:Syn
open import SOAS.Metatheory.SecondOrder.Equality ΛC:Syn

private
  variable
    α β γ τ : ΛCT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ ΛC) α Γ → (𝔐 ▷ ΛC) α Γ → Set where
  ƛβ : ⁅ α ⊩ β ⁆ ⁅ α ⁆̣ ▹ ∅ ⊢ (ƛ 𝔞⟨ x₀ ⟩) $ 𝔟 ≋ₐ 𝔞⟨ 𝔟 ⟩
  ƛη : ⁅ α ↣ β ⁆̣       ▹ ∅ ⊢      ƛ (𝔞 $ x₀) ≋ₐ 𝔞

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

postulate
  A : Set
  B : A → Set

-- fine
record R₀ : Set where
  field
    @0 x : A
    @0 y : B x

-- bad
record R : Set where
  field
    @0 x : A
    y : B x


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.NaturalTransformation.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism renaming (iso to iIso)
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Functor.Properties
open import Cubical.Categories.Commutativity
open import Cubical.Categories.Morphism renaming (isIso to isIsoC)

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
  -- syntax for sequencing in category D
  infixl 15 _⋆ᴰ_
  private
    _⋆ᴰ_ : ∀ {x y z} (f : D [ x , y ]) (g : D [ y , z ]) → D [ x , z ]
    f ⋆ᴰ g = f ⋆⟨ D ⟩ g

  open Precategory
  open Functor

  -- type aliases because it gets tedious typing it out all the time
  N-ob-Type : (F G : Functor C D) → Type _
  N-ob-Type F G = (x : C .ob) → D [(F .F-ob x) , (G .F-ob x)]

  N-hom-Type : (F G : Functor C D) → N-ob-Type F G → Type _
  N-hom-Type F G ϕ = {x y : C .ob} (f : C [ x , y ]) → (F .F-hom f) ⋆ᴰ (ϕ y) ≡ (ϕ x) ⋆ᴰ (G .F-hom f)

  record NatTrans (F G : Functor C D) : Type (ℓ-max (ℓ-max ℓC ℓC') ℓD') where
    constructor natTrans
    field
      -- components of the natural transformation
      N-ob : N-ob-Type F G
      -- naturality condition
      N-hom :  N-hom-Type F G N-ob

  record NatIso (F G : Functor C D): Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
    field
      trans : NatTrans F G
    open NatTrans trans

    field
      nIso : ∀ (x : C .ob) → isIsoC {C = D} (N-ob x)

    open isIsoC

    -- the three other commuting squares
    sqRL : ∀ {x y : C .ob} {f : C [ x , y ]}
         → F ⟪ f ⟫ ≡ (N-ob x) ⋆ᴰ G ⟪ f ⟫ ⋆ᴰ (nIso y) .inv
    sqRL {x} {y} {f} = invMoveR (isIso→areInv (nIso y)) (N-hom f)

    sqLL : ∀ {x y : C .ob} {f : C [ x , y ]}
         → G ⟪ f ⟫ ⋆ᴰ (nIso y) .inv ≡ (nIso x) .inv ⋆ᴰ F ⟪ f ⟫
    sqLL {x} {y} {f} = invMoveL (isIso→areInv (nIso x)) (sym sqRL')
      where
        sqRL' : F ⟪ f ⟫ ≡ (N-ob x) ⋆ᴰ ( G ⟪ f ⟫ ⋆ᴰ (nIso y) .inv )
        sqRL' = sqRL ∙ (D .⋆Assoc _ _ _)

    sqLR : ∀ {x y : C .ob} {f : C [ x , y ]}
         → G ⟪ f ⟫ ≡ (nIso x) .inv ⋆ᴰ F ⟪ f ⟫ ⋆ᴰ (N-ob y)
    sqLR {x} {y} {f} = invMoveR (symAreInv (isIso→areInv (nIso y))) sqLL

  open NatTrans
  open NatIso

  infix 10 NatTrans
  syntax NatTrans F G = F ⇒ G

  infix 9 NatIso
  syntax NatIso F G = F ≅ᶜ G -- c superscript to indicate that this is in the context of categories

  -- component of a natural transformation
  infix 30 _⟦_⟧
  _⟦_⟧ : ∀ {F G : Functor C D} → (F ⇒ G) → (x : C .ob) → D [(F .F-ob x) , (G .F-ob x)]
  _⟦_⟧ = N-ob

  idTrans : (F : Functor C D) → NatTrans F F
  idTrans F .N-ob x = D .id (F .F-ob x)
  idTrans F .N-hom f =
      (F .F-hom f) ⋆ᴰ (idTrans F .N-ob _)
    ≡⟨ D .⋆IdR _ ⟩
      F .F-hom f
    ≡⟨ sym (D .⋆IdL _) ⟩
      (D .id (F .F-ob _)) ⋆ᴰ (F .F-hom f)
    ∎

  syntax idTrans F = 1[ F ]

  -- vertical sequencing
  seqTrans : {F G H : Functor C D} (α : NatTrans F G) (β : NatTrans G H) → NatTrans F H
  seqTrans α β .N-ob x = (α .N-ob x) ⋆ᴰ (β .N-ob x)
  seqTrans {F} {G} {H} α β .N-hom f =
    (F .F-hom f) ⋆ᴰ ((α .N-ob _) ⋆ᴰ (β .N-ob _))
      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
    ((F .F-hom f) ⋆ᴰ (α .N-ob _)) ⋆ᴰ (β .N-ob _)
      ≡[ i ]⟨ (α .N-hom f i) ⋆ᴰ (β .N-ob _) ⟩
    ((α .N-ob _) ⋆ᴰ (G .F-hom f)) ⋆ᴰ (β .N-ob _)
      ≡⟨ D .⋆Assoc _ _ _ ⟩
    (α .N-ob _) ⋆ᴰ ((G .F-hom f) ⋆ᴰ (β .N-ob _))
      ≡[ i ]⟨ (α .N-ob _) ⋆ᴰ (β .N-hom f i) ⟩
    (α .N-ob _) ⋆ᴰ ((β .N-ob _) ⋆ᴰ (H .F-hom f))
      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
    ((α .N-ob _) ⋆ᴰ (β .N-ob _)) ⋆ᴰ (H .F-hom f)
      ∎

  compTrans : {F G H : Functor C D} (β : NatTrans G H) (α : NatTrans F G) → NatTrans F H
  compTrans β α = seqTrans α β

  infixl 8 seqTrans
  syntax seqTrans α β = α ●ᵛ β

  -- vertically sequence natural transformations whose
  -- common functor is not definitional equal
  seqTransP : {F G G' H : Functor C D} (p : G ≡ G')
            → (α : NatTrans F G) (β : NatTrans G' H)
            → NatTrans F H
  seqTransP {F} {G} {G'} {H} p α β .N-ob x
    -- sequence morphisms with non-judgementally equal (co)domain
    = seqP {C = D} {p = Gx≡G'x} (α ⟦ x ⟧) (β ⟦ x ⟧)
    where
      Gx≡G'x : ∀ {x} → G ⟅ x ⟆ ≡ G' ⟅ x ⟆
      Gx≡G'x {x} i = F-ob (p i) x
  seqTransP {F} {G} {G'} {H} p α β .N-hom {x = x} {y} f
    -- compose the two commuting squares
    -- 1. α's commuting square
    -- 2. β's commuting square, but extended to G since β is only G' ≡> H
    = compSq {C = D} (α .N-hom f) βSq
    where
      -- functor equality implies equality of actions on objects and morphisms
      Gx≡G'x : G ⟅ x ⟆ ≡ G' ⟅ x ⟆
      Gx≡G'x i = F-ob (p i) x

      Gy≡G'y : G ⟅ y ⟆ ≡ G' ⟅ y ⟆
      Gy≡G'y i = F-ob (p i) y

      Gf≡G'f : PathP (λ i → D [ Gx≡G'x i , Gy≡G'y i ]) (G ⟪ f ⟫) (G' ⟪ f ⟫)
      Gf≡G'f i = p i ⟪ f ⟫

      -- components of β extended out to Gx and Gy respectively
      βx' = subst (λ a → D [ a , H ⟅ x ⟆ ]) (sym Gx≡G'x) (β ⟦ x ⟧)
      βy' = subst (λ a → D [ a , H ⟅ y ⟆ ]) (sym Gy≡G'y) (β ⟦ y ⟧)

      -- extensions are equal to originals
      βy'≡βy : PathP (λ i → D [ Gy≡G'y i , H ⟅ y ⟆ ]) βy' (β ⟦ y ⟧)
      βy'≡βy = symP (toPathP {A = λ i → D [ Gy≡G'y (~ i) , H ⟅ y ⟆ ]} refl)

      βx≡βx' : PathP (λ i → D [ Gx≡G'x (~ i) , H ⟅ x ⟆ ]) (β ⟦ x ⟧) βx'
      βx≡βx' = toPathP refl

      -- left wall of square
      left : PathP (λ i → D [ Gx≡G'x i , H ⟅ y ⟆ ]) (G ⟪ f ⟫ ⋆⟨ D ⟩ βy') (G' ⟪ f ⟫ ⋆⟨ D ⟩ β ⟦ y ⟧)
      left i = Gf≡G'f i ⋆⟨ D ⟩ βy'≡βy i

      -- right wall of square
      right : PathP (λ i → D [ Gx≡G'x (~ i) , H ⟅ y ⟆ ]) (β ⟦ x ⟧ ⋆⟨ D ⟩ H ⟪ f ⟫) (βx' ⋆⟨ D ⟩ H ⟪ f ⟫)
      right i = βx≡βx' i ⋆⟨ D ⟩ refl {x = H ⟪ f ⟫} i

      -- putting it all together
      βSq : G ⟪ f ⟫ ⋆⟨ D ⟩ βy' ≡ βx' ⋆⟨ D ⟩ H ⟪ f ⟫
      βSq i = comp (λ k → D [ Gx≡G'x (~ k) , H ⟅ y ⟆ ])
                   (λ j → λ { (i = i0) → left (~ j)
                            ; (i = i1) → right j })
                   (β .N-hom f i)

  module _  ⦃ isCatD : isCategory D ⦄ {F G : Functor C D} {α β : NatTrans F G} where
    open Precategory
    open Functor
    open NatTrans

    makeNatTransPath : α .N-ob ≡ β .N-ob → α ≡ β
    makeNatTransPath p i .N-ob = p i
    makeNatTransPath p i .N-hom f = rem i
      where
        rem : PathP (λ i → (F .F-hom f) ⋆ᴰ (p i _) ≡ (p i _) ⋆ᴰ (G .F-hom f)) (α .N-hom f) (β .N-hom f)
        rem = toPathP (isCatD .isSetHom _ _ _ _)

  module _  ⦃ isCatD : isCategory D ⦄ {F F' G G' : Functor C D}
            {α : NatTrans F G}
            {β : NatTrans F' G'} where
    open Precategory
    open Functor
    open NatTrans
    makeNatTransPathP : ∀ (p : F ≡ F') (q : G ≡ G')
                      → PathP (λ i → (x : C .ob) → D [ (p i) .F-ob x , (q i) .F-ob x ]) (α .N-ob) (β .N-ob)
                      → PathP (λ i → NatTrans (p i) (q i)) α β
    makeNatTransPathP p q P i .N-ob = P i
    makeNatTransPathP p q P i .N-hom f = rem i
      where
        rem : PathP (λ i → ((p i) .F-hom f) ⋆ᴰ (P i _) ≡ (P i _) ⋆ᴰ ((q i) .F-hom f)) (α .N-hom f) (β .N-hom f)
        rem = toPathP (isCatD .isSetHom _ _ _ _)

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

module _ {B : Precategory ℓB ℓB'} {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
  open NatTrans
  -- whiskering
  -- αF
  _∘ˡ_ : ∀ {G H : Functor C D} (α : NatTrans G H) → (F : Functor B C)
        → NatTrans (G ∘F F) (H ∘F F)
  (_∘ˡ_ {G} {H} α F) .N-ob x = α ⟦ F ⟅ x ⟆ ⟧
  (_∘ˡ_ {G} {H} α F) .N-hom f = (α .N-hom) _

  -- Kβ
  _∘ʳ_ : ∀ (K : Functor C D) → {G H : Functor B C} (β : NatTrans G H)
       → NatTrans (K ∘F G) (K ∘F H)
  (_∘ʳ_ K {G} {H} β) .N-ob x = K ⟪ β ⟦ x ⟧ ⟫
  (_∘ʳ_ K {G} {H} β) .N-hom f = preserveCommF {C = C} {D = D} {K} (β .N-hom f)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-# OPTIONS --copatterns --sized-types #-}

open import Common.Size

module Issue1038 (A : Set) where

record S (i : Size) : Set where
  field
    force : ∀ (j : Size< i) → A

head : ∀ i → S i → (j : Size< i) → A
head i s j = S.force s _

-- Problem was:
-- Cannot solve size constraints
-- (↑ _9 A i s j) =< (_i_8 A i s j) : Size
-- (_i_8 A i s j) =< i : Size
-- when checking the definition of head

-- Works now.


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

module Data.Binary.Conversion.Fast where

-- This module provides a conversion function from
-- nats which uses built-in functions.
-- It is dramatically faster than the normal conversion
-- even at smaller numbers.

open import Data.Binary.Definition
open import Data.Nat.DivMod
open import Data.Nat.Base
open import Data.Bool

⟦_⇑⟧⟨_⟩ : ℕ → ℕ → 𝔹
⟦ suc n ⇑⟧⟨ suc w ⟩ =
  if even n
    then 1ᵇ ⟦ n ÷ 2 ⇑⟧⟨ w ⟩
    else 2ᵇ ⟦ n ÷ 2 ⇑⟧⟨ w ⟩
⟦ zero  ⇑⟧⟨ _    ⟩ = 0ᵇ
⟦ suc _ ⇑⟧⟨ zero ⟩ = 0ᵇ -- will not happen

-- We build the output by repeatedly halving the input,
-- but we also pass in the number to reduce as we go so that
-- we satisfy the termination checker.
⟦_⇑⟧ : ℕ → 𝔹
⟦ n ⇑⟧ = ⟦ n ⇑⟧⟨ n ⟩
{-# INLINE ⟦_⇑⟧ #-}

-- Without the added argument to the recursor, the function does not
-- pass the termination checker:
-- {-# TERMINATING #-}
-- ⟦_⇑⟧″ : ℕ → 𝔹
-- ⟦ zero  ⇑⟧″ = 0ᵇ
-- ⟦ suc n ⇑⟧″ =
--   if rem n 2 ℕ.≡ᴮ 0
--   then 1ᵇ ⟦ n ÷ 2 ⇑⟧″
--   else 2ᵇ ⟦ n ÷ 2 ⇑⟧″

-- The "principled" version (which uses well-founded recursion) is
-- incredibly slow. (and the following doesn't even compute, because of
-- cubical)

-- open import Data.Nat.WellFounded

-- ⟦_⇑⟧‴ : ℕ → 𝔹
-- ⟦ n ⇑⟧‴ = go n (≤-wellFounded n)
--   where
--   go : ∀ n → Acc _<_ n → 𝔹
--   go zero    wf = 0ᵇ
--   go (suc n) (acc wf) =
--     if rem n 2 ℕ.≡ᴮ 0
--     then 1ᵇ go (n ÷ 2) (wf (n ÷ 2) (s≤s (div2≤ n)))
--     else 2ᵇ go (n ÷ 2) (wf (n ÷ 2) (s≤s (div2≤ n)))

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Isos.NatLike where

open import Isos.Isomorphism

open import Nats
open import Data.Product

open import Equality
open import Data.Unit

------------------------------------------------------------------------
-- internal stuffs

private

  module WithList where

  open import Lists

  list→ℕ : List ⊤ → ℕ
  list→ℕ  []      = zero
  list→ℕ (tt ∷ a) = suc (list→ℕ a)

  ℕ→list : ℕ → List ⊤
  ℕ→list  zero   = []
  ℕ→list (suc a) = tt ∷ ℕ→list a

  proofListL : ∀ n → list→ℕ (ℕ→list n) ≡ n
  proofListL zero = refl
  proofListL (suc n) rewrite proofListL n = refl

  proofListR : ∀ n → ℕ→list (list→ℕ n) ≡ n
  proofListR [] = refl
  proofListR (tt ∷ l) rewrite proofListR l = refl

  module WithVec where

  open import Vecs

  vec→ℕ′ : ∀ {n} → Vec ⊤ n → ℕ
  vec→ℕ′ {n}  []      = n
  vec→ℕ′ {n} (tt ∷ a) = n

  vec→ℕ : ∀ {n} → Vec ⊤ n → ∃ (λ m → n ≡ m)
  vec→ℕ  []      = zero , refl
  vec→ℕ (tt ∷ a) with vec→ℕ a
  ...               | m , refl = suc m , refl

  ℕ→vec : ∀ {n} → ∃ (λ m → n ≡ m) → Vec ⊤ n
  ℕ→vec  (zero   , refl) = []
  ℕ→vec ((suc a) , refl) = tt ∷ ℕ→vec (a , refl)

  proofVecL : ∀ {n} (m : ∃ (λ m → n ≡ m)) → vec→ℕ (ℕ→vec m) ≡ m
  proofVecL (zero , refl) = refl
  proofVecL (suc a , refl) rewrite proofVecL (a , refl) = refl

  -- how to prove?
  -- proofVecR : ∀ n → ℕ→vec (vec→ℕ n) ≡ n

------------------------------------------------------------------------
-- public aliases

iso-nat-list : ℕ ⇔ List ⊤
iso-nat-list = ∧-intro ℕ→list list→ℕ

iso-nat-vec : ∀ {n} → ∃ (λ m → n ≡ m) ⇔ Vec ⊤ n
iso-nat-vec = ∧-intro ℕ→vec vec→ℕ


text:
open import Signature
import Program

module Rewrite (Σ : Sig) (V : Set) (P : Program.Program Σ V) where

open import Terms Σ
open import Program Σ V
open import Data.Empty renaming (⊥ to ∅)
open import Data.Unit
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Sum as Sum
open import Data.Fin
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

data _⟿_ (t : T V) : T V → Set where
  rew-step : (cl : dom P) (i : dom (getb P cl)) {σ : Subst V V} →
             matches (geth P cl) t σ → -- (mgm t (geth P cl) σ) →
             t ⟿ app σ (get (getb P cl) i)

Val : Pred (T V) _
Val t = (cl : dom P) (i : dom (getb P cl)) {σ : Subst V V} →
        ¬ (matches (geth P cl) t σ)

no-rewrite-on-vals : (t : T V) → Val t → (s : T V) → ¬ (t ⟿ s)
no-rewrite-on-vals t p ._ (rew-step cl i q) = p cl i q

data _↓_ (t : T V) : T V → Set where
  val : Val t → t ↓ t
  step : (r s : T V) → r ↓ s → t ⟿ r → t ↓ s

{- Strongly normalising terms wrt to P are either in normal form, i.e. values,
or for every clause that matches, every rewrite step must be SN.
This is an adaption of the usual (constructive) definition.
-}
data SN (t : T V) : Set where
  val-sn   : Val t → SN t
  steps-sn : (cl : dom P) (i : dom (getb P cl)) {σ : Subst V V} →
             (matches t (geth P cl) σ) →
             SN (app σ (get (getb P cl) i)) →
             SN t

-- | Determines whether a term t is derivable from an axiom, i.e., whether
-- there is a clause " ⇒ p" such that p matches t.
Axiom : Pred (T V) _
Axiom t = ∃₂ λ cl σ → (mgm t (geth P cl) σ) × (domEmpty (getb P cl))

-- | An inductively valid term is derivable in finitely many steps from
-- axioms.
data Valid (t : T V) : Set where
  val-sn   : Axiom t → Valid t
  steps-sn : (cl : dom P) (i : dom (getb P cl)) {σ : Subst V V} →
             (matches t (geth P cl) σ) →
             Valid (app σ (get (getb P cl) i)) →
             Valid t

{-

⊥ : {X : Set} → X ⊎ ⊤
⊥ = inj₂ tt

record Rew-Branch (F : T V → Set) (t : T V) : Set where
  constructor prf-branch
  field
    clause : dom P
    matcher : Subst V V
    isMgm : mgm t (geth P clause) matcher
    next : (i : dom (getb P clause)) →
           F (app matcher (get (getb P clause) i))

-- | Set of rewrite trees starting in t that use the rules given in P.
-- If the tree is ⊥, then t cannot be rewritten by any of the rules of P.
data Rew (t : T V) : Set where
  in-prf : Rew-Branch Rew t ⊎ ⊤ → Rew t

-- | Just as Rew, only that we also allow infinite rewriting sequences.
record Rew∞ (t : T V) : Set where
  coinductive
  field out-prf : Rew-Branch Rew∞ t ⊎ ⊤
open Rew∞

out-prf⁻¹ : ∀{t} → Rew-Branch Rew∞ t ⊎ ⊤ → Rew∞ t
out-prf (out-prf⁻¹ b) = b

-- | Finite rewriting trees are included in the set of the possibly infinite
-- ones.
χ-prf : ∀{t} → Rew t → Rew∞ t
χ-prf (in-prf (inj₁ (prf-branch c m isMgm next))) =
  out-prf⁻¹ (inj₁ (prf-branch c m isMgm (λ i → χ-prf (next i))))
χ-prf (in-prf (inj₂ tt)) = out-prf⁻¹ ⊥

Rew-Step : (F : {s : T V} → Rew∞ s → Set) → {t : T V} (R : Rew∞ t) → Set
Rew-Step F R with out-prf R
Rew-Step F R | inj₁ (prf-branch clause matcher isMgm next) = {!!}
Rew-Step F R | inj₂ tt = ∅

data Path {t : T V} (R : Rew∞ t) : Set where
  root : Path R
  step : {!!} → Path R
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Loc (K : Set) where

open import Basics
open import Pr
open import Nom

data Loc : Set where
  EL : Loc
  _*_ : Loc -> K -> Loc

infixl 50 _*_

data _!_ : Loc -> K -> Set where
  top : {L : Loc}{S : K} -> (L * S) ! S
  pop : {L : Loc}{S T : K} -> L ! S -> (L * T) ! S

_<*_ : K -> Loc -> Loc
S <* EL = EL * S
S <* (L * T) = (S <* L) * T

max : {S : K}(L : Loc) -> (S <* L) ! S
max EL = top
max (L * T) = pop (max L)

_<_ : (S : K){L : Loc}{T : K} -> L ! T -> (S <* L) ! T
S < top = top
S < pop x = pop (S < x)

data MaxV (S : K)(L : Loc) : {T : K} -> (S <* L) ! T -> Set where
  isMax : MaxV S L (max L)
  isLow : {T : K}(x : L ! T) -> MaxV S L (S < x)

maxV : (S : K)(L : Loc){T : K}(x : (S <* L) ! T) -> MaxV S L x
maxV S EL top = isMax
maxV S EL (pop ())
maxV S (L * T) top = isLow top
maxV S (L * T) (pop x) with maxV S L x
maxV S (L * T) (pop .(max L)) | isMax = isMax
maxV S (L * T) (pop .(S < x)) | isLow x = isLow (pop x)

_bar_ : (L : Loc){S : K} -> L ! S -> Loc
EL bar ()
(L * S) bar top = L
(L * S) bar (pop v) = (L bar v) * S

infixl 50 _bar_

_thin_ : {L : Loc}{S T : K}(x : L ! S) -> (L bar x) ! T -> L ! T
top thin y = pop y
(pop x) thin top = top
(pop x) thin (pop y) = pop (x thin y)

data VarQV {L : Loc}{S : K}(x : L ! S) : {T : K} -> (L ! T) -> Set where
  vSame : VarQV x x
  vDiff : {T : K}(y : (L bar x) ! T) -> VarQV x (x thin y)

varQV : {L : Loc}{S T : K}(x : L ! S)(y : L ! T) -> VarQV x y
varQV top top = vSame
varQV top (pop y) = vDiff y
varQV (pop x) top = vDiff top
varQV (pop x) (pop y) with varQV x y
varQV (pop x) (pop .x) | vSame = vSame
varQV (pop x) (pop .(x thin y)) | vDiff y = vDiff (pop y)


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

module cubical where

open import Cubical.Core.Primitives

--- Sharp of a type: you can raise any term of type A to the sharp to get a term of type sharp-A
data ♯_ {ℓ : Level} (A : Type ℓ) : Type ℓ where
  _↑♯ : A → ♯ A

-- do we need a duplicate of sharp-on-Types for crisp types?
-- data ♯c_ {@♭ ℓ : Level} (@♭ A : Type ℓ) : Type ℓ where
--   _↑♯c : A → ♯c A

-- having something crisply in sharp-A gets you something in a
-- the constructor is also the computation rule
_↓♯ : {@♭ ℓ : Level} {@♭ A : Type ℓ} (@♭ x : ♯ A) → A
(x ↑♯) ↓♯ = x

lower-then-upper : {@♭ ℓ : Level} {@♭ A : Type ℓ} (@♭ x : ♯ A) → (x ↓♯) ↑♯ ≡ x
lower-then-upper x = λ i → x

--- I is the interval pre-type
--- i0 : I
--- i1 : I

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
module Data.Nat.Properties where

import Prelude
import Logic.Base
import Logic.Relations
import Logic.Equivalence
import Logic.Operations as Operations
import Logic.Identity
import Logic.ChainReasoning
import Data.Nat
import Data.Bool

open Prelude
open Data.Nat
open Logic.Base
open Logic.Relations
open Logic.Identity
open Data.Bool

module Proofs where

  module Ops = Operations.MonoEq {Nat} Equiv
  open Ops

  module Chain = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans)
  open Chain

  +zero : (n : Nat) -> n + zero ≡ n
  +zero  zero   = refl
  +zero (suc n) = cong suc (+zero n)

  +suc : (n m : Nat) -> n + suc m ≡ suc (n + m)
  +suc  zero   m = refl
  +suc (suc n) m = cong suc (+suc n m)

  +commute : Commutative _+_
  +commute x  zero   = +zero x
  +commute x (suc y) = trans (+suc x y) (cong suc (+commute x y))

  +assoc : Associative _+_
  +assoc  zero   y z = refl
  +assoc (suc x) y z = cong suc (+assoc x y z)

  *zero : (n : Nat) -> n * zero ≡ zero
  *zero  zero   = refl
  *zero (suc n) = *zero n

  *suc : (x y : Nat) -> x * suc y ≡ x + x * y
  *suc  zero   y = refl
  *suc (suc x) y =
    chain> suc x * suc y
       === suc (y + x * suc y)   by refl
       === suc (x + (y + x * y)) by cong suc
        ( chain> y + x * suc y
             === y + (x + x * y)  by cong (_+_ y) (*suc x y)
             === (y + x) + x * y  by +assoc y x (x * y)
             === (x + y) + x * y  by cong (flip _+_ (x * y)) (+commute y x)
             === x + (y + x * y)  by sym (+assoc x y (x * y))
        )
       === suc x + suc x * y     by refl

  *commute : (x y : Nat) -> x * y ≡ y * x
  *commute x  zero   = *zero x
  *commute x (suc y) = trans (*suc x y) (cong (_+_ x) (*commute x y))

  one* : (x : Nat) -> 1 * x ≡ x
  one* x = +zero x

  *one : (x : Nat) -> x * 1 ≡ x
  *one x = trans (*commute x 1) (one* x)

  *distrOver+L : (x y z : Nat) -> x * (y + z) ≡ x * y + x * z
  *distrOver+L  zero   y z = refl
  *distrOver+L (suc x) y z =
    chain> suc x * (y + z)
       === (y + z) + x * (y + z)      by refl
       === (y + z) + (x * y + x * z)  by cong (_+_ (y + z)) ih
       === ((y + z) + x * y) + x * z  by +assoc (y + z) (x * y) (x * z)
       === (y + (z + x * y)) + x * z  by cong (flip _+_ (x * z)) (sym (+assoc y z (x * y)))
       === (y + (x * y + z)) + x * z  by cong (\w -> (y + w) + x * z) (+commute z (x * y))
       === ((y + x * y) + z) + x * z  by cong (flip _+_ (x * z)) (+assoc y (x * y) z)
       === (y + x * y) + (z + x * z)  by sym (+assoc (y + x * y) z (x * z))
       === suc x * y + suc x * z      by refl
    where
      ih = *distrOver+L x y z

  *distrOver+R : (x y z : Nat) -> (x + y) * z ≡ x * z + y * z
  *distrOver+R  zero   y z = refl
  *distrOver+R (suc x) y z =
    chain> (suc x + y) * z
       === z + (x + y) * z      by refl
       === z + (x * z + y * z)  by cong (_+_ z) (*distrOver+R x y z)
       === (z + x * z) + y * z  by +assoc z (x * z) (y * z)
       === suc x * z + y * z    by refl

  *assoc : Associative _*_
  *assoc  zero   y z = refl
  *assoc (suc x) y z =
    chain> suc x * (y * z)
       === y * z + x * (y * z)  by refl
       === y * z + (x * y) * z  by cong (_+_ (y * z)) ih
       === (y + x * y) * z      by sym (*distrOver+R y (x * y) z)
       === (suc x * y) * z      by refl
    where
      ih = *assoc x y z

  ≤refl : (n : Nat) -> IsTrue (n ≤ n)
  ≤refl  zero   = tt
  ≤refl (suc n) = ≤refl n

  <implies≤ : (n m : Nat) -> IsTrue (n < m) -> IsTrue (n ≤ m)
  <implies≤  zero    m      h = tt
  <implies≤ (suc n)  zero   ()
  <implies≤ (suc n) (suc m) h = <implies≤ n m h

  n-m≤n : (n m : Nat) -> IsTrue (n - m ≤ n)
  n-m≤n  zero    m      = tt
  n-m≤n (suc n)  zero   = ≤refl n
  n-m≤n (suc n) (suc m) = <implies≤ (n - m) (suc n) (n-m≤n n m)

--   mod≤ : (n m : Nat) -> IsTrue (mod n (suc m) ≤ m)
--   mod≤  zero   m = tt
--   mod≤ (suc n) m = mod≤ (n - m) m

open Proofs public


text:
module Structure.Category.NaturalTransformation.NaturalTransformations where

open import Functional           using () renaming (id to idᶠⁿ)
open import Functional.Dependent using () renaming (_∘_ to _∘ᶠⁿ_)
open import Logic
open import Logic.Predicate
import      Lvl
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Category.NaturalTransformation
open import Structure.Categorical.Properties
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

open CategoryObject
private variable ℓₒₗ ℓₒᵣ ℓₘₗ ℓₘᵣ ℓₑₗ ℓₑᵣ : Lvl.Level

module Raw
  (catₗ : CategoryObject{ℓₒₗ}{ℓₘₗ}{ℓₑₗ})
  (catᵣ : CategoryObject{ℓₒᵣ}{ℓₘᵣ}{ℓₑᵣ})
  where

  private variable F F₁ F₂ F₃ : Object(catₗ) → Object(catᵣ)
  private instance _ = category catₗ
  private instance _ = category catᵣ

  open Category.ArrowNotation ⦃ … ⦄
  open Category ⦃ … ⦄ hiding (identity)

  idᴺᵀ : (x : Object(catₗ)) → (F(x) ⟶ F(x))
  idᴺᵀ _ = id

  _∘ᴺᵀ_ : ((x : Object(catₗ)) → (F₂(x) ⟶ F₃(x))) → ((x : Object(catₗ)) → (F₁(x) ⟶ F₂(x))) → ((x : Object(catₗ)) → (F₁(x) ⟶ F₃(x)))
  (comp₁ ∘ᴺᵀ comp₂)(x) = comp₁(x) ∘ comp₂(x)

module _
  {catₗ : CategoryObject{ℓₒₗ}{ℓₘₗ}{ℓₑₗ}}
  {catᵣ : CategoryObject{ℓₒᵣ}{ℓₘᵣ}{ℓₑᵣ}}
  where

  private instance _ = category catₗ
  private instance _ = category catᵣ

  open Category ⦃ … ⦄ hiding (identity)
  open Functor ⦃ … ⦄
  private open module Equivᵣ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv(catᵣ){x}{y} ⦄) using ()

  module _ where
    open Raw(catₗ)(catᵣ)

    module _ {functor@([∃]-intro F) : catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ} where
      identity : NaturalTransformation(functor)(functor)(idᴺᵀ)
      NaturalTransformation.natural identity {x} {y} {f} =
        id ∘ map f 🝖-[ Morphism.identityₗ(_)(id) ⦃ identityₗ ⦄ ]
        map f      🝖-[ Morphism.identityᵣ(_)(id) ⦃ identityᵣ ⦄ ]-sym
        map f ∘ id 🝖-end

    module _ {functor₁@([∃]-intro F₁) functor₂@([∃]-intro F₂) functor₃@([∃]-intro F₃) : catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ} where
      composition : ∀{comp₁ comp₂} → NaturalTransformation(functor₂)(functor₃)(comp₁) → NaturalTransformation(functor₁)(functor₂)(comp₂) → NaturalTransformation(functor₁)(functor₃)(comp₁ ∘ᴺᵀ comp₂)
      NaturalTransformation.natural (composition {comp₁} {comp₂} nat₁ nat₂) {x} {y} {f} =
        (comp₁(y) ∘ comp₂(y)) ∘ map f 🝖-[ Morphism.associativity(_) ⦃ associativity ⦄ ]
        comp₁(y) ∘ (comp₂(y) ∘ map f) 🝖-[ congruence₂ᵣ(_∘_)(comp₁(y)) (NaturalTransformation.natural nat₂) ]
        comp₁(y) ∘ (map f ∘ comp₂(x)) 🝖-[ Morphism.associativity(_) ⦃ associativity ⦄ ]-sym
        (comp₁(y) ∘ map f) ∘ comp₂(x) 🝖-[ congruence₂ₗ(_∘_)(comp₂(x)) (NaturalTransformation.natural nat₁) ]
        (map f ∘ comp₁(x)) ∘ comp₂(x) 🝖-[ Morphism.associativity(_) ⦃ associativity ⦄ ]
        map f ∘ (comp₁(x) ∘ comp₂(x)) 🝖-end

  module Wrapped where
    private variable F F₁ F₂ F₃ : catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ

    idᴺᵀ : (F →ᴺᵀ F)
    idᴺᵀ = [∃]-intro (Raw.idᴺᵀ(catₗ)(catᵣ)) ⦃ identity ⦄

    _∘ᴺᵀ_ : (F₂ →ᴺᵀ F₃) → (F₁ →ᴺᵀ F₂) → (F₁ →ᴺᵀ F₃)
    _∘ᴺᵀ_ ([∃]-intro F ⦃ F-proof ⦄) ([∃]-intro G ⦃ G-proof ⦄) = [∃]-intro (Raw._∘ᴺᵀ_ (catₗ)(catᵣ) F G) ⦃ composition F-proof G-proof ⦄

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of disjoint lists (setoid equality)
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Disjoint.Setoid.Properties where

open import Data.List.Base
open import Data.List.Relation.Binary.Disjoint.Setoid
import Data.List.Relation.Unary.Any as Any
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
open import Data.List.Relation.Unary.Any.Properties using (++⁻)
open import Data.Product using (_,_)
open import Data.Sum.Base using (inj₁; inj₂)
open import Relation.Binary
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- Relational properties
------------------------------------------------------------------------

module _ {c ℓ} (S : Setoid c ℓ) where

  sym : Symmetric (Disjoint S)
  sym xs#ys (v∈ys , v∈xs) = xs#ys (v∈xs , v∈ys)

------------------------------------------------------------------------
-- Relationship with other predicates
------------------------------------------------------------------------

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S

  Disjoint⇒AllAll : ∀ {xs ys} → Disjoint S xs ys →
                    All (λ x → All (λ y → ¬ x ≈ y) ys) xs
  Disjoint⇒AllAll xs#ys = All.map (¬Any⇒All¬ _)
    (All.tabulate (λ v∈xs v∈ys → xs#ys (Any.map reflexive v∈xs , v∈ys)))

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- concat

module _ {c ℓ} (S : Setoid c ℓ) where

  concat⁺ʳ : ∀ {vs xss} → All (Disjoint S vs) xss → Disjoint S vs (concat xss)
  concat⁺ʳ {xss = xs ∷ xss} (vs#xs ∷ vs#xss) (v∈vs , v∈xs++concatxss)
    with ++⁻ xs v∈xs++concatxss
  ... | inj₁ v∈xs  = vs#xs (v∈vs , v∈xs)
  ... | inj₂ v∈xss = concat⁺ʳ vs#xss (v∈vs , v∈xss)


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

open import HoTT
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLaneFunctor
open import groups.ToOmega
open import cohomology.Theory
open import cohomology.SpectrumModel

module cohomology.EMModel where

module _ {i} (G : AbGroup i) where

  open EMExplicit G using (⊙EM; EM-level; EM-conn; spectrum)

  EM-E : (n : ℤ) → Ptd i
  EM-E (pos m) = ⊙EM m
  EM-E (negsucc m) = ⊙Lift ⊙Unit

  EM-spectrum : (n : ℤ) → ⊙Ω (EM-E (succ n)) ⊙≃ EM-E n
  EM-spectrum (pos n) = spectrum n
  EM-spectrum (negsucc O) = ≃-to-⊙≃ {X = ⊙Ω (EM-E 0)}
    (equiv (λ _ → _) (λ _ → idp)
           (λ _ → idp) (prop-has-all-paths {{has-level-apply (EM-level 0) _ _}} _))
    idp
  EM-spectrum (negsucc (S n)) = ≃-to-⊙≃ {X = ⊙Ω (EM-E (negsucc n))}
    (equiv (λ _ → _) (λ _ → idp)
           (λ _ → idp) (prop-has-all-paths {{=-preserves-level ⟨⟩}} _))
    idp

  EM-Cohomology : CohomologyTheory i
  EM-Cohomology = spectrum-cohomology EM-E EM-spectrum

  open CohomologyTheory EM-Cohomology

  EM-dimension : {n : ℤ} → n ≠ 0 → is-trivialᴳ (C n (⊙Lift ⊙S⁰))
  EM-dimension {pos O} neq = ⊥-rec (neq idp)
  EM-dimension {pos (S n)} _ =
    contr-is-trivialᴳ (C (pos (S n)) (⊙Lift ⊙S⁰))
      {{connected-at-level-is-contr
        {{⟨⟩}}
        {{Trunc-preserves-conn $
           equiv-preserves-conn
            (pre⊙∘-equiv ⊙lower-equiv ∘e ⊙Bool→-equiv-idf _ ⁻¹)
            {{path-conn (connected-≤T (⟨⟩-monotone-≤ (≤-ap-S (O≤ n)))
                                     )}}}}}}
  EM-dimension {negsucc O} _ =
    contr-is-trivialᴳ (C (negsucc O) (⊙Lift ⊙S⁰))
      {{Trunc-preserves-level 0 (Σ-level (Π-level λ _ →
        inhab-prop-is-contr idp {{has-level-apply (EM-level 0) _ _}})
        (λ x → has-level-apply (has-level-apply (EM-level 0) _ _) _ _))}}

  EM-dimension {negsucc (S n)} _ =
    contr-is-trivialᴳ (C (negsucc (S n)) (⊙Lift ⊙S⁰))
      {{Trunc-preserves-level 0 (Σ-level (Π-level λ _ →
        =-preserves-level ⟨⟩) λ _ → =-preserves-level (=-preserves-level ⟨⟩))}}

  EM-Ordinary : OrdinaryTheory i
  EM-Ordinary = ordinary-theory EM-Cohomology EM-dimension

module _ {i} (G : AbGroup i) (H : AbGroup i) (φ : G →ᴬᴳ H) where

  EM-E-fmap : ∀ (n : ℤ) → EM-E G n ⊙→ EM-E H n
  EM-E-fmap (pos m) = ⊙EM-fmap G H φ m
  EM-E-fmap (negsucc m) = ⊙idf _

  open SpectrumModelMap (EM-E G) (EM-spectrum G) (EM-E H) (EM-spectrum H) EM-E-fmap
    public renaming (C-coeff-fmap to EM-C-coeff-fmap;
                     CEl-coeff-fmap to EM-CEl-coeff-fmap;
                     ⊙CEl-coeff-fmap to EM-⊙CEl-coeff-fmap)

module _ {i} (G : AbGroup i) where

  private
    EM-E-fmap-idhom : ∀ (n : ℤ)
      → EM-E-fmap G G (idhom (AbGroup.grp G)) n == ⊙idf _
    EM-E-fmap-idhom (pos n) = ⊙EM-fmap-idhom G n
    EM-E-fmap-idhom (negsucc n) = idp

  private
    module M = SpectrumModelMap (EM-E G) (EM-spectrum G) (EM-E G) (EM-spectrum G)

  EM-C-coeff-fmap-idhom : (n : ℤ) (X : Ptd i)
    → EM-C-coeff-fmap G G (idhom (AbGroup.grp G)) n X == idhom _
  EM-C-coeff-fmap-idhom n X =
    ap (λ map → M.C-coeff-fmap map n X) (λ= EM-E-fmap-idhom) ∙
    C-coeff-fmap-idf (EM-E G) (EM-spectrum G) n X

module _ {i} (G : AbGroup i) (H : AbGroup i) (K : AbGroup i)
             (ψ : H →ᴬᴳ K) (φ : G →ᴬᴳ H) where

  private
    EM-E-fmap-∘ : ∀ (n : ℤ)
      → EM-E-fmap G K (ψ ∘ᴳ φ) n == EM-E-fmap H K ψ n ⊙∘ EM-E-fmap G H φ n
    EM-E-fmap-∘ (pos n) = ⊙EM-fmap-∘ G H K ψ φ n
    EM-E-fmap-∘ (negsucc n) = idp

  private
    module M = SpectrumModelMap (EM-E G) (EM-spectrum G) (EM-E K) (EM-spectrum K)

  EM-C-coeff-fmap-∘ : (n : ℤ) (X : Ptd i)
    → EM-C-coeff-fmap G K (ψ ∘ᴳ φ) n X ==
      EM-C-coeff-fmap H K ψ n X ∘ᴳ
      EM-C-coeff-fmap G H φ n X
  EM-C-coeff-fmap-∘ n X =
    ap (λ map → M.C-coeff-fmap map n X) (λ= EM-E-fmap-∘) ∙
    C-coeff-fmap-∘ (EM-E G) (EM-spectrum G)
                   (EM-E H) (EM-spectrum H)
                   (EM-E K) (EM-spectrum K)
                   (EM-E-fmap H K ψ)
                   (EM-E-fmap G H φ)
                   n X

module _ {i} (G : AbGroup i) where

  open CohomologyTheory (spectrum-cohomology (EM-E G) (EM-spectrum G))
  open EMExplicit
  open import homotopy.SuspensionLoopSpaceInverse
  private
    module G = AbGroup G

  ⊙Ω-fmap-EM-E-fmap-inv-hom : ∀ (n : ℤ) → ⊙Ω-fmap (EM-E-fmap G G (inv-hom G) n) == ⊙Ω-!
  ⊙Ω-fmap-EM-E-fmap-inv-hom (negsucc n) =
    contr-center $ =-preserves-level $
    ⊙→-level (⊙Ω (⊙Lift ⊙Unit)) (⊙Ω (⊙Lift ⊙Unit)) $
    =-preserves-level $ Lift-level $ Unit-level
  ⊙Ω-fmap-EM-E-fmap-inv-hom (pos O) =
    prop-path
      (⊙→-level (⊙Ω (⊙EM G 0)) (⊙Ω (⊙EM G 0)) $
       has-level-apply (EM-level G 0) (pt (⊙EM G 0)) (pt (⊙EM G 0)))
      _ _
  ⊙Ω-fmap-EM-E-fmap-inv-hom (pos 1) = =⊙∘-out $
    ⊙Ω-fmap (⊙Trunc-fmap (⊙EM₁-fmap (inv-hom G))) ◃⊙idf
      =⊙∘⟨ 0 & 0 & !⊙∘ $ ⊙<–-inv-l-=⊙∘ (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙EM₁-fmap (inv-hom G))) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙–>-⊙Ω-⊙Trunc-comm-natural-=⊙∘ 0 (⊙EM₁-fmap (inv-hom G)) ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙EM₁-fmap (inv-hom G))) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ap ⊙Trunc-fmap $ ⊙Ω-fmap-⊙EM₁-neg G ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘
    ⊙Trunc-fmap ⊙Ω-! ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙idf
      =⊙∘⟨ 1 & 2 & =⊙∘-in
           {gs = ⊙–> (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘ ⊙Ω-! ◃⊙idf} $
           ! $ ⊙λ=' –>-=ₜ-equiv-pres-! idp ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ◃⊙∘
    ⊙Ω-! ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙<–-inv-l-=⊙∘ (⊙Ω-⊙Trunc-comm 0 (⊙EM₁ G.grp)) ⟩
    ⊙Ω-! ◃⊙idf ∎⊙∘
  ⊙Ω-fmap-EM-E-fmap-inv-hom (pos (S (S k))) = =⊙∘-out $
    ⊙Ω-fmap (⊙EM-fmap G G (inv-hom G) (S (S k))) ◃⊙idf
      =⊙∘₁⟨ ap ⊙Ω-fmap (⊙EM-neg=⊙Trunc-fmap-⊙Susp-flip G k) ⟩
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ k (⊙EM₁ G.grp)))) ◃⊙idf
      =⊙∘⟨ 0 & 0 & !⊙∘ $
           ⊙<–-inv-l-=⊙∘ (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ k (⊙EM₁ G.grp)))) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙–>-⊙Ω-⊙Trunc-comm-natural-=⊙∘ ⟨ S k ⟩
             (⊙Susp-flip (⊙Susp^ k (⊙EM₁ G.grp))) ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-flip (⊙Susp^ k (⊙EM₁ G.grp)))) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ! $ ⊙Ω-!-⊙Susp-flip
              (⊙Susp^ k (⊙EM₁ G.grp))
              ⟨ S k ⟩
              (Spectrum.Trunc-fmap-σloop-is-equiv G k) ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
    ⊙Trunc-fmap ⊙Ω-! ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙idf
      =⊙∘⟨ 1 & 2 & =⊙∘-in
           {gs = ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
                 ⊙Ω-! ◃⊙idf} $
           ! $ ⊙λ=' –>-=ₜ-equiv-pres-! idp ⟩
    ⊙<– (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ◃⊙∘
    ⊙Ω-! ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙<–-inv-l-=⊙∘ (⊙Ω-⊙Trunc-comm ⟨ S k ⟩ (⊙Susp^ (S k) (⊙EM₁ G.grp))) ⟩
    ⊙Ω-! ◃⊙idf ∎⊙∘

  EM-C-coeff-fmap-inv-hom : ∀ (n : ℤ) (X : Ptd i)
    → EM-C-coeff-fmap G G (inv-hom G) n X ==
      inv-hom (C-abgroup n X)
  EM-C-coeff-fmap-inv-hom n X =
    group-hom= $ λ= $ Trunc-elim $ λ h → ap [_]₀ $
    ap (_⊙∘ h) (⊙Ω-fmap-EM-E-fmap-inv-hom (succ n)) ∙
    ⊙λ=' (λ _ → idp) (∙-unit-r (ap ! (snd h)))

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module BTree.Complete.Base.Properties {A : Set} where

open import BTree {A}
open import BTree.Complete.Base {A}
open import BTree.Equality {A}
open import BTree.Equality.Properties {A}

lemma-≃-⋗ : {l l' r' : BTree} → l ≃ l' → l' ⋗ r' → l ⋗ r'
lemma-≃-⋗ (≃nd x x' ≃lf ≃lf ≃lf) (⋗lf .x') = ⋗lf x
lemma-≃-⋗ (≃nd {r = r} x x' l≃r l≃l' l'≃r') (⋗nd .x' x'' r' l'' l'⋗r'') = ⋗nd x x'' r l'' (lemma-≃-⋗ l≃l' l'⋗r'')

lemma-⋗-≃ : {l r r' : BTree} → l ⋗ r → r ≃ r' → l ⋗ r'
lemma-⋗-≃ (⋗lf x) ≃lf = ⋗lf x
lemma-⋗-≃ (⋗nd {r' = r'} x x' r l' l⋗r') (≃nd {l' = l''} .x' x'' l'≃r' l'≃l'' l''≃r'') = ⋗nd x x'' r l'' (lemma-⋗-≃ l⋗r' (trans≃ (symm≃ l'≃r') (trans≃ l'≃l'' l''≃r'')))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting