text:
{-# OPTIONS --safe --experimental-lossy-unification #-}

module Cubical.Algebra.Group.EilenbergMacLane.Properties where

open import Cubical.Algebra.Group.EilenbergMacLane.Base renaming (elim to EM-elim)
open import Cubical.Algebra.Group.EilenbergMacLane.WedgeConnectivity
open import Cubical.Algebra.Group.EilenbergMacLane.GroupStructure
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup.TensorProduct
open import Cubical.Algebra.AbGroup.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Pointed.Homogeneous

open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Loopspace

open import Cubical.Functions.Morphism

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

open import Cubical.HITs.Truncation as Trunc
  renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1 renaming (rec to EMrec)
open import Cubical.HITs.Truncation
  renaming (elim to trElim ; rec to trRec ; rec2 to trRec2)
open import Cubical.HITs.Susp

private
  variable ℓ ℓ' ℓ'' : Level

isConnectedEM₁ : (G : Group ℓ) → isConnected 2 (EM₁ G)
isConnectedEM₁ G = ∣ embase ∣ , h
    where
      h : (y : hLevelTrunc 2 (EM₁ G)) → ∣ embase ∣ ≡ y
      h = trElim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y))
            (elimProp G (λ x → isOfHLevelTrunc 2 ∣ embase ∣ ∣ x ∣) refl)

module _ {G' : AbGroup ℓ} where
  private
    G = fst G'
    open AbGroupStr (snd G') renaming (_+_ to _+G_)

  isConnectedEM : (n : ℕ) → isConnected (suc n) (EM G' n)
  fst (isConnectedEM zero) = ∣ 0g ∣
  snd (isConnectedEM zero) y = isOfHLevelTrunc 1 _ _
  isConnectedEM (suc zero) = isConnectedEM₁ (AbGroup→Group G')
  fst (isConnectedEM (suc (suc n))) = ∣ 0ₖ _ ∣
  snd (isConnectedEM (suc (suc n))) =
    trElim (λ _ → isOfHLevelTruncPath)
      (trElim (λ _ → isOfHLevelSuc (3 + n) (isOfHLevelTruncPath {n = (3 + n)}))
        (raw-elim G'
          (suc n)
          (λ _ → isOfHLevelTrunc (3 + n) _ _)
          refl))

module _ (Ĝ : Group ℓ) where
  private
    G = fst Ĝ
  open GroupStr (snd Ĝ)

  emloop-id : emloop 1g ≡ refl
  emloop-id =
    emloop 1g                                 ≡⟨ rUnit (emloop 1g) ⟩
    emloop 1g ∙ refl                          ≡⟨ cong (emloop 1g ∙_) (rCancel (emloop 1g) ⁻¹) ⟩
    emloop 1g ∙ (emloop 1g ∙ (emloop 1g) ⁻¹)  ≡⟨ ∙assoc _ _ _ ⟩
    (emloop 1g ∙ emloop 1g) ∙ (emloop 1g) ⁻¹  ≡⟨ cong (_∙ emloop 1g ⁻¹)
                                                   ((emloop-comp Ĝ 1g 1g) ⁻¹) ⟩
    emloop (1g · 1g) ∙ (emloop 1g) ⁻¹         ≡⟨ cong (λ g → emloop {Group = Ĝ} g
                                                             ∙ (emloop 1g) ⁻¹)
                                                      (·IdR 1g) ⟩
    emloop 1g ∙ (emloop 1g) ⁻¹                ≡⟨ rCancel (emloop 1g) ⟩
    refl ∎

  emloop-inv : (g : G) → emloop (inv g) ≡ (emloop g) ⁻¹
  emloop-inv g =
    emloop (inv g)                              ≡⟨ rUnit (emloop (inv g)) ⟩
    emloop (inv g) ∙ refl                       ≡⟨ cong (emloop (inv g) ∙_)
                                                      (rCancel (emloop g) ⁻¹) ⟩
    emloop (inv g) ∙ (emloop g ∙ (emloop g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩
    (emloop (inv g) ∙ emloop g) ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ emloop g ⁻¹)
                                                      ((emloop-comp Ĝ (inv g) g) ⁻¹) ⟩
    emloop (inv g · g) ∙ (emloop g) ⁻¹          ≡⟨ cong (λ h → emloop {Group = Ĝ} h
                                                            ∙ (emloop g) ⁻¹)
                                                      (·InvL g) ⟩
    emloop 1g ∙ (emloop g) ⁻¹                 ≡⟨ cong (_∙ (emloop g) ⁻¹) emloop-id ⟩
    refl ∙ (emloop g) ⁻¹                      ≡⟨ (lUnit ((emloop g) ⁻¹)) ⁻¹ ⟩
    (emloop g) ⁻¹ ∎

  isGroupoidEM₁ : isGroupoid (EM₁ Ĝ)
  isGroupoidEM₁ = emsquash

  --------- Ω (EM₁ G) ≃ G ---------

  {- since we write composition in diagrammatic order,
     and function composition in the other order,
     we need right multiplication here -}
  rightEquiv : (g : G) → G ≃ G
  rightEquiv g = isoToEquiv isom
    where
    isom : Iso G G
    isom .Iso.fun = _· g
    isom .Iso.inv = _· inv g
    isom .Iso.rightInv h =
      (h · inv g) · g ≡⟨ (·Assoc h (inv g) g) ⁻¹ ⟩
        h · inv g · g ≡⟨ cong (h ·_) (·InvL g) ⟩
             h · 1g ≡⟨ ·IdR h ⟩ h ∎
    isom .Iso.leftInv h =
      (h · g) · inv g ≡⟨ (·Assoc h g (inv g)) ⁻¹ ⟩
        h · g · inv g ≡⟨ cong (h ·_) (·InvR g) ⟩
             h · 1g ≡⟨ ·IdR h ⟩ h ∎

  compRightEquiv : (g h : G)
    → compEquiv (rightEquiv g) (rightEquiv h) ≡ rightEquiv (g · h)
  compRightEquiv g h = equivEq (funExt (λ x → (·Assoc x g h) ⁻¹))

  CodesSet : EM₁ Ĝ → hSet ℓ
  CodesSet = EMrec Ĝ (isOfHLevelTypeOfHLevel 2) (G , is-set) RE REComp
    where
      RE : (g : G) → Path (hSet ℓ) (G , is-set) (G , is-set)
      RE g = Σ≡Prop (λ X → isPropIsOfHLevel {A = X} 2) (ua (rightEquiv g))

      lemma₁ : (g h : G) → Square
        (ua (rightEquiv g)) (ua (rightEquiv (g · h)))
        refl (ua (rightEquiv h))
      lemma₁ g h = invEq
                   (Square≃doubleComp (ua (rightEquiv g)) (ua (rightEquiv (g · h)))
                     refl (ua (rightEquiv h)))
                   (ua (rightEquiv g) ∙ ua (rightEquiv h)
                       ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩
                    ua (compEquiv (rightEquiv g) (rightEquiv h))
                       ≡⟨ cong ua (compRightEquiv g h) ⟩
                    ua (rightEquiv (g · h)) ∎)

      REComp : (g h : G) → Square (RE g) (RE (g · h)) refl (RE h)
      REComp g h = ΣSquareSet (λ _ → isProp→isSet isPropIsSet) (lemma₁ g h)
  Codes : EM₁ Ĝ → Type ℓ
  Codes x = CodesSet x .fst

  encode : (x : EM₁ Ĝ) → embase ≡ x → Codes x
  encode x p = subst Codes p 1g

  decode : (x : EM₁ Ĝ) → Codes x → embase ≡ x
  decode = elimSet Ĝ (λ x → isOfHLevelΠ 2 (λ c → isGroupoidEM₁ (embase) x))
    emloop λ g → ua→ λ h → emcomp h g

  decode-encode : (x : EM₁ Ĝ) (p : embase ≡ x) → decode x (encode x p) ≡ p
  decode-encode x p = J (λ y q → decode y (encode y q) ≡ q)
    (emloop (transport refl 1g) ≡⟨ cong emloop (transportRefl 1g) ⟩
     emloop 1g ≡⟨ emloop-id ⟩ refl ∎) p

  encode-decode : (x : EM₁ Ĝ) (c : Codes x) → encode x (decode x c) ≡ c
  encode-decode = elimProp Ĝ (λ x → isOfHLevelΠ 1 (λ c → CodesSet x .snd _ _))
    λ g → encode embase (decode embase g) ≡⟨ refl ⟩
          encode embase (emloop g) ≡⟨ refl ⟩
          transport (ua (rightEquiv g)) 1g ≡⟨ uaβ (rightEquiv g) 1g ⟩
          1g · g ≡⟨ ·IdL g ⟩
          g ∎

  ΩEM₁Iso : Iso (Path (EM₁ Ĝ) embase embase) G
  Iso.fun ΩEM₁Iso = encode embase
  Iso.inv ΩEM₁Iso = emloop
  Iso.rightInv ΩEM₁Iso = encode-decode embase
  Iso.leftInv ΩEM₁Iso = decode-encode embase

  ΩEM₁≡ : (Path (EM₁ Ĝ) embase embase) ≡ G
  ΩEM₁≡ = isoToPath ΩEM₁Iso

--------- Ω (EMₙ₊₁ G) ≃ EMₙ G ---------
module _ {G : AbGroup ℓ} where
  open AbGroupStr (snd G)
    renaming (_+_ to _+G_ ; -_ to -G_ ; +Assoc to +AssocG)

  CODE : (n : ℕ) → EM G (suc (suc n)) → TypeOfHLevel ℓ (3 + n)
  CODE n =
    trElim (λ _ → isOfHLevelTypeOfHLevel (3 + n))
      λ { north → EM G (suc n) , hLevelEM G (suc n)
        ; south → EM G (suc n) , hLevelEM G (suc n)
        ; (merid a i) → fib n a i}
    where
    fib : (n : ℕ) → (a : EM-raw G (suc n))
        → Path (TypeOfHLevel _ (3 + n))
                (EM G (suc n) , hLevelEM G (suc n))
                (EM G (suc n) , hLevelEM G (suc n))
    fib zero a = Σ≡Prop (λ _ → isPropIsOfHLevel 3)
                   (isoToPath (addIso 1 a))
    fib (suc n) a = Σ≡Prop (λ _ → isPropIsOfHLevel (4 + n))
                            (isoToPath (addIso (suc (suc n)) ∣ a ∣))

  decode' : (n : ℕ) (x : EM G (suc (suc n))) → CODE n x .fst → 0ₖ (suc (suc n)) ≡ x
  decode' n =
    trElim (λ _ → isOfHLevelΠ (4 + n)
            λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
           λ { north → f n
             ; south → g n
             ; (merid a i) → main a i}
     where
     f : (n : ℕ) → _
     f n = σ-EM' n

     g : (n : ℕ) → EM G (suc n) → ∣ ptEM-raw ∣ ≡ ∣ south ∣
     g n x = σ-EM' n x ∙ cong ∣_∣ₕ (merid ptEM-raw)

     lem₂ : (n : ℕ) (a x : _)
       → Path (Path (EM G (suc (suc n))) _ _)
               ((λ i → cong ∣_∣ₕ (σ-EM n x) i) ∙ sym (cong ∣_∣ₕ (σ-EM n a)) ∙ (λ i → ∣ merid a i ∣ₕ))
               (g n (EM-raw→EM G (suc n) x))
     lem₂ zero a x =
       cong (f zero x ∙_)
         (cong (_∙ cong ∣_∣ₕ (merid a)) (cong (cong ∣_∣ₕ) (symDistr (merid a) (sym (merid embase)))
                                     ∙ cong-∙ ∣_∣ₕ (merid embase) (sym (merid a)))
          ∙∙ sym (∙assoc _ _ _)
          ∙∙ cong (cong ∣_∣ₕ (merid embase) ∙_) (lCancel (cong ∣_∣ₕ (merid a)))
           ∙ sym (rUnit _))
     lem₂ (suc n) a x =
       cong (f (suc n) ∣ x ∣ ∙_)
         ((cong (_∙ cong ∣_∣ₕ (merid a)) (cong (cong ∣_∣ₕ) (symDistr (merid a) (sym (merid north)))
                                      ∙ cong-∙ ∣_∣ₕ (merid north) (sym (merid a)))
          ∙∙ sym (∙assoc _ _ _)
          ∙∙ cong (cong ∣_∣ₕ (merid north) ∙_) (lCancel (cong ∣_∣ₕ (merid a)))
           ∙ sym (rUnit _)))

     lem : (n : ℕ) (x a : EM-raw G (suc n))
             → f n (transport (sym (cong (λ x → CODE n x .fst) (cong ∣_∣ₕ (merid a))))
                    (EM-raw→EM G (suc n) x))
                ≡ cong ∣_∣ₕ (σ-EM n x) ∙ sym (cong ∣_∣ₕ (σ-EM n a))
     lem zero x a = (λ i → cong ∣_∣ₕ (merid (transportRefl x i -[ 1 ]ₖ a) ∙ sym (merid embase)))
                  ∙∙ σ-EM'-hom zero x (-ₖ a)
                  ∙∙ cong (f zero x ∙_) (σ-EM'-ₖ zero a)
     lem (suc n) x a =
          cong (f (suc n)) (λ i → transportRefl ∣ x ∣ i -[ 2 + n ]ₖ ∣ a ∣)
        ∙∙ σ-EM'-hom (suc n) ∣ x ∣ (-ₖ ∣ a ∣)
        ∙∙ cong (f (suc n) ∣ x ∣ ∙_) (σ-EM'-ₖ (suc n) ∣ a ∣)

     main : (a : _)
         → PathP (λ i → CODE n ∣ merid a i ∣ₕ .fst
                       → 0ₖ (suc (suc n)) ≡ ∣ merid a i ∣ₕ) (f n) (g n)
     main a =
       toPathP (funExt
         (EM-elim _ (λ _ → isOfHLevelPathP (2 + (suc n)) (isOfHLevelTrunc (4 + n) _ _) _ _)
           λ x →
            ((λ i → transp (λ j → Path (EM G (2 + n)) ∣ ptEM-raw ∣ ∣ merid a (i ∨ j) ∣)
                         i (compPath-filler (lem n x a i) (cong ∣_∣ₕ (merid a)) i) ))
         ∙∙ sym (∙assoc _ _ _)
         ∙∙ lem₂ n a x))

  encode' : (n : ℕ) (x : EM G (suc (suc n))) → 0ₖ (suc (suc n)) ≡ x → CODE n x .fst
  encode' n x p = subst (λ x → CODE n x .fst) p (0ₖ (suc n))

  decode'-encode' : (n : ℕ) (x : EM G (2 + n)) (p : 0ₖ (2 + n) ≡ x)
    → decode' n x (encode' n x p) ≡ p
  decode'-encode' zero x =
    J (λ x p → decode' 0 x (encode' 0 x p) ≡ p)
      (σ-EM'-0ₖ 0)
  decode'-encode' (suc n) x =
    J (λ x p → decode' (suc n) x (encode' (suc n) x p) ≡ p)
       (σ-EM'-0ₖ (suc n))

  encode'-decode' : (n : ℕ) (x : _)
    → encode' n (0ₖ (suc (suc n))) (decode' n (0ₖ (suc (suc n))) x) ≡ x
  encode'-decode' zero x =
        cong (encode' zero (0ₖ 2)) (cong-∙ ∣_∣ₕ (merid x) (sym (merid embase)))
     ∙∙ substComposite (λ x → CODE zero x .fst)
                              (cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) embase
     ∙∙ (cong (subst (λ x₁ → CODE zero x₁ .fst) (λ i → ∣ merid embase (~ i) ∣ₕ))
                                 (λ i → lUnitₖ 1 (transportRefl x i) i)
      ∙ (λ i → rUnitₖ 1 (transportRefl x i) i))
  encode'-decode' (suc n) =
    trElim (λ _ → isOfHLevelTruncPath {n = 4 + n})
      λ x → cong (encode' (suc n) (0ₖ (3 + n))) (cong-∙ ∣_∣ₕ (merid x) (sym (merid north)))
    ∙∙ substComposite (λ x → CODE (suc n) x .fst)
         (cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) (0ₖ (2 + n))
    ∙∙ cong (subst (λ x₁ → CODE (suc n) x₁ .fst) (λ i → ∣ merid ptEM-raw (~ i) ∣ₕ))
            (λ i → lUnitₖ (2 + n) (transportRefl ∣ x ∣ₕ i) i)
     ∙ (λ i → rUnitₖ (2 + n) (transportRefl ∣ x ∣ₕ i) i)

  Iso-EM-ΩEM+1 : (n : ℕ) → Iso (EM G n) (typ (Ω (EM∙ G (suc n))))
  Iso-EM-ΩEM+1 zero = invIso (ΩEM₁Iso (AbGroup→Group G))
  Iso.fun (Iso-EM-ΩEM+1 (suc zero)) = decode' 0 (0ₖ 2)
  Iso.inv (Iso-EM-ΩEM+1 (suc zero)) = encode' 0 (0ₖ 2)
  Iso.rightInv (Iso-EM-ΩEM+1 (suc zero)) = decode'-encode' 0 (0ₖ 2)
  Iso.leftInv (Iso-EM-ΩEM+1 (suc zero)) = encode'-decode' 0
  Iso.fun (Iso-EM-ΩEM+1 (suc (suc n))) = decode' (suc n) (0ₖ (3 + n))
  Iso.inv (Iso-EM-ΩEM+1 (suc (suc n))) = encode' (suc n) (0ₖ (3 + n))
  Iso.rightInv (Iso-EM-ΩEM+1 (suc (suc n))) = decode'-encode' (suc n) (0ₖ (3 + n))
  Iso.leftInv (Iso-EM-ΩEM+1 (suc (suc n))) = encode'-decode' (suc n)

  EM≃ΩEM+1 : (n : ℕ) → EM G n ≃ typ (Ω (EM∙ G (suc n)))
  EM≃ΩEM+1 n = isoToEquiv (Iso-EM-ΩEM+1 n)

  -- Some properties of the isomorphism
  EM→ΩEM+1 : (n : ℕ) → EM G n → typ (Ω (EM∙ G (suc n)))
  EM→ΩEM+1 n = Iso.fun (Iso-EM-ΩEM+1 n)

  ΩEM+1→EM : (n : ℕ) → typ (Ω (EM∙ G (suc n))) → EM G n
  ΩEM+1→EM n = Iso.inv (Iso-EM-ΩEM+1 n)

  EM→ΩEM+1-0ₖ : (n : ℕ) → EM→ΩEM+1 n (0ₖ n) ≡ refl
  EM→ΩEM+1-0ₖ zero = emloop-1g _
  EM→ΩEM+1-0ₖ (suc zero) = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw))
  EM→ΩEM+1-0ₖ (suc (suc n)) = cong (cong ∣_∣ₕ) (rCancel (merid ptEM-raw))

  EM→ΩEM+1-hom : (n : ℕ) (x y : EM G n)
    → EM→ΩEM+1 n (x +[ n ]ₖ y) ≡ EM→ΩEM+1 n x ∙ EM→ΩEM+1 n y
  EM→ΩEM+1-hom zero x y = emloop-comp _ x y
  EM→ΩEM+1-hom (suc zero) x y = σ-EM'-hom zero x y
  EM→ΩEM+1-hom (suc (suc n)) x y = σ-EM'-hom (suc n) x y

  ΩEM+1→EM-hom : (n : ℕ) → (p q : typ (Ω (EM∙ G (suc n))))
    → ΩEM+1→EM n (p ∙ q) ≡ (ΩEM+1→EM n p) +[ n ]ₖ (ΩEM+1→EM n q)
  ΩEM+1→EM-hom n =
    morphLemmas.isMorphInv (λ x y → x +[ n ]ₖ y) (_∙_) (EM→ΩEM+1 n)
      (EM→ΩEM+1-hom n) (ΩEM+1→EM n)
      (Iso.rightInv (Iso-EM-ΩEM+1 n)) (Iso.leftInv (Iso-EM-ΩEM+1 n))

  ΩEM+1→EM-refl : (n : ℕ) → ΩEM+1→EM n refl ≡ 0ₖ n
  ΩEM+1→EM-refl zero = transportRefl 0g
  ΩEM+1→EM-refl (suc zero) = refl
  ΩEM+1→EM-refl (suc (suc n)) = refl

  EM→ΩEM+1∙ : (n : ℕ) → EM∙ G n →∙ Ω (EM∙ G (suc n))
  EM→ΩEM+1∙ n .fst = EM→ΩEM+1 n
  EM→ΩEM+1∙ zero .snd = emloop-1g (AbGroup→Group G)
  EM→ΩEM+1∙ (suc zero) .snd = cong (cong ∣_∣ₕ) (rCancel (merid embase))
  EM→ΩEM+1∙ (suc (suc n)) .snd = cong (cong ∣_∣ₕ) (rCancel (merid north))

  EM≃ΩEM+1∙ : (n : ℕ) → EM∙ G n ≡ Ω (EM∙ G (suc n))
  EM≃ΩEM+1∙ n = ua∙ (EM≃ΩEM+1 n) (EM→ΩEM+1-0ₖ n)

  isHomogeneousEM : (n : ℕ) → isHomogeneous (EM∙ G n)
  isHomogeneousEM n x =
    ua∙ (isoToEquiv (addIso n x)) (lUnitₖ n x)

-- Some HLevel lemmas about function spaces (EM∙ G n →∙ EM∙ H m), mainly used for
-- the cup product
module _ where
  open AbGroupStr renaming (_+_ to comp)

  isContr-↓∙ : {G : AbGroup ℓ} {H : AbGroup ℓ'} (n : ℕ) → isContr (EM∙ G (suc n) →∙ EM∙ H n)
  fst (isContr-↓∙ {G = G} {H = H} zero) = (λ _ → 0g (snd H)) , refl
  snd (isContr-↓∙{G = G} {H = H} zero) (f , p) =
    Σ≡Prop (λ x → is-set (snd H) _ _)
      (funExt (raw-elim G 0 (λ _ → is-set (snd H) _ _) (sym p)))
  fst (isContr-↓∙ {G = G} {H = H} (suc n)) = (λ _ → 0ₖ (suc n)) , refl
  fst (snd (isContr-↓∙ {G = G} {H = H} (suc n)) f i) x =
    trElim {B = λ x → 0ₖ (suc n) ≡ fst f x}
    (λ _ → isOfHLevelPath (4 + n) (isOfHLevelSuc (3 + n) (hLevelEM H (suc n))) _ _)
    (raw-elim _ _ (λ _ → hLevelEM H (suc n) _ _) (sym (snd f)))
    x i
  snd (snd (isContr-↓∙ (suc n)) f i) j = snd f (~ i ∨ j)

  isContr-↓∙' : {G : AbGroup ℓ} {H : AbGroup ℓ'} (n : ℕ)
              → isContr ((EM-raw G (suc n) , ptEM-raw) →∙ EM∙ H n)
  isContr-↓∙' zero = isContr-↓∙ zero
  fst (isContr-↓∙' (suc n)) = (λ _ → 0ₖ (suc n)) , refl
  fst (snd (isContr-↓∙' {H = H} (suc n)) f i) x =
    raw-elim _  _ {A = λ x → 0ₖ (suc n) ≡ fst f x}
      (λ _ → hLevelEM H (suc n) _ _) (sym (snd f)) x i
  snd (snd (isContr-↓∙' (suc n)) f i) j = snd f (~ i ∨ j)

  isOfHLevel→∙EM : ∀ {ℓ} {A : Pointed ℓ} {G : AbGroup ℓ'} (n m : ℕ)
    → isOfHLevel (suc m) (A →∙ EM∙ G n)
    → isOfHLevel (suc (suc m)) (A →∙ EM∙ G (suc n))
  isOfHLevel→∙EM {A = A} {G = G} n m hlev = step₃
    where
    step₁ : isOfHLevel (suc m) (A →∙ Ω (EM∙ G (suc n)))
    step₁ =
      subst (isOfHLevel (suc m))
      (λ i → A →∙ ua∙ {A = Ω (EM∙ G (suc n))} {B = EM∙ G n}
      (invEquiv (EM≃ΩEM+1 n))
      (ΩEM+1→EM-refl n) (~ i)) hlev

    step₂ : isOfHLevel (suc m) (typ (Ω (A →∙ EM∙ G (suc n) ∙)))
    step₂ = isOfHLevelRetractFromIso (suc m) (invIso (invIso (ΩfunExtIso _ _))) step₁

    step₃ : isOfHLevel (suc (suc m)) (A →∙ EM∙ G (suc n))
    step₃ = isOfHLevelΩ→isOfHLevel m
      λ f → subst (λ x → isOfHLevel (suc m) (typ (Ω x)))
               (isHomogeneous→∙ (isHomogeneousEM (suc n)) f)
                step₂

  isOfHLevel↑∙ : {G : AbGroup ℓ} {H : AbGroup ℓ'}
            → ∀ n m → isOfHLevel (2 + n) (EM∙ G (suc m) →∙ EM∙ H (suc (n + m)))
  isOfHLevel↑∙ zero m = isOfHLevel→∙EM m 0 (isContr→isProp (isContr-↓∙ m))
  isOfHLevel↑∙ (suc n) m = isOfHLevel→∙EM (suc (n + m)) (suc n) (isOfHLevel↑∙ n m)

  isOfHLevel↑∙' : {G : AbGroup ℓ} {H : AbGroup ℓ'}
            → ∀ n m → isOfHLevel (2 + n) (EM-raw∙ G (suc m) →∙ EM∙ H (suc (n + m)))
  isOfHLevel↑∙' zero m = isOfHLevel→∙EM m 0 (isContr→isProp (isContr-↓∙' m))
  isOfHLevel↑∙' (suc n) m = isOfHLevel→∙EM (suc (n + m)) (suc n) (isOfHLevel↑∙' n m)

  →∙EMPath : ∀ {ℓ} {G : AbGroup ℓ} (A : Pointed ℓ') (n : ℕ)
           → Ω (A →∙ EM∙ G (suc n) ∙) ≡ (A →∙ EM∙ G n ∙)
  →∙EMPath {G = G} A n =
      ua∙ (isoToEquiv (ΩfunExtIso A (EM∙ G (suc n)))) refl
    ∙ (λ i → (A →∙ EM≃ΩEM+1∙ {G = G} n (~ i) ∙))

  private
    contr∙-lem : {G : AbGroup ℓ} {H : AbGroup ℓ'} {L : AbGroup ℓ''} (n m : ℕ)
      → isContr (EM∙ G (suc n) →∙ (EM∙ H (suc m) →∙ EM∙ L (suc (n + m)) ∙))
    fst (contr∙-lem n m) = (λ _ → (λ _ → 0ₖ _) , refl), refl
    snd (contr∙-lem {G = G} {H = H} {L = L} n m) (f , p) =
      →∙Homogeneous≡ (isHomogeneous→∙ (isHomogeneousEM _))
        (sym (funExt (help n f p)))
      where
      help : (n : ℕ) → (f : EM G (suc n) → EM∙ H (suc m) →∙ EM∙ L (suc (n + m)))
          → f (snd (EM∙ G (suc n))) ≡ snd (EM∙ H (suc m) →∙ EM∙ L (suc (n + m)) ∙)
          → (x : _) → (f x) ≡ ((λ _ → 0ₖ _) , refl)
      help zero f p =
        raw-elim G zero
          (λ _ → isOfHLevel↑∙ zero m _ _) p
      help (suc n) f p =
        trElim (λ _ → isOfHLevelPath (4 + n)
               (subst (λ x → isOfHLevel x (EM∙ H (suc m) →∙ EM∙ L (suc ((suc n) + m))))
                      (λ i → suc (suc (+-comm (suc n) 1 i)))
                      (isOfHLevelPlus' {n = 1} (3 + n) (isOfHLevel↑∙ (suc n) m))) _ _)
          (raw-elim G (suc n)
            (λ _ → isOfHLevel↑∙ (suc n) m _ _) p)

  isOfHLevel↑∙∙ : {G : AbGroup ℓ} {H : AbGroup ℓ'} {L : AbGroup ℓ''}
     → ∀ n m l → isOfHLevel (2 + l) (EM∙ G (suc n)
                                  →∙ (EM∙ H (suc m)
                                   →∙ EM∙ L (suc (suc (l + n + m))) ∙))
  isOfHLevel↑∙∙ {G = G} {H = H} {L = L} n m zero =
    isOfHLevelΩ→isOfHLevel 0 λ f
      → subst
          isProp (cong (λ x → typ (Ω x))
          (isHomogeneous→∙ (isHomogeneous→∙ (isHomogeneousEM _)) f))
          (isOfHLevelRetractFromIso 1 (ΩfunExtIso _ _) h)
    where
    h : isProp (EM∙ G (suc n)
             →∙ (Ω (EM∙ H (suc m)
              →∙ EM∙ L (suc (suc (n + m))) ∙)))
    h =
      subst isProp
        (λ i → EM∙ G (suc n)
            →∙ (→∙EMPath {G = L} (EM∙ H (suc m)) (suc (n + m)) (~ i)))
        (isContr→isProp (contr∙-lem n m))
  isOfHLevel↑∙∙ {G = G} {H = H} {L = L} n m (suc l) =
    isOfHLevelΩ→isOfHLevel (suc l)
      λ f →
      subst (isOfHLevel (2 + l))
          (cong (λ x → typ (Ω x))
          (isHomogeneous→∙ (isHomogeneous→∙ (isHomogeneousEM _)) f))
          (isOfHLevelRetractFromIso (2 + l) (ΩfunExtIso _ _) h)
    where
    h : isOfHLevel (2 + l)
         (EM∙ G (suc n)
           →∙ (Ω (EM∙ H (suc m)
             →∙ EM∙ L (suc (suc (suc (l + n + m)))) ∙)))
    h =
      subst (isOfHLevel (2 + l))
        (λ i → EM∙ G (suc n)
             →∙ →∙EMPath {G = L} (EM∙ H (suc m)) (suc (suc (l + n + m))) (~ i))
        (isOfHLevel↑∙∙ n m l)

-- A homomorphism φ : G → H of AbGroups induces a homomorphism
-- φ' : K(G,n) → K(H,n)
inducedFun-EM-raw : {G' : AbGroup ℓ} {H' : AbGroup ℓ'}
                     → AbGroupHom G' H'
                     → ∀ n
                     → EM-raw G' n → EM-raw H' n
inducedFun-EM-raw f =
  elim+2 (fst f)
    (EMrec _ emsquash embase
     (λ g → emloop (fst f g))
      λ g h → compPathR→PathP (sym
                (sym (lUnit _)
              ∙∙ cong (_∙ (sym (emloop (fst f h))))
                      (cong emloop (IsGroupHom.pres· (snd f) g h)
                          ∙ emloop-comp _ (fst f g) (fst f h))
              ∙∙ sym (∙assoc _ _ _)
              ∙∙ cong (emloop (fst f g) ∙_) (rCancel _)
              ∙∙ sym (rUnit _))))
    (λ n ind → λ { north → north
                  ; south → south
                  ; (merid a i) → merid (ind a) i} )

inducedFun-EM-rawIso : {G' : AbGroup ℓ} {H' : AbGroup ℓ'}
                     → AbGroupEquiv G' H'
                     → ∀ n → Iso (EM-raw G' n) (EM-raw H' n)
Iso.fun (inducedFun-EM-rawIso e n) = inducedFun-EM-raw (_ , (snd e)) n
Iso.inv (inducedFun-EM-rawIso e n) = inducedFun-EM-raw (_ , isGroupHomInv e) n
Iso.rightInv (inducedFun-EM-rawIso e n) = h n
  where
  h : (n : ℕ) → section (inducedFun-EM-raw (fst e .fst , snd e) n)
      (inducedFun-EM-raw (invEq (fst e) , isGroupHomInv e) n)
  h = elim+2
    (secEq (fst e))
    (elimSet _ (λ _ → emsquash _ _) refl
                       (λ g → compPathR→PathP
                          ((sym (cong₂ _∙_ (cong emloop (secEq (fst e) g)) (sym (lUnit _))
                               ∙ rCancel _)))))
    λ n p → λ { north → refl
               ; south → refl
               ; (merid a i) k → merid (p a k) i}
Iso.leftInv (inducedFun-EM-rawIso e n) = h n
  where
  h : (n : ℕ) → retract (Iso.fun (inducedFun-EM-rawIso e n))
                          (Iso.inv (inducedFun-EM-rawIso e n))
  h = elim+2
    (retEq (fst e))
    (elimSet _ (λ _ → emsquash _ _) refl
                       (λ g → compPathR→PathP
                          ((sym (cong₂ _∙_ (cong emloop (retEq (fst e) g)) (sym (lUnit _))
                               ∙ rCancel _)))))
    λ n p → λ { north → refl
               ; south → refl
               ; (merid a i) k → merid (p a k) i}

Iso→EMIso : {G : AbGroup ℓ} {H : AbGroup ℓ'}
  → AbGroupEquiv G H → ∀ n → Iso (EM G n) (EM H n)
Iso→EMIso is zero = inducedFun-EM-rawIso is zero
Iso→EMIso is (suc zero) = inducedFun-EM-rawIso is 1
Iso→EMIso is (suc (suc n)) = mapCompIso (inducedFun-EM-rawIso is (suc (suc n)))

EM⊗-commIso : {G : AbGroup ℓ} {H : AbGroup ℓ'}
  → ∀ n →  Iso (EM (G ⨂ H) n) (EM (H ⨂ G) n)
EM⊗-commIso {G = G} {H = H} = Iso→EMIso (GroupIso→GroupEquiv ⨂-commIso)

EM⊗-assocIso : {G : AbGroup ℓ} {H : AbGroup ℓ'} {L : AbGroup ℓ''}
  → ∀ n → Iso (EM (G ⨂ (H ⨂ L)) n) (EM ((G ⨂ H) ⨂ L) n)
EM⊗-assocIso = Iso→EMIso (GroupIso→GroupEquiv (GroupEquiv→GroupIso ⨂assoc))


text:
------------------------------------------------------------------------
-- Representation-independent results for non-dependent lenses
------------------------------------------------------------------------

import Equality.Path as P

module Lens.Non-dependent
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bij using (module _↔_)
open import Equality.Decision-procedures equality-with-J
open import Equivalence equality-with-J using (_≃_)
open import Erased.Cubical eq
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥)
open import Surjection equality-with-J using (_↠_)

private
  variable
    a b c c₁ c₂ c₃ l  : Level
    A B               : Type a
    Lens₁ Lens₂ Lens₃ : Type a → Type b → Type c

------------------------------------------------------------------------
-- Some existence results

-- There is, in general, no lens for the first projection from a
-- Σ-type, assuming that lenses with contractible domains have
-- contractible codomains.

no-first-projection-lens :
  (Lens : Type → Type → Type a) →
  @0 (∀ {A B} → Lens A B → Contractible A → Contractible B) →
  ¬ Lens (∃ λ (b : Bool) → b ≡ true) Bool
no-first-projection-lens _ contractible-to-contractible l =
  _↔_.to Erased-⊥↔⊥
    [                                $⟨ singleton-contractible _ ⟩
      Contractible (Singleton true)  ↝⟨ contractible-to-contractible l ⟩
      Contractible Bool              ↝⟨ mono₁ 0 ⟩
      Is-proposition Bool            ↝⟨ ¬-Bool-propositional ⟩□
      ⊥                              □
    ]

-- A variant of the previous result: If A is merely inhabited, and one
-- can "project" out a boolean from a value of type A, but this
-- boolean is necessarily true, then there is no lens corresponding to
-- this projection (if the get-set law holds).

no-singleton-projection-lens :
  {Lens : Type l}
  (get : Lens → A → Bool)
  (set : Lens → A → Bool → A)
  (get-set : ∀ l a b → get l (set l a b) ≡ b) →
  ∥ A ∥ →
  (bool : A → Bool) →
  (∀ x → bool x ≡ true) →
  ¬ ∃ λ (l : Lens) →
      ∀ x → get l x ≡ bool x
no-singleton-projection-lens
  get set get-set x bool is-true (l , get≡bool) =
  _↔_.to Erased-⊥↔⊥
    [ (flip (T.rec ⊥-propositional) x λ x →
       Bool.true≢false
         (true                   ≡⟨ sym $ is-true _ ⟩
          bool (set l x false)   ≡⟨ sym $ get≡bool _ ⟩
          get l (set l x false)  ≡⟨ get-set _ _ _ ⟩∎
          false                  ∎))
    ]

------------------------------------------------------------------------
-- Statements of preservation results, and some related lemmas

-- Lens-like things with getters and setters.

record Has-getter-and-setter
         (Lens : Type a → Type b → Type c) :
         Type (lsuc (a ⊔ b ⊔ c)) where
  field
    -- Getter.
    get : {A : Type a} {B : Type b} → Lens A B → A → B

    -- Typeter.
    set : {A : Type a} {B : Type b} → Lens A B → A → B → A

-- A statement of what it means for two lenses to have the same getter
-- and setter.

Same-getter-and-setter :
  {Lens₁ : Type a → Type b → Type c₁}
  {Lens₂ : Type a → Type b → Type c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  {A : Type a} {B : Type b} →
  Lens₁ A B → Lens₂ A B → Type (a ⊔ b)
Same-getter-and-setter ⦃ L₁ = L₁ ⦄ ⦃ L₂ = L₂ ⦄ l₁ l₂ =
  get L₁ l₁ ≡ get L₂ l₂ ×
  set L₁ l₁ ≡ set L₂ l₂
  where
  open Has-getter-and-setter

-- A statement of what it means for a function to preserve getters and
-- setters for all inputs.

Preserves-getters-and-setters-→ :
  {Lens₁ : Type a → Type b → Type c₁}
  {Lens₂ : Type a → Type b → Type c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  (A : Type a) (B : Type b) →
  (Lens₁ A B → Lens₂ A B) →
  Type (a ⊔ b ⊔ c₁)
Preserves-getters-and-setters-→ {Lens₁ = Lens₁} A B f =
  (l : Lens₁ A B) → Same-getter-and-setter (f l) l

-- A statement of what it means for a logical equivalence to preserve
-- getters and setters.

Preserves-getters-and-setters-⇔ :
  {Lens₁ : Type a → Type b → Type c₁}
  {Lens₂ : Type a → Type b → Type c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  (A : Type a) (B : Type b) →
  (Lens₁ A B ⇔ Lens₂ A B) →
  Type (a ⊔ b ⊔ c₁ ⊔ c₂)
Preserves-getters-and-setters-⇔ A B eq =
  Preserves-getters-and-setters-→ A B (_⇔_.to eq) ×
  Preserves-getters-and-setters-→ A B (_⇔_.from eq)

-- Composition preserves Preserves-getters-and-setters-→.

Preserves-getters-and-setters-→-∘ :
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  ⦃ L₃ : Has-getter-and-setter Lens₃ ⦄
  {f : Lens₂ A B → Lens₃ A B}
  {g : Lens₁ A B → Lens₂ A B} →
  Preserves-getters-and-setters-→ A B f →
  Preserves-getters-and-setters-→ A B g →
  Preserves-getters-and-setters-→ A B (f ∘ g)
Preserves-getters-and-setters-→-∘ p-f p-g _ =
    trans (proj₁ (p-f _)) (proj₁ (p-g _))
  , trans (proj₂ (p-f _)) (proj₂ (p-g _))

-- Composition preserves Preserves-getters-and-setters-⇔.

Preserves-getters-and-setters-⇔-∘ :
  {Lens₁ : Type a → Type b → Type c₁}
  {Lens₂ : Type a → Type b → Type c₂}
  {Lens₃ : Type a → Type b → Type c₃}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  ⦃ L₃ : Has-getter-and-setter Lens₃ ⦄
  {f : Lens₂ A B ⇔ Lens₃ A B}
  {g : Lens₁ A B ⇔ Lens₂ A B} →
  Preserves-getters-and-setters-⇔ A B f →
  Preserves-getters-and-setters-⇔ A B g →
  Preserves-getters-and-setters-⇔ A B (f F.∘ g)
Preserves-getters-and-setters-⇔-∘ p-f p-g =
    Preserves-getters-and-setters-→-∘ (proj₁ p-f) (proj₁ p-g)
  , Preserves-getters-and-setters-→-∘ (proj₂ p-g) (proj₂ p-f)

-- The function inverse preserves Preserves-getters-and-setters-⇔.

Preserves-getters-and-setters-⇔-inverse :
  {Lens₁ : Type a → Type b → Type c₁}
  {Lens₂ : Type a → Type b → Type c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  {f : Lens₁ A B ⇔ Lens₂ A B} →
  Preserves-getters-and-setters-⇔ A B f →
  Preserves-getters-and-setters-⇔ A B (inverse f)
Preserves-getters-and-setters-⇔-inverse = swap

-- If the forward direction of a split surjection preserves getters
-- and setters, then both directions do.

Preserves-getters-and-setters-→-↠-⇔ :
  {Lens₁ : Type a → Type b → Type c₁}
  {Lens₂ : Type a → Type b → Type c₂}
  ⦃ L₁ : Has-getter-and-setter Lens₁ ⦄
  ⦃ L₂ : Has-getter-and-setter Lens₂ ⦄
  (f : Lens₁ A B ↠ Lens₂ A B) →
  Preserves-getters-and-setters-→ A B (_↠_.to f) →
  Preserves-getters-and-setters-⇔ A B (_↠_.logical-equivalence f)
Preserves-getters-and-setters-→-↠-⇔ ⦃ L₁ = L₁ ⦄ ⦃ L₂ = L₂ ⦄ f p =
    p
  , λ l →
        (get L₁ (_↠_.from f l)             ≡⟨ sym $ proj₁ $ p (_↠_.from f l) ⟩
         get L₂ (_↠_.to f (_↠_.from f l))  ≡⟨ cong (get L₂) $ _↠_.right-inverse-of f _ ⟩∎
         get L₂ l                          ∎)
      , (set L₁ (_↠_.from f l)             ≡⟨ sym $ proj₂ $ p (_↠_.from f l) ⟩
         set L₂ (_↠_.to f (_↠_.from f l))  ≡⟨ cong (set L₂) $ _↠_.right-inverse-of f _ ⟩∎
         set L₂ l                          ∎)
  where
  open Has-getter-and-setter

ext: agda

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Concrete.System
open import LibraBFT.Impl.Consensus.Types

import      LibraBFT.Concrete.Properties.VotesOnce      as VO
import      LibraBFT.Concrete.Properties.PreferredRound as PR

open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})

-- This module collects in one place the obligations an
-- implementation must meet in order to enjoy the properties
-- proved in Abstract.Properties.

module LibraBFT.Concrete.Obligations where
  record ImplObligations : Set (ℓ+1 ℓ-RoundManager) where
    field
      -- Structural obligations:
      sps-cor : StepPeerState-AllValidParts

      -- Semantic obligations:
      --
      -- VotesOnce:
      vo₁ : VO.ImplObligation₁
      vo₂ : VO.ImplObligation₂

      -- PreferredRound:
      pr₁ : PR.ImplObligation₁

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
-- Andreas, 2018-05-11, issue #3051
-- Allow pattern synonyms in mutual blocks

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

id : ∀ {a} {A : Set a} → A → A
id x = x

_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         (B → C) → (A → B) → (A → C)
f ∘′ g = λ x → f (g x)

_×̇_ : ∀{A C : Set} {B : A → Set} {D : C → Set}
     (f : A → C) (g : ∀{a} → B a → D (f a)) → Σ A B → Σ C D
(f ×̇ g) (x , y) = f x , g y

mutual
  data Cxt : Set₁ where
    _▷_ : (Γ : Cxt) (A : C⦅ Γ ⦆ → Set) → Cxt

  C⦅_⦆ : Cxt → Set
  C⦅ Γ ▷ A ⦆ = Σ C⦅ Γ ⦆ A

mutual
  data _≤_ : (Δ Γ : Cxt) → Set₁ where
    id≤  : ∀{Γ} → Γ ≤ Γ
    weak : ∀{Γ Δ A} (τ : Δ ≤ Γ) → (Δ ▷ A) ≤ Γ
    lift' : ∀{Γ Δ A A'} (τ : Δ ≤ Γ) (p : A' ≡ (A ∘′ τ⦅ τ ⦆)) → (Δ ▷ A') ≤ (Γ ▷ A)

  pattern lift τ = lift' τ refl

  τ⦅_⦆ : ∀{Γ Δ} (τ : Δ ≤ Γ) → C⦅ Δ ⦆ → C⦅ Γ ⦆
  τ⦅ id≤ ⦆ = id
  τ⦅ weak τ ⦆ = τ⦅ τ ⦆ ∘′ fst
  τ⦅ lift τ ⦆ = τ⦅ τ ⦆ ×̇ id

-- Should pass.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import AC
open import Equivalence
open import Fiber
open import Functoriality
open import FunExt
open import GroupoidStructure
open import HIT.Interval
open import Homotopy
open import J
open import K
open import NTypes
open import NTypes.Contractible
open import NTypes.Coproduct
open import NTypes.Empty
open import NTypes.HedbergsTheorem
open import NTypes.Id
open import NTypes.Nat
open import NTypes.Negation
open import NTypes.Product
open import NTypes.Sigma
open import NTypes.Unit
open import NTypes.Universe
open import PathOperations
open import PathStructure.Coproduct
open import PathStructure.Empty
open import PathStructure.Id.Ap
open import PathStructure.Id.Tr
open import PathStructure.Nat
open import PathStructure.Product
open import PathStructure.Sigma
open import PathStructure.Unit
open import PathStructure.UnitNoEta
open import Sigma
open import Transport
open import Types
open import Univalence

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
-- Jesper, 2019-07-27. Cut down this example from a latent bug in
-- @antiUnify@, which was using @unAbs@ instead of @absBody@.

{-# OPTIONS --double-check #-}

open import Agda.Primitive

postulate
  I : Set
  T : ∀ {p} → Set (lsuc p) → Set (lsuc p)
  t : ∀ {p} → (B : Set (lsuc p)) → (I → I → Set) → B → T B

  x0 : I
  R0 : I → I → Set
  P0 : ∀ p → R0 x0 x0 → Set p
  d0 : R0 x0 x0

  C : ∀ {p} (X : Set) (x : (T (X → Set p))) → Set

  f : ∀ {p} (R : I → I → Set) (P : R x0 x0 → Set p)
    → {{_ : C (R x0 x0) (t (R x0 x0 → Set p) R P)}}
    → (d : R x0 x0) → P d

  instance
    iDP : ∀ {p} → C (R0 x0 x0) (t (R0 x0 x0 → Set p) R0 (P0 p))

fails : ∀ p → P0 p d0
fails p = f _ (P0 p) d0


text:
module UnknownNameInFixityDecl where

infix 40 _+_
infixr 60 _*_

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

open import lemmas-env

module lemmas-progress where
  typ-inhabitance-pres : ∀{Δ Σ' Γ E e τ} →
                           Δ , Σ' , Γ ⊢ E →
                           Δ , Σ' , Γ ⊢ e :: τ →
                           Σ[ r ∈ result ] (Δ , Σ' ⊢ r ·: τ)

  typ-inhabitance-pres Γ⊢E ta@(TAFix e-ta) = _ , (TAFix Γ⊢E ta)
  typ-inhabitance-pres Γ⊢E (TAVar x∈Γ)
    with env-all-Γ Γ⊢E x∈Γ
  ... | _ , x∈E , r-ta = _ , r-ta
  typ-inhabitance-pres Γ⊢E (TAApp _ f-ta arg-ta)
    with typ-inhabitance-pres Γ⊢E f-ta | typ-inhabitance-pres Γ⊢E arg-ta
  ... | _ , rf-ta | _ , rarg-ta = _ , TAApp rf-ta rarg-ta
  typ-inhabitance-pres Γ⊢E TAUnit = _ , TAUnit
  typ-inhabitance-pres Γ⊢E (TAPair _ ta1 ta2)
    with typ-inhabitance-pres Γ⊢E ta1 | typ-inhabitance-pres Γ⊢E ta2
  ... | _ , r-ta1 | _ , r-ta2 = _ , TAPair r-ta1 r-ta2
  typ-inhabitance-pres Γ⊢E (TAFst ta)
    with typ-inhabitance-pres Γ⊢E ta
  ... | _ , r-ta = _ , TAFst r-ta
  typ-inhabitance-pres Γ⊢E (TASnd ta)
    with typ-inhabitance-pres Γ⊢E ta
  ... | _ , r-ta = _ , TASnd r-ta
  typ-inhabitance-pres Γ⊢E (TACtor d∈Σ' c∈d e-ta)
    with typ-inhabitance-pres Γ⊢E e-ta
  ... | _ , r-ta = _ , TACtor d∈Σ' c∈d r-ta
  typ-inhabitance-pres Γ⊢E (TACase d∈Σ' e-ta h1 h2)
    with typ-inhabitance-pres Γ⊢E e-ta
  ... | _ , r-ta = _ , TACase d∈Σ' Γ⊢E r-ta h1 λ form →
                       let _ , _ , _ , h5 , h6 = h2 form in
                       _ , h5 , h6
  typ-inhabitance-pres Γ⊢E (TAHole u∈Δ) = _ , TAHole u∈Δ Γ⊢E
  typ-inhabitance-pres Γ⊢E (TAAsrt _ e-ta1 e-ta2) = _ , TAUnit

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Crypto.Crypto.Hash               as Hash
import      LibraBFT.Impl.OBM.Crypto                       as Crypto
import      LibraBFT.Impl.Types.OnChainConfig.ValidatorSet as ValidatorSet
import      LibraBFT.Impl.Types.ValidatorVerifier          as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Types.BlockInfo where

gENESIS_EPOCH   : Epoch
gENESIS_EPOCH   = {-Epoch-} 0

gENESIS_ROUND   : Round
gENESIS_ROUND   = {-Round-} 0

gENESIS_VERSION : Version
gENESIS_VERSION = Version∙new 0 0

empty : BlockInfo
empty = BlockInfo∙new
  gENESIS_EPOCH
  gENESIS_ROUND
  Hash.valueZero
  Hash.valueZero
  gENESIS_VERSION
  nothing

genesis : HashValue → ValidatorSet → Either ErrLog BlockInfo
genesis genesisStateRootHash validatorSet = do
  vv ← ValidatorVerifier.from-e-abs validatorSet
  pure $ BlockInfo∙new
    gENESIS_EPOCH
    gENESIS_ROUND
    Hash.valueZero
    genesisStateRootHash
    gENESIS_VERSION
  --gENESIS_TIMESTAMP_USECS
    (just (EpochState∙new {-Epoch-} 1 vv))

mockGenesis : Maybe ValidatorSet → Either ErrLog BlockInfo
mockGenesis
  = genesis
    (Crypto.obmHashVersion gENESIS_VERSION) -- OBM-LBFT-DIFF : Crypto.aCCUMULATOR_PLACEHOLDER_HASH
  ∘ fromMaybe ValidatorSet.empty

hasReconfiguration : BlockInfo → Bool
hasReconfiguration = is-just ∘ (_^∙ biNextEpochState)


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

   Copyright (c) 2020, 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
-- TODO-2: The following import should be eliminated and replaced
-- with the necessary module parameters (PK and MetaHonestPK)
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Abstract.Types.EpochConfig

-- This module brings in the base types used through libra
-- and those necessary for the abstract model.
module LibraBFT.Abstract.Types
  (UID    : Set)
  (NodeId : Set)
  (𝓔      : EpochConfig UID NodeId)
  where
  open EpochConfig 𝓔

  -- A member of an epoch is considered "honest" iff its public key is honest.
  Meta-Honest-Member : EpochConfig.Member 𝓔 → Set
  Meta-Honest-Member α = Meta-Honest-PK (getPubKey α)

  -- Naturally, if two witnesses that two authors belong
  -- in the epoch are the same, then the authors are also the same.
  --
  -- This proof is very Galois-like, because of the way we structured
  -- our partial isos. It's actually pretty nice! :)
  member≡⇒author≡ : ∀{α β}
                  → (authorα : Is-just (isMember? α))
                  → (authorβ : Is-just (isMember? β))
                  → to-witness authorα ≡ to-witness authorβ
                  → α ≡ β
  member≡⇒author≡ {α} {β} a b prf
    with isMember? α | inspect isMember? α
  ...| nothing | [ _ ] = ⊥-elim (maybe-any-⊥ a)
  member≡⇒author≡ {α} {β} (just _) b prf
     | just ra | [ RA ]
    with isMember? β | inspect isMember? β
  ...| nothing | [ _ ] = ⊥-elim (maybe-any-⊥ b)
  member≡⇒author≡ {α} {β} (just _) (just _) prf
     | just ra | [ RA ]
     | just rb | [ RB ]
     = trans (sym (author-nodeid-id RA))
             (trans (cong toNodeId prf)
                    (author-nodeid-id RB))


text:
import Categories.2-Category
import Categories.2-Functor
import Categories.Adjoint
import Categories.Adjoint.Construction.EilenbergMoore
import Categories.Adjoint.Construction.Kleisli
import Categories.Adjoint.Equivalence
import Categories.Adjoint.Instance.0-Truncation
import Categories.Adjoint.Instance.01-Truncation
import Categories.Adjoint.Instance.Core
import Categories.Adjoint.Instance.Discrete
import Categories.Adjoint.Instance.PosetCore
import Categories.Adjoint.Instance.StrictCore
import Categories.Adjoint.Mate
import Categories.Adjoint.Properties
import Categories.Adjoint.RAPL
import Categories.Bicategory
import Categories.Bicategory.Bigroupoid
import Categories.Bicategory.Construction.1-Category
import Categories.Bicategory.Instance.Cats
import Categories.Bicategory.Instance.EnrichedCats
import Categories.Category
import Categories.Category.BicartesianClosed
import Categories.Category.Cartesian
import Categories.Category.Cartesian.Properties
import Categories.Category.CartesianClosed
import Categories.Category.CartesianClosed.Canonical
import Categories.Category.CartesianClosed.Locally
import Categories.Category.CartesianClosed.Locally.Properties
import Categories.Category.Closed
import Categories.Category.Cocartesian
import Categories.Category.Cocomplete
import Categories.Category.Cocomplete.Finitely
import Categories.Category.Complete
import Categories.Category.Complete.Finitely
import Categories.Category.Construction.0-Groupoid
import Categories.Category.Construction.Arrow
import Categories.Category.Construction.Cocones
import Categories.Category.Construction.Comma
import Categories.Category.Construction.Cones
import Categories.Category.Construction.Coproduct
import Categories.Category.Construction.Core
import Categories.Category.Construction.EilenbergMoore
import Categories.Category.Construction.Elements
import Categories.Category.Construction.EnrichedFunctors
import Categories.Category.Construction.F-Algebras
import Categories.Category.Construction.Fin
import Categories.Category.Construction.Functors
import Categories.Category.Construction.Graphs
import Categories.Category.Construction.Grothendieck
import Categories.Category.Construction.Kleisli
import Categories.Category.Construction.Path
import Categories.Category.Construction.Presheaves
import Categories.Category.Construction.Properties.Comma
import Categories.Category.Construction.Pullbacks
import Categories.Category.Construction.Thin
import Categories.Category.Core
import Categories.Category.Discrete
import Categories.Category.Equivalence
import Categories.Category.Finite
import Categories.Category.Groupoid
import Categories.Category.Groupoid.Properties
import Categories.Category.Indiscrete
import Categories.Category.Instance.Cats
import Categories.Category.Instance.EmptySet
import Categories.Category.Instance.FamilyOfSets
import Categories.Category.Instance.Globe
import Categories.Category.Instance.Groupoids
import Categories.Category.Instance.One
import Categories.Category.Instance.PointedSets
import Categories.Category.Instance.Posets
import Categories.Category.Instance.Properties.Cats
import Categories.Category.Instance.Properties.Posets
import Categories.Category.Instance.Properties.Setoids
import Categories.Category.Instance.Setoids
import Categories.Category.Instance.Sets
import Categories.Category.Instance.Simplex
import Categories.Category.Instance.SimplicialSet
import Categories.Category.Instance.SingletonSet
import Categories.Category.Instance.Span
import Categories.Category.Instance.StrictCats
import Categories.Category.Instance.StrictGroupoids
import Categories.Category.Instance.Zero
import Categories.Category.Monoidal
import Categories.Category.Monoidal.Braided
import Categories.Category.Monoidal.Braided.Properties
import Categories.Category.Monoidal.Closed
import Categories.Category.Monoidal.Closed.IsClosed
import Categories.Category.Monoidal.Closed.IsClosed.Diagonal
import Categories.Category.Monoidal.Closed.IsClosed.Dinatural
import Categories.Category.Monoidal.Closed.IsClosed.Identity
import Categories.Category.Monoidal.Closed.IsClosed.L
import Categories.Category.Monoidal.Closed.IsClosed.Pentagon
import Categories.Category.Monoidal.Construction.Minus2
import Categories.Category.Monoidal.Core
import Categories.Category.Monoidal.Instance.Cats
import Categories.Category.Monoidal.Instance.One
import Categories.Category.Monoidal.Instance.Setoids
import Categories.Category.Monoidal.Instance.Sets
import Categories.Category.Monoidal.Instance.StrictCats
import Categories.Category.Monoidal.Properties
import Categories.Category.Monoidal.Reasoning
import Categories.Category.Monoidal.Symmetric
import Categories.Category.Monoidal.Traced
import Categories.Category.Monoidal.Utilities
import Categories.Category.Product
import Categories.Category.Product.Properties
import Categories.Category.RigCategory
import Categories.Category.SetoidDiscrete
import Categories.Category.Site
import Categories.Category.Slice
import Categories.Category.Slice.Properties
import Categories.Category.SubCategory
import Categories.Category.Topos
import Categories.Category.WithFamilies
import Categories.Comonad
import Categories.Diagram.Cocone
import Categories.Diagram.Cocone.Properties
import Categories.Diagram.Coend
import Categories.Diagram.Coequalizer
import Categories.Diagram.Coequalizer.Properties
import Categories.Diagram.Colimit
import Categories.Diagram.Colimit.DualProperties
import Categories.Diagram.Colimit.Lan
import Categories.Diagram.Colimit.Properties
import Categories.Diagram.Cone
import Categories.Diagram.Cone.Properties
import Categories.Diagram.Duality
import Categories.Diagram.End
import Categories.Diagram.End.Properties
import Categories.Diagram.Equalizer
import Categories.Diagram.Finite
import Categories.Diagram.Limit
import Categories.Diagram.Limit.Properties
import Categories.Diagram.Limit.Ran
import Categories.Diagram.Pullback
import Categories.Diagram.Pullback.Limit
import Categories.Diagram.Pullback.Properties
import Categories.Diagram.Pushout
import Categories.Diagram.Pushout.Properties
import Categories.Diagram.SubobjectClassifier
import Categories.Enriched.Category
import Categories.Enriched.Functor
import Categories.Enriched.NaturalTransformation
import Categories.Enriched.NaturalTransformation.NaturalIsomorphism
import Categories.Enriched.Over.One
import Categories.Functor
import Categories.Functor.Algebra
import Categories.Functor.Bifunctor
import Categories.Functor.Bifunctor.Properties
import Categories.Functor.Coalgebra
import Categories.Functor.Cocontinuous
import Categories.Functor.Construction.Constant
import Categories.Functor.Construction.Diagonal
import Categories.Functor.Construction.LiftSetoids
import Categories.Functor.Construction.Limit
import Categories.Functor.Construction.Zero
import Categories.Functor.Continuous
import Categories.Functor.Core
import Categories.Functor.Equivalence
import Categories.Functor.Fibration
import Categories.Functor.Groupoid
import Categories.Functor.Hom
import Categories.Functor.Instance.0-Truncation
import Categories.Functor.Instance.01-Truncation
import Categories.Functor.Instance.Core
import Categories.Functor.Instance.Discrete
import Categories.Functor.Instance.SetoidDiscrete
import Categories.Functor.Instance.StrictCore
import Categories.Functor.Monoidal
import Categories.Functor.Power
import Categories.Functor.Power.Functorial
import Categories.Functor.Power.NaturalTransformation
import Categories.Functor.Presheaf
import Categories.Functor.Profunctor
import Categories.Functor.Properties
import Categories.Functor.Representable
import Categories.Functor.Slice
import Categories.GlobularSet
import Categories.Kan
import Categories.Kan.Duality
import Categories.Minus2-Category
import Categories.Minus2-Category.Construction.Indiscrete
import Categories.Minus2-Category.Instance.One
import Categories.Minus2-Category.Properties
import Categories.Monad
import Categories.Monad.Duality
import Categories.Monad.Idempotent
import Categories.Monad.Strong
import Categories.Morphism
import Categories.Morphism.Cartesian
import Categories.Morphism.Duality
import Categories.Morphism.HeterogeneousIdentity
import Categories.Morphism.HeterogeneousIdentity.Properties
import Categories.Morphism.IsoEquiv
import Categories.Morphism.Isomorphism
import Categories.Morphism.Properties
import Categories.Morphism.Reasoning
import Categories.Morphism.Reasoning.Core
import Categories.Morphism.Reasoning.Iso
import Categories.Morphism.Universal
import Categories.NaturalTransformation
import Categories.NaturalTransformation.Core
import Categories.NaturalTransformation.Dinatural
import Categories.NaturalTransformation.Equivalence
import Categories.NaturalTransformation.Hom
import Categories.NaturalTransformation.NaturalIsomorphism
import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence
import Categories.NaturalTransformation.NaturalIsomorphism.Functors
import Categories.NaturalTransformation.NaturalIsomorphism.Properties
import Categories.NaturalTransformation.Properties
import Categories.Object.Coproduct
import Categories.Object.Duality
import Categories.Object.Exponential
import Categories.Object.Initial
import Categories.Object.Product
import Categories.Object.Product.Construction
import Categories.Object.Product.Core
import Categories.Object.Product.Morphisms
import Categories.Object.Terminal
import Categories.Object.Zero
import Categories.Pseudofunctor
import Categories.Pseudofunctor.Instance.EnrichedUnderlying
import Categories.Utils.EqReasoning
import Categories.Utils.Product
import Categories.Yoneda
import Categories.Yoneda.Properties
import Relation.Binary.Construct.Symmetrize

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module Membership where

open import Data.Sum
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Data.List.Any as Any
open Any.Membership-≡

-- _∈_

∈-++-pos : ∀ {A : Set} {x : A} xs ys → x ∈ xs ++ ys
           → (x ∈ xs) ⊎ (x ∈ ys)
∈-++-pos [] ys x∈ = inj₂ x∈
∈-++-pos (x ∷ xs) ys (here refl) = inj₁ (here refl)
∈-++-pos (x ∷ xs) ys (there x∈) with ∈-++-pos xs ys x∈
... | inj₁ x∈xs = inj₁ (there x∈xs)
... | inj₂ x∈ys = inj₂ x∈ys

∈-++-r : ∀ {A : Set} {x : A} xs {ys}
           → x ∈ ys → x ∈ (xs ++ ys)
∈-++-r [] x∈ = x∈
∈-++-r (y ∷ xs) x∈ = there (∈-++-r xs x∈)

∈-++-l : ∀ {A : Set} {x : A} {xs} ys
           → x ∈ xs → x ∈ (xs ++ ys)
∈-++-l ys (here refl) = here refl
∈-++-l ys (there x∈) = there (∈-++-l ys x∈)

∈-++-weaken : ∀ {A : Set} {x : A} xs ys zs
              → x ∈ (xs ++ zs) → x ∈ (xs ++ ys ++ zs)
∈-++-weaken [] ys zs x∈ = ∈-++-r ys x∈
∈-++-weaken (x ∷ xs) ys zs (here refl) = here refl
∈-++-weaken (_ ∷ xs) ys zs (there x∈) = there (∈-++-weaken xs ys zs x∈)

-- _∉_

∉-++-l : ∀ {A : Set} {x : A} xs ys → x ∉ xs ++ ys → x ∉ xs
∉-++-l ._ ys x∉xs++ys (here eq) = x∉xs++ys (here eq)
∉-++-l .(x' ∷ xs) ys x∉xs++ys (there {x'} {xs} pxs) =
  ∉-++-l xs ys (λ p → x∉xs++ys (there p)) pxs

∉-++-r : ∀ {A : Set} {x : A} xs ys → x ∉ xs ++ ys → x ∉ ys
∉-++-r [] ys x∉xs++ys x∈ys = x∉xs++ys x∈ys
∉-++-r (x' ∷ xs) ys x∉xs++ys x∈ys = ∉-++-r xs ys (λ p → x∉xs++ys (there p)) x∈ys

postulate
  ∉-∷ : ∀ {A : Set} {y x : A} {xs}
        → ¬ (y ≡ x) → y ∉ xs → y ∉ (x ∷ xs)

∉-++-join : ∀ {A : Set} {x : A}
            → ∀ xs ys → x ∉ xs → x ∉ ys → x ∉ xs ++ ys
∉-++-join [] ys x∉xs x∉ys x∈ys = x∉ys x∈ys
∉-++-join (_ ∷ xs) ys x∉xs x∉ys (here refl) = x∉xs (here refl)
∉-++-join (_ ∷ xs) ys x∉xxs x∉ys (there pxs) = ∉-++-join xs ys (λ x∉xs → x∉xxs (there x∉xs)) x∉ys pxs

∉-++-weaken : ∀ {A : Set} {x : A} xs ys zs
              → x ∉ (xs ++ ys ++ zs) → x ∉ (xs ++ zs)
∉-++-weaken xs ys zs x∉xyz x∈xz = x∉xyz (∈-++-weaken xs ys zs x∈xz)

∉-∷-hd : ∀ {A : Set} {x y : A} xs → x ∉ (y ∷ xs) → ¬ (x ≡ y)
∉-∷-hd {x} {._} xs x∉ refl = x∉ (here refl)

∉-∷-tl : ∀ {A : Set} {x y : A} xs → x ∉ (y ∷ xs) → x ∉ xs
∉-∷-tl {x} {y} xs x∉ x∈ = x∉ (there x∈)

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


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

open import hott.loop.core public
open import hott.loop.properties public
open import hott.loop.level public
open import hott.loop.sum public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import Cubical.Foundations.Prelude

open import Cubical.HITs.SetQuotients.Base

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

rel : (ℕ × ℕ) → (ℕ × ℕ) → Type₀
rel (a₀ , b₀) (a₁ , b₁) = x ≡ y
  where
    x = a₀ + b₁
    y = a₁ + b₀

ℤ = (ℕ × ℕ) / rel

open import Cubical.Data.Nat.Literals public

instance
  fromNatDiffInt : HasFromNat ℤ
  fromNatDiffInt = record { Constraint = λ _ → Unit ; fromNat = λ n → [ n , 0 ] }

instance
  fromNegDiffInt : HasFromNeg ℤ
  fromNegDiffInt = record { Constraint = λ _ → Unit ; fromNeg = λ n → [ 0 , n ] }

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: mchristianl/cubical


text:
module Structure.Category.Functor.Contravariant where

open import Logic.Predicate
import      Lvl
open import Structure.Category.Functor
open import Structure.Category.Dual
open import Structure.Category
open import Structure.Setoid
open import Type

private variable ℓ ℓₒ ℓₘ ℓₗₒ ℓₗₘ ℓᵣₒ ℓᵣₘ ℓₑ ℓₗₑ ℓᵣₑ : Lvl.Level
private variable Obj Objₗ Objᵣ : Type{ℓ}
private variable Morphism Morphismₗ Morphismᵣ : Objₗ → Objᵣ → Type{ℓ}

module _
  ⦃ morphism-equivₗ : ∀{x y : Objₗ} → Equiv{ℓₗₑ}(Morphismₗ x y) ⦄
  ⦃ morphism-equivᵣ : ∀{x y : Objᵣ} → Equiv{ℓᵣₑ}(Morphismᵣ x y) ⦄
  (Categoryₗ : Category(Morphismₗ))
  (Categoryᵣ : Category(Morphismᵣ))
  where

  ContravariantFunctor : (Objₗ → Objᵣ) → Type
  ContravariantFunctor = Functor (dualCategory Categoryₗ) Categoryᵣ
  module ContravariantFunctor = Functor{Categoryₗ = dualCategory Categoryₗ}{Categoryᵣ = Categoryᵣ}

module _
  ⦃ morphism-equiv : ∀{x y : Obj} → Equiv{ℓₑ}(Morphism x y) ⦄
  (Category : Category(Morphism))
  where

  ContravariantEndofunctor = ContravariantFunctor(Category)(Category)
  module ContravariantEndofunctor = ContravariantFunctor(Category)(Category)

_→ᶜᵒⁿᵗʳᵃᵛᵃʳⁱᵃⁿᵗᶠᵘⁿᶜᵗᵒʳ_ : CategoryObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ} → CategoryObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ} → Type
catₗ →ᶜᵒⁿᵗʳᵃᵛᵃʳⁱᵃⁿᵗᶠᵘⁿᶜᵗᵒʳ catᵣ = ∃(ContravariantFunctor (CategoryObject.category(catₗ)) ((CategoryObject.category(catᵣ))))

⟲ᶜᵒⁿᵗʳᵃᵛᵃʳⁱᵃⁿᵗᶠᵘⁿᶜᵗᵒʳ_ : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ} → Type
⟲ᶜᵒⁿᵗʳᵃᵛᵃʳⁱᵃⁿᵗᶠᵘⁿᶜᵗᵒʳ cat = cat →ᶜᵒⁿᵗʳᵃᵛᵃʳⁱᵃⁿᵗᶠᵘⁿᶜᵗᵒʳ cat

module _ (C₁ C₂ : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}) where
  open import Logic.Propositional
  open import Structure.Relator.Equivalence

  open CategoryObject ⦃ … ⦄
  open Category ⦃ … ⦄
  open ArrowNotation
  open Functor ⦃ … ⦄
  private open module MorphismEquiv₁ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv ⦃ C₁ ⦄ {x}{y} ⦄) using ()
  private open module MorphismEquiv₂ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv ⦃ C₂ ⦄ {x}{y} ⦄) using ()

  instance _ = C₁
  instance _ = C₂

  contravariant-functor-def-dual : (dual(C₁) →ᶠᵘⁿᶜᵗᵒʳ C₂) ↔ (C₁ →ᶠᵘⁿᶜᵗᵒʳ dual(C₂))
  contravariant-functor-def-dual = [↔]-intro l r where
    l : (dual(C₁) →ᶠᵘⁿᶜᵗᵒʳ C₂) ← (C₁ →ᶠᵘⁿᶜᵗᵒʳ dual(C₂))
    ∃.witness (l ([∃]-intro F)) = F
    Functor.map           (∃.proof (l _)) = map
    Functor.map-function  (∃.proof (l _)) = map-function
    Functor.op-preserving (∃.proof (l _)) = op-preserving
    Functor.id-preserving (∃.proof (l _)) = id-preserving

    r : (dual(C₁) →ᶠᵘⁿᶜᵗᵒʳ C₂) → (C₁ →ᶠᵘⁿᶜᵗᵒʳ dual(C₂))
    ∃.witness (r ([∃]-intro F)) = F
    Functor.map           (∃.proof (r _)) = map
    Functor.map-function  (∃.proof (r _)) = map-function
    Functor.op-preserving (∃.proof (r _)) = op-preserving
    Functor.id-preserving (∃.proof (r _)) = id-preserving

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

postulate _↦_ : Set → Set → Set
{-# BUILTIN REWRITE _↦_ #-}

postulate
  X : Set
  P : Set → Set → Set
  P-rewr : (A : Set) → (P A A ↦ X)
  {-# REWRITE P-rewr #-}

f : (B : Set → Set) {x y : Set} → P (B x) (B y)
f = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sublist-related properties
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Propositional.Properties {a} {A : Set a} where

open import Data.List using (map)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties using (here-injective; there-injective)
open import Data.List.Relation.Binary.Sublist.Propositional
  hiding (map)
import Data.List.Relation.Binary.Sublist.Setoid.Properties
  as SetoidProperties
open import Function
open import Relation.Binary.PropositionalEquality as P hiding ([_])
open import Relation.Unary as U using (Pred)

------------------------------------------------------------------------
-- Re-exporting setoid properties

open SetoidProperties (P.setoid A) public
  hiding (map⁺)

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

module _ {b} {B : Set b} where

  map⁺ : ∀ {as bs} (f : A → B) → as ⊆ bs → map f as ⊆ map f bs
  map⁺ f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f)

------------------------------------------------------------------------
-- The `lookup` function induced by a proof that `xs ⊆ ys` is injective

module _ {p} {P : Pred A p} where

  lookup-injective : ∀ {xs ys} {p : xs ⊆ ys} {v w : Any P xs} →
                     lookup p v ≡ lookup p w → v ≡ w
  lookup-injective {p = []}       {}
  lookup-injective {p = _   ∷ʳ _} {v}       {w}       =
    lookup-injective ∘′ there-injective
  lookup-injective {p = x≡y ∷ _}  {here pv} {here pw} =
    cong here ∘′ subst-injective x≡y ∘′ here-injective
  lookup-injective {p = _ ∷ _}    {there v} {there w} =
    cong there ∘′ lookup-injective ∘′ there-injective
  lookup-injective {p = _ ∷ _}    {here  _} {there _} ()
  lookup-injective {p = _ ∷ _}    {there _} {here  _} ()


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function using (_∘_; _$_; flip; id)
open import Cubical.Foundations.Logic hiding (_⇒_; _⇔_) renaming (⇔toPath to hProp⇔toPath)

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Binary.Definitions

open import Cubical.Relation.Nullary.Decidable hiding (¬_)

open import Cubical.Data.Maybe using (just; nothing; Dec→Maybe; map-Maybe)
open import Cubical.Data.Sum.Base as Sum using (inl; inr)
open import Cubical.Data.Empty using (⊥; isProp⊥) renaming (elim to ⊥-elim)
open import Cubical.HITs.PropositionalTruncation

private
  variable
    a b ℓ ℓ₁ ℓ₂ ℓ₃ p : Level
    A : Type a
    B : Type b

------------------------------------------------------------------------
-- Equality properties

≡ₚReflexive : Reflexive (_≡ₚ_ {A = A})
≡ₚReflexive = ∣ refl ∣

≡ₚSymmetric : Symmetric (_≡ₚ_ {A = A})
≡ₚSymmetric = map sym

≡ₚTransitive : Transitive (_≡ₚ_ {A = A})
≡ₚTransitive = map2 _∙_

≡ₚSubstitutive : Substitutive (_≡ₚ_ {A = A}) ℓ
≡ₚSubstitutive P = elim (λ _ → isPropΠ λ _ → P _ .snd) (subst (λ x → P x .fst))

------------------------------------------------------------------------
-- Substitutive properties

module _ (_∼_ : Rel A ℓ₁) (P : Rel A p) where

  subst→respˡ : Substitutive _∼_ p → P Respectsˡ _∼_
  subst→respˡ subst {y} x′∼x Px′y = subst (flip P y) x′∼x Px′y

  subst→respʳ : Substitutive _∼_ p → P Respectsʳ _∼_
  subst→respʳ subst {x} y′∼y Pxy′ = subst (P x) y′∼y Pxy′

  subst→resp₂ : Substitutive _∼_ p → P Respects₂ _∼_
  subst→resp₂ subst = subst→respʳ subst , subst→respˡ subst

module _ (_∼_ : Rel A ℓ) (P : A → hProp p) where

  P-resp→¬P-resp : Symmetric _∼_ → P Respects _∼_ → (¬_ ∘ P) Respects _∼_
  P-resp→¬P-resp sym resp x∼y ¬Px Py = ¬Px (resp (sym x∼y) Py)

Respectsʳ≡ₚ : (_∼_ : Rel A ℓ) → _∼_ Respectsʳ _≡ₚ_
Respectsʳ≡ₚ _∼_ = subst→respʳ _≡ₚ_ _∼_ ≡ₚSubstitutive

Respectsˡ≡ₚ : (_∼_ : Rel A ℓ) → _∼_ Respectsˡ _≡ₚ_
Respectsˡ≡ₚ _∼_ = subst→respˡ _≡ₚ_ _∼_ ≡ₚSubstitutive

Respects₂≡ₚ : (_∼_ : Rel A ℓ) → _∼_ Respects₂ _≡ₚ_
Respects₂≡ₚ _∼_ = subst→resp₂ _≡ₚ_ _∼_ ≡ₚSubstitutive

------------------------------------------------------------------------
-- Proofs for non-strict orders

module _ (_≤_ : Rel A ℓ) where

  rawtotal→FromEq : RawTotal _≤_ → FromEq _≤_
  rawtotal→FromEq total {x} {y} x≡y with total x y
  ... | inl x∼y = x∼y
  ... | inr y∼x = Respectsʳ≡ₚ _≤_ x≡y (Respectsˡ≡ₚ _≤_ (≡ₚSymmetric x≡y) y∼x)

  total→FromEq : Total _≤_ → FromEq _≤_
  total→FromEq total {x} {y} x≡y = elim (λ _ → (x ≤ y) .snd)
    (λ {
      (inl x∼y) → x∼y
    ; (inr y∼x) → Respectsʳ≡ₚ _≤_ x≡y (Respectsˡ≡ₚ _≤_ (≡ₚSymmetric x≡y) y∼x)
    }) (total x y)

------------------------------------------------------------------------
-- Proofs for strict orders

module _ (_<_ : Rel A ℓ) where

  trans∧irr→asym : Transitive _<_ → Irreflexive _<_ → Asymmetric _<_
  trans∧irr→asym transitive irrefl x<y y<x = irrefl (transitive x<y y<x)

  irr∧antisym→asym : Irreflexive _<_ → Antisymmetric _<_ → Asymmetric _<_
  irr∧antisym→asym irrefl antisym x<y y<x = irrefl→tonoteq irrefl x<y (antisym x<y y<x)
    where
      irrefl→tonoteq : Irreflexive _<_ → ToNotEq _<_
      irrefl→tonoteq irrefl {x} {y} x<y x≡y = irrefl (substₚ (λ z → x < z) (≡ₚSymmetric x≡y) x<y)

  asym→antisym : Asymmetric _<_ → Antisymmetric _<_
  asym→antisym asym x<y y<x = ⊥-elim (asym x<y y<x)

  asym→irr : Asymmetric _<_ → Irreflexive _<_
  asym→irr asym {x} x<x = asym x<x x<x

  tri→asym : Trichotomous _<_ → Asymmetric _<_
  tri→asym compare {x} {y} x<y x>y with compare x y
  ... | tri< _   _ x≯y = x≯y x>y
  ... | tri≡ _   _ x≯y = x≯y x>y
  ... | tri> x≮y _ _   = x≮y x<y

  tri→irr : Trichotomous _<_ → Irreflexive _<_
  tri→irr compare {x} x<x with compare x x
  ... | tri< _ _ x≮x = x≮x x<x
  ... | tri≡ _ _ x≮x = x≮x x<x
  ... | tri> x≮x _ _ = x≮x x<x

  tri→dec≡ : Trichotomous _<_ → Discrete A
  tri→dec≡ compare x y with compare x y
  ... | tri< _ x≢y _ = no  x≢y
  ... | tri≡ _ x≡y _ = yes x≡y
  ... | tri> _ x≢y _ = no  x≢y

  tri→dec< : Trichotomous _<_ → Decidable _<_
  tri→dec< compare x y with compare x y
  ... | tri< x<y _ _ = yes x<y
  ... | tri≡ x≮y _ _ = no  x≮y
  ... | tri> x≮y _ _ = no  x≮y

------------------------------------------------------------------------
-- Without Loss of Generality

module _ {R : Rel A ℓ₁} {Q : Rel A ℓ₂} where

  wlog : Total R → Symmetric Q →
         R ⇒ Q → Universal Q
  wlog r-total q-sym prf a b = elim (λ _ → Q a b .snd)
    (λ {
      (inl Rab) → prf Rab
    ; (inr Rba) → q-sym (prf Rba)
    }) (r-total a b)

------------------------------------------------------------------------
-- Other proofs

module _ {P : REL A B p} where

  dec→weaklyDec : Decidable P → WeaklyDecidable P
  dec→weaklyDec dec x y = Dec→Maybe (dec x y)

module _ {P : Rel A ℓ₁} {Q : Rel A ℓ₂} (f : P ⇒ Q) where

  map-Reflexive : Reflexive P → Reflexive Q
  map-Reflexive reflx = f reflx

  map-FromEq : FromEq P → FromEq Q
  map-FromEq fromEq p = f (fromEq p)

  cmap-Irreflexive : Irreflexive Q → Irreflexive P
  cmap-Irreflexive irrefl x≡x = irrefl (f x≡x)

  cmap-ToNotEq : ToNotEq Q → ToNotEq P
  cmap-ToNotEq toNotEq x = toNotEq (f x)

module _ {P : REL A B ℓ₁} {Q : REL A B ℓ₂} (f : P ⇒ Q) where

  map-Universal : Universal P → Universal Q
  map-Universal u x y = f (u x y)

  map-NonEmpty : NonEmpty P → NonEmpty Q
  map-NonEmpty = map (λ (x , p) → x , map (λ (y , q) → y , f q) p)

module _ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} where

  flip-RawConnex : RawConnex P Q → RawConnex Q P
  flip-RawConnex f x y = Sum.swap (f y x)

  flip-Connex : Connex P Q → Connex Q P
  flip-Connex f x y = map Sum.swap (f y x)

module _ (_∼_ : Rel A ℓ) where

  reflx→fromeq : Reflexive _∼_ → FromEq _∼_
  reflx→fromeq reflx {x} p = substₚ (x ∼_) p reflx

  fromeq→reflx : FromEq _∼_ → Reflexive _∼_
  fromeq→reflx fromEq = fromEq ∣ refl ∣

  irrefl→tonoteq : Irreflexive _∼_ → ToNotEq _∼_
  irrefl→tonoteq irrefl {x} {y} x<y x≡y = irrefl (substₚ (x ∼_) (≡ₚSymmetric x≡y) x<y)

  tonoteq→irrefl : ToNotEq _∼_ → Irreflexive _∼_
  tonoteq→irrefl toNotEq x<x = toNotEq x<x ∣ refl ∣

------------------------------------------------------------------------
-- Proofs for propositional relations only

isPropIsPropValued : {R : RawREL A B ℓ} → isProp (isPropValued R)
isPropIsPropValued a b i x y = isPropIsProp (a x y) (b x y) i

module _ (R : Rel A ℓ) where

  isPropReflexive : isProp (Reflexive R)
  isPropReflexive a b i {x} = R x x .snd a b i

  isPropFromEq : isProp (FromEq R)
  isPropFromEq a b i {x} {y} p = R x y .snd (a p) (b p) i

  isPropIrreflexive : isProp (Irreflexive R)
  isPropIrreflexive a b i {x} xRx = isProp⊥ (a xRx) (b xRx) i

  isPropToNotEq : isProp (ToNotEq R)
  isPropToNotEq a b i {x} {y} xRy x≡y = isProp⊥ (a xRy x≡y) (b xRy x≡y) i

  isPropAsymmetric : isProp (Asymmetric R)
  isPropAsymmetric a b i {x} {y} xRy yRx = isProp⊥ (a xRy yRx) (b xRy yRx) i

isProp⇒ : (R : REL A B ℓ₁) (Q : REL A B ℓ₂) → isProp (R ⇒ Q)
isProp⇒ R Q a b i {x} {y} xRy = Q x y .snd (a xRy) (b xRy) i

isPropSym : (R : REL A B ℓ₁) (Q : REL B A ℓ₂) → isProp (Sym R Q)
isPropSym R Q = isProp⇒ R (flip Q)

isPropTrans : ∀ {c} {C : Type c}
                      (P : REL A B ℓ₁) (Q : REL B C ℓ₂) (R : REL A C ℓ₃) →
                      isProp (Trans P Q R)
isPropTrans P Q R a b i {x} {_} {z} xPy yQz = R x z .snd (a xPy yQz) (b xPy yQz) i

isPropAntisym : (R : REL A B ℓ₁) (Q : REL B A ℓ₂) (E : REL A B ℓ₃) → isProp (Antisym R Q E)
isPropAntisym R Q E a b i {x} {y} xRy yQx = E x y .snd (a xRy yQx) (b xRy yQx) i

module _ (R : REL A B ℓ) where

  Universal→isContrValued : Universal R → ∀ {a b} → isContr ⟨ R a b ⟩
  Universal→isContrValued univr {a} {b} = univr a b , R a b .snd _

------------------------------------------------------------------------
-- Bidirectional implication and equality

⇔toPath : {R : REL A B ℓ} {Q : REL A B ℓ} → R ⇔ Q → R ≡ Q
⇔toPath (R⇒Q , Q⇒R) = funExt (λ x → funExt (λ y → hProp⇔toPath R⇒Q Q⇒R))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- "Finite" sets indexed on coinductive "natural" numbers
------------------------------------------------------------------------

{-# OPTIONS --without-K --sized-types --guardedness #-}

module Codata.Musical.Cofin where

open import Codata.Musical.Notation
open import Codata.Musical.Conat as Conat using (Coℕ; suc; ∞ℕ)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Function

------------------------------------------------------------------------
-- The type

-- Note that Cofin ∞ℕ is /not/ finite. Note also that this is not a
-- coinductive type, but it is indexed on a coinductive type.

data Cofin : Coℕ → Set where
  zero : ∀ {n} → Cofin (suc n)
  suc  : ∀ {n} (i : Cofin (♭ n)) → Cofin (suc n)

suc-injective : ∀ {m} {p q : Cofin (♭ m)} → (Cofin (suc m) ∋ suc p) ≡ suc q → p ≡ q
suc-injective refl = refl

------------------------------------------------------------------------
-- Some operations

fromℕ : ℕ → Cofin ∞ℕ
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

toℕ : ∀ {n} → Cofin n → ℕ
toℕ zero    = zero
toℕ (suc i) = suc (toℕ i)

fromFin : ∀ {n} → Fin n → Cofin (Conat.fromℕ n)
fromFin zero    = zero
fromFin (suc i) = suc (fromFin i)

toFin : ∀ n → Cofin (Conat.fromℕ n) → Fin n
toFin zero    ()
toFin (suc n) zero    = zero
toFin (suc n) (suc i) = suc (toFin n i)

import Codata.Cofin as C

fromMusical : ∀ {n} → Cofin n → C.Cofin (Conat.fromMusical n)
fromMusical zero    = C.zero
fromMusical (suc n) = C.suc (fromMusical n)

toMusical : ∀ {n} → C.Cofin n → Cofin (Conat.toMusical n)
toMusical C.zero    = zero
toMusical (C.suc n) = suc (toMusical n)


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module Number.Coercions where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_

open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Empty -- ⊥
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`

open import Number.Postulates
open import Number.Inclusions
open import Number.Base
open import MoreNatProperties

open ℕⁿ
open ℤᶻ
open ℚᶠ
open ℝʳ
open ℂᶜ

open PatternsProp

module Coerce-ℕ↪ℤ where
  open ℤ
  open IsROrderedCommSemiringInclusion -- ℕ↪ℤinc
  private f = ℕ↪ℤ
  abstract
    coerce-ℕ↪ℤ : ∀{p} → (x : Number (isNat , p)) → PositivityKindInterpretation isInt (coerce-PositivityKind isNat isInt p) (ℕ↪ℤ (num x))
    coerce-ℕ↪ℤ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℕ↪ℤ {x#0} (x ,, q) = preserves-#0 ℕ↪ℤinc _ q -- transport (λ i → f x # preserves-0 i) (preserves-# _ _ q)
    coerce-ℕ↪ℤ {0≤x} (x ,, q) = preserves-0≤ ℕ↪ℤinc _ q -- transport (λ i → preserves-0 i ≤ f x) (preserves-≤ _ _ q)
    coerce-ℕ↪ℤ {0<x} (x ,, q) = preserves-0< ℕ↪ℤinc _ q -- transport (λ i → preserves-0 i < f x) (preserves-< _ _ q)
    coerce-ℕ↪ℤ {x≤0} (x ,, q) = preserves-≤0 ℕ↪ℤinc _ q -- transport (λ i → f x ≤ preserves-0 i) (preserves-≤ _ _ q)

module Coerce-ℕ↪ℚ where
  open ℚ
  open IsROrderedCommSemiringInclusion -- ℕ↪ℚinc
  private f = ℕ↪ℚ
  abstract
    coerce-ℕ↪ℚ : ∀{p} → (x : Number (isNat , p)) → PositivityKindInterpretation isRat (coerce-PositivityKind isNat isRat p) (ℕ↪ℚ (num x))
    coerce-ℕ↪ℚ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℕ↪ℚ {x#0} (x ,, q) = preserves-#0 ℕ↪ℚinc _ q -- transport (λ i → f x # preserves-0 i) (preserves-# _ _ q)
    coerce-ℕ↪ℚ {0≤x} (x ,, q) = preserves-0≤ ℕ↪ℚinc _ q -- transport (λ i → preserves-0 i ≤ f x) (preserves-≤ _ _ q)
    coerce-ℕ↪ℚ {0<x} (x ,, q) = preserves-0< ℕ↪ℚinc _ q -- transport (λ i → preserves-0 i < f x) (preserves-< _ _ q)
    coerce-ℕ↪ℚ {x≤0} (x ,, q) = preserves-≤0 ℕ↪ℚinc _ q -- transport (λ i → f x ≤ preserves-0 i) (preserves-≤ _ _ q)

module Coerce-ℕ↪ℝ where
  open ℝ
  open IsROrderedCommSemiringInclusion -- ℕ↪ℝinc
  private f = ℕ↪ℝ
  abstract
    coerce-ℕ↪ℝ : ∀{p} → (x : Number (isNat , p)) → PositivityKindInterpretation isReal (coerce-PositivityKind isNat isReal p) (ℕ↪ℝ (num x))
    coerce-ℕ↪ℝ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℕ↪ℝ {x#0} (x ,, q) = preserves-#0 ℕ↪ℝinc _ q -- transport (λ i → f x # preserves-0 i) (preserves-# _ _ q)
    coerce-ℕ↪ℝ {0≤x} (x ,, q) = preserves-0≤ ℕ↪ℝinc _ q -- transport (λ i → preserves-0 i ≤ f x) (preserves-≤ _ _ q)
    coerce-ℕ↪ℝ {0<x} (x ,, q) = preserves-0< ℕ↪ℝinc _ q -- transport (λ i → preserves-0 i < f x) (preserves-< _ _ q)
    coerce-ℕ↪ℝ {x≤0} (x ,, q) = preserves-≤0 ℕ↪ℝinc _ q -- transport (λ i → f x ≤ preserves-0 i) (preserves-≤ _ _ q)

module Coerce-ℕ↪ℂ where
  open ℂ
  open Isℕ↪ℂ -- ℕ↪ℂinc
  private f = ℕ↪ℂ
  abstract
    coerce-ℕ↪ℂ : ∀{p} → (x : Number (isNat , p)) → PositivityKindInterpretation isComplex (coerce-PositivityKind isNat isComplex p) (ℕ↪ℂ (num x))
    coerce-ℕ↪ℂ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℕ↪ℂ {x#0} (x ,, q) = transport (λ i → f x # preserves-0 ℕ↪ℂinc i) (preserves-# ℕ↪ℂinc _ _ q)
    coerce-ℕ↪ℂ {0≤x} (x ,, q) = lift tt
    coerce-ℕ↪ℂ {0<x} (x ,, q) = transport (λ i → f x # preserves-0 ℕ↪ℂinc i) (preserves-# ℕ↪ℂinc _ _ (ℕ.#-sym _ _ (ℕ.<-implies-# _ _ q)))
    coerce-ℕ↪ℂ {x≤0} (x ,, q) = lift tt

module Coerce-ℤ↪ℚ where
  open ℚ
  open IsROrderedCommRingInclusion -- ℤ↪ℚinc
  private f = ℤ↪ℚ
  abstract
    coerce-ℤ↪ℚ : ∀{p} → (x : Number (isInt , p)) → PositivityKindInterpretation isRat (coerce-PositivityKind isInt isRat p) (ℤ↪ℚ (num x))
    coerce-ℤ↪ℚ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℤ↪ℚ {x#0} (x ,, q) = preserves-#0 ℤ↪ℚinc _ q -- transport (λ i → f x # preserves-0 i) (preserves-# _ _ q)
    coerce-ℤ↪ℚ {0≤x} (x ,, q) = preserves-0≤ ℤ↪ℚinc _ q -- transport (λ i → preserves-0 i ≤ f x) (preserves-≤ _ _ q)
    coerce-ℤ↪ℚ {0<x} (x ,, q) = preserves-0< ℤ↪ℚinc _ q -- transport (λ i → preserves-0 i < f x) (preserves-< _ _ q)
    coerce-ℤ↪ℚ {x<0} (x ,, q) = preserves-<0 ℤ↪ℚinc _ q -- transport (λ i → f x < preserves-0 i) (preserves-< _ _ q)
    coerce-ℤ↪ℚ {x≤0} (x ,, q) = preserves-≤0 ℤ↪ℚinc _ q -- transport (λ i → f x ≤ preserves-0 i) (preserves-≤ _ _ q)

module Coerce-ℤ↪ℝ where
  open ℝ
  open IsROrderedCommRingInclusion --  ℤ↪ℝinc
  private f = ℤ↪ℝ
  abstract
    coerce-ℤ↪ℝ : ∀{p} → (x : Number (isInt , p)) → PositivityKindInterpretation isReal (coerce-PositivityKind isInt isReal p) (ℤ↪ℝ (num x))
    coerce-ℤ↪ℝ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℤ↪ℝ {x#0} (x ,, q) = preserves-#0 ℤ↪ℝinc _ q -- transport (λ i → f x # preserves-0 i) (preserves-# _ _ q)
    coerce-ℤ↪ℝ {0≤x} (x ,, q) = preserves-0≤ ℤ↪ℝinc _ q -- transport (λ i → preserves-0 i ≤ f x) (preserves-≤ _ _ q)
    coerce-ℤ↪ℝ {0<x} (x ,, q) = preserves-0< ℤ↪ℝinc _ q -- transport (λ i → preserves-0 i < f x) (preserves-< _ _ q)
    coerce-ℤ↪ℝ {x<0} (x ,, q) = preserves-<0 ℤ↪ℝinc _ q -- transport (λ i → f x < preserves-0 i) (preserves-< _ _ q)
    coerce-ℤ↪ℝ {x≤0} (x ,, q) = preserves-≤0 ℤ↪ℝinc _ q -- transport (λ i → f x ≤ preserves-0 i) (preserves-≤ _ _ q)

module Coerce-ℤ↪ℂ where
  open ℂ
  open Isℤ↪ℂ -- ℤ↪ℂinc
  private f = ℤ↪ℂ
  abstract
    coerce-ℤ↪ℂ : ∀{p} → (x : Number (isInt , p)) → PositivityKindInterpretation isComplex (coerce-PositivityKind isInt isComplex p) (ℤ↪ℂ (num x))
    coerce-ℤ↪ℂ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℤ↪ℂ {x#0} (x ,, q) = transport (λ i → f x # preserves-0 ℤ↪ℂinc i) (preserves-# ℤ↪ℂinc _ _ q)
    coerce-ℤ↪ℂ {0≤x} (x ,, q) = lift tt
    coerce-ℤ↪ℂ {0<x} (x ,, q) = transport (λ i → f x # preserves-0 ℤ↪ℂinc i) (preserves-# ℤ↪ℂinc _ _ (ℤ.#-sym _ _ (ℤ.<-implies-# _ _ q)))
    coerce-ℤ↪ℂ {x<0} (x ,, q) = transport (λ i → f x # preserves-0 ℤ↪ℂinc i) (preserves-# ℤ↪ℂinc _ _              (ℤ.<-implies-# _ _ q) )
    coerce-ℤ↪ℂ {x≤0} (x ,, q) = lift tt

module Coerce-ℚ↪ℝ where
  open ℝ
  open IsROrderedFieldInclusion -- ℚ↪ℝinc
  private f = ℚ↪ℝ
  abstract
    coerce-ℚ↪ℝ : ∀{p} → (x : Number (isRat , p)) → PositivityKindInterpretation isReal (coerce-PositivityKind isRat isReal p) (ℚ↪ℝ (num x))
    coerce-ℚ↪ℝ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℚ↪ℝ {x#0} (x ,, q) = preserves-#0 ℚ↪ℝinc _ q -- transport (λ i → f x # preserves-0 i) (preserves-# _ _ q)
    coerce-ℚ↪ℝ {0≤x} (x ,, q) = preserves-0≤ ℚ↪ℝinc _ q -- transport (λ i → preserves-0 i ≤ f x) (preserves-≤ _ _ q)
    coerce-ℚ↪ℝ {0<x} (x ,, q) = preserves-0< ℚ↪ℝinc _ q -- transport (λ i → preserves-0 i < f x) (preserves-< _ _ q)
    coerce-ℚ↪ℝ {x<0} (x ,, q) = preserves-<0 ℚ↪ℝinc _ q -- transport (λ i → f x < preserves-0 i) (preserves-< _ _ q)
    coerce-ℚ↪ℝ {x≤0} (x ,, q) = preserves-≤0 ℚ↪ℝinc _ q -- transport (λ i → f x ≤ preserves-0 i) (preserves-≤ _ _ q)

module Coerce-ℚ↪ℂ where
  open ℂ
  open IsRFieldInclusion -- ℚ↪ℂinc
  private f = ℚ↪ℂ
  abstract
    coerce-ℚ↪ℂ : ∀{p} → (x : Number (isRat , p)) → PositivityKindInterpretation isComplex (coerce-PositivityKind isRat isComplex p) (ℚ↪ℂ (num x))
    coerce-ℚ↪ℂ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℚ↪ℂ {x#0} (x ,, q) = preserves-#0 ℚ↪ℂinc _ q -- transport (λ i → f x # preserves-0 ℚ↪ℂinc i) (preserves-# ℚ↪ℂinc _ _ q)
    coerce-ℚ↪ℂ {0≤x} (x ,, q) = lift tt
    coerce-ℚ↪ℂ {0<x} (x ,, q) = transport (λ i → f x # preserves-0 ℚ↪ℂinc i) (preserves-# ℚ↪ℂinc _ _ (ℚ.#-sym _ _ (ℚ.<-implies-# _ _ q)))
    coerce-ℚ↪ℂ {x<0} (x ,, q) = transport (λ i → f x # preserves-0 ℚ↪ℂinc i) (preserves-# ℚ↪ℂinc _ _              (ℚ.<-implies-# _ _ q) )
    coerce-ℚ↪ℂ {x≤0} (x ,, q) = lift tt

module Coerce-ℝ↪ℂ where
  -- open ℂ
  open IsRFieldInclusion -- ℝ↪ℂinc
  private f = ℝ↪ℂ
  abstract
    coerce-ℝ↪ℂ : ∀{p} → (x : Number (isReal , p)) → PositivityKindInterpretation isComplex (coerce-PositivityKind isReal isComplex p) (ℝ↪ℂ (num x))
    coerce-ℝ↪ℂ {⁇x⁇} (x ,, q) = lift tt
    coerce-ℝ↪ℂ {x#0} (x ,, q) = preserves-#0 ℝ↪ℂinc _ q -- transport (λ i → f x # preserves-0 ℝ↪ℂinc i) (preserves-# ℝ↪ℂinc _ _ q)
    coerce-ℝ↪ℂ {0≤x} (x ,, q) = lift tt
    coerce-ℝ↪ℂ {0<x} (x ,, q) = transport (λ i → f x ℂ.# preserves-0 ℝ↪ℂinc i) (preserves-# ℝ↪ℂinc _ _ (ℝ.#-sym _ _ (ℝ.<-implies-# _ _ q)))
    coerce-ℝ↪ℂ {x<0} (x ,, q) = transport (λ i → f x ℂ.# preserves-0 ℝ↪ℂinc i) (preserves-# ℝ↪ℂinc _ _              (ℝ.<-implies-# _ _ q) )
    coerce-ℝ↪ℂ {x≤0} (x ,, q) = lift tt

-- NOTE: typechecking of this module is very slow
--       the cause might be opening of the ten `IsXInclusion` instances
--       it could be related to https://github.com/agda/agda/issues/1646 (Exponential module chain leads to infeasible scope checking)
--       YES: this is the case. After shifting the module arguments from `open` into the code, checking became instant again

-- does this make anything faster?
open Coerce-ℕ↪ℤ public
open Coerce-ℕ↪ℚ public
open Coerce-ℕ↪ℝ public
open Coerce-ℕ↪ℂ public
open Coerce-ℤ↪ℚ public
open Coerce-ℤ↪ℝ public
open Coerce-ℤ↪ℂ public
open Coerce-ℚ↪ℝ public
open Coerce-ℚ↪ℂ public
open Coerce-ℝ↪ℂ public

coerce : (from : NumberKind)
       → (to   : NumberKind)
       → from ≤ₙₗ to
       → ∀{p}
       → Number (from ,                               p)
       → Number (to   , coerce-PositivityKind from to p)
coerce isNat     isNat     q {p} x = x
coerce isInt     isInt     q {p} x = x
coerce isRat     isRat     q {p} x = x
coerce isReal    isReal    q {p} x = x
coerce isComplex isComplex q {p} x = x
coerce isNat     isInt     q {p} x = (ℕ↪ℤ (num x) ,, coerce-ℕ↪ℤ x)
coerce isNat     isRat     q {p} x = (ℕ↪ℚ (num x) ,, coerce-ℕ↪ℚ x)
coerce isNat     isReal    q {p} x = (ℕ↪ℝ (num x) ,, coerce-ℕ↪ℝ x)
coerce isNat     isComplex q {p} x = (ℕ↪ℂ (num x) ,, coerce-ℕ↪ℂ x)
coerce isInt     isRat     q {p} x = (ℤ↪ℚ (num x) ,, coerce-ℤ↪ℚ x)
coerce isInt     isReal    q {p} x = (ℤ↪ℝ (num x) ,, coerce-ℤ↪ℝ x)
coerce isInt     isComplex q {p} x = (ℤ↪ℂ (num x) ,, coerce-ℤ↪ℂ x)
coerce isRat     isReal    q {p} x = (ℚ↪ℝ (num x) ,, coerce-ℚ↪ℝ x)
coerce isRat     isComplex q {p} x = (ℚ↪ℂ (num x) ,, coerce-ℚ↪ℂ x)
coerce isReal    isComplex q {p} x = (ℝ↪ℂ (num x) ,, coerce-ℝ↪ℂ x)
--coerce x         y         = nothing
coerce isInt     isNat  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isNat  , p)} (k+x+sy≢x _ _ _ q)
coerce isRat     isNat  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isNat  , p)} (k+x+sy≢x _ _ _ q)
coerce isRat     isInt  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isInt  , p)} (k+x+sy≢x _ _ _ q)
coerce isReal    isNat  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isNat  , p)} (k+x+sy≢x _ _ _ q)
coerce isReal    isInt  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isInt  , p)} (k+x+sy≢x _ _ _ q)
coerce isReal    isRat  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isRat  , p)} (k+x+sy≢x _ _ _ q)
coerce isComplex isNat  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isNat  , coerce-PositivityKind isComplex isNat  p)} (k+x+sy≢x _ _ _ q)
coerce isComplex isInt  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isInt  , coerce-PositivityKind isComplex isInt  p)} (k+x+sy≢x _ _ _ q)
coerce isComplex isRat  r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isRat  , coerce-PositivityKind isComplex isRat  p)} (k+x+sy≢x _ _ _ q)
coerce isComplex isReal r@(k , q) {p} x = ⊥-elim {A = λ _ → Number (isReal , coerce-PositivityKind isComplex isReal p)} (k+x+sy≢x _ _ _ q)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module Control.Exception where

open import IO
import Control.Exception.Primitive as Prim

bracket : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → IO A → (A → IO B) → (A → IO C) → IO C
bracket io final body = lift (Prim.bracket (run io) (λ a1 → run (final a1)) (λ a2 → run (body a2)))

max_stars_repo_name: ilya-fiveisky/agda-exceptions

max_issues_repo_name: ilya-fiveisky/agda-exceptions

max_forks_repo_name: ilya-fiveisky/agda-exceptions


text:
open import Oscar.Prelude

module Oscar.Class.Bind where

module _
  (𝔉 : ∀ {𝔣} → Ø 𝔣 → Ø 𝔣)
  𝔬₁ 𝔬₂
  where
  𝓫ind = ∀ {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂} → 𝔉 𝔒₁ → (𝔒₁ → 𝔉 𝔒₂) → 𝔉 𝔒₂
  record 𝓑ind : Ø ↑̂ (𝔬₁ ∙̂ 𝔬₂) where
    infixl 6 bind
    field bind : 𝓫ind
    syntax bind m f = f =<< m
  open 𝓑ind ⦃ … ⦄ public


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Concrete.Obligations
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import Util.Prelude

open        EpochConfig
open import Yasm.Base
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

-- In this module, we assume that the implementation meets its
-- obligations, and use this assumption to prove that, in any reachable
-- state, the implementatioon enjoys one of the per-epoch correctness
-- conditions proved in Abstract.Properties.  It can be extended to other
-- properties later.
module LibraBFT.Concrete.Properties
         (iiah         : SystemInitAndHandlers ℓ-RoundManager ConcSysParms)
         (st           : SystemState)
         (r            : WithInitAndHandlers.ReachableSystemState iiah st)
         (𝓔           : EpochConfig)
         (𝓔-∈sys       : ParamsWithInitAndHandlers.EpochConfig∈Sys iiah st 𝓔)
         (impl-correct : ImplObligations iiah 𝓔)
         where

  open WithEC
  open import LibraBFT.Abstract.Abstract     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs
  open import LibraBFT.Concrete.Intermediate                   𝓔 (ConcreteVoteEvidence 𝓔)
  import      LibraBFT.Concrete.Obligations.VotesOnce          𝓔 (ConcreteVoteEvidence 𝓔) as VO-obl
  import      LibraBFT.Concrete.Obligations.PreferredRound     𝓔 (ConcreteVoteEvidence 𝓔) as PR-obl
  open import LibraBFT.Concrete.Properties.VotesOnce                                       as VO
  open import LibraBFT.Concrete.Properties.PreferredRound                                  as PR
  open import LibraBFT.ImplShared.Util.HashCollisions iiah

  open        ImplObligations impl-correct
  open        PerEpoch 𝓔
  open        PerState st
  open        PerReachableState r

  {- Although the `Concrete` modules are currently specified in terms of the implementation types used by
     the implementation we are proving correct, the important aspect of the `Concrete` modules is to
     reduce implementation obligations specified in the `Abstract` modules to being about `Vote`s sent.
     These properties are stated in terms of an `IntermediateSystemState`, which is derived from a
     `ReachableSystemState` for an implementation-specific system configuration.

     The `Concrete` modules could be refactored to enable verifying a broader range of implementations,
     including those that use entirely different implementation types.  In more detail, the `Concrete`
     modules would be parameterized by (at least):

       - `SystemTypeParameters`;
       - `SystemInitAndHandlers`;
       - a predicate to satisy the requirements of PeerCanSignForPK, and a proof that it is stable
       - a function from a `ReachableSystemState` of a system instantiated with
         the provided `SystemTypeParameters` to an `IntermediateSystemState`;
       - proof that the `InSys` predicate is stable for the given types (i.e., if a Record is InSys
         according to the IntermediateSystemState for the prestate of a transition, then it is also
         InSys according to the IntermediateSystemState for the poststate of that transition.
       - an implementation Vote type
       - machinery for accessing signatures of Votes, and for deriving abstract Votes from them
       - proof that two Votes with the same signature represent the same abstract vote
       - ...

     This will also break existing proofs and require them to be reworked in terms of these module
     parameters.

     TODO-NOT-DO: Refactor Concrete so that it is independent of implementation types, thus making
     it more general for a wider range of implementations.  As our main motivation is verifying an
     implementation (and perhaps variations on it) that use the same types, we do not consider it
     worthwhile at this time.
  -}

  open        IntermediateSystemState intSystemState

  -- This module parameter asserts that there are no hash collisions between Blocks *in the system*,
  -- allowing us to eliminate that case when the abstract properties claim it is the case.
  module _ (no-collisions-InSys : NoCollisions InSys) where

    --------------------------------------------------------------------------------------------
    -- * A /ValidSysState/ is one in which both peer obligations are obeyed by honest peers * --
    --------------------------------------------------------------------------------------------

    record ValidSysState {ℓ}(𝓢 : IntermediateSystemState ℓ) : Set (ℓ+1 ℓ0 ℓ⊔ ℓ) where
      field
        vss-votes-once      : VO-obl.Type 𝓢
        vss-preferred-round : PR-obl.Type 𝓢
    open ValidSysState public

    validState : ValidSysState intSystemState
    validState = record
      { vss-votes-once      = VO.Proof.voo iiah 𝓔 sps-cor bsvc bsvr v≢0 ∈BI? iro      vo₂     r
      ; vss-preferred-round = PR.Proof.prr iiah 𝓔 sps-cor bsvr      v≢0 ∈BI? v4rc iro pr₁ pr₂ r 𝓔-∈sys
      }

    open All-InSys-props InSys
    open WithAssumptions InSys no-collisions-InSys

    -- We can now invoke the various abstract correctness properties.  Note that the arguments are
    -- expressed in Abstract terms (RecordChain, CommitRule).  Proving the corresponding properties
    -- for the actual implementation will involve proving that the implementation decides to commit
    -- only if it has evidence of the required RecordChains and CommitRules such that the records in
    -- the RecordChains are all "InSys" according to the implementation's notion thereof (defined in
    -- Concrete.System.intSystemState).
    ConcCommitsDoNotConflict :
       ∀{q q'}
       → {rc  : RecordChain (Abs.Q q)}  → All-InSys rc
       → {rc' : RecordChain (Abs.Q q')} → All-InSys rc'
       → {b b' : Abs.Block}
       → CommitRule rc  b
       → CommitRule rc' b'
       → (Abs.B b) ∈RC rc' ⊎ (Abs.B b') ∈RC rc
    ConcCommitsDoNotConflict =
      CommitsDoNotConflict
        (VO-obl.proof intSystemState (vss-votes-once validState))
        (PR-obl.proof intSystemState (vss-preferred-round validState))

    module _ (∈QC⇒AllSent : Complete InSys) where

      ConcCommitsDoNotConflict'
        : ∀{o o' q q'}
        → {rcf  : RecordChainFrom o  (Abs.Q q)}  → All-InSys rcf
        → {rcf' : RecordChainFrom o' (Abs.Q q')} → All-InSys rcf'
        → {b b' : Abs.Block}
        → CommitRuleFrom rcf  b
        → CommitRuleFrom rcf' b'
        →   Σ (RecordChain (Abs.Q q')) ((Abs.B b)  ∈RC_)
          ⊎ Σ (RecordChain (Abs.Q q))  ((Abs.B b') ∈RC_)
      ConcCommitsDoNotConflict' =
        CommitsDoNotConflict'
          (VO-obl.proof intSystemState (vss-votes-once validState))
          (PR-obl.proof intSystemState (vss-preferred-round validState))
          ∈QC⇒AllSent


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

data ⊥ : Set where

data Zero : Set where
  zero : Zero

data One : Set where
  suc : Zero → One

data _≤_ : One → Zero → Set where

_≤?_ : ∀ m n → m ≤ n → ⊥
suc m ≤? zero = λ ()

thm : (f : suc zero ≤ zero → ⊥) → suc zero ≤? zero ≡ f
thm f = refl
  -- (λ ()) zero x != f x of type ⊥
  --        ^^^^


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

module Categories.Diagram.End.Properties where

open import Level
open import Data.Product using (Σ; _,_)
open import Function using (_$_)

open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Construction.Functors
open import Categories.Category.Construction.TwistedArrow
open import Categories.Category.Equivalence
open import Categories.Category.Equivalence.Preserves
open import Categories.Diagram.Cone
open import Categories.Diagram.End as ∫
open import Categories.Diagram.Limit
open import Categories.Diagram.Wedge
open import Categories.Diagram.Wedge.Properties
open import Categories.Functor hiding (id)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Instance.Twisted
import Categories.Morphism as M
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Dinatural
open import Categories.Object.Terminal as Terminal

import Categories.Category.Construction.Wedges as Wedges
open import Categories.Object.Terminal

import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where
  open Wedges F

  -- Being an End is the same as being a Terminal object in the category of Wedges
  End⇒Terminal : End F → Terminal Wedges
  End⇒Terminal c =  record
    { ⊤ = wedge
    ; ⊤-is-terminal = record
      { ! = λ {A} → record { u = factor A ; commute = universal }
      ; !-unique = λ {A} f → unique {A} (Wedge-Morphism.commute f)
      }
    }
    where
    open End c

  Terminal⇒End : Terminal Wedges → End F
  Terminal⇒End i = record
    { wedge = ⊤
    ; factor = λ W → u {W₁ = W} !
    ; universal = commute !
    ; unique = λ {_} {g} x → !-unique (record { u = g ; commute = x })
    }
    where
    open Terminal.Terminal i
    open Wedge-Morphism

module _ {C : Category o ℓ e}
         (F : Functor E (Functors (Product (Category.op C) C) D)) where
  private
    module C = Category C
    module D = Category D
    module E = Category E
    module NT = NaturalTransformation
  open D
  open HomReasoning

  open MR D
  open Functor F
  open End hiding (E)
  open NT using (η)

  EndF : (∀ X → End (F₀ X)) → Functor E D
  EndF end = record
    { F₀           = λ X → End.E (end X)
    ; F₁           = F₁′
    ; identity     = λ {A} → unique (end A) (id-comm ○ ∘-resp-≈ˡ (⟺ identity))
    ; homomorphism = λ {A B C} {f g} → unique (end C) $ λ {Z} → begin
      dinatural.α (end C) Z ∘ F₁′ g ∘ F₁′ f                       ≈⟨ pullˡ (universal (end C)) ⟩
      (η (F₁ g) (Z , Z) ∘ dinatural.α (end B) Z) ∘ F₁′ f          ≈⟨ pullʳ (universal (end B)) ⟩
      η (F₁ g) (Z , Z) ∘ η (F₁ f) (Z , Z) ∘ dinatural.α (end A) Z ≈˘⟨ pushˡ homomorphism ⟩
      η (F₁ (g E.∘ f)) (Z , Z) ∘ dinatural.α (end A) Z            ∎
    ; F-resp-≈     = λ {A B f g} eq → unique (end B) $ λ {Z} → begin
      dinatural.α (end B) Z ∘ F₁′ g                               ≈⟨ universal (end B) ⟩
      η (F₁ g) (Z , Z) ∘ dinatural.α (end A) Z                    ≈˘⟨ F-resp-≈ eq ⟩∘⟨refl ⟩
      η (F₁ f) (Z , Z) ∘ dinatural.α (end A) Z                    ∎
    }
    where F₁′ : ∀ {X Y} → X E.⇒ Y → End.E (end X) ⇒ End.E (end Y)
          F₁′ {X} {Y} f = factor (end Y) $ record
            { E         = End.E (end X)
            ; dinatural = F₁ f <∘ dinatural (end X)
            }

-- A Natural Transformation between two functors induces an arrow between the
-- (object part of) the respective ends.
module _ {P Q : Functor (Product (Category.op C) C) D} (P⇒Q : NaturalTransformation P Q) where
  open End renaming (E to end)
  open Category D

  end-η : {ep : End P} {eq : End Q} → end ep ⇒ end eq
  end-η {ep} {eq} = factor eq (record
    { E = End.E ep
    ; dinatural = dtHelper record
      { α = λ c → η (c , c) ∘ dinatural.α ep c
      ; commute = λ {C} {C′} f → begin
        Q.₁ (C.id , f) ∘ (η (C , C) ∘ αp C) ∘ D.id       ≈⟨ pullˡ sym-assoc ⟩
        ((Q.₁ (C.id , f) ∘ η (C , C)) ∘ αp C) ∘ D.id     ≈⟨ (nt.sym-commute (C.id , f) ⟩∘⟨refl ⟩∘⟨refl) ⟩
        ((η (C , C′) ∘ P.₁ (C.id , f)) ∘ αp C) ∘ D.id    ≈⟨ assoc² ⟩
        η (C , C′) ∘ (P.₁ (C.id , f) ∘ αp C ∘ D.id)      ≈⟨ (refl⟩∘⟨ αp-comm f) ⟩
        η (C , C′) ∘ P.₁ (f , C.id) ∘ αp C′ ∘ D.id       ≈˘⟨ assoc² ⟩
        ((η (C , C′) ∘ P.₁ (f , C.id)) ∘ αp C′) ∘ D.id   ≈⟨ (nt.commute (f , C.id) ⟩∘⟨refl ⟩∘⟨refl) ⟩
        ((Q.₁ (f , C.id) ∘ η (C′ , C′)) ∘ αp C′) ∘ D.id  ≈⟨ pushˡ assoc ⟩
        Q.₁ (f , C.id) ∘ (η (C′ , C′) ∘ αp C′) ∘ D.id    ∎
      }
    })
    where
    module nt = NaturalTransformation P⇒Q
    open nt using (η)
    open HomReasoning
    module C = Category C
    module D = Category D
    module P = Functor P
    module Q = Functor Q
    open DinaturalTransformation (dinatural ep) renaming (α to αp; commute to αp-comm)
    open DinaturalTransformation (dinatural eq) renaming (α to αq; commute to αq-comm)
    open Wedge
    open MR D

-- The real start of the End Calculus. Maybe need to move such properties elsewhere?
-- This is an unpacking of the lhs of Eq. (25) of Loregian's book.
module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where
  private
    Eq = ConesTwist≅Wedges F
    module O = M D
  open M (Wedges.Wedges F)
  open Functor

  open StrongEquivalence Eq renaming (F to F⇒)

  -- Ends and Limits are equivalent, in the category Wedge F
  End-as-Limit : (end : End F) → (l : Limit (Twist C D F)) → End.wedge end ≅ F₀ F⇒ (Limit.terminal.⊤ l)
  End-as-Limit end l = Terminal.up-to-iso (Wedges.Wedges F) (End⇒Terminal F end) (pres-Terminal Eq terminal)
    where
    open Limit l

  -- Which then induces that the objects, in D, are also equivalent.
  End-as-Limit-on-Obj : (end : End F) → (l : Limit (Twist C D F)) → End.E end O.≅ Limit.apex l
  End-as-Limit-on-Obj end l = record
    { from = Wedge-Morphism.u (M._≅_.from X≅Y)
    ; to = Wedge-Morphism.u (M._≅_.to X≅Y)
    ; iso = record
      { isoˡ = M._≅_.isoˡ X≅Y
      ; isoʳ = M._≅_.isoʳ X≅Y
      }
    }
    where
      X≅Y = End-as-Limit end l
      open Category D

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:
{-# OPTIONS --cubical --safe #-}

open import Relation.Binary
open import Prelude hiding (Decidable)

module Data.List.Relation.Binary.Lexicographic {e ℓ₁ ℓ₂} {E : Type e} (ord : TotalOrder E ℓ₁ ℓ₂) where

open import Data.List
import Path as ≡

open TotalOrder ord renaming (refl to ≤-refl)

import Data.Empty.UniversePolymorphic as Poly
import Data.Unit.UniversePolymorphic as Poly

infix 4 _<′_
_<′_ : List E → List E → Type (e ℓ⊔ ℓ₁ ℓ⊔ ℓ₂)
xs <′ []     = Poly.⊥
[] <′ y ∷ ys = Poly.⊤
x ∷ xs <′ y ∷ ys = (x < y) ⊎ ((x ≡ y) × (xs <′ ys))

infix 4 _≤′_
_≤′_ : List E → List E → Type (e ℓ⊔ ℓ₁ ℓ⊔ ℓ₂)
[]     ≤′ ys     = Poly.⊤
x ∷ xs ≤′ []     = Poly.⊥
x ∷ xs ≤′ y ∷ ys = (x < y) ⊎ ((x ≡ y) × (xs ≤′ ys))

<′-trans : Transitive _<′_
<′-trans {[]}     {y ∷ ys} {z ∷ zs} p q = Poly.tt
<′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inl p) (inl q) = inl (<-trans p q)
<′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inl p) (inr q) = inl (subst (_ <_) (fst q) p)
<′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inr p) (inl q) = inl (subst (_< _) (sym (fst p)) q)
<′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inr (p , ps)) (inr (q , qs)) = inr (p ; q , <′-trans ps qs)

≤′-trans : Transitive _≤′_
≤′-trans {[]} {ys} {zs} p q = Poly.tt
≤′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inl p) (inl q) = inl (<-trans p q)
≤′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inl p) (inr q) = inl (subst (_ <_) (fst q) p)
≤′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inr p) (inl q) = inl (subst (_< _) (sym (fst p)) q)
≤′-trans {x ∷ xs} {y ∷ ys} {z ∷ zs} (inr (p , ps)) (inr (q , qs)) = inr (p ; q , ≤′-trans ps qs)

≤′-antisym : Antisymmetric _≤′_
≤′-antisym {[]} {[]} p q = refl
≤′-antisym {x ∷ xs} {y ∷ ys} (inl p) (inl q) = ⊥-elim (asym p q)
≤′-antisym {x ∷ xs} {y ∷ ys} (inl p) (inr q) = ⊥-elim (irrefl (subst (_< _) (sym (fst q)) p))
≤′-antisym {x ∷ xs} {y ∷ ys} (inr p) (inl q) = ⊥-elim (irrefl (subst (_< _) (sym (fst p)) q))
≤′-antisym {x ∷ xs} {y ∷ ys} (inr (p , ps)) (inr (_ , qs)) = cong₂ _∷_ p (≤′-antisym ps qs)

≤′-refl : Reflexive _≤′_
≤′-refl {[]} = Poly.tt
≤′-refl {x ∷ xs} = inr (refl , ≤′-refl)

<′-asym : Asymmetric _<′_
<′-asym {x ∷ xs} {y ∷ ys} (inl p) (inl q) = asym p q
<′-asym {x ∷ xs} {y ∷ ys} (inl p) (inr q) = irrefl (subst (_< _) (sym (fst q)) p)
<′-asym {x ∷ xs} {y ∷ ys} (inr p) (inl q) = irrefl (subst (_< _) (sym (fst p)) q)
<′-asym {x ∷ xs} {y ∷ ys} (inr p) (inr q) = <′-asym (snd p) (snd q)

≮′⇒≥′ : ∀ {xs ys} → ¬ (xs <′ ys) → ys ≤′ xs
≮′⇒≥′ {xs} {[]} p = Poly.tt
≮′⇒≥′ {[]} {y ∷ ys} p = ⊥-elim (p _)
≮′⇒≥′ {x ∷ xs} {y ∷ ys} xs≮ys with compare x y
≮′⇒≥′ {x ∷ xs} {y ∷ ys} xs≮ys | lt x<y = ⊥-elim (xs≮ys (inl x<y))
≮′⇒≥′ {x ∷ xs} {y ∷ ys} xs≮ys | eq x≡y = inr (sym x≡y , ≮′⇒≥′ (xs≮ys ∘ inr ∘ _,_ x≡y))
≮′⇒≥′ {x ∷ xs} {y ∷ ys} xs≮ys | gt x>y = inl x>y

<′-conn : Connected _<′_
<′-conn xs≮ys ys≮xs = ≤′-antisym (≮′⇒≥′ ys≮xs) (≮′⇒≥′ xs≮ys)

<′-irrefl : Irreflexive _<′_
<′-irrefl {x ∷ xs} (inl x<x) = irrefl x<x
<′-irrefl {x ∷ xs} (inr xs<xs) = <′-irrefl (snd xs<xs)

≰′⇒>′ : ∀ {xs ys} → ¬ (xs ≤′ ys) → ys <′ xs
≰′⇒>′ {[]} xs≰ys = ⊥-elim (xs≰ys _)
≰′⇒>′ {x ∷ xs} {[]} xs≰ys = Poly.tt
≰′⇒>′ {x ∷ xs} {y ∷ ys} xs≰ys with compare x y
≰′⇒>′ {x ∷ xs} {y ∷ ys} xs≰ys | lt x<y = ⊥-elim (xs≰ys (inl x<y))
≰′⇒>′ {x ∷ xs} {y ∷ ys} xs≰ys | eq x≡y = inr (sym x≡y , ≰′⇒>′ (xs≰ys ∘ inr ∘ _,_ x≡y))
≰′⇒>′ {x ∷ xs} {y ∷ ys} xs≰ys | gt x>y = inl x>y

≮′-cons : ∀ {x y xs ys} → x ≡ y → ¬ (xs <′ ys) → ¬ (x ∷ xs <′ y ∷ ys)
≮′-cons x≡y xs≮ys (inl x<y) = irrefl (subst (_< _) x≡y x<y)
≮′-cons x≡y xs≮ys (inr (x≡y₁ , x∷xs<y∷ys)) = xs≮ys x∷xs<y∷ys

_<′?_ : Decidable _<′_
xs <′? [] = no (λ ())
[] <′? (y ∷ ys) = yes Poly.tt
(x ∷ xs) <′? (y ∷ ys) with compare x y
((x ∷ xs) <′? (y ∷ ys)) | lt x<y = yes (inl x<y)
((x ∷ xs) <′? (y ∷ ys)) | eq x≡y = map-dec (inr ∘ _,_ x≡y) (≮′-cons x≡y) (xs <′? ys)
((x ∷ xs) <′? (y ∷ ys)) | gt x>y = no (<′-asym (inl x>y))

listOrd : TotalOrder (List E) _ _
StrictPreorder._<_   (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder listOrd)) = _<′_
StrictPreorder.trans (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder listOrd)) = <′-trans
StrictPreorder.irrefl  (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder listOrd)) = <′-irrefl
StrictPartialOrder.conn (TotalOrder.strictPartialOrder listOrd) = <′-conn
Preorder._≤_   (PartialOrder.preorder (TotalOrder.partialOrder listOrd)) = _≤′_
Preorder.refl  (PartialOrder.preorder (TotalOrder.partialOrder listOrd)) = ≤′-refl
Preorder.trans (PartialOrder.preorder (TotalOrder.partialOrder listOrd)) = ≤′-trans
PartialOrder.antisym (TotalOrder.partialOrder listOrd) = ≤′-antisym
TotalOrder._<?_ listOrd = _<′?_
TotalOrder.≰⇒> listOrd = ≰′⇒>′
TotalOrder.≮⇒≥ listOrd = ≮′⇒≥′

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground