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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Pi {{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 using (_∷_⊆_)
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Introductions.Universe

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

-- Validity of Π.
Πᵛ : ∀ {F G Γ l}
     ([Γ] : ⊩ᵛ Γ)
     ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
   → Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F])
   → Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G / [Γ]
Πᵛ {F} {G} {Γ} {l} [Γ] [F] [G] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [F]σ {σ′} [σ′] = [F] {σ = σ′} ⊢Δ [σ′]
      [σF] = proj₁ ([F]σ [σ])
      ⊢F {σ′} [σ′] = escape (proj₁ ([F]σ {σ′} [σ′]))
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      [G]σ {σ′} [σ′] = [G] {σ = liftSubst σ′} (⊢Δ ∙ ⊢F [σ′])
                           (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ′])
      ⊢G {σ′} [σ′] = escape (proj₁ ([G]σ {σ′} [σ′]))
      ⊢G≡G = escapeEq (proj₁ ([G]σ [σ])) (reflEq (proj₁ ([G]σ [σ])))
      ⊢ΠF▹G = Πⱼ ⊢F [σ] ▹ ⊢G [σ]
      [G]a : ∀ {ρ Δ₁} a ([ρ] : ρ ∷ Δ₁ ⊆ Δ) (⊢Δ₁ : ⊢ Δ₁)
             ([a] : Δ₁ ⊩⟨ l ⟩ a ∷ subst (ρ •ₛ σ) F
                / proj₁ ([F] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ])))
           → Σω₀ (Δ₁ ⊩⟨ l ⟩ subst (consSubst (ρ •ₛ σ) a) G)
               (λ [Aσ] →
               {σ′ : Nat → Term} →
               (Σω₂ (Δ₁ ⊩ˢ tail σ′ ∷ Γ / [Γ] / ⊢Δ₁)
               (λ [tailσ] →
                  Δ₁ ⊩⟨ l ⟩ head σ′ ∷ subst (tail σ′) F / proj₁ ([F] ⊢Δ₁ [tailσ]))) →
               Δ₁ ⊩ˢ consSubst (ρ •ₛ σ) a ≡ σ′ ∷ Γ ∙ F /
               [Γ] ∙″ [F] / ⊢Δ₁ /
               consSubstS {t = a} {A = F} [Γ] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]) [F]
               [a] →
               Δ₁ ⊩⟨ l ⟩ subst (consSubst (ρ •ₛ σ) a) G ≡
               subst σ′ G / [Aσ])
      [G]a {ρ} a [ρ] ⊢Δ₁ [a] = ([G] {σ = consSubst (ρ •ₛ σ) a} ⊢Δ₁
                              (consSubstS {t = a} {A = F} [Γ] ⊢Δ₁
                                          (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ])
                                          [F] [a]))
      [G]a′ : ∀ {ρ Δ₁} a ([ρ] : ρ ∷ Δ₁ ⊆ Δ) (⊢Δ₁ : ⊢ Δ₁)
            → Δ₁ ⊩⟨ l ⟩ a ∷ subst (ρ •ₛ σ) F
                 / proj₁ ([F] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]))
            → Δ₁ ⊩⟨ l ⟩ U.wk (lift ρ) (subst (liftSubst σ) G) [ a ]
      [G]a′ a ρ ⊢Δ₁ [a] = irrelevance′ (PE.sym (singleSubstWkComp a σ G))
                                   (proj₁ ([G]a a ρ ⊢Δ₁ [a]))
  in Πᵣ′ (subst σ F) (subst (liftSubst σ) G)
         (idRed:*: ⊢ΠF▹G) (⊢F [σ]) (⊢G [σ]) (≅-Π-cong (⊢F [σ]) ⊢F≡F ⊢G≡G)
         (λ ρ ⊢Δ₁ → wk ρ ⊢Δ₁ [σF])
         (λ {ρ} {Δ₁} {a} [ρ] ⊢Δ₁ [a] →
            let [a]′ = irrelevanceTerm′
                         (wk-subst F) (wk [ρ] ⊢Δ₁ [σF])
                         (proj₁ ([F] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]))) [a]
            in  [G]a′ a [ρ] ⊢Δ₁ [a]′)
         (λ {ρ} {Δ₁} {a} {b} [ρ] ⊢Δ₁ [a] [b] [a≡b] →
            let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]
                [a]′ = irrelevanceTerm′
                         (wk-subst F) (wk [ρ] ⊢Δ₁ [σF])
                         (proj₁ ([F] ⊢Δ₁ [ρσ])) [a]
                [b]′ = irrelevanceTerm′
                         (wk-subst F) (wk [ρ] ⊢Δ₁ [σF])
                         (proj₁ ([F] ⊢Δ₁ [ρσ])) [b]
                [a≡b]′ = irrelevanceEqTerm′
                           (wk-subst F) (wk [ρ] ⊢Δ₁ [σF])
                           (proj₁ ([F] ⊢Δ₁ [ρσ])) [a≡b]
            in  irrelevanceEq″
                  (PE.sym (singleSubstWkComp a σ G))
                  (PE.sym (singleSubstWkComp b σ G))
                  (proj₁ ([G]a a [ρ] ⊢Δ₁ [a]′))
                  ([G]a′ a [ρ] ⊢Δ₁ [a]′)
                  (proj₂ ([G]a a [ρ] ⊢Δ₁ [a]′)
                         ([ρσ] , [b]′)
                         (reflSubst [Γ] ⊢Δ₁ [ρσ] , [a≡b]′)))
  ,  (λ {σ′} [σ′] [σ≡σ′] →
        let var0 = var (⊢Δ ∙ ⊢F [σ])
                       (PE.subst (λ x → 0 ∷ x ∈ (Δ ∙ subst σ F))
                                 (wk-subst F) here)
            [wk1σ] = wk1SubstS [Γ] ⊢Δ (⊢F [σ]) [σ]
            [wk1σ′] = wk1SubstS [Γ] ⊢Δ (⊢F [σ]) [σ′]
            [wk1σ≡wk1σ′] = wk1SubstSEq [Γ] ⊢Δ (⊢F [σ]) [σ] [σ≡σ′]
            [F][wk1σ] = proj₁ ([F] (⊢Δ ∙ ⊢F [σ]) [wk1σ])
            [F][wk1σ′] = proj₁ ([F] (⊢Δ ∙ ⊢F [σ]) [wk1σ′])
            var0′ = conv var0
                         (≅-eq (escapeEq [F][wk1σ]
                                             (proj₂ ([F] (⊢Δ ∙ ⊢F [σ]) [wk1σ])
                                                    [wk1σ′] [wk1σ≡wk1σ′])))
        in  Π₌ _ _ (id (Πⱼ ⊢F [σ′] ▹ ⊢G [σ′]))
               (≅-Π-cong (⊢F [σ])
                       (escapeEq (proj₁ ([F] ⊢Δ [σ]))
                                    (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′]))
                       (escapeEq (proj₁ ([G]σ [σ])) (proj₂ ([G]σ [σ])
                         ([wk1σ′] , neuTerm [F][wk1σ′] (var 0) var0′ (~-var var0′))
                         ([wk1σ≡wk1σ′] , neuEqTerm [F][wk1σ]
                           (var 0) (var 0) var0 var0 (~-var var0)))))
               (λ ρ ⊢Δ₁ → wkEq ρ ⊢Δ₁ [σF] (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′]))
               (λ {ρ} {Δ₁} {a} [ρ] ⊢Δ₁ [a] →
                  let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]
                      [ρσ′] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ′]
                      [a]′ = irrelevanceTerm′ (wk-subst F) (wk [ρ] ⊢Δ₁ [σF])
                                 (proj₁ ([F] ⊢Δ₁ [ρσ])) [a]
                      [a]″ = convTerm₁ (proj₁ ([F] ⊢Δ₁ [ρσ]))
                                        (proj₁ ([F] ⊢Δ₁ [ρσ′]))
                                        (proj₂ ([F] ⊢Δ₁ [ρσ]) [ρσ′]
                                               (wkSubstSEq [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ] [σ≡σ′]))
                                        [a]′
                      [ρσa≡ρσ′a] = consSubstSEq {t = a} {A = F} [Γ] ⊢Δ₁
                                                (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ])
                                                (wkSubstSEq [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ] [σ≡σ′])
                                                [F] [a]′
                  in  irrelevanceEq″ (PE.sym (singleSubstWkComp a σ G))
                                      (PE.sym (singleSubstWkComp a σ′ G))
                                      (proj₁ ([G]a a [ρ] ⊢Δ₁ [a]′))
                                      ([G]a′ a [ρ] ⊢Δ₁ [a]′)
                                      (proj₂ ([G]a a [ρ] ⊢Δ₁ [a]′)
                                             (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ′] , [a]″)
                                             [ρσa≡ρσ′a])))

-- Validity of Π-congurence.
Π-congᵛ : ∀ {F G H E Γ l}
          ([Γ] : ⊩ᵛ Γ)
          ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
          ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
          ([H] : Γ ⊩ᵛ⟨ l ⟩ H / [Γ])
          ([E] : Γ ∙ H ⊩ᵛ⟨ l ⟩ E / ([Γ] ∙″ [H]))
          ([F≡H] : Γ ⊩ᵛ⟨ l ⟩ F ≡ H / [Γ] / [F])
          ([G≡E] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G ≡ E / [Γ] ∙″ [F] / [G])
        → Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G ≡ Π H ▹ E / [Γ] / Πᵛ {F} {G} [Γ] [F] [G]
Π-congᵛ {F} {G} {H} {E} [Γ] [F] [G] [H] [E] [F≡H] [G≡E] {σ = σ} ⊢Δ [σ] =
  let [ΠFG] = Πᵛ {F} {G} [Γ] [F] [G]
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      Πᵣ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext′ = extractMaybeEmbΠ (Π-elim [σΠFG])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      ⊢σF = escape [σF]
      [σG] = proj₁ ([G] (⊢Δ ∙ ⊢σF) (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
      ⊢σH = escape (proj₁ ([H] ⊢Δ [σ]))
      ⊢σE = escape (proj₁ ([E] (⊢Δ ∙ ⊢σH) (liftSubstS {F = H} [Γ] ⊢Δ [H] [σ])))
      ⊢σF≡σH = escapeEq [σF] ([F≡H] ⊢Δ [σ])
      ⊢σG≡σE = escapeEq [σG] ([G≡E] (⊢Δ ∙ ⊢σF) (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
  in  Π₌ (subst σ H)
         (subst (liftSubst σ) E)
         (id (Πⱼ ⊢σH ▹ ⊢σE))
         (≅-Π-cong ⊢σF ⊢σF≡σH ⊢σG≡σE)
         (λ ρ ⊢Δ₁ → let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ ρ [σ]
                    in  irrelevanceEq″ (PE.sym (wk-subst F))
                                        (PE.sym (wk-subst H))
                                        (proj₁ ([F] ⊢Δ₁ [ρσ]))
                                        ([F]′ ρ ⊢Δ₁)
                                        ([F≡H] ⊢Δ₁ [ρσ]))
         (λ {ρ} {Δ} {a} [ρ] ⊢Δ₁ [a] →
            let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]
                [a]′ = irrelevanceTerm′ (wk-subst F)
                                        ([F]′ [ρ] ⊢Δ₁)
                                        (proj₁ ([F] ⊢Δ₁ [ρσ])) [a]
                [aρσ] = consSubstS {t = a} {A = F} [Γ] ⊢Δ₁ [ρσ] [F] [a]′
            in  irrelevanceEq″ (PE.sym (singleSubstWkComp a σ G))
                                (PE.sym (singleSubstWkComp a σ E))
                                (proj₁ ([G] ⊢Δ₁ [aρσ]))
                                ([G]′ [ρ] ⊢Δ₁ [a])
                                ([G≡E] ⊢Δ₁ [aρσ]))

-- Validity of Π as a term.
Πᵗᵛ : ∀ {F G Γ} ([Γ] : ⊩ᵛ Γ)
      ([F] : Γ ⊩ᵛ⟨ ¹ ⟩ F / [Γ])
      ([U] : Γ ∙ F ⊩ᵛ⟨ ¹ ⟩ U / ([Γ] ∙″ [F]))
    → Γ ⊩ᵛ⟨ ¹ ⟩ F ∷ U / [Γ] / Uᵛ [Γ]
    → Γ ∙ F ⊩ᵛ⟨ ¹ ⟩ G ∷ U / [Γ] ∙″ [F] / (λ {Δ} {σ} → [U] {Δ} {σ})
    → Γ ⊩ᵛ⟨ ¹ ⟩ Π F ▹ G ∷ U / [Γ] / Uᵛ [Γ]
Πᵗᵛ {F} {G} {Γ} [Γ] [F] [U] [Fₜ] [Gₜ] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [liftσ] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]
      ⊢F = escape (proj₁ ([F] ⊢Δ [σ]))
      ⊢Fₜ = escapeTerm (Uᵣ′ ⁰ 0<1 ⊢Δ) (proj₁ ([Fₜ] ⊢Δ [σ]))
      ⊢F≡Fₜ = escapeTermEq (Uᵣ′ ⁰ 0<1 ⊢Δ)
                               (reflEqTerm (Uᵣ′ ⁰ 0<1 ⊢Δ) (proj₁ ([Fₜ] ⊢Δ [σ])))
      ⊢Gₜ = escapeTerm (proj₁ ([U] (⊢Δ ∙ ⊢F) [liftσ]))
                           (proj₁ ([Gₜ] (⊢Δ ∙ ⊢F) [liftσ]))
      ⊢G≡Gₜ = escapeTermEq (proj₁ ([U] (⊢Δ ∙ ⊢F) [liftσ]))
                               (reflEqTerm (proj₁ ([U] (⊢Δ ∙ ⊢F) [liftσ]))
                                           (proj₁ ([Gₜ] (⊢Δ ∙ ⊢F) [liftσ])))
      [F]₀ = univᵛ {F} [Γ] (Uᵛ [Γ]) [Fₜ]
      [Gₜ]′ = S.irrelevanceTerm {A = U} {t = G}
                                (_∙″_ {A = F} [Γ] [F]) (_∙″_ {A = F} [Γ] [F]₀)
                                (λ {Δ} {σ} → [U] {Δ} {σ})
                                (λ {Δ} {σ} → Uᵛ (_∙″_ {A = F} [Γ] [F]₀) {Δ} {σ})
                                [Gₜ]
      [G]₀ = univᵛ {G} (_∙″_ {A = F} [Γ] [F]₀)
                   (λ {Δ} {σ} → Uᵛ (_∙″_ {A = F} [Γ] [F]₀) {Δ} {σ})
                   (λ {Δ} {σ} → [Gₜ]′ {Δ} {σ})
      [ΠFG] = (Πᵛ {F} {G} [Γ] [F]₀ [G]₀) ⊢Δ [σ]
  in  Uₜ (Π subst σ F ▹ subst (liftSubst σ) G) (idRedTerm:*: (Πⱼ ⊢Fₜ ▹ ⊢Gₜ))
         Πₙ (≅ₜ-Π-cong ⊢F ⊢F≡Fₜ ⊢G≡Gₜ) (proj₁ [ΠFG])
  ,   (λ {σ′} [σ′] [σ≡σ′] →
         let [liftσ′] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ′]
             [wk1σ] = wk1SubstS [Γ] ⊢Δ ⊢F [σ]
             [wk1σ′] = wk1SubstS [Γ] ⊢Δ ⊢F [σ′]
             var0 = conv (var (⊢Δ ∙ ⊢F)
                         (PE.subst (λ x → 0 ∷ x ∈ (Δ ∙ subst σ F))
                                   (wk-subst F) here))
                    (≅-eq (escapeEq (proj₁ ([F] (⊢Δ ∙ ⊢F) [wk1σ]))
                                        (proj₂ ([F] (⊢Δ ∙ ⊢F) [wk1σ]) [wk1σ′]
                                               (wk1SubstSEq [Γ] ⊢Δ ⊢F [σ] [σ≡σ′]))))
             [liftσ′]′ = [wk1σ′]
                       , neuTerm (proj₁ ([F] (⊢Δ ∙ ⊢F) [wk1σ′])) (var 0)
                                 var0 (~-var var0)
             ⊢F′ = escape (proj₁ ([F] ⊢Δ [σ′]))
             ⊢Fₜ′ = escapeTerm (Uᵣ′ ⁰ 0<1 ⊢Δ) (proj₁ ([Fₜ] ⊢Δ [σ′]))
             ⊢Gₜ′ = escapeTerm (proj₁ ([U] (⊢Δ ∙ ⊢F′) [liftσ′]))
                                  (proj₁ ([Gₜ] (⊢Δ ∙ ⊢F′) [liftσ′]))
             ⊢F≡F′ = escapeTermEq (Uᵣ′ ⁰ 0<1 ⊢Δ)
                                     (proj₂ ([Fₜ] ⊢Δ [σ]) [σ′] [σ≡σ′])
             ⊢G≡G′ = escapeTermEq (proj₁ ([U] (⊢Δ ∙ ⊢F) [liftσ]))
                                     (proj₂ ([Gₜ] (⊢Δ ∙ ⊢F) [liftσ]) [liftσ′]′
                                            (liftSubstSEq {F = F} [Γ] ⊢Δ [F] [σ] [σ≡σ′]))
             [ΠFG]′ = (Πᵛ {F} {G} [Γ] [F]₀ [G]₀) ⊢Δ [σ′]
         in  Uₜ₌ (Π subst σ F ▹ subst (liftSubst σ) G)
                 (Π subst σ′ F ▹ subst (liftSubst σ′) G)
                 (idRedTerm:*: (Πⱼ ⊢Fₜ ▹ ⊢Gₜ))
                 (idRedTerm:*: (Πⱼ ⊢Fₜ′ ▹ ⊢Gₜ′))
                 Πₙ Πₙ (≅ₜ-Π-cong ⊢F ⊢F≡F′ ⊢G≡G′)
                 (proj₁ [ΠFG]) (proj₁ [ΠFG]′) (proj₂ [ΠFG] [σ′] [σ≡σ′]))

-- Validity of Π-congurence as a term equality.
Π-congᵗᵛ : ∀ {F G H E Γ}
           ([Γ] : ⊩ᵛ Γ)
           ([F] : Γ ⊩ᵛ⟨ ¹ ⟩ F / [Γ])
           ([H] : Γ ⊩ᵛ⟨ ¹ ⟩ H / [Γ])
           ([UF] : Γ ∙ F ⊩ᵛ⟨ ¹ ⟩ U / ([Γ] ∙″ [F]))
           ([UH] : Γ ∙ H ⊩ᵛ⟨ ¹ ⟩ U / ([Γ] ∙″ [H]))
           ([F]ₜ : Γ ⊩ᵛ⟨ ¹ ⟩ F ∷ U / [Γ] / Uᵛ [Γ])
           ([G]ₜ : Γ ∙ F ⊩ᵛ⟨ ¹ ⟩ G ∷ U / [Γ] ∙″ [F]
                                / (λ {Δ} {σ} → [UF] {Δ} {σ}))
           ([H]ₜ : Γ ⊩ᵛ⟨ ¹ ⟩ H ∷ U / [Γ] / Uᵛ [Γ])
           ([E]ₜ : Γ ∙ H ⊩ᵛ⟨ ¹ ⟩ E ∷ U / [Γ] ∙″ [H]
                                / (λ {Δ} {σ} → [UH] {Δ} {σ}))
           ([F≡H]ₜ : Γ ⊩ᵛ⟨ ¹ ⟩ F ≡ H ∷ U / [Γ] / Uᵛ [Γ])
           ([G≡E]ₜ : Γ ∙ F ⊩ᵛ⟨ ¹ ⟩ G ≡ E ∷ U / [Γ] ∙″ [F]
                                  / (λ {Δ} {σ} → [UF] {Δ} {σ}))
         → Γ ⊩ᵛ⟨ ¹ ⟩ Π F ▹ G ≡ Π H ▹ E ∷ U / [Γ] / Uᵛ [Γ]
Π-congᵗᵛ {F} {G} {H} {E}
         [Γ] [F] [H] [UF] [UH] [F]ₜ [G]ₜ [H]ₜ [E]ₜ [F≡H]ₜ [G≡E]ₜ {Δ} {σ} ⊢Δ [σ] =
  let ⊢F = escape (proj₁ ([F] ⊢Δ [σ]))
      ⊢H = escape (proj₁ ([H] ⊢Δ [σ]))
      [liftFσ] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]
      [liftHσ] = liftSubstS {F = H} [Γ] ⊢Δ [H] [σ]
      [F]ᵤ = univᵛ {F} [Γ] (Uᵛ [Γ]) [F]ₜ
      [G]ᵤ₁ = univᵛ {G} {l′ = ⁰} (_∙″_ {A = F} [Γ] [F])
                    (λ {Δ} {σ} → [UF] {Δ} {σ}) [G]ₜ
      [G]ᵤ = S.irrelevance {A = G} (_∙″_ {A = F} [Γ] [F])
                           (_∙″_ {A = F} [Γ] [F]ᵤ) [G]ᵤ₁
      [H]ᵤ = univᵛ {H} [Γ] (Uᵛ [Γ]) [H]ₜ
      [E]ᵤ = S.irrelevance {A = E} (_∙″_ {A = H} [Γ] [H]) (_∙″_ {A = H} [Γ] [H]ᵤ)
                           (univᵛ {E} {l′ = ⁰} (_∙″_ {A = H} [Γ] [H])
                                  (λ {Δ} {σ} → [UH] {Δ} {σ}) [E]ₜ)
      [F≡H]ᵤ = univEqᵛ {F} {H} [Γ] (Uᵛ [Γ]) [F]ᵤ [F≡H]ₜ
      [G≡E]ᵤ = S.irrelevanceEq {A = G} {B = E} (_∙″_ {A = F} [Γ] [F])
                               (_∙″_ {A = F} [Γ] [F]ᵤ) [G]ᵤ₁ [G]ᵤ
                 (univEqᵛ {G} {E} (_∙″_ {A = F} [Γ] [F])
                          (λ {Δ} {σ} → [UF] {Δ} {σ}) [G]ᵤ₁ [G≡E]ₜ)
      ΠFGₜ = Πⱼ escapeTerm {l = ¹} (Uᵣ′ ⁰ 0<1 ⊢Δ) (proj₁ ([F]ₜ ⊢Δ [σ]))
             ▹  escapeTerm (proj₁ ([UF] (⊢Δ ∙ ⊢F) [liftFσ]))
                           (proj₁ ([G]ₜ (⊢Δ ∙ ⊢F) [liftFσ]))
      ΠHEₜ = Πⱼ escapeTerm {l = ¹} (Uᵣ′ ⁰ 0<1 ⊢Δ) (proj₁ ([H]ₜ ⊢Δ [σ]))
             ▹  escapeTerm (proj₁ ([UH] (⊢Δ ∙ ⊢H) [liftHσ]))
                           (proj₁ ([E]ₜ (⊢Δ ∙ ⊢H) [liftHσ]))
  in  Uₜ₌ (Π subst σ F ▹ subst (liftSubst σ) G)
          (Π subst σ H ▹ subst (liftSubst σ) E)
          (idRedTerm:*: ΠFGₜ) (idRedTerm:*: ΠHEₜ)
          Πₙ Πₙ
          (≅ₜ-Π-cong ⊢F (escapeTermEq (Uᵣ′ ⁰ 0<1 ⊢Δ) ([F≡H]ₜ ⊢Δ [σ]))
                        (escapeTermEq (proj₁ ([UF] (⊢Δ ∙ ⊢F) [liftFσ]))
                                          ([G≡E]ₜ (⊢Δ ∙ ⊢F) [liftFσ])))
          (proj₁ (Πᵛ {F} {G} [Γ] [F]ᵤ [G]ᵤ ⊢Δ [σ]))
          (proj₁ (Πᵛ {H} {E} [Γ] [H]ᵤ [E]ᵤ ⊢Δ [σ]))
          (Π-congᵛ {F} {G} {H} {E} [Γ] [F]ᵤ [G]ᵤ [H]ᵤ [E]ᵤ [F≡H]ᵤ [G≡E]ᵤ ⊢Δ [σ])

-- Validity of non-dependent function types.
▹▹ᵛ : ∀ {F G Γ l}
      ([Γ] : ⊩ᵛ Γ)
      ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
    → Γ ⊩ᵛ⟨ l ⟩ G / [Γ]
    → Γ ⊩ᵛ⟨ l ⟩ F ▹▹ G / [Γ]
▹▹ᵛ {F} {G} [Γ] [F] [G] =
  Πᵛ {F} {wk1 G} [Γ] [F] (wk1ᵛ {G} {F} [Γ] [F] [G])

-- Validity of non-dependent function type congurence.
▹▹-congᵛ : ∀ {F F′ G G′ Γ l}
           ([Γ] : ⊩ᵛ Γ)
           ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
           ([F′] : Γ ⊩ᵛ⟨ l ⟩ F′ / [Γ])
           ([F≡F′] : Γ ⊩ᵛ⟨ l ⟩ F ≡ F′ / [Γ] / [F])
           ([G] : Γ ⊩ᵛ⟨ l ⟩ G / [Γ])
           ([G′] : Γ ⊩ᵛ⟨ l ⟩ G′ / [Γ])
           ([G≡G′] : Γ ⊩ᵛ⟨ l ⟩ G ≡ G′ / [Γ] / [G])
         → Γ ⊩ᵛ⟨ l ⟩ F ▹▹ G ≡ F′ ▹▹ G′ / [Γ] / ▹▹ᵛ {F} {G} [Γ] [F] [G]
▹▹-congᵛ {F} {F′} {G} {G′} [Γ] [F] [F′] [F≡F′] [G] [G′] [G≡G′] =
  Π-congᵛ {F} {wk1 G} {F′} {wk1 G′} [Γ]
          [F] (wk1ᵛ {G} {F} [Γ] [F] [G])
          [F′] (wk1ᵛ {G′} {F′} [Γ] [F′] [G′])
          [F≡F′] (wk1Eqᵛ {G} {G′} {F} [Γ] [F] [G] [G≡G′])

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 --safe --warning=error --without-K #-}

open import Groups.Abelian.Definition
open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Lists.Lists

module Groups.Polynomials.Group {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

open import Groups.Polynomials.Definition G
open import Groups.Polynomials.Addition G public
open Setoid S
open Equivalence eq

polyGroup : Group naivePolySetoid _+P_
Group.+WellDefined polyGroup = +PwellDefined
Group.0G polyGroup = []
Group.inverse polyGroup = inverse'
Group.+Associative polyGroup {a} {b} {c} = assoc {a} {b} {c}
Group.identRight polyGroup = PidentRight
Group.identLeft polyGroup = PidentLeft
Group.invLeft polyGroup {a} = invLeft' {a}
Group.invRight polyGroup {a} = invRight' {a}

abelian : AbelianGroup G → AbelianGroup polyGroup
AbelianGroup.commutative (abelian ab) {x} {y} = comm ab {x} {y}

ext: agda


text:
{-# OPTIONS --two-level #-}

open import Agda.Primitive

data Unit : Set where tt : Unit
data Unitω : Setω where tt : Unitω
data SUnit : SSet where tt : SUnit
data SUnitω : SSetω where tt : SUnitω

-- Cannot eliminate fibrant type Unit
-- unless target type is also fibrant
-- f1 : Unit → SUnit
-- f1 tt = tt

-- Cannot eliminate fibrant type Unit
-- unless target type is also fibrant
-- f2 : Unit → SUnitω
-- f2 tt = tt

--f3 : Unitω → SUnit
--f3 tt = tt

f4 : Unitω → SUnitω
f4 tt = tt

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Common.Prelude

infixr 9 _∘_

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

test : Nat → Nat
test = _* 5 ∘ 6 +_ ∘ 2 ∸_

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --erased-cubical --no-subtyping #-}

module Agda.Primitive.Cubical where

{-# BUILTIN CUBEINTERVALUNIV IUniv #-}  -- IUniv : SSet₁
{-# BUILTIN INTERVAL I  #-}  -- I : IUniv

{-# BUILTIN IZERO    i0 #-}
{-# BUILTIN IONE     i1 #-}

-- I is treated as the type of booleans.
{-# COMPILE JS i0 = false #-}
{-# COMPILE JS i1 = true  #-}

infix  30 primINeg
infixr 20 primIMin primIMax

primitive
    primIMin : I → I → I
    primIMax : I → I → I
    primINeg : I → I

{-# BUILTIN ISONE    IsOne    #-}  -- IsOne : I → Setω

postulate
  itIsOne : IsOne i1
  IsOne1  : ∀ i j → IsOne i → IsOne (primIMax i j)
  IsOne2  : ∀ i j → IsOne j → IsOne (primIMax i j)

{-# BUILTIN ITISONE  itIsOne  #-}
{-# BUILTIN ISONE1   IsOne1   #-}
{-# BUILTIN ISONE2   IsOne2   #-}

-- IsOne i is treated as the unit type.
{-# COMPILE JS itIsOne = { "tt" : a => a["tt"]() } #-}
{-# COMPILE JS IsOne1 =
  _ => _ => _ => { return { "tt" : a => a["tt"]() } }
  #-}
{-# COMPILE JS IsOne2 =
  _ => _ => _ => { return { "tt" : a => a["tt"]() } }
  #-}

-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ
-- Partial i A = IsOne i → A

{-# BUILTIN PARTIAL  Partial  #-}
{-# BUILTIN PARTIALP PartialP #-}

postulate
  isOneEmpty : ∀ {ℓ} {A : Partial i0 (Set ℓ)} → PartialP i0 A

{-# BUILTIN ISONEEMPTY isOneEmpty #-}

-- Partial i A and PartialP i A are treated as IsOne i → A.
{-# COMPILE JS isOneEmpty =
  _ => x => _ => x({ "tt" : a => a["tt"]() })
  #-}

primitive
  primPOr : ∀ {ℓ} (i j : I) {A : Partial (primIMax i j) (Set ℓ)}
            → (u : PartialP i (λ z → A (IsOne1 i j z)))
            → (v : PartialP j (λ z → A (IsOne2 i j z)))
            → PartialP (primIMax i j) A

  -- Computes in terms of primHComp and primTransp
  primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) {φ : I} (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1

syntax primPOr p q u t = [ p ↦ u , q ↦ t ]

primitive
  primTransp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a : A i0) → A i1
  primHComp  : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module *-example where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

open import Naturals using (_*_)

*-example : 3 * 4 ≡ 12
*-example =
  begin
    3 * 4
  ≡⟨⟩
    4 + (2 * 4)
  ≡⟨⟩
    4 + (4 + (1 * 4))
  ≡⟨⟩
    4 + (4 + (4 + (0 * 4)))
  ≡⟨⟩
    4 + (4 + (4 + 0))
  ≡⟨⟩
    12
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
open import x1-Base

module x3-PropositionalEquality where

data _≡_ {X} : Rel X where
  refl : ∀ {x} → x ≡ x
{-
What propositional equality means.

DEFINITIONAL EQUALITY

To decide if two types/terms are "the same", it reduces them to their normal form,
then compares them syntactically, plus some additional laws.

Every term terminates, so refl : ((λ x → x) 1) ≡ 1 is acceptable

PROPOSITIONAL EQUALITY
User-level equality expressed by the inductive family defined.

Having a propositional equality in scope does not imply definitional equality for the
related terms, unless the propositional equality is a closed term.
That is the reason ≡ is not used from the beginning.
Instead, chose to parametrise the equality relation:
- sometimes propositional equality does not work, for example when working with functions.

In general there might be propositional equalities in scope
 that do not necessarily hold or involve abstracted variables, think of λ (p : 3 ≡ 1) → ....
-}
-- prove ≡ is an equivalence relation

sym : ∀ {X} {x y : X} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

equivalence : ∀ {X} → Equivalence {X} _≡_
equivalence = record { refl = refl; sym = sym; trans = trans }

-- useful
cong : ∀ {X} {x y : X} → (f : X → X) → x ≡ y → f x ≡ f y
cong _ refl = refl
{-
Above uses pattern matching in a new way:

Since value of indices of ≡ depends on constructors,
matching on constructor refines context with new information.

E.g., sym matching refl will unify y and x,
turning them into the same variable in the context for the body of sym,
therefore letting refl be invoked again.

DEPENDENT PATTERN MATCHING
Pattern matching in Agda can change the context AND constraint possible constructors
 of other parameters, if they are a type with indices and those indices have been refined.
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
------------------------------------------------------------------------
-- A library of parser combinators
------------------------------------------------------------------------

-- This module also provides examples of parsers for which the indices
-- cannot be inferred.

module StructurallyRecursiveDescentParsing.Lib where

open import StructurallyRecursiveDescentParsing.Grammar
open import StructurallyRecursiveDescentParsing.Index

open import Data.Nat hiding (_≟_)
open import Data.Vec as Vec using (Vec;  []; _∷_)
open import Data.List using (List; []; _∷_; foldr; foldl; reverse)
open import Data.Product
open import Data.Bool using (Bool; true; false; _∧_; _∨_)
open import Function
open import Data.Maybe hiding (_>>=_)
open import Data.Unit using (⊤)
open import Data.Char using (Char; _==_)
import Data.Char.Properties as Char
open import Codata.Musical.Notation
open import Algebra
import Data.Bool.Properties as Bool
private
  module BCS = CommutativeSemiring Bool.∨-∧-commutativeSemiring
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
import Level

------------------------------------------------------------------------
-- Some important derived combinators

infixl 10 _>>=_

_>>=_ : ∀ {NT Tok e₁ c₁ i₂ R₁ R₂} → let i₁ = e₁ ◇ c₁ in
        Parser NT Tok i₁ R₁ →
        (R₁ → Parser NT Tok i₂ R₂) →
        Parser NT Tok (i₁ · i₂) R₂
_>>=_ {e₁ = true } p₁ p₂ = p₁ ?>>= p₂
_>>=_ {e₁ = false} p₁ p₂ = p₁ !>>= λ x → ♯ p₂ x

cast : ∀ {NT Tok e₁ e₂ c₁ c₂ R} →
       e₁ ≡ e₂ → c₁ ≡ c₂ →
       Parser NT Tok (e₁ ◇ c₁) R → Parser NT Tok (e₂ ◇ c₂) R
cast refl refl p = p

------------------------------------------------------------------------
-- Applicative functor parsers

-- We could get these for free with better library support.

infixl 50 _⊛_ _⊛!_ _<⊛_ _⊛>_ _<$>_ _<$_ _⊗_ _⊗!_

_⊛_ : ∀ {NT Tok i₁ i₂ R₁ R₂} →
      Parser NT Tok i₁ (R₁ → R₂) →
      Parser NT Tok i₂ R₁ →
      Parser NT Tok _  R₂
p₁ ⊛ p₂ = p₁ >>= λ f → p₂ >>= λ x → return (f x)

-- A variant: If the second parser does not accept the empty string,
-- then neither does the combination. (This is immediate for the first
-- parser, but for the second one a small lemma is needed, hence this
-- variant.)

_⊛!_ : ∀ {NT Tok i₁ c₂ R₁ R₂} →
       Parser NT Tok i₁ (R₁ → R₂) →
       Parser NT Tok (false ◇ c₂) R₁ →
       Parser NT Tok (false ◇ _)  R₂
_⊛!_ {i₁ = i₁} p₁ p₂ = cast (BCS.*-comm (empty i₁) false) refl
                            (p₁ ⊛ p₂)

_<$>_ : ∀ {NT Tok i R₁ R₂} →
        (R₁ → R₂) →
        Parser NT Tok i R₁ →
        Parser NT Tok _ R₂
f <$> p = return f ⊛ p

_<⊛_ : ∀ {NT Tok i₁ i₂ R₁ R₂} →
       Parser NT Tok i₁ R₁ →
       Parser NT Tok i₂ R₂ →
       Parser NT Tok _ R₁
p₁ <⊛ p₂ = const <$> p₁ ⊛ p₂

_⊛>_ : ∀ {NT Tok i₁ i₂ R₁ R₂} →
       Parser NT Tok i₁ R₁ →
       Parser NT Tok i₂ R₂ →
       Parser NT Tok _ R₂
p₁ ⊛> p₂ = flip const <$> p₁ ⊛ p₂

_<$_ : ∀ {NT Tok i R₁ R₂} →
       R₁ →
       Parser NT Tok i R₂ →
       Parser NT Tok _ R₁
x <$ p = const x <$> p

_⊗_ : ∀ {NT Tok i₁ i₂ R₁ R₂} →
      Parser NT Tok i₁ R₁ → Parser NT Tok i₂ R₂ →
      Parser NT Tok _ (R₁ × R₂)
p₁ ⊗ p₂ = (_,_) <$> p₁ ⊛ p₂

_⊗!_ : ∀ {NT Tok i₁ c₂ R₁ R₂} →
       Parser NT Tok i₁ R₁ → Parser NT Tok (false ◇ c₂) R₂ →
       Parser NT Tok (false ◇ _) (R₁ × R₂)
p₁ ⊗! p₂ = (_,_) <$> p₁ ⊛! p₂

------------------------------------------------------------------------
-- Parsing sequences

infix 55 _⋆ _+

-- Not accepted by the productivity checker:

-- mutual

--   _⋆ : ∀ {NT Tok R c} →
--        Parser NT Tok (false ◇ c) R     →
--        Parser NT Tok _           (List R)
--   p ⋆ = return [] ∣ p +

--   _+ : ∀ {NT Tok R c} →
--        Parser NT Tok (false ◇ c) R     →
--        Parser NT Tok _           (List R)
--   p + = _∷_ <$> p ⊛ p ⋆

-- In fact the code above risks leading to infinite loops in the
-- current version of Agda (Mar 2009), since it does not contain any
-- coinductive constructors. The following code is OK, though:

mutual

  _⋆ : ∀ {NT Tok R c} →
       Parser NT Tok (false ◇ c) R        →
       Parser NT Tok _           (List R)
  p ⋆ = return [] ∣ p +

  _+ : ∀ {NT Tok R c} →
       Parser NT Tok (false ◇ c) R        →
       Parser NT Tok _           (List R)
  p + =  p   !>>= λ x  → ♯
        (p ⋆ ?>>= λ xs →
         return (x ∷ xs))

-- p sepBy⟨ ne ⟩ sep and p sepBy sep parse one or more ps separated by
-- seps.

_sepBy⟨_⟩_ : ∀ {NT Tok i i′ R R′} →
             Parser NT Tok i R →
             (empty i′ ∧ true) ∧ (empty i ∧ true) ≡ false →
             Parser NT Tok i′ R′ →
             Parser NT Tok _ (List R)
p sepBy⟨ non-empty ⟩ sep = _∷_ <$> p ⊛ cast₁ (sep ⊛> p) ⋆
  where cast₁ = cast non-empty refl

-- _sepBy_ could be implemented by using _sepBy⟨_⟩_, but the following
-- definition is handled more efficiently by the current version of
-- Agda (Dec 2008).

_sepBy_ : ∀ {NT Tok i c R R′} →
          Parser NT Tok i R → Parser NT Tok (false ◇ c) R′ →
          Parser NT Tok _ (List R)
p sepBy sep = _∷_ <$> p ⊛ (sep ⊛> p) ⋆

mutual

  -- Note that the index of atLeast is only partly inferred; the
  -- recursive structure of atLeast-index is given manually.

  atLeast-index : Corners → ℕ → Index
  atLeast-index c zero    = _
  atLeast-index c (suc n) = _

  -- At least n occurrences of p.

  atLeast : ∀ {NT Tok c R} (n : ℕ) →
            Parser NT Tok (false ◇ c) R →
            Parser NT Tok (atLeast-index c n) (List R)
  atLeast zero    p = p ⋆
  atLeast (suc n) p = _∷_ <$> p ⊛ atLeast n p

-- exactly n p parses n occurrences of p.
--
-- (Note that, unlike what is written in "Structurally Recursive
-- Descent Parsing", Agda as of 2012-03-16 can no longer infer
-- exactly-index's second right-hand side.)

exactly-index : Index → ℕ → Index
exactly-index i zero    = 1I
exactly-index i (suc n) = (1I · i · 1I) · exactly-index i n · 1I

exactly : ∀ {NT Tok i R} n →
          Parser NT Tok i R →
          Parser NT Tok (exactly-index i n) (Vec R n)
exactly zero    p = return []
exactly (suc n) p = _∷_ <$> p ⊛ exactly n p

-- A function with a similar type:

sequence : ∀ {NT Tok i R n} →
           Vec (Parser NT Tok i R) n →
           Parser NT Tok (exactly-index i n) (Vec R n)
sequence []       = return []
sequence (p ∷ ps) = _∷_ <$> p ⊛ sequence ps

mutual

  -- p between ps parses p repeatedly, between the elements of ps:
  --   ∙ between (x ∷ y ∷ z ∷ []) ≈ x ∙ y ∙ z.

  between-corners : Corners → ℕ → Corners
  between-corners c′ zero    = _
  between-corners c′ (suc n) = _

  _between_ : ∀ {NT Tok i R c′ R′ n} →
              Parser NT Tok i R →
              Vec (Parser NT Tok (false ◇ c′) R′) (suc n) →
              Parser NT Tok (false ◇ between-corners c′ n) (Vec R n)
  p between (x ∷ [])     = [] <$ x
  p between (x ∷ y ∷ xs) = _∷_ <$> (x ⊛> p) ⊛ (p between (y ∷ xs))

------------------------------------------------------------------------
-- Chaining

-- Associativity. Used to specify how chain≥ should apply the parsed
-- operators: left or right associatively.

data Assoc : Set where
  left  : Assoc
  right : Assoc

-- Application.

appʳ : {R : Set} → R × (R → R → R) → R → R
appʳ (x , _•_) y = x • y

appˡ : {R : Set} → R → (R → R → R) × R → R
appˡ x (_•_ , y) = x • y

-- Shifting. See Examples below for an illuminating example.

shiftʳ : {A B : Set} → A → List (B × A) → List (A × B) × A
shiftʳ x  []                = ([] , x)
shiftʳ x₁ ((x₂ , x₃) ∷ xs₄) = ((x₁ , x₂) ∷ proj₁ xs₃x₄ , proj₂ xs₃x₄)
  where xs₃x₄ = shiftʳ x₃ xs₄

-- Post-processing for the chain≥ parser.

chain≥-combine : {R : Set} → Assoc → R → List ((R → R → R) × R) → R
chain≥-combine left  x ys = foldl appˡ x ys
chain≥-combine right x ys with shiftʳ x ys
... | (xs , y) = foldr appʳ y xs

-- Chains at least n occurrences of op, in an a-associative
-- manner. The ops are surrounded by ps.

chain≥ : ∀ {NT Tok c₁ i₂ R} (n : ℕ) →
         Assoc →
         Parser NT Tok (false ◇ c₁) R →
         Parser NT Tok i₂ (R → R → R) →
         Parser NT Tok _ R
chain≥ n a p op = chain≥-combine a <$> p ⊛ atLeast n (op ⊗! p)

private
 module Examples {R S : Set}
                 (x y z : R)
                 (a b : S)
                 (_+_ _*_ : R → R → R)
                 where

  ex : shiftʳ x ((a , y) ∷ (b , z) ∷ []) ≡ ((x , a) ∷ (y , b) ∷ [] , z)
  ex = refl

  exʳ : chain≥-combine right x ((_+_ , y) ∷ (_*_ , z) ∷ []) ≡
        (x + (y * z))
  exʳ = refl

  exˡ : chain≥-combine left  x ((_+_ , y) ∷ (_*_ , z) ∷ []) ≡
        ((x + y) * z)
  exˡ = refl

------------------------------------------------------------------------
-- N-ary variants of _∣_

-- choice ps parses one of the elements in ps.

choice-corners : Corners → ℕ → Corners
choice-corners c zero    = ε
choice-corners c (suc n) = c ∪ choice-corners c n

choice : ∀ {NT Tok c R n} →
         Vec (Parser NT Tok (false ◇ c) R) n →
         Parser NT Tok (false ◇ choice-corners c n) R
choice []       = fail
choice (p ∷ ps) = p ∣ choice ps

-- choiceMap f xs ≈ choice (map f xs), but avoids use of Vec and
-- fromList.

choiceMap-corners : {A : Set} → (A → Corners) → List A → Corners
choiceMap-corners c []       = ε
choiceMap-corners c (x ∷ xs) = c x ∪ choiceMap-corners c xs

choiceMap : ∀ {NT Tok R} {A : Set} {c : A → Corners} →
            ((x : A) → Parser NT Tok (false ◇ c x) R) →
            (xs : List A) →
            Parser NT Tok (false ◇ choiceMap-corners c xs) R
choiceMap f []       = fail
choiceMap f (x ∷ xs) = f x ∣ choiceMap f xs

------------------------------------------------------------------------
-- sat and friends

sat : ∀ {NT Tok R} → (Tok → Maybe R) → Parser NT Tok (0I · 1I) R
sat {NT} {Tok} {R} p = token !>>= λ c → ♯ ok (p c)
  where
  mutual
    okIndex : Maybe R → Index
    okIndex nothing  = _
    okIndex (just _) = _

    ok : (x : Maybe R) → Parser NT Tok (okIndex x) R
    ok nothing  = fail
    ok (just x) = return x

sat' : ∀ {NT Tok} → (Tok → Bool) → Parser NT Tok _ ⊤
sat' p = sat (boolToMaybe ∘ p)

any : ∀ {NT Tok} → Parser NT Tok _ Tok
any = sat just

------------------------------------------------------------------------
-- Token parsers

module Token (A : DecSetoid Level.zero Level.zero) where

  open DecSetoid A using (_≟_) renaming (Carrier to Tok)

  -- Parses a given token (or, really, a given equivalence class of
  -- tokens).

  tok : ∀ {NT} → Tok → Parser NT Tok _ Tok
  tok tok = sat p
    where
    p : Tok → Maybe Tok
    p tok′ with tok ≟ tok′
    ... | yes _ = just tok′
    ... | no  _ = nothing

  -- Parses a sequence of tokens.

  theString : ∀ {NT n} → Vec Tok n → Parser NT Tok _ (Vec Tok n)
  theString cs = sequence (Vec.map tok cs)

------------------------------------------------------------------------
-- Character parsers

digit : ∀ {NT} → Parser NT Char _ ℕ
digit = 0 <$ tok '0'
      ∣ 1 <$ tok '1'
      ∣ 2 <$ tok '2'
      ∣ 3 <$ tok '3'
      ∣ 4 <$ tok '4'
      ∣ 5 <$ tok '5'
      ∣ 6 <$ tok '6'
      ∣ 7 <$ tok '7'
      ∣ 8 <$ tok '8'
      ∣ 9 <$ tok '9'
  where open Token Char.decSetoid

number : ∀ {NT} → Parser NT Char _ ℕ
number = toNum <$> digit +
  where
  toNum = foldr (λ n x → 10 * x + n) 0 ∘ reverse

-- whitespace recognises an incomplete but useful list of whitespace
-- characters.

whitespace : ∀ {NT} → Parser NT Char _ ⊤
whitespace = sat' isSpace
  where
  isSpace = λ c →
    (c == ' ') ∨ (c == '\t') ∨ (c == '\n') ∨ (c == '\r')

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --without-K --safe #-}
open import Axiom.Extensionality.Propositional using (Extensionality)

module Cats.Category.Sets.Facts.Exponential
  (funext : ∀ {a b} → Extensionality a b)
  where

open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym)

open import Cats.Category
open import Cats.Category.Sets using (Sets)
open import Cats.Category.Sets.Facts.Product using (hasBinaryProducts)

instance
  hasExponentials : ∀ {l} → HasExponentials (Sets l)
  hasExponentials .HasExponentials.hasBinaryProducts = hasBinaryProducts
  hasExponentials .HasExponentials._↝′_ B C = record
    { Cᴮ = B → C
    ; eval = λ { (f , x) → f x }
    ; curry′ = λ f → record
      { arr = λ a b → f (a , b)
      ; prop = λ x → refl
      ; unique = λ eq a → funext λ b → sym (eq _)
      }
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

open import lib.Basics hiding (take; drop; take-drop-split)
open import lib.types.Pointed
open import lib.types.Paths

module lib.types.FunctionSeq where

infixr 80 _◃∘_
data FunctionSeq {i} : Type i → Type i → Type (lsucc i) where
  idf-seq : {A : Type i} → FunctionSeq A A
  _◃∘_ : {A B C : Type i} (g : B → C) (fs : FunctionSeq A B) → FunctionSeq A C

infix 30 _–→_
_–→_ = FunctionSeq

infix 90 _◃idf
_◃idf : ∀ {i} {A B : Type i} → (A → B) → A –→ B
_◃idf fs = fs ◃∘ idf-seq

compose : ∀ {i} {A B : Type i} → (A –→ B) → A → B
compose idf-seq = idf _
compose (g ◃∘ fs) = g ∘ compose fs

de⊙-seq : ∀ {i} {X Y : Ptd i} → (X ⊙–→ Y) → (de⊙ X –→ de⊙ Y)
de⊙-seq ⊙idf-seq = idf-seq
de⊙-seq (f ◃⊙∘ fs) = fst f ◃∘ de⊙-seq fs

de⊙-seq-⊙compose : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y)
  → compose (de⊙-seq fs) == fst (⊙compose fs)
de⊙-seq-⊙compose ⊙idf-seq = idp
de⊙-seq-⊙compose (f ◃⊙∘ fs) = ap (fst f ∘_) (de⊙-seq-⊙compose fs)

private
  pt-seq' : ∀ {i} {j} {X Y : Ptd i} {C : Type j} (g : de⊙ Y → C) (fs : X ⊙–→ Y)
    → g (compose (de⊙-seq fs) (pt X)) =-= g (pt Y)
  pt-seq' g ⊙idf-seq = []
  pt-seq' g (f ◃⊙∘ fs) =
    pt-seq' (g ∘ fst f) fs ∙∙
    ap g (snd f) ◃∎

pt-seq : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y)
  → compose (de⊙-seq fs) (pt X) =-= pt Y
pt-seq ⊙idf-seq = []
pt-seq (f ◃⊙∘ fs) = pt-seq' (fst f) fs ∙▹ snd f

private
  ⊙compose-pt' : ∀ {i} {j} {X Y : Ptd i} {C : Type j} (g : de⊙ Y → C) (fs : X ⊙–→ Y)
    → ap g (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
      ap g (snd (⊙compose fs)) ◃∎
      =ₛ
      ↯ (pt-seq' g fs) ◃∎
  ⊙compose-pt' g ⊙idf-seq = =ₛ-in idp
  ⊙compose-pt' {_} {_} {X} g (f ◃⊙∘ fs) =
    ap g (app= (ap (fst f ∘_) (de⊙-seq-⊙compose fs)) (pt X)) ◃∙
    ap g (snd (⊙compose (f ◃⊙∘ fs))) ◃∎
      =ₛ₁⟨ 0 & 1 & ∘-ap g (_$ pt X) (ap (fst f ∘_) (de⊙-seq-⊙compose fs)) ∙
                   ∘-ap (λ h → g (h (pt X))) (fst f ∘_) (de⊙-seq-⊙compose fs) ∙
                   ap-∘ (g ∘ fst f) (_$ pt X) (de⊙-seq-⊙compose fs) ⟩
    ap (g ∘ fst f) (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    ap g (snd (⊙compose (f ◃⊙∘ fs))) ◃∎
      =ₛ⟨ 1 & 1 & ap-seq-∙ g (ap (fst f) (snd (⊙compose fs)) ◃∙ snd f ◃∎) ⟩
    ap (g ∘ fst f) (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    ap g (ap (fst f) (snd (⊙compose fs))) ◃∙
    ap g (snd f) ◃∎
      =ₛ₁⟨ 1 & 1 & ∘-ap g (fst f) (snd (⊙compose fs)) ⟩
    ap (g ∘ fst f) (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    ap (g ∘ fst f) (snd (⊙compose fs)) ◃∙
    ap g (snd f) ◃∎
      =ₛ⟨ 0 & 2 & ⊙compose-pt' (g ∘ fst f) fs ⟩
    ↯ (pt-seq' (g ∘ fst f) fs) ◃∙
    ap g (snd f) ◃∎
      =ₛ₁⟨ ! (↯-∙∙ (pt-seq' (g ∘ fst f) fs) (ap g (snd f) ◃∎)) ⟩
    ↯ (pt-seq' (g ∘ fst f) fs ∙▹ ap g (snd f)) ◃∎ ∎ₛ

⊙compose-pt : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y)
  → app= (de⊙-seq-⊙compose fs) (pt X) ◃∙
    snd (⊙compose fs) ◃∎
    =ₛ
    ↯ (pt-seq fs) ◃∎
⊙compose-pt ⊙idf-seq = =ₛ-in idp
⊙compose-pt {_} {X} {Y} (f ◃⊙∘ fs) =
  app= (de⊙-seq-⊙compose (f ◃⊙∘ fs)) (pt X) ◃∙
  snd (f ⊙∘ ⊙compose fs) ◃∎
    =ₛ⟨ 1 & 1 & expand (ap (fst f) (snd (⊙compose fs)) ◃∙ snd f ◃∎) ⟩
  app= (de⊙-seq-⊙compose (f ◃⊙∘ fs)) (pt X) ◃∙
  ap (fst f) (snd (⊙compose fs)) ◃∙
  snd f ◃∎
    =ₛ₁⟨ 0 & 1 & ∘-ap (_$ pt X) (fst f ∘_) (de⊙-seq-⊙compose fs) ∙
                 ap-∘ (fst f) (_$ pt X) (de⊙-seq-⊙compose fs) ⟩
  ap (fst f) (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
  ap (fst f) (snd (⊙compose fs)) ◃∙
  snd f ◃∎
    =ₛ⟨ 0 & 2 & ⊙compose-pt' (fst f) fs ⟩
  ↯ (pt-seq' (fst f) fs) ◃∙
  snd f ◃∎
    =ₛ₁⟨ ! (↯-∙∙ (pt-seq' (fst f) fs) (snd f ◃∎)) ⟩
  ↯ (pt-seq' (fst f) fs ∙∙ snd f ◃∎) ◃∎ ∎ₛ

record _=∘_ {i} {A B : Type i} (fs gs : A –→ B) : Type i where
  constructor =∘-in
  field
    =∘-out : compose fs == compose gs
open _=∘_ public

abstract
  de⊙-seq-=⊙∘ : ∀ {i} {X Y : Ptd i} {fs gs : X ⊙–→ Y}
    → fs =⊙∘ gs
    → de⊙-seq fs =∘ de⊙-seq gs
  de⊙-seq-=⊙∘ {fs = fs} {gs = gs} p = =∘-in $
    compose (de⊙-seq fs)
      =⟨ de⊙-seq-⊙compose fs ⟩
    fst (⊙compose fs)
      =⟨ ap fst (=⊙∘-out p) ⟩
    fst (⊙compose gs)
      =⟨ ! (de⊙-seq-⊙compose gs) ⟩
    compose (de⊙-seq gs) =∎

  ⊙seq-λ= : ∀ {i} {X Y : Ptd i} {fs gs : X ⊙–→ Y}
    → (p : compose (de⊙-seq fs) ∼ compose (de⊙-seq gs))
    → pt-seq fs =ₛ p (pt X) ◃∙ pt-seq gs
    → fs =⊙∘ gs
  ⊙seq-λ= {_} {X} {Y} {fs} {gs} p q =
    =⊙∘-in $
    pair= (! (de⊙-seq-⊙compose fs) ∙ λ= p ∙ de⊙-seq-⊙compose gs) $
    ↓-app=cst-in $ =ₛ-out $
    snd (⊙compose fs) ◃∎
      =ₛ⟨ pre-rotate-in (⊙compose-pt fs) ⟩
    ! (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    ↯ (pt-seq fs) ◃∎
      =ₛ₁⟨ 1 & 1 & =ₛ-out q ⟩
    ! (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    ↯ (p (pt X) ◃∙ pt-seq gs) ◃∎
      =ₛ⟨ 1 & 1 & =ₛ-in {t = p (pt X) ◃∙ ↯ (pt-seq gs) ◃∎} $
                  ↯-∙∙ (p (pt X) ◃∎) (pt-seq gs) ⟩
    ! (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    p (pt X) ◃∙
    ↯ (pt-seq gs) ◃∎
      =ₛ⟨ 2 & 1 & !ₛ (⊙compose-pt gs) ⟩
    ! (app= (de⊙-seq-⊙compose fs) (pt X)) ◃∙
    p (pt X) ◃∙
    app= (de⊙-seq-⊙compose gs) (pt X) ◃∙
    snd (⊙compose gs) ◃∎
      =ₛ₁⟨ 0 & 1 & !-ap (_$ pt X) (de⊙-seq-⊙compose fs) ⟩
    app= (! (de⊙-seq-⊙compose fs)) (pt X) ◃∙
    p (pt X) ◃∙
    app= (de⊙-seq-⊙compose gs) (pt X) ◃∙
    snd (⊙compose gs) ◃∎
      =ₛ₁⟨ 1 & 1 & ! (app=-β p (pt X)) ⟩
    app= (! (de⊙-seq-⊙compose fs)) (pt X) ◃∙
    app= (λ= p) (pt X) ◃∙
    app= (de⊙-seq-⊙compose gs) (pt X) ◃∙
    snd (⊙compose gs) ◃∎
      =ₛ⟨ 0 & 3 & ∙-ap-seq (_$ pt X) (_ ◃∙ _ ◃∙ _ ◃∎) ⟩
    app= (! (de⊙-seq-⊙compose fs) ∙ λ= p ∙ de⊙-seq-⊙compose gs) (pt X) ◃∙
    snd (⊙compose gs) ◃∎ ∎ₛ

abstract
  !⊙∘ : ∀ {i} {X Y : Ptd i} {fs gs : X ⊙–→ Y} → fs =⊙∘ gs → gs =⊙∘ fs
  !⊙∘ (=⊙∘-in p) = =⊙∘-in (! p)

⊙expand : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y) → (⊙compose fs ◃⊙idf) =⊙∘ fs
⊙expand fs = =⊙∘-in idp

⊙contract : ∀ {i} {X Y : Ptd i} {fs : X ⊙–→ Y} → fs =⊙∘ (⊙compose fs ◃⊙idf)
⊙contract = =⊙∘-in idp

private
  _∙⊙∘_ : ∀ {i} {X Y : Ptd i} {fs gs hs : X ⊙–→ Y} → fs =⊙∘ gs → gs =⊙∘ hs → fs =⊙∘ hs
  _∙⊙∘_ (=⊙∘-in p) (=⊙∘-in q) = =⊙∘-in (p ∙ q)

  point-from-target : ∀ {i} {X Y : Ptd i}
    → ℕ → (X ⊙–→ Y) → Ptd i
  point-from-target {Y = Y} O fs = Y
  point-from-target {Y = Y} (S n) ⊙idf-seq = Y
  point-from-target (S n) (f ◃⊙∘ fs) = point-from-target n fs

  take : ∀ {i} (n : ℕ) {X Y : Ptd i} (fs : X ⊙–→ Y) → point-from-target n fs ⊙–→ Y
  take O s = ⊙idf-seq
  take (S n) ⊙idf-seq = ⊙idf-seq
  take (S n) (f ◃⊙∘ fs) = f ◃⊙∘ take n fs

  drop : ∀ {i} (n : ℕ) {X Y : Ptd i} (fs : X ⊙–→ Y) → X ⊙–→ point-from-target n fs
  drop 0 fs = fs
  drop (S n) ⊙idf-seq = ⊙idf-seq
  drop (S n) (f ◃⊙∘ fs) = drop n fs

  infixr 80 _⊙∘∘_
  _⊙∘∘_ : ∀ {i} {X Y Z : Ptd i} (gs : Y ⊙–→ Z) (fs : X ⊙–→ Y) → (X ⊙–→ Z)
  ⊙idf-seq ⊙∘∘ fs = fs
  (g ◃⊙∘ gs) ⊙∘∘ fs = g ◃⊙∘ (gs ⊙∘∘ fs)

  ⊙compose-⊙∘∘ : ∀ {i} {X Y Z : Ptd i} (gs : Y ⊙–→ Z) (fs : X ⊙–→ Y)
    → ⊙compose (gs ⊙∘∘ fs) == ⊙compose gs ⊙∘ ⊙compose fs
  ⊙compose-⊙∘∘ ⊙idf-seq fs = ! (⊙λ= (⊙∘-unit-l (⊙compose fs)))
  ⊙compose-⊙∘∘ (g ◃⊙∘ gs) fs =
    ap (g ⊙∘_) (⊙compose-⊙∘∘ gs fs) ∙
    ! (⊙λ= (⊙∘-assoc g (⊙compose gs) (⊙compose fs)))

  take-drop-split' : ∀ {i} {X Y : Ptd i} (n : ℕ) (fs : X ⊙–→ Y)
    → fs == take n fs ⊙∘∘ drop n fs
  take-drop-split' O fs = idp
  take-drop-split' (S n) ⊙idf-seq = idp
  take-drop-split' (S n) (f ◃⊙∘ fs) = ap (f ◃⊙∘_) (take-drop-split' n fs)

  take-drop-split : ∀ {i} {X Y : Ptd i} (n : ℕ) (s : X ⊙–→ Y)
    → ⊙compose s ◃⊙idf =⊙∘ ⊙compose (take n s) ◃⊙∘ ⊙compose (drop n s) ◃⊙idf
  take-drop-split n fs = =⊙∘-in $
    ⊙compose fs
      =⟨ ap ⊙compose (take-drop-split' n fs) ⟩
    ⊙compose (take n fs ⊙∘∘ drop n fs)
      =⟨ ⊙compose-⊙∘∘ (take n fs) (drop n fs) ⟩
    ⊙compose (take n fs) ⊙∘ ⊙compose (drop n fs) =∎

abstract
  private
    infixr 10 _⊙compose=⟨_&_&_&_⟩_
    _⊙compose=⟨_&_&_&_⟩_ : ∀ {i} {X Y : Ptd i} {f : X ⊙→ Y}
      → (fs : X ⊙–→ Y)
      → (n : ℕ) (m : ℕ)
      → (gs : point-from-target m (drop n fs) ⊙–→ point-from-target n fs)
      → ⊙compose (take m (drop n fs)) == ⊙compose gs
      → ⊙compose (take n fs ⊙∘∘ gs ⊙∘∘ drop m (drop n fs)) == f
      → ⊙compose fs == f
    _⊙compose=⟨_&_&_&_⟩_ {f = f} fs n m gs p p' =
      ⊙compose fs
        =⟨ =⊙∘-out (take-drop-split n fs) ⟩
      ⊙compose (take n fs) ⊙∘ ⊙compose (drop n fs)
        =⟨ ap (⊙compose (take n fs) ⊙∘_) (=⊙∘-out (take-drop-split m (drop n fs))) ⟩
      ⊙compose (take n fs) ⊙∘ ⊙compose (take m (drop n fs)) ⊙∘ ⊙compose (drop m (drop n fs))
        =⟨ ap (λ v → ⊙compose (take n fs) ⊙∘ v ⊙∘ ⊙compose (drop m (drop n fs))) p ⟩
      ⊙compose (take n fs) ⊙∘ ⊙compose gs ⊙∘ ⊙compose (drop m (drop n fs))
        =⟨ ap (⊙compose (take n fs) ⊙∘_) (! (⊙compose-⊙∘∘ gs (drop m (drop n fs)))) ⟩
      ⊙compose (take n fs) ⊙∘ ⊙compose (gs ⊙∘∘ drop m (drop n fs))
        =⟨ ! (⊙compose-⊙∘∘ (take n fs) (gs ⊙∘∘ drop m (drop n fs))) ⟩
      ⊙compose (take n fs ⊙∘∘ gs ⊙∘∘ drop m (drop n fs))
        =⟨ p' ⟩
      f =∎

  infixr 10 _=⊙∘⟨_⟩_
  _=⊙∘⟨_⟩_ : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y) {gs hs : X ⊙–→ Y}
    → fs =⊙∘ gs
    → gs =⊙∘ hs
    → fs =⊙∘ hs
  _=⊙∘⟨_⟩_ _ p q = p ∙⊙∘ q

  infixr 10 _=⊙∘⟨_&_&_⟩_
  _=⊙∘⟨_&_&_⟩_ : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y) {gs : X ⊙–→ Y}
    → (m n : ℕ)
    → {hs : point-from-target n (drop m fs) ⊙–→ point-from-target m fs}
    → take n (drop m fs) =⊙∘ hs
    → take m fs ⊙∘∘ hs ⊙∘∘ drop n (drop m fs) =⊙∘ gs
    → fs =⊙∘ gs
  _=⊙∘⟨_&_&_⟩_ fs m n {hs} p p' = =⊙∘-in (fs ⊙compose=⟨ m & n & hs & =⊙∘-out p ⟩ =⊙∘-out p')

  infixr 10 _=⊙∘₁⟨_⟩_
  _=⊙∘₁⟨_⟩_ : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y) {gs : X ⊙–→ Y}
    → {h : X ⊙→ Y}
    → ⊙compose fs == h
    → h ◃⊙idf =⊙∘ gs
    → fs =⊙∘ gs
  _=⊙∘₁⟨_⟩_ fs p p' = =⊙∘-in p ∙⊙∘ p'

  infixr 10 _=⊙∘₁⟨_&_&_⟩_
  _=⊙∘₁⟨_&_&_⟩_ : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y) {gs : X ⊙–→ Y}
    → (m n : ℕ)
    → {h : point-from-target n (drop m fs) ⊙→ point-from-target m fs}
    → ⊙compose (take n (drop m fs)) == h
    → take m fs ⊙∘∘ h ◃⊙∘ drop n (drop m fs) =⊙∘ gs
    → fs =⊙∘ gs
  _=⊙∘₁⟨_&_&_⟩_ fs m n {h} p p' = fs =⊙∘⟨ m & n & (=⊙∘-in {gs = h ◃⊙idf} p) ⟩ p'

infix 15 _∎⊙∘
_∎⊙∘ : ∀ {i} {X Y : Ptd i} (fs : X ⊙–→ Y) → fs =⊙∘ fs
_∎⊙∘ _ = =⊙∘-in idp

⊙coe-seq : ∀ {i} {X Y : Ptd i}
  → X =-= Y
  → X ⊙–→ Y
⊙coe-seq [] = ⊙idf-seq
⊙coe-seq (p ◃∙ ps) = ⊙coe-seq ps ⊙∘∘ ⊙coe p ◃⊙idf

⊙coe-seq-∙ : ∀ {i} {X Y : Ptd i} (ps : X =-= Y)
  → ⊙coe (↯ ps) ◃⊙idf =⊙∘ ⊙coe-seq ps
⊙coe-seq-∙ [] = =⊙∘-in idp
⊙coe-seq-∙ (p ◃∙ ps) =
  ⊙coe (↯ (p ◃∙ ps)) ◃⊙idf
    =⊙∘₁⟨ ap ⊙coe (↯-∙∙ (p ◃∎) ps) ⟩
  ⊙coe (p ∙ ↯ ps) ◃⊙idf
    =⊙∘⟨ ⊙coe-∙ p (↯ ps) ⟩
  ⊙coe (↯ ps) ◃⊙∘ ⊙coe p ◃⊙idf
    =⊙∘⟨ 0 & 1 & ⊙coe-seq-∙ ps ⟩
  ⊙coe-seq ps ⊙∘∘ ⊙coe p ◃⊙idf ∎⊙∘

⊙coe-seq-=ₛ : ∀ {i} {X Y : Ptd i} {ps qs : X =-= Y}
  → ps =ₛ qs
  → ⊙coe-seq ps =⊙∘ ⊙coe-seq qs
⊙coe-seq-=ₛ {ps = ps} {qs = qs} r =
  ⊙coe-seq ps
    =⊙∘⟨ !⊙∘ (⊙coe-seq-∙ ps) ⟩
  ⊙coe (↯ ps) ◃⊙idf
    =⊙∘₁⟨ ap ⊙coe (=ₛ-out r) ⟩
  ⊙coe (↯ qs) ◃⊙idf
    =⊙∘⟨ ⊙coe-seq-∙ qs ⟩
  ⊙coe-seq qs ∎⊙∘

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Colist type and some operations
------------------------------------------------------------------------

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

module Codata.Colist where

open import Size
open import Data.Unit
open import Data.Nat.Base
open import Data.Product using (_×_ ; _,_)
open import Data.These using (These; this; that; these)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.BoundedVec as BVec using (BoundedVec)
open import Function

open import Codata.Thunk using (Thunk; force)
open import Codata.Conat as Conat using (Conat ; zero ; suc)
open import Codata.Cowriter as CW using (Cowriter; _∷_)
open import Codata.Delay as Delay using (Delay ; now ; later)
open import Codata.Stream using (Stream ; _∷_)

data Colist {a} (A : Set a) (i : Size) : Set a where
  []  : Colist A i
  _∷_ : A → Thunk (Colist A) i → Colist A i

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

------------------------------------------------------------------------
-- Relationship to Cowriter.

  fromCowriter : ∀ {i} → Cowriter W A i → Colist W i
  fromCowriter CW.[ _ ] = []
  fromCowriter (w ∷ ca) = w ∷ λ where .force → fromCowriter (ca .force)

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

  toCowriter : ∀ {i} → Colist A i → Cowriter A ⊤ i
  toCowriter []       = CW.[ _ ]
  toCowriter (a ∷ as) = a ∷ λ where .force → toCowriter (as .force)

------------------------------------------------------------------------
-- Basic functions.

  [_] : A → Colist A ∞
  [ a ] = a ∷ λ where .force → []

  length : ∀ {i} → Colist A i → Conat i
  length []       = zero
  length (x ∷ xs) = suc λ where .force → length (xs .force)

  replicate : ∀ {i} → Conat i → A → Colist A i
  replicate zero    a = []
  replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a

  infixr 5 _++_ _⁺++_
  _++_ : ∀ {i} → Colist A i → Colist A i → Colist A i
  []       ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys

  lookup : ℕ → Colist A ∞ → Maybe A
  lookup n       []       = nothing
  lookup zero    (a ∷ as) = just a
  lookup (suc n) (a ∷ as) = lookup n (as .force)

  colookup : ∀ {i} → Conat i → Colist A i → Delay (Maybe A) i
  colookup n       []       = now nothing
  colookup zero    (a ∷ as) = now (just a)
  colookup (suc n) (a ∷ as) =
    later λ where .force → colookup (n .force) (as .force)

  take : ∀ (n : ℕ) → Colist A ∞ → BoundedVec A n
  take zero    xs       = BVec.[]
  take n       []       = BVec.[]
  take (suc n) (x ∷ xs) = x BVec.∷ take n (xs .force)

  cotake : ∀ {i} → Conat i → Stream A i → Colist A i
  cotake zero    xs       = []
  cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force)

  fromList : List A → Colist A ∞
  fromList []       = []
  fromList (x ∷ xs) = x ∷ λ where .force → fromList xs

  _⁺++_ : ∀ {i} → List⁺ A → Thunk (Colist A) i → Colist A i
  (x ∷ xs) ⁺++ ys = x ∷ λ where .force → fromList xs ++ ys .force

  fromStream : ∀ {i} → Stream A i → Colist A i
  fromStream = cotake Conat.infinity

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

  chunksOf : (n : ℕ) → Colist A ∞ → Cowriter (Vec A n) (BoundedVec A n) ∞
  chunksOf n = chunksOfAcc n id id module ChunksOf where

    chunksOfAcc : ∀ {i} m →
      -- We have two continuations but we are only ever going to use one.
      -- If we had linear types, we would write the type using the & conjunction here.
      (k≤ : BoundedVec A m → BoundedVec A n) →
      (k≡ : Vec A m → Vec A n) →
      -- Finally we chop up the input stream.
      Colist A ∞ → Cowriter (Vec A n) (BoundedVec A n) i
    chunksOfAcc zero    k≤ k≡ as       = k≡ [] ∷ λ where .force → chunksOfAcc n id id as
    chunksOfAcc (suc k) k≤ k≡ []       = CW.[ k≤ BVec.[] ]
    chunksOfAcc (suc k) k≤ k≡ (a ∷ as) =
      chunksOfAcc k (k≤ ∘ (a BVec.∷_)) (k≡ ∘ (a ∷_)) (as .force)

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

 map : ∀ {i} (f : A → B) → Colist A i → Colist B i
 map f []       = []
 map f (a ∷ as) = f a ∷ λ where .force → map f (as .force)

 unfold :  ∀ {i} → (A → Maybe (A × B)) → A → Colist B i
 unfold next seed with next seed
 ... | nothing          = []
 ... | just (seed′ , b) = b ∷ λ where .force → unfold next seed′

 scanl : ∀ {i} → (B → A → B) → B → Colist A i → Colist B i
 scanl c n []       = n ∷ λ where .force → []
 scanl c n (a ∷ as) = n ∷ λ where .force → scanl c (c n a) (as .force)

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

  alignWith : ∀ {i} → (These A B → C) → Colist A i → Colist B i → Colist C i
  alignWith f []         bs       = map (f ∘′ that) bs
  alignWith f as@(_ ∷ _) []       = map (f ∘′ this) as
  alignWith f (a ∷ as)   (b ∷ bs) =
    f (these a b) ∷ λ where .force → alignWith f (as .force) (bs .force)

  zipWith : ∀ {i} → (A → B → C) → Colist A i → Colist B i → Colist C i
  zipWith f []       bs       = []
  zipWith f as       []       = []
  zipWith f (a ∷ as) (b ∷ bs) =
    f a b ∷ λ where .force → zipWith f (as .force) (bs .force)

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

  align : ∀ {i} → Colist A i → Colist B i → Colist (These A B) i
  align = alignWith id

  zip : ∀ {i} → Colist A i → Colist B i → Colist (A × B) i
  zip = zipWith _,_

  ap : ∀ {i} → Colist (A → B) i → Colist A i → Colist B i
  ap = zipWith _$′_


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Group where

open import Algebra.Group.Group public
open import Algebra.Group.Monoid public
open import Algebra.Group.Semigroup public

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


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

module Agda.Builtin.Coinduction where

infix 1000 ♯_

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

{-
  Various combinators for working with Isomorphisms in the
  context of morphism equalities
  both for Category (Switch) and IsGroupoid (GroupoidR)
-}

module Categories.Morphism.Reasoning.Iso {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Function renaming (id to idᶠ; _∘_ to _∙_)

open import Categories.Category.Groupoid using (IsGroupoid)
open import Categories.Morphism C
open import Categories.Morphism.Reasoning.Core C

open import Relation.Binary hiding (_⇒_)

open Category C
private
  variable
    A B X Y : Obj
    f g h k : X ⇒ Y

open HomReasoning

module Switch (i : X ≅ Y) where
  open _≅_ i

  switch-fromtoˡ : from ∘ h ≈ k → h ≈ to ∘ k
  switch-fromtoˡ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelˡ isoˡ ⟩
    to ∘ (from ∘ h) ≈⟨ refl⟩∘⟨ pf ⟩
    to ∘ k          ∎

  switch-tofromˡ : to ∘ h ≈ k → h ≈ from ∘ k
  switch-tofromˡ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelˡ isoʳ ⟩
    from ∘ (to ∘ h) ≈⟨ refl⟩∘⟨ pf ⟩
    from ∘ k        ∎

  switch-fromtoʳ : h ∘ from ≈ k → h ≈ k ∘ to
  switch-fromtoʳ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelʳ isoʳ ⟩
    (h ∘ from) ∘ to ≈⟨ pf ⟩∘⟨refl ⟩
    k ∘ to          ∎

  switch-tofromʳ : h ∘ to ≈ k → h ≈ k ∘ from
  switch-tofromʳ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelʳ isoˡ ⟩
    (h ∘ to) ∘ from ≈⟨ pf ⟩∘⟨refl ⟩
    k ∘ from        ∎

  cancel-fromʳ : h ∘ from ≈ k ∘ from → h ≈ k
  cancel-fromʳ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelʳ isoʳ ⟩
    (h ∘ from) ∘ to ≈⟨ pf ⟩∘⟨refl ⟩
    (k ∘ from) ∘ to ≈⟨ cancelʳ isoʳ ⟩
    k               ∎

  cancel-fromˡ : from ∘ h ≈ from ∘ k → h ≈ k
  cancel-fromˡ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelˡ isoˡ ⟩
    to ∘ (from ∘ h) ≈⟨ refl⟩∘⟨ pf ⟩
    to ∘ (from ∘ k) ≈⟨ cancelˡ isoˡ ⟩
    k               ∎

  cancel-toʳ : h ∘ to ≈ k ∘ to → h ≈ k
  cancel-toʳ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelʳ isoˡ ⟩
    (h ∘ to) ∘ from ≈⟨ pf ⟩∘⟨refl ⟩
    (k ∘ to) ∘ from ≈⟨ cancelʳ isoˡ ⟩
    k               ∎

  cancel-toˡ : to ∘ h ≈ to ∘ k → h ≈ k
  cancel-toˡ {h = h} {k = k} pf = begin
    h               ≈˘⟨ cancelˡ isoʳ ⟩
    from ∘ (to ∘ h) ≈⟨ refl⟩∘⟨ pf ⟩
    from ∘ (to ∘ k) ≈⟨ cancelˡ isoʳ ⟩
    k               ∎

  -- We can flip an iso i in a commuting triangle, like so:
  --
  --          i                       i⁻¹
  --    X --------> Y            X <-------- Y
  --     \    ≃    /              \    ≃    /
  --      \       /                \       /
  --     g \     / h     ===>     g \     / h
  --        \   /                    \   /
  --         V V                      V V
  --          A                        A
  --
  flip-iso : {g : X ⇒ A} {h : Y ⇒ A} → g ≈ h ∘ from → g ∘ to ≈ h
  flip-iso tr₁ = sym (switch-fromtoʳ (sym tr₁))

  -- Consider two commuting squares
  --
  --         f₁                      f₂
  --    X -------> A            X -------> A
  --    |          |            |          |
  --    |          |            |          |
  --  ≃ | i        | h        ≃ | i        | h
  --    |          |            |          |
  --    V          V            V          V
  --    Y -------> B            Y -------> B
  --         g₁                      g₂
  --
  -- with i an isomorphism.  Then g₁ ≈ g₂ if f₁ ≈ f₂.

  push-eq : {f₁ f₂ : X ⇒ A} {g₁ g₂ : Y ⇒ B} {h : A ⇒ B} →
            CommutativeSquare f₁ from h g₁ →
            CommutativeSquare f₂ from h g₂ →
            f₁ ≈ f₂ → g₁ ≈ g₂
  push-eq {f₁ = f₁} {f₂} {g₁} {g₂} {h₂} sq₁ sq₂ hyp = begin
    g₁               ≈˘⟨ flip-iso sq₁ ⟩
    (h₂ ∘ f₁) ∘ to   ≈⟨ ∘-resp-≈ˡ (∘-resp-≈ʳ hyp) ⟩
    (h₂ ∘ f₂) ∘ to   ≈⟨ flip-iso sq₂ ⟩
    g₂               ∎

open Switch public

-- conjugates
module _ (i : A ≅ B) (j : X ≅ Y) where
  private
    module i = _≅_ i
    module j = _≅_ j

  conjugate-from : f ∘ i.from ≈ j.from ∘ g → j.to ∘ f ≈ g ∘ i.to
  conjugate-from {f = f} {g = g} eq = begin
    j.to ∘ f                   ≈⟨ introʳ i.isoʳ ⟩
    (j.to ∘ f) ∘ i.from ∘ i.to ≈⟨ center eq ⟩
    j.to ∘ (j.from ∘ g) ∘ i.to ≈⟨ center⁻¹ j.isoˡ refl ⟩
    id ∘ g ∘ i.to              ≈⟨ identityˡ ⟩
    g ∘ i.to                   ∎

  conjugate-to : j.to ∘ f ≈ g ∘ i.to → f ∘ i.from ≈ j.from ∘ g
  conjugate-to {f = f} {g = g} eq = begin
    f ∘ i.from                   ≈⟨ introˡ j.isoʳ ⟩
    (j.from ∘ j.to) ∘ f ∘ i.from ≈⟨ center eq ⟩
    j.from ∘ (g ∘ i.to) ∘ i.from ≈⟨ center⁻¹ refl i.isoˡ ⟩
    (j.from ∘ g) ∘ id            ≈⟨ identityʳ ⟩
    j.from ∘ g                   ∎

module GroupoidR (G : IsGroupoid C) where
  open IsGroupoid G using (_⁻¹; iso; equiv-obj)

  switch-fromtoˡ′ : f ∘ h ≈ k → h ≈ f ⁻¹ ∘ k
  switch-fromtoˡ′ = switch-fromtoˡ (equiv-obj _)

  switch-tofromˡ′ : f ⁻¹ ∘ h ≈ k → h ≈ f ∘ k
  switch-tofromˡ′ = switch-tofromˡ (equiv-obj _)

  switch-fromtoʳ′ : h ∘ f ≈ k → h ≈ k ∘ f ⁻¹
  switch-fromtoʳ′ = switch-fromtoʳ (equiv-obj _)

  switch-tofromʳ′ : h ∘ f ⁻¹ ≈ k → h ≈ k ∘ f
  switch-tofromʳ′ = switch-tofromʳ (equiv-obj _)

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on floats
------------------------------------------------------------------------

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

module Data.Float.Properties where

open import Data.Bool.Base as Bool using (Bool)
open import Data.Float.Base
import Data.Word.Base as Word
import Data.Word.Properties as Wₚ
open import Relation.Nullary.Decidable as RN using (map′)
open import Relation.Binary
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.Float.Properties
  renaming (primFloatToWord64Injective to toWord-injective)
  public

------------------------------------------------------------------------
-- Properties of _≈_

≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ eq = toWord-injective _ _  (Wₚ.≈⇒≡ eq)

≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive eq = Wₚ.≈-reflexive (cong toWord eq)

≈-refl : Reflexive _≈_
≈-refl = refl

≈-sym : Symmetric _≈_
≈-sym = sym

≈-trans : Transitive _≈_
≈-trans = trans

≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p

infix 4 _≈?_
_≈?_ : Decidable _≈_
_≈?_ = On.decidable toWord Word._≈_ Wₚ._≈?_

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl  = λ {i} → ≈-refl {i}
  ; sym   = λ {i j} → ≈-sym {i} {j}
  ; trans = λ {i j k} → ≈-trans {i} {j} {k}
  }

≈-setoid : Setoid _ _
≈-setoid = record
  { isEquivalence = ≈-isEquivalence
  }

≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
  { isEquivalence = ≈-isEquivalence
  ; _≟_           = _≈?_
  }

≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
  { isDecEquivalence = ≈-isDecEquivalence
  }
------------------------------------------------------------------------
-- Properties of _≡_

infix 4 _≟_
_≟_ : DecidableEquality Float
x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y)

≡-setoid : Setoid _ _
≡-setoid = setoid Float

≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid _≟_

------------------------------------------------------------------------
-- Boolean equality test.

infix 4 _==_
_==_ : Float → Float → Bool
w₁ == w₂ = RN.⌊ w₁ ≟ w₂ ⌋

------------------------------------------------------------------------
-- Properties of _<_

infix 4 _<?_
_<?_ : Decidable _<_
_<?_ = On.decidable toWord Word._<_ Wₚ._<?_

<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ = On.strictTotalOrder Wₚ.<-strictTotalOrder-≈ toWord


text:
open import Agda.Builtin.Equality

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

data ⊥ : Set where

data N : Set where
  ze : N
  su : (⊥ → N) → N

foo : N
foo = su (\ ())

postulate
  ext : ∀ {A : Set} → (f g : ⊥ → A) → f ≡ g

foo-suc : foo ≡ su (\ _ → foo)
foo-suc = cong su (ext (λ ()) (λ _ → foo))

-- bad!
no-cycle : ∀ {n} → n ≡ su (\ _ → n) → ⊥
no-cycle ()

false : ⊥
false = no-cycle foo-suc


text:
module Automaton.Deterministic.Oper where

open import Automaton.Deterministic
open import Logic.Propositional
import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.List renaming (∅ to [])
open import Data.Tuple as Tuple using (_,_) renaming (_⨯_ to _⨯'_)
open import Data.Tuple.Equivalence
open import Functional
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_)
open import Structure.Operator
open import Structure.Relator.Proofs
open import Structure.Setoid
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₚ ℓₚ₁ ℓₚ₂ : Lvl.Level
private variable Q Q₁ Q₂ State : Type{ℓ}
private variable Σ Σ₁ Σ₂ Alphabet : Type{ℓ}

module _ ⦃ equiv₁ : Equiv{ℓₑ₁}(Q₁) ⦄ ⦃ equiv₂ : Equiv{ℓₑ₂}(Q₂) ⦄ ⦃ equivₑ : Equiv{ℓₑ₃}(Σ) ⦄ where
  -- Automaton that accepts words accepted by both of the specified automatons
  _⨯_ : Deterministic{ℓₚ = ℓₚ₁}(Q₁)(Σ) → Deterministic{ℓₚ = ℓₚ₂}(Q₂)(Σ) → Deterministic(Q₁ ⨯' Q₂)(Σ)
  _⨯_ (deterministic δ₁ q₀₁ F₁) (deterministic δ₂ q₀₂ F₂) = deterministic δ ⦃ δ-op ⦄ q₀ F where
    δ : (Q₁ ⨯' Q₂) → Σ → (Q₁ ⨯' Q₂)
    δ(q₁ , q₂)(word) = (δ₁(q₁)(word) , δ₂(q₂)(word))

    instance
      δ-op : BinaryOperator(δ)
      BinaryOperator.congruence δ-op ([∧]-intro xyl xyr) cc = [∧]-intro (congruence₂(δ₁) xyl cc) (congruence₂(δ₂) xyr cc)

    q₀ : (Q₁ ⨯' Q₂)
    q₀ = (q₀₁ , q₀₂)

    F : PredSet(Q₁ ⨯' Q₂)
    F = PredSet.intro (\{(q₁ , q₂) → (q₁ ∈ F₁) ∧ (q₂ ∈ F₂)})
      ⦃ [∧]-unaryRelator
        ⦃ rel-P = [∘]-unaryRelator ⦃ rel = PredSet.preserve-equiv F₁ ⦄ ⦄
        ⦃ rel-Q = [∘]-unaryRelator ⦃ rel = PredSet.preserve-equiv F₂ ⦄ ⦄
      ⦄

  -- Automaton that accepts words accepted by any of the specified automatons
  _+_ : Deterministic{ℓₚ = ℓₚ₁}(Q₁)(Σ) → Deterministic{ℓₚ = ℓₚ₂}(Q₂)(Σ) → Deterministic(Q₁ ⨯' Q₂)(Σ)
  _+_ (deterministic δ₁ q₀₁ F₁) (deterministic δ₂ q₀₂ F₂) = deterministic δ q₀ F where
    δ : (Q₁ ⨯' Q₂) → Σ → (Q₁ ⨯' Q₂)
    δ(q₀₁ , q₀₂)(word) = (δ₁(q₀₁)(word) , δ₂(q₀₂)(word))

    instance
      δ-op : BinaryOperator(δ)
      BinaryOperator.congruence δ-op ([∧]-intro xyl xyr) cc = [∧]-intro (congruence₂(δ₁) xyl cc) (congruence₂(δ₂) xyr cc)

    q₀ : (Q₁ ⨯' Q₂)
    q₀ = (q₀₁ , q₀₂)

    F : PredSet(Q₁ ⨯' Q₂)
    F = PredSet.intro (\{(q₁ , q₂) → (q₁ ∈ F₁) ∨ (q₂ ∈ F₂)})
      ⦃ [∨]-unaryRelator
        ⦃ rel-P = [∘]-unaryRelator ⦃ rel = PredSet.preserve-equiv F₁ ⦄ ⦄
        ⦃ rel-Q = [∘]-unaryRelator ⦃ rel = PredSet.preserve-equiv F₂ ⦄ ⦄
      ⦄

module _ ⦃ equiv : Equiv{ℓₑ}(Q) ⦄ ⦃ equivₑ : Equiv{ℓₑ₃}(Σ) ⦄ where
  -- Automaton that accepts words not accepted by the specified automaton
  ∁_ : Deterministic{ℓₚ = ℓₚ}(Q)(Σ) → Deterministic(Q)(Σ)
  ∁_ (deterministic δ q₀ F) = deterministic δ q₀ (PredSet.∁ F)

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:
open import Agda.Builtin.Equality

postulate
  A : Set

id : A → A
id x = x

mutual
  ?Y : A → A → A
  ?Y = _

  ?X : A → A → A
  ?X = _

  -- This tries to solve ?X x x := ?Y x y, which fails but prunes
  -- ?Y x y := ?Z x. Failing ?X := ?Y we then try the other direction
  -- without realising that ?Y has been instantiated and (re)solve
  -- ?Y x y := ?X x x, leaving ?Z hanging!
  -- The `id` call is to make sure we get into `compareAtom`. The
  -- corresponding code in `compareTerm` does the right thing.
  constr₁ : ∀ x y → id (?X x x) ≡ id (?Y x y)
  constr₁ x y = refl

  -- We can then solve ?X.
  constr₂ : ∀ x y → ?X x y ≡ x
  constr₂ x y = refl

-- And check that they really are solved

checkY : ?Y ≡ λ x y → x
checkY = refl

checkX : ?X ≡ λ x y → x
checkX = refl

-- ...but we still have ?Z unsolved.


text:
open import Prelude hiding (_<_)

module Implicits.Resolution.GenericFinite.TerminationCondition
  where

open import Induction.WellFounded
open import Implicits.Syntax

record TerminationCondition : Set₁ where
  field
    TCtx : Set
    _<_  : TCtx → TCtx → Set
    _<?_  : (x y : TCtx) → Dec (x < y)
    step : ∀ {ν} → TCtx → ICtx ν → Type ν → Type ν → SimpleType ν → TCtx
    wf-< : Well-founded _<_

  T-Acc : TCtx → Set
  T-Acc Φ = Acc _<_ Φ


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

module Categories.Category.Finite where

open import Level
open import Data.Product using (Σ; _,_; ∃₂)
open import Function.Equality using (Π; _⟶_)
open import Function.Inverse
open import Data.Nat as ℕ hiding (_⊔_)
import Data.Fin as Fin
open import Data.Vec as Vec
open import Relation.Binary using (Setoid)
import Relation.Binary.PropositionalEquality as ≡

open import Categories.Category
open Π

FiniteSetoid : ∀ {c ℓ} n (S : Setoid c ℓ) → Set _
FiniteSetoid n S = Inverse (≡.setoid (Fin.Fin n)) S

record Finite {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C

  field
    ∣Obj∣ : ℕ
    ∣_⇒_∣ : Obj → Obj → ℕ

    Obj-finite : FiniteSetoid ∣Obj∣ (≡.setoid Obj)
    ⇒-finite   : ∀ A B → FiniteSetoid ∣ A ⇒ B ∣ (hom-setoid {A} {B})

  module Obj-finite   = Inverse Obj-finite
  module ⇒-finite A B = Inverse (⇒-finite A B)

  private
    Fins : ∀ n → Vec (Fin.Fin n) n
    Fins ℕ.zero    = []
    Fins (ℕ.suc n) = Fin.fromℕ n ∷ Vec.map (Fin.raise 1) (Fins n)

  -- enumeration of all objects
  Objs : Vec Obj ∣Obj∣
  Objs = Vec.map (Obj-finite.to ⟨$⟩_) (Fins ∣Obj∣)

  private
    ObjPairs : ∀ {a} {A : Set a} → (Obj → Obj → A) → Vec A (∣Obj∣ * ∣Obj∣)
    ObjPairs {_} {A} f = Objs >>= ap
      where ap : Obj → Vec A ∣Obj∣
            ap X = Vec.map (f X) Objs

  -- enumeration of all morphisms of a given pair of objects
  ⟦_⇒_⟧ : ∀ A B → Vec (A ⇒ B) ∣ A ⇒ B ∣
  ⟦ A ⇒ B ⟧ = Vec.map (⇒-finite.to A B ⟨$⟩_) (Fins ∣ A ⇒ B ∣)

  -- number of all morphisms
  ∣-⇒-| : ℕ
  ∣-⇒-| = foldr (λ _ → ℕ) _+_ 0 (ObjPairs ∣_⇒_∣)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties imply others
------------------------------------------------------------------------

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

module Relation.Unary.Consequences where

open import Relation.Unary
open import Relation.Nullary using (recompute)

dec⟶recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
dec⟶recomputable P-dec = recompute (P-dec _)


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Presheaves where

open import Level using (_⊔_ ; suc)

open import Cats.Category
open import Cats.Category.Fun using (Fun)
open import Cats.Category.Op using (_ᵒᵖ)
open import Cats.Category.Setoids using (Setoids)

Presheaves : ∀ {lo la l≈} (C : Category lo la l≈) l l′
  → Category (lo ⊔ la ⊔ l≈ ⊔ suc (l ⊔ l′)) (lo ⊔ la ⊔ l ⊔ l′) (lo ⊔ l ⊔ l′)
Presheaves C l l′ = Fun (C ᵒᵖ) (Setoids l l′)


text:
{-# OPTIONS --without-K #-}
infixr 1 _‘→’_

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

mutual
  data Type : Set where
    _‘→’_ : Type → Type → Type
    ‘□’ : Type → Type
    ‘⊤’ : Type
    ‘⊥’ : Type

  data □ : Type → Set where
    Lӧb : ∀ {X} → □ (‘□’ X ‘→’ X) → □ X
    ‘tt’ : □ ‘⊤’

mutual
  ⌞_⌟ : Type → Set
  ⌞ A ‘→’ B ⌟ = ⌞ A ⌟ → ⌞ B ⌟
  ⌞ ‘□’ T ⌟   = □ T
  ⌞ ‘⊤’ ⌟     = ⊤
  ⌞ ‘⊥’ ⌟     = ⊥

  ⌞_⌟t : ∀ {T : Type} → □ T → ⌞ T ⌟
  ⌞ (Lӧb □‘X’→X) ⌟t = ⌞ □‘X’→X ⌟t (Lӧb □‘X’→X)
  ⌞ ‘tt’ ⌟t = tt

¬_ : Set → Set
¬ T = T → ⊥

‘¬’_ : Type → Type
‘¬’ T = T ‘→’ ‘⊥’

lӧb : ∀ {‘X’} → □ (‘□’ ‘X’ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
lӧb f = ⌞ Lӧb f ⌟t

incompleteness : ¬ □ (‘¬’ (‘□’ ‘⊥’))
incompleteness = lӧb

soundness : ¬ □ ‘⊥’
soundness x = ⌞ x ⌟t

non-emptyness : □ ‘⊤’
non-emptyness = ‘tt’

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
------------------------------------------------------------------------
-- Truncation, defined as a HIT
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- The beginning of this module follows the HoTT book rather closely.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the truncation uses path equality,
-- but the supplied notion of equality is used for many other things.

import Equality.Path as P

module H-level.Truncation
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

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

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as TP using (∥_∥)
open import Monad equality-with-J
open import Nat equality-with-J as Nat using (_≤_; min)
import Pointed-type equality-with-J as PT
open import Sphere eq
open import Suspension eq as Susp using (north)
open import Univalence-axiom equality-with-J

private
  variable
    a b ℓ p : Level
    A B C   : Type a
    P       : A → Type p
    e x y   : A
    f g r   : A → B
    m n     : ℕ
    k       : Isomorphism-kind

-- A truncation operator for positive h-levels.

data ∥_∥[1+_] (A : Type a) (n : ℕ) : Type a where
  ∣_∣    : A → ∥ A ∥[1+ n ]
  hub    : (r : 𝕊 n → ∥ A ∥[1+ n ]) → ∥ A ∥[1+ n ]
  spokeᴾ : (r : 𝕊 n → ∥ A ∥[1+ n ]) (x : 𝕊 n) → r x P.≡ hub r

-- Spoke equalities.

spoke : (r : 𝕊 n → ∥ A ∥[1+ n ]) (x : 𝕊 n) → r x ≡ hub r
spoke r x = _↔_.from ≡↔≡ (spokeᴾ r x)

-- The truncation operator produces types of the right h-level.

truncation-has-correct-h-level : ∀ n → H-level (1 + n) ∥ A ∥[1+ n ]
truncation-has-correct-h-level {A = A} n =
  _↔_.from +↔∀contractible𝕊→ᴮ c
  where
  c : ∀ x → Contractible ((𝕊 n , north) PT.→ᴮ (∥ A ∥[1+ n ] , x))
  c x =
      (const x , (const x (north {A = 𝕊 n})  ≡⟨⟩
                  x                          ∎))
    , λ { (f , fn≡x) → Σ-≡,≡→≡
            (⟨ext⟩ λ y →
               const x y  ≡⟨⟩
               x          ≡⟨ sym fn≡x ⟩
               f north    ≡⟨ spoke f north ⟩
               hub f      ≡⟨ sym $ spoke f y ⟩∎
               f y        ∎)
            (subst (λ f → f north ≡ x)
                   (⟨ext⟩ (λ y → trans (sym fn≡x)
                                   (trans (spoke f north)
                                      (sym (spoke f y)))))
                   (refl x)                                             ≡⟨ subst-ext _ _ ⟩

             subst (_≡ x)
                   (trans (sym fn≡x)
                      (trans (spoke f north) (sym (spoke f north))))
                   (refl x)                                             ≡⟨ cong (λ p → subst (_≡ x) (trans (sym fn≡x) p) (refl x)) $ trans-symʳ _ ⟩

             subst (_≡ x) (trans (sym fn≡x) (refl (f north))) (refl x)  ≡⟨ cong (λ p → subst (_≡ x) p (refl x)) $ trans-reflʳ _ ⟩

             subst (_≡ x) (sym fn≡x) (refl x)                           ≡⟨ subst-trans _ ⟩

             trans fn≡x (refl x)                                        ≡⟨ trans-reflʳ _ ⟩∎

             fn≡x                                                       ∎)
        }

-- A dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : ∥ A ∥[1+ n ] → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ    : ∀ x → P ∣ x ∣
    hubʳ   : (r : 𝕊 n → ∥ A ∥[1+ n ]) →
             (∀ x → P (r x)) →
             P (hub r)
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ])
             (p : ∀ x → P (r x))
             (x : 𝕊 n) →
             P.[ (λ i → P (spokeᴾ r x i)) ] p x ≡ hubʳ r p

open Elimᴾ public

elimᴾ : Elimᴾ P → ∀ x → P x
elimᴾ {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : ∀ x → P x
  helper ∣ x ∣          = E.∣∣ʳ x
  helper (hub r)        = E.hubʳ r (λ x → helper (r x))
  helper (spokeᴾ r x i) = E.spokeʳ r (λ x → helper (r x)) x i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (n : ℕ) (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : A → B
    hubʳ   : (𝕊 n → ∥ A ∥[1+ n ]) → (𝕊 n → B) → B
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ]) (p : 𝕊 n → B) (x : 𝕊 n) →
             p x P.≡ hubʳ r p

open Recᴾ public

recᴾ : Recᴾ n A B → ∥ A ∥[1+ n ] → B
recᴾ r = elimᴾ eᴾ
  where
  module R = Recᴾ r

  eᴾ : Elimᴾ _
  eᴾ .∣∣ʳ    = r .∣∣ʳ
  eᴾ .hubʳ   = r .hubʳ
  eᴾ .spokeʳ = r .spokeʳ

-- A dependent eliminator.

record Elim′ {A : Type a} (P : ∥ A ∥[1+ n ] → Type p) :
             Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ    : ∀ x → P ∣ x ∣
    hubʳ   : (r : 𝕊 n → ∥ A ∥[1+ n ]) →
             (∀ x → P (r x)) →
             P (hub r)
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ])
             (p : ∀ x → P (r x))
             (x : 𝕊 n) →
             subst P (spoke r x) (p x) ≡ hubʳ r p

open Elim′ public

elim′ : Elim′ P → ∀ x → P x
elim′ e′ = elimᴾ eᴾ
  where
  module E′ = Elim′ e′

  eᴾ : Elimᴾ _
  eᴾ .∣∣ʳ          = E′.∣∣ʳ
  eᴾ .hubʳ         = E′.hubʳ
  eᴾ .spokeʳ r p x = subst≡→[]≡ (E′.spokeʳ r p x)

elim′-spoke :
  dcong (elim′ e) (spoke r x) ≡
  Elim′.spokeʳ e r (λ x → elim′ e (r x)) x
elim′-spoke = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec′ (n : ℕ) (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : A → B
    hubʳ   : (𝕊 n → ∥ A ∥[1+ n ]) → (𝕊 n → B) → B
    spokeʳ : (r : 𝕊 n → ∥ A ∥[1+ n ]) (p : 𝕊 n → B) (x : 𝕊 n) →
             p x ≡ hubʳ r p

open Rec′ public

rec′ : Rec′ n A B → ∥ A ∥[1+ n ] → B
rec′ r′ = recᴾ rᴾ
  where
  module R′ = Rec′ r′

  rᴾ : Recᴾ _ _ _
  rᴾ .∣∣ʳ          = R′.∣∣ʳ
  rᴾ .hubʳ         = R′.hubʳ
  rᴾ .spokeʳ r p x = _↔_.to ≡↔≡ (R′.spokeʳ r p x)

rec′-spoke :
  cong (rec′ e) (spoke r x) ≡ Rec′.spokeʳ e r (λ x → rec′ e (r x)) x
rec′-spoke = cong-≡↔≡ (refl _)

-- A dependent eliminator that can be used when the motive is a family
-- of types, all of a certain h-level.

record Elim {A : Type a} (P : ∥ A ∥[1+ n ] → Type p) :
            Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ      : ∀ x → P ∣ x ∣
    h-levelʳ : ∀ x → H-level (1 + n) (P x)

open Elim public

elim : Elim {n = n} {A = A} P → ∀ x → P x
elim {n = n} {A = A} {P = P} e = elim′ e′
  where
  module _ (r : 𝕊 n → ∥ A ∥[1+ n ]) (p : ∀ x → P (r x)) where

    h′ : 𝕊 n → P (hub r)
    h′ x = subst P (spoke r x) (p x)

    h = h′ north

    lemma =                                                       $⟨ e .h-levelʳ ⟩
      (∀ x → H-level (1 + n) (P x))                               ↝⟨ _$ _ ⟩
      H-level (1 + n) (P (hub r))                                 ↔⟨ +↔∀contractible𝕊→ᴮ ⟩
      (∀ h → Contractible ((𝕊 n , north) PT.→ᴮ (P (hub r) , h)))  ↝⟨ _$ _ ⟩
      Contractible ((𝕊 n , north) PT.→ᴮ (P (hub r) , h))          ↝⟨ mono₁ _ ⟩□
      Is-proposition ((𝕊 n , north) PT.→ᴮ (P (hub r) , h))        □

    s = λ x →
      subst P (spoke r x) (p x)  ≡⟨⟩
      h′ x                       ≡⟨ cong (λ f → proj₁ f x) $ lemma (h′ , refl _) (const h , refl _) ⟩
      const h x                  ≡⟨⟩
      h                          ∎

  e′ : Elim′ _
  e′ .∣∣ʳ    = e .∣∣ʳ
  e′ .hubʳ   = h
  e′ .spokeʳ = s

-- A non-dependent eliminator that can be used when the motive is a
-- type of a certain h-level.

record Rec (n : ℕ) (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ      : A → B
    h-levelʳ : H-level (1 + n) B

open Rec public

rec : Rec n A B → ∥ A ∥[1+ n ] → B
rec r = elim λ where
  .∣∣ʳ        → r .∣∣ʳ
  .h-levelʳ _ → r .h-levelʳ

-- Dependent functions into P that agree on the image of ∣_∣ agree
-- everywhere, if P is a family of types that all have a certain
-- h-level.

uniqueness′ :
  {f g : (x : ∥ A ∥[1+ n ]) → P x} →
  (∀ x → H-level (2 + n) (P x)) →
  ((x : A) → f ∣ x ∣ ≡ g ∣ x ∣) →
  ((x : ∥ A ∥[1+ n ]) → f x ≡ g x)
uniqueness′ {n = n} P-h f≡g = elim λ where
  .∣∣ʳ        → f≡g
  .h-levelʳ _ → +⇒≡ {n = suc n} (P-h _)

-- A special case of the previous property.

uniqueness :
  {f g : ∥ A ∥[1+ n ] → B} →
  H-level (1 + n) B →
  ((x : A) → f ∣ x ∣ ≡ g ∣ x ∣) →
  ((x : ∥ A ∥[1+ n ]) → f x ≡ g x)
uniqueness h = uniqueness′ (λ _ → mono₁ _ h)

-- The truncation operator's universal property.

universal-property :
  H-level (1 + n) B →
  (∥ A ∥[1+ n ] → B) ↔ (A → B)
universal-property h = record
  { surjection = record
    { logical-equivalence = record
      { to   = _∘ ∣_∣
      ; from = λ f → rec λ where
          .∣∣ʳ      → f
          .h-levelʳ → h
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = λ f → ⟨ext⟩ $ uniqueness h (λ x → f ∣ x ∣  ∎)
  }

-- The truncation operator ∥_∥[1+ n ] is a functor.

∥∥-map : (A → B) → ∥ A ∥[1+ n ] → ∥ B ∥[1+ n ]
∥∥-map f = rec λ where
  .∣∣ʳ x    → ∣ f x ∣
  .h-levelʳ → truncation-has-correct-h-level _

∥∥-map-id :
  (x : ∥ A ∥[1+ n ]) →
  ∥∥-map id x ≡ x
∥∥-map-id = uniqueness
  (truncation-has-correct-h-level _)
  (λ x → ∣ x ∣  ∎)

∥∥-map-∘ :
  (x : ∥ A ∥[1+ n ]) →
  ∥∥-map (f ∘ g) x ≡ ∥∥-map f (∥∥-map g x)
∥∥-map-∘ {f = f} {g = g} = uniqueness
  (truncation-has-correct-h-level _)
  (λ x → ∣ f (g x) ∣  ∎)

-- A zip function.

∥∥-zip : (A → B → C) → ∥ A ∥[1+ n ] → ∥ B ∥[1+ n ] → ∥ C ∥[1+ n ]
∥∥-zip f = rec λ where
  .∣∣ʳ x    → ∥∥-map (f x)
  .h-levelʳ → Π-closure ext _ λ _ →
              truncation-has-correct-h-level _

-- A has h-level 1 + n if and only if it is isomorphic to
-- ∥ A ∥[1+ n ].

+⇔∥∥↔ : H-level (1 + n) A ⇔ (∥ A ∥[1+ n ] ↔ A)
+⇔∥∥↔ {n = n} {A = A} = record
  { to = λ h → record
    { surjection = record
      { logical-equivalence = record
        { from = ∣_∣
        ; to   = rec λ where
            .∣∣ʳ      → id
            .h-levelʳ → h
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = elim λ where
        .∣∣ʳ x      → ∣ x ∣  ∎
        .h-levelʳ _ → ⇒≡ _ $ truncation-has-correct-h-level _
    }
  ; from =
      ∥ A ∥[1+ n ] ↔ A                                    ↝⟨ H-level-cong ext _ ⟩
      (H-level (1 + n) ∥ A ∥[1+ n ] ↔ H-level (1 + n) A)  ↝⟨ (λ hyp → _↔_.to hyp (truncation-has-correct-h-level _)) ⟩□
      H-level (1 + n) A                                   □
  }

-- The (1 + n)-truncation of x ≡ y, where x and y have type A, is
-- equivalent to the equality of ∣ x ∣ and ∣ y ∣ (as elements of the
-- (2 + n)-truncation of A), assuming univalence.
--
-- Along with the fact that this lemma computes in a certain way (see
-- below) this is more or less Theorem 7.3.12 from the HoTT book.

∥≡∥≃∣∣≡∣∣ :
  {A : Type a} {x y : A} →
  Univalence a →
  ∥ x ≡ y ∥[1+ n ] ≃ _≡_ {A = ∥ A ∥[1+ suc n ]} ∣ x ∣ ∣ y ∣
∥≡∥≃∣∣≡∣∣ {n = n} {A = A} univ = Eq.↔→≃
  (decode ∣ _ ∣ ∣ _ ∣)
  (encode ∣ _ ∣ ∣ _ ∣)
  (decode-encode _)
  (encode-decode _ _)
  where
  Eq : (_ _ : ∥ A ∥[1+ suc n ]) → ∃ λ (B : Type _) → H-level (suc n) B
  Eq = rec λ where
    .h-levelʳ →
      Π-closure ext (2 + n) λ _ →
      ∃-H-level-H-level-1+ ext univ (1 + n)
    .∣∣ʳ x → rec λ where
      .h-levelʳ → ∃-H-level-H-level-1+ ext univ (1 + n)
      .∣∣ʳ y →
        ∥ x ≡ y ∥[1+ n ] , truncation-has-correct-h-level n

  Eq-refl : (x : ∥ A ∥[1+ suc n ]) → proj₁ (Eq x x)
  Eq-refl = elim λ where
    .∣∣ʳ x      → ∣ refl x ∣
    .h-levelʳ x → mono₁ (1 + n) $ proj₂ (Eq x x)

  decode : ∀ x y → proj₁ (Eq x y) → x ≡ y
  decode = elim λ where
    .h-levelʳ _ →
      Π-closure ext (2 + n) λ _ →
      Π-closure ext (2 + n) λ _ →
      mono₁ (2 + n) $ truncation-has-correct-h-level (1 + n)
    .∣∣ʳ x → elim λ where
      .h-levelʳ _ →
        Π-closure ext (2 + n) λ _ →
        mono₁ (2 + n) $ truncation-has-correct-h-level (1 + n)
      .∣∣ʳ y → rec λ where
        .h-levelʳ → truncation-has-correct-h-level (1 + n)
        .∣∣ʳ      → cong ∣_∣

  encode : ∀ x y → x ≡ y → proj₁ (Eq x y)
  encode x y x≡y = subst (λ y → proj₁ (Eq x y)) x≡y (Eq-refl x)

  decode-encode : ∀ x (x≡y : x ≡ y) → decode x y (encode x y x≡y) ≡ x≡y
  decode-encode = elim λ where
    .h-levelʳ _ →
      Π-closure ext (2 + n) λ _ →
      mono₁ (3 + n) $ mono₁ (2 + n) $
      truncation-has-correct-h-level (1 + n)
    .∣∣ʳ x → elim¹
      (λ x≡y → decode _ _ (encode _ _ x≡y) ≡ x≡y)
      (decode (∣ x ∣) (∣ x ∣) (encode ∣ x ∣ ∣ x ∣ (refl ∣ x ∣))      ≡⟨⟩

       decode (∣ x ∣) (∣ x ∣)
         (subst (λ y → proj₁ (Eq ∣ x ∣ y)) (refl ∣ x ∣) ∣ refl x ∣)  ≡⟨ cong (decode _ _) $ subst-refl _ _ ⟩

       decode (∣ x ∣) (∣ x ∣) (∣ refl x ∣)                           ≡⟨⟩

       cong ∣_∣ (refl x)                                             ≡⟨ cong-refl _ ⟩∎

       refl ∣ x ∣                                                    ∎)

  encode-decode :
    ∀ x y (eq : proj₁ (Eq x y)) → encode x y (decode x y eq) ≡ eq
  encode-decode = elim λ where
    .h-levelʳ x →
       Π-closure ext (2 + n) λ y →
       Π-closure ext (2 + n) λ _ →
       mono₁ (2 + n) $ mono₁ (1 + n) $
       proj₂ (Eq x y)
    .∣∣ʳ x → elim λ where
      .h-levelʳ y →
        Π-closure ext (2 + n) λ _ →
        mono₁ (2 + n) $ mono₁ (1 + n) $
        proj₂ (Eq ∣ x ∣ y)
      .∣∣ʳ y → elim λ where
        .h-levelʳ _ →
          mono₁ (1 + n) $ truncation-has-correct-h-level n
        .∣∣ʳ eq →
          encode ∣ x ∣ ∣ y ∣ (decode (∣ x ∣) (∣ y ∣) (∣ eq ∣))         ≡⟨⟩
          subst (λ y → proj₁ (Eq ∣ x ∣ y)) (cong ∣_∣ eq) (∣ refl x ∣)  ≡⟨ sym $ subst-∘ _ _ _ ⟩
          subst (λ y → proj₁ (Eq ∣ x ∣ ∣ y ∣)) eq (∣ refl x ∣)         ≡⟨⟩
          subst (λ y → ∥ x ≡ y ∥[1+ n ]) eq (∣ refl x ∣)               ≡⟨ elim¹
                                                                            (λ eq → subst (λ y → ∥ x ≡ y ∥[1+ n ]) eq (∣ refl x ∣) ≡
                                                                                ∣ subst (x ≡_) eq (refl x) ∣)
                                                                            (trans (subst-refl _ _) $
                                                                             cong ∣_∣ $ sym $ subst-refl _ _)
                                                                            _ ⟩
          ∣ subst (x ≡_) eq (refl x) ∣                                 ≡⟨ cong ∣_∣ $ sym trans-subst ⟩
          ∣ trans (refl x) eq ∣                                        ≡⟨ cong ∣_∣ $ trans-reflˡ _ ⟩∎
          ∣ eq ∣                                                       ∎

_ :
  {A : Type a} {x y : A} {univ : Univalence a}
  {x≡y : x ≡ y} →
  _≃_.to (∥≡∥≃∣∣≡∣∣ {n = n} univ) ∣ x≡y ∣ ≡ cong ∣_∣ x≡y
_ = refl _

-- The truncation operator commutes with _×_.
--
-- This result is similar to Theorem 7.3.8 from the HoTT book.

∥∥×∥∥≃∥×∥ : (∥ A ∥[1+ n ] × ∥ B ∥[1+ n ]) ≃ ∥ A × B ∥[1+ n ]
∥∥×∥∥≃∥×∥ {n = n} = Eq.↔→≃
  (uncurry $ rec λ where
     .h-levelʳ → Π-closure ext _ λ _ →
                 truncation-has-correct-h-level _
     .∣∣ʳ x    → rec λ where
       .h-levelʳ → truncation-has-correct-h-level _
       .∣∣ʳ y    → ∣ x , y ∣)
  (rec λ where
     .∣∣ʳ      → Σ-map ∣_∣ ∣_∣
     .h-levelʳ → s)
  (elim λ where
     .∣∣ʳ _      → refl _
     .h-levelʳ _ →
       mono₁ (1 + n) $ truncation-has-correct-h-level n)
  (uncurry $ elim λ where
     .h-levelʳ _ → Π-closure ext (1 + n) λ _ →
                   mono₁ (1 + n) s
     .∣∣ʳ _      → elim λ where
       .h-levelʳ _ → mono₁ (1 + n) s
       .∣∣ʳ _      → refl _)
  where
  s = ×-closure _
        (truncation-has-correct-h-level _)
        (truncation-has-correct-h-level _)

-- Nested truncations where the inner truncation's h-level is at least
-- as large as the outer truncation's h-level can be flattened.

flatten-≥ : m ≤ n → ∥ ∥ A ∥[1+ n ] ∥[1+ m ] ↔ ∥ A ∥[1+ m ]
flatten-≥ m≤n = record
  { surjection = record
    { logical-equivalence = record
      { from = ∥∥-map ∣_∣
      ; to   = rec λ where
          .h-levelʳ → truncation-has-correct-h-level _
          .∣∣ʳ      → rec λ where
            .∣∣ʳ      → ∣_∣
            .h-levelʳ → mono (Nat.suc≤suc m≤n)
                             (truncation-has-correct-h-level _)
      }
    ; right-inverse-of = uniqueness
        (truncation-has-correct-h-level _)
        (λ x → ∣ x ∣  ∎)
    }
  ; left-inverse-of = uniqueness
      (truncation-has-correct-h-level _)
      (uniqueness
         (mono (Nat.suc≤suc m≤n)
               (truncation-has-correct-h-level _))
         (λ x → ∣ ∣ x ∣ ∣  ∎))
  }

-- The remainder of this module is not based on the HoTT book.

-- Nested truncations where the inner truncation's h-level is at most
-- as large as the outer truncation's h-level can be flattened.

flatten-≤ : m ≤ n → ∥ ∥ A ∥[1+ m ] ∥[1+ n ] ↔ ∥ A ∥[1+ m ]
flatten-≤ m≤n = record
  { surjection = record
    { logical-equivalence = record
      { from = ∣_∣
      ; to   = rec λ where
          .∣∣ʳ      → id
          .h-levelʳ → mono (Nat.suc≤suc m≤n)
                           (truncation-has-correct-h-level _)
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = uniqueness
      (truncation-has-correct-h-level _)
      (λ x → ∣ x ∣  ∎)
  }

-- Nested truncations can be flattened.

flatten : ∥ ∥ A ∥[1+ m ] ∥[1+ n ] ↔ ∥ A ∥[1+ min m n ]
flatten {A = A} {m = m} {n = n} = case Nat.total m n of λ where
  (inj₁ m≤n) → ∥ ∥ A ∥[1+ m ] ∥[1+ n ]  ↝⟨ flatten-≤ m≤n ⟩
               ∥ A ∥[1+ m ]             ↝⟨ ≡⇒↝ _ $ cong ∥ A ∥[1+_] $ sym $ _⇔_.to Nat.≤⇔min≡ m≤n ⟩□
               ∥ A ∥[1+ min m n ]       □
  (inj₂ m≥n) → ∥ ∥ A ∥[1+ m ] ∥[1+ n ]  ↝⟨ flatten-≥ m≥n ⟩
               ∥ A ∥[1+ n ]             ↝⟨ ≡⇒↝ _ $ cong ∥ A ∥[1+_] $ sym $ _⇔_.to Nat.≤⇔min≡ m≥n ⟩
               ∥ A ∥[1+ min n m ]       ↝⟨ ≡⇒↝ _ $ cong ∥ A ∥[1+_] $ Nat.min-comm _ _ ⟩□
               ∥ A ∥[1+ min m n ]       □

-- The propositional truncation operator ∥_∥ is pointwise isomorphic
-- to ∥_∥[1+ 0 ].

∥∥↔∥∥ : ∥ A ∥ ↔ ∥ A ∥[1+ 0 ]
∥∥↔∥∥ = record
  { surjection = record
    { logical-equivalence = record
      { to   = TP.rec (truncation-has-correct-h-level 0) ∣_∣
      ; from = rec λ where
          .∣∣ʳ      → TP.∣_∣
          .h-levelʳ → TP.truncation-is-proposition
      }
    ; right-inverse-of = λ _ → truncation-has-correct-h-level 0 _ _
    }
  ; left-inverse-of = λ _ → TP.truncation-is-proposition _ _
  }

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∥ A ∥[1+ n ] → (A → ∥ B ∥[1+ n ]) → ∥ B ∥[1+ n ]
_>>=′_ {A = A} {n = n} {B = B} = curry (
  ∥ A ∥[1+ n ] × (A → ∥ B ∥[1+ n ])  ↝⟨ uncurry (flip ∥∥-map) ⟩
  ∥ ∥ B ∥[1+ n ] ∥[1+ n ]            ↔⟨ flatten-≤ Nat.≤-refl ⟩□
  ∥ B ∥[1+ n ]                       □)

-- ∥_∥[1+ n ] is a monad.

instance

  monad : Monad {c = ℓ} (∥_∥[1+ n ])
  Raw-monad.return (Monad.raw-monad monad) = ∣_∣

  Raw-monad._>>=_ (Monad.raw-monad monad) = _>>=′_

  Monad.left-identity monad = λ _ _ → refl _

  Monad.right-identity monad =
    uniqueness (truncation-has-correct-h-level _) (λ _ → refl _)

  Monad.associativity monad = flip λ f → flip λ g → uniqueness
    (truncation-has-correct-h-level _)
    (λ x → f x >>=′ g  ∎)

-- The truncation operator preserves logical equivalences.

∥∥-cong-⇔ : A ⇔ B → ∥ A ∥[1+ n ] ⇔ ∥ B ∥[1+ n ]
∥∥-cong-⇔ A⇔B = record
  { to   = ∥∥-map (_⇔_.to   A⇔B)
  ; from = ∥∥-map (_⇔_.from A⇔B)
  }

-- The truncation operator preserves bijections.

∥∥-cong : A ↔[ k ] B → ∥ A ∥[1+ n ] ↔[ k ] ∥ B ∥[1+ n ]
∥∥-cong {n = n} A↝B = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = ∥∥-map (_↔_.to   A↔B)
      ; from = ∥∥-map (_↔_.from A↔B)
      }
    ; right-inverse-of = lemma A↔B
    }
  ; left-inverse-of = lemma (inverse A↔B)
  })
  where
  A↔B = from-isomorphism A↝B

  lemma :
    (A↔B : A ↔ B) (x : ∥ B ∥[1+ n ]) →
    ∥∥-map (_↔_.to A↔B) (∥∥-map (_↔_.from A↔B) x) ≡ x
  lemma A↔B x =
    ∥∥-map (_↔_.to A↔B) (∥∥-map (_↔_.from A↔B) x)  ≡⟨ sym $ ∥∥-map-∘ x ⟩
    ∥∥-map (_↔_.to A↔B ∘ _↔_.from A↔B) x           ≡⟨ cong (λ f → ∥∥-map f x) $ ⟨ext⟩ $ _↔_.right-inverse-of A↔B ⟩
    ∥∥-map id x                                    ≡⟨ ∥∥-map-id x ⟩∎
    x                                              ∎

-- ∥ A ∥[1+_] is downwards closed.

downwards-closed : m ≤ n → ∥ A ∥[1+ n ] → ∥ A ∥[1+ m ]
downwards-closed {m = m} {n = n} {A = A} m≤n =
  ∥ A ∥[1+ n ]             ↝⟨ ∥∥-map ∣_∣ ⟩
  ∥ ∥ A ∥[1+ m ] ∥[1+ n ]  ↔⟨ flatten-≤ m≤n ⟩□
  ∥ A ∥[1+ m ]             □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Prelude

module Implicits.Resolution.Termination where

open import Implicits.Resolution.Termination.SizeMeasures public
open import Implicits.Resolution.Termination.Stack public
open import Implicits.Resolution.Termination.Lemmas public


text:
-- This combination should not be allowed:

{-# OPTIONS --guardedness --sized-types --safe #-}

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
module Relation.Ternary.Separation.Morphisms where

open import Level
open import Function
open import Relation.Unary
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Separation
open import Data.Product
open import Function using (_∘_)

record Morphism {a b} (A : Set a) (B : Set b)
  {{r : RawSep A}} {u} {{s₁ : IsUnitalSep r u}}
  {{rb : RawSep B}} : Set (a ⊔ suc b) where

  field
    j    : A → B

    -- j "commutes" with _⊎_
    j-⊎  : ∀ {Φ₁ Φ₂ Φ} → Φ₁ ⊎ Φ₂ ≣ Φ → j Φ₁ ⊎ j Φ₂ ≣ j Φ
    j-⊎⁻ : ∀ {Φ₁ Φ₂ Φ} → j Φ₁ ⊎ j Φ₂ ≣ Φ → ∃ λ Φ' → Φ ≡ j Φ' × Φ₁ ⊎ Φ₂ ≣ Φ'

  instance _ = s₁

  infixr 8 _⇒ⱼ_
  _⇒ⱼ_ : ∀ {p q} → Pred A p → Pred B q → Pred A _
  P ⇒ⱼ Q = P ⇒ (Q ∘ j)

  infixr 8 _─✴ⱼ_
  _─✴ⱼ_ : ∀ {p q} → Pred A p → Pred B q → Pred B _
  P ─✴ⱼ Q = P ─✴[ j ] Q

  {- Such a morphism on SAs induces a functor on SA-predicates -}
  module _ where

    data J {p} (P : Pred A p) : Pred B (a ⊔ p) where
      inj : ∀ {Φ} → P Φ → J P (j Φ)

    jstar : ∀ {p q} {P : Pred A p} {Q : Pred A q} → ∀[ J (P ✴ Q) ⇒ J P ✴ J Q ]
    jstar (inj (p ×⟨ σ ⟩ q)) = inj p ×⟨ j-⊎ σ ⟩ inj q

    jmap : ∀ {p q} {P : Pred A p} {Q : Pred A q} → ∀[ (P ─✴ Q) ⇒ⱼ (J P ─✴ J Q) ]
    app (jmap f) (inj px) σ with j-⊎⁻ σ
    ... | _ , refl , σ' = inj (app f px σ')

  wanditⱼ : ∀ {p q} {P : Pred A p} {Q : Pred B q} → ∀[ P ⇒ⱼ Q ] → (P ─✴ⱼ Q) (j u)
  app (wanditⱼ f) px σ with j-⊎⁻ σ
  ... | _ , refl , σ' with ⊎-id⁻ˡ σ'
  ... | refl = f px

{- identity morphism -}
module _ {a} {A : Set a} {{r : RawSep A}} {u} {{s₁ : IsUnitalSep r u}} where

  instance id-morph : Morphism A A
  id-morph = record
    { j   = id
    ; j-⊎ = id
    ; j-⊎⁻ = λ x → -, refl , x
    }


text:
------------------------------------------------------------------------------
-- Common (interactive and automatic) properties using the induction principle
------------------------------------------------------------------------------

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

module PA.Inductive.PropertiesByInduction where

open import PA.Inductive.Base

------------------------------------------------------------------------------
-- Congruence properties

succCong : ∀ {m n} → m ≡ n → succ m ≡ succ n
succCong refl = refl

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

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity n = refl

+-rightIdentity : ∀ n → n + zero ≡ n
+-rightIdentity n = ℕ-ind A A0 is n
  where
  A : ℕ → Set
  A i = i + zero ≡ i

  A0 : A zero
  A0 = refl

  is : ∀ i → A i → A (succ i)
  is i ih = succCong ih

+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)
+-assoc m n o = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≡ i + (n + o)

  A0 : A zero
  A0 = refl

  is : ∀ i → A i → A (succ i)
  is i ih = succCong ih

x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)
x+Sy≡S[x+y] m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + succ n ≡ succ (i + n)

  A0 : A zero
  A0 = refl

  is : ∀ i → A i → A (succ i)
  is i ih = succCong ih

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Proof where
-- we give an example of a structure that satisfies the monad laws, but does not have a join operation.

open import Relation.Binary.PropositionalEquality

F : Set → Set₁
F x = Set → x

return : ∀ {x} → x → F x
return = λ z _ → z

_>>=_ : ∀ {x y} -> F x → (x -> F y) → F y
a >>= f = λ z → f (a z) z

-- Notice that the structure (F,return,>>=) satisfies the monad laws:

left-id : ∀ {S₁ S₂} → (f : S₁ → F S₂) → (a : S₁) →
                      (return a >>= f) ≡ f a
left-id f a = refl

right-id :  ∀ {S₁} → (m : F S₁) →
                     (m >>= return) ≡ m
right-id m = refl

assoc :  ∀ {S₁ S₂ S₃} → (f : S₁ → F S₂) → (g : S₂ → F S₃) → (m : F S₁) →
                        (m >>= f) >>= g ≡ m >>= (λ x → f x >>= g)
assoc f g m = refl

-- One could try to define this monad as the structure (F,return,fmap,join).

fmap : ∀ {S₁ S₂} → (S₁ → S₂) → F S₁ → F S₂
fmap f x = λ z → f (x z)

-- However, a definition with signature
---- join : ∀ {x} → F (F x) → F x
-- cannot typecheck, since
---- Set₁ != Set
---- when checking that the expression F x has type Set.

max_stars_repo_name: zaklogician/monads-are-not

max_issues_repo_name: zaklogician/monads-are-not

max_forks_repo_name: zaklogician/monads-are-not


text:
module ExplicitImplicitConversion where
open import ExpressionChanging
open import Data.Nat
open import Data.List
open import ParseTree
open import ScopeState
open import Data.Vec using (Vec ; _∷_)
open import Data.Fin
open import Data.List.NonEmpty
open import AgdaHelperFunctions
open import Data.Bool
open import ParseTreeOperations

-- is given types before conversion
-- namedArgument for type, never just implicit!!!!!!
conversionIns : {n : ℕ} -> Vec Expr n -> Fin n -> (List Expr -> List Expr)
conversionIns Vec.[] () l
conversionIns _ _ [] = []
conversionIns (namedArgument _ {false} ∷ x₁) zero (implicit y ∷ list) = y ∷ list
-- expecting implicit and getting explicit, i.e. argument to be moved
-- isn't specified.
conversionIns (namedArgument _ {false} ∷ x₁) zero (y ∷ list) =  newUnderscore ∷ y ∷ list
conversionIns (x ∷ x₁) zero (x₂ ∷ list) = implicit x₂ ∷ list
conversionIns (namedArgument _ {false} ∷ x₁) (suc n) (implicit x₂ ∷ list) =
  implicit x₂ ∷ conversionIns x₁ n list
conversionIns (namedArgument _ {false} ∷ x₁) (suc n) (x₂ ∷ list) =
  let result = conversionIns x₁ n (x₂ ∷ list)
  in if headImplicit? result then (implicit newUnderscore) ∷ result
        else result
    where headImplicit? : List Expr -> Bool
          headImplicit? (implicit x ∷ l) = true
          headImplicit? _ = false
conversionIns (x ∷ x₁) (suc n) (x₂ ∷ list) = x₂ ∷ conversionIns x₁ n list

convertInExpr : TypeSignature -> ℕ -> ScopeState (List⁺ Expr -> List⁺ Expr)
convertInExpr t n = makeInstruction t n conversionIns

convertInSignature : {n : ℕ} -> Vec Expr (suc n)  -> Fin n -> ScopeState (Vec Expr (suc n))
convertInSignature (namedArgument arg {isExplicit} {c}{c2} ∷ l) zero =
  return $ namedArgument arg {not isExplicit}{c}{c2} ∷ l
convertInSignature (implicit x ∷ l) zero = return $ x ∷ l
convertInSignature (x ∷ l) zero = do
    newName <- getUniqueIdentifier
    return $ namedArgument (typeSignature newName x) {false} {[]} {[]} ∷ l
convertInSignature (x ∷ v) (suc f) = do
    rest <- convertInSignature v f
    return $ x ∷ rest

convert : List ParseTree -> (funcID : ℕ) -> (whichArgument : ℕ) -> ScopeState (List ParseTree)
convert code funcId whichArgument = doForArgument code funcId whichArgument convertInSignature convertInExpr


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

single : {m n : Nat} → suc m ≡ suc n → n ≡ m
single p with refl ← p = refl

double : {m n p : Nat} → suc m ≡ n → suc n ≡ 2 + p → m ≡ p
double p q with refl ← p | refl ← q = refl

_∋_ : (A : Set) → A → A
A ∋ a = a

-- The second equality proof is only well-typed
-- after the first one has been used

tele : {m n : Nat} → suc m ≡ suc n → m ≡ n
tele {m} {n} p
  with refl ← p
       | refl ← (n ≡ m) ∋ refl
       = refl

tele' : {m n : Nat} → m ≡ n → m ≡ n
tele' {m} {n} p with refl ← p with (n ≡ m) ∋ refl
... | q = refl

-- Further splitting after a using & with

tele'' : {m n : Nat} → m ≡ n → Nat → Nat
tele'' {m} {n} p r with refl ← p | (n ≡ m) ∋ refl
tele'' {m} {m} p zero    | q = m
tele'' {m} {m} p (suc r) | q = r

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

module _ {a} {A : Set a} {n} (xs : Vec A (suc n)) where

  head : A
  head with (x ∷ _) ← xs = x

  tail : Vec A n
  tail with (_ ∷ xs) ← xs = xs -- pattern shadows variable with'd on

castVec : ∀ {m n} → m ≡ n → Vec Nat m → Vec Nat n
castVec eq ms with refl ← eq = ms

data All (P : Nat → Set) : ∀ {n} → Vec Nat n → Set where
  []  : All P []
  _∷_ : ∀ {n x xs} → P x → All P {n} xs → All P (x ∷ xs)

open import Agda.Builtin.Sigma

castAll : ∀ {P m n xs ys} → Σ (m ≡ n) (λ eq → castVec eq xs ≡ ys) →
          All P xs → All P ys
castAll (refl , refl) all = all

max_forks_repo_name: hborum/agda