text:
open import Agda.Primitive using (_⊔_ ; lsuc ; Level)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Product using (Product)

open import MultiSorted.AlgebraicTheory
import MultiSorted.Product as Product
import MultiSorted.Interpretation

module MultiSorted.InterpretationCategory
         {o ℓ e}
         {𝓈 ℴ}
         (Σ : Signature {𝓈} {ℴ})
         {𝒞 : Category.Category o ℓ e}
         (cartesian-𝒞 : Cartesian.Cartesian 𝒞) where
  open Signature Σ
  open Category.Category 𝒞
  open Cartesian.Cartesian cartesian-𝒞
  open MultiSorted.Interpretation Σ cartesian-𝒞

  -- Equality of homomorphisms of interpretations
  _≈I_ : ∀ {I J : Interpretation} → I ⇒I J → I ⇒I J → Set (e ⊔ 𝓈)
  _≈I_ {I} {J} ϕ ψ =
    let open _⇒I_ in ∀ (A : sort) → hom-morphism ϕ {A} ≈ hom-morphism ψ

  -- The category of interpretations of Σ in 𝒞
  ℐ𝓃𝓉 : Category.Category (o ⊔ ℓ ⊔ e ⊔ 𝓈 ⊔ ℴ) (o ⊔ ℓ ⊔ e ⊔ 𝓈 ⊔ ℴ) (e ⊔ 𝓈)
  ℐ𝓃𝓉 = record
          { Obj = Interpretation
          ; _⇒_ = _⇒I_
          ; _≈_ = _≈I_
          ; id = id-I
          ; _∘_ = _∘I_
          ; assoc = λ _ → assoc
          ; sym-assoc = λ _ → sym-assoc
          ; identityˡ = λ _ → identityˡ
          ; identityʳ = λ _ → identityʳ
          ; identity² = λ _ → identity²
          ; equiv = record { refl = λ A → Equiv.refl
                           ; sym = λ p A → Equiv.sym (p A)
                           ; trans = λ p₁ p₂ A → Equiv.trans (p₁ A) (p₂ A)
                           }
          ; ∘-resp-≈ = λ p₁ p₂ A → ∘-resp-≈ (p₁ A) (p₂ A)
          }

  -- Cartesian structure on the category on interpretations of Σ in 𝒞
  module _ (I J : Interpretation) where
    open Interpretation
    open Product.Producted
    open HomReasoning
    A×B-ℐ𝓃𝓉 : Interpretation
    interp-sort A×B-ℐ𝓃𝓉 A = interp-sort I A × interp-sort J A
    -- Contexts
    -- -- Structure
    prod  (interp-ctx A×B-ℐ𝓃𝓉) Γ = prod (interp-ctx I) Γ × prod (interp-ctx J) Γ
    π (interp-ctx A×B-ℐ𝓃𝓉) x = (π (interp-ctx I) x) ⁂ (π (interp-ctx J) x)
    tuple (interp-ctx A×B-ℐ𝓃𝓉) Γ fs = ⟨ (tuple (interp-ctx I) Γ λ x → π₁ ∘ fs x) , ((tuple (interp-ctx J) Γ λ x → π₂ ∘ fs x)) ⟩
    project (interp-ctx A×B-ℐ𝓃𝓉) {Γ} {B} {x} {fs} =
      begin
      π (interp-ctx A×B-ℐ𝓃𝓉) x ∘
        (tuple (interp-ctx A×B-ℐ𝓃𝓉) Γ fs) ≈⟨ ⁂∘⟨⟩ ⟩
      ⟨ π (interp-ctx I) x ∘ tuple (interp-ctx I) Γ (λ x₁ → π₁ ∘ fs x₁) ,
        π (interp-ctx J) x ∘ tuple (interp-ctx J) Γ (λ x₁ → π₂ ∘ fs x₁) ⟩ ≈⟨ ⟨⟩-congʳ (project (interp-ctx I)) ⟩
      ⟨ π₁ ∘ fs x ,
        π (interp-ctx J) x ∘ tuple (interp-ctx J) Γ (λ x₁ → π₂ ∘ fs x₁) ⟩ ≈⟨ ⟨⟩-congˡ (project (interp-ctx J)) ⟩
      ⟨ π₁ ∘ fs x , π₂ ∘ fs x ⟩ ≈⟨ Product.unique product Equiv.refl Equiv.refl ⟩
      fs x ∎
    unique (interp-ctx A×B-ℐ𝓃𝓉) {Γ} {A} {g} {fs} ps = Product.unique product
                                                 (⟺ (unique (interp-ctx I) λ i → begin
                                                 π (interp-ctx I) i ∘ product.π₁  ∘ fs ≈⟨ sym-assoc ⟩
                                                 (π (interp-ctx I) i ∘ product.π₁) ∘ fs ≈⟨ (Π-nat₁ i ⟩∘⟨refl)  ⟩
                                                 (product.π₁ ∘ (π (interp-ctx A×B-ℐ𝓃𝓉) i)) ∘ fs  ≈⟨ assoc ⟩
                                                 product.π₁ ∘((π (interp-ctx A×B-ℐ𝓃𝓉) i)  ∘ fs) ≈⟨ (refl⟩∘⟨ ps i) ⟩
                                                 product.π₁ ∘ g i ∎))
                                                 (⟺ (unique (interp-ctx J) λ i → begin
                                                 (π (interp-ctx J) i ∘ π₂ ∘ fs) ≈⟨ sym-assoc ⟩
                                                 ((π (interp-ctx J) i ∘ π₂) ∘ fs) ≈⟨ (Π-nat₂ i ⟩∘⟨refl) ⟩
                                                 ((product.π₂ ∘ π (interp-ctx A×B-ℐ𝓃𝓉) i) ∘ fs) ≈⟨ assoc ⟩
                                                 (π₂ ∘ π (interp-ctx A×B-ℐ𝓃𝓉) i ∘ fs) ≈⟨ (refl⟩∘⟨ ps i) ⟩
                                                 (π₂ ∘ g i) ∎))
           where
           Π-nat₁ : {Γ : Context} → (i : var Γ) → π (interp-ctx I) i ∘ product.π₁ ≈ product.π₁ ∘ π (interp-ctx A×B-ℐ𝓃𝓉) i
           Π-nat₁ = λ i → ⟺ project₁

           Π-nat₂ : {Γ : Context} → (i : var Γ) → π (interp-ctx J) i ∘ product.π₂ ≈ product.π₂ ∘ π (interp-ctx A×B-ℐ𝓃𝓉) i
           Π-nat₂ = λ i → ⟺ project₂

    -- Operations
    interp-oper A×B-ℐ𝓃𝓉 = λ f → (interp-oper I f) ⁂ (interp-oper J f)

  -- Useful propoerties for the definition of projections
  module _ (I J : Interpretation) f where
    open Product.Producted
    open Interpretation
    open HomReasoning

    Π-nat₁ : {Γ : Context} → (i : var Γ) → π (interp-ctx I) i ∘ product.π₁ ≈ product.π₁ ∘ π (interp-ctx (A×B-ℐ𝓃𝓉 I J)) i
    Π-nat₁ = λ i → ⟺ project₁

    Π-nat₂ : {Γ : Context} → (i : var Γ) → π (interp-ctx J) i ∘ product.π₂ ≈ product.π₂ ∘ π (interp-ctx (A×B-ℐ𝓃𝓉 I J)) i
    Π-nat₂ = λ i → ⟺ project₂

    π₁-tuple : π₁ ≈ tuple (interp-ctx I) (oper-arity f) (λ i → π₁ ∘ (π (interp-ctx I) i ⁂ π (interp-ctx J) i))
    π₁-tuple = ⟺ (begin
                     tuple (interp-ctx I) (oper-arity f)
                       (λ i → π₁ ∘ (π (interp-ctx I) i ⁂ π (interp-ctx J) i)) ≈⟨ tuple-cong (interp-ctx I) (λ i → π₁∘⁂) ⟩
                     tuple (interp-ctx I) (oper-arity f) (λ x → π (interp-ctx I) x ∘ π₁) ≈⟨ ∘-distribʳ-tuple (interp-ctx I) ⟩
                     (tuple (interp-ctx I) (oper-arity f) (λ x → π (interp-ctx I) x) ∘ π₁) ≈⟨ ∘-resp-≈ˡ (Product.Producted.η (interp-ctx I)) ⟩
                     (id ∘ π₁) ≈⟨ identityˡ ⟩
                     π₁ ∎)

    π₂-tuple : π₂ ≈ tuple (interp-ctx J) (oper-arity f) (λ i → π₂ ∘ (π (interp-ctx I) i ⁂ π (interp-ctx J) i))
    π₂-tuple = ⟺ (begin
                      tuple (interp-ctx J) (oper-arity f)
                        (λ i → π₂ ∘ (π (interp-ctx I) i ⁂ π (interp-ctx J) i)) ≈⟨ tuple-cong (interp-ctx J) (λ i → π₂∘⁂) ⟩
                      tuple (interp-ctx J) (oper-arity f) (λ x → π (interp-ctx J) x ∘ π₂) ≈⟨ ∘-distribʳ-tuple (interp-ctx J) ⟩
                      (tuple (interp-ctx J) (oper-arity f) (λ x → π (interp-ctx J) x) ∘ π₂) ≈⟨ ∘-resp-≈ˡ (Product.Producted.η (interp-ctx J)) ⟩
                      (id ∘ π₂) ≈⟨ identityˡ ⟩
                      π₂ ∎)

  -- Definition of projections
  π₁-ℐ𝓃𝓉 : ∀ {I J : Interpretation} → A×B-ℐ𝓃𝓉 I J ⇒I I
  π₁-ℐ𝓃𝓉 {I} {J} =
                   let open HomReasoning in
                   let open Product.Producted in
                   let open Interpretation in
                   record
                     { hom-morphism = Cartesian.Cartesian.π₁ cartesian-𝒞
                     ; hom-commute = λ f → begin
                                             (π₁ ∘ interp-oper (A×B-ℐ𝓃𝓉 I J) f) ≈⟨ π₁∘⁂ ⟩
                                             (interp-oper I f ∘ π₁) ≈⟨ ∘-resp-≈ʳ (π₁-tuple I J f) ⟩
                                             (interp-oper I f ∘
                                               tuple (interp-ctx I) (oper-arity f)
                                               (λ i → π₁ ∘ (π (interp-ctx I) i ⁂ π (interp-ctx J) i))) ∎
                     }

  π₂-ℐ𝓃𝓉 : ∀ {I J : Interpretation} → A×B-ℐ𝓃𝓉 I J ⇒I J
  π₂-ℐ𝓃𝓉 {I} {J} =
                   let open HomReasoning in
                   let open Product.Producted in
                   let open Interpretation in
                   record
                     { hom-morphism = Cartesian.Cartesian.π₂ cartesian-𝒞
                     ; hom-commute = λ f → begin
                                             (π₂ ∘ interp-oper (A×B-ℐ𝓃𝓉 I J) f) ≈⟨ π₂∘⁂ ⟩
                                             (interp-oper J f ∘ π₂) ≈⟨ ∘-resp-≈ʳ (π₂-tuple I J f) ⟩
                                             (interp-oper J f ∘
                                               tuple (interp-ctx J) (oper-arity f)
                                               (λ i → π₂ ∘ (π (interp-ctx I) i ⁂ π (interp-ctx J) i))) ∎
                     }

  -- Useful properties for the definition of ⟨_,_⟩-ℐ𝓃𝓉
  module _ (I J K : Interpretation) f (ϕ : I ⇒I J) (ψ : I ⇒I K) where
         open Interpretation
         open HomReasoning
         open Product.Producted

         ⟨⟩-left : interp-oper J f ∘ tuple
                                        (interp-ctx J)
                                        (oper-arity f)
                                        (λ x → π₁ ∘ ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) x) ≈ _⇒I_.hom-morphism ϕ ∘ interp-oper I f
         ⟨⟩-left = begin
                   (interp-oper J f ∘
                     tuple (interp-ctx J) (oper-arity f)
                     (λ x →
                        π₁ ∘
                        ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) x)) ≈⟨ ∘-resp-≈ʳ (tuple-cong (interp-ctx J) λ i → sym-assoc) ⟩
                   (interp-oper J f ∘
                     tuple (interp-ctx J) (oper-arity f)
                     (λ x →
                        (π₁ ∘ ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩) ∘
                        π (interp-ctx I) x)) ≈⟨ ∘-resp-≈ʳ (tuple-cong (interp-ctx J) λ i → ∘-resp-≈ˡ project₁) ⟩
                   (interp-oper J f ∘
                     tuple (interp-ctx J) (oper-arity f)
                     (λ x → _⇒I_.hom-morphism ϕ ∘ π (interp-ctx I) x)) ≈⟨ ⟺ (_⇒I_.hom-commute ϕ f) ⟩
                   (_⇒I_.hom-morphism ϕ ∘ interp-oper I f) ∎

         ⟨⟩-right : interp-oper K f ∘ tuple
                                        (interp-ctx K)
                                        (oper-arity f)
                                        (λ x → π₂ ∘ ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) x) ≈ _⇒I_.hom-morphism ψ ∘ interp-oper I f
         ⟨⟩-right = begin
                   (interp-oper K f ∘
                     tuple (interp-ctx K) (oper-arity f)
                     (λ x →
                        π₂ ∘
                        ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) x)) ≈⟨ ∘-resp-≈ʳ (tuple-cong (interp-ctx K) λ i → sym-assoc) ⟩
                   (interp-oper K f ∘
                     tuple (interp-ctx K) (oper-arity f)
                     (λ x →
                        (π₂ ∘ ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩) ∘
                        π (interp-ctx I) x)) ≈⟨ ∘-resp-≈ʳ (tuple-cong (interp-ctx K) λ i → ∘-resp-≈ˡ project₂) ⟩
                   (interp-oper K f ∘
                     tuple (interp-ctx K) (oper-arity f)
                     (λ x → _⇒I_.hom-morphism ψ ∘ π (interp-ctx I) x)) ≈⟨ ⟺ (_⇒I_.hom-commute ψ f) ⟩
                   (_⇒I_.hom-morphism ψ ∘ interp-oper I f) ∎

  -- Definition of pairing
  ⟨_,_⟩-ℐ𝓃𝓉 : ∀ {I J K : Interpretation} → I ⇒I J → I ⇒I K → I ⇒I A×B-ℐ𝓃𝓉 J K
  ⟨_,_⟩-ℐ𝓃𝓉 {I} {J} {K} ϕ ψ =
     let open HomReasoning in
     let open Product.Producted in
     let open Interpretation in
     record
       { hom-morphism = λ {A} → ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩
       ; hom-commute = λ f →
                             ⟺ (begin
                                     (interp-oper (A×B-ℐ𝓃𝓉 J K) f ∘
                                       tuple (interp-ctx (A×B-ℐ𝓃𝓉 J K)) (oper-arity f)
                                       (λ i →
                                          ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) i)) ≈⟨ ⁂∘⟨⟩ ⟩
                                     ⟨
                                       interp-oper J f ∘
                                       tuple (interp-ctx J) (oper-arity f)
                                       (λ x →
                                          π₁ ∘
                                          ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) x)
                                       ,
                                       interp-oper K f ∘
                                       tuple (interp-ctx K) (oper-arity f)
                                       (λ x →
                                          π₂ ∘
                                          ⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ π (interp-ctx I) x)
                                       ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-left I J K f ϕ ψ) (⟨⟩-right I J K f ϕ ψ) ⟩
                                     product.⟨ _⇒I_.hom-morphism ϕ ∘ interp-oper I f ,
                                       _⇒I_.hom-morphism ψ ∘ interp-oper I f ⟩ ≈˘⟨ ⟨⟩∘ ⟩
                                     (⟨ _⇒I_.hom-morphism ϕ , _⇒I_.hom-morphism ψ ⟩ ∘ interp-oper I f) ∎)
       }

  -- Properties about projections and unicity
  project₁-ℐ𝓃𝓉 : {I J K : Interpretation} {h : I ⇒I J} {i : I ⇒I K} (A : sort) → π₁ ∘ ⟨ _⇒I_.hom-morphism {I} {J} h {A} , _⇒I_.hom-morphism {I} {K} i ⟩ ≈ _⇒I_.hom-morphism h
  project₁-ℐ𝓃𝓉 A = project₁

  project₂-ℐ𝓃𝓉 : {I J K : Interpretation} {h : I ⇒I J} {i : I ⇒I K} (A : sort) → π₂ ∘ ⟨ _⇒I_.hom-morphism {I} {J} h {A} , _⇒I_.hom-morphism {I} {K} i ⟩ ≈ _⇒I_.hom-morphism i
  project₂-ℐ𝓃𝓉 A = project₂

  unique-ℐ𝓃𝓉 : {I J K : Interpretation}
                 {h : I ⇒I A×B-ℐ𝓃𝓉 J K}
                 {i : I ⇒I J} {j : I ⇒I K} →
                 ((A : sort) → π₁ ∘ _⇒I_.hom-morphism h {A} ≈ _⇒I_.hom-morphism i) →
                 ((A : sort) → π₂ ∘ _⇒I_.hom-morphism h {A} ≈ _⇒I_.hom-morphism j) →
                 (A : sort) →
                   ⟨ _⇒I_.hom-morphism i {A} , _⇒I_.hom-morphism j ⟩ ≈ _⇒I_.hom-morphism h
  unique-ℐ𝓃𝓉 = λ p₁ p₂ A → unique (p₁ A) (p₂ A)

  -- Definition of the structure of the product
  product-ℐ𝓃𝓉 : ∀ {I J} → Product ℐ𝓃𝓉 I J
  product-ℐ𝓃𝓉 {I} {J} =
    record
      { A×B = A×B-ℐ𝓃𝓉 I J
      ; π₁ = π₁-ℐ𝓃𝓉 {I} {J}
      ; π₂ = π₂-ℐ𝓃𝓉 {I} {J}
      ; ⟨_,_⟩ = ⟨_,_⟩-ℐ𝓃𝓉
      ; project₁ = λ {K} {h} {i} A → project₁-ℐ𝓃𝓉 {K} {I} {J} {h} {i} A
      ; project₂ = λ {K} {h} {i} A → project₂-ℐ𝓃𝓉 {K} {I} {J} {h} {i} A
      ; unique = λ {K} {h} {i} {j} p₁ p₂ A → unique-ℐ𝓃𝓉 {K} {I} {J} {h} {i} {j} p₁ p₂ A
      }

  -- The terminal object
  terminal-ℐ𝓃𝓉 : Terminal ℐ𝓃𝓉
  terminal-ℐ𝓃𝓉 =
    record
      { ⊤ = Trivial
      ; ⊤-is-terminal =
        record
          { ! =
              record
                { hom-morphism = !
                ; hom-commute =  λ f → !-unique₂
                }
          ; !-unique = λ f A → !-unique₂
          }
      }

  -- The category of interpretations is cartesian
  cartesian-ℐ𝓃𝓉 : Cartesian.Cartesian ℐ𝓃𝓉
  cartesian-ℐ𝓃𝓉 =
    record
      { terminal = terminal-ℐ𝓃𝓉
      ; products = record { product = product-ℐ𝓃𝓉 }
      }

  -- Each projection is a natural transformation with respect to the interpretation
  open Interpretation
  open HomReasoning
  open Product.Producted

  natural-π₁ : {I J : Interpretation} {A : sort} {Γ : Context} (t : Term Γ A) → π₁ ∘ (interp-term (A×B-ℐ𝓃𝓉 I J) t) ≈ (interp-term I t) ∘ π₁
  natural-π₁ {I} {J} (Signature.tm-var x) = project₁
  natural-π₁ {I} {J} (Signature.tm-oper f xs) = begin
                                                 (π₁ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (tm-oper f xs)) ≈⟨ ∘-resp-≈ʳ ⁂∘⟨⟩ ⟩
                                                 (π₁ ∘
                                                    ⟨
                                                    interp-oper I f ∘
                                                    Product.Producted.tuple (interp-ctx I) (oper-arity f)
                                                    (λ i → π₁ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (xs i))
                                                    ,
                                                    interp-oper J f ∘
                                                    Product.Producted.tuple (interp-ctx J) (oper-arity f)
                                                    (λ i → π₂ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (xs i))
                                                    ⟩) ≈⟨ project₁ ⟩
                                                 (interp-oper I f ∘
                                                   Product.Producted.tuple (interp-ctx I) (oper-arity f)
                                                   (λ i → π₁ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (xs i))) ≈⟨ ∘-resp-≈ʳ (tuple-cong (interp-ctx I) λ i → natural-π₁ {I} {J} {arg-sort f i} (xs i)) ⟩
                                                 (interp-oper I f ∘
                                                   tuple (interp-ctx I) (oper-arity f)
                                                   (λ i → interp-term I (xs i) ∘ π₁)) ≈⟨ ∘-resp-≈ʳ (∘-distribʳ-tuple (interp-ctx I)) ⟩
                                                 (interp-oper I f ∘
                                                   tuple (interp-ctx I) (oper-arity f) (λ x → interp-term I (xs x)) ∘
                                                   π₁) ≈⟨ sym-assoc ⟩
                                                 ((interp-oper I f ∘
                                                    tuple (interp-ctx I) (oper-arity f) (λ x → interp-term I (xs x)))
                                                   ∘ π₁) ∎

  natural-π₂ : {I J : Interpretation} {A : sort} {Γ : Context} (t : Term Γ A) → π₂ ∘ (interp-term (A×B-ℐ𝓃𝓉 I J) t) ≈ (interp-term J t) ∘ π₂
  natural-π₂ {I} {J} (Signature.tm-var x) = project₂
  natural-π₂ {I} {J} (Signature.tm-oper f xs) = begin
                                                 (π₂ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (tm-oper f xs)) ≈⟨ ∘-resp-≈ʳ ⁂∘⟨⟩ ⟩
                                                 (π₂ ∘
                                                    ⟨
                                                    interp-oper I f ∘
                                                    Product.Producted.tuple (interp-ctx I) (oper-arity f)
                                                    (λ i → π₁ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (xs i))
                                                    ,
                                                    interp-oper J f ∘
                                                    Product.Producted.tuple (interp-ctx J) (oper-arity f)
                                                    (λ i → π₂ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (xs i))
                                                    ⟩) ≈⟨ project₂ ⟩
                                                 (interp-oper J f ∘
                                                   Product.Producted.tuple (interp-ctx J) (oper-arity f)
                                                   (λ i → π₂ ∘ interp-term (A×B-ℐ𝓃𝓉 I J) (xs i))) ≈⟨ ∘-resp-≈ʳ (tuple-cong (interp-ctx J) λ i → natural-π₂ {I} {J} {arg-sort f i} (xs i)) ⟩
                                                 (interp-oper J f ∘
                                                   tuple (interp-ctx J) (oper-arity f)
                                                   (λ i → interp-term J (xs i) ∘ π₂)) ≈⟨ ∘-resp-≈ʳ (∘-distribʳ-tuple (interp-ctx J)) ⟩
                                                 (interp-oper J f ∘
                                                   tuple (interp-ctx J) (oper-arity f) (λ x → interp-term J (xs x)) ∘
                                                   π₂) ≈⟨ sym-assoc ⟩
                                                 ((interp-oper J f ∘
                                                    tuple (interp-ctx J) (oper-arity f) (λ x → interp-term J (xs x)))
                                                   ∘ π₂) ∎

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

module Interpreter where

open import Function.Base using (_$_)
open import FreeReader

-- Runs it in the reader monad
runFree : ∀ {R A} → R → FreeReader R A → A
runFree r (Pure x) = x
runFree r (Bind x f) = runFree r $ f $ runFree r x
runFree r Ask = r
-- Since it's so simple, all these compute nicely
runFree r (LeftId a f i) = runFree r $ f a
runFree r (RightId x i) = runFree r x
runFree r (Assoc x f g i) = runFree r $ g $ runFree r $ f $ runFree r x

ext: agda


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

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

open import Level
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open Category C
open import Categories.Morphism C using (Epi; _≅_)
open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟)
open import Categories.Morphism.Reasoning C

open HomReasoning

record Initial : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊥ : Obj
    ! : {A : Obj} → (⊥ ⇒ A)
    !-unique : ∀ {A} → (f : ⊥ ⇒ A) → ! ≈ f

  !-unique₂ : ∀ {A} → (f g : ⊥ ⇒ A) → f ≈ g
  !-unique₂ f g = begin
    f ≈˘⟨ !-unique f ⟩
    ! ≈⟨ !-unique g ⟩
    g ∎
    where open HomReasoning

  ⊥-id : (f : ⊥ ⇒ ⊥) → f ≈ id
  ⊥-id f = !-unique₂ f id

open Initial

to-⊥-is-Epi : ∀ {A : Obj} {i : Initial} → (f : A ⇒ ⊥ i) → Epi f
to-⊥-is-Epi {_} {i} _ = λ g h _ → !-unique₂ i g h

up-to-iso : (i₁ i₂ : Initial) → ⊥ i₁ ≅ ⊥ i₂
up-to-iso i₁ i₂ = record
  { from = ! i₁
  ; to   = ! i₂
  ; iso  = record { isoˡ = ⊥-id i₁ _; isoʳ = ⊥-id i₂ _ }
  }

transport-by-iso : (i : Initial) → ∀ {X} → ⊥ i ≅ X → Initial
transport-by-iso i {X} i≅X = record
  { ⊥        = X
  ; !        = ! i ∘ to
  ; !-unique = λ h →  begin
    ! i ∘ to        ≈⟨ !-unique i (h ∘ from) ⟩∘⟨refl  ⟩
    (h ∘ from) ∘ to ≈⟨ cancelʳ isoʳ ⟩
    h              ∎
  }
  where open _≅_ i≅X

up-to-iso-unique : ∀ i i′ → (iso : ⊥ i ≅ ⊥ i′) → up-to-iso i i′ ≃ iso
up-to-iso-unique i i′ iso = ⌞ !-unique i _ ⌟

up-to-iso-invˡ : ∀ {t X} {i : ⊥ t ≅ X} → up-to-iso t (transport-by-iso t i) ≃ i
up-to-iso-invˡ {t} {i = i} = up-to-iso-unique t (transport-by-iso t i) i

up-to-iso-invʳ : ∀ {t t′} → ⊥ (transport-by-iso t (up-to-iso t t′)) ≡ ⊥ t′
up-to-iso-invʳ {t} {t′} = ≡.refl

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module BTA-ken where
-- specialize two-level typed terms to untyped lambda calculus

open import Data.Nat hiding (_<_)
open import Data.Bool
open import Data.Fin hiding (_≤_ ; pred; _+_)
open import Data.List
open import Data.Product

open import Function
open import Algebra.FunctionProperties using (Commutative; Identity; RightIdentity)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
open import Data.Nat.Properties

-- Binding times
data BT : Set where
  S : BT
  D : BT

-- defining a data type [BT],where two members are
-- [S] standing for "static" and [D] standing for dynamic.

-- ``subsumption'' binding times; static can be treated as dynamic,
-- but not vice versa
_≼_ : BT → BT → Bool
_≼_ D S  = false
_≼_ _ _  = true

record True : Set where
data False : Set where

isTrue : Bool → Set
isTrue true  = True
isTrue false = False

-- More general purpose definitions (should also be in standard library)
-- list membership
infix 4 _∈_
data _∈_ {A : Set} : A → List A → Set where
  hd : ∀ {x xs} → x ∈ (x ∷ xs)
  tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

-- Types of the calculus
mutual
  -- s ^ BT
  data AType : Set where
    Ann : BT → SType → AType

  -- int | t -> t
  data SType : Set where
    SInt  : SType
    SFun  : AType → AType → SType

-- aux definitions
ATInt : BT → AType
ATInt bt = Ann bt SInt
ATFun  : BT → AType → AType → AType
ATFun  bt at1 at2 = Ann bt (SFun at1 at2)

-- projection: get the BT from a type
btof : AType → BT
btof (Ann bt _) = bt

-- well-formedness
data wft : AType → Set where
  wf-int  : ∀ {bt} → wft (Ann bt SInt)
  wf-fun  : ∀ {bt at1 at2} → wft at1 → wft at2
          → isTrue (bt ≼ btof at1) → isTrue (bt ≼ btof at2) → wft (Ann bt (SFun at1 at2))

-- test for dynamic by wellformedness
data IsDynamic : AType → Set where
  is-dyn : ∀ σ → IsDynamic (Ann D σ)

lem-IsDynamic-by-wf : ∀ α → isTrue (D ≼ btof α) → IsDynamic α
lem-IsDynamic-by-wf (Ann S σ) ()
lem-IsDynamic-by-wf (Ann D σ) _ = is-dyn σ

-- typed annotated expressions
ACtx = List AType

data AExp (Δ : ACtx) : AType → Set where
  AVar : ∀ {α} → α ∈ Δ → AExp Δ α
  AInt : (bt : BT) → ℕ → AExp Δ (ATInt bt)
  ALam : ∀ {α₁ α₂} (bt : BT) → wft (ATFun bt α₂ α₁) → AExp (α₂ ∷ Δ) α₁ → AExp Δ (ATFun bt α₂ α₁)
  AApp : ∀ {α₁ α₂} (bt : BT) → wft (ATFun bt α₂ α₁) → AExp Δ (ATFun bt α₂ α₁) → AExp Δ α₂ → AExp Δ α₁

-- Untyped expression, but correctly scoped
data Exp' : ℕ → Set where
  EVar : ∀ {n} → Fin n → Exp' n
  EInt : ∀ {n} → ℕ → Exp' n
  ELam : ∀ {n} → Exp' (suc n) → Exp' n
  EApp : ∀ {n} → Exp' n → Exp' n → Exp' n

---

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

n+0≡n : ∀ n → n + 0 ≡ n
n+0≡n zero    = refl
n+0≡n (suc n) = cong suc $ n+0≡n n

+-comm : ∀ m n → m + n ≡ n + m
+-comm zero    n = sym (n+0≡n n)
+-comm (suc m) n =
  begin
    suc m + n
  ≡⟨ refl ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨ sym (m+1+n≡1+m+n n m) ⟩
    n + suc m
  ∎

≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n q = z≤n
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

≤-suc-right : ∀ {m n} → m ≤ n → m ≤ suc n
≤-suc-right z≤n = z≤n
≤-suc-right (s≤s p) = s≤s (≤-suc-right p)

≤-suc-left : ∀ {m n} → suc m ≤ n → m ≤ n
≤-suc-left (s≤s p) = ≤-suc-right p

xlate : ∀ {m} {n} → Exp' (m + suc n) → Exp' (suc (n + m))
xlate {m} {n} e rewrite m+1+n≡1+m+n m n | +-comm m n = e

shifter1 : ∀ {n} m → Exp' (suc n) → Exp' (suc (n + m))
shifter1 {n} m (EVar x) = xlate {m} (EVar (raise m x))
shifter1 m (EInt x) = EInt x
shifter1 m (ELam e) = ELam (shifter1 m e)
shifter1 m (EApp e e₁) = EApp (shifter1 m e) (shifter1 m e₁)

shifter0 : ∀ m → Exp' zero → Exp' m
shifter0 m (EVar ())
shifter0 m (EInt x) = EInt x
shifter0 m (ELam e) = ELam (shifter1 m e)
shifter0 m (EApp e e₁) = EApp (shifter0 m e) (shifter0 m e₁)

shifter : ∀ m d → Exp' m → Exp' (m + d)
shifter zero d e = shifter0 d e
shifter (suc m) d e = shifter1 d e

-- m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
-- m+n∸m≡n p

helper : ∀ {m n} → n ≤ m → Exp' (n + (m ∸ n)) → Exp' m
helper p e rewrite m+n∸m≡n p = e

-- index m = nesting level of dynamic definitions
Imp : (m : ℕ) → AType → Set
Imp m (Ann S SInt) = ℕ
Imp m (Ann S (SFun α₁ α₂)) = ∀ n → m ≤ n → (Imp n α₁ → Imp n α₂)
Imp m (Ann D σ) = Exp' m

-- index = nesting level of dynamic definitions
data AEnv1 : ℕ → ACtx → Set where
  [] : AEnv1 0 []
  consS : ∀ {m Δ o} → m ≤ o → (α : AType) → Imp o α → AEnv1 m Δ → AEnv1 o (α ∷ Δ)
  consD : ∀ {m Δ} → (α : AType) → isTrue (D ≼ btof α) → Imp (suc m) α → AEnv1 m Δ → AEnv1 (suc m) (α ∷ Δ)

lift1 : ∀ {m n} α → m ≤ n → Imp m α → Imp n α
lift1 (Ann S SInt) p v = v
lift1 (Ann S (SFun x x₁)) p v = λ k n≤k → v k (≤-trans p n≤k)
lift1 {m} {n} (Ann D σ) p v = helper p (shifter m (n ∸ m) v)

lookup1 : ∀ {α Δ m n} → m  ≤ n → AEnv1 m Δ → α ∈ Δ → Imp n α
lookup1 {α} p (consS _ .α x env) hd = lift1 α p x
lookup1 {α} p (consD .α x x₁ env) hd = lift1 α p x₁
lookup1 p (consS p' .y x env) (tl {_} {y} x₁) = lookup1 (≤-trans p' p) env x₁
lookup1 p (consD .y x x₁ env) (tl {_} {y} x₂) = lookup1 (≤-suc-left p) env x₂

pe1 : ∀ {α Δ} m → AExp Δ α → AEnv1 m Δ → Imp m α
pe1 m (AVar x) env = lookup1 ≤-refl env x
pe1 m (AInt S x) env = x
pe1 m (AInt D x) env = EInt x
pe1 m (ALam S x e) env = λ o p → λ v → pe1 o e (consS p _ v env)
pe1 m (ALam {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
pe1 m (ALam {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun _ _ d≤bt₁ d≤bt₂) e) env
  | is-dyn σ₁ | is-dyn σ₂ = ELam (pe1 (suc m) e (consD (Ann D σ₁) d≤bt₁ (EVar zero) env))
pe1 m (AApp S x e e₁) env = (pe1 m e env) m ≤-refl (pe1 m e₁ env)
pe1 m (AApp {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
pe1 m (AApp {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  | is-dyn σ₁ | is-dyn σ₂ = EApp (pe1 m e env) (pe1 m e₁ env)

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
{-# OPTIONS --universe-polymorphism #-}
module Graphs.GraphMorphism where

open import Data.Product
open import Level
open import Relation.Binary
  renaming (_⇒_ to _⊆_)
open import Relation.Binary.PropositionalEquality
  using ()
  renaming
    (_≡_ to _≣_
    ; refl  to ≣-refl
    ; sym   to ≣-sym
    ; trans to ≣-trans
    ; cong  to ≣-cong
    )

open import Graphs.Graph

record GraphMorphism {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
    (A : Graph o₁ ℓ₁ e₁) (B : Graph o₂ ℓ₂ e₂) : Set (o₁ ⊔ o₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₁ ⊔ e₂) where
  module A = Graph A
  module B = Graph B
  field
    F₀        : A.Obj → B.Obj
    F₁        : ∀ {X Y} → A [ X ↝ Y ] → B [ F₀ X ↝ F₀ Y ]
    .F-resp-≈ : ∀ {X Y}{f g : A [ X ↝ Y ]} → A [ f ≈ g ] → B [ F₁ f ≈ F₁ g ]

infixr 9 _∘_
infix  4 _≈_

id : ∀{o ℓ e}{A : Graph o ℓ e} → GraphMorphism A A
id = record
  { F₀        = λ A → A
  ; F₁        = λ f → f
  ; F-resp-≈  = λ f≈g → f≈g
  }

_∘_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
        {A : Graph o₀ ℓ₀ e₀} {B : Graph o₁ ℓ₁ e₁} {C : Graph o₂ ℓ₂ e₂}
    → GraphMorphism B C → GraphMorphism A B → GraphMorphism A C
G ∘ F = record
  { F₀ = λ A → G₀ (F₀ A)
  ; F₁ = λ f → G₁ (F₁ f)
  ; F-resp-≈ = λ f≈g → G-resp-≈ (F-resp-≈ f≈g)
  } where
    open GraphMorphism F
    open GraphMorphism G renaming (F₀ to G₀; F₁ to G₁; F-resp-≈ to G-resp-≈)

_≈₀_ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Graph o₁ ℓ₁ e₁} {B : Graph o₂ ℓ₂ e₂}
  → (F G : GraphMorphism A B)
  → Set (o₁ ⊔ o₂)
_≈₀_ {A = A}{B} F G
  = ∀ X → F₀ X ≣ G₀ X
  where
    open GraphMorphism F using (F₀)
    open GraphMorphism G renaming (F₀ to G₀)

isEquivalence₀ : ∀{o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Graph o₁ ℓ₁ e₁} {B : Graph o₂ ℓ₂ e₂}
  → IsEquivalence (_≈₀_ {A = A}{B})
isEquivalence₀ {A = A}{B} = record
  { refl  = λ     x → ≣-refl
  ; sym   = λ p   x → ≣-sym   (p x)
  ; trans = λ p q x → ≣-trans (p x) (q x)
  }

_≈₁_ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Graph o₁ ℓ₁ e₁} {B : Graph o₂ ℓ₂ e₂}
  → (F G : GraphMorphism A B)
  → Set (o₁ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₂)
_≈₁_ {A = A}{B} F G
  = ∀ {X Y} (f : A [ X ↝ Y ]) → B [ F₁ f ~ G₁ f ]
  where
    open GraphMorphism F using (F₁)
    open GraphMorphism G renaming (F₁ to G₁)

isEquivalence₁ : ∀{o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Graph o₁ ℓ₁ e₁} {B : Graph o₂ ℓ₂ e₂}
  → IsEquivalence (_≈₁_ {A = A}{B})
isEquivalence₁ {A = A}{B} = record
  { refl  = λ     f → refl
  ; sym   = λ p   f → sym   (p f)
  ; trans = λ p q f → trans (p f) (q f)
  } where open Heterogeneous B

_≈_ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Graph o₁ ℓ₁ e₁} {B : Graph o₂ ℓ₂ e₂}
  → (F G : GraphMorphism A B)
  → Set (o₁ ⊔ o₂ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ e₂)
_≈_ = _≈₀_ -×- _≈₁_

isEquivalence : ∀{o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {A : Graph o₁ ℓ₁ e₁} {B : Graph o₂ ℓ₂ e₂}
  → IsEquivalence (_≈_ {A = A}{B})
isEquivalence {A = A}{B} = record
  { refl  = λ {x}       → refl₀  {x} , λ f → refl₁  {x} f
  ; sym   = λ {x}{y}    → map (sym₀   {x}{y})    (sym₁   {x}{y})
  ; trans = λ {x}{y}{z} → zip (trans₀ {x}{y}{z}) (trans₁ {x}{y}{z})
  }
  where
    open IsEquivalence isEquivalence₀
      renaming (refl to refl₀; sym to sym₀; trans to trans₀)
    open IsEquivalence isEquivalence₁
      renaming (refl to refl₁; sym to sym₁; trans to trans₁)

.∘-resp-≈  : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
               {A : Graph o₀ ℓ₀ e₀} {B : Graph o₁ ℓ₁ e₁} {C : Graph o₂ ℓ₂ e₂}
               {F H : GraphMorphism B C} {G I : GraphMorphism A B}
           → F ≈ H → G ≈ I → F ∘ G ≈ H ∘ I
∘-resp-≈ {B = B} {C} {F}{H}{G}{I} F≈H G≈I
  = (λ x → helper₁ (proj₁ G≈I x) (proj₁ F≈H (GraphMorphism.F₀ I x)))
  , (λ q → helper₂ (proj₂ G≈I q) (proj₂ F≈H (GraphMorphism.F₁ I q)))
  where
  open Heterogeneous C
  module C = Graph C
  helper₁ : ∀ {x}
    → GraphMorphism.F₀ G x ≣ GraphMorphism.F₀ I x
    → GraphMorphism.F₀ F (GraphMorphism.F₀ I x) ≣ GraphMorphism.F₀ H (GraphMorphism.F₀ I x)
    → GraphMorphism.F₀ F (GraphMorphism.F₀ G x) ≣ GraphMorphism.F₀ H (GraphMorphism.F₀ I x)
  helper₁ g≣i f≣h = ≣-trans (≣-cong (GraphMorphism.F₀ F) g≣i) f≣h

  helper₂ : ∀ {a b c d} {z w} {f : B [ a ↝ b ]} {h : B [ c ↝ d ]} {i : C [ z ↝ w ]}
         → B [ f ~ h ] → C [ GraphMorphism.F₁ F h ~ i ] → C [ GraphMorphism.F₁ F f ~ i ]
  helper₂ (≈⇒~ f≈h) (≈⇒~ g≈i) = ≈⇒~ (C.Equiv.trans (GraphMorphism.F-resp-≈ F 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:
------------------------------------------------------------------------
-- Library stuff

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

if_then_else_ : ∀ {A : Set} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_∸_ : ℕ → ℕ → ℕ
m      ∸ zero  = m
zero   ∸ suc n = zero
suc m  ∸ suc n = m ∸ n

_≤_ : ℕ → ℕ → Bool
zero   ≤ n      = true
suc m  ≤ zero   = false
suc m  ≤ suc n  = m ≤ n

data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

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

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

record Σ (X : Set) (Y : X → Set) : Set where
  constructor _,_
  field
    proj₁ : X
    proj₂ : Y proj₁

_×_ : Set → Set → Set
X × Y = Σ X λ _ → Y

record Sig : Set₁ where
  constructor _◃_
  field
    Parameter : Set
    Arity     : Parameter → Set

open Sig public

⟦_⟧ : Sig → Set → Set
⟦ P ◃ A ⟧ X = Σ P λ p → A p → X

Alg : Sig → Set → Set
Alg Σ X = ⟦ Σ ⟧ X → X

data μ (C : Sig) : Set where
  sup : Alg C (μ C)

const^C : Set → Sig
const^C X = X ◃ λ _ → ⊥

_⊎^C_ : Sig → Sig → Sig
(P₁ ◃ A₁) ⊎^C (P₂ ◃ A₂) = (P₁ ⊎ P₂) ◃ [ A₁ , A₂ ]₁

_⋆^C_ : Sig → Set → Sig
C ⋆^C X = const^C X ⊎^C C

_⋆_ : Sig → Set → Set
C ⋆ X = μ (C ⋆^C X)

do : ∀ {C X} → Alg C (C ⋆ X)
do (p , k) = sup (inj₂ p , k)

record Monad (T : Set → Set) : Set₁ where
  infixl 1 _>>=_
  field
    return  : ∀ {X} → X → T X
    _>>=_   : ∀ {X Y} → T X → (X → T Y) → T Y

monad : ∀ {Σ} → Monad (_⋆_ Σ)
monad {Σ} = record
  { return = λ x → sup (inj₁ x , λ ())
  ; _>>=_  = _>>=_
  }
  where
  _>>=_ : ∀ {X Y} → Σ ⋆ X → (X → Σ ⋆ Y) → Σ ⋆ Y
  sup (inj₁ x , _) >>= f = f x
  sup (inj₂ p , k) >>= f = do (p , λ a → k a >>= f)

generic : ∀ {Σ} (p : Parameter Σ) → Σ ⋆ Arity Σ p
generic p = do (p , return)
  where
  open Monad monad

------------------------------------------------------------------------
-- Example

Π : (X : Set) → (X → Set) → Set
Π X Y = (x : X) → (X ◃ Y) ⋆ Y x

call : ∀ {X Y} → Π X Y
call x = generic x

dom : ∀ {X Y} → ∀ {x} → (X ◃ Y) ⋆ Y x → (X → Set) → Set
dom          (sup (inj₁ _ , _))  R = ⊤
dom {Y = Y}  (sup (inj₂ x , k))  R
  = R x × ((y : Y x) → dom (k y) R)

data Dom {X}{Y} (f : (x : X) → (X ◃ Y) ⋆ Y x) : X → Set
  where
  ⟨_⟩ : ∀ {x} → dom (f x) (Dom f) → Dom f x

dom-map : ∀ {X Y} {R₁ R₂ : X → Set} {x}
          {w : (X ◃ Y) ⋆ Y x} →
          (∀ {x} → R₁ x → R₂ x) → dom w R₁ → dom w R₂
dom-map {w = sup (inj₁ _ , _)} f  _         = tt
dom-map {w = sup (inj₂ _ , _)} f  (y₁ , k)  =
  f y₁ , λ y₂ → dom-map f (k y₂)

{-# TERMINATING #-}
bove-capretta : ∀ {X Y} (f : Π X Y) → (x : X) → Dom f x → Y x
bove-capretta {X}{Y} f x ⟨ d ⟩
  = helper (f x) (dom-map (λ {x′} → bove-capretta f x′) d)
  where
  helper : ∀ {x} (w : (X ◃ Y) ⋆ Y x) → dom w Y → Y x
  helper (sup (inj₁ y , _))  _        = y
  helper (sup (inj₂ _ , k)) (d , dk)  = helper (k d) (dk d)

module _ where
  open Monad monad
  gcd : Π (ℕ × ℕ) (λ _ →  ℕ)
  gcd (0 , n)          = return n
  gcd (m , 0)          = return m
  gcd (suc m , suc n)  = if m ≤ n
                         then  call (suc m , (n ∸ m))
                         else  call ((m ∸ n) , suc n)

acc : Dom gcd (8 , 12)
acc = ⟨ ⟨ ⟨ ⟨ _ ⟩ , _ ⟩ , _ ⟩ , _ ⟩ -- ⟨ ⟨ ⟨ ⟨ tt ⟩ , (λ _ → tt) ⟩ , (λ _ → tt) ⟩ , (λ _ → tt) ⟩

test-gcd′ : bove-capretta gcd (8 , 12) acc ≡ 4
test-gcd′ = refl


text:
module Cats.Category.One where

open import Data.Unit using (⊤ ; tt)
open import Level

open import Cats.Category

One : ∀ lo la l≈ → Category lo la l≈
One lo la l≈ = record
    { Obj = Lift lo ⊤
    ; _⇒_ = λ _ _ → Lift la ⊤
    ; _≈_ = λ _ _ → Lift l≈ ⊤
    ; id = lift tt
    ; _∘_ = λ _ _ → lift tt
    ; equiv
        = record
        { refl = lift tt
        ; sym = λ _ → lift tt
        ; trans = λ _ _ → lift tt
        }
    ; ∘-resp = λ _ _ → lift tt
    ; id-r = lift tt
    ; id-l = lift tt
    ; assoc = lift tt
    }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module regex where

data Regex ( Σ : Set) : Set  where
  ε     : Regex Σ                -- empty
  φ     : Regex  Σ               -- fail
  _*    : Regex  Σ  → Regex  Σ
  _&_   : Regex  Σ  → Regex  Σ → Regex Σ
  _||_  : Regex  Σ  → Regex  Σ → Regex Σ
  <_>   : Σ → Regex  Σ

infixr 40 _&_ _||_

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A pointwise lifting of a relation to incorporate a new infimum.
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Infimum

open import Relation.Binary

module Relation.Binary.Construct.Add.Infimum.Equality
  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Relation.Binary.Construct.Add.Point.Equality _≈_ public
  renaming
  (_≈∙_                 to _≈₋_
  ; ∙≈∙                 to ⊥₋≈⊥₋
  ; ≈∙-refl             to ≈₋-refl
  ; ≈∙-sym              to ≈₋-sym
  ; ≈∙-trans            to ≈₋-trans
  ; ≈∙-dec              to ≈₋-dec
  ; ≈∙-irrelevant       to ≈₋-irrelevant
  ; ≈∙-substitutive     to ≈₋-substitutive
  ; ≈∙-isEquivalence    to ≈₋-isEquivalence
  ; ≈∙-isDecEquivalence to ≈₋-isDecEquivalence
  )


text:
-- Andreas, 2017-07-24, issue #2654 reported by rntz
-- When splitting projections in an extended lambda,
-- we have to print them postfix, regardless of whether
-- the user chose --postfix-projections or not.

-- {-# OPTIONS --postfix-projections #-}
-- {-# OPTIONS -v interaction.case:60 #-}

open import Common.Product

dup : ∀{A : Set} (a : A) → A × A
dup = λ { x → {!!}  }  -- C-c C-c RET

-- Expected result after result splitting:
-- dup = λ { x .proj₁ → {!!} ; x .proj₂ → {!!}  }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
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.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_; foldr; map)
open import Function using (_∘_)

double-negation : ∀ {A : Set} → A → ¬ ¬ A
double-negation x ¬x = ¬x x

triple-negation : ∀ {A : Set} → ¬ ¬ ¬ A → ¬ A
triple-negation ¬¬¬x x = ¬¬¬x (double-negation x)

Stable : Set → Set
Stable A = ¬ ¬ A → A

¬-stable : ∀ {A : Set} → Stable (¬ A)
¬-stable = triple-negation

×-stable : ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
×-stable ¬¬x→x ¬¬y→y ¬¬xy =
  ⟨ ¬¬x→x (contraposition (contraposition proj₁) ¬¬xy)
  , ¬¬y→y (contraposition (contraposition proj₂) ¬¬xy)
  ⟩

∀-stable : ∀ {A : Set} {B : A → Set} → (∀ (x : A) → Stable (B x)) → Stable (∀ (x : A) → B x)
∀-stable ∀x→¬¬y→y ¬¬∀x→y x =
  ∀x→¬¬y→y x (contraposition (contraposition λ{∀x→y → ∀x→y x}) ¬¬∀x→y)

-- Gödel-Gentzen translation

{--
data Var : ℕ → Set where
  zero : ∀ (n : ℕ) → Var (suc n)
  suc : ∀ (n : ℕ) → Var n → Var (suc n)

data Formula : ℕ → Set where
  _`≡_ : ∀ (n : ℕ) → Var n → Var n → Formula n
  _`×_ : ∀ (n : ℕ) → Formula n → Formula n → Formula n
  _`⊎_ : ∀ (n : ℕ) → Formula n → Formula n → Formula n
  `¬_ : ∀ (n : ℕ) → Formula n → Formula n
--}

data Formula : Set₁ where
  atomic : ∀ (A : Set) → Formula
  _`×_ : Formula → Formula → Formula
  _`⊎_ : Formula → Formula → Formula
  `¬_ : Formula → Formula

interp : Formula → Set
interp (atomic A) =  A
interp (`A `× `B) = interp `A × interp `B
interp (`A `⊎ `B) = interp `A ⊎ interp `B
interp (`¬ `A) = ¬ interp `A

g : Formula → Formula
g (atomic A) =  `¬ `¬ (atomic A)
g (`A `× `B) = g `A `× g `B
g (`A `⊎ `B) = `¬ ((`¬ g `A) `× (`¬ g `B))
g (`¬ `A) = `¬ g `A

stable-g : ∀ (`A : Formula) → Stable (interp (g `A))
stable-g (atomic A) =  ¬-stable
stable-g (`A `× `B) =  ×-stable (stable-g `A) (stable-g `B)
stable-g (`A `⊎ `B) =  ¬-stable
stable-g (`¬ `A) = ¬-stable


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

open import Fragment.Equational.Theory

module Fragment.Equational.FreeExtension.Base (Θ : Theory) where

open import Fragment.Equational.Model Θ
open import Fragment.Equational.Coproduct Θ

open import Level using (Level; Setω; _⊔_)
open import Data.Nat using (ℕ)

private
  variable
    a ℓ : Level

Extension : Setω
Extension = ∀ {a} {ℓ} → Model {a} {ℓ} → ℕ → Model {a} {a ⊔ ℓ}

IsFreeExtension : Extension → Setω
IsFreeExtension _[_] =
  ∀ {a ℓ} (A : Model {a} {ℓ}) (n : ℕ) → IsCoproduct A (J n) (A [ n ])

record FreeExtension : Setω where
  field
    _[_]        : Extension
    _[_]-isFrex : IsFreeExtension _[_]

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Prelude.Function where

id : ∀ {a} {A : Set a} → A → A
id x = x
{-# INLINE id #-}

infixl -10 id
syntax id {A = A} x = x ofType A

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x
{-# INLINE const #-}

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} → (∀ x y → C x y) → ∀ y x → C x y
flip f x y = f y x
{-# INLINE flip #-}

infixr 9 _∘_
_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c}
        (f : ∀ {x} (y : B x) → C x y) (g : ∀ x → B x) →
        ∀ x → C x (g x)
(f ∘ g) x = f (g x)
{-# INLINE _∘_ #-}

infixr 9 _∘′_
_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         (B → C) → (A → B) → (A → C)
f ∘′ g = f ∘ g
{-# INLINE _∘′_ #-}

infixr -20 _$_ _$′_
infixr 0 case_of_ case_return_of_
_$_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
f $ x = f x

_$′_ : ∀ {a b}{A : Set a} {B : Set b} → (A → B) → A → B
f $′ x = f x

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

case₂_,_of_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A → B → (A → B → C) → C
case₂ x , y of f = f x y

case₃_,_,_of_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → A → B → C → (A → B → C → D) → D
case₃ x , y , z of f = f x y z

case₄_,_,_,_of_ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} →
                A → B → C → D → (A → B → C → D → E) → E
case₄ x , y , z , w of f = f x y z w

case_return_of_ : ∀ {a b} {A : Set a} (x : A) (B : A → Set b) → (∀ x → B x) → B x
case x return B of f = f x

infixr 0 letSyntax
syntax letSyntax e (λ x → b) = let[ x := e ] b
letSyntax : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
letSyntax x f = f x

{-# INLINE _$_ #-}
{-# INLINE _$′_ #-}
{-# INLINE case_of_ #-}
{-# INLINE case₂_,_of_ #-}
{-# INLINE case_return_of_ #-}

infixl 8 _on_
_on_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x y → B x → B y → Set c} →
         (∀ {x y} (z : B x) (w : B y) → C x y z w) → (f : ∀ x → B x) → ∀ x y →
         C x y (f x) (f y)
h on f = λ x y → h (f x) (f y)
{-# INLINE _on_ #-}

it : ∀ {a} {A : Set a} {{x : A}} → A
it {{x}} = x
{-# INLINE it #-}

asInstance : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ {{x}} → B x) → B x
asInstance x f = f {{x}}
{-# INLINE asInstance #-}

record Instance {a} (A : Set a) : Set a where
  constructor !
  field {{x}} : A

mkInstance : ∀ {a} {A : Set a} → A → Instance A
mkInstance x = ! {{x}}
{-# INLINE mkInstance #-}

-- Can be used to force normalisation at compile time.
static : ∀ {a} {A : Set a} → A → A
static x = x
{-# STATIC static #-}

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:
{-
  Definition of various kinds of categories.

  This library follows the UniMath terminology, that is:

  Concept              Ob C   Hom C  Univalence

  Precategory          Type   Type   No
  Category             Type   Set    No
  Univalent Category   Type   Set    Yes

  This file also contains
    - pathToIso : Turns a path between two objects into an isomorphism between them
    - opposite categories

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Category where

open import Cubical.Categories.Category.Base public
open import Cubical.Categories.Category.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Categories.Category

module Categories.Morphism.Lifts.Properties {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Data.Product using (_,_; proj₁; proj₂)

open import Categories.Category.Construction.Arrow 𝒞

open import Categories.Diagram.Pullback 𝒞
open import Categories.Diagram.Pushout 𝒞

open import Categories.Morphism.Lifts 𝒞

open import Categories.Morphism.Reasoning 𝒞 renaming (glue to glue-■)
import Categories.Morphism as Mor

open Category 𝒞
open Definitions 𝒞
open HomReasoning

-- We want to talk about retracts of morphisms, so
-- we don't use the definition of 'Retract' applied to '𝒞'
open Mor 𝒞 hiding (Retract)
open Mor using (Retract)
open Morphism⇒

--------------------------------------------------------------------------------
-- Lifting and Retractions

module _ {X Y T} {f : X ⇒ Y} {i : X ⇒ T} {p : T ⇒ Y} (factors : f ≈ p ∘ i) where

  -- If 'f' factors into 'p ∘ i' and 'f' has the left lifting property
  -- with respect to 'p', then 'f' is a retraction of 'i' in the arrow
  -- category of 𝒞.
  retract-liftˡ : Lifts f p → Retract Arrow (mor f) (mor i)
  retract-liftˡ lifts = record
    { section = mor⇒ (fill-commˡ ○ ⟺ identityʳ)
    ; retract = mor⇒ (⟺ factors ○ ⟺ identityʳ)
    ; is-retract = identity² , fill-commʳ
    }
    where
      open Filler (lifts (identityˡ ○ factors))

  -- We have an analogous situation for right lifts.
  retract-liftʳ : Lifts i f → Retract Arrow (mor f) (mor p)
  retract-liftʳ lifts = record
    { section = mor⇒ (identityˡ ○ factors)
    ; retract = mor⇒ (identityˡ ○ ⟺ fill-commʳ)
    ; is-retract = fill-commˡ , identity²
    }
    where
      open Filler (lifts (⟺ factors ○ ⟺ identityʳ))

--------------------------------------------------------------------------------
-- Closure Properties of Injective and Projective morphisms.

module _ {j} (J : MorphismClass j) where
  private
    variable
      X Y Z : Obj
      f g h i p : X ⇒ Y

  -- If 'f' is an isomorphism, then it must be J-Projective.
  iso-proj : ∀ {X Y} (f : X ⇒ Y) → IsIso f → Proj J f
  iso-proj f f-iso g g∈J {h} {i} comm = record
    { filler = h ∘ inv
    ; fill-commˡ = cancelʳ isoˡ
    ; fill-commʳ = extendʳ (⟺ comm) ○ elimʳ isoʳ
    }
    where
      open IsIso f-iso

  -- Dually, If 'f' is an isomorphism, then it must be J-Injective.
  iso-inj : ∀ {X Y} (f : X ⇒ Y) → IsIso f → Inj J f
  iso-inj f f-iso g g∈J {h} {i} comm = record
    { filler = inv ∘ i
    ; fill-commˡ = extendˡ comm ○ elimˡ isoˡ
    ; fill-commʳ = cancelˡ isoʳ
    }
    where
      open IsIso f-iso

  -- J-Projective morphisms are closed under composition.
  proj-∘ : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → Proj J f → Proj J g → Proj J (f ∘ g)
  proj-∘ {f = f} {g = g} f-proj g-proj h h∈J {k} {i} comm = record
    { filler = UpperFiller.filler
    ; fill-commˡ = begin
        UpperFiller.filler ∘ f ∘ g
      ≈⟨ pullˡ UpperFiller.fill-commˡ ⟩
        LowerFiller.filler ∘ g
      ≈⟨ LowerFiller.fill-commˡ ⟩
        k
      ∎

    ; fill-commʳ = UpperFiller.fill-commʳ
    }
    where
      module LowerFiller = Filler (g-proj h h∈J (assoc ○ comm))
      module UpperFiller = Filler (f-proj h h∈J (⟺ LowerFiller.fill-commʳ))

  -- J-Injective morphisms are closed under composition.
  inj-∘ : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → Inj J f → Inj J g → Inj J (f ∘ g)
  inj-∘ {f = f} {g = g} f-inj g-inj h h∈J {k} {i} comm = record
    { filler = LowerFiller.filler
    ; fill-commˡ = LowerFiller.fill-commˡ
    ; fill-commʳ = begin
        (f ∘ g) ∘ LowerFiller.filler
      ≈⟨ pullʳ LowerFiller.fill-commʳ ⟩
        f ∘ UpperFiller.filler
      ≈⟨ UpperFiller.fill-commʳ ⟩
        i
      ∎
    }
    where
      module UpperFiller = Filler (f-inj h h∈J (comm ○ assoc))
      module LowerFiller = Filler (g-inj h h∈J UpperFiller.fill-commˡ)

  -- J-Projective morphisms are stable under pushout.
  proj-pushout : ∀ {X Y Z} {p : X ⇒ Y} {f : X ⇒ Z} → (P : Pushout p f) → Proj J p → Proj J (Pushout.i₂ P)
  proj-pushout {p = p} {f = f} po p-proj h h∈J sq = record
    { filler = universal fill-commˡ
    ; fill-commˡ = universal∘i₂≈h₂
    ; fill-commʳ = unique-diagram (pullʳ universal∘i₁≈h₁ ○ fill-commʳ) (pullʳ universal∘i₂≈h₂ ○ ⟺ sq)
    }
    where
      open Pushout po
      open Filler (p-proj h h∈J (glue-■ sq commute))

  -- J-Injective morphisms are stable under pullback.
  inj-pullback : ∀ {X Y Z} {i : X ⇒ Z} {f : Y ⇒ Z} → (P : Pullback i f) → Inj J i → Inj J (Pullback.p₂ P)
  inj-pullback {i = i} {f = f} pb i-inj h h∈J sq = record
    { filler = universal fill-commʳ
    ; fill-commˡ = unique-diagram (pullˡ p₁∘universal≈h₁ ○ fill-commˡ) (pullˡ p₂∘universal≈h₂ ○ sq)
    ; fill-commʳ = p₂∘universal≈h₂
    }
    where
      open Pullback pb
      open Filler (i-inj h h∈J (glue-■ (⟺ commute) sq))

  -- J-Projective morphisms are stable under retractions.
  proj-retract : Proj J p → Retract Arrow (mor f) (mor p) → Proj J f
  proj-retract {p = p} {f = f} p-proj f-retracts h h∈J {g} {k} sq = record
    { filler = filler ∘ cod⇒ section
    ; fill-commˡ = begin
        (filler ∘ cod⇒ section) ∘ f
      ≈⟨ extendˡ (square section) ⟩
        (filler ∘ p) ∘ dom⇒ section
      ≈⟨ fill-commˡ ⟩∘⟨refl ⟩
        (g ∘ dom⇒ retract) ∘ dom⇒ section
      ≈⟨ cancelʳ (proj₁ is-retract) ⟩
        g
      ∎
    ; fill-commʳ = begin
        h ∘ filler ∘ cod⇒ section
      ≈⟨ extendʳ fill-commʳ ⟩
        k ∘ (cod⇒ retract ∘ cod⇒ section)
      ≈⟨ elimʳ (proj₂ is-retract) ⟩
        k
      ∎
    }
    where
      open Retract f-retracts
      open Filler (p-proj h h∈J (glue-■ sq (square retract)))

  -- J-Injective morphisms are stable under retractions.
  inj-retract : Inj J i → Retract Arrow (mor f) (mor i) → Inj J f
  inj-retract {i = i} {f = f} i-inj f-retracts h h∈J {g} {k} sq = record
    { filler = dom⇒ retract ∘ filler
    ; fill-commˡ = begin
        (dom⇒ retract ∘ filler) ∘ h
      ≈⟨ extendˡ fill-commˡ ⟩
        (dom⇒ retract ∘ dom⇒ section) ∘ g
      ≈⟨ elimˡ (proj₁ is-retract) ⟩
        g
      ∎
    ; fill-commʳ = begin
        f ∘ dom⇒ retract ∘ filler
      ≈⟨ extendʳ (⟺ (square retract)) ⟩
        cod⇒ retract ∘ i ∘ filler
      ≈⟨ refl⟩∘⟨ fill-commʳ ⟩
        cod⇒ retract ∘ cod⇒ section ∘ k
      ≈⟨ cancelˡ (proj₂ is-retract) ⟩
        k
      ∎
    }
    where
      open Retract f-retracts
      open Filler (i-inj h h∈J (glue-■ (square section) sq))

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers
------------------------------------------------------------------------

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

module Data.Rational.Base where

open import Function using (id)
open import Data.Integer.Base as ℤ using (ℤ; ∣_∣; +_; -[1+_])
import Data.Integer.GCD as ℤ
import Data.Integer.DivMod as ℤ
open import Data.Nat.GCD
open import Data.Nat.Divisibility as ℕDiv using (divides; 0∣⇒≡0)
open import Data.Nat.Coprimality as C using (Coprime; Bézout-coprime; coprime-/gcd)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc) hiding (module ℕ)
import Data.Nat.DivMod as ℕ
open import Data.Rational.Unnormalised using (ℚᵘ; mkℚᵘ; _≢0)
open import Data.Product
open import Data.Sum.Base using (inj₂)
open import Level using (0ℓ)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Decidable using (False; fromWitnessFalse; toWitnessFalse)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; subst; cong; cong₂; module ≡-Reasoning)

open ≡-Reasoning

-- Note, these are re-exported publicly to maintain backwards
-- compatability. Although we are unable (?) to put a warning on them,
-- using these from `Data.Rational` should be viewed as a deprecated
-- feature.

open import Data.Integer public using (+0; +[1+_])

------------------------------------------------------------------------
-- Rational numbers in reduced form. Note that there is exactly one
-- way to represent every rational number.

record ℚ : Set where
  constructor mkℚ
  field
    numerator     : ℤ
    denominator-1 : ℕ
    .isCoprime    : Coprime ∣ numerator ∣ (suc denominator-1)

  denominatorℕ : ℕ
  denominatorℕ = suc denominator-1

  denominator : ℤ
  denominator = + denominatorℕ

open ℚ public using ()
  renaming
  ( numerator    to ↥_
  ; denominator  to ↧_
  ; denominatorℕ to ↧ₙ_
  )

mkℚ+ : ∀ n d → .{d≢0 : d ≢0} → .(Coprime n d) → ℚ
mkℚ+ n (suc d) coprime = mkℚ (+ n) d coprime

------------------------------------------------------------------------
-- Equality of rational numbers (coincides with _≡_)

infix 4 _≃_

_≃_ : Rel ℚ 0ℓ
p ≃ q = (↥ p ℤ.* ↧ q) ≡ (↥ q ℤ.* ↧ p)

------------------------------------------------------------------------
-- Ordering of rationals

infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≱_ _≮_ _≯_

data _≤_ : Rel ℚ 0ℓ where
  *≤* : ∀ {p q} → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p) → p ≤ q

data _<_ : Rel ℚ 0ℓ where
  *<* : ∀ {p q} → (↥ p ℤ.* ↧ q) ℤ.< (↥ q ℤ.* ↧ p) → p < q

_≥_ : Rel ℚ 0ℓ
x ≥ y = y ≤ x

_>_ : Rel ℚ 0ℓ
x > y = y < x

_≰_ : Rel ℚ 0ℓ
x ≰ y = ¬ (x ≤ y)

_≱_ : Rel ℚ 0ℓ
x ≱ y = ¬ (x ≥ y)

_≮_ : Rel ℚ 0ℓ
x ≮ y = ¬ (x < y)

_≯_ : Rel ℚ 0ℓ
x ≯ y = ¬ (x > y)

------------------------------------------------------------------------
-- Negation

-_ : ℚ → ℚ
- mkℚ -[1+ n ] d prf = mkℚ +[1+ n ] d prf
- mkℚ +0       d prf = mkℚ +0       d prf
- mkℚ +[1+ n ] d prf = mkℚ -[1+ n ] d prf

------------------------------------------------------------------------
-- Constructing rationals

-- A constructor for ℚ that takes two natural numbers, say 6 and 21,
-- and returns them in a normalized form, e.g. say 2 and 7

normalize : ∀ (m n : ℕ) {n≢0 : n ≢0} → ℚ
normalize m n {n≢0} = mkℚ+ (m ℕ./ gcd m n) (n ℕ./ gcd m n)
  {n/g≢0} (coprime-/gcd m n {g≢0})
  where
  g≢0   = fromWitnessFalse (gcd[m,n]≢0 m n (inj₂ (toWitnessFalse n≢0)))
  n/g≢0 = fromWitnessFalse (n/gcd[m,n]≢0 m n {n≢0} {g≢0})

-- A constructor for ℚ that (unlike mkℚ) automatically normalises it's
-- arguments. See the constants section below for how to use this operator.

infixl 7 _/_

_/_ : (n : ℤ) (d : ℕ) → {d≢0 : d ≢0} → ℚ
(+ n      / d) {d≢0} =   normalize n       d {d≢0}
(-[1+ n ] / d) {d≢0} = - normalize (suc n) d {d≢0}

------------------------------------------------------------------------------
-- Some constants

0ℚ : ℚ
0ℚ = + 0 / 1

1ℚ : ℚ
1ℚ = + 1 / 1

½ : ℚ
½ = + 1 / 2

-½ : ℚ
-½ = - ½

------------------------------------------------------------------------------
-- Operations on rationals

infix  8 -_ 1/_
infixl 7 _*_ _÷_
infixl 6 _-_ _+_

-- addition

_+_ : ℚ → ℚ → ℚ
p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)

-- multiplication

_*_ : ℚ → ℚ → ℚ
p * q = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)

-- subtraction

_-_ : ℚ → ℚ → ℚ
p - q = p + (- q)

-- reciprocal: requires a proof that the numerator is not zero

1/_ : (p : ℚ) → .{n≢0 : ∣ ↥ p ∣ ≢0} → ℚ
1/ mkℚ +[1+ n ] d prf = mkℚ +[1+ d ] n (C.sym prf)
1/ mkℚ -[1+ n ] d prf = mkℚ -[1+ d ] n (C.sym prf)

-- division: requires a proof that the denominator is not zero

_÷_ : (p q : ℚ) → .{n≢0 : ∣ ↥ q ∣ ≢0} → ℚ
(p ÷ q) {n≢0} = p * (1/ q) {n≢0}

------------------------------------------------------------------------
-- Conversion to and from unnormalized rationals

toℚᵘ : ℚ → ℚᵘ
toℚᵘ (mkℚ n d-1 _) = mkℚᵘ n d-1

fromℚᵘ : ℚᵘ → ℚ
fromℚᵘ (mkℚᵘ n d-1) = n / suc d-1


text:
------------------------------------------------------------------------------
-- Testing the translation of logical schemata with 11-ary predicates symbols
------------------------------------------------------------------------------

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

module P11 where

postulate
  D      : Set
  P-refl : {P : D → D → D → D → D → D → D → D → D → D → D → Set} →
           ∀ {x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁} →
           P x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁ →
           P x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁
{-# ATP prove P-refl #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- Safe modules that use --cubical
------------------------------------------------------------------------

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

module README.Safe.Cubical where

-- A proof of univalence.

import Equality.Path.Univalence

-- A proof of univalence for an arbitrary "equality with J".

import Equality.Path.Isomorphisms.Univalence

-- Very stable booleans.

import Bool.Very-stable

-- Listed finite subsets.

import Finite-subset.Listed

-- An alternative definition of listed finite subsets.

import Finite-subset.Listed.Alternative

-- Kuratowski finite subsets.

import Finite-subset.Kuratowski

-- An example related to Nat.Wrapper, defined in Cubical Agda.

import Nat.Wrapper.Cubical

-- Abstract binding trees, based on Harper's "Practical Foundations
-- for Programming Languages".

import Abstract-binding-tree
import README.Abstract-binding-tree

-- Overview of code related to a paper.

import README.HITs-without-paths

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Char.Properties where

open import Agda.Builtin.Char
open import Agda.Builtin.Equality

primitive

  primCharToNatInjective : ∀ a b → primCharToNat a ≡ primCharToNat b → a ≡ b

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.S1.Properties where

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

open import Cubical.HITs.S1.Base
open import Cubical.HITs.PropositionalTruncation

isConnectedS¹ : (s : S¹) → ∥ base ≡ s ∥
isConnectedS¹ base = ∣ refl ∣
isConnectedS¹ (loop i) =
  squash ∣ (λ j → loop (i ∧ j)) ∣ ∣ (λ j → loop (i ∨ ~ j)) ∣ i

isGroupoidS¹ : isGroupoid S¹
isGroupoidS¹ s t =
  recPropTrunc isPropIsSet
    (λ p →
      subst (λ s → isSet (s ≡ t)) p
        (recPropTrunc isPropIsSet
          (λ q → subst (λ t → isSet (base ≡ t)) q isSetΩS¹)
          (isConnectedS¹ t)))
    (isConnectedS¹ s)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Andreas, 2016-02-09, issue and test case by Nisse

{-# OPTIONS --allow-unsolved-metas #-}

open import Common.Level

postulate
  _≡_  : ∀ {a} {A : Set a} → A → A → Set a
  refl : ∀ {a} {A : Set a} (x : A) → x ≡ x

record R a p : Set (lsuc (a ⊔ p)) where
  field
    elim : {A : Set a} (P : {x y : A} → x ≡ y → Set p) →
           (∀ x → P (refl x)) →
           ∀ {x y} (x≡y : x ≡ y) → P x≡y

module _ (eq : ∀ {a p} → R a p) where

  open module M {a p} = R (eq {a} {p})

  postulate

    elim-refl   : ∀ {a p} {A : Set a} (P : {x y : A} → x ≡ y → Set p)
                  (r : ∀ x → P (refl x)) {x} →
                  elim P r (refl x) ≡ r x
    cong        : ∀ {a b} {A : Set a} {B : Set b}
                  (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
    subst       : ∀ {a p} {A : Set a} (P : A → Set p) {x y : A} →
                  x ≡ y → P x → P y
    subst-refl  : ∀ {a p} {A : Set a} (P : A → Set p) {x} (p : P x) →
                  subst P (refl x) p ≡ p
    trans       : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
    cong₂       : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
                  (f : A → B → C) {x y : A} {u v : B} →
                  x ≡ y → u ≡ v → f y v ≡ f x u
    trans-reflʳ : ∀ {a} {A : Set a} {x y : A} (x≡y : x ≡ y) →
                  trans x≡y (refl y) ≡ x≡y
    trans-reflˡ : ∀ {a} {A : Set a} {x y : A} (x≡y : x ≡ y) →
                  trans (refl x) x≡y ≡ x≡y

  [subst≡]≡[trans≡trans] :
    ∀ {a} {A : Set a} {x y : A} {p : x ≡ y} {q : x ≡ x} {r : y ≡ y} →
    (subst (λ z → z ≡ z) p q ≡ r)
      ≡
    (trans q p ≡ trans p r)
  [subst≡]≡[trans≡trans] {p = p} {q} {r} = elim
    (λ {x y} p → {q : x ≡ x} {r : y ≡ y} →
                 (subst (λ z → z ≡ z) p q ≡ r)
                   ≡
                 (trans q p ≡ trans p r))
    (λ x {q r} →
       trans (cong (λ x → x ≡ _) (subst-refl (λ z → z ≡ z) _))
             (cong₂ _≡_ (trans-reflʳ _) (trans-reflˡ _)))
    p

  foo :
    ∀ {a} {A : Set a} {x : A} {q : x ≡ x} {r : x ≡ x} →
    [subst≡]≡[trans≡trans] {p = refl x} {q = q} {r = r} ≡
    [subst≡]≡[trans≡trans] {p = refl x} {q = q} {r = r}
  foo = elim-refl ? ?

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.S3.Base where

open import Cubical.Foundations.Prelude

data S³ : Type₀ where
  base : S³
  surf : PathP (λ j → PathP (λ i → base ≡ base) refl refl) refl refl


text:
{-# OPTIONS --without-K #-}
module hott.truncation.elim where

open import sum
open import equality
open import function
open import hott.equivalence
open import hott.level
open import hott.loop
open import hott.truncation.core
open import hott.truncation.equality
open import hott.univalence
open import sets.nat
open import sets.unit

is-null : ∀ {i j}{X : Set i}{Y : Set j} → Y → (X → Y) → Set _
is-null y f = ∀ x → y ≡ f x

is-null-level : ∀ {i j}{X : Set i}{Y : Set j} → h 2 Y
              → (y : Y)(f : X → Y) → h 1 (is-null y f)
is-null-level hY y f = Π-level λ x → hY y (f x)

compose-is-null : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
                → (y : Y)(f : X → Y)(g : Y → Z)
                → is-null y f
                → is-null (g y) (g ∘ f)
compose-is-null y f g c y' = ap g (c y')

Null : ∀ {i j} → ℕ → Set i → Set j → Set _
Null n X Y = Σ (X → Y) λ f → (x : X) → is-null (refl' n (f x)) (mapΩ n f)

-- connected components

Conn : ∀ {i}{X : Set i}(n : ℕ) → Trunc n X → Set _
Conn {X = X} n c = Σ X λ x → [ x ] ≡ c

map-conn : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
         → (c : Trunc n X)
         → (X → Y)
         → (Conn n c → Y)
map-conn n c f (x , p) = f x

conn-decomp : ∀ {i}{X : Set i}(n : ℕ)
            → Σ (Trunc n X) (Conn n) ≅ X
conn-decomp {X = X} n = total-iso [_]

conn-connected : ∀ {i}{X : Set i}(n : ℕ)(c : Trunc n X)
               → contr (Trunc n (Conn n c))
conn-connected {X = X} n c = φ c , lem c
  where
    φ' : (x : X) → Trunc n (Conn n [ x ])
    φ'  x = [ x , refl ]

    φ : (c : Trunc n X) → Trunc n (Conn n c)
    φ = Trunc-dep-elim n (λ c → Trunc n (Conn n c)) (λ _ → Trunc-level n) φ'

    lem' : (c : Trunc n X)(a : Conn n c) → φ c ≡ [ a ]
    lem' .([ x ]) (x , refl) = Trunc-dep-elim-β n
      (λ c → Trunc n (Conn n c))
      (λ _ → Trunc-level n) φ' x

    lem : (c : Trunc n X)(a : Trunc n (Conn n c)) → φ c ≡ a
    lem c = Trunc-dep-elim n (λ a → φ c ≡ a) (λ a → h↑ (Trunc-level n) (φ c) a) (lem' c)

-- main result

module CM {i j} n (X : Set i)(Y : Set j)
          (hY : h (n + 2) Y) where
  cm' : Y → Null n X Y
  cm' y = (λ _ → y) , (λ x p → sym (mapΩ-const n y x p))

  cm : (Trunc (suc n) X → Y) → Null n X Y
  cm f = (λ x → f [ x ]) , λ x
       → subst₂ (is-null) (mapΩ-refl n f) (eq x)
               (compose-is-null (refl' n [ x ]) (mapΩ n [_]) (mapΩ n f)
                 (λ p → h1⇒prop (Ω-level n hT) _ _))
     where
       f' : X → Y
       f' x = f [ x ]

       eq' : (x : X)(p : Ω n x) → mapΩ n f (mapΩ n [_] p) ≡ mapΩ n f' p
       eq' x p = mapΩ-hom n [_] f p

       eq : (x : X) → mapΩ n f ∘ mapΩ n [_] ≡ mapΩ n f'
       eq x = funext (eq' x)

       hT : h (n + 1) (Trunc (suc n) X)
       hT = subst (λ m → h m (Trunc (suc n) X)) (+-commutativity 1 n) (Trunc-level (suc n))

Trunc-elim' : ∀ {i j} n (X : Set i)(Y : Set j) → h (n + 2) Y
            → (Trunc (suc n) X → Y) ≅ Null n X Y

null-connected : ∀ {i j} n {X : Set i}{Y : Set j}
               → contr (Trunc (suc n) X)
               → h (n + 2) Y
               → (f : X → Y)
               → ((x : X) → is-null (refl' n (f x)) (mapΩ n f {x}))
               → (x : X) → is-null (f x) f
null-connected zero hX hY f c x₀ x₁ = c x₀ x₁
null-connected (suc n) {X} hX hY f c x₀ x₁
  = φ (trunc-equality (suc n) (h1⇒prop (h↑ hX) _ _))
  where
    ap-null : (x y : X)(p : x ≡ y) → is-null (refl' n (ap f p)) (mapΩ n (ap f) {p})
    ap-null x .x refl = c x

    φ : Trunc (suc n) (x₀ ≡ x₁) → f x₀ ≡ f x₁
    φ = invert (Trunc-elim' n (x₀ ≡ x₁) (f x₀ ≡ f x₁) (hY _ _))
        ( ap f , ap-null x₀ x₁ )

Trunc-elim-connected : ∀ {i j} n (X : Set i)(Y : Set j)
                     → contr (Trunc (suc n) X)
                     → h (n + 2) Y
                     → Y ≅ Null n X Y
Trunc-elim-connected n X Y hX hY = ≈⇒≅ (cm' , cm-equiv' (proj₁ hX))
  where
    open CM n X Y hY

    module _ (x₀ : X) where
      g : Null n X Y → Y
      g (f , c) = f x₀

      α : (y : Y) → g (cm' y) ≡ y
      α y = refl

      β : (x : Null n X Y) → cm' (g x) ≡ x
      β (f , c) = unapΣ ( (funext λ x → null-connected n hX hY f c _ _)
                        , h1⇒prop (Π-level λ x → is-null-level (Ω-level n hY) _ _) _ _)

      f-iso : Y ≅ Null n X Y
      f-iso = iso cm' g α β

    cm-equiv : X → weak-equiv cm'
    cm-equiv x₀ = proj₂ (≅⇒≈ (f-iso x₀))

    cm-equiv' : Trunc (suc n) X → weak-equiv cm'
    cm-equiv' = invert (Trunc-elim-iso (suc n) X (weak-equiv cm') (h! (weak-equiv-h1 cm'))) cm-equiv

abstract
  Trunc-elim'₀ : ∀ {i j} n (X : Set i)(Y : Set j) → h (n + 2) Y
              → (Trunc (suc n) X → Y) ≅ Null n X Y
  Trunc-elim'₀ n X Y hY = begin
      (Trunc (suc n) X → Y)
    ≅⟨ ( Π-ap-iso refl≅ λ c
       → Trunc-elim-connected n _ _ (conn-connected (suc n) c) hY) ⟩
      ((c : Trunc (suc n) X) → Null n (Conn (suc n) c) Y)
    ≅⟨ ΠΣ-swap-iso ⟩
      ( Σ ((c : Trunc (suc n) X) → Conn (suc n) c → Y) λ f
      → ((c : Trunc (suc n) X) → (x : Conn (suc n) c) → is-null _ (mapΩ n (f c))) )
    ≅⟨ sym≅ ( Σ-ap-iso (curry-iso (λ _ _ → Y)) λ f
            → curry-iso λ c x → is-null _ (mapΩ n (λ x' → f (c , x')))  ) ⟩
      ( Σ ((Σ (Trunc (suc n) X) λ c → Conn (suc n) c) → Y) λ f
      → (((x' : (Σ (Trunc (suc n) X) λ c → Conn (suc n) c))
           → is-null _ (mapΩ n (λ x → f (proj₁ x' , x))))) )
    ≅⟨ ( Σ-ap-iso' (→-ap-iso (conn-decomp (suc n)) refl≅) λ f
       → Π-ap-iso (conn-decomp (suc n)) λ x → refl≅ ) ⟩
      ( Σ (X → Y) λ f
      → (((x : X) → is-null _ (mapΩ n (λ x → f (proj₁ x)) {x , refl}))) )
    ≅⟨ ( Σ-ap-iso refl≅ λ f → Π-ap-iso refl≅ λ x → lem f x ) ⟩
      Null n X Y
    ∎
    where
      open ≅-Reasoning

      lem : (f : X → Y) (x : X)
          → is-null (refl' n (f x)) (mapΩ n (map-conn (suc n) [ x ] f) {x , refl})
          ≅ is-null (refl' n (f x)) (mapΩ n f {x})
      lem f x = ≡⇒≅ (ap (is-null (refl' n (f x))) (funext hom)) ·≅ sym≅ is-const-equiv
        where
          π : Conn (suc n) [ x ] → X
          π = proj₁

          hom : (p : Ω n (x , refl))
              → mapΩ n (map-conn (suc n) [ x ] f) p
              ≡ mapΩ n f (mapΩ n proj₁ p)
          hom p = sym (mapΩ-hom n proj₁ f p)

          φ : Ω n {Conn (suc n) [ x ]} (x , refl) ≅ Ω n x
          φ = loop-sum n λ a → Trunc-level (suc n) _ _

          is-const-equiv : is-null {X = Ω n x} (refl' n (f x)) (mapΩ n f {x})
                         ≅ is-null {X = Ω n {Conn (suc n) [ x ]} (x , refl)}
                                   (refl' n (f x))
                                   (mapΩ n f ∘ mapΩ n proj₁)
          is-const-equiv = Π-ap-iso (sym≅ φ) λ p
                         → refl≅

  Trunc-elim'-β₀ : ∀ {i j n}{X : Set i}{Y : Set j} (hY : h (n + 2) Y)
                → (f : Trunc (suc n) X → Y)
                → proj₁ (apply (Trunc-elim'₀ n X Y hY) f) ≡ (λ x → f [ x ])
  Trunc-elim'-β₀ hY f = refl

  Trunc-elim'-β : ∀ {i j n}{X : Set i}{Y : Set j} (hY : h (n + 2) Y)
                → (f : Trunc (suc n) X → Y)
                → apply (Trunc-elim'₀ n X Y hY) f ≡ CM.cm n X Y hY f
  Trunc-elim'-β {n = n} hY f = unapΣ
    ( Trunc-elim'-β₀ hY f
    , h1⇒prop (Π-level λ x → is-null-level (Ω-level n hY) _ _) _ _ )

Trunc-elim' n X Y hY = ≈⇒≅ (cm , cm-we)
  where
    open CM n X Y hY

    cm-eq : apply (Trunc-elim'₀ n X Y hY) ≡ cm
    cm-eq = funext (Trunc-elim'-β hY)

    cm-we : weak-equiv cm
    cm-we = subst weak-equiv cm-eq (proj₂ (≅⇒≈ (Trunc-elim'₀ n X Y hY)))

-- example

Repr : ∀ {i} → Set i → Set _
Repr {i} A = Σ (Trunc 2 A → Set i) λ hom
       → (a : A) → hom [ a ] ≅ (a ≡ a)

Braiding : ∀ {i} → Set i → Set _
Braiding A = {a : A}(p q : a ≡ a) → p · q ≡ q · p

braiding-repr : ∀ {i}{A : Set i} → h 3 A → Braiding A → Repr A
braiding-repr {i}{A} hA γ = (λ c → proj₁ (hom c)) , λ a
                          → ≡⇒≅ (ap proj₁ (hom-β a))
  where
    eq : A → Set _
    eq a = (a ≡ a)

    hom' : A → Type _ 2
    hom' a = eq a , hA a a

    type-eq-iso : ∀ {n}{X Y : Type i n}
                → (X ≡ Y) ≅ (proj₁ X ≈ proj₁ Y)
    type-eq-iso {n}{X}{Y} = begin
        (X ≡ Y)
      ≅⟨ sym≅ Σ-split-iso ⟩
        (Σ (proj₁ X ≡ proj₁ Y) λ p → subst (h n) p (proj₂ X) ≡ proj₂ Y)
      ≅⟨ (Σ-ap-iso refl≅ λ p → contr-⊤-iso (hn-h1 n _ _ _)) ⟩
        ((proj₁ X ≡ proj₁ Y) × ⊤)
      ≅⟨ ×-right-unit ⟩
        (proj₁ X ≡ proj₁ Y)
      ≅⟨ uni-iso ⟩
        (proj₁ X ≈ proj₁ Y)
      ∎
      where open ≅-Reasoning

    type-eq : ∀ {n}{X : Type i n}{p : X ≡ X}
            → ((x : proj₁ X) → coerce (ap proj₁ p) x ≡ x)
            → p ≡ refl
    type-eq f = invert≅ (iso≡ type-eq-iso) (unapΣ
              ( funext f , h1⇒prop (weak-equiv-h1 _) _ _))

    ap-eq : {a b : A}(p : a ≡ b)(q : a ≡ a) → coerce (ap proj₁ (ap hom' p)) q ≡ sym p · q · p
    ap-eq refl q = sym (left-unit q)

    hom-null : (a : A) → is-null refl (mapΩ 1 hom' {a})
    hom-null a p = sym (type-eq λ q → ap-eq p q
                                    · ap (λ z → z · p) (γ (sym p) q)
                                    · associativity q (sym p) p
                                    · ap (λ z → q · z) (right-inverse p)
                                    · left-unit q)

    hom-iso : (Trunc 2 A → Type i 2) ≅ Null 1 A (Type i 2)
    hom-iso = Trunc-elim' 1 A (Type i 2) type-level

    hom : Trunc 2 A → Type _ 2
    hom = invert hom-iso (hom' , hom-null)

    hom-β : (a : A) → hom [ a ] ≡ hom' a
    hom-β a = funext-inv (ap proj₁ (_≅_.iso₂ hom-iso (hom' , hom-null))) a

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Records where

data Sigma (A : Set) (B : A -> Set) : Set where
  _,_ : (x : A) (y : B x) -> Sigma A B

fst : {A : Set}{B : A -> Set} -> Sigma A B -> A
fst (x , y) = x

snd : {A : Set}{B : A -> Set} -> (p : Sigma A B) -> B (fst p)
snd (x , y) = y

data Sigma1 (A : Set1) (B : A -> Set1) : Set1 where
  _,_ : (x : A) (y : B x) -> Sigma1 A B

fst1 : {A : Set1}{B : A -> Set1} -> Sigma1 A B -> A
fst1 (x , y) = x

snd1 : {A : Set1}{B : A -> Set1} -> (p : Sigma1 A B) -> B (fst1 p)
snd1 (x , y) = y

data Zero : Set where
data Unit  : Set where
  Void : Unit

data Test1 : Set where
data Test2 : Set where
data Test3 : Set where

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

data Fin : Nat -> Set where
  fze : {n : Nat} -> Fin (su n)
  fsu : {n : Nat} -> Fin n -> Fin (su n)

mutual
  data Sig : Set1 where
    Epsilon : Sig
    _<_ : (S : Sig)(A : [| S |] -> Set) -> Sig

  [|_|] : Sig -> Set
  [| Epsilon |] = Unit
  [| S < A |] = Sigma [| S |] A

size : Sig -> Nat
size Epsilon = ze
size (S < A) = su (size S)

typeAt : (S : Sig) -> Fin (size S) -> Sigma1 Sig (\ S -> [| S |] -> Set)
typeAt Epsilon ()
typeAt (S < A) fze = ( S , A )
typeAt (S < A) (fsu y) = typeAt S y

fsts : (S : Sig)(i : Fin (size S)) -> [| S |] -> [| fst1 (typeAt S i) |]
fsts Epsilon () rec
fsts (S < A) fze rec = fst rec
fsts (S < A) (fsu y) rec = fsts S y (fst rec)

at : (S : Sig)(i : Fin (size S))(rec : [| S |]) -> snd1 (typeAt S i) (fsts S i rec)
at Epsilon () rec
at (S < A) fze rec = snd rec
at (S < A) (fsu y) rec = at S y (fst rec)

-- * Record definition combinators:

-- ** Non dependant case works:

fi : {a : Set1} -> (S : Sig) -> Set -> (Sig -> a) -> a
fi S A k = k (S < (\_ -> A))

begin : {a : Set1} -> (Sig -> a) -> a
begin k = k Epsilon

end : (Sig -> Sig)
end x = x

test : Sig
test = begin fi Test1 fi Test2 fi Test3 end

-- ** Dependant case doesn't:

fiD : {a : Sig -> Set1} -> (S : Sig) -> (A : ([| S |] -> Set)) -> ((S : Sig) -> a S) -> a (S < A)
fiD S A k = k (S < A)

beginD : {a : Sig -> Set1} -> ((S : Sig) -> a S) -> a Epsilon
beginD k = k Epsilon

endD : (Sig -> Sig)
endD x = x

test2 : Sig
test2 = beginD fiD ((\ _ -> Test1)) fiD {!!} fiD {!!} endD

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Choice
open import cohomology.FunctionOver

module cohomology.Theory where

-- [i] for the universe level of the group
record CohomologyTheory i : Type (lsucc i) where
  field
    C : ℤ → Ptd i → Group i

  CEl : ℤ → Ptd i → Type i
  CEl n X = Group.El (C n X)

  Cid : (n : ℤ) (X : Ptd i) → CEl n X
  Cid n X = GroupStructure.ident (Group.group-struct (C n X))

  ⊙CEl : ℤ → Ptd i → Ptd i
  ⊙CEl n X = ⊙[ CEl n X , Cid n X ]

  field
    CF-hom : (n : ℤ) {X Y : Ptd i} → fst (X ⊙→ Y) → (C n Y →ᴳ C n X)

    CF-ident : (n : ℤ) {X : Ptd i}
      → CF-hom n {X} {X} (⊙idf X) == idhom (C n X)
    CF-comp : (n : ℤ) {X Y Z : Ptd i} (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
      → CF-hom n (g ⊙∘ f) == CF-hom n f ∘ᴳ CF-hom n g

  CF : (n : ℤ) {X Y : Ptd i} → fst (X ⊙→ Y) → CEl n Y → CEl n X
  CF n f = GroupHom.f (CF-hom n f)

  field
    C-abelian : (n : ℤ) (X : Ptd i) → is-abelian (C n X)

    C-Susp : (n : ℤ) (X : Ptd i) → C (succ n) (⊙Susp X) ≃ᴳ C n X

    C-SuspF : (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y))
      → fst (C-Susp n X) ∘ᴳ CF-hom (succ n) (⊙susp-fmap f)
        == CF-hom n f ∘ᴳ fst (C-Susp n Y)

    C-exact : (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y))
      → is-exact (CF-hom n (⊙cfcod' f)) (CF-hom n f)

    C-additive : (n : ℤ) {I : Type i} (Z : I → Ptd i)
      → ((W : I → Type i) → has-choice 0 I W)
      → is-equiv (GroupHom.f (Πᴳ-hom-in (CF-hom n ∘ ⊙bwin {X = Z})))

  {- Alternate form of suspension axiom naturality -}
  C-Susp-↓ : (n : ℤ) {X Y : Ptd i} (f : fst (X ⊙→ Y))
    → CF-hom (succ n) (⊙susp-fmap f) == CF-hom n f
      [ uncurry _→ᴳ_ ↓ pair×= (group-ua (C-Susp n Y)) (group-ua (C-Susp n X)) ]
  C-Susp-↓ n f =
    hom-over-isos $ function-over-equivs _ _ $ ap GroupHom.f (C-SuspF n f)

record OrdinaryTheory i : Type (lsucc i) where
  constructor ordinary-theory
  field
    cohomology-theory : CohomologyTheory i
  open CohomologyTheory cohomology-theory public
  field
    C-dimension : (n : ℤ) → n ≠ 0 → C n (⊙Lift ⊙S⁰) == 0ᴳ

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.Types
open import LibraBFT.Abstract.Types.EpochConfig
open        WithAbsVote

-- This module defines abstract records (the initial or "genesis" record, blocks, and quorum
-- certificates), along with related definitions and properties.

module LibraBFT.Abstract.Records
    (UID    : Set)
    (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁)) -- Needed to prove ≟Block and ≈?QC
    (NodeId : Set)
    (𝓔 : EpochConfig UID NodeId)
    (𝓥 : VoteEvidence UID NodeId 𝓔)
    where
  open import LibraBFT.Abstract.Types UID NodeId
  open        EpochConfig 𝓔

  -- Abstract blocks do /not/ need to carry the state hash. Since the
  -- state hash of a concrete block is supposed to be hashed in the
  -- UID of an abstract one; the connection between states is implicit.
  -- Our proofs all work modulo injectivity of UID anyway.
  record Block  : Set where
    constructor Block∙new
    field
      bRound   : Round
      bId      : UID
      bPrevQC  : Maybe UID -- 'nothing' indicates it extends the genesis block.
  open Block public

  Block-η : {b b' : Block}
         → bRound b ≡ bRound b'
         → bId b ≡ bId b'
         → bPrevQC b ≡ bPrevQC b'
         → b ≡ b'
  Block-η refl refl refl = refl

  -- We define a Vote as an AbsVoteData applied
  -- to the correct parameters; This helps in defining
  -- and manipulating the 𝓥 vote evidence predicate.
  Vote : Set
  Vote = AbsVoteData UID NodeId 𝓔

  vRound      : Vote → Round
  vRound      = abs-vRound

  vMember     : Vote → EpochConfig.Member 𝓔
  vMember     = abs-vMember

  vBlockUID   : Vote → UID
  vBlockUID   = abs-vBlockUID

  Vote-η : {v v' : Vote}
         → vRound v ≡ vRound v' → vMember v ≡ vMember v'
         → vBlockUID v ≡ vBlockUID v'
         → v ≡ v'
  Vote-η refl refl refl = refl

  -- * Quorum Certificates
  --
  -- A valid quorum certificate contains at least 'QuorumSize ec'
  -- votes from different authors.
  record QC : Set where
   constructor QC∙new
   field
     qRound         : Round
     qCertBlockId   : UID -- this is the id for the block it certifies.
     qVotes         : List Vote
     -- The voters form a quorum
     qVotes-C1      : IsQuorum (List-map vMember qVotes)
     -- All votes are for the same blockId
     qVotes-C2      : All (λ v → vBlockUID v ≡ qCertBlockId) qVotes
     -- Likewise for rounds
     qVotes-C3      : All (λ v → vRound v ≡ qRound) qVotes
     -- And we have evidence for all votes
     qVotes-C4      : All 𝓥 qVotes
  open QC public

  ------------------------
  -- QC's make a setoid --
  ------------------------

  -- Two QC's are said to be equivalent if they have the same ID;
  -- that is, they certify the same block. As we are talking about
  -- /abstract/ QCs, we have proofs that both have at least QuorumSize
  -- votes for /the same block/!
  --
  -- It might be tempting to want qRound q₀ ≡ qRound q₁ in here,
  -- but the proof of ←-≈Rec in LibraBFT.Abstract.Records.Extends
  -- would be impossible.
  _≈QC_ : QC → QC → Set
  q₀ ≈QC q₁ = qCertBlockId q₀ ≡ qCertBlockId q₁

  _≈QC?_ : (q₀ q₁ : QC) → Dec (q₀ ≈QC q₁)
  q₀ ≈QC? q₁ with qCertBlockId q₀ ≟UID qCertBlockId q₁
  ...| yes refl = yes refl
  ...| no  neq  = no λ x → neq x

  ≈QC-refl : Reflexive _≈QC_
  ≈QC-refl = refl

  ≈QC-sym : Symmetric _≈QC_
  ≈QC-sym refl = refl

  ≈QC-trans : Transitive _≈QC_
  ≈QC-trans refl x = x

  QC-setoid : Setoid ℓ0 ℓ0
  QC-setoid = record
    { Carrier       = QC
    ; _≈_           = _≈QC_
    ; isEquivalence = record
        { refl  = λ {q}         → ≈QC-refl {q}
        ; sym   = λ {q} {u}     → ≈QC-sym {q} {u}
        ; trans = λ {q} {u} {l} → ≈QC-trans {q} {u} {l}
        }
    }

  -- Accessing common fields in different Records types is a nuissance; yet, Blocks,
  -- votes and QC's all have three important common fields: author, round and maybe the
  -- ID of a previous record.  Therefore we declare a type-class that provide "getters"
  -- for commonly used fields.
  record HasRound (A : Set) : Set where
    constructor is-librabft-record
    field
      getRound  : A → Round
  open HasRound {{...}} public

  instance
    block-is-record : HasRound Block
    block-is-record = is-librabft-record bRound

    vote-is-record : HasRound Vote
    vote-is-record = is-librabft-record vRound

    qc-is-record : HasRound QC
    qc-is-record = is-librabft-record qRound

  _≟Block_ : (b₀ b₁ : Block) → Dec (b₀ ≡ b₁)
  b₀ ≟Block b₁
     with bRound b₀ ≟ bRound b₁
  ...| no neq = no λ x → neq (cong bRound x)
  ...| yes r≡
     with (bId b₀) ≟UID (bId b₁)
  ...| no neq = no λ x → neq (cong bId x)
  ...| yes i≡
     with Maybe-≡-dec {A = UID} _≟UID_ (bPrevQC b₀) (bPrevQC b₁)
  ...| no neq = no λ x → neq (cong bPrevQC x)
  ...| yes p≡ = yes (Block-η r≡ i≡ p≡)

  qcVotes : QC → List Vote
  qcVotes = qVotes

  -- Now we can state whether an author has voted in a given QC.
  _∈QC_  : Member → QC → Set
  a ∈QC qc = Any (λ v → vMember v ≡ a) (qcVotes qc)

  ∈QC-Member : ∀{α}(q : QC)(v : α ∈QC q)
             → α ≡ vMember (List-lookup (qcVotes q) (Any-index v))
  ∈QC-Member {α} q v = aux v
    where
      aux : ∀{vs}(p : Any (λ v → vMember v ≡ α) vs)
          → α ≡ vMember (List-lookup vs (Any-index p))
      aux (here px) = sym px
      aux (there p) = aux p

  -- Gets the vote of a ∈QC
  -- TODO-1: make q explicit; a implicit
  ∈QC-Vote : {a : Member} (q : QC) → (a ∈QC q) → Vote
  ∈QC-Vote q a∈q = Any-lookup a∈q

  ∈QC-Vote-correct : ∀ q → {a : Member} → (p : a ∈QC q)
                   → (∈QC-Vote {a} q p) ∈ qcVotes q
  ∈QC-Vote-correct q a∈q = Any-lookup-correct a∈q

  -- Same vote in two QC's means the QCs are equivalent
  ∈QC-Vote-≈ : {v : Vote}{q q' : QC}
             → v ∈ qcVotes q → v ∈ qcVotes q'
             → q ≈QC q'
  ∈QC-Vote-≈ {v} {q} {q'} vq vq'
    = trans (sym (All-lookup (qVotes-C2 q)  vq))
                 (All-lookup (qVotes-C2 q') vq')

  -- A record is either one of the types introduced above or the initial/genesis record.
  data Record : Set where
    I :             Record
    B : Block     → Record
    Q : QC        → Record

  -- Records are equivalent if and only if they are either not
  -- QCs and propositionally equal or they are equivalent qcs.
  data _≈Rec_ : Record → Record → Set where
    eq-I :                        I    ≈Rec I
    eq-Q : ∀{q₀ q₁} → q₀ ≈QC q₁ → Q q₀ ≈Rec Q q₁
    eq-B : ∀{b₀ b₁} → b₀  ≡  b₁ → B b₀ ≈Rec B b₁

  ≈Rec-refl : Reflexive _≈Rec_
  ≈Rec-refl {I}   = eq-I
  ≈Rec-refl {B x} = eq-B refl
  ≈Rec-refl {Q x} = eq-Q (≈QC-refl {x})

  ≈Rec-sym : Symmetric _≈Rec_
  ≈Rec-sym {I}         eq-I       = eq-I
  ≈Rec-sym {B x}       (eq-B prf) = eq-B (sym prf)
  ≈Rec-sym {Q x} {Q y} (eq-Q prf) = eq-Q (≈QC-sym {x} {y} prf)

  ≈Rec-trans : Transitive _≈Rec_
  ≈Rec-trans {I}                eq-I      eq-I      = eq-I
  ≈Rec-trans {B x}             (eq-B p₀) (eq-B p₁) = eq-B (trans p₀ p₁)
  ≈Rec-trans {Q x} {Q y} {Q z} (eq-Q p₀) (eq-Q p₁) = eq-Q (≈QC-trans {x} {y} {z} p₀ p₁)

  Rec-setoid : Setoid ℓ0 ℓ0
  Rec-setoid = record
    { Carrier       = Record
    ; _≈_           = _≈Rec_
    ; isEquivalence = record
        { refl  = λ {q}         → ≈Rec-refl {q}
        ; sym   = λ {q} {u}     → ≈Rec-sym {q} {u}
        ; trans = λ {q} {u} {l} → ≈Rec-trans {q} {u} {l}
        }
    }

  -- Record unique ids carry whether the abstract id was assigned
  -- to a QC or a Block; this can be useful to avoid having to deal
  -- with 'blockId ≟ initialAgreedID' in order to decide whether
  -- a block is the genesis block or not.
  data TypedUID : Set where
    id-I   : TypedUID
    id-B∨Q : UID -> TypedUID

  id-I≢id-B∨Q : ∀{id} → id-I ≡ id-B∨Q id → ⊥
  id-I≢id-B∨Q ()

  id-B∨Q-inj : ∀{u₁ u₂} → id-B∨Q u₁ ≡ id-B∨Q u₂ → u₁ ≡ u₂
  id-B∨Q-inj refl = refl

  uid : Record → TypedUID
  uid I     = id-I
  uid (B b) = id-B∨Q (bId   b)
  uid (Q q) = id-B∨Q (qCertBlockId q)

  -- Each record has a round
  round : Record → Round
  round I     = 0
  round (B b) = getRound b
  round (Q q) = getRound q

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Rationals.HITQ.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Relation.Nullary

open import Cubical.HITs.Ints.QuoInt

open import Cubical.Data.Nat as ℕ hiding (_·_)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma

-- ℚ as a higher inductive type

data ℚ : Type₀ where
  con : (u : ℤ) (a : ℤ) → ¬ (a ≡ pos 0) → ℚ
  path : ∀ u a v b {p q} → (u · b) ≡ (v · a) → con u a p ≡ con v b q
  trunc : isSet ℚ

[_] : ℤ × ℕ₊₁ → ℚ
[ a , 1+ b ] = con a (pos (suc b)) (ℕ.snotz ∘ cong abs)

-- Natural number and negative integer literals for ℚ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℚ : HasFromNat ℚ
  fromNatℚ = record { Constraint = λ _ → Unit ; fromNat = λ n → [ pos n , 1 ] }

instance
  fromNegℚ : HasFromNeg ℚ
  fromNegℚ = record { Constraint = λ _ → Unit ; fromNeg = λ n → [ neg n , 1 ] }


text:
module FFI where

postulate
  IO : Set -> Set

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}

postulate
  return : {A : Set} -> A -> IO A
  _>>=_  : {A B : Set} -> IO A -> (A -> IO B) -> IO B

{-# COMPILED return (\_ -> return :: a -> IO a) #-}
{-# COMPILED _>>=_  (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () nothing #-}

main : IO Unit
main = return unit

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Numeral.CoordinateVector.Proofs where

import      Lvl
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs
import      Data.Either as Either
import      Functional as Fn
open import Function.Equals
open import Function.Names
open import Function.PointwiseStructure
open import Logic.Classical
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Numeral.CoordinateVector
open import Numeral.Finite
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Finite.Proofs
open import Numeral.Natural
import      Relator.Equals as Eq
open import Relator.Equals.Proofs.Equivalence
open import Structure.Setoid
open import Structure.Function.Multi
import      Structure.Function.Names as Names
open import Structure.Function
open import Structure.Operator.Field
open import Structure.Operator.Group
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator.Vector
open import Structure.Operator
open import Structure.Relator.Properties
open import Type
open import Syntax.Function
open import Syntax.Transitivity

-- Note: The structure stuff here is actually a specialization of Function.PointwiseStructure
module _ {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ where
  private variable _▫_ _▫₁_ _▫₂_ _+_ _⋅_ : T → T → T
  private variable f inv : T → T
  private variable id 𝟎ₛ 𝟏ₛ x init : T
  private variable d n : ℕ
  private variable i j k : 𝕟(n)
  private variable v : Vector(n)(T)

  instance
    -- A component-wise operator have a left identity of repeated elements when its underlying operator have a left identity.
    map₂-fill-identityₗ : ⦃ ident : Identityₗ(_▫_)(id) ⦄ → Identityₗ(map₂{d = n}(_▫_))(fill{d = n}(id))
    map₂-fill-identityₗ = pointwiseFunction-identityₗ

  instance
    -- A component-wise operator have a right identity of repeated elements when its underlying operator have a right identity.
    map₂-fill-identityᵣ : ⦃ ident : Identityᵣ(_▫_)(id) ⦄ → Identityᵣ(map₂{d = n}(_▫_))(fill{d = n}(id))
    map₂-fill-identityᵣ = pointwiseFunction-identityᵣ

  instance
    -- A component-wise operator have an identity of repeated elements when its underlying operator have an identity.
    map₂-fill-identity : ⦃ ident : Identity(_▫_)(id) ⦄ → Identity(map₂{d = n}(_▫_))(fill{d = n}(id))
    map₂-fill-identity = pointwiseFunction-identity

  instance
    map₂-map-inverseₗ : ⦃ ident : Identityₗ(_▫_)(id) ⦄ ⦃ inver : InverseFunctionₗ(_▫_) ⦃ [∃]-intro _ ⦄ (inv) ⦄ → InverseFunctionₗ(map₂{d = n}(_▫_)) ⦃ [∃]-intro _ ⦄ (map(inv))
    map₂-map-inverseₗ = pointwiseFunction-inverseFunctionₗ

  instance
    map₂-map-inverseᵣ : ⦃ ident : Identityᵣ(_▫_)(id) ⦄ ⦃ inver : InverseFunctionᵣ(_▫_) ⦃ [∃]-intro _ ⦄ (inv) ⦄ → InverseFunctionᵣ(map₂{d = n}(_▫_)) ⦃ [∃]-intro _ ⦄ (map(inv))
    map₂-map-inverseᵣ = pointwiseFunction-inverseFunctionᵣ

  instance
    map₂-map-inverse : ⦃ ident : Identity(_▫_)(id) ⦄ ⦃ inver : InverseFunction(_▫_) ⦃ [∃]-intro _ ⦄ (inv) ⦄ → InverseFunction(map₂{d = n}(_▫_)) ⦃ [∃]-intro _ ⦄ (map(inv))
    map₂-map-inverse = pointwiseFunction-inverseFunction

  instance
    -- A component-wise operator is commutative when its underlying operator is commutative.
    map₂-commutativity : ⦃ comm : Commutativity(_▫_) ⦄ → Commutativity(map₂{d = n}(_▫_))
    map₂-commutativity = pointwiseFunction-commutativity

  instance
    -- A component-wise operator is associative when its underlying operator is associative.
    map₂-associativity : ⦃ assoc : Associativity(_▫_) ⦄ → Associativity(map₂{d = n}(_▫_))
    map₂-associativity = pointwiseFunction-associativity

  instance
    -- A component-wise operator is left distributive over another component-wise operator when their underlying operators distribute.
    map₂-distributivityₗ : ⦃ distₗ : Distributivityₗ(_▫₁_)(_▫₂_) ⦄ → Distributivityₗ(map₂{d = n}(_▫₁_))(map₂{d = n}(_▫₂_))
    map₂-distributivityₗ = pointwiseFunction-distributivityₗ

  instance
    -- A component-wise operator is right distributive over another component-wise operator when their underlying operators distribute.
    map₂-distributivityᵣ : ⦃ distᵣ : Distributivityᵣ(_▫₁_)(_▫₂_) ⦄ → Distributivityᵣ(map₂{d = n}(_▫₁_))(map₂{d = n}(_▫₂_))
    map₂-distributivityᵣ = pointwiseFunction-distributivityᵣ

  instance
    map₂-preserves : Preserving₂(fill) (_▫_) (map₂{d = n}(_▫_))
    map₂-preserves = pointwiseFunction-const-preserves

  instance
    -- A component-wise function is a function when its underlying function is a function.
    map-function : ⦃ func : Function(f) ⦄ → Function(map{d = n}(f))
    map-function = pointwiseFunction-function

  instance
    -- A component-wise binary operator is a binary operator when its underlying binary operator is a binary operator.
    map₂-binaryOperator : ⦃ oper : BinaryOperator(_▫_) ⦄ → BinaryOperator(map₂{d = n}(_▫_))
    map₂-binaryOperator = pointwiseFunction-binaryOperator

  instance
    -- A component-wise operator is a monoid when its underlying operator is a monoid.
    map₂-monoid : ⦃ monoid : Monoid(_▫_) ⦄ → Monoid(map₂{d = n}(_▫_))
    map₂-monoid = pointwiseFunction-monoid

  instance
    -- A component-wise operator is a group when its underlying operator is a group.
    map₂-group : ⦃ group : Group(_▫_) ⦄ → Group(map₂{d = n}(_▫_))
    map₂-group = pointwiseFunction-group

  instance
    -- A component-wise operator is a commutative group when its underlying operator is a commutative group.
    map₂-commutativeGroup : ⦃ commutativeGroup : CommutativeGroup(_▫_) ⦄ → CommutativeGroup(map₂{d = n}(_▫_))
    map₂-commutativeGroup = pointwiseFunction-commutativeGroup

  {- TODO: Is this even possible?
  instance
    -- Note: The reason for `d = 𝐒(n)` is so that one cannot shrink a field to the "trivial field" in this way (which is not a field).
    map₂-field : ⦃ field-structure : Field(_+_)(_⋅_) ⦄ → Field(map₂{d = 𝐒(n)}(_+_))(map₂{d = 𝐒(n)}(_⋅_))
    Field.[+]-commutative-group map₂-field = map₂-commutativeGroup
    Field.[⋅]-monoid map₂-field = map₂-monoid
    Field.⅟ (map₂-field ⦃ f ⦄) v ⦃ Field.intro nonzero ⦄ = {!!} -- map (x ↦ Field.⅟ f x ⦃ Field.intro (p ↦ nonzero (intro {!!})) ⦄) v
    Field.[⋅]-inverseₗ map₂-field = {!!}
    Field.[⋅]-inverseᵣ map₂-field = {!!}
    Field.distinct-identities (map₂-field ⦃ f ⦄) p = Field.distinct-identities f (_⊜_.proof p {𝟎})
  -}

  instance
    -- Component-wise operators constructs a vector space from a field when using the fields as scalars and coordinate vectors as vectors.
    CoordinateVector-vectorSpace : ⦃ field-structure : Field(_+_)(_⋅_) ⦄ → VectorSpace(map₂{d = n}(_+_)) (s ↦ map{d = n}(s ⋅_)) (_+_) (_⋅_)
    CoordinateVector-vectorSpace ⦃ field-structure ⦄ = pointwiseFunction-vectorSpace field-structure

  indexProject-values : ∀{true false : T} → (proj(indexProject i true false) j ≡ true) ∨ (proj(indexProject i true false) j ≡ false)
  indexProject-values {𝐒 n}{i = i}{j = j} with (i ≡? j)
  ... | 𝑇 = [∨]-introₗ (reflexivity(_≡_))
  ... | 𝐹 = [∨]-introᵣ (reflexivity(_≡_))

  indexProject-true  : ∀{true false : T} → (i Eq.≡ j) ∨ (false ≡ true) ↔ (proj(indexProject i true false) j ≡ true)
  indexProject-true {n}{i = i}{j = j} {true = true}{false = false} =
    [∨]-mapₗ-[↔] [≡][≡?]-equivalence ⦗ [↔]-transitivity ⦘ᵣ
    [↔]-intro
      (l{n}{i}{j})
      ([↔]-to-[←] [→ₗ][∨][∧]-preserving ([∧]-intro (r₁{n}{i}{j}) (r₂{n}{i}{j})))
    where
      l : ∀{n}{i j : 𝕟(n)} → IsTrue(i ≡? j) ∨ (false ≡ true) ← (proj(indexProject i true false) j ≡ true)
      l {𝐒 n} {i = i} {j = j} p with (i ≡? j)
      ... | 𝑇 = [∨]-introₗ [⊤]-intro
      ... | 𝐹 = [∨]-introᵣ p

      r₁ : ∀{n}{i j : 𝕟(n)} → IsTrue(i ≡? j) → (proj(indexProject i true false) j ≡ true)
      r₁ {𝐒 n} {i = i}{j = j} p with 𝑇 ← (i ≡? j) = reflexivity(_≡_)

      r₂ : ∀{n}{i j : 𝕟(n)} → (false ≡ true) → (proj(indexProject i true false) j ≡ true)
      r₂ {𝐒 n} {i = i}{j = j} p with (i ≡? j)
      ... | 𝑇 = reflexivity(_≡_)
      ... | 𝐹 = p

  indexProject-false : ∀{true false : T} → ((i Eq.≢ j) ∨ (false ≡ true)) ↔ (proj(indexProject i true false) j ≡ false)
  indexProject-false {n}{i = i}{j = j} {true = true}{false = false} =
    [∨]-mapₗ-[↔] ([↔]-transitivity ([¬]-unaryOperator [≡][≡?]-equivalence) ([↔]-symmetry false-true-opposites)) ⦗ [↔]-transitivity ⦘ᵣ
    [↔]-intro
      (l{n}{i}{j})
      ([↔]-to-[←] [→ₗ][∨][∧]-preserving ([∧]-intro (r₁{n}{i}{j}) (r₂{n}{i}{j})))
    where
      l : ∀{n}{i j : 𝕟(n)} → (IsFalse(i ≡? j) ∨ (false ≡ true)) ← (proj(indexProject i true false) j ≡ false)
      l {n} {i} {j} p with (i ≡? j)
      ... | 𝑇 = [∨]-introᵣ (symmetry(_≡_) p)
      ... | 𝐹 = [∨]-introₗ [⊤]-intro

      r₁ : ∀{n}{i j : 𝕟(n)} → IsFalse(i ≡? j) → (proj(indexProject i true false) j ≡ false)
      r₁ {𝐒 n} {i = i}{j = j} p with (i ≡? j)
      ... | 𝑇 = [⊥]-elim p
      ... | 𝐹 = reflexivity(_≡_)

      r₂ : ∀{n}{i j : 𝕟(n)} → (false ≡ true) → (proj(indexProject i true false) j ≡ false)
      r₂ {𝐒 n} {i = i}{j = j} p with (i ≡? j)
      ... | 𝑇 = symmetry(_≡_) p
      ... | 𝐹 = reflexivity(_≡_)

  module _
    ⦃ ident : Identityₗ(_⋅_)(𝟏ₛ) ⦄
    ⦃ absor : Absorberₗ(_⋅_)(𝟎ₛ) ⦄
    where
    map₂-indexProject-identityₗ : map₂(_⋅_) (indexProject i 𝟏ₛ 𝟎ₛ) v ≡ indexProject i (v(i)) 𝟎ₛ
    _⊜_.proof (map₂-indexProject-identityₗ {i = i}{v = v}) {x} with (i ≡? x) | [↔]-to-[←] ([≡][≡?]-equivalence {i = i}{j = x})
    ... | 𝑇 | p = identityₗ(_⋅_)(𝟏ₛ) 🝖 congruence₁ ⦃ [≡]-equiv ⦄ (v) ⦃ [≡]-to-function ⦄ (symmetry(Eq._≡_) (p([⊤]-intro)))
    ... | 𝐹 | _ = absorberₗ(_⋅_)(𝟎ₛ)

  module _
    ⦃ ident : Identityᵣ(_⋅_)(𝟏ₛ) ⦄
    ⦃ absor : Absorberᵣ(_⋅_)(𝟎ₛ) ⦄
    where
    map₂-indexProject-identityᵣ : map₂(_⋅_) v (indexProject i 𝟏ₛ 𝟎ₛ) ≡ indexProject i (v(i)) 𝟎ₛ
    _⊜_.proof (map₂-indexProject-identityᵣ {v = v}{i = i}) {x} with (i ≡? x) | [↔]-to-[←] ([≡][≡?]-equivalence {i = i}{j = x})
    ... | 𝑇 | p = identityᵣ(_⋅_)(𝟏ₛ) 🝖 congruence₁ ⦃ [≡]-equiv ⦄ (v) ⦃ [≡]-to-function ⦄ (symmetry(Eq._≡_) (p([⊤]-intro)))
    ... | 𝐹 | _ = absorberᵣ(_⋅_)(𝟎ₛ)

  tail-function : Function(tail{d = 𝐒(d)}{T = T})
  Function.congruence(tail-function{d = d}) (intro xy) = intro xy

  instance
    foldᵣ-function : ∀{ℓᵣ ℓₑᵣ}{R : Type{ℓᵣ}} ⦃ equiv-R : Equiv{ℓₑᵣ}(R)⦄ {f : T → R → R}{init} → ⦃ oper : BinaryOperator(f) ⦄ → Function(foldᵣ{d = d} f init)
    foldᵣ-function {d} {f = f}{init = init} = intro(p{d = d}) where
      p : ∀{d} → Names.Congruence₁(foldᵣ{d = d} f init)
      p {𝟎}       _  = reflexivity(_≡_)
      p {𝐒(𝟎)}    xy = congruence₂ₗ(f)(_) (_⊜_.proof xy)
      p {𝐒(𝐒(d))} xy = congruence₂(f) (_⊜_.proof xy) (p {𝐒(d)} (congruence₁(tail) ⦃ tail-function ⦄ xy))

  -- TODO: Generalize Numeral.Natural.Oper.Summation for these kinds of proofs
  {-
  module _
    ⦃ oper : BinaryOperator(_▫_) ⦄
    ⦃ ident : Identityᵣ(_▫_)(id) ⦄
    ( neq : (id ≢ x) )
    where
    foldᵣ-indexProject-identityᵣ : foldᵣ(_▫_) init (indexProject i x id) ≡ x ▫ init
    foldᵣ-indexProject-identityᵣ {init}{𝐒(𝟎)}    {i = 𝟎}   = reflexivity(_≡_)
    foldᵣ-indexProject-identityᵣ {init}{𝐒(𝐒(n))} {i = 𝟎}   =
      foldᵣ{d = 𝐒(𝐒(n))}(_▫_) init (indexProject 𝟎 x id)                                                🝖[ _≡_ ]-[]
      proj(indexProject{d = 𝐒(𝐒(n))} 𝟎 x id)(𝟎) ▫ foldᵣ{d = 𝐒(n)}(_▫_) init (tail(indexProject 𝟎 x id)) 🝖[ _≡_ ]-[]
      x ▫ foldᵣ{d = 𝐒(n)}(_▫_) init (tail(indexProject 𝟎 x id))                                         🝖[ _≡_ ]-[ {!!} ]
      x ▫ init                                                                                🝖-end
      {-foldᵣ(_▫_) id (indexProject 𝟎 x id)                                        🝖[ _≡_ ]-[ {!!} ]
      proj(indexProject 𝟎 x id)(𝟎) ▫ (foldᵣ(_▫_) id (tail(indexProject 𝟎 x id))) 🝖[ _≡_ ]-[ {!!} ]
      id ▫ (foldᵣ(_▫_) id (tail(indexProject 𝟎 x id)))                           🝖[ _≡_ ]-[ {!!} ]
      foldᵣ(_▫_) id (tail(indexProject 𝟎 x id))                                  🝖[ _≡_ ]-[ {!!} ]
      x                                                                          🝖-end-}
    foldᵣ-indexProject-identityᵣ {init}{𝐒(𝐒(n))} {i = 𝐒 i} = {!!}
  -}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda