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

module Fmmh where

open import Data.List using (List)

open import Pitch

-- Reconstruction of "Functional Modelling of Musical Harmony" (ICFP 2011)
-- using similar notation. Original code:
-- https://github.com/chordify/HarmTrace-Base

data Mode : Set where
  maj : Mode
  min : Mode

data ChordQuality : Set where
  maj  : ChordQuality
  min  : ChordQuality
  dom7 : ChordQuality
  dim  : ChordQuality

data Chord : DiatonicDegree → ChordQuality → Set where
  chord : (d : DiatonicDegree) → (q : ChordQuality) → Chord d q

data Ton : Mode → Set where
  maj : Chord d1 maj → Ton maj
  min : Chord d1 min → Ton min

data SDom : Mode → Set where
  ii     : Chord d2 min → SDom maj
  iv-maj : Chord d4 maj → SDom maj
  iii-iv : Chord d3 min → Chord d4 maj → SDom maj
  iv-min : Chord d4 min → SDom min

data Dom (m : Mode) : Set where
  v7   : Chord d5 dom7 → Dom m
  v    : Chord d5 maj → Dom m
  vii  : Chord d7 dim → Dom m
  sdom : SDom m → Dom m → Dom m
  ii-v : Chord d2 dom7 → Chord d5 dom7 → Dom m

data Phrase (m : Mode) : Set where
  i-v-i : Ton m → Dom m → Ton m → Phrase m
  v-i   : Dom m → Ton m → Phrase m

data Piece : Set where
  piece : {m : Mode} → List (Phrase m) → Piece

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module muRec where

open import Data.Nat
open import Data.Sum
open import Relation.Binary.PropositionalEquality as PE
open import PropsAsTypes

mutual
  record D (A : Set) : Set where
    coinductive
    field
      step : Dμ A

  data Dμ (A : Set) : Set where
    now   : A   → Dμ A
    later : D A → Dμ A

open D public

coiter-D : {A X : Set} → (X → A ⊎ X) → X → D A
coiter-D c x .step with c x
... | inj₁ a  = now a
... | inj₂ x' = later (coiter-D c x')

compute-D₁ : {A X : Set} (c : X → A ⊎ X) (x : X) →
            ∀ a → c x ≡ inj₁ a → coiter-D c x .step ≡ now a
compute-D₁ c x a p with c x
compute-D₁ c x .a refl | inj₁ a = refl
compute-D₁ c x  a ()   | inj₂ y

compute-D₂ : {A X : Set} (c : X → A ⊎ X) (x : X) →
             ∀ x' → c x ≡ inj₂ x' →
                    coiter-D c x .step ≡ later (coiter-D c x')
compute-D₂ c x x' p with c x
compute-D₂ c x  x' ()   | inj₁ a
compute-D₂ c x .x' refl | inj₂ x' = refl

compute-D-inv₁ : {A X : Set} (c : X → A ⊎ X) (x : X) →
                 ∀ a → coiter-D c x .step ≡ now a → c x ≡ inj₁ a
compute-D-inv₁ c x a p with c x
compute-D-inv₁ c x .a refl | inj₁ a = refl
compute-D-inv₁ c x  a ()   | inj₂ y

compute-D-inv₂ : {A X : Set} (c : X → A ⊎ X) (x : X) →
                 ∀ x' → c x ≡ inj₂ x' →
                        coiter-D c x .step ≡ later (coiter-D c x')
compute-D-inv₂ c x x' p with c x
compute-D-inv₂ c x  x' ()   | inj₁ a
compute-D-inv₂ c x .x' refl | inj₂ x' = refl

ifIsZero_then_else_ : {A : Set} → ℕ → A → A → A
ifIsZero zero    then x else y = x
ifIsZero (suc _) then x else y = y

isZeroProof : ∀{m n k : ℕ} →
              ifIsZero m then inj₁ n else inj₂ k ≡ inj₁ n →
              m ≡ 0
isZeroProof {zero}  p = refl
isZeroProof {suc m} ()

μ-rec'-coalg : (ℕ → ℕ) → ℕ → ℕ ⊎ ℕ
μ-rec'-coalg f n = ifIsZero f n then inj₁ n else inj₂ (suc n)

μ-rec' : (ℕ → ℕ) → ℕ → D ℕ
μ-rec' f = coiter-D (μ-rec'-coalg f)

μ-rec : (ℕ → ℕ) → D ℕ
μ-rec f = μ-rec' f 0

data _↓_ {A : Set} (d : D A) (a : A) : Prop where
  stopped :              d .step ≡ now a             → d ↓ a
  delayed : {d' : D A} → d .step ≡ later d' → d' ↓ a → d ↓ a

μ-rec'-coalg-correct : (f : ℕ → ℕ) (n : ℕ) → μ-rec'-coalg f n ≡ inj₁ n → f n ≡ 0
μ-rec'-coalg-correct f n p = isZeroProof p

μ-rec'-correct : (f : ℕ → ℕ) (m n : ℕ) → (μ-rec' f m ↓ n) → f (m + n) ≡ 0
μ-rec'-correct f m n (stopped p) =
  let q = compute-D-inv₁ (μ-rec'-coalg f) m n p
  in {!!}
μ-rec'-correct f m n (delayed d' p) = {!!}

μ-rec-correct : (f : ℕ → ℕ) (n : ℕ) → (μ-rec f ↓ n) → f n ≡ 0
μ-rec-correct f n (stopped p) =
  let q = compute-D-inv₁ (μ-rec'-coalg f) 0 n p
  in μ-rec'-coalg-correct f n {!!}
μ-rec-correct f n (delayed d' p) = {!!}

ext: agda

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

module Cubical.Algebra.CommAlgebra.Instances.FreeCommAlgebra where
{-
  The free commutative algebra over a commutative ring,
  or in other words the ring of polynomials with coefficients in a given ring.
  Note that this is a constructive definition, which entails that polynomials
  cannot be represented by lists of coefficients, where the last one is non-zero.
  For rings with decidable equality, that is still possible.

  I learned about this (and other) definition(s) from David Jaz Myers.
  You can watch him talk about these things here:
  https://www.youtube.com/watch?v=VNp-f_9MnVk

  This file contains
  * the definition of the free commutative algebra on a type I over a commutative ring R as a HIT
    (let us call that R[I])
  * a prove that the construction is an commutative R-algebra
  * definitions of the induced maps appearing in the universal property of R[I],
    that is:  * for any map I → A, where A is a commutative R-algebra,
                the induced algebra homomorphism R[I] → A
                ('inducedHom')
              * for any hom R[I] → A, the 'restricttion to variables' I → A
                ('evaluateAt')
  * a proof that the two constructions are inverse to each other
    ('homRetrievable' and 'mapRetrievable')
  * a proof, that the corresponding pointwise equivalence of functors is natural
    ('naturalR', 'naturalL')
-}
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function hiding (const)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring        using ()
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.Algebra
open import Cubical.HITs.SetTruncation

private
  variable
    ℓ ℓ' ℓ'' : Level

module Construction (R : CommRing ℓ) where
  open CommRingStr (snd R) using (1r; 0r) renaming (_+_ to _+r_; _·_ to _·r_)

  data R[_] (I : Type ℓ') : Type (ℓ-max ℓ ℓ') where
    var : I → R[ I ]
    const : ⟨ R ⟩ → R[ I ]
    _+_ : R[ I ] → R[ I ] → R[ I ]
    -_ : R[ I ] → R[ I ]
    _·_ : R[ I ] → R[ I ] → R[ I ]            -- \cdot

    +-assoc : (x y z : R[ I ]) → x + (y + z) ≡ (x + y) + z
    +-rid : (x : R[ I ]) → x + (const 0r) ≡ x
    +-rinv : (x : R[ I ]) → x + (- x) ≡ (const 0r)
    +-comm : (x y : R[ I ]) → x + y ≡ y + x

    ·-assoc : (x y z : R[ I ]) → x · (y · z) ≡ (x · y) · z
    ·-lid : (x : R[ I ]) → (const 1r) · x ≡ x
    ·-comm : (x y : R[ I ]) → x · y ≡ y · x

    ldist : (x y z : R[ I ]) → (x + y) · z ≡ (x · z) + (y · z)

    +HomConst : (s t : ⟨ R ⟩) → const (s +r t) ≡ const s + const t
    ·HomConst : (s t : ⟨ R ⟩) → const (s ·r t) ≡ (const s) · (const t)

    0-trunc : (x y : R[ I ]) (p q : x ≡ y) → p ≡ q

  _⋆_ : {I : Type ℓ'} → ⟨ R ⟩ → R[ I ] → R[ I ]
  r ⋆ x = const r · x

  ⋆-assoc : {I : Type ℓ'} → (s t : ⟨ R ⟩) (x : R[ I ]) → (s ·r t) ⋆ x ≡ s ⋆ (t ⋆ x)
  ⋆-assoc s t x = const (s ·r t) · x       ≡⟨ cong (λ u → u · x) (·HomConst _ _) ⟩
                  (const s · const t) · x  ≡⟨ sym (·-assoc _ _ _) ⟩
                  const s · (const t · x)  ≡⟨ refl ⟩
                  s ⋆ (t ⋆ x) ∎

  ⋆-ldist-+ : {I : Type ℓ'} → (s t : ⟨ R ⟩) (x : R[ I ]) → (s +r t) ⋆ x ≡ (s ⋆ x) + (t ⋆ x)
  ⋆-ldist-+ s t x = (s +r t) ⋆ x             ≡⟨ cong (λ u → u · x) (+HomConst _ _) ⟩
                    (const s + const t) · x  ≡⟨ ldist _ _ _ ⟩
                    (s ⋆ x) + (t ⋆ x) ∎

  ⋆-rdist-+ : {I : Type ℓ'} → (s : ⟨ R ⟩) (x y : R[ I ]) → s ⋆ (x + y) ≡ (s ⋆ x) + (s ⋆ y)
  ⋆-rdist-+ s x y = const s · (x + y)             ≡⟨ ·-comm _ _ ⟩
                    (x + y) · const s             ≡⟨ ldist _ _ _ ⟩
                    (x · const s) + (y · const s) ≡⟨ cong (λ u → u + (y · const s)) (·-comm _ _) ⟩
                    (s ⋆ x) + (y · const s)       ≡⟨ cong (λ u → (s ⋆ x) + u) (·-comm _ _)  ⟩
                    (s ⋆ x) + (s ⋆ y) ∎

  ⋆-assoc-· : {I : Type ℓ'} → (s : ⟨ R ⟩) (x y : R[ I ]) → (s ⋆ x) · y ≡ s ⋆ (x · y)
  ⋆-assoc-· s x y = (s ⋆ x) · y ≡⟨ sym (·-assoc _ _ _) ⟩
                    s ⋆ (x · y) ∎

  0a : {I : Type ℓ'} → R[ I ]
  0a = (const 0r)

  1a : {I : Type ℓ'} → R[ I ]
  1a = (const 1r)

  isCommAlgebra : {I : Type ℓ'} → IsCommAlgebra R {A = R[ I ]} 0a 1a _+_ _·_ -_ _⋆_
  isCommAlgebra = makeIsCommAlgebra 0-trunc
                                    +-assoc +-rid +-rinv +-comm
                                    ·-assoc ·-lid ldist ·-comm
                                    ⋆-assoc ⋆-ldist-+ ⋆-rdist-+ ·-lid ⋆-assoc-·

_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
(R [ I ]) = R[ I ] , commalgebrastr 0a 1a _+_ _·_ -_ _⋆_ isCommAlgebra
  where
  open Construction R

module Theory {R : CommRing ℓ} {I : Type ℓ'} where
  open CommRingStr (snd R)
         using (0r; 1r)
         renaming (_·_ to _·r_; _+_ to _+r_; ·Comm to ·r-comm; ·Rid to ·r-rid)

  module _ (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩) where
    open CommAlgebraStr (A .snd)
    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)

    imageOf0Works : 0r ⋆ 1a ≡ 0a
    imageOf0Works = 0-actsNullifying 1a

    imageOf1Works : 1r ⋆ 1a ≡ 1a
    imageOf1Works = ⋆-lid 1a

    inducedMap : ⟨ R [ I ] ⟩ → ⟨ A ⟩
    inducedMap (var x) = φ x
    inducedMap (const r) = r ⋆ 1a
    inducedMap (P +c Q) = (inducedMap P) + (inducedMap Q)
    inducedMap (-c P) = - inducedMap P
    inducedMap (Construction.+-assoc P Q S i) = +-assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
    inducedMap (Construction.+-rid P i) =
      let
        eq : (inducedMap P) + (inducedMap (const 0r)) ≡ (inducedMap P)
        eq = (inducedMap P) + (inducedMap (const 0r)) ≡⟨ refl ⟩
             (inducedMap P) + (0r ⋆ 1a)               ≡⟨ cong
                                                         (λ u → (inducedMap P) + u)
                                                         (imageOf0Works) ⟩
             (inducedMap P) + 0a                      ≡⟨ +-rid _ ⟩
             (inducedMap P) ∎
      in eq i
    inducedMap (Construction.+-rinv P i) =
      let eq : (inducedMap P - inducedMap P) ≡ (inducedMap (const 0r))
          eq = (inducedMap P - inducedMap P) ≡⟨ +-rinv _ ⟩
               0a                            ≡⟨ sym imageOf0Works ⟩
               (inducedMap (const 0r))∎
      in eq i
    inducedMap (Construction.+-comm P Q i) = +-comm (inducedMap P) (inducedMap Q) i
    inducedMap (P ·c Q) = inducedMap P · inducedMap Q
    inducedMap (Construction.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
    inducedMap (Construction.·-lid P i) =
      let eq = inducedMap (const 1r) · inducedMap P ≡⟨ cong (λ u → u · inducedMap P) imageOf1Works ⟩
               1a · inducedMap P                    ≡⟨ ·Lid (inducedMap P) ⟩
               inducedMap P ∎
      in eq i
    inducedMap (Construction.·-comm P Q i) = ·-comm (inducedMap P) (inducedMap Q) i
    inducedMap (Construction.ldist P Q S i) = ·Ldist+ (inducedMap P) (inducedMap Q) (inducedMap S) i
    inducedMap (Construction.+HomConst s t i) = ⋆-ldist s t 1a i
    inducedMap (Construction.·HomConst s t i) =
      let eq = (s ·r t) ⋆ 1a       ≡⟨ cong (λ u → u ⋆ 1a) (·r-comm _ _) ⟩
               (t ·r s) ⋆ 1a       ≡⟨ ⋆-assoc t s 1a ⟩
               t ⋆ (s ⋆ 1a)        ≡⟨ cong (λ u → t ⋆ u) (sym (·Rid _)) ⟩
               t ⋆ ((s ⋆ 1a) · 1a) ≡⟨ ⋆-rassoc t (s ⋆ 1a) 1a ⟩
               (s ⋆ 1a) · (t ⋆ 1a) ∎
      in eq i
    inducedMap (Construction.0-trunc P Q p q i j) =
      isSetAlgebra (CommAlgebra→Algebra A) (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j

    module _ where
      open IsAlgebraHom

      inducedHom : AlgebraHom (CommAlgebra→Algebra (R [ I ])) (CommAlgebra→Algebra A)
      inducedHom .fst = inducedMap
      inducedHom .snd .pres0 = 0-actsNullifying _
      inducedHom .snd .pres1 = imageOf1Works
      inducedHom .snd .pres+ x y = refl
      inducedHom .snd .pres· x y = refl
      inducedHom .snd .pres- x = refl
      inducedHom .snd .pres⋆ r x =
        (r ⋆ 1a) · inducedMap x ≡⟨ ⋆-lassoc r 1a (inducedMap x) ⟩
        r ⋆ (1a · inducedMap x) ≡⟨ cong (λ u → r ⋆ u) (·Lid (inducedMap x)) ⟩
        r ⋆ inducedMap x ∎

  module _ (A : CommAlgebra R ℓ'') where
    open CommAlgebraStr (A .snd)
    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)

    Hom = AlgebraHom (CommAlgebra→Algebra (R [ I ])) (CommAlgebra→Algebra A)
    open IsAlgebraHom

    evaluateAt : Hom → I → ⟨ A ⟩
    evaluateAt φ x = φ .fst (var x)

    mapRetrievable : ∀ (φ : I → ⟨ A ⟩)
                     → evaluateAt (inducedHom A φ) ≡ φ
    mapRetrievable φ = refl

    proveEq : ∀ {X : Type ℓ''} (isSetX : isSet X) (f g : ⟨ R [ I ] ⟩ → X)
              → (var-eq : (x : I) → f (var x) ≡ g (var x))
              → (const-eq : (r : ⟨ R ⟩) → f (const r) ≡ g (const r))
              → (+-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
                        → f (x +c y) ≡ g (x +c y))
              → (·-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
                        → f (x ·c y) ≡ g (x ·c y))
              → (-eq : (x : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x)
                        → f (-c x) ≡ g (-c x))
              → f ≡ g
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (var x) = var-eq x i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (const x) = const-eq x i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x +c y) =
      +-eq x y
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
           i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (-c x) =
      -eq x ((λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)) i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x ·c y) =
      ·-eq x y
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
           i
    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-assoc x y z j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c (y +c z)) ≡ g (x +c (y +c z))
        a₀₋ = +-eq _ _ (rec x) (+-eq _ _ (rec y) (rec z))
        a₁₋ : f ((x +c y) +c z) ≡ g ((x +c y) +c z)
        a₁₋ = +-eq _ _ (+-eq _ _ (rec x) (rec y)) (rec z)
        a₋₀ : f (x +c (y +c z)) ≡ f ((x +c y) +c z)
        a₋₀ = cong f (Construction.+-assoc x y z)
        a₋₁ : g (x +c (y +c z)) ≡ g ((x +c y) +c z)
        a₋₁ = cong g (Construction.+-assoc x y z)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rid x j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c (const 0r)) ≡ g (x +c (const 0r))
        a₀₋ = +-eq _ _ (rec x) (const-eq 0r)
        a₁₋ : f x ≡ g x
        a₁₋ = rec x
        a₋₀ : f (x +c (const 0r)) ≡ f x
        a₋₀ = cong f (Construction.+-rid x)
        a₋₁ : g (x +c (const 0r)) ≡ g x
        a₋₁ = cong g (Construction.+-rid x)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rinv x j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c (-c x)) ≡ g (x +c (-c x))
        a₀₋ = +-eq x (-c x) (rec x) (-eq x (rec x))
        a₁₋ : f (const 0r) ≡ g (const 0r)
        a₁₋ = const-eq 0r
        a₋₀ : f (x +c (-c x)) ≡ f (const 0r)
        a₋₀ = cong f (Construction.+-rinv x)
        a₋₁ : g (x +c (-c x)) ≡ g (const 0r)
        a₋₁ = cong g (Construction.+-rinv x)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-comm x y j) =
      let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x +c y) ≡ g (x +c y)
        a₀₋ = +-eq x y (rec x) (rec y)
        a₁₋ : f (y +c x) ≡ g (y +c x)
        a₁₋ = +-eq y x (rec y) (rec x)
        a₋₀ : f (x +c y) ≡ f (y +c x)
        a₋₀ = cong f (Construction.+-comm x y)
        a₋₁ : g (x +c y) ≡ g (y +c x)
        a₋₁ = cong g (Construction.+-comm x y)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-assoc x y z j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x ·c (y ·c z)) ≡ g (x ·c (y ·c z))
        a₀₋ = ·-eq _ _ (rec x) (·-eq _ _ (rec y) (rec z))
        a₁₋ : f ((x ·c y) ·c z) ≡ g ((x ·c y) ·c z)
        a₁₋ = ·-eq _ _ (·-eq _ _ (rec x) (rec y)) (rec z)
        a₋₀ : f (x ·c (y ·c z)) ≡ f ((x ·c y) ·c z)
        a₋₀ = cong f (Construction.·-assoc x y z)
        a₋₁ : g (x ·c (y ·c z)) ≡ g ((x ·c y) ·c z)
        a₋₁ = cong g (Construction.·-assoc x y z)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-lid x j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f ((const 1r) ·c x) ≡ g ((const 1r) ·c x)
        a₀₋ = ·-eq _ _ (const-eq 1r) (rec x)
        a₁₋ : f x ≡ g x
        a₁₋ = rec x
        a₋₀ : f ((const 1r) ·c x) ≡ f x
        a₋₀ = cong f (Construction.·-lid x)
        a₋₁ : g ((const 1r) ·c x) ≡ g x
        a₋₁ = cong g (Construction.·-lid x)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-comm x y j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (x ·c y) ≡ g (x ·c y)
        a₀₋ = ·-eq _ _ (rec x) (rec y)
        a₁₋ : f (y ·c x) ≡ g (y ·c x)
        a₁₋ = ·-eq _ _ (rec y) (rec x)
        a₋₀ : f (x ·c y) ≡ f (y ·c x)
        a₋₀ = cong f (Construction.·-comm x y)
        a₋₁ : g (x ·c y) ≡ g (y ·c x)
        a₋₁ = cong g (Construction.·-comm x y)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.ldist x y z j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f ((x +c y) ·c z) ≡ g ((x +c y) ·c z)
        a₀₋ = ·-eq (x +c y) z
           (+-eq _ _ (rec x) (rec y))
           (rec z)
        a₁₋ : f ((x ·c z) +c (y ·c z)) ≡ g ((x ·c z) +c (y ·c z))
        a₁₋ = +-eq _ _ (·-eq _ _ (rec x) (rec z)) (·-eq _ _ (rec y) (rec z))
        a₋₀ : f ((x +c y) ·c z) ≡ f ((x ·c z) +c (y ·c z))
        a₋₀ = cong f (Construction.ldist x y z)
        a₋₁ : g ((x +c y) ·c z) ≡ g ((x ·c z) +c (y ·c z))
        a₋₁ = cong g (Construction.ldist x y z)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+HomConst s t j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (const (s +r t)) ≡ g (const (s +r t))
        a₀₋ = const-eq (s +r t)
        a₁₋ : f (const s +c const t) ≡ g (const s +c const t)
        a₁₋ = +-eq _ _ (const-eq s) (const-eq t)
        a₋₀ : f (const (s +r t)) ≡ f (const s +c const t)
        a₋₀ = cong f (Construction.+HomConst s t)
        a₋₁ : g (const (s +r t)) ≡ g (const s +c const t)
        a₋₁ = cong g (Construction.+HomConst s t)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·HomConst s t j) =
       let
        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
        a₀₋ : f (const (s ·r t)) ≡ g (const (s ·r t))
        a₀₋ = const-eq (s ·r t)
        a₁₋ : f (const s ·c const t) ≡ g (const s ·c const t)
        a₁₋ = ·-eq _ _ (const-eq s) (const-eq t)
        a₋₀ : f (const (s ·r t)) ≡ f (const s ·c const t)
        a₋₀ = cong f (Construction.·HomConst s t)
        a₋₁ : g (const (s ·r t)) ≡ g (const s ·c const t)
        a₋₁ = cong g (Construction.·HomConst s t)
      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i

    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.0-trunc x y p q j k) =
      let
        P : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        P x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
        Q : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
        Q x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
      in isOfHLevel→isOfHLevelDep 2
           (λ z → isProp→isSet (isSetX (f z) (g z))) _ _
           (cong P p)
           (cong Q q)
           (Construction.0-trunc x y p q) j k i

    homRetrievable : ∀ (f : Hom)
                     → inducedMap A (evaluateAt f) ≡ fst f
    homRetrievable f =
       proveEq
        (isSetAlgebra (CommAlgebra→Algebra A))
        (inducedMap A (evaluateAt f))
        (λ x → f $a x)
        (λ x → refl)
        (λ r → r ⋆ 1a                     ≡⟨ cong (λ u → r ⋆ u) (sym f.pres1) ⟩
               r ⋆ (f $a (const 1r))      ≡⟨ sym (f.pres⋆ r _) ⟩
               f $a (const r ·c const 1r) ≡⟨ cong (λ u → f $a u) (sym (Construction.·HomConst r 1r)) ⟩
               f $a (const (r ·r 1r))     ≡⟨ cong (λ u → f $a (const u)) (·r-rid r) ⟩
               f $a (const r) ∎)

        (λ x y eq-x eq-y →
              ι (x +c y)            ≡⟨ refl ⟩
              (ι x + ι y)           ≡⟨ cong (λ u → u + ι y) eq-x ⟩
              ((f $a x) + ι y)      ≡⟨
                                     cong (λ u → (f $a x) + u) eq-y ⟩
              ((f $a x) + (f $a y)) ≡⟨ sym (f.pres+ _ _) ⟩ (f $a (x +c y)) ∎)

        (λ x y eq-x eq-y →
           ι (x ·c y)          ≡⟨ refl ⟩
           ι x     · ι y       ≡⟨ cong (λ u → u · ι y) eq-x ⟩
           (f $a x) · (ι y)    ≡⟨ cong (λ u → (f $a x) · u) eq-y ⟩
           (f $a x) · (f $a y) ≡⟨ sym (f.pres· _ _) ⟩
           f $a (x ·c y) ∎)
       (λ x eq-x →
           ι (-c x)    ≡⟨ refl ⟩
           - ι x       ≡⟨ cong (λ u → - u) eq-x ⟩
           - (f $a x)  ≡⟨ sym (f.pres- x) ⟩
           f $a (-c x) ∎)
      where
      ι = inducedMap A (evaluateAt f)
      module f = IsAlgebraHom (f .snd)

evaluateAt : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
             (f : AlgebraHom (CommAlgebra→Algebra (R [ I ])) (CommAlgebra→Algebra A))
             → (I → ⟨ A ⟩)
evaluateAt A f x = f $a (Construction.var x)

inducedHom : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
             (φ : I → ⟨ A ⟩)
             → AlgebraHom (CommAlgebra→Algebra (R [ I ])) (CommAlgebra→Algebra A)
inducedHom A φ = Theory.inducedHom A φ

module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
  A′ = CommAlgebra→Algebra A
  B′ = CommAlgebra→Algebra B
  R′ = (CommRing→Ring R)
  ν : AlgebraHom A′ B′ → (⟨ A ⟩ → ⟨ B ⟩)
  ν φ = φ .fst

  {-
    Hom(R[I],A) → (I → A)
         ↓          ↓
    Hom(R[I],B) → (I → B)
  -}
  naturalR : {I : Type ℓ'} (ψ : AlgebraHom A′ B′)
             (f : AlgebraHom (CommAlgebra→Algebra (R [ I ])) A′)
             → (ν ψ) ∘ evaluateAt A f ≡ evaluateAt B (ψ ∘a f)
  naturalR ψ f = refl

  {-
    Hom(R[I],A) → (I → A)
         ↓          ↓
    Hom(R[J],A) → (J → A)
  -}
  naturalL : {I J : Type ℓ'} (φ : J → I)
             (f : AlgebraHom (CommAlgebra→Algebra (R [ I ])) A′)
             → (evaluateAt A f) ∘ φ
               ≡ evaluateAt A (f ∘a (inducedHom (R [ I ]) (λ x → Construction.var (φ x))))
  naturalL φ f = refl


text:
module Imports.Issue5357-B where
import Imports.Issue5357-D

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection-based solver for monoid equalities
------------------------------------------------------------------------
--
-- This solver automates the construction of proofs of equivalences
-- between monoid expressions.
-- When called like so:
--
--   proof : ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z) ∙ ε
--   proof x y z = solve mon
--
-- The following diagram describes what happens under the hood:
--
--            ┌▸x ∙ (y ∙ (z ∙ ε)) ════ x ∙ (y ∙ (z ∙ ε))◂┐
--            │         ║                      ║         │
--            │         ║                      ║         │
--          [_⇓]        ║                      ║        [_⇓]
--          ╱           ║                      ║          ╲
--         ╱            ║                      ║           ╲
-- (x ∙′ y) ∙′ z      homo                   homo    x ∙′ (y ∙′ z) ∙′ ε′
--   ▴     ╲            ║                      ║           ╱       ▴
--   │      ╲           ║                      ║          ╱        │
--   │       [_↓]       ║                      ║        [_↓]       │
--   │        │         ║                      ║         │         │
--   │        │         ║                      ║         │         │
--   │        └───▸(x ∙ y) ∙ z          x ∙ (y ∙ z) ∙ ε◂─┘         │
--   │                  │                      │                   │
--   │                  │                      │                   │
--   └────reflection────┘                      └───reflection──────┘
--
-- The actual output—the proof constructed by the solver—is represented
-- by the double-lined path (══).
--
-- We start at the bottom, with our two expressions.
-- Through reflection, we convert these two expressions to their AST
-- representations, in the Expr type.
-- We then can evaluate the AST in two ways: one simply gives us back
-- the two expressions we put in ([_↓]), and the other normalises
-- ([_⇓]).
-- We use the homo function to prove equivalence between these two
-- forms: joining up these two proofs gives us the desired overall
-- proof.

-- Note: What's going on with the Monoid parameter?
--
-- This module is not parameterised over a monoid, which is contrary
-- to what you might expect. Instead, we take the monoid record as an
-- argument to the solve macro, and then pass it around as an
-- argument wherever we need it.
--
-- We need to get the monoid record at the call site, not the import
-- site, to ensure that it's consistent with the rest of the context.
-- For instance, if we wanted to produce `x ∙ y` using the monoid record
-- as imported, we would run into problems:
-- * If we tried to just reflect on the expression itself
--   (quoteTerm (x ∙ y)) we would likely get some de Bruijn indices
--   wrong (in x and y), and ∙ might not even be in scope where the
--   user wants us to solve! If they're solving an expression like
--   x + (y + z), they can pass in the +-0-monoid, but don't have to
--   open it themselves.
-- * If instead we tried to construct a term which accesses the _∙_
--   field on the reflection of the record, we'd run into similar
--   problems again. While the record is a parameter for us, it might
--   not be for the user.
-- Basically, we need the Monoid we're looking at to be exactly the
-- same as the one the user is looking at, and in order to do that we
-- quote it at the call site.

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

module Tactic.MonoidSolver where

open import Algebra
open import Function

open import Data.Bool    as Bool    using (Bool; _∨_; if_then_else_)
open import Data.Maybe   as Maybe   using (Maybe; just; nothing; maybe)
open import Data.List    as List    using (List; _∷_; [])
open import Data.Nat     as ℕ       using (ℕ; suc; zero)
open import Data.Product as Product using (_×_; _,_)

open import Agda.Builtin.Reflection
open import Reflection.Argument
open import Reflection.Term using (getName; _⋯⟅∷⟆_)
open import Reflection.TypeChecking.MonadSyntax

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

----------------------------------------------------------------------
-- The Expr type with homomorphism proofs
----------------------------------------------------------------------

infixl 7 _∙′_
data Expr {a} (A : Set a) : Set a where
  _∙′_  : Expr A → Expr A → Expr A
  ε′    : Expr A
  [_↑]  : A → Expr A

module _ {m₁ m₂} (monoid : Monoid m₁ m₂) where

  open Monoid monoid
  open SetoidReasoning setoid

  -- Convert the AST to an expression (i.e. evaluate it) without
  -- normalising.
  [_↓] : Expr Carrier → Carrier
  [ x ∙′ y  ↓] = [ x ↓] ∙ [ y ↓]
  [ ε′      ↓] = ε
  [ [ x ↑]  ↓] = x

  -- Convert an AST to an expression (i.e. evaluate it) while
  -- normalising.
  --
  -- This first function actually converts an AST to the Cayley
  -- representation of the underlying monoid.
  -- This obeys the monoid laws up to beta-eta equality, which is the
  -- property which gives us the "normalising" behaviour we want.
  [_⇓]′ : Expr Carrier → Carrier → Carrier
  [ x ∙′ y  ⇓]′ z = [ x ⇓]′ ([ y ⇓]′ z)
  [ ε′      ⇓]′ y = y
  [ [ x ↑]  ⇓]′ y = x ∙ y

  [_⇓] : Expr Carrier → Carrier
  [ x ⇓] = [ x ⇓]′ ε

  homo′ : ∀ x y → [ x ⇓] ∙ y ≈ [ x ⇓]′ y
  homo′ ε′ y       = identityˡ y
  homo′ [ x ↑] y   = ∙-congʳ (identityʳ x)
  homo′ (x ∙′ y) z = begin
    [ x ∙′ y ⇓] ∙ z       ≡⟨⟩
    [ x ⇓]′ [ y ⇓] ∙ z    ≈˘⟨ ∙-congʳ (homo′ x [ y ⇓]) ⟩
    ([ x ⇓] ∙ [ y ⇓]) ∙ z ≈⟨ assoc [ x ⇓] [ y ⇓] z ⟩
    [ x ⇓] ∙ ([ y ⇓] ∙ z) ≈⟨ ∙-congˡ (homo′ y z) ⟩
    [ x ⇓] ∙ ([ y ⇓]′ z)  ≈⟨ homo′ x ([ y ⇓]′ z) ⟩
    [ x ⇓]′ ([ y ⇓]′ z)   ∎

  homo : ∀ x → [ x ⇓] ≈ [ x ↓]
  homo ε′       = refl
  homo [ x ↑]   = identityʳ x
  homo (x ∙′ y) = begin
    [ x ∙′ y ⇓]     ≡⟨⟩
    [ x ⇓]′ [ y ⇓]  ≈˘⟨ homo′ x [ y ⇓] ⟩
    [ x ⇓] ∙ [ y ⇓] ≈⟨ ∙-cong (homo x) (homo y) ⟩
    [ x ↓] ∙ [ y ↓] ∎

----------------------------------------------------------------------
-- Helpers for reflection
----------------------------------------------------------------------

_==_ = primQNameEquality
{-# INLINE _==_ #-}

getArgs : Term → Maybe (Term × Term)
getArgs (def _ xs) = go xs
  where
  go : List (Arg Term) → Maybe (Term × Term)
  go (vArg x ∷ vArg y ∷ []) = just (x , y)
  go (x ∷ xs)               = go xs
  go _                      = nothing
getArgs _ = nothing

----------------------------------------------------------------------
-- Getting monoid names
----------------------------------------------------------------------

-- We try to be flexible here, by matching two kinds of names.
-- The first is the field accessor for the monoid record itself.
-- However, users will likely want to use the solver with
-- expressions like:
--
--   xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
--
-- So we also evaluate the field accessor to find functions like ++.

record MonoidNames : Set where
  field
    is-∙ : Name → Bool
    is-ε : Name → Bool

buildMatcher : Name → Maybe Name → Name → Bool
buildMatcher n nothing  x = n == x
buildMatcher n (just m) x = n == x ∨ m == x

findMonoidNames : Term → TC MonoidNames
findMonoidNames mon = do
  ∙-altName ← normalise (def (quote Monoid._∙_) (2 ⋯⟅∷⟆ mon ⟨∷⟩ []))
  ε-altName ← normalise (def (quote Monoid.ε)   (2 ⋯⟅∷⟆ mon ⟨∷⟩ []))
  returnTC record
    { is-∙ = buildMatcher (quote Monoid._∙_) (getName ∙-altName)
    ; is-ε = buildMatcher (quote Monoid.ε)   (getName ε-altName)
    }

----------------------------------------------------------------------
-- Building Expr
----------------------------------------------------------------------

-- We now define a function that takes an AST representing the LHS
-- or RHS of the equation to solve and converts it into an AST
-- respresenting the corresponding Expr.

″ε″ : Term
″ε″ = quote ε′ ⟨ con ⟩ []

[_↑]′ : Term → Term
[ t ↑]′ = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])

module _ (names : MonoidNames) where

 open MonoidNames names

 mutual
  ″∙″ : List (Arg Term) → Term
  ″∙″ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _∙′_ ⟨ con ⟩ buildExpr x ⟨∷⟩ buildExpr y ⟨∷⟩ []
  ″∙″ (x ∷ xs)         = ″∙″ xs
  ″∙″ _                = unknown

  buildExpr : Term → Term
  buildExpr t@(def n xs) =
    if is-∙ n
      then ″∙″ xs
    else if is-ε n
      then ″ε″
    else
      [ t ↑]′
  buildExpr t@(con n xs) =
    if is-∙ n
      then ″∙″ xs
    else if is-ε n
      then ″ε″
    else [ t ↑]′
  buildExpr t = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])

----------------------------------------------------------------------
-- Constructing the solution
----------------------------------------------------------------------

-- This function joins up the two homomorphism proofs. It constructs
-- a proof of the following form:
--
--   trans (sym (homo x)) (homo y)
--
-- where x and y are the Expr representations of each side of the
-- goal equation.

constructSoln : Term → MonoidNames → Term → Term → Term
constructSoln mon names lhs rhs =
  quote Monoid.trans ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
    (quote Monoid.sym ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
       (quote homo ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ buildExpr names lhs ⟨∷⟩ []) ⟨∷⟩ [])
    ⟨∷⟩
    (quote homo ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ buildExpr names rhs ⟨∷⟩ []) ⟨∷⟩
    []

----------------------------------------------------------------------
-- Macro
----------------------------------------------------------------------

solve-macro : Term → Term → TC _
solve-macro mon hole = do
  hole′ ← inferType hole >>= normalise
  names ← findMonoidNames mon
  just (lhs , rhs) ← returnTC (getArgs hole′)
    where nothing → typeError (termErr hole′ ∷ [])
  let soln = constructSoln mon names lhs rhs
  unify hole soln

macro
  solve : Term → Term → TC _
  solve = solve-macro


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SmashProduct where

open import Cubical.HITs.SmashProduct.Base public

-- open import Cubical.HITs.SmashProduct.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Categories.Category
open import Categories.Functor

-- Street fibration, which is the version of fibration that respects the principle of equivalence.
-- https://ncatlab.org/nlab/show/Grothendieck+fibration#StreetFibration
module Categories.Functor.Fibration {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F : Functor C D) where

open import Level

open import Categories.Morphism D using (_≅_)
open import Categories.Morphism.Cartesian using (Cartesian)

private
  module C = Category C
  module D = Category D
  open Functor F

record Fibration : Set (levelOfTerm F) where
  field
    universal₀ : ∀ {A B} (f : A D.⇒ F₀ B) → C.Obj
    universal₁ : ∀ {A B} (f : A D.⇒ F₀ B) → universal₀ f C.⇒ B
    iso        : ∀ {A B} (f : A D.⇒ F₀ B) → F₀ (universal₀ f) ≅ A

  module iso {A B} (f : A D.⇒ F₀ B) = _≅_ (iso f)

  field
    commute   : ∀ {A B} (f : A D.⇒ F₀ B) → f D.∘ iso.from f D.≈ F₁ (universal₁ f)
    cartesian : ∀ {A B} (f : A D.⇒ F₀ B) → Cartesian F (universal₁ f)

  module cartesian {A B} (f : A D.⇒ F₀ B) = Cartesian (cartesian f)

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 --cubical --no-import-sorts --safe #-}

module Cubical.Homotopy.EilenbergSteenrod where

{-
This module contains the Eilenberg-Steenrod axioms for ordinary
reduced cohomology theories with binary additivity.
The axioms are based on the ones given in Cavallo's MSc thesis
(https://www.cs.cmu.edu/~ecavallo/works/thesis15.pdf) and
Buchholtz/Favonia (2018)
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.Susp

open import Cubical.Data.Empty
open import Cubical.Relation.Nullary

open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Sigma
open import Cubical.Data.Int

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open GroupEquiv
open GroupHom

record coHomTheory {ℓ ℓ' : Level} (H : (n : Int) → Pointed ℓ → AbGroup {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ'))
  where
  Boolℓ : Pointed ℓ
  Boolℓ = Lift Bool , lift true
  field
    Hmap : (n : Int) → {A B : Pointed ℓ} (f : A →∙ B) → AbGroupHom (H n B) (H n A)
    Suspension : Σ[ F ∈ ((n : Int) {A : Pointed ℓ} → AbGroupEquiv (H (sucInt n) (Susp (typ A) , north)) (H n A)) ]
                   ({A B : Pointed ℓ} (f : A →∙ B) (n : Int)
               → fun (Hmap (sucInt n) (suspFun (fst f) , refl)) ∘ invEq (eq (F n {A = B}))
                ≡ invEq (eq (F n {A = A})) ∘ fun (Hmap n f))
    Exactness : {A B : Pointed ℓ}  (f : A →∙ B) (n :  Int)
              → Ker (Hmap n f)
               ≡ Im (Hmap n {B = _ , inr (pt B)} (cfcod (fst f) , refl))
    Dimension : (n : Int) → ¬ n ≡ 0 → isContr (fst (H n Boolℓ))
    BinaryWedge : (n : Int) {A B : Pointed ℓ} → AbGroupEquiv (H n (A ⋁ B , (inl (pt A)))) (dirProdAb (H n A) (H n B))


text:
data D : Set → Set1 where
  c : (A B : Set) → D (A → B)

test : (X : Set) → D X → Set
test .(A → B) (c A B) = A

-- this should crash Epic as long as A is considered forced in constructor c


text:
postulate
  A : Set
  P : A → Set
  p : (a : A) → P a

record R : Set where
  field
    a : A
  b : P _
  b = p a

test : A
test = R.b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2014-09-23
-- Check fixity declarations also in new 'instance' block.

module _ where

postulate
  D : Set

instance
  infixl 0 D Undeclared
  postulate d : D

-- Should fail with error:
-- Names out of scope in fixity declarations: Undeclared


text:
------------------------------------------------------------------------------
-- Example using distributive laws on a binary operation via Agsy
------------------------------------------------------------------------------

{-# OPTIONS --allow-unsolved-metas     #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- Tested with the development version of the Agda standard library on
-- 17 May 2012.

module Agsy.DistributiveLaws.TaskB-TopDown where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

infixl 7 _·_

------------------------------------------------------------------------------
-- Distributive laws axioms

postulate
  D   : Set        -- The universe
  _·_ : D → D → D  -- The binary operation.

  leftDistributive  : ∀ x y z → x · (y · z) ≡ (x · y) · (x · z)
  rightDistributive : ∀ x y z → (x · y) · z ≡ (x · z) · (y · z)

-- We test Agsy with the longest chains of equalities from
-- DistributiveLaws.TaskB-TopDownATP.
taskB : ∀ u x y z →
        (x · y · (z · u)) · ((x · y · ( z · u)) · (x · z · (y · u))) ≡
          x · z · (y · u)
taskB u x y z =
-- The numbering of the proof step justifications are associated with
-- the numbers used in DistributiveLaws.TaskB-I.
  begin
    xy·zu · (xy·zu · xz·yu)                                         ≡⟨ j₁₋₅ ⟩
    xy·zu · (xz · xu·yu · (y·zu · xz·yu))                           ≡⟨ j₅₋₉ ⟩
    xy·zu · (xz · xyu · (yxz · yu))                                 ≡⟨ j₉₋₁₄ ⟩
    xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))              ≡⟨ j₁₄₋₂₀ ⟩
    xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡⟨ j₂₀₋₂₃ ⟩
    xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))            ≡⟨ j₂₃₋₂₅ ⟩
    (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))                 ≡⟨ j₂₅₋₃₀ ⟩
    xz · xyu · (y·zy · xzu)                                         ≡⟨ j₃₀₋₃₅ ⟩
    xz·yu
  ∎
  where
  -- Two variables abbreviations

  xz = x · z
  yu = y · u
  yz = y · z

  -- Three variables abbreviations

  xyu = x · y · u
  xyz = x · y · z
  xzu = x · z · u
  yxz = y · x · z

  y·xu = y · (x · u)
  y·yu = y · (y · u)
  y·zu = y · (z · u)
  y·zy = y · (z · y)

  z·xu = z · (x · u)
  z·yu = z · (y · u)

  -- Four variables abbreviations

  xu·yu = x · u · (y · u)
  xu·zu = x · u · (z · u)

  xy·zu = x · y · (z · u)

  xz·yu = x · z · (y · u)

  -- Steps justifications

  j₁₋₅ : xy·zu · (xy·zu · xz·yu) ≡
         xy·zu · (xz · xu·yu · (y·zu · xz·yu))
  j₁₋₅ = {!-t 20 -m !}  -- Agsy fails

  j₅₋₉ : xy·zu · (xz · xu·yu · (y·zu · xz·yu)) ≡
         xy·zu · (xz · xyu · (yxz · yu))
  j₅₋₉ = {!-t 20 -m !}  -- Agsy fails

  j₉₋₁₄ : xy·zu · (xz · xyu · (yxz · yu)) ≡
          xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))
  j₉₋₁₄ = {!-t 20 -m!}  -- Agsy fails

  j₁₄₋₂₀ : xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu)) ≡
           xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  j₁₄₋₂₀ = {!-t 20 -m!}  -- Agsy fails

  j₂₀₋₂₃ : xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
           xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))
  j₂₀₋₂₃ = {!-t 20 -m!}  -- Agsy fails

  j₂₃₋₂₅ : xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu))) ≡
           (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))
  j₂₃₋₂₅ = {!-t 20 -m!}  -- Agsy fails

  j₂₅₋₃₀ : (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu)) ≡
           xz · xyu · (y·zy · xzu)
  j₂₅₋₃₀ = {!-t 20 -m!}  -- Agsy fails

  j₃₀₋₃₅ : xz · xyu · (y·zy · xzu) ≡
           xz·yu
  j₃₀₋₃₅ = {!-t 20 -m!}  -- Agsy fails

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Cubical.Algebra.Algebra.Base public


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

module Definition.Conversion.FullReduction where

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.Typed.Weakening
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Conversion.Stability
open import Definition.Typed.Consequences.Inversion
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.RelevanceUnicity
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.TypeUnicity

open import Tools.Empty using (⊥; ⊥-elim)
open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  data NfNeutral (Γ : Con Term) : Term → Set where
    var     : ∀ n                     → NfNeutral Γ (var n)
    ∘ₙ      : ∀ {k u l}     → NfNeutral Γ  k → Nf Γ u → NfNeutral Γ  (k ∘ u ^ l)
    natrecₙ : ∀ {l C c g k} →  Nf (Γ ∙ ℕ ^ [ ! , ι ⁰ ]) C → Nf Γ c → Nf Γ g → NfNeutral Γ  k → NfNeutral Γ  (natrec l C c g k)
    Idₙ : ∀ {A t u} → NfNeutral Γ  A → Nf Γ t → Nf Γ u → NfNeutral Γ  (Id A t u)
    Idℕₙ : ∀ {t u} → NfNeutral Γ  t → Nf Γ u → NfNeutral Γ  (Id ℕ t u)
    Idℕ0ₙ : ∀ {u} → NfNeutral Γ  u → NfNeutral Γ  (Id ℕ zero u)
    IdℕSₙ : ∀ {t u} → Nf Γ t → NfNeutral Γ  u → NfNeutral Γ  (Id ℕ (suc t) u)
    IdUₙ : ∀ {t u l} → NfNeutral Γ  t → Nf Γ u → NfNeutral Γ  (Id (U l) t u)
    IdUℕₙ : ∀ {u l} → NfNeutral Γ  u → NfNeutral Γ  (Id (U l) ℕ u)
    IdUΠₙ : ∀ {A rA lA B lB l u} → Nf Γ A → Nf (Γ ∙ A ^ [ rA , ι lA ]) B → NfNeutral Γ  u
                                 → NfNeutral Γ  (Id (U l) (Π A ^ rA ° lA ▹ B ° lB ° l) u)
    castₙ : ∀ {l A B e t} → NfNeutral Γ  A → Nf Γ B → Nf Γ t → NfNeutral Γ  (cast l A B e t)
    castℕₙ : ∀ {l B e t} → NfNeutral Γ  B → Nf Γ t → NfNeutral Γ  (cast l ℕ B e t)
    castΠₙ : ∀ {l A rA lA P lP B e t} → Nf Γ A → Nf (Γ ∙ A ^ [ rA , ι lA ]) P → NfNeutral Γ  B → Nf Γ t
                                      → NfNeutral Γ (cast l (Π A ^ rA ° lA ▹ P ° lP ° l) B e t)
    castℕℕₙ : ∀ {l e t} → NfNeutral Γ  t → NfNeutral Γ  (cast l ℕ ℕ e t)
    castℕΠₙ : ∀ {l A rA B e t} → Nf Γ A → Nf (Γ ∙ A ^ [ rA , ι ⁰ ]) B → Nf Γ t → NfNeutral Γ  (cast l ℕ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) e t)
    castΠℕₙ : ∀ {l A rA B e t} → Nf Γ A → Nf (Γ ∙ A ^ [ rA , ι ⁰ ]) B → Nf Γ t → NfNeutral Γ  (cast l (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) ℕ e t)
    castΠΠ%!ₙ : ∀ {l A B A' B' e t} → Nf Γ A → Nf (Γ ∙ A ^ [ % , ι ⁰ ]) B → Nf Γ A' → Nf (Γ ∙ A' ^ [ ! , ι ⁰ ]) B' → Nf Γ t
                                    → NfNeutral Γ  (cast l (Π A ^ % ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ ! ° ⁰ ▹ B' ° ⁰ ° l) e t)
    castΠΠ!%ₙ : ∀ {l A B A' B' e t} → Nf Γ A → Nf (Γ ∙ A ^ [ ! , ι ⁰ ]) B → Nf Γ A' → Nf (Γ ∙ A' ^ [ % , ι ⁰ ]) B' → Nf Γ t
                                    → NfNeutral Γ  (cast l (Π A ^ ! ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ % ° ⁰ ▹ B' ° ⁰ ° l) e t)
    Emptyrecₙ : ∀ {l lEmpty A e} → Nf Γ A → NfNeutral Γ  (Emptyrec l lEmpty A e)

  data Nf (Γ : Con Term) : Term → Set where

    Uₙ    : ∀ {r l} → Nf Γ (Univ r l)
    Πₙ    : ∀ {A r lA B lB l} → Nf Γ A → Nf (Γ ∙ A ^ [ r , ι lA ]) B → Nf Γ (Π A ^ r ° lA ▹ B ° lB ° l)
    ∃ₙ    : ∀ {l A B} → Γ ⊢ A ^ [ % , ι l ] → Nf Γ A → Nf (Γ ∙ A ^ [ % , ι l ]) B → Nf Γ (∃ A ▹ B)
    ℕₙ    : Nf Γ ℕ
    Emptyₙ : ∀ {l} → Nf Γ (Empty l)

    lamₙ  : ∀ {A l rF lF t} → Γ ⊢ A ^ [ rF , ι lF ] → Nf (Γ ∙ A ^ [ rF , ι lF ]) t → Nf Γ (lam A ▹ t ^ l)
    zeroₙ : Nf Γ zero
    sucₙ  : ∀ {t} → Nf Γ t → Nf Γ (suc t)

    ne   : ∀ {n} → NfNeutral Γ  n → Nf Γ n
    sprop   : ∀ {t A l} → Γ ⊢ t ∷ A ^ [ % , l ] → Nf Γ t

NfNeutralNeutral :  ∀ {t Γ} → NfNeutral Γ t → Neutral t
NfNeutralNeutral (var n) = var n
NfNeutralNeutral (∘ₙ X x) = ∘ₙ (NfNeutralNeutral X)
NfNeutralNeutral (natrecₙ x x₁ x₂ X) = natrecₙ (NfNeutralNeutral X)
NfNeutralNeutral (Idₙ X x x₁) = Idₙ (NfNeutralNeutral X)
NfNeutralNeutral (Idℕₙ X x) = Idℕₙ (NfNeutralNeutral X)
NfNeutralNeutral (Idℕ0ₙ X) = Idℕ0ₙ (NfNeutralNeutral X)
NfNeutralNeutral (IdℕSₙ x X) = IdℕSₙ (NfNeutralNeutral X)
NfNeutralNeutral (IdUₙ X x) = IdUₙ (NfNeutralNeutral X)
NfNeutralNeutral (IdUℕₙ X) = IdUℕₙ (NfNeutralNeutral X)
NfNeutralNeutral (IdUΠₙ x x₁ X) = IdUΠₙ (NfNeutralNeutral X)
NfNeutralNeutral (castₙ X x x₁) = castₙ (NfNeutralNeutral X)
NfNeutralNeutral (castℕₙ X x) = castℕₙ (NfNeutralNeutral X)
NfNeutralNeutral (castΠₙ x x₁ X x₂) = castΠₙ (NfNeutralNeutral X)
NfNeutralNeutral (castℕℕₙ X) = castℕℕₙ (NfNeutralNeutral X)
NfNeutralNeutral (castℕΠₙ x x₁ x₂) = castℕΠₙ
NfNeutralNeutral (castΠℕₙ x x₁ x₂) = castΠℕₙ
NfNeutralNeutral (castΠΠ%!ₙ x x₁ x₂ x₃ x₄) = castΠΠ%!ₙ
NfNeutralNeutral (castΠΠ!%ₙ x x₁ x₂ x₃ x₄) = castΠΠ!%ₙ
NfNeutralNeutral (Emptyrecₙ x) = Emptyrecₙ

NfWhnf :  ∀ {Γ t A l} → Γ ⊢ t ∷ A ^ [ ! , l ] → Nf Γ t → Whnf t
NfWhnf ⊢t Uₙ = Uₙ
NfWhnf ⊢t (Πₙ X X₁) = Πₙ
NfWhnf ⊢t (∃ₙ _ X X₁) = ∃ₙ
NfWhnf ⊢t ℕₙ = ℕₙ
NfWhnf ⊢t Emptyₙ = Emptyₙ
NfWhnf ⊢t (lamₙ _ X) = lamₙ
NfWhnf ⊢t zeroₙ = zeroₙ
NfWhnf ⊢t (sucₙ X) = sucₙ
NfWhnf ⊢t (ne x) = ne (NfNeutralNeutral x)
NfWhnf ⊢t (sprop ⊢t') = let !≡% , _  = type-uniq ⊢t ⊢t' in ⊥-elim (!≢% !≡%)

NfΠinversion :  ∀ {F G rF lF lG lΠ Γ} → Nf Γ (Π F ^ rF ° lF ▹ G ° lG ° lΠ ) → Nf Γ F × Nf (Γ ∙ F ^ [ rF , ι lF ]) G
NfΠinversion (Πₙ X Y) = X , Y
NfΠinversion (sprop ⊢t) =
  let _ , _ , _ , _ , _ , _ , e = inversion-Π ⊢t
      %≡! , _ = typelevel-injectivity e
  in ⊥-elim (!≢% (PE.sym %≡!))

NfΠA′ : ∀ {A F G rF lF lG lΠ Γ l} ([Π] : Γ ⊩⟨ l ⟩Π Π F ^ rF ° lF ▹ G ° lG ° lΠ ^[ ! , lΠ ] )
    → Γ ⊩⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≡ A ^ [ ! ,  ι lΠ ] / (Π-intr [Π])
    → Nf Γ A
    → ∃₂ λ H E → Nf Γ H × Nf (Γ ∙ H ^ [ rF , ι lF ]) E × A PE.≡ Π H ^ rF ° lF ▹ E ° lG ° lΠ
NfΠA′ (noemb (Πᵣ rF′ lF′ lG′ lF≤ lG≤  F G D ⊢F ⊢G A≡A [F] [G] G-ext)) (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) nfA =
    let _ , rF≡rF′ , lF≡lF′ , _ , lG≡lG′ , _ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
        X = whnfRed* D′ (NfWhnf (un-univ (redFirst* D′)) nfA)
        NfH , NfE =  NfΠinversion (PE.subst (Nf _) X nfA)
    in F′ , G′ , NfH , PE.subst₂ (λ r l →  Nf (_ ∙ _ ^ [ r , ι l ]) _) (PE.sym rF≡rF′) (PE.sym lF≡lF′) NfE ,
       PE.subst (λ r → _ PE.≡ Π _ ^ r ° _ ▹ _ ° _ ° _) (PE.sym rF≡rF′)
         (PE.subst (λ l → _ PE.≡ Π _ ^ _ ° l ▹ _ ° _ ° _) (PE.sym lF≡lF′)
           (PE.subst (λ l → _ PE.≡ Π _ ^ _ ° _ ▹ _ ° l ° _) (PE.sym lG≡lG′) X))
NfΠA′ (emb emb< [Π]) [Π≡A] nfA = NfΠA′ [Π] [Π≡A] nfA
NfΠA′ (emb ∞< [Π]) [Π≡A] nfA = NfΠA′ [Π] [Π≡A] nfA

NfΠA : ∀ {A F G rF lF lG lΠ Γ}
    → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≡ A ^ [ ! ,  ι lΠ ]
    → Nf Γ A
    → ∃₂ λ H E → Nf Γ H × Nf (Γ ∙ H ^ [ rF , ι lF ]) E × A PE.≡ Π H ^ rF ° lF ▹ E ° lG ° lΠ
NfΠA {A} Π≡A whnfA  =
  let X = reducibleEq Π≡A
      [Π] = proj₁ X
      [A] = proj₁ (proj₂ X)
      [Π≡A] = proj₂ (proj₂ X)
  in NfΠA′ (Π-elim [Π]) (irrelevanceEq [Π] (Π-intr (Π-elim [Π])) [Π≡A]) whnfA

mutual

  convNfNeutral :  ∀ {Γ Δ t A r} → ⊢ Γ ≡ Δ → Γ ⊢ t ∷ A ^ r → NfNeutral Γ t → NfNeutral Δ t
  convNfNeutral Γ≡Δ ⊢t (var n) = var n
  convNfNeutral Γ≡Δ ⊢t (∘ₙ X x) =
    let F , rF , lF , G , lG , rG , ⊢k , ⊢u , _ , erl = inversion-app ⊢t
    in ∘ₙ (convNfNeutral Γ≡Δ ⊢k X) (convNf Γ≡Δ ⊢u x)
  convNfNeutral Γ≡Δ ⊢t (natrecₙ x x₁ x₂ X) =
    let _ , ⊢x , ⊢x₁ , ⊢x₂ , ⊢X , _ = inversion-natrec ⊢t
    in natrecₙ (convNf (Γ≡Δ ∙ refl (univ (ℕⱼ (wfTerm ⊢t)))) (un-univ ⊢x) x) (convNf Γ≡Δ ⊢x₁ x₁)
               (convNf Γ≡Δ ⊢x₂ x₂) (convNfNeutral Γ≡Δ ⊢X X)
  convNfNeutral Γ≡Δ ⊢t (Idₙ X x x₁) =
    let _ , ⊢X , ⊢x , ⊢x₁ , _ = inversion-Id ⊢t
    in Idₙ (convNfNeutral Γ≡Δ ⊢X X) (convNf Γ≡Δ ⊢x x) (convNf Γ≡Δ ⊢x₁ x₁)
  convNfNeutral Γ≡Δ ⊢t (Idℕₙ X x) =
    let _ , _ , ⊢X , ⊢x , _ = inversion-Id ⊢t
    in Idℕₙ (convNfNeutral Γ≡Δ ⊢X X) (convNf Γ≡Δ ⊢x x)
  convNfNeutral Γ≡Δ ⊢t (Idℕ0ₙ X) =
    let _ , _ , _ , ⊢X , _ = inversion-Id ⊢t
    in Idℕ0ₙ (convNfNeutral Γ≡Δ ⊢X X)
  convNfNeutral Γ≡Δ ⊢t (IdℕSₙ x X) =
    let _ , _ , ⊢x , ⊢X , _ = inversion-Id ⊢t
    in IdℕSₙ (convNf Γ≡Δ (proj₁ (inversion-suc ⊢x)) x) (convNfNeutral Γ≡Δ ⊢X X)
  convNfNeutral Γ≡Δ ⊢t (IdUₙ X x) =
    let _ , _ , ⊢X , ⊢x , _ = inversion-Id ⊢t
    in IdUₙ (convNfNeutral Γ≡Δ ⊢X X) (convNf Γ≡Δ ⊢x x)
  convNfNeutral Γ≡Δ ⊢t (IdUℕₙ X) =
    let _ , _ , _ , ⊢X , _ = inversion-Id ⊢t
    in IdUℕₙ (convNfNeutral Γ≡Δ ⊢X X)
  convNfNeutral Γ≡Δ ⊢t (IdUΠₙ x x₁ X) =
    let _ , _ , ⊢Π , ⊢X , _ = inversion-Id ⊢t
        _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢Π
    in IdUΠₙ (convNf Γ≡Δ ⊢F x) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G x₁) (convNfNeutral Γ≡Δ ⊢X X)
  convNfNeutral Γ≡Δ ⊢t (castₙ X x x₁) =
    let _ , ⊢X , ⊢x , ⊢e , ⊢x₁ , _ = inversion-cast ⊢t
    in castₙ (convNfNeutral Γ≡Δ ⊢X X) (convNf Γ≡Δ ⊢x x) (convNf Γ≡Δ ⊢x₁ x₁)
  convNfNeutral Γ≡Δ ⊢t (castℕₙ X x) =
    let _ , _ , ⊢X , ⊢e , ⊢x , _ = inversion-cast ⊢t
    in castℕₙ (convNfNeutral Γ≡Δ ⊢X X) (convNf Γ≡Δ ⊢x x)
  convNfNeutral Γ≡Δ ⊢t (castΠₙ x x₁ X x₂) =
    let _ , ⊢Π , ⊢X , ⊢e , ⊢x₂ , _ = inversion-cast ⊢t
        _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢Π
    in castΠₙ (convNf Γ≡Δ ⊢F x) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G x₁) (convNfNeutral Γ≡Δ ⊢X X) (convNf Γ≡Δ ⊢x₂ x₂)
  convNfNeutral Γ≡Δ ⊢t (castℕℕₙ X) =
    let _ , _ , _ , _ , ⊢X , _ = inversion-cast ⊢t
    in castℕℕₙ (convNfNeutral Γ≡Δ ⊢X X)
  convNfNeutral Γ≡Δ ⊢t (castℕΠₙ x x₁ x₂) =
    let _ , _ , ⊢Π , ⊢e , ⊢x₂ , _ = inversion-cast ⊢t
        _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢Π
    in castℕΠₙ (convNf Γ≡Δ ⊢F x) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G x₁) (convNf Γ≡Δ ⊢x₂ x₂)
  convNfNeutral Γ≡Δ ⊢t (castΠℕₙ x x₁ x₂) =
    let _ , ⊢Π , _ , ⊢e , ⊢x₂ , _ = inversion-cast ⊢t
        _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢Π
    in castΠℕₙ (convNf Γ≡Δ ⊢F x) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G x₁) (convNf Γ≡Δ ⊢x₂ x₂)
  convNfNeutral Γ≡Δ ⊢t (castΠΠ%!ₙ x x₁ x₂ x₃ x₄) =
    let _ , ⊢Π , ⊢Π' , ⊢e , ⊢x₄ , _ = inversion-cast ⊢t
        _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢Π
        _ , _ , _ , ⊢F' , ⊢G' , _ = inversion-Π ⊢Π'
    in castΠΠ%!ₙ (convNf Γ≡Δ ⊢F x) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G x₁)
               (convNf Γ≡Δ ⊢F' x₂) (convNf (Γ≡Δ ∙ refl (univ ⊢F')) ⊢G' x₃) (convNf Γ≡Δ ⊢x₄ x₄)
  convNfNeutral Γ≡Δ ⊢t (castΠΠ!%ₙ x x₁ x₂ x₃ x₄) =
    let _ , ⊢Π , ⊢Π' , ⊢e , ⊢x₄ , _ = inversion-cast ⊢t
        _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢Π
        _ , _ , _ , ⊢F' , ⊢G' , _ = inversion-Π ⊢Π'
    in castΠΠ!%ₙ (convNf Γ≡Δ ⊢F x) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G x₁)
               (convNf Γ≡Δ ⊢F' x₂) (convNf (Γ≡Δ ∙ refl (univ ⊢F')) ⊢G' x₃) (convNf Γ≡Δ ⊢x₄ x₄)
  convNfNeutral Γ≡Δ ⊢t (Emptyrecₙ x) =
    let _ , ⊢x , _ = inversion-Emptyrec ⊢t
    in Emptyrecₙ (convNf Γ≡Δ (un-univ ⊢x) x)

  convNf :  ∀ {Γ Δ t A r} → ⊢ Γ ≡ Δ → Γ ⊢ t ∷ A ^ r → Nf Γ t → Nf Δ t
  convNf Γ≡Δ ⊢t Uₙ = Uₙ
  convNf Γ≡Δ ⊢t (Πₙ X X₁) =
    let _ , _ , _ , ⊢F , ⊢G , _ = inversion-Π ⊢t
    in Πₙ (convNf Γ≡Δ ⊢F X) (convNf (Γ≡Δ ∙ refl (univ ⊢F)) ⊢G X₁)
  convNf Γ≡Δ ⊢t (∃ₙ ⊢A X X₁) =
    let l , ⊢F , ⊢G , _ , erl = inversion-∃ ⊢t
        _ , _  , erl  = type-uniq (un-univ ⊢A) ⊢F
        _ , elA = Uinjectivity erl
    in ∃ₙ (stability Γ≡Δ ⊢A) (convNf Γ≡Δ ⊢F X) (convNf (Γ≡Δ ∙ refl (⊢A))
          (PE.subst (λ l → _ ∙ _ ^ [ % , ι l ] ⊢ _ ∷ SProp l ^ [ ! , next l ]) (PE.sym elA) ⊢G) X₁)
  convNf Γ≡Δ ⊢t ℕₙ = ℕₙ
  convNf Γ≡Δ ⊢t Emptyₙ = Emptyₙ
  convNf Γ≡Δ ⊢t (lamₙ ⊢F X) =
    let rF , lF , G , rG , lG , ⊢F' , ⊢t' , _ , erl = inversion-lam ⊢t
        er , el = typelevel-injectivity erl
        _ , _  , erl  = type-uniq (un-univ ⊢F) (un-univ ⊢F')
        erF , elF = Uinjectivity erl
    in lamₙ (stability Γ≡Δ  ⊢F) (convNf (Γ≡Δ ∙ refl ⊢F)
            (PE.subst₂ (λ r l → _ ∙ _ ^ [ r , ι l ] ⊢ _ ∷ G ^ [ rG , ι lG ]) (PE.sym erF) (PE.sym elF) ⊢t')  X)
  convNf Γ≡Δ ⊢t zeroₙ = zeroₙ
  convNf Γ≡Δ ⊢t (sucₙ X) = sucₙ (convNf Γ≡Δ (proj₁ (inversion-suc ⊢t)) X )
  convNf Γ≡Δ ⊢t (ne x) = ne (convNfNeutral Γ≡Δ ⊢t x)
  convNf Γ≡Δ ⊢t (sprop x) = sprop (stabilityTerm Γ≡Δ x)

mutual
  fullRedNe : ∀ {t A l Γ} → Γ ⊢ t ~ t ↑! A ^ l → ∃ λ u → NfNeutral Γ u × Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
  fullRedNe (var-refl x _) = var _ , var _ , refl x
  fullRedNe (app-cong {rF = !} {lΠ = lΠ} t u) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
        u′ , nfU′ , u≡u′ = fullRedTerm u
    in  (t′ ∘ u′ ^ lΠ) ,
        ∘ₙ nfT′ nfU′ ,
        app-cong t≡t′ u≡u′
  fullRedNe (app-cong {t = a} {rF = %} {lΠ = lΠ} t (%~↑ ⊢a ⊢a')) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
    in  (t′ ∘ a ^ lΠ) ,
        ∘ₙ nfT′ (sprop ⊢a) ,
        app-cong t≡t′ (proof-irrelevance ⊢a ⊢a')
  fullRedNe (natrec-cong {lF = l} C z s n) =
    let C′ , nfC′ , C≡C′ = fullRed C
        z′ , nfZ′ , z≡z′ = fullRedTerm z
        s′ , nfS′ , s≡s′ = fullRedTerm s
        n′ , nfN′ , n≡n′ = fullRedNe′ n
    in  natrec l C′ z′ s′ n′
     , natrecₙ nfC′ nfZ′ nfS′ nfN′
     ,  natrec-cong C≡C′ z≡z′ s≡s′ n≡n′
  fullRedNe (Emptyrec-cong {k = k} {ll = l} {lEmpty = lEmpty} C (%~↑ ⊢e ⊢e')) =
    let C′ , nfC′ , C≡C′ = fullRed C
    in  Emptyrec l lEmpty C′ k , Emptyrecₙ nfC′
     ,  Emptyrec-cong C≡C′ ⊢e ⊢e'
  fullRedNe (Id-cong A t u) =
    let A′ , nfA′ , A≡A′ = fullRedNe′ A
        t′ , nfT′ , t≡t′ = fullRedTerm t
        u′ , nfU′ , u≡u′ = fullRedTerm u
    in Id A′ t′ u′ , Idₙ nfA′ nfT′ nfU′ , Id-cong A≡A′ t≡t′ u≡u′
  fullRedNe (Id-ℕ t u) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
        u′ , nfU′ , u≡u′ = fullRedTerm u
    in Id ℕ t′ u′ , Idℕₙ  nfT′ nfU′ , Id-cong (refl (ℕⱼ (wfEqTerm u≡u′))) t≡t′ u≡u′
  fullRedNe (Id-ℕ0 t) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
    in Id ℕ zero t′ , Idℕ0ₙ  nfT′ , Id-cong (refl (ℕⱼ (wfEqTerm t≡t′))) (refl (zeroⱼ (wfEqTerm t≡t′))) t≡t′
  fullRedNe (Id-ℕS t u) =
    let t′ , nfT′ , t≡t′ = fullRedTerm t
        u′ , nfU′ , u≡u′ = fullRedNe′ u
    in Id ℕ (suc t′) u′ , IdℕSₙ nfT′ nfU′ , Id-cong (refl (ℕⱼ (wfEqTerm u≡u′))) (suc-cong t≡t′) u≡u′
  fullRedNe (Id-U t u) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
        u′ , nfU′ , u≡u′ = fullRedTerm u
    in Id (U _) t′ u′ , IdUₙ nfT′ nfU′ , Id-cong (refl (univ 0<1 (wfEqTerm u≡u′))) t≡t′ u≡u′
  fullRedNe (Id-Uℕ t) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
    in Id (U _) ℕ t′ , IdUℕₙ nfT′ , Id-cong (refl (univ 0<1 (wfEqTerm t≡t′))) (refl (ℕⱼ (wfEqTerm t≡t′))) t≡t′
  fullRedNe (Id-UΠ {rA = rA} A t) =
    let t′ , nfT′ , t≡t′ = fullRedNe′ t
        A′ , nfA′ , A≡A′ = fullRedTerm A
        H , E , NfH , NfE , Π≡HE = NfΠA (univ A≡A′) nfA′
    in Id (U _) (Π H ^ rA ° ⁰ ▹ E ° ⁰ ° ⁰) t′ ,
       IdUΠₙ NfH NfE nfT′ ,
       Id-cong (refl (univ 0<1 (wfEqTerm t≡t′))) (PE.subst (λ A → _ ⊢ _ ≡ A ∷ U ⁰ ^ _) Π≡HE A≡A′) t≡t′
  fullRedNe (cast-cong {e = e} {e' = e'} x x₁ x₂ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedNe′ x
        B′ , nfB′ , B≡B′ = fullRedTerm x₁
        t′ , nft′ , t≡t′ = fullRedTerm x₂
    in cast ⁰ A′ B′ e t′ , castₙ nfA′ nfB′ nft′ ,
       cast-cong A≡A′ B≡B′ t≡t′ ⊢e (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) A≡A′ B≡B′)))
  fullRedNe (cast-ℕ {e = e} {e' = e'} x x₁ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedNe′ x
        t′ , nft′ , t≡t′ = fullRedTerm x₁
    in cast ⁰ _ A′ e t′ , castℕₙ nfA′ nft′ ,
       cast-cong (refl (ℕⱼ (wfTerm ⊢e)) ) A≡A′ t≡t′ ⊢e
                 (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) (refl (ℕⱼ (wfTerm ⊢e))) A≡A′)))
  fullRedNe (cast-ℕℕ {e = e} {e' = e'} x ⊢e ⊢e') =
      let t′ , nft′ , t≡t′ = fullRedNe′ x
    in cast ⁰ _ _ e t′ , castℕℕₙ nft′ ,
       cast-cong (refl (ℕⱼ (wfTerm ⊢e)) ) (refl (ℕⱼ (wfTerm ⊢e)) ) t≡t′ ⊢e ⊢e
  fullRedNe (cast-Π {e = e} {e' = e'} x x₁ x₂ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedTerm x
        B′ , nfB′ , B≡B′ = fullRedNe′ x₁
        t′ , nft′ , t≡t′ = fullRedTerm x₂
        H , E , NfH , NfE , Π≡HE = NfΠA (univ A≡A′) nfA′
        nfCast = castΠₙ NfH NfE nfB′ nft′
    in cast ⁰ A′ B′ e t′ , PE.subst (λ A →  NfNeutral _ (cast ⁰ A _ _ _)) (PE.sym Π≡HE) nfCast ,
       cast-cong A≡A′ B≡B′ t≡t′ ⊢e (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) A≡A′ B≡B′)))
  fullRedNe (cast-Πℕ {e = e} {e' = e'} x x₁ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedTerm x
        t′ , nft′ , t≡t′ = fullRedTerm x₁
        H , E , NfH , NfE , Π≡HE = NfΠA (univ A≡A′) nfA′
        nfCast = castΠℕₙ NfH NfE nft′
    in cast ⁰ A′ ℕ e t′ , PE.subst (λ A →  NfNeutral _ (cast ⁰ A _ _ _)) (PE.sym Π≡HE) nfCast ,
       cast-cong A≡A′ (refl (ℕⱼ (wfTerm ⊢e))) t≡t′ ⊢e (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) A≡A′ (refl (ℕⱼ (wfTerm ⊢e))))))
  fullRedNe (cast-ℕΠ {e = e} {e' = e'} x x₁ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedTerm x
        t′ , nft′ , t≡t′ = fullRedTerm x₁
        H , E , NfH , NfE , Π≡HE = NfΠA (univ A≡A′) nfA′
        nfCast = castℕΠₙ NfH NfE nft′
    in cast ⁰ ℕ A′ e t′ , PE.subst (λ A →  NfNeutral _ (cast ⁰ _ A _ _)) (PE.sym Π≡HE) nfCast ,
       cast-cong (refl (ℕⱼ (wfTerm ⊢e))) A≡A′ t≡t′ ⊢e (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) (refl (ℕⱼ (wfTerm ⊢e))) A≡A′ )))
  fullRedNe (cast-ΠΠ%! {e = e} {e' = e'} x x₁ x₂ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedTerm x
        B′ , nfB′ , B≡B′ = fullRedTerm x₁
        t′ , nft′ , t≡t′ = fullRedTerm x₂
        H , E , NfH , NfE , Π≡HE = NfΠA (univ A≡A′) nfA′
        H' , E' , NfH' , NfE' , Π≡HE' = NfΠA (univ B≡B′) nfB′
        nfCast = castΠΠ%!ₙ NfH NfE NfH' NfE' nft′
    in cast ⁰ A′ B′ e t′ , PE.subst₂ (λ A B →  NfNeutral _ (cast ⁰ A B _ _)) (PE.sym Π≡HE) (PE.sym Π≡HE') nfCast ,
       cast-cong A≡A′ B≡B′ t≡t′ ⊢e (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) A≡A′ B≡B′ )))
  fullRedNe (cast-ΠΠ!% {e = e} {e' = e'} x x₁ x₂ ⊢e ⊢e') =
    let A′ , nfA′ , A≡A′ = fullRedTerm x
        B′ , nfB′ , B≡B′ = fullRedTerm x₁
        t′ , nft′ , t≡t′ = fullRedTerm x₂
        H , E , NfH , NfE , Π≡HE = NfΠA (univ A≡A′) nfA′
        H' , E' , NfH' , NfE' , Π≡HE' = NfΠA (univ B≡B′) nfB′
        nfCast = castΠΠ!%ₙ NfH NfE NfH' NfE' nft′
    in cast ⁰ A′ B′ e t′ , PE.subst₂ (λ A B →  NfNeutral _ (cast ⁰ A B _ _)) (PE.sym Π≡HE) (PE.sym Π≡HE') nfCast ,
       cast-cong A≡A′ B≡B′ t≡t′ ⊢e (conv ⊢e (univ (Id-cong (refl (univ 0<1 (wfTerm ⊢e)) ) A≡A′ B≡B′ )))

  fullRedNe′ : ∀ {t A rA Γ} → Γ ⊢ t ~ t ↓! A ^ rA → ∃ λ u → NfNeutral Γ u × Γ ⊢ t ≡ u ∷ A ^ [ ! , rA ]
  fullRedNe′ ([~] A D whnfB k~l) =
    let u , nf , t≡u = fullRedNe k~l
    in u , nf , conv t≡u (subset* D)

  fullRed : ∀ {A rA Γ} → Γ ⊢ A [conv↑] A ^ rA → ∃ λ B → Nf Γ B × Γ ⊢ A ≡ B ^ rA
  fullRed ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
    rewrite whrDet* (D , whnfA′) (D′ , whnfB′) =
    let B″ , nf , B′≡B″ = fullRed′ A′<>B′
    in  B″ , nf , trans (subset* D′) B′≡B″

  fullRed′ : ∀ {A rA Γ} → Γ ⊢ A [conv↓] A ^ rA → ∃ λ B → Nf Γ B × Γ ⊢ A ≡ B ^ rA
  fullRed′ (U-refl {r = r} _ ⊢Γ) = Univ r ¹  , Uₙ , refl (Uⱼ ⊢Γ)
  fullRed′ (univ x) =
    let u , Nfu , u≡u = fullRedTerm′ x
    in u , Nfu , univ u≡u

  fullRedTerm : ∀ {t A l Γ} → Γ ⊢ t [conv↑] t ∷ A ^ l → ∃ λ u → Nf Γ u × Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
  fullRedTerm ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
    rewrite whrDet*Term (d , whnft′) (d′ , whnfu′) =
    let u″ , nf , u′≡u″ = fullRedTerm′ t<>u
    in  u″ , nf , conv (trans (subset*Term d′) u′≡u″) (sym (subset* D))

  fullRedTerm′ : ∀ {t A l Γ} → Γ ⊢ t [conv↓] t ∷ A ^ l → ∃ λ u → Nf Γ u × Γ ⊢ t ≡ u ∷ A ^ [ ! , l ]
  fullRedTerm′ (U-refl {r = r} _ ⊢Γ) = Univ r ⁰ , Uₙ , refl (univ 0<1 ⊢Γ)
  fullRedTerm′ (ne A) =
    let B , nf , A≡B = fullRedNe′ A
    in  B , ne nf , A≡B
  fullRedTerm′ (ℕ-refl ⊢Γ) = ℕ , ℕₙ , refl (ℕⱼ ⊢Γ)
  fullRedTerm′ (Empty-refl PE.refl ⊢Γ) = Empty _ , Emptyₙ , refl (Emptyⱼ ⊢Γ)
  fullRedTerm′ (Π-cong {rF = rF} PE.refl PE.refl PE.refl PE.refl l< l<' ⊢F F G) =
    let F′ , nfF′ , F≡F′ = fullRedTerm F
        G′ , nfG′ , G≡G′ = fullRedTerm G
    in Π F′ ^ rF ° _ ▹ G′ ° _ ° _  , Πₙ nfF′ (convNf (reflConEq (wf ⊢F) ∙ univ F≡F′) (proj₂ (proj₂ (syntacticEqTerm G≡G′))) nfG′)
    ,  Π-cong l< l<' ⊢F F≡F′ G≡G′
  fullRedTerm′ (∃-cong PE.refl ⊢F F G) =
    let F′ , nfF′ , F≡F′ = fullRedTerm F
        G′ , nfG′ , G≡G′ = fullRedTerm G
    in ∃ F′ ▹ G′ , ∃ₙ (univ (proj₂ (proj₂ (syntacticEqTerm F≡F′)))) nfF′
         (convNf (reflConEq (wf ⊢F) ∙ univ F≡F′) (proj₂ (proj₂ (syntacticEqTerm G≡G′))) nfG′)
     , ∃-cong ⊢F F≡F′ G≡G′
  fullRedTerm′  (ℕ-ins t) =
    let u , nf , t≡u = fullRedNe′ t
    in  u , ne nf , t≡u
  fullRedTerm′ (ne-ins ⊢t _ _ t) =
    let u , nfU , t≡u = fullRedNe′ t
        _ , ⊢t∷M , _ = syntacticEqTerm t≡u
        _ , neT , _ = ne~↓! t
    in  u , ne nfU , conv t≡u (proj₂ (neTypeEq neT ⊢t∷M ⊢t))
  fullRedTerm′ (zero-refl ⊢Γ) = zero , zeroₙ , refl (zeroⱼ ⊢Γ)
  fullRedTerm′ (suc-cong t) =
    let u , nf , t≡u = fullRedTerm t
    in  suc u , sucₙ nf , suc-cong t≡u
  fullRedTerm′ (η-eq {F = F} {l = l} l< l<' ⊢F ⊢t _ _ _ t∘0) =
    let u , nf , t∘0≡u = fullRedTerm t∘0
        _ , _ , ⊢u = syntacticEqTerm t∘0≡u
        ΓF⊢ = wf ⊢F ∙ ⊢F
        wk⊢F = wk (step id) ΓF⊢ ⊢F
        ΓFF'⊢ = ΓF⊢ ∙ wk⊢F
        wk⊢u = wkTerm (lift (step id)) ΓFF'⊢ ⊢u
        λu∘0 = (lam _ ▹ (U.wk (lift (step id)) u) ^ _) ∘ var 0 ^ l
    in  lam _ ▹ u ^ _ ,
        lamₙ ⊢F nf
     ,  η-eq l< l<' ⊢F ⊢t (lamⱼ l< l<' ⊢F ⊢u)
             (trans t∘0≡u (PE.subst₂ (λ x y → _ ⊢ x ≡ λu∘0 ∷ y ^ _)
                                     (wkSingleSubstId u) (wkSingleSubstId _)
                                     (sym (β-red l< l<' wk⊢F wk⊢u (var ΓF⊢ here)))))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.EpochManager           as EpochManager
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.TestUtils.MockStorage  as MockStorage
import      LibraBFT.Impl.Types.OnChainConfig.ValidatorSet as ValidatorSet
import      LibraBFT.Impl.Types.ValidatorSigner            as ValidatorSigner
import      LibraBFT.Impl.Types.Waypoint                   as Waypoint
import      LibraBFT.Impl.IO.OBM.GenKeyFile                as GenKeyFile
import      LibraBFT.Impl.OBM.ConfigHardCoded              as ConfigHardCoded
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.PKCS
open import Util.Prelude                                   hiding (_++_)
------------------------------------------------------------------------------
open import Data.String                                    using (String; _++_)

module LibraBFT.Impl.Consensus.ConsensusProvider where

obmInitialData
  : GenKeyFile.NfLiwsVsVvPe
  → Either ErrLog
           (NodeConfig × OnChainConfigPayload × LedgerInfoWithSignatures × SK × ProposerElection)
obmInitialData ( _numFaults , genesisLIWS , validatorSigner
               , validatorVerifier , proposerElection ) = do
  let vs   = ValidatorSet.obmFromVV validatorVerifier
      occp = onChainConfigPayload vs
  wp       ← Waypoint.newEpochBoundary (genesisLIWS ^∙ liwsLedgerInfo)
  let nc   = nodeConfig wp
  pure (nc , occp , genesisLIWS , validatorSigner ^∙ vsPrivateKey , proposerElection)
 where
  onChainConfigPayload : ValidatorSet → OnChainConfigPayload
  onChainConfigPayload = OnChainConfigPayload∙new ({-Epoch-} 1)

  nodeConfig : Waypoint → NodeConfig
  nodeConfig genesisWaypoint =
    record -- NodeConfig
    { _ncObmMe     = validatorSigner ^∙ vsAuthor
    ; _ncConsensus = record -- ConsensusConfig
      { _ccMaxPrunedBlocksInMem  = ConfigHardCoded.maxPrunedBlocksInMem
      ; _ccRoundInitialTimeoutMS = ConfigHardCoded.roundInitialTimeoutMS
      ; _ccSafetyRules           = record -- SafetyRulesConfig
        { _srcService                     = SRSLocal
        ; _srcExportConsensusKey          = true
        ; _srcObmGenesisWaypoint          = genesisWaypoint
        }
      ; _ccSyncOnly              = false
      }
    }

abstract
  obmInitialData-ed-abs
    : GenKeyFile.NfLiwsVsVvPe
    → EitherD ErrLog
              (NodeConfig × OnChainConfigPayload × LedgerInfoWithSignatures × SK × ProposerElection)
  obmInitialData-ed-abs = fromEither ∘ obmInitialData

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

-- LBFT-OBM-DIFF
-- 'start_consensus' in Rust inits and loops
-- that is split so 'startConsensus' returns init data
-- then loop is called with that data.
module startConsensus-ed
  (nodeConfig : NodeConfig)
  -- BEGIN OBM
  (obmNow               : Instant)
  (obmPayload           : OnChainConfigPayload)
  (obmGenesisLIWS       : LedgerInfoWithSignatures)
  (obmSK                : SK)
  (obmNeedFetch         : ObmNeedFetch)
  (obmProposalGenerator : ProposalGenerator)
  (obmStateComputer     : StateComputer)
  where
  -- END OBM

  step₁ : ValidatorSet → (RecoveryData × PersistentLivenessStorage) → EitherD ErrLog (EpochManager × List Output)
  step₂ : PersistentLivenessStorage → ValidatorInfo → EitherD ErrLog (EpochManager × List Output)

  step₀ : EitherD ErrLog (EpochManager × List Output)
  step₀ = do
    let obmValidatorSet = obmPayload ^∙ occpObmValidatorSet
    eitherS (MockStorage.startForTesting obmValidatorSet (just obmGenesisLIWS)) LeftD (step₁ obmValidatorSet)

  step₁ obmValidatorSet (_obmRecoveryData , persistentLivenessStorage) = do
        let stateComputer = obmStateComputer
        eitherS (ValidatorSet.obmGetValidatorInfo (nodeConfig ^∙ ncObmMe) obmValidatorSet) LeftD (step₂ persistentLivenessStorage)

  step₂ persistentLivenessStorage vi = do
          eitherS (EpochManager.new nodeConfig stateComputer persistentLivenessStorage
                            (vi ^∙ viAccountAddress) obmSK) LeftD $
                   λ epochMgr →
                       EpochManager.start-ed
                         epochMgr obmNow
                         obmPayload obmNeedFetch obmProposalGenerator
                         obmGenesisLIWS

abstract
  startConsensus-ed-abs = startConsensus-ed.step₀
  startConsensus-ed-abs-≡ : startConsensus-ed-abs ≡ startConsensus-ed.step₀
  startConsensus-ed-abs-≡ = refl


text:
{-# OPTIONS --type-in-type
            --guardedness-preserving-type-constructors #-}

module Issue690b where

open import Common.Coinduction

data Rec (A : ∞ Set) : Set where
  fold : (x : ♭ A) → Rec A

infixr 4 _,_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

infix 4 _≡_

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

data ⊥ : Set where

{-# NON_TERMINATING #-}
D : Set
D = Rec (♯ Σ Set λ E → Σ (D ≡ E) λ _ → E → ⊥)

lam : (D → ⊥) → D
lam f = fold (D , refl , f)

app : D → D → ⊥
app (fold (.D , refl , f)) d = f d

omega : D
omega = lam (λ x → app x x)

Omega : ⊥
Omega = app omega omega

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core properties related to propositional list membership.
--
-- This file is needed to break the cyclic dependency with the proof
-- `Any-cong` in `Data.Any.Properties` which relies on `Any↔` in this
-- file.
------------------------------------------------------------------------

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

module Data.List.Membership.Propositional.Properties.Core where

open import Function using (flip; id; _∘_)
open import Function.Inverse using (_↔_; inverse)
open import Data.List.Base using (List)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Membership.Propositional
open import Data.Product as Prod
  using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl)
open import Relation.Unary using (_⊆_)

-- Lemmas relating map and find.

map∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs}
           (p : Any P xs) → let p′ = find p in
           {f : _≡_ (proj₁ p′) ⊆ P} →
           f refl ≡ proj₂ (proj₂ p′) →
           Any.map f (proj₁ (proj₂ p′)) ≡ p
map∘find (here  p) hyp = P.cong here  hyp
map∘find (there p) hyp = P.cong there (map∘find p hyp)

find∘map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
           {xs : List A} (p : Any P xs) (f : P ⊆ Q) →
           find (Any.map f p) ≡ Prod.map id (Prod.map id f) (find p)
find∘map (here  p) f = refl
find∘map (there p) f rewrite find∘map p f = refl

-- find satisfies a simple equality when the predicate is a
-- propositional equality.

find-∈ : ∀ {a} {A : Set a} {x : A} {xs : List A} (x∈xs : x ∈ xs) →
         find x∈xs ≡ (x , x∈xs , refl)
find-∈ (here refl)  = refl
find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl

-- find and lose are inverses (more or less).

lose∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A}
            (p : Any P xs) →
            uncurry′ lose (proj₂ (find p)) ≡ p
lose∘find p = map∘find p P.refl

find∘lose : ∀ {a p} {A : Set a} (P : A → Set p) {x xs}
            (x∈xs : x ∈ xs) (pp : P x) →
            find {P = P} (lose x∈xs pp) ≡ (x , x∈xs , pp)
find∘lose P x∈xs p
  rewrite find∘map x∈xs (flip (P.subst P) p)
        | find-∈ x∈xs
        = refl

-- Any can be expressed using _∈_

∃∈-Any : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
         (∃ λ x → x ∈ xs × P x) → Any P xs
∃∈-Any = uncurry′ lose ∘ proj₂

Any↔ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
       (∃ λ x → x ∈ xs × P x) ↔ Any P xs
Any↔ = inverse ∃∈-Any find from∘to lose∘find
  where
  from∘to : ∀ v → find (∃∈-Any v) ≡ v
  from∘to p = find∘lose _ (proj₁ (proj₂ p)) (proj₂ (proj₂ p))


text:
module core where

open import Data.Nat
open import Data.Vec
open import Data.Fin
open import Data.String
open import Data.Rational
open import Data.Sum
open import Data.Unit

open import Binders.Var

{-
module ABTLearning where
   data View {univ : Set} (f : univ -> Set) (a : univ) : list univ -> Set where
     Syn : f a -> View f a []
     Var :
   record ABT {u : Set}

data Var (a b : Set) where
    Free
-}

module Term  where
    data Literal : Set where
        Nat : ℕ  -> Literal
        Rat : ℚ -> Literal
        Str : String -> Literal
    data term (a : Set) : Set where
      v : a -> term a
      app : ∀  (n : ℕ ) ->   term a -> Vec (term a) n -> term a
      abs : ∀ (n : ℕ ) -> term (Var (Fin n) (term a))-> term a
      primcall : ∀ {n : ℕ } -> String -> Vec (term a) n -> term a
      lit :  Literal -> term a
      force : term a -> term a
      delay : term a -> term a

module TypedTerm where
  data PrimType : Set where
       Nat : PrimType
       Rat : PrimType
       Str : PrimType
  data Sort : Set where -- should this be a record??
       lit : ℕ -> Sort
       -- var :
       -- univ→ :
  data Literal : PrimType ->  Set where
        NatL : ℕ  -> Literal Nat
        RatL : ℚ -> Literal Rat
        StrL : String -> Literal Str

module PHOAS where
  data Exp (a : Set) : Set where
    Lam : (a -> Exp a) -> Exp a
    App : (Exp a) -> Exp a -> Exp a


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

open import HoTT hiding (_::_)

module algebra.ReducedWord {i} (A : Type i) (dec : has-dec-eq A) where

  open import algebra.Word A

  is-reduced : Word → Type i
  is-reduced nil                 = Lift ⊤
  is-reduced (x    :: nil)       = Lift ⊤
  is-reduced (x    :: y    :: w) = is-reduced (y :: w)
  is-reduced (x    :: y inv:: w) = (x ≠ y) × is-reduced (y inv:: w)
  is-reduced (x inv:: nil)       = Lift Unit
  is-reduced (x inv:: y    :: w) = (x ≠ y) × is-reduced (y :: w)
  is-reduced (x inv:: y inv:: w) = is-reduced (y inv:: w)

  ReducedWord : Type i
  ReducedWord = Σ Word is-reduced

  -- Everything is a set.

  A-is-set : is-set A
  A-is-set = dec-eq-is-set dec

  Word-has-dec-eq : has-dec-eq (Word)
  Word-has-dec-eq nil nil = inl idp
  Word-has-dec-eq nil         (x    :: w) = inr (lower ∘ Word=-out)
  Word-has-dec-eq nil         (x inv:: w) = inr (lower ∘ Word=-out)
  Word-has-dec-eq (x    :: v) nil         = inr (lower ∘ Word=-out)
  Word-has-dec-eq (x    :: v) (y    :: w) with (dec x y)
  Word-has-dec-eq (x    :: v) (y    :: w) | inl x=y with (Word-has-dec-eq v w)
  Word-has-dec-eq (x    :: v) (y    :: w) | inl x=y | inl v=w = inl (Word=-in (x=y , v=w))
  Word-has-dec-eq (x    :: v) (y    :: w) | inl x=y | inr v≠w = inr (v≠w ∘ Word-snd=)
  Word-has-dec-eq (x    :: v) (y    :: w) | inr x≠y = inr (x≠y ∘ Word-fst=)
  Word-has-dec-eq (x    :: v) (y inv:: w) = inr (lower ∘ Word=-out)
  Word-has-dec-eq (x inv:: v) nil         = inr (lower ∘ Word=-out)
  Word-has-dec-eq (x inv:: v) (y    :: w) = inr (lower ∘ Word=-out)
  Word-has-dec-eq (x inv:: v) (y inv:: w) with (dec x y)
  Word-has-dec-eq (x inv:: v) (y inv:: w) | inl x=y with (Word-has-dec-eq v w)
  Word-has-dec-eq (x inv:: v) (y inv:: w) | inl x=y | inl v=w = inl (Word=-in (x=y , v=w))
  Word-has-dec-eq (x inv:: v) (y inv:: w) | inl x=y | inr v≠w = inr (v≠w ∘ Word-snd=')
  Word-has-dec-eq (x inv:: v) (y inv:: w) | inr x≠y = inr (x≠y ∘ Word-fst=')

  Word-is-set : is-set Word
  Word-is-set = dec-eq-is-set Word-has-dec-eq

  is-reduced-is-prop : (w : Word) → is-prop (is-reduced w)
  is-reduced-is-prop nil                 = Lift-level Unit-is-prop
  is-reduced-is-prop (x    :: nil)       = Lift-level Unit-is-prop
  is-reduced-is-prop (x    :: y    :: w) = is-reduced-is-prop (y :: w)
  is-reduced-is-prop (x    :: y inv:: w) =
    ×-level (Π-is-prop (λ _ → λ ())) (is-reduced-is-prop (y inv:: w))
  is-reduced-is-prop (x inv:: nil)       = Lift-level Unit-is-prop
  is-reduced-is-prop (x inv:: y    :: w) =
    ×-level (Π-is-prop (λ _ → λ ())) (is-reduced-is-prop (y :: w))
  is-reduced-is-prop (x inv:: y inv:: w) = is-reduced-is-prop (y inv:: w)

  ReducedWord-is-set : is-set ReducedWord
  ReducedWord-is-set = subtype-level Word-is-set is-reduced-is-prop

  ReducedWord= : ReducedWord → ReducedWord → Type i
  ReducedWord= = subtype=

  ReducedWord=-in : {x y : ReducedWord} → ReducedWord= x y → x == y
  ReducedWord=-in = subtype=-in is-reduced-is-prop

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --no-termination-check
  #-}

------------------------------------------------------------------------
-- Examples
------------------------------------------------------------------------

module RecursiveDescent.Coinductive.Examples where

open import Data.List
open import Data.Nat
open import Data.Bool
open import Data.Product.Record
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Data.Char as C
import Data.String as S
open C using (Char)
open S using (String)

open import RecursiveDescent.Coinductive
open import Utilities
open import RecursiveDescent.Coinductive.Lib
open Sym C.decSetoid

-- A function used to simplify the examples a little.

_∈?_ : forall {i r} -> String -> Parser Char i r -> List r
s ∈? p = parse-complete p (S.toList s)

{-
module Ex₀ where

  -- This is not well-typed.

  p : Parser Char _ String
  p ~ return 5 ⊛> p
-}

module Ex₁ where

  -- e ∷= 0 + e | 0

  e ~ sym '0' ⊛> sym '+' ⊛> e
    ∣ sym '0'

  ex₁ : "0+0" ∈? e ≡ '0' ∷ []
  ex₁ = refl

module Ex₂ where

  -- e ∷= f + e | f
  -- f ∷= 0 | 0 * f | ( e )

  mutual

    expr   ~ factor ⊛> sym '+' ⊛> expr
           ∣ factor

    factor ~ sym '0'
           ∣ sym '0' ⊛> sym '*' ⊛> factor
           ∣ sym '(' ⊛> expr <⊛ sym ')'

  ex₁ : "(0*)" ∈? expr ≡ []
  ex₁ = refl

  ex₂ : "0*(0+0)" ∈? expr ≡ '0' ∷ []
  ex₂ = refl

{-
module Ex₃ where

  -- This is not allowed:

  -- e ∷= f + e | f
  -- f ∷= 0 | f * 0 | ( e )

  mutual

    expr   = factor ⊛> sym '+' ⊛> expr
           ∣ factor

    factor = sym '0'
           ∣ factor ⊛> sym '*' ⊛> sym '0'
           ∣ sym '(' ⊛> expr <⊛ sym ')'
-}

module Ex₄ where

  -- The language aⁿbⁿcⁿ, which is not context free.

  -- The non-terminal top returns the number of 'a' characters parsed.

  -- top     ∷= aⁿbⁿcⁿ
  -- as n    ∷= aˡ⁺¹bⁿ⁺ˡ⁺¹cⁿ⁺ˡ⁺¹
  -- bcs x n ∷= xⁿ⁺¹

  bcs : Char -> ℕ -> Parser Char _ ℕ
  bcs c zero    = sym c ⊛> return 0
  bcs c (suc n) = sym c ⊛> bcs c n

  as : ℕ -> Parser Char _ ℕ
  as n ~ suc <$ sym 'a' ⊛
         ( as (suc n)
         ∣ _+_ <$> bcs 'b' n ⊛ bcs 'c' n
         )

  top = return 0 ∣ as zero

  ex₁ : "aaabbbccc" ∈? top ≡ 3 ∷ []
  ex₁ = refl

  ex₂ : "aaabbccc" ∈? top ≡ []
  ex₂ = refl

module Ex₅ where

  -- A grammar making use of a parameterised parser from the library.

  a  = sym 'a'
  as = length <$> a ⋆

  ex₁ : "aaaaa" ∈? as ≡ 5 ∷ []
  ex₁ = refl

module Ex₆ where

  -- A grammar which uses the chain₁ combinator.

  op = _+_ <$ sym '+'
     ∣ _*_ <$ sym '*'
     ∣ _∸_ <$ sym '∸'

  expr : Assoc -> Parser Char _ ℕ
  expr a = chain₁ a number op

  ex₁ : "12345" ∈? number ≡ 12345 ∷ []
  ex₁ = refl

  ex₂ : "1+5*2∸3" ∈? expr left ≡ 9 ∷ []
  ex₂ = refl

  ex₃ : "1+5*2∸3" ∈? expr right ≡ 1 ∷ []
  ex₃ = refl

module Ex₇ where

  -- A proper expression example.

  addOp = _+_ <$ sym '+'
        ∣ _∸_ <$ sym '∸'
  mulOp = _*_ <$ sym '*'

  mutual

    expr   ~ chain₁ left term   addOp
    term   ~ chain₁ left factor mulOp
    factor ~ sym '(' ⊛> expr <⊛ sym ')'
           ∣ number

  ex₁ : "1+5*2∸3" ∈? expr ≡ 8 ∷ []
  ex₁ = refl

  ex₂ : "1+5*(2∸3)" ∈? expr ≡ 1 ∷ []
  ex₂ = refl

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- The debug output should include the text "Termination checking
-- mutual block MutId 0" once, not three times.

{-# OPTIONS -vterm.mutual.id:40 #-}

open import Agda.Builtin.Nat

record R : Set₁ where
  field
    A : Set

  f0 : Nat → Nat
  f0 zero    = zero
  f0 (suc n) = f0 n

  f1 : Nat → Nat
  f1 zero    = zero
  f1 (suc n) = f1 n

  f2 : Nat → Nat
  f2 zero    = zero
  f2 (suc n) = f2 n

-- Included in order to make the code fail to type-check.

Bad : Set
Bad = Set


text:
-- Andreas, 2013-11-07
-- Instance candidates are now considered modulo judgemental equality.

module Issue899 where

postulate
  A B : Set
  f : {{ x : A }} → B
  instance a : A

instance
  a' : A
  a' = a

test : B
test = f

{- The previous code fails with the following message:

  Resolve implicit argument _x_257 : A. Candidates: [a : A, a : A]

There are indeed two values in scope of type A (a and a'), but given
that they are definitionally equal, Agda should not complain about it
but just pick any one of them.  -}

-- Andreas, 2017-07-28: the other example now also works, thanks to G. Brunerie

record Eq (A : Set) : Set₁ where
  field
    _==_ : A → A → Set

record Ord (A : Set) : Set₁ where
  field
    {{eq}} : Eq A
    _<_ : A → A → Set

postulate
  N : Set
  eqN : N → N → Set
  ordN : N → N → Set

instance
  EqN : Eq N
  EqN = record {_==_ = eqN}

  OrdN : Ord N
  OrdN = record {_<_ = ordN}

  ordToEq : {A : Set} → Ord A → Eq A
  ordToEq o = Ord.eq o

postulate
  f2 : (A : Set) {{e : Eq A}} → Set → Set

test2 = f2 N N

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
variable
  X : Set

postulate
  foo : ∀ A -> X   -- error at `src/full/Agda/TypeChecking/Monad/MetaVars.hs:98`
                   -- expected: `{X : Set} -> _1 -> X`
  Y : Set
  bar : ∀ A -> Y   -- normal `_1 -> Y` type with unsolved metavar


text:
-- Andreas, 2012-09-15
-- Positive effects of making Agda recognize constant functions.
-- Arguments to constant functions are ignored in definitional equality.
{-# OPTIONS --copatterns #-}
module NonvariantPolarity where

open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where
  constructor trivial

data Bool : Set where
  true false : Bool

True : Bool → Set
True true  = ⊤
True false = ⊥

module IgnoreArg where

  -- A function ignoring its first argument
  knot : Bool → Bool → Bool
  knot x true  = false
  knot x false = true

  test : (y : Bool) → knot true y ≡ knot false y
  test y = refl

module UnusedModulePar where

  -- An unused module parameter
  module M (x : Bool) where

    not : Bool → Bool
    not true  = false
    not false = true

  open M true
  open M false renaming (not to not′)

  test : (y : Bool) → not y ≡ not′ y
  test y = refl

module Absurd where

  -- Absurd patterns do not count as matches; abort is constant in its 2nd arg.
  abort : (A : Set) → ⊥ → A
  abort A ()

  test : (x y : ⊥) → abort Bool x ≡ abort Bool y
  test x y = refl

module ProofIrrelevance where

  -- Record and absurd patterns do not count as match.
  fun : (b : Bool) → True b → Bool
  fun true  trivial = true
  fun false ()

  -- This gives us a kind of proof irrelevance.
  test : (b : Bool) → (x y : True b) → fun b x ≡ fun b y
  test b x y = refl

module CoinductiveUnit where

  record Unit : Set where
    coinductive
    constructor delay
    field force : Unit
  open Unit

  -- The identity on Unit does not match on its argument, so it is constant.
  id : Unit → Unit
  force (id x) = id (force x)

  idConst : (x y : Unit) → id x ≡ id y
  idConst x y = refl

  -- That does not imply x ≡ y (needs bisimulation).

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Issue3564-2 where

open import Issue3564


text:
-- Andreas, 2016-08-08, issue #2131 reported by Andrea

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

-- {-# OPTIONS --show-irrelevant #-}
-- {-# OPTIONS -v tc:25 #-}

postulate
  A : Set
  P : (F : .(U : Set) → Set) → Set

const : (X : Set) .(Y : Set) → Set
const X Y = X

works : (G : .(Z : Set) → Set) (p : P G) → P (λ V → const (G _) V) -- V is irrelevant
works G p = p

irr : (G : .(Z : Set) → Set) (p : P G) → P (const (G {!!}))
irr G p = p

-- Agda computes as follows:
--   P G =? P (const (G (?0 G p))) : Set
--   G =? const (G (?0 G p)) : .(U : Set) → Set
--   G U =? const (G (?0 G p)) U : Set
--   G U =? G (?0 G p)
--   ?0 G p := U
-- This assignment fails, since U is not in scope of ?0
-- However, since ?0 is in irrelevant context, this should not be
-- a definite failure, but leave the meta unsolved.


text:
module Lec5 where

open import Lec1Done
open import Lec2Done
open import Lec3Done

data List (X : Set) : Set where -- BUILTIN insists on level polymorphism
  []   : List X
  _,-_ : (x : X)(xs : List X) -> List X
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _,-_ #-}
{-# COMPILE GHC List = data [] ([] | (:)) #-}

list : {X Y : Set} -> (X -> Y) -> List X -> List Y
list f []         = []
list f (x ,- xs)  = f x ,- list f xs

data Two : Set where ff tt : Two
{-# BUILTIN BOOL Two #-}
{-# BUILTIN FALSE ff #-}
{-# BUILTIN TRUE tt #-}

----------------------------------------------------------------------------
-- chars and strings
----------------------------------------------------------------------------

postulate       -- this means that we just suppose the following things exist...
  Char : Set
  String : Set
{-# BUILTIN CHAR Char #-}
{-# BUILTIN STRING String #-}

primitive       -- these are baked in; they even work!
  primCharEquality    : Char -> Char -> Two
  primStringAppend    : String -> String -> String
  primStringToList    : String -> List Char
  primStringFromList  : List Char -> String

---------------------------------------------------------------------------
-- COLOURS
---------------------------------------------------------------------------

-- We're going to be making displays from coloured text.

data Colour : Set where
  black red green yellow blue magenta cyan white : Colour
{-# COMPILE GHC Colour = data HaskellSetup.Colour (HaskellSetup.Black | HaskellSetup.Red | HaskellSetup.Green | HaskellSetup.Yellow | HaskellSetup.Blue | HaskellSetup.Magenta | HaskellSetup.Cyan | HaskellSetup.White) #-}

record _**_ (S T : Set) : Set where
  constructor _,_
  field
    outl : S
    outr : T
open _**_
{-# COMPILE GHC _**_ = data (,) ((,)) #-}
infixr 4 _**_ _,_

{- Here's the characterization of keys I give you -}
data Direction : Set where up down left right : Direction
data Modifier : Set where normal shift control : Modifier
data Key : Set where
  char       : Char -> Key
  arrow      : Modifier -> Direction -> Key
  enter      : Key
  backspace  : Key
  delete     : Key
  escape     : Key
  tab        : Key
data Event : Set where
  key     : (k : Key) -> Event
  resize  : (w h : Nat) -> Event

{- This type collects the things you're allowed to do with the text window. -}
data Action : Set where
  goRowCol : Nat -> Nat -> Action    -- send the cursor somewhere
  sendText : List Char -> Action     -- send some text
  move     : Direction -> Nat -> Action  -- which way and how much
  fgText   : Colour -> Action
  bgText   : Colour -> Action

{- I wire all of that stuff up to its Haskell counterpart. -}
{-# FOREIGN GHC import qualified ANSIEscapes #-}
{-# FOREIGN GHC import qualified HaskellSetup #-}
{-# COMPILE GHC Direction = data ANSIEscapes.Dir (ANSIEscapes.DU | ANSIEscapes.DD | ANSIEscapes.DL | ANSIEscapes.DR) #-}
{-# COMPILE GHC Modifier = data HaskellSetup.Modifier (HaskellSetup.Normal | HaskellSetup.Shift | HaskellSetup.Control) #-}
{-# COMPILE GHC Key = data HaskellSetup.Key (HaskellSetup.Char | HaskellSetup.Arrow | HaskellSetup.Enter | HaskellSetup.Backspace | HaskellSetup.Delete | HaskellSetup.Escape | HaskellSetup.Tab) #-}
{-# COMPILE GHC Event = data HaskellSetup.Event (HaskellSetup.Key | HaskellSetup.Resize) #-}
{-# COMPILE GHC Action = data HaskellSetup.Action (HaskellSetup.GoRowCol | HaskellSetup.SendText | HaskellSetup.Move | HaskellSetup.FgText | HaskellSetup.BgText) #-}

data ColourChar : Set where
  _-_/_ : (fg : Colour)(c : Char)(bg : Colour) -> ColourChar

-- ... e.g.     green - '*' / black    for a green * on black.

Matrix : Set -> Nat * Nat -> Set
Matrix C (w , h) = Vec (Vec C w) h

Painting : Nat * Nat -> Set
Painting = Matrix ColourChar

vecFoldR : {X Y : Set} -> (X -> Y -> Y) -> Y -> {n : Nat} -> Vec X n -> Y
vecFoldR c n [] = n
vecFoldR c n (x ,- xs) = c x (vecFoldR c n xs)

paintAction : {wh : Nat * Nat} -> Matrix ColourChar wh -> List Action
paintAction = vecFoldR (vecFoldR (\ {(f - c / b) k -> \ as ->
  fgText f ,- bgText b ,- sendText (c ,- []) ,- k as}) id) []

postulate       -- Haskell has a monad for doing IO, which we use at the top level
  IO      : Set -> Set
  return  : {A : Set} -> A -> IO A
  _>>=_   : {A B : Set} -> IO A -> (A -> IO B) -> IO B
infixl 1 _>>=_
{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}
{-# COMPILE GHC return = (\ _ -> return) #-}
{-# COMPILE GHC _>>=_ = (\ _ _ -> (>>=)) #-}

---------------------------------------------------------------------------
-- APPLICATIONS                                                          --
---------------------------------------------------------------------------

-- Here's a general idea of what it means to be an "application".
-- You need to choose some sort of size-dependent state, then provide these
-- bits and pieces. We need to know how the state is updated according to
-- events, with resizing potentially affecting the state's type. We must
-- be able to paint the state. The state should propose a cursor position.
-- (Keen students may modify this definition to ensure the cursor must be
-- within the bounds of the application.)

record Application (wh : Nat * Nat) : Set where
  coinductive
  field
    handleKey     : Key -> Application wh
    handleResize  : (wh' : Nat * Nat) -> Application wh'
    paintMe       : Painting wh
    cursorMe      : Nat * Nat  -- x,y coords
open Application public

-- Now your turn. Build the appropriate handler to connect these
-- applications with mainAppLoop. Again, work in two stages, first
-- figuring out how to do the right actions, then managing the
-- state properly. (1 mark)

_+L_ : {X : Set} -> List X -> List X -> List X
[] +L ys = ys
(x ,- xs) +L ys = x ,- (xs +L ys)
infixr 3 _+L_

APP : Set
APP = Sg (Nat * Nat) Application

appPaint : APP -> List Action
appPaint (_ , app) =
  goRowCol 0 0 ,- paintAction p
     -- must have composition here, to work around compiler bug
     -- paintAction (paintMatrix p)
     -- segfaults, because p is erased
  +L (goRowCol (snd xy) (fst xy) ,- [])
  where
    p  = paintMe app
    xy = cursorMe app

appHandler : Event -> APP -> APP ** List Action
appHandler (key k) (wh , app) = app' , appPaint app'
  where
    app' : APP
    app' = _ , handleKey app k
appHandler (resize w h) (wh , app) = app' , appPaint app'
  where
    app' : APP
    app' = _ , handleResize app (w , h)

{- This is the bit of code I wrote in Haskell to animate your code. -}
postulate
  mainAppLoop : {S : Set} ->             -- program state
    -- INITIALIZER
    S ->                              -- initial state
    -- EVENT HANDLER
    (Event -> S ->                    -- event and state in
     S ** List Action) ->              -- new state and screen actions out
    -- PUT 'EM TOGETHER AND YOU'VE GOT AN APPLICATION!
    IO One
{-# COMPILE GHC mainAppLoop = (\ _ -> HaskellSetup.mainAppLoop) #-}

appMain : (forall wh -> Application wh) -> IO One
appMain app = mainAppLoop ((0 , 0) , app (0 , 0)) appHandler
  -- will get resized dynamically to size of terminal, first thing

vPure : {n : Nat}{X : Set} -> X -> Vec X n
vPure {zero} x = []
vPure {suc n} x = x ,- vPure x

rectApp : Char -> forall wh -> Application wh
handleKey (rectApp c wh) (char x) = rectApp x wh
handleKey (rectApp c wh) _ = rectApp c wh
handleResize (rectApp c _)  wh = rectApp c wh
paintMe      (rectApp c wh)    = vPure (vPure (green - c / black))
cursorMe     (rectApp c wh)    = wh

main : IO One
main = appMain (rectApp '*')

--  agda --compile --ghc-flag "-lncurses" Lec5.agda

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
open import Agda.Builtin.Size

postulate
  X : Set
  P : X → Set
  Q : (x : X) → P x → Set

data D (i : Size) : Set where
  c : D i

f : (i : Size) → D i → X
f i c = {!!}

g : (x : X) (y : P x) → Q x y → Q x y
g _ _ q = q

h : (i : Size) (n : D i) → P (f i n)
h _ c = {!!}

k : (n : D ∞) → Q (f ∞ n) (h ∞ n)
k _ = g _ (h _ {!!}) _