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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.SingleSubst {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening using (id)
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Conversion
open import Definition.LogicalRelation.Substitution.Weakening

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

-- Validity of substitution of single variable in types.
substS : ∀ {F G t Γ l} ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
         ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
         ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
       → Γ ⊩ᵛ⟨ l ⟩ G [ t ] / [Γ]
substS {F} {G} {t} [Γ] [F] [G] [t] {σ = σ} ⊢Δ [σ] =
  let Geq = substConsId G
      G[t] = proj₁ ([G] ⊢Δ ([σ] , (proj₁ ([t] ⊢Δ [σ]))))
      G[t]′ = irrelevance′ Geq G[t]
  in  G[t]′
  ,   (λ {σ′} [σ′] [σ≡σ′] →
         irrelevanceEq″ Geq
                         (substConsId G)
                         G[t] G[t]′
                         (proj₂ ([G] ⊢Δ
                                     ([σ] , proj₁ ([t] ⊢Δ [σ])))
                                     ([σ′] , proj₁ ([t] ⊢Δ [σ′]))
                                     (([σ≡σ′] , (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])))))

-- Validity of substitution of single variable in type equality.
substSEq : ∀ {F F′ G G′ t t′ Γ l} ([Γ] : ⊩ᵛ Γ)
           ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
           ([F′] : Γ ⊩ᵛ⟨ l ⟩ F′ / [Γ])
           ([F≡F′] : Γ ⊩ᵛ⟨ l ⟩ F ≡ F′ / [Γ] / [F])
           ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
           ([G′] : Γ ∙ F′ ⊩ᵛ⟨ l ⟩ G′ / ([Γ] ∙″ [F′]))
           ([G≡G′] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G ≡ G′ / [Γ] ∙″ [F] / [G])
           ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
           ([t′] : Γ ⊩ᵛ⟨ l ⟩ t′ ∷ F′ / [Γ] / [F′])
           ([t≡t′] : Γ ⊩ᵛ⟨ l ⟩ t ≡ t′ ∷ F / [Γ] / [F])
         → Γ ⊩ᵛ⟨ l ⟩ G [ t ] ≡ G′ [ t′ ] / [Γ]
                   / substS {F} {G} {t} [Γ] [F] [G] [t]
substSEq {F} {F′} {G} {G′} {t} {t′}
         [Γ] [F] [F′] [F≡F′] [G] [G′] [G≡G′] [t] [t′] [t≡t′] {σ = σ} ⊢Δ [σ] =
  let Geq = substConsId G
      G′eq = substConsId G′
      G[t] = (proj₁ ([G] ⊢Δ ([σ] , (proj₁ ([t] ⊢Δ [σ])))))
      G[t]′ = irrelevance′ Geq G[t]
      [t]′ = convᵛ {t} {F} {F′} [Γ] [F] [F′] [F≡F′] [t]
      G′[t] = (proj₁ ([G′] ⊢Δ ([σ] , proj₁ ([t]′ ⊢Δ [σ]))))
      G[t]≡G′[t] = irrelevanceEq′ Geq G[t] G[t]′
                                  ([G≡G′] ⊢Δ ([σ] , proj₁ ([t] ⊢Δ [σ])))
      G′[t]≡G′[t′] = irrelevanceEq″ PE.refl G′eq G′[t] G′[t]
                       (proj₂ ([G′] ⊢Δ ([σ] , proj₁ ([t]′ ⊢Δ [σ])))
                              ([σ] , proj₁ ([t′] ⊢Δ [σ]))
                              (reflSubst [Γ] ⊢Δ [σ] ,
                                convEqᵛ {t} {t′} {F} {F′}
                                        [Γ] [F] [F′] [F≡F′] [t≡t′] ⊢Δ [σ]))
      G′[t′] = (proj₁ ([G′] ⊢Δ ([σ] , proj₁ ([t′] ⊢Δ [σ]))))
      G′[t′]′ = irrelevance′ G′eq G′[t′]
  in  transEq G[t]′ G′[t] G′[t′]′ G[t]≡G′[t] G′[t]≡G′[t′]

-- Validity of substitution of single variable in terms.
substSTerm : ∀ {F G t f Γ l} ([Γ] : ⊩ᵛ Γ)
             ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
             ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
             ([f] : Γ ∙ F ⊩ᵛ⟨ l ⟩ f ∷ G / ([Γ] ∙″ [F]) / [G])
             ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
           → Γ ⊩ᵛ⟨ l ⟩ f [ t ] ∷ G [ t ] / [Γ]
                      / substS {F} {G} {t} [Γ] [F] [G] [t]
substSTerm {F} {G} {t} {f} [Γ] [F] [G] [f] [t] {σ = σ} ⊢Δ [σ] =
  let prfG = substConsId G
      prff = substConsId f
      G[t] = proj₁ ([G] ⊢Δ ([σ] , proj₁ ([t] ⊢Δ [σ])))
      G[t]′ = irrelevance′ prfG G[t]
      f[t] = proj₁ ([f] ⊢Δ ([σ] , proj₁ ([t] ⊢Δ [σ])))
      f[t]′ = irrelevanceTerm″ prfG prff G[t] G[t]′ f[t]
  in  f[t]′
  ,   (λ {σ′} [σ′] [σ≡σ′] →
         irrelevanceEqTerm″
           prff
           (substConsId f)
           prfG G[t] G[t]′
           (proj₂ ([f] ⊢Δ ([σ] , proj₁ ([t] ⊢Δ [σ])))
                  ([σ′] , proj₁ ([t] ⊢Δ [σ′]))
                  ([σ≡σ′] , proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])))

-- Validity of substitution of single lifted variable in types.
subst↑S : ∀ {F G t Γ l} ([Γ] : ⊩ᵛ Γ)
          ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
          ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
          ([t] : Γ ∙ F ⊩ᵛ⟨ l ⟩ t ∷ wk1 F / ([Γ] ∙″ [F])
                              / wk1ᵛ {F} {F} [Γ] [F] [F])
        → Γ ∙ F ⊩ᵛ⟨ l ⟩ G [ t ]↑ / ([Γ] ∙″ [F])
subst↑S {F} {G} {t} [Γ] [F] [G] [t] {σ = σ} ⊢Δ [σ] =
  let [wk1F] = wk1ᵛ {F} {F} [Γ] [F] [F]
      [σwk1F] = proj₁ ([wk1F] {σ = σ} ⊢Δ [σ])
      [σwk1F]′ = proj₁ ([F] {σ = tail σ} ⊢Δ (proj₁ [σ]))
      [t]′ = irrelevanceTerm′ (subst-wk F) [σwk1F] [σwk1F]′ (proj₁ ([t] ⊢Δ [σ]))
      G[t] = proj₁ ([G] {σ = consSubst (tail σ) (subst σ t)} ⊢Δ
                               (proj₁ [σ] , [t]′))
      G[t]′ = irrelevance′ (substConsTailId {G} {t} {σ}) G[t]
  in  G[t]′
  ,   (λ {σ′} [σ′] [σ≡σ′] →
         let [σ′t] = irrelevanceTerm′ (subst-wk F)
                                      (proj₁ ([wk1F] {σ = σ′} ⊢Δ [σ′]))
                                      (proj₁ ([F] ⊢Δ (proj₁ [σ′])))
                                      (proj₁ ([t] ⊢Δ [σ′]))
             [σt≡σ′t] = irrelevanceEqTerm′ (subst-wk F) [σwk1F] [σwk1F]′
                                           (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′])
             [σG[t]≡σ′G[t]] = proj₂ ([G] ⊢Δ (proj₁ [σ] , [t]′))
                                    (proj₁ [σ′] , [σ′t])
                                    (proj₁ [σ≡σ′] , [σt≡σ′t])
         in irrelevanceEq″ (substConsTailId {G} {t} {σ}) (substConsTailId {G} {t} {σ′})
                            G[t] G[t]′ [σG[t]≡σ′G[t]])

-- Validity of substitution of single lifted variable in type equality.
subst↑SEq : ∀ {F G G′ t t′ Γ l} ([Γ] : ⊩ᵛ Γ)
            ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
            ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
            ([G′] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G′ / ([Γ] ∙″ [F]))
            ([G≡G′] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G ≡ G′ / [Γ] ∙″ [F] / [G])
            ([t] : Γ ∙ F ⊩ᵛ⟨ l ⟩ t ∷ wk1 F / [Γ] ∙″ [F]
                                / wk1ᵛ {F} {F} [Γ] [F] [F])
            ([t′] : Γ ∙ F ⊩ᵛ⟨ l ⟩ t′ ∷ wk1 F / [Γ] ∙″ [F]
                                 / wk1ᵛ {F} {F} [Γ] [F] [F])
            ([t≡t′] : Γ ∙ F ⊩ᵛ⟨ l ⟩ t ≡ t′ ∷ wk1 F / [Γ] ∙″ [F]
                                   / wk1ᵛ {F} {F} [Γ] [F] [F])
          → Γ ∙ F ⊩ᵛ⟨ l ⟩ G [ t ]↑ ≡ G′ [ t′ ]↑ / [Γ] ∙″ [F]
                        / subst↑S {F} {G} {t} [Γ] [F] [G] [t]
subst↑SEq {F} {G} {G′} {t} {t′}
          [Γ] [F] [G] [G′] [G≡G′] [t] [t′] [t≡t′] {σ = σ} ⊢Δ [σ] =
  let [wk1F] = wk1ᵛ {F} {F} [Γ] [F] [F]
      [σwk1F] = proj₁ ([wk1F] {σ = σ} ⊢Δ [σ])
      [σwk1F]′ = proj₁ ([F] {σ = tail σ} ⊢Δ (proj₁ [σ]))
      [t]′ = irrelevanceTerm′ (subst-wk F) [σwk1F] [σwk1F]′ (proj₁ ([t] ⊢Δ [σ]))
      [t′]′ = irrelevanceTerm′ (subst-wk F) [σwk1F] [σwk1F]′ (proj₁ ([t′] ⊢Δ [σ]))
      [t≡t′]′ = irrelevanceEqTerm′ (subst-wk F) [σwk1F] [σwk1F]′ ([t≡t′] ⊢Δ [σ])
      G[t] = proj₁ ([G] ⊢Δ (proj₁ [σ] , [t]′))
      G[t]′ = irrelevance′ (substConsTailId {G} {t} {σ}) G[t]
      G′[t] = proj₁ ([G′] ⊢Δ (proj₁ [σ] , [t]′))
      G′[t]′ = irrelevance′ (substConsTailId {G′} {t} {σ}) G′[t]
      G′[t′] = proj₁ ([G′] ⊢Δ (proj₁ [σ] , [t′]′))
      G′[t′]′ = irrelevance′ (substConsTailId {G′} {t′} {σ}) G′[t′]
      G[t]≡G′[t] = irrelevanceEq″ (substConsTailId {G} {t} {σ}) (substConsTailId {G′} {t} {σ})
                                   G[t] G[t]′ ([G≡G′] ⊢Δ (proj₁ [σ] , [t]′))
      G′[t]≡G′[t′] = irrelevanceEq″ (substConsTailId {G′} {t} {σ})
                                     (substConsTailId {G′} {t′} {σ})
                                     G′[t] G′[t]′
                                     (proj₂ ([G′] ⊢Δ (proj₁ [σ] , [t]′))
                                            (proj₁ [σ] , [t′]′)
                                            (reflSubst [Γ] ⊢Δ (proj₁ [σ]) , [t≡t′]′))
  in  transEq G[t]′ G′[t]′ G′[t′]′ G[t]≡G′[t] G′[t]≡G′[t′]

-- Helper function for reducible substitution of Π-types with specific typing derivations.
substSΠ₁′ : ∀ {F G t Γ l l′}
           ([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
           ([F] : Γ ⊩⟨ l′ ⟩ F)
           ([t] : Γ ⊩⟨ l′ ⟩ t ∷ F / [F])
         → Γ ⊩⟨ l ⟩ G [ t ]
substSΠ₁′ {t = t} (noemb (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)) [F]₁ [t] =
  let F≡F′ , G≡G′ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
      Feq = PE.trans F≡F′ (PE.sym (wk-id _))
      Geq = PE.cong (λ x → x [ _ ]) (PE.trans (wk-lift-id _) (PE.sym G≡G′))
      ⊢Γ = wf (escape [F]₁)
      [t]′ = irrelevanceTerm′ Feq [F]₁ ([F] id ⊢Γ) [t]
  in  irrelevance′ Geq ([G] id ⊢Γ [t]′)
substSΠ₁′ (emb 0<1 x) [F]₁ [t] = emb′ 0<1 (substSΠ₁′ x [F]₁ [t])

-- Reducible substitution of Π-types.
substSΠ₁ : ∀ {F G t Γ l l′}
           ([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
           ([F] : Γ ⊩⟨ l′ ⟩ F)
           ([t] : Γ ⊩⟨ l′ ⟩ t ∷ F / [F])
         → Γ ⊩⟨ l ⟩ G [ t ]
substSΠ₁ [ΠFG] [F] [t] = substSΠ₁′ (Π-elim [ΠFG]) [F] [t]

-- Helper function for reducible substitution of Π-congurence with specific typing derivations.
substSΠ₂′ : ∀ {F F′ G G′ t t′ Γ l l′ l″ l‴}
           ([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
           ([ΠFG≡ΠF′G′] : Γ ⊩⟨ l ⟩ Π F ▹ G ≡ Π F′ ▹ G′ / Π-intr [ΠFG])
           ([F] : Γ ⊩⟨ l′ ⟩ F)
           ([F′] : Γ ⊩⟨ l′ ⟩ F′)
           ([t] : Γ ⊩⟨ l′ ⟩ t ∷ F / [F])
           ([t′] : Γ ⊩⟨ l′ ⟩ t′ ∷ F′ / [F′])
           ([t≡t′] : Γ ⊩⟨ l′ ⟩ t ≡ t′ ∷ F / [F])
           ([G[t]] : Γ ⊩⟨ l″ ⟩ G [ t ])
           ([G′[t′]] : Γ ⊩⟨ l‴ ⟩ G′ [ t′ ])
         → Γ ⊩⟨ l″ ⟩ G [ t ] ≡ G′ [ t′ ] / [G[t]]
substSΠ₂′ (noemb (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
          (Π₌ F″ G″ D′ A≡B [F≡F′] [G≡G′])
          [F]₁ [F′] [t] [t′] [t≡t′] [G[t]] [G′[t′]] =
  let F≡F′ , G≡G′ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
      F′≡F″ , G′≡G″ = Π-PE-injectivity (whnfRed* D′ Πₙ)
      Feq = PE.trans F≡F′ (PE.sym (wk-id _))
      F′eq = PE.trans F′≡F″ (PE.sym (wk-id _))
      Geq = PE.cong (λ x → x [ _ ]) (PE.trans (wk-lift-id _) (PE.sym G≡G′))
      Geq′ = PE.cong (λ x → x [ _ ]) (PE.trans G′≡G″ (PE.sym (wk-lift-id _)))
      ⊢Γ = wf (escape [F]₁)
      [t]′ = irrelevanceTerm′ Feq [F]₁ ([F] id ⊢Γ) [t]
      [t′]′ = convTerm₂′ F′eq ([F] id ⊢Γ) [F′] ([F≡F′] id ⊢Γ) [t′]
      [t≡t′]′ = irrelevanceEqTerm′ Feq [F]₁ ([F] id ⊢Γ) [t≡t′]
      [Gt≡Gt′] = G-ext id ⊢Γ [t]′ [t′]′ [t≡t′]′
      [Gt′≡G′t′] = [G≡G′] id ⊢Γ [t′]′
  in  irrelevanceEq′ Geq ([G] id ⊢Γ [t]′) [G[t]]
        (transEq′ PE.refl Geq′ ([G] id ⊢Γ [t]′) ([G] id ⊢Γ [t′]′)
                  [G′[t′]] [Gt≡Gt′] [Gt′≡G′t′])
substSΠ₂′ (emb 0<1 x) (ιx y) = substSΠ₂′ x y

-- Reducible substitution of Π-congurence.
substSΠ₂ : ∀ {F F′ G G′ t t′ Γ l l′ l″ l‴}
           ([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
           ([ΠFG≡ΠF′G′] : Γ ⊩⟨ l ⟩ Π F ▹ G ≡ Π F′ ▹ G′ / [ΠFG])
           ([F] : Γ ⊩⟨ l′ ⟩ F)
           ([F′] : Γ ⊩⟨ l′ ⟩ F′)
           ([t] : Γ ⊩⟨ l′ ⟩ t ∷ F / [F])
           ([t′] : Γ ⊩⟨ l′ ⟩ t′ ∷ F′ / [F′])
           ([t≡t′] : Γ ⊩⟨ l′ ⟩ t ≡ t′ ∷ F / [F])
           ([G[t]] : Γ ⊩⟨ l″ ⟩ G [ t ])
           ([G′[t′]] : Γ ⊩⟨ l‴ ⟩ G′ [ t′ ])
         → Γ ⊩⟨ l″ ⟩ G [ t ] ≡ G′ [ t′ ] / [G[t]]
substSΠ₂ [ΠFG] [ΠFG≡ΠF′G′] =
  let [ΠFG≡ΠF′G′]′ = irrelevanceEq [ΠFG] (Π-intr (Π-elim [ΠFG])) [ΠFG≡ΠF′G′]
  in  substSΠ₂′ (Π-elim [ΠFG]) [ΠFG≡ΠF′G′]′

-- Valid substitution of Π-types.
substSΠ : ∀ {F G t Γ l}
          ([Γ] : ⊩ᵛ Γ)
          ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
          ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G / [Γ])
          ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
        → Γ ⊩ᵛ⟨ l ⟩ G [ t ] / [Γ]
substSΠ {F} {G} {t} [Γ] [F] [ΠFG] [t] ⊢Δ [σ] =
  let [σG[t]] = substSΠ₁ (proj₁ ([ΠFG] ⊢Δ [σ])) (proj₁ ([F] ⊢Δ [σ]))
                         (proj₁ ([t] ⊢Δ [σ]))
      [σG[t]]′ = irrelevance′ (PE.sym (singleSubstLift G t))
                          [σG[t]]
  in  [σG[t]]′
  ,   (λ [σ′] [σ≡σ′] →
         irrelevanceEq″ (PE.sym (singleSubstLift G t))
                         (PE.sym (singleSubstLift G t))
                         [σG[t]] [σG[t]]′
                         (substSΠ₂ (proj₁ ([ΠFG] ⊢Δ [σ]))
                                   (proj₂ ([ΠFG] ⊢Δ [σ]) [σ′] [σ≡σ′])
                                   (proj₁ ([F] ⊢Δ [σ])) (proj₁ ([F] ⊢Δ [σ′]))
                                   (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ′]))
                                   (proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]) [σG[t]]
                                   (substSΠ₁ (proj₁ ([ΠFG] ⊢Δ [σ′]))
                                             (proj₁ ([F] ⊢Δ [σ′]))
                                             (proj₁ ([t] ⊢Δ [σ′])))))

-- Valid substitution of Π-congurence.
substSΠEq : ∀ {F G F′ G′ t u Γ l}
            ([Γ] : ⊩ᵛ Γ)
            ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
            ([F′] : Γ ⊩ᵛ⟨ l ⟩ F′ / [Γ])
            ([ΠFG] : Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G / [Γ])
            ([ΠF′G′] : Γ ⊩ᵛ⟨ l ⟩ Π F′ ▹ G′ / [Γ])
            ([ΠFG≡ΠF′G′] : Γ ⊩ᵛ⟨ l ⟩ Π F ▹ G ≡ Π F′ ▹ G′ / [Γ] / [ΠFG])
            ([t]   : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
            ([u]   : Γ ⊩ᵛ⟨ l ⟩ u ∷ F′ / [Γ] / [F′])
            ([t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ F / [Γ] / [F])
          → Γ ⊩ᵛ⟨ l ⟩ G [ t ] ≡ G′ [ u ] / [Γ]
                    / substSΠ {F} {G} {t} [Γ] [F] [ΠFG] [t]
substSΠEq {F} {G} {F′} {G′} {t} {u} [Γ] [F] [F′] [ΠFG] [ΠF′G′] [ΠFG≡ΠF′G′]
           [t] [u] [t≡u] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁ = extractMaybeEmbΠ (Π-elim [σΠFG])
      F≡F₁ , G≡G₁ = Π-PE-injectivity (whnfRed* (red D₁) Πₙ)
      [σΠF′G′] = proj₁ ([ΠF′G′] ⊢Δ [σ])
      Πᵣ F₂ G₂ D₂ ⊢F₂ ⊢G₂ A≡A₂ [F]₂ [G]₂ G-ext₂ = extractMaybeEmbΠ (Π-elim [σΠF′G′])
      F′≡F₂ , G′≡G₂ = Π-PE-injectivity (whnfRed* (red D₂) Πₙ)
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [σF′] = proj₁ ([F′] ⊢Δ [σ])
      [σt] = proj₁ ([t] ⊢Δ [σ])
      [σu] = proj₁ ([u] ⊢Δ [σ])
      [σt]′ = irrelevanceTerm′ (PE.trans F≡F₁ (PE.sym (wk-id F₁)))
                               [σF] ([F]₁ id ⊢Δ) [σt]
      [σu]′ = irrelevanceTerm′ (PE.trans F′≡F₂ (PE.sym (wk-id F₂)))
                               [σF′] ([F]₂ id ⊢Δ) [σu]
      [σt≡σu] = [t≡u] ⊢Δ [σ]
      [G[t]] = irrelevance′ (PE.cong (λ x → x [ subst σ t ])
                                     (PE.trans (wk-lift-id G₁) (PE.sym G≡G₁)))
                            ([G]₁ id ⊢Δ [σt]′)
      [G′[u]] = irrelevance′ (PE.cong (λ x → x [ subst σ u ])
                                      (PE.trans (wk-lift-id G₂) (PE.sym G′≡G₂)))
                             ([G]₂ id ⊢Δ [σu]′)
  in  irrelevanceEq″ (PE.sym (singleSubstLift G t))
                      (PE.sym (singleSubstLift G′ u))
                      [G[t]]
                        (proj₁ (substSΠ {F} {G} {t} [Γ] [F] [ΠFG] [t] ⊢Δ [σ]))
                      (substSΠ₂ {subst σ F} {subst σ F′}
                                {subst (liftSubst σ) G}
                                {subst (liftSubst σ) G′}
                                (proj₁ ([ΠFG] ⊢Δ [σ]))
                                ([ΠFG≡ΠF′G′] ⊢Δ [σ])
                                [σF] [σF′] [σt] [σu] [σt≡σu] [G[t]] [G′[u]])

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable equality over lists using propositional equality
------------------------------------------------------------------------

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

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Data.List.Relation.Binary.Equality.DecPropositional
  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where

open import Data.List using (List)
open import Data.List.Properties using (≡-dec)
import Data.List.Relation.Binary.Equality.Propositional as PropositionalEq
import Data.List.Relation.Binary.Equality.DecSetoid as DecSetoidEq

------------------------------------------------------------------------
-- Publically re-export everything from decSetoid and propositional
-- equality

open PropositionalEq public
open DecSetoidEq (decSetoid _≟_) public
  using (_≋?_; ≋-isDecEquivalence; ≋-decSetoid)

------------------------------------------------------------------------
-- Additional proofs

_≡?_ : Decidable (_≡_ {A = List A})
_≡?_ = ≡-dec _≟_

ext: agda


text:
module Data.Real.Base where

open import Data.Float renaming (Float to ℝ) public

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Semigroup.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Functions.Embedding

open import Cubical.Algebra
open import Cubical.Algebra.Magma.Morphism

private
  variable
    s t : Level

IsSemigroupHom : (S : Semigroup s) (T : Semigroup t) → (⟨ S ⟩ → ⟨ T ⟩) → Type (ℓ-max s t)
IsSemigroupHom S T fun = Homomorphic₂ fun (Semigroup._•_ S) (Semigroup._•_ T)

record SemigroupHom (S : Semigroup s) (T : Semigroup t) : Type (ℓ-max s t) where
  constructor semigrouphom
  field
    fun : ⟨ S ⟩ → ⟨ T ⟩
    isHom : IsSemigroupHom S T fun

record SemigroupEquiv (S : Semigroup s) (T : Semigroup t) : Type (ℓ-max s t) where
  constructor semigroupequiv
  field
    eq : ⟨ S ⟩ ≃ ⟨ T ⟩
    isHom : IsSemigroupHom S T (equivFun eq)

  hom : SemigroupHom S T
  hom = record { isHom = isHom }

instance
  SemigroupHomOperators : HomOperators (Semigroup s) (Semigroup t) (ℓ-max s t)
  SemigroupHomOperators = record { _⟶ᴴ_ = SemigroupHom; _≃ᴴ_ = SemigroupEquiv }

private
  variable
    S : Semigroup s
    T : Semigroup t

SemigroupHom→MagmaHom : (S ⟶ᴴ T) → (Semigroup.magma S ⟶ᴴ Semigroup.magma T)
SemigroupHom→MagmaHom hom .MagmaHom.fun = hom .SemigroupHom.fun
SemigroupHom→MagmaHom hom .MagmaHom.isHom = hom .SemigroupHom.isHom

MagmaHom→SemigroupHom : (Semigroup.magma S ⟶ᴴ Semigroup.magma T) → (S ⟶ᴴ T)
MagmaHom→SemigroupHom hom .SemigroupHom.fun = hom .MagmaHom.fun
MagmaHom→SemigroupHom hom .SemigroupHom.isHom = hom .MagmaHom.isHom

SemigroupHom≃MagmaHom : (S ⟶ᴴ T) ≃ (Semigroup.magma S ⟶ᴴ Semigroup.magma T)
SemigroupHom≃MagmaHom = isoToEquiv (iso SemigroupHom→MagmaHom MagmaHom→SemigroupHom (λ _ → refl) (λ _ → refl))

SemigroupEquiv→MagmaEquiv : S ≃ᴴ T → Semigroup.magma S ≃ᴴ Semigroup.magma T
SemigroupEquiv→MagmaEquiv eq .MagmaEquiv.eq = eq .SemigroupEquiv.eq
SemigroupEquiv→MagmaEquiv eq .MagmaEquiv.isHom = eq .SemigroupEquiv.isHom

MagmaEquiv→SemigroupEquiv : Semigroup.magma S ≃ᴴ Semigroup.magma T → S ≃ᴴ T
MagmaEquiv→SemigroupEquiv eq .SemigroupEquiv.eq = eq .MagmaEquiv.eq
MagmaEquiv→SemigroupEquiv eq .SemigroupEquiv.isHom = eq .MagmaEquiv.isHom

SemigroupEquiv≃MagmaEquiv : (S ≃ᴴ T) ≃ (Semigroup.magma S ≃ᴴ Semigroup.magma T)
SemigroupEquiv≃MagmaEquiv = isoToEquiv (iso SemigroupEquiv→MagmaEquiv MagmaEquiv→SemigroupEquiv (λ _ → refl) (λ _ → refl))


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

module Ch2-5 where

open import Level hiding (lift)

open import Ch2-1
open import Ch2-2
open import Ch2-3
open import Ch2-4

open import Data.Product
open import Function using (_∘_; id)

-- Example 2.5.1 (equivalence)
Example-2-5-1 : ∀ {a b} {A : Set a} {B : Set b}
  → (a a' : A) (b b' : B)
  → ((a , b) ≡ (a' , b')) ≅ ((a ≡ a') × (b ≡ b'))
Example-2-5-1 {_} {_} {A} {B} a a' b b' = f , f-isequiv

  where
    f : ∀ {a b a' b'} → (a , b) ≡ (a' , b') → a ≡ a' × b ≡ b'
    f {a} {b} {a'} {b'} eq = J (A × B) D d (a , b) (a' , b') eq
      where
        D : (x y : A × B) → (p : x ≡ y) → Set _
        D (a , b) (a' , b') p = a ≡ a' × b ≡ b'

        d : (x : A × B) → D x x refl
        d x = refl , refl

    f-isequiv : isequiv f
    f-isequiv = (g , α) , (g , β)
      where
        g : ∀ {a b a' b'} → a ≡ a' × b ≡ b' → (a , b) ≡ (a' , b')
        g {a} {b} {a'} {b'} (fst , snd) = J A D d a a' fst b b' snd
          where
            D : (a a' : A) → (p : a ≡ a') → Set _
            D a a' p = (b b' : B) (q : b ≡ b') → (a , b) ≡ (a' , b')

            d : (x : A) → D x x refl
            d x b b' q = J B E e b b' q
              where
                E : (b b' : B) → (q : b ≡ b') → Set _
                E b b' q = (x , b) ≡ (x , b')

                e : (x : B) → E x x refl
                e x = refl

        α : f ∘ g ~ id
        α (fst , snd) = J A D d a a' fst b b' snd
          where
            D : (x y : A) (p : x ≡ y) → Set _
            D x y p = (x' y' : B) (snd : x' ≡ y')
              → (f ∘ g) (p , snd) ≡ ((p , snd))

            d : (x : A) → D x x refl
            d x x' y' q = J B E e x' y' q
              where
                E : (x' y' : B) (q : x' ≡ y') → Set _
                E x' y' q = (f ∘ g) (refl , q) ≡ ((refl , q))

                e : (x' : B) → E x' x' refl
                e x' = refl

        β : g ∘ f ~ id
        β p = J (A × B) D d (a , b) (a' , b') p
          where
            D : (x y : A × B) (p : x ≡ y) → Set _
            D x y p = (g ∘ f) p ≡ p

            d : (x : A × B) → D x x refl
            d x = refl

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Slice {o ℓ e} (C : Category o ℓ e) where

open Category C
open Equiv

open import Level
open import Relation.Binary using (Rel)

record SliceObj (X : Obj) : Set (o ⊔ ℓ) where
  constructor sliceobj
  field
    {Y} : Obj
    arr : Y ⇒ X

record Slice⇒ {A : Obj} (X Y : SliceObj A) : Set (ℓ ⊔ e) where
  constructor slicearr
  module X = SliceObj X
  module Y = SliceObj Y
  field
    {h} : X.Y ⇒ Y.Y
    .triangle : Y.arr ∘ h ≡ X.arr

slice : Obj → Category _ _ _
slice x = record
  { Obj = Obj′
  ; _⇒_ = _⇒′_
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = slicearr identityʳ
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → assoc′ {f = f} {g} {h}
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≡ = λ {_} {_} {_} {f} {h} {g} {i} → ∘-resp-≡′ {f = f} {h} {g} {i}
  }
  where
  Obj′ = SliceObj x

  _⇒′_ : Rel Obj′ _
  _⇒′_ = Slice⇒

  infixr 9 _∘′_
  infix  4 _≡′_

  _≡′_ : ∀ {A B} → Rel (A ⇒′ B) _
  slicearr {f} _ ≡′ slicearr {g} _ = f ≡ g

  _∘′_ : ∀ {A B C} → (B ⇒′ C) → (A ⇒′ B) → (A ⇒′ C)
  _∘′_ {sliceobj a⇒x} {sliceobj b⇒x} {sliceobj c⇒x} (slicearr {b⇒c} pf₁) (slicearr {a⇒b} pf₂) = slicearr pf
    where
    .pf : c⇒x ∘ (b⇒c ∘ a⇒b) ≡ a⇒x
    pf = begin
           c⇒x ∘ (b⇒c ∘ a⇒b)
         ↑⟨ assoc ⟩
           (c⇒x ∘ b⇒c) ∘ a⇒b
         ↓⟨ ∘-resp-≡ˡ pf₁ ⟩
           b⇒x ∘ a⇒b
         ↓⟨ pf₂ ⟩
           a⇒x
         ∎
      where
      open HomReasoning

  .assoc′ : ∀ {A B C D} {f : A ⇒′ B} {g : B ⇒′ C} {h : C ⇒′ D}
         → (h ∘′ g) ∘′ f ≡′ h ∘′ (g ∘′ f)
  assoc′ = assoc

  .∘-resp-≡′ : ∀ {A B C} {f h : B ⇒′ C} {g i : A ⇒′ B}
           → f ≡′ h
           → g ≡′ i
           → f ∘′ g ≡′ h ∘′ i
  ∘-resp-≡′ f≡h g≡i = ∘-resp-≡ f≡h g≡i

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Formalization.LambdaCalculus.Semantics.CallByName where

import      Lvl
open import Data
open import Formalization.LambdaCalculus
open import Formalization.LambdaCalculus.Semantics
open import Formalization.LambdaCalculus.SyntaxTransformation
open import Logic.Predicate
open import Numeral.Natural
open import Syntax.Number
open import Type

private variable d db : ℕ
private variable f t x : Term(d)
private variable body : Term(db)
private variable v : ∃(Value)

data _⇓_ : Term(d) → ∃(Value) → Type{0} where
  value : ⦃ val : Value(t) ⦄ → (t ⇓ [∃]-intro t)
  apply : (f ⇓ [∃]-intro(Abstract body)) → (substituteVar0 x body ⇓ v) → (Apply f x ⇓ v)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.AbelianGroup
         {g₁ g₂} (G : AbelianGroup g₁ g₂) where

open AbelianGroup G
open import Function
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Publicly re-export group properties

open import Algebra.Properties.Group group public

------------------------------------------------------------------------
-- Properties of abelian groups

private

  lemma₁ : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
  lemma₁ x y = begin
    x ∙ y ∙ x ⁻¹    ≈⟨ ∙-congʳ $ comm _ _ ⟩
    y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩
    y ∙ (x ∙ x ⁻¹)  ≈⟨ ∙-congˡ $ inverseʳ _ ⟩
    y ∙ ε           ≈⟨ identityʳ _ ⟩
    y               ∎

  lemma₂ : ∀ x y → x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ≈ y ⁻¹
  lemma₂ x y = begin
    x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹)  ≈˘⟨ assoc _ _ _ ⟩
    x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹  ≈˘⟨ ∙-congʳ $ assoc _ _ _ ⟩
    x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹    ≈⟨ ∙-congʳ $ inverseʳ _ ⟩
    ε ∙ y ⁻¹                     ≈⟨ identityˡ _ ⟩
    y ⁻¹                         ∎

⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
⁻¹-∙-comm x y = begin
  x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩
  y ⁻¹ ∙ x ⁻¹                         ≈˘⟨ ∙-congʳ $ lemma₂ x y ⟩
  x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma₁ _ _ ⟩
  y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹               ≈⟨ lemma₁ _ _ ⟩
  (x ∙ y) ⁻¹                          ∎


text:
import Relation.Binary.Reasoning.Setoid as SetoidR
open import SingleSorted.AlgebraicTheory

import SingleSorted.Interpretation as Interpretation
import SingleSorted.Model as Model
import SingleSorted.UniversalInterpretation as UniversalInterpretation
import SingleSorted.Substitution as Substitution
import SingleSorted.SyntacticCategory as SyntacticCategory

module SingleSorted.UniversalModel
  {ℓt}
  {Σ : Signature}
  (T : Theory ℓt Σ) where

  open Theory T
  open Substitution T
  open UniversalInterpretation T
  open Interpretation.Interpretation ℐ
  open SyntacticCategory T

  𝒰 : Model.Model T cartesian-𝒮 ℐ
  𝒰 =
     record
        { model-eq = λ ε var-var →
                       let open SetoidR (eq-setoid (ax-ctx ε)) in
                         begin
                         interp-term (ax-lhs ε) var-var ≈⟨ interp-term-self (ax-lhs ε) var-var ⟩
                         ax-lhs ε ≈⟨ id-action ⟩
                         ax-lhs ε [ id-s ]s ≈⟨ eq-axiom ε id-s ⟩
                         ax-rhs ε [ id-s ]s ≈˘⟨ id-action ⟩
                         ax-rhs ε ≈˘⟨ interp-term-self (ax-rhs ε) var-var ⟩
                         interp-term (ax-rhs ε) var-var ∎ }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

open import lib.Base

module lib.Relation where

Rel : ∀ {i} (A : Type i) j → Type (lmax i (lsucc j))
Rel A j = A → A → Type j

Decidable : ∀ {i} {A : Type i} {j} → Rel A j → Type (lmax i j)
Decidable rel = ∀ a₁ a₂ → Dec (rel a₁ a₂)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

module Data.Word8.FromNat where

open import Data.Word8.Primitive
-- open import Agda.Builtin.Bool using (Bool; true)
-- open import Agda.Builtin.Nat using (Nat; _<_)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.FromNat using (Number)

{-
instance
  NumberNat : Number Nat
  NumberNat = record
    { Constraint = λ _ → ⊤
    ; fromNat = λ n → n
    }

data IsTrue : Bool → Set where
  itis : IsTrue true

instance
  indeed : IsTrue true
  indeed = itis
-}

instance
  NumberWord8 : Number Word8
  NumberWord8 = record
    { Constraint = λ n → ⊤ -- IsTrue (n < 256)
    ; fromNat = λ n → primWord8fromNat n
    }

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
module PiQ.Invariants where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Function using (_∘_)
open import PiQ.Syntax
open import PiQ.Opsem
open import PiQ.NoRepeat

-- Reconstruct the whole combinator from context
getℂκ : ∀ {A B} → A ↔ B → Context {A} {B} → ∃[ C ] ∃[ D ] (C ↔ D)
getℂκ c ☐ = _ , _ , c
getℂκ c (☐⨾ c₂ • κ) = getℂκ (c ⨾ c₂) κ
getℂκ c (c₁ ⨾☐• κ) = getℂκ (c₁ ⨾ c) κ
getℂκ c (☐⊕ c₂ • κ) = getℂκ (c ⊕ c₂) κ
getℂκ c (c₁ ⊕☐• κ) = getℂκ (c₁ ⊕ c) κ
getℂκ c (☐⊗[ c₂ , x ]• κ) = getℂκ (c ⊗ c₂) κ
getℂκ c ([ c₁ , x ]⊗☐• κ) = getℂκ (c₁ ⊗ c) κ

getℂ : (st : State) → st ≢ ⊠ → ∃[ A ] ∃[ B ] (A ↔ B)
getℂ ⟨ c ∣ _ ∣ κ ⟩▷  _ = getℂκ c κ
getℂ ［ c ∣ _ ∣ κ ］▷ _ = getℂκ c κ
getℂ ⟨ c ∣ _ ∣ κ ⟩◁ _ = getℂκ c κ
getℂ ［ c ∣ _ ∣ κ ］◁ _ = getℂκ c κ
getℂ ⊠ st≢⊠ = ⊥-elim (st≢⊠ refl)

-- The reconstructed combinator stays the same
ℂInvariant : ∀ {st st'} → st ↦ st' → (¬fail : st ≢ ⊠) → (¬fail' : st' ≢ ⊠) → getℂ st ¬fail ≡ getℂ st' ¬fail'
ℂInvariant ↦⃗₁ _ _ = refl
ℂInvariant ↦⃗₂ _ _ = refl
ℂInvariant ↦⃗₃ _ _ = refl
ℂInvariant ↦⃗₄ _ _ = refl
ℂInvariant ↦⃗₅ _ _ = refl
ℂInvariant ↦⃗₆ _ _ = refl
ℂInvariant ↦⃗₇ _ _ = refl
ℂInvariant ↦⃗₈ _ _ = refl
ℂInvariant ↦⃗₉ _ _ = refl
ℂInvariant ↦⃗₁₀ _ _ = refl
ℂInvariant ↦⃗₁₁ _ _ = refl
ℂInvariant ↦⃗₁₂ _ _ = refl
ℂInvariant ↦⃖₁ _ _ = refl
ℂInvariant ↦⃖₂ _ _ = refl
ℂInvariant ↦⃖₃ _ _ = refl
ℂInvariant ↦⃖₄ _ _ = refl
ℂInvariant ↦⃖₅ _ _ = refl
ℂInvariant ↦⃖₆ _ _ = refl
ℂInvariant ↦⃖₇ _ _ = refl
ℂInvariant ↦⃖₈ _ _ = refl
ℂInvariant ↦⃖₉ _ _ = refl
ℂInvariant ↦⃖₁₀ _ _ = refl
ℂInvariant ↦⃖₁₁ _ _ = refl
ℂInvariant ↦⃖₁₂ _ _ = refl
ℂInvariant ↦η₊₁ _ _ = refl
ℂInvariant ↦η₊₂ _ _ = refl
ℂInvariant ↦ε₊₁ _ _ = refl
ℂInvariant ↦ε₊₂ _ _ = refl
ℂInvariant ↦⃗ηₓ _ _ = refl
ℂInvariant ↦⃖ηₓ₁ _ _ = refl
ℂInvariant ↦⃖ηₓ₂ _ ¬fail' = ⊥-elim (¬fail' refl)
ℂInvariant ↦⃗εₓ₁ _ _ = refl
ℂInvariant ↦⃗εₓ₂ _ ¬fail' = ⊥-elim (¬fail' refl)
ℂInvariant ↦⃖εₓ _ _ = refl

ℂInvariant* : ∀ {st st'} → st ↦* st' → (¬fail : st ≢ ⊠) → (¬fail' : st' ≢ ⊠) → getℂ st ¬fail ≡ getℂ st' ¬fail'
ℂInvariant* {⟨ _ ∣ _ ∣ _ ⟩▷} ◾ _ _ = refl
ℂInvariant* {［ _ ∣ _ ∣ _ ］▷} ◾ _ _ = refl
ℂInvariant* {⟨ _ ∣ _ ∣ _ ⟩◁} ◾ _ _ = refl
ℂInvariant* {［ _ ∣ _ ∣ _ ］◁} ◾ _ _ = refl
ℂInvariant* {⊠} ◾ ¬fail _ = ⊥-elim (¬fail refl)
ℂInvariant* (r ∷ ◾) ¬fail ¬fail' = ℂInvariant r ¬fail ¬fail'
ℂInvariant* (r ∷ (r' ∷ rs)) ¬fail ¬fail' = trans (ℂInvariant r ¬fail λ {refl → ⊠-is-stuck refl (_ , r')})
                                                 (ℂInvariant* (r' ∷ rs) _ ¬fail')

-- Get the type of the deepest context
get𝕌 : ∀ {A B} → Context {A} {B} → 𝕌 × 𝕌
get𝕌 {A} {B} ☐ = A , B
get𝕌 (☐⨾ c₂ • κ) = get𝕌 κ
get𝕌 (c₁ ⨾☐• κ) = get𝕌 κ
get𝕌 (☐⊕ c₂ • κ) = get𝕌 κ
get𝕌 (c₁ ⊕☐• κ) = get𝕌 κ
get𝕌 (☐⊗[ c₂ , x ]• κ) = get𝕌 κ
get𝕌 ([ c₁ , x ]⊗☐• κ) = get𝕌 κ

get𝕌State : (st : State) → st ≢ ⊠ → 𝕌 × 𝕌
get𝕌State ⟨ c ∣ v ∣ κ ⟩▷ _ = get𝕌 κ
get𝕌State ［ c ∣ v ∣ κ ］▷ _ = get𝕌 κ
get𝕌State ⟨ c ∣ v ∣ κ ⟩◁ _ = get𝕌 κ
get𝕌State ［ c ∣ v ∣ κ ］◁ _ = get𝕌 κ
get𝕌State ⊠ nf = ⊥-elim (nf refl)

-- Append a context to another context
appendκ : ∀ {A B} → (ctx : Context {A} {B}) → let (C , D) = get𝕌  ctx
                                              in  Context {C} {D} → Context {A} {B}
appendκ ☐ ctx = ctx
appendκ (☐⨾ c₂ • κ) ctx = ☐⨾ c₂ • appendκ κ ctx
appendκ (c₁ ⨾☐• κ) ctx = c₁ ⨾☐• appendκ κ ctx
appendκ (☐⊕ c₂ • κ) ctx = ☐⊕ c₂ • appendκ κ ctx
appendκ (c₁ ⊕☐• κ) ctx = c₁ ⊕☐• appendκ κ ctx
appendκ (☐⊗[ c₂ , x ]• κ) ctx = ☐⊗[ c₂ , x ]• appendκ κ ctx
appendκ ([ c₁ , x ]⊗☐• κ) ctx = [ c₁ , x ]⊗☐• appendκ κ ctx

appendκState : ∀ st → (nf : st ≢ ⊠)
             → let (A , B) = get𝕌State st nf
               in  Context {A} {B} → State
appendκState ⟨ c ∣ v ∣ κ ⟩▷ _ ctx = ⟨ c ∣ v ∣ appendκ κ ctx ⟩▷
appendκState ［ c ∣ v ∣ κ ］▷ _ ctx = ［ c ∣ v ∣ appendκ κ ctx ］▷
appendκState ⟨ c ∣ v ∣ κ ⟩◁ _ ctx = ⟨ c ∣ v ∣ appendκ κ ctx ⟩◁
appendκState ［ c ∣ v ∣ κ ］◁ _ ctx = ［ c ∣ v ∣ appendκ κ ctx ］◁
appendκState ⊠ nf = ⊥-elim (nf refl)

-- The type of context does not change during execution
𝕌Invariant : ∀ {st st'} → st ↦ st' → (nf : st ≢ ⊠) → (nf' : st' ≢ ⊠) → get𝕌State st nf ≡ get𝕌State st' nf'
𝕌Invariant ↦⃗₁ nf nf' = refl
𝕌Invariant ↦⃗₂ nf nf' = refl
𝕌Invariant ↦⃗₃ nf nf' = refl
𝕌Invariant ↦⃗₄ nf nf' = refl
𝕌Invariant ↦⃗₅ nf nf' = refl
𝕌Invariant ↦⃗₆ nf nf' = refl
𝕌Invariant ↦⃗₇ nf nf' = refl
𝕌Invariant ↦⃗₈ nf nf' = refl
𝕌Invariant ↦⃗₉ nf nf' = refl
𝕌Invariant ↦⃗₁₀ nf nf' = refl
𝕌Invariant ↦⃗₁₁ nf nf' = refl
𝕌Invariant ↦⃗₁₂ nf nf' = refl
𝕌Invariant ↦⃖₁ nf nf' = refl
𝕌Invariant ↦⃖₂ nf nf' = refl
𝕌Invariant ↦⃖₃ nf nf' = refl
𝕌Invariant ↦⃖₄ nf nf' = refl
𝕌Invariant ↦⃖₅ nf nf' = refl
𝕌Invariant ↦⃖₆ nf nf' = refl
𝕌Invariant ↦⃖₇ nf nf' = refl
𝕌Invariant ↦⃖₈ nf nf' = refl
𝕌Invariant ↦⃖₉ nf nf' = refl
𝕌Invariant ↦⃖₁₀ nf nf' = refl
𝕌Invariant ↦⃖₁₁ nf nf' = refl
𝕌Invariant ↦⃖₁₂ nf nf' = refl
𝕌Invariant ↦η₊₁ nf nf' = refl
𝕌Invariant ↦η₊₂ nf nf' = refl
𝕌Invariant ↦ε₊₁ nf nf' = refl
𝕌Invariant ↦ε₊₂ nf nf' = refl
𝕌Invariant ↦⃗ηₓ nf nf' = refl
𝕌Invariant ↦⃖ηₓ₁ nf nf' = refl
𝕌Invariant ↦⃖ηₓ₂ nf nf' = ⊥-elim (nf' refl)
𝕌Invariant ↦⃗εₓ₁ nf nf' = refl
𝕌Invariant ↦⃗εₓ₂ nf nf' = ⊥-elim (nf' refl)
𝕌Invariant ↦⃖εₓ nf nf' = refl

𝕌Invariant* : ∀ {st st'} → st ↦* st' → (nf : st ≢ ⊠) → (nf' : st' ≢ ⊠) → get𝕌State st nf ≡  get𝕌State st' nf'
𝕌Invariant* {⟨ _ ∣ _ ∣ _ ⟩▷} ◾ nf nf' = refl
𝕌Invariant* {［ _ ∣ _ ∣ _ ］▷} ◾ nf nf' = refl
𝕌Invariant* {⟨ _ ∣ _ ∣ _ ⟩◁} ◾ nf nf' = refl
𝕌Invariant* {［ _ ∣ _ ∣ _ ］◁} ◾ nf nf' = refl
𝕌Invariant* {⊠} ◾ nf nf' = ⊥-elim (nf' refl)
𝕌Invariant* (r ∷ ◾) nf nf' = 𝕌Invariant r nf nf'
𝕌Invariant* (r ∷ (r' ∷ rs)) nf nf' = trans (𝕌Invariant r nf nf'') (𝕌Invariant* (r' ∷ rs) nf'' nf')
  where
  nf'' = λ eq → ⊠-is-stuck eq (_ , r')

-- Appending context does not affect reductions
appendκ↦ : ∀ {st st'} → (r : st ↦ st') (nf : st ≢ ⊠) (nf' : st' ≢ ⊠) (eq : get𝕌State st nf ≡  get𝕌State st' nf')
         → (κ : Context {proj₁ (get𝕌State st nf)} {proj₂ (get𝕌State st nf)})
         → appendκState st nf κ ↦ appendκState st' nf' (subst (λ {(A , B) → Context {A} {B}}) eq κ)
appendκ↦ ↦⃗₁ nf nf' refl ctx = ↦⃗₁
appendκ↦ ↦⃗₂ nf nf' refl ctx = ↦⃗₂
appendκ↦ ↦⃗₃ nf nf' refl ctx = ↦⃗₃
appendκ↦ ↦⃗₄ nf nf' refl ctx = ↦⃗₄
appendκ↦ ↦⃗₅ nf nf' refl ctx = ↦⃗₅
appendκ↦ ↦⃗₆ nf nf' refl ctx = ↦⃗₆
appendκ↦ ↦⃗₇ nf nf' refl ctx = ↦⃗₇
appendκ↦ ↦⃗₈ nf nf' refl ctx = ↦⃗₈
appendκ↦ ↦⃗₉ nf nf' refl ctx = ↦⃗₉
appendκ↦ ↦⃗₁₀ nf nf' refl ctx = ↦⃗₁₀
appendκ↦ ↦⃗₁₁ nf nf' refl ctx = ↦⃗₁₁
appendκ↦ ↦⃗₁₂ nf nf' refl ctx = ↦⃗₁₂
appendκ↦ ↦⃖₁ nf nf' refl ctx = ↦⃖₁
appendκ↦ ↦⃖₂ nf nf' refl ctx = ↦⃖₂
appendκ↦ ↦⃖₃ nf nf' refl ctx = ↦⃖₃
appendκ↦ ↦⃖₄ nf nf' refl ctx = ↦⃖₄
appendκ↦ ↦⃖₅ nf nf' refl ctx = ↦⃖₅
appendκ↦ ↦⃖₆ nf nf' refl ctx = ↦⃖₆
appendκ↦ ↦⃖₇ nf nf' refl ctx = ↦⃖₇
appendκ↦ ↦⃖₈ nf nf' refl ctx = ↦⃖₈
appendκ↦ ↦⃖₉ nf nf' refl ctx = ↦⃖₉
appendκ↦ ↦⃖₁₀ nf nf' refl ctx = ↦⃖₁₀
appendκ↦ ↦⃖₁₁ nf nf' refl ctx = ↦⃖₁₁
appendκ↦ ↦⃖₁₂ nf nf' refl ctx = ↦⃖₁₂
appendκ↦ ↦η₊₁ nf nf' refl ctx = ↦η₊₁
appendκ↦ ↦η₊₂ nf nf' refl ctx = ↦η₊₂
appendκ↦ ↦ε₊₁ nf nf' refl ctx = ↦ε₊₁
appendκ↦ ↦ε₊₂ nf nf' refl ctx = ↦ε₊₂
appendκ↦ ↦⃗ηₓ nf nf' refl ctx = ↦⃗ηₓ
appendκ↦ (↦⃖ηₓ₁ {eq = eq}) nf nf' refl ctx = ↦⃖ηₓ₁ {eq = eq}
appendκ↦ ↦⃖ηₓ₂ nf nf' eq ctx = ⊥-elim (nf' refl)
appendκ↦ (↦⃗εₓ₁ {eq = eq}) nf nf' refl ctx = ↦⃗εₓ₁ {eq = eq}
appendκ↦ ↦⃗εₓ₂ nf nf' eq ctx = ⊥-elim (nf' refl)
appendκ↦ ↦⃖εₓ nf nf' refl ctx = ↦⃖εₓ

appendκ↦* : ∀ {st st'} → (r : st ↦* st') (nf : st ≢ ⊠) (nf' : st' ≢ ⊠) (eq : get𝕌State st nf ≡  get𝕌State st' nf')
          → (κ : Context {proj₁ (get𝕌State st nf)} {proj₂ (get𝕌State st nf)})
          → appendκState st nf κ ↦* appendκState st' nf' (subst (λ {(A , B) → Context {A} {B}}) eq κ)
appendκ↦* {⟨ _ ∣ _ ∣ _ ⟩▷} ◾ nf nf' refl ctx = ◾
appendκ↦* {［ _ ∣ _ ∣ _ ］▷} ◾ nf nf' refl ctx = ◾
appendκ↦* {⟨ _ ∣ _ ∣ _ ⟩◁} ◾ nf nf' refl ctx = ◾
appendκ↦* {［ _ ∣ _ ∣ _ ］◁} ◾ nf nf' refl ctx = ◾
appendκ↦* {⊠} ◾ nf nf' eq ctx = ⊥-elim (nf' refl)
appendκ↦* (↦⃗₁ {b = b} {v} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₁ {b = b} {v} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₂ {v = v} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₂ {v = v} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₃ {v = v} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₃ {v = v} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₄ {x = x} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₄ {x = x} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₅ {y = y} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₅ {y = y} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₆ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₆ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₇ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₇ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₈ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₈ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₉ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₉ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₁₀ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₁₀ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₁₁ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₁₁ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗₁₂ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗₁₂ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₁ {b = b} {v} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₁ {b = b} {v} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₂ {v = v} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₂ {v = v} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₃ {v = v} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₃ {v = v} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₄ {x = x} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₄ {x = x} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₅ {y = y} {κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₅ {y = y} {κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₆ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₆ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₇ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₇ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₈ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₈ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₉ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₉ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₁₀ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₁₀ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₁₁ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₁₁ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖₁₂ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖₁₂ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦η₊₁ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦η₊₁ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦η₊₂ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦η₊₂ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦ε₊₁ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦ε₊₁ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦ε₊₂ {κ = κ} ∷ rs) nf nf' eq ctx = appendκ↦ (↦ε₊₂ {κ = κ}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗ηₓ ∷ rs) nf nf' eq ctx = appendκ↦ ↦⃗ηₓ nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖ηₓ₁ {eq = eq'} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃖ηₓ₁ {eq = eq'}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃖ηₓ₂ ∷ ◾) nf nf' eq ctx = ⊥-elim (nf' refl)
appendκ↦* (↦⃗εₓ₁ {eq = eq'} ∷ rs) nf nf' eq ctx = appendκ↦ (↦⃗εₓ₁ {eq = eq'}) nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx
appendκ↦* (↦⃗εₓ₂ ∷ ◾) nf nf' eq ctx = ⊥-elim (nf' refl)
appendκ↦* (↦⃖εₓ ∷ rs) nf nf' eq ctx = appendκ↦ ↦⃖εₓ nf (λ ()) refl ctx ∷ appendκ↦* rs (λ ()) nf' eq ctx

appendκ↦⊠ : ∀ {st} → (r : st ↦ ⊠) (nf : st ≢ ⊠)
          → (κ : Context {proj₁ (get𝕌State st nf)} {proj₂ (get𝕌State st nf)})
          → appendκState st nf κ ↦ ⊠
appendκ↦⊠ (↦⃖ηₓ₂ {neq = neq}) nf ctx = ↦⃖ηₓ₂ {neq = neq}
appendκ↦⊠ (↦⃗εₓ₂ {neq = neq}) nf ctx = ↦⃗εₓ₂ {neq = neq}

appendκ↦*⊠ : ∀ {st} → (r : st ↦* ⊠) (nf : st ≢ ⊠)
           → (κ : Context {proj₁ (get𝕌State st nf)} {proj₂ (get𝕌State st nf)})
           → appendκState st nf κ ↦* ⊠
appendκ↦*⊠ ◾ nf ctx = ⊥-elim (nf refl)
appendκ↦*⊠ (r ∷ ◾) nf ctx = appendκ↦⊠ r nf ctx ∷ ◾
appendκ↦*⊠ (↦⃗₁ ∷ (r' ∷ rs)) nf ctx = ↦⃗₁ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₂ ∷ (r' ∷ rs)) nf ctx = ↦⃗₂ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₃ ∷ (r' ∷ rs)) nf ctx = ↦⃗₃ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₄ ∷ (r' ∷ rs)) nf ctx = ↦⃗₄ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₅ ∷ (r' ∷ rs)) nf ctx = ↦⃗₅ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₆ ∷ (r' ∷ rs)) nf ctx = ↦⃗₆ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₇ ∷ (r' ∷ rs)) nf ctx = ↦⃗₇ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₈ ∷ (r' ∷ rs)) nf ctx = ↦⃗₈ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₉ ∷ (r' ∷ rs)) nf ctx = ↦⃗₉ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₁₀ ∷ (r' ∷ rs)) nf ctx = ↦⃗₁₀ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₁₁ ∷ (r' ∷ rs)) nf ctx = ↦⃗₁₁ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗₁₂ ∷ (r' ∷ rs)) nf ctx = ↦⃗₁₂ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₁ ∷ (r' ∷ rs)) nf ctx = ↦⃖₁ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₂ ∷ (r' ∷ rs)) nf ctx = ↦⃖₂ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₃ ∷ (r' ∷ rs)) nf ctx = ↦⃖₃ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₄ ∷ (r' ∷ rs)) nf ctx = ↦⃖₄ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₅ ∷ (r' ∷ rs)) nf ctx = ↦⃖₅ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₆ ∷ (r' ∷ rs)) nf ctx = ↦⃖₆ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₇ ∷ (r' ∷ rs)) nf ctx = ↦⃖₇ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₈ ∷ (r' ∷ rs)) nf ctx = ↦⃖₈ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₉ ∷ (r' ∷ rs)) nf ctx = ↦⃖₉ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₁₀ ∷ (r' ∷ rs)) nf ctx = ↦⃖₁₀ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₁₁ ∷ (r' ∷ rs)) nf ctx = ↦⃖₁₁ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖₁₂ ∷ (r' ∷ rs)) nf ctx = ↦⃖₁₂ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦η₊₁ ∷ (r' ∷ rs)) nf ctx = ↦η₊₁ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦η₊₂ ∷ (r' ∷ rs)) nf ctx = ↦η₊₂ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦ε₊₁ ∷ (r' ∷ rs)) nf ctx = ↦ε₊₁ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦ε₊₂ ∷ (r' ∷ rs)) nf ctx = ↦ε₊₂ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗ηₓ ∷ (r' ∷ rs)) nf ctx = ↦⃗ηₓ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖ηₓ₁ {eq = eq} ∷ (r' ∷ rs)) nf ctx = ↦⃖ηₓ₁ {eq = eq} ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃗εₓ₁ {eq = eq} ∷ (r' ∷ rs)) nf ctx = ↦⃗εₓ₁ {eq = eq} ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx
appendκ↦*⊠ (↦⃖εₓ ∷ (r' ∷ rs)) nf ctx = ↦⃖εₓ ∷ appendκ↦*⊠ (r' ∷ rs) (λ ()) ctx


text:
module Pi-.Dir where
open import Relation.Binary.PropositionalEquality

data Dir : Set where
  ◁ : Dir
  ▷ : Dir

-ᵈⁱʳ_ : Dir → Dir
-ᵈⁱʳ ▷ = ◁
-ᵈⁱʳ ◁ = ▷

_×ᵈⁱʳ_ : Dir → Dir → Dir
◁ ×ᵈⁱʳ ◁ = ▷
◁ ×ᵈⁱʳ ▷ = ◁
▷ ×ᵈⁱʳ ◁ = ◁
▷ ×ᵈⁱʳ ▷ = ▷

identˡᵈⁱʳ : ∀ d → ▷ ×ᵈⁱʳ d ≡ d
identˡᵈⁱʳ ◁ = refl
identˡᵈⁱʳ ▷ = refl

assoclᵈⁱʳ : ∀ d₁ d₂ d₃ → d₁ ×ᵈⁱʳ (d₂ ×ᵈⁱʳ d₃) ≡ (d₁ ×ᵈⁱʳ d₂) ×ᵈⁱʳ d₃
assoclᵈⁱʳ ◁ ◁ ◁ = refl
assoclᵈⁱʳ ◁ ◁ ▷ = refl
assoclᵈⁱʳ ◁ ▷ ◁ = refl
assoclᵈⁱʳ ◁ ▷ ▷ = refl
assoclᵈⁱʳ ▷ ◁ ◁ = refl
assoclᵈⁱʳ ▷ ◁ ▷ = refl
assoclᵈⁱʳ ▷ ▷ ◁ = refl
assoclᵈⁱʳ ▷ ▷ ▷ = refl

commᵈⁱʳ : ∀ d₁ d₂ → d₁ ×ᵈⁱʳ d₂ ≡ d₂ ×ᵈⁱʳ d₁
commᵈⁱʳ ◁ ◁ = refl
commᵈⁱʳ ◁ ▷ = refl
commᵈⁱʳ ▷ ◁ = refl
commᵈⁱʳ ▷ ▷ = refl

assocl-commᵈⁱʳ : ∀ d₁ d₂ d₃ → d₁ ×ᵈⁱʳ (d₂ ×ᵈⁱʳ d₃) ≡ (d₂ ×ᵈⁱʳ d₁) ×ᵈⁱʳ d₃
assocl-commᵈⁱʳ ◁ ◁ ◁ = refl
assocl-commᵈⁱʳ ◁ ◁ ▷ = refl
assocl-commᵈⁱʳ ◁ ▷ ◁ = refl
assocl-commᵈⁱʳ ◁ ▷ ▷ = refl
assocl-commᵈⁱʳ ▷ ◁ ◁ = refl
assocl-commᵈⁱʳ ▷ ◁ ▷ = refl
assocl-commᵈⁱʳ ▷ ▷ ◁ = refl
assocl-commᵈⁱʳ ▷ ▷ ▷ = refl

assoc-commᵈⁱʳ : ∀ d₁ d₂ d₃ → d₁ ×ᵈⁱʳ (d₂ ×ᵈⁱʳ d₃) ≡ d₂ ×ᵈⁱʳ (d₁ ×ᵈⁱʳ d₃)
assoc-commᵈⁱʳ ◁ ◁ ◁ = refl
assoc-commᵈⁱʳ ◁ ◁ ▷ = refl
assoc-commᵈⁱʳ ◁ ▷ ◁ = refl
assoc-commᵈⁱʳ ◁ ▷ ▷ = refl
assoc-commᵈⁱʳ ▷ ◁ ◁ = refl
assoc-commᵈⁱʳ ▷ ◁ ▷ = refl
assoc-commᵈⁱʳ ▷ ▷ ◁ = refl
assoc-commᵈⁱʳ ▷ ▷ ▷ = refl


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

module Parametrized where

open import Generics

open import Agda.Primitive
open import Function.Base
open import Data.Nat.Base hiding (pred)
open import Data.Fin.Base hiding (pred; _+_)
open import Data.List.Base hiding (sum; length)

open import Relation.Nullary
open import Relation.Nullary.Decidable as Decidable
open import Relation.Binary.HeterogeneousEquality.Core using (_≅_; refl)
open import Relation.Binary.PropositionalEquality

open import Data.String hiding (show; _≟_; length)
open import Data.Maybe.Base

module Nat where

  instance
    natD : HasDesc ℕ
    natD = deriveDesc ℕ

  ---------------------------
  -- Deriving the eliminator

  elimℕ = deriveElim natD

  plus : ℕ → ℕ → ℕ
  plus n = elimℕ (const ℕ) n suc

  mult : ℕ → ℕ → ℕ
  mult n = elimℕ (const ℕ) 0 (plus n)

  -- things defined with the eliminator reduce properly on open terms

  plus0 : ∀ {n} → plus n 0 ≡ n
  plus0 = refl

  plusS : ∀ {n m} → plus n (suc m) ≡ suc (plus n m)
  plusS = refl

  mult0 : ∀ {n} → mult n 0 ≡ 0
  mult0 = refl

  multS : ∀ {n m} → mult n (suc m) ≡ plus n (mult n m)
  multS = refl

  -----------------
  -- Deriving fold

  foldℕ = deriveFold natD

  t : ℕ
  t = foldℕ 1 suc 2

  -----------------
  -- Deriving show

  instance showℕ : Show ℕ
           showℕ = deriveShow natD

  _ : show 2 ≡ "suc (suc (zero))"
  _ = refl

  ------------------------------------
  -- Deriving case analysis principle

  caseℕ = deriveCase natD

  pred : ℕ → ℕ
  pred = caseℕ (const ℕ) 0 id

  pred0 : pred 0 ≡ 0
  pred0 = refl

  predS : ∀ {n} → pred (suc n) ≡ n
  predS = refl

  -----------------------
  -- Deriving congruence

  congℕ = deriveCong natD

  ze≅ze : 0 ≅ 0
  ze≅ze = congℕ zero

  su≅su : ∀ {n m} → n ≅ m → suc n ≅ suc m
  su≅su = congℕ (suc zero)

  -------------------------------
  -- Deriving decidable equality

  instance decℕ : DecEq ℕ
           decℕ = deriveDecEq natD

  _ : 3 ≟ 3 ≡ yes refl
  _ = refl

  _ : 3 ≟ 2 ≡ no _
  _ = refl

module ListDemo where

  data list (A : Set) : Set where
    []  : list A
    _∷_ : A → list A → list A

  listD : HasDesc list
  listD = deriveDesc list

  foldList = deriveFold listD

  sum : list ℕ → ℕ
  sum = foldList 0 _+_

  []-sum : sum [] ≡ 0
  []-sum = refl

  ∷-sum : ∀ {x xs} → sum (x ∷ xs) ≡ x + sum xs
  ∷-sum = refl

  mul : list ℕ → ℕ
  mul = foldList 1 _*_

module Vec where
  private variable A : Set
                   n : ℕ

  data Vec (A : Set) : ℕ → Set where
    nil  : Vec A 0
    cons : ∀ {n} → A → Vec A n → Vec A (suc n)

  instance
    vekD : HasDesc Vec
    vekD = deriveDesc Vec

  ---------------------------
  -- Deriving the eliminator

  elimVec = deriveElim vekD

  length : Vec A n → ℕ
  length = elimVec (const ℕ) 0 (const suc)

  length0 : length (nil {A}) ≡ 0
  length0 = refl

  lengthP : (x : Vec A n) → length x ≡ n
  lengthP = elimVec (λ {n} x → length x ≡ n) refl (const (cong suc))

  ---------------------------
  -- Deriving fold

  foldVec = deriveFold vekD

  vekToList : ∀ {A n} → Vec A n → List A
  vekToList = foldVec [] _∷_

  -----------------------
  -- Deriving congruence

  congV = deriveCong vekD

  []≅[] : ∀ {A} → nil {A} ≅ nil {A}
  []≅[] = congV zero

  cong-cons : ∀ {A n} {x y : A} → x ≅ y → {xs ys : Vec A n} → xs ≅ ys
            → cons x xs ≅ cons y ys
  cong-cons = congV (suc zero) refl

module WType  where

  private variable A : Set
                   B : A → Set
                   c : Level

  data W (A : Set) (B : A → Set) : Set where
    node : ∀ x → (B x → W A B) → W A B

  wD : HasDesc W
  wD = deriveDesc W

  ---------------------------
  -- Deriving the eliminator

  elimW : (Pr : W A B → Set c)
        → (∀ x {g} → (∀ y → Pr (g y)) → Pr (node x g) )
        → ∀ x → Pr x
  elimW = deriveElim wD

  elimW-node
    : {Pr : W A B → Set c}
      (M : ∀ x {g} → (∀ y → Pr (g y)) → Pr (node x g) )
    → ∀ {x g}
    → elimW Pr M (node x g) ≡ M x (λ y → elimW Pr M (g y))
  elimW-node M = refl

module Irrelevance where

  data Squash (A : Set) : Set where
    squash : .(x : A) → Squash A

  -- Irrelevant arguments are supported
  squashD : HasDesc Squash
  squashD = deriveDesc Squash

  -----------------
  -- Deriving fold

  foldSquash : ∀ {A X : Set} → (.A → X) → Squash A → X
  foldSquash = deriveFold squashD

  ------------------------------
  -- Deriving printing function

  -- Because the value of type A is irrelevant,
  -- we don't require an instance of Show A
  instance showSquash : ∀ {A} → Show (Squash A)
           showSquash = deriveShow squashD

  _ : show (squash 3) ≡ "squash (._)"
  _ = refl

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


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

-- Constructions of a Cocone from the Twisted Arrow function from a Cowedge
-- and vice-versa, by Duality.
-- Note that the proper functioning of this relies crucially on
-- Functor.op (Functor.op F) being definitionally equal to F.

open import Categories.Category using (Category)
open import Categories.Functor.Bifunctor using (Bifunctor)

module Categories.Diagram.Cowedge.Properties {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

open import Level

open import Categories.Category.Construction.Cocones using (Cocones)
open import Categories.Category.Construction.Cowedges
open import Categories.Category.Construction.TwistedArrow
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Diagram.Cocone
open import Categories.Diagram.Cowedge
open import Categories.Diagram.Duality
open import Categories.Diagram.Wedge.Properties
open import Categories.Functor hiding (id)
open import Categories.Functor.Instance.Twisted C D
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation.Dinatural
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)

Cowedge-to-Cocone : (W : Cowedge F) → Cocone (Twist′ F)
Cowedge-to-Cocone W = coCone⇒Cocone D (Wedge-to-Cone (Functor.op F) (Cowedge⇒coWedge D W))

Cocone-to-Cowedge : Cocone (Twist′ F) → Cowedge F
Cocone-to-Cowedge C = coWedge⇒Cowedge D (Cone-to-Wedge (Functor.op F) (Cocone⇒coCone D C))

CooneTwist⇒CowedgeF : Functor (Cocones (Twist′ F)) (Cowedges F)
CooneTwist⇒CowedgeF = record
  { F₀ = Cocone-to-Cowedge
  ; F₁ = λ co⇒ → record { u = arr co⇒ ; commute = commute co⇒ }
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈ = λ f≈g → f≈g
  }
  where
  open Cocone⇒
  open Category D

Cowedge⇒CoconeTwistF : Functor (Cowedges F) (Cocones (Twist′ F))
Cowedge⇒CoconeTwistF = record
  { F₀ = Cowedge-to-Cocone
  ; F₁ = λ we⇒ → record
    { arr = u we⇒
    ; commute = pullˡ (commute we⇒)
    }
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈ = λ f≈g → f≈g
  }
  where
  open Cowedge
  open Cowedge-Morphism
  open Category D
  open MR D

-- The duality here is not just 'op', so spell out some of it.  Note how the proofs need the explicit commutations.
CoconesTwist≅Cowedges : StrongEquivalence (Cocones (Twist′ F)) (Cowedges F)
CoconesTwist≅Cowedges = record
  { F = CooneTwist⇒CowedgeF
  ; G = Cowedge⇒CoconeTwistF
  ; weak-inverse = record
    { F∘G≈id = niHelper (record
      { η = λ X → record { u = id ; commute = identityˡ ○ MR.elimʳ D identity }
      ; η⁻¹ = λ X → record { u = id ; commute = MR.id-comm-sym D ○ (refl⟩∘⟨ Equiv.sym identity) }
      ; commute = λ _ → MR.id-comm-sym D
      ; iso = λ _ → record { isoˡ = identity² ; isoʳ = identity² }
      })
    ; G∘F≈id = niHelper record
      { η = λ X → record { arr = id ; commute = λ {Y} → identityˡ ○ Coapex.commute (coapex X) (mor⇒ (MR.elimˡ C C.identity²)) }
      ; η⁻¹ = λ X → record { arr = id ; commute = λ {Y} → identityˡ ○ Equiv.sym (Coapex.commute (coapex X) (mor⇒ (MR.elimˡ C C.identity²))) }
      ; commute = λ _ → MR.id-comm-sym D
      ; iso = λ X → record { isoˡ = identity² ; isoʳ = identity² }
      }
    }
  }
  where
  module C = Category C
  open Category D
  open HomReasoning
  open Cocone
  open Functor F
  open Cowedge
  open DinaturalTransformation

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module InstanceArgumentsSections where

postulate A : Set

module Basic where
  record B : Set where
    field bA : A

  open B {{...}}

  bA' : B → A
  bA' _ = bA

module Parameterised (a : A) where
  record C : Set where
    field cA : A

  open C {{...}}

  cA' : C → A
  cA' _ = cA

module RecordFromParameterised where
  postulate a : A

  open Parameterised a
  open C {{...}}

  cA'' : C → A
  cA'' _ = cA

module RecordFromParameterisedInParameterised (a : A) where

  open Parameterised a
  open C {{...}}

  cA'' : C → A
  cA'' _ = cA

module RecordFromParameterised' (a : A) where

  open Parameterised
  open C {{...}}

  cA'' : C a → A
  cA'' _ = cA a

module AppliedRecord (a : A) where
  open Parameterised

  D : Set
  D = C a

  module D = C a
  open D {{...}}

  dA' : D → A
  dA' _ = cA

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

import Level

open import Data.Empty
open import Data.Product
open import Data.List using (_∷_; []; _++_)
open import Data.List.Properties using (∷-injectiveʳ)

open import Relation.Unary using (Pred; _⊆_; _∈_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst)

open import Common

module TraceSet {ℙ : Set} (message : Message ℙ)
  where

open import Trace message
open import SessionType message
open import Transitions message
open import HasTrace message

TraceSet : Set₁
TraceSet = Pred Trace Level.zero

⟦_⟧ : SessionType -> TraceSet
⟦_⟧ = _HasTrace_

_⊆⊇_ : TraceSet -> TraceSet -> Set
X ⊆⊇ Y = X ⊆ Y × Y ⊆ X

PrefixClosed : TraceSet -> Set
PrefixClosed X = ∀{φ ψ} -> ψ ⊑ φ -> X φ -> X ψ

Coherent : TraceSet -> Set
Coherent X = ∀{φ ψ₁ ψ₂ x y} -> X (φ ++ I x ∷ ψ₁) -> X (φ ++ O y ∷ ψ₂) -> ⊥

_∂_ : TraceSet -> Action -> TraceSet
(X ∂ α) φ = X (α ∷ φ)

--| CO-SETS |--

CoSet : TraceSet -> TraceSet
CoSet X φ = X (co-trace φ)

co-set-involution : ∀{X} -> CoSet (CoSet X) ≡ X
co-set-involution {X} =
  extensionality λ φ -> subst (λ z -> X z ≡ X φ) (sym (co-trace-involution φ)) refl

co-set-⊆ : ∀{X Y} -> X ⊆ Y -> CoSet X ⊆ CoSet Y
co-set-⊆ sub xcφ = sub xcφ

co-set-right->left : ∀{X Y} -> X ⊆ CoSet Y -> CoSet X ⊆ Y
co-set-right->left {X} {Y} sub xcφ with co-set-⊆ {X} {CoSet Y} sub
... | sub' = subst Y (co-trace-involution _) (sub' xcφ)

co-definition : ∀{X φ} -> φ ∈ X -> co-trace φ ∈ CoSet X
co-definition {_} {φ} xφ rewrite co-trace-involution φ = xφ

co-inversion : ∀{X φ} -> co-trace φ ∈ CoSet X -> φ ∈ X
co-inversion {_} {φ} coφ rewrite co-trace-involution φ = coφ

--| MAXIMAL TRACES |--

data Maximal : TraceSet -> Trace -> Set where
  maximal : ∀{X φ} (wit : φ ∈ X) (F : ∀{ψ} -> φ ⊑ ψ -> ψ ∈ X -> ψ ≡ φ) -> Maximal X φ

maximal-sub : ∀{X} -> Maximal X ⊆ X
maximal-sub (maximal x _) = x

derive-maximal : ∀{α φ X} -> α ∷ φ ∈ Maximal X -> φ ∈ Maximal (X ∂ α)
derive-maximal (maximal wit F) = maximal wit λ le p -> ∷-injectiveʳ (F (some le) p)

input-maximal : ∀{x φ f} -> I x ∷ φ ∈ Maximal ⟦ inp f ⟧ -> φ ∈ Maximal ⟦ f x .force ⟧
input-maximal (maximal (_ , def , step inp tr) F) =
  maximal (_ , def , tr) λ { le tψ -> ∷-injectiveʳ (F (some le) (inp-has-trace tψ)) }

output-maximal : ∀{x φ f} -> O x ∷ φ ∈ Maximal ⟦ out f ⟧ -> φ ∈ Maximal ⟦ f x .force ⟧
output-maximal (maximal (_ , def , step (out _) tr) F) =
  maximal (_ , def , tr) λ { le tψ -> ∷-injectiveʳ (F (some le) (out-has-trace tψ)) }

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Data.List.Relation.Quantification.Proofs where

import      Lvl
open import Data.List
open import Data.List.Functions
open import Data.List.Equiv.Id
open import Data.List.Relation.Permutation
open import Data.List.Relation.Quantification
open import Functional
open import Logic.Propositional
open import Logic
open import Structure.Relator.Properties
open import Type.Dependent
open import Type

private variable ℓ : Lvl.Level
private variable T A B C : Type{ℓ}
private variable l l₁ l₂ : List(T)
private variable ll : List(List(T))
private variable x : T
private variable P Q : T → Stmt{ℓ}
private variable Q₂ : A → B → Stmt{ℓ}
private variable _▫_ : T → T → Stmt{ℓ}

AllElements-map : (f : A → B) → (g : A → C) → (∀{x} → P(f(x)) → Q(g(x))) → (AllElements P(map f(l)) → AllElements Q(map g(l)))
AllElements-map {l = ∅}     f g pq ∅        = ∅
AllElements-map {l = x ⊰ l} f g pq (p ⊰ ap) = pq p ⊰ AllElements-map f g pq ap

AllElements-mapᵣ : (f : A → B) → (∀{x} → P(x) → Q(f(x))) → (AllElements P l → AllElements Q (map f(l)))
AllElements-mapᵣ = AllElements-map id

AllElements-mapₗ : (f : A → B) → (∀{x} → P(f(x)) → Q(x)) → (AllElements P (map f(l)) → AllElements Q l)
AllElements-mapₗ f = AllElements-map f id

AllElements-fn : (∀{x} → P(x) → Q(x)) → (AllElements P l → AllElements Q l)
AllElements-fn = AllElements-map id id

AllElements-[++] : AllElements P l₁ → AllElements P l₂ → AllElements P (l₁ ++ l₂)
AllElements-[++] {l₁ = ∅}     p       q = q
AllElements-[++] {l₁ = _ ⊰ _} (x ⊰ p) q = x ⊰ AllElements-[++] p q

AllElements-concat : (AllElements (AllElements P) l → AllElements P (concat l))
AllElements-concat ∅        = ∅
AllElements-concat (p ⊰ pl) = AllElements-[++] p (AllElements-concat pl)

AllElements-concatMap : (f : A → List(B)) → (∀{x} → P(x) → AllElements Q(f(x))) → (AllElements P(l) → AllElements Q(concatMap f(l)))
AllElements-concatMap f pq ∅       = ∅
AllElements-concatMap f pq (x ⊰ p) = AllElements-[++] (pq x) (AllElements-concatMap f pq p)

AllElements-order-independent : ∀{P : T → Type{ℓ}}{l₁ l₂} → (l₁ permutes l₂) → (AllElements P(l₁) → AllElements P(l₂))
AllElements-order-independent _permutes_.empty          ∅           = ∅
AllElements-order-independent (_permutes_.prepend perm) (x ⊰ p)     = x ⊰ AllElements-order-independent perm p
AllElements-order-independent _permutes_.swap           (x ⊰ y ⊰ p) = y ⊰ x ⊰ p
AllElements-order-independent (trans perm₁ perm₂)                   = AllElements-order-independent perm₂ ∘ AllElements-order-independent perm₁

AllElements-of-transitive-binary-relationₗ : ⦃ trans : Transitivity(_▫_) ⦄ → (l₁ ▫ l₂) → (AllElements (_▫ l₁) ll → AllElements (_▫ l₂) ll)
AllElements-of-transitive-binary-relationₗ             _ ∅        = ∅
AllElements-of-transitive-binary-relationₗ {_▫_ = _▫_} p (a ⊰ al) = transitivity(_▫_) a p ⊰ AllElements-of-transitive-binary-relationₗ p al

AllElements-of-transitive-binary-relationᵣ : ⦃ trans : Transitivity(_▫_) ⦄ → (l₂ ▫ l₁) → (AllElements (l₁ ▫_) ll → AllElements (l₂ ▫_) ll)
AllElements-of-transitive-binary-relationᵣ             _ ∅        = ∅
AllElements-of-transitive-binary-relationᵣ {_▫_ = _▫_} p (a ⊰ al) = (transitivity(_▫_) p a) ⊰ AllElements-of-transitive-binary-relationᵣ p al

AllElements-sigma : Σ(List(T)) (AllElements(P)) ↔ List(Σ T P)
AllElements-sigma = [↔]-intro L R where
  L : Σ(List(T)) (AllElements(P)) ← List(Σ T P)
  L ∅                 = intro ∅ ∅
  L ((intro x p) ⊰ sl) =
    let (intro l pl) = L sl
    in  intro (x ⊰ l) (p ⊰ pl)

  R : Σ(List(T)) (AllElements(P)) → List(Σ T P)
  R (intro ∅       ∅)        = ∅
  R (intro (x ⊰ l) (p ⊰ pl)) = intro x p ⊰ R(intro l pl)


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.QuoInt where

open import Cubical.Data.Int.MoreInts.QuoInt.Base public

open import Cubical.Data.Int.MoreInts.QuoInt.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Andreas, 2012-01-11
module Issue551a where

data Box (A : Set) : Set where
  [_] : A → Box A

implicit : {A : Set}{{a : A}} -> A
implicit {{a}} = a

postulate
  A : Set
  .a : A  -- this irrelevant definition needs to be ignored by instance search

a' : Box A
a' = [ implicit ]
-- this should fail

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Dependent product combinators for setoid equality preserving
-- functions
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Product.Function.Dependent.Setoid.WithK where

open import Data.Product
open import Data.Product.Function.Dependent.Setoid using (surjection)
open import Data.Product.Relation.Binary.Pointwise.Dependent
open import Relation.Binary
open import Function
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; Injective; _↣_; module Injection)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; _LeftInverseOf_; _RightInverseOf_; module LeftInverse)
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)
open import Relation.Binary as B
open import Relation.Binary.Indexed.Heterogeneous
  using (IndexedSetoid)
open import Relation.Binary.Indexed.Heterogeneous.Construct.At
  using (_atₛ_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Combinator for Inverse

module _ {a₁ a₂ b₁ b₁′ b₂ b₂′} {A₁ : Set a₁} {A₂ : Set a₂} where

  inverse : {B₁ : IndexedSetoid A₁ b₁ b₁′} (B₂ : IndexedSetoid A₂ b₂ b₂′) →
    (A₁↔A₂ : A₁ ↔ A₂) →
    (∀ {x} → Inverse (B₁ atₛ x) (B₂ atₛ (Inverse.to A₁↔A₂ ⟨$⟩ x))) →
    Inverse (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
  inverse {B₁} B₂ A₁↔A₂ B₁↔B₂ = record
    { to         = Surjection.to   surj
    ; from       = Surjection.from surj
    ; inverse-of = record
      { left-inverse-of  = left
      ; right-inverse-of = Surjection.right-inverse-of surj
      }
    }
    where
    surj = surjection B₂ (Inverse.surjection A₁↔A₂)
                         (Inverse.surjection B₁↔B₂)

    left : Surjection.from surj LeftInverseOf Surjection.to surj
    left (x , y) =
      Inverse.left-inverse-of A₁↔A₂ x ,
      IndexedSetoid.trans B₁
        (lemma (P.sym (Inverse.left-inverse-of A₁↔A₂ x))
               (P.sym (Inverse.right-inverse-of A₁↔A₂
                       (Inverse.to A₁↔A₂ ⟨$⟩ x))))
        (Inverse.left-inverse-of B₁↔B₂ y)
      where
      lemma :
        ∀ {x x′ y} → x ≡ x′ →
        (eq : (Inverse.to A₁↔A₂ ⟨$⟩ x) ≡ (Inverse.to A₁↔A₂ ⟨$⟩ x′)) →
        IndexedSetoid._≈_ B₁
          (Inverse.from B₁↔B₂ ⟨$⟩ P.subst (IndexedSetoid.Carrier B₂) eq y)
          (Inverse.from B₁↔B₂ ⟨$⟩ y)
      lemma P.refl P.refl = IndexedSetoid.refl B₁


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

module Categories.Functor where

open import Prelude
open import Categories

record Functor {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (C : PreCategory ℓ₁ ℓ₂) (D : PreCategory ℓ₃ ℓ₄) : Type (ℓ₁ ℓ⊔ ℓ₂ ℓ⊔ ℓ₃ ℓ⊔ ℓ₄) where
  private module C = PreCategory C
  private module D = PreCategory D
  field
    F₀ : C.Ob → D.Ob
    F₁ : ∀ {X Y} → (X C.⟶ Y) → (F₀ X D.⟶ F₀ Y)

    identity : ∀ {X} → F₁ (C.Id {X}) ≡ D.Id
    homomorphism : ∀ {X Y Z} → (f : X C.⟶ Y) (g : Y C.⟶ Z) →
                   F₁ (g C.· f) ≡ F₁ g D.· F₁ f

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- Raw terms
------------------------------------------------------------------------

import Level
open import Data.Universe

module README.DependentlyTyped.Raw-term
  (Uni₀ : Universe Level.zero Level.zero)
  where

open import Data.Nat
import README.DependentlyTyped.Term as Term; open Term Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_)

mutual

  infixl 9 _·_
  infix  5 _∶_

  -- Raw types.

  data Raw-ty : Set where
    ⋆  : Raw-ty
    el : (t : Raw) → Raw-ty
    π  : (t₁ t₂ : Raw-ty) → Raw-ty

  -- Raw terms.
  --
  -- One could distinguish between "checkable" and "inferrable" terms,
  -- but without a corresponding split for the well-typed terms this
  -- seems awkward.

  data Raw : Set where
    var : (x : ℕ) → Raw
    ƛ   : (t : Raw) → Raw
    _·_ : (t₁ t₂ : Raw) → Raw

    -- Type annotation.
    _∶_ : (t : Raw) (σ : Raw-ty) → Raw

-- The context position corresponding to a variable.

position : ∀ {Γ σ} → Γ ∋ σ → ℕ
position zero    = zero
position (suc x) = suc (position x)

-- Well-typed terms can be turned into raw ones.

⌊_⌋ : ∀ {Γ σ} → Γ ⊢ σ → Raw
⌊ var x   ⌋ = var (position x)
⌊ ƛ t     ⌋ = ƛ ⌊ t ⌋
⌊ t₁ · t₂ ⌋ = ⌊ t₁ ⌋ · ⌊ t₂ ⌋

-- The same applies to syntactic types.

⌊_⌋ty : ∀ {Γ σ} → Γ ⊢ σ type → Raw-ty
⌊ ⋆       ⌋ty = ⋆
⌊ el t    ⌋ty = el ⌊ t ⌋
⌊ π σ′ τ′ ⌋ty = π ⌊ σ′ ⌋ty ⌊ τ′ ⌋ty

mutual

  -- The following functions remove type-annotations.

  ⌊_⌋raw-ty : Raw-ty → Raw-ty
  ⌊ ⋆       ⌋raw-ty = ⋆
  ⌊ el t    ⌋raw-ty = el ⌊ t ⌋raw
  ⌊ π t₁ t₂ ⌋raw-ty = π ⌊ t₁ ⌋raw-ty ⌊ t₂ ⌋raw-ty

  ⌊_⌋raw : Raw → Raw
  ⌊ var x   ⌋raw = var x
  ⌊ ƛ t     ⌋raw = ƛ ⌊ t ⌋raw
  ⌊ t₁ · t₂ ⌋raw = ⌊ t₁ ⌋raw · ⌊ t₂ ⌋raw
  ⌊ t ∶ σ   ⌋raw = ⌊ t ⌋raw

-- Some congruence lemmas.

position-cong : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
                  {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
                x₁ ≅-∋ x₂ → position x₁ ≡ position x₂
position-cong P.refl = P.refl

⌊⌋-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁}
            {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
          t₁ ≅-⊢ t₂ → ⌊ t₁ ⌋ ≡ ⌊ t₂ ⌋
⌊⌋-cong P.refl = P.refl

⌊⌋ty-cong : ∀ {Γ₁ σ₁} {σ′₁ : Γ₁ ⊢ σ₁ type}
              {Γ₂ σ₂} {σ′₂ : Γ₂ ⊢ σ₂ type} →
            σ′₁ ≅-type σ′₂ → ⌊ σ′₁ ⌋ty ≡ ⌊ σ′₂ ⌋ty
⌊⌋ty-cong P.refl = P.refl

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module FStream.Bisimulation where

open import Library
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.Core as Core
-- open ≡-Reasoning

open import FStream.Core

mutual
  record _~_ {i} {ℓ₁ ℓ₂} {X : Set ℓ₁} {C : Container ℓ₂} (s₁ s₂ : FStream {i} C X) : Set (ℓ₁ ⊔ ℓ₂) where
    coinductive
    field
      sameInitShapes : proj₁ (inF s₁) ≡ proj₁ (inF s₂)
      bisim : ∀ pos → proj₂ (inF s₁) pos ~' proj₂ (inF s₂) (subst (Position C) sameInitShapes pos)
  record _~'_ {i} {ℓ₁ ℓ₂} {X : Set ℓ₁} {C : Container ℓ₂} (s₁ s₂ : FStream' {i} C X) : Set (ℓ₁ ⊔ ℓ₂) where
    coinductive
    field
      hd∼ : head s₁ ≡ head s₂
      tl∼ : ∀ {j : Size< i} → tail s₁ ~ tail s₂
open _~_ public
open _~'_ public

-- alias
_∼_ = _~_

{-
mutual
  BisimEquiv  : ∀ {i : Size} → IsEquivalence (_~_ {i})
  sameInitShapes (IsEquivalence.refl BisimEquiv {x = x}) = refl
  bisim (IsEquivalence.refl (BisimEquiv {i}) {x}) {j} pos = IsEquivalence.refl (BisimEquiv' {i})
  sameInitShapes (IsEquivalence.sym BisimEquiv x) = sym (sameInitShapes x)
  bisim (IsEquivalence.sym (BisimEquiv {i}) {i = s1} {j = s2} x) pos with bisim x pos
  ... | bla = IsEquivalence.sym BisimEquiv' (subst (λ x₁ → {!   !}) lemma x)
    where
      lemma = begin {!   !}
  sameInitShapes (IsEquivalence.trans BisimEquiv bisim1 bisim2) = trans (sameInitShapes bisim1) (sameInitShapes bisim2)
  bisim (IsEquivalence.trans BisimEquiv bisim1 bisim2) pos = IsEquivalence.trans BisimEquiv' {!   !} {!   !}

  BisimEquiv' : ∀ {i : Size} → IsEquivalence (_~'_ {i})
  hd∼ (IsEquivalence.refl BisimEquiv' {x}) = refl
  tl∼ (IsEquivalence.refl BisimEquiv' {x}) {j} = IsEquivalence.refl (BisimEquiv {j})
  hd∼ (IsEquivalence.sym BisimEquiv' x) = sym (hd∼ x)
  tl∼ (IsEquivalence.sym BisimEquiv' x) {j} = IsEquivalence.sym BisimEquiv (tl∼ x)
  hd∼ (IsEquivalence.trans BisimEquiv' bisim1 bisim2) = trans (hd∼ bisim1) (hd∼ bisim2)
  tl∼ (IsEquivalence.trans BisimEquiv' bisim1 bisim2) {j} = IsEquivalence.trans BisimEquiv (tl∼ bisim1) (tl∼ bisim2)
-}

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

data Is-nothing {A} : Maybe A → Set where
  nothing : Is-nothing nothing

record ℕ∞ : Set where
  coinductive
  field
    prd∞ : Maybe ℕ∞

open ℕ∞

f :  ℕ∞ → ℕ∞
prd∞ (f m) with prd∞ m
prd∞ (f m) | just pm with f pm
prd∞ (f m) | just pm | x = prd∞ x
prd∞ (f m) | nothing = nothing

inf∞ : ℕ∞
prd∞ inf∞ = just inf∞

test : Is-nothing (prd∞ (f inf∞))
test = nothing

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Pattern matching on a (decidably) empty type allows you to omit the
-- right-hand side.
module AbsurdPattern where

data Empty : Set where

elim-Empty : {A : Set} -> Empty -> A
elim-Empty ()


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

-- Polynomials over a commutative ring in sparse Horner normal form.
--
-- Much of the implementation is inspired by:
--
--   B. Grégoire and A. Mahboubi, ‘Proving Equalities in a Commutative
--   Ring Done Right in Coq’, in Theorem Proving in Higher Order
--   Logics, Berlin, Heidelberg, 2005, vol. 3603, pp. 98–113.
--
-- The main sources of efficience come from:
--
-- * Careful arrangement of operators to maintain *syntactic equality*.
--
-- * Avoiding of identities (like *1 or +0) with specialised data
--  structures.
open import Polynomial.Parameters

module Polynomial.NormalForm
  {c r₁ r₂ r₃}
  (homo : Homomorphism c r₁ r₂ r₃)
  where

open Homomorphism homo

-- The "injection index" is what allows us to store the nested
-- polynomials sparsely.
open import Polynomial.NormalForm.InjectionIndex public

-- The definition and types for the polynomial.
open import Polynomial.NormalForm.Definition coeffs public

-- Normalizing constructors.
open import Polynomial.NormalForm.Construction coeffs public

-- Definition of arithmetic operations etc.
open import Polynomial.NormalForm.Operations coeffs public

-- "Running" the polynomial on some input.
open import Polynomial.NormalForm.Semantics homo public

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


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

open import Relation.Binary.Core

module Definitions
  {a ℓ} {A : Set a}   -- The underlying set
  (_≈_ : Rel A ℓ)     -- The underlying equality
  where

open import Algebra.Core
open import Data.Product
open import Algebra.Definitions

-- (x²y)x = x²(yx)
JordanIdentity: : Op₂ A → Set _
JordanIdentity: _∙_ = ∀ x y → (((x ∙ x) ∙ y) ∙ x) ≈ (((x ∙ x) ∙ y) ∙ x)

-- x = xyx
PesudoInverse₁ : Op₂ A → Set _
PesudoInverse₁ _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ x

-- y = yxy
PseudoInverse₂ : Op₂ A → Set _
PseudoInverse₂ _∙_ = ∀ x y → ((y ∙ x) ∙ y) ≈ y

PseudoInverse : Op₂ A → Set _
PseudoInverse ∙ = (PesudoInverse₁ ∙) × (PseudoInverse₂ ∙)

-- JacobiIdentity is (x ∙ (y ∙ z)) + ((y ∙ (z ∙ x)) + (z ∙ (x ∙ y))) = 0
-- Using the antisymmetry property Jacobi identity may be rewritten as a modification of the associative property

JacobiIdentity : Op₂ A → Op₂ A → Set _
JacobiIdentity _∙_  _-_ = ∀ x y z → (x ∙ (y ∙ z)) ≈ ((y ∙ (z ∙ x)) - (z ∙ (x ∙ y)))


text:
-- We use instance argument to overload the algebraic operations + and
-- * etc.. For example, Ring record here is like what Num class in
-- Haskell. Also like Haskell, we don't require the operations abide
-- by any laws (we can use the algebraic definitions in stdlib if
-- needed).

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

module Typeclasses where

-- ----------------------------------------------------------------------
-- Type classes for Ring.

-- SemiRing typecalss has two operations + and * and two special
-- numbers 0 and 1.
record SemiRing (A : Set) : Set where
  infixl 6 _+_
  infixl 7 _*_
  infixr 8 _^2
  field
    _+_ : A -> A -> A
    _*_ : A -> A -> A
    0# : A
    1# : A
  -- A useful shot-hand.
  _^2 : A -> A
  x ^2 = x * x

-- A special way to open a module in order to make the fields of the
-- record available as functions taking instance arguments.
open SemiRing {{...}} public

-- Ring typeclass is a subclass of SemiRing typeclass, and has
-- addtitve inverse. Hence we can define subtraction.
record Ring (A : Set) : Set where
  infixl 6 _-_
  infix 8 -_
  field
    {{sra}} : SemiRing A
    -_ : A -> A

  _-_ :  A -> A -> A
  _-_ x y = x + (- y)

open Ring {{...}} public

-- ----------------------------------------------------------------------
-- Type classes decidable order.

-- We will use orders on ℕ and ℤ simultaneously, so we also overload
-- the comparsion operations using typeclass.

-- Decidable order typeclass. Normally DecEq is a super class of
-- DecOrd, here we don't enforce this, since the main purpose is to
-- overload operators.

open import Relation.Binary using (Rel ; Decidable)

record DecOrd (A : Set) : Set₁ where
  infixl 4 _≤_ _<_
  infixl 4 _≤?_ _<?_
  field
    _≤_ : Rel A _
    _≤?_ : Decidable _≤_
    _<_ : Rel A _
    _<?_ : Decidable _<_
open DecOrd {{...}} public

-- ----------------------------------------------------------------------
-- Type classes NonZero and DivMod

-- We will use irrelevant implicit argument to exlude the zero divisor
-- case when defining the partial function "div" and "mod".

record NonZeroTypeclass (A : Set) : Set₁  where
  field
    NonZero : (a : A) -> Set

open NonZeroTypeclass {{...}} public

-- DivMod typeclass is used to overload _/_ and _%_.
record DivMod (A : Set) : Set₁ where
  infixl 7 _/_ _%_
  field
    {{NZT}} : NonZeroTypeclass A
    _/_     : (n d : A) .{{_ : NonZero d}} -> A
    _%_     : (n d : A) .{{_ : NonZero d}} -> A
open DivMod {{...}} public

-- ----------------------------------------------------------------------
-- Type classes for Rank (to be used in defining Euclidean structure)

-- Rank record has a rank function that spcifies the rank of the given
-- argument.
import Data.Nat as Nat
record Rank (A : Set) : Set where
  field
    rank : A -> Nat.ℕ
open Rank {{...}} public

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
module Tactic.Nat.Subtract where

open import Tactic.Nat.Subtract.Auto public using (autosub-tactic)
open import Tactic.Nat.Subtract.Simplify public using (simplifysub-tactic; simplifygoal-tactic)
open import Tactic.Nat.Subtract.By public using (by-tactic)
open import Tactic.Nat.Subtract.Refute public using (refutesub-tactic)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module Acme.Data.Nat where

open import Acme.Type

ℕ   : Type
isZ : Type
isS : Type

ℕ cs = isZ cs || isS cs

isZ [] = false
isZ (c ∷ cs) = c == 'Z' && isNil cs

isS [] = false
isS (c ∷ cs) = c == 'S' && ℕ cs

zero = ℕ ∋ "Z"

suc : Elt ℕ → Elt ℕ
suc [ n ] = [ 'S' ∷ n ]

one    = ℕ ∋ "SZ"
two    = suc (suc zero)
three  = ℕ ∋ "SSSZ"
four   = suc three

module _ (P : Elt ℕ → Set)
         (P0 : P zero)
         (PS : ∀ n → P n → P (suc n))
         where

  induction : ∀ n → P n
  induction [ ccs@(c ∷ cs) ] = checkZ (c ≟ 'Z') cs refl where

    checkS : ∀ {b} → Reflects c 'S' b → ∀ cs →
             {{@0 _ : IsTrue (b && ℕ cs)}} →
             ∀ {ccs} → c ∷ cs ≡ ccs .value → P ccs
    checkS true cs refl = PS [ cs ] (induction [ cs ])

    checkZ : ∀ {b} → Reflects c 'Z' b → ∀ cs →
             {{@0 _ : IsTrue (b && isNil cs || isS (c ∷ cs))}} →
             ∀ {ccs} → c ∷ cs ≡ ccs .value → P ccs
    checkZ true  [] refl = P0
    checkZ false cs eq   = checkS (c ≟ 'S') cs eq

_ : ∀ {P P0 PS} → induction P P0 PS zero ≡ P0
_ = refl

_ : ∀ {P P0 PS n} →
    induction P P0 PS (suc n) ≡ PS n (induction P P0 PS n)
_ = refl

_+_ : Elt ℕ → Elt ℕ → Elt ℕ
m + n = induction (λ _ → Elt ℕ) n (λ _ → suc) m

_ : three + one ≡ four
_ = refl

_*_ : Elt ℕ → Elt ℕ → Elt ℕ
m * n = induction (λ _ → Elt ℕ) zero (λ _ → n +_) m

_ : two * three ≡ four + two
_ = refl

zero-+ : ∀ m → zero + m ≡ m
zero-+ m = refl

+-zero : ∀ m → m + zero ≡ m
+-zero =
  induction
    (λ m → m + zero ≡ m)
    refl
    (λ n → cong suc)

suc-+ : ∀ m n → suc m + n ≡ suc (m + n)
suc-+ m n = refl

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc m n =
  induction
    (λ m → (m + suc n) ≡ suc (m + n))
    refl
    (λ n → cong suc)
    m

+-comm : ∀ m n → m + n ≡ n + m
+-comm m n =
  induction
    (λ m → m + n ≡ n + m)
    (sym (+-zero n))
    (λ m ih → trans (cong suc ih) (sym (+-suc n m)))
    m

+-assoc : ∀ m n p → (m + n) + p ≡ m + (n + p)
+-assoc m n p =
  induction
    (λ m → ((m + n) + p) ≡ (m + (n + p)))
    refl
    (λ m → cong suc)
    m

max_stars_repo_name: gallais/STRINaGda

max_issues_repo_name: gallais/STRINaGda

max_forks_repo_name: gallais/STRINaGda


text:
module Agda.Builtin.List where

infixr 5 _∷_
data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

{-# HASKELL type AgdaList a b = [b] #-}

{-# COMPILED_DATA List MAlonzo.Code.Agda.Builtin.List.AgdaList [] (:) #-}
{-# COMPILED_DATA_UHC List __LIST__ __NIL__ __CONS__ #-}


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Strict2Group where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.ReflGraph
open import Cubical.DStructures.Structures.VertComp

private
  variable
    ℓ ℓ' : Level

module _ (ℓ ℓ' : Level) where
  private
    ℓℓ' = ℓ-max ℓ ℓ'

  𝒮ᴰ-Strict2Group : URGStrᴰ (𝒮-ReflGraph ℓ ℓ')
                            VertComp
                            ℓ-zero
  𝒮ᴰ-Strict2Group = Subtype→Sub-𝒮ᴰ (λ 𝒢 → VertComp 𝒢 , isPropVertComp 𝒢)
                                   (𝒮-ReflGraph ℓ ℓ')

  Strict2Group : Type (ℓ-suc ℓℓ')
  Strict2Group = Σ[ 𝒢 ∈ ReflGraph ℓ ℓ' ] VertComp 𝒢

  record S2G : Type (ℓ-suc ℓℓ') where
    no-eta-equality
    field
      G₀ : Group {ℓ}
      G₁ : Group {ℓ'}
      σ : GroupHom G₁ G₀
      τ : GroupHom G₁ G₀
      ι : GroupHom G₀ G₁
      split-σ : isGroupSplitEpi ι σ
      split-τ : isGroupSplitEpi ι τ
      V : VertComp (((((G₀ , G₁) , ι , σ) , split-σ) , τ) , split-τ)

{-
  open S2G

  make-S2G : {G₀ : Group {ℓ}} {G₁ : Group {ℓ'}}
             → (σ τ : GroupHom G₁ G₀)
             → (ι : GroupHom G₀ G₁)
             → (split-σ : isGroupSplitEpi ι σ)
             → (split-τ : isGroupSplitEpi ι τ)
             → VertComp (((((G₀ , G₁) , ι , σ) , split-σ) , τ) , split-τ)
             → S2G
  make-S2G = {!!}

Group→S2G : Group {ℓ} → S2G ℓ ℓ
Group→S2G G .G₀ = G
Group→S2G G .G₁ = G
Group→S2G G .σ = idGroupHom G
Group→S2G G .τ = idGroupHom G
Group→S2G G .ι = idGroupHom G
Group→S2G G .split-σ = GroupMorphismExt (λ _ → refl)
Group→S2G G .split-τ = GroupMorphismExt (λ _ → refl)
Group→S2G G .V = {!!}
-}

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import HoTT
open import groups.Cokernel
open import cohomology.Theory

open import cw.CW

module cw.cohomology.HigherCoboundary {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S (S n))) where

open OrdinaryTheory OT
open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.GridLongExactSequence cohomology-theory
  (ℕ-to-ℤ (S n)) (⊙cw-incl-last (⊙cw-init ⊙skel)) (⊙cw-incl-last ⊙skel)

cw-co∂-last : CXₙ/Xₙ₋₁ (⊙cw-init ⊙skel) (ℕ-to-ℤ (S n)) →ᴳ CXₙ/Xₙ₋₁ ⊙skel (ℕ-to-ℤ (S (S n)))
cw-co∂-last = grid-co∂

module CokerCo∂ where
  grp = Coker cw-co∂-last (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (S (S n))))
  open Group grp public

CokerCo∂ = CokerCo∂.grp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- The "intro" command manages to refine goals of type ∞ A with the
-- term ♯ ?.

module IntroSharp where

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

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

Foo : ∞ Set
Foo = ?


text:
module par-swap.dpg-e-view where

open import par-swap
open import par-swap.properties
open import par-swap.confluent
open import par-swap.dpg-pot
open import utility
open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Plug
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Data.Empty
open import sn-calculus
open import context-properties -- get view, E-views

DPG-E-view :
 ∀ {E C r₁ r₂ p q θ θ' pin qin A A'} ->
  (peq : p ≐ E ⟦ pin ⟧e) ->
  (qeq : q ≐ E ⟦ qin ⟧e) ->
  p ≐ C ⟦ r₁ ∥ r₂ ⟧c ->
  (psn⟶₁q : ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θ' , A' ⟩· q) ->
  ->E-view psn⟶₁q peq qeq ->
  Σ[ d ∈ Term ]
  Σ[ sn⟶₁d ∈ ρ⟨ θ , A ⟩· C ⟦ r₂ ∥ r₁ ⟧c sn⟶₁ ρ⟨ θ' , A' ⟩· d ]
  Σ[ ∥Rd ∈ q ∥R* d ]
  Σ[ E′ ∈ List EvaluationContext1 ]
  Σ[ pin′ ∈ Term ]
  Σ[ qin′ ∈ Term ]
  Σ[ peq′ ∈ C ⟦ r₂ ∥ r₁ ⟧c ≐ E′ ⟦ pin′ ⟧e ]
  Σ[ qeq′ ∈ d ≐ E′ ⟦ qin′ ⟧e ]
  ->E-view sn⟶₁d peq′ qeq′

DPG-E-view dehole dehole dchole psn⟶₁q ()
DPG-E-view dehole dehole (dcpar₁ pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcpar₂ pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcseq₁ pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcseq₂ pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcsuspend pC) psn⟶₁q ()
DPG-E-view dehole dehole (dctrap pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcsignl pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcloop pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcloopˢ₁ pC) psn⟶₁q ()
DPG-E-view dehole dehole (dcloopˢ₂ pC) psn⟶₁q ()

DPG-E-view dehole dehole (dcpresent₁ pC)
           (ris-present S∈ s[θ]≡p dehole)
           vis-present
  =  _ , ris-present S∈ s[θ]≡p dehole , ∥Rn (∥Rstep pC) ∥R0 ,
    _ , _ , _ , dehole , dehole , vis-present

DPG-E-view dehole dehole (dcpresent₁ pC)
           (ris-absent S∈ s[θ]≡p dehole)
           vis-absent
 = _ , ris-absent S∈ s[θ]≡p dehole , ∥R0 ,
   _ , _ , _ , dehole , dehole , vis-absent

DPG-E-view dehole dehole (dcpresent₂ pC)
           (ris-present S∈ s[θ]≡a dehole)
           vis-present
 = _ , ris-present S∈ s[θ]≡a dehole , ∥R0 ,
   _ , _ , _ , dehole , dehole , vis-present

DPG-E-view dehole dehole (dcpresent₂ pC)
           (ris-absent S∈ s[θ]≡a dehole)
           vis-absent
 = _ ,  ris-absent S∈ s[θ]≡a dehole , ∥Rn (∥Rstep pC) ∥R0 ,
   _ , _ , _ , dehole , dehole , vis-absent

DPG-E-view dehole dehole (dcshared pC)
           (rraise-shared allready dehole)
           vraise-shared
 = _ , rraise-shared allready dehole ,
       Context1-∥R* (cenv _ _) (∥Rn (∥Rstep pC) ∥R0) ,
   _ , _ , _ , dehole , dehole , vraise-shared

DPG-E-view dehole dehole (dcvar pC)
           (rraise-var allready dehole)
           vraise-var
 = _ , rraise-var allready dehole ,
       Context1-∥R* (cenv _ _) (∥Rn (∥Rstep pC) ∥R0) ,
   _ , _ , _ , dehole , dehole , vraise-var

DPG-E-view dehole dehole (dcif₁ pC)
           (rif-false x∈ x[θ]≡0 dehole)
           vif-false
 = _ , rif-false x∈ x[θ]≡0 dehole , ∥R0 ,
   _ , _ , _ , dehole , dehole , vif-false

DPG-E-view dehole dehole (dcif₁ pC)
           (rif-true x∈ x[θ]≡s dehole)
           vif-true
 = _ , rif-true x∈ x[θ]≡s dehole , ∥Rn (∥Rstep pC) ∥R0 ,
   _ , _ , _ , dehole , dehole , vif-true

DPG-E-view dehole dehole (dcif₂ pC)
           (rif-false x∈ x[θ]≡0 dehole)
           vif-false
 = _ , rif-false x∈ x[θ]≡0 dehole , ∥Rn (∥Rstep pC) ∥R0 ,
   _ , _ , _ , dehole , dehole , vif-false

DPG-E-view dehole dehole (dcif₂ pC)
           (rif-true x∈ x[θ]≡s dehole)
           vif-true
 = _ , rif-true x∈ x[θ]≡s dehole , ∥R0 ,
   _ , _ , _ , dehole , dehole , vif-true

DPG-E-view dehole dehole (dcenv pC)
           (rmerge dehole)
           vmerge
 = _ , rmerge dehole , ∥Rn (∥Rstep pC) ∥R0 ,
   _ , _ , _ , dehole , dehole , vmerge

DPG-E-view (depar₁ pE) (depar₁ qE) dchole psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (depar₁ pE) (depar₁ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with wrap-rho redo-sub pE qE E-view-sub
               _ (depar₂ pE) (depar₂ qE)
... | (redo′ , E-view′)
 = _ , redo′ , ∥Rn (∥Rstep dchole) ∥R0 ,
   _ , _ , _ , depar₂ pE , depar₂ qE , E-view′

DPG-E-view (depar₂ pE) (depar₂ qE) dchole psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (depar₂ pE) (depar₂ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with wrap-rho redo-sub pE qE E-view-sub
               _ (depar₁ pE) (depar₁ qE)
... | (redo′ , E-view′)
 = _ , redo′ , ∥Rn (∥Rstep dchole) ∥R0 ,
   _ , _ , _ , depar₁ pE , depar₁ qE , E-view′

DPG-E-view {e ∷ _} (depar₁ pE) (depar₁ qE) (dcpar₁ pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (depar₁ pE) (depar₁ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with DPG-E-view pE qE pC redo-sub E-view-sub
... | (ds , pssn⟶₁ds , qs∥Rds , _ , _ , _ , pE′ , qE′ , E-view-sub′)
 with wrap-rho pssn⟶₁ds pE′ qE′ E-view-sub′ _ (depar₁ pE′) (depar₁ qE′)
... | (redo , E-view′)
 = _ , redo , Context1-∥R* (ceval e) qs∥Rds ,
   _ , _ , _ , depar₁ pE′ , depar₁ qE′ , E-view′

DPG-E-view {e ∷ _} (depar₂ pE) (depar₂ qE) (dcpar₂ pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (depar₂ pE) (depar₂ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with DPG-E-view pE qE pC redo-sub E-view-sub
... | (ds , pssn⟶₁ds , qs∥Rds , _ , _ , _ , pE′ , qE′ , E-view-sub′)
 with wrap-rho pssn⟶₁ds pE′ qE′ E-view-sub′ _ (depar₂ pE′) (depar₂ qE′)
... | (redo , E-view′)
 = _ , redo , Context1-∥R* (ceval e) qs∥Rds ,
   _ , _ , _ , depar₂ pE′ , depar₂ qE′ , E-view′

DPG-E-view {e ∷ _} (desuspend pE) (desuspend qE) (dcsuspend pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (desuspend pE) (desuspend qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with DPG-E-view pE qE pC redo-sub E-view-sub
... | (ds , pssn⟶₁ds , qs∥Rds , _ , _ , _ , pE′ , qE′ , E-view-sub′)
 with wrap-rho pssn⟶₁ds pE′ qE′ E-view-sub′ _ (desuspend pE′) (desuspend qE′)
... | (redo , E-view′)
 = _ , redo , Context1-∥R* (ceval e) qs∥Rds ,
   _ , _ , _ , desuspend pE′ , desuspend qE′ , E-view′

DPG-E-view {e ∷ _} (detrap pE) (detrap qE) (dctrap pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (detrap pE) (detrap qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with DPG-E-view pE qE pC redo-sub E-view-sub
... | (ds , pssn⟶₁ds , qs∥Rds , _ , _ , _ , pE′ , qE′ , E-view-sub′)
 with wrap-rho pssn⟶₁ds pE′ qE′ E-view-sub′ _ (detrap pE′) (detrap qE′)
... | (redo , E-view′)
 = _ , redo ,  Context1-∥R* (ceval e) qs∥Rds ,
   _ , _ , _ , detrap pE′ , detrap qE′ , E-view′

DPG-E-view {e ∷ _} (deseq pE) (deseq qE) (dcseq₁ pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (deseq pE) (deseq qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with DPG-E-view pE qE pC redo-sub E-view-sub
... | (ds , pssn⟶₁ds , qs∥Rds , _ , _ , _ , pE′ , qE′ , E-view-sub′)
 with wrap-rho pssn⟶₁ds pE′ qE′ E-view-sub′ _ (deseq pE′) (deseq qE′)
... | (redo , E-view′)
 = _ , redo , Context1-∥R* (ceval e) qs∥Rds ,
   _ , _ , _ , deseq pE′ , deseq qE′ , E-view′

DPG-E-view {e ∷ _} (deloopˢ pE) (deloopˢ qE) (dcloopˢ₁ pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (deloopˢ pE) (deloopˢ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with DPG-E-view pE qE pC redo-sub E-view-sub
... | (ds , pssn⟶₁ds , qs∥Rds , _ , _ , _ , pE′ , qE′ , E-view-sub′)
 with wrap-rho pssn⟶₁ds pE′ qE′ E-view-sub′ _ (deloopˢ pE′) (deloopˢ qE′)
... | (redo , E-view′)
 = _ , redo , Context1-∥R* (ceval e) qs∥Rds ,
   _ , _ , _ , deloopˢ pE′ , deloopˢ qE′ , E-view′

DPG-E-view{_}{_}{r₁}{r₂} (depar₁ pE) (depar₁ qE) (dcpar₂{C = C} pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (depar₁ pE) (depar₁ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with wrap-rho redo-sub pE qE E-view-sub
               (epar₁ (C ⟦ r₂ ∥ r₁ ⟧c))
               (depar₁ pE) (depar₁ qE)
... | (redo′ , E-view′)
 = _ , redo′ , ∥Rn (Context1-∥R (ceval (epar₂ _)) (∥Rstep pC)) ∥R0 ,
   _ , _ , _ , depar₁ pE , depar₁ qE , E-view′

DPG-E-view{_}{_}{r₁}{r₂} (depar₂ pE) (depar₂ qE) (dcpar₁{C = C} pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (depar₂ pE) (depar₂ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with wrap-rho redo-sub pE qE E-view-sub
               (epar₂ (C ⟦ r₂ ∥ r₁ ⟧c))
               (depar₂ pE) (depar₂ qE)
... | (redo′ , E-view′)
 = _ , redo′ , ∥Rn (Context1-∥R (ceval (epar₁ _)) (∥Rstep pC)) ∥R0 ,
   _ , _ , _ , depar₂ pE , depar₂ qE , E-view′

DPG-E-view{_}{_}{r₁}{r₂} (deseq pE) (deseq qE) (dcseq₂{C = C} pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (deseq pE) (deseq qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with wrap-rho redo-sub pE qE E-view-sub
               (eseq (C ⟦ r₂ ∥ r₁ ⟧c))
               (deseq pE) (deseq qE)
... | (redo′ , E-view′)
 = _ , redo′ , ∥Rn (Context1-∥R (cseq₂ _) (∥Rstep pC)) ∥R0 ,
   _ , _ , _ , deseq pE , deseq qE , E-view′

DPG-E-view{_}{_}{r₁}{r₂} (deloopˢ pE) (deloopˢ qE) (dcloopˢ₂{C = C} pC) psn⟶₁q E-view
 with unwrap-rho psn⟶₁q (deloopˢ pE) (deloopˢ qE) pE qE E-view
... | (redo-sub , E-view-sub)
 with wrap-rho redo-sub pE qE E-view-sub
               (eloopˢ (C ⟦ r₂ ∥ r₁ ⟧c))
               (deloopˢ pE) (deloopˢ qE)
... | (redo′ , E-view′)
 = _ , redo′ , ∥Rn (Context1-∥R (cloopˢ₂ _) (∥Rstep pC)) ∥R0 ,
   _ , _ , _ , deloopˢ pE , deloopˢ qE , E-view′

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Fixities where

open import Haskell.Prelude

leftAssoc : Int → List Int
leftAssoc n = 2 * n + 1
            ∷ 2 * (n + 1)
            ∷ 1 + n * 2
            ∷ (1 + n) * 2
            ∷ (n + n) + n
            ∷ n + (n + n)
            ∷ []

rightAssoc : List Int → List Int
rightAssoc xs = xs ++ xs ++ ((xs ++ xs) ++ xs) ++ xs

nonAssoc : Bool → Bool
nonAssoc b = (b == b) == (b == b)

mixedAssoc : Maybe Int → (Int → Maybe Int) → Maybe Int
mixedAssoc m f = f =<< (((f =<< m) >>= f) >>= f)

{-# COMPILE AGDA2HS leftAssoc  #-}
{-# COMPILE AGDA2HS rightAssoc #-}
{-# COMPILE AGDA2HS nonAssoc   #-}
{-# COMPILE AGDA2HS mixedAssoc #-}


text:
-- Nils' suggestion

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Relation.Nullary using (¬_)
open import Function using (_∘_; id)
open import Data.Product using (_×_; _,_; proj₁; proj₂; map; ∃; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)

data even : ℕ → Set
data odd  : ℕ → Set

data even where
  even-zero : even zero
  even-suc  : ∀ {n : ℕ} → odd n → even (suc n)

data odd where
  odd-suc   : ∀ {n : ℕ} → even n → odd (suc n)

∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ m * 2)
∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + m * 2)

∃-even even-zero    = zero , refl
∃-even (even-suc o) with ∃-odd o
...                    | m , refl = suc m , refl

∃-odd  (odd-suc  e) with ∃-even e
...                    | m , refl = m , refl


text:
-- Andreas, 2014-03-03, report and test case by Nisse.

-- {-# OPTIONS -v tc.lhs.unify:60 #-}

module Issue1071 where

postulate
  F : Set → Set

module M (_ : Set₁) where
  postulate A : Set

open M Set

data P : Set → Set₁ where
  c : (R : Set) → P (F R)

data Q : (R : Set) → R → P R → Set₁ where
  d : (R : Set) (f : F R) → Q (F R) f (c R)

Foo : (f' : F A) → Q (F A) f' (c A) → Set₁
Foo ._ (d ._ _) = Set

-- WAS:
-- Refuse to solve heterogeneous constraint f₁ : F A =?= f : F A
-- when checking that the pattern d ._ _ has type Q (F A) f (c A)

-- SHOULD: succeed


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

module CombiningProofs.CommDisjunctionSchema where

open import Common.FOL.FOL

postulate ∨-comm : {A B : Set} → A ∨ B → B ∨ A
{-# ATP prove ∨-comm #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2018-08-14, issue #1556
-- Rule out very dependent types by looking for recursive calls
-- in the types of definitions.

-- {-# OPTIONS -v term:20 -v rec.graph:80 #-}

A : Set
data D : A → Set      -- D --> A  (new!)
a : A                 -- a --> A  (new!)

A = D a               -- A --> D, a
data D where d : D a  -- TODO: D --> a
a = d                 -- a --> d

-- Should be rejected, e.g., by termination checker.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.Traced where

open import Level

open import Data.Product
open import Data.Fin

open import Categories.Category
open import Categories.Monoidal
open import Categories.Functor hiding (id; _∘_; identityʳ; assoc)
open import Categories.Monoidal.Braided
open import Categories.Monoidal.Helpers
open import Categories.Monoidal.Braided.Helpers
open import Categories.Monoidal.Symmetric
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation hiding (id)

------------------------------------------------------------------------------
-- Helpers

unary : ∀ {o ℓ e} → (C : Category o ℓ e) → (A : Category.Obj C) →
          Fin 1 → Category.Obj C
unary C A zero = A
unary C A (suc ())

binary : ∀ {o ℓ e} → (C : Category o ℓ e) → (A B : Category.Obj C) →
          Fin 2 → Category.Obj C
binary C A B zero = A
binary C A B (suc zero) = B
binary C A B (suc (suc ()))

ternary : ∀ {o ℓ e} → (C : Category o ℓ e) → (A X Y : Category.Obj C) →
          Fin 3 → Category.Obj C
ternary C A X Y zero = A
ternary C A X Y (suc zero) = X
ternary C A X Y (suc (suc zero)) = Y
ternary C A X Y (suc (suc (suc ())))

------------------------------------------------------------------------------
-- Def from http://ncatlab.org/nlab/show/traced+monoidal+category
--
-- A symmetric monoidal category (C,⊗,1,b) (where b is the symmetry) is
-- said to be traced if it is equipped with a natural family of functions
--
-- TrXA,B:C(A⊗X,B⊗X)→C(A,B)
-- satisfying three axioms:
--
-- Vanishing: Tr1A,B(f)=f (for all f:A→B) and
-- TrX⊗YA,B=TrXA,B(TrYA⊗X,B⊗X(f)) (for all f:A⊗X⊗Y→B⊗X⊗Y)
--
-- Superposing: TrXC⊗A,C⊗B(idC⊗f)=idC⊗TrXA,B(f) (for all f:A⊗X→B⊗X)
--
-- Yanking: TrXX,X(bX,X)=idX

record Traced {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} {B : Braided M}
  (S : Symmetric B) : Set (o ⊔ ℓ ⊔ e) where

  private module C = Category C
  open C using (Obj; id; _∘_)

  private module M = Monoidal M
  open M using (⊗; identityʳ; assoc) renaming (id to 𝟙)

  private module F = Functor ⊗
  open F using () renaming (F₀ to ⊗ₒ; F₁ to ⊗ₘ)

  private module NIʳ = NaturalIsomorphism identityʳ
  open NaturalTransformation NIʳ.F⇒G renaming (η to ηidr⇒)
  open NaturalTransformation NIʳ.F⇐G renaming (η to ηidr⇐)

  private module NIassoc = NaturalIsomorphism assoc
  open NaturalTransformation NIassoc.F⇒G renaming (η to ηassoc⇒)
  open NaturalTransformation NIassoc.F⇐G renaming (η to ηassoc⇐)

  private module B = Braided B
  open B using (braid)

  private module NIbraid = NaturalIsomorphism braid
  open NaturalTransformation NIbraid.F⇒G renaming (η to ηbraid⇒)

  field
    trace : ∀ {X A B} → C [ ⊗ₒ (A , X)  , ⊗ₒ (B , X) ] → C [ A , B ]

    vanish_id : ∀ {A B f} →
                C [
                    trace {𝟙} {A} {B} f
                  ≡
                    (ηidr⇒ (unary C B) ∘ f ∘ ηidr⇐ (unary C A))
                  ]

    vanish_⊗ : ∀ {X Y A B f} →
               C [
                    trace {⊗ₒ (X , Y)} {A} {B} f
                  ≡
                    trace {X} {A} {B}
                      (trace {Y} {⊗ₒ (A , X)} {⊗ₒ (B , X)}
                        ((ηassoc⇐ (ternary C B X Y)) ∘ f ∘ (ηassoc⇒ (ternary C A X Y))))
                 ]

    superpose : ∀ {X Y A B} {f : C [ ⊗ₒ (A , X) , ⊗ₒ (B , X) ]} →
                C [
                    trace {X} {⊗ₒ (Y , A)} {⊗ₒ (Y , B)}
                      (ηassoc⇐ (ternary C Y B X) ∘ ⊗ₘ (id , f) ∘ ηassoc⇒ (ternary C Y A X))
                   ≡
                    ⊗ₘ (id , (trace {X} {A} {B} f))
                  ]

    yank : ∀ {X} →
           C [
               trace {X} {X} {X} (ηbraid⇒ (binary C X X))
              ≡
               id
             ]

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

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.Setoid module directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.EqReasoning {s₁ s₂} (S : Setoid s₁ s₂) where

open import Relation.Binary.Reasoning.Setoid S public