text:
-- 2010-09-29 Andreas, mail to Ulf

module ExistentialsProjections where

postulate
 .irrelevant : {A : Set} -> .A -> A

record Exists (A : Set) (P : A -> Set) : Set where
  constructor exists
  field
    .fwitness : A
    fcontent : P fwitness

.witness : forall {A P} -> (x : Exists A P) -> A
witness (exists a p) = irrelevant a

-- second projection out of existential is breaking abstraction, so should be forbidden

content : forall {A P} -> (x : Exists A P) -> P (witness x)
content (exists a p) = p  -- should not typecheck!!

{- We have p : P a != P (witness (exists a p)) = P (irrelevant a)
because a != irrelevant a.
-}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Some definitions related to and properties of finite sets
------------------------------------------------------------------------

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

open import Equality

module Fin
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence using (_⇔_)
open import Prelude hiding (id)

open import Bijection eq as Bijection using (_↔_; module _↔_)
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq as F hiding (_∘_; Distinct↔≢)
open import H-level eq hiding (⌞_⌟)
open import H-level.Closure eq
open import List eq
open import Nat eq as Nat using (_≤_; ≤-refl; ≤-step; _<_; pred)
open import Univalence-axiom eq

------------------------------------------------------------------------
-- Some bijections relating Fin and ∃

∃-Fin-zero : ∀ {p ℓ} (P : Fin zero → Type p) → ∃ P ↔ ⊥ {ℓ = ℓ}
∃-Fin-zero P = Σ-left-zero

∃-Fin-suc : ∀ {p n} (P : Fin (suc n) → Type p) →
            ∃ P ↔ P fzero ⊎ ∃ (P ∘ fsuc)
∃-Fin-suc P =
  ∃ P                          ↔⟨ ∃-⊎-distrib-right ⟩
  ∃ (P ∘ inj₁) ⊎ ∃ (P ∘ inj₂)  ↔⟨ Σ-left-identity ⊎-cong id ⟩□
  P (inj₁ tt) ⊎ ∃ (P ∘ inj₂)   □

------------------------------------------------------------------------
-- Fin n is a set

abstract

  Fin-set : ∀ n → Is-set (Fin n)
  Fin-set zero    = mono₁ 1 ⊥-propositional
  Fin-set (suc n) = ⊎-closure 0 (mono 0≤2 ⊤-contractible) (Fin-set n)
    where
    0≤2 : 0 ≤ 2
    0≤2 = ≤-step (≤-step ≤-refl)

------------------------------------------------------------------------
-- If two nonempty finite sets are isomorphic, then we can remove one
-- element from each and get new isomorphic finite sets

private

  well-behaved : ∀ {m n} (f : Fin (1 + m) ↔ Fin (1 + n)) →
                 Well-behaved (_↔_.to f)
  well-behaved f {b = i} eq₁ eq₂ = ⊎.inj₁≢inj₂ (
    fzero         ≡⟨ sym $ to-from f eq₂ ⟩
    from f fzero  ≡⟨ to-from f eq₁ ⟩∎
    fsuc i        ∎)
    where open _↔_

cancel-suc : ∀ {m n} → Fin (1 + m) ↔ Fin (1 + n) → Fin m ↔ Fin n
cancel-suc f =
  ⊎-left-cancellative f (well-behaved f) (well-behaved $ inverse f)

-- In fact, we can do it in such a way that, if the input bijection
-- relates elements of two lists with equal heads, then the output
-- bijection relates elements of the tails of the lists.
--
-- xs And ys Are-related-by f is inhabited if the indices of xs and ys
-- which are related by f point to equal elements.

infix 4 _And_Are-related-by_

_And_Are-related-by_ :
  ∀ {a} {A : Type a}
  (xs ys : List A) → Fin (length xs) ↔ Fin (length ys) → Type a
xs And ys Are-related-by f =
  ∀ i → index xs i ≡ index ys (_↔_.to f i)

abstract

  -- The tails are related.

  cancel-suc-preserves-relatedness :
    ∀ {a} {A : Type a} (x : A) xs ys
    (f : Fin (length (x ∷ xs)) ↔ Fin (length (x ∷ ys))) →
    x ∷ xs And x ∷ ys Are-related-by f →
    xs And ys Are-related-by cancel-suc f
  cancel-suc-preserves-relatedness x xs ys f related = helper
    where
    open _↔_ f

    helper : xs And ys Are-related-by cancel-suc f
    helper i with inspect (to (fsuc i)) | related (fsuc i)
    helper i | fsuc k , eq₁ | hyp₁ =
      index xs i                    ≡⟨ hyp₁ ⟩
      index (x ∷ ys) (to (fsuc i))  ≡⟨ cong (index (x ∷ ys)) eq₁ ⟩
      index (x ∷ ys) (fsuc k)       ≡⟨ refl _ ⟩∎
      index ys k                    ∎
    helper i | fzero , eq₁ | hyp₁
      with inspect (to (fzero)) | related (fzero)
    helper i | fzero , eq₁ | hyp₁ | fsuc j , eq₂ | hyp₂ =
      index xs i                    ≡⟨ hyp₁ ⟩
      index (x ∷ ys) (to (fsuc i))  ≡⟨ cong (index (x ∷ ys)) eq₁ ⟩
      index (x ∷ ys) (fzero)        ≡⟨ refl _ ⟩
      x                             ≡⟨ hyp₂ ⟩
      index (x ∷ ys) (to (fzero))   ≡⟨ cong (index (x ∷ ys)) eq₂ ⟩
      index (x ∷ ys) (fsuc j)       ≡⟨ refl _ ⟩∎
      index ys j                    ∎
    helper i | fzero , eq₁ | hyp₁ | fzero , eq₂ | hyp₂ =
      ⊥-elim $ well-behaved f eq₁ eq₂

-- By using cancel-suc we can show that finite sets are isomorphic iff
-- they have equal size.

isomorphic-same-size : ∀ {m n} → (Fin m ↔ Fin n) ⇔ m ≡ n
isomorphic-same-size {m} {n} = record
  { to   = to m n
  ; from = λ m≡n → subst (λ n → Fin m ↔ Fin n) m≡n id
  }
  where
  abstract
    to : ∀ m n → (Fin m ↔ Fin n) → m ≡ n
    to zero    zero    _       = refl _
    to (suc m) (suc n) 1+m↔1+n = cong suc $ to m n $ cancel-suc 1+m↔1+n
    to zero    (suc n)   0↔1+n = ⊥-elim $ _↔_.from 0↔1+n fzero
    to (suc m) zero    1+m↔0   = ⊥-elim $ _↔_.to 1+m↔0 fzero

------------------------------------------------------------------------
-- The natural number corresponding to a value in Fin n

-- The underlying natural number.

⌞_⌟ : ∀ {n} → Fin n → ℕ
⌞_⌟ {n = zero}  ()
⌞_⌟ {n = suc _} fzero    = zero
⌞_⌟ {n = suc _} (fsuc i) = suc ⌞ i ⌟

-- Use of subst Fin does not change the underlying natural number.

⌞subst⌟ : ∀ {m n} (p : m ≡ n) (i : Fin m) → ⌞ subst Fin p i ⌟ ≡ ⌞ i ⌟
⌞subst⌟ {m} p i =
  ⌞ subst Fin p i ⌟         ≡⟨ cong (uncurry λ n p → ⌞ subst Fin p i ⌟) (Σ-≡,≡→≡ (sym p) (

      subst (m ≡_) (sym p) p     ≡⟨ sym trans-subst ⟩
      trans p (sym p)            ≡⟨ trans-symʳ p ⟩∎
      refl m                     ∎)) ⟩

  ⌞ subst Fin (refl m) i ⌟  ≡⟨ cong ⌞_⌟ (subst-refl _ _) ⟩∎
  ⌞ i ⌟                     ∎

-- If the underlying natural numbers are equal, then the values in
-- Fin n are equal.

cancel-⌞⌟ : ∀ {n} {i j : Fin n} → ⌞ i ⌟ ≡ ⌞ j ⌟ → i ≡ j
cancel-⌞⌟ {zero}  {}
cancel-⌞⌟ {suc _} {fzero}  {fzero}  _   = refl _
cancel-⌞⌟ {suc _} {fzero}  {fsuc _} 0≡+ = ⊥-elim (Nat.0≢+ 0≡+)
cancel-⌞⌟ {suc _} {fsuc _} {fzero}  +≡0 = ⊥-elim (Nat.0≢+ (sym +≡0))
cancel-⌞⌟ {suc _} {fsuc _} {fsuc _} +≡+ =
  cong fsuc (cancel-⌞⌟ (Nat.cancel-suc +≡+))

-- Tries to convert from natural numbers.

from-ℕ′ : ∀ {m} (n : ℕ) → m ≤ n ⊎ ∃ λ (i : Fin m) → ⌞ i ⌟ ≡ n
from-ℕ′ {zero}  _       = inj₁ (Nat.zero≤ _)
from-ℕ′ {suc m} zero    = inj₂ (fzero , refl _)
from-ℕ′ {suc m} (suc n) =
  ⊎-map Nat.suc≤suc (Σ-map fsuc (cong suc)) (from-ℕ′ {m} n)

from-ℕ : ∀ {m} (n : ℕ) → m ≤ n ⊎ Fin m
from-ℕ = ⊎-map id proj₁ ∘ from-ℕ′

-- Values of type Fin n can be seen as natural numbers smaller than n.

Fin↔< : ∀ n → Fin n ↔ ∃ λ m → m < n
Fin↔< zero =
  ⊥                   ↝⟨ inverse ×-right-zero ⟩
  ℕ × ⊥               ↔⟨ ∃-cong (λ _ → inverse <zero↔) ⟩□
  (∃ λ m → m < zero)  □
Fin↔< (suc n) =
  ⊤ ⊎ Fin n                                  ↝⟨ inverse (_⇔_.to contractible⇔↔⊤ (singleton-contractible 0)) ⊎-cong Fin↔< n ⟩
  (∃ λ m → m ≡ 0) ⊎ (∃ λ m → m < n)          ↝⟨ id ⊎-cong ∃<↔∃0<×≤ ⟩
  (∃ λ m → m ≡ 0) ⊎ (∃ λ m → 0 < m × m ≤ n)  ↝⟨ inverse ∃-⊎-distrib-left ⟩
  (∃ λ m → m ≡ 0 ⊎ 0 < m × m ≤ n)            ↝⟨ ∃-cong (λ _ → inverse ≤↔≡0⊎0<×≤) ⟩
  (∃ λ m → m ≤ n)                            ↝⟨ ∃-cong (λ _ → inverse suc≤suc↔) ⟩
  (∃ λ m → suc m ≤ suc n)                    ↔⟨⟩
  (∃ λ m → m < suc n)                        □

-- The forward direction of Fin↔< gives the underlying natural number.

Fin↔<≡⌞⌟ :
  ∀ {n} (i : Fin n) → proj₁ (_↔_.to (Fin↔< n) i) ≡ ⌞ i ⌟
Fin↔<≡⌞⌟ {n = zero}  ()
Fin↔<≡⌞⌟ {n = suc _} fzero    = refl _
Fin↔<≡⌞⌟ {n = suc _} (fsuc i) = cong suc (Fin↔<≡⌞⌟ i)

-- The largest possible number.

largest : ∀ n → Fin (suc n)
largest zero    = fzero
largest (suc n) = fsuc (largest n)

largest-correct : ∀ n → ⌞ largest n ⌟ ≡ n
largest-correct zero    = refl _
largest-correct (suc n) = cong suc (largest-correct n)

-- The largest possible number can be expressed using Fin↔<.

largest≡Fin↔< :
  ∀ {n} → largest n ≡ _↔_.from (Fin↔< (suc n)) (n , ≤-refl)
largest≡Fin↔< {n} =
  largest n                                                      ≡⟨ sym (_↔_.left-inverse-of (Fin↔< (suc n)) _) ⟩
  _↔_.from (Fin↔< (suc n)) (_↔_.to (Fin↔< (suc n)) (largest n))  ≡⟨ cong (_↔_.from (Fin↔< (suc n))) (Σ-≡,≡→≡ (Fin↔<≡⌞⌟ (largest n)) (refl _)) ⟩
  _↔_.from (Fin↔< (suc n)) (⌞ largest n ⌟ , p₁)                  ≡⟨ cong (_↔_.from (Fin↔< (suc n)))
                                                                      (Σ-≡,≡→≡ (largest-correct n) (≤-propositional p₂ ≤-refl)) ⟩∎
  _↔_.from (Fin↔< (suc n)) (n , ≤-refl)                          ∎
  where
  p₁ = subst (_< suc n) (Fin↔<≡⌞⌟ (largest n))
             (proj₂ (_↔_.to (Fin↔< (suc n)) (largest n)))
  p₂ = subst (_< suc n) (largest-correct n) p₁

------------------------------------------------------------------------
-- Weakening

-- Single-step weakening.

weaken₁ : ∀ {n} → Fin n → Fin (suc n)
weaken₁ {zero}  ()
weaken₁ {suc _} fzero    = fzero
weaken₁ {suc _} (fsuc i) = fsuc (weaken₁ i)

weaken₁-correct : ∀ {n} (i : Fin n) → ⌞ weaken₁ i ⌟ ≡ ⌞ i ⌟
weaken₁-correct {zero}  ()
weaken₁-correct {suc _} fzero    = refl _
weaken₁-correct {suc _} (fsuc i) = cong suc (weaken₁-correct i)

-- Multiple-step weakening.

weaken : ∀ {m n} → m ≤ n → Fin m → Fin n
weaken (Nat.≤-refl′ m≡n)       = subst Fin m≡n
weaken (Nat.≤-step′ m≤k 1+k≡n) = subst Fin 1+k≡n ∘ weaken₁ ∘ weaken m≤k

weaken-correct : ∀ {m n} (m≤n : m ≤ n) (i : Fin m) →
                 ⌞ weaken m≤n i ⌟ ≡ ⌞ i ⌟
weaken-correct (Nat.≤-refl′ m≡n) i =
  ⌞ subst Fin m≡n i ⌟  ≡⟨ ⌞subst⌟ _ _ ⟩∎
  ⌞ i ⌟                ∎
weaken-correct (Nat.≤-step′ m≤k 1+k≡n) i =
  ⌞ subst Fin 1+k≡n (weaken₁ (weaken m≤k i)) ⌟  ≡⟨ ⌞subst⌟ _ _ ⟩
  ⌞ weaken₁ (weaken m≤k i) ⌟                    ≡⟨ weaken₁-correct _ ⟩
  ⌞ weaken m≤k i ⌟                              ≡⟨ weaken-correct m≤k _ ⟩∎
  ⌞ i ⌟                                         ∎

------------------------------------------------------------------------
-- Predecessor and successor

-- Predecessor.

predᶠ : ∀ {n} → Fin n → Fin n
predᶠ {n = zero}  ()
predᶠ {n = suc _} fzero    = fzero
predᶠ {n = suc _} (fsuc i) = weaken₁ i

predᶠ-correct : ∀ {n} (i : Fin n) → ⌞ predᶠ i ⌟ ≡ Nat.pred ⌞ i ⌟
predᶠ-correct {n = zero}  ()
predᶠ-correct {n = suc _} fzero    = refl _
predᶠ-correct {n = suc _} (fsuc i) = weaken₁-correct i

-- Successor.

sucᶠ : ∀ {n} (i : Fin (suc n)) →
       i ≡ largest n ⊎
       i ≢ largest n × ∃ λ (j : Fin (suc n)) → ⌞ j ⌟ ≡ suc ⌞ i ⌟
sucᶠ {zero}  fzero     = inj₁ (refl _)
sucᶠ {zero}  (fsuc ())
sucᶠ {suc _} fzero     = inj₂ (⊎.inj₁≢inj₂ , fsuc fzero , refl _)
sucᶠ {suc _} (fsuc i)  =
  ⊎-map (cong fsuc)
        (Σ-map (_∘ ⊎.cancel-inj₂) (Σ-map fsuc (cong suc)))
        (sucᶠ i)

------------------------------------------------------------------------
-- Arithmetic

-- Addition.

_+ᶠ_ : ∀ {m n} → Fin m → Fin n → Fin (m + n)
_+ᶠ_ {m = zero}  ()
_+ᶠ_ {m = suc m} fzero    j = weaken (Nat.m≤n+m _ (suc m)) j
_+ᶠ_ {m = suc _} (fsuc i) j = fsuc (i +ᶠ j)

+ᶠ-correct :
  ∀ {m n} (i : Fin m) (j : Fin n) → ⌞ i +ᶠ j ⌟ ≡ ⌞ i ⌟ + ⌞ j ⌟
+ᶠ-correct {m = zero}  ()
+ᶠ-correct {m = suc m} fzero    j = weaken-correct
                                      (Nat.m≤n+m _ (suc m)) _
+ᶠ-correct {m = suc _} (fsuc i) j = cong suc (+ᶠ-correct i j)

------------------------------------------------------------------------
-- "Type arithmetic" using Fin

-- Taking the disjoint union of two finite sets amounts to the same
-- thing as adding the sizes.

Fin⊎Fin↔Fin+ : ∀ m n → Fin m ⊎ Fin n ↔ Fin (m + n)
Fin⊎Fin↔Fin+ zero n =
  Fin 0 ⊎ Fin n  ↝⟨ id ⟩
  ⊥ ⊎ Fin n      ↝⟨ ⊎-left-identity ⟩
  Fin n          ↝⟨ id ⟩□
  Fin (0 + n)    □
Fin⊎Fin↔Fin+ (suc m) n =
  Fin (suc m) ⊎ Fin n  ↝⟨ id ⟩
  (⊤ ⊎ Fin m) ⊎ Fin n  ↝⟨ inverse ⊎-assoc ⟩
  ⊤ ⊎ (Fin m ⊎ Fin n)  ↝⟨ id ⊎-cong Fin⊎Fin↔Fin+ m n ⟩
  ⊤ ⊎ Fin (m + n)      ↝⟨ id ⟩
  Fin (suc (m + n))    ↝⟨ id ⟩□
  Fin (suc m + n)      □

-- Taking the product of two finite sets amounts to the same thing as
-- multiplying the sizes.

Fin×Fin↔Fin* : ∀ m n → Fin m × Fin n ↔ Fin (m * n)
Fin×Fin↔Fin* zero n =
  Fin 0 × Fin n  ↝⟨ id ⟩
  ⊥ × Fin n      ↝⟨ ×-left-zero ⟩
  ⊥              ↝⟨ id ⟩□
  Fin 0          □
Fin×Fin↔Fin* (suc m) n =
  Fin (suc m) × Fin n        ↝⟨ id ⟩
  (⊤ ⊎ Fin m) × Fin n        ↝⟨ ∃-⊎-distrib-right ⟩
  ⊤ × Fin n ⊎ Fin m × Fin n  ↝⟨ ×-left-identity ⊎-cong Fin×Fin↔Fin* m n ⟩
  Fin n ⊎ Fin (m * n)        ↝⟨ Fin⊎Fin↔Fin+ _ _ ⟩
  Fin (n + m * n)            ↝⟨ id ⟩□
  Fin (suc m * n)            □

-- Forming the function space between two finite sets amounts to the
-- same thing as raising one size to the power of the other (assuming
-- extensionality).

[Fin→Fin]↔Fin^ :
  Extensionality (# 0) (# 0) →
  ∀ m n → (Fin m → Fin n) ↔ Fin (n ^ m)
[Fin→Fin]↔Fin^ ext zero n =
  (Fin 0 → Fin n)  ↝⟨ id ⟩
  (⊥ → Fin n)      ↝⟨ Π⊥↔⊤ ext ⟩
  ⊤                ↝⟨ inverse ⊎-right-identity ⟩□
  Fin 1            □
[Fin→Fin]↔Fin^ ext (suc m) n =
  (Fin (suc m) → Fin n)          ↝⟨ id ⟩
  (⊤ ⊎ Fin m → Fin n)            ↝⟨ Π⊎↔Π×Π ext ⟩
  (⊤ → Fin n) × (Fin m → Fin n)  ↝⟨ Π-left-identity ×-cong [Fin→Fin]↔Fin^ ext m n ⟩
  Fin n × Fin (n ^ m)            ↝⟨ Fin×Fin↔Fin* _ _ ⟩
  Fin (n * n ^ m)                ↝⟨ id ⟩□
  Fin (n ^ suc m)                □

-- Automorphisms on Fin n are isomorphic to Fin (n !) (assuming
-- extensionality).

[Fin↔Fin]↔Fin! :
  Extensionality (# 0) (# 0) →
  ∀ n → (Fin n ↔ Fin n) ↔ Fin (n !)
[Fin↔Fin]↔Fin! ext zero =
  Fin 0 ↔ Fin 0  ↝⟨ Eq.↔↔≃ ext (Fin-set 0) ⟩
  Fin 0 ≃ Fin 0  ↝⟨ id ⟩
  ⊥ ≃ ⊥          ↔⟨ ≃⊥≃¬ ext ⟩
  ¬ ⊥            ↝⟨ ¬⊥↔⊤ ext ⟩
  ⊤              ↝⟨ inverse ⊎-right-identity ⟩
  ⊤ ⊎ ⊥          ↝⟨ id ⟩□
  Fin 1          □
[Fin↔Fin]↔Fin! ext (suc n) =
  Fin (suc n) ↔ Fin (suc n)      ↝⟨ [⊤⊎↔⊤⊎]↔[⊤⊎×↔] Fin._≟_ ext ⟩
  Fin (suc n) × (Fin n ↔ Fin n)  ↝⟨ id ×-cong [Fin↔Fin]↔Fin! ext n ⟩
  Fin (suc n) × Fin (n !)        ↝⟨ Fin×Fin↔Fin* _ _ ⟩□
  Fin (suc n !)                  □

-- A variant of the previous property.

[Fin≡Fin]↔Fin! :
  Extensionality (# 0) (# 0) →
  Univalence (# 0) →
  ∀ n → (Fin n ≡ Fin n) ↔ Fin (n !)
[Fin≡Fin]↔Fin! ext univ n =
  Fin n ≡ Fin n  ↔⟨ ≡≃≃ univ ⟩
  Fin n ≃ Fin n  ↝⟨ inverse $ Eq.↔↔≃ ext (Fin-set n) ⟩
  Fin n ↔ Fin n  ↝⟨ [Fin↔Fin]↔Fin! ext n ⟩□
  Fin (n !)      □

------------------------------------------------------------------------
-- Inequality and a related isomorphism

-- Inequality.

Distinct : ∀ {n} → Fin n → Fin n → Type
Distinct i j = Nat.Distinct ⌞ i ⌟ ⌞ j ⌟

-- This definition of inequality is pointwise logically equivalent to
-- _≢_, and in the presence of extensionality the two definitions are
-- pointwise isomorphic.

Distinct↔≢ :
  ∀ {k n} {i j : Fin n} →
  Extensionality? ⌊ k ⌋-sym lzero lzero →
  Distinct i j ↝[ ⌊ k ⌋-sym ] i ≢ j
Distinct↔≢ {i = i} {j} ext =
  Distinct i j              ↔⟨⟩
  Nat.Distinct ⌞ i ⌟ ⌞ j ⌟  ↝⟨ F.Distinct↔≢ ext ⟩
  ⌞ i ⌟ ≢ ⌞ j ⌟             ↝⟨ generalise-ext?-prop ≢⇔≢ ¬-propositional ¬-propositional ext ⟩□
  i ≢ j                     □
  where
  ≢⇔≢ : ⌞ i ⌟ ≢ ⌞ j ⌟ ⇔ i ≢ j
  ≢⇔≢ = record { to = _∘ cong ⌞_⌟; from = _∘ cancel-⌞⌟ }

-- For every i : Fin n there is a bijection between Fin (pred n) and
-- numbers in Fin n distinct from i.
--
-- When n is positive the forward direction of this bijection
-- corresponds to the function "thin" from McBride's "First-order
-- unification by structural recursion", with an added inequality
-- proof, and the other direction is a total variant of "thick".

Fin↔Fin+≢ :
  ∀ {n} (i : Fin n) →
  Fin (pred n) ↔ ∃ λ (j : Fin n) → Distinct j i
Fin↔Fin+≢ {suc n} fzero =
  Fin n                                       ↝⟨ inverse ⊎-left-identity ⟩
  ⊥ ⊎ Fin n                                   ↝⟨ inverse $ id ⊎-cong ×-right-identity ⟩
  ⊥ ⊎ Fin n × ⊤                               ↝⟨ inverse $ ∃-Fin-suc _ ⟩□
  (∃ λ (j : Fin (suc n)) → Distinct j fzero)  □

Fin↔Fin+≢ {suc (suc n)} (fsuc i) =
  Fin (1 + n)                                    ↔⟨⟩
  ⊤ ⊎ Fin n                                      ↝⟨ id ⊎-cong Fin↔Fin+≢ i ⟩
  ⊤ ⊎ (∃ λ (j : Fin (1 + n)) → Distinct j i)     ↔⟨ inverse $ ∃-Fin-suc _ ⟩□
  (∃ λ (j : Fin (2 + n)) → Distinct j (fsuc i))  □

Fin↔Fin+≢ {zero}     ()
Fin↔Fin+≢ {suc zero} (fsuc ())

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by total orders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.TotalOrder
         {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where

open Relation.Binary.TotalOrder T
open import Relation.Binary.Consequences

decTotalOrder : Decidable _≈_ → DecTotalOrder _ _ _
decTotalOrder ≟ = record
  { isDecTotalOrder = record
      { isTotalOrder = isTotalOrder
      ; _≟_          = ≟
      ; _≤?_         = total+dec⟶dec reflexive antisym total ≟
      }
  }


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.HLevel
open import HoTT.HLevel.Truncate
open import HoTT.Logic
open import HoTT.Identity
open import HoTT.Identity.Identity
open import HoTT.Identity.Coproduct
open import HoTT.Identity.Sigma
open import HoTT.Identity.Pi
open import HoTT.Identity.Universe
open import HoTT.Equivalence
open import HoTT.Equivalence.Lift
open import HoTT.Sigma.Transport

module HoTT.Exercises.Chapter3 where

module Exercise1 {i} {A B : 𝒰 i} (e : A ≃ B) (A-set : isSet A)
  where
  □ : isSet B
  □ {x} {y} p q = ap⁻¹ (ap≃ (e ⁻¹ₑ) x y) (A-set (ap g p) (ap g q))
    where open Iso (eqv→iso e)

module Exercise2 {i} {A B : 𝒰 i} (A-set : isSet A) (B-set : isSet B)
  where
  □ : isSet (A + B)
  □ {inl x} {inl y} p q = ap⁻¹ =+-equiv
    (ap lift (A-set (lower (=+-elim p)) (lower (=+-elim q))))
  □ {inl x} {inr y} p q = 𝟎-rec (=+-elim p)
  □ {inr x} {inl y} p q = 𝟎-rec (=+-elim p)
  □ {inr x} {inr y} p q = ap⁻¹ =+-equiv
    (ap lift (B-set (lower (=+-elim p)) (lower (=+-elim q))))

module Exercise3
  {i} {A : 𝒰 i} (A-set : isSet A)
  {j} {B : A → 𝒰 j} (B-set : {x : A} → isSet (B x))
  where
  □ : isSet (Σ A B)
  □ {x = x@(x₁ , x₂)} {y = y@(y₁ , y₂)} p q =
    ap⁻¹ =Σ-equiv (lemma (pr₁ =Σ-equiv p) (pr₁ =Σ-equiv q))
    where
    lemma : (p q : Σ (x₁ == y₁) λ p₁ → (transport B p₁ x₂ == y₂)) → p == q
    lemma (p₁ , p₂) (q₁ , q₂) = pair⁼ (r₁ , r₂)
      where
      r₁ = A-set p₁ q₁
      r₂ = B-set (transport _ r₁ p₂) q₂

module Exercise4 {i} {A : 𝒰 i} where
  _ : isProp A → isContr (A → A)
  _ = λ A-prop → id , λ f → funext λ x → A-prop x (f x)

  _ : isContr (A → A) → isProp A
  _ = λ where
      (f , contr) x y → happly (contr (const x) ⁻¹ ∙ contr (const y)) x

module Exercise5 {i} {A : 𝒰 i} where
  open import HoTT.Pi.Transport
  open import HoTT.Sigma.Transport

  _ : isProp A ≃ (A → isContr A)
  _ = f , qinv→isequiv (g , η , ε)
    where
    f : isProp A → (A → isContr A)
    f A-prop x = x , A-prop x
    g : (A → isContr A) → isProp A
    g h x y = let contr = pr₂ (h x) in contr x ⁻¹ ∙ contr y
    η : g ∘ f ~ id
    η _ = isProp-prop _ _
    ε : f ∘ g ~ id
    ε h = funext λ _ → isContr-prop _ _

module Exercise6 {i} {A : 𝒰 i} where
  instance
    LEM-prop : ⦃ hlevel 1 A ⦄ → hlevel 1 (A + ¬ A)
    LEM-prop = isProp→hlevel1 λ where
      (inl a) (inl a') → ap inl center
      (inl a) (inr f) → 𝟎-rec (f a)
      (inr f) (inl b') → 𝟎-rec (f b')
      (inr f) (inr f') → ap inr center

module Exercise7
  {i} {A : 𝒰 i} {A-prop : isProp A}
  {j} {B : 𝒰 j} {B-prop : isProp B}
  where
  □ : ¬ (A × B) → isProp (A + B)
  □ f = λ where
      (inl x) (inl y) → ap inl (A-prop _ _)
      (inl x) (inr y) → 𝟎-rec (f (x , y))
      (inr x) (inl y) → 𝟎-rec (f (y , x))
      (inr x) (inr y) → ap inr (B-prop _ _)

module Exercise8 {i j} {A : 𝒰 i} {B : 𝒰 j} {f : A → B} where
  open import HoTT.Equivalence.Proposition
  prop₁ : qinv f → ∥ qinv f ∥
  prop₁ e = ∣ e ∣
  prop₂ : ∥ qinv f ∥ → qinv f
  prop₂ e = isequiv→qinv (∥-rec ⦃ isProp→hlevel1 isequiv-prop ⦄ qinv→isequiv e)
  prop₃ : isProp ∥ qinv f ∥
  prop₃ = hlevel1→isProp

module Exercise9 {i} (lem : LEM {i}) where
  open import HoTT.Logic
  open import HoTT.Equivalence.Lift

  _ : Prop𝒰 i ≃ 𝟐
  _ = f , qinv→isequiv (g , η , ε)
    where
    f : Prop𝒰 i → 𝟐
    f P with lem P
    ... | inl _ = 0₂
    ... | inr _ = 1₂
    g : 𝟐 → Prop𝒰 i
    g 0₂ = ⊤
    g 1₂ = ⊥
    η : g ∘ f ~ id
    η P with lem P
    ... | inl t = hlevel⁼ (ua (prop-equiv (const t) (const ★)))
    ... | inr f = hlevel⁼ (ua (prop-equiv 𝟎-rec (𝟎-rec ∘ f)))
    ε : f ∘ g ~ id
    ε 0₂ with lem (g 0₂)
    ... | inl _ = refl
    ... | inr f = 𝟎-rec (f ★)
    ε 1₂ with lem (g 1₂)
    ... | inl ()
    ... | inr _ = refl

import HoTT.Exercises.Chapter3.Exercise10

module Exercise11 where
  open variables
  open import HoTT.Pi.Transport
  open import HoTT.Identity.Boolean

  prop : ¬ ((A : 𝒰₀) → ∥ A ∥ → A)
  prop f = 𝟎-rec (g (f 𝟐 ∣ 0₂ ∣) p)
    where
    not = 𝟐-rec 1₂ 0₂
    e : 𝟐 ≃ 𝟐
    e = not , qinv→isequiv (not , 𝟐-ind _ refl refl , 𝟐-ind _ refl refl)
    g : (x : 𝟐) → ¬ (not x == x)
    g 0₂ = 𝟎-rec ∘ pr₁ =𝟐-equiv
    g 1₂ = 𝟎-rec ∘ pr₁ =𝟐-equiv
    p : not (f 𝟐 ∣ 0₂ ∣) == f 𝟐 ∣ 0₂ ∣
    p =
      not (f 𝟐 ∣ 0₂ ∣)
        =⟨ ap (λ e → pr₁ e (f 𝟐 ∣ 0₂ ∣)) (=𝒰-β e) ⁻¹ ⟩
      transport id (ua e) (f 𝟐 ∣ 0₂ ∣)
        =⟨ ap (λ x → transport id (ua e) (f 𝟐 x)) center ⟩
      transport id (ua e) (f 𝟐 (transport ∥_∥ (ua e ⁻¹) ∣ 0₂ ∣))
        =⟨ happly (transport-→ ∥_∥ id (ua e) (f 𝟐) ⁻¹) ∣ 0₂ ∣ ⟩
      transport (λ A → ∥ A ∥ → A) (ua e) (f 𝟐) ∣ 0₂ ∣
        =⟨ happly (apd f (ua e)) ∣ 0₂ ∣ ⟩
      f 𝟐 ∣ 0₂ ∣
        ∎
      where open =-Reasoning

module Exercise12 {i} {A : 𝒰 i} (lem : LEM {i}) where
  open variables using (B ; j)

  □ : ∥ (∥ A ∥ → A) ∥
  □ with lem (type ∥ A ∥)
  ... | inl x = swap ∥-rec x λ x → ∣ const x ∣
  ... | inr f = ∣ 𝟎-rec ∘ f ∣

module Exercise13 {i} (lem : LEM∞ {i}) where
  □ : AC {i} {i} {i}
  □ {X = X} {A = A} {P = P} f = ∣ pr₁ ∘ g , pr₂ ∘ g ∣
    where
    g : (x : X) → Σ (A x) (P x)
    g x with lem (Σ (A x) (P x))
    ... | inl t = t
    ... | inr b = ∥-rec ⦃ hlevel-in (λ {x} → 𝟎-rec (b x)) ⦄ id (f x)

module Exercise14 (lem : ∀ {i} → LEM {i}) where
  open import HoTT.Sigma.Universal

  open variables

  ∥_∥' : 𝒰 i → 𝒰 i
  ∥ A ∥' = ¬ ¬ A

  ∣_∣' : A → ∥ A ∥'
  ∣ a ∣' f = f a

  ∥'-hlevel : hlevel 1 ∥ A ∥'
  ∥'-hlevel = ⟨⟩

  ∥'-rec : ⦃ hlevel 1 B ⦄ → (f : A → B) →
           Σ[ g ∶ (∥ A ∥' → B) ] Π[ a ∶ A ] g ∣ a ∣' == f a
  ∥'-rec f = λ where
    .pr₁ a → +-rec id (λ b → 𝟎-rec (a (𝟎-rec ∘ b ∘ f))) (lem (type _))
    .pr₂ _ → center

  _ : ∥ A ∥' ≃ ∥ A ∥
  _ = let open Iso in iso→eqv λ where
    .f → pr₁ (∥'-rec ∣_∣)
    .g → ∥-rec ∣_∣'
    .η _ → center
    .ε _ → center

module Exercise15
  (LiftProp-isequiv : ∀ {i j} → isequiv (LiftProp {i} {j}))
  where
  open import HoTT.Equivalence.Transport
  open variables

  open module LiftProp-qinv {i} {j} = qinv (isequiv→qinv (LiftProp-isequiv {i} {j}))
    renaming (g to LowerProp ; η to LiftProp-η ; ε to LiftProp-ε)

  ∥_∥' : 𝒰 (lsuc i) → 𝒰 (lsuc i)
  ∥_∥' {i} A = (P : Prop𝒰 i) → (A → P ty) → P ty

  ∣_∣' : A → ∥ A ∥'
  ∣ a ∣' _ f = f a

  ∥'-hlevel : hlevel 1 ∥ A ∥'
  ∥'-hlevel = ⟨⟩

  ∥'-rec : {A : 𝒰 (lsuc i)} {(type B) : Prop𝒰 (lsuc i)} → (f : A → B) →
           Σ (∥ A ∥' → B) λ g → (a : A) → g ∣ a ∣' == f a
  ∥'-rec {_} {_} {B} f = let p = ap _ty (LiftProp-ε B) in λ where
    .pr₁ a → transport id p (lift (a (LowerProp B) (lower ∘ transport id (p ⁻¹) ∘ f)))
    -- We do not get a definitional equality since our propositional
    -- resizing equivalence does not give us definitionally equal
    -- types, i.e. LowerProp B ≢ B. If it did, then we could write
    --
    --   ∥'-rec f a :≡ a (LowerProp B) f
    --
    -- and then we'd have ∥'-rec f ∣a∣' ≡ f a.
    .pr₂ a → Eqv.ε (transport-equiv p) (f a)

module Exercise16
  {i} {(type X) : Set𝒰 i}
  {j} {Y : X → Prop𝒰 j}
  (lem : ∀ {i} → LEM {i})
  where
  _ : Π[ x ∶ X ] ¬ ¬ Y x ty ≃ ¬ ¬ (Π[ x ∶ X ] Y x ty)
  _ = let open Iso in iso→eqv λ where
    .f s t → t λ x → +-rec id (𝟎-rec ∘ s x) (lem (Y x))
    .g s x y → 𝟎-rec (s λ f → 𝟎-rec (y (f x)))
    .η _ → center
    .ε _ → center

module Exercise17
  {i} {A : 𝒰 i}
  {j} {B : ∥ A ∥ → Prop𝒰 j}
  where
  ∥-ind : ((a : A) → B ∣ a ∣ ty) → (x : ∥ A ∥) → B x ty
  ∥-ind f x = ∥-rec (transport (_ty ∘ B) center ∘ f) x
    where instance _ = λ {x} → hlevel𝒰.h (B x)

module Exercise18 {i} where
  open Exercise6

  _ : LEM {i} → LDN {i}
  _ = λ lem P f → +-rec id (𝟎-rec ∘ f) (lem P)

  _ : LDN {i} → LEM {i}
  _ = λ ldn P → ldn (type (P ty + ¬ P ty)) λ f → f (inr (f ∘ inl))

module Exercise19
  {i} {P : ℕ → 𝒰 i}
  (P-lem : (n : ℕ) → P n + ¬ P n)
  -- Do not assume that all P n are mere propositions so we can
  -- reuse this solution for exercise 23.
  where
  open import HoTT.NaturalNumber renaming (_+_ to _+ₙ_ ; +-comm to +ₙ-comm)
  open import HoTT.Identity.NaturalNumber
  open import HoTT.Transport.Identity
  open import HoTT.Base.Inspect
  open import HoTT.Identity.Product
  open import HoTT.Equivalence.Sigma
  open import HoTT.Equivalence.Coproduct
  open import HoTT.Equivalence.Empty

  -- P n does not hold for any m < n
  ℕ* : ℕ → 𝒰 i
  ℕ* zero = 𝟏
  ℕ* (succ n) = ¬ P n × ℕ* n

  P* : {n : ℕ} → P n → 𝒰 i
  P* {n} p = inl p == P-lem n

  -- ℕ* is the product of 𝟏 and some ¬ P n, all of which are
  -- propositions, so it is a proposition as well.
  instance ℕ*-hlevel : {n : ℕ} → hlevel 1 (ℕ* n)
  ℕ*-hlevel {zero} = 𝟏-hlevel
  ℕ*-hlevel {succ n} = ×-hlevel

  P*-hlevel : {n : ℕ} → hlevel 1 (Σ (P n) P*)
  hlevel-out (P*-hlevel {n}) {p , _} = ⟨⟩
    where
    e : P n ≃ P n + ¬ P n
    e = +-empty₂ ⁻¹ₑ ∙ₑ +-equiv reflₑ (𝟎-equiv (_$ p))
    instance
      _ = =-contrᵣ (P-lem n)
      _ = raise ⦃ equiv-hlevel (Σ-equiv₁ e ⁻¹ₑ) ⦄
  instance _ = P*-hlevel

  -- Extract evidence that ¬ P m for some m < n
  extract : {m n : ℕ} → m < n → ℕ* n → ¬ P m
  extract {m} (k , p) = pr₁ ∘ weaken ∘ transport ℕ* p'
    where
    p' = p ⁻¹ ∙ +ₙ-comm (succ m) k
    weaken : {k : ℕ} → ℕ* (k +ₙ succ m) → ℕ* (succ m)
    weaken {zero} = id
    weaken {succ k} = weaken ∘ pr₂

  -- The smallest n such that P n holds
  Pₒ = Σ (Σ ℕ λ n → Σ (P n) P*) (ℕ* ∘ pr₁)

  Pₒ-prop : isProp Pₒ
  Pₒ-prop ((n , p , _) , n*) ((m , q , _) , m*) =
    pair⁼ (pair⁼ (n=m , center) , center)
    where
    n=m : n == m
    n=m with n <=> m
    -- If n = m, then there is nothing to do.
    ... | inl n=m = n=m
    -- If n < m, we have P n and we know ℕ* m contains ¬ P n
    -- somewhere inside, so we can just extract it to find a
    -- contradiction.
    ... | inr (inl n<m) = 𝟎-rec (extract n<m m* p)
    -- The m < n case is symmetrical.
    ... | inr (inr m<n) = 𝟎-rec (extract m<n n* q)
  instance _ = isProp→hlevel1 Pₒ-prop

  -- Use the decidability of P to search for an instance of P in
  -- some finite range of natural numbers, keeping track of evidence
  -- that P does not hold for lower n.
  find-P : (n : ℕ) → Pₒ + ℕ* n
  find-P zero = inr ★
  find-P (succ n) with find-P n | P-lem n | inspect P-lem n
  ... | inl x  | _      | _      = inl x
  ... | inr n* | inl p  | [ p* ] = inl ((n , p , p*) , n*)
  ... | inr n* | inr ¬p | _      = inr (¬p , n*)

  -- If we know P holds for some n, then we have an upper bound for
  -- which to search for the smallest n. If we do not find any other
  -- n' ≤ n such that P n', then we have a contradiction.
  to-Pₒ : Σ ℕ P → Pₒ
  to-Pₒ (n , p) with find-P (succ n)
  ... | inl x = x
  ... | inr (¬p , _) = 𝟎-rec (¬p p)

  from-Pₒ : Pₒ → Σ ℕ P
  from-Pₒ ((n , p , p*) , n*) = n , p

  _ : ∥ Σ ℕ P ∥ → Σ ℕ P
  _ = from-Pₒ ∘ ∥-rec to-Pₒ

module Exercise20 where
  open variables

  -- See HoTT.HLevel
  _ : ⦃ _ : hlevel 0 A ⦄ → Σ A P ≃ P center
  _ = Σ-contr₁

module Exercise21 {i} {P : 𝒰 i} where
  open import HoTT.Equivalence.Proposition
  _ : isProp P ≃ (P ≃ ∥ P ∥)
  _ = prop-equiv ⦃ isProp-hlevel1 ⦄ f g
    where
    f : isProp P → P ≃ ∥ P ∥
    f p = prop-equiv ∣_∣ (∥-rec id)
      where instance _ = isProp→hlevel1 p
    g : P ≃ ∥ P ∥ → isProp P
    g e = hlevel1→isProp ⦃ equiv-hlevel (e ⁻¹ₑ) ⦄
    instance
      _ = Σ-hlevel ⦃ Π-hlevel ⦄ ⦃ isProp→hlevel1 isequiv-prop ⦄

module Exercise22 where
  Fin : ℕ → 𝒰₀
  Fin zero = 𝟎
  Fin (succ n) = Fin n + 𝟏

  □ : ∀ {i} (n : ℕ) {A : Fin n → 𝒰 i} {P : (x : Fin n) → A x → 𝒰 i} →
      ((x : Fin n) → ∥ Σ (A x) (P x) ∥) →
      ∥ Σ ((x : Fin n) → A x) (λ g → ((x : Fin n) → P x (g x))) ∥
  □ zero _ = ∣ 𝟎-ind , 𝟎-ind ∣
  □ (succ n) {A} {P} f =
    swap ∥-rec (f (inr ★))     λ zₛ →
    swap ∥-rec (□ n (f ∘ inl)) λ zₙ →
    let f = f' zₛ zₙ in ∣ pr₁ ∘ f , pr₂ ∘ f ∣
    where
    f' : _ → _ → (x : Fin (succ n)) → Σ (A x) (P x)
    f' (_ , _) (g , h) (inl m) = g m , h m
    f' (x , y) (_ , _) (inr ★) = x , y

module Exercise23 where
  -- The solution for Exercise19 covers the case where P is not
  -- necessarily a mere proposition.
  open Exercise19

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
{-# OPTIONS --without-K #-}
module sets.vec.core where

open import function.core
open import sets.nat.core using (ℕ; zero; suc)
open import sets.fin

data Vec {i}(A : Set i) : ℕ → Set i where
  [] : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
infixr 5 _∷_

head : ∀ {i}{A : Set i}{n : ℕ} → Vec A (suc n) → A
head (x ∷ _) = x

tail : ∀ {i}{A : Set i}{n : ℕ} → Vec A (suc n) → Vec A n
tail (_ ∷ xs) = xs

tabulate : ∀ {i}{A : Set i}{n : ℕ}
         → (Fin n → A) → Vec A n
tabulate {n = zero} _ = []
tabulate {n = suc m} f = f zero ∷ tabulate (f ∘ suc)

lookup : ∀ {i}{A : Set i}{n : ℕ}
       → Vec A n → Fin n → A
lookup [] ()
lookup (x ∷ xs) zero = x
lookup (x ∷ xs) (suc i) = lookup xs i

_!_ : ∀ {i}{A : Set i}{n : ℕ}
    → Vec A n → Fin n → A
_!_ = lookup

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
-- Andreas, 2020-05-08, issue #4637
-- Print record pattern (in with-function) in termination error.

-- {-# OPTIONS -v reify:60 #-}

record R : Set where
  pattern; inductive
  field foo : R

postulate
  bar : R → R

test : R → R
test r with bar r
test r | record { foo = x } with bar x
test r | record { foo = x } | _ = test x

-- WAS:
-- Termination checking failed for the following functions:
--   test
-- Problematic calls:
--   test r | bar r
--   Issue4637.with-14 r (recCon-NOT-PRINTED x)
--   | bar x
--   test x

-- EXPECTED:
-- Termination checking failed for the following functions:
--   test
-- Problematic calls:
--   test r | bar r
--   Issue4637.with-14 r (record { foo = x })
--   | bar x
--   test x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import LogicalFormulae
open import Lists.Definition
open import Lists.Fold.Fold
open import Lists.Concat
open import Lists.Length
open import Numbers.Naturals.Semiring

module Lists.Monad where

open import Lists.Map.Map public

flatten : {a : _} {A : Set a} → (l : List (List A)) → List A
flatten [] = []
flatten (l :: ls) = l ++ flatten ls

flatten' : {a : _} {A : Set a} → (l : List (List A)) → List A
flatten' = fold _++_ []

flatten=flatten' : {a : _} {A : Set a} (l : List (List A)) → flatten l ≡ flatten' l
flatten=flatten' [] = refl
flatten=flatten' (l :: ls) = applyEquality (l ++_) (flatten=flatten' ls)

lengthFlatten : {a : _} {A : Set a} (l : List (List A)) → length (flatten l) ≡ (fold _+N_ zero (map length l))
lengthFlatten [] = refl
lengthFlatten (l :: ls) rewrite lengthConcat l (flatten ls) | lengthFlatten ls = refl

flattenConcat : {a : _} {A : Set a} (l1 l2 : List (List A)) → flatten (l1 ++ l2) ≡ (flatten l1) ++ (flatten l2)
flattenConcat [] l2 = refl
flattenConcat (l1 :: ls) l2 rewrite flattenConcat ls l2 | concatAssoc l1 (flatten ls) (flatten l2) = refl

pure : {a : _} {A : Set a} → A → List A
pure a = [ a ]

bind : {a b : _} {A : Set a} {B : Set b} → (f : A → List B) → List A → List B
bind f l = flatten (map f l)

private
  leftIdentLemma : {a : _} {A : Set a} (xs : List A) → flatten (map pure xs) ≡ xs
  leftIdentLemma [] = refl
  leftIdentLemma (x :: xs) rewrite leftIdentLemma xs = refl

leftIdent : {a b : _} {A : Set a} {B : Set b} → (f : A → List B) → {x : A} → bind pure (f x) ≡ f x
leftIdent f {x} with f x
leftIdent f {x} | [] = refl
leftIdent f {x} | y :: ys rewrite leftIdentLemma ys = refl

rightIdent : {a b : _} {A : Set a} {B : Set b} → (f : A → List B) → {x : A} → bind f (pure x) ≡ f x
rightIdent f {x} with f x
rightIdent f {x} | [] = refl
rightIdent f {x} | y :: ys rewrite appendEmptyList ys = refl

associative : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : A → List B) (g : B → List C) → {x : List A} → bind g (bind f x) ≡ bind (λ a → bind g (f a)) x
associative f g {[]} = refl
associative f g {x :: xs} rewrite mapConcat (f x) (flatten (map f xs)) g | flattenConcat (map g (f x)) (map g (flatten (map f xs))) = applyEquality (flatten (map g (f x)) ++_) (associative f g {xs})


text:
-- Andreas, 2013-06-22, bug reported by evancavallo
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.conv:20 -v impossible:100 #-}
module Issue874 where

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

module _ {A : Set} where

  postulate
    P : A → Set

  foo : A → Set
  foo _ = Σ (A → A) (λ _ → (∀ _ → A))
    -- the unsolved meta here is essential to trigger the bug

  bar : (x : A) → foo x → Set
  bar x (g , _) = P (g x)

  postulate
    pos : {x : A} → Σ (foo x) (bar x)

  test : {x : A} → Σ (foo x) (bar x)
  test = pos

-- this raised an internal error in Conversion.compareElims
-- when projecting at unsolved record type


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

-- adding eta/epsilon to PiPointed
-- separate file for presentation in paper

module PiPointedFrac where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Singleton

infixr 90 _#_
infixr 70 _×ᵤ_
infixr 60 _+ᵤ_
infixr 50 _⊚_
infix 100 !_

infixr 70 _∙×ᵤ_
infixr 60 _∙+ᵤl_
infixr 60 _∙+ᵤr_
infixr 70 _∙⊗_
infixr 60 _∙⊕ₗ_
infixr 60 _∙⊕ᵣ_
infixr 50 _∙⊚_
infix 100 !∙_

------------------------------------------------------------------------------
-- Pi

data 𝕌 : Set
⟦_⟧ : (A : 𝕌) → Set
data _⟷_ : 𝕌 → 𝕌 → Set
eval : {A B : 𝕌} → (A ⟷ B) → ⟦ A ⟧ → ⟦ B ⟧

data 𝕌 where
  𝟘       : 𝕌
  𝟙       : 𝕌
  _+ᵤ_    : 𝕌 → 𝕌 → 𝕌
  _×ᵤ_    : 𝕌 → 𝕌 → 𝕌

⟦ 𝟘 ⟧ = ⊥
⟦ 𝟙 ⟧ = ⊤
⟦ t₁ +ᵤ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ t₁ ×ᵤ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

data _⟷_ where
  unite₊l : {t : 𝕌} → 𝟘 +ᵤ t ⟷ t
  uniti₊l : {t : 𝕌} → t ⟷ 𝟘 +ᵤ t
  unite₊r : {t : 𝕌} → t +ᵤ 𝟘 ⟷ t
  uniti₊r : {t : 𝕌} → t ⟷ t +ᵤ 𝟘
  swap₊   : {t₁ t₂ : 𝕌} → t₁ +ᵤ t₂ ⟷ t₂ +ᵤ t₁
  assocl₊ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ +ᵤ t₂) +ᵤ t₃
  assocr₊ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) +ᵤ t₃ ⟷ t₁ +ᵤ (t₂ +ᵤ t₃)
  unite⋆l : {t : 𝕌} → 𝟙 ×ᵤ t ⟷ t
  uniti⋆l : {t : 𝕌} → t ⟷ 𝟙 ×ᵤ t
  unite⋆r : {t : 𝕌} → t ×ᵤ 𝟙 ⟷ t
  uniti⋆r : {t : 𝕌} → t ⟷ t ×ᵤ 𝟙
  swap⋆   : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ⟷ t₂ ×ᵤ t₁
  assocl⋆ : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) ×ᵤ t₃
  assocr⋆ : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ⟷ t₁ ×ᵤ (t₂ ×ᵤ t₃)
  absorbr : {t : 𝕌} → 𝟘 ×ᵤ t ⟷ 𝟘
  absorbl : {t : 𝕌} → t ×ᵤ 𝟘 ⟷ 𝟘
  factorzr : {t : 𝕌} → 𝟘 ⟷ t ×ᵤ 𝟘
  factorzl : {t : 𝕌} → 𝟘 ⟷ 𝟘 ×ᵤ t
  dist    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) ×ᵤ t₃ ⟷ (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃)
  factor  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ +ᵤ t₂) ×ᵤ t₃
  distl   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)
  factorl : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃) ⟷ t₁ ×ᵤ (t₂ +ᵤ t₃)
  id⟷     : {t : 𝕌} → t ⟷ t
  _⊚_     : {t₁ t₂ t₃ : 𝕌} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ +ᵤ t₂ ⟷ t₃ +ᵤ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ ×ᵤ t₂ ⟷ t₃ ×ᵤ t₄)

!_ : {A B : 𝕌} → A ⟷ B → B ⟷ A
! unite₊l = uniti₊l
! uniti₊l = unite₊l
! unite₊r = uniti₊r
! uniti₊r = unite₊r
! swap₊ = swap₊
! assocl₊ = assocr₊
! assocr₊ = assocl₊
! unite⋆l = uniti⋆l
! uniti⋆l = unite⋆l
! unite⋆r = uniti⋆r
! uniti⋆r = unite⋆r
! swap⋆ = swap⋆
! assocl⋆ = assocr⋆
! assocr⋆ = assocl⋆
! absorbr = factorzl
! absorbl = factorzr
! factorzr = absorbl
! factorzl = absorbr
! dist = factor
! factor = dist
! distl = factorl
! factorl = distl
! id⟷ = id⟷
! (c₁ ⊚ c₂) = (! c₂) ⊚ (! c₁)
! (c₁ ⊕ c₂) = (! c₁) ⊕ (! c₂)
! (c₁ ⊗ c₂) = (! c₁) ⊗ (! c₂)

eval unite₊l (inj₂ v) = v
eval uniti₊l v  = inj₂ v
eval unite₊r (inj₁ v) = v
eval uniti₊r v  = inj₁ v
eval swap₊ (inj₁ v) = inj₂ v
eval swap₊ (inj₂ v) = inj₁ v
eval assocl₊ (inj₁ v) = inj₁ (inj₁ v)
eval assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
eval assocl₊ (inj₂ (inj₂ v)) = inj₂ v
eval assocr₊ (inj₁ (inj₁ v)) = inj₁ v
eval assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
eval assocr₊ (inj₂ v) = inj₂ (inj₂ v)
eval unite⋆l (tt , v) = v
eval uniti⋆l v = (tt , v)
eval unite⋆r (v , tt) = v
eval uniti⋆r v = (v , tt)
eval swap⋆ (v₁ , v₂)          = (v₂ , v₁)
eval assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
eval assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
eval absorbl ()
eval absorbr ()
eval factorzl ()
eval factorzr ()
eval dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
eval dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
eval factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
eval factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
eval distl (v , inj₁ v₁) = inj₁ (v , v₁)
eval distl (v , inj₂ v₂) = inj₂ (v , v₂)
eval factorl (inj₁ (v , v₁)) = (v , inj₁ v₁)
eval factorl (inj₂ (v , v₂)) = (v , inj₂ v₂)
eval id⟷ v = v
eval (c₁ ⊚ c₂) v = eval c₂ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₁ v) = inj₁ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₂ v) = inj₂ (eval c₂ v)
eval (c₁ ⊗ c₂) (v₁ , v₂) = (eval c₁ v₁ , eval c₂ v₂)

ΠisRev : ∀ {A B} → (c : A ⟷ B) (a : ⟦ A ⟧) → eval (c ⊚ ! c) a ≡ a
ΠisRev unite₊l (inj₂ y) = refl
ΠisRev uniti₊l a = refl
ΠisRev unite₊r (inj₁ x) = refl
ΠisRev uniti₊r a = refl
ΠisRev swap₊ (inj₁ x) = refl
ΠisRev swap₊ (inj₂ y) = refl
ΠisRev assocl₊ (inj₁ x) = refl
ΠisRev assocl₊ (inj₂ (inj₁ x)) = refl
ΠisRev assocl₊ (inj₂ (inj₂ y)) = refl
ΠisRev assocr₊ (inj₁ (inj₁ x)) = refl
ΠisRev assocr₊ (inj₁ (inj₂ y)) = refl
ΠisRev assocr₊ (inj₂ y) = refl
ΠisRev unite⋆l (tt , y) = refl
ΠisRev uniti⋆l a = refl
ΠisRev unite⋆r (x , tt) = refl
ΠisRev uniti⋆r a = refl
ΠisRev swap⋆ (x , y) = refl
ΠisRev assocl⋆ (x , (y , z)) = refl
ΠisRev assocr⋆ ((x , y) , z) = refl
ΠisRev dist (inj₁ x , z) = refl
ΠisRev dist (inj₂ y , z) = refl
ΠisRev factor (inj₁ (x , z)) = refl
ΠisRev factor (inj₂ (y , z)) = refl
ΠisRev distl (x , inj₁ y) = refl
ΠisRev distl (x , inj₂ z) = refl
ΠisRev factorl (inj₁ (x , y)) = refl
ΠisRev factorl (inj₂ (x , z)) = refl
ΠisRev id⟷ a = refl
ΠisRev (c₁ ⊚ c₂) a rewrite ΠisRev c₂ (eval c₁ a) = ΠisRev c₁ a
ΠisRev (c₁ ⊕ c₂) (inj₁ x) rewrite ΠisRev c₁ x = refl
ΠisRev (c₁ ⊕ c₂) (inj₂ y) rewrite ΠisRev c₂ y = refl
ΠisRev (c₁ ⊗ c₂) (x , y) rewrite ΠisRev c₁ x | ΠisRev c₂ y = refl

------------------------------------------------------------------------------
-- Pointed types and singleton types

data ∙𝕌 : Set where
  _#_ : (t : 𝕌) → (v : ⟦ t ⟧) → ∙𝕌
  _∙×ᵤ_ : ∙𝕌 → ∙𝕌 → ∙𝕌
  _∙+ᵤl_ : ∙𝕌 → ∙𝕌 → ∙𝕌
  _∙+ᵤr_ : ∙𝕌 → ∙𝕌 → ∙𝕌
  Singᵤ : ∙𝕌 → ∙𝕌
  Recipᵤ : ∙𝕌 → ∙𝕌

∙⟦_⟧ : ∙𝕌 → Σ[ A ∈ Set ] A
∙⟦ t # v ⟧ = ⟦ t ⟧ , v
∙⟦ T₁ ∙×ᵤ T₂ ⟧ = zip _×_ _,_ ∙⟦ T₁ ⟧ ∙⟦ T₂ ⟧
∙⟦ T₁ ∙+ᵤl T₂ ⟧ = zip _⊎_ (λ x _ → inj₁ x) ∙⟦ T₁ ⟧ ∙⟦ T₂ ⟧
∙⟦ T₁ ∙+ᵤr T₂ ⟧ = zip _⊎_ (λ _ y → inj₂ y) ∙⟦ T₁ ⟧ ∙⟦ T₂ ⟧
∙⟦ Singᵤ T ⟧ = < uncurry Singleton , (λ y → proj₂ y , refl) > ∙⟦ T ⟧
∙⟦ Recipᵤ T ⟧ = < uncurry Recip , (λ _ _ → tt) > ∙⟦ T ⟧

∙𝟙 : ∙𝕌
∙𝟙 = 𝟙 # tt

data _∙⟶_ : ∙𝕌 → ∙𝕌 → Set where
  -- when we know the base type
  ∙c :  {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} →
        (c : t₁ ⟷ t₂) → t₁ # v ∙⟶ t₂ # (eval c v)
  ∙times# : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            ((t₁ ×ᵤ t₂) # (v₁ , v₂)) ∙⟶ ((t₁ # v₁) ∙×ᵤ (t₂ # v₂))
  ∙#times : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            ((t₁ # v₁) ∙×ᵤ (t₂ # v₂)) ∙⟶ ((t₁ ×ᵤ t₂) # (v₁ , v₂))
  -- some things need to be explicitly lifted
  ∙id⟷ : {T : ∙𝕌} → T ∙⟶ T
  _∙⊚_ : {T₁ T₂ T₃ : ∙𝕌} → (T₁ ∙⟶ T₂) → (T₂ ∙⟶ T₃) → (T₁ ∙⟶ T₃)
  ∙unite⋆l : {t : ∙𝕌} → ∙𝟙 ∙×ᵤ t ∙⟶ t
  ∙uniti⋆l : {t : ∙𝕌} → t ∙⟶ ∙𝟙 ∙×ᵤ t
  ∙unite⋆r : {t : ∙𝕌} → t ∙×ᵤ ∙𝟙 ∙⟶ t
  ∙uniti⋆r : {t : ∙𝕌} → t ∙⟶ t ∙×ᵤ ∙𝟙
  ∙swap⋆   : {T₁ T₂ : ∙𝕌} → T₁ ∙×ᵤ T₂ ∙⟶ T₂ ∙×ᵤ T₁
  ∙assocl⋆ : {T₁ T₂ T₃ : ∙𝕌} → T₁ ∙×ᵤ (T₂ ∙×ᵤ T₃) ∙⟶ (T₁ ∙×ᵤ T₂) ∙×ᵤ T₃
  ∙assocr⋆ : {T₁ T₂ T₃ : ∙𝕌} → (T₁ ∙×ᵤ T₂) ∙×ᵤ T₃ ∙⟶ T₁ ∙×ᵤ (T₂ ∙×ᵤ T₃)
  _∙⊗_ : {T₁ T₂ T₃ T₄ : ∙𝕌} → (T₁ ∙⟶ T₃) → (T₂ ∙⟶ T₄)
       → (T₁ ∙×ᵤ T₂ ∙⟶ T₃ ∙×ᵤ T₄)
  _∙⊕ₗ_ : {T₁ T₂ T₃ T₄ : ∙𝕌} → (T₁ ∙⟶ T₃) → (T₂ ∙⟶ T₄)
        → (T₁ ∙+ᵤl T₂ ∙⟶ T₃ ∙+ᵤl T₄)
  _∙⊕ᵣ_ : {T₁ T₂ T₃ T₄ : ∙𝕌} → (T₁ ∙⟶ T₃) → (T₂ ∙⟶ T₄)
        → (T₁ ∙+ᵤr T₂ ∙⟶ T₃ ∙+ᵤr T₄)
  -- monad
  return : (T : ∙𝕌) → T ∙⟶ Singᵤ T
  -- comonad
  extract : (T : ∙𝕌) → Singᵤ T ∙⟶ T
  -- eta/epsilon
  η : (T : ∙𝕌) → ∙𝟙 ∙⟶ (Singᵤ T ∙×ᵤ Recipᵤ T)
  ε : (T : ∙𝕌) → (Singᵤ T ∙×ᵤ Recipᵤ T) ∙⟶ ∙𝟙

tensor : {T₁ T₂ : ∙𝕌} → (Singᵤ T₁ ∙×ᵤ Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙×ᵤ T₂)
tensor {T₁} {T₂} = (extract T₁ ∙⊗ extract T₂) ∙⊚ return (T₁ ∙×ᵤ T₂)

untensor : {T₁ T₂ : ∙𝕌} → Singᵤ (T₁ ∙×ᵤ T₂) ∙⟶ (Singᵤ T₁ ∙×ᵤ Singᵤ T₂)
untensor {T₁} {T₂} = extract (T₁ ∙×ᵤ T₂) ∙⊚ (return T₁ ∙⊗ return T₂)

tensorl : {T₁ T₂ : ∙𝕌} → (Singᵤ T₁ ∙×ᵤ T₂) ∙⟶ Singᵤ (T₁ ∙×ᵤ T₂)
tensorl {T₁} {T₂} = (extract T₁ ∙⊗ ∙id⟷) ∙⊚ return (T₁ ∙×ᵤ T₂)

tensorr : {T₁ T₂ : ∙𝕌} → (T₁ ∙×ᵤ Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙×ᵤ T₂)
tensorr {T₁} {T₂} = (∙id⟷ ∙⊗ extract T₂) ∙⊚ return (T₁ ∙×ᵤ T₂)

cotensorl : {T₁ T₂ : ∙𝕌} → Singᵤ (T₁ ∙×ᵤ T₂) ∙⟶ (Singᵤ T₁ ∙×ᵤ T₂)
cotensorl {T₁} {T₂} = extract (T₁ ∙×ᵤ T₂) ∙⊚ (return T₁ ∙⊗ ∙id⟷)

cotensorr : {T₁ T₂ : ∙𝕌} → Singᵤ (T₁ ∙×ᵤ T₂) ∙⟶ (T₁ ∙×ᵤ Singᵤ T₂)
cotensorr {T₁} {T₂} = extract (T₁ ∙×ᵤ T₂) ∙⊚ (∙id⟷ ∙⊗ return T₂)

plusl : {T₁ T₂ : ∙𝕌} → (Singᵤ T₁ ∙+ᵤl T₂) ∙⟶ Singᵤ (T₁ ∙+ᵤl T₂)
plusl {T₁} {T₂} = (extract T₁ ∙⊕ₗ ∙id⟷) ∙⊚ return (T₁ ∙+ᵤl T₂)

plusr : {T₁ T₂ : ∙𝕌} → (T₁ ∙+ᵤr Singᵤ T₂) ∙⟶ Singᵤ (T₁ ∙+ᵤr T₂)
plusr {T₁} {T₂} = (∙id⟷ ∙⊕ᵣ extract T₂) ∙⊚ return (T₁ ∙+ᵤr T₂)

coplusl : {T₁ T₂ : ∙𝕌} → Singᵤ (T₁ ∙+ᵤl T₂) ∙⟶ (Singᵤ T₁ ∙+ᵤl T₂)
coplusl {T₁} {T₂} = extract (T₁ ∙+ᵤl T₂) ∙⊚ (return T₁ ∙⊕ₗ ∙id⟷)

coplusr : {T₁ T₂ : ∙𝕌} → Singᵤ (T₁ ∙+ᵤr T₂) ∙⟶ (T₁ ∙+ᵤr Singᵤ T₂)
coplusr {T₁} {T₂} = extract (T₁ ∙+ᵤr T₂) ∙⊚ (∙id⟷ ∙⊕ᵣ return T₂)

-- functor
∙Singᵤ : {T₁ T₂ : ∙𝕌} → (T₁ ∙⟶ T₂) → (Singᵤ T₁ ∙⟶ Singᵤ T₂)
∙Singᵤ {T₁} {T₂} c = extract T₁ ∙⊚ c ∙⊚ return T₂

join : {T₁ : ∙𝕌} → Singᵤ (Singᵤ T₁) ∙⟶ Singᵤ T₁
join {T₁} = extract (Singᵤ T₁)

duplicate : {T₁ : ∙𝕌} → Singᵤ T₁ ∙⟶ Singᵤ (Singᵤ T₁)
duplicate {T₁} = return (Singᵤ T₁)

!∙_ : {A B : ∙𝕌} → A ∙⟶ B → B ∙⟶ A
!∙ (∙c {t₁} {t₂} {v} c) = subst (λ x → t₂ # eval c v ∙⟶ t₁ # x) (ΠisRev c v) (∙c (! c))
!∙ ∙times# = ∙#times
!∙ ∙#times = ∙times#
!∙ ∙id⟷ = ∙id⟷
!∙ (c₁ ∙⊚ c₂) = (!∙ c₂) ∙⊚ (!∙ c₁)
!∙ ∙unite⋆l = ∙uniti⋆l
!∙ ∙uniti⋆l = ∙unite⋆l
!∙ ∙unite⋆r = ∙uniti⋆r
!∙ ∙uniti⋆r = ∙unite⋆r
!∙ ∙swap⋆ = ∙swap⋆
!∙ ∙assocl⋆ = ∙assocr⋆
!∙ ∙assocr⋆ = ∙assocl⋆
!∙ (c₁ ∙⊗ c₂) = (!∙ c₁) ∙⊗ (!∙ c₂)
!∙ (c₁ ∙⊕ₗ c₂) = (!∙ c₁) ∙⊕ₗ (!∙ c₂)
!∙ (c₁ ∙⊕ᵣ c₂) = (!∙ c₁) ∙⊕ᵣ (!∙ c₂)
!∙ return T = extract T
!∙ extract T = return T
!∙ η T = ε T
!∙ ε T = η T

∙eval : {T₁ T₂ : ∙𝕌} → (C : T₁ ∙⟶ T₂) →
  let (t₁ , v₁) = ∙⟦ T₁ ⟧
      (t₂ , v₂) = ∙⟦ T₂ ⟧
  in Σ (t₁ → t₂) (λ f → f v₁ ≡ v₂)
∙eval ∙id⟷ = (λ x → x) , refl
∙eval (∙c c) = eval c , refl
∙eval (C₁ ∙⊚ C₂) with ∙eval C₁ | ∙eval C₂
... | (f , p) | (g , q) = (λ x → g (f x)) , trans (cong g p) q
∙eval ∙unite⋆l = (λ {(tt , x) → x}) , refl
∙eval ∙uniti⋆l = (λ {x → (tt , x)}) , refl
∙eval ∙unite⋆r = (λ {(x , tt) → x}) , refl
∙eval ∙uniti⋆r = (λ {x → (x , tt)}) , refl
∙eval ∙swap⋆ = (λ {(x , y) → y , x}) , refl
∙eval ∙assocl⋆ = (λ {(x , (y , z)) → ((x , y) , z)}) , refl
∙eval ∙assocr⋆ = (λ {((x , y) , z) → (x , (y , z))}) , refl
∙eval (C₀ ∙⊗ C₁) with ∙eval C₀ | ∙eval C₁
... | (f , p) | (g , q) = (λ {(t₁ , t₂) → f t₁ , g t₂}) , cong₂ _,_ p q
∙eval (C₀ ∙⊕ₗ C₁) with ∙eval C₀ | ∙eval C₁
... | (f , p) | (g , q) = (λ { (inj₁ x) → inj₁ (f x)
                             ; (inj₂ y) → inj₂ (g y) })
                        , cong inj₁ p
∙eval (C₀ ∙⊕ᵣ C₁) with ∙eval C₀ | ∙eval C₁
... | (f , p) | (g , q) = (λ { (inj₁ x) → inj₁ (f x)
                             ; (inj₂ y) → inj₂ (g y) })
                        , cong inj₂ q
∙eval ∙times# = (λ x → x) , refl
∙eval ∙#times = (λ x → x) , refl
∙eval (return T) = (λ _ → proj₂ ∙⟦ T ⟧ , refl) , refl
∙eval (extract T) = (λ {(w , refl) → w}) , refl
∙eval (η T) = (λ tt → (proj₂ ∙⟦ T ⟧ , refl) , λ _ → tt) , refl
∙eval (ε T) = (λ { ((_ , refl) , f) → f (proj₂ ∙⟦ T ⟧ , refl)}) , refl

-- you don't need to prove this
∙ΠisRev : ∀ {T₁ T₂} → (c : T₁ ∙⟶ T₂) →
  let (t₁ , v₁) = ∙⟦ T₁ ⟧
      (t₂ , v₂) = ∙⟦ T₂ ⟧
      (f , pf) = ∙eval (c ∙⊚ !∙ c) in
  f v₁ ≡ v₁
∙ΠisRev c = proj₂ (∙eval (c ∙⊚ !∙ c))

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Formalization.LambdaCalculus.SyntaxTransformation where

open import Formalization.LambdaCalculus
open import Lang.Instance
open import Numeral.Natural
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals

private variable d d₁ d₂ : ℕ
private variable x y : Term(d)

-- Increase the depth level of the given term by something.
-- Example: `depth-[≤](Var(2) : Term(5)) = Var(2) : Term(50)`
depth-[≤] : ⦃ _ : (d₁ ≤ d₂) ⦄ → Term(d₁) → Term(d₂)
depth-[≤] (Apply t1 t2) = Apply(depth-[≤] t1) (depth-[≤] t2)
depth-[≤] (Abstract t)  = Abstract(depth-[≤] t)
depth-[≤] (Var x)       = Var(bound-[≤] infer x)

-- Increment the depth level of the given term by 1.
-- Example: `depth-𝐒(Var(2) : Term(5)) = Var(2) : Term(6)`
depth-𝐒 : Term(d) → Term(𝐒(d))
depth-𝐒 = depth-[≤]
-- depth-𝐒 (Apply(f)(x))       = Apply (depth-𝐒(f)) (depth-𝐒(x))
-- depth-𝐒 (Abstract(body))    = Abstract(depth-𝐒(body))
-- depth-𝐒 (Var(n))            = Var(bound-𝐒 (n))

Apply₊ : ⦃ _ : (d₁ ≤ d₂) ⦄ → Term(d₂) → Term(d₁) → Term(d₂)
Apply₊ {d₁}{d₂} f(x) = Apply f(depth-[≤] {d₁}{d₂} (x))

{-
-- Increase all variables of the given term
var-[≤] : ∀{d₁ d₂} → ⦃ _ : (d₁ ≤ d₂) ⦄ → Term(d₁) → Term(d₂)
var-[≤] (Apply t1 t2) = Apply(depth-[≤] t1) (depth-[≤] t2)
var-[≤] (Abstract t)  = Abstract(depth-[≤] t)
var-[≤] (Var x) = Var({!x + (d₂ − d₁)!}) where
  open import Numeral.Natural.TotalOper
-}

-- Increment all variables of the given term.
-- Example: `var-𝐒(Var(2) : Term(5)) = Var(3) : Term(6)`
-- Examples:
--   term : Term(1)
--   term = (1 ↦ (2 ↦ 2 ← 2) ← 0 ← 1 ← 0)
--
--   Then:
--   term               = 1 ↦ (2 ↦ 2 ← 2) ← 0 ← 1 ← 0
--   var-𝐒(term)        = 2 ↦ (3 ↦ 3 ← 3) ← 1 ← 2 ← 1
--   var-𝐒(var-𝐒(term)) = 3 ↦ (4 ↦ 4 ← 4) ← 2 ← 3 ← 2
var-𝐒 : Term(d) → Term(𝐒(d))
var-𝐒 (Apply(f)(x))       = Apply (var-𝐒(f)) (var-𝐒(x))
var-𝐒 (Abstract{d}(body)) = Abstract{𝐒(d)} (var-𝐒(body))
var-𝐒 (Var{𝐒(d)}(n))      = Var{𝐒(𝐒(d))} (𝐒(n))

-- Substitutes the most recent free variable with a term in a term, while also decrementing them.
-- `substitute val term` is the term where all occurences in `term` of the outer-most variable is replaced with the term `val`.
-- Examples:
--   substituteOuterVar x (Var(0) : Term(1)) = x
--   substituteOuterVar x ((Apply (Var(1)) (Var(0))) : Term(2)) = Apply (Var(0)) x
--   substituteOuterVar (𝜆 0 0) ((𝜆 1 1) ← 0) = ((𝜆 0 0) ← (𝜆 0 0))
--   substituteOuterVar (𝜆 0 0) ((𝜆 1 1 ← 0) ← 0) = (((𝜆 0 0) ← (𝜆 0 0)) ← (𝜆 0 0))
substituteVar0 : Term(d) → Term(𝐒(d)) → Term(d)
substituteVar0 val (Apply(f)(x))    = Apply (substituteVar0 val f) (substituteVar0 val x)
substituteVar0 val (Abstract(body)) = Abstract (substituteVar0 (var-𝐒 val) body)
substituteVar0 val (Var(𝟎))         = val
substituteVar0 val (Var(𝐒(v)))      = Var v

{-
substituteMap : (𝕟(d₁) → Term(d₂)) → Term(d₁) → Term(d₂)
substituteMap F (Apply(f)(x))    = Apply (substituteMap F (f)) (substituteMap F (x))
substituteMap F (Var(v))         = F(v)
substituteMap F (Abstract(body)) = Abstract (substituteMap F (body)) -- TODO: Probably incorrect
-}

-- Substituting the outer variable of `var-𝐒 x` yields `x`.
-- This is useful because `substituteVar0` uses `var-𝐒` in its definition.
substituteVar0-var-𝐒 : (substituteVar0 y (var-𝐒 x) ≡ x)
substituteVar0-var-𝐒 {d}{y}{Apply f x}  rewrite substituteVar0-var-𝐒 {d}{y}{f} rewrite substituteVar0-var-𝐒 {d}{y}{x} = [≡]-intro
substituteVar0-var-𝐒 {d}{y}{Abstract x} rewrite substituteVar0-var-𝐒 {𝐒 d}{var-𝐒 y}{x} = [≡]-intro
substituteVar0-var-𝐒 {_}{_}{Var 𝟎}      = [≡]-intro
substituteVar0-var-𝐒 {_}{_}{Var(𝐒 _)}   = [≡]-intro
{-# REWRITE substituteVar0-var-𝐒 #-}

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:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}

module Cubical.HITs.InfNat.Properties where

open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Data.Nat

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

open import Cubical.HITs.InfNat.Base
import Cubical.Data.InfNat as Coprod

ℕ+∞→Cℕ+∞ : ℕ+∞ → Coprod.ℕ+∞
ℕ+∞→Cℕ+∞ zero = Coprod.zero
ℕ+∞→Cℕ+∞ (suc n) = Coprod.suc (ℕ+∞→Cℕ+∞ n)
ℕ+∞→Cℕ+∞ ∞ = Coprod.∞
ℕ+∞→Cℕ+∞ (suc-inf i) = Coprod.∞

ℕ→ℕ+∞ : ℕ → ℕ+∞
ℕ→ℕ+∞ zero = zero
ℕ→ℕ+∞ (suc n) = suc (ℕ→ℕ+∞ n)

Cℕ+∞→ℕ+∞ : Coprod.ℕ+∞ → ℕ+∞
Cℕ+∞→ℕ+∞ Coprod.∞ = ∞
Cℕ+∞→ℕ+∞ (Coprod.fin n) = ℕ→ℕ+∞ n

ℕ→ℕ+∞→Cℕ+∞ : ∀ n → ℕ+∞→Cℕ+∞ (ℕ→ℕ+∞ n) ≡ Coprod.fin n
ℕ→ℕ+∞→Cℕ+∞ zero = refl
ℕ→ℕ+∞→Cℕ+∞ (suc n) = cong Coprod.suc (ℕ→ℕ+∞→Cℕ+∞ n)

Cℕ+∞→ℕ+∞→Cℕ+∞ : ∀ n → ℕ+∞→Cℕ+∞ (Cℕ+∞→ℕ+∞ n) ≡ n
Cℕ+∞→ℕ+∞→Cℕ+∞ Coprod.∞ = refl
Cℕ+∞→ℕ+∞→Cℕ+∞ (Coprod.fin n) = ℕ→ℕ+∞→Cℕ+∞ n

suc-hom : ∀ n → Cℕ+∞→ℕ+∞ (Coprod.suc n) ≡ suc (Cℕ+∞→ℕ+∞ n)
suc-hom Coprod.∞ = suc-inf
suc-hom (Coprod.fin x) = refl

ℕ+∞→Cℕ+∞→ℕ+∞ : ∀ n → Cℕ+∞→ℕ+∞ (ℕ+∞→Cℕ+∞ n) ≡ n
ℕ+∞→Cℕ+∞→ℕ+∞ zero = refl
ℕ+∞→Cℕ+∞→ℕ+∞ ∞ = refl
ℕ+∞→Cℕ+∞→ℕ+∞ (suc n) = suc-hom (ℕ+∞→Cℕ+∞ n) ∙ cong suc (ℕ+∞→Cℕ+∞→ℕ+∞ n)
ℕ+∞→Cℕ+∞→ℕ+∞ (suc-inf i) = lemma i
  where
  lemma : (λ i → ∞ ≡ suc-inf i) [ refl ≡ suc-inf ∙ refl ]
  lemma i j = hcomp (λ k → λ
    { (i = i0) → ∞
    ; (i = i1) → compPath-filler suc-inf refl k j
    ; (j = i0) → ∞
    ; (j = i1) → suc-inf i
    }) (suc-inf (i ∧ j))

open Iso

ℕ+∞⇔Cℕ+∞ : Iso ℕ+∞ Coprod.ℕ+∞
ℕ+∞⇔Cℕ+∞ .fun = ℕ+∞→Cℕ+∞
ℕ+∞⇔Cℕ+∞ .inv = Cℕ+∞→ℕ+∞
ℕ+∞⇔Cℕ+∞ .leftInv = ℕ+∞→Cℕ+∞→ℕ+∞
ℕ+∞⇔Cℕ+∞ .rightInv = Cℕ+∞→ℕ+∞→Cℕ+∞

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Function.Surjective where

open import Function.Surjective.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Issue3295 where

open import Issue3295.Incomplete
open import Issue3295.Incomplete2
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

_ : f 0 ≡ 0
_ = {!!}

_ : g 0 ≡ 0
_ = {!!}

_ : f 1 ≡ 1 -- the evaluation of `f` should be blocked here
_ = {!!}    -- so looking at the normalised type should not cause any issue

_ : g 1 ≡ 1 -- the evaluation of `g` should be blocked here
_ = {!!}    -- so looking at the normalised type should not cause any issue


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

open import Relation.Binary using (Poset)

-- A thin (or posetal) category is a category with at most one
-- morphism between any pair of objects.
--
-- As explained on nLab:
--
--   "Up to isomorphism, a thin category is the same thing as a
--   proset. Up to equivalence, a thin category is the same thing as a
--   poset. (...) (It is really a question of whether you're working
--   with strict categories, which are classified up to isomorphism,
--   or categories as such, which are classified up to equivalence.)"
--
--                  -- https://ncatlab.org/nlab/show/thin+category
--
-- Since
--
--  1. posets in the standard library are defined up to an underlying
--     equivalence/setoid, but
--
--  2. categories in this library do not have a notion of equality on
--     objects (i.e. objects are considered up to isomorphism),
--
-- it makes sense to work with the weaker notion of thin categories
-- here, i.e. those generated by posets rather than prosets.  This
-- means that the core of a thin category (the groupoid consisting of
-- all its isomorphism) is just the setoid underlying the
-- corresponding poset.
--
-- (See Categories.Adjoint.Instance.PosetCore for more details.)

module Categories.Category.Construction.Thin {o ℓ₁ ℓ₂} e (P : Poset o ℓ₁ ℓ₂) where

open import Level
open import Data.Unit using (⊤)
open import Function using (flip)

open import Categories.Category
import Categories.Morphism as Morphism

open Poset P

Thin : Category o ℓ₂ e
Thin = record
  { Obj       = Carrier
  ; _⇒_       = _≤_
  ; _≈_       = λ _ _ → Lift e ⊤
  ; id        = refl
  ; _∘_       = flip trans
  ; assoc     = _
  ; identityˡ = _
  ; identityʳ = _
  ; equiv     = _
  ; ∘-resp-≈  = _
  }

module EqIsIso where

  open Category Thin hiding (_≈_)
  open Morphism Thin using (_≅_)
  open _≅_

  -- Equivalent elements of |P| are isomorphic objects of |Thin P|.

  ≈⇒≅ : ∀ {x y : Obj} → x ≈ y → x ≅ y
  ≈⇒≅ x≈y = record
    { from = reflexive x≈y
    ; to   = reflexive (Eq.sym x≈y)
    }

  ≅⇒≈ : ∀ {x y : Obj} → x ≅ y → x ≈ y
  ≅⇒≈ x≅y = antisym (from x≅y) (to x≅y)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Data.Char.Base using (Char)
open import Data.List.Base using (List; []; _∷_)

module PiCalculus.Syntax where

Name : Set
Name = List Char

module Raw where
  infixr 20 _∥_
  infixr 15 ⦅ν_⦆_
  infixr 10 _⦅_⦆_ _⟨_⟩_

  data Raw : Set where
    𝟘     : Raw
    ⦅ν_⦆_ : Name → Raw → Raw
    _∥_   : Raw → Raw → Raw
    _⦅_⦆_ : Name → Name → Raw → Raw
    _⟨_⟩_ : Name → Name → Raw → Raw

module Scoped where
  open import Data.Fin.Base
  open import Data.Nat.Base

  infixr 20 _∥_
  infixr 15 ν
  infixr 10 _⦅⦆_ _⟨_⟩_

  private
    variable
      n : ℕ

  data Scoped : ℕ → Set where
    𝟘     : Scoped n
    ν : Scoped (suc n) → ⦃ name : Name ⦄ → Scoped n
    _∥_   : Scoped n → Scoped n → Scoped n
    _⦅⦆_ : Fin n → Scoped (suc n) → ⦃ name : Name ⦄ → Scoped n
    _⟨_⟩_ : Fin n → Fin n → Scoped n → Scoped n

module Conversion where
  private
    open Raw
    open Scoped

    open import Level using (Lift; _⊔_)
    open import Function using (_∘_)
    open import Relation.Nullary using (Dec; yes; no)
    open import Relation.Nullary.Decidable using (isYes; True; toWitness)
    open import Relation.Nullary.Product using (_×-dec_)
    open import Relation.Nullary.Negation using (¬?)

    import Data.Vec.Base as Vec
    import Data.Char.Base as Char
    import Data.Char.Properties as Charₚ
    import Data.List.Base as List
    import Data.List.Properties as Listₚ
    import Data.String.Base as String
    import Data.String.Properties as Stringₚ
    import Data.Nat.Show as ℕₛ
    import Data.Vec.Membership.DecPropositional as DecPropositional

    open import Data.Empty using (⊥)
    open import Data.Bool.Base using (true; false; if_then_else_)
    open import Data.Product using (_,_; _×_)
    open import Data.Unit using (⊤; tt)
    open import Data.Nat.Base using (ℕ; zero; suc)
    open import Data.Fin.Base using (Fin; zero; suc)
    open import Data.String.Base using (_++_)
    open import Data.Vec.Membership.Propositional using (_∈_; _∉_)
    open import Data.Vec.Relation.Unary.Any using (here; there)

    open Vec using (Vec; []; _∷_)

    _∈?_ = DecPropositional._∈?_ (Listₚ.≡-dec Charₚ._≟_)

    variable
      n m : ℕ

  Ctx : ℕ → Set
  Ctx = Vec Name

  count : Name → Ctx n → ℕ
  count name = Vec.count (Listₚ.≡-dec Charₚ._≟_ name)

  toChars : Name × ℕ → List Char.Char
  toChars (x , i) = x List.++ ('^' ∷ ℕₛ.charsInBase 10 i)

  repr : ∀ x (xs : Vec Name n) → Name
  repr x xs = toChars (x , (count x xs))

  apply : Ctx n → Ctx n
  apply [] = []
  apply (x ∷ xs) = repr x xs ∷ apply xs

  WellScoped : Ctx n → Raw → Set
  WellScoped ctx 𝟘 = ⊤
  WellScoped ctx (⦅ν x ⦆ P) = WellScoped (x ∷ ctx) P
  WellScoped ctx (P ∥ Q) = WellScoped ctx P × WellScoped ctx Q
  WellScoped ctx (x ⦅ y ⦆ P) = (x ∈ ctx) × WellScoped (y ∷ ctx) P
  WellScoped ctx (x ⟨ y ⟩ P) = (x ∈ ctx) × (y ∈ ctx) × WellScoped ctx P

  WellScoped? : (ctx : Ctx n) (P : Raw) → Dec (WellScoped ctx P)
  WellScoped? ctx 𝟘 = yes tt
  WellScoped? ctx (⦅ν x ⦆ P) = WellScoped? (x ∷ ctx) P
  WellScoped? ctx (P ∥ Q) = WellScoped? ctx P ×-dec WellScoped? ctx Q
  WellScoped? ctx (x ⦅ y ⦆ P) = x ∈? ctx ×-dec WellScoped? (y ∷ ctx) P
  WellScoped? ctx (x ⟨ y ⟩ P) = x ∈? ctx ×-dec y ∈? ctx ×-dec WellScoped? ctx P

  NotShadowed : Ctx n → Raw → Set
  NotShadowed ctx 𝟘 = ⊤
  NotShadowed ctx (⦅ν name ⦆ P) = name ∉ ctx × NotShadowed (name ∷ ctx) P
  NotShadowed ctx (P ∥ Q) = NotShadowed ctx P × NotShadowed ctx Q
  NotShadowed ctx (x ⦅ y ⦆ P) = y ∉ ctx × NotShadowed (y ∷ ctx) P
  NotShadowed ctx (x ⟨ y ⟩ P) = NotShadowed ctx P

  NotShadowed? : (ctx : Ctx n) (P : Raw) → Dec (NotShadowed ctx P)
  NotShadowed? ctx 𝟘 = yes tt
  NotShadowed? ctx (⦅ν name ⦆ P) = ¬? (name ∈? ctx) ×-dec NotShadowed? (name ∷ ctx) P
  NotShadowed? ctx (P ∥ Q) = NotShadowed? ctx P ×-dec NotShadowed? ctx Q
  NotShadowed? ctx (x ⦅ y ⦆ P) = ¬? (y ∈? ctx) ×-dec NotShadowed? (y ∷ ctx) P
  NotShadowed? ctx (x ⟨ y ⟩ P) = NotShadowed? ctx P

  ∈toFin : ∀ {a} {A : Set a} {x} {xs : Vec A n} → x ∈ xs → Fin n
  ∈toFin (here px) = zero
  ∈toFin (there x∈xs) = suc (∈toFin x∈xs)

  fromRaw' : (ctx : Ctx n) (P : Raw) → WellScoped ctx P → Scoped n
  fromRaw' ctx 𝟘 tt = 𝟘
  fromRaw' ctx (⦅ν x ⦆ P) wsP =
    ν (fromRaw' (x ∷ ctx) P wsP) ⦃ x ⦄
  fromRaw' ctx (P ∥ Q) (wsP , wsQ) =
    fromRaw' ctx P wsP ∥ fromRaw' ctx Q wsQ
  fromRaw' ctx (x ⦅ y ⦆ P) (x∈ctx , wsP) =
    (∈toFin x∈ctx ⦅⦆ fromRaw' (y ∷ ctx) P wsP) ⦃ y ⦄
  fromRaw' ctx (x ⟨ y ⟩ P) (x∈ctx , y∈ctx , wsP) =
    ∈toFin x∈ctx ⟨ ∈toFin y∈ctx ⟩ fromRaw' ctx P wsP

  fromRaw : (ctx : Ctx n) (P : Raw) → ⦃ _ : True (WellScoped? ctx P) ⦄ → Scoped n
  fromRaw ctx P ⦃ p ⦄ = fromRaw' ctx P (toWitness p)

  toRaw : Ctx n → Scoped n → Raw
  toRaw ctx 𝟘 = 𝟘
  toRaw ctx (ν P ⦃ name ⦄) =
    ⦅ν repr name ctx ⦆ toRaw (name ∷ ctx) P
  toRaw ctx (P ∥ Q) =
    toRaw ctx P ∥ toRaw ctx Q
  toRaw ctx ((x ⦅⦆ P) ⦃ name ⦄) =
    let ctx' = apply ctx
    in Vec.lookup ctx' x ⦅ repr name ctx ⦆ toRaw (name ∷ ctx) P
  toRaw ctx (x ⟨ y ⟩ P) =
    let ctx' = apply ctx
    in Vec.lookup ctx' x ⟨ Vec.lookup ctx' y ⟩ toRaw ctx P

  map : ∀ {a} (B : Scoped n → Set a) (ctx : Vec Name n) (P : Raw) → Set a
  map B ctx P with WellScoped? ctx P
  map B ctx P | yes wsP = B (fromRaw' ctx P wsP)
  map B ctx P | no _ = Lift _ ⊥

  map₂ : ∀ {a} (B : Scoped n → Scoped n → Set a) (ctx : Vec Name n) (P Q : Raw) → Set a
  map₂ B ctx P Q with WellScoped? ctx P | WellScoped? ctx Q
  map₂ B ctx P Q | yes wsP | yes wsQ = B (fromRaw' ctx P wsP) (fromRaw' ctx Q wsQ)
  map₂ B ctx P Q | _       | _       = Lift _ ⊥

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-
  Day 3, 1st part
-}
module a3 where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String; primShowNat)
open import Agda.Builtin.Equality

open import Data.Nat
open import Data.Bool
open import Data.List hiding (lookup;allFin)
                      renaming (map to mapList)
open import Data.Vec
open import Data.Fin hiding (_+_)
open import Data.Maybe renaming (map to maybeMap)

open import a3-input

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

-- helper
showMaybeNat : Maybe ℕ → String
showMaybeNat (just n) = primShowNat n
showMaybeNat nothing = "nothing"

data Bit : Set where
  one : Bit
  zero : Bit

BitVec = Vec Bit

Vecℕ→BitVec : {n : ℕ} → Vec ℕ n → Maybe (BitVec n)
Vecℕ→BitVec [] = just []
Vecℕ→BitVec (x ∷ v) with Vecℕ→BitVec v
...                     | just v' with x
...                                  | 0 = just (zero ∷ v')
...                                  | 1 = just (one ∷ v')
...                                  | suc (suc _) = nothing
Vecℕ→BitVec (x ∷ v)     | nothing = nothing

findMostCommonBit : {n : ℕ} (index : Fin n) → List (BitVec n) → Bit
findMostCommonBit {n = n} index input = iterate 0 0 input
  where
        iterate : (zeros : ℕ) (ones : ℕ) → List (BitVec n) → Bit
        iterate zeros ones [] =
          if zeros <ᵇ ones then one else zero
        iterate zeros ones (bitVec ∷ list) with lookup bitVec index
        ...                                   | zero = iterate (1 + zeros) ones list
        ...                                   | one = iterate zeros (1 + ones) list

bitVecToℕ : {n : ℕ} → BitVec n → ℕ
bitVecToℕ [] = 0
bitVecToℕ (zero ∷ v) = bitVecToℕ v
bitVecToℕ {n = suc n} (one ∷ v) = 2 ^ n + (bitVecToℕ v)

invertBitVec  : {n : ℕ} → BitVec n → BitVec n
invertBitVec  [] = []
invertBitVec  (zero ∷ v) = one ∷ invertBitVec v
invertBitVec  (one ∷ v) = zero ∷ invertBitVec v

listMaybe : {A : Set} → List (Maybe A) → Maybe (List A)
listMaybe [] = just []
listMaybe (just x ∷ list) with listMaybe list
...                          | just proccessedList = just (x ∷ proccessedList)
...                          | nothing = nothing
listMaybe (nothing ∷ list) = nothing

doTask : List (BitVec 12) → ℕ
doTask input = gamma * epsilon
               where
                 bitVecGamma = map (λ index → findMostCommonBit index input) (allFin 12)
                 gamma : ℕ
                 gamma = bitVecToℕ bitVecGamma
                 epsilon = bitVecToℕ (invertBitVec bitVecGamma)

main : IO ⊤
main = putStrLn (showMaybeNat ((maybeMap doTask) (listMaybe (mapList Vecℕ→BitVec input))))

private
  -- checks from the exercise text
  testInput : Maybe (List (BitVec 5))
  testInput = listMaybe (mapList Vecℕ→BitVec
    ((0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
    (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
    (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
    (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
    (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
    (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
    (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
    (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
    (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
    (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
    (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
    (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
    []))

  _ : maybeMap (findMostCommonBit Fin.zero) testInput ≡ just one
  _ = refl

  _ : maybeMap (findMostCommonBit (Fin.suc Fin.zero)) testInput ≡ just zero
  _ = refl

  _ : maybeMap (findMostCommonBit (Fin.suc (Fin.suc Fin.zero))) testInput ≡ just one
  _ = refl

  _ : maybeMap (findMostCommonBit (Fin.suc (Fin.suc (Fin.suc Fin.zero)))) testInput ≡ just one
  _ = refl

  _ : maybeMap (findMostCommonBit (fromℕ 4)) testInput ≡ just zero
  _ = refl

  -- test bitVecToℕ
  _ : bitVecToℕ (one ∷ zero ∷ one ∷ one ∷ zero ∷ []) ≡ 22
  _ = refl

  _ : Vecℕ→BitVec (1 ∷ 0 ∷ 1 ∷ 1 ∷ 0 ∷ []) ≡ just (one ∷ zero ∷ one ∷ one ∷ zero ∷ [])
  _ = refl

  _ : Vecℕ→BitVec (1 ∷ 0 ∷ 1 ∷ 5 ∷ 0 ∷ []) ≡ nothing
  _ = refl

max_stars_repo_name: felixwellen/adventOfCode

max_issues_repo_name: felixwellen/adventOfCode

max_forks_repo_name: felixwellen/adventOfCode


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

module Data.Nat.Square where

open import Data.Nat
open import Data.Nat.Properties

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)

_² : ℕ → ℕ
n ² = n * n

n^2≡n² : ∀ n → n ^ 2 ≡ n ²
n^2≡n² n = Eq.cong (n *_) (*-identityʳ n)

²-mono : _² Preserves _≤_ ⟶ _≤_
²-mono m≤n = *-mono-≤ m≤n m≤n

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Structure.Type.Quotient where

import      Lvl
open import Logic
open import Logic.Propositional
open import Structure.Function hiding (intro)
open import Structure.Function.Domain hiding (intro)
open import Structure.Relator.Equivalence hiding (intro)
open import Structure.Setoid hiding (intro)
import      Type
open import Type.Properties.Empty hiding (intro)

record Quotient {ℓ₁ ℓ₂} {T : TYPE(ℓ₁)} (_≅_ : T → T → Stmt{ℓ₂}) ⦃ equivalence : Equivalence(_≅_) ⦄ : Stmtω where
  field
    {ℓ} : Lvl.Level
    Type : TYPE(ℓ)
    {ℓₑ} : Lvl.Level
    ⦃ equiv ⦄ : Equiv{ℓₑ}(Type) -- TODO: Consider using Id instead of this because otherwise every type has a quotient by just using itself
    class : T → Type
    ⦃ intro-function ⦄ : Function ⦃ Structure.Setoid.intro(_≅_) ⦃ equivalence ⦄ ⦄ (class)
    ⦃ intro-bijective ⦄ : Bijective ⦃ Structure.Setoid.intro(_≅_) ⦃ equivalence ⦄ ⦄ (class)
    -- elim : Type → T -- TODO: Choice?
    -- inverseᵣ : ∀{q : Type} → (class(elim(q)) ≡ q)
    -- extensionality : ∀{a b : T} → (class(a) ≡ class(b)) ↔ (a ≅ b)

_/_ : ∀{ℓ₁ ℓ₂} → (T : TYPE(ℓ₁)) → (_≅_ : T → T → Stmt{ℓ₂}) → ⦃ e : Equivalence(_≅_) ⦄ → ⦃ q : Quotient(_≅_) ⦃ e ⦄ ⦄ → TYPE(Quotient.ℓ q)
(T / (_≅_)) ⦃ _ ⦄ ⦃ q ⦄ = Quotient.Type(q)

[_of_] : ∀{ℓ₁ ℓ₂}{T : TYPE(ℓ₁)} → T → (_≅_ : T → T → Stmt{ℓ₂}) → ⦃ e : Equivalence(_≅_) ⦄ → ⦃ q : Quotient(_≅_) ⦃ e ⦄ ⦄ → (T / (_≅_))
[ x of (_≅_) ] ⦃ _ ⦄ ⦃ q ⦄ = Quotient.class(q)(x)

{-
record Filterer (Filter : ∀{T : Type} → (T → Stmt) → Type) : Stmt where
  field
    intro : ∀{P} → (x : T) → ⦃ _ : P(x) ⦄ → Filter(P)
    obj   : ∀{P} → Filter(P) → T
    proof : ∀{P} → (X : Filter(P)) → P(obj(X))
    inverseₗ : ∀{P}{X : Filter(P)} → (intro(obj(X)) ⦃ proof(X) ⦄ ≡ X)
    inverseᵣ : ∀{P}{x}{px} → (obj(intro(x) ⦃ px ⦄) ≡ x)
    extensionality : ∀{T} → ⦃ _ : Equiv(T) ⦄ → ∀{Q : (T / (_≡_))}{a b : Q} → (intro(a) ≡ intro(b)) ↔ (a ≡ b)
-}


text:
module GUIgeneric.Prelude where

open import Data.Sum public hiding (map)
open import Data.List public
open import Data.Bool public
open import Data.String hiding (decSetoid) renaming (_++_ to _++Str_; _==_ to _==Str_; _≟_ to _≟Str_) public
open import Data.Unit hiding (_≟_; decSetoid; setoid) public
open import Data.Empty public
open import Data.Product hiding (map; zip) public
open import Data.Sum hiding (map) public
open import Data.Nat hiding (_≟_; _≤_; _≤?_) public
open import Data.Maybe.Base hiding (map) public
open import Function public
open import Relation.Binary.PropositionalEquality.Core public
open import Relation.Binary.PropositionalEquality hiding (setoid ; preorder ; decSetoid; [_]) public
open import Size public

open import Level renaming (_⊔_ to _⊔Level_; suc to sucLevel; zero to zeroLevel) public

open import Relation.Binary.Core using (Decidable) public
open import Relation.Nullary using (Dec) public
open import Relation.Nullary.Decidable using (⌊_⌋) public
--
-- ooAgda Imports
--

open import NativeIO public

open import StateSizedIO.Base hiding (IOInterfaceˢ; IOˢ; IOˢ'; IOˢ+; delayˢ; doˢ; fmapˢ; fmapˢ'; returnˢ) public

open import StateSizedIO.GUI.WxGraphicsLibLevel3 public renaming (createFrame to createWxFrame)
open import StateSizedIO.GUI.WxBindingsFFI  renaming (Frame to FFIFrame; Button to FFIButton; TextCtrl to FFITextCtrl) public

open import SizedIO.Base public

open import StateSizedIO.GUI.BaseStateDependent public
open import StateSizedIO.GUI.VariableList renaming (addVar to addVar'; addVar' to addVar) public

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module Dave.Extensionality where
    open import Dave.Equality

    postulate
        extensionality : ∀ {A B : Set} {f g : A → B}
            → (∀ (x : A) → f x ≡ g x)
            → f ≡ g

    postulate
        ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
            → (∀ (x : A) → f x ≡ g x)
            → f ≡ g


text:
module Cats.Category.Preorder where

open import Data.Unit using (⊤ ; tt)
open import Level
open import Relation.Binary as Rel
  using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_ ; Setoid)

open import Cats.Category
open import Cats.Category.Setoids using (Setoids ; ≈-intro)
open import Cats.Util.Conv
open import Cats.Util.Function as Fun using (_on_)

module _ (lc l≈ l≤ : Level) where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module Setoids = Category (Setoids lc l≈)

  Obj : Set (suc (lc ⊔ l≈ ⊔ l≤))
  Obj = Rel.Preorder lc l≈ l≤

  Universe : Obj → Setoid lc l≈
  Universe A = record
      { Carrier = Rel.Preorder.Carrier A
      ; _≈_ = Rel.Preorder._≈_ A
      ; isEquivalence = Rel.Preorder.isEquivalence A
      }

  record _⇒_ (A B : Obj) : Set (lc ⊔ l≈ ⊔ l≤) where
    private
      module A = Rel.Preorder A
      module B = Rel.Preorder B

    field
      arr : Universe A Setoids.⇒ Universe B
      monotone : ∀ {x y} → x A.∼ y → (arr ⃗) x B.∼ (arr ⃗) y

    open Cats.Category.Setoids._⇒_ arr public using (resp)

  open _⇒_ using (monotone ; resp)

  instance
    HasArrow-⇒ : ∀ A B → HasArrow (A ⇒ B) _ _ _
    HasArrow-⇒ A B = record { Cat = Setoids lc l≈ ; _⃗ = _⇒_.arr }

  id : ∀ {A} → A ⇒ A
  id = record { arr = Setoids.id ; monotone = Fun.id }

  _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
  g ∘ f = record
      { arr = g ⃗ Setoids.∘ f ⃗
      ; monotone = monotone g Fun.∘ monotone f
      }

  _≈_ : {A B : Obj} → Rel (A ⇒ B) (lc ⊔ l≈)
  _≈_ = Setoids._≈_ on _⃗

  instance Preorder : Category (suc (lc ⊔ l≈ ⊔ l≤)) (lc ⊔ l≈ ⊔ l≤) (lc ⊔ l≈)
  Preorder = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = Fun.on-isEquivalence _⃗ Setoids.equiv
      ; ∘-resp = Setoids.∘-resp
      ; id-r = Setoids.id-r
      ; id-l = Setoids.id-l
      ; assoc = λ { {f = f} {g} {h} → Setoids.assoc {f = f ⃗} {g ⃗} {h ⃗} }
      }

preorderAsCategory : ∀ {lc l≈ l≤} → Rel.Preorder lc l≈ l≤ → Category lc l≤ zero
preorderAsCategory P = record
    { Obj = P.Carrier
    ; _⇒_ = P._∼_
    ; _≈_ = λ _ _ → ⊤
    ; id = P.refl
    ; _∘_ = λ B≤C A≤B → P.trans A≤B B≤C
    ; equiv = record { refl = tt ; sym = λ _ → tt ; trans = λ _ _ → tt }
    ; ∘-resp = λ _ _ → tt
    ; id-r = tt
    ; id-l = tt
    ; assoc = tt
    }
  where
    module P = Rel.Preorder P

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module plfa.part1.Isomorphism where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)


text:
module Issue2447.Internal-error where

import Issue2447.M

{-# IMPOSSIBLE #-}


text:
{-# OPTIONS --without-K #-}
module sets.nat.ordering.lt where

open import sets.nat.ordering.lt.core public
open import sets.nat.ordering.lt.level public

max_stars_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Thesis.SIRelBigStep.DLangDerive where

open import Thesis.SIRelBigStep.DSyntax public

derive-const : ∀ {Δ σ} → (c : Const σ) → DSVal Δ σ
derive-const (lit n) = dconst (lit 0)

derive-dterm : ∀ {Δ σ} → (t : Term Δ σ) → DTerm Δ σ

derive-dsval : ∀ {Δ σ} → (t : SVal Δ σ) → DSVal Δ σ
derive-dsval (var x) = dvar x
derive-dsval (abs t) = dabs (derive-dterm t)
derive-dsval (cons sv1 sv2) = dcons (derive-dsval sv1) (derive-dsval sv2)
derive-dsval (const c) = derive-const c

derive-dterm (val x) = dval (derive-dsval x)
derive-dterm (primapp p sv) = dprimapp p sv (derive-dsval sv)
derive-dterm (app vs vt) = dapp (derive-dsval vs) vt (derive-dsval vt)
derive-dterm (lett s t) = dlett s (derive-dterm s) (derive-dterm t)

-- Nontrivial because of unification problems in pattern matching. I wanted to
-- use it to define ⊕ on closures purely on terms of the closure change.

-- Instead, I decided to use decidable equality on contexts: that's a lot of
-- tedious boilerplate, but not too hard, but the proof that validity and ⊕
-- agree becomes easier.
-- -- Define a DVar and be done?
-- underive-dvar :  ∀ {Δ σ} → Var (ΔΔ Δ) (Δτ σ) → Var Δ σ
-- underive-dvar {∅} ()
-- underive-dvar {τ • Δ} x = {!!}

--underive-dvar {σ • Δ} (that x) = that (underive-dvar x)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import HoTT
open import homotopy.elims.CofPushoutSection as CofPushoutSection

module homotopy.SmashIsCofiber {i j} (X : Ptd i) (Y : Ptd j) where

{- the proof that our smash matches the more classical definition as a cofiber -}

Smash-equiv-Cof : Smash X Y ≃ Cofiber (∨-to-× {X = X} {Y = Y})
Smash-equiv-Cof = equiv to from to-from from-to where
  module To = SmashRec {C = Cofiber (∨-to-× {X = X} {Y = Y})}
    (curry cfcod) cfbase cfbase
    (λ x → ! (cfglue (winl x)))
    (λ y → ! (cfglue (winr y)))
  to : Smash X Y → Cofiber (∨-to-× {X = X} {Y = Y})
  to = To.f

  module FromGlue = WedgeElim
    {P = λ x∨y → smin (pt X) (pt Y) == uncurry smin (∨-to-× {X = X} {Y = Y} x∨y)}
    (λ x → smgluel (pt X) ∙' ! (smgluel x))
    (λ y → smgluer (pt Y) ∙' ! (smgluer y))
    (↓-cst=app-in $
        ap2 _∙'_ (!-inv'-r (smgluel (pt X)))
          ( ap-∘ (uncurry smin) (∨-to-× {X = X} {Y = Y}) wglue
          ∙ ap (ap (uncurry smin)) (∨-to-×-glue-β {X = X} {Y = Y}))
      ∙ ! (!-inv'-r (smgluer (pt Y))))

  module From = CofiberRec {C = Smash X Y}
    (smin (pt X) (pt Y)) (uncurry smin)
    FromGlue.f

  from : Cofiber (∨-to-× {X = X} {Y = Y}) → Smash X Y
  from = From.f

  abstract
    from-to : ∀ x → from (to x) == x
    from-to = Smash-elim
      (λ _ _ → idp) (smgluel (pt X)) (smgluer (pt Y))
      (λ x → ↓-∘=idf-in' from to $
        ap from (ap to (smgluel x)) ∙' smgluel (pt X)
          =⟨ ap (_∙' smgluel (pt X)) $
              ap from (ap to (smgluel x))
                =⟨ ap (ap from) (To.smgluel-β x) ⟩
              ap from (! (cfglue (winl x)))
                =⟨ ap-! from (cfglue (winl x)) ⟩
              ! (ap from (cfglue (winl x)))
                =⟨ ap ! $ From.glue-β (winl x) ⟩
              ! (smgluel (pt X) ∙' ! (smgluel x))
                =⟨ !-∙' (smgluel (pt X)) (! (smgluel x)) ⟩
              ! (! (smgluel x)) ∙' ! (smgluel (pt X))
                =∎ ⟩
        (! (! (smgluel x)) ∙' ! (smgluel (pt X))) ∙' smgluel (pt X)
          =⟨ ∙'-assoc (! (! (smgluel x))) (! (smgluel (pt X))) (smgluel (pt X)) ⟩
        ! (! (smgluel x)) ∙' ! (smgluel (pt X)) ∙' smgluel (pt X)
          =⟨ ap2 _∙'_ (!-! (smgluel x)) (!-inv'-l (smgluel (pt X))) ⟩
        smgluel x
          =∎)
      (λ y → ↓-∘=idf-in' from to $
        ap from (ap to (smgluer y)) ∙' smgluer (pt Y)
          =⟨ ap (_∙' smgluer (pt Y)) $
              ap from (ap to (smgluer y))
                =⟨ ap (ap from) (To.smgluer-β y) ⟩
              ap from (! (cfglue (winr y)))
                =⟨ ap-! from (cfglue (winr y)) ⟩
              ! (ap from (cfglue (winr y)))
                =⟨ ap ! $ From.glue-β (winr y) ⟩
              ! (smgluer (pt Y) ∙' ! (smgluer y))
                =⟨ !-∙' (smgluer (pt Y)) (! (smgluer y)) ⟩
              ! (! (smgluer y)) ∙' ! (smgluer (pt Y))
                =∎ ⟩
        (! (! (smgluer y)) ∙' ! (smgluer (pt Y))) ∙' smgluer (pt Y)
          =⟨ ∙'-assoc (! (! (smgluer y))) (! (smgluer (pt Y))) (smgluer (pt Y)) ⟩
        ! (! (smgluer y)) ∙' ! (smgluer (pt Y)) ∙' smgluer (pt Y)
          =⟨ ap2 _∙'_ (!-! (smgluer y)) (!-inv'-l (smgluer (pt Y))) ⟩
        smgluer y
          =∎)

    to-from : ∀ x → to (from x) == x
    to-from = CofPushoutSection.elim
      (λ _ → unit) (λ _ → idp)
      (! (cfglue (winr (pt Y)))) (λ _ → idp)
      (λ x → ↓-∘=idf-in' to from $
        ap to (ap from (cfglue (winl x)))
          =⟨ ap (ap to) (From.glue-β (winl x)) ⟩
        ap to (FromGlue.f (winl x))
          =⟨ ap-∙' to (smgluel (pt X)) (! (smgluel x)) ⟩
        ap to (smgluel (pt X)) ∙' ap to (! (smgluel x))
          =⟨ ap2 _∙'_
              (To.smgluel-β (pt X))
              (ap-! to (smgluel x) ∙ ap ! (To.smgluel-β x) ∙ !-! (cfglue (winl x))) ⟩
        ! (cfglue (winl (pt X))) ∙' cfglue (winl x)
          =⟨ ap (λ p → ! p ∙' cfglue (winl x)) $
              ap (cfglue (winl (pt X)) ∙'_)
                ( ap (ap cfcod) (! ∨-to-×-glue-β)
                ∙ ∘-ap cfcod ∨-to-× wglue)
            ∙ ↓-cst=app-out (apd cfglue wglue)
          ⟩
        ! (cfglue (winr (pt Y))) ∙' cfglue (winl x)
          =⟨ ∙'=∙ (! (cfglue (winr (pt Y)))) (cfglue (winl x)) ⟩
        ! (cfglue (winr (pt Y))) ∙ cfglue (winl x)
          =∎)
      (λ y → ↓-∘=idf-in' to from $
        ap to (ap from (cfglue (winr y)))
          =⟨ ap (ap to) (From.glue-β (winr y)) ⟩
        ap to (FromGlue.f (winr y))
          =⟨ ap-∙' to (smgluer (pt Y)) (! (smgluer y)) ⟩
        ap to (smgluer (pt Y)) ∙' ap to (! (smgluer y))
          =⟨ ap2 _∙'_
              (To.smgluer-β (pt Y))
              (ap-! to (smgluer y) ∙ ap ! (To.smgluer-β y) ∙ !-! (cfglue (winr y))) ⟩
        ! (cfglue (winr (pt Y))) ∙' cfglue (winr y)
          =⟨ ∙'=∙ (! (cfglue (winr (pt Y)))) (cfglue (winr y)) ⟩
        ! (cfglue (winr (pt Y))) ∙ cfglue (winr y)
          =∎)

Smash-⊙equiv-Cof : ⊙Smash X Y ⊙≃ ⊙Cofiber (∨-⊙to-× {X = X} {Y = Y})
Smash-⊙equiv-Cof = ≃-to-⊙≃ Smash-equiv-Cof (! (cfglue (winl (pt X))))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- The abstract syntax is a set, and the semantics is propositional
------------------------------------------------------------------------

open import Atom

module Propositional (atoms : χ-atoms) where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (const)

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J

open import Cancellation  atoms
open import Chi           atoms
open import Deterministic atoms

open χ-atoms atoms

-- Exp has decidable equality.

mutual

  _≟_ : Decidable-equality Exp
  apply e₁₁ e₂₁ ≟ apply e₁₂ e₂₂ with e₁₁ ≟ e₁₂
  ... | no  e₁₁≢e₁₂ = no (e₁₁≢e₁₂ ∘ proj₁ ∘ cancel-apply)
  ... | yes e₁₁≡e₁₂ = ⊎-map (cong₂ apply e₁₁≡e₁₂)
                            (_∘ proj₂ ∘ cancel-apply)
                            (e₂₁ ≟ e₂₂)

  lambda x₁ e₁ ≟ lambda x₂ e₂ with x₁ V.≟ x₂
  ... | no  x₁≢x₂ = no (x₁≢x₂ ∘ proj₁ ∘ cancel-lambda)
  ... | yes x₁≡x₂ = ⊎-map (cong₂ lambda x₁≡x₂)
                          (_∘ proj₂ ∘ cancel-lambda)
                          (e₁ ≟ e₂)

  case e₁ bs₁ ≟ case e₂ bs₂ with e₁ ≟ e₂
  ... | no  e₁≢e₂ = no (e₁≢e₂ ∘ proj₁ ∘ cancel-case)
  ... | yes e₁≡e₂ = ⊎-map (cong₂ case e₁≡e₂)
                          (_∘ proj₂ ∘ cancel-case)
                          (bs₁ ≟-B⋆ bs₂)

  rec x₁ e₁ ≟ rec x₂ e₂ with x₁ V.≟ x₂
  ... | no  x₁≢x₂ = no (x₁≢x₂ ∘ proj₁ ∘ cancel-rec)
  ... | yes x₁≡x₂ = ⊎-map (cong₂ rec x₁≡x₂)
                          (_∘ proj₂ ∘ cancel-rec)
                          (e₁ ≟ e₂)

  var x₁ ≟ var x₂ = ⊎-map (cong var) (_∘ cancel-var) (x₁ V.≟ x₂)

  const c₁ es₁ ≟ const c₂ es₂ with c₁ C.≟ c₂
  ... | no  c₁≢c₂ = no (c₁≢c₂ ∘ proj₁ ∘ cancel-const)
  ... | yes c₁≡c₂ = ⊎-map (cong₂ const c₁≡c₂)
                          (_∘ proj₂ ∘ cancel-const)
                          (es₁ ≟-⋆ es₂)

  apply _ _  ≟ lambda _ _ = no (λ ())
  apply _ _  ≟ case _ _   = no (λ ())
  apply _ _  ≟ rec _ _    = no (λ ())
  apply _ _  ≟ var _      = no (λ ())
  apply _ _  ≟ const _ _  = no (λ ())
  lambda _ _ ≟ apply _ _  = no (λ ())
  lambda _ _ ≟ case _ _   = no (λ ())
  lambda _ _ ≟ rec _ _    = no (λ ())
  lambda _ _ ≟ var _      = no (λ ())
  lambda _ _ ≟ const _ _  = no (λ ())
  case _ _   ≟ apply _ _  = no (λ ())
  case _ _   ≟ lambda _ _ = no (λ ())
  case _ _   ≟ rec _ _    = no (λ ())
  case _ _   ≟ var _      = no (λ ())
  case _ _   ≟ const _ _  = no (λ ())
  rec _ _    ≟ apply _ _  = no (λ ())
  rec _ _    ≟ lambda _ _ = no (λ ())
  rec _ _    ≟ case _ _   = no (λ ())
  rec _ _    ≟ var _      = no (λ ())
  rec _ _    ≟ const _ _  = no (λ ())
  var _      ≟ apply _ _  = no (λ ())
  var _      ≟ lambda _ _ = no (λ ())
  var _      ≟ case _ _   = no (λ ())
  var _      ≟ rec _ _    = no (λ ())
  var _      ≟ const _ _  = no (λ ())
  const _ _  ≟ apply _ _  = no (λ ())
  const _ _  ≟ lambda _ _ = no (λ ())
  const _ _  ≟ case _ _   = no (λ ())
  const _ _  ≟ rec _ _    = no (λ ())
  const _ _  ≟ var _      = no (λ ())

  _≟-B_ : Decidable-equality Br
  branch c₁ xs₁ e₁ ≟-B branch c₂ xs₂ e₂ with c₁ C.≟ c₂
  ... | no  c₁≢c₂ = no (c₁≢c₂ ∘ proj₁ ∘ cancel-branch)
  ... | yes c₁≡c₂ with List.Dec._≟_ V._≟_ xs₁ xs₂
  ...   | no  xs₁≢xs₂ = no (xs₁≢xs₂ ∘ proj₁ ∘ proj₂ ∘ cancel-branch)
  ...   | yes xs₁≡xs₂ = ⊎-map (cong₂ (uncurry branch)
                                     (cong₂ _,_ c₁≡c₂ xs₁≡xs₂))
                              (_∘ proj₂ ∘ proj₂ ∘ cancel-branch)
                              (e₁ ≟ e₂)

  _≟-⋆_ : Decidable-equality (List Exp)
  []         ≟-⋆ []         = yes refl
  (e₁ ∷ es₁) ≟-⋆ (e₂ ∷ es₂) with e₁ ≟ e₂
  ... | no  e₁≢e₂ = no (e₁≢e₂ ∘ List.cancel-∷-head)
  ... | yes e₁≡e₂ = ⊎-map (cong₂ _∷_ e₁≡e₂)
                          (_∘ List.cancel-∷-tail)
                          (es₁ ≟-⋆ es₂)

  []      ≟-⋆ (_ ∷ _) = no (λ ())
  (_ ∷ _) ≟-⋆ []      = no (λ ())

  _≟-B⋆_ : Decidable-equality (List Br)
  []         ≟-B⋆ []         = yes refl
  (b₁ ∷ bs₁) ≟-B⋆ (b₂ ∷ bs₂) with b₁ ≟-B b₂
  ... | no  b₁≢b₂ = no (b₁≢b₂ ∘ List.cancel-∷-head)
  ... | yes b₁≡b₂ = ⊎-map (cong₂ _∷_ b₁≡b₂)
                          (_∘ List.cancel-∷-tail)
                          (bs₁ ≟-B⋆ bs₂)

  []      ≟-B⋆ (_ ∷ _) = no (λ ())
  (_ ∷ _) ≟-B⋆ []      = no (λ ())

-- Exp is a set.

Exp-set : Is-set Exp
Exp-set = decidable⇒set _≟_

-- An alternative definition of the semantics.

data Lookup′ (c : Const) : List Br → List Var → Exp → Type where
  here  : ∀ {c′ xs xs′ e e′ bs} →
          c ≡ c′ → xs ≡ xs′ → e ≡ e′ →
          Lookup′ c (branch c′ xs′ e′ ∷ bs) xs e
  there : ∀ {c′ xs′ e′ bs xs e} →
          c ≢ c′ → Lookup′ c bs xs e →
          Lookup′ c (branch c′ xs′ e′ ∷ bs) xs e

infixr 5 _∷_
infix  4 _[_←_]↦′_

data _[_←_]↦′_ (e : Exp) : List Var → List Exp → Exp → Type where
  []  : ∀ {e′} → e ≡ e′ → e [ [] ← [] ]↦′ e′
  _∷_ : ∀ {x xs e′ es′ e″ e‴} →
        e‴ ≡ e″ [ x ← e′ ] → e [ xs ← es′ ]↦′ e″ →
        e [ x ∷ xs ← e′ ∷ es′ ]↦′ e‴

infix 4 _⇓′_ _⇓⋆′_

mutual

  data _⇓′_ : Exp → Exp → Type where
    apply  : ∀ {e₁ e₂ x e v₂ v} →
             e₁ ⇓′ lambda x e → e₂ ⇓′ v₂ → e [ x ← v₂ ] ⇓′ v →
             apply e₁ e₂ ⇓′ v
    case   : ∀ {e bs c es xs e′ e″ v} →
             e ⇓′ const c es → Lookup′ c bs xs e′ →
             e′ [ xs ← es ]↦′ e″ → e″ ⇓′ v →
             case e bs ⇓′ v
    rec    : ∀ {x e v} → e [ x ← rec x e ] ⇓′ v → rec x e ⇓′ v
    lambda : ∀ {x x′ e e′} →
             x ≡ x′ → e ≡ e′ → lambda x e ⇓′ lambda x′ e′
    const  : ∀ {c c′ es vs} →
             c ≡ c′ → es ⇓⋆′ vs → const c es ⇓′ const c′ vs

  data _⇓⋆′_ : List Exp → List Exp → Type where
    []  : [] ⇓⋆′ []
    _∷_ : ∀ {e es v vs} → e ⇓′ v → es ⇓⋆′ vs → e ∷ es ⇓⋆′ v ∷ vs

-- The alternative definition is isomorphic to the other one.

Lookup↔Lookup′ : ∀ {c bs xs e} → Lookup c bs xs e ↔ Lookup′ c bs xs e
Lookup↔Lookup′ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : ∀ {c bs xs e} → Lookup c bs xs e → Lookup′ c bs xs e
  to here          = here refl refl refl
  to (there p₁ p₂) = there p₁ (to p₂)

  from : ∀ {c bs xs e} → Lookup′ c bs xs e → Lookup c bs xs e
  from (here refl refl refl) = here
  from (there p₁ p₂)         = there p₁ (from p₂)

  from∘to : ∀ {c bs xs e} (p : Lookup c bs xs e) → from (to p) ≡ p
  from∘to here          = refl
  from∘to (there p₁ p₂) rewrite from∘to p₂ = refl

  to∘from : ∀ {c bs xs e} (p : Lookup′ c bs xs e) → to (from p) ≡ p
  to∘from (here refl refl refl) = refl
  to∘from (there p₁ p₂)         rewrite to∘from p₂ = refl

↦↔↦′ : ∀ {e xs es e′} → e [ xs ← es ]↦ e′ ↔ e [ xs ← es ]↦′ e′
↦↔↦′ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : ∀ {e xs es e′} → e [ xs ← es ]↦ e′ → e [ xs ← es ]↦′ e′
  to []    = [] refl
  to (∷ p) = refl ∷ to p

  from : ∀ {e xs es e′} → e [ xs ← es ]↦′ e′ → e [ xs ← es ]↦ e′
  from ([] refl)  = []
  from (refl ∷ p) = ∷ from p

  from∘to : ∀ {e xs es e′} (p : e [ xs ← es ]↦ e′) → from (to p) ≡ p
  from∘to []    = refl
  from∘to (∷ p) rewrite from∘to p = refl

  to∘from : ∀ {e xs es e′} (p : e [ xs ← es ]↦′ e′) → to (from p) ≡ p
  to∘from ([] refl)  = refl
  to∘from (refl ∷ p) rewrite to∘from p = refl

⇓↔⇓′ : ∀ {e v} → e ⇓ v ↔ e ⇓′ v
⇓↔⇓′ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  mutual

    to : ∀ {e v} → e ⇓ v → e ⇓′ v
    to (apply p q r)  = apply (to p) (to q) (to r)
    to (case p q r s) = case (to p) (_↔_.to Lookup↔Lookup′ q)
                             (_↔_.to ↦↔↦′ r) (to s)
    to (rec p)        = rec (to p)
    to lambda         = lambda refl refl
    to (const ps)     = const refl (to⋆ ps)

    to⋆ : ∀ {e v} → e ⇓⋆ v → e ⇓⋆′ v
    to⋆ []       = []
    to⋆ (p ∷ ps) = to p ∷ to⋆ ps

  mutual

    from : ∀ {e v} → e ⇓′ v → e ⇓ v
    from (apply p q r)      = apply (from p) (from q) (from r)
    from (case p q r s)     = case (from p) (_↔_.from Lookup↔Lookup′ q)
                                   (_↔_.from ↦↔↦′ r) (from s)
    from (rec p)            = rec (from p)
    from (lambda refl refl) = lambda
    from (const refl ps)    = const (from⋆ ps)

    from⋆ : ∀ {e v} → e ⇓⋆′ v → e ⇓⋆ v
    from⋆ []       = []
    from⋆ (p ∷ ps) = from p ∷ from⋆ ps

  mutual

    from∘to : ∀ {e v} (p : e ⇓ v) → from (to p) ≡ p
    from∘to (apply p q r)  rewrite from∘to p | from∘to q | from∘to r
                           = refl
    from∘to (case p q r s) rewrite from∘to p
                                 | _↔_.left-inverse-of Lookup↔Lookup′ q
                                 | _↔_.left-inverse-of ↦↔↦′ r
                                 | from∘to s = refl
    from∘to (rec p)        rewrite from∘to p = refl
    from∘to lambda         = refl
    from∘to (const ps)     rewrite from⋆∘to⋆ ps = refl

    from⋆∘to⋆ : ∀ {e v} (ps : e ⇓⋆ v) → from⋆ (to⋆ ps) ≡ ps
    from⋆∘to⋆ []       = refl
    from⋆∘to⋆ (p ∷ ps) rewrite from∘to p | from⋆∘to⋆ ps = refl

  mutual

    to∘from : ∀ {e v} (p : e ⇓′ v) → to (from p) ≡ p
    to∘from (apply p q r)      rewrite to∘from p | to∘from q | to∘from r
                               = refl
    to∘from (case p q r s)     rewrite to∘from p
                                     | _↔_.right-inverse-of
                                         Lookup↔Lookup′ q
                                     | _↔_.right-inverse-of ↦↔↦′ r
                                     | to∘from s = refl
    to∘from (rec p)            rewrite to∘from p = refl
    to∘from (lambda refl refl) = refl
    to∘from (const refl ps)    rewrite to⋆∘from⋆ ps = refl

    to⋆∘from⋆ : ∀ {e v} (ps : e ⇓⋆′ v) → to⋆ (from⋆ ps) ≡ ps
    to⋆∘from⋆ []       = refl
    to⋆∘from⋆ (p ∷ ps) rewrite to∘from p | to⋆∘from⋆ ps = refl

-- The alternative semantics is deterministic.

Lookup′-deterministic :
  ∀ {c bs xs₁ xs₂ e₁ e₂} →
  Lookup′ c bs xs₁ e₁ → Lookup′ c bs xs₂ e₂ →
  xs₁ ≡ xs₂ × e₁ ≡ e₂
Lookup′-deterministic p q =
  Lookup-deterministic
    (_↔_.from Lookup↔Lookup′ p) (_↔_.from Lookup↔Lookup′ q) refl

↦′-deterministic :
  ∀ {e xs es e₁ e₂} →
  e [ xs ← es ]↦′ e₁ → e [ xs ← es ]↦′ e₂ → e₁ ≡ e₂
↦′-deterministic p q =
  ↦-deterministic (_↔_.from ↦↔↦′ p) (_↔_.from ↦↔↦′ q)

⇓′-deterministic : ∀ {e v₁ v₂} → e ⇓′ v₁ → e ⇓′ v₂ → v₁ ≡ v₂
⇓′-deterministic p q =
  ⇓-deterministic (_↔_.from ⇓↔⇓′ p) (_↔_.from ⇓↔⇓′ q)

-- The alternative semantics is propositional.

Lookup′-propositional :
  ∀ {c bs xs e} → Is-proposition (Lookup′ c bs xs e)
Lookup′-propositional (here p₁ p₂ p₃) (here q₁ q₂ q₃)
    rewrite C.Name-set p₁ q₁
          | decidable⇒set (List.Dec._≟_ V._≟_) p₂ q₂
          | Exp-set p₃ q₃
    = refl
Lookup′-propositional (there p₁ p₂) (there q₁ q₂)
  rewrite ¬-propositional ext p₁ q₁
        | Lookup′-propositional p₂ q₂
  = refl

Lookup′-propositional (here c≡c′ _ _) (there c≢c′ _) =
  ⊥-elim (c≢c′ c≡c′)
Lookup′-propositional (there c≢c′ _) (here c≡c′ _ _) =
  ⊥-elim (c≢c′ c≡c′)

↦′-propositional :
  ∀ {e xs es e′} → Is-proposition (e [ xs ← es ]↦′ e′)
↦′-propositional ([] p)    ([] q)    rewrite Exp-set p q = refl
↦′-propositional (p₁ ∷ p₂) (q₁ ∷ q₂)
  with ↦′-deterministic p₂ q₂
... | refl rewrite Exp-set p₁ q₁
                 | ↦′-propositional p₂ q₂
  = refl

mutual

  ⇓′-propositional : ∀ {e v} → Is-proposition (e ⇓′ v)
  ⇓′-propositional (apply p₁ p₂ p₃) (apply q₁ q₂ q₃)
    with ⇓′-deterministic p₁ q₁
  ... | refl rewrite ⇓′-propositional p₁ q₁
                with ⇓′-deterministic p₂ q₂
  ... | refl rewrite ⇓′-propositional p₂ q₂
                   | ⇓′-propositional p₃ q₃
             = refl
  ⇓′-propositional (case p₁ p₂ p₃ p₄) (case q₁ q₂ q₃ q₄)
    with ⇓′-deterministic p₁ q₁
  ... | refl rewrite ⇓′-propositional p₁ q₁
                with Lookup′-deterministic p₂ q₂
  ... | refl , refl rewrite Lookup′-propositional p₂ q₂
                       with ↦′-deterministic p₃ q₃
  ... | refl rewrite ↦′-propositional p₃ q₃
                   | ⇓′-propositional p₄ q₄
    = refl
  ⇓′-propositional (rec p) (rec q)
    rewrite ⇓′-propositional p q
    = refl
  ⇓′-propositional (lambda p₁ p₂) (lambda q₁ q₂)
    rewrite V.Name-set p₁ q₁
          | Exp-set p₂ q₂
          = refl
  ⇓′-propositional (const p ps) (const q qs)
    rewrite C.Name-set p q
          | ⇓⋆′-propositional ps qs
    = refl

  ⇓⋆′-propositional : ∀ {es vs} → Is-proposition (es ⇓⋆′ vs)
  ⇓⋆′-propositional []       []       = refl
  ⇓⋆′-propositional (p ∷ ps) (q ∷ qs)
    rewrite ⇓′-propositional p q
          | ⇓⋆′-propositional ps qs
    = refl

-- The semantics is propositional.

⇓-propositional : ∀ {e v} → Is-proposition (e ⇓ v)
⇓-propositional {e} {v} =  $⟨ ⇓′-propositional ⟩
  Is-proposition (e ⇓′ v)  ↝⟨ H-level.respects-surjection (_↔_.surjection $ inverse ⇓↔⇓′) 1 ⟩□
  Is-proposition (e ⇓ v)   □

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi