text:
module Data.Fin where

open import Data.Nat hiding (_==_; _<_)
open import Data.Bool
open import Logic.Identity
open import Logic.Base

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (suc n)
  fsuc  : {n : Nat} -> Fin n -> Fin (suc n)

pred : {n : Nat} -> Fin (suc (suc n)) -> Fin (suc n)
pred fzero    = fzero
pred (fsuc i) = i

fzero≠fsuc : {n : Nat}{i : Fin n} -> fzero ≢ fsuc i
fzero≠fsuc ()

fsuc-inj : {n : Nat}{i j : Fin n} -> fsuc i ≡ fsuc j -> i ≡ j
fsuc-inj refl = refl

_==_ : {n : Nat}(i j : Fin n) -> i ≡ j \/ i ≢ j
fzero  == fzero  = \/-IL refl
fzero  == fsuc j = \/-IR fzero≠fsuc
fsuc i == fzero  = \/-IR (sym≢ fzero≠fsuc)
fsuc i == fsuc j = aux i j (i == j)
  where
    aux : {n : Nat}(i j : Fin n) -> i ≡ j \/ i ≢ j -> fsuc i ≡ fsuc j \/ fsuc i ≢ fsuc j
    aux i .i (\/-IL refl) = \/-IL refl
    aux i j  (\/-IR i≠j)  = \/-IR \si=sj -> i≠j (fsuc-inj si=sj)

_<_ : {n : Nat} -> Fin n -> Fin n -> Bool
_      < fzero  = false
fzero  < fsuc j = true
fsuc i < fsuc j = i < j

fromNat : (n : Nat) -> Fin (suc n)
fromNat  zero	= fzero
fromNat (suc n) = fsuc (fromNat n)

liftSuc : {n : Nat} -> Fin n -> Fin (suc n)
liftSuc  fzero	 = fzero
liftSuc (fsuc i) = fsuc (liftSuc i)

lift+ : {n : Nat}(m : Nat) -> Fin n -> Fin (m + n)
lift+  zero   i = i
lift+ (suc m) i = liftSuc (lift+ m i)

thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
thin  fzero i	       = fsuc i
thin (fsuc j) fzero    = fzero
thin (fsuc j) (fsuc i) = fsuc (thin j i)

-- Two elements of Fin n are either the same or one is the thinning of
-- something with respect to the other.
data ThinView : {n : Nat}(i j : Fin n) -> Set where
  same : {n : Nat}{i : Fin n}		       -> ThinView i i
  diff : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> ThinView i (thin i j)

thinView : {n : Nat}(i j : Fin n) -> ThinView i j
thinView fzero fzero		      = same
thinView  fzero (fsuc j) = diff j
thinView {suc zero} (fsuc ()) fzero
thinView {suc (suc n)} (fsuc i) fzero	 = diff fzero
thinView (fsuc i) (fsuc j) = aux i j (thinView i j)
  where
    aux : {n : Nat}(i j : Fin n) -> ThinView i j -> ThinView (fsuc i) (fsuc j)
    aux i .i	       same    = same
    aux i .(thin i j) (diff j) = diff (fsuc j)

thin-ij≠i : {n : Nat}(i : Fin (suc n))(j : Fin n) -> thin i j ≢ i
thin-ij≠i  fzero    j	    ()
thin-ij≠i (fsuc i)  fzero   ()
thin-ij≠i (fsuc i) (fsuc j) eq = thin-ij≠i i j (fsuc-inj eq)

-- Thickening.
--    thin i (thick i j) ≡ j  ?
--    thick i (thin i j) ≡ j
thick : {n : Nat}(i j : Fin (suc n)) -> i ≢ j -> Fin n
thick i j i≠j = thick' i j i≠j (thinView i j) where
  thick' : {n : Nat}(i j : Fin (suc n)) -> i ≢ j -> ThinView i j -> Fin n
  thick' i .i	       i≠i same	   = elim-False (i≠i refl)
  thick' i .(thin i j) _  (diff j) = j

-- thin∘thick=id : {n : Nat}(i j : Fin (suc n))(p : i ≢ j) ->
-- 		thin i (thick i j p) ≡ j
-- thin∘thick=id i j p = ?
--
-- thick∘thin=id : {n : Nat}(i : Fin (suc n))(j : Fin n) ->
-- 		thick i (thin i j) (sym≢ (thin-ij≠i i j)) ≡ j
-- thick∘thin=id i j = ?
--

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- Andreas, 2016-09-12
--
-- Underscores should also get meaningful names
-- (not just metas from omitted hidden arguments)

-- {-# OPTIONS -v tc.meta.name:100 #-}

postulate
  F : (A : Set) → Set
  G : {B : Set} → Set

test1 : Set
test1 = F _
  -- name of this meta should be _A_0

test2 : Set
test2 = G
  -- creates meta _B_1

test3 : Set
test3 = G {_}
  -- name of this meta should be _B_2

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Primitive
open import Agda.Primitive.Cubical

record Wrap : Set (lsuc lzero) where
  field
    A : IUniv


text:
{-

Basic theory about h-levels/n-types:

- Basic properties of isContr, isProp and isSet (definitions are in Prelude)

- Hedberg's theorem can be found in Cubical/Relation/Nullary/DecidableEq

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.HLevels where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence using (ua ; univalence)

open import Cubical.Data.Sigma
open import Cubical.Data.Nat   using (ℕ; zero; suc; _+_; +-zero; +-comm)

HLevel : Type₀
HLevel = ℕ

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level
    A : Type ℓ
    B : A → Type ℓ
    C : (x : A) → B x → Type ℓ
    D : (x : A) (y : B x) → C x y → Type ℓ
    E : (x : A) (y : B x) → (z : C x y) → D x y z → Type ℓ
    x y : A
    n : HLevel

isOfHLevel : HLevel → Type ℓ → Type ℓ
isOfHLevel 0 A = isContr A
isOfHLevel 1 A = isProp A
isOfHLevel (suc (suc n)) A = (x y : A) → isOfHLevel (suc n) (x ≡ y)

isOfHLevelFun : (n : HLevel) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ')
isOfHLevelFun n f = ∀ b → isOfHLevel n (fiber f b)

TypeOfHLevel : ∀ ℓ → HLevel → Type (ℓ-suc ℓ)
TypeOfHLevel ℓ n = TypeWithStr ℓ (isOfHLevel n)

hProp hSet hGroupoid h2Groupoid : ∀ ℓ → Type (ℓ-suc ℓ)
hProp      ℓ = TypeOfHLevel ℓ 1
hSet       ℓ = TypeOfHLevel ℓ 2
hGroupoid  ℓ = TypeOfHLevel ℓ 3
h2Groupoid ℓ = TypeOfHLevel ℓ 4

-- lower h-levels imply higher h-levels

isOfHLevelSuc : (n : HLevel) → isOfHLevel n A → isOfHLevel (suc n) A
isOfHLevelSuc 0 = isContr→isProp
isOfHLevelSuc 1 = isProp→isSet
isOfHLevelSuc (suc (suc n)) h a b = isOfHLevelSuc (suc n) (h a b)

isSet→isGroupoid : isSet A → isGroupoid A
isSet→isGroupoid = isOfHLevelSuc 2

isGroupoid→is2Groupoid : isGroupoid A → is2Groupoid A
isGroupoid→is2Groupoid = isOfHLevelSuc 3

isOfHLevelPlus : (m : HLevel) → isOfHLevel n A → isOfHLevel (m + n) A
isOfHLevelPlus zero hA = hA
isOfHLevelPlus (suc m) hA = isOfHLevelSuc _ (isOfHLevelPlus m hA)

isContr→isOfHLevel : (n : HLevel) → isContr A → isOfHLevel n A
isContr→isOfHLevel {A = A} n cA = subst (λ m → isOfHLevel m A) (+-zero n) (isOfHLevelPlus n cA)

isProp→isOfHLevelSuc : (n : HLevel) → isProp A → isOfHLevel (suc n) A
isProp→isOfHLevelSuc {A = A} n pA = subst (λ m → isOfHLevel m A) (+-comm n 1) (isOfHLevelPlus n pA)

-- hlevel of path and dependent path types

isProp→isContrPath : isProp A → (x y : A) → isContr (x ≡ y)
isProp→isContrPath h x y = h x y , isProp→isSet h x y _

isContr→isContrPath : isContr A → (x y : A) → isContr (x ≡ y)
isContr→isContrPath cA = isProp→isContrPath (isContr→isProp cA)

isOfHLevelPath' : (n : HLevel) → isOfHLevel (suc n) A → (x y : A) → isOfHLevel n (x ≡ y)
isOfHLevelPath' 0 = isProp→isContrPath
isOfHLevelPath' (suc n) h x y = h x y

isOfHLevelPath'⁻ : (n : HLevel) → ((x y : A) → isOfHLevel n (x ≡ y)) → isOfHLevel (suc n) A
isOfHLevelPath'⁻ zero h x y = h x y .fst
isOfHLevelPath'⁻ (suc n) h = h

isOfHLevelPath : (n : HLevel) → isOfHLevel n A → (x y : A) → isOfHLevel n (x ≡ y)
isOfHLevelPath 0 h x y = isContr→isContrPath h x y
isOfHLevelPath (suc n) h x y = isOfHLevelSuc n (isOfHLevelPath' n h x y)

isOfHLevelPathP' : {A : I → Type ℓ} (n : HLevel)
                   → isOfHLevel (suc n) (A i1)
                   → (x : A i0) (y : A i1) → isOfHLevel n (PathP A x y)
isOfHLevelPathP' {A = A} n h x y = transport⁻ (λ i → isOfHLevel n (PathP≡Path A x y i))
                                              (isOfHLevelPath' n h _ _)

isOfHLevelPathP : {A : I → Type ℓ} (n : HLevel)
                  → isOfHLevel n (A i1)
                  → (x : A i0) (y : A i1) → isOfHLevel n (PathP A x y)
isOfHLevelPathP {A = A} n h x y = transport⁻ (λ i → isOfHLevel n (PathP≡Path A x y i))
                                             (isOfHLevelPath n h _ _)

isProp→isContrPathP : {A : I → Type ℓ} → (∀ i → isProp (A i))
                                       → (x : A i0) (y : A i1) → isContr (PathP A x y)
isProp→isContrPathP h x y = isProp→PathP h x y , isOfHLevelPathP 1 (h i1) x y _

-- h-level of isOfHLevel

isPropIsOfHLevel : (n : HLevel) → isProp (isOfHLevel n A)
isPropIsOfHLevel 0 = isPropIsContr
isPropIsOfHLevel 1 = isPropIsProp
isPropIsOfHLevel (suc (suc n)) f g i a b =
  isPropIsOfHLevel (suc n) (f a b) (g a b) i

isPropIsSet : isProp (isSet A)
isPropIsSet = isPropIsOfHLevel 2

isPropIsGroupoid : isProp (isGroupoid A)
isPropIsGroupoid = isPropIsOfHLevel 3

isPropIs2Groupoid : isProp (is2Groupoid A)
isPropIs2Groupoid = isPropIsOfHLevel 4

-- Fillers for cubes from h-level

isSet→isSet' : isSet A → isSet' A
isSet→isSet' {A = A} Aset a₀₋ a₁₋ a₋₀ a₋₁ =
  transport⁻ (PathP≡Path (λ i → a₋₀ i ≡ a₋₁ i) a₀₋ a₁₋) (Aset _ _ _ _)

isSet'→isSet : isSet' A → isSet A
isSet'→isSet {A = A} Aset' x y p q = Aset' p q refl refl

isGroupoid→isGroupoid' : isGroupoid A → isGroupoid' A
isGroupoid→isGroupoid' {A = A} Agpd a₀₋₋ a₁₋₋ a₋₀₋ a₋₁₋ a₋₋₀ a₋₋₁ =
  transport⁻ (PathP≡Path (λ i → Square (a₋₀₋ i) (a₋₁₋ i) (a₋₋₀ i) (a₋₋₁ i)) a₀₋₋ a₁₋₋)
    (isGroupoid→isPropSquare _ _ _ _ _ _)
  where
  isGroupoid→isPropSquare :
    {a₀₀ a₀₁ : A} (a₀₋ : a₀₀ ≡ a₀₁)
    {a₁₀ a₁₁ : A} (a₁₋ : a₁₀ ≡ a₁₁)
    (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁)
    → isProp (Square a₀₋ a₁₋ a₋₀ a₋₁)
  isGroupoid→isPropSquare a₀₋ a₁₋ a₋₀ a₋₁ =
    transport⁻
      (cong isProp (PathP≡Path (λ i → a₋₀ i ≡ a₋₁ i) a₀₋ a₁₋))
      (Agpd _ _ _ _)

isGroupoid'→isGroupoid : isGroupoid' A → isGroupoid A
isGroupoid'→isGroupoid Agpd' x y p q r s = Agpd' r s refl refl refl refl

-- hlevels are preserved by retracts (and consequently equivalences)

isContrRetract
  : ∀ {B : Type ℓ}
  → (f : A → B) (g : B → A)
  → (h : retract f g)
  → (v : isContr B) → isContr A
isContrRetract f g h (b , p) = (g b , λ x → (cong g (p (f x))) ∙ (h x))

isPropRetract
  : {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isProp B → isProp A
isPropRetract f g h p x y i =
  hcomp
    (λ j → λ
      { (i = i0) → h x j
      ; (i = i1) → h y j})
    (g (p (f x) (f y) i))

isOfHLevelRetract
  : (n : HLevel) {B : Type ℓ}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isOfHLevel n B → isOfHLevel n A
isOfHLevelRetract 0 = isContrRetract
isOfHLevelRetract 1 = isPropRetract
isOfHLevelRetract (suc (suc n)) f g h ofLevel x y =
  isOfHLevelRetract (suc n)
    (cong f)
    (λ q i →
      hcomp
        (λ j → λ
          { (i = i0) → h x j
          ; (i = i1) → h y j})
        (g (q i)))
    (λ p k i →
      hcomp
        (λ j → λ
          { (i = i0) → h x (j ∨ k)
          ; (i = i1) → h y (j ∨ k)
          ; (k = i1) → p i})
        (h (p i) k))
    (ofLevel (f x) (f y))

isOfHLevelRespectEquiv : {A : Type ℓ} {B : Type ℓ'} → (n : HLevel) → A ≃ B → isOfHLevel n A → isOfHLevel n B
isOfHLevelRespectEquiv n eq = isOfHLevelRetract n (invEq eq) (eq .fst) (retEq eq)

-- h-level of Σ-types

isContrΣ : isContr A → ((x : A) → isContr (B x)) → isContr (Σ A B)
isContrΣ {A = A} {B = B} (a , p) q =
  let h : (x : A) (y : B x) → (q x) .fst ≡ y
      h x y = (q x) .snd y
  in (( a , q a .fst)
     , ( λ x i → p (x .fst) i
       , h (p (x .fst) i) (transp (λ j → B (p (x .fst) (i ∨ ~ j))) i (x .snd)) i))

isContrΣ′ : (ca : isContr A) → isContr (B (fst ca)) → isContr (Σ A B)
isContrΣ′ ca cb = isContrΣ ca (λ x → subst _ (snd ca x) cb)

Σ≡Prop-equiv
  : (pB : (x : A) → isProp (B x)) {u v : Σ[ a ∈ A ] B a}
  → isEquiv (Σ≡Prop pB {u} {v})
Σ≡Prop-equiv {A = A} pB {u} {v} = isoToIsEquiv (iso (Σ≡Prop pB) (cong fst) sq (λ _ → refl))
  where sq : (p : u ≡ v) → Σ≡Prop pB (cong fst p) ≡ p
        sq p j i = (p i .fst) , isProp→PathP (λ i → isOfHLevelPath 1 (pB (fst (p i)))
                                                       (Σ≡Prop pB {u} {v} (cong fst p) i .snd)
                                                       (p i .snd) )
                                              refl refl i j

isPropΣ : isProp A → ((x : A) → isProp (B x)) → isProp (Σ A B)
isPropΣ pA pB t u = Σ≡Prop pB (pA (t .fst) (u .fst))

isOfHLevelΣ : ∀ n → isOfHLevel n A → ((x : A) → isOfHLevel n (B x))
                  → isOfHLevel n (Σ A B)
isOfHLevelΣ 0 = isContrΣ
isOfHLevelΣ 1 = isPropΣ
isOfHLevelΣ {B = B} (suc (suc n)) h1 h2 x y =
  let h3 : isOfHLevel (suc n) (ΣPathTransport x y)
      h3 = isOfHLevelΣ (suc n) (h1 (fst x) (fst y)) λ p → h2 (p i1)
                       (subst B p (snd x)) (snd y)
  in transport (λ i → isOfHLevel (suc n) (ΣPathTransport≡PathΣ x y i)) h3

isSetΣ : isSet A → ((x : A) → isSet (B x)) → isSet (Σ A B)
isSetΣ = isOfHLevelΣ 2

isGroupoidΣ : isGroupoid A → ((x : A) → isGroupoid (B x)) → isGroupoid (Σ A B)
isGroupoidΣ = isOfHLevelΣ 3

is2GroupoidΣ : is2Groupoid A → ((x : A) → is2Groupoid (B x)) → is2Groupoid (Σ A B)
is2GroupoidΣ = isOfHLevelΣ 4

-- h-level of ×

isProp× : {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → isProp (A × B)
isProp× pA pB = isPropΣ pA (λ _ → pB)

isProp×2 : {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         → isProp A → isProp B → isProp C → isProp (A × B × C)
isProp×2 pA pB pC = isProp× pA (isProp× pB pC)

isProp×3 : {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
         → isProp A → isProp B → isProp C → isProp D → isProp (A × B × C × D)
isProp×3 pA pB pC pD = isProp×2 pA pB (isProp× pC pD)

isOfHLevel× : ∀ {A : Type ℓ} {B : Type ℓ'} n → isOfHLevel n A → isOfHLevel n B
                                             → isOfHLevel n (A × B)
isOfHLevel× n hA hB = isOfHLevelΣ n hA (λ _ → hB)

isSet× : ∀ {A : Type ℓ} {B : Type ℓ'} → isSet A → isSet B → isSet (A × B)
isSet× = isOfHLevel× 2

isGroupoid× : ∀ {A : Type ℓ} {B : Type ℓ'} → isGroupoid A → isGroupoid B
                                           → isGroupoid (A × B)
isGroupoid× = isOfHLevel× 3

is2Groupoid× : ∀ {A : Type ℓ} {B : Type ℓ'} → is2Groupoid A → is2Groupoid B
                                            → is2Groupoid (A × B)
is2Groupoid× = isOfHLevel× 4

-- h-level of Π-types

isOfHLevelΠ : ∀ n → ((x : A) → isOfHLevel n (B x))
                  → isOfHLevel n ((x : A) → B x)
isOfHLevelΠ 0 h = (λ x → fst (h x)) , λ f i y → snd (h y) (f y) i
isOfHLevelΠ 1 h f g i x = (h x) (f x) (g x) i
isOfHLevelΠ (suc (suc n)) h f g =
  subst (isOfHLevel (suc n)) funExtPath (isOfHLevelΠ (suc n) λ x → h x (f x) (g x))

isPropΠ : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
isPropΠ = isOfHLevelΠ 1

isPropΠ2 : (h : (x : A) (y : B x) → isProp (C x y))
         → isProp ((x : A) (y : B x) → C x y)
isPropΠ2 h = isPropΠ λ x → isPropΠ λ y → h x y

isPropΠ3 : (h : (x : A) (y : B x) (z : C x y) → isProp (D x y z))
         → isProp ((x : A) (y : B x) (z : C x y) → D x y z)
isPropΠ3 h = isPropΠ λ x → isPropΠ λ y → isPropΠ λ z → h x y z

isPropΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isProp (E x y z w))
            → isProp ((x : A) (y : B x) (z : C x y) (w : D x y z) → E x y z w)
isPropΠ4 h = isPropΠ λ _ → isPropΠ3 λ _ → h _ _

isPropImplicitΠ : (h : (x : A) → isProp (B x)) → isProp ({x : A} → B x)
isPropImplicitΠ h f g i {x} = h x (f {x}) (g {x}) i

isProp→ : {A : Type ℓ} {B : Type ℓ'} → isProp B → isProp (A → B)
isProp→ pB = isPropΠ λ _ → pB

isSetΠ : ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
isSetΠ = isOfHLevelΠ 2

isSetΠ2 : (h : (x : A) (y : B x) → isSet (C x y))
        → isSet ((x : A) (y : B x) → C x y)
isSetΠ2 h = isSetΠ λ x → isSetΠ λ y → h x y

isGroupoidΠ : ((x : A) → isGroupoid (B x)) → isGroupoid ((x : A) → B x)
isGroupoidΠ = isOfHLevelΠ 3

isGroupoidΠ2 : (h : (x : A) (y : B x) → isGroupoid (C x y)) → isGroupoid ((x : A) (y : B x) → C x y)
isGroupoidΠ2 h = isGroupoidΠ λ _ → isGroupoidΠ λ _ → h _ _

isGroupoidΠ3 : (h : (x : A) (y : B x) (z : C x y) → isGroupoid (D x y z))
            → isGroupoid ((x : A) (y : B x) (z : C x y) → D x y z)
isGroupoidΠ3 h = isGroupoidΠ λ _ → isGroupoidΠ2 λ _ → h _ _

isGroupoidΠ4 : (h : (x : A) (y : B x) (z : C x y) (w : D x y z) → isGroupoid (E x y z w))
            → isGroupoid ((x : A) (y : B x) (z : C x y) (w : D x y z) → E x y z w)
isGroupoidΠ4 h = isGroupoidΠ λ _ → isGroupoidΠ3 λ _ → h _ _

is2GroupoidΠ : ((x : A) → is2Groupoid (B x)) → is2Groupoid ((x : A) → B x)
is2GroupoidΠ = isOfHLevelΠ 4

isOfHLevelΠ⁻ : ∀ {A : Type ℓ} {B : Type ℓ'} n
             → isOfHLevel n (A → B) → (A → isOfHLevel n B)
isOfHLevelΠ⁻ 0 h x = fst h x , λ y → funExt⁻ (snd h (const y)) x
isOfHLevelΠ⁻ 1 h x y z = funExt⁻ (h (const y) (const z)) x
isOfHLevelΠ⁻ (suc (suc n)) h x y z =
  isOfHLevelΠ⁻ (suc n) (subst (isOfHLevel (suc n)) (sym funExtPath) (h (const y) (const z))) x

-- h-level of A ≃ B and A ≡ B

isOfHLevel≃ : ∀ n → {A B : Type ℓ} (hA : isOfHLevel n A) (hB : isOfHLevel n B) → isOfHLevel n (A ≃ B)
isOfHLevel≃ zero {A = A} {B = B} hA hB = A≃B , contr
  where
  A≃B : A ≃ B
  A≃B = isoToEquiv (iso (λ _ → fst hB) (λ _ → fst hA) (snd hB ) (snd hA))

  contr : (y : A ≃ B) → A≃B ≡ y
  contr y = Σ≡Prop isPropIsEquiv (funExt (λ a → snd hB (fst y a)))

isOfHLevel≃ (suc n) hA hB =
  isOfHLevelΣ (suc n) (isOfHLevelΠ (suc n) (λ _ → hB))
              (λ a → subst (λ n → isOfHLevel n (isEquiv a)) (+-comm n 1) (isOfHLevelPlus n (isPropIsEquiv a)))

isOfHLevel≡ : ∀ n → {A B : Type ℓ} (hA : isOfHLevel n A) (hB : isOfHLevel n B) →
  isOfHLevel n (A ≡ B)
isOfHLevel≡ n hA hB = isOfHLevelRespectEquiv n (invEquiv univalence) (isOfHLevel≃ n hA hB)

-- h-level of TypeOfHLevel

isPropHContr : isProp (TypeOfHLevel ℓ 0)
isPropHContr x y = Σ≡Prop (λ _ → isPropIsContr) (isOfHLevel≡ 0 (x .snd) (y .snd) .fst)

isOfHLevelTypeOfHLevel : ∀ n → isOfHLevel (suc n) (TypeOfHLevel ℓ n)
isOfHLevelTypeOfHLevel 0 = isPropHContr
isOfHLevelTypeOfHLevel (suc n) x y = subst (isOfHLevel (suc n)) eq (isOfHLevel≡ (suc n) (snd x) (snd y))
  where eq : ∀ {A B : Type ℓ} {hA : isOfHLevel (suc n) A} {hB : isOfHLevel (suc n) B}
             → (A ≡ B) ≡ ((A , hA) ≡ (B , hB))
        eq = ua (_ , Σ≡Prop-equiv (λ _ → isPropIsOfHLevel (suc n)))

isSetHProp : isSet (hProp ℓ)
isSetHProp = isOfHLevelTypeOfHLevel 1

-- h-level of lifted type

isOfHLevelLift : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A)
isOfHLevelLift n = isOfHLevelRetract n lower lift λ _ → refl

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

-- More consequences of isProp and isContr

inhProp→isContr : A → isProp A → isContr A
inhProp→isContr x h = x , h x

extend : isContr A → (∀ φ → (u : Partial φ A) → Sub A φ u)
extend (x , p) φ u = inS (hcomp (λ { j (φ = i1) → p (u 1=1) j }) x)

isContrPartial→isContr : ∀ {ℓ} {A : Type ℓ}
                       → (extend : ∀ φ → Partial φ A → A)
                       → (∀ u → u ≡ (extend i1 λ { _ → u}))
                       → isContr A
isContrPartial→isContr {A = A} extend law
  = ex , λ y → law ex ∙ (λ i → Aux.v y i) ∙ sym (law y)
    where ex = extend i0 empty
          module Aux (y : A) (i : I) where
            φ = ~ i ∨ i
            u : Partial φ A
            u = λ { (i = i0) → ex ; (i = i1) → y }
            v = extend φ u

-- Dependent h-level over a type

isOfHLevelDep : HLevel → {A : Type ℓ} (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
isOfHLevelDep 0 {A = A} B = {a : A} → Σ[ b ∈ B a ] ({a' : A} (b' : B a') (p : a ≡ a') → PathP (λ i → B (p i)) b b')
isOfHLevelDep 1 {A = A} B = {a0 a1 : A} (b0 : B a0) (b1 : B a1) (p : a0 ≡ a1)  → PathP (λ i → B (p i)) b0 b1
isOfHLevelDep (suc (suc  n)) {A = A} B = {a0 a1 : A} (b0 : B a0) (b1 : B a1) → isOfHLevelDep (suc n) {A = a0 ≡ a1} (λ p → PathP (λ i → B (p i)) b0 b1)

isOfHLevel→isOfHLevelDep : (n : HLevel)
  → {A : Type ℓ} {B : A → Type ℓ'} (h : (a : A) → isOfHLevel n (B a)) → isOfHLevelDep n {A = A} B
isOfHLevel→isOfHLevelDep 0 h {a} =
  (h a .fst , λ b' p → isProp→PathP (λ i → isContr→isProp (h (p i))) (h a .fst) b')
isOfHLevel→isOfHLevelDep 1 h = λ b0 b1 p → isProp→PathP (λ i → h (p i)) b0 b1
isOfHLevel→isOfHLevelDep (suc (suc n)) {A = A} {B} h {a0} {a1} b0 b1 =
  isOfHLevel→isOfHLevelDep (suc n) (λ p → helper a1 p b1)
  where
  helper : (a1 : A) (p : a0 ≡ a1) (b1 : B a1) →
    isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1)
  helper a1 p b1 = J
                     (λ a1 p → ∀ b1 → isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1))
                     (λ _ → h _ _ _) p b1

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
-- Andreas, 2017-03-10, issue #2493, reported by nad
-- {-# OPTIONS -v tc.meta.assign:10 -v tc.size:90 -v tc:30 #-}

A : Set
A = {!!}

P : A → Set
P = {!λ _ → ?!}  -- give

-- Giving this made Agda loop as it solved ?0 := A.
-- Solution: don't assign metas during CheckInternal!


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 Haskell.Modules.RWS.RustAnyHow
import      LibraBFT.Impl.Consensus.BlockStorage.BlockRetriever     as BlockRetriever
import      LibraBFT.Impl.Consensus.BlockStorage.BlockStore         as BlockStore
import      LibraBFT.Impl.Consensus.BlockStorage.BlockTree          as BlockTree
import      LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-1 as ECP-LBFT-OBM-Diff-1
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote             as Vote
import      LibraBFT.Impl.Consensus.PersistentLivenessStorage       as PersistentLivenessStorage
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Hash
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                             using (String)

module LibraBFT.Impl.Consensus.BlockStorage.SyncManager where

data NeedFetchResult : Set where
  QCRoundBeforeRoot QCAlreadyExist QCBlockExist NeedFetch : NeedFetchResult

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

fastForwardSyncM         : QuorumCert → BlockRetriever → LBFT (Either ErrLog RecoveryData)
fetchQuorumCertM         : QuorumCert → BlockRetriever → LBFT (Either ErrLog Unit)
insertQuorumCertM        : QuorumCert → BlockRetriever → LBFT (Either ErrLog Unit)
syncToHighestCommitCertM : QuorumCert → BlockRetriever → LBFT (Either ErrLog Unit)

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

needSyncForQuorumCert : QuorumCert → BlockStore → Either ErrLog Bool
needSyncForQuorumCert qc bs = maybeS (bs ^∙ bsRoot) (Left fakeErr) {-bsRootErrL here-} $ λ btr → Right
  (not (  BlockStore.blockExists (qc ^∙ qcCommitInfo ∙ biId) bs
        ∨ ⌊ btr ^∙ ebRound ≥?ℕ qc ^∙ qcCommitInfo ∙ biRound ⌋ ))
 where
  here' : List String → List String
  here' t = "SyncManager" ∷ "needSyncForQuorumCert" ∷ t

needFetchForQuorumCert : QuorumCert → BlockStore → Either ErrLog NeedFetchResult
needFetchForQuorumCert qc bs = maybeS (bs ^∙ bsRoot) (Left fakeErr) {-bsRootErrL here-} $ λ btr →
 grd‖ qc ^∙ qcCertifiedBlock ∙ biRound <?ℕ btr ^∙ ebRound                           ≔
      Right QCRoundBeforeRoot
    ‖ is-just (BlockStore.getQuorumCertForBlock (qc ^∙ qcCertifiedBlock ∙ biId) bs) ≔
      Right QCAlreadyExist
    ‖ BlockStore.blockExists (qc ^∙ qcCertifiedBlock ∙ biId) bs                     ≔
      Right QCBlockExist
    ‖ otherwise≔
      Right NeedFetch
 where
  here' : List String → List String
  here' t = "SyncManager" ∷ "needFetchForQuorumCert" ∷ t

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

addCertsM : SyncInfo → BlockRetriever → LBFT (Either ErrLog Unit)
addCertsM {-reason-} syncInfo retriever =
  syncToHighestCommitCertM     (syncInfo ^∙ siHighestCommitCert) retriever ∙?∙ \_ ->
  insertQuorumCertM {-reason-} (syncInfo ^∙ siHighestCommitCert) retriever ∙?∙ \_ ->
  insertQuorumCertM {-reason-} (syncInfo ^∙ siHighestQuorumCert) retriever ∙?∙ \_ ->
  maybeSD                      (syncInfo ^∙ siHighestTimeoutCert) (ok unit) $
    \tc -> BlockStore.insertTimeoutCertificateM tc

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

module insertQuorumCertM (qc : QuorumCert) (retriever : BlockRetriever) where
  step₀ :                            LBFT (Either ErrLog Unit)
  step₁ : BlockStore               → LBFT (Either ErrLog Unit)
  step₁-else :                       LBFT (Either ErrLog Unit)
  step₂ : ExecutedBlock            → LBFT (Either ErrLog Unit)
  step₃ : LedgerInfoWithSignatures → LBFT (Either ErrLog Unit)

  step₀ = do
    bs ← use lBlockStore
    _ ← case⊎D needFetchForQuorumCert qc bs of λ where
      (Left e) →
        bail e
      (Right NeedFetch) →
        fetchQuorumCertM qc retriever
        ∙^∙ withErrCtx ("" ∷ [])
      (Right QCBlockExist) →
        BlockStore.insertSingleQuorumCertM qc ∙^∙ withErrCtx ("" ∷ []) ∙?∙ λ _ → do
        use lBlockStore >>= const (logInfo fakeInfo) -- InfoBlockStoreShort (here [lsQC qc])
        ok unit
      (Right _) →
        ok unit
    step₁ bs

  step₁ bs = do
    maybeSD (bs ^∙ bsRoot) (bail fakeErr) $ λ bsr →
      ifD (bsr ^∙ ebRound) <?ℕ (qc ^∙ qcCommitInfo ∙ biRound)
        then step₂ bsr
        else
          step₁-else

  step₂ bsr = do
          let finalityProof = qc ^∙ qcLedgerInfo
          BlockStore.commitM finalityProof ∙?∙ λ xx →
            step₃ finalityProof

  step₃ finalityProof = do
            ifD qc ^∙ qcEndsEpoch
              then ECP-LBFT-OBM-Diff-1.e_SyncManager_insertQuorumCertM_commit finalityProof
              else ok unit

  step₁-else =
          ok unit

insertQuorumCertM = insertQuorumCertM.step₀

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

loop1     : BlockRetriever → List Block → QuorumCert → LBFT (Either ErrLog (List Block))
loop2     : List Block → LBFT (Either ErrLog Unit)
hereFQCM' : List String → List String

fetchQuorumCertM qc retriever =
  loop1 retriever [] qc ∙?∙ loop2

-- TODO-1 PROVE IT TERMINATES
{-# TERMINATING #-}
loop1 retriever pending retrieveQC = do
    bs ← use lBlockStore
    ifD (BlockStore.blockExists (retrieveQC ^∙ qcCertifiedBlock ∙ biId) bs)
      then ok pending
      else
        BlockRetriever.retrieveBlockForQCM retriever retrieveQC 1
          ∙^∙ withErrCtx (hereFQCM' ("loop1" ∷ [])) ∙?∙ λ where
            (block ∷ []) → loop1 retriever (block ∷ pending) (block ^∙ bQuorumCert)
            (_ ∷ _ ∷ _)  → errorCase
            []           → errorCase
 where
  errorCase : LBFT (Either ErrLog (List Block))
  errorCase = do
              -- let msg = here ["loop1", "retrieveBlockForQCM returned more than asked for"]
              -- logErrExit msg
              bail fakeErr -- (ErrL msg)

loop2 = λ where
    [] -> ok unit
    (block ∷ bs) →
      BlockStore.insertSingleQuorumCertM (block ^∙ bQuorumCert)
        ∙^∙ withErrCtx (hereFQCM' ("loop2" ∷ [])) ∙?∙ \_ ->
          BlockStore.executeAndInsertBlockM block ∙?∙ \_ ->
            loop2 bs

hereFQCM' t = "SyncManager" ∷ "fetchQuorumCertM" ∷ t

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

syncToHighestCommitCertM highestCommitCert retriever = do
  bs ← use lBlockStore
  eitherSD (needSyncForQuorumCert highestCommitCert bs) bail $ λ b →
    if not b
      then ok unit
      else
        fastForwardSyncM highestCommitCert retriever ∙?∙ \rd -> do
          logInfo fakeInfo -- (here ["fastForwardSyncM success", lsRD rd])
          BlockStore.rebuildM (rd ^∙ rdRoot) (rd ^∙ rdRootMetadata) (rd ^∙ rdBlocks) (rd ^∙ rdQuorumCerts)
            ∙^∙ withErrCtx (here' []) ∙?∙ λ _ -> do
            whenD (highestCommitCert ^∙ qcEndsEpoch) $ do
              me ← use (lRoundManager ∙ rmObmMe)
              -- TODO-1 : Epoch Change Proof
              -- let ecp = EpochChangeProof ∙ new [highestCommitCert ^∙ qcLedgerInfo] False
              logInfo fakeInfo -- (here ["fastForwardSyncM detected an EpochChange"])
              -- TODO-1 : uncomment this and remove pure unit when Epoch Change supported
              -- act (BroadcastEpochChangeProof lEC ecp (mkNodesInOrder1 me))
              pure unit
            ok unit
 where
  here' : List String → List String
  here' t = "SyncManager" ∷ "syncToHighestCommitCertM" ∷ t

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

fastForwardSyncM highestCommitCert retriever = do
  logInfo fakeInfo -- (here' [ "start state sync with peer", lsA (retriever^.brPreferredPeer)
                   --        , "to block", lsBI (highestCommitCert^.qcCommitInfo) ])
  BlockRetriever.retrieveBlockForQCM retriever highestCommitCert 3 ∙?∙ λ where
    blocks@(_ ∷ _ ∷ i ∷ []) ->
      if highestCommitCert ^∙ qcCommitInfo ∙ biId /= i ^∙ bId
      then bail fakeErr -- (here' [ "should have a 3-chain"
                        --        , lsHV (highestCommitCert^.qcCommitInfo.biId), lsHV (i^.bId) ]))
      else continue blocks
    x -> bail fakeErr -- (here' ["incorrect number of blocks returned", show (length x)]))

 where

  here' : List String → List String

  zipWithNatsFrom : {A : Set} → ℕ → List A → List (ℕ × A)
  zipWithNatsFrom n = λ where
    [] → []
    (x ∷ xs) → (n , x) ∷ zipWithNatsFrom (n + 1) xs

  checkBlocksMatchQCs : List QuorumCert → List (ℕ × Block) → LBFT (Either ErrLog Unit)

  continue : List Block → LBFT (Either ErrLog RecoveryData)
  continue blocks = do
    logInfo fakeInfo -- (here' (["received blocks"] <> fmap (lsHV . (^.bId)) blocks))
    let quorumCerts = highestCommitCert ∷ fmap (_^∙ bQuorumCert) blocks
    logInfo fakeInfo -- (here' (["quorumCerts"]     <> fmap (lsHV . (^.qcCommitInfo.biId)) quorumCerts))
    checkBlocksMatchQCs quorumCerts (zipWithNatsFrom 0 blocks)  ∙?∙ λ _ →
      PersistentLivenessStorage.saveTreeM blocks quorumCerts ∙?∙ λ _ → do
        -- TODO-1 : requires adding bsStorage to BlockStore
        -- use (lBlockStore ∙ bsStorage) >>= λ x → logInfo fakeInfo -- (here' ["XXX", lsPLS x])
        -- OBM NOT NEEDED: state_computer.sync_to
        -- This returns recovery data
        PersistentLivenessStorage.startM ∙^∙ withErrCtx (here' [])

  checkBlocksMatchQCs quorumCerts = λ where
    []                 → ok unit
    ((i , block) ∷ xs) →
      maybeSD (quorumCerts !? i)
                  (bail fakeErr) -- (here' ["checkBlocksMatchQCs", "!?"])
                  $ λ qc →
      ifD (block ^∙ bId /= qc ^∙ qcCertifiedBlock ∙ biId)
      then (do
        logInfo fakeInfo -- [lsHV (block^.bId), lsB block]
        logInfo fakeInfo -- [lsHV (quorumCerts Prelude.!! i ^.qcCertifiedBlock.biId)
                         -- ,lsQC (quorumCerts Prelude.!! i)]
        bail fakeErr) -- (here' ("checkBlocksMatchQCs" ∷ "/=" ∷ []))
      else checkBlocksMatchQCs quorumCerts xs

  here' t = "SyncManager" ∷ "fastForwardSyncM" ∷ t


text:
open import Prelude

module Implicits.Oliveira.Deterministic.Decidable where

open import Data.Fin.Substitution
open import Implicits.Oliveira.Types
open import Implicits.Oliveira.Terms
open import Implicits.Oliveira.Contexts
open import Implicits.Oliveira.Substitutions
open import Implicits.Oliveira.Substitutions.Lemmas
open import Implicits.Oliveira.Deterministic.Resolution
open import Implicits.Oliveira.Types.Unification
open import Data.Star hiding (map)

MICtx : ℕ → ℕ → Set
MICtx m ν = List (MetaType m ν)

private
  module M = MetaTypeMetaSubst
  module T = MetaTypeTypeSubst

{-
{-# NO_TERMINATION_CHECK #-}
_,_amatch_ : ∀ {m ν} → (MetaType m ν) → (ρs : MICtx m ν) → (τ : SimpleType ν) → Maybe (ICtx ν)
(a ⇒ b) , ρs amatch τ = b , a List.∷ ρs amatch τ
∀' x , ρs amatch τ = open-meta x , (List.map meta-weaken ρs) amatch τ
(simpl x) , ρs amatch τ with mgu (simpl x) τ
(simpl x) , ρs amatch τ | just (u , proj₂) =
  just $ List.map (λ r → from-meta $ substitute (asub u) r) ρs
(simpl x) , ρs amatch τ | nothing = nothing

_match_ : ∀ {ν} → (Type ν) → (SimpleType ν) → Maybe (ICtx ν)
r match a = (to-meta {zero} r) , List.[] amatch a

{-# NO_TERMINATION_CHECK #-}
lem-a6 : ∀ {m ν} {ρs ρs'} (a : MetaType m ν) (τ : SimpleType ν) → a , ρs amatch τ ≡ just ρs' →
  (∃ λ (u : AList ν m zero) → (from-meta $ substitute (asub u) a) ◁ τ)
lem-a6 {ρs = ρs} (a ⇒ b) τ m
  with _,_amatch_ b (a List.∷ ρs) τ | inspect (_,_amatch_ b (a List.∷ ρs)) τ
lem-a6 (a ⇒ b) τ refl | ._ | reveal[ eq ] with lem-a6 b τ eq
lem-a6 (a ⇒ b) τ refl | ._ | reveal[ eq ] | u , b/u◁τ = u , (m-iabs b/u◁τ)
lem-a6 {ρs = ρs} (∀' a) τ m
  with open-meta a , (List.map meta-weaken ρs) amatch τ | inspect (_,_amatch_ (open-meta a) (List.map meta-weaken ρs)) τ
lem-a6 (∀' a) τ refl | ._ | reveal[ eq ] with lem-a6 (open-meta a) τ eq
lem-a6 (∀' a) τ refl | ._ | reveal[ eq ] | (t' // x ◅ u , b/u◁τ) = {!!} -- {!u!} , (m-tabs {!!})
lem-a6 (simpl x) τ m with mgu (simpl x) τ | inspect (mgu (simpl x)) τ
lem-a6 (simpl x) τ refl | just (u , proj₂) | reveal[ eq ] =
  u , subst (λ u → u ◁ τ) (sym $ mgu-unifies (simpl x) τ {!!}) m-simp
lem-a6 (simpl x) τ () | nothing

_match1st_ : ∀ {ν} (Δ : ICtx ν) → (a : SimpleType ν) → Maybe (Type ν × ICtx ν)
List.[] match1st a = nothing
(x List.∷ Δ) match1st a with x match a
(x List.∷ Δ) match1st a | just z = just (x , z)
(x List.∷ Δ) match1st a | nothing = Δ match1st a

_⊢alg_ : ∀ {ν n} (K : Ktx ν n) → (a : Type ν) → Dec (K ⊢ᵣ a)
(Γ , Δ) ⊢alg simpl x with Δ match1st x
(Γ , Δ) ⊢alg simpl x | just (proj₁ , proj₂) = {!!}
(Γ , Δ) ⊢alg simpl x | nothing = {!!}
K ⊢alg (a ⇒ b) with (a ∷K K) ⊢alg b
K ⊢alg (a ⇒ b) | yes p = yes $ r-iabs a p
K ⊢alg (a ⇒ b) | no ¬p = no (λ{ (r-iabs .a x) → ¬p x })
K ⊢alg ∀' a with (ktx-weaken K) ⊢alg a
K ⊢alg ∀' a | yes p = yes (r-tabs p)
K ⊢alg ∀' a | no ¬p = no (λ{ (r-tabs p) → ¬p p })

-}
module relational where

  data _⊢_amatch_↠_ {m ν} : (ρs : MICtx m ν) → MetaType m ν → SimpleType ν → (ICtx ν) → Set where
    mtc-tabs : ∀ {r ρs ρs' a} → (List.map meta-weaken ρs) ⊢ (open-meta r) amatch a ↠ ρs' →
                ρs ⊢ ∀' r amatch a ↠ ρs'
    mtc-iabs : ∀ {ρs ρs' a b c} → (a List.∷ ρs) ⊢ b amatch c ↠ ρs' → ρs ⊢ a ⇒ b amatch c ↠ ρs'
    mtc-simp : ∀ {ρs a b} → (u : Unifiable (simpl a) b) →
               ρs ⊢ (simpl a) amatch b ↠ (List.map (λ r → from-meta $ r M./ (asub (proj₁ u))) ρs)

  _⊢match_↠_ : ∀ {ν} → (Type ν) → (SimpleType ν) → ICtx ν → Set
  r ⊢match a ↠ ρs = List.[] ⊢ (to-meta {zero} r) amatch a ↠ ρs

  data _⊢match1st_↠_ {ν} : List (Type ν) → (a : SimpleType ν) → ICtx ν → Set where
    m1-head : ∀ {rs ρs} {r : Type ν} {a} → r ⊢match a ↠ ρs → (r List.∷ rs) ⊢match1st a ↠ ρs
    m1-tail : ∀ {rs ρs} {r : Type ν} {a} → ¬ r ⊢match a ↠ ρs → rs ⊢match1st a ↠ ρs →
              (r List.∷ rs) ⊢match1st a ↠ ρs

  {-}
  gather : ∀ {ν} {ρs ρs' : ICtx ν} {a} → ρs ⊢match1st a ↠ ρs' → List (Type ν)
  gather (m1-head x) = gather' x
    where
        gather' : ∀ {m ν} {ρs : MICtx m ν} {r a} → ρs ⊢ r amatch a ↠→ List (Type ν)
        gather' (mtc-tabs x) = gather' x
        gather' (mtc-iabs x) = gather' x
        gather' {ρs = ρs} (mtc-simp {a = a} {b = b} u) =
                (List.map (λ r → from-meta $ substitute (asub (proj₁ u)) r) ρs)
  gather (m1-tail ¬x xs) = gather xs
  -}

  {-# NO_TERMINATION_CHECK #-}
  amatch : ∀ {m ν} → (ρs : MICtx m ν) → (r : MetaType m ν) (a : SimpleType ν) →
            Dec (∃ λ ρs' → ρs ⊢ r amatch a ↠ ρs')
  amatch ρs (simpl x) a with mgu (simpl x) a | inspect (mgu (simpl x)) a
  amatch ρs (simpl x) a | just mgu | _ = yes (, mtc-simp mgu)
  amatch ρs (simpl x) a | nothing | reveal[ eq ] =
    no (λ{ (._ , mtc-simp p) → (mgu-sound (simpl x) a eq) p})
  amatch ρs (b ⇒ c) a with amatch (b List.∷ ρs) c a
  amatch ρs (b ⇒ c) a | yes (_ , p) = yes $ , mtc-iabs p
  amatch ρs (b ⇒ c) a | no ¬p = no (λ{ (._ , mtc-iabs x) → ¬p (, x)})
  amatch ρs (∀' r) a with amatch (List.map meta-weaken ρs) (open-meta r) a
  amatch ρs (∀' r) a | yes (_ , p) = yes $ , mtc-tabs p
  amatch ρs (∀' r) a | no ¬p = no (λ{ (._ , mtc-tabs x) → ¬p (, x) })

  match : ∀ {ν} → (r : Type ν) → (a : SimpleType ν) → Dec (∃ λ ρs → r ⊢match a ↠ ρs)
  match r a = amatch List.[] (to-meta {zero} r) a

  _match1st_ : ∀ {ν} (Δ : ICtx ν) → (a : SimpleType ν) → Dec (∃ λ ρs → Δ ⊢match1st a ↠ ρs)
  List.[] match1st a = no (λ{ (_ , ()) })
  (x List.∷ xs) match1st a with match x a
  (x List.∷ xs) match1st a | yes (ρs , p) = yes (ρs , m1-head p)
  (x List.∷ xs) match1st a | no ¬p with xs match1st a
  (x List.∷ xs) match1st a | no ¬p | yes p = yes  ? -- (, m1-tail ¬p p)
  (x List.∷ xs) match1st a | no ¬p-head | no ¬p-tail =
    no (λ{ (_ , m1-head p-head) → ¬p-head (, p-head) ; (_ , m1-tail _ p-tail) → ¬p-tail (, p-tail) })

  module Lemmas where

    lem-A3 : ∀ {ν n} (K : Ktx ν n) {a r} → proj₂ K ⟨ a ⟩= r → r List.∈ (proj₂ K)
    lem-A3 f = proj₁ ∘ FirstLemmas.first⟶∈

    lem-A6-1 : ∀ {m ν} → AList ν (suc m) zero → ASub ν (suc m) m × AList ν m zero
    lem-A6-1 (t' // zero ◅ s) = t' // zero , s
    lem-A6-1 {zero} (t' // suc () ◅ xs)
    lem-A6-1 {suc m} (t' // x ◅ xs) with lem-A6-1 xs
    lem-A6-1 {suc m} (t' // zero ◅ xs) | e , u = t' // zero , xs -- same case as above
    lem-A6-1 {suc m} (t' // suc x ◅ xs) | e , u = asub-weaken e , t' // x ◅ u

    lem-A6 : ∀ {m ν} {ρs ρs'} {a : MetaType m ν} {τ : SimpleType ν} → ρs ⊢ a amatch τ ↠ ρs' →
             (∃ λ (u : AList ν m zero) → (from-meta $ a M./ (asub u)) ◁ τ)
    lem-A6 {a = ∀' a} {τ = τ} (mtc-tabs x) with lem-A6 x
    lem-A6 {a = ∀' a} {τ = τ} (mtc-tabs x) | u , p with lem-A6-1 u
    lem-A6 {a = ∀' a} {τ = τ} (mtc-tabs x) | u , p | b , bs = bs , m-tabs {!p!}
      where
        -- q : from-meta (substitute (asub u) a []) ◁ τ
        -- q = {!!}
    lem-A6 (mtc-iabs x) with lem-A6 x
    lem-A6 (mtc-iabs x) | u , p = u , (m-iabs p)
    lem-A6 {τ = τ} (mtc-simp {a = a} (u , eq)) =
      u , subst (flip _◁_ τ) (sym $ mgu-unifies (simpl a) τ (u , eq)) m-simp

    lem-A6' : ∀ {ν} {ρs ρs' } {r : Type ν} {a} → r ◁ a → ρs ⊢ (to-meta {zero} r) amatch a ↠ ρs'
    lem-A6' {a = a} m-simp = mtc-simp (mgu-id a)
    lem-A6' (m-tabs r◁a) = mtc-tabs {!!}
    lem-A6' (m-iabs r◁a) = mtc-iabs (lem-A6' r◁a)

    -- p'haps counterintuitively the following proposition is NOT a theorem:
    -- Δ⊢ᵣa⟶Δ≢Ø : ∀ {ν n} {K : Ktx ν n} {a} → K ⊢ᵣ a → ∃ λ b → b List.∈ (proj₂ K)
    -- since [] ⊢ᵣ Nat ⇒ Nat through the r-iabs rule, but also:
    -- [] ⊢ᵣ Nat ⇒ (Nat ⇒ Nat), etc; through recursion on r-iabs

    lem-A7a : ∀ {ν} (Δ : ICtx ν) {a ρs} → Δ ⊢match1st a ↠ ρs → ∃ λ r → Δ ⟨ a ⟩= r
    lem-A7a List.[] ()
    lem-A7a (x List.∷ Δ) {a = a} (m1-head x₁) = , (l-head u Δ)
        where
        p = lem-A6 x₁
        u = subst (λ u' → u' ◁ a) (alist-zero-vanishes (proj₁ p)) (proj₂ p)
    lem-A7a (r List.∷ Δ) (m1-tail ¬pr y) =
        , (l-tail (λ r◁a → ¬pr $ lem-A6' r◁a) (proj₂ $ lem-A7a Δ y))

  open Lemmas

  _⊢alg_ : ∀ {ν n} (K : Ktx ν n) → (a : Type ν) → Dec (K ⊢ᵣ a)
  K ⊢alg simpl x with proj₂ K match1st x
  K ⊢alg simpl x | yes p = yes (r-simp (proj₂ $ lem-A7a (proj₂ K) p) {!!})
  K ⊢alg simpl x | no ¬p = no (λ{ (r-simp x₁ x₂) → {!!} })
  K ⊢alg (a ⇒ b) with (a ∷K K) ⊢alg b
  K ⊢alg (a ⇒ b) | yes p = yes $ r-iabs a p
  K ⊢alg (a ⇒ b) | no ¬p = no (λ{ (r-iabs .a x) → ¬p x })
  K ⊢alg ∀' a with (ktx-weaken K) ⊢alg a
  K ⊢alg ∀' a | yes p = yes (r-tabs p)
  K ⊢alg ∀' a | no ¬p = no (λ{ (r-tabs x) → ¬p x })


text:
-- Basic intuitionistic logic of proofs, without ∨, ⊥, or +.
-- Common syntax.

module BasicILP.Syntax.Common where

open import Common.ContextPair public

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- https://github.com/bitonic/tog/wiki/Implicit-Arguments
-- aj s popisom checkingu od Andreasa Abela

module ImplArg where
data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
  vnil  : Vec A zero
  vcons : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

Cons = {A : Set} (a : A) {n : Nat} -> Vec A n -> Vec A (suc n)

cons : Cons
cons a = vcons a

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

module Dipsy.Polarity where

data Polarity : Set where
  pos : Polarity
  neg : Polarity

open import Algebra.FunctionProperties {A = Polarity} _≡_

flip : Polarity → Polarity
flip pos = neg
flip neg = pos

flip-inv : Involutive flip
flip-inv pos = refl
flip-inv neg = refl

max_stars_repo_name: wenkokke/Dipsy

max_issues_repo_name: wenkokke/dipsy

max_forks_repo_name: wenkokke/dipsy


text:
postulate
  A B C : Set

module M where

  infixl 4 _+_
  infixl 6 _*_

  postulate
    _+_ _*_ : Set → Set → Set

  T : Set
  T = A + B * C

open M renaming (_*_ to infix 2 _*_)

test : T → A + B * C
test x = x  -- should use the updated fixity when printing the value of T !


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

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Addition

module Numbers.Naturals.Multiplication where

infix 25 _*N_
_*N_ : ℕ → ℕ → ℕ
zero *N y = zero
(succ x) *N y = y +N (x *N y)
{-# BUILTIN NATTIMES _*N_ #-}

productZeroIsZeroLeft : (a : ℕ) → (zero *N a ≡ zero)
productZeroIsZeroLeft a = refl

productZeroIsZeroRight : (a : ℕ) → (a *N zero ≡ zero)
productZeroIsZeroRight zero = refl
productZeroIsZeroRight (succ a) = productZeroIsZeroRight a

productWithOneLeft : (a : ℕ) → ((succ zero) *N a) ≡ a
productWithOneLeft a = transitivity refl (transitivity (applyEquality (λ { m -> a +N m }) refl) (additionNIsCommutative a zero))

productWithOneRight : (a : ℕ) → a *N succ zero ≡ a
productWithOneRight zero = refl
productWithOneRight (succ a) = transitivity refl (addingPreservesEqualityLeft (succ zero) (productWithOneRight a))

productDistributes : (a b c : ℕ) → (a *N (b +N c)) ≡ a *N b +N a *N c
productDistributes zero b c = refl
productDistributes (succ a) b c = transitivity refl
  (transitivity (addingPreservesEqualityLeft (b +N c) (productDistributes a b c))
    (transitivity (equalityCommutative (additionNIsAssociative (b +N c) (a *N b) (a *N c)))
      (transitivity (addingPreservesEqualityRight (a *N c) (additionNIsCommutative (b +N c) (a *N b)))
        (transitivity (addingPreservesEqualityRight (a *N c) (equalityCommutative (additionNIsAssociative (a *N b) b c)))
          (transitivity (addingPreservesEqualityRight (a *N c) (addingPreservesEqualityRight c (additionNIsCommutative (a *N b) b)))
            (transitivity (addingPreservesEqualityRight (a *N c) (addingPreservesEqualityRight {b +N a *N b} {(succ a) *N b} c (refl)))
              (transitivity (additionNIsAssociative ((succ a) *N b) c (a *N c))
                (transitivity (addingPreservesEqualityLeft (succ a *N b) refl)
                  refl)
            )
        ))))))

productPreservesEqualityLeft : (a : ℕ) → {b c : ℕ} → b ≡ c → a *N b ≡ a *N c
productPreservesEqualityLeft a {b} {.b} refl = refl

aSucB : (a b : ℕ) → a *N succ b ≡ a *N b +N a
aSucB a b = transitivity {_} {ℕ} {a *N succ b} {a *N (b +N succ zero)} (productPreservesEqualityLeft a (succIsAddOne b)) (transitivity {_} {ℕ} {a *N (b +N succ zero)} {a *N b +N a *N succ zero} (productDistributes a b (succ zero)) (addingPreservesEqualityLeft (a *N b) (productWithOneRight a)))

aSucBRight : (a b : ℕ) → (succ a) *N b ≡ a *N b +N b
aSucBRight a b = additionNIsCommutative b (a *N b)

multiplicationNIsCommutative : (a b : ℕ) → (a *N b) ≡ (b *N a)
multiplicationNIsCommutative zero b = transitivity (productZeroIsZeroLeft b) (equalityCommutative (productZeroIsZeroRight b))
multiplicationNIsCommutative (succ a) zero = multiplicationNIsCommutative a zero
multiplicationNIsCommutative (succ a) (succ b) = transitivity refl
  (transitivity (addingPreservesEqualityLeft (succ b) (aSucB a b))
    (transitivity (additionNIsCommutative (succ b) (a *N b +N a))
      (transitivity (additionNIsAssociative (a *N b) a (succ b))
        (transitivity (addingPreservesEqualityLeft (a *N b) (succCanMove a b))
          (transitivity (addingPreservesEqualityLeft (a *N b) (additionNIsCommutative (succ a) b))
            (transitivity (equalityCommutative (additionNIsAssociative (a *N b) b (succ a)))
              (transitivity (addingPreservesEqualityRight (succ a) (equalityCommutative (aSucBRight a b)))
                (transitivity (addingPreservesEqualityRight (succ a) (multiplicationNIsCommutative (succ a) b))
                  (transitivity (additionNIsCommutative (b *N (succ a)) (succ a))
                    refl
                )))))))))

productDistributes' : (a b c : ℕ) → (a +N b) *N c ≡ a *N c +N b *N c
productDistributes' a b c rewrite multiplicationNIsCommutative (a +N b) c | productDistributes c a b | multiplicationNIsCommutative c a | multiplicationNIsCommutative c b = refl

flipProductsWithinSum : (a b c : ℕ) → (c *N a +N c *N b ≡ a *N c +N b *N c)
flipProductsWithinSum a b c = transitivity (addingPreservesEqualityRight (c *N b) (multiplicationNIsCommutative c a)) ((addingPreservesEqualityLeft (a *N c) (multiplicationNIsCommutative c b)))

productDistributesRight : (a b c : ℕ) → (a +N b) *N c ≡ a *N c +N b *N c
productDistributesRight a b c = transitivity (multiplicationNIsCommutative (a +N b) c) (transitivity (productDistributes c a b) (flipProductsWithinSum a b c))

multiplicationNIsAssociative : (a b c : ℕ) → (a *N (b *N c)) ≡ ((a *N b) *N c)
multiplicationNIsAssociative zero b c = refl
multiplicationNIsAssociative (succ a) b c =
    transitivity refl
      (transitivity refl
        (transitivity (applyEquality ((λ x → b *N c +N x)) (multiplicationNIsAssociative a b c)) (transitivity (equalityCommutative (productDistributesRight b (a *N b) c)) refl)))

productOne : {a b : ℕ} → a ≡ a *N b → (a ≡ 0) || (b ≡ 1)
productOne {zero} {b} pr = inl refl
productOne {succ a} {zero} pr rewrite multiplicationNIsCommutative a 0 = exFalso (naughtE (equalityCommutative pr))
productOne {succ a} {succ zero} pr = inr refl
productOne {succ a} {succ (succ b)} pr rewrite multiplicationNIsCommutative a (succ (succ b)) | additionNIsCommutative (succ b) (a +N (a +N b *N a)) | additionNIsAssociative (succ a) (a +N b *N a) (succ b) | additionNIsCommutative (a +N b *N a) (succ b) = exFalso (bad pr)
  where
    bad' : {x : ℕ} → x ≡ succ x → False
    bad' ()
    bad : {x y : ℕ} → x ≡ x +N succ y → False
    bad {succ x} {zero} pr rewrite additionNIsCommutative x 1 = bad' pr
    bad {succ x} {succ y} pr = bad (succInjective pr)


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

module reachability where
  -- algorithmically, we break reachability into two halves: first you
  -- produce a list of actions that are all "move parent" to pull the cursor
  -- to the very top of the expression in question. then, you go back down
  -- into the expression with a sequence of move firstChild and move
  -- nextSibs as appropriate. the append of these two lists will reach from
  -- one expression to the other.
  --
  -- there may well be a shorter list of actions that does the same thing;
  -- the expression with top-level cursor may not be the Least Common
  -- Ancestor in the expression tree of the given pair. however, the work
  -- of this less minimal thing and corresponding size of the proof term is
  -- still bounded linearly by the size of the expression, and is far
  -- easier to maniupulate judgementally.

  reachup-type : {t : ztyp} {t' : htyp} →
                 erase-t t t' →
                 Σ[ L ∈ List action ] (runtype t L (▹ t' ◃) × movements L)
  reachup-type ETTop = [] , DoRefl , AM[]
  reachup-type (ETArrL er) with reachup-type er
  ... | (l , ih , m ) = l ++ [ move parent ] ,
                        runtype++ (ziplem-tmarr1 ih) (DoType TMArrParent1 DoRefl) ,
                        movements++ m (AM:: AM[])
  reachup-type (ETArrR er) with reachup-type er
  ... | (l , ih , m ) = l ++ [ move parent ] ,
                        runtype++ (ziplem-tmarr2 ih) (DoType TMArrParent2 DoRefl) ,
                        movements++ m (AM:: AM[])
  reachup-type (ETPlusL er) with reachup-type er
  ... | (l , ih , m ) = l ++ [ move parent ] ,
                        runtype++ (ziplem-tmplus1 ih) (DoType TMPlusParent1 DoRefl) ,
                        movements++ m (AM:: AM[])
  reachup-type (ETPlusR er) with reachup-type er
  ... | (l , ih , m ) = l ++ [ move parent ] ,
                        runtype++ (ziplem-tmplus2 ih) (DoType TMPlusParent2 DoRefl) ,
                        movements++ m (AM:: AM[])
  reachup-type (ETProdL er) with reachup-type er
  ... | (l , ih , m) =  l ++ [ move parent ] ,
                        runtype++ (ziplem-tmprod1 ih) (DoType TMProdParent1 DoRefl) ,
                        movements++ m (AM:: AM[])
  reachup-type (ETProdR er) with reachup-type er
  ... | (l , ih , m) =  l ++ [ move parent ] ,
                        runtype++ (ziplem-tmprod2 ih) (DoType TMProdParent2 DoRefl) ,
                        movements++ m (AM:: AM[])

  mutual
    reachup-synth : {Γ : tctx} {e : zexp} {t : htyp} {e' : hexp} →
                      erase-e e e' →
                      Γ ⊢ e' => t →
                     Σ[ L ∈ List action ] (runsynth Γ e t L ▹ e' ◃ t × movements L)
    reachup-synth (EELam _) ()
    reachup-synth (EEInl er) ()
    reachup-synth (EEInr er) ()
    reachup-synth (EECase1 er) ()
    reachup-synth (EECase2 er) ()
    reachup-synth (EECase3 er) ()

    reachup-synth EETop _ = [] , DoRefl , AM[]
    reachup-synth (EEPlusL er) (SPlus x x₁) with reachup-ana er x
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-plus1 ih) (DoSynth (SAMove EMPlusParent1) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEPlusR er) (SPlus x x₁) with reachup-ana er x₁
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-plus2 ih) (DoSynth (SAMove EMPlusParent2) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEAscL er) (SAsc x) with reachup-ana er x
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-asc1 ih) (DoSynth (SAMove EMAscParent1) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEAscR er) (SAsc x₁) with reachup-type er
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ {L1 = l} (ziplem-moves-asc2 m er x₁ ih)
                                  (DoSynth (SAMove EMAscParent2) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEHalfLamL er) (SLam x wt) with reachup-type er
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ {L1 = l}
                                  (ziplem-moves-halflam1 x er ETTop m ih wt wt)
                                  (DoSynth (SAMove EMHalfLamParent1) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEHalfLamR er) (SLam x wt) with reachup-synth er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ {L1 = l}
                                  (ziplem-halflam2 x er wt ih)
                                  (DoSynth (SAMove EMHalfLamParent2) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEApL er) (SAp wt x x₁) with reachup-synth er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ {L1 = l}
                                  (ziplem-moves-ap1 (lem-erase-synth er wt) x x₁ m ih)
                                                    (DoSynth (SAMove EMApParent1) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEApR er) (SAp wt x x₁) with reachup-ana er x₁
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-ap2 wt x ih) (DoSynth (SAMove EMApParent2) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EENEHole er) (SNEHole wt) with reachup-synth er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-nehole-a (lem-erase-synth er wt) ih)
                                                   (DoSynth (SAMove EMNEHoleParent) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEFst er) (SFst wt pr) with reachup-synth er wt
    ... | l , ih , m = (l ++ [ move parent ]) ,
                       runsynth++ (ziplem-moves-fst pr pr er wt m ih)
                                  (DoSynth (SAMove EMFstParent) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EESnd er) (SSnd wt pr) with reachup-synth er wt
    ... | l , ih , m = (l ++ [ move parent ]) ,
                       runsynth++ (ziplem-moves-snd pr pr er wt m ih)
                                  (DoSynth (SAMove EMSndParent) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEPairL er) (SPair wt wt₁) with reachup-synth er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-pair1 er wt ih wt₁)
                                  (DoSynth (SAMove EMPairParent1) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-synth (EEPairR er) (SPair wt wt₁) with reachup-synth er wt₁
    ... | l , ih , m = l ++ [ move parent ] ,
                       runsynth++ (ziplem-pair2 wt er wt₁ ih)
                                  (DoSynth (SAMove EMPairParent2) DoRefl) ,
                       movements++ m (AM:: AM[])

    reachup-ana : {Γ : tctx} {e : zexp} {t : htyp} {e' : hexp} →
                  erase-e e e' →
                  Γ ⊢ e' <= t →
                  Σ[ L ∈ List action ] (runana Γ e L ▹ e' ◃ t × movements L)
    reachup-ana EETop _ = [] , DoRefl , AM[]
    reachup-ana er (ASubsume x x₁) with reachup-synth er x
    ... | l , ih , m = l ,
                       synthana-moves (lem-erase-synth er x) m x₁ ih ,
                       m
    reachup-ana (EELam er) (ALam x₁ x₂ wt) with reachup-ana er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runana++ (ziplem-lam x₁ x₂ ih) (DoAna (AAMove EMLamParent) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-ana (EEInl er) (AInl x wt) with reachup-ana er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runana++ (ziplem-inl x ih) (DoAna (AAMove EMInlParent) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-ana (EEInr er) (AInr x wt) with reachup-ana er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runana++ (ziplem-inr x ih) (DoAna (AAMove EMInrParent) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-ana (EECase1 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) with reachup-synth er x₄
    ... | l , ih , m = l ++ [ move parent ] ,
                       runana++ {L1 = l} (ziplem-case1a x₁ x₂ er x₄ ih x₃ wt wt₁ m)
                                (DoAna (AAMove EMCaseParent1) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-ana (EECase2 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) with reachup-ana er wt
    ... | l , ih , m = l ++ [ move parent ] ,
                       runana++ (ziplem-case2 x₁ x₂ x₄ wt₁ x₃ ih)
                                (DoAna (AAMove EMCaseParent2) DoRefl) ,
                       movements++ m (AM:: AM[])
    reachup-ana (EECase3 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) with reachup-ana er wt₁
    ... | l , ih , m = l ++ [ move parent ] ,
                       runana++ (ziplem-case3 x₁ x₂ x₄ wt x₃ ih)
                                (DoAna (AAMove EMCaseParent3) DoRefl) ,
                       movements++ m (AM:: AM[])

  reachdown-type : {t : htyp} {t' : ztyp} → (p : erase-t t' t) →
                   Σ[ L ∈ List action ] (runtype (▹ t ◃) L t' × movements L)
  reachdown-type ETTop = [] , DoRefl , AM[]
  reachdown-type (ETArrL er) with reachdown-type er
  ... | (l , ih , m ) = move (child 1) :: l ,
                        DoType TMArrChild1 (ziplem-tmarr1 ih) ,
                        AM:: m
  reachdown-type (ETArrR er) with reachdown-type er
  ... | (l , ih , m ) = move (child 2) :: l ,
                        DoType TMArrChild2 (ziplem-tmarr2 ih) ,
                        AM:: m
  reachdown-type (ETPlusL er) with reachdown-type er
  ... | (l , ih , m ) = move (child 1) :: l ,
                        DoType TMPlusChild1 (ziplem-tmplus1 ih) ,
                        AM:: m
  reachdown-type (ETPlusR er) with reachdown-type er
  ... | (l , ih , m ) = move (child 2) :: l ,
                        DoType TMPlusChild2 (ziplem-tmplus2 ih) ,
                        AM:: m
  reachdown-type (ETProdL er) with reachdown-type er
  ... | (l , ih , m ) = move (child 1) :: l ,
                        DoType TMProdChild1 (ziplem-tmprod1 ih) ,
                        AM:: m
  reachdown-type (ETProdR er) with reachdown-type er
  ... | (l , ih , m ) = move (child 2) :: l ,
                        DoType TMProdChild2 (ziplem-tmprod2 ih) ,
                        AM:: m

  mutual
    reachdown-synth : {Γ : tctx} {e : zexp} {t : htyp} {e' : hexp} →
                      (p : erase-e e e') →
                      (wt : Γ ⊢ e' => t) →
                      Σ[ L ∈ List action ] (runsynth Γ ▹ e' ◃ t L e t × movements L)
    reachdown-synth (EELam _) ()
    reachdown-synth (EEInl er) ()
    reachdown-synth (EEInr er) ()
    reachdown-synth (EECase1 er) ()
    reachdown-synth (EECase2 er) ()
    reachdown-synth (EECase3 er) ()

    reachdown-synth EETop _ = [] , DoRefl , AM[]
    reachdown-synth (EEAscL er) (SAsc x) with reachdown-ana er x
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMAscChild1) (ziplem-asc1 ih) ,
                       AM:: m
    reachdown-synth (EEAscR er) (SAsc x₁) with reachdown-type er
    ... | l , ih , m = move (child 2) :: l ,
                       DoSynth (SAMove EMAscChild2) (ziplem-moves-asc2 m ETTop x₁ ih) ,
                       AM:: m
    reachdown-synth (EEHalfLamL er) (SLam x wt) with reachdown-type er
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMHalfLamChild1)
                               (ziplem-moves-halflam1 x ETTop er m ih wt wt) ,
                       AM:: m
    reachdown-synth (EEHalfLamR er) (SLam x wt) with reachdown-synth er wt
    ... | l , ih , m = move (child 2) :: l ,
                       DoSynth (SAMove EMHalfLamChild2) (ziplem-halflam2 x EETop wt ih) ,
                       AM:: m
    reachdown-synth (EEApL er) (SAp wt x x₁) with reachdown-synth er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMApChild1) (ziplem-moves-ap1 wt x x₁ m ih) ,
                       AM:: m
    reachdown-synth (EEApR er) (SAp wt x x₁) with reachdown-ana er x₁
    ... | l , ih , m = move (child 2) :: l ,
                       DoSynth (SAMove EMApChild2) (ziplem-ap2 wt x ih) ,
                       AM:: m
    reachdown-synth (EEPlusL er) (SPlus x x₁) with reachdown-ana er x
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMPlusChild1) (ziplem-plus1 ih) ,
                       AM:: m
    reachdown-synth (EEPlusR er) (SPlus x x₁) with reachdown-ana er x₁
    ... | l , ih , m = move (child 2) :: l ,
                       DoSynth (SAMove EMPlusChild2) (ziplem-plus2 ih) ,
                       AM:: m
    reachdown-synth (EENEHole er) (SNEHole wt) with reachdown-synth er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMNEHoleChild1) (ziplem-nehole-a wt ih) ,
                       AM:: m
    reachdown-synth (EEPairL er) (SPair wt wt₁) with reachdown-synth er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMPairChild1) (ziplem-pair1 EETop wt ih wt₁) ,
                       AM:: m
    reachdown-synth (EEPairR er) (SPair wt wt₁)
      with reachdown-synth er wt₁
    ... | l , ih , m = move (child 2) :: l ,
                       DoSynth (SAMove EMPairChild2) (ziplem-pair2 wt EETop wt₁ ih) ,
                       AM:: m
    reachdown-synth (EEFst er) (SFst wt pr) with reachdown-synth er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMFstChild1)
                               (ziplem-moves-fst pr pr EETop wt m ih) ,
                       AM:: m
    reachdown-synth (EESnd er) (SSnd wt pr) with reachdown-synth er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoSynth (SAMove EMSndChild1)
                               (ziplem-moves-snd pr pr EETop wt m ih) ,
                       AM:: m

    reachdown-ana : {Γ : tctx} {e : zexp} {t : htyp} {e' : hexp} →
                    (p : erase-e e e') →
                    (wt : Γ ⊢ e' <= t) →
                    Σ[ L ∈ List action ] (runana Γ ▹ e' ◃ L e  t × movements L)
    reachdown-ana EETop _ = [] , DoRefl , AM[]
    reachdown-ana er (ASubsume x x₁) with reachdown-synth er x
    ... | l , ih , m = l ,
                       synthana-moves x m x₁ ih ,
                       m
    reachdown-ana (EELam er) (ALam x₁ x₂ wt) with reachdown-ana er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoAna (AAMove EMLamChild1) (ziplem-lam x₁ x₂ ih) ,
                       AM:: m
    reachdown-ana (EEInl er) (AInl x wt) with reachdown-ana er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoAna (AAMove EMInlChild1) (ziplem-inl x ih) ,
                       AM:: m
    reachdown-ana (EEInr er) (AInr x wt) with reachdown-ana er wt
    ... | l , ih , m = move (child 1) :: l ,
                       DoAna (AAMove EMInrChild1) (ziplem-inr x ih) ,
                       AM:: m
    reachdown-ana (EECase1 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) with reachdown-synth er x₄
    ... | l , ih , m = move (child 1) :: l ,
                       DoAna (AAMove EMCaseChild1)
                             (ziplem-case1a x₁ x₂ EETop x₄ ih x₃ wt wt₁ m) ,
                       AM:: m
    reachdown-ana (EECase2 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) with reachdown-ana er wt
    ... | l , ih , m = move (child 2) :: l ,
                       DoAna (AAMove EMCaseChild2) (ziplem-case2 x₁ x₂ x₄ wt₁ x₃ ih) ,
                       AM:: m
    reachdown-ana (EECase3 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) with reachdown-ana er wt₁
    ... | l , ih , m = move (child 3)  :: l ,
                       DoAna (AAMove EMCaseChild3) (ziplem-case3 x₁ x₂ x₄ wt x₃ ih) ,
                       AM:: m

  -- this is the final statement of the reachability triplet. the movement
  -- between judgemental and metafunctional erasure happens internally to
  -- theses statements to present a consistent interface with the text of
  -- the paper, while also allowing easy pattern matching in the proofs.
  --
  -- the intuition for these statements is that the cursor cannot change
  -- the type of things because the typing judgement is defined on the
  -- cursor-erased terms and types.
  reachability-types : (t1 t2 : ztyp) → (t1 ◆t) == (t2 ◆t) →
                       Σ[ L ∈ List action ] (runtype t1 L t2 × movements L)
  reachability-types t1 t2 eq
    with ◆erase-t t1 (t2 ◆t) eq | ◆erase-t t2 (t1 ◆t) (! eq)
  ... | er1 | er2 with reachup-type er1 | reachdown-type er2
  ... | (lup , rup , mvup)  | (ldwn , rdwn , mvdwn) =
        lup ++ ldwn ,
        runtype++ rup (tr (λ x → runtype ▹ x ◃ ldwn t2) eq rdwn) ,
        movements++ mvup mvdwn

  reachability-synth : (Γ : tctx) (t : htyp) (e1 e2 : zexp) →
                       Γ ⊢ e1 ◆e => t →
                       e1 ◆e == e2 ◆e →
                       Σ[ L ∈ List action ] (runsynth Γ e1 t L e2 t × movements L)
  reachability-synth Γ t e1 e2 wt1 eq
    with ◆erase-e e1 (e2 ◆e) eq | ◆erase-e e2 (e1 ◆e) (! eq)
  ... | er1 | er2 with reachup-synth er1 (tr (λ x → Γ ⊢ x => t) eq wt1)
                     | reachdown-synth er2 wt1
  ... | (lup , rup , mvup)  | (ldwn , rdwn , mvdwn) =
      (lup ++ ldwn) ,
      runsynth++ rup (tr (λ x → runsynth Γ ▹ x ◃ t ldwn e2 t) eq rdwn) ,
      movements++ mvup mvdwn

  reachability-ana : (Γ : tctx) (t : htyp) (e1 e2 : zexp) →
                     Γ ⊢ e1 ◆e <= t →
                     e1 ◆e == e2 ◆e →
                     Σ[ L ∈ List action ] (runana Γ e1 L e2 t × movements L)
  reachability-ana Γ t e1 e2 wt1 eq
    with ◆erase-e e1 (e2 ◆e) eq | ◆erase-e e2 (e1 ◆e) (! eq)
  ... | er1 | er2 with reachup-ana er1 (tr (λ x → Γ ⊢ x <= t) eq wt1)
                     | reachdown-ana er2 wt1
  ... | (lup , rup , mvup)  | (ldwn , rdwn , mvdwn) =
      lup ++ ldwn ,
      (runana++ rup (tr (λ x → runana Γ ▹ x ◃ ldwn e2 t) eq rdwn)) ,
      (movements++ mvup mvdwn)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module UniDB.Morph.Star where

open import UniDB.Spec

infixl 4 _▻_
data Star (Ξ : MOR) : MOR where
  ε   : {γ : Dom} → Star Ξ γ γ
  _▻_ : {γ₁ γ₂ γ₃ : Dom} (ξs : Star Ξ γ₁ γ₂) (ξ : Ξ γ₂ γ₃) → Star Ξ γ₁ γ₃

module _ {Ξ : MOR} where
  instance
    iIdmStar : Idm (Star Ξ)
    idm {{iIdmStar}} _ = ε

    iCompStar : Comp (Star Ξ)
    _⊙_ {{iCompStar}} ξs ε = ξs
    _⊙_ {{iCompStar}} ξs (ζs ▻ ζ) = (ξs ⊙ ζs) ▻ ζ

module _ {Ξ : MOR} {{upΞ : Up Ξ}} where

  instance
    iUpStar : Up (Star Ξ)
    _↑₁ {{iUpStar}} ε        = ε
    _↑₁ {{iUpStar}} (ξs ▻ ξ) = (ξs ↑₁) ▻ (ξ ↑₁)
    _↑_ {{iUpStar}} ξ 0 = ξ
    _↑_ {{iUpStar}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
    ↑-zero {{iUpStar}} ξ = refl
    ↑-suc {{iUpStar}} ξ δ⁺ = refl

    iUpIdmStar : UpIdm (Star Ξ)
    idm-↑₁ {{iUpIdmStar}} = refl

    iUpCompStar : UpComp (Star Ξ)
    ⊙-↑₁ {{iUpCompStar}} ξs ε        = refl
    ⊙-↑₁ {{iUpCompStar}} ξs (ζs ▻ ζ) =
      cong₂ _▻_ (⊙-↑₁ {Star Ξ} ξs ζs ) (refl {x = ζ ↑₁})

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
module NoParseForLHS where

data X : Set where
  _! : X -> X
  z  : X

right : X -> X
right (x !) = x
right z     = z !

wrong : X -> X
wrong (! x) = x
wrong z     = z !


text:
module par-swap where

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Context
open import sn-calculus

data _∥R_ : Term -> Term -> Set where
  ∥Rstep : ∀ {C p q d} ->
          (d≐C⟦p∥q⟧c : d ≐ C ⟦ (p ∥ q) ⟧c) ->
          d ∥R (C ⟦ (q ∥ p) ⟧c)

data _∥R*_ : Term -> Term -> Set where
  ∥R0 : ∀ {p} -> p ∥R* p
  ∥Rn : ∀ {p q r} ->
        (p∥Rq : p ∥R q) ->
        (q∥R*r : q ∥R* r) ->
        p ∥R* r

∥R*-concat : ∀ {p q r} -> p ∥R* q -> q ∥R* r -> p ∥R* r
∥R*-concat ∥R0 q∥R*r = q∥R*r
∥R*-concat (∥Rn p∥Rq p∥R*q) q∥R*r = ∥Rn p∥Rq (∥R*-concat p∥R*q q∥R*r)

data _∥R*∪sn⟶*_ : Term -> Term -> Set where
  ∪∥R* : ∀ {p q r} ->
         (p∥R*q : p ∥R* q) ->
         (q∥R∪sn⟶*r : q ∥R*∪sn⟶* r) ->
         p ∥R*∪sn⟶* r
  ∪sn⟶* : ∀ {p q r} ->
         (psn⟶*q : p sn⟶* q) ->
         (q∥R∪sn⟶*r : q ∥R*∪sn⟶* r) ->
         p ∥R*∪sn⟶* r
  ∪refl : ∀ {p} -> p ∥R*∪sn⟶* p

∥R*∪sn⟶*-concat : ∀ {p q r} -> p ∥R*∪sn⟶* q -> q ∥R*∪sn⟶* r -> p ∥R*∪sn⟶* r
∥R*∪sn⟶*-concat (∪∥R* p∥R*q a) b = ∪∥R* p∥R*q (∥R*∪sn⟶*-concat a b)
∥R*∪sn⟶*-concat (∪sn⟶* psn⟶*q a) b = ∪sn⟶* psn⟶*q (∥R*∪sn⟶*-concat a b)
∥R*∪sn⟶*-concat ∪refl b = b

data _∥R∪sn≡ₑ_ : Term → Term → Set where
  ∪stpsn : ∀{p q} → (psn⟶q : p sn⟶ q) → p ∥R∪sn≡ₑ q
  ∪stp∥ : ∀{p q} → (p∥Rq : p ∥R q) → p ∥R∪sn≡ₑ q
  ∪sym : ∀{p q BV FV} → (psn∪∥R≡ₑq : p ∥R∪sn≡ₑ q) → (CBp : CorrectBinding p BV FV) → q ∥R∪sn≡ₑ p
  ∪ref : ∀{p} → p ∥R∪sn≡ₑ p
  ∪trn : ∀{p r q} → (p∥R∪sn≡ₑr : p ∥R∪sn≡ₑ r) → (r∥R∪sn≡ₑq : r ∥R∪sn≡ₑ q) → p ∥R∪sn≡ₑ q

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
-- DontCares shouldn't end up in the generated with functions.
module Issue337 where

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

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

postulate
  _≤_ : ℕ → ℕ → Set
  p₁  : 0 ≤ 1
  p₂  : 0 ≤ 1

data SList (bound : ℕ) : Set where
  []    : SList bound
  scons : (head : ℕ) →
          .(head ≤ bound) →
          (tail : SList head) →
          SList bound

l₁ : SList 1
l₁ = scons 0 p₁ []

l₂ : SList 1
l₂ = scons 0 p₂ []

l₁≡l₂ : l₁ ≡ l₂
l₁≡l₂ with Set
... | _ = refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import Categories.Category

module Categories.End {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {V : Category o′ ℓ′ e′} where
private
  module C = Category C
  module V = Category V
open import Categories.Bifunctor using (Bifunctor; Functor; module Functor)
open import Categories.DinaturalTransformation
open import Categories.Functor.Constant
open import Level
open import Categories.Morphisms V
open import Categories.Square
open import Data.Product

record End-data (F : Bifunctor C.op C V) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    E : V.Obj
    π : DinaturalTransformation {C = C} (Constant E) F

  module π = DinaturalTransformation π
  open π using (α)
  π∘_ : ∀ {Q} → Q V.⇒ E → End-data F
  π∘_ {Q} g = record { π = record { α = λ c → α c ∘ g; commute = λ {c c′} f →
               begin
                  F.F₁ (f , C.id) ∘ ((α c′ ∘ g) ∘ id)
                ↓⟨ ∘-resp-≡ʳ identityʳ ⟩
                  F.F₁ (f , C.id) ∘ (α c′ ∘ g)
                ↑⟨ assoc ⟩
                  (F.F₁ (f , C.id) ∘ α c′) ∘ g
                ↑⟨ ∘-resp-≡ʳ identityˡ ⟩
                  (F.F₁ (f , C.id) ∘ α c′) ∘ (id ∘ g)
                ↑⟨ assoc ⟩
                  ((F.F₁ (f , C.id) ∘ α c′) ∘ id) ∘ g
                ↓⟨ ∘-resp-≡ˡ assoc ⟩
                  (F.F₁ (f , C.id) ∘ (α c′ ∘ id)) ∘ g
                ↓⟨ ∘-resp-≡ˡ (π.commute f) ⟩
                  (F.F₁ (C.id , f) ∘ (α c ∘ id)) ∘ g
                ↓⟨ assoc ⟩
                  F.F₁ (C.id , f) ∘ (α c ∘ id) ∘ g
                ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ identityʳ) ⟩
                  F.F₁ (C.id , f) ∘ α c ∘ g
                ↑⟨ ∘-resp-≡ʳ identityʳ ⟩
                  F.F₁ (C.id , f) ∘ (α c ∘ g) ∘ id ∎
{-          begin
            F.F₁ (f , C.id) ∘ (α c′ ∘ g) ∘ ID ↓⟨ Equiv.refl ⟩
            (F.F₁ (f , C.id) ∙ α c′ ∙ ID) ∙ g ↓≡⟨ ∘-resp-≡ˡ (π.commute f) ⟩
            (F.F₁ (C.id , f) ∙ α c ∙ ID) ∙ g  ↓⟨ Equiv.refl ⟩
            F.F₁ (C.id , f) ∙ (α c ∙ g) ∙ ID  ∎ -} } }
   where
     -- open AUReasoning V
     open V.HomReasoning
     module F = Functor F
     open V

  .commute : ∀ {a b} (f : a C.⇒ b) -> Functor.F₁ F (f , C.id) V.∘ α b V.≡ Functor.F₁ F (C.id , f) V.∘ α a
  commute {c} {c′} f =  begin
            F.F₁ (f , C.id) ∘ α c′      ↑⟨ ∘-resp-≡ʳ identityʳ ⟩
            F.F₁ (f , C.id) ∘ α c′ ∘ id ↓⟨ π.commute f ⟩
            F.F₁ (C.id , f) ∘ α c  ∘ id ↓⟨ ∘-resp-≡ʳ identityʳ ⟩
            F.F₁ (C.id , f) ∘ α c       ∎
    where
      open V.HomReasoning
      module F = Functor F
      open V

open DinaturalTransformation using (α)

record End (F : Bifunctor C.op C V) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    Data : End-data F

  open End-data Data

  IsUni : (Q : End-data F) → (u : End-data.E Q V.⇒ E) → Set _
  IsUni Q u = ∀ c → α π c V.∘ u V.≡ α (End-data.π Q) c

  field
    universal : (Q : End-data F) → End-data.E Q V.⇒ E

    .π[c]∘universal≡δ[c] : {Q : End-data F} → IsUni Q (universal Q)

    .universal-unique : {Q : End-data F} → ∀ u → IsUni Q u → u V.≡ universal Q

  .eta-rule : universal Data V.≡ V.id
  eta-rule = begin universal Data ↑⟨ universal-unique {Data} V.id (λ c → V.identityʳ) ⟩
                   V.id           ∎
   where
    open V.HomReasoning

  .π-mono : ∀ {Q} (g₁ g₂ : Q V.⇒ E) → (∀ c → α π c V.∘ g₁ V.≡ α π c V.∘ g₂) → g₁ V.≡ g₂
  π-mono {Q} g₁ g₂ π∘g₁≡π∘g₂ = begin
     g₁                ↓⟨ universal-unique {π∘ g₁} g₁ (λ c → V.Equiv.refl) ⟩
     universal (π∘ g₁) ↑⟨ universal-unique {π∘ g₁} g₂ (λ c → V.Equiv.sym (π∘g₁≡π∘g₂ c)) ⟩
     g₂                ∎
    where
     open V.HomReasoning

  open End-data Data public

open import Data.Product
open import Categories.Product
open import Categories.FunctorCategory
import Categories.NaturalTransformation as NT
open NT.NaturalTransformation using (η)

endF : ∀ {o ℓ e} {A : Category o ℓ e}(F : Functor A (Functors (Product C.op C) V))
        → (∀ a → End (Functor.F₀ F a)) → Functor A V
endF {A = A} F mke = record {
                   F₀ = λ a → End.E (mke a);
                   F₁ = λ {a b} → F₁ {a} {b} ;
                   identity = λ {a} → V.Equiv.sym (End.universal-unique (mke a) V.id (λ c →
                     begin α (End.π (mke a)) c ∘ id                    ↓⟨ identityʳ ⟩
                           α (End.π (mke a)) c                         ↑⟨ identityˡ ⟩
                           id ∘ α (End.π (mke a)) c                    ↑⟨ ∘-resp-≡ˡ F.identity ⟩
                           η (F.F₁ A.id) (c , c) ∘ α (End.π (mke a)) c ∎ )) ;
                   homomorphism = λ {X Y Z f g} → V.Equiv.sym (End.universal-unique (mke Z) _ (λ c →
                       begin α (End.π (mke Z)) c ∘ F₁ g ∘ F₁ f
                                   ↑⟨ assoc ⟩
                             (α (End.π (mke Z)) c ∘ F₁ g) ∘ F₁ f
                                   ↓⟨ ∘-resp-≡ˡ (End.π[c]∘universal≡δ[c] (mke Z) {record {π = F.F₁ g <∘ End.π (mke Y)}} c) ⟩
                             (η (F.F₁ g) (c , c) ∘ α (End.π (mke Y)) c) ∘ F₁ f
                                   ↓⟨ assoc ⟩
                             η (F.F₁ g) (c , c) ∘ α (End.π (mke Y)) c ∘ F₁ f
                                   ↓⟨ ∘-resp-≡ʳ (End.π[c]∘universal≡δ[c] (mke Y) {record {π = F.F₁ f <∘ End.π (mke X)}} c) ⟩
                             η (F.F₁ g) (c , c) ∘ η (F.F₁ f) (c , c) ∘ α (End.π (mke X)) c
                                   ↑⟨ assoc ⟩
                             (η (F.F₁ g) (c , c) ∘ η (F.F₁ f) (c , c)) ∘ α (End.π (mke X)) c
                                   ↑⟨ ∘-resp-≡ˡ F.homomorphism  ⟩
                             η (F.F₁ (A [ g ∘ f ])) (c , c) ∘ α (End.π (mke X)) c
                                                                                ∎ ));
                   F-resp-≡ = λ {a b f g} f≡g → End.universal-unique (mke b) _ (λ c →
                          begin α (End.π (mke b)) c ∘ F₁ f               ↓⟨ End.π[c]∘universal≡δ[c] (mke b) c ⟩
                                η (F.F₁ f) (c , c) ∘ α (End.π (mke a)) c ↓⟨ ∘-resp-≡ˡ (F.F-resp-≡ f≡g) ⟩
                                η (F.F₁ g) (c , c) ∘ α (End.π (mke a)) c ∎ ) }
 where
  module A = Category A
  module F = Functor F
  open V
  open V.HomReasoning
  F₁ = λ {a b} f → End.universal (mke b) (record { E = _; π = (F.F₁ f) <∘ (End.π (mke a)) })

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Lemmachine.Request where
{-# IMPORT Hack #-}
{-# IMPORT Lemmachine.FFI #-}
open import Data.Product
open import Data.List
open import Data.Maybe
open import Data.Bool
open import Data.Nat
open import Data.String

data Method : Set where
  HEAD GET PUT DELETE POST : Method
  TRACE CONNECT OPTIONS : Method

{-# COMPILED_DATA Method Hack.RequestMethod
    Hack.OPTIONS Hack.GET Hack.HEAD Hack.POST
    Hack.PUT Hack.DELETE Hack.TRACE Hack.CONNECT
#-}

eqMethod : Method → Method → Bool
eqMethod HEAD HEAD = true
eqMethod GET GET = true
eqMethod PUT PUT = true
eqMethod DELETE DELETE = true
eqMethod POST POST = true
eqMethod TRACE TRACE = true
eqMethod CONNECT CONNECT = true
eqMethod OPTIONS OPTIONS = true
eqMethod _ _ = false

Version = String
IP = String
LocalPath = String
Path = String

RawPath = String
PathToken = String
PathTokens = List PathToken

data RequestHeader : Set where
  _,_ : String → String → RequestHeader

{-# COMPILED_DATA RequestHeader
    Lemmachine.FFI.RequestHeader
    Lemmachine.FFI.RequestHeader
#-}

headerKey : RequestHeader → String
headerKey (k , _) = k

headerValue : RequestHeader → String
headerValue (_ , v) = v

RequestHeaders = List RequestHeader
Body = Maybe String
Cookie = String
QueryString = String
Port = String

record Request : Set where
  field
    method : Method
    version : Version
    peer : IP
    dispPath : LocalPath
    path : Path
    rawPath : RawPath
    pathTokens : PathTokens
    headers : RequestHeaders
    reqBody : Body
    cookie : Cookie
    queryString : QueryString
    port : Port

postulate isRedirect : Request → Bool

max_issues_repo_name: larrytheliquid/Lemmachine


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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.IntegralDomains.Definition

module Rings.Associates.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Units.Definition R
open Setoid S
open Ring R
open Equivalence eq

Associates : Rel A
Associates x y = Sg A (λ z → Unit z && (x ∼ (y * z)))


text:
{-# OPTIONS --with-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Equality.Erase where

open import Agda.Builtin.Equality

primitive primEraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y


text:
------------------------------------------------------------------------
-- "Reasoning" combinators
------------------------------------------------------------------------

open import Atom

module Reasoning (atoms : χ-atoms) where

open import Equality.Propositional

open import Chi    atoms
open import Values atoms

infix  -1 finally-⇓ _■⟨_⟩ _■⟨_⟩⋆
infixr -2 step-≡⇓ step-⇓ _⟶⟨⟩_ modus-ponens-⇓

step-≡⇓ : ∀ e₁ {e₂ e₃} → e₂ ⇓ e₃ → e₁ ≡ e₂ → e₁ ⇓ e₃
step-≡⇓ _ e₂⇓e₃ refl = e₂⇓e₃

syntax step-≡⇓ e₁ e₂⇓e₃ e₁≡e₂ = e₁ ≡⟨ e₁≡e₂ ⟩⟶ e₂⇓e₃

_⟶⟨⟩_ : ∀ e₁ {e₂} → e₁ ⇓ e₂ → e₁ ⇓ e₂
_ ⟶⟨⟩ e₁⇓e₂ = e₁⇓e₂

mutual

  _■⟨_⟩ : ∀ e → Value e → e ⇓ e
  _ ■⟨ lambda x e ⟩ = lambda
  _ ■⟨ const c vs ⟩ = const (_ ■⟨ vs ⟩⋆)

  _■⟨_⟩⋆ : ∀ es → Values es → es ⇓⋆ es
  _ ■⟨ []     ⟩⋆ = []
  _ ■⟨ v ∷ vs ⟩⋆ = (_ ■⟨ v ⟩) ∷ (_ ■⟨ vs ⟩⋆)

finally-⇓ : (e₁ e₂ : Exp) → e₁ ⇓ e₂ → e₁ ⇓ e₂
finally-⇓ _ _ e₁⇓e₂ = e₁⇓e₂

syntax finally-⇓ e₁ e₂ e₁⇓e₂ = e₁ ⇓⟨ e₁⇓e₂ ⟩■ e₂

modus-ponens-⇓ : ∀ e {e′ v} → e′ ⇓ v → (e′ ⇓ v → e ⇓ v) → e ⇓ v
modus-ponens-⇓ _ x f = f x

syntax modus-ponens-⇓ e x f = e ⟶⟨ f ⟩ x

mutual

  trans-⇓ : ∀ {e₁ e₂ e₃} → e₁ ⇓ e₂ → e₂ ⇓ e₃ → e₁ ⇓ e₃
  trans-⇓ (apply p q r)  s          = apply p q (trans-⇓ r s)
  trans-⇓ (case p q r s) t          = case p q r (trans-⇓ s t)
  trans-⇓ (rec p)        q          = rec (trans-⇓ p q)
  trans-⇓ lambda         lambda     = lambda
  trans-⇓ (const ps)     (const qs) = const (trans-⇓⋆ ps qs)

  trans-⇓⋆ : ∀ {es₁ es₂ es₃} → es₁ ⇓⋆ es₂ → es₂ ⇓⋆ es₃ → es₁ ⇓⋆ es₃
  trans-⇓⋆ []       []       = []
  trans-⇓⋆ (p ∷ ps) (q ∷ qs) = trans-⇓ p q ∷ trans-⇓⋆ ps qs

step-⇓ : ∀ e₁ {e₂ e₃} → e₂ ⇓ e₃ → e₁ ⇓ e₂ → e₁ ⇓ e₃
step-⇓ _ e₂⇓e₃ e₁⇓e₂ = trans-⇓ e₁⇓e₂ e₂⇓e₃

syntax step-⇓ e₁ e₂⇓e₃ e₁⇓e₂ = e₁ ⇓⟨ e₁⇓e₂ ⟩ e₂⇓e₃

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text: test = Prop


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decorated star-lists
------------------------------------------------------------------------

module Data.Star.Decoration where

open import Data.Star
open import Relation.Binary
open import Function
open import Data.Unit
open import Level

-- A predicate on relation "edges" (think of the relation as a graph).

EdgePred : {I : Set} → Rel I zero → Set₁
EdgePred T = ∀ {i j} → T i j → Set

data NonEmptyEdgePred {I : Set}
                      (T : Rel I zero) (P : EdgePred T) : Set where
  nonEmptyEdgePred : ∀ {i j} {x : T i j}
                     (p : P x) → NonEmptyEdgePred T P

-- Decorating an edge with more information.

data DecoratedWith {I : Set} {T : Rel I zero} (P : EdgePred T)
       : Rel (NonEmpty (Star T)) zero where
  ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
      (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs)

edge : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
       DecoratedWith {T = T} P i j → NonEmpty T
edge (↦ {x = x} p) = nonEmpty x

decoration : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
             (d : DecoratedWith {T = T} P i j) →
             P (NonEmpty.proof (edge d))
decoration (↦ p) = p

-- Star-lists decorated with extra information. All P xs means that
-- all edges in xs satisfy P.

All : ∀ {I} {T : Rel I zero} → EdgePred T → EdgePred (Star T)
All P {j = j} xs =
  Star (DecoratedWith P) (nonEmpty xs) (nonEmpty {y = j} ε)

-- We can map over decorated vectors.

gmapAll : ∀ {I} {T : Rel I zero} {P : EdgePred T}
                {J} {U : Rel J zero} {Q : EdgePred U}
                {i j} {xs : Star T i j}
          (f : I → J) (g : T =[ f ]⇒ U) →
          (∀ {i j} {x : T i j} → P x → Q (g x)) →
          All P xs → All {T = U} Q (gmap f g xs)
gmapAll f g h ε          = ε
gmapAll f g h (↦ x ◅ xs) = ↦ (h x) ◅ gmapAll f g h xs

-- Since we don't automatically have gmap id id xs ≡ xs it is easier
-- to implement mapAll in terms of map than in terms of gmapAll.

mapAll : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
         (∀ {i j} {x : T i j} → P x → Q x) →
         All P xs → All Q xs
mapAll {P = P} {Q} f ps = map F ps
  where
  F : DecoratedWith P ⇒ DecoratedWith Q
  F (↦ x) = ↦ (f x)

-- We can decorate star-lists with universally true predicates.

decorate : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
           (∀ {i j} (x : T i j) → P x) →
           (xs : Star T i j) → All P xs
decorate f ε        = ε
decorate f (x ◅ xs) = ↦ (f x) ◅ decorate f xs

-- We can append Alls. Unfortunately _◅◅_ does not quite work.

infixr 5 _◅◅◅_ _▻▻▻_

_◅◅◅_ : ∀ {I} {T : Rel I zero} {P : EdgePred T}
              {i j k} {xs : Star T i j} {ys : Star T j k} →
        All P xs → All P ys → All P (xs ◅◅ ys)
ε          ◅◅◅ ys = ys
(↦ x ◅ xs) ◅◅◅ ys = ↦ x ◅ xs ◅◅◅ ys

_▻▻▻_ : ∀ {I} {T : Rel I zero} {P : EdgePred T}
              {i j k} {xs : Star T j k} {ys : Star T i j} →
        All P xs → All P ys → All P (xs ▻▻ ys)
_▻▻▻_ = flip _◅◅◅_


text:
module Issue1701.ModParamsToLose where

module Param (A : Set) where

  module R (B : Set) (G : A → B) where
    F = G

  private
   module Tmp (B : Set) (G : A → B) where
    module r = R B G

  open Tmp public

module Works (A : Set) where
  module ParamA = Param A
  open ParamA

  works : (A → A) → A → A
  works G = S.F
    module works where
      module S = r A G


text:
{- Basic definitions using Σ-types

Σ-types are defined in Core/Primitives as they are needed for Glue types.

The file contains:

- Non-dependent pair types: A × B
- Mere existence: ∃[x ∈ A] B
- Unique existence: ∃![x ∈ A] B

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Sigma.Base where

open import Cubical.Core.Primitives public

open import Cubical.Foundations.Prelude
open import Cubical.HITs.PropositionalTruncation.Base

-- Non-dependent pair types

_×_ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
A × B = Σ A (λ _ → B)

infixr 5 _×_

-- Mere existence

∃ : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃ A B = ∥ Σ A B ∥

infix 2 ∃-syntax

∃-syntax : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃-syntax = ∃

syntax ∃-syntax A (λ x → B) = ∃[ x ∈ A ] B

-- Unique existence

∃! : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃! A B = isContr (Σ A B)

infix 2 ∃!-syntax

∃!-syntax : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
∃!-syntax = ∃!

syntax ∃!-syntax A (λ x → B) = ∃![ x ∈ A ] B

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 #-}
module Categories.Category.Dagger.Instance.Rels where

open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Level

open import Categories.Category.Dagger
open import Categories.Category.Instance.Rels

RelsHasDagger : ∀ {o ℓ} → HasDagger (Rels o ℓ)
RelsHasDagger = record
  { _† = flip
  ; †-identity = λ _ _ → (λ p → lift (sym (lower p))) , λ p → lift (sym (lower p))
  ; †-homomorphism = λ _ _ → map₂ swap , map₂ swap
  ; †-resp-≈ = flip
  ; †-involutive = λ _ _ _ → id , id
  }

RelsDagger : ∀ o ℓ → DaggerCategory (suc o) (suc (o ⊔ ℓ)) (o ⊔ ℓ)
RelsDagger o ℓ = record
  { C = Rels o ℓ
  ; hasDagger = RelsHasDagger
  }


text:
module Categories.Fam where

open import Level
open import Relation.Binary using (Rel)
import Relation.Binary.HeterogeneousEquality as Het
open Het using (_≅_) renaming (refl to ≣-refl)

open import Categories.Support.PropositionalEquality

open import Categories.Category

module Fam {a b : Level} where
  record Fam : Set (suc a ⊔ suc b) where
      constructor _,_
      field
        U : Set a
        T : U → Set b
  open Fam public

  record Hom (A B : Fam) : Set (a ⊔ b) where
    constructor _,_
    field
      f : U A → U B
      φ : (x : U A) → T A x → T B (f x)

  record _≡Fam_ {X Y} (f g : (Hom X Y)) : Set (a ⊔ b) where
      constructor _,_
      field
        f≡g : {x : _} → Hom.f f x ≣ Hom.f g x
        φ≡γ : {x : _} {bx : _} → Hom.φ f x bx ≅ Hom.φ g x bx

  module Eq = _≡Fam_

  Cat : Category (suc a ⊔ suc b) (a ⊔ b) (a ⊔ b)
  Cat = record {
                Obj = Fam;
                _⇒_ = Hom;
                _≡_ = _≡Fam_;
                id = id′;
                _∘_ = _∘′_;
                assoc = ≣-refl , ≣-refl;
                identityˡ = ≣-refl , ≣-refl;
                identityʳ = ≣-refl , ≣-refl;
                equiv = record {
                  refl  = ≣-refl , ≣-refl;
                  sym   = \ { (f≡g , φ≡γ) → ≣-sym f≡g , Het.sym φ≡γ };
                  trans = λ {(f≡g , φ≡γ) (g≡h , γ≡η) → ≣-trans f≡g g≡h , Het.trans φ≡γ γ≡η} };
                ∘-resp-≡ = ∘-resp-≡′ }
   where
     id′ : {A : Fam} → Hom A A
     id′ = (\ x → x) , (\ x bx → bx)

     _∘′_ : {A B C : Fam} → Hom B C → Hom A B → Hom A C
     _∘′_ (f , φ) (g , γ) = (λ x → f (g x)) , (λ x bx → φ (g x) (γ x bx))

     sym′ : ∀ {X Y} → Relation.Binary.Symmetric (_≡Fam_ {X} {Y})
     sym′ {Ax , Bx} {Ay , By} {f , φ} {g , γ} (f≡g , φ≡γ) = ≣-sym f≡g , Het.sym φ≡γ

     ∘-resp-≡′ : {A B C : Fam} {f h : Hom B C} {g i : Hom A B} → f ≡Fam h → g ≡Fam i → (f ∘′ g) ≡Fam (h ∘′ i)
     ∘-resp-≡′ {f = (f , φ)} {g , γ} {h , η} {i , ι} (f≡g , φ≡γ) (h≡i , η≡ι) =
       ≣-trans f≡g (≣-cong g h≡i) , Het.trans φ≡γ (Het.cong₂ γ (Het.≡-to-≅ h≡i) η≡ι)

  open Category Cat public

Fam : ∀ a b → Category (suc a ⊔ suc b) (a ⊔ b) (a ⊔ b)
Fam a b = Fam.Cat {a} {b}


text:
record R (A : Set) : Set where
  constructor c₂
  field
    f : A → A

  g : A → A
  g x = f (f x)

open R public

_ : (@0 A : Set) → R A → A → A
_ = λ A → g {A = A}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module SetoidEquiv where

open import Level using (Level; _⊔_)
open import Function.Equality using (_∘_; _⟶_; _⟨$⟩_)
open import Relation.Binary using (Setoid; module Setoid)
open import Relation.Binary.PropositionalEquality as P using (setoid)

open Setoid

infix 4 _≃S_

------------------------------------------------------------------------------
-- A setoid gives us a set and an equivalence relation on that set.
-- A common equivalence relation that is used on setoids is ≡

-- In general, two setoids are equivalent if:

record _≃S_ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} (A : Setoid ℓ₁ ℓ₂) (B : Setoid ℓ₃ ℓ₄) :
  Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  constructor equiv
  field
    f : A ⟶ B
    g : B ⟶ A
    α : ∀ {x y} → _≈_ B x y → _≈_ B ((f ∘ g) ⟨$⟩ x) y
    β : ∀ {x y} → _≈_ A x y → _≈_ A ((g ∘ f) ⟨$⟩ x) y

-- Abbreviation for the special case in which the equivalence relation
-- is just ≡:

_≃S≡_ : ∀ {ℓ₁} → (A B : Set ℓ₁) → Set ℓ₁
A ≃S≡ B = (P.setoid A) ≃S (P.setoid B)

-- Two equivalences between setoids are themselves equivalent if

record _≋_ {ℓ₁} {A B : Set ℓ₁} (eq₁ eq₂ : A ≃S≡ B) : Set ℓ₁ where
  constructor equivS
  field
    f≡ : ∀ (x : A) → P._≡_ (_≃S_.f eq₁ ⟨$⟩ x) (_≃S_.f eq₂ ⟨$⟩ x)
    g≡ : ∀ (x : B) → P._≡_ (_≃S_.g eq₁ ⟨$⟩ x) (_≃S_.g eq₂ ⟨$⟩ x)
    -- note that this appears to be redundant (especially when looking
    -- at the proofs), but having both f and g is needed for inference
    -- of other aspects to succeed.

id≋ : ∀ {ℓ} {A B : Set ℓ} {x : A ≃S≡ B} → x ≋ x
id≋ = record { f≡ = λ x → P.refl ; g≡ = λ x → P.refl }

sym≋ : ∀ {ℓ} {A B : Set ℓ} {x y : A ≃S≡ B} → x ≋ y → y ≋ x
sym≋ (equivS f≡ g≡) = equivS (λ a → P.sym (f≡ a)) (λ b → P.sym (g≡ b))

trans≋ : ∀ {ℓ} {A B : Set ℓ} {x y z : A ≃S≡ B} → x ≋ y → y ≋ z → x ≋ z
trans≋ (equivS f≡ g≡) (equivS h≡ i≡) =
   equivS (λ a → P.trans (f≡ a) (h≡ a)) (λ b → P.trans (g≡ b) (i≡ b))

-- The set of equivalences between setoids is itself is a setoid
-- WARNING: this is not generic, but specific to ≡-Setoids of functions.

≃S-Setoid : ∀ {ℓ₁} → (A B : Set ℓ₁) → Setoid ℓ₁ ℓ₁
≃S-Setoid {ℓ₁} A B = record
  { Carrier = AS ≃S BS
  ; _≈_ = _≋_
  ; isEquivalence = record
    { refl = id≋
    ; sym = sym≋
    ; trans = trans≋
    }
  }
  where
    open _≃S_
    AS = P.setoid A
    BS = P.setoid B

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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.ConsensusTypes.BlockData  as BlockData
import      LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert as QuorumCert
import      LibraBFT.Impl.Types.BlockInfo                     as BlockInfo
import      LibraBFT.Impl.Types.ValidatorVerifier             as ValidatorVerifier
open import LibraBFT.Impl.OBM.Crypto
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Hash
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                       using (String)

module LibraBFT.Impl.Consensus.ConsensusTypes.Block where

genBlockInfo : Block → HashValue → Version → Maybe EpochState → BlockInfo
genBlockInfo b executedStateId version nextEpochState = BlockInfo∙new
  (b ^∙ bEpoch) (b ^∙ bRound) (b ^∙ bId) executedStateId version nextEpochState

isGenesisBlock : Block → Bool
isGenesisBlock b = BlockData.isGenesisBlock (b ^∙ bBlockData)

isNilBlock : Block → Bool
isNilBlock b = BlockData.isNilBlock (b ^∙ bBlockData)

makeGenesisBlockFromLedgerInfo : LedgerInfo → Either ErrLog Block
makeGenesisBlockFromLedgerInfo li = do
  blockData <- BlockData.newGenesisFromLedgerInfo li
  pure (Block∙new (hashBD blockData) blockData nothing)

newNil : Round → QuorumCert → Block
newNil r qc = Block∙new (hashBD blockData) blockData nothing
 where blockData = BlockData.newNil r qc

newProposalFromBlockDataAndSignature : BlockData → Signature → Block
newProposalFromBlockDataAndSignature blockData signature =
  Block∙new (hashBD blockData) blockData (just signature)

validateSignature : Block → ValidatorVerifier → Either ErrLog Unit
validateSignature self validator = case self ^∙ bBlockData ∙ bdBlockType of λ where
  Genesis             → Left fakeErr -- (ErrL (here' ["do not accept genesis from others"]))
  NilBlock            → QuorumCert.verify (self ^∙ bQuorumCert) validator
  (Proposal _ author) → do
    fromMaybeM
      (Left fakeErr) -- (ErrL (here' ["Missing signature in Proposal"])))
      (pure (self ^∙ bSignature)) >>= λ sig -> withErrCtx' (here' [])
        (ValidatorVerifier.verify validator author (self ^∙ bBlockData) sig)
    QuorumCert.verify (self ^∙ bQuorumCert) validator
 where
  here' : List String → List String
  here' t = "Block" ∷ "validateSignatures" {-∷ lsB self-} ∷ t

verifyWellFormed : Block → Either ErrLog Unit
verifyWellFormed self = do
  lcheck (not (isGenesisBlock self))
         (here' ("Do not accept genesis from others" ∷ []))
  let parent = self ^∙ bQuorumCert ∙ qcCertifiedBlock
  lcheck (parent ^∙ biRound <? self ^∙ bRound)
         (here' ("Block must have a greater round than parent's block" ∷ []))
  lcheck (parent ^∙ biEpoch == self ^∙ bEpoch)
         (here' ("block's parent should be in the same epoch" ∷ []))
  lcheck (not (BlockInfo.hasReconfiguration parent)
          ∨ maybe true payloadIsEmpty (self ^∙ bPayload))
         (here' ("Reconfiguration suffix should not carry payload" ∷ []))
  -- timestamps go here -- Haskell removed them
  lcheck (not (self ^∙ bQuorumCert ∙ qcEndsEpoch))
         (here' ("Block cannot be proposed in an epoch that has ended" ∷ []))
  lcheck (self ^∙ bId == hashBD (self ^∙ bBlockData))
         (here' ("Block id hash mismatch" ∷ []))
 where
  here' : List String → List String
  here' t = "Block" ∷ "verifyWellFormed" {-∷ lsB self-} ∷ t


text:
-- Andreas, 2013-10-21 fixed this issue
-- by refactoring Internal to spine syntax.
module Issue901 where

open import Common.Level

record Ls : Set where
  constructor _,_
  field
    fst : Level
    snd : Level
open Ls

record R (ls : Ls) : Set (lsuc (fst ls ⊔ snd ls)) where
  field
    A : Set (fst ls)
    B : Set (snd ls)

bad : R _
bad = record { A = Set; B = Set₁ }

good : R (_ , _)
good = record { A = Set; B = Set₁ }

{- PROBLEM WAS:

"good" is fine while the body and signature of "bad" are marked in yellow.
Both are fine if we change the parameter of R to not contain levels.

The meta _1 in R _ is never eta-expanded somehow.  I think this
problem will vanish if we let whnf eta-expand metas that are
projected.  E.g.

  fst _1

will result in

  _1 := _2,_3

and then reduce to

  _2

(And that would be easier to implement if Internal was a spine syntax
(with post-fix projections)).  -}


text:
module halt where

open import Level renaming ( zero to Zero ; suc to Suc )
open import Data.Nat
open import Data.Maybe
open import Data.List hiding ([_])
open import Data.Nat.Properties
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import  Relation.Binary.Core hiding (_⇔_)
open import  Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality

open import logic

record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
   field
       fun←  :  S → R
       fun→  :  R → S
       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
--  normal bijection required below, but we don't need this to show the inconsistency
--     fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x

injection' :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
injection' R S f = (x y : R) → f x ≡ f y → x ≡ y

open HBijection

diag : {S : Set }  (b : HBijection  ( S → Bool ) S) → S → Bool
diag b n = not (fun← b n n)

diagonal : { S : Set } → ¬ HBijection  ( S → Bool ) S
diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
    diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n )
    diagn1 n dn = ¬t=f (diag b n ) ( begin
           not (diag b n)
        ≡⟨⟩
           not (not fun← b n n)
        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
           not (fun← b (fun→ b (diag b))  n)
        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
           not (fun← b n n)
        ≡⟨⟩
           diag b n
        ∎ ) where open ≡-Reasoning

record TM : Set where
   field
      tm : List Bool → Maybe Bool

open TM

record UTM : Set where
   field
      utm : TM
      encode : TM → List Bool
      is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x

open UTM

open _∧_

open import Axiom.Extensionality.Propositional
postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n

record Halt : Set where
   field
      halt :  (t : TM ) → (x : List Bool ) → Bool
      is-halt :     (t : TM ) → (x : List Bool ) → (halt t x ≡ true )  ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
      is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )

open Halt

TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
TNL halt utm = record {
       fun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
     ; fun→  = λ h  → encode utm record { tm = h1 h }
     ; fiso← = λ h →  f-extensionality (λ y → TN1 h y )
  } where
     open ≡-Reasoning
     h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
     h1 h x with h x
     ... | true =  just true
     ... | false = nothing
     tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool
     tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y
     h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing
     h-nothing h y eq with h y
     h-nothing h y refl | false = refl
     h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true
     h-just h y eq with h y
     h-just h y refl | true = refl
     TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
     TN1 h y with h y | inspect h y
     ... | true  | record { eq = eq1 } = begin
        Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
        true ∎  where
          tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ just true
          tm-tenc = begin
              tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
              h1 h y ≡⟨ h-just h y eq1  ⟩
              just true  ∎
     ... | false | record { eq = eq1 } = begin
        Halt.halt halt (UTM.utm utm)  (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
        false ∎  where
          tm-tenc :  tm (UTM.utm utm) (tenc h y) ≡ nothing
          tm-tenc = begin
              tm (UTM.utm utm) (tenc h y)  ≡⟨  is-tm utm _ y ⟩
              h1 h y ≡⟨  h-nothing h y eq1 ⟩
              nothing  ∎
     -- the rest of bijection means encoding is unique
     -- fiso→ :  (y : List Bool ) → encode utm record { tm = λ x →  h1 (λ tm → Halt.halt halt (UTM.utm utm) tm  ) x } ≡ y

TNL1 : UTM → ¬ Halt
TNL1 utm halt = diagonal ( TNL halt utm )

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda