text:
module Data.BitVector.NumericOrder where

open import Data.Empty
open import Data.Sum
open import Data.Vec

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.Nat hiding (decTotalOrder; _≟_; _<_; _≤_; module _≤_; _≤?_; compare) renaming (zero to Nzero; suc to Nsuc)

open import Data.BitVector

open import Function

infix 4 _<_
infix 4 _≤_

mutual
  data _<_ : ∀ {n} → BitVector n → BitVector n → Set where
    b#<b# : ∀ {n} {x y : BitVector n} {b#} → (pf : x < y) → (b# ∷ x) < (b# ∷ y)

    0#<1# : ∀ {n} {x y : BitVector n} → (pf : x ≤ y) → (0# ∷ x) < (1# ∷ y)
    1#<0# : ∀ {n} {x y : BitVector n} → (pf : x < y) → (1# ∷ x) < (0# ∷ y)

  -- Silly agda bug is preventing me from using the _≤_ name even though it's not in scope :(
  data _≤_ : ∀ {n} → BitVector n → BitVector n → Set where
    []≤[] : [] ≤ []
    b#≤b# : ∀ {n} {x y : BitVector n} {b#} → (pf : x ≤ y) → (b# ∷ x) ≤ (b# ∷ y)

    0#≤1# : ∀ {n} {x y : BitVector n} → (pf : x ≤ y) → (0# ∷ x) ≤ (1# ∷ y)
    1#≤0# : ∀ {n} {x y : BitVector n} → (pf : x <  y) → (1# ∷ x) ≤ (0# ∷ y)

<-irr : ∀ {n} {x : BitVector n} → ¬ x < x
<-irr {0} ()
<-irr (b#<b# pf) = <-irr pf

≤-refl : ∀ {n} → _≡_ ⇒ (_≤_ {n})
≤-refl {0} {[]} refl = []≤[]
≤-refl {Nsuc n} {b# ∷ xs} refl = b#≤b# (≤-refl refl)

opposites : ∀ {n} {x y : BitVector n} → x ≤ y → y < x → ⊥
opposites []≤[] ()
opposites (b#≤b# pf₀) (b#<b# pf₁) = opposites pf₀ pf₁
opposites (0#≤1# pf₀) (1#<0# pf₁) = opposites pf₀ pf₁
opposites (1#≤0# pf₀) (0#<1# pf₁) = opposites pf₁ pf₀

≤-antisym : ∀ {n} → Antisymmetric _≡_ (_≤_ {n})
≤-antisym []≤[] q = refl
≤-antisym (b#≤b# pf₀) (b#≤b# pf₁) rewrite ≤-antisym pf₀ pf₁ = refl
≤-antisym (0#≤1# (b#≤b# pf₀)) (1#≤0# (b#<b# pf₁)) = ⊥-elim (opposites pf₀ pf₁)
≤-antisym (0#≤1# (1#≤0# pf₀)) (1#≤0# (0#<1# pf₁)) = ⊥-elim (opposites pf₁ pf₀)
≤-antisym (0#≤1# (0#≤1# pf₀)) (1#≤0# (1#<0# pf₁)) = ⊥-elim (opposites pf₀ pf₁)
≤-antisym (0#≤1# pf₀) (1#≤0# pf₁) = ⊥-elim (opposites pf₀ pf₁)
≤-antisym (1#≤0# pf₀) (0#≤1# pf₁) = ⊥-elim (opposites pf₁ pf₀)

mutual
  ≤-<-trans-< : ∀ {n} {x y z : BitVector n} → x ≤ y → y < z → x < z
  ≤-<-trans-< []≤[] ()
  ≤-<-trans-< (b#≤b# pf₀) (b#<b# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
  ≤-<-trans-< (b#≤b# pf₀) (0#<1# pf₁) = 0#<1# (≤-trans pf₀ pf₁)
  ≤-<-trans-< (b#≤b# pf₀) (1#<0# pf₁) = 1#<0# (≤-<-trans-< pf₀ pf₁)
  ≤-<-trans-< (0#≤1# pf₀) (b#<b# pf₁) = 0#<1# (≤-<-trans-≤ pf₀ pf₁)
  ≤-<-trans-< (0#≤1# pf₀) (1#<0# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
  ≤-<-trans-< (1#≤0# pf₀) (b#<b# pf₁) = 1#<0# (<-trans pf₀ pf₁)
  ≤-<-trans-< (1#≤0# pf₀) (0#<1# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)

  <-≤-trans-< : ∀ {n} {x y z : BitVector n} → x < y → y ≤ z → x < z
  <-≤-trans-< (b#<b# pf₀) (b#≤b# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)
  <-≤-trans-< (b#<b# pf₀) (0#≤1# pf₁) = 0#<1# (<-≤-trans-≤ pf₀ pf₁)
  <-≤-trans-< (b#<b# pf₀) (1#≤0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
  <-≤-trans-< (0#<1# pf₀) (b#≤b# pf₁) = 0#<1# (≤-trans pf₀ pf₁)
  <-≤-trans-< (0#<1# pf₀) (1#≤0# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
  <-≤-trans-< (1#<0# pf₀) (b#≤b# pf₁) = 1#<0# (<-≤-trans-< pf₀ pf₁)
  <-≤-trans-< (1#<0# pf₀) (0#≤1# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)

  ≤-<-trans-≤ : ∀ {n} {x y z : BitVector n} → x ≤ y → y < z → x ≤ z
  ≤-<-trans-≤ []≤[] ()
  ≤-<-trans-≤ (b#≤b# pf₀) (b#<b# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
  ≤-<-trans-≤ (b#≤b# pf₀) (0#<1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
  ≤-<-trans-≤ (b#≤b# pf₀) (1#<0# pf₁) = 1#≤0# (≤-<-trans-< pf₀ pf₁)
  ≤-<-trans-≤ (0#≤1# pf₀) (b#<b# pf₁) = 0#≤1# (≤-<-trans-≤ pf₀ pf₁)
  ≤-<-trans-≤ (0#≤1# pf₀) (1#<0# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
  ≤-<-trans-≤ (1#≤0# pf₀) (b#<b# pf₁) = 1#≤0# (<-trans pf₀ pf₁)
  ≤-<-trans-≤ (1#≤0# pf₀) (0#<1# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)

  <-≤-trans-≤ : ∀ {n} {x y z : BitVector n} → x < y → y ≤ z → x ≤ z
  <-≤-trans-≤ (b#<b# pf₀) (b#≤b# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)
  <-≤-trans-≤ (b#<b# pf₀) (0#≤1# pf₁) = 0#≤1# (<-≤-trans-≤ pf₀ pf₁)
  <-≤-trans-≤ (b#<b# pf₀) (1#≤0# pf₁) = 1#≤0# (<-trans pf₀ pf₁)
  <-≤-trans-≤ (0#<1# pf₀) (b#≤b# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
  <-≤-trans-≤ (0#<1# pf₀) (1#≤0# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
  <-≤-trans-≤ (1#<0# pf₀) (b#≤b# pf₁) = 1#≤0# (<-≤-trans-< pf₀ pf₁)
  <-≤-trans-≤ (1#<0# pf₀) (0#≤1# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)

  <-trans : ∀ {n} → Transitive (_<_ {n})
  <-trans (b#<b# pf₀) (b#<b# pf₁) = b#<b# (<-trans pf₀ pf₁)
  <-trans (b#<b# pf₀) (0#<1# pf₁) = 0#<1# (<-≤-trans-≤ pf₀ pf₁)
  <-trans (b#<b# pf₀) (1#<0# pf₁) = 1#<0# (<-trans pf₀ pf₁)
  <-trans (0#<1# pf₀) (b#<b# pf₁) = 0#<1# (≤-<-trans-≤ pf₀ pf₁)
  <-trans (0#<1# pf₀) (1#<0# pf₁) = b#<b# (≤-<-trans-< pf₀ pf₁)
  <-trans (1#<0# pf₀) (b#<b# pf₁) = 1#<0# (<-trans pf₀ pf₁)
  <-trans (1#<0# pf₀) (0#<1# pf₁) = b#<b# (<-≤-trans-< pf₀ pf₁)

  ≤-trans : ∀ {n} → Transitive (_≤_ {n})
  ≤-trans []≤[] []≤[] = []≤[]
  ≤-trans (b#≤b# pf₀) (b#≤b# pf₁) = b#≤b# (≤-trans pf₀ pf₁)
  ≤-trans (b#≤b# pf₀) (0#≤1# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
  ≤-trans (b#≤b# pf₀) (1#≤0# pf₁) = 1#≤0# (≤-<-trans-< pf₀ pf₁)
  ≤-trans (0#≤1# pf₀) (b#≤b# pf₁) = 0#≤1# (≤-trans pf₀ pf₁)
  ≤-trans (0#≤1# pf₀) (1#≤0# pf₁) = b#≤b# (≤-<-trans-≤ pf₀ pf₁)
  ≤-trans (1#≤0# pf₀) (b#≤b# pf₁) = 1#≤0# (<-≤-trans-< pf₀ pf₁)
  ≤-trans (1#≤0# pf₀) (0#≤1# pf₁) = b#≤b# (<-≤-trans-≤ pf₀ pf₁)

<⇒≤ : ∀ {n} {x y : BitVector n} → x < y → x ≤ y
<⇒≤ (b#<b# pf) = b#≤b# (<⇒≤ pf)
<⇒≤ (0#<1# pf) = 0#≤1# pf
<⇒≤ (1#<0# pf) = 1#≤0# pf

≤⇒≡⊎< : ∀ {n} → {x y : BitVector n} → x ≤ y → x ≡ y ⊎ x < y
≤⇒≡⊎< []≤[] = inj₁ refl
≤⇒≡⊎< (b#≤b# pf) with ≤⇒≡⊎< pf
...                 | inj₁ refl = inj₁ refl
...                 | inj₂ x<y = inj₂ (b#<b# x<y)
≤⇒≡⊎< (0#≤1# pf) = inj₂ (0#<1# pf)
≤⇒≡⊎< (1#≤0# pf) = inj₂ (1#<0# pf)

helper≢ : ∀ {n} {x y} {xs ys : BitVector n} → ¬ xs < ys → xs ≢ ys → ¬ x ∷ xs < y ∷ ys
helper≢ xs≮ys xs≢ys (b#<b# pf) = xs≮ys pf
helper≢ xs≮ys xs≢ys (1#<0# pf) = xs≮ys pf
helper≢ xs≮ys xs≢ys (0#<1# pf) with ≤⇒≡⊎< pf
...                               | inj₁ x≡y = xs≢ys x≡y
...                               | inj₂ x<y = xs≮ys x<y

helper≡ : ∀ {n} {xs : BitVector n} → ¬ 1# ∷ xs < 0# ∷ xs
helper≡ (1#<0# pf) = <-irr pf

compare : ∀ {n} → Trichotomous _≡_ (_<_ {n})
compare [] [] = tri≈ (λ ()) refl (λ ())
compare (x ∷ xs) (y ∷ ys) with compare xs ys
compare (0# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = tri< (b#<b# a)       (¬b ∘ cong tail) (helper≢ ¬c (¬b ∘ sym))
compare (0# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = tri< (0#<1# (<⇒≤ a)) (¬b ∘ cong tail) (helper≢ ¬c (¬b ∘ sym))
compare (1# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = tri< (1#<0# a)       (¬b ∘ cong tail) (helper≢ ¬c (¬b ∘ sym))
compare (1# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = tri< (b#<b# a)       (¬b ∘ cong tail) (helper≢ ¬c (¬b ∘ sym))
compare (0# ∷ xs) (0# ∷ ._) | tri≈ ¬a refl ¬c = tri≈ <-irr refl <-irr
compare (0# ∷ xs) (1# ∷ ._) | tri≈ ¬a refl ¬c = tri< (0#<1# (≤-refl refl)) (λ ()) helper≡
compare (1# ∷ xs) (0# ∷ ._) | tri≈ ¬a refl ¬c = tri> helper≡ (λ ()) (0#<1# (≤-refl refl))
compare (1# ∷ xs) (1# ∷ ._) | tri≈ ¬a refl ¬c = tri≈ <-irr refl <-irr
compare (0# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = tri> (helper≢ ¬a ¬b) (¬b ∘ cong tail) (b#<b# c)
compare (0# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = tri> (helper≢ ¬a ¬b) (λ ()) (1#<0# c)
compare (1# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = tri> (helper≢ ¬a ¬b) (λ ()) (0#<1# (<⇒≤ c))
compare (1# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = tri> (helper≢ ¬a ¬b) (¬b ∘ cong tail) (b#<b# c)

≤-total : ∀ {n} → Total (_≤_ {n})
≤-total [] [] = inj₁ []≤[]
≤-total (x  ∷ xs) (y  ∷ ys) with compare xs ys
≤-total (0# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = inj₁ (b#≤b# (<⇒≤ a))
≤-total (0# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = inj₁ (0#≤1# (<⇒≤ a))
≤-total (1# ∷ xs) (0# ∷ ys) | tri< a ¬b ¬c = inj₁ (1#≤0# a)
≤-total (1# ∷ xs) (1# ∷ ys) | tri< a ¬b ¬c = inj₁ (b#≤b# (<⇒≤ a))
≤-total (0# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (b#≤b# (≤-refl b))
≤-total (0# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (0#≤1# (≤-refl b))
≤-total (1# ∷ xs) (0# ∷ ys) | tri≈ ¬a b ¬c = inj₂ (0#≤1# (≤-refl (sym b)))
≤-total (1# ∷ xs) (1# ∷ ys) | tri≈ ¬a b ¬c = inj₁ (b#≤b# (≤-refl b))
≤-total (0# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = inj₂ (b#≤b# (<⇒≤ c))
≤-total (0# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = inj₂ (1#≤0# c)
≤-total (1# ∷ xs) (0# ∷ ys) | tri> ¬a ¬b c = inj₂ (0#≤1# (<⇒≤ c))
≤-total (1# ∷ xs) (1# ∷ ys) | tri> ¬a ¬b c = inj₂ (b#≤b# (<⇒≤ c))

_≤?_ : ∀ {n} → Decidable (_≤_ {n})
x ≤? y with compare x y
...       | tri< a ¬b ¬c = yes (<⇒≤ a)
...       | tri≈ ¬a b ¬c = yes (≤-refl b)
...       | tri> ¬a ¬b c = no  helper
  where helper : ¬ x ≤ y
        helper x≤y with ≤⇒≡⊎< x≤y
        ...           | inj₁ x≡y = ¬b x≡y
        ...           | inj₂ x<y = ¬a x<y

decTotalOrder : ∀ {n} → DecTotalOrder _ _ _
decTotalOrder {n} = record
  { Carrier         = BitVector n
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = record
      { isTotalOrder = record
        { isPartialOrder = record
          { isPreorder = record
              { isEquivalence = isEquivalence
              ; reflexive     = ≤-refl
              ; trans         = ≤-trans
              }
            ; antisym  = ≤-antisym
            }
            ; total = ≤-total
            }
          ; _≟_  = _≟_
          ; _≤?_ = _≤?_
          }
    }

strictTotalOrder : ∀ {n} → StrictTotalOrder _ _ _
strictTotalOrder {n} = record
  { Carrier            = BitVector n
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = record
      { isEquivalence = isEquivalence
      ; trans         = <-trans
      ; compare       = compare
      }
  }

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


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

open import Prelude
open import Relation.Binary
open import Function.Injective

module Relation.Binary.Construct.On
  {a b ℓ₁ ℓ₂} {A : Type a} {B : Type b}
  (f : A → B) (f-inj : Injective f)
  (ord : TotalOrder B ℓ₁ ℓ₂)
  where

open TotalOrder ord renaming (refl to ≤-refl)

_<′_ : A → A → Type _
x <′ y = f x < f y

_≤′_ : A → A → Type _
x ≤′ y = f x ≤ f y

on-ord : TotalOrder A ℓ₁ ℓ₂
StrictPreorder._<_   (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder on-ord)) = _<′_
StrictPreorder.trans (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder on-ord)) = <-trans
StrictPreorder.irrefl  (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder on-ord)) = irrefl
StrictPartialOrder.conn (TotalOrder.strictPartialOrder on-ord) p q = f-inj _ _ (conn p q)
Preorder._≤_   (PartialOrder.preorder (TotalOrder.partialOrder on-ord)) = _≤′_
Preorder.refl  (PartialOrder.preorder (TotalOrder.partialOrder on-ord)) = ≤-refl
Preorder.trans (PartialOrder.preorder (TotalOrder.partialOrder on-ord)) = ≤-trans
PartialOrder.antisym (TotalOrder.partialOrder on-ord) p q = f-inj _ _ (antisym p q)
TotalOrder._<?_ on-ord x y = f x <? f y
TotalOrder.≰⇒> on-ord = ≰⇒>
TotalOrder.≮⇒≥ on-ord = ≮⇒≥

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2015-06-17
-- Postponing checkArguments dropped already inserted implicit arguments.

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.def.alias:100 -v tc.decl:10 -v tc.term.expr:20 -v tc.data.con:20 #-}
-- {-# OPTIONS  -v tc.meta.assign:10 #-}
-- {-# OPTIONS  -v tc.term.expr.args:80 #-}
-- {-# OPTIONS  -v tc.term.args:30 #-}

postulate
  S : Set
  Cxt : Set
  N : (Γ : Cxt) → Set

  NeP  : ∀ (i : S) Δ (n : N Δ) → Set
  inhN : ∀ i Δ (v : N Δ) → NeP i Δ v

data Val (Δ : Cxt) : Set where
  ne : ∀ (n : N Δ) → Val Δ

-- BEGIN mutual

data ValP i Δ : (v : Val Δ) → Set
NeO : _

data ValP i Δ where
  cn  : ∀ (n : N Δ) → NeO n i  → ValP i Δ (ne n)
-- adding constructor cn : (n : N Δ) → _24 i Δ n → ValP i Δ (ne n)
-- LATER    : term _24 i Δ n := NeO n i
-- SHOULD BE: term _24 i Δ n := NeO {Δ} i n

-- must be last in mutual block for error
-- implicit argument needed for error
-- NeO_[_] : ∀ {Δ} (n : N Δ) (i : S) → Set  -- full type signature removes error
NeO = λ {Δ} n i → NeP i Δ n

-- END mutual

inhVal : ∀ i Δ (v : Val Δ) → ValP i Δ v
inhVal i Δ (ne n) = cn n (inhN i Δ n)

-- Checking inhN i Δ n : NeO n [ i ] -->  λ i₁ → NeP i₁ n i

-- ANALYSIS:
-- checked type signature NeO : _20
-- checking constructor cn : (n : N Δ) → NeO n i → ValP i Δ (ne n)
-- adding constructor cn : (n : N Δ) → _24 i Δ n → ValP i Δ (ne n)
-- postponed checking arguments [n, i] against _20
-- progress: checked [] remaining [n, i] : _20
-- term _20 :>= {Δ : _27} → _29 {Δ}
-- term _20 :>= {Δ : _27} → _29 {Δ}
-- solving _20 := {Δ : _27} → _29 {Δ}
-- postponed checking arguments [n, i] against _29 {_Δ_30 i Δ n}
-- progress: checked [] remaining [n, i] : _29 {_Δ_30 i Δ n}
-- Checking λ n i → NeP i Δ n : _29 {Δ}
-- solving _29 := λ {Δ} → (n : N Δ) (i : S) → Set
-- solving _24 := (λ i Δ n → NeO n i)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module WellFounded where

open import Level

data Acc {a r} {A : Type a} (R : A → A → Type r) (x : A) : Type (a ℓ⊔ r) where
  acc : (∀ y → R y x → Acc R y) → Acc R x

-- record Acc {a r} {A : Type a} (R : A → A → Type r) (x : A) : Type (a ℓ⊔ r) where
--   inductive
--   constructor acc
--   field step : ∀ y → R y x → Acc R y
-- open Acc public

WellFounded : ∀ {r} → (A → A → Type r) → Type _
WellFounded R = ∀ x → Acc R x

open import HLevels
open import Path

isPropAcc : ∀ {r} {R : A → A → Type r} {x : A} → isProp (Acc R x)
isPropAcc (acc x) (acc y) = cong acc (funExt λ n → funExt λ p → isPropAcc (x n p) (y n p))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Fixed-size tables of values, implemented as functions from 'Fin n'.
-- Similar to 'Data.Vec', but focusing on ease of retrieval instead of
-- ease of adding and removing elements.
------------------------------------------------------------------------

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

module Data.Table where

open import Data.Table.Base public

open import Data.Bool using (true; false)
open import Data.Fin using (Fin; _≟_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (Inverse; _↔_)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

-- Changes the order of elements in the table according to a permutation (i.e.
-- an 'Inverse' object on the indices).

permute : ∀ {m n a} {A : Set a} → Fin m ↔ Fin n → Table A n → Table A m
permute π = rearrange (Inverse.to π ⟨$⟩_)

-- The result of 'select z i t' takes the value of 'lookup t i' at index 'i',
-- and 'z' everywhere else.

select : ∀ {n} {a} {A : Set a} → A → Fin n → Table A n → Table A n
lookup (select z i t) j with j ≟ i
... | yes _ = lookup t i
... | no  _ = z


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 provides some scaffolding to define the handlers for our
-- implementation and connect them to the interface of the SystemModel.

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Concrete.Records
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
open import LibraBFT.Impl.IO.OBM.Properties.InputOutputHandlers
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Encode
open import Util.KVMap
open import Util.Hash
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude

module LibraBFT.Impl.Handle.Properties where

open        EpochConfig
import      LibraBFT.Impl.Handle                as Handle
open import LibraBFT.Impl.Handle.InitProperties
open        initHandlerSpec
open        ParamsWithInitAndHandlers Handle.InitHandler.initAndHandlers
open        PeerCanSignForPK
open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms
                      Handle.InitHandler.initAndHandlers
                      PeerCanSignForPK PeerCanSignForPK-stable
open        Invariants
open        RoundManagerTransProps

-- TODO-1: Should 'invariantsCorrect' and direct corollaries be in a `Properties.Invariants` module?
------------------------------------------------------------------------------

-- For any peer in a reachable state, show that it respects RoundManager invariants.
invariantsCorrect
  : ∀ pid (pre : SystemState)
  → initialised pre pid ≡ initd
  → ReachableSystemState pre
  → RoundManagerInv (peerStates pre pid)

--------------------------------------------------
-- AN UNINITIALIZED PEER.
-- A peer has NOT been initialized at 'step-0', therefore it cannot be initialized (i.e., absurd).
invariantsCorrect _ _ () step-0

--------------------------------------------------
-- A CHEATER DOES NOT MODIFY STATE NOR INITIALIZED.
-- pid    : the peer we are reasoning about
-- pid'   : the peer taking the step
--          in the cheat step case, if does not matter if pid == pid'
-- pre    : the prestate of pid
-- pre'   : pre state for this reachable state (before the step, i.e., cheat here)
-- preach : evidence that pre' is reachable
-- cheatStepDNMPeerStates₁  : Does Not Modify state
-- cheatStepDNMInitialised₁ : Does Not Modify initialized
invariantsCorrect pid pre ini (step-s {pre = pre'} preach (step-peer step@(step-cheat  {pid'} _)))
  -- Goal: RoundManagerInv (override (peerStates pre') pid' (peerStates pre' pid') pid)
  rewrite cheatStepDNMPeerStates₁ {pid'} {pid} {pre = pre'} step unit
  -- Goal: RoundManagerInv (peerStates pre' pid)
  with trans (sym $ cheatStepDNMInitialised₁ step unit) ini
...| initialised-pre'-pid≡-initd                        -- preach : ReachableSystemState pre'
  = invariantsCorrect pid pre' initialised-pre'-pid≡-initd preach

--------------------------------------------------
-- Honest steps for the rest of the proof.
-- Note: all these top-level 'invariantsCorrect' are the SAME clause,
-- each with different pattern matching.

--------------------------------------------------
-- PEERS CANNOT MODIFY EACH OTHER'S STATE NOR INITIALIZED STATUS.
-- Reasoning about pid.
-- Peer taking step is different (pid').
invariantsCorrect pid pre ini (step-s {pre = pre'} preach (step-peer step@(step-honest {pid'} sps)))
  with pid ≟ pid'
...| no pid≢pid' -- NO case : step is for a different peer (pid') not this peer (pid).
  -- In that case pid' cannot modify pid's state,
  rewrite sym (pids≢StepDNMPeerStates {pre = pre'} sps pid≢pid')
  -- nor pid's initialized status.
  = invariantsCorrect pid pre' (trans (pids≢StepDNMInitialised {pre = pre'} sps pid≢pid') ini) preach

--------------------------------------------------
-- INITIALIZATION STEP
-- pre' is pre state of this init step
invariantsCorrect pid _   _   (step-s {pre = pre'} preach (step-peer (step-honest {outs = outs} (step-init {rm} rm×acts _))))
   | yes refl -- YES is from the 'with' above
              -- because this is the SAME clause except pattern matching deeper to get 'step-init'.
  -- Goal: RoundManagerInv ... where peerStates pre' pid "contains" the 'rm' from init
  rewrite override-target-≡ {a = pid} {b = rm} {f = peerStates pre'}
  -- Goal: RoundManagerInv rm
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  = initHandlerSpec.ContractOk.rmInv init-contract

--------------------------------------------------
-- PROPOSAL MSG
invariantsCorrect pid _   _   (step-s {pre = pre'} preach (step-peer (step-honest (step-msg {sndr , P pm} m∈pool ini))))
   | yes refl -- pid≡pid'
   -- Goal: RoundManagerInv ... where peerStates pre' pid "contains" the proposal msg
  with handleProposalSpec.contract! 0 pm (msgPool pre') (peerStates pre' pid)
...| c -- contract that says proposal has been handled
  with handleProposalSpec.Contract.rmInv c
...| invPres --   RoundManagerInv (peerStates pre' pid)
             -- → RoundManagerInv where state is updated from proposal message
  with invariantsCorrect pid pre' ini preach
...| ic      --   RoundManagerInv (peerStates pre' pid)
  -- Modify state to contain "results" of handling the proposal.
  rewrite override-target-≡ {a = pid} {b = LBFT-post (handleProposal 0 pm) (peerStates pre' pid)} {f = peerStates pre'}
  = invPres ic

--------------------------------------------------
-- VOTE MSG
invariantsCorrect pid _   _   (step-s {pre = pre'} preach (step-peer (step-honest (step-msg {sndr , V vm} m∈pool ini))))
   | yes refl -- pid≡pid'
  with handleVoteSpec.Contract.rmInv $ handleVoteSpec.contract! 0 vm (msgPool pre') (peerStates pre' pid)
...| invPres
  rewrite override-target-≡ {a = pid} {b = LBFT-post (handleVote 0 vm) (peerStates pre' pid)} {f = peerStates pre'}
  = invPres (invariantsCorrect pid pre' ini preach)

--------------------------------------------------
-- COMMIT MSG
invariantsCorrect pid _   _   (step-s {pre = pre'} preach (step-peer (step-honest (step-msg {sndr , C cm} m∈pool ini))))
   | yes refl -- pid≡pid'
  rewrite override-target-≡ {a = pid} {b = LBFT-post (handle pid (C cm) 0) (peerStates pre' pid)} {f = peerStates pre'}
  = invariantsCorrect pid pre' ini preach

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

-- All signatures represented in QCs that are in the RoundManager for each peer
-- have been sent before (i.e., no peer conjures a signature and makes a QC out of it
-- and stores it).
qcVoteSigsSentB4 :
    ∀ pid (st : SystemState)
    → initialised st pid ≡ initd
    → ReachableSystemState st
    → QCProps.SigsForVotes∈Rm-SentB4 (msgPool st) (peerStates st pid)

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

-- Handling any messages preserves the above 'qcVoteSigsSentB4' property.
-- Says this indirectly, via ReachableSystemState
-- then says the property holds after executing a handler from that ReachableSystemState.
-- "preserves"
-- - know it is true in the prestate (from qcVoteSigsSendB4)
-- - proving it's true in the poststate.
handlePreservesSigsB4 :
    ∀ {nm pid pre sndr}
    → initialised pre pid ≡ initd
    → ReachableSystemState pre
    → (sndr , nm) ∈ msgPool pre
    → QCProps.SigsForVotes∈Rm-SentB4 (msgPool pre) (LBFT-post (handle pid nm 0) (peerStates pre pid))
handlePreservesSigsB4 {nm} {pid} {pre} {sndr} ini preach m∈pool {qc} {v} {pk} = hyp
   where
   hPool = msgPool pre
   hPre  = peerStates pre pid

   hPost = LBFT-post (handle pid nm 0) hPre

   qcPost' : (nm' : NetworkMsg) → nm' ≡ nm → QCProps.∈Post⇒∈PreOr (_QC∈NM nm) hPre hPost
   qcPost' (P pm) refl = qcPost
      where open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm hPool hPre)
   qcPost' (V vm) refl = qcPost
      where open handleVoteSpec.Contract     (handleVoteSpec.contract!     0 vm hPool hPre)
   qcPost' (C cm) refl qc qc∈pre = Left qc∈pre

   hyp : QCProps.SigForVote∈Rm-SentB4 v pk qc hPost hPool
   hyp qc∈hpPst sig {vs} vs∈qcvs ≈v ¬bootstrap
      with qcPost' nm refl qc qc∈hpPst
   ...| Left qc∈hpPre =
     qcVoteSigsSentB4 pid pre ini preach qc∈hpPre sig vs∈qcvs ≈v ¬bootstrap
   ...| Right qc∈m =
      mkMsgWithSig∈ nm v (vote∈qc vs∈qcvs ≈v qc∈m) sndr m∈pool sig (cong (_^∙ vSignature) ≈v)

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

qcVoteSigsSentB4 pid st ()   step-0

qcVoteSigsSentB4 pid st ini (step-s rss (step-peer {pid'} {pre = pre} step@(step-cheat cmc)))
  rewrite cheatStepDNMPeerStates₁ {pid'} {pid} {pre = pre} step unit
  with trans (sym $ cheatStepDNMInitialised₁ step unit) ini
...| initialised-pre-pid≡-initd
  = QCProps.++-SigsForVote∈Rm-SentB4
      {rm = peerStates pre pid} _ (qcVoteSigsSentB4 pid pre initialised-pre-pid≡-initd rss)

qcVoteSigsSentB4 pid st ini (step-s rss (step-peer {pid'} {pre = pre} (step-honest sps)))
  with pid ≟ pid'

-- DIFFERENT PEER CASE
...| no  pid≢pid'
  rewrite sym (pids≢StepDNMPeerStates {pre = pre} sps pid≢pid')
  = QCProps.++-SigsForVote∈Rm-SentB4
      {rm = peerStates pre pid} _
      (qcVoteSigsSentB4 pid pre (trans (pids≢StepDNMInitialised {pre = pre} sps pid≢pid') ini) rss)
...| yes refl
  with sps

-- INIT CASE
...| step-init {rm} rm×acts _
  = ret
   where
    ret : QCProps.SigsForVotes∈Rm-SentB4 (msgPool st) (peerStates st pid)
    ret
      with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
    ...| init-contract
      rewrite override-target-≡ {a = pid} {b = rm} {f = peerStates pre}
      = λ qc∈rm sig vs∈qc rbld≈ ¬bootstrap
        → ⊥-elim $
          ¬bootstrap
          (initHandlerSpec.ContractOk.sigs∈bs
            init-contract vs∈qc qc∈rm)

-- MSG CASE
...| step-msg {sndr , nm} m∈pool init
  rewrite override-target-≡ {a = pid} {b = LBFT-post (handle pid nm 0) (peerStates pre pid)} {f = peerStates pre}
  = QCProps.++-SigsForVote∈Rm-SentB4
      {rm = LBFT-post (handle pid nm 0) (peerStates pre pid)} _
      (handlePreservesSigsB4 init rss m∈pool)

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

qcVoteSigsSentB4-sps
  : ∀ pid (pre : SystemState) {s acts}
  → ReachableSystemState pre
  → (StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s , acts))
  → ∀ {qc v pk}
  → qc QCProps.∈RoundManager s
  → WithVerSig pk v
  → ∀ {vs : Author × Signature} → let (pid , sig) = vs in
    vs ∈ qcVotes qc → rebuildVote qc vs ≈Vote v
  → ¬ ∈BootstrapInfo-impl fakeBootstrapInfo sig
  → MsgWithSig∈ pk sig (msgPool pre)

qcVoteSigsSentB4-sps pid pre rss (step-init {rm} rm×acts _) qc∈s sig vs∈qcvs ≈v ¬bootstrap
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  rewrite sym $ ++-identityʳ (msgPool pre)
  = QCProps.++-SigsForVote∈Rm-SentB4 {rm = rm} (msgPool pre)
      (λ qc∈rm sig vs∈qc rbld≈ ¬bootstrap
       → ⊥-elim $
           ¬bootstrap
           (initHandlerSpec.ContractOk.sigs∈bs
             init-contract vs∈qc qc∈rm))
      qc∈s sig vs∈qcvs ≈v ¬bootstrap

qcVoteSigsSentB4-sps pid pre rss (step-msg {sndr , m} m∈pool ini) {qc} {v} {pk} qc∈s sig {vs} vs∈qcvs ≈v ¬bootstrap
  with m
  -- TODO-2: refactor for DRY
...| P pm = help
  where
    hpPre = peerStates pre pid
    open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm (msgPool pre) hpPre)

    help : MsgWithSig∈ pk (proj₂ vs) (msgPool pre)
    help
      with qcPost qc qc∈s
    ...| Left qc∈pre = qcVoteSigsSentB4 pid pre ini rss qc∈pre sig vs∈qcvs ≈v ¬bootstrap
    ...| Right qc∈pm =
      mkMsgWithSig∈ (P pm) v (vote∈qc vs∈qcvs ≈v qc∈pm) sndr m∈pool sig (cong (_^∙ vSignature) ≈v)

   -- TODO-2: refactor for DRY
...| V vm = help
  where
    hvPre = peerStates pre pid
    open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)

    help : MsgWithSig∈ pk (proj₂ vs) (msgPool pre)
    help
      with qcPost qc qc∈s
    ...| Left qc∈pre = qcVoteSigsSentB4 pid pre ini rss qc∈pre sig vs∈qcvs ≈v ¬bootstrap
    ...| Right qc∈vm =
      mkMsgWithSig∈ (V vm) v (vote∈qc vs∈qcvs ≈v qc∈vm) sndr m∈pool sig (cong (_^∙ vSignature) ≈v)

...| C cm = qcVoteSigsSentB4 pid pre ini rss qc∈s sig vs∈qcvs ≈v ¬bootstrap

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

lastVotedRound-mono
  : ∀ pid (pre : SystemState) {ppost} {msgs}
  → ReachableSystemState pre
  → initialised pre pid ≡ initd
  → StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (ppost , msgs)
  → peerStates pre pid ≡L ppost at rmEpoch
  → Meta.getLastVoteRound ((peerStates pre pid) ^∙ pssSafetyData-rm)
    ≤
    Meta.getLastVoteRound (ppost                ^∙ pssSafetyData-rm)

lastVotedRound-mono pid pre preach ini (step-init _ uni) epoch≡ =
  case (trans (sym ini) uni) of λ ()

lastVotedRound-mono pid pre {ppost} preach ini₀ (step-msg {_ , m} m∈pool ini₁) epoch≡
  with m
...| P pm rewrite sym $ StepPeer-post-lemma {pre = pre} (step-honest (step-msg m∈pool ini₁)) = help
  where
  hpPool = msgPool pre
  hpPre  = peerStates pre pid
  hpPst  = LBFT-post (handleProposal 0 pm) hpPre
  hpOut  = LBFT-outs (handleProposal 0 pm) hpPre

  open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm hpPool hpPre {- hpReq -} )
  open RoundManagerInv (invariantsCorrect pid pre ini₁ preach)

  module VoteOld (lv≡ : hpPre ≡L hpPst at pssSafetyData-rm ∙ sdLastVote) where
    help : Meta.getLastVoteRound (hpPre ^∙ pssSafetyData-rm) ≤ Meta.getLastVoteRound (hpPst ^∙ pssSafetyData-rm)
    help = ≡⇒≤ (cong (Maybe-maybe {B = const ℕ} (_^∙ vRound) 0) lv≡)

  module VoteNew {vote : Vote}
    (lv≡v : just vote ≡ hpPst ^∙ pssSafetyData-rm ∙ sdLastVote)
    (lvr< : hpPre [ _<_ ]L hpPst at pssSafetyData-rm ∙ sdLastVotedRound)
    (lvr≡ : vote ^∙ vRound ≡ hpPst ^∙ pssSafetyData-rm ∙ sdLastVotedRound )
   where
    help : Meta.getLastVoteRound (hpPre ^∙ pssSafetyData-rm) ≤ Meta.getLastVoteRound (hpPst ^∙ pssSafetyData-rm)
    help = ≤-trans (SafetyDataInv.lvRound≤ ∘ SafetyRulesInv.sdInv $ rmSafetyRulesInv ) (≤-trans (<⇒≤ lvr<) (≡⇒≤ (trans (sym lvr≡) $ cong (Maybe-maybe {B = const ℕ} (_^∙ vRound) 0) lv≡v)))

  open Invariants
  open Reqs (pm ^∙ pmProposal) (hpPre ^∙ lBlockTree)
  open BlockTreeInv
  open BlockStoreInv
  open RoundManagerInv

  rmi : _
  rmi = invariantsCorrect pid pre ini₁ preach

  help : Meta.getLastVoteRound (hpPre ^∙ pssSafetyData-rm) ≤ Meta.getLastVoteRound (hpPst ^∙ pssSafetyData-rm)
  help
    with BlockId-correct? (pm ^∙ pmProposal)
  ...| no ¬validProposal
    = VoteOld.help (cong (_^∙ pssSafetyData-rm ∙ sdLastVote) (proj₁ $ invalidProposal ¬validProposal))
  ...| yes pmIdCorr
    with voteAttemptCorrect pmIdCorr (nohc preach m∈pool pid ini₀ rmi refl pmIdCorr)
  ...| Voting.mkVoteAttemptCorrectWithEpochReq (inj₁ (_ , Voting.mkVoteUnsentCorrect noVoteMsgOuts nvg⊎vgusc)) sdEpoch≡?
    with nvg⊎vgusc
  ...| inj₁  (mkVoteNotGenerated lv≡  lvr≤) = VoteOld.help lv≡
  ...| inj₂  (Voting.mkVoteGeneratedUnsavedCorrect vote (Voting.mkVoteGeneratedCorrect (mkVoteGenerated lv≡v voteSrc) blockTriggered))
    with voteSrc
  ...| inj₁  (mkVoteOldGenerated lvr≡ lv≡)  = VoteOld.help lv≡
  ...| inj₂  (mkVoteNewGenerated lvr< lvr≡) = VoteNew.help lv≡v lvr< lvr≡
  help
     | yes refl
     | Voting.mkVoteAttemptCorrectWithEpochReq (Right (Voting.mkVoteSentCorrect vm _ _ (Voting.mkVoteGeneratedCorrect (mkVoteGenerated lv≡v voteSrc) _))) sdEpoch≡?
    with voteSrc
  ...| Left  (mkVoteOldGenerated lvr≡ lv≡)  = VoteOld.help lv≡
  ...| Right (mkVoteNewGenerated lvr< lvr≡) = VoteNew.help lv≡v lvr< lvr≡

-- Receiving a vote or commit message does not update the last vote
...| V vm = ≡⇒≤ $ cong (Maybe-maybe (_^∙ vRound) 0 ∘ (_^∙ sdLastVote)) noSDChange
   where
   hvPre = peerStates pre pid
   hvPst = LBFT-post (handle pid (V vm) 0) hvPre

   open handleVoteSpec.Contract (handleVoteSpec.contract! 0 vm (msgPool pre) hvPre)

...| C cm = ≤-refl

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

qcVoteSigsSentB4-handle
  : ∀ pid {pre m s acts}
  → ReachableSystemState pre
  → (StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s , acts))
  → send m ∈ acts
  → ∀ {qc v pk}
  → qc QC∈NM m
  → WithVerSig pk v
  → ∀ {vs : Author × Signature} → let (pid , sig) = vs in vs ∈ qcVotes qc
  → rebuildVote qc vs ≈Vote v
  → ¬ ∈BootstrapInfo-impl fakeBootstrapInfo sig
  → MsgWithSig∈ pk sig (msgPool pre)

qcVoteSigsSentB4-handle pid {pre} {m} {s} {acts} preach
                        (step-init {rm} rm×acts _)
                        send∈acts
                        {qc}
                        qc∈m sig vs∈qc v≈rbld ¬bootstrap
  with initHandlerSpec.contract pid fakeBootstrapInfo rm×acts
...| init-contract
  with initHandlerSpec.ContractOk.isInitPM init-contract send∈acts
...| _ , refl , noSigs = ⊥-elim (noSigs vs∈qc qc∈m)

qcVoteSigsSentB4-handle pid {pre} {m} {s} {acts} preach
                        sps@(step-msg {_ , nm} m∈pool ini)
                        m∈acts
                        {qc} qc∈m sig vs∈qc v≈rbld ¬bootstrap =
  qcVoteSigsSentB4-sps pid pre preach sps qc∈rm sig vs∈qc v≈rbld ¬bootstrap
 where
  hdPool = msgPool pre
  hdPre  = peerStates pre pid
  hdPst  = LBFT-post (handle pid nm 0) hdPre
  hdOut  = LBFT-outs (handle pid nm 0) hdPre

  qc∈rm : qc QCProps.∈RoundManager hdPst
  qc∈rm
    with sendMsg∈actions {hdOut} {st = hdPre} m∈acts
  ...| out , out∈hdOut , m∈out = All-lookup (outQcs∈RM1 nm refl) out∈hdOut qc m qc∈m m∈out
   where
    outQcs∈RM1 : (nm' : NetworkMsg) → nm ≡ nm' → QCProps.OutputQc∈RoundManager hdOut hdPst
    outQcs∈RM1 (P pm) refl = outQcs∈RM
     where open handleProposalSpec.Contract (handleProposalSpec.contract! 0 pm hdPool hdPre)
    outQcs∈RM1 (V vm) refl = outQcs∈RM
     where open handleVoteSpec.Contract     (handleVoteSpec.contract!     0 vm hdPool hdPre)


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

-- Common cost monoids.

module Calf.CostMonoids where

open import Calf.CostMonoid
open import Data.Product
open import Relation.Binary.PropositionalEquality

ℕ-CostMonoid : CostMonoid
ℕ-CostMonoid = record
  { ℂ = ℕ
  ; _+_ = _+_
  ; zero = zero
  ; _≤_ = _≤_
  ; isCostMonoid = record
    { isMonoid = +-0-isMonoid
    ; isCancellative = record { ∙-cancel-≡ = +-cancel-≡ }
    ; isPreorder = ≤-isPreorder
    ; isMonotone = record { ∙-mono-≤ = +-mono-≤ }
    }
  }
  where
    open import Data.Nat
    open import Data.Nat.Properties

ℕ-Work-ParCostMonoid : ParCostMonoid
ℕ-Work-ParCostMonoid = record
  { ℂ = ℕ
  ; _⊕_ = _+_
  ; 𝟘 = 0
  ; _⊗_ = _+_
  ; 𝟙 = 0
  ; _≤_ = _≤_
  ; isParCostMonoid = record
    { isMonoid = +-0-isMonoid
    ; isCommutativeMonoid = +-0-isCommutativeMonoid
    ; isCancellative = record { ∙-cancel-≡ = +-cancel-≡ }
    ; isPreorder = ≤-isPreorder
    ; isMonotone-⊕ = record { ∙-mono-≤ = +-mono-≤ }
    ; isMonotone-⊗ = record { ∙-mono-≤ = +-mono-≤ }
    }
  }
  where
    open import Data.Nat
    open import Data.Nat.Properties

ℕ-Span-ParCostMonoid : ParCostMonoid
ℕ-Span-ParCostMonoid = record
  { ℂ = ℕ
  ; _⊕_ = _+_
  ; 𝟘 = 0
  ; _⊗_ = _⊔_
  ; 𝟙 = 0
  ; _≤_ = _≤_
  ; isParCostMonoid = record
    { isMonoid = +-0-isMonoid
    ; isCommutativeMonoid = ⊔-0-isCommutativeMonoid
    ; isPreorder = ≤-isPreorder
    ; isCancellative = record { ∙-cancel-≡ = +-cancel-≡ }
    ; isMonotone-⊕ = record { ∙-mono-≤ = +-mono-≤ }
    ; isMonotone-⊗ = record { ∙-mono-≤ = ⊔-mono-≤ }
    }
  }
  where
    open import Data.Nat
    open import Data.Nat.Properties

combineParCostMonoids : ParCostMonoid → ParCostMonoid → ParCostMonoid
combineParCostMonoids pcm₁ pcm₂ = record
  { ℂ = ℂ pcm₁ × ℂ pcm₂
  ; _⊕_ = λ (a₁ , a₂) (b₁ , b₂) → _⊕_ pcm₁ a₁ b₁ , _⊕_ pcm₂ a₂ b₂
  ; 𝟘 = 𝟘 pcm₁ , 𝟘 pcm₂
  ; _⊗_ = λ (a₁ , a₂) (b₁ , b₂) → _⊗_ pcm₁ a₁ b₁ , _⊗_ pcm₂ a₂ b₂
  ; 𝟙 = 𝟙 pcm₁ , 𝟙 pcm₂
  ; _≤_ = λ (a₁ , a₂) (b₁ , b₂) → _≤_ pcm₁ a₁ b₁ × _≤_ pcm₂ a₂ b₂
  ; isParCostMonoid = record
    { isMonoid = record
      { isSemigroup = record
        { isMagma = record
          { isEquivalence = isEquivalence
          ; ∙-cong = λ h₁ h₂ →
              cong₂ _,_
                (cong₂ (_⊕_ pcm₁) (cong proj₁ h₁) (cong proj₁ h₂))
                (cong₂ (_⊕_ pcm₂) (cong proj₂ h₁) (cong proj₂ h₂))
          }
        ; assoc = λ (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) → cong₂ _,_ (⊕-assoc pcm₁ a₁ b₁ c₁) (⊕-assoc pcm₂ a₂ b₂ c₂)
        }
      ; identity =
        (λ (a₁ , a₂) → cong₂ _,_ (⊕-identityˡ pcm₁ a₁) (⊕-identityˡ pcm₂ a₂)) ,
        (λ (a₁ , a₂) → cong₂ _,_ (⊕-identityʳ pcm₁ a₁) (⊕-identityʳ pcm₂ a₂))
      }
    ; isCommutativeMonoid = record
      { isMonoid = record
        { isSemigroup = record
          { isMagma = record
            { isEquivalence = isEquivalence
            ; ∙-cong = λ h₁ h₂ →
                cong₂ _,_
                  (cong₂ (_⊗_ pcm₁) (cong proj₁ h₁) (cong proj₁ h₂))
                  (cong₂ (_⊗_ pcm₂) (cong proj₂ h₁) (cong proj₂ h₂))
            }
          ; assoc = λ (a₁ , a₂) (b₁ , b₂) (c₁ , c₂) → cong₂ _,_ (⊗-assoc pcm₁ a₁ b₁ c₁) (⊗-assoc pcm₂ a₂ b₂ c₂)
          }
        ; identity =
          (λ (a₁ , a₂) → cong₂ _,_ (⊗-identityˡ pcm₁ a₁) (⊗-identityˡ pcm₂ a₂)) ,
          (λ (a₁ , a₂) → cong₂ _,_ (⊗-identityʳ pcm₁ a₁) (⊗-identityʳ pcm₂ a₂))
        }
      ; comm = λ (a₁ , a₂) (b₁ , b₂) → cong₂ _,_ (⊗-comm pcm₁ a₁ b₁) (⊗-comm pcm₂ a₂ b₂)
      }
    ; isCancellative = record
      { ∙-cancel-≡ =
        (λ (x₁ , x₂)           h → cong₂ _,_ (⊕-cancelˡ-≡ pcm₁ x₁    (cong proj₁ h)) (⊕-cancelˡ-≡ pcm₂ x₂    (cong proj₂ h))) ,
        (λ (y₁ , y₂) (z₁ , z₂) h → cong₂ _,_ (⊕-cancelʳ-≡ pcm₁ y₁ z₁ (cong proj₁ h)) (⊕-cancelʳ-≡ pcm₂ y₂ z₂ (cong proj₂ h)))
      }
    ; isPreorder = record
      { isEquivalence = isEquivalence
      ; reflexive = λ { refl → ≤-refl pcm₁ , ≤-refl pcm₂ }
      ; trans = λ (h₁ , h₂) (h₁' , h₂') → ≤-trans pcm₁ h₁ h₁' , ≤-trans pcm₂ h₂ h₂'
      }
    ; isMonotone-⊕ = record
      { ∙-mono-≤ = λ (h₁ , h₂) (h₁' , h₂') → ⊕-mono-≤ pcm₁ h₁ h₁' , ⊕-mono-≤ pcm₂ h₂ h₂'
      }
    ; isMonotone-⊗ = record
      { ∙-mono-≤ = λ (h₁ , h₂) (h₁' , h₂') → ⊗-mono-≤ pcm₁ h₁ h₁' , ⊗-mono-≤ pcm₂ h₂ h₂'
      }
    }
  }
  where open ParCostMonoid

ℕ²-ParCostMonoid : ParCostMonoid
ℕ²-ParCostMonoid = combineParCostMonoids ℕ-Work-ParCostMonoid ℕ-Span-ParCostMonoid

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Data.Sum.Instance where

open import Class.Equality
open import Class.Monoid
open import Class.Show
open import Data.Bool using (false)
open import Data.String.Instance
open import Data.Sum
open import Data.Sum.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

instance
  Sum-Eq : {A B : Set} -> {{_ : Eq A}} -> {{_ : Eq B}} -> Eq (A ⊎ B)
  Sum-Eq = record { _≟_ = ≡-dec _≟_ _≟_ }

  Sum-Show : {A B : Set} -> {{_ : Show A}} -> {{_ : Show B}} -> Show (A ⊎ B)
  Sum-Show = record { show = λ { (inj₁ x) → "inj₁ " + show x ; (inj₂ y) → "inj₂ " + show y } }

  Sum-EqB : {A B : Set} -> {{_ : EqB A}} -> {{_ : EqB B}} -> EqB (A ⊎ B)
  Sum-EqB = record { _≣_ = λ { (inj₁ x) (inj₁ y) → x ≣ y
                             ; (inj₁ x) (inj₂ y) → false
                             ; (inj₂ x) (inj₁ y) → false
                             ; (inj₂ x) (inj₂ y) → x ≣ y } }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
open import Data.Bool using (Bool; true; false)
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open import Relation.Nullary using (¬_)

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

trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

-- This can be done in Coq but not in Agda?
--disc'' : ∀ {x : Bool} → x ≡ x → x ≡ (¬ x) → ⊥
--disc'' = ?

-- How to prove this???
disc' : ∀ {a} {x : Set a} → x ≡ x → x ≡ (¬ x) → ⊥
disc' refl = ?

disc : ∀ {a} {x : Set a} → ¬ (x ≡ (¬ x))
disc {x} x≡¬x = ? -- disc' ? ? -- (refl {x}) x≡¬x

open import Data.Nat using (ℕ; suc; zero; _+_)

right-zero : ∀ n → n + 0 ≡ n
right-zero 0 = refl
right-zero (suc n) = cong suc (right-zero n)

comm : ∀ m n p → m + (n + p) ≡ (m + n) + p
comm 0 _ _ = refl
comm (suc m) n p = cong suc (comm m n p)


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

module Avionics.Probability where

--open import Data.Fin using (Fin; fromℕ<)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_)
open import Data.Vec using (Vec; lookup)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Unary using (_∈_)

open import Avionics.Real using (
    ℝ; _+_; _-_; _*_; _÷_; _^_; √_; 1/_; _^2;
    -1/2; π; e; 2ℝ; 1ℝ; 0ℝ;
    ⟨0,∞⟩; [0,∞⟩; [0,1])

record Dist (Input : Set) : Set where
  field
    pdf : Input → ℝ
    cdf : Input → ℝ
    pdf→[0,∞⟩ : ∀ x → pdf x ∈ [0,∞⟩
    cdf→[0,1] : ∀ x → cdf x ∈ [0,1]
    --∫pdf≡cdf : ∫ pdf ≡ cdf
    --∫pdf[-∞,∞]≡1ℝ : ∫ pdf [ -∞ , ∞ ] ≡ 1ℝ

record NormalDist : Set where
  constructor ND
  field
    μ : ℝ
    σ : ℝ
    --.0<σ : 0ℝ <? σ

  dist : Dist ℝ
  dist = record
    {
      pdf = pdf
    ; cdf = ?
    ; pdf→[0,∞⟩ = ?
    ; cdf→[0,1] = ?
    }
    where
      √2π = (√ (2ℝ * π))
      1/⟨σ√2π⟩ = (1/ (σ * √2π))

      pdf : ℝ → ℝ
      pdf x = 1/⟨σ√2π⟩ * e ^ (-1/2 * (⟨x-μ⟩÷σ ^2))
        where
          ⟨x-μ⟩÷σ = ((x - μ) ÷ σ)

-- Bivariate Normal Distribution
-- Representation taken from: https://upload.wikimedia.org/wikipedia/commons/a/a2/Cumulative_function_n_dimensional_Gaussians_12.2013.pdf
record BiNormalDist : Set where
  constructor ND
  field
    μ₁ : ℝ
    μ₂ : ℝ
    σ₁ : ℝ
    σ₂ : ℝ
    ρ : ℝ

  μ : ℝ × ℝ
  μ = μ₁ , μ₂

  Σ : ℝ × ℝ × ℝ × ℝ
  Σ = σ₁ , (ρ * σ₁ * σ₂) , (ρ * σ₁ * σ₂) , σ₂

  Σ-¹ : ℝ × ℝ × ℝ × ℝ
  Σ-¹ = ( 1/1-ρ² * (1ℝ ÷ σ₁)
        , 1/1-ρ² * -ρ/σ₁σ₂
        , 1/1-ρ² * -ρ/σ₁σ₂
        , 1/1-ρ² * (1ℝ ÷ σ₂))
    where 1/1-ρ² = 1ℝ ÷ (1ℝ - ρ * ρ)
          -ρ/σ₁σ₂ = (0ℝ - ρ) ÷ (σ₁ * σ₂)

  dist : Dist ℝ
  dist = record
    {
      pdf = ?
    ; cdf = ?
    ; pdf→[0,∞⟩ = ?
    ; cdf→[0,1] = ?
    }

Mat : ℕ → Set
Mat n = Vec (Vec ℝ n) n

-- Multivariate Normal Distribution
record MultiNormal : Set where
  constructor MultiND
  field
    n : ℕ
    μ : Vec ℝ n
    Σ : Mat n

  dist : Dist (Vec ℝ n)
  dist = record
    {
      pdf = ?
    ; cdf = ?
    ; pdf→[0,∞⟩ = ?
    ; cdf→[0,1] = ?
    }

--num : Vec ℕ 2 → ℕ
--num vec = lookup vec (fromℕ< {0} _)

--num2 : MultiNormal → ℝ
--num2 mn = lookup μ (fromℕ< {0} _)
--  where open MultiNormal mn using (n; μ; Σ) --; dist)
--        --open Dist dist using (pdf)

max_stars_repo_name: helq/safety-envelopes-sentinels

max_issues_repo_name: helq/safety-envelopes-sentinels

max_forks_repo_name: helq/safety-envelopes-sentinels


text:
{-# IMPORT Issue223 #-}

data A : Set
{-# COMPILED_DECLARE_DATA A Issue223.A #-}
data B : Set
{-# COMPILED_DECLARE_DATA B Issue223.B #-}

data A where
  BA : B → A
{-# COMPILED_DATA A Issue223.A Issue223.BA #-}

data B where
  AB : A → B
  BB : B
{-# COMPILED_DATA B Issue223.B Issue223.AB Issue223.BB #-}


text:
{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness #-}
module Agda.Builtin.Cubical.Path where

  open import Agda.Primitive.Cubical

  postulate
    PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

  {-# BUILTIN PATHP        PathP     #-}

  infix 4 _≡_
  _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
  _≡_ {A = A} = PathP (λ _ → A)

  {-# BUILTIN PATH         _≡_     #-}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


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

open import Categories.Category
open import Categories.Category.Monoidal.Core using (Monoidal)

module Categories.Category.Monoidal.Braided {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level

open import Data.Product using (Σ; _,_)

open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.NaturalIsomorphism

open Category C
open Commutation

private
  variable
    X Y Z : Obj

-- braided monoidal category
-- it has a braiding natural isomorphism has two hexagon identities.
-- these two identities are directly expressed in the morphism level.
record Braided : Set (levelOfTerm M) where
  open Monoidal M public

  field
    braiding : NaturalIsomorphism ⊗ (flip-bifunctor ⊗)

  module braiding = NaturalIsomorphism braiding

  private
    B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
    B {X} {Y} = braiding.⇒.η (X , Y)

  field
    hexagon₁ : [ (X ⊗₀ Y) ⊗₀ Z ⇒ Y ⊗₀ Z ⊗₀ X ]⟨
                 B  ⊗₁ id                    ⇒⟨ (Y ⊗₀ X) ⊗₀ Z ⟩
                 associator.from             ⇒⟨ Y ⊗₀ X ⊗₀ Z ⟩
                 id ⊗₁ B
               ≈ associator.from             ⇒⟨ X ⊗₀ Y ⊗₀ Z ⟩
                 B                           ⇒⟨ (Y ⊗₀ Z) ⊗₀ X ⟩
                 associator.from
               ⟩
    hexagon₂ : [ X ⊗₀ Y ⊗₀ Z ⇒ (Z ⊗₀ X) ⊗₀ Y ]⟨
                 id ⊗₁ B                     ⇒⟨ X ⊗₀ Z ⊗₀ Y ⟩
                 (associator.to              ⇒⟨ (X ⊗₀ Z) ⊗₀ Y ⟩
                 B ⊗₁ id)
               ≈ associator.to               ⇒⟨ (X ⊗₀ Y) ⊗₀ Z ⟩
                 (B                          ⇒⟨ Z ⊗₀ X ⊗₀ Y ⟩
                 associator.to)
               ⟩

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- this is the first test I run
-- Its been a while since i used my brain, @KMx404

module test1 where

data 𝕟 : Set where
  --zero : 𝕟 --its not practical to do so, we can use more efficient math formulas
  suc : 𝕟 → 𝕟  -- since We have the value of zero => n, any next item succ will consider it as n.num
  _+_ : 𝕟 → 𝕟 → 𝕟 -- Defining addition? I guess (wtf is guess? haha)
 -- zero : zero
  --zero + zero = zero
  --zero + 𝕟 =  𝕟 -- Zero has no effect in addition


text:
module Base.Free.Instance.Identity where

open import Data.Empty using (⊥)

open import Base.Free  using (Free)

-- Representation of the `Identity` monad using free.
Shape : Set
Shape = ⊥

Position : Shape → Set
Position _ = ⊥

Identity : Set → Set
Identity = Free Shape Position

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Sn where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.KcompPrelims
open import Cubical.ZCohomology.Groups.Prelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁) hiding (map)

open import Cubical.Data.Bool
open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec)
open import Cubical.Data.Unit

open import Cubical.Homotopy.Connected

open import Cubical.Algebra.Group

infixr 31 _□_
_□_ : _
_□_ = compGroupIso

open GroupEquiv
open vSES
open GroupIso
open GroupHom
open BijectionIso

Sn-connected : (n : ℕ) (x : typ (S₊∙ (suc n))) → ∥ pt (S₊∙ (suc n)) ≡ x ∥₁
Sn-connected zero = toPropElim (λ _ → propTruncIsProp) ∣ refl ∣₁
Sn-connected (suc zero) = suspToPropElim base (λ _ → propTruncIsProp) ∣ refl ∣₁
Sn-connected (suc (suc n)) = suspToPropElim north (λ _ → propTruncIsProp) ∣ refl ∣₁

H⁰-Sⁿ≅ℤ : (n : ℕ) → GroupIso (coHomGr 0 (S₊ (suc n))) intGroup
H⁰-Sⁿ≅ℤ zero = H⁰-connected base (Sn-connected 0)
H⁰-Sⁿ≅ℤ (suc n) = H⁰-connected north (Sn-connected (suc n))

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

--- We will need to switch between Sⁿ defined using suspensions and using pushouts
--- in order to apply Mayer Vietoris.

S1Iso : Iso S¹ (Pushout {A = Bool} (λ _ → tt) λ _ → tt)
S1Iso = S¹IsoSuspBool ⋄ invIso PushoutSuspIsoSusp

coHomPushout≅coHomSn : (n m : ℕ) → GroupIso (coHomGr m (S₊ (suc n)))
                                             (coHomGr m (Pushout {A = S₊ n} (λ _ → tt) λ _ → tt))
coHomPushout≅coHomSn zero m =
  Iso+Hom→GrIso (setTruncIso (domIso S1Iso))
                (sElim2 (λ _ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ _ → refl))
coHomPushout≅coHomSn (suc n) m =
  Iso+Hom→GrIso (setTruncIso (domIso (invIso PushoutSuspIsoSusp)))
                (sElim2 (λ _ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ _ → refl))

-------------------------- H⁰(S⁰) -----------------------------
S0→Int : (a : Int × Int) → S₊ 0 → Int
S0→Int a true = fst a
S0→Int a false = snd a

H⁰-S⁰≅ℤ×ℤ : GroupIso (coHomGr 0 (S₊ 0)) (dirProd intGroup intGroup)
fun (map H⁰-S⁰≅ℤ×ℤ) = sRec (isSet× isSetInt isSetInt) λ f → (f true) , (f false)
isHom (map H⁰-S⁰≅ℤ×ℤ) = sElim2 (λ _ _ → isSet→isGroupoid (isSet× isSetInt isSetInt) _ _)
                                λ a b i → addLemma (a true) (b true) i , addLemma (a false) (b false) i
inv H⁰-S⁰≅ℤ×ℤ a = ∣ S0→Int a ∣₂
rightInv H⁰-S⁰≅ℤ×ℤ _ = refl
leftInv H⁰-S⁰≅ℤ×ℤ = sElim (λ _ → isSet→isGroupoid setTruncIsSet _ _)
                           λ f → cong ∣_∣₂ (funExt (λ {true → refl ; false → refl}))

------------------------- H¹(S⁰) ≅ 0 -------------------------------

private
  Hⁿ-S0≃Kₙ×Kₙ : (n : ℕ) → Iso (S₊ 0 → coHomK (suc n)) (coHomK (suc n) × coHomK (suc n))
  Iso.fun (Hⁿ-S0≃Kₙ×Kₙ n) f = (f true) , (f false)
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) true = a
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) false = b
  Iso.rightInv (Hⁿ-S0≃Kₙ×Kₙ n) a = refl
  Iso.leftInv (Hⁿ-S0≃Kₙ×Kₙ n) b = funExt λ {true → refl ; false → refl}

  isContrHⁿ-S0 : (n : ℕ) → isContr (coHom (suc n) (S₊ 0))
  isContrHⁿ-S0 n = isContrRetract (Iso.fun (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (Iso.inv (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (Iso.leftInv (setTruncIso (Hⁿ-S0≃Kₙ×Kₙ n)))
                                  (isContrHelper n)
    where
    isContrHelper : (n : ℕ) → isContr (∥ (coHomK (suc n) × coHomK (suc n)) ∥₂)
    fst (isContrHelper zero) = ∣ (0₁ , 0₁) ∣₂
    snd (isContrHelper zero) = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0₁ , 0₁) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isOfHLevelPlus {n = 2} 2 setTruncIsSet _ _)
                                  (toPropElim2 (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)
    isContrHelper (suc zero) = ∣ (0₂ , 0₂) ∣₂
                          , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0₂ , 0₂) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isOfHLevelPlus {n = 2} 3 setTruncIsSet _ _)
                                  (suspToPropElim2 base (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)
    isContrHelper (suc (suc n)) = ∣ (0ₖ (3 + n) , 0ₖ (3 + n)) ∣₂
                          , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                  λ y → elim2 {B = λ x y → ∣ (0ₖ (3 + n) , 0ₖ (3 + n)) ∣₂ ≡ ∣(x , y) ∣₂ }
                                  (λ _ _ → isProp→isOfHLevelSuc (4 + n) (setTruncIsSet _ _))
                                  (suspToPropElim2 north (λ _ _ → setTruncIsSet _ _) refl) (fst y) (snd y)

H¹-S⁰≅0 : (n : ℕ) → GroupIso (coHomGr (suc n) (S₊ 0)) trivialGroup
H¹-S⁰≅0 n = IsoContrGroupTrivialGroup (isContrHⁿ-S0 n)

------------------------- H²(S¹) ≅ 0 -------------------------------

Hⁿ-S¹≅0 : (n : ℕ) → GroupIso (coHomGr (2 + n) (S₊ 1)) trivialGroup
Hⁿ-S¹≅0 n = IsoContrGroupTrivialGroup
            (isOfHLevelRetractFromIso 0 helper
              (_ , helper2))
  where
  helper : Iso ⟨ coHomGr (2 + n) (S₊ 1)⟩ ∥ Σ (hLevelTrunc (4 + n) (S₊ (2 + n))) (λ x → ∥ x ≡ x ∥₂) ∥₂
  helper = compIso (setTruncIso IsoFunSpaceS¹) IsoSetTruncateSndΣ

  helper2 : (x : ∥ Σ (hLevelTrunc (4 + n) (S₊ (2 + n))) (λ x → ∥ x ≡ x ∥₂) ∥₂) → ∣ ∣ north ∣ , ∣ refl ∣₂ ∣₂ ≡ x
  helper2 =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          (uncurry
            (trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isProp→isOfHLevelSuc (3 + n) (setTruncIsSet _ _))
              (suspToPropElim (ptSn (suc n)) (λ _ → isPropΠ λ _ → setTruncIsSet _ _)
                (sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                       λ p
                    → cong ∣_∣₂ (ΣPathP (refl , isContr→isProp helper3 _ _))))))
    where
    helper4 : isConnected (n + 3) (hLevelTrunc (4 + n) (S₊ (2 + n)))
    helper4 = subst (λ m → isConnected m (hLevelTrunc (4 + n) (S₊ (2 + n)))) (+-comm 3 n)
                    (isOfHLevelRetractFromIso 0 (invIso (truncOfTruncIso (3 + n) 1)) (sphereConnected (2 + n)))

    helper3 : isContr ∥ ∣ north ∣ ≡ ∣ north ∣ ∥₂
    helper3 = isOfHLevelRetractFromIso 0 setTruncTrunc2Iso
                                         (isConnectedPath 2 (isConnectedSubtr 3 n helper4) _ _)

-- --------------- H¹(Sⁿ), n ≥ 1 --------------------------------------------

H¹-Sⁿ≅0 : (n : ℕ) → GroupIso (coHomGr 1 (S₊ (2 + n))) trivialGroup
H¹-Sⁿ≅0 zero = IsoContrGroupTrivialGroup isContrH¹S²
  where
  isContrH¹S² : isContr ⟨ coHomGr 1 (S₊ 2) ⟩
  isContrH¹S² = ∣ (λ _ → ∣ base ∣) ∣₂
              , coHomPointedElim 0 north (λ _ → setTruncIsSet _ _)
                   λ f p → cong ∣_∣₂ (funExt λ x → sym p ∙∙ sym (spoke f north) ∙∙ spoke f x)
H¹-Sⁿ≅0 (suc n) = IsoContrGroupTrivialGroup isContrH¹S³⁺ⁿ
  where
  anIso : Iso ⟨ coHomGr 1 (S₊ (3 + n)) ⟩ ∥ (S₊ (3 + n) → hLevelTrunc (4 + n) (coHomK 1)) ∥₂
  anIso =
    setTruncIso
      (codomainIso
        (invIso (truncIdempotentIso (4 + n) (isOfHLevelPlus' {n = 1 + n} 3 (isOfHLevelTrunc 3)))))

  isContrH¹S³⁺ⁿ-ish : (f : (S₊ (3 + n) → hLevelTrunc (4 + n) (coHomK 1)))
                   → ∣ (λ _ → ∣ ∣ base ∣ ∣) ∣₂ ≡ ∣ f ∣₂
  isContrH¹S³⁺ⁿ-ish f = ind (f north) refl
    where
    ind : (x : hLevelTrunc (4 + n) (coHomK 1))
       → x ≡ f north
       → ∣ (λ _ → ∣ ∣ base ∣ ∣) ∣₂ ≡ ∣ f ∣₂
    ind = trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelPlus' {n = (3 + n)} 1 (setTruncIsSet _ _))
              (trElim (λ _ → isOfHLevelΠ 3 λ _ → isOfHLevelPlus {n = 1} 2 (setTruncIsSet _ _))
              (toPropElim (λ _ → isPropΠ λ _ → setTruncIsSet _ _)
              λ p → cong ∣_∣₂ (funExt λ x → p ∙∙ sym (spoke f north) ∙∙ spoke f x)))
  isContrH¹S³⁺ⁿ : isContr ⟨ coHomGr 1 (S₊ (3 + n)) ⟩
  isContrH¹S³⁺ⁿ =
    isOfHLevelRetractFromIso 0
      anIso
      (∣ (λ _ → ∣ ∣ base ∣ ∣) ∣₂
      , sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _) isContrH¹S³⁺ⁿ-ish)

--------- Direct proof of H¹(S¹) ≅ ℤ without Mayer-Vietoris -------

-- The strategy is to use the proof that ΩS¹ ≃ ℤ. Since we only have this for S¹ with the base/loop definition
-- we begin with some functions translating between H¹(S₊ 1) and ∥ S¹ → S¹ ∥₀.  The latter type is easy to characterise,
-- by (S¹ → S¹) ≃ S¹ × ℤ (see Cubical.ZCohomology.Groups.Prelims). Truncating this leaves only ℤ, since S¹ is connected.

-- The translation mentioned above uses the basechange function. We use basechange-lemma (Cubical.ZCohomology.Groups.Prelims) to prove the basechange2⁻ preserves
-- path composition (in a more general sense than what is proved in basechange2⁻-morph)

-- We can now give the group equivalence. The first bit is just a big composition of our previously defined translations and is pretty uninteresting.
-- The harder step is proving that the equivalence is a morphism. This relies heavily on the fact that addition the cohomology groups essentially is defined using an
-- application of cong₂, which allows us to use basechange-lemma.

coHom1S1≃ℤ : GroupIso (coHomGr 1 (S₊ 1)) intGroup
coHom1S1≃ℤ = theIso
  where
  F = Iso.fun S¹→S¹≡S¹×Int
  F⁻ = Iso.inv S¹→S¹≡S¹×Int

  theIso : GroupIso (coHomGr 1 (S₊ 1)) intGroup
  fun (map theIso) = sRec isSetInt (λ f → snd (F f))
  isHom (map theIso) = sElim2 (λ _ _ → isOfHLevelPath 2 isSetInt _ _)
                              λ f g → ((λ i → winding (guy (ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f base) ∙ Kn→ΩKn+1 1 (g base)))
                                              (λ i → S¹map (ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f (loop i)) ∙ Kn→ΩKn+1 1 (g (loop i))))))))
                                   ∙∙ cong winding (helper (f base) (g base) f g refl refl)
                                   ∙∙ winding-hom (guy (f base) (λ i → S¹map (f (loop i))))
                                                  (guy (g base) (λ i → S¹map (g (loop i))))
    where
    guy = basechange2⁻ ∘ S¹map

    helper : (x y : coHomK 1) (f g : S₊ 1 → coHomK 1)
           → (f base) ≡ x
           → (g base) ≡ y
           → (guy (ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f base) ∙ Kn→ΩKn+1 1 (g base)))
                   (λ i → S¹map ((ΩKn+1→Kn 1 (Kn→ΩKn+1 1 (f (loop i)) ∙ Kn→ΩKn+1 1 (g (loop i)))))))
             ≡ (guy (f base)
                    (λ i → S¹map (f (loop i))))
             ∙ (guy (g base)
                    (λ i → S¹map ((g (loop i)))))
    helper =
      elim2 (λ _ _ → isGroupoidΠ4 λ _ _ _ _ → isOfHLevelPath 3 (isOfHLevelSuc 3 (isGroupoidS¹) base base) _ _)
            (toPropElim2
              (λ _ _ → isPropΠ4 λ _ _ _ _ → isGroupoidS¹ _ _ _ _)
              λ f g reflf reflg →
              basechange-lemma base base
                (S¹map ∘ (ΩKn+1→Kn 1))
                ((Kn→ΩKn+1 1) ∘ f) ((Kn→ΩKn+1 1) ∘ g)
                (cong (Kn→ΩKn+1 1) reflf ∙ Kn→ΩKn+10ₖ 1) (cong (Kn→ΩKn+1 1) reflg ∙ Kn→ΩKn+10ₖ 1)
              ∙ λ j → guy (Iso.leftInv (Iso-Kn-ΩKn+1 1) (f base) j)
                          (λ i → S¹map (Iso.leftInv (Iso-Kn-ΩKn+1 1) (f (loop i)) j))
                    ∙ guy (Iso.leftInv (Iso-Kn-ΩKn+1 1) (g base) j)
                          (λ i → S¹map (Iso.leftInv (Iso-Kn-ΩKn+1 1) (g (loop i)) j)))
  inv theIso a = ∣ (F⁻ (base , a)) ∣₂
  rightInv theIso a = cong snd (Iso.rightInv S¹→S¹≡S¹×Int (base , a))
  leftInv theIso = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                          λ f → cong ((sRec setTruncIsSet ∣_∣₂)
                                        ∘ sRec setTruncIsSet λ x → ∣ F⁻ (x , (snd (F f))) ∣₂)
                                      (Iso.inv PathIdTrunc₀Iso (isConnectedS¹ (fst (F f))))
                              ∙ cong ∣_∣₂ (Iso.leftInv S¹→S¹≡S¹×Int f)

---------------------------- Hⁿ(Sⁿ) ≅ ℤ , n ≥ 1 -------------------

Hⁿ-Sⁿ≅ℤ : (n : ℕ) → GroupIso intGroup (coHomGr (suc n) (S₊ (suc n)))
Hⁿ-Sⁿ≅ℤ zero = invGroupIso coHom1S1≃ℤ
Hⁿ-Sⁿ≅ℤ (suc n) =
    Hⁿ-Sⁿ≅ℤ n
  □ vSES→GroupIso _ _ theIso
  □ invGroupIso (coHomPushout≅coHomSn (suc n) (suc (suc n)))
  where
  module K = MV Unit Unit (S₊ (suc n)) (λ _ → tt) (λ _ → tt)
  theIso : vSES (coHomGr (suc n) (S₊ (suc n))) (coHomGr (suc (suc n))
                (Pushout {A = S₊ (suc n)} (λ _ → tt) (λ _ → tt)))
                _
                _
  isTrivialLeft theIso p q = ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit n) (fst p) (fst q)
                                        , isOfHLevelSuc 0 (isContrHⁿ-Unit n) (snd p) (snd q))
  isTrivialRight theIso p q = ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)) (fst p) (fst q)
                                         , isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)) (snd p) (snd q))
  left theIso = K.Δ (suc n)
  right theIso = K.i (2 + n)
  vSES.ϕ theIso = K.d (suc n)
  Ker-ϕ⊂Im-left theIso = K.Ker-d⊂Im-Δ  (suc n)
  Ker-right⊂Im-ϕ theIso = K.Ker-i⊂Im-d (suc n)

{- More standard proof of H¹(S¹) ≅ ℤ using Mayer-Vietoris.
This is much slower than the direct proof, but let's keep it here for completeness.

-- --------------------------H¹(S¹) -----------------------------------
{-
In order to apply Mayer-Vietoris, we need the following lemma.
Given the following diagram
  a ↦ (a , 0)   ψ         ϕ
 A -->  A × A -------> B --->  C
If ψ is an isomorphism and ϕ is surjective with ker ϕ ≡ {ψ (a , a) ∣ a ∈ A}, then C ≅ B
-}

diagonalIso : ∀ {ℓ ℓ' ℓ''} {A : Group {ℓ}} (B : Group {ℓ'}) {C : Group {ℓ''}}
               (ψ : GroupIso (dirProd A A) B) (ϕ : GroupHom B C)
             → isSurjective _ _ ϕ
             → ((x : ⟨ B ⟩) → isInKer B C ϕ x
                                    → ∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
             → ((x : ⟨ B ⟩) → (∃[ y ∈ ⟨ A ⟩ ] x ≡ (fun (map ψ)) (y , y))
                                    → isInKer B C ϕ x)
             → GroupIso A C
diagonalIso {A = A} B {C = C} ψ ϕ issurj ker→diag diag→ker = BijectionIsoToGroupIso bijIso
  where
  open GroupStr
  module A = GroupStr (snd A)
  module B = GroupStr (snd B)
  module C = GroupStr (snd C)
  module A×A = GroupStr (snd (dirProd A A))
  module ψ = GroupIso ψ
  module ϕ = GroupHom ϕ
  ψ⁻ = inv ψ

  fstProj : GroupHom A (dirProd A A)
  fun fstProj a = a , GroupStr.0g (snd A)
  isHom fstProj g0 g1 i = (g0 A.+ g1) , GroupStr.lid (snd A) (GroupStr.0g (snd A)) (~ i)

  bijIso : BijectionIso A C
  map' bijIso = compGroupHom fstProj (compGroupHom (map ψ) ϕ)
  inj bijIso a inker = pRec (isSetCarrier A _ _)
                             (λ {(a' , id) → (cong fst (sym (leftInv ψ (a , GroupStr.0g (snd A))) ∙∙ cong ψ⁻ id ∙∙ leftInv ψ (a' , a')))
                                           ∙ cong snd (sym (leftInv ψ (a' , a')) ∙∙ cong ψ⁻ (sym id) ∙∙ leftInv ψ (a , GroupStr.0g (snd A)))})
                             (ker→diag _ inker)
  surj bijIso c =
    pRec propTruncIsProp
         (λ { (b , id) → ∣ (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)))
                          , ((sym (GroupStr.rid (snd C) _)
                           ∙∙ cong ((fun ϕ) ((fun (map ψ)) (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)) , GroupStr.0g (snd A))) C.+_)
                                  (sym (diag→ker (fun (map ψ) ((snd (ψ⁻ b)) , (snd (ψ⁻ b))))
                                                  ∣ (snd (ψ⁻ b)) , refl ∣₁))
                           ∙∙ sym ((isHom ϕ) _ _))
                           ∙∙ cong (fun ϕ) (sym ((isHom (map ψ)) _ _)
                                        ∙∙ cong (fun (map ψ)) (ΣPathP (sym (GroupStr.assoc (snd A) _ _ _)
                                                                           ∙∙ cong (fst (ψ⁻ b) A.+_) (GroupStr.invl (snd A) _)
                                                                           ∙∙ GroupStr.rid (snd A) _
                                                                        , (GroupStr.lid (snd A) _)))
                                        ∙∙ rightInv ψ b)
                           ∙∙ id) ∣₁ })
         (issurj c)

H¹-S¹≅ℤ : GroupIso intGroup (coHomGr 1 (S₊ 1))
H¹-S¹≅ℤ =
    diagonalIso (coHomGr 0 (S₊ 0))
                (invGroupIso H⁰-S⁰≅ℤ×ℤ)
                (K.d 0)
                (λ x → K.Ker-i⊂Im-d 0 x
                                     (ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _
                                            , isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _)))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                        (λ x inker
                            → pRec propTruncIsProp
                                    (λ {((f , g) , id') → helper x f g id' inker})
                                    ((K.Ker-d⊂Im-Δ 0 ∣ x ∣₂ inker)))))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                         λ F surj
                           → pRec (setTruncIsSet _ _)
                                   (λ { (x , id) → K.Im-Δ⊂Ker-d 0 ∣ F ∣₂
                                                      ∣ (∣ (λ _ → x) ∣₂ , ∣ (λ _ → 0) ∣₂) ,
                                                       (cong ∣_∣₂ (funExt (surjHelper x))) ∙ sym id ∣₁ })
                                   surj) )
  □ invGroupIso (coHomPushout≅coHomSn 0 1)
  where
  module K = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)

  surjHelper :  (x : Int) (x₁ : S₊ 0) → x -[ 0 ]ₖ 0 ≡ S0→Int (x , x) x₁
  surjHelper x true = Iso.leftInv (Iso-Kn-ΩKn+1 0) x
  surjHelper x false = Iso.leftInv (Iso-Kn-ΩKn+1 0) x

  helper : (F : S₊ 0 → Int) (f g : ∥ (Unit → Int) ∥₂)
           (id : GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂)
         → isInKer (coHomGr 0 (S₊ 0))
                    (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
                    (K.d 0)
                    ∣ F ∣₂
         → ∃[ x ∈ Int ] ∣ F ∣₂ ≡ inv H⁰-S⁰≅ℤ×ℤ (x , x)
  helper F =
    sElim2 (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
           λ f g id inker
             → pRec propTruncIsProp
                     (λ ((a , b) , id2)
                        → sElim2 {C = λ f g → GroupHom.fun (K.Δ 0) (f , g) ≡ ∣ F ∣₂ → _ }
                                  (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                                  (λ f g id → ∣ (helper2 f g .fst) , (sym id ∙ sym (helper2 f g .snd)) ∣₁)
                                  a b id2)
                     (MV.Ker-d⊂Im-Δ _ _ (S₊ 0) (λ _ → tt) (λ _ → tt) 0 ∣ F ∣₂ inker)
    where
    helper2 : (f g : Unit → Int)
            → Σ[ x ∈ Int ] (inv H⁰-S⁰≅ℤ×ℤ (x , x))
             ≡ GroupHom.fun (K.Δ 0) (∣ f ∣₂ , ∣ g ∣₂)
    helper2 f g = (f _ -[ 0 ]ₖ g _) , cong ∣_∣₂ (funExt λ {true → refl ; false → refl})

-}

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


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

module Coinduction where

infix 1000 ♯_

postulate
  ∞  : ∀ {i} (A : Set i) → Set i
  ♯_ : ∀ {i} {A : Set i} → A → ∞ A
  ♭  : ∀ {i} {A : Set i} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Empty.Polymorphic where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

import Cubical.Data.Empty as Empty

⊥ : ∀ {ℓ} → Type ℓ
⊥ = Lift Empty.⊥

⊥-elim : ∀ {w ℓ} {Whatever : ⊥ {ℓ} → Type w} → (witness : ⊥ {ℓ}) → Whatever witness
⊥-elim ()

isProp⊥ : ∀ {ℓ} → isProp (⊥ {ℓ})
isProp⊥ ()

isContr⊥→A : ∀ {ℓ ℓ′} {A : Type ℓ′} → isContr (⊥ {ℓ} → A)
fst isContr⊥→A ()
snd isContr⊥→A f i ()


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.DirectSumHIT
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

private variable
  ℓ ℓ' : Level

-----------------------------------------------------------------------------
-- Def, notation, lemma

module GradedRing-⊕HIT-index
  (IdM@(Idx , IdxStr) : Monoid ℓ)
  (G : (n : Idx) → Type ℓ')
  (Gstr : (n : Idx) → AbGroupStr (G n))
  where

  ⊕G-AbGroup = ⊕HIT-AbGr Idx G Gstr
  ⊕G = ⊕HIT Idx G Gstr

  open MonoidStr IdxStr renaming (is-set to isSetIdx)
  open AbGroupStr (snd ⊕G-AbGroup)
    renaming
    ( 0g     to 0⊕
    ; _+_    to _+⊕_
    ; -_     to -⊕_
    ; +Assoc to +⊕Assoc
    ; +IdR   to +⊕IdR
    ; +IdL   to +⊕IdL
    ; +InvR  to +⊕InvR
    ; +InvL  to +⊕InvL
    ; +Comm  to +⊕Comm
    ; is-set to isSet⊕G )
  open AbGroupTheory ⊕G-AbGroup

  open AbGroupStr
    renaming
    ( +Assoc to +Assoc
    ; +IdR   to +IdR
    ; +IdL   to +IdL
    ; +InvR  to +InvR
    ; +InvL  to +InvL
    ; +Comm  to +Comm
    ; is-set to isSetG )

  module GradedRing-⊕HIT-⋆
    (1⋆      : G ε)
    (_⋆_     : {k l : Idx} → G k → G l → G (k · l))
    (0-⋆     : {k l : Idx} → (b : G l) → (0g (Gstr k)) ⋆ b ≡ 0g (Gstr (k · l)))
    (⋆-0     : {k l : Idx} → (a : G k) → a ⋆ (0g (Gstr l)) ≡ 0g (Gstr (k · l)))
    (⋆Assoc  : {k l m : Idx} → (a : G k) → (b : G l) → (c : G m) →
                _≡_ {A = Σ[ k ∈ Idx ] G k} ((k · (l · m)) , (a ⋆ (b ⋆ c))) (((k · l) · m) , ((a ⋆ b) ⋆ c)))
    (⋆IdR    : {k : Idx} → (a : G k) → _≡_ {A = Σ[ k ∈ Idx ] G k} ( k · ε , a ⋆ 1⋆ ) (k , a))
    (⋆IdL    : {l : Idx} → (b : G l) → _≡_ {A = Σ[ k ∈ Idx ] G k} ( ε · l , 1⋆ ⋆ b ) (l , b))
    (⋆DistR+ : {k l : Idx} → (a : G k) → (b c : G l) →
               a ⋆ ((Gstr l) ._+_ b c) ≡ Gstr (k · l) ._+_ (a ⋆ b) (a ⋆ c))
    (⋆DistL+ : {k l : Idx} → (a b : G k) → (c : G l) →
               ((Gstr k) ._+_ a b) ⋆ c ≡ Gstr (k · l) ._+_ (a ⋆ c) (b ⋆ c))
    where

-----------------------------------------------------------------------------
-- Ring Properties

    _prod_ : ⊕G → ⊕G → ⊕G
    _prod_ = DS-Rec-Set.f _ _ _ _ (isSetΠ λ _ → isSet⊕G)
             (λ _ → 0⊕)
             (λ k a → DS-Rec-Set.f _ _ _ _ isSet⊕G
                       0⊕
                       (λ l b → base (k · l) (a ⋆ b))
                       _+⊕_
                       +⊕Assoc
                       +⊕IdR
                       +⊕Comm
                       (λ l → cong (base (k · l)) (⋆-0 a) ∙ base-neutral _)
                       λ l b c → base-add _ _ _ ∙ cong (base (k · l)) (sym (⋆DistR+ _ _ _)))
             (λ xs ys y → (xs y) +⊕ (ys y))
             (λ xs ys zs i y → +⊕Assoc (xs y) (ys y) (zs y) i)
             (λ xs i y       → +⊕IdR (xs y) i)
             (λ xs ys i y    → +⊕Comm (xs y) (ys y) i)
             (λ k → funExt (DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕G _ _)
                     refl
                     (λ l b → cong (base (k · l)) (0-⋆ _) ∙ base-neutral _)
                     λ {U V} ind-U ind-V → cong₂ _+⊕_ ind-U ind-V ∙ +⊕IdR _))
             λ k a b → funExt (DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕G _ _)
                        (+⊕IdR _)
                        (λ l c → base-add _ _ _ ∙ cong (base (k · l)) (sym (⋆DistL+ _ _ _)))
                        (λ {U V} ind-U ind-V → comm-4 _ _ _ _ ∙ cong₂ _+⊕_ ind-U ind-V))

    1⊕ : ⊕G
    1⊕ = base ε 1⋆

    prodAssoc : (x y z : ⊕G) → x prod (y prod z) ≡ (x prod y) prod z
    prodAssoc = DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ2 λ _ _ → isSet⊕G _ _)
                (λ _ _ → refl)
                (λ k a → DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ (λ _ → isSet⊕G _ _))
                          (λ z → refl)
                          (λ l b → DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕G _ _)
                                    refl
                                    (λ m c → cong₂ base (cong fst (⋆Assoc _ _ _)) (cong snd (⋆Assoc _ _ _)))
                                    λ {U V} ind-U ind-V → cong₂ _+⊕_ ind-U ind-V)
                          λ {U V} ind-U ind-V z → cong₂ _+⊕_ (ind-U z) (ind-V z))
                λ {U V} ind-U ind-V y z → cong₂ _+⊕_ (ind-U y z) (ind-V y z)

    prodIdR : (x : ⊕G) → x prod 1⊕ ≡ x
    prodIdR = DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕G _ _)
              refl
              (λ k a → cong₂ base (cong fst (⋆IdR _)) (cong snd (⋆IdR _)) )
              λ {U V} ind-U ind-V → (cong₂ _+⊕_ ind-U ind-V)

    prodIdL : (y : ⊕G) → 1⊕ prod y ≡ y
    prodIdL = DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕G _ _)
              refl
              (λ l b → cong₂ base (cong fst (⋆IdL _)) (cong snd (⋆IdL _)) )
              λ {U V} ind-U ind-V → (cong₂ _+⊕_ ind-U ind-V)

    prodDistR+ : (x y z : ⊕G) → x prod (y +⊕ z) ≡ (x prod y) +⊕ (x prod z)
    prodDistR+ = DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ2 (λ _ _ → isSet⊕G _ _))
                 (λ _ _ → sym (+⊕IdR _))
                 (λ k a y z → refl)
                 λ {U V} ind-U ind-V y z → cong₂ _+⊕_ (ind-U y z) (ind-V y z) ∙ comm-4 _ _ _ _

    prodDistL+ : (x y z : ⊕G) → (x +⊕ y) prod z ≡ (x prod z) +⊕ (y prod z)
    prodDistL+ = λ x y z → refl

-----------------------------------------------------------------------------
-- Ring Instances

    ⊕HITgradedRing-Ring : Ring (ℓ-max ℓ ℓ')
    fst ⊕HITgradedRing-Ring = ⊕G
    RingStr.0r (snd ⊕HITgradedRing-Ring) = 0⊕
    RingStr.1r (snd ⊕HITgradedRing-Ring) = 1⊕
    RingStr._+_ (snd ⊕HITgradedRing-Ring) = _+⊕_
    RingStr._·_ (snd ⊕HITgradedRing-Ring) = _prod_
    RingStr.- snd ⊕HITgradedRing-Ring = -⊕_
    RingStr.isRing (snd ⊕HITgradedRing-Ring) = makeIsRing isSet⊕G
                                               +⊕Assoc +⊕IdR +⊕InvR +⊕Comm
                                               prodAssoc prodIdR prodIdL prodDistR+ prodDistL+

-----------------------------------------------------------------------------
-- CommRing extension

    module ExtensionCommRing
      (⋆Comm : {k l : Idx} → (a : G k) → (b : G l) →
               _≡_ {A = Σ[ k ∈ Idx ] G k} ((k · l) , (a ⋆ b)) ((l · k) , (b ⋆ a)))
      where

      open RingTheory ⊕HITgradedRing-Ring

      prodComm : (x y : ⊕G) → x prod y ≡ y prod x
      prodComm = DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ (λ _ → isSet⊕G _ _))
                 (λ y → sym (0RightAnnihilates y))
                 (λ k a → DS-Ind-Prop.f _ _ _ _ (λ _ → isSet⊕G _ _)
                           refl
                           (λ l b → cong₂ base (cong fst (⋆Comm _ _)) (cong snd (⋆Comm _ _)))
                           λ {U V} ind-U ind-V → cong₂ _+⊕_ ind-U ind-V)
                 λ {U V} ind-U ind-V Q → ((cong₂ _+⊕_ (ind-U Q) (ind-V Q)) ∙ sym (prodDistR+ Q U V))

      ⊕HITgradedRing-CommRing : CommRing (ℓ-max ℓ ℓ')
      ⊕HITgradedRing-CommRing = Ring→CommRing ⊕HITgradedRing-Ring prodComm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K --safe #-}
open import Axiom.Extensionality.Propositional using (Extensionality)

module Cats.Category.Sets.Facts
  (funext : ∀ {a b} → Extensionality a b)
  where

open import Cats.Category.Sets.Facts.Exponential funext public using (hasExponentials)
open import Cats.Category.Sets.Facts.Initial public using (hasInitial)
open import Cats.Category.Sets.Facts.Product public using
  (hasBinaryProducts ; hasFiniteProducts)
open import Cats.Category.Sets.Facts.Terminal public using (hasTerminal)

open import Cats.Category
open import Cats.Category.Sets using (Sets)

instance
  isCCC : ∀ {l} → IsCCC (Sets l)
  isCCC = record {}

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

module Relation.Unary where

open import Relation.Nullary.Decidable
open import Level
open import Path

Decidable : (A → Type b) → Type _
Decidable P = ∀ x → Dec (P x)

AtMostOne : (A → Type b) → Type _
AtMostOne P = ∀ x y → P x → P y → x ≡ y

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Common.Prelude hiding (pred)
open import Common.Reflection
open import Common.Equality

un-function : Definition → FunDef
un-function (funDef cs) = funDef unknown cs
un-function _           = funDef unknown []

data Is-suc : Nat → Set where
  is-suc : ∀ n → Is-suc (suc n)

pred : (n : Nat) → Is-suc n → Nat
pred ._ (is-suc n) = n

pred-def : FunDef
pred-def =
  funDef (quoteTerm ((n : Nat) → Is-suc n → Nat))
         (clause (vArg dot ∷ vArg (con (quote is-suc) (vArg (var "n") ∷ [])) ∷ [])
                 (var 0 []) ∷ [])

data Is-zero : Nat → Set where
  is-zero : Is-zero zero

f : (n : Nat) → Is-zero n → Nat
f ._ is-zero = zero

f-def : FunDef
f-def =
  funDef (quoteTerm ((n : Nat) → Is-zero n → Nat))
         (clause (vArg dot ∷ vArg (con (quote is-zero) []) ∷ [])
                 (con (quote zero) []) ∷ [])

unquoteDecl pred' = define (vArg pred') pred-def
unquoteDecl f'    = define (vArg f')    f-def

check-pred : pred' 4 (is-suc _) ≡ 3
check-pred = refl

check-f : f' 0 is-zero ≡ 0
check-f = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Prelude renaming (_<_ to _N<_)

module Implicits.Resolution.GenericFinite.Algorithm where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Vec
open import Data.List
open import Data.Fin.Substitution
open import Data.Nat.Base using (_<′_)
open import Data.Maybe
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming (refl to ≤-refl; trans to ≤-trans)

open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.GenericFinite.Resolution
open import Implicits.Resolution.GenericFinite.TerminationCondition
open import Implicits.Resolution.Termination

private
  module M = MetaTypeMetaSubst

module Lemmas where
  m<-Acc : ∀ {m ν} → MetaType m ν → Set
  m<-Acc {m} {ν} r = Acc _m<_ (m , ν , r)

  ρ<-Acc : ∀ {ν} → Type ν → Set
  ρ<-Acc {ν} r = Acc _ρ<_ (ν , r)

  module Arg<-well-founded  where
    open Lexicographic (_N<_) (const _ρ<_)

    open import Induction.Nat
    open import Data.Nat.Properties
    module image = Subrelation {A = ℕ} {_N<_} {_<′_} ≤⇒≤′

    arg<-well-founded : Well-founded _<_
    arg<-well-founded = well-founded (image.well-founded <-well-founded) ρ<-well-founded

    _arg<_ = _<_

    -- Accessibility of the 'goal' type during resolution.
    -- Either the *head* of the goal shrinks (Oliveira's termination condition)
    -- Or the head size remains equal and the goal shrinks in an absolute sense.
    Arg<-Acc : ∀ {ν} → Type ν → Set
    Arg<-Acc a = Acc _arg<_ (h|| a || , (, a))

  open Arg<-well-founded using (Arg<-Acc; arg<-well-founded) public

open Lemmas

module ResolutionAlgorithm (cond : TerminationCondition) where
  open TerminationCondition cond
  open ResolutionRules cond

  mutual

    match' : ∀ {m ν} (Δ : ICtx ν) (Φ : TCtx) τ → (r : MetaType m ν) →
            T-Acc Φ →
            m<-Acc r →
            Maybe (Sub (flip MetaType ν) m zero)
    match' Δ Φ τ (simpl x) f g = mgu (simpl x) τ

    match' Δ Φ τ (a ⇒ b) f (acc g) with match' Δ Φ τ b f (g _ (b-m<-a⇒b a b))
    match' Δ Φ τ (a ⇒ b) f (acc g) | nothing = nothing
    match' Δ Φ τ (a ⇒ b) f (acc g) | just u
      with (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ) <? Φ
    match' Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | yes Φ<
      with resolve' Δ (step Φ Δ (from-meta (a M./ u)) (from-meta (b M./ u)) τ)
                    (from-meta (a M./ u)) (f _ Φ<)
    match' Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | yes Φ< | true = just u
    match' Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | yes Φ< | false = nothing
    match' Δ Φ τ (a ⇒ b) (acc f) (acc g) | just u | no φ> = nothing

    match' Δ Φ τ (∀' a) f (acc g) with match' Δ Φ τ (open-meta a) f (g _ (open-meta-a-m<-∀'a a))
    match' Δ Φ τ (∀' a) f (acc g) | just p = just (tail p)
    match' Δ Φ τ (∀' r) f (acc g) | nothing = nothing

    -- match defers to match', which concerns itself with MetaTypes.
    -- If match' finds a match, we can use the fact that we have zero unification variables open here
    -- to show that we found the right thing.
    match : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) τ r → T-Acc Φ → Bool
    match Δ Φ τ a f = is-just (match' Δ Φ τ (to-meta {zero} a) f (m<-well-founded _))

    match1st : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) (ρs : ICtx ν) → (τ : SimpleType ν) → T-Acc Φ → Bool
    match1st Δ Φ [] τ Φ↓ = false
    match1st Δ Φ (x ∷ xs) τ Φ↓ with match Δ Φ τ x Φ↓
    match1st Δ Φ (x ∷ xs) τ Φ↓ | true = true
    match1st Δ Φ (x ∷ xs) τ Φ↓ | false = match1st Δ Φ xs τ Φ↓

    resolve' : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) r → T-Acc Φ → Bool
    resolve' Δ Φ (simpl x) Φ↓ = match1st Δ Φ Δ x Φ↓
    resolve' Δ Φ (a ⇒ b) Φ↓ = resolve' (a ∷ Δ) Φ b Φ↓
    resolve' Δ Φ (∀' r) Φ↓ = resolve' (ictx-weaken Δ) Φ r Φ↓

    resolve : ∀ {ν} (Δ : ICtx ν) (Φ : TCtx) r → Bool
    resolve Δ Φ r = resolve' Δ Φ r (wf-< Φ)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- List Zipper-related properties
------------------------------------------------------------------------

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

module Data.List.Zipper.Properties where

open import Data.List.Base as List using (List ; [] ; _∷_)
open import Data.List.Properties
open import Data.List.Zipper
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function

-- Invariant: Zipper represents a given list
------------------------------------------------------------------------

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

 -- Stability under moving left or right

 toList-left-identity : (zp : Zipper A) → All ((_≡_ on toList) zp) (left zp)
 toList-left-identity (mkZipper []        val) = nothing
 toList-left-identity (mkZipper (x ∷ ctx) val) = just $′ begin
   List.reverse (x ∷ ctx) List.++ val
     ≡⟨ cong (List._++ val) (unfold-reverse x ctx) ⟩
   (List.reverse ctx List.++ List.[ x ]) List.++ val
     ≡⟨ ++-assoc (List.reverse ctx) List.[ x ] val ⟩
   toList (mkZipper ctx (x ∷ val))
     ∎

 toList-right-identity : (zp : Zipper A) → All ((_≡_ on toList) zp) (right zp)
 toList-right-identity (mkZipper ctx [])        = nothing
 toList-right-identity (mkZipper ctx (x ∷ val)) = just $′ begin
   List.reverse ctx List.++ x ∷ val
     ≡⟨ sym (++-assoc (List.reverse ctx) List.[ x ] val) ⟩
   (List.reverse ctx List.++ List.[ x ]) List.++ val
     ≡⟨ cong (List._++ val) (sym (unfold-reverse x ctx)) ⟩
   List.reverse (x ∷ ctx) List.++ val
     ∎

 -- Applying reverse does correspond to reversing the represented list

 toList-reverse-commute : (zp : Zipper A) → toList (reverse zp) ≡ List.reverse (toList zp)
 toList-reverse-commute (mkZipper ctx val) = begin
   List.reverse val List.++ ctx
     ≡⟨ cong (List.reverse val List.++_) (sym (reverse-involutive ctx)) ⟩
   List.reverse val List.++ List.reverse (List.reverse ctx)
     ≡⟨ sym (reverse-++-commute (List.reverse ctx) val) ⟩
   List.reverse (List.reverse ctx List.++ val)
     ∎

-- Properties of the insertion functions
------------------------------------------------------------------------

 -- _ˡ++_ properties

 toList-ˡ++-commute : ∀ xs (zp : Zipper A) → toList (xs ˡ++ zp) ≡ xs List.++ toList zp
 toList-ˡ++-commute xs (mkZipper ctx val) = begin
   List.reverse (ctx List.++ List.reverse xs) List.++ val
     ≡⟨ cong (List._++ _) (reverse-++-commute ctx (List.reverse xs)) ⟩
   (List.reverse (List.reverse xs) List.++ List.reverse ctx) List.++ val
     ≡⟨ ++-assoc (List.reverse (List.reverse xs)) (List.reverse ctx) val ⟩
   List.reverse (List.reverse xs) List.++ List.reverse ctx List.++ val
     ≡⟨ cong (List._++ _) (reverse-involutive xs) ⟩
   xs List.++ List.reverse ctx List.++ val
     ∎

 ˡ++-assoc : ∀ xs ys (zp : Zipper A) → xs ˡ++ (ys ˡ++ zp) ≡ (xs List.++ ys) ˡ++ zp
 ˡ++-assoc xs ys (mkZipper ctx val) = cong (λ ctx → mkZipper ctx val) $ begin
   (ctx List.++ List.reverse ys) List.++ List.reverse xs
     ≡⟨ ++-assoc ctx _ _ ⟩
   ctx List.++ List.reverse ys List.++ List.reverse xs
     ≡⟨ cong (ctx List.++_) (sym (reverse-++-commute xs ys)) ⟩
   ctx List.++ List.reverse (xs List.++ ys)
     ∎

 -- _ʳ++_ properties

 ʳ++-assoc : ∀ xs ys (zp : Zipper A) → xs ʳ++ (ys ʳ++ zp) ≡ (ys List.++ xs) ʳ++ zp
 ʳ++-assoc xs ys (mkZipper ctx val) =  cong (λ ctx → mkZipper ctx val) $ begin
   List.reverse xs List.++ List.reverse ys List.++ ctx
     ≡⟨ sym (++-assoc (List.reverse xs) (List.reverse ys) ctx) ⟩
   (List.reverse xs List.++ List.reverse ys) List.++ ctx
     ≡⟨ cong (List._++ ctx) (sym (reverse-++-commute ys xs)) ⟩
   List.reverse (ys List.++ xs) List.++ ctx
     ∎

 -- _++ˡ_ properties

 ++ˡ-assoc : ∀ xs ys (zp : Zipper A) → zp ++ˡ xs ++ˡ ys ≡ zp ++ˡ (ys List.++ xs)
 ++ˡ-assoc xs ys (mkZipper ctx val) =  cong (mkZipper ctx) $ sym $ ++-assoc ys xs val

 -- _++ʳ_ properties

 toList-++ʳ-commute : ∀ (zp : Zipper A) xs → toList (zp ++ʳ xs) ≡ toList zp List.++ xs
 toList-++ʳ-commute (mkZipper ctx val) xs = begin
   List.reverse ctx List.++ val List.++ xs
     ≡⟨ sym (++-assoc (List.reverse ctx) val xs) ⟩
   (List.reverse ctx List.++ val) List.++ xs
     ∎

 ++ʳ-assoc : ∀ xs ys (zp : Zipper A) → zp ++ʳ xs ++ʳ ys ≡ zp ++ʳ (xs List.++ ys)
 ++ʳ-assoc xs ys (mkZipper ctx val) = cong (mkZipper ctx) $ ++-assoc val xs ys

-- List-like operations indeed correspond to their counterparts
------------------------------------------------------------------------

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

 toList-map-commute : ∀ (f : A → B) zp → toList (map f zp) ≡ List.map f (toList zp)
 toList-map-commute f zp@(mkZipper ctx val) = begin
   List.reverse (List.map f ctx) List.++ List.map f val
     ≡⟨ cong (List._++ _) (sym (reverse-map-commute f ctx)) ⟩
   List.map f (List.reverse ctx) List.++ List.map f val
     ≡⟨ sym (map-++-commute f (List.reverse ctx) val) ⟩
   List.map f (List.reverse ctx List.++ val)
     ∎

 toList-foldr-commute : ∀ (c : A → B → B) n zp → foldr c n zp ≡ List.foldr c n (toList zp)
 toList-foldr-commute c n (mkZipper ctx val) = begin
   List.foldl (flip c) (List.foldr c n val) ctx
     ≡⟨ sym (reverse-foldr c (List.foldr c n val) ctx) ⟩
   List.foldr c (List.foldr c n val) (List.reverse ctx)
     ≡⟨ sym (foldr-++ c n (List.reverse ctx) val) ⟩
   List.foldr c n (List.reverse ctx List.++ val)
     ∎


text:
module ImplicitRecordFields where

record R (X Y : Set) : Set₁ where
  field
    {A}         : Set
    f           : A → A
    {B C} D {E} : Set
    g           : B → C → E → X → Y

postulate A : Set

r : R A A
r = record
  { f = f
  ; B = A
  ; D = A
  ; g = λ (_ _ _ : _) → f
  }
  where
  f : A → A
  f x = x

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

lemma₁ : r ≡ record {}
lemma₁ = refl

lemma₂ : R.B r ≡ A
lemma₂ = refl


text:
-- Interpretation of partial weakenings as partial finite maps.

module Dimension.PartialWeakening.Model (E : Set) where

import Level

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Fin using (Fin; zero; suc)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Axiom.FunctionExtensionality

open import Control.Category
open import Control.Category.Functor

open import Control.Kleisli
open import Control.Monad using (IsMonad; module IsMonad)
import Control.Monad.Error as Err
open module Error = Err E using (Error; fail; return; errorIsMonad)

-- open import Dimension.PartialWeakening E  -- horrible names
import Dimension.PartialWeakening as PW
open module PWeak = PW E

open IsMonad errorIsMonad hiding (return)
module Kl = IsCategory (kleisliIsCategory errorIsMonad)

-- Semantics given by application to a name in Fin n

apply : ∀ {n m} (f : PWeak n m) (i : Fin n) → Error (Fin m)
apply []       ()
apply (e ∷ f)  zero    = fail e
apply (e ∷ f)  (suc i) = apply f i
apply (lift f) zero    = return zero
apply (lift f) (suc i) = suc <$> apply f i
apply (weak f) i       = suc <$> apply f i

-- Soundness of id

abstract
  apply-id : ∀ n (i : Fin n) → apply id i ≡ return i
  apply-id 0       ()
  apply-id (suc n) zero    = refl
  apply-id (suc n) (suc i) with (apply id i) | (apply-id n i)
  apply-id (suc n) (suc i) | .(return i) | refl = refl

-- Lemma: one inductive step

abstract
  lift-lift-suc : ∀ {n m l} (f : PWeak n m) {g : PWeak m l} {i : Fin n} →

    (ih : apply (comp f g) i ≡ apply f i >>= apply g) →

    apply (comp (lift f) (lift g)) (suc i)  ≡
    apply (lift f) (suc i) >>= apply (lift g)

  lift-lift-suc f {g = g} {i = i} ih = begin

      apply (comp (lift f) (lift g)) (suc i)

    ≡⟨⟩                                      -- definition of comp

      apply (lift (comp f g)) (suc i)

    ≡⟨⟩                                      -- definition of apply

      suc <$> apply (comp f g) i

    ≡⟨ cong (_<$>_ suc) ih ⟩                 -- induction hypothesis

      suc <$> (apply f i >>= apply g)

    ≡⟨ map-after-bind (apply f i) ⟩          -- map commutes with bind I

      (apply f i >>= λ j → suc <$> apply g j)

    ≡⟨⟩                                      -- definition of apply

      (apply f i >>= λ j → apply (lift g) (suc j))

    ≡⟨ sym (bind-after-map (apply f i)) ⟩    -- map commutes with bind II

      (suc <$> apply f i) >>= apply (lift g)

    ≡⟨⟩                                      -- definition of apply

      apply (lift f) (suc i) >>= apply (lift g)
    ∎

-- Soundness of comp

abstract
  apply-comp : ∀ {n m l} (f : PWeak n m) (g : PWeak m l) (i : Fin n) →

   apply (comp f g) i ≡ apply f i >>= apply g

  apply-comp [] g ()
  apply-comp (e ∷ f) g zero = refl
  apply-comp (e ∷ f) g (suc i) = apply-comp f g i
  apply-comp (lift f) (e ∷ g) zero = refl
  apply-comp (lift f) (e ∷ g) (suc i) rewrite apply-comp f g i with apply f i
  ... | fail e′  = refl
  ... | return j = refl
  apply-comp (lift f) (lift g) zero = refl
  apply-comp (lift f) (lift g) (suc i) = lift-lift-suc f (apply-comp f g i)
  apply-comp (lift f) (weak g) i = begin

      suc <$> apply (comp (lift f) g) i

    ≡⟨ cong (_<$>_ suc) (apply-comp (lift f) g i) ⟩  -- ind. hyp.

      suc <$> (apply (lift f) i >>= apply g)

    ≡⟨ map-after-bind (apply (lift f) i) ⟩           -- move map

      apply (lift f) i >>= (λ j → suc <$> apply g j)
    ∎

  apply-comp (weak f) (e ∷ g) i rewrite apply-comp f g i = sym (bind-after-map (apply f i))

  apply-comp (weak f) (lift g) i rewrite apply-comp f g i = begin

      suc <$> (apply f i >>= apply g)

    ≡⟨ map-after-bind (apply f i) ⟩

      apply f i >>= (λ j → suc <$> apply g j)

    ≡⟨⟩

      apply f i >>= (λ j → apply (lift g) (suc j))

    ≡⟨ sym (bind-after-map (apply f i)) ⟩

      (suc <$> apply f i) >>= apply (lift g)
    ∎

  apply-comp (weak f) (weak g) i rewrite apply-comp (weak f) g i =
    map-after-bind (apply (weak f) i)

-- The Kleisli category of partial finite maps  Fin n → Error (Fin m)

PFin : (n m : ℕ) → Set
PFin n m = Fin n → Error (Fin m)

SPFin = λ n m → setoid (PFin n m)

pFinIsCategory : IsCategory SPFin
pFinIsCategory = record
  { ops = record
    { id  = return
    ; _⟫_ = λ f g a → f a >>= g
    }
  ; laws = record
    { id-first = fun-ext (bind-β _)
    ; id-last  = fun-ext (λ a → bind-η _)
    ; ∘-assoc  = λ f → fun-ext (λ a → bind-assoc (f a))
    ; ∘-cong   = λ{ refl refl → refl }
    }
  }

PFIN : Category _ _ _
PFIN = record { Hom = SPFin; isCategory = pFinIsCategory }

-- The evaluation functor

-- ⟦_⟧ : ∀ {n m} → PWeak n m → PFin n m
-- ⟦ f ⟧ = apply f

applyIsFunctor : IsFunctor {C = PWEAK} {D = PFIN} (λ n → n)
applyIsFunctor = record
  { ops  = record
    { map = apply
    }
  ; laws = record
    { map-id = fun-ext (apply-id _)
    ; map-∘  = λ f → fun-ext (apply-comp f _)
    }
  }

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical