text:
import PiCalculus.Utils
import PiCalculus.Syntax
import PiCalculus.Syntax.Properties
import PiCalculus.Semantics
import PiCalculus.Semantics.Properties
import PiCalculus.LinearTypeSystem
import PiCalculus.LinearTypeSystem.Algebras
import PiCalculus.LinearTypeSystem.Algebras.Graded
import PiCalculus.LinearTypeSystem.Algebras.Shared
import PiCalculus.LinearTypeSystem.Algebras.Linear
import PiCalculus.LinearTypeSystem.ContextLemmas
import PiCalculus.LinearTypeSystem.Framing
import PiCalculus.LinearTypeSystem.Weakening
import PiCalculus.LinearTypeSystem.Exchange
import PiCalculus.LinearTypeSystem.Strengthening
import PiCalculus.LinearTypeSystem.Substitution
import PiCalculus.LinearTypeSystem.SubjectCongruence
import PiCalculus.LinearTypeSystem.SubjectReduction
import PiCalculus.Examples

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
module UnifyMgu where

open import UnifyTerm

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

amgu : ∀ {m} (s t : Term m) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))
amgu leaf leaf acc = just acc
amgu leaf (s' fork t') acc = nothing
amgu (s' fork t') leaf acc = nothing
amgu (s1 fork s2) (t1 fork t2) acc =
                  amgu s2 t2 =<< amgu s1 t1 acc
amgu (i x) (i y) (m , anil) = just (flexFlex x y)
amgu (i x) t     (m , anil) = flexRigid x t
amgu t     (i x) (m , anil) = flexRigid x t
amgu s     t  (n , σ asnoc r / z) =
         (λ σ -> σ ∃asnoc r / z) <$>
           amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)

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

ext: agda


text:
module examplesPaperJFP.StatefulObject where

open import Data.Product
open import Data.String.Base as Str
open import Data.Nat.Base as N
open import Data.Vec as Vec using (Vec; []; _∷_; head; tail)

open import SizedIO.Console hiding (main)
open import Size

open import NativeIO

open import SizedIO.Base

StackStateˢ = ℕ

record Interfaceˢ : Set₁ where
  field  Stateˢ    :  Set
         Methodˢ   :  (s : Stateˢ)  →  Set
         Resultˢ   :  (s : Stateˢ)  →  (m : Methodˢ s)  →  Set
         nextˢ     :  (s : Stateˢ)  →  (m : Methodˢ s)  →  (r : Resultˢ s m) → Stateˢ

open Interfaceˢ public

data StackMethodˢ (A : Set) : (n : StackStateˢ) → Set where
  push  :  ∀ {n}  →  A  →  StackMethodˢ A n
  pop   :  ∀ {n}        →  StackMethodˢ A (suc n)

StackResultˢ                      :  (A : Set) → (s : StackStateˢ) → StackMethodˢ A s → Set
StackResultˢ A _  (push _)  =  Unit
StackResultˢ A _  pop       =  A

stackNextˢ  :  ∀ A n (m : StackMethodˢ A n) (r : StackResultˢ A n m) →  StackStateˢ
stackNextˢ _  n        (push _)  _  =  suc n
stackNextˢ _  (suc n)  pop       _  =  n

StackInterfaceˢ : (A : Set)  →  Interfaceˢ
Stateˢ   (StackInterfaceˢ A)  =  StackStateˢ
Methodˢ  (StackInterfaceˢ A)  =  StackMethodˢ A
Resultˢ  (StackInterfaceˢ A)  =  StackResultˢ A
nextˢ    (StackInterfaceˢ A)  =  stackNextˢ A

record Objectˢ (I : Interfaceˢ) (s : Stateˢ I) : Set where
  coinductive
  field objectMethod :  (m : Methodˢ I s) →
                        Σ[ r ∈ Resultˢ I s m ] Objectˢ I (nextˢ I s m r)
open Objectˢ public

record IOObjectˢ (Iᵢₒ : IOInterface) (I : Interfaceˢ) (s : Stateˢ I) : Set where
  coinductive
  field method :  (m : Methodˢ I s) →
                  IO Iᵢₒ ∞ (Σ[ r ∈ Resultˢ I s m ] IOObjectˢ Iᵢₒ I (nextˢ I s m r))
open IOObjectˢ public

stack  :  ∀{A}{n : ℕ} (as : Vec A n) →  Objectˢ (StackInterfaceˢ A) n
objectMethod (stack as)        (push a)  =  unit  ,  stack (a ∷ as)
objectMethod (stack (a ∷ as))  pop       =  a     ,  stack as

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Fin
open import lib.types.Pi
open import lib.types.Truncation

module lib.types.Choice where

unchoose : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : A → Type j}
  → Trunc n (Π A B) → Π A (Trunc n ∘ B)
unchoose = Trunc-rec (λ f → [_] ∘ f)

has-choice : ∀ {i} (n : ℕ₋₂) (A : Type i) j → Type (lmax i (lsucc j))
has-choice {i} n A j = (B : A → Type j) → is-equiv (unchoose {n = n} {A} {B})

Empty-has-choice : ∀ {n} {j} → has-choice n Empty j
Empty-has-choice {n} B = is-eq to from to-from from-to where
  to = unchoose {n = n} {Empty} {B}

  from : Π Empty (Trunc n ∘ B) → Trunc n (Π Empty B)
  from _ = [ (λ{()}) ]

  abstract
    to-from : ∀ f → to (from f) == f
    to-from _ = λ= λ{()}

    from-to : ∀ f → from (to f) == f
    from-to = Trunc-elim (λ _ → ap [_] (λ= λ{()}))

Unit-has-choice : ∀ {n} {j} → has-choice n Unit j
Unit-has-choice {n} B = is-eq to from to-from from-to where
  to = unchoose {n = n} {Unit} {B}

  Unit-elim' : B unit → Π Unit B
  Unit-elim' u unit = u

  from : Π Unit (Trunc n ∘ B) → Trunc n (Π Unit B)
  from f = Trunc-fmap Unit-elim' (f unit)

  abstract
    to-from : ∀ f → to (from f) == f
    to-from f = λ= λ{unit →
      Trunc-elim
        {P = λ f-unit → to (Trunc-fmap Unit-elim' f-unit) unit == f-unit}
        (λ _ → idp)
        (f unit)}

    from-to : ∀ f → from (to f) == f
    from-to = Trunc-elim (λ f → ap [_] (λ= λ{unit → idp}))

Coprod-has-choice : ∀ {i j} {n} {A : Type i} {B : Type j} {k}
  → has-choice n A k → has-choice n B k
  → has-choice n (A ⊔ B) k
Coprod-has-choice {n = n} {A} {B} A-hc B-hc C = is-eq to from to-from from-to where
  A-unchoose = unchoose {n = n} {A} {C ∘ inl}
  B-unchoose = unchoose {n = n} {B} {C ∘ inr}
  module A-unchoose = is-equiv (A-hc (C ∘ inl))
  module B-unchoose = is-equiv (B-hc (C ∘ inr))

  to = unchoose {n = n} {A ⊔ B} {C}

  from : Π (A ⊔ B) (Trunc n ∘ C) → Trunc n (Π (A ⊔ B) C)
  from f = Trunc-fmap2 Coprod-elim (A-unchoose.g (f ∘ inl)) (B-unchoose.g (f ∘ inr))

  abstract
    to-from-inl' : ∀ f a → to (from f) (inl a) == A-unchoose (A-unchoose.g (f ∘ inl)) a
    to-from-inl' f a = Trunc-elim
      {P = λ f-inl → to (Trunc-fmap2 Coprod-elim f-inl (B-unchoose.g (f ∘ inr))) (inl a) == A-unchoose f-inl a}
      (λ f-inl → Trunc-elim
        {P = λ f-inr → to (Trunc-fmap2 Coprod-elim [ f-inl ] f-inr) (inl a) == [ f-inl a ]}
        (λ f-inr → idp)
        (B-unchoose.g (f ∘ inr)))
      (A-unchoose.g (f ∘ inl))

    to-from-inl : ∀ f a → to (from f) (inl a) == f (inl a)
    to-from-inl f a = to-from-inl' f a ∙ app= (A-unchoose.f-g (f ∘ inl)) a

    to-from-inr' : ∀ f b → to (from f) (inr b) == B-unchoose (B-unchoose.g (f ∘ inr)) b
    to-from-inr' f b = Trunc-elim
      {P = λ f-inr → to (Trunc-fmap2 Coprod-elim (A-unchoose.g (f ∘ inl)) f-inr) (inr b) == B-unchoose f-inr b}
      (λ f-inr → Trunc-elim
        {P = λ f-inl → to (Trunc-fmap2 Coprod-elim f-inl [ f-inr ]) (inr b) == [ f-inr b ]}
        (λ f-inl → idp)
        (A-unchoose.g (f ∘ inl)))
      (B-unchoose.g (f ∘ inr))

    to-from-inr : ∀ f b → to (from f) (inr b) == f (inr b)
    to-from-inr f b = to-from-inr' f b ∙ app= (B-unchoose.f-g (f ∘ inr)) b

    to-from : ∀ f → to (from f) == f
    to-from f = λ= λ{(inl a) → to-from-inl f a; (inr b) → to-from-inr f b}

    from-to : ∀ f → from (to f) == f
    from-to = Trunc-elim
      (λ f →
        Trunc-fmap2 Coprod-elim (A-unchoose.g (λ a → [ f (inl a)])) (B-unchoose.g (λ b → [ f (inr b)]))
          =⟨ ap2 (Trunc-fmap2 Coprod-elim) (A-unchoose.g-f [ f ∘ inl ]) (B-unchoose.g-f [ f ∘ inr ]) ⟩
        [ Coprod-elim (f ∘ inl) (f ∘ inr) ]
          =⟨ ap [_] $ λ= (λ{(inl _) → idp; (inr _) → idp}) ⟩
        [ f ]
          =∎)

equiv-preserves-choice : ∀ {i j} {n} {A : Type i} {B : Type j} (e : A ≃ B) {k}
  → has-choice n A k → has-choice n B k
equiv-preserves-choice {n = n} {A} {B} (f , f-ise) A-hc C = is-eq to from to-from from-to where
  module f = is-equiv f-ise

  A-unchoose = unchoose {n = n} {A} {C ∘ f}
  module A-unchoose = is-equiv (A-hc (C ∘ f))

  to = unchoose {n = n} {B} {C}

  from' : Trunc n (Π A (C ∘ f)) → Trunc n (Π B C)
  from' = Trunc-fmap (λ g' b → transport C (f.f-g b) (g' (f.g b)))

  from : Π B (Trunc n ∘ C) → Trunc n (Π B C)
  from g = from' (A-unchoose.g (g ∘ f))

  abstract
    to-from''' : ∀ (g-f' : Π A (C ∘ f)) {a a'} (path : f.g (f a) == a')
      → transport C (ap f path) (g-f' (f.g (f a))) == g-f' a'
    to-from''' g-f' idp = idp

    to-from'' : ∀ (g-f' : Π A (C ∘ f)) a
      → transport C (f.f-g (f a)) (g-f' (f.g (f a))) == g-f' a
    to-from'' g-f' a =
      transport C (f.f-g (f a)) (g-f' (f.g (f a)))
        =⟨ ! $ ap (λ p → transport C p (g-f' (f.g (f a)))) (f.adj a) ⟩
      transport C (ap f (f.g-f a)) (g-f' (f.g (f a)))
        =⟨ to-from''' g-f' (f.g-f a) ⟩
      g-f' a
        =∎

    to-from' : ∀ g a → to (from g) (f a) == A-unchoose (A-unchoose.g (g ∘ f)) a
    to-from' g a =
      Trunc-elim
        {P = λ g-f → to (from' g-f) (f a) == A-unchoose g-f a}
        (λ g-f' → ap [_] $ to-from'' g-f' a)
        (A-unchoose.g (g ∘ f))

    to-from : ∀ g → to (from g) == g
    to-from g = λ= λ b → transport
      (λ b → to (from g) b == g b)
      (f.f-g b)
      ( to (from g) (f (f.g b))
          =⟨ to-from' g (f.g b) ⟩
        A-unchoose (A-unchoose.g (g ∘ f)) (f.g b)
          =⟨ app= (A-unchoose.f-g (g ∘ f)) (f.g b) ⟩
        g (f (f.g b))
          =∎)

    from-to' : ∀ g {b b'} (path : f (f.g b) == b')
      → transport C path (g (f (f.g b))) == g b'
    from-to' g idp = idp

    from-to : ∀ g → from (to g) == g
    from-to = Trunc-elim
      {P = λ g → from (to g) == g}
      (λ g →
        from' (A-unchoose.g (λ a → [ g (f a) ]))
          =⟨ ap from' (A-unchoose.g-f [ (g ∘ f) ]) ⟩
        from' [ (g ∘ f) ]
          =⟨ ap [_] $ λ= (λ b → from-to' g (f.f-g b)) ⟩
        [ g ]
          =∎)

Fin-has-choice : ∀ (n : ℕ₋₂) {m} l → has-choice n (Fin m) l
Fin-has-choice _ {O} _ = equiv-preserves-choice
  (Fin-equiv-Empty ⁻¹) Empty-has-choice
Fin-has-choice n {S m} l = equiv-preserves-choice
  (Fin-equiv-Coprod ⁻¹) (Coprod-has-choice (Fin-has-choice n l) Unit-has-choice)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

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

-- This module defines Outputs produced by handlers, as well as functions and properties relating
-- these to Yasm Actions.

open import LibraBFT.ImplShared.NetworkMsg
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.KVMap
open import Util.Prelude
open import Yasm.Types

module LibraBFT.ImplShared.Interface.Output where

  data Output : Set where
    --BroadcastEpochChangeProof : EpochChangeProof → List Author → Output -- TODO-1
    BroadcastProposal : ProposalMsg → List Author     → Output
    BroadcastSyncInfo : SyncInfo    → List Author     → Output
    LogErr            : ErrLog                        → Output
    LogInfo           : InfoLog                       → Output
    SendBRP           : Author      → BlockRetrievalResponse → Output
    SendVote          : VoteMsg     → List Author     → Output
  open Output public

  SendVote-inj-v : ∀ {x1 x2 y1 y2} → SendVote x1 y1 ≡ SendVote x2 y2 → x1 ≡ x2
  SendVote-inj-v refl = refl

  SendVote-inj-si : ∀ {x1 x2 y1 y2} → SendVote x1 y1 ≡ SendVote x2 y2 → y1 ≡ y2
  SendVote-inj-si refl = refl

  IsSendVote : Output → Set
  IsSendVote (BroadcastProposal _ _) = ⊥
  IsSendVote (BroadcastSyncInfo _ _) = ⊥
  IsSendVote (LogErr _) = ⊥
  IsSendVote (LogInfo _) = ⊥
  IsSendVote (SendBRP _ _) = ⊥
  IsSendVote (SendVote _ _) = ⊤

  IsBroadcastProposal : Output → Set
  IsBroadcastProposal (BroadcastProposal _ _) = ⊤
  IsBroadcastProposal (BroadcastSyncInfo _ _) = ⊥
  IsBroadcastProposal (LogErr _) = ⊥
  IsBroadcastProposal (LogInfo _) = ⊥
  IsBroadcastProposal (SendBRP _ _) = ⊥
  IsBroadcastProposal (SendVote _ _) = ⊥

  IsBroadcastSyncInfo : Output → Set
  IsBroadcastSyncInfo (BroadcastProposal _ _) = ⊥
  IsBroadcastSyncInfo (BroadcastSyncInfo _ _) = ⊤
  IsBroadcastSyncInfo (LogErr _)              = ⊥
  IsBroadcastSyncInfo (LogInfo _)             = ⊥
  IsBroadcastSyncInfo (SendBRP _ _)           = ⊥
  IsBroadcastSyncInfo (SendVote _ _)          = ⊥

  IsLogErr : Output → Set
  IsLogErr (BroadcastProposal _ _) = ⊥
  IsLogErr (BroadcastSyncInfo _ _) = ⊥
  IsLogErr (LogErr _)            = ⊤
  IsLogErr (LogInfo _)           = ⊥
  IsLogErr (SendBRP _ _)         = ⊥
  IsLogErr (SendVote _ _)        = ⊥

  logErrMB : Output → Maybe ErrLog
  logErrMB (BroadcastProposal _ _) = nothing
  logErrMB (BroadcastSyncInfo _ _) = nothing
  logErrMB (LogErr e)              = just e
  logErrMB (LogInfo _)             = nothing
  logErrMB (SendBRP _ _)           = nothing
  logErrMB (SendVote _ _)          = nothing

  isSendVote? : (out : Output) → Dec (IsSendVote out)
  isSendVote? (BroadcastProposal _ _) = no λ ()
  isSendVote? (BroadcastSyncInfo _ _) = no λ ()
  isSendVote? (LogErr _)            = no λ ()
  isSendVote? (LogInfo _)           = no λ ()
  isSendVote? (SendBRP _ _)         = no λ ()
  isSendVote? (SendVote mv pid)     = yes tt

  isBroadcastProposal? : (out : Output) →  Dec (IsBroadcastProposal out)
  isBroadcastProposal? (BroadcastProposal _ _) = yes tt
  isBroadcastProposal? (BroadcastSyncInfo _ _) = no λ ()
  isBroadcastProposal? (LogErr _)            = no λ ()
  isBroadcastProposal? (LogInfo _)           = no λ ()
  isBroadcastProposal? (SendBRP _ _)         = no λ ()
  isBroadcastProposal? (SendVote _ _)        = no λ ()

  isBroadcastSyncInfo? : (out : Output) →  Dec (IsBroadcastSyncInfo out)
  isBroadcastSyncInfo? (BroadcastProposal _ _) = no λ ()
  isBroadcastSyncInfo? (BroadcastSyncInfo _ _) = yes tt
  isBroadcastSyncInfo? (LogErr _)              = no λ ()
  isBroadcastSyncInfo? (LogInfo _)             = no λ ()
  isBroadcastSyncInfo? (SendBRP _ _)           = no λ ()
  isBroadcastSyncInfo? (SendVote _ _)          = no λ ()

  isLogErr? : (out : Output) → Dec (IsLogErr out)
  isLogErr? (BroadcastProposal x _) = no λ ()
  isLogErr? (BroadcastSyncInfo x _) = no λ ()
  isLogErr? (LogErr x)            = yes tt
  isLogErr? (LogInfo x)           = no λ ()
  isLogErr? (SendBRP _ _)         = no λ ()
  isLogErr? (SendVote x x₁)       = no λ ()

  IsOutputMsg : Output → Set
  IsOutputMsg = IsBroadcastProposal ∪ IsBroadcastSyncInfo ∪ IsSendVote

  isOutputMsg? = isBroadcastProposal? ∪? (isBroadcastSyncInfo? ∪? isSendVote?)

  data _Msg∈Out_ : NetworkMsg → Output → Set where
    inBP : ∀ {pm pids} → P pm Msg∈Out BroadcastProposal pm pids
    inSV : ∀ {vm pids} → V vm Msg∈Out SendVote vm pids

  sendVote∉Output : ∀ {vm pid outs} → List-filter isSendVote? outs ≡ [] → ¬ (SendVote vm pid ∈ outs)
  sendVote∉Output () (here refl)
  sendVote∉Output{outs = x ∷ outs'} eq (there vm∈outs)
     with isSendVote? x
  ... | no proof = sendVote∉Output eq vm∈outs

  -- Note: the SystemModel allows anyone to receive any message sent, so intended recipient is ignored;
  -- it is included in the model only to facilitate future work on liveness properties, when we will need
  -- assumptions about message delivery between honest peers.
  outputToActions : RoundManager → Output → List (Action NetworkMsg)
  outputToActions rm (BroadcastProposal p rcvrs) = List-map (const (send (P p))) rcvrs
  outputToActions _  (BroadcastSyncInfo _ _) = []
  outputToActions _  (LogErr x)            = []
  outputToActions _  (LogInfo x)           = []
  outputToActions _  (SendVote vm rcvrs)   = List-map (const (send (V vm))) rcvrs
  outputToActions _  (SendBRP p brr)       = [] -- TODO-1: Update `NetworkMsg`

  outputsToActions : ∀ {State} → List Output → List (Action NetworkMsg)
  outputsToActions {st} = concat ∘ List-map (outputToActions st)

  -- Lemmas about `outputsToActions`
  outputToActions-sendVote∉actions
    : ∀ {out vm st} → ¬ (IsSendVote out) → ¬ (send (V vm) ∈ outputToActions st out)
  outputToActions-sendVote∉actions {BroadcastProposal pm rcvrs}{vm}{st} ¬sv m∈acts =
    help rcvrs m∈acts
    where
    help : ∀ xs → ¬ (send (V vm) ∈ List-map (const (send (P pm))) xs)
    help (x ∷ xs) (there m∈acts) = help xs m∈acts
  outputToActions-sendVote∉actions {SendVote _ _} ¬sv m∈acts = ¬sv tt

  outputToActions-m∈sendVoteList
    : ∀ {m vm rcvrs} → send m ∈ List-map (const $ send (V vm)) rcvrs
      → m Msg∈Out SendVote vm rcvrs
  outputToActions-m∈sendVoteList {.(V vm)} {vm} {x ∷ rcvrs} (here refl) = inSV
  outputToActions-m∈sendVoteList {m} {vm} {x ∷ rcvrs} (there m∈svl)
    with outputToActions-m∈sendVoteList{rcvrs = rcvrs} m∈svl
  ... | inSV = inSV

  outputToActions-m∈sendProposalList
    : ∀ {m pm rcvrs} → send m ∈ List-map (const $ send (P pm)) rcvrs
      → m Msg∈Out BroadcastProposal pm rcvrs
  outputToActions-m∈sendProposalList {.(P pm)} {pm} {x ∷ rcvrs} (here refl) = inBP
  outputToActions-m∈sendProposalList {m} {pm} {x ∷ rcvrs} (there m∈spl)
    with outputToActions-m∈sendProposalList {rcvrs = rcvrs} m∈spl
  ... | inBP = inBP

  sendVote∉actions
    : ∀ {outs vm st} → [] ≡ List-filter isSendVote? outs → ¬ (send (V vm) ∈ outputsToActions{st} outs)
  sendVote∉actions {[]} {st = st} outs≡ ()
  sendVote∉actions {x ∷ outs} {st = st} outs≡ m∈acts
    with Any-++⁻ (outputToActions st x) m∈acts
  ... | Left m∈[]
    with isSendVote? x
  ...| no  proof = outputToActions-sendVote∉actions {st = st} proof m∈[]
  sendVote∉actions {x ∷ outs} {st = st} outs≡ m∈acts | Right m∈acts'
    with isSendVote? x
  ...| no  proof = sendVote∉actions{outs = outs}{st = st} outs≡ m∈acts'

  sendVote∈actions
    : ∀ {vm vm' pids outs st} → SendVote vm pids ∷ [] ≡ List-filter isSendVote? outs
      → send (V vm') ∈ outputsToActions{st} outs
      → vm' ≡ vm
  sendVote∈actions {outs = (BroadcastProposal x rcvrs) ∷ outs}{st = st} outs≡ m∈acts
    with Any-++⁻ (outputToActions st (BroadcastProposal x rcvrs)) m∈acts
  ... | Left m∈[] = ⊥-elim (outputToActions-sendVote∉actions{out = BroadcastProposal x rcvrs}{st = st} id m∈[])
  ... | Right m∈acts' = sendVote∈actions{outs = outs}{st = st} outs≡ m∈acts'
  sendVote∈actions {outs = (BroadcastSyncInfo x rcvrs) ∷ outs}{st = st} outs≡ m∈acts =
    sendVote∈actions{outs = outs}{st = st} outs≡ m∈acts
  sendVote∈actions {outs = LogErr x ∷ outs}{st = st} outs≡ m∈acts =
    sendVote∈actions{outs = outs}{st = st} outs≡ m∈acts
  sendVote∈actions {outs = LogInfo x ∷ outs}{st = st} outs≡ m∈acts =
    sendVote∈actions{outs = outs}{st = st} outs≡ m∈acts
  sendVote∈actions {vm}{vm'}{outs = SendBRP pid brr ∷ outs}{st = st} outs≡ m∈acts =
    sendVote∈actions{outs = outs}{st = st} outs≡ m∈acts
  sendVote∈actions {vm}{vm'}{outs = SendVote vm“ pids' ∷ outs}{st = st} outs≡ m∈acts
    with ∷-injective outs≡
  ...| refl , tl≡
    with Any-++⁻ (List-map (const (send (V vm“))) pids') m∈acts
  ... | Right m∈[] = ⊥-elim (sendVote∉actions{outs = outs}{st = st} tl≡ m∈[])
  ... | Left m∈acts' = help pids' m∈acts'
    where
    help : ∀ pids → send (V vm') ∈ List-map (const (send (V vm“))) pids → vm' ≡ vm“
    help (_ ∷ pids) (here refl) = refl
    help (_ ∷ pids) (there m∈acts) = help pids m∈acts

  sendMsg∈actions
    : ∀ {outs m st} → send m ∈ outputsToActions{st} outs
      → Σ[ out ∈ Output ] (out ∈ outs × m Msg∈Out out)
  sendMsg∈actions {BroadcastProposal pm rcvrs ∷ outs} {m} {st} m∈acts
    with Any-++⁻ (List-map (const $ send (P pm)) rcvrs) m∈acts
  ... | Left m∈bpl =
    BroadcastProposal pm rcvrs , here refl , outputToActions-m∈sendProposalList m∈bpl
  ... | Right m∈acts'
    with sendMsg∈actions{outs}{m}{st} m∈acts'
  ... | out , out∈outs , m∈out = out , there out∈outs , m∈out
  -- NOTE: When we represent sending `BroadcastSyncInfo` as an action, this will require updating
  sendMsg∈actions {BroadcastSyncInfo _ _ ∷ outs} {m} {st} m∈acts
    with sendMsg∈actions{outs}{m}{st} m∈acts
  ...| out , out∈outs , m∈out = out , there out∈outs , m∈out
  sendMsg∈actions {LogErr _ ∷ outs} {m} {st} m∈acts
    with sendMsg∈actions{outs}{m}{st} m∈acts
  ...| out , out∈outs , m∈out = out , there out∈outs , m∈out
  sendMsg∈actions {LogInfo _ ∷ outs} {m} {st} m∈acts
    with sendMsg∈actions{outs}{m}{st} m∈acts
  ...| out , out∈outs , m∈out = out , there out∈outs , m∈out
  sendMsg∈actions {SendBRP pid brr ∷ outs} {m} {st} m∈acts
     with sendMsg∈actions{outs}{m}{st} m∈acts
  ...| out , out∈outs , m∈out = out , there out∈outs , m∈out
  sendMsg∈actions {SendVote vm rcvrs ∷ outs} {m} {st} m∈acts
    with Any-++⁻ (List-map (const (send (V vm))) rcvrs) m∈acts
  ... | Left m∈svl =
    SendVote vm rcvrs , here refl , outputToActions-m∈sendVoteList m∈svl
  ... | Right m∈acts'
    with sendMsg∈actions{outs}{m}{st} m∈acts'
  ... | out , out∈outs , m∈out = out , there out∈outs , m∈out


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- This module re-exports all Basics/* modules for convenience.     --
-- Note that both Basics.Nat and Basics.Ordering define ≥ operator. --
-- Here we re-export the one from Basics.Ordering as it will be     --
-- used most of the time.                                           --
-- This module also defines two type synonyms that will be helpful  --
-- when working on heaps: Rank and Priority.                        --
----------------------------------------------------------------------

module Basics where

open import Basics.Bool      public
open import Basics.Nat       public hiding (_≥_)
open import Basics.Ordering  public
open import Basics.Reasoning public

-- Rank of a weight biased leftist heap is defined as number of nodes
-- in a heap. In other words it is size of a tree used to represent a
-- heap.
Rank : Set
Rank = Nat

-- Priority assigned to elements stored in a Heap.
--
-- CONVENTION: Lower number means higher Priority. Therefore the
-- highest Priority is zero. It will sometimes be more convenient not
-- to use this inversed terminology. We will then use terms "smaller"
-- and "greater" (in contrast to "lower" and "higher"). Example:
-- Priority 3 is higher than 5, but 3 is smaller than 5.
Priority : Set
Priority = Nat

-- Note that both Rank and Priority are Nat, which allows us to
-- operate on them with functions that work for Nat.

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
module Example where

open import Data.List

-- reverse
rev : ∀ {a} {A : Set a} → List A → List A
rev [] = []
rev (x ∷ xs) = rev xs ++ [ x ]

-- https://code.google.com/p/agda/issues/detail?id=1252 暫定対策
rev' = rev
{-# COMPILED_EXPORT rev' rev' #-}

private
  open import Relation.Binary.PropositionalEquality

  -- reverse2回で元に戻る証明
  lemma : ∀ {a} {A : Set a} (x : A) (xs : List A) → rev (xs ∷ʳ x) ≡ x ∷ rev xs
  lemma x [] = refl
  lemma x (_ ∷ xs)
    rewrite lemma x xs
          = refl

  revrev-is-id : ∀ {a} {A : Set a} (xs : List A) → rev (rev xs) ≡ xs
  revrev-is-id [] = refl
  revrev-is-id (x ∷ xs)
    rewrite lemma x (rev xs)
          | revrev-is-id xs
          = refl

open import Data.Empty

head : ∀ {a} {A : Set a} (xs : List A) → {xs≢[] : xs ≢ []} → A
head [] {xs≠[]} = ⊥-elim (xs≠[] refl)
head (x ∷ xs) = x
{-
{-# COMPILED_EXPORT head safeHead' #-}
-- エラーになる
-- The type _≡_ cannot be translated to a Haskell type.
-- when checking the pragma COMPILED_EXPORT head' safeHead
--
-- つまり，証明オブジェクトを取るような関数は，
-- そのままではCOMPILED_EXPORTできないことが多い
-}

open import Data.Maybe

head' : ∀ {a} {A : Set a} (xs : List A) → Maybe A
head' = go where
  go : ∀ {a} {A : Set a} (xs : List A) → Maybe A
  go [] = nothing
  go (x ∷ xs) = just (head (x ∷ xs) {λ ()})
{-# COMPILED_EXPORT head' safeHead' #-}
-- つまり，安全なheadを使うには，
-- 安全なものだけ渡せるようにしてjustで結果が得られ，
-- それ以外についてはnothingになるように，
-- 適切にラップしないとCOMPILED_EXPORTできない．

max_stars_repo_name: notogawa/agda-haskell-example

max_issues_repo_name: notogawa/agda-haskell-example

max_forks_repo_name: notogawa/agda-haskell-example


text:
module Issue4373.A where

postulate
  T : Set
  instance t : T

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Languages.ILL.TypeSyntax where

open import bool

open import Utils.HaskellTypes

{-# IMPORT Languages.ILL.TypeSyntax #-}

data Type : Set where
  TVar : String → Type
  Top : Type
  Imp : Type → Type → Type
  Tensor : Type → Type → Type
  Bang : Type → Type

{-# COMPILED_DATA Type Languages.ILL.TypeSyntax.Type
                       Languages.ILL.TypeSyntax.TVar
                       Languages.ILL.TypeSyntax.Top
                       Languages.ILL.TypeSyntax.Imp
                       Languages.ILL.TypeSyntax.Tensor
                       Languages.ILL.TypeSyntax.Bang #-}

_eq-type_ : Type → Type → 𝔹
(TVar _) eq-type (TVar _) = tt
Top eq-type Top = tt
(Imp A C) eq-type (Imp B D) = (A eq-type B) && (C eq-type D)
(Tensor A C) eq-type (Tensor B D) = (A eq-type B) && (C eq-type D)
(Bang A) eq-type (Bang B) = A eq-type B
_ eq-type _ = ff

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
-- Andreas, 2017-01-21, issue #2422 overloading inherited projections

-- {-# OPTIONS -v tc.proj.amb:100 #-}
-- {-# OPTIONS -v tc.mod.apply:100 #-}

postulate
  A : Set

record R : Set where
  field f : A

record S : Set where
  field r : R
  open R r public
  -- The inherited projection (in the eyes of the scope checker) S.f
  -- is actually a composition of projections R.f ∘ S.r
  -- s .S.f = s .S.r .R.f

open R  -- works without this
open S

test : S → A
test s = f s
  -- f is not really a projection, but a composition of projections
  -- it would be nice if overloading is still allowed.

-- Error WAS:
-- Cannot resolve overloaded projection f because no matching candidate found

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{- Type class for functors. -}
module CategoryTheory.Functor where

open import CategoryTheory.Categories
open import Relation.Binary

-- Functor between two categories
record Functor {n} (ℂ : Category n) (𝔻 : Category n) : Set (lsuc n) where
    private module ℂ = Category ℂ
    private module 𝔻 = Category 𝔻
    field
        -- || Definitions
        -- Object map
        omap : ℂ.obj -> 𝔻.obj
        -- Arrow map
        fmap : ∀{A B : ℂ.obj} -> (A ℂ.~> B) -> (omap A 𝔻.~> omap B)

        -- || Laws
        -- Functor preseres identities
        fmap-id   : ∀{A : ℂ.obj} -> fmap (ℂ.id {A}) 𝔻.≈ 𝔻.id
        -- Functor preserves composition
        fmap-∘    : ∀{A B C : ℂ.obj} {g : B ℂ.~> C} {f : A ℂ.~> B}
                 -> fmap (g ℂ.∘ f) 𝔻.≈ fmap g 𝔻.∘ fmap f
        -- Congruence of equality and fmap
        fmap-cong : ∀{A B : ℂ.obj} {f f′ : A ℂ.~> B}
                -> f ℂ.≈ f′ -> fmap f 𝔻.≈ fmap f′

-- Type synonym for endofunctors
Endofunctor : ∀{n} -> Category n -> Set (lsuc n)
Endofunctor ℂ = Functor ℂ ℂ

-- Identity functor
I : ∀ {n} {ℂ : Category n} -> Endofunctor ℂ
I {n} {ℂ} = record { omap = λ a → a
               ; fmap = λ a → a
               ; fmap-id = IsEquivalence.refl (Category.≈-equiv ℂ)
               ; fmap-∘ =  IsEquivalence.refl (Category.≈-equiv ℂ)
               ; fmap-cong = λ p → p }

-- Functors are closed under composition.
infixl 40 _◯_
_◯_ : ∀ {n} {𝔸 𝔹 ℂ : Category n} -> Functor 𝔹 ℂ -> Functor 𝔸 𝔹 -> Functor 𝔸 ℂ
_◯_ {n} {𝔸} {𝔹} {ℂ} G F =
    record { omap = λ a → G.omap (F.omap a)
           ; fmap = λ f → G.fmap (F.fmap f)
           ; fmap-id = fmap-◯-id
           ; fmap-∘ = fmap-◯-∘
           ; fmap-cong = λ p → G.fmap-cong (F.fmap-cong p)}
    where private module F = Functor F
          private module G = Functor G
          private module 𝔸 = Category 𝔸
          private module 𝔹 = Category 𝔹
          open Category ℂ

          fmap-◯-id : ∀{A : 𝔸.obj} -> G.fmap (F.fmap (𝔸.id {A})) ≈ id
          fmap-◯-id {A} =
                begin
                    G.fmap (F.fmap (𝔸.id))
                ≈⟨ G.fmap-cong (F.fmap-id) ⟩
                    G.fmap (𝔹.id)
                ≈⟨ G.fmap-id ⟩
                    id
                ∎
          fmap-◯-∘ : ∀{A B C : 𝔸.obj} {g : B 𝔸.~> C} {f : A 𝔸.~> B}
                   -> G.fmap (F.fmap (g 𝔸.∘ f)) ≈
                      G.fmap (F.fmap g) ∘ G.fmap (F.fmap f)
          fmap-◯-∘ {A} {g = g} {f = f} =
                begin
                    G.fmap (F.fmap (g 𝔸.∘ f))
                ≈⟨ G.fmap-cong (F.fmap-∘) ⟩
                    G.fmap ((F.fmap g) 𝔹.∘ (F.fmap f))
                ≈⟨ G.fmap-∘ ⟩
                    G.fmap (F.fmap g) ∘ G.fmap (F.fmap f)
                ∎

-- Endofunctor tensor product
infixl 40 _⨂_
_⨂_ : ∀ {n} {ℂ : Category n} -> Endofunctor ℂ -> Endofunctor ℂ -> Endofunctor ℂ
(T ⨂ S) = T ◯ S

-- Square and cube of an endofunctor
_² : ∀ {n} {ℂ : Category n} -> Endofunctor ℂ -> Endofunctor ℂ
F ² = F ⨂ F

_³ : ∀ {n} {ℂ : Category n} -> Endofunctor ℂ -> Endofunctor ℂ
F ³ = F ⨂ F ⨂ F

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Issue3579 where

open import Agda.Builtin.String
open import Agda.Builtin.Reflection

data _==_ {A : Set} (a : A) : A → Set where
  refl : a == a

{-# BUILTIN EQUALITY _==_ #-}

max_forks_repo_name: Agda-zh/agda


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

module Literals.Number where

open import Agda.Builtin.FromNat public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/masters-thesis

max_forks_repo_name: oisdk/masters-thesis


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

open import BTree {A}
open import BTree.Equality {A}
open import BTree.Equality.Properties {A}
open import BTree.Complete.Alternative {A}
open import Data.Sum renaming (_⊎_ to _∨_)

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

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

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

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; ⊨a-resp-≡³ ; ⊨a-impl-⊨b ; ⊨b-impl-⊨a
  ; _,_ ; inb ; on-bnode ; bnodes )
open import Web.Semantic.DL.Category.Object using ( Object ; IN ; iface )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; _,_ ; BN ; impl ; _⊑_ ; _≣_ )
open import Web.Semantic.DL.KB using ( _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox ; _,_ )
open import Web.Semantic.DL.TBox.Interp using ( Δ )
open import Web.Semantic.Util using ( _⊕_⊕_ ; inode )

module Web.Semantic.DL.Category.Properties.Equivalence
  {Σ : Signature} {S T : TBox Σ} where

⊑-refl : ∀ {A B : Object S T} (F : A ⇒ B) → (F ⊑ F)
⊑-refl F I I⊨STA I⊨F = ⊨a-impl-⊨b I (impl F) I⊨F

⊑-trans : ∀ {A B : Object S T} (F G H : A ⇒ B) → (F ⊑ G) → (G ⊑ H) → (F ⊑ H)
⊑-trans {A} {B} F G H F⊑G G⊑H I I⊨STA I⊨F = (g , I⊨H) where

  f : BN G → Δ ⌊ I ⌋
  f = inb (F⊑G I I⊨STA I⊨F)

  J : Interp Σ (IN A ⊕ BN G ⊕ IN B)
  J = bnodes I f

  J⊨STA : inode * J ⊨ (S , T) , iface A
  J⊨STA = I⊨STA

  J⊨G : J ⊨a impl G
  J⊨G = ⊨b-impl-⊨a (F⊑G I I⊨STA I⊨F)

  g : BN H → Δ ⌊ I ⌋
  g = inb (G⊑H J J⊨STA J⊨G)

  K : Interp Σ (IN A ⊕ BN H ⊕ IN B)
  K = bnodes J g

  K⊨H : K ⊨a impl H
  K⊨H = ⊨b-impl-⊨a (G⊑H J J⊨STA J⊨G)

  I⊨H : bnodes I g ⊨a impl H
  I⊨H = ⊨a-resp-≡³ K (on-bnode g (ind I)) refl (impl H) K⊨H

≣-refl : ∀ {A B : Object S T} (F : A ⇒ B) → (F ≣ F)
≣-refl F = (⊑-refl F , ⊑-refl F)

≣-sym :  ∀ {A B : Object S T} {F G : A ⇒ B} → (F ≣ G) → (G ≣ F)
≣-sym (F⊑G , G⊑F) = (G⊑F , F⊑G)

≣-trans :  ∀ {A B : Object S T} {F G H : A ⇒ B} → (F ≣ G) → (G ≣ H) → (F ≣ H)
≣-trans {A} {B} {F} {G} {H} (F⊑G , G⊑F) (G⊑H , H⊑G) =
  (⊑-trans F G H F⊑G G⊑H , ⊑-trans H G F H⊑G G⊑F)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties imply others
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Relation.Binary.Consequences.

module Relation.Binary.Consequences.Core where

open import Relation.Binary.Core
open import Data.Product

subst⟶resp₂ : ∀ {a ℓ p} {A : Set a} {∼ : Rel A ℓ}
              (P : Rel A p) → Substitutive ∼ p → P Respects₂ ∼
subst⟶resp₂ {∼ = ∼} P subst =
  (λ {x _ _} y'∼y Pxy' → subst (P x)         y'∼y Pxy') ,
  (λ {y _ _} x'∼x Px'y → subst (λ x → P x y) x'∼x Px'y)


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

module Data.Binary.Addition where

open import Data.Binary.Definition
open import Data.Binary.Increment

add₁ : 𝔹 → 𝔹 → 𝔹
add₂ : 𝔹 → 𝔹 → 𝔹

add₁ 0ᵇ      ys      = inc ys
add₁ (1ᵇ xs) 0ᵇ      = 2ᵇ xs
add₁ (2ᵇ xs) 0ᵇ      = 1ᵇ inc xs
add₁ (1ᵇ xs) (1ᵇ ys) = 1ᵇ add₁ xs ys
add₁ (1ᵇ xs) (2ᵇ ys) = 2ᵇ add₁ xs ys
add₁ (2ᵇ xs) (1ᵇ ys) = 2ᵇ add₁ xs ys
add₁ (2ᵇ xs) (2ᵇ ys) = 1ᵇ add₂ xs ys

add₂ 0ᵇ      0ᵇ      = 2ᵇ 0ᵇ
add₂ 0ᵇ      (1ᵇ ys) = 1ᵇ inc ys
add₂ 0ᵇ      (2ᵇ ys) = 2ᵇ inc ys
add₂ (1ᵇ xs) 0ᵇ      = 1ᵇ inc xs
add₂ (2ᵇ xs) 0ᵇ      = 2ᵇ inc xs
add₂ (1ᵇ xs) (1ᵇ ys) = 2ᵇ add₁ xs ys
add₂ (1ᵇ xs) (2ᵇ ys) = 1ᵇ add₂ xs ys
add₂ (2ᵇ xs) (1ᵇ ys) = 1ᵇ add₂ xs ys
add₂ (2ᵇ xs) (2ᵇ ys) = 2ᵇ add₂ xs ys

infixl 6 _+_
_+_ : 𝔹 → 𝔹 → 𝔹
0ᵇ    + ys    = ys
1ᵇ xs + 0ᵇ    = 1ᵇ xs
2ᵇ xs + 0ᵇ    = 2ᵇ xs
1ᵇ xs + 1ᵇ ys = 2ᵇ (xs + ys)
1ᵇ xs + 2ᵇ ys = 1ᵇ add₁ xs ys
2ᵇ xs + 1ᵇ ys = 1ᵇ add₁ xs ys
2ᵇ xs + 2ᵇ ys = 2ᵇ add₁ xs ys

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2020-09-24
-- Equal
-- Author: dplaindoux
--

module Equal where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Bool using (Bool; true; false)

infix 30 _=?_

data Type : Set where
    nat  : Type

▲_ : Type → Set
▲ nat  = ℕ

_=?_ : { a : Type } → ▲ a → ▲ a → Bool

_=?_ {nat} zero zero       = true
_=?_ {nat} (suc m) (suc n) = m =? n
_=?_ {nat} _ _             = false

Nat :
  ∀self(P : Nat → Set) →
  ∀(zero : P(λz. λs. z)) →
  ∀(succ : ∀(n : Nat) → P (λz. λs. s n)) →
  P self

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" in multiple Setoids
------------------------------------------------------------------------

-- Example use:
--
--   open import Data.Maybe
--   open import Relation.Binary.Reasoning.MultiSetoid
--
--   begin⟨ S ⟩
--     x ≈⟨ drop-just (begin⟨ setoid S ⟩
--          just x ≈⟨ justx≈mz ⟩
--          mz     ≈⟨ mz≈justy ⟩
--          just y ∎)⟩
--     y ≈⟨ y≈z ⟩
--     z ∎

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

module Relation.Binary.Reasoning.MultiSetoid where

open import Relation.Binary
open import Relation.Binary.Reasoning.Setoid as EqR using (_IsRelatedTo_)
open import Relation.Binary.PropositionalEquality

open Setoid renaming (_≈_ to [_]_≈_)

infix 1 begin⟨_⟩_
infixr 2 _≈⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix 3 _∎

begin⟨_⟩_ : ∀ {c l} (S : Setoid c l) {x y} → _IsRelatedTo_ S x y → [ S ] x ≈ y
begin⟨_⟩_ S p = EqR.begin_ S p

_≈⟨_⟩_ : ∀ {c l} {S : Setoid c l} x {y z} → [ S ] x ≈ y → _IsRelatedTo_ S y z → _IsRelatedTo_ S x z
_≈⟨_⟩_ {S = S} = EqR._≈⟨_⟩_ S

_≡⟨_⟩_ : ∀ {c l} {S : Setoid c l} x {y z} → x ≡ y → _IsRelatedTo_ S y z → _IsRelatedTo_ S x z
_≡⟨_⟩_ {S = S} = EqR._≡⟨_⟩_ S

_≡˘⟨_⟩_ : ∀ {c l} {S : Setoid c l} x {y z} → y ≡ x → _IsRelatedTo_ S y z → _IsRelatedTo_ S x z
_≡˘⟨_⟩_ {S = S} = EqR._≡˘⟨_⟩_ S

_≡⟨⟩_ : ∀ {c l} {S : Setoid c l} x {y} → _IsRelatedTo_ S x y → _IsRelatedTo_ S x y
_≡⟨⟩_ {S = S} = EqR._≡⟨⟩_ S

_∎ : ∀ {c l} {S : Setoid c l} x → _IsRelatedTo_ S x x
_∎ {S = S} = EqR._∎ S


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Lists.Lists
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.BinaryNaturals.Definition
open import Numbers.BinaryNaturals.Addition
open import Numbers.BinaryNaturals.SubtractionGo
open import Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalRight
open import Orders.Total.Definition
open import Semirings.Definition
open import Maybe

module Numbers.BinaryNaturals.Subtraction where

private
  aMinusAGo : (a : BinNat) → mapMaybe canonical (go zero a a) ≡ yes []
  aMinusAGo [] = refl
  aMinusAGo (zero :: a) with aMinusAGo a
  ... | bl with go zero a a
  aMinusAGo (zero :: a) | bl | yes x rewrite yesInjective bl = refl
  aMinusAGo (one :: a) with aMinusAGo a
  ... | bl with go zero a a
  aMinusAGo (one :: a) | bl | yes x rewrite yesInjective bl = refl

aMinusALemma : (a : BinNat) → mapMaybe canonical (mapMaybe (_::_ zero) (go zero a a)) ≡ yes []
aMinusALemma a with inspect (go zero a a)
aMinusALemma a | no with≡ x with aMinusAGo a
... | r rewrite x = exFalso (noNotYes r)
aMinusALemma a | yes xs with≡ pr with inspect (canonical xs)
aMinusALemma a | yes xs with≡ pr | [] with≡ pr2 rewrite pr | pr2 = refl
aMinusALemma a | yes xs with≡ pr | (x :: t) with≡ pr2 with aMinusAGo a
... | b rewrite pr | pr2 = exFalso (nonEmptyNotEmpty (yesInjective b))

aMinusA : (a : BinNat) → mapMaybe canonical (a -B a) ≡ yes []
aMinusA [] = refl
aMinusA (zero :: a) = aMinusALemma a
aMinusA (one :: a) = aMinusALemma a

goOne : (a b : BinNat) → mapMaybe canonical (go one (incr a) b) ≡ mapMaybe canonical (go zero a b)
goOne [] [] = refl
goOne [] (zero :: b) with inspect (go zero [] b)
goOne [] (zero :: b) | no with≡ pr rewrite pr = refl
goOne [] (zero :: b) | yes x with≡ pr with goZeroEmpty b pr
... | t with inspect (canonical x)
goOne [] (zero :: b) | yes x with≡ pr | t | [] with≡ pr2 rewrite pr | pr2 = refl
goOne [] (zero :: b) | yes x with≡ pr | t | (x₁ :: y) with≡ pr2 with goZeroEmpty' b pr
... | bl = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr2) bl))
goOne [] (one :: b) with inspect (go one [] b)
goOne [] (one :: b) | no with≡ pr rewrite pr = refl
goOne [] (one :: b) | yes x with≡ pr = exFalso (goOneEmpty b pr)
goOne (zero :: a) [] = refl
goOne (zero :: a) (zero :: b) = refl
goOne (zero :: a) (one :: b) = refl
goOne (one :: a) [] with inspect (go one (incr a) [])
goOne (one :: a) [] | no with≡ pr with goOne a []
... | bl rewrite pr | goEmpty a = exFalso (noNotYes bl)
goOne (one :: a) [] | yes y with≡ pr with goOne a []
... | bl rewrite pr = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity bl (applyEquality (mapMaybe canonical) (goEmpty a))))
goOne (one :: a) (zero :: b) with inspect (go zero a b)
goOne (one :: a) (zero :: b) | no with≡ pr with inspect (go one (incr a) b)
goOne (one :: a) (zero :: b) | no with≡ pr | no with≡ x rewrite pr | x = refl
goOne (one :: a) (zero :: b) | no with≡ pr | yes y with≡ x with goOne a b
... | f rewrite pr | x = exFalso (noNotYes (equalityCommutative f))
goOne (one :: a) (zero :: b) | yes y with≡ pr with inspect (go one (incr a) b)
goOne (one :: a) (zero :: b) | yes y with≡ pr | no with≡ x with goOne a b
... | f rewrite pr | x = exFalso (noNotYes f)
goOne (one :: a) (zero :: b) | yes y with≡ pr | yes z with≡ x rewrite pr | x = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative x)) (goOne a b)) (applyEquality (mapMaybe canonical) pr)))
goOne (one :: a) (one :: b) with inspect (go zero a b)
goOne (one :: a) (one :: b) | no with≡ pr with inspect (go one (incr a) b)
goOne (one :: a) (one :: b) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
goOne (one :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr)) (transitivity (equalityCommutative (goOne a b)) (applyEquality (mapMaybe canonical) pr2))))
goOne (one :: a) (one :: b) | yes y with≡ pr with inspect (go one (incr a) b)
goOne (one :: a) (one :: b) | yes y with≡ pr | yes z with≡ pr2 rewrite pr | pr2 = applyEquality yes t
  where
    u : canonical z ≡ canonical y
    u = yesInjective (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (goOne a b)) (applyEquality (mapMaybe canonical) pr))
    t : canonical (zero :: z) ≡ canonical (zero :: y)
    t with inspect (canonical z)
    t | [] with≡ pr1 rewrite equalityCommutative u | pr1 = refl
    t | (x :: bl) with≡ pr rewrite equalityCommutative u | pr = refl
goOne (one :: a) (one :: b) | yes y with≡ pr | no with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goOne a b) (applyEquality (mapMaybe canonical) pr))))

plusThenMinus : (a b : BinNat) → mapMaybe canonical ((a +B b) -B b) ≡ yes (canonical a)
plusThenMinus [] b = aMinusA b
plusThenMinus (zero :: a) [] = refl
plusThenMinus (zero :: a) (zero :: b) = t
  where
    t : mapMaybe canonical (mapMaybe (zero ::_) (go zero (a +B b) b)) ≡ yes (canonical (zero :: a))
    t with inspect (go zero (a +B b) b)
    t | no with≡ x with plusThenMinus a b
    ... | bl rewrite x = exFalso (noNotYes bl)
    t | yes y with≡ x with plusThenMinus a b
    ... | f rewrite x = applyEquality yes u
      where
        u : canonical (zero :: y) ≡ canonical (zero :: a)
        u with inspect (canonical y)
        u | [] with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
        u | (x :: bl) with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
plusThenMinus (zero :: a) (one :: b) = t
  where
    t : mapMaybe canonical (mapMaybe (zero ::_) (go zero (a +B b) b)) ≡ yes (canonical (zero :: a))
    t with inspect (go zero (a +B b) b)
    t | no with≡ x with plusThenMinus a b
    ... | bl rewrite x = exFalso (noNotYes bl)
    t | yes y with≡ x with plusThenMinus a b
    ... | f rewrite x = applyEquality yes u
      where
        u : canonical (zero :: y) ≡ canonical (zero :: a)
        u with inspect (canonical y)
        u | [] with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
        u | (x :: bl) with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
plusThenMinus (one :: a) [] = refl
plusThenMinus (one :: a) (zero :: b) = t
  where
    t : mapMaybe canonical (mapMaybe (_::_ one) (go zero (a +B b) b)) ≡ yes (one :: canonical a)
    t with inspect (go zero (a +B b) b)
    t | no with≡ x with plusThenMinus a b
    ... | bl rewrite x = exFalso (noNotYes bl)
    t | yes y with≡ x with plusThenMinus a b
    ... | bl rewrite x = applyEquality (λ i → yes (one :: i)) (yesInjective bl)
plusThenMinus (one :: a) (one :: b) = t
  where
    t : mapMaybe canonical (mapMaybe (_::_ one) (go one (incr (a +B b)) b)) ≡ yes (one :: canonical a)
    t with inspect (go one (incr (a +B b)) b)
    t | no with≡ x with goOne (a +B b) b
    ... | f rewrite x | plusThenMinus a b = exFalso (noNotYes f)
    t | yes y with≡ x with goOne (a +B b) b
    ... | f rewrite x | plusThenMinus a b = applyEquality (λ i → yes (one :: i)) (yesInjective f)

subLemma : (a b : ℕ) → a <N b → succ (a +N a) <N b +N b
subLemma a b a<b with TotalOrder.totality ℕTotalOrder (succ (a +N a)) (b +N b)
subLemma a b a<b | inl (inl x) = x
subLemma a b a<b | inl (inr x) = exFalso (noIntegersBetweenXAndSuccX (a +N a) (addStrongInequalities a<b a<b) x)
subLemma a b a<b | inr x = exFalso (parity a b (transitivity (applyEquality (succ a +N_) (Semiring.sumZeroRight ℕSemiring a)) (transitivity x (applyEquality (b +N_) (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))))))

subLemma2 : (a b : ℕ) → a <N b → 2 *N a <N succ (2 *N b)
subLemma2 a b a<b with TotalOrder.totality ℕTotalOrder (2 *N a) (succ (2 *N b))
subLemma2 a b a<b | inl (inl x) = x
subLemma2 a b a<b | inl (inr x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder x (TotalOrder.<Transitive ℕTotalOrder (lessRespectsMultiplicationLeft a b 2 a<b (le 1 refl)) (le 0 refl))))
subLemma2 a b a<b | inr x = exFalso (parity b a (equalityCommutative x))

subtraction : (a b : BinNat) → a -B b ≡ no → binNatToN a <N binNatToN b
subtraction' : (a b : BinNat) → go one a b ≡ no → (binNatToN a <N binNatToN b) || (binNatToN a ≡ binNatToN b)

subtraction' [] [] pr = inr refl
subtraction' [] (x :: b) pr with TotalOrder.totality ℕTotalOrder 0 (binNatToN (x :: b))
subtraction' [] (x :: b) pr | inl (inl x₁) = inl x₁
subtraction' [] (x :: b) pr | inr x₁ = inr x₁
subtraction' (zero :: a) [] pr with subtraction' a [] (mapMaybePreservesNo pr)
subtraction' (zero :: a) [] pr | inr x rewrite x = inr refl
subtraction' (zero :: a) (zero :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
subtraction' (zero :: a) (zero :: b) pr | inl x = inl (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 x (le 1 refl))
subtraction' (zero :: a) (zero :: b) pr | inr x rewrite x = inr refl
subtraction' (zero :: a) (one :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
subtraction' (zero :: a) (one :: b) pr | inl x = inl (subLemma2 (binNatToN a) (binNatToN b) x)
subtraction' (zero :: a) (one :: b) pr | inr x rewrite x = inl (le zero refl)
subtraction' (one :: a) (zero :: b) pr with subtraction a b (mapMaybePreservesNo pr)
... | t rewrite Semiring.sumZeroRight ℕSemiring (binNatToN a) | Semiring.sumZeroRight ℕSemiring (binNatToN b) = inl (subLemma (binNatToN a) (binNatToN b) t)
subtraction' (one :: a) (one :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
subtraction' (one :: a) (one :: b) pr | inl x = inl (succPreservesInequality (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 x (le 1 refl)))
subtraction' (one :: a) (one :: b) pr | inr x rewrite x = inr refl

subtraction [] (zero :: b) pr with inspect (binNatToN b)
subtraction [] (zero :: b) pr | zero with≡ pr1 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr)) (transitivity (goPreservesCanonicalRight zero [] b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero [] i)) (binNatToNZero b pr1)) refl))))
subtraction [] (zero :: b) pr | (succ bl) with≡ pr1 rewrite pr | pr1 = succIsPositive _
subtraction [] (one :: b) pr = succIsPositive _
subtraction (zero :: a) (zero :: b) pr = lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 u (le 1 refl)
  where
    u : binNatToN a <N binNatToN b
    u = subtraction a b (mapMaybePreservesNo pr)
subtraction (zero :: a) (one :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
subtraction (zero :: a) (one :: b) pr | inl x = subLemma2 (binNatToN a) (binNatToN b) x
subtraction (zero :: a) (one :: b) pr | inr x rewrite x = le zero refl
subtraction (one :: a) (zero :: b) pr rewrite Semiring.sumZeroRight ℕSemiring (binNatToN a) | Semiring.sumZeroRight ℕSemiring (binNatToN b) = subLemma (binNatToN a) (binNatToN b) u
  where
    u : binNatToN a <N binNatToN b
    u = subtraction a b (mapMaybePreservesNo pr)
subtraction (one :: a) (one :: b) pr = succPreservesInequality (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 u (le 1 refl))
  where
    u : binNatToN a <N binNatToN b
    u = subtraction a b (mapMaybePreservesNo pr)

subLemma4 : (a b : BinNat) {t : BinNat} → go one a b ≡ no → go zero a b ≡ yes t → canonical t ≡ []
subLemma4 [] [] {t} pr1 pr2 rewrite yesInjective (equalityCommutative pr2) = refl
subLemma4 [] (x :: b) {t} pr1 pr2 = goZeroEmpty' (x :: b) pr2
subLemma4 (zero :: a) [] {t} pr1 pr2 with inspect (go one a [])
subLemma4 (zero :: a) [] {t} pr1 pr2 | no with≡ pr3 with subLemma4 a [] pr3 (goEmpty a)
... | bl with applyEquality canonical (yesInjective pr2)
... | th rewrite bl = equalityCommutative th
subLemma4 (zero :: a) [] {t} pr1 pr2 | yes x with≡ pr3 rewrite pr3 = exFalso (noNotYes (equalityCommutative pr1))
subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 with inspect (go one a b)
subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | no with≡ pr3 with inspect (go zero a b)
subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | no with≡ pr3 | no with≡ pr4 rewrite pr4 = exFalso (noNotYes pr2)
subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | no with≡ pr3 | yes x with≡ pr4 with subLemma4 a b pr3 pr4
... | bl rewrite pr3 | pr4 = ans
  where
    ans : canonical t ≡ []
    ans rewrite equalityCommutative (applyEquality canonical (yesInjective pr2)) | bl = refl
subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | yes x with≡ pr3 rewrite pr3 = exFalso (noNotYes (equalityCommutative pr1))
subLemma4 (zero :: a) (one :: b) {t} pr1 pr2 with go one a b
... | no = exFalso (noNotYes pr2)
subLemma4 (zero :: a) (one :: b) {t} pr1 pr2 | yes x = exFalso (noNotYes (equalityCommutative pr1))
subLemma4 (one :: a) (zero :: b) {t} pr1 pr2 with go zero a b
subLemma4 (one :: a) (zero :: b) {t} pr1 pr2 | no = exFalso (noNotYes pr2)
subLemma4 (one :: a) (zero :: b) {t} pr1 pr2 | yes x = exFalso (noNotYes (equalityCommutative pr1))
subLemma4 (one :: a) (one :: b) {t} pr1 pr2 with inspect (go zero a b)
subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | no with≡ pr3 rewrite pr3 = exFalso (noNotYes pr2)
subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | yes x with≡ pr3 with inspect (go one a b)
subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | yes x with≡ pr3 | no with≡ pr4 with subLemma4 a b pr4 pr3
... | bl rewrite pr3 | pr4 | bl = ans
  where
    ans : canonical t ≡ []
    ans rewrite equalityCommutative (applyEquality canonical (yesInjective pr2)) | bl = refl
subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | yes x with≡ pr3 | yes x₁ with≡ pr4 rewrite pr4 = exFalso (noNotYes (equalityCommutative pr1))

goOneFromZero : (a b : BinNat) → go zero a b ≡ no → go one a b ≡ no
goOneFromZero [] (zero :: b) pr = refl
goOneFromZero [] (one :: b) pr = refl
goOneFromZero (zero :: a) (zero :: b) pr rewrite goOneFromZero a b (mapMaybePreservesNo pr) = refl
goOneFromZero (zero :: a) (one :: b) pr rewrite (mapMaybePreservesNo pr) = refl
goOneFromZero (one :: a) (zero :: b) pr rewrite (mapMaybePreservesNo pr) = refl
goOneFromZero (one :: a) (one :: b) pr rewrite goOneFromZero a b (mapMaybePreservesNo pr) = refl

subLemma5 : (a b : BinNat) → mapMaybe canonical (go zero a b) ≡ yes [] → go one a b ≡ no
subLemma5 [] b pr = goOneEmpty' b
subLemma5 (zero :: a) [] pr with inspect (canonical a)
subLemma5 (zero :: a) [] pr | (z :: zs) with≡ pr2 rewrite pr2 = exFalso (nonEmptyNotEmpty (yesInjective pr))
subLemma5 (zero :: a) [] pr | [] with≡ pr2 rewrite pr2 = applyEquality (mapMaybe (one ::_)) (subLemma5 a [] (transitivity (applyEquality (mapMaybe canonical) (goEmpty a)) (applyEquality yes pr2)))
subLemma5 (zero :: a) (zero :: b) pr with inspect (go zero a b)
subLemma5 (zero :: a) (zero :: b) pr | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr)
subLemma5 (zero :: a) (zero :: b) pr | yes x with≡ pr2 with inspect (canonical x)
subLemma5 (zero :: a) (zero :: b) pr | yes x with≡ pr2 | [] with≡ pr3 rewrite pr | pr2 | pr3 = applyEquality (mapMaybe (one ::_)) (subLemma5 a b (transitivity (applyEquality (mapMaybe canonical) pr2) (applyEquality yes pr3)))
subLemma5 (zero :: a) (zero :: b) pr | yes x with≡ pr2 | (x₁ :: bl) with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (nonEmptyNotEmpty (yesInjective pr))
subLemma5 (zero :: a) (one :: b) pr with (go one a b)
subLemma5 (zero :: a) (one :: b) pr | no = exFalso (noNotYes pr)
subLemma5 (zero :: a) (one :: b) pr | yes y = exFalso (nonEmptyNotEmpty (yesInjective pr))
subLemma5 (one :: a) (zero :: b) pr with go zero a b
subLemma5 (one :: a) (zero :: b) pr | no = exFalso (noNotYes pr)
subLemma5 (one :: a) (zero :: b) pr | yes x = exFalso (nonEmptyNotEmpty (yesInjective pr))
subLemma5 (one :: a) (one :: b) pr with inspect (go zero a b)
subLemma5 (one :: a) (one :: b) pr | yes x with≡ pr2 with inspect (canonical x)
subLemma5 (one :: a) (one :: b) pr | yes x with≡ pr2 | [] with≡ pr3 rewrite pr | pr2 | pr3 = applyEquality (mapMaybe (one ::_)) (subLemma5 a b (transitivity (applyEquality (mapMaybe canonical) pr2) (applyEquality yes pr3)))
subLemma5 (one :: a) (one :: b) pr | yes x with≡ pr2 | (x₁ :: y) with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (nonEmptyNotEmpty (yesInjective pr))
subLemma5 (one :: a) (one :: b) pr | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr)

subLemma3 : (a b : BinNat) → go zero a b ≡ no → (go zero (incr a) b ≡ no) || (mapMaybe canonical (go zero (incr a) b) ≡ yes [])
subLemma3 a b pr with inspect (go zero (incr a) b)
subLemma3 a b pr | no with≡ x = inl x
subLemma3 [] (zero :: b) pr | yes y with≡ pr1 rewrite pr = exFalso (noNotYes pr1)
subLemma3 [] (one :: b) pr | yes y with≡ pr1 with inspect (go zero [] b)
subLemma3 [] (one :: b) pr | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes pr1)
subLemma3 [] (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 with goZeroEmpty' b pr2
... | f rewrite pr1 | pr2 | equalityCommutative (yesInjective pr1) | f = inr refl
subLemma3 (zero :: a) (zero :: b) pr | yes y with≡ pr1 rewrite mapMaybePreservesNo pr = exFalso (noNotYes pr1)
subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 with inspect (go zero a b)
subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes pr1)
subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 with inspect (canonical x)
... | [] with≡ pr3 rewrite pr1 | pr2 | equalityCommutative (yesInjective pr1) | pr3 = inr refl
... | (z :: zs) with≡ pr3 with inspect (go one a b)
subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 | (z :: zs) with≡ pr3 | no with≡ pr4 rewrite pr1 | pr2 | pr3 | pr4 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr3) (subLemma4 a b pr4 pr2)))
subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 | (z :: zs) with≡ pr3 | yes x₁ with≡ pr4 rewrite pr1 | pr2 | pr3 | pr4 = exFalso (noNotYes (equalityCommutative pr))
subLemma3 (one :: a) (zero :: b) pr | yes y with≡ pr1 with subLemma3 a b (mapMaybePreservesNo pr)
subLemma3 (one :: a) (zero :: b) pr | yes y with≡ pr1 | inl x rewrite x = inl refl
subLemma3 (one :: a) (zero :: b) pr | yes y with≡ pr1 | inr x with inspect (go zero (incr a) b)
... | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes x)
... | yes z with≡ pr2 rewrite pr1 | pr2 = inr (applyEquality yes (transitivity (transitivity (applyEquality canonical (yesInjective (equalityCommutative pr1))) r) (yesInjective x)))
  where
    r : canonical (zero :: z) ≡ canonical z
    r rewrite yesInjective x = refl
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 with subLemma3 a b (mapMaybePreservesNo pr)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inl x with inspect (go one (incr a) b)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inl th | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr1)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inl th | yes x with≡ pr2 with goOneFromZero (incr a) b th
... | bad rewrite pr2 = exFalso (noNotYes (equalityCommutative bad))
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr x with inspect (go one (incr a) b)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr x | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr1)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 with inspect (go zero (incr a) b)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | no with≡ pr3 rewrite pr3 = exFalso (noNotYes th)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | yes x with≡ pr3 with inspect (go zero a b)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | yes x with≡ pr3 | no with≡ pr4 rewrite pr1 | th | pr2 | pr3 | pr4 | equalityCommutative (yesInjective pr1) = exFalso false
  where
    false : False
    false with applyEquality (mapMaybe canonical) pr3
    ... | f rewrite th | subLemma5 (incr a) b f = exFalso (noNotYes pr2)
subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | yes x with≡ pr3 | yes w with≡ pr4 rewrite pr4 = exFalso (noNotYes (equalityCommutative pr))

goIncrOne : (a b : BinNat) → mapMaybe canonical (go one a b) ≡ mapMaybe canonical (go zero a (incr b))
goIncrOne [] b rewrite goOneEmpty' b | goZeroIncr b = refl
goIncrOne (zero :: a) [] = refl
goIncrOne (zero :: a) (zero :: b) = refl
goIncrOne (zero :: a) (one :: b) with inspect (go one a b)
goIncrOne (zero :: a) (one :: b) | no with≡ pr1 with inspect (go zero a (incr b))
goIncrOne (zero :: a) (one :: b) | no with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = refl
goIncrOne (zero :: a) (one :: b) | no with≡ pr1 | yes x with≡ pr2 with goIncrOne a b
... | f rewrite pr1 | pr2 = exFalso (noNotYes f)
goIncrOne (zero :: a) (one :: b) | yes x with≡ pr1 with inspect (go zero a (incr b))
goIncrOne (zero :: a) (one :: b) | yes x with≡ pr1 | no with≡ pr2 with goIncrOne a b
... | f rewrite pr1 | pr2 = exFalso (noNotYes (equalityCommutative f))
goIncrOne (zero :: a) (one :: b) | yes x with≡ pr1 | yes y with≡ pr2 with goIncrOne a b
... | f rewrite pr1 | pr2 | yesInjective f = refl
goIncrOne (one :: a) [] rewrite goEmpty a = refl
goIncrOne (one :: a) (zero :: b) = refl
goIncrOne (one :: a) (one :: b) with inspect (go one a b)
goIncrOne (one :: a) (one :: b) | no with≡ pr with inspect (go zero a (incr b))
goIncrOne (one :: a) (one :: b) | no with≡ pr | no with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 = refl
goIncrOne (one :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 = exFalso (noNotYes f)
goIncrOne (one :: a) (one :: b) | yes x with≡ pr with inspect (go zero a (incr b))
goIncrOne (one :: a) (one :: b) | yes x with≡ pr | no with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 = exFalso (noNotYes (equalityCommutative f))
goIncrOne (one :: a) (one :: b) | yes x with≡ pr | yes y with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 | yesInjective f = refl

goIncrIncr : (a b : BinNat) → mapMaybe canonical (go zero (incr a) (incr b)) ≡ mapMaybe canonical (go zero a b)
goIncrIncr [] [] = refl
goIncrIncr [] (zero :: b) with inspect (go zero [] b)
... | no with≡ pr rewrite goIncrIncr [] b | pr = refl
... | yes y with≡ pr rewrite goIncrIncr [] b | pr | goZeroEmpty' b {y} pr = refl
goIncrIncr [] (one :: b) rewrite goZeroIncr b = refl
goIncrIncr (zero :: a) [] rewrite goEmpty a = refl
goIncrIncr (zero :: a) (zero :: b) = refl
goIncrIncr (zero :: a) (one :: b) with inspect (go zero a (incr b))
goIncrIncr (zero :: a) (one :: b) | no with≡ pr with inspect (go one a b)
goIncrIncr (zero :: a) (one :: b) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
goIncrIncr (zero :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 = exFalso (noNotYes (equalityCommutative f))
goIncrIncr (zero :: a) (one :: b) | yes y with≡ pr with inspect (go one a b)
goIncrIncr (zero :: a) (one :: b) | yes y with≡ pr | yes z with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 = applyEquality (λ i → yes (one :: i)) (equalityCommutative (yesInjective f))
goIncrIncr (zero :: a) (one :: b) | yes y with≡ pr | no with≡ pr2 with goIncrOne a b
... | f rewrite pr | pr2 = exFalso (noNotYes f)
goIncrIncr (one :: a) [] with goOne a []
... | f with go one (incr a) []
goIncrIncr (one :: a) [] | f | no rewrite goEmpty a = exFalso (noNotYes f)
goIncrIncr (one :: a) [] | f | yes x rewrite goEmpty a | yesInjective f = refl
goIncrIncr (one :: a) (zero :: b) with goOne a b
... | f with go one (incr a) b
goIncrIncr (one :: a) (zero :: b) | f | no with go zero a b
goIncrIncr (one :: a) (zero :: b) | f | no | no = refl
goIncrIncr (one :: a) (zero :: b) | f | yes x with go zero a b
goIncrIncr (one :: a) (zero :: b) | f | yes x | yes x₁ rewrite yesInjective f = refl
goIncrIncr (one :: a) (one :: b) with goIncrIncr a b
... | f with go zero a b
goIncrIncr (one :: a) (one :: b) | f | no with go zero (incr a) (incr b)
goIncrIncr (one :: a) (one :: b) | f | no | no = refl
goIncrIncr (one :: a) (one :: b) | f | yes x with go zero (incr a) (incr b)
goIncrIncr (one :: a) (one :: b) | f | yes x | yes x₁ rewrite yesInjective f = refl

subtractionConverse : (a b : ℕ) → a <N b → go zero (NToBinNat a) (NToBinNat b) ≡ no
subtractionConverse zero (succ b) a<b with NToBinNat b
subtractionConverse zero (succ b) a<b | [] = refl
subtractionConverse zero (succ b) a<b | zero :: bl = refl
subtractionConverse zero (succ b) a<b | one :: bl = goZeroIncr bl
subtractionConverse (succ a) (succ b) a<b with inspect (NToBinNat a)
subtractionConverse (succ a) (succ b) a<b | [] with≡ pr with inspect (NToBinNat b)
subtractionConverse (succ a) (succ b) a<b | [] with≡ pr | [] with≡ pr2 rewrite NToBinNatZero a pr | NToBinNatZero b pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder a<b)
subtractionConverse (succ a) (succ zero) a<b | [] with≡ pr | (zero :: y) with≡ pr2 rewrite NToBinNatZero a pr | pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder a<b)
subtractionConverse (succ a) (succ (succ b)) a<b | [] with≡ pr | (zero :: y) with≡ pr2 with inspect (go zero [] y)
... | no with≡ pr3 rewrite NToBinNatZero a pr | pr2 | pr3 = refl
... | yes t with≡ pr3 with applyEquality canonical pr2
... | g rewrite (goZeroEmpty y pr3) = exFalso (incrNonzero (NToBinNat b) g)
subtractionConverse (succ a) (succ b) a<b | [] with≡ pr | (one :: y) with≡ pr2 rewrite NToBinNatZero a pr | pr2 = applyEquality (mapMaybe (one ::_)) (goZeroIncr y)
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr with inspect (NToBinNat b)
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | [] with≡ pr2 rewrite NToBinNatZero b pr2 = exFalso (bad a<b)
  where
    bad : {a : ℕ} → succ a <N 1 → False
    bad {zero} (le zero ())
    bad {zero} (le (succ x) ())
    bad {succ a} (le zero ())
    bad {succ a} (le (succ x) ())
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (zero :: z) with≡ pr2 rewrite pr | pr2 = applyEquality (mapMaybe (zero ::_)) (mapMaybePreservesNo u)
  where
    t : go zero (NToBinNat a) (NToBinNat b) ≡ no
    t = subtractionConverse a b (canRemoveSuccFrom<N a<b)
    u : go zero (zero :: y) (zero :: z) ≡ no
    u = transitivity (transitivity {x = _} {go zero (NToBinNat a) (zero :: z)} (applyEquality (λ i → go zero i (zero :: z)) (equalityCommutative pr)) (applyEquality (go zero (NToBinNat a)) (equalityCommutative pr2))) t
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 with subtractionConverse a (succ b) (le (succ (_<N_.x a<b)) (transitivity (applyEquality succ (transitivity (applyEquality succ (Semiring.commutative ℕSemiring (_<N_.x a<b) a)) (Semiring.commutative ℕSemiring (succ a) (_<N_.x a<b)))) (_<N_.proof a<b)))
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 | thing=no with subLemma3 (NToBinNat a) (incr (NToBinNat b)) thing=no
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 | thing=no | inl x = x
subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 | thing=no | inr x rewrite pr | pr2 | mapMaybePreservesNo thing=no = exFalso (noNotYes x)
subtractionConverse (succ a) (succ b) a<b | (one :: y) with≡ pr with goIncrIncr (NToBinNat a) (NToBinNat b)
... | f rewrite subtractionConverse a b (canRemoveSuccFrom<N a<b) = mapMaybePreservesNo f

bad : (b : ℕ) {t : BinNat} → incr (NToBinNat b) ≡ zero :: t → canonical t ≡ [] → False
bad b {c} t pr with applyEquality canonical t
... | bl with canonical c
bad b {c} t pr | bl | [] = exFalso (incrNonzero (NToBinNat b) bl)

lemma6 : (a : BinNat) (b : ℕ) → canonical a ≡ [] → NToBinNat b ≡ one :: a → a ≡ []
lemma6 [] b pr1 pr2 = refl
lemma6 (a :: as) b pr1 pr2 with applyEquality canonical pr2
lemma6 (a :: as) b pr1 pr2 | th rewrite pr1 | equalityCommutative (NToBinNatIsCanonical b) | pr2 = exFalso (bad' th)
  where
    bad' : one :: a :: as ≡ one :: [] → False
    bad' ()

doublingLemma : (y : BinNat) → NToBinNat (2 *N binNatToN y) ≡ canonical (zero :: y)
doublingLemma y with inspect (canonical y)
doublingLemma y | [] with≡ pr rewrite binNatToNZero' y pr | pr = refl
doublingLemma y | (a :: as) with≡ pr with inspect (binNatToN y)
doublingLemma y | (a :: as) with≡ pr | zero with≡ pr2 rewrite binNatToNZero y pr2 = exFalso (nonEmptyNotEmpty (equalityCommutative pr))
doublingLemma y | (a :: as) with≡ pr | succ bl with≡ pr2 rewrite pr | pr2 | doubleIsBitShift' bl | equalityCommutative pr = applyEquality (zero ::_) (equalityCommutative (transitivity (equalityCommutative (binToBin y)) (applyEquality NToBinNat pr2)))

private
  doubling : (a : ℕ) {y : BinNat} → (NToBinNat a ≡ zero :: y) → binNatToN y +N (binNatToN y +N 0) ≡ a
  doubling a {y} pr = NToBinNatInj (binNatToN y +N (binNatToN y +N zero)) a (transitivity (transitivity (equalityCommutative (NToBinNatIsCanonical (binNatToN y +N (binNatToN y +N zero)))) (doublingLemma y)) (applyEquality canonical (equalityCommutative pr)))

subtraction2 : (a b : ℕ) {t : BinNat} → (NToBinNat a) -B (NToBinNat b) ≡ yes t → (binNatToN t) +N b ≡ a
subtraction2 zero zero {t} pr rewrite yesInjective (equalityCommutative pr) = refl
subtraction2 zero (succ b) pr with goZeroEmpty (NToBinNat (succ b)) pr
... | t = exFalso (incrNonzero (NToBinNat b) t)
subtraction2 (succ a) b {t} pr with inspect (NToBinNat a)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 with inspect (NToBinNat b)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | [] with≡ pr3 rewrite pr2 | pr3 | equalityCommutative (yesInjective pr) | NToBinNatZero a pr2 | NToBinNatZero b pr3 = refl
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 with inspect (go zero [] bl)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 | no with≡ pr4 rewrite pr2 | pr3 | pr4 = exFalso (noNotYes pr)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 | yes x with≡ pr4 with goZeroEmpty bl pr4
subtraction2 (succ a) (succ b) {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 | yes x with≡ pr4 | r with goZeroEmpty' bl pr4
... | s rewrite pr2 | pr3 | pr4 | r | equalityCommutative (yesInjective pr) | NToBinNatZero a pr2 = exFalso (bad b pr3 r)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (one :: bl) with≡ pr3 with inspect (go zero [] bl)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (one :: bl) with≡ pr3 | no with≡ pr4 rewrite pr2 | pr3 | pr4 = exFalso (noNotYes pr)
subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (one :: bl) with≡ pr3 | yes x with≡ pr4 with goZeroEmpty bl pr4
... | u with goZeroEmpty' bl pr4
... | v rewrite pr2 | pr3 | pr4 | u | NToBinNatZero a pr2 | lemma6 bl b u pr3 | equalityCommutative (yesInjective pr4) | equalityCommutative (yesInjective pr) = ans pr3
  where
    z : bl ≡ []
    z = lemma6 bl b u pr3
    ans : (NToBinNat b ≡ one :: bl) → b ≡ 1
    ans pr with applyEquality binNatToN pr
    ... | th rewrite z = transitivity (equalityCommutative (nToN b)) th
subtraction2 (succ a) b pr | (x :: y) with≡ pr2 with inspect (NToBinNat b)
subtraction2 (succ a) b pr | (zero :: y) with≡ pr2 | [] with≡ pr3 rewrite NToBinNatZero b pr3 | pr2 | pr3 | equalityCommutative (yesInjective pr) = applyEquality succ (transitivity (Semiring.sumZeroRight ℕSemiring _) (doubling a pr2))
subtraction2 (succ a) b pr | (one :: y) with≡ pr2 | [] with≡ pr3 rewrite NToBinNatZero b pr3 | pr2 | pr3 | equalityCommutative (yesInjective pr) = transitivity (Semiring.sumZeroRight ℕSemiring (binNatToN (incr y) +N (binNatToN (incr y) +N zero))) (equalityCommutative (transitivity (equalityCommutative (nToN (succ a))) (applyEquality binNatToN (transitivity (equalityCommutative (NToBinNatSucc a)) (applyEquality incr pr2)))))
subtraction2 (succ a) (succ b) {t} pr | (y :: ys) with≡ pr2 | (z :: zs) with≡ pr3 = transitivity (transitivity (Semiring.commutative ℕSemiring (binNatToN t) (succ b)) (applyEquality succ (transitivity (Semiring.commutative ℕSemiring b (binNatToN t)) (applyEquality (_+N b) (equalityCommutative (binNatToNIsCanonical t)))))) (applyEquality succ inter)
  where
    inter : binNatToN (canonical t) +N b ≡ a
    inter with inspect (go zero (NToBinNat a) (NToBinNat b))
    inter | no with≡ pr4 with goIncrIncr (NToBinNat a) (NToBinNat b)
    ... | f rewrite pr | pr4 = exFalso (noNotYes (equalityCommutative f))
    inter | yes x with≡ pr4 with goIncrIncr (NToBinNat a) (NToBinNat b)
    ... | f with subtraction2 a b {x} pr4
    ... | g = transitivity (applyEquality (_+N b) (transitivity (applyEquality binNatToN h) (binNatToNIsCanonical x))) g
      where
        h : (canonical t) ≡ (canonical x)
        h rewrite pr | pr4 = yesInjective f

subtraction2' : (a b : ℕ) {t : BinNat} → (NToBinNat a) -B (NToBinNat b) ≡ yes t → b ≤N a
subtraction2' a b {t} pr with subtraction2 a b pr
... | f with binNatToN t
subtraction2' a b {t} pr | f | zero = inr f
subtraction2' a b {t} pr | f | succ g = inl (le g f)

subtraction2'' : (a b : ℕ) → (pr : b ≤N a) → mapMaybe binNatToN ((NToBinNat a) -B (NToBinNat b)) ≡ yes (subtractionNResult.result (-N pr))
subtraction2'' a b pr with -N pr
subtraction2'' a b pr | record { result = result ; pr = subPr } with inspect (go zero (NToBinNat a) (NToBinNat b))
subtraction2'' a b (inl pr) | record { result = result ; pr = subPr } | no with≡ pr2 with subtraction (NToBinNat a) (NToBinNat b) pr2
... | bl rewrite nToN a | nToN b = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder pr bl))
subtraction2'' a b (inr pr) | record { result = result ; pr = subPr } | no with≡ pr2 with subtraction (NToBinNat a) (NToBinNat b) pr2
... | bl rewrite nToN a | nToN b | pr = exFalso (TotalOrder.irreflexive ℕTotalOrder bl)
subtraction2'' a b pr | record { result = result ; pr = subPr } | yes x with≡ pr2 with subtraction2 a b pr2
... | f rewrite pr2 | Semiring.commutative ℕSemiring (binNatToN x) b = applyEquality yes (canSubtractFromEqualityLeft {b} {binNatToN x} (transitivity f (equalityCommutative subPr)))


text:
import      Lvl
open import Structure.Category

module Structure.Category.Functor.Equiv
  {ℓₗₒ ℓᵣₒ ℓₗₘ ℓᵣₘ ℓₗₑ ℓᵣₑ : Lvl.Level}
  {catₗ : CategoryObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ}}
  {catᵣ : CategoryObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ}}
  where

open import Functional.Dependent as Fn using (_$_)
import      Function.Equals
open        Function.Equals.Dependent
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Equals using ([≡]-intro) renaming (_≡_ to _≡ₑ_)
open import Relator.Equals.Proofs
open import Relator.Equals.Proofs.Equiv
open import Structure.Category.Functor
open import Structure.Category.Functor.Functors as Functors
open import Structure.Category.Morphism.IdTransport
import      Structure.Categorical.Names as Names
open import Structure.Category.NaturalTransformation
open import Structure.Category.Proofs
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

open Structure.Category

open Category ⦃ … ⦄
open CategoryObject
open Functor ⦃ … ⦄
private instance _ = category catₗ
private instance _ = category catᵣ
private open module MorphismEquivₗ {x}{y} = Equiv(morphism-equiv(catₗ){x}{y}) using () renaming (_≡_ to _≡ₗₘ_)
private open module MorphismEquivᵣ {x}{y} = Equiv(morphism-equiv(catᵣ){x}{y}) using () renaming (_≡_ to _≡ᵣₘ_)

module _
  (f₁@([∃]-intro F₁) f₂@([∃]-intro F₂) : (catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ))
  where

  record _≡ᶠᵘⁿᶜᵗᵒʳ_ : Type{Lvl.of(Type.of(catₗ)) Lvl.⊔ Lvl.of(Type.of(catᵣ))} where
    constructor intro
    field
      functor-proof : (F₁ ⊜ F₂)
      map-proof : NaturalTransformation(f₁)(f₂) (\x → transport(catᵣ) (_⊜_.proof functor-proof {x}))

instance
  [≡ᶠᵘⁿᶜᵗᵒʳ]-reflexivity : Reflexivity(_≡ᶠᵘⁿᶜᵗᵒʳ_)
  _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (Reflexivity.proof [≡ᶠᵘⁿᶜᵗᵒʳ]-reflexivity) = intro [≡]-intro
  NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (Reflexivity.proof [≡ᶠᵘⁿᶜᵗᵒʳ]-reflexivity {functor})) {f = f} =
    trans-refl ∘ map(f) 🝖[ _≡ᵣₘ_ ]-[]
    id ∘ map(f)         🝖[ _≡ᵣₘ_ ]-[ Morphism.identityₗ(_∘_)(id) ]
    map(f)              🝖[ _≡ᵣₘ_ ]-[ Morphism.identityᵣ(_∘_)(id) ]-sym
    map(f) ∘ id         🝖[ _≡ᵣₘ_ ]-[]
    map(f) ∘ trans-refl 🝖-end
    where
      trans-refl = \{x} → transport(catᵣ) ([≡]-intro {x = x})

instance
  [≡ᶠᵘⁿᶜᵗᵒʳ]-symmetry : Symmetry(_≡ᶠᵘⁿᶜᵗᵒʳ_)
  _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (Symmetry.proof [≡ᶠᵘⁿᶜᵗᵒʳ]-symmetry xy) = symmetry(_⊜_) (_≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof xy)
  NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (Symmetry.proof [≡ᶠᵘⁿᶜᵗᵒʳ]-symmetry {[∃]-intro F₁} {[∃]-intro F₂} (intro (intro fe) (intro me)))) {x}{y} {f = f} =
    trans-sym(y) ∘ map(f)                               🝖[ _≡ᵣₘ_ ]-[ Morphism.identityᵣ(_∘_)(id) ]-sym
    (trans-sym(y) ∘ map(f)) ∘ id                        🝖[ _≡ᵣₘ_ ]-[ congruence₂ᵣ(_∘_)(_) ([∘]-on-transport-inverseᵣ catᵣ {ab = fe}) ]-sym
    (trans-sym(y) ∘ map(f)) ∘ (trans(x) ∘ trans-sym(x)) 🝖[ _≡ᵣₘ_ ]-[ associate4-213-121 (category catᵣ) ]-sym
    (trans-sym(y) ∘ (map(f) ∘ trans(x))) ∘ trans-sym(x) 🝖[ _≡ᵣₘ_ ]-[ congruence₂ₗ(_∘_)(_) (congruence₂ᵣ(_∘_)(_) me) ]-sym
    (trans-sym(y) ∘ (trans(y) ∘ map(f))) ∘ trans-sym(x) 🝖[ _≡ᵣₘ_ ]-[ associate4-213-121 (category catᵣ) ]
    (trans-sym(y) ∘ trans(y)) ∘ (map(f) ∘ trans-sym(x)) 🝖[ _≡ᵣₘ_ ]-[ congruence₂ₗ(_∘_)(_) ([∘]-on-transport-inverseₗ catᵣ {ab = fe}) ]
    id ∘ (map(f) ∘ trans-sym(x))                        🝖[ _≡ᵣₘ_ ]-[ Morphism.identityₗ(_∘_)(id) ]
    map(f) ∘ trans-sym(x)                               🝖-end
    where
      trans     = \(x : Object(catₗ)) → transport catᵣ (fe{x})
      trans-sym = \(x : Object(catₗ)) → transport catᵣ (symmetry(_≡ₑ_) (fe{x}))

instance
  [≡ᶠᵘⁿᶜᵗᵒʳ]-transitivity : Transitivity(_≡ᶠᵘⁿᶜᵗᵒʳ_)
  _≡ᶠᵘⁿᶜᵗᵒʳ_.functor-proof (Transitivity.proof [≡ᶠᵘⁿᶜᵗᵒʳ]-transitivity (intro fe₁ _) (intro fe₂ _)) = transitivity(_⊜_) fe₁ fe₂
  NaturalTransformation.natural (_≡ᶠᵘⁿᶜᵗᵒʳ_.map-proof (Transitivity.proof [≡ᶠᵘⁿᶜᵗᵒʳ]-transitivity {[∃]-intro F₁} {[∃]-intro F₂} {[∃]-intro F₃} (intro (intro fe₁) (intro me₁)) (intro (intro fe₂) (intro me₂)))) {x}{y} {f = f} =
    transport catᵣ (transitivity(_≡ₑ_) (fe₁{y}) (fe₂{y})) ∘ map(f) 🝖[ _≡ᵣₘ_ ]-[ congruence₂ₗ(_∘_)(_) (transport-of-transitivity catᵣ {ab = fe₁}{bc = fe₂}) ]
    (transport catᵣ (fe₂{y}) ∘ transport catᵣ (fe₁{y})) ∘ map(f)         🝖[ _≡ᵣₘ_ ]-[ Morphism.associativity(_∘_) ]
    transport catᵣ (fe₂{y}) ∘ (transport catᵣ (fe₁{y}) ∘ map(f))         🝖[ _≡ᵣₘ_ ]-[ congruence₂ᵣ(_∘_)(_) me₁ ]
    transport catᵣ (fe₂{y}) ∘ (map(f) ∘ transport catᵣ (fe₁{x}))         🝖[ _≡ᵣₘ_ ]-[ Morphism.associativity(_∘_) ]-sym
    (transport catᵣ (fe₂{y}) ∘ map(f)) ∘ transport catᵣ (fe₁{x})         🝖[ _≡ᵣₘ_ ]-[ congruence₂ₗ(_∘_)(_) me₂ ]
    (map(f) ∘ transport catᵣ (fe₂{x})) ∘ transport catᵣ (fe₁{x})         🝖[ _≡ᵣₘ_ ]-[ Morphism.associativity(_∘_) ]
    map(f) ∘ (transport catᵣ (fe₂{x}) ∘ transport catᵣ (fe₁{x}))         🝖[ _≡ᵣₘ_ ]-[ congruence₂ᵣ(_∘_)(_) (transport-of-transitivity catᵣ {ab = fe₁}{bc = fe₂}) ]-sym
    map(f) ∘ transport catᵣ (transitivity(_≡ₑ_) (fe₁{x}) (fe₂{x})) 🝖-end

instance
  [≡ᶠᵘⁿᶜᵗᵒʳ]-equivalence : Equivalence(_≡ᶠᵘⁿᶜᵗᵒʳ_)
  [≡ᶠᵘⁿᶜᵗᵒʳ]-equivalence = intro

instance
  [≡ᶠᵘⁿᶜᵗᵒʳ]-equiv : Equiv(catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ)
  [≡ᶠᵘⁿᶜᵗᵒʳ]-equiv = intro(_≡ᶠᵘⁿᶜᵗᵒʳ_) ⦃ [≡ᶠᵘⁿᶜᵗᵒʳ]-equivalence ⦄

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:
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit

data ⊥ : Set where

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

Fin : Nat → Set
Fin zero    = ⊥
Fin (suc n) = ⊤ ⊎ Fin n

n = 49

postulate
  P : Nat → Set
  Q : Set → Set
  f : (n : Nat) → Q (Fin n) → P n
  q : Q (Fin n)

p : P n
p = f _ q


text:
-- Andreas, 2018-10-17
--
-- Cannot branch on erased argument.

open import Agda.Builtin.Bool

T : @0 Bool → Set
T true  = Bool
T false = Bool → Bool

-- Should fail with error like:
--
-- Cannot branch on erased argument of datatype Bool
-- when checking the definition of T


text:
module MLib where

import MLib.Prelude

import MLib.Fin.Parts

import MLib.Fin.Parts.Simple

import MLib.Finite
import MLib.Finite.Properties

import MLib.Algebra.PropertyCode
import MLib.Matrix


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

module sets.nat where

open import sets.nat.core public
open import sets.nat.properties public
open import sets.nat.ordering public
open import sets.nat.solver public
open import sets.nat.struct public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module _<?_ where

open import Data.Nat using (ℕ; zero; suc)
open import Relation.Nullary using (¬_)
open import decidable using (Dec; yes; no)

-- 厳密な不等式 (strict inequality)
infix 4 _<_
data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

-- 0未満の自然数は存在しない
¬m<z : ∀ {m : ℕ} → ¬ (m < zero)
¬m<z ()

-- m < n が成り立たなければ (m + 1) < (n + 1) も成り立たない
¬s<s : ∀ {m n : ℕ} → ¬ (m < n) → ¬ (suc m < suc n)
¬s<s ¬m<n (s<s m<n) = ¬m<n m<n

-- decidableを使った厳密な不等式
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
m     <? zero                = no ¬m<z
zero  <? suc n               = yes z<s
suc m <? suc n with m <? n
...               | yes m<n  = yes (s<s m<n)
...               | no  ¬m<n = no (¬s<s ¬m<n)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
-- Andrea & Andreas, 2014-11-12
-- Pruning projected vars during solving

open import Common.Product
open import Common.Equality

postulate
  A : Set

works1 : {q1 : Set} {q2 : Set → Set} ->
       let M : Set -> Set; M = _ in {z : Set} -> q1 ≡ M (q2 z)
works1 = refl

works2 : {q1 : Set} {q2 : Set → Set} ->
       let M : Set -> Set; M = _ in q1 ≡ M (q2 A)
works2 = refl

works3 : {q : Set × Set} ->
       let M : Set -> Set; M = _ in proj₁ q ≡ M (proj₂ q)
works3 = refl

test1 : {q : Set × (Set → Set)} ->
       let M : Set -> Set; M = _ in {z : Set} -> proj₁ q ≡ M (proj₂ q z)
test1 = refl

test2 : {q : Set × (Set → Set)} ->
       let M : Set -> Set; M = _ in proj₁ q ≡ M (proj₂ q A)
test2 = refl

-- these tests should succeed, as expanding q into a pair gets us back to
-- works1 and works2


text:
module Syntax where

open import Data.Fin
open import Data.List hiding (reverse)
open import Data.List.All
open import Data.Nat
open import Data.Product

open import Typing hiding (send ; recv)

-- expressions
data Expr Φ : Type → Set where
  var : ∀ {t}
      → (x : t ∈ Φ)
      → Expr Φ t

  nat : (unr-Φ : All Unr Φ)
      → (i : ℕ)
      → Expr Φ TInt

  unit : (unr-Φ : All Unr Φ)
      → Expr Φ TUnit

  letbind : ∀ {Φ₁ Φ₂ t₁ t₂}
    → (sp : Split Φ Φ₁ Φ₂)
    → (e₁ : Expr Φ₁ t₁)
    → (e₂ : Expr (t₁ ∷ Φ₂) t₂)
    → Expr Φ t₂

  pair : ∀ {Φ₁ Φ₂ t₁ t₂}
    → (sp : Split Φ Φ₁ Φ₂)
    → (x₁ : t₁ ∈ Φ₁)
    → (x₂ : t₂ ∈ Φ₂)
    → Expr Φ (TPair t₁ t₂)

  letpair : ∀ {Φ₁ Φ₂ t₁ t₂ t}
    → (sp : Split Φ Φ₁ Φ₂)
    → (p : TPair t₁ t₂ ∈ Φ₁)
    → (e : Expr (t₁ ∷ t₂ ∷ Φ₂) t)
    → Expr Φ t

  fork : (e : Expr Φ TUnit)
    → Expr Φ TUnit

  new : (unr-Φ : All Unr Φ)
      → (s : SType)
      → Expr Φ (TPair (TChan (SType.force s)) (TChan (SType.force (dual s))))

  send : ∀ {Φ₁ Φ₂ s t}
      → (sp : Split Φ Φ₁ Φ₂)
      → (ch : (TChan (transmit SND t s)) ∈ Φ₁)
      → (vv : t ∈ Φ₂)
      → Expr Φ (TChan (SType.force s))

  recv : ∀ {s t}
      → (ch : (TChan (transmit RCV t s)) ∈ Φ)
      → Expr Φ (TPair (TChan (SType.force s)) t)

  close : (ch : TChan send! ∈ Φ)
      → Expr Φ TUnit

  wait : (ch : TChan send? ∈ Φ)
      → Expr Φ TUnit

  select : ∀ {s₁ s₂}
      → (lab : Selector)
      → (ch : TChan (sintern s₁ s₂) ∈ Φ)
      → Expr Φ (TChan (selection lab (SType.force s₁) (SType.force s₂)))

  branch : ∀ {s₁ s₂ Φ₁ Φ₂ t}
      → (sp : Split Φ Φ₁ Φ₂)
      → (ch : TChan (sextern s₁ s₂) ∈ Φ₁)
      → (eleft : Expr (TChan (SType.force s₁) ∷ Φ₂) t)
      → (erght : Expr (TChan (SType.force s₂) ∷ Φ₂) t)
      → Expr Φ t

  nselect : ∀ {m alt}
      → (lab : Fin m)
      → (ch : TChan (sintN m alt) ∈ Φ)
      → Expr Φ (TChan (SType.force (alt lab)))

  nbranch : ∀ {m alt Φ₁ Φ₂ t}
      → (sp : Split Φ Φ₁ Φ₂)
      → (ch : TChan (sextN m alt) ∈ Φ₁)
      → (ealts : (i : Fin m) → Expr (TChan (SType.force (alt i)) ∷ Φ₂) t)
      → Expr Φ t

  ulambda : ∀ {Φ₁ Φ₂ t₁ t₂}
      → (sp : Split Φ Φ₁ Φ₂)
      → (unr-Φ₁ : All Unr Φ₁)
      → (unr-Φ₂ : All Unr Φ₂)
      → (ebody : Expr (t₁ ∷ Φ₁) t₂)
      → Expr Φ (TFun UU t₁ t₂)

  llambda : ∀ {Φ₁ Φ₂ t₁ t₂}
      → (sp : Split Φ Φ₁ Φ₂)
      → (unr-Φ₂ : All Unr Φ₂)
      → (ebody : Expr (t₁ ∷ Φ₁) t₂)
      → Expr Φ (TFun LL t₁ t₂)

  app : ∀ {Φ₁ Φ₂ lu t₁ t₂}
      → (sp : Split Φ Φ₁ Φ₂)
      → (xfun : TFun lu t₁ t₂ ∈ Φ₁)
      → (xarg : t₁ ∈ Φ₂)
      → Expr Φ t₂

  rec : ∀ {t₁ t₂}
      → (unr-Φ : All Unr Φ)
      → let t = TFun UU t₁ t₂ in
        (ebody : Expr (t ∷ t₁ ∷ Φ) t₂)
      → Expr Φ t

  subsume : ∀ {t₁ t₂}
      → (e : Expr Φ t₁)
      → (t≤t' : SubT t₁ t₂)
      → Expr Φ t₂

unr-weaken : ∀ {Φ Φ₁ Φ₂ t} → Split Φ Φ₁ Φ₂ → All Unr Φ₂ → Expr Φ₁ t → Expr Φ t
unr-weaken sp un-Φ₂ (var x) = var (unr-weaken-var sp un-Φ₂ x)
unr-weaken sp un-Φ₂ (nat unr-Φ i) = letbind sp (nat unr-Φ i) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (unit unr-Φ) = letbind sp (unit unr-Φ) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (letbind sp₁ e e₁) = letbind sp (letbind sp₁ e e₁) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (pair sp₁ x₁ x₂) = letbind sp (pair sp₁ x₁ x₂) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (letpair sp₁ p e) = letbind sp (letpair sp₁ p e) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (fork e) = unr-weaken sp un-Φ₂ e
unr-weaken sp un-Φ₂ (new unr-Φ s) = letbind sp (new unr-Φ s) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (send sp₁ ch vv) = letbind sp (send sp₁ ch vv) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (recv ch) = letbind sp (recv ch) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (close ch) = letbind sp (close ch) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (wait ch) = letbind sp (wait ch) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (nselect lab ch) = letbind sp (nselect lab ch) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (nbranch sp₁ ch ealts) = letbind sp (nbranch sp₁ ch ealts) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (select lab ch) = letbind sp (select lab ch) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (branch sp₁ ch e e₁) with split-rotate sp sp₁
... | Φ' , sp-ΦΦ₃Φ' , sp-Φ'Φ₄Φ₂ = branch sp-ΦΦ₃Φ' ch (unr-weaken (left sp-Φ'Φ₄Φ₂) un-Φ₂ e) (unr-weaken (left sp-Φ'Φ₄Φ₂) un-Φ₂ e₁)
unr-weaken sp un-Φ₂ (ulambda sp₁ unr-Φ₁ unr-Φ₂ e) = ulambda sp (split-unr sp₁ unr-Φ₁ unr-Φ₂) un-Φ₂ (unr-weaken (left sp₁) unr-Φ₂ e)
unr-weaken sp un-Φ₂ (llambda sp₁ unr-Φ₂ e) = llambda sp un-Φ₂ (unr-weaken (left sp₁) unr-Φ₂ e)
unr-weaken sp un-Φ₂ (app sp₁ xfun xarg) = letbind sp (app sp₁ xfun xarg) (var (here un-Φ₂))
unr-weaken sp un-Φ₂ (rec unr-Φ e) = rec (split-unr sp unr-Φ un-Φ₂) (unr-weaken (left (left sp)) un-Φ₂ e)
unr-weaken sp un-Φ₂ (subsume e t≤t') = subsume (unr-weaken sp un-Φ₂ e) t≤t'

lift-expr : ∀ {Φ t tᵤ} → Unr tᵤ → Expr Φ t → Expr (tᵤ ∷ Φ) t
lift-expr unrtu (var x) = var (there unrtu x)
lift-expr unrtu (nat unr-Φ i) = nat (unrtu ∷ unr-Φ) i
lift-expr unrtu (unit unr-Φ) = unit (unrtu ∷ unr-Φ)
lift-expr unrtu (letbind sp e e₁) = letbind (left sp) (lift-expr unrtu e) e₁
lift-expr unrtu (pair sp x₁ x₂) = pair (rght sp) x₁ (there unrtu x₂)
lift-expr unrtu (letpair sp p e) = letpair (left sp) (there unrtu p) e
lift-expr unrtu (fork e) = lift-expr unrtu e
lift-expr unrtu (new unr-Φ s) = new (unrtu ∷ unr-Φ) s
lift-expr unrtu (close ch) = close (there unrtu ch)
lift-expr unrtu (wait ch) = wait (there unrtu ch)
lift-expr unrtu (send sp ch vv) = send (rght sp) ch (there unrtu vv)
lift-expr unrtu (recv ch) = recv (there unrtu ch)
lift-expr unrtu (nselect lab ch) = nselect lab (there unrtu ch)
lift-expr unrtu (nbranch sp ch ealts) = nbranch (left sp) (there unrtu ch) ealts
lift-expr unrtu (select lab ch) = select lab (there unrtu ch)
lift-expr unrtu (branch sp ch x₁ x₂) = branch (left sp) (there unrtu ch) x₁ x₂
lift-expr unrtu (ulambda sp unr-Φ unr-Φ₂ ebody) = ulambda (rght sp) unr-Φ (unrtu ∷ unr-Φ₂) ebody
lift-expr unrtu (llambda sp unr-Φ₂ ebody) = llambda (rght sp) (unrtu ∷ unr-Φ₂) ebody
lift-expr unrtu (app sp xfun xarg) = app (rght sp) xfun (there unrtu xarg)
lift-expr{Φ} unrtu (rec unr-Φ ebody) = letbind (left (split-all-right Φ)) (var (here [])) (rec (unrtu ∷ unr-Φ) (unr-weaken (left (left (rght (split-all-left Φ)))) (unrtu ∷ []) ebody))
lift-expr unrtu (subsume e t≤t') = subsume (lift-expr unrtu e) t≤t'

unr-subst : ∀ {Φ Φ₁ Φ₂ tᵤ t} → Unr tᵤ → Split Φ Φ₁ Φ₂ → All Unr Φ₁ → Expr Φ₁ tᵤ → Expr (tᵤ ∷ Φ₂) t → Expr Φ t
unr-subst unrtu sp unr-Φ₁ etu (var (here x)) = unr-weaken sp x etu
unr-subst unrtu sp unr-Φ₁ etu (var (there x x₁)) = var (unr-weaken-var (split-sym sp) unr-Φ₁ x₁)
unr-subst unrtu sp unr-Φ₁ etu (nat (unr-tu ∷ unr-Φ) i) = nat (split-unr sp unr-Φ₁ unr-Φ) i
unr-subst unrtu sp unr-Φ₁ etu (unit (_ ∷ unr-Φ)) = unit (split-unr sp unr-Φ₁ unr-Φ)
unr-subst unrtu sp unr-Φ₁ etu (letbind sp₁ e e₁) = letbind sp etu (letbind sp₁ e e₁)
unr-subst unrtu sp unr-Φ₁ etu (pair sp₁ x₁ x₂) = letbind sp etu (pair sp₁ x₁ x₂)
unr-subst unrtu sp unr-Φ₁ etu (letpair sp₁ p e) = letbind sp etu (letpair sp₁ p e)
unr-subst unrtu sp unr-Φ₁ etu (fork e) = unr-subst unrtu sp unr-Φ₁ etu e
unr-subst unrtu sp unr-Φ₁ etu (new unr-Φ s) = letbind sp etu (new unr-Φ s)
unr-subst unrtu sp unr-Φ₁ etu (send sp₁ ch vv) = letbind sp etu (send sp₁ ch vv)
unr-subst unrtu sp unr-Φ₁ etu (recv ch) = letbind sp etu (recv ch)
unr-subst unrtu sp unr-Φ₁ etu (close ch) = letbind sp etu (close ch)
unr-subst unrtu sp unr-Φ₁ etu (wait ch) = letbind sp etu (wait ch)
unr-subst unrtu sp unr-Φ₁ etu (nselect lab ch) = letbind sp etu (nselect lab ch)
unr-subst unrtu sp unr-Φ₁ etu (nbranch sp₁ ch ealts) = letbind sp etu (nbranch sp₁ ch ealts)
unr-subst unrtu sp unr-Φ₁ etu (select lab ch) = letbind sp etu (select lab ch)
unr-subst unrtu sp unr-Φ₁ etu (branch sp₁ ch e e₁) = letbind sp etu (branch sp₁ ch e e₁)
unr-subst unrtu sp unr-Φ₁ etu (ulambda sp₁ unr-Φ₂ unr-Φ₃ e) = letbind sp etu (ulambda sp₁ unr-Φ₂ unr-Φ₃ e)
unr-subst unrtu sp unr-Φ₁ etu (llambda sp₁ unr-Φ₂ e) = letbind sp etu (llambda sp₁ unr-Φ₂ e)
unr-subst unrtu sp unr-Φ₁ etu (app sp₁ xfun xarg) = letbind sp etu (app sp₁ xfun xarg)
unr-subst unrtu sp unr-Φ₁ etu (rec unr-Φ e) = letbind sp etu (rec unr-Φ e)
unr-subst unrtu sp unr-Φ₁ etu (subsume e t≤t') = subsume (unr-subst unrtu sp unr-Φ₁ etu e) t≤t'

expr-coerce : ∀ {Φ t₁ t₂ t₁' t₂'} → Expr (t₁ ∷ Φ) t₂ → SubT t₂ t₂' → SubT t₁' t₁ → Expr (t₁' ∷ Φ) t₂'
expr-coerce e t2≤t2' t1'≤t1 = letbind (left (split-all-right _)) (subsume (var (here [])) t1'≤t1) (subsume e t2≤t2')

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
{-# OPTIONS --without-K --safe --no-universe-polymorphism --sized-types
            --no-guardedness --no-subtyping #-}

module Agda.Builtin.Size where

{-# BUILTIN SIZEUNIV SizeUniv #-}
{-# BUILTIN SIZE     Size     #-}
{-# BUILTIN SIZELT   Size<_   #-}
{-# BUILTIN SIZESUC  ↑_       #-}
{-# BUILTIN SIZEINF  ∞        #-}
{-# BUILTIN SIZEMAX  _⊔ˢ_     #-}

{-# FOREIGN GHC
  type SizeLT i = ()
  #-}

{-# COMPILE GHC Size   = type ()     #-}
{-# COMPILE GHC Size<_ = type SizeLT #-}
{-# COMPILE GHC ↑_     = \_ -> ()    #-}
{-# COMPILE GHC ∞      = ()          #-}
{-# COMPILE GHC _⊔ˢ_   = \_ _ -> ()  #-}


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

module CPermCat where

open import Level using (zero)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using () renaming (zero to 0F)
open import Data.Product using (_,_; uncurry)
import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; sym; cong₂; isEquivalence)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Monoidal.Braided using (Braided)
open import Categories.Monoidal.Symmetric using (Symmetric)
open import Categories.RigCategory
  using (RigCategory; module BimonoidalHelperFunctors)

--

open import ConcretePermutation using (CPerm)

open import Permutation using (idp; symp; _●p_; _⊎p_; _×p_)
open import PermutationProperties
  using (assocp; lidp; ridp; rinv; linv; 1p⊎1p≡1p; ⊎p●p≡●p⊎p)

------------------------------------------------------------------------------
-- CPerm is is a category
-- Permutations can be compared by strict propositional equality

CPermCat : Category zero zero zero
CPermCat = record
  { Obj = ℕ
  ; _⇒_ = CPerm
  ; _≡_ = P._≡_
  ; id = idp
  ; _∘_ = _●p_
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → assocp {p₁ = h} {g} {f}
  ; identityˡ = lidp
  ; identityʳ = ridp
  ; equiv = P.isEquivalence
  ; ∘-resp-≡ = λ { {_} {_} {_} {f} {.f} {g} {.g} P.refl P.refl → P.refl}
  }

-- ... and a groupoid

CPermGroupoid : Groupoid CPermCat
CPermGroupoid = record
  { _⁻¹ = symp
  ; iso = λ {_} {_} {f} → record { isoˡ = linv f ; isoʳ = rinv f }
  }

-- additive bifunctor and monoidal structure

⊎p-bifunctor : Bifunctor CPermCat CPermCat CPermCat
⊎p-bifunctor = record
  { F₀ = uncurry _+_
  ; F₁ = uncurry _⊎p_
  ; identity = 1p⊎1p≡1p
    -- perhaps the weird order below means the underlying combinators should be fixed?
  ; homomorphism = λ { {_} {_} {_} {p₁ , p₂} {q₁ , q₂} → ⊎p●p≡●p⊎p {f = q₁} {q₂} {p₁} {p₂}}
  ; F-resp-≡ = uncurry (P.cong₂ _⊎p_)
  }

-- the 0 below is the id from CPermMonoidal

module ⊎h = MonoidalHelperFunctors CPermCat ⊎p-bifunctor 0

{- these are all commented out because unite+p and companions are
  no longer defined!
0⊕x≡x : NaturalIsomorphism ⊎h.id⊗x ⊎h.x
0⊕x≡x = record
  { F⇒G = record { η = λ _ → unite+p
                 ; commute = λ f → unite+p∘[0⊎x]≡x∘unite+p (f 0F)
                 }
  ; F⇐G = record { η = λ _ → uniti+p
                  ; commute = λ f → uniti+p∘x≡[0⊎x]∘uniti+p (f 0F)
                  }
  ; iso = λ X → record { isoˡ = linv uniti+p ; isoʳ = linv unite+p }
  }

x⊕0≡x : NaturalIsomorphism ⊎h.x⊗id ⊎h.x
x⊕0≡x = record
  { F⇒G = record { η = λ _ → uniti+rp
                 ; commute = λ f → uniti+rp∘[x⊎0]≡x∘uniti+rp (f 0F)
                 }
  ; F⇐G = record { η = λ _ → unite+rp
                 ; commute = λ f → unite+rp∘[x⊎0]≡x∘unite+rp (f 0F)
                 }
  ; iso = λ X → record { isoˡ = linv unite+rp ; isoʳ = linv uniti+rp }
  }
-}

{--
[x⊕y]⊕z≡x⊕[y⊕z] : NaturalIsomorphism ⊎h.[x⊗y]⊗z ⊎h.x⊗[y⊗z]
[x⊕y]⊕z≡x⊕[y⊕z] = record
  { F⇒G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; F⇐G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

-- and a monoidal category (additive)

M⊕ : Monoidal CPermCat
M⊕ = record
  { ⊗ = ⊎p-bifunctor
  ; id = 0
  ; identityˡ = 0⊕x≡x
  ; identityʳ = x⊕0≡x
  ; assoc = [x⊕y]⊕z≡x⊕[y⊕z]
  ; triangle = {!!}
  ; pentagon = {!!}
  }

-- multiplicative bifunctor and monoidal structure

×p-bifunctor : Bifunctor CPermCat CPermCat CPermCat
×p-bifunctor = record
  { F₀ = λ { (m , n) → m * n}
  ; F₁ = λ { (p₁ , p₂) → p₁ ×p p₂ }
  ; identity = λ { {m , n} → 1p×1p≡1p {m} }
  ; homomorphism = λ { {_} {_} {_} {p₁ , p₂} {q₁ , q₂} →
      ×p-distrib {p₁ = q₁} {q₂} {p₁} {p₂}}
  ; F-resp-≡ = λ {(p₁≡p₃ , p₂≡p₄) → P.cong₂ _×p_ p₁≡p₃ p₂≡p₄ }
  }

module ×h = MonoidalHelperFunctors CPermCat ×p-bifunctor 1

1⊗x≡x : NaturalIsomorphism ×h.id⊗x ×h.x
1⊗x≡x = record
  { F⇒G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; F⇐G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

x⊗1≡x : NaturalIsomorphism ×h.x⊗id ×h.x
x⊗1≡x = record
  { F⇒G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; F⇐G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

[x⊗y]⊗z≡x⊗[y⊗z] : NaturalIsomorphism ×h.[x⊗y]⊗z ×h.x⊗[y⊗z]
[x⊗y]⊗z≡x⊗[y⊗z] = record
  { F⇒G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; F⇐G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

-- and a monoidal category (multiplicative)

M⊗ : Monoidal CPermCat
M⊗ = record
  { ⊗ = ×p-bifunctor
  ; id = 1
  ; identityˡ = 1⊗x≡x
  ; identityʳ = x⊗1≡x
  ; assoc = [x⊗y]⊗z≡x⊗[y⊗z]
  ; triangle = {!!}
  ; pentagon = {!!}
  }

x⊕y≡y⊕x : NaturalIsomorphism ⊎h.x⊗y ⊎h.y⊗x
x⊕y≡y⊕x = record
  { F⇒G = record { η = {!!} ; commute = {!!} }
  ; F⇐G = record { η = {!!} ; commute = {!!} }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} } }

BM⊕ : Braided M⊕
BM⊕ = record
  { braid = x⊕y≡y⊕x
  ; hexagon₁ = {!!}
  ; hexagon₂ = {!!}
  }

x⊗y≡y⊗x : NaturalIsomorphism ×h.x⊗y ×h.y⊗x
x⊗y≡y⊗x = record
  { F⇒G = record { η = {!!} ; commute = {!!} }
  ; F⇐G = record { η = {!!} ; commute = {!!} }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} } }

BM⊗ : Braided M⊗
BM⊗ = record
  { braid = x⊗y≡y⊗x
  ; hexagon₁ = {!!}
  ; hexagon₂ = {!!}
  }

-- with both monoidal structures being symmetric

SBM⊕ : Symmetric BM⊕
SBM⊕ = record { symmetry = {!!} }

SBM⊗ : Symmetric BM⊗
SBM⊗ = record { symmetry = {!!} }

module r = BimonoidalHelperFunctors BM⊕ BM⊗

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; F⇐G = record
    { η = {!!}
    ; commute = {!!}
    }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record { η = {!!} ; commute = {!!} }
  ; F⇐G = record { η = {!!} ; commute = {!!} }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record
  { F⇒G = record { η = {!!} ; commute = {!!} }
  ; F⇐G = record { η = {!!} ; commute = {!!} }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record { η = {!!} ; commute = {!!} }
  ; F⇐G = record { η = {!!} ; commute = {!!} }
  ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
  }

-- and the multiplicative structure distributing over the additive one

Pi1Rig : RigCategory SBM⊕ SBM⊗
Pi1Rig = record
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = 0⊗x≡0
  ; annᵣ = x⊗0≡0
  ; laplazaI = {!!}
  ; laplazaII = {!!}
  ; laplazaIV = {!!}
  ; laplazaVI = {!!}
  ; laplazaIX = {!!}
  ; laplazaX = {!!}
  ; laplazaXI = {!!}
  ; laplazaXIII = {!!}
  ; laplazaXV = {!!}
  ; laplazaXVI =  {!!}
  ; laplazaXVII = {!!}
  ; laplazaXIX = {!!}
  ; laplazaXXIII = {!!}
  }

--}
------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

record Functor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

IdF : Functor (λ A → A)
unquoteDef IdF =
  defineFun IdF (clause (vArg (projP (quote Functor.fmap)) ∷ vArg (var "f") ∷ vArg (var "x") ∷ [])
                        (var 1 (vArg (var 0 []) ∷ [])) ∷ [])

check : ∀ {A B} (f : A → B) (x : A) → Functor.fmap IdF f x ≡ f x
check f x = refl

open Functor {{...}}

instance
  InstF : Functor (λ A → A)
  unquoteDef InstF =
    defineFun InstF (clause (iArg (projP (quote fmap)) ∷ vArg (var "f") ∷ vArg (var "x") ∷ [])
                            (var 1 (vArg (var 0 []) ∷ [])) ∷ [])

check₁ : ∀ {A B} (f : A → B) (x : A) → fmap f x ≡ f x
check₁ f x = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

open import Categories.Category.Core

module Categories.Morphism.Regular.Properties {o ℓ e} (𝒞 : Category o ℓ e) where

open import Categories.Morphism 𝒞
open import Categories.Morphism.Regular 𝒞
open import Categories.Diagram.Equalizer 𝒞
open import Categories.Diagram.Equalizer.Properties 𝒞
open import Categories.Diagram.Coequalizer.Properties 𝒞

open Category 𝒞

private
  variable
    A B : Obj
    f g : A ⇒ B

Section⇒RegularMono : f SectionOf g → RegularMono f
Section⇒RegularMono {f = f} {g = g} g∘f≈id = record
  { g = id
  ; h = f ∘ g
  ; equalizer = section-equalizer g∘f≈id
  }

Retract⇒RegularEpi : f RetractOf g → RegularEpi f
Retract⇒RegularEpi {f = f} {g = g} f∘g≈id = record
  { h = g ∘ f
  ; g = id
  ; coequalizer = retract-coequalizer f∘g≈id
  }

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text: module Categories.Monad.Algebra where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories