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

  The main definitions of this module are:

    * explore⊎
    * explore⊎-ind
    * ⟦explore⊎⟧
    * Σᵉ⊎-ok
    * Πᵉ⊎-ok

-}
open import Type hiding (★)
open import Function.NP
open import Function.Extensionality
open import Data.Nat using (_+_)
open import Level.NP
open import Type.Identities
open import Data.Product.NP
open import Data.Sum using (_⊎_) renaming (inj₁ to inl; inj₂ to inr; [_,_] to [inl:_,inr:_])
open import Data.Sum.Logical
open import HoTT
open import Data.Fin using (Fin)
open import Relation.Binary.Logical
open import Relation.Binary.Sum
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_ ; module ≡-Reasoning; cong; !_; _∙_; refl; ap)

open import Explore.Core
open import Explore.Properties
open import Explore.Explorable

module Explore.Sum where

module _ {a b u} {A : ★ a} {B : ★ b} {U : ★ u}
         (_∙_ : U → U → U)
         (e₁  : (A → U) → U)
         (e₂  : (B → U) → U)
         (f   : (A ⊎ B) → U)
  where
      -- find a better place/name for it
      ⊎ᶜ : U
      ⊎ᶜ = e₁ (f ∘ inl) ∙ e₂ (f ∘ inr)

module _ {ℓ a b} {A : ★ a} {B : ★ b} where
    explore⊎ : Explore ℓ A → Explore ℓ B → Explore ℓ (A ⊎ B)
    explore⊎ exploreᴬ exploreᴮ ε _∙_ = ⊎ᶜ _∙_ (exploreᴬ ε _∙_) (exploreᴮ ε _∙_)

    module _ {p} {eᴬ : Explore ℓ A} {eᴮ : Explore ℓ B} where
        explore⊎-ind : ExploreInd p eᴬ → ExploreInd p eᴮ → ExploreInd p (explore⊎ eᴬ eᴮ)
        explore⊎-ind Psᴬ Psᴮ P Pε P∙ Pf
        -- TODO clean this up:
          = P∙ (Psᴬ (λ s → P (λ _ _ f → s _ _ (f ∘ inl))) Pε P∙ (Pf ∘ inl))
               (Psᴮ (λ s → P (λ _ _ f → s _ _ (f ∘ inr))) Pε P∙ (Pf ∘ inr))

module _ {ℓ₀ ℓ₁ ℓᵣ}
         {A₀ A₁} {Aᵣ : ⟦★₀⟧ A₀ A₁}
         {B₀ B₁} {Bᵣ : ⟦★₀⟧ B₀ B₁}
         {eᴬ₀ : Explore ℓ₀ A₀} {eᴬ₁ : Explore ℓ₁ A₁}(eᴬᵣ : ⟦Explore⟧ ℓᵣ Aᵣ eᴬ₀ eᴬ₁)
         {eᴮ₀ : Explore ℓ₀ B₀} {eᴮ₁ : Explore ℓ₁ B₁}(eᴮᵣ : ⟦Explore⟧ ℓᵣ Bᵣ eᴮ₀ eᴮ₁)
         where
    ⟦explore⊎⟧ : ⟦Explore⟧ ℓᵣ (Aᵣ ⟦⊎⟧ Bᵣ) (explore⊎ eᴬ₀ eᴮ₀) (explore⊎ eᴬ₁ eᴮ₁)
    ⟦explore⊎⟧ P Pε P∙ Pf
       = P∙ (eᴬᵣ P Pε P∙ (Pf ∘ ⟦inl⟧))
            (eᴮᵣ P Pε P∙ (Pf ∘ ⟦inr⟧))

module _ {ℓ₀ ℓ₁ ℓᵣ} {A B : ★₀}
         {eᴬ₀ : Explore ℓ₀ A}{eᴬ₁ : Explore ℓ₁ A}(eᴬᵣ : ⟦Explore⟧ ℓᵣ _≡_ eᴬ₀ eᴬ₁)
         {eᴮ₀ : Explore ℓ₀ B}{eᴮ₁ : Explore ℓ₁ B}(eᴮᵣ : ⟦Explore⟧ ℓᵣ _≡_ eᴮ₀ eᴮ₁)
         where
    ⟦explore⊎⟧≡ : ⟦Explore⟧ ℓᵣ _≡_ (explore⊎ eᴬ₀ eᴮ₀) (explore⊎ eᴬ₁ eᴮ₁)
    ⟦explore⊎⟧≡ P Pε P∙ Pf
       = P∙ (eᴬᵣ P Pε P∙ (Pf ∘ ap inl))
            (eᴮᵣ P Pε P∙ (Pf ∘ ap inr))

infixr 4 _⊎ᵉ_ _⊎ⁱ_
_⊎ᵉ_ = explore⊎
_⊎ⁱ_ = explore⊎-ind

module _ {a b} {A : ★ a} {B : ★ b} where
    infixr 4 _⊎ˢ_
    _⊎ˢ_ : Sum A → Sum B → Sum (A ⊎ B)
    _⊎ˢ_ = ⊎ᶜ _+_

module _ {A : ★₀} {B : ★₀} {sumᴬ : Sum A} {sumᴮ : Sum B}{{_ : UA}} where
    open Adequacy _≡_

    adequate-sum⊎ : Adequate-sum sumᴬ → Adequate-sum sumᴮ → Adequate-sum (sumᴬ ⊎ˢ sumᴮ)
    adequate-sum⊎ asumᴬ asumᴮ f    = (Fin (sumᴬ (f ∘ inl) + sumᴮ (f ∘ inr)))
                                   ≡⟨ ! Fin-⊎-+ ⟩
                                     (Fin (sumᴬ (f ∘ inl)) ⊎ Fin (sumᴮ (f ∘ inr)))
                                   ≡⟨ ⊎= (asumᴬ (f ∘ inl)) (asumᴮ (f ∘ inr)) ⟩
                                     (Σ A (Fin ∘ f ∘ inl) ⊎ Σ B (Fin ∘ f ∘ inr))
                                   ≡⟨ ! dist-⊎-Σ ⟩
                                     Σ (A ⊎ B) (Fin ∘ f)
                                   ∎
      where open ≡-Reasoning

    _⊎ᵃ_ = adequate-sum⊎

module _ {ℓ} {a b} {A : ★ a} {B : ★ b} {eᴬ : Explore (ₛ ℓ) A} {eᴮ : Explore (ₛ ℓ) B} where
  private
    eᴬ⁺ᴮ = eᴬ ⊎ᵉ eᴮ

  focus⊎ : Focus eᴬ → Focus eᴮ → Focus eᴬ⁺ᴮ
  focus⊎ fᴬ fᴮ (inl x , y) = inl (fᴬ (x , y))
  focus⊎ fᴬ fᴮ (inr x , y) = inr (fᴮ (x , y))

  unfocus⊎ : Unfocus eᴬ → Unfocus eᴮ → Unfocus eᴬ⁺ᴮ
  unfocus⊎ fᴬ fᴮ (inl x) = first inl (fᴬ x)
  unfocus⊎ fᴬ fᴮ (inr y) = first inr (fᴮ y)

module _ {ℓ} {A : ★₀} {B : ★₀} {eᴬ : Explore (ₛ ℓ) A} {eᴮ : Explore (ₛ ℓ) B} where
  private
    eᴬ⁺ᴮ = eᴬ ⊎ᵉ eᴮ

  Σᵉ⊎-ok : {{_ : UA}} → Adequate-Σ (Σᵉ eᴬ) → Adequate-Σ (Σᵉ eᴮ) → Adequate-Σ (Σᵉ eᴬ⁺ᴮ)
  Σᵉ⊎-ok fᴬ fᴮ _ = ⊎= (fᴬ _) (fᴮ _) ∙ ! dist-⊎-Σ

  lookup⊎ : Lookup eᴬ → Lookup eᴮ → Lookup (eᴬ ⊎ᵉ eᴮ)
  lookup⊎ lookupᴬ lookupᴮ (x , y) = [inl: lookupᴬ x ,inr: lookupᴮ y ]

  reify⊎ : Reify eᴬ → Reify eᴮ → Reify (eᴬ ⊎ᵉ eᴮ)
  reify⊎ reifyᴬ reifyᴮ f = (reifyᴬ (f ∘ inl)) , (reifyᴮ (f ∘ inr))

  Πᵉ⊎-ok : {{_ : UA}}{{_ : FunExt}} → Adequate-Π (Πᵉ eᴬ) → Adequate-Π (Πᵉ eᴮ) → Adequate-Π (Πᵉ eᴬ⁺ᴮ)
  Πᵉ⊎-ok fᴬ fᴮ _ = ×= (fᴬ _) (fᴮ _) ∙ ! dist-×-Π

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

ext: agda

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import Data.Nat    using (ℕ; _+_) renaming (_≤?_ to _≤?ₙ_)
open import Data.Bool   using (Bool; true; false; not; _∧_)
open import Data.String using (String)
open import Data.Sum    using (_⊎_; [_,_]; inj₁; inj₂)
open import Relation.Binary using (Decidable)
open import Relation.Nullary           using (yes; no; ¬_)
open import Relation.Nullary.Negation  using (contradiction)
open import Data.List                  using (List; []; _∷_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.Empty                 using (⊥-elim)
open import Data.Product               using (_×_; -,_; _-,-_; ∃; ∃-syntax) renaming (_,_ to _,,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Level using (Level; suc; _⊔_)
open import Agda.Builtin.Sigma hiding (_,_) -- renaming (_,_ to _,,_)
open import Data.Maybe using (Maybe; just; nothing; Is-just)
import Relation.Binary.PropositionalEquality as Eq

open import IMP hiding (com; state) ---using (aexp; aval; bexp; bval)

postulate
  _≟_ : Decidable {A = ℕ} _≡_

addr = ℕ

heap = addr → Maybe val

store = vname → val

state = store × heap

assn : ∀{l} → Set (suc l)
assn {a} = store → heap → Set a

emp : assn
emp _ h = ∀ a → h a ≡ nothing

_⊢>_ : IMP.aexp → IMP.aexp → assn
_⊢>_ a a′ s h = h (aval a s) ≡ just (aval a′ s)
              × ∀ (a″) → ¬(a″ ≡ aval a s) → h a″ ≡ nothing

_⊆_ : heap → heap → Set
h₀ ⊆ h = ∀ a → (h a ≡ nothing → h₀ a ≡ nothing)
             × (∀{o} → h₀ a ≡ just o → h₀ a ≡ h a)

heap-union : heap → heap → heap → addr → Set
heap-union h h₁ h₂ a with h a
... | just o = (h₁ a ≡ just o  × h₂ a ≡ nothing)
             ⊎ (h₁ a ≡ nothing × h₂ a ≡ just o)
... | nothing = h₁ a ≡ nothing × h₂ a ≡ nothing

_∼_⊥_ :  heap → heap → heap → Set
h ∼ h₁ ⊥ h₂ = ∀ a → heap-union h h₁ h₂ a

union-subset : ∀ h {h₁ h₂}
  → h ∼ h₁ ⊥ h₂
  → h₁ ⊆ h
union-subset h x a with h a  | x a
union-subset h x a | just x₁ | inj₁ (fst₁ ,, snd₁) = (λ ()) ,, (λ {x} x₁ → fst₁)
union-subset h x a | just x₁ | inj₂ (fst₁ ,, snd₁) rewrite fst₁ = (λ _ → refl) ,, (λ {x} ())
union-subset h x a | nothing | fst₁ ,, snd₁ = (λ x → fst₁) ,, (λ {x} x₁ → fst₁)

_*_ : ∀{l} → assn {l} → assn {l} → assn {l}
_*_ P Q s h = ∃[ h₁ ] ∃[ h₂ ] ((h ∼ h₁ ⊥ h₂)
                              × P s h₁
                              × Q s h₂)

_dom_ : addr → heap → Set
a dom h = ∃[ v ] (h a ≡ just v)

_¬dom_ : addr → heap → Set
a ¬dom h = h a ≡ nothing

_[_::=ₕ_] : heap → addr → val → heap
(h [ X ::=ₕ n ]) Y with Y ≟ X
... | yes _ = just n
... | no  _ = h Y

_/[_] : heap → addr → heap
(h /[ X ]) Y with Y ≟ X
... | yes _ = nothing
... | no  _ = h Y

data com : Set where
  SKIP  : com
  _::=_ : String → aexp → com
  _::_  : com  → com  → com
  IF_THEN_ELSE_ : bexp → com  → com  → com
  WHILE_DO_     : bexp → com  → com
  _::=cons_     : String → addr → com
  _::=[_]  : String → aexp → com
  [_]::=_  : aexp → aexp → com
  dispose_ : aexp → com

data ⊢[_]_[_] {l} : assn {l} → com → assn {l} → Set (suc l) where
  Skip : ∀{P}
    → ⊢[ P ] SKIP [ P ]
  Loc : ∀{Q a x}
    → ⊢[ (λ s → Q (s [ x ::= aval a s ])) ] (x ::= a) [ Q ]
  Comp : ∀{P Q R c₁ c₂}
    → ⊢[ P ] c₁ [ Q ]
    → ⊢[ Q ] c₂ [ R ]
    → ⊢[ P ] c₁ :: c₂ [ R ]
  If : ∀{P b c₁ Q c₂}
    → ⊢[ (λ s h → P s h × bval b s ≡ true)  ] c₁ [ Q ]
    → ⊢[ (λ s h → P s h × bval b s ≡ false) ] c₂ [ Q ]
    → ⊢[ P ] (IF b THEN c₁ ELSE c₂) [ Q ]
  While : ∀{P b c}
    → ⊢[ (λ s h → P s h × bval b s ≡ true) ] c [ P ]
    → ⊢[ P ] (WHILE b DO c) [ (λ s h → P s h × bval b s ≡ false) ]
  Conseq : ∀{P Q P′ Q′ : assn} {c}
    → (∀ s h → P′ s h → P s h)
    → ⊢[ P  ] c [ Q  ]
    → (∀ s h → Q s h → Q′ s h)
    → ⊢[ P′ ] c [ Q′ ]
  Frame : ∀{A B R c}
    → ⊢[ A     ] c [ B     ]
    → ⊢[ A * R ] c [ B * R ]

data config : Set where
  ⦅_,_,_⦆ : com → store → heap → config
  abort  : config

data _⇒_ : config → config → Set where
  Loc : ∀{x a s h}
      → ⦅ x ::= a , s , h ⦆ ⇒ ⦅ SKIP , (s [ x ::= aval a s ]) , h ⦆
  Comp₁ : ∀{c s h}
      → ⦅ SKIP :: c , s , h ⦆ ⇒ ⦅ c , s , h ⦆
  Comp₂ : ∀{c₁ c₁′ c₂ s s′ h h′}
      → ⦅ c₁       , s , h ⦆ ⇒ ⦅ c₁′       , s′ , h′ ⦆
      → ⦅ c₁ :: c₂ , s , h ⦆ ⇒ ⦅ c₁′ :: c₂ , s′ , h′  ⦆
  CompFail : ∀{c₁ c₂ s h}
      → ⦅ c₁       , s , h ⦆ ⇒ abort
      → ⦅ c₁ :: c₂ , s , h ⦆ ⇒ abort
  IfTrue  : ∀{b s c₁ c₂ h}
      → bval b s ≡ true
      → ⦅ IF b THEN c₁ ELSE c₂ , s , h ⦆ ⇒ ⦅ c₁ , s , h ⦆
  IfFalse : ∀{b s c₁ c₂ h}
      → bval b s ≡ false
      → ⦅ IF b THEN c₁ ELSE c₂ , s , h ⦆ ⇒ ⦅ c₂ , s , h ⦆
  While : ∀{b s c h}
      → ⦅ WHILE b DO c , s , h ⦆ ⇒ ⦅ IF b THEN (c :: (WHILE b DO c)) ELSE SKIP , s , h ⦆
  Cons : ∀{l h s x h′ s′}
      → l ¬dom h
      → h′ ≡ h [ l ::=ₕ 0 ]
      → s′ ≡ s [ x ::= l  ]
      → ⦅ x ::=cons l , s , h ⦆ ⇒ ⦅ SKIP , s′ , h′ ⦆
  Lookup : ∀{a s x h v s′}
      → (aval a s) dom h
      → s′ ≡ s [ x ::= v ]
      → ⦅ x ::=[ a ] , s , h ⦆ ⇒ ⦅ SKIP , s′ , h  ⦆
  LookupFail : ∀{a s x h}
      → (aval a s) ¬dom h
      → ⦅ x ::=[ a ] , s , h ⦆ ⇒ abort
  Write : ∀{a s a′ h}
      → (aval a s) dom h
      → ⦅ [ a ]::= a′ , s , h ⦆ ⇒ ⦅ SKIP , s , h [ aval a s ::=ₕ aval a′ s ]  ⦆
  WriteFail : ∀{a s a′ x h}
      → (aval a s) ¬dom h
      → ⦅ [ x ]::= a′ , s , h ⦆ ⇒ abort
  Dispose : ∀{a s h}
      → (aval a s) dom h
      → ⦅ dispose a , s , h ⦆ ⇒ ⦅ SKIP , s , h /[ aval a s ]  ⦆
  DisposeFail : ∀{a s h}
      → (aval a s) ¬dom h
      → ⦅ dispose a , s , h ⦆ ⇒ abort

data _⇒*_ : config → config → Set where
  _∎ : ∀ c → c ⇒* c
  _→⟨_⟩_ : ∀ c {c′ c″}
         → c  ⇒  c′
         → c′ ⇒* c″
         → c  ⇒* c″

Safe : config → Set
Safe c = ¬ (c ⇒* abort)

lemma1 : ∀{c s h₀ h}
       → h₀ ⊆ h
       → ⦅ c , s , h  ⦆ ⇒ abort
       → ⦅ c , s , h₀ ⦆ ⇒ abort
lemma1 sub (CompFail r) = CompFail (lemma1 sub r)
lemma1 sub (LookupFail {a}{s} r) = LookupFail (fst (sub (aval a s)) r)
lemma1 sub (WriteFail {a}{s} r) = WriteFail {a} (fst (sub (aval a s)) r)
lemma1 sub (DisposeFail {a}{s} r) = DisposeFail (fst (sub (aval a s)) r)

subset-update : ∀ l {h h₀ v}
  →  h₀ ⊆ h
  → (h₀ [ l ::=ₕ v ]) ⊆ (h [ l ::=ₕ v ])
subset-update l b Y with Y ≟ l
... | yes p = (λ x → x) ,, λ {o} _ → refl
... | no ¬p = b Y

subset-delete : ∀ v {h h₀}
  →  h₀ ⊆ h
  → (h₀ /[ v ]) ⊆ (h /[ v ])
subset-delete l b Y with Y ≟ l
... | yes p = (λ x → refl) ,, (λ {x} x₁ → refl)
... | no ¬p = b Y

lemma2 : ∀ h₀ {h c c′ s s′ h′}
       → h₀ ⊆ h
       → ⦅ c , s , h  ⦆ ⇒ ⦅ c′ , s′ , h′ ⦆
       → ⦅ c , s , h₀ ⦆ ⇒ abort
       ⊎ (∃[ h′₀ ] (h′₀ ⊆ h′
       × ⦅ c , s , h₀ ⦆ ⇒ ⦅ c′ , s′ , h′₀ ⦆))
lemma2 h₀ x Loc = inj₂ (h₀ ,, x ,, Loc)
lemma2 h₀ x Comp₁ = inj₂ (h₀ ,, x ,, Comp₁)
lemma2 h₀ x (Comp₂ x₁) with lemma2 h₀ x x₁
lemma2 h₀ x (Comp₂ x₁) | inj₁ x₂ = inj₁ (CompFail x₂)
lemma2 h₀ x (Comp₂ x₁) | inj₂ (h′₀ ,, sub ,, red) = inj₂ (h′₀ ,, sub ,, Comp₂ red)
lemma2 h₀ x (IfTrue x₁) = inj₂ (h₀ ,, x ,, IfTrue x₁)
lemma2 h₀ x (IfFalse x₁)  = inj₂ (h₀ ,, x ,, IfFalse x₁)
lemma2 h₀ x While         = inj₂ (h₀ ,, x ,, While)
lemma2 h₀ x (Cons {l} x₁ A B) rewrite A | B = inj₂ ( (h₀ [ l ::=ₕ 0 ])
                                            ,, subset-update l x
                                            ,, Cons (fst (x l) x₁) refl refl)
lemma2 h₀ x (Lookup {a}{s} (_ ,, p) A) rewrite A with h₀ (aval a s) | Eq.inspect h₀ (aval a s)
... | nothing | Eq.[ eq ] = inj₁ (LookupFail eq)
... | just o  | Eq.[ eq ] = inj₂ ( h₀
                                ,, x
                                ,, Lookup (-, Eq.trans (snd (x (aval a s)) eq) p) refl)
lemma2 h₀ x (Write {a}{s}{a′} (_ ,, x₁)) with h₀ (aval a s) | Eq.inspect h₀ (aval a s)
... | nothing | Eq.[ eq ] = inj₁ (WriteFail {a} eq)
... | just o  | Eq.[ eq ] = inj₂ ( (h₀ [ aval a s ::=ₕ aval a′ s ])
                                ,, subset-update (aval a s) x
                                ,, Write (-, (Eq.trans (snd (x (aval a s)) eq) x₁)))
lemma2 h₀ x (Dispose {a}{s} (_ ,, x₁)) with h₀ (aval a s) | Eq.inspect h₀ (aval a s)
... | nothing | Eq.[ eq ] = inj₁ (DisposeFail eq)
... | just o  | Eq.[ eq ] = inj₂ ( (h₀ /[ aval a s ])
                                ,, subset-delete (aval a s) x
                                ,, Dispose (-, (Eq.trans (snd (x (aval a s)) eq) x₁)))

frame1sub : ∀{c s h H}
  → h ⊆ H
  → Safe ⦅ c , s , h ⦆
  → Safe ⦅ c , s , H ⦆
frame1sub {c}{s}{h}{H} x x₁ (_→⟨_⟩_ .(⦅ c , s , H ⦆) {⦅ x₄ , x₅ , x₆ ⦆} x₂ x₃) with lemma2 h x x₂
... | inj₁ x₇ = x₁ (⦅ c , s , h ⦆ →⟨ x₇ ⟩ (abort ∎))
... | inj₂ (_ ,, fst₂ ,, snd₁) = frame1sub fst₂ (λ z → x₁ (_ →⟨ snd₁ ⟩ z)) x₃
frame1sub {c}{s}{h}{H} x x₁ (_→⟨_⟩_ .(⦅ c , s , H ⦆) {abort} x₂ x₃) = x₁ (_ →⟨ lemma1 x x₂ ⟩ (abort ∎))

frame1 : ∀{c s h H z}
  → H ∼ h ⊥ z
  → Safe ⦅ c , s , h ⦆
  → Safe ⦅ c , s , H ⦆
frame1 {H = H} x x₁ x₂ = frame1sub (union-subset H x) x₁ x₂

heap-union-update : ∀{l h h₀ h₁ v}
  → l ¬dom h₁
  →  h               ∼  h₀               ⊥ h₁
  → (h [ l ::=ₕ v ]) ∼ (h₀ [ l ::=ₕ v ]) ⊥ h₁
heap-union-update {l}{h}{v = v} d x a with (h [ l ::=ₕ v ]) a | Eq.inspect (h [ l ::=ₕ v ]) a
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] with a ≟ l | h a | Eq.inspect h a | x a
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] | yes p | just x₂ | Eq.[ eq2 ] | inj₁ x₃ = inj₁ (eq ,, snd x₃)
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] | yes p | just x₂ | Eq.[ eq2 ] | inj₂ y rewrite p = inj₁ (eq ,, d)
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] | yes p | nothing | Eq.[ eq2 ] | C = inj₁ (eq ,, snd C)
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] | no ¬p | just x₂ | Eq.[ eq2 ] | inj₁ x₃ rewrite (Eq.trans (sym eq) eq2) = inj₁ x₃
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] | no ¬p | just x₂ | Eq.[ eq2 ] | inj₂ y  rewrite (Eq.trans (sym eq) eq2) = inj₂ y
heap-union-update {l}{h} d x a | just x₁ | Eq.[ eq ] | no ¬p | nothing | Eq.[ eq2 ] | C       rewrite (Eq.trans (sym eq) eq2) = inj₁ C
heap-union-update {l}{h} d x a | nothing | Eq.[ eq ] with a ≟ l | h a | Eq.inspect h a | x a
heap-union-update {l}{h} d x a | nothing | Eq.[ eq ] | no ¬p | just x₁ | Eq.[ eq2 ] | inj₁ x₂ = Eq.trans (Eq.trans (fst x₂) (sym eq2)) eq ,, snd x₂
heap-union-update {l}{h} d x a | nothing | Eq.[ eq ] | no ¬p | just x₁ | Eq.[ eq2 ] | inj₂ y = fst y ,, Eq.trans (snd y) (Eq.trans (sym eq2) eq)
heap-union-update {l}{h} d x a | nothing | Eq.[ eq ] | no ¬p | nothing | Eq.[ eq2 ] | E = E

heap-union-delete : ∀{h h₀ h₁ v}
  → v ¬dom h₁
  → h          ∼  h₀         ⊥ h₁
  → (h /[ v ]) ∼ (h₀ /[ v ]) ⊥ h₁
heap-union-delete {h}{h₀}{h₁}{v} d x a with (h /[ v ]) a | Eq.inspect (h /[ v ]) a
heap-union-delete {h} {h₀} {h₁} {v} d x a | just x₁ | Eq.[ eq ] with a ≟ v | h a | Eq.inspect h a | x a
heap-union-delete {h} {h₀} {h₁} {v} d x a | just x₁ | Eq.[ () ] | yes p | just x₂ | Eq.[ eq2 ] | R
heap-union-delete {h} {h₀} {h₁} {v} d x a | just x₁ | Eq.[ eq ] | no ¬p | just x₂ | Eq.[ eq2 ] | inj₁ x₃ rewrite (Eq.trans (sym eq) eq2) = inj₁ x₃
heap-union-delete {h} {h₀} {h₁} {v} d x a | just x₁ | Eq.[ eq ] | no ¬p | just x₂ | Eq.[ eq2 ] | inj₂ y  rewrite (Eq.trans (sym eq) eq2) = inj₂ y
heap-union-delete {h} {h₀} {h₁} {v} d x a | just x₁ | Eq.[ eq ] | no ¬p | nothing | Eq.[ eq2 ] | fst₁ ,, snd₁ = inj₂ (fst₁ ,, Eq.trans snd₁ (Eq.trans (sym eq2) eq))
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] with a ≟ v | h a | Eq.inspect h a | x a
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] | yes p | just x₁ | Eq.[ eq2 ] | inj₁ x₂ = refl ,, snd x₂
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] | yes p | just x₁ | Eq.[ eq2 ] | inj₂ y rewrite p = refl ,, d
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] | yes p | nothing | Eq.[ eq2 ] | E = refl ,, snd E
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] | no ¬p | just x₁ | Eq.[ eq2 ] | inj₁ x₂ = Eq.trans (fst x₂) (Eq.trans (sym eq2) eq) ,, snd x₂
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] | no ¬p | just x₁ | Eq.[ eq2 ] | inj₂ y = fst y ,, Eq.trans (snd y) (Eq.trans (sym eq2) eq)
heap-union-delete {h} {h₀} {h₁} {v} d x a | nothing | Eq.[ eq ] | no ¬p | nothing | Eq.[ eq2 ] | E = E

union-exclusionᵣ : ∀{l h h₀ h₁}
  → h ∼ h₀ ⊥ h₁
  → l ¬dom h
  → l ¬dom h₁
union-exclusionᵣ {l}{h} A B with h l | A l
... | nothing | fst₁ ,, snd₁ = snd₁

union-presenceᵣ : ∀{l h h₀ h₁}
  → h ∼ h₀ ⊥ h₁
  → l dom h
  → l dom h₀
  → l ¬dom h₁
union-presenceᵣ {l}{h} A B C with h l | A l
union-presenceᵣ {l} {h} A B C | just x | inj₁ (fst₁ ,, snd₁) = snd₁
union-presenceᵣ {l} {h} A B (fst₁ ,, snd₁) | just x | inj₂ (fst₂ ,, snd₂) with Eq.trans (sym fst₂) snd₁
... | ()

union-reduction : ∀{a b c s h′ h h₀ h′₀ h₁}
  → ⦅ c , s , h₀ ⦆ ⇒ ⦅ a , b , h′₀ ⦆
  → ⦅ c , s , h  ⦆ ⇒ ⦅ a , b , h′  ⦆
  → h  ∼ h₀  ⊥ h₁
  → h′ ∼ h′₀ ⊥ h₁
union-reduction Loc Loc C = C
union-reduction Comp₁ Comp₁ C = C
union-reduction (Comp₂ A) (Comp₂ B) C = union-reduction A B C
union-reduction (IfTrue x) (IfTrue x₁) C = C
union-reduction (IfTrue x) (IfFalse x₁) C = C
union-reduction (IfFalse x) (IfTrue x₁) C = C
union-reduction (IfFalse x) (IfFalse x₁) C = C
union-reduction While While C = C
union-reduction (Cons d A B) (Cons d2 A′ B′) C a rewrite A | B | A′ | B′ = heap-union-update (union-exclusionᵣ C d2) C a
union-reduction (Lookup e A) (Lookup e2 A′) C rewrite A | A′ = C
union-reduction (Write x) (Write x₁) C a = heap-union-update (union-presenceᵣ C x₁ x) C a
union-reduction (Dispose x) (Dispose x₁) C a = heap-union-delete (union-presenceᵣ C x₁ x) C a

frame2 : ∀{c s h h₀ h₁ h′ s′}
  → Safe ⦅ c , s , h₀ ⦆
  → h ∼ h₀ ⊥ h₁
  → ⦅ c , s , h ⦆ ⇒* ⦅ SKIP , s′ , h′ ⦆
  → ∃[ h′₀ ] ( ⦅ c , s , h₀ ⦆ ⇒* ⦅ SKIP , s′ , h′₀ ⦆
             × h′ ∼ h′₀ ⊥ h₁ )
frame2 s t (.(⦅ SKIP , _ , _ ⦆) ∎) = _ ,, (_ ∎) ,, t
frame2 {h₀ = h₀} s t (_→⟨_⟩_ .(⦅ _ , _ , _ ⦆) {⦅ _ , _ , _ ⦆} x r) with lemma2 h₀ (union-subset _ t) x
... | inj₁ x₄ = ⊥-elim (s (_ →⟨ x₄ ⟩ (abort ∎)))
... | inj₂ (fst₁ ,, fst₂ ,, snd₁) with frame2 (λ z → s (_ →⟨ snd₁ ⟩ z)) (union-reduction snd₁ x t) r
... | fst₃ ,, fst₄ ,, snd₂ = fst₃ ,, (_ →⟨ snd₁ ⟩ fst₄) ,, snd₂
frame2 s t (_→⟨_⟩_ .(⦅ _ , _ , _ ⦆) {abort} x (.abort →⟨ () ⟩ r))

⊨[_]_[_] : assn → com → assn → Set
⊨[ A ] c [ B ] = ∀{s h}
  → A s h
  → Safe ⦅ c , s , h ⦆
  × (∀{s′ h′} → ⦅ c , s , h ⦆ ⇒* ⦅ SKIP , s′ , h′ ⦆ → B s′ h′)

NotInfluenced : assn → com → Set
NotInfluenced R c = ∀{s s′ z h₀ h′₀ hᵣ}
  → z ∼ h′₀ ⊥ hᵣ
  → ⦅ c , s , h₀ ⦆ ⇒* ⦅ SKIP , s′ , h′₀ ⦆
  → R s hᵣ → R s′ hᵣ

frame-soundness : ∀{A B R : assn} {c}
  → NotInfluenced R c
  → ⊨[ A     ] c [ B     ]
  → ⊨[ A * R ] c [ B * R ]
frame-soundness {A}{B}{R}{c} Inf H {s}{h} (h₀ ,, h₁ ,, ⊥ ,, A₀ ,, R₁) with H A₀
... | safe ,, conv = frame1 ⊥ safe ,, frame2-ex
   where frame2-ex : ∀{s′ h′}
                   → ⦅ c , s , h ⦆ ⇒* ⦅ SKIP , s′ , h′ ⦆
                   → ∃[ h₁ ] ∃[ h₂ ] ( (h′ ∼ h₁ ⊥ h₂)
                                     × B s′ h₁
                                     × R s′ h₂)
         frame2-ex rs with frame2 safe ⊥ rs
         ... | h′₀ ,, r ,, ⊥′ = h′₀ ,, h₁ ,, ⊥′ ,, conv r  ,, Inf ⊥′ r R₁

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
module Issue784.Context where

open import Data.List using (List; []; _∷_; _++_; [_]; filter) renaming (map to mapL)
import Level

open import Issue784.Values

record Context ℓ : Set (Level.suc ℓ) where
  constructor context
  field get : Values ℓ

signature : ∀ {ℓ} → Context ℓ → Types ℓ
signature = types ∘ Context.get

ctxnames : ∀ {ℓ} → Context ℓ → Names
ctxnames = names ∘ Context.get

NonRepetitiveContext : ∀ {ℓ} → Context ℓ → _
NonRepetitiveContext = NonRepetitiveNames ∘ Context.get

getBySignature : ∀ {ℓ} {n : String} {A : Set ℓ} {x : Context ℓ} → (n , A) ∈ signature x → A
getBySignature {x = x} = getBySignature′ {x = Context.get x} where
  getBySignature′ : ∀ {ℓ} {n : String} {A : Set ℓ} {x : Values ℓ} → (n , A) ∈ types x → A
  getBySignature′ {x = []} ()
  getBySignature′ {x = (_ , _ , à) ∷ _} (here {x = ._} {xs = ._} p) = ≡-elim′ proj₂ (≡-sym p) à
  getBySignature′ {x = _ ∷ _} (there {x = ._} {xs = ._} p) = getBySignature′ p

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Boolean.Functions where

open import Data.Boolean
open import Type

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A definition for the permutation relation using setoid equality
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Permutation.Setoid
  {a ℓ} (S : Setoid a ℓ) where

open import Data.List.Base using (List; _∷_)
import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
import Data.List.Relation.Binary.Pointwise as Pointwise
open import Data.List.Relation.Binary.Equality.Setoid S
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

private
  module Eq = Setoid S
open Eq using (_≈_) renaming (Carrier to A)

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

open Homogeneous public
  using (refl; prep; swap; trans)

infix 3 _↭_

_↭_ : Rel (List A) (a ⊔ ℓ)
_↭_ = Homogeneous.Permutation _≈_

------------------------------------------------------------------------
-- Constructor aliases

-- These provide aliases for `swap` and `prep` when the elements being
-- swapped or prepended are propositionally equal

↭-prep : ∀ x {xs ys} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
↭-prep x xs↭ys = prep Eq.refl xs↭ys

↭-swap : ∀ x y {xs ys} → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
↭-swap x y xs↭ys = swap Eq.refl Eq.refl xs↭ys

------------------------------------------------------------------------
-- Functions over permutations

steps : ∀ {xs ys} → xs ↭ ys → ℕ
steps (refl _)            = 1
steps (prep _ xs↭ys)      = suc (steps xs↭ys)
steps (swap _ _ xs↭ys)    = suc (steps xs↭ys)
steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs

------------------------------------------------------------------------
-- _↭_ is an equivalence

↭-reflexive : _≡_ ⇒ _↭_
↭-reflexive refl = refl (Pointwise.refl Eq.refl)

↭-refl : Reflexive _↭_
↭-refl = ↭-reflexive refl

↭-sym : Symmetric _↭_
↭-sym = Homogeneous.sym Eq.sym

↭-trans : Transitive _↭_
↭-trans = trans

↭-isEquivalence : IsEquivalence _↭_
↭-isEquivalence = Homogeneous.isEquivalence Eq.refl Eq.sym

↭-setoid : Setoid _ _
↭-setoid = Homogeneous.setoid {R = _≈_} Eq.refl Eq.sym

------------------------------------------------------------------------
-- A reasoning API to chain permutation proofs

module PermutationReasoning where

  private
    module Base = SetoidReasoning ↭-setoid

  open SetoidReasoning ↭-setoid public
    hiding (step-≈; step-≈˘)

  infixr 2 step-↭  step-↭˘ step-≋ step-≋˘ step-swap step-prep

  step-↭  = Base.step-≈
  step-↭˘ = Base.step-≈˘

  -- Step with pointwise list equality
  step-≋ : ∀ x {y z} → y IsRelatedTo z → x ≋ y → x IsRelatedTo z
  step-≋ x (relTo y↔z) x≋y = relTo (trans (refl x≋y) y↔z)

  -- Step with flipped pointwise list equality
  step-≋˘ : ∀ x {y z} → y IsRelatedTo z → y ≋ x → x IsRelatedTo z
  step-≋˘ x y↭z y≋x = x ≋⟨ ≋-sym y≋x ⟩ y↭z

  -- Skip reasoning on the first element
  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
  step-prep x xs rel xs↭ys = relTo (trans (prep Eq.refl xs↭ys) (begin rel))

  -- Skip reasoning about the first two elements
  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
  step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl xs↭ys) (begin rel))

  syntax step-↭  x y↭z x↭y = x ↭⟨  x↭y ⟩ y↭z
  syntax step-↭˘ x y↭z y↭x = x ↭˘⟨  y↭x ⟩ y↭z
  syntax step-≋  x y↭z x≋y = x ≋⟨  x≋y ⟩ y↭z
  syntax step-≋˘ x y↭z y≋x = x ≋˘⟨  y≋x ⟩ y↭z
  syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
  syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z


text:
module Issue919 where

open import Common.Prelude

Zero : Nat → Set
Zero 0 = ⊤
Zero (suc _) = ⊥

test : (n : Nat) {p : Zero n} → Set → Set
test 0            A = A
test (suc _) {()}

-- Horrible error for first clause:
-- Cannot eliminate type Set with pattern {(implicit)} (did you supply
-- too many arguments?)
-- when checking that the pattern zero has type Nat

-- Caused by trailing implicit insertion (see Rules/Def.hs).

-- With trailing implicit insertion switched off, this should work now.


text:
{-# OPTIONS --no-termination-check #-}
module Issue137 where

record Foo : Set1 where
  field
    foo : {x : Set} → Set

record Bar : Set1 where
  field
    bar : Foo

record Baz (P : Bar) : Set1 where
  field
    baz : Set

postulate
  P : Bar
  Q : Baz P

f : Baz.baz Q → Set
f r with f r
f r | A = A

-- The bug was:

-- Issue137.agda:22,1-12
-- Set should be a function type, but it isn't
-- when checking that the expression λ x → Foo.foo (Bar.bar P) {x} has
-- type Set

-- If the field foo is replaced by
--   foo : (x : Set) → Set
-- then the code type checks.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, AIM XXIII 2016-04-21 Overloaded projections

-- Milestone 1: Check overloaded projections on rhs (without postponing).

{-# OPTIONS --allow-unsolved-metas #-}

module _ (A : Set) (a : A) where

record R B : Set where
  field f : B
open R

record S B : Set where
  field f : B
open S

r : R A
R.f r = a

s : S A
S.f s = f r

t : R A → S A
S.f (t r) = f r

u : _
u = f s

-- interactive

hole0 : A
hole0 = {! f s !}  -- normalize me

hole1 = {!λ r → f (t r)!} -- normalize me

record T B : Set where
  field f : B → B
open T

-- Postpone /further/ argument of overloaded projection.

hole2 : ∀{A} → T A → A → A
hole2 t x = f t {!x!}

-- Milestone 2: Postpone overloading.

hole3 = f {! r !}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by strict partial orders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.StrictPartialOrder
       {s₁ s₂ s₃} (SPO : StrictPartialOrder s₁ s₂ s₃) where

open Relation.Binary.StrictPartialOrder SPO
  renaming (trans to <-trans)
open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_

------------------------------------------------------------------------
-- Strict partial orders can be converted to posets

poset : Poset _ _ _
poset = record
  { isPartialOrder = isPartialOrder isStrictPartialOrder
  }

open Poset poset public


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

open import Cubical.Foundations.Prelude

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

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Semigroup.Base
open import Cubical.Algebra.Monoid.Base

open import Cubical.HITs.SetQuotients

open GroupStr

ℤ-isGroup : IsGroup {G = ℤ} ([ 0 , 0 ]) (_+ℤ_) (-ℤ_)
IsSemigroup.is-set (IsMonoid.isSemigroup (IsGroup.isMonoid ℤ-isGroup)) = ℤ-isSet
IsSemigroup.assoc (IsMonoid.isSemigroup (IsGroup.isMonoid ℤ-isGroup)) = +ℤ-assoc
IsMonoid.identity (IsGroup.isMonoid ℤ-isGroup) = λ x → (zero-identityʳ 0 x  , zero-identityˡ 0 x)
IsGroup.inverse ℤ-isGroup = λ x → (-ℤ-invʳ x , -ℤ-invˡ x)

ℤGroup : Group₀
fst ℤGroup = ℤ
1g (snd ℤGroup) = [ 0 , 0 ]
_·_ (snd ℤGroup) = _+ℤ_
inv (snd ℤGroup) = -ℤ_
isGroup (snd ℤGroup) = ℤ-isGroup

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


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

{- Remember to keep CodeBP.agda in sync. -}

open import HoTT
import homotopy.RelativelyConstantToSetExtendsViaSurjection as SurjExt

module homotopy.vankampen.CodeAP {i j k l}
  (span : Span {i} {j} {k})
  {D : Type l} (h : D → Span.C span) (h-is-surj : is-surj h) where

  open Span span

  data precodeAA (a₀ : A) : A → Type (lmax (lmax (lmax i j) k) l)
  data precodeAB (a₀ : A) (b₁ : B) : Type (lmax (lmax (lmax i j) k) l)

  data precodeAA a₀ where
    pc-a : ∀ {a₁} (pA : a₀ =₀ a₁) → precodeAA a₀ a₁
    pc-aba : ∀ d {a₁} (pc : precodeAB a₀ (g (h d))) (pA : f (h d) =₀ a₁) → precodeAA a₀ a₁

  infix 66 pc-a
  syntax pc-a p = ⟧a p
  infixl 65 pc-aba
  syntax pc-aba d pcAB pA = pcAB ab⟦ d ⟧a pA

  data precodeAB a₀ b₁ where
    pc-aab : ∀ d (pc : precodeAA a₀ (f (h d))) (pB : g (h d) =₀ b₁) → precodeAB a₀ b₁

  infixl 65 pc-aab
  syntax pc-aab d pcAA pB = pcAA aa⟦ d ⟧b pB

  data precodeAA-rel {a₀ : A} : {a₁ : A}
    → precodeAA a₀ a₁ → precodeAA a₀ a₁ → Type (lmax (lmax (lmax i j) k) l)
  data precodeAB-rel {a₀ : A} : {b₁ : B}
    → precodeAB a₀ b₁ → precodeAB a₀ b₁ → Type (lmax (lmax (lmax i j) k) l)
  data precodeAA-rel {a₀} where
    pcAAr-idp₀-idp₀ : ∀ {d} pcAA → precodeAA-rel (pcAA aa⟦ d ⟧b idp₀ ab⟦ d ⟧a idp₀) pcAA
    pcAAr-cong : ∀ {d a₁ pcAB₁ pcAB₂} (r : precodeAB-rel pcAB₁ pcAB₂) (pA : f (h d) =₀ a₁)
      → precodeAA-rel (pcAB₁ ab⟦ d ⟧a pA) (pcAB₂ ab⟦ d ⟧a pA)
  data precodeAB-rel {a₀} where
    pcABr-idp₀-idp₀ : ∀ {d} pcAB → precodeAB-rel (pcAB ab⟦ d ⟧a idp₀ aa⟦ d ⟧b idp₀) pcAB
    pcABr-switch : ∀ {d₀ d₁ : D} pcAB (pC : h d₀ =₀ h d₁)
      → precodeAB-rel (pcAB ab⟦ d₀ ⟧a ap₀ f pC aa⟦ d₁ ⟧b idp₀) (pcAB ab⟦ d₀ ⟧a idp₀ aa⟦ d₀ ⟧b ap₀ g pC)
    pcABr-cong : ∀ {d b₁ pcAA₁ pcAA₂} (r : precodeAA-rel pcAA₁ pcAA₂) (pB : g (h d) =₀ b₁)
      → precodeAB-rel (pcAA₁ aa⟦ d ⟧b pB) (pcAA₂ aa⟦ d ⟧b pB)

  codeAA : A → A → Type (lmax (lmax (lmax i j) k) l)
  codeAA a₀ a₁ = SetQuot (precodeAA-rel {a₀} {a₁})

  codeAB : A → B → Type (lmax (lmax (lmax i j) k) l)
  codeAB a₀ b₁ = SetQuot (precodeAB-rel {a₀} {b₁})

  c-aba : ∀ {a₀} d {a₁} (pc : codeAB a₀ (g (h d))) (pA : f (h d) =₀ a₁) → codeAA a₀ a₁
  c-aba d {a₁} c pA = SetQuot-rec SetQuot-is-set
    (λ pc → q[ pc-aba d pc pA ])
    (λ r → quot-rel $ pcAAr-cong r pA) c

  c-aab : ∀ {a₀} d {b₁} (pc : codeAA a₀ (f (h d))) (pB : g (h d) =₀ b₁) → codeAB a₀ b₁
  c-aab d {a₁} c pB = SetQuot-rec SetQuot-is-set
    (λ pc → q[ pc-aab d pc pB ])
    (λ r → quot-rel $ pcABr-cong r pB) c

-- codeAP

  abstract
    pcAA-idp₀-idp₀-head : ∀ {d₀ a} (pA : f (h d₀) =₀ a)
      → q[ ⟧a idp₀ aa⟦ d₀ ⟧b idp₀ ab⟦ d₀ ⟧a pA ] == q[ ⟧a pA ] :> codeAA _ a
    pcAA-idp₀-idp₀-head {d₀} = Trunc-elim (λ _ → =-preserves-set SetQuot-is-set) lemma where
      lemma : ∀ {a} (pA : f (h d₀) == a)
        → q[ ⟧a idp₀ aa⟦ d₀ ⟧b idp₀ ab⟦ d₀ ⟧a [ pA ] ] == q[ ⟧a [ pA ] ] :> codeAA _ a
      lemma idp = quot-rel $ pcAAr-idp₀-idp₀ (⟧a idp₀)

  pcAA-prepend : ∀ {a₀} d₁ {a₂} → a₀ =₀ f (h d₁) → precodeAA (f (h d₁)) a₂ → precodeAA a₀ a₂
  pcAB-prepend : ∀ {a₀} d₁ {b₂} → a₀ =₀ f (h d₁) → precodeAB (f (h d₁)) b₂ → precodeAB a₀ b₂
  pcAA-prepend d₁ pA (pc-a pA₁) = pc-aba d₁ (pc-aab d₁ (pc-a pA) idp₀) pA₁
  pcAA-prepend d₁ pA (pc-aba d pc pA₁) = pc-aba d (pcAB-prepend d₁ pA pc) pA₁
  pcAB-prepend d₁ pA (pc-aab d pc pB) = pc-aab d (pcAA-prepend d₁ pA pc) pB

  abstract
    pcAA-prepend-idp₀ : ∀ {d₀ a₁} (pcAA : precodeAA (f (h d₀)) a₁)
      → q[ pcAA-prepend d₀ idp₀ pcAA ] == q[ pcAA ] :> codeAA (f (h d₀)) a₁
    pcAB-prepend-idp₀ : ∀ {d₀ b₁} (pcAB : precodeAB (f (h d₀)) b₁)
      → q[ pcAB-prepend d₀ idp₀ pcAB ] == q[ pcAB ] :> codeAB (f (h d₀)) b₁
    pcAA-prepend-idp₀ (pc-a pA) = pcAA-idp₀-idp₀-head pA
    pcAA-prepend-idp₀ (pc-aba d pc pA) = pcAB-prepend-idp₀ pc |in-ctx λ c → c-aba d c pA
    pcAB-prepend-idp₀ (pc-aab d pc pA) = pcAA-prepend-idp₀ pc |in-ctx λ c → c-aab d c pA

    transp-cAA-l : ∀ d {a₀ a₁} (p : f (h d) == a₀) (pcAA : precodeAA (f (h d)) a₁)
      → transport (λ x → codeAA x a₁) p q[ pcAA ] == q[ pcAA-prepend d [ ! p ] pcAA ]
    transp-cAA-l d idp pcAA = ! $ pcAA-prepend-idp₀ pcAA

    transp-cAB-l : ∀ d {a₀ b₁} (p : f (h d) == a₀) (pcAB : precodeAB (f (h d)) b₁)
      → transport (λ x → codeAB x b₁) p q[ pcAB ] == q[ pcAB-prepend d [ ! p ] pcAB ]
    transp-cAB-l d idp pcAB = ! $ pcAB-prepend-idp₀ pcAB

    transp-cAA-r : ∀ d {a₀ a₁} (p : f (h d) == a₁) (pcAA : precodeAA a₀ (f (h d)))
      → transport (λ x → codeAA a₀ x) p q[ pcAA ] == q[ pcAA aa⟦ d ⟧b idp₀ ab⟦ d ⟧a [ p ] ]
    transp-cAA-r d idp pcAA = ! $ quot-rel $ pcAAr-idp₀-idp₀ pcAA

    transp-cAB-r : ∀ d {a₀ b₁} (p : g (h d) == b₁) (pcAB : precodeAB a₀ (g (h d)))
      → transport (λ x → codeAB a₀ x) p q[ pcAB ] == q[ pcAB ab⟦ d ⟧a idp₀ aa⟦ d ⟧b [ p ] ]
    transp-cAB-r d idp pcAB = ! $ quot-rel $ pcABr-idp₀-idp₀ pcAB

  module CodeAAEquivCodeAB (a₀ : A) where

    eqv-on-image : (d : D) → codeAA a₀ (f (h d)) ≃ codeAB a₀ (g (h d))
    eqv-on-image d = equiv to from to-from from-to where
      to = λ c → c-aab d c idp₀
      from = λ c → c-aba d c idp₀

      abstract
        from-to : ∀ cAA → from (to cAA) == cAA
        from-to = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (λ pcAA → quot-rel (pcAAr-idp₀-idp₀ pcAA))
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

        to-from : ∀ cAB → to (from cAB) == cAB
        to-from = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (λ pcAB → quot-rel (pcABr-idp₀-idp₀ pcAB))
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    abstract
      eqv-is-const : ∀ d₁ d₂ (p : h d₁ == h d₂)
        → eqv-on-image d₁ == eqv-on-image d₂
        [ (λ c → codeAA a₀ (f c) ≃ codeAB a₀ (g c)) ↓ p ]
      eqv-is-const d₁ d₂ p = ↓-Subtype-in (λ d → is-equiv-prop) $
        ↓-→-from-transp $ λ= $
          SetQuot-elim (λ _ → =-preserves-set SetQuot-is-set)
            (λ pcAA →
              transport (λ c → codeAB a₀ (g c)) p q[ pcAA aa⟦ d₁ ⟧b idp₀ ]
                =⟨ ap-∘ (codeAB a₀) g p |in-ctx (λ p → coe p q[ pcAA aa⟦ d₁ ⟧b idp₀ ]) ⟩
              transport (codeAB a₀) (ap g p) q[ pcAA aa⟦ d₁ ⟧b idp₀ ]
                =⟨ transp-cAB-r d₁ (ap g p) (pcAA aa⟦ d₁ ⟧b idp₀) ⟩
              q[ pcAA aa⟦ d₁ ⟧b idp₀ ab⟦ d₁ ⟧a idp₀ aa⟦ d₁ ⟧b [ ap g p ] ]
                =⟨ ! $ quot-rel $ pcABr-switch (pcAA aa⟦ d₁ ⟧b idp₀) [ p ] ⟩
              q[ pcAA aa⟦ d₁ ⟧b idp₀ ab⟦ d₁ ⟧a [ ap f p ] aa⟦ d₂ ⟧b idp₀ ]
                =⟨ ! $ transp-cAA-r d₁ (ap f p) pcAA |in-ctx (λ c → c-aab d₂ c idp₀) ⟩
              c-aab d₂ (transport (codeAA a₀) (ap f p) q[ pcAA ]) idp₀
                =⟨ ∘-ap (codeAA a₀) f p |in-ctx (λ p → coe p q[ pcAA ]) |in-ctx (λ c → c-aab d₂ c idp₀) ⟩
              c-aab d₂ (transport (λ c → codeAA a₀ (f c)) p q[ pcAA ]) idp₀
                =∎)
            (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    module SE = SurjExt
      (λ c → ≃-is-set SetQuot-is-set SetQuot-is-set)
      h h-is-surj
      eqv-on-image
      eqv-is-const

    abstract
      eqv : ∀ c → codeAA a₀ (f c) ≃ codeAB a₀ (g c)
      eqv = SE.ext

      eqv-β : ∀ d → eqv (h d) == eqv-on-image d
      eqv-β = SE.β

  module CodeAP (a₀ : A) = PushoutRec (codeAA a₀) (codeAB a₀)
    (ua ∘ CodeAAEquivCodeAB.eqv a₀)

  codeAP : A → Pushout span → Type (lmax (lmax (lmax i j) k) l)
  codeAP = CodeAP.f

  abstract
    codeAP-level : ∀ {a₀ p₁} → is-set (codeAP a₀ p₁)
    codeAP-level {a₀} {p₁} = Pushout-elim
      {P = λ p₁ → is-set (codeAP a₀ p₁)}
      (λ a₁ → SetQuot-is-set)
      (λ b₁ → SetQuot-is-set)
      (λ c₁ → prop-has-all-paths-↓ is-set-is-prop)
      p₁
  codeAP-is-set = codeAP-level

  abstract
    transp-cAP-glue : ∀ {a₀} d₁ (pcAA : precodeAA a₀ (f (h d₁)))
      → transport (codeAP a₀) (glue (h d₁)) q[ pcAA ] == q[ pcAA aa⟦ d₁ ⟧b idp₀ ]
    transp-cAP-glue {a₀} d₁ pcAA =
      transport (codeAP a₀) (glue (h d₁)) q[ pcAA ]
        =⟨ ap (λ e → coe e q[ pcAA ]) (CodeAP.glue-β a₀ (h d₁) ∙ ap ua (CodeAAEquivCodeAB.eqv-β a₀ d₁)) ⟩
      coe (ua (CodeAAEquivCodeAB.eqv-on-image a₀ d₁)) q[ pcAA ]
        =⟨ coe-β (CodeAAEquivCodeAB.eqv-on-image a₀ d₁) q[ pcAA ] ⟩
      q[ pcAA aa⟦ d₁ ⟧b idp₀ ]
        =∎

    transp-cAP-!glue : ∀ {a₀} d₁ (pcAB : precodeAB a₀ (g (h d₁)))
      → transport (codeAP a₀) (! (glue (h d₁))) q[ pcAB ] == q[ pcAB ab⟦ d₁ ⟧a idp₀ ]
    transp-cAP-!glue {a₀} d₁ pcAB =
      transport (codeAP a₀) (! (glue (h d₁))) q[ pcAB ]
        =⟨ ap (λ e → coe e q[ pcAB ]) (ap-! (codeAP a₀) (glue (h d₁)))
         ∙ coe-! (ap (codeAP a₀) (glue (h d₁))) q[ pcAB ] ⟩
      transport! (codeAP a₀) (glue (h d₁)) q[ pcAB ]
        =⟨ ap (λ e → coe! e q[ pcAB ]) (CodeAP.glue-β a₀ (h d₁) ∙ ap ua (CodeAAEquivCodeAB.eqv-β a₀ d₁)) ⟩
      coe! (ua (CodeAAEquivCodeAB.eqv-on-image a₀ d₁)) q[ pcAB ]
        =⟨ coe!-β (CodeAAEquivCodeAB.eqv-on-image a₀ d₁) q[ pcAB ] ⟩
      q[ pcAB ab⟦ d₁ ⟧a idp₀ ]
        =∎

  -- code to path
  pcAA-to-path : ∀ {a₀ a₁} → precodeAA a₀ a₁ → left a₀ =₀ left a₁ :> Pushout span
  pcAB-to-path : ∀ {a₀ b₁} → precodeAB a₀ b₁ → left a₀ =₀ right b₁ :> Pushout span
  pcAA-to-path (pc-a pA) = ap₀ left pA
  pcAA-to-path (pc-aba d pc pA) = pcAB-to-path pc ∙₀' !₀ [ glue (h d) ] ∙₀' ap₀ left pA
  pcAB-to-path (pc-aab d pc pB) = pcAA-to-path pc ∙₀' [ glue (h d) ] ∙₀' ap₀ right pB

  abstract
    pcAA-to-path-rel : ∀ {a₀ a₁} {pcAA₀ pcAA₁ : precodeAA a₀ a₁}
      → precodeAA-rel pcAA₀ pcAA₁ → pcAA-to-path pcAA₀ == pcAA-to-path pcAA₁
    pcAB-to-path-rel : ∀ {a₀ b₁} {pcAB₀ pcAB₁ : precodeAB a₀ b₁}
      → precodeAB-rel pcAB₀ pcAB₁ → pcAB-to-path pcAB₀ == pcAB-to-path pcAB₁
    pcAA-to-path-rel (pcAAr-idp₀-idp₀ pcAA) =
        ∙₀'-assoc (pcAA-to-path pcAA) [ glue (h _) ] [ ! (glue (h _)) ]
      ∙ ap (λ p → pcAA-to-path pcAA ∙₀' [ p ]) (!-inv'-r (glue (h _)))
      ∙ ∙₀'-unit-r (pcAA-to-path pcAA)
    pcAA-to-path-rel (pcAAr-cong pcAB pA) = pcAB-to-path-rel pcAB |in-ctx _∙₀' !₀ [ glue (h _) ] ∙₀' ap₀ left pA
    pcAB-to-path-rel (pcABr-idp₀-idp₀ pcAB) =
        ∙₀'-assoc (pcAB-to-path pcAB) [ ! (glue (h _)) ] [ glue (h _) ]
      ∙ ap (λ p → pcAB-to-path pcAB ∙₀' [ p ]) (!-inv'-l (glue (h _)))
      ∙ ∙₀'-unit-r (pcAB-to-path pcAB)
    pcAB-to-path-rel (pcABr-switch pcAB pC) =
        ap (_∙₀' [ glue (h _) ]) (! (∙₀'-assoc (pcAB-to-path pcAB) [ ! (glue (h _)) ] (ap₀ left (ap₀ f pC))))
      ∙ ∙₀'-assoc (pcAB-to-path pcAB ∙₀' [ ! (glue (h _)) ]) (ap₀ left (ap₀ f pC)) [ glue (h _) ]
      ∙ ap ((pcAB-to-path pcAB ∙₀' [ ! (glue (h _)) ]) ∙₀'_) (natural₀ pC)
      where
        natural : ∀ {c₀ c₁} (p : c₀ == c₁)
          → (ap left (ap f p) ∙' glue c₁) == (glue c₀ ∙' ap right (ap g p))
          :> (left (f c₀) == right (g c₁) :> Pushout span)
        natural idp = ∙'-unit-l (glue _)

        natural₀ : ∀ {c₀ c₁} (p : c₀ =₀ c₁)
          → (ap₀ left (ap₀ f p) ∙₀' [ glue c₁ ]) == ([ glue c₀ ] ∙₀' ap₀ right (ap₀ g p))
          :> (left (f c₀) =₀ right (g c₁) :> Pushout span)
        natural₀ = Trunc-elim (λ _ → =-preserves-set Trunc-level) (ap [_] ∘ natural)
    pcAB-to-path-rel (pcABr-cong pcAA pB) = pcAA-to-path-rel pcAA |in-ctx _∙₀' [ glue (h _) ] ∙₀' ap₀ right pB

  decodeAA : ∀ {a₀ a₁} → codeAA a₀ a₁ → left a₀ =₀ left a₁ :> Pushout span
  decodeAB : ∀ {a₀ b₁} → codeAB a₀ b₁ → left a₀ =₀ right b₁ :> Pushout span
  decodeAA = SetQuot-rec Trunc-level pcAA-to-path pcAA-to-path-rel
  decodeAB = SetQuot-rec Trunc-level pcAB-to-path pcAB-to-path-rel

  abstract
    decodeAA-is-decodeAB : ∀ {a₀} c₁ →
      decodeAA {a₀} {f c₁} == decodeAB {a₀} {g c₁}
      [ (λ p₁ → codeAP a₀ p₁ → left a₀ =₀ p₁) ↓ glue c₁ ]
    decodeAA-is-decodeAB {a₀ = a₀} = SurjExt.ext
      (λ _ → ↓-preserves-level $ Π-is-set λ _ → Trunc-level) h h-is-surj
      (λ d₁ → ↓-→-from-transp $ λ= $ SetQuot-elim
        {P = λ cAA → transport (left a₀ =₀_) (glue (h d₁)) (decodeAA cAA)
                  == decodeAB (transport (codeAP a₀) (glue (h d₁)) cAA)}
        (λ _ → =-preserves-set Trunc-level)
        (λ pcAA →
          transport (left a₀ =₀_) (glue (h d₁)) (pcAA-to-path pcAA)
            =⟨ transp₀-cst=₀idf [ glue (h d₁) ] (pcAA-to-path pcAA) ⟩
          pcAA-to-path pcAA ∙₀' [ glue (h d₁) ]
            =⟨ ! $ ap (λ e → decodeAB (–> e q[ pcAA ])) (CodeAAEquivCodeAB.eqv-β a₀ d₁) ⟩
          decodeAB (–> (CodeAAEquivCodeAB.eqv a₀ (h d₁)) q[ pcAA ])
            =⟨ ! $ ap decodeAB (coe-β (CodeAAEquivCodeAB.eqv a₀ (h d₁)) q[ pcAA ]) ⟩
          decodeAB (coe (ua (CodeAAEquivCodeAB.eqv a₀ (h d₁))) q[ pcAA ])
            =⟨ ! $ ap (λ p → decodeAB (coe p q[ pcAA ])) (CodeAP.glue-β a₀ (h d₁)) ⟩
          decodeAB (transport (codeAP a₀) (glue (h d₁)) q[ pcAA ])
            =∎)
        (λ _ → prop-has-all-paths-↓ $ Trunc-level {n = 0} _ _))
      (λ _ _ _ → prop-has-all-paths-↓ $ ↓-level $ Π-is-set λ _ → Trunc-level)

  decodeAP : ∀ {a₀ p₁} → codeAP a₀ p₁ → left a₀ =₀ p₁
  decodeAP {p₁ = p₁} = Pushout-elim
    (λ a₁ → decodeAA) (λ b₁ → decodeAB)
    decodeAA-is-decodeAB
    p₁

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

-- this is mostly reference for an unused intermediate step.
module Cauchy2 where

open import Data.Nat
open import Data.Vec renaming (map to mapV; _++_ to _++V_; concat to concatV)
open import Data.Fin using (Fin; inject+; raise; inject≤; fromℕ; toℕ)
open import Function using (id)
open import Relation.Binary.PropositionalEquality using (_≡_; subst)

open import VectorLemmas
open import LeqLemmas
open import Cauchy using (id+)

Cauchy : ℕ → ℕ → Set
Cauchy n₁ n₂ = Vec (Fin n₁) n₂

------------------------------------------------------------------------------
-- Elementary permutations in the Cauchy representation

emptycauchy : Cauchy 0 0
emptycauchy = []

idcauchy : (n : ℕ) → Cauchy n n
idcauchy = allFin

-- Sequential composition

scompcauchy : ∀ {n₀ n₁ n₂} → Cauchy n₁ n₀ → Cauchy n₂ n₁ → Cauchy n₂ n₀
scompcauchy {n} perm₁ perm₂ =
 tabulate (λ i → lookup (lookup i perm₁) perm₂)

-- swap the first m elements with the last n elements
-- [ v₀ , v₁   , v₂   , ... , vm-1 ,     vm , vm₊₁ , ... , vm+n-1 ]
-- ==>
-- [ vm , vm₊₁ , ... , vm+n-1 ,     v₀ , v₁   , v₂   , ... , vm-1 ]

swap+cauchy : (m n : ℕ) → Cauchy (m + n) (n + m)
swap+cauchy m n = {!!} -- tabulate swapper

-- Parallel additive composition
-- append both permutations but adjust the indices in the second
-- permutation by the size of the first type so that it acts on the
-- second part of the vector

pcompcauchy : ∀ {m₁ n₁ m₂ n₂} → Cauchy m₁ m₂ → Cauchy n₁ n₂ → Cauchy (m₁ + n₁) (m₂ + n₂)
pcompcauchy {m} {n} α β = mapV (inject+ n) α ++V mapV (raise m) β

-- Tensor multiplicative composition
-- Transpositions in α correspond to swapping entire rows
-- Transpositions in β correspond to swapping entire columns
tcompcauchy : ∀ {m₁ n₁ m₂ n₂} → Cauchy m₁ m₂ → Cauchy n₁ n₂ → Cauchy (m₁ * n₁) (m₂ * n₂)
tcompcauchy {m} {n} α β =
 concatV
   (mapV
     (λ b →
        mapV (λ d → inject≤ (fromℕ (toℕ b * n + toℕ d)) (i*n+k≤m*n b d)) β)
     α)

-- swap⋆
--
-- This is essentially the classical problem of in-place matrix transpose:
-- "http://en.wikipedia.org/wiki/In-place_matrix_transposition"
-- Given m and n, the desired permutation in Cauchy representation is:
-- P(i) = m*n-1 if i=m*n-1
--      = m*i mod m*n-1 otherwise

transposeIndex : (m n : ℕ) →
      (b : Fin m) → (d : Fin n) → Fin (n * m)
transposeIndex m n b d =
   inject≤ (fromℕ (toℕ d * m + toℕ b))
     (i*n+k≤m*n d b)
 {- inject≤
   (fromℕ (toℕ d * m + toℕ b))
   (trans≤ (i*n+k≤m*n d b) (refl′ (*-comm n m))) -}

swap⋆cauchy : (m₁ n₁ m₂ n₂ : ℕ) → (meq : m₂ ≡ m₁) → (neq : n₂ ≡ n₁) → Cauchy (n₁ * m₁) (n₂ * m₂)
swap⋆cauchy m₁ n₁ m₂ n₂ meq neq =
 concatV (mapV
           (λ d → mapV (λ b → transposeIndex m₁ n₁ (subst Fin meq b) (subst Fin neq d)) (allFin m₂))
           (allFin n₂))

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import lib.Basics
open import lib.types.Truncation
open import lib.types.Fin
open import lib.types.Nat
open import lib.types.Empty
open import lib.types.Unit
open import lib.types.Coproduct
open import lib.types.Sigma
open import lib.types.Paths
open import lib.NConnected

open import Util.Misc
open import Util.Finite
open import Util.Coproducts

open import Graphs.Definition
open import Graphs.Properties

open import Coequalizers.Definition
open import Coequalizers.PreserveEquivalence
open import Coequalizers.EdgeCoproduct
open import Coequalizers.Misc
open import Graphs.SubTrees

{- We show that graphs with finite vertex set have spanning trees. -}
module Graphs.SpanningTreeFinite {i : ULevel} where

module _ (E : Type i) (V : Type i) ⦃ gph : Graph E V ⦄ where

instance
  noedges : {j : ULevel} {V : Type j} → Graph ⊥ V -- defines the trivial coequalizer V / ⊥
  noedges = record { π₀ = ⊥-elim ; π₁ = ⊥-elim }

noedge-triv : {j : ULevel} {V : Type j} → V / ⊥ ≃ V
noedge-triv {V = V} = f , (record { g = c[_] ; f-g = f-g ; g-f = g-f ; adj = adj })
  where
    f : V / ⊥ → V
    f = Coeq-rec (idf V) (λ _ → idp)

    f-g : (v : V) → (f (c[ v ]) == v)
    f-g v = idp

    g-f : (z : V / ⊥) → (c[ (f z) ] == z)
    g-f = Coeq-elim _ (λ _ → idp) ⊥-elim

    adj : (z : V / ⊥) → ap f (g-f z) == idp
    adj = Coeq-elim _ (λ _ → idp) ⊥-elim

{- A spanning tree is a subtree where the inclusion of vertex sets is an
   equivalence and the inclusion of edge sets is complemented.
-}
record SpanningTree {j k l : ULevel} (E : Type i) (V : Type j) ⦃ gph : Graph E V ⦄
    (E' : Type k) (V' : Type l) : Type (lmax (lmax i j) (lmax l k)) where
  field
    is-st : SubTree E V E' V'
  open SubTree is-st public
  field
    all-vertices : is-equiv inU
    is-complemented : E ≃ E' ⊔ Σ E (λ e → ¬ (hfiber inD e))
    inD-comm : inD ∼ (<– is-complemented) ∘ inl

module ExtendSpanningTree {j k l : ULevel} (E : Type i) (V : Type j) ⦃ gph : Graph E V ⦄
  (E' : Type k) (V' : Type l) (spantree : SpanningTree E V E' V') where

  open SpanningTree spantree

  ¬E' = Σ E (λ e → ¬ (hfiber (SubTree.inD is-st) e))

  instance
    gph-coprod : Graph (E' ⊔ ¬E') V'
    gph-coprod = record { π₀ = ⊔-rec π₀ λ e → is-equiv.g all-vertices (π₀ (<– is-complemented (inr e)))
                       ; π₁ = ⊔-rec π₁ λ e → is-equiv.g all-vertices (π₁ (<– is-complemented (inr e))) }

  inU-equiv : V' ≃ V
  inU-equiv = (inU , all-vertices)

  spantree-equiv : V / E ≃ V' / (E' ⊔ ¬E')
  spantree-equiv = (Coeq-emap inU-equiv (is-complemented ⁻¹)
                   (λ { (inl e') → ! (comm₀ e') ∙ ap π₀ (inD-comm e') ; (inr x) → <–-inv-r inU-equiv _})
                   λ { (inl e') → ! (comm₁ e') ∙ ap π₁ (inD-comm e') ; (inr x) → <–-inv-r inU-equiv _}) ⁻¹

composepp : {j k l : ULevel} {E' : Type j} {E : Type k} {V : Type l} ( inc : E' → E ) ⦃ gph : Graph E V ⦄ → Graph E' V
composepp inc ⦃ gph = gph ⦄ = record { π₀ = P.π₀ ∘ inc ; π₁ = P.π₁ ∘ inc }
    where
      module P = Graph gph

Fin-equiv-Unit : Fin 1 ≃ ⊤
Fin-equiv-Unit =
  Fin 1
    ≃⟨ Fin-equiv-Coprod ⟩
  Fin 0 ⊔ ⊤
    ≃⟨ ⊔-emap Fin-equiv-Empty (ide ⊤) ⟩
  ⊥ ⊔ ⊤
    ≃⟨ ⊔₁-Empty ⊤ ⟩
  ⊤
    ≃∎

compose-equiv-subtree-l : {j k l m n : ULevel} {E : Type i} {V : Type j} ⦃ gph : Graph E V ⦄
  (D : Type k) (U : Type l) (D' : Type m) (U' : Type n) → (D' ≃ D) → (U' ≃ U) →
  SubTree E V D U → SubTree E V D' U'

compose-equiv-subtree-l D U D' U' equivD equivU (subtree inD inU D-inj U-inj U-dec comm₀ comm₁) =
  subtree (inD ∘ –> equivD) (inU ∘ –> equivU) (∘-is-inj D-inj (–>-is-inj equivD)) (∘-is-inj U-inj (–>-is-inj equivU))
          (λ v → ⊔-rec (λ {(u , p) → inl ((<– equivU u) , (ap inU (<–-inv-r equivU u) ∙ p))})
                          (λ f → inr (λ {(u , p) → f ((–> equivU u) , p) })) (U-dec v))
          (λ d → comm₀ (–> equivD d) ∙ ap inU (! (<–-inv-r equivU _)))
          (λ d → comm₁ (–> equivD d) ∙ ap inU (! (<–-inv-r equivU _)))
  where
    instance
      gph' : Graph D' U'
      gph' = record { π₀ = λ d → <– equivU (π₀ (–> equivD d)) ; π₁ = λ d → <– equivU (π₁ (–> equivD d)) }

      c : is-contr (U' / D')
      c = equiv-preserves-level ((Coeq-emap equivU equivD (λ d → <–-inv-r equivU _) λ d → <–-inv-r equivU _) ⁻¹)

{- Since the vertex set is finite, we can build the spanning tree up a step at a time. -}
build-spanning-tree : (E : Type i) (n : ℕ) ⦃ gph : Graph E (Fin (S n)) ⦄ ⦃ conn : gph-is-connected gph ⦄ →
  (k : ℕ) → (k < S n) → ∥ SubTree E (Fin (S n)) (Fin k) (Fin (S k)) ∥

build-spanning-tree E n O l =
  [ compose-equiv-subtree-l _ _ _ _ Fin-equiv-Empty Fin-equiv-Unit t ]
  where
    instance
      ic : is-contr (⊤ / ⊥)
      ic = equiv-preserves-level (noedge-triv ⁻¹)

    t : SubTree E (Fin (S n)) ⊥ ⊤
    t = subtree ⊥-elim (λ _ → 0 , l) ⊥-elim (λ {unit unit _ → idp}) (λ v → ⊔-fmap (λ p → unit , (! p)) (λ {f (unit , p) → f (! p)}) (Fin-has-dec-eq v (0 , l)))
                ⊥-elim ⊥-elim

build-spanning-tree E n (S k) l =
  do
    ih ← (build-spanning-tree E n k (<-trans ltS l))
    let x = Fin-smaller-is-smaller l (SubTree.inU ih)
    t ← (extend-subtree E (Fin (S n)) Fin-has-dec-eq ih (fst x) (snd x))
    [ compose-equiv-subtree-l _ _ _ _ (⊔-sym ∘e Fin-equiv-Coprod) Fin-equiv-Coprod t ]

spanning-tree : (E : Type i) (Edec : has-dec-eq E) (n : ℕ) ⦃ gph : Graph E (Fin (S n)) ⦄ ⦃ conn : gph-is-connected gph ⦄ →
  ∥ SpanningTree E (Fin (S n)) (Fin n) (Fin (S n)) ∥

spanning-tree E Edec n = Trunc-fmap from-subtree (build-spanning-tree E _ _ ltS)
  where
    from-subtree : SubTree E (Fin (S n)) (Fin n) (Fin (S n)) → SpanningTree E (Fin (S n)) (Fin n) (Fin (S n))
    from-subtree st@(subtree ⦃ gphDU ⦄ inD inU D-inj U-inj U-dec comm₀ comm₁) =
      record
        { is-st = st
        ; all-vertices = Fin-inj-to-equiv inU U-inj
        ; is-complemented = dec-img-to-⊔ inD D-inj (Fin-hfiber-dec Edec inD) ⁻¹
        ; inD-comm = λ _ → idp
        }

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


text:
{-# OPTIONS --universe-polymorphism #-}
module SortDependingOnIndex where

open import Imports.Level

data Bad : (l : Level) → Set l where

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import LogicalFormulae
open import Orders.Total.Definition
open import Orders.Total.Lemmas
open import Maybe
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Vectors

open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module KeyValue.LinearStore.Implementation {a b c} (keySet : Set a) (valueSet : Set b) (keyOrder : TotalOrder {_} keySet {c}) where

record ReducedMap (min : keySet) : Set (a ⊔ b ⊔ c)
record ReducedMap min where
  inductive
  field
    firstEntry : valueSet
    next : Maybe (Sg keySet (λ nextKey → (ReducedMap nextKey) && (TotalOrder._<_ keyOrder min nextKey)))

addReducedMap : {min : keySet} → (k : keySet) → (v : valueSet) → (m : ReducedMap min) → ReducedMap (TotalOrder.min keyOrder min k)
addReducedMap {min} k v m with TotalOrder.totality keyOrder min k
addReducedMap {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) = record { firstEntry = firstEntry ; next = yes (k , (record { firstEntry = v ; next = no} ,, min<k))}
addReducedMap {min} k v record { firstEntry = minVal ; next = yes (nextKey , (m ,, pr)) } | inl (inl min<k) = record { firstEntry = minVal ; next = yes ((TotalOrder.min keyOrder nextKey k) , (addReducedMap {_} k v m ,, minFromBoth keyOrder pr min<k))}
addReducedMap {min} k v record { firstEntry = firstEntry ; next = next } | inl (inr k<min) = record { firstEntry = v ; next = yes (min , (record { firstEntry = firstEntry ; next = next } ,, k<min)) }
addReducedMap {min} k v record { firstEntry = firstEntry ; next = next } | inr min=k rewrite min=k = record { firstEntry = v ; next = next }

lookupReduced : {min : keySet} → (m : ReducedMap min) → (target : keySet) → Maybe valueSet
lookupReduced {min} m k with TotalOrder.totality keyOrder min k
lookupReduced {min} record { firstEntry = firstEntry ; next = no } k | inl (inl min<k) = no
lookupReduced {min} record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, _))) } k | inl (inl min<k) = lookupReduced {newMin} m k
lookupReduced {min} m k | inl (inr k<min) = no
lookupReduced {min} record { firstEntry = firstEntry ; next = next } k | inr min=k = yes firstEntry

countReduced : {min : keySet} → (m : ReducedMap min) → ℕ
countReduced record { firstEntry = firstEntry ; next = no } = 1
countReduced record { firstEntry = firstEntry ; next = (yes (key , (m ,, pr))) } = succ (countReduced m)

lookupReducedSucceedsAfterAdd : {min : keySet} → (k : keySet) → (v : valueSet) → (m : ReducedMap min) → (lookupReduced (addReducedMap k v m) k ≡ yes v)
lookupReducedSucceedsAfterAdd {min} k v m with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) with TotalOrder.totality keyOrder k k
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inl _) | inr p = refl
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = no } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder min<k)
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inl _) = lookupReducedSucceedsAfterAdd k v m
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
lookupReducedSucceedsAfterAdd {min} k v record { firstEntry = firstEntry ; next = (yes (newMin , (m ,, pr))) } | inl (inl min<k) | inr min=k rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder min<k)
lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) with TotalOrder.totality keyOrder k k
lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
lookupReducedSucceedsAfterAdd {min} k v m | inl (inr k<min) | inr p = refl
lookupReducedSucceedsAfterAdd {min} k v m | inr min=k with TotalOrder.totality keyOrder k k
lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inr p with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inr p | inl (inl min<k) rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder min<k)
lookupReducedSucceedsAfterAdd {min} k v m | inr min=k | inr p | inl (inr k<min) rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder k<min)
lookupReducedSucceedsAfterAdd {.k} k v record { firstEntry = firstEntry ; next = next } | inr refl | inr p | inr s = refl

lookupReducedSucceedsAfterUnrelatedAdd : {min : keySet} → (unrelatedK : keySet) → (unrelatedV : valueSet) → (k : keySet) → (v : valueSet) → ((TotalOrder._<_ keyOrder unrelatedK k) || (TotalOrder._<_ keyOrder k unrelatedK)) → (m : ReducedMap min) → (lookupReduced m k ≡ yes v) → lookupReduced (addReducedMap unrelatedK unrelatedV m) k ≡ yes v
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds with TotalOrder.totality keyOrder min k'
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inl min<k') with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr record { firstEntry = firstEntry ; next = no } () | inl (inl min<k') | inl (inl min<k)
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inl min<k') | inl (inl min<k) = lookupReducedSucceedsAfterUnrelatedAdd {a} k' v' k v pr fst lookupReducedSucceeds
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min (TotalOrder.<Transitive keyOrder min<k' x)))
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr k<k') m () | inl (inl min<k') | inl (inr k<min)
lookupReducedSucceedsAfterUnrelatedAdd {.min} k' v' min v (inl x) m lookupReducedSucceeds | inl (inl min<k') | inr refl = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder x min<k'))
lookupReducedSucceedsAfterUnrelatedAdd {.min} k' v' min v (inr x) record { firstEntry = v2 ; next = no } p | inl (inl min<k') | inr refl = applyEquality yes (yesInjective p)
lookupReducedSucceedsAfterUnrelatedAdd {.min} k' v' min v (inr x) record { firstEntry = .v ; next = (yes (a , b)) } refl | inl (inl min<k') | inr refl = applyEquality yes refl
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) with TotalOrder.totality keyOrder k' k
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inl (inl min<k) = lookupReducedSucceeds
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m () | inl (inr k'<min) | inl (inl k'<k) | inl (inr k<min)
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inl (inr k'<min) | inl (inl k'<k) | inr refl = lookupReducedSucceeds
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder x k<k'))
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder x (TotalOrder.<Transitive keyOrder k<k' k'<min)))
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr _) m () | inl (inr k'<min) | inl (inr k<k') | inl (inr x)
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr _) m lookupReducedSucceeds | inl (inr k'<min) | inl (inr k<k') | inr x rewrite x = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<k' k'<min))
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inl x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v (inr x) m lookupReducedSucceeds | inl (inr k'<min) | inr k'=k rewrite k'=k = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedSucceedsAfterUnrelatedAdd {min} k' v' k v pr m lookupReducedSucceeds | inr refl with TotalOrder.totality keyOrder min k
lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = no } () | inr refl | inl (inl min<k)
lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inl _) record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inr refl | inl (inl min<k) = lookupReducedSucceeds
lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inr x) m lookupReducedSucceeds | inr refl | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k x))
lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inl x) m () | inr refl | inl (inr k<min)
lookupReducedSucceedsAfterUnrelatedAdd {k'} k' v' k v (inr x) m () | inr refl | inl (inr k<min)
lookupReducedSucceedsAfterUnrelatedAdd {.min} .min v' min v (inl x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedSucceedsAfterUnrelatedAdd {.min} .min v' min v (inr x) m lookupReducedSucceeds | inr refl | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)

lookupReducedFailsAfterUnrelatedAdd : {min : keySet} → (unrelatedK : keySet) → (unrelatedV : valueSet) → (k : keySet) → ((TotalOrder._<_ keyOrder unrelatedK k) || (TotalOrder._<_ keyOrder k unrelatedK)) → (m : ReducedMap min) → (lookupReduced m k ≡ no) → lookupReduced (addReducedMap unrelatedK unrelatedV m) k ≡ no
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails with TotalOrder.totality keyOrder min k'
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inl min<k') with TotalOrder.totality keyOrder min k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) with TotalOrder.totality keyOrder k' k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inl (inl x) = refl
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inl (inr x) = refl
lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inl x) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inl min<k') | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedFails | inl (inl min<k') | inl (inl min<k) = lookupReducedFailsAfterUnrelatedAdd k' v' k pr fst lookupReducedFails
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inl min<k') | inl (inr k<min) = refl
lookupReducedFailsAfterUnrelatedAdd {.min} k' v' min pr m () | inl (inl min<k') | inr refl
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) with TotalOrder.totality keyOrder min k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) with TotalOrder.totality keyOrder k' k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl x₁) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = refl
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl x₁) record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = lookupReducedFails
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inr x₁) record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = refl
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inr x₁) record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inl _) = lookupReducedFails
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inl (inr x) = refl
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inl k'<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder min<k)
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inl (inr k<k') = refl
lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inl x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inr x) record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr k'<min) | inl (inl min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) with TotalOrder.totality keyOrder k' k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) with TotalOrder.totality keyOrder min k
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min min<k))
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inl (inr k<min') = refl
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inl _) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder k<min)
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inl k'<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k'<k x))
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inl (inr k<k') = refl
lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inl x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedFailsAfterUnrelatedAdd {min} .k v' k (inr x) m lookupReducedFails | inl (inr k'<min) | inl (inr k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder x)
lookupReducedFailsAfterUnrelatedAdd {min} k' v' k pr m () | inl (inr k'<min) | inr min=k
lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min k
lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr record { firstEntry = firstEntry ; next = no } lookupReducedFails | inr refl | inl (inl min<k) = refl
lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedFails | inr refl | inl (inl min<k) = lookupReducedFails
lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr m lookupReducedFails | inr refl | inl (inr k<min) = refl
lookupReducedFailsAfterUnrelatedAdd {min} .min v' k pr m () | inr refl | inr min=k

countReducedBehavesWhenAddingNotPresent : {min : keySet} → (k : keySet) → (v : valueSet) → (m : ReducedMap min) → (lookupReduced m k ≡ no) → countReduced (addReducedMap k v m) ≡ succ (countReduced m)
countReducedBehavesWhenAddingNotPresent {min} k v m lookupReducedFails with TotalOrder.totality keyOrder k min
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) with TotalOrder.totality keyOrder min k
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inl (inr _) = refl
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inl k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder k<min)
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) with TotalOrder.totality keyOrder min k
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = no } lookupReducedFails | inl (inr min<k) | inl (inl _) = refl
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedFails | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingNotPresent k v (_&&_.fst b) lookupReducedFails)
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inl (inr k<min) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder min<k k<min))
countReducedBehavesWhenAddingNotPresent {min} k v record { firstEntry = firstEntry ; next = next } lookupReducedFails | inl (inr min<k) | inr refl = exFalso (TotalOrder.irreflexive keyOrder min<k)
countReducedBehavesWhenAddingNotPresent {min} k v m lookupReducedFails | inr refl with TotalOrder.totality keyOrder min min
countReducedBehavesWhenAddingNotPresent {k} k v m lookupReducedFails | inr refl | inl (inl min<min) = exFalso (TotalOrder.irreflexive keyOrder min<min)
countReducedBehavesWhenAddingNotPresent {k} k v m lookupReducedFails | inr refl | inl (inr min<min) = exFalso (TotalOrder.irreflexive keyOrder min<min)
countReducedBehavesWhenAddingNotPresent {k} k v record { firstEntry = firstEntry ; next = no } () | inr refl | inr p
countReducedBehavesWhenAddingNotPresent {k} k v record { firstEntry = firstEntry ; next = (yes x) } () | inr refl | inr p

countReducedBehavesWhenAddingPresent : {min : keySet} → (k : keySet) → (v v' : valueSet) → (m : ReducedMap min) → (lookupReduced m k ≡ yes v') → countReduced (addReducedMap k v m) ≡ countReduced m
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds with TotalOrder.totality keyOrder k min
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inl k<min) with TotalOrder.totality keyOrder min k
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min min<k))
countReducedBehavesWhenAddingPresent {min} k v v' m () | inl (inl k<min) | inl (inr _)
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inl k<min) | inr q = exFalso (TotalOrder.irreflexive keyOrder (identityOfIndiscernablesLeft (TotalOrder._<_ keyOrder) k<min (equalityCommutative q)))
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inr min<k) with TotalOrder.totality keyOrder min k
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } () | inl (inr min<k) | inl (inl _)
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } lookupReducedSucceeds | inl (inr min<k) | inl (inl _) = applyEquality succ (countReducedBehavesWhenAddingPresent k v v' fst lookupReducedSucceeds)
countReducedBehavesWhenAddingPresent {min} k v v' m () | inl (inr min<k) | inl (inr k<min)
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inl (inr min<k) | inr q = exFalso (TotalOrder.irreflexive keyOrder (identityOfIndiscernablesLeft (λ a b → TotalOrder._<_ keyOrder a b) min<k q))
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inr q with TotalOrder.totality keyOrder min min
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inr q | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
countReducedBehavesWhenAddingPresent {min} k v v' m lookupReducedSucceeds | inr q | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } lookupReducedSucceeds | inr _ | inr p with TotalOrder.totality keyOrder min k
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } () | inr _ | inr p | inl (inl x)
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = no } () | inr _ | inr p | inl (inr x`)
countReducedBehavesWhenAddingPresent {.k} k v v' record { firstEntry = firstEntry ; next = no } lookupReducedSucceeds | inr q | inr p | inr refl = refl
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p with TotalOrder.totality keyOrder k k
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , b)) } lookupReducedSucceeds | inr q | inr p | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
countReducedBehavesWhenAddingPresent {min} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr q1 | inr p | inr x with TotalOrder.totality keyOrder min k
countReducedBehavesWhenAddingPresent {.k} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr refl | inr p | inr x | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder min<k)
countReducedBehavesWhenAddingPresent {.k} k v v' record { firstEntry = firstEntry ; next = (yes (a , (m ,, pr))) } q | inr q1 | inr p | inr x | inr refl = refl

data Map : Set (a ⊔ b ⊔ c) where
  empty : Map
  nonempty : {min : keySet} → ReducedMap min → Map

addMap : (m : Map) → (k : keySet) → (v : valueSet) → Map
addMap empty k v = nonempty {min = k} record { firstEntry = v ; next = no }
addMap (nonempty x) k v = nonempty (addReducedMap k v x)

lookup : (m : Map) → (target : keySet) → Maybe valueSet
lookup empty t = no
lookup (nonempty x) t = lookupReduced x t

count : (m : Map) → ℕ
count empty = 0
count (nonempty x) = countReduced x

keysReduced : {min : keySet} → (m : ReducedMap min) → Vec keySet (countReduced m)
keysReduced {min = min} record { firstEntry = firstEntry ; next = no } = min ,- []
keysReduced {min = min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } = min ,- (keysReduced fst)

keys : (m : Map) → Vec keySet (count m)
keys empty = []
keys (nonempty m) = keysReduced m

lookupReducedWhenLess : {min : keySet} → (m : ReducedMap min) → (k : keySet) → (TotalOrder._<_ keyOrder k min) → (lookupReduced m k ≡ no)
lookupReducedWhenLess {min} m k k<min with TotalOrder.totality keyOrder min k
lookupReducedWhenLess {min} m k k<min | inl (inl min<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min min<k))
lookupReducedWhenLess {min} m k k<min | inl (inr _) = refl
lookupReducedWhenLess {min} m k k<min | inr min=k rewrite min=k = exFalso (TotalOrder.irreflexive keyOrder k<min)

lookupCertainReduced : {min : keySet} → (m : ReducedMap min) → (k : keySet) → (vecContains (keysReduced m) k) → Sg valueSet (λ v → lookupReduced m k ≡ yes v)
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = no } k pr = firstEntry , q
  where
    t : min ≡ k
    t = vecSolelyContains k pr
    q : lookupReduced {min} (record { firstEntry = firstEntry ; next = no }) k ≡ yes firstEntry
    q with TotalOrder.totality keyOrder k k
    q | inl (inl k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
    q | inl (inr k<k) = exFalso (TotalOrder.irreflexive keyOrder k<k)
    q | inr p with TotalOrder.totality keyOrder min k
    q | inr p | inl (inl min<k) rewrite t = exFalso (TotalOrder.irreflexive keyOrder min<k)
    q | inr p | inl (inr k<min) rewrite t = exFalso (TotalOrder.irreflexive keyOrder k<min)
    q | inr p | inr x = refl
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr with TotalOrder.totality keyOrder min k
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inl min<k) rewrite isHere = exFalso (TotalOrder.irreflexive keyOrder min<k)
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inl min<k) = lookupCertainReduced fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = zero ; index<m = _ ; isHere = isHere } | inl (inr k<min) rewrite isHere = exFalso (TotalOrder.irreflexive keyOrder k<min)
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) with TotalOrder.totality keyOrder a k
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inl a<k) = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder k<min (TotalOrder.<Transitive keyOrder snd a<k)))
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inl (inr k<a) = exFalso h
  where
    f : Sg valueSet (λ v → lookupReduced fst k ≡ yes v)
    f = lookupCertainReduced fst k record { index = index ; index<m = canRemoveSuccFrom<N index<m ; isHere = isHere }
    g : lookupReduced fst k ≡ no
    g = lookupReducedWhenLess fst k k<a
    noIsNotYes : {a : _} → {A : Set a} → {b : A} → (no ≡ yes b) → False
    noIsNotYes {a} {A} {b} ()
    h : False
    h with f
    h | a , b rewrite g = noIsNotYes b
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k record { index = (succ index) ; index<m = index<m ; isHere = isHere } | inl (inr k<min) | inr refl = exFalso (TotalOrder.irreflexive keyOrder (TotalOrder.<Transitive keyOrder snd k<min))
lookupCertainReduced {min} record { firstEntry = firstEntry ; next = (yes (a , (fst ,, snd))) } k pr | inr min=k = firstEntry , refl

lookupCertain : (m : Map) → (k : keySet) → (vecContains (keys m) k) → Sg valueSet (λ v → lookup m k ≡ yes v)
lookupCertain empty k record { index = index ; index<m = (le x ()) ; isHere = isHere }
lookupCertain (nonempty {min} m) k pr = lookupCertainReduced {min} m k pr


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

open import HoTT
open import homotopy.PtdAdjoint

module homotopy.SuspAdjointLoop where

module Σ⊣Ω {i} where

  SuspFunctor : PtdFunctor i i
  SuspFunctor = record {
    obj = ⊙Susp;
    arr = ⊙susp-fmap;
    id = ⊙susp-fmap-idf;
    comp = ⊙susp-fmap-∘}

  LoopFunctor : PtdFunctor i i
  LoopFunctor = record {
    obj = ⊙Ω;
    arr = ⊙ap;
    id = λ _ → ⊙ap-idf;
    comp = ⊙ap-∘}

  module _ (X : Ptd i) where

    η : fst X → Ω (⊙Susp X)
    η x = merid _ x ∙ ! (merid _ (snd X))

    module E = SuspensionRec (Ω X) (snd X) (snd X) (idf _)

    ε : fst (⊙Susp (⊙Ω X)) → fst X
    ε = E.f

    ⊙η : fst (X ⊙→ ⊙Ω (⊙Susp X))
    ⊙η = (η , !-inv-r (merid _ (snd X)))

    ⊙ε : fst (⊙Susp (⊙Ω X) ⊙→ X)
    ⊙ε = (ε , idp)

  η-natural : {X Y : Ptd i} (f : fst (X ⊙→ Y))
    → ⊙η Y ⊙∘ f == ⊙ap (⊙susp-fmap f) ⊙∘ ⊙η X
  η-natural {X = X} (f , idp) = ⊙λ=
    (λ x → ! $
      ap-∙ (susp-fmap f) (merid _ x) (! (merid _ (snd X)))
      ∙ SuspFmap.glue-β f x
        ∙2 (ap-! (susp-fmap f) (merid _ (snd X))
            ∙ ap ! (SuspFmap.glue-β f (snd X))))
    (pt-lemma (susp-fmap f) (merid _ (snd X)) (SuspFmap.glue-β f (snd X)))
    where
    pt-lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
      {x y : A} (p : x == y) {q : f x == f y} (α : ap f p == q)
      → !-inv-r q == (! $ ap-∙ f p (! p) ∙ α ∙2 (ap-! f p ∙ ap ! α))
                     ∙ ap (ap f) (!-inv-r p) ∙ idp
    pt-lemma f idp idp = idp

  ε-natural : {X Y : Ptd i} (f : fst (X ⊙→ Y))
    → ⊙ε Y ⊙∘ ⊙susp-fmap (⊙ap f) == f ⊙∘ ⊙ε X
  ε-natural (f , idp) = ⊙λ=
    (SuspensionElim.f _ idp idp
      (λ p → ↓-='-from-square $ vert-degen-square $
        ap-∘ (ε _) (susp-fmap (ap f)) (merid _ p)
        ∙ ap (ap (ε _)) (SuspFmap.glue-β (ap f) p)
        ∙ E.glue-β _ (ap f p)
        ∙ ap (ap f) (! (E.glue-β _ p))
        ∙ ∘-ap f (ε _) (merid _ p)))
    idp

  εΣ-Ση : (X : Ptd i) → ⊙ε (⊙Susp X) ⊙∘ ⊙susp-fmap (⊙η X) == ⊙idf _
  εΣ-Ση X = ⊙λ=
    (SuspensionElim.f _
      idp
      (merid _ (snd X))
      (λ x → ↓-='-from-square $
        (ap-∘ (ε (⊙Susp X)) (susp-fmap (η X)) (merid _ x)
         ∙ ap (ap (ε (⊙Susp X))) (SuspFmap.glue-β (η X) x)
         ∙ E.glue-β _ (merid _ x ∙ ! (merid _ (snd X))))
        ∙v⊡ square-lemma (merid _ x) (merid _ (snd X))
        ⊡v∙ ! (ap-idf (merid _ x))))
    idp
    where
    square-lemma : ∀ {i} {A : Type i} {x y z : A}
      (p : x == y) (q : z == y)
      → Square idp (p ∙ ! q) p q
    square-lemma idp idp = ids

  Ωε-ηΩ : (X : Ptd i) → ⊙ap (⊙ε X) ⊙∘ ⊙η (⊙Ω X) == ⊙idf _
  Ωε-ηΩ X = ⊙λ=
    (λ p → ap-∙ (ε X) (merid _ p) (! (merid _ idp))
         ∙ (E.glue-β X p ∙2 (ap-! (ε X) (merid _ idp) ∙ ap ! (E.glue-β X idp)))
         ∙ ∙-unit-r _)
    (pt-lemma (ε X) (merid _ idp) (E.glue-β X idp))
    where
    pt-lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
      {x y : A} (p : x == y) {q : f x == f y} (α : ap f p == q)
      → ap (ap f) (!-inv-r p) ∙ idp
        == (ap-∙ f p (! p) ∙ (α ∙2 (ap-! f p ∙ ap ! α)) ∙ !-inv-r q) ∙ idp
    pt-lemma f idp idp = idp

  adj : CounitUnitAdjoint SuspFunctor LoopFunctor
  adj = record {
    η = ⊙η;
    ε = ⊙ε;

    η-natural = η-natural;
    ε-natural = ε-natural;

    εF-Fη = εΣ-Ση;
    Gε-ηG = Ωε-ηΩ}

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module EvenOdd where

open import Data.Nat

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

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

_e+e_ : {n m : ℕ} → Even n → Even m → Even (n + m)
evenZero e+e b = b
evenSuc a e+e b = evenSuc (a e+e b)

_o+o_ : {n m : ℕ} → Odd n → Odd m → Even (n + m)
oddOne o+o oddOne = evenSuc evenZero
oddOne o+o oddSuc b = evenSuc (oddOne o+o b)
oddSuc a o+o b = evenSuc (a o+o b)

_o+e_ : {n m : ℕ} → Odd n → Even m → Odd (n + m)
oddOne o+e evenZero = oddOne
oddOne o+e evenSuc b = oddSuc (oddOne o+e b)
oddSuc a o+e b = oddSuc (a o+e b)

_e+o_ : {n m : ℕ} → Even n → Odd m → Odd (n + m)
evenZero e+o b = b
evenSuc a e+o b = oddSuc (a e+o b)


text:
-- {-# OPTIONS -v tc.meta:40 #-}
-- {-# OPTIONS --verbose tc.conv.term:40 #-}
-- {-# OPTIONS --verbose tc.conv.level:40 #-}
-- {-# OPTIONS --verbose tc.conv.atom:50 #-}
-- {-# OPTIONS --verbose tc.conv.elim:50 #-}

module Issue680-NeutralLevels where

open import Common.Level

postulate
  N     : Set
  A     : N → Set
  level : N → Level
  lac   : ∀ {n} → A n → N
  I     : Level → Level → Set
  refl  : ∀ {l : Level} → I l l

data Test : Set where
  mkTest : (n : N) → (tel : A n) → Test

test : Test → N
test (mkTest n tel) = n
  where
    test′ : I (lsuc (level (lac tel)))
              (lsuc (level (lac tel)))
    test′ = refl


text:
module sum where

open import level
open import bool
open import eq
open import maybe
open import product
open import functions
open import empty public

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data _⊎_ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

_∨_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
_∨_ = _⊎_

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixr 1 _⊎_ _∨_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

_≫=⊎_ : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{C : Set (ℓ ⊔ ℓ')}  → A ⊎ B → (B → A ⊎ C) → A ⊎ C
inj₁ x ≫=⊎ f = inj₁ x
inj₂ x ≫=⊎ f = f x

return⊎ : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → B → A ⊎ B
return⊎ b = inj₂ b

infix 5 error⊎_

error⊎_ : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → A → A ⊎ B
error⊎_ a = inj₁ a

extract-inj₁≡ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'}{a a' : A} → inj₁{B = B} a ≡ inj₁ a' → a ≡ a'
extract-inj₁≡ refl = refl

extract-inj₂≡ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'}{b b' : B} → inj₂{A = A} b ≡ inj₂ b' → b ≡ b'
extract-inj₂≡ refl = refl

=⊎ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'} → (A → A → 𝔹) → (B → B → 𝔹) → A ⊎ B → A ⊎ B → 𝔹
=⊎ eqa eqb (inj₁ a) (inj₁ a') = eqa a a'
=⊎ eqa eqb (inj₂ b) (inj₂ b') = eqb b b'
=⊎ _ _ _ _ = ff

=⊎-to-≡ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'} → (_eqa_ : A → A → 𝔹) → (_eqb_ : B → B → 𝔹) → ((a a' : A) → (a eqa a' ≡ tt) → a ≡ a') → ((b b' : B) → (b eqb b' ≡ tt) → b ≡ b') →  (x y : A ⊎ B) → =⊎ _eqa_ _eqb_ x y  ≡ tt → x ≡ y
=⊎-to-≡ eqa eqb risea riseb (inj₁ a) (inj₁ a') p rewrite risea a a' p = refl
=⊎-to-≡ eqa eqb risea riseb (inj₂ b) (inj₂ b') p rewrite riseb b b' p = refl
=⊎-to-≡ eqa eqb risea riseb (inj₁ a) (inj₂ b) ()
=⊎-to-≡ eqa eqb risea riseb (inj₂ b) (inj₁ a) ()

≡⊎-to-= : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'} → (_eqa_ : A → A → 𝔹) → (_eqb_ : B → B → 𝔹) → ((a a' : A) → a ≡ a' → a eqa a' ≡ tt) → ((b b' : B) → b ≡ b' → b eqb b' ≡ tt) →  (x y : A ⊎ B) → x ≡ y → =⊎ _eqa_ _eqb_ x y  ≡ tt
≡⊎-to-= eqa eqb dropa dropb (inj₁ a) (inj₁ a') p = dropa a a' (extract-inj₁≡ p)
≡⊎-to-= eqa eqb dropa dropb (inj₂ b) (inj₂ b') p = dropb b b' (extract-inj₂≡ p)
≡⊎-to-= eqa eqb dropa dropb (inj₁ a) (inj₂ b) ()
≡⊎-to-= eqa eqb dropa dropb (inj₂ b) (inj₁ a) ()

⊎-assoc : ∀{ℓ}{U V W : Set ℓ} → U ⊎ V ⊎ W → (U ⊎ V) ⊎ W
⊎-assoc (inj₁ x) = inj₁ (inj₁ x)
⊎-assoc (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
⊎-assoc (inj₂ (inj₂ y)) = inj₂ y

⊎-assoc-inv : ∀{ℓ}{U V W : Set ℓ} → (U ⊎ V) ⊎ W → U ⊎ V ⊎ W
⊎-assoc-inv (inj₁ (inj₁ x)) = inj₁ x
⊎-assoc-inv (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
⊎-assoc-inv (inj₂ y) = inj₂ (inj₂ y)

⊎-ar : ∀{ℓ}{U V W : Set ℓ} → (U → W) → (V → W) → U ⊎ V → W
⊎-ar f g (inj₁ x) = f x
⊎-ar f g (inj₂ y) = g y

⊎-sym : ∀{ℓ}{X Y : Set ℓ} → X ⊎ Y → Y ⊎ X
⊎-sym (inj₁ x) = inj₂ x
⊎-sym (inj₂ y) = inj₁ y

⊎-left-ident : ∀{ℓ}{X : Set ℓ} → ⊥ {ℓ} ⊎ X → X
⊎-left-ident (inj₁ x) = ⊥-elim x
⊎-left-ident (inj₂ y) = y

⊎-left-ident-inv : ∀{ℓ}{X : Set ℓ} → X → ⊥ {ℓ} ⊎ X
⊎-left-ident-inv = inj₂

⊎-right-ident : ∀{ℓ}{X : Set ℓ} → X ⊎ ⊥ {ℓ} → X
⊎-right-ident (inj₁ x) = x
⊎-right-ident (inj₂ y) = ⊥-elim y

⊎-right-ident-inv : ∀{ℓ}{X : Set ℓ} → X → X ⊎ ⊥ {ℓ}
⊎-right-ident-inv = inj₁

⊎-map : {U W V R : Set} → (U → V) → (W → R) → U ⊎ W → V ⊎ R
⊎-map {U} {W} {V} {R} f g (inj₁ u) = inj₁ (f u)
⊎-map {U} {W} {V} {R} f g (inj₂ w) = inj₂ (g w)

⊎-×-distl : {U V W : Set} → U × (V ⊎ W) → U × V ⊎ U × W
⊎-×-distl {U} {V} {W} (u , inj₁ v) = inj₁ (u , v)
⊎-×-distl {U} {V} {W} (u , inj₂ w) = inj₂ (u , w)

⊎-×-distl-inv : {X Y Z : Set} → X × Y ⊎ X × Z → X × (Y ⊎ Z)
⊎-×-distl-inv {X} {Y} {Z} (inj₁ (x , y)) = x , inj₁ y
⊎-×-distl-inv {X} {Y} {Z} (inj₂ (x , z)) = x , inj₂ z

⊎-×-distl-iso₁ : ∀{U V W}{a : U × (V ⊎ W)} → (⊎-×-distl-inv ∘ ⊎-×-distl) a ≡ id a
⊎-×-distl-iso₁ {a = u , inj₁ v} = refl
⊎-×-distl-iso₁ {a = u , inj₂ w} = refl

⊎-×-distl-iso₂ : ∀{U V W}{a : U × V ⊎ U × W} → (⊎-×-distl ∘ ⊎-×-distl-inv) a ≡ id a
⊎-×-distl-iso₂ {a = inj₁ (u , v)} = refl
⊎-×-distl-iso₂ {a = inj₂ (u , w)} = refl

⊎-×-distr : {U V W : Set} → (U ⊎ V) × W → U × W ⊎ V × W
⊎-×-distr {U} {V} {W} (inj₁ u , w) = inj₁ (u , w)
⊎-×-distr {U} {V} {W} (inj₂ v , w) = inj₂ (v , w)

⊎-×-distr-inv : {X Z Y : Set} → X × Z ⊎ Y × Z → (X ⊎ Y) × Z
⊎-×-distr-inv {X} {Z} {Y} (inj₁ (x , z)) = inj₁ x , z
⊎-×-distr-inv {X} {Z} {Y} (inj₂ (y , z)) = inj₂ y , z

⊎-×-distr-iso₁ : ∀{U V W}{a : (U ⊎ V) × W} → (⊎-×-distr-inv ∘ ⊎-×-distr) a ≡ id a
⊎-×-distr-iso₁ {a = inj₁ u , w} = refl
⊎-×-distr-iso₁ {a = inj₂ v , w} = refl

⊎-×-distr-iso₂ : ∀{U V W}{a : (U × W) ⊎ (V × W)} → (⊎-×-distr ∘ ⊎-×-distr-inv) a ≡ id a
⊎-×-distr-iso₂ {a = inj₁ (u , w)} = refl
⊎-×-distr-iso₂ {a = inj₂ (v , w)} = refl

⊎-codiag : ∀{ℓ : level}{U : Set ℓ} → U ⊎ U → U
⊎-codiag (inj₁ x) = x
⊎-codiag (inj₂ y) = y

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL