text:
{-
This file contains a proof of the fact that the Brunerie number,
i.e. absolute value of the Hopf invariant of [e , e] : π₃S², is 2.
Here, e is the generator of π₂S² and [_,_] denotes the Whitehead
product. The proof follows Proposition 5.4.4. in Brunerie (2016)
closely, but, for simplicity, considers only the case n = 2.
-}

{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.HopfInvariant.Brunerie where

open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
open import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso
open import Cubical.Homotopy.Whitehead

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.SphereProduct
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma
open import Cubical.Data.Int hiding (_+'_)
open import Cubical.Data.Nat hiding (_+_)
open import Cubical.Data.Unit
open import Cubical.Data.Sum renaming (rec to ⊎rec)

open import Cubical.HITs.Pushout
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Join
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.Truncation
open import Cubical.HITs.SetTruncation
  renaming (elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation
  renaming (map to pMap ; rec to pRec)

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.Unit

open Iso
open IsGroupHom
open PlusBis

-- Some abstract versions of imported lemmas/definitions from
-- ZCohomology.Groups.SphereProduct for faster type checking.
abstract
  H²-genₗabs : coHom 2 (S₊ 2 × S₊ 2)
  H²-genₗabs = H²-S²×S²-genₗ

  H²-genᵣabs : coHom 2 (S₊ 2 × S₊ 2)
  H²-genᵣabs = H²-S²×S²-genᵣ

  Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs : (n m : ℕ)
    → GroupIso (coHomGr ((suc n) +' (suc m))
                    (S₊ (suc n) × S₊ (suc m)))
                ℤGroup
  Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs = Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ

  Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs≡ : (n m : ℕ)
    → Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs n m ≡ Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ n m
  Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs≡ n m = refl

  Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-⌣ :
      fun (fst (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1))
          (H²-S²×S²-genₗ ⌣ H²-S²×S²-genᵣ)
    ≡ 1
  Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-⌣ =
     fun (fst (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1)) (H²-S²×S²-genₗ ⌣ H²-S²×S²-genᵣ)
    ≡⟨ cong (fun (fst (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1))) (sym H²-S²≅H⁴-S²×S²⌣) ⟩
    fun (fst (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1)) (fun (fst (H²-S²≅H⁴-S²×S²)) ∣ ∣_∣ₕ ∣₂)
    ≡⟨ speedUp ∣_∣ₕ ⟩
    fun (fst (Hⁿ-Sⁿ≅ℤ 1)) ∣ ∣_∣ₕ ∣₂
    ≡⟨ refl ⟩ -- Computation! :-)
    1 ∎
    where
    speedUp : (f : _) →
         fun (fst (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1)) (fun (fst (H²-S²≅H⁴-S²×S²)) ∣ f ∣₂)
       ≡ fun (fst (Hⁿ-Sⁿ≅ℤ 1)) ∣ f ∣₂
    speedUp f i =
      fun (fst (Hⁿ-Sⁿ≅ℤ 1)) (leftInv (fst H²-S²≅H⁴-S²×S²) ∣ f ∣₂ i)

-- Some abbreviations
private
  inl' : S₊ 2 × S₊ 2 → Pushout⋁↪fold⋁ (S₊∙ 2)
  inl' = inl

  qHom : GroupHom (coHomGr 4 (Pushout⋁↪fold⋁ (S₊∙ 2)))
                  (coHomGr 4 (S₊ 2 × S₊ 2))
  qHom = coHomMorph 4 inl'

  qHomGen : (n : ℕ) →
         GroupHom (coHomGr n (Pushout⋁↪fold⋁ (S₊∙ 2)))
                  (coHomGr n (S₊ 2 × S₊ 2))
  qHomGen n = coHomMorph n inl'

-- The type C and generator α, β in dim 2 and 4 respectively
-- Recall, the goal is to prove that α ⌣ α = ±2 β
  CHopf : Type
  CHopf = HopfInvariantPush 0 fold∘W

  Hopfαfold∘W = Hopfα 0 (fold∘W , refl)
  Hopfβfold∘W = Hopfβ 0 (fold∘W , refl)

-- Rewriting CHopf as our favourite pushout
-- S²×S² ← S²∨S² → S²
  CHopfIso : Iso CHopf (Pushout⋁↪fold⋁ (S₊∙ 2))
  CHopfIso =
    compIso (invIso (equivToIso
      (compEquiv (compEquiv pushoutSwitchEquiv
        (isoToEquiv (PushoutDistr.PushoutDistrIso fold⋁ W λ _ → tt)))
            pushoutSwitchEquiv)))
            (equivToIso Pushout-coFibW-fold⋁≃Pushout⋁↪fold⋁)

-- Cohomology group version of the Iso
  coHomCHopfIso : (n : ℕ)
    → GroupIso (coHomGr n CHopf) (coHomGr n (Pushout⋁↪fold⋁ (S₊∙ 2)))
  coHomCHopfIso n = invGroupIso (coHomIso n CHopfIso)

-- We instantiate Mayer-Vietoris for the pushout
module MV-⋁↪-fold⋁ = MV _ _ (S₊∙ 2 ⋁ S₊∙ 2) ⋁↪ fold⋁

-- This give us an iso H⁴(S²×S² ← S²∨S² → S²) ≅ H⁴(S²×S²)
isEquiv-qHom : GroupEquiv (coHomGr 4 (Pushout⋁↪fold⋁ (S₊∙ 2)))
                (coHomGr 4 (S₊ 2 × S₊ 2))
fst (fst isEquiv-qHom) = qHom .fst
snd (fst isEquiv-qHom) =
  subst isEquiv
    (funExt (sElim (λ _ → isSetPathImplicit) (λ _ → refl)))
    (×UnitEquiv (isoToPath
      (invIso
        (fst (Hⁿ-Sᵐ≅0 3 1 λ p → snotz (cong predℕ p)))))
           _ isEquiv-i)
  where
  ×UnitEquiv : {A B C : Type}
         → Unit ≡ C
         → (f : A → B × C)
         → isEquiv f
         → isEquiv (fst ∘ f)
  ×UnitEquiv {A = A} {B = B} =
    J (λ C _ → (f : A → B × C) → isEquiv f → isEquiv (fst ∘ f))
      λ f eq → record { equiv-proof =
        λ b → ((fst (fst (equiv-proof eq (b , tt))))
          , cong fst (fst (equiv-proof eq (b , tt)) .snd))
          , λ y → ΣPathP ((cong fst (equiv-proof eq (b , tt)
                                      .snd ((fst y)
            , ΣPathP ((snd y) , refl))))
            , λ i j → equiv-proof eq (b , tt) .snd ((fst y)
            , ΣPathP ((snd y) , refl)) i .snd j .fst) }

  isEquiv-i : isEquiv (fst (MV-⋁↪-fold⋁.i 4))
  isEquiv-i =
    SES→isEquiv
      (isContr→≡UnitGroup
        (isOfHLevelRetractFromIso 0
          (compIso
            (fst (Hⁿ-⋁ (S₊∙ 2) (S₊∙ 2) 2))
            (compIso
              (prodIso (fst (Hⁿ-Sᵐ≅0 2 1 λ p → snotz (cong predℕ p)))
                       (fst (Hⁿ-Sᵐ≅0 2 1 λ p → snotz (cong predℕ p))))
              rUnit×Iso))
          isContrUnit))
      ((isContr→≡UnitGroup
        (isOfHLevelRetractFromIso 0
          (compIso
            (fst (Hⁿ-⋁ (S₊∙ 2) (S₊∙ 2) 3))
            (compIso
              (prodIso (fst (Hⁿ-Sᵐ≅0 3 1 λ p → snotz (cong predℕ p)))
                       (fst (Hⁿ-Sᵐ≅0 3 1 λ p → snotz (cong predℕ p))))
              rUnit×Iso))
          isContrUnit)))
      (MV-⋁↪-fold⋁.d 3)
      (MV-⋁↪-fold⋁.i 4)
      (MV-⋁↪-fold⋁.Δ 4)
      (MV-⋁↪-fold⋁.Ker-i⊂Im-d 3)
      (MV-⋁↪-fold⋁.Ker-Δ⊂Im-i 4)
snd isEquiv-qHom = qHom .snd

-- The goal now is reducing α ⌣ α = ±2 β to gₗ ⌣ gᵣ = e for
-- gₗ, gᵣ generators of H²(S²×S²) ≅ ℤ × ℤ and e generator of
-- H⁴(S²×S²) ≅ ℤ. This essentially just elementary linear algebra at
-- this point. We do it for an arbitrary (well-behaved) iso
-- H⁴(S²×S²) ≅ ℤ in order to speed up type checking.
module BrunerieNumLem
  (is : GroupIso (coHomGr 4 (S₊ 2 × S₊ 2)) ℤGroup)
  (isEq : (fun (fst is) (H²-S²×S²-genₗ ⌣ H²-S²×S²-genᵣ) ≡ 1)) where

  x = H²-S²×S²-genₗ
  y = H²-S²×S²-genᵣ

  α = Hopfαfold∘W
  β = Hopfβfold∘W

  α' : coHom 2 (Pushout⋁↪fold⋁ (S₊∙ 2))
  α' = fun (fst (coHomCHopfIso 2)) α

  β' : coHom 4 (Pushout⋁↪fold⋁ (S₊∙ 2))
  β' = fun (fst (coHomCHopfIso 4)) β

  rewriteEquation :
       (α' ⌣ α' ≡ β' +ₕ β') ⊎ (α' ⌣ α' ≡ -ₕ (β' +ₕ β'))
    → (α ⌣ α ≡ β +ₕ β) ⊎ (α ⌣ α ≡ -ₕ (β +ₕ β))
  rewriteEquation (inl x) =
    inl ((λ i → leftInv (fst (coHomCHopfIso 2)) α (~ i)
               ⌣ leftInv (fst (coHomCHopfIso 2)) α (~ i))
       ∙∙ cong (inv (fst (coHomCHopfIso 4))) x
       ∙∙ leftInv (fst (coHomCHopfIso 4)) (β +ₕ β))
  rewriteEquation (inr x) =
    inr ((λ i → leftInv (fst (coHomCHopfIso 2)) α (~ i)
               ⌣ leftInv (fst (coHomCHopfIso 2)) α (~ i))
      ∙∙ cong (inv (fst (coHomCHopfIso 4))) x
      ∙∙ leftInv (fst (coHomCHopfIso 4))
           (-ₕ (β +ₕ β)))

  rewriteEquation2 : (qHom .fst β' ≡  x ⌣ y) ⊎ (qHom .fst β' ≡  -ₕ (x ⌣ y))
  rewriteEquation2 =
    ⊎rec
      (λ p → inl (sym (leftInv (fst is) (qHom .fst β'))
                ∙∙ cong (inv (fst is)) (p ∙ sym isEq)
                ∙∙ leftInv (fst is) (x ⌣ y)))
      (λ p → inr (sym (leftInv (fst is) (qHom .fst β'))
               ∙∙ cong (inv (fst is))
                    (p ∙ sym (cong (GroupStr.inv (snd ℤGroup)) isEq))
               ∙∙ (presinv (invGroupIso is .snd) (fun (fst is) (x ⌣ y))
                 ∙ cong -ₕ_ (leftInv (fst is) (x ⌣ y)))))
      eqs
    where
    grIso : GroupEquiv (coHomGr 4 (HopfInvariantPush 0 fold∘W)) ℤGroup
    grIso = compGroupEquiv (GroupIso→GroupEquiv (coHomCHopfIso 4))
          (compGroupEquiv
            isEquiv-qHom
            (GroupIso→GroupEquiv is))

    eqs : (fst (fst grIso) β ≡ 1) ⊎ (fst (fst grIso) β ≡ -1)
    eqs = groupEquivPresGen _ (GroupIso→GroupEquiv (Hopfβ-Iso 0 (fold∘W , refl)))
          β (inl (Hopfβ↦1 0 (fold∘W , refl))) grIso

  qpres⌣ : (x y : coHom 2 _)
    → fst qHom (x ⌣ y) ≡ fst (qHomGen 2) x ⌣ fst (qHomGen 2) y
  qpres⌣ = sElim2 (λ _ _ → isSetPathImplicit) λ _ _ → refl

  α'↦x+y : fst (qHomGen 2) α' ≡ x +ₕ y
  α'↦x+y = lem ((coHomFun 2 (inv CHopfIso) α)) refl
    where
    lem : (x' : coHom 2 (Pushout⋁↪fold⋁ (S₊∙ 2)))
        → coHomFun 2 inr x' ≡ ∣ ∣_∣ ∣₂
        → fst (qHomGen 2) x' ≡ x +ₕ y
    lem = sElim (λ _ → isSetΠ λ _ → isSetPathImplicit)
      λ f p → Cubical.HITs.PropositionalTruncation.rec
        (squash₂ _ _)
        (λ r → cong ∣_∣₂ (funExt (uncurry
          (wedgeconFun 1 1 (λ _ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _)
            (λ x → cong f (push (inr x)) ∙∙ funExt⁻ r x ∙∙ refl)
            ((λ x → cong f (push (inl x)) ∙∙ funExt⁻ r x ∙∙ sym (rUnitₖ 2 ∣ x ∣ₕ)))
            (cong (_∙∙ funExt⁻ r north ∙∙ refl)
              (cong (cong f) λ j i → push (push tt j) i))))))
        (fun PathIdTrunc₀Iso p)

  mainEq : ((fst qHom) (α' ⌣ α') ≡ qHom .fst (β' +ₕ β'))
         ⊎ ((fst qHom) (α' ⌣ α') ≡ qHom .fst (-ₕ (β' +ₕ β')))
  mainEq =
    ⊎rec
      (λ id → inl (lem₁ ∙ lem₂
                  ∙ cong (λ x → x +ₕ x) (sym id)
                  ∙ sym (pres· (snd qHom) β' β')))
      (λ id → inr (lem₁ ∙ lem₂
                 ∙ ((sym (distLem (x ⌣ y))
                 ∙ cong -ₕ_ (cong (λ x → x +ₕ x) (sym id)))
                 ∙ cong (-ₕ_) (pres· (snd qHom) β' β'))
                 ∙ sym (presinv (snd qHom) (β' +ₕ β'))))
      rewriteEquation2
    where
    triv⌣ : (a : S¹)
      → cong₂ (_⌣ₖ_ {n = 2} {m = 2}) (cong ∣_∣ₕ (merid a)) (cong ∣_∣ₕ (merid a))
       ≡ λ _ → ∣ north ∣ₕ
    triv⌣ a =
      cong₂Funct (_⌣ₖ_ {n = 2} {m = 2})
        (cong ∣_∣ₕ (merid a)) (cong ∣_∣ₕ (merid a))
        ∙ sym (rUnit λ j → _⌣ₖ_ {n = 2} {m = 2} ∣ merid a j ∣ₕ ∣ north ∣)
        ∙ (λ i j → ⌣ₖ-0ₖ 2 2 ∣ merid a j ∣ₕ i)

    distLem : (x : coHom 4 (S₊ 2 × S₊ 2)) → -ₕ ((-ₕ x) +ₕ (-ₕ x)) ≡ x +ₕ x
    distLem =
      sElim (λ _ → isSetPathImplicit)
        λ f → cong ∣_∣₂ (funExt λ x → cong -ₖ_ (sym (-distrₖ 4 (f x) (f x)))
                       ∙ -ₖ^2  (f x +ₖ f x))

    x⌣x≡0 : x ⌣ x ≡ 0ₕ 4
    x⌣x≡0 =
      cong ∣_∣₂
       (funExt (uncurry λ { north y → refl
                          ; south y → refl
                          ; (merid a i) y j → triv⌣ a j i}))

    y⌣y≡0 : y ⌣ y ≡ 0ₕ 4
    y⌣y≡0 =
      cong ∣_∣₂
       (funExt (uncurry λ { x north → refl
                          ; x south → refl
                          ; x (merid a i) j → triv⌣ a j i}))

    -ₕ'Id : (x : coHom 4 (S₊ 2 × S₊ 2)) → (-ₕ'^ 2 · 2) x ≡ x
    -ₕ'Id =
      sElim (λ _ → isSetPathImplicit)
         λ f → cong ∣_∣₂ (funExt λ x → -ₖ'-gen-inl-left 2 2 tt (inl tt) (f x))

    y⌣x≡x⌣y : y ⌣ x ≡ x ⌣ y
    y⌣x≡x⌣y =
      y ⌣ x                                 ≡⟨ gradedComm'-⌣ 2 2 y x ⟩
      (-ₕ'^ 2 · 2) (transport refl (x ⌣ y))  ≡⟨ -ₕ'Id (transport refl (x ⌣ y)) ⟩
      transport refl (x ⌣ y)                ≡⟨ transportRefl (x ⌣ y) ⟩
      x ⌣ y ∎

    lem₂ : (x +ₕ y) ⌣ (x +ₕ y) ≡ (x ⌣ y) +ₕ (x ⌣ y)
    lem₂ =
     (x +ₕ y) ⌣ (x +ₕ y)                       ≡⟨ leftDistr-⌣ 2 2 (x +ₕ y) x y ⟩
     ((x +ₕ y) ⌣ x) +ₕ ((x +ₕ y) ⌣ y)          ≡⟨ cong₂ _+ₕ_ (rightDistr-⌣ 2 2 x y x) (rightDistr-⌣ 2 2 x y y) ⟩
     ((x ⌣ x +ₕ y ⌣ x)) +ₕ (x ⌣ y +ₕ y ⌣ y)    ≡⟨ cong₂ _+ₕ_ (cong (_+ₕ y ⌣ x) x⌣x≡0 ∙ lUnitₕ 4 (y ⌣ x))
                                                             (cong (x ⌣ y +ₕ_) y⌣y≡0 ∙ rUnitₕ 4 (x ⌣ y)) ⟩
     y ⌣ x +ₕ x ⌣ y                            ≡⟨ cong (_+ₕ (x ⌣ y)) y⌣x≡x⌣y ⟩
     ((x ⌣ y) +ₕ (x ⌣ y)) ∎

    lem₁ : (fst qHom) (α' ⌣ α') ≡ (x +ₕ y) ⌣ (x +ₕ y)
    lem₁ =
     fst qHom (α' ⌣ α')                        ≡⟨ refl ⟩
     fst (qHomGen 2) α' ⌣ fst (qHomGen 2) α'   ≡⟨ cong (λ x → x ⌣ x) α'↦x+y ⟩
     ((x +ₕ y) ⌣ (x +ₕ y)) ∎

  main⊎ : (HopfInvariant 0 (fold∘W , refl) ≡ 2)
        ⊎ (HopfInvariant 0 (fold∘W , refl) ≡ -2)
  main⊎ =
    ⊎rec (λ p → inl (lem₁
                   ∙ cong (fun (fst (Hopfβ-Iso 0 (fold∘W , refl)))) p
                   ∙ pres· (Hopfβ-Iso 0 (fold∘W , refl) .snd) β β
                   ∙ cong (λ x → x + x) (Hopfβ↦1 0 (fold∘W , refl))))
         (λ p → inr (lem₁
                   ∙ cong (fun (fst (Hopfβ-Iso 0 (fold∘W , refl)))) p
                   ∙ presinv (Hopfβ-Iso 0 (fold∘W , refl) .snd) (β +ₕ β)
                   ∙ cong (GroupStr.inv (snd ℤGroup))
                          (pres· (Hopfβ-Iso 0 (fold∘W , refl) .snd) β β
                         ∙ cong (λ x → x + x) (Hopfβ↦1 0 (fold∘W , refl)))))
         lem₂
    where
    lem₁ : HopfInvariant 0 (fold∘W , refl)
       ≡ fun (fst (Hopfβ-Iso 0 (fold∘W , refl))) (α ⌣ α)
    lem₁ =
      cong (fun (fst (Hopfβ-Iso 0 (fold∘W , refl)))) (transportRefl (α ⌣ α))

    lem₂ : (α ⌣ α ≡ β +ₕ β) ⊎ (α ⌣ α ≡ -ₕ (β +ₕ β))
    lem₂ =
      rewriteEquation
      (⊎rec (λ p → inl (sym (retEq (fst isEquiv-qHom) (α' ⌣ α'))
                              ∙∙ cong (invEq (fst isEquiv-qHom)) p
                              ∙∙ retEq (fst isEquiv-qHom) (β' +ₕ β')))
             (λ p → inr ((sym (retEq (fst isEquiv-qHom) (α' ⌣ α'))
                       ∙∙ cong (invEq (fst isEquiv-qHom)) p
                       ∙∙ retEq (fst isEquiv-qHom) (-ₕ (β' +ₕ β')))))
             mainEq)

  main : abs (HopfInvariant 0 (fold∘W , refl)) ≡ 2
  main = ⊎→abs _ 2 main⊎

-- We instantiate the module
Brunerie'≡2 : abs (HopfInvariant 0 (fold∘W , refl)) ≡ 2
Brunerie'≡2 = BrunerieNumLem.main (Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-abs 1 1) Hⁿ⁺ᵐ-Sⁿ×Sᵐ≅ℤ-⌣

-- We rewrite the it slightly, to get the definition of the Brunerie
-- number in Brunerie (2016)
Brunerie'≡Brunerie : [ ∣ idfun∙ (S₊∙ 2) ∣₂ ∣ ∣ idfun∙ (S₊∙ 2) ∣₂ ]π' ≡ ∣ fold∘W , refl ∣₂
Brunerie'≡Brunerie =
    cong ∣_∣₂ ([]≡[]₂ (idfun∙ (S₊∙ 2)) (idfun∙ (S₊∙ 2)) )
  ∙ sym fold∘W≡Whitehead
  ∙ cong ∣_∣₂ (∘∙-idˡ (fold∘W , refl))

-- And we get the main result
Brunerie≡2 : Brunerie ≡ 2
Brunerie≡2 =
  cong abs (cong (HopfInvariant-π' 0) Brunerie'≡Brunerie)
  ∙ Brunerie'≡2

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise equality over lists parameterised by a setoid
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where

open import Data.Fin.Base
open import Data.List.Base
open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
open import Data.List.Relation.Unary.Unique.Setoid S using (Unique)
open import Function using (_∘_)
open import Level
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
open import Relation.Unary as U using (Pred)

open Setoid S renaming (Carrier to A)

private
  variable
    p q : Level

------------------------------------------------------------------------
-- Definition of equality
------------------------------------------------------------------------

infix 4 _≋_

_≋_ : Rel₂ (List A) (a ⊔ ℓ)
_≋_ = Pointwise _≈_

open PW public
  using ([]; _∷_)

------------------------------------------------------------------------
-- Relational properties
------------------------------------------------------------------------

≋-refl : Reflexive _≋_
≋-refl = PW.refl refl

≋-reflexive : _≡_ ⇒ _≋_
≋-reflexive P.refl = ≋-refl

≋-sym : Symmetric _≋_
≋-sym = PW.symmetric sym

≋-trans : Transitive _≋_
≋-trans = PW.transitive trans

≋-isEquivalence : IsEquivalence _≋_
≋-isEquivalence = PW.isEquivalence isEquivalence

≋-setoid : Setoid _ _
≋-setoid = PW.setoid S

------------------------------------------------------------------------
-- Relationships to predicates
------------------------------------------------------------------------

open PW public
  using () renaming
  ( Any-resp-Pointwise      to Any-resp-≋
  ; All-resp-Pointwise      to All-resp-≋
  ; AllPairs-resp-Pointwise to AllPairs-resp-≋
  )

Unique-resp-≋ : Unique Respects _≋_
Unique-resp-≋ = AllPairs-resp-≋ ≉-resp₂

------------------------------------------------------------------------
-- List operations
------------------------------------------------------------------------

------------------------------------------------------------------------
-- length

≋-length : ∀ {xs ys} → xs ≋ ys → length xs ≡ length ys
≋-length = PW.Pointwise-length

------------------------------------------------------------------------
-- map

module _ {b ℓ₂} (T : Setoid b ℓ₂) where

  open Setoid T using () renaming (_≈_ to _≈′_)
  private
    _≋′_ = Pointwise _≈′_

  map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ →
         ∀ {xs ys} → xs ≋ ys → map f xs ≋′ map f ys
  map⁺ {f} pres xs≋ys = PW.map⁺ f f (PW.map pres xs≋ys)

------------------------------------------------------------------------
-- _++_

++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
++⁺ = PW.++⁺

++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs
++-cancelˡ = PW.++-cancelˡ

++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≋ zs ++ xs → ys ≋ zs
++-cancelʳ = PW.++-cancelʳ

------------------------------------------------------------------------
-- concat

concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss
concat⁺ = PW.concat⁺

------------------------------------------------------------------------
-- tabulate

tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
            (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g
tabulate⁺ = PW.tabulate⁺

tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
            tabulate f ≋ tabulate g → (∀ i → f i ≈ g i)
tabulate⁻ = PW.tabulate⁻

------------------------------------------------------------------------
-- filter

module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_)
  where

  filter⁺ : ∀ {xs ys} → xs ≋ ys → filter P? xs ≋ filter P? ys
  filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys

------------------------------------------------------------------------
-- reverse

ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′
ʳ++⁺ = PW.ʳ++⁺

reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys
reverse⁺ = PW.reverse⁺

ext: agda


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

{-
  Useful notation for Epimorphisms, Mononmorphisms, and isomorphisms
-}
module Categories.Morphism.Notation where

open import Level

open import Categories.Category.Core
open import Categories.Morphism

private
  variable
    o ℓ e : Level

_[_↣_] : (𝒞 : Category o ℓ e) → (A B : Category.Obj 𝒞) → Set (o ⊔ ℓ ⊔ e)
𝒞 [ A ↣ B ] = _↣_ 𝒞 A B

_[_↠_] : (𝒞 : Category o ℓ e) → (A B : Category.Obj 𝒞) → Set (o ⊔ ℓ ⊔ e)
𝒞 [ A ↠ B ] = _↠_ 𝒞 A B

_[_≅_] : (𝒞 : Category o ℓ e) → (A B : Category.Obj 𝒞) → Set (ℓ ⊔ e)
𝒞 [ A ≅ B ] = _≅_ 𝒞 A B

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Agda.Builtin.Nat

data V : (n : Nat) → Set where
  cons : (n : Nat) → V (suc n)
       -- ^ this n is forced

    -- v and this n is marked shape irrelevant
g : ..(n : Nat) → V n → Nat
g _ (cons n) = n
--             ^ so we can't return n here, since we're really
--               returning the shape irrelevant one.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Numbers where

open import Haskell.Prelude
open import Agda.Builtin.Nat

posNatural : Nat
posNatural = 14

posInteger : Integer
posInteger = 52

negInteger : Integer
negInteger = -1001

natToPos : Nat → Integer
natToPos n = fromNat n

natToNeg : Nat → Integer
natToNeg n = fromNeg n

{-# COMPILE AGDA2HS posNatural #-}
{-# COMPILE AGDA2HS posInteger #-}
{-# COMPILE AGDA2HS negInteger #-}
{-# COMPILE AGDA2HS natToPos   #-}
{-# COMPILE AGDA2HS natToNeg   #-}


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

-- Type classes following Kettelhoit's approach.

module Kettelhoit where

open import Data.Bool.Base
open import Data.Nat hiding ( equal ) renaming ( suc to succ )

record Eq (A : Set) : Set where
  field equal : A → A → Bool

open Eq {{...}} public

boolEq : Bool → Bool → Bool
boolEq true  true  = true
boolEq false false = true
{-# CATCHALL #-}
boolEq _     _     = false

natEq : ℕ → ℕ → Bool
natEq zero  zero         = true
natEq (succ m) (succ n)  = natEq m n
{-# CATCHALL #-}
natEq _     _            = false

instance
  eqInstanceBool : Eq Bool
  eqInstanceBool = record { equal = boolEq }

  eqInstanceℕ : Eq ℕ
  eqInstanceℕ = record { equal = natEq }

test : Bool
test = equal 5 3 ∨ equal true false

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import lib.Basics
open import lib.Equivalences2
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel

module lib.NType2 where

module _ {i j} {A : Type i} {B : A → Type j} where
  abstract
    ↓-level : {a b : A} {p : a == b} {u : B a} {v : B b} {n : ℕ₋₂}
      → ((x : A) → has-level (S n) (B x)) → has-level n (u == v [ B ↓ p ])
    ↓-level {p = idp} k = k _ _ _

    ↓-preserves-level : {a b : A} {p : a == b} {u : B a} {v : B b} (n : ℕ₋₂)
      → ((x : A) → has-level n (B x)) → has-level n (u == v [ B ↓ p ])
    ↓-preserves-level {p = idp} n k = =-preserves-level n (k _)

    prop-has-all-paths-↓ : {x y : A} {p : x == y} {u : B x} {v : B y}
      → (is-prop (B y) → u == v [ B ↓ p ])
    prop-has-all-paths-↓ {p = idp} k = prop-has-all-paths k _ _

    set-↓-has-all-paths-↓ : ∀ {k} {C : Type k}
      {x y : C → A} {p : (t : C) → x t == y t} {u : (t : C) → B (x t)} {v : (t : C) → B (y t)}
      {a b : C} {q : a == b} {α : u a == v a [ B ↓ p a ]} {β : u b == v b [ B ↓ p b ]}
      → (is-set (B (y a)) → α == β [ (λ t → u t == v t [ B ↓ p t ]) ↓ q ])
    set-↓-has-all-paths-↓ {q = idp} = lemma _
      where
        lemma : {x y : A} (p : x == y) {u : B x} {v : B y} {α β : u == v [ B ↓ p ]}
          → is-set (B y) → α == β
        lemma idp k = fst (k _ _ _ _)

abstract
  -- Every map between contractible types is an equivalence
  contr-to-contr-is-equiv : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
    → (is-contr A → is-contr B → is-equiv f)
  contr-to-contr-is-equiv f cA cB =
    is-eq f (λ _ → fst cA) (λ b → ! (snd cB _) ∙ snd cB b) (snd cA)

  is-contr-is-prop : ∀ {i} {A : Type i} → is-prop (is-contr A)
  is-contr-is-prop {A = A} = all-paths-is-prop (λ x y →
    pair= (snd x (fst y))
          (↓-cst→app-in (λ a → ↓-idf=cst-in (lemma x (fst y) a (snd y a))))) where

    lemma : (x : is-contr A) (b a : A) (p : b == a)
      → snd x a == snd x b ∙' p
    lemma x b ._ idp = idp

  has-level-is-prop : ∀ {i} {n : ℕ₋₂} {A : Type i}
    → is-prop (has-level n A)
  has-level-is-prop {n = ⟨-2⟩} = is-contr-is-prop
  has-level-is-prop {n = S n} =
    Π-level (λ x → Π-level (λ y → has-level-is-prop))

  is-prop-is-prop : ∀ {i} {A : Type i} → is-prop (is-prop A)
  is-prop-is-prop = has-level-is-prop

  is-set-is-prop : ∀ {i} {A : Type i} → is-prop (is-set A)
  is-set-is-prop = has-level-is-prop

  subtype-level : ∀ {i j} {n : ℕ₋₂}
    {A : Type i} {P : A → Type j}
    → (has-level (S n) A → ((x : A) → is-prop (P x))
      → has-level (S n) (Σ A P))
  subtype-level p q = Σ-level p (λ x → prop-has-level-S (q x))

subtype= : ∀ {i j} {A : Type i} {P : A → Type j}
  → (x y : Σ A P) → Type i
subtype= (a₁ , _) (a₂ , _) = a₁ == a₂

subtype=-in : ∀ {i j} {A : Type i} {P : A → Type j}
  → (p : (x : A) → is-prop (P x)) → {x y : Σ A P}
  → subtype= x y → x == y
subtype=-in p idp = pair= idp (fst (p _ _ _))

-- Groupoids

is-gpd : {i : ULevel} → Type i → Type i
is-gpd = has-level 1

-- Type of all n-truncated types

_-Type_ : (n : ℕ₋₂) (i : ULevel) → Type (lsucc i)
n -Type i = Σ (Type i) (has-level n)

hProp : (i : ULevel) → Type (lsucc i)
hProp i = -1 -Type i

hSet : (i : ULevel) → Type (lsucc i)
hSet i = 0 -Type i

_-Type₀ : (n : ℕ₋₂) → Type₁
n -Type₀ = n -Type lzero

hProp₀ = hProp lzero
hSet₀ = hSet lzero

-- [n -Type] is an (n+1)-type

abstract
  ≃-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j}
    → (has-level n A → has-level n B → has-level n (A ≃ B))
  ≃-level {n = ⟨-2⟩} pA pB =
    ((cst (fst pB) , contr-to-contr-is-equiv _ pA pB)
    , (λ e → pair= (λ= (λ _ → snd pB _))
                   (from-transp is-equiv _ (fst (is-equiv-is-prop _ _ _)))))
  ≃-level {n = S n} pA pB =
    Σ-level (→-level pB) (λ _ → prop-has-level-S (is-equiv-is-prop _))

  ≃-is-set : ∀ {i j} {A : Type i} {B : Type j}
            → is-set A → is-set B → is-set (A ≃ B)
  ≃-is-set = ≃-level

  universe-=-level : ∀ {i} {n : ℕ₋₂} {A B : Type i}
    → (has-level n A → has-level n B → has-level n (A == B))
  universe-=-level pA pB = equiv-preserves-level ua-equiv (≃-level pA pB)

  universe-=-is-set : ∀ {i} {A B : Type i}
    → (is-set A → is-set B → is-set (A == B))
  universe-=-is-set = universe-=-level

  nType= : ∀ {i} {n : ℕ₋₂} (A B : n -Type i) → Type (lsucc i)
  nType= = subtype=

  nType=-in : ∀ {i} {n : ℕ₋₂} {A B : n -Type i} → fst A == fst B → A == B
  nType=-in = subtype=-in (λ _ → has-level-is-prop)

  nType=-β : ∀ {i} {n : ℕ₋₂} {A B : n -Type i} (p : fst A == fst B)
    → fst= (nType=-in {A = A} {B = B} p) == p
  nType=-β idp = fst=-β idp _

  nType=-η : ∀ {i} {n : ℕ₋₂} {A B : n -Type i} (p : A == B)
    → nType=-in (fst= p) == p
  nType=-η {A = A} {B = .A} idp = ap (pair= idp)
    (ap fst {x = has-level-is-prop _ _}
            {y = (idp , (λ p → fst (prop-is-set has-level-is-prop _ _ _ _)))}
        (fst (is-contr-is-prop _ _)))

  nType=-equiv : ∀ {i} {n : ℕ₋₂} (A B : n -Type i) → (nType= A B) ≃ (A == B)
  nType=-equiv A B = equiv nType=-in fst= nType=-η nType=-β

  _-Type-level_ : (n : ℕ₋₂) (i : ULevel)
    → has-level (S n) (n -Type i)
  (n -Type-level i) A B =
    equiv-preserves-level (nType=-equiv A B)
                          (universe-=-level (snd A) (snd B))

  hProp-is-set : (i : ULevel) → is-set (hProp i)
  hProp-is-set i = -1 -Type-level i

  hSet-level : (i : ULevel) → has-level 1 (hSet i)
  hSet-level i = 0 -Type-level i

{- The following two lemmas are in NType2 instead of NType because of cyclic
   dependencies -}

module _ {i} {A : Type i} where
  abstract
    raise-level-<T : {m n : ℕ₋₂} → (m <T n) → has-level m A → has-level n A
    raise-level-<T ltS = raise-level _
    raise-level-<T (ltSR lt) = raise-level _ ∘ raise-level-<T lt

    raise-level-≤T : {m n : ℕ₋₂} → (m ≤T n) → has-level m A → has-level n A
    raise-level-≤T (inl p) = transport (λ t → has-level t A) p
    raise-level-≤T (inr lt) = raise-level-<T lt

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Record expressions are translated to copattern matches.

module _ where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

open _×_

dup : ∀ {A} → A → A × A
dup x = record {fst = x; snd = x}

-- dup is translated internally to
--   dup x .fst = x
--   dup x .snd = x
-- so dup should not normalise to λ x → x , x

dup' : ∀ {A} → A → A × A
dup' x = x , x

-- But dup' is not translated, so dup' does reduce.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module hott.level.closure.core where

open import level
open import decidable
open import equality
open import function.isomorphism.core
-- open import function.isomorphism.properties
open import sum
open import hott.level.core
open import hott.equivalence.core
open import hott.univalence
open import sets.nat.core
-- open import sets.nat.ordering.leq.core
-- open import sets.nat.ordering.leq.decide
open import sets.empty
open import sets.unit

Σ-contr : ∀ {i j}{X : Set i}{Y : X → Set j}
        → contr X → ((x : X) → contr (Y x))
        → contr (Σ X Y)
Σ-contr {X = X}{Y = Y} (x₀ , cx) hY
  = (x₀ , proj₁ (hY x₀)) , λ { (x , y) → c x y }
    where
      c : (x : X)(y : Y x) → (x₀ , proj₁ (hY x₀)) ≡ (x , y)
      c x y = ap (λ x → (x , proj₁ (hY x))) (cx x)
            · ap (_,_ x) (proj₂ (hY x) y)

×-contr : ∀ {i j}{X : Set i}{Y : Set j}
        → contr X → contr Y
        → contr (X × Y)
×-contr hX hY = Σ-contr hX (λ _ → hY)

unique-contr : ∀ {i}{A B : Set i}
             → contr A
             → contr B
             → A ≡ B
unique-contr {i}{A}{B} hA hB = ≈⇒≡ (f , f-we)
  where
    f : A → B
    f _ = proj₁ hB

    f-we : weak-equiv f
    f-we b = ×-contr hA (h↑ hB _ _)

-- h-≤ : ∀ {i n m}{X : Set i}
--     → n ≤ m → h n X → h m X
-- h-≤ {m = 0} z≤n hX = hX
-- h-≤ {m = suc m} z≤n hX = λ x y
--   → h-≤ {m = m} z≤n (h↑ hX x y)
-- h-≤ (s≤s p) hX = λ x y
--   → h-≤ p (hX x y)
--
-- h! : ∀ {i n m}{X : Set i}
--    → {p : True (n ≤? m)}
--    → h n X → h m X
-- h! {p = p} = h-≤ (witness p)

abstract
  -- retractions preserve levels
  retract-level : ∀ {i j n} {X : Set i}{Y : Set j}
                 → (f : X → Y)(g : Y → X)
                 → ((y : Y) → f (g y) ≡ y)
                 → h n X → h n Y
  retract-level {n = 0}{X}{Y} f g r (x , c) = (f x , c')
    where
      c' : (y : Y) → f x ≡ y
      c' y = ap f (c (g y)) · r y
  retract-level {n = suc n}{X}{Y} f g r hX = λ y y'
    → retract-level f' g' r' (hX (g y) (g y'))
    where
      f' : {y y' : Y} → g y ≡ g y' → y ≡ y'
      f' {y}{y'} p = sym (r y) · ap f p · r y'

      g' : {y y' : Y} → y ≡ y' → g y ≡ g y'
      g' = ap g

      r' : {y y' : Y}(p : y ≡ y') → f' (g' p) ≡ p
      r' {y}{.y} refl = ap (λ α → α · r y) (left-unit (sym (r y)))
                      · right-inverse (r y)

  iso-level : ∀ {i j n}{X : Set i}{Y : Set j}
             → X ≅ Y → h n X → h n Y
  iso-level (iso f g H K) = retract-level f g K

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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

-- This is a file for dealing with Monuses: these are monoids that are like the
-- positive half of a group. Much of my info on them comes from these papers:
--
-- * Wehrung, Friedrich. ‘Injective Positively Ordered Monoids I’. Journal of
--   Pure and Applied Algebra 83, no. 1 (11 November 1992): 43–82.
--   https://doi.org/10.1016/0022-4049(92)90104-N.
-- * Wehrung, Friedrich. ‘Embedding Simple Commutative Monoids into Simple
--   Refinement Monoids’. Semigroup Forum 56, no. 1 (January 1998): 104–29.
--   https://doi.org/10.1007/s00233-002-7008-0.
-- * Amer, K. ‘Equationally Complete Classes of Commutative Monoids with Monus’.
--   Algebra Universalis 18, no. 1 (1 February 1984): 129–31.
--   https://doi.org/10.1007/BF01182254.
-- * Wehrung, Friedrich. ‘Metric Properties of Positively Ordered Monoids’.
--   Forum Mathematicum 5, no. 5 (1993).
--   https://doi.org/10.1515/form.1993.5.183.
-- * Wehrung, Friedrich. ‘Restricted Injectivity, Transfer Property and
--   Decompositions of Separative Positively Ordered Monoids.’ Communications in
--   Algebra 22, no. 5 (1 January 1994): 1747–81.
--   https://doi.org/10.1080/00927879408824934.
--
-- These monoids have a preorder defined on them, the algebraic preorder:
--
--   x ≤ y = ∃ z × (y ≡ x ∙ z)
--
-- The _∸_ operator extracts the z from above, if it exists.

module Algebra.Monus where

open import Prelude
open import Algebra
open import Relation.Binary
open import Path.Reasoning
open import Function.Reasoning

-- Positively ordered monoids.
--
-- These are monoids which have a preorder that respects the monoid operation
-- in a straightforward way.
record POM ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field commutativeMonoid : CommutativeMonoid ℓ₁
  open CommutativeMonoid commutativeMonoid public
  field preorder : Preorder 𝑆 ℓ₂
  open Preorder preorder public renaming (refl to ≤-refl)
  field
    positive : ∀ x → ε ≤ x
    ≤-cong : ∀ x {y z} → y ≤ z → x ∙ y ≤ x ∙ z

  x≤x∙y : ∀ {x y} → x ≤ x ∙ y
  x≤x∙y {x} {y} = subst (_≤ x ∙ y) (∙ε x) (≤-cong x (positive y))

  ≤-congʳ : ∀ x {y z} → y ≤ z → y ∙ x ≤ z ∙ x
  ≤-congʳ x {y} {z} p = subst₂ _≤_ (comm x y) (comm x z) (≤-cong x p)

  alg-≤-trans : ∀ {x y z k₁ k₂} → y ≡ x ∙ k₁ → z ≡ y ∙ k₂ → z ≡ x ∙ (k₁ ∙ k₂)
  alg-≤-trans {x} {y} {z} {k₁} {k₂} y≡x∙k₁ z≡y∙k₂ =
    z             ≡⟨ z≡y∙k₂ ⟩
    y ∙ k₂        ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
    (x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
    x ∙ (k₁ ∙ k₂) ∎

  infix 4 _≺_
  _≺_ : 𝑆 → 𝑆 → Type _
  x ≺ y = ∃ k × (y ≡ x ∙ k) × (k ≢ ε)

-- Total Antisymmetric POM
record TAPOM ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field pom : POM ℓ₁ ℓ₂
  open POM pom public using (preorder; _≤_; ≤-cong; ≤-congʳ; x≤x∙y; commutativeMonoid; positive)
  open CommutativeMonoid commutativeMonoid public
  field
    _≤|≥_   : Total _≤_
    antisym : Antisymmetric _≤_

  totalOrder : TotalOrder 𝑆 ℓ₂ ℓ₂
  totalOrder = fromPartialOrder (record { preorder = preorder ; antisym = antisym }) _≤|≥_
  open TotalOrder totalOrder public hiding (_≤|≥_; antisym) renaming (refl to ≤-refl)

-- Every commutative monoid generates a positively ordered monoid
-- called the "algebraic" or "minimal" pom
module AlgebraicPOM {ℓ} (mon : CommutativeMonoid ℓ) where
  commutativeMonoid = mon
  open CommutativeMonoid mon

  infix 4 _≤_
  _≤_ : 𝑆 → 𝑆 → Type _
  x ≤ y = ∃ z × (y ≡ x ∙ z)

  -- The snd here is the same proof as alg-≤-trans, so could be refactored out.
  ≤-trans : Transitive _≤_
  ≤-trans (k₁ , _) (k₂ , _) .fst = k₁ ∙ k₂
  ≤-trans {x} {y} {z} (k₁ , y≡x∙k₁) (k₂ , z≡y∙k₂) .snd =
    z             ≡⟨ z≡y∙k₂ ⟩
    y ∙ k₂        ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
    (x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
    x ∙ (k₁ ∙ k₂) ∎

  preorder : Preorder 𝑆 ℓ
  Preorder._≤_ preorder = _≤_
  Preorder.refl preorder = ε , sym (∙ε _)
  Preorder.trans preorder = ≤-trans

  positive : ∀ x → ε ≤ x
  positive x = x , sym (ε∙ x)

  ≤-cong : ∀ x {y z} → y ≤ z → x ∙ y ≤ x ∙ z
  ≤-cong x (k , z≡y∙k) = k , cong (x ∙_) z≡y∙k ; sym (assoc x _ k)

algebraic-pom : ∀ {ℓ} → CommutativeMonoid ℓ → POM ℓ ℓ
algebraic-pom mon = record { AlgebraicPOM mon }

-- Total Minimal POM
record TMPOM ℓ : Type (ℓsuc ℓ) where
  field commutativeMonoid : CommutativeMonoid ℓ

  pom : POM _ _
  pom = algebraic-pom commutativeMonoid

  open POM pom public

  infix 4 _≤|≥_
  field _≤|≥_ : Total _≤_

  <⇒≺ : ∀ x y → y ≰ x → x ≺ y
  <⇒≺ x y x<y with x ≤|≥ y
  ... | inr y≤x = ⊥-elim (x<y y≤x)
  ... | inl (k , y≡x∙k) = λ
    where
    .fst → k
    .snd .fst → y≡x∙k
    .snd .snd k≡ε → x<y (ε , sym (∙ε y ; y≡x∙k ; cong (x ∙_) k≡ε ; ∙ε x))

  infixl 6 _∸_
  _∸_ : 𝑆 → 𝑆 → 𝑆
  x ∸ y = either′ (const ε) fst (x ≤|≥ y)

  x∸y≤x : ∀ x y → x ∸ y ≤ x
  x∸y≤x x y with x ≤|≥ y
  ... | inl (k , p) = positive x
  ... | inr (k , x≡y∙k) = y , x≡y∙k ; comm y k

-- Total Minimal Antisymmetric POM
record TMAPOM ℓ : Type (ℓsuc ℓ) where
  field tmpom : TMPOM ℓ
  open TMPOM tmpom public using (_≤_; _≤|≥_; positive; alg-≤-trans; _≺_; <⇒≺; _∸_; x∸y≤x)
  field antisym : Antisymmetric _≤_

  tapom : TAPOM _ _
  TAPOM.pom tapom = TMPOM.pom tmpom
  TAPOM._≤|≥_ tapom = _≤|≥_
  TAPOM.antisym tapom = antisym

  open TAPOM tapom public hiding (antisym; _≤|≥_; _≤_; positive)

  zeroSumFree : ∀ x y → x ∙ y ≡ ε → x ≡ ε
  zeroSumFree x y x∙y≡ε = antisym (y , sym x∙y≡ε) (positive x)

  ≤‿∸‿cancel : ∀ x y → x ≤ y → (y ∸ x) ∙ x ≡ y
  ≤‿∸‿cancel x y x≤y with y ≤|≥ x
  ... | inl y≤x = ε∙ x ; antisym x≤y y≤x
  ... | inr (k , y≡x∙k) = comm k x ; sym y≡x∙k

  ∸‿comm : ∀ x y → x ∙ (y ∸ x) ≡ y ∙ (x ∸ y)
  ∸‿comm x y with y ≤|≥ x | x ≤|≥ y
  ... | inl y≤x | inl x≤y = cong (_∙ ε) (antisym x≤y y≤x)
  ... | inr (k , y≡x∙k) | inl x≤y = sym y≡x∙k ; sym (∙ε y)
  ... | inl y≤x | inr (k , x≥y) = ∙ε x ; x≥y
  ... | inr (k₁ , y≡x∙k₁) | inr (k₂ , x≡y∙k₂) =
    x ∙ k₁ ≡˘⟨ y≡x∙k₁ ⟩
    y      ≡⟨ antisym  (k₂ , x≡y∙k₂) (k₁ , y≡x∙k₁) ⟩
    x      ≡⟨ x≡y∙k₂ ⟩
    y ∙ k₂ ∎

  ∸‿≺ : ∀ x y → x ≢ ε → y ≢ ε → x ∸ y ≺ x
  ∸‿≺ x y x≢ε y≢ε with x ≤|≥ y
  ... | inl _ = x , sym (ε∙ x) , x≢ε
  ... | inr (k , x≡y∙k) = y , x≡y∙k ; comm y k , y≢ε

-- Commutative Monoids with Monus
record CMM ℓ : Type (ℓsuc ℓ) where
  field commutativeMonoid : CommutativeMonoid ℓ

  pom : POM _ _
  pom = algebraic-pom commutativeMonoid

  open POM pom public

  field _∸_ : 𝑆 → 𝑆 → 𝑆
  infixl 6 _∸_
  field
    ∸‿comm  : ∀ x y → x ∙ (y ∸ x) ≡ y ∙ (x ∸ y)
    ∸‿assoc : ∀ x y z → (x ∸ y) ∸ z ≡ x ∸ (y ∙ z)
    ∸‿inv   : ∀ x → x ∸ x ≡ ε
    ε∸      : ∀ x → ε ∸ x ≡ ε

  ∸ε : ∀ x → x ∸ ε ≡ x
  ∸ε x =
    x ∸ ε       ≡˘⟨ ε∙ (x ∸ ε) ⟩
    ε ∙ (x ∸ ε) ≡⟨ ∸‿comm ε x ⟩
    x ∙ (ε ∸ x) ≡⟨ cong (x ∙_) (ε∸ x) ⟩
    x ∙ ε       ≡⟨ ∙ε x ⟩
    x ∎

  ∸≤ : ∀ x y → x ≤ y → x ∸ y ≡ ε
  ∸≤ x y (k , y≡x∙k) =
    x ∸ y       ≡⟨ cong (x ∸_) y≡x∙k ⟩
    x ∸ (x ∙ k) ≡˘⟨ ∸‿assoc x x k ⟩
    (x ∸ x) ∸ k ≡⟨ cong (_∸ k) (∸‿inv x) ⟩
    ε ∸ k       ≡⟨ ε∸ k ⟩
    ε ∎

  ∣_-_∣ : 𝑆 → 𝑆 → 𝑆
  ∣ x - y ∣ = (x ∸ y) ∙ (y ∸ x)

  _⊔₂_ : 𝑆 → 𝑆 → 𝑆
  x ⊔₂ y = x ∙ y ∙ ∣ x - y ∣

  _⊓₂_ : 𝑆 → 𝑆 → 𝑆
  x ⊓₂ y = (x ∙ y) ∸ ∣ x - y ∣

-- Cancellative Commutative Monoids with Monus
record CCMM ℓ : Type (ℓsuc ℓ) where
  field cmm : CMM ℓ
  open CMM cmm public

  field ∸‿cancel : ∀ x y → (x ∙ y) ∸ x ≡ y

  cancelˡ : Cancellativeˡ _∙_
  cancelˡ x y z x∙y≡x∙z =
    y           ≡˘⟨ ∸‿cancel x y ⟩
    (x ∙ y) ∸ x ≡⟨ cong (_∸ x) x∙y≡x∙z ⟩
    (x ∙ z) ∸ x ≡⟨ ∸‿cancel x z ⟩
    z ∎

  cancelʳ : Cancellativeʳ _∙_
  cancelʳ x y z y∙x≡z∙x =
    y           ≡˘⟨ ∸‿cancel x y ⟩
    (x ∙ y) ∸ x ≡⟨ cong (_∸ x) (comm x y) ⟩
    (y ∙ x) ∸ x ≡⟨ cong (_∸ x) y∙x≡z∙x ⟩
    (z ∙ x) ∸ x ≡⟨ cong (_∸ x) (comm z x) ⟩
    (x ∙ z) ∸ x ≡⟨ ∸‿cancel x z ⟩
    z ∎

  zeroSumFree : ∀ x y → x ∙ y ≡ ε → x ≡ ε
  zeroSumFree x y x∙y≡ε =
    x           ≡˘⟨ ∸‿cancel y x ⟩
    (y ∙ x) ∸ y ≡⟨ cong (_∸ y) (comm y x) ⟩
    (x ∙ y) ∸ y ≡⟨ cong (_∸ y) x∙y≡ε ⟩
    ε ∸ y       ≡⟨ ε∸ y ⟩
    ε ∎

  antisym : Antisymmetric _≤_
  antisym {x} {y} (k₁ , y≡x∙k₁) (k₂ , x≡y∙k₂) =
      x      ≡⟨ x≡y∙k₂ ⟩
      y ∙ k₂ ≡⟨ [ lemma                 ]⇒ y ∙ ε   ≡ y ∙ (k₂ ∙ k₁)
                ⟨ cancelˡ y ε (k₂ ∙ k₁) ⟩⇒ ε       ≡ k₂ ∙ k₁
                ⟨ sym                   ⟩⇒ k₂ ∙ k₁ ≡ ε
                ⟨ zeroSumFree k₂ k₁     ⟩⇒ k₂      ≡ ε
                ⟨ cong (y ∙_)           ⟩⇒ y ∙ k₂  ≡ y ∙ ε ⇒∎ ⟩
      y ∙ ε  ≡⟨ ∙ε y ⟩
      y ∎
    where
    lemma = ∙ε y ; alg-≤-trans x≡y∙k₂ y≡x∙k₁

  partialOrder : PartialOrder _ _
  PartialOrder.preorder partialOrder = preorder
  PartialOrder.antisym partialOrder = antisym

  ≺⇒< : ∀ x y → x ≺ y → y ≰ x
  ≺⇒< x y (k₁ , y≡x∙k₁ , k₁≢ε) (k₂ , x≡y∙k₂) =
    [ x ∙ ε         ≡⟨ ∙ε x ⟩
      x             ≡⟨ x≡y∙k₂ ⟩
      y ∙ k₂        ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
      (x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
      x ∙ (k₁ ∙ k₂) ∎       ]⇒ x ∙ ε ≡ x ∙ (k₁ ∙ k₂)
    ⟨ cancelˡ x ε (k₁ ∙ k₂) ⟩⇒ ε ≡ k₁ ∙ k₂
    ⟨ sym                   ⟩⇒ k₁ ∙ k₂ ≡ ε
    ⟨ zeroSumFree k₁ k₂     ⟩⇒ k₁ ≡ ε
    ⟨ k₁≢ε                  ⟩⇒ ⊥ ⇒∎

  ≤⇒<⇒≢ε : ∀ x y → (x≤y : x ≤ y) → y ≰ x → fst x≤y ≢ ε
  ≤⇒<⇒≢ε x y (k₁ , y≡x∙k₁) y≰x k₁≡ε = y≰x λ
    where
    .fst → ε
    .snd → x      ≡˘⟨ ∙ε x ⟩
           x ∙ ε  ≡˘⟨ cong (x ∙_) k₁≡ε ⟩
           x ∙ k₁ ≡˘⟨ y≡x∙k₁ ⟩
           y      ≡˘⟨ ∙ε y ⟩
           y ∙ ε ∎

  ≤-cancelʳ : ∀ x y z → y ∙ x ≤ z ∙ x → y ≤ z
  ≤-cancelʳ x y z (k , z∙x≡y∙x∙k) .fst = k
  ≤-cancelʳ x y z (k , z∙x≡y∙x∙k) .snd = cancelʳ x z (y ∙ k) $
    z ∙ x ≡⟨ z∙x≡y∙x∙k ⟩
    (y ∙ x) ∙ k ≡⟨ assoc y x k ⟩
    y ∙ (x ∙ k) ≡⟨ cong (y ∙_) (comm x k) ⟩
    y ∙ (k ∙ x) ≡˘⟨ assoc y k x ⟩
    (y ∙ k) ∙ x ∎

  ≤-cancelˡ : ∀ x y z → x ∙ y ≤ x ∙ z → y ≤ z
  ≤-cancelˡ x y z (k , x∙z≡x∙y∙k) .fst = k
  ≤-cancelˡ x y z (k , x∙z≡x∙y∙k) .snd =
    cancelˡ x z (y ∙ k) (x∙z≡x∙y∙k ; assoc x y k)

  ≺-irrefl : Irreflexive _≺_
  ≺-irrefl {x} (k , x≡x∙k , k≢ε) = k≢ε (sym (cancelˡ x ε k (∙ε x ; x≡x∙k)))

  ≤∸ : ∀ x y → (x≤y : x ≤ y) → y ∸ x ≡ fst x≤y
  ≤∸ x y (k , y≡x∙k) =
   y ∸ x       ≡⟨ cong (_∸ x) y≡x∙k ⟩
   (x ∙ k) ∸ x ≡⟨ ∸‿cancel x k ⟩
   k ∎

  ≤‿∸‿cancel : ∀ x y → x ≤ y → (y ∸ x) ∙ x ≡ y
  ≤‿∸‿cancel x y (k , y≡x∙k) =
    (y ∸ x) ∙ x ≡⟨ cong (λ y → (y ∸ x) ∙ x) y≡x∙k ⟩
    ((x ∙ k) ∸ x) ∙ x ≡⟨ cong (_∙ x) (∸‿cancel x k) ⟩
    k ∙ x ≡⟨ comm k x ⟩
    x ∙ k ≡˘⟨ y≡x∙k ⟩
    y ∎

-- Cancellative total minimal antisymmetric pom (has monus)
record CTMAPOM ℓ : Type (ℓsuc ℓ) where
  field tmapom : TMAPOM ℓ
  open TMAPOM tmapom public
  field cancel : Cancellativeˡ _∙_

  module cmm where
    ∸≤ : ∀ x y → x ≤ y → x ∸ y ≡ ε
    ∸≤ x y x≤y with x ≤|≥ y
    ∸≤ x y x≤y | inl _ = refl
    ∸≤ x y (k₁ , y≡x∙k₁) | inr (k₂ , x≡y∙k₂) =
      [ lemma                ]⇒ y ∙ ε   ≡ y ∙ (k₂ ∙ k₁)
      ⟨ cancel y ε (k₂ ∙ k₁) ⟩⇒ ε       ≡ k₂ ∙ k₁
      ⟨ sym                  ⟩⇒ k₂ ∙ k₁ ≡ ε
      ⟨ zeroSumFree k₂ k₁    ⟩⇒ k₂      ≡ ε ⇒∎
      where
      lemma = ∙ε y ; alg-≤-trans x≡y∙k₂ y≡x∙k₁

    ∸‿inv : ∀ x → x ∸ x ≡ ε
    ∸‿inv x = ∸≤ x x ≤-refl

    ε∸ : ∀ x → ε ∸ x ≡ ε
    ε∸ x = ∸≤ ε x (positive x)

    ∸‿assoc : ∀ x y z → (x ∸ y) ∸ z ≡ x ∸ (y ∙ z)
    ∸‿assoc x y z with x ≤|≥ y
    ∸‿assoc x y z | inl x≤y  = ε∸ z ; sym (∸≤ x (y ∙ z) (≤-trans x≤y x≤x∙y))
    ∸‿assoc x y z | inr x≥y with x ≤|≥ y ∙ z
    ∸‿assoc x y z | inr (k₁ , x≡y∙k₁) | inl (k₂ , y∙z≡x∙k₂) = ∸≤ k₁ z (k₂ , lemma)
      where
      lemma : z ≡ k₁ ∙ k₂
      lemma = cancel y z (k₁ ∙ k₂) (alg-≤-trans x≡y∙k₁ y∙z≡x∙k₂)

    ∸‿assoc x y z | inr (k , x≡y∙k) | inr x≥y∙z with k ≤|≥ z
    ∸‿assoc x y z | inr (k₁ , x≡y∙k₁) | inr (k₂ , x≡y∙z∙k₂) | inl (k₃ , z≡k₁∙k₃) =
        [ lemma₁            ]⇒ ε       ≡ k₂ ∙ k₃
        ⟨ sym               ⟩⇒ k₂ ∙ k₃ ≡ ε
        ⟨ zeroSumFree k₂ k₃ ⟩⇒ k₂      ≡ ε
        ⟨ sym               ⟩⇒ ε       ≡ k₂ ⇒∎
      where
      lemma₃ =
        y ∙ k₁       ≡˘⟨ x≡y∙k₁ ⟩
        x            ≡⟨ x≡y∙z∙k₂ ⟩
        (y ∙ z) ∙ k₂ ≡⟨ assoc y z k₂ ⟩
        y ∙ (z ∙ k₂) ∎

      lemma₂ =
        k₁ ∙ ε         ≡⟨ ∙ε k₁ ⟩
        k₁             ≡⟨ alg-≤-trans z≡k₁∙k₃ (cancel y k₁ (z ∙ k₂) lemma₃) ⟩
        k₁ ∙ (k₃ ∙ k₂) ∎

      lemma₁ =
        ε       ≡⟨ cancel k₁ ε (k₃ ∙ k₂) lemma₂ ⟩
        k₃ ∙ k₂ ≡⟨ comm k₃ k₂ ⟩
        k₂ ∙ k₃ ∎

    ∸‿assoc x y z | inr (k₁ , x≡y∙k₁) | inr (k₂ , x≡y∙z∙k₂) | inr (k₃ , k₁≡z∙k₃) =
        cancel z k₃ k₂ lemma₂
      where
      lemma₁ =
        y ∙ k₁       ≡˘⟨ x≡y∙k₁ ⟩
        x            ≡⟨ x≡y∙z∙k₂ ⟩
        (y ∙ z) ∙ k₂ ≡⟨ assoc y z k₂ ⟩
        y ∙ (z ∙ k₂) ∎

      lemma₂ =
        z ∙ k₃ ≡˘⟨ k₁≡z∙k₃ ⟩
        k₁     ≡⟨ cancel y k₁ (z ∙ k₂) lemma₁ ⟩
        z ∙ k₂ ∎

  open cmm public

  ∸‿cancel : ∀ x y → (x ∙ y) ∸ x ≡ y
  ∸‿cancel x y with (x ∙ y) ≤|≥ x
  ... | inl x∙y≤x = sym (cancel x y ε (antisym x∙y≤x x≤x∙y ; sym (∙ε x)))
  ... | inr (k , x∙y≡x∙k) = sym (cancel x y k x∙y≡x∙k)

  ccmm : CCMM _
  ccmm = record { ∸‿cancel = ∸‿cancel
                ; cmm = record { cmm
                               ; ∸‿comm = ∸‿comm
                               ; commutativeMonoid = commutativeMonoid } }

  open CCMM ccmm public
    using (cancelʳ; cancelˡ; ∸ε; ≺⇒<; ≤⇒<⇒≢ε; _⊔₂_; _⊓₂_; ≺-irrefl; ≤∸)

  ∸‿< : ∀ x y → x ≢ ε → y ≢ ε → x ∸ y < x
  ∸‿< x y x≢ε y≢ε = ≺⇒< (x ∸ y) x (∸‿≺ x y x≢ε y≢ε)

  ∸‿<-< : ∀ x y → x < y → x ≢ ε → y ∸ x < y
  ∸‿<-< x y x<y x≢ε = ∸‿< y x (λ y≡ε → x<y (x , sym (cong (_∙ x) y≡ε ; ε∙ x))) x≢ε

  2× : 𝑆 → 𝑆
  2× x = x ∙ x

  open import Relation.Binary.Lattice totalOrder

  double-max : ∀ x y → 2× (x ⊔ y) ≡ x ⊔₂ y
  double-max x y with x ≤|≥ y | y ≤|≥ x
  double-max x y | inl x≤y | inl y≤x =
    x ∙ x ≡⟨ cong (x ∙_) (antisym x≤y y≤x) ⟩
    x ∙ y ≡˘⟨ ∙ε (x ∙ y) ⟩
    (x ∙ y) ∙ ε ≡˘⟨ cong ((x ∙ y) ∙_)  (ε∙ ε) ⟩
    (x ∙ y) ∙ (ε ∙ ε) ∎
  double-max x y | inl x≤y | inr (k , y≡x∙k) =
    y ∙ y ≡⟨ cong (y ∙_) y≡x∙k ⟩
    y ∙ (x ∙ k) ≡˘⟨ assoc y x k ⟩
    (y ∙ x) ∙ k ≡⟨ cong (_∙ k) (comm y x) ⟩
    (x ∙ y) ∙ k ≡˘⟨ cong ((x ∙ y) ∙_) (ε∙ k) ⟩
    (x ∙ y) ∙ (ε ∙ k) ∎
  double-max x y | inr (k , x≡y∙k) | inl y≤x =
    x ∙ x ≡⟨ cong (x ∙_) x≡y∙k ⟩
    x ∙ (y ∙ k) ≡˘⟨ assoc x y k ⟩
    (x ∙ y) ∙ k ≡˘⟨ cong ((x ∙ y) ∙_) (∙ε k) ⟩
    (x ∙ y) ∙ (k ∙ ε) ∎
  double-max x y | inr (k₁ , x≡y∙k₁) | inr (k₂ , y≡x∙k₂) =
    x ∙ x ≡⟨ cong (x ∙_) (antisym (k₂ , y≡x∙k₂) (k₁ , x≡y∙k₁)) ⟩
    x ∙ y ≡⟨ cong₂ _∙_ x≡y∙k₁ y≡x∙k₂ ⟩
    (y ∙ k₁) ∙ (x ∙ k₂) ≡˘⟨ assoc (y ∙ k₁) x k₂ ⟩
    ((y ∙ k₁) ∙ x) ∙ k₂ ≡⟨ cong (_∙ k₂) (comm (y ∙ k₁) x) ⟩
    (x ∙ (y ∙ k₁)) ∙ k₂ ≡˘⟨ cong (_∙ k₂) (assoc x y k₁) ⟩
    ((x ∙ y) ∙ k₁) ∙ k₂ ≡⟨ assoc (x ∙ y) k₁ k₂ ⟩
    (x ∙ y) ∙ (k₁ ∙ k₂) ∎

  open import Data.Sigma.Properties

  ≤-prop : ∀ x y → isProp (x ≤ y)
  ≤-prop x y (k₁ , y≡x∙k₁) (k₂ , y≡x∙k₂) = Σ≡Prop (λ _ → total⇒isSet _ _) (cancelˡ x k₁ k₂ (sym y≡x∙k₁ ; y≡x∙k₂))

  open import Cubical.Foundations.HLevels using (isProp×)
  open import Data.Empty.Properties using (isProp¬)

  ≺-prop : ∀ x y → isProp (x ≺ y)
  ≺-prop x y (k₁ , y≡x∙k₁ , k₁≢ε) (k₂ , y≡x∙k₂ , k₂≢ε) = Σ≡Prop (λ k → isProp× (total⇒isSet _ _) (isProp¬ _)) (cancelˡ x k₁ k₂ (sym y≡x∙k₁ ; y≡x∙k₂))

-- We can construct the viterbi semiring by adjoining a top element to
-- a tapom
module Viterbi {ℓ₁} {ℓ₂} (tapom : TAPOM ℓ₁ ℓ₂) where
  open TAPOM tapom
  open import Relation.Binary.Construct.UpperBound totalOrder
  open import Relation.Binary.Lattice totalOrder

  ⟨⊓⟩∙ : _∙_ Distributesˡ _⊓_
  ⟨⊓⟩∙ x y z with x <? y | (x ∙ z) <? (y ∙ z)
  ... | yes x<y | yes xz<yz = refl
  ... | no  x≮y | no  xz≮yz = refl
  ... | no  x≮y | yes xz<yz = ⊥-elim (<⇒≱ xz<yz (≤-congʳ z (≮⇒≥ x≮y)))
  ... | yes x<y | no  xz≮yz = antisym (≤-congʳ z (<⇒≤ x<y)) (≮⇒≥ xz≮yz)

  ∙⟨⊓⟩ : _∙_ Distributesʳ _⊓_
  ∙⟨⊓⟩ x y z = comm x (y ⊓ z) ; ⟨⊓⟩∙ y z x ; cong₂ _⊓_ (comm y x) (comm z x)

  open UBSugar

  module NS where
    𝑅 = ⌈∙⌉

    0# 1# : 𝑅
    _*_ _+_ : 𝑅 → 𝑅 → 𝑅

    1# = ⌈ ε ⌉

    ⌈⊤⌉   * y     = ⌈⊤⌉
    ⌈ x ⌉ * ⌈⊤⌉   = ⌈⊤⌉
    ⌈ x ⌉ * ⌈ y ⌉ = ⌈ x ∙ y ⌉

    0# = ⌈⊤⌉

    ⌈⊤⌉   + y     = y
    ⌈ x ⌉ + ⌈⊤⌉   = ⌈ x ⌉
    ⌈ x ⌉ + ⌈ y ⌉ = ⌈ x ⊓ y ⌉

    *-assoc : Associative _*_
    *-assoc ⌈⊤⌉   _     _     = refl
    *-assoc ⌈ _ ⌉ ⌈⊤⌉   _     = refl
    *-assoc ⌈ _ ⌉ ⌈ _ ⌉ ⌈⊤⌉   = refl
    *-assoc ⌈ x ⌉ ⌈ y ⌉ ⌈ z ⌉ = cong ⌈_⌉ (assoc x y z)

    *-com : Commutative _*_
    *-com ⌈⊤⌉   ⌈⊤⌉   = refl
    *-com ⌈⊤⌉   ⌈ _ ⌉ = refl
    *-com ⌈ _ ⌉ ⌈⊤⌉   = refl
    *-com ⌈ x ⌉ ⌈ y ⌉ = cong ⌈_⌉ (comm x y)

    ⟨+⟩* : _*_ Distributesˡ _+_
    ⟨+⟩* ⌈⊤⌉   _     _     = refl
    ⟨+⟩* ⌈ _ ⌉ ⌈⊤⌉   ⌈⊤⌉   = refl
    ⟨+⟩* ⌈ _ ⌉ ⌈⊤⌉   ⌈ _ ⌉ = refl
    ⟨+⟩* ⌈ x ⌉ ⌈ y ⌉ ⌈⊤⌉   = refl
    ⟨+⟩* ⌈ x ⌉ ⌈ y ⌉ ⌈ z ⌉ = cong ⌈_⌉ (⟨⊓⟩∙ x y z)

    +-assoc : Associative _+_
    +-assoc ⌈⊤⌉   _     _     = refl
    +-assoc ⌈ x ⌉ ⌈⊤⌉   _     = refl
    +-assoc ⌈ x ⌉ ⌈ _ ⌉ ⌈⊤⌉   = refl
    +-assoc ⌈ x ⌉ ⌈ y ⌉ ⌈ z ⌉ = cong ⌈_⌉ (⊓-assoc x y z)

    0+ : ∀ x → 0# + x ≡ x
    0+ ⌈⊤⌉   = refl
    0+ ⌈ _ ⌉ = refl

    +0 : ∀ x → x + 0# ≡ x
    +0 ⌈ _ ⌉ = refl
    +0 ⌈⊤⌉   = refl

    1* : ∀ x → 1# * x ≡ x
    1* ⌈⊤⌉   = refl
    1* ⌈ x ⌉ = cong ⌈_⌉ (ε∙ x)

    *1 : ∀ x → x * 1# ≡ x
    *1 ⌈⊤⌉   = refl
    *1 ⌈ x ⌉ = cong ⌈_⌉ (∙ε x)

    0* : ∀ x → 0# * x ≡ 0#
    0* _ = refl

  open NS

  nearSemiring : NearSemiring _
  nearSemiring = record { NS }

  +-comm : Commutative _+_
  +-comm ⌈⊤⌉   ⌈⊤⌉   = refl
  +-comm ⌈⊤⌉   ⌈ _ ⌉ = refl
  +-comm ⌈ _ ⌉ ⌈⊤⌉   = refl
  +-comm ⌈ x ⌉ ⌈ y ⌉ = cong ⌈_⌉ (⊓-comm x y)

  *0 : ∀ x → x * ⌈⊤⌉ ≡ ⌈⊤⌉
  *0 ⌈ _ ⌉ = refl
  *0 ⌈⊤⌉   = refl

  *⟨+⟩ : _*_ Distributesʳ _+_
  *⟨+⟩ x y z = *-com x (y + z) ; ⟨+⟩* y z x ; cong₂ _+_ (*-com y x) (*-com z x)

viterbi : ∀ {ℓ₁ ℓ₂} → TAPOM ℓ₁ ℓ₂ → Semiring ℓ₁
viterbi tapom = record { Viterbi tapom }

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Fixpoint combinators
------------------------------------------------------------------------

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

module Partiality-monad.Inductive.Fixpoints where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Monad equality-with-J hiding (sequence)
open import Univalence-axiom equality-with-J

open import Partiality-algebra using (Partiality-algebra)
import Partiality-algebra.Fixpoints as PAF
open import Partiality-algebra.Monotone
open import Partiality-algebra.Omega-continuous
open import Partiality-algebra.Pi as Pi hiding (at)
open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Monad
open import Partiality-monad.Inductive.Monotone using ([_⊥→_⊥]⊑)
open import Partiality-monad.Inductive.Omega-continuous

------------------------------------------------------------------------
-- The fixpoint combinator machinery instantiated with the partiality
-- monad

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

  open PAF.Fix {P = partiality-algebra A} public
  open [_⊥→_⊥]

  -- A variant of fix.

  fix′ : (A → A ⊥) → A ⊥
  fix′ f = fix (monotone-function (f ∗))

  -- This variant also produces a kind of least fixpoint.

  fix′-is-fixpoint-combinator :
    (f : A → A ⊥) →
    fix′ f ≡ fix′ f >>= f
  fix′-is-fixpoint-combinator f =
    fix′ f                               ≡⟨⟩
    fix (monotone-function (f ∗))        ≡⟨ fix-is-fixpoint-combinator (f ∗) ⟩∎
    fix (monotone-function (f ∗)) >>= f  ∎

  fix′-is-least :
    (f : A → A ⊥) →
    (x : A ⊥) → x >>= f ⊑ x → fix′ f ⊑ x
  fix′-is-least f = fix-is-least (monotone-function (f ∗))

  -- Taking steps that are "twice as large" does not affect the end
  -- result.

  fix′-∘ : (f : A → A ⊥) → fix′ (λ x → f x >>= f) ≡ fix′ f
  fix′-∘ f =
    fix′ (λ x → f x >>= f)                                    ≡⟨⟩

    fix (monotone-function ((λ x → f x >>= f) ∗))             ≡⟨ cong fix (_↔_.to equality-characterisation-monotone λ (x : A ⊥) →

        (x >>= λ y → f y >>= f)                                    ≡⟨ associativity x f f ⟩∎
        x >>= f >>= f                                              ∎) ⟩

    fix (monotone-function (f ∗) ∘⊑ monotone-function (f ∗))  ≡⟨ fix-∘ (monotone-function (f ∗)) ⟩∎

    fix′ f                                                    ∎

  -- Unary Scott induction for fix′.

  fix′-induction₁ :
    ∀ {p}
    (P : A ⊥ → Type p)
    (P⊥ : P never)
    (P⨆ : ∀ s → (∀ n → P (s [ n ])) → P (⨆ s))
    (f : A → A ⊥) →
    (∀ x → P x → P (x >>= f)) →
    P (fix′ f)
  fix′-induction₁ P P⊥ P⨆ f =
    fix-induction₁ P P⊥ P⨆ ([_⊥→_⊥].monotone-function (f ∗))

-- N-ary Scott induction.

module _ {a p} n
  (As : Fin n → Type a)
  (P : (∀ i → As i ⊥) → Type p)
  (P⊥ : P (λ _ → never))
  (P⨆ : ∀ ss → (∀ n → P (λ i → ss i [ n ])) → P (⨆ ∘ ss))
  where

  open PAF.N-ary n As (λ i → partiality-algebra (As i)) P P⊥ P⨆ public

  fix′-induction :
    (fs : ∀ i → As i → As i ⊥) →
    (∀ xs → P xs → P (λ i → xs i >>= fs i)) →
    P (fix′ ∘ fs)
  fix′-induction fs =
    fix-induction (λ i → [_⊥→_⊥].monotone-function (fs i ∗))

------------------------------------------------------------------------
-- The fixpoint combinator machinery instantiated with dependent
-- functions to the partiality monad

module _ {a b} (A : Type a) (B : A → Type b) where

  -- Partial function transformers.

  Trans : Type (a ⊔ b)
  Trans = ((x : A) → B x ⊥) → ((x : A) → B x ⊥)

  -- A partiality algebra.

  Pi : Partiality-algebra (a ⊔ b) (a ⊔ b) ((x : A) → B x)
  Pi = Π A (partiality-algebra ∘ B)

  -- Monotone partial function transformers.

  Trans-⊑ : Type (a ⊔ b)
  Trans-⊑ = [ Pi ⟶ Pi ]⊑

  private

    sanity-check : Trans-⊑ → Trans
    sanity-check = [_⟶_]⊑.function

  -- Partial function transformers that are ω-continuous.

  Trans-ω : Type (a ⊔ b)
  Trans-ω = [ Pi ⟶ Pi ]

module _ {a b} {A : Type a} {B : A → Type b} where

  module Trans-⊑ = [_⟶_]⊑ {P₁ = Pi A B} {P₂ = Pi A B}
  module Trans-ω = [_⟶_]  {P₁ = Pi A B} {P₂ = Pi A B}

  private
    module F = PAF.Fix {P = Pi A B}

  -- Applies an increasing sequence of functions to a value.

  at :
    (∃ λ (f : ℕ → (x : A) → B x ⊥) → ∀ n x → f n x ⊑ f (suc n) x) →
    (x : A) → ∃ λ (f : ℕ → B x ⊥) → ∀ n → f n ⊑ f (suc n)
  at = Pi.at (partiality-algebra ∘ B)

  -- Repeated application of a monotone partial function transformer
  -- to the least element.

  app→ : Trans-⊑ A B → ℕ → ((x : A) → B x ⊥)
  app→ = F.app

  -- The increasing sequence fix→-sequence f consists of the elements
  -- const never, Trans-⊑.function f (const never), and so on. This
  -- sequence is used in the implementation of fix→.

  fix→-sequence : Trans-⊑ A B →
                  Partiality-algebra.Increasing-sequence (Pi A B)
  fix→-sequence = F.fix-sequence

  -- A fixpoint combinator.

  fix→ : Trans-⊑ A B → ((x : A) → B x ⊥)
  fix→ = F.fix

  -- The fixpoint combinator produces fixpoints for ω-continuous
  -- arguments.

  fix→-is-fixpoint-combinator :
    (f : Trans-ω A B) →
    fix→ (Trans-ω.monotone-function f) ≡
    Trans-ω.function f (fix→ (Trans-ω.monotone-function f))
  fix→-is-fixpoint-combinator = F.fix-is-fixpoint-combinator

  -- The result of the fixpoint combinator is pointwise smaller than
  -- or equal to every "pointwise post-fixpoint".

  fix→-is-least :
    (f : Trans-⊑ A B) →
    ∀ g → (∀ x → Trans-⊑.function f g x ⊑ g x) →
      ∀ x → fix→ f x ⊑ g x
  fix→-is-least = F.fix-is-least

  -- Taking steps that are "twice as large" does not affect the end
  -- result.

  fix→-∘ : (f : Trans-⊑ A B) → fix→ (f ∘⊑ f) ≡ fix→ f
  fix→-∘ = F.fix-∘

-- N-ary Scott induction.

module _
  {a b p} n
  (As : Fin n → Type a)
  (Bs : (i : Fin n) → As i → Type b)
  (P : (∀ i → (x : As i) → Bs i x ⊥) → Type p)
  (P⊥ : P (λ _ _ → never))
  (P⨆ : (ss : ∀ i (x : As i) → Increasing-sequence (Bs i x)) →
        (∀ n → P (λ i xs → ss i xs [ n ])) →
        P (λ i xs → ⨆ (ss i xs)))
  (fs : ∀ i → Trans-⊑ (As i) (Bs i)) where

  private
    module N = PAF.N-ary n
                 (λ i → (x : As i) → Bs i x)
                 (λ i → Π (As i) (partiality-algebra ∘ Bs i))
                 P
                 P⊥
                 (λ _ → P⨆ _)
                 fs

  -- Generalised.

  fix→-induction′ :
    (∀ n → P (λ i → app→ (fs i) n) →
           P (λ i → app→ (fs i) (suc n))) →
    P (λ i → fix→ (fs i))
  fix→-induction′ = N.fix-induction′

  -- Basic.

  fix→-induction :
    ((gs : ∀ i (x : As i) → Bs i x ⊥) →
     P gs → P (λ i → Trans-⊑.function (fs i) (gs i))) →
    P (λ i → fix→ (fs i))
  fix→-induction = N.fix-induction

-- Unary Scott induction.

fix→-induction₁ :
  ∀ {a b p} {A : Type a} {B : A → Type b}
  (P : ((x : A) → B x ⊥) → Type p) →
  P (λ _ → never) →
  ((s : (x : A) → Increasing-sequence (B x)) →
   (∀ n → P (λ x → s x [ n ])) →
   P (λ x → ⨆ (s x))) →
  (f : Trans-⊑ A B) →
  (∀ g → P g → P (Trans-⊑.function f g)) →
  P (fix→ f)
fix→-induction₁ P P⊥ P⨆ = PAF.fix-induction₁ P P⊥ (λ _ → P⨆ _)

------------------------------------------------------------------------
-- Some combinators that can be used to construct ω-continuous partial
-- function transformers, for use with fix→

-- A type used by these combinators.

record Partial
         {a b c}
         (A : Type a) (B : A → Type b) (C : Type c) :
         Type (a ⊔ b ⊔ lsuc c) where
  field
    -- A function that is allowed to make "recursive calls" of type
    -- (x : A) → B x ⊥.

    function : ((x : A) → B x ⊥) → C ⊥

    -- The function must be monotone.

    monotone : ∀ {rec₁ rec₂} →
               (∀ x → rec₁ x ⊑ rec₂ x) →
               function rec₁ ⊑ function rec₂

  -- The function can be turned into an increasing sequence.

  sequence : ((x : A) → Increasing-sequence (B x)) →
             Increasing-sequence C
  sequence recs =
      (λ n → function (λ x → recs x [ n ]))
    , (λ n → monotone (λ x → increasing (recs x) n))

  field
    -- The function must be ω-continuous in the following sense.

    ω-continuous : (recs : (x : A) → Increasing-sequence (B x)) →
                   function (⨆ ∘ recs) ≡ ⨆ (sequence recs)

-- The first two arguments of Partial specify the domain and codomain
-- of "recursive calls".

rec : ∀ {a b} {A : Type a} {B : A → Type b} →
      (x : A) → Partial A B (B x)
rec x = record
  { function     = _$ x
  ; monotone     = _$ x
  ; ω-continuous = λ _ → refl
  }

-- Turns certain Partial-valued functions into monotone partial
-- function transformers.

transformer : ∀ {a b} {A : Type a} {B : A → Type b} →
              ((x : A) → Partial A B (B x)) → Trans-⊑ A B
transformer f = record
  { function = λ g     x → function (f x) g
  ; monotone = λ g₁⊑g₂ x → monotone (f x) g₁⊑g₂
  }
  where
  open Partial

-- Turns certain Partial-valued functions into ω-continuous partial
-- function transformers.

transformer-ω : ∀ {a b} {A : Type a} {B : A → Type b} →
                ((x : A) → Partial A B (B x)) → Trans-ω A B
transformer-ω f = record
  { monotone-function = transformer f
  ; ω-continuous      = λ _ → ⟨ext⟩ λ x → ω-continuous (f x) _
  }
  where
  open Partial

-- A fixpoint combinator.

fixP : ∀ {a b} {A : Type a} {B : A → Type b} →
       ((x : A) → Partial A B (B x)) → ((x : A) → B x ⊥)
fixP {A = A} {B} =
  ((x : A) → Partial A B (B x))  ↝⟨ transformer ⟩
  Trans-⊑ A B                    ↝⟨ fix→ ⟩□
  ((x : A) → B x ⊥)              □

-- The fixpoint combinator produces fixpoints.

fixP-is-fixpoint-combinator :
  ∀ {a b} {A : Type a} {B : A → Type b} →
  (f : (x : A) → Partial A B (B x)) →
  fixP f ≡ flip (Partial.function ∘ f) (fixP f)
fixP-is-fixpoint-combinator =
  fix→-is-fixpoint-combinator ∘ transformer-ω

-- The result of the fixpoint combinator is pointwise smaller than
-- or equal to every "pointwise post-fixpoint".

fixP-is-least :
  ∀ {a b} {A : Type a} {B : A → Type b}
  (f : (x : A) → Partial A B (B x)) →
  ∀ g → (∀ x → Partial.function (f x) g ⊑ g x) →
    ∀ x → fixP f x ⊑ g x
fixP-is-least = fix→-is-least ∘ transformer

-- Composition of certain Partial-valued functions.

infixr 40 _∘P_

_∘P_ :
  ∀ {a b} {A : Type a} {B : A → Type b} →
  ((x : A) → Partial A B (B x)) →
  ((x : A) → Partial A B (B x)) →
  ((x : A) → Partial A B (B x))
Partial.function     ((f ∘P g) x) = λ h →
                                      Partial.function (f x) λ y →
                                      Partial.function (g y) h
Partial.monotone     ((f ∘P g) x) = λ hyp →
                                      Partial.monotone (f x) λ y →
                                      Partial.monotone (g y) hyp
Partial.ω-continuous ((f ∘P g) x) = λ recs →
  function (f x) (λ y → function (g y) (⨆ ∘ recs))  ≡⟨ cong (function (f x)) (⟨ext⟩ λ y → ω-continuous (g y) recs) ⟩
  function (f x) (λ y → ⨆ (sequence (g y) recs))    ≡⟨ ω-continuous (f x) (λ y → sequence (g y) recs) ⟩∎
  ⨆ (sequence (f x) λ y → sequence (g y) recs)      ∎
  where
  open Partial

-- Taking steps that are "twice as large" does not affect the end
-- result.

fixP-∘ : ∀ {a b} {A : Type a} {B : A → Type b}
         (f : (x : A) → Partial A B (B x)) →
         fixP (f ∘P f) ≡ fixP f
fixP-∘ f =
  fix→ (transformer (f ∘P f))            ≡⟨⟩
  fix→ (transformer f ∘⊑ transformer f)  ≡⟨ fix→-∘ (transformer f) ⟩∎
  fix→ (transformer f)                   ∎

-- N-ary Scott induction.

module _
  {a b p} n
  (As : Fin n → Type a)
  (Bs : (i : Fin n) → As i → Type b)
  (P : (∀ i (x : As i) → Bs i x ⊥) → Type p)
  (P⊥ : P (λ _ _ → never))
  (P⨆ : (ss : ∀ i (x : As i) → Increasing-sequence (Bs i x)) →
        (∀ n → P (λ i xs → ss i xs [ n ])) →
        P (λ i xs → ⨆ (ss i xs)))
  (fs : ∀ i (x : As i) → Partial (As i) (Bs i) (Bs i x)) where

  -- Generalised.

  fixP-induction′ :
    (∀ n → P (λ i → app→ (transformer (fs i)) n) →
           P (λ i → app→ (transformer (fs i)) (suc n))) →
    P (λ i → fixP (fs i))
  fixP-induction′ =
    fix→-induction′ n As Bs P P⊥ P⨆ (transformer ∘ fs)

  -- Basic.

  fixP-induction :
    ((gs : ∀ i (x : As i) → Bs i x ⊥) →
     P gs → P (λ i xs → Partial.function (fs i xs) (gs i))) →
    P (λ i → fixP (fs i))
  fixP-induction =
    fix→-induction n As Bs P P⊥ P⨆ (transformer ∘ fs)

-- Unary Scott induction.

fixP-induction₁ :
  ∀ {a b p} {A : Type a} {B : A → Type b}
  (P : ((x : A) → B x ⊥) → Type p) →
  P (λ _ → never) →
  ((s : (x : A) → Increasing-sequence (B x)) →
   (∀ n → P (λ x → s x [ n ])) →
   P (λ x → ⨆ (s x))) →
  (f : (x : A) → Partial A B (B x)) →
  (∀ g → P g → P (λ x → Partial.function (f x) g)) →
  P (fixP f)
fixP-induction₁ P P⊥ P⨆ f =
  fix→-induction₁ P P⊥ P⨆ (transformer f)

-- Equality characterisation lemma for Partial.

equality-characterisation-Partial :
  ∀ {a b c} {A : Type a} {B : A → Type b} {C : Type c}
    {f g : Partial A B C} →
  (∀ rec → Partial.function f rec ≡ Partial.function g rec) ↔
  f ≡ g
equality-characterisation-Partial {f = f} {g} =
  (∀ rec → function f rec ≡ function g rec)  ↔⟨ Eq.extensionality-isomorphism bad-ext ⟩
  function f ≡ function g                    ↝⟨ ignore-propositional-component
                                                  (Σ-closure 1
                                                     (implicit-Π-closure ext 1 λ _ →
                                                      implicit-Π-closure ext 1 λ _ →
                                                      Π-closure          ext 1 λ _ →
                                                      ⊑-propositional) λ _ →
                                                     Π-closure ext 1 λ _ →
                                                     ⊥-is-set) ⟩
  (function f , _) ≡ (function g , _)        ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ lemma) ⟩□
  f ≡ g                                      □
  where
  open Partial

  lemma :
    Partial _ _ _
      ↔
    ∃ λ f →
    ∃ λ (_ : ∀ {rec₁ rec₂} → (∀ x → rec₁ x ⊑ _) → f rec₁ ⊑ _) → _
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ x → function x , monotone x , ω-continuous x
        ; from = λ { (f , m , ω) → record
                      { function     = f
                      ; monotone     = λ {rec₁ rec₂} → m {rec₁ = rec₁} {rec₂ = rec₂}
                      ; ω-continuous = ω
                      } }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }

-- "Non-recursive" computations can be converted into possibly
-- recursive ones.

non-recursive :
  ∀ {a b c} {A : Type a} {B : A → Type b} {C : Type c} →
  C ⊥ → Partial A B C
non-recursive x = record
  { function     = const x
  ; monotone     = const (x ■)
  ; ω-continuous = λ _ →
      x             ≡⟨ sym ⨆-const ⟩∎
      ⨆ (constˢ x)  ∎
  }

instance

  -- Partial A B is a monad.

  partial-raw-monad : ∀ {a b c} {A : Type a} {B : A → Type b} →
                      Raw-monad (Partial {c = c} A B)
  Raw-monad.return partial-raw-monad x   = non-recursive (return x)
  Raw-monad._>>=_  partial-raw-monad x f = record
    { function     = λ rec →
                       function x rec >>=′ λ y →
                       function (f y) rec
    ; monotone     = λ rec⊑rec →
                       monotone x rec⊑rec >>=-mono λ y →
                       monotone (f y) rec⊑rec
    ; ω-continuous = λ recs →
        (function x (⨆ ∘ recs) >>=′ λ y → function (f y) (⨆ ∘ recs))     ≡⟨ cong₂ _>>=′_ (ω-continuous x recs)
                                                                                (⟨ext⟩ λ y → ω-continuous (f y) recs) ⟩
        (⨆ (sequence x recs) >>=′ λ y → ⨆ (sequence (f y) recs))         ≡⟨ ⨆->>= ⟩

        ⨆ ( (λ n →
               function x (λ z → recs z [ n ]) >>=′ λ y →
               ⨆ (sequence (f y) recs))
          , _
          )                                                              ≡⟨ ⨆>>=⨆≡⨆>>= (sequence x recs)
                                                                                (λ y → sequence (f y) recs) ⟩∎
        ⨆ ( (λ n → function x (λ z → recs z [ n ]) >>=′ λ y →
                   function (f y) (λ z → recs z [ n ]))
          , _
          )                                                              ∎
    }
    where
    open Partial

  partial-monad : ∀ {a b c} {A : Type a} {B : A → Type b} →
                  Monad (Partial {c = c} A B)
  Monad.raw-monad partial-monad = partial-raw-monad

  Monad.left-identity partial-monad _ f =
    _↔_.to equality-characterisation-Partial
      (λ h → left-identity _ (λ y → Partial.function (f y) h))

  Monad.right-identity partial-monad _ =
    _↔_.to equality-characterisation-Partial
      (λ _ → right-identity _)

  Monad.associativity partial-monad x _ _ =
    _↔_.to equality-characterisation-Partial
      (λ h → associativity (Partial.function x h) _ _)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.ChainComplex
open import cohomology.Theory

module cw.cohomology.AxiomaticIsoCellular (OT : OrdinaryTheory lzero) where

  open OrdinaryTheory OT
  open import cw.cohomology.cellular.ChainComplex
  import cw.cohomology.reconstructed.cochain.Complex OT as RCC
  open import cw.cohomology.ReconstructedCohomologyGroups OT
  open import cw.cohomology.ReconstructedCochainsEquivCellularCochains OT

  axiomatic-iso-cellular : ∀ m {n} (⊙fin-skel : ⊙FinSkeleton n)
    →  C m ⊙⟦ ⊙⦉ ⊙fin-skel ⦊ ⟧
    ≃ᴳ cohomology-group
        (cochain-complex ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
          (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
          (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))
          (C2-abgroup 0))
        m
  axiomatic-iso-cellular m ⊙fin-skel =
      C m ⊙⟦ ⊙⦉ ⊙fin-skel ⦊ ⟧
        ≃ᴳ⟨ reconstructed-cohomology-group m ⊙⦉ ⊙fin-skel ⦊
              (⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero) ⟩
      cohomology-group (RCC.cochain-complex ⊙⦉ ⊙fin-skel ⦊) m
        ≃ᴳ⟨ frc-iso-fcc ⊙fin-skel m ⟩
      cohomology-group
        (cochain-complex ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
          (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
          (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))
          (C2-abgroup 0))
        m
        ≃ᴳ∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import System.IO using ( _>>_ ; putStr ; commit )

module System.IO.Examples.HelloWorld where

main = putStr "Hello, World\n" >> commit

max_stars_repo_name: PushpneetSingh/Hello-world

max_issues_repo_name: PushpneetSingh/Hello-world

max_forks_repo_name: PushpneetSingh/Hello-world


text:
------------------------------------------------------------------------
-- Grammars defined as functions from non-terminals to productions
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Grammar.Non-terminal where

open import Algebra
open import Category.Monad
open import Data.Bool
open import Data.Bool.Properties
open import Data.Char
open import Data.Empty
open import Data.List hiding (unfold)
open import Data.List.Properties
open import Data.Maybe hiding (_>>=_)
open import Data.Maybe.Categorical as MaybeC
open import Data.Nat
open import Data.Product as Product
open import Data.Unit
open import Function
open import Level using (Lift; lift)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Relation.Nullary
open import Tactic.MonoidSolver

private
  module LM {A : Set} = Monoid (++-monoid A)
  open module MM {f} = RawMonadPlus (MaybeC.monadPlus {f = f})
    using ()
    renaming (_<$>_ to _<$>M_; _⊛_ to _⊛M_;
              _>>=_ to _>>=M_; _∣_ to _∣M_)

open import Utilities

------------------------------------------------------------------------
-- Grammars

-- Productions. (Note that productions can contain choices.)

infix  30 _⋆
infixl 20 _⊛_ _<⊛_
infixl 15 _>>=_
infixl 10 _∣_

data Prod (NT : Set → Set₁) : Set → Set₁ where
  !      : ∀ {A} → NT A → Prod NT A
  fail   : ∀ {A} → Prod NT A
  return : ∀ {A} → A → Prod NT A
  token  : Prod NT Char
  tok    : Char → Prod NT Char
  _⊛_    : ∀ {A B} → Prod NT (A → B) → Prod NT A → Prod NT B
  _<⊛_   : ∀ {A B} → Prod NT A → Prod NT B → Prod NT A
  _>>=_  : ∀ {A B} → Prod NT A → (A → Prod NT B) → Prod NT B
  _∣_    : ∀ {A} → Prod NT A → Prod NT A → Prod NT A
  _⋆     : ∀ {A} → Prod NT A → Prod NT (List A)

-- Grammars.

Grammar : (Set → Set₁) → Set₁
Grammar NT = ∀ A → NT A → Prod NT A

-- An empty non-terminal type.

Empty-NT : Set → Set₁
Empty-NT _ = Lift _ ⊥

-- A corresponding grammar.

empty-grammar : Grammar Empty-NT
empty-grammar _ (lift ())

------------------------------------------------------------------------
-- Production combinators

-- Map.

infixl 20 _<$>_ _<$_

_<$>_ : ∀ {NT A B} → (A → B) → Prod NT A → Prod NT B
f <$> p = return f ⊛ p

_<$_ : ∀ {NT A B} → A → Prod NT B → Prod NT A
x <$ p = return x <⊛ p

-- Various sequencing operators.

infixl 20 _⊛>_
infixl 15 _>>_

_>>_ : ∀ {NT A B} → Prod NT A → Prod NT B → Prod NT B
p₁ >> p₂ = (λ _ x → x) <$> p₁ ⊛ p₂

_⊛>_ : ∀ {NT A B} → Prod NT A → Prod NT B → Prod NT B
_⊛>_ = _>>_

-- Kleene plus.

infix 30 _+

_+ : ∀ {NT A} → Prod NT A → Prod NT (List A)
p + = _∷_ <$> p ⊛ p ⋆

-- Elements separated by something.

infixl 18 _sep-by_

_sep-by_ : ∀ {NT A B} → Prod NT A → Prod NT B → Prod NT (List A)
g sep-by sep = _∷_ <$> g ⊛ (sep >> g) ⋆

-- A production for tokens satisfying a given predicate.

if-true : ∀ {NT} (b : Bool) → Prod NT (T b)
if-true true  = return tt
if-true false = fail

sat : ∀ {NT} (p : Char → Bool) → Prod NT (∃ λ t → T (p t))
sat p = token >>= λ t → _,_ t <$> if-true (p t)

-- A production for whitespace.

whitespace : ∀ {NT} → Prod NT Char
whitespace = tok ' ' ∣ tok '\n'

-- A production for a given string.

string : ∀ {NT} → List Char → Prod NT (List Char)
string []      = return []
string (t ∷ s) = _∷_ <$> tok t ⊛ string s

-- A production for the given string, possibly followed by some
-- whitespace.

symbol : ∀ {NT} → List Char → Prod NT (List Char)
symbol s = string s <⊛ whitespace ⋆

------------------------------------------------------------------------
-- Semantics

infix 4 [_]_∈_·_

data [_]_∈_·_ {NT : Set → Set₁} (g : Grammar NT) :
              ∀ {A} → A → Prod NT A → List Char → Set₁ where
  !-sem      : ∀ {A} {nt : NT A} {x s} →
               [ g ] x ∈ g A nt · s → [ g ] x ∈ ! nt · s
  return-sem : ∀ {A} {x : A} → [ g ] x ∈ return x · []
  token-sem  : ∀ {t} → [ g ] t ∈ token · [ t ]
  tok-sem    : ∀ {t} → [ g ] t ∈ tok t · [ t ]
  ⊛-sem      : ∀ {A B} {p₁ : Prod NT (A → B)} {p₂ : Prod NT A}
                 {f x s₁ s₂} →
               [ g ] f ∈ p₁ · s₁ → [ g ] x ∈ p₂ · s₂ →
               [ g ] f x ∈ p₁ ⊛ p₂ · s₁ ++ s₂
  <⊛-sem     : ∀ {A B} {p₁ : Prod NT A} {p₂ : Prod NT B} {x y s₁ s₂} →
               [ g ] x ∈ p₁ · s₁ → [ g ] y ∈ p₂ · s₂ →
               [ g ] x ∈ p₁ <⊛ p₂ · s₁ ++ s₂
  >>=-sem    : ∀ {A B} {p₁ : Prod NT A} {p₂ : A → Prod NT B}
                 {x y s₁ s₂} →
               [ g ] x ∈ p₁ · s₁ → [ g ] y ∈ p₂ x · s₂ →
               [ g ] y ∈ p₁ >>= p₂ · s₁ ++ s₂
  left-sem   : ∀ {A} {p₁ p₂ : Prod NT A} {x s} →
               [ g ] x ∈ p₁ · s → [ g ] x ∈ p₁ ∣ p₂ · s
  right-sem  : ∀ {A} {p₁ p₂ : Prod NT A} {x s} →
               [ g ] x ∈ p₂ · s → [ g ] x ∈ p₁ ∣ p₂ · s
  ⋆-[]-sem   : ∀ {A} {p : Prod NT A} →
               [ g ] [] ∈ p ⋆ · []
  ⋆-+-sem    : ∀ {A} {p : Prod NT A} {xs s} →
               [ g ] xs ∈ p + · s → [ g ] xs ∈ p ⋆ · s

-- Cast lemma.

cast : ∀ {NT g A} {p : Prod NT A} {x s₁ s₂} →
       s₁ ≡ s₂ → [ g ] x ∈ p · s₁ → [ g ] x ∈ p · s₂
cast P.refl = id

------------------------------------------------------------------------
-- Semantics combinators

<$>-sem : ∀ {NT} {g : Grammar NT} {A B} {f : A → B} {x p s} →
          [ g ] x ∈ p · s → [ g ] f x ∈ f <$> p · s
<$>-sem x∈ = ⊛-sem return-sem x∈

<$-sem : ∀ {NT g A B} {p : Prod NT B} {x : A} {y s} →
         [ g ] y ∈ p · s → [ g ] x ∈ x <$ p · s
<$-sem y∈ = <⊛-sem return-sem y∈

>>-sem : ∀ {NT g A B} {p₁ : Prod NT A} {p₂ : Prod NT B} {x y s₁ s₂} →
         [ g ] x ∈ p₁ · s₁ → [ g ] y ∈ p₂ · s₂ →
         [ g ] y ∈ p₁ >> p₂ · s₁ ++ s₂
>>-sem x∈ y∈ = ⊛-sem (⊛-sem return-sem x∈) y∈

⊛>-sem : ∀ {NT g A B} {p₁ : Prod NT A} {p₂ : Prod NT B} {x y s₁ s₂} →
         [ g ] x ∈ p₁ · s₁ → [ g ] y ∈ p₂ · s₂ →
         [ g ] y ∈ p₁ ⊛> p₂ · s₁ ++ s₂
⊛>-sem = >>-sem

+-sem : ∀ {NT g A} {p : Prod NT A} {x xs s₁ s₂} →
        [ g ] x ∈ p · s₁ → [ g ] xs ∈ p ⋆ · s₂ →
        [ g ] x ∷ xs ∈ p + · s₁ ++ s₂
+-sem x∈ xs∈ = ⊛-sem (⊛-sem return-sem x∈) xs∈

⋆-∷-sem : ∀ {NT g A} {p : Prod NT A} {x xs s₁ s₂} →
          [ g ] x ∈ p · s₁ → [ g ] xs ∈ p ⋆ · s₂ →
          [ g ] x ∷ xs ∈ p ⋆ · s₁ ++ s₂
⋆-∷-sem x∈ xs∈ = ⋆-+-sem (+-sem x∈ xs∈)

⋆-⋆-sem : ∀ {NT g A} {p : Prod NT A} {xs₁ xs₂ s₁ s₂} →
          [ g ] xs₁ ∈ p ⋆ · s₁ → [ g ] xs₂ ∈ p ⋆ · s₂ →
          [ g ] xs₁ ++ xs₂ ∈ p ⋆ · s₁ ++ s₂
⋆-⋆-sem ⋆-[]-sem xs₂∈ = xs₂∈
⋆-⋆-sem (⋆-+-sem (⊛-sem (⊛-sem {s₂ = s₁} return-sem x∈) xs₁∈)) xs₂∈ =
  cast (P.sym $ LM.assoc s₁ _ _)
       (⋆-∷-sem x∈ (⋆-⋆-sem xs₁∈ xs₂∈))

+-∷-sem : ∀ {NT g A} {p : Prod NT A} {x xs s₁ s₂} →
          [ g ] x ∈ p · s₁ → [ g ] xs ∈ p + · s₂ →
          [ g ] x ∷ xs ∈ p + · s₁ ++ s₂
+-∷-sem x∈ xs∈ = +-sem x∈ (⋆-+-sem xs∈)

+-⋆-sem : ∀ {NT g A} {p : Prod NT A} {xs₁ xs₂ s₁ s₂} →
          [ g ] xs₁ ∈ p + · s₁ → [ g ] xs₂ ∈ p ⋆ · s₂ →
          [ g ] xs₁ ++ xs₂ ∈ p + · s₁ ++ s₂
+-⋆-sem (⊛-sem (⊛-sem {s₂ = s₁} return-sem x∈) xs₁∈) xs₂∈ =
  cast (P.sym $ LM.assoc s₁ _ _)
       (+-sem x∈ (⋆-⋆-sem xs₁∈ xs₂∈))

sep-by-sem-singleton :
  ∀ {NT g A B} {p : Prod NT A} {sep : Prod NT B} {x s} →
  [ g ] x ∈ p · s → [ g ] [ x ] ∈ p sep-by sep · s
sep-by-sem-singleton x∈ =
  cast (proj₂ LM.identity _) (⊛-sem (<$>-sem x∈) ⋆-[]-sem)

sep-by-sem-∷ :
  ∀ {NT g A B} {p : Prod NT A} {sep : Prod NT B} {x y xs s₁ s₂ s₃} →
  [ g ] x ∈ p · s₁ → [ g ] y ∈ sep · s₂ → [ g ] xs ∈ p sep-by sep · s₃ →
  [ g ] x ∷ xs ∈ p sep-by sep · s₁ ++ s₂ ++ s₃
sep-by-sem-∷ {s₂ = s₂} x∈ y∈ (⊛-sem (⊛-sem return-sem x′∈) xs∈) =
  ⊛-sem (<$>-sem x∈)
        (cast (LM.assoc s₂ _ _) (⋆-∷-sem (>>-sem y∈ x′∈) xs∈))

if-true-sem : ∀ {NT} {g : Grammar NT} {b}
              (t : T b) → [ g ] t ∈ if-true b · []
if-true-sem {b = true}  _  = return-sem
if-true-sem {b = false} ()

sat-sem : ∀ {NT} {g : Grammar NT} {p t}
          (pt : T (p t)) → [ g ] (t , pt) ∈ sat p · [ t ]
sat-sem pt = >>=-sem token-sem (<$>-sem (if-true-sem pt))

whitespace-sem-space : ∀ {NT} {g : Grammar NT} →
                       [ g ] ' ' ∈ whitespace · [ ' ' ]
whitespace-sem-space = left-sem tok-sem

whitespace-sem-newline : ∀ {NT} {g : Grammar NT} →
                         [ g ] '\n' ∈ whitespace · [ '\n' ]
whitespace-sem-newline = right-sem tok-sem

string-sem : ∀ {NT} {g : Grammar NT} {s} →
             [ g ] s ∈ string s · s
string-sem {s = []}    = return-sem
string-sem {s = t ∷ s} = ⊛-sem (<$>-sem tok-sem) string-sem

symbol-sem : ∀ {NT} {g : Grammar NT} {s s′ s″} →
             [ g ] s″ ∈ whitespace ⋆ · s′ → [ g ] s ∈ symbol s · s ++ s′
symbol-sem s″∈ = <⊛-sem string-sem s″∈

------------------------------------------------------------------------
-- Some production transformers

-- Replaces all non-terminals with non-terminal-free productions.

replace : ∀ {NT A} → (∀ {A} → NT A → Prod Empty-NT A) →
          Prod NT A → Prod Empty-NT A
replace f (! nt)      = f nt
replace f fail        = fail
replace f (return x)  = return x
replace f token       = token
replace f (tok x)     = tok x
replace f (p₁ ⊛ p₂)   = replace f p₁ ⊛ replace f p₂
replace f (p₁ <⊛ p₂)  = replace f p₁ <⊛ replace f p₂
replace f (p₁ >>= p₂) = replace f p₁ >>= λ x → replace f (p₂ x)
replace f (p₁ ∣ p₂)   = replace f p₁ ∣ replace f p₂
replace f (p ⋆)       = replace f p ⋆

-- A lemma relating the resulting production with the original one in
-- case every non-terminal is replaced by fail.

replace-fail :
  ∀ {NT A g} (p : Prod NT A) {x s} →
  [ empty-grammar ] x ∈ replace (λ _ → fail) p · s →
  [ g             ] x ∈                      p · s
replace-fail (! nt)      ()
replace-fail fail        ()
replace-fail (return x)  return-sem      = return-sem
replace-fail token       token-sem       = token-sem
replace-fail (tok t)     tok-sem         = tok-sem
replace-fail (p₁ ⊛ p₂)   (⊛-sem f∈ x∈)   = ⊛-sem   (replace-fail p₁ f∈) (replace-fail p₂     x∈)
replace-fail (p₁ <⊛ p₂)  (<⊛-sem x∈ y∈)  = <⊛-sem  (replace-fail p₁ x∈) (replace-fail p₂     y∈)
replace-fail (p₁ >>= p₂) (>>=-sem x∈ y∈) = >>=-sem (replace-fail p₁ x∈) (replace-fail (p₂ _) y∈)
replace-fail (p₁ ∣ p₂)   (left-sem  x∈)  = left-sem  (replace-fail p₁ x∈)
replace-fail (p₁ ∣ p₂)   (right-sem x∈)  = right-sem (replace-fail p₂ x∈)
replace-fail (p ⋆)       ⋆-[]-sem        = ⋆-[]-sem
replace-fail (p ⋆)       (⋆-+-sem xs∈)   = ⋆-+-sem (replace-fail (p +) xs∈)

-- Unfolds every non-terminal. At most n /nested/ unfoldings are
-- performed.

unfold : ∀ {NT A} → (n : ℕ) → Grammar NT → Prod NT A → Prod NT A
unfold zero    g p           = p
unfold (suc n) g (! nt)      = unfold n g (g _ nt)
unfold n       g fail        = fail
unfold n       g (return x)  = return x
unfold n       g token       = token
unfold n       g (tok x)     = tok x
unfold n       g (p₁ ⊛ p₂)   = unfold n g p₁ ⊛ unfold n g p₂
unfold n       g (p₁ <⊛ p₂)  = unfold n g p₁ <⊛ unfold n g p₂
unfold n       g (p₁ >>= p₂) = unfold n g p₁ >>= λ x → unfold n g (p₂ x)
unfold n       g (p₁ ∣ p₂)   = unfold n g p₁ ∣ unfold n g p₂
unfold n       g (p ⋆)       = unfold n g p ⋆

-- Unfold is semantics-preserving.

unfold-to : ∀ {NT A} {g : Grammar NT} {x s} n (p : Prod NT A) →
            [ g ] x ∈ p · s → [ g ] x ∈ unfold n g p · s
unfold-to zero    p           x∈              = x∈
unfold-to (suc n) (! nt)      (!-sem x∈)      = unfold-to n _ x∈
unfold-to (suc n) fail        x∈              = x∈
unfold-to (suc n) (return x)  x∈              = x∈
unfold-to (suc n) token       x∈              = x∈
unfold-to (suc n) (tok x)     x∈              = x∈
unfold-to (suc n) (p₁ ⊛ p₂)   (⊛-sem f∈ x∈)   = ⊛-sem (unfold-to (suc n) p₁ f∈)
                                                      (unfold-to (suc n) p₂ x∈)
unfold-to (suc n) (p₁ <⊛ p₂)  (<⊛-sem x∈ y∈)  = <⊛-sem (unfold-to (suc n) p₁ x∈)
                                                       (unfold-to (suc n) p₂ y∈)
unfold-to (suc n) (p₁ >>= p₂) (>>=-sem x∈ y∈) = >>=-sem (unfold-to (suc n) p₁ x∈)
                                                        (unfold-to (suc n) (p₂ _) y∈)
unfold-to (suc n) (p₁ ∣ p₂)   (left-sem x∈)   = left-sem  (unfold-to (suc n) p₁ x∈)
unfold-to (suc n) (p₁ ∣ p₂)   (right-sem x∈)  = right-sem (unfold-to (suc n) p₂ x∈)
unfold-to (suc n) (p ⋆)       ⋆-[]-sem        = ⋆-[]-sem
unfold-to (suc n) (p ⋆)       (⋆-+-sem xs∈)   = ⋆-+-sem (unfold-to (suc n) (p +) xs∈)

unfold-from : ∀ {NT A} {g : Grammar NT} {x s} n (p : Prod NT A) →
              [ g ] x ∈ unfold n g p · s → [ g ] x ∈ p · s
unfold-from zero    p           x∈              = x∈
unfold-from (suc n) (! nt)      x∈              = !-sem (unfold-from n _ x∈)
unfold-from (suc n) fail        x∈              = x∈
unfold-from (suc n) (return x)  x∈              = x∈
unfold-from (suc n) token       x∈              = x∈
unfold-from (suc n) (tok x)     x∈              = x∈
unfold-from (suc n) (p₁ ⊛ p₂)   (⊛-sem f∈ x∈)   = ⊛-sem (unfold-from (suc n) p₁ f∈)
                                                        (unfold-from (suc n) p₂ x∈)
unfold-from (suc n) (p₁ <⊛ p₂)  (<⊛-sem x∈ y∈)  = <⊛-sem (unfold-from (suc n) p₁ x∈)
                                                         (unfold-from (suc n) p₂ y∈)
unfold-from (suc n) (p₁ >>= p₂) (>>=-sem x∈ y∈) = >>=-sem (unfold-from (suc n) p₁ x∈)
                                                          (unfold-from (suc n) (p₂ _) y∈)
unfold-from (suc n) (p₁ ∣ p₂)   (left-sem x∈)   = left-sem  (unfold-from (suc n) p₁ x∈)
unfold-from (suc n) (p₁ ∣ p₂)   (right-sem x∈)  = right-sem (unfold-from (suc n) p₂ x∈)
unfold-from (suc n) (p ⋆)       ⋆-[]-sem        = ⋆-[]-sem
unfold-from (suc n) (p ⋆)       (⋆-+-sem xs∈)   = ⋆-+-sem (unfold-from (suc n) (p +) xs∈)

------------------------------------------------------------------------
-- Nullability

-- A production is nullable (with respect to a given grammar) if the
-- empty string is a member of the language defined by the production.

Nullable : ∀ {NT A} → Grammar NT → Prod NT A → Set₁
Nullable g p = ∃ λ x → [ g ] x ∈ p · []

-- Nullability is not decidable, not even for productions without
-- non-terminals. If nullability were decidable, then we could decide
-- if a given function of type ℕ → Bool always returns false.

nullability-not-decidable :
  (∀ {A} (p : Prod Empty-NT A) → Dec (Nullable empty-grammar p)) →
  (f : ℕ → Bool) → Dec (∀ n → f n ≡ false)
nullability-not-decidable dec f = goal
  where
  p : Prod Empty-NT ℕ
  p = return tt ⋆ >>= λ tts →
      let n = length tts in
      if f n then return n else fail

  true-lemma : ∀ {n s} → [ empty-grammar ] n ∈ p · s → f n ≡ true
  true-lemma (>>=-sem {x = tts} _ _)
    with f (length tts) | P.inspect f (length tts)
  true-lemma (>>=-sem _ return-sem) | true  | P.[ fn≡true ] = fn≡true
  true-lemma (>>=-sem _ ())         | false | _

  no-lemma : ∀ {n} → f n ≡ true → ¬ (∀ n → f n ≡ false)
  no-lemma {n} ≡true ≡false with begin
    true   ≡⟨ P.sym ≡true ⟩
    f n    ≡⟨ ≡false n ⟩
    false  ∎
    where open P.≡-Reasoning
  ... | ()

  to-tts : ℕ → List ⊤
  to-tts n = replicate n tt

  n∈₁ : ∀ n → [ empty-grammar ] to-tts n ∈ return tt ⋆ · []
  n∈₁ zero    = ⋆-[]-sem
  n∈₁ (suc n) = ⋆-∷-sem return-sem (n∈₁ n)

  n∈₂ : ∀ n → f n ≡ true →
        let n′ = length (replicate n tt) in
        [ empty-grammar ] n ∈ if f n′ then return n′ else fail · []
  n∈₂ n fn≡true rewrite length-replicate n {x = tt} | fn≡true =
    return-sem

  yes-lemma : ∀ n → ¬ ([ empty-grammar ] n ∈ p · []) → f n ≢ true
  yes-lemma n n∉ fn≡true = n∉ (>>=-sem (n∈₁ n) (n∈₂ n fn≡true))

  goal : Dec (∀ n → f n ≡ false)
  goal with dec p
  ... | yes (_ , n∈) = no (no-lemma (true-lemma n∈))
  ... | no ¬[]∈      = yes λ n → ¬-not (yes-lemma n (¬[]∈ ∘ -,_))

-- However, we can implement a procedure that either proves that a
-- production is nullable, or returns "don't know" as the answer.
--
-- Note that, in the case of bind, the second argument is only applied
-- to one input—the first argument could give rise to infinitely many
-- results (as in the example above).
--
-- Note also that no attempt is made to memoise non-terminals—the
-- grammar could consist of an infinite number of non-terminals.
-- Instead the grammar is unfolded a certain number of times (n).
-- Memoisation still seems like a useful heuristic, but requires that
-- equality of non-terminals is decidable.

nullable? : ∀ {NT A} (n : ℕ) (g : Grammar NT) (p : Prod NT A) →
            Maybe (Nullable g p)
nullable? {NT} n g p =
  Product.map id (unfold-from n _) <$>M null? (unfold n g p)
  where
  null? : ∀ {A} (p : Prod NT A) → Maybe (Nullable g p)
  null? (! nt)        = nothing
  null? fail          = nothing
  null? token         = nothing
  null? (tok t)       = nothing
  null? (return x)    = just (x , return-sem)
  null? (p ⋆)         = just ([] , ⋆-[]-sem)
  null? (p₁ ⊛ p₂)     = Product.zip _$_   ⊛-sem  <$>M null? p₁ ⊛M null? p₂
  null? (p₁ <⊛ p₂)    = Product.zip const <⊛-sem <$>M null? p₁ ⊛M null? p₂
  null? (p₁ >>= p₂)   = null? p₁                  >>=M λ { (x , x∈) →
                        null? (p₂ x)              >>=M λ { (y , y∈) →
                        just (y , >>=-sem x∈ y∈)  }}
  null? (p₁ ∣ p₂)     = (Product.map id left-sem  <$>M null? p₁)
                          ∣M
                        (Product.map id right-sem <$>M null? p₂)

------------------------------------------------------------------------
-- Detecting the whitespace combinator

-- A predicate for the whitespace combinator.

data Is-whitespace {NT} : ∀ {A} → Prod NT A → Set₁ where
  is-whitespace : Is-whitespace whitespace

-- Detects the whitespace combinator.

is-whitespace? : ∀ {NT A} (p : Prod NT A) → Maybe (Is-whitespace p)
is-whitespace? {NT} (tok ' ' ∣ p) = helper p P.refl
  where
  helper : ∀ {A} (p : Prod NT A) (eq : A ≡ Char) →
           Maybe (Is-whitespace (tok ' ' ∣ P.subst (Prod NT) eq p))
  helper (tok '\n') P.refl = just is-whitespace
  helper _          _      = nothing

is-whitespace? _ = nothing

------------------------------------------------------------------------
-- Trailing whitespace

-- A predicate for productions that can "swallow" extra trailing
-- whitespace.

Trailing-whitespace : ∀ {NT A} → Grammar NT → Prod NT A → Set₁
Trailing-whitespace g p =
  ∀ {x s} → [ g ] x ∈ p <⊛ whitespace ⋆ · s → [ g ] x ∈ p · s

-- A heuristic procedure that either proves that a production can
-- swallow trailing whitespace, or returns "don't know" as the answer.

trailing-whitespace :
  ∀ {NT A} (n : ℕ) (g : Grammar NT) (p : Prod NT A) →
  Maybe (Trailing-whitespace g p)
trailing-whitespace {NT} n g p =
  convert ∘ unfold-lemma <$>M trailing? (unfold n g p)
  where
  -- An alternative formulation of Trailing-whitespace.

  Trailing-whitespace′ : ∀ {NT A} → Grammar NT → Prod NT A → Set₁
  Trailing-whitespace′ g p =
    ∀ {x s₁ s₂ s} →
    [ g ] x ∈ p · s₁ → [ g ] s ∈ whitespace ⋆ · s₂ →
    [ g ] x ∈ p · s₁ ++ s₂

  convert : ∀ {NT A} {g : Grammar NT} {p : Prod NT A} →
            Trailing-whitespace′ g p → Trailing-whitespace g p
  convert t (<⊛-sem x∈ w) = t x∈ w

  ++-lemma : ∀ s₁ {s₂} → (s₁ ++ s₂) ++ [] ≡ (s₁ ++ []) ++ s₂
  ++-lemma _ = solve (++-monoid Char)

  unfold-lemma : Trailing-whitespace′ g (unfold n g p) →
                 Trailing-whitespace′ g p
  unfold-lemma t x∈ white = unfold-from n _ (t (unfold-to n _ x∈) white)

  ⊛-return-lemma :
    ∀ {A B} {p : Prod NT (A → B)} {x} →
    Trailing-whitespace′ g p →
    Trailing-whitespace′ g (p ⊛ return x)
  ⊛-return-lemma t (⊛-sem {s₁ = s₁} f∈ return-sem) white =
    cast (++-lemma s₁) (⊛-sem (t f∈ white) return-sem)

  +-lemma :
    ∀ {A} {p : Prod NT A} →
    Trailing-whitespace′ g p →
    Trailing-whitespace′ g (p +)
  +-lemma t (⊛-sem (⊛-sem {s₂ = s₁} return-sem x∈) ⋆-[]-sem) white =
    cast (++-lemma s₁) (+-sem (t x∈ white) ⋆-[]-sem)
  +-lemma t (⊛-sem (⊛-sem {s₂ = s₁} return-sem x∈) (⋆-+-sem xs∈))
          white =
    cast (P.sym $ LM.assoc s₁ _ _)
         (+-∷-sem x∈ (+-lemma t xs∈ white))

  ⊛-⋆-lemma :
    ∀ {A B} {p₁ : Prod NT (List A → B)} {p₂ : Prod NT A} →
    Trailing-whitespace′ g p₁ →
    Trailing-whitespace′ g p₂ →
    Trailing-whitespace′ g (p₁ ⊛ p₂ ⋆)
  ⊛-⋆-lemma t₁ t₂ (⊛-sem {s₁ = s₁} f∈ ⋆-[]-sem) white =
    cast (++-lemma s₁) (⊛-sem (t₁ f∈ white) ⋆-[]-sem)
  ⊛-⋆-lemma t₁ t₂ (⊛-sem {s₁ = s₁} f∈ (⋆-+-sem xs∈)) white =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛-sem f∈ (⋆-+-sem (+-lemma t₂ xs∈ white)))

  ⊛-∣-lemma : ∀ {A B} {p₁ : Prod NT (A → B)} {p₂ p₃ : Prod NT A} →
              Trailing-whitespace′ g (p₁ ⊛ p₂) →
              Trailing-whitespace′ g (p₁ ⊛ p₃) →
              Trailing-whitespace′ g (p₁ ⊛ (p₂ ∣ p₃))
  ⊛-∣-lemma t₁₂ t₁₃ {s₂ = s₃}
    (⊛-sem {f = f} {x = x} {s₁ = s₁} {s₂ = s₂} f∈ (left-sem x∈))
    white
    with f x | (s₁ ++ s₂) ++ s₃ | t₁₂ (⊛-sem f∈ x∈) white
  ... | ._ | ._ | ⊛-sem f∈′ x∈′ = ⊛-sem f∈′ (left-sem x∈′)
  ⊛-∣-lemma t₁₂ t₁₃ {s₂ = s₃}
    (⊛-sem {f = f} {x = x} {s₁ = s₁} {s₂ = s₂} f∈ (right-sem x∈))
    white
    with f x | (s₁ ++ s₂) ++ s₃ | t₁₃ (⊛-sem f∈ x∈) white
  ... | ._ | ._ | ⊛-sem f∈′ x∈′ = ⊛-sem f∈′ (right-sem x∈′)

  ⊛-lemma : ∀ {A B} {p₁ : Prod NT (A → B)} {p₂ : Prod NT A} →
            Trailing-whitespace′ g p₂ →
            Trailing-whitespace′ g (p₁ ⊛ p₂)
  ⊛-lemma t₂ (⊛-sem {s₁ = s₁} f∈ x∈) white =
    cast (P.sym $ LM.assoc s₁ _ _)
         (⊛-sem f∈ (t₂ x∈ white))

  <⊛-return-lemma :
    ∀ {A B} {p : Prod NT A} {x : B} →
    Trailing-whitespace′ g p →
    Trailing-whitespace′ g (p <⊛ return x)
  <⊛-return-lemma t (<⊛-sem {s₁ = s₁} f∈ return-sem) white =
    cast (++-lemma s₁) (<⊛-sem (t f∈ white) return-sem)

  <⊛-⋆-lemma :
    ∀ {A B} {p₁ : Prod NT A} {p₂ : Prod NT B} →
    Is-whitespace p₂ →
    Trailing-whitespace′ g (p₁ <⊛ p₂ ⋆)
  <⊛-⋆-lemma is-whitespace (<⊛-sem {s₁ = s₁} x∈ white₁) white₂ =
    cast (P.sym $ LM.assoc s₁ _ _)
         (<⊛-sem x∈ (⋆-⋆-sem white₁ white₂))

  <⊛-lemma : ∀ {A B} {p₁ : Prod NT A} {p₂ : Prod NT B} →
             Trailing-whitespace′ g p₂ →
             Trailing-whitespace′ g (p₁ <⊛ p₂)
  <⊛-lemma t₂ (<⊛-sem {s₁ = s₁} f∈ x∈) white =
    cast (P.sym $ LM.assoc s₁ _ _)
         (<⊛-sem f∈ (t₂ x∈ white))

  fail->>=-lemma : ∀ {A B} {p : A → Prod NT B} →
                   Trailing-whitespace′ g (fail >>= p)
  fail->>=-lemma (>>=-sem () _)

  return->>=-lemma : ∀ {A B} {p : A → Prod NT B} {x} →
                     Trailing-whitespace′ g (p x) →
                     Trailing-whitespace′ g (return x >>= p)
  return->>=-lemma t (>>=-sem return-sem y∈) white =
    >>=-sem return-sem (t y∈ white)

  tok->>=-lemma : ∀ {A} {p : Char → Prod NT A} {t} →
                  Trailing-whitespace′ g (p t) →
                  Trailing-whitespace′ g (tok t >>= p)
  tok->>=-lemma t (>>=-sem tok-sem y∈) white =
    >>=-sem tok-sem (t y∈ white)

  ∣-lemma : ∀ {A} {p₁ p₂ : Prod NT A} →
            Trailing-whitespace′ g p₁ →
            Trailing-whitespace′ g p₂ →
            Trailing-whitespace′ g (p₁ ∣ p₂)
  ∣-lemma t₁ t₂ (left-sem  x∈) white = left-sem  (t₁ x∈ white)
  ∣-lemma t₁ t₂ (right-sem x∈) white = right-sem (t₂ x∈ white)

  trailing? : ∀ {A} (p : Prod NT A) →
              Maybe (Trailing-whitespace′ g p)
  trailing? fail             = just (λ ())
  trailing? (p ⊛ return x)   = ⊛-return-lemma <$>M trailing? p
  trailing? (p₁ ⊛ p₂ ⋆)      = ⊛-⋆-lemma <$>M trailing? p₁ ⊛M trailing? p₂
  trailing? (p₁ ⊛ (p₂ ∣ p₃)) = ⊛-∣-lemma <$>M trailing? (p₁ ⊛ p₂)
                                           ⊛M trailing? (p₁ ⊛ p₃)
  trailing? (p₁ ⊛ p₂)        = ⊛-lemma <$>M trailing? p₂
  trailing? (p <⊛ return x)  = <⊛-return-lemma <$>M trailing? p
  trailing? (p₁ <⊛ p₂ ⋆)     = <⊛-⋆-lemma <$>M is-whitespace? p₂
  trailing? (p₁ <⊛ p₂)       = <⊛-lemma <$>M trailing? p₂
  trailing? (fail >>= p)     = just fail->>=-lemma
  trailing? (return x >>= p) = return->>=-lemma <$>M trailing? (p x)
  trailing? (tok t >>= p)    = tok->>=-lemma <$>M trailing? (p t)
  trailing? (p₁ ∣ p₂)        = ∣-lemma <$>M trailing? p₁ ⊛M trailing? p₂
  trailing? _                = nothing

private

  -- A unit test.

  test : T (is-just (trailing-whitespace
                       0 empty-grammar (tt <$ whitespace ⋆)))
  test = _

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


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

module hott.truncation.const where

open import sum
open import equality
open import function.overloading
open import hott.truncation.core
open import hott.level

const-factorisation : ∀ {i j}{A : Set i}{B : Set j}
                    → h 2 B
                    → (f : A → B)
                    → ((x y : A) → f x ≡ f y)
                    → (Trunc 1 A → B)
const-factorisation {A = A}{B} hB f c = f'
  where
    E : Set _
    E = Σ B λ b → (a : A) → f a ≡ b

    p : E → B
    p (b , _) = b

    lem : (a₀ : A)(b : B)(u : (a : A) → f a ≡ b)
        → (_≡_ {A = E} (f a₀ , λ a → c a a₀) (b , u))
    lem a₀ b u = unapΣ (u a₀ , h1⇒prop (Π-level (λ a → hB (f a) b)) _ u)

    hE : A → contr E
    hE a₀ = (f a₀ , λ a → c a a₀) , λ { (b , u) → lem a₀ b u }

    u : Trunc 1 A → contr E
    u = Trunc-elim 1 _ _ (contr-h1 E) hE

    s : Trunc 1 A → E
    s a = proj₁ (u a)

    f' : Trunc 1 A → B
    f' a = p (s a)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --without-K  #-}
module algebra where

open import algebra.semigroup public
open import algebra.monoid public
open import algebra.group public


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.SequentialColimit where

open import Cubical.HITs.SequentialColimit.Base public
open import Cubical.HITs.SequentialColimit.Properties public