text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.KleinBottle where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to pRec2 ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; ∣_∣ to ∣_∣₁)
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; elim2 to trElim2)
open import Cubical.Data.Nat hiding (+-assoc)
open import Cubical.Algebra.Group renaming (Int to IntGroup ; Bool to BoolGroup ; Unit to UnitGroup)

open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Transport

open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn

open import Cubical.Data.Sigma

open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.Equiv
open import Cubical.Homotopy.Connected

open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Bool
open import Cubical.Data.Int renaming (+-comm to +-commℤ ; _+_ to _+ℤ_)

open import Cubical.HITs.KleinBottle
open import Cubical.Data.Empty
open import Cubical.Foundations.Path

open import Cubical.Homotopy.Loopspace

open IsGroupHom
open Iso

characFunSpace𝕂² : ∀ {ℓ} (A : Type ℓ) →
               Iso (KleinBottle → A)
                   (Σ[ x ∈ A ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙∙ q ∙∙ p ≡ q)
fun (characFunSpace𝕂² A) f =
  (f point) ,
  ((cong f line1) ,
   (cong f line2 ,
   fst (Square≃doubleComp
         (cong f line2) (cong f line2)
         (sym (cong f line1)) (cong f line1))
         (λ i j → f (square i j))))
inv (characFunSpace𝕂² A) (x , p , q , sq) point = x
inv (characFunSpace𝕂² A) (x , p , q , sq) (line1 i) = p i
inv (characFunSpace𝕂² A) (x , p , q , sq) (line2 i) = q i
inv (characFunSpace𝕂² A) (x , p , q , sq) (square i j) =
  invEq (Square≃doubleComp q q (sym p) p) sq i j
rightInv (characFunSpace𝕂² A) (x , (p , (q , sq))) =
  ΣPathP (refl , (ΣPathP (refl , (ΣPathP (refl , secEq (Square≃doubleComp q q (sym p) p) sq)))))
leftInv (characFunSpace𝕂² A) f _ point = f point
leftInv (characFunSpace𝕂² A) f _ (line1 i) = f (line1 i)
leftInv (characFunSpace𝕂² A) f _ (line2 i) = f (line2 i)
leftInv (characFunSpace𝕂² A) f z (square i j) =
  retEq (Square≃doubleComp
          (cong f line2) (cong f line2)
          (sym (cong f line1)) (cong f line1))
          (λ i j → f (square i j)) z i j
private
  movePathLem : ∀ {ℓ} {A : Type ℓ} {x : A} (p q : x ≡ x) → isComm∙ (A , x)
             → (p ∙∙ q ∙∙ p ≡ q) ≡ ((p ∙ p) ∙ q ≡ q)
  movePathLem p q comm =
    cong (_≡ q) (doubleCompPath-elim' p q p ∙∙ cong (p ∙_) (comm q p) ∙∙ assoc _ _ _)

  movePathLem2 : ∀ {ℓ} {A : Type ℓ} {x : A} (p q : x ≡ x)
             → (((p ∙ p) ∙ q) ∙ sym q ≡ q ∙ sym q) ≡ (p ∙ p ≡ refl)
  movePathLem2 p q =
    cong₂ _≡_ (sym (assoc (p ∙ p) q (sym q)) ∙∙ cong ((p ∙ p) ∙_) (rCancel q) ∙∙ sym (rUnit (p ∙ p)))
              (rCancel q)

  movePathIso : ∀ {ℓ} {A : Type ℓ} {x : A} (p q : x ≡ x) → isComm∙ (A , x)
                → Iso (p ∙∙ q ∙∙ p ≡ q) (p ∙ p ≡ refl)
  movePathIso {x = x} p q comm =
    compIso (pathToIso (movePathLem p q comm))
      (compIso (helper (p ∙ p))
               (pathToIso (movePathLem2 p q)))
    where
    helper : (p : x ≡ x) → Iso (p ∙ q ≡ q) ((p ∙ q) ∙ sym q ≡ q ∙ sym q)
    helper p = congIso (equivToIso (_ , compPathr-isEquiv (sym q)))

------ H¹(𝕂²) ≅ 0 --------------
H⁰-𝕂² : GroupIso (coHomGr 0 KleinBottle) IntGroup
fun (fst H⁰-𝕂²) = sRec isSetInt λ f → f point
inv (fst H⁰-𝕂²) x = ∣ (λ _ → x) ∣₂
rightInv (fst H⁰-𝕂²) _ = refl
leftInv (fst H⁰-𝕂²) =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ f → cong ∣_∣₂ (funExt (λ {point → refl
                                 ; (line1 i) j → isSetInt (f point) (f point) refl (cong f line1) j i
                                 ; (line2 i) j → isSetInt (f point) (f point) refl (cong f line2) j i
                                 ; (square i j) z → helper f i j z}))
  where
  helper : (f : KleinBottle → Int)
        → Cube (λ j z → isSetInt (f point) (f point) refl (cong  f line2) z j)
                (λ j z → isSetInt (f point) (f point) refl (cong  f line2) z j)
                (λ i z → isSetInt (f point) (f point) refl (cong  f line1) z (~ i))
                (λ i z → isSetInt (f point) (f point) refl (cong  f line1) z i)
                refl
                λ i j → f (square i j)
  helper f = isGroupoid→isGroupoid' (isOfHLevelSuc 2 isSetInt) _ _ _ _ _ _
snd H⁰-𝕂² =
  makeIsGroupHom (sElim2 (λ _ _ → isOfHLevelPath 2 isSetInt _ _) λ _ _ → refl)

------ H¹(𝕂¹) ≅ ℤ ------------
{-
Step one :
H¹(𝕂²) := ∥ 𝕂² → K₁ ∥₂
        ≡ ∥ Σ[ x ∈ K₁ ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] (p ∙∙ q ∙∙ p ≡ q) ∥₂    (characFunSpace𝕂²)
        ≡ ∥ Σ[ x ∈ K₁ ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙ p ≡ refl ∥₂         (movePathIso, using commutativity of ΩK₂)
        ≡ ∥ Σ[ x ∈ K₁ ] (x ≡ x) ∥₂                                             (p ∙ p ≡ refl forces p ≡ refl. Also, p ∙ p ≡ refl is an hProp)
-}

nilpotent→≡0 : (x : Int) → x +ℤ x ≡ 0 → x ≡ 0
nilpotent→≡0 (pos zero) p = refl
nilpotent→≡0 (pos (suc n)) p =
  ⊥-rec (negsucNotpos _ _
        (sym (cong (_- 1) (cong sucInt (sym (helper2 n)) ∙ p))))
  where
  helper2 : (n : ℕ) → pos (suc n) +pos n ≡ pos (suc (n + n))
  helper2 zero = refl
  helper2 (suc n) = cong sucInt (sym (sucInt+pos n (pos (suc n))))
                 ∙∙ cong (sucInt ∘ sucInt) (helper2 n)
                 ∙∙ cong (pos ∘ suc ∘ suc) (sym (+-suc n n))
nilpotent→≡0 (negsuc n) p = ⊥-rec (negsucNotpos _ _ (helper2 n p))
  where
  helper2 : (n : ℕ) → (negsuc n +negsuc n) ≡ pos 0 → negsuc n ≡ pos (suc n)
  helper2 n p = cong (negsuc n +ℤ_) (sym (helper3 n))
              ∙ +-assoc (negsuc n) (negsuc n) (pos (suc n))
              ∙∙ cong (_+ℤ (pos (suc n))) p
              ∙∙ cong sucInt (+-commℤ (pos 0) (pos n))
    where
    helper3 : (n : ℕ) → negsuc n +pos (suc n) ≡ 0
    helper3 zero = refl
    helper3 (suc n) = cong sucInt (sucInt+pos n (negsuc (suc n))) ∙ helper3 n

nilpotent→≡refl : (x : coHomK 1) (p : x ≡ x) → p ∙ p ≡ refl → p ≡ refl
nilpotent→≡refl =
  trElim (λ _ → isGroupoidΠ2 λ _ _ → isOfHLevelPlus {n = 1} 2 (isOfHLevelTrunc 3 _ _ _ _))
         (toPropElim (λ _ → isPropΠ2 λ _ _ → isOfHLevelTrunc 3 _ _ _ _)
          λ p pId → sym (rightInv (Iso-Kn-ΩKn+1 0) p)
                  ∙∙ cong (Kn→ΩKn+1 0) (nilpotent→≡0 (ΩKn+1→Kn 0 p)
                                                       (sym (ΩKn+1→Kn-hom 0 p p)
                                                        ∙ cong (ΩKn+1→Kn 0) pId))
                  ∙∙ Kn→ΩKn+10ₖ 0)

Iso-H¹-𝕂²₁ : Iso (Σ[ x ∈ coHomK 1 ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙ p ≡ refl)
                  (Σ[ x ∈ coHomK 1 ] x ≡ x)
fun Iso-H¹-𝕂²₁ (x , (_ , (q , _))) = x , q
inv Iso-H¹-𝕂²₁ (x , q) = x , (refl , (q , (sym (rUnit refl))))
rightInv Iso-H¹-𝕂²₁ _ = refl
leftInv Iso-H¹-𝕂²₁ (x , (p , (q , P))) =
  ΣPathP (refl ,
   (ΣPathP (sym (nilpotent→≡refl x p P)
     , toPathP (Σ≡Prop (λ _ → isOfHLevelTrunc 3 _ _ _ _)
               (transportRefl q)))))

{- But this is precisely the type (minus set-truncation) of H¹(S¹) -}
Iso-H¹-𝕂²₂ : Iso (Σ[ x ∈ coHomK 1 ] x ≡ x) (S¹ → coHomK 1)
Iso-H¹-𝕂²₂ = invIso IsoFunSpaceS¹

H¹-𝕂²≅ℤ : GroupIso (coHomGr 1 KleinBottle) IntGroup
H¹-𝕂²≅ℤ = compGroupIso theGroupIso (Hⁿ-Sⁿ≅ℤ 0)
  where
  theIso : Iso (coHom 1 KleinBottle) (coHom 1 S¹)
  theIso =
    setTruncIso (
    compIso (characFunSpace𝕂² (coHomK 1))
      (compIso
         (Σ-cong-iso-snd (λ x → Σ-cong-iso-snd
                            λ p → Σ-cong-iso-snd
                              λ q → movePathIso p q (isCommΩK-based 1 x)))
         (compIso Iso-H¹-𝕂²₁
                  Iso-H¹-𝕂²₂)))

  is-hom : IsGroupHom (coHomGr 1 KleinBottle .snd) (fun theIso) (coHomGr 1 S¹ .snd)
  is-hom =
    makeIsGroupHom
      (sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ f g → cong ∣_∣₂ (funExt λ {base → refl ; (loop i) → refl}))

  theGroupIso : GroupIso (coHomGr 1 KleinBottle) (coHomGr 1 S¹)
  theGroupIso = (theIso , is-hom)

------ H²(𝕂²) ≅ ℤ/2ℤ (represented here by BoolGroup) -------
-- It suffices to show that H²(Klein) is equivalent to Bool as types

{-
Step one :
H²(𝕂²) := ∥ 𝕂² → K₂ ∥₂
        ≡ ∥ Σ[ x ∈ K₂ ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] (p ∙∙ q ∙∙ p ≡ q) ∥₂    (characFunSpace𝕂²)
        ≡ ∥ Σ[ x ∈ K₂ ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙ p ≡ refl ∥₂         (movePathIso, using commutativity of ΩK₂)
        ≡ ∥ Σ[ p ∈ x ≡ x ] p ∙ p ≡ refl ∥₂                                    (connectedness of K₂)
-}

Iso-H²-𝕂²₁ : Iso ∥ Σ[ x ∈ coHomK 2 ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙ p ≡ refl ∥₂
                  ∥ Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ∙ p ≡ refl ∥₂
fun Iso-H²-𝕂²₁ =
  sRec setTruncIsSet
    (uncurry (trElim (λ _ → is2GroupoidΠ λ _ → isOfHLevelPlus {n = 2} 2 setTruncIsSet)
                     (sphereElim _ (λ _ → isSetΠ λ _ → setTruncIsSet)
                                 λ y → ∣ fst y , snd (snd y) ∣₂)))
inv Iso-H²-𝕂²₁ =
  sMap λ p → (0ₖ 2) , ((fst p) , (refl , (snd p)))
rightInv Iso-H²-𝕂²₁ =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ p → refl
leftInv Iso-H²-𝕂²₁ =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        (uncurry (trElim (λ _ → is2GroupoidΠ λ _ → isOfHLevelPlus {n = 1} 3 (setTruncIsSet _ _))
                 (sphereToPropElim _
                   (λ _ → isPropΠ λ _ → setTruncIsSet _ _)
                   λ {(p , (q , sq))
                     → trRec (setTruncIsSet _ _)
                              (λ qid → cong ∣_∣₂ (ΣPathP (refl , (ΣPathP (refl , (ΣPathP (sym qid  , refl)))))))
                              (fun (PathIdTruncIso _)
                                       (isContr→isProp (isConnectedPathKn 1 (0ₖ 2) (0ₖ 2)) ∣ q ∣ ∣ refl ∣))})))

{- Step two :  ∥ Σ[ p ∈ x ≡ x ] p ∙ p ≡ refl ∥₂ ≡ ∥ Σ[ x ∈ K₁ ] x + x ≡ 0 ∥₂ -}
Iso-H²-𝕂²₂ : Iso ∥ (Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ∙ p ≡ refl) ∥₂ ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
Iso-H²-𝕂²₂ = setTruncIso (Σ-cong-iso {B' = λ x → x +ₖ x ≡ 0ₖ 1} (invIso (Iso-Kn-ΩKn+1 1))
                                    λ p → compIso (congIso (invIso (Iso-Kn-ΩKn+1 1)))
                                                   (pathToIso λ i → ΩKn+1→Kn-hom 1 p p i ≡ 0ₖ 1))

{- Step three :
∥ Σ[ x ∈ K₁ ] x + x ≡ 0 ∥₂ ≡ Bool
We begin by defining the a map Σ[ x ∈ K₁ ] x + x ≡ 0 → Bool. For a point
(0 , p) we map it to true if winding(p) is even and false if winding(p) is odd.
We also have to show that this map respects the loop
-}

ΣKₙNilpot→Bool :  Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 → Bool
ΣKₙNilpot→Bool = uncurry (trElim (λ _ → isGroupoidΠ λ _ → isOfHLevelSuc 2 isSetBool)
                        λ {base p → isEven (ΩKn+1→Kn 0 p)
                        ; (loop i) p → hcomp (λ k → λ { (i = i0) → respectsLoop p k
                                                        ; (i = i1) → isEven (ΩKn+1→Kn 0 p)})
                        (isEven (ΩKn+1→Kn 0 (transp (λ j → ∣ (loop ∙ loop) (i ∨ j) ∣ ≡ 0ₖ 1) i
                                                      p)))})
  where
  isEven-2 : (x : Int) → isEven (-2 +ℤ x) ≡ isEven x
  isEven-2 (pos zero) = refl
  isEven-2 (pos (suc zero)) = refl
  isEven-2 (pos (suc (suc n))) =
      cong isEven (cong sucInt (sucInt+pos _ _)
              ∙∙ sucInt+pos _ _
              ∙∙ +-commℤ 0 (pos n))
    ∙ lossy n
    where
    lossy : (n : ℕ) → isEven (pos n) ≡ isEven (pos n)
    lossy n = refl
  isEven-2 (negsuc zero) = refl
  isEven-2 (negsuc (suc n)) =
      cong isEven (predInt+negsuc n _
               ∙ +-commℤ -3 (negsuc n))
    ∙ lossy2 n
      where
      lossy2 : (n : ℕ) → isEven (negsuc (suc (suc (suc n)))) ≡ isEven (pos n)
      lossy2 n = refl
  respectsLoop : (p : 0ₖ 1 ≡ 0ₖ 1)
              → isEven (ΩKn+1→Kn 0 (transport (λ i → ∣ (loop ∙ loop) i ∣ ≡ 0ₖ 1) p))
               ≡ isEven (ΩKn+1→Kn 0 p)
  respectsLoop p =
       cong isEven (cong (ΩKn+1→Kn 0) (cong (transport (λ i → ∣ (loop ∙ loop) i ∣ ≡ 0ₖ 1))
                                             (lUnit p)))
    ∙∙ cong isEven (cong (ΩKn+1→Kn 0)
                             λ j → transp (λ i → ∣ (loop ∙ loop) (i ∨ j) ∣ ≡ 0ₖ 1) j
                                           ((λ i → ∣ (loop ∙ loop) (~ i ∧ j) ∣) ∙ p))
    ∙∙ cong isEven (ΩKn+1→Kn-hom 0 (sym (cong ∣_∣ (loop ∙ loop))) p)
     ∙ isEven-2 (ΩKn+1→Kn 0 p)

{-
We show that for any x : Int we have ∣ (0ₖ 1 , Kn→ΩKn+1 0 x) ∣₂ ≡ ∣ (0ₖ 1 , refl) ∣₂ when x is even
and ∣ (0ₖ 1 , Kn→ΩKn+1 0 x) ∣₂ ≡ ∣ (0ₖ 1 , cong ∣_∣ loop) ∣₂ when x is odd

This is done by induction on x. For the inductive step we define a multiplication _*_ on ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
which is just ∣ (0 , p) ∣₂ * ∣ (0 , q) ∣₂ ≡ ∣ (0 , p ∙ q) ∣₂ when x is 0
-}

private
  _*_ : ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
  _*_ = sRec (isSetΠ (λ _ → setTruncIsSet)) λ a → sRec setTruncIsSet λ b → *' (fst a) (fst b) (snd a) (snd b)
    where
    *' : (x y : coHomK 1) (p : x +ₖ x ≡ 0ₖ 1) (q : y +ₖ y ≡ 0ₖ 1) → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
    *' =
      trElim2 (λ _ _ → isGroupoidΠ2 λ _ _ → isOfHLevelSuc 2 setTruncIsSet)
              (wedgeconFun _ _
                (λ _ _ → isSetΠ2 λ _ _ → setTruncIsSet)
                (λ x p q → ∣ ∣ x ∣ , cong₂ _+ₖ_ p q ∣₂)
                (λ y p q → ∣ ∣ y ∣ , sym (rUnitₖ 1 (∣ y ∣ +ₖ ∣ y ∣)) ∙ cong₂ _+ₖ_ p q ∣₂)
                (funExt λ p → funExt λ q → cong ∣_∣₂ (ΣPathP (refl , (sym (lUnit _))))))

  *=∙ : (p q : 0ₖ 1 ≡ 0ₖ 1) → ∣ 0ₖ 1 , p ∣₂ * ∣ 0ₖ 1 , q ∣₂ ≡ ∣ 0ₖ 1 , p ∙ q ∣₂
  *=∙ p q = cong ∣_∣₂ (ΣPathP (refl , sym (∙≡+₁ p q)))

isEvenNegsuc : (n : ℕ) → isEven (pos (suc n)) ≡ true → isEven (negsuc n) ≡ true
isEvenNegsuc zero p = ⊥-rec (true≢false (sym p))
isEvenNegsuc (suc n) p = p

¬isEvenNegSuc : (n : ℕ) → isEven (pos (suc n)) ≡ false → isEven (negsuc n) ≡ false
¬isEvenNegSuc zero p = refl
¬isEvenNegSuc (suc n) p = p

evenCharac : (x : Int) → isEven x ≡ true
    → Path ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
            ∣ (0ₖ 1 , Kn→ΩKn+1 0 x) ∣₂
            ∣ (0ₖ 1 , refl) ∣₂
evenCharac (pos zero) isisEven i = ∣ (0ₖ 1) , (rUnit refl (~ i)) ∣₂
evenCharac (pos (suc zero)) isisEven = ⊥-rec (true≢false (sym isisEven))
evenCharac (pos (suc (suc zero))) isisEven =
    cong ∣_∣₂ ((λ i → 0ₖ 1 , rUnit (cong ∣_∣ ((lUnit loop (~ i)) ∙ loop)) (~ i))
  ∙ (ΣPathP (cong ∣_∣ loop , λ i j → ∣ (loop ∙ loop) (i ∨ j) ∣)))
evenCharac (pos (suc (suc (suc n)))) isisEven =
     (λ i → ∣ 0ₖ 1 , Kn→ΩKn+1-hom 0 (pos (suc n)) 2 i ∣₂)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (pos (suc n))) (Kn→ΩKn+1 0 (pos 2)))
  ∙∙ (cong₂ _*_ (evenCharac (pos (suc n)) isisEven) (evenCharac 2 refl))

evenCharac (negsuc zero) isisEven = ⊥-rec (true≢false (sym isisEven))
evenCharac (negsuc (suc zero)) isisEven =
  cong ∣_∣₂ ((λ i → 0ₖ 1
                  , λ i₁ → hfill (doubleComp-faces (λ i₂ → ∣ base ∣) (λ _ → ∣ base ∣) i₁)
                                  (inS ∣ compPath≡compPath' (sym loop) (sym loop) i i₁ ∣) (~ i))
          ∙ ΣPathP ((cong ∣_∣ (sym loop)) , λ i j → ∣ (sym loop ∙' sym loop) (i ∨ j) ∣))
evenCharac (negsuc (suc (suc n))) isisEven =
     cong ∣_∣₂ (λ i → 0ₖ 1 , Kn→ΩKn+1-hom 0 (negsuc n) -2 i)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (negsuc n)) (Kn→ΩKn+1 0 -2))
  ∙∙ cong₂ _*_ (evenCharac (negsuc n) (isEvenNegsuc n isisEven)) (evenCharac -2 refl)

oddCharac : (x : Int) → isEven x ≡ false
    → Path ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
            ∣ (0ₖ 1 , Kn→ΩKn+1 0 x) ∣₂
            ∣ (0ₖ 1 , cong ∣_∣ loop) ∣₂
oddCharac (pos zero) isOdd = ⊥-rec (true≢false isOdd)
oddCharac (pos (suc zero)) isOdd i =
  ∣ (0ₖ 1 , λ j → hfill (doubleComp-faces (λ i₂ → ∣ base ∣) (λ _ → ∣ base ∣) j)
                         (inS ∣ lUnit loop (~ i) j ∣) (~ i)) ∣₂
oddCharac (pos (suc (suc n))) isOdd =
  (λ i → ∣ 0ₖ 1 , Kn→ΩKn+1-hom 0 (pos n) 2 i ∣₂)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (pos n)) (Kn→ΩKn+1 0 2))
  ∙∙ cong₂ _*_ (oddCharac (pos n) isOdd) (evenCharac 2 refl)
oddCharac (negsuc zero) isOdd =
    cong ∣_∣₂ ((λ i → 0ₖ 1 , rUnit (sym (cong ∣_∣ loop)) (~ i))
  ∙ ΣPathP (cong ∣_∣ (sym loop) , λ i j → ∣ hcomp (λ k → λ { (i = i0) → loop (~ j ∧ k)
                                                           ; (i = i1) → loop j
                                                           ; (j = i1) → base})
                                                 (loop (j ∨ ~ i)) ∣))
oddCharac (negsuc (suc zero)) isOdd = ⊥-rec (true≢false isOdd)
oddCharac (negsuc (suc (suc n))) isOdd =
     cong ∣_∣₂ (λ i → 0ₖ 1 , Kn→ΩKn+1-hom 0 (negsuc n) -2 i)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (negsuc n)) (Kn→ΩKn+1 0 -2))
  ∙∙ cong₂ _*_ (oddCharac (negsuc n) (¬isEvenNegSuc n isOdd)) (evenCharac (negsuc 1) refl)

{- We now have all we need to establish the Iso -}
Bool→ΣKₙNilpot : Bool → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
Bool→ΣKₙNilpot false = ∣ 0ₖ 1 , cong ∣_∣ loop ∣₂
Bool→ΣKₙNilpot true = ∣ 0ₖ 1 , refl ∣₂

testIso : Iso ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ Bool
fun testIso = sRec isSetBool ΣKₙNilpot→Bool
inv testIso = Bool→ΣKₙNilpot
rightInv testIso false = refl
rightInv testIso true = refl
leftInv testIso =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        (uncurry (trElim
          (λ _ → isGroupoidΠ λ _ → isOfHLevelPlus {n = 1} 2 (setTruncIsSet _ _))
          (toPropElim (λ _ → isPropΠ (λ _ → setTruncIsSet _ _))
          (λ p → path p (isEven (ΩKn+1→Kn 0 p)) refl))))
  where
  path : (p : 0ₖ 1 ≡ 0ₖ 1) (b : Bool) → (isEven (ΩKn+1→Kn 0 p) ≡ b)
       → Bool→ΣKₙNilpot (ΣKₙNilpot→Bool (∣ base ∣ , p)) ≡ ∣ ∣ base ∣ , p ∣₂
  path p false q =
       (cong Bool→ΣKₙNilpot q)
    ∙∙ sym (oddCharac (ΩKn+1→Kn 0 p) q)
    ∙∙ cong ∣_∣₂ λ i → 0ₖ 1 , rightInv (Iso-Kn-ΩKn+1 0) p i
  path p true q =
       cong Bool→ΣKₙNilpot q
    ∙∙ sym (evenCharac (ΩKn+1→Kn 0 p) q)
    ∙∙ cong ∣_∣₂ λ i → 0ₖ 1 , rightInv (Iso-Kn-ΩKn+1 0) p i

H²-𝕂²≅Bool : GroupIso (coHomGr 2 KleinBottle) BoolGroup
H²-𝕂²≅Bool = invGroupIso (≅Bool theIso)
  where
  theIso : Iso _ _
  theIso =
    compIso (setTruncIso
               (compIso (characFunSpace𝕂² (coHomK 2))
                          (Σ-cong-iso-snd
                            λ x → Σ-cong-iso-snd
                              λ p → Σ-cong-iso-snd
                                λ q → (movePathIso p q (isCommΩK-based 2 x)))))
      (compIso Iso-H²-𝕂²₁
        (compIso
          Iso-H²-𝕂²₂
          testIso))

------ Hⁿ(𝕂²) ≅ 0 , n ≥ 3 ------
isContrHⁿ-𝕂² : (n : ℕ) → isContr (coHom (3 + n) KleinBottle)
isContrHⁿ-𝕂² n =
  isOfHLevelRetractFromIso 0
    (setTruncIso (characFunSpace𝕂² (coHomK _)))
    isContrΣ-help
  where
  helper : (x : coHomK (3 + n))(p : x ≡ x) → (refl ≡ p) → (q : x ≡ x) → (refl ≡ q)
      → (P : p ∙∙ q ∙∙ p ≡ q)
      → Path ∥ (Σ[ x ∈ coHomK (3 + n) ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙∙ q ∙∙ p ≡ q) ∥₂
              ∣ x , p , q , P ∣₂
              ∣ 0ₖ _ , refl , refl , sym (rUnit refl) ∣₂
  helper =
    trElim (λ _ → isProp→isOfHLevelSuc (4 + n) (isPropΠ4 λ _ _ _ _ → isPropΠ λ _ → setTruncIsSet _ _))
      (sphereToPropElim _ (λ _ → isPropΠ4 λ _ _ _ _ → isPropΠ λ _ → setTruncIsSet _ _)
        λ p → J (λ p _ → (q : 0ₖ _ ≡ 0ₖ _) → (refl ≡ q)
                        → (P : p ∙∙ q ∙∙ p ≡ q)
                        → Path ∥ (Σ[ x ∈ coHomK (3 + n) ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙∙ q ∙∙ p ≡ q) ∥₂
                                ∣ 0ₖ _ , p , q , P ∣₂
                                ∣ 0ₖ _ , refl , refl , sym (rUnit refl) ∣₂)
                λ q → J (λ q _ → (P : refl ∙∙ q ∙∙ refl ≡ q)
                                → Path ∥ (Σ[ x ∈ coHomK (3 + n) ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙∙ q ∙∙ p ≡ q) ∥₂
                                        ∣ 0ₖ _ , refl , q , P ∣₂
                                        ∣ 0ₖ _ , refl , refl , sym (rUnit refl) ∣₂)
                         λ P → trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                                      (λ P≡rUnitrefl i → ∣ 0ₖ (3 + n) , refl , refl , P≡rUnitrefl i ∣₂)
                                      (fun (PathIdTruncIso _)
                                                 (isContr→isProp (isConnectedPath _ (isConnectedPathKn (2 + n) _ _)
                                                                     (refl ∙∙ refl ∙∙ refl) refl)
                                                                     ∣ P ∣ ∣ sym (rUnit refl) ∣)))

  isContrΣ-help : isContr ∥ (Σ[ x ∈ coHomK (3 + n) ] Σ[ p ∈ x ≡ x ] Σ[ q ∈ x ≡ x ] p ∙∙ q ∙∙ p ≡ q) ∥₂
  fst isContrΣ-help = ∣ 0ₖ _ , refl , refl , sym (rUnit refl) ∣₂
  snd isContrΣ-help =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
      λ {(x , p , q , P)
        → trRec (isProp→isOfHLevelSuc (suc n) (setTruncIsSet _ _))
            (λ pId → trRec (isProp→isOfHLevelSuc (suc n) (setTruncIsSet _ _))
                      (λ qId → sym (helper x p pId q qId P))
                      (fun (PathIdTruncIso (2 + n))
                                 (isContr→isProp (isConnectedPathKn (2 + n) _ _) ∣ refl ∣ ∣ q ∣)))
                 (fun (PathIdTruncIso (2 + n))
                            (isContr→isProp (isConnectedPathKn (2 + n) _ _) ∣ refl ∣ ∣ p ∣))}

Hⁿ⁺³-𝕂²≅0 : (n : ℕ) → GroupIso (coHomGr (3 + n) KleinBottle) UnitGroup
Hⁿ⁺³-𝕂²≅0 n = contrGroupIsoUnit (isContrHⁿ-𝕂² n)

max_stars_repo_name: LuuBluum/cubical

max_issues_repo_name: LuuBluum/cubical

max_forks_repo_name: LuuBluum/cubical


text:
{-# OPTIONS --cubical #-}
module Cubical.Codata.Everything where

open import Cubical.Codata.EverythingSafe public

--- Modules making assumptions that might be incompatible with other
--  flags or make use of potentially unsafe features.

-- Assumes --guardedness
open import Cubical.Codata.Stream public

open import Cubical.Codata.Conat public

open import Cubical.Codata.M public

-- Also uses {-# TERMINATING #-}.
open import Cubical.Codata.M.Bisimilarity public

ext: agda

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.Poset where

open import Cubical.Foundations.Prelude

open import Cubical.Relation.Binary.Poset

open import Cubical.Categories.Category

open Category

private
  variable
    ℓ ℓ' : Level

module _ (P : Poset ℓ ℓ') where

  open PosetStr (snd P)

  PosetCategory : Category ℓ ℓ'
  ob PosetCategory           = fst P
  Hom[_,_] PosetCategory     = _≤_
  id PosetCategory           = is-refl _
  _⋆_ PosetCategory          = is-trans _ _ _
  ⋆IdL PosetCategory _       = is-prop-valued _ _ _ _
  ⋆IdR PosetCategory _       = is-prop-valued _ _ _ _
  ⋆Assoc PosetCategory _ _ _ = is-prop-valued _ _ _ _
  isSetHom PosetCategory     = isProp→isSet (is-prop-valued _ _)

max_stars_repo_name: FernandoLarrain/cubical


text:
open import FRP.JS.Bool using ( Bool ; true ; false )

module FRP.JS.Maybe where

-- Data.Maybe doesn't have bindings for JavaScript, so we define Maybe here.

-- We'd like to use JavaScript's built-in null as the
-- representation of nothing, and use x as the representation of just
-- x.  Unfortunately this doens't work for nested Maybes, as it
-- identifies nothing and just nothing at type Maybe Maybe A, which in
-- turn breaks parametericity. Instead, we link to a JS library which
-- provides functions box and unbox such that box(x) !== null,
-- unbox(box(x)) === x, and if x !== box^n (null) then x ==
-- box(x). Note that for never-null types (e.g. String), values
-- of type Maybe T are either null or values of type T, which
-- corresponds to the JavaScript idiom (for example, a lookup in an
-- array of strings can be translated to native array lookup).

data Maybe {α} (A : Set α) : Set α where
  just : (a : A) → Maybe A
  nothing : Maybe A

{-# COMPILED_JS Maybe function(x,v) {
  if (x === null) { return v.nothing(); }
  else { return v.just(require("agda.box").unbox(x)); }
} #-}
{-# COMPILED_JS just require("agda.box").box #-}
{-# COMPILED_JS nothing null #-}

_≟[_]_ : ∀ {α β A B} → Maybe {α} A → (A → B → Bool) → Maybe {β} B → Bool
just a  ≟[ p ] just b  = p a b
just a  ≟[ p ] nothing = false
nothing ≟[ p ] just b  = false
nothing ≟[ p ] nothing = true

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Homomorphism.Base (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Homomorphism.Definitions Σ

open import Fragment.Setoid.Morphism as Morphism
  hiding (id; ∣_∣; ∣_∣-cong)

open import Level using (Level; _⊔_)
open import Function using (_∘_; _$_)

open import Data.Vec using (map)
open import Data.Vec.Properties using (map-id; map-∘)
import Data.Vec.Relation.Binary.Equality.Setoid as VecSetoid

open import Relation.Binary using (IsEquivalence)
import Relation.Binary.Reasoning.Setoid as Reasoning

private
  variable
    a b c ℓ₁ ℓ₂ ℓ₃ : Level

module _
  (A : Algebra {a} {ℓ₁})
  (B : Algebra {b} {ℓ₂})
  where

  infixr 1 _⟿_

  record _⟿_ : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      ∣_∣⃗    : ∥ A ∥/≈ ↝ ∥ B ∥/≈
      ∣_∣-hom : Homomorphic A B (Morphism.∣_∣ ∣_∣⃗)

    ∣_∣ : ∥ A ∥ → ∥ B ∥
    ∣_∣ = Morphism.∣_∣ ∣_∣⃗

    ∣_∣-cong : Congruent ≈[ A ] ≈[ B ] ∣_∣
    ∣_∣-cong = Morphism.∣_∣-cong ∣_∣⃗

open _⟿_ public

module _ {A : Algebra {a} {ℓ₁}} where

  private

    ∣id∣-hom : Homomorphic A A (λ x → x)
    ∣id∣-hom {n} f xs = A ⟦ f ⟧-cong $ reflexive (map-id xs)
      where open VecSetoid ∥ A ∥/≈
            open IsEquivalence (≋-isEquivalence n) using (reflexive)

  id : A ⟿ A
  id = record { ∣_∣⃗    = Morphism.id
              ; ∣_∣-hom = ∣id∣-hom
              }

module _
  {A : Algebra {a} {ℓ₁}}
  {B : Algebra {b} {ℓ₂}}
  {C : Algebra {c} {ℓ₃}}
  (g : B ⟿ C)
  (f : A ⟿ B)
  where

  private

    ⊙-hom : Homomorphic A C (∣ g ∣ ∘ ∣ f ∣)
    ⊙-hom {n} op xs = begin
        C ⟦ op ⟧ (map (∣ g ∣ ∘ ∣ f ∣) xs)
      ≈⟨ C ⟦ op ⟧-cong $ reflexive (map-∘ ∣ g ∣ ∣ f ∣ xs) ⟩
        C ⟦ op ⟧ (map ∣ g ∣ (map ∣ f ∣ xs))
      ≈⟨ ∣ g ∣-hom op (map ∣ f ∣ xs) ⟩
        ∣ g ∣ (B ⟦ op ⟧ (map ∣ f ∣ xs))
      ≈⟨ ∣ g ∣-cong (∣ f ∣-hom op xs) ⟩
        ∣ g ∣ (∣ f ∣ (A ⟦ op ⟧ xs))
      ∎
      where open Reasoning ∥ C ∥/≈
            open VecSetoid ∥ C ∥/≈
            open IsEquivalence (≋-isEquivalence n) using (reflexive)

  infixr 9 _⊙_

  _⊙_ : A ⟿ C
  _⊙_ = record { ∣_∣⃗    = ∣ g ∣⃗ · ∣ f ∣⃗
               ; ∣_∣-hom = ⊙-hom
               }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module CategoryTheory.CartesianStrength where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.BCCCs.Cartesian
open import CategoryTheory.Monad
open import CategoryTheory.Comonad

-- Type class for Cartesian functors
record CartesianFunctor {n}
        {ℂ : Category n} {𝔻 : Category n} (Fn : Functor ℂ 𝔻)
        (ℂ-cart : Cartesian ℂ) (𝔻-cart : Cartesian 𝔻) : Set (lsuc n) where
    private module ℂ = Category ℂ
    private module 𝔻 = Category 𝔻
    open Category 𝔻
    open Functor Fn renaming (omap to F)
    open Cartesian ℂ-cart renaming
        ( ⊤ to ⊤ᶜ ; _⊗_ to _⊗ᶜ_ ; _*_ to _*ᶜ_ ; assoc-right to αᶜ
        ; unit-left to λᶜ ; unit-right to ρᶜ)
    open Cartesian 𝔻-cart renaming
        ( ⊤ to ⊤ᵈ ; _⊗_ to _⊗ᵈ_ ; _*_ to _*ᵈ_; assoc-right to αᵈ
        ; unit-left to λᵈ ; unit-right to ρᵈ)

    field
        -- | Data
        -- F preserves terminal objects (0-ary products)
        u : ⊤ᵈ ~> F ⊤ᶜ
        -- F preserves binary products
        m : ∀(A B : ℂ.obj) -> F A ⊗ᵈ F B ~> F (A ⊗ᶜ B)

        -- | Laws
        -- Naturality conditions
        m-nat₁ : ∀{A B C : ℂ.obj} (f : A ℂ.~> B)
              -> fmap (f *ᶜ ℂ.id) ∘ m A C ≈ m B C ∘ fmap f *ᵈ id
        m-nat₂ : ∀{A B C : ℂ.obj} (f : A ℂ.~> B)
              -> fmap (ℂ.id *ᶜ f) ∘ m C A ≈ m C B ∘ id *ᵈ fmap f

        -- Monoid laws
        associative : ∀{A B C : ℂ.obj} ->
              m A (B ⊗ᶜ C) ∘ (id *ᵈ m B C) ∘ αᵈ
            ≈ fmap αᶜ ∘ m (A ⊗ᶜ B) C ∘ (m A B *ᵈ id)
        unital-right : ∀{A : ℂ.obj} ->
            fmap ρᶜ ∘ m A ⊤ᶜ ∘ (id *ᵈ u) ≈ ρᵈ
        unital-left : ∀{B : ℂ.obj} ->
            fmap λᶜ ∘ m ⊤ᶜ B ∘ (u *ᵈ id) ≈ λᵈ

    -- Canonical distribution morphism
    m⁻¹ : ∀(A B : ℂ.obj) -> F (A ⊗ᶜ B) ~> F A ⊗ᵈ F B
    m⁻¹ A B = Cartesian.⟨_,_⟩ 𝔻-cart (fmap (Cartesian.π₁ ℂ-cart))
                                     (fmap (Cartesian.π₂ ℂ-cart))

-- Type class for Cartesian comonads
record CartesianComonad {n}
        {ℂ : Category n} (C : Comonad ℂ)
        (ℂ-cart : Cartesian ℂ) : Set (lsuc n) where
    open Category ℂ
    open Comonad C
    open Functor W renaming (omap to F)
    open Cartesian ℂ-cart

    field
        -- Cartesian comonads are Cartesian functors
        cart-fun : CartesianFunctor W ℂ-cart ℂ-cart
    open CartesianFunctor cart-fun
    field
        -- | Laws
        u-ε : u ∘ ε.at ⊤ ≈ id
        u-δ : δ.at ⊤ ∘ u ≈ fmap u ∘ u
        m-ε : ∀{A B : obj} -> ε.at (A ⊗ B) ∘ m A B ≈ ε.at A * ε.at B
        m-δ : ∀{A B : obj} -> fmap (m A B) ∘ m (F A) (F B) ∘ δ.at A * δ.at B
                            ≈ δ.at (A ⊗ B) ∘ m A B

-- Type class for W-strong monads (for a Cartesian comonad W)
record WStrongMonad {n}
        {ℂ : Category n} (ℂ-cart : Cartesian ℂ) {Co : Comonad ℂ}
        (Mo : Monad ℂ) (W-cart-com : CartesianComonad Co ℂ-cart)
        : Set (lsuc n) where
    open Category ℂ
    open Comonad Co
    open Monad Mo
    open Functor W renaming (omap to C ; fmap to C-f)
    open Functor T renaming (omap to M ; fmap to M-f)
    open Cartesian ℂ-cart
    open CartesianComonad W-cart-com
    open CartesianFunctor cart-fun

    λᶜ : ∀(A : obj) -> C ⊤ ⊗ A ~> A
    λᶜ _ = π₂

    αᶜ : ∀(A B D : obj) -> (C (A ⊗ B) ⊗ D) ~> (C A ⊗ (C B ⊗ D))
    αᶜ A B D = assoc-right ∘ m⁻¹ A B * id

    field
        -- C-tensorial strength
        st : ∀(A B : obj) -> C A ⊗ M B ~> M (C A ⊗ B)

        -- | Laws
        -- Naturality conditions
        st-nat₁ : ∀{A B D : obj} (f : A ~> B)
               -> M-f (C-f f * id) ∘ st A D ≈ st B D ∘ C-f f * id
        st-nat₂ : ∀{A B D : obj} (f : A ~> B)
               -> M-f (id * f) ∘ st D A ≈ st D B ∘ id * M-f f

        -- Strength and left unit
        st-λ : ∀{A} -> M-f (λᶜ A) ∘ st ⊤ A ≈ λᶜ (M A)
        -- Strength and associativity
        st-α : ∀{A B D} -> st A (C B ⊗ D) ∘ id * st B D ∘ αᶜ A B (M D)
                         ≈ M-f (αᶜ A B D) ∘ st (A ⊗ B) D
        -- Strength and unit
        st-η : ∀{A B} -> st A B ∘ id * η.at B ≈ η.at (C A ⊗ B)
        -- Strength and multiplication
        st-μ : ∀{A B} -> μ.at (C A ⊗ B) ∘ M-f (st A B) ∘ st A (M B)
                       ≈ st A B ∘ (id * μ.at B)

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Example where

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

downFrom : Nat → List Nat
downFrom zero    = []
downFrom (suc n) = n ∷ downFrom n

sum-rec : List Nat → Nat
sum-rec []       = 0
sum-rec (x ∷ xs) = x + sum-rec xs

sum-acc : Nat → List Nat → Nat
sum-acc z [] = z
sum-acc z (x ∷ xs) = sum-acc (z + x) xs

sum-acc! : Nat → List Nat → Nat
sum-acc! z [] = z
sum-acc! 0 (x ∷ xs) = sum-acc! x xs
sum-acc! z (x ∷ xs) = sum-acc! (z + x) xs

n = 10000
bench-rec  = sum-rec    (downFrom n)
bench-acc  = sum-acc  0 (downFrom n)
bench-acc! = sum-acc! 0 (downFrom n)

max_stars_repo_name: L-TChen/agda-bench

max_issues_repo_name: L-TChen/agda-bench

max_forks_repo_name: L-TChen/agda-bench


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Agda.ISetoids.Cocomplete where

open import Level
open import Relation.Binary using (Setoid; module Setoid; Preorder; module Preorder; Rel; _=[_]⇒_)
open import Data.Product using (Σ; _,_)
-- import Relation.Binary.EqReasoning as EqReasoning

open import Categories.Support.Equivalence using (module I→R-Wrapper; setoid-i→r) renaming (Setoid to ISetoid; module Setoid to ISetoid)
open import Categories.Support.SetoidFunctions using (module _⟶_)
open import Categories.Support.PropositionalEquality
import Categories.Support.ZigZag as ZigZag

open import Categories.Category
open import Categories.Functor
open import Categories.Agda
open import Categories.Colimit
open import Categories.Object.Initial
open import Categories.Cocones
open import Categories.Cocone
open import Categories.Agda.ISetoids.Cocomplete.Helpers

open I→R-Wrapper

ISetoidsCocomplete : ∀ {o ℓ e c ℓ′} → Cocomplete o ℓ e (ISetoids (c ⊔ ding (o ⊔ ℓ ⊔ e)) (c ⊔ ℓ′ ⊔ ding (o ⊔ ℓ ⊔ e)))
ISetoidsCocomplete {o} {ℓ} {e} {c} {cℓ} = record { colimit = colimit }
  where
  c′ = c ⊔ ding (o ⊔ ℓ ⊔ e)
  ℓ′ = c ⊔ cℓ ⊔ ding (o ⊔ ℓ ⊔ e)
  C = ISetoids c′ ℓ′
  colimit : ∀ {J : Category o ℓ e} (F : Functor J C) → Colimit F
  colimit {J} F = record { initial = my-initial-cocone }
    where
    module J = Category J
    open Functor F
    open ISetoid
    open _⟶_

    open ColimitCocone {c = c} {cℓ} {J} F

    .my-!-unique : (A : Cocone F) (φ : CoconeMorphism ⊥ A) (x : vertex-carrier) → (_≈_ (Cocone.N A) (CoconeMorphism.f (! {A}) ⟨$⟩ x) (CoconeMorphism.f φ ⟨$⟩ x))
    my-!-unique A φ (X , x) = sym (Cocone.N A) (CoconeMorphism.commute φ (refl (F₀ X)))

    my-initial-cocone : Initial (Cocones F)
    my-initial-cocone = record
      { ⊥ = ⊥
      ; ! = !
      ; !-unique = λ {A} φ {x} {y} x≡y → trans (Cocone.N A) (my-!-unique A φ x) (cong (CoconeMorphism.f φ) x≡y)
      }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import Type
open import Type.Identities
open import Algebra.FunctionProperties.Eq
              renaming (Injective to is-injective)
open import Function.NP
open import Function.Extensionality
open import Data.Fin.NP using (Fin; Fin▹ℕ; _==_)
open import Data.Vec.NP
open import Data.Vec.Properties
open import Data.Product renaming (proj₁ to fst; proj₂ to snd) hiding (map)
open import Data.Zero
open import Data.One
open import Data.Two hiding (_==_)
open import Data.Sum hiding (map)
open import Data.Nat.NP hiding (_==_)
open import Data.Nat.Properties
import Data.List as L
import Data.List.Properties as LP
open L using (List; []; _∷_)
open import Relation.Binary.PropositionalEquality.NP
open import HoTT
open Equivalences
--open import Explore.Fin

is-distinct : {A : Set}{n : ℕ} → Vec A n → Set
is-distinct {n = n} v = is-injective (_‼_ v)
-- is-distinct {n = n} v = {p q : Fin n}(e : v ‼ p ≡ v ‼ q) → p ≡ q

Distinct : (A : Set)(n : ℕ) → Set
Distinct A n = Σ (Vec A n) is-distinct

Injection : (A B : Set) → Set
Injection A B = Σ (A → B) is-injective

Auto : (A : Set) → Set
Auto A = Injection A A

Perm : (n : ℕ) → Set
Perm n = Distinct (Fin n) n

module _ {n} {{_ : FunExt}} where
    Perm→Auto : Perm n → Auto (Fin n)
    Perm→Auto (v , v-dist) = _‼_ v , v-dist

    tabulate-dist : (f : Fin n → Fin n) (f-inj : Injective f) → is-distinct
    tabulate-dist f f-inj e = f-inj (! lookup∘tabulate f _ ∙ e ∙ lookup∘tabulate f _)

    Auto→Perm : Auto (Fin n) → Perm n
    Auto→Perm (f , f-inj)
      = tabulate f , λ e → f-inj (! lookup∘tabulate f _ ∙ e ∙ lookup∘tabulate f _)

Goal: tr is-injective (λ= (lookup∘tabulate f))
      (snd (Auto→Perm (f , f-inj)))
      ≡ f-inj
    Perm→Auto→Perm : ∀ a → Perm→Auto (Auto→Perm a) ≡ a
    Perm→Auto→Perm (f , f-inj) = pair= (λ= (lookup∘tabulate f)) {!!}

    Auto→Perm→Auto : ∀ π → Auto→Perm (Perm→Auto π) ≡ π
    Auto→Perm→Auto (v , v-dist) = pair= (tabulate∘lookup v) {!!}

    Perm≃Auto : Perm n ≃ Auto (Fin n)
    Perm≃Auto = equiv Perm→Auto Auto→Perm Perm→Auto→Perm Auto→Perm→Auto

Arr : (n : ℕ) → Set
Arr n = Vec (Fin n) n

Sum : Set → Set
Sum A = (A → ℕ) → ℕ
Prod = Sum

postulate
    sumFin : (n : ℕ) → Sum (Fin n)
    prodFin : (n : ℕ) → Prod (Fin n)
    -- sumVec : (A : Set)(n : ℕ) (f : Vec A n → ℕ) → ℕ
    sumArr : (n : ℕ) → Sum (Arr n)
    prodFinEq : {n : ℕ}(x y : Fin n) → Prod (x ≡ y)

distinctℕ : (n : ℕ) → (sumArr  n λ v →
                        prodFin n λ p →
                        prodFin n λ q →
                        prodFinEq p q λ e →
                        𝟚▹ℕ (p == q)) ≡ {!!}
distinctℕ = {!!}

{-
ℕ< : ℕ → Set
ℕ< n = Σ ℕ λ x → x < n

sum< : (n : ℕ) (f : ℕ< n → ℕ) → ℕ
sum< n f = {!!}

prod< : (n : ℕ) (f : ℕ< n → ℕ) → ℕ
prod< n f = {!!}

{-
foo : ∀ n a x → sumFin n λ i → a i * x ^ i
foo = ?

bar : ∀ n a x → sumFin n λ i → a i * x ^ i
bar = ?
-}

baz : ∀ n (u : ℕ< n → ℕ) → (sum< n λ { (i , p) → prod< i (λ { (j , q) → u (j , <-trans q p) }) }) ≡ {!!}
baz = {!!}

module _ n (u : ℕ< n → Set) {{_ : UA}} {{_ : FunExt}} where
    open ≡-Reasoning
    Baz : _ ≡ _
    Baz = (Σ (ℕ< n) λ { (i , p) → Π (ℕ< i) λ { (j , q) → u (j , <-trans q p) } })
        ≡⟨ ! Σ-assoc ⟩
          (Σ ℕ λ i → Σ (i < n) λ p → Π (ℕ< i) λ { (j , q) → u (j , <-trans q p) })
        ≡⟨ Σ=′ ℕ (λ i → Σ=′ (i < n) λ p → ΠΣ-curry) ⟩
          (Σ ℕ λ i → Σ (i < n) λ p → Π ℕ λ j → Π (j < i) λ q → u (j , <-trans q p))
        ∎

module DataVersion (A : ★) where
    open import Data.Tree.Binary
    data T : BinTree A → ★ where
      empty : T empty
      _⊕_ : ∀ {t u} → (𝟙 ⊎ T t × T u) → T (fork t u)

module TypeVersion where
    ε = 𝟙
    _⊕_ : ★ → ★ → ★
    _⊕_ = λ u z → ε ⊎ u × z

module ListVersion where
    open L
    open ≡-Reasoning
    map-∘ = LP.map-compose

    sum-lin : ∀ k xs → sum (map (_*_ k) xs) ≡ k * sum xs
    sum-lin k []       = ℕ°.*-comm 0 k
    sum-lin k (x ∷ xs) = k * x + sum (map (_*_ k) xs)
                       ≡⟨ ap (_+_ (k * x)) (sum-lin k xs) ⟩
                          k * x + k * sum xs
                       ≡⟨ ! fst ℕ°.distrib k x (sum xs) ⟩
                          k * (x + sum xs)
                       ∎

    lemma : ∀ x xss → sum (map product (map (_∷_ x) xss)) ≡ x * sum (map product xss)
    lemma x xss = sum (map product (map (_∷_ x) xss))
                ≡⟨ ap sum (! map-∘ xss) ⟩
                  sum (map (product ∘ _∷_ x) xss)
                ≡⟨by-definition⟩
                  sum (map (_*_ x ∘ product) xss)
                ≡⟨ ap sum (map-∘ xss) ⟩
                  sum (map (_*_ x) (map product xss))
                ≡⟨ sum-lin x (map product xss) ⟩
                  x * sum (map product xss)
                ∎

    ε = 1
    _⊕_ = λ u z → ε + u * z
    t3 = ∀ xs → sum (map product (inits xs)) ≡ foldr _⊕_ ε xs
    t4 : t3
    t4 [] = refl
    t4 (x ∷ xs) = ap suc (lemma x (inits xs) ∙ ap (_*_ x) (t4 xs))
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text: unquoteDef x = ?

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Helper.Fin where

open import Data.Fin hiding (_+_)
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation

------------------------------------------------------------------------
-- Fin magic
------------------------------------------------------------------------

+₁ : (x y : ℕ) (i : Fin x) -> Fin (x + y)
+₁ zero    y ()
+₁ (suc x) y zero = zero
+₁ (suc x) y (suc i) = suc (+₁ x y i)

+₂ : (x y : ℕ) (j : Fin y) -> Fin (x + y)
+₂ zero    y j = j
+₂ (suc x) y j = suc (+₂ x y j)

data Fin+ (x y : ℕ) : Fin (x + y) -> Set where
  is+₁ : (i : Fin x) -> Fin+ x y (+₁ x y i)
  is+₂ : (j : Fin y) -> Fin+ x y (+₂ x y j)

⨁ : (x y : ℕ) (i : Fin (x + y)) -> Fin+ x y i
⨁ zero y i = is+₂ i
⨁ (suc x) y zero = is+₁ zero
⨁ (suc x) y (suc i) with ⨁ x y i
⨁ (suc x) y (suc ._) | is+₁ i = is+₁ (suc i)
⨁ (suc x) y (suc ._) | is+₂ j = is+₂ j

[_,_] : {X : Set} {x y : ℕ} (l : Fin x -> X) (r : Fin y -> X) -> {s : Fin (x + y)} -> Fin+ x y s -> X
[_,_] l r {._} (is+₁ i) = l i
[_,_] l r {._} (is+₂ j) = r j

{-
[_,_] : {X : Set} {x y : ℕ} (l : Fin x -> X) (r : Fin y -> X) -> (s : Fin (x + y)) -> X
[_,_] {X} {x} {y} l r s with ⨁ x y s
[_,_] l r ._ | is+₁ i = l i
[_,_] l r ._ | is+₂ j = r j
-}

× : (x y : ℕ) (i : Fin x) (j : Fin y) -> Fin (x * y)
× zero _ () _
× (suc x) y zero j = +₁ y (x * y) j
× (suc x) y (suc i) j = +₂ y (x * y) (× x y i j)

data Fin* (x y : ℕ) : Fin (x * y) -> Set where
  is× : (i : Fin x) (j : Fin y) -> Fin* x y (× x y i j)

⨂ : (x y : ℕ) (i : Fin (x * y)) -> Fin* x y i
⨂ zero y ()
⨂ (suc x) y i with ⨁ y (x * y) i
⨂ (suc x) y ._ | is+₁ i = is× zero i
⨂ (suc x) y ._ | is+₂ j with ⨂ x y j
⨂ (suc x) y ._ | is+₂ ._ | is× i j  = is× (suc i) j

------------------------------------------------------------------------
-- Fin lemma's
------------------------------------------------------------------------

suc-eq : {n : ℕ} {x x₁ : Fin n} -> ((Data.Fin.suc x) ≡ (Data.Fin.suc x₁)) -> (x ≡ x₁)
suc-eq refl = refl

+-eq : {n n₁ : ℕ} {x x₁ : Fin n} -> (m : Fin n₁) -> ((m Data.Fin.+ x) ≡ (m Data.Fin.+ x₁)) -> (x ≡ x₁)
+-eq zero p = p
+-eq (suc m) p = +-eq m (suc-eq p)

+-eq₁ : {n n₁ : ℕ} {x x₁ : Fin n} -> (+₁ n n₁ x ≡ +₁ n n₁ x₁) -> (x ≡ x₁)
+-eq₁ {x = zero} {x₁ = zero} p = refl
+-eq₁ {x = zero} {suc x₁} ()
+-eq₁ {x = suc x} {zero} ()
+-eq₁ {x = suc x} {x₁ = suc x₁} p with +-eq (fromℕ 1) p
... | p1 with +-eq₁ p1
... | p2 = cong suc p2

+-eq₂ : {n n₁ : ℕ} {x x₁ : Fin n₁} -> (+₂ n n₁ x ≡ +₂ n n₁ x₁) -> (x ≡ x₁)
+-eq₂ {zero} refl = refl
+-eq₂ {suc n} {suc n₁} {zero} {zero} refl = refl
+-eq₂ {suc n} {suc n₁} {zero} {suc x₁} p with suc-eq p
... | p1 = +-eq₂ {n} {suc n₁} p1
+-eq₂ {suc n} {suc n₁} {suc x} {zero} p with suc-eq p
... | p1 = +-eq₂ {n} {suc n₁} p1
+-eq₂ {suc n} {suc n₁} {suc x} {suc x₁} p with suc-eq p
... | p1 = +-eq₂ {n} {suc n₁} p1

¬+-eq₁ : {n m : ℕ} {x : Fin n} {y : Fin m} -> ¬( (+₁ n m) x ≡ (+₂ n m) y)
¬+-eq₁ {zero} {zero} {()}
¬+-eq₁ {zero} {suc m} {()}
¬+-eq₁ {suc n} {zero} {y = ()}
¬+-eq₁ {suc n} {suc m} {zero} ()
¬+-eq₁ {suc n} {suc m} {suc x} {zero} with ¬+-eq₁ {n} {suc m} {x} {zero}
... | p1 = contraposition suc-eq p1
¬+-eq₁ {suc n} {suc m} {suc x} {suc y} with ¬+-eq₁ {n} {suc m} {x} {suc y}
... | p1 = contraposition suc-eq p1

¬+-eq₂ : {n m : ℕ} {x : Fin n} {y : Fin m} -> ¬( (+₂ n m) y ≡ (+₁ n m) x)
¬+-eq₂ {zero} {zero} {()} x₁
¬+-eq₂ {zero} {suc m} {()} x₁
¬+-eq₂ {suc n} {zero} {zero} ()
¬+-eq₂ {suc n} {zero} {suc x} {()}
¬+-eq₂ {suc n} {suc m} {zero} {zero} ()
¬+-eq₂ {suc n} {suc m} {zero} {suc y} ()
¬+-eq₂ {suc n} {suc m} {suc x} {zero} with ¬+-eq₂ {n} {suc m} {x} {zero}
... | p1 = contraposition suc-eq p1
¬+-eq₂ {suc n} {suc m} {suc x} {suc y} =  contraposition suc-eq (¬+-eq₂ {n} {suc m} {x} {suc y})

×-equal₁ : ∀ {n m : ℕ} {x₁ x₂ : Fin n} {y₁ y₂ : Fin m} -> (× n m x₁ y₁) ≡ (× n m x₂ y₂) -> (y₁ ≡ y₂)
×-equal₁ {zero} {x₁ = ()} x
×-equal₁ {suc n} {zero} {y₁ = ()} x
×-equal₁ {suc n} {suc m} {zero} {zero} p = +-eq₁ p
×-equal₁ {suc n} {suc m} {zero} {suc x₂} {zero} ()
×-equal₁ {suc n} {suc m} {zero} {suc x₂} {suc y₁} p with suc-eq p
... | p1 with ¬+-eq₁ {m} {(n * suc m)} p1
×-equal₁ {suc n} {suc m} {zero} {suc x₂} {suc y₁} p | p1 | ()
×-equal₁ {suc n} {suc m} {suc x₁} {zero} {zero} {zero} p = refl
×-equal₁ {suc n} {suc m} {suc x₁} {zero} {zero} {suc y₂} p with suc-eq p
... | p1 with ¬+-eq₂ p1
×-equal₁ {suc n} {suc m} {suc x₁} {zero} {zero} {suc y₂} p | p1 | ()
×-equal₁ {suc n} {suc m} {suc x₁} {zero} {suc y₁} {zero} ()
×-equal₁ {suc n} {suc m} {suc x₁} {zero} {suc y₁} {suc y₂} p with suc-eq p
... | p1 with ¬+-eq₂ p1
×-equal₁ {suc n} {suc m} {suc x₁} {zero} {suc y₁} {suc y₂} p | p1 | ()
×-equal₁ {suc n} {suc m} {suc x₁} {suc x₂} p with suc-eq p
... | p2 with +-eq₂ {suc m} {(n * suc m)} p
... | p3 = ×-equal₁ {n} {suc m} p3

×-equal₂ : ∀ {n m : ℕ} {x₁ x₂ : Fin n} {y₁ y₂ : Fin m} -> (× n m x₁ y₁) ≡ (× n m x₂ y₂) -> (x₁ ≡ x₂)
×-equal₂ {zero} {x₁ = ()} x
×-equal₂ {suc n} {zero} {y₁ = ()} x
×-equal₂ {suc n} {suc m} {zero} {zero} x = refl
×-equal₂ {suc n} {suc m} {zero} {suc x₂} {zero} {zero} ()
×-equal₂ {suc n} {suc m} {zero} {suc x₂} {zero} {suc y₂} ()
×-equal₂ {suc n} {suc m} {zero} {suc x₂} {suc y₁} {zero} p with suc-eq p
... | p1 with ¬+-eq₁ p1
×-equal₂ {suc n} {suc m} {zero} {suc x₂} {suc y₁} {zero} p | p1 | ()
×-equal₂ {suc n} {suc m} {zero} {suc x₂} {suc y₁} {suc y₂} p with suc-eq p
... | p1 with ¬+-eq₁ p1
×-equal₂ {suc n} {suc m} {zero} {suc x₂} {suc y₁} {suc y₂} p | p1 | ()
×-equal₂ {suc n} {suc m} {suc x₁} {zero} {y₂ = zero} ()
×-equal₂ {suc n} {suc m} {suc x₁} {zero} {zero} {suc y₂} p with suc-eq p
... | p1 with ¬+-eq₂ p1
×-equal₂ {suc n} {suc m} {suc x₁} {zero} {zero} {suc y₂} p | p1 | ()
×-equal₂ {suc n} {suc m} {suc x₁} {zero} {suc y₁} {suc y₂} p  with suc-eq p
... | p1 with ¬+-eq₂ p1
×-equal₂ {suc n} {suc m} {suc x₁} {zero} {suc y₁} {suc y₂} p | p1 | ()
×-equal₂ {suc n} {suc m} {suc x₁} {suc x₂} p with suc-eq p
... | p1 with +-eq₂ {m} {(n * suc m)} p1
... | p2 with ×-equal₂ {n} {suc m} p2
... | p3 = cong suc p3

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


text:
{-
  Copyright 2019 Lisandra Silva

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

      http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.
-}

open import Prelude
open import Data.Fin hiding (_≟_; _<_; _+_; pred; _≤_; lift)
open import Data.List
open import Data.List.Properties
open import Relation.Nullary.Negation using (contradiction ; contraposition)

open import StateMachineModel

module Examples.ProducerConsumer2
  (Message : Set) -- Message type
  where

  -----------------------------------------------------------------------------
  -- SPECIFICATION
  -----------------------------------------------------------------------------
  record State : Set where
    field
     produced   : List Message
     consumed   : List Message
  open State

  data MyEvent : Set where
    produce : Message → MyEvent
    consume : Message → MyEvent

  data MyEnabled : MyEvent → State → Set where
    prodEnabled : ∀ {st : State} {msg} -- always enabled
                  → MyEnabled (produce msg) st
    consEnabled : ∀ {st : State} {msg}
                  → (cons<prod : length (consumed st) < length (produced st) )
                  → msg ≡ lookup (produced st) (fromℕ≤ cons<prod)
                  → MyEnabled (consume msg) st

  MyAction : ∀ {preState : State} {event : MyEvent}
             → MyEnabled event preState
             → State
  MyAction {preSt} {produce m} enabled = record preSt
                                          { produced  = produced preSt ++ [ m ]
                                          }
  MyAction {preSt} {consume m} enabled = record preSt
                                          { consumed  = consumed preSt ++ [ m ]
                                          }

  initialState : State
  initialState = record
                   { produced   = []
                   ; consumed   = []
                   }

  MyStateMachine : StateMachine State MyEvent
  MyStateMachine = record
                     { initial = λ st → produced st ≡ [] × consumed st ≡ []
                     ; enabled = MyEnabled
                     ; action  = MyAction
                     }

  MyEventSet : EventSet {Event = MyEvent}
  MyEventSet (produce m) = ⊥
  MyEventSet (consume m) = ⊤

  data MyWeakFairness : EventSet → Set where
    wf : MyWeakFairness MyEventSet

  MySystem : System State MyEvent
  MySystem = record
             { stateMachine = MyStateMachine
             ; weakFairness = MyWeakFairness
             }

  -----------------------------------------------------------------------------
  -- PROOFS
  -----------------------------------------------------------------------------
  open LeadsTo State MyEvent MySystem

  myWFR : ∀ {n} → Z → State → Set
  myWFR {n} d st =  d + length (consumed st) ≡ n × n ≤ length (produced st)

  length-suc : ∀ {x : Message} l → length (l ++ [ x ]) ≡ 1 + length l
  length-suc {x} l rewrite length-++ l {[ x ]} | +-comm (length l) 1 = refl

  <⇒≤-l : ∀ {n} (m : Message) (l : List Message)
             → length l < n
             → length (l ++ [ m ]) ≤ n
  <⇒≤-l m l l<n rewrite length-suc {m} l = l<n

  suc-+-l : ∀ {w} (m : Message) (l : List Message)
               →  w + length (l ++ m ∷ []) ≡ suc (w + length l)
  suc-+-l {w} m l rewrite length-suc {m} l = +-suc w (length l)

  inv-cons≤prod : Invariant
                    MyStateMachine
                    λ state → length (consumed state) ≤ length (produced state)
  inv-cons≤prod (init (refl , refl)) = z≤n
  inv-cons≤prod (step {st} {produce m} rs enEv)
    rewrite length-suc {m} (produced st)
      = ≤-step (inv-cons≤prod rs)
  inv-cons≤prod (step {st} {consume m} rs (consEnabled c<p x₁))
      = <⇒≤-l m (consumed st) c<p
      --subst (_≤ length (produced st)) (sym (length-suc {m} (consumed st))) c<p

  m≤n⇒m≡n⊎m<n : ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
  m≤n⇒m≡n⊎m<n {0} {0} z≤n = inj₂ refl
  m≤n⇒m≡n⊎m<n {0} {suc n} x = inj₁ (s≤s z≤n)
  m≤n⇒m≡n⊎m<n {suc m} {suc n} (s≤s x)
    with m≤n⇒m≡n⊎m<n x
  ... | inj₁ m<n  = inj₁ (s≤s m<n)
  ... | inj₂ refl = inj₂ refl

  [Q∪Fx] : ∀ {st : State} {n}
           → length (produced st) ≡ n
           → length (consumed st) ≤ n
           → length (consumed st) ≡ n ⊎ ∃[ x ] myWFR {n} x st
  [Q∪Fx] {st} {n} refl cons≤n
    with m≤n⇒m≡n⊎m<n cons≤n
  ... | inj₂ cons≡n = inj₁ cons≡n
  ... | inj₁ cons<n = inj₂ ( n ∸ length (consumed st) , m∸n+n≡m cons≤n , ≤-refl )

  wfr-l++ : ∀ {m : Message} {n} l
                → n < length l
                → length (l ++ [ m ]) ∸ 1 ∸ n + n ≡ length l
                × length l ≤ length (l ++ [ m ])
  wfr-l++ {m} {n} l n<l rewrite length-suc {m} l
    = (m∸n+n≡m (<⇒≤ n<l)) , ≤-step ≤-refl

{-  [P]l-t[Q∪Fx] : ∀ {n}
                 → λ preSt → length (produced preSt) ≡ n
                           × length (consumed preSt) < n
                   l-t
                   (λ posSt → length (consumed posSt) ≡ n) ∪ [∃ x ∶ myWFR {n} x ]
-}
  [P]l-t[Q∪Fx] : ∀ {n}
                 → (_≡ n) ∘ length ∘ produced   ∩   (_< n) ∘ length ∘ consumed
                   l-t
                   (_≡ n) ∘ length ∘ consumed   ∪   [∃ x ∶ myWFR {n} x ]
  [P]l-t[Q∪Fx] =
    viaEvSet
      MyEventSet
      wf
      ( λ { (consume m) evSet
              → hoare λ { {st} (p≡n , c<p) enEv → let state = MyAction {st} enEv
                                                      cons  = consumed st
                                                      c≤p   = <⇒≤-l m cons c<p
                                                  in [Q∪Fx] {state} p≡n c≤p }
          }
      )
      (λ { (produce m) x
             → hoare λ { {st} (refl , c<p) enEv
                         → let l = length (produced st ++ [ m ]) ∸ 1
                               c = length (consumed st)
                           in inj₂ (inj₂ ( l ∸ c , wfr-l++ (produced st) c<p))}
         ; (consume x₁) ⊥ → ⊥-elim (⊥ tt)
         }
      )
      λ { {state} rs (refl , c<p)
          → consume (lookup (produced state) (fromℕ≤ c<p))
          , tt
          , (consEnabled c<p refl) }

  m+n<o⇒n<o : ∀ {l} w m → w + m < l → m < l
  m+n<o⇒n<o w m w+m<l rewrite sym (+-suc w m) = m+n≤o⇒n≤o w w+m<l

  mono-l++ : ∀ {n} (m : Message) l → n ≤ length l → n ≤ length (l ++ [ m ])
  mono-l++ m l n<l rewrite length-suc {m} l = ≤-step n<l

{-[Fw]l-t[Q∪Fx] : ∀ {w n}
                  → myWFR {n} w
                    l-t
                    (λ posSt → length (consumed posSt) ≡ n)
                    ∪ [∃ x ⇒ _< w ∶ myWFR {n} x ]
-}
  [Fw]l-t[Q∪Fx] : ∀ {n} w
                  → myWFR {n} w
                    l-t
                    (_≡ n) ∘ length ∘ consumed   ∪   [∃ x ⇒ _< w ∶ myWFR {n} x ]
  [Fw]l-t[Q∪Fx] 0 = viaInv λ { rs (c≡n , c<p) → inj₁ c≡n }
  [Fw]l-t[Q∪Fx] (suc w) =
    viaEvSet
      MyEventSet
      wf
      (λ { (consume m) ⊤ → hoare λ { {st} (refl , c<p) (consEnabled cons<prod x)
                           → inj₂ (w , ≤-refl , suc-+-l m (consumed st) , c<p)}
         }
      )
      (λ { (produce m) ⊥ → hoare λ { {st} (c≡n , n≤p) enEv
                                 → inj₁ (c≡n , mono-l++ m (produced st) n≤p) }
         ; (consume m) ⊥ → ⊥-elim (⊥ tt)
         }
      )
      λ { {st} rs (refl , n<p) → let c<l = m+n<o⇒n<o w (length (consumed st)) n<p
                                 in consume (lookup (produced st) (fromℕ≤ c<l))
                                  , tt
                                  , (consEnabled c<l refl) }

{-P2-l-t-Q : ∀ {n}
            → λ preSt → length (produced preSt) ≡ n
                      × length (consumed preSt) < n
              l-t
              λ posSt → length (consumed posSt) ≡ n
-}
  cons<n-l-t-cons≡n : ∀ {n}
             → (_≡ n) ∘ length ∘ produced   ∩   (_< n) ∘ length ∘ consumed
               l-t
               (_≡ n) ∘ length ∘ consumed
  cons<n-l-t-cons≡n = viaWFR myWFR [P]l-t[Q∪Fx] [Fw]l-t[Q∪Fx]

  P⊆P1∪P2 : ∀ {m n : ℕ} {ℓ} { P : Set ℓ } → P × m ≤ n → P × m ≡ n ⊎ P × m < n
  P⊆P1∪P2 {m} {n} (p , m≤n)
    with m ≟ n
  ... | yes prf = inj₁ (p , prf)
  ... | no  imp = inj₂ (p , (≤∧≢⇒< m≤n imp))

{-c≢n-l-t-c<n : ∀ {n} → ( λ preSt → length (produced preSt) ≡ n
                                  × length (consumed preSt) ≢ n )
                        l-t
                        ( λ posSt → length (produced posSt) ≡ n
                                  × length (consumed posSt) < n )
-}
  p≡n-l-t-c≤n : ∀ {n}
                → (_≡ n) ∘ length ∘ produced
                  l-t
                  (_≡ n) ∘ length ∘ produced   ∩  (_≤ n) ∘ length ∘ consumed
  p≡n-l-t-c≤n = viaInv (λ { {st} rs refl → refl , (inv-cons≤prod rs) })

  progressOnLength : ∀ n
                     → (_≡ n) ∘ length ∘ produced
                       l-t
                       (_≡ n) ∘ length ∘ consumed
  progressOnLength n =
    viaTrans
      p≡n-l-t-c≤n
      (viaDisj
         (λ { {st} (p≡n , c≤n) → P⊆P1∪P2 (p≡n , c≤n) })
         (viaInv (λ { {st} rs (_ , c≡n) → c≡n }))
         cons<n-l-t-cons≡n )

  lookup-++ : ∀ {n} {m : Message} l₁ l₂
                 → (finl₁ : n < length l₁) → (finl₂ : n < length l₂)
                 → (fin++ : n < length (l₂ ++ [ m ]))
                 → lookup l₁ (fromℕ≤ finl₁) ≡ lookup l₂ (fromℕ≤ finl₂)
                 → lookup l₁ (fromℕ≤ finl₁) ≡ lookup (l₂ ++ [ m ]) (fromℕ≤ fin++)
  lookup-++ {zero}  (x ∷ l₁) (x₁ ∷ l₂) finl₁ finl₂ fin++ ll₁≡ll₂ = ll₁≡ll₂
  lookup-++ {suc n} (x ∷ l₁) (x₁ ∷ l₂) finl₁ finl₂ fin++ ll₁≡ll₂
    = lookup-++ l₁ l₂ (≤-pred finl₁) (≤-pred finl₂) (≤-pred fin++) ll₁≡ll₂

  n≤l++⇒n≤l⊎n≡l : ∀ {m : Message} {n} l
                  → n ≤ length (l ++ [ m ])
                  → n ≤ length l ⊎ n ≡ 1 + length l
  n≤l++⇒n≤l⊎n≡l {m} l n≤l++ rewrite length-suc {m} l
    with m≤n⇒m≡n⊎m<n n≤l++
  ... | inj₁ 1+n≤1+l = inj₁ (≤-pred 1+n≤1+l)
  ... | inj₂ n≡1+l   = inj₂ n≡1+l

  lookup-length : ∀ {m : Message} l
                     → (prf : length l < length (l ++ [ m ]))
                     → lookup (l ++ [ m ]) (fromℕ≤ prf) ≡ m
  lookup-length [] prf = refl
  lookup-length (x ∷ l) prf = lookup-length l (≤-pred prf)

  <-refl-l : ∀ {m : Message} l → length l < length (l ++ [ m ])
  <-refl-l [] = s≤s z≤n
  <-refl-l (x ∷ l) = s≤s (<-refl-l l)

  lookup-c≡lookup-p : ∀ {n}
                    → Invariant
                        MyStateMachine
                        λ st → (prfC : n < length (consumed st))
                             → (prfP : n < length (produced st))
                             → lookup (consumed st) (fromℕ≤ prfC)
                             ≡ lookup (produced st) (fromℕ≤ prfP)
  lookup-c≡lookup-p {n} (init (refl , refl)) () ()
  lookup-c≡lookup-p {n} (step {st} {produce x} rs enEv) prfC prfP
    = let c<p = <-transˡ prfC (inv-cons≤prod rs)
      in lookup-++
           (consumed st) (produced st)
           prfC c<p prfP
           (lookup-c≡lookup-p rs prfC c<p)
  lookup-c≡lookup-p {n} (step {st} {consume m} rs enEv) prfC prfP
    with enEv
  ... | consEnabled cons<prod m≡lookup
      with n≤l++⇒n≤l⊎n≡l (consumed st) prfC
  ... | inj₁ n<c  = sym (lookup-++
                          (produced st) (consumed st)
                          prfP n<c prfC
                          (sym (lookup-c≡lookup-p rs n<c prfP)))
  ... | inj₂ refl = trans
                      (lookup-length (consumed st) (<-refl-l (consumed st)))
                      m≡lookup

  -- TODO : Generalize all functions about lists
  take-n-l++ : ∀ {n} (l₁ l₂ : List Message)
               → n ≤ length l₁
               → take n l₁ ≡ take n (l₁ ++ l₂)
  take-n-l++ {zero}  l₁ l₂ n≤l₁ = refl
  take-n-l++ {suc n} (x ∷ l₁) l₂ n≤l₁
    rewrite take-n-l++ l₁ l₂ (≤-pred n≤l₁) = refl

  l₁≡l₂ : ∀ {m₁ m₂ : Message} {l₁ l₂}
          → m₁ ∷ l₁ ≡ m₂ ∷ l₂
          → m₁ ≡ m₂ × l₁ ≡ l₂
  l₁≡l₂ refl = refl , refl

  m₁≡m∧l₁≡l₂₂⇒l≡l : ∀ {m₁ m₂ : Message} {l₁ l₂}
                    → m₁ ≡ m₂
                    → l₁ ≡ l₂
                    → m₁ ∷ l₁ ≡ m₂ ∷ l₂
  m₁≡m∧l₁≡l₂₂⇒l≡l refl refl = refl

  taken×lookup : ∀ {m : Message} l₁ l₂
                 → (prf : length l₁ < length l₂)
                 → l₁ ≡ take (length l₁) l₂
                 → m ≡ lookup l₂ (fromℕ≤ prf)
                 → l₁ ++ [ m ] ≡ take (suc (length l₁)) l₂
  taken×lookup [] (x₂ ∷ l₂) l₁<l₂ l₁≡take refl = refl
  taken×lookup (x₂ ∷ l₁) (x₃ ∷ l₂) l₁<l₂ l₁≡tk m≡lkp
    rewrite taken×lookup l₁ l₂ (≤-pred l₁<l₂) (proj₂ (l₁≡l₂ l₁≡tk)) m≡lkp
      = m₁≡m∧l₁≡l₂₂⇒l≡l (proj₁ (l₁≡l₂ l₁≡tk)) refl

  take1+l≡takel++m : ∀ {m : Message} {n} l
                         → n ≡ 1 + length l
                         → take n (l ++ [ m ]) ≡ l ++ [ m ]
  take1+l≡takel++m [] refl = refl
  take1+l≡takel++m {m} (x₁ ∷ l) refl
    rewrite take1+l≡takel++m {m} l refl = refl

  take-length≡l : ∀ (l : List Message) → take (length l) l ≡ l
  take-length≡l [] = refl
  take-length≡l (x ∷ l) rewrite take-length≡l l = refl

  [c]-prefix-[p] : ∀ {n}
                   → Invariant
                       MyStateMachine
                       λ st → n ≤ length (consumed st)
                            → take n (consumed st) ≡ take n (produced st)
  [c]-prefix-[p] {n} (init (refl , refl)) n<lc = refl
  [c]-prefix-[p] {n} (step {st} {produce m} rs enEv) n<lc
    = trans
        ([c]-prefix-[p] rs n<lc)
        (take-n-l++ (produced st) ([ m ]) (≤-trans n<lc (inv-cons≤prod rs)))
  [c]-prefix-[p] {n} (step {st} {consume m} rs enEv) n≤c++
     with enEv
  ... | consEnabled cons<prod m≡lookup
       with n≤l++⇒n≤l⊎n≡l (consumed st) n≤c++
  ... | inj₁ n≤c   = trans
                       (sym (take-n-l++ (consumed st) [ m ] n≤c))
                       ([c]-prefix-[p] rs n≤c)
  ... | inj₂ refl =  let tc≡tp = [c]-prefix-[p] rs ≤-refl
                     in trans
                          (take1+l≡takel++m (consumed st) refl)
                          (taken×lookup
                            (consumed st) (produced st) cons<prod
                            (trans (sym (take-length≡l (consumed st))) tc≡tp)
                            m≡lookup)

  take-presrv-prfix : ∀ {l₁ l₂} {m : Message}
                          → take (length l₂) l₁ ≡ l₂
                          → take (length l₂) (l₁ ++ [ m ]) ≡ l₂
  take-presrv-prfix {[]} {[]} {m} tl₁≡l₂ = refl
  take-presrv-prfix {m₁ ∷ l₁} {[]} {m} tl₁≡l₂ = refl
  take-presrv-prfix {m₁ ∷ l₁} {m₂ ∷ l₂} {m} tl₁≡l₂
    with l₁≡l₂ tl₁≡l₂
  ... | m₁≡m₂ , tll₁≡l₂
      with take-presrv-prfix {m = m} tll₁≡l₂
  ... | tl₁+m≡l₂ = m₁≡m∧l₁≡l₂₂⇒l≡l m₁≡m₂ tl₁+m≡l₂

  stable-produced : ∀ {msgs}
                    → Stable MyStateMachine
                             λ st → take (length msgs) (produced st) ≡ msgs
  stable-produced {msgs} {st} {produce m}  enEv tkp≡m = take-presrv-prfix tkp≡m
  stable-produced {msgs} {st} {consume x₁} enEv tkp≡m = tkp≡m

  aux : ∀ {n m} {l₁ l₂ : List Message}
        → n ≡ m
        → take n l₁ ≡ take n l₂
        → take n l₁ ≡ take m l₂
  aux refl prf = prf

  lc≡lm-l-t-c≡m : ∀ {msgs}
        → (λ preSt → length (consumed preSt) ≡ length msgs
             × take (length msgs) (produced preSt) ≡ msgs )
          l-t
           λ posSt → consumed posSt ≡ msgs
  lc≡lm-l-t-c≡m {msgs} =
    viaInv
      (λ { {st} rs (lc≡lm , tp≡msgs)
            → trans
                (trans
                  (sym (take-length≡l (consumed st)))
                  (aux lc≡lm ([c]-prefix-[p] rs ≤-refl)))
                tp≡msgs })

  msgsPrefixProd : ∀ {msgs} → (λ st → produced st ≡ msgs)
                              l-t
                              (λ st →  length (produced st) ≡ length msgs
                                     × take (length msgs) (produced st) ≡ msgs)
  msgsPrefixProd = viaInv (λ { {st} rs refl → refl , take-length≡l (produced st) })

  progress : ∀ {msgs} → (_≡ msgs) ∘ produced l-t (_≡ msgs) ∘ consumed
  progress {msgs} = viaStable
                      stable-produced
                      msgsPrefixProd
                      (progressOnLength (length msgs))
                      lc≡lm-l-t-c≡m

{-
  Another way of proving without the viaStable rule

  progressOnLength' : ∀ {msgs} → (λ st₁ → length (produced st₁) ≡ length msgs
                                     × take (length msgs) (produced st₁) ≡ msgs)
                                 l-t
                                 λ st₂ → length (consumed st₂) ≡ length msgs
                                        × take (length msgs) (produced st₂) ≡ msgs

  progress : ∀ {msgs} → (_≡ msgs) ∘ produced l-t (_≡ msgs) ∘ consumed
  progress {msgs} =
      viaTrans
      (viaInv inv-prodPrefix)
      (viaTrans
        progressOnLength'
        lc≡lm-l-t-c≡m)
-}

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


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

open import lib.Basics
open import lib.NType2

-- [Subtype] is defined in lib.NType.

module lib.types.Subtype where

infix 40 _⊆_
_⊆_ : ∀ {i j₁ j₂} {A : Type i} → SubtypeProp A j₁ → SubtypeProp A j₂
  → Type (lmax i (lmax j₁ j₂))
P₁ ⊆ P₂ = ∀ a → SubtypeProp.prop P₁ a → SubtypeProp.prop P₂ a

infix 80 _∘sub_
_∘sub_ : ∀ {i j k} {A : Type i} {B : Type j}
  → SubtypeProp B k → (A → B) → SubtypeProp A k
P ∘sub f = SubtypeProp.prop P ∘ f , level where
  abstract level = SubtypeProp.level P ∘ f

Subtype-has-dec-eq : ∀ {i j} {A : Type i} (subProp : SubtypeProp A j)
  → has-dec-eq A → has-dec-eq (Subtype subProp)
Subtype-has-dec-eq subProp dec s₁ s₂ with dec (fst s₁) (fst s₂)
... | inl s₁=s₂ = inl (Subtype=-out subProp s₁=s₂)
... | inr s₁≠s₂ = inr λ s₁=s₂ → s₁≠s₂ (ap fst s₁=s₂)

{- Dependent paths in a Σ-type -}
module _ {i j k} {A : Type i} {B : A → Type j} (subB : (a : A) → SubtypeProp (B a) k)
  where

  ↓-Subtype-in : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : SubtypeProp.prop (subB x) r} {s' : SubtypeProp.prop (subB x') r'}
    (q : r == r' [ B ↓ p ])
    → (r , s) == (r' , s') [ (λ x → Subtype (subB x)) ↓ p ]
  ↓-Subtype-in {p = idp} q = Subtype=-out (subB _) q

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

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

open import Cubical.Data.Sigma

open import Cubical.Foundations.Structure
open import Cubical.Foundations.Structure using (typ) public
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism

private
  variable
    ℓ ℓ' : Level

Pointed : (ℓ : Level) → Type (ℓ-suc ℓ)
Pointed ℓ = TypeWithStr ℓ (λ x → x)

pt : ∀ {ℓ} (A∙ : Pointed ℓ) → typ A∙
pt = str

Pointed₀ = Pointed ℓ-zero

{- Pointed functions -}
_→∙_ : ∀{ℓ ℓ'} → (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
_→∙_ A B = Σ[ f ∈ (typ A → typ B) ] f (pt A) ≡ pt B

_→∙_∙ : ∀{ℓ ℓ'} → (A : Pointed ℓ) (B : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
A →∙ B ∙  = (A →∙ B) , (λ x → pt B) , refl

idfun∙ : ∀ {ℓ} (A : Pointed ℓ) → A →∙ A
idfun∙ A = (λ x → x) , refl

-- Pointed equivalences
_≃∙_ : (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
A ≃∙ B = Σ[ (f , p) ∈ A →∙ B ] isEquiv f

≃∙→≃ : {A : Pointed ℓ} {B : Pointed ℓ'}
       (f : A ≃∙ B)
       → typ A ≃ typ B
≃∙→≃ f = fst (fst f) , snd f

idEquiv∙ : (A : Pointed ℓ) → A ≃∙ A
idEquiv∙ (A , ⋆) =
  (idfun∙ (A , ⋆)) ,
  record { equiv-proof = λ a → p a }
    where
      module _ (a : A) where
        p : isContr (Σ[ a' ∈ A ] a' ≡ a)
        p = isContrRespectEquiv (Σ-cong-equiv-snd (λ a₁ → isoToEquiv (iso sym sym (λ _ → refl) λ _ → refl))) (isContrSingl a)

{- HIT allowing for pattern matching on pointed types -}
data Pointer {ℓ} (A : Pointed ℓ) : Type ℓ where
  pt₀ : Pointer A
  ⌊_⌋ : typ A → Pointer A
  id : ⌊ pt A ⌋ ≡ pt₀

IsoPointedPointer : ∀ {ℓ} {A : Pointed ℓ} → Iso (typ A) (Pointer A)
Iso.fun IsoPointedPointer = ⌊_⌋
Iso.inv (IsoPointedPointer {A = A}) pt₀ = pt A
Iso.inv IsoPointedPointer ⌊ x ⌋ = x
Iso.inv (IsoPointedPointer {A = A}) (id i) = pt A
Iso.rightInv IsoPointedPointer pt₀ = id
Iso.rightInv IsoPointedPointer ⌊ x ⌋ = refl
Iso.rightInv IsoPointedPointer (id i) j = id (i ∧ j)
Iso.leftInv IsoPointedPointer x = refl

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import Categories.Category using (Category; module Commutation)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)

-- Extra identities that hold only for symmetric monoidal categories.

module Categories.Category.Monoidal.Interchange.Symmetric
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (S : Symmetric M) where

open import Data.Product using (_,_)

import Categories.Category.Construction.Core C as Core
import Categories.Category.Monoidal.Braided.Properties as BraidedProps
open import Categories.Category.Monoidal.Interchange using (HasInterchange)
import Categories.Category.Monoidal.Interchange.Braided as BraidedInterchange
  using (module swapInner; swapInner-braiding)
import Categories.Category.Monoidal.Reasoning M as MonoidalReasoning
import Categories.Category.Monoidal.Utilities M as MonoidalUtilities
open import Categories.Category.Product using (_⁂_; assocˡ)
open import Categories.Functor using (_∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (_≃_; niHelper)
open import Categories.Morphism.IsoEquiv C using (to-unique)
open import Categories.Morphism.Reasoning C
  using (elim-center; pushˡ; pullʳ; cancelInner; switch-fromtoˡ)

open Category C using (Obj; _⇒_; _∘_; id; sym-assoc; ∘-resp-≈ʳ; module Equiv)
open Commutation C
open MonoidalReasoning
open MonoidalUtilities using (_⊗ᵢ_)
open Symmetric S renaming (associator to α; braided to B)
open BraidedInterchange B
open Core.Shorthands               -- for idᵢ, _∘ᵢ_, ...
open MonoidalUtilities.Shorthands  -- for λ⇒, ρ⇒, α⇒, ...
open BraidedProps.Shorthands B     -- for σ⇒, ...

private
  variable
    W W₁ W₂ X X₁ X₂ Y Y₁ Y₂ Z Z₁ Z₂ : Obj
    f g h i : X ⇒ Y

private
  i⇒ = swapInner.from
  i⇐ = swapInner.to

swapInner-commutative : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒
                          (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ]⟨
                           i⇒    ⇒⟨ (X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂) ⟩
                           i⇒
                        ≈ id
                        ⟩
swapInner-commutative = begin
    i⇒ ∘ i⇒                                                               ≈⟨ pullʳ (cancelInner α.isoʳ) ⟩
    α⇐ ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒  ≈˘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    α⇐ ∘ id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒        ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (∘-resp-≈ʳ sym-assoc ○ α[σ⊗1]α⁻¹.isoʳ) ⟩∘⟨refl ⟩
    α⇐ ∘ id ⊗₁ id ∘ α⇒                                                    ≈⟨ elim-center ⊗.identity ○ α.isoˡ ⟩
    id                                                                     ∎
  where module α[σ⊗1]α⁻¹ = _≅_ (α ∘ᵢ braided-iso ⊗ᵢ idᵢ ∘ᵢ α ⁻¹) using (isoʳ)

swapInner-iso : (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)
swapInner-iso = record
  { from = i⇒
  ; to   = i⇒
  ; iso  = record
    { isoˡ = swapInner-commutative
    ; isoʳ = swapInner-commutative
    }
  }

swapInner-selfInverse : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒
                          (X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂) ]⟨
                          i⇒
                        ≈ i⇐
                        ⟩
swapInner-selfInverse =
  to-unique (iso swapInner-iso) swapInner.iso Equiv.refl

swapInner-braiding′ : [ (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ⇒ (Y ⊗₀ W) ⊗₀ (Z ⊗₀ X) ]⟨
                        i⇒         ⇒⟨ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z) ⟩
                        σ⇒ ⊗₁ σ⇒
                      ≈ σ⇒         ⇒⟨ (Y ⊗₀ Z) ⊗₀ (W ⊗₀ X) ⟩
                        i⇒
                      ⟩
swapInner-braiding′ = switch-fromtoˡ swapInner-iso swapInner-braiding

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:
-- This code is based on https://github.com/agda/agda-stdlib/pull/800/files

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

module Experiment.Categories.Solver.Category.Reflection where

open import Data.Nat
open import Data.List
open import Data.Maybe using (Maybe; nothing; just; maybe)
open import Data.Product
open import Data.Bool
open import Function using (_⟨_⟩_)
open import Agda.Builtin.Reflection as Builtin

open import Categories.Category

open import Experiment.Categories.Solver.Category hiding (solve)

_==_ = Builtin.primQNameEquality
{-# INLINE _==_ #-}

_>>=_ = bindTC
{-# INLINE _>>=_ #-}

infixr 5 _⟨∷⟩_ _⟅∷⟆_
pattern _⟨∷⟩_ x xs = arg (arg-info visible relevant) x ∷ xs
pattern _⟅∷⟆_ x xs = arg (arg-info hidden  relevant) x ∷ xs

infixr 5 _⋯⟅∷⟆_
_⋯⟅∷⟆_ : ℕ → List (Arg Term) → List (Arg Term)
zero  ⋯⟅∷⟆ xs = xs
suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ i ⋯⟅∷⟆ xs
{-# INLINE _⋯⟅∷⟆_ #-}

getName : Term → Maybe Name
getName (con c args) = just c
getName (def f args) = just f
getName _            = nothing

getArgs : Term → Maybe (Term × Term)
getArgs (def _ xs) = go xs
  where
  go : List (Arg Term) → Maybe (Term × Term)
  go (x ⟨∷⟩ y ⟨∷⟩ []) = just (x , y)
  go (x ∷ xs)         = go xs
  go _                = nothing
getArgs _ = nothing

record CategoryNames : Set where
  field
    is-∘  : Name → Bool
    is-id : Name → Bool

findCategoryNames : Term → TC CategoryNames
findCategoryNames cat = do
  ∘-name ← normalise (quote Category._∘_ ⟨ def ⟩ 2 ⋯⟅∷⟆ cat ⟨∷⟩ [])
  id-name ← normalise (quote Category.id ⟨ def ⟩ 2 ⋯⟅∷⟆ cat ⟨∷⟩ [])
  returnTC record
    { is-∘  = buildMatcher (quote Category._∘_) (getName ∘-name)
    ; is-id = buildMatcher (quote Category.id) (getName id-name)
    }
  where
    buildMatcher : Name → Maybe Name → Name → Bool
    buildMatcher n = maybe (λ m x → n == x ∨ m == x) (n ==_)

:id′ : Term
:id′ = quote :id ⟨ con ⟩ []

∥_∥′ : Term → Term
∥_∥′ t = quote ∥_∥ ⟨ con ⟩ (t ⟨∷⟩ [])

module _ (names : CategoryNames) where
  open CategoryNames names

  :∘′ : List (Arg Term) → Term
  E′ : Term → Term

  :∘′ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _:∘_ ⟨ con ⟩ E′ x ⟨∷⟩ E′ y ⟨∷⟩ []
  :∘′ (x ∷ xs)          = :∘′ xs
  :∘′ _                 = unknown

  E′ t@(def n xs) = if is-∘ n
    then :∘′ xs
    else if is-id n
      then :id′
      else ∥ t ∥′
  E′ t@(con n xs) = if is-∘ n
    then :∘′ xs
    else if is-id n
     then :id′
     else ∥ t ∥′
  E′ t = ∥ t ∥′

constructSoln : Term → CategoryNames → Term → Term → Term
constructSoln cat names lhs rhs =
  quote Category.Equiv.trans ⟨ def ⟩ 2 ⋯⟅∷⟆ cat ⟨∷⟩
  (quote Category.Equiv.sym ⟨ def ⟩ 2 ⋯⟅∷⟆ cat ⟨∷⟩
     (quote ⟦e⟧N≈⟦e⟧ ⟨ def ⟩ 2 ⋯⟅∷⟆ cat ⟨∷⟩ E′ names lhs ⟨∷⟩ []) ⟨∷⟩ [])
  ⟨∷⟩
  (quote ⟦e⟧N≈⟦e⟧ ⟨ def ⟩ 2 ⋯⟅∷⟆ cat ⟨∷⟩ E′ names rhs ⟨∷⟩ []) ⟨∷⟩
  []

macro
  solve : Term → Term → TC _
  solve cat = λ hole → do
    hole′ ← inferType hole >>= normalise
    names ← findCategoryNames cat
    just (lhs , rhs) ← returnTC (getArgs hole′)
      where nothing → typeError (termErr hole′ ∷ [])
    let soln = constructSoln cat names lhs rhs
    unify hole soln

-- Example
module _ {o l e} (C : Category o l e) where
  open Category C
  _ : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} →
      (h ∘ id ∘ g) ∘ f ≈ id ∘ h ∘ (g ∘ f ∘ id)
  _ = solve C

  _ : ∀ {A} {f g h i j : A ⇒ A} →
      id ∘ (f ∘ id ∘ g) ∘ id ∘ (h ∘ id ∘ i) ∘ id ∘ j ≈ f ∘ (g ∘ h) ∘ (i ∘ j)
  _ = solve C


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Hilbert-style formalisation of closed syntax.
-- Nested terms.

module BasicIPC.Syntax.ClosedHilbert where

open import BasicIPC.Syntax.Common public

-- Derivations.

infix 3 ⊢_
data ⊢_ : Ty → Set where
  app   : ∀ {A B}   → ⊢ A ▻ B → ⊢ A → ⊢ B
  ci    : ∀ {A}     → ⊢ A ▻ A
  ck    : ∀ {A B}   → ⊢ A ▻ B ▻ A
  cs    : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  cpair : ∀ {A B}   → ⊢ A ▻ B ▻ A ∧ B
  cfst  : ∀ {A B}   → ⊢ A ∧ B ▻ A
  csnd  : ∀ {A B}   → ⊢ A ∧ B ▻ B
  unit  : ⊢ ⊤

infix 3 ⊢⋆_
⊢⋆_ : Cx Ty → Set
⊢⋆ ∅     = 𝟙
⊢⋆ Ξ , A = ⊢⋆ Ξ × ⊢ A

-- Cut and multicut.

cut : ∀ {A B} → ⊢ A → ⊢ A ▻ B → ⊢ B
cut t u = app u t

multicut : ∀ {Ξ A} → ⊢⋆ Ξ → ⊢ Ξ ▻⋯▻ A → ⊢ A
multicut {∅}     ∙        u = u
multicut {Ξ , B} (ts , t) u = app (multicut ts u) t

-- Contraction.

ccont : ∀ {A B} → ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = app (app cs cs) (app ck ci)

cont : ∀ {A B} → ⊢ A ▻ A ▻ B → ⊢ A ▻ B
cont t = app ccont t

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = app (app cs (app (app cs (app ck cs))
                         (app (app cs (app ck ck)) cs)))
            (app ck ck)

exch : ∀ {A B C} → ⊢ A ▻ B ▻ C → ⊢ B ▻ A ▻ C
exch t = app cexch t

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C} → ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = app (app cs (app ck cs)) ck

comp : ∀ {A B C} → ⊢ B ▻ C → ⊢ A ▻ B → ⊢ A ▻ C
comp t u = app (app ccomp t) u

-- Useful theorems in functional form.

pair : ∀ {A B} → ⊢ A → ⊢ B → ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B} → ⊢ A ∧ B → ⊢ A
fst t = app cfst t

snd : ∀ {A B} → ⊢ A ∧ B → ⊢ B
snd t = app csnd t

-- Convertibility.

data _⋙_ : ∀ {A} → ⊢ A → ⊢ A → Set where
  refl⋙     : ∀ {A} → {t : ⊢ A}
                     → t ⋙ t

  trans⋙    : ∀ {A} → {t t′ t″ : ⊢ A}
                     → t ⋙ t′ → t′ ⋙ t″
                     → t ⋙ t″

  sym⋙      : ∀ {A} → {t t′ : ⊢ A}
                     → t ⋙ t′
                     → t′ ⋙ t

  congapp⋙  : ∀ {A B} → {t t′ : ⊢ A ▻ B} → {u u′ : ⊢ A}
                       → t ⋙ t′ → u ⋙ u′
                       → app t u ⋙ app t′ u′

  congi⋙    : ∀ {A} → {t t′ : ⊢ A}
                     → t ⋙ t′
                     → app ci t ⋙ app ci t′

  congk⋙    : ∀ {A B} → {t t′ : ⊢ A} → {u u′ : ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app ck t) u ⋙ app (app ck t′) u′

  congs⋙    : ∀ {A B C} → {t t′ : ⊢ A ▻ B ▻ C} → {u u′ : ⊢ A ▻ B} → {v v′ : ⊢ A}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′
                         → app (app (app cs t) u) v ⋙ app (app (app cs t′) u′) v′

  congpair⋙ : ∀ {A B} → {t t′ : ⊢ A} → {u u′ : ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app cpair t) u ⋙ app (app cpair t′) u′

  congfst⋙  : ∀ {A B} → {t t′ : ⊢ A ∧ B}
                       → t ⋙ t′
                       → app cfst t ⋙ app cfst t′

  congsnd⋙  : ∀ {A B} → {t t′ : ⊢ A ∧ B}
                       → t ⋙ t′
                       → app csnd t ⋙ app csnd t′

  -- TODO: Verify this.
  beta▻ₖ⋙   : ∀ {A B} → {t : ⊢ A} → {u : ⊢ B}
                       → app (app ck t) u ⋙ t

  -- TODO: Verify this.
  beta▻ₛ⋙   : ∀ {A B C} → {t : ⊢ A ▻ B ▻ C} → {u : ⊢ A ▻ B} → {v : ⊢ A}
                         → app (app (app cs t) u) v ⋙ app (app t v) (app u v)

  -- TODO: What about eta for ▻?

  beta∧₁⋙   : ∀ {A B} → {t : ⊢ A} → {u : ⊢ B}
                       → app cfst (app (app cpair t) u) ⋙ t

  beta∧₂⋙   : ∀ {A B} → {t : ⊢ A} → {u : ⊢ B}
                       → app csnd (app (app cpair t) u) ⋙ u

  eta∧⋙     : ∀ {A B} → {t : ⊢ A ∧ B}
                       → t ⋙ app (app cpair (app cfst t)) (app csnd t)

  eta⊤⋙    : ∀ {t : ⊢ ⊤} → t ⋙ unit

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

open import level
open import algebra.semigroup
open import equality.core
open import sum

record IsMonoid {i} (M : Set i) : Set i where
  field
    instance sgrp : IsSemigroup M

  open IsSemigroup sgrp public
  field
    e : M
    lunit : (x : M) → e * x ≡ x
    runit : (x : M) → x * e ≡ x

Monoid : ∀ i → Set (lsuc i)
Monoid i = Σ (Set i) IsMonoid

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Nats.Add.Assoc where

open import Equality
open import Nats
open import Function

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

private

  a+/b+c/=/a+b/+c : ∀ a b c → a + b + c ≡ a + (b + c)
  a+/b+c/=/a+b/+c  zero   b c = refl
  a+/b+c/=/a+b/+c (suc a) b c = cong suc $ a+/b+c/=/a+b/+c a b c

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

nat-add-assoc : ∀ a b c → a + b + c ≡ a + (b + c)
nat-add-assoc = a+/b+c/=/a+b/+c


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle sha256 sha256-cr
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK

-- This module contains placeholders for the future analog of the
-- corresponding VotesOnce property.  Defining the implementation
-- obligation and proving that it is an invariant of an implementation
-- is a substantial undertaking.  We are working first on proving the
-- simpler VotesOnce property to settle down the structural aspects
-- before tackling the harder semantic issues.
module LibraBFT.Concrete.Properties.LockedRound where
 -- TODO-3: define the implementation obligation
 ImplObligation₁ : Set
 ImplObligation₁ = Unit

 -- Next, we prove that given the necessary obligations,
 module Proof
   (sps-corr : StepPeerState-AllValidParts)
   (Impl-LR1 : ImplObligation₁)
   where
  -- Any reachable state satisfies the LR rule for any epoch in the system.
  module _ {e}(st : SystemState e)(r : ReachableSystemState st)(eid : Fin e) where
   -- Bring in 'unwind', 'ext-unforgeability' and friends
   open Structural sps-corr

   -- Bring in IntSystemState
   open import LibraBFT.Concrete.System sps-corr
   open        PerState st r
   open        PerEpoch eid
   open import LibraBFT.Concrete.Obligations.LockedRound 𝓔 (ConcreteVoteEvidence 𝓔) as LR

   postulate  -- TODO-3: prove it
     lrr : LR.Type IntSystemState

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


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

data D : Set where
  @0 c : D

data P : D → Set where
  d : P c


text:
------------------------------------------------------------------------
-- Unary relations
------------------------------------------------------------------------

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

-- Adapted from the Agda standard library.

module Common.Relation.Unary where

infix 4 _∈_ _⊆_

------------------------------------------------------------------------
-- Unary relations
Pred : Set → Set₁
Pred A = A → Set

_∈_ : ∀ {A} → A → Pred A → Set
x ∈ P = P x

-- P ⊆ Q means that P is a subset of Q.
_⊆_ : ∀ {A} → Pred A → Pred A → Set
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Prelude
open import Nat

module contexts where
  -- variables are named with naturals in ė. therefore we represent
  -- contexts as functions from names for variables (nats) to possible
  -- bindings.
  _ctx : Set → Set
  A ctx = Nat → Maybe A

  -- convenient shorthand for the (unique up to fun. ext.) empty context
  ∅ : {A : Set} → A ctx
  ∅ _ = None

  infixr 100 ■_

  -- the domain of a context is those naturals which cuase it to emit some τ
  dom : {A : Set} → A ctx → Nat → Set
  dom {A} Γ x = Σ[ τ ∈ A ] (Γ x == Some τ)

  -- membership, or presence, in a context
  _∈_ : {A : Set} (p : Nat × A) → (Γ : A ctx) → Set
  (x , y) ∈ Γ = (Γ x) == Some y

  -- this packages up an appeal to context memebership into a form that
  -- lets us retain more information
  ctxindirect : {A : Set} (Γ : A ctx) (n : Nat) → Σ[ a ∈ A ] (Γ n == Some a) + (Γ n == None)
  ctxindirect Γ n with Γ n
  ctxindirect Γ n | Some x = Inl (x , refl)
  ctxindirect Γ n | None = Inr refl

  -- apartness for contexts
  _#_ : {A : Set} (n : Nat) → (Γ : A ctx) → Set
  x # Γ = (Γ x) == None

  -- disjoint contexts are those which share no mappings
  _##_ : {A : Set} → A ctx → A ctx → Set
  _##_ {A} Γ Γ'  = ((n : Nat) → dom Γ n → n # Γ') × ((n : Nat) → dom Γ' n → n # Γ)

  -- contexts give at most one binding for each variable
  ctxunicity : {A : Set} → {Γ : A ctx} {n : Nat} {t t' : A} →
               (n , t) ∈ Γ →
               (n , t') ∈ Γ →
               t == t'
  ctxunicity {n = n} p q with natEQ n n
  ctxunicity p q | Inl refl = someinj (! p · q)
  ctxunicity _ _ | Inr x≠x = abort (x≠x refl)

  -- warning: this is union, but it assumes WITHOUT CHECKING that the
  -- domains are disjoint. this is inherently asymmetric, and that's
  -- reflected throughout the development that follows
  _∪_ : {A : Set} → A ctx → A ctx → A ctx
  (C1 ∪ C2) x with C1 x
  (C1 ∪ C2) x | Some x₁ = Some x₁
  (C1 ∪ C2) x | None = C2 x

  -- the singleton context
  ■_ : {A : Set} → (Nat × A) → A ctx
  (■ (x , a)) y with natEQ x y
  (■ (x , a)) .x | Inl refl = Some a
  ... | Inr _ = None

  -- context extension
  -- Note that if x is not apart from Γ, this relies on the asymmetry
  -- of union to set Γ x = t.
  _,,_ : {A : Set} → A ctx → (Nat × A) → A ctx
  (Γ ,, (x , t)) = (■ (x , t)) ∪ Γ

  infixl 10 _,,_

  extend-empty : {A : Set} (x : Nat) (t : A) →
                 ∅ ,, (x , t) == ■ (x , t)
  extend-empty x t = funext eq
    where
      eq : (y : Nat) → (∅ ,, (x , t)) y == (■ (x , t)) y
      eq y with natEQ x y
      ... | Inl refl = refl
      ... | Inr x≠y = refl

  -- used below in proof of ∪ commutativity and associativity
  lem-dom-union1 : {A : Set} {C1 C2 : A ctx} {x : Nat} →
                   C1 ## C2 →
                   dom C1 x →
                   (C1 ∪ C2) x == C1 x
  lem-dom-union1 {A} {C1} {C2} {x} (d1 , d2) D with C1 x
  lem-dom-union1 (d1 , d2) D | Some x₁ = refl
  lem-dom-union1 (d1 , d2) D | None = abort (somenotnone (! (π2 D)))

  lem-dom-union2 : {A : Set} {C1 C2 : A ctx} {x : Nat} →
                   C1 ## C2 →
                   dom C1 x →
                   (C2 ∪ C1) x == C1 x
  lem-dom-union2 {A} {C1} {C2} {x} (d1 , d2) D with ctxindirect C2 x
  lem-dom-union2 {A} {C1} {C2} {x} (d1 , d2) D | Inl x₁ = abort (somenotnone (! (π2 x₁) · d1 x D ))
  lem-dom-union2 {A} {C1} {C2} {x} (d1 , d2) D | Inr x₁ with C2 x
  lem-dom-union2 (d1 , d2) D | Inr x₂ | Some x₁ = abort (somenotnone x₂)
  lem-dom-union2 (d1 , d2) D | Inr x₁ | None = refl

  -- if the contexts in question are disjoint, then union is commutative
  ∪comm : {A : Set} → (C1 C2 : A ctx) → C1 ## C2 → (C1 ∪ C2) == (C2 ∪ C1)
  ∪comm C1 C2 (d1 , d2)= funext guts
    where
      lem-apart-union1 : {A : Set} (C1 C2 : A ctx) (x : Nat) → x # C1 → x # C2 → x # (C1 ∪ C2)
      lem-apart-union1 C1 C2 x apt1 apt2 with C1 x
      lem-apart-union1 C1 C2 x apt1 apt2 | Some x₁ = abort (somenotnone apt1)
      lem-apart-union1 C1 C2 x apt1 apt2 | None = apt2

      lem-apart-union2 : {A : Set} (C1 C2 : A ctx) (x : Nat) → x # C1 → x # C2 → x # (C2 ∪ C1)
      lem-apart-union2 C1 C2 x apt1 apt2 with C2 x
      lem-apart-union2 C1 C2 x apt1 apt2 | Some x₁ = abort (somenotnone apt2)
      lem-apart-union2 C1 C2 x apt1 apt2 | None = apt1

      guts : (x : Nat) → (C1 ∪ C2) x == (C2 ∪ C1) x
      guts x with ctxindirect C1 x | ctxindirect C2 x
      guts x | Inl (π1 , π2) | Inl (π3 , π4) = abort (somenotnone (! π4 · d1 x (π1 , π2)))
      guts x | Inl x₁ | Inr x₂ = tr (λ qq → qq == (C2 ∪ C1) x) (! (lem-dom-union1 (d1 , d2) x₁)) (tr (λ qq → C1 x == qq) (! (lem-dom-union2 (d1 , d2) x₁)) refl)
      guts x | Inr x₁ | Inl x₂ = tr (λ qq → (C1 ∪ C2) x == qq) (! (lem-dom-union1 (d2 , d1) x₂)) (tr (λ qq → qq == C2 x) (! (lem-dom-union2 (d2 , d1) x₂)) refl)
      guts x | Inr x₁ | Inr x₂ = tr (λ qq → qq == (C2 ∪ C1) x) (! (lem-apart-union1 C1 C2 x x₁ x₂)) (tr (λ qq → None == qq) (! (lem-apart-union2 C1 C2 x x₁ x₂)) refl)

  -- an element in the left of a union is in the union
  x∈∪l : {A : Set} → (Γ Γ' : A ctx) (n : Nat) (x : A) → (n , x) ∈ Γ → (n , x) ∈ (Γ ∪ Γ')
  x∈∪l Γ Γ' n x xin with Γ n
  x∈∪l Γ Γ' n x₁ xin | Some x = xin
  x∈∪l Γ Γ' n x ()   | None

  -- an element in the right of a union is in the union as long as it is not in the left;
  -- this asymmetry reflects the asymmetry in the definition of union
  x∈∪r : {A : Set} → (Γ Γ' : A ctx) (n : Nat) (x : A) →
                             (n , x) ∈ Γ' →
                             n # Γ →
                             (n , x) ∈ (Γ ∪ Γ')
  x∈∪r Γ Γ' n x nx∈ apt with Γ n
  ... | None = nx∈

  -- an element is in the context formed with just itself
  x∈■ : {A : Set} (n : Nat) (a : A) → (n , a) ∈ (■ (n , a))
  x∈■ n a with natEQ n n
  x∈■ n a | Inl refl = refl
  x∈■ n a | Inr x = abort (x refl)

  -- if an index is in the domain of a singleton context, it's the only
  -- index in the context
  lem-dom-eq : {A : Set} {y : A} {n m : Nat} →
                                 dom (■ (m , y)) n →
                                 n == m
  lem-dom-eq {n = n} {m = m} (π1 , π2) with natEQ m n
  lem-dom-eq (π1 , π2) | Inl refl = refl
  lem-dom-eq (π1 , π2) | Inr x = abort (somenotnone (! π2))

  -- a singleton context formed with an index apart from a context is
  -- disjoint from that context
  lem-apart-sing-disj : {A : Set} {n : Nat} {a : A} {Γ : A ctx} →
                                     n # Γ →
                                     (■ (n , a)) ## Γ
  lem-apart-sing-disj {A} {n} {a} {Γ} apt = asd1 , asd2
    where
      asd1 : (n₁ : Nat) → dom (■ (n , a)) n₁ → n₁ # Γ
      asd1 m d with lem-dom-eq  d
      asd1 .n d | refl = apt

      asd2 : (n₁ : Nat) → dom Γ n₁ → n₁ # (■ (n , a))
      asd2 m (π1 , π2) with natEQ n m
      asd2 .n (π1 , π2) | Inl refl = abort (somenotnone (! π2 · apt ))
      asd2 m (π1 , π2) | Inr x = refl

  -- the only index of a singleton context is in its domain
  lem-domsingle : {A : Set} (p : Nat) (q : A) → dom (■ (p , q)) p
  lem-domsingle p q with natEQ p p
  lem-domsingle p q | Inl refl = q , refl
  lem-domsingle p q | Inr x₁ = abort (x₁ refl)

  -- dual of above
  lem-disj-sing-apart : {A : Set} {n : Nat} {a : A} {Γ : A ctx} →
                                     (■ (n , a)) ## Γ →
                                     n # Γ
  lem-disj-sing-apart {A} {n} {a} {Γ} (d1 , d2) = d1 n (lem-domsingle n a)

  -- the singleton context can only produce one non-none result
  lem-insingeq : {A : Set} {x x' : Nat} {τ τ' : A} →
                              (■ (x , τ)) x' == Some τ' →
                              τ == τ'
  lem-insingeq {A} {x} {x'} {τ} {τ'} eq with lem-dom-eq (τ' , eq)
  lem-insingeq {A} {x} {.x} {τ} {τ'} eq | refl with natEQ x x
  lem-insingeq refl | refl | Inl refl = refl
  lem-insingeq eq | refl | Inr x₁ = abort (somenotnone (! eq))

  -- if an index doesn't appear in a context, and the union of that context
  -- with a singleton does produce a result, it must have come from the singleton
  lem-apart-union-eq : {A : Set} {Γ : A ctx} {x x' : Nat} {τ τ' : A} →
                                    x' # Γ →
                                    (Γ ∪ ■ (x , τ)) x' == Some τ' →
                                    τ == τ'
  lem-apart-union-eq {A} {Γ} {x} {x'} {τ} {τ'} apart eq with Γ x'
  lem-apart-union-eq apart eq | Some x = abort (somenotnone apart)
  lem-apart-union-eq apart eq | None = lem-insingeq eq

  -- if an index not in a singleton context produces a result from that
  -- singleton unioned with another context, the result must have come from
  -- the other context
  lem-neq-union-eq : {A : Set} {Γ : A ctx} {x x' : Nat} {τ τ' : A} →
                                    x' ≠ x →
                                    (Γ ∪ ■ (x , τ)) x' == Some τ' →
                                    Γ x' == Some τ'
  lem-neq-union-eq {A} {Γ} {x} {x'} {τ} {τ'} neq eq with Γ x'
  lem-neq-union-eq neq eq | Some x = eq
  lem-neq-union-eq {A} {Γ} {x} {x'} {τ} {τ'} neq eq | None with natEQ x x'
  lem-neq-union-eq neq eq | None | Inl x₁ = abort ((flip neq) x₁)
  lem-neq-union-eq neq eq | None | Inr x₁ = abort (somenotnone (! eq))

  -- extending a context with a new index produces the result paired with
  -- that index.
  ctx-top : {A : Set} →
            (Γ : A ctx) (n : Nat) (a : A) →
            (n # Γ) →
            (n , a) ∈ (Γ ,, (n , a))
  ctx-top Γ n a apt with natEQ n n
  ... | Inl refl = refl
  ... | Inr n≠n = abort (n≠n refl)

  -- if a union of a singleton and a ctx produces no result, the argument
  -- index must be apart from the ctx and disequal to the index of the
  -- singleton
  lem-union-none : {A : Set} {Γ : A ctx} {a : A} {x x' : Nat}
                      → (Γ ∪ ■ (x , a)) x' == None
                      → (x ≠ x') × (x' # Γ)
  lem-union-none {A} {Γ} {a} {x} {x'} emp with ctxindirect Γ x'
  lem-union-none {A} {Γ} {a} {x} {x'} emp | Inl (π1 , π2) with Γ x'
  lem-union-none emp | Inl (π1 , π2) | Some x = abort (somenotnone emp)
  lem-union-none {A} {Γ} {a} {x} {x'} emp | Inl (π1 , π2) | None with natEQ x x'
  lem-union-none emp | Inl (π1 , π2) | None | Inl x₁ = abort (somenotnone (! π2))
  lem-union-none emp | Inl (π1 , π2) | None | Inr x₁ = x₁ , refl
  lem-union-none {A} {Γ} {a} {x} {x'} emp | Inr y with Γ x'
  lem-union-none emp | Inr y | Some x = abort (somenotnone emp)
  lem-union-none {A} {Γ} {a} {x} {x'} emp | Inr y | None with natEQ x x'
  lem-union-none emp | Inr y | None | Inl refl = abort (somenotnone emp)
  lem-union-none emp | Inr y | None | Inr x₁ = x₁ , refl

  --- lemmas building up to a proof of associativity of ∪
  ctxignore1 : {A : Set} (x : Nat) (C1 C2 : A ctx) → x # C1 → (C1 ∪ C2) x == C2 x
  ctxignore1 x C1 C2 apt with ctxindirect C1 x
  ctxignore1 x C1 C2 apt | Inl x₁ = abort (somenotnone (! (π2 x₁) · apt))
  ctxignore1 x C1 C2 apt | Inr x₁ with C1 x
  ctxignore1 x C1 C2 apt | Inr x₂ | Some x₁ = abort (somenotnone (x₂))
  ctxignore1 x C1 C2 apt | Inr x₁ | None = refl

  ctxignore2 : {A : Set} (x : Nat) (C1 C2 : A ctx) → x # C2 → (C1 ∪ C2) x == C1 x
  ctxignore2 x C1 C2 apt with ctxindirect C2 x
  ctxignore2 x C1 C2 apt | Inl x₁ = abort (somenotnone (! (π2 x₁) · apt))
  ctxignore2 x C1 C2 apt | Inr x₁ with C1 x
  ctxignore2 x C1 C2 apt | Inr x₂ | Some x₁ = refl
  ctxignore2 x C1 C2 apt | Inr x₁ | None = x₁

  ctxcollapse1 : {A : Set} → (C1 C2 C3 : A ctx) (x : Nat) →
               (x # C3) →
               (C2 ∪ C3) x == C2 x →
               (C1 ∪ (C2 ∪ C3)) x == (C1 ∪ C2) x
  ctxcollapse1 C1 C2 C3 x apt eq with C2 x
  ctxcollapse1 C1 C2 C3 x apt eq | Some x₁ with C1 x
  ctxcollapse1 C1 C2 C3 x apt eq | Some x₂ | Some x₁ = refl
  ctxcollapse1 C1 C2 C3 x apt eq | Some x₁ | None with C2 x
  ctxcollapse1 C1 C2 C3 x apt eq | Some x₂ | None | Some x₁ = refl
  ctxcollapse1 C1 C2 C3 x apt eq | Some x₁ | None | None = apt
  ctxcollapse1 C1 C2 C3 x apt eq | None with C1 x
  ctxcollapse1 C1 C2 C3 x apt eq | None | Some x₁ = refl
  ctxcollapse1 C1 C2 C3 x apt eq | None | None with C2 x
  ctxcollapse1 C1 C2 C3 x apt eq | None | None | Some x₁ = refl
  ctxcollapse1 C1 C2 C3 x apt eq | None | None | None = eq

  ctxcollapse2 : {A : Set} → (C1 C2 C3 : A ctx) (x : Nat) →
                 (x # C2) →
                 (C2 ∪ C3) x == C3 x →
                 (C1 ∪ (C2 ∪ C3)) x == (C1 ∪ C3) x
  ctxcollapse2 C1 C2 C3 x apt eq with C1 x
  ctxcollapse2 C1 C2 C3 x apt eq | Some x₁ = refl
  ctxcollapse2 C1 C2 C3 x apt eq | None with C2 x
  ctxcollapse2 C1 C2 C3 x apt eq | None | Some x₁ = eq
  ctxcollapse2 C1 C2 C3 x apt eq | None | None = refl

  ctxcollapse3 : {A : Set} → (C1 C2 C3 : A ctx) (x : Nat) →
                 (x # C2) →
                 ((C1 ∪ C2) ∪ C3) x == (C1 ∪ C3) x
  ctxcollapse3 C1 C2 C3 x apt with C1 x
  ctxcollapse3 C1 C2 C3 x apt | Some x₁ = refl
  ctxcollapse3 C1 C2 C3 x apt | None with C2 x
  ctxcollapse3 C1 C2 C3 x apt | None | Some x₁ = abort (somenotnone apt)
  ctxcollapse3 C1 C2 C3 x apt | None | None = refl

  ∪assoc : {A : Set} (C1 C2 C3 : A ctx) → (C2 ## C3) → (C1 ∪ C2) ∪ C3 == C1 ∪ (C2 ∪ C3)
  ∪assoc C1 C2 C3 (d1 , d2) = funext guts
    where
      case2 : (x : Nat) → x # C3 → dom C2 x → ((C1 ∪ C2) ∪ C3) x == (C1 ∪ (C2 ∪ C3)) x
      case2 x apt dom = (ctxignore2 x (C1 ∪ C2) C3 apt) ·
                        ! (ctxcollapse1 C1 C2 C3 x apt (lem-dom-union1 (d1 , d2) dom))

      case34 : (x : Nat) → x # C2 → ((C1 ∪ C2) ∪ C3) x == (C1 ∪ (C2 ∪ C3)) x
      case34 x apt = ctxcollapse3 C1 C2 C3 x apt ·
                        ! (ctxcollapse2 C1 C2 C3 x apt (ctxignore1 x C2 C3 apt))

      guts : (x : Nat) → ((C1 ∪ C2) ∪ C3) x == (C1 ∪ (C2 ∪ C3)) x
      guts x with ctxindirect C2 x | ctxindirect C3 x
      guts x | Inl (π1 , π2) | Inl (π3 , π4) = abort (somenotnone (! π4 · d1 x (π1 , π2)))
      guts x | Inl x₁ | Inr x₂ = case2 x x₂ x₁
      guts x | Inr x₁ | Inl x₂ = case34 x x₁
      guts x | Inr x₁ | Inr x₂ = case34 x x₁

  -- if x is apart from either part of a union, the answer comes from the other one
  lem-dom-union-apt1 : {A : Set} {Δ1 Δ2 : A ctx} {x : Nat} {y : A} → x # Δ1 → ((Δ1 ∪ Δ2) x == Some y) → (Δ2 x == Some y)
  lem-dom-union-apt1 {A} {Δ1} {Δ2} {x} {y} apt xin with Δ1 x
  lem-dom-union-apt1 apt xin | Some x₁ = abort (somenotnone apt)
  lem-dom-union-apt1 apt xin | None = xin

  lem-dom-union-apt2 : {A : Set} {Δ1 Δ2 : A ctx} {x : Nat} {y : A} → x # Δ2 → ((Δ1 ∪ Δ2) x == Some y) → (Δ1 x == Some y)
  lem-dom-union-apt2 {A} {Δ1} {Δ2} {x} {y} apt xin with Δ1 x
  lem-dom-union-apt2 apt xin | Some x₁ = xin
  lem-dom-union-apt2 apt xin | None = abort (somenotnone (! xin · apt))

  -- if x is in the union , it is in one of the parts
  lem-dom-union : {A : Set} {Δ1 Δ2 : A ctx} {x : Nat} {y : A} → (x , y) ∈ (Δ1 ∪ Δ2) → ((x , y) ∈ Δ1) + ((x , y) ∈ Δ2)
  lem-dom-union {Δ1 = Δ1} {Δ2 = Δ2} {x = x} ∈∪ with Δ1 x
  ... | Some x₁ = Inl ∈∪
  ... | None = Inr ∈∪

  update : {A : Set} (Γ : A ctx) (x : Nat) (τ1 τ2 : A) → Γ ,, (x , τ1) ,, (x , τ2) == Γ ,, (x , τ2)
  update Γ x τ1 τ2 = funext eq
    where
      eq : (y : Nat) → (Γ ,, (x , τ1) ,, (x , τ2)) y == (Γ ,, (x , τ2)) y
      eq y with natEQ x y
      ... | Inl refl = refl
      ... | Inr x≠y with natEQ x y
      ... | Inl refl = abort (x≠y refl)
      ... | Inr x≠y' = refl

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

open import Algebra

module Algebra.Construct.OrderedMonoid {ℓ} (monoid : Monoid ℓ) where

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

open Monoid monoid

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

_<_ : 𝑆 → 𝑆 → Type ℓ
x < y = ∃ z × (z ≢ ε) × (y ≡ x ∙ z)

_>_ = flip _<_
_≥_ = flip _≤_

≤-refl : Reflexive _≤_
≤-refl = ε , sym (∙ε _)

≤-trans : Transitive _≤_
≤-trans {x} {y} {z} (k₁ , y≡x∙k₁) (k₂ , z≡y∙k₂) = k₁ ∙ k₂ ,_ $
  z ≡⟨ z≡y∙k₂ ⟩
  y ∙ k₂ ≡⟨ cong (_∙ k₂) y≡x∙k₁ ⟩
  (x ∙ k₁) ∙ k₂ ≡⟨ assoc x k₁ k₂ ⟩
  x ∙ (k₁ ∙ k₂) ∎

ε≤x : ∀ x → ε ≤ x
ε≤x 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)

-- Trichotomous : Type _
-- Trichotomous = (x y : 𝑆) → Tri _<_ _≡_ _>_ x y

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import lib.Basics

module lib.types.Empty where

⊥ = Empty

⊥-elim : ∀ {i} {A : ⊥ → Type i} → ((x : ⊥) → A x)
⊥-elim = Empty-elim

Empty-rec : ∀ {i} {A : Type i} → (Empty → A)
Empty-rec = Empty-elim

⊥-rec : ∀ {i} {A : Type i} → (⊥ → A)
⊥-rec = Empty-rec

Empty-is-prop : is-prop Empty
Empty-is-prop = Empty-elim

⊥-is-prop : is-prop ⊥
⊥-is-prop = Empty-is-prop

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
module UnequalSorts where

data One  : Set  where one : One
data One' : Set1 where one' : One'

err : One
err = one'


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

open import Categories.Category
open import Categories.Functor.Bifunctor

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

private
  module C = Category C
  module D = Category D
  open D
  open HomReasoning
  variable
    A : Obj

open import Level

open import Categories.Functor hiding (id)
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation.Dinatural

open Functor F

record Wedge : Set (levelOfTerm F) where
  field
    E         : Obj
    dinatural : DinaturalTransformation (const E) F

  module dinatural = DinaturalTransformation dinatural

Wedge-∘ : (W : Wedge) → A ⇒ Wedge.E W → Wedge
Wedge-∘ {A = A} W f = record
  { E         = A
  ; dinatural = extranaturalʳ (λ X → dinatural.α X ∘ f)
                              (sym-assoc ○ ∘-resp-≈ˡ (extranatural-commʳ dinatural) ○ assoc)
  }
  where open Wedge W

record Wedge-Morphism (W₁ W₂ : Wedge) : Set (levelOfTerm F) where
  private
    module W₁ = Wedge W₁
    module W₂ = Wedge W₂
    open DinaturalTransformation
  field
    u : W₁.E ⇒ W₂.E
    commute : ∀ {C} → W₂.dinatural.α C ∘ u ≈ W₁.dinatural.α C

Wedge-id : ∀ {W} → Wedge-Morphism W W
Wedge-id {W} = record { u = D.id ; commute = D.identityʳ }

Wedge-Morphism-∘ : {A B C : Wedge} → Wedge-Morphism B C → Wedge-Morphism A B → Wedge-Morphism A C
Wedge-Morphism-∘ M N = record { u = u M ∘ u N ; commute =  sym-assoc ○ (∘-resp-≈ˡ (commute M) ○ commute N) }
  where
  open Wedge-Morphism
  open HomReasoning