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

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

open import Level using (0ℓ)

-- This module incldes various Agda lemmas that are independent of the project's domain

module LibraBFT.Lemmas where

 cong₃ : ∀{a b c d}{A : Set a}{B : Set b}{C : Set c}{D : Set d}
       → (f : A → B → C → D) → ∀{x y u v m n} → x ≡ y → u ≡ v → m ≡ n
       → f x u m ≡ f y v n
 cong₃ f refl refl refl = refl

 ≡-pi : ∀{a}{A : Set a}{x y : A}(p q : x ≡ y) → p ≡ q
 ≡-pi refl refl = refl

 Unit-pi : {u1 u2 : Unit}
         → u1 ≡ u2
 Unit-pi {unit} {unit} = refl

 ++-inj : ∀{a}{A : Set a}{m n o p : List A}
        → length m ≡ length n → m ++ o ≡ n ++ p
        → m ≡ n × o ≡ p
 ++-inj {m = []}     {x ∷ n} () hip
 ++-inj {m = x ∷ m}  {[]}    () hip
 ++-inj {m = []}     {[]}     lhip hip
   = refl , hip
 ++-inj {m = m ∷ ms} {n ∷ ns} lhip hip
   with ++-inj {m = ms} {ns} (suc-injective lhip) (proj₂ (∷-injective hip))
 ...| (mn , op) rewrite proj₁ (∷-injective hip)
    = cong (n ∷_) mn , op

 ++-abs : ∀{a}{A : Set a}{n : List A}(m : List A)
        → 1 ≤ length m → [] ≡ m ++ n → ⊥
 ++-abs [] ()
 ++-abs (x ∷ m) imp ()

 data All-vec {ℓ} {A : Set ℓ} (P : A → Set ℓ) : ∀ {n} → Vec {ℓ} A n → Set (Level.suc ℓ) where
   []  : All-vec P []
   _∷_ : ∀ {x n} {xs : Vec A n} (px : P x) (pxs : All-vec P xs) → All-vec P (x ∷ xs)

 ≤-unstep : ∀{m n} → suc m ≤ n → m ≤ n
 ≤-unstep (s≤s ss) = ≤-step ss

 ≡⇒≤ : ∀{m n} → m ≡ n → m ≤ n
 ≡⇒≤ refl = ≤-refl

 ∈-cong : ∀{a b}{A : Set a}{B : Set b}{x : A}{l : List A}
        → (f : A → B) → x ∈ l → f x ∈ List-map f l
 ∈-cong f (here px) = here (cong f px)
 ∈-cong f (there hyp) = there (∈-cong f hyp)

 All-self : ∀{a}{A : Set a}{xs : List A} → All (_∈ xs) xs
 All-self = All-tabulate (λ x → x)

 All-reduce⁺
   : ∀{a b}{A : Set a}{B : Set b}{Q : A → Set}{P : B → Set}
   → { xs : List A }
   → (f : ∀{x} → Q x → B)
   → (∀{x} → (prf : Q x) → P (f prf))
   → (all : All Q xs)
   → All P (All-reduce f all)
 All-reduce⁺ f hyp []         = []
 All-reduce⁺ f hyp (ax ∷ axs) = (hyp ax) ∷ All-reduce⁺ f hyp axs

 All-reduce⁻
   : ∀{a b}{A : Set a}{B : Set b}
     {Q : A → Set}
   → { xs : List A }
   → ∀ {vdq}
   → (f : ∀{x} → Q x → B)
   → (all : All Q xs)
   → vdq ∈ All-reduce f all
   → ∃[ v ] ∃[ v∈xs ] (vdq ≡ f {v} v∈xs)
 All-reduce⁻ {Q = Q} {(h ∷ _)} {vdq} f (px ∷ pxs) (here refl)  = h , px , refl
 All-reduce⁻ {Q = Q} {(_ ∷ t)} {vdq} f (px ∷ pxs) (there vdq∈) = All-reduce⁻ {xs = t} f pxs vdq∈

 List-index : ∀ {A : Set} → (_≟A_ : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)) → A → (l : List A) → Maybe (Fin (length l))
 List-index _≟A_ x l with break (_≟A x) l
 ...| not≡ , _ with length not≡ <? length l
 ...| no  _     = nothing
 ...| yes found = just ( fromℕ< {length not≡} {length l} found)

 nats : ℕ → List ℕ
 nats 0 = []
 nats (suc n) = (nats n) ++ (n ∷ [])

 _ : nats 4 ≡ 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
 _ = refl

 _ : Maybe-map toℕ (List-index _≟_ 2 (nats 4)) ≡ just 2
 _ = refl

 _ : Maybe-map toℕ (List-index _≟_ 4 (nats 4)) ≡ nothing
 _ = refl

 allDistinct : ∀ {A : Set} → List A → Set
 allDistinct l = ∀ (i j : Σ ℕ (_< length l)) →
                   proj₁ i ≡ proj₁ j
                   ⊎ List-lookup l (fromℕ< (proj₂ i)) ≢ List-lookup l (fromℕ< (proj₂ j))

 postulate -- TODO-1: currently unused; prove it, if needed
   allDistinct? : ∀ {A : Set} → {≟A : (a₁ a₂ : A) → Dec (a₁ ≡ a₂)} → (l : List A) → Dec (allDistinct l)

  -- Extends an arbitrary relation to work on the head of
  -- the supplied list, if any.
 data OnHead {A : Set}(P : A → A → Set) (x : A) : List A → Set where
    []   : OnHead P x []
    on-∷ : ∀{y ys} → P x y → OnHead P x (y ∷ ys)

  -- Establishes that a list is sorted according to the supplied
  -- relation.
 data IsSorted {A : Set}(_<_ : A → A → Set) : List A → Set where
    []  : IsSorted _<_ []
    _∷_ : ∀{x xs} → OnHead _<_ x xs → IsSorted _<_ xs → IsSorted _<_ (x ∷ xs)

 OnHead-prop : ∀{A}(P : A → A → Set)(x : A)(l : List A)
             → Irrelevant P
             → isPropositional (OnHead P x l)
 OnHead-prop P x [] hyp [] [] = refl
 OnHead-prop P x (x₁ ∷ l) hyp (on-∷ x₂) (on-∷ x₃) = cong on-∷ (hyp x₂ x₃)

 IsSorted-prop : ∀{A}(_<_ : A → A → Set)(l : List A)
               → Irrelevant _<_
               → isPropositional (IsSorted _<_ l)
 IsSorted-prop _<_ [] hyp [] []                  = refl
 IsSorted-prop _<_ (x ∷ l) hyp (x₁ ∷ a) (x₂ ∷ b)
   = cong₂ _∷_ (OnHead-prop _<_ x l hyp x₁ x₂)
               (IsSorted-prop _<_ l hyp a b)

 IsSorted-map⁻ : {A : Set}{_≤_ : A → A → Set}
               → {B : Set}(f : B → A)(l : List B)
               → IsSorted (λ x y → f x ≤ f y) l
               → IsSorted _≤_ (List-map f l)
 IsSorted-map⁻ f .[] [] = []
 IsSorted-map⁻ f .(_ ∷ []) (x ∷ []) = [] ∷ []
 IsSorted-map⁻ f .(_ ∷ _ ∷ _) (on-∷ x ∷ (x₁ ∷ is)) = (on-∷ x) ∷ IsSorted-map⁻ f _ (x₁ ∷ is)

 -- TODO-1 : Better name and/or replace with library property
 Any-sym : ∀ {a b}{A : Set a}{B : Set b}{tgt : B}{l : List A}{f : A → B}
         → Any (λ x → tgt ≡ f x) l
         → Any (λ x → f x ≡ tgt) l
 Any-sym (here x)  = here (sym x)
 Any-sym (there x) = there (Any-sym x)

 Any-lookup-correct :  ∀ {a b}{A : Set a}{B : Set b}{tgt : B}{l : List A}{f : A → B}
                    → (p : Any (λ x → f x ≡ tgt) l)
                    → Any-lookup p ∈ l
 Any-lookup-correct (here px) = here refl
 Any-lookup-correct (there p) = there (Any-lookup-correct p)

 Any-lookup-correctP :  ∀ {a}{A : Set a}{l : List A}{P : A → Set}
                     → (p : Any P l)
                     → Any-lookup p ∈ l
 Any-lookup-correctP (here px) = here refl
 Any-lookup-correctP (there p) = there (Any-lookup-correctP p)

 Any-witness : ∀ {a b} {A : Set a} {l : List A} {P : A → Set b}
             → (p : Any P l) → P (Any-lookup p)
 Any-witness (here px) = px
 Any-witness (there x) = Any-witness x

 -- TODO-1: there is probably a library property for this.
 ∈⇒Any : ∀ {A : Set}{x : A}
       → {xs : List A}
       → x ∈ xs
       → Any (_≡ x) xs
 ∈⇒Any {x = x} (here refl) = here refl
 ∈⇒Any {x = x} {h ∷ t} (there xxxx) = there (∈⇒Any {xs = t} xxxx)

 false≢true : false ≢ true
 false≢true ()

 witness : {A : Set}{P : A → Set}{x : A}{xs : List A}
         → x ∈ xs → All P xs → P x
 witness x y = All-lookup y x

 maybe-⊥ : ∀{a}{A : Set a}{x : A}{y : Maybe A}
         → y ≡ just x
         → y ≡ nothing
         → ⊥
 maybe-⊥ () refl

 Maybe-map-cool : ∀ {S S₁ : Set} {f : S → S₁} {x : Maybe S} {z}
                → Maybe-map f x ≡ just z
                → x ≢ nothing
 Maybe-map-cool {x = nothing} ()
 Maybe-map-cool {x = just y} prf = λ x → ⊥-elim (maybe-⊥ (sym x) refl)

 Maybe-map-cool-1 : ∀ {S S₁ : Set} {f : S → S₁} {x : Maybe S} {z}
                  → Maybe-map f x ≡ just z
                  → Σ S (λ x' → f x' ≡ z)
 Maybe-map-cool-1 {x = nothing} ()
 Maybe-map-cool-1 {x = just y} {z = z} refl = y , refl

 Maybe-map-cool-2 : ∀ {S S₁ : Set} {f : S → S₁} {x : S} {z}
                  → f x ≡ z
                  → Maybe-map f (just x) ≡ just z
 Maybe-map-cool-2 {S}{S₁}{f}{x}{z} prf rewrite prf = refl

 T⇒true : ∀ {a : Bool} → T a → a ≡ true
 T⇒true {true} _ = refl

 isJust : ∀ {A : Set}{aMB : Maybe A}{a : A}
        → aMB ≡ just a
        → Is-just aMB
 isJust refl = just tt

 to-witness-isJust-≡ : ∀ {A : Set}{aMB : Maybe A}{a prf}
                     → to-witness (isJust {aMB = aMB} {a} prf) ≡ a
 to-witness-isJust-≡ {aMB = just a'} {a} {prf}
    with to-witness-lemma (isJust {aMB = just a'} {a} prf) refl
 ...| xxx = just-injective (trans (sym xxx) prf)


text:
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.rec.proj:15 #-}
-- {-# OPTIONS --verbose tc.rec:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}
-- {-# OPTIONS --verbose tc.section.apply:15 #-}
-- {-# OPTIONS --verbose tc.mod.apply:15 #-}

module 02-classes-indep where

data T : Set where
  tt : T

data Bool : Set where
  true : Bool
  false : Bool

module testMod (a : Bool) where
  testModEntry : Bool
  testModEntry = a

record Monoid (t : Set) : Set where
  field
    zeroT : t
    plusT : t → t → t
  test : Bool
  test = false

or : Bool → Bool → Bool
or true _ = true
or _ true = true
or false false = false

aT : Monoid T
aT = record { zeroT = tt; plusT = λ _ _ → tt }

testMonoid : {t : Set} → {{tM : Monoid t}} → t → t
testMonoid {{tM}} t = let open Monoid tM in plusT t zeroT

aBool : Monoid Bool
aBool = record { zeroT = false; plusT = or }

test : Bool
test = testMonoid false

open Monoid {{...}}

test2 : {t : Set} → {{tM : Monoid t}} → t
test2 = zeroT

test3 : T
test3 = zeroT

test4 : Bool
test4 = zeroT

⋯ : {A : Set} → {{v : A}} → A
⋯ {{v}} = v

test5 : Bool
test5 = Monoid.zeroT ⋯

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

module Data.Bits.Strict where

open import Data.Bits
open import Prelude

infixr 8 0∷!_ 1∷!_
0∷!_ : Bits → Bits
0∷!_ = λ! xs →! 0∷ xs
{-# INLINE 0∷!_ #-}

1∷!_ : Bits → Bits
1∷!_ = λ! xs →! 1∷ xs
{-# INLINE 1∷!_ #-}

0∷!≡0∷ : ∀ xs → 0∷! xs ≡ 0∷ xs
0∷!≡0∷ = $!-≡ 0∷_

1∷!≡1∷ : ∀ xs → 1∷! xs ≡ 1∷ xs
1∷!≡1∷ = $!-≡ 1∷_

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module CauchyProofsT where

-- Proofs about permutations defined in module Cauchy (multiplicative)

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        proof-irrelevance; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.TrustMe
  using (trustMe)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Nat.Properties
  using (m≤m+n; n≤m+n; n≤1+n; cancel-*-right-≤; ≰⇒>; ¬i+1+j≤i)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+; +-*-suc)
open import Data.Nat.DivMod using (DivMod; result; _divMod_; _div_; _mod_)
open import Relation.Binary using (Rel; Decidable; Setoid)
open import Relation.Binary.Core using (Transitive)

open import Data.String using (String)
  renaming (_++_ to _++S_)
open import Data.Nat.Show using (show)
open import Data.Bool using (Bool; false; true)
open import Data.Nat using (ℕ; suc; _+_; _∸_; _*_; _<_; _≮_; _≤_; _≰_;
  _≥_; z≤n; s≤s; _≟_; _≤?_; ≤-pred; module ≤-Reasoning)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; fromℕ≤; _ℕ-_; _≺_; reduce≥;
         raise; inject+; inject₁; inject≤; _≻toℕ_)
  renaming (_+_ to _F+_)
open import Data.Fin.Properties
  using (bounded; inject+-lemma; to-from; toℕ-injective; inject≤-lemma; toℕ-fromℕ≤)
open import Data.Vec.Properties
  using (lookup∘tabulate; tabulate∘lookup; lookup-allFin; tabulate-∘;
         tabulate-allFin; allFin-map; lookup-++-inject+; lookup-++-≥)
open import Data.Product using (Σ)

open import Data.List
  using (List; []; _∷_; _∷ʳ_; foldl; replicate; reverse; downFrom;
         concatMap; gfilter; initLast; InitLast; _∷ʳ'_)
  renaming (_++_ to _++L_; map to mapL; concat to concatL; zip to zipL)
open import Data.List.NonEmpty
  using (List⁺; [_]; _∷⁺_; head; last; _⁺++_)
  renaming (toList to nonEmptyListtoList; _∷ʳ_ to _n∷ʳ_; tail to ntail)
open import Data.List.Any using (Any; here; there; any; module Membership)
open import Data.Maybe using (Maybe; nothing; just; maybe′)
open import Data.Vec
  using (Vec; tabulate; []; _∷_; tail; lookup; zip; zipWith; splitAt;
         _[_]≔_; allFin; toList)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Function using (id; _∘_; _$_; _∋_)

open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Unit    using (⊤; tt)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import Proofs
open import Cauchy
open import Perm
open import CauchyProofs

------------------------------------------------------------------------------
-- Proofs about multiplicative permutations

concat-nil : ∀ {m} →
  concatV (tabulate {m} (λ b → [])) ≡ subst Cauchy (sym (*-right-zero m)) []
concat-nil {0} = refl
concat-nil {suc m} = concat-nil {m}

empty-vec : ∀ {m} → (eq : m ≡ 0) → allFin m ≡ subst Cauchy (sym eq) []
empty-vec {0} refl = refl
empty-vec {suc m} ()

inj-lemma' : (m n : ℕ) (d : Fin n) (leq : suc (toℕ d) ≤ n + m) →
  inject+ m d ≡ inject≤ (fromℕ (toℕ d)) leq
inj-lemma' m 0 () _
inj-lemma' m (suc n) zero (s≤s _) = refl
inj-lemma' m (suc n) (suc d) (s≤s leq) = cong suc (inj-lemma' m n d leq)

inj-lemma : (m n : ℕ) (d : Fin n) (leq : suc (toℕ d) ≤ suc m * n) →
  inject+ (m * n) d ≡ inject≤ (fromℕ (toℕ d)) leq
inj-lemma m 0 () _
inj-lemma m (suc n) zero (s≤s _) = refl
inj-lemma m (suc n) (suc d) (s≤s leq) = cong suc (inj-lemma' (m * suc n) n d leq)

map-f≡g : {B : Set} (n : ℕ) (f g : Fin n → B) → (∀ i → f i ≡ g i) →
  mapV f (allFin n) ≡ mapV g (allFin n)
map-f≡g n f g eq =
  begin (mapV f (tabulate id)
           ≡⟨ sym (tabulate-∘ f id) ⟩
         tabulate f
           ≡⟨ finext eq ⟩
         tabulate g
           ≡⟨ tabulate-∘ g id ⟩
         mapV g (tabulate id) ∎)
  where open ≡-Reasoning

map-inj-lemma : (m n : ℕ) →
  (mapV (inject+ (m * n)) (allFin n)) ≡
  (mapV
    (λ d → inject≤
             (fromℕ (toℕ d))
             (i*n+k≤m*n {suc m} {n} zero d))
    (allFin n))
map-inj-lemma m n =
  map-f≡g n (inject+ (m * n))
            (λ d → inject≤ (fromℕ (toℕ d)) (i*n+k≤m*n {suc m} zero d))
            (λ d → inj-lemma m n d (i*n+k≤m*n {suc m} zero d))

map-raise-suc : (m n : ℕ) (j : Fin (suc m)) →
  mapV (λ d → raise (suc n)
                (inject≤
                  (fromℕ (toℕ j * suc n + toℕ d))
                   (i*n+k≤m*n j d)))
       (idcauchy (suc n)) ≡
  mapV (λ d → inject≤
                (fromℕ (toℕ (suc j) * suc n + toℕ d))
                (i*n+k≤m*n (suc j) d))
       (idcauchy (suc n))
map-raise-suc m n j = map-f≡g (suc n)
        (λ d → raise (suc n)
            (inject≤
              (fromℕ (toℕ j * suc n + toℕ d))
              (i*n+k≤m*n j d)))
        (λ d → inject≤
            (fromℕ (toℕ (suc j) * suc n + toℕ d))
            (i*n+k≤m*n (suc j) d))
        ( (λ d → raise-suc m n j d (i*n+k≤m*n j d) (i*n+k≤m*n (suc j) d)))

-- what should this be named?

lemma3 : (n m : ℕ) → (j : Fin m) →
  mapV (raise (suc n))
    (mapV (λ d → inject≤
                 (fromℕ (toℕ j * suc n + toℕ d))
                 (i*n+k≤m*n j d))
          (idcauchy (suc n)))
  ≡
  mapV (λ d → inject≤
              (fromℕ (toℕ (suc j) * suc n + toℕ d))
              (i*n+k≤m*n (suc j) d))
       (idcauchy (suc n))
lemma3 n 0 ()
lemma3 n (suc m) j =
  begin (
  _
    ≡⟨ sym (map-∘ (raise (suc n)) (λ d → inject≤
                 (fromℕ (toℕ j * suc n + toℕ d))
                 (i*n+k≤m*n j d)) (idcauchy (suc n))) ⟩
  mapV (λ d → raise (suc n) (inject≤
                 (fromℕ (toℕ j * suc n + toℕ d))
                 (i*n+k≤m*n j d))) (idcauchy (suc n))
    ≡⟨ map-raise-suc m n j ⟩
  _ ∎)
  where open ≡-Reasoning

map-raise-lemma : (m n : ℕ) →
  mapV
    (λ b → mapV
             (raise (suc n))
             (mapV
               (λ d → inject≤
                        (fromℕ (toℕ b * suc n + toℕ d))
                        (i*n+k≤m*n b d))
               (idcauchy (suc n))))
    (idcauchy m) ≡
  mapV
    (λ b → mapV
             (λ d → inject≤
                      (fromℕ (toℕ b * suc n + toℕ d))
                      (i*n+k≤m*n b d))
             (idcauchy (suc n)))
    (tabulate {m} suc)
map-raise-lemma 0 n = refl
map-raise-lemma (suc m) n =
  begin (
  mapV (λ b → mapV (raise (suc n))
             (mapV
               (λ d → inject≤
                        (fromℕ (toℕ b * suc n + toℕ d))
                        (i*n+k≤m*n b d))
               (idcauchy (suc n))))
    (idcauchy (suc m))
    ≡⟨ sym (tabulate-∘ _ id) ⟩
  tabulate  {suc m} (λ b → mapV (raise (suc n))
             (mapV
               (λ d → inject≤
                        (fromℕ (toℕ b * suc n + toℕ d))
                        (i*n+k≤m*n b d))
               (idcauchy (suc n))))
    ≡⟨ finext (lemma3 n (suc m)) ⟩
  tabulate {suc m} ((λ b → mapV
               (λ d → inject≤
                      (fromℕ (toℕ b * suc n + toℕ d))
                      (i*n+k≤m*n b d))
             (idcauchy (suc n))) ∘ suc)
    ≡⟨ tabulate-∘ _ suc ⟩
  mapV (λ b → mapV
             (λ d → inject≤
                      (fromℕ (toℕ b * suc n + toℕ d))
                      (i*n+k≤m*n b d))
             (idcauchy (suc n)))
    (tabulate {suc m} suc) ∎)
  where open ≡-Reasoning

allFin* : (m n : ℕ) → allFin (m * n) ≡
          concatV
            (mapV
              (λ b →
                mapV
                  (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                  (idcauchy n))
            (idcauchy m))
allFin* 0 _ = refl
allFin* (suc m) 0 =
  begin (allFin (suc m * 0)
           ≡⟨ empty-vec {suc m * 0} (*-right-zero (suc m)) ⟩
         subst Cauchy (sym (*-right-zero (suc m))) []
           ≡⟨ sym (concat-nil {suc m}) ⟩
         concatV (tabulate {suc m} (λ b → []))
           ≡⟨ cong concatV (tabulate-allFin {suc m} (λ b → [])) ⟩
         concatV (mapV (λ b → []) (idcauchy (suc m))) ∎)
  where open ≡-Reasoning
allFin* (suc m) (suc n) =
  begin (allFin (suc n + m * suc n)
           ≡⟨ allFin+ (suc n) (m * suc n) ⟩
         mapV (inject+ (m * suc n)) (allFin (suc n)) ++V
         mapV (raise (suc n)) (allFin (m * suc n))
           ≡⟨ cong
                (λ x →
                  mapV (inject+ (m * suc n)) (allFin (suc n)) ++V
                  mapV (raise (suc n)) x)
                (allFin* m (suc n)) ⟩
         mapV (inject+ (m * suc n)) (allFin (suc n)) ++V
         mapV
           (raise (suc n))
           (concatV
             (mapV
               (λ b →
                 mapV
                   (λ d → inject≤
                            (fromℕ (toℕ b * suc n + toℕ d))
                            (i*n+k≤m*n b d))
                   (idcauchy (suc n)))
               (idcauchy m)))
           ≡⟨ cong
                (_++V_ (mapV (inject+ (m * suc n)) (allFin (suc n))))
                (sym (concat-map
                       (mapV
                         (λ b →
                           mapV
                             (λ d → inject≤
                                      (fromℕ (toℕ b * suc n + toℕ d))
                                      (i*n+k≤m*n b d))
                             (idcauchy (suc n)))
                         (idcauchy m))
                       (raise (suc n)))) ⟩
         mapV (inject+ (m * suc n)) (allFin (suc n)) ++V
         concatV
           (mapV
             (mapV (raise (suc n)))
             (mapV
               (λ b →
                 mapV
                   (λ d → inject≤
                            (fromℕ (toℕ b * suc n + toℕ d))
                            (i*n+k≤m*n b d))
                   (idcauchy (suc n)))
               (idcauchy m)))
           ≡⟨ refl ⟩
         concatV
           (mapV (inject+ (m * suc n)) (allFin (suc n)) ∷
            mapV
              (mapV (raise (suc n)))
              (mapV
                (λ b →
                  mapV
                    (λ d → inject≤
                             (fromℕ (toℕ b * suc n + toℕ d))
                             (i*n+k≤m*n b d))
                    (idcauchy (suc n)))
                (idcauchy m)))
           ≡⟨ cong
                 (λ x →
                   concatV
                     ((mapV (inject+ (m * suc n)) (allFin (suc n))) ∷ x))
                 (sym (map-∘
                        (mapV (raise (suc n)))
                        (λ b →
                          mapV
                            (λ d → inject≤
                                     (fromℕ (toℕ b * suc n + toℕ d))
                                     (i*n+k≤m*n b d))
                            (idcauchy (suc n)))
                        (idcauchy m))) ⟩
         concatV
           (mapV (inject+ (m * suc n)) (allFin (suc n)) ∷
            mapV
              (λ b → mapV
                       (raise (suc n))
                       (mapV
                         (λ d → inject≤
                                  (fromℕ (toℕ b * suc n + toℕ d))
                                  (i*n+k≤m*n b d))
                         (idcauchy (suc n))))
              (idcauchy m))
           ≡⟨ cong
                (λ x →
                  concatV
                    (x ∷
                    mapV
                      (λ b →
                        mapV
                          (raise (suc n))
                          (mapV
                            (λ d → inject≤
                                     (fromℕ (toℕ b * suc n + toℕ d))
                                     (i*n+k≤m*n b d))
                            (idcauchy (suc n))))
                      (idcauchy m)))
                (map-inj-lemma m (suc n)) ⟩
         concatV
           (mapV
              (λ d → inject≤
                       (fromℕ (toℕ d))
                       (i*n+k≤m*n {suc m} {suc n} zero d))
              (idcauchy (suc n)) ∷
            (mapV
              (λ b → mapV
                       (raise (suc n))
                       (mapV
                         (λ d → inject≤
                                  (fromℕ (toℕ b * suc n + toℕ d))
                                  (i*n+k≤m*n b d))
                         (idcauchy (suc n))))
              (idcauchy m)))
           ≡⟨ cong
                 (λ x →
                   concatV
                     (mapV
                       (λ d → inject≤
                                (fromℕ (toℕ d))
                                (i*n+k≤m*n {suc m} {suc n} zero d))
                       (idcauchy (suc n)) ∷
                     x))
                 (map-raise-lemma m n) ⟩
         concatV
           (mapV
              (λ d → inject≤
                       (fromℕ (toℕ d))
                       (i*n+k≤m*n {suc m} {suc n} zero d))
              (idcauchy (suc n)) ∷
            (mapV
               (λ b → mapV
                        (λ d → inject≤
                                 (fromℕ (toℕ b * suc n + toℕ d))
                                 (i*n+k≤m*n b d))
                        (idcauchy (suc n)))
               (tabulate {m} suc)))
           ≡⟨ refl ⟩
         concatV
           (mapV
             (λ b →
               mapV
                 (λ d → inject≤
                          (fromℕ (toℕ b * suc n + toℕ d))
                          (i*n+k≤m*n b d))
                 (idcauchy (suc n)))
             (idcauchy (suc m))) ∎)
  where open ≡-Reasoning

tcomp-id : ∀ {m n} → tcompcauchy (idcauchy m) (idcauchy n) ≡ idcauchy (m * n)
tcomp-id {m} {n} = sym (allFin* m n)

-- Behaviour of parallel multiplicative composition wrt sequential

absurd : (m n q : ℕ) (r : Fin (suc n)) (k : Fin (suc (n + m * suc n)))
         (k≡r+q*sn : toℕ k ≡ toℕ r + q * suc n) (p : suc m ≤ q) → ⊥
absurd m n q r k k≡r+q*sn p = ¬i+1+j≤i (toℕ k) {toℕ r} k≥k+sr
  where k≥k+sr : toℕ k ≥ toℕ k + suc (toℕ r)
        k≥k+sr =
          begin (toℕ k + suc (toℕ r)
                   ≡⟨ +-suc (toℕ k) (toℕ r) ⟩
                 suc (toℕ k) + toℕ r
                   ≤⟨ cong+r≤ (bounded k) (toℕ r) ⟩
                 (suc n + m * suc n) + toℕ r
                   ≡⟨ +-comm (suc n + m * suc n) (toℕ r) ⟩
                 toℕ r + (suc n + m * suc n)
                   ≡⟨ refl ⟩
                 toℕ r + suc m * suc n
                   ≤⟨ cong+l≤ (cong*r≤ p (suc n)) (toℕ r) ⟩
                 toℕ r + q * suc n
                   ≡⟨ sym k≡r+q*sn ⟩
                 toℕ k ∎)
          where open ≤-Reasoning

concat-tabulate-[] : ∀ {m n} {f : Fin m →  Fin n} →
    concatV (tabulate {m} ((λ x → []) ∘ f)) ≡
    subst (λ n → Vec (Fin (m * 0)) n) (sym (*-right-zero m)) []
concat-tabulate-[] {0} = refl
concat-tabulate-[] {suc m} {_} {f} = concat-tabulate-[] {m} {_} {f ∘ suc}

tabulate-⊥ : ∀ {m n} {g : Fin (m * 0) → Fin n} →
  tabulate g ≡ subst (Vec (Fin n)) (sym (*-right-zero m)) []
tabulate-⊥ {0} = refl
tabulate-⊥ {suc m}{_} {g} = tabulate-⊥ {m}

toℕ-inject+ : ∀ {n k} → (i : Fin n) → toℕ (inject+ k i) ≡ toℕ i
toℕ-inject+ {0} ()
toℕ-inject+ {suc n} zero = refl
toℕ-inject+ {suc n} (suc i) = cong suc (toℕ-inject+ i)

q≡ : (m : ℕ) (q : ℕ) (¬p : ¬ suc m ≤ q) →
  q ≡ toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p))))
q≡ m q ¬p = sym (toℕ-fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p))))

absurd2 : (n q : ℕ) (i : Fin (suc n)) (r  : Fin (suc (suc n)))
  (eq : suc (toℕ i) ≡ toℕ r + suc (suc (n + q * suc (suc n)))) → ⊥
absurd2 n q i r eq = ¬i+1+j≤i (suc (toℕ i)) {toℕ r} leq
  where leq' = begin (suc (toℕ i)
                   ≤⟨ bounded i ⟩
                      suc n
                   ≤⟨ m≤m+n (suc n) (q * suc (suc n)) ⟩
                      suc (n + q * suc (suc n)) ∎)
               where open ≤-Reasoning
        leq = begin (suc (toℕ i) + suc (toℕ r)
                   ≡⟨ +-suc (suc (toℕ i)) (toℕ r) ⟩
                     suc (suc (toℕ i)) + toℕ r
                   ≡⟨ +-comm (suc (suc (toℕ i))) (toℕ r) ⟩
                     toℕ r + suc (suc (toℕ i))
                   ≤⟨ cong+l≤ (s≤s leq') (toℕ r) ⟩
                     toℕ r + suc (suc (n + q * suc (suc n)))
                   ≡⟨ sym eq ⟩
                     suc (toℕ i) ∎)
              where open ≤-Reasoning

small-quotient : (n q : ℕ) → (i : Fin n) → (r : Fin (suc n)) →
  (eq₁ : suc (toℕ i) ≡ toℕ r + q * suc n) → (q ≡ 0) × (toℕ r ≡ suc (toℕ i))
small-quotient 0 _ () _ _
small-quotient (suc n) 0 i r eq = (refl , sym  (trans eq (+-right-identity (toℕ r))))
small-quotient (suc n) (suc q) i r eq = ⊥-elim (absurd2 n q i r eq)

first-row :
  (m n : ℕ) → (f : Fin (suc m) × Fin (suc n) → Fin ((suc m) * (suc n))) →
  tabulate {suc n} (λ x → f (zero , x)) ≡
  tabulate {suc n} ((λ k →  f (fin-project (suc m) (suc n) k)) ∘ inject+ (m * suc n))
first-row m n f =
  finext pf
    where
      pf : (i : Fin (suc n)) →  f (zero , i) ≡
           f (fin-project (suc m) (suc n) (inject+ (m * suc n) i))
      pf zero = refl
      pf (suc i) with suc (toℕ (inject+ (m * suc n) i)) divMod suc n
      pf (suc i) | result q r property with suc m ≤? q
      pf (suc i) | result q r property | yes p =
                ⊥-elim (absurd m n q r (suc (inject+ (m * suc n) i)) property p)
      pf (suc i) | result q r property | no ¬p =
                cong f (cong₂ _,_ (toℕ-injective (sym a₁)) a₂)
        where
           q≡f₁ : q ≡ toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p))))
           q≡f₁ = q≡ m q ¬p
           si≡f₂ : _≡_ {A = ℕ} (suc (toℕ (inject+ (m * suc n) i)))  (suc (toℕ i))
           si≡f₂ = cong suc (toℕ-inject+ {k = m * suc n} i)
           sq : (q ≡ 0) × (toℕ r ≡ suc (toℕ i))
           sq = small-quotient n q i r (trans (sym si≡f₂) property)
           a₁ : toℕ (fromℕ≤ (s≤s (≤-pred (≰⇒> ¬p)))) ≡ toℕ {suc q} zero
           a₁ = trans (sym q≡f₁) (proj₁ sq)
           a₂ :  (suc i) ≡ r
           a₂ = toℕ-injective (sym (proj₂ sq))

lookup-2d' : (m n : ℕ) (k : Fin (m * n))
  (f : Fin m × Fin n → Fin (m * n)) →
  lookup k (concatV (tabulate (λ i → tabulate (λ j → f (i , j)))))
  ≡ f (fin-project m n k)
lookup-2d' m n k f =
  let fin-result b d dec dec' = fin-divMod m n k in
  begin (lookup k (concatV (tabulate (λ i → tabulate (λ j → f (i , j)))))
        ≡⟨ cong (λ x → lookup k (concatV x))
            (finext (λ i → tabulate-allFin (λ j → f (i , j)))) ⟩
         lookup k (concatV (tabulate (λ i → mapV (λ j → f (i , j)) (allFin n))))
        ≡⟨ cong
             (λ x → lookup k (concatV x))
             (tabulate-allFin (λ i → mapV (λ j → f (i , j)) (allFin n))) ⟩
         lookup k (concatV (mapV (λ i → mapV (λ j → f (i , j)) (allFin n)) (allFin m)))
        ≡⟨ lookup-2d m n k (allFin m) (allFin n) f ⟩
         f (lookup b (allFin m) , lookup d (allFin n))
        ≡⟨ cong₂ (λ x y → f (x , y)) (lookup-allFin b) (lookup-allFin d) ⟩
         f (b , d)
        ≡⟨ cong f (sym (inv' (fin-product-iso m n) (b , d))) ⟩
         f (split (fin-product-iso m n) (combine (fin-product-iso m n) (b , d)))
        ≡⟨ refl ⟩
         f (fin-project m n (combine (fin-product-iso m n) (b , d)))
        ≡⟨ cong
             (λ x → f (fin-project m n x))
             (sym dec') ⟩
         f (fin-project m n k) ∎)
  where open ≡-Reasoning
        open Fin-Product-Iso

tabulate-concat : ∀ {m n} → (f : Fin m × Fin n → Fin (m * n)) →
  concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i , j)))) ≡
  tabulate {m * n} (λ (k : Fin (m * n)) → f (fin-project m n k))
tabulate-concat {m} {n} f =
  begin (concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i , j))))
       ≡⟨ sym (tabulate∘lookup
                (concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i , j)))))) ⟩
         tabulate (λ i →
           lookup i
             (concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i , j))))))
       ≡⟨ finext (λ i → lookup-2d' m n i f) ⟩
         tabulate {m * n} (λ (k : Fin (m * n)) → f (fin-project m n k)) ∎)
  where open ≡-Reasoning

lookup-concat :
  ∀ {m n} → (k : Fin (m * n)) → (pm qm : Cauchy m) → (pn qn : Cauchy n) →
  let vs = concatV
             (mapV
               (λ b →
                 mapV
                   (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                   pn)
             pm)
      ws = concatV
             (mapV
               (λ b →
                 mapV
                   (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                   qn)
             qm)
  in lookup (lookup k vs) ws
  ≡
  let (b , d) = fin-project m n k
      x = lookup (lookup b pm) qm
      y = lookup (lookup d pn) qn
  in inject≤ (fromℕ (toℕ x * n + toℕ y)) (i*n+k≤m*n x y)
lookup-concat {0} () pm qm pn qn
lookup-concat {suc m} {0} k pm qm [] [] =
  ⊥-elim (Fin0-⊥ (subst Fin (*-right-zero m) k))
lookup-concat {suc m} {suc n} zero (x ∷ pm) (x₁ ∷ qm) (x₂ ∷ pn) (x₃ ∷ qn) =
  begin (lookup
           (inject≤ (fromℕ (toℕ x * suc n + toℕ x₂)) (i*n+k≤m*n x x₂))
           (concatV
             (mapV
               (λ b →
                 mapV
                   (λ d → inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                   (x₃ ∷ qn))
               (x₁ ∷ qm)))
       ≡⟨ lookup-concat'
            (suc m) (suc n) x x₂ (i*n+k≤m*n x x₂)
            (λ {(b , d) → inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d)})
            (x₁ ∷ qm) (x₃ ∷ qn) ⟩
         inject≤
           (fromℕ (toℕ (lookup x (x₁ ∷ qm)) * suc n + toℕ (lookup x₂ (x₃ ∷ qn))))
           (i*n+k≤m*n (lookup x (x₁ ∷ qm)) (lookup x₂ (x₃ ∷ qn)))
       ≡⟨ refl ⟩
         let (b , d) = fin-project (suc m) (suc n) zero
             x = lookup (lookup b (x ∷ pm)) (x₁ ∷ qm)
             y = lookup (lookup d (x₂ ∷ pn)) (x₃ ∷ qn)
         in inject≤ (fromℕ (toℕ x * suc n + toℕ y)) (i*n+k≤m*n x y) ∎)
  where open ≡-Reasoning
lookup-concat {suc m} {suc n} (suc k) (x ∷ pm) (x₁ ∷ qm) (x₂ ∷ pn) (x₃ ∷ qn) =
  begin (let vs = concatV
                    (mapV
                      (λ b →
                        mapV
                          (λ d →
                            inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                          (x₂ ∷ pn))
                      (x ∷ pm))
             ws = concatV
                    (mapV
                      (λ b →
                        mapV
                          (λ d →
                            inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                          (x₃ ∷ qn))
                    (x₁ ∷ qm))
         in lookup (lookup (suc k) vs) ws
       ≡⟨ cong (λ z →
                lookup
                  (lookup z
                    (concatV
                      (mapV
                        (λ b →
                          mapV
                            (λ d →
                              inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                            (x₂ ∷ pn))
                        (x ∷ pm))))
                  (concatV
                    (mapV
                      (λ b →
                        mapV
                          (λ d →
                            inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                          (x₃ ∷ qn))
                    (x₁ ∷ qm))))
                  (fin-proj-lem (suc m) (suc n) (suc k)) ⟩
         let (b' , d') = fin-project (suc m) (suc n) (suc k)
             vs = concatV
                    (mapV
                      (λ b →
                        mapV
                          (λ d →
                            inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                          (x₂ ∷ pn))
                      (x ∷ pm))
             ws = concatV
                    (mapV
                      (λ b →
                        mapV
                          (λ d →
                            inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                          (x₃ ∷ qn))
                    (x₁ ∷ qm))
         in lookup
              (lookup
                (inject≤ (fromℕ (toℕ b' * (suc n) + toℕ d')) (i*n+k≤m*n b' d'))
                vs)
              ws
       ≡⟨ cong
            (λ x → lookup x ws)
            (lookup-concat' (suc m) (suc n) b' d' (i*n+k≤m*n b' d')
              (λ {(b , d) → inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d)})
              (x ∷ pm) (x₂ ∷ pn)) ⟩
         let (b' , d') = fin-project (suc m) (suc n) (suc k)
             ws = concatV
                    (mapV
                      (λ b →
                        mapV
                          (λ d →
                            inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d))
                          (x₃ ∷ qn))
                    (x₁ ∷ qm))
         in lookup
              (inject≤
                (fromℕ (toℕ (lookup b' (x ∷ pm)) * suc n + toℕ (lookup d' (x₂ ∷ pn))))
                (i*n+k≤m*n (lookup b' (x ∷ pm)) (lookup d' (x₂ ∷ pn))))
              ws
       ≡⟨ lookup-concat' (suc m) (suc n) (lookup b' (x ∷ pm)) (lookup d' (x₂ ∷ pn))
             (i*n+k≤m*n (lookup b' (x ∷ pm)) (lookup d' (x₂ ∷ pn)))
             (λ {(b , d) → inject≤ (fromℕ (toℕ b * suc n + toℕ d)) (i*n+k≤m*n b d)})
             (x₁ ∷ qm) (x₃ ∷ qn) ⟩
         let (b , d) = fin-project (suc m) (suc n) (suc k)
             r = lookup (lookup b (x ∷ pm)) (x₁ ∷ qm)
             s = lookup (lookup d (x₂ ∷ pn)) (x₃ ∷ qn)
         in inject≤
              (fromℕ (toℕ r * suc n + toℕ s))
              (i*n+k≤m*n r s) ∎)
  where open ≡-Reasoning

tcomp-dist : ∀ {m n} → (pm qm : Cauchy m) → (pn qn : Cauchy n) →
  scompcauchy (tcompcauchy pm pn) (tcompcauchy qm qn) ≡
  tcompcauchy (scompcauchy pm qm) (scompcauchy pn qn)
tcomp-dist {m} {n} pm qm pn qn =
  begin (scompcauchy (tcompcauchy pm pn) (tcompcauchy qm qn)
           ≡⟨ refl ⟩
         tabulate {m * n} (λ k →
           lookup
             (lookup k (concatV
                         (mapV
                           (λ b →
                             mapV (λ d →
                               inject≤
                                 (fromℕ (toℕ b * n + toℕ d))
                                 (i*n+k≤m*n b d)) pn)
                           pm)))
             (concatV
               (mapV
                 (λ b →
                   mapV (λ d →
                     inject≤
                       (fromℕ (toℕ b * n + toℕ d))
                       (i*n+k≤m*n b d)) qn)
                 qm)))
           ≡⟨  finext (λ k → lookup-concat {m} {n} k pm qm pn qn) ⟩
         tabulate {m * n}
           (λ k →
             let (i , j) = fin-project m n k
                 b = lookup (lookup i pm) qm
                 d = lookup (lookup j pn) qn in
             inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
           ≡⟨  sym (tabulate-concat
                 (λ {(i , j) →
                   let b = lookup (lookup i pm) qm
                       d = lookup (lookup j pn) qn in
                   inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d)})) ⟩
         concatV
           (tabulate {m}
             (λ i →
               tabulate {n}
                 (λ j →
                   let b = lookup (lookup i pm) qm
                       d = lookup (lookup j pn) qn in
                   inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))))
           ≡⟨  cong concatV
                 (finext
                   (λ i →
                     tabulate-∘
                       (let b = lookup (lookup i pm) qm in
                        λ d →
                          inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                       (λ i → lookup (lookup i pn) qn))) ⟩
         concatV
           (tabulate {m}
             (λ i →
               let b = lookup (lookup i pm) qm in
               mapV
                 (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                 (tabulate (λ i → lookup (lookup i pn) qn))))
           ≡⟨ cong concatV (tabulate-∘
                (λ b →
                  mapV
                    (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                    (tabulate (λ i → lookup (lookup i pn) qn)))
                 (λ i → lookup (lookup i pm) qm)) ⟩
         concatV
           (mapV
             (λ b →
               mapV
                 (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d))
                 (tabulate (λ i → lookup (lookup i pn) qn)))
             (tabulate (λ i → lookup (lookup i pm) qm)))
           ≡⟨  refl ⟩
         tcompcauchy (scompcauchy pm qm) (scompcauchy pn qn) ∎)
  where open ≡-Reasoning

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Andreas, 2016-07-29 issue #707

-- {-# OPTIONS -v tc.ip:20 #-}

postulate A B : {!!}

-- Should not create two interaction points!
-- Also not two sort metas!

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the case expressions can be used with anonymous
-- pattern-matching lambda abstractions
------------------------------------------------------------------------

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

module README.Case where

open import Data.Fin   hiding (pred)
open import Data.Maybe hiding (from-just)
open import Data.Nat   hiding (pred)
open import Data.List
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Different types of pattern-matching lambdas

-- absurd pattern

empty : ∀ {a} {A : Set a} → Fin 0 → A
empty i = case i of λ ()

-- {}-delimited and ;-separated list of clauses
-- Note that they do not need to be on different lines

pred : ℕ → ℕ
pred n = case n of λ
  { zero    → zero
  ; (suc n) → n
  }

-- where-introduced and indentation-identified block of list of clauses

from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x
from-just x = case x return From-just of λ where
  (just x) → x
  nothing  → _

------------------------------------------------------------------------
-- We can define some recursive functions with case

plus : ℕ → ℕ → ℕ
plus m n = case m of λ
   { zero    → n
   ; (suc m) → suc (plus m n)
   }

div2 : ℕ → ℕ
div2 zero    = zero
div2 (suc m) = case m of λ where
  zero     → zero
  (suc m') → suc (div2 m')

-- Note that some natural uses of case are rejected by the termination
-- checker:

-- module _ {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where

--  pairBy : List A → List (A ⊎ (A × A))
--  pairBy []           = []
--  pairBy (x ∷ [])     = inj₁ x ∷ []
--  pairBy (x ∷ y ∷ xs) = case eq? x y of λ where
--    (yes _) → inj₂ (x , y) ∷ pairBy xs
--    (no _)  → inj₁ x ∷ pairBy (y ∷ xs)


text:
open import Oscar.Prelude
open import Oscar.Data.¶

module Oscar.Data.Vec where

data ⟨_⟩¶⟨≤_⟩ {𝔭} (𝔓 : ¶ → Ø 𝔭) : ¶ → Ø 𝔭 where
  ∅ : ⟨ 𝔓 ⟩¶⟨≤ ∅ ⟩
  _,_ : ∀ {n} → 𝔓 n → ⟨ 𝔓 ⟩¶⟨≤ n ⟩ → ⟨ 𝔓 ⟩¶⟨≤ ↑ n ⟩

Vec⟨_⟩ = ⟨_⟩¶⟨≤_⟩


text:
module Logic.Structure.Applicative where

data Applicative (f : Set -> Set) : Set1 where
  applicative :
      (pure  : {a : Set} -> a -> f a)
      (_<*>_ : {a b : Set} -> f (a -> b) -> f a -> f b) ->
      Applicative f

module Applicative {f : Set -> Set}(App : Applicative f) where

  private
    pure' : Applicative f -> {a : Set} -> a -> f a
    pure' (applicative p _) = p

    app' : Applicative f -> {a b : Set} -> f (a -> b) -> f a -> f b
    app' (applicative _ a) = a

  pure : {a : Set} -> a -> f a
  pure = pure' App

  _<*>_ : {a b : Set} -> f (a -> b) -> f a -> f b
  _<*>_ = app' App

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import HoTT

module groups.ProductRepr {i j}
  {G : Group (lmax i j)} {H₁ : Group i} {H₂ : Group j}
  (i₁ : H₁ →ᴳ G) (i₂ : H₂ →ᴳ G) (j₁ : G →ᴳ H₁) (j₂ : G →ᴳ H₂)
  (p₁ : ∀ h₁ → GroupHom.f j₁ (GroupHom.f i₁ h₁) == h₁)
  (p₂ : ∀ h₂ → GroupHom.f j₂ (GroupHom.f i₂ h₂) == h₂)
  (ex₁ : is-exact i₁ j₂) (ex₂ : is-exact i₂ j₁) where

  {- Given the following commutative diagram of homomorphisms,

         H₁  i₁  i₂  H₂
            ↘     ↙
      id ↓     G     ↓ id
             ↙   ↘
         H₁ j₁   j₂  H₂

   - assuming i₁,j₂ and i₂,j₁ are exact sequences,
   - there exists an isomorphism G == H₁ × H₂ such that i₁,i₂ correspond
   - to the natural injections and j₁,j₂ correspond to the natural
   - projections. -}

  private
    module G = Group G
    module H₁ = Group H₁
    module H₂ = Group H₂
    module i₁ = GroupHom i₁
    module i₂ = GroupHom i₂
    module j₁ = GroupHom j₁
    module j₂ = GroupHom j₂

  fanout-has-trivial-ker : has-trivial-kerᴳ (×ᴳ-fanout j₁ j₂)
  fanout-has-trivial-ker g q = Trunc-rec (G.El-level _ _)
      (lemma g (fst×= q))
      (ker-sub-im ex₁ g (snd×= q))
    where
    lemma : ∀ g → j₁.f g == H₁.ident
      → hfiber i₁.f g → g == G.ident
    lemma ._ r (h , idp) =
      ap i₁.f (! (p₁ h) ∙ r) ∙ i₁.pres-ident

  β₁ : (h₁ : H₁.El) (h₂ : H₂.El)
    → j₁.f (G.comp (i₁.f h₁) (i₂.f h₂)) == h₁
  β₁ h₁ h₂ =
    j₁.pres-comp (i₁.f h₁) (i₂.f h₂)
    ∙ ap2 H₁.comp (p₁ h₁) (im-sub-ker ex₂ _ [ h₂ , idp ])
    ∙ H₁.unit-r h₁

  β₂ : (h₁ : H₁.El) (h₂ : H₂.El)
    → j₂.f (G.comp (i₁.f h₁) (i₂.f h₂)) == h₂
  β₂ h₁ h₂ =
    j₂.pres-comp (i₁.f h₁) (i₂.f h₂)
    ∙ ap2 H₂.comp (im-sub-ker ex₁ _ [ h₁ , idp ]) (p₂ h₂)
    ∙ H₂.unit-l h₂

  iso : G ≃ᴳ (H₁ ×ᴳ H₂)
  iso = surjᴳ-and-injᴳ-iso (×ᴳ-fanout j₁ j₂)
    (λ {(h₁ , h₂) → [ G.comp (i₁.f h₁) (i₂.f h₂) ,
                      pair×= (β₁ h₁ h₂) (β₂ h₁ h₂) ]})
    (has-trivial-ker-is-injᴳ (×ᴳ-fanout j₁ j₂) fanout-has-trivial-ker)

  j₁-fst-comm-sqr : CommSquareᴳ j₁ ×ᴳ-fst (–>ᴳ iso) (idhom _)
  j₁-fst-comm-sqr = comm-sqrᴳ λ _ → idp

  j₂-snd-comm-sqr : CommSquareᴳ j₂ (×ᴳ-snd {G = H₁}) (–>ᴳ iso) (idhom _)
  j₂-snd-comm-sqr = comm-sqrᴳ λ _ → idp

  abstract
    i₁-inl-comm-sqr : CommSquareᴳ i₁ ×ᴳ-inl (idhom _) (–>ᴳ iso)
    i₁-inl-comm-sqr = comm-sqrᴳ λ h₁ →
      pair×= (p₁ h₁) (im-sub-ker ex₁ _ [ h₁ , idp ])

    i₂-inr-comm-sqr : CommSquareᴳ i₂ ×ᴳ-inr (idhom _) (–>ᴳ iso)
    i₂-inr-comm-sqr = comm-sqrᴳ λ h₂ →
      pair×= (im-sub-ker ex₂ _ [ h₂ , idp ]) (p₂ h₂)

  {- Given additionally maps

            i₀    j₀
         K –––→ G ––→ L

   - such that j₀∘i₀ = 0, we have j₀(i₁(j₁(i₀ k)))⁻¹ = j₀(i₂(j₂(i₀ k))).
   - (This is called the hexagon lemma in Eilenberg & Steenrod's book.
   - The hexagon is not visible in this presentation.)
   -}

  module HexagonLemma {k l}
    {K : Group k} {L : Group l}
    (i₀ : K →ᴳ G) (j₀ : G →ᴳ L)
    (ex₀ : ∀ g → GroupHom.f j₀ (GroupHom.f i₀ g) == Group.ident L)
    where

    abstract
      decomp : ∀ g → G.comp (i₁.f (j₁.f g)) (i₂.f (j₂.f g)) == g
      decomp g = <– (ap-equiv (GroupIso.f-equiv iso) _ g) $
        GroupIso.f iso (G.comp (i₁.f (j₁.f g)) (i₂.f (j₂.f g)))
          =⟨ GroupIso.pres-comp iso (i₁.f (j₁.f g)) (i₂.f (j₂.f g)) ⟩
        Group.comp (H₁ ×ᴳ H₂) (GroupIso.f iso (i₁.f (j₁.f g))) (GroupIso.f iso (i₂.f (j₂.f g)))
          =⟨ ap2 (Group.comp (H₁ ×ᴳ H₂))
              ((i₁-inl-comm-sqr □$ᴳ j₁.f g) ∙ ap (_, H₂.ident) (j₁-fst-comm-sqr □$ᴳ g))
              ((i₂-inr-comm-sqr □$ᴳ j₂.f g) ∙ ap (H₁.ident ,_) (j₂-snd-comm-sqr □$ᴳ g)) ⟩
        (H₁.comp (fst (GroupIso.f iso g)) H₁.ident , H₂.comp H₂.ident (snd (GroupIso.f iso g)))
          =⟨ pair×= (H₁.unit-r (fst (GroupIso.f iso g))) (H₂.unit-l (snd (GroupIso.f iso g))) ⟩
        (fst (GroupIso.f iso g) , snd (GroupIso.f iso g))
          =⟨ idp ⟩
        GroupIso.f iso g
          =∎

      cancel : ∀ k →
        Group.comp L (GroupHom.f (j₀ ∘ᴳ i₁ ∘ᴳ j₁ ∘ᴳ i₀) k)
                     (GroupHom.f (j₀ ∘ᴳ i₂ ∘ᴳ j₂ ∘ᴳ i₀) k)
        == Group.ident L
      cancel k = ! (GroupHom.pres-comp j₀ _ _)
               ∙ ap (GroupHom.f j₀) (decomp (GroupHom.f i₀ k))
               ∙ ex₀ k

      inv₁ : ∀ k → Group.inv L (GroupHom.f (j₀ ∘ᴳ i₁ ∘ᴳ j₁ ∘ᴳ i₀) k)
                == GroupHom.f (j₀ ∘ᴳ i₂ ∘ᴳ j₂ ∘ᴳ i₀) k
      inv₁ k = Group.inv-unique-r L _ _ (cancel k)

      inv₂ : ∀ k → Group.inv L (GroupHom.f (j₀ ∘ᴳ i₂ ∘ᴳ j₂ ∘ᴳ i₀) k)
                == GroupHom.f (j₀ ∘ᴳ i₁ ∘ᴳ j₁ ∘ᴳ i₀) k
      inv₂ k = Group.inv-unique-l L _ _ (cancel k)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Intuitionistic propositional logic, de Bruijn approach, final encoding

module Bf.Ip where

open import Lib using (List; _,_; LMem; lzero; lsuc)

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Set
Cx = List Ty

isTrue : Ty -> Cx -> Set
isTrue a tc = LMem a tc

-- Terms

TmRepr : Set1
TmRepr = Cx -> Ty -> Set

module ArrMp where
  record Tm (tr : TmRepr) : Set1 where
    infixl 1 _$_
    infixr 0 lam=>_
    field
      var    : forall {tc a}   -> isTrue a tc               -> tr tc a
      lam=>_ : forall {tc a b} -> tr (tc , a) b             -> tr tc (a => b)
      _$_    : forall {tc a b} -> tr tc (a => b) -> tr tc a -> tr tc b

    v0 : forall {tc a} -> tr (tc , a) a
    v0 = var lzero

    v1 : forall {tc a b} -> tr (tc , a , b) a
    v1 = var (lsuc lzero)

    v2 : forall {tc a b c} -> tr (tc , a , b , c) a
    v2 = var (lsuc (lsuc lzero))
  open Tm {{...}} public

module Mp where
  record Tm (tr : TmRepr) : Set1 where
    field
      pair' : forall {tc a b}   -> tr tc a        -> tr tc b -> tr tc (a && b)
      fst   : forall {tc a b}   -> tr tc (a && b)            -> tr tc a
      snd   : forall {tc a b}   -> tr tc (a && b)            -> tr tc b
      left  : forall {tc a b}   -> tr tc a                   -> tr tc (a || b)
      right : forall {tc a b}   -> tr tc b                   -> tr tc (a || b)
      case' : forall {tc a b c} -> tr tc (a || b) -> tr (tc , a) c -> tr (tc , b) c -> tr tc c

      isArrMp : ArrMp.Tm tr
    open ArrMp.Tm isArrMp public

    syntax pair' x y    = [ x , y ]
    syntax case' xy x y = case xy => x => y
  open Tm {{...}} public

module Ip where
  record Tm (tr : TmRepr) : Set1 where
    field
      abort : forall {tc a} -> tr tc FALSE -> tr tc a

      isMp : Mp.Tm tr
    open Mp.Tm isMp public
  open Tm {{...}} public

  Thm : Ty -> Set1
  Thm a = forall {tr tc} {{_ : Tm tr}} -> tr tc a
open Ip public

-- Example theorems

t1 : forall {a b} -> Thm (a => NOT a => b)
t1 =
  lam=>
    lam=> abort (v0 $ v1)

t2 : forall {a b} -> Thm (NOT a => a => b)
t2 =
  lam=>
    lam=> abort (v1 $ v0)

t3 : forall {a} -> Thm (a => NOT (NOT a))
t3 =
  lam=>
    lam=> v0 $ v1

t4 : forall {a} -> Thm (NOT a <=> NOT (NOT (NOT a)))
t4 =
  [ lam=>
      lam=> v0 $ v1
  , lam=>
      lam=> v1 $ (lam=> v0 $ v1)
  ]

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
------------------------------------------------------------------------
-- Experiments related to equality
--
-- Nils Anders Danielsson
--
-- Some files have been developed in collaboration with others, see
-- the individual files.
------------------------------------------------------------------------

{-# OPTIONS --cubical --with-K --guardedness --sized-types --prop #-}

module README where

-- "Safe" code that uses --without-K.

import README.Safe.Without-K

-- "Safe" code that uses --erased-cubical.

import README.Safe.Cubical.Erased

-- "Safe" code that uses --erased-cubical and --guardedness.

import README.Safe.Cubical.Erased.Guardedness

-- "Safe" code that uses --erased-cubical and --prop.

import README.Safe.Cubical.Erased.Prop

-- "Safe" code that uses --cubical.

import README.Safe.Cubical

-- "Safe" code that uses --with-K.

import README.Safe.With-K

-- Code which might depend on potentially unsafe features (other than
-- --sized-types).

import README.Unsafe

-- Code which is "safe", except for the use of --sized-types.

import README.Unsafe.Sized-types

-- Code related to the paper "Logical properties of a modality for
-- erasure". This code uses both --cubical and --with-K, but not at
-- the same time, except in the module README.Erased, which for that
-- reason cannot use --safe.

import README.Erased

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category

-- small indexed products of specific shapes

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

open Category C
-- open Equiv

open import Level

open import Categories.Support.Equivalence using (Setoid; module Setoid)

import Categories.Object.Indexed as IObj
import Categories.Object.IndexedProduct as IProduct
import Categories.Morphism.Indexed as IArrow
import Categories.Morphisms as Morphisms

record IndexedProducts {c q} {Shape : Setoid c q} : Set (o ⊔ ℓ ⊔ e ⊔ c ⊔ q) where
  open IObj C Shape
  open IArrow C Shape
  open IProduct C
  module Fan-Setoid {V} (xs : Dust) = Setoid (fan-setoid V xs)
  open Fan-Setoid using () renaming (_≈_ to _[_≜_])

  field
    product : ∀ {As} → IndexedProduct Shape As

  ∏ : ∀ As → Obj
  ∏ As = IndexedProduct.∏ (product {As})

  -- ×-comm : ∀ {A B} → _≅_ C (A × B) (B × A)
  -- ×-comm = Commutative product product

  -- ×-assoc : ∀ {X Y Z} → _≅_ C (X × (Y × Z)) ((X × Y) × Z)
  -- ×-assoc = Associative product product product product

  -- Convenience!  well, sort of.
  module Product {As} = IndexedProduct {As = As} (product {As = As})
  open Product using (π; π[_]; π-cong; π▹_; uncurry; commute; commute∗; universal; universal∗; g-η; η; uncurry-cong; uncurry-cong∗; uncurry∘)

  -- assocˡ : ∀ {A B C} → (((A × B) × C) ⇒ (A × (B × C)))
  -- assocˡ = _≅_.g C ×-assoc

  -- assocʳ : ∀ {A B C} → ((A × (B × C)) ⇒ ((A × B) × C))
  -- assocʳ = _≅_.f C ×-assoc

  _⋉π : ∀ {As Bs} → (As ∗⇒∗ Bs) → (∏ As ⇒∗ Bs)
  _⋉π {As} {Bs} fs = _⋉_ {Ys = As} {Bs} fs (π {As})

  bundle : ∀ {As Bs} → (As ∗⇒∗ Bs) → (∏ As ⇒ ∏ Bs)
  bundle {As} {Bs} fs = uncurry {Bs} (_⋉π {As} {Bs} fs)

  -- TODO: this is probably harder to use than necessary because of this definition. Maybe make a version
  -- that doesn't have an explicit id in it, too?
  -- first : ∀ {A B C} → (A ⇒ B) → ((A × C) ⇒ (B × C))
  -- first f = f ⁂ id

  -- second : ∀ {A C D} → (C ⇒ D) → ((A × C) ⇒ (A × D))
  -- second g = id ⁂ g

  -- Just to make this more obvious
  .π▹bundle : ∀ {As Bs} {fs : As ∗⇒∗ Bs} → Bs [ π▹ bundle {As} {Bs} fs ≜ _⋉π {As} {Bs} fs ]
  π▹bundle {As} {Bs} {fs = fs} = commute∗ {Bs} (_⋉π {As} {Bs} fs)

  .π∘bundle : ∀ {As Bs} {fs : As ∗⇒∗ Bs} {x} → π[_] {Bs} x ∘ bundle {As} {Bs} fs ≡ (fs ‼ x) ∘ π[_] {As} x
  π∘bundle {As} {Bs} {fs = fs} = commute {Bs} (_⋉π {As} {Bs} fs)

  .bundle∘uncurry : ∀ {A Bs Cs} {fs : Bs ∗⇒∗ Cs} {gs : A ⇒∗ Bs} → bundle {Bs} {Cs} fs ∘ uncurry {Bs} gs ≡ uncurry {Cs} (_⋉_ {Ys = Bs} {Cs} fs gs)
  bundle∘uncurry {Bs = Bs} {Cs} {fs = fs} {gs} = Equiv.sym (universal {Cs} (_⋉_ {Ys = Bs} {Cs} fs gs) helper)
    where
    helper : ∀ {x} → π[_] {Cs} x ∘ (bundle {Bs} {Cs} fs ∘ uncurry {Bs} gs) ≡ (fs ‼ x) ∘ (gs ‼ x)
    helper {x} =
      begin
        π[_] {Cs} x ∘ (bundle {Bs} {Cs} fs ∘ uncurry {Bs} gs)
      ↑⟨ assoc ⟩
        (π[_] {Cs} x ∘ bundle {Bs} {Cs} fs) ∘ uncurry {Bs} gs
      ↓⟨ ∘-resp-≡ˡ (π∘bundle {Bs} {Cs} {fs = fs}) ⟩
        ((fs ‼ x) ∘ π[_] {Bs} x) ∘ uncurry {Bs} gs
      ↓⟨ assoc ⟩
        (fs ‼ x) ∘ (π[_] {Bs} x ∘ uncurry {Bs} gs)
      ↓⟨ ∘-resp-≡ʳ (commute {Bs} gs) ⟩
        (fs ‼ x) ∘ (gs ‼ x)
      ∎
      where
      open HomReasoning

  {-
  .first∘⟨⟩ : ∀ {A B C D} → {f : B ⇒ C} {f′ : A ⇒ B} {g′ : A ⇒ D} → first f ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f ∘ f′ , g′ ⟩
  first∘⟨⟩ {f = f} {f′} {g′} =
    begin
      first f ∘ ⟨ f′ , g′ ⟩
    ↓⟨ ⁂∘⟨⟩ ⟩
      ⟨ f ∘ f′ , id ∘ g′ ⟩
    ↓⟨ ⟨⟩-cong₂ refl identityˡ ⟩
      ⟨ f ∘ f′ , g′ ⟩
    ∎
    where
    open HomReasoning

  .second∘⟨⟩ : ∀ {A B D E} → {f′ : A ⇒ B} {g : D ⇒ E} {g′ : A ⇒ D} → second g ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f′ , g ∘ g′ ⟩
  second∘⟨⟩ {f′ = f′} {g} {g′} =
    begin
      second g ∘ ⟨ f′ , g′ ⟩
    ↓⟨ ⁂∘⟨⟩ ⟩
      ⟨ id ∘ f′ , g ∘ g′ ⟩
    ↓⟨ ⟨⟩-cong₂ identityˡ refl ⟩
      ⟨ f′ , g ∘ g′ ⟩
    ∎
    where
    open HomReasoning
  -}

  .bundle∘bundle : ∀ {As Bs Cs} → {fs : Bs ∗⇒∗ Cs} {gs : As ∗⇒∗ Bs} → (bundle {Bs} {Cs} fs) ∘ (bundle {As} {Bs} gs) ≡ bundle {As} {Cs} (_◽_ {As} {Bs} {Cs} fs gs)
  bundle∘bundle {As} {Bs} {Cs} {fs = fs} {gs} =
    begin
      (bundle {Bs} {Cs} fs) ∘ (bundle {As} {Bs} gs)
    ↓⟨ bundle∘uncurry {Bs = Bs} {Cs} {fs = fs} ⟩
      uncurry {Cs} (_⋉_ {Ys = Bs} {Cs} fs (_⋉_ {Ys = As} {Bs} gs (π {As})))
    ↑⟨ uncurry-cong∗ {Cs} {_} {_⋉_ {Ys = As} {Cs} (_◽_ {As} {Bs} {Cs} fs gs) (π {As})} {_⋉_ {Ys = Bs} {Cs} fs (_⋉_ {Ys = As} {Bs} gs (π {As}))} (assoc-◽⋉ {Ys = As} {Bs} {Cs} {fs} {gs} {π {As}}) ⟩
      (bundle {As} {Cs} (_◽_ {As} {Bs} {Cs} fs gs))
    ∎
    where
    open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Issue807b where

open import Common.Coinduction

data Unit : Set where
  unit : Unit

From-unit : Unit → Set
From-unit unit = Unit

from-unit : (x : Unit) → From-unit x
from-unit unit = unit

data D : Set where
  d₁ : D
  d₂ : ∞ D → D

foo : D → Unit
foo d₁     = unit
foo (d₂ x) with ♭ x
foo (d₂ x) | d₁   = unit
foo (d₂ x) | d₂ _ = unit

-- x : ∞ D
x = ♯ d₁

-- There was an internal error if type-signature was not supplied.


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

open import Prelude
open import Relation.Binary

module Relation.Binary.Construct.UpperBound {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open TotalOrder totalOrder renaming (refl to <-refl)
import Data.Unit.UniversePolymorphic as Poly
import Data.Empty.UniversePolymorphic as Poly
open import Data.Maybe.Base using () renaming (nothing to ⌈⊤⌉; just to ⌈_⌉) public

⌈∙⌉ : Type e
⌈∙⌉ = Maybe E

_≤⌈_⌉ : ⌈∙⌉ → E → Type _
⌈⊤⌉   ≤⌈ y ⌉ = Poly.⊥
⌈ x ⌉ ≤⌈ y ⌉ = x ≤ y

_⌈≤⌉_ : ⌈∙⌉ → ⌈∙⌉ → Type _
x ⌈≤⌉ ⌈⊤⌉   = Poly.⊤
x ⌈≤⌉ ⌈ y ⌉ = x ≤⌈ y ⌉

⌈_⌉<_ : E → ⌈∙⌉ → Type _
⌈ x ⌉< ⌈⊤⌉   = Poly.⊤
⌈ x ⌉< ⌈ y ⌉ = x < y

_⌈<⌉_ : ⌈∙⌉ → ⌈∙⌉ → Type _
⌈⊤⌉   ⌈<⌉ _ = Poly.⊥
⌈ x ⌉ ⌈<⌉ y = ⌈ x ⌉< y

ub-pord : PartialOrder ⌈∙⌉ _
ub-pord .PartialOrder.preorder .Preorder._≤_ = _⌈≤⌉_
ub-pord .PartialOrder.preorder .Preorder.refl {⌈⊤⌉} = Poly.tt
ub-pord .PartialOrder.preorder .Preorder.refl {⌈ x ⌉} = <-refl
ub-pord .PartialOrder.preorder .Preorder.trans {x} {y} {⌈⊤⌉} x≤y y≤z = Poly.tt
ub-pord .PartialOrder.preorder .Preorder.trans {⌈ x ⌉} {⌈ y ⌉} {⌈ z ⌉} x≤y y≤z = ≤-trans x≤y y≤z
ub-pord .PartialOrder.antisym {⌈⊤⌉} {⌈⊤⌉} p q = refl
ub-pord .PartialOrder.antisym {⌈ x ⌉} {⌈ y ⌉} p q = cong ⌈_⌉ (antisym p q)

ub-sord : StrictPartialOrder ⌈∙⌉ _
StrictPreorder._<_   (StrictPartialOrder.strictPreorder ub-sord) = _⌈<⌉_
StrictPreorder.trans (StrictPartialOrder.strictPreorder ub-sord) {⌈ x ⌉} {⌈ y ⌉} {⌈⊤⌉} p q = Poly.tt
StrictPreorder.trans (StrictPartialOrder.strictPreorder ub-sord) {⌈ x ⌉} {⌈ y ⌉} {⌈ z ⌉} p q = <-trans p q
StrictPreorder.irrefl  (StrictPartialOrder.strictPreorder ub-sord) {⌈ x ⌉} = irrefl {x = x}
StrictPartialOrder.conn ub-sord {⌈⊤⌉} {⌈⊤⌉} p q = refl
StrictPartialOrder.conn ub-sord {⌈⊤⌉} {⌈ x ⌉} p q = ⊥-elim (q Poly.tt)
StrictPartialOrder.conn ub-sord {⌈ x ⌉} {⌈⊤⌉} p q = ⊥-elim (p Poly.tt)
StrictPartialOrder.conn ub-sord {⌈ x ⌉} {⌈ y ⌉} p q = cong ⌈_⌉ (conn p q)

ub-lt : ∀ x y → Dec (x ⌈<⌉ y)
ub-lt ⌈⊤⌉ y = no λ ()
ub-lt ⌈ x ⌉ ⌈⊤⌉ = yes Poly.tt
ub-lt ⌈ x ⌉ ⌈ y ⌉ = x <? y

ub-ord : TotalOrder ⌈∙⌉ _ _
TotalOrder.strictPartialOrder ub-ord = ub-sord
TotalOrder.partialOrder ub-ord = ub-pord
TotalOrder._<?_ ub-ord = ub-lt
TotalOrder.≰⇒> ub-ord {x} {⌈⊤⌉} p = ⊥-elim (p Poly.tt)
TotalOrder.≰⇒> ub-ord {⌈⊤⌉} {⌈ y ⌉} p = Poly.tt
TotalOrder.≰⇒> ub-ord {⌈ x ⌉} {⌈ y ⌉} p = ≰⇒> p
TotalOrder.≮⇒≥ ub-ord {⌈⊤⌉} {y} p = Poly.tt
TotalOrder.≮⇒≥ ub-ord {⌈ x ⌉} {⌈⊤⌉} p = ⊥-elim (p Poly.tt)
TotalOrder.≮⇒≥ ub-ord {⌈ x ⌉} {⌈ y ⌉} p = ≮⇒≥ p

import Data.Maybe.Sugar
module UBSugar = Data.Maybe.Sugar


text:
variable A : Set

f : A
f = {!!}

-- The goal type should be printed as A, not A₁.
-- Introducing the hidden variable with C-c C-c should choose name A.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propositional equality
--
-- This file contains some core definitions which are re-exported by
-- Relation.Binary.PropositionalEquality.
------------------------------------------------------------------------

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

module Relation.Binary.PropositionalEquality.Core where

open import Data.Product using (_,_)
open import Level
open import Relation.Binary.Core
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- Propositional equality

open import Agda.Builtin.Equality public

infix 4 _≢_
_≢_ : ∀ {a} {A : Set a} → Rel A a
x ≢ y = ¬ x ≡ y

------------------------------------------------------------------------
-- Some properties

module _ {a} {A : Set a} where

  sym : Symmetric {A = A} _≡_
  sym refl = refl

  trans : Transitive {A = A} _≡_
  trans refl eq = eq

  subst : ∀ {p} → Substitutive {A = A} _≡_ p
  subst P refl p = p

  cong : ∀ {b} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
  cong f refl = refl

  respˡ : ∀ {ℓ} (∼ : Rel A ℓ) → ∼ Respectsˡ _≡_
  respˡ _∼_ refl x∼y = x∼y

  respʳ : ∀ {ℓ} (∼ : Rel A ℓ) → ∼ Respectsʳ _≡_
  respʳ _∼_ refl x∼y = x∼y

  resp₂ : ∀ {ℓ} (∼ : Rel A ℓ) → ∼ Respects₂ _≡_
  resp₂ _∼_ = respʳ _∼_ , respˡ _∼_

  isEquivalence : IsEquivalence {A = A} _≡_
  isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }

------------------------------------------------------------------------
-- Various equality rearrangement lemmas

module _ {a} {A : Set a} {x y : A} where

  trans-reflʳ : (p : x ≡ y) → trans p refl ≡ p
  trans-reflʳ refl = refl

  trans-assoc : ∀ {z u} (p : x ≡ y) {q : y ≡ z} {r : z ≡ u} →
    trans (trans p q) r ≡ trans p (trans q r)
  trans-assoc refl = refl

  trans-symˡ : (p : x ≡ y) → trans (sym p) p ≡ refl
  trans-symˡ refl = refl

  trans-symʳ : (p : x ≡ y) → trans p (sym p) ≡ refl
  trans-symʳ refl = refl

------------------------------------------------------------------------
-- Convenient syntax for equational reasoning

-- This is a special instance of `Relation.Binary.Reasoning.Setoid`.
-- Rather than instantiating the latter with (setoid A), we reimplement
-- equation chains from scratch since then goals are printed much more
-- readably.

module ≡-Reasoning {a} {A : Set a} where

  infix  3 _∎
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_
  infix  1 begin_

  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
  begin_ x≡y = x≡y

  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
  _ ≡⟨⟩ x≡y = x≡y

  _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

  _≡˘⟨_⟩_ : ∀ (x {y z} : A) → y ≡ x → y ≡ z → x ≡ z
  _ ≡˘⟨ y≡x ⟩ y≡z = trans (sym y≡x) y≡z

  _∎ : ∀ (x : A) → x ≡ x
  _∎ _ = refl


text:
module objectOrientedGui where

open import Data.Product hiding (map)
open import Data.List
open import Data.Bool.Base
open import SizedIO.Base
open import NativeIO
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Size
open import Function

open import StateSizedIO.GUI.BaseStateDependent
open import StateSizedIO.GUI.WxBindingsFFI

data VarList : Set₁ where
  []v     :  VarList
  addVar  :  (A : Set) → Var A → VarList → VarList

prod : VarList → Set
prod  []v               =  Unit
prod  (addVar A v []v)  =  A
prod  (addVar A v l)   =  A × prod l

takeVar : (l : VarList) → NativeIO (prod l)
takeVar  []v                            = nativeReturn _
takeVar (addVar A v []v)                = nativeTakeVar {A} v
takeVar (addVar A v (addVar B v' l))   =
  nativeTakeVar {A} v       native>>= λ a →
  takeVar (addVar B v' l)   native>>= λ rest →
  nativeReturn ( a , rest )

putVar : (l : VarList) → prod l → NativeIO Unit
putVar  []v _                                     = nativeReturn _
putVar  (addVar A v []v) a                        = nativePutVar {A} v a
putVar  (addVar A v (addVar B v' l)) (a , rest)  =
  nativePutVar {A} v a          native>>= λ _ →
  putVar (addVar B v' l)  rest

data GuiLev1Command : Set where
  makeFrame   :  GuiLev1Command
  makeButton  :  Frame  →  GuiLev1Command
  addButton   :  Frame  →  Button  →  GuiLev1Command
  drawBitmap  :  DC     →  Bitmap  →  Point → Bool → GuiLev1Command
  repaint     :  Frame  →  GuiLev1Command

GuiLev1Response : GuiLev1Command → Set
GuiLev1Response  makeFrame       = Frame
GuiLev1Response (makeButton _)   = Button
GuiLev1Response  _               = Unit

GuiLev1Interface : IOInterface
Command   GuiLev1Interface  =  GuiLev1Command
Response  GuiLev1Interface  =  GuiLev1Response

GuiLev2State : Set₁
GuiLev2State = VarList

data GuiLev2Command (s :  GuiLev2State) : Set₁ where
  level1C           :  GuiLev1Command → GuiLev2Command s
  createVar         :  {A : Set} → A → GuiLev2Command s
  setButtonHandler  :  Button
                       → List (prod s → IO GuiLev1Interface ∞ (prod s))
                       → GuiLev2Command s
  setOnPaint        :  Frame
                       → List (prod s → DC → Rect → IO GuiLev1Interface ∞ (prod s))
                       → GuiLev2Command s

GuiLev2Response : (s : GuiLev2State) → GuiLev2Command s → Set
GuiLev2Response  _ (level1C c)        =  GuiLev1Response c
GuiLev2Response  _ (createVar {A} a)  =  Var A
GuiLev2Response  _  _                 =  Unit

GuiLev2Next : (s : GuiLev2State) → (c : GuiLev2Command s)
              → GuiLev2Response s c
              → GuiLev2State
GuiLev2Next s (createVar {A} a)  var  =  addVar A var s
GuiLev2Next s _                   _   =  s

GuiLev2Interface : IOInterfaceˢ
Stateˢ     GuiLev2Interface  =  GuiLev2State
Commandˢ   GuiLev2Interface  =  GuiLev2Command
Responseˢ  GuiLev2Interface  =  GuiLev2Response
nextˢ      GuiLev2Interface  =  GuiLev2Next

translateLev1Local : (c : GuiLev1Command) → NativeIO (GuiLev1Response c)
translateLev1Local  makeFrame              =  nativeMakeFrame
translateLev1Local (makeButton fra)        =  nativeMakeButton fra
translateLev1Local (addButton fra bt)      =  nativeAddButton fra bt
translateLev1Local (drawBitmap dc bm p b)  =  nativeDrawBitmap dc bm p b
translateLev1Local (repaint fra)           =  nativeRepaint fra

translateLev1 : {A : Set} → IO GuiLev1Interface ∞ A → NativeIO A
translateLev1 = translateIO translateLev1Local

translateLev1List : {A : Set} → List (IO GuiLev1Interface ∞ A) → List (NativeIO A)
translateLev1List l = map translateLev1 l

dispatch : (l : VarList) → (prod l → NativeIO (prod l)) → NativeIO Unit
dispatch l f =  takeVar l     native>>= λ a   →
                f a           native>>= λ a₁  →
                putVar l a₁

dispatchList : (l : VarList) → List (prod l → NativeIO (prod l)) → NativeIO Unit
dispatchList l []          =  nativeReturn _
dispatchList l (p ∷ rest)  =  dispatch l p         native>>= λ _ →
                              dispatchList l rest

translateLev2Local  :   (s : GuiLev2State)
                        → (c : GuiLev2Command s)
                        → NativeIO (GuiLev2Response s c)
translateLev2Local s (level1C c)        =  translateLev1Local c
translateLev2Local s (createVar {A} a)  =  nativeNewVar {A} a
translateLev2Local s (setButtonHandler bt proglist) =
  nativeSetButtonHandler bt
         (dispatchList s (map (λ prog → translateLev1 ∘ prog)  proglist))
translateLev2Local s (setOnPaint fra proglist) =
  nativeSetOnPaint fra (λ dc rect → dispatchList s
         (map (λ prog aa → translateLev1 (prog aa dc rect)) proglist))

translateLev2 : ∀ {A s} → IOˢ GuiLev2Interface ∞ (λ _ → A) s → NativeIO A
translateLev2 = translateIOˢ  translateLev2Local

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between magma-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Algebra.Core
open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core

module Algebra.Morphism.MagmaMonomorphism
  {a b ℓ₁ ℓ₂} {M₁ : RawMagma a ℓ₁} {M₂ : RawMagma b ℓ₂} {⟦_⟧}
  (isMagmaMonomorphism : IsMagmaMonomorphism M₁ M₂ ⟦_⟧)
  where

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

open import Algebra.Structures
open import Algebra.Definitions
open import Data.Product
open import Data.Sum.Base using (inj₁; inj₂)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism

------------------------------------------------------------------------
-- Properties

module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where

  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
  open SetoidReasoning setoid

  cong : Congruent₂ _≈₁_ _∙_
  cong {x} {y} {u} {v} x≈y u≈v = injective (begin
    ⟦ x ∙ u ⟧      ≈⟨  homo x u ⟩
    ⟦ x ⟧ ◦ ⟦ u ⟧  ≈⟨  ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
    ⟦ y ⟧ ◦ ⟦ v ⟧  ≈˘⟨ homo y v ⟩
    ⟦ y ∙ v ⟧      ∎)

  assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
  assoc assoc x y z = injective (begin
    ⟦ (x ∙ y) ∙ z ⟧          ≈⟨  homo (x ∙ y) z ⟩
    ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧        ≈⟨  ◦-cong (homo x y) refl ⟩
    (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧  ≈⟨  assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
    ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧)  ≈˘⟨ ◦-cong refl (homo y z) ⟩
    ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧        ≈˘⟨ homo x (y ∙ z) ⟩
    ⟦ x ∙ (y ∙ z) ⟧          ∎)

  comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
  comm comm x y = injective (begin
    ⟦ x ∙ y ⟧      ≈⟨  homo x y ⟩
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨  comm ⟦ x ⟧ ⟦ y ⟧ ⟩
    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈˘⟨ homo y x ⟩
    ⟦ y ∙ x ⟧      ∎)

  idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
  idem idem x = injective (begin
    ⟦ x ∙ x ⟧     ≈⟨ homo x x ⟩
    ⟦ x ⟧ ◦ ⟦ x ⟧ ≈⟨ idem ⟦ x ⟧ ⟩
    ⟦ x ⟧         ∎)

  sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
  sel sel x y with sel ⟦ x ⟧ ⟦ y ⟧
  ... | inj₁ x◦y≈x = inj₁ (injective (begin
    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈x ⟩
    ⟦ x ⟧          ∎))
  ... | inj₂ x◦y≈y = inj₂ (injective (begin
    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈y ⟩
    ⟦ y ⟧          ∎))

  cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
  cancelˡ cancelˡ x {y} {z} x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ (begin
    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈˘⟨ homo x y ⟩
    ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
    ⟦ x ∙ z ⟧      ≈⟨  homo x z ⟩
    ⟦ x ⟧ ◦ ⟦ z ⟧  ∎))

  cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
  cancelʳ cancelʳ {x} y z y∙x≈z∙x = injective (cancelʳ ⟦ y ⟧ ⟦ z ⟧ (begin
    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈˘⟨ homo y x ⟩
    ⟦ y ∙ x ⟧      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
    ⟦ z ∙ x ⟧      ≈⟨  homo z x ⟩
    ⟦ z ⟧ ◦ ⟦ x ⟧  ∎))

  cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_
  cancel = map cancelˡ cancelʳ

------------------------------------------------------------------------
-- Structures

isMagma : IsMagma _≈₂_ _◦_ → IsMagma _≈₁_ _∙_
isMagma isMagma = record
  { isEquivalence = RelMorphism.isEquivalence M.isEquivalence
  ; ∙-cong        = cong isMagma
  } where module M = IsMagma isMagma

isSemigroup : IsSemigroup _≈₂_ _◦_ → IsSemigroup _≈₁_ _∙_
isSemigroup isSemigroup = record
  { isMagma = isMagma S.isMagma
  ; assoc   = assoc   S.isMagma S.assoc
  } where module S = IsSemigroup isSemigroup

isBand : IsBand _≈₂_ _◦_ → IsBand _≈₁_ _∙_
isBand isBand = record
  { isSemigroup = isSemigroup B.isSemigroup
  ; idem        = idem        B.isMagma B.idem
  } where module B = IsBand isBand

isSemilattice : IsSemilattice _≈₂_ _◦_ → IsSemilattice _≈₁_ _∙_
isSemilattice isSemilattice = record
  { isBand = isBand S.isBand
  ; comm   = comm   S.isMagma S.comm
  } where module S = IsSemilattice isSemilattice

isSelectiveMagma : IsSelectiveMagma _≈₂_ _◦_ → IsSelectiveMagma _≈₁_ _∙_
isSelectiveMagma isSelMagma = record
  { isMagma = isMagma S.isMagma
  ; sel     = sel     S.isMagma S.sel
  } where module S = IsSelectiveMagma isSelMagma


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

open import Cubical.Algebra.Algebra.Base public
open import Cubical.Algebra.Algebra.Properties public

max_stars_repo_name: FernandoLarrain/cubical


text:
{- Type classes and instances for categories. -}
module CategoryTheory.Categories where

open import Relation.Binary.PropositionalEquality
            using (_≡_ ; refl ; sym ; trans ; subst ; cong) public
open import Relation.Binary using (IsEquivalence)
open import Agda.Primitive using (Level ; _⊔_ ; lzero ; lsuc) public
open import Relation.Binary.PropositionalEquality

-- Function extensionality
postulate
    ext : ∀{a b} -> Extensionality a b

-- Type class for categories.
-- Based on https://github.com/UlfNorell/category-theory-experiments
record Category (n : Level) : Set (lsuc (lsuc n)) where
    infixr 10 _~>_
    infixl 40 _≈_
    infixr 60 _∘_
    field
        -- || Data
        -- Objects
        obj  : Set (lsuc n)
        -- Arrows
        _~>_ : obj -> obj -> Set n

        -- || Operations
        -- Identity arrow
        id   : {A : obj} -> A ~> A
        -- Composition of arrows
        _∘_  : {A B C : obj} -> (B ~> C) -> (A ~> B) -> (A ~> C)
        -- Equality of arrows (as we don't have function extensionality)
        _≈_  : {A B : obj} -> (A ~> B) -> (A ~> B) -> Set n

        -- || Laws
        -- Left identity
        id-left  : {A B : obj} {f : A ~> B} -> id ∘ f ≈ f
        -- Right identity
        id-right : {A B : obj} {f : A ~> B} -> f ∘ id ≈ f
        -- Associativity of composition
        ∘-assoc  : {A B C D : obj} {f : C ~> D} {g : B ~> C} {h : A ~> B}
                -> (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
        -- Arrow equality is an equivalence relation
        ≈-equiv  : ∀{A B : obj} -> IsEquivalence (_≈_ {A} {B})
        -- Congruence of equality and composition
        ≈-cong   : ∀{A B C : obj} {f f′ : A ~> B} {g g′ : B ~> C}
                -> f ≈ f′ -> g ≈ g′ -> g ∘ f ≈ g′ ∘ f′

    -- Equational reasoning for ≈ (based on the standard library definitions)
    infix  3 _∎
    infixr 2 _≈⟨⟩_ _≈⟨_⟩_
    infix  1 begin_
    infixl 20 _[sym]
    infixr 15 _≈>_

    begin_ : ∀{A B : obj} {x y : A ~> B} → x ≈ y → x ≈ y
    begin_ x≈y = x≈y

    _≈⟨⟩_ : ∀{A B : obj} (x {y} : A ~> B) → x ≈ y → x ≈ y
    _ ≈⟨⟩ x≈y = x≈y

    _≈⟨_⟩_ : ∀{A B : obj} (x {y z} : A ~> B) → x ≈ y → y ≈ z → x ≈ z
    _ ≈⟨ x≈y ⟩ y≈z = IsEquivalence.trans ≈-equiv x≈y y≈z

    _∎ : ∀{A B : obj} (x : A ~> B) → x ≈ x
    _∎ _ = IsEquivalence.refl ≈-equiv

    r≈ : ∀{A B : obj} {x : A ~> B} → x ≈ x
    r≈ = IsEquivalence.refl ≈-equiv

    _[sym] : ∀{A B : obj} {x y : A ~> B} → x ≈ y → y ≈ x
    p [sym] = IsEquivalence.sym ≈-equiv p

    _≈>_ : ∀{A B : obj} {x y z : A ~> B} → x ≈ y → y ≈ z → x ≈ z
    p1 ≈> p2 = IsEquivalence.trans ≈-equiv p1 p2

    id-comm : {A B : obj} {f : A ~> B} -> f ∘ id ≈ id ∘ f
    id-comm = id-right ≈> id-left [sym]

    -- Derived congruence properties
    ≈-cong-left : ∀{A B C : obj} {f : A ~> B} {g g′ : B ~> C}
            -> g ≈ g′ -> g ∘ f ≈ g′ ∘ f
    ≈-cong-left e = ≈-cong r≈ e
    ≈-cong-right : ∀{A B C : obj} {g : B ~> C} {f f′ : A ~> B}
            -> f ≈ f′ -> g ∘ f ≈ g ∘ f′
    ≈-cong-right e = ≈-cong e r≈

    -- Isomorphism of two objects
    record _<~>_  (A B : obj) : Set (lsuc n) where
        field
            -- | Data
            -- Arrow in one direction
            iso~> : A ~> B
            -- Arrow in other direction
            iso<~ : B ~> A

            -- | Laws
            iso-id₁ : iso<~ ∘ iso~> ≈ id {A}
            iso-id₂ : iso~> ∘ iso<~ ≈ id {B}

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 GGT.Group.Structures
  {a b ℓ}
  where

open import Relation.Unary using (Pred)
open import Relation.Binary
open import Algebra.Bundles using (Group)
open import Level
open import GGT.Group.Definitions

record IsSubGroup (G : Group a ℓ) (P : Pred (Group.Carrier G) b) : Set (a ⊔ b ⊔ ℓ) where
  open Group G
  field
    ε∈ : (P ε)
    ∙-⁻¹-closed : IsOpInvClosed G P
    r : P Respects _≈_

  -- coset relation
  _∼_ : Rel Carrier b
  x ∼ y = P (x - y)

syntax IsSubGroup G P = P ≤ G

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
{-# OPTIONS --type-in-type #-}

module Structure where

open import Data.Nat
open import Prelude

record Struct (A : Set) : Set where
  field
    ℜ : {n : ℕ} → A ^ n → Set
    𝔉 : {n : ℕ} → A ^ n → A

max_stars_repo_name: vikraman/agda-structures

max_issues_repo_name: vikraman/agda-structures

max_forks_repo_name: vikraman/agda-structures


text:
module ctxt-types where

open import lib
open import cedille-types
open import general-util
open import syntax-util

location : Set
location = string × posinfo -- file path and starting position in the file

-- file path and starting / ending position in file
span-location = string × posinfo × posinfo

-- missing locations
missing-location : location
missing-location = ("missing" , "missing")

missing-span-location : span-location
missing-span-location = ("missing" , "missing" , "missing")

{- we will generally keep classifiers of variables in hnf in the ctxt, although
   we will not necessarily unfold recursive type definitions. -}

defScope : Set
defScope = 𝔹

localScope : defScope
localScope = tt

globalScope : defScope
globalScope = ff

defParams : Set
defParams = maybe params

data ctxt-info : Set where
  -- for defining a datatype
  datatype-def : params → kind → ctxt-info

  -- for defining a datatype constructor
  const-def : type → ctxt-info

  -- for declaring a variable to have a given type (with no definition)
  term-decl : type → ctxt-info

  -- for defining a variable to equal a term with a given type
  term-def : defParams → opacity → term → type → ctxt-info

  -- for untyped term definitions
  term-udef : defParams → opacity → term → ctxt-info

  -- for declaring a variable to have a given kind (with no definition)
  type-decl : kind → ctxt-info

  -- for defining a variable to equal a type with a given kind
  type-def : defParams → opacity → type → kind → ctxt-info

  -- for defining a variable to equal a kind
  kind-def : params → kind → ctxt-info

  -- to rename a variable at any level to another
  rename-def : var → ctxt-info

  -- representing a declaration of a variable with no other information about it
  var-decl : ctxt-info

sym-info : Set
sym-info = ctxt-info × location

-- module filename, name, parameters, and qualifying substitution
mod-info : Set
mod-info = string × string × params × qualif

-- datatypes info
datatype-info : Set
datatype-info = defDatatype

is-term-level : ctxt-info → 𝔹
is-term-level (term-decl _) = tt
is-term-level (term-def _ _ _ _) = tt
is-term-level (term-udef _ _ _) = tt
is-term-level (const-def _ ) = tt
is-term-level _ = ff

data ctxt : Set where
  mk-ctxt : (mod : mod-info) →                     -- current module
            (syms : trie (string × 𝕃 string) × trie string × trie params × trie ℕ × Σ ℕ (𝕍 string)) →    -- map each filename to its module name and the symbols declared in that file, map each module name to its filename and params, and file ID's for use in to-string.agda
            (i : trie sym-info) →                  -- map symbols (from Cedille files) to their ctxt-info and location
            (sym-occurrences : trie (𝕃 (var × posinfo × string))) →  -- map symbols to a list of definitions they occur in (and relevant file info)
            (datatypes-info : trie datatype-info) →
            ctxt

ctxt-binds-var : ctxt → var → 𝔹
ctxt-binds-var (mk-ctxt (_ , _ , _ , q) _ i _ _) x = trie-contains q x || trie-contains i x

ctxt-var-decl : var → ctxt → ctxt
ctxt-var-decl v (mk-ctxt (fn , mn , ps , q) syms i symb-occs d) =
  mk-ctxt (fn , mn , ps , (trie-insert q v (v , ArgsNil))) syms (trie-insert i v (var-decl , "missing" , "missing")) symb-occs d

ctxt-var-decl-loc : posinfo → var → ctxt → ctxt
ctxt-var-decl-loc pi v (mk-ctxt (fn , mn , ps , q) syms i symb-occs d) =
  mk-ctxt (fn , mn , ps , (trie-insert q v (v , ArgsNil))) syms (trie-insert i v (var-decl , fn , pi)) symb-occs d

qualif-var : ctxt → var → var
qualif-var (mk-ctxt (_ , _ , _ , q) _ _ _ _) v with trie-lookup q v
...| just (v' , _) = v'
...| nothing = v

start-modname : start → string
start-modname (File _ _ _ _ mn _ _ _) = mn

ctxt-get-current-filename : ctxt → string
ctxt-get-current-filename (mk-ctxt (fn , _) _ _ _ _) = fn

ctxt-get-current-mod : ctxt → mod-info
ctxt-get-current-mod (mk-ctxt m _ _ _ _) = m

ctxt-get-current-modname : ctxt → string
ctxt-get-current-modname (mk-ctxt (_ , mn , _ , _) _ _ _ _) = mn

ctxt-get-current-params : ctxt → params
ctxt-get-current-params (mk-ctxt (_ , _ , ps , _) _ _ _ _) = ps

ctxt-get-symbol-occurrences : ctxt → trie (𝕃 (var × posinfo × string))
ctxt-get-symbol-occurrences (mk-ctxt _ _ _ symb-occs _) = symb-occs

ctxt-set-symbol-occurrences : ctxt → trie (𝕃 (var × posinfo × string)) → ctxt
ctxt-set-symbol-occurrences (mk-ctxt fn syms i symb-occs d) new-symb-occs = mk-ctxt fn syms i new-symb-occs d

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

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

-- This module contains definitions allowing RWS programs to be written using
-- Agda's do-notation, as well as convenient short names for operations
-- (including lens operations).
module Dijkstra.RWS.Syntax where

open import Dijkstra.RWS
open import Dijkstra.Syntax
open import Haskell.Modules.RWS public
open import Haskell.Modules.RWS.Lens public
open import Haskell.Modules.RWS.RustAnyHow public
open import Haskell.Prelude

open import Level
  renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)
  public

private
  variable
    Ev Wr St : Set
    A B C    : Set

-- These instance declarations give us variant conditional operations that we
-- can define to play nice with `RWS-weakestPre`

instance
  RWS-MonadIfD : MonadIfD{ℓ₃ = ℓ0} (RWS Ev Wr St)
  MonadIfD.monad RWS-MonadIfD = RWS-Monad
  MonadIfD.ifD‖  RWS-MonadIfD = RWS-if

  RWS-MonadMaybeD : MonadMaybeD (RWS Ev Wr St)
  MonadMaybeD.monad  RWS-MonadMaybeD = RWS-Monad
  MonadMaybeD.maybeD RWS-MonadMaybeD = RWS-maybe

  RWS-MonadEitherD : MonadEitherD (RWS Ev Wr St)
  MonadEitherD.monad   RWS-MonadEitherD = RWS-Monad
  MonadEitherD.eitherD RWS-MonadEitherD = RWS-either

maybeM : RWS Ev Wr St B → (A → RWS Ev Wr St B) → RWS Ev Wr St (Maybe A) → RWS Ev Wr St B
maybeM mb f mma = do
  x ← mma
  caseMD x of λ where
    nothing  → mb
    (just j) → f j

maybeMP-RWS : B → (A → RWS Ev Wr St B)
              → RWS Ev Wr St (Maybe A)
              → RWS Ev Wr St B
maybeMP-RWS b f ma = do
  x ← ma
  caseMD x of λ where
    nothing  → pure b
    (just j) → f j

RWS-weakestPre-∙^∙Post : (ev : Ev) (e : C → C) → RWS-Post Wr St (Either C A) → RWS-Post Wr St (Either C A)
RWS-weakestPre-∙^∙Post ev e Post =
  RWS-weakestPre-bindPost ev (either (bail ∘ e) ok) Post


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

open import common
open import common using (_===_)
open import syntx
open import derivability
open import structuralrules
open import typingrules

{- Type theories -}

Σ₀ : Signature
Symbols Σ₀ ar = Empty

E₀ : DerivabilityStructure Σ₀
E₀ = StructuralRules Σ₀

data TypeTheory : Set
TTSig : TypeTheory → Signature
TTDer : (t : TypeTheory) → DerivabilityStructure (TTSig t)

data TypeTheory where
  ◇ : TypeTheory
  _,_ : (t : TypeTheory) {ar : SyntaxArity} (r : TypingRule (TTDer t) (args ar) (sort ar)) → TypeTheory
  _,=_ : (t : TypeTheory) {ar : SyntaxArityArgs} {k : SyntaxSort} (r : EqualityRule (TTDer t) ar k) → TypeTheory

TTSig ◇ = Σ₀
TTSig (_,_ t {ar} r) = ExtSig (TTSig t) ar
TTSig (t ,= _) = TTSig t

TTDer ◇ = E₀
TTDer (t , r) = extend (TTDer t) (TRules r)
TTDer (t ,= r) = extendE (TTDer t) (ERule r)

{- Instances to make it possible to use numeric literals to refer to symbols and typing rules -}

instance
  NumΣ₀ : Number Empty
  Number.Constraint NumΣ₀ n = Empty

  NumExtSig : {A : SyntaxArity → Set} {ar ar' : SyntaxArity} {{_ : Number (A ar')}} → Number (ExtSigSymbols A ar ar')
  Number.Constraint (NumExtSig {ar = ar} {ar'}) zero = ar === ar'
  Number.Constraint (NumExtSig {{r}}) (suc n) = Number.Constraint r n
  Number.fromNat NumExtSig zero {{refl}} = new
  Number.fromNat (NumExtSig {{r}}) (suc n) = prev (Number.fromNat r n)

instance
  NumExtT : {A : JudgmentArity → Set} {ar : SyntaxArity} {ar' : JudgmentArity} {{_ : Number (A ar')}} → Number (ExtT A ar ar')
  Number.Constraint (NumExtT {ar = ar} {ar'}) zero = TArity ar === ar'
  Number.Constraint (NumExtT {{r}}) (suc n) = Number.Constraint r n
  Number.fromNat NumExtT zero {{refl}} = typingrule
  Number.fromNat (NumExtT {{r}}) (suc n) = prev (Number.fromNat r n)

  NumExtC : {A : JudgmentArity → Set} {ar : SyntaxArity} {ar' : JudgmentArity} {{_ : Number (A ar')}} → Number (ExtC A ar ar')
  Number.Constraint (NumExtC {ar = ar} {ar'}) zero = CArity ar === ar'
  Number.Constraint (NumExtC {{r}}) (suc n) = Number.Constraint r n
  Number.fromNat NumExtC zero {{refl}} = congruencerule
  Number.fromNat (NumExtC {{r}}) (suc n) = prev (Number.fromNat r n)

  NumExtE : {A : JudgmentArity → Set} {nar ar' : JudgmentArity} {{_ : Number (A ar')}} → Number (ExtE A nar ar')
  Number.Constraint (NumExtE {nar = nar} {ar'}) zero = nar === ar'
  Number.Constraint (NumExtE {{r}}) (suc n) = Number.Constraint r n
  Number.fromNat NumExtE zero {{refl}} = equalityrule
  Number.fromNat (NumExtE {{r}}) (suc n) = prev (Number.fromNat r n)

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


text:
open import Agda.Builtin.Nat

data Bal : Nat → Nat → Nat → Set where
  leanR : ∀ {n} → Bal n (suc n) (suc n)
  leanL : ∀ {n} → Bal (suc n) n (suc n)

data Tree : Nat → Set where
  leaf : Tree 0
  node : ∀ {hˡ hʳ h} (t : Tree hʳ) (b : Bal hˡ hʳ h) → Tree (suc h)

join : ∀ {hˡ hʳ} h → Bal hˡ hʳ h → Tree (suc hˡ) → Nat
join _       leanL (node (node t b) leanR) = 0
join (suc _) leanL (node t          leanL) = 1
join _       leanR t₁                      = 2


text:
------------------------------------------------------------------------
-- Lemmas related to weak bisimilarity and CCS
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude hiding (step-→)

module Bisimilarity.Weak.CCS {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.CCS as SE
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
import Expansion.CCS as E
import Expansion.Equational-reasoning-instances
open import Labelled-transition-system.CCS Name

import Bisimilarity CCS as S
open import Bisimilarity.Weak CCS
open import Expansion CCS using (_≳_; ≳:_)
import Labelled-transition-system.Equational-reasoning-instances CCS
  as Dummy

-- An instantiation of a module with helper lemmas.

private
  module CL {i} =
    E.Cong-lemmas
      [ i ]_≈′_ right-to-left (⇒̂→[]⇒ (λ ())) ⇒→⇒̂
      map-⇒̂ map-⇒̂′ zip-⇒̂
      (λ hyp {P Q} → λ where

        (silent s done) →
            _
          , (! P      →⟨ silent s done ⟩■)
          , (! P      ∼⟨ symmetric SE.6-1-2 ⟩
             ! P ∣ P  ∼≡⟨ refl ⟩■
             ! P ∣ Q)

        (silent s (step {q = R} s′ P⟶R R⇒Q)) →
            _
          , (! P      →⟨ ⟶→⇒ s′ (replication (par-right P⟶R)) ⟩
             ! P ∣ R  →⟨ silent s (map-⇒ par-right R⇒Q) ⟩■)
          , (! P ∣ Q  ■)

        (non-silent ¬s P⇒Q) →
            _
          , (! P  →⟨ non-silent ¬s (hyp P⇒Q) ⟩■)
          , (! P ∣ Q  ■))

mutual

  -- _∣_ preserves weak bisimilarity.

  infix 6 _∣-cong_ _∣-cong′_

  _∣-cong_ : ∀ {i P P′ Q Q′} →
             [ i ] P ≈ P′ → [ i ] Q ≈ Q′ → [ i ] P ∣ Q ≈ P′ ∣ Q′
  P≈P′ ∣-cong Q≈Q′ =
    ⟨ Σ-map id (Σ-map id symmetric) ∘
      rl (symmetric P≈P′) (symmetric Q≈Q′)
    , rl P≈P′ Q≈Q′
    ⟩
    where
    rl = CL.∣-cong _∣-cong′_

  _∣-cong′_ : ∀ {i P P′ Q Q′} →
              [ i ] P ≈′ P′ → [ i ] Q ≈′ Q′ → [ i ] P ∣ Q ≈′ P′ ∣ Q′
  force (P≈P′ ∣-cong′ Q≈Q′) = force P≈P′ ∣-cong force Q≈Q′

-- _·_ preserves weak bisimilarity.

infix 12 _·-cong_ _·-cong′_

_·-cong_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≈′ force P′ → [ i ] μ · P ≈ μ′ · P′
_·-cong_ {i} refl P≈P′ =
  ⟨ Σ-map id (Σ-map id symmetric) ∘ rl (symmetric P≈P′)
  , rl P≈P′
  ⟩
  where
  rl = CL.·-cong {i = i}

_·-cong′_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≈′ force P′ → [ i ] μ · P ≈′ μ′ · P′
force (μ≡μ′ ·-cong′ P≈P′) = μ≡μ′ ·-cong P≈P′

-- _∙_ preserves weak bisimilarity.

infix 12 _∙-cong_ _∙-cong′_

_∙-cong_ : ∀ {i μ μ′ P P′} →
           μ ≡ μ′ → [ i ] P ≈ P′ → [ i ] μ ∙ P ≈ μ′ ∙ P′
refl ∙-cong P≈P′ = refl ·-cong convert {a = ℓ} P≈P′

_∙-cong′_ : ∀ {i μ μ′ P P′} →
            μ ≡ μ′ → [ i ] P ≈′ P′ → [ i ] μ ∙ P ≈′ μ′ ∙ P′
force (μ≡μ′ ∙-cong′ P≈P′) = μ≡μ′ ∙-cong force P≈P′

-- _∙ turns equal actions into weakly bisimilar processes.

infix 12 _∙-cong _∙-cong′

_∙-cong : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≈ μ′ ∙
refl ∙-cong = reflexive

_∙-cong′ : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≈′ μ′ ∙
refl ∙-cong′ = reflexive

mutual

  -- ⟨ν_⟩ preserves weak bisimilarity.

  ⟨ν_⟩-cong : ∀ {i a a′ P P′} →
              a ≡ a′ → [ i ] P ≈ P′ → [ i ] ⟨ν a ⟩ P ≈ ⟨ν a′ ⟩ P′
  ⟨ν_⟩-cong {i} {a} {P = P} {P′} refl P≈P′ =
    ⟨ Σ-map id (Σ-map id symmetric) ∘
      CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′ (symmetric P≈P′)
    , CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′ P≈P′
    ⟩

  ⟨ν_⟩-cong′ : ∀ {i a a′ P P′} →
               a ≡ a′ → [ i ] P ≈′ P′ → [ i ] ⟨ν a ⟩ P ≈′ ⟨ν a′ ⟩ P′
  force (⟨ν a≡a′ ⟩-cong′ P≈P′) = ⟨ν a≡a′ ⟩-cong (force P≈P′)

mutual

  -- !_ preserves weak bisimilarity.

  infix 10 !-cong_ !-cong′_

  !-cong_ : ∀ {i P P′} →
            [ i ] P ≈ P′ → [ i ] ! P ≈ ! P′
  !-cong_ {i} {P} {P′} P≈P′ =
    ⟨ Σ-map id (Σ-map id symmetric) ∘
      CL.!-cong _∣-cong′_ !-cong′_ (symmetric P≈P′)
    , CL.!-cong _∣-cong′_ !-cong′_ P≈P′
    ⟩

  !-cong′_ : ∀ {i P P′} → [ i ] P ≈′ P′ → [ i ] ! P ≈′ ! P′
  force (!-cong′ P≈P′) = !-cong (force P≈P′)

-- _⊕_ does not, in general, preserve weak bisimilarity in its first
-- argument (assuming that Name is inhabited).

¬⊕-congˡ : Name → ¬ (∀ {P P′ Q} → P ≈ P′ → P ⊕ Q ≈ P′ ⊕ Q)
¬⊕-congˡ x =
  (∀ {P P′ Q} → P ≈ P′ → P ⊕ Q ≈ P′ ⊕ Q)  ↝⟨ _∘ ≳⇒≈ ⟩
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)  ↝⟨ E.¬⊕-congˡ-≳≈ x ⟩□
  ⊥                                       □

-- _⊕_ does not, in general, preserve weak bisimilarity in its second
-- argument (assuming that Name is inhabited).

¬⊕-congʳ : Name → ¬ (∀ {P Q Q′} → Q ≈ Q′ → P ⊕ Q ≈ P ⊕ Q′)
¬⊕-congʳ x =
  (∀ {P Q Q′} → Q ≈ Q′ → P ⊕ Q ≈ P ⊕ Q′)  ↝⟨ _∘ ≳⇒≈ ⟩
  (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≈ P ⊕ Q′)  ↝⟨ E.¬⊕-congʳ-≳≈ x ⟩□
  ⊥                                       □

-- Some congruence lemmas for combinations of _⊕_ and _·_.

⊕·-cong :
  ∀ {i P μ Q Q′} →
  [ i ] force Q ≈′ force Q′ → [ i ] P ⊕ μ · Q ≈ P ⊕ μ · Q′
⊕·-cong {i} Q≈Q′ =
  ⟨ Σ-map id (Σ-map id symmetric) ∘ CL.⊕·-cong (symmetric Q≈Q′)
  , CL.⊕·-cong {i = i} Q≈Q′
  ⟩

⊕·-cong′ :
  ∀ {i P μ Q Q′} →
  [ i ] force Q ≈′ force Q′ → [ i ] P ⊕ μ · Q ≈′ P ⊕ μ · Q′
force (⊕·-cong′ Q≈Q′) = ⊕·-cong Q≈Q′

·⊕-cong : ∀ {i P P′ μ Q} →
          [ i ] force P ≈′ force P′ → [ i ] μ · P ⊕ Q ≈ μ · P′ ⊕ Q
·⊕-cong {P = P} {P′} {μ} {Q} P≈P′ =
  μ · P ⊕ Q   ∼⟨ SE.⊕-comm ⟩
  Q ⊕ μ · P   ∼′⟨ ⊕·-cong P≈P′ ⟩ S.∼:
  Q ⊕ μ · P′  ∼⟨ SE.⊕-comm ⟩■
  μ · P′ ⊕ Q

·⊕-cong′ :
  ∀ {i P P′ μ Q} →
  [ i ] force P ≈′ force P′ → [ i ] μ · P ⊕ Q ≈′ μ · P′ ⊕ Q
force (·⊕-cong′ P≈P′) = ·⊕-cong P≈P′

infix 8 _·⊕·-cong_ _·⊕·-cong′_

_·⊕·-cong_ :
  ∀ {i μ₁ μ₂ P₁ P₁′ P₂ P₂′} →
  [ i ] force P₁ ≈′ force P₁′ → [ i ] force P₂ ≈′ force P₂′ →
  [ i ] μ₁ · P₁ ⊕ μ₂ · P₂ ≈ μ₁ · P₁′ ⊕ μ₂ · P₂′
_·⊕·-cong_ {i} P₁≈P₁′ P₂≈P₂′ =
  ⟨ Σ-map id (Σ-map id symmetric) ∘
    CL.·⊕·-cong (symmetric P₁≈P₁′) (symmetric P₂≈P₂′)
  , CL.·⊕·-cong {i = i} P₁≈P₁′ P₂≈P₂′
  ⟩

_·⊕·-cong′_ :
  ∀ {i μ₁ μ₂ P₁ P₁′ P₂ P₂′} →
  [ i ] force P₁ ≈′ force P₁′ → [ i ] force P₂ ≈′ force P₂′ →
  [ i ] μ₁ · P₁ ⊕ μ₂ · P₂ ≈′ μ₁ · P₁′ ⊕ μ₂ · P₂′
force (P₁≈′P₁′ ·⊕·-cong′ P₂≈′P₂′) = P₁≈′P₁′ ·⊕·-cong P₂≈′P₂′

-- _[_] preserves weak bisimilarity for non-degenerate contexts. (This
-- result is similar to Theorem 6.5.25 in "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.)
--
-- TODO: This definition is very similar to E._[_]-cong. Find some way
-- to reduce the code duplication. (There was much less code
-- duplication before contexts were made coinductive.)

infix 5 _[_]-cong _[_]-cong′

_[_]-cong :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≈ Qs x) →
  [ i ] C [ Ps ] ≈ C [ Qs ]
hole     [ Ps≈Qs ]-cong = Ps≈Qs _
∅        [ Ps≈Qs ]-cong = reflexive
D₁ ∣ D₂  [ Ps≈Qs ]-cong = (D₁ [ Ps≈Qs ]-cong) ∣-cong (D₂ [ Ps≈Qs ]-cong)
action D [ Ps≈Qs ]-cong = refl ·-cong λ { .force → force D [ Ps≈Qs ]-cong }
⟨ν⟩ D    [ Ps≈Qs ]-cong = ⟨ν refl ⟩-cong (D [ Ps≈Qs ]-cong)
! D      [ Ps≈Qs ]-cong = !-cong (D [ Ps≈Qs ]-cong)
D₁ ⊕ D₂  [ Ps≈Qs ]-cong = ⊕-cong Ps≈Qs D₁ D₂
  where
  _[_]-cong′ :
    ∀ {i n Ps Qs} {C : Context ∞ n} →
    Non-degenerate′ ∞ C → (∀ x → [ i ] Ps x ≈ Qs x) →
    [ i ] C [ Ps ] ≈′ C [ Qs ]
  force (D [ Ps≈Qs ]-cong′) = force D [ Ps≈Qs ]-cong

  ⊕-cong :
    ∀ {i n Ps Qs} {C₁ C₂ : Context ∞ n} →
    (∀ x → [ i ] Ps x ≈ Qs x) →
    Non-degenerate-summand ∞ C₁ →
    Non-degenerate-summand ∞ C₂ →
    [ i ] (C₁ [ Ps ]) ⊕ (C₂ [ Ps ]) ≈ (C₁ [ Qs ]) ⊕ (C₂ [ Qs ])
  ⊕-cong {Ps = Ps} {Qs} Ps≈Qs = λ where
    (process P₁) (process P₂) →
      (context P₁ [ Ps ]) ⊕ (context P₂ [ Ps ])  ∼⟨ symmetric (SE.≡→∼ (context-[] P₁) SE.⊕-cong SE.≡→∼ (context-[] P₂)) ⟩
      P₁ ⊕ P₂                                    ∼⟨ SE.≡→∼ (context-[] P₁) SE.⊕-cong SE.≡→∼ (context-[] P₂) ⟩■
      (context P₁ [ Qs ]) ⊕ (context P₂ [ Qs ])

    (process P₁) (action {μ = μ₂} {C = C₂} D₂) →
      (context P₁ [ Ps ]) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ symmetric (SE.≡→∼ (context-[] P₁)) SE.⊕-cong (_ ■) ⟩
      P₁ ⊕ μ₂ · (C₂ [ Ps ]′)                   ∼′⟨ ⊕·-cong (D₂ [ Ps≈Qs ]-cong′) ⟩ S.∼:
      P₁ ⊕ μ₂ · (C₂ [ Qs ]′)                   ∼⟨ SE.≡→∼ (context-[] P₁) SE.⊕-cong (_ ■) ⟩■
      (context P₁ [ Qs ]) ⊕ μ₂ · (C₂ [ Qs ]′)

    (action {μ = μ₁} {C = C₁} D₁) (process P₂) →
      μ₁ · (C₁ [ Ps ]′) ⊕ (context P₂ [ Ps ])  ∼⟨ (_ ■) SE.⊕-cong symmetric (SE.≡→∼ (context-[] P₂)) ⟩
      μ₁ · (C₁ [ Ps ]′) ⊕ P₂                   ∼′⟨ ·⊕-cong (D₁ [ Ps≈Qs ]-cong′) ⟩ S.∼:
      μ₁ · (C₁ [ Qs ]′) ⊕ P₂                   ∼⟨ (_ ■) SE.⊕-cong SE.≡→∼ (context-[] P₂) ⟩■
      μ₁ · (C₁ [ Qs ]′) ⊕ (context P₂ [ Qs ])

    (action {μ = μ₁} {C = C₁} D₁) (action {μ = μ₂} {C = C₂} D₂) →
      μ₁ · (C₁ [ Ps ]′) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ (D₁ [ Ps≈Qs ]-cong′) ·⊕·-cong (D₂ [ Ps≈Qs ]-cong′) ⟩■
      μ₁ · (C₁ [ Qs ]′) ⊕ μ₂ · (C₂ [ Qs ]′)

_[_]-cong′ :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≈′ Qs x) →
  [ i ] C [ Ps ] ≈′ C [ Qs ]
force (C [ Ps≈Qs ]-cong′) = C [ (λ x → force (Ps≈Qs x)) ]-cong

-- A variant of _[_]-cong for weakly guarded contexts.
--
-- Note that the input uses the primed variant of weak bisimilarity.
--
-- I got the idea for this lemma from Lemma 23 in Schäfer and Smolka's
-- "Tower Induction and Up-to Techniques for CCS with Fixed Points".

[]-cong-w :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Weakly-guarded C → Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≈′ Qs x) →
  [ i ] C [ Ps ] ≈ C [ Qs ]
[]-cong-w ()        hole
[]-cong-w _         ∅          Ps≈Qs = reflexive
[]-cong-w (W₁ ∣ W₂) (D₁ ∣ D₂)  Ps≈Qs = []-cong-w W₁ D₁ Ps≈Qs ∣-cong
                                       []-cong-w W₂ D₂ Ps≈Qs
[]-cong-w action    (action D) Ps≈Qs = refl ·-cong
                                         (force D [ Ps≈Qs ]-cong′)
[]-cong-w (⟨ν⟩ W)   (⟨ν⟩ D)    Ps≈Qs = ⟨ν refl ⟩-cong
                                         ([]-cong-w W D Ps≈Qs)
[]-cong-w (! W)     (! D)      Ps≈Qs = !-cong []-cong-w W D Ps≈Qs
[]-cong-w {Ps = Ps} {Qs}
          (W₁ ⊕ W₂) (D₁ ⊕ D₂)  Ps≈Qs = case D₁ ,′ D₂ of λ where
  (process P₁ , process P₂) →
    (context P₁ [ Ps ]) ⊕ (context P₂ [ Ps ])  ∼⟨ symmetric (SE.≡→∼ (context-[] P₁) SE.⊕-cong SE.≡→∼ (context-[] P₂)) ⟩
    P₁ ⊕ P₂                                    ∼⟨ SE.≡→∼ (context-[] P₁) SE.⊕-cong SE.≡→∼ (context-[] P₂) ⟩■
    (context P₁ [ Qs ]) ⊕ (context P₂ [ Qs ])

  (process P₁ , action {μ = μ₂} {C = C₂} D₂) →
    (context P₁ [ Ps ]) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ symmetric (SE.≡→∼ (context-[] P₁)) SE.⊕-cong (_ ■) ⟩
    P₁ ⊕ μ₂ · (C₂ [ Ps ]′)                   ∼′⟨ ⊕·-cong (force D₂ [ Ps≈Qs ]-cong′) ⟩ S.∼:
    P₁ ⊕ μ₂ · (C₂ [ Qs ]′)                   ∼⟨ SE.≡→∼ (context-[] P₁) SE.⊕-cong (_ ■) ⟩■
    (context P₁ [ Qs ]) ⊕ μ₂ · (C₂ [ Qs ]′)

  (action {μ = μ₁} {C = C₁} D₁ , process P₂) →
    μ₁ · (C₁ [ Ps ]′) ⊕ (context P₂ [ Ps ])  ∼⟨ (_ ■) SE.⊕-cong symmetric (SE.≡→∼ (context-[] P₂)) ⟩
    μ₁ · (C₁ [ Ps ]′) ⊕ P₂                   ∼′⟨ ·⊕-cong (force D₁ [ Ps≈Qs ]-cong′) ⟩ S.∼:
    μ₁ · (C₁ [ Qs ]′) ⊕ P₂                   ∼⟨ (_ ■) SE.⊕-cong SE.≡→∼ (context-[] P₂) ⟩■
    μ₁ · (C₁ [ Qs ]′) ⊕ (context P₂ [ Qs ])

  (action {μ = μ₁} {C = C₁} D₁ , action {μ = μ₂} {C = C₂} D₂) →
    μ₁ · (C₁ [ Ps ]′) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ (force D₁ [ Ps≈Qs ]-cong′) ·⊕·-cong (force D₂ [ Ps≈Qs ]-cong′) ⟩■
    μ₁ · (C₁ [ Qs ]′) ⊕ μ₂ · (C₂ [ Qs ]′)

-- A generalisation to systems of inequations of the following
-- property: If two processes satisfy the same equation X ≳ C [ X ],
-- for a weakly guarded, non-degenerate context C, then the two
-- processes are weakly bisimilar (assuming extensionality).
--
-- This result is a variant of Bisimilarity.CCS.unique-solutions.
-- Proposition 4.4.4 in Milner's "Operational and Algebraic Semantics
-- of Concurrent Processes" is perhaps more useful in practice, as
-- well as some of the results in Sangiorgi's "Equations,
-- Contractions, and Unique Solutions".

module _ (ext : Proc-extensionality) where

  mutual

    unique-solutions :
      ∀ {i n} {Ps Qs : Fin n → Proc ∞} {C : Fin n → Context ∞ n} →
      (∀ x → Weakly-guarded (C x)) →
      (∀ x → Non-degenerate ∞ (C x)) →
      (∀ x → Ps x ≳ C x [ Ps ]) →
      (∀ x → Qs x ≳ C x [ Qs ]) →
      ∀ x → [ i ] Ps x ≈ Qs x
    unique-solutions {i} {Ps = Ps} {Qs} {C} w nd ≳C[Ps] ≳C[Qs] x =
      Ps x        ∼⟨ ≳C[Ps] x ⟩
      C x [ Ps ]  ∼′⟨ ≈: ⟨ lr ≳C[Ps] ≳C[Qs] , Σ-map id (Σ-map id symmetric) ∘ lr ≳C[Qs] ≳C[Ps] ⟩ ⟩ ≳:
      C x [ Qs ]  ∽⟨ ≳C[Qs] x ⟩■
      Qs x
      where
      lr :
        ∀ {Ps Qs μ P} →
        (∀ x → Ps x ≳ C x [ Ps ]) →
        (∀ x → Qs x ≳ C x [ Qs ]) →
        C x [ Ps ] [ μ ]⟶ P →
        ∃ λ Q → C x [ Qs ] [ μ ]⇒̂ Q × [ i ] P ≈′ Q
      lr {Ps} {Qs} {μ} ≳C[Ps] ≳C[Qs] ⟶P =
        case 6-2-15-nd ext (C x) (w x) (nd x) ⟶P of λ where
          (C′ , nd′ , refl , trs) →
              _
            , (C x [ Qs ]  →⟨ trs Qs ⟩■
               C′ [ Qs ])
            , (C′ [ Ps ]  ∼⟨ nd′ [ unique-solutions′ w nd ≳C[Ps] ≳C[Qs] ]-cong′ ⟩■
               C′ [ Qs ])

    unique-solutions′ :
      ∀ {i n} {Ps Qs : Fin n → Proc ∞} {C : Fin n → Context ∞ n} →
      (∀ x → Weakly-guarded (C x)) →
      (∀ x → Non-degenerate ∞ (C x)) →
      (∀ x → Ps x ≳ C x [ Ps ]) →
      (∀ x → Qs x ≳ C x [ Qs ]) →
      ∀ x → [ i ] Ps x ≈′ Qs x
    force (unique-solutions′ w nd ≳C[Ps] ≳C[Qs] x) =
      unique-solutions w nd ≳C[Ps] ≳C[Qs] x

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

module sets.empty where

open import level

data ⊥ {i} : Set i where

⊥-elim : ∀ {i j}{A : Set j} → ⊥ {i} → A
⊥-elim ()

¬_ : ∀ {i} → Set i → Set i
¬ X = X → ⊥ {lzero}
infix 3 ¬_

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --type-in-type #-}
module chu.lens where
open import prelude
open import functors
open import chu
open import poly.core

→∫ : Chu → ∫
→∫ (A⁺ , A⁻ ! Ω) = A⁺ , λ a⁺ → ∃ (Ω a⁺)

→Lens : {A B : Chu} → Chu[ A , B ] → ∫[ →∫ A , →∫ B ]
→Lens (f ↔ fᵗ ! †)  a⁺ = f a⁺ , λ (b⁻ , fa⁺Ωb⁻) → fᵗ b⁻ , subst id († a⁺ b⁻) fa⁺Ωb⁻

module _ {A B C : Chu}
         (F@(f ↔ fᵗ ! _†₁_) : Chu[ A , B ])
         (G@(g ↔ gᵗ ! _†₂_) : Chu[ B , C ]) where

    comp₂ : ∀ a⁺ → π₂  (→Lens (F ▸       G) a⁺)
                 ≡ π₂ ((→Lens  F ▸ →Lens G) a⁺)
    comp₂ a⁺ = extensionality λ ( c⁻ , gfaΩc ) → (λ x → (fᵗ ∘ gᵗ) c⁻ , x) ⟨$⟩
               subst⋯ id (f a⁺ †₂ c⁻) (a⁺ †₁ gᵗ c⁻) gfaΩc

    comp∀ : ∀ a⁺ → →Lens (F ▸ G) a⁺ ≡ (→Lens F ▸ →Lens G) a⁺
    comp∀ a⁺ rewrite comp₂ a⁺ = refl

instance
    open Chu[_,_]
    chu-lens-functor : Functor →∫
    chu-lens-functor = φ: →Lens
                       𝒾: refl
                       ▸: λ F G → extensionality (comp∀ F G)

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

data AB : Set where
  A B : AB

foo : Nat → AB → AB
foo 0       t = A
foo (suc n) t = foo n A -- NB tail-recursive

test : foo 100000 A ≡ A
test = refl -- memory blows up here

data N : Set where
  z : N
  s : N → N

produce : Nat → AB → N
produce 0       t = z
produce (suc n) t = s (produce n A)

consume : N → AB → AB
consume z     t = t
consume (s n) t = consume n A

test₁ : consume (produce 100000 B) A ≡ A
test₁ = refl