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

module Examples.Traced where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)

open import Singleton
open import PiFrac
open import Trace
open import Reasoning

open import Examples.BooleanCircuits

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

-- Example in Sec. 4.3 from Abramsky's paper
-- http://www.cs.ox.ac.uk/files/341/calco05.pdf

q : {A1 A2 A3 A4 B1 B2 B3 B4 : 𝕌} →
  (f1 : A1 ⟷ B2) →
  (f2 : A2 ⟷ B4) →
  (f3 : A3 ⟷ B3) →
  (f4 : A4 ⟷ B1) →
  A1 ×ᵤ (A2 ×ᵤ (A3 ×ᵤ A4)) ⟷ B1 ×ᵤ (B2 ×ᵤ (B3 ×ᵤ B4))
q {A1} {A2} {A3} {A4} {B1} {B2} {B3} {B4} f1 f2 f3 f4 =
  (A1 ×ᵤ A2 ×ᵤ A3 ×ᵤ A4)     ⟷⟨ f1 ⊗ (f2 ⊗ (f3 ⊗ f4)) ⟩
  (B2 ×ᵤ B4 ×ᵤ B3 ×ᵤ B1)     ⟷⟨ assocl⋆ ⟩
  (B2 ×ᵤ B4) ×ᵤ (B3 ×ᵤ B1)   ⟷⟨ swap⋆ ⟩
  (B3 ×ᵤ B1) ×ᵤ (B2 ×ᵤ B4)   ⟷⟨ swap⋆ ⊗ id⟷ ⟩
  (B1 ×ᵤ B3) ×ᵤ (B2 ×ᵤ B4)   ⟷⟨ assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⟩
  B1 ×ᵤ ((B3 ×ᵤ B2) ×ᵤ B4)   ⟷⟨ id⟷ ⊗ ((swap⋆ ⊗ id⟷) ⊚ assocr⋆) ⟩
  B1 ×ᵤ (B2 ×ᵤ (B3 ×ᵤ B4)) □

q' : {A1 U2 U3 U4 B1 : 𝕌} →
  (f1 : A1 ⟷ U2) →
  (f2 : U2 ⟷ U4) →
  (f3 : U3 ⟷ U3) →
  (f4 : U4 ⟷ B1) → (v : ⟦ A1 ⟧) (u3 : ⟦ U3 ⟧)  → (u3-fix : eval f3 u3 ≡ u3) →
  let u2 = eval f1 v in
  let u4 = eval f2 u2 in
  ● A1 [ v ] ⟷ ● B1 [ proj₁ (eval (q f1 f2 f3 f4) (v , u2 , u3 , u4)) ]
q' f1 f2 f3 f4 v u3 u3fix =
  trace v (q f1 f2 f3 f4) (( u2 , ( u3 , u4 ) ), cong₂ _,_ refl (cong₂ _,_ u3fix refl))
  where
    u2 = eval f1 v
    u3′ = eval f3 u3
    u4 = eval f2 u2

-- The point is that q' acts in a very particular way:
q'-closed-form : {A1 U2 U3 U4 B1 : 𝕌} →
  (f1 : A1 ⟷ U2) →
  (f2 : U2 ⟷ U4) →
  (f3 : U3 ⟷ U3) →
  (f4 : U4 ⟷ B1) → (u3 : ⟦ U3 ⟧) (u3-fix : eval f3 u3 ≡ u3) → (v : ⟦ A1 ⟧) →
  proj₁ (eval (q' f1 f2 f3 f4 v u3 u3-fix) (v , refl)) ≡ eval (f1 ⊚ f2 ⊚ f4) v
q'-closed-form f1 f2 f3 f4 u3 u3fix v = refl

---------------------------------------------------------------------------------
-- I think the examples below are 'obsolete', in the sense that the one above
-- is more faithful to the original, and more general too.  Delete?
p : {A1 A2 A3 A4 : 𝕌} →
    (A1 ×ᵤ A2) ×ᵤ (A3 ×ᵤ A4) ⟷ (A2 ×ᵤ A4) ×ᵤ (A3 ×ᵤ A1)
p = (swap⋆ ⊗ swap⋆) ⊚
       assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⊚ (id⟷ ⊗ (swap⋆ ⊗ id⟷)) ⊚
       (id⟷ ⊗ assocr⋆) ⊚ assocl⋆ ⊚ (id⟷ ⊗ swap⋆)

p' : {A1 A2 A3 A4 : 𝕌} →
    ((A1 ×ᵤ A2) ×ᵤ A4) ×ᵤ A3 ⟷ ((A2 ×ᵤ A4) ×ᵤ A1) ×ᵤ A3
p' = assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚ p ⊚ (id⟷ ⊗ swap⋆) ⊚ assocl⋆

p2 : 𝔹 ×ᵤ (𝔹 ×ᵤ (𝔹 ×ᵤ 𝔹)) ⟷ 𝔹 ×ᵤ (𝔹 ×ᵤ (𝔹 ×ᵤ 𝔹))
p2 = assocl⋆ ⊚ (swap⋆ ⊗ swap⋆) ⊚
       assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⊚ (id⟷ ⊗ (swap⋆ ⊗ id⟷)) ⊚
       (id⟷ ⊗ assocr⋆) ⊚ assocl⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚ assocr⋆

p2' : (v : ⟦ 𝔹 ⟧) →
      ● 𝔹 [ v ] ⟷ ● 𝔹 [ proj₁ (proj₁ (eval p ((v , v) , (v , v)))) ]
p2' v = trace v p2 ((v , (v , v)) , refl)

---------------------------------------------------------------------------------
-- Examples inspired by compact closed categories and fractional numbers.

-- Intuition:
-- 1/A x B is a space transformer; takes A space and returns B space
-- denote space transformers as A ⊸ B

-- Best we can do:
-- we need Singletons, so |a ⊸ b| is 1 component of a function.

_⊸_ : {A : 𝕌} → (a : ⟦ A ⟧) → {B : 𝕌} → (b : ⟦ B ⟧) → 𝕌
_⊸_ {A} a {B} b = 𝟙/● A [ a ] ×ᵤ ● B [ b ]

id⊸ : {A : 𝕌} {a : ⟦ A ⟧} → (a ⊸ a) ⟷ 𝟙
id⊸ {A} {a} =
  (𝟙/● A [ a ] ×ᵤ ● A [ a ]) ⟷⟨ swap⋆ ⟩
  (● A [ a ] ×ᵤ 𝟙/● A [ a ]) ⟷⟨ ε a ⟩
  𝟙 □

comp⊸ : {A B C : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧} →
        (a ⊸ b) ×ᵤ (b ⊸ c) ⟷ (a ⊸ c)
comp⊸ {A} {B} {C} {a} {b} {c} =
  (𝟙/● A [ a ] ×ᵤ ● B [ b ]) ×ᵤ (𝟙/● B [ b ] ×ᵤ ● C [ c ]) ⟷⟨ assocr⋆ ⟩
  𝟙/● A [ a ] ×ᵤ (● B [ b ] ×ᵤ (𝟙/● B [ b ] ×ᵤ ● C [ c ])) ⟷⟨ id⟷ ⊗ assocl⋆ ⟩
  𝟙/● A [ a ] ×ᵤ (● B [ b ] ×ᵤ 𝟙/● B [ b ]) ×ᵤ ● C [ c ]   ⟷⟨ id⟷ ⊗ (ε b ⊗ id⟷) ⟩
  𝟙/● A [ a ] ×ᵤ (𝟙 ×ᵤ ● C [ c ])                          ⟷⟨ id⟷ ⊗ unite⋆l ⟩
  𝟙/● A [ a ] ×ᵤ ● C [ c ] □

app : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} → (a ⊸ b) ×ᵤ ● A [ a ] ⟷ ● B [ b ]
app {A} {B} {a} {b} =
  (𝟙/● A [ a ] ×ᵤ ● B [ b ]) ×ᵤ ● A [ a ] ⟷⟨ swap⋆ ⊗ id⟷ ⟩
  (● B [ b ] ×ᵤ 𝟙/● A [ a ]) ×ᵤ ● A [ a ] ⟷⟨ assocr⋆ ⊚ (id⟷ ⊗ (swap⋆ ⊚ ε a)) ⟩
  ● B [ b ] ×ᵤ 𝟙                          ⟷⟨ unite⋆r ⟩
  ● B [ b ] □

-- B/A × D/C ⟷ B × D / A × C
dist×/ : {A B C D : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧} {d : ⟦ D ⟧}
       → (a ⊸ b) ×ᵤ (c ⊸ d) ⟷ ((a , c) ⊸ (b , d))
dist×/ {A} {B} {C} {D} {a} {b} {c} {d} =
  (𝟙/● A [ a ] ×ᵤ ● B [ b ]) ×ᵤ (𝟙/● C [ c ] ×ᵤ ● D [ d ]) ⟷⟨ assocr⋆ ⊚ (id⟷ ⊗ assocl⋆) ⟩
  (𝟙/● A [ a ] ×ᵤ (● B [ b ] ×ᵤ 𝟙/● C [ c ]) ×ᵤ ● D [ d ]) ⟷⟨ id⟷ ⊗ (swap⋆ ⊗ id⟷) ⟩
  (𝟙/● A [ a ] ×ᵤ (𝟙/● C [ c ] ×ᵤ ● B [ b ]) ×ᵤ ● D [ d ]) ⟷⟨ (id⟷ ⊗ assocr⋆) ⊚ assocl⋆ ⟩
  (𝟙/● A [ a ] ×ᵤ 𝟙/● C [ c ]) ×ᵤ (● B [ b ] ×ᵤ ● D [ d ]) ⟷⟨ fracr ⊗ tensorr ⟩
  (𝟙/● A ×ᵤ C [ a , c ]) ×ᵤ (● B ×ᵤ D [ b , d ]) □

-- 1/A x 1/B <-> 1 / (A x B)
rev× : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧}
     → (a ⊸ tt) ×ᵤ (b ⊸ tt) ⟷ ((a , b) ⊸ tt)
rev× {A} {B} {a} {b} =
  (𝟙/● A [ a ] ×ᵤ ● 𝟙 [ tt ]) ×ᵤ (𝟙/● B [ b ] ×ᵤ ● 𝟙 [ tt ]) ⟷⟨ dist×/ ⟩
  (𝟙/● A ×ᵤ B [ a , b ] ×ᵤ ● 𝟙 ×ᵤ 𝟙 [ tt , tt ]) ⟷⟨ id⟷ ⊗ lift unite⋆l ⟩
  (𝟙/● A ×ᵤ B [ a , b ] ×ᵤ ● 𝟙 [ tt ]) □

{--
trivial : ● 𝟙 [ tt ] ⟷ 𝟙
trivial = {!!}
--}

-- (A <-> B) -> (1/A <-> 1/B)
--rev : {A B : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧}
--     → ● A [ a ] ⟷ ● B [ b ] → (b ⊸ tt) ⟷ (a ⊸ tt)
--  (𝟙/● A [ a ] ×ᵤ ● 𝟙 [ tt ]) ⟷⟨ {!!} ⟩
--  (𝟙/● B [ b ] ×ᵤ ● 𝟙 [ tt ]) □

rev : {A B : 𝕌} {a : ⟦ A ⟧}
     → (f : A ⟷ B) → (𝟙/● B [ eval f a ] ⟷ 𝟙/● A [ a ])
rev {A} {B} {a} f = dual f a

-- A <-> 1 / (1/A)
revrev : {A : 𝕌} {a : ⟦ A ⟧} {a⋆ : ⟦ 𝟙/● A [ a ] ⟧} →
         ● A [ a ] ⟷ 𝟙/● (𝟙/● A [ a ]) [ a⋆ ]
revrev {A} {a} {a⋆} =
  ● A [ a ] ⟷⟨ uniti⋆r ⟩
  ● A [ a ] ×ᵤ 𝟙 ⟷⟨ {!id⟷ ⊗ η a⋆!} ⟩
  ● A [ a ] ×ᵤ (𝟙/● A [ a ] ×ᵤ 𝟙/● (𝟙/● A [ a ]) [ a⋆ ]) ⟷⟨ {!!} ⟩
  𝟙/● (𝟙/● A [ a ]) [ a⋆ ] □

-- this is strange
-- A/C + B/C <-> (A + B) / C
-- factor+/l : {A B C : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧}
--           → (c ⊸ a) +ᵤ (c ⊸ b) ⟷ (_⊸_ {C} c {A +ᵤ B} (inj₁ a))
-- factor+/l {A} {B} {C} {a} {b} {c} =
--   (𝟙/● C [ c ] ×ᵤ ● A [ a ] +ᵤ 𝟙/● C [ c ] ×ᵤ ● B [ b ]) ⟷⟨ factorl ⟩
--   (𝟙/● C [ c ] ×ᵤ (● A [ a ] +ᵤ ● B [ b ])) ⟷⟨ id⟷ ⊗ {!!} ⟩
--   (𝟙/● C [ c ] ×ᵤ ● A +ᵤ B [ inj₁ a ]) □

-- same issue here with the +
-- A/B + C/D <-> (A x D + B x C) / (B x D)

-- SAT solver Sec. 5 from https://www.cs.indiana.edu/~sabry/papers/rational.pdf

-- can we do this?
-- curry⊸ : {A B C : 𝕌} {a : ⟦ A ⟧} {b : ⟦ B ⟧} {c : ⟦ C ⟧}
--        → (● A [ a ] ×ᵤ (b ⊸ c)) ⟷ (a ⊸ {!!}) -- what do we put here?
-- curry⊸ {A} {B} {C} {a} {b} {c} = {!!}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-

This file proves the higher groupoid structure of types
for homogeneous and heterogeneous paths

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.GroupoidLaws where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level
    A : Type ℓ
    x y z w : A

_⁻¹ : (x ≡ y) → (y ≡ x)
x≡y ⁻¹ = sym x≡y

infix 40 _⁻¹

-- homogeneous groupoid laws

symInvo : (p : x ≡ y) → p ≡ p ⁻¹ ⁻¹
symInvo p = refl

rUnit : (p : x ≡ y) → p ≡ p ∙ refl
rUnit p j i = compPath-filler p refl j i

-- The filler of left unit: lUnit-filler p =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (p (~ j ∨ i)))
-- (refl i) (λ j → compPath-filler refl p i j)) (λ k i → (p (~ k ∧ i ))) (lUnit p)

lUnit-filler : {x y : A} (p : x ≡ y) → I → I → I → A
lUnit-filler {x = x} p j k i =
  hfill (λ j → λ { (i = i0) → x
                  ; (i = i1) → p (~ k ∨ j )
                  ; (k = i0) → p i
               -- ; (k = i1) → compPath-filler refl p j i
                  }) (inS (p (~ k ∧ i ))) j

lUnit : (p : x ≡ y) → p ≡ refl ∙ p
lUnit p j i = lUnit-filler p i1 j i

symRefl : refl {x = x} ≡ refl ⁻¹
symRefl i = refl

compPathRefl : refl {x = x} ≡ refl ∙ refl
compPathRefl = rUnit refl

-- The filler of right cancellation: rCancel-filler p =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (p (~ j ∧ ~ i)))
-- (λ j → compPath-filler p (p ⁻¹) i j) (refl i)) (λ j i → (p (i ∧ ~ j))) (rCancel p)

rCancel-filler : ∀ {x y : A} (p : x ≡ y) → (k j i : I) → A
rCancel-filler {x = x} p k j i =
  hfill (λ k → λ { (i = i0) → x
                  ; (i = i1) → p (~ k ∧ ~ j)
               -- ; (j = i0) → compPath-filler p (p ⁻¹) k i
                  ; (j = i1) → x
                  }) (inS (p (i ∧ ~ j))) k

rCancel : (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
rCancel {x = x} p j i = rCancel-filler p i1 j i

lCancel : (p : x ≡ y) → p ⁻¹ ∙ p ≡ refl
lCancel p = rCancel (p ⁻¹)

-- The filler of the three-out-of-four identification: 3outof4-filler α p β =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) (α i i0) (α i i1))
-- (λ j → α i j) (λ j → β i j)) (λ j i → α i0 i) (3outof4 α p β)

3outof4-filler : (α : I → I → A) → (p : α i1 i0 ≡ α i1 i1) →
  (β : PathP (λ j → Path A (α j i0) (α j i1)) (λ i → α i0 i) p) → I → I → I → A
3outof4-filler α p β k j i =
  hfill (λ k → λ { (i = i0) → α k i0
                  ; (i = i1) → α k i1
                  ; (j = i0) → α k i
                  ; (j = i1) → β k i
                  }) (inS (α i0 i)) k

3outof4 : (α : I → I → A) → (p : α i1 i0 ≡ α i1 i1) →
  (β : PathP (λ j → Path A (α j i0) (α j i1)) (λ i → α i0 i) p) → (λ i → α i1 i) ≡ p
3outof4 α p β j i = 3outof4-filler α p β i1 j i

-- The filler of the pre-associative square: preassoc p q r =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (compPath-filler q r i j))
-- (refl i) (λ j → compPath-filler (p ∙ q) r i j)) (λ j i → compPath-filler p q j i) (preassoc p q r)

preassoc-filler : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → I → I → I → A
preassoc-filler {x = x} p q r k j i =
  hfill (λ k → λ { (i = i0) → x
                  ; (i = i1) → compPath-filler q r k j
                  ; (j = i0) → p i
               -- ; (j = i1) → compPath-filler (p ∙ q) r k i
                  }) (inS (compPath-filler p q j i)) k

preassoc : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
  PathP (λ j → Path A x ((q ∙ r) j)) p ((p ∙ q) ∙ r)
preassoc {x = x} p q r j i = preassoc-filler p q r i1 j i

assoc : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
  p ∙ q ∙ r ≡ (p ∙ q) ∙ r
assoc p q r = 3outof4 (compPath-filler p (q ∙ r)) ((p ∙ q) ∙ r) (preassoc p q r)

-- heterogeneous groupoid laws

symInvoP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
     PathP (λ j → PathP (λ i → symInvo (λ i → A i) j i) x y) p (symP (symP p))
symInvoP p = refl

rUnitP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
  PathP (λ j → PathP (λ i → rUnit (λ i → A i) j i) x y) p (compPathP p refl)
rUnitP p j i = compPathP-filler p refl i j

lUnitP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
  PathP (λ j → PathP (λ i → lUnit (λ i → A i) j i) x y) p (compPathP refl p)
lUnitP {A = A} {x = x} p k i =
  comp (λ j → lUnit-filler (λ i → A i) j k i)
       (λ j → λ { (i = i0) → x
                ; (i = i1) → p (~ k ∨ j )
                ; (k = i0) → p i
                }) (p (~ k ∧ i ))

rCancelP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
   PathP (λ j → PathP (λ i → rCancel (λ i → A i) j i) x x) (compPathP p (symP p)) refl
rCancelP {A = A} {x = x} p j i =
  comp (λ k → rCancel-filler (λ i → A i) k j i)
       (λ k → λ { (i = i0) → x
                ; (i = i1) → p (~ k ∧ ~ j)
                ; (j = i1) → x
                }) (p (i ∧ ~ j))

lCancelP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
   PathP (λ j → PathP (λ i → lCancel (λ i → A i) j i) y y) (compPathP (symP p) p) refl
lCancelP p = rCancelP (symP p)

3outof4P : {A : I → I → Type ℓ} {P : (A i0 i1) ≡ (A i1 i1)}
  {B : PathP (λ j → Path (Type ℓ) (A i0 j) (A i1 j)) (λ i → A i i0) P}
  (α : ∀ (i j : I) → A j i)
  (p : PathP (λ i → P i) (α i1 i0) (α i1 i1)) →
  (β : PathP (λ j → PathP (λ i → B j i) (α j i0) (α j i1)) (λ i → α i0 i) p) →
  PathP (λ j → PathP (λ i → 3outof4 (λ j i → A i j) P B j i) (α i1 i0) (α i1 i1)) (λ i → α i1 i) p
3outof4P {A = A} {P} {B} α p β j i =
  comp (λ k → 3outof4-filler (λ j i → A i j) P B k j i)
       (λ k → λ { (i = i0) → α k i0
                ; (i = i1) → α k i1
                ; (j = i0) → α k i
                ; (j = i1) → β k i
                }) (α i0 i)

preassocP : {A : I → Type ℓ} {x : A i0} {y : A i1} {B_i1 : Type ℓ} {B : (A i1) ≡ B_i1} {z : B i1}
  {C_i1 : Type ℓ} {C : (B i1) ≡ C_i1} {w : C i1} (p : PathP A x y) (q : PathP (λ i → B i) y z) (r : PathP (λ i → C i) z w) →
  PathP (λ j → PathP (λ i → preassoc (λ i → A i) B C j i) x ((compPathP q r) j)) p (compPathP (compPathP p q) r)
preassocP {A = A} {x = x} {B = B} {C = C} p q r j i =
  comp (λ k → preassoc-filler (λ i → A i) B C k j i)
       (λ k → λ { (i = i0) → x
                ; (i = i1) → compPathP-filler q r j k
                ; (j = i0) → p i
             -- ; (j = i1) → compPathP-filler (compPathP p q) r i k
                }) (compPathP-filler p q i j)

assocP : {A : I → Type ℓ} {x : A i0} {y : A i1} {B_i1 : Type ℓ} {B : (A i1) ≡ B_i1} {z : B i1}
  {C_i1 : Type ℓ} {C : (B i1) ≡ C_i1} {w : C i1} (p : PathP A x y) (q : PathP (λ i → B i) y z) (r : PathP (λ i → C i) z w) →
  PathP (λ j → PathP (λ i → assoc (λ i → A i) B C j i) x w) (compPathP p (compPathP q r)) (compPathP (compPathP p q) r)
assocP p q r =
  3outof4P (λ i j → compPathP-filler p (compPathP q r) j i) (compPathP (compPathP p q) r) (preassocP p q r)

-- Loic's code below

-- simultaneaous composition on both sides of a path

doubleCompPath-filler : {ℓ : Level} {A : Type ℓ} {w x y z : A} → w ≡ x → x ≡ y → y ≡ z →
                        I → I → A
doubleCompPath-filler p q r i =
  hfill (λ t → λ { (i = i0) → p (~ t)
                 ; (i = i1) → r t })
        (inS (q i))

doubleCompPath : {ℓ : Level} {A : Type ℓ} {w x y z : A} → w ≡ x → x ≡ y → y ≡ z → w ≡ z
doubleCompPath p q r i = doubleCompPath-filler p q r i i1

_∙∙_∙∙_ : {ℓ : Level} {A : Type ℓ} {w x y z : A} → w ≡ x → x ≡ y → y ≡ z → w ≡ z
p ∙∙ q ∙∙ r = doubleCompPath p q r

-- some exchange law for doubleCompPath and refl

rhombus-filler : {ℓ : Level} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → I → I → A
rhombus-filler p q i j =
  hcomp (λ t → λ { (i = i0) → p (~ t ∨ j)
                 ; (i = i1) → q (t ∧ j)
                 ; (j = i0) → p (~ t ∨ i)
                 ; (j = i1) → q (t ∧ i) })
        (p i1)

leftright : {ℓ : Level} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) →
            (refl ∙∙ p ∙∙ q) ≡ (p ∙∙ q ∙∙ refl)
leftright p q i j =
  hcomp (λ t → λ { (j = i0) → p (i ∧ (~ t))
                 ; (j = i1) → q (t ∨ i) })
        (rhombus-filler p q i j)

-- equating doubleCompPath and a succession of two compPath

split-leftright : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
                  (p ∙∙ q ∙∙ r) ≡ (refl ∙∙ (p ∙∙ q ∙∙ refl) ∙∙ r)
split-leftright p q r i j =
  hcomp (λ t → λ { (j = i0) → p (~ i ∧ ~ t)
                 ; (j = i1) → r t })
        (doubleCompPath-filler p q refl j i)

split-leftright' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
                  (p ∙∙ q ∙∙ r) ≡ (p ∙∙ (refl ∙∙ q ∙∙ r) ∙∙ refl)
split-leftright' p q r i j =
  hcomp (λ t → λ { (j = i0) → p (~ t)
                 ; (j = i1) → r (i ∨ t) })
        (doubleCompPath-filler refl q r j i)

doubleCompPath-elim : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y)
                      (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ (p ∙ q) ∙ r
doubleCompPath-elim p q r = (split-leftright p q r) ∙ (λ i → (leftright p q (~ i)) ∙ r)

doubleCompPath-elim' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y)
                       (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ p ∙ (q ∙ r)
doubleCompPath-elim' p q r = (split-leftright' p q r) ∙ (sym (leftright p (q ∙ r)))

-- deducing associativity for compPath

-- assoc : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
--                 (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
-- assoc p q r = (sym (doubleCompPath-elim p q r)) ∙ (doubleCompPath-elim' p q r)

hcomp-unique : ∀ {ℓ} {A : Set ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
               (h2 : ∀ i → A [ (φ ∨ ~ i) ↦ (\ { (φ = i1) → u i 1=1; (i = i0) → outS u0}) ])
               → (hcomp u (outS u0) ≡ outS (h2 i1)) [ φ ↦ (\ { (φ = i1) → (\ i → u i1 1=1)}) ]
hcomp-unique {φ = φ} u u0 h2 = inS (\ i → hcomp (\ k → \ { (φ = i1) → u k 1=1
                                                            ; (i = i1) → outS (h2 k) })
                                                   (outS u0))

lid-unique : ∀ {ℓ} {A : Set ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
               (h1 h2 : ∀ i → A [ (φ ∨ ~ i) ↦ (\ { (φ = i1) → u i 1=1; (i = i0) → outS u0}) ])
               → (outS (h1 i1) ≡ outS (h2 i1)) [ φ ↦ (\ { (φ = i1) → (\ i → u i1 1=1)}) ]
lid-unique {φ = φ} u u0 h1 h2 = inS (\ i → hcomp (\ k → \ { (φ = i1) → u k 1=1
                                                            ; (i = i0) → outS (h1 k)
                                                            ; (i = i1) → outS (h2 k) })
                                                   (outS u0))

transp-hcomp : ∀ {ℓ} (φ : I) {A' : Set ℓ}
                     (A : (i : I) → Set ℓ [ φ ↦ (λ _ → A') ]) (let B = \ (i : I) → outS (A i))
                 → ∀ {ψ} (u : I → Partial ψ (B i0)) → (u0 : B i0 [ ψ ↦ u i0 ]) →
                 (transp B φ (hcomp u (outS u0)) ≡ hcomp (\ i o → transp B φ (u i o)) (transp B φ (outS u0)))
                   [ ψ ↦ (\ { (ψ = i1) → (\ i → transp B φ (u i1 1=1))}) ]
transp-hcomp φ A u u0 = inS (sym (outS (hcomp-unique
               ((\ i o → transp B φ (u i o))) (inS (transp B φ (outS u0)))
                 \ i → inS (transp B φ (hfill u u0 i)))))
  where
    B = \ (i : I) → outS (A i)

hcomp-cong : ∀ {ℓ} {A : Set ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
                                    (u' : I → Partial φ A) → (u0' : A [ φ ↦ u' i0 ]) →

             (ueq : ∀ i → PartialP φ (\ o → u i o ≡ u' i o)) → (outS u0 ≡ outS u0') [ φ ↦ (\ { (φ = i1) → ueq i0 1=1}) ]
             → (hcomp u (outS u0) ≡ hcomp u' (outS u0')) [ φ ↦ (\ { (φ = i1) → ueq i1 1=1 }) ]
hcomp-cong u u0 u' u0' ueq 0eq = inS (\ j → hcomp (\ i o → ueq i o j) (outS 0eq j))

squeezeSq≡
  : ∀{w x y z : A}
  → (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z)
  → (q ≡ p ∙∙ r ∙∙ sym s) ≡ (Square p q r s)
squeezeSq≡ p q r s k
  = Square
      (λ j → p (j ∧ k))
      q
      (λ j → doubleCompPath-filler p r (sym s) j (~ k))
      (λ j → s (j ∧ k))

ext: agda

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool

-- A function that requires call-by-need
f : Nat → Nat → Nat
f a 0       = a
f a (suc b) = f (a + a) b

even : Nat → Bool
even n = mod-helper 0 1 n 1 == 0

data ⊥ : Set where
record ⊤ : Set where

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

-- Previously we reverted to slow reduce in when positivity checking.
f-even : IsTrue (even (f 1 64))
f-even = _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2 where

open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.GroupPath

open import Cubical.HITs.Sn
open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.Pushout
open import Cubical.HITs.Truncation renaming
  (rec to trRec ; elim to trElim ; elim2 to trElim2 ; map to trMap)
open import Cubical.HITs.S2

≡→Pushout⋁↪fold⋁≡ : ∀ {ℓ} {A B : Pointed ℓ}
  → (A ≡ B) → Pushout⋁↪fold⋁∙ A ≡ Pushout⋁↪fold⋁∙ B
≡→Pushout⋁↪fold⋁≡ = cong Pushout⋁↪fold⋁∙

private
  ∙≃→π≅ : ∀ {ℓ} {A B : Pointed ℓ} (n : ℕ)
        → (e : typ A ≃ typ B)
        → fst e (pt A) ≡ pt B
        → GroupEquiv (πGr n A) (πGr n B)
  ∙≃→π≅ {A = A} {B = B} n e =
    EquivJ (λ A e → (a : A) → fst e a ≡ pt B
                  → GroupEquiv (πGr n (A , a)) (πGr n B))
      (λ b p → J (λ b p → GroupEquiv (πGr n (typ B , b)) (πGr n B))
        idGroupEquiv (sym p))
      e (pt A)

{- π₄(S³) ≅ π₃((S² × S²) ⊔ᴬ S²)
  where A = S² ∨ S² -}
π₄S³≅π₃PushS² :
  GroupIso (πGr 3 (S₊∙ 3))
           (πGr 2 (Pushout⋁↪fold⋁∙ (S₊∙ 2)))
π₄S³≅π₃PushS² =
  compGroupIso
    (GroupEquiv→GroupIso
     (∙≃→π≅ 3 (compEquiv (isoToEquiv (invIso IsoS³S3)) S³≃SuspS²) refl))
    (compGroupIso
     (invGroupIso (GrIso-πΩ-π 2))
     (compGroupIso
       (πTruncGroupIso 2)
       (compGroupIso
         (GroupEquiv→GroupIso
          (∙≃→π≅ {B = _ , ∣ inl (base , base) ∣ₕ}
           2 (isoToEquiv IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅) encode∙))
         (compGroupIso
         (invGroupIso (πTruncGroupIso 2))
          (GroupEquiv→GroupIso (invEq (GroupPath _ _)
           (cong (πGr 2)
            (cong Pushout⋁↪fold⋁∙ (ua∙ S²≃SuspS¹ refl)))))))))
  where
  encode∙ : encode ∣ north ∣ refl ≡ ∣ inl (base , base) ∣
  encode∙ = transportRefl _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- 2012-03-08 Andreas
module NoTerminationCheck where

postulate A : Set

-- Skipping a single definition: before type signature

{-# NO_TERMINATION_CHECK #-}
a : A
a = a

-- Skipping a single definition: before first clause

b : A
{-# NO_TERMINATION_CHECK #-}
b = b

-- Skipping an old-style mutual block (placed before)

{-# NO_TERMINATION_CHECK #-}
mutual
  c : A
  c = d

  d : A
  d = c

-- Skipping an old-style mutual block (placed within)

mutual
  {-# NO_TERMINATION_CHECK #-}
  c1 : A
  c1 = d1

  d1 : A
  d1 = c1

mutual
  c2 : A
  {-# NO_TERMINATION_CHECK #-}
  c2 = d2

  d2 : A
  d2 = c2

mutual
  c3 : A
  c3 = d3

  {-# NO_TERMINATION_CHECK #-}
  d3 : A
  d3 = c3

-- Skipping a new-style mutual block

{-# NO_TERMINATION_CHECK #-}
e : A
f : A

e = f
f = e

-- Skipping a new-style mutual block, variant 2

g : A
{-# NO_TERMINATION_CHECK #-}
h : A

g = h
h = g

-- Skipping a new-style mutual block, variant 4

i : A
j : A

i = j
{-# NO_TERMINATION_CHECK #-}
j = i

private
  {-# NO_TERMINATION_CHECK #-}
  k : A
  k = k

abstract
  {-# NO_TERMINATION_CHECK #-}
  l : A
  l = l

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Cubical.HITs.Ints.HAEquivInt.Base public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module plfa-exercises.weird where

open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Bool.Base using (Bool; true; false; _∧_; _∨_; not)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; subst)

data ℕ∨Bool : Set where
  N B : ℕ∨Bool

-- Idea taken from paper: Fractional Types by Chao-Hong Chen et al.
⟦_⟧ : ℕ∨Bool → Set
⟦ N ⟧ = ℕ
⟦ B ⟧ = Bool

manyinputs : {a : ℕ∨Bool} → ⟦ a ⟧ → ⟦ a ⟧
manyinputs {N} n = suc n
manyinputs {B} b = not b

_ : manyinputs 6 ≡ 7
_ = refl

_ : manyinputs true ≡ false  -- WOW!!
_ = refl

open import Relation.Nullary using (¬_)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
-- Actually this should use "isomorphisms" not mere 'iff' between propositions.
-- https://agda.github.io/agda-stdlib/v1.1/Function.Inverse.html#2229
open import plfa.part1.Isomorphism using (_⇔_)

lemma₁ : ¬ ⊤ → ⊥
lemma₁ ¬⊤ = ¬⊤ tt

lemma₂ : ⊥ → ¬ ⊤
lemma₂ ()

-- I can easily prove this!! Which is not the same as ¬ ⊤ same as ⊥,
-- but ¬ ⊤ iff ⊥, where ⊤ and ⊥ are predicates
prf₀ : (¬ ⊤) ⇔ ⊥
prf₀ = record {
    to = lemma₁
  ; from = lemma₂
  }

-- But how to prove the following?
--prf : ¬ ⊤ ≡ ⊥
--prf = ?  -- seems to require extensionality and iso-is-≡, or cubical, see https://stackoverflow.com/a/58912530

open import Level using (0ℓ)
open import Agda.Primitive using (lsuc)
open import Relation.Binary.Definitions using (Substitutive; _Respects_; _⟶_Respects_)

prf₂ : ¬ (⊤ ≡ ⊥)  -- same as:  ⊤ ≢ ⊥
prf₂ ⊤≡⊥ = subst (λ x → x) ⊤≡⊥ tt
-- We don't need to give the implicit parameters but doing so lets us look
-- inside of the definitions and how they get reduced to other terms
--prf₂ ⊤≡⊥ = subst {A = Set} {ℓ = 0ℓ} (λ x → x) ⊤≡⊥ tt

-- `subst` has type: {a : Level} {A : Set a} {ℓ : Level} → Substitutive _≡_ ℓ
-- `subst {A = Set}` has type: {ℓ : Level} → Substitutive _≡_ ℓ
-- `subst {A = Set} {ℓ = 0ℓ}` has type: Substitutive _≡_ 0ℓ
--    actually it has type: Substitutive {A = Set} _≡_ 0ℓ
-- `Substitutive {A = Set} _≡_ 0ℓ` which reduces to  (P : Set → Set) {x y : Set} → x ≡ y → P x → P y
-- which means that the type of
--  `subst {A = Set} {ℓ = 0ℓ}`
-- is
--  (P : Set → Set) {x y : Set} → x ≡ y → P x → P y
-- thus, the type of
--  `subst {A = Set} {ℓ = 0ℓ} (λ x → x)`   (*)
-- is
--   {x y : Set} → x ≡ y → P x → P y
-- Note: careful, Agda tells us that the type of (*) is:
--   (λ x → x) Respects _≡_
-- but it is actually:
--   _Respects_ {A = Set} (λ x → x) _≡_
--
-- From reading the code:
--   _Respects_ {A = Set} (λ x → x) _≡_   (**)
-- reduces first to:
--   _⟶_Respects_ {A = Set} (λ x → x) (λ x → x) _≡_
--
-- There is even more. (**) actually has some implicit parameters, here they are
--   _Respects_ {A = Set} {ℓ₁ = 0ℓ} {ℓ₂ = lsuc 0ℓ} (λ x → x) _≡_
--
-- LESSON LEARNT: Implicit arguments are cool because you don't need to give
-- them, Agda can generally infer them from context which makes code to look
-- prettier but excesively harder to read
--
-- Other stuff:
-- `Substitutive {A = Set} _≡_ 0ℓ` reduces to  (P : Set → Set) {x y : Set} → x ≡ y → P x → P y
-- `Substitutive {A = Set} _≡_ (lsuc 0ℓ)` reduces to  (P : Set → Set₁) {x y : Set} → x ≡ y → P x → P y


text:
open import Relation.Binary
open import Level

module Experiments.Infer {c ℓ₁ ℓ₂}(PO : Preorder c ℓ₁ ℓ₂) where

open Preorder PO renaming (_∼_ to _⊑_)

record IsIncluded (W W' : Carrier) : Set ℓ₂ where
  field
    is-included : W ⊑ W'

record IsIncludedOnce (W W' : Carrier) : Set ℓ₂ where
  field
    is-included-once : W ⊑ W'

instance
  is-included-refl : ∀ {W} → IsIncluded W W
  is-included-refl = record { is-included = refl }

  is-included-step : ∀ {W W' W''} ⦃ p : IsIncludedOnce W W' ⦄ ⦃ q : IsIncluded W' W'' ⦄ → IsIncluded W W''
  is-included-step
    {{p = record { is-included-once = p }}}
    {{record { is-included = q }}} = record { is-included = trans p q }

-- typeclass for world-indexed things that support weakening
record Weakenable {i}(I : Carrier → Set i) : Set (i ⊔ ℓ₂ ⊔ c) where
  field
    weaken : ∀ {W W'} → W ⊑ W' → I W → I W'

  wk     : ∀ {W W'} → I W → ⦃ p : IsIncluded W W' ⦄ → I W'
  wk x ⦃ record { is-included = p } ⦄ = weaken p x

ISet = Carrier → Set

module Monad
  (M    : ISet → ISet)
  (ret  : ∀ {P : ISet}{c} → P c → M P c)
  (bind : ∀ {P Q : ISet}{c} → (∀ {c'} ⦃ sub : IsIncludedOnce c c' ⦄ → P c' → M Q c') → M P c → M Q c)
  (V    : ISet)
  (wV   : Weakenable V)
  (get  : ∀ {c} → M V c)
  (App  : ∀ {c} → V c → V c → V c)
  where

  instance
    weakenable-val = wV

  open Weakenable ⦃...⦄

  {- uncomment to see the compiler error -}
  -- test : ∀ {c} → M V c
  -- test = bind (λ x → bind (λ y → ret (App (wk x) (wk y))) get) get


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

module Data.List.Indexing where

open import Data.List.Base
open import Data.Fin
open import Prelude

infixl 6 _!_
_!_ : (xs : List A) → Fin (length xs) → A
(x ∷ xs) ! f0 = x
(x ∷ xs) ! fs i = xs ! i

tabulate : ∀ n → (Fin n → A) → List A
tabulate zero f = []
tabulate (suc n) f = f f0 ∷ tabulate n (f ∘ fs)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the extensional sublist relation over setoid equality.
------------------------------------------------------------------------

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

open import Relation.Binary hiding (Decidable)

module Data.List.Relation.Binary.Subset.Setoid.Properties where

open import Data.Bool.Base using (Bool; true; false)
open import Data.List.Base
open import Data.List.Relation.Unary.Any using (here; there)
import Data.List.Membership.Setoid as Membership
open import Data.List.Membership.Setoid.Properties
import Data.List.Relation.Binary.Subset.Setoid as Sublist
import Data.List.Relation.Binary.Equality.Setoid as Equality
open import Relation.Nullary using (¬_; does)
open import Relation.Unary using (Pred; Decidable)
import Relation.Binary.Reasoning.Preorder as PreorderReasoning

open Setoid using (Carrier)

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

module _ {a ℓ} (S : Setoid a ℓ) where

  open Equality S
  open Sublist S
  open Membership S

  ⊆-reflexive : _≋_ ⇒ _⊆_
  ⊆-reflexive xs≋ys = ∈-resp-≋ S xs≋ys

  ⊆-refl : Reflexive _⊆_
  ⊆-refl x∈xs = x∈xs

  ⊆-trans : Transitive _⊆_
  ⊆-trans xs⊆ys ys⊆zs x∈xs = ys⊆zs (xs⊆ys x∈xs)

  ⊆-isPreorder : IsPreorder _≋_ _⊆_
  ⊆-isPreorder = record
    { isEquivalence = ≋-isEquivalence
    ; reflexive     = ⊆-reflexive
    ; trans         = ⊆-trans
    }

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = record
    { isPreorder = ⊆-isPreorder
    }

  -- Reasoning over subsets
  module ⊆-Reasoning where
    private
      module Base = PreorderReasoning ⊆-preorder

    open Base public
      hiding (step-∼; step-≈; step-≈˘)
      renaming (_≈⟨⟩_ to _≋⟨⟩_)

    infix 2 step-⊆ step-≋ step-≋˘
    infix 1 step-∈

    step-∈ : ∀ x {xs ys} → xs IsRelatedTo ys → x ∈ xs → x ∈ ys
    step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs

    step-⊆  = Base.step-∼
    step-≋  = Base.step-≈
    step-≋˘ = Base.step-≈˘

    syntax step-∈  x  xs⊆ys x∈xs  = x  ∈⟨  x∈xs  ⟩ xs⊆ys
    syntax step-⊆  xs ys⊆zs xs⊆ys = xs ⊆⟨  xs⊆ys ⟩ ys⊆zs
    syntax step-≋  xs ys⊆zs xs≋ys = xs ≋⟨  xs≋ys ⟩ ys⊆zs
    syntax step-≋˘ xs ys⊆zs xs≋ys = xs ≋˘⟨ xs≋ys ⟩ ys⊆zs

------------------------------------------------------------------------
-- filter

module _ {a p ℓ} (S : Setoid a ℓ)
         {P : Pred (Carrier S) p} (P? : Decidable P) where

  open Setoid S renaming (Carrier to A)
  open Sublist S

  filter⁺ : ∀ xs → filter P? xs ⊆ xs
  filter⁺ (x ∷ xs) y∈f[x∷xs] with does (P? x)
  ... | false = there (filter⁺ xs y∈f[x∷xs])
  ... | true  with y∈f[x∷xs]
  ...   | here  y≈x     = here y≈x
  ...   | there y∈f[xs] = there (filter⁺ xs y∈f[xs])


text:
postulate Ty : Set

data Cxt : Set where
  ε : Cxt
  sg : (A : Ty) → Cxt
  _∙_ : (Γ₁ Γ₂ : Cxt) → Cxt

variable Γ Γ₁ Γ₂ Δ : Cxt

postulate Ren : (Δ Γ : Cxt) → Set

<_,_> : (f₁ : Ren Δ Γ₁) (f₂ : Ren Δ Γ₂) → Ren Δ (Γ₁ ∙ Γ₂)
<_,_> = {!!}

<_,_>₁ : (f₁ : Ren Δ Γ₁) (f₂ : Ren Δ Γ₂) → Cxt → Ren Δ (Γ₁ ∙ Γ₂)
< f₁ , f₂ >₁ x = {!!}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists with fast append
------------------------------------------------------------------------

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

module Data.DifferenceList where

open import Level using (Level)
open import Data.List.Base as List using (List)
open import Function
open import Data.Nat.Base

private
  variable
    a b : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Type definition and list function lifting

DiffList : Set a → Set a
DiffList A = List A → List A

lift : (List A → List A) → (DiffList A → DiffList A)
lift f xs = λ k → f (xs k)

------------------------------------------------------------------------
-- Building difference lists

infixr 5 _∷_ _++_

[] : DiffList A
[] = λ k → k

_∷_ : A → DiffList A → DiffList A
_∷_ x = lift (x List.∷_)

[_] : A → DiffList A
[ x ] = x ∷ []

_++_ : DiffList A → DiffList A → DiffList A
xs ++ ys = λ k → xs (ys k)

infixl 6 _∷ʳ_
_∷ʳ_ : DiffList A → A → DiffList A
xs ∷ʳ x = λ k → xs (x List.∷ k)

------------------------------------------------------------------------
-- Conversion back and forth with List

toList : DiffList A → List A
toList xs = xs List.[]

-- fromList xs is linear in the length of xs.

fromList : List A → DiffList A
fromList xs = λ k → xs ⟨ List._++_ ⟩ k

------------------------------------------------------------------------
-- Transforming difference lists

-- It is OK to use List._++_ here, since map is linear in the length of
-- the list anyway.

map : (A → B) → DiffList A → DiffList B
map f xs = λ k → List.map f (toList xs) ⟨ List._++_ ⟩ k

-- concat is linear in the length of the outer list.

concat : DiffList (DiffList A) → DiffList A
concat xs = concat' (toList xs)
  where
  concat' : List (DiffList A) → DiffList A
  concat' = List.foldr _++_ []

take : ℕ → DiffList A → DiffList A
take n = lift (List.take n)

drop : ℕ → DiffList A → DiffList A
drop n = lift (List.drop n)


text:
----------------------------------------------------------------------------------
-- The contents of this file is based on the work in "Setoids in Type           --
-- Theory" by Barthe et al. and Capretta's "Universal Algebra in Type Theory."  --
--                                                                              --
-- See http://www.cs.ru.nl/~venanzio/publications/Setoids_JFP_2003.pdf and      --
-- http://www.cs.ru.nl/~venanzio/publications/Universal_Algebra_TPHOLs_1999.pdf --
----------------------------------------------------------------------------------
module Setoid.Total where

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

open import Relation.Relation
open import Basics public
open import Equality.Eq public

open ParRel public
open EqRel public

-- Total setoids.
record Setoid {l : Level} : Set (lsuc l) where
 constructor Setoid_,_,_
 field
   el : Set l
   eq  : el → el → Set l
   eqRpf : EqRel eq

open Setoid public

-- Notation for the underlying equivalence of a setoid.
⟨_⟩[_≡_] : {l : Level} → (A : Setoid {l}) → el A → el A → Set l
⟨ A ⟩[ x ≡ y ] = eq A x y

-- Total empty setoids.
EmptySetoid : {l : Level} → Setoid {l}
EmptySetoid = record { el = ⊥-poly; eq = λ x y → x ≅ y; eqRpf = isEqRel }

-- Total setoids maps.  Barthe et al. calls "map."
record SetoidFun {l₁ l₂ : Level} (A : Setoid {l₁}) (B : Setoid {l₂}) : Set (l₁ ⊔ l₂) where
  field
    appT : el A → el B
    extT : ∀ {x y} → ⟨ A ⟩[ x ≡ y ] → ⟨ B ⟩[ appT x ≡ appT y ]

open SetoidFun public

-- The setoid function space from A to B.  Barthe et al. calls this
-- "Map."
SetoidFunSpace : {l₁ l₂ : Level} → Setoid {l₁} → Setoid {l₂} → Setoid {l₁ ⊔ l₂}
SetoidFunSpace A B with parEqPf (eqRpf B)
... | b = record { el = SetoidFun A B;
                   eq = λ f g → ∀ (x : el A) → ⟨ B ⟩[ appT f x ≡ appT g x ];
                eqRpf = record { parEqPf = record { symPf = λ x₁ x₂ → symPf b (x₁ x₂);
                                                  transPf = λ x₁ x₂ x₃ → transPf b (x₁ x₃) (x₂ x₃) };
                                 refPf   = λ x₁ → refPf (eqRpf B) } }

-- Total binary setoid maps.
BinSetoidFun : {l₁ l₂ l₃ : Level} → Setoid {l₁} → Setoid {l₂} → Setoid {l₃} → Set (l₁ ⊔ l₂ ⊔ l₃)
BinSetoidFun A B C = SetoidFun A (SetoidFunSpace B C)

-- A nice notation for composition of BMap's.
_○[_]_ : {l : Level}{A B C : Setoid {l}} → el A → BinSetoidFun A B C → el B → el C
f ○[ comp ] g = appT (appT comp f) g

-- Setoid predicates.
record Pred {l : Level} (A : Setoid {l}) : Set (lsuc l) where
  field
    -- The predicate.
    pf  : el A → Set l
    -- The proof that the predicate respects equality.
    inv : ∀{x y} → ⟨ A ⟩[ x ≡ y ] → pf x → pf y

open Pred

-- Setoid Subcarriers.
record Subcarrier {l : Level} (A : Setoid {l}) (P : Pred A) : Set l where
  field
    subel : el A
    insub : pf P subel

open Subcarrier

-- Subsetoids.
Subsetoid : {l : Level} → (A : Setoid {l}) → (P : Pred A) → Setoid {l}
Subsetoid A P with parEqPf (eqRpf A)
... | a = record { el    = Subcarrier A P; eq = λ x y → ⟨ A ⟩[ subel x ≡ subel y ];
                   eqRpf = record { parEqPf = record { symPf   = λ x₁ → symPf a x₁;
                                                       transPf = λ x₁ x₂ → transPf a x₁ x₂ };
                                    refPf = λ {x} → refPf (eqRpf A) } }

-- The product of two setoids.
ProductSetoid : {l₁ l₂ : Level} → Setoid {l₁} → Setoid {l₂} → Setoid {l₁ ⊔ l₂}
ProductSetoid A B =  record { el = (el A) × (el B);
                              eq = ProductRel (eq A) (eq B);
                           eqRpf = ProductRelIsEqRel (eq A) (eq B) (eqRpf A) (eqRpf B) }
_●ₛ_ : {l₁ l₂ : Level} → Setoid {l₁} → Setoid {l₂} → Setoid {l₁ ⊔ l₂}
A ●ₛ B = ProductSetoid A B

-- Product setoid functions.
ProdSetoidFun : {l₁ l₂ l₃ l₄ : Level}
                {A₁ : Setoid {l₁}}
                {B₁ : Setoid {l₂}}
                {A₂ : Setoid {l₃}}
                {B₂ : Setoid {l₄}}
              → (F₁ : SetoidFun A₁ A₂)
              → (F₂ : SetoidFun B₁ B₂)
              → SetoidFun (A₁ ●ₛ B₁) (A₂ ●ₛ B₂)
ProdSetoidFun F₁ F₂ = record { appT = λ x → appT F₁ (proj₁ x) , appT F₂ (proj₂ x);
                               extT = λ x₁ → extT F₁ (proj₁ x₁) , extT F₂ (proj₂ x₁) }

-- Binary product setoid functions.
BinProdSetoidFun : {l₁ l₂ l₃ l₄ : Level}
                   {A₁ : Setoid {l₁}}
                   {B₁ : Setoid {l₂}}
                   {C₁ : Setoid {l₃}}
                   {A₂ : Setoid {l₄}}
                   {B₂ : Setoid {l₄}}
                   {C₂ : Setoid {l₄}}
                 → (F₁ : BinSetoidFun A₁ B₁ C₁)
                 → (F₂ : BinSetoidFun A₂ B₂ C₂)
                 → BinSetoidFun (A₁ ●ₛ A₂) (B₁ ●ₛ B₂) (C₁ ●ₛ C₂)
BinProdSetoidFun F₁ F₂ = record { appT = λ x → ProdSetoidFun (appT F₁ (proj₁ x)) (appT F₂ (proj₂ x));
                                  extT = λ {a b} c d → (extT F₁ (proj₁ c) (proj₁ d)) , (extT F₂ (proj₂ c) (proj₂ d)) }

_●b_ : {l₁ l₂ l₃ l₄ : Level}
                   {A₁ : Setoid {l₁}}
                   {B₁ : Setoid {l₂}}
                   {C₁ : Setoid {l₃}}
                   {A₂ : Setoid {l₄}}
                   {B₂ : Setoid {l₄}}
                   {C₂ : Setoid {l₄}}
                 → (F₁ : BinSetoidFun A₁ B₁ C₁)
                 → (F₂ : BinSetoidFun A₂ B₂ C₂)
                 → BinSetoidFun (A₁ ●ₛ A₂) (B₁ ●ₛ B₂) (C₁ ●ₛ C₂)
F₁ ●b F₂ = BinProdSetoidFun F₁ F₂

-- Next we define a relaxed notion of a subsetoid where the predicate
-- does not have to be invariant on the equality.
↓Setoid : {l : Level}
  → (S : Setoid {l})
  → (P : el S → Set l)
  → Setoid {l}
↓Setoid S P =
  record { el = eq S ↓ P;
           eq = λ f g → ⟨ S ⟩[ proj₁ f ≡ proj₁ g ];
        eqRpf = ↓EqRel (eq S) P (eqRpf S)}

-- Restricted setoid functions.
↓SetoidFun :
    {l : Level}
    {S₁ S₂ : Setoid {l}}
    {P₁ : el S₁ → Set l}
    {P₂ : el S₂ → Set l}
  → (F : SetoidFun S₁ S₂)
  → ({f : el S₁} → (P₁ f) → P₂ (appT F f))
  → SetoidFun (↓Setoid S₁ P₁) (↓Setoid S₂ P₂)
↓SetoidFun {l}{S₁}{S₂}{P₁}{P₂} F pf =
  record { appT = λ x₁ → appT F (proj₁ x₁) , pf {proj₁ x₁} (proj₂ x₁);
           extT = λ {x}{y} x₂ → extT F x₂ }

-- Binary restricted setoid functions.
↓BinSetoidFun :
    {l : Level}
    {S₁ S₂ S₃ : Setoid {l}}
    {P₁ : el S₁ → Set l}
    {P₂ : el S₂ → Set l}
    {P₃ : el S₃ → Set l}
  → (F : BinSetoidFun S₁ S₂ S₃)
  → ({f : el S₁}{g : el S₂} → (P₁ f) → (P₂ g) → P₃ (f ○[ F ] g))
  → BinSetoidFun (↓Setoid S₁ P₁) (↓Setoid S₂ P₂) (↓Setoid S₃ P₃)
↓BinSetoidFun {l}{S₁}{S₂}{S₃}{P₁}{P₂}{P₃} F pf =
  record { appT = λ f → ↓SetoidFun (appT F (proj₁ f)) (pf (proj₂ f));
           extT = λ x₁ x₂ → extT F x₁ (proj₁ x₂) }

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly0-A where

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

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

private variable
  ℓ : Level

module Equiv-Poly0-A
  (Acr@(A , Astr) : CommRing ℓ) where

  private
    PA = PolyCommRing Acr 0

  open CommRingStr

-----------------------------------------------------------------------------
-- Equivalence

  Poly0→A : Poly Acr 0 → A
  Poly0→A = DS-Rec-Set.f _ _ _ _ (is-set Astr)
             (0r Astr)
             (λ v a → a)
             (_+_ Astr)
             (+Assoc Astr)
             (+IdR Astr)
             (+Comm Astr)
             (λ _ → refl)
             λ _ a b → refl

  A→Poly0 : A → Poly Acr 0
  A→Poly0 a = base [] a

  e-sect : (a : A) → Poly0→A (A→Poly0 a) ≡ a
  e-sect a = refl

  e-retr : (P : Poly Acr 0) → A→Poly0 (Poly0→A P) ≡ P
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
           (base-neutral [])
           (λ { [] a → refl })
           λ {U V} ind-U ind-V → (sym (base-add _ _ _)) ∙ (cong₂ (snd PA ._+_ ) ind-U ind-V)

-----------------------------------------------------------------------------
-- Ring homomorphism

  Poly0→A-pres1 : Poly0→A (snd PA .1r) ≡ 1r Astr
  Poly0→A-pres1 = refl

  Poly0→A-pres+ : (P Q : Poly Acr 0) → Poly0→A (snd PA ._+_ P Q) ≡ Astr ._+_ (Poly0→A P) (Poly0→A Q)
  Poly0→A-pres+ P Q = refl

  Poly0→A-pres· : (P Q : Poly Acr 0) → Poly0→A ( snd PA ._·_ P Q) ≡ Astr ._·_ (Poly0→A P) (Poly0→A Q)
  Poly0→A-pres· = DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ λ _ → is-set Astr _ _)
                    (λ Q → sym (RingTheory.0LeftAnnihilates (CommRing→Ring Acr) (Poly0→A Q)))
                    (λ v a → DS-Ind-Prop.f _ _ _ _ (λ _ → is-set Astr _ _)
                              (sym (RingTheory.0RightAnnihilates (CommRing→Ring Acr) (Poly0→A (base v a))))
                              (λ v' a' → refl)
                              λ {U V} ind-U ind-V → (cong₂ (Astr ._+_) ind-U ind-V) ∙ sym (·DistR+ Astr _ _ _))
                    λ {U V} ind-U ind-V Q → (cong₂ (Astr ._+_) (ind-U Q) (ind-V Q)) ∙ sym (·DistL+ Astr _ _ _)

-----------------------------------------------------------------------------
-- Ring Equivalence

module _ (A' : CommRing ℓ) where

  open Equiv-Poly0-A A'

  CRE-Poly0-A : CommRingEquiv (PolyCommRing A' 0) A'
  fst CRE-Poly0-A = isoToEquiv is
    where
    is : Iso (Poly A' 0) (A' .fst)
    Iso.fun is = Poly0→A
    Iso.inv is = A→Poly0
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr
  snd CRE-Poly0-A = makeIsRingHom Poly0→A-pres1 Poly0→A-pres+ Poly0→A-pres·


text:
-- Andreas, 2017-07-28, issue #1077

-- Agda's reconstruction of the top-level module can be confusing
-- in case the user puts some illegal declarations before the
-- top level module in error.

-- Thus, Agda now rejects the following if the anon. module is omitted.
-- If the user writes the anon. module, it should be accepted,
-- (even if it looks stupid in this case).

module _ where

foo = Set

module Issue1077 where

  bar = Set

-- Should be accepted.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module DefinitionalEquality where

postulate
  _≡_      : {A B : Set} -> A -> B -> Set
  refl-≡   : {A : Set}{x : A} -> x ≡ x
  subst-≡  : {A : Set}{x y : A}(C : A -> Set) -> x ≡ y -> C y -> C x
  subst-≡¹ : {A : Set}{x y : A}(C : A -> Set1) -> x ≡ y -> C y -> C x

  subst-≡' : {A B : Set}{x : A}{y : B}(C : {X : Set} -> X -> Set) -> x ≡ y -> C y -> C x

  app-≡₀ : {A₁ A₂ : Set}{B₁ : A₁ -> Set}{B₂ : A₂ -> Set}
           {f : (x : A₁) -> B₁ x}{g : (x : A₂) -> B₂ x}{a₁ : A₁}{a₂ : A₂} ->
            f ≡ g -> a₁ ≡ a₂ -> f a₁ ≡ g a₂

  η-≡ : {A₁ A₂ : Set}{B₁ : A₁ -> Set}{B₂ : A₂ -> Set}
        {f₁ : (x : A₁) -> B₁ x}{f₂ : (x : A₂) -> B₂ x} ->
        ((x : A₁)(y : A₂) -> x ≡ y -> f₁ x ≡ f₂ y) -> f₁ ≡ f₂

  -- Substitution is a no-op
  subst-≡-identity : {A : Set}{x y : A}(C : A -> Set)(p : x ≡ y)(cy : C y) ->
                     subst-≡ C p cy ≡ cy

cong-≡ : {A B : Set}{x y : A}(f : A -> B)(p : x ≡ y) -> f x ≡ f y
cong-≡ {_}{_}{_}{y} f p = subst-≡ (\z -> f z ≡ f y) p refl-≡

cong-≡' : {A : Set}{B : A -> Set}{x y : A}(f : (z : A) -> B z)(p : x ≡ y) -> f x ≡ f y
cong-≡' {_}{_}{_}{y} f p = subst-≡ (\z -> f z ≡ f y) p refl-≡

cong₂-≡' : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
	   {x y : A}{z : B x}{w : B y}(f : (x : A)(z : B x) -> C x z) ->
	   x ≡ y -> z ≡ w -> f x z ≡ f y w
cong₂-≡' f xy zw = app-≡₀ (cong-≡' f xy) zw

trans-≡ : {A B C : Set}(x : A)(y : B)(z : C) -> x ≡ y -> y ≡ z -> x ≡ z
trans-≡ x y z xy yz = subst-≡' (\w -> w ≡ z) xy yz

postulate
  _≡₁_     : {A B : Set1} -> A -> B -> Set1
  refl-≡₁  : {A : Set1}{x : A} -> x ≡₁ x
  subst-≡₁ : {A : Set1}{x y : A}(C : A -> Set1) -> x ≡₁ y -> C y -> C x
  subst-≡₁' : {A B : Set1}{x : A}{y : B}(C : {X : Set1} -> X -> Set1) -> x ≡₁ y -> C y -> C x

  -- Substitution is a no-op
  subst-≡₁-identity : {A : Set1}{x y : A}(C : A -> Set1)(p : x ≡₁ y)(cy : C y) ->
                      subst-≡₁ C p cy ≡₁ cy

  app-≡₁ : {A₁ A₂ : Set1}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
           {f : (x : A₁) -> B₁ x}{g : (x : A₂) -> B₂ x}{a₁ : A₁}{a₂ : A₂} ->
           f ≡₁ g -> a₁ ≡₁ a₂ -> f a₁ ≡₁ g a₂

  app-≡₁⁰ : {A₁ A₂ : Set}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
            {f : (x : A₁) -> B₁ x}{g : (x : A₂) -> B₂ x}{a₁ : A₁}{a₂ : A₂} ->
            f ≡₁ g -> a₁ ≡ a₂ -> f a₁ ≡₁ g a₂

  η-≡₁ : {A₁ A₂ : Set1}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
         {f₁ : (x : A₁) -> B₁ x}{f₂ : (x : A₂) -> B₂ x} ->
         ((x : A₁)(y : A₂) -> x ≡₁ y -> f₁ x ≡₁ f₂ y) -> f₁ ≡₁ f₂

  η-≡₁⁰ : {A₁ A₂ : Set}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
          {f₁ : (x : A₁) -> B₁ x}{f₂ : (x : A₂) -> B₂ x} ->
          ((x : A₁)(y : A₂) -> x ≡ y -> f₁ x ≡₁ f₂ y) -> f₁ ≡₁ f₂

cong-≡₁ : {A B : Set1}{x y : A}(f : A -> B)(p : x ≡₁ y) -> f x ≡₁ f y
cong-≡₁ {_}{_}{_}{y} f p = subst-≡₁ (\z -> f z ≡₁ f y) p refl-≡₁

cong-≡₁⁰ : {A : Set}{B : A -> Set1}{x y : A}(f : (x : A) -> B x)(p : x ≡ y) -> f x ≡₁ f y
cong-≡₁⁰ {_}{_}{_}{y} f p = subst-≡¹ (\z -> f z ≡₁ f y) p refl-≡₁

trans-≡₁ : {A B C : Set1}(x : A)(y : B)(z : C) -> x ≡₁ y -> y ≡₁ z -> x ≡₁ z
trans-≡₁ x y z xy yz = subst-≡₁' (\w -> w ≡₁ z) xy yz

max_stars_repo_name: asr/agda-kanso


text:
-- Andreas, 2016-06-16 Issue #2045
-- Size solver should be called before checking extended lambda

-- {-# OPTIONS -v tc.term.exlam:100 #-}

open import Common.Size

postulate anything : ∀{a}{A : Set a} → A

data Exp : Size → Set where
  abs : ∀ i (t : Exp i) → Exp (↑ i)

data Val : ∀ i (t : Exp i) → Set where
  valAbs : ∀ i (t : Exp i) → Val (↑ i) (abs i t)

data Whnf i (t : Exp i) : Set where
  immed : (v : Val i t) → Whnf i t

postulate
  Evaluate : ∀ i (t : Exp i) (P : (w : Whnf i t) → Set) → Set

worksE : ∀ i (fa : Exp i) → Set
worksE i fa = Evaluate i fa λ{ (immed (valAbs _ _)) → anything }

works : ∀ i (fa : Exp i) → Set
works i fa = Evaluate i fa aux
  where
  aux : Whnf i fa → Set
  aux (immed (valAbs _ _)) = anything

test : ∀ i (fa : Exp i) → Set
test i fa = Evaluate _ fa λ{ (immed (valAbs _ _)) → anything }

-- Should work.

-- WAS:
-- extended lambda's implementation ".extendedlambda1" has type:
-- (Whnf (_38 i fa) fa → Set)

-- Cannot instantiate the metavariable _38 to solution (↑ i₁) since it
-- contains the variable i₁ which is not in scope of the metavariable
-- or irrelevant in the metavariable but relevant in the solution
-- when checking that the pattern (valAbs _ _) has type
-- (Val (_38 i fa) fa)


text:
module Issue23 where

postulate
  ℝ   : Set
  r₀  : ℝ
  _+_ : ℝ → ℝ → ℝ
  -_  : ℝ → ℝ

_-_ : ℝ → ℝ → ℝ
x - y = x + (- y)

infixl 4 _≡_

-- Equality.
data _≡_ : ℝ → ℝ → Set where
  refl : (x : ℝ) → x ≡ x

postulate ─-neut : {x : ℝ} → r₀ - x ≡ - x
{-# ATP prove ─-neut #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

open import Functions.Definition
open import Functions.Lemmas
open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Sets.Cardinality.Infinite.Definition
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas

module Sets.Cardinality.Infinite.Lemmas where

finsetNotInfinite : {n : ℕ} → InfiniteSet (FinSet n) → False
finsetNotInfinite {n} isInfinite = isInfinite n id idIsBijective

noInjectionNToFinite : {n : ℕ} → {f : ℕ → FinSet n} → Injection f → False
noInjectionNToFinite {n} {f} inj = pigeonhole (le 0 refl) tInj
  where
    t : FinSet (succ n) → FinSet n
    t m = f (toNat m)
    tInj : Injection t
    tInj {x} {y} fx=fy = toNatInjective x y (inj fx=fy)

dedekindInfiniteImpliesInfinite : {a : _} (A : Set a) → DedekindInfiniteSet A → InfiniteSet A
dedekindInfiniteImpliesInfinite A record { inj = inj ; isInjection = isInjection } zero f x with Invertible.inverse (bijectionImpliesInvertible x) (inj 0)
... | ()
dedekindInfiniteImpliesInfinite A record { inj = inj ; isInjection = isInj } (succ n) f isBij = noInjectionNToFinite {f = t} tInjective
  where
    t : ℕ → FinSet (succ n)
    t n = Invertible.inverse (bijectionImpliesInvertible isBij) (inj n)
    tInjective : Injection t
    tInjective pr = isInj ((Bijection.inj (invertibleImpliesBijection (inverseIsInvertible (bijectionImpliesInvertible isBij)))) pr)


text:
module Issue642 where

module M₁ (X : Set) where
  postulate F : X → Set

module M₂ (X : Set) where
  open M₁ X public

postulate
  A : Set
  x : A

open M₂ A

foo : F x
foo = {!!}

-- The goal was displayed as M₁.F A x rather than F x. If "open M₂ A"
-- is replaced by "open M₁ A", then the goal is displayed correctly.

max_stars_repo_name: np/agda-git-experiment


text:
-- Andreas, 2021-04-19, fixed #5236, regression introduced by #2858.
-- In record declarations, `constructor` should not be a layout keyword,
-- in order to be compatible with Agda 2.6.1.

record Works : Set₁ where
  eta-equality; field
    W : Set

record Test : Set₁ where
  constructor c; field
    F : Set   -- Should work

record Test2 : Set₁ where
  constructor c; eta-equality -- Should work
  field
    foo : Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module F1a where

open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Product hiding (map)
open import Data.List

open import Data.Nat
open import Data.Bool

{--
infixr 90 _⊗_
infixr 80 _⊕_
infixr 60 _∘_
infix  30 _⟷_
--}

---------------------------------------------------------------------------
-- Paths

-- Path relation should be an equivalence
data IPath (I A : Set) : Set where
  _↝_ : {i : I} (a : A) → (b : A) → IPath I A

id↝ : {A : Set} → A → IPath ⊤ A
id↝ a = a ↝ a

ap : {A B I J : Set} → (I → J) → (A → B) → IPath I A → IPath J B
ap g f (_↝_ {i} a a') = _↝_ {i = g i} (f a) (f a')

ZIP : (K : Set → Set → Set) → (P : Set → Set → Set)
     → (I : Set) → (J : Set) → (A : Set) → (B : Set) → Set
ZIP K P I J A B = K I A → K J B → K (P I J) (P A B)

pathProd : {A B I J : Set} → ZIP IPath _×_ I J A B
pathProd (_↝_ {i = i} a a') (_↝_ {i = j} b b') = _↝_ {i = i , j} (a , b) (a' , b')

prod : {X Y Z : Set} → (X → Y → Z) → List X → List Y → List Z
prod f l₁ l₂ = concatMap (λ b → map (f b) l₂) l₁

_×↝_ : {A B I J : Set} → List (IPath I A) → List (IPath J B) → List (IPath (I × J) (A × B))
_×↝_ = prod pathProd

-- pi types with exactly one level of reciprocals

data B0 : Set where
  ONE    : B0
  PLUS0  : B0 → B0 → B0
  TIMES0 : B0 → B0 → B0

data B1 : Set where
  LIFT0  : B0 → B1
  PLUS1  : B1 → B1 → B1
  TIMES1 : B1 → B1 → B1
  RECIP1 : B0 → B1

-- interpretation of B0 as discrete groupoids

record 0-type : Set₁ where
  constructor G₀
  field
    ∣_∣₀ : Set

open 0-type public

plus : 0-type → 0-type → 0-type
plus t₁ t₂ = G₀ (∣ t₁ ∣₀ ⊎ ∣ t₂ ∣₀)

times : 0-type → 0-type → 0-type
times t₁ t₂ = G₀ (∣ t₁ ∣₀ × ∣ t₂ ∣₀)

⟦_⟧₀ : B0 → 0-type
⟦ ONE ⟧₀ = G₀ ⊤
⟦ PLUS0 b₁ b₂ ⟧₀ = plus ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀
⟦ TIMES0 b₁ b₂ ⟧₀ = times ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀

ı₀ : B0 → Set
ı₀ b = ∣ ⟦ b ⟧₀ ∣₀

elems0 : (b : B0) → List (ı₀ b)
elems0 ONE = [ tt ]
elems0 (PLUS0 b b') = map inj₁ (elems0 b) ++ map inj₂ (elems0 b')
elems0 (TIMES0 b b') =
--  concatMap (λ a → map (λ b → (a , b)) (elems0 b')) (elems0 b)
    prod _,_ (elems0 b) (elems0 b')

point : (b : B0) → ı₀ b
point ONE = tt
point (PLUS0 b _) = inj₁ (point b)
point (TIMES0 b₀ b₁) = point b₀ , point b₁

expand : ∀ {I} (b : B0) → ( ı₀ b → IPath I (ı₀ b)) → List (IPath I (ı₀ b))
expand x f = map f (elems0 x)

-- interpretation of B1 types as 2-types

record 1-type : Set₁ where
  constructor G₂
  field
    I : Set
    ∣_∣₁ : Set
    1-paths : List (IPath I ∣_∣₁)

open 1-type public

_⊎↝_ : {I J A B : Set} → List (IPath I A) → List (IPath J B) → List (IPath (I ⊎ J) (A ⊎ B))
p₁ ⊎↝ p₂ = map (ap inj₁ inj₁) p₁ ++ map (ap inj₂ inj₂) p₂

⟦_⟧₁ : B1 → 1-type
⟦ LIFT0 b0 ⟧₁ = G₂ ⊤ (ı₀ b0) (expand b0 id↝)
⟦ PLUS1 b₁ b₂ ⟧₁ with ⟦ b₁ ⟧₁ | ⟦ b₂ ⟧₁
... | G₂ I₁ 0p₁ 1p₁ | G₂ I₂ 0p₂ 1p₂ = G₂ (I₁ ⊎ I₂) (0p₁ ⊎ 0p₂) (1p₁ ⊎↝ 1p₂)
⟦ TIMES1 b₁ b₂ ⟧₁ with ⟦ b₁ ⟧₁ | ⟦ b₂ ⟧₁
... | G₂ I₁ 0p₁ 1p₁ | G₂ I₂ 0p₂ 1p₂ = G₂ (I₁ × I₂) (0p₁ × 0p₂) (1p₁ ×↝ 1p₂)
⟦ RECIP1 b0 ⟧₁ = G₂ (ı₀ (TIMES0 b0 b0)) ⊤ (prod (λ a b → _↝_ {i = a , b} tt tt) (elems0 b0) (elems0 b0) )

ı₁ : B1 → Set
ı₁ b = ∣ ⟦ b ⟧₁ ∣₁

test10 = ⟦ LIFT0 ONE ⟧₁
test11 = ⟦ LIFT0 (PLUS0 ONE ONE) ⟧₁
test12 = ⟦ RECIP1 (PLUS0 ONE ONE) ⟧₁

-- isos

data _⟷_ : B1 → B1 → Set where
  -- +
  swap₊   : { b₁ b₂ : B1 } → PLUS1 b₁ b₂ ⟷ PLUS1 b₂ b₁
  -- *
  unite⋆  : { b : B1 } → TIMES1 (LIFT0 ONE) b ⟷ b
  uniti⋆  : { b : B1 } → b ⟷ TIMES1 (LIFT0 ONE) b
{-  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  -- congruence
  id⟷   : { b : B } → b ⟷ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _∘_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)
-}
  η⋆ : (b : B0) → LIFT0 ONE ⟷ TIMES1 (LIFT0 b) (RECIP1 b)
  ε⋆ : (b : B0) → TIMES1 (LIFT0 b) (RECIP1 b) ⟷ LIFT0 ONE
-- interpret isos as functors

record 1-functor (A B : 1-type) : Set where
  constructor F₁
  field
    find : I A → I B
    fobj : ∣ A ∣₁ → ∣ B ∣₁
    fmor : List (IPath (I A) ∣ A ∣₁) →  List (IPath (I B) ∣ B ∣₁)

open 1-functor public

ipath : B1 → Set
ipath b = IPath (I ⟦ b ⟧₁) (ı₁ b)

swap⊎ : {A B : Set} → A ⊎ B → B ⊎ A
swap⊎ (inj₁ a) = inj₂ a
swap⊎ (inj₂ b) = inj₁ b

elim1⋆ : {b : B1} → ipath (TIMES1 (LIFT0 ONE) b) → ipath b
elim1⋆ (_↝_ {tt , x} (tt , y) (tt , z)) = _↝_ {i = x} y z

intro1⋆ : {b : B1} → ipath b → ipath (TIMES1 (LIFT0 ONE) b)
intro1⋆ (_↝_ {x} y z) = _↝_ {i = tt , x} (tt , y) (tt , z)

Iη⋆ : (b : B0) → I ⟦ LIFT0 ONE ⟧₁ → I ⟦ TIMES1 (LIFT0 b) (RECIP1 b) ⟧₁
Iη⋆ b tt = tt , (point b , point b)

Iε⋆ : (b : B0) → I ⟦ TIMES1 (LIFT0 b) (RECIP1 b) ⟧₁ → I ⟦ LIFT0 ONE ⟧₁
Iε⋆ b (tt , x) = tt

objη⋆ : (b : B0) → ı₁ (LIFT0 ONE) → ı₁ (TIMES1 (LIFT0 b) (RECIP1 b))
objη⋆ b tt = point b , tt

objε⋆ : (b : B0) → ı₁ (TIMES1 (LIFT0 b) (RECIP1 b)) → ı₁ (LIFT0 ONE)
objε⋆ b (x , tt) = tt

sw : {b₁ b₂ : B1} → ipath (PLUS1 b₁ b₂) → ipath (PLUS1 b₂ b₁)
sw (_↝_ {i} (inj₁ x) (inj₁ y)) = _↝_ {i = swap⊎ i} (inj₂ x) (inj₂ y)
sw (_↝_ {i} (inj₁ x) (inj₂ y)) = _↝_ {i = swap⊎ i} (inj₂ x) (inj₁ y)
sw (_↝_ {i} (inj₂ x) (inj₁ y)) = _↝_ {i = swap⊎ i} (inj₁ x) (inj₂ y)
sw (_↝_ {i} (inj₂ x) (inj₂ y)) = _↝_ {i = swap⊎ i} (inj₁ x) (inj₁ y)

elim1I : (b : B1) → I ⟦ TIMES1 (LIFT0 ONE) b ⟧₁ → I ⟦ b ⟧₁
elim1I b (tt , x) = x

elim1∣₁ : (b : B1) → ı₁ (TIMES1 (LIFT0 ONE) b) → ı₁ b
elim1∣₁ b (tt , x) = x

introI : (b : B1) → I ⟦ b ⟧₁ → I ⟦ TIMES1 (LIFT0 ONE) b ⟧₁
introI b x = (tt , x)

intro1∣₁ : (b : B1) → ı₁ b → ı₁ (TIMES1 (LIFT0 ONE) b)
intro1∣₁ b x = (tt , x)

eta : (b : B0) → List (ipath (LIFT0 ONE)) → List (ipath (TIMES1 (LIFT0 b) (RECIP1 b)))
-- note how the input list is not used at all!
eta b _ = prod (λ a a' → _↝_ {i = tt , a , a'} (a , tt) (a' , tt)) (elems0 b) (elems0 b)

eps : (b : B0) → ipath (TIMES1 (LIFT0 b) (RECIP1 b)) → ipath (LIFT0 ONE)
eps b0 (_↝_ {i = i} a b) = _↝_ tt tt

mutual
  eval : {b₁ b₂ : B1} → (b₁ ⟷ b₂) → 1-functor ⟦ b₁ ⟧₁ ⟦ b₂ ⟧₁
  eval (swap₊ {b₁} {b₂}) = F₁ swap⊎ swap⊎ (map (sw {b₁} {b₂}))
  eval (unite⋆ {b}) = F₁ (elim1I b) (elim1∣₁ b) (map (elim1⋆ {b}))
  eval (uniti⋆ {b}) = F₁ (introI b) (intro1∣₁ b) (map (intro1⋆ {b}))
  eval (η⋆ b) = F₁ (Iη⋆ b) (objη⋆ b) (eta b )
  eval (ε⋆ b) = F₁ (Iε⋆ b) (objε⋆ b) (map (eps b))

  evalB : {b₁ b₂ : B1} → (b₁ ⟷ b₂) → 1-functor ⟦ b₂ ⟧₁ ⟦ b₁ ⟧₁
  evalB (swap₊ {b₁} {b₂}) = F₁ swap⊎ swap⊎ (map (sw {b₂} {b₁}))
  evalB (unite⋆ {b}) = F₁ (introI b) (intro1∣₁ b) (map (intro1⋆ {b}))
  evalB (uniti⋆ {b}) = F₁ (elim1I b) (elim1∣₁ b) (map (elim1⋆ {b}))
  evalB (η⋆ b) = F₁ (Iε⋆ b) (objε⋆ b) (map (eps b))
  evalB (ε⋆ b) = F₁ (Iη⋆ b) (objη⋆ b) (eta b)

{- eval assocl₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
eval assocr₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
eval uniti⋆ = ? -- : { b : B } → b ⟷ TIMES ONE b
eval swap⋆ = ? --  : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
eval assocl⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
eval assocr⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
eval dist = ? -- : { b₁ b₂ b₃ : B } → TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
eval factor = ? -- : { b₁ b₂ b₃ : B } → PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
eval id⟷ = ? --  : { b : B } → b ⟷ b
eval (sym c) = ? -- : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
eval (c₁ ∘ c₂) = ? -- : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
eval (c₁ ⊕ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
eval (c₁ ⊗ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)

---------------------------------------------------------------------------
--}


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary using (Setoid)

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.Renaming
import SecondOrder.Term
import SecondOrder.Substitution
import SecondOrder.Instantiation
import SecondOrder.Theory

module SecondOrder.Equality
  {ℓ ℓa}
  {𝔸 : SecondOrder.Arity.Arity}
  {Σ : SecondOrder.Signature.Signature ℓ 𝔸}
  (𝕋 : SecondOrder.Theory.Theory Σ ℓa)
  where

  open SecondOrder.Metavariable Σ
  open SecondOrder.Renaming Σ
  open SecondOrder.Term Σ
  open SecondOrder.Substitution Σ
  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Instantiation Σ
  open SecondOrder.Theory.Theory 𝕋

  record Equation : Set (lsuc ℓ) where
    constructor make-eq
    field
      eq-mv-ctx : MContext -- metavariable context of an equation
      eq-ctx : VContext -- variable context of an equation
      eq-sort : sort -- sort of an equation
      eq-lhs : Term eq-mv-ctx eq-ctx eq-sort -- left-hand side
      eq-rhs : Term eq-mv-ctx eq-ctx eq-sort -- right-hand side

  infix 5 make-eq

  syntax make-eq Θ Γ A s t = Θ ⊕ Γ ∥ s ≋ t ⦂ A

  -- Instantiate an axiom of 𝕋 to an equation
  instantiate-axiom : ∀ (ε : ax) {Θ Γ} (I : ax-mv-ctx ε ⇒ⁱ Θ ⊕ Γ) → Equation
  instantiate-axiom ε {Θ} {Γ} I =
     Θ ⊕ Γ ∥ [ I ]ⁱ (ax-lhs ε) ≋  [ I ]ⁱ (ax-rhs ε) ⦂ ax-sort ε

  -- The equality judgement

  infix 4 ⊢_

  data ⊢_ : Equation → Set (lsuc (ℓ ⊔ ℓa)) where
    -- general rules
    eq-refl : ∀ {Θ Γ A} {t : Term Θ Γ A} → ⊢ Θ ⊕ Γ ∥ t ≋ t ⦂ A
    eq-symm : ∀ {Θ Γ A} {s t : Term Θ Γ A} → ⊢ Θ ⊕ Γ ∥ s ≋ t ⦂ A → ⊢ Θ ⊕ Γ ∥ t ≋ s ⦂ A
    eq-trans : ∀ {Θ Γ A} {s t u : Term Θ Γ A} → ⊢ Θ ⊕ Γ ∥ s ≋ t ⦂ A → ⊢ Θ ⊕ Γ ∥ t ≋ u ⦂ A → ⊢ Θ ⊕ Γ ∥ s ≋ u ⦂ A

    -- Congruence rule for operations
    -- the premises are: an operation f, two sets of arguments xs, ys of f that give
    -- for each argument of f a term in the extended context with the arguments that f binds
    -- such that xᵢ ≋ yᵢ for each i ∈ oper-arity f
    -- then f xs ≋ f ys (in the appropriate context)
    eq-oper : ∀ {Γ Θ} {f : oper}
                 {xs ys : ∀ (i : oper-arg f) → Term Θ (Γ ,, arg-bind f i) (arg-sort f i)}
                 → (∀ i → ⊢ Θ ⊕ (Γ ,, arg-bind f i) ∥ (xs i) ≋ (ys i) ⦂ (arg-sort f i))
                 → ⊢ Θ ⊕ Γ ∥  (tm-oper f xs) ≋ (tm-oper f ys) ⦂ (oper-sort f)
    -- Congruence rule for metavariables
    -- the permises are: a meta-variable M, and two sets of arguments of the appropriate
    -- sorts and arities to apply M, such that xᵢ ≋ yᵢ
    -- then M xs ≋ M ys
    eq-meta : ∀ {Γ Θ} {Γᴹ Aᴹ} {M : [ Γᴹ , Aᴹ ]∈ Θ} {xs ys : ∀ {B : sort} (i : B ∈ Γᴹ) → Term Θ Γ B}
                → (∀ {B : sort} (i : B ∈ Γᴹ)
                → ⊢ Θ ⊕ Γ ∥ (xs i) ≋ (ys i) ⦂ B)
                → ⊢ Θ ⊕ Γ ∥  (tm-meta M xs) ≋ (tm-meta M ys) ⦂ Aᴹ
    -- equational axiom
    eq-axiom : ∀ (ε : ax) {Θ Γ} (I : ax-mv-ctx ε ⇒ⁱ Θ ⊕ Γ) → ⊢ instantiate-axiom ε I

  -- Syntactically equal terms are judgementally equal
  ≈-≋ : ∀ {Θ Γ A} {s t : Term Θ Γ A} → s ≈ t → ⊢ Θ ⊕ Γ ∥ s ≋ t ⦂ A
  ≈-≋ (≈-≡ refl) = eq-refl
  ≈-≋ (≈-meta ξ) = eq-meta (λ i → ≈-≋ (ξ i))
  ≈-≋ (≈-oper ξ) = eq-oper (λ i → ≈-≋ (ξ i))

  --  terms and judgemental equality form a setoid
  eq-setoid : ∀ (Γ : VContext) (Θ : MContext) (A : sort) → Setoid ℓ (lsuc (ℓ ⊔ ℓa))
  eq-setoid Γ Θ A =
    record
      { Carrier = Term Θ Γ A
      ;  _≈_ = λ s t → ⊢ Θ ⊕ Γ ∥ s ≋ t ⦂ A
      ; isEquivalence =
          record
            { refl = eq-refl
            ; sym = eq-symm
            ; trans = eq-trans
            }
      }

  -- judgemental equality of substitutions
  _≋ˢ_ : ∀ {Θ Γ Δ} (σ τ : Θ ⊕ Γ ⇒ˢ Δ) → Set (lsuc (ℓ ⊔ ℓa))
  _≋ˢ_ {Θ} {Γ} {Δ} σ τ = ∀ {A} (x : A ∈ Γ) → ⊢ Θ ⊕ Δ ∥ σ x ≋ τ x ⦂ A

  ≈ˢ-≋ˢ : ∀ {Θ Γ Δ} {σ τ : Θ ⊕ Γ ⇒ˢ Δ} → σ ≈ˢ τ → σ ≋ˢ τ
  ≈ˢ-≋ˢ ξ = λ x → ≈-≋ (ξ x)

  -- judgemental equality of metavariable instatiations
  _≋ⁱ_ : ∀ {Θ Ξ Γ} (I J : Θ ⇒ⁱ Ξ ⊕ Γ) → Set (lsuc (ℓ ⊔ ℓa))
  _≋ⁱ_ {Θ} {Ξ} {Γ} I J = ∀ {Γᴹ Aᴹ} (M : [ Γᴹ , Aᴹ ]∈ Θ) → ⊢ Ξ ⊕ (Γ ,, Γᴹ) ∥ I M ≋ J M ⦂ Aᴹ

max_stars_repo_name: andrejbauer/formal

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------

-- The definition of lexicographic ordering used here is suitable if
-- the argument order is a strict partial order. The lexicographic
-- ordering itself can be either strict or non-strict, depending on
-- the value of a parameter.

module Relation.Binary.List.StrictLex where

open import Data.Empty
open import Data.Unit using (⊤; tt)
open import Function
open import Data.Product
open import Data.Sum
open import Data.List
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.List.Pointwise as Pointwise
   using ([]; _∷_; head; tail)

module _ {A : Set} where

  data Lex (P : Set) (_≈_ _<_ : Rel A zero) : Rel (List A) zero where
    base : P                             → Lex P _≈_ _<_ []       []
    halt : ∀ {y ys}                      → Lex P _≈_ _<_ []       (y ∷ ys)
    this : ∀ {x xs y ys} (x<y : x < y)   → Lex P _≈_ _<_ (x ∷ xs) (y ∷ ys)
    next : ∀ {x xs y ys} (x≈y : x ≈ y)
           (xs⊴ys : Lex P _≈_ _<_ xs ys) → Lex P _≈_ _<_ (x ∷ xs) (y ∷ ys)

  -- Strict lexicographic ordering.

  Lex-< : (_≈_ _<_ : Rel A zero) → Rel (List A) zero
  Lex-< = Lex ⊥

  ¬[]<[] : ∀ {_≈_ _<_} → ¬ Lex-< _≈_ _<_ [] []
  ¬[]<[] (base ())

  -- Non-strict lexicographic ordering.

  Lex-≤ : (_≈_ _<_ : Rel A zero) → Rel (List A) zero
  Lex-≤ = Lex ⊤

  -- Utilities.

  ¬≤-this : ∀ {P _≈_ _<_ x y xs ys} → ¬ (x ≈ y) → ¬ (x < y) →
            ¬ Lex P _≈_ _<_ (x ∷ xs) (y ∷ ys)
  ¬≤-this ¬x≈y ¬x<y (this x<y)       = ¬x<y x<y
  ¬≤-this ¬x≈y ¬x<y (next x≈y xs⊴ys) = ¬x≈y x≈y

  ¬≤-next : ∀ {P _≈_ _<_ x y xs ys} →
            ¬ (x < y) → ¬ Lex P _≈_ _<_ xs ys →
            ¬ Lex P _≈_ _<_ (x ∷ xs) (y ∷ ys)
  ¬≤-next ¬x<y ¬xs⊴ys (this x<y)       = ¬x<y x<y
  ¬≤-next ¬x<y ¬xs⊴ys (next x≈y xs⊴ys) = ¬xs⊴ys xs⊴ys

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

  ≤-reflexive : ∀ _≈_ _<_ → Pointwise.Rel _≈_ ⇒ Lex-≤ _≈_ _<_
  ≤-reflexive _≈_ _<_ []            = base tt
  ≤-reflexive _≈_ _<_ (x≈y ∷ xs≈ys) =
    next x≈y (≤-reflexive _≈_ _<_ xs≈ys)

  <-irreflexive : ∀ {_≈_ _<_} → Irreflexive _≈_ _<_ →
                  Irreflexive (Pointwise.Rel _≈_) (Lex-< _≈_ _<_)
  <-irreflexive irr []            (base ())
  <-irreflexive irr (x≈y ∷ xs≈ys) (this x<y)       = irr x≈y x<y
  <-irreflexive irr (x≈y ∷ xs≈ys) (next x≊y xs⊴ys) =
    <-irreflexive irr xs≈ys xs⊴ys

  transitive : ∀ {P _≈_ _<_} →
               IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
               Transitive (Lex P _≈_ _<_)
  transitive {P} {_≈_} {_<_} eq resp tr = trans
    where
    trans : Transitive (Lex P _≈_ _<_)
    trans (base p)         (base _)         = base p
    trans (base y)         halt             = halt
    trans halt             (this y<z)       = halt
    trans halt             (next y≈z ys⊴zs) = halt
    trans (this x<y)       (this y<z)       = this (tr x<y y<z)
    trans (this x<y)       (next y≈z ys⊴zs) = this (proj₁ resp y≈z x<y)
    trans (next x≈y xs⊴ys) (this y<z)       =
       this (proj₂ resp (IsEquivalence.sym eq x≈y) y<z)
    trans (next x≈y xs⊴ys) (next y≈z ys⊴zs) =
       next (IsEquivalence.trans eq x≈y y≈z) (trans xs⊴ys ys⊴zs)

  antisymmetric :
    ∀ {P _≈_ _<_} →
    Symmetric _≈_ → Irreflexive _≈_ _<_ →  Asymmetric _<_ →
    Antisymmetric (Pointwise.Rel _≈_) (Lex P _≈_ _<_)
  antisymmetric {P} {_≈_} {_<_} sym ir asym = as
    where
    as : Antisymmetric (Pointwise.Rel _≈_) (Lex P _≈_ _<_)
    as (base _)         (base _)         = []
    as halt             ()
    as (this x<y)       (this y<x)       = ⊥-elim (asym x<y y<x)
    as (this x<y)       (next y≈x ys⊴xs) = ⊥-elim (ir (sym y≈x) x<y)
    as (next x≈y xs⊴ys) (this y<x)       = ⊥-elim (ir (sym x≈y) y<x)
    as (next x≈y xs⊴ys) (next y≈x ys⊴xs) = x≈y ∷ as xs⊴ys ys⊴xs

  <-asymmetric : ∀ {_≈_ _<_} →
                 Symmetric _≈_ → _<_ Respects₂ _≈_ → Asymmetric _<_ →
                 Asymmetric (Lex-< _≈_ _<_)
  <-asymmetric {_≈_} {_<_} sym resp as = asym
    where
    irrefl : Irreflexive _≈_ _<_
    irrefl = asym⟶irr resp sym as

    asym : Asymmetric (Lex-< _≈_ _<_)
    asym (base bot)       _                = bot
    asym halt             ()
    asym (this x<y)       (this y<x)       = as x<y y<x
    asym (this x<y)       (next y≈x ys⊴xs) = irrefl (sym y≈x) x<y
    asym (next x≈y xs⊴ys) (this y<x)       = irrefl (sym x≈y) y<x
    asym (next x≈y xs⊴ys) (next y≈x ys⊴xs) = asym xs⊴ys ys⊴xs

  respects₂ : ∀ {P _≈_ _<_} →
              IsEquivalence _≈_ → _<_ Respects₂ _≈_ →
              Lex P _≈_ _<_ Respects₂ Pointwise.Rel _≈_
  respects₂ {P} {_≈_} {_<_} eq resp =
    (λ {xs} {ys} {zs} → resp¹ {xs} {ys} {zs}) ,
    (λ {xs} {ys} {zs} → resp² {xs} {ys} {zs})
    where
    resp¹ : ∀ {xs} → Lex P _≈_ _<_ xs Respects Pointwise.Rel _≈_
    resp¹ []            xs⊴[]            = xs⊴[]
    resp¹ (x≈y ∷ xs≈ys) halt             = halt
    resp¹ (x≈y ∷ xs≈ys) (this z<x)       = this (proj₁ resp x≈y z<x)
    resp¹ (x≈y ∷ xs≈ys) (next z≈x zs⊴xs) =
      next (Eq.trans z≈x x≈y) (resp¹ xs≈ys zs⊴xs)
      where module Eq = IsEquivalence eq

    resp² : ∀ {ys} → flip (Lex P _≈_ _<_) ys Respects Pointwise.Rel _≈_
    resp² []            []⊴ys            = []⊴ys
    resp² (x≈z ∷ xs≈zs) (this x<y)       = this (proj₂ resp x≈z x<y)
    resp² (x≈z ∷ xs≈zs) (next x≈y xs⊴ys) =
      next (Eq.trans (Eq.sym x≈z) x≈y) (resp² xs≈zs xs⊴ys)
      where module Eq = IsEquivalence eq

  decidable : ∀ {P _≈_ _<_} →
              Dec P → Decidable _≈_ → Decidable _<_ →
              Decidable (Lex P _≈_ _<_)
  decidable (yes p) dec-≈ dec-< []       []       = yes (base p)
  decidable (no ¬p) dec-≈ dec-< []       []       = no λ{(base p) → ¬p p}
  decidable dec-P   dec-≈ dec-< []       (y ∷ ys) = yes halt
  decidable dec-P   dec-≈ dec-< (x ∷ xs) []       = no (λ ())
  decidable dec-P   dec-≈ dec-< (x ∷ xs) (y ∷ ys) with dec-< x y
  ... | yes x<y = yes (this x<y)
  ... | no ¬x<y with dec-≈ x y
  ...           | no ¬x≈y = no (¬≤-this ¬x≈y ¬x<y)
  ...           | yes x≈y with decidable dec-P dec-≈ dec-< xs ys
  ...                     | yes xs⊴ys = yes (next x≈y xs⊴ys)
  ...                     | no ¬xs⊴ys = no (¬≤-next ¬x<y ¬xs⊴ys)

  <-decidable :
    ∀ {_≈_ _<_} →
    Decidable _≈_ → Decidable _<_ → Decidable (Lex-< _≈_ _<_)
  <-decidable = decidable (no id)

  ≤-decidable :
    ∀ {_≈_ _<_} →
    Decidable _≈_ → Decidable _<_ → Decidable (Lex-≤ _≈_ _<_)
  ≤-decidable = decidable (yes tt)

  -- Note that trichotomy is an unnecessarily strong precondition for
  -- the following lemma.

  ≤-total :
    ∀ {_≈_ _<_} →
    Symmetric _≈_ → Trichotomous _≈_ _<_ → Total (Lex-≤ _≈_ _<_)
  ≤-total {_≈_} {_<_} sym tri = total
    where
    total : Total (Lex-≤ _≈_ _<_)
    total []       []       = inj₁ (base tt)
    total []       (x ∷ xs) = inj₁ halt
    total (x ∷ xs) []       = inj₂ halt
    total (x ∷ xs) (y ∷ ys) with tri x y
    ... | tri< x<y _ _ = inj₁ (this x<y)
    ... | tri> _ _ y<x = inj₂ (this y<x)
    ... | tri≈ _ x≈y _ with total xs ys
    ...                | inj₁ xs≲ys = inj₁ (next      x≈y  xs≲ys)
    ...                | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)

  <-compare : ∀ {_≈_ _<_} →
              Symmetric _≈_ → Trichotomous _≈_ _<_ →
              Trichotomous (Pointwise.Rel _≈_) (Lex-< _≈_ _<_)
  <-compare {_≈_} {_<_} sym tri = cmp
   where
   cmp : Trichotomous (Pointwise.Rel _≈_) (Lex-< _≈_ _<_)
   cmp []       []       = tri≈ ¬[]<[] [] ¬[]<[]
   cmp []       (y ∷ ys) = tri< halt (λ ()) (λ ())
   cmp (x ∷ xs) []       = tri> (λ ()) (λ ()) halt
   cmp (x ∷ xs) (y ∷ ys) with tri x y
   ... | tri< x<y ¬x≈y ¬y<x =
         tri< (this x<y) (¬x≈y ∘ head) (¬≤-this (¬x≈y ∘ sym) ¬y<x)
   ... | tri> ¬x<y ¬x≈y y<x =
         tri> (¬≤-this ¬x≈y ¬x<y) (¬x≈y ∘ head) (this y<x)
   ... | tri≈ ¬x<y x≈y ¬y<x with cmp xs ys
   ...    | tri< xs<ys ¬xs≈ys ¬ys<xs =
            tri< (next x≈y xs<ys) (¬xs≈ys ∘ tail) (¬≤-next ¬y<x ¬ys<xs)
   ...    | tri≈ ¬xs<ys xs≈ys ¬ys<xs =
            tri≈ (¬≤-next ¬x<y ¬xs<ys) (x≈y ∷ xs≈ys) (¬≤-next ¬y<x ¬ys<xs)
   ...    | tri> ¬xs<ys ¬xs≈ys ys<xs =
            tri> (¬≤-next ¬x<y ¬xs<ys) (¬xs≈ys ∘ tail) (next (sym x≈y) ys<xs)

  -- Some collections of properties which are preserved by Lex-≤ or
  -- Lex-<.

  ≤-isPreorder : ∀ {_≈_ _<_} →
                 IsEquivalence _≈_ → Transitive _<_ → _<_ Respects₂ _≈_ →
                 IsPreorder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _<_)
  ≤-isPreorder {_≈_} {_<_} eq tr resp = record
    { isEquivalence = Pointwise.isEquivalence eq
    ; reflexive     = ≤-reflexive _≈_ _<_
    ; trans         = transitive eq resp tr
    }

  ≤-isPartialOrder : ∀ {_≈_ _<_} →
                     IsStrictPartialOrder _≈_ _<_ →
                     IsPartialOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _<_)
  ≤-isPartialOrder {_≈_} {_<_} spo = record
    { isPreorder = ≤-isPreorder isEquivalence trans <-resp-≈
    ; antisym    = antisymmetric Eq.sym irrefl
                     (trans∧irr⟶asym {_≈_ = _≈_} {_<_ = _<_}
                                     Eq.refl trans irrefl)
    } where open IsStrictPartialOrder spo

  ≤-isTotalOrder : ∀ {_≈_ _<_} →
                   IsStrictTotalOrder _≈_ _<_ →
                   IsTotalOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _<_)
  ≤-isTotalOrder sto = record
    { isPartialOrder =
        ≤-isPartialOrder (record
          { isEquivalence = isEquivalence
          ; irrefl        = tri⟶irr <-resp-≈ Eq.sym compare
          ; trans         = trans
          ; <-resp-≈      = <-resp-≈
          })
    ; total          = ≤-total Eq.sym compare
    } where open IsStrictTotalOrder sto

  ≤-isDecTotalOrder : ∀ {_≈_ _<_} →
                      IsStrictTotalOrder _≈_ _<_ →
                      IsDecTotalOrder (Pointwise.Rel _≈_) (Lex-≤ _≈_ _<_)
  ≤-isDecTotalOrder sto = record
    { isTotalOrder = ≤-isTotalOrder sto
    ; _≟_          = Pointwise.decidable _≟_
    ; _≤?_         = ≤-decidable _≟_ (tri⟶dec< compare)
    } where open IsStrictTotalOrder sto

  <-isStrictPartialOrder
    : ∀ {_≈_ _<_} → IsStrictPartialOrder _≈_ _<_ →
      IsStrictPartialOrder (Pointwise.Rel _≈_) (Lex-< _≈_ _<_)
  <-isStrictPartialOrder spo = record
    { isEquivalence = Pointwise.isEquivalence isEquivalence
    ; irrefl        = <-irreflexive irrefl
    ; trans         = transitive isEquivalence <-resp-≈ trans
    ; <-resp-≈      = respects₂ isEquivalence <-resp-≈
    } where open IsStrictPartialOrder spo

  <-isStrictTotalOrder
    : ∀ {_≈_ _<_} → IsStrictTotalOrder _≈_ _<_ →
      IsStrictTotalOrder (Pointwise.Rel _≈_) (Lex-< _≈_ _<_)
  <-isStrictTotalOrder sto = record
    { isEquivalence = Pointwise.isEquivalence isEquivalence
    ; trans         = transitive isEquivalence <-resp-≈ trans
    ; compare       = <-compare Eq.sym compare
    ; <-resp-≈      = respects₂ isEquivalence <-resp-≈
    } where open IsStrictTotalOrder sto

-- "Packages" (e.g. preorders) can also be handled.

≤-preorder : Preorder _ _ _ → Preorder _ _ _
≤-preorder pre = record
  { isPreorder = ≤-isPreorder isEquivalence trans ∼-resp-≈
  } where open Preorder pre

≤-partialOrder : StrictPartialOrder _ _ _ → Poset _ _ _
≤-partialOrder spo = record
  { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
  } where open StrictPartialOrder spo

≤-decTotalOrder : StrictTotalOrder _ _ _ → DecTotalOrder _ _ _
≤-decTotalOrder sto = record
  { isDecTotalOrder = ≤-isDecTotalOrder isStrictTotalOrder
  } where open StrictTotalOrder sto

<-strictPartialOrder :
  StrictPartialOrder _ _ _ → StrictPartialOrder _ _ _
<-strictPartialOrder spo = record
  { isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
  } where open StrictPartialOrder spo

<-strictTotalOrder : StrictTotalOrder _ _ _ → StrictTotalOrder _ _ _
<-strictTotalOrder sto = record
  { isStrictTotalOrder = <-isStrictTotalOrder isStrictTotalOrder
  } where open StrictTotalOrder sto


text:
open import Relation.Binary.PropositionalEquality

module Experiments.STLCRef
       (funext : ∀ {a b} → Extensionality a b) where

open import Level
open import Data.Nat
open import Data.Unit as Unit
open import Data.List
open import Data.List.Most
open import Data.Product
open import Data.Maybe as Maybe hiding (All)
open import Function as Fun using (case_of_)
import Relation.Binary.PropositionalEquality as PEq
open PEq.≡-Reasoning

data Ty : Set where
  unit : Ty
  arrow : (a b : Ty) → Ty
  ref  : Ty → Ty

open import Experiments.Category (⊑-preorder {A = Ty})

Ctx     = List Ty
StoreTy = List Ty

data Expr (Γ : List Ty) : Ty → Set where
  var : ∀ {t} → t ∈ Γ → Expr Γ t
  ƛ     : ∀ {a b} → Expr (a ∷ Γ) b → Expr Γ (arrow a b)
  app   : ∀ {a b} → Expr Γ (arrow a b) → Expr Γ a → Expr Γ b
  unit  : Expr Γ unit
  ref   : ∀ {t} → Expr Γ t → Expr Γ (ref t)
  !_    : ∀ {t} → Expr Γ (ref t) → Expr Γ t
  _≔_   : ∀ {t} → Expr Γ (ref t) → Expr Γ t → Expr Γ unit

mutual
  Env : (Γ : Ctx)(Σ : StoreTy) → Set
  Env Γ Σ = All (λ t → Val t Σ) Γ

  data Val : Ty → List Ty → Set where
    unit   : ∀ {Σ} → Val unit Σ
    ⟨_,_⟩  : ∀ {Σ Γ a b} → Expr (a ∷ Γ) b → Env Γ Σ → Val (arrow a b) Σ
    loc    : ∀ {Σ t} → t ∈ Σ → Val (ref t) Σ

weaken-all : ∀ {i}{A : Set i}{j}{B : Set j}{xs : List B}
               {k}{C : B → List A → Set k}( wₐ : ∀ {x} {bs cs} → bs ⊑ cs → C x bs → C x cs) →
               ∀ {bs cs} → bs ⊑ cs → All (λ x → C x bs) xs → All (λ x → C x cs) xs
weaken-all wₐ ext x = map-all (λ y → wₐ ext y) x

mutual
  weaken-val  :  ∀ {a : Ty}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Val a Σ → Val a Σ'
  weaken-val ext unit      = unit
  weaken-val ext ⟨ e , E ⟩ = ⟨ e , weaken-env ext E ⟩
  weaken-val ext (loc l)   = loc (∈-⊒ l ext)

  weaken-env  :  ∀ {Γ}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Env Γ Σ → Env Γ Σ'
  weaken-env ext (v ∷ vs)  = weaken-val ext v ∷ weaken-env ext vs
  weaken-env ext []        = []

  -- weaken-env : ∀ {Γ}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Env Γ Σ → Env Γ Σ'
  -- weaken-env ext E = weaken-all weaken-val ext E

import Relation.Binary.HeterogeneousEquality as H

mutual
  clo-cong : ∀ {Γ a t Σ}{e e' : Expr (a ∷ Γ) t}{E E' : Env Γ Σ} →
             e ≡ e' → E ≡ E' → ⟨ e , E ⟩ ≡ ⟨ e' , E' ⟩
  clo-cong refl refl = refl

  mono-val-refl  :  ∀ {t c}{ext : c ⊑ c}(p : Val t c) →
                        weaken-val ext p ≡ p
  mono-val-refl unit      = refl
  mono-val-refl ⟨ e , E ⟩ = clo-cong refl (mono-env-refl E)
  mono-val-refl (loc l)   = {!!}

  mono-env-refl  :  ∀ {Γ c}{ext : c ⊑ c}(p : Env Γ c) →
                        weaken-env ext p ≡ p
  mono-env-refl []       = refl
  mono-env-refl (v ∷ vs) = {!!}

  Val' : Ty → MP₀
  Val' t = mp (Val t)
              (record { monotone = weaken-val ;
                        monotone-refl = mono-val-refl ;
                        monotone-trans = {!!} })

  Env' : List Ty → MP₀
  Env' Γ = mp (Env Γ)
              (record { monotone = weaken-env ;
                        monotone-refl = mono-env-refl ;
                        monotone-trans = {!!} })

open import Experiments.StrongMonad Ty Val' funext

meq' : ∀ {Σ' b}{B : World → Set b}{Γ}{f g : (Σ : World) → Σ' ⊑ Σ → Env' Γ · Σ → Store Σ → B Σ} →
       (∀ Σ → (ext : Σ' ⊑ Σ) → (E : Env' Γ · Σ) → (μ : Store Σ) → f Σ ext E μ ≡ g Σ ext E μ) →
       f ≡ g
meq' p = funext λ Σ → funext λ ext → funext λ E → funext λ μ → p Σ ext E μ

M' : ∀ {ℓ} → List Ty → MP ℓ → MP ℓ
M' Γ P = mp (λ Σ → ∀ Σ₁ → Σ ⊑ Σ₁ → Env' Γ · Σ₁ → Store Σ₁ →
         Maybe (∃ λ Σ₂ → Σ₂ ⊒ Σ₁ × Store Σ₂ × P · Σ₂))
  record {
    monotone = λ w₀ f Σ w₁ E μ → f Σ (⊑-trans w₀ w₁) E μ ;
    monotone-refl = λ f → meq' (λ Σ₁ _ E μ → cong (λ u → f Σ₁ u E μ) ⊑-trans-refl) ;
    monotone-trans = λ f w₀ w₁ → meq' (λ Σ₁ w₂ E μ → cong (λ u → f Σ₁ u E μ) (sym ⊑-trans-assoc))
  }

Const : ∀ (T : Set) → MP₀
Const T = mp (λ _ → T) ((record {
    monotone = λ x x₁ → x₁ ;
    monotone-refl = λ _ → refl ;
    monotone-trans = λ _ _ _ → refl
  }))

-- one : ∀ {Γ} → M' Γ One
-- one = ?

η' : ∀ {Γ}{p}(P : MP p) → P ⇒ M' Γ P
η' P =
  mk⇒
    (λ p Σ ext _ μ → just (Σ , ⊑-refl , μ , MP.monotone P ext p))
    (λ c~c' {p} → begin
      (λ z ext E μ → just (z , ⊑-refl , μ , MP.monotone P ext (MP.monotone P c~c' p)))
        ≡⟨ meq' (λ z ext E μ → cong (λ u → just (z , ⊑-refl , μ , u)) (sym (MP.monotone-trans P p c~c' ext))) ⟩
      (λ z ext E μ → just (z , ⊑-refl , μ , MP.monotone P (⊑-trans c~c' ext) p))
        ≡⟨ refl ⟩
      MP.monotone (M' _ P) c~c' (λ z ext E μ → just (z , ⊑-refl , μ , MP.monotone P ext p))
    ∎)

-- necessary because Agda's unification is shaky for pattern matching
-- lambdas
join : ∀ {l}{a : Set l} → Maybe (Maybe a) → Maybe a
join nothing         = nothing
join (just nothing)  = nothing
join (just (just x)) = just x

μ' : ∀ {Γ}{p}(P : MP p) → M' Γ (M' Γ P) ⇒ M' Γ P
μ' P = mk⇒
  (λ pc Σ₁ ext E μ →
    join (case pc Σ₁ ext E μ of (Maybe.map (λ{
      (Σ₂ , ext₁ , μ₁ , f) →
        case f Σ₂ ⊑-refl (weaken-env ext₁ E) μ₁ of (Maybe.map (λ{
          (Σ₃ , ext₂ , μ₂ , v) →
            Σ₃ , ⊑-trans ext₁ ext₂ , μ₂ , v
        }))
    }))))
  (λ c~c' → refl)

fmap' : ∀ {Γ p q}{P : MP p}{Q : MP q} → (P ⇒ Q) → M' Γ P ⇒ M' Γ Q
fmap' F = mk⇒
  (λ x Σ₁ ext E μ → case x Σ₁ ext E μ of Maybe.map (λ{
    (Σ₂ , ext₁ , μ₁ , v) → Σ₂ , ext₁ , μ₁ , apply F v
  }))
  (λ c~c' → refl)

bind' : ∀ {p q}{P : MP p}{Q : MP q}{Γ} → (P ⇒ M' Γ Q) → M' Γ P ⇒ M' Γ Q
bind' {Q = Q} F = μ' Q ∘ fmap' F

-- mbind : ∀ {p q}{P : MP p}{Q : MP q}{Γ Σ} →
--         M' Γ P · Σ →
--         (∀ {Σ'} → P · Σ' → M' Γ Q · Σ') → M' Γ Q · Σ
-- mbind f g Σ ext E μ =
--   case (f Σ ext E μ) of (λ{
--     nothing → nothing
--   ; (just (Σ₁ , ext₁ , μ₁ , v)) →
--     bind'
--     case g v Σ₁ ⊑-refl (weaken-env ext₁ E) μ₁ of (λ{
--       nothing → nothing
--     ; (just (Σ₂ , ext₂ , μ₂ , v')) →
--       just (Σ₂ , ⊑-trans ext₁ ext₂ , μ₂ , v')
--     })
--   })

mbind : ∀ {p q}{P : MP p}{Q : MP q}{Γ Σ} →
        M' Γ P · Σ → (P ⇒ M' Γ Q) → M' Γ Q · Σ
mbind {_} {_} {P} {Q} f g =
  apply (bind' {_} {_} {P} {Q} g) f

return : ∀ {p}{P : MP p}{Γ Σ} → P · Σ → M' Γ P · Σ
return {_} {P} p = apply (η' P) p

timeout  : ∀ {P Q : MP₀}{Γ} → P ⇒ M' Γ Q
timeout = mk⇒ (λ _ _ _ _ _ → nothing) (λ _ → refl)

getEnv  :  ∀ {Γ Σ} → M' Γ (Env' Γ) · Σ
getEnv {Γ} Σ ext E μ = (return {_} {Env' Γ} E) Σ ⊑-refl E μ

setEnv : ∀ {P : MP₀}{Γ Γ' Σ} → Env' Γ' · Σ → M' Γ' P · Σ → M' Γ P · Σ
setEnv E f Σ ext _ = f Σ ext (weaken-env ext E)

open Product

strength : ∀ {Γ}{Q P : MP₀} → Q ⊗ M' Γ P ⇒ M' Γ (Q ⊗ P)
strength {_} {Q} =
  mk⇒ (λ p Σ ext E μ →
         case p of λ{
           (x , y) →
             case y Σ ext E μ of Maybe.map (λ{
               (Σ₁ , ext₁ , μ₁ , v) →
                 (Σ₁ , ext₁ , μ₁ , (MP.monotone Q (⊑-trans ext ext₁) x , v))
             })})
      (λ c~c' → {!!})

-- eval : ℕ → ∀ {Γ t} → Const (Expr Γ t) ⇒ M' Γ (Val' t)
-- eval zero    = timeout {_} {Val' _}
-- eval (suc k) =
--   mk⇒ (λ{ unit →
--           return {_} {Val' unit} unit
--         ; (var x) →
--           (mbind {_} {_} {Env' _} {Val' _}
--                  getEnv
--                  (mk⇒
--                    (λ E →
--                       return {_} {Val' _} (lookup E x))
--                    (λ c~c' → {- ugh -} {!!})))
--         ; (app {a} {b} e1 e2) →
--           (mbind {_} {_} {Val' (arrow a b)} {Val' b}
--                  (apply (eval k) e1)
--                  (mk⇒ (λ{ (⟨_,_⟩ {_} {Γ} e E) →
--                           (mbind {_} {_} {Env' Γ ⊗ Val' a} {Val' b}
--                                  (apply (strength {_} {Env' Γ} {Val' a}) (E , apply (eval k) e2))
--                                  (mk⇒
--                                    (λ{ (E' , v) →
--                                        setEnv {Val' b} (v ∷ E')
--                                               (apply (eval k) e) })
--                                    (λ c~c' → {!!})))
--                                   })
--                       λ c~c' → {!!} ))

--         ; _ → {!!} })
--       (λ c~c' → {!!})

eval : ℕ → ∀ {Γ t} → Const (Expr Γ t) ⇒ M' Γ (Val' t)
eval zero    = timeout {_} {Val' _}
eval (suc k) =
  mk⇒ (λ{ unit →
          apply (η' (Val' unit)) unit
        ; (var x) →
          apply (bind' {_} {_} {Env' _} {Val' _}
                       (mk⇒ (λ E →
                               apply (η' (Val' _)) (lookup E x))
                            (λ c~c' → {- ugh -} {!!})))
                getEnv
        ; (app {a} {b} e1 e2) →
          apply (bind' {_} {_} {Val' (arrow a b)} {Val' b}
                       (mk⇒ (λ{ (⟨_,_⟩ {_} {Γ} e E) →
                                apply (bind' {_} {_} {Env' Γ ⊗ Val' a} {Val' b}
                                             (mk⇒
                                               (λ{ (E' , v) →
                                                   setEnv {Val' b} (v ∷ E')
                                                          (apply (eval k) e) })
                                               (λ c~c' → {!!})))
                                      (apply (strength {_} {Env' Γ} {Val' a}) (E , apply (eval k) e2)) })
                            λ c~c' → {!!} ))
                (apply (eval k) e1)
        ; _ → {!!} })
      (λ c~c' → {!!})


text:
module BTree.Heap {A : Set}(_≤_ : A → A → Set) where

open import BTree {A}

data Heap : BTree → Set where
  leaf : Heap leaf
  single : (x : A)
                   → Heap (node x leaf leaf)
  left : {l r : BTree}{x y : A}
                   → x ≤ y
                   → Heap (node y l r)
                   → Heap (node x (node y l r) leaf)
  right : {l r : BTree}{x y : A}
                   → x ≤ y
                   → Heap (node y l r)
                   → Heap (node x leaf (node y l r))
  both : {l r l' r' : BTree}{x y y' : A}
                   → x ≤ y
                   → x ≤ y'
                   → Heap (node y l r)
                   → Heap (node y' l' r')
                   → Heap (node x (node y l r) (node y' l' r'))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax PropLog | PR

type
  * : 0-ary

term
  false : * | ⊥
  or    : *  *  ->  * | _∨_ l20
  true  : * | ⊤
  and   : *  *  ->  * | _∧_ l30
  not   : *  ->  * | ¬_ r50

theory
  (⊥U∨ᴸ) a |> or (false, a) = a
  (⊥U∨ᴿ) a |> or (a, false) = a
  (∨A) a b c |> or (or(a, b), c) = or (a, or(b, c))
  (∨C) a b |> or(a, b) = or(b, a)
  (⊤U∧ᴸ) a |> and (true, a) = a
  (⊤U∧ᴿ) a |> and (a, true) = a
  (∧A) a b c |> and (and(a, b), c) = and (a, and(b, c))
  (∧D∨ᴸ) a b c |> and (a, or (b, c)) = or (and(a, b), and(a, c))
  (∧D∨ᴿ) a b c |> and (or (a, b), c) = or (and(a, c), and(b, c))
  (⊥X∧ᴸ) a |> and (false, a) = false
  (⊥X∧ᴿ) a |> and (a, false) = false
  (¬N∨ᴸ) a |> or (not (a), a) = false
  (¬N∨ᴿ) a |> or (a, not (a)) = false
  (∧C) a b |> and(a, b) = and(b, a)
  (∨I) a |> or(a, a) = a
  (∧I) a |> and(a, a) = a
  (¬²) a |> not(not (a)) = a
  (∨D∧ᴸ) a b c |> or (a, and (b, c)) = and (or(a, b), or(a, c))
  (∨D∧ᴿ) a b c |> or (and (a, b), c) = and (or(a, c), or(b, c))
  (∨B∧ᴸ) a b |> or (and (a, b), a) = a
  (∨B∧ᴿ) a b |> or (a, and (a, b)) = a
  (∧B∨ᴸ) a b |> and (or (a, b), a) = a
  (∧B∨ᴿ) a b |> and (a, or (a, b)) = a
  (⊤X∨ᴸ) a |> or (true, a) = true
  (⊤X∨ᴿ) a |> or (a, true) = true
  (¬N∧ᴸ) a |> and (not (a), a) = false
  (¬N∧ᴿ) a |> and (a, not (a)) = false
  (DM∧) a b |> not (and (a, b)) = or  (not(a), not(b))
  (DM∨) a b |> not (or  (a, b)) = and (not(a), not(b))
-}

module PropLog.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import PropLog.Signature
open import PropLog.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution PR:Syn
open import SOAS.Metatheory.SecondOrder.Equality PR:Syn

private
  variable
    α β γ τ : *T
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ PR) α Γ → (𝔐 ▷ PR) α Γ → Set where
  ⊥U∨ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ⊥ ∨ 𝔞 ≋ₐ 𝔞
  ∨A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ∨ 𝔟) ∨ 𝔠 ≋ₐ 𝔞 ∨ (𝔟 ∨ 𝔠)
  ∨C   : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢       𝔞 ∨ 𝔟 ≋ₐ 𝔟 ∨ 𝔞
  ⊤U∧ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ⊤ ∧ 𝔞 ≋ₐ 𝔞
  ∧A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ∧ 𝔟) ∧ 𝔠 ≋ₐ 𝔞 ∧ (𝔟 ∧ 𝔠)
  ∧D∨ᴸ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ (𝔟 ∨ 𝔠) ≋ₐ (𝔞 ∧ 𝔟) ∨ (𝔞 ∧ 𝔠)
  ⊥X∧ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ⊥ ∧ 𝔞 ≋ₐ ⊥
  ¬N∨ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢   (¬ 𝔞) ∨ 𝔞 ≋ₐ ⊥
  ∧C   : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢       𝔞 ∧ 𝔟 ≋ₐ 𝔟 ∧ 𝔞
  ∨I   : ⁅ * ⁆̣             ▹ ∅ ⊢       𝔞 ∨ 𝔞 ≋ₐ 𝔞
  ∧I   : ⁅ * ⁆̣             ▹ ∅ ⊢       𝔞 ∧ 𝔞 ≋ₐ 𝔞
  ¬²   : ⁅ * ⁆̣             ▹ ∅ ⊢     ¬ (¬ 𝔞) ≋ₐ 𝔞
  ∨D∧ᴸ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ (𝔟 ∧ 𝔠) ≋ₐ (𝔞 ∨ 𝔟) ∧ (𝔞 ∨ 𝔠)
  ∨B∧ᴸ : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢ (𝔞 ∧ 𝔟) ∨ 𝔞 ≋ₐ 𝔞
  ∧B∨ᴸ : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢ (𝔞 ∨ 𝔟) ∧ 𝔞 ≋ₐ 𝔞
  ⊤X∨ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢       ⊤ ∨ 𝔞 ≋ₐ ⊤
  ¬N∧ᴸ : ⁅ * ⁆̣             ▹ ∅ ⊢   (¬ 𝔞) ∧ 𝔞 ≋ₐ ⊥
  DM∧  : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢   ¬ (𝔞 ∧ 𝔟) ≋ₐ (¬ 𝔞) ∨ (¬ 𝔟)
  DM∨  : ⁅ * ⁆ ⁅ * ⁆̣       ▹ ∅ ⊢   ¬ (𝔞 ∨ 𝔟) ≋ₐ (¬ 𝔞) ∧ (¬ 𝔟)

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

-- Derived equations
⊥U∨ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ ⊥ ≋ 𝔞
⊥U∨ᴿ = tr (ax ∨C with《 𝔞 ◃ ⊥ 》) (ax ⊥U∨ᴸ with《 𝔞 》)
⊤U∧ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ ⊤ ≋ 𝔞
⊤U∧ᴿ = tr (ax ∧C with《 𝔞 ◃ ⊤ 》) (ax ⊤U∧ᴸ with《 𝔞 》)
∧D∨ᴿ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ∨ 𝔟) ∧ 𝔠 ≋ (𝔞 ∧ 𝔠) ∨ (𝔟 ∧ 𝔠)
∧D∨ᴿ = begin
  (𝔞 ∨ 𝔟) ∧ 𝔠       ≋⟨ ax ∧C with《 𝔞 ∨ 𝔟 ◃ 𝔠 》 ⟩
  𝔠 ∧ (𝔞 ∨ 𝔟)       ≋⟨ ax ∧D∨ᴸ with《 𝔠 ◃ 𝔞 ◃ 𝔟 》 ⟩
  (𝔠 ∧ 𝔞) ∨ (𝔠 ∧ 𝔟)  ≋⟨ cong₂[ ax ∧C with《 𝔠 ◃ 𝔞 》 ][ ax ∧C with《 𝔠 ◃ 𝔟 》 ]inside ◌ᵈ ∨ ◌ᵉ ⟩
  (𝔞 ∧ 𝔠) ∨ (𝔟 ∧ 𝔠)  ∎
⊥X∧ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ ⊥ ≋ ⊥
⊥X∧ᴿ = tr (ax ∧C with《 𝔞 ◃ ⊥ 》) (ax ⊥X∧ᴸ with《 𝔞 》)
¬N∨ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ (¬ 𝔞) ≋ ⊥
¬N∨ᴿ = tr (ax ∨C with《 𝔞 ◃ (¬ 𝔞) 》) (ax ¬N∨ᴸ with《 𝔞 》)
∨D∧ᴿ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ∧ 𝔟) ∨ 𝔠 ≋ (𝔞 ∨ 𝔠) ∧ (𝔟 ∨ 𝔠)
∨D∧ᴿ = begin
  (𝔞 ∧ 𝔟) ∨ 𝔠       ≋⟨ ax ∨C with《 𝔞 ∧ 𝔟 ◃ 𝔠 》 ⟩
  𝔠 ∨ (𝔞 ∧ 𝔟)       ≋⟨ ax ∨D∧ᴸ with《 𝔠 ◃ 𝔞 ◃ 𝔟 》 ⟩
  (𝔠 ∨ 𝔞) ∧ (𝔠 ∨ 𝔟)  ≋⟨ cong₂[ ax ∨C with《 𝔠 ◃ 𝔞 》 ][ ax ∨C with《 𝔠 ◃ 𝔟 》 ]inside ◌ᵈ ∧ ◌ᵉ ⟩
  (𝔞 ∨ 𝔠) ∧ (𝔟 ∨ 𝔠)  ∎
∨B∧ᴿ : ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ (𝔞 ∧ 𝔟) ≋ 𝔞
∨B∧ᴿ = tr (ax ∨C with《 𝔞 ◃ (𝔞 ∧ 𝔟) 》) (ax ∨B∧ᴸ with《 𝔞 ◃ 𝔟 》)
∧B∨ᴿ : ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ (𝔞 ∨ 𝔟) ≋ 𝔞
∧B∨ᴿ = tr (ax ∧C with《 𝔞 ◃ (𝔞 ∨ 𝔟) 》) (ax ∧B∨ᴸ with《 𝔞 ◃ 𝔟 》)
⊤X∨ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∨ ⊤ ≋ ⊤
⊤X∨ᴿ = tr (ax ∨C with《 𝔞 ◃ ⊤ 》) (ax ⊤X∨ᴸ with《 𝔞 》)
¬N∧ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ∧ (¬ 𝔞) ≋ ⊥
¬N∧ᴿ = tr (ax ∧C with《 𝔞 ◃ (¬ 𝔞) 》) (ax ¬N∧ᴸ with《 𝔞 》)

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

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

import      LibraBFT.Impl.Types.LedgerInfoWithSignatures as LedgerInfoWithSignatures
open import LibraBFT.ImplShared.Consensus.Types
open import Util.PKCS

module LibraBFT.Impl.Types.CryptoProxies where

addToLi : AccountAddress → Signature → LedgerInfoWithSignatures → LedgerInfoWithSignatures
addToLi = LedgerInfoWithSignatures.addSignature


text:
module cfg where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat  hiding ( _≟_ )
open import Data.Fin
open import Data.Product
open import Data.List
open import Data.Maybe
open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
-- open import Data.String

data IsTerm (Token : Set) : Set (succ Zero) where
    isTerm :  Token → IsTerm Token
    noTerm  : IsTerm Token

record CFGGrammer  (Token Node : Set) : Set (succ Zero) where
   field
      cfg : Node → List ( List ( Node ) )
      cfgtop : Node
      term? :  Node → IsTerm Token
      tokensz : ℕ
      tokenid : Token → Fin tokensz

open CFGGrammer

-----------------
--
-- CGF language
--
-----------------

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] ∧ y []
split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

cfg-language0 :  {Node  Token : Set} → CFGGrammer  Token Node  → List (List Node ) →  List Token → Bool

{-# TERMINATING #-}
cfg-language2 :  {Node  Token : Set} → CFGGrammer  Token Node  → Node →  List Token → Bool
cfg-language2 cg _ [] = false
cfg-language2 cg x (h1  ∷ [] ) with term? cg x
cfg-language2 cg x (h1 ∷ []) | isTerm t with tokenid cg h1 ≟ tokenid cg t
cfg-language2 cg x (h1 ∷ []) | isTerm t | yes p = true
cfg-language2 cg x (h1 ∷ []) | isTerm t | no ¬p = false
cfg-language2 cg x (h1 ∷ []) | noTerm = cfg-language0 cg (cfg cg x) ( h1 ∷ [] )
cfg-language2 cg x In with term? cg x
cfg-language2 cg x In | isTerm t = false
cfg-language2 cg x In | noTerm =  cfg-language0 cg (cfg cg x ) In

cfg-language1 :  {Node  Token : Set} → CFGGrammer  Token Node  → List Node →  List Token → Bool
cfg-language1 cg [] [] = true
cfg-language1 cg [] _ = false
cfg-language1 cg (node ∷ T) = split ( cfg-language2 cg node ) ( cfg-language1 cg T )

cfg-language0 cg [] [] = true
cfg-language0 cg [] _ = false
cfg-language0 cg (node ∷ T) In = cfg-language1 cg node In ∨ cfg-language0 cg T In

cfg-language :  {Node  Token : Set} → CFGGrammer  Token Node  →  List Token → Bool
cfg-language cg = cfg-language0 cg (cfg cg (cfgtop cg))

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

data IFToken : Set where
   t:EA : IFToken
   t:EB : IFToken
   t:EC : IFToken
   t:IF : IFToken
   t:THEN : IFToken
   t:ELSE : IFToken
   t:SA : IFToken
   t:SB : IFToken
   t:SC : IFToken

IFtokenid : IFToken → Fin 9
IFtokenid t:EA = # 0
IFtokenid t:EB = # 1
IFtokenid t:EC = # 2
IFtokenid t:IF = # 3
IFtokenid t:THEN = # 4
IFtokenid t:ELSE = # 5
IFtokenid t:SA = # 6
IFtokenid t:SB = # 7
IFtokenid t:SC = # 8

data IFNode (T : Set) : Set where
   Token : T → IFNode T
   expr : IFNode T
   statement : IFNode T

IFGrammer : CFGGrammer IFToken (IFNode IFToken)
IFGrammer = record {
      cfg = cfg'
    ; cfgtop = statement
    ; term? = term?'
    ; tokensz = 9
    ; tokenid = IFtokenid
   } where
     term?' : IFNode IFToken → IsTerm IFToken
     term?' (Token x) = isTerm x
     term?' _ = noTerm
     cfg' :  IFNode IFToken → List ( List (IFNode IFToken) )
     cfg' (Token t) = ( (Token t)  ∷ [] ) ∷ []
     cfg' expr  =  ( Token t:EA  ∷ [] )  ∷
                  ( Token t:EB  ∷ [] )  ∷
                  ( Token t:EC  ∷ [] )  ∷ []
     cfg' statement = ( Token t:SA   ∷ [] ) ∷
                     ( Token t:SB   ∷ [] ) ∷
                     ( Token t:SC   ∷ [] ) ∷
                     ( Token t:IF ∷ expr ∷ statement ∷ [] ) ∷
                     ( Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ [] ) ∷  []

cfgtest1 = cfg-language IFGrammer (  t:SA ∷ [] )

cfgtest2 = cfg-language2 IFGrammer (Token t:SA) (  t:SA ∷ [] )

cfgtest3 = cfg-language1 IFGrammer (Token t:SA  ∷ []  ) (  t:SA ∷ [] )

cfgtest4 = cfg-language IFGrammer  (t:IF  ∷ t:EA ∷ t:SA ∷ [] )

cfgtest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF  ∷ t:EA ∷ t:EA ∷ [] )
cfgtest6 = cfg-language2 IFGrammer statement (t:IF  ∷ t:EA ∷ t:SA ∷ [] )
cfgtest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE  ∷ statement  ∷ []) (t:IF  ∷ t:EA ∷ t:SA ∷ t:ELSE  ∷ t:SB  ∷ [] )

cfgtest8 = cfg-language IFGrammer  (t:IF  ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE  ∷ t:SB  ∷ [] )

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


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

module Data.Sum where

open import Level
open import Cubical.Data.Sum using (_⊎_; inl; inr) public
open import Data.Bool using (Bool; true; false)
open import Function using (const)

either : ∀ {ℓ} {C : A ⊎ B → Type ℓ} →  ((a : A) → C (inl a)) → ((b : B) → C (inr b))
        → (x : A ⊎ B) → C x
either f _ (inl x) = f x
either _ g (inr y) = g y

⟦l_,r_⟧ = either

either′ : (A → C) → (B → C) → (A ⊎ B) → C
either′ = either

is-l : A ⊎ B → Bool
is-l = either′ (const true) (const false)

map-⊎ : ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂} {B₁ : Type b₁} {B₂ : Type b₂} →
      (A₁ → A₂) →
      (B₁ → B₂) →
      (A₁ ⊎ B₁) →
      (A₂ ⊎ B₂)
map-⊎ f g (inl x) = inl (f x)
map-⊎ f g (inr x) = inr (g x)

mapˡ : (A → B) → A ⊎ C → B ⊎ C
mapˡ f (inl x) = inl (f x)
mapˡ f (inr x) = inr x

mapʳ : (A → B) → C ⊎ A → C ⊎ B
mapʳ f (inl x) = inl x
mapʳ f (inr x) = inr (f x)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Sigma
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

infixr 0 _$_
_$_ : ∀ {a b}{A : Set a}{B : Set b} → (A → B) → (A → B)
f $ x = f x

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

reverseAcc : {A : Set} → List A → List A → List A
reverseAcc [] ys = ys
reverseAcc (x ∷ xs) ys = reverseAcc xs (x ∷ ys)

reverse : {A : Set} → List A → List A
reverse xs = reverseAcc xs []

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

macro
  ntest : Name → Term → TC ⊤
  ntest f a = do
     (function te@(clause tel _ t ∷ [])) ← withReconstructed $ getDefinition f where
        _ → typeError $ strErr "ERROR" ∷ []
     t ← withReconstructed $ inContext (reverse tel) $ normalise t
     quoteTC t >>= unify a

-- A record with parameters.
record X {n} (x : Vec Nat n) : Set where
  constructor mk
  field
    c : Nat

-- A function that we will call at the unknown argument position
-- when defining the type of `f`.
[_] : ∀ {X} → X → Vec X 1
[ x ] = x ∷ []

-- The function that has two reconstructable arguments in the body.
f : X [ 1 ]
f = mk 1

-- Normalisation of the body of the function should also
-- normalise reconstructed arguments.
test : ntest f ≡ con (quote mk) (_ ∷ arg _ (con (quote Vec._∷_) _) ∷ _)
test = refl