text:
module STLC2 where

open import Data.Nat
-- open import Data.List
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; subst)
open import Relation.Nullary
open import Data.Product

-- de Bruijn indexed lambda calculus
infix  5 ƛ_
infixl 7 _∙_
infix  9 var_
data Term : Set where
  var_ : ℕ → Term

  ƛ_ : Term → Term

  _∙_ : Term → Term → Term

-- only "shift" the variable when
--  1. it's free
--  2. it will be captured after substitution
--  free <= x && x < subst-depth
shift : ℕ → ℕ → Term → Term
shift free subst-depth (var x) with free >? x
shift free subst-depth (var x) | yes p = var x                -- bound
shift free subst-depth (var x) | no ¬p with subst-depth >? x  -- free
shift free subst-depth (var x) | no ¬p | yes q = var (suc x)  -- will be captured, should increment
shift free subst-depth (var x) | no ¬p | no ¬q = var x
shift free subst-depth (ƛ M)   = ƛ (shift (suc free) (suc subst-depth) M)
shift free subst-depth (M ∙ N) = shift free subst-depth M ∙ shift free subst-depth N

infixl 10 _[_/_]
_[_/_] : Term → Term → ℕ → Term
(var x)   [ N / n ] with x ≟ n
(var x)   [ N / n ] | yes p = N
(var x)   [ N / n ] | no ¬p = var x
(ƛ M)     [ N / n ] = ƛ ((M [ shift 0 (suc n) N / suc n ]))
(L ∙ M)   [ N / n ] = L [ N / n ] ∙ M [ N / n ]

-- substitution
infixl 10 _[_]
_[_] : Term → Term → Term
M [ N ] = M [ N / zero ]

-- β reduction
infix 3 _β→_
data _β→_ : Term → Term → Set where

  β-ƛ-∙ : ∀ {M N} → ((ƛ M) ∙ N) β→ (M [ N ])

  β-ƛ : ∀ {M N} → M β→ N → ƛ M β→ ƛ N

  β-∙-l : ∀ {L M N} → M β→ N → M ∙ L β→ N ∙ L

  β-∙-r : ∀ {L M N} → M β→ N → L ∙ M β→ L ∙ N

-- the reflexive and transitive closure of _β→_
infix  2 _β→*_
infixr 2 _→*_
data _β→*_ : Term → Term → Set where

  ∎ : ∀ {M} → M β→* M

  _→*_
    : ∀ {L M N}
    → L β→ M
    → M β→* N
    --------------
    → L β→* N

infixl  3 _<β>_
_<β>_ : ∀ {M N O} → M β→* N → N β→* O → M β→* O
_<β>_ {M} {.M} {O} ∎            N→O = N→O
_<β>_ {M} {N}  {O} (L→M →* M→N) N→O = L→M →* M→N <β> N→O

-- infix  2 _-↠_

infixr 2 _→⟨_⟩_
_→⟨_⟩_
  : ∀ {M N}
  → ∀ L
  → L β→ M
  → M β→* N
  --------------
  → L β→* N
L →⟨ P ⟩ Q = P →* Q

infixr 2 _→*⟨_⟩_
_→*⟨_⟩_
  : ∀ {M N}
  → ∀ L
  → L β→* M
  → M β→* N
  --------------
  → L β→* N
L →*⟨ P ⟩ Q = P <β> Q

infix 3 _→∎
_→∎ : ∀ M → M β→* M
M →∎ = ∎

jump : ∀ {M N} → M β→ N → M β→* N
jump {M} {N} M→N = M→N →* ∎

-- the symmetric closure of _β→*_

infix  1 _β≡_
data _β≡_ : Term → Term → Set where
  β-sym : ∀ {M N}
    → M β→* N
    → N β→* M
    -------
    → M β≡ N

infixr 2 _=*⟨_⟩_
_=*⟨_⟩_
  : ∀ {M N}
  → ∀ L
  → L β≡ M
  → M β≡ N
  --------------
  → L β≡ N
L =*⟨ β-sym A B ⟩ β-sym C D = β-sym (A <β> C) (D <β> B)

infixr 2 _=*⟨⟩_
_=*⟨⟩_
  : ∀ {N}
  → ∀ L
  → L β≡ N
  --------------
  → L β≡ N
L =*⟨⟩ β-sym C D = β-sym C D

infix 3 _=∎
_=∎ : ∀ M → M β≡ M
M =∎ = β-sym ∎ ∎

forward : ∀ {M N} → M β≡ N → M β→* N
forward (β-sym A _) = A

backward : ∀ {M N} → M β≡ N → N β→* M
backward (β-sym _ B) = B

-- data Normal : Set where

Normal : Term → Set
Normal M = ¬ ∃ (λ N → M β→ N)

normal : ∀ {M N} → Normal M → M β→* N → M ≡ N
normal P ∎            = refl
normal P (M→L →* L→N) = ⊥-elim (P (_ , M→L))

normal-ƛ : ∀ {M} → Normal (ƛ M) → Normal M
normal-ƛ P (N , M→N) = P ((ƛ N) , (β-ƛ M→N))

normal-ƛ' : ∀ {M} → Normal M → Normal (ƛ M)
normal-ƛ' P (.(ƛ N) , β-ƛ {N = N} ƛM→N) = P (N , ƛM→N)

normal-∙-r : ∀ {M N} → Normal (M ∙ N) → Normal N
normal-∙-r {M} P (O , N→O) = P (M ∙ O , (β-∙-r N→O))

normal-∙-l : ∀ {M N} → Normal (M ∙ N) → Normal M
normal-∙-l {_} {N} P (O , M→O) = P (O ∙ N , (β-∙-l M→O))

cong-ƛ : ∀ {M N} → M β→* N → ƛ M β→* ƛ N
cong-ƛ ∎            = ∎
cong-ƛ (M→N →* N→O) = β-ƛ M→N →* cong-ƛ N→O

cong-∙-l : ∀ {L M N} → M β→* N → M ∙ L β→* N ∙ L
cong-∙-l ∎            = ∎
cong-∙-l (M→N →* N→O) = β-∙-l M→N →* cong-∙-l N→O

cong-∙-r : ∀ {L M N} → M β→* N → L ∙ M β→* L ∙ N
cong-∙-r ∎            = ∎
cong-∙-r (M→N →* N→O) = β-∙-r M→N →* cong-∙-r N→O

∙-dist-r : ∀ M N O → (ƛ (M ∙ N)) ∙ O β→* ((ƛ M) ∙ O) ∙ ((ƛ N) ∙ O)
∙-dist-r (var x) N O = {!   !}
∙-dist-r (ƛ M) N O = {!   !}
∙-dist-r (M ∙ L) N O = {!   !}

∙-dist-r2 : ∀ M N O → (ƛ (M ∙ N)) ∙ O β≡ ((ƛ M) ∙ O) ∙ ((ƛ N) ∙ O)
∙-dist-r2 (var x) N O = {!   !}
∙-dist-r2 (ƛ M) N O = {!   !}
∙-dist-r2 (M ∙ L) (var x) O =
    (ƛ (M ∙ L ∙ var x)) ∙ O
  =*⟨ β-sym (β-ƛ-∙ →* ∎) {!   !} ⟩
    ((M ∙ L ∙ var x) [ O ])
  =*⟨ {!   !} ⟩
    {!   !}
  =*⟨ {!   !} ⟩
    (ƛ M ∙ L) ∙ O ∙ ((ƛ var x) ∙ O)
  =∎
∙-dist-r2 (M ∙ L) (ƛ N) O = {!   !}
∙-dist-r2 (M ∙ L) (N ∙ K) O = {!   !}

  --   {!   !}
  -- →*⟨ {!   !} ⟩
  --   {!   !}
  -- →*⟨ {!   !} ⟩
  --   {!   !}
  -- →*⟨ {!   !} ⟩
  --   {!   !}
  -- →*⟨ {!   !} ⟩
  --   {!   !}
  -- →∎

-- (ƛ M)     [ N / n ] = ƛ ((M [ shift 0 (suc n) N / suc n ]))

cong-[]2 : ∀ {M N L n} → M β→ N → (M [ L / n ]) β→* (N [ L / n ])
cong-[]2 (β-ƛ-∙ {var x} {N}) = {!   !}
cong-[]2 {_} {_} {L} {n} (β-ƛ-∙ {ƛ M} {N}) =
    (ƛ (ƛ (M [ shift 0 (suc (suc n)) (shift 0 (suc n) L) / suc (suc n) ]))) ∙ (N [ L / n ])
  →*⟨ jump β-ƛ-∙ ⟩
    ƛ ((M [ shift 0 (suc (suc n)) (shift 0 (suc n) L) / suc (suc n) ]) [ shift 0 1 (N [ L / n ]) / 1 ])
  →*⟨  cong-ƛ {!  !} ⟩
    ƛ {!   !}
  →*⟨ {!   !} ⟩
    {!   !}
  →*⟨ {!   !} ⟩
    ƛ ((M [ shift 0 1 N / 1 ]) [ shift 0 (suc n) L / suc n ])
  →∎
cong-[]2 {_} {_} {L} {n} (β-ƛ-∙ {M ∙ K} {N}) =
    (ƛ (M [ shift 0 (suc n) L / suc n ]) ∙ (K [ shift 0 (suc n) L / suc n ])) ∙ (N [ L / n ])
  →*⟨ {!   !} ⟩
  -- →*⟨ forward (∙-dist-r2 (M [ shift zero (suc n) L / suc n ]) (K [ shift zero (suc n) L / suc n ]) (N [ L / n ])) ⟩
    (ƛ (M [ shift zero (suc n) L / suc n ])) ∙ (N [ L / n ]) ∙ ((ƛ (K [ shift 0 (suc n) L / suc n ])) ∙ (N [ L / n ]))
  →*⟨ cong-∙-l (cong-[]2 (β-ƛ-∙ {M} {N})) ⟩
    ((M [ N ]) [ L / n ]) ∙ ((ƛ (K [ shift 0 (suc n) L / suc n ])) ∙ (N [ L / n ]))
  →*⟨ cong-∙-r (cong-[]2 (β-ƛ-∙ {K} {N})) ⟩
    ((M [ N ]) [ L / n ]) ∙ ((K [ N ]) [ L / n ])
  →∎
cong-[]2 (β-ƛ M→N) = cong-ƛ (cong-[]2 M→N)
cong-[]2 (β-∙-l M→N) = cong-∙-l (cong-[]2 M→N)
cong-[]2 (β-∙-r M→N) = cong-∙-r (cong-[]2 M→N)

cong-∙-l' : ∀ {L M N} → M β→* N → M ∙ L ≡ N ∙ L
cong-∙-l' ∎                = refl
cong-∙-l' {L} {M} {O} (_→*_ {M = N} M→N N→O) = trans M∙L≡N∙L N∙L≡O∙L
  where
    M∙L≡N∙L : M ∙ L ≡ N ∙ L
    M∙L≡N∙L = {!   !}

    N∙L≡O∙L : N ∙ L ≡ O ∙ L
    N∙L≡O∙L = cong-∙-l' N→O
  -- rans (cong-∙-l' (M→N →* ∎)) (cong-∙-l' N→O)

cong-[] : ∀ {M N L n} → M β→ N → (M [ L / n ]) ≡ (N [ L / n ])
cong-[] β-ƛ-∙ = {!   !}
cong-[] (β-ƛ M→N) = {!   !}
cong-[] (β-∙-l M→N) = cong-∙-l' {! cong-[] M→N  !}
cong-[] (β-∙-r M→N) = {!   !}

normal-unique' : ∀ {M N O} → Normal N → Normal O → M β→ N → M β→ O → N ≡ O
normal-unique' P Q β-ƛ-∙ β-ƛ-∙ = refl
normal-unique' P Q (β-ƛ-∙ {M} {L}) (β-∙-l {N = .(ƛ N)} (β-ƛ {N = N} M→N)) = {!   !}
  -- trans (normal P (cong-[]2 M→N)) N[L]≡ƛN∙L
  -- trans (normal P (cong-[]2 M→N)) N[L]≡ƛN∙L
  where
    N[L]≡ƛN∙L : (N [ L ]) ≡ (ƛ N) ∙ L
    N[L]≡ƛN∙L = sym (normal Q (jump β-ƛ-∙))
-- β-ƛ-∙ : ∀ {M N} → ((ƛ M) ∙ N) β→ (M [ N ])
normal-unique' P Q (β-ƛ-∙ {M} {L}) (β-∙-r {N = N} L→N) = {!  sym (normal Q (jump β-ƛ-∙)) !}
  -- sym (trans (normal Q (jump β-ƛ-∙)) (cong (λ x → M [ x ]) (sym (normal {!   !} (jump N→O)))))
  -- sym (trans (normal Q (jump β-ƛ-∙)) (cong (λ x → {! M [ x ]  !}) {!   !}))
  -- sym (trans {!   !} (normal {! P  !} (jump β-ƛ-∙)))
normal-unique' P Q (β-ƛ M→N) (β-ƛ M→O) = cong ƛ_ (normal-unique' (normal-ƛ P) (normal-ƛ Q) M→N M→O)
normal-unique' P Q (β-∙-l M→N) β-ƛ-∙ = {!normal (normal-∙-l P) !}
normal-unique' P Q (β-∙-l {L} {N = N} M→N) (β-∙-l {N = O} M→O) =
  cong (λ x → x ∙ L) (normal-unique' (normal-∙-l P) (normal-∙-l Q) M→N M→O)
normal-unique' P Q (β-∙-l M→N) (β-∙-r M→O) =
  cong₂ _∙_ (sym (normal (normal-∙-l Q) (jump M→N))) (normal (normal-∙-r P) (jump M→O))
normal-unique' {O = O} P Q (β-∙-r {L} {N = N} M→N) M→O =
  {!   !}

normal-unique : ∀ {M N O} → Normal N → Normal O → M β→* N → M β→* O → N ≡ O
normal-unique P Q ∎            M→O          = normal P M→O
normal-unique P Q M→N          ∎            = sym (normal Q M→N)
normal-unique P Q (_→*_ {M = L} M→L L→N) (_→*_ {M = K} M→K K→O) = {!   !}
  -- rewrite (normal-unique' {!   !} {!   !} M→L M→K) = normal-unique P Q L→N {!  K→O !}
  -- where
  --   postulate L≡K : L ≡ K
  -- normal-unique' P Q {!   !} {!   !}
-- ... | U = {!   !}
  -- trans {!   !} (normal-unique {!   !} {!   !} L→N {!   !})
    -- L≡K = {!   !}
  -- normal-unique P Q {!   !} M→O
-- normal-unique P Q M→N ∎            = sym (normal Q M→N)
-- normal-unique P Q M→N (M→L →* L→O) = {!   !}

-- β→*-confluent : ∀ {M N O} → (M β→* N) → (M β→* O) → ∃ (λ P → (N β→* P) × (O β→* P))
-- β→*-confluent {M} {.M} {O} ∎            M→O          = O , M→O , ∎
-- β→*-confluent {M} {N} {.M} (M→L →* L→N) ∎            = N , ∎   , (M→L →* L→N)
-- β→*-confluent {M} {N} {O}  (M→L →* L→N) (M→K →* K→O) = {!   !}

-- lemma-0 : ∀ M N → M [ N ] β→* (ƛ M) ∙ N
-- lemma-0 (var zero) (var zero) = (var zero) →⟨ {!   !} ⟩ {!   !}
-- lemma-0 (var zero) (var suc y) = {!   !}
-- lemma-0 (var suc x) (var y) = {!   !}
-- lemma-0 (var x) (ƛ O) = {!   !}
-- lemma-0 (var x) (O ∙ P) = {!   !}
-- lemma-0 (ƛ M)   O = {!   !}
-- lemma-0 (M ∙ N) O = {!   !}

-- lemma : ∀ M N O → ((ƛ M) ∙ N β→* O) → M [ N ] β→* O
-- lemma (var x) N .((ƛ var x) ∙ N) (.((ƛ var x) ∙ N) ∎) = {!   !}
-- lemma (ƛ M) N .((ƛ (ƛ M)) ∙ N) (.((ƛ (ƛ M)) ∙ N) ∎) = {!   !}
-- lemma (M ∙ M₁) N .((ƛ M ∙ M₁) ∙ N) (.((ƛ M ∙ M₁) ∙ N) ∎) = {!   !}
-- lemma M N O (.((ƛ M) ∙ N) →⟨⟩ redex→O) = lemma M N O redex→O
-- lemma M N O (_→⟨_⟩_ .((ƛ M) ∙ N) {P} ƛM∙N→P P→O) = {!   !}
-- -- lemma M N P (jump ƛM∙N→P) <β> P→O

-- lemma-1 : ∀ M N O P → (ƛ M β→* N) → (N ∙ O β→* P) → M [ O ] β→* P
-- lemma-1 M .(ƛ M) O P (.(ƛ M) ∎)           N∙O→P = lemma M O P N∙O→P
-- lemma-1 M N      O P (.(ƛ M) →⟨⟩ ƛM→N)    N∙O→P = lemma-1 M N O P ƛM→N N∙O→P
-- lemma-1 M N O .(N ∙ O) (.(ƛ M) →⟨ x ⟩ ƛM→N) (.(N ∙ O) ∎) = {!   !}
-- lemma-1 M N O P (.(ƛ M) →⟨ x ⟩ ƛM→N) (.(N ∙ O) →⟨⟩ N∙O→P) = {!   !}
-- lemma-1 M N O P (.(ƛ M) →⟨ x ⟩ ƛM→N) (.(N ∙ O) →⟨ x₁ ⟩ N∙O→P) = {!   !}

-- -- (M [ N ]) β→* O
-- -- M'→O : P ∙ N β→* O
-- -- L→M' : ƛ M β→ P
-- -- (M [ N ]) β→* O

-- -- M'→O : N₂ ∙ N β→* O

-- -- L→M' : ƛ M β→ N₂

-- -- M→N : (M [ N ]) β→* N₁

-- -- that diamond prop
-- --
-- --      M
-- --   N     O
-- --      P
-- --
-- β→*-confluent : ∀ {M N O} → (M β→* N) → (M β→* O) → ∃ (λ P → (N β→* P) × (O β→* P))
-- β→*-confluent {O = O} (M ∎)            M→O                 = O , M→O , (O ∎)
-- β→*-confluent         (L →⟨⟩ M→N)      M→O                 = β→*-confluent M→N M→O
-- β→*-confluent {N = N} (L →⟨ x ⟩ M→N)   (.L ∎)              = N , (N ∎) , (L →⟨ x ⟩ M→N)
-- β→*-confluent         (L →⟨ x ⟩ M→N)   (.L →⟨⟩ M→O)        = β→*-confluent (L →⟨ x ⟩ M→N) M→O
-- β→*-confluent (.((ƛ _) ∙ _) →⟨ β-ƛ-∙ ⟩ M→N) (.((ƛ _) ∙ _) →⟨ β-ƛ-∙ ⟩ M'→O) = β→*-confluent M→N M'→O
-- β→*-confluent {N = N} {O} (.((ƛ M) ∙ N₁) →⟨ β-ƛ-∙ {M} {N₁} ⟩ M→N) (.((ƛ M) ∙ N₁) →⟨ β-∙-l {N = N₂} L→M' ⟩ M'→O) = β→*-confluent M→N (lemma-1 M N₂ N₁ O ((ƛ M) →⟨ L→M' ⟩ (N₂ ∎)) M'→O)
-- β→*-confluent (.((ƛ _) ∙ _) →⟨ β-ƛ-∙ ⟩ M→N) (.((ƛ _) ∙ _) →⟨ β-∙-r L→M' ⟩ M'→O) = {!   !}
-- β→*-confluent (.(ƛ _) →⟨ β-ƛ L→M ⟩ M→N) (.(ƛ _) →⟨ L→M' ⟩ M'→O) = {!   !}
-- β→*-confluent (.(_ ∙ _) →⟨ β-∙-l L→M ⟩ M→N) (.(_ ∙ _) →⟨ L→M' ⟩ M'→O) = {!   !}
-- β→*-confluent (.(_ ∙ _) →⟨ β-∙-r L→M ⟩ M→N) (.(_ ∙ _) →⟨ L→M' ⟩ M'→O) = {!   !}

--       L
--     M   M'
--   N       O
--       P
--

-- module Example where

--   S : Term
--   S = ƛ ƛ ƛ var 2 ∙ var 0 ∙ (var 1 ∙ var 0)

--   K : Term
--   K = ƛ ƛ var 1

--   I : Term
--   I = ƛ (var 0)

--   Z : Term
--   Z = ƛ ƛ var 0

--   SZ : Term
--   SZ = ƛ ƛ var 1 ∙ var 0

--   PLUS : Term
--   PLUS = ƛ ƛ ƛ ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var 0)

--   test-0 : ƛ (ƛ ƛ var 1) ∙ var 0 β→* ƛ ƛ var 1
--   test-0 =
--       ƛ (ƛ ƛ var 1) ∙ var 0
--     →⟨ β-ƛ β-ƛ-∙ ⟩
--       ƛ (ƛ var 1) [ var 0 / 0 ]
--     →⟨⟩
--       ƛ ƛ ((var 1) [ shift 0 1 (var 0) / 1 ])
--     →⟨⟩
--       ƛ ƛ ((var 1) [ var 1 / 1 ])
--     →⟨⟩
--       ƛ (ƛ var 1)
--     ∎

--   test-2 : PLUS ∙ Z ∙ SZ β→* SZ
--   test-2 =
--       PLUS ∙ Z ∙ SZ
--     →⟨⟩
--       (ƛ (ƛ (ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero))))) ∙ Z ∙ SZ
--     →⟨ β-∙-l β-ƛ-∙ ⟩
--       ((ƛ (ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)))) [ Z ]) ∙ SZ
--     →⟨⟩
--       ((ƛ (ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)))) [ Z / 0 ]) ∙ SZ
--     →⟨⟩
--       (ƛ ((ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero))) [ shift 0 1 Z / 1 ])) ∙ SZ
--     →⟨⟩
--       (ƛ ((ƛ (ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero))) [ Z / 1 ])) ∙ SZ
--     →⟨⟩
--       (ƛ (ƛ ((ƛ var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)) [ Z / 2 ]))) ∙ SZ
--     →⟨⟩
--       (ƛ (ƛ (ƛ ((var 3 ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)) [ Z / 3 ])))) ∙ SZ
--     →⟨⟩
--       (ƛ ƛ ƛ Z ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)) ∙ SZ
--     →⟨ β-ƛ-∙ ⟩
--       ((ƛ ƛ Z ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)) [ SZ / 0 ])
--     →⟨⟩
--       ƛ ((ƛ Z ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)) [ SZ / 1 ])
--     →⟨⟩
--       ƛ ƛ ((Z ∙ var 1 ∙ (var 2 ∙ var 1 ∙ var zero)) [ SZ / 2 ])
--     →⟨⟩
--       ƛ ƛ Z ∙ var 1 ∙ (SZ ∙ var 1 ∙ var 0)
--     →⟨ β-ƛ (β-ƛ (β-∙-r (β-∙-l β-ƛ-∙))) ⟩
--       ƛ ƛ Z ∙ var 1 ∙ (((ƛ var 1 ∙ var 0) [ var 1 ]) ∙ var 0)
--     →⟨⟩
--       ƛ ƛ Z ∙ var 1 ∙ (((ƛ var 1 ∙ var 0) [ var 1 / 0 ]) ∙ var 0)
--     →⟨⟩
--       ƛ ƛ Z ∙ var 1 ∙ ((ƛ ((var 1 ∙ var 0) [ shift 0 1 (var 1) / 1 ])) ∙ var 0)
--     →⟨⟩
--       ƛ ƛ Z ∙ var 1 ∙ ((ƛ ((var 1 ∙ var 0) [ var 1 / 1 ])) ∙ var 0)
--     →⟨⟩
--       ƛ ƛ Z ∙ var 1 ∙ ((ƛ var 1 ∙ var 0) ∙ var 0)
--     →⟨ β-ƛ (β-ƛ (β-∙-r β-ƛ-∙)) ⟩
--       ƛ ƛ Z ∙ var 1 ∙ ((var 1 ∙ var 0) [ var 0 / 0 ])
--     →⟨⟩
--       ƛ ƛ (ƛ ƛ var 0) ∙ var 1 ∙ (var 1 ∙ var 0)
--     →⟨ β-ƛ (β-ƛ (β-∙-l β-ƛ-∙)) ⟩
--       ƛ ƛ ((ƛ var 0) [ var 1 / 0 ]) ∙ (var 1 ∙ var 0)
--     →⟨⟩
--       ƛ ƛ (ƛ ((var 0) [ var 1 / 1 ])) ∙ (var 1 ∙ var 0)
--     →⟨⟩
--       ƛ ƛ (ƛ var 0) ∙ (var 1 ∙ var 0)
--     →⟨ β-ƛ (β-ƛ β-ƛ-∙) ⟩
--       ƛ ƛ ((var 0) [ var 1 ∙ var 0 / 0 ])
--     →⟨⟩
--       SZ
--     ∎

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid; cong; trans)
import Function.Equality
open import Relation.Binary using (Setoid)

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Instance.Setoids
open import Categories.Monad.Relative
open import Categories.Category.Equivalence
open import Categories.Category.Cocartesian

module SecondOrder.RelativeMonadMorphism
  {o ℓ e o′ ℓ′ e′ : Level}
  {C : Category o ℓ e}
  {D : Category o′ ℓ′ e′}
  where

  record RMonadMorph {J : Functor C D} (M M’ : Monad J) : Set (lsuc (o ⊔ ℓ′ ⊔ e′))
    where
      open Category D
      open Monad
      field
        morph : ∀ {X} → (F₀ M X) ⇒ (F₀ M’ X)
        law-unit : ∀ {X} → morph ∘ (unit M {X}) ≈ unit M’ {X}
        law-extend : ∀ {X Y} {k : (Functor.F₀ J X) ⇒ (F₀ M Y)}
                → (morph {Y}) ∘ (extend  M k)
                  ≈ (extend M’ ((morph {Y}) ∘ k)) ∘ (morph {X})

  -- here, the equality used is the equivalence relation between morphisms of the category D

ext: agda

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
open import Preliminaries
open import Preorder

module PreorderExamples where

-- there is a preorder on Unit

  unit-p : Preorder Unit
  unit-p = preorder (preorder-structure (λ x x₁ → Unit) (λ x → <>) (λ x y z _ _ → <>))

-- there is a preorder on Nat

  _≤n_ : Nat → Nat → Set
  _≤n_ Z Z = Unit
  _≤n_ Z (S n) = Unit
  _≤n_ (S m) Z = Void
  _≤n_ (S m) (S n) = m ≤n n

  nat-refl : ∀ (n : Nat) → n ≤n n
  nat-refl Z = <>
  nat-refl (S n) = nat-refl n

  nat-trans : ∀ (m n p : Nat) → m ≤n n → n ≤n p → m ≤n p
  nat-trans Z Z Z x x₁ = <>
  nat-trans Z Z (S p) x x₁ = <>
  nat-trans Z (S n) Z x x₁ = <>
  nat-trans Z (S n) (S p) x x₁ = <>
  nat-trans (S m) Z Z () x₁
  nat-trans (S m) Z (S p) () x₁
  nat-trans (S m) (S n) Z x ()
  nat-trans (S m) (S n) (S p) x x₁ = nat-trans m n p x x₁

  nat-p : Preorder Nat
  nat-p = preorder (preorder-structure (λ m n → m ≤n n) nat-refl nat-trans)

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
-- Andreas, 2020-06-17, issue #4135
-- Do not allow meta-solving during projection disambiguation!

data Bool : Set where
  true false : Bool

module Foo (b : Bool) where
  record R : Set where
    field f : Bool
  open R public

open module True  = Foo true
open module False = Foo false

test : Foo.R {!!}
test .f = {!!}

-- WAS: succeeds with constraint ?0 := true
-- C-c C-=

-- Expected error:
-- Ambiguous projection f.
-- It could refer to any of
--   True.f (introduced at <open module True>)
--   False.f (introduced at <open module False>)
-- when checking the clause left hand side
-- test .f

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- 2010-10-15 and 2012-03-09
{-# OPTIONS -v tc.conv.irr:50 -v tc.decl.ax:10 #-}

module Issue351 where

import Common.Irrelevance

data _==_ {A : Set1}(a : A) : A -> Set where
  refl : a == a

record R : Set1 where
  constructor mkR
  field
    fromR : Set

reflR : (r : R) -> r == (mkR _)
reflR r = refl {a = _}

record IR : Set1 where
  constructor mkIR
  field
    .fromIR : Set

reflIR : (r : IR) -> r == (mkIR _)
reflIR r = refl {a = _}
-- peeking into the irrelevant argument, we can immediately solve for the meta

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
open import Prelude

module Implicits.Semantics.Type where

open import Data.Vec
open import Implicits.Syntax
open import SystemF.Everything as F using ()

⟦_⟧tp→ : ∀ {ν} → Type ν → F.Type ν
⟦ simpl (tc n) ⟧tp→ = F.tc n
⟦ simpl (tvar n) ⟧tp→ = F.tvar n
⟦ simpl (a →' b) ⟧tp→ = ⟦ a ⟧tp→ F.→' ⟦ b ⟧tp→
⟦ a ⇒ b ⟧tp→ = ⟦ a ⟧tp→ F.→' ⟦ b ⟧tp→
⟦ ∀' x ⟧tp→ = F.∀' ⟦ x ⟧tp→

⟦_⟧tps→ : ∀ {ν n} → Vec (Type ν) n → Vec (F.Type ν) n
⟦ v ⟧tps→ = map (⟦_⟧tp→) v


text:
-- Andreas, 2011-04-05
module EtaContractToMillerPattern where

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

record Prod (A B : Set) : Set where
  constructor _,_
  field fst : A
        snd : B
open Prod

postulate A B C : Set

test : let X : (Prod A B -> C) -> (Prod A B -> C)
           X = _
       in (x : Prod A B -> C) ->
            X (\ z -> x (fst z , snd z)) == x
test x = refl
-- eta contracts unification problem to  X x = x

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Foundations.Path where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Reflection.StrictEquiv

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- Less polymorphic version of `cong`, to avoid some unresolved metas
cong′ : ∀ {B : Type ℓ'} (f : A → B) {x y : A} (p : x ≡ y)
      → Path B (f x) (f y)
cong′ f = cong f
{-# INLINE cong′ #-}

PathP≡Path : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) →
             PathP P p q ≡ Path (P i1) (transport (λ i → P i) p) q
PathP≡Path P p q i = PathP (λ j → P (i ∨ j)) (transport-filler (λ j → P j) p i) q

PathP≡Path⁻ : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) →
             PathP P p q ≡ Path (P i0) p (transport⁻ (λ i → P i) q)
PathP≡Path⁻ P p q i = PathP (λ j → P (~ i ∧ j)) p (transport⁻-filler (λ j → P j) q i)

PathPIsoPath : ∀ (A : I → Type ℓ) (x : A i0) (y : A i1) → Iso (PathP A x y) (transport (λ i → A i) x ≡ y)
PathPIsoPath A x y .Iso.fun = fromPathP
PathPIsoPath A x y .Iso.inv = toPathP
PathPIsoPath A x y .Iso.rightInv q k i =
  hcomp
    (λ j → λ
      { (i = i0) → slide (j ∨ ~ k)
      ; (i = i1) → q j
      ; (k = i0) → transp (λ l → A (i ∨ l)) i (fromPathPFiller j)
      ; (k = i1) → ∧∨Square i j
      })
    (transp (λ l → A (i ∨ ~ k ∨ l)) (i ∨ ~ k)
      (transp (λ l → (A (i ∨ (~ k ∧ l)))) (k ∨ i)
        (transp (λ l → A (i ∧ l)) (~ i)
          x)))
  where
  fromPathPFiller : _
  fromPathPFiller =
    hfill
      (λ j → λ
        { (i = i0) → x
        ; (i = i1) → q j })
      (inS (transp (λ j → A (i ∧ j)) (~ i) x))

  slide : I → _
  slide i = transp (λ l → A (i ∨ l)) i (transp (λ l → A (i ∧ l)) (~ i) x)

  ∧∨Square : I → I → _
  ∧∨Square i j =
    hcomp
      (λ l → λ
        { (i = i0) → slide j
        ; (i = i1) → q (j ∧ l)
        ; (j = i0) → slide i
        ; (j = i1) → q (i ∧ l)
        })
      (slide (i ∨ j))
PathPIsoPath A x y .Iso.leftInv q k i =
  outS
    (hcomp-unique
      (λ j → λ
        { (i = i0) → x
        ; (i = i1) → transp (λ l → A (j ∨ l)) j (q j)
        })
      (inS (transp (λ l → A (i ∧ l)) (~ i) x))
      (λ j → inS (transp (λ l → A (i ∧ (j ∨ l))) (~ i ∨ j) (q (i ∧ j)))))
    k

PathP≃Path : (A : I → Type ℓ) (x : A i0) (y : A i1) →
             PathP A x y ≃ (transport (λ i → A i) x ≡ y)
PathP≃Path A x y = isoToEquiv (PathPIsoPath A x y)

PathP≡compPath : ∀ {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) (r : x ≡ z)
                 → (PathP (λ i → x ≡ q i) p r) ≡ (p ∙ q ≡ r)
PathP≡compPath p q r k = PathP (λ i → p i0 ≡ q (i ∨ k)) (λ j → compPath-filler p q k j) r

PathP≡doubleCompPathˡ : ∀ {A : Type ℓ} {w x y z : A} (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z)
                        → (PathP (λ i → p i ≡ s i) q r) ≡ (p ⁻¹ ∙∙ q ∙∙ s ≡ r)
PathP≡doubleCompPathˡ p q r s k = PathP (λ i → p (i ∨ k) ≡ s (i ∨ k))
                                        (λ j → doubleCompPath-filler (p ⁻¹) q s k j) r

PathP≡doubleCompPathʳ : ∀ {A : Type ℓ} {w x y z : A} (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z)
                        → (PathP (λ i → p i ≡ s i) q r) ≡ (q ≡ p ∙∙ r ∙∙ s ⁻¹)
PathP≡doubleCompPathʳ p q r s k  = PathP (λ i → p (i ∧ (~ k)) ≡ s (i ∧ (~ k)))
                                         q (λ j → doubleCompPath-filler p r (s ⁻¹) k j)

compPathl-cancel : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : x ≡ z) → p ∙ (sym p ∙ q) ≡ q
compPathl-cancel p q = p ∙ (sym p ∙ q) ≡⟨ assoc p (sym p) q ⟩
                       (p ∙ sym p) ∙ q ≡⟨ cong (_∙ q) (rCancel p) ⟩
                              refl ∙ q ≡⟨ sym (lUnit q) ⟩
                                     q ∎

compPathr-cancel : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : z ≡ y) (q : x ≡ y) → (q ∙ sym p) ∙ p ≡ q
compPathr-cancel {x = x} p q i j =
  hcomp-equivFiller (doubleComp-faces (λ _ → x) (sym p) j) (inS (q j)) (~ i)

compPathl-isEquiv : {x y z : A} (p : x ≡ y) → isEquiv (λ (q : y ≡ z) → p ∙ q)
compPathl-isEquiv p = isoToIsEquiv (iso (p ∙_) (sym p ∙_) (compPathl-cancel p) (compPathl-cancel (sym p)))

compPathlEquiv : {x y z : A} (p : x ≡ y) → (y ≡ z) ≃ (x ≡ z)
compPathlEquiv p = (p ∙_) , compPathl-isEquiv p

compPathr-isEquiv : {x y z : A} (p : y ≡ z) → isEquiv (λ (q : x ≡ y) → q ∙ p)
compPathr-isEquiv p = isoToIsEquiv (iso (_∙ p) (_∙ sym p) (compPathr-cancel p) (compPathr-cancel (sym p)))

compPathrEquiv : {x y z : A} (p : y ≡ z) → (x ≡ y) ≃ (x ≡ z)
compPathrEquiv p = (_∙ p) , compPathr-isEquiv p

-- Variations of isProp→isSet for PathP
isProp→SquareP : ∀ {B : I → I → Type ℓ} → ((i j : I) → isProp (B i j))
             → {a : B i0 i0} {b : B i0 i1} {c : B i1 i0} {d : B i1 i1}
             → (r : PathP (λ j → B j i0) a c) (s : PathP (λ j → B j i1) b d)
             → (t : PathP (λ j → B i0 j) a b) (u : PathP (λ j → B i1 j) c d)
             → SquareP B t u r s
isProp→SquareP {B = B} isPropB {a = a} r s t u i j =
  hcomp (λ { k (i = i0) → isPropB i0 j (base i0 j) (t j) k
           ; k (i = i1) → isPropB i1 j (base i1 j) (u j) k
           ; k (j = i0) → isPropB i i0 (base i i0) (r i) k
           ; k (j = i1) → isPropB i i1 (base i i1) (s i) k
        }) (base i j) where
    base : (i j : I) → B i j
    base i j = transport (λ k → B (i ∧ k) (j ∧ k)) a

isProp→isPropPathP : ∀ {ℓ} {B : I → Type ℓ} → ((i : I) → isProp (B i))
                   → (b0 : B i0) (b1 : B i1)
                   → isProp (PathP (λ i → B i) b0 b1)
isProp→isPropPathP {B = B} hB b0 b1 = isProp→SquareP (λ _ → hB) refl refl

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

-- Flipping a square along its diagonal

flipSquare : {a₀₀ a₀₁ : A} {a₀₋ : a₀₀ ≡ a₀₁}
  {a₁₀ a₁₁ : A} {a₁₋ : a₁₀ ≡ a₁₁}
  {a₋₀ : a₀₀ ≡ a₁₀} {a₋₁ : a₀₁ ≡ a₁₁}
  → Square a₀₋ a₁₋ a₋₀ a₋₁ → Square a₋₀ a₋₁ a₀₋ a₁₋
flipSquare sq i j = sq j i

module _ {a₀₀ a₀₁ : A} {a₀₋ : a₀₀ ≡ a₀₁} {a₁₀ a₁₁ : A} {a₁₋ : a₁₀ ≡ a₁₁}
  {a₋₀ : a₀₀ ≡ a₁₀} {a₋₁ : a₀₁ ≡ a₁₁}
  where

  flipSquareEquiv : Square a₀₋ a₁₋ a₋₀ a₋₁ ≃ Square a₋₀ a₋₁ a₀₋ a₁₋
  unquoteDef flipSquareEquiv = defStrictEquiv flipSquareEquiv flipSquare flipSquare

  flipSquarePath : Square a₀₋ a₁₋ a₋₀ a₋₁ ≡ Square a₋₀ a₋₁ a₀₋ a₁₋
  flipSquarePath = ua flipSquareEquiv

module _ {a₀₀ a₁₁ : A} {a₋ : a₀₀ ≡ a₁₁}
  {a₁₀ : A} {a₁₋ : a₁₀ ≡ a₁₁} {a₋₀ : a₀₀ ≡ a₁₀} where

  slideSquareFaces : (i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
  slideSquareFaces i j k (i = i0) = a₋ (j ∧ ~ k)
  slideSquareFaces i j k (i = i1) = a₁₋ j
  slideSquareFaces i j k (j = i0) = a₋₀ i
  slideSquareFaces i j k (j = i1) = a₋ (i ∨ ~ k)

  slideSquare : Square a₋ a₁₋ a₋₀ refl → Square refl a₁₋ a₋₀ a₋
  slideSquare sq i j = hcomp (slideSquareFaces i j) (sq i j)

  slideSquareEquiv : (Square a₋ a₁₋ a₋₀ refl) ≃ (Square refl a₁₋ a₋₀ a₋)
  slideSquareEquiv = isoToEquiv (iso slideSquare slideSquareInv fillerTo fillerFrom) where
    slideSquareInv : Square refl a₁₋ a₋₀ a₋ → Square a₋ a₁₋ a₋₀ refl
    slideSquareInv sq i j = hcomp (λ k → slideSquareFaces i j (~ k)) (sq i j)
    fillerTo : ∀ p → slideSquare (slideSquareInv p) ≡ p
    fillerTo p k i j = hcomp-equivFiller (λ k → slideSquareFaces i j (~ k)) (inS (p i j)) (~ k)
    fillerFrom : ∀ p → slideSquareInv (slideSquare p) ≡ p
    fillerFrom p k i j = hcomp-equivFiller (slideSquareFaces i j) (inS (p i j)) (~ k)

-- The type of fillers of a square is equivalent to the double composition identites
Square≃doubleComp : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
                    (a₀₋ : a₀₀ ≡ a₀₁) (a₁₋ : a₁₀ ≡ a₁₁)
                    (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁)
                    → Square a₀₋ a₁₋ a₋₀ a₋₁ ≃ (a₋₀ ⁻¹ ∙∙ a₀₋ ∙∙ a₋₁ ≡ a₁₋)
Square≃doubleComp a₀₋ a₁₋ a₋₀ a₋₁ = transportEquiv (PathP≡doubleCompPathˡ a₋₀ a₀₋ a₁₋ a₋₁)

-- Flipping a square in Ω²A is the same as inverting it
sym≡flipSquare : {x : A} (P : Square (refl {x = x}) refl refl refl)
  → sym P ≡ flipSquare P
sym≡flipSquare {x = x} P = sym (main refl P)
  where
  B : (q : x ≡ x) → I → Type _
  B q i = PathP (λ j → x ≡ q (i ∨ j)) (λ k → q (i ∧ k)) refl

  main : (q : x ≡ x) (p : refl ≡ q) → PathP (λ i → B q i) (λ i j → p j i) (sym p)
  main q = J (λ q p → PathP (λ i → B q i) (λ i j → p j i) (sym p)) refl

-- Inverting both interval arguments of a square in Ω²A is the same as doing nothing
sym-cong-sym≡id : {x : A} (P : Square (refl {x = x}) refl refl refl)
  → P ≡ λ i j → P (~ i) (~ j)
sym-cong-sym≡id {x = x} P = sym (main refl P)
  where
  B : (q : x ≡ x) → I → Type _
  B q i = Path (x ≡ q i) (λ j → q (i ∨ ~ j)) λ j → q (i ∧ j)

  main : (q : x ≡ x) (p : refl ≡ q) → PathP (λ i → B q i) (λ i j → p (~ i) (~ j)) p
  main q = J (λ q p → PathP (λ i → B q i) (λ i j → p (~ i) (~ j)) p) refl

-- Applying cong sym is the same as flipping a square in Ω²A
flipSquare≡cong-sym : ∀ {ℓ} {A : Type ℓ} {x : A} (P : Square (refl {x = x}) refl refl refl)
  → flipSquare P ≡ λ i j → P i (~ j)
flipSquare≡cong-sym P = sym (sym≡flipSquare P) ∙ sym (sym-cong-sym≡id (cong sym P))

-- Applying cong sym is the same as inverting a square in Ω²A
sym≡cong-sym : ∀ {ℓ} {A : Type ℓ} {x : A} (P : Square (refl {x = x}) refl refl refl)
  → sym P ≡ cong sym P
sym≡cong-sym P = sym-cong-sym≡id (sym P)

-- sym induces an equivalence on identity types of paths
symIso : {a b : A} (p q : a ≡ b) → Iso (p ≡ q) (q ≡ p)
symIso p q = iso sym sym (λ _ → refl) λ _ → refl

-- J is an equivalence
Jequiv : {x : A} (P : ∀ y → x ≡ y → Type ℓ') → P x refl ≃ (∀ {y} (p : x ≡ y) → P y p)
Jequiv P = isoToEquiv isom
  where
  isom : Iso _ _
  Iso.fun isom = J P
  Iso.inv isom f = f refl
  Iso.rightInv isom f =
    implicitFunExt λ {_} →
    funExt λ t →
    J (λ _ t → J P (f refl) t ≡ f t) (JRefl P (f refl)) t
  Iso.leftInv isom = JRefl P

-- Action of PathP on equivalences (without relying on univalence)

congPathIso : ∀ {ℓ ℓ'} {A : I → Type ℓ} {B : I → Type ℓ'}
  (e : ∀ i → A i ≃ B i) {a₀ : A i0} {a₁ : A i1}
  → Iso (PathP A a₀ a₁) (PathP B (e i0 .fst a₀) (e i1 .fst a₁))
congPathIso {A = A} {B} e {a₀} {a₁} .Iso.fun p i = e i .fst (p i)
congPathIso {A = A} {B} e {a₀} {a₁} .Iso.inv q i =
  hcomp
    (λ j → λ
      { (i = i0) → retEq (e i0) a₀ j
      ; (i = i1) → retEq (e i1) a₁ j
      })
    (invEq (e i) (q i))
congPathIso {A = A} {B} e {a₀} {a₁} .Iso.rightInv q k i =
  hcomp
    (λ j → λ
      { (i = i0) → commSqIsEq (e i0 .snd) a₀ j k
      ; (i = i1) → commSqIsEq (e i1 .snd) a₁ j k
      ; (k = i0) →
        e i .fst
          (hfill
            (λ j → λ
              { (i = i0) → retEq (e i0) a₀ j
              ; (i = i1) → retEq (e i1) a₁ j
              })
            (inS (invEq (e i) (q i)))
            j)
      ; (k = i1) → q i
      })
    (secEq (e i) (q i) k)
    where b = commSqIsEq
congPathIso {A = A} {B} e {a₀} {a₁} .Iso.leftInv p k i =
  hcomp
    (λ j → λ
      { (i = i0) → retEq (e i0) a₀ (j ∨ k)
      ; (i = i1) → retEq (e i1) a₁ (j ∨ k)
      ; (k = i1) → p i
      })
    (retEq (e i) (p i) k)

congPathEquiv : ∀ {ℓ ℓ'} {A : I → Type ℓ} {B : I → Type ℓ'}
  (e : ∀ i → A i ≃ B i) {a₀ : A i0} {a₁ : A i1}
  → PathP A a₀ a₁ ≃ PathP B (e i0 .fst a₀) (e i1 .fst a₁)
congPathEquiv e = isoToEquiv (congPathIso e)

-- Characterizations of dependent paths in path types

doubleCompPath-filler∙ : {a b c d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d)
  → PathP (λ i → p i ≡ r (~ i)) (p ∙ q ∙ r) q
doubleCompPath-filler∙ {A = A} {b = b} p q r j i =
  hcomp (λ k → λ { (i = i0) → p j
                  ; (i = i1) → side j k
                  ; (j = i1) → q (i ∧ k)})
        (p (j ∨ i))
  where
  side : I → I → A
  side i j =
    hcomp (λ k → λ { (i = i1) → q j
                    ; (j = i0) → b
                    ; (j = i1) → r (~ i ∧ k)})
          (q j)

PathP→compPathL : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
  → PathP (λ i → p i ≡ q i) r s
  → sym p ∙ r ∙ q ≡ s
PathP→compPathL {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (j ∨ k)
                 ; (i = i1) → q (j ∨ k)
                 ; (j = i0) → doubleCompPath-filler∙ (sym p) r q (~ k) i
                 ; (j = i1) → s i })
        (P j i)

PathP→compPathR : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
  → PathP (λ i → p i ≡ q i) r s
  → r ≡ p ∙ s ∙ sym q
PathP→compPathR {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (j ∧ (~ k))
                 ; (i = i1) → q (j ∧ (~ k))
                 ; (j = i0) → r i
                 ; (j = i1) → doubleCompPath-filler∙ p s (sym q) (~ k) i})
        (P j i)

-- Other direction

compPathL→PathP : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
  → sym p ∙ r ∙ q ≡ s
  → PathP (λ i → p i ≡ q i) r s
compPathL→PathP {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (~ k ∨ j)
                 ; (i = i1) → q (~ k ∨ j)
                 ; (j = i0) → doubleCompPath-filler∙ (sym p) r q k i
                 ; (j = i1) → s i})
        (P j i)

compPathR→PathP : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
  → r ≡ p ∙ s ∙ sym q
  → PathP (λ i → p i ≡ q i) r s
compPathR→PathP {p = p} {q = q} {r = r} {s = s} P j i =
  hcomp (λ k → λ { (i = i0) → p (k ∧ j)
                 ; (i = i1) → q (k ∧ j)
                 ; (j = i0) → r i
                 ; (j = i1) → doubleCompPath-filler∙  p s (sym q) k i})
        (P j i)

compPathR→PathP∙∙ : {a b c d : A} {p : a ≡ c} {q : b ≡ d} {r : a ≡ b} {s : c ≡ d}
  → r ≡ p ∙∙ s ∙∙ sym q
  → PathP (λ i → p i ≡ q i) r s
compPathR→PathP∙∙ {p = p} {q = q} {r = r} {s = s} P j i =
    hcomp (λ k → λ { (i = i0) → p (k ∧ j)
                   ; (i = i1) → q (k ∧ j)
                   ; (j = i0) → r i
                   ; (j = i1) → doubleCompPath-filler  p s (sym q) (~ k) i})
          (P j i)


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteData as VoteData
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.Properties.VoteData (self : VoteData) where

  record Contract : Set where
    field
      ep≡     : self ^∙ vdParent ∙ biEpoch ≡ self ^∙ vdProposed ∙ biEpoch
      parRnd< : self ^∙ vdParent ∙ biRound < self ^∙ vdProposed ∙ biRound
      parVer≤ : (self ^∙ vdParent ∙ biVersion) ≤-Version (self ^∙ vdProposed ∙ biVersion)
  open Contract

  contract
      : VoteData.verify self ≡ Right unit → Contract
  contract
     with self ^∙ vdParent ∙ biEpoch ≟ self ^∙ vdProposed ∙ biEpoch
  ...| no neq = (λ ())
  ...| yes refl
     with self ^∙ vdParent ∙ biRound <? self ^∙ vdProposed ∙ biRound
  ...| no ¬par<prop = (λ ())
  ...| yes par<prop
     with (self ^∙ vdParent ∙ biVersion) ≤?-Version (self ^∙ vdProposed ∙ biVersion)
  ...| no ¬parVer≤ = (λ ())
  ...| yes parVer≤ = (λ x → record { ep≡ = refl
                                   ; parRnd< = par<prop
                                   ; parVer≤ = parVer≤ })


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

open import LogicalFormulae
open import Setoids.Setoids
open import Groups.Definition
open import Sets.EquivalenceRelations

module Groups.Groups where

reflGroupWellDefined : {lvl : _} {A : Set lvl} {m n x y : A} {op : A → A → A} → m ≡ x → n ≡ y → (op m n) ≡ (op x y)
reflGroupWellDefined {lvl} {A} {m} {n} {.m} {.n} {op} refl refl = refl
fourWay+Associative : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → {r s t u : A} → (Setoid._∼_ S) (r · ((s · t) · u)) ((r · s) · (t · u))
fourWay+Associative {S = S} {_·_} G {r} {s} {t} {u} = transitive p1 (transitive p2 p3)
  where
    open Group G renaming (inverse to _^-1)
    open Setoid S
    open Equivalence eq
    p1 : r · ((s · t) · u) ∼ (r · (s · t)) · u
    p2 : (r · (s · t)) · u ∼ ((r · s) · t) · u
    p3 : ((r · s) · t) · u ∼ (r · s) · (t · u)
    p1 = Group.+Associative G
    p2 = Group.+WellDefined G (Group.+Associative G) reflexive
    p3 = symmetric (Group.+Associative G)

fourWay+Associative' : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) {a b c d : A} → (Setoid._∼_ S (((a · b) · c) · d) (a · ((b · c) · d)))
fourWay+Associative' {S = S} G = transitive (symmetric +Associative) (symmetric (fourWay+Associative G))
  where
    open Group G
    open Setoid S
    open Equivalence eq

fourWay+Associative'' : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) {a b c d : A} → (Setoid._∼_ S (a · (b · (c · d))) (a · ((b · c) · d)))
fourWay+Associative'' {S = S} {_·_ = _·_} G = transitive +Associative (symmetric (fourWay+Associative G))
  where
    open Group G
    open Setoid S
    open Equivalence eq


text:
module Punctaffy.Hypersnippet.Dim where

open import Level using (Level; suc; _⊔_)
open import Algebra.Bundles using (IdempotentCommutativeMonoid)
open import Algebra.Morphism using (IsIdempotentCommutativeMonoidMorphism)

-- For all the purposes we have for it so far, a `DimSys` is a bounded
-- semilattice. The `agda-stdlib` library calls this an idempotent commutative
-- monoid.
record DimSys {n l : Level} : Set (suc (n ⊔ l)) where
  field
    dimIdempotentCommutativeMonoid : IdempotentCommutativeMonoid n l
  open IdempotentCommutativeMonoid dimIdempotentCommutativeMonoid public

record DimSysMorphism {n₀ n₁ l₀ l₁ : Level} : Set (suc (n₀ ⊔ n₁ ⊔ l₀ ⊔ l₁)) where
  field
    From : DimSys {n₀} {l₀}
    To : DimSys {n₁} {l₁}

  private
    module F = DimSys From
    module T = DimSys To

  field
    morphDim : F.Carrier → T.Carrier
    isIdempotentCommutativeMonoidMorphism :
      IsIdempotentCommutativeMonoidMorphism F.dimIdempotentCommutativeMonoid T.dimIdempotentCommutativeMonoid morphDim

dimLte : {n l : Level} → {ds : DimSys {n} {l}} → DimSys.Carrier ds → DimSys.Carrier ds → Set l
dimLte {n} {l} {ds} a b = DimSys._≈_ ds (DimSys._∙_ ds a b) b

max_stars_repo_name: rocketnia/lexmeta

max_issues_repo_name: rocketnia/lexmeta

max_forks_repo_name: lathe/punctaffy-for-racket


text:
{-# OPTIONS --without-K #-}
module equality.groupoid where

open import equality.core

_⁻¹ : ∀ {i}{X : Set i}{x y : X} → x ≡ y → y ≡ x
_⁻¹ = sym

left-unit : ∀ {i}{X : Set i}{x y : X}
          → (p : x ≡ y)
          → p · refl ≡ p
left-unit refl = refl

right-unit : ∀ {i}{X : Set i}{x y : X}
           → (p : x ≡ y)
           → refl · p ≡ p
right-unit refl = refl

associativity : ∀ {i}{X : Set i}{x y z w : X}
              → (p : x ≡ y)(q : y ≡ z)(r : z ≡ w)
              → p · q · r ≡ p · (q · r)
associativity refl _ _ = refl

left-inverse : ∀ {i}{X : Set i}{x y : X}
             → (p : x ≡ y)
             → p · p ⁻¹ ≡ refl
left-inverse refl = refl

right-inverse : ∀ {i}{X : Set i}{x y : X}
              → (p : x ≡ y)
              → p ⁻¹ · p ≡ refl
right-inverse refl = refl

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

module Issue2250-2 where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data ⊥ : Set where

abstract

  f : Bool → Bool
  f x = true
  {-# INJECTIVE f #-}

  same : f true ≡ f false
  same = refl

not-same : f true ≡ f false → ⊥
not-same ()

absurd : ⊥
absurd = not-same same

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2011-05-09
-- {-# OPTIONS -v tc.meta:15 -v tc.inj:40 #-}
module Issue383 where

data D (A : Set) : A → Set where

data Unit : Set where
  unit : Unit

D′ : (A : Set) → A → Unit → Set
D′ A x unit = D A x

postulate
  Q : (A : Set) → A → Set
  q : (u : Unit) (A : Set) (x : A) → D′ A x u → Q A x

  A : Set
  x : A
  d : D A x

  P : (A : Set) → A → Set
  p : P (Q _ _) (q _ _ _ d)

-- SOLVED, WORKS NOW.
-- OLD BEHAVIOR:
-- Agda does not infer the values of the underscores on the last line.
-- Shouldn't constructor-headedness come to the rescue here? Agda does
-- identify D′ as being constructor-headed, and does invert D′ /six
-- times/, but still fails to infer that the third underscore should
-- be unit.

{-
blocked _41 := d
     by [(D A x) =< (D′ _39 _40 _38) : Set]
blocked _42 := q _38 _36 _40 _41
     by [_40 == _37 : _36]
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT
import homotopy.HopfConstruction
open import homotopy.CircleHSpace
open import homotopy.SuspensionJoin using () renaming (e to suspension-join)
open import homotopy.S1SuspensionS0 using () renaming (e to S¹≃SuspensionS⁰)
import homotopy.JoinAssoc

module homotopy.Hopf where

-- To move
S⁰ = Bool
S² = Suspension S¹
S³ = Suspension S²

-- To move
S¹-connected : is-connected ⟨0⟩ S¹
S¹-connected =
  ([ base ] , Trunc-elim (λ x → =-preserves-level ⟨0⟩ Trunc-level)
             (S¹-elim idp (prop-has-all-paths-↓ ((Trunc-level :> is-set (Trunc ⟨0⟩ S¹)) _ _))))

module Hopf = homotopy.HopfConstruction S¹ S¹-connected S¹-hSpace

Hopf : S² → Type₀
Hopf = Hopf.H.f

Hopf-fiber : Hopf (north _) == S¹
Hopf-fiber = idp

Hopf-total : Σ _ Hopf == S³
Hopf-total =
  Σ _ Hopf               =⟨ Hopf.theorem ⟩
  S¹ * S¹                =⟨ ua S¹≃SuspensionS⁰ |in-ctx (λ u → u * S¹) ⟩
  (Suspension S⁰) * S¹   =⟨ ua (suspension-join S⁰) |in-ctx (λ u → u * S¹) ⟩
  (S⁰ * S⁰) * S¹         =⟨ ua (homotopy.JoinAssoc.*-assoc S⁰ S⁰ S¹) ⟩
  S⁰ * (S⁰ * S¹)         =⟨ ! (ua (suspension-join S¹)) |in-ctx (λ u → S⁰ * u) ⟩
  S⁰ * S²                =⟨ ! (ua (suspension-join S²)) ⟩
  S³ ∎

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Common.Prelude
open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

postulate is-id : ∀ {A : Set} → (A → A) → Bool
postulate is-id-true : ∀ {A} → is-id {A} (λ x → x) ≡ true

{-# REWRITE is-id-true #-}

test₁ : is-id {Nat} (λ x → x) ≡ true
test₁ = refl

postulate is-const : ∀ {A : Set} → (A → A) → Bool
postulate is-const-true : ∀ {A} (x : A) → is-const (λ _ → x) ≡ true

{-# REWRITE is-const-true #-}

test₂ : is-const {Nat} (λ _ → 42) ≡ true
test₂ = refl

ap : {A B : Set} (f : A → B) {x y : A} →
  x ≡ y → f x ≡ f y
ap f refl = refl

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

{- Cartesian product -}

module _ {A B : Set} where

  _,=_ : {a a' : A} (p : a ≡ a') {b b' : B} (q : b ≡ b') → (a , b) ≡ (a' , b')
  refl ,= refl = refl

  ap-,-l : (b : B) {a a' : A} (p : a ≡ a') →
    ap (λ z → z , b) p ≡ (p ,= refl)
  ap-,-l b refl = refl
  {-# REWRITE ap-,-l #-}

  test₃ : (b : B) {a a' : A} (p : a ≡ a') →
    ap (λ z → z , b) p ≡ (p ,= refl)
  test₃ _ _ = refl

  ap-,-r : (a : A) {b b' : B} (p : b ≡ b') →
    ap (λ z → a , z) p ≡ (refl ,= p)
  ap-,-r a refl = refl
  {-# REWRITE ap-,-r #-}

  test₄ : (a : A) {b b' : B} (p : b ≡ b') →
    ap (λ z → a , z) p ≡ (refl ,= p)
  test₄ a _ = refl

ap-idf : {A : Set} {x y : A} (p : x ≡ y) → ap (λ x → x) p ≡ p
ap-idf refl = refl
{-# REWRITE ap-idf #-}

{- Function extensionality -}

module _ {A B : Set} {f g : A → B} where

  postulate
    funext : ((x : A) → f x ≡ g x) → f ≡ g

  postulate
    ap-app-funext : (a : A) (h : (x : A) → f x ≡ g x) →
      ap (λ f → f a) (funext h) ≡ h a
  {-# REWRITE ap-app-funext #-}

  test₅ : (a : A) (h : (x : A) → f x ≡ g x) →
      ap (λ f → f a) (funext h) ≡ h a
  test₅ a h = refl

{- Dependent paths -}

module _ where
  PathOver : {A : Set} (B : A → Set)
    {x y : A} (p : x ≡ y) (u : B x) (v : B y) → Set
  PathOver B refl u v = (u ≡ v)

  postulate
    PathOver-triv : {A B : Set} {x y : A} (p : x ≡ y) (u v : B) →
      (PathOver (λ _ → B) p u v) ≡ (u ≡ v)
  {-# REWRITE PathOver-triv #-}

  test₆ : (p : 1 ≡ 1) → PathOver (λ _ → Nat) p 2 2
  test₆ p = refl


text:
module Numeral.Real where

open import Data.Tuple
open import Logic
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Rational
open import Numeral.Rational.Oper
open import Relator.Equals
open import Type
open import Type.Quotient

-- TODO: This will not work, but it is the standard concept at least. Maybe there is a better way

record CauchySequence (a : ℕ → ℚ) : Stmt where
  field
    N : ℚ₊ → ℕ
    ∀{ε : ℚ₊}{m n : ℕ} → (m > N(ε)) → (n > N(ε)) → (‖ a(m) − a(n) ‖ < ε)

_converges-to-same_ : Σ(CauchySequence) → Σ(CauchySequence) → Stmt{Lvl.𝟎}
a converges-to-same b = lim(n ↦ Σ.left(a) − Σ.left(b)) ≡ 𝟎

ℝ : Type{Lvl.𝟎}
ℝ = Σ(CauchySequence) / (_converges-to-same_)

-- TODO: Here is another idea: https://github.com/dylanede/cubical-experiments/blob/master/scratch.agda
-- TODO: Also these: https://en.wikipedia.org/wiki/Construction_of_the_real_numbers#Construction_from_Cauchy_sequences

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------------
-- The division program is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the division program using
-- repeated subtraction (Dybjer 1985).

-- Peter Dybjer. Program verification in a logical theory of
-- constructions. In Jean-Pierre Jouannaud, editor. Functional
-- Programming Languages and Computer Architecture, volume 201 of
-- LNCS, 1985, pages 334-349. Appears in revised form as Programming
-- Methodology Group Report 26, June 1986.

module LTC-PCF.Program.Division.CorrectnessProof where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Data.Nat.Properties

import LTC-PCF.Data.Nat.Induction.NonAcc.WF
open module WFInd = LTC-PCF.Data.Nat.Induction.NonAcc.WF.WFInd

open import LTC-PCF.Program.Division.Division
open import LTC-PCF.Program.Division.Specification
open import LTC-PCF.Program.Division.Result
open import LTC-PCF.Program.Division.Totality

------------------------------------------------------------------------------
-- The division program is correct when the dividend is less than the
-- divisor.
div-x<y-correct : ∀ {i j} → N i → N j → i < j → divSpec i j (div i j)
div-x<y-correct Ni Nj i<j = div-x<y-N i<j , div-x<y-resultCorrect Ni Nj i<j

-- The division program is correct when the dividend is greater or
-- equal than the divisor.
div-x≮y-correct : ∀ {i j} → N i → N j →
                  (∀ {i'} → N i' → i' < i → divSpec i' j (div i' j)) →
                  j > zero →
                  i ≮ j →
                  divSpec i j (div i j)
div-x≮y-correct {i} {j} Ni Nj ah j>0 i≮j =
  div-x≮y-N ih i≮j , div-x≮y-resultCorrect Ni Nj ih i≮j

  where
  -- The inductive hypothesis on i ∸ j.
  ih : divSpec (i ∸ j) j (div (i ∸ j) j)
  ih = ah {i ∸ j}
          (∸-N Ni Nj)
          (x≥y→y>0→x∸y<x Ni Nj (x≮y→x≥y Ni Nj i≮j) j>0)

------------------------------------------------------------------------------
-- The division program is correct.

-- We do the well-founded induction on i and we keep j fixed.
divCorrect : ∀ {i j} → N i → N j → j > zero → divSpec i j (div i j)
divCorrect {j = j} Ni Nj j>0 = <-wfind A ih Ni
  where
  A : D → Set
  A d = divSpec d j (div d j)

  -- The inductive step doesn't use the variable i (nor Ni). To make
  -- this clear we write down the inductive step using the variables m
  -- and n.
  ih : ∀ {n} → N n → (∀ {m} → N m → m < n → A m) → A n
  ih {n} Nn ah =
     case (div-x<y-correct Nn Nj) (div-x≮y-correct Nn Nj ah j>0) (x<y∨x≮y Nn Nj)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Data.Num.Bij.Properties where

open import Data.Num.Bij renaming (_+B_ to _+_; _*B_ to _*_)

open import Data.List
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; sym; trans)
open PropEq.≡-Reasoning

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

1∷≡incrB∘*2 : ∀ m → one ∷ m ≡ incrB (*2 m)
1∷≡incrB∘*2 []         = refl
1∷≡incrB∘*2 (one ∷ ms) = cong (λ x → one ∷ x)       (1∷≡incrB∘*2 ms)
1∷≡incrB∘*2 (two ∷ ms) = cong (λ x → one ∷ incrB x) (1∷≡incrB∘*2 ms)

split-∷ : ∀ m ms → m ∷ ms ≡ (m ∷ []) + *2 ms
split-∷ m [] = refl
split-∷ one (one ∷ ns) = cong (λ x → one ∷ x)       (1∷≡incrB∘*2 ns)
split-∷ one (two ∷ ns) = cong (λ x → one ∷ incrB x) (1∷≡incrB∘*2 ns)
split-∷ two (one ∷ ns) = cong (λ x → two ∷ x)       (1∷≡incrB∘*2 ns)
split-∷ two (two ∷ ns) = cong (λ x → two ∷ incrB x) (1∷≡incrB∘*2 ns)

{-
+B-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
+B-assoc []       _ _ = refl
+B-assoc (m ∷ ms) n o =
    begin
        (m ∷ ms) + n + o
    ≡⟨ cong (λ x → x + n + o) (split-∷ m ms) ⟩
        (m ∷ []) + *2 ms + n + o
    ≡⟨ cong (λ x → x + o) (+B-assoc (m ∷ []) (*2 ms) n) ⟩
        (m ∷ []) + (*2 ms + n) + o
    ≡⟨ +B-assoc (m ∷ []) (*2 ms + n) o ⟩
        (m ∷ []) + ((*2 ms + n) + o)
    ≡⟨ cong (λ x → (m ∷ []) + x) (+B-assoc (*2 ms) n o) ⟩
        (m ∷ []) + (*2 ms + (n + o))
    ≡⟨ sym (+B-assoc (m ∷ []) (*2 ms) (n + o))  ⟩
        (m ∷ []) + *2 ms + (n + o)
    ≡⟨ cong (λ x → x + (n + o)) (sym (split-∷ m ms)) ⟩
        (m ∷ ms) + (n + o)
    ∎
+B-right-identity : ∀ n → n + [] ≡ n
+B-right-identity []       = refl
+B-right-identity (n ∷ ns) = refl

+B-comm : ∀ m n → m + n ≡ n + m
+B-comm []       n = sym (+B-right-identity n)
+B-comm (m ∷ ms) n =
    begin
        (m ∷ ms) + n
    ≡⟨ cong (λ x → x + n) (split-∷ m ms) ⟩
        (m ∷ []) + *2 ms + n
    ≡⟨ +B-comm ((m ∷ []) + *2 ms) n ⟩
        n + ((m ∷ []) + *2 ms)
    ≡⟨ cong (λ x → n + x) (sym (split-∷ m ms)) ⟩
        n + (m ∷ ms)
    ∎
{-
    begin
        (m ∷ ms) + n
    ≡⟨ cong (λ x → x + n) (split-∷ m ms) ⟩
        (m ∷ []) + *2 ms + n
    ≡⟨ +B-assoc (m ∷ []) (*2 ms) n ⟩
        (m ∷ []) + (*2 ms + n)
    ≡⟨ cong (λ x → (m ∷ []) + x) (+B-comm (*2 ms) n) ⟩
        (m ∷ []) + (n + *2 ms)
    ≡⟨ sym (+B-assoc (m ∷ []) n (*2 ms)) ⟩
        (m ∷ []) + n + *2 ms
    ≡⟨ cong (λ x → x + *2 ms) (+B-comm (m ∷ []) n) ⟩
        n + (m ∷ []) + *2 ms
    ≡⟨ +B-assoc n (m ∷ []) (*2 ms) ⟩
        n + ((m ∷ []) + *2 ms)
    ≡⟨ cong (λ x → n + x) (sym (split-∷ m ms)) ⟩
        n + (m ∷ ms)
    ∎
-}
+B-*2-distrib : ∀ m n → *2 (m + n) ≡ *2 m + *2 n
+B-*2-distrib []       n = refl
+B-*2-distrib (m ∷ ms) n =
    begin
        *2 ((m ∷ ms) + n)
    ≡⟨ cong (λ x → *2 (x + n)) (split-∷ m ms) ⟩
        *2 ((m ∷ []) + *2 ms + n)
    ≡⟨ +B-*2-distrib ((m ∷ []) + *2 ms) n ⟩
        *2 ((m ∷ []) + *2 ms) + *2 n
    ≡⟨ cong (λ x → *2 x + *2 n) (sym (split-∷ m ms)) ⟩
        *2 (m ∷ ms) + *2 n
    ∎

+B-*B-incrB : ∀ m n → m * incrB n ≡ m + m * n
+B-*B-incrB []         n = refl
+B-*B-incrB (m ∷ ms) n =
    begin
        (m ∷ ms) * incrB n
    ≡⟨ cong (λ x → x * incrB n) (split-∷ m ms) ⟩
        ((m ∷ []) + *2 ms) * incrB n
    ≡⟨ +B-*B-incrB ((m ∷ []) + *2 ms) n ⟩
        (m ∷ []) + *2 ms + ((m ∷ []) + *2 ms) * n
    ≡⟨ cong (λ x → x + x * n) (sym (split-∷ m ms)) ⟩
        (m ∷ ms) + (m ∷ ms) * n
    ∎

*B-right-[] : ∀ n → n * [] ≡ []
*B-right-[] [] = refl
*B-right-[] (one ∷ ns) = cong *2_ (*B-right-[] ns)
*B-right-[] (two ∷ ns) = cong *2_ (*B-right-[] ns)

*B-+B-distrib : ∀ m n o → (n + o) * m ≡ n * m + o * m
*B-+B-distrib m []       o = refl
*B-+B-distrib m (n ∷ ns) o =
    begin
        ((n ∷ ns) + o) * m
    ≡⟨ cong (λ x → (x + o) * m) (split-∷ n ns) ⟩
        ((n ∷ []) + *2 ns + o) * m
    ≡⟨ *B-+B-distrib m ((n ∷ []) + *2 ns) o ⟩
        ((n ∷ []) + *2 ns) * m + o * m
    ≡⟨ cong (λ x → x * m + o * m) (sym (split-∷ n ns)) ⟩
        (n ∷ ns) * m + o * m
    ∎

*B-comm : ∀ m n → m * n ≡ n * m
*B-comm []         n = sym (*B-right-[] n)
*B-comm (m ∷ ms) n =
    begin
        (m ∷ ms) * n
    ≡⟨ cong (λ x → x * n) (split-∷ m ms) ⟩
        ((m ∷ []) + *2 ms) * n
    ≡⟨ *B-comm ((m ∷ []) + *2 ms) n ⟩
        n * ((m ∷ []) + *2 ms)
    ≡⟨ cong (λ x → n * x) (sym (split-∷ m ms)) ⟩
        n * (m ∷ ms)
    ∎

{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}
{-
+B-*B-incrB : ∀ m n → m * incrB n ≡ m + m * n
+B-*B-incrB []         n = refl
+B-*B-incrB (one ∷ ms) [] = {!   !}
+B-*B-incrB (one ∷ ms) (n ∷ ns) = {!   !}
    begin
        incrB n + ms * incrB n
    ≡⟨ cong (λ x → incrB n + x) (+B-*B-incrB ms n) ⟩
        incrB n + (ms + ms * n)
    ≡⟨ sym (+B-assoc (incrB n) ms (ms * n)) ⟩
        incrB n + ms + ms * n
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        (one ∷ []) + *2 ms + (n + ms * n)
    ≡⟨ cong (λ x → x + (n + ms * n)) (sym (split-∷ one ms)) ⟩
        (one ∷ ms) + (n + ms * n)
    ∎
+B-*B-incrB (two ∷ ms) n =
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!    !}
    ∎
-}
{-
    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.OrderedCommMonoid.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP using (TypeWithStr)

open import Cubical.Data.Sigma

open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.OrderedCommMonoid.Base

open import Cubical.Relation.Binary.Poset

private
  variable
    ℓ ℓ' ℓ'' : Level

module _
    (M : OrderedCommMonoid ℓ ℓ')
    (P : ⟨ M ⟩ → hProp ℓ'')
    where
  open OrderedCommMonoidStr (snd M)
  module _
    (·Closed : (x y : ⟨ M ⟩) → ⟨ P x ⟩ → ⟨ P y ⟩ → ⟨ P (x · y) ⟩)
    (εContained : ⟨ P ε ⟩)
    where
    private
      subtype = Σ[ x ∈ ⟨ M ⟩ ] ⟨ P x ⟩
      submonoid =  makeSubCommMonoid (OrderedCommMonoid→CommMonoid M) P ·Closed εContained
      _≤ₛ_ : (x y : ⟨ submonoid ⟩) → Type ℓ'
      x ≤ₛ y = (fst x) ≤ (fst y)
      pres≤ : (x y : ⟨ submonoid ⟩) (x≤y : x ≤ₛ y) → (fst x) ≤ (fst y)
      pres≤ x y x≤y = x≤y

    makeOrderedSubmonoid : OrderedCommMonoid _ ℓ'
    fst makeOrderedSubmonoid = subtype
    OrderedCommMonoidStr._≤_ (snd makeOrderedSubmonoid) = _≤ₛ_
    OrderedCommMonoidStr._·_ (snd makeOrderedSubmonoid) = CommMonoidStr._·_ (snd submonoid)
    OrderedCommMonoidStr.ε (snd makeOrderedSubmonoid) = CommMonoidStr.ε (snd submonoid)
    OrderedCommMonoidStr.isOrderedCommMonoid (snd makeOrderedSubmonoid) =
      IsOrderedCommMonoidFromIsCommMonoid
        (CommMonoidStr.isCommMonoid (snd submonoid))
        (λ x y → is-prop-valued (fst x) (fst y))
        (λ x → is-refl (fst x))
        (λ x y z → is-trans (fst x) (fst y) (fst z))
        (λ x y x≤y y≤x
          → Σ≡Prop (λ x → snd (P x))
                   (is-antisym (fst x) (fst y) (pres≤ x y x≤y) (pres≤ y x y≤x)))
        (λ x y z x≤y → MonotoneR (pres≤ x y x≤y))
        λ x y z x≤y → MonotoneL (pres≤ x y x≤y)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.conv.elim:100 #-}
module Issue814 where

record IsMonoid (M : Set) : Set where
  field
    unit : M
    _*_ : M → M → M

record Monoid : Set₁ where
  field
    carrier : Set
    is-mon : IsMonoid carrier

record Structure (Struct : Set₁)
                 (HasStruct : Set → Set)
                 (carrier : Struct → Set) : Set₁ where
  field
    has-struct : (X : Struct) → HasStruct (carrier X)

mon-mon-struct : Structure Monoid IsMonoid Monoid.carrier
mon-mon-struct = record
  { has-struct = Monoid.is-mon }

mon-mon-struct' : Structure Monoid IsMonoid Monoid.carrier
mon-mon-struct' = record
  { has-struct = Monoid.is-mon }

unit : {Struct : Set₁}{C : Struct → Set}
     → ⦃ X : Struct ⦄
     → ⦃ struct : Structure Struct IsMonoid C ⦄
     → C X
unit {Struct}{C} ⦃ X ⦄ ⦃ struct ⦄ = IsMonoid.unit (Structure.has-struct struct X)

f : (M : Monoid) → Monoid.carrier M
f M = unit

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

-- This used to crash, but should only produce unsolved metas.

max_stars_repo_name: larrytheliquid/agda


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

module Properties.Subtyping where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
open import Properties.Equality using (_≢_)
open import Properties.Functions using (_∘_)
open import Properties.Product using (_×_; _,_)

-- Language membership is decidable
dec-language : ∀ T t → Either (¬Language T t) (Language T t)
dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ()))
dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
dec-language nil (scalar nil) = Right (scalar nil)
dec-language nil function = Left (scalar-function nil)
dec-language nil (function-ok s t) = Left (scalar-function-ok nil)
dec-language nil (function-err t) = Left (scalar-function-err nil)
dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
dec-language boolean (scalar boolean) = Right (scalar boolean)
dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
dec-language boolean function = Left (scalar-function boolean)
dec-language boolean (function-ok s t) = Left (scalar-function-ok boolean)
dec-language boolean (function-err t) = Left (scalar-function-err boolean)
dec-language number (scalar number) = Right (scalar number)
dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
dec-language number function = Left (scalar-function number)
dec-language number (function-ok s t) = Left (scalar-function-ok number)
dec-language number (function-err t) = Left (scalar-function-err number)
dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
dec-language string (scalar string) = Right (scalar string)
dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
dec-language string function = Left (scalar-function string)
dec-language string (function-ok s t) = Left (scalar-function-ok string)
dec-language string (function-err t) = Left (scalar-function-err string)
dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
dec-language (T₁ ⇒ T₂) function = Right function
dec-language (T₁ ⇒ T₂) (function-ok s t) = cond (Right ∘ function-ok₁) (λ p → mapLR (function-ok p) function-ok₂ (dec-language T₂ t)) (dec-language T₁ s)
dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
dec-language never t = Left never
dec-language unknown t = Right unknown
dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
dec-language nil (function-tgt t) = Left (scalar-function-tgt nil)
dec-language (T₁ ⇒ T₂) (function-tgt t) = mapLR function-tgt function-tgt (dec-language T₂ t)
dec-language boolean (function-tgt t) = Left (scalar-function-tgt boolean)
dec-language number (function-tgt t) = Left (scalar-function-tgt number)
dec-language string (function-tgt t) = Left (scalar-function-tgt string)

-- ¬Language T is the complement of Language T
language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q
language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q
language-comp t (left p) (q₁ , q₂) = language-comp t p q₁
language-comp t (right p) (q₁ , q₂) = language-comp t p q₂
language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
language-comp (scalar s) never (scalar ())
language-comp function (scalar-function ()) function
language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₁ p)
language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₁ q) = language-comp s q p₁
language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₂ q) = language-comp t p₂ q
language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
language-comp (function-tgt t) (scalar-function-tgt ()) (function-tgt q)
language-comp (function-tgt t) (function-tgt p) (function-tgt q) = language-comp t p q

-- ≮: is the complement of <:
¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
¬≮:-impl-<: {T} {U} p t q with dec-language U t
¬≮:-impl-<: {T} {U} p t q | Left r = CONTRADICTION (p (witness t q r))
¬≮:-impl-<: {T} {U} p t q | Right r = r

<:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U)
<:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)

<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t
<:-impl-⊇ {T} p t q with dec-language T t
<:-impl-⊇ {_} p t q | Left r = r
<:-impl-⊇ {_} p t q | Right r = CONTRADICTION (language-comp t q (p t r))

-- reflexivity
≮:-refl : ∀ {T} → ¬(T ≮: T)
≮:-refl (witness t p q) = language-comp t q p

<:-refl : ∀ {T} → (T <: T)
<:-refl = ¬≮:-impl-<: ≮:-refl

-- transititivity
≮:-trans-≡ : ∀ {S T U} → (S ≮: T) → (T ≡ U) → (S ≮: U)
≮:-trans-≡ p refl = p

<:-trans-≡ : ∀ {S T U} → (S <: T) → (T ≡ U) → (S <: U)
<:-trans-≡ p refl = p

≡-impl-<: : ∀ {T U} → (T ≡ U) → (T <: U)
≡-impl-<: refl = <:-refl

≡-trans-≮: : ∀ {S T U} → (S ≡ T) → (T ≮: U) → (S ≮: U)
≡-trans-≮: refl p = p

≡-trans-<: : ∀ {S T U} → (S ≡ T) → (T <: U) → (S <: U)
≡-trans-<: refl p = p

≮:-trans : ∀ {S T U} → (S ≮: U) → Either (S ≮: T) (T ≮: U)
≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t)

<:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U)
<:-trans p q t r = q t (p t r)

<:-trans-≮: : ∀ {S T U} → (S <: T) → (S ≮: U) → (T ≮: U)
<:-trans-≮: p (witness t q r) = witness t (p t q) r

≮:-trans-<: : ∀ {S T U} → (S ≮: U) → (T <: U) → (S ≮: T)
≮:-trans-<: (witness t p q) r = witness t p (<:-impl-⊇ r t q)

-- Properties of union

<:-union : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∪ S) <: (T ∪ U))
<:-union p q t (left r) = left (p t r)
<:-union p q t (right r) = right (q t r)

<:-∪-left : ∀ {S T} → S <: (S ∪ T)
<:-∪-left t p = left p

<:-∪-right : ∀ {S T} → T <: (S ∪ T)
<:-∪-right t p = right p

<:-∪-lub : ∀ {S T U} → (S <: U) → (T <: U) → ((S ∪ T) <: U)
<:-∪-lub p q t (left r) = p t r
<:-∪-lub p q t (right r) = q t r

<:-∪-symm : ∀ {T U} → (T ∪ U) <: (U ∪ T)
<:-∪-symm t (left p) = right p
<:-∪-symm t (right p) = left p

<:-∪-assocl : ∀ {S T U} → (S ∪ (T ∪ U)) <: ((S ∪ T) ∪ U)
<:-∪-assocl t (left p) = left (left p)
<:-∪-assocl t (right (left p)) = left (right p)
<:-∪-assocl t (right (right p)) = right p

<:-∪-assocr : ∀ {S T U} → ((S ∪ T) ∪ U) <: (S ∪ (T ∪ U))
<:-∪-assocr t (left (left p)) = left p
<:-∪-assocr t (left (right p)) = right (left p)
<:-∪-assocr t (right p) = right (right p)

≮:-∪-left : ∀ {S T U} → (S ≮: U) → ((S ∪ T) ≮: U)
≮:-∪-left (witness t p q) = witness t (left p) q

≮:-∪-right : ∀ {S T U} → (T ≮: U) → ((S ∪ T) ≮: U)
≮:-∪-right (witness t p q) = witness t (right p) q

≮:-left-∪ : ∀ {S T U} → (S ≮: (T ∪ U)) → (S ≮: T)
≮:-left-∪ (witness t p (q₁ , q₂)) = witness t p q₁

≮:-right-∪ : ∀ {S T U} → (S ≮: (T ∪ U)) → (S ≮: U)
≮:-right-∪ (witness t p (q₁ , q₂)) = witness t p q₂

-- Properties of intersection

<:-intersect : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∩ S) <: (T ∩ U))
<:-intersect p q t (r₁ , r₂) = (p t r₁ , q t r₂)

<:-∩-left : ∀ {S T} → (S ∩ T) <: S
<:-∩-left t (p , _) = p

<:-∩-right : ∀ {S T} → (S ∩ T) <: T
<:-∩-right t (_ , p) = p

<:-∩-glb : ∀ {S T U} → (S <: T) → (S <: U) → (S <: (T ∩ U))
<:-∩-glb p q t r = (p t r , q t r)

<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
<:-∩-symm t (p₁ , p₂) = (p₂ , p₁)

<:-∩-assocl : ∀ {S T U} → (S ∩ (T ∩ U)) <: ((S ∩ T) ∩ U)
<:-∩-assocl t (p , (p₁ , p₂)) = (p , p₁) , p₂

<:-∩-assocr : ∀ {S T U} → ((S ∩ T) ∩ U) <: (S ∩ (T ∩ U))
<:-∩-assocr t ((p , p₁) , p₂) = p , (p₁ , p₂)

≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
≮:-∩-left (witness t p q) = witness t p (left q)

≮:-∩-right : ∀ {S T U} → (S ≮: U) → (S ≮: (T ∩ U))
≮:-∩-right (witness t p q) = witness t p (right q)

-- Distribution properties
<:-∩-distl-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U))
<:-∩-distl-∪ t (p₁ , left p₂) = left (p₁ , p₂)
<:-∩-distl-∪ t (p₁ , right p₂) = right (p₁ , p₂)

∩-distl-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U))
∩-distl-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂)
∩-distl-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂)

<:-∩-distr-∪ : ∀ {S T U} → ((S ∪ T) ∩ U) <:  ((S ∩ U) ∪ (T ∩ U))
<:-∩-distr-∪ t (left p₁ , p₂) = left (p₁ , p₂)
<:-∩-distr-∪ t (right p₁ , p₂) = right (p₁ , p₂)

∩-distr-∪-<: : ∀ {S T U} → ((S ∩ U) ∪ (T ∩ U)) <: ((S ∪ T) ∩ U)
∩-distr-∪-<: t (left (p₁ , p₂)) = (left p₁ , p₂)
∩-distr-∪-<: t (right (p₁ , p₂)) = (right p₁ , p₂)

<:-∪-distl-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U))
<:-∪-distl-∩ t (left p) = (left p , left p)
<:-∪-distl-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂)

∪-distl-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U))
∪-distl-∩-<: t (left p₁ , p₂) = left p₁
∪-distl-∩-<: t (right p₁ , left p₂) = left p₂
∪-distl-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂)

<:-∪-distr-∩ : ∀ {S T U} → ((S ∩ T) ∪ U) <: ((S ∪ U) ∩ (T ∪ U))
<:-∪-distr-∩ t (left (p₁ , p₂)) = left p₁ , left p₂
<:-∪-distr-∩ t (right p) = (right p , right p)

∪-distr-∩-<: : ∀ {S T U} → ((S ∪ U) ∩ (T ∪ U)) <: ((S ∩ T) ∪ U)
∪-distr-∩-<: t (left p₁ , left p₂) = left (p₁ , p₂)
∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
∪-distr-∩-<: t (right p₁ , p₂) = right p₁

∩-<:-∪ : ∀ {S T} → (S ∩ T) <: (S ∪ T)
∩-<:-∪ t (p , _) = left p

-- Properties of functions
<:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U)
<:-function p q function function = function
<:-function p q (function-ok s t) (function-ok₁ r) = function-ok₁ (<:-impl-⊇ p s r)
<:-function p q (function-ok s t) (function-ok₂ r) = function-ok₂ (q t r)
<:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r)
<:-function p q (function-tgt t) (function-tgt r) = function-tgt (q t r)

<:-function-∩-∩ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∩ S) ⇒ (T ∩ U))
<:-function-∩-∩ function (function , function) = function
<:-function-∩-∩ (function-ok s t) (function-ok₁ p , q) = function-ok₁ (left p)
<:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₁ q) = function-ok₁ (right q)
<:-function-∩-∩ (function-ok s t) (function-ok₂ p , function-ok₂ q) = function-ok₂ (p , q)
<:-function-∩-∩ (function-err s) (function-err p , q) = function-err (left p)
<:-function-∩-∩ (function-tgt s) (function-tgt p , function-tgt q) = function-tgt (p , q)

<:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U))
<:-function-∩-∪ function (function , function) = function
<:-function-∩-∪ (function-ok s t) (function-ok₁ p₁ , function-ok₁ p₂) = function-ok₁ (p₁ , p₂)
<:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂)
<:-function-∩-∪ (function-ok s t) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁)
<:-function-∩-∪ (function-err s) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
<:-function-∩-∪ (function-tgt t) (function-tgt p , q) = function-tgt (left p)

<:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
<:-function-∩ function (function , function) = function
<:-function-∩ (function-ok s t) (p₁ , function-ok₁ p₂) = function-ok₁ p₂
<:-function-∩ (function-ok s t) (function-ok₁ p₁ , p₂) = function-ok₁ p₁
<:-function-∩ (function-ok s t) (function-ok₂ p₁ , function-ok₂ p₂) = function-ok₂ (p₁ , p₂)
<:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂
<:-function-∩ (function-tgt t) (function-tgt p₁ , function-tgt p₂) = function-tgt (p₁ , p₂)

<:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U))
<:-function-∪ function (left function) = function
<:-function-∪ (function-ok s t) (left (function-ok₁ p)) = function-ok₁ (left p)
<:-function-∪ (function-ok s t) (left (function-ok₂ p)) = function-ok₂ (left p)
<:-function-∪ (function-err s) (left (function-err p)) = function-err (left p)
<:-function-∪ (scalar s) (left (scalar ()))
<:-function-∪ function (right function) = function
<:-function-∪ (function-ok s t) (right (function-ok₁ p)) = function-ok₁ (right p)
<:-function-∪ (function-ok s t) (right (function-ok₂ p)) = function-ok₂ (right p)
<:-function-∪ (function-err s) (right (function-err x)) = function-err (right x)
<:-function-∪ (scalar s) (right (scalar ()))
<:-function-∪ (function-tgt t) (left (function-tgt p)) = function-tgt (left p)
<:-function-∪ (function-tgt t) (right (function-tgt p)) = function-tgt (right p)

<:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U))
<:-function-∪-∩ function function = left function
<:-function-∪-∩ (function-ok s t) (function-ok₁ (left p)) = left (function-ok₁ p)
<:-function-∪-∩ (function-ok s t) (function-ok₂ (left p)) = left (function-ok₂ p)
<:-function-∪-∩ (function-ok s t) (function-ok₁ (right p)) = right (function-ok₁ p)
<:-function-∪-∩ (function-ok s t) (function-ok₂ (right p)) = right (function-ok₂ p)
<:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p)
<:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)
<:-function-∪-∩ (function-tgt t) (function-tgt (left p)) = left (function-tgt p)
<:-function-∪-∩ (function-tgt t) (function-tgt (right p)) = right (function-tgt p)

<:-function-left : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R <: S)
<:-function-left {R} {S} p s Rs with dec-language S s
<:-function-left p s Rs | Right Ss = Ss
<:-function-left p s Rs | Left ¬Ss with p (function-err s) (function-err ¬Ss)
<:-function-left p s Rs | Left ¬Ss | function-err ¬Rs = CONTRADICTION (language-comp s ¬Rs Rs)

<:-function-right : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (T <: U)
<:-function-right p t Tt with p (function-tgt t) (function-tgt Tt)
<:-function-right p t Tt | function-tgt St = St

≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p)

≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-right (witness t p q) = witness (function-tgt t) (function-tgt p) (function-tgt q)

-- Properties of scalars
skalar-function-ok : ∀ {s t} → (¬Language skalar (function-ok s t))
skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))

scalar-<: : ∀ {S T} → (s : Scalar S) → Language T (scalar s) → (S <: T)
scalar-<: number p (scalar number) (scalar number) = p
scalar-<: boolean p (scalar boolean) (scalar boolean) = p
scalar-<: string p (scalar string) (scalar string) = p
scalar-<: nil p (scalar nil) (scalar nil) = p

scalar-∩-function-<:-never : ∀ {S T U} → (Scalar S) → ((T ⇒ U) ∩ S) <: never
scalar-∩-function-<:-never number .(scalar number) (() , scalar number)
scalar-∩-function-<:-never boolean .(scalar boolean) (() , scalar boolean)
scalar-∩-function-<:-never string .(scalar string) (() , scalar string)
scalar-∩-function-<:-never nil .(scalar nil) (() , scalar nil)

function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
function-≮:-scalar s = witness function function (scalar-function s)

scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T))
scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s)

unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U)
unknown-≮:-scalar s = witness function unknown (scalar-function s)

scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never)
scalar-≮:-never s = witness (scalar s) (scalar s) never

scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U)
scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)

scalar-≢-∩-<:-never : ∀ {T U V} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ∩ U) <: V
scalar-≢-∩-<:-never s t p u (scalar s₁ , scalar s₂) = CONTRADICTION (p refl)

skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
skalar-scalar number = left (scalar number)
skalar-scalar boolean = right (right (right (scalar boolean)))
skalar-scalar string = right (left (scalar string))
skalar-scalar nil = right (right (left (scalar nil)))

-- Properties of unknown and never
unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U)
unknown-≮: (witness t p q) = witness t unknown q

never-≮: : ∀ {T U} → (T ≮: U) → (T ≮: never)
never-≮: (witness t p q) = witness t p never

unknown-≮:-never : (unknown ≮: never)
unknown-≮:-never = witness (scalar nil) unknown never

unknown-≮:-function : ∀ {S T} → (unknown ≮: (S ⇒ T))
unknown-≮:-function = witness (scalar nil) unknown (function-scalar nil)

function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never)
function-≮:-never = witness function function never

<:-never : ∀ {T} → (never <: T)
<:-never t (scalar ())

≮:-never-left : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: T) → (S ∩ U) ≮: never
≮:-never-left p (witness t q₁ q₂) with p t q₁
≮:-never-left p (witness t q₁ q₂) | left r = CONTRADICTION (language-comp t q₂ r)
≮:-never-left p (witness t q₁ q₂) | right r = witness t (q₁ , r) never

≮:-never-right : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: U) → (S ∩ T) ≮: never
≮:-never-right p (witness t q₁ q₂) with p t q₁
≮:-never-right p (witness t q₁ q₂) | left r = witness t (q₁ , r) never
≮:-never-right p (witness t q₁ q₂) | right r = CONTRADICTION (language-comp t q₂ r)

<:-unknown : ∀ {T} → (T <: unknown)
<:-unknown t p = unknown

<:-everything : unknown <: ((never ⇒ unknown) ∪ skalar)
<:-everything (scalar s) p = right (skalar-scalar s)
<:-everything function p = left function
<:-everything (function-ok s t) p = left (function-ok₁ never)
<:-everything (function-err s) p = left (function-err never)
<:-everything (function-tgt t) p = left (function-tgt unknown)

-- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
-- defines a "set-theoretic" model (sec 2.5)
-- Unfortunately we don't quite have this property, due to uninhabited types,
-- for example (never -> T) is equivalent to (never -> U)
-- when types are interpreted as sets of syntactic values.

_⊆_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set
(P ⊆ Q) = ∀ a → (P a) → (Q a)

_⊗_ : ∀ {A B : Set} → (A → Set) → (B → Set) → ((A × B) → Set)
(P ⊗ Q) (a , b) = (P a) × (Q b)

Comp : ∀ {A : Set} → (A → Set) → (A → Set)
Comp P a = ¬(P a)

Lift : ∀ {A : Set} → (A → Set) → (Maybe A → Set)
Lift P nothing = ⊥
Lift P (just a) = P a

set-theoretic-if : ∀ {S₁ T₁ S₂ T₂} →

  -- This is the "if" part of being a set-theoretic model
  -- though it uses the definition from Frisch's thesis
  -- rather than from the Gentle Introduction. The difference
  -- being the presence of Lift, (written D_Ω in Defn 4.2 of
  -- https://www.cduce.org/papers/frisch_phd.pdf).
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) →
  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂))))

set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T₂u) = q (t , just u) Qtu (S₁t , ¬T₁u) where

  S₁t : Language S₁ t
  S₁t with dec-language S₁ t
  S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
  S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
  S₁t | Right r = r

  ¬T₁u : ¬(Language T₁ u)
  ¬T₁u T₁u with p (function-ok t u) (function-ok₂ T₁u)
  ¬T₁u T₁u | function-ok₁ ¬S₂t = language-comp t ¬S₂t S₂t
  ¬T₁u T₁u | function-ok₂ T₂u = ¬T₂u T₂u

set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _) = q (t , nothing) Qt- (S₁t , λ ()) where

  S₁t : Language S₁ t
  S₁t with dec-language S₁ t
  S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
  S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
  S₁t | Right r = r

not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →

  -- We don't quite have that this is a set-theoretic model
  -- it's only true when Language S₂ is inhabited
  -- in particular it's not true when S₂ is never,
  ∀ s₂ → Language S₂ s₂ →

  -- This is the "only if" part of being a set-theoretic model
  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) →
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))

not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ S₂s₂ p = r where

  Q : (Tree × Maybe Tree) → Set
  Q (t , just u) = Either (¬Language S₁ t) (Language T₁ u)
  Q (t , nothing) = ¬Language S₁ t

  q : Q ⊆ Comp(Language S₁ ⊗ Comp(Lift(Language T₁)))
  q (t , just u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
  q (t , just u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
  q (t , nothing) ¬S₁t (S₁t , _) = language-comp t ¬S₁t S₁t

  r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)
  r function function = function
  r (function-err s) (function-err ¬S₁s) with dec-language S₂ s
  r (function-err s) (function-err ¬S₁s) | Left ¬S₂s = function-err ¬S₂s
  r (function-err s) (function-err ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ()))
  r (function-ok s t) (function-ok₁ ¬S₁s) with dec-language S₂ s
  r (function-ok s t) (function-ok₁ ¬S₁s) | Left ¬S₂s = function-ok₁ ¬S₂s
  r (function-ok s t) (function-ok₁ ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ()))
  r (function-ok s t) (function-ok₂ T₁t) with dec-language T₂ t
  r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t with dec-language S₂ s
  r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Left ¬S₂s = function-ok₁ ¬S₂s
  r (function-ok s t) (function-ok₂ T₁t) | Left ¬T₂t | Right S₂s = CONTRADICTION (p Q q (s , just t) (Right T₁t) (S₂s , language-comp t ¬T₂t))
  r (function-ok s t) (function-ok₂ T₁t) | Right T₂t = function-ok₂ T₂t
  r (function-tgt t) (function-tgt T₁t) with dec-language T₂ t
  r (function-tgt t) (function-tgt T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
  r (function-tgt t) (function-tgt T₁t) | Right T₂t = function-tgt T₂t

-- A counterexample when the argument type is empty.

set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language number))) → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language string))))
set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)

set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
set-theoretic-counterexample-two = witness (function-tgt (scalar number)) (function-tgt (scalar number)) (function-tgt (scalar-scalar number string (λ ())))

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


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

module moveerase where
  -- type actions don't change the term other than moving the cursor
  -- around
  moveeraset : {t t' : τ̂} {δ : direction} →
            (t + move δ +> t') →
            (t ◆t) == (t' ◆t)
  moveeraset TMArrChild1 = refl
  moveeraset TMArrChild2 = refl
  moveeraset TMArrParent1 = refl
  moveeraset TMArrParent2 = refl
  moveeraset (TMArrZip1 {t2 = t2} m) = ap1 (λ x → x ==> t2) (moveeraset m)
  moveeraset (TMArrZip2 {t1 = t1} m) = ap1 (λ x → t1 ==> x) (moveeraset m)

  -- the actual movements don't change the erasure
  moveerase : {e e' : ê} {δ : direction} →
            (e + move δ +>e e') →
            (e ◆e) == (e' ◆e)
  moveerase EMAscChild1 = refl
  moveerase EMAscChild2 = refl
  moveerase EMAscParent1 = refl
  moveerase EMAscParent2 = refl
  moveerase EMLamChild1 = refl
  moveerase EMLamParent = refl
  moveerase EMPlusChild1 = refl
  moveerase EMPlusChild2 = refl
  moveerase EMPlusParent1 = refl
  moveerase EMPlusParent2 = refl
  moveerase EMApChild1 = refl
  moveerase EMApChild2 = refl
  moveerase EMApParent1 = refl
  moveerase EMApParent2 = refl
  moveerase EMNEHoleChild1 = refl
  moveerase EMNEHoleParent = refl

  -- this form is essentially the same as above, but for judgemental
  -- erasure, which is sometimes more convenient.
  moveerasee' : {e e' : ê} {e◆ : ė} {δ : direction} →
            erase-e e e◆ →
            (e + move δ +>e e') →
            erase-e e' e◆
  moveerasee' er1 m with erase-e◆ er1
  ... | refl = ◆erase-e _ _ (! (moveerase m))

  moveeraset' : ∀{ t t◆ t'' δ} →
                 erase-t t t◆ →
                 t + move δ +> t'' →
                 erase-t t'' t◆
  moveeraset' er m with erase-t◆ er
  moveeraset' er m | refl = ◆erase-t _ _ (! (moveeraset m))

  -- movements don't change either the type or expression under expression
  -- actions
  mutual
    moveerase-synth : ∀{Γ e e' e◆ t t' δ } →
                       (er : erase-e e e◆) →
                       Γ ⊢ e◆ => t →
                       Γ ⊢ e => t ~ move δ ~> e' => t' →
                       (e ◆e) == (e' ◆e) × t == t'
    moveerase-synth er wt (SAMove x) = moveerase x , refl
    moveerase-synth (EEAscL er) (SAsc x) (SAZipAsc1 x₁) = ap1 (λ q → q ·: _) (moveerase-ana er x x₁) , refl
    moveerase-synth er wt (SAZipAsc2 x x₁ x₂ x₃)
      with (moveeraset x)
    ... | qq = ap1 (λ q → _ ·: q) qq , eq-ert-trans qq x₂ x₁
    moveerase-synth (EEApL er) (SAp wt x x₁) (SAZipApArr x₂ x₃ x₄ d x₅)
      with erasee-det x₃ er
    ... | refl with synthunicity wt x₄
    ... | refl with moveerase-synth er x₄ d
    ... | pp , refl with matcharrunicity x x₂
    ... | refl = (ap1 (λ q → q ∘ _) pp ) , refl
    moveerase-synth (EEApR er) (SAp wt x x₁) (SAZipApAna x₂ x₃ x₄)
      with synthunicity x₃ wt
    ... | refl with matcharrunicity x x₂
    ... | refl = ap1 (λ q → _ ∘ q)  (moveerase-ana er x₁ x₄ ) , refl
    moveerase-synth (EEPlusL er) (SPlus x x₁) (SAZipPlus1 x₂) = ap1 (λ q → q ·+ _) (moveerase-ana er x x₂)  , refl
    moveerase-synth (EEPlusR er) (SPlus x x₁) (SAZipPlus2 x₂) = ap1 (λ q → _ ·+ q) (moveerase-ana er x₁ x₂) , refl
    moveerase-synth er wt (SAZipHole x x₁ d) = ap1 ⦇⌜_⌟⦈ (π1 (moveerase-synth x x₁ d)) , refl

    moveerase-ana : ∀{Γ e e' e◆ t δ } →
                      (er : erase-e e e◆) →
                      Γ ⊢ e◆ <= t →
                      Γ ⊢ e ~ move δ ~> e' ⇐ t →
                      (e ◆e) == (e' ◆e)
    moveerase-ana er wt (AASubsume x x₁ x₂ x₃) = π1 (moveerase-synth x x₁ x₂)
    moveerase-ana er wt (AAMove x) = moveerase x
    moveerase-ana (EELam er) (ASubsume () x₂) _
    moveerase-ana (EELam er) (ALam x₁ x₂ wt) (AAZipLam x₃ x₄ d) with matcharrunicity x₂ x₄
    ... | refl =  ap1 (λ q → ·λ _ q) (moveerase-ana er wt d)


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

open import Cubical.Core.Everything

open import Cubical.Functions.Involution

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

open import Cubical.Data.Bool.Base
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

notnot : ∀ x → not (not x) ≡ x
notnot true  = refl
notnot false = refl

notIsEquiv : isEquiv not
notIsEquiv = involIsEquiv {f = not} notnot

notEquiv : Bool ≃ Bool
notEquiv = involEquiv {f = not} notnot

notEq : Bool ≡ Bool
notEq = involPath {f = not} notnot

private
  variable
    ℓ : Level

  -- This computes to false as expected
  nfalse : Bool
  nfalse = transp (λ i → notEq i) i0 true

  -- Sanity check
  nfalsepath : nfalse ≡ false
  nfalsepath = refl

K-Bool
  : (P : {b : Bool} → b ≡ b → Type ℓ)
  → (∀{b} → P {b} refl)
  → ∀{b} → (q : b ≡ b) → P q
K-Bool P Pr {false} = J (λ{ false q → P q ; true _ → Lift ⊥ }) Pr
K-Bool P Pr {true}  = J (λ{ true q → P q ; false _ → Lift ⊥ }) Pr

isSetBool : isSet Bool
isSetBool a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool (refl ≡_) refl)

true≢false : ¬ true ≡ false
true≢false p = subst (λ b → if b then Bool else ⊥) p true

false≢true : ¬ false ≡ true
false≢true p = subst (λ b → if b then ⊥ else Bool) p true

not≢const : ∀ x → ¬ not x ≡ x
not≢const false = true≢false
not≢const true  = false≢true

zeroˡ : ∀ x → true or x ≡ true
zeroˡ false = refl
zeroˡ true  = refl

zeroʳ : ∀ x → x or true ≡ true
zeroʳ false = refl
zeroʳ true  = refl

or-identityˡ : ∀ x → false or x ≡ x
or-identityˡ false = refl
or-identityˡ true  = refl

or-identityʳ : ∀ x → x or false ≡ x
or-identityʳ false = refl
or-identityʳ true  = refl

or-comm      : ∀ x y → x or y ≡ y or x
or-comm false y =
  false or y ≡⟨ or-identityˡ y ⟩
  y          ≡⟨ sym (or-identityʳ y) ⟩
  y or false ∎
or-comm true y =
  true or y ≡⟨ zeroˡ y ⟩
  true      ≡⟨ sym (zeroʳ y) ⟩
  y or true ∎

or-assoc     : ∀ x y z → x or (y or z) ≡ (x or y) or z
or-assoc false y z =
  false or (y or z)   ≡⟨ or-identityˡ _ ⟩
  y or z              ≡[ i ]⟨ or-identityˡ y (~ i) or z ⟩
  ((false or y) or z) ∎
or-assoc true y z  =
 true or (y or z)  ≡⟨ zeroˡ _ ⟩
  true             ≡⟨ sym (zeroˡ _) ⟩
  true or z        ≡[ i ]⟨ zeroˡ y (~ i) or z ⟩
  (true or y) or z ∎

or-idem      : ∀ x → x or x ≡ x
or-idem false = refl
or-idem true  = refl

⊕-identityʳ : ∀ x → x ⊕ false ≡ x
⊕-identityʳ false = refl
⊕-identityʳ true = refl

⊕-comm : ∀ x y → x ⊕ y ≡ y ⊕ x
⊕-comm false false = refl
⊕-comm false true  = refl
⊕-comm true  false = refl
⊕-comm true  true  = refl

⊕-assoc : ∀ x y z → x ⊕ (y ⊕ z) ≡ (x ⊕ y) ⊕ z
⊕-assoc false y z = refl
⊕-assoc true false z = refl
⊕-assoc true true z = notnot z

not-⊕ˡ : ∀ x y → not (x ⊕ y) ≡ not x ⊕ y
not-⊕ˡ false y = refl
not-⊕ˡ true  y = notnot y

⊕-invol : ∀ x y → x ⊕ (x ⊕ y) ≡ y
⊕-invol false x = refl
⊕-invol true  x = notnot x

isEquiv-⊕ : ∀ x → isEquiv (x ⊕_)
isEquiv-⊕ x = involIsEquiv (⊕-invol x)

⊕-Path : ∀ x → Bool ≡ Bool
⊕-Path x = involPath {f = x ⊕_} (⊕-invol x)

⊕-Path-refl : ⊕-Path false ≡ refl
⊕-Path-refl = isInjectiveTransport refl

¬transportNot : ∀(P : Bool ≡ Bool) b → ¬ (transport P (not b) ≡ transport P b)
¬transportNot P b eq = not≢const b sub
  where
  sub : not b ≡ b
  sub = subst {A = Bool → Bool} (λ f → f (not b) ≡ f b)
          (λ i c → transport⁻Transport P c i) (cong (transport⁻ P) eq)

module BoolReflection where
  data Table (A : Type₀) (P : Bool ≡ A) : Type₀ where
    inspect : (b c : A)
            → transport P false ≡ b
            → transport P true ≡ c
            → Table A P

  table : ∀ P → Table Bool P
  table = J Table (inspect false true refl refl)

  reflLemma : (P : Bool ≡ Bool)
         → transport P false ≡ false
         → transport P true ≡ true
         → transport P ≡ transport (⊕-Path false)
  reflLemma P ff tt i false = ff i
  reflLemma P ff tt i true = tt i

  notLemma : (P : Bool ≡ Bool)
         → transport P false ≡ true
         → transport P true ≡ false
         → transport P ≡ transport (⊕-Path true)
  notLemma P ft tf i false = ft i
  notLemma P ft tf i true  = tf i

  categorize : ∀ P → transport P ≡ transport (⊕-Path (transport P false))
  categorize P with table P
  categorize P | inspect false true p q
    = subst (λ b → transport P ≡ transport (⊕-Path b)) (sym p) (reflLemma P p q)
  categorize P | inspect true false p q
    = subst (λ b → transport P ≡ transport (⊕-Path b)) (sym p) (notLemma P p q)
  categorize P | inspect false false p q
    = rec (¬transportNot P false (q ∙ sym p))
  categorize P | inspect true true p q
    = rec (¬transportNot P false (q ∙ sym p))

  ⊕-complete : ∀ P → P ≡ ⊕-Path (transport P false)
  ⊕-complete P = isInjectiveTransport (categorize P)

  ⊕-comp : ∀ p q → ⊕-Path p ∙ ⊕-Path q ≡ ⊕-Path (q ⊕ p)
  ⊕-comp p q = isInjectiveTransport (λ i x → ⊕-assoc q p x i)

  open Iso

  reflectIso : Iso Bool (Bool ≡ Bool)
  reflectIso .fun = ⊕-Path
  reflectIso .inv P = transport P false
  reflectIso .leftInv = ⊕-identityʳ
  reflectIso .rightInv P = sym (⊕-complete P)

  reflectEquiv : Bool ≃ (Bool ≡ Bool)
  reflectEquiv = isoToEquiv reflectIso

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:
-- There were some serious bugs in the termination checker
-- which were hidden by the fact that it didn't go inside
-- records. They should be fixed now.
module Issue222 where

record R (A : Set) : Set where
  module M (a : A) where

-- Bug.agda:4,17-18
-- Panic: unbound variable A
-- when checking that the expression A has type _5


text:
-- {-# OPTIONS -v scope.decl.trace:50 #-}

data D : Set where
D : Set


text:
-- A Simple selection of modules with some renamings to
-- make my (your) life easier when starting a new agda module.
--
-- This includes standard functionality to work on:
--  1. Functions,
--  2. Naturals,
--  3. Products and Coproducts (projections and injections are p1, p2, i1, i2).
--  4. Finite Types (zero and suc are fz and fs)
--  5. Lists
--  6. Booleans and PropositionalEquality
--  7. Decidable Predicates
--
module Prelude where

  open import Data.Unit.NonEta
    using (Unit; unit)
    public

  open import Data.Empty
    using (⊥; ⊥-elim)
    public

  open import Function
    using (_∘_; _$_; flip; id; const; _on_)
    public

  open import Data.Nat
    using (ℕ; suc; zero; _+_; _*_; _∸_)
    renaming (_≟_ to _≟-ℕ_; _≤?_ to _≤?-ℕ_)
    public

  open import Data.Fin
    using (Fin; fromℕ; fromℕ≤; toℕ)
    renaming (zero to fz; suc to fs)
    public

  open import Data.Fin.Properties
    using ()
    renaming (_≟_ to _≟-Fin_)
    public

  open import Data.List
    using (List; _∷_; []; map; _++_; zip; filter;
           all; any; concat; foldr; reverse; length)
    public

  open import Data.Product
    using (∃; Σ; _×_; _,_; uncurry; curry)
    renaming (proj₁ to p1; proj₂ to p2
           ; <_,_> to split)
    public

  open import Data.Sum
    using (_⊎_; [_,_]′)
    renaming (inj₁ to i1; inj₂ to i2
           ; [_,_] to either)
    public

  open import Data.Bool
    using (Bool; true; false; if_then_else_; not)
    renaming (_∧_ to _and_; _∨_ to _or_)
    public

  open import Relation.Nullary
    using (Dec; yes; no; ¬_)
    public

  open import Relation.Binary.PropositionalEquality
    using (_≡_; refl; sym; trans; cong; cong₂; subst)
    public

  open import Data.Maybe
    using (Maybe; just; nothing)
    renaming (maybe′ to maybe)
    public

  dec-elim : ∀{a b}{A : Set a}{B : Set b}
           → (A → B) → (¬ A → B) → Dec A → B
  dec-elim f g (yes p) = f p
  dec-elim f g (no  p) = g p

  dec2set : ∀{a}{A : Set a} → Dec A → Set
  dec2set (yes _) = Unit
  dec2set (no  _) = ⊥

  isTrue : ∀{a}{A : Set a} → Dec A → Bool
  isTrue (yes _) = true
  isTrue _       = false

  takeWhile : ∀{a}{A : Set a} → (A → Bool) → List A → List A
  takeWhile _ [] = []
  takeWhile f (x ∷ xs) with f x
  ...| true = x ∷ takeWhile f xs
  ...| _    = takeWhile f xs

  -- Some minor boilerplate to solve equality problem...
  record Eq (A : Set) : Set where
    constructor eq
    field cmp : (x y : A) → Dec (x ≡ y)

  open Eq {{...}}

  record Enum (A : Set) : Set where
    constructor enum
    field
      toEnum   : A → Maybe ℕ
      fromEnum : ℕ → Maybe A

  open Enum {{...}}

  instance
    eq-ℕ : Eq ℕ
    eq-ℕ = eq _≟-ℕ_

    enum-ℕ : Enum ℕ
    enum-ℕ = enum just just

    eq-Fin : ∀{n} → Eq (Fin n)
    eq-Fin = eq _≟-Fin_

    enum-Fin : ∀{n} → Enum (Fin n)
    enum-Fin {n} = enum (λ x → just (toℕ x)) fromℕ-partial
      where
        fromℕ-partial : ℕ → Maybe (Fin n)
        fromℕ-partial m with suc m ≤?-ℕ n
        ...| yes prf = just (fromℕ≤ {m} {n} prf)
        ...| no  _   = nothing

    eq-⊥ : Eq ⊥
    eq-⊥ = eq (λ x → ⊥-elim x)

    enum-⊥ : Enum ⊥
    enum-⊥ = enum ⊥-elim (const nothing)

    eq-Maybe : ∀{A} ⦃ eqA : Eq A ⦄ → Eq (Maybe A)
    eq-Maybe = eq decide
      where
        just-inj : ∀{a}{A : Set a}{x y : A}
                 → _≡_ {a} {Maybe A} (just x) (just y) → x ≡ y
        just-inj refl = refl

        decide : {A : Set} ⦃ eqA : Eq A ⦄
               → (x y : Maybe A) → Dec (x ≡ y)
        decide nothing nothing   = yes refl
        decide nothing (just _)  = no (λ ())
        decide (just _) nothing  = no (λ ())
        decide ⦃ eq f ⦄ (just x) (just y) with f x y
        ...| yes x≡y = yes (cong just x≡y)
        ...| no  x≢y = no (x≢y ∘ just-inj)

    enum-Maybe : ∀{A} ⦃ enA : Enum A ⦄ → Enum (Maybe A)
    enum-Maybe ⦃ enum aℕ ℕa ⦄ = enum (maybe aℕ nothing) (just ∘ ℕa)

    eq-List : {A : Set}{{eq : Eq A}} → Eq (List A)
    eq-List {A} {{eq _≟_}} = eq decide
      where
        open import Data.List.Properties
          renaming (∷-injective to ∷-inj)

        decide : (a b : List A) → Dec (a ≡ b)
        decide [] (_ ∷ _) = no (λ ())
        decide (_ ∷ _) [] = no (λ ())
        decide []   []    = yes refl
        decide (a ∷ as) (b ∷ bs)
          with a ≟ b | decide as bs
        ...| yes a≡b | yes as≡bs
          rewrite a≡b = yes (cong (_∷_ b) as≡bs)
        ...| no  a≢b | yes as≡bs = no (a≢b ∘ p1 ∘ ∷-inj)
        ...| yes a≡b | no  as≢bs = no (as≢bs ∘ p2 ∘ ∷-inj)
        ...| no  a≢b | no  as≢bs = no (a≢b ∘ p1 ∘ ∷-inj)

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw