text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

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

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
 using (_≅_; ≅-to-≡; ≡-to-≅; _≇_)
 renaming (cong to ≅-cong; refl to ≅-refl; cong₂ to ≅-cong₂)

open import Function

-- This module proves a number of properties about even numbers.
-- We borrow some things from Data.Nat.Divisibility but specialize most
-- of them to divisibility-by-2.
module Data.Nat.Even where

 open import AAOSL.Lemmas

 Even : ℕ → Set
 Even n = 2 ∣ n

 even? : (n : ℕ) → Dec (Even n)
 even? n = 2 ∣? n

 Odd : ℕ → Set
 Odd = ¬_ ∘ Even

 even-irrelevant : ∀{n}(p q : Even n) → p ≡ q
 even-irrelevant (divides q₁ e₁) (divides q₂ e₂)
   with *2-injective q₁ q₂ (trans (sym e₁) e₂)
 ...| refl = cong (divides q₁) (≡-irrelevant e₁ e₂)

 --------------------------------------------------
 -- Properties about stepping and unstepping 'Even'

 even-unstep : ∀ k → Even (2 + k) → Even k
 even-unstep k (divides (suc q) e) = divides q (suc-injective (suc-injective e))

 even-step : ∀ k → Even k → Even (2 + k)
 even-step k (divides q₁ eq) = divides (1 + q₁) (cong (suc ∘ suc) eq)

 -----------------------------
 -- Properties of Even and Odd

 mutual
  even-odd-suc : ∀ k → Even k → Odd (suc k)
  even-odd-suc zero    x (divides q e) = ⊥-1≡m*2 q e
  even-odd-suc (suc k) x x₁            = even-suc-odd (suc k) x₁ x

  even-suc-odd : ∀ k → Even (suc k) → Odd k
  even-suc-odd zero    (divides q e) x₁ = ⊥-1≡m*2 q e
  even-suc-odd (suc k) x             x₁ = even-odd-suc k (even-unstep k x) x₁

 mutual
  odd-suc-suc : ∀ k → Odd k → Even (suc k)
  odd-suc-suc zero x = ⊥-elim (x (divides 0 refl))
  odd-suc-suc (suc k) x = even-step k (odd-pred-even (suc k) x)

  odd-pred-even : ∀ k → Odd k → Even (pred k)
  odd-pred-even zero x = ⊥-elim (x (divides 0 refl))
  odd-pred-even (suc k) x with even? k
  ...| no imp = ⊥-elim (x (odd-suc-suc k imp))
  ...| yes prf = prf

 -----------------------------
 -- Properties of Even and _*_

 *-preserve-even : ∀ k d → Even k → Even (k * d)
 *-preserve-even k d = ∣m⇒∣m*n d

 -----------------------------
 -- Properties of Even and _≤_

 even>0⇒>1 : ∀ {k} → 0 < k → Even k → 1 < k
 even>0⇒>1 {0}           ()
 even>0⇒>1 {1}           0<k e = ⊥-elim ((even-odd-suc 0 (divides 0 refl)) e)
 even>0⇒>1 {suc (suc k)} (s≤s z≤n) _ = s≤s (s≤s z≤n)

 0<odd : ∀{d} → Odd d → 0 < d
 0<odd {zero}  imp = ⊥-elim (imp (divides zero refl))
 0<odd {suc d} _   = s≤s z≤n

 -----------------------------
 -- Properties of Even and _∸_

 even∸1-odd : ∀ {k} → 1 < k → Even k → Odd (k ∸ 1)
 even∸1-odd {suc zero} 1<k ek = λ x → contradiction refl (<⇒≢ 1<k)
 even∸1-odd {suc (suc k)} 1<k ek = λ x → even-suc-odd (suc k) ek x

 odd∸1-even : ∀ {k} → Odd k → Even (k ∸ 1)
 odd∸1-even {zero} ok = ⊥-elim (ok (divides 0 refl))
 odd∸1-even {suc zero} ok = divides 0 refl
 odd∸1-even {suc (suc k)} ok = odd-pred-even (suc (suc k)) ok

 -----------------------------
 -- Properties of Even and _^_

 even-2^k : ∀ {k} → 0 < k → Even (2 ^ k)
 even-2^k {suc k} x = *-preserve-even 2 (2 ^ k) (divides 1 refl)

 odd-2^kd-1 : ∀ k d → 0 < k → 0 < d → ¬ Even (2 ^ k * d ∸ 1)
 odd-2^kd-1 k d 0<k 0<d x
   = even∸1-odd {2 ^ k * d} (pow*d>1 k d 0<k 0<d)
                            (*-preserve-even (2 ^ k) d (even-2^k 0<k))
                            x

 ----------------------------------------------------------------
 -- Every natural number can be viewed as a power of two times
 -- an odd number. We can witness that conversion in the from and
 -- to functions below.
 data Pow2 : ℕ → Set where
   zero : Pow2 zero
   pos  : ∀ {n} l d → Odd d → n ≡ 2 ^ l * d → Pow2 n

 pos-cong : ∀{n₁ n₂} (p : n₁ ≡ n₂)
          → ∀{d₁ d₂} (q : d₁ ≡ d₂)
          → (o₁ : Odd d₁)(o₂ : Odd d₂)
          → ∀{m} (r₁ : m ≡ 2 ^ n₁ * d₁) (r₂ : m ≡ 2 ^ n₂ * d₂)
          → pos n₁ d₁ o₁ r₁ ≡ pos n₂ d₂ o₂ r₂
 pos-cong {n₁ = n} refl {d₁ = d} refl o₁ o₂ r₁ r₂
   = cong₂ (pos n d) (fun-ext (λ x → ⊥-elim (o₁ x))) (≡-irrelevant r₁ r₂)

 -- One must mark this as terminating. The recursive call
 -- is made with 'quotient prf', and although we know it is
 -- strictly smaller than (suc n), Agda can't infer it.
 {-# TERMINATING #-}
 to : (n : ℕ) → Pow2 n
 to 0       = zero
 to (suc n) with even? (suc n)
 ...| no  odd = pos 0 (suc n) odd (cong suc (+-comm 0 n))
 ...| yes prf with to (quotient prf)
 ...| zero             = ⊥-elim (1+n≢0 (_∣_.equality prf))
 ...| pos l d odd prf' = pos (suc l) d odd
                         (trans (_∣_.equality prf)
                         (trans (cong (λ x → x * 2) prf')
                                (a*b*2-lemma (2 ^ l) d)))

 -- Converting from a Pow2 is trivial, since we kept the
 -- original number there.
 from : ∀{n} → Pow2 n → ℕ
 from zero              = zero
 from (pos {n} _ _ _ _) = n

 -- From and To form an isomorphism
 -- TODO-1: Document and justify this pragma
 {-# TERMINATING #-}
 from-to-iso : ∀ n → from (to n) ≡ n
 from-to-iso zero = refl
 from-to-iso (suc n) with even? (suc n)
 ...| no  odd = refl
 ...| yes prf with to (quotient prf)
 ...| zero             = ⊥-elim (1+n≢0 (_∣_.equality prf))
 ...| pos l d odd prf' = refl

 --------------------------------
 -- Properties of to and equality

 inj-to : ∀ {m n} → m ≡ n → to m ≅ to n
 inj-to refl = ≅-refl

 to-inj :  ∀ {m n} → to m ≇ to n → m ≢ n
 to-inj x x₁ = x (inj-to x₁)

 ---------------------------
 -- Uniqueness of 2^k*d form

 2^kd-≢-d : ∀{k d₁ d₂}
          → d₁ ≢ d₂
          → 2 ^ k * d₁ ≢ 2 ^ k * d₂
 2^kd-≢-d {k} hip abs with 2^k-is-suc k
 ...| r , prf rewrite prf = hip (*-cancelˡ-≡ r abs)

 2^kd-≢-k : ∀{k₁ k₂ d₁ d₂}
             → k₁ ≢ k₂
             → Odd d₁ → Odd d₂
             → 2 ^ k₁ * d₁ ≢ 2 ^ k₂ * d₂
 2^kd-≢-k {zero} {zero} {d₁} {d₂} k₁≢k₂ o₁ o₂ e₁≡e₂ = k₁≢k₂ refl
 2^kd-≢-k {zero} {suc k₂} {d₁} {d₂} k₁≢k₂ o₁ o₂ e₁≡e₂
   rewrite +-identityʳ d₁
         | *-assoc 2 (2 ^ k₂) d₂
         | *-comm 2 (2 ^ k₂ * d₂) = o₁ (divides (2 ^ k₂ * d₂) e₁≡e₂)
 2^kd-≢-k {suc k₁} {zero} {d₁} {d₂} k₁≢k₂ o₁ o₂ e₁≡e₂
   rewrite +-identityʳ d₂
         | *-assoc 2 (2 ^ k₁) d₁
         | *-comm 2 (2 ^ k₁ * d₁) = o₂ (divides (2 ^ k₁ * d₁) (sym e₁≡e₂))
 2^kd-≢-k {suc k₁} {suc k₂} {d₁} {d₂} k₁≢k₂ o₁ o₂ e₁≡e₂
   rewrite  *-assoc 2 (2 ^ k₁) d₁
         |  *-assoc 2 (2 ^ k₂) d₂ = *-cong-≢ 2 (s≤s z≤n) (2^kd-≢-k (suc-≢ k₁≢k₂) o₁ o₂) e₁≡e₂

 ----------------------
 -- Correctness of 'to'

 -- The trick to 2^kd is to use heterogeneous equality first.
 -- The problem stems from the type of arguments of pos depending
 -- on each other. Agda has trouble understanding that the different
 -- ways to write 'n' are all equal. Hence, we abstract that away.
 to-2^kd-≅ : ∀{n d} k → (o : Odd d)(p : n ≡ 2 ^ k * d)
           → to n ≅ pos k d o refl
 to-2^kd-≅ {n} {d} k o p with to n
 ...| zero = ⊥-elim (0≢a*b-magic (1≤2^n k) (0<odd o) p)
 to-2^kd-≅ {n} {d} k o p
    | pos k₀ d₀ o₀ p₀
   with k ≟ k₀
 ...| no abs = ⊥-elim (2^kd-≢-k abs o o₀ (trans (sym p) p₀))
 ...| yes refl
   with d ≟ d₀
 ...| no abs = ⊥-elim (2^kd-≢-d {k₀} abs (trans (sym p) p₀))
 to-2^kd-≅ {n} {d} .k₀ o p
    | pos k₀ d₀ o₀ p₀ | yes refl | yes refl
   rewrite fun-ext {f = o} {o₀} (λ x → ⊥-elim (o x)) | p
   with p₀
 ...| refl = ≅-refl

 -- And then, Agda is happy to understand it is equal after all.
 to-2^kd : ∀{d} k → (o : Odd d) → to (2 ^ k * d) ≡ pos k d o refl
 to-2^kd {d} k p = ≅-to-≡ (to-2^kd-≅ k p refl)

 to-reduce : ∀ {m k d}
           → (mprf : m ≡ (2 ^ k) * d)
           → (od : Odd d)
           → to m ≡ pos k d od mprf
 to-reduce {m} {k} {d} refl od = to-2^kd k od


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

module Data.List.Properties where

open import Data.List
open import Prelude
open import Data.Fin
open import Strict.Properties

map-length : (f : A → B) (xs : List A)
           → length xs ≡ length (map f xs)
map-length f [] _ = zero
map-length f (x ∷ xs) i = suc (map-length f xs i)

map-ind : (f : A → B) (xs : List A)
        → PathP (λ i → Fin (map-length f xs i) → B) (f ∘ (xs !_)) (map f xs !_)
map-ind f [] i ()
map-ind f (x ∷ xs) i f0 = f x
map-ind f (x ∷ xs) i (fs n) = map-ind f xs i n

tab-length : ∀ n (f : Fin n → A) → length (tabulate n f) ≡ n
tab-length zero f _ = zero
tab-length (suc n) f i = suc (tab-length n (f ∘ fs) i)

tab-distrib : ∀ n (f : Fin n → A) m → ∃ i × (f i ≡ tabulate n f ! m)
tab-distrib (suc n) f f0 = f0 , refl
tab-distrib (suc n) f (fs m) = let i , p = tab-distrib n (f ∘ fs) m in fs i , p

tab-id : ∀ n (f : Fin n → A) → PathP (λ i → Fin (tab-length n f i) → A) (_!_ (tabulate n f)) f
tab-id zero f _ ()
tab-id (suc n) f i f0 = f f0
tab-id (suc n) f i (fs m) = tab-id n (f ∘ fs) i m

list-elim : ∀ {p} (P : List A → Type p) →
                  (∀ x xs → P xs → P (x ∷ xs)) →
                  (P []) →
                  ∀ xs → P xs
list-elim P f b [] = b
list-elim P f b (x ∷ xs) = f x xs (list-elim P f b xs)

foldr-universal : ∀ (h : List B → A) f e
                → (h [] ≡ e)
                → (∀ x xs → h (x ∷ xs) ≡ f x (h xs))
                → ∀ xs → h xs ≡ foldr f e xs
foldr-universal h f e base step [] = base
foldr-universal h f e base step (x ∷ xs) =
  step x xs ; cong (f x) (foldr-universal h f e base step xs)

foldr-id : (xs : List A) → xs ≡ foldr _∷_ [] xs
foldr-id = foldr-universal id _∷_ [] refl (λ _ _ → refl)

foldr-fusion : ∀ (f : C → A) {_⊕_ : B → C → C} {_⊗_ : B → A → A} e
              → (∀ x y → f (x ⊕ y) ≡ x ⊗ f y)
              → ∀ xs → f (foldr _⊕_ e xs) ≡ foldr _⊗_ (f e) xs
foldr-fusion h {f} {g} e fuse =
  foldr-universal (h ∘ foldr f e) g (h e) refl (λ x xs → fuse x (foldr f e xs))

foldl-is-foldr : (f : B → A → B) (z : B) (xs : List A) →
                 foldl f z xs ≡ foldr (λ x k xs → k (f xs x)) id xs z
foldl-is-foldr f z xs =
  cong (_$ z) (foldr-universal (flip (foldl f)) (λ x k xs → k (f xs x)) id refl (λ x xs → refl) xs)

foldl-fusion : ∀ (f : C → A) {_⊕_ : C → B → C}  {_⊗_ : A → B → A} e →
                 (∀ x y → f (x ⊕ y) ≡ f x ⊗ y) →
                 ∀ xs → f (foldl _⊕_ e xs) ≡ foldl _⊗_ (f e) xs
foldl-fusion h {f} {g} e fuse [] = refl
foldl-fusion h {f} {g} e fuse (x ∷ xs) =
  foldl-fusion h (f e x) fuse xs ; cong (flip (foldl g) xs) (fuse e x)

++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc xs ys zs = foldr-fusion (_++ zs) ys (λ _ _ → refl) xs

map-fusion : ∀ f (b : C) (g : A → B) xs → foldr f b (map g xs) ≡ foldr (f ∘ g) b xs
map-fusion f b g  = foldr-fusion (foldr f b) [] λ _ _ → refl

++-idʳ : (xs : List A) → xs ++ [] ≡ xs
++-idʳ [] = refl
++-idʳ (x ∷ xs) = cong (x ∷_) (++-idʳ xs)

open import Function.Injective

∷-inj : (x : A) → Injective (x ∷_)
∷-inj x xs ys = cong λ where [] → []
                             (_ ∷ zs) → zs

++-inj : (xs : List A) → Injective (xs ++_)
++-inj []       ys zs ys≡zs = ys≡zs
++-inj (x ∷ xs) ys zs ys≡zs = ++-inj xs ys zs (∷-inj x (xs ++ ys) (xs ++ zs) ys≡zs)

open import Algebra

module _ (mon : Monoid b) where
  open Monoid mon

  module _ (f : A → 𝑆) where
    monStepL : 𝑆 → A → 𝑆
    monStepL xs x = xs ∙ f x
    {-# INLINE monStepL #-}

    foldMapL : List A → 𝑆
    foldMapL = foldl monStepL ε

    foldMapLStep : ∀ x xs → f x ∙ foldMapL xs ≡ foldMapL (x ∷ xs)
    foldMapLStep x xs = foldl-fusion (f x ∙_) ε (λ y z → sym (assoc (f x) y (f z))) xs ; cong (flip (foldl monStepL) xs) (∙ε (f x) ; sym (ε∙ (f x)))

    foldl-foldr-monoid : (xs : List A) → foldMapL xs ≡ foldr (_∙_ ∘ f) ε xs
    foldl-foldr-monoid = foldr-universal _ (_∙_ ∘ f) ε refl λ x xs → sym (foldMapLStep x xs)

module _ (A : Type a) where
  listMonoid : Monoid a
  listMonoid .Monoid.𝑆 = List A
  listMonoid .Monoid._∙_ = _++_
  listMonoid .Monoid.ε = []
  listMonoid .Monoid.assoc = ++-assoc
  listMonoid .Monoid.ε∙ _ = refl
  listMonoid .Monoid.∙ε = ++-idʳ

foldl′-foldl : (f : B → A → B) (z : B) (xs : List A) → foldl′ f z xs ≡ foldl f z xs
foldl′-foldl f z [] = refl
foldl′-foldl f z (x ∷ xs) = $!-≡ (λ y → foldl′ f y xs) (f z x) ; foldl′-foldl f (f z x) xs

foldr′-foldr : (f : A → B → B) (z : B) (xs : List A) → foldr′ f z xs ≡ foldr f z xs
foldr′-foldr f z [] = refl
foldr′-foldr f z (x ∷ xs) = $!-≡ (f x) (foldr′ f z xs) ; cong (f x) (foldr′-foldr f z xs)

is-empty : List A → Bool
is-empty [] = true
is-empty (_ ∷ _) = false

NonEmpty : List A → Type
NonEmpty = T ∘ not ∘ is-empty

open import Data.Maybe.Properties

foldrMay-nonEmpty : (f : A → A → A) (xs : List A) → NonEmpty xs → IsJust (foldrMay f xs)
foldrMay-nonEmpty f (x ∷ xs) _ = tt

foldr1 : (A → A → A) → (xs : List A) → ⦃ NonEmpty xs ⦄ → A
foldr1 f xs ⦃ xsne ⦄ = fromJust (foldrMay f xs)
 where instance _ = foldrMay-nonEmpty f xs xsne

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import Agda.Primitive.Cubical public

postulate
  Int : Set
  _↦_ : {A : Set} → A → A → Set
  id↦ : {A : Set} {a : A} → a ↦ a

{-# BUILTIN REWRITE _↦_ #-}

postulate
  hcompIntEmpty : (n : Int) → primHComp (λ _ → isOneEmpty) n ↦ n

{-# REWRITE hcompIntEmpty #-}

test : (n : Int) → primHComp (λ _ → isOneEmpty) n ↦ n
test n = id↦

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
module Oscar (FunctionName PredicateName VariableName QuantifierName Name : Set) where

open import Oscar.Data.Fin using (Fin; zero; suc; thick?)

open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
open import Function using (_∘_; flip)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (∃; _,_; _×_)
open import Data.Empty using (⊥-elim)
open import Data.Vec using (Vec; []; _∷_)

data Term (n : ℕ) : Set where
  i : (x : Fin n) -> Term n
  leaf : Term n
  _fork_ : (s t : Term n) -> Term n
  function : FunctionName → ∀ {f} → Vec (Term n) f → Term n

data Formula (n : ℕ) : Set
 where
  atomic : PredicateName → ∀ {t} → Vec (Term n) t → Formula n
  logical : Formula n →
            Formula n →
            Formula n
  quantified : VariableName → Formula (suc n) → Formula n

Term-function-inj-FunctionName : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → fn₁ ≡ fn₂
Term-function-inj-FunctionName refl = refl

Term-function-inj-VecSize : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → N₁ ≡ N₂
Term-function-inj-VecSize refl = refl

Term-function-inj-Vector : ∀ {fn₁ fn₂} {n N} {ts₁ : Vec (Term n) N} {ts₂ : Vec (Term n) N} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≡ ts₂
Term-function-inj-Vector refl = refl

Term-fork-inj-left : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ Term.fork r₁ ≡ l₂ fork r₂ → l₁ ≡ l₂
Term-fork-inj-left refl = refl

Term-fork-inj-right : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ Term.fork r₁ ≡ l₂ fork r₂ → r₁ ≡ r₂
Term-fork-inj-right refl = refl

open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)

Term-function-inj-HetVector : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≅ ts₂
Term-function-inj-HetVector refl = refl

_~>_ : (m n : ℕ) -> Set
m ~> n = Fin m -> Term n

▹ : ∀ {m n} -> (r : Fin m -> Fin n) -> Fin m -> Term n
▹ r = i ∘ r

record Substitution (T : ℕ → Set) : Set where
  field
    _◃_ : ∀ {m n} -> (f : m ~> n) -> T m -> T n

open Substitution ⦃ … ⦄ public

{-# DISPLAY Substitution._◃_ _ = _◃_ #-}

mutual

  instance SubstitutionTerm : Substitution Term
  Substitution._◃_ SubstitutionTerm = _◃′_ where
    _◃′_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
    f ◃′ i x = f x
    f ◃′ leaf = leaf
    f ◃′ (s fork t) = (f ◃ s) fork (f ◃ t)
    f ◃′ (function fn ts) = function fn (f ◃ ts)

  instance SubstitutionVecTerm : ∀ {N} → Substitution (flip Vec N ∘ Term )
  Substitution._◃_ (SubstitutionVecTerm {N}) = _◃′_ where
    _◃′_ : ∀ {m n} -> (f : m ~> n) -> Vec (Term m) N -> Vec (Term n) N
    f ◃′ [] = []
    f ◃′ (t ∷ ts) = f ◃ t ∷ f ◃ ts

_≐_ : {m n : ℕ} -> (Fin m -> Term n) -> (Fin m -> Term n) -> Set
f ≐ g = ∀ x -> f x ≡ g x

record SubstitutionExtensionality (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set₁ where
  field
    ◃ext : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> (t : T m) -> f ◃ t ≡ g ◃ t

open SubstitutionExtensionality ⦃ … ⦄ public

mutual

  instance SubstitutionExtensionalityTerm : SubstitutionExtensionality Term
  SubstitutionExtensionality.◃ext SubstitutionExtensionalityTerm = ◃ext′ where
    ◃ext′ : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ t -> f ◃ t ≡ g ◃ t
    ◃ext′ p (Term.i x) = p x
    ◃ext′ p leaf = refl
    ◃ext′ p (s fork t) = cong₂ _fork_ (◃ext p s) (◃ext p t)
    ◃ext′ p (function fn ts) = cong (function fn) (◃ext p ts)

  instance SubstitutionExtensionalityVecTerm : ∀ {N} → SubstitutionExtensionality (flip Vec N ∘ Term)
  SubstitutionExtensionality.◃ext (SubstitutionExtensionalityVecTerm {N}) = λ x → ◃ext′ x where
    ◃ext′ : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ {N} (t : Vec (Term m) N) -> f ◃ t ≡ g ◃ t
    ◃ext′ p [] = refl
    ◃ext′ p (t ∷ ts) = cong₂ _∷_ (◃ext p t) (◃ext p ts)

_◇_ : ∀ {l m n : ℕ } -> (f : Fin m -> Term n) (g : Fin l -> Term m) -> Fin l -> Term n
f ◇ g = (f ◃_) ∘ g

≐-cong : ∀ {m n o} {f : m ~> n} {g} (h : _ ~> o) -> f ≐ g -> (h ◇ f) ≐ (h ◇ g)
≐-cong h f≐g t = cong (h ◃_) (f≐g t)

≐-sym : ∀ {m n} {f : m ~> n} {g} -> f ≐ g -> g ≐ f
≐-sym f≐g = sym ∘ f≐g

module Sub where
  record Fact1 (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set where
    field
      fact1 : ∀ {n} -> (t : T n) -> i ◃ t ≡ t

  open Fact1 ⦃ … ⦄ public

  mutual

    instance Fact1Term : Fact1 Term
    Fact1.fact1 Fact1Term (i x) = refl
    Fact1.fact1 Fact1Term leaf = refl
    Fact1.fact1 Fact1Term (s fork t) = cong₂ _fork_ (fact1 s) (fact1 t)
    Fact1.fact1 Fact1Term (function fn ts) = cong (function fn) (fact1 ts)

    instance Fact1TermVec : ∀ {N} → Fact1 (flip Vec N ∘ Term)
    Fact1.fact1 Fact1TermVec [] = refl
    Fact1.fact1 Fact1TermVec (t ∷ ts) = cong₂ _∷_ (fact1 t) (fact1 ts)

  record Fact2 (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set where
    field
      -- ⦃ s ⦄ : Substitution T
      fact2 : ∀ {l m n} -> {f : Fin m -> Term n} {g : _} (t : T l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)

  open Fact2 ⦃ … ⦄ public

  mutual

    instance Fact2Term : Fact2 Term
    -- Fact2.s Fact2Term = SubstitutionTerm
    Fact2.fact2 Fact2Term (i x) = refl
    Fact2.fact2 Fact2Term leaf = refl
    Fact2.fact2 Fact2Term (s fork t) = cong₂ _fork_ (fact2 s) (fact2 t)
    Fact2.fact2 Fact2Term {f = f} {g = g} (function fn ts) = cong (function fn) (fact2 {f = f} {g = g} ts) -- fact2 ts

    instance Fact2TermVec : ∀ {N} → Fact2 (flip Vec N ∘ Term)
    -- Fact2.s Fact2TermVec = SubstitutionVecTerm
    Fact2.fact2 Fact2TermVec [] = refl
    Fact2.fact2 Fact2TermVec (t ∷ ts) = cong₂ _∷_ (fact2 t) (fact2 ts)

  fact3 : ∀ {l m n} (f : Fin m -> Term n) (r : Fin l -> Fin m) -> (f ◇ (▹ r)) ≡ (f ∘ r)
  fact3 f r = refl

◃ext' : ∀ {m n o} {f : Fin m -> Term n}{g : Fin m -> Term o}{h} -> f ≐ (h ◇ g) -> ∀ (t : Term _) -> f ◃ t ≡ h ◃ (g ◃ t)
◃ext' p t = trans (◃ext p t) (Sub.fact2 t)

open import Data.Maybe using (Maybe; nothing; just; functor; maybe′)
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

record Check (T : ℕ → Set) : Set where
  field
    check : ∀{n} (x : Fin (suc n)) (t : T (suc n)) -> Maybe (T n)

open Check ⦃ … ⦄ public

_<*>_ = _⊛_

mutual

  instance CheckTerm : Check Term
  Check.check CheckTerm x (i y) = i <$> thick? x y
  Check.check CheckTerm x leaf = just leaf
  Check.check CheckTerm x (s fork t) = _fork_ <$> check x s ⊛ check x t
  Check.check CheckTerm x (function fn ts) = ⦇ (function fn) (check x ts) ⦈

  instance CheckTermVec : ∀ {N} → Check (flip Vec N ∘ Term)
  Check.check CheckTermVec x [] = just []
  Check.check CheckTermVec x (t ∷ ts) = ⦇ check x t ∷ check x ts ⦈

_for_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) -> Fin (suc n) -> Term n
(t' for x) y = maybe′ i t' (thick? x y)

data AList : ℕ -> ℕ -> Set where
  anil : ∀ {n} -> AList n n
  _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
               -> AList (suc m) n

sub : ∀ {m n} (σ : AList m n) -> Fin m -> Term n
sub anil = i
sub (σ asnoc t' / x) = sub σ ◇ (t' for x)

_++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n
ρ ++ anil = ρ
ρ ++ (σ asnoc t' / x) = (ρ ++ σ) asnoc t' / x

++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) -> ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
++-assoc ρ σ anil = refl
++-assoc ρ σ (τ asnoc t / x) = cong (λ s -> s asnoc t / x) (++-assoc ρ σ τ)

module SubList where
  anil-id-l : ∀ {m n} (σ : AList m n) -> anil ++ σ ≡ σ
  anil-id-l anil = refl
  anil-id-l (σ asnoc t' / x) = cong (λ σ -> σ asnoc t' / x) (anil-id-l σ)

  fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> sub (ρ ++ σ) ≐ (sub ρ ◇ sub σ)
  fact1 ρ anil v = refl
  fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
    where
      t = (t' for x) v
      hyp-on-terms = ◃ext (fact1 r s) t
      ◃-assoc = Sub.fact2 t

_∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
  -> ∃ (AList (suc m))
(n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

flexFlex : ∀ {m} (x y : Fin m) -> ∃ (AList m)
flexFlex {suc m} x y with thick? x y
...              | just y' = m , anil asnoc i y' / x
...              | nothing = suc m , anil
flexFlex {zero} () _

flexRigid : ∀ {m} (x : Fin m) (t : Term m) -> Maybe (∃(AList m))
flexRigid {suc m} x t with check x t
...                   | just t' = just (m , anil asnoc t' / x)
...                   | nothing = nothing
flexRigid {zero} () _


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a (non-strict) partial order.

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

module Data.Product.Relation.Binary.Lex.NonStrict where

open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum.Base using (inj₁; inj₂)
open import Level using (Level)
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.Construct.NonStrictToStrict as Conv
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
  using (Pointwise)
import Data.Product.Relation.Binary.Lex.Strict as Strict

private
  variable
    a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
    A : Set a
    B : Set b

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

×-Lex : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
        Rel (A × B) _
×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_

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

×-reflexive : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂)
              {_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
              _≈₂_ ⇒ _≤₂_ →
              (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
  Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂

module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂} {_≤₂_ : Rel B ℓ₃} where

  private
    _≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_

  ×-transitive : IsPartialOrder _≈₁_ _≤₁_ → Transitive _≤₂_ →
                 Transitive _≤ₗₑₓ_
  ×-transitive po₁ trans₂ =
    Strict.×-transitive {_≈₁_ = _≈₁_} {_<₂_ = _≤₂_}
      isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
      (Conv.<-trans _ _ po₁)
      trans₂
    where open IsPartialOrder po₁

  ×-total : Symmetric _≈₁_ → Decidable _≈₁_ → Antisymmetric _≈₁_ _≤₁_ →
            Total _≤₁_ → Total _≤₂_ → Total _≤ₗₑₓ_
  ×-total sym₁ dec₁ antisym₁ total₁ total₂ =
    total
    where
    tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    tri₁ = Conv.<-trichotomous _ _ sym₁ dec₁ antisym₁ total₁

    total : Total _≤ₗₑₓ_
    total x y with tri₁ (proj₁ x) (proj₁ y)
    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
    ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
    ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))

  ×-decidable : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
                Decidable _≤ₗₑₓ_
  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
    Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
                       dec-≤₂

module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
         {_≈₂_ : Rel B ℓ₃} {_≤₂_ : Rel B ℓ₄}
         where

  private
    _≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
    _≋_    = Pointwise _≈₁_ _≈₂_

  ×-antisymmetric : IsPartialOrder _≈₁_ _≤₁_ → Antisymmetric _≈₂_ _≤₂_ →
                   Antisymmetric _≋_ _≤ₗₑₓ_
  ×-antisymmetric po₁ antisym₂ =
    Strict.×-antisymmetric {_≈₁_ = _≈₁_} {_<₂_ = _≤₂_}
       ≈-sym₁ irrefl₁ asym₁ antisym₂
    where
    open IsPartialOrder po₁
    open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)

    irrefl₁ : Irreflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
    irrefl₁ = Conv.<-irrefl _≈₁_ _≤₁_

    asym₁ : Asymmetric (Conv._<_ _≈₁_ _≤₁_)
    asym₁ = trans∧irr⟶asym {_≈_ = _≈₁_}
                           ≈-refl₁ (Conv.<-trans _ _ po₁) irrefl₁

  ×-respects₂ : IsEquivalence _≈₁_ →
                _≤₁_ Respects₂ _≈₁_ → _≤₂_ Respects₂ _≈₂_ →
                _≤ₗₑₓ_ Respects₂ _≋_
  ×-respects₂ eq₁ resp₁ resp₂ =
    Strict.×-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂

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

  ×-isPartialOrder : IsPartialOrder _≈₁_ _≤₁_ →
                     IsPartialOrder _≈₂_ _≤₂_ →
                     IsPartialOrder _≋_ _≤ₗₑₓ_
  ×-isPartialOrder po₁ po₂ = record
    { isPreorder = record
        { isEquivalence = Pointwise.×-isEquivalence
                            (isEquivalence po₁)
                            (isEquivalence po₂)
        ; reflexive     = ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
        ; trans         = ×-transitive {_≤₂_ = _≤₂_} po₁ (trans po₂)
        }
    ; antisym = ×-antisymmetric po₁ (antisym po₂)
    }
    where open IsPartialOrder

  ×-isTotalOrder : Decidable _≈₁_ →
                   IsTotalOrder _≈₁_ _≤₁_ →
                   IsTotalOrder _≈₂_ _≤₂_ →
                   IsTotalOrder _≋_ _≤ₗₑₓ_
  ×-isTotalOrder ≈₁-dec to₁ to₂ = record
    { isPartialOrder = ×-isPartialOrder
                         (isPartialOrder to₁) (isPartialOrder to₂)
    ; total          = ×-total (Eq.sym to₁) ≈₁-dec
                                             (antisym to₁) (total to₁)
                               (total to₂)
    }
    where open IsTotalOrder

  ×-isDecTotalOrder : IsDecTotalOrder _≈₁_ _≤₁_ →
                      IsDecTotalOrder _≈₂_ _≤₂_ →
                      IsDecTotalOrder _≋_ _≤ₗₑₓ_
  ×-isDecTotalOrder to₁ to₂ = record
    { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                    (isTotalOrder to₁)
                                    (isTotalOrder to₂)
    ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
    ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
    }
    where open IsDecTotalOrder

------------------------------------------------------------------------
-- Bundles

×-poset : Poset a ℓ₁ ℓ₂ → Poset b ℓ₃ ℓ₄ → Poset _ _ _
×-poset p₁ p₂ = record
  { isPartialOrder = ×-isPartialOrder O₁.isPartialOrder O₂.isPartialOrder
  } where module O₁ = Poset p₁; module O₂ = Poset p₂

×-totalOrder : DecTotalOrder a ℓ₁ ℓ₂ →
               TotalOrder b ℓ₃ ℓ₄ →
               TotalOrder _ _ _
×-totalOrder t₁ t₂ = record
  { isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
  } where module T₁ = DecTotalOrder t₁; module T₂ = TotalOrder t₂

×-decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ →
                  DecTotalOrder b ℓ₃ ℓ₄ →
                  DecTotalOrder _ _ _
×-decTotalOrder t₁ t₂ = record
  { isDecTotalOrder = ×-isDecTotalOrder O₁.isDecTotalOrder O₂.isDecTotalOrder
  } where module O₁ = DecTotalOrder t₁; module O₂ = DecTotalOrder t₂

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

_×-isPartialOrder_  = ×-isPartialOrder
{-# WARNING_ON_USAGE _×-isPartialOrder_
"Warning: _×-isPartialOrder_ was deprecated in v0.15.
Please use ×-isPartialOrder instead."
#-}
_×-isDecTotalOrder_ = ×-isDecTotalOrder
{-# WARNING_ON_USAGE _×-isDecTotalOrder_
"Warning: _×-isDecTotalOrder_ was deprecated in v0.15.
Please use ×-isDecTotalOrder instead."
#-}
_×-poset_           = ×-poset
{-# WARNING_ON_USAGE _×-poset_
"Warning: _×-poset_ was deprecated in v0.15.
Please use ×-poset instead."
#-}
_×-totalOrder_      = ×-totalOrder
{-# WARNING_ON_USAGE _×-totalOrder_
"Warning: _×-totalOrder_ was deprecated in v0.15.
Please use ×-totalOrder instead."
#-}
_×-decTotalOrder_   = ×-decTotalOrder
{-# WARNING_ON_USAGE _×-decTotalOrder_
"Warning: _×-decTotalOrder_ was deprecated in v0.15.
Please use ×-decTotalOrder instead."
#-}
×-≈-respects₂       = ×-respects₂
{-# WARNING_ON_USAGE ×-≈-respects₂
"Warning: ×-≈-respects₂ was deprecated in v0.15.
Please use ×-respects₂ instead."
#-}


text:
-- Andreas, 2016-10-10, AIM XXIV

{-# REWRITE #-}  -- This should yield a warning.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2016-12-31, issue #2371 reported by subttle

-- Module parameter Nat shadowed by import
module Issue2371 (Nat : Set) where

open import Agda.Builtin.Nat

-- C-c C-n zero RET

-- ERROR WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Utils/List.hs:304

-- Should succeed.

-- C-c C-n Nat RET will report an ambiguous name


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

module Rose where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data List (A : Set) : {_ : Size} -> Set where
  []   : {size : Size} -> List A {size ^}
  _::_ : {size : Size} -> A -> List A {size} -> List A {size ^}

map : {A B : Set} -> (A -> B) ->
      {size : Size} -> List A {size} -> List B {size}
map f [] = []
map f (x :: xs) = f x :: map f xs

data Rose (A : Set) : {_ : Size} -> Set where
  rose : {size : Size} -> A -> List (Rose A {size}) {∞} -> Rose A {size ^}

{-
mapRose : {A B : Set} -> (A -> B) ->
          {size : Size} -> Rose A {size} -> Rose B {size}
mapRose {A} {B} f .{size ^} (rose {size} a l) =
   rose (f a) (map (\ r -> mapRose {A} {B} f {size} r) l)
-}

mapRose : {A B : Set} -> (A -> B) ->
          {size : Size} -> Rose A {size} -> Rose B {size}
mapRose f (rose a l) = rose (f a) (map (mapRose f) l)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Terms where

open import Library

-- * Variables
------------------------------------------------------------------------

data Ty : Set where
  base : Ty
  _→̂_ : (a b : Ty) → Ty

-- Typing contexts.

Cxt = List Ty

-- Variables.

data Var : (Γ : Cxt) (a : Ty) → Set where
  zero : ∀{Γ a}                 → Var (a ∷ Γ) a
  suc  : ∀{Γ a b} (x : Var Γ a) → Var (b ∷ Γ) a

-- De Bruijn index 0.

v₀ : ∀ {a Γ} → Var (a ∷ Γ) a
v₀ = zero

-- * Terms
------------------------------------------------------------------------

-- Well-typed terms.

data Tm (Γ : Cxt) : (a : Ty) → Set where
  var  : ∀{a}          (x : Var Γ a)                   → Tm Γ a
  abs  : ∀{a b}        (t : Tm (a ∷ Γ) b)              → Tm Γ (a →̂ b)
  app  : ∀{a b}        (t : Tm Γ (a →̂ b)) (u : Tm Γ a) → Tm Γ b

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text: {-# BUILTIN CUBEINTERVALUNIV IUniv #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

-- | Quotient integer
module QuoInt where

open import Cubical.Core.Everything
open import Cubical.HITs.Ints.QuoInt renaming (_+ℤ_ to _+_; ℤ to Z)

open import Cubical.Data.Nat hiding (_+_)
open import Cubical.Foundations.Prelude

+-i-zero : ∀ a i → posneg i + a ≡ a
+-i-zero a i =
  cong (_+ a) (lemma₁ i)
  ∙ -- x ≡ y → y ≡ z → x ≡ z
  lemma₀ a
  where
    lemma₀ : ∀ a → pos 0 + a ≡ a
    lemma₀ (pos zero) = refl
    lemma₀ (pos (suc n)) = cong sucℤ (lemma₀ (pos n))
    lemma₀ (neg zero) = posneg
    lemma₀ (neg (suc n)) = cong predℤ (lemma₀ (neg n))
    lemma₀ (posneg i) j = posneg (i ∧ j)

    lemma₁ : ∀ i → posneg i ≡ pos 0
    lemma₁ i j = posneg (i ∧ ~ j)

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text: module Categories.Monoidal.CartesianClosed where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ : Level

record IsMonoid {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor ismonoid

  field
    isSemigroup : IsSemigroup _·_
    identity    : (x : A) → (x · ε ≡ x) × (ε · x ≡ x)

  open IsSemigroup isSemigroup public

  lid : (x : A) → ε · x ≡ x
  lid x = identity x .snd

  rid : (x : A) → x · ε ≡ x
  rid x = identity x .fst

unquoteDecl IsMonoidIsoΣ = declareRecordIsoΣ IsMonoidIsoΣ (quote IsMonoid)

record MonoidStr (A : Type ℓ) : Type ℓ where
  constructor monoidstr

  field
    ε        : A
    _·_      : A → A → A
    isMonoid : IsMonoid ε _·_

  infixl 7 _·_

  open IsMonoid isMonoid public

Monoid : ∀ ℓ → Type (ℓ-suc ℓ)
Monoid ℓ = TypeWithStr ℓ MonoidStr

monoid : (A : Type ℓ) (ε : A) (_·_ : A → A → A) (h : IsMonoid ε _·_) → Monoid ℓ
monoid A ε _·_ h = A , monoidstr ε _·_ h

-- Easier to use constructors

makeIsMonoid : {M : Type ℓ} {ε : M} {_·_ : M → M → M}
               (is-setM : isSet M)
               (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
               (rid : (x : M) → x · ε ≡ x)
               (lid : (x : M) → ε · x ≡ x)
             → IsMonoid ε _·_
IsMonoid.isSemigroup (makeIsMonoid is-setM assoc rid lid) = issemigroup is-setM assoc
IsMonoid.identity (makeIsMonoid is-setM assoc rid lid) = λ x → rid x , lid x

makeMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             (is-setM : isSet M)
             (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
             (rid : (x : M) → x · ε ≡ x)
             (lid : (x : M) → ε · x ≡ x)
           → Monoid ℓ
makeMonoid ε _·_ is-setM assoc rid lid =
  monoid _ ε _·_ (makeIsMonoid is-setM assoc rid lid)

record IsMonoidEquiv {A : Type ℓ} {B : Type ℓ}
  (M : MonoidStr A) (e : A ≃ B) (N : MonoidStr B)
  : Type ℓ
  where

  constructor monoidequiv

  -- Shorter qualified names
  private
    module M = MonoidStr M
    module N = MonoidStr N

  field
    presε : equivFun e M.ε ≡ N.ε
    isHom : (x y : A) → equivFun e (x M.· y) ≡ equivFun e x N.· equivFun e y

MonoidEquiv : (M N : Monoid ℓ) → Type ℓ
MonoidEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsMonoidEquiv (M .snd) e (N .snd)

-- We now extract the important results from the above module

isPropIsMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M) → isProp (IsMonoid ε _·_)
isPropIsMonoid ε _·_ =
  isOfHLevelRetractFromIso 1 IsMonoidIsoΣ
    (isPropΣ
      (isPropIsSemigroup _·_)
      (λ semi → isPropΠ λ _ → isProp× (semi .is-set _ _) (semi .is-set _ _)))
  where
  open IsSemigroup

𝒮ᴰ-Monoid : DUARel (𝒮-Univ ℓ) MonoidStr ℓ
𝒮ᴰ-Monoid =
  𝒮ᴰ-Record (𝒮-Univ _) IsMonoidEquiv
    (fields:
      data[ ε ∣ autoDUARel _ _ ∣ presε ]
      data[ _·_ ∣ autoDUARel _ _ ∣ isHom ]
      prop[ isMonoid ∣ (λ _ _ → isPropIsMonoid _ _) ])
  where
  open MonoidStr
  open IsMonoidEquiv

MonoidPath : (M N : Monoid ℓ) → MonoidEquiv M N ≃ (M ≡ N)
MonoidPath = ∫ 𝒮ᴰ-Monoid .UARel.ua

module MonoidTheory {ℓ} (M : Monoid ℓ) where

  open MonoidStr (snd M)

  -- Added for its use in groups
  -- If there exists a inverse of an element it is unique
  inv-lemma : (x y z : ⟨ M ⟩) → y · x ≡ ε → x · z ≡ ε → y ≡ z
  inv-lemma x y z left-inverse right-inverse =
    y           ≡⟨ sym (rid y) ⟩
    y · ε       ≡⟨ cong (λ - → y · -) (sym right-inverse) ⟩
    y · (x · z) ≡⟨ assoc y x z ⟩
    (y · x) · z ≡⟨ cong (λ - → - · z) left-inverse ⟩
    ε · z       ≡⟨ lid z ⟩
    z ∎

max_stars_repo_name: jespercockx/cubical

max_issues_repo_name: jespercockx/cubical

max_forks_repo_name: jespercockx/cubical


text:
module Numeral.Matrix where

import      Lvl
open import Syntax.Number
open import Data
open import Data.Boolean
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional using (const)
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Finite.Oper
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Natural
open import Numeral.CoordinateVector as Vector using (Vector)
open import Type

-- Accessor of data in 2-dimensional finite space (Implies bounded).
-- Like a data table.
record Matrix {ℓ} (s : ℕ ⨯ ℕ) (T : Type{ℓ}) : Type{ℓ} where
  constructor mat

  -- Type of elements in the matrix.
  Element : Type
  Element = T

  -- Width of the matrix (Number of columns).
  width : ℕ
  width = Tuple.left(s)

  -- Height of the matrix (Number of rows).
  height : ℕ
  height = Tuple.right(s)

  field
    -- Projection of a matrix.
    -- A cell in the matrix.
    proj : (𝕟(width) ⨯ 𝕟(height)) → T

  -- Vector of a row in the matrix.
  row : 𝕟(height) → Vector(width)(T)
  (row(y))(x) = proj(x , y)

  -- Vector of a column in the matrix.
  col : 𝕟(width) → Vector(height)(T)
  (col(x))(y) = proj(x , y)

  -- Transpose (Reflection on main diagonal).
  ⬔_ : Matrix(height , width)(T)
  proj(⬔_)(x , y) = proj(y , x)

module Rows where
  module _ {ℓ} {w}{h} {T : Type{ℓ}} where
    -- A matrix with two rows swapped.
    swap : 𝕟(h) → 𝕟(h) → Matrix(w , h)(T) → Matrix(w , h)(T)
    Matrix.proj(swap(y₁)(y₂)(M))(x , y) =
      if      (y ≡? y₁) then Matrix.proj(M)(x , y₂)
      else if (y ≡? y₂) then Matrix.proj(M)(x , y₁)
      else                   Matrix.proj(M)(x , y)

  module _ {ℓ₁ ℓ₂} {w₁ w₂}{h} {A : Type{ℓ₁}} {B : Type{ℓ₂}} where
    -- A matrix where a function has been applied to every row.
    map : (Vector(w₁)(A) → Vector(w₂)(B)) → Matrix(w₁ , h)(A) → Matrix(w₂ , h)(B)
    Matrix.proj(map f(M))(x , y) = Vector.proj(f(Matrix.row(M)(y)))(x)

  module _ {ℓ} {w}{h} {T : Type{ℓ}} where
    -- A matrix where a function has been applied to every element of the specified row.
    mapSingle : 𝕟(h) → (T → T) → Matrix(w , h)(T) → Matrix(w , h)(T)
    Matrix.proj(mapSingle target f(M))(x , y) =
      if      (y ≡? target) then f(Matrix.proj(M)(x , y))
      else                       Matrix.proj(M)(x , y)

    -- A matrix where a function has been applied to the specified row.
    applyOn : 𝕟(h) → (Vector(w)(T) → Vector(w)(T)) → Matrix(w , h)(T) → Matrix(w , h)(T)
    Matrix.proj(applyOn target f(M))(x , y) =
      if      (y ≡? target) then Vector.proj(f(Matrix.row(M)(y)))(x)
      else                       Matrix.proj(M)(x , y)

module Cols where
  module _ {ℓ} {w}{h} {T : Type{ℓ}} where
    -- A matrix with two columns swapped.
    swap : 𝕟(w) → 𝕟(w) → Matrix(w , h)(T) → Matrix(w , h)(T)
    Matrix.proj(swap(x₁)(x₂)(M))(x , y) =
      if      (x ≡? x₁) then Matrix.proj(M)(x₂ , y)
      else if (x ≡? x₂) then Matrix.proj(M)(x₁ , y)
      else                   Matrix.proj(M)(x , y)

  module _ {ℓ₁ ℓ₂} {w}{h₁ h₂} {A : Type{ℓ₁}} {B : Type{ℓ₂}} where
    -- A matrix where a function has been applied to every column.
    map : (Vector(h₁)(A) → Vector(h₂)(B)) → Matrix(w , h₁)(A) → Matrix(w , h₂)(B)
    Matrix.proj(map f(M))(x , y) = Vector.proj(f(Matrix.col(M)(x)))(y)

  module _ {ℓ} {w}{h} {T : Type{ℓ}} where
    -- A matrix where a function has been applied to every element of the specified column.
    mapSingle : 𝕟(w) → (T → T) → Matrix(w , h)(T) → Matrix(w , h)(T)
    Matrix.proj(mapSingle target f(M))(x , y) =
      if      (y ≡? target) then f(Matrix.proj(M)(x , y))
      else                       Matrix.proj(M)(x , y)

    -- A matrix where a function has been applied to the specified column.
    applyOn : 𝕟(w) → (Vector(h)(T) → Vector(h)(T)) → Matrix(w , h)(T) → Matrix(w , h)(T)
    Matrix.proj(applyOn target f(M))(x , y) =
      if      (x ≡? target) then Vector.proj(f(Matrix.col(M)(x)))(y)
      else                       Matrix.proj(M)(x , y)

module _ {ℓ₁ ℓ₂} {s} {A : Type{ℓ₁}} {B : Type{ℓ₂}} where
  -- A matrix where a function has been applied to every element.
  map : (A → B) → Matrix(s)(A) → Matrix(s)(B) -- TODO: Same implementation in Vector.agda. Generalize. Maybe like in Haskell? With Applicative, Functor and stuff?
  Matrix.proj(map f(m))(x , y) = f(Matrix.proj(m)(x , y))

module _ {ℓ₁ ℓ₂ ℓ₃} {s} {A : Type{ℓ₁}} {B : Type{ℓ₂}} {C : Type{ℓ₃}} where
  -- A matrix where a binary operator has been pairwise applied to every element of the given matrices at the same positions.
  -- This can be used to construct a component-wise operator.
  map₂ : (A → B → C) → Matrix(s)(A) → Matrix(s)(B) → Matrix(s)(C)
  Matrix.proj(map₂(_▫_) (v₁)(v₂))(x , y) = Matrix.proj(v₁)(x , y) ▫ Matrix.proj(v₂)(x , y)

module _ {ℓ} {w}{h} {T : Type{ℓ}} where
  -- A matrix from a vector of vectors. The inner vectors becomes rows.
  rowMat : Vector(h)(Vector(w)(T)) → Matrix(w , h)(T)
  Matrix.proj(rowMat(vs))(x , y) = Vector.proj(Vector.proj(vs)(y))(x)

  -- A matrix from a vector of vectors. The inner vectors becomes columns.
  colMat : Vector(w)(Vector(h)(T)) → Matrix(w , h)(T)
  Matrix.proj(colMat(vs))(x , y) = Vector.proj(Vector.proj(vs)(x))(y)

  -- A matrix represented as a vector of vectors where the inner vectors are the rows of the matrix.
  rows : Matrix(w , h)(T) → Vector(h)(Vector(w)(T))
  ((rows(M))(y))(x) = Matrix.proj(M)(x , y)

  -- A matrix represented as a vector of vectors where the inner vectors are the columns of the matrix.
  cols : Matrix(w , h)(T) → Vector(w)(Vector(h)(T))
  ((cols(M))(x))(y) = Matrix.proj(M)(x , y)

  -- Matrix with one row and one column removed.
  minor : Matrix(𝐒(w) , 𝐒(h))(T) → (𝕟(𝐒(w)) ⨯ 𝕟(𝐒(h))) → Matrix(w , h)(T)
  Matrix.proj(minor(M)(X , Y))(x , y) = Matrix.proj(M)(new-x , new-y) where
    new-x = if(x <? X) then bound-𝐒(x) else 𝐒(x)
    new-y = if(y <? Y) then bound-𝐒(y) else 𝐒(y)

module _ {ℓ} {s} {T : Type{ℓ}} where
  -- A matrix filled with a single element.
  fill : T → Matrix(s)(T)
  Matrix.proj(fill(elem)) = const(elem)

  -- submatrix : Matrix(w , h)(T) → ((X , Y) : (𝕟(w) ⨯ 𝕟(h))) → ((W , H) : (𝕟(w −₀ X) ⨯ 𝕟(h −₀ Y))) → Matrix(W −₀ X , H −₀ Y)(T)

-- A square matrix is a matrix with equal length in both directions.
SquareMatrix : ∀{ℓ} → ℕ → Type{ℓ} → Type{ℓ}
SquareMatrix(d)(T) = Matrix(d , d)(T)
module SquareMatrix {ℓ} {d} {T : Type{ℓ}} where
  module _ (m : SquareMatrix(d)(T)) where
    -- The diagonal vector.
    -- The vector consisting of the elements in the main diagonal of the matrix.
    diag : Vector(d)(T)
    (diag)(i) = Matrix.proj(m)(i , i)

    -- The maximum number of dimensions of a space that the matrix can describe linear transformations in.
    -- The width/height of the matrix.
    dim : ℕ
    dim = d

  -- The diagonal matrix from a vector.
  -- The matrix consisting of the elements from the vector in the main diagonal and a default element (zero) in the rest of the positions.
  diagMat : T → Vector(d)(T) → SquareMatrix(d)(T)
  Matrix.proj(diagMat(zero)(v))(x , y) = if (x ≡? y) then Vector.proj(v)(x) else zero

  -- Scalar matrix.
  -- The matrix consisting of a constant element in the main diagonal and a default element (zero) in the rest of the positions.
  scalarMat : T → T → SquareMatrix(d)(T)
  scalarMat(zero)(elem) = diagMat(zero)(Vector.fill(elem))

module _ {ℓ} where
  RowVector : ℕ → Type{ℓ} → Type{ℓ}
  RowVector(d)(T) = Matrix(d , 1)(T)
  module RowVector {d}{T} where
    rowVecMat : Vector(d)(T) → RowVector(d)(T)
    Matrix.proj(rowVecMat(v))(x , _) = Vector.proj(v)(x)

  ColVector : ℕ → Type{ℓ} → Type{ℓ}
  ColVector(d)(T) = Matrix(1 , d)(T)
  module ColVector {d}{T} where
    colVecMat : Vector(d)(T) → ColVector(d)(T)
    Matrix.proj(colVecMat(v))(_ , y) = Vector.proj(v)(y)

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Type{ℓ₁}} {B : Type{ℓ₂}} {C : Type{ℓ₃}} {D : Type{ℓ₄}} where
  multPattern : ∀{x y z} → (C → D → D) → (A → B → C) → D → Matrix(y , z)(A) → Matrix(x , y)(B) → Matrix(x , z)(D)
  Matrix.proj(multPattern (_+_) (_⋅_) (zero) M₁ M₂)(x , y) = Vector.foldᵣ(_+_) zero (Vector.map₂(_⋅_) (Matrix.row(M₁)(y)) (Matrix.col(M₂)(x)))

{-
module _ {ℓ} {T : Type{ℓ}} where
  detPatternX : T → ∀{d} → SquareMatrix(d)(T) → 𝕟(d) → T
  detPatternX _    {𝐒(𝟎)}    M _ = Matrix.proj M(0 , 0)
  detPatternX zero {𝐒(𝐒(d))} M y = Vector.foldᵣ {!+_!} zero (Vector.map () (Matrix.row M(y)))
-}

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:
module Data.Fin.Properties.Extra where

open import Data.Nat
    renaming (suc to S; zero to Z; _+_ to _ℕ+_; _*_ to _ℕ*_)
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open import Data.Nat.Properties
open import Data.Nat.Properties.Extra renaming (cancel-suc to S-injective)
open import Data.Nat.Properties.Simple
open import Data.Fin
open import Data.Fin.Extra
open import Data.Fin.Properties
open import Data.Product

open import Function
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open DecTotalOrder decTotalOrder renaming (refl to ≤-refl)

-- start
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- □
-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

inject-1-lemma : ∀ {n} → (i : Fin (S n)) → (¬p : toℕ i ≢ n) → toℕ (inject-1 i ¬p) ≡ toℕ i
inject-1-lemma {Z}   zero     ¬p = contradiction refl ¬p
inject-1-lemma {Z}   (suc ()) ¬p
inject-1-lemma {S n} zero     ¬p = refl
inject-1-lemma {S n} (suc i)  ¬p = cong S (inject-1-lemma i (¬p ∘ cong S))

cancel-suc : ∀ {b} {x y : Fin b} → suc x ≡ suc y → x ≡ y
cancel-suc {b} {x} {.x} refl = refl

some-lemma : ∀ {b} (x y : Fin (S b)) (xs ys : ℕ)
    → toℕ {S b} x ℕ+ xs ℕ* S b ≡ toℕ {S b} y ℕ+ ys ℕ* S b
    → x ≡ y × xs ≡ ys
some-lemma zero    zero    Z      Z      p = refl , refl
some-lemma zero    (suc n) Z      Z      ()
some-lemma (suc m) zero    Z      Z      ()
some-lemma (suc m) (suc n) Z      Z      p =
    cong suc (toℕ-injective (cancel-+-right Z (S-injective p)))
    , refl
some-lemma zero    zero    Z      (S ns) ()
some-lemma zero    (suc n) Z      (S ns) ()
some-lemma {b} (suc m) zero    Z      (S ns) p = contradiction p ¬p
    where
            ¬p : S (toℕ m ℕ+ Z) ≢ S (b ℕ+ ns ℕ* S b)
            ¬p = <⇒≢ $ s≤s $
                start
                    S (toℕ m ℕ+ Z)
                ≈⟨ +-right-identity (S (toℕ m)) ⟩
                    S (toℕ m)
                ≤⟨ bounded m ⟩
                    b
                ≤⟨ m≤m+n b (ns ℕ* S b) ⟩
                    b ℕ+ ns ℕ* S b
                □
some-lemma {b} (suc m) (suc n) Z      (S ns) p = contradiction p ¬p
    where
            ¬p : S (toℕ m ℕ+ Z) ≢ S (toℕ n ℕ+ S (b ℕ+ ns ℕ* S b))
            ¬p = <⇒≢ $ s≤s $
                start
                    S (toℕ m ℕ+ Z)
                ≈⟨ +-right-identity (S (toℕ m)) ⟩
                    S (toℕ m)
                ≤⟨ bounded m ⟩
                    b
                ≤⟨ ≤-step ≤-refl ⟩
                    S b
                ≤⟨ m≤m+n (S b) (ns ℕ* S b) ⟩
                    S (b ℕ+ ns ℕ* S b)
                ≤⟨ n≤m+n (toℕ n) (S (b ℕ+ ns ℕ* S b)) ⟩
                    toℕ n ℕ+ S (b ℕ+ ns ℕ* S b)
                □
some-lemma {b} zero    zero    (S ms) Z      ()
some-lemma {b} zero    (suc n) (S ms) Z      p = contradiction p ¬p
    where
            ¬p : S (b ℕ+ ms ℕ* S b) ≢ S (toℕ n ℕ+ Z)
            ¬p = >⇒≢ $ s≤s $
                start
                    S (toℕ n ℕ+ Z)
                ≈⟨ +-right-identity (S (toℕ n)) ⟩
                    S (toℕ n)
                ≤⟨ bounded n ⟩
                    b
                ≤⟨ m≤m+n b (ms ℕ* S b) ⟩
                    b ℕ+ ms ℕ* S b
                □
some-lemma {b} (suc m) zero    (S ms) Z     ()
some-lemma {b} (suc m) (suc n) (S ms) Z     p = contradiction p ¬p
    where
            ¬p : S (toℕ m ℕ+ S (b ℕ+ ms ℕ* S b)) ≢ S (toℕ n ℕ+ Z)
            ¬p = >⇒≢ $ s≤s $
                start
                    S (toℕ n ℕ+ Z)
                ≈⟨ +-right-identity (S (toℕ n)) ⟩
                    S (toℕ n)
                ≤⟨ bounded n ⟩
                    b
                ≤⟨ ≤-step ≤-refl ⟩
                    S b
                ≤⟨ m≤m+n (S b) (ms ℕ* S b) ⟩
                    S (b ℕ+ ms ℕ* S b)
                ≤⟨ n≤m+n (toℕ m) (S (b ℕ+ ms ℕ* S b)) ⟩
                    toℕ m ℕ+ S (b ℕ+ ms ℕ* S b)
                □
some-lemma {b} zero    zero    (S ms) (S ns) p =
    refl
    , (cong S (cancel-*-right ms ns {b} (cancel-+-left b (S-injective p))))
some-lemma {b} zero    (suc n) (S ms) (S ns) p = (proj₁ ind) , cong S (proj₂ ind)
    where
            p' : S b ℕ+ ms ℕ* S b ≡ S b ℕ+ S (toℕ n ℕ+ ns ℕ* S b)
            p' = begin
                    S (b ℕ+ ms ℕ* S b)
                ≡⟨ p ⟩
                    S (toℕ n ℕ+ S (b ℕ+ ns ℕ* S b))
                ≡⟨ sym (+-assoc (S (toℕ n)) (S b) (ns ℕ* S b)) ⟩
                    (S (toℕ n) ℕ+ S b) ℕ+ ns ℕ* S b
                ≡⟨ cong (λ x → x ℕ+ ns ℕ* S b) (+-comm (S (toℕ n)) (S b)) ⟩
                    S (b ℕ+ S (toℕ n) ℕ+ ns ℕ* S b)
                ≡⟨ +-assoc (S b) (S (toℕ n)) (ns ℕ* S b) ⟩
                    S (b ℕ+ S (toℕ n ℕ+ ns ℕ* S b))
                ∎
            ind : zero ≡ suc n × ms ≡ ns
            ind = some-lemma {b} zero (suc n) ms ns (cancel-+-left (S b) p')
some-lemma {b} (suc m) zero    (S ms) (S ns) p = (proj₁ ind) , (cong S (proj₂ ind))
    where
            p' : S b ℕ+ (S (toℕ m) ℕ+ ms ℕ* S b) ≡ S b ℕ+ ns ℕ* S b
            p' = begin
                    S b ℕ+ S (toℕ m ℕ+ ms ℕ* S b)
                ≡⟨ sym (+-assoc (S b) (S (toℕ m)) (ms ℕ* S b)) ⟩
                    S (b ℕ+ S (toℕ m) ℕ+ ms ℕ* S b)
                ≡⟨ cong (λ x → x ℕ+ ms ℕ* S b) (+-comm (S b) (S (toℕ m))) ⟩
                    S (toℕ m ℕ+ S b ℕ+ ms ℕ* S b)
                ≡⟨ +-assoc (S (toℕ m)) (S b) (ms ℕ* S b) ⟩
                    S (toℕ m ℕ+ S (b ℕ+ ms ℕ* S b))
                ≡⟨ p ⟩
                    S (b ℕ+ ns ℕ* S b)
                ∎
            ind : suc m ≡ zero × ms ≡ ns
            ind = some-lemma {b} (suc m) zero ms ns (cancel-+-left (S b) p')
some-lemma {b} (suc m) (suc n) (S ms) (S ns) p = (proj₁ ind) , (cong S (proj₂ ind))
    where
            p' : S (b ℕ+ S (toℕ m ℕ+ ms ℕ* S b)) ≡ S (b ℕ+ S (toℕ n ℕ+ ns ℕ* S b))
            p' = begin
                    S (b ℕ+ S (toℕ m ℕ+ ms ℕ* S b))
                ≡⟨ sym (+-assoc (S b) (S (toℕ m)) (ms ℕ* S b)) ⟩
                    S (b ℕ+ S (toℕ m) ℕ+ ms ℕ* S b)
                ≡⟨ cong (λ x → x ℕ+ ms ℕ* S b) (+-comm (S b) (S (toℕ m))) ⟩
                    S (toℕ m ℕ+ S b ℕ+ ms ℕ* S b)
                ≡⟨ +-assoc (S (toℕ m)) (S b) (ms ℕ* S b) ⟩
                    S (toℕ m ℕ+ S (b ℕ+ ms ℕ* S b))
                ≡⟨ p ⟩
                    S (toℕ n ℕ+ S (b ℕ+ ns ℕ* S b))
                ≡⟨ sym (+-assoc (S (toℕ n)) (S b) (ns ℕ* S b)) ⟩
                    S (toℕ n ℕ+ S b ℕ+ ns ℕ* S b)
                ≡⟨ cong (λ x → x ℕ+ ns ℕ* S b) (+-comm (S (toℕ n)) (S b)) ⟩
                    S (b ℕ+ S (toℕ n) ℕ+ ns ℕ* S b)
                ≡⟨ +-assoc (S b) (S (toℕ n)) (ns ℕ* S b) ⟩
                    S (b ℕ+ S (toℕ n ℕ+ ns ℕ* S b))
                ∎
            ind : suc m ≡ suc n × ms ≡ ns
            ind = some-lemma {b} (suc m) (suc n) ms ns (cancel-+-left (S b) p')

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Martin-Löf identity type without the K axiom
-- (we do not assume uniqueness of identity proofs).

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

module Tools.PropositionalEquality where

-- We reexport Agda's builtin equality type.

open import Tools.Empty public
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; subst₂) public
open Eq.≡-Reasoning public

-- Non-dependent congruence rules.

cong₃ : ∀ {A B C D : Set} {a a′ b b′ c c′}
        (f : A → B → C → D) → a ≡ a′ → b ≡ b′ → c ≡ c′
      → f a b c ≡ f a′ b′ c′
cong₃ f refl refl refl = refl

cong₄ : ∀ {A B C D E : Set} {a a′ b b′ c c′ d d′}
        (f : A → B → C → D → E) → a ≡ a′ → b ≡ b′ → c ≡ c′ → d ≡ d′
      → f a b c d ≡ f a′ b′ c′ d′
cong₄ f refl refl refl refl = refl

-- Substitution (type-cast).

-- Three substitutions simultaneously.

subst₃ : ∀ {A B C : Set} {a a′ b b′ c c′} (F : A → B → C → Set)
       → a ≡ a′ → b ≡ b′ → c ≡ c′ → F a b c → F a′ b′ c′
subst₃ F refl refl refl f = f

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
{-# OPTIONS --without-K  #-}
module sets.fin where

open import sets.fin.core public
open import sets.fin.properties public
open import sets.fin.ordering public
open import sets.fin.universe public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import Base
open import Homotopy.TruncatedHIT

{-
The idea is that if [n : ℕ] and [A : Set i], then [τ n A] is defined by the
following n-truncated higher inductive type:

    module Homotopy.TruncationHIT {i} (n : ℕ) (A : Set i) where

    (n)data τ : Set i where
      proj : A → τ

More explanations on the way this is done can be found in TruncatedHIT.agda.
This file contains nothing but stuff that could (should) be autogenerated from
the three lines above.
-}

module Homotopy.TruncationHIT {i} (n : ℕ₋₂) (A : Set i) where

private
  data #τ : Set i where
    #proj : A → #τ

    #top : (f : hSⁿ n → #τ) → #τ

τ : Set i
τ = #τ

proj : A → τ
proj = #proj

top : (f : hSⁿ n → τ) → τ
top = #top

postulate  -- HIT
  rays : (f : hSⁿ n → τ) (x : hSⁿ n) → top f ≡ f x
  hack-prop : (p : n ≡ ⟨-2⟩) (x y : τ) → (x ≡ y)

#τ-rec : ∀ {j} (P : τ → Set j)
  (proj* : (x : A) → P (proj x))
  {top* : (f : hSⁿ n → τ) (p : (x : hSⁿ n) → P (f x)) → P (top f)}
  {rays* : (f : hSⁿ n → τ) (p : (x : hSⁿ n) → P (f x)) (x : hSⁿ n)
    → transport P (rays f x) (top* f p) ≡ p x}
  {hack-prop* : (p : n ≡ ⟨-2⟩) (x y : τ) (x* : P x) (y* : P y)
    → (transport P (hack-prop p x y) x* ≡ y* )}
  → ((x : τ) → P x)
#τ-rec P proj* {top*} {rays*} {hack-prop*} (#proj u) = proj* u
#τ-rec P proj* {top*} {rays*} {hack-prop*} (#top f) =
  top* f (λ x → #τ-rec P proj* {top*} {rays*} {hack-prop*} (f x))

#τ-rec-nondep : ∀ {j} (C : Set j)
  (proj* : A → C)
  {top* : (f : hSⁿ n → τ) (p : hSⁿ n → C) → C}
  {rays* : (f : hSⁿ n → τ) (p : hSⁿ n → C) (x : hSⁿ n) → top* f p ≡ p x}
  {hack-prop* : (p : n ≡ ⟨-2⟩) (x y : τ) (x* y* : C) → x* ≡ y*}
  → (τ → C)
#τ-rec-nondep C proj* {top*} {rays*} {hack-prop*} (#proj u) = proj* u
#τ-rec-nondep C proj* {top*} {rays*} {hack-prop*} (#top f) =
  top* f (λ x → #τ-rec-nondep C proj* {top*} {rays*} {hack-prop*} (f x))

private
  contr : (n ≡ ⟨-2⟩) → is-contr τ
abstract
  contr p = inhab-prop-is-contr (top (λ x → abort-nondep (transport hSⁿ p x)))
                                (all-paths-is-prop (hack-prop p))

-- Computation rules for [rays] are not needed

τ-rec :  ∀ {j} (P : τ → Set j)
  (proj* : (x : A) → P (proj x))
  {hack-prop* : (p : n ≡ ⟨-2⟩) (x y : τ) (x* : P x) (y* : P y)
    → (transport P (hack-prop p x y) x* ≡ y* )}
  (trunc : (x : τ) → is-truncated n (P x))
  → ((x : τ) → P x)
τ-rec P proj* {hack-prop*} trunc =
  #τ-rec P proj* {x₁} {x₂} {hack-prop*} where
  abstract
    u : (f : hSⁿ n → τ) (p : (x : hSⁿ n) → P (f x))
      → filling-dep n P f (top f , rays f) p
    u = truncated-has-filling-dep τ P n contr (λ f → (top f , rays f))

    x₁ : (f : hSⁿ n → τ) (p : (x : hSⁿ n) → P (f x)) → P (top f)
    x₁ = λ f p → π₁ (u f p)

    x₂ : (f : hSⁿ n → τ) (p : (x : hSⁿ n) → P (f x)) (x : hSⁿ n)
      → transport P (rays f x) (x₁ f p) ≡ p x
    x₂ = λ f p → π₂ (u f p)

τ-rec-nondep : ∀ {j} (C : Set j)
  (proj* : A → C)
  {hack-prop* : (p : n ≡ ⟨-2⟩) (x y : τ) (x* y* : C) → x* ≡ y*}
  (trunc : is-truncated n C)
  → (τ → C)
τ-rec-nondep C proj* {hack-prop*} trunc =
  #τ-rec-nondep C proj* {λ _ p → π₁ (u p)}
                        {λ _ p → π₂ (u p)} {hack-prop*} where
  u : _
  u = truncated-has-spheres-filled n _ trunc

-- The nth truncation is of h-level [n]
abstract
  τ-is-truncated : is-truncated n τ
  τ-is-truncated =
    spheres-filled-is-truncated n τ contr (λ f → (top f , rays f))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, 2016-07-17

record R : Set₁ where
  abstract
    field T : Set

-- Expected error:
--
-- Using abstract here has no effect. Abstract applies only
-- definitions like data definitions, record type definitions and
-- function clauses.

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module Prelude.Unit where

open import Agda.Builtin.Unit public

record ⊤′ {a} : Set a where
  instance constructor tt

-- To keep changes from compat-2.4.0 to a minimum.
Unit = ⊤
pattern unit = tt

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Kan where

-- Left and Right Kan extensions (known as Lan and Ran)

open import Level
open import Categories.Category using (Category)
open import Categories.Functor
open import Categories.NaturalTransformation using (NaturalTransformation; _∘ʳ_; _∘ᵥ_)
open import Categories.NaturalTransformation.Equivalence using (_≃_)

private
  variable
    o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ : Level

module _ {A : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁} {C : Category o₂ ℓ₂ e₂}
           (F : Functor A B) (X : Functor A C) where

  record Lan : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ o₁ ⊔ ℓ₁ ⊔ e₁ ⊔ o₂ ⊔ ℓ₂ ⊔ e₂) where
    field
      L : Functor B C
      η : NaturalTransformation X (L ∘F F)

      σ : (M : Functor B C) → (α : NaturalTransformation X (M ∘F F)) → NaturalTransformation L M

      σ-unique : {M : Functor B C} → {α : NaturalTransformation X (M ∘F F)} →
                  (σ′ : NaturalTransformation L M) → α ≃ (σ′ ∘ʳ F) ∘ᵥ η → σ′ ≃ σ M α
      commutes : (M : Functor B C) → (α : NaturalTransformation X (M ∘F F)) → α ≃ (σ M α ∘ʳ F) ∘ᵥ η

    module L = Functor L
    module η = NaturalTransformation η

  record Ran : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ o₁ ⊔ ℓ₁ ⊔ e₁ ⊔ o₂ ⊔ ℓ₂ ⊔ e₂) where
    field
      R : Functor B C
      ε : NaturalTransformation (R ∘F F) X

      δ : (M : Functor B C) → (α : NaturalTransformation (M ∘F F) X) → NaturalTransformation M R

      δ-unique : {M : Functor B C} → {α : NaturalTransformation (M ∘F F) X} →
                  (δ′ : NaturalTransformation M R) → α ≃ ε ∘ᵥ (δ′ ∘ʳ F) → δ′ ≃ δ M α
      commutes : (M : Functor B C) → (α : NaturalTransformation (M ∘F F) X) → α ≃ ε ∘ᵥ (δ M α ∘ʳ F)

    module R = Functor R
    module ε = NaturalTransformation ε

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Categories.Category
open import Categories.Category.Complete.Finitely

module Categories.Category.Complete.Finitely.Properties {o ℓ e} {C : Category o ℓ e} (finite : FinitelyComplete C) where

open import Level using (Level)
open import Data.Nat using (ℕ)
open import Data.Product using (Σ; _,_; proj₁; ∃₂) renaming (_×_ to _&_)
open import Data.Fin
open import Data.Fin.Properties
open import Data.Sum using (inj₁; inj₂)
open import Data.List hiding ([_])
open import Data.List.Relation.Unary.Any as Any using (here; there)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Relation.Unary.Unique.Propositional
open import Data.List.Membership.Propositional
open import Relation.Binary.PropositionalEquality as ≡ using (refl; _≡_; cong)
open import Function renaming (_∘_ to _∙_)

import Data.List.Relation.Unary.Unique.Propositional.Properties as Uₚ
import Data.List.Membership.Propositional.Properties as ∈ₚ
import Data.List.Membership.Setoid.Properties as S∈ₚ

open import Categories.Category
open import Categories.Category.Cartesian.Properties C
open import Categories.Category.Finite.Fin
open import Categories.Diagram.Equalizer C
open import Categories.Morphism.Reasoning C
open import Categories.Functor

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

open FinitelyComplete finite

module GeneralProperties where

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

    concatMap-∈ : ∀ {b} {B : Set b} (f : A → List B) {l : List A} →
                  ∀ {x y} → x ∈ l → y ∈ f x → y ∈ concatMap f l
    concatMap-∈ f (here refl) y∈fx     = ++⁺ˡ y∈fx
    concatMap-∈ f (there {z} x∈l) y∈fx = ++⁺ʳ (f z) (concatMap-∈ f x∈l y∈fx)

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

    concatMap²-∈ : ∀ {m n} {ms : List (Fin m)} {ns : List (Fin n)}
                     (f : Fin m → Fin n → List A) →
                     ∀ {x y k} → x ∈ ms → y ∈ ns → k ∈ f x y →
                       k ∈ concatMap (λ z → concatMap (λ w → f z w) ns) ms
    concatMap²-∈ {m} {n} {ms} {ns} f {x} {y} {k} x∈ms y∈ns k∈fxy = concatMap-∈ _ x∈ms k∈ns
      where k∈ns : k ∈ concatMap (λ w → f x w) ns
            k∈ns  = concatMap-∈ _ y∈ns k∈fxy

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

      concatMap²-map-∈ : ∀ {m n} {ms : List (Fin m)} {ns : List (Fin n)}
                           (f : Fin m → Fin n → List A) →
                           (g : A → B) →
                           ∀ {x y k} → x ∈ ms → y ∈ ns → k ∈ f x y →
                             g k ∈ map g (concatMap (λ z → concatMap (λ w → f z w) ns) ms)
      concatMap²-map-∈ f g x∈ms y∈ns k∈fxy = map⁺ (Any.map (cong g) (concatMap²-∈ f x∈ms y∈ns k∈fxy))

open GeneralProperties
open Prods cartesian

-- construct a finite limit from cartesian products and equalizer
--
-- c.f. Awodey 5.21
module _ (shape : FinCatShape) (F : Functor (FinCategory shape) C) where
  private
    module C = Category C
    open C
    open HomReasoning
    S = FinCategory shape
    open Co F
    open Lim F
    open FinCatShape shape using (size; ∣_⇒_∣; objects; morphisms; wrap-arr; Obj-UIP)
    module S = Category S
    module F = Functor F

    obj∈-irr : ∀ {x} → (p q : x ∈ objects) → p ≡ q
    obj∈-irr = S∈ₚ.unique⇒irrelevant (≡.setoid _) Obj-UIP (Uₚ.allFin⁺ size)

    prods-gen : List (Fin size) → Obj
    prods-gen ns = prod (map F.₀ ns)

    prods : Obj
    prods = prods-gen objects

    cods : List Obj
    cods = map (λ n → F.₀ (Arrow.cod n)) morphisms

    arrs : Obj
    arrs = prod cods

    ∈-objects : ∀ n → n ∈ objects
    ∈-objects n = ∈ₚ.∈-allFin n

    Fn∈obj : ∀ n → F.₀ n ∈ map F.₀ objects
    Fn∈obj n = ∈ₚ.∈-map⁺ F.₀ (∈-objects n)

    π : ∀ n → prods ⇒ F.₀ n
    π n = π[ Fn∈obj n ]

    ϕ⇒ : ∀ (a : Arrow size ∣_⇒_∣) → prods ⇒ F.F₀ (Arrow.cod a)
    ϕ⇒ a = π (Arrow.cod a)

    ϕπ : prods ⇒ cods *
    ϕπ = build-mors _ ϕ⇒ morphisms

    ϕ : prods ⇒ arrs
    ϕ = ⟨ ϕπ ⟩*

    ψ⇒ : ∀ a → prods ⇒ F.F₀ (Arrow.cod a)
    ψ⇒ a = F.₁ (Arrow.arr a) ∘ π (Arrow.dom a)

    ψπ : prods ⇒ cods *
    ψπ = build-mors _ ψ⇒ morphisms

    ψ : prods ⇒ arrs
    ψ = ⟨ ψπ ⟩*

    ∈-morphisms : ∀ {d c} (f : Fin ∣ d ⇒ c ∣) → record { arr = f } ∈ morphisms
    ∈-morphisms {d} {c} f = concatMap²-∈ (λ _ _ → tabulate wrap-arr) (∈-objects d) (∈-objects c) (∈ₚ.∈-tabulate⁺ f)

    Fc∈cods : ∀ {d c} (f : Fin ∣ d ⇒ c ∣) → F.₀ c ∈ cods
    Fc∈cods f = ∈ₚ.∈-map⁺ (λ a → F.₀ (Arrow.cod a)) (∈-morphisms f)

    π′ : ∀ {d c} (f : Fin ∣ d ⇒ c ∣) → arrs ⇒ F.₀ c
    π′ f = π[ Fc∈cods f ]

    ψπ-proj : ∀ {d c} (f : Fin ∣ d ⇒ c ∣) →
                F.₁ f ∘ π d ≈ π[ Fc∈cods f ] ∘ ψ
    ψπ-proj f = build-proj (λ a → F.₀ (Arrow.cod a))
                           (λ a → F.₁ (Arrow.arr a) ∘ π (Arrow.dom a))
                           (∈-morphisms f)

    ϕπ-proj : ∀ {d c} (f : Fin ∣ d ⇒ c ∣) →
                π c ≈ π[ Fc∈cods f ] ∘ ϕ
    ϕπ-proj f = build-proj (λ a → F.₀ (Arrow.cod a))
                           (λ a → π (Arrow.cod a))
                           (∈-morphisms f)

    e⇒prods : Equalizer ψ ϕ
    e⇒prods = equalizer ψ ϕ

    module e⇒prods = Equalizer e⇒prods

    open e⇒prods

    ⊤cone : Cone
    ⊤cone = record
      { N    = obj
      ; apex = record
        { ψ       = λ n → π n ∘ arr
        ; commute = λ {m n} f → begin
          F.₁ f ∘ π m ∘ arr ≈⟨ pullˡ (ψπ-proj f) ⟩
          (π′ f ∘ ψ) ∘ arr  ≈⟨ pullʳ equality ⟩
          π′ f ∘ ϕ ∘ arr    ≈˘⟨ pushˡ (ϕπ-proj f) ⟩
          π n ∘ arr         ∎
        }
      }

    module _ {K : Cone} where
      private
        module K = Cone K

      N⇒* : K.N ⇒ map F.₀ objects *
      N⇒* = build-mors F.₀ K.ψ objects

      Kmor : K.N ⇒ prods
      Kmor = ⟨ N⇒* ⟩*

      ψ∘Kmor≈ϕ∘Kmor : ∀ a → ψ⇒ a ∘ Kmor ≈ ϕ⇒ a ∘ Kmor
      ψ∘Kmor≈ϕ∘Kmor a = begin
        ψ⇒ a ∘ Kmor                           ≈˘⟨ pushʳ (build-proj F.₀ K.ψ (∈-objects (Arrow.dom a))) ⟩
        F.₁ (Arrow.arr a) ∘ K.ψ (Arrow.dom a) ≈⟨ K.commute (Arrow.arr a) ⟩
        K.ψ (Arrow.cod a)                     ≈⟨ build-proj F.₀ K.ψ (∈-objects (Arrow.cod a)) ⟩
        ϕ⇒ a ∘ Kmor                           ∎

      equalize-eq : ψ ∘ Kmor ≈ ϕ ∘ Kmor
      equalize-eq = begin
        ψ ∘ Kmor                                        ≈⟨ build-⟨⟩*∘ _ ψ⇒ Kmor morphisms ⟩
        ⟨ build-mors _ (λ a → ψ⇒ a ∘ Kmor) morphisms ⟩* ≈⟨ build-uniqueness* _ ψ∘Kmor≈ϕ∘Kmor morphisms ⟩
        ⟨ build-mors _ (λ a → ϕ⇒ a ∘ Kmor) morphisms ⟩* ≈˘⟨ build-⟨⟩*∘ _ ϕ⇒ Kmor morphisms ⟩
        ϕ ∘ Kmor ∎

      !cone : Cone⇒ K ⊤cone
      !cone = record
        { arr     = equalize equalize-eq
        ; commute = commute _
        }
        where commute : ∀ n → (π n ∘ arr) ∘ equalize equalize-eq ≈ K.ψ n
              commute n = begin
                (π n ∘ arr) ∘ equalize equalize-eq ≈˘⟨ pushʳ universal ⟩
                π n ∘ Kmor                         ≈˘⟨ build-proj _ K.ψ (∈-objects n) ⟩
                K.ψ n                              ∎

    module _ {K : Cone} (f : Cones [ K , ⊤cone ]) where
      private
        module K = Cone K
        module f = Cone⇒ f

      !cone-unique : Cones [ !cone ≈ f ]
      !cone-unique = begin
        equalize equalize-eq ≈˘⟨ e⇒prods.unique eq ⟩
        f.arr                ∎
        where eq″ : ∀ y → π y ∘ arr ∘ f.arr ≈ π y ∘ Kmor {K}
              eq″ y = begin
                π y ∘ arr ∘ f.arr   ≈⟨ sym-assoc ⟩
                (π y ∘ arr) ∘ f.arr ≈⟨ f.commute ⟩
                K.ψ y               ≈⟨ build-proj _ K.ψ (∈-objects y) ⟩
                π y ∘ Kmor {K}      ∎

              eq′ : ∀ {y : Fin size} (y∈ys : y ∈ objects) →
                    π[ ∈ₚ.∈-map⁺ F.₀ y∈ys ] ∘ arr ∘ f.arr ≈ π[ ∈ₚ.∈-map⁺ F.₀ y∈ys ] ∘ Kmor {K}
              eq′ {y} y∈ys with obj∈-irr y∈ys (∈-objects y)
              ... | refl = eq″ y

              eq : Kmor {K} ≈ arr ∘ f.arr
              eq = sym (uniqueness*′ F.₀ {K.N} {objects} eq′)

  finiteLimit : Limit
  finiteLimit = record
    { terminal = record
      { ⊤        = ⊤cone
      ; !        = !cone
      ; !-unique = !cone-unique
      }
    }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

record × (A B : Prop) : Prop where
  field
    fst : A
    snd : B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

postulate F : Set → Set

{-# POLARITY F ++ #-}


text:
{-# OPTIONS  --no-termination-check #-}
module Data.Bin.DivModTests where

open import Data.Bin.DivMod
open Everything using (BinFin; _divMod_; result)
open import IO
open import Data.Bin hiding (suc; fromℕ)
open import Data.String hiding (_≟_)
open import Data.Unit hiding (_≟_)
open import Coinduction
open import Data.List
open import Data.Char hiding (_≟_)
open import Data.Digit hiding (toDigits)
open import Data.Fin hiding (_+_; fromℕ; _≟_)
open import Data.Bin.Bijection using (fromℕ)

showBits : Bin → String
showBits x = fromList (Data.List.reverse (Data.List.map showDigit (toBits x)))

open import Relation.Nullary.Decidable
import Data.Bin.Properties
-- eq =  Data.Bin.Properties._≟_
open import Relation.Binary
open import Data.Bin.Properties using (<-strictTotalOrder)
open StrictTotalOrder <-strictTotalOrder using (_≟_)

toDigits : (base : Bin) → {≢0 : False (base ≟ (fromℕ 0))} → Bin → List (BinFin base)
toDigits _ 0# = []
toDigits base {≢0} x with (x divMod base) {≢0}
... | result q r _ = r ∷ toDigits base {≢0} q -- still need to prove termination of this

showBinDigit : Bin → Char
showBinDigit 0# = '0'
showBinDigit ([] 1#) = '1'
showBinDigit ((zero ∷ []) 1#) = '2'
showBinDigit ((suc zero ∷ []) 1#) = '3'
showBinDigit ((zero ∷ zero ∷ []) 1#) = '4'
showBinDigit ((suc zero ∷ zero ∷ []) 1#) = '5'
showBinDigit ((zero ∷ suc zero ∷ []) 1#) = '6'
showBinDigit ((suc zero ∷ suc zero ∷ []) 1#) = '7'
showBinDigit ((zero ∷ zero ∷ zero ∷ []) 1#) = '8'
showBinDigit ((suc zero ∷ zero ∷ zero ∷ []) 1#) = '9'
showBinDigit _ = 'x'

open import Function
open import Data.Product

showDigits : Bin → String
showDigits x = fromList (Data.List.reverse (Data.List.map (showBinDigit ∘ proj₁) (toDigits (fromℕ 10) x)))

test : Bin → String
test x = showDigits x

go : Bin → IO ⊤
go n = ♯ putStrLn (test n) >> ♯ go (n + (fromℕ 1))

main = run (go (fromℕ 0))

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
open import Nat
open import Prelude
open import List
open import judgemental-erase
open import statics-checks
open import statics-core

module constructability where
  -- we construct expressions and types by induction on their
  -- structure. for each sub term, we call the relevant theorem, then
  -- assemble the results with carefully chosen lists of actions that allow
  -- us to call the appropriate zipper lemmas and maintain well-typedness
  -- at every stage of the contruction.
  --
  -- the proof term at each stage except subsumption is, morally, just the
  -- mapping of the fragment of the action semantics used by the constructs
  -- in the list in the current formation context into the list monoid.

  -- if the name of the given hole is irrelevant
  irr-hole : Nat
  irr-hole = 0

  -- construction of types
  construct-type : (t : htyp) → Σ[ L ∈ List action ] runtype (▹ ⦇-⦈ ◃) L (▹ t ◃)
  construct-type num  = [ construct num ] , DoType TMConNum DoRefl
  construct-type ⦇-⦈ = [ del irr-hole ] , DoType TMDel DoRefl
  construct-type (t1 ==> t2) with construct-type t1 | construct-type t2
  ... | (l1 , ih1) | (l2 , ih2) = l1 ++ construct arrow :: l2 ++ [ move parent ] ,
                                  runtype++ ih1
                                   (DoType TMConArrow
                                     (runtype++ (ziplem-tmarr2 ih2)
                                       (DoType TMArrParent2 DoRefl)))
  construct-type (t1 ⊕ t2) with construct-type t1 | construct-type t2
  ... | (l1 , ih1) | (l2 , ih2) = l1 ++ construct sum :: l2 ++ [ move parent ] ,
                                  runtype++ ih1
                                    (DoType TMConPlus
                                       (runtype++ (ziplem-tmplus2 ih2)
                                         (DoType TMPlusParent2 DoRefl)))
  construct-type (t1 ⊠ t2) with construct-type t1 | construct-type t2
  ... | (l1 , ih1) | (l2 , ih2) = l1 ++ construct prod :: l2 ++ [ move parent ] ,
                                  runtype++ ih1
                                    (DoType TMConProd
                                      (runtype++ (ziplem-tmprod2 ih2)
                                        (DoType TMProdParent2 DoRefl)))
  mutual
    -- construction of expressions in synthetic positions
    construct-synth : {Γ : tctx} {u : Nat} {t : htyp} {e : hexp} →
                      (Γ ⊢ e => t) →
                      Σ[ L ∈ List action ]
                        runsynth Γ ▹ ⦇-⦈[ u ] ◃ ⦇-⦈ L ▹ e ◃ t
      -- the three base cases
    construct-synth (SVar x) = [ construct (var _ irr-hole) ] , DoSynth (SAConVar x) DoRefl
    construct-synth SNum = [ construct (numlit _ irr-hole) ] , DoSynth SAConNumlit DoRefl
    construct-synth SEHole = [ del _ ] , DoSynth SADel DoRefl

      -- the inductive cases
    construct-synth (SPlus e1 e2 ) with construct-ana e1 | construct-ana e2
    ... | (l1 , ih1) | (l2 , ih2) =
      construct (plus irr-hole irr-hole) :: (l2 ++ move parent ::
         move (child 1) :: (l1 ++ [ move parent ])) ,
      DoSynth (SAConPlus1 TCHole2)
       (runsynth++ (ziplem-plus2 ih2)
        (DoSynth (SAMove EMPlusParent2)
         (DoSynth (SAMove EMPlusChild1)
          (runsynth++ (ziplem-plus1 ih1)
           (DoSynth (SAMove EMPlusParent1) DoRefl)))))

    construct-synth {t = t} (SAsc x) with construct-type t | construct-ana x
    ... | (l1 , ih1) | (l2 , ih2) =
      construct asc :: (l1 ++ move parent :: move (child 1) :: (l2 ++ [ move parent ])) ,
      DoSynth SAConAsc
       (runsynth++ (ziplem-asc2 ETTop ETTop ih1)
        (DoSynth (SAMove EMAscParent2)
         (DoSynth (SAMove EMAscChild1)
          (runsynth++ (ziplem-asc1 ih2)
           (DoSynth (SAMove EMAscParent1) DoRefl)))))

    construct-synth {t = t1 ==> t2} (SLam x wt) with construct-type t1 | construct-synth wt
    ... | l1 , ih1 | l2 , ih2 =
      construct (lam _ irr-hole irr-hole) ::
        (l1 ++ (move parent :: move (child 2) :: (l2 ++ [ move parent ]))) ,
      DoSynth (SAConLam x)
       (runsynth++ (ziplem-halflam1 x ETTop (rel◆t _) ih1)
        (DoSynth (SAMove EMHalfLamParent1)
         (DoSynth (SAMove EMHalfLamChild2)
          (runsynth++ (ziplem-halflam2 x EETop SEHole ih2)
           (DoSynth (SAMove EMHalfLamParent2) DoRefl)))))

    construct-synth (SAp e1 m e2) with construct-synth e1 | construct-ana e2
    ... | l1 , ih1 | l2 , ih2 =
      l1 ++ construct (ap irr-hole irr-hole) :: (l2 ++ [ move parent ]) ,
      runsynth++ ih1
       (DoSynth (SAConApArr m)
        (runsynth++ (ziplem-ap2 e1 m ih2)
         (DoSynth (SAMove EMApParent2) DoRefl)))

    construct-synth (SNEHole {u = u} wt) with construct-synth wt
    ... | l , ih = l ++ construct (nehole u) :: move parent :: [] ,
                   runsynth++ ih
                    (DoSynth SAConNEHole
                     (DoSynth (SAMove EMNEHoleParent) DoRefl))

    construct-synth (SPair e1 e2) with construct-synth e1 | construct-synth e2
    ... | l1 , ih1 | l2 , ih2 =
      construct (pair irr-hole irr-hole) :: (l1 ++ move parent :: move (child 2)
        :: l2 ++ [ move parent ]) ,
      DoSynth SAConPair
       (runsynth++ (ziplem-pair1 EETop SEHole ih1 SEHole)
        (DoSynth (SAMove EMPairParent1)
         (DoSynth (SAMove EMPairChild2)
          (runsynth++ (ziplem-pair2 e1 EETop SEHole ih2)
           (DoSynth (SAMove EMPairParent2) DoRefl)))))

    construct-synth (SFst e pr) with construct-synth e
    ... | l , ih = l ++ [ construct (fst irr-hole) ] ,
                   runsynth++ ih (DoSynth (SAConFst1 pr) DoRefl)

    construct-synth (SSnd e pr) with construct-synth e
    ... | l , ih = l ++ [ construct (snd irr-hole) ] ,
                   runsynth++ ih (DoSynth (SAConSnd1 pr) DoRefl)

    -- construction of expressions in analytic positions
    construct-ana : {Γ : tctx} {u : Nat} {t : htyp} {e : hexp} →
                    (Γ ⊢ e <= t) →
                    Σ[ L ∈ List action ]
                      runana Γ ▹ ⦇-⦈[ u ] ◃ L ▹ e ◃ t
    construct-ana (ASubsume x c) with construct-synth x
    ... | l , ih = construct (nehole irr-hole) :: l ++ (move parent :: finish :: []) ,
                   DoAna (AASubsume EETop SEHole SAConNEHole TCHole1)
                    (runana++  (ziplem-nehole-b SEHole c ih)
                     (DoAna (AAMove EMNEHoleParent)
                      (DoAna (AAFinish (ASubsume x c)) DoRefl)))

    construct-ana (ALam a m e) with construct-ana e
    ... | l , ih = construct (lam _ irr-hole irr-hole) :: (l ++ [ move parent ]) ,
                   DoAna (AAConLam1 a m)
                    (runana++ (ziplem-lam a m ih)
                     (DoAna (AAMove EMLamParent) DoRefl))

    construct-ana (AInl m wt) with construct-ana wt
    ... | l , ih = construct (inl irr-hole irr-hole) :: l ++ [ move parent ]  ,
                   DoAna (AAConInl1 m)
                    (runana++ (ziplem-inl m ih)
                     (DoAna (AAMove EMInlParent) DoRefl))

    construct-ana (AInr m wt) with construct-ana wt
    ... | l , ih = construct (inr irr-hole irr-hole) :: l ++ [ move parent ]  ,
                   DoAna (AAConInr1 m)
                    (runana++ (ziplem-inr m ih)
                     (DoAna (AAMove EMInrParent) DoRefl))

    construct-ana (ACase {x = x} {y = y} x# y# m wt0 wt1 wt2)
      with construct-synth wt0
         | construct-ana wt1
         | construct-ana wt2
    ... | l0 , ih0 | l1 , ih1 | l2 , ih2 =
      construct (case x y irr-hole irr-hole irr-hole) :: construct (nehole irr-hole) ::
      l0 ++ (move parent :: finish :: move parent :: move (child 2) ::
      l1 ++ (move parent :: move (child 3) ::
      l2 ++ [ move parent ])) ,
      DoAna (AAConCase x# y#)
       (DoAna (AAZipCase1 x# y# EETop SEHole SAConNEHole MSHole
              (ASubsume SEHole TCHole1) (ASubsume SEHole TCHole1))
        (runana++ (ziplem-case1b x# y# EETop SEHole ih0)
         (DoAna (AAZipCase1 x# y# (EENEHole EETop)
                (SNEHole wt0) (SAMove EMNEHoleParent) MSHole (ASubsume SEHole TCHole1)
                (ASubsume SEHole TCHole1))
          (DoAna (AAZipCase1 x# y# EETop (SNEHole wt0) (SAFinish wt0) m
                 (ASubsume SEHole TCHole1) (ASubsume SEHole TCHole1))
           (DoAna (AAMove EMCaseParent1)
            (DoAna (AAMove EMCaseChild2)
             (runana++ (ziplem-case2 x# y# wt0 (ASubsume SEHole TCHole1) m ih1)
              (DoAna (AAMove EMCaseParent2)
               (DoAna (AAMove EMCaseChild3)
                (runana++ (ziplem-case3 x# y# wt0 wt1 m ih2)
                 (DoAna (AAMove EMCaseParent3) DoRefl)))))))))))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
-- Andreas, 2017-01-12, issue #2386

postulate
  B : Set

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

{-# BUILTIN EQUALITY _≡_ #-}

-- Wrong type of _≡_

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Prelude

module Implicits.Substitutions.Context where

open import Implicits.Syntax.Type
open import Implicits.Syntax.Context
open import Implicits.Substitutions.Type as TS using ()

open import Data.Fin.Substitution
open import Data.Star as Star hiding (map)
open import Data.Star.Properties
open import Data.Vec
open import Data.List as List using ()

ktx-map : ∀ {ν μ n} → (Type ν → Type μ) →  Ktx ν n → Ktx μ n
ktx-map f (Γ , Δ) = map f Γ , List.map f Δ

_/_ : ∀ {ν μ n} → Ktx ν n → Sub Type ν μ → Ktx μ n
K / σ = ktx-map (λ t → t TS./ σ) K

_/Var_ : ∀ {ν m n} → Sub Fin n m → Ktx ν m → Ktx ν n
σ /Var (Γ , Δ) = map (λ x → lookup x Γ) σ , Δ

ictx-weaken : ∀ {ν} → ICtx ν → ICtx (suc ν)
ictx-weaken Δ = List.map (flip TS._/_ TS.wk) Δ

ctx-weaken : ∀ {ν n} → Ctx ν n → Ctx (suc ν) n
ctx-weaken Γ = map (flip TS._/_ TS.wk) Γ

weaken : ∀ {ν n} → Ktx ν n → Ktx (suc ν) n
weaken K = K / TS.wk


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

open import lib.Basics
open import lib.cubical.Square
open import lib.types.Group
open import lib.types.EilenbergMacLane1.Core

module lib.types.EilenbergMacLane1.PathElim where

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

  private
    module G = Group G

  module EM₁Level₂PathElim {k} {C : Type k}
    {{C-level : has-level 2 C}}
    (f₁ f₂ : EM₁ G → C)
    (embase* : f₁ embase == f₂ embase)
    (emloop* : ∀ g →
      Square embase* (ap f₁ (emloop g))
             (ap f₂ (emloop g)) embase*)
    (emloop-comp* : ∀ g₁ g₂ →
      emloop* (G.comp g₁ g₂) ⊡v∙
      ap (ap f₂) (emloop-comp' G g₁ g₂)
      ==
      ap (ap f₁) (emloop-comp' G g₁ g₂) ∙v⊡
      ↓-='-square-comp (emloop* g₁) (emloop* g₂))
    where

    private
      module M =
        EM₁Level₁Elim {i} {G}
          {P = λ x → f₁ x == f₂ x}
          {{λ x → has-level-apply C-level _ _}}
          embase*
          (λ g → ↓-='-from-square (emloop* g))
          (λ g₁ g₂ →
            ↓-='-from-square-comp-path (emloop-comp g₁ g₂)
                                       (emloop* g₁)
                                       (emloop* g₂)
                                       (emloop* (G.comp g₁ g₂))
                                       (emloop-comp* g₁ g₂))

    open M public

  module EM₁Level₂PathConstElim {k} {C : Type k}
    {{C-level : has-level 2 C}}
    (f : EM₁ G → C) (c : C)
    (embase* : f embase == c)
    (emloop* : ∀ g →
      Square embase* (ap f (emloop g))
             idp embase*)
    (emloop-comp* : ∀ g₁ g₂ →
      emloop* (G.comp g₁ g₂)
      ==
      (ap (ap f) (emloop-comp' G g₁ g₂) ∙
       ap-∙ f (emloop g₁) (emloop g₂)) ∙v⊡
      (emloop* g₁ ⊡h emloop* g₂))
    where

    emloop** : ∀ g → Square embase* (ap f (emloop g))
                                    (ap (cst c) (emloop' G g)) embase*
    emloop** g = emloop* g ⊡v∙ ! (ap-cst c (emloop g))

    private

      emloop-comp** : ∀ g₁ g₂ →
        emloop** (G.comp g₁ g₂) ⊡v∙ ap (ap (cst c)) (emloop-comp' G g₁ g₂)
        ==
        ap (ap f) (emloop-comp g₁ g₂) ∙v⊡
        ↓-='-square-comp (emloop** g₁) (emloop** g₂)
      emloop-comp** g₁ g₂ =
        (emloop* (G.comp g₁ g₂) ⊡v∙ ! (ap-cst c (emloop (G.comp g₁ g₂)))) ⊡v∙ ap (ap (cst c)) (emloop-comp g₁ g₂)
          =⟨ ⊡v∙-assoc (emloop* (G.comp g₁ g₂))
                       (! (ap-cst c (emloop (G.comp g₁ g₂))))
                       (ap (ap (cst c)) (emloop-comp g₁ g₂)) ⟩
        emloop* (G.comp g₁ g₂) ⊡v∙
        (! (ap-cst c (emloop (G.comp g₁ g₂))) ∙
        ap (ap (cst c)) (emloop-comp g₁ g₂))
          =⟨ ap (emloop* (G.comp g₁ g₂) ⊡v∙_) $ =ₛ-out $
             ! (ap-cst c (emloop (G.comp g₁ g₂))) ◃∙
             ap (ap (cst c)) (emloop-comp g₁ g₂) ◃∎
               =ₛ⟨ pre-rotate'-in $
                   post-rotate-in {p = _ ◃∎} $
                   homotopy-naturality-to-cst (ap (cst c)) idp (ap-cst c) (emloop-comp g₁ g₂) ⟩
             ! (ap-cst c (emloop g₁ ∙ emloop g₂)) ◃∎
               =ₛ⟨ !-=ₛ (ap-cst-coh c (emloop g₁) (emloop g₂)) ⟩
             ! (ap2 _∙_ (ap-cst c (emloop g₁)) (ap-cst c (emloop g₂))) ◃∙
             ! (ap-∙ (cst c) (emloop g₁) (emloop g₂)) ◃∎
               =ₛ₁⟨ 0 & 1 & !-ap2 _∙_ (ap-cst c (emloop g₁)) (ap-cst c (emloop g₂)) ⟩
             ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂))) ◃∙
             ! (ap-∙ (cst c) (emloop g₁) (emloop g₂)) ◃∎
               =ₛ₁⟨ 1 & 1 & !ap-∙=∙-ap (cst c) (emloop g₁) (emloop g₂) ⟩
             ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂))) ◃∙
             ∙-ap (cst c) (emloop g₁) (emloop g₂) ◃∎ ∎ₛ
           ⟩
        emloop* (G.comp g₁ g₂) ⊡v∙
        (ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂))) ∙
        ∙-ap (cst c) (emloop g₁) (emloop g₂))
          =⟨ ! $ ⊡v∙-assoc (emloop* (G.comp g₁ g₂))
                           (ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂))))
                           (∙-ap (cst c) (emloop g₁) (emloop g₂)) ⟩
        (emloop* (G.comp g₁ g₂) ⊡v∙
        ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂)))) ⊡v∙
        ∙-ap (cst c) (emloop g₁) (emloop g₂)
          =⟨ ap (λ s → (s ⊡v∙
                       ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂)))) ⊡v∙
                       ∙-ap (cst c) (emloop g₁) (emloop g₂))
                (emloop-comp* g₁ g₂) ⟩
        (((ap (ap f) (emloop-comp' G g₁ g₂) ∙
        ap-∙ f (emloop g₁) (emloop g₂)) ∙v⊡
        emloop* g₁ ⊡h emloop* g₂) ⊡v∙
        ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂)))) ⊡v∙
        ∙-ap (cst c) (emloop g₁) (emloop g₂)
          =⟨ ap (_⊡v∙ ∙-ap (cst c) (emloop g₁) (emloop g₂)) $
             ((ap (ap f) (emloop-comp' G g₁ g₂) ∙
             ap-∙ f (emloop g₁) (emloop g₂)) ∙v⊡
             emloop* g₁ ⊡h emloop* g₂) ⊡v∙
             ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂)))
               =⟨ ∙v⊡-⊡v∙-comm
                    (ap (ap f) (emloop-comp' G g₁ g₂) ∙ ap-∙ f (emloop g₁) (emloop g₂))
                    (emloop* g₁ ⊡h emloop* g₂)
                    (ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂)))) ⟩
             (ap (ap f) (emloop-comp' G g₁ g₂) ∙
             ap-∙ f (emloop g₁) (emloop g₂)) ∙v⊡
             ((emloop* g₁ ⊡h emloop* g₂) ⊡v∙
             ap2 _∙_ (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂))))
               =⟨ ap ((ap (ap f) (emloop-comp' G g₁ g₂) ∙
                       ap-∙ f (emloop g₁) (emloop g₂)) ∙v⊡_) $
                  ⊡h-⊡v∙-comm (emloop* g₁) (emloop* g₂)
                              (! (ap-cst c (emloop g₁))) (! (ap-cst c (emloop g₂))) ⟩
             (ap (ap f) (emloop-comp' G g₁ g₂) ∙
             ap-∙ f (emloop g₁) (emloop g₂)) ∙v⊡
             (emloop** g₁ ⊡h emloop** g₂)
               =⟨ ∙v⊡-assoc (ap (ap f) (emloop-comp' G g₁ g₂))
                            (ap-∙ f (emloop g₁) (emloop g₂))
                            (emloop** g₁ ⊡h emloop** g₂) ⟩
             ap (ap f) (emloop-comp' G g₁ g₂) ∙v⊡
             (ap-∙ f (emloop g₁) (emloop g₂) ∙v⊡
             (emloop** g₁ ⊡h emloop** g₂)) =∎
           ⟩
        (ap (ap f) (emloop-comp' G g₁ g₂) ∙v⊡
        (ap-∙ f (emloop g₁) (emloop g₂) ∙v⊡
        (emloop** g₁ ⊡h emloop** g₂))) ⊡v∙
        ∙-ap (cst c) (emloop g₁) (emloop g₂)
          =⟨ ∙v⊡-⊡v∙-comm (ap (ap f) (emloop-comp' G g₁ g₂))
                          (ap-∙ f (emloop g₁) (emloop g₂) ∙v⊡ (emloop** g₁ ⊡h emloop** g₂))
                          (∙-ap (cst c) (emloop g₁) (emloop g₂)) ⟩
        ap (ap f) (emloop-comp' G g₁ g₂) ∙v⊡
        (ap-∙ f (emloop g₁) (emloop g₂) ∙v⊡ emloop** g₁ ⊡h emloop** g₂) ⊡v∙ ∙-ap (cst c) (emloop g₁) (emloop g₂)
          =⟨ ap (ap (ap f) (emloop-comp' G g₁ g₂) ∙v⊡_) $
             ∙v⊡-⊡v∙-comm (ap-∙ f (emloop g₁) (emloop g₂))
                          (emloop** g₁ ⊡h emloop** g₂)
                          (∙-ap (cst c) (emloop g₁) (emloop g₂)) ⟩
        ap (ap f) (emloop-comp' G g₁ g₂) ∙v⊡
        ↓-='-square-comp' (emloop** g₁) (emloop** g₂)
          =⟨ ap (ap (ap f) (emloop-comp' G g₁ g₂) ∙v⊡_) $
             ↓-='-square-comp'=↓-='-square-comp {f = f} {g = cst c}
                                                (emloop** g₁) (emloop** g₂) ⟩
        ap (ap f) (emloop-comp g₁ g₂) ∙v⊡
        ↓-='-square-comp (emloop** g₁) (emloop** g₂) =∎

      module M =
        EM₁Level₂PathElim {k} {C}
          {{C-level}}
          f (cst c)
          embase*
          emloop**
          emloop-comp**

    open M public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
postulate
  ANY : ∀{a}{A : Set a} → A

data Ty : Set where
  _⇒_ : (a b : Ty) → Ty

data Tm : (b : Ty) → Set where
  S   : ∀{c a b} → Tm ((c ⇒ (a ⇒ b)) ⇒ ((c ⇒ a) ⇒ (c ⇒ b)))
  _∙_ : ∀{a b} (t : Tm (a ⇒ b)) (u : Tm a) → Tm b

data _↦_ : ∀{a} (t t' : Tm a) → Set where

  ↦S : ∀{c a b} {t : Tm (c ⇒ (a ⇒ b))} {u : Tm (c ⇒ a)} {v : Tm c}
     → (((S ∙ t) ∙ u) ∙ v) ↦ ((t ∙ v) ∙ (u ∙ v))

  ↦r : ∀{a b} {u u' : Tm a} {t : Tm (a ⇒ b)}
     → (t ∙ u) ↦ (t ∙ u')

data SN {a} (t : Tm a) : Set where
  acc : (h : ∀{t'} (r : t ↦ t') → SN t') → SN t

test : ∀{a b} {t : Tm (a ⇒ b)} {u : Tm a} → SN t → SN u → SN (t ∙ u)
test snt snu = acc λ{ (↦S) → ANY ; (↦r) → {!test snt ?!} }

  -- Refine with (test snt)
  -- or give (test snt ?)

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Substitute.hs:456

max_stars_repo_name: andreas-roehler/agda

max_issues_repo_name: andreas-roehler/agda

max_forks_repo_name: andreas-roehler/agda


text:
-- The error on Agda 2.5.3 was:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Substitute/Class.hs:209

open import Agda.Primitive using (_⊔_ ; Level ; lsuc)

record Unit {U : Level} : Set U where
-- error still occurs with no constructors or fields in these types
  constructor unit

record _×_ {U V : Level} (A : Set U) (B : Set V) : Set (U ⊔ V) where
  constructor _,,_
  field
    x : A
    y : B

infixr 25 _×_

data _⇔_ {U V : Level} : (A : Set U) → (B : Set V) → Set (U ⊔ V) where
  unitIL : {A : Set U} → A ⇔ A × Unit


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

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

-- This module proves the two "VotesOnce" proof obligations for our fake handler

open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.PKCS

import      LibraBFT.Concrete.Properties.VotesOnce as VO

open import LibraBFT.Impl.Consensus.Types hiding (EpochConfigFor)
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle.Properties                               sha256 sha256-cr
open import LibraBFT.Impl.Properties.Aux
open import LibraBFT.Concrete.System impl-sps-avp
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK
open        Structural impl-sps-avp
open import LibraBFT.Impl.Properties.VotesOnce

-- In this module, we (will) prove the two implementation obligations for the VotesOnce rule.  Note
-- that it is not yet 100% clear that the obligations are the best definitions to use.  See comments
-- in Concrete.VotesOnce.  We will want to prove these obligations for the fake/simple
-- implementation (or some variant on it) and streamline the proof before we proceed to tacke more
-- ambitious properties.

module LibraBFT.Impl.Properties.VotesOnceDirect where

  oldVoteRound≤lvr :  ∀ {e pid pk v}{pre : SystemState e}
                   → (r : ReachableSystemState pre)
                   → initialised pre pid ≡ initd
                   → Meta-Honest-PK pk → (sig : WithVerSig pk v)
                   → MsgWithSig∈ pk (ver-signature sig) (msgPool pre)
                   → ValidSenderForPK (availEpochs pre) v pid pk
                   → (₋epEC (peerStates pre pid)) ^∙ epEpoch ≡ (v ^∙ vEpoch)
                   → v ^∙ vRound ≤ (₋epEC (peerStates pre pid)) ^∙ epLastVotedRound
  oldVoteRound≤lvr (step-s r (step-epoch _)) pidIn pkH sig msv vspk ep≡ = {!!}
  oldVoteRound≤lvr {pid = pid'} {pre = pre} (step-s r (step-peer {pid = pid} cheat@(step-cheat f c)))
                    pidIn pkH sig msv vspk ep≡
     with ¬cheatForgeNew cheat refl unit pkH msv
  ...| msb4
     rewrite cheatStepDNMPeerStates₁ {pid = pid} {pid' = pid'} cheat unit
       = oldVoteRound≤lvr r pidIn pkH sig msb4 vspk ep≡
  oldVoteRound≤lvr {pid = pid'} {pre = pre}
                   step@(step-s r (step-peer {pid = pid} stHon@(step-honest stPeer)))
                   pidIn pkH sig msv vspk ep≡
     with newMsg⊎msgSentB4 r stHon pkH (msgSigned msv) (msg⊆ msv) (msg∈pool msv)
  ...| inj₂ msb4 rewrite msgSameSig msv
     with pid ≟ pid'
  ...| no imp = oldVoteRound≤lvr r pidIn pkH sig msb4 vspk ep≡
  ...| yes refl = let ep≡st = noEpochChangeYet r refl stPeer
                      lvr≤  = lastVoteRound-mono r refl stPeer ep≡st
                      ep≡v  = trans ep≡st ep≡
                  in ≤-trans (oldVoteRound≤lvr r pidIn pkH sig msb4 vspk ep≡v) lvr≤
  oldVoteRound≤lvr {pid = pid'} {pre = pre}
                   step@(step-s r (step-peer {pid = pid} stHon@(step-honest stPeer)))
                   pidIn pkH sig msv vspk ep≡
     | inj₁ (m∈outs , vspkN , newV)
     with sameHonestSig⇒sameVoteData pkH (msgSigned msv) sig (msgSameSig msv)
  ...| inj₁ hb = ⊥-elim (PerState.meta-sha256-cr pre step hb)
  ...| inj₂ refl
     with sameEpoch⇒sameEC vspk vspkN refl
          -- Both peers are allowed to sign for the same PK in the same epoch,
          -- so they are the same peer
  ...| refl
     with NodeId-PK-OK-injective (vp-ec vspk) (vp-sender-ok vspk) (vp-sender-ok vspkN)
  ...| refl rewrite eventProcessorPostSt r stPeer refl
       = let nvr = newVoteSameEpochGreaterRound r stPeer (msg⊆ msv) m∈outs (msgSigned msv) newV
         in ≡⇒≤ ((proj₂ ∘ proj₂) nvr)

  votesOnce₁ : VO.ImplObligation₁
  votesOnce₁ {pid' = pid'} r (step-msg {_ , P m} _ psI) {v' = v'} {m' = m'}
             pkH v⊂m (here refl) sv ¬msb vspkv v'⊂m' m'∈pool sv' ep≡ r≡
     with v⊂m
  ...| vote∈vm = let m'mwsb = mkMsgWithSig∈ m' v' v'⊂m' pid' m'∈pool sv' refl
                     vspkv' = ValidSenderForPK⇒ep≡ sv sv' ep≡ vspkv
                     rv'<rv = oldVoteRound≤lvr r psI pkH sv' m'mwsb vspkv' ep≡
                 in ⊥-elim (<⇒≢ (s≤s rv'<rv) (sym r≡))
  ...| vote∈qc vs∈qc v≈rbld (inV qc∈m) rewrite cong ₋vSignature v≈rbld
       = ⊥-elim (¬msb (qcVotesSentB4 r psI refl qc∈m refl vs∈qc))

  votesOnce₂ : VO.ImplObligation₂
  votesOnce₂ {pk = pk} {st} r (step-msg {_ , P m} _ psI) hpk v⊂m m∈outs sig vnew
             vpk v'⊂m' m'∈outs sig' v'new vpk' es≡ rnds≡
     with m∈outs | m'∈outs
  ...| here refl | here refl
     with v⊂m                          | v'⊂m'
  ...| vote∈vm                         | vote∈vm = refl
  ...| vote∈vm                         | vote∈qc vs∈qc' v≈rbld' (inV qc∈m')
       rewrite cong ₋vSignature v≈rbld'
       = ⊥-elim (v'new (qcVotesSentB4 r psI refl qc∈m' refl vs∈qc'))
  ...| vote∈qc vs∈qc v≈rbld (inV qc∈m) | _
       rewrite cong ₋vSignature v≈rbld
       = ⊥-elim (vnew (qcVotesSentB4 r psI refl qc∈m refl vs∈qc))

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
open import Data.Product using ( _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Web.Semantic.DL.ABox.Interp using ( _*_ )
open import Web.Semantic.DL.ABox.Model using ( *-resp-⟨ABox⟩ )
open import Web.Semantic.DL.Category.Object using ( Object ; iface )
open import Web.Semantic.DL.Category.Morphism using ( _⇒_ ; _≣_ ; _⊑_ ; _,_ )
open import Web.Semantic.DL.Category.Tensor using ( _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Properties.Tensor.Lemmas using
  ( tensor-up ; tensor-down ; tensor-resp-⊨b )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( inode ; up ; down )

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

tensor-resp-⊑ : ∀ {A₁ A₂ B₁ B₂ : Object S T}
  (F₁ G₁ : A₁ ⇒ B₁) (F₂ G₂ : A₂ ⇒ B₂) →
    (F₁ ⊑ G₁) → (F₂ ⊑ G₂) → (F₁ ⟨⊗⟩ F₂ ⊑ G₁ ⟨⊗⟩ G₂)
tensor-resp-⊑ {A₁} {A₂} F₁ G₁ F₂ G₂ F₁⊑G₁ F₂⊑G₂
  I (I⊨ST , (I⊨A₁ , I⊨A₂)) I⊨F₁F₂ =
    tensor-resp-⊨b G₁ G₂ I
      (F₁⊑G₁ (up * I)
        (I⊨ST , *-resp-⟨ABox⟩ inj₁ (inode * I) (iface A₁) I⊨A₁)
        (tensor-up F₁ F₂ I I⊨F₁F₂))
      (F₂⊑G₂ (down * I)
        (I⊨ST , *-resp-⟨ABox⟩ inj₂ (inode * I) (iface A₂) I⊨A₂)
        (tensor-down F₁ F₂ I I⊨F₁F₂))

tensor-resp-≣ : ∀ {A₁ A₂ B₁ B₂ : Object S T}
  {F₁ G₁ : A₁ ⇒ B₁} {F₂ G₂ : A₂ ⇒ B₂} →
    (F₁ ≣ G₁) → (F₂ ≣ G₂) → (F₁ ⟨⊗⟩ F₂ ≣ G₁ ⟨⊗⟩ G₂)
tensor-resp-≣ {A₁} {A₂} {B₁} {B₂} {F₁} {G₁} {F₂} {G₂}
  (F₁⊑G₁ , G₁⊑F₁) (F₂⊑G₂ , G₂⊑F₂) =
    ( tensor-resp-⊑ F₁ G₁ F₂ G₂ F₁⊑G₁ F₂⊑G₂
    , tensor-resp-⊑ G₁ F₁ G₂ F₂ G₁⊑F₁ G₂⊑F₂ )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Algebra.LabelledGraph where

open import Algebra.Dioid

-- Core graph construction primitives
data LabelledGraph {D eq} (d : Dioid D eq) (A : Set) : Set where
    ε   : LabelledGraph d A      -- Empty graph
    v   : A -> LabelledGraph d A -- Graph comprising a single vertex
    _[_]>_ : LabelledGraph d A -> D -> LabelledGraph d A -> LabelledGraph d A
                               -- Connect two graphs

_+_ : ∀ {A D eq} {d : Dioid D eq} -> LabelledGraph d A -> LabelledGraph d A -> LabelledGraph d A
_+_ {_} {_} {_} {d} g h = g [ Dioid.zero d ]> h

_*_ : ∀ {A D eq} {d : Dioid D eq}  -> LabelledGraph d A -> LabelledGraph d A -> LabelledGraph d A
_*_ {_} {_} {_} {d} g h = g [ Dioid.one d ]> h

infixl 4  _≡_
infixl 8  _+_
infixl 9  _*_
infixl 9  _[_]>_
infix  10 _⊆_

-- Equational theory of graphs
data _≡_ {A D eq} {d : Dioid D eq} : (x y : LabelledGraph d A) -> Set where
    -- Equivalence relation
    reflexivity  : ∀ {x     : LabelledGraph d A} ->                   x ≡ x
    symmetry     : ∀ {x y   : LabelledGraph d A} -> x ≡ y ->          y ≡ x
    transitivity : ∀ {x y z : LabelledGraph d A} -> x ≡ y -> y ≡ z -> x ≡ z

    -- Congruence
    left-congruence  : ∀ {x y z : LabelledGraph d A} {r : D} -> x ≡ y  -> x [ r ]> z ≡ y [ r ]> z
    right-congruence : ∀ {x y z : LabelledGraph d A} {r : D} -> x ≡ y  -> z [ r ]> x ≡ z [ r ]> y
    dioid-congruence : ∀ {x y : LabelledGraph d A} {r s : D} -> eq r s -> x [ r ]> y ≡ x [ s ]> y

    -- Axioms
    zero-commutativity  : ∀ {x y : LabelledGraph d A} -> x + y ≡ y + x
    left-identity       : ∀ {x     : LabelledGraph d A} {r   : D} -> ε [ r ]> x ≡ x
    right-identity      : ∀ {x     : LabelledGraph d A} {r   : D} -> x [ r ]> ε ≡ x
    left-decomposition  : ∀ {x y z : LabelledGraph d A} {r s : D} -> x [ r ]> (y [ s ]> z) ≡ (x [ r ]> y) + (x [ r ]> z) + (y [ s ]> z)
    right-decomposition : ∀ {x y z : LabelledGraph d A} {r s : D} -> (x [ r ]> y) [ s ]> z ≡ (x [ r ]> y) + (x [ s ]> z) + (y [ s ]> z)
    label-addition      : ∀ {x y   : LabelledGraph d A} {r s : D} -> (x [ r ]> y) + (x [ s ]> y) ≡ (x [ Dioid.plus d r s ]> y)

-- Subgraph relation
_⊆_ : ∀ {A D eq} {d : Dioid D eq} -> LabelledGraph d A -> LabelledGraph d A -> Set
x ⊆ y = x + y ≡ y

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs