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

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

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

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

open import Cubical.Relation.Binary

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

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

open import Cubical.DStructures.Meta.Isomorphism
open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.Action
open import Cubical.DStructures.Structures.XModule
open import Cubical.DStructures.Structures.ReflGraph
open import Cubical.DStructures.Structures.PeifferGraph
open import Cubical.DStructures.Equivalences.GroupSplitEpiAction
open import Cubical.DStructures.Equivalences.PreXModReflGraph

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓC ℓ≅C ℓ≅ᴰ ℓ≅ᴰ' ℓ≅B' : Level

open Kernel
open GroupHom -- such .fun!
open GroupLemmas
open MorphismLemmas
open ActionLemmas

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

    ℱ = Iso-PreXModule-ReflGraph ℓ ℓℓ'
    F = Iso.fun ℱ

    𝒮ᴰ-S2G = 𝒮ᴰ-ReflGraph\Peiffer

    𝒮ᴰ-♭PIso-XModule-Strict2Group : 𝒮ᴰ-♭PIso F (𝒮ᴰ-XModule ℓ ℓℓ') (𝒮ᴰ-S2G ℓ ℓℓ')
    RelIso.fun (𝒮ᴰ-♭PIso-XModule-Strict2Group (((((G₀' , H) , _α_) , isAct) , φ) , isEqui)) isPeif a b = q
      where
        -- G₀ = G₀', but the former is introduced in ReflGraphNotation as well
        open GroupNotationᴴ H
        -- open GroupNotation₀ G₀
        f = GroupHom.fun φ
        A = groupaction _α_ isAct
        open ActionNotationα A using (α-assoc ; α-hom)

        SG = F (((((G₀' , H) , _α_) , isAct) , φ) , isEqui)
        -- H⋊G : Group {ℓℓ'}
        H⋊G = snd (fst (fst (fst (fst SG))))
        -- open GroupNotation₁ H⋊G
        open ReflGraphNotation SG
        -- σ : GroupHom H⋊G G₀
        -- ι : GroupHom G₀ H⋊G
        -- τ : GroupHom H⋊G G₀
        u = fst a
        v = snd a
        x = fst b
        y = snd b
        abstract
          -- alright folks, let's do some simple arithmetic with a `twist`, that is Peiffer identities and equivariance
          r = ((0ᴴ +ᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))) +ᴴ (((y +₀ (v +₀ (-₀ (f u +₀ v)))) +₀ ((-₀ y) +₀ y)) α 0ᴴ)
                ≡⟨ cong (((0ᴴ +ᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))) +ᴴ_)
                        (actOnUnit A ((y +₀ (v +₀ (-₀ (f u +₀ v)))) +₀ ((-₀ y) +₀ y))) ⟩
              ((0ᴴ +ᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))) +ᴴ 0ᴴ
                ≡⟨ rIdᴴ ((0ᴴ +ᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))) ⟩
              (0ᴴ +ᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))
                ≡⟨ cong (_+ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x))))
                        (lIdᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) ⟩
              (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))
                ≡⟨ cong (λ z → (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (z +ᴴ ((-₀ y) α x))))
                        (actOn-Unit A (-₀ y)) ⟩
              (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (0ᴴ +ᴴ ((-₀ y) α x)))
                ≡⟨ cong (λ z → (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α z))
                        (lIdᴴ ((-₀ y) α x)) ⟩
              (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x))
                ≡⟨ cong (λ z → (y α (u +ᴴ (v α z))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x)))
                        (actOn-Unit A (-₀ ((f u) +₀ v))) ⟩
              (y α (u +ᴴ (v α 0ᴴ))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x))
                ≡⟨ cong (λ z → (y α (u +ᴴ z)) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x)))
                        (actOnUnit A v) ⟩
              (y α (u +ᴴ 0ᴴ)) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x))
                ≡⟨ cong (λ z → (y α z) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x)))
                        (rIdᴴ u) ⟩
              (y α u) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α ((-₀ y) α x))
                ≡⟨ cong (λ z → (y α u) +ᴴ ((y +₀ (v +₀ z)) α ((-₀ y) α x)))
                        (invDistr G₀ (f u) v) ⟩
              (y α u) +ᴴ ((y +₀ (v +₀ ((-₀ v) +₀ (-₀ (f u))))) α ((-₀ y) α x))
                ≡⟨ cong (λ z → (y α u) +ᴴ ((y +₀ z) α ((-₀ y) α x)))
                        (assoc-rCancel G₀ v (-₀ f u)) ⟩
              (y α u) +ᴴ ((y +₀ (-₀ (f u))) α ((-₀ y) α x))
                ≡⟨ cong ((y α u) +ᴴ_)
                        (sym (α-assoc (y +₀ (-₀ f u)) (-₀ y) x)) ⟩
              (y α u) +ᴴ (((y +₀ (-₀ (f u))) +₀ (-₀ y)) α x)
                ≡⟨ cong (λ z → (y α u) +ᴴ (((y +₀ z) +₀ (-₀ y)) α x))
                        (sym (mapInv φ u)) ⟩
              (y α u) +ᴴ (((y +₀ (f (-ᴴ u))) -₀ y) α x)
              -- apply equivariance here
                ≡⟨ cong (λ z → (y α u) +ᴴ (z α x))
                        (sym (isEqui y (-ᴴ u))) ⟩
              (y α u) +ᴴ ((f (y α (-ᴴ u))) α x)
              -- apply peiffer condition here
                ≡⟨ cong ((y α u) +ᴴ_)
                        (isPeif (y α (-ᴴ u)) x) ⟩
              (y α u) +ᴴ (((y α (-ᴴ u)) +ᴴ x) +ᴴ (-ᴴ (y α (-ᴴ u))))
                ≡⟨ cong (λ z → (y α u) +ᴴ ((z +ᴴ x) +ᴴ (-ᴴ z)))
                        (actOn- A y u) ⟩
              (y α u) +ᴴ (((-ᴴ (y α u)) +ᴴ x) +ᴴ (-ᴴ (-ᴴ (y α u))))
                ≡⟨ cong (λ z → (y α u) +ᴴ (((-ᴴ (y α u)) +ᴴ x) +ᴴ z))
                        (invInvo H (y α u)) ⟩
              (y α u) +ᴴ (((-ᴴ (y α u)) +ᴴ x) +ᴴ (y α u))
                ≡⟨ assoc-assoc H (y α u) (-ᴴ (y α u)) x (y α u) ⟩
              (((y α u) +ᴴ (-ᴴ (y α u))) +ᴴ x) +ᴴ (y α u)
                ≡⟨ cong (_+ᴴ (y α u))
                        (rCancel-lId H (y α u) x) ⟩
              x +ᴴ (y α u) ∎

          r' = ((y +₀ (v +₀ (-₀ (f u +₀ v)))) +₀ ((-₀ y) +₀ y)) +₀ (f u +₀ v)
                 ≡⟨ cong (_+₀ (f u +₀ v))
                         (lCancel-rId G₀ (y +₀ (v +₀ (-₀ (f u +₀ v)))) y) ⟩
               (y +₀ (v +₀ (-₀ (f u +₀ v)))) +₀ (f u +₀ v)
                 ≡⟨ cong (λ z → (y +₀ (v +₀ z)) +₀ (f u +₀ v))
                         (invDistr G₀ (f u) v) ⟩
               (y +₀ (v +₀ ((-₀ v) +₀ (-₀ f u)))) +₀ (f u +₀ v)
                 ≡⟨ cong (λ z → (y +₀ z) +₀ (f u +₀ v))
                         (assoc-rCancel G₀ v (-₀ f u)) ⟩
               (y +₀ (-₀ f u)) +₀ (f u +₀ v)
                 ≡⟨ assoc⁻-assocr-lCancel-lId G₀ y (f u) v ⟩
               y +₀ v ∎

          q = ((is b +₁ (a +₁ -it a)) +₁ (-is b +₁ b)) +₁ it a
                ≡⟨ refl ⟩
              ((0ᴴ +ᴴ (y α (u +ᴴ (v α ((-₀ ((f u) +₀ v)) α (-ᴴ 0ᴴ)))))) +ᴴ ((y +₀ (v +₀ (-₀ (f u +₀ v)))) α (((-₀ y) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ y) α x)))) +ᴴ (((y +₀ (v +₀ (-₀ (f u +₀ v)))) +₀ ((-₀ y) +₀ y)) α 0ᴴ)
              , ((y +₀ (v +₀ (-₀ (f u +₀ v)))) +₀ ((-₀ y) +₀ y)) +₀ (f u +₀ v)
                ≡⟨ ΣPathP (r , r') ⟩
              x +ᴴ (y α u) , y +₀ v
                ≡⟨ refl ⟩
              b +₁ a ∎
    RelIso.inv (𝒮ᴰ-♭PIso-XModule-Strict2Group (((((G₀' , H) , _α_) , isAct) , φ) , isEqui)) ♭isPeif h h' = q
      where
        open GroupNotationᴴ H
        f = GroupHom.fun φ
        A = groupaction _α_ isAct
        open ActionNotationα A using (α-assoc ; α-hom ; α-id)

        SG = F (((((G₀' , H) , _α_) , isAct) , φ) , isEqui)
        -- H⋊G : Group {ℓℓ'}
        H⋊G = snd (fst (fst (fst (fst SG))))
        -- open GroupNotation₁ H⋊G
        open ReflGraphNotation SG
        -- σ : GroupHom H⋊G G₀
        -- ι : GroupHom G₀ H⋊G
        -- τ : GroupHom H⋊G G₀
        -h = -ᴴ h
        abstract
          r₁ = ((0ᴴ +ᴴ (0₀ α (-h +ᴴ (0₀ α ((-₀ ((f -h) +₀ 0₀)) α (-ᴴ 0ᴴ)))))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))) +ᴴ (((0₀ +₀ (0₀ +₀ (-₀ ((f -h) +₀ 0₀)))) +₀ ((-₀ 0₀) +₀ 0₀)) α 0ᴴ)
                 ≡⟨ cong fst
                         (♭isPeif (-h , 0₀) (h' , 0₀)) ⟩
               h' +ᴴ (0₀ α -h)
                 ≡⟨ cong (h' +ᴴ_)
                         (α-id -h) ⟩
               h' +ᴴ -h ∎

          r₂ = ((0ᴴ +ᴴ (0₀ α (-h +ᴴ (0₀ α ((-₀ ((f -h) +₀ 0₀)) α (-ᴴ 0ᴴ)))))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                  +ᴴ (((0₀ +₀ (0₀ +₀ (-₀ ((f -h) +₀ 0₀)))) +₀ ((-₀ 0₀) +₀ 0₀)) α 0ᴴ)
                  ≡⟨ cong (((0ᴴ +ᴴ (0₀ α (-h +ᴴ (0₀ α ((-₀ ((f -h) +₀ 0₀)) α (-ᴴ 0ᴴ)))))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))) +ᴴ_)
                          (actOnUnit A (((0₀ +₀ (0₀ +₀ (-₀ ((f -h) +₀ 0₀)))) +₀ ((-₀ 0₀) +₀ 0₀))))
                     ∙ rIdᴴ _ ⟩
                (0ᴴ +ᴴ (0₀ α (-h +ᴴ (0₀ α ((-₀ ((f -h) +₀ 0₀)) α (-ᴴ 0ᴴ)))))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → (0ᴴ +ᴴ (0₀ α (-h +ᴴ (0₀ α z)))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                          (actOn-Unit A (-₀ ((f -h) +₀ 0₀))) ⟩
                (0ᴴ +ᴴ (0₀ α (-h +ᴴ (0₀ α 0ᴴ)))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → (0ᴴ +ᴴ (0₀ α (-h +ᴴ z))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                          (actOnUnit A 0₀) ⟩
                (0ᴴ +ᴴ (0₀ α (-h +ᴴ 0ᴴ))) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → (0ᴴ +ᴴ (0₀ α z)) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                          (rIdᴴ -h) ⟩
                (0ᴴ +ᴴ (0₀ α -h)) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → (0ᴴ +ᴴ z) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                          (α-id -h) ⟩
                (0ᴴ +ᴴ -h) +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (_+ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                          (lIdᴴ -h) ⟩
                -h +ᴴ ((0₀ +₀ (0₀ +₀ (-₀ (f -h +₀ 0₀)))) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → -h +ᴴ (z α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h'))))
                          (lId-lId G₀ (-₀ (f -h +₀ 0₀))) ⟩
                -h +ᴴ ((-₀ (f -h +₀ 0₀)) α (((-₀ 0₀) α (-ᴴ 0ᴴ)) +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → -h +ᴴ ((-₀ (f -h +₀ 0₀)) α (z +ᴴ ((-₀ 0₀) α h'))))
                          (actOn-Unit A (-₀ 0₀)) ⟩
                -h +ᴴ ((-₀ (f -h +₀ 0₀)) α (0ᴴ +ᴴ ((-₀ 0₀) α h')))
                  ≡⟨ cong (λ z → -h +ᴴ ((-₀ (f -h +₀ 0₀)) α z))
                          (lIdᴴ ((-₀ 0₀) α h')) ⟩
                -h +ᴴ ((-₀ (f -h +₀ 0₀)) α ((-₀ 0₀) α h'))
                  ≡⟨ cong (λ z → -h +ᴴ ((-₀ (f -h +₀ 0₀)) α z))
                          (-idAct A h') ⟩
                -h +ᴴ ((-₀ (f -h +₀ 0₀)) α h')
                  ≡⟨ cong (λ z → -h +ᴴ ((-₀ z) α h'))
                          (rId₀ (f -h)) ⟩
                -h +ᴴ ((-₀ (f -h)) α h')
                  ≡⟨ cong (λ z → -h +ᴴ (z α h'))
                          (cong -₀_ (mapInv φ h) ∙ invInvo G₀ (f h)) ⟩
                -h +ᴴ (f h α h') ∎

          q = f h α h'
                ≡⟨ sym (lIdᴴ (f h α h'))
                   ∙∙ sym (cong (_+ᴴ (f h α h')) (rCancelᴴ h))
                   ∙∙ sym (assocᴴ h -h (f h α h')) ⟩
              h +ᴴ (-h +ᴴ (f h α h'))
                ≡⟨ cong (h +ᴴ_)
                        (sym r₂ ∙ r₁) ⟩
              h +ᴴ (h' +ᴴ -h)
                ≡⟨ assocᴴ h h' -h ⟩
              (h +ᴴ h') +ᴴ (-ᴴ h) ∎

    RelIso.leftInv (𝒮ᴰ-♭PIso-XModule-Strict2Group _) _ = tt
    RelIso.rightInv (𝒮ᴰ-♭PIso-XModule-Strict2Group _) _ = tt

  Iso-XModule-PeifferGraph : Iso (XModule ℓ ℓℓ') (PeifferGraph ℓ ℓℓ')
  Iso-XModule-PeifferGraph = 𝒮ᴰ-♭PIso-Over→TotalIso ℱ (𝒮ᴰ-XModule ℓ ℓℓ') (𝒮ᴰ-S2G ℓ ℓℓ') 𝒮ᴰ-♭PIso-XModule-Strict2Group

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --universe-polymorphism #-}
open import Level
open import Categories.Category
module Categories.Power.NaturalTransformation {o ℓ e : Level} (C : Category o ℓ e) where

open import Function using () renaming (_∘_ to _∙_)
open import Data.Fin using (Fin; inject+; raise)
open import Data.Sum using (_⊎_; [_,_]′; inj₁; inj₂)
open import Data.Product using (_,_)

import Categories.Power
module Pow = Categories.Power C
open Pow public
open import Categories.Bifunctor using (Bifunctor)

open import Categories.Bifunctor.NaturalTransformation renaming (id to idⁿ; _≡_ to _≡ⁿ_)
open import Categories.Functor using (module Functor) renaming (_∘_ to _∘F_)

flattenPⁿ : ∀ {D : Category o ℓ e} {n m} {F G : Powerfunctor′ D (Fin n ⊎ Fin m)} (η : NaturalTransformation F G) → NaturalTransformation (flattenP F) (flattenP G)
flattenPⁿ {n = n} {m} η = record
  { η = λ Xs → η.η (Xs ∙ pack)
  ; commute = λ fs → η.commute (fs ∙ pack)
  }
  where
  private module η = NaturalTransformation η
  pack = [ inject+ m , raise n ]′

reduceN′ : ∀ (H : Bifunctor C C C) {I} {F F′ : Powerendo′ I} (φ : NaturalTransformation F F′) {J} {G G′ : Powerendo′ J} (γ : NaturalTransformation G G′) → NaturalTransformation (reduce′ H F G) (reduce′ H F′ G′)
reduceN′ H {I} {F} {F′} φ {J} {G} {G′} γ = record
  { η = my-η
  ; commute = λ {Xs Ys} → my-commute Xs Ys
  }
  where
  module F = Functor F
  module F′ = Functor F′
  module G = Functor G
  module G′ = Functor G′
  module φ = NaturalTransformation φ
  module γ = NaturalTransformation γ
  module H = Functor H
  module L = Functor (reduce′ H F G)
  module R = Functor (reduce′ H F′ G′)
  my-η : ∀ Xs → C [ L.F₀ Xs , R.F₀ Xs ]
  my-η Xs = H.F₁ ((φ.η (Xs ∙ inj₁)) , (γ.η (Xs ∙ inj₂)))
  .my-commute : ∀ Xs Ys fs → C.CommutativeSquare (L.F₁ fs) (my-η Xs) (my-η Ys) (R.F₁ fs)
  my-commute Xs Ys fs = begin
      my-η Ys ∘ L.F₁ fs
    ↑⟨ H.homomorphism ⟩
      H.F₁ ((φ.η (Ys ∙ inj₁) ∘ F.F₁ (fs ∙ inj₁)) , (γ.η (Ys ∙ inj₂) ∘ G.F₁ (fs ∙ inj₂)))
    ↓⟨ H.F-resp-≡ ((φ.commute (fs ∙ inj₁)) , (γ.commute (fs ∙ inj₂))) ⟩
      H.F₁ ((F′.F₁ (fs ∙ inj₁) ∘ φ.η (Xs ∙ inj₁)) , (G′.F₁ (fs ∙ inj₂) ∘ γ.η (Xs ∙ inj₂)))
    ↓⟨ H.homomorphism ⟩
      R.F₁ fs ∘ my-η Xs
    ∎
    where
    open C using (_∘_; _≡_)
    open C.HomReasoning

reduceN : ∀ (H : Bifunctor C C C) {n} {F F′ : Powerendo n} (φ : NaturalTransformation F F′) {m} {G G′ : Powerendo m} (γ : NaturalTransformation G G′) → NaturalTransformation (reduce H F G) (reduce H F′ G′)
reduceN  H {n}  {F = f} {f′} F {m} {g} {g′} G = flattenPⁿ  {F = a} {G = b}  (reduceN′ H F G)
  where
    a : Categories.Bifunctor.Functor     (Categories.Power.Exp C (Fin n ⊎ Fin m)) C
    a = reduce′ H f g
    b : Categories.Bifunctor.Functor     (Categories.Power.Exp C (Fin n ⊎ Fin m)) C
    b = reduce′ H f′ g′

overlapN : ∀ (H : Bifunctor C C C) {n} {F F′ : Powerendo n} (φ : NaturalTransformation F F′) {G G′ : Powerendo n} (γ : NaturalTransformation G G′) → NaturalTransformation (overlaps {C} {C} H F G) (overlaps {C} {C} H F′ G′)
overlapN H F G = overlapN-× {D₁ = C} {D₂ = C} H F G

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Erased-cubical-Pattern-matching.Cubical

-- The following definition should be rejected. Matching on a
-- non-erased constructor that is treated as erased because it was
-- defined in a module that uses --cubical should not on its own make
-- it possible to use erased definitions in the right-hand side.

f : D → D
f c = c

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-09-01
-- This module exports a module M

module Imports.Module where

module M where


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

module Avionics.Probability where

open import Data.Nat using (ℕ; zero; suc)
open import Relation.Unary using (_∈_)

open import Avionics.Real using (
    ℝ; _+_; _-_; _*_; _÷_; _^_; √_; 1/_; _^2;
    -1/2; π; e; 2ℝ;
    ⟨0,∞⟩; [0,∞⟩; [0,1])

--postulate
--  Vec : Set → ℕ → Set
--  Mat : Set → ℕ → ℕ → Set

record Dist (Input : Set) : Set where
  field
    pdf : Input → ℝ
    cdf : Input → ℝ
    pdf→[0,∞⟩ : ∀ x → pdf x ∈ [0,∞⟩
    cdf→[0,1] : ∀ x → cdf x ∈ [0,1]
    --∫pdf≡cdf : ∫ pdf ≡ cdf
    --∫pdf[-∞,∞]≡1ℝ : ∫ pdf [ -∞ , ∞ ] ≡ 1ℝ

record NormalDist : Set where
  constructor ND
  field
    μ : ℝ
    σ : ℝ

  dist : Dist ℝ
  dist = record
    {
      pdf = pdf
    ; cdf = ?
    ; pdf→[0,∞⟩ = ?
    ; cdf→[0,1] = ?
    }
    where
      √2π = (√ (2ℝ * π))
      1/⟨σ√2π⟩ = (1/ (σ * √2π))

      pdf : ℝ → ℝ
      pdf x = 1/⟨σ√2π⟩ * e ^ (-1/2 * (⟨x-μ⟩÷σ ^2))
        where
          ⟨x-μ⟩÷σ = ((x - μ) ÷ σ)

--MultiNormal : ∀ {n : ℕ} → Vec ℝ n → Mat ℝ n n → Dist (Vec ℝ n)
--MultiNormal {n} means cov = record
--  {
--    pdf = ?
--  ; cdf = ?
--  }

--Things to prove using this approach
--_ : ∀ (mean1 std1 mean2 std2 x)
--  → Dist.pdf (Normal mean1 std1) x + Dist.pdf (Normal mean2 std2) x ≡ Dist.pdf (Normal (mean1 + mean2) (...))

max_stars_repo_name: RPI-WCL/safety-envelopes-sentinels

max_issues_repo_name: RPI-WCL/safety-envelopes-sentinels

max_forks_repo_name: RPI-WCL/safety-envelopes-sentinels


text:
module Isos.TreeLike where

open import Isos.Isomorphism

open import Trees
open import Tuples
open import Equality

open import Data.Product
open import Data.Unit

------------------------------------------------------------------------
-- internal stuffs

private

  pattern ∅ = Empty tt
  ∅′ : BareBinTree
  ∅′ = Empty tt
  _,,_ : BareBinTree → BareBinTree → BareBinTree
  _,,_ = Node tt
  infixl 4 _,,_
  pattern [_,_] a b = Node tt a b

  tree⁷->tree : BareBinTree ⁷ → BareBinTree
  tree⁷->tree (∅ , ∅ , ∅ , ∅ , ∅ , ∅ , [ [ [ [ a , b ] , c ] , d ] , e ])
              = ∅′ ,, a ,, b ,, c ,, d ,, e
  tree⁷->tree (∅  , ∅  , ∅  , ∅  , ∅  , ∅  , a) = a
  tree⁷->tree (∅  , ∅  , ∅  , ∅  , ∅  , t₅ , t₆)
              = t₅ ,, t₆ ,, ∅′ ,, ∅′ ,, ∅′ ,, ∅′ ,, ∅′
  tree⁷->tree (∅  , ∅  , ∅  , ∅  , [ a , b ] , t₅ , t₆)
              = ∅′ ,, t₆ ,, t₅ ,, a ,, b
  tree⁷->tree (t₀ , t₁ , t₂ , t₃ , t₄ , t₅ , t₆)
              = t₆ ,, t₅ ,, t₄ ,, t₃ ,, t₂ ,, t₁ ,, t₀

  tree->tree⁷ : BareBinTree → BareBinTree ⁷
  tree->tree⁷ [ [ [ [ [ ∅ , a ] , b ] , c ] , d ] , e ]
              = ∅ , ∅ , ∅ , ∅ , ∅ , ∅ , (a ,, b ,, c ,, d ,, e)
  tree->tree⁷ [ [ [ [ [ t₆ , t₅ ] , ∅ ] , ∅ ] , ∅ ] , ∅ ]
              = ∅ , ∅ , ∅ , ∅ , ∅ , t₅ , t₆
  tree->tree⁷ [ [ [ [ ∅ , t₆ ] , t₅ ] , a ] , b ]
              = ∅ , ∅ , ∅ , ∅ , (a ,, b) , t₅ , t₆
  tree->tree⁷ [ [ [ [ [ [ t₆ , t₅ ] , t₄ ] , t₃ ] , t₂ ] , t₁ ] , t₀ ]
              = t₀ , t₁ , t₂ , t₃ , t₄ , t₅ , t₆
  tree->tree⁷ a = ∅ , ∅ , ∅ , ∅ , ∅ , ∅ , a

  tree⁷<=>tree : BareBinTree ⁷ ⇔ BareBinTree
  tree⁷<=>tree = ∧-intro tree⁷->tree tree->tree⁷

  -- too hard
  -- proofL : ∀ tree → tree⁷->tree (tree->tree⁷ tree) ≡ tree
  -- proofL [ [ [ [ [ ∅ , a ] , b ] , c ] , d ] , e ]
  --        = refl
  -- proofL [ [ [ [ [ Node x t₆ t7 , t₅ ] , ∅ ] , ∅ ] , ∅ ] , ∅ ]
  --        = {!!}
  -- proofL [ [ [ [ ∅ , t₆ ] , t₅ ] , a ] , b ]
  --        = refl
  -- proofL [ [ [ [ [ [ t₆ , t₅ ] , t₄ ] , t₃ ] , t₂ ] , t₁ ] , t₀ ]
  --        = {!!}
  -- proofL _ = {!!}

------------------------------------------------------------------------
-- public aliases

iso-seven-tree-in-one : BareBinTree ⁷ ⇔ BareBinTree
iso-seven-tree-in-one = tree⁷<=>tree


text:
module Categories.Category.CartesianClosed.Bundle where

open import Categories.Category using (Category)
open import Categories.Category.CartesianClosed using (CartesianClosed)

open import Level

record CartesianClosedCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U : Category o ℓ e
    cartesianClosed : CartesianClosed U

  open Category U public
  open CartesianClosed cartesianClosed public

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
module String where

open import Common.IO
open import Common.List
open import Common.String
open import Common.Unit

testString : String
testString = "To boldly go where no man gone before"

printList : {A : Set} -> (A -> IO Unit) -> List A -> IO Unit
printList p [] = return unit
printList p (x ∷ xs) =
    p x ,,
    printList p xs

main : IO Unit
main =
    putStrLn testString ,,
    printList printChar (stringToList testString) ,,
    putStrLn "" ,,
    putStrLn (fromList (stringToList testString)) ,,
    return unit


text:
module SafetyProof where

open import Algebra
import Algebra.Properties.CommutativeSemigroup as CommutativeSemigroupProperties
open import Data.List
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Fin.Patterns using (0F; 1F)
open import Data.Nat using (z≤n; s≤s)
open import Data.Integer using (+≤+; +<+; +_)
open import Data.Vec using (_∷_)
import Data.Vec.Functional as Vector
open import Data.Product using (_×_; _,_; uncurry)
open import Data.Sum
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)

open import Vehicle.Data.Tensor
open import AbstractRationals
import WindControllerSpec as Vehicle

open ≤-Reasoning

------------------------------------------------------------------------
-- Setup

toTensor : ℚ → ℚ → Tensor ℚ (2 ∷ [])
toTensor x y = Vector.fromList (x ∷ y ∷ [])

roadWidth : ℚ
roadWidth = + 3 / 1

maxWindShift : ℚ
maxWindShift = 1ℚ

maxSensorError : ℚ
maxSensorError = + 1 / 4

roadWidth≥0 : roadWidth ≥ 0ℚ
roadWidth≥0 = *≤* (+≤+ z≤n)

maxWindShift≥0 : maxWindShift ≥ 0ℚ
maxWindShift≥0 = *≤* (+≤+ z≤n)

maxSensorError≥0 : maxSensorError ≥ 0ℚ
maxSensorError≥0 = *≤* (+≤+ z≤n)

------------------------------------------------------------------------
-- Model data

record State : Set where
  constructor state
  field
    windSpeed : ℚ
    position  : ℚ
    velocity  : ℚ
    sensor    : ℚ

open State

record Observation : Set where
  constructor observe
  field
    windShift   : ℚ
    sensorError : ℚ

open Observation

------------------------------------------------------------------------
-- Model transitions

initialState : State
initialState = record
  { windSpeed = 0ℚ
  ; position  = 0ℚ
  ; velocity  = 0ℚ
  ; sensor    = 0ℚ
  }

controller : ℚ → ℚ → ℚ
controller x y = Vehicle.controller (toTensor x y)

nextState : Observation → State → State
nextState o s = record
  { windSpeed = newWindSpeed
  ; position  = newPosition
  ; velocity  = newVelocity
  ; sensor    = newSensor
  }
  where
  newWindSpeed = windSpeed s + windShift o
  newPosition  = position s + velocity s + newWindSpeed
  newSensor    = newPosition + sensorError o
  newVelocity  = velocity s + controller newSensor (sensor s)

finalState : List Observation → State
finalState xs = foldr nextState initialState xs

------------------------------------------------------------------------
-- Definition of correctness

nextPosition-windShift : State → ℚ
nextPosition-windShift s = position s + velocity s + windSpeed s

-- The vehicle is on the road if its position is less than the
-- width of the road.
OnRoad : State → Set
OnRoad s = ∣ position s ∣ ≤ roadWidth

-- The vehicle is in a "safe" state if it's more than the maxWindShift away
-- from the edge of the road.
SafeDistanceFromEdge : State → Set
SafeDistanceFromEdge s = ∣ nextPosition-windShift s ∣ < roadWidth - maxWindShift

-- The vehicle's previous sensor reading is accurate if it is no more than the
-- maximum error away from it's true location.
AccurateSensorReading : State → Set
AccurateSensorReading s = ∣ position s - sensor s ∣ ≤ maxSensorError

-- The vehicle's previous sensor reading was not off the road
SensorReadingNotOffRoad : State → Set
SensorReadingNotOffRoad s = ∣ sensor s ∣ ≤ roadWidth + maxSensorError

-- A state is safe if it both a safe distance from the edge and it's sensor
-- reading is accurate.
SafeState : State → Set
SafeState s = SafeDistanceFromEdge s
            × AccurateSensorReading s
            × SensorReadingNotOffRoad s

-- An observation is valid if the observed sensor error and the wind shift
-- are less than the expected maximum shifts.
ValidObservation : Observation → Set
ValidObservation o = ∣ sensorError o ∣ ≤ maxSensorError
                   × ∣ windShift   o ∣ ≤ maxWindShift

------------------------------------------------------------------------
-- Proof of correctness

-- Initial state is both a safe distance from the edge and on the road

initialState-onRoad : OnRoad initialState
initialState-onRoad = roadWidth≥0

initialState-safe : SafeState initialState
initialState-safe rewrite +-eq | *-eq | neg-eq =
  *<* (+<+ (s≤s z≤n)) ,
  *≤* (+≤+ z≤n) ,
  *≤* (+≤+ z≤n)

-- Transitions are well-behaved

controller-lem : ∀ x y →
                 ∣ x ∣ ≤ roadWidth + maxSensorError →
                 ∣ y ∣ ≤ roadWidth + maxSensorError →
                 ∣ controller x y + 2ℚ * x - y ∣ < roadWidth - maxWindShift - 3ℚ * maxSensorError
controller-lem x y ∣x∣≤rw+εₘₐₓ ∣y∣≤rw+εₘₐₓ rewrite +-eq | *-eq | neg-eq =
  uncurry -p<q<p⇒∣q∣<p (Vehicle.safe (toTensor x y) (λ
    { 0F → ∣p∣≤q⇒-q≤p≤q x ∣x∣≤rw+εₘₐₓ
    ; 1F → ∣p∣≤q⇒-q≤p≤q y ∣y∣≤rw+εₘₐₓ
    }))

valid⇒nextState-accurateSensor : ∀ o → ValidObservation o → ∀ s →
                                 AccurateSensorReading (nextState o s)
valid⇒nextState-accurateSensor o (ε≤εₘₐₓ , _) s = let s' = nextState o s in begin
  ∣ position s' - sensor s' ∣                     ≡⟨⟩
  ∣ position s' - (position s' + sensorError o) ∣ ≡⟨ cong ∣_∣ (p-[p+q]≡q (position s') (sensorError o)) ⟩
  ∣ sensorError o ∣                               ≤⟨ ε≤εₘₐₓ ⟩
  maxSensorError                                  ∎

valid+safe⇒nextState-onRoad : ∀ o → ValidObservation o →
                              ∀ s → SafeState s →
                              OnRoad (nextState o s)
valid+safe⇒nextState-onRoad o (_ , δw≤δwₘₐₓ) s (safeDist , _ , _) = begin
  ∣ position s + velocity s + (windSpeed s + windShift o) ∣ ≡˘⟨ cong ∣_∣ (+-assoc (position s + velocity s) (windSpeed s) (windShift o)) ⟩
  ∣ position s + velocity s + windSpeed s + windShift o   ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ _ (windShift o) ⟩
  ∣ nextPosition-windShift s ∣ + ∣ windShift o ∣            ≤⟨ +-mono-≤ (<⇒≤ safeDist) δw≤δwₘₐₓ ⟩
  roadWidth - maxWindShift + maxWindShift                   ≡⟨ p-q+q≡p roadWidth maxWindShift ⟩
  roadWidth                                                 ∎

valid+safe⇒nextState-sensorReadingNotOffRoad : ∀ s → SafeState s → ∀ o → ValidObservation o →
                                               SensorReadingNotOffRoad (nextState o s)
valid+safe⇒nextState-sensorReadingNotOffRoad s safe o valid@(ε≤εₘₐₓ , _) = begin
  ∣ position (nextState o s) + sensorError o ∣       ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (position s + velocity s + (windSpeed s + windShift o)) (sensorError o) ⟩
  ∣ position (nextState o s) ∣ + ∣ sensorError o ∣   ≤⟨ +-mono-≤ (valid+safe⇒nextState-onRoad o valid s safe) ε≤εₘₐₓ ⟩
  roadWidth + maxSensorError                         ∎

valid+safe⇒nextState-safeDistanceFromEdge : ∀ o → ValidObservation o →
                                            ∀ s → SafeState s →
                                            SafeDistanceFromEdge (nextState o s)
valid+safe⇒nextState-safeDistanceFromEdge o valid@(ε-accurate , _) s safe@(safeDist , ε'-accurate , s-notOffRoad) = let
    s' = nextState o s
    y  = position  s; y' = position  s'
    v  = velocity  s; v' = velocity  s'
    w  = windSpeed s; w' = windSpeed s'
    p  = sensor    s; p' = sensor    s'
    ε  = y - p;       ε' = sensorError o
    dw = windShift   o
    dv = controller p' p
    ∣dv+2p'-p∣ = ∣ dv + 2ℚ * p' - p ∣
    s'-notOffRoad = valid+safe⇒nextState-sensorReadingNotOffRoad s safe o valid
  in begin-strict
  ∣ y' + v' + w' ∣                                                  ≡⟨ cong ∣_∣ (sym (p+q-q≡p (y' + v' + w') _)) ⟩
  ∣ y' + (v + dv) + w' + (y + ε' + ε' - p) - (y + ε' + ε' - p) ∣    ≡⟨ cong ∣_∣ (lem1 y' v dv w' y ε' p) ⟩
  ∣ dv + (y' + ε' + (y + v + w' + ε')) - p - (ε' + ε' + (y - p)) ∣  ≡⟨⟩
  ∣ dv + (p' + p') - p - (ε' + ε' + (y - p)) ∣                      ≡⟨ cong ∣_∣ (cong₂ (λ a b → dv + a - p - (b + (y - p))) (sym (2*p≡p+p p')) (sym (2*p≡p+p ε'))) ⟩
  ∣ dv + 2ℚ * p' - p - (2ℚ * ε' + (y - p)) ∣                        ≤⟨ ∣p-q∣≤∣p∣+∣q∣ (dv + 2ℚ * p' - p) (2ℚ * ε' + (y - p)) ⟩
  ∣ dv + 2ℚ * p' - p ∣ + ∣ 2ℚ * ε' + (y - p) ∣                      ≤⟨ +-monoʳ-≤ _ (∣p+q∣≤∣p∣+∣q∣ (2ℚ * ε') (y - p)) ⟩
  ∣ dv + 2ℚ * p' - p ∣ + (∣ 2ℚ * ε' ∣ + ∣ y - p ∣)                  ≡⟨ cong (λ v → ∣dv+2p'-p∣ + v) (cong (_+ _) (∣p*q∣≡∣p∣*∣q∣ 2ℚ ε')) ⟩
  ∣ dv + 2ℚ * p' - p ∣ + (2ℚ * ∣ ε' ∣ + ∣ ε ∣)                      ≤⟨ +-monoʳ-≤ _ (+-mono-≤ (*-monoʳ-≤ 2ℚ _ ε-accurate) ε'-accurate) ⟩
  ∣ dv + 2ℚ * p' - p ∣ + (2ℚ * maxSensorError + maxSensorError)     ≡⟨ cong (λ v → ∣dv+2p'-p∣ + v) (2p+p≡3p maxSensorError) ⟩
  ∣ dv + 2ℚ * p' - p ∣ + 3ℚ * maxSensorError                        <⟨ p<r-q⇒p+q<r _ _ _ (controller-lem p' p s'-notOffRoad s-notOffRoad) ⟩
  roadWidth - maxWindShift                                          ∎

safe⇒nextState-safe : ∀ s → SafeState s → ∀ o → ValidObservation o → SafeState (nextState o s)
safe⇒nextState-safe s safe o valid =
  valid+safe⇒nextState-safeDistanceFromEdge o valid s safe ,
  valid⇒nextState-accurateSensor o valid s ,
  valid+safe⇒nextState-sensorReadingNotOffRoad s safe o valid

finalState-safe : ∀ xs → All ValidObservation xs → SafeState (finalState xs)
finalState-safe []       []         = initialState-safe
finalState-safe (x ∷ xs) (px ∷ pxs) = safe⇒nextState-safe (finalState xs) (finalState-safe xs pxs) x px

finalState-onRoad : ∀ xs → All ValidObservation xs → OnRoad (finalState xs)
finalState-onRoad []       []         = initialState-onRoad
finalState-onRoad (x ∷ xs) (px ∷ pxs) = valid+safe⇒nextState-onRoad x px (finalState xs) (finalState-safe xs pxs)

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
------------------------------------------------------------------------------
-- First-order Peano arithmetic
------------------------------------------------------------------------------

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

module PA.Inductive.README where

-- Formalization of first-order Peano arithmetic using Agda data types
-- and primitive recursive functions for addition and multiplication.

------------------------------------------------------------------------------
-- Inductive definitions
open import PA.Inductive.Base

-- Some properties
open import PA.Inductive.PropertiesATP
open import PA.Inductive.PropertiesI

open import PA.Inductive.PropertiesByInduction
open import PA.Inductive.PropertiesByInductionATP
open import PA.Inductive.PropertiesByInductionI

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use `Data.Vec.Functional` instead.
------------------------------------------------------------------------

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

-- Disabled to prevent warnings from other Table modules
{-# OPTIONS --warn=noUserWarning #-}

module Data.Table.Relation.Equality where

open import Data.Table.Relation.Binary.Equality public

{-# WARNING_ON_IMPORT
"Data.Table.Relation.Equality was deprecated in v1.0.
Use Data.Vec.Functional.Relation.Binary.Pointwise instead."
#-}


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

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

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

postulate
  A : Set
  .a : A

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

f : {X : Set} → Box X → Box (Box X)
f [ x ] = [ [ implicit ] ]
-- this as well

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.GradedRing.Instances.CohomologyRing where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.Instances.NatPlusBis
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.Unit
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumHIT

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

private variable
  ℓ : Level

open PlusBis
open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆

module _
  (A : Type ℓ)
  where

  CohomologyRing-GradedRing : GradedRing ℓ-zero ℓ
  CohomologyRing-GradedRing = makeGradedRingSelf
                              NatPlusBis-Monoid
                              (λ k → coHom k A)
                              (λ k → snd (coHomGroup k A) )
                              1⌣
                              _⌣_
                              (λ {k} {l} → 0ₕ-⌣ k l)
                              (λ {k} {l} → ⌣-0ₕ k l)
                              (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ ((sym (+'-assoc _ _ _)) , (sym (assoc-⌣ _ _ _ _ _ _)))) )
                              (λ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _) , sym (lUnit⌣ _ _))))
                              (λ _ → ΣPathTransport→PathΣ _ _ (refl , transportRefl _ ∙ rUnit⌣ _ _))
                              (λ _ _ _ → leftDistr-⌣ _ _ _ _ _)
                              ( λ _ _ _ → rightDistr-⌣ _ _ _ _ _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module RandomAccessList.Redundant where

open import RandomAccessList.Redundant.Core
open import RandomAccessList.Redundant.Core.Properties
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)
import BuildingBlock.BinaryLeafTree as BLT

-- open import Data.Fin
open import Data.Num.Nat
open import Data.Num.Redundant
open import Data.Num.Redundant.Properties
open import Data.Nat renaming (_<_ to _<ℕ_)
open import Data.Nat.DivMod
open import Data.Nat.Etc
open import Data.Product
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; trans; sym; subst; inspect)

--------------------------------------------------------------------------------
--  Operations
--------------------------------------------------------------------------------

consₙ : ∀ {n A} → BinaryLeafTree A n → 0-2-RAL A n → 0-2-RAL A n
consₙ a []            = a 1∷ []
consₙ a (      0∷ xs) = a 1∷ xs
consₙ a (x     1∷ xs) = a , x 2∷ xs
consₙ a (x , y 2∷ xs) = a 1∷ consₙ (Node x y) xs

cons : ∀ {A} → A → 0-2-RAL A 0 → 0-2-RAL A 0
cons a xs = consₙ (Leaf a) xs

headₙ :  ∀ {n A} → (xs : 0-2-RAL A n) → ⟦ xs ⟧ₙ ≉ zero ∷ [] → BinaryLeafTree A n
headₙ []            p = contradiction (eq refl) p
headₙ (      0∷ xs) p = proj₁ (BLT.split (headₙ xs (contraposition (>>-zero ⟦ xs ⟧ₙ) p)))
headₙ (x     1∷ xs) p = x
headₙ (x , y 2∷ xs) p = x

head : ∀ {A} → (xs : 0-2-RAL A 0) → ⟦ xs ⟧ ≉ zero ∷ [] → A
head xs p = BLT.head (headₙ xs p)

tailₙ : ∀ {n A} → (xs : 0-2-RAL A n) → ⟦ xs ⟧ₙ ≉ zero ∷ [] → 0-2-RAL A n
tailₙ []            p = contradiction (eq refl) p
tailₙ (      0∷ xs) p = proj₂ (BLT.split (headₙ xs (contraposition (>>-zero ⟦ xs ⟧ₙ) p))) 1∷ tailₙ xs (contraposition (>>-zero ⟦ xs ⟧ₙ) p)
tailₙ (x     1∷ xs) p = 0∷ xs
tailₙ (x , y 2∷ xs) p = y 1∷ xs

tail : ∀ {A} → (xs : 0-2-RAL A 0) → ⟦ xs ⟧ ≉ zero ∷ [] → 0-2-RAL A 0
tail xs p = tailₙ xs p
--------------------------------------------------------------------------------
--  Searching
--------------------------------------------------------------------------------

data Finite : Redundant → Set where
    finite  : ∀ {bound}                         -- # of elements
            → (a : Redundant)                   -- inhabitant
            → {a<bound : a < bound}
            → Finite bound

elemAt : ∀ {n A} → (xs : 0-2-RAL A n) → Finite ⟦ xs ⟧ → A
elemAt {n} {A} [] (finite a {a<[]}) = contradiction a<[] {!   !}
-- elemAt {n} {A} [] (finite a {a<b}) = contradiction a<b (contraposition (map-≤ refl (to≡ (<<<-zero 0 ⟦ [] {A} {n} ⟧ {⟦[]⟧≈zero∷[] ([] {A} {n}) {refl}}))) (λ ()))
elemAt (0∷ xs) i = elemAt xs {!   !}
elemAt (x     1∷ xs) i = {!   !}
elemAt (x , y 2∷ xs) i = {!   !}

{-
-- data Occurrence : Set where
--    here : ∀ {a n} → a * Fin (2 ^ n) → Occurrence
--    there : Occurrence

transportFin : ∀ {a b} → a ≡ b → Fin a → Fin b
transportFin refl i = i

elemAt : ∀ {n A} → (xs : 0-2-RAL A n) → Fin ⟦ xs ⟧ → A
elemAt {zero} [] ()
elemAt {suc n} {A} []    i = elemAt {n} ([] {A} {n}) (transportFin (⟦[]⟧≡⟦[]⟧ {m = suc n} {n = n} {A = A}) i)
elemAt     (      0∷ xs) i = elemAt xs (transportFin (⟦0∷xs⟧≡⟦xs⟧ xs) i)
elemAt {n} (x     1∷ xs) i with (1 * 2 ^ n) ≤? toℕ i
elemAt     (x     1∷ xs) i | yes p rewrite splitIndex x xs = elemAt xs (reduce≥ i p)
elemAt {n} (x     1∷ xs) i | no ¬p with toℕ i divMod (2 ^ n)
elemAt (x 1∷ xs) i | no ¬p | result quotient remainder property = BLT.elemAt x remainder
elemAt {n} (x , y 2∷ xs) i with (2 * 2 ^ n) ≤? toℕ i
elemAt     (x , y 2∷ xs) i | yes p rewrite splitIndex2 x y xs = elemAt xs (reduce≥ i p)
elemAt {n} (x , y 2∷ xs) i | no ¬p with toℕ i divMod (2 ^ n)
elemAt (x , y 2∷ xs) i | no ¬p | result zero remainder property = BLT.elemAt x remainder
elemAt (x , y 2∷ xs) i | no ¬p | result (suc quotient) remainder property = BLT.elemAt y remainder
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module examplesPaperJFP.Object where

open import Data.Product
open import Data.String.Base

open import examplesPaperJFP.NativeIOSafe
open import examplesPaperJFP.BasicIO hiding (main)
open import examplesPaperJFP.Console hiding (main)

record Interface  :  Set₁ where
  field  Method   :  Set
         Result   :  (m : Method) → Set

open Interface public

record Object (I : Interface) : Set where
  coinductive
  field objectMethod : (m : Method I) → Result I m × Object I

open Object public

record IOObject (Iᵢₒ : IOInterface) (I : Interface) : Set where
  coinductive
  field method : (m : Method I) → IO Iᵢₒ (Result I m × IOObject Iᵢₒ I)

open IOObject public

data CellMethod A : Set where
    get  :  CellMethod A
    put  :  A → CellMethod A

CellResult             :  ∀{A} → CellMethod A → Set
CellResult   {A} get   =  A
CellResult   (put _)   =  Unit

cellJ                  :  (A : Set) → Interface
Method    (cellJ A)    =  CellMethod A
Result    (cellJ A) m  =  CellResult m

CellC : Set
CellC = IOObject ConsoleInterface (cellJ String)

simpleCell : (s : String) → CellC
force (method (simpleCell s) get) =
  exec′ (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  delay (return′ (s , simpleCell s))
force (method (simpleCell s) (put x)) =
  exec′ (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  delay (return′ (unit , simpleCell x))

{-# TERMINATING #-}

program : IOConsole Unit
force program =
  let c₁ = simpleCell "Start" in
  exec′ getLine          λ{ nothing → return unit; (just s) →
  method c₁ (put s)    >>= λ{ (_ , c₂) →
  method c₂ get        >>= λ{ (s′ , _ ) →
  exec (putStrLn s′)     λ _ →
  program }}}

main : NativeIO Unit
main = translateIOConsole program

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2019-05-15
-- imports
-- Author: ice1000
--

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

import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality
import Relation.Binary.PropositionalEquality using ()
import Relation.Binary.PropositionalEquality using (sym) hiding (cong)
import Relation.Binary.PropositionalEquality renaming (sym to symBla)

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_name: dubinsky/intellij-dtlc


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

module FOT.FOTC.Data.List.PostulatesVersusDataTypes where

-- See Agda mailing list.
-- Subject: Agda's unification: postulates versus data types

module M₁ where
  data D : Set where
    _∷_ : D → D → D

  data List : D → Set where
    cons : ∀ x xs → List xs → List (x ∷ xs)

  tail : ∀ {x xs} → List (x ∷ xs) → List xs
  tail {x} {xs} (cons .x .xs xsL) = xsL

module M₂ where
  postulate
    D   : Set
    _∷_ : D → D → D

  data List : D → Set where
    cons : ∀ x xs → List xs → List (x ∷ xs)

  tail : ∀ {x xs} → List (x ∷ xs) → List xs
  tail l = {!!}  -- C-c C-c fails


text:
------------------------------------------------------------------------
-- Some tactics aimed at making equational reasoning proofs more
-- readable for path equality
------------------------------------------------------------------------

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

module Tactic.By.Path where

import Agda.Builtin.Cubical.Path

open import Equality.Path
open import Prelude

open import List equality-with-J as L
open import Maybe equality-with-J
open import Monad equality-with-J
open import Tactic.By equality-with-J as TB
open import TC-monad equality-with-J as TC hiding (Type)

open TB public using (⟨_⟩)

private

  -- Constructs the type of equalities between its two arguments.

  equality : Term → Term → TC.Type
  equality lhs rhs = def (quote _≡_) (varg lhs ∷ varg rhs ∷ [])

  -- An illustration of what the cong functions constructed by
  -- make-cong-called look like.

  cong₃′ :
    ∀ {a b c d : Level}
      {A : Type a} {B : Type b} {C : Type c} {D : Type d}
      {x₁ y₁ x₂ y₂ x₃ y₃}
    (f : A → B → C → D) →
    x₁ ≡ y₁ → x₂ ≡ y₂ → x₃ ≡ y₃ → f x₁ x₂ x₃ ≡ f y₁ y₂ y₃
  cong₃′ f eq₁ eq₂ eq₃ = λ i → f (eq₁ i) (eq₂ i) (eq₃ i)

  -- Constructs a "cong" function, with the given name, for functions
  -- with the given number of arguments.

  make-cong-called : Name → ℕ → TC ⊤
  make-cong-called cong n = do
    declareDef (varg cong) (type-of-cong equality n)
    defineFun cong (the-clause ∷ [])
    where
    arguments : ℕ → List (Arg Term)
    arguments zero    = []
    arguments (suc m) = varg (var (suc m) (varg (var 0 []) ∷ [])) ∷
                        arguments m

    the-clause = clause
      (("f" , varg unknown) ∷ replicate n ("eq" , varg unknown))
      (varg (var n) ∷ L.map (varg ∘ var) (nats-< n))
      (lam visible $ abs "i" $
       var (n + 1) (arguments n))

  unquoteDecl cong₃  = make-cong-called cong₃   3
  unquoteDecl cong₄  = make-cong-called cong₄   4
  unquoteDecl cong₅  = make-cong-called cong₅   5
  unquoteDecl cong₆  = make-cong-called cong₆   6
  unquoteDecl cong₇  = make-cong-called cong₇   7
  unquoteDecl cong₈  = make-cong-called cong₈   8
  unquoteDecl cong₉  = make-cong-called cong₉   9
  unquoteDecl cong₁₀ = make-cong-called cong₁₀ 10

  -- Constructs a "cong" function (similar to cong and cong₂ in
  -- Equality) for functions with the given number of arguments. The
  -- name of the constructed function is returned (for 1 and 2 the
  -- functions in Equality are returned). The cong functions for
  -- functions with 3 up to 10 arguments are cached to avoid creating
  -- lots of copies of the same functions.

  make-cong : ℕ → TC Name
  make-cong  1 = return (quote cong)
  make-cong  2 = return (quote cong₂)
  make-cong  3 = return (quote cong₃)
  make-cong  4 = return (quote cong₄)
  make-cong  5 = return (quote cong₅)
  make-cong  6 = return (quote cong₆)
  make-cong  7 = return (quote cong₇)
  make-cong  8 = return (quote cong₈)
  make-cong  9 = return (quote cong₉)
  make-cong 10 = return (quote cong₁₀)
  make-cong n  = do
    cong ← freshName "cong"
    make-cong-called cong n
    return cong

open Tactics
  (λ where
     (def (quote Agda.Builtin.Cubical.Path.PathP)
          (arg _ a ∷ arg _ P ∷ arg _ x ∷ arg _ y ∷ [])) → do
       A ← case P of λ where
             (lam _ (abs _ A)) → case bound? 0 A of λ where
               (definitely true) → return unknown
               _                 → return (strengthen-term 0 1 A)
             _ → return unknown
       return $ just (a , A , x , y)
     _ → return nothing)
  equality
  (λ a A x → def (quote refl) (harg a ∷ harg A ∷ harg x ∷ []))
  (λ p → def (quote sym) (varg p ∷ []))
  (λ lhs rhs f p → def (quote cong)
                       (replicate 3 (harg unknown) ++
                        harg lhs ∷ harg rhs ∷ varg f ∷ varg p ∷ []))
  false
  make-cong
  true
  public

------------------------------------------------------------------------
-- Some unit tests

-- Test cases that are commented out fail (or at least they failed at
-- some point).

private

  module Tests
    (assumption : 48 ≡ 42)
    (lemma      : ∀ n → n + 8 ≡ n + 2)
    (f          : ℕ → ℕ → ℕ → ℕ)
    where

    g : ℕ → ℕ → ℕ → ℕ
    g zero    _ _ = 12
    g (suc _) _ _ = 12

    fst : ∀ {a b} {A : Type a} {B : A → Type b} →
          Σ A B → A
    fst = proj₁

    {-# NOINLINE fst #-}

    _≡′_ : {A : Type} → A → A → Type
    _≡′_ = _≡_

    {-# NOINLINE _≡′_ #-}

    record R (F : Type → Type) : Type₁ where
      field
        p : {A : Type} {x : F A} → x ≡ x

    open R ⦃ … ⦄ public

    -- Tests for by.

    module By-tests where

      test₁ : 40 + 2 ≡ 42
      test₁ = by definition

      test₂ : 48 ≡ 42 → 42 ≡ 48
      test₂ eq = by eq

      test₃ : (f : ℕ → ℕ) → f 42 ≡ f 48
      test₃ f = by assumption

      test₄ : (f : ℕ → ℕ) → f 48 ≡ f 42
      test₄ f = by assumption

      test₅ : (f : ℕ → ℕ → ℕ) → f 42 48 ≡ f 48 42
      test₅ f = by assumption

      test₆ : (f : ℕ → ℕ → ℕ → ℕ) → f 42 45 48 ≡ f 48 45 42
      test₆ f = by assumption

      test₇ : f 48 (f 42 45 48) 42 ≡ f 48 (f 48 45 42) 48
      test₇ = by assumption

      test₈ : ∀ n → g n (g n 45 48) 42 ≡ g n (g n 45 42) 48
      test₈ n = by assumption

      test₉ : (f : ℕ → ℕ) → f 42 ≡ f 48
      test₉ f = by (lemma 40)

      test₁₀ : (f : ℕ → ℕ) → f 42 ≡ f 48
      test₁₀ f = by (λ (_ : ⊤) → assumption)

      test₁₁ : (f : ℕ × ℕ → ℕ × ℕ) → (∀ x → f x ≡′ x) →
               fst (f (12 , 73)) ≡ fst {B = λ _ → ℕ} (12 , 73)
      test₁₁ _ hyp = by hyp

      test₁₂ : (h : ℕ → Maybe ℕ) →
               ((xs : ℕ) → h xs ≡ just xs) →
               (xs : ℕ) → suc ⟨$⟩ h xs ≡ suc ⟨$⟩ return xs
      test₁₂ h hyp xs =
        suc ⟨$⟩ h xs       ≡⟨ by (hyp xs) ⟩∎h
        suc ⟨$⟩ return xs  ∎

      -- test₁₃ : (h : List ⊤ → Maybe (List ⊤)) →
      --          ((xs : List ⊤) → h xs ≡ just xs) →
      --          (x : ⊤) (xs : List ⊤) → _ ≡ _
      -- test₁₃ h hyp x xs =
      --   _∷_ ⟨$⟩ return x ⊛ h xs       ≡⟨ by (hyp xs) ⟩∎
      --   _∷_ ⟨$⟩ return x ⊛ return xs  ∎

      test₁₅ :
        (F : Type → Type → Type)
        (G : Bool → Type → Type) →
        ((A : Type) → F (G false A) A ≡ G false (F A A)) →
        (A : Type) →
        G false (F (G false A) A) ≡
        G false (G false (F A A))
      test₁₅ F G hyp A =
        G false (F (G false A) A)  ≡⟨ by hyp ⟩∎
        G false (G false (F A A))  ∎

      test₁₇ :
        (P : ℕ → Type)
        (f : ∀ {n} → P n → P n)
        (p : P 0) →
        f (subst P refl p) ≡ f p
      test₁₇ P _ _ = by (subst-refl P)

      test₁₈ :
        (subst′ :
           ∀ {a p} {A : Type a} {x y : A}
           (P : A → Type p) → x ≡ y → P x → P y) →
        (∀ {a p} {A : Type a} {x : A} (P : A → Type p) (p : P x) →
         subst′ P refl p ≡ p) →
        (P : ℕ → Type)
        (f : ∀ {n} → P n → P n)
        (p : P 0) →
        f (subst′ P refl p) ≡ f p
      test₁₈ _ subst′-refl P _ _ = by (subst′-refl P)

      -- test₁₉ :
      --   {F : Type → Type} ⦃ r : R F ⦄ {A : Type} {x₁ x₂ : F A}
      --   (p₁ p₂ : x₁ ≡ x₂) (assumption : p₁ ≡ p₂) →
      --   trans p p₁ ≡ trans p p₂
      -- test₁₉ p₁ p₂ assumption =
      --   trans p p₁  ≡⟨ by assumption ⟩∎
      --   trans p p₂  ∎

    -- Tests for ⟨by⟩.

    module ⟨By⟩-tests where

      test₁ : ⟨ 40 + 2 ⟩ ≡ 42
      test₁ = ⟨by⟩ refl

      test₂ : 48 ≡ 42 → ⟨ 42 ⟩ ≡ 48
      test₂ eq = ⟨by⟩ eq

      test₃ : (f : ℕ → ℕ) → f ⟨ 42 ⟩ ≡ f 48
      test₃ f = ⟨by⟩ assumption

      test₄ : (f : ℕ → ℕ) → f ⟨ 48 ⟩ ≡ f 42
      test₄ f = ⟨by⟩ assumption

      test₅ : (f : ℕ → ℕ → ℕ) → f ⟨ 42 ⟩ ⟨ 42 ⟩ ≡ f 48 48
      test₅ f = ⟨by⟩ assumption

      test₆ : (f : ℕ → ℕ → ℕ → ℕ) → f ⟨ 48 ⟩ 45 ⟨ 48 ⟩ ≡ f 42 45 42
      test₆ f = ⟨by⟩ assumption

      test₇ : f ⟨ 48 ⟩ (f ⟨ 48 ⟩ 45 ⟨ 48 ⟩) ⟨ 48 ⟩ ≡ f 42 (f 42 45 42) 42
      test₇ = ⟨by⟩ assumption

      test₈ : ∀ n → g n (g n 45 ⟨ 48 ⟩) ⟨ 48 ⟩ ≡ g n (g n 45 42) 42
      test₈ n = ⟨by⟩ assumption

      test₉ : (f : ℕ → ℕ) → f ⟨ 42 ⟩ ≡ f 48
      test₉ f = ⟨by⟩ (lemma 40)

      test₁₀ : (f : ℕ → ℕ) → f ⟨ 42 ⟩ ≡ f 48
      test₁₀ f = ⟨by⟩ (λ (_ : ⊤) → assumption)

      test₁₁ : (f : ℕ × ℕ → ℕ × ℕ) → (∀ x → f x ≡′ x) →
               fst ⟨ f (12 , 73) ⟩ ≡ fst {B = λ _ → ℕ} (12 , 73)
      test₁₁ _ hyp = ⟨by⟩ hyp

      test₁₂ : (h : ℕ → Maybe ℕ) →
               ((xs : ℕ) → h xs ≡ just xs) →
               (xs : ℕ) → suc ⟨$⟩ h xs ≡ suc ⟨$⟩ return xs
      test₁₂ h hyp xs =
        suc ⟨$⟩ ⟨ h xs ⟩   ≡⟨ ⟨by⟩ (hyp xs) ⟩∎
        suc ⟨$⟩ return xs  ∎

      test₁₃ : (h : List ⊤ → Maybe (List ⊤)) →
               ((xs : List ⊤) → h xs ≡ just xs) →
               (x : ⊤) (xs : List ⊤) → _ ≡ _
      test₁₃ h hyp x xs =
        _∷_ ⟨$⟩ return x ⊛ ⟨ h xs ⟩   ≡⟨ ⟨by⟩ (hyp xs) ⟩∎
        _∷_ ⟨$⟩ return x ⊛ return xs  ∎

      test₁₄ : (h : List ℕ → Maybe (List ℕ)) →
               ((xs : List ℕ) → h xs ≡ just xs) →
               (x : ℕ) (xs : List ℕ) → _ ≡ _
      test₁₄ h hyp x xs =
        _∷_ ⟨$⟩ ⟨ h xs ⟩   ≡⟨ ⟨by⟩ (hyp xs) ⟩∎
        _∷_ ⟨$⟩ return xs  ∎

      test₁₅ :
        (F : Type → Type → Type)
        (G : Bool → Type → Type) →
        ((A : Type) → F (G false A) A ≡ G false (F A A)) →
        (A : Type) →
        G false (F (G false A) A) ≡
        G false (G false (F A A))
      test₁₅ F G hyp A =
        G false ⟨ F (G false A) A ⟩  ≡⟨ ⟨by⟩ hyp ⟩∎
        G false (G false (F A A))    ∎

      test₁₆ : 48 ≡ 42 →
               _≡_ {A = ℕ → ℕ} (λ x → x + ⟨ 42 ⟩) (λ x → x + 48)
      test₁₆ hyp = ⟨by⟩ hyp

      test₁₇ :
        (P : ℕ → Type)
        (f : ∀ {n} → P n → P n)
        (p : P 0) →
        f ⟨ subst P refl p ⟩ ≡ f p
      test₁₇ P _ _ = ⟨by⟩ (subst-refl P)

      test₁₈ :
        (subst′ :
           ∀ {a p} {A : Type a} {x y : A}
           (P : A → Type p) → x ≡ y → P x → P y) →
        (∀ {a p} {A : Type a} {x : A} (P : A → Type p) (p : P x) →
         subst′ P refl p ≡ p) →
        (P : ℕ → Type)
        (f : ∀ {n} → P n → P n)
        (p : P 0) →
        f ⟨ subst′ P refl p ⟩ ≡ f p
      test₁₈ _ subst′-refl _ _ _ = ⟨by⟩ subst′-refl

      -- test₁₉ :
      --   {F : Type → Type} ⦃ r : R F ⦄ {A : Type} {x₁ x₂ : F A}
      --   (p₁ p₂ : x₁ ≡ x₂) (assumption : p₁ ≡ p₂) →
      --   trans p p₁ ≡ trans p p₂
      -- test₁₉ p₁ p₂ assumption =
      --   trans p p₁      ≡⟨⟩
      --   trans p ⟨ p₁ ⟩  ≡⟨ ⟨by⟩ assumption ⟩∎
      --   trans p p₂      ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import Polynomial.Simple.AlmostCommutativeRing
open import Relation.Binary
open import Data.Bool using (Bool; false; true ; _∧_; _∨_; not; if_then_else_)
open import Data.String using (String)
open import EqBool

module Relation.Traced
  {c ℓ}
  (base : AlmostCommutativeRing c ℓ)
  ⦃ eqBase : HasEqBool (AlmostCommutativeRing.Carrier base) ⦄
  (showBase : AlmostCommutativeRing.Carrier base → String)
  where

open import Data.Sum
open import Relation.Binary.Construct.Closure.Equivalence
open import Relation.Binary.Construct.Closure.Symmetric
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Data.String
open import Relation.Nullary
open import Function
open import Level using (_⊔_)
open import Algebra.FunctionProperties
open import Data.String renaming (_==_ to eqBoolString)
open import Data.Maybe
open import Data.Nat using (ℕ)

open AlmostCommutativeRing base
open import Polynomial.Expr.Normalising rawRing showBase

open import Agda.Builtin.FromNat using (Number; fromNat) public

instance
  numberVar : {{nc : Number Carrier}} → Number Expr
  numberVar {{nc}} = record
    { Constraint = Number.Constraint nc
    ; fromNat = λ n → C ( (Number.fromNat nc n)) }

data BinOp : Set where
  [+] : BinOp
  [*] : BinOp

instance
  eqBinOp : HasEqBool BinOp
  EqBool._==_ ⦃ eqBinOp ⦄ [+] [+] = true
  EqBool._==_ ⦃ eqBinOp ⦄ [+] [*] = false
  EqBool._==_ ⦃ eqBinOp ⦄ [*] [+] = false
  EqBool._==_ ⦃ eqBinOp ⦄ [*] [*] = true

liftBinOp : BinOp → Expr → Expr → Expr
liftBinOp [+] (C x) (C y) = normalise (C (x + y))
liftBinOp [+] (C x) (O y) = normalise (O (K x ⊕ y))
liftBinOp [+] (O x) (C y) = normalise (O (x ⊕ K y))
liftBinOp [+] (O x) (O y) = normalise (O (x ⊕ y))
liftBinOp [*] (C x) (C y) = normalise (C (x * y))
liftBinOp [*] (C x) (O y) = normalise (O (K x ⊗ y))
liftBinOp [*] (O x) (C y) = normalise (O (x ⊗ K y))
liftBinOp [*] (O x) (O y) = normalise (O (x ⊗ y))

⊟_ : Expr → Expr
⊟ C x = C (- x)
⊟ O x = normalise (O (⊝ x))

data Step : Set c where
  [sym]      : Step → Step
  [cong]     : Step → BinOp → Step → Step
  [-cong]    : Step → Step
  [refl]     : Expr  → Step
  [assoc]    : BinOp → Expr → Expr → Expr → Step
  [ident]    : BinOp → Expr → Step
  [comm]     : BinOp → Expr → Expr → Step
  [zero]     : Expr → Step
  [distrib]  : Expr → Expr → Expr → Step
  [-distrib] : Expr → Expr → Step
  [-+comm]   : Expr → Expr → Step

_==S_ : Step → Step → Bool
_==S_ ([sym] x) ([sym] y) = x ==S y
_==S_ ([cong] x x₁ x₂) ([cong] y y₁ y₂) = x ==S y ∧ x₁ EqBool.== y₁ ∧ x₂ ==S y₂
_==S_ ([-cong] x) ([-cong] y) = x ==S y
_==S_ ([assoc] x x₁ x₂ x₃) ([assoc] y y₁ y₂ y₃) = x EqBool.== y ∧ x₁ EqBool.== y₁ ∧ x₂ EqBool.== y₂ ∧ x₃ EqBool.== y₃
_==S_ ([ident] x x₁) ([ident] y y₁) = x EqBool.== y ∧ x₁ EqBool.== y₁
_==S_ ([comm] x x₁ x₂) ([comm] y y₁ y₂) = x EqBool.== y ∧ x₁ EqBool.== y₁ ∧ x₂ EqBool.== y₂
_==S_ ([zero] x) ([zero] y) = x EqBool.== y
_==S_ ([distrib] x x₁ x₂) ([distrib] y y₁ y₂) = x EqBool.== y ∧ x₁ EqBool.== y₁ ∧ x₂ EqBool.== y₂
_==S_ ([-distrib] x x₁) ([-distrib] y y₁) = x EqBool.== y ∧ x₁ EqBool.== y₁
_==S_ ([-+comm] x x₁) ([-+comm] y y₁) = x EqBool.== y ∧ x₁ EqBool.== y₁
_==S_ ([refl] x) ([refl] y) = x EqBool.== y
_==S_ _ _ = false

instance
  eqStep : HasEqBool Step
  EqBool._==_ {{eqStep}} = _==S_

record _≈ⁱ_ (x y : Expr) : Set c where
   constructor ~?_
   field
     why : Step
open _≈ⁱ_

interesting : Step → Maybe Step
interesting ([sym] x) = interesting x
interesting ([-cong] x) = interesting x
interesting ([refl] x) = nothing
interesting ([assoc] x x₁ x₂ x₃) = nothing
interesting ([ident] x x₁) = nothing
interesting ([zero] x) = nothing
interesting ([cong] x x₁ x₂) with interesting x | interesting x₂
interesting ([cong] x x₁ x₂) | just res₁ | just res₂ = just ([cong] res₁ x₁ res₂)
interesting ([cong] x x₁ x₂) | just res₁ | nothing  = just res₁
interesting ([cong] x x₁ x₂) | nothing | just res₂ = just res₂
interesting ([cong] x x₁ x₂) | nothing | nothing  = nothing
interesting s@([comm] _ x y) with x EqBool.== y
interesting s@([comm] _ x y) | true = nothing
interesting s@([comm] o (C x) (C y))    | false = nothing
interesting s@([comm] [+] (C x) x₂)     | false = if x EqBool.== 0# then nothing else just s
interesting s@([comm] [+] (O x) (C x₁)) | false = if x₁ EqBool.== 0# then nothing else just s
interesting s@([comm] [+] (O x) (O x₁)) | false = just s
interesting s@([comm] [*] (C x) x₂)     | false = if (x EqBool.== 0# ∨ x EqBool.== 1#) then nothing else just s
interesting s@([comm] [*] (O x) (C x₁)) | false = if (x₁ EqBool.== 0# ∨ x₁ EqBool.== 1#) then nothing else just s
interesting s@([comm] [*] (O x) (O x₁)) | false = just s
interesting s@([distrib] (C _) (C _) (C _)) = nothing
interesting s@([distrib] (C x) x₁ x₂) = if (x EqBool.== 0# ∨ x EqBool.== 1#) then nothing else just s
interesting s@([distrib] x x₁ x₂) = just s
interesting s@([-distrib] x x₁) = nothing
interesting s@([-+comm] x x₁) = nothing

neg-cong : ∀ {x y} → x ≈ⁱ y → ⊟_  x ≈ⁱ ⊟_  y
neg-cong (~? reason) = ~? ( [-cong] reason)

zip-cong : BinOp
         → (f : Expr → Expr → Expr)
         → Congruent₂ (EqClosure _≈ⁱ_) f
zip-cong op f {x₁} {x₂} {y₁} {y₂} ε ε = ε
zip-cong op f {x₁} {x₂} {y₁} {y₂} ε (inj₁ (~? yr) ◅ ys) = inj₁ (~? ([cong] ([refl] x₁) op yr)) ◅ zip-cong op f ε ys
zip-cong op f {x₁} {x₂} {y₁} {y₂} ε (inj₂ (~? yr) ◅ ys) = inj₂ (~? ([cong] ([refl] x₁) op yr)) ◅ zip-cong op f ε ys
zip-cong op f {x₁} {x₂} {y₁} {y₂} (inj₁ (~? xr) ◅ xs) ε = inj₁ (~? ([cong] xr op ([refl] y₁))) ◅ zip-cong op f xs ε
zip-cong op f {x₁} {x₂} {y₁} {y₂} (inj₂ (~? xr) ◅ xs) ε = inj₂ (~? ([cong] xr op ([refl] y₁))) ◅ zip-cong op f xs ε
zip-cong op f {x₁} {x₂} {y₁} {y₂} (inj₁ (~? xr) ◅ xs) (inj₁ (~? yr) ◅ ys) = inj₁ (~? ([cong] xr op yr)) ◅ zip-cong op f xs ys
zip-cong op f {x₁} {x₂} {y₁} {y₂} (inj₁ (~? xr) ◅ xs) (inj₂ (~? yr) ◅ ys) = inj₁ (~? ([cong] xr op ([sym] yr))) ◅ zip-cong op f xs ys
zip-cong op f {x₁} {x₂} {y₁} {y₂} (inj₂ (~? xr) ◅ xs) (inj₁ (~? yr) ◅ ys) = inj₂ (~? ([cong] xr op ([sym] yr))) ◅ zip-cong op f xs ys
zip-cong op f {x₁} {x₂} {y₁} {y₂} (inj₂ (~? xr) ◅ xs) (inj₂ (~? yr) ◅ ys) = inj₂ (~? ([cong] xr op yr)) ◅ zip-cong op f xs ys

isZero : (x : Expr) → Maybe (EqClosure _≈ⁱ_ (C 0#) x)
isZero (C x) = if 0# EqBool.== x then just (inj₁ (~? [refl] (C x)) ◅ ε) else nothing
isZero _ = nothing

tracedRing : AlmostCommutativeRing c c
tracedRing = record
  { Carrier                 = Expr
  ; _≈_                     = EqClosure _≈ⁱ_
  ; _+_                     = liftBinOp [+]
  ; _*_                     = liftBinOp [*]
  ; -_                      = ⊟_
  ; 0#                      = C 0#
  ; 1#                      = C 1#
  ; 0≟_                     = isZero
  ; isAlmostCommutativeRing = record
    {  -‿cong      = Relation.Binary.Construct.Closure.ReflexiveTransitive.gmap ⊟_ (Data.Sum.map neg-cong neg-cong)
    ; -‿*-distribˡ = λ x y → return (inj₁ (~? [-distrib] x y))
    ; -‿+-comm     = λ x y → return (inj₁ (~? [-+comm] x y))
    ; isCommutativeSemiring = record
      { distribʳ = λ x y z → return (inj₁ (~? [distrib] x y z))
      ; zeroˡ = λ x → return (inj₁ (~? ([zero] x)))
      ; *-isCommutativeMonoid = record
        { identityˡ = λ x → return (inj₁ (~? [ident] [*] x))
        ; comm = λ x y → return (inj₁ (~? [comm] [*] x y))
        ; isSemigroup = record
          { assoc = λ x y z → return (inj₁ (~? [assoc] [*] x y z))
          ; isMagma = record
            { isEquivalence = Relation.Binary.Construct.Closure.Equivalence.isEquivalence _≈ⁱ_
            ; ∙-cong = zip-cong [*] (liftBinOp [*])
            }
          }
        }
      ; +-isCommutativeMonoid = record
        { identityˡ = λ x → return (inj₁ (~? ([ident] [+] x)))
        ; comm = λ x y → return (inj₁ (~? ([comm] [+] x y)))
        ; isSemigroup = record
          { assoc = λ x y z → return (inj₁ (~? ([assoc] [+] x y z)))
          ; isMagma = record
            { isEquivalence = Relation.Binary.Construct.Closure.Equivalence.isEquivalence _≈ⁱ_
            ; ∙-cong = zip-cong [+] (liftBinOp [+])
            }
          }
        }
      }
    }
  }

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

record Explanation {a} (A : Set a) : Set (a ⊔ c) where
  constructor _≈⟨_⟩≈_
  field
    lhs : A
    step : Step
    rhs : A
open Explanation

toExplanation : ∀ {x y} → x ≈ⁱ y → Explanation Expr
toExplanation {x} {y} x≈y = x ≈⟨ why x≈y ⟩≈ y

showProof′ : ∀ {x y} → EqClosure _≈ⁱ_ x y → List (Explanation Expr)
showProof′ ε = []
showProof′ (inj₁ x ◅ xs) = toExplanation x ∷ showProof′ xs
showProof′ (inj₂ y ◅ xs) = toExplanation y ∷ showProof′ xs

open import Data.String.Printf
open Printf standard

⟨_⟩ₛ : Step → String
⟨ [sym] x  ⟩ₛ             = printf "sym (%s)" ⟨ x ⟩ₛ
⟨ [cong] x [+] x₂ ⟩ₛ      = printf "(%s) + (%s)" ⟨ x ⟩ₛ ⟨ x₂ ⟩ₛ
⟨ [cong] x [*] x₂ ⟩ₛ      = printf "(%s) * (%s)" ⟨ x ⟩ₛ ⟨ x₂ ⟩ₛ
⟨ [-cong] x ⟩ₛ            = printf "- (%s)" ⟨ x ⟩ₛ
⟨ [refl] x ⟩ₛ             = "eval"
⟨ [assoc] [+] x₁ x₂ x₃ ⟩ₛ = printf "+-assoc(%s, %s, %s)" ⟨ x₁ ⟩ₑ  ⟨ x₂ ⟩ₑ ⟨ x₃ ⟩ₑ
⟨ [assoc] [*] x₁ x₂ x₃ ⟩ₛ = printf "*-assoc(%s, %s, %s)" ⟨ x₁ ⟩ₑ  ⟨ x₂ ⟩ₑ ⟨ x₃ ⟩ₑ
⟨ [ident] [+] x₁ ⟩ₛ       = printf "+-ident(%s)" ⟨ x₁ ⟩ₑ
⟨ [ident] [*] x₁ ⟩ₛ       = printf "*-ident(%s)" ⟨ x₁ ⟩ₑ
⟨ [comm] [+] x₁ x₂ ⟩ₛ     = printf "+-comm(%s, %s)" ⟨ x₁ ⟩ₑ ⟨ x₂ ⟩ₑ
⟨ [comm] [*] x₁ x₂ ⟩ₛ     = printf "*-comm(%s, %s)" ⟨ x₁ ⟩ₑ ⟨ x₂ ⟩ₑ
⟨ [zero] x ⟩ₛ             = printf "*-zero(%s)" ⟨ x ⟩ₑ
⟨ [distrib] x x₁ x₂ ⟩ₛ    = printf "*-distrib(%s, %s, %s)" ⟨ x ⟩ₑ ⟨ x₁ ⟩ₑ  ⟨ x₂ ⟩ₑ
⟨ [-distrib] x x₁ ⟩ₛ      = printf "-‿distrib(%s, %s)" ⟨ x ⟩ₑ ⟨ x₁ ⟩ₑ
⟨ [-+comm] x x₁ ⟩ₛ        = printf "-+-comm(%s, %s)" ⟨ x ⟩ₑ ⟨ x₁ ⟩ₑ

showProof : ∀ {x y} → EqClosure _≈ⁱ_ x y → List String
showProof = List.foldr unparse [] ∘ List.foldr spotReverse [] ∘ List.mapMaybe interesting′ ∘ showProof′
  where
  unparse : Explanation Expr → List String → List String
  unparse (lhs₁ ≈⟨ step₁ ⟩≈ rhs₁) [] = ⟨ lhs₁ ⟩ₑ ∷ printf "    ={ %s }" ⟨ step₁ ⟩ₛ ∷ ⟨ rhs₁ ⟩ₑ ∷ []
  unparse (lhs₁ ≈⟨ step₁ ⟩≈ rhs₁) (y ∷ ys) = if r EqBool.== y then l ∷ m ∷ y ∷ ys else l ∷ m ∷ r ∷ "    ={ eval }" ∷ y ∷ ys
    where
    l = ⟨ lhs₁ ⟩ₑ
    m = printf "    ={ %s }" ⟨ step₁ ⟩ₛ
    r = ⟨ rhs₁ ⟩ₑ

  spotReverse : Explanation Expr → List (Explanation Expr) → List (Explanation Expr)
  spotReverse x [] = x ∷ []
  spotReverse x (y ∷ xs) = if lhs x EqBool.== rhs y then xs else x ∷ y ∷ xs

  interesting′ : Explanation Expr → Maybe (Explanation Expr)
  interesting′ (lhs ≈⟨ stp ⟩≈ rhs) with interesting stp
  interesting′ (lhs ≈⟨ stp ⟩≈ rhs) | just x = just (lhs ≈⟨ x ⟩≈ rhs)
  interesting′ (lhs ≈⟨ stp ⟩≈ rhs) | nothing = nothing

open import Agda.Builtin.FromString using (IsString; fromString) public
import Data.String.Literals
open import Data.Unit using (⊤)
open import Level using (Lift)

instance
  stringString : IsString String
  stringString = Data.String.Literals.isString

instance
  lift-inst : ∀ {ℓ a} { A : Set a } → ⦃ x : A ⦄ → Lift ℓ A
  lift-inst ⦃ x = x ⦄ = Level.lift x

instance
  exprString : IsString Expr
  exprString = record
    { Constraint = λ _ → Lift _ ⊤ ; fromString = λ s → O (V s) }

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
module Pi-1 where

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

open import Groupoid

import Pi-2 as P

--infixr 10 _◎_
--infixr 30 _⟷_

------------------------------------------------------------------------------
-- Level -1:
-- Types are -1 groupoids or equivalently all types are mere propositions
--
-- Types and values are defined without references to programs
-- Types include PATHs from the previous level in addition to the usual types

data U : Set where
  ZERO  : U
  ONE   : U
  TIMES : U → U → U
  PATH  : {t₁ t₂ : P.U•} → (t₁ P.⟷ t₂) → U

data Path {t₁ t₂ : P.U•} : P.Space t₁ → P.Space t₂ → Set where
  path : (c : t₁ P.⟷ t₂) → Path (P.point t₁) (P.point t₂)

⟦_⟧ : U → Set
⟦ ZERO ⟧             = ⊥
⟦ ONE ⟧              = ⊤
⟦ TIMES t₁ t₂ ⟧      = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
⟦ PATH {t₁} {t₂} c ⟧ = Path {t₁} {t₂} (P.point t₁) (P.point t₂)

-- Proof that all types are mere propositions. Def. 3.3.1 in the HoTT book

isMereProposition : (t : U) → (v v' : ⟦ t ⟧) → (v ≡ v')
isMereProposition ZERO ()
isMereProposition ONE tt tt = refl
isMereProposition (TIMES t₁ t₂) (v₁ , v₂) (v₁' , v₂') =
 cong₂ _,′_ (isMereProposition t₁ v₁ v₁') (isMereProposition t₂ v₂ v₂')
isMereProposition (PATH {t₁} {t₂} c) (path c₁) (path c₂) = {!!}

-- c₁ : t₁ ⟷ t₂ in Pi-2
-- c₂ : t₁ ⟷ t₂ in Pi-2

-- Proof that every type is a groupoid; this does not depend on the
-- definition of programs

isGroupoid : U → 1Groupoid
isGroupoid ZERO               = discrete ⊥
isGroupoid ONE                = discrete ⊤
isGroupoid (TIMES t₁ t₂)      = isGroupoid t₁ ×G isGroupoid t₂
isGroupoid (PATH {t₁} {t₂} c) = {!!}

{--
------------------------------------------------------------------------------
-- Level -1:
-- if types are non-empty they must contain one point only like above
-- types may however be empty
--
-- We can prove that all types are either empty or equivalent to the unit
-- type (i.e., they are mere propositions)

module Pi-1 where

  data U : Set where
    ZERO : U
    ONE : U
    TIMES : U → U → U

  ⟦_⟧ : U → Set
  ⟦ ZERO ⟧ = ⊥
  ⟦ ONE ⟧ = ⊤
  ⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

------------------------------------------------------------------------------
-- Level 0:
-- types may contain any number of points (including none)
-- they are sets
--
-- We define isomorphisms between these sets that are reified to paths in the
-- next level (level 1). These isomorphisms are the combinators for a
-- commutative semiring structure which is sound and complete for sets.

module Pi0 where

  infixr 10 _◎_
  infixr 30 _⟷_

  -- types

  data U : Set where
    ZERO  : U
    ONE   : U
    PLUS  : U → U → U
    TIMES : U → U → U

  -- values

  ⟦_⟧ : U → Set
  ⟦ ZERO ⟧        = ⊥
  ⟦ ONE ⟧         = ⊤
  ⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
  ⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

  -- pointed types

  record U• : Set where
    constructor •[_,_]
    field
      ∣_∣ : U
      • : ⟦ ∣_∣ ⟧

  open U•

  Space : (t• : U•) → Set
  Space •[ t , v ] = ⟦ t ⟧

  point : (t• : U•) → Space t•
  point •[ t , v ] = v

  -- examples

  ONE• : U•
  ONE• = •[ ONE , tt ]

  BOOL : U
  BOOL = PLUS ONE ONE

  BOOL² : U
  BOOL² = TIMES BOOL BOOL

  TRUE : ⟦ BOOL ⟧
  TRUE = inj₁ tt

  FALSE : ⟦ BOOL ⟧
  FALSE = inj₂ tt

  BOOL•F : U•
  BOOL•F = •[ BOOL , FALSE ]

  BOOL•T : U•
  BOOL•T = •[ BOOL , TRUE ]

  -- isomorphisms between pointed types

  data _⟷_ : U• → U• → Set where
    unite₊  : {t : U•} → •[ PLUS ZERO ∣ t ∣ , inj₂ (• t) ] ⟷ t
    uniti₊  : {t : U•} → t ⟷ •[ PLUS ZERO ∣ t ∣ , inj₂ (• t) ]
    swap1₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷
                             •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₂ (• t₁) ]
    swap2₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷
                             •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₁ (• t₂) ]
    assocl1₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₁ (• t₁) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₁ (• t₁)) ]
    assocl2₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₁ (• t₂)) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₂ (• t₂)) ]
    assocl3₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₂ (• t₃)) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₂ (• t₃) ]
    assocr1₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₁ (• t₁)) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₁ (• t₁) ]
    assocr2₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₂ (• t₂)) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₁ (• t₂)) ]
    assocr3₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₂ (• t₃) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₂ (• t₃)) ]
    unite⋆  : {t : U•} → •[ TIMES ONE ∣ t ∣ , (tt , • t) ] ⟷ t
    uniti⋆  : {t : U•} → t ⟷ •[ TIMES ONE ∣ t ∣ , (tt , • t) ]
    swap⋆   : {t₁ t₂ : U•} → •[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂) ] ⟷
                             •[ TIMES ∣ t₂ ∣ ∣ t₁ ∣ , (• t₂ , • t₁) ]
    assocl⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ] ⟷
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ]
    assocr⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ] ⟷
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ]
    distz : {t : U•} {absurd : ⟦ ZERO ⟧} →
            •[ TIMES ZERO ∣ t ∣ , (absurd , • t) ] ⟷ •[ ZERO , absurd ]
    factorz : {t : U•} {absurd : ⟦ ZERO ⟧} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO ∣ t ∣ , (absurd , • t) ]
    dist1   : {t₁ t₂ t₃ : U•} →
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₁ (• t₁) , • t₃) ] ⟷
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₁ (• t₁ , • t₃) ]
    dist2   : {t₁ t₂ t₃ : U•} →
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₂ (• t₂) , • t₃) ] ⟷
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₂ (• t₂ , • t₃) ]
    factor1   : {t₁ t₂ t₃ : U•} →
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₁ (• t₁ , • t₃) ] ⟷
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₁ (• t₁) , • t₃) ]
    factor2   : {t₁ t₂ t₃ : U•} →
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₂ (• t₂ , • t₃) ] ⟷
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₂ (• t₂) , • t₃) ]
    id⟷    : {t : U•} → t ⟷ t
    sym⟷   : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
    _◎_    : {t₁ t₂ t₃ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
    _⊕1_   : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
             (•[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷
              •[ PLUS ∣ t₃ ∣ ∣ t₄ ∣ , inj₁ (• t₃) ])
    _⊕2_   : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
             (•[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷
              •[ PLUS ∣ t₃ ∣ ∣ t₄ ∣ , inj₂ (• t₄) ])
    _⊗_     : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
            (•[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂ ) ] ⟷
             •[ TIMES ∣ t₃ ∣ ∣ t₄ ∣ , (• t₃ , • t₄ ) ])

  -- examples

  NOT•T : •[ BOOL , TRUE ] ⟷ •[ BOOL , FALSE ]
  NOT•T = swap1₊

  NOT•F : •[ BOOL , FALSE ] ⟷ •[ BOOL , TRUE ]
  NOT•F = swap2₊

  CNOT•Fx : {b : ⟦ BOOL ⟧} →
            •[ BOOL² , (FALSE , b) ] ⟷ •[ BOOL² , (FALSE , b) ]
  CNOT•Fx = dist2 ◎ ((id⟷ ⊗ NOT•F) ⊕2 id⟷) ◎ factor2

  CNOT•TF : •[ BOOL² , (TRUE , FALSE) ] ⟷ •[ BOOL² , (TRUE , TRUE) ]
  CNOT•TF = dist1 ◎
            ((id⟷ ⊗ NOT•F) ⊕1 (id⟷ {•[ TIMES ONE BOOL , (tt , FALSE) ]})) ◎
            factor1

  CNOT•TT : •[ BOOL² , (TRUE , TRUE) ] ⟷ •[ BOOL² , (TRUE , FALSE) ]
  CNOT•TT = dist1 ◎
            ((id⟷ ⊗ NOT•T) ⊕1 (id⟷ {•[ TIMES ONE BOOL , (tt , TRUE) ]})) ◎
            factor1

------------------------------------------------------------------------------
-- Level 1
-- types are 1groupoids; they consist of points with collections of
-- non-trivial paths between them; the paths are defined at the previous
-- level (level 0).
--
-- We define isomorphisms between these level 1 paths that are reified as
-- 2paths in the next level (level 2). These isomorphisms include groupoid
-- combinators and commutative semiring combinators

module Pi1 where

  infixr 10 _◎_
  infixr 30 _⟷_

  -- types

  data U : Set where
    ZERO  : U
    ONE   : U
    PLUS  : U → U → U
    TIMES : U → U → U
    PATH  : {t₁ t₂ : Pi0.U•} → (t₁ Pi0.⟷ t₂) → U

  -- values

  data Path {t₁ t₂ : Pi0.U•} : (Pi0.Space t₁) → (Pi0.Space t₂) → Set where
    path : (c : t₁ Pi0.⟷ t₂) → Path (Pi0.point t₁) (Pi0.point t₂)

  ⟦_⟧ : U → Set
  ⟦ ZERO ⟧             = ⊥
  ⟦ ONE ⟧              = ⊤
  ⟦ PLUS t₁ t₂ ⟧       = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
  ⟦ TIMES t₁ t₂ ⟧      = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
  ⟦ PATH {t₁} {t₂} c ⟧ = Path {t₁} {t₂} (Pi0.point t₁) (Pi0.point t₂)

  -- pointed types

  record U• : Set where
    constructor •[_,_]
    field
      ∣_∣ : U
      • : ⟦ ∣_∣ ⟧

  open U•

  Space : (t• : U•) → Set
  Space •[ t , p ] = ⟦ t ⟧

  point : (t• : U•) → Space t•
  point •[ t , p ] = p

  _∘_ : {t₁ t₂ t₃ : Pi0.U•} →
        Path (Pi0.point t₁) (Pi0.point t₂) →
        Path (Pi0.point t₂) (Pi0.point t₃) →
        Path (Pi0.point t₁) (Pi0.point t₃)
  path c₁ ∘ path c₂ = path (c₁ Pi0.◎ c₂)

  PathSpace : {t₁ t₂ : Pi0.U•} → (c : t₁ Pi0.⟷ t₂) → U•
  PathSpace c = •[ PATH c , path c ]

  -- examples
  -- several paths between T and F; some of these will be equivalent

  p₁ p₂ p₃ p₄ : Path Pi0.TRUE Pi0.FALSE
  p₁ = path Pi0.swap1₊
  p₂ = path (Pi0.swap1₊ Pi0.◎ Pi0.id⟷)
  p₃ = path (Pi0.swap1₊ Pi0.◎ Pi0.swap2₊ Pi0.◎ Pi0.swap1₊)
  p₄ = path (Pi0.uniti⋆ Pi0.◎
             Pi0.swap⋆ Pi0.◎
             (Pi0.swap1₊ Pi0.⊗ Pi0.id⟷) Pi0.◎
             Pi0.swap⋆ Pi0.◎
             Pi0.unite⋆)

  -- groupoid combinators to reason about id, sym, and trans
  -- commutative semiring combinators for 0, 1, +, *

  data _⟷_ : U• → U• → Set where

    -- common combinators

    id⟷    : {t : U•} → t ⟷ t
    sym⟷   : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
    _◎_     : {t₁ t₂ t₃ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)

    -- groupoid combinators

    lidl    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (Pi0.id⟷ Pi0.◎ c) ⟷ PathSpace c
    lidr    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace c ⟷ PathSpace (Pi0.id⟷ Pi0.◎ c)
    ridl    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (c Pi0.◎ Pi0.id⟷) ⟷ PathSpace c
    ridr    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace c ⟷ PathSpace (c Pi0.◎ Pi0.id⟷)
    invll   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (Pi0.sym⟷ c Pi0.◎ c) ⟷ PathSpace {t₂} {t₂} Pi0.id⟷
    invlr   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace {t₂} {t₂} Pi0.id⟷ ⟷ PathSpace (Pi0.sym⟷ c Pi0.◎ c)
    invrl   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (c Pi0.◎ Pi0.sym⟷ c) ⟷ PathSpace {t₁} {t₁} Pi0.id⟷
    invrr   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace {t₁} {t₁} Pi0.id⟷ ⟷ PathSpace (c Pi0.◎ Pi0.sym⟷ c)
    invinvl : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (Pi0.sym⟷ (Pi0.sym⟷ c)) ⟷ PathSpace c
    invinvr : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace c ⟷ PathSpace (Pi0.sym⟷ (Pi0.sym⟷ c))
    tassocl : {t₁ t₂ t₃ t₄ : Pi0.U•}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃} {c₃ : t₃ Pi0.⟷ t₄} →
              PathSpace (c₁ Pi0.◎ (c₂ Pi0.◎ c₃)) ⟷
              PathSpace ((c₁ Pi0.◎ c₂) Pi0.◎ c₃)
    tassocr : {t₁ t₂ t₃ t₄ : Pi0.U•}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃} {c₃ : t₃ Pi0.⟷ t₄} →
              PathSpace ((c₁ Pi0.◎ c₂) Pi0.◎ c₃) ⟷
              PathSpace (c₁ Pi0.◎ (c₂ Pi0.◎ c₃))
    -- resp◎ is closely related to Eckmann-Hilton
    resp◎   : {t₁ t₂ t₃ : Pi0.U•}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃}
              {c₃ : t₁ Pi0.⟷ t₂} {c₄ : t₂ Pi0.⟷ t₃} →
              (PathSpace c₁ ⟷ PathSpace c₃) →
              (PathSpace c₂ ⟷ PathSpace c₄) →
              PathSpace (c₁ Pi0.◎ c₂) ⟷ PathSpace (c₃ Pi0.◎ c₄)

    -- commutative semiring combinators

    unite₊  : {t : U•} → •[ PLUS ZERO ∣ t ∣ , inj₂ (• t) ] ⟷ t
    uniti₊  : {t : U•} → t ⟷ •[ PLUS ZERO ∣ t ∣ , inj₂ (• t) ]
    swap1₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷
                             •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₂ (• t₁) ]
    swap2₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷
                             •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₁ (• t₂) ]
    assocl1₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₁ (• t₁) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₁ (• t₁)) ]
    assocl2₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₁ (• t₂)) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₂ (• t₂)) ]
    assocl3₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₂ (• t₃)) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₂ (• t₃) ]
    assocr1₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₁ (• t₁)) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₁ (• t₁) ]
    assocr2₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₂ (• t₂)) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₁ (• t₂)) ]
    assocr3₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₂ (• t₃) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₂ (• t₃)) ]
    unite⋆  : {t : U•} → •[ TIMES ONE ∣ t ∣ , (tt , • t) ] ⟷ t
    uniti⋆  : {t : U•} → t ⟷ •[ TIMES ONE ∣ t ∣ , (tt , • t) ]
    swap⋆   : {t₁ t₂ : U•} → •[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂) ] ⟷
                             •[ TIMES ∣ t₂ ∣ ∣ t₁ ∣ , (• t₂ , • t₁) ]
    assocl⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ] ⟷
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ]
    assocr⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ] ⟷
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ]
    distz : {t : U•} {absurd : ⟦ ZERO ⟧} →
            •[ TIMES ZERO ∣ t ∣ , (absurd , • t) ] ⟷ •[ ZERO , absurd ]
    factorz : {t : U•} {absurd : ⟦ ZERO ⟧} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO ∣ t ∣ , (absurd , • t) ]
    dist1   : {t₁ t₂ t₃ : U•} →
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₁ (• t₁) , • t₃) ] ⟷
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₁ (• t₁ , • t₃) ]
    dist2   : {t₁ t₂ t₃ : U•} →
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₂ (• t₂) , • t₃) ] ⟷
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₂ (• t₂ , • t₃) ]
    factor1   : {t₁ t₂ t₃ : U•} →
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₁ (• t₁ , • t₃) ] ⟷
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₁ (• t₁) , • t₃) ]
    factor2   : {t₁ t₂ t₃ : U•} →
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₂ (• t₂ , • t₃) ] ⟷
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₂ (• t₂) , • t₃) ]
    _⊕1_   : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
             (•[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷
              •[ PLUS ∣ t₃ ∣ ∣ t₄ ∣ , inj₁ (• t₃) ])
    _⊕2_   : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
             (•[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷
              •[ PLUS ∣ t₃ ∣ ∣ t₄ ∣ , inj₂ (• t₄) ])
    _⊗_     : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
            (•[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂ ) ] ⟷
             •[ TIMES ∣ t₃ ∣ ∣ t₄ ∣ , (• t₃ , • t₄ ) ])

  -- proof that we have a 1Groupoid structure

  G : 1Groupoid
  G = record
        { set = Pi0.U•
        ; _↝_ = Pi0._⟷_
        ; _≈_ = λ c₀ c₁ → PathSpace c₀ ⟷ PathSpace c₁
        ; id = Pi0.id⟷
        ; _∘_ = λ c₀ c₁ → c₁ Pi0.◎ c₀
        ; _⁻¹ = Pi0.sym⟷
        ; lneutr = λ _ → ridl
        ; rneutr = λ _ → lidl
        ; assoc = λ _ _ _ → tassocl
        ; equiv = record { refl = id⟷
                                ; sym = λ c → sym⟷ c
                                ; trans = λ c₀ c₁ → c₀ ◎ c₁ }
        ; linv = λ _ → invrl
        ; rinv = λ _ → invll
        ; ∘-resp-≈ = λ f⟷h g⟷i → resp◎ g⟷i f⟷h
        }

------------------------------------------------------------------------------
-- Level 2
-- types are 2groupoids; they are points with non-trivial paths between them
-- and non-trivial 2paths between the paths

module Pi2 where

  infixr 10 _◎_
  infixr 30 _⟷_

  -- types

  data U : Set where
    ZERO   : U
    ONE    : U
    PLUS   : U → U → U
    TIMES  : U → U → U
    PATH   : {t₁ t₂ : Pi0.U•} → (t₁ Pi0.⟷ t₂) → U
    2PATH  : {t₁ t₂ : Pi1.U•} → (t₁ Pi1.⟷ t₂) → U

  -- values

  data Path {t₁ t₂ : Pi0.U•} : (Pi0.Space t₁) → (Pi0.Space t₂) → Set where
    path : (c : t₁ Pi0.⟷ t₂) → Path (Pi0.point t₁) (Pi0.point t₂)

  data 2Path {t₁ t₂ : Pi1.U•} : Pi1.Space t₁ → Pi1.Space t₂ → Set where
    2path : (c : t₁ Pi1.⟷ t₂) → 2Path (Pi1.point t₁) (Pi1.point t₂)

  ⟦_⟧ : U → Set
  ⟦ ZERO ⟧             = ⊥
  ⟦ ONE ⟧              = ⊤
  ⟦ PLUS t₁ t₂ ⟧       = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
  ⟦ TIMES t₁ t₂ ⟧      = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
  ⟦ PATH {t₁} {t₂} c ⟧ = Path {t₁} {t₂} (Pi0.point t₁) (Pi0.point t₂)
  ⟦ 2PATH {t₁} {t₂} c ⟧ = 2Path {t₁} {t₂} (Pi1.point t₁) (Pi1.point t₂)

  -- pointed types

  record U• : Set where
    constructor •[_,_]
    field
      ∣_∣ : U
      • : ⟦ ∣_∣ ⟧

  open U•

  Space : (t• : U•) → Set
  Space •[ t , p ] = ⟦ t ⟧

  point : (t• : U•) → Space t•
  point •[ t , p ] = p

  _∘1_ : {t₁ t₂ t₃ : Pi0.U•} →
        Path (Pi0.point t₁) (Pi0.point t₂) →
        Path (Pi0.point t₂) (Pi0.point t₃) →
        Path (Pi0.point t₁) (Pi0.point t₃)
  path c₁ ∘1 path c₂ = path (c₁ Pi0.◎ c₂)

  _∘2_ : {t₁ t₂ t₃ : Pi1.U•} →
        2Path (Pi1.point t₁) (Pi1.point t₂) →
        2Path (Pi1.point t₂) (Pi1.point t₃) →
        2Path (Pi1.point t₁) (Pi1.point t₃)
  2path c₁ ∘2 2path c₂ = 2path (c₁ Pi1.◎ c₂)

  PathSpace : {t₁ t₂ : Pi0.U•} → (c : t₁ Pi0.⟷ t₂) → U•
  PathSpace c = •[ PATH c , path c ]

  2PathSpace : {t₁ t₂ : Pi1.U•} → (c : t₁ Pi1.⟷ t₂) → U•
  2PathSpace c = •[ 2PATH c , 2path c ]

  -- examples

  -- groupoid combinators to reason about id, sym, and trans
  -- commutative semiring combinators for 0, 1, +, *

  data _⟷_ : U• → U• → Set where

    -- common combinators

    id⟷    : {t : U•} → t ⟷ t
    sym⟷   : {t₁ t₂ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
    _◎_     : {t₁ t₂ t₃ : U•} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)

    -- 1groupoid combinators

    1lidl    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (Pi0.id⟷ Pi0.◎ c) ⟷ PathSpace c
    1lidr    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace c ⟷ PathSpace (Pi0.id⟷ Pi0.◎ c)
    1ridl    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (c Pi0.◎ Pi0.id⟷) ⟷ PathSpace c
    1ridr    : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace c ⟷ PathSpace (c Pi0.◎ Pi0.id⟷)
    1invll   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (Pi0.sym⟷ c Pi0.◎ c) ⟷ PathSpace {t₂} {t₂} Pi0.id⟷
    1invlr   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace {t₂} {t₂} Pi0.id⟷ ⟷ PathSpace (Pi0.sym⟷ c Pi0.◎ c)
    1invrl   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (c Pi0.◎ Pi0.sym⟷ c) ⟷ PathSpace {t₁} {t₁} Pi0.id⟷
    1invrr   : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace {t₁} {t₁} Pi0.id⟷ ⟷ PathSpace (c Pi0.◎ Pi0.sym⟷ c)
    1invinvl : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace (Pi0.sym⟷ (Pi0.sym⟷ c)) ⟷ PathSpace c
    1invinvr : {t₁ t₂ : Pi0.U•} {c : t₁ Pi0.⟷ t₂} →
              PathSpace c ⟷ PathSpace (Pi0.sym⟷ (Pi0.sym⟷ c))
    1tassocl : {t₁ t₂ t₃ t₄ : Pi0.U•}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃} {c₃ : t₃ Pi0.⟷ t₄} →
              PathSpace (c₁ Pi0.◎ (c₂ Pi0.◎ c₃)) ⟷
              PathSpace ((c₁ Pi0.◎ c₂) Pi0.◎ c₃)
    1tassocr : {t₁ t₂ t₃ t₄ : Pi0.U•}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃} {c₃ : t₃ Pi0.⟷ t₄} →
              PathSpace ((c₁ Pi0.◎ c₂) Pi0.◎ c₃) ⟷
              PathSpace (c₁ Pi0.◎ (c₂ Pi0.◎ c₃))
    -- resp◎ is closely related to Eckmann-Hilton
    1resp◎   : {t₁ t₂ t₃ : Pi0.U•}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃}
              {c₃ : t₁ Pi0.⟷ t₂} {c₄ : t₂ Pi0.⟷ t₃} →
              (PathSpace c₁ ⟷ PathSpace c₃) →
              (PathSpace c₂ ⟷ PathSpace c₄) →
              PathSpace (c₁ Pi0.◎ c₂) ⟷ PathSpace (c₃ Pi0.◎ c₄)

    -- 2groupoid combinators

    lidl    : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace (Pi1.id⟷ Pi1.◎ c) ⟷ 2PathSpace c
    lidr    : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace c ⟷ 2PathSpace (Pi1.id⟷ Pi1.◎ c)
    ridl    : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace (c Pi1.◎ Pi1.id⟷) ⟷ 2PathSpace c
    ridr    : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace c ⟷ 2PathSpace (c Pi1.◎ Pi1.id⟷)
    invll   : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace (Pi1.sym⟷ c Pi1.◎ c) ⟷ 2PathSpace {t₂} {t₂} Pi1.id⟷
    invlr   : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace {t₂} {t₂} Pi1.id⟷ ⟷ 2PathSpace (Pi1.sym⟷ c Pi1.◎ c)
    invrl   : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace (c Pi1.◎ Pi1.sym⟷ c) ⟷ 2PathSpace {t₁} {t₁} Pi1.id⟷
    invrr   : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace {t₁} {t₁} Pi1.id⟷ ⟷ 2PathSpace (c Pi1.◎ Pi1.sym⟷ c)
    invinvl : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace (Pi1.sym⟷ (Pi1.sym⟷ c)) ⟷ 2PathSpace c
    invinvr : {t₁ t₂ : Pi1.U•} {c : t₁ Pi1.⟷ t₂} →
              2PathSpace c ⟷ 2PathSpace (Pi1.sym⟷ (Pi1.sym⟷ c))
    tassocl : {t₁ t₂ t₃ t₄ : Pi1.U•}
              {c₁ : t₁ Pi1.⟷ t₂} {c₂ : t₂ Pi1.⟷ t₃} {c₃ : t₃ Pi1.⟷ t₄} →
              2PathSpace (c₁ Pi1.◎ (c₂ Pi1.◎ c₃)) ⟷
              2PathSpace ((c₁ Pi1.◎ c₂) Pi1.◎ c₃)
    tassocr : {t₁ t₂ t₃ t₄ : Pi1.U•}
              {c₁ : t₁ Pi1.⟷ t₂} {c₂ : t₂ Pi1.⟷ t₃} {c₃ : t₃ Pi1.⟷ t₄} →
              2PathSpace ((c₁ Pi1.◎ c₂) Pi1.◎ c₃) ⟷
              2PathSpace (c₁ Pi1.◎ (c₂ Pi1.◎ c₃))
    -- resp◎ is closely related to Eckmann-Hilton
    resp◎   : {t₁ t₂ t₃ : Pi1.U•}
              {c₁ : t₁ Pi1.⟷ t₂} {c₂ : t₂ Pi1.⟷ t₃}
              {c₃ : t₁ Pi1.⟷ t₂} {c₄ : t₂ Pi1.⟷ t₃} →
              (2PathSpace c₁ ⟷ 2PathSpace c₃) →
              (2PathSpace c₂ ⟷ 2PathSpace c₄) →
              2PathSpace (c₁ Pi1.◎ c₂) ⟷ 2PathSpace (c₃ Pi1.◎ c₄)

    -- commutative semiring combinators

    unite₊  : {t : U•} → •[ PLUS ZERO ∣ t ∣ , inj₂ (• t) ] ⟷ t
    uniti₊  : {t : U•} → t ⟷ •[ PLUS ZERO ∣ t ∣ , inj₂ (• t) ]
    swap1₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷
                             •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₂ (• t₁) ]
    swap2₊  : {t₁ t₂ : U•} → •[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷
                             •[ PLUS ∣ t₂ ∣ ∣ t₁ ∣ , inj₁ (• t₂) ]
    assocl1₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₁ (• t₁) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₁ (• t₁)) ]
    assocl2₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₁ (• t₂)) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₂ (• t₂)) ]
    assocl3₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₂ (• t₃)) ] ⟷
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₂ (• t₃) ]
    assocr1₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₁ (• t₁)) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₁ (• t₁) ]
    assocr2₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₁ (inj₂ (• t₂)) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₁ (• t₂)) ]
    assocr3₊ : {t₁ t₂ t₃ : U•} →
               •[ PLUS (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , inj₂ (• t₃) ] ⟷
               •[ PLUS ∣ t₁ ∣ (PLUS ∣ t₂ ∣ ∣ t₃ ∣) , inj₂ (inj₂ (• t₃)) ]
    unite⋆  : {t : U•} → •[ TIMES ONE ∣ t ∣ , (tt , • t) ] ⟷ t
    uniti⋆  : {t : U•} → t ⟷ •[ TIMES ONE ∣ t ∣ , (tt , • t) ]
    swap⋆   : {t₁ t₂ : U•} → •[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂) ] ⟷
                             •[ TIMES ∣ t₂ ∣ ∣ t₁ ∣ , (• t₂ , • t₁) ]
    assocl⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ] ⟷
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ]
    assocr⋆ : {t₁ t₂ t₃ : U•} →
           •[ TIMES (TIMES ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , ((• t₁ , • t₂) , • t₃) ] ⟷
           •[ TIMES ∣ t₁ ∣ (TIMES ∣ t₂ ∣ ∣ t₃ ∣) , (• t₁ , (• t₂ , • t₃)) ]
    distz : {t : U•} {absurd : ⟦ ZERO ⟧} →
            •[ TIMES ZERO ∣ t ∣ , (absurd , • t) ] ⟷ •[ ZERO , absurd ]
    factorz : {t : U•} {absurd : ⟦ ZERO ⟧} →
            •[ ZERO , absurd ] ⟷ •[ TIMES ZERO ∣ t ∣ , (absurd , • t) ]
    dist1   : {t₁ t₂ t₃ : U•} →
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₁ (• t₁) , • t₃) ] ⟷
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₁ (• t₁ , • t₃) ]
    dist2   : {t₁ t₂ t₃ : U•} →
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₂ (• t₂) , • t₃) ] ⟷
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₂ (• t₂ , • t₃) ]
    factor1   : {t₁ t₂ t₃ : U•} →
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₁ (• t₁ , • t₃) ] ⟷
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₁ (• t₁) , • t₃) ]
    factor2   : {t₁ t₂ t₃ : U•} →
              •[ PLUS (TIMES ∣ t₁ ∣ ∣ t₃ ∣) (TIMES ∣ t₂ ∣ ∣ t₃ ∣) ,
                 inj₂ (• t₂ , • t₃) ] ⟷
              •[ TIMES (PLUS ∣ t₁ ∣ ∣ t₂ ∣) ∣ t₃ ∣ , (inj₂ (• t₂) , • t₃) ]
    _⊕1_   : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
             (•[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₁ (• t₁) ] ⟷
              •[ PLUS ∣ t₃ ∣ ∣ t₄ ∣ , inj₁ (• t₃) ])
    _⊕2_   : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
             (•[ PLUS ∣ t₁ ∣ ∣ t₂ ∣ , inj₂ (• t₂) ] ⟷
              •[ PLUS ∣ t₃ ∣ ∣ t₄ ∣ , inj₂ (• t₄) ])
    _⊗_     : {t₁ t₂ t₃ t₄ : U•} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) →
            (•[ TIMES ∣ t₁ ∣ ∣ t₂ ∣ , (• t₁ , • t₂ ) ] ⟷
             •[ TIMES ∣ t₃ ∣ ∣ t₄ ∣ , (• t₃ , • t₄ ) ])

  -- proof that we have a 2Groupoid structure; this is 1Groupoid whose
  -- equivalences are themselves a 1Groupoid

  G : 1Groupoid
  G = record
        { set = Pi1.U•
        ; _↝_ = Pi1._⟷_
        ; _≈_ = λ c₀ c₁ → 2PathSpace c₀ ⟷ 2PathSpace c₁
        ; id = Pi1.id⟷
        ; _∘_ = λ c₀ c₁ → c₁ Pi1.◎ c₀
        ; _⁻¹ = Pi1.sym⟷
        ; lneutr = λ _ → ridl
        ; rneutr = λ _ → lidl
        ; assoc = λ _ _ _ → tassocl
        ; equiv = record { refl = id⟷
                                ; sym = λ c → sym⟷ c
                                ; trans = λ c₀ c₁ → c₀ ◎ c₁ }
        ; linv = λ _ → invrl
        ; rinv = λ _ → invll
        ; ∘-resp-≈ = λ f⟷h g⟷i → resp◎ g⟷i f⟷h
        }

  -- examples

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

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import HoTT
open import cohomology.ChainComplex
open import cohomology.Theory
open import groups.KernelImage
open import cw.CW

module cw.cohomology.ReconstructedZerothCohomologyGroup {i : ULevel} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  import cw.cohomology.TipCoboundary OT as TC
  import cw.cohomology.TipAndAugment OT as TAA
  open import cw.cohomology.Descending OT
  open import cw.cohomology.ReconstructedCochainComplex OT
  import cw.cohomology.ZerothCohomologyGroup OT as ZCG
  import cw.cohomology.ZerothCohomologyGroupOnDiag OT as ZCGD

  private
    ≤-dec-has-all-paths : {m n : ℕ} → has-all-paths (Dec (m ≤ n))
    ≤-dec-has-all-paths = prop-has-all-paths (Dec-level ≤-is-prop)

  private
    abstract
      zeroth-cohomology-group-descend : ∀ {n} (⊙skel : ⊙Skeleton {i} (2 + n))
        →  cohomology-group (cochain-complex ⊙skel) 0
        == cohomology-group (cochain-complex (⊙cw-init ⊙skel)) 0
      zeroth-cohomology-group-descend {n = O} ⊙skel
        = ap
            (λ δ → Ker/Im δ
              (TAA.cw-coε (⊙cw-take (lteSR lteS) ⊙skel))
              (TAA.C2×CX₀-is-abelian (⊙cw-take (lteSR lteS) ⊙skel) 0))
            (coboundary-first-template-descend-from-two ⊙skel)
      zeroth-cohomology-group-descend {n = S n} ⊙skel
        = ap (λ δ → Ker/Im δ
                (TAA.cw-coε (⊙cw-take (inr (O<S (2 + n))) ⊙skel))
                (TAA.C2×CX₀-is-abelian (⊙cw-take (inr (O<S (2 + n))) ⊙skel) 0))
            (coboundary-first-template-descend-from-far ⊙skel (O<S (1 + n)) (<-+-l 1 (O<S n)))

      zeroth-cohomology-group-β : ∀ (⊙skel : ⊙Skeleton {i} 1)
        →  cohomology-group (cochain-complex ⊙skel) 0
        == Ker/Im
            (TC.cw-co∂-head ⊙skel)
            (TAA.cw-coε (⊙cw-init ⊙skel))
            (TAA.C2×CX₀-is-abelian (⊙cw-init ⊙skel) 0)
      zeroth-cohomology-group-β ⊙skel
        = ap
            (λ δ → Ker/Im δ
              (TAA.cw-coε (⊙cw-init ⊙skel))
              (TAA.C2×CX₀-is-abelian (⊙cw-init ⊙skel) 0))
            (coboundary-first-template-β ⊙skel)

  abstract
    zeroth-cohomology-group : ∀ {n} (⊙skel : ⊙Skeleton {i} n)
      → ⊙has-cells-with-choice 0 ⊙skel i
      → C 0 ⊙⟦ ⊙skel ⟧ ≃ᴳ cohomology-group (cochain-complex ⊙skel) 0
    zeroth-cohomology-group {n = 0} ⊙skel ac = ZCGD.C-cw-iso-ker/im ⊙skel ac
    zeroth-cohomology-group {n = 1} ⊙skel ac =
          coe!ᴳ-iso (zeroth-cohomology-group-β ⊙skel)
      ∘eᴳ ZCG.C-cw-iso-ker/im ⊙skel ac
    zeroth-cohomology-group {n = S (S n)} ⊙skel ac =
          coe!ᴳ-iso (zeroth-cohomology-group-descend ⊙skel)
      ∘eᴳ zeroth-cohomology-group (⊙cw-init ⊙skel) (⊙init-has-cells-with-choice ⊙skel ac)
      ∘eᴳ C-cw-descend-at-lower ⊙skel (O<S n) ac

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

module Calf.Types.Sum where

open import Calf.Prelude
open import Calf.Metalanguage

open import Data.Sum using (_⊎_; inj₁; inj₂) public

sum : tp pos → tp pos → tp pos
sum A B = U (meta (val A ⊎ val B))

sum/case : ∀ A B (X : val (sum A B) → tp neg) → (s : val (sum A B)) → ((a : val A) → cmp (X (inj₁ a))) → ((b : val B) → cmp (X (inj₂ b))) → cmp (X s)
sum/case A B X (inj₁ x) b₁ _  = b₁ x
sum/case A B X (inj₂ x) _  b₂ = b₂ x

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

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

open import Cubical.HITs.FiniteMultiset.Base

private
  variable
    A : Type₀

infixr 30 _++_

_++_ : ∀ (xs ys : FMSet A) → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs zs p q i j ++ ys =
  trunc (xs ++ ys) (zs ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

unitl-++ : ∀ (xs : FMSet A) → [] ++ xs ≡ xs
unitl-++ xs = refl

unitr-++ : ∀ (xs : FMSet A) → xs ++ [] ≡ xs
unitr-++ = FMSetElimProp.f (trunc _ _)
  refl
  (λ x p → cong (_∷_ x) p)

assoc-++ : ∀ (xs ys zs : FMSet A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ = FMSetElimProp.f (propPi (λ _ → propPi (λ _ → trunc _ _)))
  (λ ys zs → refl)
  (λ x p ys zs → cong (_∷_ x) (p ys zs))

cons-++ : ∀ (x : A) (xs : FMSet A) → x ∷ xs ≡ xs ++ [ x ]
cons-++ x = FMSetElimProp.f (trunc _ _)
  refl
  (λ y {xs} p → comm x y xs ∙ cong (_∷_ y) p)

comm-++ : ∀ (xs ys : FMSet A) → xs ++ ys ≡ ys ++ xs
comm-++ = FMSetElimProp.f (propPi (λ _ → trunc _ _))
  (λ ys → sym (unitr-++ ys))
  (λ x {xs} p ys → cong (x ∷_) (p ys)
                 ∙ cong (_++ xs) (cons-++ x ys)
                 ∙ sym (assoc-++ ys [ x ] xs))

module FMSetUniversal {ℓ} {M : Type ℓ} (MSet : isSet M)
  (e : M) (_⊗_ : M → M → M)
  (comm-⊗ : ∀ x y → x ⊗ y ≡ y ⊗ x) (assoc-⊗ : ∀ x y z → x ⊗ (y ⊗ z) ≡ (x ⊗ y) ⊗ z)
  (unit-⊗ : ∀ x → e ⊗ x ≡ x)
  (f : A → M) where

  f-extend : FMSet A → M
  f-extend = FMSetRec.f MSet e (λ x m → f x ⊗ m)
         (λ x y m → comm-⊗ (f x) (f y ⊗ m) ∙ sym (assoc-⊗ (f y) m (f x)) ∙ cong (f y ⊗_) (comm-⊗ m (f x)))

  f-extend-nil : f-extend [] ≡ e
  f-extend-nil = refl

  f-extend-cons : ∀ x xs → f-extend (x ∷ xs) ≡ f x ⊗ f-extend xs
  f-extend-cons x xs = refl

  f-extend-sing : ∀ x → f-extend [ x ] ≡ f x
  f-extend-sing x = comm-⊗ (f x) e ∙ unit-⊗ (f x)

  f-extend-++ : ∀ xs ys → f-extend (xs ++ ys) ≡ f-extend xs ⊗ f-extend ys
  f-extend-++ = FMSetElimProp.f (propPi λ _ → MSet _ _)
    (λ ys → sym (unit-⊗ (f-extend ys)))
    (λ x {xs} p ys → cong (f x ⊗_) (p ys) ∙ assoc-⊗ (f x) (f-extend xs) (f-extend ys))

  module _ (h : FMSet A → M) (h-nil : h [] ≡ e) (h-sing : ∀ x → h [ x ] ≡ f x)
           (h-++ : ∀ xs ys → h (xs ++ ys) ≡ h xs ⊗ h ys) where

    f-extend-unique : h ≡ f-extend
    f-extend-unique = funExt (FMSetElimProp.f (MSet _ _)
                              h-nil
                              (λ x {xs} p → (h-++ [ x ] xs) ∙ cong (_⊗ h xs) (h-sing x) ∙ cong (f x ⊗_) p))

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

data C (A : Set) : Set where
  c : (x : A) → C A

data D : Set where

data E (A : Set) : Set where
  e : A → E A

postulate
  F : {A : Set} → A → Set

G : {A : Set} → C A → Set
G (c x) = E (F x)

postulate
  H : {A : Set} → (A → Set) → C A → Set
  f : {A : Set} {P : A → Set} {y : C A} → H P y → (x : A) → G y → P x
  g : {A : Set} {y : C A} {P : A → Set} → ((x : A) → G y → P x) → H P y

variable
  A : Set
  P : A → Set
  x : A
  y : C A

postulate
  h : {p : ∀ x → G y → P x} → (∀ x (g : G y) → F (p x g)) → F (g p)

id : (A : Set) → A → A
id _ x = x

-- i : (h : H P y) → (∀ x (g : G y) → F (f h x g)) → F (g (f h))
-- i x y = id (F (g (f x))) (h y)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --guardedness #-}

import Tutorials.Monday-Complete
import Tutorials.Tuesday-Complete
import Tutorials.Wednesday-Complete
import Tutorials.Thursday-Complete

max_stars_repo_name: poncev/agda-bcam

max_issues_repo_name: poncev/agda-bcam

max_forks_repo_name: poncev/agda-bcam


text:
open import Agda.Builtin.Equality

postulate
  A : Set
  B : A → Set

variable
  a : A
  b : B a

postulate
  C : B a → Set

postulate
  f : (b : B a) → {!!}
  g : (c : C b) → {!!}

module _ (a′ : A) where
  postulate
    h : (b : B a) (b′ : B a′) → {!!}
    j : (b′ : B a) (c : C b) (c′ : C b′) → {!!}