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

open import HoTT
open import homotopy.elims.SuspSmash

-- (ΣX)∧Y ≃ Σ(X∧Y)

module homotopy.SuspSmash where

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  private
    x₀ = pt X
    y₀ = pt Y

  Σ∧-out-smgluel-merid : ∀ (x : de⊙ X) →
    Square idp
           (ap (Susp-fmap (λ x' → smin x' y₀)) (merid x))
           (ap (λ sx → north) (merid x))
           (! (merid (smin x₀ y₀)))
  Σ∧-out-smgluel-merid x =
    ((SuspFmap.merid-β (λ x' → smin x' y₀) x ∙ ap merid (∧-norm-l x)) ∙v⊡
     tr-square (merid (smin x₀ y₀))) ⊡v∙
    ! (ap-cst north (merid x))

  module Σ∧OutSmgluel =
    SuspPathElim
      (Susp-fmap (λ x' → smin x' y₀))
      (λ sx → north)
      idp
      (! (merid (smin x₀ y₀)))
      Σ∧-out-smgluel-merid

  module Σ∧Out =
    SmashRec {X = ⊙Susp (de⊙ X)} {Y = Y}
      {C = Susp (X ∧ Y)}
      (λ sx y → Susp-fmap (λ x → smin x y) sx)
      north
      north
      Σ∧OutSmgluel.f
      (λ y → idp)

  Σ∧-out : ⊙Susp (de⊙ X) ∧ Y → Susp (X ∧ Y)
  Σ∧-out = Σ∧Out.f

  ⊙Σ∧-out : ⊙Susp (de⊙ X) ⊙∧ Y ⊙→ ⊙Susp (X ∧ Y)
  ⊙Σ∧-out = Σ∧-out , idp

  Σ∧-out-∧-norm-r : ∀ (y : de⊙ Y) →
    ap Σ∧-out (∧-norm-r y) == idp
  Σ∧-out-∧-norm-r y = Σ∧Out.∧-norm-r-β y

  ∧Σ-out-smgluer-merid : ∀ (y : de⊙ Y) →
    Square idp
           (ap (λ sy → Susp-fmap (smin x₀) sy) (merid y))
           (ap (λ sy → north) (merid y))
           (! (merid (smin x₀ y₀)))
  ∧Σ-out-smgluer-merid y =
    ((SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡
     tr-square (merid (smin x₀ y₀))) ⊡v∙
    ! (ap-cst north (merid y))

  module ∧ΣOutSmgluer =
    SuspPathElim
      (λ sy → Susp-fmap (smin x₀) sy)
      (λ sy → north)
      idp
      (! (merid (smin x₀ y₀)))
      ∧Σ-out-smgluer-merid

  module ∧ΣOut =
    SmashRec {X = X} {Y = ⊙Susp (de⊙ Y)}
      {C = Susp (X ∧ Y)}
      (λ x sy → Susp-fmap (smin x) sy)
      north
      north
      (λ x → idp)
      ∧ΣOutSmgluer.f

  ∧Σ-out : X ∧ ⊙Susp (de⊙ Y) → Susp (X ∧ Y)
  ∧Σ-out = ∧ΣOut.f

  ⊙∧Σ-out : X ⊙∧ ⊙Susp (de⊙ Y) ⊙→ ⊙Susp (X ∧ Y)
  ⊙∧Σ-out = ∧Σ-out , idp

  ∧Σ-out-∧-norm-l : ∀ (x : de⊙ X) →
    ap ∧Σ-out (∧-norm-l x) == idp
  ∧Σ-out-∧-norm-l x = ∧ΣOut.∧-norm-l-β x

  Σ∧-in-merid-smin : de⊙ X → de⊙ Y → pt (⊙Susp (de⊙ X) ⊙∧ Y) == pt (⊙Susp (de⊙ X) ⊙∧ Y)
  Σ∧-in-merid-smin x y = ↯ $
    smin north y₀
      =⟪ ! (∧-norm-r y) ⟫
    smin north y
      =⟪ ap (λ sx → smin sx y) (merid x ∙ ! (merid x₀)) ⟫
    smin north y
      =⟪ ∧-norm-r y ⟫
    smin north y₀ ∎∎

  Σ∧-in-merid-smgluel : ∀ (x : de⊙ X) → Σ∧-in-merid-smin x y₀ == idp
  Σ∧-in-merid-smgluel x = ↯ $
    Σ∧-in-merid-smin x y₀
      =⟪ ap (λ u → ! u ∙ ap (λ sx → smin sx y₀) (merid x ∙ ! (merid x₀)) ∙ u)
            (!-inv-r (smgluer y₀)) ⟫
    ap (λ sx → smin sx y₀) (merid x ∙ ! (merid x₀)) ∙ idp
      =⟪ ap (_∙ idp) $
         ap-null-homotopic (λ sx → smin sx y₀)
                           smgluel
                           (merid x ∙ ! (merid x₀)) ⟫
    (smgluel north ∙ ! (smgluel north)) ∙ idp
      =⟪ ap (_∙ idp) (!-inv-r (smgluel north)) ⟫
    idp ∎∎

  Σ∧-in-merid-smgluer : ∀ (y : de⊙ Y) → Σ∧-in-merid-smin x₀ y == idp
  Σ∧-in-merid-smgluer y = ↯ $
    Σ∧-in-merid-smin x₀ y
      =⟪ ap (λ p → ! (∧-norm-r y) ∙ ap (λ sx → smin sx y) p ∙ ∧-norm-r y)
            (!-inv-r (merid x₀)) ⟫
    ! (∧-norm-r y) ∙ ∧-norm-r y
      =⟪ !-inv-l (∧-norm-r y) ⟫
    idp ∎∎

  Σ∧-in : Susp (X ∧ Y) → ⊙Susp (de⊙ X) ∧ Y
  Σ∧-in =
    Susp-rec
      {C = ⊙Susp (de⊙ X) ∧ Y}
      (smin north y₀)
      (smin north y₀)
      (Smash-rec
        {C = smin north y₀ == smin north y₀}
        Σ∧-in-merid-smin
        idp
        idp
        Σ∧-in-merid-smgluel
        Σ∧-in-merid-smgluer)

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  private
    x₀ = pt X
    y₀ = pt Y

    ∧-swap-∧Σ-out-merid : ∀ (x : de⊙ X) (y : de⊙ Y) →
      ap (Susp-fmap (∧-swap X Y) ∘ Susp-fmap (smin x)) (merid y) =-=
      merid (smin y x)
    ∧-swap-∧Σ-out-merid x y =
      ap (Susp-fmap (∧-swap X Y) ∘ Susp-fmap (smin x)) (merid y)
        =⟪ ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x)) (merid y) ⟫
      ap (Susp-fmap (∧-swap X Y)) (ap (Susp-fmap (smin x)) (merid y))
        =⟪ ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x) y) ⟫
      ap (Susp-fmap (∧-swap X Y)) (merid (smin x y))
        =⟪ SuspFmap.merid-β (∧-swap X Y) (smin x y) ⟫
      merid (smin y x) ∎∎

    {- This is the same as `! (Susp-fmap-∘ (∧-swap X Y) (smin x))`, except that
       the merid case is easier to reason about, which we will do in
       `Σ∧-∧Σ-swap-smgluer-merid`. -}
    module Σ∧-∧Σ-swap-smin (x : de⊙ X) =
      SuspPathElim
        (Susp-fmap (∧-swap X Y) ∘ Susp-fmap (smin x))
        (Susp-fmap (λ y → smin y x))
        idp
        idp
        (λ y → ↯ (∧-swap-∧Σ-out-merid x y) ∙v⊡ vid-square ⊡v∙ ! (SuspFmap.merid-β (λ y' → smin y' x) y))

    ∧-swap-∧Σ-out-smgluel : ∀ x →
      ap (Susp-fmap (∧-swap X Y) ∘ ∧Σ-out X Y) (smgluel x) == idp
    ∧-swap-∧Σ-out-smgluel x =
      ap (Susp-fmap (∧-swap X Y) ∘ ∧Σ-out X Y) (smgluel x)
        =⟨ ap-∘ (Susp-fmap (∧-swap X Y)) (∧Σ-out X Y) (smgluel x) ⟩
      ap (Susp-fmap (∧-swap X Y)) (ap (∧Σ-out X Y) (smgluel x))
        =⟨ ap (ap (Susp-fmap (∧-swap X Y))) (∧ΣOut.smgluel-β X Y x) ⟩
      idp =∎

    Σ∧-out-∧-swap-smgluel : ∀ x →
      ap (Σ∧-out Y X ∘ ∧-swap X (⊙Susp (de⊙ Y))) (smgluel x) == idp
    Σ∧-out-∧-swap-smgluel x =
      ap (Σ∧-out Y X ∘ ∧-swap X (⊙Susp (de⊙ Y))) (smgluel x)
        =⟨ ap-∘ (Σ∧-out Y X) (∧-swap X (⊙Susp (de⊙ Y))) (smgluel x) ⟩
      ap (Σ∧-out Y X) (ap (∧-swap X (⊙Susp (de⊙ Y))) (smgluel x))
        =⟨ ap (ap (Σ∧-out Y X)) (SmashSwap.smgluel-β X (⊙Susp (de⊙ Y)) x) ⟩
      ap (Σ∧-out Y X) (∧-norm-r x)
        =⟨ Σ∧-out-∧-norm-r Y X x ⟩
      idp =∎

    ∧-swap-∧Σ-out-smgluer : ∀ sy →
      ap (Susp-fmap (∧-swap X Y) ∘ ∧Σ-out X Y) (smgluer sy) ==
      ap (Susp-fmap (∧-swap X Y)) (∧ΣOutSmgluer.f X Y sy)
    ∧-swap-∧Σ-out-smgluer sy =
      ap (Susp-fmap (∧-swap X Y) ∘ ∧Σ-out X Y) (smgluer sy)
        =⟨ ap-∘ (Susp-fmap (∧-swap X Y)) (∧Σ-out X Y) (smgluer sy) ⟩
      ap (Susp-fmap (∧-swap X Y)) (ap (∧Σ-out X Y) (smgluer sy))
        =⟨ ap (ap (Susp-fmap (∧-swap X Y))) (∧ΣOut.smgluer-β X Y sy) ⟩
      ap (Susp-fmap (∧-swap X Y)) (∧ΣOutSmgluer.f X Y sy) =∎

    Σ∧-out-∧-swap-smgluer : ∀ sy →
      ap (Σ∧-out Y X ∘ ∧-swap X (⊙Susp (de⊙ Y))) (smgluer sy) == Σ∧OutSmgluel.f Y X sy
    Σ∧-out-∧-swap-smgluer sy =
      ap (Σ∧-out Y X ∘ ∧-swap X (⊙Susp (de⊙ Y))) (smgluer sy)
        =⟨ ap-∘ (Σ∧-out Y X) (∧-swap X (⊙Susp (de⊙ Y))) (smgluer sy) ⟩
      ap (Σ∧-out Y X) (ap (∧-swap X (⊙Susp (de⊙ Y))) (smgluer sy))
        =⟨ ap (ap (Σ∧-out Y X)) (SmashSwap.smgluer-β X (⊙Susp (de⊙ Y)) sy) ⟩
      ap (Σ∧-out Y X) (∧-norm-l sy)
        =⟨ Σ∧Out.∧-norm-l-β Y X sy ⟩
      Σ∧OutSmgluel.f Y X sy ∙ idp
        =⟨ ∙-unit-r (Σ∧OutSmgluel.f Y X sy) ⟩
      Σ∧OutSmgluel.f Y X sy =∎

    Σ∧-∧Σ-swap-smgluer-merid : ∀ y →
      Cube ids
           ((ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
             ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
            ∙v⊡ vid-square)
           (natural-square (Σ∧-∧Σ-swap-smin.f x₀) (merid y))
           (natural-square (ap (Susp-fmap (∧-swap X Y)) ∘ ∧ΣOutSmgluer.f X Y) (merid y))
           (natural-square (Σ∧OutSmgluel.f Y X) (merid y))
           (natural-square (λ v → idp) (merid y))
    Σ∧-∧Σ-swap-smgluer-merid y =
      cube-shift-back (! (Σ∧-∧Σ-swap-smin.merid-square-β x₀ y)) $
      custom-cube-∙v⊡
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
        (↯ (∧-swap-∧Σ-out-merid x₀ y))
        (ap-cst north (merid y)) $
      cube-shift-top (! top-path) $
      custom-cube-⊡v∙
        (! (SuspFmap.merid-β (λ y' → smin y' x₀) y))
        (ap-cst north (merid y)) $
      cube-shift-front (! front-path) $
      cube-shift-bot (! bot-path) $
      custom-cube (ap merid (∧-norm-l y))
      where
      custom-cube-∙v⊡ :
        ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀  : a₀₀₀ == a₀₁₀}
        {p₋₀₀ : a₀₀₀ == a₁₀₀}
        {p₋₁₀ : a₀₁₀ == a₁₁₀}
        {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left
        {p₀₋₁ : a₀₀₁ == a₀₁₁}
        {p₋₀₁ p₋₀₁' : a₀₀₁ == a₁₀₁} (q₋₀₁ : p₋₀₁' == p₋₀₁)
        {p₋₁₁ : a₀₁₁ == a₁₁₁}
        {p₁₋₁ : a₁₀₁ == a₁₁₁}
        {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right
        {p₀₀₋ p₀₀₋' : a₀₀₀ == a₀₀₁} (q₀₀₋ : p₀₀₋' == p₀₀₋)
        {p₀₁₋ : a₀₁₀ == a₀₁₁}
        {p₁₀₋ p₁₀₋' : a₁₀₀ == a₁₀₁} (q₁₀₋ : p₁₀₋ == p₁₀₋')
        {p₁₁₋ : a₁₁₀ == a₁₁₁}
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋' p₁₀₋ p₋₀₁'} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
        → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ ((! q₀₀₋ ∙v⊡ sq₋₀₋ ⊡v∙ q₁₀₋) ⊡h∙ q₋₀₁) sq₋₁₋ (! q₁₀₋ ∙v⊡ sq₁₋₋)
        → Cube sq₋₋₀ (q₋₀₁ ∙v⊡ sq₋₋₁) (q₀₀₋ ∙v⊡ sq₀₋₋) sq₋₀₋ sq₋₁₋ sq₁₋₋
      custom-cube-∙v⊡ idp idp idp c = c
      custom-cube-⊡v∙ : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀  : a₀₀₀ == a₀₁₀}
        {p₋₀₀ : a₀₀₀ == a₁₀₀}
        {p₋₁₀ : a₀₁₀ == a₁₁₀}
        {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left
        {p₀₋₁ : a₀₀₁ == a₀₁₁}
        {p₋₀₁ : a₀₀₁ == a₁₀₁}
        {p₋₁₁ : a₀₁₁ == a₁₁₁}
        {p₁₋₁ : a₁₀₁ == a₁₁₁}
        {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right
        {p₀₀₋ : a₀₀₀ == a₀₀₁}
        {p₀₁₋ p₀₁₋' : a₀₁₀ == a₀₁₁} (q₀₁₋ : p₀₁₋ == p₀₁₋')
        {p₁₀₋ : a₁₀₀ == a₁₀₁}
        {p₁₁₋ p₁₁₋' : a₁₁₀ == a₁₁₁} (q₁₁₋ : p₁₁₋ == p₁₁₋')
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋' p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
        → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ (q₀₁₋ ∙v⊡ sq₋₁₋ ⊡v∙ q₁₁₋) (sq₁₋₋ ⊡v∙ q₁₁₋)
        → Cube sq₋₋₀ sq₋₋₁ (sq₀₋₋ ⊡v∙ q₀₁₋) sq₋₀₋ sq₋₁₋ sq₁₋₋
      custom-cube-⊡v∙ idp idp c = c
      custom-cube : ∀ {i} {A : Type i} {a₀ a₁ : A}
        {p q : a₀ == a₁} (r : p == q)
        → Cube ids
               vid-square
               vid-square
               (r ∙v⊡ tr-square q)
               (r ∙v⊡ tr-square q)
               ids
      custom-cube {p = idp} {q = .idp} r@idp = idc
      top-path :
        (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
         natural-square (ap (Susp-fmap (∧-swap X Y)) ∘ ∧ΣOutSmgluer.f X Y) (merid y) ⊡v∙
         ap-cst north (merid y)) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
        ==
        ap merid (∧-norm-l y) ∙v⊡ tr-square (merid (smin y₀ x₀))
      top-path =
        (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
         natural-square (ap (Susp-fmap (∧-swap X Y)) ∘ ∧ΣOutSmgluer.f X Y) (merid y) ⊡v∙
         ap-cst north (merid y)) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
                        u ⊡v∙
                        ap-cst north (merid y)) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             natural-square-ap (Susp-fmap (∧-swap X Y)) (∧ΣOutSmgluer.f X Y) (merid y) ⟩
        (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
         (ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ∙v⊡
          ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
          ∘-ap (Susp-fmap (∧-swap X Y)) (λ _ → north) (merid y)) ⊡v∙
         ap-cst north (merid y)) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
                        u) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             ∙v⊡-⊡v∙-comm
               (ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y))
               (ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
                ∘-ap (Susp-fmap (∧-swap X Y)) (λ _ → north) (merid y))
               (ap-cst north (merid y)) ⟩
        (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
         ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
         ∘-ap (Susp-fmap (∧-swap X Y)) (λ _ → north) (merid y) ⊡v∙
         ap-cst north (merid y)) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
                        ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ∙v⊡
                        u) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             ⊡v∙-assoc
               (ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)))
               (∘-ap (Susp-fmap (∧-swap X Y)) (λ _ → north) (merid y))
               (ap-cst north (merid y)) ⟩
        (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
         ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
         (∘-ap (Susp-fmap (∧-swap X Y)) (λ _ → north) (merid y) ∙ ap-cst north (merid y))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
                        ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ∙v⊡
                        ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
                        u) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             =ₛ-out $ ap-∘-cst-coh (Susp-fmap (∧-swap X Y)) north (merid y) ⟩
        (! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙v⊡
         ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
         ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → u ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $ ! $
             ∙v⊡-assoc
               (! (↯ (∧-swap-∧Σ-out-merid x₀ y)))
               (ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y))
               (ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
                ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⟩
        ((! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ∙
          ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y)) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
         ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (u ∙v⊡
                        ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
                        ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $ =ₛ-out $
             ! (↯ (∧-swap-∧Σ-out-merid x₀ y)) ◃∙
             ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ◃∎
               =ₛ⟨ 0 & 1 & !-∙-seq $
                   ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ◃∙
                   ↯ (tail (∧-swap-∧Σ-out-merid x₀ y)) ◃∎ ⟩
             ! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ◃∙
             ! (ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y)) ◃∙
             ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ◃∎
               =ₛ⟨ 1 & 2 & seq-!-inv-l (ap-∘ (Susp-fmap (∧-swap X Y)) (Susp-fmap (smin x₀)) (merid y) ◃∎) ⟩
             ! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ◃∎ ∎ₛ ⟩
        (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (natural-square (∧ΣOutSmgluer.f X Y) (merid y)) ⊡v∙
         ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
                        ap-square (Susp-fmap (∧-swap X Y)) u ⊡v∙
                        ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             ∧ΣOutSmgluer.merid-square-β X Y y ⟩
        (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (∧Σ-out-smgluer-merid X Y y) ⊡v∙
         ap (ap (Susp-fmap (∧-swap X Y))) (ap-cst north (merid y))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
                        u) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             ap-square-⊡v∙
               (Susp-fmap (∧-swap X Y))
               (∧Σ-out-smgluer-merid X Y y)
               (ap-cst north (merid y)) ⟩
        (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y))
                   (∧Σ-out-smgluer-merid X Y y ⊡v∙ ap-cst north (merid y))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
                        ap-square (Susp-fmap (∧-swap X Y)) u) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $
             ∧Σ-out-smgluer-merid X Y y ⊡v∙ ap-cst north (merid y)
               =⟨ ⊡v∙-assoc
                    ((SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡ tr-square (merid (smin x₀ y₀)))
                    (! (ap-cst north (merid y)))
                    (ap-cst north (merid y)) ⟩
             ((SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡
              tr-square (merid (smin x₀ y₀))) ⊡v∙
             (! (ap-cst north (merid y)) ∙ ap-cst north (merid y))
               =⟨ ap (((SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                       tr-square (merid (smin x₀ y₀))) ⊡v∙_) $
                  !-inv-l (ap-cst north (merid y)) ⟩
             (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡
             tr-square (merid (smin x₀ y₀)) =∎ ⟩
        (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y))
                   ((SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                    tr-square (merid (smin x₀ y₀)))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
                        u) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $ ! $
             ap-square-∙v⊡
               (Susp-fmap (∧-swap X Y))
               (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y))
               (tr-square (merid (smin x₀ y₀))) ⟩
        (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙v⊡
         ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀)))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (_⊡h∙ (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                       ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $ ! $
             ∙v⊡-assoc
               (! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))))
               (ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)))
               (ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀)))) ⟩
        ((! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ∙
          ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y))) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀)))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap (λ u → (u ∙v⊡
                        ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀)))) ⊡h∙
                       (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))) $ =ₛ-out $
             ! (↯ (tail (∧-swap-∧Σ-out-merid x₀ y))) ◃∙
             ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 0 & 1 & !-∙-seq (tail (∧-swap-∧Σ-out-merid x₀ y)) ⟩
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y)) ◃∙
             ! (ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y)) ◃∙
             ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y ∙ ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 2 & 1 &
                   ap-seq-∙ (ap (Susp-fmap (∧-swap X Y))) $
                            (SuspFmap.merid-β (smin x₀) y ◃∙ ap merid (∧-norm-r y) ◃∎) ⟩
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y)) ◃∙
             ! (ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y)) ◃∙
             ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y) ◃∙
             ap (ap (Susp-fmap (∧-swap X Y))) (ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 1 & 2 & seq-!-inv-l (ap (ap (Susp-fmap (∧-swap X Y))) (SuspFmap.merid-β (smin x₀) y) ◃∎) ⟩
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y)) ◃∙
             ap (ap (Susp-fmap (∧-swap X Y))) (ap merid (∧-norm-r y)) ◃∎
               =ₛ₁⟨ 1 & 1 & ∘-ap (ap (Susp-fmap (∧-swap X Y))) merid (∧-norm-r y) ⟩
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y)) ◃∙
             ap (ap (Susp-fmap (∧-swap X Y)) ∘ merid) (∧-norm-r y) ◃∎
               =ₛ⟨ !ₛ $ homotopy-naturality
                     (merid ∘ ∧-swap X Y)
                     (ap (Susp-fmap (∧-swap X Y)) ∘ merid)
                     (! ∘ SuspFmap.merid-β (∧-swap X Y))
                     (∧-norm-r y) ⟩
             ap (merid ∘ ∧-swap X Y) (∧-norm-r y) ◃∙
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)) ◃∎
               =ₛ₁⟨ 0 & 1 & ap-∘ merid (∧-swap X Y) (∧-norm-r y) ⟩
             ap merid (ap (∧-swap X Y) (∧-norm-r y)) ◃∙
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)) ◃∎
               =ₛ₁⟨ 0 & 1 & ap (ap merid) (∧-swap-norm-r-β X Y y) ⟩
             ap merid (∧-norm-l y) ◃∙
             ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)) ◃∎ ∎ₛ ⟩
        ((ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡
         ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀)))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ∙v⊡-⊡h∙-comm
               (ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
               (ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀))))
               (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
                ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ⟩
        (ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡
        ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀))) ⊡h∙
        (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
         ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
          =⟨ ap ((ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡_) $
             ! $ ⊡h∙-assoc
               (ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀))))
               (ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)))
               (ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ⟩
        (ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡
        ap-square (Susp-fmap (∧-swap X Y)) (tr-square (merid (smin x₀ y₀))) ⊡h∙
        ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ⊡h∙
        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))
          =⟨ ap (λ u → (ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡
                       u ⊡h∙
                       ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) $
             ap-tr-square (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ⟩
        (ap merid (∧-norm-l y) ∙ ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡
        tr-square (ap (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀))) ⊡h∙
        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))
          =⟨ ∙v⊡-assoc
               (ap merid (∧-norm-l y))
               (! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)))
               (tr-square (ap (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀))) ⊡h∙
                ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ⟩
        ap merid (∧-norm-l y) ∙v⊡
        ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)) ∙v⊡
        tr-square (ap (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀))) ⊡h∙
        ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))
          =⟨ ap (ap merid (∧-norm-l y) ∙v⊡_) $
             tr-square-∙v⊡-⊡h∙ (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀)) ⟩
        ap merid (∧-norm-l y) ∙v⊡ tr-square (merid (smin y₀ x₀)) =∎
      front-path :
        (! (ap-cst (north {A = Y ∧ X}) (merid y)) ∙v⊡
         natural-square (λ v → idp) (merid y)) ⊡v∙
        ap-cst north (merid y)
        ==
        ids
      front-path =
        (! (ap-cst (north {A = Y ∧ X}) (merid y)) ∙v⊡
         natural-square (λ v → idp) (merid y)) ⊡v∙
        ap-cst north (merid y)
          =⟨ ∙v⊡-⊡v∙-comm
               (! (ap-cst (north {A = Y ∧ X}) (merid y)))
               (natural-square (λ v → idp) (merid y))
               (ap-cst north (merid y)) ⟩
        ! (ap-cst (north {A = Y ∧ X}) (merid y)) ∙v⊡
        natural-square (λ v → idp) (merid y) ⊡v∙
        ap-cst north (merid y)
          =⟨ natural-square-cst
               north
               north
               (λ v → idp)
               (merid y) ⟩
        disc-to-square (ap (λ v → idp) (merid y))
          =⟨ ap disc-to-square (ap-cst idp (merid y)) ⟩
        ids =∎
      bot-path :
        ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡
        natural-square (Σ∧OutSmgluel.f Y X) (merid y) ⊡v∙
        ap-cst north (merid y)
        ==
        ap merid (∧-norm-l y) ∙v⊡ tr-square (merid (smin y₀ x₀))
      bot-path =
        ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡
        natural-square (Σ∧OutSmgluel.f Y X) (merid y) ⊡v∙
        ap-cst north (merid y)
          =⟨ ap (λ u → ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡ u ⊡v∙ ap-cst north (merid y)) $
             Σ∧OutSmgluel.merid-square-β Y X y ⟩
        ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡
        Σ∧-out-smgluel-merid Y X y ⊡v∙
        ap-cst north (merid y)
          =⟨ ap (! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡_) $
             ⊡v∙-assoc
               ((SuspFmap.merid-β (λ y' → smin y' x₀) y ∙ ap merid (∧-norm-l y)) ∙v⊡
                tr-square (merid (smin y₀ x₀)))
               (! (ap-cst north (merid y)))
               (ap-cst north (merid y)) ⟩
        ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡
        ((SuspFmap.merid-β (λ y' → smin y' x₀) y ∙ ap merid (∧-norm-l y)) ∙v⊡
         tr-square (merid (smin y₀ x₀))) ⊡v∙
        (! (ap-cst north (merid y)) ∙ ap-cst north (merid y))
          =⟨ ap (λ u → ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡
                       ((SuspFmap.merid-β (λ y' → smin y' x₀) y ∙ ap merid (∧-norm-l y)) ∙v⊡
                        tr-square (merid (smin y₀ x₀))) ⊡v∙
                       u) $
             !-inv-l (ap-cst north (merid y)) ⟩
        ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙v⊡
        ((SuspFmap.merid-β (λ y' → smin y' x₀) y ∙ ap merid (∧-norm-l y)) ∙v⊡
         tr-square (merid (smin y₀ x₀)))
          =⟨ ! $ ∙v⊡-assoc
               (! (SuspFmap.merid-β (λ y' → smin y' x₀) y))
               (SuspFmap.merid-β (λ y' → smin y' x₀) y ∙ ap merid (∧-norm-l y))
               (tr-square (merid (smin y₀ x₀))) ⟩
        (! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ∙
         SuspFmap.merid-β (λ y' → smin y' x₀) y ∙
         ap merid (∧-norm-l y)) ∙v⊡
        tr-square (merid (smin y₀ x₀))
          =⟨ ap (_∙v⊡ tr-square (merid (smin y₀ x₀))) $ =ₛ-out $
             ! (SuspFmap.merid-β (λ y' → smin y' x₀) y) ◃∙
             SuspFmap.merid-β (λ y' → smin y' x₀) y ◃∙
             ap merid (∧-norm-l y) ◃∎
               =ₛ⟨ 0 & 2 & seq-!-inv-l (SuspFmap.merid-β (λ y' → smin y' x₀) y ◃∎) ⟩
             ap merid (∧-norm-l y) ◃∎ ∎ₛ ⟩
        ap merid (∧-norm-l y) ∙v⊡ tr-square (merid (smin y₀ x₀)) =∎

    Σ∧-∧Σ-swap-smgluer : ∀ sy →
      Square (Σ∧-∧Σ-swap-smin.f x₀ sy)
             (ap (Susp-fmap (∧-swap X Y)) (∧ΣOutSmgluer.f X Y sy))
             (Σ∧OutSmgluel.f Y X sy)
             idp
    Σ∧-∧Σ-swap-smgluer =
      Susp-elim
        ids
        ((ap-! (Susp-fmap (∧-swap X Y)) (merid (smin x₀ y₀)) ∙
          ap ! (SuspFmap.merid-β (∧-swap X Y) (smin x₀ y₀))) ∙v⊡
         vid-square)
        (λ y → cube-to-↓-square (Σ∧-∧Σ-swap-smgluer-merid y))

  swap-∧Σ-out : Susp-fmap (∧-swap X Y) ∘ ∧Σ-out X Y
              ∼ Σ∧-out Y X ∘ ∧-swap X (⊙Susp (de⊙ Y))
  swap-∧Σ-out =
    Smash-Path-elim
      (Susp-fmap (∧-swap X Y) ∘ ∧Σ-out X Y)
      (Σ∧-out Y X ∘ ∧-swap X (⊙Susp (de⊙ Y)))
      Σ∧-∧Σ-swap-smin.f
      idp
      idp
      (λ x → ∧-swap-∧Σ-out-smgluel x ∙v⊡ ids ⊡v∙ ! (Σ∧-out-∧-swap-smgluel x))
      (λ sy → ∧-swap-∧Σ-out-smgluer sy ∙v⊡
              Σ∧-∧Σ-swap-smgluer sy ⊡v∙
              ! (Σ∧-out-∧-swap-smgluer sy))

  ⊙swap-∧Σ-out : ⊙Susp-fmap (∧-swap X Y) ◃⊙∘ ⊙∧Σ-out X Y ◃⊙idf
                 =⊙∘
                 ⊙Σ∧-out Y X ◃⊙∘ ⊙∧-swap X (⊙Susp (de⊙ Y)) ◃⊙idf
  ⊙swap-∧Σ-out = =⊙∘-in (⊙λ=' swap-∧Σ-out idp)

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙swap-Σ∧-out : ⊙Susp-fmap (∧-swap X Y) ◃⊙∘ ⊙Σ∧-out X Y ◃⊙idf
                 =⊙∘
                 ⊙∧Σ-out Y X ◃⊙∘ ⊙∧-swap (⊙Susp (de⊙ X)) Y ◃⊙idf
  ⊙swap-Σ∧-out =
    ⊙Susp-fmap (∧-swap X Y) ◃⊙∘ ⊙Σ∧-out X Y ◃⊙idf
      =⊙∘⟨ 2 & 0 & !⊙∘ $ ⊙∧-swap-inv (⊙Susp (de⊙ X)) Y ⟩
    ⊙Susp-fmap (∧-swap X Y) ◃⊙∘
    ⊙Σ∧-out X Y ◃⊙∘
    ⊙∧-swap Y (⊙Susp (de⊙ X)) ◃⊙∘
    ⊙∧-swap (⊙Susp (de⊙ X)) Y ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ (⊙swap-∧Σ-out Y X) ⟩
    ⊙Susp-fmap (∧-swap X Y) ◃⊙∘
    ⊙Susp-fmap (∧-swap Y X) ◃⊙∘
    ⊙∧Σ-out Y X ◃⊙∘
    ⊙∧-swap (⊙Susp (de⊙ X)) Y ◃⊙idf
      =⊙∘⟨ 0 & 2 & !⊙∘ $ =⊙∘-in {fs = ⊙Susp-fmap (∧-swap X Y ∘ ∧-swap Y X) ◃⊙idf} $
                   ⊙Susp-fmap-∘ (∧-swap X Y) (∧-swap Y X) ⟩
    ⊙Susp-fmap (∧-swap X Y ∘ ∧-swap Y X) ◃⊙∘
    ⊙∧Σ-out Y X ◃⊙∘
    ⊙∧-swap (⊙Susp (de⊙ X)) Y ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ap ⊙Susp-fmap (λ= (∧-swap-inv Y X)) ⟩
    ⊙Susp-fmap (idf _) ◃⊙∘
    ⊙∧Σ-out Y X ◃⊙∘
    ⊙∧-swap (⊙Susp (de⊙ X)) Y ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙Susp-fmap-idf (Y ∧ X) ⟩
    ⊙∧Σ-out Y X ◃⊙∘
    ⊙∧-swap (⊙Susp (de⊙ X)) Y ◃⊙idf ∎⊙∘

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.data:25 #-}
-- {-# OPTIONS -v tc.conv.coerce:0 -v tc.with:25 #-}

module FilterSub where

open import Common.Level
open import Common.Equality

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

data Bool : Set where
  true false : Bool

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

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

infixr 5 _∷_

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

data Any {a p} {A : Set a}
         (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

infix 4 _⊆_ _∈_

_∈_ : ∀ {a}{A : Set a} → A → List A → Set _
x ∈ xs = Any (_≡_ x) xs

_⊆_ : ∀ {a}{A : Set a} → List A → List A → Set _
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter p []       = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false =     filter p xs

filter-⊆ : ∀ {a} {A : Set a} (p : A → Bool) →
           (xs : List A) → filter p xs ⊆ xs
filter-⊆ _ []       = λ ()
filter-⊆ p (x ∷ xs) with p x | filter-⊆ p xs
... | false | hyp = there ∘ hyp
... | true  | hyp =
  λ { (here  eq)      → here eq
    ; (there ∈filter) → there (hyp ∈filter)
    }

ext: agda

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Powerset

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommAlgebra

open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base

open import Cubical.HITs.PropositionalTruncation

open Category
open CommAlgebraHoms

private
 variable
  ℓ ℓ' ℓ'' : Level

module _ (R : CommRing ℓ) where
  CommAlgebrasCategory : Category (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
  ob CommAlgebrasCategory       = CommAlgebra R _
  Hom[_,_] CommAlgebrasCategory = CommAlgebraHom
  id CommAlgebrasCategory {A}   = idCommAlgebraHom A
  _⋆_ CommAlgebrasCategory {A} {B} {C}     = compCommAlgebraHom A B C
  ⋆IdL CommAlgebrasCategory {A} {B}           = compIdCommAlgebraHom {A = A} {B}
  ⋆IdR CommAlgebrasCategory {A} {B}           = idCompCommAlgebraHom {A = A} {B}
  ⋆Assoc CommAlgebrasCategory {A} {B} {C} {D} = compAssocCommAlgebraHom {A = A} {B} {C} {D}
  isSetHom CommAlgebrasCategory               = isSetAlgebraHom _ _

module PreSheafFromUniversalProp (C : Category ℓ ℓ') (P : ob C → Type ℓ)
         {R : CommRing ℓ''} (𝓕 : Σ (ob C) P → CommAlgebra R ℓ'')
         (uniqueHom : ∀ x y → C [ fst x , fst y ] → isContr (CommAlgebraHom (𝓕 y) (𝓕 x)))
         where

 private
  ∥P∥ : ℙ (ob C)
  ∥P∥ x  = ∥ P x ∥ , isPropPropTrunc
  ΣC∥P∥Cat = ΣPropCat C ∥P∥

 𝓕UniqueEquiv : (x : ob C) (p q : P x) → isContr (CommAlgebraEquiv (𝓕 (x , p)) (𝓕 (x , q)))
 𝓕UniqueEquiv x = contrCommAlgebraHom→contrCommAlgebraEquiv (curry 𝓕 x) λ p q → uniqueHom _ _ (id C)

 theMap : (x : ob C) → ∥ P x ∥ → CommAlgebra R ℓ''
 theMap x = recPT→CommAlgebra (curry 𝓕 x) (λ p q → 𝓕UniqueEquiv x p q .fst)
                                         λ p q r → 𝓕UniqueEquiv x p r .snd _

 theAction : (x y : ob C) → C [ x , y ]
           → (p : ∥ P x ∥) (q : ∥ P y ∥) → isContr (CommAlgebraHom (theMap y q) (theMap x p))
 theAction _ _ f = elim2 (λ _ _ → isPropIsContr) λ _ _ → uniqueHom _ _ f

 open Functor
 universalPShf : Functor (ΣC∥P∥Cat ^op) (CommAlgebrasCategory {ℓ = ℓ''} R {ℓ' = ℓ''})
 F-ob universalPShf = uncurry theMap
 F-hom universalPShf {x = x} {y = y} f = theAction _ _ f (y .snd) (x. snd) .fst
 F-id universalPShf {x = x} = theAction (x .fst) (x .fst) (id C) (x .snd) (x .snd) .snd _
 F-seq universalPShf {x = x} {z = z} f g = theAction _ _ (g ⋆⟨ C ⟩ f) (z .snd) (x .snd) .snd _

max_stars_repo_name: FernandoLarrain/cubical


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

module Definition.Typed.RedSteps where

open import Definition.Untyped
open import Definition.Typed

-- Concatenation of type reduction closures
_⇨*_ : ∀ {Γ A B C r} → Γ ⊢ A ⇒* B ^ r → Γ ⊢ B ⇒* C ^ r → Γ ⊢ A ⇒* C ^ r
id ⊢B ⇨* B⇒C = B⇒C
(A⇒A′ ⇨ A′⇒B) ⇨* B⇒C = A⇒A′ ⇨ (A′⇒B ⇨* B⇒C)

-- Concatenation of term reduction closures
_⇨∷*_ : ∀ {Γ A t u v l} → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ u ⇒* v ∷ A ^ l → Γ ⊢ t ⇒* v ∷ A ^ l
id ⊢u ⇨∷* u⇒v = u⇒v
(t⇒t′ ⇨ t′⇒u) ⇨∷* u⇒v = t⇒t′ ⇨ (t′⇒u ⇨∷* u⇒v)

-- Conversion of reduction closures
conv* : ∀ {Γ A B t u l } → Γ ⊢ t ⇒* u ∷ A ^ l → Γ ⊢ A ≡ B ^ [ ! , l ] → Γ ⊢ t ⇒* u ∷ B ^ l
conv* (id x) A≡B = id (conv x A≡B)
conv* (x ⇨ d) A≡B = conv x A≡B ⇨ conv* d A≡B

conv:* : ∀ {Γ A B t u l } → Γ ⊢ t :⇒*: u ∷ A ^ l → Γ ⊢ A ≡ B ^ [ ! , l ] → Γ ⊢ t :⇒*: u ∷ B ^ l
conv:* [[ ⊢t , ⊢u , d ]] e = [[ (conv ⊢t e) , (conv ⊢u e) , (conv* d e) ]]

-- Universe of reduction closures
univ* : ∀ {Γ A B r l} → Γ ⊢ A ⇒* B ∷ (Univ r l) ^ next l → Γ ⊢ A ⇒* B ^ [ r , ι l ]
univ* (id x) = id (univ x)
univ* (x ⇨ A⇒B) = univ x ⇨ univ* A⇒B

-- Application substitution of reduction closures
app-subst* : ∀ {Γ A B t t′ a rA lA lB l} → Γ ⊢ t ⇒* t′ ∷ Π A ^ rA ° lA ▹ B ° lB ° l ^ ι l → Γ ⊢ a ∷ A ^ [ rA , ι lA ]
           → Γ ⊢ t ∘ a ^ l ⇒* t′ ∘ a ^ l ∷ B [ a ] ^ ι lB
app-subst* (id x) a₁ = id (x ∘ⱼ a₁)
app-subst* (x ⇨ t⇒t′) a₁ = app-subst x a₁ ⇨ app-subst* t⇒t′ a₁

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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
-}

import      LibraBFT.Impl.Types.BlockInfo             as BlockInfo
import      LibraBFT.Impl.Crypto.Crypto.Hash          as Hash
open import LibraBFT.ImplShared.Consensus.Types
open import Util.Prelude

module LibraBFT.Impl.Types.LedgerInfo where

mockGenesis : Maybe ValidatorSet → Either ErrLog LedgerInfo
mockGenesis mvs = LedgerInfo∙new <$> BlockInfo.mockGenesis mvs <*> pure Hash.valueZero


text:
open import Prelude
open import Nat
open import core
open import contexts

module lemmas-env where
  env-ctx-same-1 : ∀{Δ Σ' Γ E x} →
                     Δ , Σ' , Γ ⊢ E →
                     x # E →
                     x # Γ
  env-ctx-same-1 EnvId h = x#∅
  env-ctx-same-1 {x = x} (EnvInd {E = E} {x = x'} ctxcons _) x#E+
    with natEQ x x'
  ... | Inl refl = abort (x#E+ (_ , x,a∈Γ,,x,a {Γ = E}))
  ... | Inr x≠x'
    with env-ctx-same-1 ctxcons (x#Γ+→x#Γ {Γ = E} x#E+)
  ... | x#Γ = x#Γ→x#Γ+ x≠x' x#Γ

  env-ctx-same-2 : ∀{Δ Σ' Γ E x} →
                     Δ , Σ' , Γ ⊢ E →
                     x # Γ →
                     x # E
  env-ctx-same-2 EnvId h = x#∅
  env-ctx-same-2 {x = x} (EnvInd {Γ = Γ} {x = x'} ctxcons _) x#Γ+
    with natEQ x x'
  ... | Inl refl = abort (x#Γ+ (_ , x,a∈Γ,,x,a {Γ = Γ}))
  ... | Inr x≠x'
    with env-ctx-same-2 ctxcons (x#Γ+→x#Γ {Γ = Γ} x#Γ+)
  ... | x#E = x#Γ→x#Γ+ x≠x' x#E

  env-all-Γ : ∀{Δ Σ' Γ E x τ} →
                Δ , Σ' , Γ ⊢ E →
                (x , τ) ∈ Γ →
                Σ[ r ∈ result ] ((x , r) ∈ E ∧ Δ , Σ' ⊢ r ·: τ)
  env-all-Γ EnvId x∈Γ = abort (x#∅ (_ , x∈Γ))
  env-all-Γ {x = x} (EnvInd {Γ = Γ} {E} {x'} ctxcons ta) x∈Γ
    with natEQ x x'
  ... | Inl refl
          rewrite ctxunicity x∈Γ (x,a∈Γ,,x,a {Γ = Γ})
            = _ , x,a∈Γ,,x,a {Γ = E} , ta
  ... | Inr x≠x'
    with env-all-Γ ctxcons (x∈Γ+→x∈Γ {Γ = Γ} x≠x' x∈Γ)
  ... | _ , x∈E , ta-rec = _ , x∈Γ→x∈Γ+ x≠x' x∈E , ta-rec

  env-all-E : ∀{Δ Σ' Γ E x r} →
                Δ , Σ' , Γ ⊢ E →
                (x , r) ∈ E →
                Σ[ τ ∈ typ ] ((x , τ) ∈ Γ ∧ Δ , Σ' ⊢ r ·: τ)
  env-all-E EnvId x∈E = abort (x#∅ (_ , x∈E))
  env-all-E {x = x} (EnvInd {Γ = Γ} {E} {x'} ctxcons ta) x∈E
    with natEQ x x'
  ... | Inl refl
          rewrite ctxunicity x∈E (x,a∈Γ,,x,a {Γ = E})
            = _ , x,a∈Γ,,x,a {Γ = Γ} , ta
  ... | Inr x≠x'
    with env-all-E ctxcons (x∈Γ+→x∈Γ {Γ = E} x≠x' x∈E)
  ... | _ , x∈Γ , ta-rec = _ , x∈Γ→x∈Γ+ x≠x' x∈Γ , ta-rec

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


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

open import Level
open import Ordinals
module OPair {n : Level } (O : Ordinals {n})   where

open import zf
open import logic
import OD
import ODUtil
import OrdUtil

open import Relation.Nullary
open import Relation.Binary
open import Data.Empty
open import Relation.Binary
open import Relation.Binary.Core
open import  Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )

open OD O
open OD.OD
open OD.HOD
open ODAxiom odAxiom

open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

open _∧_
open _∨_
open Bool

open _==_

<_,_> : (x y : HOD) → HOD
< x , y > = (x , x ) , (x , y )

exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z
    left (case1 t) = case2 t
    left (case2 t) = case1 t
    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z
    right (case1 t) = case2 t
    right (case2 t) = case1 t

ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )

od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )

eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
eq-prod refl refl = refl

xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
xx=zy→x=y {x} {y} eq with trio< (& x) (& y)
xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl)
xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {& y} (case2 refl)
xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )

prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
    lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq )  where
        lemma3 : ( x , x ) =h= ( y , z )
        lemma3 = ==-trans eq exg-pair
    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
    lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
    lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
    ... | refl with lemma2 (==-sym eq )
    ... | refl = refl
    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
    lemmax : x ≡ x'
    lemmax with eq→ eq {& (x , x)} (case1 refl)
    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
    ... | refl = lemma1 (ord→== s )
    lemmay : y ≡ y'
    lemmay with lemmax
    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
    ... | eq1 = lemma4 (ord→== (cong (λ  k → & k )  eq1 ))

--
-- unlike ordered pair, ZFProduct is not a HOD

data ord-pair : (p : Ordinal) → Set n where
   pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )

ZFProduct : OD
ZFProduct = record { def = λ x → ord-pair x }

-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
-- eq-pair refl refl = HE.refl

pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
pi1 ( pair x y) = x

π1 : { p : HOD } → def ZFProduct (& p) → HOD
π1 lt = * (pi1 lt )

pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
pi2 ( pair x y ) = y

π2 : { p : HOD } → def ZFProduct (& p) → HOD
π2 lt = * (pi2 lt )

op-cons :  { ox oy  : Ordinal } → def ZFProduct (& ( < * ox , * oy >   ))
op-cons {ox} {oy} = pair ox oy

def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
def-subst df refl refl = df

p-cons :  ( x y  : HOD ) → def ZFProduct (& ( < x , y >))
p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl (
   let open ≡-Reasoning in begin
       & < * (& x) , * (& y) >
   ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
       & < x , y >
   ∎ )

op-iso :  { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
op-iso (pair ox oy) = refl

p-iso :  { x  : HOD } → (p : def ZFProduct (&  x) ) → < π1 p , π2 p > ≡ x
p-iso {x} p = ord≡→≡ (op-iso p)

p-pi1 :  { x y : HOD } → (p : def ZFProduct (&  < x , y >) ) →  π1 p ≡ x
p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))

p-pi2 :  { x y : HOD } → (p : def ZFProduct (&  < x , y >) ) →  π2 p ≡ y
p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))

ω-pair :  {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m
ω-pair lx ly = next< (omax<nx lx ly ) ho<

ω-opair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & < x , y > o< next m
ω-opair {x} {y} {m} lx ly = lemma0 where
    lemma0 : & < x , y > o< next m
    lemma0 = osucprev (begin
         osuc (& < x , y >)
       <⟨ osuc<nx ho< ⟩
         next (omax (& (x , x)) (& (x , y)))
       ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
         next (osuc (& (x , y)))
       ≡⟨ sym (nexto≡) ⟩
         next (& (x , y))
       ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩
         next m
       ∎ ) where
          open o≤-Reasoning O

_⊗_ : (A B : HOD) → HOD
A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))

product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >)))
             ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where
    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
    lemma1 = replacement← B b B∋b
    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
    lemma2 = replacement← A a A∋a

x<nextA : {A x : HOD} → A ∋ x →  & x o< next (odmax A)
x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<

A<Bnext : {A B x : HOD} → & A o< & B → A ∋ x → & x o< next (odmax B)
A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
          osuc (& x)
       <⟨ osucc (c<→o< A∋x) ⟩
          osuc (& A)
       <⟨ osucc lt ⟩
          osuc (& B)
       <⟨ osuc<nx ho<  ⟩
          next (odmax B)
       ∎ ) where open o≤-Reasoning O

ZFP  : (A B : HOD) → HOD
ZFP  A B = record { od = record { def = λ x → ord-pair x ∧ ((p : ord-pair x ) → odef A (pi1 p) ∧ odef B (pi2 p) )} ;
        odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px }
   where
       lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (next (odmax A)) (next (odmax B))
       lemma y lt with proj1 lt
       lemma p lt | pair x y with trio< (& A) (& B)
       lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym &iso)
           (proj1 (proj2 lt (pair x y))))) (lemma1 (proj2 (proj2 lt (pair x y))))) (omax-y _ _ ) where
               lemma1 : odef B y → & (* y) o< next (HOD.odmax B)
               lemma1 lt = x<nextA {B} (d→∋ B lt)
       lemma p lt | pair x y | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) lemma2 ) (omax-x _ _ ) where
                lemma2 :  & (* y) o< next (HOD.odmax A)
                lemma2 = ordtrans ( subst (λ k → & (* y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
       lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair  (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
           (A<Bnext c (subst (λ k → odef B k ) (sym &iso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ )

ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
ZFP⊆⊗ {A} {B} {px} ⟪ (pair x y) ,  p2 ⟫ = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))

-- axiom of choice required
-- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (& x)
-- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (& k )) {!!} op-cons

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
module PreludeString where
import RTP -- magic module

import PreludeList
open   PreludeList using (List)

open import AlonzoPrelude

infixr 50 _++_

private
    primitive
      primStringAppend	 : String -> String -> String
      -- primStringReverse  : String -> String
      primStringToList	 : String -> List Char
      primStringFromList : List Char -> String

_++_     = primStringAppend
reverseString = RTP.primStringReverse

toList : String -> List Char
toList = primStringToList

fromList : List Char -> String
fromList = primStringFromList

-- toList   = RTP.primStringToList
-- fromList = RTP.primStringFromList

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- ----------------------------------------------------------------------
-- The Agda Descriptor Library
--
-- (Closed) Sets
-- ----------------------------------------------------------------------

module Data.Set where

open import Data.Empty using (⊥)
open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ)
open import Data.Product using (Σ)
open import Data.Unit using (⊤)

open import Data.Desc using (Desc; μ; _##_; _⟶_; Π)

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- ----------------------------------------------------------------------
-- Definition
--
-- A `Desc is a closed dependent type theory of
-- strictly positive functors : Set/A → Set/A
--
-- A `Set is a open dependent type theory of
-- the Agda model
--
-- To ensure a closed universe, we use
-- induction recursion.

data `Set : Set
⟦_⟧ : `Set → Set

private
  variable
    A : `Set

data `Desc (A : `Set) : Set
⟪_⟫ : `Desc A → Desc ⟦ A ⟧

data `Set where
  `Fin : ℕ → `Set
  `Σ `Π : (B : `Set) → (⟦ B ⟧ → `Set) → `Set
  `μ : `Desc A → ⟦ A ⟧ → `Set

⟦ `Fin n ⟧ = Fin n
⟦ `Σ A B ⟧ = Σ ⟦ A ⟧ (λ a → ⟦ B a ⟧ )
⟦ `Π A B ⟧ = (a : ⟦ A ⟧) → ⟦ B a ⟧
⟦ `μ d a ⟧ = μ ⟪ d ⟫ a

infixr 6 _⟶_

data `Desc A where
  `Π : (B : `Set) → (⟦ B ⟧ → `Desc A) → `Desc A
  _⟶_ : `Desc A → `Desc A → `Desc A
  _`##_ : (`Set → `Set) → ⟦ A ⟧ → `Desc A

⟪ `Π B d ⟫ = Π ⟦ B ⟧ (λ b → ⟪ d b ⟫)
⟪ d₁ ⟶ d₂ ⟫ = ⟪ d₁ ⟫ ⟶ ⟪ d₂ ⟫
⟪ f `## a ⟫ = {!   !} ## a

-- ----------------------------------------------------------------------
-- Example (Basic)

-- `⊤ : `Set
-- `⊤ = `Fin 1

-- `tt : ⟦ `⊤ ⟧
-- `tt = zero

-- `const : `Set → `Desc `⊤
-- `const A = `Π A λ _ → `# `tt

-- _`≡_ : ⟦ A ⟧ → ⟦ A ⟧ → `Set
-- x `≡ y = `μ (`# x) y

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

-- pattern nil = zero
-- pattern cons = (suc zero)

-- TODO: First order isomorphisms

-- _ : ⟦ zero `≡ zero ⟧
-- _ = {! refl  !}

-- ListD : `Set → `Desc `⊤
-- ListD A = `Π (`Fin 2)
--   λ{ nil → `# `tt
--    ; cons → `const A ⟶ `# `tt ⟶ `# `tt }

-- `List : `Set → `Set
-- `List A = `μ (ListD A) `tt

-- RoseD : `Set → `Desc `⊤
-- RoseD A = `const A ⟶ `List $ (`# `tt) ⟶ `# `tt

-- _#_ : (Set → Set) → A → Desc A
--
-- Computional:
-- f (X a)
--
-- Propositional:
-- f (a′ ≡ a)

max_stars_repo_name: johnyob/agda-desc

max_issues_repo_name: johnyob/agda-desc

max_forks_repo_name: johnyob/agda-desc


text:
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

module Common.Level where

postulate
  Level : Set
  lzero : Level
  lsuc  : (i : Level) → Level
  _⊔_   : Level -> Level -> Level

{-# IMPORT Common.FFI #-}
{-# COMPILED_TYPE Level Common.FFI.Level #-}
{-# COMPILED lzero Common.FFI.Zero #-}
{-# COMPILED lsuc Common.FFI.Suc #-}

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}
{-# BUILTIN LEVELMAX  _⊔_ #-}

infixl 6 _⊔_

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

open import Labelled-transition-system

-- Note that the module parameter is explicit. If the LTS is not given
-- explicitly, then the use of _[ μ ]⟶_ in the instances below can
-- make it hard for Agda to infer what instance to use.

module Labelled-transition-system.Equational-reasoning-instances
         {ℓ} (lts : LTS ℓ) where

open import Prelude

open import Equational-reasoning

open LTS lts

private

  -- Converts one kind of proof of silence to another kind.

  get : ∀ {μ} → T (silent? μ) → Silent μ
  get {μ} _  with silent? μ
  get {μ} () | no _
  get {μ} _  | yes s = s

instance

  convert⟶ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⟶_
  convert⟶ = is-convertible id

  convert⟶⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⟶_ _⇒_
  convert⟶⇒ {s = s} = is-convertible (⟶→⇒ (get s))

  convert⟶[]⇒ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⇒_
  convert⟶[]⇒ = is-convertible ⟶→[]⇒

  convert⟶⇒̂ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⇒̂_
  convert⟶⇒̂ = is-convertible ⟶→⇒̂

  convert⟶⟶̂ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⟶̂_
  convert⟶⟶̂ = is-convertible ⟶→⟶̂

  convert⇒ : Convertible _⇒_ _⇒_
  convert⇒ = is-convertible id

  convert⇒⇒̂ : ∀ {μ} {s : T (silent? μ)} → Convertible _⇒_ _[ μ ]⇒̂_
  convert⇒⇒̂ {s = s} = is-convertible (silent (get s))

  convert[]⇒ : ∀ {μ} → Convertible _[ μ ]⇒_ _[ μ ]⇒_
  convert[]⇒ = is-convertible id

  convert[]⇒⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⇒_ _⇒_
  convert[]⇒⇒ {s = s} = is-convertible ([]⇒→⇒ (get s))

  convert[]⇒⇒̂ : ∀ {μ} → Convertible _[ μ ]⇒_ _[ μ ]⇒̂_
  convert[]⇒⇒̂ = is-convertible ⇒→⇒̂

  convert⇒̂ : ∀ {μ} → Convertible _[ μ ]⇒̂_ _[ μ ]⇒̂_
  convert⇒̂ = is-convertible id

  convert⇒̂⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⇒̂_ _⇒_
  convert⇒̂⇒ {s = s} = is-convertible (⇒̂→⇒ (get s))

  convert⇒̂[]⇒ : ∀ {μ} {¬s : if (silent? μ) then ⊥ else ⊤} →
                Convertible _[ μ ]⇒̂_ _[ μ ]⇒_
  convert⇒̂[]⇒ {μ}       with silent? μ
  convert⇒̂[]⇒ {¬s = ()} | yes _
  convert⇒̂[]⇒           | no ¬s = is-convertible (⇒̂→[]⇒ ¬s)

  convert⟶̂ : ∀ {μ} → Convertible _[ μ ]⟶̂_ _[ μ ]⟶̂_
  convert⟶̂ = is-convertible id

  convert⟶̂⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⟶̂_ _⇒_
  convert⟶̂⇒ {s = s} = is-convertible (⟶̂→⇒ (get s))

  convert⟶̂⇒̂ : ∀ {μ} → Convertible _[ μ ]⟶̂_ _[ μ ]⇒̂_
  convert⟶̂⇒̂ = is-convertible ⟶̂→⇒̂

  reflexive⇒ : Reflexive _⇒_
  reflexive⇒ = is-reflexive done

  reflexive⟶̂ : ∀ {μ} {s : T (silent? μ)} → Reflexive _[ μ ]⟶̂_
  reflexive⟶̂ {s = s} = is-reflexive (done (get s))

  reflexive⇒̂ : ∀ {μ} {s : T (silent? μ)} → Reflexive _[ μ ]⇒̂_
  reflexive⇒̂ {s = s} = is-reflexive (silent (get s) done)

  trans⇒ : Transitive _⇒_ _⇒_
  trans⇒ = is-transitive ⇒-transitive

  trans⟶⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive _[ μ ]⟶_ _⇒_
  trans⟶⇒ {s = s} = is-transitive (⇒-transitive ∘ ⟶→⇒ (get s))

  trans⇒̂⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive _[ μ ]⇒̂_ _⇒_
  trans⇒̂⇒ {s = s} = is-transitive (⇒-transitive ∘ ⇒̂→⇒ (get s))

  trans⟶̂⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive _[ μ ]⟶̂_ _⇒_
  trans⟶̂⇒ {s = s} = is-transitive (⇒-transitive ∘ ⟶̂→⇒ (get s))

  trans⇒[]⇒ : ∀ {μ} → Transitive _⇒_ _[ μ ]⇒_
  trans⇒[]⇒ = is-transitive ⇒[]⇒-transitive

  trans⟶[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
              Transitive _[ μ′ ]⟶_ _[ μ ]⇒_
  trans⟶[]⇒ {s = s} = is-transitive (⇒[]⇒-transitive ∘ ⟶→⇒ (get s))

  trans[]⇒[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
                Transitive _[ μ′ ]⇒_ _[ μ ]⇒_
  trans[]⇒[]⇒ {s = s} = is-transitive (⇒[]⇒-transitive ∘ []⇒→⇒ (get s))

  trans⟶̂[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
              Transitive _[ μ′ ]⟶̂_ _[ μ ]⇒_
  trans⟶̂[]⇒ {s = s} = is-transitive (⇒[]⇒-transitive ∘ ⟶̂→⇒ (get s))

  trans⇒⇒̂ : ∀ {μ} → Transitive _⇒_ _[ μ ]⇒̂_
  trans⇒⇒̂ = is-transitive ⇒⇒̂-transitive

  trans⟶⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
              Transitive _[ μ′ ]⟶_ _[ μ ]⇒̂_
  trans⟶⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ ⟶→⇒ (get s))

  trans[]⇒⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
                Transitive _[ μ′ ]⇒_ _[ μ ]⇒̂_
  trans[]⇒⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ []⇒→⇒ (get s))

  trans[]⇒̂⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
              Transitive _[ μ′ ]⇒̂_ _[ μ ]⇒̂_
  trans[]⇒̂⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ ⇒̂→⇒ (get s))

  trans⟶̂⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
              Transitive _[ μ′ ]⟶̂_ _[ μ ]⇒̂_
  trans⟶̂⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ ⟶̂→⇒ (get s))

  trans′⇒⟶ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⟶_
  trans′⇒⟶ {s = s} =
    is-transitive (flip (flip ⇒-transitive ∘ ⟶→⇒ (get s)))

  trans′⇒[]⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⇒_
  trans′⇒[]⇒ {s = s} =
    is-transitive (flip (flip ⇒-transitive ∘ []⇒→⇒ (get s)))

  trans′⇒⇒̂ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⇒̂_
  trans′⇒⇒̂ {s = s} =
    is-transitive (flip (flip ⇒-transitive ∘ ⇒̂→⇒ (get s)))

  trans′⇒⟶̂ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⟶̂_
  trans′⇒⟶̂ {s = s} =
    is-transitive (flip (flip ⇒-transitive ∘ ⟶̂→⇒ (get s)))

  trans′[]⇒⟶ : ∀ {μ μ′} {s : T (silent? μ′)} →
               Transitive′ _[ μ ]⇒_ _[ μ′ ]⟶_
  trans′[]⇒⟶ {s = s} =
    is-transitive (flip (flip []⇒⇒-transitive ∘ ⟶→⇒ (get s)))

  trans′[]⇒⇒ : ∀ {μ} → Transitive′ _[ μ ]⇒_ _⇒_
  trans′[]⇒⇒ = is-transitive []⇒⇒-transitive

  trans′[]⇒[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
                 Transitive′ _[ μ ]⇒_ _[ μ′ ]⇒_
  trans′[]⇒[]⇒ {s = s} =
    is-transitive (flip (flip []⇒⇒-transitive ∘ []⇒→⇒ (get s)))

  trans′[]⇒[]⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
                 Transitive′ _[ μ ]⇒_ _[ μ′ ]⇒̂_
  trans′[]⇒[]⇒̂ {s = s} =
    is-transitive (flip (flip []⇒⇒-transitive ∘ ⇒̂→⇒ (get s)))

  trans′[]⇒⟶̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
               Transitive′ _[ μ ]⇒_ _[ μ′ ]⟶̂_
  trans′[]⇒⟶̂ {s = s} =
    is-transitive (flip (flip []⇒⇒-transitive ∘ ⟶̂→⇒ (get s)))

  trans′⇒̂⟶ : ∀ {μ μ′} {s : T (silent? μ′)} →
             Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⟶_
  trans′⇒̂⟶ {s = s} =
    is-transitive (flip (flip ⇒̂⇒-transitive ∘ ⟶→⇒ (get s)))

  trans′⇒̂⇒ : ∀ {μ} → Transitive′ _[ μ ]⇒̂_ _⇒_
  trans′⇒̂⇒ = is-transitive ⇒̂⇒-transitive

  trans′⇒̂[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
               Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⇒_
  trans′⇒̂[]⇒ {s = s} =
    is-transitive (flip (flip ⇒̂⇒-transitive ∘ []⇒→⇒ (get s)))

  trans′⇒̂⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
             Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⇒̂_
  trans′⇒̂⇒̂ {s = s} =
    is-transitive (flip (flip ⇒̂⇒-transitive ∘ ⇒̂→⇒ (get s)))

  trans′⇒̂⟶̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
             Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⟶̂_
  trans′⇒̂⟶̂ {s = s} =
    is-transitive (flip (flip ⇒̂⇒-transitive ∘ ⟶̂→⇒ (get s)))

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.ConsensusProvider as ConsensusProvider
import      LibraBFT.Impl.IO.OBM.GenKeyFile           as GenKeyFile
import      LibraBFT.Impl.IO.OBM.ObmNeedFetch         as ObmNeedFetch
import      LibraBFT.Impl.Types.ValidatorSigner       as ValidatorSigner
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.PKCS
open import Util.Prelude

module LibraBFT.Impl.IO.OBM.Start where

{-
This only does the initialization steps from the Haskell version.
If initialization succeeds, it returns
- the EpochManager (for all epochs)
  - note: this contains the initialized RoundManager for the current epoch (i.e., Epoch 0)
- any output from the RoundManager produced during initialization

The only output is (with info logging removed):

-- only the leader of round 1 will broadcast a proposal
BroadcastProposal; [ ... peer addresses ... ];
                   (ProposalMsg
                     (B 7194dca (BD 1 1 (Prop ("TX/1/1")) ...)) -- proposed block
                     (SI (hqc c66a132) (hcc N) (htc (TC N))))   -- SyncInfo

The Haskell code, after initialization, hooks up the communication channels and sockets
and starts threads that handle them.  One of the threads is given to
EpochManager.obmStartLoop to get input and pass it through the EpochManager
and then (usually) on to the RoundMnager.

TODO-3: Replace 'Handle.initRM' with the initialized RoundManager obtained
through the following 'startViaConsensusProvider'.
TODO-3: Figure out how to handle the initial BroadcastProposal.
-}
module startViaConsensusProvider-ed
  (now   : Instant)
  (nfl   : GenKeyFile.NfLiwsVsVvPe)
  (txTDS : TxTypeDependentStuffForNetwork)
  where
    step₁ : (NodeConfig × OnChainConfigPayload × LedgerInfoWithSignatures × SK × ProposerElection)
          → EitherD ErrLog (EpochManager × List Output)

    step₀ : EitherD ErrLog (EpochManager × List Output)
    step₀ = do
      let (nf , liws , vs , vv , pe) = nfl
      (nc , occp , liws , sk , pe) ← ConsensusProvider.obmInitialData-ed-abs (nf , liws , vs , vv , pe)
      step₁ (nc , occp , liws , sk , pe)
    step₁ (nc , occp , liws' , sk , _) =
      ConsensusProvider.startConsensus-ed-abs
        nc now occp liws' sk
        (ObmNeedFetch∙new {- newNetwork -stps'-})
        (txTDS ^∙ ttdsnProposalGenerator) (txTDS ^∙ ttdsnStateComputer)

abstract
  startViaConsensusProvider-ed-abs = startViaConsensusProvider-ed.step₀
  startViaConsensusProvider-ed-abs-≡ : startViaConsensusProvider-ed-abs ≡ startViaConsensusProvider-ed.step₀
  startViaConsensusProvider-ed-abs-≡ = refl


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_; dropWhile)
open import Data.Char using (Char)
open import Data.Bool using (Bool; true; false)
import Data.Char as Char using (_≟_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)

data Head {A : Set} (P : A → Bool) : List A → Set where
  head : ∀ (c : A) (s : List A) → P c ≡ true → Head P (c ∷ s)

prime : Char
prime = '′'

isPrime : Char → Bool
isPrime c = ⌊ c Char.≟ prime ⌋

head-lemma : ∀ (s : List Char) → ¬ Head isPrime (dropWhile isPrime s)
head-lemma [] = λ()
head-lemma (c ∷ s) with isPrime c
...                   | true       =  head-lemma s
...                   | false      =  ¬h
  where
  ¬h : ¬ Head isPrime (c ∷ s)
  ¬h (head c s eqn′) = {!!}

{-
Goal: ⊥
————————————————————————————————————————————————————————————
s    : List Char
c    : Char
eqn′ : ⌊ (c Char.≟ '′' | .Agda.Builtin.Char.primCharEquality c '′')
       ⌋
       ≡ true
s    : List Char
c    : Char
-}


text:
------------------------------------------------------------------------------
-- A proof that is rejected using the --without-K option
------------------------------------------------------------------------------

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

module Lists where

open import FOTC.Base
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Cons
open import FOTC.Data.List.WF-Relation.LT-Length

------------------------------------------------------------------------------
-- LTC → LTL.

-- 25 April 2014. The proof is accepted using Cockx's --without-K
-- implementation.
LTC→LTL : ∀ {xs ys} → List xs → LTC xs ys → LTL xs ys
LTC→LTL Lxs (x , refl) = lg-x<lg-x∷xs x Lxs

LTC→LTL' : ∀ {xs ys} → List xs → LTC xs ys → LTL xs ys
LTC→LTL' {xs} {ys} Lxs (x , h) =
  subst (λ ys' → length xs < length ys')
        (sym h)
        (lg-x<lg-x∷xs x Lxs)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Data.Fin.Properties.Extra where

open import Data.Fin hiding (_≤_)
open import Data.Nat
open import Data.Nat.Properties

open import Relation.Binary.PropositionalEquality

inject≤-trans : ∀ {l m n} i (p : l ≤ m)(q : m ≤ n) → inject≤ (inject≤ i p) q ≡ inject≤ i (≤-trans p q)
inject≤-trans () z≤n q
inject≤-trans zero (s≤s p) (s≤s q) = refl
inject≤-trans (suc i) (s≤s p) (s≤s q) = cong suc (inject≤-trans i p q)


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Comma.Functors where

open import Categories.Category
open import Categories.Functor renaming (_∘_ to _∘F_)
open import Categories.FunctorCategory renaming (Functors to [_⇒_])
open import Categories.NaturalTransformation using (module NaturalTransformation)
open import Data.Product using (∃; _,_; proj₁; proj₂; zip; map)
open import Level
open import Relation.Binary using (Rel)
open import Categories.Support.EqReasoning
open import Categories.Square

open import Categories.Comma
open import Categories.Product renaming (Product to _×_)

πComma :
  ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
    → {A : Category o₁ ℓ₁ e₁}
    → {B : Category o₂ ℓ₂ e₂}
    → {C : Category o₃ ℓ₃ e₃}
    → (S : Functor B C) (T : Functor A C)
    → Functor (S ↓ T) (B × A)
πComma {A = A} {B} {C} S T =
  record
    { F₀ = F₀′
    ; F₁ = F₁′
    ; identity = B×A.Equiv.refl
    ; homomorphism = B×A.Equiv.refl
    ; F-resp-≡ = λ pf → pf
    }
  where
    module S↓T = Category (S ↓ T)
    module B×A = Category (B × A)
    open Comma S T using (_,_[_]) renaming (_,_,_ to ⟨_,_,_⟩)

    F₀′ : S↓T.Obj → B×A.Obj
    F₀′ ⟨ α , β , f ⟩ = α , β

    F₁′ : ∀ {X Y} → (S ↓ T) [ X , Y ] → (B × A) [ F₀′ X , F₀′ Y ]
    F₁′ (g , h [ commutes ]) = g , h

InducedFunctor : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
                   {A : Category o₁ ℓ₁ e₁}
                   {B : Category o₂ ℓ₂ e₂}
                   {C : Category o₃ ℓ₃ e₃}
                   {s₁ s₂ d₁ d₂}
                   (m : (Category.op [ A ⇒ C ] × [ B ⇒ C ]) [ (s₁ , s₂) , (d₁ , d₂) ])
                 → Functor (s₁ ↓ s₂) (d₁ ↓ d₂)
InducedFunctor {A = A} {B} {C} {s₁} {s₂} {d₁} {d₂} m = record
  { F₀ = F₀′
  ; F₁ = F₁′
  ; identity = λ {X} → d₁↓d₂.Equiv.refl {_} {_} {d₁↓d₂.id {F₀′ X}}
  ; homomorphism = λ {_ _ _ f g} → d₁↓d₂.Equiv.refl {_} {_} {F₁′ ((s₁ ↓ s₂) [ g ∘ f ])}
  ; F-resp-≡ = λ pf → pf
  }
  where
  module s₁↓s₂ = Category (s₁ ↓ s₂)
  module d₁↓d₂ = Category (d₁ ↓ d₂)
  module s₁ = Functor s₁
  module s₂ = Functor s₂
  module d₁ = Functor d₁
  module d₂ = Functor d₂
  module m₁ = NaturalTransformation (proj₁ m)
  module m₂ = NaturalTransformation (proj₂ m)

  open Category C
  open Comma renaming (_,_,_ to ⟨_,_,_⟩)

  F₀′ : s₁↓s₂.Obj → d₁↓d₂.Obj
  F₀′ ⟨ α , β , f ⟩ = ⟨ α , β , m₂.η β ∘ f ∘ m₁.η α ⟩

  F₁′ : ∀ {X Y} → (s₁ ↓ s₂) [ X , Y ] → (d₁ ↓ d₂) [ F₀′ X , F₀′ Y ]
  F₁′ {⟨ α₁ , β₁ , f₁ ⟩} {⟨ α₂ , β₂ , f₂ ⟩} (g , h [ commutes ]) = g , h [ (
      begin
        d₂.F₁ h ∘ m₂.η β₁ ∘ f₁ ∘ m₁.η α₁
      ↑⟨ pushˡ (m₂.commute h) ⟩
        (m₂.η β₂ ∘ s₂.F₁ h) ∘ f₁ ∘ m₁.η α₁
      ↓⟨ pullˡ (pullʳ commutes) ⟩
        (m₂.η β₂ ∘ f₂ ∘ s₁.F₁ g) ∘ m₁.η α₁
      ↑⟨ extendˡ (extendˡ (m₁.commute g)) ⟩
        (m₂.η β₂ ∘ f₂ ∘ m₁.η α₂) ∘ d₁.F₁ g
      ∎ ) ]
    where
    open HomReasoning
    open GlueSquares C

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, Bentfest 2016-04-28 Marsstrand
-- Issue 1944: also resolve overloaded projections in checking position

module _ (A : Set) (a : A) where

record R B : Set where
  field f : B
open R

record S B : Set where
  field f : B
open S

test : R A → A
test = f

test1 : ∀{A} → R A → A
test1 = f

test2 : ∀ A → R A → A
test2 A = f {A}

postulate
  F : Set → Set
  mapF : ∀{A B} (f : A → B) → F A → F B
  fr : F (R A)

test3 : F (R A) → F A
test3 = mapF f

test4 : F (R _) → F A
test4 = mapF f

test5 : ∀{A} → F (F (R A)) → F _
test5 = mapF (mapF f)

test6 = mapF f fr

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module nat-thms where

open import bool
open import bool-thms
open import bool-thms2
open import eq
open import nat
open import neq
open import product
open import product-thms
open import sum
open import level
open import negation

--------------------------------------------------
-- properties of addition
--------------------------------------------------

0+ : ∀ (x : ℕ) → 0 + x ≡ x
0+ x = refl

+0 : ∀ (x : ℕ) → x + 0 ≡ x
+0 zero = refl
+0 (suc x) rewrite +0 x = refl

+1 : ∀ (x : ℕ) → x + 1 ≡ suc x
+1 zero = refl
+1 (suc x) rewrite +1 x = refl

+suc : ∀ (x y : ℕ) → x + (suc y) ≡ suc(x + y)
+suc zero y = refl
+suc (suc x) y rewrite +suc x y = refl

+assoc : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
+assoc zero y z = refl
+assoc (suc x) y z rewrite +assoc x y z = refl

+comm : ∀ (x y : ℕ) → x + y ≡ y + x
+comm zero y rewrite +0 y = refl
+comm (suc x) y rewrite +suc y x | +comm x y = refl

+perm : ∀ (x y z : ℕ) → x + (y + z) ≡ y + (x + z)
+perm x y z rewrite +assoc x y z | +comm x y | sym (+assoc y x z) = refl

+perm2 : ∀ (x y z : ℕ) → (x + y) + z ≡ (x + z) + y
+perm2 x y z rewrite sym (+assoc x y z) | +comm y z | +assoc x z y = refl

+≡0 : ∀ {x y : ℕ} → x + y ≡ 0 → x ≡ 0 ∧ y ≡ 0
+≡0{zero}{zero} p = refl , refl
+≡0{zero}{suc y} ()
+≡0{suc x}{zero} ()
+≡0{suc x}{suc y} ()

--------------------------------------------------
-- properties of multiplication
--------------------------------------------------

*0 : ∀ (x : ℕ) → x * 0 ≡ 0
*0 zero = refl
*0 (suc x) rewrite *0 x = refl

*1 : ∀ {n : ℕ} → n * 1 ≡ n
*1 {0} = refl
*1 {suc n} rewrite *1 {n} = refl

*suc : ∀ (x y : ℕ) → x * (suc y) ≡ x + x * y
*suc zero y = refl
*suc (suc x) y rewrite *suc x y | +assoc y x (x * y) | +assoc x y (x * y) | +comm y x = refl

*distribr : ∀ (x y z : ℕ) → (x + y) * z ≡ x * z + y * z
*distribr zero y z = refl
*distribr (suc x) y z rewrite *distribr x y z = +assoc z (x * z) (y * z)

*distribl : ∀ (x y z : ℕ) → x * (y + z) ≡ x * y + x * z
*distribl 0 y z = refl
*distribl (suc x) y z rewrite *distribl x y z | +assoc (y + z) (x * y) (x * z) | +assoc (y + x * y) z (x * z) | +comm (y + z) (x * y) | +assoc (x * y) y z | +comm (x * y) y = refl

*comm : ∀ (x y : ℕ) → x * y ≡ y * x
*comm zero y rewrite *0 y = refl
*comm (suc x) y rewrite *suc y x | *comm x y = refl

*assoc : ∀ (x y z : ℕ) → x * (y * z) ≡ (x * y) * z
*assoc zero y z = refl
*assoc (suc x) y z rewrite *assoc x y z | *distribr y (x * y) z = refl

--------------------------------------------------
-- basic properties of pred
--------------------------------------------------

sucpred : ∀ {x : ℕ} → iszero x ≡ ff → suc (pred x) ≡ x
sucpred{0} ()
sucpred{suc x} p = refl

pred+ : ∀ (x y : ℕ) → iszero x ≡ ff → (pred x) + y ≡ pred (x + y)
pred+ 0 y ()
pred+ (suc x) y p = refl

--------------------------------------------------
-- properties of <, ≤, and =ℕ, iszero
--------------------------------------------------

<-0 : ∀ (x : ℕ) → x < 0 ≡ ff
<-0 0 = refl
<-0 (suc y) = refl

0-≤ : ∀ (x : ℕ) → 0 ≤ x ≡ tt
0-≤ 0 = refl
0-≤ (suc x) = refl

<-drop : ∀ {x y : ℕ} → (x < (suc y) ≡ tt) → x ≡ y ∨ x < y ≡ tt
<-drop {0} {0} p = inj₁ refl
<-drop {suc x} {0} p rewrite <-0 x = 𝔹-contra p
<-drop {0} {suc y} p = inj₂ refl
<-drop {suc x} {suc y} p with <-drop {x} {y} p
... | inj₁ u rewrite u = inj₁ refl
... | inj₂ u = inj₂ u

=ℕ-refl : ∀ (x : ℕ) → (x =ℕ x) ≡ tt
=ℕ-refl 0 = refl
=ℕ-refl (suc x) = (=ℕ-refl x)

=ℕ-to-≡ : ∀ {x y : ℕ} → x =ℕ y ≡ tt → x ≡ y
=ℕ-to-≡ {0} {0} u = refl
=ℕ-to-≡ {suc x} {0} ()
=ℕ-to-≡ {0} {suc y} ()
=ℕ-to-≡ {suc x} {suc y} u rewrite =ℕ-to-≡ {x} {y} u = refl

=ℕ-from-≡ : ∀ {x y : ℕ} → x ≡ y → x =ℕ y ≡ tt
=ℕ-from-≡ {x} refl = =ℕ-refl x

=ℕ-sym : ∀ (x y : ℕ) → (x =ℕ y) ≡ (y =ℕ x)
=ℕ-sym 0 0 = refl
=ℕ-sym 0 (suc y) = refl
=ℕ-sym (suc x) 0 = refl
=ℕ-sym (suc x) (suc y) rewrite =ℕ-sym x y = refl

=ℕ-suc : ∀ (x : ℕ) → suc x =ℕ x ≡ ff
=ℕ-suc 0 = refl
=ℕ-suc (suc x) = =ℕ-suc x

<-suc : ∀ (n : ℕ) → n < suc n ≡ tt
<-suc 0 = refl
<-suc (suc n) rewrite <-suc n = refl

<-suc2 : ∀ (n : ℕ) → suc n < n ≡ ff
<-suc2 0 = refl
<-suc2 (suc n) = <-suc2 n

≤-suc : ∀ (n : ℕ) → n ≤ suc n ≡ tt
≤-suc n rewrite <-suc n = refl

≤-suc2 : ∀ (n : ℕ) → suc n ≤ n ≡ ff
≤-suc2 n rewrite <-suc2 n | =ℕ-suc n = refl

<-push : ∀ {x y : ℕ} → (suc x) < y ≡ tt → Σ ℕ (λ y' → y ≡ (suc y'))
<-push {x} {0} ()
<-push {0} {suc y} p = (y , refl)
<-push {suc x} {suc y} p with <-push {x} {y} p
... | ( y' , p' ) rewrite p' = (suc y' , refl)

suc-inj : ∀ {n m : ℕ} → suc n ≡ suc m → n ≡ m
suc-inj {n} {m} p rewrite (=ℕ-to-≡{n} (=ℕ-from-≡ p)) = refl

<-implies-suc : ∀ {x y : ℕ} → x < y ≡ tt → Σ ℕ λ y' → y ≡ suc y'
<-implies-suc{x}{0} p rewrite <-0 x = 𝔹-contra p
<-implies-suc{y = suc y} p = y , refl

<=ℕff : ∀ (x : ℕ) → 0 < x ≡ tt → x =ℕ 0 ≡ ff
<=ℕff 0 ()
<=ℕff (suc x) p = refl

nonzero< : ∀ {n : ℕ} → iszero n ≡ ff → 0 < n ≡ tt
nonzero<{0} ()
nonzero<{(suc n)} p = refl

iszerosum : ∀ (x y : ℕ) → iszero(x + y) ≡ iszero(x) && iszero(y)
iszerosum 0 y = refl
iszerosum (suc x) y = refl

iszerosum2 : ∀ (x y : ℕ) → iszero x ≡ ff → iszero(x + y) ≡ ff
iszerosum2 0 y ()
iszerosum2 (suc x) y _ = refl

iszeromult : ∀ (x y : ℕ) → iszero x ≡ ff → iszero y ≡ ff →
               iszero (x * y) ≡ ff
iszeromult zero zero () q
iszeromult zero (suc y) () q
iszeromult (suc x) zero p ()
iszeromult (suc x) (suc y) p q = refl

<≤ : ∀ {n m : ℕ} → n < m ≡ tt → n ≤ m ≡ tt
<≤ {n}{m} p rewrite p = refl

≤+1 : ∀(x y : ℕ) → x ≤ x + y ≡ tt
≤+1 zero zero = refl
≤+1 zero (suc y) = refl
≤+1 (suc x) zero rewrite +0 x | =ℕ-refl x | ||-tt (x < x) = refl
≤+1 (suc x) (suc y) = ≤+1 x (suc y)

≤+2 : ∀(x y : ℕ) → y ≤ x + y ≡ tt
≤+2 x y rewrite +comm x y = ≤+1 y x

-- a theorem about quotients q, divisors d, and remainders r
÷< : ∀ {d q r x : ℕ} → 1 < d ≡ tt → q * d + r ≡ suc x → q < suc x ≡ tt
÷<{0} () p
÷<{suc 0} () p
÷<{suc (suc d)}{0} u p = refl
÷<{suc (suc d)}{suc q}{r}{0} u ()
÷<{suc (suc d)}{suc q}{r}{suc x} u p with suc-inj{suc (d + q * suc (suc d) + r)}{suc x} p
... | p' rewrite sym (+suc (d + q * suc (suc d)) r) | +comm d (q * suc (suc d))
               | sym (+assoc (q * (suc (suc d))) d (suc r)) = ÷<{suc (suc d)}{q}{d + suc r}{x} refl p'

--------------------------------------------------
-- ordering properties of < and ≤ℕ
--------------------------------------------------

<-irrefl : ∀ (n : ℕ) → n < n ≡ ff
<-irrefl 0 = refl
<-irrefl (suc n) = <-irrefl n

<-asym : ∀ {x y : ℕ} → x < y ≡ tt → y < x ≡ ff
<-asym {0} {0} _ = refl
<-asym {0} {suc y} p = refl
<-asym {suc x}{0} ()
<-asym {suc x}{suc y} p = <-asym {x} {y} p

ℕ-trichotomy𝔹 : ∀ (n m : ℕ) → n < m || n =ℕ m || m < n ≡ tt
ℕ-trichotomy𝔹 0 0 = refl
ℕ-trichotomy𝔹 0 (suc m) = refl
ℕ-trichotomy𝔹 (suc n) 0 = refl
ℕ-trichotomy𝔹 (suc n) (suc m) = ℕ-trichotomy𝔹 n m

ℕ-trichotomy : ∀ (n m : ℕ) → (n < m ≡ tt) ∨ (n =ℕ m ≡ tt) ∨ (m < n ≡ tt)
ℕ-trichotomy n m with ||-split{n < m} (ℕ-trichotomy𝔹 n m)
... | inj₁ p = inj₁ p
... | inj₂ p with ||-split{n =ℕ m} p
... | inj₁ p' = inj₂ (inj₁ p')
... | inj₂ p' = inj₂ (inj₂ p')

<-insert : ∀ {x n m : ℕ} → n ≤ m ≡ tt → (x < n ≡ tt) ∨ (n ≤ x && x ≤ m ≡ tt) ∨ (m < x ≡ tt)
<-insert{x}{n}{m} q with ℕ-trichotomy x n
<-insert{x}{n}{m} q | inj₁ p = inj₁ p
<-insert{x}{n}{m} q | inj₂ (inj₁ p) rewrite (=ℕ-to-≡{x} p) | =ℕ-refl n | ||-tt (n < n) = inj₂ (inj₁ q)
<-insert{x}{n}{m} q | inj₂ (inj₂ p) rewrite p with ℕ-trichotomy x m
<-insert{x}{n}{m} q | inj₂ (inj₂ p) | inj₁ p' rewrite p' = inj₂ (inj₁ refl)
<-insert{x}{n}{m} q | inj₂ (inj₂ p) | inj₂ (inj₁ p') rewrite p' | ||-tt (x < m) = inj₂ (inj₁ refl)
<-insert{x}{n}{m} q | inj₂ (inj₂ p) | inj₂ (inj₂ p') = inj₂ (inj₂ p')

<-insert2 : ∀ {x n m : ℕ} → n ≤ m ≡ tt → (x < n ≡ tt) ∨ (n ≤ x ≡ tt ∧ x ≤ m ≡ tt) ∨ (m < x ≡ tt)
<-insert2{x}{n}{m} p with <-insert{x}{n}{m} p
<-insert2{x}{n}{m} p | inj₁ p' = inj₁ p'
<-insert2{x}{n}{m} p | inj₂ (inj₁ p') with &&-elim {n ≤ x} {x ≤ m} p'
<-insert2{x}{n}{m} p | inj₂ (inj₁ p') | p1 , p2 = inj₂ (inj₁ (p1 , p2))
<-insert2{x}{n}{m} p | inj₂ (inj₂ p') = inj₂ (inj₂ p')

<-trans : ∀ {x y z : ℕ} → x < y ≡ tt → y < z ≡ tt → x < z ≡ tt
<-trans {x} {0} p1 p2 rewrite <-0 x = 𝔹-contra p1
<-trans {0} {suc y} {0} p1 ()
<-trans {0} {suc y} {suc z} p1 p2 = refl
<-trans {suc x} {suc y} {0} p1 ()
<-trans {suc x} {suc y} {suc z} p1 p2 = <-trans {x} {y} {z} p1 p2

-- <≤-trans : ∀ {x y z : ℕ} → x < y ≡ tt → y ≤ z ≡ tt → x < z ≡ tt
-- <≤-trans {x} {y} {z} p1 p2 with ||-split p2
-- ... | inj₁ p' = <-trans{x}  p1 p'
-- ... | inj₂ p' rewrite =ℕ-to-≡ {y} {z} p' = p1

≤<-trans : ∀ {x y z : ℕ} → x ≤ y ≡ tt → y < z ≡ tt → x < z ≡ tt
≤<-trans {x} {y} {z} p1 p2 with ||-split p1
... | inj₁ p' = <-trans{x} p' p2
... | inj₂ p' rewrite =ℕ-to-≡ {x} {y} p' = p2

≤-refl : ∀ (x : ℕ) → x ≤ x ≡ tt
≤-refl 0 = refl
≤-refl (suc x) = ≤-refl x

≤-trans : ∀ {x y z : ℕ} → x ≤ y ≡ tt → y ≤ z ≡ tt → x ≤ z ≡ tt
≤-trans {x} {y} {z} p1 p2 with ||-split p1 | ||-split p2
... | inj₁ p' | inj₁ p'' rewrite <-trans {x} p' p'' = refl
... | inj₂ p' | inj₁ p'' rewrite =ℕ-to-≡ {x} p'  | p'' = refl
... | inj₁ p' | inj₂ p'' rewrite =ℕ-to-≡ {y} p'' | p' = refl
... | inj₂ p' | inj₂ p'' rewrite =ℕ-to-≡ {x} p'  | =ℕ-to-≡ {y} p'' | =ℕ-refl z | ||-tt (z < z) = refl

suc≤ : ∀ {n n' : ℕ} → suc n ≤ suc n' ≡ tt → n ≤ n' ≡ tt
suc≤{n}{n'} p = p

-- suc≤< : ∀ {n n' : ℕ} → suc n ≤ n' ≡ tt → n < n' ≡ tt
-- suc≤<{n} p = <≤-trans{n} (<-suc n) p

suc<< : ∀ {n' n : ℕ} → suc n < n' ≡ tt → n < n' ≡ tt
suc<<{n = n} p = <-trans{n} (<-suc n) p

<-suc-trans : ∀{x y : ℕ} → x < y ≡ tt → x < suc y ≡ tt
<-suc-trans{0}{0} _ = refl
<-suc-trans{suc x}{0} ()
<-suc-trans{0}{suc y} _ = refl
<-suc-trans{suc x}{suc y} p = <-suc-trans{x}{y} p

≤-suc-trans : ∀{x y : ℕ} → x ≤ y ≡ tt → x ≤ suc y ≡ tt
≤-suc-trans{0}{0} _ = refl
≤-suc-trans{suc x}{0} ()
≤-suc-trans{0}{suc y} _ = refl
≤-suc-trans{suc x}{suc y} p = ≤-suc-trans{x}{y} p

-------------------------------------------------------------
-- more properties relating <, ≤ with arithmetic operations
-------------------------------------------------------------

<+ : ∀ {x y : ℕ} → y =ℕ 0 ≡ ff → x < y + x ≡ tt
<+{y = 0} ()
<+{x}{suc 0} p = <-suc x
<+{x}{suc (suc y)} p = <-trans{x}{(suc y) + x}{suc ((suc y) + x)} (<+{x}{suc y} refl) (<-suc ((suc y) + x))

<+2 : ∀ {x y : ℕ} → x < (suc y) + x ≡ tt
<+2{x}{y} = <+{x}{suc y} refl

<-iter-suc-trans-t-h : (n : ℕ) → (x : ℕ) → (accum : ℕ) → Set
<-iter-suc-trans-t-h 0 x accum = x < accum ≡ tt
<-iter-suc-trans-t-h (suc n) x accum = <-iter-suc-trans-t-h n x (suc accum)

<-iter-suc-trans-t : (n : ℕ) → (x : ℕ) → Set
<-iter-suc-trans-t n x = <-iter-suc-trans-t-h n x (suc x)

<-iter-suc-trans-h : ∀ (n : ℕ) → (x : ℕ) → (accum : ℕ) → x < accum ≡ tt → <-iter-suc-trans-t-h n x accum
<-iter-suc-trans-h 0 x accum p = p
<-iter-suc-trans-h (suc n) x accum p = <-iter-suc-trans-h n x (suc accum) (<-suc-trans{x} p)

<-iter-suc-trans : ∀ (n : ℕ) → (x : ℕ) → <-iter-suc-trans-t n x
<-iter-suc-trans n x = <-iter-suc-trans-h n x (suc x) (<-suc x)

≤0 : ∀ (n : ℕ) → 0 ≤ n ≡ tt
≤0 0 = refl
≤0 (suc n) = refl

≤2* : ∀ (x : ℕ) → x ≤ 2 * x ≡ tt
≤2* 0 = refl
≤2* (suc x) rewrite +suc x (x + 0) | ≤<-trans {x} (≤2* x) (<-suc (2 * x)) = refl

0<+ : ∀ (x y : ℕ) → 0 < y ≡ tt → 0 < x + y ≡ tt
0<+ 0 y p = p
0<+ (suc x) y p = refl

<=ℕff2 : ∀ (x : ℕ) → 1 < x ≡ tt → x =ℕ 0 ≡ ff
<=ℕff2 x p = <=ℕff x (<-trans{0}{1}{x} refl p)

*≤ : ∀(x y : ℕ) → x ≤ x * (suc y) ≡ tt
*≤ zero y = refl
*≤ (suc x) y = ≤-trans {x} (*≤ x y) (≤+2 y (x * suc y))

--------------------------------------------------
-- relationships between ≤ and <
--------------------------------------------------

≤ff : ∀ {x y : ℕ} → x ≤ y ≡ ff → y < x ≡ tt
≤ff{0}{0} ()
≤ff{0}{suc y} ()
≤ff{suc x}{0} _ = refl
≤ff{suc x}{suc y} p rewrite ≤ff {x}{y} p = refl

<ff : ∀ {x y : ℕ} → x < y ≡ ff → y ≤ x ≡ tt
<ff{x}{y} p with ℕ-trichotomy x y
... | inj₁ u rewrite u = 𝔹-contra (sym p)
... | inj₂ (inj₁ u) rewrite (=ℕ-to-≡{x} u) | =ℕ-refl y | ||-tt (y < y) = refl
... | inj₂ (inj₂ u) rewrite u = refl

<-not-=ℕ : ∀{x y : ℕ} → x < y ≡ tt → y =ℕ x ≡ ff
<-not-=ℕ{0}{0} ()
<-not-=ℕ{suc x}{0} ()
<-not-=ℕ{0}{suc y} p = refl
<-not-=ℕ{suc x}{suc y} p = <-not-=ℕ{x}{y} p

<-not-> : ∀{x y : ℕ} → x < y ≡ tt → y < x ≡ ff
<-not->{0}{0} ()
<-not->{suc x}{0} ()
<-not->{0}{suc y} p = refl
<-not->{suc x}{suc y} p = <-not->{x}{y} p

<tt : ∀ {x y : ℕ} → x < y ≡ tt → y ≤ x ≡ ff
<tt{x}{y} p rewrite <-not-=ℕ{x}{y} p | <-not->{x}{y} p = refl

≤-antisym : ∀{x y : ℕ} → x ≤ y ≡ tt → y ≤ x ≡ tt → x ≡ y
≤-antisym{x}{y} p q with ||-split {x < y} p
≤-antisym{x}{y} p q | inj₁ u rewrite <tt{x} u with q
≤-antisym{x}{y} p q | inj₁ u | ()
≤-antisym{x}{y} p q | inj₂ u = =ℕ-to-≡ u

--------------------------------------------------
-- monotonicity properties of < and ≤ℕ
--------------------------------------------------
<+mono1 : ∀ {z x y : ℕ} → x < y ≡ tt → z + x < z + y ≡ tt
<+mono1{0} p = p
<+mono1{suc z} p = <+mono1{z} p

<+mono2 : ∀ {x y z : ℕ} → x < y ≡ tt → x + z < y + z ≡ tt
<+mono2{x}{y}{z} p rewrite +comm x z | +comm y z | <+mono1{z}{x}{y} p = refl

--------------------------------------------------
-- properties of subtraction
--------------------------------------------------

0∸ : ∀ {x : ℕ} → 0 ∸ x ≡ 0
0∸{0} = refl
0∸{suc x} = refl

∸≤ : ∀ (x y : ℕ) → x ∸ y ≤ x ≡ tt
∸≤ 0 0 = refl
∸≤ (suc x) 0 rewrite (=ℕ-refl x) = ||-tt (x < x)
∸≤ 0 (suc y) = refl
∸≤ (suc x) (suc y) with ||-split{x ∸ y < x}{x ∸ y =ℕ x} (∸≤ x y)
... | inj₁ u rewrite <-trans {x ∸ y} u (<-suc x) = refl
... | inj₂ u rewrite (=ℕ-to-≡ {x ∸ y} u) | <-suc x = refl

∸< : ∀ {x y : ℕ} → x =ℕ 0 ≡ ff → x ∸ (suc y) < x ≡ tt
∸< {0} {y} ()
∸< {suc x} {y} _ with ||-split{x ∸ y < x}{x ∸ y =ℕ x} (∸≤ x y)
... | inj₁ u = <-trans {x ∸ y} u (<-suc x)
... | inj₂ u rewrite (=ℕ-to-≡ {x ∸ y} u) = <-suc x

∸<1 : ∀ {x y : ℕ} → x ∸ y < suc x ≡ tt
∸<1 {zero} {zero} = refl
∸<1 {zero} {suc y} = refl
∸<1 {suc x} {zero} = <-suc x
∸<1 {suc x} {suc y} = <-trans {x ∸ y}{suc x} (∸<1 {x} {y}) (<-suc x)

+∸1 : ∀ {x y : ℕ} → x < y ≡ tt → x + (y ∸ x) ≡ y
+∸1{0} p = refl
+∸1{suc x}{0} ()
+∸1{suc x}{suc y} p rewrite +∸1{x}{y} p = refl

∸+ : ∀ {x y z : ℕ} → x ∸ (y + z) ≡ (x ∸ y) ∸ z
∸+{x}{0} = refl
∸+{0}{suc y}{z} rewrite 0∸{z} = refl
∸+{suc x}{suc y} = ∸+{x}{y}

∸+2 : ∀ {x y : ℕ} → y ≤ x ≡ tt → (x ∸ y) + y ≡ x
∸+2{0}{0} _ = refl
∸+2{suc x}{0} _ rewrite +0 x = refl
∸+2{0}{suc y} ()
∸+2{suc x}{suc y} p rewrite +suc (x ∸ y) y | ∸+2{x}{y} p = refl

∸eq-swap : ∀ {x y z : ℕ} → y ≤ x ≡ tt → z ≡ x ∸ y → z + y ≡ x
∸eq-swap{x}{y}{z} p q = lem (cong (λ w → w + y) q)
                        where lem : z + y ≡ (x ∸ y) + y → z + y ≡ x
                              lem p' rewrite ∸+2{x}{y} p = p'

<∸ : ∀ {x y : ℕ} → (y < x ≡ tt) → ((x ∸ y =ℕ 0) ≡ ff)
<∸ {0}{y} p with <-0 y
... | q rewrite p = 𝔹-contra (sym q)
<∸ {suc x}{0} p = refl
<∸ {suc x}{suc y} p = <∸{x}{y} p

<∸suc : ∀ {x y : ℕ} → (y < x ≡ tt) → Σ ℕ (λ n → x ∸ y ≡ suc n)
<∸suc{x}{y} p with keep (x ∸ y)
<∸suc{x}{y} p | 0 , r with <∸{x}{y} p
<∸suc{x}{y} p | 0 , r | q rewrite r with q
<∸suc{x}{y} p | 0 , r | q | ()
<∸suc{x}{y} p | suc n , r = n , r

∸suc : ∀ {x y z : ℕ } → y < x ≡ tt → x ∸ (y + (suc z)) < x ∸ y ≡ tt
∸suc{x}{y}{z} p rewrite ∸+{x}{y}{suc z} = ∸< {x ∸ y} (<∸{x}{y} p)

∸suc2 : ∀ {x y z : ℕ } → y < x ≡ tt → x ∸ ((suc z) + y) < x ∸ y ≡ tt
∸suc2{x}{y}{z} p rewrite +comm (suc z) y = ∸suc{x}{y}{z} p

∸cancel : ∀ (x y z : ℕ) → (x + y) ∸ (x + z) ≡ y ∸ z
∸cancel 0 y z = refl
∸cancel (suc x) y z = ∸cancel x y z

distribr*∸ : ∀ (x y z : ℕ) → (x ∸ y) * z ≡  x * z ∸ y * z
distribr*∸ 0 y z rewrite 0∸{y} | 0∸{y * z} = refl
distribr*∸ (suc x) 0 z = refl
distribr*∸ (suc x) (suc y) z rewrite distribr*∸ x y z | ∸cancel z (x * z) (y * z) = refl

∸≤2 : ∀ (n x y : ℕ) →  x ≤ suc n ≡ tt → y =ℕ 0 ≡ ff → x ∸ y ≤ n ≡ tt
∸≤2 0 0 y p1 p2 rewrite 0∸{y} = refl
∸≤2 0 (suc x) 0 p1 ()
∸≤2 0 (suc 0) (suc y) p1 p2 rewrite 0∸{y}= refl
∸≤2 0 (suc (suc x)) (suc y) () p2
∸≤2 (suc n) 0 y p1 p2 rewrite 0∸{y} = refl
∸≤2 (suc n) (suc x) 0 p1 ()
∸≤2 (suc n) (suc x) (suc 0) p1 p2 = p1
∸≤2 (suc n) (suc x) (suc (suc y)) p1 p2 = ≤-trans{x ∸ suc y}{n}{suc n} (∸≤2 n x (suc y) p1 refl) (≤-suc n)

--------------------------------------------------
-- properties of min, max
--------------------------------------------------
min-forced1 : ∀ {n n' m : ℕ} → n < n' ≡ tt → n ≡ min n' m → n ≡ m
min-forced1{n}{n'}{m} p1 p2 with n' < m
... | tt rewrite p2 = 𝔹-contra (trans (sym (<-irrefl n')) p1)
... | ff = p2

min-suc : ∀ (n m : ℕ) → min (suc n) (suc m) ≡ suc (min n m)
min-suc n m rewrite (ite-arg suc (n < m) n m) = refl

max-suc : ∀ (n m : ℕ) → max (suc n) (suc m) ≡ suc (max n m)
max-suc n m rewrite (ite-arg suc (n < m) m n) = refl

min-mono1 : ∀ (n n' m : ℕ) → n ≤ n' ≡ tt → min n m ≤ min n' m ≡ tt
min-mono1 n n' m p with ||-split{n < n'} p
... | inj₂ p' rewrite =ℕ-to-≡ {n} p' | =ℕ-refl (min n' m) | ||-tt ((min n' m) < (min n' m)) = refl
... | inj₁ p' with ℕ-trichotomy n' m
... | inj₁ p'' rewrite <-trans {n} p' p'' | p'' | p' = refl
... | inj₂ (inj₁ p'') rewrite =ℕ-to-≡ {n'} p'' | p' | =ℕ-refl (min n m) | ||-tt ((min n m) < (min n m)) | <-irrefl m | p' = refl
... | inj₂ (inj₂ p'') rewrite <-asym {m} p'' with ℕ-trichotomy n m
... | inj₁ p''' rewrite p''' | p''' = refl
... | inj₂ (inj₁ p''') rewrite =ℕ-to-≡ {n} p''' | <-irrefl m | =ℕ-refl m | ||-tt (m < m) = refl
... | inj₂ (inj₂ p''') rewrite <-asym {m} p''' | =ℕ-refl m | ||-tt (m < m) = refl

min-comm : ∀ (n m : ℕ) → min n m ≡ min m n
min-comm n m with ℕ-trichotomy n m
... | inj₁ p rewrite p | <-asym {n} p = refl
... | inj₂ (inj₁ p) rewrite =ℕ-to-≡ {n} p = refl
... | inj₂ (inj₂ p) rewrite p | <-asym {m} p = refl

min-mono2 : ∀ (n m m' : ℕ) → m ≤ m' ≡ tt → min n m ≤ min n m' ≡ tt
min-mono2 n m m' p rewrite min-comm n m | min-comm n m' = min-mono1 m m' n p

min-same : ∀ (n : ℕ) → min n n ≡ n
min-same n rewrite <-irrefl n = refl

min-<1 : ∀ {n m : ℕ} → min n m ≤ m ≡ tt
min-<1{0}{0} = refl
min-<1{0}{suc m} = refl
min-<1{suc n}{0} = refl
min-<1{suc n}{suc m} rewrite min-suc n m = min-<1{n}

min-<2 : ∀ {n m : ℕ} → min n m ≤ n ≡ tt
min-<2{0}{0} = refl
min-<2{0}{suc m} = refl
min-<2{suc n}{0} = refl
min-<2{suc n}{suc m} rewrite min-suc n m = min-<2{n}

max-<1 : ∀ {n m : ℕ} → n ≤ max n m ≡ tt
max-<1{0}{0} = refl
max-<1{0}{suc m} = refl
max-<1{suc n}{0} rewrite =ℕ-refl n | ||-tt (n < n) = refl
max-<1{suc n}{suc m} rewrite max-suc n m = max-<1{n}

max-<2 : ∀ {n m : ℕ} → n ≤ max n m ≡ tt
max-<2{0}{0} = refl
max-<2{0}{suc m} = refl
max-<2{suc n}{0} rewrite =ℕ-refl n | ||-tt (n < n) = refl
max-<2{suc n}{suc m} rewrite max-suc n m = max-<2{n}

--------------------------------------------------
-- some disequalities
--------------------------------------------------

+≢ : ∀ (x y : ℕ) → x ≢ x + suc y
+≢ 0 y ()
+≢ (suc x) y p with =ℕ-from-≡ {suc x} p
... | q with =ℕ-to-≡ {x} q
... | r = +≢ x y r

--------------------------------------------------
-- properties of parity
--------------------------------------------------
parity-even : ∀ (x : ℕ) → parity (x * 2) ≡ ff
parity-even 0 = refl
parity-even (suc x) rewrite parity-even x = refl

parity-even2 : ∀ (x : ℕ) → parity (2 * x) ≡ ff
parity-even2 x rewrite *comm 2 x = parity-even x

parity-odd : ∀ (x : ℕ) → parity (x * 2 + 1) ≡ tt
parity-odd 0 = refl
parity-odd (suc x) rewrite parity-odd x = refl

parity-add : ∀ (x y : ℕ) → parity (x + y) ≡ (parity x) xor (parity y)
parity-add 0 y rewrite ff-xor (parity y) = refl
parity-add (suc x) y rewrite parity-add x y | ~-xor-distrb (parity x) (parity y) = refl

parity-mult : ∀ (x y : ℕ) → parity (x * y) ≡ (parity x) && (parity y)
parity-mult 0 y = refl
parity-mult (suc x) y rewrite parity-add y (x * y) | parity-mult x y = xor-distrib-&& (parity y) (parity x)

--------------------------------------------------
-- properties of power
--------------------------------------------------
1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1
1-pow {0} = refl
1-pow {(suc n)} rewrite 1-pow {n} = refl

nonzero-pow : ∀ (x y : ℕ) → x =ℕ 0 ≡ ff → iszero (x pow y) ≡ ff
nonzero-pow x 0 _ = refl
nonzero-pow 0 (suc y) ()
nonzero-pow (suc x) (suc y) p rewrite iszerosum2 (suc x pow y) (x * suc x pow y) (nonzero-pow (suc x) y refl) = refl

pow+ : ∀ (x y z : ℕ) → x pow (y + z) ≡ (x pow y) * (x pow z)
pow+ x 0 z rewrite +0 (x pow z) = refl
pow+ x (suc y) z rewrite pow+ x y z | *assoc x (x pow y) (x pow z) = refl

pow* : ∀ (x y z : ℕ) → x pow (y * z) ≡ (x pow y) pow z
pow* x y 0 rewrite *0 y = refl
pow* x y (suc z) rewrite sym (pow* x y z) | sym (pow+ x y (y * z)) | *comm y (suc z) | *comm y z = refl

--------------------------------------------------
-- properties of factorial
--------------------------------------------------
factorial-nonzero : ∀ (n : ℕ) → iszero (factorial n) ≡ ff
factorial-nonzero zero = refl
factorial-nonzero (suc x) rewrite iszerosum (factorial x) (x * factorial x) | factorial-nonzero x = refl

--------------------------------------------------
-- injectivity properties of addition
--------------------------------------------------
+inj1 : ∀ {x y z : ℕ} → x + y ≡ x + z → y ≡ z
+inj1 {0} {y} {z} p = p
+inj1 {suc x} {y} {z} p = +inj1 {x} {y} {z} (suc-inj p)

+inj2 : ∀ {x y z : ℕ} → x + z ≡ y + z → x ≡ y
+inj2 {x} {y} {z} p rewrite +comm x z | +comm y z = +inj1 {z} {x} {y} p

--------------------------------------------------
-- properties of is-even, is-odd
--------------------------------------------------

even~odd : ∀ (x : ℕ) → is-even x ≡ ~ is-odd x
odd~even : ∀ (x : ℕ) → is-odd x ≡ ~ is-even x
even~odd zero = refl
even~odd (suc x) = odd~even x
odd~even zero = refl
odd~even (suc x) = even~odd x

suc-eq : ∀{x y} → suc x ≡ suc y → x ≡ y
suc-eq refl = refl

suc-eq⊥ : ∀{x y} → ¬ (x ≡ y) → ¬ (suc x ≡ suc y)
suc-eq⊥ p refl = p refl

zero-suc-eq⊥ : ∀{x} → zero ≡ suc x → ⊥ {lzero}
zero-suc-eq⊥ ()

suc-zero-eq⊥ : ∀{x} → suc x ≡ zero → ⊥ {lzero}
suc-zero-eq⊥ ()

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module _ where

module M (X : Set) where
  postulate
    F : Set
    G : Set

data ⊥ : Set where

open M ⊥ hiding (F)

easy : M.G ⊥
easy = {!!}   -- G

hard : M.F ⊥
hard = {!!}    -- M.F ⊥ (and not .Issue1640._.F)

data ⊤ : Set where
  tt : ⊤

module With where
  private
    F : ⊤ → Set
    F x with x
    F _ | tt = ⊥

  T = F

tricky : ∀ t → With.T t
tricky t = {!!}  -- .Issue1640.With.F t | t

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

variable
  k l m n : Nat

postulate
  max : Nat → Nat → Nat
  max-0l : max 0 n ≡ n
  max-0r : max m 0 ≡ m
  max-diag : max m m ≡ m
  max-ss : max (suc m) (suc n) ≡ suc (max m n)
  max-assoc : max (max k l) m ≡ max k (max l m)

{-# REWRITE max-0l #-}
{-# REWRITE max-0r #-}
{-# REWRITE max-diag #-}
{-# REWRITE max-ss #-}
{-# REWRITE max-assoc #-} -- not confluent!

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module bstd.bake where

open import Agda.Builtin.Nat
open import Agda.Builtin.String
open import Data.Word8.Primitive
open import Data.ByteString.Primitive.Strict
open import Data.Tuple.Base

module bpace
  (Scalar : Set)
  (Point : Set)
  (scalarMul : Scalar → Point → Point)
  (2ᴸ : Set)
  (Key : Set)
  (enc dec : Key → 2ᴸ → 2ᴸ)
  (swu : 2ᴸ → 2ᴸ → Point)
  (Hello : Set)
  (I : Set) (i₀ i₁ : I)
  (kdf : (K Vᵃ Vᵇ : Point) (helloᵃ helloᵇ : Hello) → I → Key)
  (Tag : Set)
  (mac : Key → I → Tag)
  where

  s₂ : (K₂ : Key)
    → (Rᵇ : 2ᴸ)
    → 2ᴸ
  s₂ K₂ Rᵇ = Yᵇ where
    Yᵇ = enc K₂ Rᵇ

  s₃ : (K₂ : Key)
    → (Rᵃ : 2ᴸ) → (uᵃ : Scalar)
    → (Yᵇ : 2ᴸ)
    → 2ᴸ ∥ Point
  s₃ K₂ Rᵃ uᵃ Yᵇ = Yᵃ , Vᵃ where
    Rᵇ = dec K₂ Yᵇ
    Yᵃ = enc K₂ Rᵃ
    W = swu Rᵃ Rᵇ
    Vᵃ = scalarMul uᵃ W

  s₄ : (K₂ : Key)
    → (Rᵇ : 2ᴸ) → (uᵇ : Scalar) → (helloᵇ : Hello)
    → (Yᵃ : 2ᴸ) → (Vᵃ : Point) → (helloᵃ : Hello)
    → Point ∥ Tag
  s₄ K₂ Rᵇ uᵇ helloᵇ Yᵃ Vᵃ helloᵃ = Vᵇ , Tᵇ where
    Rᵃ = dec K₂ Yᵃ
    W = swu Rᵃ Rᵇ
    Vᵇ = scalarMul uᵇ W
    K = scalarMul uᵇ Vᵃ
    K₀ = kdf K Vᵃ Vᵇ helloᵃ helloᵇ i₀
    K₁ = kdf K Vᵃ Vᵇ helloᵃ helloᵇ i₁
    Tᵇ = mac K₁ i₁

  s₅ : (Vᵇ : Point) → (helloᵇ : Hello)
    → (uᵃ : Scalar) → (Vᵃ : Point) → (helloᵃ : Hello)
    → Tag
  s₅ Vᵇ helloᵇ uᵃ Vᵃ helloᵃ = Tᵃ where
    K = scalarMul uᵃ Vᵇ
    K₀ = kdf K Vᵃ Vᵇ helloᵃ helloᵇ i₀
    K₁ = kdf K Vᵃ Vᵇ helloᵃ helloᵇ i₁
    Tᵃ = mac K₁ i₀

max_stars_repo_name: semenov-vladyslav/bstd

max_issues_repo_name: semenov-vladyslav/bstd

max_forks_repo_name: semenov-vladyslav/bstd


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pretty Printing
-- This module is based on Jean-Philippe Bernardy's functional pearl
-- "A Pretty But Not Greedy Printer"
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

open import Data.Nat.Base using (ℕ)

module Text.Pretty (width : ℕ) where

import Level
open import Data.Char.Base     using (Char)
open import Data.List.Base
  using (List; _∷_; []; [_]; uncons; _++_; map; filter)
open import Data.List.NonEmpty as List⁺ using (foldr₁)
open import Data.Maybe.Base    using (maybe′)
open import Data.Product       using (uncurry)
open import Data.String.Base   using (String; fromList; replicate)
open import Function.Base

open import Category.Monad using (RawMonad)
import Data.List.Categorical as Cat
open RawMonad (Cat.monad {Level.zero})

import Data.Nat.Properties as ℕₚ
open import Data.List.Extrema.Core ℕₚ.≤-totalOrder using (⊓ᴸ)

------------------------------------------------------------------------
-- Internal representation of documents and rendering function

import Text.Pretty.Core as Core

Doc = List Core.Block

render : Doc → String
render = Core.render
       ∘ maybe′ (foldr₁ (⊓ᴸ Core.Block.height) ∘′ uncurry List⁺._∷_) Core.empty
       ∘ uncons

------------------------------------------------------------------------
-- Basic building blocks

fail : Doc
fail = []

text : String → Doc
text = filter (Core.valid width) ∘ pure ∘ Core.text

empty : Doc
empty = text ""

char : Char → Doc
char c = text (fromList (c ∷ []))

spaces : ℕ → Doc
spaces n = text (replicate n ' ')

semi colon comma space dot : Doc
semi = char ';'; colon = char ':'
comma = char ','; space = char ' '; dot = char '.'

backslash forwardslash equal : Doc
backslash = char '\\'; forwardslash = char '/'; equal = char '='

squote dquote : Doc
squote = char '\''; dquote = char '"'

lparen rparen langle rangle : Doc
lparen = char '('; rparen = char ')'
langle = char '<'; rangle = char '>'

lbrace rbrace llbrace rrbrace : Doc
lbrace = char '{'; rbrace = char '}'
llbrace = char '⦃'; rrbrace = char '⦄'

lbracket rbracket llbracket rrbracket : Doc
lbracket = char '['; rbracket = char ']'
llbracket = char '⟦'; rrbracket = char '⟧'

------------------------------------------------------------------------
-- Combining two documents

infixr 5 _<>_
_<>_ : Doc → Doc → Doc
xs <> ys = filter (Core.valid width) (Core._<>_ <$> xs ⊛ ys)

flush : Doc → Doc
flush = map Core.flush

infixr 5 _<+>_
_<+>_ : Doc → Doc → Doc
x <+> y = x <> space <> y

infixr 5 _$$_
_$$_ : Doc → Doc → Doc
x $$ y = flush x <> y

infixr 4 _<|>_
_<|>_ : Doc → Doc → Doc
x <|> y = x ++ y

------------------------------------------------------------------------
-- Combining lists of documents

foldDoc : (Doc → Doc → Doc) → List Doc → Doc
foldDoc _ []       = empty
foldDoc _ (x ∷ []) = x
foldDoc f (x ∷ xs) = f x (foldDoc f xs)

hsep vcat : List Doc → Doc
hsep = foldDoc _<+>_
vcat = foldDoc _$$_

sep : List Doc → Doc
sep [] = empty
sep xs = hsep xs <|> vcat xs

------------------------------------------------------------------------
-- Defined combinators

parens : Doc → Doc
parens d = lparen <> d <> rparen

commaSep : List Doc → Doc
commaSep = foldDoc (λ d e → d <> comma <+> e)

newline : Doc
newline = flush empty


text:
{-# OPTIONS --safe #-}
module Cubical.Data.NatPlusOne.MoreNats.AssocNat where

open import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base public
open import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical