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

open import lib.Basics
open import lib.types.FunctionSeq
open import lib.types.Nat
open import lib.types.Pointed
open import lib.types.Suspension.Core
open import lib.types.Suspension.Iterated

module lib.types.Suspension.IteratedEquivs where

Susp^-+ : ∀ {i} (m n : ℕ) {A : Type i}
  → Susp^ m (Susp^ n A) == Susp^ (m + n) A
Susp^-+ O n = idp
Susp^-+ (S m) n = ap Susp (Susp^-+ m n)

⊙Susp^-+ : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ⊙Susp^ m (⊙Susp^ n X) == ⊙Susp^ (m + n) X
⊙Susp^-+ 0 n {X} = idp
⊙Susp^-+ (S m) n {X} = ap ⊙Susp (Susp^-+ m n)

de⊙-⊙Susp^-+ : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ap de⊙ (⊙Susp^-+ m n {X}) == Susp^-+ m n {de⊙ X}
de⊙-⊙Susp^-+ 0 n {X} = idp
de⊙-⊙Susp^-+ (S m) n {X} = ∘-ap de⊙ ⊙Susp (Susp^-+ m n)

Susp^-+-0-r : ∀ {i} (m : ℕ) {A : Type i}
  → Susp^-+ m 0 ◃∙ ap (λ k → Susp^ k A) (+-unit-r m) ◃∎ =ₛ []
Susp^-+-0-r O {A} = =ₛ-in $
  ap (ap (λ k → Susp^ k A))
     (set-path ℕ-level (+-unit-r 0) idp)
Susp^-+-0-r (S m) {A} =
  ap Susp (Susp^-+ m 0) ◃∙
  ap (λ k → Susp^ k A) (+-unit-r (S m)) ◃∎
    =ₛ₁⟨ 1 & 1 & ap (ap (λ k → Susp^ k A)) $
                 set-path ℕ-level (+-unit-r (S m)) (ap S (+-unit-r m)) ⟩
  ap Susp (Susp^-+ m 0) ◃∙
  ap (λ k → Susp^ k A) (ap S (+-unit-r m)) ◃∎
    =ₛ₁⟨ 1 & 1 &
         ∘-ap (λ k → Susp^ k A) S (+-unit-r m) ∙
         ap-∘ Susp (λ k → Susp^ k A) (+-unit-r m) ⟩
  ap Susp (Susp^-+ m 0) ◃∙
  ap Susp (ap (λ k → Susp^ k A) (+-unit-r m)) ◃∎
    =ₛ⟨ ap-seq-=ₛ Susp (Susp^-+-0-r m) ⟩
  [] ∎ₛ

⊙Susp^-+-0-r : ∀ {i} (m : ℕ) {X : Ptd i}
  → ⊙Susp^-+ m 0 ◃∙ ap (λ k → ⊙Susp^ k X) (+-unit-r m) ◃∎ =ₛ []
⊙Susp^-+-0-r 0 {X} = =ₛ-in $
  ap (ap (λ k → ⊙Susp^ k X))
     (set-path ℕ-level (+-unit-r 0) idp)
⊙Susp^-+-0-r (S m) {X} =
  ap ⊙Susp (Susp^-+ m 0) ◃∙
  ap (λ k → ⊙Susp^ k X) (+-unit-r (S m)) ◃∎
    =ₛ₁⟨ 1 & 1 & ap (ap (λ k → ⊙Susp^ k X)) $
                 set-path ℕ-level (+-unit-r (S m)) (ap S (+-unit-r m)) ⟩
  ap ⊙Susp (Susp^-+ m 0) ◃∙
  ap (λ k → ⊙Susp^ k X) (ap S (+-unit-r m)) ◃∎
    =ₛ₁⟨ 1 & 1 &
         ∘-ap (λ k → ⊙Susp^ k X) S (+-unit-r m) ∙
         ap-∘ ⊙Susp (λ k → Susp^ k (de⊙ X)) (+-unit-r m) ⟩
  ap ⊙Susp (Susp^-+ m 0) ◃∙
  ap ⊙Susp (ap (λ k → Susp^ k (de⊙ X)) (+-unit-r m)) ◃∎
    =ₛ⟨ ap-seq-=ₛ ⊙Susp (Susp^-+-0-r m) ⟩
  [] ∎ₛ

Susp^-+-assoc-coh : ∀ {i} (m n o : ℕ) {A : Type i}
  → ap (Susp^ m) (Susp^-+ n o {A}) ◃∙
    Susp^-+ m (n + o) {A} ◃∎
    =ₛ
    Susp^-+ m n {Susp^ o A} ◃∙
    Susp^-+ (m + n) o ◃∙
    ap (λ k → Susp^ k A) (+-assoc m n o) ◃∎
Susp^-+-assoc-coh O n o {A} =
  ap (idf _) (Susp^-+ n o {A}) ◃∙
  idp ◃∎
    =ₛ₁⟨ 0 & 1 & ap-idf (Susp^-+ n o {A}) ⟩
  Susp^-+ n o {A} ◃∙
  idp ◃∎
    =ₛ₁⟨ 1 & 1 & ap (ap (λ k → Susp^ k A)) $
         set-path ℕ-level idp (+-assoc 0 n o) ⟩
  Susp^-+ n o {A} ◃∙
  ap (λ k → Susp^ k A) (+-assoc 0 n o) ◃∎
    =ₛ⟨ 0 & 0 & contract ⟩
  idp ◃∙
  Susp^-+ n o {A} ◃∙
  ap (λ k → Susp^ k A) (+-assoc 0 n o) ◃∎ ∎ₛ
Susp^-+-assoc-coh (S m) n o {A} =
  ap (Susp ∘ Susp^ m) (Susp^-+ n o {A}) ◃∙
  ap Susp (Susp^-+ m (n + o) {A}) ◃∎
    =ₛ₁⟨ 0 & 1 & ap-∘ Susp (Susp^ m) (Susp^-+ n o {A}) ⟩
  ap Susp (ap (Susp^ m) (Susp^-+ n o {A})) ◃∙
  ap Susp (Susp^-+ m (n + o) {A}) ◃∎
    =ₛ⟨ ap-seq-=ₛ Susp (Susp^-+-assoc-coh m n o) ⟩
  ap Susp (Susp^-+ m n) ◃∙
  ap Susp (Susp^-+ (m + n) o) ◃∙
  ap Susp (ap (λ k → Susp^ k A) (+-assoc m n o)) ◃∎
    =ₛ₁⟨ 2 & 1 & ∘-ap Susp (λ k → Susp^ k A) (+-assoc m n o) ∙
                 ap-∘ (λ k → Susp^ k A) S (+-assoc m n o) ⟩
  ap Susp (Susp^-+ m n) ◃∙
  ap Susp (Susp^-+ (m + n) o) ◃∙
  ap (λ k → Susp^ k A) (ap S (+-assoc m n o)) ◃∎
    =ₛ₁⟨ 2 & 1 & ap (ap (λ k → Susp^ k A)) $
                 set-path ℕ-level (ap S (+-assoc m n o)) (+-assoc (S m) n o) ⟩
  ap Susp (Susp^-+ m n) ◃∙
  ap Susp (Susp^-+ (m + n) o) ◃∙
  ap (λ k → Susp^ k A) (+-assoc (S m) n o) ◃∎ ∎ₛ

⊙Susp^-+-assoc-coh : ∀ {i} (m n o : ℕ) {X : Ptd i}
  → ap (⊙Susp^ m) (⊙Susp^-+ n o {X}) ◃∙
    ⊙Susp^-+ m (n + o) {X} ◃∎
    =ₛ
    ⊙Susp^-+ m n {⊙Susp^ o X} ◃∙
    ⊙Susp^-+ (m + n) o ◃∙
    ap (λ k → ⊙Susp^ k X) (+-assoc m n o) ◃∎
⊙Susp^-+-assoc-coh O n o {X} =
  ap (idf _) (⊙Susp^-+ n o) ◃∙
  idp ◃∎
    =ₛ₁⟨ 0 & 1 & ap-idf (⊙Susp^-+ n o) ⟩
  ⊙Susp^-+ n o ◃∙
  idp ◃∎
    =ₛ₁⟨ 1 & 1 & ap (ap (λ k → ⊙Susp^ k X)) $
                 set-path ℕ-level idp (+-assoc 0 n o) ⟩
  ⊙Susp^-+ n o ◃∙
  ap (λ k → ⊙Susp^ k X) (+-assoc 0 n o) ◃∎
    =ₛ⟨ 0 & 0 & contract ⟩
  idp ◃∙
  ⊙Susp^-+ n o ◃∙
  ap (λ k → ⊙Susp^ k X) (+-assoc 0 n o) ◃∎ ∎ₛ
⊙Susp^-+-assoc-coh (S m) n o {X} =
  ap (⊙Susp ∘ Susp^ m ∘ de⊙) (⊙Susp^-+ n o {X}) ◃∙
  ap ⊙Susp (Susp^-+ m (n + o) {de⊙ X}) ◃∎
    =ₛ₁⟨ 0 & 1 & ap-∘ (⊙Susp ∘ Susp^ m) de⊙ (⊙Susp^-+ n o {X}) ⟩
  ap (⊙Susp ∘ Susp^ m) (ap de⊙ (⊙Susp^-+ n o {X})) ◃∙
  ap ⊙Susp (Susp^-+ m (n + o) {de⊙ X}) ◃∎
    =ₛ₁⟨ 0 & 1 & ap (ap (⊙Susp ∘ Susp^ m)) (de⊙-⊙Susp^-+ n o {X}) ⟩
  ap (⊙Susp ∘ Susp^ m) (Susp^-+ n o {de⊙ X}) ◃∙
  ap ⊙Susp (Susp^-+ m (n + o) {de⊙ X}) ◃∎
    =ₛ₁⟨ 0 & 1 & ap-∘ ⊙Susp (Susp^ m) (Susp^-+ n o {de⊙ X}) ⟩
  ap ⊙Susp (ap (Susp^ m) (Susp^-+ n o {de⊙ X})) ◃∙
  ap ⊙Susp (Susp^-+ m (n + o) {de⊙ X}) ◃∎
    =ₛ⟨ ap-seq-=ₛ ⊙Susp (Susp^-+-assoc-coh m n o) ⟩
  ap ⊙Susp (Susp^-+ m n) ◃∙
  ap ⊙Susp (Susp^-+ (m + n) o) ◃∙
  ap ⊙Susp (ap (λ k → Susp^ k (de⊙ X)) (+-assoc m n o)) ◃∎
    =ₛ₁⟨ 2 & 1 & ∘-ap ⊙Susp (λ k → Susp^ k (de⊙ X)) (+-assoc m n o) ∙
                 ap-∘ (λ k → ⊙Susp^ k X) S (+-assoc m n o) ⟩
  ap ⊙Susp (Susp^-+ m n) ◃∙
  ap ⊙Susp (Susp^-+ (m + n) o) ◃∙
  ap (λ k → ⊙Susp^ k X) (ap S (+-assoc m n o)) ◃∎
    =ₛ₁⟨ 2 & 1 & ap (ap (λ k → ⊙Susp^ k X)) $
                 set-path ℕ-level (ap S (+-assoc m n o)) (+-assoc (S m) n o) ⟩
  ap ⊙Susp (Susp^-+ m n) ◃∙
  ap ⊙Susp (Susp^-+ (m + n) o) ◃∙
  ap (λ k → ⊙Susp^ k X) (+-assoc (S m) n o) ◃∎ ∎ₛ

Susp^-comm-seq : ∀ {i} (m n : ℕ) {A : Type i}
  → Susp^ m (Susp^ n A) =-= Susp^ n (Susp^ m A)
Susp^-comm-seq m n {A} =
  Susp^ m (Susp^ n A)
    =⟪ Susp^-+ m n ⟫
  Susp^ (m + n) A
    =⟪ ap (λ k → Susp^ k A) (+-comm m n) ⟫
  Susp^ (n + m) A
    =⟪ ! (Susp^-+ n m) ⟫
  Susp^ n (Susp^ m A) ∎∎

Susp^-comm : ∀ {i} (m n : ℕ) {A : Type i}
  → Susp^ m (Susp^ n A) == Susp^ n (Susp^ m A)
Susp^-comm m n {A} = ↯ (Susp^-comm-seq m n {A})

⊙Susp^-comm-seq : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ⊙Susp^ m (⊙Susp^ n X) =-= ⊙Susp^ n (⊙Susp^ m X)
⊙Susp^-comm-seq m n {X} =
  ⊙Susp^ m (⊙Susp^ n X)
    =⟪ ⊙Susp^-+ m n ⟫
  ⊙Susp^ (m + n) X
    =⟪ ap (λ k → ⊙Susp^ k X) (+-comm m n) ⟫
  ⊙Susp^ (n + m) X
    =⟪ ! (⊙Susp^-+ n m) ⟫
  ⊙Susp^ n (⊙Susp^ m X) ∎∎

⊙Susp^-comm : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ⊙Susp^ m (⊙Susp^ n X) == ⊙Susp^ n (⊙Susp^ m X)
⊙Susp^-comm m n {X} = ↯ (⊙Susp^-comm-seq m n {X})

de⊙-⊙Susp^-comm : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ap de⊙ (⊙Susp^-comm m n {X}) == Susp^-comm m n {de⊙ X}
de⊙-⊙Susp^-comm m n {X} = =ₛ-out {t = Susp^-comm m n {de⊙ X} ◃∎} $
  ap de⊙ (⊙Susp^-comm m n {X}) ◃∎
    =ₛ⟨ ap-seq-∙ de⊙ (⊙Susp^-comm-seq m n {X}) ⟩
  ap de⊙ (⊙Susp^-+ m n) ◃∙
  ap de⊙ (ap (λ k → ⊙Susp^ k X) (+-comm m n)) ◃∙
  ap de⊙ (! (⊙Susp^-+ n m)) ◃∎
    =ₛ₁⟨ 0 & 1 & de⊙-⊙Susp^-+ m n ⟩
  Susp^-+ m n ◃∙
  ap de⊙ (ap (λ k → ⊙Susp^ k X) (+-comm m n)) ◃∙
  ap de⊙ (! (⊙Susp^-+ n m)) ◃∎
    =ₛ₁⟨ 1 & 1 & ∘-ap de⊙ (λ k → ⊙Susp^ k X) (+-comm m n) ⟩
  Susp^-+ m n ◃∙
  ap (λ k → Susp^ k (de⊙ X)) (+-comm m n) ◃∙
  ap de⊙ (! (⊙Susp^-+ n m)) ◃∎
    =ₛ₁⟨ 2 & 1 & ap-! de⊙ (⊙Susp^-+ n m) ⟩
  Susp^-+ m n ◃∙
  ap (λ k → Susp^ k (de⊙ X)) (+-comm m n) ◃∙
  ! (ap de⊙ (⊙Susp^-+ n m)) ◃∎
    =ₛ₁⟨ 2 & 1 & ap ! (de⊙-⊙Susp^-+ n m) ⟩
  Susp^-+ m n ◃∙
  ap (λ k → Susp^ k (de⊙ X)) (+-comm m n) ◃∙
  ! (Susp^-+ n m) ◃∎
    =ₛ⟨ contract ⟩
  Susp^-comm m n ◃∎ ∎ₛ

⊙Susp^-swap : ∀ {i} (m n : ℕ) {X : Ptd i}
  → ⊙Susp^ m (⊙Susp^ n X) ⊙→ ⊙Susp^ n (⊙Susp^ m X)
⊙Susp^-swap m n {X} = ⊙coe (⊙Susp^-comm m n {X})

abstract
  ⊙Susp^-comm-diag : ∀ {i} (m : ℕ) {X : Ptd i}
    → ⊙Susp^-comm m m {X} ◃∎ =ₛ []
  ⊙Susp^-comm-diag m {X} =
    ↯ (⊙Susp^-comm-seq m m {X}) ◃∎
      =ₛ⟨ expand (⊙Susp^-comm-seq m m {X}) ⟩
    ⊙Susp^-+ m m ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm m m) ◃∙
    ! (⊙Susp^-+ m m) ◃∎
      =ₛ₁⟨ 1 & 1 & ap (ap (λ k → ⊙Susp^ k X)) (set-path ℕ-level (+-comm m m) idp) ⟩
    ⊙Susp^-+ m m ◃∙
    idp ◃∙
    ! (⊙Susp^-+ m m) ◃∎
      =ₛ⟨ 1 & 1 & expand [] ⟩
    ⊙Susp^-+ m m ◃∙
    ! (⊙Susp^-+ m m) ◃∎
      =ₛ⟨ seq-!-inv-r (⊙Susp^-+ m m ◃∎) ⟩
    [] ∎ₛ

  Susp^-comm-! : ∀ {i} (m n : ℕ) {A : Type i}
    → ! (Susp^-comm m n {A}) == Susp^-comm n m
  Susp^-comm-! m n {A} = =ₛ-out $
    ! (↯ (Susp^-comm-seq m n {A})) ◃∎
      =ₛ⟨ !-∙-seq (Susp^-comm-seq m n {A}) ⟩
    ! (! (Susp^-+ n m)) ◃∙
    ! (ap (λ k → Susp^ k A) (+-comm m n)) ◃∙
    ! (Susp^-+ m n) ◃∎
      =ₛ₁⟨ 0 & 1 & !-! (Susp^-+ n m) ⟩
    Susp^-+ n m ◃∙
    ! (ap (λ k → Susp^ k A) (+-comm m n)) ◃∙
    ! (Susp^-+ m n) ◃∎
      =ₛ₁⟨ 1 & 1 & !-ap (λ k → Susp^ k A) (+-comm m n) ⟩
    Susp^-+ n m ◃∙
    ap (λ k → Susp^ k A) (! (+-comm m n)) ◃∙
    ! (Susp^-+ m n) ◃∎
      =ₛ₁⟨ 1 & 1 & ap (ap (λ k → Susp^ k A)) $
           set-path ℕ-level (! (+-comm m n)) (+-comm n m) ⟩
    Susp^-+ n m ◃∙
    ap (λ k → Susp^ k A) (+-comm n m) ◃∙
    ! (Susp^-+ m n) ◃∎ ∎ₛ

  ⊙Susp^-comm-! : ∀ {i} (m n : ℕ) {X : Ptd i}
    → ! (⊙Susp^-comm m n {X}) == ⊙Susp^-comm n m
  ⊙Susp^-comm-! m n {X} = =ₛ-out $
    ! (↯ (⊙Susp^-comm-seq m n {X})) ◃∎
      =ₛ⟨ !-∙-seq (⊙Susp^-comm-seq m n {X}) ⟩
    ! (! (⊙Susp^-+ n m)) ◃∙
    ! (ap (λ k → ⊙Susp^ k X) (+-comm m n)) ◃∙
    ! (⊙Susp^-+ m n) ◃∎
      =ₛ₁⟨ 0 & 1 & !-! (⊙Susp^-+ n m) ⟩
    ⊙Susp^-+ n m ◃∙
    ! (ap (λ k → ⊙Susp^ k X) (+-comm m n)) ◃∙
    ! (⊙Susp^-+ m n) ◃∎
      =ₛ₁⟨ 1 & 1 & !-ap (λ k → ⊙Susp^ k X) (+-comm m n) ⟩
    ⊙Susp^-+ n m ◃∙
    ap (λ k → ⊙Susp^ k X) (! (+-comm m n)) ◃∙
    ! (⊙Susp^-+ m n) ◃∎
      =ₛ₁⟨ 1 & 1 & ap (ap (λ k → ⊙Susp^ k X)) $
           set-path ℕ-level (! (+-comm m n)) (+-comm n m) ⟩
    ⊙Susp^-+ n m ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm n m) ◃∙
    ! (⊙Susp^-+ m n) ◃∎ ∎ₛ

  ⊙Susp^-comm-0-r : ∀ {i} (m : ℕ) (X : Ptd i)
    → ⊙Susp^-comm m 0 {X} == idp
  ⊙Susp^-comm-0-r m X = =ₛ-out $
    ⊙Susp^-+ m 0 ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm m 0) ◃∙
    ! (⊙Susp^-+ 0 m) ◃∎
      =ₛ⟨ 2 & 1 & expand [] ⟩
    ⊙Susp^-+ m 0 ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm m 0) ◃∎
      =ₛ₁⟨ 1 & 1 & ap (ap (λ k → ⊙Susp^ k X)) $
                  set-path ℕ-level (+-comm m 0) (+-unit-r m) ⟩
    ⊙Susp^-+ m 0 ◃∙
    ap (λ k → ⊙Susp^ k X) (+-unit-r m) ◃∎
      =ₛ⟨ ⊙Susp^-+-0-r m ⟩
    [] ∎ₛ

  ⊙Susp^-comm-0-l : ∀ {i} (n : ℕ) (X : Ptd i)
    → ⊙Susp^-comm 0 n {X} == idp
  ⊙Susp^-comm-0-l n X =
    ⊙Susp^-comm 0 n {X}
      =⟨ ! (⊙Susp^-comm-! n 0 {X}) ⟩
    ! (⊙Susp^-comm n 0 {X})
      =⟨ ap ! (⊙Susp^-comm-0-r n X) ⟩
    idp =∎

  ⊙Susp^-comm-S-r : ∀ {i} (m n : ℕ) {X : Ptd i}
    → ⊙Susp^-comm m (S n) {X} ◃∎ =ₛ ⊙Susp^-comm m 1 {⊙Susp^ n X} ◃∙ ap ⊙Susp (Susp^-comm m n) ◃∎
  ⊙Susp^-comm-S-r m n {X} =
    ⊙Susp^-comm m (S n) {X} ◃∎
      =ₛ⟨ expand (⊙Susp^-comm-seq m (S n) {X}) ⟩
    ⊙Susp^-+ m (S n) ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm m (S n)) ◃∙
    ! (⊙Susp^-+ (S n) m {X}) ◃∎
      =ₛ⟨ 0 & 0 & contract ⟩
    idp ◃∙
    ⊙Susp^-+ m (S n) ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm m (S n)) ◃∙
    ! (⊙Susp^-+ (S n) m {X}) ◃∎
      =ₛ⟨ 0 & 2 & ⊙Susp^-+-assoc-coh m 1 n ⟩
    ⊙Susp^-+ m 1 ◃∙
    ⊙Susp^-+ (m + 1) n ◃∙
    ap (λ k → ⊙Susp^ k X) (+-assoc m 1 n) ◃∙
    ap (λ k → ⊙Susp^ k X) (+-comm m (S n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ⟨ 2 & 2 & ap-seq-=ₛ (λ k → ⊙Susp^ k X) $
          =ₛ-in {s = +-assoc m 1 n ◃∙ +-comm m (S n) ◃∎}
                {t = ap (_+ n) (+-comm m 1) ◃∙ ap S (+-comm m n) ◃∎} $
          set-path ℕ-level _ _ ⟩
    ⊙Susp^-+ m 1 ◃∙
    ⊙Susp^-+ (m + 1) n ◃∙
    ap (λ k → ⊙Susp^ k X) (ap (_+ n) (+-comm m 1)) ◃∙
    ap (λ k → ⊙Susp^ k X) (ap S (+-comm m n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ₁⟨ 2 & 1 & ∘-ap (λ k → ⊙Susp^ k X) (_+ n) (+-comm m 1) ⟩
    ⊙Susp^-+ m 1 ◃∙
    ⊙Susp^-+ (m + 1) n ◃∙
    ap (λ k → ⊙Susp^ (k + n) X) (+-comm m 1) ◃∙
    ap (λ k → ⊙Susp^ k X) (ap S (+-comm m n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ⟨ 1 & 2 & !ₛ $ homotopy-naturality
            (λ l → ⊙Susp^ l (⊙Susp^ n X))
            (λ l → ⊙Susp^ (l + n) X)
            (λ l → ⊙Susp^-+ l n)
            (+-comm m 1) ⟩
    ⊙Susp^-+ m 1 ◃∙
    ap (λ l → ⊙Susp^ l (⊙Susp^ n X)) (+-comm m 1) ◃∙
    ap ⊙Susp (Susp^-+ m n) ◃∙
    ap (λ k → ⊙Susp^ k X) (ap S (+-comm m n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ⟨ 2 & 0 & contract ⟩
    ⊙Susp^-+ m 1 ◃∙
    ap (λ l → ⊙Susp^ l (⊙Susp^ n X)) (+-comm m 1) ◃∙
    idp ◃∙
    ap ⊙Susp (Susp^-+ m n) ◃∙
    ap (λ k → ⊙Susp^ k X) (ap S (+-comm m n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ⟨ 0 & 3 & contract ⟩
    ⊙Susp^-comm m 1 ◃∙
    ap ⊙Susp (Susp^-+ m n) ◃∙
    ap (λ k → ⊙Susp^ k X) (ap S (+-comm m n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ₁⟨ 2 & 1 & ∘-ap (λ k → ⊙Susp^ k X) S (+-comm m n) ∙
                   ap-∘ ⊙Susp (λ k → Susp^ k (de⊙ X)) (+-comm m n) ⟩
    ⊙Susp^-comm m 1 ◃∙
    ap ⊙Susp (Susp^-+ m n) ◃∙
    ap ⊙Susp (ap (λ k → Susp^ k (de⊙ X)) (+-comm m n)) ◃∙
    ! (ap ⊙Susp (Susp^-+ n m)) ◃∎
      =ₛ₁⟨ 3 & 1 & !-ap ⊙Susp (Susp^-+ n m) ⟩
    ⊙Susp^-comm m 1 ◃∙
    ap ⊙Susp (Susp^-+ m n) ◃∙
    ap ⊙Susp (ap (λ k → Susp^ k (de⊙ X)) (+-comm m n)) ◃∙
    ap ⊙Susp (! (Susp^-+ n m)) ◃∎
      =ₛ⟨ 1 & 3 & ∙-ap-seq ⊙Susp (Susp^-comm-seq m n) ⟩
    ⊙Susp^-comm m 1 ◃∙
    ap ⊙Susp (Susp^-comm m n) ◃∎ ∎ₛ

  ⊙Susp^-comm-S-l : ∀ {i} (m n : ℕ) {X : Ptd i}
    → ⊙Susp^-comm (S m) n {X} ◃∎ =ₛ ap ⊙Susp (Susp^-comm m n) ◃∙ ⊙Susp^-comm 1 n {⊙Susp^ m X} ◃∎
  ⊙Susp^-comm-S-l m n {X} =
    ⊙Susp^-comm (S m) n {X} ◃∎
      =ₛ₁⟨ ! (⊙Susp^-comm-! n (S m) {X}) ⟩
    ! (⊙Susp^-comm n (S m) {X}) ◃∎
      =ₛ⟨ !-=ₛ (⊙Susp^-comm-S-r n m {X}) ⟩
    ! (ap ⊙Susp (Susp^-comm n m)) ◃∙
    ! (⊙Susp^-comm n 1) ◃∎
      =ₛ₁⟨ 0 & 1 & !-ap ⊙Susp (Susp^-comm n m) ⟩
    ap ⊙Susp (! (Susp^-comm n m)) ◃∙
    ! (⊙Susp^-comm n 1) ◃∎
      =ₛ₁⟨ 0 & 1 & ap (ap ⊙Susp) (Susp^-comm-! n m) ⟩
    ap ⊙Susp (Susp^-comm m n) ◃∙
    ! (⊙Susp^-comm n 1) ◃∎
      =ₛ₁⟨ 1 & 1 & ⊙Susp^-comm-! n 1 ⟩
    ap ⊙Susp (Susp^-comm m n) ◃∙
    ⊙Susp^-comm 1 n ◃∎ ∎ₛ

  ⊙Susp^-comm-S-1 : ∀ {i} (m : ℕ) {X : Ptd i}
    → ⊙Susp^-comm (S m) 1 {X} == ap ⊙Susp (Susp^-comm m 1 {de⊙ X})
  ⊙Susp^-comm-S-1 m {X} = =ₛ-out $
    ⊙Susp^-comm (S m) 1 {X} ◃∎
      =ₛ⟨ ⊙Susp^-comm-S-l m 1 ⟩
    ap ⊙Susp (Susp^-comm m 1) ◃∙
    ⊙Susp^-comm 1 1 ◃∎
      =ₛ⟨ 1 & 1 & ⊙Susp^-comm-diag 1 ⟩
    ap ⊙Susp (Susp^-comm m 1) ◃∎ ∎ₛ

  ⊙Susp^-comm-1-S : ∀ {i} (n : ℕ) {X : Ptd i}
    → ⊙Susp^-comm 1 (S n) {X} == ap ⊙Susp (Susp^-comm 1 n {de⊙ X})
  ⊙Susp^-comm-1-S n {X} =
    ⊙Susp^-comm 1 (S n) {X}
      =⟨ ! (⊙Susp^-comm-! (S n) 1 {X}) ⟩
    ! (⊙Susp^-comm (S n) 1 {X})
      =⟨ ap ! (⊙Susp^-comm-S-1 n {X}) ⟩
    ! (ap ⊙Susp (Susp^-comm n 1 {de⊙ X}))
      =⟨ !-ap ⊙Susp (Susp^-comm n 1 {de⊙ X}) ⟩
    ap ⊙Susp (! (Susp^-comm n 1 {de⊙ X}))
      =⟨ ap (ap ⊙Susp) (Susp^-comm-! n 1 {de⊙ X}) ⟩
    ap ⊙Susp (Susp^-comm 1 n {de⊙ X}) =∎

  ⊙Susp^-comm-S-S : ∀ {i} (m n : ℕ) {X : Ptd i}
    → ⊙Susp^-comm (S m) (S n) {X} == ap ⊙Susp (Susp^-comm m (S n) ∙ Susp^-comm 1 n)
  ⊙Susp^-comm-S-S m n {X} = =ₛ-out $
    ⊙Susp^-comm (S m) (S n) {X} ◃∎
      =ₛ⟨ ⊙Susp^-comm-S-l m (S n) ⟩
    ap ⊙Susp (Susp^-comm m (S n)) ◃∙
    ⊙Susp^-comm 1 (S n) ◃∎
      =ₛ₁⟨ 1 & 1 & ⊙Susp^-comm-1-S n ⟩
    ap ⊙Susp (Susp^-comm m (S n)) ◃∙
    ap ⊙Susp (Susp^-comm 1 n) ◃∎
      =ₛ⟨ ∙-ap-seq ⊙Susp (Susp^-comm m (S n) ◃∙ Susp^-comm 1 n ◃∎) ⟩
    ap ⊙Susp (Susp^-comm m (S n) ∙ Susp^-comm 1 n) ◃∎ ∎ₛ

abstract
  Susp^-+-natural : ∀ {i j} (m n : ℕ) {A : Type i} {B : Type j} (f : A → B)
    → coe (Susp^-+ m n) ∘ Susp^-fmap m (Susp^-fmap n f) ∼
      Susp^-fmap (m + n) f ∘ coe (Susp^-+ m n)
  Susp^-+-natural O n f sa = idp
  Susp^-+-natural (S m) n f sa =
    transport Susp (Susp^-+ m n) (Susp^-fmap (S m) (Susp^-fmap n f) sa)
      =⟨ transport-Susp (Susp^-+ m n) (Susp^-fmap (S m) (Susp^-fmap n f) sa) ⟩
    Susp-fmap (coe (Susp^-+ m n)) (Susp^-fmap (S m) (Susp^-fmap n f) sa)
      =⟨ ! (Susp-fmap-∘ (coe (Susp^-+ m n)) (Susp^-fmap m (Susp^-fmap n f)) sa) ⟩
    Susp-fmap (coe (Susp^-+ m n) ∘ Susp^-fmap m (Susp^-fmap n f)) sa
      =⟨ ap (λ f → Susp-fmap f sa) (λ= (Susp^-+-natural m n f)) ⟩
    Susp-fmap (Susp^-fmap (m + n) f ∘ coe (Susp^-+ m n)) sa
      =⟨ Susp-fmap-∘ (Susp^-fmap (m + n) f) (coe (Susp^-+ m n)) sa ⟩
    Susp^-fmap (S m + n) f (Susp-fmap (coe (Susp^-+ m n)) sa)
      =⟨ ap (Susp^-fmap (S m + n) f) (! (transport-Susp (Susp^-+ m n) sa)) ⟩
    Susp^-fmap (S m + n) f (transport Susp (Susp^-+ m n) sa) =∎

  ⊙Susp^-+-natural : ∀ {i j} (m n : ℕ) {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
    → ⊙coe (⊙Susp^-+ m n) ⊙∘ ⊙Susp^-fmap m (⊙Susp^-fmap n f) ==
      ⊙Susp^-fmap (m + n) f ⊙∘ ⊙coe (⊙Susp^-+ m n)
  ⊙Susp^-+-natural 0 n f = ⊙λ= (⊙∘-unit-l _)
  ⊙Susp^-+-natural (S m) n f =
    ⊙coe (ap ⊙Susp (Susp^-+ m n)) ⊙∘
    ⊙Susp^-fmap (S m) (⊙Susp^-fmap n f)
      =⟨ ap (_⊙∘ ⊙Susp^-fmap (S m) (⊙Susp^-fmap n f)) $
         ! (⊙transport-⊙coe ⊙Susp (Susp^-+ m n)) ∙
         ⊙transport-⊙Susp (Susp^-+ m n) ⟩
    ⊙Susp-fmap (coe (Susp^-+ m n)) ⊙∘
    ⊙Susp^-fmap (S m) (⊙Susp^-fmap n f)
      =⟨ ! $ ⊙Susp-fmap-∘ (coe (Susp^-+ m n)) (Susp^-fmap m (Susp^-fmap n (fst f))) ⟩
    ⊙Susp-fmap (coe (Susp^-+ m n) ∘ Susp^-fmap m (Susp^-fmap n (fst f)))
      =⟨ ap ⊙Susp-fmap (λ= (Susp^-+-natural m n (fst f))) ⟩
    ⊙Susp-fmap (Susp^-fmap (m + n) (fst f) ∘ coe (Susp^-+ m n))
      =⟨ ⊙Susp-fmap-∘ (Susp^-fmap (m + n) (fst f)) (coe (Susp^-+ m n)) ⟩
    ⊙Susp-fmap (Susp^-fmap (m + n) (fst f)) ⊙∘
    ⊙Susp-fmap (coe (Susp^-+ m n))
      =⟨ ap (⊙Susp-fmap (Susp^-fmap (m + n) (fst f)) ⊙∘_) $
         ! (⊙transport-⊙Susp (Susp^-+ m n)) ∙
         ⊙transport-⊙coe ⊙Susp (Susp^-+ m n) ⟩
    ⊙Susp-fmap (Susp^-fmap (m + n) (fst f)) ⊙∘
    ⊙coe (ap ⊙Susp (Susp^-+ m n)) =∎

  Susp^-+-natural' : ∀ {i j} (m n : ℕ) {A : Type i} {B : Type j} (f : A → B)
    → Susp^-fmap m (Susp^-fmap n f) ∘ coe (! (Susp^-+ m n)) ∼
      coe (! (Susp^-+ m n)) ∘ Susp^-fmap (m + n) f
  Susp^-+-natural' m n f sa =
    Susp^-fmap m (Susp^-fmap n f) (coe (! (Susp^-+ m n)) sa)
      =⟨ ap (λ p → coe p (Susp^-fmap m (Susp^-fmap n f) (coe (! (Susp^-+ m n)) sa))) $
         ! $ !-inv-r (Susp^-+ m n) ⟩
    coe (Susp^-+ m n ∙ ! (Susp^-+ m n))
        (Susp^-fmap m (Susp^-fmap n f) (coe (! (Susp^-+ m n)) sa))
      =⟨ coe-∙ (Susp^-+ m n) (! (Susp^-+ m n))
               (Susp^-fmap m (Susp^-fmap n f) (coe (! (Susp^-+ m n)) sa)) ⟩
    coe (! (Susp^-+ m n)) (coe (Susp^-+ m n) (Susp^-fmap m (Susp^-fmap n f) (coe (! (Susp^-+ m n)) sa)))
      =⟨ ap (coe (! (Susp^-+ m n))) $
         Susp^-+-natural m n f (coe (! (Susp^-+ m n)) sa) ⟩
    coe (! (Susp^-+ m n)) (Susp^-fmap (m + n) f (coe (Susp^-+ m n) (coe (! (Susp^-+ m n)) sa)))
      =⟨ ap (coe (! (Susp^-+ m n)) ∘ Susp^-fmap (m + n) f) $
         ! $ coe-∙ (! (Susp^-+ m n)) (Susp^-+ m n) sa ⟩
    coe (! (Susp^-+ m n)) (Susp^-fmap (m + n) f (coe (! (Susp^-+ m n) ∙ Susp^-+ m n) sa))
      =⟨ ap (λ p → coe (! (Susp^-+ m n)) (Susp^-fmap (m + n) f (coe p sa))) $
         !-inv-l (Susp^-+ m n) ⟩
    coe (! (Susp^-+ m n)) (Susp^-fmap (m + n) f sa) =∎

  ⊙Susp^-+-natural' : ∀ {i j} (m n : ℕ) {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
    → ⊙Susp^-fmap m (⊙Susp^-fmap n f) ⊙∘ ⊙coe (! (⊙Susp^-+ m n)) ==
      ⊙coe (! (⊙Susp^-+ m n)) ⊙∘ ⊙Susp^-fmap (m + n) f
  ⊙Susp^-+-natural' m n f =
    ⊙Susp^-fmap m (⊙Susp^-fmap n f) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ap (_⊙∘ ⊙coe (! (⊙Susp^-+ m n))) $
         ! $ ⊙λ= $ ⊙∘-unit-l (⊙Susp^-fmap m (⊙Susp^-fmap n f)) ⟩
    (⊙idf _ ⊙∘
     ⊙Susp^-fmap m (⊙Susp^-fmap n f)) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ap (_⊙∘ ⊙coe (! (⊙Susp^-+ m n))) $
         ap (_⊙∘ ⊙Susp^-fmap m (⊙Susp^-fmap n f)) $
         ap ⊙coe (! (!-inv-r (⊙Susp^-+ m n))) ∙
         =⊙∘-out (⊙coe-∙ (⊙Susp^-+ m n) (! (⊙Susp^-+ m n))) ⟩
    ((⊙coe (! (⊙Susp^-+ m n)) ⊙∘
      ⊙coe (⊙Susp^-+ m n)) ⊙∘
     ⊙Susp^-fmap m (⊙Susp^-fmap n f)) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ap (_⊙∘ ⊙coe (! (⊙Susp^-+ m n))) $ ⊙λ= $
         ⊙∘-assoc (⊙coe (! (⊙Susp^-+ m n)))
                  (⊙coe (⊙Susp^-+ m n))
                  (⊙Susp^-fmap m (⊙Susp^-fmap n f)) ⟩
    (⊙coe (! (⊙Susp^-+ m n)) ⊙∘
     ⊙coe (⊙Susp^-+ m n) ⊙∘
     ⊙Susp^-fmap m (⊙Susp^-fmap n f)) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ap (_⊙∘ ⊙coe (! (⊙Susp^-+ m n))) $
         ap (⊙coe (! (⊙Susp^-+ m n)) ⊙∘_) $
         ⊙Susp^-+-natural m n f ⟩
    (⊙coe (! (⊙Susp^-+ m n)) ⊙∘
     ⊙Susp^-fmap (m + n) f ⊙∘
     ⊙coe (⊙Susp^-+ m n)) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ⊙λ= $ ⊙∘-assoc
           (⊙coe (! (⊙Susp^-+ m n)))
           (⊙Susp^-fmap (m + n) f ⊙∘ ⊙coe (⊙Susp^-+ m n))
           (⊙coe (! (⊙Susp^-+ m n))) ⟩
    ⊙coe (! (⊙Susp^-+ m n)) ⊙∘
    (⊙Susp^-fmap (m + n) f ⊙∘
     ⊙coe (⊙Susp^-+ m n)) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ap (⊙coe (! (⊙Susp^-+ m n)) ⊙∘_) $ ⊙λ= $
         ⊙∘-assoc (⊙Susp^-fmap (m + n) f)
                  (⊙coe (⊙Susp^-+ m n))
                  (⊙coe (! (⊙Susp^-+ m n))) ⟩
    ⊙coe (! (⊙Susp^-+ m n)) ⊙∘
    ⊙Susp^-fmap (m + n) f ⊙∘
    ⊙coe (⊙Susp^-+ m n) ⊙∘
    ⊙coe (! (⊙Susp^-+ m n))
      =⟨ ap (⊙coe (! (⊙Susp^-+ m n)) ⊙∘_) $
         ap (⊙Susp^-fmap (m + n) f ⊙∘_) $
         ! (=⊙∘-out (⊙coe-∙ (! (⊙Susp^-+ m n)) (⊙Susp^-+ m n))) ∙
         ap ⊙coe (!-inv-l (⊙Susp^-+ m n)) ⟩
    ⊙coe (! (⊙Susp^-+ m n)) ⊙∘
    ⊙Susp^-fmap (m + n) f =∎

  Susp^-comm-natural : ∀ {i j} {A : Type i} {B : Type j} (m n : ℕ)
    (f : A → B)
    → coe (Susp^-comm m n) ∘ Susp^-fmap m (Susp^-fmap n f) ∼
      Susp^-fmap n (Susp^-fmap m f) ∘ coe (Susp^-comm m n)
  Susp^-comm-natural {A = A} {B = B} m n f s =
    coe (Susp^-comm m n) (Susp^-fmap m (Susp^-fmap n f) s)
      =⟨ coe-∙ (Susp^-+ m n)
               (ap (λ k → Susp^ k B) (+-comm m n) ∙ ! (Susp^-+ n m))
               (Susp^-fmap m (Susp^-fmap n f) s) ⟩
    coe (ap (λ k → Susp^ k B) (+-comm m n) ∙ ! (Susp^-+ n m))
        (coe (Susp^-+ m n) (Susp^-fmap m (Susp^-fmap n f) s))
      =⟨ ap (coe (ap (λ k → Susp^ k B) (+-comm m n) ∙ ! (Susp^-+ n m)))
            (Susp^-+-natural m n f s) ⟩
    coe (ap (λ k → Susp^ k B) (+-comm m n) ∙ ! (Susp^-+ n m))
        (Susp^-fmap (m + n) f (coe (Susp^-+ m n) s))
      =⟨ coe-∙ (ap (λ k → Susp^ k B) (+-comm m n))
               (! (Susp^-+ n m))
               (Susp^-fmap (m + n) f (coe (Susp^-+ m n) s)) ⟩
    coe (! (Susp^-+ n m))
        (transport (λ k → Susp^ k B) (+-comm m n)
          (Susp^-fmap (m + n) f (coe (Susp^-+ m n) s)))
      =⟨ ! $ ap (coe (! (Susp^-+ n m))) $
         app= (transp-naturality (λ {k} → Susp^-fmap k f) (+-comm m n))
              (coe (Susp^-+ m n) s) ⟩
    coe (! (Susp^-+ n m)) (Susp^-fmap (n + m) f
      (transport (λ k → Susp^ k A) (+-comm m n) (coe (Susp^-+ m n) s)))
      =⟨ ! $ Susp^-+-natural' n m f
           (transport (λ k → Susp^ k A) (+-comm m n) (coe (Susp^-+ m n) s)) ⟩
    Susp^-fmap n (Susp^-fmap m f)
      (coe (! (Susp^-+ n m)) (transport (λ k → Susp^ k A) (+-comm m n) (coe (Susp^-+ m n) s)))
      =⟨ ap (Susp^-fmap n (Susp^-fmap m f)) $ ! $
         coe-∙ (ap (λ k → Susp^ k A) (+-comm m n))
               (! (Susp^-+ n m))
               (coe (Susp^-+ m n) s) ⟩
    Susp^-fmap n (Susp^-fmap m f)
      (coe (ap (λ k → Susp^ k A) (+-comm m n) ∙ ! (Susp^-+ n m)) (coe (Susp^-+ m n) s))
      =⟨ ! $ ap (Susp^-fmap n (Susp^-fmap m f)) $
         coe-∙ (Susp^-+ m n) (ap (λ k → Susp^ k A) (+-comm m n) ∙ ! (Susp^-+ n m)) s ⟩
    Susp^-fmap n (Susp^-fmap m f) (coe (Susp^-comm m n) s) =∎

  ⊙Susp^-swap-natural : ∀ {i} {X Y : Ptd i} (m n : ℕ) (f : X ⊙→ Y)
    → ⊙Susp^-swap m n ◃⊙∘ ⊙Susp^-fmap m (⊙Susp^-fmap n f) ◃⊙idf
      =⊙∘
      ⊙Susp^-fmap n (⊙Susp^-fmap m f) ◃⊙∘ ⊙Susp^-swap m n ◃⊙idf
  ⊙Susp^-swap-natural {X = X} {Y = Y} m n f =
    ⊙Susp^-swap m n ◃⊙∘
    ⊙Susp^-fmap m (⊙Susp^-fmap n f) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙coe-∙ (⊙Susp^-+ m n)
                          (ap (λ k → ⊙Susp^ k Y) (+-comm m n) ∙ ! (⊙Susp^-+ n m)) ⟩
    ⊙coe (ap (λ k → ⊙Susp^ k Y) (+-comm m n) ∙ ! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙∘
    ⊙Susp^-fmap m (⊙Susp^-fmap n f) ◃⊙idf
      =⊙∘⟨ 1 & 2 & =⊙∘-in {gs = ⊙Susp^-fmap (m + n) f ◃⊙∘ ⊙coe (⊙Susp^-+ m n) ◃⊙idf} $
                   ⊙Susp^-+-natural m n f ⟩
    ⊙coe (ap (λ k → ⊙Susp^ k Y) (+-comm m n) ∙ ! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙Susp^-fmap (m + n) f ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙coe-∙ (ap (λ k → ⊙Susp^ k Y) (+-comm m n)) (! (⊙Susp^-+ n m)) ⟩
    ⊙coe (! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙coe (ap (λ k → ⊙Susp^ k Y) (+-comm m n)) ◃⊙∘
    ⊙Susp^-fmap (m + n) f ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ! $ ⊙transport-⊙coe (λ k → ⊙Susp^ k Y) (+-comm m n) ⟩
    ⊙coe (! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙transport (λ k → ⊙Susp^ k Y) (+-comm m n) ◃⊙∘
    ⊙Susp^-fmap (m + n) f ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘ (+-comm m n) (λ k → ⊙Susp^-fmap k f) ⟩
    ⊙coe (! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙Susp^-fmap (n + m) f ◃⊙∘
    ⊙transport (λ k → ⊙Susp^ k X) (+-comm m n) ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘₁⟨ 2 & 1 & ⊙transport-⊙coe (λ k → ⊙Susp^ k X) (+-comm m n) ⟩
    ⊙coe (! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙Susp^-fmap (n + m) f ◃⊙∘
    ⊙coe (ap (λ k → ⊙Susp^ k X) (+-comm m n)) ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘⟨ 0 & 2 & =⊙∘-in {gs = ⊙Susp^-fmap n (⊙Susp^-fmap m f) ◃⊙∘
                                ⊙coe (! (⊙Susp^-+ n m)) ◃⊙idf} $
           ! $ ⊙Susp^-+-natural' n m f ⟩
    ⊙Susp^-fmap n (⊙Susp^-fmap m f) ◃⊙∘
    ⊙coe (! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙coe (ap (λ k → ⊙Susp^ k X) (+-comm m n)) ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙coe-∙ (ap (λ k → ⊙Susp^ k X) (+-comm m n)) (! (⊙Susp^-+ n m)) ⟩
    ⊙Susp^-fmap n (⊙Susp^-fmap m f) ◃⊙∘
    ⊙coe (ap (λ k → ⊙Susp^ k X) (+-comm m n) ∙ ! (⊙Susp^-+ n m)) ◃⊙∘
    ⊙coe (⊙Susp^-+ m n) ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $
           ⊙coe-∙ (⊙Susp^-+ m n)
                  (ap (λ k → ⊙Susp^ k X) (+-comm m n) ∙ ! (⊙Susp^-+ n m)) ⟩
    ⊙Susp^-fmap n (⊙Susp^-fmap m f) ◃⊙∘
    ⊙Susp^-swap m n ◃⊙idf ∎⊙∘

Susp^-Susp-split-iso : ∀ {i} (n : ℕ) (A : Type i)
  → Susp (Susp^ n A) ≃ Susp^ n (Susp A)
Susp^-Susp-split-iso O A = ide _
Susp^-Susp-split-iso (S n) A = Susp-emap (Susp^-Susp-split-iso n A)

⊙Susp^-Susp-split-iso : ∀ {i} (n : ℕ) (A : Type i)
  → ⊙Susp (Susp^ n A) ⊙≃ ⊙Susp^ n (⊙Susp A)
⊙Susp^-Susp-split-iso O A = ⊙ide _
⊙Susp^-Susp-split-iso (S n) A = ⊙Susp-emap (Susp^-Susp-split-iso n A)


text:
open import Issue481PonderBase using (List)

module Issue481PonderImportMe (as bs : List) where

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2018-06-19, issue #3130
-- Produce parenthesized dot pattern .(p) instead of .p
-- when is a projection.

-- {-# OPTIONS -v reify.pat:80 #-}

record R : Set₁ where
  field p : Set
open R

data D : (R → Set) → Set₁ where
  c : D p

test : (f : R → Set) (x : D f) → Set₁
test f x = {!x!}  -- split on x

-- Expected:
-- test .(p) c = ?


text:
-- This is the preferred version of the integers in the library. Other
-- versions can be found in the MoreInts directory.
{-# OPTIONS --safe #-}
module Cubical.Data.Int.Base where

open import Cubical.Core.Everything
open import Cubical.Data.Bool
open import Cubical.Data.Nat hiding (_+_ ; _·_) renaming (isEven to isEvenℕ ; isOdd to isOddℕ)

infix  8 -_
infixl 7 _·_
infixl 6 _+_ _-_

data ℤ : Type₀ where
  pos    : (n : ℕ) → ℤ
  negsuc : (n : ℕ) → ℤ

neg : (n : ℕ) → ℤ
neg zero    = pos zero
neg (suc n) = negsuc n

sucℤ : ℤ → ℤ
sucℤ (pos n)          = pos (suc n)
sucℤ (negsuc zero)    = pos zero
sucℤ (negsuc (suc n)) = negsuc n

predℤ : ℤ → ℤ
predℤ (pos zero)    = negsuc zero
predℤ (pos (suc n)) = pos n
predℤ (negsuc n)    = negsuc (suc n)

isEven : ℤ → Bool
isEven (pos n) = isEvenℕ n
isEven (negsuc n) = isOddℕ n

isOdd : ℤ → Bool
isOdd (pos n) = isOddℕ n
isOdd (negsuc n) = isEvenℕ n

abs : ℤ → ℕ
abs (pos n) = n
abs (negsuc n) = suc n

_ℕ-_ : ℕ → ℕ → ℤ
a ℕ- 0 = pos a
0 ℕ- suc b = negsuc b
suc a ℕ- suc b = a ℕ- b

_+pos_ : ℤ → ℕ  → ℤ
z +pos 0 = z
z +pos (suc n) = sucℤ (z +pos n)

_+negsuc_ : ℤ → ℕ → ℤ
z +negsuc 0 = predℤ z
z +negsuc (suc n) = predℤ (z +negsuc n)

_+_ : ℤ → ℤ → ℤ
m + pos n = m +pos n
m + negsuc n = m +negsuc n

-_ : ℤ → ℤ
- pos zero = pos zero
- pos (suc n) = negsuc n
- negsuc n = pos (suc n)

_-_ : ℤ → ℤ → ℤ
m - n = m + (- n)

_·_ : ℤ → ℤ → ℤ
pos zero · m = pos zero
pos (suc n) · m = m + pos n · m
negsuc zero · m = - m
negsuc (suc n) · m = - m + negsuc n · m

-- Natural number and negative integer literals for ℤ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℤ : HasFromNat ℤ
  fromNatℤ = record { Constraint = λ _ → Unit ; fromNat = λ n → pos n }

instance
  fromNegℤ : HasFromNeg ℤ
  fromNegℤ = record { Constraint = λ _ → Unit ; fromNeg = λ n → neg n }

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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

open import Categories.Category.Core using (Category)

-- Defines BinaryProducts -- for when a Category has all Binary Products

module Categories.Category.BinaryProducts {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level hiding (suc)
open import Data.Product using (uncurry)

open Category 𝒞
open HomReasoning

open import Categories.Object.Product 𝒞
open import Categories.Morphism 𝒞 using (_≅_; module Iso)
open import Categories.Morphism.Reasoning 𝒞 using (pullʳ; pullˡ; elimʳ; cancelˡ)
open import Categories.Category.Monoidal.Core using (Monoidal)

open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor; appʳ; appˡ)

private
  variable
    A B C D X Y Z : Obj
    f f′ g g′ h i : A ⇒ B

record BinaryProducts : Set (levelOfTerm 𝒞) where

  infixr 7 _×_
  infixr 8 _⁂_
  infix 11 ⟨_,_⟩

  field
    product : ∀ {A B} → Product A B

  private
    module product {A} {B} = Product (product {A} {B})

  _×_ : Obj → Obj → Obj
  A × B = Product.A×B (product {A} {B})

  ×-comm : A × B ≅ B × A
  ×-comm = Commutative product product

  ×-assoc : X × Y × Z ≅ (X × Y) × Z
  ×-assoc = Associative product product product product

  open product hiding (⟨_,_⟩; ∘-distribʳ-⟨⟩) public

  -- define it like this instead of reexporting to redefine fixity
  ⟨_,_⟩ : X ⇒ A → X ⇒ B → X ⇒ A × B
  ⟨_,_⟩ = Product.⟨_,_⟩ product

  _⁂_ : A ⇒ B → C ⇒ D → A × C ⇒ B × D
  f ⁂ g = [ product ⇒ product ] f × g

  assocˡ : (A × B) × C ⇒ A × B × C
  assocˡ = _≅_.to ×-assoc

  assocʳ : A × B × C ⇒ (A × B) × C
  assocʳ = _≅_.from ×-assoc

  assocʳ∘assocˡ : assocʳ {A}{B}{C} ∘ assocˡ {A}{B}{C} ≈ id
  assocʳ∘assocˡ = Iso.isoʳ (_≅_.iso ×-assoc)

  assocˡ∘assocʳ : assocˡ {A}{B}{C} ∘ assocʳ {A}{B}{C} ≈ id
  assocˡ∘assocʳ = Iso.isoˡ (_≅_.iso ×-assoc)

  ⟨⟩-congʳ : f ≈ f′ → ⟨ f , g ⟩ ≈ ⟨ f′ , g ⟩
  ⟨⟩-congʳ pf = ⟨⟩-cong₂ pf Equiv.refl

  ⟨⟩-congˡ : g ≈ g′ → ⟨ f , g ⟩ ≈ ⟨ f , g′ ⟩
  ⟨⟩-congˡ pf = ⟨⟩-cong₂ Equiv.refl pf

  swap : A × B ⇒ B × A
  swap = ⟨ π₂ , π₁ ⟩

  -- TODO: this is probably harder to use than necessary because of this definition. Maybe make a version
  -- that doesn't have an explicit id in it, too?
  first : A ⇒ B → A × C ⇒ B × C
  first f = f ⁂ id

  second : C ⇒ D → A × C ⇒ A × D
  second g = id ⁂ g

  -- Just to make this more obvious
  π₁∘⁂ : π₁ ∘ (f ⁂ g) ≈ f ∘ π₁
  π₁∘⁂ {f = f} {g} = project₁

  π₂∘⁂ : π₂ ∘ (f ⁂ g) ≈ g ∘ π₂
  π₂∘⁂ {f = f} {g} = project₂

  ⁂-cong₂ : f ≈ g → h ≈ i → f ⁂ h ≈ g ⁂ i
  ⁂-cong₂ = [ product ⇒ product ]×-cong₂

  ⁂∘⟨⟩ : (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g ∘ g′ ⟩
  ⁂∘⟨⟩ = [ product ⇒ product ]×∘⟨⟩

  first∘⟨⟩ : first f ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g′ ⟩
  first∘⟨⟩ = [ product ⇒ product ]×id∘⟨⟩

  second∘⟨⟩ : second g ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f′ , g ∘ g′ ⟩
  second∘⟨⟩ = [ product ⇒ product ]id×∘⟨⟩

  ⁂∘⁂ : (f ⁂ g) ∘ (f′ ⁂ g′) ≈ (f ∘ f′) ⁂ (g ∘ g′)
  ⁂∘⁂ = [ product ⇒ product ⇒ product ]×∘×

  ⟨⟩∘ : ⟨ f , g ⟩ ∘ h ≈ ⟨ f ∘ h , g ∘ h ⟩
  ⟨⟩∘ = [ product ]⟨⟩∘

  first∘first : ∀ {C} → first {C = C} f ∘ first g ≈ first (f ∘ g)
  first∘first = [ product ⇒ product ⇒ product ]×id∘×id

  second∘second : ∀ {A} → second {A = A} f ∘ second g ≈ second (f ∘ g)
  second∘second = [ product ⇒ product ⇒ product ]id×∘id×

  first∘second : first f ∘ second g ≈ f ⁂ g
  first∘second {f = f} {g = g} = begin
    first f ∘ second g       ≈⟨ first∘⟨⟩ ⟩
    ⟨ f ∘ id ∘ π₁ , g ∘ π₂ ⟩ ≈⟨ ⟨⟩-congʳ (∘-resp-≈ʳ identityˡ) ⟩
    f ⁂ g                    ∎

  second∘first : second f ∘ first g ≈ g ⁂ f
  second∘first {f = f} {g = g} = begin
    second f ∘ first g ≈⟨ second∘⟨⟩ ⟩
    ⟨ g ∘ π₁ , f ∘ id ∘ π₂ ⟩ ≈⟨ ⟨⟩-congˡ (∘-resp-≈ʳ identityˡ) ⟩
    g ⁂ f ∎

  first↔second : first f ∘ second g ≈ second g ∘ first f
  first↔second = [ product ⇒ product , product ⇒ product ]first↔second

  firstid : ∀ {f : A ⇒ A} (g : A ⇒ C) → first {C = C} f ≈ id → f ≈ id
  firstid {f = f} g eq = begin
    f                    ≈˘⟨ elimʳ project₁ ⟩
    f ∘ π₁ ∘ ⟨ id , g ⟩  ≈⟨ pullˡ fπ₁≈π₁ ⟩
    π₁ ∘ ⟨ id , g ⟩      ≈⟨ project₁ ⟩
    id                   ∎
    where fπ₁≈π₁ = begin
            f ∘ π₁       ≈˘⟨ project₁ ⟩
            π₁ ∘ first f ≈⟨ refl⟩∘⟨ eq ⟩
            π₁ ∘ id      ≈⟨ identityʳ ⟩
            π₁           ∎

  swap∘⟨⟩ : swap ∘ ⟨ f , g ⟩ ≈ ⟨ g , f ⟩
  swap∘⟨⟩ {f = f} {g = g} = begin
    ⟨ π₂ , π₁ ⟩ ∘ ⟨ f , g ⟩             ≈⟨ ⟨⟩∘ ⟩
    ⟨ π₂ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ project₂ project₁ ⟩
    ⟨ g , f ⟩                           ∎

  swap∘⁂ : swap ∘ (f ⁂ g) ≈ (g ⁂ f) ∘ swap
  swap∘⁂ {f = f} {g = g} = begin
    swap ∘ (f ⁂ g)      ≈⟨ swap∘⟨⟩ ⟩
    ⟨ g ∘ π₂ , f ∘ π₁ ⟩  ≈˘⟨ ⁂∘⟨⟩ ⟩
    (g ⁂ f) ∘ swap      ∎

  swap∘swap : (swap {A}{B}) ∘ (swap {B}{A}) ≈ id
  swap∘swap = Equiv.trans swap∘⟨⟩ η

  assocʳ∘⟨⟩ : assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈ ⟨ ⟨ f , g ⟩ , h ⟩
  assocʳ∘⟨⟩ {f = f} {g = g} {h = h} = begin
    assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩
    ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    , (π₂ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    ⟩                          ≈⟨ ⟨⟩-cong₂ ⟨⟩∘ (pullʳ project₂) ⟩
    ⟨ ⟨ π₁        ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      , (π₁ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      ⟩
    , π₂ ∘ ⟨ g , h ⟩
    ⟩                          ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁
                                                     (pullʳ project₂ ○ project₁))
                                           project₂ ⟩
    ⟨ ⟨ f , g ⟩ , h ⟩          ∎

  assocˡ∘⟨⟩ : assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩ ≈ ⟨ f , ⟨ g , h ⟩ ⟩
  assocˡ∘⟨⟩ {f = f} {g = g} {h = h} = begin
    assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩          ≈˘⟨ refl⟩∘⟨ assocʳ∘⟨⟩ ⟩
    assocˡ ∘ assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈⟨ cancelˡ assocˡ∘assocʳ ⟩
    ⟨ f , ⟨ g , h ⟩ ⟩                   ∎

  assocʳ∘⁂ : assocʳ ∘ (f ⁂ (g ⁂ h)) ≈ ((f ⁂ g) ⁂ h) ∘ assocʳ
  assocʳ∘⁂ {f = f} {g = g} {h = h} =
    begin
      assocʳ ∘ (f ⁂ (g ⁂ h))
    ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
      assocʳ ∘ ⟨ f ∘ π₁ , ⟨ (g ∘ π₁) ∘ π₂ , (h ∘ π₂) ∘ π₂ ⟩ ⟩
    ≈⟨ assocʳ∘⟨⟩ ⟩
      ⟨ ⟨ f ∘ π₁ , (g ∘ π₁) ∘ π₂ ⟩ , (h ∘ π₂) ∘ π₂ ⟩
    ≈⟨ ⟨⟩-cong₂ (⟨⟩-congˡ assoc) assoc ⟩
      ⟨ ⟨ f ∘ π₁ , g ∘ π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
    ≈˘⟨ ⟨⟩-congʳ ⁂∘⟨⟩ ⟩
      ⟨ (f ⁂ g) ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
    ≈˘⟨ ⁂∘⟨⟩ ⟩
      ((f ⁂ g) ⁂ h) ∘ assocʳ
    ∎

  assocˡ∘⁂ : assocˡ ∘ ((f ⁂ g) ⁂ h) ≈ (f ⁂ (g ⁂ h)) ∘ assocˡ
  assocˡ∘⁂ {f = f} {g = g} {h = h} =
    begin
      assocˡ ∘ ((f ⁂ g) ⁂ h)
    ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
      assocˡ ∘ ⟨ ⟨ (f ∘ π₁) ∘ π₁ , (g ∘ π₂) ∘ π₁ ⟩ , h ∘ π₂ ⟩
    ≈⟨ assocˡ∘⟨⟩ ⟩
      ⟨ (f ∘ π₁) ∘ π₁ , ⟨ (g ∘ π₂) ∘ π₁ , h ∘ π₂ ⟩ ⟩
    ≈⟨ ⟨⟩-cong₂ assoc (⟨⟩-congʳ assoc) ⟩
      ⟨ f ∘ π₁ ∘ π₁ , ⟨ g ∘ π₂ ∘ π₁ , h ∘ π₂ ⟩ ⟩
    ≈˘⟨ ⟨⟩-congˡ ⁂∘⟨⟩ ⟩
      ⟨ f ∘ π₁ ∘ π₁ , (g ⁂ h) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
    ≈˘⟨ ⁂∘⟨⟩ ⟩
      (f ⁂ (g ⁂ h)) ∘ assocˡ
    ∎

  Δ : ∀ {C} → C ⇒ C × C
  Δ {C} = ⟨ id {C} , id ⟩

  Δ∘ : Δ ∘ f ≈ ⟨ f , f ⟩
  Δ∘ {f = f} = begin
    Δ ∘ f               ≈⟨ ⟨⟩∘ ⟩
    ⟨ id ∘ f , id ∘ f ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
    ⟨ f , f ⟩           ∎

  ⁂∘Δ : (f ⁂ g) ∘ Δ ≈ ⟨ f , g ⟩
  ⁂∘Δ {f = f} {g = g} = begin
    (f ⁂ g) ∘ Δ         ≈⟨ ⁂∘⟨⟩ ⟩
    ⟨ f ∘ id , g ∘ id ⟩ ≈⟨ ⟨⟩-cong₂ identityʳ identityʳ ⟩
    ⟨ f , g ⟩           ∎

  -×- : Bifunctor 𝒞 𝒞 𝒞
  -×- = record
    { F₀           = uncurry _×_
    ; F₁           = uncurry _⁂_
    ; identity     = id×id product
    ; homomorphism = ⟺ ⁂∘⁂
    ; F-resp-≈     = uncurry [ product ⇒ product ]×-cong₂
    }

  -×_ : Obj → Functor 𝒞 𝒞
  -×_ = appʳ -×-

  _×- : Obj → Functor 𝒞 𝒞
  _×- = appˡ -×-

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Data.Nat     using (ℕ) renaming (_+_ to _+ᵢ_; _≤?_ to _≤?ᵢ_)
open import Agda.Builtin.Float renaming (primFloatPlus to _+ᵣ_; primFloatLess to _≤?ᵣ_)
open import Data.Bool    using (Bool; true; false; not; _∧_)
open import Data.Sum     using (inj₁; inj₂; _⊎_)
open import Data.Product using (_×_; _,_; -,_; _-,-_; ∃; ∃-syntax; proj₂)
open import Data.String  using (String; _≟_)
open import Relation.Nullary           using (¬_; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Nullary.Negation  using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

vname = String
int = ℕ
real = Float
bool = Bool

data val : Set where
  Iv : int  → val
  Rv : real → val

data aexp : Set where
  Ic   : int   → aexp
  Rc   : real  → aexp
  V    : vname → aexp
  Plus : aexp  → aexp → aexp

data bexp : Set where
  Bc   : Bool → bexp
  Not  : bexp → bexp
  And  : bexp → bexp → bexp
  Less : aexp → aexp → bexp

data com : Set where
  SKIP  : com
  _::=_ : String → aexp → com
  _::_  : com → com → com
  IF_THEN_ELSE_ : bexp → com → com → com
  WHILE_DO_     : bexp → com → com

data ty : Set where
  Ity : ty
  Rty : ty

tyenv = vname → ty
state = vname → val

_[_::=_] : state → vname → val → state
(s [ X ::= n ]) Y with Y ≟ X
... | yes _ = n
... | no  _ = s Y

data _⊢ₐ_∷_ : tyenv → aexp → ty → Set where
  taexpI : ∀{Γ i} → Γ ⊢ₐ Ic i ∷ Ity
  taexpR : ∀{Γ r} → Γ ⊢ₐ Rc r ∷ Rty
  taexpV : ∀{Γ x} → Γ ⊢ₐ V x ∷ Γ x
  taexpP : ∀{Γ a₁ a₂ τ}
      → Γ ⊢ₐ a₁ ∷ τ
      → Γ ⊢ₐ a₂ ∷ τ
      → Γ ⊢ₐ Plus a₁ a₂ ∷ τ

data _⊢₆_ : tyenv → bexp → Set where
  tbexpC : ∀{Γ v} → Γ ⊢₆ Bc v
  tbexpN : ∀{Γ b} → Γ ⊢₆ b
                   → Γ ⊢₆ Not b
  tbexpA : ∀{Γ b₁ b₂}
      → Γ ⊢₆ b₁
      → Γ ⊢₆ b₂
      → Γ ⊢₆ And b₁ b₂
  tbexpL : ∀{Γ a₁ a₂ τ}
      → Γ ⊢ₐ a₁ ∷ τ
      → Γ ⊢ₐ a₂ ∷ τ
      → Γ ⊢₆ Less a₁ a₂

data _⊢_ : tyenv → com → Set where
  TSkip : ∀{Γ} → Γ ⊢ SKIP
  TLoc : ∀{Γ a x} → Γ ⊢ₐ a ∷ Γ x
                 → Γ ⊢ (x ::= a)
  TSeq : ∀{Γ c₁ c₂}
       → Γ ⊢ c₁
       → Γ ⊢ c₂
       → Γ ⊢ (c₁ :: c₂)
  TIf : ∀{Γ b c₁ c₂}
      → Γ ⊢₆ b
      → Γ ⊢ c₁
      → Γ ⊢ c₂
      → Γ ⊢ (IF b THEN c₁ ELSE c₂)
  TWhile : ∀{Γ b c}
         → Γ ⊢₆ b
         → Γ ⊢ c
         → Γ ⊢ (WHILE b DO c)

type : val → ty
type (Iv i) = Ity
type (Rv r) = Rty

_⊢ₛ_ : tyenv → state → Set
Γ ⊢ₛ s = ∀ x → type (s x) ≡ Γ x

data taval : aexp → state → val → Set where
  tavalI : ∀{i s}
         → taval (Ic i) s (Iv i)
  tavalR : ∀{r s}
         → taval (Rc r) s (Rv r)
  tavalV : ∀{x s}
         → taval (V x) s (s x)
  tavalSI : ∀{s a₁ a₂ i₁ i₂}
          → taval a₁ s (Iv i₁)
          → taval a₂ s (Iv i₂)
          → taval (Plus a₁ a₂) s (Iv (i₁ +ᵢ i₂))
  tavalSR : ∀{s a₁ a₂ r₁ r₂}
          → taval a₁ s (Rv r₁)
          → taval a₂ s (Rv r₂)
          → taval (Plus a₁ a₂) s (Rv (r₁ +ᵣ r₂))

data tbval : bexp → state → bool → Set where
  tbvalC : ∀{s v}
         → tbval (Bc v) s v
  tbvalN : ∀{s b bv}
         → tbval b s bv
         → tbval (Not b) s (not bv)
  tbvalA : ∀{s b₁ b₂ bv₁ bv₂}
         → tbval b₁ s bv₁
         → tbval b₂ s bv₂
         → tbval (And b₁ b₂) s (bv₁ ∧ bv₂)
  tbvalLI : ∀{s a₁ a₂ i₁ i₂}
         → taval a₁ s (Iv i₁)
         → taval a₂ s (Iv i₂)
         → tbval (Less a₁ a₂) s (⌊ i₁ ≤?ᵢ i₂ ⌋)
  tbvalLR : ∀{s a₁ a₂ r₁ r₂}
         → taval a₁ s (Rv r₁)
         → taval a₂ s (Rv r₂)
         → tbval (Less a₁ a₂) s (r₁ ≤?ᵣ r₂)

data ⦅_,_⦆→⦅_,_⦆ : com → state → com → state → Set where
  Loc : ∀{x a s v}
      → taval a s v
      → ⦅ x ::= a , s ⦆→⦅ SKIP , s [ x ::= v ] ⦆
  Comp₁ : ∀{c s}
        → ⦅ SKIP :: c , s ⦆→⦅ c , s ⦆
  Comp₂ : ∀{c₁ c₁′ c₂ s s′}
        →  ⦅ c₁       , s ⦆→⦅ c₁′       , s′ ⦆
        →  ⦅ c₁ :: c₂ , s ⦆→⦅ c₁′ :: c₂ , s′ ⦆
  IfTrue  : ∀{b s c₁ c₂}
          → tbval b s true
          → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆→⦅ c₁ , s ⦆
  IfFalse : ∀{b s c₁ c₂}
          → tbval b s false
          → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆→⦅ c₂ , s ⦆
  While : ∀{b s c}
        → ⦅ WHILE b DO c , s ⦆→⦅ IF b THEN (c :: (WHILE b DO c)) ELSE SKIP , s ⦆

data  ⦅_,_⦆→*⦅_,_⦆ : com → state → com → state → Set where
  Ref : ∀{c s} → ⦅ c , s ⦆→*⦅ c , s ⦆
  Step : ∀{c c′ c² s s′ s²}
       → ⦅ c  , s  ⦆→⦅ c′ , s′ ⦆
       → ⦅ c′ , s′ ⦆→*⦅ c² , s² ⦆
       → ⦅ c  , s  ⦆→*⦅ c² , s² ⦆

trans : ∀{c c′ c² s s′ s²}
      → ⦅ c  , s  ⦆→*⦅ c′ , s′ ⦆
      → ⦅ c′ , s′ ⦆→*⦅ c² , s² ⦆
      → ⦅ c  , s  ⦆→*⦅ c² , s² ⦆
trans Ref b = b
trans (Step x a) b = Step x (trans a b)

preservation-aval : ∀{Γ a s τ v}
  → Γ ⊢ₐ a ∷ τ
  → Γ ⊢ₛ s
  → taval a s v
  → type v ≡ τ
preservation-aval taexpI b tavalI = refl
preservation-aval taexpR b tavalR = refl
preservation-aval taexpV b (tavalV {x}) = b x
preservation-aval (taexpP a a₁) b (tavalSI c c₁) = preservation-aval a₁ b c₁
preservation-aval (taexpP a a₁) b (tavalSR c c₁) = preservation-aval a₁ b c₁

extract-ity : ∀ v
  → type v ≡ Ity
  → ∃[ i ] (v ≡ Iv i)
extract-ity (Iv x) r = x , refl

extract-rty : ∀ v
  → type v ≡ Rty
  → ∃[ i ] (v ≡ Rv i)
extract-rty (Rv x) r = x , refl

progress-aval : ∀{Γ a s τ}
  → Γ ⊢ₐ a ∷ τ
  → Γ ⊢ₛ s
  → ∃[ v ] (taval a s v)
progress-aval taexpI b = -, tavalI
progress-aval taexpR b = -, tavalR
progress-aval taexpV b = -, tavalV
progress-aval {τ = Ity} (taexpP a₁ a₂) b with progress-aval a₁ b | progress-aval a₂ b
... | rv , r  | mv , m with extract-ity rv (preservation-aval a₁ b r)
                          | extract-ity mv (preservation-aval a₂ b m)
... | v1 , e1 | v2 , e2 rewrite e1 | e2 = -, tavalSI r m
progress-aval {τ = Rty} (taexpP a₁ a₂) b with progress-aval a₁ b | progress-aval a₂ b
... | rv , r  | mv , m with extract-rty rv (preservation-aval a₁ b r)
                          | extract-rty mv (preservation-aval a₂ b m)
... | v1 , e1 | v2 , e2 rewrite e1 | e2 = -, tavalSR r m

progress-bval : ∀{Γ b s}
  → Γ ⊢₆ b
  → Γ ⊢ₛ s
  → ∃[ v ] (tbval b s v)
progress-bval tbexpC x₁ = -, tbvalC
progress-bval (tbexpN x) x₁ = -, tbvalN (proj₂ (progress-bval x x₁))
progress-bval (tbexpA a b) x = -, tbvalA (proj₂ (progress-bval a x))
                                         (proj₂ (progress-bval b x))
progress-bval (tbexpL {τ = Ity} a₁ a₂) b with progress-aval a₁ b | progress-aval a₂ b
... | rv , r  | mv , m with extract-ity rv (preservation-aval a₁ b r)
                          | extract-ity mv (preservation-aval a₂ b m)
... | v1 , e1 | v2 , e2 rewrite e1 | e2 = -, tbvalLI r m
progress-bval (tbexpL {τ = Rty} a₁ a₂) b with progress-aval a₁ b | progress-aval a₂ b
... | rv , r  | mv , m with extract-rty rv (preservation-aval a₁ b r)
                          | extract-rty mv (preservation-aval a₂ b m)
... | v1 , e1 | v2 , e2 rewrite e1 | e2 = -, tbvalLR r m

preservation-com : ∀{Γ c s c′ s′}
  → ⦅ c , s ⦆→⦅ c′ , s′ ⦆
  → Γ ⊢ c
  → Γ ⊢ c′
preservation-com (Loc x₁) (TLoc x₂) = TSkip
preservation-com Comp₁ (TSeq b b₁) = b₁
preservation-com (Comp₂ a) (TSeq b b₁) = TSeq (preservation-com a b) b₁
preservation-com (IfTrue x) (TIf x₁ b b₁) = b
preservation-com (IfFalse x) (TIf x₁ b b₁) = b₁
preservation-com While (TWhile x b) = TIf x (TSeq b (TWhile x b)) TSkip

preservation-state : ∀{Γ c s c′ s′}
  → ⦅ c , s ⦆→⦅ c′ , s′ ⦆
  → Γ ⊢ c
  → Γ ⊢ₛ s
  → Γ ⊢ₛ s′
preservation-state (Loc {x₃} x₁) (TLoc x₂) r x₄ with x₄ ≟ x₃
... | no ¬p = r x₄
... | yes p with preservation-aval x₂ r x₁
... | z rewrite p = z
preservation-state Comp₁ (TSeq c c₁) r = r
preservation-state (Comp₂ d) (TSeq c c₁) r = preservation-state d c r
preservation-state (IfTrue x) (TIf x₁ c c₁) r = r
preservation-state (IfFalse x) (TIf x₁ c c₁) r = r
preservation-state While (TWhile x c) r = r

preservation : ∀{Γ c s c′ s′}
  → Γ ⊢  c
  → Γ ⊢ₛ s
  → ⦅ c , s ⦆→⦅ c′ , s′ ⦆
  → Γ ⊢ c′ × Γ ⊢ₛ s′
preservation a b c = preservation-com c a , preservation-state c a b

either-skip : ∀ c
            → c ≡ SKIP ⊎ ¬ c ≡ SKIP
either-skip SKIP = inj₁ refl
either-skip (x ::= x₁) = inj₂ (λ ())
either-skip (c :: c₁) = inj₂ (λ ())
either-skip (IF x THEN c ELSE c₁) = inj₂ (λ ())
either-skip (WHILE x DO c) = inj₂ (λ ())

progress : ∀{Γ c s}
  → Γ ⊢  c
  → Γ ⊢ₛ s
  → ¬ c ≡ SKIP
  → ∃[ c′ ] (∃[ s′ ] ( ⦅ c , s ⦆→⦅ c′ , s′ ⦆ ))
progress TSkip b c = contradiction refl c
progress {s = s} (TLoc x) b _ = SKIP , -, Loc (proj₂ (progress-aval x b))
progress {s = s} (TSeq {_}{c₁}{c₂} a a₁) b _ with either-skip c₁
... | inj₁  skip rewrite skip = c₂ , s , Comp₁
... | inj₂ ¬skip = let c₁′       , s′ ,       r = progress a b ¬skip
                    in c₁′ :: c₂ , s′ , Comp₂ r
progress (TIf x a a₁) b _ with progress-bval x b
... | false , tb = -, -, IfFalse tb
... | true  , tb = -, -, IfTrue tb
progress (TWhile x a) b _ = -, -, While

type-soundness : ∀{c s c′ s′ Γ}
  → ⦅ c , s ⦆→*⦅ c′ , s′ ⦆
  → Γ ⊢  c
  → Γ ⊢ₛ s
  → ¬ c′ ≡ SKIP
  → ∃[ c″ ] (∃[ s″ ] ( ⦅ c′ , s′ ⦆→⦅ c″ , s″ ⦆ ))
type-soundness Ref c d e =  progress c d e
type-soundness (Step x r) c d e with preservation c d x
... | ct , st = type-soundness r ct st e

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
module Test where

open import Agda.Primitive

f : Level -> Level
f x = x


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

module container where

import container.core
import container.fixpoint
import container.equality
import container.m
import container.w

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

open import HoTT
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLaneFunctor
open import cohomology.CupProduct.OnEM.CommutativityInLowDegrees

module cohomology.CupProduct.OnEM.CommutativityInLowDegrees2 {i} {j} (G : AbGroup i) (H : AbGroup j) where

private
  module G = AbGroup G
  module H = AbGroup H
  module G⊗H = TensorProduct G H
  module H⊗G = TensorProduct H G
  module GHc = CP₁₁-comm G H
  module HGc = CP₁₁-comm H G

import cohomology.CupProduct.OnEM.InLowDegrees2 G H as GH
import cohomology.CupProduct.OnEM.InLowDegrees2 H G as HG

private
  ∧-cp₁₁-comm-smgluel : ∀ (x : EM₁ G.grp)
    → Square (GHc.CP₁₁Comm.f x embase)
             (ap GH.∧-cp₁₁ (smgluel x))
             (ap (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluel x))
             idp
  ∧-cp₁₁-comm-smgluel x =
    GH.∧-cp₁₁-Rec.smgluel-β x ∙v⊡
    lt-square (GH.cp₁₁-embase-r x) ⊡v∙
    ! bottom-path
    where
    bottom-path : ap (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluel x) == idp
    bottom-path =
      ap (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluel x)
        =⟨ ap-∘ (GHc.− ∘ HG.∧-cp₁₁) (∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluel x) ⟩
      ap (GHc.− ∘ HG.∧-cp₁₁) (ap (∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluel x))
        =⟨ ap (ap (GHc.− ∘ HG.∧-cp₁₁)) (SmashSwap.smgluel-β (⊙EM₁ G.grp) (⊙EM₁ H.grp) x) ⟩
      ap (GHc.− ∘ HG.∧-cp₁₁) (∧-norm-r x)
        =⟨ ap-∘ GHc.− HG.∧-cp₁₁ (∧-norm-r x) ⟩
      ap GHc.− (ap HG.∧-cp₁₁ (∧-norm-r x))
        =⟨ ap (ap GHc.−) (HG.∧-cp₁₁-Rec.∧-norm-r-β x) ⟩
      idp =∎

  cp₁₁-comm-sym : ∀ (y : EM₁ H.grp)
    → ! (GHc.CP₁₁Comm.f embase y) == ap GHc.− (HGc.CP₁₁Comm.f y embase)
  cp₁₁-comm-sym =
    EM₁-set-elim
      {P = λ y → ! (GHc.CP₁₁Comm.f embase y) == ap GHc.− (HGc.CP₁₁Comm.f y embase)}
      {{λ y → has-level-apply (has-level-apply (Trunc-level {n = 2}) _ _) _ _}}
      idp $ λ h →
    ↓-=-in $
    idp ◃ apd (λ y → ap GHc.− (HGc.CP₁₁Comm.f y embase)) (emloop h)
      =⟨ idp◃ (apd (λ y → ap GHc.− (HGc.CP₁₁Comm.f y embase)) (emloop h)) ⟩
    apd (λ y → ap GHc.− (HGc.CP₁₁Comm.f y embase)) (emloop h)
      =⟨ apd-∘' (ap GHc.−) (λ y → HGc.CP₁₁Comm.f y embase) (emloop h) ⟩
    ap↓ (ap GHc.−) (apd (λ y → HGc.CP₁₁Comm.f y embase) (emloop h))
      =⟨ ap (ap↓ (ap GHc.−)) (HGc.CP₁₁Comm.emloop-embase-β h) ⟩
    ap↓ (ap GHc.−) (↓-='-from-square (HGc.comm-emloop-embase h))
      =⟨ ↓-='-from-square-post-∘ {h = GHc.−} (HGc.comm-emloop-embase h) ⟩
    ↓-='-from-square (ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡
                      ap-square GHc.− (HGc.comm-emloop-embase h) ⊡v∙
                      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h))
      =⟨ ap ↓-='-from-square (square-path h) ⟩
    ↓-='-from-square (!□v (GHc.comm-embase-emloop h))
      =⟨ ! (↓-='-from-square-! (GHc.comm-embase-emloop h)) ⟩
    ap↓ ! (↓-='-from-square (GHc.comm-embase-emloop h))
      =⟨ ap (ap↓ !) (! (GHc.CP₁₁Comm.embase-emloop-β h)) ⟩
    ap↓ ! (apd (λ y → GHc.CP₁₁Comm.f embase y) (emloop h))
      =⟨ ! (apd-∘' ! (λ y → GHc.CP₁₁Comm.f embase y) (emloop h)) ⟩
    apd (λ y → ! (GHc.CP₁₁Comm.f embase y)) (emloop h)
      =⟨ ! (▹idp (apd (λ y → ! (GHc.CP₁₁Comm.f embase y)) (emloop h))) ⟩
    apd (λ y → ! (GHc.CP₁₁Comm.f embase y)) (emloop h) ▹ idp =∎
    where
    =ₛ-path : ∀ (h : H.El) →
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ◃∙
      ap (ap GHc.−) (HGc.comm-emloop-embase' h) ◃∙
      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h) ◃∎
      =ₛ
      ! (GHc.comm-embase-emloop' h) ◃∎
    =ₛ-path h = !ₛ $
      ! (GHc.comm-embase-emloop' h) ◃∎
        =ₛ⟨ !-∙-seq (GHc.comm-embase-emloop-seq h) ⟩
      ! (∘-ap GHc.− (λ y → HG.cp₁₁ y embase) (emloop h)) ◃∙
      ! (! (ap (ap GHc.−) (HG.ap-cp₁₁-embase h))) ◃∙
      ! (ap-cst [ north ] (emloop h)) ◃∎
        =ₛ₁⟨ 0 & 1 & ap ! (! (!ap-∘=∘-ap GHc.− (λ y → HG.cp₁₁ y embase) (emloop h))) ∙
                     !-! (ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h)) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ◃∙
      ! (! (ap (ap GHc.−) (HG.ap-cp₁₁-embase h))) ◃∙
      ! (ap-cst [ north ] (emloop h)) ◃∎
        =ₛ₁⟨ 1 & 1 & !-! (ap (ap GHc.−) (HG.ap-cp₁₁-embase h)) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ◃∙
      ap (ap GHc.−) (HG.ap-cp₁₁-embase h) ◃∙
      ! (ap-cst [ north ]₂ (emloop h)) ◃∎
        =ₛ⟨ 2 & 2 & !ₛ $
            post-rotate-in {p = _ ◃∙ _ ◃∎} $
            pre-rotate'-in $
            ap-∘-cst-coh GHc.− [ north ]₂ (emloop h) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ◃∙
      ap (ap GHc.−) (HG.ap-cp₁₁-embase h) ◃∙
      ! (ap (ap GHc.−) (ap-cst [ north ] (emloop h))) ◃∙
      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h) ◃∎
        =ₛ₁⟨ 2 & 1 & !-ap (ap GHc.−) (ap-cst [ north ]₂ (emloop h)) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ◃∙
      ap (ap GHc.−) (HG.ap-cp₁₁-embase h) ◃∙
      ap (ap GHc.−) (! (ap-cst [ north ]₂ (emloop h))) ◃∙
      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h) ◃∎
        =ₛ⟨ 1 & 2 & ∙-ap-seq (ap GHc.−) (HGc.comm-emloop-embase-seq h) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ◃∙
      ap (ap GHc.−) (HGc.comm-emloop-embase' h) ◃∙
      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h) ◃∎ ∎ₛ
    square-path : ∀ (h : H.El) →
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡
      ap-square GHc.− (HGc.comm-emloop-embase h) ⊡v∙
      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h)
      ==
      !□v (GHc.comm-embase-emloop h)
    square-path h =
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡
      ap-square GHc.− (HGc.comm-emloop-embase h) ⊡v∙
      ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h)
        =⟨ ap (λ u → ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡
                     u ⊡v∙
                     ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h)) $
           ap-vert-degen-square GHc.− (HGc.comm-emloop-embase' h) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡
      vert-degen-square (ap (ap GHc.−) (HGc.comm-emloop-embase' h))
      ⊡v∙ ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h)
        =⟨ ap (ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡_) $
           vert-degen-square-⊡v∙ (ap (ap GHc.−) (HGc.comm-emloop-embase' h))
                                 (∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h)) ⟩
      ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙v⊡
      vert-degen-square (ap (ap GHc.−) (HGc.comm-emloop-embase' h) ∙
                         ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h))
        =⟨ vert-degen-square-∙v⊡
             (ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h))
             (ap (ap GHc.−) (HGc.comm-emloop-embase' h) ∙
              ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h)) ⟩
      vert-degen-square (ap-∘ GHc.− (λ y → HG.cp₁₁ y embase) (emloop h) ∙
                         ap (ap GHc.−) (HGc.comm-emloop-embase' h) ∙
                         ∘-ap GHc.− (λ y → HGc.− (GH.cp₁₁ embase y)) (emloop h))
        =⟨ ap vert-degen-square (=ₛ-out (=ₛ-path h)) ⟩
      vert-degen-square (! (GHc.comm-embase-emloop' h))
        =⟨ ! (!□v-vert-degen-square (GHc.comm-embase-emloop' h)) ⟩
      !□v (GHc.comm-embase-emloop h) =∎

  ∧-cp₁₁-comm-smgluer : ∀ (y : EM₁ H.grp)
    → Square (GHc.CP₁₁Comm.f embase y)
             (ap GH.∧-cp₁₁ (smgluer y))
             (ap (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluer y))
             idp
  ∧-cp₁₁-comm-smgluer y =
    GH.∧-cp₁₁-Rec.smgluer-β y ∙v⊡
    lb-square (GHc.CP₁₁Comm.f embase y) ⊡v∙
    (cp₁₁-comm-sym y ∙ ! bottom-path)
    where
    bottom-path : ap (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluer y) == ap GHc.− (HG.cp₁₁-embase-r y)
    bottom-path =
      ap (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluer y)
        =⟨ ap-∘ (GHc.− ∘ HG.∧-cp₁₁) (∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluer y) ⟩
      ap (GHc.− ∘ HG.∧-cp₁₁) (ap (∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) (smgluer y))
        =⟨ ap (ap (GHc.− ∘ HG.∧-cp₁₁)) (SmashSwap.smgluer-β (⊙EM₁ G.grp) (⊙EM₁ H.grp) y) ⟩
      ap (GHc.− ∘ HG.∧-cp₁₁) (∧-norm-l y)
        =⟨ ap-∘ GHc.− HG.∧-cp₁₁ (∧-norm-l y) ⟩
      ap GHc.− (ap HG.∧-cp₁₁ (∧-norm-l y))
        =⟨ ap (ap GHc.−) (HG.∧-cp₁₁-Rec.∧-norm-l-β y) ⟩
      ap GHc.− (HG.cp₁₁-embase-r y ∙ idp)
        =⟨ ap (ap GHc.−) (∙-unit-r (HG.cp₁₁-embase-r y)) ⟩
      ap GHc.− (HG.cp₁₁-embase-r y) =∎

private
  ∧-cp₁₁-comm' : GH.∧-cp₁₁ ∼ GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)
  ∧-cp₁₁-comm' =
    Smash-Path-elim
      GH.∧-cp₁₁
      (GHc.− ∘ HG.∧-cp₁₁ ∘ ∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp))
      GHc.CP₁₁Comm.f
      idp
      idp
      ∧-cp₁₁-comm-smgluel
      ∧-cp₁₁-comm-smgluer

  ⊙∧-cp₁₁-comm' : GH.⊙∧-cp₁₁ ◃⊙idf
                  =⊙∘
                  GHc.⊙− ◃⊙∘
                  HG.⊙∧-cp₁₁ ◃⊙∘
                  ⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp) ◃⊙idf
  ⊙∧-cp₁₁-comm' = =⊙∘-in (⊙λ=' ∧-cp₁₁-comm' idp)

⊙∧-cp₁₁-comm : ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 2 ◃⊙∘
               GH.⊙∧-cp₁₁ ◃⊙idf
               =⊙∘
               ⊙EM-neg H⊗G.abgroup 2 ◃⊙∘
               HG.⊙∧-cp₁₁ ◃⊙∘
               ⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp) ◃⊙idf
⊙∧-cp₁₁-comm =
  ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 2 ◃⊙∘
  GH.⊙∧-cp₁₁ ◃⊙idf
    =⊙∘⟨ 1 & 1 & ⊙∧-cp₁₁-comm' ⟩
  ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 2 ◃⊙∘
  GHc.⊙− ◃⊙∘
  HG.⊙∧-cp₁₁ ◃⊙∘
  ⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp) ◃⊙idf
    =⊙∘⟨ 1 & 1 & minus ⟩
  ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 2 ◃⊙∘
  ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap 2 ◃⊙∘
  ⊙EM-neg H⊗G.abgroup 2 ◃⊙∘
  HG.⊙∧-cp₁₁ ◃⊙∘ ⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp) ◃⊙idf
    =⊙∘⟨ 0 & 2 & =⊙∘-in {gs = ⊙idf-seq} $
         ! (⊙EM-fmap-∘ H⊗G.abgroup G⊗H.abgroup H⊗G.abgroup G⊗H.swap H⊗G.swap 2) ∙
         ap (λ φ → ⊙EM-fmap H⊗G.abgroup H⊗G.abgroup φ 2) H⊗G.swap-swap-idhom ∙
         ⊙EM-fmap-idhom H⊗G.abgroup 2 ⟩
  ⊙EM-neg H⊗G.abgroup 2 ◃⊙∘
  HG.⊙∧-cp₁₁ ◃⊙∘ ⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp) ◃⊙idf ∎⊙∘
  where
  minus : GHc.⊙− ◃⊙idf
          =⊙∘
          ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap 2 ◃⊙∘
          ⊙EM-neg H⊗G.abgroup 2 ◃⊙idf
  minus = =⊙∘-in $
    ⊙Trunc-fmap (⊙Susp-fmap (EM₁-fmap (inv-hom G⊗H.abgroup) ∘ EM₁-fmap H⊗G.swap))
      =⟨ ap (⊙Trunc-fmap ∘ ⊙Susp-fmap) $ ! $
         λ= (EM₁-fmap-∘ (inv-hom G⊗H.abgroup) H⊗G.swap) ⟩
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup (inv-hom G⊗H.abgroup ∘ᴳ H⊗G.swap) 2
      =⟨ ap (λ φ → ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup φ 2) $
         ! $ inv-hom-natural H⊗G.abgroup G⊗H.abgroup H⊗G.swap ⟩
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup (H⊗G.swap ∘ᴳ inv-hom H⊗G.abgroup) 2
      =⟨ ⊙EM-fmap-∘ H⊗G.abgroup H⊗G.abgroup G⊗H.abgroup (H⊗G.swap) (inv-hom H⊗G.abgroup) 2 ⟩
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap 2 ⊙∘ ⊙EM-neg H⊗G.abgroup 2 =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- Modules that are not safe because they use --sized-types
------------------------------------------------------------------------

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

module README.Unsafe.Sized-types where

-- Support for sized types.

import Prelude.Size

-- Some results that could not be placed in Function-universe because
-- they make use of --sized-types.

import Function-universe.Size

-- Conatural numbers.

import Conat

-- Colists.

import Colist

-- M-types.

import M

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module unit where

open import level
open import eq

data ⊤ : Set where
  triv : ⊤

{-# COMPILED_DATA ⊤ () ()  #-}

single-range : ∀{U : Set}{g : U → ⊤} → ∀{u : U} → g u ≡ triv
single-range {U}{g}{u} with g u
... | triv = refl

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


text:
-- Reported by nad, 2018-12-13.
-- The option --no-sized-types should turn off sized types
{-# OPTIONS --no-sized-types #-}

{-# BUILTIN SIZE   Size   #-}
{-# BUILTIN SIZELT Size<_ #-}

record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : {j : Size< i} → Stream A j

open Stream

postulate
  destroy-guardedness : {A : Set} → A → A

repeat : ∀ {A i} → A → Stream A i
repeat x .head = x
repeat x .tail = destroy-guardedness (repeat x)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------

-- Some operations on/properties of nullary relations, i.e. sets.

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

module Relation.Nullary where

open import Data.Empty hiding (⊥-elim)
open import Data.Empty.Irrelevant
open import Level

-- Negation.

infix 3 ¬_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⊥

-- Decidable relations.

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

-- Given an irrelevant proof of a decidable type, a proof can
-- be recomputed and subsequently used in relevant contexts.
recompute : ∀ {a} {A : Set a} → Dec A → .A → A
recompute (yes x) _ = x
recompute (no ¬p) x = ⊥-elim (¬p x)


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module Quicksort {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import Data.Product
open import Data.Sum
open import SBList _≤_
open import Size
open import SOList.Total _≤_

deal : {ι : Size}{b t : Bound}{x : A} → LeB b (val x) → LeB (val x) t → SBList {ι} b t → SBList {ι} b (val x) × SBList {ι} (val x) t
deal b≤x x≤t (nil b≤t) = (nil b≤x , nil x≤t)
deal {x = x} b≤x x≤t (cons y b≤y y≤t ys)
    with tot≤ x y | deal b≤x x≤t ys
... | inj₁ x≤y | (us , vs) = (us , cons y (lexy x≤y) y≤t vs)
... | inj₂ y≤x | (us , vs) = (cons y b≤y (lexy y≤x) us , vs)

quickSort : {ι : Size}{b t : Bound} → SBList {ι} b t → SOList b t
quickSort (nil b≤t) = onil b≤t
quickSort (cons x b≤x x≤t xs)
    with deal b≤x x≤t xs
... | (ys , zs) = ocons x (quickSort ys) (quickSort zs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Confluence where

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

cong : ∀ {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

add : ℕ → ℕ → ℕ
add n Z = n
add n (S m) = S (add n m)

_ : ∀ {a : ℕ} → add a Z ≡ a
_ = refl

thm : ∀ {a : ℕ} → add Z a ≡ a
thm {a = Z} = refl
thm {a = (S m)} = cong S thm
-- Confluence checking is not supported;
-- Check out Jesper Cockx's Phd thesis for overlapping patterns.

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
module Prelude.Nat.Core where

open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Number
open import Prelude.Semiring

open import Agda.Builtin.Nat public
  renaming ( _+_        to _+N_
           ; _*_        to _*N_
           ; _-_        to _-N_
           ; _==_       to eqNat
           ; _<_        to lessNat
           ; div-helper to divAux
           ; mod-helper to modAux )

{-# DISPLAY _+N_ = _+_ #-}
{-# DISPLAY _-N_ = _-_ #-}
{-# DISPLAY _*N_ = _*_ #-}

--- Semiring ---

instance
  NumberNat : Number Nat
  Number.Constraint NumberNat _ = ⊤
  Number.fromNat    NumberNat n = n

  SemiringNat : Semiring Nat
  zro {{SemiringNat}} = 0
  one {{SemiringNat}} = 1
  _+_ {{SemiringNat}} = _+N_
  _*_ {{SemiringNat}} = _*N_

  SubtractiveNat : Subtractive Nat
  _-_    {{SubtractiveNat}}   = _-N_
  negate {{SubtractiveNat}} _ = 0

--- Division and modulo ---

NonZero : Nat → Set
NonZero zero    = ⊥
NonZero (suc _) = ⊤

infixl 7 natDiv natMod
syntax natDiv m n = n div m
natDiv : (m : Nat) {{nz : NonZero m}} → Nat → Nat
natDiv zero {{}} n
natDiv (suc m) n = divAux 0 m n m

syntax natMod m n = n mod m
natMod : (m : Nat) {{nz : NonZero m}} → Nat → Nat
natMod zero {{}} n
natMod (suc m) n = modAux 0 m n m

{-# INLINE natMod #-}
{-# INLINE natDiv #-}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
import      Lvl

module Function.Names where

open import Functional.Dependent
open import Logic.Predicate
open import Structure.Setoid
open import Type

private variable ℓ ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ : Lvl.Level

module _ {A : Type{ℓₒ₁}} {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₃}(B(a)) ⦄ where
  -- Extensional equality on functions.
  -- Alternative definition: f ⊜ g = (∀{x} → (f(x) ≡ g(x)))
  _⊜_ : ((a : A) → B(a)) → ((a : A) → B(a)) → Type
  _⊜_ = ∀¹ ∘₂ pointwise₂,₁(_≡_)
  _⊜₁_ = _⊜_

module _ {A : Type{ℓₒ₁}} {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₃}(B(a)) ⦄ where
  _⊜ᵢ_ : ({a : A} → B(a)) → ({a : A} → B(a)) → Type
  _⊜ᵢ_ f g = (∀{x} → (f{x} ≡ g{x}))

module _ {A : Type{ℓₒ₁}} {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₃}(B(a)) ⦄ where
  _⦃⊜⦄_ : (⦃ a : A ⦄ → B(a)) → (⦃ a : A ⦄ → B(a)) → Type
  _⦃⊜⦄_ f g = (∀{x} → (f ⦃ x ⦄ ≡ g ⦃ x ⦄))

module _ {A₁ : Type{ℓₒ₁}} {A₂ : A₁ → Type{ℓₒ₂}} {B : (a₁ : A₁) → A₂(a₁) → Type{ℓₒ₂}} ⦃ _ : ∀{a₁}{a₂} → Equiv{ℓₗ₃}(B(a₁)(a₂)) ⦄ where
  -- Alternative definition: f ⊜ g = (∀{x}{y} → (f(x)(y) ≡ g(x)(y)))
  _⊜₂_ : (f g : ∀(a₁)(a₂) → B(a₁)(a₂)) → Type
  _⊜₂_ = ∀¹ ∘₂ (∀¹ ∘₃ pointwise₂,₂(_≡_))

module _ {A₁ : Type{ℓₒ₁}} {A₂ : A₁ → Type{ℓₒ₂}} {A₃ : (a₁ : A₁) → A₂(a₁) → Type{ℓₒ₂}} {B : (a₁ : A₁) → (a₂ : A₂(a₁)) → A₃(a₁)(a₂) → Type{ℓₒ₂}} ⦃ _ : ∀{a₁}{a₂}{a₃} → Equiv{ℓₗ₃}(B(a₁)(a₂)(a₃)) ⦄ where
  -- Alternative definition: f ⊜ g = (∀{x}{y}{z} → (f(x)(y)(z) ≡ g(x)(y)(z)))
  _⊜₃_ : (f g : ∀(a₁)(a₂)(a₃) → B(a₁)(a₂)(a₃)) → Type
  _⊜₃_ = ∀¹ ∘₂ (∀¹ ∘₃ (∀¹ ∘₄ pointwise₂,₃(_≡_)))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Data.Boolean.Equiv.Path where

open import Data
open import Data.Boolean
open import Data.Boolean.Stmt
open import Functional
open import Logic.Propositional
open import Structure.Relator.Properties
open import Structure.Relator
open import Type.Cubical.Path.Equality
open import Type.Cubical.Path
open import Type.Identity

Bool-different-values : ¬(Path 𝐹 𝑇)
Bool-different-values p = substitute₁ₗ(IsTrue) p <>

Bool-Path-to-Id : ∀{x y : Bool} → (Path x y) → (Id x y)
Bool-Path-to-Id {𝑇} {𝑇} _ = intro
Bool-Path-to-Id {𝑇} {𝐹}   = [⊥]-elim ∘ Bool-different-values ∘ symmetry(Path)
Bool-Path-to-Id {𝐹} {𝑇}   = [⊥]-elim ∘ Bool-different-values
Bool-Path-to-Id {𝐹} {𝐹} _ = intro


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures as LIWS
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Types.EpochState where

verify : EpochState → LedgerInfoWithSignatures → Either ErrLog Unit
verify self ledgerInfo = do
  lcheck (self ^∙ esEpoch == ledgerInfo ^∙ liwsLedgerInfo ∙ liEpoch)
         ( "EpochState" ∷ "LedgerInfo has unexpected epoch" ∷ [])
         --, show (self^.esEpoch), show (ledgerInfo^.liwsLedgerInfo.liEpoch) ]
  LIWS.verifySignatures ledgerInfo (self ^∙ esVerifier)

epochChangeVerificationRequired : EpochState → Epoch → Bool
epochChangeVerificationRequired self epoch = ⌊ self ^∙ esEpoch <? epoch ⌋

isLedgerInfoStale : EpochState → LedgerInfo → Bool
isLedgerInfoStale self ledgerInfo = ⌊ ledgerInfo ^∙ liEpoch <? self ^∙ esEpoch ⌋


text:
open import Level using (_⊔_; suc)

open import Data.Empty using (⊥)

open import Relation.Binary using (Rel; Decidable; DecSetoid)

module AKS.Algebra.Bundles where

open import AKS.Nat using (ℕ)

open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Bundles using (CommutativeRing) public
open import AKS.Algebra.Structures using
  ( IsNonZeroCommutativeRing; IsIntegralDomain; IsGCDDomain
  ; IsUniqueFactorizationDomain; IsEuclideanDomain; IsField
  ; IsDecField; IsFiniteField
  ) public

record NonZeroCommutativeRing a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isNonZeroCommutativeRing : IsNonZeroCommutativeRing Carrier _≈_ _+_ _*_ -_ 0# 1#

  open IsNonZeroCommutativeRing isNonZeroCommutativeRing using (isCommutativeRing; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#; C/0; 1#-nonzero; -1#-nonzero) public

  commutativeRing : CommutativeRing a ℓ
  commutativeRing = record { isCommutativeRing = isCommutativeRing }

  open CommutativeRing commutativeRing using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; setoid; isEquivalence
    ) public

record IntegralDomain a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isIntegralDomain : IsIntegralDomain Carrier _≈_ _+_ _*_ -_ 0# 1#

  open IsIntegralDomain isIntegralDomain using (isNonZeroCommutativeRing; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_) public

  nonZeroCommutativeRing : NonZeroCommutativeRing a ℓ
  nonZeroCommutativeRing = record { isNonZeroCommutativeRing = isNonZeroCommutativeRing }

  open NonZeroCommutativeRing nonZeroCommutativeRing using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#; C/0; 1#-nonzero; -1#-nonzero
    ; setoid; isEquivalence
    ) public

record GCDDomain a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    gcd     : Op₂ Carrier
    isGCDDomain : IsGCDDomain Carrier _≈_ _+_ _*_ -_ 0# 1# gcd

  open IsGCDDomain isGCDDomain using (isIntegralDomain) public

  integralDomain : IntegralDomain a ℓ
  integralDomain = record { isIntegralDomain = isIntegralDomain }

  open IntegralDomain integralDomain using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing; nonZeroCommutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#
    ; C/0; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_; 1#-nonzero; -1#-nonzero
    ; setoid; isEquivalence
    ) public

record UniqueFactorizationDomain a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    gcd     : Op₂ Carrier
    isUniqueFactorizationDomain : IsUniqueFactorizationDomain Carrier _≈_ _+_ _*_ -_ 0# 1# gcd

  open IsUniqueFactorizationDomain isUniqueFactorizationDomain using (isGCDDomain) public

  gcdDomain : GCDDomain a ℓ
  gcdDomain = record { isGCDDomain = isGCDDomain }

  open GCDDomain gcdDomain using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing; nonZeroCommutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#
    ; C/0; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_; 1#-nonzero; -1#-nonzero
    ; setoid; isEquivalence
    ) public

record EuclideanDomain a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 7 _div_
  infixl 7 _mod_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_   : Op₂ Carrier
    _*_   : Op₂ Carrier
    -_    : Op₁ Carrier
    0#    : Carrier
    1#    : Carrier
    ∣_∣   : ∀ n {n≉0 : n ≉ 0#} → ℕ
    _div_ : ∀ (n m : Carrier) {m≉0 : m ≉ 0#} → Carrier
    _mod_ : ∀ (n m : Carrier) {m≉0 : m ≉ 0#} → Carrier
    gcd   : Op₂ Carrier
    isEuclideanDomain : IsEuclideanDomain Carrier _≈_ _+_ _*_ -_ 0# 1# ∣_∣ _div_ _mod_ gcd

  open import AKS.Algebra.Structures Carrier _≈_ using (module Modulus)
  open Modulus 0# ∣_∣ _mod_ using (Remainder; 0≈; 0≉)
  open IsEuclideanDomain isEuclideanDomain using
    ( isUniqueFactorizationDomain
    ; division; modulus
    ) public

  uniqueFactorizationDomain : UniqueFactorizationDomain a ℓ
  uniqueFactorizationDomain = record { isUniqueFactorizationDomain = isUniqueFactorizationDomain }

  open UniqueFactorizationDomain uniqueFactorizationDomain using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing; nonZeroCommutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#
    ; C/0; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_; 1#-nonzero; -1#-nonzero
    ; setoid; isEquivalence
    ) public

record Field a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 7 _/_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    _/_     : ∀ (n m : Carrier) {m≉0 : m ≉ 0#} → Carrier
    gcd     : Op₂ Carrier
    isField : IsField Carrier _≈_ _+_ _*_ -_ 0# 1# _/_ gcd

  open IsField isField using
    ( isEuclideanDomain
    ; m*[n/m]≈n; [n/m]*m≈n; /-cong; _/-nonzero_
    ; _⁻¹; ⁻¹-inverseʳ; ⁻¹-inverseˡ
    ; x⁻¹≉0; ⁻¹-cong
    )public

  euclideanDomain : EuclideanDomain a ℓ
  euclideanDomain = record { isEuclideanDomain = isEuclideanDomain }

  open EuclideanDomain euclideanDomain using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing; nonZeroCommutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#
    ; C/0; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_; 1#-nonzero; -1#-nonzero
    ; setoid; isEquivalence
    ) public

record DecField a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 7 _/_
  infixl 6 _+_
  infix  4 _≈_
  infix  4 _≈?_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ
    _≈?_    : Decidable _≈_

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    _/_     : ∀ (n m : Carrier) {m≉0 : m ≉ 0#} → Carrier
    gcd     : Op₂ Carrier
    isDecField : IsDecField Carrier _≈_ _≈?_ _+_ _*_ -_ 0# 1# _/_ gcd

  open IsDecField isDecField using (isField; isDecEquivalence) public

  [field] : Field a ℓ
  [field] = record { isField = isField }

  decSetoid : DecSetoid a ℓ
  decSetoid = record { isDecEquivalence = isDecEquivalence }

  open Field [field] using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing; nonZeroCommutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#
    ; C/0; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_; _/-nonzero_; 1#-nonzero; -1#-nonzero
    ; m*[n/m]≈n; [n/m]*m≈n; /-cong
    ; _⁻¹; ⁻¹-inverseʳ; ⁻¹-inverseˡ
    ; x⁻¹≉0; ⁻¹-cong
    ; setoid; isEquivalence
    ) public

record FiniteField a ℓ : Set (suc (a ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 7 _/_
  infixl 6 _+_
  infix  4 _≈_
  infix  4 _≈?_
  field
    Carrier : Set a
    _≈_     : Rel Carrier ℓ
    _≈?_    : Decidable _≈_

  infix 4 _≉_
  _≉_ : Rel Carrier ℓ
  x ≉ y = x ≈ y → ⊥

  field
    _+_  : Op₂ Carrier
    _*_  : Op₂ Carrier
    -_   : Op₁ Carrier
    0#   : Carrier
    1#   : Carrier
    _/_  : ∀ (n m : Carrier) {m≉0 : m ≉ 0#} → Carrier
    gcd  : Op₂ Carrier
    cardinality   : ℕ
    isFiniteField : IsFiniteField Carrier _≈_ _≈?_ _+_ _*_ -_ 0# 1# _/_ gcd cardinality

  open IsFiniteField isFiniteField using (isDecField) public

  decField : DecField a ℓ
  decField = record { isDecField = isDecField }

  open DecField decField using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; +-group; +-abelianGroup; _-_
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne; commutativeSemiring
    ; ring; commutativeRing; nonZeroCommutativeRing
    ; 0#≉1#; 1#≉0#; 0#≉-1#; -1#≉0#
    ; C/0; *-cancelˡ; *-cancelʳ; *≉0; _*-nonzero_; _/-nonzero_; 1#-nonzero; -1#-nonzero
    ; m*[n/m]≈n; [n/m]*m≈n; /-cong
    ; _⁻¹; ⁻¹-inverseʳ; ⁻¹-inverseˡ
    ; x⁻¹≉0; ⁻¹-cong
    ; setoid; isEquivalence; decSetoid; isDecEquivalence
    ) public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
module Languages.ILL.Syntax where

open import level
open import bool
open import nat
open import unit
open import empty
open import eq
open import sum
open import product

open import Utils.HaskellTypes
open import Utils.HaskellFunctions
open import Languages.ILL.TypeSyntax

True : Set
True = ⊤{lzero}

False : Set
False = ⊥{lzero}

Name : Set
Name = ℕ

name-in : ∀{A : Set} → (A → A → 𝔹) → A → List A → Set
name-in eq x ctx with list-member eq x ctx
name-in _ x ctx | tt = True
name-in _ x ctx | ff = False

-- Bound Variable Labels:
data VLabel : Set where
  LLPV : VLabel         -- Let-Bound Left Pattern Variable
  RLPV : VLabel         -- Let-Bound Right Pattern Variable
  LCPV : VLabel         -- Copy-Bound Left Pattern Variable
  RCPV : VLabel         -- Copy-Bound Right Pattern Variable
  BV  : VLabel          -- λ-Bound Variable
  PBV : VLabel          -- Promote-Bound Variable that is ith in the sequence

_vl-eq_ : VLabel → VLabel → 𝔹
LLPV vl-eq LLPV = tt
RLPV vl-eq RLPV = tt
LCPV vl-eq LCPV = tt
RCPV vl-eq RCPV = tt
BV vl-eq BV = tt
PBV vl-eq PBV = tt
_ vl-eq _ = ff

data Pattern : Set where
  PTriv : Pattern
  PTensor : String → String → Pattern

data Term : Set where
  Triv : Term
  FVar : String → Term
  BVar : Name → String → VLabel → Term
  Let : Term → Type → Pattern → Term → Term
  Lam : String → Type → Term → Term
  App : Term → Term → Term
  Tensor : Term → Term → Term
  Promote : List (Triple Term String Type) → Term → Term
  Discard : Term → Term → Term
  Copy : Term → (Prod String String) → Term → Term
  Derelict : Term → Term

{-# TERMINATING #-}
open-t : Name → String → VLabel → Term → Term → Term
open-t x xs l u (BVar y ys l') with x =ℕ y | xs str-eq ys | l vl-eq l'
... | tt | tt | tt = u
... | _  | _  | _ = BVar y ys l'
open-t x xs BV u (Let t₁ y z t₂) = Let (open-t x xs BV u t₁) y z (open-t x xs BV u t₂)
open-t x xs l@LCPV u (Let t₁ y z t₂) = Let (open-t x xs l u t₁) y z (open-t x xs l u t₂)
open-t x xs l@RCPV u (Let t₁ y z t₂) = Let (open-t x xs l u t₁) y z (open-t x xs l u t₂)
open-t x xs l u (Let t₁ a p t₂) = Let (open-t x xs l u t₁) a p (open-t (suc x) xs l u t₂)
open-t x xs BV u (Lam ys a t) = Lam ys a (open-t (suc x) xs BV u t)
open-t x xs l u (Lam ys a t) = Lam ys a (open-t x xs l u t)
open-t x xs l u (App t₁ t₂) = App (open-t x xs l u t₁) (open-t x xs l u t₂)
open-t x xs l u (Tensor t₁ t₂) = Tensor (open-t x xs l u t₁) (open-t x xs l u t₂)
open-t x xs l@PBV y (Promote ms n) = Promote oms (open-t (suc x) xs l y n)
  where
    oms = map (fstMapT (open-t x xs l y)) ms
open-t x xs l y (Promote ms n) = Promote oms (open-t x xs l y n)
  where
    oms = map (fstMapT (open-t x xs l y)) ms
open-t x xs l@LCPV y (Copy m p n) = Copy (open-t x xs l y m ) p (open-t (suc x) xs l y n)
open-t x xs l@RCPV y (Copy m p n) = Copy (open-t x xs l y m ) p (open-t (suc x) xs l y n)
open-t x xs l y (Copy m p n) = Copy (open-t x xs l y m ) p (open-t x xs l y n)
open-t x xs l y (Discard m n) = Discard (open-t x xs l y m) (open-t x xs l y n)
open-t x xs l y (Derelict m) = Derelict (open-t x xs l y m)
open-t _ _ _ _ t = t

{-# TERMINATING #-}
close-t : Name → String → VLabel → String → Term → Term
close-t x xs l y (FVar z) with y str-eq z
... | tt = BVar x xs l
... | ff = FVar z
close-t x xs l@LLPV y (Let t₁ ty p t₂) = Let (close-t x xs l y t₁) ty p (close-t (suc x) xs l y t₂)
close-t x xs l@RLPV y (Let t₁ ty p t₂) = Let (close-t x xs l y t₁) ty p (close-t (suc x) xs l y t₂)
close-t x xs l y (Let t₁ ty p t₂) = Let (close-t x xs l y t₁) ty p (close-t x xs l y t₂)
close-t x xs l@BV y (Lam ys a t) = Lam ys a (close-t (suc x) xs l y t)
close-t x xs l y (Lam ys a t) = Lam ys a (close-t x xs l y t)
close-t x xs l y (App t₁ t₂) = App (close-t x xs l y t₁) (close-t x xs l y t₂)
close-t x xs l y (Tensor t₁ t₂) = Tensor (close-t x xs l y t₁) (close-t x xs l y t₂)
close-t x xs l@PBV y (Promote ms n) = Promote cms (close-t (suc x) xs l y n)
  where
    cms = map (fstMapT (close-t x xs l y)) ms
close-t x xs l y (Promote ms n) = Promote cms (close-t x xs l y n)
  where
    cms = map (fstMapT (close-t x xs l y)) ms
close-t x xs l@LCPV y (Copy m p n) = Copy (close-t x xs l y m) p (close-t (suc x) xs l y n)
close-t x xs l@RCPV y (Copy m p n) = Copy (close-t x xs l y m) p (close-t (suc x) xs l y n)
close-t x xs l y (Copy m p n) = Copy (close-t x xs l y m) p (close-t x xs l y n)
close-t x xs l y (Discard m n) = Discard (close-t x xs l y m) (close-t x xs l y n)
close-t x xs l y (Derelict m) = Derelict (close-t x xs l y m)
close-t _ _ _ _ t = t

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


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

open import HoTT
open import homotopy.PtdAdjoint

module homotopy.SuspAdjointLoop {i} where

private
  SuspFunctor : PtdFunctor i i
  SuspFunctor = record {
    obj = ⊙Susp;
    arr = ⊙Susp-fmap;
    id = ⊙Susp-fmap-idf;
    comp = ⊙Susp-fmap-∘}

  LoopFunctor : PtdFunctor i i
  LoopFunctor = record {
    obj = ⊙Ω;
    arr = ⊙Ω-fmap;
    id = λ _ → ⊙Ω-fmap-idf;
    comp = ⊙Ω-fmap-∘}

  module _ (X : Ptd i) where

    η : de⊙ X → Ω (⊙Susp X)
    η x = σloop X x

    module E = SuspRec (pt X) (pt X) (idf _)

    ε : de⊙ (⊙Susp (⊙Ω X)) → de⊙ X
    ε = E.f

    ⊙η : X ⊙→ ⊙Ω (⊙Susp X)
    ⊙η = (η , σloop-pt)

    ⊙ε : ⊙Susp (⊙Ω X) ⊙→ X
    ⊙ε = (ε , idp)

  η-natural : {X Y : Ptd i} (f : X ⊙→ Y)
    → ⊙η Y ⊙∘ f == ⊙Ω-fmap (⊙Susp-fmap f) ⊙∘ ⊙η X
  η-natural {X = X} (f , idp) = ⊙λ='
    (λ x → ! $
      ap-∙ (Susp-fmap f) (merid x) (! (merid (pt X)))
      ∙ SuspFmap.merid-β f x
        ∙2 (ap-! (Susp-fmap f) (merid (pt X))
            ∙ ap ! (SuspFmap.merid-β f (pt X))))
    (pt-lemma (Susp-fmap f) (merid (pt X)) (SuspFmap.merid-β f (pt X)))
    where
    pt-lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
      {x y : A} (p : x == y) {q : f x == f y} (α : ap f p == q)
      → !-inv-r q == ap (ap f) (!-inv-r p) ∙ idp
        [ _== idp ↓ ! (ap-∙ f p (! p) ∙ α ∙2 (ap-! f p ∙ ap ! α)) ]
    pt-lemma f idp idp = idp

  ε-natural : {X Y : Ptd i} (f : X ⊙→ Y)
    → ⊙ε Y ⊙∘ ⊙Susp-fmap (⊙Ω-fmap f) == f ⊙∘ ⊙ε X
  ε-natural (f , idp) = ⊙λ='
    (SuspElim.f idp idp
      (λ p → ↓-='-from-square $ vert-degen-square $
        ap-∘ (ε _) (Susp-fmap (ap f)) (merid p)
        ∙ ap (ap (ε _)) (SuspFmap.merid-β (ap f) p)
        ∙ E.merid-β _ (ap f p)
        ∙ ap (ap f) (! (E.merid-β _ p))
        ∙ ∘-ap f (ε _) (merid p)))
    idp

  εΣ-Ση : (X : Ptd i) → ⊙ε (⊙Susp X) ⊙∘ ⊙Susp-fmap (⊙η X) == ⊙idf _
  εΣ-Ση X = ⊙λ='
    (SuspElim.f
      idp
      (merid (pt X))
      (λ x → ↓-='-from-square $
        (ap-∘ (ε (⊙Susp X)) (Susp-fmap (η X)) (merid x)
         ∙ ap (ap (ε (⊙Susp X))) (SuspFmap.merid-β (η X) x)
         ∙ E.merid-β _ (merid x ∙ ! (merid (pt X))))
        ∙v⊡ square-lemma (merid x) (merid (pt X))
        ⊡v∙ ! (ap-idf (merid x))))
    idp
    where
    square-lemma : ∀ {i} {A : Type i} {x y z : A}
      (p : x == y) (q : z == y)
      → Square idp (p ∙ ! q) p q
    square-lemma idp idp = ids

  Ωε-ηΩ : (X : Ptd i) → ⊙Ω-fmap (⊙ε X) ⊙∘ ⊙η (⊙Ω X) == ⊙idf _
  Ωε-ηΩ X = ⊙λ='
    (λ p → ap-∙ (ε X) (merid p) (! (merid idp))
         ∙ (E.merid-β X p ∙2 (ap-! (ε X) (merid idp) ∙ ap ! (E.merid-β X idp)))
         ∙ ∙-unit-r _)
    (pt-lemma (ε X) (merid idp) (E.merid-β X idp))
    where
    pt-lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
      {x y : A} (p : x == y) {q : f x == f y} (α : ap f p == q)
      → ap (ap f) (!-inv-r p) ∙ idp == idp
        [ _== idp ↓ ap-∙ f p (! p) ∙ (α ∙2 (ap-! f p ∙ ap ! α)) ∙ !-inv-r q ]
    pt-lemma f idp idp = idp

module Eta = E

adj : CounitUnitAdjoint SuspFunctor LoopFunctor
adj = record {
  η = ⊙η;
  ε = ⊙ε;

  η-natural = η-natural;
  ε-natural = ε-natural;

  εF-Fη = εΣ-Ση;
  Gε-ηG = Ωε-ηΩ}

hadj = counit-unit-to-hom adj

open CounitUnitAdjoint adj public
open HomAdjoint hadj public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Code related to the paper Beating the Productivity Checker Using
-- Embedded Languages
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module Productivity where

------------------------------------------------------------------------
-- Making Programs Guarded

-- A definition of the stream of Fibonacci numbers, as well
-- as a definition of the Hamming numbers.

import StreamProg

------------------------------------------------------------------------
-- Several Types at Once

-- By indexing the program and WHNF types on a universe one can handle
-- several types at the same time.

import UniverseIndex

-- Breadth-first labelling of trees, /almost/ implementing the classic
-- tie-the-recursive-knot algorithm due to Jeremy Gibbons and Geraint
-- Jones (see "Linear-time Breadth-first Tree Algorithms: An Exercise
-- in the Arithmetic of Folds and Zips", or Chris Okasaki's
-- explanation in "Breadth-First Numbering: Lessons from a Small
-- Exercise in Algorithm Design"). Proper sharing is not maintained,
-- though, so this implementation is far from being linear in the size
-- of the tree.

import Stream
import Tree
import BreadthFirst.Universe
import BreadthFirst.Programs
import BreadthFirst

-- A simplified variant of the code above, without any correctness
-- statement or proof.

import BreadthFirstWithoutProof

------------------------------------------------------------------------
-- Making Proofs Guarded

-- Proofs of the map-iterate property and iterate fusion.

import MapIterate

-- A formalisation of parts of Ralf Hinze's paper "Streams and Unique
-- Fixed Points".

import Stream
import Stream.Programs
import Stream.Equality
import Stream.Pointwise
import Hinze.Lemmas
import Hinze.Section2-4
import Hinze.Section3
import Hinze.Simplified.Section2-4
import Hinze.Simplified.Section3

-- Code not mentioned in the paper:

-- An investigation of various ways to define the semantics of an
-- untyped λ-calculus and a virtual machine, and a discussion of
-- compiler correctness. The module Lambda.Closure.Relational uses the
-- language-based technique to establish guardedness.

import Lambda
import Lambda.Closure.Relational

------------------------------------------------------------------------
-- Destructors

-- A somewhat more elaborate/complicated variant of the method which
-- can handle functions like tail.

import SingletonChunks

-- Code not mentioned in the paper:

-- Another variant which can handle tail. I believe that this one has
-- limited applicability.

import LargeCombinators

------------------------------------------------------------------------
-- Other Chunk Sizes

-- A generalised variant of (parts of) SingletonChunks, plus some
-- extra examples.

import ArbitraryChunks

-- Implementations of the Thue-Morse sequence, using non-uniform chunk
-- sizes.

import ThueMorse
import ThueMorseLeq

------------------------------------------------------------------------
-- Nested Applications

-- An example which shows that nested applications of the defined
-- function can be handled.

import Nested

-- Code not mentioned in the paper:

-- A solution to a problem posed by Venanzio Capretta: The equation
--
--   φ s = s ⋎ φ (evens (φ s))
--
-- has at most one solution. (Notice the nested uses of φ, and the use
-- of evens which removes every other element from its input.)

import VenanziosProblem

------------------------------------------------------------------------
-- Related Work

-- Formalisation of subtyping for recursive types, partly based on
-- "Coinductive Axiomatization of Recursive Type Equality and
-- Subtyping" by Michael Brandt and Fritz Henglein.

import RecursiveTypes

-- The following modules use the language-based technique to establish
-- guardedness. The last of them was briefly discussed in the paper.

import RecursiveTypes.Subtyping.Semantic.Coinductive
import RecursiveTypes.Subtyping.Axiomatic.Coinductive
import RecursiveTypes.Subtyping.Axiomatic.Inductive

-- An implementation of "A Unifying Approach to Recursive and
-- Co-recursive Definitions" by Pietro Di Gianantonio and Marino
-- Miculan. Contains one postulate.

import Contractive
import Contractive.Function
import Contractive.Stream
import Contractive.Examples

------------------------------------------------------------------------
-- Appendix

-- A sound, inductive approximation of stream equality.

import InductiveStreamEquality

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- Andreas, 2011-04-14
-- {-# OPTIONS -v tc.cover:20 -v tc.lhs.unify:20 #-}
module Issue291a where

open import Imports.Coinduction

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

data RUnit : Set where
  runit : ∞ RUnit -> RUnit

j : (u : ∞ RUnit) -> ♭ u ≡ runit u -> Set
j u ()
-- needs to fail (reports a Bad split!)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment