text:
------------------------------------------------------------------------
-- Integers
------------------------------------------------------------------------

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

open import Equality

module Integer {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude as P hiding (suc) renaming (_+_ to _⊕_; _*_ to _⊛_)

open import Bijection eq using (_↔_)
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq hiding (_∘_)
open import Group eq using (Group; Abelian)
open import H-level eq
open import H-level.Closure eq
import Nat eq as Nat

open import Integer.Basics eq public

private
  variable
    i j : ℤ

------------------------------------------------------------------------
-- Some lemmas

-- The sum of i and - i is zero.

+-right-inverse : ∀ i → i + - i ≡ + 0
+-right-inverse = λ where
    (+ zero)    → refl _
    (+ P.suc n) → lemma n
    -[1+ n ]    → lemma n
  where
  lemma : ∀ n → + P.suc n +-[1+ n ] ≡ + 0
  lemma n
    with P.suc n Nat.<= n | T[<=]↔≤ {m = P.suc n} {n = n}
  … | false | _  = cong (+_) $ Nat.∸≡0 n
  … | true  | eq = ⊥-elim $ Nat.<-irreflexive (_↔_.to eq _)

-- The sum of - i and i is zero.

+-left-inverse : ∀ i → - i + i ≡ + 0
+-left-inverse i =
  - i + i  ≡⟨ +-comm (- i) ⟩
  i + - i  ≡⟨ +-right-inverse i ⟩∎
  + 0      ∎

-- + 0 is a left identity for addition.

+-left-identity : + 0 + i ≡ i
+-left-identity {i = + _}      = refl _
+-left-identity {i = -[1+ _ ]} = refl _

-- + 0 is a right identity for addition.

+-right-identity : i + + 0 ≡ i
+-right-identity {i = + _}      = cong (+_) Nat.+-right-identity
+-right-identity {i = -[1+ _ ]} = refl _

-- Addition is associative.

+-assoc : ∀ i {j k} → i + (j + k) ≡ (i + j) + k
+-assoc = λ where
    (+ m) {j = + _} {k = + _} →
      cong (+_) $ Nat.+-assoc m
    -[1+ m ] {j = -[1+ n ]} {k = -[1+ o ]} →
      cong (-[1+_] ∘ P.suc)
        (m ⊕ P.suc (n ⊕ o)  ≡⟨ sym $ Nat.suc+≡+suc m ⟩
         P.suc m ⊕ (n ⊕ o)  ≡⟨ Nat.+-assoc (P.suc m) ⟩∎
         (P.suc m ⊕ n) ⊕ o  ∎)
    -[1+ m ] {j = + n} {k = + o} →
      sym $ ++-[1+]++ _ n _
    (+ m) {j = -[1+ n ]} {k = -[1+ o ]} →
      sym $ ++-[1+]+-[1+] m _ _
    (+ m) {j = + n} {k = -[1+ o ]} →
      lemma₁ m _ _
    (+ m) {j = -[1+ n ]} {k = + o} →
      lemma₂ m _ _
    -[1+ m ] {j = -[1+ n ]} {k = + o} →
      lemma₃ _ o _
    -[1+ m ] {j = + n} {k = -[1+ o ]} →
      lemma₄ _ n _
  where
  ++-[1+]++ : ∀ m n o → + n +-[1+ m ] + + o ≡ (+ (n ⊕ o) +-[1+ m ])
  ++-[1+]++ m         zero      o = refl _
  ++-[1+]++ zero      (P.suc n) o = refl _
  ++-[1+]++ (P.suc m) (P.suc n) o = ++-[1+]++ m n o

  ++-[1+]+-[1+] :
    ∀ m n o → + m +-[1+ n ] + -[1+ o ] ≡ (+ m +-[1+ 1 ⊕ n ⊕ o ])
  ++-[1+]+-[1+] zero      n         o = refl _
  ++-[1+]+-[1+] (P.suc m) zero      o = refl _
  ++-[1+]+-[1+] (P.suc m) (P.suc n) o = ++-[1+]+-[1+] m n o

  lemma₁ : ∀ m n o → + m + (+ n +-[1+ o ]) ≡ (+ m ⊕ n +-[1+ o ])
  lemma₁ m n o =
    + m + (+ n +-[1+ o ])  ≡⟨ +-comm (+ m) {j = + n +-[1+ o ]} ⟩
    (+ n +-[1+ o ]) + + m  ≡⟨ ++-[1+]++ _ n _ ⟩
    (+ n ⊕ m +-[1+ o ])    ≡⟨ cong +_+-[1+ o ] $ Nat.+-comm n ⟩∎
    (+ m ⊕ n +-[1+ o ])    ∎

  lemma₂ : ∀ m n o → + m + (+ n +-[1+ o ]) ≡ (+ m +-[1+ o ]) + + n
  lemma₂ m n o =
    + m + (+ n +-[1+ o ])  ≡⟨ lemma₁ m n o ⟩
    (+ m ⊕ n +-[1+ o ])    ≡⟨ sym $ ++-[1+]++ _ m _ ⟩∎
    (+ m +-[1+ o ]) + + n  ∎

  lemma₃ :
    ∀ m n o → -[1+ m ] + (+ n +-[1+ o ]) ≡ (+ n +-[1+ 1 ⊕ m ⊕ o ])
  lemma₃ m n o =
    -[1+ m ] + (+ n +-[1+ o ])  ≡⟨ +-comm -[1+ m ] {j = + n +-[1+ o ]} ⟩
    (+ n +-[1+ o ]) + -[1+ m ]  ≡⟨ ++-[1+]+-[1+] n o m ⟩
    (+ n +-[1+ 1 ⊕ o ⊕ m ])     ≡⟨ cong + n +-[1+_] $ cong (1 ⊕_) $ Nat.+-comm o ⟩∎
    (+ n +-[1+ 1 ⊕ m ⊕ o ])     ∎

  lemma₄ :
    ∀ m n o → -[1+ m ] + (+ n +-[1+ o ]) ≡ (+ n +-[1+ m ]) + -[1+ o ]
  lemma₄ m n o =
    -[1+ m ] + (+ n +-[1+ o ])  ≡⟨ lemma₃ m n o ⟩
    (+ n +-[1+ 1 ⊕ m ⊕ o ])     ≡⟨ sym $ ++-[1+]+-[1+] n _ _ ⟩∎
    (+ n +-[1+ m ]) + -[1+ o ]  ∎

------------------------------------------------------------------------
-- Successor and predecessor

-- The successor function.

suc : ℤ → ℤ
suc (+ n)          = + P.suc n
suc -[1+ zero ]    = + zero
suc -[1+ P.suc n ] = -[1+ n ]

-- The successor function adds one to its input.

suc≡1+ : ∀ i → suc i ≡ + 1 + i
suc≡1+ (+ _)          = refl _
suc≡1+ -[1+ zero ]    = refl _
suc≡1+ -[1+ P.suc _ ] = refl _

-- The predecessor function.

pred : ℤ → ℤ
pred (+ zero)    = -[1+ zero ]
pred (+ P.suc n) = + n
pred -[1+ n ]    = -[1+ P.suc n ]

-- The predecessor function adds minus one to its input.

pred≡-1+ : ∀ i → pred i ≡ -[ 1 ] + i
pred≡-1+ (+ zero)    = refl _
pred≡-1+ (+ P.suc _) = refl _
pred≡-1+ -[1+ _ ]    = refl _

-- An equivalence between ℤ and ℤ corresponding to the successor
-- function.

successor : ℤ ≃ ℤ
successor = Eq.↔→≃ suc pred suc-pred pred-suc
  where
  suc-pred : ∀ i → suc (pred i) ≡ i
  suc-pred (+ zero)    = refl _
  suc-pred (+ P.suc _) = refl _
  suc-pred -[1+ _ ]    = refl _

  pred-suc : ∀ i → pred (suc i) ≡ i
  pred-suc (+ _)          = refl _
  pred-suc -[1+ zero ]    = refl _
  pred-suc -[1+ P.suc _ ] = refl _

------------------------------------------------------------------------
-- Positive, negative

-- The property of being positive.

Positive : ℤ → Type
Positive (+ zero)    = ⊥
Positive (+ P.suc _) = ⊤
Positive -[1+ _ ]    = ⊥

-- Positive is propositional.

Positive-propositional : Is-proposition (Positive i)
Positive-propositional {i = + zero}    = ⊥-propositional
Positive-propositional {i = + P.suc _} = mono₁ 0 ⊤-contractible
Positive-propositional {i = -[1+ _ ]}  = ⊥-propositional

-- The property of being negative.

Negative : ℤ → Type
Negative (+ _)    = ⊥
Negative -[1+ _ ] = ⊤

-- Negative is propositional.

Negative-propositional : Is-proposition (Negative i)
Negative-propositional {i = + _}      = ⊥-propositional
Negative-propositional {i = -[1+ _ ]} = mono₁ 0 ⊤-contractible

-- No integer is both positive and negative.

¬+- : Positive i → Negative i → ⊥₀
¬+- {i = + _}      _   neg = neg
¬+- {i = -[1+ _ ]} pos _   = pos

-- No integer is both positive and equal to zero.

¬+0 : Positive i → i ≡ + 0 → ⊥₀
¬+0 {i = + zero}    pos _  = pos
¬+0 {i = + P.suc _} _   ≡0 = Nat.0≢+ $ sym $ +-cancellative ≡0
¬+0 {i = -[1+ _ ]}  pos _  = pos

-- No integer is both negative and equal to zero.

¬-0 : Negative i → i ≡ + 0 → ⊥₀
¬-0 {i = + _}      neg _  = neg
¬-0 {i = -[1+ _ ]} _   ≡0 = +≢-[1+] $ sym ≡0

-- One can decide if an integer is negative, zero or positive.

-⊎0⊎+ : ∀ i → Negative i ⊎ i ≡ + 0 ⊎ Positive i
-⊎0⊎+ (+ zero)    = inj₂ (inj₁ (refl _))
-⊎0⊎+ (+ P.suc _) = inj₂ (inj₂ _)
-⊎0⊎+ -[1+ _ ]    = inj₁ _

-- If i and j are positive, then i + j is positive.

>0→>0→+>0 : ∀ i j → Positive i → Positive j → Positive (i + j)
>0→>0→+>0 (+ P.suc _) (+ P.suc _) _ _ = _

-- If i and j are negative, then i + j is negative.

<0→<0→+<0 : ∀ i j → Negative i → Negative j → Negative (i + j)
<0→<0→+<0 -[1+ _ ] -[1+ _ ] _ _ = _

------------------------------------------------------------------------
-- The group of integers

-- The group of integers.

ℤ-group : Group lzero
ℤ-group .Group.Carrier          = ℤ
ℤ-group .Group.Carrier-is-set   = ℤ-set
ℤ-group .Group._∘_              = _+_
ℤ-group .Group.id               = + 0
ℤ-group .Group._⁻¹              = -_
ℤ-group .Group.left-identity _  = +-left-identity
ℤ-group .Group.right-identity _ = +-right-identity
ℤ-group .Group.assoc i _ _      = +-assoc i
ℤ-group .Group.right-inverse    = +-right-inverse
ℤ-group .Group.left-inverse     = +-left-inverse

-- The group of integers is abelian.

ℤ-abelian : Abelian ℤ-group
ℤ-abelian i _ = +-comm i

private
  module ℤG = Group ℤ-group
open ℤG public
  using ()
  renaming (_^+_ to infixl 7 _*+_;
            _^_  to infixl 7 _*_)

-- + 1 is a left identity for multiplication.

*-left-identity : ∀ i → + 1 * i ≡ i
*-left-identity = lemma
  where
  +lemma : ∀ n → + 1 *+ n ≡ + n
  +lemma zero      = refl _
  +lemma (P.suc n) =
    + 1 + (+ 1) *+ n  ≡⟨ cong (λ i → + 1 + i) $ +lemma n ⟩
    + 1 + + n         ≡⟨⟩
    + P.suc n         ∎

  -lemma : ∀ n → -[ 1 ] *+ n ≡ -[ n ]
  -lemma zero              = refl _
  -lemma (P.suc zero)      = refl _
  -lemma (P.suc (P.suc n)) =
    -[ 1 ] + -[ 1 ] *+ P.suc n  ≡⟨ cong (λ i → -[ 1 ] + i) $ -lemma (P.suc n) ⟩
    -[ 1 ] + -[ P.suc n ]       ≡⟨⟩
    -[ P.suc (P.suc n) ]        ∎

  lemma : ∀ i → + 1 * i ≡ i
  lemma (+ n)    = +lemma n
  lemma -[1+ n ] = -lemma (P.suc n)

-- _*+ n distributes over addition.

*+-distrib-+ : ∀ n → (i + j) *+ n ≡ i *+ n + j *+ n
*+-distrib-+ {i = i} n = ℤG.∘^+≡^+∘^+ (+-comm i) n

-- If a positive number is multiplied by a positive number, then
-- the result is positive.

>0→*+suc> : ∀ i m → Positive i → Positive (i *+ P.suc m)
>0→*+suc> i zero =
  Positive i          ↝⟨ subst Positive (sym $ ℤG.right-identity i) ⟩
  Positive (i + + 0)  ↔⟨⟩
  Positive (i *+ 1)   □
>0→*+suc> i (P.suc m) =
  Positive i                            ↝⟨ (λ p → p , >0→*+suc> i m p) ⟩
  Positive i × Positive (i *+ P.suc m)  ↝⟨ uncurry (>0→>0→+>0 i (i *+ P.suc m)) ⟩
  Positive (i + i *+ P.suc m)           ↔⟨⟩
  Positive (i *+ P.suc (P.suc m))       □

-- If a negative number is multiplied by a positive number, then
-- the result is negative.

<0→*+suc<0 : ∀ i m → Negative i → Negative (i *+ P.suc m)
<0→*+suc<0 i zero =
  Negative i          ↝⟨ subst Negative (sym $ ℤG.right-identity i) ⟩
  Negative (i + + 0)  ↔⟨⟩
  Negative (i *+ 1)   □
<0→*+suc<0 i (P.suc m) =
  Negative i                            ↝⟨ (λ p → p , <0→*+suc<0 i m p) ⟩
  Negative i × Negative (i *+ P.suc m)  ↝⟨ uncurry (<0→<0→+<0 i (i *+ P.suc m)) ⟩
  Negative (i + i *+ P.suc m)           ↔⟨⟩
  Negative (i *+ P.suc (P.suc m))       □

------------------------------------------------------------------------
-- Integer division by two

-- Division by two, rounded downwards.

⌊_/2⌋ : ℤ → ℤ
⌊ + n      /2⌋ = + Nat.⌊ n /2⌋
⌊ -[1+ n ] /2⌋ = -[ Nat.⌈ P.suc n /2⌉ ]

-- A kind of distributivity property for ⌊_/2⌋ and _+_.

⌊+*+2/2⌋≡ : ∀ i {j} → ⌊ i + j *+ 2 /2⌋ ≡ ⌊ i /2⌋ + j
⌊+*+2/2⌋≡ = λ where
    (+ m) {j = + n} → cong +_
      (Nat.⌊ m ⊕ 2 ⊛ n /2⌋  ≡⟨ cong Nat.⌊_/2⌋ $ Nat.+-comm m ⟩
       Nat.⌊ 2 ⊛ n ⊕ m /2⌋  ≡⟨ Nat.⌊2*+/2⌋≡ n ⟩
       n ⊕ Nat.⌊ m /2⌋      ≡⟨ Nat.+-comm n ⟩∎
       Nat.⌊ m /2⌋ ⊕ n      ∎)

    -[1+ zero ] {j = -[1+ n ]} → cong -[1+_]
      (Nat.⌈ P.suc (n ⊕ n) /2⌉            ≡⟨ cong (Nat.⌈_/2⌉ ∘ P.suc) $ ⊕-lemma n ⟩
       Nat.⌈ 1 ⊕ 2 ⊛ n /2⌉                ≡⟨ cong Nat.⌈_/2⌉ $ Nat.+-comm 1 ⟩
       Nat.⌈ 2 ⊛ n ⊕ 1 /2⌉                ≡⟨ Nat.⌈2*+/2⌉≡ n ⟩
       n ⊕ Nat.⌈ 1 /2⌉                    ≡⟨ Nat.+-comm n ⟩∎
       P.suc n                            ∎)

    -[1+ P.suc m ] {j = -[1+ n ]} → cong -[1+_]
      (Nat.⌈ P.suc m ⊕ P.suc (n ⊕ n) /2⌉  ≡⟨ cong (Nat.⌈_/2⌉ ∘ P.suc) $ sym $ Nat.suc+≡+suc m ⟩
       P.suc Nat.⌈ m ⊕ (n ⊕ n) /2⌉        ≡⟨ cong (P.suc ∘ Nat.⌈_/2⌉ ∘ (m ⊕_)) $ ⊕-lemma n ⟩
       P.suc Nat.⌈ m ⊕ 2 ⊛ n /2⌉          ≡⟨ cong (P.suc ∘ Nat.⌈_/2⌉) $ Nat.+-comm m ⟩
       P.suc Nat.⌈ 2 ⊛ n ⊕ m /2⌉          ≡⟨ cong P.suc $ Nat.⌈2*+/2⌉≡ n ⟩
       P.suc (n ⊕ Nat.⌈ m /2⌉)            ≡⟨ cong P.suc $ Nat.+-comm n ⟩∎
       P.suc (Nat.⌈ m /2⌉ ⊕ n)            ∎)

    (+ m) {j = -[1+ n ]} →
      ⌊ + m +-[1+ P.suc (n ⊕ n) ] /2⌋  ≡⟨ cong (λ n → ⌊ + m +-[1+ P.suc n ] /2⌋) $ ⊕-lemma n ⟩
      ⌊ + m +-[1+ P.suc (2 ⊛ n) ] /2⌋  ≡⟨ lemma₁ m n ⟩∎
      + Nat.⌊ m /2⌋ +-[1+ n ]          ∎

    -[1+ 0 ] {j = + 0} →
      -[ 1 ]  ≡⟨⟩
      -[ 1 ]  ∎

    -[1+ 0 ] {j = + P.suc n} → cong +_
      (Nat.⌊ n ⊕ P.suc (n ⊕ 0) /2⌋  ≡⟨ cong Nat.⌊_/2⌋ $ sym $ Nat.suc+≡+suc n ⟩
       Nat.⌊ 1 ⊕ 2 ⊛ n /2⌋          ≡⟨ Nat.⌊1+2*/2⌋≡ n ⟩∎
       n                            ∎)

    -[1+ P.suc m ] {j = + n} →
      ⌊ + 2 ⊛ n +-[1+ P.suc m ] /2⌋  ≡⟨ lemma₂ m n ⟩∎
      + n +-[1+ Nat.⌈ m /2⌉ ]        ∎
  where
  ⊕-lemma : ∀ n → n ⊕ n ≡ 2 ⊛ n
  ⊕-lemma n = cong (n ⊕_) $ sym Nat.+-right-identity

  lemma₁ :
    ∀ m n →
    ⌊ + m +-[1+ P.suc (2 ⊛ n) ] /2⌋ ≡
    + Nat.⌊ m /2⌋ +-[1+ n ]
  lemma₁ zero n = cong -[1+_]
    (Nat.⌈ 2 ⊛ n /2⌉  ≡⟨ Nat.⌈2*/2⌉≡ n ⟩∎
     n                ∎)
  lemma₁ (P.suc zero) n =
    -[ Nat.⌈ 1 ⊕ 2 ⊛ n /2⌉ ]  ≡⟨ cong -[_] $ Nat.⌈1+2*/2⌉≡ n ⟩∎
    -[1+ n ]                  ∎
  lemma₁ (P.suc (P.suc m)) zero =
    ⌊ + m /2⌋      ≡⟨⟩
    + Nat.⌊ m /2⌋  ∎
  lemma₁ (P.suc (P.suc m)) (P.suc n) =
    ⌊ + m +-[1+ n ⊕ P.suc (n ⊕ 0) ] /2⌋  ≡⟨ cong (⌊_/2⌋ ∘ + m +-[1+_]) $ sym $ Nat.suc+≡+suc n ⟩
    ⌊ + m +-[1+ P.suc (2 ⊛ n) ] /2⌋      ≡⟨ lemma₁ m n ⟩∎
    + Nat.⌊ m /2⌋ +-[1+ n ]              ∎

  mutual

    lemma₂ :
      ∀ m n →
      ⌊ + 2 ⊛ n +-[1+ P.suc m ] /2⌋ ≡
      + n +-[1+ Nat.⌈ m /2⌉ ]
    lemma₂ m zero =
      ⌊ -[1+ P.suc m ] /2⌋  ≡⟨⟩
      -[1+ Nat.⌈ m /2⌉ ]    ∎
    lemma₂ m (P.suc n) =
      ⌊ + n ⊕ P.suc (n ⊕ 0) +-[1+ m ] /2⌋  ≡⟨ cong (⌊_/2⌋ ∘ +_+-[1+ m ]) $ sym $ Nat.suc+≡+suc n ⟩
      ⌊ + P.suc (2 ⊛ n) +-[1+ m ] /2⌋      ≡⟨ lemma₃ m n ⟩∎
      + P.suc n +-[1+ Nat.⌈ m /2⌉ ]        ∎

    lemma₃ :
      ∀ m n →
      ⌊ + P.suc (2 ⊛ n) +-[1+ m ] /2⌋ ≡
      + P.suc n +-[1+ Nat.⌈ m /2⌉ ]
    lemma₃ zero n = cong +_
      (Nat.⌊ 2 ⊛ n /2⌋  ≡⟨ Nat.⌊2*/2⌋≡ n ⟩∎
       n                ∎)
    lemma₃ (P.suc zero) zero =
      -[ 1 ]  ≡⟨⟩
      -[ 1 ]  ∎
    lemma₃ (P.suc zero) (P.suc n) = cong +_
      (Nat.⌊ n ⊕ P.suc (n ⊕ zero) /2⌋  ≡⟨ cong Nat.⌊_/2⌋ $ sym $ Nat.suc+≡+suc n ⟩
       Nat.⌊ 1 ⊕ 2 ⊛ n /2⌋             ≡⟨ Nat.⌊1+2*/2⌋≡ n ⟩∎
       n                               ∎)
    lemma₃ (P.suc (P.suc m)) n =
      ⌊ + 2 ⊛ n +-[1+ P.suc m ] /2⌋  ≡⟨ lemma₂ m n ⟩∎
      + n +-[1+ Nat.⌈ m /2⌉ ]        ∎

-- If you double and then halve an integer, then you get back what you
-- started with.

⌊*+2/2⌋≡ : ∀ i → ⌊ i *+ 2 /2⌋ ≡ i
⌊*+2/2⌋≡ i =
  ⌊ i *+ 2 /2⌋        ≡⟨ cong ⌊_/2⌋ $ sym $ +-left-identity {i = i *+ 2} ⟩
  ⌊ + 0 + i *+ 2 /2⌋  ≡⟨ ⌊+*+2/2⌋≡ (+ 0) {j = i} ⟩
  ⌊ + 0 /2⌋ + i       ≡⟨⟩
  + 0 + i             ≡⟨ +-left-identity ⟩∎
  i                   ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Coinduction using ( ♯_ )
open import Data.Bool using ( Bool ; true ; false ; not )
open import Data.ByteString using ( null ) renaming ( span to #span )
open import Data.Natural using ( Natural )
open import Data.Product using ( _×_ ; _,_ )
open import Data.Word using ( Byte )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; _⟫_ ; π₁ ; π₂ ; _[&]_ )
open import System.IO.Transducers.Weight using ( weight )
open import System.IO.Transducers.Stateful using ( loop )
open import System.IO.Transducers.Session using ( ⟨_⟩ ; _&_ ; ¿ ; * ; _&*_ )
open import System.IO.Transducers.Strict using ( _⇛_ )

module System.IO.Transducers.Bytes where

open System.IO.Transducers.Session public using ( Bytes ; Bytes' )

mutual

  span' : (Byte → Bool) → Bytes' ⇛ (Bytes & Bytes)
  span' φ x with #span φ x
  span' φ x | (x₁ , x₂) with null x₁ | null x₂
  span' φ x | (x₁ , x₂) | true  | true  = inp (♯ span φ)
  span' φ x | (x₁ , x₂) | true  | false = out false (out true (out x₂ done))
  span' φ x | (x₁ , x₂) | false | true  = out true (out x₁ (inp (♯ span φ)))
  span' φ x | (x₁ , x₂) | false | false = out true (out x₁ (out false (out true (out x₂ done))))

  span : (Byte → Bool) → Bytes ⇛ (Bytes & Bytes)
  span φ false = out false (out false done)
  span φ true  = inp (♯ span' φ)

break : (Byte → Bool) → Bytes ⇛ (Bytes & Bytes)
break φ = span (λ x → not (φ x))

mutual

  nonempty' : Bytes' & Bytes ⇛ ¿ Bytes & Bytes
  nonempty' x with null x
  nonempty' x | true  = inp (♯ nonempty)
  nonempty' x | false = out true (out true (out x done))

  nonempty : Bytes & Bytes ⇛ ¿ Bytes & Bytes
  nonempty true  = inp (♯ nonempty')
  nonempty false = out false done

split? : (Byte → Bool) → Bytes ⇒ (¿ Bytes & Bytes)
split? φ = inp (♯ span φ) ⟫ π₂ {Bytes} ⟫ inp (♯ break φ) ⟫ inp (♯ nonempty)

split : (Byte → Bool) → Bytes ⇒ * Bytes
split φ = loop {Bytes} (split? φ) ⟫ π₁

bytes : Bytes ⇒ ⟨ Natural ⟩
bytes = weight

ext: agda

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
-- Andreas, 2016-02-02 added Ambiguous

module Issue480 where

module Simple where

  data Q : Set where
    a : Q

  f : _ → Q
  f a = a

  postulate helper : ∀ {T : Set} → (T → T) → Q

  test₁ : Q → Q
  test₁ = λ { a → a }

  test₂ : Q
  test₂ = helper test₁

  -- Same as test₂ and test₁, but stuck together.
  test₃ : Q
  test₃ = helper λ { a → a } -- this says "Type mismatch when checking that the pattern a has type _45"

module Ambiguous where

  data Q : Set where
    a : Q

  data Overlap : Set where
    a : Overlap

  postulate helper : ∀ {T : Set} → (T → T) → T -- result type needs to be propagated

  test₁ : Q → Q
  test₁ = λ { a → a }

  test₃ : Q
  test₃ = helper λ { a → a }

  _$_ : ∀ {T : Set} → (T → T) → T → T
  f $ x = f x

  test : Q
  test = (λ { a → a }) $ a

  test₂ : _
  test₂ = (λ { a → a }) $ Q.a

module Example where

  infixr 5 _∷_

  data ℕ : Set where
    zero : ℕ
    suc  : (n : ℕ) → ℕ

  data List : Set₁ where
    []   : List
    _∷_  : Set → List → List

  data Tree (L : Set) : List → Set₁ where
    tip  : Tree L []
    node : ∀ {T Ts} → (cs : T → Tree L Ts) → Tree L (T ∷ Ts)

  data Q (n : ℕ) : Set where
    a : Q n
    b : Q n

  test₁ : Q zero → Tree ℕ (Q zero ∷ [])
  test₁ = λ
    { a → node λ { a → tip ; b → tip }
    ; b → node λ { a → tip ; b → tip }
    }

  test₂ = node test₁

  test₃ : Tree ℕ (Q zero ∷ Q zero ∷ [])
  test₃ = node λ
    { a → node λ { a → tip ; b → tip }
    ; b → node λ { a → tip ; b → tip }
    }


text:
{-# OPTIONS --guardedness #-}
module Builtin.Coinduction where

open import Agda.Builtin.Coinduction public

max_stars_repo_name: UlfNorell/agda-prelude

max_issues_repo_name: UlfNorell/agda-prelude

max_forks_repo_name: UlfNorell/agda-prelude


text:
module FFI.Data.Either where

{-# FOREIGN GHC import qualified Data.Either #-}

data Either (A B : Set) : Set where
  Left : A → Either A B
  Right : B → Either A B
{-# COMPILE GHC Either = data Data.Either.Either (Data.Either.Left|Data.Either.Right) #-}

swapLR : ∀ {A B} → Either A B → Either B A
swapLR (Left x) = Right x
swapLR (Right x) = Left x

mapL : ∀ {A B C} → (A → B) → Either A C → Either B C
mapL f (Left x) = Left (f x)
mapL f (Right x) = Right x

mapR : ∀ {A B C} → (B → C) → Either A B → Either A C
mapR f (Left x) = Left x
mapR f (Right x) = Right (f x)

mapLR : ∀ {A B C D} → (A → B) → (C → D) → Either A C → Either B D
mapLR f g (Left x) = Left (f x)
mapLR f g (Right x) = Right (g x)

cond : ∀ {A B C : Set} → (A → C) → (B → C) → (Either A B) → C
cond f g (Left x) = f x
cond f g (Right x) = g x

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
-- Andreas, 2018-10-27, issue #3324 reported by Guillaume Brunerie
-- Missing 'reduce' leads to arbitrary rejection of pattern matching on props

{-# OPTIONS --prop #-}

-- {-# OPTIONS -v tc.cover:60 #-}

data Unit : Prop where
  tt : Unit

-- Works
f : {A : Set} → Unit → Unit
f tt = tt

-- Should work
g : Unit → Unit
g tt = tt

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Transitive closures
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Closure.Transitive where

open import Function
open import Function.Equivalence as Equiv using (_⇔_)
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

------------------------------------------------------------------------
-- Transitive closure

infix 4 Plus

syntax Plus R x y = x [ R ]⁺ y

data Plus {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  [_]     : ∀ {x y} (x∼y : x ∼ y) → x [ _∼_ ]⁺ y
  _∼⁺⟨_⟩_ : ∀ x {y z} (x∼⁺y : x [ _∼_ ]⁺ y) (y∼⁺z : y [ _∼_ ]⁺ z) →
            x [ _∼_ ]⁺ z

module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where

 []-injective : ∀ {x y p q} → (x [ _∼_ ]⁺ y ∋ [ p ]) ≡ [ q ] → p ≡ q
 []-injective refl = refl

 -- See also ∼⁺⟨⟩-injectiveˡ and ∼⁺⟨⟩-injectiveʳ in
 -- Relation.Binary.Construct.Closure.Transitive.WithK.

-- "Equational" reasoning notation. Example:
--
--   lemma =
--     x  ∼⁺⟨ [ lemma₁ ] ⟩
--     y  ∼⁺⟨ lemma₂ ⟩∎
--     z  ∎

finally : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} x y →
          x [ _∼_ ]⁺ y → x [ _∼_ ]⁺ y
finally _ _ = id

syntax finally x y x∼⁺y = x ∼⁺⟨ x∼⁺y ⟩∎ y ∎

infixr 2 _∼⁺⟨_⟩_
infix  3 finally

-- Map.

map : ∀ {a a′ ℓ ℓ′} {A : Set a} {A′ : Set a′}
        {_R_ : Rel A ℓ} {_R′_ : Rel A′ ℓ′} {f : A → A′} →
      _R_ =[ f ]⇒ _R′_ → Plus _R_ =[ f ]⇒ Plus _R′_
map R⇒R′ [ xRy ]             = [ R⇒R′ xRy ]
map R⇒R′ (x ∼⁺⟨ xR⁺z ⟩ zR⁺y) =
  _ ∼⁺⟨ map R⇒R′ xR⁺z ⟩ map R⇒R′ zR⁺y

------------------------------------------------------------------------
-- Alternative definition of transitive closure

-- A generalisation of Data.List.Nonempty.List⁺.

infixr 5 _∷_ _++_
infix  4 Plus′

syntax Plus′ R x y = x ⟨ R ⟩⁺ y

data Plus′ {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  [_] : ∀ {x y} (x∼y : x ∼ y) → x ⟨ _∼_ ⟩⁺ y
  _∷_ : ∀ {x y z} (x∼y : x ∼ y) (y∼⁺z : y ⟨ _∼_ ⟩⁺ z) → x ⟨ _∼_ ⟩⁺ z

-- Transitivity.

_++_ : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} {x y z} →
       x ⟨ _∼_ ⟩⁺ y → y ⟨ _∼_ ⟩⁺ z → x ⟨ _∼_ ⟩⁺ z
[ x∼y ]      ++ y∼⁺z = x∼y ∷ y∼⁺z
(x∼y ∷ y∼⁺z) ++ z∼⁺u = x∼y ∷ (y∼⁺z ++ z∼⁺u)

-- Plus and Plus′ are equivalent.

equivalent : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} {x y} →
             Plus _∼_ x y ⇔ Plus′ _∼_ x y
equivalent {_∼_ = _∼_} = Equiv.equivalence complete sound
  where
  complete : Plus _∼_ ⇒ Plus′ _∼_
  complete [ x∼y ]             = [ x∼y ]
  complete (x ∼⁺⟨ x∼⁺y ⟩ y∼⁺z) = complete x∼⁺y ++ complete y∼⁺z

  sound : Plus′ _∼_ ⇒ Plus _∼_
  sound [ x∼y ]      = [ x∼y ]
  sound (x∼y ∷ y∼⁺z) = _ ∼⁺⟨ [ x∼y ] ⟩ sound y∼⁺z


text:
------------------------------------------------------------------------
-- Imports every module so that it is easy to see if everything builds
------------------------------------------------------------------------

module Everything where

import Parallel
import Parallel.Examples
import Parallel.Index
import Parallel.Lib
import RecursiveDescent.Coinductive
import RecursiveDescent.Coinductive.Examples
import RecursiveDescent.Coinductive.Internal
import RecursiveDescent.Coinductive.Lib
import RecursiveDescent.Hybrid
import RecursiveDescent.Hybrid.Examples
import RecursiveDescent.Hybrid.Lib
-- import RecursiveDescent.Hybrid.Memoised  -- Agda is too slow...
import RecursiveDescent.Hybrid.Memoised.Monad
import RecursiveDescent.Hybrid.Mixfix
  hiding (module Expr)  -- Necessary due to an Agda bug.
import RecursiveDescent.Hybrid.Mixfix.Example
import RecursiveDescent.Hybrid.Mixfix.Expr
import RecursiveDescent.Hybrid.Mixfix.Fixity
import RecursiveDescent.Hybrid.PBM
import RecursiveDescent.Hybrid.Simple
import RecursiveDescent.Hybrid.Type
import RecursiveDescent.Index
import RecursiveDescent.Inductive
import RecursiveDescent.Inductive.Char
import RecursiveDescent.Inductive.Examples
import RecursiveDescent.Inductive.Internal
import RecursiveDescent.Inductive.Lib
import RecursiveDescent.Inductive.Semantics
import RecursiveDescent.Inductive.SimpleLib
import RecursiveDescent.Inductive.Token
import RecursiveDescent.InductiveWithFix
import RecursiveDescent.InductiveWithFix.Examples
import RecursiveDescent.InductiveWithFix.Internal
import RecursiveDescent.InductiveWithFix.Lib
import RecursiveDescent.InductiveWithFix.PBM
import Utilities

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
open import Prelude
open import Prelude.List.Relations.Any
open import Prelude.List.Relations.Properties
open import Tactic.Deriving.Eq
open import Tactic.Reflection

module DeriveEqTest where

  module Test₀ where

    eqVec : deriveEqType Vec
    unquoteDef eqVec = deriveEqDef eqVec (quote Vec)

  module Test₁ where

    data D (A : Set) (B : A → Set) : Set where
      c : (x : A) → B x → D A B

    eqD : {A : Set} {B : A → Set} {{_ : Eq A}} {{_ : {x : A} → Eq (B x)}}
          (p q : D A B) → Dec (p ≡ q)
    unquoteDef eqD = deriveEqDef eqD (quote D)

  module Test₂ where

    data D (A B : Set) (C : A → B → Set)  : B → Set where
      c : (x : A)(y : B)(z : C x y) → D A B C y

    eqD : {A B : Set} {C : A → B → Set} {{_ : Eq A}} {{_ : Eq B}} {{_ : ∀ {x y} → Eq (C x y)}} →
          ∀ {x} (p q : D A B C x) → Dec (p ≡ q)
    unquoteDef eqD = deriveEqDef eqD (quote D)

  module Test₃ where

    data Test : Set where
      test : {x : Nat} → Vec Nat x → Test

    instance EqTest : Eq Test
    EqTest = record { _==_ = eqTest }
      where
        eqTest : (p q : Test) → Dec (p ≡ q)
        unquoteDef eqTest = deriveEqDef eqTest (quote Test)

  module Test₄ where

    data Test : Nat → Set where
      test : (x : Nat) → Test x

    unquoteDecl EqTest = deriveEq EqTest (quote Test)

  module Test₅ where

    data Test (B : Nat → Set) : Set where
      test : B zero → Test B

    unquoteDecl EqTest = deriveEq EqTest (quote Test)

    prf : (x y : Test (Vec Nat)) → Dec (x ≡ y)
    prf x y = x == y

  module Test₆ where

    data Test (A : Set) (xs : List A) (x : A) : Set where
      test : x ∈ xs → Test A xs x

    unquoteDecl EqTest = deriveEq EqTest (quote Test)

  module Issue-#2 where

    data Test : Set where
      test : {x : Nat} → Vec Nat x → Test

    unquoteDecl EqTest = deriveEq EqTest (quote Test)

  module Issue-#3 where

    data Test : Nat → Set where
       test : (x : Nat) → Test x

    unquoteDecl EqTest = deriveEq EqTest (quote Test)

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.MaybeEmb {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation
import Tools.PropositionalEquality as PE

import Data.Nat as Nat

-- Any level can be embedded into the highest level.
maybeEmb : ∀ {l A r Γ}
         → Γ ⊩⟨ l ⟩ A ^ r
         → Γ ⊩⟨ ∞ ⟩ A ^ r
maybeEmb {ι ⁰} [A] = emb ∞< (emb emb< [A])
maybeEmb {ι ¹} [A] = emb ∞< [A]
maybeEmb {∞} [A] = [A]

-- Any level can be embedded into the highest level.
maybeEmbTerm : ∀ {l A t r Γ}
         → ([A] : Γ ⊩⟨ l ⟩ A ^ r)
         → Γ ⊩⟨ l ⟩ t ∷ A ^ r / [A]
         → Γ ⊩⟨ ∞ ⟩ t ∷ A ^ r / maybeEmb [A]
maybeEmbTerm {ι ⁰} [A] [t] = [t]
maybeEmbTerm {ι ¹} [A] [t] = [t]
maybeEmbTerm {∞} [A] [t] = [t]

-- The lowest level can be embedded in any level.
maybeEmb′ : ∀ {l l' A r Γ}
          → l ≤ l'
          → Γ ⊩⟨ ι l ⟩ A ^ r
          → Γ ⊩⟨ ι l' ⟩ A ^ r
maybeEmb′ (<is≤ 0<1) [A] = emb emb< [A]
maybeEmb′ (≡is≤ PE.refl) [A] = [A]

maybeEmb″ : ∀ {l A r Γ}
         → Γ ⊩⟨ ι ⁰ ⟩ A ^ r
         → Γ ⊩⟨ l ⟩ A ^ r
maybeEmb″ {ι ⁰} [A] = [A]
maybeEmb″ {ι ¹} [A] = emb emb< [A]
maybeEmb″ {∞} [A] = emb ∞< (emb emb< [A])

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-

Descriptor language for easily defining relational structures

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Relational.Macro where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure

open import Cubical.Structures.Relational.Constant
open import Cubical.Structures.Relational.Product
open import Cubical.Structures.Relational.Maybe
open import Cubical.Structures.Relational.Parameterized
open import Cubical.Structures.Relational.Pointed
open import Cubical.Structures.Relational.UnaryOp

open import Cubical.Structures.Macro

data RelDesc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} → hSet ℓ' → RelDesc ℓ
  -- pointed structure: X ↦ X
  var : RelDesc ℓ
  -- join of structures S,T : X ↦ (S X × T X)
  _,_ : RelDesc ℓ  → RelDesc ℓ  → RelDesc ℓ
  -- structure S parameterized by constant A : X ↦ (A → S X)
  param : ∀ {ℓ'} → (A : Type ℓ') → RelDesc ℓ  → RelDesc ℓ
  -- structure S parameterized by variable argument: X ↦ (X → S X)
  recvar : RelDesc ℓ  → RelDesc ℓ
  -- Maybe on a structure S: X ↦ Maybe (S X)
  maybe : RelDesc ℓ → RelDesc ℓ

infixr 4 _,_

{- Universe level calculations -}

relDesc→Desc : ∀ {ℓ} → RelDesc ℓ → Desc ℓ
relDesc→Desc (constant A) = constant (A .fst)
relDesc→Desc var = var
relDesc→Desc (d₀ , d₁) = relDesc→Desc d₀ , relDesc→Desc d₁
relDesc→Desc (param A d) = param A (relDesc→Desc d)
relDesc→Desc (recvar d) = recvar (relDesc→Desc d)
relDesc→Desc (maybe d) = maybe (relDesc→Desc d)

relMacroStrLevel : ∀ {ℓ} → RelDesc ℓ → Level
relMacroStrLevel d = macroStrLevel (relDesc→Desc d)

relMacroRelLevel : ∀ {ℓ} → RelDesc ℓ → Level
relMacroRelLevel d = macroEquivLevel (relDesc→Desc d)

RelMacroStructure : ∀ {ℓ} → (d : RelDesc ℓ) → Type ℓ → Type (relMacroStrLevel d)
RelMacroStructure d = MacroStructure (relDesc→Desc d)

preservesSetsRelMacro : ∀ {ℓ} → (d : RelDesc ℓ)
  {X : Type ℓ} → isSet X → isSet (RelMacroStructure d X)
preservesSetsRelMacro (constant A) = preservesSetsConstant A
preservesSetsRelMacro var = preservesSetsPointed
preservesSetsRelMacro (d₀ , d₁) =
  preservesSetsProduct (preservesSetsRelMacro d₀) (preservesSetsRelMacro d₁)
preservesSetsRelMacro (param A d) =
  preservesSetsParam A (λ _ → preservesSetsRelMacro d)
preservesSetsRelMacro (recvar d) =
  preservesSetsUnaryFun (preservesSetsRelMacro d)
preservesSetsRelMacro (maybe d) =
  preservesSetsMaybe (preservesSetsRelMacro d)

-- Notion of structured relation defined by a descriptor
RelMacroRelStr : ∀ {ℓ} → (d : RelDesc ℓ) → StrRel {ℓ} (RelMacroStructure d) (relMacroRelLevel d)
RelMacroRelStr (constant A) = ConstantRelStr A
RelMacroRelStr var = PointedRelStr
RelMacroRelStr (d₀ , d₁) = ProductRelStr (RelMacroRelStr d₀) (RelMacroRelStr d₁)
RelMacroRelStr (param A d) = ParamRelStr A (λ _ → RelMacroRelStr d)
RelMacroRelStr (recvar d) = UnaryFunRelStr (RelMacroRelStr d)
RelMacroRelStr (maybe d) = MaybeRelStr (RelMacroRelStr d)

-- Proof that structure induced by descriptor is suitable
relMacroSuitableRel : ∀ {ℓ} → (d : RelDesc ℓ) → SuitableStrRel _ (RelMacroRelStr d)
relMacroSuitableRel (constant A) = constantSuitableRel A
relMacroSuitableRel var = pointedSuitableRel
relMacroSuitableRel (d₀ , d₁) = productSuitableRel (relMacroSuitableRel d₀) (relMacroSuitableRel d₁)
relMacroSuitableRel (param A d) = paramSuitableRel A (λ _ → relMacroSuitableRel d)
relMacroSuitableRel (recvar d) = unaryFunSuitableRel (preservesSetsRelMacro d) (relMacroSuitableRel d)
relMacroSuitableRel (maybe d) = maybeSuitableRel (relMacroSuitableRel d)

-- Proof that structured relations and equivalences agree
relMacroMatchesEquiv : ∀ {ℓ} → (d : RelDesc ℓ)
  → StrRelMatchesEquiv (RelMacroRelStr d) (MacroEquivStr (relDesc→Desc d))
relMacroMatchesEquiv (constant A) = constantRelMatchesEquiv A
relMacroMatchesEquiv var = pointedRelMatchesEquiv
relMacroMatchesEquiv (d₁ , d₂) =
  productRelMatchesEquiv
    (RelMacroRelStr d₁) (RelMacroRelStr d₂)
    (relMacroMatchesEquiv d₁) (relMacroMatchesEquiv d₂)
relMacroMatchesEquiv (param A d) =
  paramRelMatchesEquiv A (λ _ → RelMacroRelStr d) (λ _ → relMacroMatchesEquiv d)
relMacroMatchesEquiv (recvar d) =
  unaryFunRelMatchesEquiv (RelMacroRelStr d) (relMacroMatchesEquiv d)
relMacroMatchesEquiv (maybe d) =
  maybeRelMatchesEquiv (RelMacroRelStr d) (relMacroMatchesEquiv d)

-- Module for easy importing
module RelMacro ℓ (d : RelDesc ℓ) where
  relation = RelMacroRelStr d
  suitable = relMacroSuitableRel d
  matches = relMacroMatchesEquiv d
  open Macro ℓ (relDesc→Desc d) public

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
infix 50 _∼_

postulate
  A : Set
  x : A
  _∼_ : A → A → Set

record T : Set where
  -- This fixity declaration should not be ignored.
  infix 60 _∘_
  _∘_ : A → A → A
  _∘_ _ _ = x
  field
    law : x ∘ x ∼ x

-- Some more examples

record R : Set₁ where
  infixl 6 _+_
  field
    _+_   : Set → Set → Set
    Times : Set → Set → Set
    Sigma : (A : Set) → (A → Set) → Set
    One   : Set

  infixl 7 _*_
  _*_ = _+_

  infixr 3 Σ
  syntax Σ A (λ a → B) = a ∈ A × B
  Σ = Sigma

  field
    three : One + One * One * One + One
    pair  : x ∈ One × One + One

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --prop --rewriting #-}

open import Examples.Sorting.Sequential.Comparable

module Examples.Sorting.Sequential.MergeSort.Merge (M : Comparable) where

open Comparable M
open import Examples.Sorting.Sequential.Core M

open import Calf costMonoid
open import Calf.Types.Bool
open import Calf.Types.Nat
open import Calf.Types.List
open import Calf.Types.Eq
open import Calf.Types.Bounded costMonoid

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
open import Function
open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s; _+_; _*_)
import Data.Nat.Properties as N

open import Examples.Sorting.Sequential.MergeSort.Split M

merge/clocked : cmp (Π nat λ _ → Π pair λ _ → F (list A))
merge/clocked zero    (l₁     , l₂    ) = ret (l₁ ++ l₂)
merge/clocked (suc k) ([]     , l₂    ) = ret l₂
merge/clocked (suc k) (x ∷ xs , []    ) = ret (x ∷ xs)
merge/clocked (suc k) (x ∷ xs , y ∷ ys) =
  bind (F (list A)) (x ≤ᵇ y) λ b →
    if b
      then (bind (F (list A)) (merge/clocked k (xs , y ∷ ys)) (ret ∘ (x ∷_)))
      else (bind (F (list A)) (merge/clocked k (x ∷ xs , ys)) (ret ∘ (y ∷_)))

merge/clocked/correct : ∀ k l₁ l₂ →
  ◯ (∃ λ l → merge/clocked k (l₁ , l₂) ≡ ret l × (length l₁ + length l₂ Nat.≤ k → Sorted l₁ → Sorted l₂ → SortedOf (l₁ ++ l₂) l))
merge/clocked/correct zero    l₁       l₂       u = l₁ ++ l₂ , refl , λ { h [] [] → refl , [] }
merge/clocked/correct (suc k) []       l₂       u = l₂ , refl , λ { h [] sorted₂ → refl , sorted₂ }
merge/clocked/correct (suc k) (x ∷ xs) []       u = x ∷ xs , refl , λ { h sorted₁ [] → ++-identityʳ (x ∷ xs) , sorted₁ }
merge/clocked/correct (suc k) (x ∷ xs) (y ∷ ys) u with h-cost x y
merge/clocked/correct (suc k) (x ∷ xs) (y ∷ ys) u | ⇓ b withCost q [ _ , h-eq ] rewrite eq/ref h-eq
  with ≤ᵇ-reflects-≤ u (Eq.trans (eq/ref h-eq) (step/ext (F bool) (ret b) q u))
merge/clocked/correct (suc k) (x ∷ xs) (y ∷ ys) u | ⇓ false withCost q [ _ , h-eq ] | ofⁿ ¬p =
  let (l , ≡ , h-sorted) = merge/clocked/correct k (x ∷ xs) ys u in
  y ∷ l , (
    let open ≡-Reasoning in
    begin
      step (F (list A)) q (bind (F (list A)) (merge/clocked k (x ∷ xs , ys)) (ret ∘ (y ∷_)))
    ≡⟨ step/ext (F (list A)) (bind (F (list A)) (merge/clocked k _) _) q u ⟩
      bind (F (list A)) (merge/clocked k (x ∷ xs , ys)) (ret ∘ (y ∷_))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) ≡ ⟩
      ret (y ∷ l)
    ∎
  ) , (
    λ { (s≤s h) (h₁ ∷ sorted₁) (h₂ ∷ sorted₂) →
      let h = Eq.subst (Nat._≤ k) (N.+-suc (length xs) (length ys)) h in
      let (↭ , sorted) = h-sorted h (h₁ ∷ sorted₁) sorted₂ in
      (
        let open PermutationReasoning in
        begin
          (x ∷ xs ++ y ∷ ys)
        ↭⟨ ++-comm-↭ (x ∷ xs) (y ∷ ys) ⟩
          (y ∷ ys ++ x ∷ xs)
        ≡⟨⟩
          y ∷ (ys ++ x ∷ xs)
        <⟨ ++-comm-↭ ys (x ∷ xs) ⟩
          y ∷ (x ∷ xs ++ ys)
        <⟨ ↭ ⟩
          y ∷ l
        ∎
      ) , (
        let p = ≰⇒≥ ¬p in
        All-resp-↭ (↭) (++⁺-All (p ∷ ≤-≤* p h₁) h₂) ∷ sorted
      )
    }
  )
merge/clocked/correct (suc k) (x ∷ xs) (y ∷ ys) u | ⇓ true withCost q [ _ , h-eq ] | ofʸ p =
  let (l , ≡ , h-sorted) = merge/clocked/correct k xs (y ∷ ys) u in
  x ∷ l , (
    let open ≡-Reasoning in
    begin
      step (F (list A)) q (bind (F (list A)) (merge/clocked k (xs , y ∷ ys)) (ret ∘ (x ∷_)))
    ≡⟨ step/ext (F (list A)) (bind (F (list A)) (merge/clocked k _) _) q u ⟩
      bind (F (list A)) (merge/clocked k (xs , y ∷ ys)) (ret ∘ (x ∷_))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) ≡ ⟩
      ret (x ∷ l)
    ∎
  ) , (
    λ { (s≤s h) (h₁ ∷ sorted₁) (h₂ ∷ sorted₂) →
      let (↭ , sorted) = h-sorted h sorted₁ (h₂ ∷ sorted₂)  in
      prep x ↭ , All-resp-↭ (↭) (++⁺-All h₁ (p ∷ ≤-≤* p h₂)) ∷ sorted
    }
  )

merge/clocked/cost : cmp (Π nat λ _ → Π pair λ _ → cost)
merge/clocked/cost zero    (l₁     , l₂    ) = zero
merge/clocked/cost (suc k) ([]     , l₂    ) = zero
merge/clocked/cost (suc k) (x ∷ xs , []    ) = zero
merge/clocked/cost (suc k) (x ∷ xs , y ∷ ys) =
  bind cost (x ≤ᵇ y) λ b →
    1 + (
      if b
        then (bind cost (merge/clocked k (xs , y ∷ ys)) (λ l → merge/clocked/cost k (xs , y ∷ ys) + 0))
        else (bind cost (merge/clocked k (x ∷ xs , ys)) (λ l → merge/clocked/cost k (x ∷ xs , ys) + 0))
    )

merge/clocked/cost/closed : cmp (Π nat λ _ → Π pair λ _ → cost)
merge/clocked/cost/closed k _ = k

merge/clocked/cost≤merge/clocked/cost/closed : ∀ k p → ◯ (merge/clocked/cost k p Nat.≤ merge/clocked/cost/closed k p)
merge/clocked/cost≤merge/clocked/cost/closed zero    (l₁     , l₂    ) u = N.≤-refl
merge/clocked/cost≤merge/clocked/cost/closed (suc k) ([]     , l₂    ) u = z≤n
merge/clocked/cost≤merge/clocked/cost/closed (suc k) (x ∷ xs , []    ) u = z≤n
merge/clocked/cost≤merge/clocked/cost/closed (suc k) (x ∷ xs , y ∷ ys) u with h-cost x y
... | ⇓ false withCost q [ _ , h-eq ] rewrite eq/ref h-eq =
  let (l , ≡ , _) = merge/clocked/correct k (x ∷ xs) ys u in
  begin
    step cost q (1 + bind cost (merge/clocked k (x ∷ xs , ys)) (λ l → merge/clocked/cost k (x ∷ xs , ys) + 0))
  ≡⟨ step/ext cost _ q u ⟩
    1 + bind cost (merge/clocked k (x ∷ xs , ys)) (λ l → merge/clocked/cost k (x ∷ xs , ys) + 0)
  ≡⟨⟩
    suc (bind cost (merge/clocked k (x ∷ xs , ys)) (λ l → merge/clocked/cost k (x ∷ xs , ys) + 0))
  ≡⟨ Eq.cong (λ e → suc (bind cost e λ l → merge/clocked/cost k (x ∷ xs , ys) + 0)) (≡) ⟩
    suc (merge/clocked/cost k (x ∷ xs , ys) + 0)
  ≡⟨ Eq.cong suc (N.+-identityʳ _) ⟩
    suc (merge/clocked/cost k (x ∷ xs , ys))
  ≤⟨ s≤s (merge/clocked/cost≤merge/clocked/cost/closed k (x ∷ xs , ys) u) ⟩
    suc (merge/clocked/cost/closed k (x ∷ xs , ys))
  ≡⟨⟩
    suc k
  ∎
    where open ≤-Reasoning
... | ⇓ true withCost q [ _ , h-eq ] rewrite eq/ref h-eq =
  let (l , ≡ , _) = merge/clocked/correct k xs (y ∷ ys) u in
  begin
    step cost q (1 + bind cost (merge/clocked k (xs , y ∷ ys)) (λ l → merge/clocked/cost k (xs , y ∷ ys) + 0))
  ≡⟨ step/ext cost _ q u ⟩
    1 + bind cost (merge/clocked k (xs , y ∷ ys)) (λ l → merge/clocked/cost k (xs , y ∷ ys) + 0)
  ≡⟨⟩
    suc (bind cost (merge/clocked k (xs , y ∷ ys)) (λ l → merge/clocked/cost k (xs , y ∷ ys) + 0))
  ≡⟨ Eq.cong (λ e → suc (bind cost e λ l → merge/clocked/cost k (xs , y ∷ ys) + 0)) (≡) ⟩
    suc (merge/clocked/cost k (xs , y ∷ ys) + 0)
  ≡⟨ Eq.cong suc (N.+-identityʳ _) ⟩
    suc (merge/clocked/cost k (xs , y ∷ ys))
  ≤⟨ s≤s (merge/clocked/cost≤merge/clocked/cost/closed k (xs , y ∷ ys) u) ⟩
    suc (merge/clocked/cost/closed k (xs , y ∷ ys))
  ≡⟨⟩
    suc k
  ∎
    where open ≤-Reasoning

merge/clocked≤merge/clocked/cost : ∀ k p → IsBounded (list A) (merge/clocked k p) (merge/clocked/cost k p)
merge/clocked≤merge/clocked/cost zero    (l₁     , l₂    ) = bound/ret
merge/clocked≤merge/clocked/cost (suc k) ([]     , l₂    ) = bound/ret
merge/clocked≤merge/clocked/cost (suc k) (x ∷ xs , []    ) = bound/ret
merge/clocked≤merge/clocked/cost (suc k) (x ∷ xs , y ∷ ys) =
  bound/bind 1 _ (h-cost x y) λ b →
    bound/bool {p = λ b → if_then_else_ b _ _} b
      (bound/bind (merge/clocked/cost k (x ∷ xs , ys)) _ (merge/clocked≤merge/clocked/cost k (x ∷ xs , ys)) λ l → bound/ret)
      (bound/bind (merge/clocked/cost k (xs , y ∷ ys)) _ (merge/clocked≤merge/clocked/cost k (xs , y ∷ ys)) λ l → bound/ret)

merge/clocked≤merge/clocked/cost/closed : ∀ k p → IsBounded (list A) (merge/clocked k p) (merge/clocked/cost/closed k p)
merge/clocked≤merge/clocked/cost/closed k p = bound/relax (merge/clocked/cost≤merge/clocked/cost/closed k p) (merge/clocked≤merge/clocked/cost k p)

merge : cmp (Π pair λ _ → F (list A))
merge (l₁ , l₂) = merge/clocked (length l₁ + length l₂) (l₁ , l₂)

merge/correct : ∀ l₁ l₂ →
  ◯ (∃ λ l → merge (l₁ , l₂) ≡ ret l × (Sorted l₁ → Sorted l₂ → SortedOf (l₁ ++ l₂) l))
merge/correct l₁ l₂ u =
  let (l , ≡ , h-sorted) = merge/clocked/correct (length l₁ + length l₂) l₁ l₂ u in
  l , ≡ , h-sorted N.≤-refl

merge/cost : cmp (Π pair λ _ → cost)
merge/cost (l₁ , l₂) = merge/clocked/cost (length l₁ + length l₂) (l₁ , l₂)

merge/cost/closed : cmp (Π pair λ _ → cost)
merge/cost/closed (l₁ , l₂) = merge/clocked/cost/closed (length l₁ + length l₂) (l₁ , l₂)

merge≤merge/cost : ∀ p → IsBounded (list A) (merge p) (merge/cost p)
merge≤merge/cost (l₁ , l₂) = merge/clocked≤merge/clocked/cost (length l₁ + length l₂) (l₁ , l₂)

merge≤merge/cost/closed : ∀ p → IsBounded (list A) (merge p) (merge/cost/closed p)
merge≤merge/cost/closed (l₁ , l₂) = merge/clocked≤merge/clocked/cost/closed (length l₁ + length l₂) (l₁ , l₂)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
-- Andreas, 2014-10-18 AIM XX

module EvalInTopLevel where

data Bool : Set where true false : Bool

not : Bool → Bool
not true = false
not false = true

-- Evaluate @not false@ in top level.


text:
{-# OPTIONS --without-K #-}
module PathStructure.UnitNoEta where

open import Equivalence
open import Types

split-path : {x y : Unit} → x ≡ y → Unit
split-path _ = tt

merge-path : {x y : Unit} → Unit → x ≡ y
merge-path _ = 1-elim
  (λ x → ∀ y → x ≡ y)
  (1-elim (λ y → tt ≡ y) refl) _ _

split-merge-eq : {x y : Unit} → (x ≡ y) ≃ Unit
split-merge-eq
  = split-path
  , (merge-path , 1-elim (λ x → tt ≡ x) refl)
  , (merge-path , J
      (λ _ _ p → merge-path (split-path p) ≡ p)
      (1-elim
        (λ x → merge-path {x} {x} (split-path {x} {x} refl) ≡ refl)
        refl)
      _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

open import HoTT
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLane1
open import homotopy.EilenbergMacLaneFunctor
open import homotopy.EM1HSpaceAssoc
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.FunCategory
open import lib.two-semi-categories.FundamentalCategory

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

private
  module G = AbGroup G
  module H = AbGroup H
  module G⊗H = TensorProduct G H
  open G⊗H using (_⊗_)
  open EMExplicit

⊙×-cp₀₀' : G.⊙El ⊙× H.⊙El ⊙→ G⊗H.⊙El
⊙×-cp₀₀' = uncurry G⊗H._⊗_ , G⊗H.⊗-unit-l H.ident

⊙×-cp₀₀-seq : (⊙EM G 0 ⊙× ⊙EM H 0) ⊙–→ ⊙EM G⊗H.abgroup 0
⊙×-cp₀₀-seq =
  ⊙–> (⊙emloop-equiv G⊗H.grp) ◃⊙∘
  ⊙×-cp₀₀' ◃⊙∘
  ⊙×-fmap (⊙<– (⊙emloop-equiv G.grp)) (⊙<– (⊙emloop-equiv H.grp)) ◃⊙idf

⊙×-cp₀₀ : ⊙EM G 0 ⊙× ⊙EM H 0 ⊙→ ⊙EM G⊗H.abgroup 0
⊙×-cp₀₀ = ⊙compose ⊙×-cp₀₀-seq

×-cp₀₀ : EM G 0 × EM H 0 → EM G⊗H.abgroup 0
×-cp₀₀ = fst ⊙×-cp₀₀

open EM₁HSpaceAssoc G⊗H.abgroup hiding (comp-functor) renaming (mult to EM₁-mult) public

cp₀₁ : G.El → EM₁ H.grp → EM₁ G⊗H.grp
cp₀₁ g = EM₁-fmap (G⊗H.ins-r-hom g)

abstract
  cp₀₁-emloop-β : ∀ g h → ap (cp₀₁ g) (emloop h) == emloop (g ⊗ h)
  cp₀₁-emloop-β g = EM₁-fmap-emloop-β (G⊗H.ins-r-hom g)

cp₀₁-distr-l : (g₁ g₂ : G.El) (y : EM₁ H.grp)
  → cp₀₁ (G.comp g₁ g₂) y == EM₁-mult (cp₀₁ g₁ y) (cp₀₁ g₂ y)
cp₀₁-distr-l g₁ g₂ =
  EM₁-set-elim
    {P = λ x → f x == g x}
    {{λ x → has-level-apply (EM₁-level₁ G⊗H.grp) _ _}}
    idp loop'
  where
  f : EM₁ H.grp → EM₁ G⊗H.grp
  f x = cp₀₁ (G.comp g₁ g₂) x
  g : EM₁ H.grp → EM₁ G⊗H.grp
  g x = EM₁-mult (cp₀₁ g₁ x) (cp₀₁ g₂ x)
  abstract
    loop' : (h : H.El) → idp == idp [ (λ x → f x == g x) ↓ emloop h ]
    loop' h = ↓-='-in {f = f} {g = g} {p = emloop h} {u = idp} {v = idp} $
      idp ∙' ap g (emloop h)
        =⟨ ∙'-unit-l (ap g (emloop h)) ⟩
      ap g (emloop h)
        =⟨ ! (ap2-diag (λ x y → EM₁-mult (cp₀₁ g₁ x) (cp₀₁ g₂ y)) (emloop h)) ⟩
      ap2 (λ x y → EM₁-mult (cp₀₁ g₁ x) (cp₀₁ g₂ y)) (emloop h) (emloop h)
        =⟨ =ₛ-out $ ap2-out (λ x y → EM₁-mult (cp₀₁ g₁ x) (cp₀₁ g₂ y)) (emloop h) (emloop h) ⟩
      ap (λ x → EM₁-mult (cp₀₁ g₁ x) embase) (emloop h) ∙ ap (cp₀₁ g₂) (emloop h)
        =⟨ ap2 _∙_ part (cp₀₁-emloop-β g₂ h) ⟩
      emloop (g₁ ⊗ h) ∙ emloop (g₂ ⊗ h)
        =⟨ ! (emloop-comp (g₁ ⊗ h) (g₂ ⊗ h)) ⟩
      emloop (G⊗H.comp (g₁ ⊗ h) (g₂ ⊗ h))
        =⟨ ap emloop (! (G⊗H.⊗-lin-l g₁ g₂ h)) ⟩
      emloop (G.comp g₁ g₂ ⊗ h)
        =⟨ ! (cp₀₁-emloop-β (G.comp g₁ g₂) h) ⟩
      ap f (emloop h)
        =⟨ ! (∙-unit-r (ap f (emloop h))) ⟩
      ap f (emloop h) ∙ idp =∎
      where
      part : ap (λ x → EM₁-mult (cp₀₁ g₁ x) embase) (emloop h) == emloop (g₁ ⊗ h)
      part =
        ap (λ x → EM₁-mult (cp₀₁ g₁ x) embase) (emloop h)
          =⟨ ap-∘ (λ u → EM₁-mult u embase) (cp₀₁ g₁) (emloop h) ⟩
        ap (λ u → EM₁-mult u embase) (ap (cp₀₁ g₁) (emloop h))
          =⟨ ap (ap (λ u → EM₁-mult u embase)) (cp₀₁-emloop-β g₁ h) ⟩
        ap (λ u → EM₁-mult u embase) (emloop (g₁ ⊗ h))
          =⟨ mult-emloop-β (g₁ ⊗ h) embase ⟩
        emloop (g₁ ⊗ h) =∎

module _ (g₁ g₂ g₃ : G.El) (y : EM₁ H.grp) where

  cp₀₁-distr-l₁ : cp₀₁ (G.comp (G.comp g₁ g₂) g₃) y =-=
                  EM₁-mult (cp₀₁ g₁ y) (EM₁-mult (cp₀₁ g₂ y) (cp₀₁ g₃ y))
  cp₀₁-distr-l₁ =
    cp₀₁ (G.comp (G.comp g₁ g₂) g₃) y
      =⟪ cp₀₁-distr-l (G.comp g₁ g₂) g₃ y ⟫
    EM₁-mult (cp₀₁ (G.comp g₁ g₂) y) (cp₀₁ g₃ y)
      =⟪ ap (λ s → EM₁-mult s (cp₀₁ g₃ y)) (cp₀₁-distr-l g₁ g₂ y) ⟫
    EM₁-mult (EM₁-mult (cp₀₁ g₁ y) (cp₀₁ g₂ y)) (cp₀₁ g₃ y)
      =⟪ H-⊙EM₁-assoc (cp₀₁ g₁ y) (cp₀₁ g₂ y) (cp₀₁ g₃ y) ⟫
    EM₁-mult (cp₀₁ g₁ y) (EM₁-mult (cp₀₁ g₂ y) (cp₀₁ g₃ y)) ∎∎

  cp₀₁-distr-l₂ : cp₀₁ (G.comp (G.comp g₁ g₂) g₃) y =-=
                  EM₁-mult (cp₀₁ g₁ y) (EM₁-mult (cp₀₁ g₂ y) (cp₀₁ g₃ y))
  cp₀₁-distr-l₂ =
    cp₀₁ (G.comp (G.comp g₁ g₂) g₃) y
      =⟪ ap (λ s → cp₀₁ s y) (G.assoc g₁ g₂ g₃) ⟫
    cp₀₁ (G.comp g₁ (G.comp g₂ g₃)) y
      =⟪ cp₀₁-distr-l g₁ (G.comp g₂ g₃) y ⟫
    EM₁-mult (cp₀₁ g₁ y) (cp₀₁ (G.comp g₂ g₃) y)
      =⟪ ap (EM₁-mult (cp₀₁ g₁ y)) (cp₀₁-distr-l g₂ g₃ y) ⟫
    EM₁-mult (cp₀₁ g₁ y) (EM₁-mult (cp₀₁ g₂ y) (cp₀₁ g₃ y)) ∎∎

abstract
  cp₀₁-distr-l-coh : (g₁ g₂ g₃ : G.El) (y : EM₁ H.grp)
    → cp₀₁-distr-l₁ g₁ g₂ g₃ y =ₛ cp₀₁-distr-l₂ g₁ g₂ g₃ y
  cp₀₁-distr-l-coh g₁ g₂ g₃ =
    EM₁-prop-elim
      {P = λ y → cp₀₁-distr-l₁ g₁ g₂ g₃ y =ₛ cp₀₁-distr-l₂ g₁ g₂ g₃ y}
      {{λ y → =ₛ-level (EM₁-level₁ G⊗H.grp)}} $
    idp ◃∙ idp ◃∙ idp ◃∎
      =ₛ₁⟨ 0 & 1 & ! (ap-cst embase (G.assoc g₁ g₂ g₃)) ⟩
    ap (cst embase) (G.assoc g₁ g₂ g₃) ◃∙ idp ◃∙ idp ◃∎ ∎ₛ

cp₀₁-functor :
  TwoSemiFunctor
    (group-to-cat G.grp)
    (fun-cat (EM₁ H.grp) EM₁-2-semi-category)
cp₀₁-functor =
  record
  { F₀ = λ _ _ → unit
  ; F₁ = λ g x → cp₀₁ g x
  ; pres-comp = λ g₁ g₂ → λ= (cp₀₁-distr-l g₁ g₂)
  ; pres-comp-coh = λ g₁ g₂ g₃ → pres-comp-coh g₁ g₂ g₃
    -- TODO: for some reason, this last field takes a really long time to check
    -- it is recommended to comment it out
  }
  where
  abstract
    pres-comp-coh : ∀ g₁ g₂ g₃ →
      λ= (cp₀₁-distr-l (G.comp g₁ g₂) g₃) ◃∙
      ap (λ s y → EM₁-mult (s y) (cp₀₁ g₃ y)) (λ= (cp₀₁-distr-l g₁ g₂)) ◃∙
      λ= (λ y → H-⊙EM₁-assoc (cp₀₁ g₁ y) (cp₀₁ g₂ y) (cp₀₁ g₃ y)) ◃∎
      =ₛ
      ap (λ s → cp₀₁ s) (G.assoc g₁ g₂ g₃) ◃∙
      λ= (cp₀₁-distr-l g₁ (G.comp g₂ g₃)) ◃∙
      ap (λ s y → EM₁-mult (cp₀₁ g₁ y) (s y)) (λ= (cp₀₁-distr-l g₂ g₃)) ◃∎
    pres-comp-coh g₁ g₂ g₃ =
      λ= (cp₀₁-distr-l (G.comp g₁ g₂) g₃) ◃∙
      ap (λ s y → EM₁-mult (s y) (cp₀₁ g₃ y)) (λ= (cp₀₁-distr-l g₁ g₂)) ◃∙
      λ= (λ y → H-⊙EM₁-assoc (cp₀₁ g₁ y) (cp₀₁ g₂ y) (cp₀₁ g₃ y)) ◃∎
        =ₛ₁⟨ 1 & 1 & λ=-ap (λ y s → EM₁-mult s (cp₀₁ g₃ y)) (cp₀₁-distr-l g₁ g₂) ⟩
      λ= (cp₀₁-distr-l (G.comp g₁ g₂) g₃) ◃∙
      λ= (λ y → ap (λ s → EM₁-mult s (cp₀₁ g₃ y)) (cp₀₁-distr-l g₁ g₂ y)) ◃∙
      λ= (λ y → H-⊙EM₁-assoc (cp₀₁ g₁ y) (cp₀₁ g₂ y) (cp₀₁ g₃ y)) ◃∎
        =ₛ⟨ ∙∙-λ= (cp₀₁-distr-l (G.comp g₁ g₂) g₃)
                  (λ y → ap (λ s → EM₁-mult s (cp₀₁ g₃ y)) (cp₀₁-distr-l g₁ g₂ y))
                  (λ y → H-⊙EM₁-assoc (cp₀₁ g₁ y) (cp₀₁ g₂ y) (cp₀₁ g₃ y)) ⟩
      λ= (λ y → ↯ (cp₀₁-distr-l₁ g₁ g₂ g₃ y)) ◃∎
        =ₛ₁⟨ ap λ= (λ= (λ y → =ₛ-out (cp₀₁-distr-l-coh g₁ g₂ g₃ y))) ⟩
      λ= (λ y → ↯ (cp₀₁-distr-l₂ g₁ g₂ g₃ y)) ◃∎
        =ₛ⟨ λ=-∙∙ (λ y → ap (λ s → cp₀₁ s y) (G.assoc g₁ g₂ g₃))
                  (cp₀₁-distr-l g₁ (G.comp g₂ g₃))
                  (λ y → ap (EM₁-mult (cp₀₁ g₁ y)) (cp₀₁-distr-l g₂ g₃ y)) ⟩
      λ= (λ y → ap (λ s → cp₀₁ s y) (G.assoc g₁ g₂ g₃)) ◃∙
      λ= (cp₀₁-distr-l g₁ (G.comp g₂ g₃)) ◃∙
      λ= (λ y → ap (EM₁-mult (cp₀₁ g₁ y)) (cp₀₁-distr-l g₂ g₃ y)) ◃∎
        =ₛ₁⟨ 0 & 1 & ap λ= (λ= (λ y → ap-∘ (λ f → f y) cp₀₁ (G.assoc g₁ g₂ g₃))) ⟩
      λ= (app= (ap (λ s → cp₀₁ s) (G.assoc g₁ g₂ g₃))) ◃∙
      λ= (cp₀₁-distr-l g₁ (G.comp g₂ g₃)) ◃∙
      λ= (λ y → ap (EM₁-mult (cp₀₁ g₁ y)) (cp₀₁-distr-l g₂ g₃ y)) ◃∎
        =ₛ₁⟨ 0 & 1 & ! (λ=-η (ap (λ s → cp₀₁ s) (G.assoc g₁ g₂ g₃))) ⟩
      ap (λ s → cp₀₁ s) (G.assoc g₁ g₂ g₃) ◃∙
      λ= (cp₀₁-distr-l g₁ (G.comp g₂ g₃)) ◃∙
      λ= (λ y → ap (EM₁-mult (cp₀₁ g₁ y)) (cp₀₁-distr-l g₂ g₃ y)) ◃∎
        =ₛ₁⟨ 2 & 1 & ! (λ=-ap (λ y s → EM₁-mult (cp₀₁ g₁ y) s) (cp₀₁-distr-l g₂ g₃)) ⟩
      ap (λ s → cp₀₁ s) (G.assoc g₁ g₂ g₃) ◃∙
      λ= (cp₀₁-distr-l g₁ (G.comp g₂ g₃)) ◃∙
      ap (λ s y → EM₁-mult (cp₀₁ g₁ y) (s y)) (λ= (cp₀₁-distr-l g₂ g₃)) ◃∎ ∎ₛ

comp-functor :
  TwoSemiFunctor
    EM₁-2-semi-category
    (=ₜ-fundamental-cat (Susp (EM₁ G⊗H.grp)))
comp-functor =
  record
  { F₀ = λ _ → [ north ]
  ; F₁ = λ x → [ η x ]
  ; pres-comp = comp
  ; pres-comp-coh = comp-coh
  }
  -- this is *exactly* the same as
  --   `EM₁HSpaceAssoc.comp-functor G⊗H.abgroup`
  -- inlined but Agda chokes on this shorter definition

module _ where

  private
    T : TwoSemiCategory (lmax i j) (lmax i j)
    T = fun-cat (EM₁ H.grp) (=ₜ-fundamental-cat (Susp (EM₁ G⊗H.grp)))

    module T = TwoSemiCategory T
    cst-north : T.El
    cst-north = λ _ → [ north ]
    T-comp' = T.comp {x = cst-north} {y = cst-north} {z = cst-north}
    T-assoc' = T.assoc {x = cst-north} {y = cst-north} {z = cst-north} {w = cst-north}

  group-to-EM₁→EM₂ : TwoSemiFunctor (group-to-cat G.grp) T
  group-to-EM₁→EM₂ =
    cp₀₁-functor –F→
    fun-functor-map (EM₁ H.grp) comp-functor

  abstract
    app=-group-to-EM₁→EM₂-pres-comp-embase : ∀ g₁ g₂ →
      app= (TwoSemiFunctor.pres-comp group-to-EM₁→EM₂ g₁ g₂) embase ==
      comp embase embase
    app=-group-to-EM₁→EM₂-pres-comp-embase g₁ g₂ = =ₛ-out $
      app= (TwoSemiFunctor.pres-comp group-to-EM₁→EM₂ g₁ g₂) embase ◃∎
        =ₛ⟨ ap-seq-=ₛ (λ f → f embase) (comp-functors-pres-comp-β cp₀₁-functor G₁₂ g₁ g₂) ⟩
      app= (ap (TwoSemiFunctor.F₁ G₁₂) (TwoSemiFunctor.pres-comp cp₀₁-functor g₁ g₂)) embase ◃∙
      app= (TwoSemiFunctor.pres-comp G₁₂ (cp₀₁ g₁) (cp₀₁ g₂)) embase ◃∎
        =ₛ⟨ 0 & 1 & =ₛ-in {t = []} $
            app= (ap (λ f x → [ η (f x) ]) (λ= (cp₀₁-distr-l g₁ g₂))) embase
              =⟨ ap (λ w → app= w embase) (λ=-ap (λ _ y → [ η y ]) (cp₀₁-distr-l g₁ g₂)) ⟩
            app= (λ= (λ a → ap (λ y → [ η y ]) (cp₀₁-distr-l g₁ g₂ a))) embase
              =⟨ app=-β (λ a → ap (λ y → [ η y ]) (cp₀₁-distr-l g₁ g₂ a)) embase ⟩
            idp =∎
          ⟩
      app= (TwoSemiFunctor.pres-comp G₁₂ (cp₀₁ g₁) (cp₀₁ g₂)) embase ◃∎
        =ₛ₁⟨ app=-β (λ y → comp (cp₀₁ g₁ y) (cp₀₁ g₂ y)) embase ⟩
      comp embase embase ◃∎ ∎ₛ
      where
        G₁₂ = fun-functor-map (EM₁ H.grp) comp-functor

module CP₁₁ where

  private
    C : Type (lmax i j)
    C = EM₁ H.grp → EM G⊗H.abgroup 2

    C-level : has-level 2 C
    C-level = Π-level (λ _ → EM-level G⊗H.abgroup 2)

    D₀ : TwoSemiCategory lzero i
    D₀ = group-to-cat G.grp

    D₁' : TwoSemiCategory (lmax i j) (lmax i j)
    D₁' = =ₜ-fundamental-cat (Susp (EM₁ G⊗H.grp))

    D₁ : TwoSemiCategory (lmax i j) (lmax i j)
    D₁ = fun-cat (EM₁ H.grp) D₁'

    D₂' : TwoSemiCategory (lmax i j) (lmax i j)
    D₂' = 2-type-fundamental-cat (EM G⊗H.abgroup 2)

    D₂ : TwoSemiCategory (lmax i j) (lmax i j)
    D₂ = fun-cat (EM₁ H.grp) D₂'

    D₃ : TwoSemiCategory (lmax i j) (lmax i j)
    D₃ = 2-type-fundamental-cat (EM₁ H.grp → EM G⊗H.abgroup 2) {{C-level}}

    F₀₁ : TwoSemiFunctor D₀ D₁
    F₀₁ = group-to-EM₁→EM₂

    F₁₂' : TwoSemiFunctor D₁' D₂'
    F₁₂' = =ₜ-to-2-type-fundamental-cat (Susp (EM₁ G⊗H.grp))

    F₁₂ : TwoSemiFunctor D₁ D₂
    F₁₂ = fun-functor-map (EM₁ H.grp) F₁₂'

  F₀₂ : TwoSemiFunctor D₀ D₂
  F₀₂ = F₀₁ –F→ F₁₂

  module F₂₃-Funext = FunextFunctors (EM₁ H.grp) (EM G⊗H.abgroup 2) {{⟨⟩}}
  F₂₃ : TwoSemiFunctor D₂ D₃
  F₂₃ = F₂₃-Funext.λ=-functor

  module F₀₂ = TwoSemiFunctor F₀₂
  module F₂₃ = TwoSemiFunctor F₂₃

  private
    module F₀₃-Comp = FunctorComposition F₀₂ F₂₃
    F₀₃ : TwoSemiFunctor D₀ D₃
    F₀₃ = F₀₃-Comp.composition

    module F₀₁  = TwoSemiFunctor F₀₁
    module F₁₂  = TwoSemiFunctor F₁₂
    module F₁₂' = TwoSemiFunctor F₁₂'
    module F₀₃  = TwoSemiFunctor F₀₃

    module CP₁₁-Rec = EM₁Rec {G = G.grp} {C = C} {{C-level}} F₀₃

  abstract
    cp₁₁ : EM₁ G.grp → EM₁ H.grp → EM G⊗H.abgroup 2
    cp₁₁ = CP₁₁-Rec.f

    cp₁₁-embase-β : cp₁₁ embase ↦ (λ _ → [ north ])
    cp₁₁-embase-β = CP₁₁-Rec.embase-β
    {-# REWRITE cp₁₁-embase-β #-}

    cp₁₁-emloop-β : ∀ g → ap cp₁₁ (emloop g) == λ= (λ y → ap [_] (η (cp₀₁ g y)))
    cp₁₁-emloop-β g = CP₁₁-Rec.emloop-β g

    app=-F₀₂-pres-comp-embase-β : ∀ g₁ g₂ →
      app= (F₀₂.pres-comp g₁ g₂) embase ◃∎
      =ₛ
      ap (ap [_]) (comp-l embase) ◃∙
      ap-∙ [_] (η embase) (η embase) ◃∎
    app=-F₀₂-pres-comp-embase-β g₁ g₂ =
      app= (F₀₂.pres-comp g₁ g₂) embase ◃∎
        =ₛ⟨ ap-seq-=ₛ (λ f → f embase) (comp-functors-pres-comp-β F₀₁ F₁₂ g₁ g₂) ⟩
      app= (ap (λ α y → <– (=ₜ-equiv [ north ] [ north ]) (α y))
               (F₀₁.pres-comp g₁ g₂)) embase ◃∙
      app= (F₁₂.pres-comp {x = λ _ → [ north ]} {y = λ _ → [ north ]} {z = λ _ → [ north ]}
                          (λ y → [ η (cp₀₁ g₁ y) ]₁) (λ y → [ η (cp₀₁ g₂ y) ]₁)) embase ◃∎
        =ₛ₁⟨ 0 & 1 & step₂ ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      app= (F₁₂.pres-comp {x = λ _ → [ north ]} {y = λ _ → [ north ]} {z = λ _ → [ north ]}
                          (λ y → [ η (cp₀₁ g₁ y) ]₁) (λ y → [ η (cp₀₁ g₂ y) ]₁)) embase ◃∎
        =ₛ₁⟨ 1 & 1 & step₃ ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      ap-∙ [_] (η embase) (η embase) ◃∎ ∎ₛ
      where
      step₂ :
        app= (ap (λ α y → <– (=ₜ-equiv [ north ] [ north ]) (α y))
             (F₀₁.pres-comp g₁ g₂)) embase
        == ap (ap [_]) (comp-l embase)
      step₂ =
        app= (ap (λ α y → <– (=ₜ-equiv [ north ] [ north ]) (α y)) (F₀₁.pres-comp g₁ g₂)) embase
          =⟨ ∘-ap (λ f → f embase)
                  (λ α y → <– (=ₜ-equiv [ north ] [ north ]) (α y))
                  (F₀₁.pres-comp g₁ g₂) ⟩
        ap (λ α → <– (=ₜ-equiv [ north ] [ north ]) (α embase))
           (F₀₁.pres-comp g₁ g₂)
          =⟨ ap-∘ (<– (=ₜ-equiv [ north ] [ north ]))
                  (λ f → f embase)
                  (F₀₁.pres-comp g₁ g₂) ⟩
        ap (<– (=ₜ-equiv [ north ] [ north ]))
           (app= (F₀₁.pres-comp g₁ g₂) embase)
          =⟨ ap (ap (<– (=ₜ-equiv [ north ] [ north ])))
                (app=-group-to-EM₁→EM₂-pres-comp-embase g₁ g₂) ⟩
        ap (<– (=ₜ-equiv [ north ] [ north ])) (comp embase embase)
          =⟨ ap (ap (<– (=ₜ-equiv [ north ] [ north ])))
                (comp-unit-l embase) ⟩
        ap (<– (=ₜ-equiv [ north ] [ north ]))
           (comp-l₁ embase)
          =⟨ ∘-ap (<– (=ₜ-equiv [ north ] [ north ])) [_]₁ (comp-l embase) ⟩
        ap (ap [_]) (comp-l embase) =∎
      step₃ :
        app= (F₁₂.pres-comp {x = λ _ → [ north ]₂} {y = λ _ → [ north ]₂} {z = λ _ → [ north ]₂}
                            (λ y → [ η (cp₀₁ g₁ y) ]₁) (λ y → [ η (cp₀₁ g₂ y) ]₁)) embase
        == ap-∙ [_] (η embase) (η embase)
      step₃ =
        app= (F₁₂.pres-comp {x = λ _ → [ north ]} {y = λ _ → [ north ]} {z = λ _ → [ north ]}
                            (λ y → [ η (cp₀₁ g₁ y) ]₁) (λ y → [ η (cp₀₁ g₂ y) ]₁)) embase
           =⟨ app=-β (λ y → F₁₂'.pres-comp {x = [ north ]} {y = [ north ]} {z = [ north ]}
                                           [ η (cp₀₁ g₁ y) ]₁ [ η (cp₀₁ g₂ y) ]₁) embase ⟩
        F₁₂'.pres-comp {x = [ north ]} {y = [ north ]} {z = [ north ]} [ η embase ]₁ [ η embase ]₁
          =⟨ =ₜ-to-2-type-fundamental-cat-pres-comp-β (Susp (EM₁ G⊗H.grp)) (η embase) (η embase) ⟩
        ap-∙ [_] (η embase) (η embase) =∎

    app=-F₀₂-pres-comp-embase-coh : ∀ g₁ g₂ →
      app= (F₀₂.pres-comp g₁ g₂) embase ◃∙
      ap2 _∙_ (ap (ap [_]) (!-inv-r (merid embase)))
              (ap (ap [_]) (!-inv-r (merid embase))) ◃∎
      =ₛ
      ap (ap [_]) (!-inv-r (merid embase)) ◃∎
    app=-F₀₂-pres-comp-embase-coh g₁ g₂ =
      app= (F₀₂.pres-comp g₁ g₂) embase ◃∙
      ap2 _∙_ (ap (ap [_]) (!-inv-r (merid embase)))
              (ap (ap [_]) (!-inv-r (merid embase))) ◃∎
        =ₛ⟨ 0 & 1 & app=-F₀₂-pres-comp-embase-β g₁ g₂ ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      ap-∙ [_] (η embase) (η embase) ◃∙
      ap2 _∙_ (ap (ap [_]) (!-inv-r (merid embase)))
              (ap (ap [_]) (!-inv-r (merid embase))) ◃∎
        =ₛ₁⟨ 2 & 1 & ap2-ap-lr _∙_ (ap [_]) (ap [_]) (!-inv-r (merid embase)) (!-inv-r (merid embase)) ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      ap-∙ [_] (η embase) (η embase) ◃∙
      ap2 (λ s t → ap [_] s ∙ ap [_] t) (!-inv-r (merid embase)) (!-inv-r (merid embase)) ◃∎
        =ₛ⟨ 1 & 2 & !ₛ $
            homotopy-naturality2 (λ s t → ap [_] (s ∙ t))
                                 (λ s t → ap [_] s ∙ ap [_] t)
                                 (ap-∙ [_])
                                 (!-inv-r (merid embase))
                                 (!-inv-r (merid embase)) ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      ap2 (λ s t → ap [_] (s ∙ t)) (!-inv-r (merid embase)) (!-inv-r (merid embase)) ◃∙
      idp ◃∎
        =ₛ⟨ 2 & 1 & expand [] ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      ap2 (λ s t → ap [_] (s ∙ t)) (!-inv-r (merid embase)) (!-inv-r (merid embase)) ◃∎
        =ₛ₁⟨ 1 & 1 & ! (ap-ap2 (ap [_]) _∙_ (!-inv-r (merid embase)) (!-inv-r (merid embase))) ⟩
      ap (ap [_]) (comp-l embase) ◃∙
      ap (ap [_]) (ap2 _∙_ (!-inv-r (merid embase)) (!-inv-r (merid embase))) ◃∎
        =ₛ⟨ ap-seq-=ₛ (ap [_]) step₇' ⟩
      ap (ap [_]) (!-inv-r (merid embase)) ◃∎ ∎ₛ
      where
        helper : ∀ {i} {A : Type i} {a₀ a₁ : A} (p : a₀ == a₁)
          → add-path-inverse-l (p ∙ ! p) p ◃∙ ap2 _∙_ (!-inv-r p) (!-inv-r p) ◃∎
            =ₛ !-inv-r p ◃∎
        helper idp = =ₛ-in idp
        step₇' : comp-l embase ◃∙ ap2 _∙_ (!-inv-r (merid embase)) (!-inv-r (merid embase)) ◃∎
                =ₛ !-inv-r (merid embase) ◃∎
        step₇' = helper (merid embase)

    app=-ap-cp₁₁-seq : ∀ g y → app= (ap cp₁₁ (emloop g)) y =-= ap [_] (η (cp₀₁ g y))
    app=-ap-cp₁₁-seq g y =
      app= (ap cp₁₁ (emloop g)) y
        =⟪ ap (λ p → app= p y) (cp₁₁-emloop-β g) ⟫
      app= (λ= (λ x → ap [_] (η (cp₀₁ g x)))) y
        =⟪ app=-β (λ x → ap [_] (η (cp₀₁ g x))) y ⟫
      ap [_] (η (cp₀₁ g y)) ∎∎

    app=-ap-cp₁₁ : ∀ g y → app= (ap cp₁₁ (emloop g)) y == ap [_] (η (cp₀₁ g y))
    app=-ap-cp₁₁ g y = ↯ (app=-ap-cp₁₁-seq g y)

  app=-ap-cp₁₁-coh-seq₁ : ∀ g₁ g₂ y →
    app= (ap cp₁₁ (emloop (G.comp g₁ g₂))) y =-= ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y))
  app=-ap-cp₁₁-coh-seq₁ g₁ g₂ y =
    app= (ap cp₁₁ (emloop (G.comp g₁ g₂))) y
      =⟪ ap (λ u → app= (ap cp₁₁ u) y) (emloop-comp g₁ g₂) ⟫
    app= (ap cp₁₁ (emloop g₁ ∙ emloop g₂)) y
      =⟪ ap (λ u → app= u y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ⟫
    app= (ap cp₁₁ (emloop g₁) ∙ ap cp₁₁ (emloop g₂)) y
      =⟪ ap-∙ (λ f → f y) (ap cp₁₁ (emloop g₁)) (ap cp₁₁ (emloop g₂)) ⟫
    app= (ap cp₁₁ (emloop g₁)) y ∙ app= (ap cp₁₁ (emloop g₂)) y
      =⟪ ap2 _∙_ (app=-ap-cp₁₁ g₁ y) (app=-ap-cp₁₁ g₂ y) ⟫
    ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y)) ∎∎

  app=-ap-cp₁₁-coh-seq₂ : ∀ g₁ g₂ y →
    app= (ap cp₁₁ (emloop (G.comp g₁ g₂))) y =-= ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y))
  app=-ap-cp₁₁-coh-seq₂ g₁ g₂ y =
    app= (ap cp₁₁ (emloop (G.comp g₁ g₂))) y
      =⟪ app=-ap-cp₁₁ (G.comp g₁ g₂) y ⟫
    ap [_] (η (cp₀₁ (G.comp g₁ g₂) y))
      =⟪ app= (F₀₂.pres-comp g₁ g₂) y ⟫
    ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y)) ∎∎

  abstract
    app=-ap-cp₁₁-coh : ∀ g₁ g₂ y →
      app=-ap-cp₁₁-coh-seq₁ g₁ g₂ y =ₛ app=-ap-cp₁₁-coh-seq₂ g₁ g₂ y
    app=-ap-cp₁₁-coh g₁ g₂ y =
      ap (λ u → app= (ap cp₁₁ u) y) (emloop-comp g₁ g₂) ◃∙
      ap (λ u → app= u y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap-∙ (λ f → f y) (ap cp₁₁ (emloop g₁)) (ap cp₁₁ (emloop g₂)) ◃∙
      ap2 _∙_ (app=-ap-cp₁₁ g₁ y) (app=-ap-cp₁₁ g₂ y) ◃∎
        =ₛ⟨ 3 & 2 & ap2-seq-∙ _∙_ (app=-ap-cp₁₁-seq g₁ y) (app=-ap-cp₁₁-seq g₂ y) ⟩
      ap (λ u → app= (ap cp₁₁ u) y) (emloop-comp g₁ g₂) ◃∙
      ap (λ u → app= u y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap-∙ (λ f → f y) (ap cp₁₁ (emloop g₁)) (ap cp₁₁ (emloop g₂)) ◃∙
      ap2 _∙_ (ap (λ z → app= z y) (cp₁₁-emloop-β g₁)) (ap (λ z → app= z y) (cp₁₁-emloop-β g₂)) ◃∙
      ap2 _∙_ (app=-β (λ x → ap [_] (η (cp₀₁ g₁ x))) y) (app=-β (λ x → ap [_] (η (cp₀₁ g₂ x))) y) ◃∎
        =ₛ₁⟨ 3 & 1 & ap2-ap-lr _∙_ (λ z → app= z y) (λ z → app= z y) (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂) ⟩
      ap (λ u → app= (ap cp₁₁ u) y) (emloop-comp g₁ g₂) ◃∙
      ap (λ u → app= u y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap-∙ (λ f → f y) (ap cp₁₁ (emloop g₁)) (ap cp₁₁ (emloop g₂)) ◃∙
      ap2 (λ a b → app= a y ∙ app= b y) (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂) ◃∙
      ap2 _∙_ (app=-β (λ x → ap [_] (η (cp₀₁ g₁ x))) y) (app=-β (λ x → ap [_] (η (cp₀₁ g₂ x))) y) ◃∎
        =ₛ⟨ 2 & 2 & !ₛ $
            homotopy-naturality2 (λ a b → app= (a ∙ b) y)
                                 (λ a b → app= a y ∙ app= b y)
                                 (ap-∙ (λ f → f y))
                                 (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂) ⟩
      ap (λ u → app= (ap cp₁₁ u) y) (emloop-comp g₁ g₂) ◃∙
      ap (λ u → app= u y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap2 (λ a b → app= (a ∙ b) y) (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂) ◃∙
      ap-∙ (λ f → f y) (λ= (λ y' → ap [_] (η (cp₀₁ g₁ y')))) (λ= (λ y' → ap [_] (η (cp₀₁ g₂ y')))) ◃∙
      ap2 _∙_ (app=-β (λ x → ap [_] (η (cp₀₁ g₁ x))) y) (app=-β (λ x → ap [_] (η (cp₀₁ g₂ x))) y) ◃∎
        =ₛ⟨ 3 & 2 &
            app=-β-coh (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))) y ⟩
      ap (λ x → app= (ap cp₁₁ x) y) (emloop-comp g₁ g₂) ◃∙
      ap (λ p → app= p y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap2 (λ a b → app= (a ∙ b) y) (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂) ◃∙
      ap (λ p → app= p y) (=ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))))) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ g₁ x)) ∙ ap [_] (η (cp₀₁ g₂ x))) y ◃∎
        =ₛ₁⟨ 0 & 1 & ap-∘ (λ p → app= p y) (ap cp₁₁) (emloop-comp g₁ g₂) ⟩
      ap (λ p → app= p y) (ap (ap cp₁₁) (emloop-comp g₁ g₂)) ◃∙
      ap (λ p → app= p y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap2 (λ a b → app= (a ∙ b) y) (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂) ◃∙
      ap (λ p → app= p y) (=ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))))) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ g₁ x)) ∙ ap [_] (η (cp₀₁ g₂ x))) y ◃∎
        =ₛ₁⟨ 2 & 1 & ! (ap-ap2 (λ p → app= p y) _∙_ (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂)) ⟩
      ap (λ p → app= p y) (ap (ap cp₁₁) (emloop-comp g₁ g₂)) ◃∙
      ap (λ p → app= p y) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap (λ p → app= p y) (ap2 _∙_ (cp₁₁-emloop-β g₁) (cp₁₁-emloop-β g₂)) ◃∙
      ap (λ p → app= p y) (=ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))))) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ g₁ x)) ∙ ap [_] (η (cp₀₁ g₂ x))) y ◃∎
        =ₛ⟨ 0 & 3 & ap-seq-=ₛ (λ p → app= p y) (CP₁₁-Rec.emloop-comp-path g₁ g₂) ⟩
      ap (λ p → app= p y) (cp₁₁-emloop-β (G.comp g₁ g₂)) ◃∙
      ap (λ p → app= p y) (F₀₃.pres-comp g₁ g₂) ◃∙
      ap (λ p → app= p y) (=ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))))) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ g₁ x)) ∙ ap [_] (η (cp₀₁ g₂ x))) y ◃∎
        =ₛ⟨ 1 & 2 & step₈ ⟩
      ap (λ p → app= p y) (cp₁₁-emloop-β (G.comp g₁ g₂)) ◃∙
      ap (λ p → app= p y) (ap λ= (F₀₂.pres-comp g₁ g₂)) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ g₁ x)) ∙ ap [_] (η (cp₀₁ g₂ x))) y ◃∎
        =ₛ₁⟨ 1 & 1 & ∘-ap (λ p → app= p y) λ= (F₀₂.pres-comp g₁ g₂) ⟩
      ap (λ p → app= p y) (cp₁₁-emloop-β (G.comp g₁ g₂)) ◃∙
      ap (λ γ → app= (λ= γ) y) (F₀₂.pres-comp g₁ g₂) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ g₁ x)) ∙ ap [_] (η (cp₀₁ g₂ x))) y ◃∎
        =ₛ⟨ 1 & 2 &
            homotopy-naturality (λ γ → app= (λ= γ) y)
                                (λ γ → γ y)
                                (λ γ → app=-β γ y)
                                (F₀₂.pres-comp g₁ g₂) ⟩
      ap (λ p → app= p y) (cp₁₁-emloop-β (G.comp g₁ g₂)) ◃∙
      app=-β (λ x → ap [_] (η (cp₀₁ (G.comp g₁ g₂) x))) y ◃∙
      app= (F₀₂.pres-comp g₁ g₂) y ◃∎
        =ₛ⟨ 0 & 2 & contract ⟩
      app=-ap-cp₁₁ (G.comp g₁ g₂) y ◃∙
      app= (F₀₂.pres-comp g₁ g₂) y ◃∎ ∎ₛ
      where
      step₈ :
        ap (λ p → app= p y) (F₀₃.pres-comp g₁ g₂) ◃∙
        ap (λ p → app= p y) (=ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))))) ◃∎
        =ₛ
        ap (λ p → app= p y) (ap λ= (F₀₂.pres-comp g₁ g₂)) ◃∎
      step₈ = ap-seq-=ₛ (λ p → app= p y) $
        F₀₃.pres-comp g₁ g₂ ◃∙
        =ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x)))) ◃∎
          =ₛ⟨ 0 & 1 & F₀₃-Comp.pres-comp-β g₁ g₂ ⟩
        ap λ= (F₀₂.pres-comp g₁ g₂) ◃∙
        F₂₃.pres-comp (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))) ◃∙
        =ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x)))) ◃∎
          =ₛ₁⟨ 1 & 1 & F₂₃-Funext.λ=-functor-pres-comp=λ=-∙ (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x))) ⟩
        ap λ= (F₀₂.pres-comp g₁ g₂) ◃∙
        =ₛ-out (λ=-∙ (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x)))) ◃∙
        =ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x)))) ◃∎
          =ₛ⟨ 1 & 2 & seq-!-inv-l (=ₛ-out (∙-λ= (λ x → ap [_] (η (cp₀₁ g₁ x))) (λ x → ap [_] (η (cp₀₁ g₂ x)))) ◃∎) ⟩
        ap λ= (F₀₂.pres-comp g₁ g₂) ◃∎ ∎ₛ

    ap-cp₁₁-seq : ∀ g y → ap (λ x → cp₁₁ x y) (emloop g) =-= ap [_] (η (cp₀₁ g y))
    ap-cp₁₁-seq g y =
      ap (λ x → cp₁₁ x y) (emloop g)
        =⟪ ap-∘ (λ f → f y) cp₁₁ (emloop g) ⟫
      ap (λ f → f y) (ap cp₁₁ (emloop g))
        =⟪ app=-ap-cp₁₁ g y ⟫
      ap [_] (η (cp₀₁ g y)) ∎∎

    ap-cp₁₁ : ∀ g y → ap (λ x → cp₁₁ x y) (emloop g) == ap [_] (η (cp₀₁ g y))
    ap-cp₁₁ g y = ↯ (ap-cp₁₁-seq g y)

  ap-cp₁₁-coh-seq₁ : ∀ g₁ g₂ y →
    ap (λ x → cp₁₁ x y) (emloop (G.comp g₁ g₂)) =-= ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y))
  ap-cp₁₁-coh-seq₁ g₁ g₂ y =
    ap (λ x → cp₁₁ x y) (emloop (G.comp g₁ g₂))
      =⟪ ap (ap (λ x → cp₁₁ x y)) (emloop-comp g₁ g₂) ⟫
    ap (λ x → cp₁₁ x y) (emloop g₁ ∙ emloop g₂)
      =⟪ ap-∙ (λ x → cp₁₁ x y) (emloop g₁) (emloop g₂) ⟫
    ap (λ x → cp₁₁ x y) (emloop g₁) ∙ ap (λ x → cp₁₁ x y) (emloop g₂)
      =⟪ ap2 _∙_ (ap-cp₁₁ g₁ y) (ap-cp₁₁ g₂ y) ⟫
    ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y)) ∎∎

  ap-cp₁₁-coh-seq₂ : ∀ g₁ g₂ y →
    ap (λ x → cp₁₁ x y) (emloop (G.comp g₁ g₂)) =-= ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y))
  ap-cp₁₁-coh-seq₂ g₁ g₂ y =
    ap (λ x → cp₁₁ x y) (emloop (G.comp g₁ g₂))
      =⟪ ap-cp₁₁ (G.comp g₁ g₂) y ⟫
    ap [_] (η (cp₀₁ (G.comp g₁ g₂) y))
      =⟪ app= (F₀₂.pres-comp g₁ g₂) y ⟫
    ap [_] (η (cp₀₁ g₁ y)) ∙ ap [_] (η (cp₀₁ g₂ y)) ∎∎

  abstract
    ap-cp₁₁-coh : ∀ g₁ g₂ y →
      ap-cp₁₁-coh-seq₁ g₁ g₂ y =ₛ ap-cp₁₁-coh-seq₂ g₁ g₂ y
    ap-cp₁₁-coh g₁ g₂ y =
      ap (ap (λ x → cp₁₁ x y)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (λ x → cp₁₁ x y) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (ap-cp₁₁ g₁ y) (ap-cp₁₁ g₂ y) ◃∎
        =ₛ⟨ 2 & 1 & ap2-seq-∙ _∙_ (ap-cp₁₁-seq g₁ y) (ap-cp₁₁-seq g₂ y) ⟩
      ap (ap (λ x → cp₁₁ x y)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (λ x → cp₁₁ x y) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (ap-∘ (λ f → f y) cp₁₁ (emloop g₁)) (ap-∘ (λ f → f y) cp₁₁ (emloop g₂)) ◃∙
      ap2 _∙_ (app=-ap-cp₁₁ g₁ y) (app=-ap-cp₁₁ g₂ y) ◃∎
        =ₛ⟨ 1 & 2 & ap-∘-∙-coh (λ f → f y) cp₁₁ (emloop g₁) (emloop g₂) ⟩
      ap (ap (λ x → cp₁₁ x y)) (emloop-comp g₁ g₂) ◃∙
      ap-∘ (λ f → f y) cp₁₁ (emloop g₁ ∙ emloop g₂) ◃∙
      ap (ap (λ f → f y)) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap-∙ (λ f → f y) (ap cp₁₁ (emloop g₁)) (ap cp₁₁ (emloop g₂)) ◃∙
      ap2 _∙_ (app=-ap-cp₁₁ g₁ y) (app=-ap-cp₁₁ g₂ y) ◃∎
        =ₛ⟨ 0 & 2 & homotopy-naturality {A = embase' G.grp == embase} {B = cp₁₁ embase y == cp₁₁ embase y}
                                        (ap (λ x → cp₁₁ x y)) (λ p → app= (ap cp₁₁ p) y)
                                        (ap-∘ (λ f → f y) cp₁₁) (emloop-comp g₁ g₂) ⟩
      ap-∘ (λ f → f y) cp₁₁ (emloop (G.comp g₁ g₂)) ◃∙
      ap (λ p → app= (ap cp₁₁ p) y) (emloop-comp g₁ g₂) ◃∙
      ap (ap (λ f → f y)) (ap-∙ cp₁₁ (emloop g₁) (emloop g₂)) ◃∙
      ap-∙ (λ f → f y) (ap cp₁₁ (emloop g₁)) (ap cp₁₁ (emloop g₂)) ◃∙
      ap2 _∙_ (app=-ap-cp₁₁ g₁ y) (app=-ap-cp₁₁ g₂ y) ◃∎
        =ₛ⟨ 1 & 4 & app=-ap-cp₁₁-coh g₁ g₂ y ⟩
      ap-∘ (λ f → f y) cp₁₁ (emloop (G.comp g₁ g₂)) ◃∙
      app=-ap-cp₁₁ (G.comp g₁ g₂) y ◃∙
      app= (F₀₂.pres-comp g₁ g₂) y ◃∎
        =ₛ₁⟨ 0 & 2 & idp ⟩
      ap-cp₁₁ (G.comp g₁ g₂) y ◃∙
      app= (F₀₂.pres-comp g₁ g₂) y ◃∎ ∎ₛ

  ap-cp₁₁-embase-seq : ∀ g →
    ap (λ x → cp₁₁ x embase) (emloop g) =-= idp
  ap-cp₁₁-embase-seq g =
    ap (λ x → cp₁₁ x embase) (emloop g)
      =⟪ ap-cp₁₁ g embase ⟫
    ap [_] (η (cp₀₁ g embase))
      =⟪idp⟫
    ap [_] (η embase)
      =⟪ ap (ap [_]) (!-inv-r (merid embase)) ⟫
    ap [_] (idp {a = north})
      =⟪idp⟫
    idp ∎∎

  ap-cp₁₁-embase : ∀ g →
    ap (λ x → cp₁₁ x embase) (emloop g) == idp
  ap-cp₁₁-embase g = ↯ (ap-cp₁₁-embase-seq g)

  ap-cp₁₁-embase-coh-seq : ∀ g₁ g₂ →
    ap (λ x → cp₁₁ x embase) (emloop (G.comp g₁ g₂)) =-= idp
  ap-cp₁₁-embase-coh-seq g₁ g₂ =
    ap (λ x → cp₁₁ x embase) (emloop (G.comp g₁ g₂))
      =⟪ ap (ap (λ x → cp₁₁ x embase)) (emloop-comp g₁ g₂) ⟫
    ap (λ x → cp₁₁ x embase) (emloop g₁ ∙ emloop g₂)
      =⟪ ap-∙ (λ x → cp₁₁ x embase) (emloop g₁) (emloop g₂) ⟫
    ap (λ x → cp₁₁ x embase) (emloop g₁) ∙ ap (λ x → cp₁₁ x embase) (emloop g₂)
      =⟪ ap2 _∙_ (ap-cp₁₁-embase g₁) (ap-cp₁₁-embase g₂) ⟫
    idp ∎∎

  ap-cp₁₁-embase-coh : ∀ g₁ g₂ →
    ap-cp₁₁-embase (G.comp g₁ g₂) ◃∎ =ₛ ap-cp₁₁-embase-coh-seq g₁ g₂
  ap-cp₁₁-embase-coh g₁ g₂ =
    ap-cp₁₁-embase (G.comp g₁ g₂) ◃∎
      =ₛ⟨ expand (ap-cp₁₁-embase-seq (G.comp g₁ g₂)) ⟩
    ap-cp₁₁ (G.comp g₁ g₂) embase ◃∙
    ap (ap [_]) (!-inv-r (merid embase)) ◃∎
      =ₛ⟨ 1 & 1 & !ₛ (app=-F₀₂-pres-comp-embase-coh g₁ g₂) ⟩
    ap-cp₁₁ (G.comp g₁ g₂) embase ◃∙
    app= (F₀₂.pres-comp g₁ g₂) embase ◃∙
    ap2 _∙_ (ap (ap [_]) (!-inv-r (merid embase))) (ap (ap [_]) (!-inv-r (merid embase))) ◃∎
      =ₛ⟨ 0 & 2 & !ₛ (ap-cp₁₁-coh g₁ g₂ embase) ⟩
    ap (ap (λ x → cp₁₁ x embase)) (emloop-comp g₁ g₂) ◃∙
    ap-∙ (λ x → cp₁₁ x embase) (emloop g₁) (emloop g₂) ◃∙
    ap2 _∙_ (ap-cp₁₁ g₁ embase) (ap-cp₁₁ g₂ embase) ◃∙
    ap2 _∙_ (ap (ap [_]) (!-inv-r (merid embase))) (ap (ap [_]) (!-inv-r (merid embase))) ◃∎
      =ₛ⟨ 2 & 2 & ∙-ap2-seq _∙_ (ap-cp₁₁-embase-seq g₁) (ap-cp₁₁-embase-seq g₂) ⟩
    ap (ap (λ x → cp₁₁ x embase)) (emloop-comp g₁ g₂) ◃∙
    ap-∙ (λ x → cp₁₁ x embase) (emloop g₁) (emloop g₂) ◃∙
    ap2 _∙_ (ap-cp₁₁-embase g₁) (ap-cp₁₁-embase g₂) ◃∎ ∎ₛ

open CP₁₁ public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- Strings
------------------------------------------------------------------------

module Data.String where

open import Data.List as List using (List)
open import Data.Vec as Vec using (Vec)
open import Data.Colist as Colist using (Colist)
open import Data.Char using (Char)
open import Data.Bool using (Bool; true; false)
open import Data.Function
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)

------------------------------------------------------------------------
-- Types

-- Finite strings.

postulate
  String : Set

{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

-- Possibly infinite strings.

Costring : Set
Costring = Colist Char

------------------------------------------------------------------------
-- Operations

private
 primitive
  primStringAppend   : String → String → String
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringEquality : String → String → Bool

infixr 5 _++_

_++_ : String → String → String
_++_ = primStringAppend

toList : String → List Char
toList = primStringToList

fromList : List Char → String
fromList = primStringFromList

toVec : (s : String) → Vec Char (List.length (toList s))
toVec s = Vec.fromList (toList s)

toCostring : String → Costring
toCostring = Colist.fromList ∘ toList

infix 4 _==_

_==_ : String → String → Bool
_==_ = primStringEquality

_≟_ : Decidable {String} _≡_
s₁ ≟ s₂ with s₁ == s₂
... | true  = yes trustMe
  where postulate trustMe : _
... | false = no trustMe
  where postulate trustMe : _

setoid : Setoid
setoid = PropEq.setoid String

decSetoid : DecSetoid
decSetoid = PropEq.decSetoid _≟_

max_issues_repo_name: larrytheliquid/Lemmachine


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

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

module LibraBFT.Base.Encode where

 -- An encoder for values of type A is
 -- an injective mapping of 'A's into 'ByteString's
 record Encoder {a}(A : Set a) : Set a where
   constructor mkEncoder
   field
     encode     : A → ByteString
     encode-inj : ∀{a₁ a₂} → encode a₁ ≡ encode a₂ → a₁ ≡ a₂
 open Encoder {{...}} public

 ≡-Encoder : ∀ {a} {A : Set a} → Encoder A → DecidableEquality A
 ≡-Encoder (mkEncoder enc enc-inj) x y
    with enc x ≟ByteString enc y
 ...| yes enc≡ = yes (enc-inj enc≡)
 ...| no  neq  = no  (⊥-elim ∘ neq ∘ cong enc)

 postulate  -- valid assumption
  instance
    encℕ   : Encoder ℕ
    encBS  : Encoder ByteString

 instance
   encFin : {n : ℕ} → Encoder (Fin n)
   encFin {n} = record { encode     = encode ⦃ encℕ ⦄ ∘ toℕ ;
                         encode-inj = toℕ-injective ∘ encode-inj ⦃ encℕ ⦄ }

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
data U : Set
T : U -> Set
record V u (t : T u) : Set -- note that u's Set is found by unification


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Functor.Compose where

open import Cubical.Foundations.Prelude

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

open import Cubical.Categories.Instances.Functors

module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
  {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'}
  (E : Precategory ℓE ℓE') ⦃ isCatE : isCategory E ⦄
  (F : Functor C D)
  where

  open Functor
  open NatTrans

  precomposeF : Functor (FUNCTOR D E) (FUNCTOR C E)
  precomposeF .F-ob G = funcComp G F
  precomposeF .F-hom α .N-ob c = α .N-ob (F .F-ob c)
  precomposeF .F-hom α .N-hom f = α .N-hom (F .F-hom f)
  precomposeF .F-id = refl
  precomposeF .F-seq f g = refl

module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
  (C : Precategory ℓC ℓC')
  {D : Precategory ℓD ℓD'} ⦃ isCatD : isCategory D ⦄
  {E : Precategory ℓE ℓE'} ⦃ isCatE : isCategory E ⦄
  (G : Functor D E)
  where

  open Functor
  open NatTrans

  postcomposeF : Functor (FUNCTOR C D) (FUNCTOR C E)
  postcomposeF .F-ob F = funcComp G F
  postcomposeF .F-hom α .N-ob c = G. F-hom (α .N-ob c)
  postcomposeF .F-hom {F₀} {F₁} α .N-hom {x} {y} f =
    sym (G .F-seq (F₀ ⟪ f ⟫) (α ⟦ y ⟧))
    ∙∙ cong (G ⟪_⟫) (α .N-hom f)
    ∙∙ G .F-seq (α ⟦ x ⟧) (F₁ ⟪ f ⟫)
  postcomposeF .F-id = makeNatTransPath (funExt λ _ → G .F-id)
  postcomposeF .F-seq f g = makeNatTransPath (funExt λ _ → G .F-seq _ _)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module NoSuchModule where

open X


text:
{-

Mapping cones or the homotopy cofiber/cokernel

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.HITs.MappingCones.Base where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' ℓ'' : Level

data Cone {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) : Type (ℓ-max ℓ ℓ') where
  inj   : Y → Cone f
  hub   : Cone f
  spoke : (x : X) → hub ≡ inj (f x)

-- the attachment of multiple mapping cones

data Cones {X : Type ℓ} {Y : Type ℓ'} (A : Type ℓ'') (f : A → X → Y) : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'') where
  inj   : Y → Cones A f
  hub   : A → Cones A f
  spoke : (a : A) (x : X) → hub a ≡ inj (f a x)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Util.Equality where

open import Relation.Binary.PropositionalEquality

app-≡ : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x} (x : A) → f ≡ g → f x ≡ g x
app-≡ x refl = refl

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


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

module Fragment.Setoid.Morphism.Properties where

open import Fragment.Setoid.Morphism.Base
open import Fragment.Setoid.Morphism.Setoid

open import Level using (Level)
open import Relation.Binary using (Setoid)

private
  variable
    a b c d ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
    A : Setoid a ℓ₁
    B : Setoid b ℓ₂
    C : Setoid c ℓ₃
    D : Setoid d ℓ₄

id-unitˡ : ∀ {f : A ↝ B} → id · f ≗ f
id-unitˡ {B = B} = Setoid.refl B

id-unitʳ : ∀ {f : A ↝ B} → f · id ≗ f
id-unitʳ {B = B} = Setoid.refl B

·-assoc : ∀ (h : C ↝ D) (g : B ↝ C) (f : A ↝ B)
          → (h · g) · f ≗ h · (g · f)
·-assoc {D = D} _ _ _ = Setoid.refl D

·-congˡ : ∀ (h : B ↝ C) (f g : A ↝ B)
          → f ≗ g
          → h · f ≗ h · g
·-congˡ h _ _ f≗g = ∣ h ∣-cong f≗g

·-congʳ : ∀ (h : A ↝ B) (f g : B ↝ C)
          → f ≗ g
          → f · h ≗ g · h
·-congʳ _ _ _ f≗g = f≗g

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Thesis.SIRelBigStep.OpSem where

open import Data.Nat
open import Thesis.SIRelBigStep.Syntax public

data Val : Type → Set

import Base.Denotation.Environment
open Base.Denotation.Environment Type Val public
open import Base.Data.DependentList public

data Val where
  closure : ∀ {Γ σ τ} → (t : Term (σ • Γ) τ) → (ρ : ⟦ Γ ⟧Context) → Val (σ ⇒ τ)
  natV : ∀ (n : ℕ) → Val nat
  pairV : ∀ {σ τ} → Val σ → Val τ → Val (pair σ τ)

eval-const : ∀ {τ} → Const τ → Val τ
eval-const (lit n) = natV n

eval : ∀ {Γ τ} (sv : SVal Γ τ) (ρ : ⟦ Γ ⟧Context) → Val τ
eval (var x) ρ = ⟦ x ⟧Var ρ
eval (abs t) ρ = closure t ρ
eval (cons sv1 sv2) ρ = pairV (eval sv1 ρ) (eval sv2 ρ)
eval (const c) ρ = eval-const c

eval-primitive : ∀ {σ τ} → Primitive (σ ⇒ τ) → Val σ → Val τ
eval-primitive succ (natV n) = natV (suc n)
eval-primitive add (pairV (natV n1) (natV n2)) = natV (n1 + n2)

-- Yann's idea.
data HasIdx : Set where
  true : HasIdx
  false : HasIdx
data Idx : HasIdx → Set where
  i' : ℕ → Idx true
  no : Idx false

i : {hasIdx : HasIdx} → ℕ → Idx hasIdx
i {false} j = no
i {true} j = i' j

module _ {hasIdx : HasIdx} where
  data _⊢_↓[_]_ {Γ} (ρ : ⟦ Γ ⟧Context) : ∀ {τ} → Term Γ τ → Idx hasIdx → Val τ → Set where
    val : ∀ {τ} (sv : SVal Γ τ) →
      ρ ⊢ val sv ↓[ i 0 ] eval sv ρ
    primapp : ∀ {σ τ} (p : Primitive (σ ⇒ τ)) (sv : SVal Γ σ) →
      ρ ⊢ primapp p sv ↓[ i 1 ] eval-primitive p (eval sv ρ)
    app : ∀ n {Γ′ σ τ ρ′} vtv {v} {vs : SVal Γ (σ ⇒ τ)} {vt : SVal Γ σ} {t : Term (σ • Γ′) τ} →
      ρ ⊢ val vs ↓[ i 0 ] closure t ρ′ →
      ρ ⊢ val vt ↓[ i 0 ] vtv →
      (vtv • ρ′) ⊢ t ↓[ i n ] v →
      ρ ⊢ app vs vt ↓[ i (suc n) ] v
    lett :
      ∀ n1 n2 {σ τ} vsv {v} (s : Term Γ σ) (t : Term (σ • Γ) τ) →
      ρ ⊢ s ↓[ i n1 ] vsv →
      (vsv • ρ) ⊢ t ↓[ i n2 ] v →
      ρ ⊢ lett s t ↓[ i (suc n1 + n2) ] v

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --safe #-}
module Extraction where
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
open import Relation.Nullary
open import PiPointedFrac as Pi/ hiding (𝕌; ⟦_⟧; eval)
open import PiFracDyn

Inj𝕌 : Pi/.𝕌 → 𝕌
Inj𝕌 𝟘 = 𝟘
Inj𝕌 𝟙 = 𝟙
Inj𝕌 (t₁ +ᵤ t₂) = Inj𝕌 t₁ +ᵤ Inj𝕌 t₂
Inj𝕌 (t₁ ×ᵤ t₂) = Inj𝕌 t₁ ×ᵤ Inj𝕌 t₂

Inj𝕌≡ : (t : Pi/.𝕌) → Pi/.⟦ t ⟧ ≡ ⟦ Inj𝕌 t ⟧
Inj𝕌≡ 𝟘 = refl
Inj𝕌≡ 𝟙 = refl
Inj𝕌≡ (t₁ +ᵤ t₂) rewrite (Inj𝕌≡ t₁) | (Inj𝕌≡ t₂) = refl
Inj𝕌≡ (t₁ ×ᵤ t₂) rewrite (Inj𝕌≡ t₁) | (Inj𝕌≡ t₂) = refl

Inj⟦𝕌⟧ : {t : Pi/.𝕌} → Pi/.⟦ t ⟧ → ⟦ Inj𝕌 t ⟧
Inj⟦𝕌⟧ {𝟙} tt = tt
Inj⟦𝕌⟧ {t₁ +ᵤ t₂} (inj₁ x) = inj₁ (Inj⟦𝕌⟧ x)
Inj⟦𝕌⟧ {t₁ +ᵤ t₂} (inj₂ y) = inj₂ (Inj⟦𝕌⟧ y)
Inj⟦𝕌⟧ {t₁ ×ᵤ t₂} (x , y) = Inj⟦𝕌⟧ x , Inj⟦𝕌⟧ y

Inj⟦𝕌⟧≅ : {t : Pi/.𝕌} (x : Pi/.⟦ t ⟧) → x ≅ Inj⟦𝕌⟧ x
Inj⟦𝕌⟧≅ {𝟙} tt = refl
Inj⟦𝕌⟧≅ {t₁ +ᵤ t₂} (inj₁ x) = inj1 (Inj𝕌≡ t₂) (Inj⟦𝕌⟧≅ x)
  where
    inj1 : {A B A' B' : Set} {x : A} {x' : A'}
         → B ≡ B' → x ≅ x'
         → inj₁ {B = B} x ≅ inj₁ {B = B'} x'
    inj1 refl refl = refl
Inj⟦𝕌⟧≅ {t₁ +ᵤ t₂} (inj₂ y) = inj2 (Inj𝕌≡ t₁) (Inj⟦𝕌⟧≅ y)
  where
    inj2 : {A B A' B' : Set} {y : B} {y' : B'}
         → A ≡ A' → y ≅ y'
         → inj₂ {A = A} y ≅ inj₂ {A = A'} y'
    inj2 refl refl = refl
Inj⟦𝕌⟧≅ {t₁ ×ᵤ t₂} (x , y) = ⦅ Inj⟦𝕌⟧≅ x , Inj⟦𝕌⟧≅ y ⦆
  where
    ⦅_,_⦆ : {A B A' B' : Set} {x : A} {y : B} {x' : A'} {y' : B'}
         → x ≅ x' → y ≅ y'
         → (x , y) ≅ (x' , y')
    ⦅ refl , refl ⦆ = refl

Inj⟷ : ∀ {t₁ t₂} → t₁ ⟷ t₂ → Inj𝕌 t₁ ↔ Inj𝕌 t₂
Inj⟷ unite₊l = unite₊l
Inj⟷ uniti₊l = uniti₊l
Inj⟷ unite₊r = unite₊r
Inj⟷ uniti₊r = uniti₊r
Inj⟷ swap₊ = swap₊
Inj⟷ assocl₊ = assocl₊
Inj⟷ assocr₊ = assocr₊
Inj⟷ unite⋆l = unite⋆l
Inj⟷ uniti⋆l = uniti⋆l
Inj⟷ unite⋆r = unite⋆r
Inj⟷ uniti⋆r = uniti⋆r
Inj⟷ swap⋆ = swap⋆
Inj⟷ assocl⋆ = assocl⋆
Inj⟷ assocr⋆ = assocr⋆
Inj⟷ absorbr = absorbr
Inj⟷ absorbl = absorbl
Inj⟷ factorzr = factorzr
Inj⟷ factorzl = factorzl
Inj⟷ dist = dist
Inj⟷ factor = factor
Inj⟷ distl = distl
Inj⟷ factorl = factorl
Inj⟷ id⟷ = id↔
Inj⟷ (c₁ ⊚ c₂) = Inj⟷ c₁ ⊚ Inj⟷ c₂
Inj⟷ (c₁ ⊕ c₂) = Inj⟷ c₁ ⊕ Inj⟷ c₂
Inj⟷ (c₁ ⊗ c₂) = Inj⟷ c₁ ⊗ Inj⟷ c₂

Ext𝕌 : ∙𝕌 → Σ[ t ∈ 𝕌 ] ⟦ t ⟧
Ext𝕌 (t # v) = (Inj𝕌 t , Inj⟦𝕌⟧ v)
Ext𝕌 (t₁ ∙×ᵤ t₂) with Ext𝕌 t₁ | Ext𝕌 t₂
... | (t₁' , v₁') | (t₂' , v₂') = t₁' ×ᵤ t₂' , v₁' , v₂'
Ext𝕌 (t₁ ∙+ᵤl t₂) with Ext𝕌 t₁ | Ext𝕌 t₂
... | (t₁' , v₁') | (t₂' , v₂') = t₁' +ᵤ t₂' , inj₁ v₁'
Ext𝕌 (t₁ ∙+ᵤr t₂) with Ext𝕌 t₁ | Ext𝕌 t₂
... | (t₁' , v₁') | (t₂' , v₂') = t₁' +ᵤ t₂' , inj₂ v₂'
Ext𝕌 (Singᵤ T) with Ext𝕌 T
... | (t , v) = t , v
Ext𝕌 (Recipᵤ T) with Ext𝕌 T
... | (t , v) = 𝟙/ v , ○

Ext∙⟶ : ∀ {t₁ t₂} → t₁ ∙⟶ t₂ → proj₁ (Ext𝕌 t₁) ↔ proj₁ (Ext𝕌 t₂)
Ext∙⟶ (∙c c) = Inj⟷ c
Ext∙⟶ ∙times# = id↔
Ext∙⟶ ∙#times = id↔
Ext∙⟶ ∙id⟷ = id↔
Ext∙⟶ (c₁ ∙⊚ c₂) = Ext∙⟶ c₁ ⊚ Ext∙⟶ c₂
Ext∙⟶ ∙unite⋆l = unite⋆l
Ext∙⟶ ∙uniti⋆l = uniti⋆l
Ext∙⟶ ∙unite⋆r = unite⋆r
Ext∙⟶ ∙uniti⋆r = uniti⋆r
Ext∙⟶ ∙swap⋆ = swap⋆
Ext∙⟶ ∙assocl⋆ = assocl⋆
Ext∙⟶ ∙assocr⋆ = assocr⋆
Ext∙⟶ (c₁ ∙⊗ c₂) = Ext∙⟶ c₁ ⊗ Ext∙⟶ c₂
Ext∙⟶ (c₁ ∙⊕ₗ c₂) = Ext∙⟶ c₁ ⊕ Ext∙⟶ c₂
Ext∙⟶ (c₁ ∙⊕ᵣ c₂) = Ext∙⟶ c₁ ⊕ Ext∙⟶ c₂
Ext∙⟶ (return T) = id↔
Ext∙⟶ (extract T) = id↔
Ext∙⟶ (η T) = η (proj₂ (Ext𝕌 T))
Ext∙⟶ (ε T) = ε (proj₂ (Ext𝕌 T))

Eval≡ : ∀ {t₁ t₂} {v} (c : t₁ ⟷ t₂) → interp (Inj⟷ c) (Inj⟦𝕌⟧ v) ≡ just (Inj⟦𝕌⟧ (Pi/.eval c v))
Eval≡ {_} {_} {inj₂ y} unite₊l = refl
Eval≡ {_} {_} {x} uniti₊l = refl
Eval≡ {_} {_} {inj₁ x} unite₊r = refl
Eval≡ {_} {_} {x} uniti₊r = refl
Eval≡ {_} {_} {inj₁ x} swap₊ = refl
Eval≡ {_} {_} {inj₂ y} swap₊ = refl
Eval≡ {_} {_} {inj₁ x} assocl₊ = refl
Eval≡ {_} {_} {inj₂ (inj₁ y)} assocl₊ = refl
Eval≡ {_} {_} {inj₂ (inj₂ z)} assocl₊ = refl
Eval≡ {_} {_} {inj₁ (inj₁ x)} assocr₊ = refl
Eval≡ {_} {_} {inj₁ (inj₂ y)} assocr₊ = refl
Eval≡ {_} {_} {inj₂ z} assocr₊ = refl
Eval≡ {_} {_} {x} unite⋆l = refl
Eval≡ {_} {_} {x} uniti⋆l = refl
Eval≡ {_} {_} {x} unite⋆r = refl
Eval≡ {_} {_} {x} uniti⋆r = refl
Eval≡ {_} {_} {x , y} swap⋆ = refl
Eval≡ {_} {_} {x , y , z} assocl⋆ = refl
Eval≡ {_} {_} {(x , y) , z} assocr⋆ = refl
Eval≡ {_} {_} {inj₁ x , z} dist = refl
Eval≡ {_} {_} {inj₂ y , z} dist = refl
Eval≡ {_} {_} {inj₁ (x , z)} factor = refl
Eval≡ {_} {_} {inj₂ (y , z)} factor = refl
Eval≡ {_} {_} {x , inj₁ y} distl = refl
Eval≡ {_} {_} {x , inj₂ z} distl = refl
Eval≡ {_} {_} {inj₁ (x , y)} factorl = refl
Eval≡ {_} {_} {inj₂ (x , z)} factorl = refl
Eval≡ {_} {_} {x} id⟷ = refl
Eval≡ {_} {_} {x} (c₁ ⊚ c₂) rewrite Eval≡ {v = x} c₁ = Eval≡ c₂
Eval≡ {_} {_} {inj₁ x} (c₁ ⊕ c₂) rewrite Eval≡ {v = x} c₁ = refl
Eval≡ {_} {_} {inj₂ y} (c₁ ⊕ c₂) rewrite Eval≡ {v = y} c₂ = refl
Eval≡ {_} {_} {x , y} (c₁ ⊗ c₂) rewrite Eval≡ {v = x} c₁ | Eval≡ {v = y} c₂ = refl

Ext≡ : ∀ {t₁ t₂} → (c : t₁ ∙⟶ t₂)
     → let c'          = Ext∙⟶ c
           (t₁' , v₁') = Ext𝕌 t₁
           (t₂' , v₂') = Ext𝕌 t₂
       in  interp c' v₁' ≡ just v₂'
Ext≡ (∙c c) = Eval≡ c
Ext≡ (∙times# {t₁} {t₂}) = refl
Ext≡ (∙#times {t₁} {t₂}) = refl
Ext≡ ∙id⟷ = refl
Ext≡ (c₁ ∙⊚ c₂) rewrite Ext≡ c₁ | Ext≡ c₂ = refl
Ext≡ (c₁ ∙⊕ₗ c₂) rewrite Ext≡ c₁ = refl
Ext≡ (c₁ ∙⊕ᵣ c₂) rewrite Ext≡ c₂ = refl
Ext≡ ∙unite⋆l = refl
Ext≡ ∙uniti⋆l = refl
Ext≡ ∙unite⋆r = refl
Ext≡ ∙uniti⋆r = refl
Ext≡ ∙swap⋆ = refl
Ext≡ ∙assocl⋆ = refl
Ext≡ ∙assocr⋆ = refl
Ext≡ (c₁ ∙⊗ c₂) rewrite Ext≡ c₁ | Ext≡ c₂ = refl
Ext≡ (return T) = refl
Ext≡ (extract T) = refl
Ext≡ (η T) = refl
Ext≡ (ε T) with 𝕌dec _ (proj₂ (Ext𝕌 T)) (proj₂ (Ext𝕌 T))
Ext≡ (ε T) | yes p = refl
Ext≡ (ε T) | no ¬p = ⊥-elim (¬p refl)

𝔹 : Pi/.𝕌
𝔹 = 𝟙 +ᵤ 𝟙

infixr 2  _→⟨_⟩_
infix  3  _□

_→⟨_⟩_ : (T₁ : ∙𝕌) → {T₂ T₃ : ∙𝕌} →
          (T₁ ∙⟶ T₂) → (T₂ ∙⟶ T₃) → (T₁ ∙⟶ T₃)
_ →⟨ α ⟩ β = α ∙⊚ β

_□ : (T : ∙𝕌) → {T : ∙𝕌} → (T ∙⟶ T)
_□ T = ∙id⟷

zigzag : ∀ b → 𝔹 # b ∙⟶ 𝔹 # b
zigzag b = ∙c uniti⋆l ∙⊚
           ∙times# ∙⊚
           (∙id⟷ ∙⊗ return ((𝟙 +ᵤ 𝟙) # b)) ∙⊚
           (η ((𝟙 +ᵤ 𝟙) # b) ∙⊗ ∙id⟷) ∙⊚
           ∙assocr⋆ ∙⊚
           (∙id⟷ ∙⊗ ∙swap⋆) ∙⊚
           (∙id⟷ ∙⊗ ε ((𝟙 +ᵤ 𝟙) # b)) ∙⊚
           (extract ((𝟙 +ᵤ 𝟙) # b) ∙⊗ ∙id⟷) ∙⊚ ∙#times ∙⊚ ∙c unite⋆r ∙⊚ ∙id⟷

zigzag-ext : ∀ b → Σ[ c ∈ 𝟙 +ᵤ 𝟙 ↔ 𝟙 +ᵤ 𝟙 ] interp c (Inj⟦𝕌⟧ b) ≡ just (Inj⟦𝕌⟧ b)
zigzag-ext b = Ext∙⟶ (zigzag b) , Ext≡ (zigzag b)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module UnquoteDef where

open import Common.Reflection
open import Common.Prelude

module Target where
  mutual
    even : Nat → Bool
    even zero    = true
    even (suc n) = odd n

    odd : Nat → Bool
    odd zero    = false
    odd (suc n) = even n

pattern `false = con (quote false) []
pattern `true  = con (quote true) []
pattern `zero  = con (quote zero) []
pattern `suc n = con (quote suc) (vArg n ∷ [])

pattern _`→_ a b = pi (vArg a) (abs "A" b)
pattern `Nat = def (quote Nat) []
pattern `Bool = def (quote Bool) []

`idType = `Nat `→ `Nat

-- Simple non-mutual case
`id : QName → FunDef
`id f = funDef `idType
        ( clause (vArg `zero            ∷ []) `zero
        ∷ clause (vArg (`suc (var "n")) ∷ []) (`suc (def f (vArg (var 0 []) ∷ [])))
        ∷ [])

`idDef : QName → List Clause
`idDef f =
   clause (vArg `zero            ∷ []) `zero
 ∷ clause (vArg (`suc (var "n")) ∷ []) (`suc (def f (vArg (var 0 []) ∷ [])))
 ∷ []

-- id : Nat → Nat
-- unquoteDef id = `idDef id

-- Now for the mutal ones
`evenOdd : Term → QName → List Clause
`evenOdd base step =
    clause (vArg `zero            ∷ []) base
  ∷ clause (vArg (`suc (var "n")) ∷ []) (def step (vArg (var 0 []) ∷ []))
  ∷ []

_>>_ : TC ⊤ → TC ⊤ → TC ⊤
m >> m₁ = bindTC m λ _ → m₁

even odd : Nat → Bool
unquoteDef even odd =
  defineFun even (`evenOdd `true  odd) >>
  defineFun odd  (`evenOdd `false even)


text:
{-

Basic properties about Σ-types

- Characterization of equality in Σ-types using transport ([pathSigma≡sigmaPath])

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sigma.Properties where

open import Cubical.Data.Sigma.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq
open import Cubical.Data.Unit.Base

private
  variable
    ℓ : Level
    A A' : Type ℓ
    B B' : (a : A) → Type ℓ
    C : (a : A) (b : B a) → Type ℓ

mapʳ : (∀ {a} → B a → B' a) → Σ A B → Σ A B'
mapʳ f (a , b) = (a , f b)

mapˡ : {B : Type ℓ} → (f : A → A') → Σ A (λ _ → B) → Σ A' (λ _ → B)
mapˡ f (a , b) = (f a , b)

ΣPathP : ∀ {x y}
  → Σ (fst x ≡ fst y) (λ a≡ → PathP (λ i → B (a≡ i)) (snd x) (snd y))
  → x ≡ y
ΣPathP eq i = fst eq i , snd eq i

Σ-split-iso : {x y : Σ A B}
  → Iso (Σ[ q ∈ fst x ≡ fst y ] (PathP (λ i → B (q i)) (snd x) (snd y)))
         (x ≡ y)
Iso.fun (Σ-split-iso) = ΣPathP
Iso.inv (Σ-split-iso) eq = (λ i → fst (eq i)) , (λ i → snd (eq i))
Iso.rightInv (Σ-split-iso) x = refl {x = x}
Iso.leftInv (Σ-split-iso) x = refl {x = x}

Σ≃ : {x y : Σ A B}  →
     Σ (fst x ≡ fst y) (λ p → PathP (λ i → B (p i)) (snd x) (snd y)) ≃
     (x ≡ y)
Σ≃ {A = A} {B = B} {x} {y} = isoToEquiv (Σ-split-iso)

Σ≡ : {a a' : A} {b : B a} {b' : B a'} → (Σ (a ≡ a') (λ q → PathP (λ i → B (q i)) b b')) ≡ ((a , b) ≡ (a' , b'))
Σ≡ = isoToPath Σ-split-iso -- ua Σ≃

ΣProp≡ : ((x : A) → isProp (B x)) → {u v : Σ A B}
       → (p : u .fst ≡ v .fst) → u ≡ v
ΣProp≡ pB {u} {v} p i = (p i) , isProp→PathP (λ i → pB (p i)) (u .snd) (v .snd) i

-- Alternative version for path in Σ-types, as in the HoTT book

sigmaPathTransport : (a b : Σ A B) → Type _
sigmaPathTransport {B = B} a b =
  Σ (fst a ≡ fst b) (λ p → transport (λ i → B (p i)) (snd a) ≡ snd b)

_Σ≡T_ : (a b : Σ A B) → Type _
a Σ≡T b = sigmaPathTransport a b

-- now we prove that the alternative path space a Σ≡ b is equal to the usual path space a ≡ b

-- forward direction

private
  pathSigma-π1 : {a b : Σ A B} → a ≡ b → fst a ≡ fst b
  pathSigma-π1 p i = fst (p i)

  filler-π2 : {a b : Σ A B} → (p : a ≡ b) → I → (i : I) → B (fst (p i))
  filler-π2 {B = B} {a = a} p i =
    fill (λ i → B (fst (p i)))
         (λ t → λ { (i = i0) → transport-filler (λ j → B (fst (p j))) (snd a) t
                  ; (i = i1) → snd (p t) })
         (inS (snd a))

  pathSigma-π2 : {a b : Σ A B} → (p : a ≡ b) →
    subst B (pathSigma-π1 p) (snd a) ≡ snd b
  pathSigma-π2 p i = filler-π2 p i i1

pathSigma→sigmaPath : (a b : Σ A B) → a ≡ b → a Σ≡T b
pathSigma→sigmaPath _ _ p = (pathSigma-π1 p , pathSigma-π2 p)

-- backward direction

private
  filler-comp : (a b : Σ A B) → a Σ≡T b → I → I → Σ A B
  filler-comp {B = B} a b (p , q) i =
    hfill (λ t → λ { (i = i0) → a
                   ; (i = i1) → (p i1 , q t) })
          (inS (p i , transport-filler (λ j → B (p j)) (snd a) i))

sigmaPath→pathSigma : (a b : Σ A B) → a Σ≡T b → (a ≡ b)
sigmaPath→pathSigma a b x i = filler-comp a b x i i1

-- first homotopy

private
  homotopy-π1 : (a b : Σ A B) →
    ∀ (x : a Σ≡T b) → pathSigma-π1 (sigmaPath→pathSigma a b x) ≡ fst x
  homotopy-π1 a b x i j = fst (filler-comp a b x j (~ i))

  homotopy-π2 : (a b : Σ A B) → (p : a Σ≡T b) → (i : I) →
             (transport (λ j → B (fst (filler-comp a b p j i))) (snd a) ≡ snd b)
  homotopy-π2 {B = B} a b p i j =
    comp (λ t → B (fst (filler-comp a b p t (i ∨ j))))
         (λ t → λ { (j = i0) → transport-filler (λ t → B (fst (filler-comp a b p t i)))
                                                (snd a) t
                  ; (j = i1) → snd (sigmaPath→pathSigma a b p t)
                  ; (i = i0) → snd (filler-comp a b p t j)
                  ; (i = i1) → filler-π2 (sigmaPath→pathSigma a b p) j t })
         (snd a)

pathSigma→sigmaPath→pathSigma : {a b : Σ A B} →
  ∀ (x : a Σ≡T b) → pathSigma→sigmaPath _ _ (sigmaPath→pathSigma a b x) ≡ x
pathSigma→sigmaPath→pathSigma {a = a} p i =
  (homotopy-π1 a _ p i , homotopy-π2 a _ p (~ i))

-- second homotopy

sigmaPath→pathSigma→sigmaPath : {a b : Σ A B} →
  ∀ (x : a ≡ b) → sigmaPath→pathSigma a b (pathSigma→sigmaPath _ _ x) ≡ x
sigmaPath→pathSigma→sigmaPath {B = B} {a = a} {b = b} p i j =
  hcomp (λ t → λ { (i = i1) → (fst (p j) , filler-π2 p t j)
                 ; (i = i0) → filler-comp a b (pathSigma→sigmaPath _ _ p) j t
                 ; (j = i0) → (fst a , snd a)
                 ; (j = i1) → (fst b , filler-π2 p t i1) })
        (fst (p j) , transport-filler (λ k → B (fst (p k))) (snd a) j)

pathSigma≡sigmaPath : (a b : Σ A B) → (a ≡ b) ≡ (a Σ≡T b)
pathSigma≡sigmaPath a b =
  isoToPath (iso (pathSigma→sigmaPath a b)
                 (sigmaPath→pathSigma a b)
                 (pathSigma→sigmaPath→pathSigma {a = a})
                 sigmaPath→pathSigma→sigmaPath)

discreteΣ : Discrete A → ((a : A) → Discrete (B a)) → Discrete (Σ A B)
discreteΣ {B = B} Adis Bdis (a0 , b0) (a1 , b1) = discreteΣ' (Adis a0 a1)
  where
    discreteΣ' : Dec (a0 ≡ a1) → Dec ((a0 , b0) ≡ (a1 , b1))
    discreteΣ' (yes p) = J (λ a1 p → ∀ b1 → Dec ((a0 , b0) ≡ (a1 , b1))) (discreteΣ'') p b1
      where
        discreteΣ'' : (b1 : B a0) → Dec ((a0 , b0) ≡ (a0 , b1))
        discreteΣ'' b1 with Bdis a0 b0 b1
        ... | (yes q) = yes (transport (ua Σ≃) (refl , q))
        ... | (no ¬q) = no (λ r → ¬q (subst (λ X → PathP (λ i → B (X i)) b0 b1) (Discrete→isSet Adis a0 a0 (cong fst r) refl) (cong snd r)))
    discreteΣ' (no ¬p) = no (λ r → ¬p (cong fst r))

Σ-contractFst : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} (c : isContr A)
  → Σ A B ≃ B (c .fst)
Σ-contractFst {B = B} c =
  isoToEquiv
    (iso
      (λ {(a , b) → subst B (sym (c .snd a)) b})
      (c .fst ,_)
      (λ b →
        cong (λ p → subst B p b) (isProp→isSet (isContr→isProp c) _ _ _ _)
        ∙ transportRefl _)
      (λ {(a , b) →
        sigmaPath→pathSigma _ _ (c .snd a , transportTransport⁻ (cong B (c .snd a)) _)}))

-- a special case of the above
ΣUnit : ∀ {ℓ} (A : Unit → Type ℓ) → Σ Unit A ≃ A tt
ΣUnit A = isoToEquiv (iso snd (λ { x → (tt , x) }) (λ _ → refl) (λ _ → refl))

assocΣ : (Σ[ (a , b) ∈ Σ A B ] C a b) ≃ (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
assocΣ = isoToEquiv (iso (λ { ((x , y) , z) → (x , (y , z)) })
                         (λ { (x , (y , z)) → ((x , y) , z) })
                         (λ _ → refl) (λ _ → refl))

congΣEquiv : (∀ a → B a ≃ B' a) → Σ A B ≃ Σ A B'
congΣEquiv h =
  isoToEquiv (iso (λ { (x , y)   → (x , equivFun (h x) y) })
                  (λ { (x , y)   → (x , invEq    (h x) y) })
                  (λ { (x , y) i → (x , retEq    (h x) y i) })
                  (λ { (x , y) i → (x , secEq    (h x) y i) }))

PiΣ : ((a : A) → Σ[ b ∈ B a ] C a b) ≃ (Σ[ f ∈ ((a : A) → B a) ] ∀ a → C a (f a))
PiΣ = isoToEquiv (iso (λ f → fst ∘ f , snd ∘ f)
                      (λ (f , g) → (λ x → f x , g x))
                      (λ _ → refl) (λ _ → refl))

swapΣEquiv : ∀ {ℓ'} (A : Type ℓ) (B : Type ℓ') → A × B ≃ B × A
swapΣEquiv A B = isoToEquiv (iso (λ x → x .snd , x .fst) (λ z → z .snd , z .fst) (\ _ → refl) (\ _ → refl))

Σ-ap-iso₁ : ∀ {ℓ} {ℓ'} {A A' : Type ℓ} {B : A' → Type ℓ'}
          → (isom : Iso A A')
          → Iso (Σ A (B ∘ (Iso.fun isom)))
                (Σ A' B)
Iso.fun (Σ-ap-iso₁ isom) x = (Iso.fun isom) (x .fst) , x .snd
Iso.inv (Σ-ap-iso₁ {B = B} isom) x = (Iso.inv isom) (x .fst) , subst B (sym (ε' (x .fst))) (x .snd)
  where
    ε' = fst (vogt isom)
Iso.rightInv (Σ-ap-iso₁ {B = B} isom) (x , y) = ΣPathP (ε' x ,
  transport
    (sym (PathP≡Path (λ j → cong B (ε' x) j) (subst B (sym (ε' x)) y) y))
    (subst B (ε' x) (subst B (sym (ε' x)) y)
      ≡⟨ sym (substComposite B (sym (ε' x)) (ε' x) y) ⟩
    subst B ((sym (ε' x)) ∙ (ε' x)) y
      ≡⟨ (cong (λ a → subst B a y) (lCancel (ε' x))) ⟩
    subst B refl y
      ≡⟨ substRefl {B = B} y ⟩
    y ∎))
  where
    ε' = fst (vogt isom)
Iso.leftInv (Σ-ap-iso₁ {A = A} {B = B} isom@(iso f g ε η)) (x , y) = ΣPathP (η x ,
  transport
    (sym (PathP≡Path (λ j → cong B (cong f (η x)) j) (subst B (sym (ε' (f x))) y) y))
    (subst B (cong f (η x)) (subst B (sym (ε' (f x))) y)
      ≡⟨ sym (substComposite B (sym (ε' (f x))) (cong f (η x)) y) ⟩
    subst B (sym (ε' (f x)) ∙ (cong f (η x))) y
      ≡⟨ cong (λ a → subst B a y) (lem x) ⟩
    subst B (refl) y
      ≡⟨ substRefl {B = B} y ⟩
    y ∎))
  where
    ε' = fst (vogt isom)
    γ = snd (vogt isom)

    lem : (x : A) → sym (ε' (f x)) ∙ cong f (η x) ≡ refl
    lem x = cong (λ a → sym (ε' (f x)) ∙ a) (γ x) ∙ lCancel (ε' (f x))

Σ-ap₁ : (isom : A ≡ A') → Σ A (B ∘ transport isom) ≡ Σ A' B
Σ-ap₁ isom = isoToPath (Σ-ap-iso₁ (pathToIso isom))

Σ-ap-iso₂ : ((x : A) → Iso (B x) (B' x)) → Iso (Σ A B) (Σ A B')
Iso.fun (Σ-ap-iso₂ isom) (x , y) = x , Iso.fun (isom x) y
Iso.inv (Σ-ap-iso₂ isom) (x , y') = x , Iso.inv (isom x) y'
Iso.rightInv (Σ-ap-iso₂ isom) (x , y) = ΣPathP (refl , Iso.rightInv (isom x) y)
Iso.leftInv (Σ-ap-iso₂ isom) (x , y') = ΣPathP (refl , Iso.leftInv (isom x) y')

Σ-ap₂ : ((x : A) → B x ≡ B' x) → Σ A B ≡ Σ A B'
Σ-ap₂ isom = isoToPath (Σ-ap-iso₂ (pathToIso ∘ isom))

Σ-ap-iso :
  ∀ {ℓ ℓ'} {A A' : Type ℓ}
  → {B : A → Type ℓ'} {B' : A' → Type ℓ'}
  → (isom : Iso A A')
  → ((x : A) → Iso (B x) (B' (Iso.fun isom x)))
  ------------------------
  → Iso (Σ A B) (Σ A' B')
Σ-ap-iso isom isom' = compIso (Σ-ap-iso₂ isom') (Σ-ap-iso₁ isom)

Σ-ap :
  ∀ {ℓ ℓ'} {X X' : Type ℓ} {Y : X → Type ℓ'} {Y' : X' → Type ℓ'}
  → (isom : X ≡ X')
  → ((x : X) → Y x ≡ Y' (transport isom x))
  ----------
  → (Σ X Y)
  ≡ (Σ X' Y')
Σ-ap isom isom' = isoToPath (Σ-ap-iso (pathToIso isom) (pathToIso ∘ isom'))

Σ-ap' :
  ∀ {ℓ ℓ'} {X X' : Type ℓ} {Y : X → Type ℓ'} {Y' : X' → Type ℓ'}
  → (isom : X ≡ X')
  → (PathP (λ i → isom i → Type ℓ') Y Y')
  ----------
  → (Σ X Y)
  ≡ (Σ X' Y')
Σ-ap'  {ℓ} {ℓ'} isom isom' = cong₂ (λ (a : Type ℓ) (b : a → Type ℓ') → Σ a λ x → b x) isom isom'


text:
-- Andreas, 2016-06-20 issue #2051
-- Try to preserve rhs when splitting a clause

data D : Set where
  d : D
  c : D → D

-- A simple RHS that should be preserved by splitting:

con : (x : D) → D
con x = c {!x!}  -- C-c C-c

-- More delicate, a meta variable applied to something:
-- This means the hole is not at the rightmost position.

app : (x : D) → D
app x = {!x!} x

-- A let-binding (not represented in internal syntax):

test : (x : D) → D
test x = let y = c in {!x!}  -- C-c C-c

-- Case splitting replaces entire RHS by hole
--   test c = ?