text:
{-# OPTIONS --rewriting #-}
open import ExtractSac as ES using ()
open import Extract (ES.kompile-fun)

open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.Fin using (Fin; zero; suc; #_)

open import Relation.Binary.PropositionalEquality

open import Reflection

open import Structures
open import Function

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE +-identityʳ #-}

test1-f : ℕ → ℕ
test1-f x = 1 + x

test₁ : kompile test1-f [] [] ≡ (ok $ "\n\n// Function Example-00.test1-f\n"
                                   ++ "int\n"
                                   ++ "Example_00_test1_f(int x_1) {\n"
                                   ++ "int __ret;\n"
                                   ++ "x = x_1;\n"
                                   ++ "__ret = (1 + x);\n"
                                   ++ "return __ret;\n"
                                   ++ "}\n\n")
test₁ = refl

test2-f : ℕ → ℕ
test2-f x = 0

test₂ : kompile test2-f [] [] ≡ (ok $ "\n\n// Function Example-00.test2-f\n"
                                   ++ "int\n"
                                   ++ "Example_00_test2_f(int x_1) {\n"
                                   ++ "int __ret;\n"
                                   ++ "x = x_1;\n"
                                   ++ "__ret = 0;\n"
                                   ++ "return __ret;\n"
                                   ++ "}\n\n")
test₂ = refl

-- Rewriting test
test3-f : ℕ → ℕ
test3-f x = x + 0

test₃ : kompile test3-f [] [] ≡ (ok $ "\n\n// Function Example-00.test3-f\n"
                                   ++ "int\n"
                                   ++ "Example_00_test3_f(int x_1) {\n"
                                   ++ "int __ret;\n"
                                   ++ "x = x_1;\n"
                                   ++ "__ret = x;\n"
                                   ++ "return __ret;\n"
                                   ++ "}\n\n")
test₃ = refl

-- Make sure that we can deal with functions inside
-- the type and properly collect them while extraction.
test-4h : ℕ → ℕ
test-4h x = 1 + x

test-4f : Fin (test-4h 3) → Fin 4
test-4f a = zero

test₄ : kompile test-4f (quote test-4h ∷ []) [] ≡ ok _
test₄ = refl

-- Test if we can deal with multiple patterns.
module _ where
  test-5f : ℕ → ℕ
  test-5f (suc (suc x)) = x
  test-5f _ = 0

  test₅ : kompile test-5f [] [] ≡ ok _
  test₅ = refl

  test-6f : Fin 5 → Fin 3
  test-6f (suc (suc x)) = x
  test-6f _ = zero

-- Make sure that we are compiling multi-argument function correctly
test-7f : (a b c : ℕ) → ℕ
test-7f a b c = c

test₇ : kompile test-7f [] [] ≡ (ok $ "\n\n// Function Example-00.test-7f\nint\nExample_00_test_7f(int x_1, int x_2, int x_3) {\n"
                                   ++ "int __ret;\na = x_1;\nb = x_2;\nc = x_3;\n__ret = c;\nreturn __ret;\n}\n\n")
test₇ = refl

-- With-clauses
test-8f : ℕ → ℕ
test-8f x with x
test-8f x | zero = 0
test-8f x | _    = 1

test₈ : kompile test-8f [] [] ≡ ok _
test₈ = refl

-- Testing lists
test-9f : List ℕ → List ℕ
test-9f [] = []
test-9f (x ∷ xs) = 1 + x ∷ test-9f xs

test₉ : kompile test-9f [] [] ≡ ok _
test₉ = refl

-- Test constraints accumulated from the list type.
module _ where
  test-10f : (n : ℕ) → List (Fin n) → ℕ
  test-10f n xs = 10
  test₁₀ : kompile test-10f [] [] ≡ ok _
  test₁₀ = refl

  -- Higher-order functions are not allowed:
  test-11f : ℕ → List (ℕ → ℕ)
  test-11f n = []
  test₁₁ : _≡_ {A = Prog} (kompile test-11f [] []) $ error _
  test₁₁ = refl

  -- Lists can bring per-element constraints, which we are currently
  -- generating with foreach macro.
  test-12f : (n : ℕ) → List (List $ Fin n) → ℕ
  test-12f n xs = 10
  test₁₂ : _≡_ {A = Prog} (kompile test-12f [] []) $ error _
  test₁₂ = refl

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


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

module ScaleDegree where

open import Data.Fin        using (Fin; toℕ; #_)
open import Data.Nat        using (ℕ; suc; _+_)
open import Data.Nat.DivMod using (_mod_; _div_)
open import Data.Product    using (_×_; _,_)
open import Data.Vec        using (lookup)

open import Pitch

ScaleDegree : ℕ → Set
ScaleDegree = Fin

ScaleDegreeOctave : ℕ → Set
ScaleDegreeOctave n = ScaleDegree n × Octave

transposeScaleDegree : {n : ℕ} → ℕ → ScaleDegreeOctave (suc n) → ScaleDegreeOctave (suc n)
transposeScaleDegree {n} k (d , o) =
  let d' = (toℕ d) + k
  in d' mod (suc n) , o + (d' div (suc n))

scaleDegreeToPC : {n : ℕ} → Scale n → ScaleDegree n → PC
scaleDegreeToPC scale d = lookup scale d

ext: agda

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Data.Product using ( _,_ ; proj₁ ; proj₂ )
open import Web.Semantic.DL.ABox.Interp using
  ( Interp ; _*_ ; ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; _**_ ; ≲-refl )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; _⊨b_ ; *-resp-⟨ABox⟩ ; ⊨a-resp-≲ )
open import Web.Semantic.DL.Category.Object using
  ( Object ; _,_ ; IN ; fin ; iface )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; _,_ ; BN ; impl
  ; apply ; apply✓ ; apply-init )
open import Web.Semantic.DL.Category.Wiring using
  ( identity ; wires-≈ ; wires-≈⁻¹ )
open import Web.Semantic.DL.Category.Composition using
  ( _∙_ ; ⊨a-intro-⟫ ; ⊨b-intro-⟫ )
open import Web.Semantic.DL.Integrity using ( med-≲ ; init-med )
open import Web.Semantic.DL.KB using ( _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox ; _,_ )
open import Web.Semantic.DL.TBox.Interp using ( _⊨_≈_ )
open import Web.Semantic.Util using
  ( id ; _⊕_⊕_ ; inode ; bnode ; enode ; left ; right )

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

identity-elim : ∀ (A : Object S T) I → (I ⊨a impl (identity A)) →
  ∀ x → (⌊ I ⌋ ⊨ ind I (inode x) ≈ ind I (enode x))
identity-elim (X , X∈Fin , A) I I⊨id x = wires-≈ id (proj₂ X∈Fin x) I⊨id

identity-intro : ∀ (A : Object S T) I →
  (∀ x → (⌊ I ⌋ ⊨ ind I (inode x) ≈ ind I (enode x))) →
    (I ⊨a impl (identity A))
identity-intro (X , X∈Fin , A) I ∀x∙x₁≈x₂ = wires-≈⁻¹ id ∀x∙x₁≈x₂ (proj₁ X∈Fin)

compose-left : ∀ {A B C : Object S T} (F : A ⇒ B) (G : B ⇒ C) I →
  (I ⊨a impl (F ∙ G)) → (left * I ⊨a impl F)
compose-left {X , X∈Fin , A} {Y , Y∈Fin , B} {Z , Z∈Fin , C}
  (V , F , F✓) (W , G , G✓) I (I⊨F , I⊨G) =
    *-resp-⟨ABox⟩ left I F I⊨F

compose-right : ∀ {A B C : Object S T} (F : A ⇒ B) (G : B ⇒ C) I →
  (I ⊨a impl (F ∙ G)) → (right * I ⊨a impl G)
compose-right {X , X∈Fin , A} {Y , Y∈Fin , B} {Z , Z∈Fin , C}
  (V , F , F✓) (W , G , G✓) I (I⊨F , I⊨G) =
    *-resp-⟨ABox⟩ right I G I⊨G

compose-mid : ∀ {A B C : Object S T} (F : A ⇒ B) (G : B ⇒ C)
  (I : Interp Σ (IN A ⊕ (BN F ⊕ IN B ⊕ BN G) ⊕ IN C)) →
    (inode * I ⊨ (S , T) , iface A) → (I ⊨a impl (F ∙ G)) →
      (bnode * bnode * I ⊨ (S , T) , iface B)
compose-mid {A} {B} {C} F G I ((I⊨S , I⊨T) , I⊨A) I⊨F⟫G =
  ((I⊨S , I⊨T) , ⊨a-resp-≲ (enode ** J≲I) (iface B) J⊨B) where

  J : Interp Σ (IN A ⊕ BN F ⊕ IN B)
  J = apply F (inode * I) ((I⊨S , I⊨T) , I⊨A)

  J⊨B : enode * J ⊨a iface B
  J⊨B = proj₂ (apply✓ F (inode * I) ((I⊨S , I⊨T) , I⊨A))

  J≲I : J ≲ left * I
  J≲I = med-≲ (init-med (apply-init F (inode * I) ((I⊨S , I⊨T) , I⊨A))
    (left * I) (≲-refl (inode * I)) (I⊨S , compose-left F G I I⊨F⟫G))

compose-resp-⊨a : ∀ {A B C : Object S T} (F : A ⇒ B) (G : B ⇒ C) I →
  (left * I ⊨a impl F) → (right * I ⊨a impl G) → (I ⊨a impl (F ∙ G))
compose-resp-⊨a {X , X∈Fin , A} {Y , Y∈Fin , B} {Z , Z∈Fin , C}
  (V , F , F✓) (W , G , G✓) I I⊨F I⊨G =
    ⊨a-intro-⟫ I F G I⊨F I⊨G

compose-resp-⊨b : ∀ {A B C : Object S T} {V W : Set} (F : A ⇒ B) (G : B ⇒ C)
  (I : Interp Σ (IN A ⊕ (V ⊕ IN B ⊕ W) ⊕ IN C)) →
    (left * I ⊨b impl F) → (right * I ⊨b impl G) → (I ⊨b impl (F ∙ G))
compose-resp-⊨b {X , X∈Fin , A} {Y , Y∈Fin , B} {Z , Z∈Fin , C}
  (V , F , F✓) (W , G , G✓) I I⊨F I⊨G =
    ⊨b-intro-⟫ I F G I⊨F I⊨G

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
{-# OPTIONS --rewriting --confluence-check #-}
module Issue4333.N0 where

open import Issue4333.M
{-# REWRITE p₀ #-}

b₀' : B a₀'
b₀' = b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Relation.Relation where

open import Level renaming (suc to lsuc)
open import Data.Product

-- Partial equivalence relations.
record ParRel {l l' : Level}{A : Set l}(R : A → A → Set l') : Set (l ⊔ l') where
  field
    symPf   : ∀{x y} → R x y → R y x
    transPf : ∀{x y z} → R x y → R y z → R x z

-- (Total) equivalence relation.
record EqRel {l l' : Level}{A : Set l}(R : A → A → Set l') : Set (l ⊔ l') where
  field
    parEqPf : ParRel R
    refPf   : ∀{x} → R x x

open ParRel public
open EqRel public

-- The product of two relations.
ProductRel : {l l' : Level}{A : Set l}{B : Set l'}
  → (R : A → A → Set l)
  → (R' : B → B → Set l')
  → (A × B → A × B → Set (l ⊔ l'))
ProductRel R R' a b = (R (proj₁ a) (proj₁ b)) × (R' (proj₂ a) (proj₂ b))

-- The product of two partial equivalence relations is also a partial
-- equivalence relation.
ProductRelIsParRel : {l l' : Level}{A : Set l}{B : Set l'}
  → (R : A → A → Set l)
  → (R' : B → B → Set l')
  → ParRel R
  → ParRel R'
  → ParRel (ProductRel R R')
ProductRelIsParRel R R' erPF₁ erPF₂ =
  record { symPf   = λ x₁ → symPf erPF₁ (proj₁ x₁) , symPf erPF₂ (proj₂ x₁);
           transPf = λ x₁ x₂ → (transPf erPF₁ (proj₁ x₁) (proj₁ x₂)) , (transPf erPF₂ (proj₂ x₁) (proj₂ x₂)) }

-- The product of two (total) equivalence relations is also a (total)
-- equivalence relation.
ProductRelIsEqRel : {l l' : Level}{A : Set l}{B : Set l'}
  → (R : A → A → Set l)
  → (R' : B → B → Set l')
  → EqRel R
  → EqRel R'
  → EqRel (ProductRel R R')
ProductRelIsEqRel R R' erPF₁ erPF₂ =
  record { parEqPf = ProductRelIsParRel R R' (parEqPf erPF₁) (parEqPf erPF₂);
           refPf   = λ {x} → (refPf erPF₁ {proj₁ x}) , (refPf erPF₂ {proj₂ x}) }

-- The restriction of a relation by a predicate.
_↓_ : {l l' : Level}
      {A : Set l}
    → (R : A → A → Set l)
    → (P : A → Set l')
    → Set (l ⊔ l')
_↓_ {A = A} R P = Σ[ f ∈ A ] (P f)

-- The restriction of a paritial equivalence is also a partial
-- equivalence.
↓ParRel : {l l' : Level}
          {A : Set l}
        → (R : A → A → Set l)
        → (P : A → Set l')
        → ParRel R
        → ParRel (λ (f g : R ↓ P) → R (proj₁ f) (proj₁ g))
↓ParRel R P prPF = record { symPf = λ x₁ → symPf prPF x₁; transPf = λ x₁ x₂ → transPf prPF x₁ x₂ }

-- The restriction of an equivalence relation is also an equivalence
-- relation.
↓EqRel : {l l' : Level}
         {A : Set l}
       → (R : A → A → Set l)
       → (P : A → Set l')
       → EqRel R
       → EqRel (λ (f g : R ↓ P) → R (proj₁ f) (proj₁ g))
↓EqRel R P eqrPF = record { parEqPf = ↓ParRel R P (parEqPf eqrPF); refPf = refPf eqrPF }

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Agda.Primitive public

variable
 ℓ ℓ' : Level

data _≡_ {X : Set ℓ} : X → X → Set ℓ where
  refl : {x : X} → x ≡ x

ap : {X : Set ℓ} {Y : Set ℓ'} (f : X → Y) {x x' : X} → x ≡ x' → f x ≡ f x'
ap f refl = refl

_∙_ : {X : Set ℓ} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙ refl = p

yoneda-elem-lc : {X : Set ℓ} {x : X} {A : X → Set ℓ'} (η θ : (y : X) → x ≡ y → A y)
               → η x refl ≡ θ x refl → ∀ y p → η y p ≡ θ y p
yoneda-elem-lc η θ q y refl = ap (λ a → a) q

ext-assoc : {X : Set ℓ} {z t : X} (r : z ≡ t)
          → (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → (p ∙ q) ∙ r)
          ≡ (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → p ∙ (q ∙ r))
ext-assoc {ℓ} {X} {z} {t} = yoneda-elem-lc
                            -- {A = λ - → (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ - }
                            (λ z r x y p q → (p ∙ q) ∙ r)
                            (λ z r x y p q → p ∙ (q ∙ r))
                            refl
                            t

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Generic.Test.Experiment where

open import Generic.Lib.Prelude

data Desc (I : Set) : Set₁ where
  ret : I -> Desc I
  π   : (A : Set) -> (A -> Desc I) -> Desc I
  _⊕_ : Desc I -> Desc I -> Desc I

data RecDesc (I : Set) : Set₁ where
  rec : ((I -> Set) -> Desc I) -> RecDesc I

⟦_⟧ : ∀ {I} -> Desc I -> (I -> Set) -> I -> Set
⟦ ret i ⟧ B j = i ≡ j
⟦ π A D ⟧ B j = ∃ λ x -> ⟦ D x ⟧ B j
⟦ D ⊕ E ⟧ B j = ⟦ D ⟧ B j ⊎ ⟦ E ⟧ B j

⟦_⟧ʳ : ∀ {I} -> RecDesc I -> (I -> Set) -> I -> Set
⟦ rec K ⟧ʳ B j = ⟦ K B ⟧ B j

{-# NO_POSITIVITY_CHECK #-}
data μ {I} (D : RecDesc I) j : Set where
  node : ⟦ D ⟧ʳ (μ D) j -> μ D j

DescEq : ∀ {I} -> Desc I -> Set
DescEq (ret i) = ⊤
DescEq (π A D) = Eq A × ∀ x -> DescEq (D x)
DescEq (D ⊕ E) = DescEq D × DescEq E

RecDescEq : ∀ {I} -> RecDesc I -> Set₁
RecDescEq (rec K) = ∀ {B} {{eqB : ∀ {i} -> Eq (B i)}} -> DescEq (K B)

instance
  {-# TERMINATING #-}
  DataEq : ∀ {I} {D : RecDesc I} {j} {{recDescEq : RecDescEq D}} -> Eq (μ D j)
  DataEq {D = D} {j} = record
    { _≟_ = eqMu
    } where
        node-inj : ∀ {I D j x y} -> node {I} {D} {j} x ≡ node y -> x ≡ y
        node-inj refl = refl

        eqSem : ∀ {j} D₀ D {{descEq : DescEq D}} -> IsSet (⟦ D ⟧ (μ D₀) j)
        eqSem D₀ (ret i)               refl refl = yes refl
        eqSem D₀ (π A D) {{eqA , eqD}} p₁   p₂   =
          decProd (_≟_ {{eqA}}) (eqSem D₀ (D _) {{eqD _}}) p₁ p₂
        eqSem D₀ (D ⊕ E) {{eqD , eqE}} s₁   s₂   =
          decSum (eqSem D₀ D {{eqD}}) (eqSem D₀ E {{eqE}}) s₁ s₂

        eqMu : ∀ {D} {{recDescEq : RecDescEq D}} -> IsSet (μ D j)
        eqMu {D@(rec K)} {{recDescEq}} (node d₁) (node d₂) =
          dcong node node-inj (eqSem D _ {{recDescEq {{DataEq {D = D}}}}} d₁ d₂)

module Example1 where
  open import Generic.Main using (deriveEqTo)

  instance
    ListEq : {A : Set} {{eqA : Eq A}} -> Eq (List A)
    unquoteDef ListEq = deriveEqTo ListEq (quote List)

  data Rose (A : Set) : Set where
    rose : A -> List (Rose A) -> Rose A

  Rose′ : Set -> Set
  Rose′ A = flip μ tt $ rec λ Rose′ -> π A λ _ -> π (List (Rose′ tt)) λ _ -> ret tt

  pattern rose′ x rs = node (x , rs , refl)

  {-# TERMINATING #-}
  Rose→Rose′ : ∀ {A} -> Rose A -> Rose′ A
  Rose→Rose′ (rose x rs) = rose′ x (map Rose→Rose′ rs)

  {-# TERMINATING #-}
  Rose′→Rose : ∀ {A} -> Rose′ A -> Rose A
  Rose′→Rose (rose′ x rs) = rose x (map Rose′→Rose rs)

  arose : Rose′ ℕ
  arose = rose′ 4 (rose′ 1 (rose′ 6 [] ∷ []) ∷ rose′ 2 [] ∷ [])

  find : {A : Set} {{x : A}} -> A
  find {{x}} = x

  -- -- Instance search cannot be used to find elements in an explicit function type
  -- test : _≟_ {{DataEq {{λ {_} -> find}}}} arose arose ≡ yes refl
  -- test = refl

module Example2 where
  -- If `A` is a parameter, then this definition would be strictly positive,
  -- but I intentionally made it an index, because we can't make `A` a parameter
  -- in the described version of `D`.
  {-# NO_POSITIVITY_CHECK #-}
  data D : Set -> Set where
    ret : ∀ {A} -> A -> D A
    rec : ∀ {A} -> D (D A) -> D A

  D′ : Set -> Set
  D′ = μ $ rec λ D′ -> (π Set λ A -> π A λ _ -> ret A)
                     ⊕ (π Set λ A -> π (D′ (D′ A)) λ _ -> ret A)

  pattern ret′ x = node (inj₁ (_ , x , refl))
  pattern rec′ r = node (inj₂ (_ , r , refl))

  Dⁿ : ℕ -> Set -> Set
  Dⁿ  0      A = A
  Dⁿ (suc n) A = D (Dⁿ n A)

  D′ⁿ : ℕ -> Set -> Set
  D′ⁿ  0      A = A
  D′ⁿ (suc n) A = D′ (D′ⁿ n A)

  ⟨D→D′⟩ⁿ : ∀ {A} n -> D (Dⁿ n A) -> D′ (D′ⁿ n A)
  ⟨D→D′⟩ⁿ  0      (ret x) = ret′ x
  ⟨D→D′⟩ⁿ (suc n) (ret r) = ret′ (⟨D→D′⟩ⁿ  n      r)
  ⟨D→D′⟩ⁿ  n      (rec r) = rec′ (⟨D→D′⟩ⁿ (suc n) r)

  ⟨D′→D⟩ⁿ : ∀ {A} n -> D′ (D′ⁿ n A) -> D (Dⁿ n A)
  ⟨D′→D⟩ⁿ  0      (ret′ x) = ret x
  ⟨D′→D⟩ⁿ (suc n) (ret′ r) = ret (⟨D′→D⟩ⁿ  n      r)
  ⟨D′→D⟩ⁿ  n      (rec′ r) = rec (⟨D′→D⟩ⁿ (suc n) r)

  D→D′ : ∀ {A} -> D A -> D′ A
  D→D′ = ⟨D→D′⟩ⁿ 0

  D′→D : ∀ {A} -> D′ A -> D A
  D′→D = ⟨D′→D⟩ⁿ 0

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category
open import Categories.Object.Products
open import Categories.Object.Terminal
open import Level

module Categories.Object.Terminal.Exponentiating {o ℓ e : Level}
    (C : Category o ℓ e)
    (P : Products C) where

open Category C
open Products P
open Terminal terminal

open import Categories.Object.Exponentiating
import Categories.Object.Terminal.Exponentials

open Categories.Object.Terminal.Exponentials C terminal

⊤-exponentiating : Exponentiating C binary ⊤
⊤-exponentiating = record
  { exponential = λ {X : Obj} → [⊤↑ X ]-exponential
  }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Cubical.Data.FinSet.Binary.Small where

open import Cubical.Data.FinSet.Binary.Small.Base public
open import Cubical.Data.FinSet.Binary.Small.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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

module Fragment.Examples.CSemigroup.Arith.Atomic where

open import Fragment.Examples.CSemigroup.Arith.Base

-- Fully dynamic associativity

+-dyn-assoc₁ : ∀ {m n o} → (m + n) + o ≡ m + (n + o)
+-dyn-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-dyn-assoc₂ : ∀ {m n o p} → ((m + n) + o) + p ≡ m + (n + (o + p))
+-dyn-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-dyn-assoc₃ : ∀ {m n o p q} → (m + n) + o + (p + q) ≡ m + (n + o + p) + q
+-dyn-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-dyn-assoc₁ : ∀ {m n o} → (m * n) * o ≡ m * (n * o)
*-dyn-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-dyn-assoc₂ : ∀ {m n o p} → ((m * n) * o) * p ≡ m * (n * (o * p))
*-dyn-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-dyn-assoc₃ : ∀ {m n o p q} → (m * n) * o * (p * q) ≡ m * (n * o * p) * q
*-dyn-assoc₃ = fragment CSemigroupFrex *-csemigroup

-- Fully dynamic commutativity

+-dyn-comm₁ : ∀ {m n} → m + n ≡ n + m
+-dyn-comm₁ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm₂ : ∀ {m n o} → m + (n + o) ≡ (o + n) + m
+-dyn-comm₂ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm₃ : ∀ {m n o p} → (m + n) + (o + p) ≡ (p + o) + (n + m)
+-dyn-comm₃ = fragment CSemigroupFrex +-csemigroup

*-dyn-comm₁ : ∀ {m n} → m * n ≡ n * m
*-dyn-comm₁ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm₂ : ∀ {m n o} → m * (n * o) ≡ (o * n) * m
*-dyn-comm₂ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm₃ : ∀ {m n o p} → (m * n) * (o * p) ≡ (p * o) * (n * m)
*-dyn-comm₃ = fragment CSemigroupFrex *-csemigroup

-- Fully dynamic associavity and commutativity

+-dyn-comm-assoc₁ : ∀ {m n o} → (m + n) + o ≡ n + (m + o)
+-dyn-comm-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm-assoc₂ : ∀ {m n o p} → ((m + n) + o) + p ≡ p + (o + (n + m))
+-dyn-comm-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-dyn-comm-assoc₃ : ∀ {m n o p q} → (m + n) + o + (p + q) ≡ q + (p + o + n) + m
+-dyn-comm-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-dyn-comm-assoc₁ : ∀ {m n o} → (m * n) * o ≡ n * (m * o)
*-dyn-comm-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm-assoc₂ : ∀ {m n o p} → ((m * n) * o) * p ≡ p * (o * (n * m))
*-dyn-comm-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-dyn-comm-assoc₃ : ∀ {m n o p q} → (m * n) * o * (p * q) ≡ q * (p * o * n) * m
*-dyn-comm-assoc₃ = fragment CSemigroupFrex *-csemigroup

-- Partially static associativity

+-sta-assoc₁ : ∀ {m n} → (m + 2) + (3 + n) ≡ m + (5 + n)
+-sta-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-sta-assoc₂ : ∀ {m n o p} → (((m + n) + 5) + o) + p ≡ m + (n + (2 + (3 + (o + p))))
+-sta-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-sta-assoc₃ : ∀ {m n o p} → ((m + n) + 2) + (3 + (o + p)) ≡ m + ((n + 1) + (4 + o)) + p
+-sta-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-sta-assoc₁ : ∀ {m n} → (m * 2) * (3 * n) ≡ m * (6 * n)
*-sta-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-sta-assoc₂ : ∀ {m n o p} → (((m * n) * 6) * o) * p ≡ m * (n * (2 * (3 * (o * p))))
*-sta-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-sta-assoc₃ : ∀ {m n o p} → ((m * n) * 2) * (6 * (o * p)) ≡ m * ((n * 2) * (6 * o)) * p
*-sta-assoc₃ = fragment CSemigroupFrex *-csemigroup

-- Partially static commutativity

+-sta-comm₁ : ∀ {m} → m + 1 ≡ 1 + m
+-sta-comm₁ = fragment CSemigroupFrex +-csemigroup

+-sta-comm₂ : ∀ {m n} → m + (2 + n) ≡ (n + 2) + m
+-sta-comm₂ = fragment CSemigroupFrex +-csemigroup

+-sta-comm₃ : ∀ {m n o p} → (1 + (m + n)) + ((o + p) + 2) ≡ ((p + o) + 2) + (1 + (n + m))
+-sta-comm₃ = fragment CSemigroupFrex +-csemigroup

*-sta-comm₁ : ∀ {m} → m * 4 ≡ 4 * m
*-sta-comm₁ = fragment CSemigroupFrex *-csemigroup

*-sta-comm₂ : ∀ {m n} → m * (2 * n) ≡ (n * 2) * m
*-sta-comm₂ = fragment CSemigroupFrex *-csemigroup

*-sta-comm₃ : ∀ {m n o p} → (4 * (m * n)) * ((o * p) * 2) ≡ ((p * o) * 2) * (4 * (n * m))
*-sta-comm₃ = fragment CSemigroupFrex *-csemigroup

-- Partially static associavity and commutativity

+-sta-comm-assoc₁ : ∀ {m n o} → 1 + (m + n) + o + 4 ≡ 5 + n + (m + o)
+-sta-comm-assoc₁ = fragment CSemigroupFrex +-csemigroup

+-sta-comm-assoc₂ : ∀ {m n o p} → 5 + ((m + n) + o) + p ≡ p + ((o + 1) + (n + m)) + 4
+-sta-comm-assoc₂ = fragment CSemigroupFrex +-csemigroup

+-sta-comm-assoc₃ : ∀ {m n o p q} → (m + n + 1) + o + (p + q + 4) ≡ (2 + q) + (p + o + n) + (m + 3)
+-sta-comm-assoc₃ = fragment CSemigroupFrex +-csemigroup

*-sta-comm-assoc₁ : ∀ {m n o} → 2 * (m * n) * o * 3 ≡ 6 * n * (m * o)
*-sta-comm-assoc₁ = fragment CSemigroupFrex *-csemigroup

*-sta-comm-assoc₂ : ∀ {m n o p} → 6 * ((m * n) * o) * p ≡ p * ((o * 2) * (n * m)) * 3
*-sta-comm-assoc₂ = fragment CSemigroupFrex *-csemigroup

*-sta-comm-assoc₃ : ∀ {m n o p q} → (m * n * 3) * o * (p * q * 4) ≡ (2 * q) * (p * o * n) * (m * 6)
*-sta-comm-assoc₃ = fragment CSemigroupFrex *-csemigroup

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Inductive pointwise lifting of relations to vectors
------------------------------------------------------------------------

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

module Data.Vec.Relation.Binary.Pointwise.Inductive where

open import Algebra.FunctionProperties
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_)
open import Data.Vec as Vec hiding ([_]; head; tail; map; lookup)
open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
open import Level using (_⊔_)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

------------------------------------------------------------------------
-- Relation

infixr 5 _∷_

data Pointwise {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) :
               ∀ {m n} (xs : Vec A m) (ys : Vec B n) → Set (a ⊔ b ⊔ ℓ)
               where
  []  : Pointwise _∼_ [] []
  _∷_ : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n}
        (x∼y : x ∼ y) (xs∼ys : Pointwise _∼_ xs ys) →
        Pointwise _∼_ (x ∷ xs) (y ∷ ys)

length-equal : ∀ {a b m n ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ}
               {xs : Vec A m} {ys : Vec B n} →
               Pointwise _∼_ xs ys → m ≡ n
length-equal []          = P.refl
length-equal (_ ∷ xs∼ys) = P.cong suc (length-equal xs∼ys)

------------------------------------------------------------------------
-- Operations

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  head : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
         Pointwise _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
  head (x∼y ∷ xs∼ys) = x∼y

  tail : ∀ {m n x y} {xs : Vec A m} {ys : Vec B n} →
         Pointwise _∼_ (x ∷ xs) (y ∷ ys) → Pointwise _∼_ xs ys
  tail (x∼y ∷ xs∼ys) = xs∼ys

  lookup : ∀ {n} {xs : Vec A n} {ys : Vec B n} → Pointwise _∼_ xs ys →
           ∀ i → (Vec.lookup xs i) ∼ (Vec.lookup ys i)
  lookup (x∼y ∷ _)     zero    = x∼y
  lookup (_   ∷ xs∼ys) (suc i) = lookup xs∼ys i

  map : ∀ {ℓ₂} {_≈_ : REL A B ℓ₂} →
        _≈_ ⇒ _∼_ → ∀ {m n} → Pointwise _≈_ ⇒ Pointwise _∼_ {m} {n}
  map ∼₁⇒∼₂ []             = []
  map ∼₁⇒∼₂ (x∼y ∷ xs∼ys) = ∼₁⇒∼₂ x∼y ∷ map ∼₁⇒∼₂ xs∼ys

------------------------------------------------------------------------
-- Relational properties

refl : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} →
       ∀ {n} → Reflexive _∼_ → Reflexive (Pointwise _∼_ {n})
refl ∼-refl {[]}      = []
refl ∼-refl {x ∷ xs} = ∼-refl ∷ refl ∼-refl

sym : ∀ {a b ℓ} {A : Set a} {B : Set b}
      {P : REL A B ℓ} {Q : REL B A ℓ} {m n} →
      Sym P Q → Sym (Pointwise P) (Pointwise Q {m} {n})
sym sm []             = []
sym sm (x∼y ∷ xs∼ys) = sm x∼y ∷ sym sm xs∼ys

trans : ∀ {a b c ℓ} {A : Set a} {B : Set b} {C : Set c}
        {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {m n o} →
        Trans P Q R →
        Trans (Pointwise P {m}) (Pointwise Q {n} {o}) (Pointwise R)
trans trns []             []             = []
trans trns (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
  trns x∼y y∼z ∷ trans trns xs∼ys ys∼zs

decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
            Decidable _∼_ → ∀ {m n} → Decidable (Pointwise _∼_ {m} {n})
decidable dec []       []       = yes []
decidable dec []       (y ∷ ys) = no λ()
decidable dec (x ∷ xs) []       = no λ()
decidable dec (x ∷ xs) (y ∷ ys) with dec x y
... | no ¬x∼y = no (¬x∼y ∘ head)
... | yes x∼y with decidable dec xs ys
...   | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
...   | yes xs∼ys = yes (x∼y ∷ xs∼ys)

isEquivalence : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} →
                IsEquivalence _∼_ → ∀ n →
                IsEquivalence (Pointwise _∼_ {n})
isEquivalence equiv n = record
  { refl  = refl  (IsEquivalence.refl  equiv)
  ; sym   = sym   (IsEquivalence.sym   equiv)
  ; trans = trans (IsEquivalence.trans equiv)
  }

isDecEquivalence : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} →
                   IsDecEquivalence _∼_ → ∀ n →
                   IsDecEquivalence (Pointwise _∼_ {n})
isDecEquivalence decEquiv n = record
  { isEquivalence = isEquivalence (IsDecEquivalence.isEquivalence decEquiv) n
  ; _≟_           = decidable (IsDecEquivalence._≟_ decEquiv)
  }

setoid : ∀ {a ℓ} → Setoid a ℓ → ℕ → Setoid a (a ⊔ ℓ)
setoid S n = record
   { isEquivalence = isEquivalence (Setoid.isEquivalence S) n
   }

decSetoid : ∀ {a ℓ} → DecSetoid a ℓ → ℕ → DecSetoid a (a ⊔ ℓ)
decSetoid S n = record
   { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence S) n
   }

------------------------------------------------------------------------
-- map

module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where

  map⁺ : ∀ {ℓ₁ ℓ₂} {_∼₁_ : REL A B ℓ₁} {_∼₂_ : REL C D ℓ₂}
         {f : A → C} {g : B → D} →
         (∀ {x y} → x ∼₁ y → f x ∼₂ g y) →
         ∀ {m n xs ys} → Pointwise _∼₁_ {m} {n} xs ys →
         Pointwise _∼₂_ (Vec.map f xs) (Vec.map g ys)
  map⁺ ∼₁⇒∼₂ []             = []
  map⁺ ∼₁⇒∼₂ (x∼y ∷ xs∼ys) = ∼₁⇒∼₂ x∼y ∷ map⁺ ∼₁⇒∼₂ xs∼ys

------------------------------------------------------------------------
-- _++_

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  ++⁺ : ∀ {m n p q}
        {ws : Vec A m} {xs : Vec B p} {ys : Vec A n} {zs : Vec B q} →
        Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs)
  ++⁺ []            ys∼zs = ys∼zs
  ++⁺ (w∼x ∷ ws∼xs) ys∼zs = w∼x ∷ (++⁺ ws∼xs ys∼zs)

  ++ˡ⁻ : ∀ {m n}
         (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
         Pointwise _∼_ (ws ++ ys) (xs ++ zs) → Pointwise _∼_ ws xs
  ++ˡ⁻ []       []        _                    = []
  ++ˡ⁻ (w ∷ ws) (x ∷ xs) (w∼x ∷ ps) = w∼x ∷ ++ˡ⁻ ws xs ps

  ++ʳ⁻ : ∀ {m n}
         (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
         Pointwise _∼_ (ws ++ ys) (xs ++ zs) → Pointwise _∼_ ys zs
  ++ʳ⁻ [] [] ys∼zs = ys∼zs
  ++ʳ⁻ (w ∷ ws) (x ∷ xs) (_ ∷ ps) = ++ʳ⁻ ws xs ps

  ++⁻ : ∀ {m n}
        (ws : Vec A m) (xs : Vec B m) {ys : Vec A n} {zs : Vec B n} →
        Pointwise _∼_ (ws ++ ys) (xs ++ zs) →
        Pointwise _∼_ ws xs × Pointwise _∼_ ys zs
  ++⁻ ws xs ps = ++ˡ⁻ ws xs ps , ++ʳ⁻ ws xs ps

------------------------------------------------------------------------
-- concat

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  concat⁺ : ∀ {m n p q}
            {xss : Vec (Vec A m) n} {yss : Vec (Vec B p) q} →
            Pointwise (Pointwise _∼_) xss yss →
            Pointwise _∼_ (concat xss) (concat yss)
  concat⁺ []           = []
  concat⁺ (xs∼ys ∷ ps) = ++⁺ xs∼ys (concat⁺ ps)

  concat⁻ : ∀ {m n} (xss : Vec (Vec A m) n) (yss : Vec (Vec B m) n) →
            Pointwise _∼_ (concat xss) (concat yss) →
            Pointwise (Pointwise _∼_) xss yss
  concat⁻ []         []         [] = []
  concat⁻ (xs ∷ xss) (ys ∷ yss) ps =
    ++ˡ⁻ xs ys ps ∷ concat⁻ xss yss (++ʳ⁻ xs ys ps)

------------------------------------------------------------------------
-- tabulate

module _ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              (∀ i → f i ∼ g i) →
              Pointwise _∼_ (tabulate f) (tabulate g)
  tabulate⁺ {zero}  f∼g = []
  tabulate⁺ {suc n} f∼g = f∼g zero ∷ tabulate⁺ (f∼g ∘ suc)

  tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → B} →
              Pointwise _∼_ (tabulate f) (tabulate g) →
              (∀ i → f i ∼ g i)
  tabulate⁻ (f₀∼g₀ ∷ _)   zero    = f₀∼g₀
  tabulate⁻ (_     ∷ f∼g) (suc i) = tabulate⁻ f∼g i

------------------------------------------------------------------------
-- Degenerate pointwise relations

module _ {a b ℓ} {A : Set a} {B : Set b} {P : A → Set ℓ} where

  Pointwiseˡ⇒All : ∀ {m n} {xs : Vec A m} {ys : Vec B n} →
                   Pointwise (λ x y → P x) xs ys → All P xs
  Pointwiseˡ⇒All []       = []
  Pointwiseˡ⇒All (p ∷ ps) = p ∷ Pointwiseˡ⇒All ps

  Pointwiseʳ⇒All : ∀ {n} {xs : Vec B n} {ys : Vec A n} →
                   Pointwise (λ x y → P y) xs ys → All P ys
  Pointwiseʳ⇒All []       = []
  Pointwiseʳ⇒All (p ∷ ps) = p ∷ Pointwiseʳ⇒All ps

  All⇒Pointwiseˡ : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
                   All P xs → Pointwise (λ x y → P x) xs ys
  All⇒Pointwiseˡ {ys = []}    []       = []
  All⇒Pointwiseˡ {ys = _ ∷ _} (p ∷ ps) = p ∷ All⇒Pointwiseˡ ps

  All⇒Pointwiseʳ : ∀ {n} {xs : Vec B n} {ys : Vec A n} →
                   All P ys → Pointwise (λ x y → P y) xs ys
  All⇒Pointwiseʳ {xs = []}    []       = []
  All⇒Pointwiseʳ {xs = _ ∷ _} (p ∷ ps) = p ∷ All⇒Pointwiseʳ ps

------------------------------------------------------------------------
-- Pointwise _≡_ is equivalent to _≡_

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

  Pointwise-≡⇒≡ : ∀ {n} {xs ys : Vec A n} →
                  Pointwise _≡_ xs ys → xs ≡ ys
  Pointwise-≡⇒≡ []               = P.refl
  Pointwise-≡⇒≡ (P.refl ∷ xs∼ys) = P.cong (_ ∷_) (Pointwise-≡⇒≡ xs∼ys)

  ≡⇒Pointwise-≡ : ∀ {n} {xs ys : Vec A n} →
                  xs ≡ ys → Pointwise _≡_ xs ys
  ≡⇒Pointwise-≡ P.refl = refl P.refl

  Pointwise-≡↔≡ : ∀ {n} {xs ys : Vec A n} →
                  Pointwise _≡_ xs ys ⇔ xs ≡ ys
  Pointwise-≡↔≡ = equivalence Pointwise-≡⇒≡ ≡⇒Pointwise-≡

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

-- Version 0.15

Pointwise-≡ = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Pointwise-≡
"Warning: Pointwise-≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}


text:
module map-++-distribute where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import lists using (List; []; _∷_; _++_; map)

-- リストの結合に関するmapの分配法則の証明
map-++-distribute : {A B : Set} → (f : A → B) → (xs ys : List A)
  → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-distribute f [] ys =
  begin
    map f ([] ++ ys)
  ≡⟨⟩
    map f ys
  ≡⟨⟩
    map f [] ++ map f ys
  ∎
map-++-distribute f (x ∷ xs) ys =
  begin
    map f ((x ∷ xs) ++ ys)
  ≡⟨⟩
    f x ∷ map f (xs ++ ys)
  ≡⟨ cong (f x ∷_) (map-++-distribute f xs ys) ⟩
    f x ∷ map f xs ++ map f ys
  ≡⟨⟩
    map f (x ∷ xs) ++ map f ys
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Floats
------------------------------------------------------------------------

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

module Data.Float where

open import Data.String.Base using (String)

------------------------------------------------------------------------
-- Re-export built-ins publically

open import Agda.Builtin.Float public
  using
  ( Float
  ; primFloatEquality
  ; primShowFloat
  )

------------------------------------------------------------------------
-- Operations

show : Float → String
show = primShowFloat


text:
{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.HITs.SetTruncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec ; elim to pElim) hiding (elim2 ; elim3 ; rec2 ; map)

private
  variable
    ℓ ℓ' ℓ'' : Level
    A B C D : Type ℓ

rec : isSet B → (A → B) → ∥ A ∥₂ → B
rec Bset f ∣ x ∣₂ = f x
rec Bset f (squash₂ x y p q i j) =
  Bset _ _ (cong (rec Bset f) p) (cong (rec Bset f) q) i j

rec2 : isSet C → (A → B → C) → ∥ A ∥₂ → ∥ B ∥₂ → C
rec2 Cset f ∣ x ∣₂ ∣ y ∣₂ = f x y
rec2 Cset f ∣ x ∣₂ (squash₂ y z p q i j) =
  Cset _ _ (cong (rec2 Cset f ∣ x ∣₂) p) (cong (rec2 Cset f ∣ x ∣₂) q) i j
rec2 Cset f (squash₂ x y p q i j) z =
  Cset _ _ (cong (λ a → rec2 Cset f a z) p) (cong (λ a → rec2 Cset f a z) q) i j

-- Old version:
-- rec2 Cset f = rec (isSetΠ λ _ → Cset) λ x → rec Cset (f x)

-- lemma 6.9.1 in HoTT book
elim : {B : ∥ A ∥₂ → Type ℓ}
       (Bset : (x : ∥ A ∥₂) → isSet (B x))
       (f : (a : A) → B (∣ a ∣₂))
       (x : ∥ A ∥₂) → B x
elim Bset f ∣ a ∣₂ = f a
elim Bset f (squash₂ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset _ _
    (cong (elim Bset f) p) (cong (elim Bset f) q) (squash₂ x y p q) i j

elim2 : {C : ∥ A ∥₂ → ∥ B ∥₂ → Type ℓ}
        (Cset : ((x : ∥ A ∥₂) (y : ∥ B ∥₂) → isSet (C x y)))
        (f : (a : A) (b : B) → C ∣ a ∣₂ ∣ b ∣₂)
        (x : ∥ A ∥₂) (y : ∥ B ∥₂) → C x y
elim2 Cset f ∣ x ∣₂ ∣ y ∣₂ = f x y
elim2 Cset f ∣ x ∣₂ (squash₂ y z p q i j) =
  isOfHLevel→isOfHLevelDep 2 (λ a → Cset ∣ x ∣₂ a) _ _
     (cong (elim2 Cset f ∣ x ∣₂) p) (cong (elim2 Cset f ∣ x ∣₂) q) (squash₂ y z p q) i j
elim2 Cset f (squash₂ x y p q i j) z =
  isOfHLevel→isOfHLevelDep 2 (λ a → Cset a z) _ _
    (cong (λ a → elim2 Cset f a z) p) (cong (λ a → elim2 Cset f a z) q) (squash₂ x y p q) i j

-- Old version:
-- elim2 Cset f = elim (λ _ → isSetΠ (λ _ → Cset _ _))
--                     (λ a → elim (λ _ → Cset _ _) (f a))

-- TODO: generalize
elim3 : {B : (x y z : ∥ A ∥₂) → Type ℓ}
        (Bset : ((x y z : ∥ A ∥₂) → isSet (B x y z)))
        (g : (a b c : A) → B ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂)
        (x y z : ∥ A ∥₂) → B x y z
elim3 Bset g = elim2 (λ _ _ → isSetΠ (λ _ → Bset _ _ _))
                     (λ a b → elim (λ _ → Bset _ _ _) (g a b))

-- the recursor for maps into groupoids following the "HIT proof" in:
-- https://arxiv.org/abs/1507.01150
-- i.e. for any type A and groupoid B we can construct a map ∥ A ∥₂ → B
-- from a map A → B satisfying the condition
--    ∀ (a b : A) (p q : a ≡ b) → cong f p ≡ cong f q
-- TODO: prove that this is an equivalence
module rec→Gpd {A : Type ℓ} {B : Type ℓ'} (Bgpd : isGroupoid B) (f : A → B)
               (congFConst : ∀ (a b : A) (p q : a ≡ b) → cong f p ≡ cong f q) where

 data H : Type ℓ where
  η : A → H
  ε : ∀ (a b : A) → ∥ a ≡ b ∥ → η a ≡ η b -- prop. trunc. of a≡b
  δ : ∀ (a b : A) (p : a ≡ b) → ε a b ∣ p ∣ ≡ cong η p
  gtrunc : isGroupoid H

 -- write elimination principle for H
 module Helim {P : H → Type ℓ''} (Pgpd : ∀ h → isGroupoid (P h))
              (η* : (a : A) → P (η a))
              (ε* : ∀ (a b : A) (∣p∣ : ∥ a ≡ b ∥)
                  → PathP (λ i → P (ε a b ∣p∣ i)) (η* a) (η* b))
              (δ* : ∀ (a b : A) (p : a ≡ b)
                  → PathP (λ i → PathP (λ j → P (δ a b p i j)) (η* a) (η* b))
                          (ε* a b ∣ p ∣) (cong η* p)) where

  fun : (h : H) → P h
  fun (η a) = η* a
  fun (ε a b ∣p∣ i) = ε* a b ∣p∣ i
  fun (δ a b p i j) = δ* a b p i j
  fun (gtrunc x y p q α β i j k) = isOfHLevel→isOfHLevelDep 3 Pgpd
                                   (fun x) (fun y)
                                   (cong fun p) (cong fun q)
                                   (cong (cong fun) α) (cong (cong fun) β)
                                   (gtrunc x y p q α β) i j k

 module Hrec {C : Type ℓ''} (Cgpd : isGroupoid C)
             (η* : A → C)
             (ε* : ∀ (a b : A) → ∥ a ≡ b ∥ → η* a ≡ η* b)
             (δ* : ∀ (a b : A) (p : a ≡ b) → ε* a b ∣ p ∣ ≡ cong η* p) where

  fun : H → C
  fun (η a) = η* a
  fun (ε a b ∣p∣ i) = ε* a b ∣p∣ i
  fun (δ a b p i j) = δ* a b p i j
  fun (gtrunc x y p q α β i j k) = Cgpd (fun x) (fun y) (cong fun p) (cong fun q)
                                   (cong (cong fun) α) (cong (cong fun) β) i j k

 module HelimProp {P : H → Type ℓ''} (Pprop : ∀ h → isProp (P h))
                  (η* : (a : A) → P (η a)) where

  fun : ∀ h → P h
  fun = Helim.fun (λ _ → isSet→isGroupoid (isProp→isSet (Pprop _))) η*
                  (λ a b ∣p∣ → isOfHLevel→isOfHLevelDep 1 Pprop _ _ (ε a b ∣p∣))
                   λ a b p → isOfHLevel→isOfHLevelDep 1
                              {B = λ p → PathP (λ i → P (p i)) (η* a) (η* b)}
                              (λ _ → isOfHLevelPathP 1 (Pprop _) _ _) _ _ (δ a b p)

 -- The main trick: eliminating into hsets is easy
 -- i.e. H has the universal property of set truncation...
 module HelimSet {P : H → Type ℓ''} (Pset : ∀ h → isSet (P h))
                 (η* : ∀ a → P (η a)) where

  fun : (h : H) → P h
  fun = Helim.fun (λ _ → isSet→isGroupoid (Pset _)) η* ε*
                   λ a b p → isOfHLevel→isOfHLevelDep 1
                             {B = λ p → PathP (λ i → P (p i)) (η* a) (η* b)}
                             (λ _ → isOfHLevelPathP' 1 (Pset _) _ _) _ _ (δ a b p)
   where
   ε* : (a b : A) (∣p∣ : ∥ a ≡ b ∥) → PathP (λ i → P (ε a b ∣p∣ i)) (η* a) (η* b)
   ε* a b = pElim (λ _ → isOfHLevelPathP' 1 (Pset _) (η* a) (η* b))
                   λ p → subst (λ x → PathP (λ i → P (x i)) (η* a) (η* b))
                               (sym (δ a b p)) (cong η* p)

 -- Now we need to prove that H is a set.
 -- We start with a  little lemma:
 localHedbergLemma : {X : Type ℓ''} (P : X → Type ℓ'')
                   → (∀ x → isProp (P x))
                   → ((x : X) → P x → (y : X) → P y → x ≡ y)
                  --------------------------------------------------
                   → (x : X) → P x → (y : X) → isProp (x ≡ y)
 localHedbergLemma {X = X} P Pprop P→≡ x px y = isPropRetract
                   (λ p → subst P p px) (λ py → sym (P→≡ x px x px) ∙ P→≡ x px y py)
                   isRetract (Pprop y)
  where
  isRetract : (p : x ≡ y) → (sym (P→≡ x px x px)) ∙ P→≡ x px y (subst P p px) ≡ p
  isRetract = J (λ y' p' → (sym (P→≡ x px x px)) ∙ P→≡ x px y' (subst P p' px) ≡ p')
                (subst (λ px' → sym (P→≡ x px x px) ∙ P→≡ x px x px' ≡ refl)
                (sym (substRefl {B = P} px)) (lCancel (P→≡ x px x px)))

 Hset : isSet H
 Hset = HelimProp.fun (λ _ → isPropΠ λ _ → isPropIsProp) baseCaseLeft
  where
  baseCaseLeft : (a₀ : A) (y : H) → isProp (η a₀ ≡ y)
  baseCaseLeft a₀ = localHedbergLemma (λ x → Q x .fst) (λ x → Q x .snd) Q→≡ _ ∣ refl ∣
   where
   Q : H → hProp ℓ
   Q = HelimSet.fun (λ _ → isSetHProp) λ b → ∥ a₀ ≡ b ∥ , propTruncIsProp
   -- Q (η b) = ∥ a ≡ b ∥

   Q→≡ : (x : H) → Q x .fst → (y : H) → Q y .fst → x ≡ y
   Q→≡ = HelimSet.fun (λ _ → isSetΠ3 λ _ _ _ → gtrunc _ _)
       λ a p → HelimSet.fun (λ _ → isSetΠ λ _ → gtrunc _ _)
       λ b q → sym (ε a₀ a p) ∙ ε a₀ b q

 -- our desired function will split through H,
 -- i.e. we get a function ∥ A ∥₂ → H → B
 fun : ∥ A ∥₂ → B
 fun = f₁ ∘ f₂
  where
  f₁ : H → B
  f₁ = Hrec.fun Bgpd f εᶠ λ _ _ _ → refl
   where
   εᶠ : (a b : A) → ∥ a ≡ b ∥ → f a ≡ f b
   εᶠ a b = rec→Set (Bgpd _ _) (cong f) λ p q → congFConst a b p q
   -- this is the inductive step,
   -- we use that maps ∥ A ∥ → B for an hset B
   -- correspond to 2-Constant maps A → B (which cong f is by assumption)
  f₂ : ∥ A ∥₂ → H
  f₂ = rec Hset η

map : (A → B) → ∥ A ∥₂ → ∥ B ∥₂
map f = rec squash₂ λ x → ∣ f x ∣₂

setTruncUniversal : isSet B → (∥ A ∥₂ → B) ≃ (A → B)
setTruncUniversal {B = B} Bset =
  isoToEquiv (iso (λ h x → h ∣ x ∣₂) (rec Bset) (λ _ → refl) rinv)
  where
  rinv : (f : ∥ A ∥₂ → B) → rec Bset (λ x → f ∣ x ∣₂) ≡ f
  rinv f i x =
    elim (λ x → isProp→isSet (Bset (rec Bset (λ x → f ∣ x ∣₂) x) (f x)))
         (λ _ → refl) x i

setTruncIsSet : isSet ∥ A ∥₂
setTruncIsSet a b p q = squash₂ a b p q

setTruncIdempotentIso : isSet A → Iso ∥ A ∥₂ A
Iso.fun (setTruncIdempotentIso hA) = rec hA (idfun _)
Iso.inv (setTruncIdempotentIso hA) x = ∣ x ∣₂
Iso.rightInv (setTruncIdempotentIso hA) _ = refl
Iso.leftInv (setTruncIdempotentIso hA) = elim (λ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ → refl)

setTruncIdempotent≃ : isSet A → ∥ A ∥₂ ≃ A
setTruncIdempotent≃ {A = A} hA = isoToEquiv (setTruncIdempotentIso hA)

setTruncIdempotent : isSet A → ∥ A ∥₂ ≡ A
setTruncIdempotent hA = ua (setTruncIdempotent≃ hA)

isContr→isContrSetTrunc : isContr A → isContr (∥ A ∥₂)
isContr→isContrSetTrunc contr = ∣ fst contr ∣₂
                                , elim (λ _ → isOfHLevelPath 2 (setTruncIsSet) _ _)
                                       λ a → cong ∣_∣₂ (snd contr a)

setTruncIso : Iso A B → Iso ∥ A ∥₂ ∥ B ∥₂
Iso.fun (setTruncIso is) = rec setTruncIsSet (λ x → ∣ Iso.fun is x ∣₂)
Iso.inv (setTruncIso is) = rec setTruncIsSet (λ x → ∣ Iso.inv is x ∣₂)
Iso.rightInv (setTruncIso is) =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ a → cong ∣_∣₂ (Iso.rightInv is a)
Iso.leftInv (setTruncIso is) =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ a → cong ∣_∣₂ (Iso.leftInv is a)

setSigmaIso : {B : A → Type ℓ} → Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
setSigmaIso {A = A} {B = B} = iso fun funinv sect retr
  where
  {- writing it out explicitly to avoid yellow highlighting -}
  fun : ∥ Σ A B ∥₂ → ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
  fun = rec setTruncIsSet λ {(a , p) → ∣ a , ∣ p ∣₂ ∣₂}
  funinv : ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂ → ∥ Σ A B ∥₂
  funinv = rec setTruncIsSet (λ {(a , p) → rec setTruncIsSet (λ p → ∣ a , p ∣₂) p})
  sect : section fun funinv
  sect = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { (a , p) → elim {B = λ p → fun (funinv ∣ a , p ∣₂) ≡ ∣ a , p ∣₂}
              (λ p → isOfHLevelPath 2 setTruncIsSet _ _) (λ _ → refl) p }
  retr : retract fun funinv
  retr = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { _ → refl }

sigmaElim : {B : ∥ A ∥₂ → Type ℓ} {C : Σ ∥ A ∥₂ B  → Type ℓ'}
            (Bset : (x : Σ ∥ A ∥₂ B) → isSet (C x))
            (g : (a : A) (b : B ∣ a ∣₂) → C (∣ a ∣₂ , b))
            (x : Σ ∥ A ∥₂ B) → C x
sigmaElim {B = B} {C = C} set g (x , y) =
  elim {B = λ x → (y : B x) → C (x , y)} (λ _ → isSetΠ λ _ → set _) g x y

sigmaProdElim : {C : ∥ A ∥₂ × ∥ B ∥₂ → Type ℓ} {D : Σ (∥ A ∥₂ × ∥ B ∥₂) C  → Type ℓ'}
                (Bset : (x : Σ (∥ A ∥₂ × ∥ B ∥₂) C) → isSet (D x))
                (g : (a : A) (b : B) (c : C (∣ a ∣₂ , ∣ b ∣₂)) → D ((∣ a ∣₂ , ∣ b ∣₂) , c))
                (x : Σ (∥ A ∥₂ × ∥ B ∥₂) C) → D x
sigmaProdElim {B = B} {C = C} {D = D} set g ((x , y) , c) =
  elim {B = λ x → (y : ∥ B ∥₂) (c : C (x , y)) → D ((x , y) , c)}
       (λ _ → isSetΠ λ _ → isSetΠ λ _ → set _)
       (λ x → elim (λ _ → isSetΠ λ _ → set _) (g x))
       x y c

prodElim : {C : ∥ A ∥₂ × ∥ B ∥₂ → Type ℓ}
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) → isSet (C x))
         → ((a : A) (b : B) → C (∣ a ∣₂ , ∣ b ∣₂))
         → (x : ∥ A ∥₂ × ∥ B ∥₂) → C x
prodElim setC f (a , b) = elim2 (λ x y → setC (x , y)) f a b

prodRec : {C : Type ℓ} → isSet C → (A → B → C) → ∥ A ∥₂ × ∥ B ∥₂ → C
prodRec setC f (a , b) = rec2 setC f a b

prodElim2 : {E : (∥ A ∥₂ × ∥ B ∥₂) → (∥ C ∥₂ × ∥ D ∥₂) → Type ℓ}
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) (y : ∥ C ∥₂ × ∥ D ∥₂) → isSet (E x y))
         → ((a : A) (b : B) (c : C) (d : D) → E (∣ a ∣₂ , ∣ b ∣₂) (∣ c ∣₂ , ∣ d ∣₂))
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) (y : ∥ C ∥₂ × ∥ D ∥₂) → (E x y))
prodElim2 isset f = prodElim (λ _ → isSetΠ λ _ → isset _ _)
                             λ a b → prodElim (λ _ → isset _ _)
                                     λ c d → f a b c d

setTruncOfProdIso :  Iso ∥ A × B ∥₂ (∥ A ∥₂ × ∥ B ∥₂)
Iso.fun setTruncOfProdIso = rec (isSet× setTruncIsSet setTruncIsSet) λ { (a , b) → ∣ a ∣₂ , ∣ b ∣₂ }
Iso.inv setTruncOfProdIso = prodRec setTruncIsSet λ a b → ∣ a , b ∣₂
Iso.rightInv setTruncOfProdIso =
  prodElim (λ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _) λ _ _ → refl
Iso.leftInv setTruncOfProdIso =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _) λ {(a , b) → refl}

IsoSetTruncateSndΣ : {A : Type ℓ} {B : A → Type ℓ'} → Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
Iso.fun IsoSetTruncateSndΣ = map λ a → (fst a) , ∣ snd a ∣₂
Iso.inv IsoSetTruncateSndΣ = rec setTruncIsSet (uncurry λ x → map λ b → x , b)
Iso.rightInv IsoSetTruncateSndΣ =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        (uncurry λ a → elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ _ → refl)
Iso.leftInv IsoSetTruncateSndΣ =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
         λ _ → refl

PathIdTrunc₀Iso : {a b : A} → Iso (∣ a ∣₂ ≡ ∣ b ∣₂) ∥ a ≡ b ∥
Iso.fun (PathIdTrunc₀Iso {b = b}) p =
  transport (λ i → rec {B = TypeOfHLevel _ 1} (isOfHLevelTypeOfHLevel 1)
                        (λ a → ∥ a ≡ b ∥ , squash) (p (~ i)) .fst)
            ∣ refl ∣
Iso.inv PathIdTrunc₀Iso = pRec (squash₂ _ _) (cong ∣_∣₂)
Iso.rightInv PathIdTrunc₀Iso _ = squash _ _
Iso.leftInv PathIdTrunc₀Iso _ = squash₂ _ _ _ _

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-

Finite Structures over Finite Set
  In short, the type of structures should be finite set itself.

This file contains:
- Definition and properties of finite sets equipped with finite structures;
- The type of finitely-structured finite sets is Rijke finite,
  so that we can count their number up to equivalence/isomorphism.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinType.FiniteStructure where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.HITs.SetTruncation as Set

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Data.FinSet
open import Cubical.Data.FinSet.Induction
open import Cubical.Data.FinSet.Cardinality
open import Cubical.Data.FinType
open import Cubical.Data.FinType.Sigma

private
  variable
    ℓ ℓ' : Level
    n : ℕ
    S : FinSet ℓ → FinSet ℓ'

-- type of finite sets with finite structure

FinSetWithStr : (S : FinSet ℓ → FinSet ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
FinSetWithStr {ℓ = ℓ} S = Σ[ X ∈ FinSet ℓ ] S X .fst

-- type of finite sets with a fixed cardinal

FinSetOfCard : (ℓ : Level) (n : ℕ) → Type (ℓ-suc ℓ)
FinSetOfCard ℓ n = Σ[ X ∈ FinSet ℓ ] (card X ≡ n)

FinSetWithStrOfCard : (S : FinSet ℓ → FinSet ℓ') (n : ℕ) → Type (ℓ-max (ℓ-suc ℓ) ℓ')
FinSetWithStrOfCard {ℓ = ℓ} S n = Σ[ X ∈ FinSetOfCard ℓ n ] S (X .fst) .fst

FinSetOfCard≡ : (X Y : FinSetOfCard ℓ n) → (X .fst ≡ Y .fst) ≃ (X ≡ Y)
FinSetOfCard≡ _ _ = Σ≡PropEquiv (λ _ → isSetℕ _ _)

open Iso

∥FinSetOfCard∥₂≡ : (X Y : FinSetOfCard ℓ n) → ∥ X .fst ≡ Y .fst ∥ → ∣ X ∣₂ ≡ ∣ Y ∣₂
∥FinSetOfCard∥₂≡ _ _ =
  Prop.rec (squash₂ _ _) (λ p → PathIdTrunc₀Iso .inv ∣ FinSetOfCard≡ _ _ .fst p ∣)

isPathConnectedFinSetOfCard : isContr ∥ FinSetOfCard ℓ n ∥₂
isPathConnectedFinSetOfCard {n = n} .fst = ∣ 𝔽in n , card𝔽in n ∣₂
isPathConnectedFinSetOfCard {n = n} .snd =
  Set.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ (X , p) → sym (∥FinSetOfCard∥₂≡ _ _ (card≡n p)))

isFinTypeFinSetOfCard : isFinType 1 (FinSetOfCard ℓ n)
isFinTypeFinSetOfCard .fst = isPathConnected→isFinType0 isPathConnectedFinSetOfCard
isFinTypeFinSetOfCard .snd X Y =
  isFinSet→isFinType 0 (EquivPresIsFinSet (FinSet≡ _ _ ⋆ FinSetOfCard≡ _ _) (isFinSetType≡Eff (X .fst) (Y .fst)))

-- the type of finitely-structured finite sets is Rijke finite
-- in particular, we can count their number up to equivalence

isFinTypeFinSetWithStrOfCard :
  (S : FinSet ℓ → FinSet ℓ') (n : ℕ)
  → isFinType 0 (FinSetWithStrOfCard S n)
isFinTypeFinSetWithStrOfCard S n =
  isFinTypeΣ {n = 0} (_ , isFinTypeFinSetOfCard) (λ X → _ , isFinSet→isFinType 0 (S (X .fst) .snd))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
open import List
open import Nat
open import Prelude
open import contexts
open import core

module statics-core where
  open core public

   -- zippered form of types
  data ztyp : Set where
    ▹_◃    : htyp → ztyp
    _==>₁_ : ztyp → htyp → ztyp
    _==>₂_ : htyp → ztyp → ztyp
    _⊕₁_   : ztyp → htyp → ztyp
    _⊕₂_   : htyp → ztyp → ztyp
    _⊠₁_   : ztyp → htyp → ztyp
    _⊠₂_   : htyp → ztyp → ztyp

  -- zippered form of expressions
  data zexp : Set where
    ▹_◃        : hexp → zexp
    _·:₁_      : zexp → htyp → zexp
    _·:₂_      : hexp → ztyp → zexp
    ·λ         : Nat → zexp → zexp
    ·λ_·[_]₁_  : Nat → ztyp → hexp → zexp
    ·λ_·[_]₂_  : Nat → htyp → zexp → zexp
    _∘₁_       : zexp → hexp → zexp
    _∘₂_       : hexp → zexp → zexp
    _·+₁_      : zexp → hexp → zexp
    _·+₂_      : hexp → zexp → zexp
    ⦇⌜_⌟⦈[_]   : zexp → Nat → zexp
    inl        : zexp → zexp
    inr        : zexp → zexp
    case₁      : zexp → Nat → hexp → Nat → hexp → zexp
    case₂      : hexp → Nat → zexp → Nat → hexp → zexp
    case₃      : hexp → Nat → hexp → Nat → zexp → zexp
    ⟨_,_⟩₁     : zexp → hexp → zexp
    ⟨_,_⟩₂     : hexp → zexp → zexp
    fst        : zexp → zexp
    snd        : zexp → zexp

  -- erasure of cursor for types and expressions, judgementally. see
  -- jugemental-erase.agda for an argument that this defines an isomorphic
  -- object to the direct metafunction provided in the text of the paper
  data erase-t : ztyp → htyp → Set where
    ETTop   : ∀{t} →
              erase-t (▹ t ◃) t
    ETArrL  : ∀{t1 t1' t2} →
              erase-t t1 t1' →
              erase-t (t1 ==>₁ t2) (t1' ==> t2)
    ETArrR  : ∀{t1 t2 t2'} →
              erase-t t2 t2' →
              erase-t (t1 ==>₂ t2) (t1 ==> t2')
    ETPlusL : ∀{t1 t1' t2} →
              erase-t t1 t1' →
              erase-t (t1 ⊕₁ t2) (t1' ⊕ t2)
    ETPlusR : ∀{t1 t2 t2'} →
              erase-t t2 t2' →
              erase-t (t1 ⊕₂ t2) (t1 ⊕ t2')
    ETProdL : ∀{t1 t1' t2} →
              erase-t t1 t1' →
              erase-t (t1 ⊠₁ t2) (t1' ⊠ t2)
    ETProdR : ∀{t1 t2 t2'} →
              erase-t t2 t2' →
              erase-t (t1 ⊠₂ t2) (t1 ⊠ t2')

  data erase-e : zexp → hexp → Set where
    EETop      : ∀{x} →
                 erase-e (▹ x ◃) x
    EEPlusL    : ∀{e1 e1' e2} →
                 erase-e e1 e1' →
                 erase-e (e1 ·+₁ e2) (e1' ·+ e2)
    EEPlusR    : ∀{e1 e2 e2'} →
                 erase-e e2 e2' →
                 erase-e (e1 ·+₂ e2) (e1 ·+ e2')
    EEAscL     : ∀{e e' t} →
                 erase-e e e' →
                 erase-e (e ·:₁ t) (e' ·: t)
    EEAscR     : ∀{e t t'} →
                 erase-t t t' →
                 erase-e (e ·:₂ t) (e ·: t')
    EELam      : ∀{x e e'} →
                 erase-e e e' →
                 erase-e (·λ x e) (·λ x e')
    EEHalfLamL : ∀{x e t t'} →
                 erase-t t t' →
                 erase-e (·λ x ·[ t ]₁ e) (·λ x ·[ t' ] e)
    EEHalfLamR : ∀{x e e' t} →
                 erase-e e e' →
                 erase-e (·λ x ·[ t ]₂ e) (·λ x ·[ t ] e')
    EEApL      : ∀{e1 e1' e2} →
                 erase-e e1 e1' →
                 erase-e (e1 ∘₁ e2) (e1' ∘ e2)
    EEApR      : ∀{e1 e2 e2'} →
                 erase-e e2 e2' →
                 erase-e (e1 ∘₂ e2) (e1 ∘ e2')
    EEInl      : ∀{e e'} →
                 erase-e e e' →
                 erase-e (inl e) (inl e')
    EEInr      : ∀{e e'} →
                 erase-e e e' →
                 erase-e (inr e) (inr e')
    EECase1    : ∀{e e' x e1 y e2} →
                 erase-e e e' →
                 erase-e (case₁ e x e1 y e2) (case e' x e1 y e2)
    EECase2    : ∀{e x e1 e1' y e2} →
                 erase-e e1 e1' →
                 erase-e (case₂ e x e1 y e2) (case e x e1' y e2)
    EECase3    : ∀{e x e1 y e2 e2'} →
                 erase-e e2 e2' →
                 erase-e (case₃ e x e1 y e2) (case e x e1 y e2')
    EEPairL    : ∀{e1 e1' e2} →
                 erase-e e1 e1' →
                 erase-e ⟨ e1 , e2 ⟩₁ ⟨ e1' , e2 ⟩
    EEPairR    : ∀{e1 e2 e2'} →
                 erase-e e2 e2' →
                 erase-e ⟨ e1 , e2 ⟩₂ ⟨ e1 , e2' ⟩
    EEFst      : ∀{e e'} →
                 erase-e e e' →
                 erase-e (fst e) (fst e')
    EESnd      : ∀{e e'} →
                 erase-e e e' →
                 erase-e (snd e) (snd e')
    EENEHole   : ∀{e e' u} →
                 erase-e e e' →
                 erase-e ⦇⌜ e ⌟⦈[ u ] ⦇⌜ e' ⌟⦈[ u ]

  -- the three grammars that define actions
  data direction : Set where
    child  : Nat → direction
    parent : direction

  -- in contrast to the POPL 2017 hazelnut paper, we include named holes in static
  -- semantics since they are required by the dynamic semantics. a given action
  -- may introduce a different number of holes depending on the context it is
  -- applied in, so the action must always supply enough names for every location
  -- in the term where a hole could occur. moreover, care must be taken to have
  -- the same hole names always correspond to the same hole locations. for example,
  -- when we show that each derivation has an equivalently subsumption-minimal
  -- derivation, this is needed to guarentee the same action (which includes hole names)
  -- can be used in the minimal derivation.
  data shape : Set where
    arrow  : shape
    num    : shape
    asc    : shape
    var    : Nat → Nat → shape
    lam    : Nat → Nat → Nat → shape
    ap     : Nat → Nat → shape
    numlit : Nat → Nat → shape
    plus   : Nat → Nat → shape
    nehole : Nat → shape
    sum    : shape
    inl    : Nat → Nat → shape
    inr    : Nat → Nat → shape
    case   : Nat → Nat → Nat → Nat → Nat → shape
    prod   : shape
    pair   : Nat → Nat → shape
    fst    : Nat → shape
    snd    : Nat → shape

  data action : Set where
    move      : direction → action
    construct : shape → action
    del       : Nat → action
    finish    : action

  -- type actions
  data _+_+>_ : (t : ztyp) → (α : action) → (t' : ztyp) → Set where
    TMArrChild1   : {t1 t2 : htyp} →
                    ▹ t1 ==> t2 ◃ + move (child 1) +> (▹ t1 ◃ ==>₁ t2)
    TMArrChild2   : {t1 t2 : htyp} →
                    ▹ t1 ==> t2 ◃ + move (child 2) +> (t1 ==>₂ ▹ t2 ◃)
    TMArrParent1  : {t1 t2 : htyp} →
                    (▹ t1 ◃ ==>₁ t2) + move parent +> ▹ t1 ==> t2 ◃
    TMArrParent2  : {t1 t2 : htyp} →
                    (t1 ==>₂ ▹ t2 ◃) + move parent +> ▹ t1 ==> t2 ◃
    TMPlusChild1  : {t1 t2 : htyp} →
                    ▹ t1 ⊕ t2 ◃ + move (child 1) +> (▹ t1 ◃ ⊕₁ t2)
    TMPlusChild2  : {t1 t2 : htyp} →
                    ▹ t1 ⊕ t2 ◃ + move (child 2) +> (t1 ⊕₂ ▹ t2 ◃)
    TMPlusParent1 : {t1 t2 : htyp} →
                    (▹ t1 ◃ ⊕₁ t2) + move parent +> ▹ t1 ⊕ t2 ◃
    TMPlusParent2 : {t1 t2 : htyp} →
                    (t1 ⊕₂ ▹ t2 ◃) + move parent +> ▹ t1 ⊕ t2 ◃
    TMProdChild1  : {t1 t2 : htyp} →
                    ▹ t1 ⊠ t2 ◃ + move (child 1) +> (▹ t1 ◃ ⊠₁ t2)
    TMProdChild2  : {t1 t2 : htyp} →
                    ▹ t1 ⊠ t2 ◃ + move (child 2) +> (t1 ⊠₂ ▹ t2 ◃)
    TMProdParent1 : {t1 t2 : htyp} →
                    (▹ t1 ◃ ⊠₁ t2) + move parent +> ▹ t1 ⊠ t2 ◃
    TMProdParent2 : {t1 t2 : htyp} →
                    (t1 ⊠₂ ▹ t2 ◃) + move parent +> ▹ t1 ⊠ t2 ◃
    TMDel         : {t : htyp} {u : Nat} →
                    (▹ t ◃) + del u +> (▹ ⦇-⦈ ◃)
    TMConArrow    : {t : htyp} →
                    (▹ t ◃) + construct arrow +> (t ==>₂ ▹ ⦇-⦈ ◃)
    TMConPlus     : {t : htyp} →
                    (▹ t ◃) + construct sum +> (t ⊕₂ ▹ ⦇-⦈ ◃)
    TMConProd     : {t : htyp} →
                    (▹ t ◃) + construct prod +> (t ⊠₂ ▹ ⦇-⦈ ◃)
    TMConNum      : (▹ ⦇-⦈ ◃) + construct num +> (▹ num ◃)
    TMArrZip1     : {t1 t1' : ztyp} {t2 : htyp} {α : action} →
                    (t1 + α +> t1') →
                    ((t1 ==>₁ t2) + α +> (t1' ==>₁ t2))
    TMArrZip2     : {t2 t2' : ztyp} {t1 : htyp} {α : action} →
                    (t2 + α +> t2') →
                    ((t1 ==>₂ t2) + α +> (t1 ==>₂ t2'))
    TMPlusZip1    : {t1 t1' : ztyp} {t2 : htyp} {α : action} →
                    (t1 + α +> t1') →
                    ((t1 ⊕₁ t2) + α +> (t1' ⊕₁ t2))
    TMPlusZip2    : {t2 t2' : ztyp} {t1 : htyp} {α : action} →
                    (t2 + α +> t2') →
                    ((t1 ⊕₂ t2) + α +> (t1 ⊕₂ t2'))
    TMProdZip1    : {t1 t1' : ztyp} {t2 : htyp} {α : action} →
                    (t1 + α +> t1') →
                    ((t1 ⊠₁ t2) + α +> (t1' ⊠₁ t2))
    TMProdZip2    : {t2 t2' : ztyp} {t1 : htyp} {α : action} →
                    (t2 + α +> t2') →
                    ((t1 ⊠₂ t2) + α +> (t1 ⊠₂ t2'))

  -- expression movement
  data _+_+>e_ : (e : zexp) → (α : action) → (e' : zexp) → Set where
    EMPlusChild1     : {e1 e2 : hexp} →
                       (▹ e1 ·+ e2 ◃) + move (child 1) +>e (▹ e1 ◃ ·+₁ e2)
    EMPlusChild2     : {e1 e2 : hexp} →
                       (▹ e1 ·+ e2 ◃) + move (child 2) +>e (e1 ·+₂ ▹ e2 ◃)
    EMPlusParent1    : {e1 e2 : hexp} →
                       (▹ e1 ◃ ·+₁ e2) + move parent +>e (▹ e1 ·+ e2 ◃)
    EMPlusParent2    : {e1 e2 : hexp} →
                       (e1 ·+₂ ▹ e2 ◃) + move parent +>e (▹ e1 ·+ e2 ◃)
    EMAscChild1      : {e : hexp} {t : htyp} →
                       (▹ e ·: t ◃) + move (child 1) +>e (▹ e ◃ ·:₁ t)
    EMAscChild2      : {e : hexp} {t : htyp} →
                       (▹ e ·: t ◃) + move (child 2) +>e (e  ·:₂ ▹ t ◃)
    EMAscParent1     : {e : hexp} {t : htyp} →
                       (▹ e ◃ ·:₁ t) + move parent +>e (▹ e ·: t ◃)
    EMAscParent2     : {e : hexp} {t : htyp} →
                       (e ·:₂ ▹ t ◃) + move parent +>e (▹ e ·: t ◃)
    EMLamChild1      : {e : hexp} {x : Nat} →
                       ▹ (·λ x e) ◃ + move (child 1) +>e ·λ x (▹ e ◃)
    EMLamParent      : {e : hexp} {x : Nat} →
                       ·λ x (▹ e ◃) + move parent +>e ▹ (·λ x e) ◃
    EMHalfLamChild1  : {e : hexp} {t : htyp} {x : Nat} →
                       ▹ (·λ x ·[ t ] e) ◃ + move (child 1) +>e (·λ x ·[ ▹ t ◃ ]₁ e)
    EMHalfLamChild2  : {e : hexp} {t : htyp} {x : Nat} →
                       ▹ (·λ x ·[ t ] e) ◃ + move (child 2) +>e (·λ x ·[ t ]₂ ▹ e ◃)
    EMHalfLamParent1 : {e : hexp} {t : htyp} {x : Nat} →
                       (·λ x ·[ ▹ t ◃ ]₁ e)  + move parent +>e ▹ (·λ x ·[ t ] e) ◃
    EMHalfLamParent2 : {e : hexp} {t : htyp} {x : Nat} →
                       (·λ x ·[ t ]₂ ▹ e ◃) + move parent +>e ▹ (·λ x ·[ t ] e) ◃
    EMApChild1       : {e1 e2 : hexp} →
                       (▹ e1 ∘ e2 ◃) + move (child 1)+>e (▹ e1 ◃ ∘₁ e2)
    EMApChild2       : {e1 e2 : hexp} →
                       (▹ e1 ∘ e2 ◃) + move (child 2) +>e (e1 ∘₂ ▹ e2 ◃)
    EMApParent1      : {e1 e2 : hexp} →
                       (▹ e1 ◃ ∘₁ e2) + move parent +>e (▹ e1 ∘ e2 ◃)
    EMApParent2      : {e1 e2 : hexp} →
                       (e1 ∘₂ ▹ e2 ◃) + move parent +>e (▹ e1 ∘ e2 ◃)
    EMInlChild1      : {e : hexp} →
                       ▹ inl e ◃ + move (child 1) +>e inl ▹ e ◃
    EMInlParent      : {e : hexp} →
                       inl ▹ e ◃ + move parent +>e ▹ inl e  ◃
    EMInrChild1      : {e : hexp} →
                       ▹ inr e ◃ + move (child 1) +>e inr ▹ e ◃
    EMInrParent      : {e : hexp} →
                       inr ▹ e ◃ + move parent +>e ▹ inr e  ◃
    EMCaseParent1    : {e e1 e2 : hexp} {x y : Nat} →
                       case₁ ▹ e ◃ x e1 y e2 + move parent +>e ▹ case e x e1 y e2 ◃
    EMCaseParent2    : {e e1 e2 : hexp} {x y : Nat} →
                       case₂ e x ▹ e1 ◃ y e2 + move parent +>e ▹ case e x e1 y e2 ◃
    EMCaseParent3    : {e e1 e2 : hexp} {x y : Nat} →
                       case₃ e x e1 y ▹ e2 ◃ + move parent +>e ▹ case e x e1 y e2 ◃
    EMCaseChild1     : {e e1 e2 : hexp} {x y : Nat} →
                       ▹ case e x e1 y e2 ◃ + move (child 1) +>e case₁ ▹ e ◃ x e1 y e2
    EMCaseChild2     : {e e1 e2 : hexp} {x y : Nat} →
                       ▹ case e x e1 y e2 ◃ + move (child 2) +>e case₂ e x ▹ e1 ◃ y e2
    EMCaseChild3     : {e e1 e2 : hexp} {x y : Nat} →
                       ▹ case e x e1 y e2 ◃ + move (child 3) +>e case₃ e x e1 y ▹ e2 ◃
    EMPairChild1     : {e1 e2 : hexp} →
                       (▹ ⟨ e1 , e2 ⟩ ◃) + move (child 1)+>e ⟨ ▹ e1 ◃ , e2 ⟩₁
    EMPairChild2     : {e1 e2 : hexp} →
                       (▹ ⟨ e1 , e2 ⟩ ◃) + move (child 2) +>e ⟨ e1 , ▹ e2 ◃ ⟩₂
    EMPairParent1    : {e1 e2 : hexp} →
                       ( ⟨ ▹ e1 ◃ , e2 ⟩₁ ) + move parent +>e (▹ ⟨ e1 , e2 ⟩ ◃)
    EMPairParent2    : {e1 e2 : hexp} →
                       ( ⟨ e1 , ▹ e2 ◃ ⟩₂ ) + move parent +>e (▹ ⟨ e1 , e2 ⟩ ◃)
    EMFstChild1      : {e : hexp} →
                       ▹ fst e ◃ + move (child 1) +>e fst ▹ e ◃
    EMFstParent      : {e : hexp} →
                       fst ▹ e ◃ + move parent +>e ▹ fst e  ◃
    EMSndChild1      : {e : hexp} →
                       ▹ snd e ◃ + move (child 1) +>e snd ▹ e ◃
    EMSndParent      : {e : hexp} →
                       snd ▹ e ◃ + move parent +>e ▹ snd e  ◃
    EMNEHoleChild1   : {e : hexp} {u : Nat} →
                       (▹ ⦇⌜ e ⌟⦈[ u ] ◃) + move (child 1) +>e ⦇⌜ ▹ e ◃ ⌟⦈[ u ]
    EMNEHoleParent   : {e : hexp} {u : Nat} →
                       ⦇⌜ ▹ e ◃ ⌟⦈[ u ] + move parent +>e (▹ ⦇⌜ e ⌟⦈[ u ] ◃)

  mutual
  -- synthetic action expressions.
    data _⊢_=>_~_~>_=>_ : (Γ : tctx) → (e1 : zexp) → (t1 : htyp) → (α : action) →
                          (e2 : zexp) → (t2 : htyp) → Set where
      SAFinish    : {Γ : tctx} {e : hexp} {t : htyp} {u : Nat} →
                    Γ ⊢ e => t →
                    Γ ⊢ ▹ ⦇⌜ e ⌟⦈[ u ] ◃ => ⦇-⦈ ~ finish ~> ▹ e ◃ => t
      SAMove      : {δ : direction} {e e' : zexp} {Γ : tctx} {t : htyp} →
                    e + move δ +>e e' →
                    Γ ⊢ e => t ~ move δ ~> e' => t
      SADel       : {Γ : tctx} {e : hexp} {t : htyp} {u : Nat} →
                    Γ ⊢ ▹ e ◃ => t ~ del u ~> ▹ ⦇-⦈[ u ] ◃ => ⦇-⦈
      SAConNumlit : {Γ : tctx} {n : Nat} {u u1 : Nat} →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ => ⦇-⦈ ~ construct (numlit n u1) ~> ▹ N n ◃ => num
      SAConPlus1  : {Γ : tctx} {e : hexp} {t : htyp} {u1 u2 : Nat} →
                    t ~ num →
                    Γ ⊢ ▹ e ◃ => t ~ construct (plus u1 u2) ~> e ·+₂ ▹ ⦇-⦈[ u2 ] ◃ => num
      SAConPlus2  : {Γ : tctx} {e : hexp} {t : htyp} {u1 u2 : Nat} →
                    t ~̸ num →
                    Γ ⊢ ▹ e ◃ => t ~ construct (plus u1 u2) ~>
                      ⦇⌜ e ⌟⦈[ u1 ] ·+₂ ▹ ⦇-⦈[ u2 ] ◃ => num
      SAConAsc    : {Γ : tctx} {e : hexp} {t : htyp} →
                    Γ ⊢ ▹ e ◃ => t ~ construct asc  ~> (e ·:₂ ▹ t ◃ ) => t
      SAConVar    : {Γ : tctx} {x : Nat} {t : htyp} {u u1 : Nat} →
                    (x , t) ∈ Γ →
                      Γ ⊢ ▹ ⦇-⦈[ u ] ◃ => ⦇-⦈ ~ construct (var x u1) ~> ▹ X x ◃ => t
      SAConLam    : {Γ : tctx} {x : Nat} {u u1 u2 : Nat} →
                    x # Γ →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ => ⦇-⦈ ~ construct (lam x u1 u2) ~>
                      (·λ x ·[ ▹ ⦇-⦈ ◃ ]₁ ⦇-⦈[ u2 ]) => (⦇-⦈ ==> ⦇-⦈)
      SAConApArr  : {Γ : tctx} {t t1 t2 : htyp} {e : hexp} {u1 u2 : Nat} →
                    t ▸arr (t1 ==> t2) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (ap u1 u2) ~>
                      e ∘₂ ▹ ⦇-⦈[ u2 ] ◃ => t2
      SAConApOtw  : {Γ : tctx} {t : htyp} {e : hexp} {u1 u2 : Nat} →
                    t ~̸ (⦇-⦈ ==> ⦇-⦈) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (ap u1 u2) ~>
                      ⦇⌜ e ⌟⦈[ u1 ] ∘₂ ▹ ⦇-⦈[ u2 ] ◃ => ⦇-⦈
      SAConInl    : {Γ : tctx} {t : htyp} {u u1 u2 : Nat} →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ => t ~ construct (inl u1 u2) ~>
                      inl (⦇-⦈[ u2 ]) ·:₂ (▹ ⦇-⦈ ◃ ⊕₁ ⦇-⦈) => (⦇-⦈ ⊕ ⦇-⦈)
      SAConInr    : {Γ : tctx} {t : htyp} {u u1 u2 : Nat} →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ => t ~ construct (inr u1 u2) ~>
                      inr (⦇-⦈[ u2 ]) ·:₂ (⦇-⦈ ⊕₂ ▹ ⦇-⦈ ◃) => (⦇-⦈ ⊕ ⦇-⦈)
      SAConCase1  : {Γ : tctx} {x y : Nat} {t t1 t2 : htyp} {e : hexp} {u1 u2 u3 : Nat} →
                    x # Γ →
                    y # Γ →
                    t ▸sum (t1 ⊕ t2) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (case x y u1 u2 u3) ~>
                      (case₂ e x (▹ ⦇-⦈[ u2 ] ◃) y ⦇-⦈[ u3 ]) ·:₁ ⦇-⦈ => ⦇-⦈
      SAConCase2  : {Γ : tctx} {x y : Nat} {t : htyp} {e : hexp} → {u1 u2 u3 : Nat} →
                    x # Γ →
                    y # Γ →
                    t ~̸ (⦇-⦈ ⊕ ⦇-⦈) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (case x y u1 u2 u3) ~>
                      (case₁ (⦇⌜ ▹ e ◃ ⌟⦈[ u1 ]) x ⦇-⦈[ u2 ] y ⦇-⦈[ u3 ]) ·:₁ ⦇-⦈ => ⦇-⦈
      SAConPair   : {Γ : tctx} {t : htyp} {u u1 u2 : Nat} →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ => t ~ construct (pair u1 u2) ~>
                      ⟨ ▹ ⦇-⦈[ u1 ] ◃ , ⦇-⦈[ u2 ] ⟩₁ => (⦇-⦈ ⊠ ⦇-⦈)
      SAConFst1   : {Γ : tctx} {t t1 t2 : htyp} {e : hexp} {u : Nat} →
                    t ▸prod (t1 ⊠ t2) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (fst u) ~> ▹ fst e ◃ => t1
      SAConFst2   : {Γ : tctx} {t : htyp} {e : hexp} {u : Nat} →
                    t ~̸ (⦇-⦈ ⊠ ⦇-⦈) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (fst u) ~> fst ⦇⌜ ▹ e ◃ ⌟⦈[ u ] => ⦇-⦈
      SAConSnd1   : {Γ : tctx} {t t1 t2 : htyp} {e : hexp} {u : Nat} →
                    t ▸prod (t1 ⊠ t2) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (snd u) ~> ▹ snd e ◃ => t2
      SAConSnd2   : {Γ : tctx} {t : htyp} {e : hexp} {u : Nat} →
                    t ~̸ (⦇-⦈ ⊠ ⦇-⦈) →
                    Γ ⊢ ▹ e ◃ => t ~ construct (snd u) ~> snd ⦇⌜ ▹ e ◃ ⌟⦈[ u ]  => ⦇-⦈
      SAConNEHole : {Γ : tctx} {e : hexp} {t : htyp} {u : Nat} →
                    Γ ⊢ ▹ e ◃ => t ~ construct (nehole u) ~> ⦇⌜ ▹ e ◃ ⌟⦈[ u ] => ⦇-⦈
      SAZipPlus1  : {Γ : tctx} {e : hexp} {eh eh' : zexp} {α : action} →
                    Γ ⊢ eh ~ α ~> eh' ⇐ num →
                    Γ ⊢ (eh ·+₁ e) => num ~ α ~> (eh' ·+₁ e) => num
      SAZipPlus2  : {Γ : tctx} {e : hexp} {eh eh' : zexp} {α : action} →
                    Γ ⊢ eh ~ α ~> eh' ⇐ num →
                    Γ ⊢ (e ·+₂ eh) => num ~ α ~> (e ·+₂ eh') => num
      SAZipAsc1   : {Γ : tctx} {e e' : zexp} {α : action} {t : htyp} →
                    Γ ⊢ e ~ α ~> e' ⇐ t →
                    Γ ⊢ (e ·:₁ t) => t ~ α ~> (e' ·:₁ t) => t
      SAZipAsc2   : {Γ : tctx} {e : hexp} {α : action} {t t' : ztyp} {t◆ t'◆ : htyp} →
                    t + α +> t' →
                    erase-t t' t'◆ →
                    erase-t t t◆ →
                    Γ ⊢ e <= t'◆ →
                    Γ ⊢ (e ·:₂ t) => t◆ ~ α ~> (e ·:₂ t') => t'◆
      SAZipLam1   : {Γ : tctx} {e : hexp} {t1 t1' : ztyp} {t1◆ t1'◆ t2 t2' : htyp} {x : Nat}
                    {α : action} →
                    x # Γ →
                    erase-t t1 t1◆ →
                    erase-t t1' t1'◆ →
                    t1 + α +> t1' →
                    (Γ ,, (x , t1◆)) ⊢ e => t2 →
                    (Γ ,, (x , t1'◆)) ⊢ e => t2' →
                    Γ ⊢ (·λ x ·[ t1 ]₁ e) => (t1◆ ==> t2) ~ α ~>
                      (·λ x ·[ t1' ]₁ e) => (t1'◆ ==> t2')
      SAZipLam2   : {Γ : tctx} {e e' : zexp} {e◆ : hexp} {t1 t2 t2' : htyp} {x : Nat}
                    {α : action }→
                    x # Γ →
                    erase-e e e◆ →
                    (Γ ,, (x , t1)) ⊢ e◆ => t2 →
                    (Γ ,, (x , t1)) ⊢ e => t2 ~ α ~> e' => t2' →
                    Γ ⊢ (·λ x ·[ t1 ]₂ e) => (t1 ==> t2) ~ α ~>
                      (·λ x ·[ t1 ]₂ e') => (t1 ==> t2')
      SAZipApArr  : {Γ : tctx} {t t1 t2 t3 t4 : htyp} {α : action}
                    {eh eh' : zexp} {e eh◆ : hexp} →
                    t ▸arr (t3 ==> t4) →
                    erase-e eh eh◆ →
                    Γ ⊢ (eh◆) => t2 →
                    Γ ⊢ eh => t2 ~ α ~> eh' => t →
                    Γ ⊢ e <= t3 →
                    Γ ⊢ (eh ∘₁ e) => t1 ~ α ~> (eh' ∘₁ e) => t4
      SAZipApAna  : {Γ : tctx} {t' t2 t : htyp} {e : hexp}
                    {eh eh' : zexp} {α : action}  →
                    t' ▸arr (t2 ==> t) →
                    Γ ⊢ e => t' →
                    Γ ⊢ eh ~ α ~> eh' ⇐ t2 →
                    Γ ⊢ (e ∘₂ eh) => t ~ α ~> (e ∘₂ eh') => t
      SAZipPair1  : {Γ : tctx} {t1 t1' t2 : htyp} {α : action} {eh eh' : zexp}
                    {e eh◆ : hexp} →
                    erase-e eh eh◆ →
                    Γ ⊢ (eh◆) => t1 →
                    Γ ⊢ eh => t1 ~ α ~> eh' => t1' →
                    Γ ⊢ e => t2 →
                    Γ ⊢ ⟨ eh , e ⟩₁ => (t1 ⊠ t2) ~ α ~> ⟨ eh' , e ⟩₁ => (t1' ⊠ t2)
      SAZipPair2  : {Γ : tctx} {t1 t2 t2' : htyp} {α : action} {eh eh' : zexp}
                    {e eh◆ : hexp} →
                    Γ ⊢ e => t1 →
                    erase-e eh eh◆ →
                    Γ ⊢ (eh◆) => t2 →
                    Γ ⊢ eh => t2 ~ α ~> eh' => t2' →
                    Γ ⊢ ⟨ e , eh ⟩₂ => (t1 ⊠ t2) ~ α ~> ⟨ e , eh' ⟩₂ => (t1 ⊠ t2')
      SAZipFst    : {Γ : tctx} {t× t×' t1 t1' t2 t2' : htyp} {α : action}
                    {eh eh' : zexp} {eh◆ : hexp} →
                    t× ▸prod (t1 ⊠ t2) →
                    t×' ▸prod (t1' ⊠ t2') →
                    erase-e eh eh◆ →
                    Γ ⊢ (eh◆) => t× →
                    Γ ⊢ eh => t× ~ α ~> eh' => t×' →
                    Γ ⊢ fst eh => t1 ~ α ~> fst eh' => t1'
      SAZipSnd    : {Γ : tctx} {t× t×' t1 t1' t2 t2' : htyp} {α : action}
                    {eh eh' : zexp} {eh◆ : hexp} →
                    t× ▸prod (t1 ⊠ t2) →
                    t×' ▸prod (t1' ⊠ t2') →
                    erase-e eh eh◆ →
                    Γ ⊢ (eh◆) => t× →
                    Γ ⊢ eh => t× ~ α ~> eh' => t×' →
                    Γ ⊢ snd eh => t2 ~ α ~> snd eh' => t2'
      SAZipNEHole : {Γ : tctx} {e e' : zexp} {u : Nat} {t t' : htyp} {α : action}
                    {e◆ : hexp} →
                    erase-e e e◆ →
                    Γ ⊢ e◆ => t →
                    Γ ⊢ e => t ~ α ~> e' => t' →
                    Γ ⊢ ⦇⌜ e ⌟⦈[ u ] => ⦇-⦈ ~ α ~>  ⦇⌜ e' ⌟⦈[ u ] => ⦇-⦈

    -- analytic action expressions
    data _⊢_~_~>_⇐_ : (Γ : tctx) → (e : zexp) → (α : action) →
                        (e' : zexp) → (t : htyp) → Set where
      AASubsume   : {Γ : tctx} {e e' : zexp} {t t' t'' : htyp} {α : action} {e◆ : hexp} →
                    erase-e e e◆ →
                    Γ ⊢ e◆ => t' →
                    Γ ⊢ e => t' ~ α ~> e' => t'' →
                    t ~ t'' →
                    Γ ⊢ e ~ α ~> e' ⇐ t
      AAFinish    : {Γ : tctx} {e : hexp} {t : htyp} {u : Nat} →
                    Γ ⊢ e <= t →
                    Γ ⊢ ▹ ⦇⌜ e ⌟⦈[ u ] ◃ ~ finish ~> ▹ e ◃ ⇐ t
      AAMove      : {e e' : zexp} {δ : direction} {Γ : tctx} {t : htyp} →
                    e + move δ +>e e' →
                    Γ ⊢ e ~ move δ ~> e' ⇐ t
      AADel       : {e : hexp} {Γ : tctx} {t : htyp} {u : Nat} →
                    Γ ⊢ ▹ e ◃ ~ del u ~> ▹ ⦇-⦈[ u ] ◃ ⇐ t
      AAConNumlit : {Γ : tctx} {t : htyp} {n u u1 : Nat} →
                    t ~̸ num →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (numlit n u1) ~> ⦇⌜ ▹ (N n) ◃ ⌟⦈[ u1 ] ⇐ t
      AAConAsc    : {Γ : tctx} {e : hexp} {t : htyp} →
                    Γ ⊢ ▹ e ◃ ~ construct asc ~> (e ·:₂ ▹ t ◃) ⇐ t
      AAConVar    : {Γ : tctx} {t t' : htyp} {x u u1 : Nat} →
                    t ~̸ t' →
                    (x , t') ∈ Γ →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (var x u1) ~> ⦇⌜ ▹ X x ◃ ⌟⦈[ u1 ] ⇐ t
      AAConLam1   : {Γ : tctx} {x : Nat} {t t1 t2 : htyp} {u u1 u2 : Nat} →
                    x # Γ →
                    t ▸arr (t1 ==> t2) →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (lam x u1 u2) ~>
                      ·λ x (▹ ⦇-⦈[ u2 ] ◃) ⇐ t
      AAConLam2   : {Γ : tctx} {x : Nat} {t : htyp} {u u1 u2 : Nat} →
                    x # Γ →
                    t ~̸ (⦇-⦈ ==> ⦇-⦈) →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (lam x u1 u2) ~>
                      ⦇⌜ ·λ x ⦇-⦈[ u2 ] ·:₂ (▹ ⦇-⦈ ◃ ==>₁ ⦇-⦈) ⌟⦈[ u1 ] ⇐ t
      AAConInl1   : {Γ : tctx} {t+ t1 t2 : htyp} {u u1 u2 : Nat} →
                    t+ ▸sum (t1 ⊕ t2) →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (inl u1 u2) ~> inl ▹ ⦇-⦈[ u2 ] ◃ ⇐ t+
      AAConInl2   : {Γ : tctx} {t : htyp} {u u1 u2 : Nat} →
                    t ~̸ (⦇-⦈ ⊕ ⦇-⦈) →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (inl u1 u2) ~>
                      ⦇⌜ inl ⦇-⦈[ u2 ] ·:₂ (▹ ⦇-⦈ ◃ ⊕₁ ⦇-⦈) ⌟⦈[ u1 ] ⇐ t
      AAConInr1   : {Γ : tctx} {t+ t1 t2 : htyp} {u u1 u2 : Nat} →
                    t+ ▸sum (t1 ⊕ t2) →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (inr u1 u2) ~> inr ▹ ⦇-⦈[ u2 ] ◃ ⇐ t+
      AAConInr2   : {Γ : tctx} {t : htyp} {u u1 u2 : Nat} →
                    t ~̸ (⦇-⦈ ⊕ ⦇-⦈) →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (inr u1 u2) ~>
                      ⦇⌜ inr ⦇-⦈[ u2 ] ·:₂ (▹ ⦇-⦈ ◃ ⊕₁ ⦇-⦈) ⌟⦈[ u1 ] ⇐ t
      AAConCase   : {Γ : tctx} {x y : Nat} {t : htyp} {u u1 u2 u3 : Nat} →
                    x # Γ →
                    y # Γ →
                    Γ ⊢ ▹ ⦇-⦈[ u ] ◃ ~ construct (case x y u1 u2 u3) ~>
                      case₁ ▹ ⦇-⦈[ u1 ] ◃ x ⦇-⦈[ u2 ] y ⦇-⦈[ u3 ] ⇐ t
      AAZipLam    : {Γ : tctx} {x : Nat} {t t1 t2 : htyp} {e e' : zexp} {α : action} →
                    x # Γ →
                    t ▸arr (t1 ==> t2) →
                    (Γ ,, (x , t1)) ⊢ e ~ α ~> e' ⇐ t2 →
                    Γ ⊢ (·λ x e) ~ α ~> (·λ x e') ⇐ t
      AAZipInl    : {Γ : tctx} {t+ t1 t2 : htyp} {e e' : zexp} {α : action} →
                    t+ ▸sum (t1 ⊕ t2) →
                    Γ ⊢ e ~ α ~> e' ⇐ t1 →
                    Γ ⊢ inl e ~ α ~> inl e' ⇐ t+
      AAZipInr    : {Γ : tctx} {t+ t1 t2 : htyp} {e e' : zexp} {α : action} →
                    t+ ▸sum (t1 ⊕ t2) →
                    Γ ⊢ e ~ α ~> e' ⇐ t2 →
                    Γ ⊢ inr e ~ α ~> inr e' ⇐ t+
      AAZipCase1  : {Γ : tctx} {e e' : zexp} {e◆ e1 e2 : hexp} {x y : Nat}
                    {t t0 t+ t1 t2 : htyp} {α : action} →
                    x # Γ →
                    y # Γ →
                    erase-e e e◆ →
                    Γ ⊢ e◆ => t0 →
                    Γ ⊢ e => t0 ~ α ~> e' => t+ →
                    t+ ▸sum (t1 ⊕ t2) →
                    (Γ ,, (x , t1)) ⊢ e1 <= t →
                    (Γ ,, (y , t2)) ⊢ e2 <= t →
                    Γ ⊢ case₁ e x e1 y e2 ~ α ~> case₁ e' x e1 y e2 ⇐ t
      AAZipCase2  : {Γ : tctx} {e1 e1' : zexp} {e e2 : hexp} {x y : Nat}
                    {t t+ t1 t2 : htyp} {α : action} →
                    x # Γ →
                    y # Γ →
                    Γ ⊢ e => t+ →
                    t+ ▸sum (t1 ⊕ t2) →
                    (Γ ,, (x , t1)) ⊢ e1 ~ α ~> e1' ⇐ t →
                    Γ ⊢ case₂ e x e1 y e2 ~ α ~> case₂ e x e1' y e2 ⇐ t
      AAZipCase3  : {Γ : tctx} {e2 e2' : zexp} {e e1 : hexp} {x y : Nat}
                    {t t+ t1 t2 : htyp} {α : action} →
                    x # Γ →
                    y # Γ →
                    Γ ⊢ e => t+ →
                    t+ ▸sum (t1 ⊕ t2) →
                    (Γ ,, (y , t2)) ⊢ e2 ~ α ~> e2' ⇐ t →
                    Γ ⊢ case₃ e x e1 y e2 ~ α ~> case₃ e x e1 y e2' ⇐ t

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
------------------------------------------------------------------------------
-- PA properties
------------------------------------------------------------------------------

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

module PA.Axiomatic.Mendelson.PropertiesATP where

open import PA.Axiomatic.Mendelson.Base

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

+-leftIdentity : ∀ n → zero + n ≈ n
+-leftIdentity = S₅

-- See Issue https://github.com/asr/apia/issues/81 .
+-rightIdentityA : ℕ → Set
+-rightIdentityA i = i + zero ≈ i
{-# ATP definition +-rightIdentityA #-}

+-rightIdentity : ∀ n → n + zero ≈ n
+-rightIdentity = S₉ +-rightIdentityA A0 is
  where
  A0 : +-rightIdentityA zero
  A0 = +-leftIdentity zero

  postulate is : ∀ i → +-rightIdentityA i → +-rightIdentityA (succ i)
  {-# ATP prove is #-}

-- See Issue https://github.com/asr/apia/issues/81 .
x+Sy≈S[x+y]A : ℕ → ℕ → Set
x+Sy≈S[x+y]A n i = i + succ n ≈ succ (i + n)
{-# ATP definition x+Sy≈S[x+y]A #-}

x+Sy≈S[x+y] : ∀ m n → m + succ n ≈ succ (m + n)
x+Sy≈S[x+y] m n = S₉ (x+Sy≈S[x+y]A n) A0 is m
  where
  postulate A0 : x+Sy≈S[x+y]A n zero
  {-# ATP prove A0 #-}

  postulate is : ∀ i → x+Sy≈S[x+y]A n i → x+Sy≈S[x+y]A n (succ i)
  {-# ATP prove is #-}

-- See Issue https://github.com/asr/apia/issues/81 .
+-leftCongA : ℕ → ℕ → ℕ → Set
+-leftCongA m n i = m + i ≈ n + i
{-# ATP definition +-leftCongA #-}

+-leftCong : ∀ {m n o} → m ≈ n → m + o ≈ n + o
+-leftCong {m} {n} {o} h = S₉ (+-leftCongA m n) A0 is o
  where
  postulate A0 : +-leftCongA m n zero
  {-# ATP prove A0 +-rightIdentity #-}

  postulate is : ∀ i → +-leftCongA m n i → +-leftCongA m n (succ i)
  {-# ATP prove is x+Sy≈S[x+y] #-}

-- See Issue https://github.com/asr/apia/issues/81 .
+-commA : ℕ → ℕ → Set
+-commA n i = i + n ≈ n + i
{-# ATP definition +-commA #-}

+-comm : ∀ m n → m + n ≈ n + m
+-comm m n = S₉ (+-commA n) A0 is m
  where
  postulate A0 : +-commA n zero
  {-# ATP prove A0 +-rightIdentity #-}

  postulate is : ∀ i → +-commA n i → +-commA n (succ i)
  {-# ATP prove is x+Sy≈S[x+y] #-}

+-asocc : ∀ m n o → m + n + o ≈ m + (n + o)
+-asocc m n o = S₉ A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≈ i + (n + o)
  {-# ATP definition A #-}

  postulate A0 : A zero
  {-# ATP prove A0 +-leftCong #-}

  postulate is : ∀ i → A i → A (succ i)
  {-# ATP prove is +-leftCong #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

-- Definition of a cost monoid.

open import Relation.Binary using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)

module Calf.CostMonoid where

open import Level using (Level; 0ℓ; suc; _⊔_)
open import Algebra.Core
open import Relation.Binary.PropositionalEquality using (_≡_; resp₂)
open import Data.Product

module _ {ℂ : Set} where
  Relation = Rel ℂ 0ℓ

  _≈_ : Relation
  _≈_ = _≡_

  open import Algebra.Definitions _≈_
  open import Algebra.Structures _≈_ public
  open import Relation.Binary.Structures _≈_

  record IsCancellative (_∙_ : Op₂ ℂ) : Set where
    field
      ∙-cancel-≡ : Cancellative _∙_

    ∙-cancelˡ-≡ : LeftCancellative _∙_
    ∙-cancelˡ-≡ = proj₁ ∙-cancel-≡

    ∙-cancelʳ-≡ : RightCancellative _∙_
    ∙-cancelʳ-≡ = proj₂ ∙-cancel-≡

  record IsMonotone (_∙_ : Op₂ ℂ) (_≤_ : Relation) (isPreorder : IsPreorder _≤_) : Set where
    field
      ∙-mono-≤ : _∙_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_

    open IsPreorder isPreorder
      using ()
      renaming (reflexive to ≤-reflexive; refl to ≤-refl; trans to ≤-trans)

    ∙-monoˡ-≤ : ∀ n → (_∙ n) Preserves _≤_ ⟶ _≤_
    ∙-monoˡ-≤ n m≤o = ∙-mono-≤ m≤o (≤-refl {n})

    ∙-monoʳ-≤ : ∀ n → (n ∙_) Preserves _≤_ ⟶ _≤_
    ∙-monoʳ-≤ n m≤o = ∙-mono-≤ (≤-refl {n}) m≤o

  record IsCostMonoid (_+_ : Op₂ ℂ) (zero : ℂ) (_≤_ : Relation) : Set where
    field
      isMonoid       : IsMonoid _+_ zero
      isCancellative : IsCancellative _+_
      isPreorder     : IsPreorder _≤_
      isMonotone     : IsMonotone _+_ _≤_ isPreorder

    open IsMonoid isMonoid public
      using ()
      renaming (
        identityˡ to +-identityˡ;
        identityʳ to +-identityʳ;
        assoc to +-assoc
      )

    open IsCancellative isCancellative public
      renaming (
        ∙-cancel-≡ to +-cancel-≡;
        ∙-cancelˡ-≡ to +-cancelˡ-≡;
        ∙-cancelʳ-≡ to +-cancelʳ-≡
      )

    open IsPreorder isPreorder public
      using ()
      renaming (reflexive to ≤-reflexive; refl to ≤-refl; trans to ≤-trans)

    open IsMonotone isMonotone public
      renaming (
        ∙-mono-≤ to +-mono-≤;
        ∙-monoˡ-≤ to +-monoˡ-≤;
        ∙-monoʳ-≤ to +-monoʳ-≤
      )

  record IsParCostMonoid (_⊕_ : Op₂ ℂ) (𝟘 : ℂ) (_⊗_ : Op₂ ℂ) (𝟙 : ℂ) (_≤_ : Relation) : Set where
    field
      isMonoid            : IsMonoid _⊕_ 𝟘
      isCommutativeMonoid : IsCommutativeMonoid _⊗_ 𝟙
      isCancellative      : IsCancellative _⊕_
      isPreorder          : IsPreorder _≤_
      isMonotone-⊕        : IsMonotone _⊕_ _≤_ isPreorder
      isMonotone-⊗        : IsMonotone _⊗_ _≤_ isPreorder

    open IsMonoid isMonoid public
      using ()
      renaming (
        identityˡ to ⊕-identityˡ;
        identityʳ to ⊕-identityʳ;
        assoc to ⊕-assoc
      )

    open IsCommutativeMonoid isCommutativeMonoid public
      using ()
      renaming (
        identityˡ to ⊗-identityˡ;
        identityʳ to ⊗-identityʳ;
        assoc to ⊗-assoc;
        comm to ⊗-comm
      )

    open IsCancellative isCancellative public
      renaming (
        ∙-cancel-≡ to ⊕-cancel-≡;
        ∙-cancelˡ-≡ to ⊕-cancelˡ-≡;
        ∙-cancelʳ-≡ to ⊕-cancelʳ-≡
      )

    open IsPreorder isPreorder public
      using ()
      renaming (reflexive to ≤-reflexive; refl to ≤-refl; trans to ≤-trans)

    open IsMonotone isMonotone-⊕ public
      renaming (
        ∙-mono-≤ to ⊕-mono-≤;
        ∙-monoˡ-≤ to ⊕-monoˡ-≤;
        ∙-monoʳ-≤ to ⊕-monoʳ-≤
      )

    open IsMonotone isMonotone-⊗ public
      renaming (
        ∙-mono-≤ to ⊗-mono-≤;
        ∙-monoˡ-≤ to ⊗-monoˡ-≤;
        ∙-monoʳ-≤ to ⊗-monoʳ-≤
      )

record CostMonoid : Set₁ where
  infixl 6 _+_

  field
    ℂ            : Set
    _+_          : Op₂ ℂ
    zero         : ℂ
    _≤_          : Relation
    isCostMonoid : IsCostMonoid _+_ zero _≤_

  open IsCostMonoid isCostMonoid public

  module ≤-Reasoning where
    open import Relation.Binary.Reasoning.Base.Triple
      isPreorder
      ≤-trans
      (resp₂ _≤_)
      (λ h → h)
      ≤-trans
      ≤-trans
      public
      hiding (step-≈; step-≈˘; step-<)

record ParCostMonoid : Set₁ where
  infixl 7 _⊗_
  infixl 6 _⊕_

  field
    ℂ               : Set
    _⊕_             : Op₂ ℂ
    𝟘               : ℂ
    _⊗_             : Op₂ ℂ
    𝟙               : ℂ
    _≤_             : Relation
    isParCostMonoid : IsParCostMonoid _⊕_ 𝟘 _⊗_ 𝟙 _≤_

  open IsParCostMonoid isParCostMonoid public

  costMonoid : CostMonoid
  costMonoid = record
    { ℂ = ℂ
    ; _+_ = _⊕_
    ; zero = 𝟘
    ; _≤_ = _≤_
    ; isCostMonoid = record
      { isMonoid = isMonoid
      ; isPreorder = isPreorder
      ; isCancellative = isCancellative
      ; isMonotone = isMonotone-⊕
      }
    }

  module ≤-Reasoning where
    open import Relation.Binary.Reasoning.Base.Triple
      isPreorder
      ≤-trans
      (resp₂ _≤_)
      (λ h → h)
      ≤-trans
      ≤-trans
      public
      hiding (step-≈; step-≈˘; step-<)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
-- Minimal implicational logic, PHOAS approach, initial encoding

module Pi.ArrMp where

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty

-- Context and truth judgement

Cx : Set1
Cx = Ty -> Set

isTrue : Ty -> Cx -> Set
isTrue a tc = tc a

-- Terms

module ArrMp where
  infixl 1 _$_
  data Tm (tc : Cx) : Ty -> Set where
    var  : forall {a}   -> isTrue a tc               -> Tm tc a
    lam' : forall {a b} -> (isTrue a tc -> Tm tc b)  -> Tm tc (a => b)
    _$_  : forall {a b} -> Tm tc (a => b) -> Tm tc a -> Tm tc b

  lam'' : forall {tc a b} -> (Tm tc a -> Tm tc b) -> Tm tc (a => b)
  lam'' f = lam' \x -> f (var x)

  syntax lam'' (\a -> b) = lam a => b

  Thm : Ty -> Set1
  Thm a = forall {tc} -> Tm tc a
open ArrMp public

-- Example theorems

aI : forall {a} -> Thm (a => a)
aI =
  lam x => x

aK : forall {a b} -> Thm (a => b => a)
aK =
  lam x =>
    lam _ => x

aS : forall {a b c} -> Thm ((a => b => c) => (a => b) => a => c)
aS =
  lam f =>
    lam g =>
      lam x => f $ x $ (g $ x)

tSKK : forall {a} -> Thm (a => a)
tSKK {a = a} =
  aS {b = a => a} $ aK $ aK

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


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

module container.m where

open import container.m.coalgebra public
open import container.m.from-nat public
-- open import container.m.core public
-- open import container.m.extensionality public
-- open import container.m.level public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

module TypeConstructorsWhichPreserveGuardedness2 where

record ⊤ : Set where

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

-- This should not be allowed.

ℕ : Set
ℕ = ⊤ ⊎ ℕ

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

open import BaseOver

module Spaces.Flattening {i j k}
  (A : Set i) (B : Set j) (f g : B → A)
  (C : A → Set k) (D : (b : B) → C (f b) ≃ C (g b)) where

open import Spaces.FlatteningTypes A B f g C D

-- The family of paths used in the definition of [flatten]
paths-flatten : (b : B) → (cct (f b) == cct (g b) [ (λ w → (P w → Wt)) ↓ pp b ])
paths-flatten b =
  ↓-app→cst-in (λ q → ppt b _ ∘' ap (cct (g b)) (↓-pp-out q))

flatten-curried : (w : W) → (P w → Wt)
flatten-curried = W-rec _ cct paths-flatten

flatten : Σ W P → Wt
flatten (w , x) = flatten-curried w x

unflatten : Wt → Σ W P
unflatten = Wt-rec-nondep _ (λ a c → (cc a , c))
                            (λ b d → Σ-eq (pp b) (↓-pp-in refl))

--

flatten-unflatten : (w : Wt) → flatten (unflatten w) ≡ w
flatten-unflatten =
  Wt-rec _
    (λ _ _ → refl)
    (λ b d → ↓-◯=id-in unflatten flatten
      (ap flatten (ap unflatten (ppt b d))
                 ≡⟨ Wt-rec-nondep-β _ (λ a c → (cc a , c)) (λ b d → Σ-eq (pp b) (↓-pp-in refl)) b d |in-ctx ap flatten ⟩
       ap flatten (Σ-eq (pp b) (↓-pp-in refl))
                 ≡⟨ split-ap2 flatten (pp b) (↓-pp-in refl) ⟩
       ↓-app→cst-out (apd flatten-curried (pp b)) (↓-pp-in refl)
                 ≡⟨ W-rec-β _ cct paths-flatten b |in-ctx (λ u → ↓-app→cst-out u (↓-pp-in refl)) ⟩
       ↓-app→cst-out (paths-flatten b) (↓-pp-in refl)
                 ≡⟨ refl ⟩
       ↓-app→cst-out (↓-app→cst-in
         (λ q → ppt b _ ∘' ap (cct (g b)) (↓-pp-out q))) (↓-pp-in refl)
                 ≡⟨ ↓-app→cst-β (λ q → ppt b _ ∘' ap (cct (g b)) (↓-pp-out q)) (↓-pp-in refl) ⟩
       ppt b d ∘' ap (cct (g b)) (↓-pp-out (↓-pp-in refl))
                 ≡⟨ ↓-pp-β refl |in-ctx (λ u → ppt b d ∘' ap (cct (g b)) u) ⟩
       ppt b d ∎))

unflatten-flatten-curried : (w : W) (x : P w)
  →  unflatten (flatten-curried w x) ≡ (w , x)
unflatten-flatten-curried =
  W-rec _ (λ a x → refl)
    (λ b → ↓-Π-in
    (λ q → ↓-◯=id-in flatten unflatten
      (ap unflatten (ap flatten (Σ-eq (pp b) q))
                 ≡⟨ split-ap2 flatten (pp b) q |in-ctx ap unflatten ⟩
       ap unflatten (↓-app→cst-out (apd flatten-curried (pp b)) q)
                 ≡⟨ W-rec-β _ cct paths-flatten b |in-ctx (λ u → ap unflatten (↓-app→cst-out u q)) ⟩
       ap unflatten (↓-app→cst-out (paths-flatten b) q)
                 ≡⟨ refl ⟩
       ap unflatten (↓-app→cst-out (↓-app→cst-in (λ qq → ppt b _ ∘' ap (cct (g b)) (↓-pp-out qq))) q)
                 ≡⟨ ↓-app→cst-β (λ qq → ppt b _ ∘' ap (cct (g b)) (↓-pp-out qq)) q |in-ctx ap unflatten ⟩
       ap unflatten (ppt b _ ∘' ap (cct (g b)) (↓-pp-out q))
                 ≡⟨ ap-∘' unflatten (ppt b _) (ap (cct (g b)) (↓-pp-out q)) ⟩
       ap unflatten (ppt b _) ∘' ap unflatten (ap (cct (g b)) (↓-pp-out q))
                 ≡⟨ Wt-rec-nondep-β _ (λ a c → (cc a , c)) (λ b d → Σ-eq (pp b) (↓-pp-in refl)) b _ |in-ctx (λ u → u ∘' ap unflatten (ap (cct (g b)) (↓-pp-out q))) ⟩
       Σ-eq (pp b) (↓-pp-in refl) ∘' ap unflatten (ap (cct (g b)) (↓-pp-out q))
                 ≡⟨ compose-ap unflatten (cct (g b)) (↓-pp-out q) |in-ctx (λ u → (Σ-eq (pp b) (↓-pp-in refl) ∘' u)) ⟩
       Σ-eq (pp b) (↓-pp-in refl) ∘' ap (unflatten ◯ cct (g b)) (↓-pp-out q)
                 ≡⟨ refl ⟩
       Σ-eq (pp b) (↓-pp-in refl) ∘' ap (λ x → (cc (g b), x)) (↓-pp-out q)
                 ≡⟨ ap-cst,id P (↓-pp-out q) |in-ctx (λ u → Σ-eq (pp b) (↓-pp-in refl) ∘' u) ⟩
       Σ-eq (pp b) (↓-pp-in refl) ∘' Σ-eq refl (↓-pp-out q)
                 ≡⟨ Σ-∘' (↓-pp-in refl) (↓-pp-out q) ⟩
       Σ-eq (pp b) (↓-pp-in refl ∘'dep ↓-pp-out q)
                 ≡⟨ to-transp-weird q (pp-path _ _) |in-ctx Σ-eq (pp b) ⟩
       Σ-eq (pp b) q ∎)))

unflatten-flatten : (wx : Σ W P) → unflatten (flatten wx) ≡ wx
unflatten-flatten (w , x) = unflatten-flatten-curried w x

eqv : Σ W P ≃ Wt
eqv = (flatten , iso-is-eq flatten unflatten flatten-unflatten unflatten-flatten)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

postulate
  A : Set
  B : Set
  b : B

f : (\ {a : A} (x : B) → b) ≡ (\ _ → b)
f i x = b


text:
module RandomAccessList.Zeroless where

open import RandomAccessList.Zeroless.Core
open import RandomAccessList.Zeroless.Core.Properties
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf; split)
import BuildingBlock.BinaryLeafTree as BLT

open import Data.Fin using (Fin; fromℕ; fromℕ≤; reduce≥; toℕ)
import      Data.Fin as Fin
open import Data.Nat
open import Data.Nat.DivMod
-- open import Data.Nat.Properties.Simple
open import Data.Nat.Etc
open import Data.Product
open import Function
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; trans; sym; inspect)
open PropEq.≡-Reasoning

--------------------------------------------------------------------------------
-- Operations
--------------------------------------------------------------------------------

-- cons
consₙ : ∀ {n A} → BinaryLeafTree A n → 1-2-RAL A n → 1-2-RAL A n
consₙ a (         []) = a     1∷ []
consₙ a (x     1∷ xs) = a , x 2∷ xs
consₙ a (x , y 2∷ xs) = a     1∷ consₙ (Node x y) xs

cons : ∀ {A} → A → 1-2-RAL A 0 → 1-2-RAL A 0
cons a xs = consₙ (Leaf a) xs

-- head
headₙ : ∀ {n A} → (xs : 1-2-RAL A n) → ⟦ xs ⟧ ≢ 0 → BinaryLeafTree A n
headₙ {n} {A} []    p = contradiction (⟦[]⟧≡0 ([] {A} {n}) refl) p
headₙ (x     1∷ xs) p = x
headₙ (x , y 2∷ xs) p = x

head : ∀ {A} → (xs : 1-2-RAL A 0) → ⟦ xs ⟧ ≢ 0 → A
head xs p = BLT.head (headₙ xs p)

-- tail
tailₙ : ∀ {n A} → (xs : 1-2-RAL A n) → ⟦ xs ⟧ ≢ 0 → 1-2-RAL A n
tailₙ []            p = []
tailₙ (x 1∷ xs) p with ⟦ xs ⟧ ≟ 0
tailₙ (x 1∷ xs) p | yes q = []
tailₙ (x 1∷ xs) p | no ¬q =
    let y₀ = proj₁ (split (headₙ xs ¬q))
        y₁ = proj₂ (split (headₙ xs ¬q))
    in  y₀ , y₁ 2∷ tailₙ xs ¬q
tailₙ (x , y 2∷ xs) p = y 1∷ xs

tail : ∀ {A} → (xs : 1-2-RAL A 0) → ⟦ xs ⟧ ≢ 0 → 1-2-RAL A 0
tail = tailₙ

--------------------------------------------------------------------------------
-- Searching
--------------------------------------------------------------------------------

{-
data Occurrence : ℕ → Set where
    here : ∀ {n b} → ℕ → Fin (b * 2 ^ n) → Occurrence n
    there : ∀ {n} → Occurrence n

transportFin : ∀ {a b} → a ≡ b → Fin a → Fin b
transportFin refl i = i

search : ∀ {n A} → (xs : 1-2-RAL A n) → ℕ → Occurrence n
search []            i = there
search {n} (x     1∷ xs) i with (1 * 2 ^ n) ≤? i
search (x 1∷ xs) i | yes p = there
search {n} (x 1∷ xs) i | no ¬p = here 0 (fromℕ≤ (m≰n⇒n<m (1 * 2 ^ n) i ¬p))
search {n} (x , y 2∷ xs) i with (2 * 2 ^ n) ≤? i
search (x , y 2∷ xs) i | yes p = there
search {n} (x , y 2∷ xs) i | no ¬p with i divMod (2 ^ n)
search (x , y 2∷ xs) i | no ¬p | result zero remainder _ = here zero {!   !}
search (x , y 2∷ xs) i | no ¬p | result (suc quotient) remainder _ = {!   !}

elemAt : ∀ {n A} → (xs : 1-2-RAL A n) → Fin ⟦ xs ⟧ → A
elemAt {n} {A} []    i = contradiction (transportFin (⟦[]⟧≡0 ([] {A} {n}) refl) i) (λ ())
elemAt (x     1∷ xs) i = {!   !}
elemAt (x , y 2∷ xs) i = {!   !}

splitIndex1∷ : ∀ {n A} → (x : BinaryLeafTree A n) → (xs : 1-2-RAL A (suc n)) → ⟦ x 1∷ xs ⟧ ≡ (2 ^ n) + ⟦ xs ⟧
splitIndex1∷ {n} x xs =
    begin
        ⟦ x 1∷ xs ⟧
    ≡⟨ +-*-suc (2 ^ n) (2 * ⟦ xs ⟧ₙ) ⟩
        2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ cong (_+_ (2 ^ n)) (sym (*-assoc (2 ^ n) 2 ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + 2 ^ n * 2 * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → 2 ^ n + w * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        (2 ^ n) + ⟦ xs ⟧
    ∎

n+n≡2*n : (n : ℕ) → n + n ≡ 2 * n
n+n≡2*n n = cong (_+_ n) (sym (+-right-identity n))

splitIndex2∷ : ∀ {n A}
            → (x : BinaryLeafTree A n)
            → (y : BinaryLeafTree A n)
            → (xs : 1-2-RAL A (suc n)) → ⟦ x , y 2∷ xs ⟧ ≡ 2 * (2 ^ n) + ⟦ xs ⟧
splitIndex2∷ {n} x y xs =
    begin
        ⟦ x , y 2∷ xs ⟧
    ≡⟨ +-*-suc (2 ^ n) (suc (2 * ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + 2 ^ n * suc (2 * ⟦ xs ⟧ₙ)
    ≡⟨ cong (_+_ (2 ^ n)) (+-*-suc (2 ^ n) (2 * ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + (2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ))
    ≡⟨ sym (+-assoc (2 ^ n) (2 ^ n) (2 ^ n * (2 * ⟦ xs ⟧ₙ))) ⟩
        2 ^ n + 2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ cong (λ w → 2 ^ n + 2 ^ n + w) (sym (*-assoc (2 ^ n) 2 ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + 2 ^ n + 2 ^ n * 2 * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → 2 ^ n + 2 ^ n + w * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        2 ^ n + 2 ^ n + 2 * 2 ^ n * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → w + 2 * 2 ^ n * ⟦ xs ⟧ₙ) (n+n≡2*n (2 ^ n)) ⟩
        2 * 2 ^ n + ⟦ xs ⟧
    ∎
{-
elemAt : ∀ {n A} → (xs : 1-2-RAL A n) → Fin ⟦ xs ⟧ → A
elemAt     (         []) ()
elemAt {n} (x     1∷ xs) i with  (2 ^ n) ≤? toℕ i
elemAt {n} (x     1∷ xs) i | yes p rewrite splitIndex1∷ x xs = elemAt xs (reduce≥ i p)
elemAt     (x     1∷ xs) i | no ¬p = BLT.elemAt x (fromℕ≤ (BLT.¬a≤b⇒b<a ¬p))
elemAt {n} (x , y 2∷ xs) i with  (2 * (2 ^ n)) ≤? toℕ i
elemAt     (x , y 2∷ xs) i | yes p rewrite splitIndex2∷ x y xs = elemAt xs (reduce≥ i p)
elemAt {n} (x , y 2∷ xs) i | no ¬p with (2 ^ n) ≤? toℕ i
elemAt     (x , y 2∷ xs) i | no ¬p | yes q rewrite splitIndex2∷ x y xs = BLT.elemAt y {!   !} -- y
elemAt     (x , y 2∷ xs) i | no ¬p | no ¬q = BLT.elemAt x (fromℕ≤ (BLT.¬a≤b⇒b<a ¬q)) -- x
-}
-- reduce≥ : ∀ {m n} (i : Fin (m N+ n)) (i≥m : toℕ i N≥ m) → Fin n
-- i : 2 * 2 ^ n + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
-- m : 2 ^ n
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Nat
open import Prelude
open import Hazelnut-core

-- the obvious small step dynamics for complete expressions.
module Hazelnut-complete-dynamics where
  value : (e : ė) (p : ecomplete e) (t : τ̇) (q : ∅ ⊢ e => t) → Set
  value ._ _ _ (SAsc _) = ⊥
  value ._ _ _ (SVar x) with x
  ... | ()
  value ._ _ _ (SAp _ _) = ⊥
  value ._ _ .num SNum = ⊤
  value ._ _ .num (SPlus _ _) = ⊥
  value .<||> () .<||> SEHole
  value ._ () .<||> (SFHole _)
  value ._ _ .<||> (SApHole _ _) = ⊥

  -- "substitute e1 for x in e2". note that this only works on well typed
  -- terms because of barendrecht's convention. that's a theorem we need to
  -- prove. on non well typed terms, this is not correct.
  [_/_]_ : ė → Nat → ė → ė
  [ e1 / x ] (e2 ·: y)  = ([ e1 / x ] e2) ·: y
  [ e1 / x ] X y with natEQ x y
  ... | Inl p           = e1
  ... | Inr _           = X y
  [ e1 / x ] ·λ y e2    = ·λ y ([ e1 / x ] e2)
  [ e1 / x ] N n        = N n
  [ e1 / x ] (e2 ·+ e3) = ([ e1 / x ] e2) ·+ ([ e1 / x ] e3)
  [ e1 / x ] <||>       = <||>
  [ e1 / x ] <| e2 |>   = <| [ e1 / x ] e2 |>
  [ e1 / x ] (e2 ∘ e3)  = ([ e1 / x ] e2) ∘ ([ e1 / x ] e3)