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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Weakening {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening as T hiding (wk; wkEq; wkTerm; wkEqTerm)
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Weakening of neutrals in WHNF

wkTermNe : ∀ {ρ Γ Δ k A} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
         → Γ ⊩neNf k ∷ A → Δ ⊩neNf U.wk ρ k ∷ U.wk ρ A
wkTermNe {ρ} [ρ] ⊢Δ (neNfₜ neK ⊢k k≡k) =
  neNfₜ (wkNeutral ρ neK) (T.wkTerm [ρ] ⊢Δ ⊢k) (~-wk [ρ] ⊢Δ k≡k)

wkEqTermNe : ∀ {ρ Γ Δ k k′ A} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
           → Γ ⊩neNf k ≡ k′ ∷ A → Δ ⊩neNf U.wk ρ k ≡ U.wk ρ k′ ∷ U.wk ρ A
wkEqTermNe {ρ} [ρ] ⊢Δ (neNfₜ₌ neK neM k≡m) =
  neNfₜ₌ (wkNeutral ρ neK) (wkNeutral ρ neM) (~-wk [ρ] ⊢Δ k≡m)

-- Weakening of reducible natural numbers

mutual
  wkTermℕ : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
          → _⊩ℕ_∷ℕ Γ n → _⊩ℕ_∷ℕ Δ (U.wk ρ n)
  wkTermℕ {ρ} [ρ] ⊢Δ (ℕₜ n d n≡n prop) =
    ℕₜ (U.wk ρ n) (wkRed:*:Term [ρ] ⊢Δ d)
       (≅ₜ-wk [ρ] ⊢Δ n≡n)
       (wkNatural-prop [ρ] ⊢Δ prop)

  wkNatural-prop : ∀ {ρ Γ Δ n} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
                 → Natural-prop Γ n
                 → Natural-prop Δ (U.wk ρ n)
  wkNatural-prop ρ ⊢Δ (sucᵣ n) = sucᵣ (wkTermℕ ρ ⊢Δ n)
  wkNatural-prop ρ ⊢Δ zeroᵣ = zeroᵣ
  wkNatural-prop ρ ⊢Δ (ne nf) = ne (wkTermNe ρ ⊢Δ nf)

mutual
  wkEqTermℕ : ∀ {ρ Γ Δ t u} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
            → _⊩ℕ_≡_∷ℕ Γ t u
            → _⊩ℕ_≡_∷ℕ Δ (U.wk ρ t) (U.wk ρ u)
  wkEqTermℕ {ρ} [ρ] ⊢Δ (ℕₜ₌ k k′ d d′ t≡u prop) =
    ℕₜ₌ (U.wk ρ k) (U.wk ρ k′) (wkRed:*:Term [ρ] ⊢Δ d)
        (wkRed:*:Term [ρ] ⊢Δ d′) (≅ₜ-wk [ρ] ⊢Δ t≡u)
        (wk[Natural]-prop [ρ] ⊢Δ prop)

  wk[Natural]-prop : ∀ {ρ Γ Δ n n′} → ρ ∷ Δ ⊆ Γ → (⊢Δ : ⊢ Δ)
                   → [Natural]-prop Γ n n′
                   → [Natural]-prop Δ (U.wk ρ n) (U.wk ρ n′)
  wk[Natural]-prop ρ ⊢Δ (sucᵣ [n≡n′]) = sucᵣ (wkEqTermℕ ρ ⊢Δ [n≡n′])
  wk[Natural]-prop ρ ⊢Δ zeroᵣ = zeroᵣ
  wk[Natural]-prop ρ ⊢Δ (ne x) = ne (wkEqTermNe ρ ⊢Δ x)

-- Weakening of the logical relation

wk : ∀ {ρ Γ Δ A l} → ρ ∷ Δ ⊆ Γ → ⊢ Δ → Γ ⊩⟨ l ⟩ A → Δ ⊩⟨ l ⟩ U.wk ρ A
wk ρ ⊢Δ (Uᵣ′ l′ l< ⊢Γ) = Uᵣ′ l′ l< ⊢Δ
wk ρ ⊢Δ (ℕᵣ D) = ℕᵣ (wkRed:*: ρ ⊢Δ D)
wk {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) =
  ne′ (U.wk ρ K) (wkRed:*: [ρ] ⊢Δ D) (wkNeutral ρ neK) (~-wk [ρ] ⊢Δ K≡K)
wk {ρ} {Γ} {Δ} {A} {l} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢ρF = T.wk [ρ] ⊢Δ ⊢F
      [F]′ : ∀ {ρ ρ′ E} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
           → E ⊩⟨ l ⟩ U.wk ρ (U.wk ρ′ F)
      [F]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E = irrelevance′
                              (PE.sym (wk-comp ρ ρ′ F))
                              ([F] ([ρ] •ₜ [ρ′]) ⊢E)
      [a]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ a ∷ U.wk (ρ • ρ′) F / [F] ([ρ] •ₜ [ρ′]) ⊢E
      [a]′ {ρ} {ρ′} [ρ] [ρ′] ⊢E [a] = irrelevanceTerm′ (wk-comp ρ ρ′ F)
                                          ([F]′ [ρ] [ρ′] ⊢E) ([F] ([ρ] •ₜ [ρ′]) ⊢E) [a]
      [G]′ : ∀ {ρ ρ′ E a} ([ρ] : ρ ∷ E ⊆ Δ) ([ρ′] : ρ′ ∷ Δ ⊆ Γ) (⊢E : ⊢ E)
             ([a] : E ⊩⟨ l ⟩ a ∷ U.wk ρ (U.wk ρ′ F) / [F]′ [ρ] [ρ′] ⊢E)
           → E ⊩⟨ l ⟩ U.wk (lift (ρ • ρ′)) G [ a ]
      [G]′ η η′ ⊢E [a] = [G] (η •ₜ η′) ⊢E ([a]′ η η′ ⊢E [a])
  in  Πᵣ′ (U.wk ρ F) (U.wk (lift ρ) G) (T.wkRed:*: [ρ] ⊢Δ D) ⊢ρF
           (T.wk (lift [ρ]) (⊢Δ ∙ ⊢ρF) ⊢G)
           (≅-wk [ρ] ⊢Δ A≡A)
           (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] → irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                        ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
           (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
              let [a≡b]′ = irrelevanceEqTerm′ (wk-comp ρ₁ ρ F)
                                              ([F]′ [ρ₁] [ρ] ⊢Δ₁)
                                              ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                              [a≡b]
              in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                                  (wk-comp-subst ρ₁ ρ G)
                                  ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                  (irrelevance′
                                            (wk-comp-subst ρ₁ ρ G)
                                            ([G]′ [ρ₁] [ρ] ⊢Δ₁ [a]))
                                  (G-ext ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [a])
                                         ([a]′ [ρ₁] [ρ] ⊢Δ₁ [b])
                                         [a≡b]′))
wk ρ ⊢Δ (emb′ 0<1 x) = emb′ 0<1 (wk ρ ⊢Δ x)

wkEq : ∀ {ρ Γ Δ A B l} → ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
       ([A] : Γ ⊩⟨ l ⟩ A)
     → Γ ⊩⟨ l ⟩ A ≡ B / [A]
     → Δ ⊩⟨ l ⟩ U.wk ρ A ≡ U.wk ρ B / wk [ρ] ⊢Δ [A]
wkEq ρ ⊢Δ (Uᵣ′ _ _ _) (U₌ PE.refl) = (U₌ PE.refl)
wkEq ρ ⊢Δ (ℕᵣ D) (ιx (ℕ₌ A≡B)) = ιx (ℕ₌ (wkRed* ρ ⊢Δ A≡B))
wkEq {ρ} [ρ] ⊢Δ (ne′ _ _ _ _) (ιx (ne₌ M D′ neM K≡M)) =
  ιx (ne₌ (U.wk ρ M) (wkRed:*: [ρ] ⊢Δ D′)
      (wkNeutral ρ neM) (~-wk [ρ] ⊢Δ K≡M))
wkEq {ρ} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  Π₌ (U.wk ρ F′) (U.wk (lift ρ) G′) (T.wkRed* [ρ] ⊢Δ D′) (≅-wk [ρ] ⊢Δ A≡B)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ → irrelevanceEq″ (PE.sym (wk-comp ρ₁ ρ F))
                                 (PE.sym (wk-comp ρ₁ ρ F′))
                                 ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁)
                                 (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                               ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                 ([F≡F′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F)
                                    (irrelevance′ (PE.sym (wk-comp ρ₁ ρ F))
                                                  ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁))
                                    ([F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁) [a]
        in  irrelevanceEq″ (wk-comp-subst ρ₁ ρ G)
                            (wk-comp-subst ρ₁ ρ G′)
                            ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′)
                            (irrelevance′ (wk-comp-subst ρ₁ ρ G)
                                          ([G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
                            ([G≡G′] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEq ρ ⊢Δ (emb′ 0<1 x) (ιx A≡B) = ιx (wkEq ρ ⊢Δ x A≡B)

wkTerm : ∀ {ρ Γ Δ A t l} ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
         ([A] : Γ ⊩⟨ l ⟩ A)
       → Γ ⊩⟨ l ⟩ t ∷ A / [A]
       → Δ ⊩⟨ l ⟩ U.wk ρ t ∷ U.wk ρ A / wk [ρ] ⊢Δ [A]
wkTerm {ρ} [ρ] ⊢Δ (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ A d typeA A≡A [t]) =
  Uₜ (U.wk ρ A) (wkRed:*:Term [ρ] ⊢Δ d)
     (wkType ρ typeA) (≅ₜ-wk [ρ] ⊢Δ A≡A) (wk [ρ] ⊢Δ [t])
wkTerm ρ ⊢Δ (ℕᵣ D) (ιx [t]) = ιx (wkTermℕ ρ ⊢Δ [t])
--
wkTerm {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) (ιx (neₜ k d nf)) =
  ιx (neₜ (U.wk ρ k) (wkRed:*:Term [ρ] ⊢Δ d) (wkTermNe [ρ] ⊢Δ nf))
wkTerm {ρ} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ (U.wk ρ f) (wkRed:*:Term [ρ] ⊢Δ d) (wkFunction ρ funcF)
     (≅ₜ-wk [ρ] ⊢Δ f≡f)
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] [b] [a≡b] →
        let F-compEq = wk-comp ρ₁ ρ F
            G-compEq = wk-comp-subst ρ₁ ρ G
            [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
            [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
            [a]′ = irrelevanceTerm′ F-compEq [F]₂ [F]₁ [a]
            [b]′ = irrelevanceTerm′ F-compEq [F]₂ [F]₁ [b]
            [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
            [G]₂ = irrelevance′ G-compEq [G]₁
            [a≡b]′ = irrelevanceEqTerm′ F-compEq [F]₂ [F]₁ [a≡b]
        in  irrelevanceEqTerm″ (PE.cong (λ x → x ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                (PE.cong (λ x → x ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                G-compEq
                                [G]₁ [G]₂
                                ([f] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′ [b]′ [a≡b]′))
     (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
        let [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
            [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
            [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) [F]₂ [F]₁ [a]
            [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
            [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
        in  irrelevanceTerm″ (wk-comp-subst ρ₁ ρ G)
                              (PE.cong (λ x → x ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                              [G]₁ [G]₂ ([f]₁ ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkTerm ρ ⊢Δ (emb′ 0<1 x) (ιx t) = ιx (wkTerm ρ ⊢Δ x t)

wkEqTerm : ∀ {ρ Γ Δ A t u l} ([ρ] : ρ ∷ Δ ⊆ Γ) (⊢Δ : ⊢ Δ)
           ([A] : Γ ⊩⟨ l ⟩ A)
         → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
         → Δ ⊩⟨ l ⟩ U.wk ρ t ≡ U.wk ρ u ∷ U.wk ρ A / wk [ρ] ⊢Δ [A]
wkEqTerm {ρ} [ρ] ⊢Δ (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ₌ A B d d′ typeA typeB A≡B [t] [u] [t≡u]) =
  Uₜ₌ (U.wk ρ A) (U.wk ρ B) (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
      (wkType ρ typeA) (wkType ρ typeB) (≅ₜ-wk [ρ] ⊢Δ A≡B)
      (wk [ρ] ⊢Δ [t]) (wk [ρ] ⊢Δ [u]) (wkEq [ρ] ⊢Δ [t] [t≡u])
wkEqTerm ρ ⊢Δ (ℕᵣ D) (ιx [t≡u]) = ιx (wkEqTermℕ ρ ⊢Δ [t≡u])
wkEqTerm {ρ} [ρ] ⊢Δ (ne′ K D neK K≡K) (ιx (neₜ₌ k m d d′ nf)) =
  ιx (neₜ₌ (U.wk ρ k) (U.wk ρ m)
       (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
       (wkEqTermNe [ρ] ⊢Δ nf))
wkEqTerm {ρ} [ρ] ⊢Δ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                    (Πₜ₌ f g d d′ funcF funcG f≡g [t] [u] [f≡g]) =
  let [A] = Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext
  in  Πₜ₌ (U.wk ρ f) (U.wk ρ g) (wkRed:*:Term [ρ] ⊢Δ d) (wkRed:*:Term [ρ] ⊢Δ d′)
          (wkFunction ρ funcF) (wkFunction ρ funcG)
          (≅ₜ-wk [ρ] ⊢Δ f≡g) (wkTerm [ρ] ⊢Δ [A] [t]) (wkTerm [ρ] ⊢Δ [A] [u])
          (λ {ρ₁} [ρ₁] ⊢Δ₁ [a] →
             let [F]₁ = [F] ([ρ₁] •ₜ [ρ]) ⊢Δ₁
                 [F]₂ = irrelevance′ (PE.sym (wk-comp ρ₁ ρ F)) [F]₁
                 [a]′ = irrelevanceTerm′ (wk-comp ρ₁ ρ F) [F]₂ [F]₁ [a]
                 [G]₁ = [G] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′
                 [G]₂ = irrelevance′ (wk-comp-subst ρ₁ ρ G) [G]₁
             in  irrelevanceEqTerm″ (PE.cong (λ y → y ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                     (PE.cong (λ y → y ∘ _) (PE.sym (wk-comp ρ₁ ρ _)))
                                     (wk-comp-subst ρ₁ ρ G)
                                     [G]₁ [G]₂
                                     ([f≡g] ([ρ₁] •ₜ [ρ]) ⊢Δ₁ [a]′))
wkEqTerm ρ ⊢Δ (emb′ 0<1 x) (ιx t≡u) = ιx (wkEqTerm ρ ⊢Δ x t≡u)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --copatterns #-}

open import Common.Prelude
open import Common.Product

postulate
  A : Set
  B : A → Set
  f : ∀ a → B a

bla : ∃ B
{-# NON_TERMINATING #-}
proj₁ bla = proj₁ bla
proj₂ bla = f (proj₁ bla)

T : Bool → Set
T true  = Bool
T false = Bool

test : (∀ b → T b) → ∃ T
{-# NON_TERMINATING #-}
proj₁ (test f) = proj₁ (test f)
proj₂ (test f) = f (proj₁ (test f))

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Common.Sum where

open import Common.Level

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module Numbers.Modulo.Definition where

record ℤn (n : ℕ) .(pr : 0 <N n) : Set where
  field
    x : ℕ
    .xLess : x <N n

equalityZn : {n : ℕ} .{pr : 0 <N n} → {a b : ℤn n pr} → (ℤn.x a ≡ ℤn.x b) → a ≡ b
equalityZn {a = record { x = a ; xLess = aLess }} {record { x = .a ; xLess = bLess }} refl = refl


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Monoid where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.Pointed
open import Cubical.Structures.NAryOp

private
  variable
    ℓ : Level

-- Monoids
raw-monoid-structure : Type ℓ → Type ℓ
raw-monoid-structure X = X × (X → X → X)

-- If we ignore the axioms we get a "raw" monoid
raw-monoid-is-SNS : SNS {ℓ} raw-monoid-structure _
raw-monoid-is-SNS = join-SNS pointed-iso pointed-is-SNS (nAryFunIso 2) (nAryFunSNS 2)

-- Monoid axioms
monoid-axioms : (X : Type ℓ) → raw-monoid-structure X → Type ℓ
monoid-axioms X (e , _·_ ) = isSet X
                           × ((x y z : X) → x · (y · z) ≡ (x · y) · z)
                           × ((x : X) → x · e ≡ x)
                           × ((x : X) → e · x ≡ x)

monoid-structure : Type ℓ → Type ℓ
monoid-structure = add-to-structure raw-monoid-structure monoid-axioms

Monoid : Type (ℓ-suc ℓ)
Monoid {ℓ} = TypeWithStr ℓ monoid-structure

-- Monoid extractors

⟨_⟩ : Monoid {ℓ} → Type ℓ
⟨ G , _ ⟩ = G

monoid-id : (M : Monoid {ℓ}) → ⟨ M ⟩
monoid-id (_ , (e , _) , _) = e

monoid-operation : (M : Monoid {ℓ}) → ⟨ M ⟩ → ⟨ M ⟩ → ⟨ M ⟩
monoid-operation (_ , (_ , f) , _) = f

-- Monoid syntax with explicit monoid

module monoid-syntax where
  id : (M : Monoid {ℓ}) → ⟨ M ⟩
  id = monoid-id

  monoid-operation-syntax : (M : Monoid {ℓ}) → ⟨ M ⟩ → ⟨ M ⟩ → ⟨ M ⟩
  monoid-operation-syntax = monoid-operation

  infixr 18 monoid-operation-syntax
  syntax monoid-operation-syntax M x y = x ·⟨ M ⟩ y

open monoid-syntax

-- More Monoid extractors

monoid-is-set : (M : Monoid {ℓ}) → isSet (⟨ M ⟩)
monoid-is-set (_ , _ , P , _) = P

monoid-assoc : (M : Monoid {ℓ})
             → (x y z : ⟨ M ⟩) → x ·⟨ M ⟩ (y ·⟨ M ⟩ z) ≡ (x ·⟨ M ⟩ y) ·⟨ M ⟩ z
monoid-assoc (_ , _ , _ , P , _) = P

monoid-rid : (M : Monoid {ℓ})
           → (x : ⟨ M ⟩) → x ·⟨ M ⟩ (id M) ≡ x
monoid-rid (_ , _ , _ , _ , P , _) = P

monoid-lid : (M : Monoid {ℓ})
           → (x : ⟨ M ⟩) → (id M) ·⟨ M ⟩ x ≡ x
monoid-lid (_ , _ , _ , _ , _ , P) = P

-- Monoid equivalence
monoid-iso : StrIso monoid-structure ℓ
monoid-iso = add-to-iso (join-iso pointed-iso (nAryFunIso 2)) monoid-axioms

-- We have to show that the monoid axioms are indeed propositions
monoid-axioms-are-Props : (X : Type ℓ) (s : raw-monoid-structure X) → isProp (monoid-axioms X s)
monoid-axioms-are-Props X (e , _·_) s = β s
   where
   α = s .fst
   β = isProp× isPropIsSet
      (isProp× (isPropΠ3 (λ x y z → α (x · (y · z)) ((x · y) · z)))
      (isProp× (isPropΠ (λ x → α (x · e) x)) (isPropΠ (λ x → α (e · x) x))))

monoid-is-SNS : SNS {ℓ} monoid-structure monoid-iso
monoid-is-SNS = add-axioms-SNS _ monoid-axioms-are-Props raw-monoid-is-SNS

MonoidPath : (M N : Monoid {ℓ}) → (M ≃[ monoid-iso ] N) ≃ (M ≡ N)
MonoidPath = SIP monoid-is-SNS

-- Added for its use in groups
-- If there exists a inverse of an element it is unique

inv-lemma : (M : Monoid {ℓ})
          → (x y z : ⟨ M ⟩)
          → y ·⟨ M ⟩ x ≡ id M
          → x ·⟨ M ⟩ z ≡ id M
          → y ≡ z
inv-lemma M x y z left-inverse right-inverse =
  y                     ≡⟨ sym (monoid-rid M y) ⟩
  y ·⟨ M ⟩ id M         ≡⟨ cong (λ - → y ·⟨ M ⟩ -) (sym right-inverse) ⟩
  y ·⟨ M ⟩ (x ·⟨ M ⟩ z) ≡⟨ monoid-assoc M y x z ⟩
  (y ·⟨ M ⟩ x) ·⟨ M ⟩ z ≡⟨ cong (λ - → - ·⟨ M ⟩ z) left-inverse ⟩
  id M ·⟨ M ⟩ z         ≡⟨ monoid-lid M z ⟩
  z ∎

-- Monoid ·syntax

module monoid-·syntax (M : Monoid {ℓ}) where

  infixr 18 _·_

  _·_ : ⟨ M ⟩ → ⟨ M ⟩ → ⟨ M ⟩
  _·_ = monoid-operation M

  ₁ : ⟨ M ⟩
  ₁ = monoid-id M


text:
-- TODO
-- Common syntax.

module BasicT.Syntax.Common where

open import Common.Context public

-- Types, or propositions.

infixl 9 _∧_
infixr 7 _▻_
data Ty : Set where
  α_   : Atom → Ty
  _▻_  : Ty → Ty → Ty
  _∧_  : Ty → Ty → Ty
  ⊤   : Ty
  BOOL : Ty
  NAT  : Ty

-- Additional useful types.

infix 7 _▻◅_
_▻◅_ : Ty → Ty → Ty
A ▻◅ B = (A ▻ B) ∧ (B ▻ A)

infixr 7 _▻⋯▻_
_▻⋯▻_ : Cx Ty → Ty → Ty
∅       ▻⋯▻ B = B
(Ξ , A) ▻⋯▻ B = Ξ ▻⋯▻ (A ▻ B)

infixr 7 _▻⋯▻⋆_
_▻⋯▻⋆_ : Cx Ty → Cx Ty → Ty
Γ ▻⋯▻⋆ ∅       = ⊤
Γ ▻⋯▻⋆ (Ξ , A) = (Γ ▻⋯▻⋆ Ξ) ∧ (Γ ▻⋯▻ A)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --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.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Pointed

open import Cubical.Data.Sum
open import Cubical.Data.Bool.Base
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation hiding (rec)

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

private
  variable
    ℓ : Level
    A : Type ℓ

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

notIso : Iso Bool Bool
Iso.fun notIso = not
Iso.inv notIso = not
Iso.rightInv notIso = notnot
Iso.leftInv notIso = notnot

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
  -- 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

¬true→false : (x : Bool) → ¬ x ≡ true → x ≡ false
¬true→false false _ = refl
¬true→false true p = Empty.rec (p refl)

¬false→true : (x : Bool) → ¬ x ≡ false → x ≡ true
¬false→true false p = Empty.rec (p refl)
¬false→true true _ = refl

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
    = Empty.rec (¬transportNot P false (q ∙ sym p))
  categorize P | inspect true true p q
    = Empty.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

IsoBool→∙ : ∀ {ℓ} {A : Pointed ℓ} → Iso ((Bool , true) →∙ A) (typ A)
Iso.fun IsoBool→∙ f = fst f false
fst (Iso.inv IsoBool→∙ a) false = a
fst (Iso.inv (IsoBool→∙ {A = A}) a) true = pt A
snd (Iso.inv IsoBool→∙ a) = refl
Iso.rightInv IsoBool→∙ a = refl
Iso.leftInv IsoBool→∙ (f , p) =
  ΣPathP ((funExt (λ { false → refl ; true → sym p}))
        , λ i j → p (~ i ∨ j))

-- import here to avoid conflicts
open import Cubical.Data.Unit

-- relation to hProp

BoolProp≃BoolProp* : {a : Bool} → Bool→Type a ≃ Bool→Type* {ℓ} a
BoolProp≃BoolProp* {a = true} = Unit≃Unit*
BoolProp≃BoolProp* {a = false} = uninhabEquiv Empty.rec Empty.rec*

Bool→TypeInj : (a b : Bool) → Bool→Type a ≃ Bool→Type b → a ≡ b
Bool→TypeInj true true _ = refl
Bool→TypeInj true false p = Empty.rec (p .fst tt)
Bool→TypeInj false true p = Empty.rec (invEq p tt)
Bool→TypeInj false false _ = refl

Bool→TypeInj* : (a b : Bool) → Bool→Type* {ℓ} a ≃ Bool→Type* {ℓ} b → a ≡ b
Bool→TypeInj* true true _ = refl
Bool→TypeInj* true false p = Empty.rec* (p .fst tt*)
Bool→TypeInj* false true p = Empty.rec* (invEq p tt*)
Bool→TypeInj* false false _ = refl

isPropBool→Type : {a : Bool} → isProp (Bool→Type a)
isPropBool→Type {a = true} = isPropUnit
isPropBool→Type {a = false} = isProp⊥

isPropBool→Type* : {a : Bool} → isProp (Bool→Type* {ℓ} a)
isPropBool→Type* {a = true} = isPropUnit*
isPropBool→Type* {a = false} = isProp⊥*

DecBool→Type : {a : Bool} → Dec (Bool→Type a)
DecBool→Type {a = true} = yes tt
DecBool→Type {a = false} = no (λ x → x)

DecBool→Type* : {a : Bool} → Dec (Bool→Type* {ℓ} a)
DecBool→Type* {a = true} = yes tt*
DecBool→Type* {a = false} = no (λ (lift x) → x)

Dec→DecBool : {P : Type ℓ} → (dec : Dec P) → P → Bool→Type (Dec→Bool dec)
Dec→DecBool (yes p) _ = tt
Dec→DecBool (no ¬p) q = Empty.rec (¬p q)

DecBool→Dec : {P : Type ℓ} → (dec : Dec P) → Bool→Type (Dec→Bool dec) → P
DecBool→Dec (yes p) _ = p

Dec≃DecBool : {P : Type ℓ} → (h : isProp P)(dec : Dec P) → P ≃ Bool→Type (Dec→Bool dec)
Dec≃DecBool h dec = propBiimpl→Equiv h isPropBool→Type (Dec→DecBool dec) (DecBool→Dec dec)

Bool≡BoolDec : {a : Bool} → a ≡ Dec→Bool (DecBool→Type {a = a})
Bool≡BoolDec {a = true} = refl
Bool≡BoolDec {a = false} = refl

Dec→DecBool* : {P : Type ℓ} → (dec : Dec P) → P → Bool→Type* {ℓ} (Dec→Bool dec)
Dec→DecBool* (yes p) _ = tt*
Dec→DecBool* (no ¬p) q = Empty.rec (¬p q)

DecBool→Dec* : {P : Type ℓ} → (dec : Dec P) → Bool→Type* {ℓ} (Dec→Bool dec) → P
DecBool→Dec* (yes p) _ = p

Dec≃DecBool* : {P : Type ℓ} → (h : isProp P)(dec : Dec P) → P ≃ Bool→Type* {ℓ} (Dec→Bool dec)
Dec≃DecBool* h dec = propBiimpl→Equiv h isPropBool→Type* (Dec→DecBool* dec) (DecBool→Dec* dec)

Bool≡BoolDec* : {a : Bool} → a ≡ Dec→Bool (DecBool→Type* {ℓ} {a = a})
Bool≡BoolDec* {a = true} = refl
Bool≡BoolDec* {a = false} = refl

Bool→Type× : (a b : Bool) → Bool→Type (a and b) → Bool→Type a × Bool→Type b
Bool→Type× true true _ = tt , tt
Bool→Type× true false p = Empty.rec p
Bool→Type× false true p = Empty.rec p
Bool→Type× false false p = Empty.rec p

Bool→Type×' : (a b : Bool) → Bool→Type a × Bool→Type b → Bool→Type (a and b)
Bool→Type×' true true _ = tt
Bool→Type×' true false (_ , p) = Empty.rec p
Bool→Type×' false true (p , _) = Empty.rec p
Bool→Type×' false false (p , _) = Empty.rec p

Bool→Type×≃ : (a b : Bool) → Bool→Type a × Bool→Type b ≃ Bool→Type (a and b)
Bool→Type×≃ a b =
  propBiimpl→Equiv (isProp× isPropBool→Type isPropBool→Type) isPropBool→Type
    (Bool→Type×' a b) (Bool→Type× a b)

Bool→Type⊎ : (a b : Bool) → Bool→Type (a or b) → Bool→Type a ⊎ Bool→Type b
Bool→Type⊎ true true _ = inl tt
Bool→Type⊎ true false _ = inl tt
Bool→Type⊎ false true _ = inr tt
Bool→Type⊎ false false p = Empty.rec p

Bool→Type⊎' : (a b : Bool) → Bool→Type a ⊎ Bool→Type b → Bool→Type (a or b)
Bool→Type⊎' true true _ = tt
Bool→Type⊎' true false _ = tt
Bool→Type⊎' false true _ = tt
Bool→Type⊎' false false (inl p) = Empty.rec p
Bool→Type⊎' false false (inr p) = Empty.rec p

PropBoolP→P : (dec : Dec A) → Bool→Type (Dec→Bool dec) → A
PropBoolP→P (yes p) _ = p

P→PropBoolP : (dec : Dec A) → A → Bool→Type (Dec→Bool dec)
P→PropBoolP (yes p) _ = tt
P→PropBoolP (no ¬p) = ¬p

Bool≡ : Bool → Bool → Bool
Bool≡ true true = true
Bool≡ true false = false
Bool≡ false true = false
Bool≡ false false = true

Bool≡≃ : (a b : Bool) → (a ≡ b) ≃ Bool→Type (Bool≡ a b)
Bool≡≃ true true = isContr→≃Unit (inhProp→isContr refl (isSetBool _ _))
Bool≡≃ true false = uninhabEquiv true≢false Empty.rec
Bool≡≃ false true = uninhabEquiv false≢true Empty.rec
Bool≡≃ false false = isContr→≃Unit (inhProp→isContr refl (isSetBool _ _))
open Iso

-- Bool is equivalent to bi-point type

Iso-⊤⊎⊤-Bool : Iso (Unit ⊎ Unit) Bool
Iso-⊤⊎⊤-Bool .fun (inl tt) = true
Iso-⊤⊎⊤-Bool .fun (inr tt) = false
Iso-⊤⊎⊤-Bool .inv true = inl tt
Iso-⊤⊎⊤-Bool .inv false = inr tt
Iso-⊤⊎⊤-Bool .leftInv (inl tt) = refl
Iso-⊤⊎⊤-Bool .leftInv (inr tt) = refl
Iso-⊤⊎⊤-Bool .rightInv true = refl
Iso-⊤⊎⊤-Bool .rightInv false = refl

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Adjoint where

import Category
import Functor

open Category
open Functor using (Functor)

module Adj where

  open Functor.Projections using (Map; map)

  data _⊢_ {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)(G : Functor ⅅ ℂ) : Set1 where
    adjunction :
      (_*   : {X : Obj ℂ}{Y : Obj ⅅ} -> Map F X ─→ Y -> X ─→ Map G Y)
      (_#   : {X : Obj ℂ}{Y : Obj ⅅ} -> X ─→ Map G Y -> Map F X ─→ Y)
      (inv₁ : {X : Obj ℂ}{Y : Obj ⅅ}(g : X ─→ Map G Y) -> g # * == g)
      (inv₂ : {X : Obj ℂ}{Y : Obj ⅅ}(f : Map F X ─→ Y) -> f * # == f)
      (nat₁ : {X₁ X₂ : Obj ℂ}{Y₁ Y₂ : Obj ⅅ}
	      (f : Y₁ ─→ Y₂)(g : X₂ ─→ X₁)(h : Map F X₁ ─→ Y₁) ->
	      (f ∘ h ∘ map F g) * == map G f ∘ (h *) ∘ g
      )
      (nat₂ : {X₁ X₂ : Obj ℂ}{Y₁ Y₂ : Obj ⅅ}
	      (f : Y₁ ─→ Y₂)(g : X₂ ─→ X₁)(h : X₁ ─→ Map G Y₁) ->
	      (map G f ∘ h ∘ g) # == f ∘ (h #) ∘ map F g
      )
      -> F ⊢ G

open Adj public

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-
  This is mostly for convenience, when working with ideals
  (which are defined for general rings) in a commutative ring.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Ideal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset

open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.Ring.Ideal renaming (IdealsIn to IdealsInRing)
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

IdealsIn : (R : CommRing ℓ) → Type _
IdealsIn R = IdealsInRing (CommRing→Ring R)

module _ (Ring@(R , str) : CommRing ℓ) where
  open CommRingStr str
  makeIdeal : (I : R → hProp ℓ)
              → (+-closed : {x y : R} → x ∈ I → y ∈ I → (x + y) ∈ I)
              → (0r-closed : 0r ∈ I)
              → (·-closedLeft : {x : R} → (r : R) → x ∈ I → r · x ∈ I)
              → IdealsIn (R , str)
  makeIdeal I +-closed 0r-closed ·-closedLeft = I ,
    (record
       { +-closed = +-closed
       ; -closed = λ x∈I → subst (_∈ I) (useSolver _)
                             (·-closedLeft (- 1r) x∈I)
       ; 0r-closed = 0r-closed
       ; ·-closedLeft = ·-closedLeft
       ; ·-closedRight = λ r x∈I →
                       subst (_∈ I)
                             (·-comm r _)
                             (·-closedLeft r x∈I)
       })
       where useSolver : (x : R) → - 1r · x ≡ - x
             useSolver = solve Ring


text:
-- Jesper, 2018-11-29: Instances with explicit arguments will never be
-- used, so declaring them should give a warning.

postulate
  X : Set
  instance _ : Set → X -- this should give a warning

it : {{_ : X}} → X
it {{x}} = x

-- OTOH, this is fine as the instance can be used inside the module
module _ (A : Set) where
  postulate instance instX : X

  test : X
  test = it

-- Andreas, 2020-01-29, issue #4360:
-- Such warnings should also be given for data and record constructors.

record R (A : Set) : Set where
  instance constructor r
  field
    a : A

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

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor where

open import Level
open import Function renaming (id to id→; _∘_ to _●_) using ()

open import Categories.Category
open import Categories.Functor.Core public

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

Endofunctor : Category o ℓ e → Set _
Endofunctor C = Functor C C

id : ∀ {C : Category o ℓ e} → Functor C C
id {C = C} = record
  { F₀           = id→
  ; F₁           = id→
  ; identity     = Category.Equiv.refl C
  ; homomorphism = Category.Equiv.refl C
  ; F-resp-≈     = id→
  }

infixr 9 _∘F_

-- note that this definition could be shortened by inlining the definitions for
-- identity′ and homomorphism′, but the definitions below are simpler to understand.
_∘F_ : ∀ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o″ ℓ″ e″}
    → Functor D E → Functor C D → Functor C E
_∘F_ {C = C} {D = D} {E = E} F G = record
  { F₀ = F.₀ ● G.₀
  ; F₁ = F.₁ ● G.₁
  ; identity = identity′
  ; homomorphism = homomorphism′
  ; F-resp-≈ =  F.F-resp-≈ ● G.F-resp-≈
  }
  where
  module C = Category C using (id)
  module D = Category D using (id)
  module E = Category E using (id; module HomReasoning)
  module F = Functor F
  module G = Functor G

  identity′ : ∀ {A} → E [ F.₁ (G.₁ (C.id {A})) ≈ E.id ]
  identity′ = begin
    F.₁ (G.₁ C.id) ≈⟨ F.F-resp-≈ G.identity ⟩
    F.₁ D.id       ≈⟨ F.identity ⟩
    E.id           ∎
    where open E.HomReasoning

  homomorphism′ : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]}
                 → E [ F.₁ (G.₁ (C [ g ∘ f ])) ≈ E [ F.₁ (G.₁ g) ∘ F.₁ (G.₁ f) ] ]
  homomorphism′ {f = f} {g = g} = begin
    F.₁ (G.₁ (C [ g ∘ f ]))         ≈⟨ F.F-resp-≈ G.homomorphism ⟩
    F.₁ (D [ G.₁ g ∘ G.₁ f ])       ≈⟨ F.homomorphism ⟩
    E [ F.₁ (G.₁ g) ∘ F.₁ (G.₁ f) ] ∎
    where open E.HomReasoning

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:
module Type.Properties.Inhabited{ℓ} where

import      Lvl
open import Type

-- An inhabited type, which essentially means non-empty (there exists objects with this type), and this object is pointed out/specified/chosen.
-- This means that there exists objects with such an type, and such an object is extractable constructively (like a witness).
-- Also called: Pointed type.
record ◊ (T : Type{ℓ}) : Type{ℓ} where
  constructor intro
  field
    ⦃ existence ⦄ : T
open ◊ ⦃ ... ⦄ renaming (existence to [◊]-existence) public

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:
{-

ℚ is a Commutative Ring

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.QuoQ where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.HITs.Rationals.QuoQ
  renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)

open CommRingStr

ℚCommRing : CommRing ℓ-zero
ℚCommRing .fst = ℚType
ℚCommRing .snd .0r = 0
ℚCommRing .snd .1r = 1
ℚCommRing .snd ._+_ = _+ℚ_
ℚCommRing .snd ._·_ = _·ℚ_
ℚCommRing .snd .-_ = -ℚ_
ℚCommRing .snd .isCommRing = isCommRingℚ
  where
  abstract
    isCommRingℚ : IsCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_
    isCommRingℚ = makeIsCommRing
      isSetℚ +-assoc +-identityʳ
      +-inverseʳ +-comm ·-assoc
      ·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Calf.CostMonoid
open import Data.Nat using (ℕ)

module Examples.Sorting.Comparable
  (costMonoid : CostMonoid) (fromℕ : ℕ → CostMonoid.ℂ costMonoid) where

open CostMonoid costMonoid using (ℂ)

open import Calf costMonoid
open import Calf.Types.Bool
open import Calf.Types.Bounded costMonoid

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
open import Function

record Comparable : Set₁ where
  field
    A : tp pos
    _≤_ : val A → val A → Set
    _≤ᵇ_ : val A → val A → cmp (F bool)
    ≤ᵇ-reflects-≤ : ∀ {x y b} → ◯ ((x ≤ᵇ y) ≡ ret b → Reflects (x ≤ y) b)
    ≤-refl : Reflexive _≤_
    ≤-trans : Transitive _≤_
    ≤-total : Total _≤_
    ≤-antisym : Antisymmetric _≡_ _≤_
    h-cost : (x y : val A) → IsBounded bool (x ≤ᵇ y) (fromℕ 1)

NatComparable : Comparable
NatComparable = record
  { A = nat
  ; _≤_ = _≤_
  ; _≤ᵇ_ = λ x y → step (F bool) (fromℕ 1) (ret (x ≤ᵇ y))
  ; ≤ᵇ-reflects-≤ = reflects
  ; ≤-refl = ≤-refl
  ; ≤-trans = ≤-trans
  ; ≤-total = ≤-total
  ; ≤-antisym = ≤-antisym
  ; h-cost = λ _ _ →
      bound/relax
        (λ u → CostMonoid.≤-reflexive costMonoid (CostMonoid.+-identityʳ costMonoid (fromℕ 1)))
        (bound/step (fromℕ 1) (CostMonoid.zero costMonoid) bound/ret)
  }
  where
    open import Calf.Types.Nat

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

    ret-injective : ∀ {𝕊 v₁ v₂} → ret {U (meta 𝕊)} v₁ ≡ ret {U (meta 𝕊)} v₂ → v₁ ≡ v₂
    ret-injective {𝕊} = Eq.cong (λ e → bind {U (meta 𝕊)} (meta 𝕊) e id)

    reflects : ∀ {m n b} → ◯ (step (F bool) (fromℕ 1) (ret (m ≤ᵇ n)) ≡ ret {bool} b → Reflects (m ≤ n) b)
    reflects {m} {n} {b} u h with ret-injective (Eq.subst (_≡ ret b) (step/ext (F bool) (ret (m ≤ᵇ n)) (fromℕ 1) u) h)
    ... | refl = ≤ᵇ-reflects-≤ m n

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{- Name: Bowornmet (Ben) Hudson and Theodore (Ted) Kim

    -- COMP360 Final Project: Group Theory in Agda --

In this project, we define some fundamental ideas of group theory and
prove a few basic theorems about the topic using Agda. For example, we
define what a group is, and give several elementary examples of groups.
We utilize the notion of propositional equality in Agda to prove our
theorems using equation chains.

-}

open import Preliminaries

module finalproject where

  -- addition of nats
  plusNat : Nat → Nat → Nat
  plusNat Z m = m
  plusNat (S n) m = S (plusNat n m)

  -- integers
  data Int : Set where
    _-_ : (n : Nat) → (m : Nat) → Int

  -- negation
  -_ : Int → Int
  - (n - m) = m - n

  -- addition of ints
  plusInt : Int → Int → Int
  plusInt (n1 - m1) (n2 - m2) = plusNat n1 n2 - plusNat m1 m2

  -- operation
  Op : Set → Set
  Op el = el → el → el

  -- record of Group
  {- Definition: a Group is a set G with a binary operation, *, with three properties:
     1.) G has an identity element, e ∈ G, such that ∀ x ∈ G, e*x = x = x*e.
     2.) ∀ x ∈ G, ∃ x' ∈ G such that x*x' = e = x'*x, where e is the identity element of G.
     3.) G is associative. That is, ∀ x y z ∈ G, (x*y)*z = x*(y*z).
  -}
  record Group : Set1 where
    field
      el : Set
      _*_ : Op el
      e : el
      inv : el → el
      assoc :  ∀ x y z → ((x * y) * z) == (x * (y * z))
      ident-l : ∀ x → (e * x) == x
      ident-r : ∀ x → (x * e) == x
      inv-l : ∀ x → ((inv x) * x) == e
      inv-r : ∀ x → (x * (inv x)) == e

  -- first example, Bools with "multiplication" operation. Comparable to Z mod 2
  -- with addition

  -- multiplication of bools
  multB : Bool → Bool → Bool
  multB True True = True
  multB True False = False
  multB False True = False
  multB False False = True

  -- associativity of bools
  assocB : ∀ (x y z : Bool) → multB (multB x y) z == multB x (multB y z)
  assocB True True True = Refl
  assocB True True False = Refl
  assocB True False True = Refl
  assocB True False False = Refl
  assocB False True True = Refl
  assocB False True False = Refl
  assocB False False True = Refl
  assocB False False False = Refl

  -- proof of identity
  multTruel : ∀ (x : Bool) → (multB True x == x)
  multTruel True = Refl
  multTruel False = Refl

  multTruer : ∀ (x : Bool) → (multB x True == x)
  multTruer True = Refl
  multTruer False = Refl

  -- inverses of bools
  invB : Bool → Bool
  invB True = True
  invB False = False

  -- proof of inverses with identity
  invBMultl : ∀ (x : Bool) → (multB (invB x) x == True)
  invBMultl True = Refl
  invBMultl False = Refl

  invBMultr : ∀ (x : Bool) → (multB x (invB x) == True)
  invBMultr True = Refl
  invBMultr False = Refl

  -- proof that the Booleans are a group on multiplication
  Bool*-isgroup : Group
  Bool*-isgroup = record {
               el = Bool;
               _*_ = multB;
               e = True;
               inv = invB;
               assoc = assocB;
               ident-l = multTruel;
               ident-r = multTruer;
               inv-l = invBMultl;
               inv-r = invBMultr }

  -- second example of a group, ints with the addition operation

  -- congruence
  congruenceNatInt : ∀ (a b c d : Nat) → a == c → b == d → a - b == c - d
  congruenceNatInt .c .d c d Refl Refl = Refl

  congruenceNat : ∀ (x y : Nat) → x == y → (S x) == (S y)
  congruenceNat .y y Refl = Refl

  congruenceNat' : ∀ (n m : Nat) → n == m → S n == S m
  congruenceNat' .m m Refl = Refl

  -- lemma
  addZNat : ∀ (x : Nat) → plusNat x Z == x
  addZNat Z = Refl
  addZNat (S x) = congruenceNat (plusNat x Z) x (addZNat x)

  -- proof of associativity
  assocNat+ : (x y z : Nat) → plusNat (plusNat x y) z == plusNat x (plusNat y z)
  assocNat+ Z y z = Refl
  assocNat+ (S x) y z = congruenceNat (plusNat (plusNat x y) z) (plusNat x (plusNat y z)) (assocNat+ x y z)

  assocInt+ : ∀ (a b c : Int) → plusInt (plusInt a b) c == plusInt a (plusInt b c)
  assocInt+ (n1 - m1) (n2 - m2) (n3 - m3) = congruenceNatInt (plusNat (plusNat n1 n2) n3)
                                              (plusNat (plusNat m1 m2) m3) (plusNat n1 (plusNat n2 n3))
                                              (plusNat m1 (plusNat m2 m3)) (assocNat+ n1 n2 n3) (assocNat+ m1 m2 m3)

  -- proof of identity
  addIntZl : ∀ (n : Int) → (plusInt (Z - Z) n == n)
  addIntZl (n - m) = Refl

  addIntZr : ∀ (n : Int) → (plusInt n (Z - Z) == n)
  addIntZr (n - m) = congruenceNatInt (plusNat n 0) (plusNat m 0) n m (addZNat n) (addZNat m)

  -- proof of inverses
  -- issue with quotient type: impossible to prove that (S n) - (S n) = 0 - 0 without equality constructor
  -- had problems in including the equality constructor, only thing we could not work out
  invIntl : ∀ (n : Int) → plusInt (- n) n == (Z - Z)
  invIntl (n - m) = {!!}

  invIntr : ∀ (n : Int) → plusInt n (- n) == (Z - Z)
  invIntr (n - m) = {!!}

  -- proof that the integers on addition are a group
  Int+-isgroup : Group
  Int+-isgroup = record {
              el = Int;
              _*_ = plusInt;
              e = Z - Z;
              inv = -_;
              assoc = assocInt+;
              ident-l = addIntZl;
              ident-r = addIntZr;
              inv-l = invIntl;
              inv-r = invIntr }

   {- Definition: an group is called abelian if it is commutative.
      That is, ∀ x y ∈ G, x*y = y*x. Our record of an abelian group
      requires a group and a proof that the group operation
      is commutative.
   -}
  record AbelianGroup (G : Group) : Set where
    open Group G
    field
      comm : ∀ (x y : el) → x * y == y * x

  -- proof of commutativity for multiplication on bools
  commB : ∀ (x y : Bool) → multB x y == multB y x
  commB True True = Refl
  commB True False = Refl
  commB False True = Refl
  commB False False = Refl

  Bool*-isAbelian : AbelianGroup Bool*-isgroup
  Bool*-isAbelian = record {
                 comm = commB }

  -- some theorems
  module Theorems (G : Group) where
    open Group G
    congruenceOP : {a b c : el} → a == b → a * c == b * c
    congruenceOP Refl = Refl

    congruenceOP' : {a b c : el} → b == c → a * b == a * c
    congruenceOP' Refl = Refl

    sym : {a b : el} → a == b → b == a
    sym Refl = Refl

    -- extremely simple theorem
    babytheorem : (a b : el) → ((a * e) * b) == (a * b)
    babytheorem a b = congruenceOP (ident-r a)

    -- theorem 1: Let G be a group, and let a and b ∈ G. Then (a * b)^-1 = b^-1 * a^-1.
    theorem1 : ∀ (a b : el) → inv (a * b) == (inv b * inv a)
    theorem1 a b  = inv (a * b)                                      =⟨ sym (ident-r (inv (a * b))) ⟩
                    (inv (a * b) * e)                               =⟨ sym (congruenceOP' (inv-r a)) ⟩
                    (inv (a * b) * (a * inv a))                     =⟨ congruenceOP' (congruenceOP (sym (ident-r a))) ⟩
                    (inv (a * b) * ((a * e) * inv a))               =⟨ congruenceOP' (congruenceOP (congruenceOP' (sym (inv-r b)))) ⟩
                    (inv (a * b) * ((a * (b * inv b)) * inv a))     =⟨ congruenceOP' (congruenceOP (sym (assoc a b (inv b)))) ⟩
                    (inv (a * b) * (((a * b) * inv b) * inv a))     =⟨ congruenceOP' (assoc (a * b) (inv b) (inv a)) ⟩
                    (inv (a * b) * ((a * b) * (inv b * inv a)))     =⟨ sym (assoc (inv (a * b)) (a * b) (inv b * inv a)) ⟩
                    ((inv (a * b) * (a * b)) * (inv b * inv a))     =⟨ congruenceOP (inv-l (a * b)) ⟩
                    (e * (inv b * inv a))                           =⟨ ident-l (inv b * inv a) ⟩
                    (inv b * inv a)                                 ∎

    -- theorem 2: Let G be a group, and let a, b, and c ∈ G. If a * c = b * c, then a = b.
    theorem2 : ∀ (a b c : el) → (a * c) == (b * c) → a == b
    theorem2 a b c p = a                            =⟨ sym (ident-r a) ⟩
                       a * e                        =⟨ congruenceOP' (sym (inv-r c)) ⟩
                       (a * (c * inv c))            =⟨ sym (assoc a c (inv c)) ⟩
                       (a * c) * inv c              =⟨ congruenceOP p ⟩
                       (b * c) * inv c              =⟨ assoc b c (inv c) ⟩
                       (b * (c * inv c))            =⟨ congruenceOP' (inv-r c) ⟩
                       (b * e)                      =⟨ ident-r b ⟩
                       b                            ∎

    -- theorem 3: Let G be a group, and let g ∈ G. If g * g = g, then g = e.
    theorem3 : ∀ (g : el) → (g * g) == g → g == e
    theorem3 g p = g                       =⟨ sym (ident-r g) ⟩
                   (g * e)                 =⟨ congruenceOP' (sym (inv-r g)) ⟩
                   (g * (g * inv g))       =⟨ sym (assoc g g (inv g)) ⟩
                   (g * g) * inv g         =⟨ congruenceOP p ⟩
                   g * inv g               =⟨ inv-r g ⟩
                   e                       ∎

    -- lemma 1: for all x ∈ G, if x * x = e, x^-1 = x. That is, x is its own inverse.
    lemma1 : ∀ (x : el) → (p : x * x == e) → inv x == x
    lemma1 x p = (inv x)                          =⟨ sym (ident-r (inv x)) ⟩
                 (inv x * e)                      =⟨ congruenceOP' (sym p) ⟩
                 inv x * (x * x)                  =⟨ sym (assoc (inv x) x x) ⟩
                 (inv x * x) * x                  =⟨ congruenceOP (inv-l x) ⟩
                 (e * x)                          =⟨ ident-l x ⟩
                 x                                ∎

    -- theorem 4: let G be a group. If ∀ x ∈ G, x * x = e, then G is abelian.
    theorem4 : (p : ∀ x → (x * x) == e) → AbelianGroup G
    theorem4 p = record {
                comm = λ a b → a * b                            =⟨ congruenceOP (sym (ident-r a)) ⟩
                               (a * e) * b                      =⟨ congruenceOP (congruenceOP' (sym (inv-r a))) ⟩
                               (a * (a * inv a)) * b            =⟨ congruenceOP (sym (assoc a a (inv a))) ⟩
                               ((a * a) * inv a) * b            =⟨ congruenceOP (congruenceOP (p a)) ⟩
                               (e * inv a) * b                  =⟨ congruenceOP (ident-l (inv a)) ⟩
                               inv a * b                        =⟨ congruenceOP' (sym (ident-r b)) ⟩
                               inv a * (b * e)                  =⟨ congruenceOP' (congruenceOP' (sym (inv-r b))) ⟩
                               inv a * (b * (b * inv b))        =⟨ congruenceOP' (sym (assoc b b (inv b))) ⟩
                               inv a * ((b * b) * inv b)        =⟨ congruenceOP' (congruenceOP (p b)) ⟩
                               inv a * (e * inv b)              =⟨ congruenceOP' (ident-l (inv b)) ⟩
                               (inv a * inv b)                  =⟨ sym (theorem1 b a) ⟩
                               (inv (b * a))                    =⟨ lemma1 (b * a) (p (b * a)) ⟩
                               (b * a)                          ∎ }

    -- theorem 5: Let G be a group, and a, b, and c ∈ G. If (a * b) * c = e, then (b * c) * a = e as well.
    theorem5 : ∀ (a b c : el) → ((a * b) * c) == e → ((b * c) * a) == e
    theorem5 a b c p = ((b * c) * a)                         =⟨ sym (ident-l ((b * c) * a)) ⟩
                       e * ((b * c) * a)                     =⟨ congruenceOP (sym (inv-l a)) ⟩
                       (inv a * a) * ((b * c) * a)           =⟨ assoc (inv a) a ((b * c) * a) ⟩
                       inv a * (a * ((b * c) * a))           =⟨ sym (congruenceOP' (assoc a (b * c) a)) ⟩
                       inv a * ((a * (b * c)) * a)           =⟨ congruenceOP' (congruenceOP (sym (assoc a b c))) ⟩
                       inv a * (((a * b) * c) * a)           =⟨ congruenceOP' (congruenceOP p) ⟩
                       inv a * (e * a)                       =⟨ congruenceOP' (ident-l a) ⟩
                       (inv a * a)                           =⟨ inv-l a ⟩
                       e                                     ∎

  {- Definition: a homomorphism is a function f from a group (G , *) to another group (H , ∘)
     such that (∀ a,b ∈ G), f(a*b) = f(a)∘f(b). Our definition of a homomorphism also includes a
     proof that homomorphisms preserve identity elements between groups. That is, f(e_G) = e_H,
     where e_G and e_H are the identity elements in G and H, respectively.
  -}
  -- record of homomorphisms
  record Homomorphism (G : Group) (H : Group) : Set where
    open Group renaming (_*_ to *)
    field
      f : el G → el H
      preserve-id : f (e G) == e H
      preserve-op : ∀ (a b : el G) → (f (* G a b)) == * H (f a) (f b)

  -- third example of a group, Z mod 2 under addition.
  -- Z mod 2
  data Zmod2 : Set where
    Zero : Zmod2
    One : Zmod2

  -- addition mod 2
  plusmod2 : Zmod2 → Zmod2 → Zmod2
  plusmod2 Zero Zero = Zero
  plusmod2 Zero One = One
  plusmod2 One Zero = One
  plusmod2 One One = Zero

  -- identity of Z mod 2
  idenZmod2-l : (x : Zmod2) → plusmod2 Zero x == x
  idenZmod2-l Zero = Refl
  idenZmod2-l One = Refl

  idenZmod2-r : (x : Zmod2) → plusmod2 x Zero == x
  idenZmod2-r Zero = Refl
  idenZmod2-r One = Refl

  -- inverses of Z mod 2 (the inverse of anything in Z mod 2 is itself)
  invZmod2 : Zmod2 → Zmod2
  invZmod2 x = x

  -- left and right inverses of Z mod 2
  invZmod2-lr : (x : Zmod2) → plusmod2 x x == Zero
  invZmod2-lr Zero = Refl
  invZmod2-lr One = Refl

  -- associativity of addition in Z mod 2
  assocZmod2 : (x y z : Zmod2) → plusmod2 (plusmod2 x y) z == plusmod2 x (plusmod2 y z)
  assocZmod2 Zero Zero Zero = Refl
  assocZmod2 Zero Zero One = Refl
  assocZmod2 Zero One Zero = Refl
  assocZmod2 Zero One One = Refl
  assocZmod2 One Zero Zero = Refl
  assocZmod2 One Zero One = Refl
  assocZmod2 One One Zero = Refl
  assocZmod2 One One One = Refl

  -- commutativity of addition in Z mod 2
  commZmod2 : (x y : Zmod2) → plusmod2 x y == plusmod2 y x
  commZmod2 Zero Zero = Refl
  commZmod2 Zero One = Refl
  commZmod2 One Zero = Refl
  commZmod2 One One = Refl

  -- Zmod2 is a group on addition.
  Zmod2+-isgroup : Group
  Zmod2+-isgroup = record {
                el = Zmod2;
                _*_ = plusmod2;
                e = Zero;
                inv = invZmod2;
                assoc = assocZmod2;
                ident-l = idenZmod2-l;
                ident-r = idenZmod2-r;
                inv-l = λ x → invZmod2-lr x;
                inv-r = λ x → invZmod2-lr x }

  -- proof that Z mod 2 on addition is an abelian group.
  Zmod2+-isAbelian : AbelianGroup (Zmod2+-isgroup)
  Zmod2+-isAbelian = record {
                  comm = commZmod2 }

  -- example of a homomorphism: mapBool-to-Zmod2 is a homomorphism from Bools on multiplication to Zmod2 with addition.
  -- map from Bools to the elements of Zmod2.
  mapBool-to-Zmod2 : Bool → Zmod2
  mapBool-to-Zmod2 True = Zero
  mapBool-to-Zmod2 False = One

  -- proof that the map from Bools to Zmod2 preserves composition.
  mapBool-to-Zmod2-preserve-op : (a b : Bool) → mapBool-to-Zmod2 (multB a b) == plusmod2 (mapBool-to-Zmod2 a) (mapBool-to-Zmod2 b)
  mapBool-to-Zmod2-preserve-op True True = Refl
  mapBool-to-Zmod2-preserve-op True False = Refl
  mapBool-to-Zmod2-preserve-op False True = Refl
  mapBool-to-Zmod2-preserve-op False False = Refl

  homomorphism-example : Homomorphism (Bool*-isgroup) (Zmod2+-isgroup)
  homomorphism-example = record {
                      f = mapBool-to-Zmod2;
                      preserve-id = Refl;
                      preserve-op = mapBool-to-Zmod2-preserve-op }

   -- record of isomorphisms.
  {- Definition: a homomorphism between two groups is called an isomorphism
     if it is bijective (both one-to-one and onto). The isomorphism record
     requires a homomorphism along with proofs that it is both one-to-one
     (injective) and onto (surjective).
  -}
  record Isomorphism (G : Group) (H : Group) : Set where
    open Group
    open Homomorphism
    field
      homomorphism : Homomorphism G H
      injective : ∀ (a b : el G) → f homomorphism a == f homomorphism b → a == b
      surjective : ∀ (b : el H) → Σ (λ g → f homomorphism g == b)

  -- example of an isomorphism
  -- proof that this map from Bools to Zmod2 is injective (that is, ∀ a b : Bool, f(a) = f(b) implies a = b).
  mapB-Zmod2-inj : (a b : Bool) → mapBool-to-Zmod2 a == mapBool-to-Zmod2 b → a == b
  mapB-Zmod2-inj True True p = Refl
  mapB-Zmod2-inj True False ()
  mapB-Zmod2-inj False True ()
  mapB-Zmod2-inj False False p = Refl

  -- proof that this map from Bools to Zmod2 is surjective (that is, ∀ b : Zmod2, ∃ a ∈ Bool such that f(a) = b).
  mapB-Zmod2-sur : (n : Zmod2) → Σ (λ bool → mapBool-to-Zmod2 bool == n)
  mapB-Zmod2-sur Zero = True , Refl
  mapB-Zmod2-sur One = False , Refl

  -- the homomorphism between Bools on multiplication to Zmod2 with addition is isomorphic
  isomorphism-example : Isomorphism Bool*-isgroup Zmod2+-isgroup
  isomorphism-example = record {
                     homomorphism = homomorphism-example;
                     injective = mapB-Zmod2-inj;
                     surjective = mapB-Zmod2-sur }

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
module PiQ.Eval where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Data.Nat hiding (_≟_)
open import Data.List as L hiding (_∷_)
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiQ.Syntax
open import PiQ.Opsem
open import PiQ.AuxLemmas
open import PiQ.NoRepeat
open import PiQ.Invariants

infix 100 _⃗
infix 100 _⃖

-- Stuck states must be either of the form ⟨ c ∣ v ∣ ☐ ⟩◁), ［ c ∣ v ∣ ☐ ］▷ or ⊠
Stuck : ∀ {st} → is-stuck st
      → (Σ[ A ∈ 𝕌 ] Σ[ B ∈ 𝕌 ] Σ[ c ∈ A ↔ B ] Σ[ v ∈ ⟦ A ⟧ ] st ≡ ⟨ c ∣ v ∣ ☐ ⟩◁)
      ⊎ (Σ[ A ∈ 𝕌 ] Σ[ B ∈ 𝕌 ] Σ[ c ∈ A ↔ B ] Σ[ v ∈ ⟦ B ⟧ ] st ≡ ［ c ∣ v ∣ ☐ ］▷)
      ⊎ st ≡ ⊠
Stuck {⟨ unite₊l ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ uniti₊l ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ swap₊   ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ assocl₊ ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ assocr₊ ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ unite⋆l ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ uniti⋆l ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ swap⋆   ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ assocl⋆ ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ assocr⋆ ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ dist    ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ factor  ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₁))
Stuck {⟨ id↔     ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₂))
Stuck {⟨ c₁ ⨾ c₂ ∣ v          ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₃))
Stuck {⟨ c₁ ⊕ c₂ ∣ inj₁ x     ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₄))
Stuck {⟨ c₁ ⊕ c₂ ∣ inj₂ y     ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₅))
Stuck {⟨ c₁ ⊗ c₂ ∣ (x , y)    ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗₆))
Stuck {⟨ ε₊      ∣ inj₁ x     ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦ε₊₁))
Stuck {⟨ ε₊      ∣ inj₂ (- x) ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦ε₊₂))
Stuck {⟨ ηₓ _    ∣ tt         ∣ κ ⟩▷} stuck = ⊥-elim (stuck (_ , ↦⃗ηₓ))
Stuck {⟨ εₓ v    ∣ (v' , ↻)   ∣ κ ⟩▷} stuck with v ≟ v'
... | yes p = ⊥-elim (stuck (_ , ↦⃗εₓ₁ {eq = p}))
... | no  p = ⊥-elim (stuck (_ , ↦⃗εₓ₂ {neq = p}))
Stuck {［ c ∣ v ∣ ☐ ］▷}               stuck = inj₂ (inj₁ (_ , _ , c , v , refl))
Stuck {［ c₁ ∣ v ∣ ☐⨾ c₂ • κ ］▷}      stuck = ⊥-elim (stuck (_ , ↦⃗₇))
Stuck {［ c ∣ v ∣ c₁ ⨾☐• κ ］▷}        stuck = ⊥-elim (stuck (_ , ↦⃗₁₀))
Stuck {［ c ∣ v ∣ ☐⊕ c₂ • κ ］▷}       stuck = ⊥-elim (stuck (_ , ↦⃗₁₁))
Stuck {［ c ∣ v ∣ c₁ ⊕☐• κ ］▷}        stuck = ⊥-elim (stuck (_ , ↦⃗₁₂))
Stuck {［ c ∣ v ∣ ☐⊗[ c₂ , x ]• κ ］▷} stuck = ⊥-elim (stuck (_ , ↦⃗₈))
Stuck {［ c ∣ v ∣ [ c₁ , x ]⊗☐• κ ］▷} stuck = ⊥-elim (stuck (_ , ↦⃗₉))
Stuck {⟨ c  ∣ v ∣ ☐ ⟩◁}                stuck = inj₁ (_ , _ , c , v , refl)
Stuck {⟨ c₁ ∣ v ∣ ☐⨾ c₂ • κ ⟩◁}        stuck = ⊥-elim (stuck (_ , ↦⃖₃))
Stuck {⟨ c₂ ∣ v ∣ c₁ ⨾☐• κ ⟩◁}         stuck = ⊥-elim (stuck (_ , ↦⃖₇))
Stuck {⟨ c₁ ∣ v ∣ ☐⊕ c₂ • κ ⟩◁}        stuck = ⊥-elim (stuck (_ , ↦⃖₄))
Stuck {⟨ c₂ ∣ v ∣ c₁ ⊕☐• κ ⟩◁}         stuck = ⊥-elim (stuck (_ , ↦⃖₅))
Stuck {⟨ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ⟩◁}  stuck = ⊥-elim (stuck (_ , ↦⃖₆))
Stuck {⟨ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ⟩◁}  stuck = ⊥-elim (stuck (_ , ↦⃖₈))
Stuck {［ unite₊l ∣ v ∣ κ ］◁}             stuck = ⊥-elim (stuck (⟨ _ ∣ inj₂ v ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ uniti₊l ∣ inj₂ y ∣ κ ］◁}        stuck = ⊥-elim (stuck (⟨ _ ∣ y ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ swap₊ ∣ inj₁ x ∣ κ ］◁}          stuck = ⊥-elim (stuck (⟨ _ ∣ inj₂ x ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ swap₊ ∣ inj₂ y ∣ κ ］◁}          stuck = ⊥-elim (stuck (⟨ _ ∣ inj₁ y ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocl₊ ∣ inj₁ (inj₁ x) ∣ κ ］◁} stuck = ⊥-elim (stuck (⟨ _ ∣ inj₁ x ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocl₊ ∣ inj₁ (inj₂ y) ∣ κ ］◁} stuck = ⊥-elim (stuck (⟨ _ ∣ inj₂ (inj₁ y) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocl₊ ∣ inj₂ y ∣ κ ］◁}        stuck = ⊥-elim (stuck (⟨ _ ∣ inj₂ (inj₂ y) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocr₊ ∣ inj₁ x ∣ κ ］◁}        stuck = ⊥-elim (stuck (⟨ _ ∣ inj₁ (inj₁ x) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocr₊ ∣ inj₂ (inj₁ x) ∣ κ ］◁} stuck = ⊥-elim (stuck (⟨ _ ∣ inj₁ (inj₂ x) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocr₊ ∣ inj₂ (inj₂ y) ∣ κ ］◁} stuck = ⊥-elim (stuck (⟨ _ ∣ (inj₂ y) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ unite⋆l ∣ v ∣ κ ］◁}             stuck = ⊥-elim (stuck (⟨ _ ∣ (tt , v) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ uniti⋆l ∣ (tt , v) ∣ κ ］◁}      stuck = ⊥-elim (stuck (⟨ _ ∣ v ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ swap⋆ ∣ (x , y) ∣ κ ］◁}         stuck = ⊥-elim (stuck (⟨ _ ∣ (y , x) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocl⋆ ∣ (x , y) , z ∣ κ ］◁}   stuck = ⊥-elim (stuck (⟨ _ ∣ x , (y , z) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ assocr⋆ ∣ x , (y , z) ∣ κ ］◁}   stuck = ⊥-elim (stuck (⟨ _ ∣ (x , y) , z ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ dist ∣ inj₁ (x , z) ∣ κ ］◁}     stuck = ⊥-elim (stuck (⟨ _ ∣ inj₁ x , z ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ dist ∣ inj₂ (y , z) ∣ κ ］◁}     stuck = ⊥-elim (stuck (⟨ _ ∣ inj₂ y , z ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ factor ∣ inj₁ x , z ∣ κ ］◁}     stuck = ⊥-elim (stuck (⟨ _ ∣ inj₁ (x , z) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ factor ∣ inj₂ y , z ∣ κ ］◁}     stuck = ⊥-elim (stuck (⟨ _ ∣ inj₂ (y , z) ∣ _ ⟩◁ , ↦⃖₁))
Stuck {［ id↔     ∣ v ∣ κ ］◁}             stuck = ⊥-elim (stuck (_ , ↦⃖₂))
Stuck {［ c₁ ⨾ c₂ ∣ v ∣ κ ］◁}             stuck = ⊥-elim (stuck (_ , ↦⃖₁₀))
Stuck {［ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ］◁}        stuck = ⊥-elim (stuck (_ , ↦⃖₁₁))
Stuck {［ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ］◁}        stuck = ⊥-elim (stuck (_ , ↦⃖₁₂))
Stuck {［ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ］◁}       stuck = ⊥-elim (stuck (_ , ↦⃖₉))
Stuck {［ η₊      ∣ inj₁ x ∣ κ ］◁}        stuck = ⊥-elim (stuck (_ , ↦η₊₁))
Stuck {［ η₊      ∣ inj₂ (- x) ∣ κ ］◁}    stuck = ⊥-elim (stuck (_ , ↦η₊₂))
Stuck {［ ηₓ v    ∣ (v' , ↻)   ∣ κ ］◁}    stuck with v ≟ v'
... | yes p = ⊥-elim (stuck (_ , ↦⃖ηₓ₁ {eq = p}))
... | no  p = ⊥-elim (stuck (_ , ↦⃖ηₓ₂ {neq = p}))
Stuck {［ εₓ _    ∣ tt         ∣ κ ］◁}    stuck = ⊥-elim (stuck (_ , ↦⃖εₓ))
Stuck {⊠}                                 stuck = inj₂ (inj₂ refl)

-- Find next step of given the state
step : (st : State) → ∃[ st' ] (st ↦ st') ⊎ is-stuck st
step ⟨ unite₊l ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ uniti₊l ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ swap₊   ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ assocl₊ ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ assocr₊ ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ unite⋆l ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ uniti⋆l ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ swap⋆   ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ assocl⋆ ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ assocr⋆ ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ dist    ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ factor  ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₁)
step ⟨ id↔     ∣ v ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₂)
step ⟨ c₁ ⨾ c₂ ∣ v          ∣ κ ⟩▷ = inj₁ (⟨ c₁ ∣ v ∣ ☐⨾ c₂ • κ ⟩▷ , ↦⃗₃)
step ⟨ c₁ ⊕ c₂ ∣ inj₁ x     ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₄)
step ⟨ c₁ ⊕ c₂ ∣ inj₂ y     ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₅)
step ⟨ c₁ ⊗ c₂ ∣ (x , y)    ∣ κ ⟩▷ = inj₁ (_ , ↦⃗₆)
step ⟨ ε₊      ∣ inj₁ x     ∣ κ ⟩▷ = inj₁ (_ , ↦ε₊₁)
step ⟨ ε₊      ∣ inj₂ (- x) ∣ κ ⟩▷ = inj₁ (_ , ↦ε₊₂)
step ⟨ ηₓ _    ∣ tt         ∣ κ ⟩▷ = inj₁ (_ , ↦⃗ηₓ)
step ⟨ εₓ v    ∣ v' , ↻     ∣ κ ⟩▷ with v ≟ v'
... | yes p = inj₁ (_ , (↦⃗εₓ₁ {eq = p}))
... | no  p = inj₁ (_ , (↦⃗εₓ₂ {neq = p}))
step ［ c  ∣ v ∣ ☐ ］▷               = inj₂ (λ ())
step ［ c₁ ∣ v ∣ ☐⨾ c₂ • κ ］▷       = inj₁ (_ , ↦⃗₇)
step ［ c₂ ∣ v ∣ c₁ ⨾☐• κ ］▷        = inj₁ (_ , ↦⃗₁₀)
step ［ c₁ ∣ v ∣ ☐⊕ c₂ • κ ］▷       = inj₁ (_ , ↦⃗₁₁)
step ［ c₂ ∣ v ∣ c₁ ⊕☐• κ ］▷        = inj₁ (_ , ↦⃗₁₂)
step ［ c₁ ∣ v ∣ ☐⊗[ c₂ , x ]• κ ］▷ = inj₁ (_ , ↦⃗₈)
step ［ c₂ ∣ v ∣ [ c₁ , x ]⊗☐• κ ］▷ = inj₁ (_ , ↦⃗₉)
step ⟨ c ∣ v ∣ ☐ ⟩◁                = inj₂ (λ ())
step ⟨ c₁ ∣ v ∣ ☐⨾ c₂ • κ ⟩◁       = inj₁ (_ , ↦⃖₃)
step ⟨ c₂ ∣ v ∣ c₁ ⨾☐• κ ⟩◁        = inj₁ (_ , ↦⃖₇)
step ⟨ c₁ ∣ v ∣ ☐⊕ c₂ • κ ⟩◁       = inj₁ (_ , ↦⃖₄)
step ⟨ c₂ ∣ v ∣ c₁ ⊕☐• κ ⟩◁        = inj₁ (_ , ↦⃖₅)
step ⟨ c₁ ∣ v ∣ ☐⊗[ c₂ , x ]• κ ⟩◁ = inj₁ (_ , ↦⃖₆)
step ⟨ c₂ ∣ v ∣ [ c₁ , x ]⊗☐• κ ⟩◁ = inj₁ (_ , ↦⃖₈)
step ［ unite₊l ∣ v             ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ v ∣ _ ⟩◁ , ↦⃖₁)
step ［ uniti₊l ∣ inj₂ v        ∣ κ ］◁ = inj₁ (⟨ _ ∣ v ∣ _ ⟩◁ , ↦⃖₁)
step ［ swap₊   ∣ inj₁ x        ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ x ∣ _ ⟩◁ , ↦⃖₁)
step ［ swap₊   ∣ inj₂ y        ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₁ y ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocl₊ ∣ inj₁ (inj₁ x) ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₁ x ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocl₊ ∣ inj₁ (inj₂ y) ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ (inj₁ y) ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocl₊ ∣ inj₂ z        ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ (inj₂ z) ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocr₊ ∣ inj₁ x        ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₁ (inj₁ x) ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocr₊ ∣ inj₂ (inj₁ y) ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₁ (inj₂ y) ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocr₊ ∣ inj₂ (inj₂ z) ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ z ∣ _ ⟩◁ , ↦⃖₁)
step ［ unite⋆l ∣ v             ∣ κ ］◁ = inj₁ (⟨ _ ∣ tt , v ∣ _ ⟩◁ , ↦⃖₁)
step ［ uniti⋆l ∣ (tt , v)      ∣ κ ］◁ = inj₁ (⟨ _ ∣ v ∣ _ ⟩◁ , ↦⃖₁)
step ［ swap⋆   ∣ (x , y)       ∣ κ ］◁ = inj₁ (⟨ _ ∣ (y , x) ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocl⋆ ∣ (x , y) , z   ∣ κ ］◁ = inj₁ (⟨ _ ∣ x , (y , z) ∣ _ ⟩◁ , ↦⃖₁)
step ［ assocr⋆ ∣ x , (y , z)   ∣ κ ］◁ = inj₁ (⟨ _ ∣ (x , y) , z ∣ _ ⟩◁ , ↦⃖₁)
step ［ dist    ∣ inj₁ (x , z)  ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₁ x , z ∣ _ ⟩◁ , ↦⃖₁)
step ［ dist    ∣ inj₂ (y , z)  ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ y , z ∣ _ ⟩◁ , ↦⃖₁)
step ［ factor  ∣ inj₁ x , z    ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₁ (x , z) ∣ _ ⟩◁ , ↦⃖₁)
step ［ factor  ∣ inj₂ y , z    ∣ κ ］◁ = inj₁ (⟨ _ ∣ inj₂ (y , z) ∣ _ ⟩◁ , ↦⃖₁)
step ［ id↔     ∣ v             ∣ κ ］◁ = inj₁ (_ , ↦⃖₂)
step ［ c₁ ⨾ c₂ ∣ v             ∣ κ ］◁ = inj₁ (_ , ↦⃖₁₀)
step ［ c₁ ⊕ c₂ ∣ inj₁ x        ∣ κ ］◁ = inj₁ (_ , ↦⃖₁₁)
step ［ c₁ ⊕ c₂ ∣ inj₂ y        ∣ κ ］◁ = inj₁ (_ , ↦⃖₁₂)
step ［ c₁ ⊗ c₂ ∣ (x , y)       ∣ κ ］◁ = inj₁ (_ , ↦⃖₉)
step ［ η₊      ∣ inj₁ x        ∣ κ ］◁ = inj₁ (_ , ↦η₊₁)
step ［ η₊      ∣ inj₂ (- x)    ∣ κ ］◁ = inj₁ (_ , ↦η₊₂)
step ［ ηₓ v    ∣ (v' , ↻)      ∣ κ ］◁ with v ≟ v'
... | yes p = inj₁ (_ , (↦⃖ηₓ₁ {eq = p}))
... | no  p = inj₁ (_ , (↦⃖ηₓ₂ {neq = p}))
step ［ εₓ _    ∣ tt            ∣ κ ］◁ = inj₁ (_ , ↦⃖εₓ)
step ⊠ = inj₂ (λ ())

-- Values tagged with direction
data Val (A B : 𝕌) : Set where
  _⃗ : ⟦ A ⟧ → Val A B
  _⃖ : ⟦ B ⟧ → Val A B

-- Termination is guaranteed by PiQ.NoRepeat and the finiteness of states
{-# TERMINATING #-}
run : (st₀ : State) → (init : is-initial st₀)
    → let (A , B , c) = getℂ st₀ (st-is-initial⇒st≢⊠ st₀ init)
      in  (Σ[ v ∈ ⟦ A ⟧ ] st₀ ↦* ⟨ c ∣ v ∣ ☐ ⟩◁)
       ⊎  (Σ[ v ∈ ⟦ B ⟧ ] st₀ ↦* ［ c ∣ v ∣ ☐ ］▷)
       ⊎  st₀ ↦* ⊠
run st₀ init = run' st₀ ◾
  where
    run' : (st : State) → st₀ ↦* st → let (A , B , c) = getℂ st₀ (st-is-initial⇒st≢⊠ st₀ init)
                                      in (Σ[ v ∈ ⟦ A ⟧ ] st₀ ↦* ⟨ c ∣ v ∣ ☐ ⟩◁)
                                       ⊎ (Σ[ v ∈ ⟦ B ⟧ ] st₀ ↦* ［ c ∣ v ∣ ☐ ］▷)
                                       ⊎  st₀ ↦* ⊠
    run' st rs with step st
    ... | inj₁ (st' , r) = run' st' (rs ++↦ (r ∷ ◾))
    ... | inj₂ stuck     with Stuck stuck
    ... | inj₁ (A , B , c , v , refl) with ℂInvariant* rs (st-is-initial⇒st≢⊠ st₀ init) (λ ())
    ... | refl = inj₁ (v , rs)
    run' st rs | inj₂ stuck | inj₂ (inj₁ (A , B , c , v , refl)) with ℂInvariant* rs (st-is-initial⇒st≢⊠ st₀ init) (λ ())
    ... | refl = inj₂ (inj₁ (v , rs))
    run' st rs | inj₂ stuck | inj₂ (inj₂ refl) = inj₂ (inj₂ rs)

-- Forward evaluator of PiQ
eval : ∀ {A B} → (A ↔ B) → Val A B → Maybe (Val B A)
eval c (v ⃗) = [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ (run ⟨ c ∣ v ∣ ☐ ⟩▷ (λ ()))
eval c (v ⃖) = [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ (run ［ c ∣ v ∣ ☐ ］◁ (λ ()))

-- Backward evaluator of PiQ
evalᵣₑᵥ : ∀ {A B} → (A ↔ B) → Val B A → Maybe (Val A B)
evalᵣₑᵥ c (v ⃖) = [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ (run ⟨ c ∣ v ∣ ☐ ⟩▷ (λ ()))
evalᵣₑᵥ c (v ⃗) = [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ (run ［ c ∣ v ∣ ☐ ］◁ (λ ()))

-- Evaluator which generate execution traces
convert↦ : ∀ {st st'} → st ↦* st' → List State
convert↦ (◾ {st}) = st L.∷ []
convert↦ (_∷_ {st} r rs) = st L.∷ convert↦ rs

evalₜᵣ : ∀ {A B} → (A ↔ B) → ⟦ A ⟧ → List State
evalₜᵣ c v with (run ⟨ c ∣ v ∣ ☐ ⟩▷ (λ ()))
... | inj₁ (_ , rs) = convert↦ rs
... | inj₂ (inj₁ (_ , rs)) = convert↦ rs
... | inj₂ (inj₂ rs) = convert↦ rs

-- Faster evaluator which does not carry the reduction trace.
-- Returns the result and the number of steps it takes
{-# TERMINATING #-}
eval' : ∀ {A B} → (A ↔ B) → ⟦ A ⟧ → Maybe (Σ[ t ∈ 𝕌 ] ⟦ t ⟧) × ℕ
eval' c v = run' ⟨ c ∣ v ∣ ☐ ⟩▷ 0
  where
  getV : State → Maybe (Σ[ t ∈ 𝕌 ] ⟦ t ⟧)
  getV ⟨ _ ∣ v ∣ _ ⟩▷ = just (_ , v)
  getV ［ _ ∣ v ∣ _ ］▷ = just (_ , v)
  getV ⟨ _ ∣ v ∣ _ ⟩◁ = just (_ , v)
  getV ［ _ ∣ v ∣ _ ］◁ = just (_ , v)
  getV ⊠ = nothing

  run' : State → ℕ → Maybe (Σ[ t ∈ 𝕌 ] ⟦ t ⟧) × ℕ
  run' st n with step st
  ... | inj₁ (st' , _) = run' st' (suc n)
  ... | inj₂ stuck     = getV st , n


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.LinearCombination.Proofs
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

import      Lvl
open import Function.Equals
open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Structure.Function.Multi
import      Structure.Function.Names as Names
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Operator.Vector.LinearCombination ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Operator.Vector.Proofs
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Number
open import Syntax.Transitivity
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₗ : Lvl.Level
private variable n n₁ n₂ : ℕ
private variable i j k : 𝕟(n)
private variable vf vf₁ vf₂ : Vec(n)(V)
private variable sf sf₁ sf₂ : Vec(n)(S)

instance
  linearCombination-binaryOperator : BinaryOperator(linearCombination{n})
  linearCombination-binaryOperator = intro p where
    p : Names.Congruence₂(linearCombination{n})
    p {𝟎}       {vf₁} {vf₂} (intro vfeq) {sf₁} {sf₂} (intro sfeq) = reflexivity(_≡_)
    p {𝐒(𝟎)}    {vf₁} {vf₂} (intro vfeq) {sf₁} {sf₂} (intro sfeq) = congruence₂(_⋅ₛᵥ_) sfeq vfeq
    p {𝐒(𝐒(n))} {vf₁} {vf₂} (intro vfeq) {sf₁} {sf₂} (intro sfeq) =
      (sf₁(𝟎) ⋅ₛᵥ vf₁(𝟎)) +ᵥ linearCombination(Vec.tail vf₁) (Vec.tail sf₁) 🝖[ _≡_ ]-[ congruence₂(_+ᵥ_) (congruence₂(_⋅ₛᵥ_) sfeq vfeq) (p {𝐒(n)} (intro vfeq) (intro sfeq)) ]
      (sf₂(𝟎) ⋅ₛᵥ vf₂(𝟎)) +ᵥ linearCombination(Vec.tail vf₂) (Vec.tail sf₂) 🝖-end

instance
  linearCombination-scalar-preserves-[+] : Preserving₂(linearCombination vf) (Vec.map₂(_+ₛ_)) (_+ᵥ_)
  linearCombination-scalar-preserves-[+] {vf = vf} = intro(p{vf = vf}) where
    p : ∀{n}{vf : Vec(n)(V)} → Names.Preserving₂(linearCombination vf) (Vec.map₂(_+ₛ_)) (_+ᵥ_)
    p {𝟎}{vf} {sf₁} {sf₂} =
      𝟎ᵥ       🝖[ _≡_ ]-[ identityₗ(_+ᵥ_)(𝟎ᵥ) ]-sym
      𝟎ᵥ +ᵥ 𝟎ᵥ 🝖-end
    p {𝐒(𝟎)}{vf} {sf₁} {sf₂} =
      (Vec.map₂(_+ₛ_) sf₁ sf₂ 𝟎) ⋅ₛᵥ vf(𝟎)     🝖[ _≡_ ]-[]
      (sf₁(𝟎) +ₛ sf₂(𝟎)) ⋅ₛᵥ vf(𝟎)             🝖[ _≡_ ]-[ [⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ ]
      (sf₁(𝟎) ⋅ₛᵥ vf(𝟎)) +ᵥ (sf₂(𝟎) ⋅ₛᵥ vf(𝟎)) 🝖-end
    p {𝐒(𝐒(n))}{vf} {sf₁} {sf₂} =
      ((Vec.map₂(_+ₛ_) sf₁ sf₂ 𝟎) ⋅ₛᵥ vf(𝟎)) +ᵥ (linearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail(Vec.map₂(_+ₛ_) sf₁ sf₂)))                                                🝖[ _≡_ ]-[]
      ((sf₁(𝟎) +ₛ sf₂(𝟎)) ⋅ₛᵥ vf(𝟎)) +ᵥ (linearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail(Vec.map₂(_+ₛ_) sf₁ sf₂)))                                                        🝖[ _≡_ ]-[ congruence₂(_+ᵥ_) [⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ (p {𝐒(n)}{Vec.tail vf} {Vec.tail sf₁} {Vec.tail sf₂}) ]
      ((sf₁(𝟎) ⋅ₛᵥ vf(𝟎)) +ᵥ (sf₂(𝟎) ⋅ₛᵥ vf(𝟎))) +ᵥ ((linearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail sf₁)) +ᵥ (linearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail sf₂)))   🝖[ _≡_ ]-[ One.associate-commute4 (commutativity(_+ᵥ_)) ]
      (((sf₁(𝟎) ⋅ₛᵥ vf(𝟎)) +ᵥ (linearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail sf₁))) +ᵥ ((sf₂(𝟎) ⋅ₛᵥ vf(𝟎)) +ᵥ (linearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail sf₂)))) 🝖-end

instance
  linearCombination-scalar-preserves-[⋅] : ∀{s} → Preserving₁(linearCombination vf) (Vec.map(s ⋅ₛ_)) (s ⋅ₛᵥ_)
  linearCombination-scalar-preserves-[⋅] {vf = vf} {s = s} = intro(p{vf = vf}) where
    p : ∀{n}{vf : Vec(n)(V)} → Names.Preserving₁(linearCombination vf) (Vec.map(s ⋅ₛ_)) (s ⋅ₛᵥ_)
    p {𝟎} {vf} {sf} =
      𝟎ᵥ       🝖[ _≡_ ]-[ [⋅ₛᵥ]-absorberᵣ ]-sym
      s ⋅ₛᵥ 𝟎ᵥ 🝖-end
    p {𝐒(𝟎)} {vf} {sf} =
      (s ⋅ₛ sf(𝟎)) ⋅ₛᵥ vf(𝟎)  🝖[ _≡_ ]-[ [⋅ₛ][⋅ₛᵥ]-compatibility ]
      s ⋅ₛᵥ (sf(𝟎) ⋅ₛᵥ vf(𝟎)) 🝖-end
    p {𝐒(𝐒(n))} {vf} {sf} =
      linearCombination vf (Vec.map (s ⋅ₛ_) sf)                                                     🝖[ _≡_ ]-[]
      ((s ⋅ₛ sf(𝟎)) ⋅ₛᵥ vf(𝟎)) +ᵥ (linearCombination (Vec.tail vf) (Vec.map (s ⋅ₛ_) (Vec.tail sf))) 🝖[ _≡_ ]-[ congruence₂(_+ᵥ_) ⦃ [+ᵥ]-binary-operator ⦄ [⋅ₛ][⋅ₛᵥ]-compatibility (p {𝐒(n)} {Vec.tail vf} {Vec.tail sf}) ]
      (s ⋅ₛᵥ (sf(𝟎) ⋅ₛᵥ vf(𝟎))) +ᵥ (s ⋅ₛᵥ (linearCombination (Vec.tail vf) (Vec.tail sf)))          🝖[ _≡_ ]-[ distributivityₗ(_⋅ₛᵥ_)(_+ᵥ_) ]-sym
      s ⋅ₛᵥ ((sf(𝟎) ⋅ₛᵥ vf(𝟎)) +ᵥ (linearCombination (Vec.tail vf) (Vec.tail sf)))                  🝖[ _≡_ ]-[]
      s ⋅ₛᵥ (linearCombination vf sf)                                                               🝖-end

-- linearCombination-of-unit : linearCombination vf (Vec.fill 𝟏ₛ) ≡ (foldᵣ(_+_) 𝟎ᵥ vf)
postulate linearCombination-of-indexProject : (linearCombination vf (Vec.indexProject i 𝟏ₛ 𝟎ₛ) ≡ vf(i))


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

module hott.equivalence.properties where

open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.isomorphism
open import function.extensionality
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.univalence
open import hott.level

sym≈ : ∀ {i j}{X : Set i}{Y : Set j}
     → X ≈ Y → Y ≈ X
sym≈ = ≅'⇒≈ ∘ sym≅' ∘ ≈⇒≅'

-- being a weak equivalence is propositional
we-h1 : ∀ {i j}{X : Set i}{Y : Set j}
      → (f : X → Y)
      → h 1 (weak-equiv f)
we-h1 f = Π-level λ _ → contr-h1 _

apply≈-inj : ∀ {i j}{X : Set i}{Y : Set j}
           → injective (apply≈ {X = X}{Y = Y})
apply≈-inj {x = (f , w)}{.f , w'} refl =
  unapΣ (refl , h1⇒prop (we-h1 f) w w')

abstract
  univ-sym≈ : ∀ {i}{X Y : Set i}
            → (w : X ≈ Y)
            → sym (≈⇒≡ w)
            ≡ ≈⇒≡ (sym≈ w)
  univ-sym≈ {i}{X}{Y} w = inverse-unique p q lem-inv
    where
      p : X ≡ Y
      p = ≈⇒≡ w

      q : Y ≡ X
      q = ≈⇒≡ (sym≈ w)

      p-β : coerce p ≡ apply≈ w
      p-β = uni-coherence w

      q-β : coerce q ≡ invert≈ w
      q-β = uni-coherence (sym≈ w)

      lem : coerce (p · q) ≡ coerce refl
      lem = coerce-hom p q
          · (ap (λ h → coerce q ∘ h) p-β
          · ap (λ h → h ∘ apply≈ w) q-β
          · funext (_≅_.iso₁ (≈⇒≅ w)))

      lem-inv : p · q ≡ refl
      lem-inv = iso⇒inj uni-iso (apply≈-inj lem)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
module FFI.Data.HaskellInt where

open import Agda.Builtin.Int using (Int)

{-# FOREIGN GHC import qualified Data.Int #-}

postulate HaskellInt : Set
{-# COMPILE GHC HaskellInt = type Data.Int.Int #-}

postulate
  intToHaskellInt : Int → HaskellInt
  haskellIntToInt : HaskellInt → Int
{-# COMPILE GHC intToHaskellInt = fromIntegral #-}
{-# COMPILE GHC haskellIntToInt = fromIntegral #-}

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-# OPTIONS -v tc.unquote:30 #-}
open import Common.Prelude
open import Common.Reflection

data Box : Bool → Set where
  box : (b : Bool) → Box b

works : (b : Bool) → Box b → Bool
works b (box .b) = unquote (give (var 0 []))

works₂ : (b : Bool) → Box b → Bool
unquoteDef works₂ = defineFun works₂ (clause
  ( arg (argInfo visible relevant) (var "b")
  ∷ arg (argInfo visible relevant) (con (quote box)
        (arg (argInfo visible relevant) dot ∷ []))
  ∷ [])
  (var 0 []) ∷ [])

works₃ : (b : Bool) → Box b → (x y : Bool) → Bool
unquoteDef works₃ = defineFun works₃ (clause
  ( arg (argInfo visible relevant) (var "b")
  ∷ arg (argInfo visible relevant) (con (quote box)
        (arg (argInfo visible relevant) dot ∷ []))
  ∷ arg (argInfo visible relevant) (var "x")
  ∷ arg (argInfo visible relevant) (var "y")
  ∷ [])
  (var 2 []) ∷ [])

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------

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

module Data.Maybe where

open import Data.Unit using (⊤)
open import Data.Empty using (⊥)
open import Data.Bool.Base using (T)
open import Data.Maybe.Relation.Unary.All
open import Data.Maybe.Relation.Unary.Any

------------------------------------------------------------------------
-- The base type and some operations

open import Data.Maybe.Base public

------------------------------------------------------------------------
-- Using Any and All to define Is-just and Is-nothing

Is-just : ∀ {a} {A : Set a} → Maybe A → Set a
Is-just = Any (λ _ → ⊤)

Is-nothing : ∀ {a} {A : Set a} → Maybe A → Set a
Is-nothing = All (λ _ → ⊥)

to-witness : ∀ {p} {P : Set p} {m : Maybe P} → Is-just m → P
to-witness (just {x = p} _) = p

to-witness-T : ∀ {p} {P : Set p} (m : Maybe P) → T (is-just m) → P
to-witness-T (just p) _  = p
to-witness-T nothing  ()


text:
module OldBasicILP.Syntax.Projection where

open import Common.UntypedContext public

import OldBasicILP.UntypedSyntax.ClosedHilbertSequential as CHS
import OldBasicILP.UntypedSyntax.ClosedHilbert as CH

-- Projection of types and derivations to a form parametrised by a closed, untyped representation of syntax.

module ClosedHilbertSequential where
  open import OldBasicILP.Syntax.ClosedHilbertSequential

  mutual
    ⌊_⌋ᵀ : Ty → CHS.Ty
    ⌊ α P ⌋ᵀ   = CHS.α P
    ⌊ A ▻ B ⌋ᵀ = ⌊ A ⌋ᵀ CHS.▻ ⌊ B ⌋ᵀ
    ⌊ p ⦂ A ⌋ᵀ = ⌊ p ⌋ᴾ CHS.⦂ ⌊ A ⌋ᵀ
    ⌊ A ∧ B ⌋ᵀ = ⌊ A ⌋ᵀ CHS.∧ ⌊ B ⌋ᵀ
    ⌊ ⊤ ⌋ᵀ    = CHS.⊤

    -- FIXME: WHat is going on here?
    postulate
      ⌊_⌋ᴾ : ∀ {Ξ A} → Proof Ξ A → CHS.Proof

    ⌊_⌋ᵀ⋆ : Cx Ty → Cx CHS.Ty
    ⌊ ∅ ⌋ᵀ⋆     = ∅
    ⌊ Γ , A ⌋ᵀ⋆ = ⌊ Γ ⌋ᵀ⋆ , ⌊ A ⌋ᵀ

    ⌊_⌋∈ : ∀ {Ξ A} → A ∈ Ξ → ⌊ A ⌋ᵀ ∈ ⌊ Ξ ⌋ᵀ⋆
    ⌊ top ⌋∈   = top
    ⌊ pop i ⌋∈ = pop ⌊ i ⌋∈

    ⌊_⌋ᴰ : ∀ {Ξ} → ⊢ᴰ Ξ → CHS.⊢ᴰ ⌊ Ξ ⌋ᵀ⋆
    ⌊ nil ⌋ᴰ      = CHS.nil
    ⌊ mp i j d ⌋ᴰ = CHS.mp ⌊ i ⌋∈ ⌊ j ⌋∈ ⌊ d ⌋ᴰ
    ⌊ ci d ⌋ᴰ     = CHS.ci ⌊ d ⌋ᴰ
    ⌊ ck d ⌋ᴰ     = CHS.ck ⌊ d ⌋ᴰ
    ⌊ cs d ⌋ᴰ     = CHS.cs ⌊ d ⌋ᴰ
    ⌊ nec `d d ⌋ᴰ = {!CHS.nec ⌊ `d ⌋ᴰ ⌊ d ⌋ᴰ!}
    ⌊ cdist d ⌋ᴰ  = {!CHS.cdist ⌊ d ⌋ᴰ!}
    ⌊ cup d ⌋ᴰ    = {!CHS.cup ⌊ d ⌋ᴰ!}
    ⌊ cdown d ⌋ᴰ  = CHS.cdown ⌊ d ⌋ᴰ
    ⌊ cpair d ⌋ᴰ  = CHS.cpair ⌊ d ⌋ᴰ
    ⌊ cfst d ⌋ᴰ   = CHS.cfst ⌊ d ⌋ᴰ
    ⌊ csnd d ⌋ᴰ   = CHS.csnd ⌊ d ⌋ᴰ
    ⌊ unit d ⌋ᴰ   = CHS.unit ⌊ d ⌋ᴰ

    ⌊_⌋ : ∀ {A} → ⊢ A → CHS.⊢ ⌊ A ⌋ᵀ
    ⌊ Ξ , d ⌋ = ⌊ Ξ ⌋ᵀ⋆ , ⌊ d ⌋ᴰ

-- Projection of types and derivations to a form parametrised by a closed, untyped representation of syntax.

module ClosedHilbert where
  open import OldBasicILP.Syntax.ClosedHilbert

  mutual
    ⌊_⌋ᵀ : Ty → CH.Ty
    ⌊ α P ⌋ᵀ   = CH.α P
    ⌊ A ▻ B ⌋ᵀ = ⌊ A ⌋ᵀ CH.▻ ⌊ B ⌋ᵀ
    ⌊ p ⦂ A ⌋ᵀ = ⌊ p ⌋ᴾ CH.⦂ ⌊ A ⌋ᵀ
    ⌊ A ∧ B ⌋ᵀ = ⌊ A ⌋ᵀ CH.∧ ⌊ B ⌋ᵀ
    ⌊ ⊤ ⌋ᵀ    = CH.⊤

    ⌊_⌋ᴾ : ∀ {A} → Proof A → CH.Proof
    ⌊ [ d ] ⌋ᴾ = CH.[ CH.ᴿ⌊ ⌊ d ⌋ ⌋ ]

    ⌊_⌋ : ∀ {A} → ⊢ A → CH.⊢ ⌊ A ⌋ᵀ
    ⌊ app d₁ d₂ ⌋ = CH.app ⌊ d₁ ⌋ ⌊ d₂ ⌋
    ⌊ ci ⌋        = CH.ci
    ⌊ ck ⌋        = CH.ck
    ⌊ cs ⌋        = CH.cs
    ⌊ box d ⌋     = CH.box ⌊ d ⌋
    ⌊ cdist ⌋     = CH.cdist
    ⌊ cup ⌋       = CH.cup
    ⌊ cdown ⌋     = CH.cdown
    ⌊ cpair ⌋     = CH.cpair
    ⌊ cfst ⌋      = CH.cfst
    ⌊ csnd ⌋      = CH.csnd
    ⌊ unit ⌋      = CH.unit


text:
-- Andreas, 2016-07-19 revisiting issue #418

module Issue418private where

open import Common.Equality

abstract

  A : Set₁
  A = Set

  private
    works : A ≡ A
    works = refl

    test : A ≡ _
    test = refl

-- Since test is private, abstract definitions are transparent in its type.
-- The meta should be solved (by A or Set).


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

open import lib.Basics
open import lib.NType2
open import lib.PathFunctor
open import lib.PathGroupoid

open import lib.types.Bool
open import lib.types.IteratedSuspension
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Suspension
open import lib.types.TLevel
open import lib.types.Unit

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim
open import nicolai.pseudotruncations.wconstSequence

module nicolai.pseudotruncations.PseudoTruncs-wconst-seq where

open import nicolai.pseudotruncations.pointed-O-Sphere
open import nicolai.pseudotruncations.LoopsAndSpheres
open import nicolai.pseudotruncations.PseudoTruncs

{- The special sequence that we consider -}
module PtruncsSeq {i} (X : Type i) where

  A : ℕ → Type i
  A O = X
  A (S n) = Pseudo n -1-trunc (A n)

  f : (n : ℕ) → A n → A (S n)
  f n x = point n -1 x

  C : Sequence {i}
  C = (A , f)

{- A main result: If we have an inhabitant of X, then the sequence is weakly constant.
   This is Lemma 6.2 ! -}
module PtruncSeqWC {i} (X : Type i) (x₀ : X) where

  open PtruncsSeq {i} X

  fs : (n : ℕ) → A n
  fs O = x₀
  fs (S n) = f n (fs n)

  P : (n : ℕ) → (x : A n) → Type i
  P n x = f n x == fs (S n)

  {- This is the easy 'Case j ≡ -2' -}
  f₀-x₀ : (y : X) → P O y
  f₀-x₀ y = (spoke O -1 r (lift false)) ∙ ! (spoke O -1 r (lift true))  where

    r : Sphere {i} O → X
    r (lift true) = x₀
    r (lift false) = y

  {- Now, the general case is done by induction on n
     (note that this variable is called 'j' in the paper).
     Hence, what is 'j' in the paper is now 'S n'.

     Unfortunately, we have to do everything in one "big"
     step with many "where" clauses due to the mutual dependencies. -}

  fₙ-x₀ : (n : ℕ) → (y : A n) → P n y
  fₙ-x₀ O y = f₀-x₀ y
  fₙ-x₀ (S n) = Pseudotrunc-ind n Point Hub Spoke where

    -- just for convenience - saves brackets
    norₙ' : Sphere' {i} n
    norₙ' = nor' n

    fⁿx₀ = fs n

    Point : (w : A n) → P (S n) (point n -1 w)
    Point w = ap (point (S n) -1) (fₙ-x₀ n w)

    Hub : (r : Sphere' n → A n) → point S n -1 _ == _
    Hub r = ap (point (S n) -1) (! (spoke n -1 r norₙ') ∙ fₙ-x₀ n (r norₙ'))

    {- The definition of [Spoke] is the hard part.
       First, we do the easy things that we have to do... -}
    Spoke : (r : _) → (x : Sphere' n) → _
    Spoke r = λ x → from-transp (P (S n))
                                (spoke n -1 r x)
                                (
      transport (P (S n)) (spoke n -1 r x) (Point (r x))
        =⟨ trans-ap₁ (f (S n)) (fs (S (S n))) (spoke n -1 r x) (Point (r x)) ⟩
      ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ Point (r x)
        =⟨ ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ₗ ! (∙-unit-r (Point (r x))) ⟩
      ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ Point (r x) ∙ idp
        {- Now comes the hard step which requires A LOT of work in the where clause
           below: we can compose with something which, for a complicated reason, is idp! -}
        =⟨ ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ₗ (Point (r x) ∙ₗ ! (k-const x)) ⟩
      ! (ap (point (S n) -1) (spoke n -1 r x)) ∙ Point (r x) ∙ k x
        {- From here, it's easy; we just have to re-associate paths and cancel inverses.
           This could be done with standard library lemmas, but it's easier to just use
           an 'ad-hoc' lemma. -}
        =⟨ multi-cancelling (ap (point S n -1) (spoke n -1 r x)) (Point (r x)) (Hub r) ⟩
      Hub r
        ∎
      )

        where

          {- Now, the actual work follows! -}

          {- First, we define the interesting loop.
             In the paper, it is called [kₓ].
             Here, it is just [k x].  -}
          k : (x : Sphere' {i} n)
              → Ω (Pseudo S n -1-trunc (A (S n)) ,
                   f (S n) (f n fⁿx₀))
          k x = ! (Point (r x)) ∙ ap (point (S n) -1) (spoke n -1 r x) ∙ (Hub r)

          {- We want to show that [k] factors as [ap pₙ ∘ h].
             First, we define h. -}
          h : Sphere' {i} n
              → Ω (Pseudo n -1-trunc (A n) ,
                   f n fⁿx₀)
          h x =   ! (fₙ-x₀ n (r x))
                ∙ (spoke n -1 r x)
                ∙ (! (spoke n -1 r norₙ') ∙ fₙ-x₀ n (r norₙ'))

          {- The statement that k == ap pₙ ∘ h: -}
          k-p-h : k == ap (point S n -1) ∘ h
          k-p-h = λ= (λ (x : Sphere' {i} n)
                     → k x
                         =⟨ idp ⟩
                         ! (Point (r x))
                       ∙ (ap (point (S n) -1) (spoke n -1 r x) ∙ (Hub r))
                         =⟨ !-ap (point S n -1) (fₙ-x₀ n (r x))
                                ∙ᵣ (  ap (point S n -1) (spoke n -1 r x)
                                    ∙ Hub r) ⟩
                         ap (point (S n) -1) (! (fₙ-x₀ n (r x)))
                       ∙ ap (point (S n) -1) (spoke n -1 r x)
                       ∙ (Hub r)
                         =⟨ ! (ap (point (S n) -1) (! (fₙ-x₀ n (r x)))
                                ∙ₗ ap-∙ point S n -1
                                        (spoke n -1 r x)
                                        _ ) ⟩
                         ap (point (S n) -1) (! (fₙ-x₀ n (r x)))
                       ∙ ap (point (S n) -1)
                            (  spoke n -1 r x
                             ∙ (! (spoke n -1 r norₙ')
                             ∙ fₙ-x₀ n (r norₙ')))
                         =⟨ ! (ap-∙ point S n -1 (! (fₙ-x₀ n (r x))) _) ⟩
                       ap (point S n -1) (h x)
                         ∎)

          {- [h] can be made into a a pointed map, written [ĥ] -}
          ĥ : (⊙Sphere' {i} n)
                 →̇ ⊙Ω (A (S n) ,
                      f n fⁿx₀)
          ĥ = h ,
                  (! (fₙ-x₀ n (r _))
                ∙ (spoke n -1 r _)
                ∙ ! (spoke n -1 r norₙ')
                ∙ fₙ-x₀ n (r norₙ')

                  =⟨ (! (fₙ-x₀ n (r _)))
                      ∙ₗ (! (∙-assoc (spoke n -1 r _)
                                     (! (spoke n -1 r norₙ'))
                                     (fₙ-x₀ n (r norₙ')))) ⟩

                ! (fₙ-x₀ n (r _))
                ∙ ((spoke n -1 r _) ∙ (! (spoke n -1 r norₙ')))
                ∙ fₙ-x₀ n (r norₙ')

                  =⟨ ! (fₙ-x₀ n (r _))
                     ∙ₗ !-inv-r (spoke n -1 r _)
                     ∙ᵣ fₙ-x₀ n (r norₙ') ⟩

                ! (fₙ-x₀ n (r _))
                ∙ idp
                ∙ fₙ-x₀ n (r norₙ')

                  =⟨ !-inv-l (fₙ-x₀ n (r _)) ⟩

                idp

                  ∎ )

          {- A pointed version of the first constructor. -}
          pointsₙ : (A (S n) , f n fⁿx₀) →̇ A (S (S n)) , f (S n) (f n fⁿx₀)
          pointsₙ = point S n -1 , idp

          open null
          open hom-adjoint

          points-Φ⁻¹-null : isNull∙ (pointsₙ ⊙∘ Φ⁻¹ _ _ ĥ)
          points-Φ⁻¹-null = <– (isNull-equiv (pointsₙ ⊙∘ Φ⁻¹ _ _ ĥ))
                            -- translate from isNull∙'
                                 (null-lequiv (pointsₙ ⊙∘ Φ⁻¹ _ _ ĥ)
                                 -- translate from isNulld; this,
                                 -- we have done already!
                                    (cmp-nll'.from-sphere-null'∙ n (Φ⁻¹ _ _ ĥ)))

          ap-points-ĥ-null : isNull∙ (⊙ap (point S n -1 , idp) ⊙∘ ĥ)
          ap-points-ĥ-null = –> (combine-isnull-nat' ĥ (point S n -1 , idp)) points-Φ⁻¹-null

          {- ... consequently, h is always refl [in the library "idp"]: -}
          points-h-const : (x : Sphere' n) → ap (point S n -1) (h x) == idp
          points-h-const x = null-lequiv-easy _ ap-points-ĥ-null x

          {- ... and so is k: -}
          k-const : (x : Sphere' n) → k x == idp
          k-const x = app= k-p-h x  ∙ points-h-const x

  {- Main result: each function in the sequence is propositional! -}
  wconst-f : wconst-chain C
  wconst-f n w₁ w₂ = fₙ-x₀ n w₁ ∙ ! (fₙ-x₀ n w₂)

{- Another important result:
   if we want to show a proposition, we can assume A₀ instead of Aω
   But this should follow from the general induction principle, so... TODO
-}
module PtruncSeqResult' {i} (X : Type i) where

  open PtruncsSeq {i} X -- this defines the chain C of pseudo-truncations

  SC = SeqCo C

  reduction-lemma : (P : Type i) → (is-prop P) → (A O → P) → (SC → P)
  reduction-lemma P ip ff = SeqCo-rec {C = C} {B = P} Ins Glue where

    Ins : (n : ℕ) → A n → P
    Ins O = ff
    Ins (S n) = Pseudotrunc-rec {P = P} n Point-1 Hub-1 Spoke-1 where
      Point-1 : _ → P
      Point-1 x = Ins n x
      Hub-1 : (Sphere' n → A n) → P
      Hub-1 r = Ins n (r (nor' n))
      Spoke-1 : (r : Sphere' n → A n) (x : Sphere' n) → Point-1 (r x) == Hub-1 r
      Spoke-1 r x = prop-has-all-paths {A = P} ip _ _

    Glue : (n : ℕ) (a : A n) → Ins n a == Ins (S n) (f n a)
    Glue n a = prop-has-all-paths ip _ _

{- Corollary of the main result: The colimit of the considered sequence is propositional! -}
module PtruncSeqResult {i} (X : Type i) where

  open PtruncsSeq {i} X -- this defines the chain C of pseudo-truncations

  colim-is-prp : is-prop (SeqCo C)
  colim-is-prp =
    inhab-to-contr-is-prop
      (PtruncSeqResult'.reduction-lemma X (is-contr (SeqCo C)) has-level-is-prop
        (λ x₀ → ins O x₀ , prop-has-all-paths (wconst-prop C (PtruncSeqWC.wconst-f X x₀))
          (ins O x₀)))

  open PtruncSeqResult' X

  {- If we have the propositional truncation in the theory: -}
  open import lib.types.Truncation

  colim-is-trunc : (Trunc ⟨-1⟩ X) ≃ SeqCo C
  colim-is-trunc = equiv (Trunc-rec (colim-is-prp) (ins 0))
                         (reduction-lemma (Trunc ⟨-1⟩ X) Trunc-level [_])
                         (λ _ → prop-has-all-paths colim-is-prp _ _)
                         (λ _ → prop-has-all-paths Trunc-level _ _)

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Categories.Category
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Closed

module Categories.Category.Monoidal.Closed.IsClosed.Pentagon
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (Cl : Closed M) where

open import Data.Product using (Σ; _,_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality as Π using (Π)

open import Categories.Category.Product
open import Categories.Category.Monoidal.Properties M
open import Categories.Morphism C
open import Categories.Morphism.Properties C
open import Categories.Morphism.Reasoning C
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Dinatural hiding (_∘ʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism as NI hiding (refl)
import Categories.Category.Closed as Cls

open Closed Cl

private
  module C = Category C
  open Category C
  open Commutation
  module ℱ = Functor
  module ⊗ = Functor ⊗
  α⇒ = associator.from
  α⇐ = associator.to
  λ⇒ = unitorˡ.from
  λ⇐ = unitorˡ.to
  ρ⇒ = unitorʳ.from
  ρ⇐ = unitorʳ.to

open HomReasoning
open Π.Π
open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
 Ladjunct-resp-≈ to 𝕃-resp-≈)

open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl
open import Categories.Category.Monoidal.Closed.IsClosed.L Cl

-- some intermediate steps as lemmas

private
-- ⊗.F₀ (⊗.F₀ ([-,-].F₀ (u , v) , [-,-].F₀ (x , u)) , x) ⇒ v
  inner : {x : Obj} (v u : Obj) → ((Functor.F₀ [ u ,-] v) ⊗₀ (Functor.F₀ [ x ,-] u) ) ⊗₀ x ⇒ v
  inner {x} v u = ε.η v ∘ id ⊗₁ ε.η {x} u ∘ α⇒

  VU-UY⇒VY-VU : {U V X Y : Obj} → inner {X} V U ∘ (id ⊗₁ 𝕃 (inner U Y) ∘ α⇒) ⊗₁ id ≈
                          inner V Y ∘ (𝕃 (inner V U) ⊗₁ id) ⊗₁ id
  VU-UY⇒VY-VU {U} {V} {X} {Y} = begin
    inner V U ∘ (id ⊗₁ 𝕃 (inner U Y) ∘ α⇒) ⊗₁ id                        ≈⟨ pushʳ $ ℱ.homomorphism (-⊗ X) ⟩
    (inner V U ∘ (id ⊗₁ 𝕃 (inner U Y)) ⊗₁ id) ∘ α⇒ ⊗₁ id                ≈⟨ pull-last assoc-commute-from ⟩∘⟨refl ⟩
    (ε.η V ∘ id ⊗₁ ε.η U ∘ id ⊗₁ 𝕃 (inner U Y) ⊗₁ id ∘ α⇒) ∘ α⇒ ⊗₁ id   ≈⟨ (∘-resp-≈ʳ $ pullˡ $ ⟺ (ℱ.homomorphism ([ U , V ]₀ ⊗-))) ⟩∘⟨refl ⟩
    (ε.η V ∘ id ⊗₁ (ε.η U ∘ 𝕃 (inner U Y) ⊗₁ id) ∘ α⇒) ∘ α⇒ ⊗₁ id       ≈⟨ ∘-resp-≈ˡ (⟺ assoc) ○ assoc ⟩
    (ε.η V ∘ id ⊗₁ (ε.η U ∘ 𝕃 (inner U Y) ⊗₁ id)) ∘ (α⇒ ∘ α⇒ ⊗₁ id)     ≈⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ ℱ.F-resp-≈ ([ U , V ]₀ ⊗-) (RLadjunct≈id ○ ⟺ assoc) ⟩
    (ε.η V ∘ id ⊗₁ ((ε.η U ∘ id ⊗₁ ε.η Y) ∘ α⇒)) ∘ (α⇒ ∘ α⇒ ⊗₁ id)      ≈⟨ ∘-resp-≈ˡ $ ∘-resp-≈ʳ $ ℱ.homomorphism ([ U , V ]₀ ⊗-) ⟩
    (ε.η V ∘ id ⊗₁ (ε.η U ∘ id ⊗₁ ε.η Y) ∘ id ⊗₁ α⇒) ∘ (α⇒ ∘ α⇒ ⊗₁ id)  ≈⟨ pull-last refl ⟩
    ε.η V ∘ id ⊗₁ (ε.η U ∘ id ⊗₁ ε.η Y) ∘ (id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id)    ≈⟨ refl⟩∘⟨ ∘-resp-≈ (ℱ.homomorphism ([ U , V ]₀ ⊗-)) pentagon ⟩
    ε.η V ∘ (id ⊗₁ ε.η U ∘ id ⊗₁ (id ⊗₁ ε.η Y)) ∘ (α⇒ ∘ α⇒)             ≈⟨ ⟺ assoc ○ ⟺ assoc ⟩
    ((ε.η V ∘ id ⊗₁ ε.η U ∘ id ⊗₁ (id ⊗₁ ε.η Y)) ∘ α⇒) ∘ α⇒             ≈⟨ pull-last (⟺ assoc-commute-from) ⟩∘⟨refl ⟩
    (ε.η V ∘ id ⊗₁ ε.η U ∘ α⇒ ∘ (id ⊗₁ id) ⊗₁ ε.η Y) ∘ α⇒                ≈⟨ assoc ○ ∘-resp-≈ʳ (∘-resp-≈ˡ (⟺ assoc)) ○ ⟺ (center refl) ⟩
    (ε.η V ∘ id ⊗₁ ε.η U ∘ α⇒) ∘ (id ⊗₁ id) ⊗₁ ε.η Y ∘ α⇒                ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ⊗.F-resp-≈ (⊗.identity , refl) ⟩
    (ε.η V ∘ id ⊗₁ ε.η U ∘ α⇒) ∘ id ⊗₁ ε.η Y ∘ α⇒                        ≈˘⟨ center⁻¹ RLadjunct≈id refl ⟩
    ε.η V ∘ (𝕃 (ε.η V ∘ id ⊗₁ ε.η U ∘ α⇒) ⊗₁ id ∘ id ⊗₁ ε.η Y) ∘ α⇒      ≈⟨ ∘-resp-≈ʳ $ pushˡ (⟺ [ ⊗ ]-commute) ⟩
    ε.η V ∘ id ⊗₁ ε.η Y ∘ 𝕃 (inner V U) ⊗₁ id ∘ α⇒                       ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.F-resp-≈ (refl , ⊗.identity) ⟩∘⟨refl ⟩
    ε.η V ∘ id ⊗₁ ε.η Y ∘ 𝕃 (inner V U) ⊗₁ (id ⊗₁ id) ∘ α⇒               ≈˘⟨ pull-last assoc-commute-from ⟩
    (inner V Y) ∘ (𝕃 (inner V U) ⊗₁ id) ⊗₁ id                             ∎

  expand-[-,-] : {U V X Y : Obj} →
      (ε.η [ X , V ]₀ ∘ id ⊗₁ ε.η [ X , U ]₀ ∘ α⇒) ∘ (L X U V ⊗₁ L X Y U) ⊗₁ id ≈
      𝕃 (ε.η V ∘ id ⊗₁ ε.η Y ∘ α⇒) ∘ 𝕃 (ε.η V ∘ id ⊗₁ ε.η U ∘ α⇒) ⊗₁ id
  expand-[-,-] {U} {V} {X} {Y} = begin
    (inner XV XU) ∘ (L X U V ⊗₁ L X Y U) ⊗₁ id                        ≈⟨ pull-last assoc-commute-from ⟩
    ε.η XV ∘ id ⊗₁ ε.η XU ∘ L X U V ⊗₁ L X Y U ⊗₁ id ∘ α⇒             ≈⟨ refl⟩∘⟨ pullˡ (⟺ ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , refl)) ⟩
    ε.η XV ∘ L X U V ⊗₁ (ε.η XU ∘ L X Y U ⊗₁ id) ∘ α⇒                 ≈⟨ refl⟩∘⟨ [ ⊗ ]-decompose₁ ⟩∘⟨refl ⟩
    ε.η XV ∘ (L X U V ⊗₁ id ∘ id ⊗₁ (ε.η XU ∘ L X Y U ⊗₁ id)) ∘ α⇒    ≈⟨ center⁻¹ RLadjunct≈id (∘-resp-≈ˡ (ℱ.F-resp-≈ ([ U , V ]₀ ⊗-) RLadjunct≈id)) ⟩
    𝕃 (inner V U) ∘ (id ⊗₁ 𝕃 (inner U Y) ∘ α⇒)                         ≈˘⟨ 𝕃-comm′ ⟩
    𝕃 (inner V U ∘ (id ⊗₁ 𝕃 (inner U Y) ∘ α⇒) ⊗₁ id)                   ≈⟨ 𝕃-resp-≈ VU-UY⇒VY-VU ⟩
    𝕃 (inner V Y ∘ (𝕃 (inner V U) ⊗₁ id) ⊗₁ id)                        ≈⟨ 𝕃-comm′ ⟩
    𝕃 (inner V Y) ∘ 𝕃 (inner V U) ⊗₁ id ∎
    where
    XV = [ X , V ]₀
    XU = [ X , U ]₀
    UV = [ U , V ]₀

pentagon′ : {U V X Y : Obj} →
            [ [ U , V ]₀ ⇒ [ [ Y , U ]₀ , [ [ X , Y ]₀ , [ X , V ]₀ ]₀ ]₀ ]⟨
             L X U V                            ⇒⟨ [ [ X , U ]₀ , [ X , V ]₀ ]₀ ⟩
             L [ X , Y ]₀ [ X , U ]₀ [ X , V ]₀ ⇒⟨ [ [ [ X , Y ]₀ , [ X , U ]₀ ]₀ , [ [ X , Y ]₀ , [ X , V ]₀ ]₀ ]₀ ⟩
             [ L X Y U , id ]₁
           ≈ L Y U V                            ⇒⟨ [ [ Y , U ]₀ , [ Y , V ]₀ ]₀ ⟩
             [ id , L X Y V ]₁
           ⟩
pentagon′ {U} {V} {X} {Y} = begin
  [ L X Y U , id ]₁ ∘ L [ X , Y ]₀ XU XV ∘ L X U V                               ≈˘⟨ refl ⟩∘⟨ 𝕃-comm′ ⟩
  [ L X Y U , id ]₁ ∘ 𝕃 (𝕃 (ε.η XV ∘ id ⊗₁ ε.η XU ∘ α⇒) ∘ L X U V ⊗₁ id)        ≈˘⟨ pushˡ [ [-,-] ]-commute ⟩
  ([ id , 𝕃 (inner XV XU) ∘ L X U V ⊗₁ id ]₁ ∘ [ L X Y U , id ]₁) ∘ η.η UV       ≈˘⟨ pushʳ (mate.commute₁ (L X Y U)) ⟩
  [ id , 𝕃 (inner XV XU) ∘ L X U V ⊗₁ id ]₁ ∘ [ id , id ⊗₁ L X Y U ]₁ ∘ η.η UV   ≈˘⟨ pushˡ (ℱ.homomorphism [ [ Y , U ]₀ ,-]) ⟩
  𝕃 ((𝕃 (inner XV XU) ∘ L X U V ⊗₁ id) ∘ id ⊗₁ L X Y U)                          ≈˘⟨ 𝕃-resp-≈ $ pushʳ [ ⊗ ]-decompose₁ ⟩
  𝕃 (𝕃 (inner XV XU) ∘ L X U V ⊗₁ L X Y U)                                       ≈˘⟨ 𝕃-resp-≈ $ 𝕃-comm′ ⟩
  𝕃 (𝕃 $ (inner XV XU) ∘ (L X U V ⊗₁ L X Y U) ⊗₁ id)                             ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ $ expand-[-,-] ⟩
  𝕃 (𝕃 $ 𝕃 (inner V Y) ∘ 𝕃 (inner V U) ⊗₁ id)                                    ≈⟨ 𝕃-resp-≈ 𝕃-comm′ ⟩
  𝕃 (L X Y V ∘ 𝕃 (inner V U))                                                     ≈⟨ pushˡ (ℱ.homomorphism [ [ Y , U ]₀ ,-]) ⟩
  [ id , L X Y V ]₁ ∘ L Y U V                                                     ∎
  where
  XV = [ X , V ]₀
  XU = [ X , U ]₀
  UV = [ U , V ]₀

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
-- Andreas, 2019-06-17, LAIM 2019, issue #3855
-- Only allow erased definitions (such as projections of erased fields)
-- in erased context.

open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Bool

record Erased (A : Set) : Set where
  constructor erase
  field
    @0 gone : A

noWorld : Bool → Erased String
noWorld true  = erase "Hello world!"
noWorld false = erase "Hallo, Welt!"

-- Illegal definition, should raise a type error.

unerase : ∀{A : Set} → Erased A → A
unerase = Erased.gone

main = putStrLn (unerase (noWorld false))

-- WAS: type checker let it through, compiler produces ill-formed Haskell


text:
module Structure.Relator.Apartness.Proofs where

open import Data
open import Data.Either as Either
open import Data.Tuple as Tuple
open import Functional
open import Logic.Classical
open import Logic.Propositional
open import Logic.Propositional.Theorems
import      Lvl
open import Structure.Relator.Apartness
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Syntax.Implication
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ ℓₗ₄ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level
private variable T A B : Type{ℓ}
private variable _▫_ : T → T → Type{ℓ}

module _ {_▫_ : T → T → Type{ℓ}} where
  instance
    -- The negation of an apartness relation is an equivalence relation.
    -- This is a reason for using an apartness relation in constructive real mathematics. Both the apartness properties and the equivalence properties are sought after and by starting with an apartness relation, one gets both.
    apartness-equivalenceᵣ : ⦃ apart : Apartness(_▫_) ⦄ → Equivalence((¬_) ∘₂ (_▫_))
    Reflexivity.proof  (Equivalence.reflexivity  apartness-equivalenceᵣ) = irreflexivity(_▫_)
    Symmetry.proof     (Equivalence.symmetry     apartness-equivalenceᵣ) = contrapositiveᵣ(symmetry(_▫_))
    Transitivity.proof (Equivalence.transitivity apartness-equivalenceᵣ) nxy nyz = [∨]-elim nxy nyz ∘ cotransitivity(_▫_)

  module _ ⦃ classical : Classical₂(_▫_) ⦄ where
    equivalence-apartnessᵣ : ⦃ equi : Equivalence(_▫_) ⦄ → Apartness((¬_) ∘₂ (_▫_))
    Irreflexivity.proof  (Apartness.irreflexivity  equivalence-apartnessᵣ) = [¬¬]-intro (reflexivity(_▫_))
    Symmetry.proof       (Apartness.symmetry       equivalence-apartnessᵣ) = contrapositiveᵣ(symmetry(_▫_))
    CoTransitivity.proof (Apartness.cotransitivity equivalence-apartnessᵣ) {x}{y}{z} nxz with excluded-middle(x ▫ y) | excluded-middle(y ▫ z)
    ... | Left  xy  | Left  yz  with () ← nxz(transitivity(_▫_) xy yz)
    ... | Left  xy  | Right nyz = [∨]-introᵣ nyz
    ... | Right nxy | Left  yz  = [∨]-introₗ nxy
    ... | Right nxy | Right nyz = [∨]-introₗ nxy

    equivalence-apartnessₗ : ⦃ apart : Apartness((¬_) ∘₂ (_▫_)) ⦄ → Equivalence(_▫_)
    Reflexivity.proof  (Equivalence.reflexivity equivalence-apartnessₗ) = [¬¬]-elim(irreflexivity((¬_) ∘₂ (_▫_)))
    Symmetry.proof     (Equivalence.symmetry equivalence-apartnessₗ) = contrapositiveₗ(symmetry((¬_) ∘₂ (_▫_)))
    Transitivity.proof (Equivalence.transitivity equivalence-apartnessₗ) {x}{y}{z} xy yz with excluded-middle(x ▫ z)
    ... | Left xz   = xz
    ... | Right nxz with cotransitivity((¬_) ∘₂ (_▫_)) nxz
    ... |   Left  nxy with () ← nxy xy
    ... |   Right nyz with () ← nyz yz

    apartness-equivalenceₗ : ⦃ equi : Equivalence((¬_) ∘₂ (_▫_)) ⦄ → Apartness(_▫_)
    Irreflexivity.proof (Apartness.irreflexivity apartness-equivalenceₗ) = reflexivity((¬_) ∘₂ (_▫_))
    Symmetry.proof (Apartness.symmetry apartness-equivalenceₗ) = contrapositiveₗ(symmetry((¬_) ∘₂ (_▫_)))
    CoTransitivity.proof (Apartness.cotransitivity apartness-equivalenceₗ) {x}{y}{z} =
      (x ▫ z)                ⇒-[ [¬¬]-intro ]
      ¬¬(x ▫ z)              ⇒-[ contrapositiveᵣ(uncurry(transitivity((¬_) ∘₂ (_▫_)))) ]
      ¬(¬(x ▫ y) ∧ ¬(y ▫ z)) ⇒-[ [¬]-preserves-[∧][∨]ᵣ ]
      ¬¬(x ▫ y) ∨ ¬¬(y ▫ z)  ⇒-[ Either.map [¬¬]-elim [¬¬]-elim ]
      (x ▫ y) ∨ (y ▫ z)      ⇒-end