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

module Pif where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        proof-irrelevance; module ≡-Reasoning)
open import Data.Nat.Properties using (m≢1+m+n; i+j≡0⇒i≡0; i+j≡0⇒j≡0)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+)
open import Relation.Binary.Core using (Transitive)

open import Data.String using (String)
  renaming (_++_ to _++S_)
open import Data.Nat.Show using (show)
open import Data.Bool using (Bool; false; true; _∧_; _∨_)
open import Data.Nat using (ℕ; suc; _+_; _∸_; _*_; _<_; _≮_; _≤_; _≰_;
  z≤n; s≤s; _≟_; _≤?_; module ≤-Reasoning)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; _ℕ-_; _≺_;
         raise; inject+; inject₁; inject≤; _≻toℕ_)
  renaming (_+_ to _F+_)

open import Data.Vec
  using (Vec; tabulate; []; _∷_ ; tail; lookup; zip; zipWith; splitAt;
         _[_]≔_; allFin; toList)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)

open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Unit    using (⊤; tt)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import PiLevel0
open import Cauchy
open import Perm
open import Proofs
open import CauchyProofs
open import CauchyProofsT
open import CauchyProofsS
open import Groupoid

------------------------------------------------------------------------------
-- A combinator t₁ ⟷ t₂ denotes a permutation.

c2cauchy : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → Cauchy (size t₁)
-- the cases that do not inspect t₁ and t₂ should be at the beginning
-- so that Agda would unfold them
c2cauchy (c₁ ◎ c₂) =
  scompcauchy
    (c2cauchy c₁)
    (subst Cauchy (size≡! c₁) (c2cauchy c₂))
c2cauchy (c₁ ⊕ c₂) = pcompcauchy (c2cauchy c₁) (c2cauchy c₂)
c2cauchy (c₁ ⊗ c₂) = tcompcauchy (c2cauchy c₁) (c2cauchy c₂)
c2cauchy {PLUS ZERO t} unite₊ = idcauchy (size t)
c2cauchy {t} uniti₊ = idcauchy (size t)
c2cauchy {PLUS t₁ t₂} swap₊ = swap+cauchy (size t₁) (size t₂)
c2cauchy {PLUS t₁ (PLUS t₂ t₃)} assocl₊ =
  idcauchy (size t₁ + (size t₂ + size t₃))
c2cauchy {PLUS (PLUS t₁ t₂) t₃} assocr₊ =
  idcauchy ((size t₁ + size t₂) + size t₃)
c2cauchy {TIMES ONE t} unite⋆ =
  subst Cauchy (sym (+-right-identity (size t))) (idcauchy (size t))
c2cauchy {t} uniti⋆ = idcauchy (size t)
c2cauchy {TIMES t₁ t₂} {TIMES .t₂ .t₁} swap⋆ = swap⋆cauchy (size t₁) (size t₂)
c2cauchy {TIMES t₁ (TIMES t₂ t₃)} assocl⋆ =
  idcauchy (size t₁ * (size t₂ * size t₃))
c2cauchy {TIMES (TIMES t₁ t₂) t₃} assocr⋆ =
  idcauchy ((size t₁ * size t₂) * size t₃)
c2cauchy {TIMES ZERO t} distz = []
c2cauchy factorz = []
c2cauchy {TIMES (PLUS t₁ t₂) t₃} dist =
  idcauchy ((size t₁ + size t₂) * size t₃)
c2cauchy {PLUS (TIMES t₁ t₃) (TIMES t₂ .t₃)} factor =
  idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))
c2cauchy {t} id⟷  = idcauchy (size t)

c2perm : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → Permutation (size t₁)
-- the cases that do not inspect t₁ and t₂ should be at the beginning
-- so that Agda would unfold them
c2perm (c₁ ◎ c₂) =
  scompperm
    (c2perm c₁)
    (subst Permutation (size≡! c₁) (c2perm c₂))
c2perm (c₁ ⊕ c₂) = pcompperm (c2perm c₁) (c2perm c₂)
c2perm (c₁ ⊗ c₂) = tcompperm (c2perm c₁) (c2perm c₂)
c2perm unfoldBool = idperm 2
c2perm foldBool   = idperm 2
c2perm {PLUS ZERO t} unite₊ = idperm (size t)
c2perm {t} uniti₊ = idperm (size t)
c2perm {PLUS t₁ t₂} swap₊ = swap+perm (size t₁) (size t₂)
c2perm {PLUS t₁ (PLUS t₂ t₃)} assocl₊ =
  idperm (size t₁ + (size t₂ + size t₃))
c2perm {PLUS (PLUS t₁ t₂) t₃} assocr₊ =
  idperm ((size t₁ + size t₂) + size t₃)
c2perm {TIMES ONE t} unite⋆ =
  subst Permutation (sym (+-right-identity (size t))) (idperm (size t))
c2perm {t} uniti⋆ = idperm (size t)
c2perm {TIMES t₁ t₂} {TIMES .t₂ .t₁} swap⋆ = swap⋆perm (size t₁) (size t₂)
c2perm {TIMES t₁ (TIMES t₂ t₃)} assocl⋆ =
  idperm (size t₁ * (size t₂ * size t₃))
c2perm {TIMES (TIMES t₁ t₂) t₃} assocr⋆ =
  idperm ((size t₁ * size t₂) * size t₃)
c2perm {TIMES ZERO t} distz = emptyperm
c2perm factorz = emptyperm
c2perm {TIMES (PLUS t₁ t₂) t₃} dist =
  idperm ((size t₁ + size t₂) * size t₃)
c2perm {PLUS (TIMES t₁ t₃) (TIMES t₂ .t₃)} factor =
  idperm ((size t₁ * size t₃) + (size t₂ * size t₃))
c2perm {t} id⟷  = idperm (size t)

-- Looking forward to Sec. 2.2 (Functions are functors). The
-- corresponding statement to Lemma 2.2.1 in our setting would be the
-- following. Given any *size preserving* function f : U → U, it is
-- the case that a combinator (path) c : t₁ ⟷ t₂ maps to a combinator
-- (path) ap_f(c) : f(t₁) ⟷ f(t₂).

------------------------------------------------------------------------------
-- Extensional equivalence of combinators

-- Two combinators are equivalent if they denote the same
-- permutation. Generally we would require that the two permutations
-- map the same value x to values y and z that have a path between
-- them, but because the internals of each type are discrete
-- groupoids, this reduces to saying that y and z are identical, and
-- hence that the permutations are identical.

infix  10  _∼_

_∼_ : {t₁ t₂ : U} → (c₁ c₂ : t₁ ⟷ t₂) → Set
c₁ ∼ c₂ = (c2cauchy c₁ ≡ c2cauchy c₂)

-- The relation ~ is an equivalence relation

refl∼ : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (c ∼ c)
refl∼ = refl

sym∼ : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ∼ c₂) → (c₂ ∼ c₁)
sym∼ = sym

trans∼ : {t₁ t₂ : U} {c₁ c₂ c₃ : t₁ ⟷ t₂} → (c₁ ∼ c₂) → (c₂ ∼ c₃) → (c₁ ∼ c₃)
trans∼ = trans

assoc∼ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
         c₁ ◎ (c₂ ◎ c₃) ∼ (c₁ ◎ c₂) ◎ c₃
assoc∼ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃} =
  begin (c2cauchy (c₁ ◎ (c₂ ◎ c₃))
           ≡⟨ refl ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (scompcauchy
               (c2cauchy c₂)
               (subst Cauchy (size≡! c₂) (c2cauchy c₃))))
           ≡⟨ cong
                (scompcauchy (c2cauchy c₁))
                (subst-dist
                  scompcauchy
                  (size≡! c₁)
                  (c2cauchy c₂)
                  (subst Cauchy (size≡! c₂) (c2cauchy c₃))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (scompcauchy
             (subst Cauchy (size≡! c₁) (c2cauchy c₂))
             (subst Cauchy (size≡! c₁)
               (subst Cauchy (size≡! c₂) (c2cauchy c₃))))
           ≡⟨ cong (λ x →
                scompcauchy
                  (c2cauchy c₁)
                  (scompcauchy
                    (subst Cauchy (size≡! c₁) (c2cauchy c₂))
                    x))
                (subst-trans (size≡! c₁) (size≡! c₂) (c2cauchy c₃)) ⟩
         scompcauchy
           (c2cauchy c₁)
           (scompcauchy
             (subst Cauchy (size≡! c₁) (c2cauchy c₂))
             (subst Cauchy (trans (size≡! c₂) (size≡! c₁)) (c2cauchy c₃)))
           ≡⟨ scompassoc
                (c2cauchy c₁)
                (subst Cauchy (size≡! c₁) (c2cauchy c₂))
                (subst Cauchy (trans (size≡! c₂) (size≡! c₁)) (c2cauchy c₃)) ⟩
         scompcauchy
           (scompcauchy
             (c2cauchy c₁)
             (subst Cauchy (size≡! c₁) (c2cauchy c₂)))
           (subst Cauchy (trans (size≡! c₂) (size≡! c₁)) (c2cauchy c₃))
           ≡⟨ refl ⟩
         c2cauchy ((c₁ ◎ c₂) ◎ c₃) ∎)
  where open ≡-Reasoning

-- The combinators c : t₁ ⟷ t₂ are paths; we can transport
-- size-preserving properties across c. In particular, for some
-- appropriate P we want P(t₁) to map to P(t₂) via c.

-- The relation ~ validates the groupoid laws

c◎id∼c : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ◎ id⟷ ∼ c
c◎id∼c {t₁} {t₂} {c} =
  begin (c2cauchy (c ◎ id⟷)
           ≡⟨ refl ⟩
        scompcauchy
          (c2cauchy c)
          (subst Cauchy (size≡! c) (allFin (size t₂)))
           ≡⟨ cong (λ x → scompcauchy (c2cauchy c) x)
              (congD! {B = Cauchy} allFin (size≡! c)) ⟩
        scompcauchy (c2cauchy c) (allFin (size t₁))
           ≡⟨ scomprid (c2cauchy c) ⟩
         c2cauchy c ∎)
  where open ≡-Reasoning

id◎c∼c : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → id⟷ ◎ c ∼ c
id◎c∼c {t₁} {t₂} {c} =
  begin (c2cauchy (id⟷ ◎ c)
           ≡⟨ refl ⟩
        scompcauchy
          (allFin (size t₁))
          (subst Cauchy refl (c2cauchy c))
           ≡⟨ refl ⟩
        scompcauchy (allFin (size t₁)) (c2cauchy c)
           ≡⟨ scomplid (c2cauchy c) ⟩
         c2cauchy c ∎)
  where open ≡-Reasoning

linv∼ : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ◎ ! c ∼ id⟷
linv∼ {PLUS ZERO t} {.t} {unite₊} =
  begin (c2cauchy {PLUS ZERO t} (unite₊ ◎ uniti₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t)) (idcauchy (size t))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {PLUS ZERO t} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {t} {PLUS ZERO .t} {uniti₊} =
  begin (c2cauchy {t} (uniti₊ ◎ unite₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t)) (idcauchy (size t))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {t} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {PLUS t₁ t₂} {PLUS .t₂ .t₁} {swap₊} =
  begin (c2cauchy {PLUS t₁ t₂} (swap₊ ◎ swap₊)
           ≡⟨ refl ⟩
         scompcauchy
           (swap+cauchy (size t₁) (size t₂))
           (subst Cauchy (+-comm (size t₂) (size t₁))
             (swap+cauchy (size t₂) (size t₁)))
           ≡⟨ swap+idemp (size t₁) (size t₂) ⟩
         c2cauchy {PLUS t₁ t₂} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃} {assocl₊} =
  begin (c2cauchy {PLUS t₁ (PLUS t₂ t₃)} (assocl₊ ◎ assocr₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t₁ + (size t₂ + size t₃)))
           (subst Cauchy (+-assoc (size t₁) (size t₂) (size t₃))
             (idcauchy ((size t₁ + size t₂) + size t₃)))
           ≡⟨ cong
               (scompcauchy (idcauchy (size t₁ + (size t₂ + size t₃))))
               (congD! idcauchy (+-assoc (size t₁) (size t₂) (size t₃))) ⟩
         scompcauchy (idcauchy (size t₁ + (size t₂ + size t₃)))
           (idcauchy (size t₁ + (size t₂ + size t₃)))
           ≡⟨ scomplid (idcauchy (size t₁ + (size t₂ + size t₃))) ⟩
         c2cauchy {PLUS t₁ (PLUS t₂ t₃)} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {PLUS (PLUS t₁ t₂) t₃} {PLUS .t₁ (PLUS .t₂ .t₃)} {assocr₊} =
  begin (c2cauchy {PLUS (PLUS t₁ t₂) t₃} (assocr₊ ◎ assocl₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) + size t₃))
           (subst Cauchy (sym (+-assoc (size t₁) (size t₂) (size t₃)))
             (idcauchy (size t₁ + (size t₂ + size t₃))))
           ≡⟨ cong
                (scompcauchy (idcauchy ((size t₁ + size t₂) + size t₃)))
                (congD! idcauchy (sym (+-assoc (size t₁) (size t₂) (size t₃)))) ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) + size t₃))
           (idcauchy ((size t₁ + size t₂) + size t₃))
           ≡⟨ scomplid (idcauchy ((size t₁ + size t₂) + size t₃)) ⟩
         c2cauchy {PLUS (PLUS t₁ t₂) t₃} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {TIMES ONE t} {.t} {unite⋆} =
  begin (c2cauchy {TIMES ONE t} (unite⋆ ◎ uniti⋆)
           ≡⟨ refl ⟩
         scompcauchy
           (subst Cauchy (sym (+-right-identity (size t))) (idcauchy (size t)))
           (subst Cauchy (sym (+-right-identity (size t))) (idcauchy (size t)))
           ≡⟨ cong
                (λ x → scompcauchy x x)
                (congD! idcauchy (sym (+-right-identity (size t)))) ⟩
         scompcauchy (idcauchy (size t + 0)) (idcauchy (size t + 0))
           ≡⟨ scomplid (idcauchy (size t + 0)) ⟩
         c2cauchy {TIMES ONE t} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {t} {TIMES ONE .t} {uniti⋆} =
  begin (c2cauchy {t} (uniti⋆ ◎ unite⋆)
           ≡⟨ refl ⟩
         scompcauchy
           (idcauchy (size t))
           (subst Cauchy (+-right-identity (size t))
             (subst Cauchy (sym (+-right-identity (size t)))
               (idcauchy (size t))))
           ≡⟨ cong
                (scompcauchy (idcauchy (size t)))
                (subst-trans
                  (+-right-identity (size t))
                  (sym (+-right-identity (size t)))
                  (idcauchy (size t))) ⟩
         scompcauchy
           (idcauchy (size t))
           (subst Cauchy (trans (sym (+-right-identity (size t)))
                                (+-right-identity (size t)))
               (idcauchy (size t)))
           ≡⟨ cong
                 (λ x → scompcauchy
                          (idcauchy (size t))
                          (subst Cauchy x (idcauchy (size t))))
                 (trans-syml (+-right-identity (size t))) ⟩
         scompcauchy
           (idcauchy (size t))
           (subst Cauchy refl (idcauchy (size t)))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {t} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {TIMES t₁ t₂} {TIMES .t₂ .t₁} {swap⋆} =
  begin (c2cauchy {TIMES t₁ t₂} (swap⋆ ◎ swap⋆)
           ≡⟨ refl ⟩
         scompcauchy
           (swap⋆cauchy (size t₁) (size t₂))
           (subst Cauchy (*-comm (size t₂) (size t₁))
             (swap⋆cauchy (size t₂) (size t₁)))
           ≡⟨ swap⋆idemp (size t₁) (size t₂) ⟩
         c2cauchy {TIMES t₁ t₂} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {TIMES t₁ (TIMES t₂ t₃)} {TIMES (TIMES .t₁ .t₂) .t₃} {assocl⋆} =
  begin (c2cauchy {TIMES t₁ (TIMES t₂ t₃)} (assocl⋆ ◎ assocr⋆)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t₁ * (size t₂ * size t₃)))
           (subst Cauchy (*-assoc (size t₁) (size t₂) (size t₃))
             (idcauchy ((size t₁ * size t₂) * size t₃)))
           ≡⟨ cong
                (scompcauchy (idcauchy (size t₁ * (size t₂ * size t₃))))
                (congD! idcauchy (*-assoc (size t₁) (size t₂) (size t₃))) ⟩
         scompcauchy (idcauchy (size t₁ * (size t₂ * size t₃)))
           (idcauchy (size t₁ * (size t₂ * size t₃)))
           ≡⟨ scomplid (idcauchy (size t₁ * (size t₂ * size t₃))) ⟩
         c2cauchy {TIMES t₁ (TIMES t₂ t₃)} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {TIMES (TIMES t₁ t₂) t₃} {TIMES .t₁ (TIMES .t₂ .t₃)} {assocr⋆} =
  begin (c2cauchy {TIMES (TIMES t₁ t₂) t₃} (assocr⋆ ◎ assocl⋆)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ * size t₂) * size t₃))
           (subst Cauchy (sym (*-assoc (size t₁) (size t₂) (size t₃)))
             (idcauchy (size t₁ * (size t₂ * size t₃))))
           ≡⟨ cong
                (scompcauchy (idcauchy ((size t₁ * size t₂) * size t₃)))
                (congD! idcauchy (sym (*-assoc (size t₁) (size t₂) (size t₃)))) ⟩
         scompcauchy (idcauchy ((size t₁ * size t₂) * size t₃))
           (idcauchy ((size t₁ * size t₂) * size t₃))
           ≡⟨ scomplid (idcauchy ((size t₁ * size t₂) * size t₃)) ⟩
         c2cauchy {TIMES (TIMES t₁ t₂) t₃} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {TIMES ZERO t} {ZERO} {distz} = refl
linv∼ {ZERO} {TIMES ZERO t} {factorz} = refl
linv∼ {TIMES (PLUS t₁ t₂) t₃} {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)} {dist} =
  begin (c2cauchy {TIMES (PLUS t₁ t₂) t₃} (dist ◎ factor)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) * size t₃))
           (subst Cauchy (sym (distribʳ-*-+ (size t₃) (size t₁) (size t₂)))
             (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))))
           ≡⟨ cong
                (scompcauchy (idcauchy ((size t₁ + size t₂) * size t₃)))
                (congD! idcauchy
                  (sym (distribʳ-*-+ (size t₃) (size t₁) (size t₂)))) ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) * size t₃))
           (idcauchy ((size t₁ + size t₂) * size t₃))
           ≡⟨ scomplid (idcauchy ((size t₁ + size t₂) * size t₃)) ⟩
         c2cauchy {TIMES (PLUS t₁ t₂) t₃} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {PLUS (TIMES t₁ t₃) (TIMES t₂ .t₃)} {TIMES (PLUS .t₁ .t₂) .t₃} {factor} =
  begin (c2cauchy {PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)} (factor ◎ dist)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃)))
           (subst Cauchy (distribʳ-*-+ (size t₃) (size t₁) (size t₂))
             (idcauchy ((size t₁ + size t₂) * size t₃)))
           ≡⟨ cong
                (scompcauchy
                  (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))))
                (congD! idcauchy
                  (distribʳ-*-+ (size t₃) (size t₁) (size t₂))) ⟩
         scompcauchy (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃)))
           (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃)))
           ≡⟨ scomplid (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))) ⟩
         c2cauchy {PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {t} {.t} {id⟷} =
  begin (c2cauchy {t} (id⟷ ◎ id⟷)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t)) (idcauchy (size t))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {t} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {t₁} {t₃} {_◎_ {t₂ = t₂} c₁ c₂} =
  begin (c2cauchy {t₁} ((c₁ ◎ c₂) ◎ ((! c₂) ◎ (! c₁)))
           ≡⟨ refl ⟩
         scompcauchy
           (scompcauchy
              (c2cauchy c₁)
              (subst Cauchy (size≡! c₁) (c2cauchy c₂)))
           (subst Cauchy (trans (size≡! c₂) (size≡! c₁))
              (scompcauchy
                (c2cauchy (! c₂))
                (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))))
           ≡⟨ sym (scompassoc
                    (c2cauchy c₁)
                    (subst Cauchy (size≡! c₁) (c2cauchy c₂))
                    (subst Cauchy (trans (size≡! c₂) (size≡! c₁))
                      (scompcauchy
                        (c2cauchy (! c₂))
                        (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))))  ⟩
         scompcauchy
           (c2cauchy c₁)
           (scompcauchy
              (subst Cauchy (size≡! c₁) (c2cauchy c₂))
              (subst Cauchy (trans (size≡! c₂) (size≡! c₁))
                (scompcauchy
                  (c2cauchy (! c₂))
                  (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (scompcauchy
                           (subst Cauchy (size≡! c₁) (c2cauchy c₂))
                           x))
                (sym (subst-trans (size≡! c₁) (size≡! c₂)
                       (scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (scompcauchy
              (subst Cauchy (size≡! c₁) (c2cauchy c₂))
              (subst Cauchy (size≡! c₁)
                (subst Cauchy (size≡! c₂)
                  (scompcauchy
                    (c2cauchy (! c₂))
                    (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))))))
           ≡⟨ cong
                (scompcauchy (c2cauchy c₁))
                (sym (subst-dist scompcauchy (size≡! c₁)
                       (c2cauchy c₂)
                       (subst Cauchy (size≡! c₂)
                         (scompcauchy
                           (c2cauchy (! c₂))
                           (subst Cauchy (size≡! (! c₂))
                             (c2cauchy (! c₁))))))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (scompcauchy
               (c2cauchy c₂)
               (subst Cauchy (size≡! c₂)
                 (scompcauchy
                   (c2cauchy (! c₂))
                   (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁)
                           (scompcauchy (c2cauchy c₂) x)))
                (subst-dist scompcauchy (size≡! c₂)
                  (c2cauchy (! c₂))
                  (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (scompcauchy
               (c2cauchy c₂)
                 (scompcauchy
                   (subst Cauchy (size≡! c₂) (c2cauchy (! c₂)))
                   (subst Cauchy (size≡! c₂)
                     (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁) x))
                (scompassoc
                  (c2cauchy c₂)
                  (subst Cauchy (size≡! c₂) (c2cauchy (! c₂)))
                  (subst Cauchy (size≡! c₂)
                    (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (scompcauchy
               (scompcauchy
                 (c2cauchy c₂)
                 (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))))
               (subst Cauchy (size≡! c₂)
                 (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁)
                           (scompcauchy
                             x
                             (subst Cauchy (size≡! c₂)
                               (subst Cauchy (size≡! (! c₂))
                                 (c2cauchy (! c₁)))))))
                (linv∼ {t₂} {t₃} {c₂}) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (scompcauchy
               (allFin (size t₂))
               (subst Cauchy (size≡! c₂)
                 (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁) x))
                (scomplid
                  (subst Cauchy (size≡! c₂)
                    (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (subst Cauchy (size≡! c₂)
               (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁) x))
                (subst-trans (size≡! c₂) (size≡! (! c₂))
                  (c2cauchy (! c₁))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁)
             (subst Cauchy (trans (size≡! (! c₂)) (size≡! c₂))
               (c2cauchy (! c₁))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁)
                           (subst Cauchy x (c2cauchy (! c₁)))))
                (trans
                  (cong (λ y → trans y (size≡! c₂)) (size≡!! c₂))
                  (trans-syml (size≡! c₂))) ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁) (c2cauchy (! c₁)))
           ≡⟨ linv∼ {t₁} {t₂} {c₁} ⟩
         c2cauchy {t₁} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {PLUS t₁ t₂} {PLUS t₃ t₄} {c₁ ⊕ c₂} =
  begin (c2cauchy {PLUS t₁ t₂} ((c₁ ⊕ c₂) ◎ ((! c₁) ⊕ (! c₂)))
           ≡⟨ refl ⟩
         scompcauchy
           (pcompcauchy (c2cauchy c₁) (c2cauchy c₂))
           (subst Cauchy (cong₂ _+_ (size≡! c₁) (size≡! c₂))
             (pcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂))))
           ≡⟨ cong
                (scompcauchy (pcompcauchy (c2cauchy c₁) (c2cauchy c₂)))
                (subst₂+
                  (size≡! c₁) (size≡! c₂)
                  (c2cauchy (! c₁)) (c2cauchy (! c₂))
                  pcompcauchy) ⟩
         scompcauchy
           (pcompcauchy (c2cauchy c₁) (c2cauchy c₂))
           (pcompcauchy
             (subst Cauchy (size≡! c₁) (c2cauchy (! c₁)))
             (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))))
           ≡⟨ pcomp-dist
               (c2cauchy c₁)
               (subst Cauchy (size≡! c₁) (c2cauchy (! c₁)))
               (c2cauchy c₂) (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))) ⟩
         pcompcauchy
           (scompcauchy
             (c2cauchy c₁)
             (subst Cauchy (size≡! c₁) (c2cauchy (! c₁))))
           (scompcauchy
             (c2cauchy c₂)
             (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))))
           ≡⟨ cong₂ pcompcauchy (linv∼ {t₁} {t₃} {c₁}) (linv∼ {t₂} {t₄} {c₂}) ⟩
         pcompcauchy (c2cauchy {t₁} id⟷) (c2cauchy {t₂} id⟷)
           ≡⟨ pcomp-id {size t₁} {size t₂} ⟩
         c2cauchy {PLUS t₁ t₂} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {TIMES t₁ t₂} {TIMES t₃ t₄} {c₁ ⊗ c₂} =
  begin (c2cauchy {TIMES t₁ t₂} ((c₁ ⊗ c₂) ◎ ((! c₁) ⊗ (! c₂)))
           ≡⟨ refl ⟩
         scompcauchy
           (tcompcauchy (c2cauchy c₁) (c2cauchy c₂))
           (subst Cauchy (cong₂ _*_ (size≡! c₁) (size≡! c₂))
             (tcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂))))
           ≡⟨ cong
                (scompcauchy (tcompcauchy (c2cauchy c₁) (c2cauchy c₂)))
                (subst₂*
                  (size≡! c₁) (size≡! c₂)
                  (c2cauchy (! c₁)) (c2cauchy (! c₂))
                  tcompcauchy) ⟩
         scompcauchy
           (tcompcauchy (c2cauchy c₁) (c2cauchy c₂))
           (tcompcauchy
             (subst Cauchy (size≡! c₁) (c2cauchy (! c₁)))
             (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))))
           ≡⟨ tcomp-dist
                (c2cauchy c₁)
                (subst Cauchy (size≡! c₁) (c2cauchy (! c₁)))
                (c2cauchy c₂)
                (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))) ⟩
         tcompcauchy
           (scompcauchy
             (c2cauchy c₁)
             (subst Cauchy (size≡! c₁) (c2cauchy (! c₁))))
           (scompcauchy
             (c2cauchy c₂)
             (subst Cauchy (size≡! c₂) (c2cauchy (! c₂))))
           ≡⟨ cong₂ tcompcauchy (linv∼ {t₁} {t₃} {c₁}) (linv∼ {t₂} {t₄} {c₂}) ⟩
         tcompcauchy (c2cauchy {t₁} id⟷) (c2cauchy {t₂} id⟷)
            ≡⟨ tcomp-id {size t₁} {size t₂} ⟩
         c2cauchy {TIMES t₁ t₂} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {PLUS ONE ONE} {BOOL} {foldBool} =
  begin (c2cauchy {PLUS ONE ONE} (foldBool ◎ unfoldBool)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy 2) (idcauchy 2)
           ≡⟨ scomplid (idcauchy 2) ⟩
         c2cauchy {PLUS ONE ONE} id⟷ ∎)
  where open ≡-Reasoning
linv∼ {BOOL} {PLUS ONE ONE} {unfoldBool} =
  begin (c2cauchy {BOOL} (unfoldBool ◎ foldBool)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy 2) (idcauchy 2)
           ≡⟨ scomplid (idcauchy 2) ⟩
         c2cauchy {BOOL} id⟷ ∎)
  where open ≡-Reasoning

rinv∼ : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → ! c ◎ c ∼ id⟷
rinv∼ {PLUS ZERO t} {.t} {unite₊} =
  begin (c2cauchy {t} (uniti₊ ◎ unite₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t)) (idcauchy (size t))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {t} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {t} {PLUS ZERO .t} {uniti₊} =
  begin (c2cauchy {PLUS ZERO t} (unite₊ ◎ uniti₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t)) (idcauchy (size t))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {PLUS ZERO t} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {PLUS t₁ t₂} {PLUS .t₂ .t₁} {swap₊} =
  begin (c2cauchy {PLUS t₂ t₁} (swap₊ ◎ swap₊)
           ≡⟨ refl ⟩
         scompcauchy
           (swap+cauchy (size t₂) (size t₁))
           (subst Cauchy (+-comm (size t₁) (size t₂))
             (swap+cauchy (size t₁) (size t₂)))
           ≡⟨ swap+idemp (size t₂) (size t₁) ⟩
         c2cauchy {PLUS t₂ t₁} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃} {assocl₊} =
  begin (c2cauchy {PLUS (PLUS t₁ t₂) t₃} (assocr₊ ◎ assocl₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) + size t₃))
           (subst Cauchy (sym (+-assoc (size t₁) (size t₂) (size t₃)))
             (idcauchy (size t₁ + (size t₂ + size t₃))))
           ≡⟨ cong
                (scompcauchy (idcauchy ((size t₁ + size t₂) + size t₃)))
                (congD! idcauchy (sym (+-assoc (size t₁) (size t₂) (size t₃)))) ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) + size t₃))
           (idcauchy ((size t₁ + size t₂) + size t₃))
           ≡⟨ scomplid (idcauchy ((size t₁ + size t₂) + size t₃)) ⟩
         c2cauchy {PLUS (PLUS t₁ t₂) t₃} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {PLUS (PLUS t₁ t₂) t₃} {PLUS .t₁ (PLUS .t₂ .t₃)} {assocr₊} =
  begin (c2cauchy {PLUS t₁ (PLUS t₂ t₃)} (assocl₊ ◎ assocr₊)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t₁ + (size t₂ + size t₃)))
           (subst Cauchy (+-assoc (size t₁) (size t₂) (size t₃))
             (idcauchy ((size t₁ + size t₂) + size t₃)))
           ≡⟨ cong
                (scompcauchy (idcauchy (size t₁ + (size t₂ + size t₃))))
                (congD! idcauchy (+-assoc (size t₁) (size t₂) (size t₃))) ⟩
         scompcauchy (idcauchy (size t₁ + (size t₂ + size t₃)))
           (idcauchy (size t₁ + (size t₂ + size t₃)))
           ≡⟨ scomplid (idcauchy (size t₁ + (size t₂ + size t₃))) ⟩
         c2cauchy {PLUS t₁ (PLUS t₂ t₃)} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {TIMES ONE t} {.t} {unite⋆} =
  begin (c2cauchy {t} (uniti⋆ ◎ unite⋆)
           ≡⟨ refl ⟩
         scompcauchy
           (idcauchy (size t))
           (subst Cauchy (+-right-identity (size t))
             (subst Cauchy (sym (+-right-identity (size t)))
               (idcauchy (size t))))
           ≡⟨ cong
                (scompcauchy (idcauchy (size t)))
                (subst-trans
                  (+-right-identity (size t))
                  (sym (+-right-identity (size t)))
                  (idcauchy (size t))) ⟩
         scompcauchy
           (idcauchy (size t))
           (subst Cauchy (trans (sym (+-right-identity (size t)))
                                (+-right-identity (size t)))
               (idcauchy (size t)))
           ≡⟨ cong
                 (λ x → scompcauchy
                          (idcauchy (size t))
                          (subst Cauchy x (idcauchy (size t))))
                 (trans-syml (+-right-identity (size t))) ⟩
         scompcauchy
           (idcauchy (size t))
           (subst Cauchy refl (idcauchy (size t)))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {t} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {t} {TIMES ONE .t} {uniti⋆} =
  begin (c2cauchy {TIMES ONE t} (unite⋆ ◎ uniti⋆)
           ≡⟨ refl ⟩
         scompcauchy
           (subst Cauchy (sym (+-right-identity (size t))) (idcauchy (size t)))
           (subst Cauchy (sym (+-right-identity (size t))) (idcauchy (size t)))
           ≡⟨ cong
                (λ x → scompcauchy x x)
                (congD! idcauchy (sym (+-right-identity (size t)))) ⟩
         scompcauchy (idcauchy (size t + 0)) (idcauchy (size t + 0))
           ≡⟨ scomplid (idcauchy (size t + 0)) ⟩
         c2cauchy {TIMES ONE t} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {TIMES t₁ t₂} {TIMES .t₂ .t₁} {swap⋆} =
  begin (c2cauchy {TIMES t₂ t₁} (swap⋆ ◎ swap⋆)
           ≡⟨ refl ⟩
         scompcauchy
           (swap⋆cauchy (size t₂) (size t₁))
           (subst Cauchy (*-comm (size t₁) (size t₂))
             (swap⋆cauchy (size t₁) (size t₂)))
           ≡⟨ swap⋆idemp (size t₂) (size t₁) ⟩
         c2cauchy {TIMES t₂ t₁} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {TIMES t₁ (TIMES t₂ t₃)} {TIMES (TIMES .t₁ .t₂) .t₃} {assocl⋆} =
  begin (c2cauchy {TIMES (TIMES t₁ t₂) t₃} (assocr⋆ ◎ assocl⋆)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ * size t₂) * size t₃))
           (subst Cauchy (sym (*-assoc (size t₁) (size t₂) (size t₃)))
             (idcauchy (size t₁ * (size t₂ * size t₃))))
           ≡⟨ cong
                (scompcauchy (idcauchy ((size t₁ * size t₂) * size t₃)))
                (congD! idcauchy (sym (*-assoc (size t₁) (size t₂) (size t₃)))) ⟩
         scompcauchy (idcauchy ((size t₁ * size t₂) * size t₃))
           (idcauchy ((size t₁ * size t₂) * size t₃))
           ≡⟨ scomplid (idcauchy ((size t₁ * size t₂) * size t₃)) ⟩
         c2cauchy {TIMES (TIMES t₁ t₂) t₃} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {TIMES (TIMES t₁ t₂) t₃} {TIMES .t₁ (TIMES .t₂ .t₃)} {assocr⋆} =
  begin (c2cauchy {TIMES t₁ (TIMES t₂ t₃)} (assocl⋆ ◎ assocr⋆)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t₁ * (size t₂ * size t₃)))
           (subst Cauchy (*-assoc (size t₁) (size t₂) (size t₃))
             (idcauchy ((size t₁ * size t₂) * size t₃)))
           ≡⟨ cong
                (scompcauchy (idcauchy (size t₁ * (size t₂ * size t₃))))
                (congD! idcauchy (*-assoc (size t₁) (size t₂) (size t₃))) ⟩
         scompcauchy (idcauchy (size t₁ * (size t₂ * size t₃)))
           (idcauchy (size t₁ * (size t₂ * size t₃)))
           ≡⟨ scomplid (idcauchy (size t₁ * (size t₂ * size t₃))) ⟩
         c2cauchy {TIMES t₁ (TIMES t₂ t₃)} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {TIMES ZERO t} {ZERO} {distz} = refl
rinv∼ {ZERO} {TIMES ZERO t} {factorz} = refl
rinv∼ {TIMES (PLUS t₁ t₂) t₃} {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)} {dist} =
  begin (c2cauchy {PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)} (factor ◎ dist)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃)))
           (subst Cauchy (distribʳ-*-+ (size t₃) (size t₁) (size t₂))
             (idcauchy ((size t₁ + size t₂) * size t₃)))
           ≡⟨ cong
                (scompcauchy
                  (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))))
                (congD! idcauchy
                  (distribʳ-*-+ (size t₃) (size t₁) (size t₂))) ⟩
         scompcauchy (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃)))
           (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃)))
           ≡⟨ scomplid (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))) ⟩
         c2cauchy {PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {PLUS (TIMES t₁ t₃) (TIMES t₂ .t₃)} {TIMES (PLUS .t₁ .t₂) .t₃} {factor} =
  begin (c2cauchy {TIMES (PLUS t₁ t₂) t₃} (dist ◎ factor)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) * size t₃))
           (subst Cauchy (sym (distribʳ-*-+ (size t₃) (size t₁) (size t₂)))
             (idcauchy ((size t₁ * size t₃) + (size t₂ * size t₃))))
           ≡⟨ cong
                (scompcauchy (idcauchy ((size t₁ + size t₂) * size t₃)))
                (congD! idcauchy
                  (sym (distribʳ-*-+ (size t₃) (size t₁) (size t₂)))) ⟩
         scompcauchy (idcauchy ((size t₁ + size t₂) * size t₃))
           (idcauchy ((size t₁ + size t₂) * size t₃))
           ≡⟨ scomplid (idcauchy ((size t₁ + size t₂) * size t₃)) ⟩
         c2cauchy {TIMES (PLUS t₁ t₂) t₃} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {t} {.t} {id⟷} =
  begin (c2cauchy {t} (id⟷ ◎ id⟷)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy (size t)) (idcauchy (size t))
           ≡⟨ scomplid (idcauchy (size t)) ⟩
         c2cauchy {t} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {t₁} {t₃} {_◎_ {t₂ = t₂} c₁ c₂} =
  begin (c2cauchy {t₃} (((! c₂) ◎ (! c₁)) ◎ (c₁ ◎ c₂))
           ≡⟨ refl ⟩
         scompcauchy
           (scompcauchy
              (c2cauchy (! c₂))
              (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁))))
           (subst Cauchy (trans (size≡! (! c₁)) (size≡! (! c₂)))
             (scompcauchy
               (c2cauchy c₁)
               (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))
           ≡⟨ sym (scompassoc
                     (c2cauchy (! c₂))
                     (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))
                     (subst Cauchy (trans (size≡! (! c₁)) (size≡! (! c₂)))
                       (scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (scompcauchy
              (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))
              (subst Cauchy (trans (size≡! (! c₁)) (size≡! (! c₂)))
                (scompcauchy
                  (c2cauchy c₁)
                  (subst Cauchy (size≡! c₁) (c2cauchy  c₂)))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (scompcauchy
                           (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))
                           x))
                (sym (subst-trans (size≡! (! c₂)) (size≡! (! c₁))
                       (scompcauchy
                         (c2cauchy c₁)
                         (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (scompcauchy
              (subst Cauchy (size≡! (! c₂)) (c2cauchy (! c₁)))
              (subst Cauchy (size≡! (! c₂))
                (subst Cauchy (size≡! (! c₁))
                  (scompcauchy
                    (c2cauchy c₁)
                    (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))))
           ≡⟨ cong
                (scompcauchy (c2cauchy (! c₂)))
                (sym (subst-dist scompcauchy (size≡! (! c₂))
                       (c2cauchy (! c₁))
                       (subst Cauchy (size≡! (! c₁))
                         (scompcauchy
                           (c2cauchy c₁)
                           (subst Cauchy (size≡! c₁) (c2cauchy c₂)))))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂))
             (scompcauchy
               (c2cauchy (! c₁))
               (subst Cauchy (size≡! (! c₁))
                 (scompcauchy
                   (c2cauchy c₁)
                   (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂))
                           (scompcauchy (c2cauchy (! c₁)) x)))
                (subst-dist scompcauchy (size≡! (! c₁))
                  (c2cauchy c₁)
                  (subst Cauchy (size≡! c₁) (c2cauchy  c₂))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂))
             (scompcauchy
               (c2cauchy (! c₁))
                 (scompcauchy
                   (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁))
                   (subst Cauchy (size≡! (! c₁))
                     (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂)) x))
                (scompassoc
                  (c2cauchy (! c₁))
                  (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁))
                  (subst Cauchy (size≡! (! c₁))
                    (subst Cauchy (size≡! c₁) (c2cauchy  c₂)))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂))
             (scompcauchy
               (scompcauchy
                 (c2cauchy (! c₁))
                 (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁)))
               (subst Cauchy (size≡! (! c₁))
                 (subst Cauchy (size≡! c₁) (c2cauchy  c₂)))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂))
                           (scompcauchy
                             x
                             (subst Cauchy (size≡! (! c₁))
                               (subst Cauchy (size≡! c₁) (c2cauchy  c₂))))))
                (rinv∼ {t₁} {t₂} {c₁}) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂))
             (scompcauchy
               (allFin (size t₂))
               (subst Cauchy (size≡! (! c₁))
                 (subst Cauchy (size≡! c₁) (c2cauchy  c₂)))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂)) x))
                (scomplid
                  (subst Cauchy (size≡! (! c₁))
                    (subst Cauchy (size≡! c₁) (c2cauchy  c₂)))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂))
             (subst Cauchy (size≡! (! c₁))
               (subst Cauchy (size≡! c₁) (c2cauchy c₂))))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂)) x))
                (subst-trans (size≡! (! c₁)) (size≡! c₁) (c2cauchy c₂)) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂))
             (subst Cauchy (trans (size≡! c₁) (size≡! (! c₁)))
               (c2cauchy c₂)))
           ≡⟨ cong
                (λ x → scompcauchy
                         (c2cauchy (! c₂))
                         (subst Cauchy (size≡! (! c₂))
                           (subst Cauchy x (c2cauchy c₂))))
                (trans
                  (cong (λ y → trans (size≡! c₁) y) (size≡!! c₁))
                  (trans-symr (size≡! c₁))) ⟩
         scompcauchy
           (c2cauchy (! c₂))
           (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂))
           ≡⟨ rinv∼ {t₂} {t₃} {c₂} ⟩
         c2cauchy {t₃} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {PLUS t₁ t₂} {PLUS t₃ t₄} {c₁ ⊕ c₂} =
  begin (c2cauchy {PLUS t₃ t₄} (((! c₁) ⊕ (! c₂)) ◎ (c₁ ⊕ c₂))
           ≡⟨ refl ⟩
         scompcauchy
           (pcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂)))
           (subst Cauchy (cong₂ _+_ (size≡! (! c₁)) (size≡! (! c₂)))
             (pcompcauchy (c2cauchy c₁) (c2cauchy c₂)))
           ≡⟨ cong
                (scompcauchy (pcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂))))
                (subst₂+
                  (size≡! (! c₁)) (size≡! (! c₂))
                  (c2cauchy c₁) (c2cauchy c₂)
                  pcompcauchy) ⟩
         scompcauchy
           (pcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂)))
           (pcompcauchy
             (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁))
             (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂)))
           ≡⟨ pcomp-dist
               (c2cauchy (! c₁))
               (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁))
               (c2cauchy (! c₂)) (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂)) ⟩
         pcompcauchy
           (scompcauchy
             (c2cauchy (! c₁))
             (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁)))
           (scompcauchy
             (c2cauchy (! c₂))
             (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂)))
           ≡⟨ cong₂ pcompcauchy (rinv∼ {t₁} {t₃} {c₁}) (rinv∼ {t₂} {t₄} {c₂}) ⟩
         pcompcauchy (c2cauchy {t₃} id⟷) (c2cauchy {t₄} id⟷)
           ≡⟨ pcomp-id {size t₃} {size t₄} ⟩
         c2cauchy {PLUS t₃ t₄} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {TIMES t₁ t₂} {TIMES t₃ t₄} {c₁ ⊗ c₂} =
  begin (c2cauchy {TIMES t₃ t₄} (((! c₁) ⊗ (! c₂)) ◎ (c₁ ⊗ c₂))
           ≡⟨ refl ⟩
         scompcauchy
           (tcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂)))
           (subst Cauchy (cong₂ _*_ (size≡! (! c₁)) (size≡! (! c₂)))
             (tcompcauchy (c2cauchy c₁) (c2cauchy c₂)))
           ≡⟨ cong
                (scompcauchy (tcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂))))
                (subst₂*
                  (size≡! (! c₁)) (size≡! (! c₂))
                  (c2cauchy c₁) (c2cauchy c₂)
                  tcompcauchy) ⟩
         scompcauchy
           (tcompcauchy (c2cauchy (! c₁)) (c2cauchy (! c₂)))
           (tcompcauchy
             (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁))
             (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂)))
           ≡⟨ tcomp-dist
                (c2cauchy (! c₁))
                (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁))
                (c2cauchy (! c₂))
                (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂)) ⟩
         tcompcauchy
           (scompcauchy
             (c2cauchy (! c₁))
             (subst Cauchy (size≡! (! c₁)) (c2cauchy c₁)))
           (scompcauchy
             (c2cauchy (! c₂))
             (subst Cauchy (size≡! (! c₂)) (c2cauchy c₂)))
           ≡⟨ cong₂ tcompcauchy (rinv∼ {t₁} {t₃} {c₁}) (rinv∼ {t₂} {t₄} {c₂}) ⟩
         tcompcauchy (c2cauchy {t₃} id⟷) (c2cauchy {t₄} id⟷)
            ≡⟨ tcomp-id {size t₃} {size t₄} ⟩
         c2cauchy {TIMES t₃ t₄} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {PLUS ONE ONE} {BOOL} {foldBool} =
  begin (c2cauchy {BOOL} (unfoldBool ◎ foldBool)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy 2) (idcauchy 2)
           ≡⟨ scomplid (idcauchy 2) ⟩
         c2cauchy {BOOL} id⟷ ∎)
  where open ≡-Reasoning
rinv∼ {BOOL} {PLUS ONE ONE} {unfoldBool} =
  begin (c2cauchy {PLUS ONE ONE} (foldBool ◎ unfoldBool)
           ≡⟨ refl ⟩
         scompcauchy (idcauchy 2) (idcauchy 2)
           ≡⟨ scomplid (idcauchy 2) ⟩
         c2cauchy {PLUS ONE ONE} id⟷ ∎)
  where open ≡-Reasoning

resp∼ : {t₁ t₂ t₃ : U} {c₁ c₂ : t₁ ⟷ t₂} {c₃ c₄ : t₂ ⟷ t₃} →
        (c₁ ∼ c₂) → (c₃ ∼ c₄) → (c₁ ◎ c₃ ∼ c₂ ◎ c₄)
resp∼ {t₁} {t₂} {t₃} {c₁} {c₂} {c₃} {c₄} c₁∼c₂ c₃∼c₄ =
  begin (c2cauchy (c₁ ◎ c₃)
           ≡⟨ refl ⟩
         scompcauchy
           (c2cauchy c₁)
           (subst Cauchy (size≡! c₁) (c2cauchy c₃))
           ≡⟨ cong₂
                (λ x y → scompcauchy x (subst Cauchy (size≡! c₁) y))
                c₁∼c₂ c₃∼c₄ ⟩
         scompcauchy
           (c2cauchy c₂)
           (subst Cauchy (size≡! c₁) (c2cauchy c₄))
           ≡⟨ cong
                (λ x → scompcauchy (c2cauchy c₂) (subst Cauchy x (c2cauchy c₄)))
                (size∼! c₁ c₂) ⟩
         scompcauchy
           (c2cauchy c₂)
           (subst Cauchy (size≡! c₂) (c2cauchy c₄))
           ≡⟨ refl ⟩
         c2cauchy (c₂ ◎ c₄) ∎)
  where open ≡-Reasoning

-- The equivalence ∼ of paths makes U a 1groupoid: the points are
-- types (t : U); the 1paths are ⟷; and the 2paths between them are
-- based on extensional equivalence ∼

G : 1Groupoid
G = record
        { set = U
        ; _↝_ = _⟷_
        ; _≈_ = _∼_
        ; id  = id⟷
        ; _∘_ = λ p q → q ◎ p
        ; _⁻¹ = !
        ; lneutr = λ c → c◎id∼c {c = c}
        ; rneutr = λ c → id◎c∼c {c = c}
        ; assoc  = λ c₃ c₂ c₁ → assoc∼ {c₁ = c₁} {c₂ = c₂} {c₃ = c₃}
        ; equiv = record {
            refl  = λ {c} → refl∼ {c = c}
          ; sym   = λ {c₁} {c₂} → sym∼ {c₁ = c₁} {c₂ = c₂}
          ; trans = λ {c₁} {c₂} {c₃} → trans∼ {c₁ = c₁} {c₂ = c₂} {c₃ = c₃}
          }
        ; linv = λ c → linv∼ {c = c}
        ; rinv = λ c → rinv∼ {c = c}
        ; ∘-resp-≈ = λ {t₁} {t₂} {t₃} {p} {q} {r} {s} p∼q r∼s →
                    resp∼ {t₁} {t₂} {t₃} {r} {s} {p} {q} r∼s p∼q
        }

-- There are additional laws that should hold:
--
-- assoc⊕∼ : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
--           {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
--           c₁ ⊕ (c₂ ⊕ c₃) ∼ assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊
--
-- assoc⊗∼ : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
--           {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
--           c₁ ⊗ (c₂ ⊗ c₃) ∼ assocl⋆ ◎ ((c₁ ⊗ c₂) ⊗ c₃) ◎ assocr⋆
--
-- but we will turn our attention to completeness below (in Pif2) in a more
-- systematic way.

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Agda.Builtin.Cubical.Path

data D : Set where
  c : (@0 x y : D) → x ≡ y

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-

Axiom of Finite Choice
- Yep, it's a theorem actually.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.FiniteChoice where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)

open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Data.SumFin
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties

private
  variable
    ℓ ℓ' : Level

choice≃Fin :
  {n : ℕ}(Y : Fin n → Type ℓ) → ((x : Fin n) → ∥ Y x ∥) ≃ ∥ ((x : Fin n) → Y x) ∥
choice≃Fin {n = 0} Y =
    isContr→≃Unit (isContrΠ⊥)
  ⋆ Unit≃Unit*
  ⋆ invEquiv (propTruncIdempotent≃ isPropUnit*)
  ⋆ propTrunc≃ (invEquiv (isContr→≃Unit* (isContrΠ⊥ {A = Y})))
choice≃Fin {n = suc n} Y =
    Π⊎≃
  ⋆ Σ-cong-equiv-fst (ΠUnit (λ x → ∥ Y (inl x) ∥))
  ⋆ Σ-cong-equiv-snd (λ _ → choice≃Fin {n = n} (λ x → Y (inr x)))
  ⋆ Σ-cong-equiv-fst (propTrunc≃ (invEquiv (ΠUnit (λ x → Y (inl x)))))
  ⋆ ∥∥-×-≃
  ⋆ propTrunc≃ (invEquiv (Π⊎≃ {E = Y}))

module _
  (X : Type ℓ)(p : isFinOrd X)
  (Y : X → Type ℓ') where

  private
    e = p .snd

  choice≃' : ((x : X) → ∥ Y x ∥) ≃ ∥ ((x : X) → Y x) ∥
  choice≃' =
      equivΠ {B' = λ x → ∥ Y (invEq e x) ∥} e (transpFamily p)
    ⋆ choice≃Fin _
    ⋆ propTrunc≃ (invEquiv (equivΠ {B' = λ x → Y (invEq e x)} e (transpFamily p)))

module _
  (X : FinSet ℓ)
  (Y : X .fst → Type ℓ') where

  choice≃ : ((x : X .fst) → ∥ Y x ∥) ≃ ∥ ((x : X .fst) → Y x) ∥
  choice≃ =
    Prop.rec
      (isOfHLevel≃ 1 (isPropΠ (λ x → isPropPropTrunc)) isPropPropTrunc)
      (λ p → choice≃' (X .fst) (_ , p) Y) (X .snd .snd)

  choice : ((x : X .fst) → ∥ Y x ∥) → ∥ ((x : X .fst) → Y x) ∥
  choice = choice≃ .fst

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module CS410-Monoid where

open import CS410-Prelude

record Monoid (M : Set) : Set where
  field
    -- OPERATIONS ----------------------------------------
    e     : M
    op    : M -> M -> M
    -- LAWS ----------------------------------------------
    lunit : forall m -> op e m == m
    runit : forall m -> op m e == m
    assoc : forall m m' m'' ->
              op m (op m' m'') == op (op m m') m''


text:
------------------------------------------------------------------------
-- A combinator for running two computations in parallel
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Delay-monad.Parallel where

import Equality.Propositional as Eq
open import Prelude
open import Prelude.Size

open import Conat Eq.equality-with-J as Conat
  using (zero; suc; force; max)

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Bisimilarity.Kind
open import Delay-monad.Monad
import Delay-monad.Sequential as S

private

  variable
    a b             : Level
    A B             : Type a
    i               : Size
    k               : Kind
    f f₁ f₂ g       : Delay (A → B) ∞
    x x₁ x₂ y y₁ y₂ : Delay A ∞
    f′              : Delay′ (A → B) ∞
    x′              : Delay′ A ∞
    h               : A → B
    z               : A

------------------------------------------------------------------------
-- The _⊛_ operator

-- Parallel composition of computations.

infixl 6 _⊛_

_⊛_ : Delay (A → B) i → Delay A i → Delay B i
now f   ⊛ now x   = now (f x)
now f   ⊛ later x = later λ { .force → now f ⊛ x .force }
later f ⊛ now x   = later λ { .force → f .force ⊛ now x }
later f ⊛ later x = later λ { .force → f .force ⊛ x .force }

-- The number of later constructors in f ⊛ x is bisimilar to the
-- maximum of the number of later constructors in f and the number of
-- later constructors in x.

steps-⊛∼max-steps-steps :
  Conat.[ i ] steps (f ⊛ x) ∼ max (steps f) (steps x)
steps-⊛∼max-steps-steps {f = now _}   {x = now _}   = zero
steps-⊛∼max-steps-steps {f = now _}   {x = later _} = suc λ { .force → steps-⊛∼max-steps-steps }
steps-⊛∼max-steps-steps {f = later _} {x = now _}   = suc λ { .force → steps-⊛∼max-steps-steps }
steps-⊛∼max-steps-steps {f = later _} {x = later _} = suc λ { .force → steps-⊛∼max-steps-steps }

-- Rearrangement lemmas for _⊛_.

later-⊛ :
  later f′ ⊛ x ∼ later (record { force = f′ .force ⊛ drop-later x })
later-⊛ {x = now _}   = later λ { .force → _ ∎ }
later-⊛ {x = later _} = later λ { .force → _ ∎ }

⊛-later :
  f ⊛ later x′ ∼ later (record { force = drop-later f ⊛ x′ .force })
⊛-later {f = now _}   = later λ { .force → _ ∎ }
⊛-later {f = later _} = later λ { .force → _ ∎ }

-- The _⊛_ operator preserves strong and weak bisimilarity and
-- expansion.

infixl 6 _⊛-cong_

_⊛-cong_ :
  [ i ] f₁ ⟨ k ⟩ f₂ →
  [ i ] x₁ ⟨ k ⟩ x₂ →
  [ i ] f₁ ⊛ x₁ ⟨ k ⟩ f₂ ⊛ x₂
now      ⊛-cong now      = now
now      ⊛-cong later  q = later λ { .force → now ⊛-cong q .force }
now      ⊛-cong laterˡ q = laterˡ (now ⊛-cong q)
now      ⊛-cong laterʳ q = laterʳ (now ⊛-cong q)
later  p ⊛-cong now      = later λ { .force → p .force ⊛-cong now }
laterˡ p ⊛-cong now      = laterˡ (p ⊛-cong now)
laterʳ p ⊛-cong now      = laterʳ (p ⊛-cong now)

later  p ⊛-cong later  q = later λ { .force → p .force ⊛-cong q .force }
laterʳ p ⊛-cong laterʳ q = laterʳ (p ⊛-cong q)
laterˡ p ⊛-cong laterˡ q = laterˡ (p ⊛-cong q)

later {x = f₁} {y = f₂} p ⊛-cong laterˡ {x = x₁} {y = x₂} q =
  later f₁ ⊛ later x₁                                   ∼⟨ (later λ { .force → _ ∎ }) ⟩
  later (record { force = f₁ .force ⊛ x₁ .force })      ?⟨ (later λ { .force → p .force ⊛-cong drop-laterʳ q }) ⟩∼
  later (record { force = f₂ .force ⊛ drop-later x₂ })  ∼⟨ symmetric later-⊛ ⟩
  later f₂ ⊛ x₂                                         ∎

later {x = f₁} {y = f₂} p ⊛-cong laterʳ {x = x₁} {y = x₂} q =
  later f₁ ⊛ x₁                                         ∼⟨ later-⊛ ⟩
  later (record { force = f₁ .force ⊛ drop-later x₁ })  ≈⟨ (later λ { .force → p .force ⊛-cong drop-laterˡ q }) ⟩∼
  later (record { force = f₂ .force ⊛ x₂ .force })      ∼⟨ (later λ { .force → _ ∎ }) ⟩
  later f₂ ⊛ later x₂                                   ∎

laterˡ {x = f₁} {y = f₂} p ⊛-cong later {x = x₁} {y = x₂} q =
  later f₁ ⊛ later x₁                                   ∼⟨ (later λ { .force → _ ∎ }) ⟩
  later (record { force = f₁ .force ⊛ x₁ .force })      ?⟨ (later λ { .force → drop-laterʳ p ⊛-cong q .force }) ⟩∼
  later (record { force = drop-later f₂ ⊛ x₂ .force })  ∼⟨ symmetric ⊛-later ⟩
  f₂ ⊛ later x₂                                         ∎

laterʳ {x = f₁} {y = f₂} p ⊛-cong later {x = x₁} {y = x₂} q =
  f₁ ⊛ later x₁                                         ∼⟨ ⊛-later ⟩
  later (record { force = drop-later f₁ ⊛ x₁ .force })  ≈⟨ (later λ { .force → drop-laterˡ p ⊛-cong q .force }) ⟩∼
  later (record { force = f₂ .force ⊛ x₂ .force })      ∼⟨ (later λ { .force → _ ∎ }) ⟩
  later f₂ ⊛ later x₂                                   ∎

laterˡ {x = f₁} {y = f₂} p ⊛-cong laterʳ {x = x₁} {y = x₂} q =
  later f₁ ⊛ x₁                                         ∼⟨ later-⊛ ⟩
  later (record { force = f₁ .force ⊛ drop-later x₁ })  ≈⟨ (later λ { .force → drop-laterʳ p ⊛-cong drop-laterˡ q }) ⟩∼
  later (record { force = drop-later f₂ ⊛ x₂ .force })  ∼⟨ symmetric ⊛-later ⟩
  f₂ ⊛ later x₂                                         ∎

laterʳ {x = f₁} {y = f₂} p ⊛-cong laterˡ {x = x₁} {y = x₂} q =
  f₁ ⊛ later x₁                                         ∼⟨ ⊛-later ⟩
  later (record { force = drop-later f₁ ⊛ x₁ .force })  ≈⟨ (later λ { .force → drop-laterˡ p ⊛-cong drop-laterʳ q }) ⟩∼
  later (record { force = f₂ .force ⊛ drop-later x₂ })  ∼⟨ symmetric later-⊛ ⟩
  later f₂ ⊛ x₂                                         ∎

-- The _⊛_ operator is (kind of) commutative.

⊛-comm : [ i ] f ⊛ x ∼ map′ (flip _$_) x ⊛ f
⊛-comm {f = now f}   {x = now x}   = reflexive _
⊛-comm {f = now f}   {x = later x} = later λ { .force → ⊛-comm }
⊛-comm {f = later f} {x = now x}   = later λ { .force → ⊛-comm }
⊛-comm {f = later f} {x = later x} = later λ { .force → ⊛-comm }

-- The function map′ can be expressed using _⊛_.

map∼now-⊛ : [ i ] map′ h x ∼ now h ⊛ x
map∼now-⊛ {x = now x}   = now
map∼now-⊛ {x = later x} = later λ { .force → map∼now-⊛ }

-- The applicative functor laws hold up to strong bisimilarity.

now-id-⊛ : [ i ] now id ⊛ x ∼ x
now-id-⊛ {x = now x}   = now
now-id-⊛ {x = later x} = later λ { .force → now-id-⊛ }

now-∘-⊛-⊛-⊛ :
  [ i ] now (λ f → f ∘_) ⊛ f ⊛ g ⊛ x ∼ f ⊛ (g ⊛ x)
now-∘-⊛-⊛-⊛ {f = now _}   {g = now _}   {x = now _}   = now
now-∘-⊛-⊛-⊛ {f = now _}   {g = now _}   {x = later _} = later λ { .force → now-∘-⊛-⊛-⊛ }
now-∘-⊛-⊛-⊛ {f = now _}   {g = later _} {x = now _}   = later λ { .force → now-∘-⊛-⊛-⊛ }
now-∘-⊛-⊛-⊛ {f = now _}   {g = later _} {x = later _} = later λ { .force → now-∘-⊛-⊛-⊛ }
now-∘-⊛-⊛-⊛ {f = later _} {g = now _}   {x = now _}   = later λ { .force → now-∘-⊛-⊛-⊛ }
now-∘-⊛-⊛-⊛ {f = later _} {g = now _}   {x = later _} = later λ { .force → now-∘-⊛-⊛-⊛ }
now-∘-⊛-⊛-⊛ {f = later _} {g = later _} {x = now _}   = later λ { .force → now-∘-⊛-⊛-⊛ }
now-∘-⊛-⊛-⊛ {f = later _} {g = later _} {x = later _} = later λ { .force → now-∘-⊛-⊛-⊛ }

now-⊛-now : [ i ] now h ⊛ now z ∼ now (h z)
now-⊛-now = now

⊛-now : [ i ] f ⊛ now z ∼ now (λ f → f z) ⊛ f
⊛-now {f = now f}   = now
⊛-now {f = later f} = later λ { .force → ⊛-now }

-- Sequential composition is an expansion of parallel composition.

⊛≳⊛ : [ i ] f S.⊛ x ≳ f ⊛ x
⊛≳⊛ {f = now f} {x = now x}   = now (f x)  ∎
⊛≳⊛ {f = now f} {x = later x} = later λ { .force →
  now f S.⊛ x .force  ≳⟨ ⊛≳⊛ ⟩∎
  now f ⊛ x .force    ∎ }
⊛≳⊛ {f = later f} {x = now x} = later λ { .force →
  f .force S.⊛ now x  ≳⟨ ⊛≳⊛ ⟩∎
  f .force ⊛ now x    ∎ }
⊛≳⊛ {f = later f} {x = later x} = later λ { .force →
  f .force S.⊛ later x   ≳⟨ ((f .force ∎) >>=-cong λ _ → laterˡ (_ ∎)) ⟩
  f .force S.⊛ x .force  ≳⟨ ⊛≳⊛ ⟩∎
  f .force ⊛ x .force    ∎ }

------------------------------------------------------------------------
-- The _∣_ operator

-- Parallel composition of computations.

infix 10 _∣_

_∣_ : Delay A i → Delay B i → Delay (A × B) i
x ∣ y = map′ _,_ x ⊛ y

-- The number of later constructors in x ∣ y is bisimilar to the
-- maximum of the number of later constructors in x and the number of
-- later constructors in y.

steps-∣∼max-steps-steps :
  Conat.[ i ] steps (x ∣ y) ∼ max (steps x) (steps y)
steps-∣∼max-steps-steps {x = x} {y = y} =
  steps (x ∣ y)                       Conat.∼⟨ Conat.reflexive-∼ _ ⟩
  steps (map′ _,_ x ⊛ y)              Conat.∼⟨ steps-⊛∼max-steps-steps ⟩
  max (steps (map′ _,_ x)) (steps y)  Conat.∼⟨ Conat.max-cong (steps-map′ x) (Conat.reflexive-∼ _) ⟩∎
  max (steps x) (steps y)             ∎∼

-- The _∣_ operator preserves strong and weak bisimilarity and
-- expansion.

infix 10 _∣-cong_

_∣-cong_ :
  [ i ] x₁ ⟨ k ⟩ x₂ →
  [ i ] y₁ ⟨ k ⟩ y₂ →
  [ i ] x₁ ∣ y₁ ⟨ k ⟩ x₂ ∣ y₂
p ∣-cong q = map-cong _,_ p ⊛-cong q

-- The _∣_ operator is commutative (up to swapping of results).

∣-comm : [ i ] x ∣ y ∼ map′ swap (y ∣ x)
∣-comm {x = x} {y = y} =
  x ∣ y                                                          ∼⟨⟩
  map′ _,_ x ⊛ y                                                 ∼⟨ ⊛-comm ⟩
  map′ (flip _$_) y ⊛ map′ _,_ x                                 ∼⟨ map∼now-⊛ ⊛-cong map∼now-⊛ ⟩
  now (flip _$_) ⊛ y ⊛ (now _,_ ⊛ x)                             ∼⟨ symmetric now-∘-⊛-⊛-⊛ ⟩
  now (λ f → f ∘_) ⊛ (now (flip _$_) ⊛ y) ⊛ now _,_ ⊛ x          ∼⟨ symmetric now-∘-⊛-⊛-⊛ ⊛-cong (_ ∎) ⊛-cong (_ ∎) ⟩
  now _∘_ ⊛ now (λ f → f ∘_) ⊛ now (flip _$_) ⊛ y ⊛ now _,_ ⊛ x  ∼⟨⟩
  now (λ x f y → f y x) ⊛ y ⊛ now _,_ ⊛ x                        ∼⟨ ⊛-now ⊛-cong (_ ∎) ⟩
  now (_$ _,_) ⊛ (now (λ x f y → f y x) ⊛ y) ⊛ x                 ∼⟨ symmetric now-∘-⊛-⊛-⊛ ⊛-cong (_ ∎) ⟩
  now _∘_ ⊛ now (_$ _,_) ⊛ now (λ x f y → f y x) ⊛ y ⊛ x         ∼⟨⟩
  now (curry swap) ⊛ y ⊛ x                                       ∼⟨⟩
  now _∘_ ⊛ now (swap ∘_) ⊛ now _,_ ⊛ y ⊛ x                      ∼⟨ now-∘-⊛-⊛-⊛ ⊛-cong (_ ∎) ⟩
  now (swap ∘_) ⊛ (now _,_ ⊛ y) ⊛ x                              ∼⟨ (_ ∎) ⊛-cong symmetric map∼now-⊛ ⊛-cong (_ ∎) ⟩
  now (swap ∘_) ⊛ map′ _,_ y ⊛ x                                 ∼⟨⟩
  now _∘_ ⊛ now swap ⊛ map′ _,_ y ⊛ x                            ∼⟨ now-∘-⊛-⊛-⊛ ⟩
  now swap ⊛ (map′ _,_ y ⊛ x)                                    ∼⟨ symmetric map∼now-⊛ ⟩
  map′ swap (map′ _,_ y ⊛ x)                                     ∼⟨⟩
  map′ swap (y ∣ x)                                              ∎

-- Sequential composition is an expansion of parallel composition.

∣≳∣ : [ i ] x S.∣ y ≳ x ∣ y
∣≳∣ {x = x} {y = y} =
  x S.∣ y           ∼⟨⟩
  map′ _,_ x S.⊛ y  ≳⟨ ⊛≳⊛ ⟩
  map′ _,_ x ⊛ y    ∼⟨⟩
  x ∣ y             ∎

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-# OPTIONS --allow-exec #-}

open import Agda.Builtin.FromNat

open import Data.Bool.Base using (T; Bool; if_then_else_)
open import Data.String using (String; _++_; lines)
open import Data.Nat.Base using (ℕ)
open import Data.Fin using (Fin)
import Data.Fin.Literals as Fin
import Data.Nat.Literals as Nat
open import Data.Vec.Base using (Vec)
open import Data.Float.Base using (Float; _≤ᵇ_)
open import Data.List.Base using (List; []; _∷_)
open import Data.Unit.Base using (⊤; tt)
open import Relation.Nullary using (does)
open import Relation.Binary.Core using (Rel)

open import Reflection.Argument
open import Reflection.Term
open import Reflection.External
open import Reflection.TypeChecking.Monad
open import Reflection.TypeChecking.Monad.Syntax
open import Reflection.Show using (showTerm)

open import Vehicle.Utils

module Vehicle where

------------------------------------------------------------------------
-- Metadata
------------------------------------------------------------------------

VEHICLE_COMMAND : String
VEHICLE_COMMAND = "vehicle"

------------------------------------------------------------------------
-- Checking
------------------------------------------------------------------------

record CheckArgs : Set where
  field
    proofCache : String

checkCmd : CheckArgs → CmdSpec
checkCmd checkArgs = cmdSpec VEHICLE_COMMAND
  ( "check"
  ∷ ("--proofCache=" ++ proofCache)
  ∷ []) ""
  where open CheckArgs checkArgs

checkSuccessful : String → Bool
checkSuccessful output = "verified" ⊆ output

postulate valid : ∀ {a} {A : Set a} → A

`valid : Term
`valid = def (quote valid) (hArg unknown ∷ [])

checkSpecificationMacro : CheckArgs → Term → TC ⊤
checkSpecificationMacro args hole = do
  goal   ← inferType hole
  -- (showTerm goal)
  output ← runCmdTC (checkCmd args)
  if checkSuccessful output
    then unify hole `valid
    else typeError (strErr ("Error: " ++ output) ∷ [])

macro
  checkSpecification : CheckArgs → Term → TC ⊤
  checkSpecification = checkSpecificationMacro

------------------------------------------------------------------------
-- Other
------------------------------------------------------------------------

instance
  finNumber : ∀ {n} -> Number (Fin n)
  finNumber {n} = Fin.number n

  natNumber : Number ℕ
  natNumber = Nat.number

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module Theory where

open import Data.List using (List; []; _∷_; _++_)
open import Data.Fin using () renaming (zero to fzero; suc to fsuc)

open import Relation.Binary using (Rel)

open import Level using (suc; _⊔_)

open import Syntax

record Theory ℓ₁ ℓ₂ ℓ₃ : Set (suc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  field
    Sg : Signature ℓ₁ ℓ₂

  open Signature Sg
  open Term Sg

  field
    Ax : forall Γ A -> Rel (Γ ⊢ A) ℓ₃

  infix 3 _⊢_≡_
  infix 3 _⊨_≡_

  data _⊢_≡_ : forall Γ {A} -> Γ ⊢ A -> Γ ⊢ A -> Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
  data _⊨_≡_ : forall Γ {Γ′} -> Γ ⊨ Γ′ -> Γ ⊨ Γ′ -> Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)

  -- Theorems
  data _⊢_≡_ where
    ax : forall {Γ A e₁ e₂} -> Ax Γ A e₁ e₂ -> Γ ⊢ e₁ ≡ e₂

    refl : forall {Γ} {A} {e : Γ ⊢ A} -> Γ ⊢ e ≡ e
    sym : forall {Γ} {A} {e₁ : Γ ⊢ A} {e₂} -> Γ ⊢ e₁ ≡ e₂ -> Γ ⊢ e₂ ≡ e₁
    trans : forall {Γ} {A} {e₁ : Γ ⊢ A} {e₂ e₃} -> Γ ⊢ e₁ ≡ e₂ -> Γ ⊢ e₂ ≡ e₃ -> Γ ⊢ e₁ ≡ e₃

    sub/id : forall {Γ} {A} {e : Γ ⊢ A} -> Γ ⊢ e [ id ] ≡ e
    sub/∙ : forall {Γ} {A} {Γ′ Γ′′} {e : Γ′′ ⊢ A} {γ : Γ′ ⊨ Γ′′} {δ}
      -> Γ ⊢ e [ γ ∙ δ ] ≡ e [ γ ] [ δ ]

    eta/Unit : forall {Γ} (e : Γ ⊢ Unit) -> Γ ⊢ unit ≡ e

    beta/*₁ : forall {Γ} {A B} (e₁ : Γ ⊢ A) (e₂ : Γ ⊢ B) -> Γ ⊢ fst (pair e₁ e₂) ≡ e₁
    beta/*₂ : forall {Γ} {A B} (e₁ : Γ ⊢ A) (e₂ : Γ ⊢ B) -> Γ ⊢ snd (pair e₁ e₂) ≡ e₂
    eta/* : forall {Γ} {A B} (e : Γ ⊢ A * B) -> Γ ⊢ pair (fst e) (snd e) ≡ e

    beta/=> : forall {Γ} {A B} (e : A ∷ Γ ⊢ B) (e′ : Γ ⊢ A) -> Γ ⊢ app (abs e) e′ ≡ e [ ext id e′ ]
    eta/=> : forall {Γ} {A B} (e : Γ ⊢ A => B) -> Γ ⊢ abs (app (e [ weaken ]) var) ≡ e

    -- cong
    cong/func : forall {Γ} {f : Func} {e e′ : Γ ⊢ dom f}
      -> Γ ⊢ e ≡ e′
      -> Γ ⊢ func f e ≡ func f e′
    cong/sub : forall {Γ Γ′} {γ γ′ : Γ ⊨ Γ′} {A} {e e′ : Γ′ ⊢ A}
      -> Γ ⊨ γ ≡ γ′
      -> Γ′ ⊢ e ≡ e′
      -> Γ ⊢ e [ γ ] ≡ e′ [ γ′ ]
    cong/pair : forall {Γ} {A B} {e₁ e₁′ : Γ ⊢ A} {e₂ e₂′ : Γ ⊢ B}
      -> Γ ⊢ e₁ ≡ e₁′
      -> Γ ⊢ e₂ ≡ e₂′
      -> Γ ⊢ pair e₁ e₂ ≡ pair e₁′ e₂′
    cong/fst : forall {Γ} {A B} {e e′ : Γ ⊢ A * B}
      -> Γ ⊢ e ≡ e′
      -> Γ ⊢ fst e ≡ fst e′
    cong/snd : forall {Γ} {A B} {e e′ : Γ ⊢ A * B}
      -> Γ ⊢ e ≡ e′
      -> Γ ⊢ snd e ≡ snd e′
    cong/abs : forall {Γ} {A B} {e e′ : A ∷ Γ ⊢ B}
      -> A ∷ Γ ⊢ e ≡ e′
      -> Γ ⊢ abs e ≡ abs e′
    cong/app : forall {Γ} {A B} {e₁ e₁′ : Γ ⊢ A => B} {e₂ e₂′ : Γ ⊢ A}
      -> Γ ⊢ e₁ ≡ e₁′
      -> Γ ⊢ e₂ ≡ e₂′
      -> Γ ⊢ app e₁ e₂ ≡ app e₁′ e₂′

    -- subst commutes with term formers
    comm/func : forall Γ Γ′ (γ : Γ ⊨ Γ′) f e
      -> Γ ⊢ func f e [ γ ] ≡ func f (e [ γ ])

    comm/unit : forall Γ Γ′ (γ : Γ ⊨ Γ′)
      -> Γ ⊢ unit [ γ ] ≡ unit

    comm/pair : forall {Γ Γ′} {γ : Γ ⊨ Γ′} {A B} {e₁ : Γ′ ⊢ A} {e₂ : Γ′ ⊢ B}
      -> Γ ⊢ pair e₁ e₂ [ γ ] ≡ pair (e₁ [ γ ]) (e₂ [ γ ])
    comm/fst : forall {Γ Γ′} {γ : Γ ⊨ Γ′} {A B} {e : Γ′ ⊢ A * B}
      -> Γ ⊢ fst e [ γ ] ≡ fst (e [ γ ])
    comm/snd : forall {Γ Γ′} {γ : Γ ⊨ Γ′} {A B} {e : Γ′ ⊢ A * B}
      -> Γ ⊢ snd e [ γ ] ≡ snd (e [ γ ])

    comm/abs : forall {Γ Γ′} {γ : Γ ⊨ Γ′} {A B} {e : A ∷ Γ′ ⊢ B}
      -> Γ ⊢ (abs e) [ γ ] ≡ abs (e [ ext (γ ∙ weaken) var ])
    comm/app : forall {Γ Γ′} {γ : Γ ⊨ Γ′} {A B} {e₁ : Γ′ ⊢ A => B} {e₂}
      -> Γ ⊢ app e₁ e₂ [ γ ] ≡ app (e₁ [ γ ]) (e₂ [ γ ])

    var/ext : forall {Γ Γ′} (γ : Γ ⊨ Γ′) {A} (e : Γ ⊢ A)
      -> Γ ⊢ var [ ext γ e ] ≡ e

  data _⊨_≡_ where
    refl : forall {Γ Γ′} {γ : Γ ⊨ Γ′} -> Γ ⊨ γ ≡ γ
    sym : forall {Γ Γ′} {γ γ′ : Γ ⊨ Γ′} -> Γ ⊨ γ ≡ γ′ -> Γ ⊨ γ′ ≡ γ
    trans : forall {Γ Γ′} {γ₁ γ₂ γ₃ : Γ ⊨ Γ′}
      -> Γ ⊨ γ₁ ≡ γ₂
      -> Γ ⊨ γ₂ ≡ γ₃
      -> Γ ⊨ γ₁ ≡ γ₃

    id∙ˡ : forall {Γ Γ′} {γ : Γ ⊨ Γ′} -> Γ ⊨ id ∙ γ ≡ γ
    id∙ʳ : forall {Γ Γ′} {γ : Γ ⊨ Γ′} -> Γ ⊨ γ ∙ id ≡ γ

    assoc∙ : forall {Γ Γ′ Γ′′ Γ′′′} {γ₁ : Γ′′ ⊨ Γ′′′} {γ₂ : Γ′ ⊨ Γ′′} {γ₃ : Γ ⊨ Γ′}
      -> Γ ⊨ (γ₁ ∙ γ₂) ∙ γ₃ ≡ γ₁ ∙ (γ₂ ∙ γ₃)

    !-unique : forall {Γ} {γ : Γ ⊨ []} -> Γ ⊨ ! ≡ γ
    η-pair : forall {Γ : Context} {A : Type}
      -> A ∷ Γ ⊨ ext weaken var ≡ id
    ext∙ : forall {Γ Γ′ Γ′′} {γ : Γ′ ⊨ Γ′′} {γ′ : Γ ⊨ Γ′} {A} {e : Γ′ ⊢ A}
      -> Γ ⊨ ext γ e ∙ γ′ ≡ ext (γ ∙ γ′) (e [ γ′ ])

    weaken/ext : forall {Γ Γ′} {γ : Γ ⊨ Γ′} {A} {e : Γ ⊢ A}
      -> Γ ⊨ weaken ∙ ext γ e ≡ γ

    cong/ext : forall {Γ Γ′} {γ γ′ : Γ ⊨ Γ′} {A} {e e′ : Γ ⊢ A}
      -> Γ ⊨ γ ≡ γ′
      -> Γ ⊢ e ≡ e′
      -> Γ ⊨ ext γ e ≡ ext γ′ e′
    cong/∙ : forall {Γ Γ′ Γ′′} {γ γ′ : Γ′ ⊨ Γ′′} {δ δ′ : Γ ⊨ Γ′}
      -> Γ′ ⊨ γ ≡ γ′
      -> Γ ⊨ δ ≡ δ′
      -> Γ ⊨ γ ∙ δ ≡ γ′ ∙ δ′

  ×id′-∙ : forall {Γ Γ′ Γ′′} {γ′ : Γ ⊨ Γ′} {γ : Γ′ ⊨ Γ′′} {A}
    -> A ∷ Γ ⊨ γ ×id′ ∙ γ′ ×id′ ≡ (γ ∙ γ′) ×id′
  ×id′-∙ = trans ext∙ (cong/ext (trans assoc∙ (trans (cong/∙ refl weaken/ext) (sym assoc∙))) (var/ext _ _))

  ×id′-ext : forall {Γ Γ′ Γ′′} {γ′ : Γ ⊨ Γ′} {γ : Γ′ ⊨ Γ′′} {A} {e : Γ ⊢ A}
    -> Γ ⊨ γ ×id′ ∙ ext γ′ e ≡ ext (γ ∙ γ′) e
  ×id′-ext = trans ext∙ (cong/ext (trans assoc∙ (cong/∙ refl weaken/ext)) (var/ext _ _))

  open import Relation.Binary.Bundles

  TermSetoid : forall {Γ : Context} {A : Type} -> Setoid (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
  TermSetoid {Γ} {A} = record
             { Carrier = Γ ⊢ A
             ; _≈_ = λ e₁ e₂ → Γ ⊢ e₁ ≡ e₂
             ;isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
             }

  SubstSetoid : forall {Γ : Context} {Γ′ : Context} -> Setoid (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
  SubstSetoid {Γ} {Γ′} = record
             { Carrier = Γ ⊨ Γ′
             ; _≈_ = λ γ₁ γ₂ → Γ ⊨ γ₁ ≡ γ₂
             ;isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
             }

open import Categories.Category
open import Categories.Category.CartesianClosed

module _ {o ℓ e} (𝒞 : Category o ℓ e) (CC : CartesianClosed 𝒞) {ℓ₁ ℓ₂ ℓ₃} (Th : Theory ℓ₁ ℓ₂ ℓ₃) where
  open Category 𝒞
  open import Data.Product using (Σ-syntax)
  open Theory Th
  open import Semantics 𝒞 CC Sg

  Model : Set (o ⊔ ℓ ⊔ e ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
  Model = Σ[ M ∈ Structure ] forall {Γ A e₁ e₂} -> Ax Γ A e₁ e₂ -> ⟦ e₁ ⟧ M ≈ ⟦ e₂ ⟧ M

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
module Prelude.Unit where

data Unit : Set where
  unit : Unit


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors (inefficient implementation)
------------------------------------------------------------------------

-- Vectors of a specified maximum length.

module Data.Star.BoundedVec where

open import Data.Star
open import Data.Star.Nat
open import Data.Star.Decoration
open import Data.Star.Pointer
open import Data.Star.List using (List)
open import Data.Unit
open import Function
import Data.Maybe as Maybe
open import Relation.Binary
open import Relation.Binary.Consequences

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

-- Finite sets decorated with elements (note the use of suc).

BoundedVec : Set → ℕ → Set
BoundedVec a n = Any (λ _ → a) (λ _ → ⊤) (suc n)

[] : ∀ {a n} → BoundedVec a n
[] = this tt

infixr 5 _∷_

_∷_ : ∀ {a n} → a → BoundedVec a n → BoundedVec a (suc n)
_∷_ = that

------------------------------------------------------------------------
-- Increasing the bound

-- Note that this operation is linear in the length of the list.

↑ : ∀ {a n} → BoundedVec a n → BoundedVec a (suc n)
↑ {a} = gmap inc lift
  where
  inc = Maybe.map (map-NonEmpty suc)

  lift : Pointer (λ _ → a) (λ _ → ⊤) =[ inc ]⇒
         Pointer (λ _ → a) (λ _ → ⊤)
  lift (step x) = step x
  lift (done _) = done _

------------------------------------------------------------------------
-- Conversions

fromList : ∀ {a} → (xs : List a) → BoundedVec a (length xs)
fromList ε        = []
fromList (x ◅ xs) = x ∷ fromList xs

toList : ∀ {a n} → BoundedVec a n → List a
toList xs = gmap (const tt) decoration (init xs)


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

open import HoTT

module homotopy.SmashFmapConn where

module _ {i} {j} {A : Type i} (B : A → Type j) where

  custom-assoc : {a₀ a₁ a₂ a₃ : A}
    {b₀ : B a₀} {b₁ b₁' b₁'' : B a₁} {b₂ : B a₂} {b₃ : B a₃}
    {p : a₀ == a₁} (p' : b₀ == b₁ [ B ↓ p ])
    (q' : b₁ == b₁')
    (r' : b₁' == b₁'')
    {s : a₁ == a₂} (s' : b₁'' == b₂ [ B ↓ s ])
    {t : a₂ == a₃} (t' : b₂ == b₃ [ B ↓ t ])
    → p' ∙ᵈ (((q' ∙ r') ◃ s') ∙ᵈ t')
      ==
      ((p' ▹ q') ▹ r') ∙ᵈ s' ∙ᵈ t'
  custom-assoc {p = idp} p'@idp q'@idp r'@idp {s = idp} s'@idp {t = idp} t' = idp

  transp-over : {a₀ a₁ : A} (p : a₀ == a₁) (b₀ : B a₀)
    → b₀ == transport B p b₀ [ B ↓ p ]
  transp-over p b₀ = from-transp B p (idp {a = transport B p b₀})

  transp-over-naturality : ∀ {a₀ a₁ : A} (p : a₀ == a₁)
    {b₀ b₀' : B a₀} (q : b₀ == b₀')
    → q ◃ transp-over p b₀'
      ==
      transp-over p b₀ ▹ ap (transport B p) q
  transp-over-naturality p@idp q@idp = idp

  to-transp-over : {a₀ a₁ : A} {p : a₀ == a₁}
    {b₀ : B a₀} {b₁ : B a₁} (q : b₀ == b₁ [ B ↓ p ])
    → q ▹ ! (to-transp q) == transp-over p b₀
  to-transp-over {p = idp} q@idp = idp

module _ {i} {j} {S* : Type i} (P* : S* → Type j) where

  -- cpa = custom path algebra
  cpa₁ : {s₁ s₂ t : S*} (p* : P* s₂) (p₁ : s₁ == t) (p₂ : s₂ == t)
    → transport P* (! (p₁ ∙ ! p₂)) p*  == transport P* p₂ p* [ P* ↓ p₁ ]
  cpa₁ p* p₁@idp p₂@idp = idp

  -- cpac = custom path algebra coherence
  cpac₁ : ∀ {k} {C : Type k} (f : C → S*)
    {c₁ c₂ : C} (q : c₁ == c₂)
    (d : Π C (P* ∘ f))
    {t : S*} (p₁ : f c₁ == t) (p₂ : f c₂ == t)
    (r : ap f q == p₁ ∙' ! p₂)
    {u  : P* (f c₂)} (v  : u  == transport P* (! (p₂ ∙ ! p₂)) (d c₂))
    {u' : P* (f c₁)} (v' : u' == transport P* (! (p₁ ∙ ! p₂)) (d c₂))
    → (v' ∙
       ap (λ pp → transport P* pp (d c₂)) (ap ! (! (r ∙ ∙'=∙ p₁ (! p₂))) ∙ !-ap f q) ∙
       to-transp {B = P*} {p = ap f (! q)}
                 (↓-ap-in P* f (apd d (! q)))) ◃
      apd d q
      ==
      ↓-ap-out= P* f q (r ∙ ∙'=∙ p₁ (! p₂))
                ((v' ◃ cpa₁ (d c₂) p₁ p₂) ∙ᵈ !ᵈ (v ◃ cpa₁ (d c₂) p₂ p₂)) ▹
      (v ∙ ap (λ pp → transport P* (! pp) (d c₂)) (!-inv-r p₂))
  cpac₁ f q@idp d p₁@.idp p₂@idp r@idp v@idp v'@idp = idp

  cpa₂ : ∀ {k} {C : Type k} (f : C → S*)
    {c₁ c₂ : C} (q : c₁ == c₂)
    (d : Π C (P* ∘ f))
    {s t : S*} (p : f c₁ == s) (r : s == t) (u : f c₂ == t)
    (h : ap f q == p ∙' (r ∙ ! u))
    → transport P* p (d c₁)
      ==
      transport P* u (d c₂)
        [ P* ↓ r ]
  cpa₂ f q@idp d p@.idp r@idp u@idp h@idp = idp

  cpac₂ : ∀ {k} {C : Type k} (f : C → S*)
    {c₁ c₂ c₃ : C} (q : c₁ == c₂) (q' : c₃ == c₂)
    (d : Π C (P* ∘ f))
    {s t : S*} (p : f c₁ == s) (p' : f c₃ == f c₂) (r : s == t) (u : f c₂ == t)
    (h : ap f q == p ∙' (r ∙ ! u))
    (h' : ap f q' == p' ∙' u ∙ ! u)
    {x : P* (f c₂)} (x' : x == transport P* p' (d c₃))
    {y : P* (f c₁)} (y' : y == d c₁)
    → ↓-ap-out=
        P*
        f
        q
        (h ∙ ∙'=∙ p (r ∙ ! u))
        ((y' ◃ transp-over P* p (d c₁)) ∙ᵈ cpa₂ f q d p r u h ∙ᵈ !ᵈ (x' ◃ cpa₂ f q' d p' u u h')) ▹
      (x' ∙
       ap (λ pp → transport P* pp (d c₃))
          (! (∙-unit-r p') ∙
           ap (p' ∙_) (! (!-inv-r u)) ∙
           ! (h' ∙ ∙'=∙ p' (u ∙ ! u))) ∙
       to-transp (↓-ap-in P* f (apd d q')))
      ==
      y' ◃ apd d q
  cpac₂ f q@idp q'@idp d p@.idp p'@.idp r@idp u@idp h@idp h'@idp x'@idp y'@idp = idp

module _ {i} {j} {k} {A : Ptd i} {A' : Ptd j} (f : A ⊙→ A') (B : Ptd k)
         {m n : ℕ₋₂}
         (f-is-m-conn : has-conn-fibers m (fst f))
         (B-is-Sn-conn : is-connected (S n) (de⊙ B)) where

  private
    a₀ = pt A
    a₀' = pt A'
    b₀ = pt B

  module ConnIn (P : A' ∧ B → (n +2+ m) -Type (lmax i (lmax j k)))
                (d : ∀ (ab : A ∧ B) → fst (P (∧-fmap f (⊙idf B) ab))) where

    h : ∀ (b : de⊙ B)
      → (∀ (a' : de⊙ A') → fst (P (smin a' b)))
      → (∀ (a : de⊙ A) → fst (P (smin (fst f a) b)))
    h b s = s ∘ fst f

    Q : de⊙ B → n -Type (lmax i (lmax j k))
    Q b = Q' , Q'-level
      where
      Q' : Type (lmax i (lmax j k))
      Q' = hfiber (h b) (λ a → d (smin a b))
      Q'-level : has-level n Q'
      Q'-level =
        conn-extend-general
          {n = m} {k = n}
          f-is-m-conn
          (λ a → P (smin a b))
          (λ a → d (smin a b))

    s₀ : ∀ (a' : de⊙ A') → fst (P (smin a' b₀))
    s₀ a' = transport (fst ∘ P) (! (∧-norm-l a')) (d smbasel)

    ∧-fmap-smgluel-β-∙' : ∀ (a : de⊙ A) →
      ap (∧-fmap f (⊙idf B)) (smgluel a)
      ==
      smgluel (fst f a) ∙' ! (smgluel a₀')
    ∧-fmap-smgluel-β-∙' a =
      ∧-fmap-smgluel-β' f (⊙idf B) a ∙
      ∙=∙' (smgluel (fst f a)) (! (smgluel a₀'))

    ∧-fmap-smgluel-β-∙ : ∀ (a : de⊙ A) →
      ap (∧-fmap f (⊙idf B)) (smgluel a)
      ==
      smgluel (fst f a) ∙ ! (smgluel a₀')
    ∧-fmap-smgluel-β-∙ a =
      ∧-fmap-smgluel-β-∙' a ∙
      ∙'=∙ (smgluel (fst f a)) (! (smgluel a₀'))

    ∧-fmap-smgluer-β-∙' : ∀ (b : de⊙ B) →
      ap (∧-fmap f (⊙idf B)) (smgluer b)
      ==
      ap (λ a' → smin a' b) (snd f) ∙' ∧-norm-r b
    ∧-fmap-smgluer-β-∙' b =
      ∧-fmap-smgluer-β' f (⊙idf B) b ∙
      ∙=∙' (ap (λ a' → smin a' b) (snd f)) (∧-norm-r b)

    ∧-fmap-smgluer-β-∙ : ∀ (b : de⊙ B) →
      ap (∧-fmap f (⊙idf B)) (smgluer b)
      ==
      ap (λ a' → smin a' b) (snd f) ∙ ∧-norm-r b
    ∧-fmap-smgluer-β-∙ b =
      ∧-fmap-smgluer-β-∙' b ∙
      ∙'=∙ (ap (λ a' → smin a' b) (snd f)) (∧-norm-r b)

    s₀-f : ∀ (a : de⊙ A) → s₀ (fst f a) == d (smin a b₀)
    s₀-f a =
      ap (λ p → transport (λ a'b → fst (P a'b)) p (d smbasel)) q ∙
      to-transp {B = fst ∘ P}
                {p = ap (∧-fmap f (⊙idf B)) (! (smgluel a))}
                (↓-ap-in (fst ∘ P)
                         (∧-fmap f (⊙idf B))
                         (apd d (! (smgluel a))))
      where
      q : ! (∧-norm-l (fst f a)) == ap (∧-fmap f (⊙idf B)) (! (smgluel a))
      q = ap ! (! (∧-fmap-smgluel-β-∙ a)) ∙ !-ap (∧-fmap f (⊙idf B)) (smgluel a)

    q₀ : fst (Q b₀)
    q₀ = s₀ , s₀-lies-over-pt
      where
      s₀-lies-over-pt : h b₀ s₀ == (λ a → d (smin a b₀))
      s₀-lies-over-pt = λ= s₀-f

    q : ∀ (b : de⊙ B) → fst (Q b)
    q = conn-extend {n = n} {h = cst b₀}
                    (pointed-conn-out (de⊙ B) b₀ {{B-is-Sn-conn}})
                    Q
                    (λ _ → q₀)

    q-f : q b₀ == q₀
    q-f = conn-extend-β {n = n} {h = cst b₀}
                        (pointed-conn-out (de⊙ B) b₀ {{B-is-Sn-conn}})
                        Q
                        (λ _ → q₀)
                        unit

    s : ∀ (a' : de⊙ A') (b : de⊙ B) → fst (P (smin a' b))
    s a' b = fst (q b) a'

    s-b₀ : ∀ (a' : de⊙ A') → s a' b₀ == s₀ a'
    s-b₀ a' = ap (λ u → fst u a') q-f

    s-f : ∀ (a : de⊙ A) (b : de⊙ B)
      → s (fst f a) b == d (smin a b)
    s-f a b = app= (snd (q b)) a

    s-f-b₀ : ∀ (a : de⊙ A)
      → s-f a b₀ == s-b₀ (fst f a) ∙ s₀-f a
    s-f-b₀ a =
      app= (snd (q b₀)) a
        =⟨ ↓-app=cst-out' (apd (λ u → app= (snd u) a) q-f) ⟩
      s-b₀ (fst f a) ∙' app= (snd q₀) a
        =⟨ ap (s-b₀ (fst f a) ∙'_) (app=-β s₀-f a) ⟩
      s-b₀ (fst f a) ∙' s₀-f a
        =⟨ ∙'=∙ (s-b₀ (fst f a)) (s₀-f a) ⟩
      s-b₀ (fst f a) ∙ s₀-f a =∎

    s-a₀' : ∀ (b : de⊙ B) →
      s a₀' b
      ==
      transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (d (smin a₀ b))
    s-a₀' b = ↯ $
      s a₀' b
        =⟪ ! (to-transp (↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)))) ⟫
      transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (s (fst f a₀) b)
        =⟪ ap (transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f)))
              (s-f a₀ b) ⟫
      transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (d (smin a₀ b)) ∎∎

    section-smbasel : fst (P smbasel)
    section-smbasel = transport (fst ∘ P) (smgluel a₀') (d smbasel)

    section-smbaser : fst (P smbaser)
    section-smbaser = transport (fst ∘ P) (smgluer b₀) (d smbaser)

    section-smgluel' : ∀ (a' : de⊙ A') → s₀ a' == section-smbasel [ fst ∘ P ↓ smgluel a' ]
    section-smgluel' a' = cpa₁ (fst ∘ P) (d smbasel) (smgluel a') (smgluel a₀')

    section-smgluel : ∀ (a' : de⊙ A') → s a' b₀ == section-smbasel [ fst ∘ P ↓ smgluel a' ]
    section-smgluel a' = s-b₀ a' ◃ section-smgluel' a'

    section-smgluer' : ∀ (b : de⊙ B) →
      transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (d (smin a₀ b))
      ==
      section-smbaser
      [ fst ∘ P ↓ smgluer b ]
    section-smgluer' b =
      cpa₂
        (fst ∘ P)
        (∧-fmap f (⊙idf B))
        (smgluer b)
        d
        (ap (λ a' → smin a' b) (snd f))
        (smgluer b)
        (smgluer b₀)
        (∧-fmap-smgluer-β-∙' b)

    section-smgluer : ∀ (b : de⊙ B) → s a₀' b == section-smbaser [ fst ∘ P ↓ smgluer b ]
    section-smgluer b = s-a₀' b ◃ section-smgluer' b

    module Section =
      SmashElim
        {P = fst ∘ P}
        s
        section-smbasel
        section-smbaser
        section-smgluel
        section-smgluer

    section : Π (A' ∧ B) (fst ∘ P)
    section = Section.f

    is-section-smbasel : s a₀' b₀ == d smbasel
    is-section-smbasel = ↯ $
      s a₀' b₀
        =⟪ s-b₀ a₀' ⟫
      s₀ a₀'
        =⟪idp⟫
      transport (fst ∘ P) (! (∧-norm-l a₀')) (d smbasel)
        =⟪ ap (λ p → transport (fst ∘ P) (! p) (d smbasel))
              (!-inv-r (smgluel a₀')) ⟫
      d smbasel ∎∎

    is-section-smgluel : ∀ (a : de⊙ A) →
      s-f a b₀ ◃ apd d (smgluel a)
      ==
      apd (section ∘ ∧-fmap f (⊙idf B)) (smgluel a) ▹
      is-section-smbasel
    is-section-smgluel a =
      s-f a b₀ ◃ apd d (smgluel a)
        =⟨ ap (_◃ apd d (smgluel a)) (s-f-b₀ a) ⟩
      (s-b₀ (fst f a) ∙ s₀-f a) ◃ apd d (smgluel a)
        =⟨ cpac₁
             (fst ∘ P)
             (∧-fmap f (⊙idf B))
             (smgluel a)
             d
             (smgluel (fst f a))
             (smgluel a₀')
             (∧-fmap-smgluel-β-∙' a)
             (s-b₀ a₀')
             (s-b₀ (fst f a)) ⟩
      ↓-ap-out= (fst ∘ P)
                (∧-fmap f (⊙idf B))
                (smgluel a)
                (∧-fmap-smgluel-β-∙ a)
                (section-smgluel (fst f a) ∙ᵈ !ᵈ (section-smgluel a₀')) ▹
      is-section-smbasel
        =⟨ ! $ ap (_▹ is-section-smbasel) $
           ap (↓-ap-out= (fst ∘ P)
                         (∧-fmap f (⊙idf B))
                         (smgluel a)
                         (∧-fmap-smgluel-β-∙ a)) $
           apd-section-norm-l (fst f a) ⟩
      ↓-ap-out= (fst ∘ P)
                (∧-fmap f (⊙idf B))
                (smgluel a)
                (∧-fmap-smgluel-β-∙ a)
                (apd section (∧-norm-l (fst f a))) ▹
      is-section-smbasel
        =⟨ ! $ ap (_▹ is-section-smbasel) $
           apd-∘'' section
                   (∧-fmap f (⊙idf B))
                   (smgluel a)
                   (∧-fmap-smgluel-β-∙ a) ⟩
      apd (section ∘ ∧-fmap f (⊙idf B)) (smgluel a) ▹
      is-section-smbasel =∎
      where
      apd-section-norm-l : ∀ (a' : de⊙ A') →
        apd section (∧-norm-l a')
        ==
        section-smgluel a' ∙ᵈ !ᵈ (section-smgluel a₀')
      apd-section-norm-l a' =
        apd section (∧-norm-l a')
          =⟨ apd-∙ section (smgluel a') (! (smgluel a₀')) ⟩
        apd section (smgluel a') ∙ᵈ apd section (! (smgluel a₀'))
          =⟨ ap2 _∙ᵈ_ (Section.smgluel-β a')
                      (apd-! section (smgluel a₀') ∙
                       ap !ᵈ (Section.smgluel-β a₀')) ⟩
        section-smgluel a' ∙ᵈ !ᵈ (section-smgluel a₀') =∎

    is-section-smbaser : s a₀' b₀ == d smbaser
    is-section-smbaser = ↯ $
      s a₀' b₀
        =⟪ s-a₀' b₀ ⟫
      transport (fst ∘ P) (ap (λ a' → smin a' b₀) (snd f)) (d (smin a₀ b₀))
        =⟪ ap (λ p → transport (fst ∘ P) p (d (smin a₀ b₀))) (↯ r) ⟫
      transport (fst ∘ P) (ap (∧-fmap f (⊙idf B)) (smgluer b₀)) (d (smin a₀ b₀))
        =⟪ to-transp (↓-ap-in (fst ∘ P) (∧-fmap f (⊙idf B)) (apd d (smgluer b₀))) ⟫
      d smbaser ∎∎
      where
      r : ap (λ a' → smin a' b₀) (snd f) =-= ap (∧-fmap f (⊙idf B)) (smgluer b₀)
      r =
        ap (λ a' → smin a' b₀) (snd f)
          =⟪ ! (∙-unit-r _) ⟫
        ap (λ a' → smin a' b₀) (snd f) ∙ idp
          =⟪ ap (ap (λ a' → smin a' b₀) (snd f) ∙_)
                (! (!-inv-r (smgluer b₀))) ⟫
        ap (λ a' → smin a' b₀) (snd f) ∙ ∧-norm-r b₀
          =⟪ ! (∧-fmap-smgluer-β-∙ b₀) ⟫
        ap (∧-fmap f (⊙idf B)) (smgluer b₀) ∎∎

    is-section-smgluer : ∀ (b : de⊙ B) →
      s-f a₀ b ◃
      apd d (smgluer b)
      ==
      apd (section ∘ ∧-fmap f (⊙idf B)) (smgluer b) ▹
      is-section-smbaser
    is-section-smgluer b = ! $
      apd (section ∘ ∧-fmap f (⊙idf B)) (smgluer b) ▹
      is-section-smbaser
        =⟨ ap (_▹ is-section-smbaser) $
           apd-∘'' section
                  (∧-fmap f (⊙idf B))
                  (smgluer b)
                  (∧-fmap-smgluer-β-∙ b) ⟩
      ↓-ap-out= (fst ∘ P)
                (∧-fmap f (⊙idf B))
                (smgluer b)
                (∧-fmap-smgluer-β-∙ b)
                (apd section (ap (λ a' → smin a' b) (snd f) ∙ ∧-norm-r b)) ▹
      is-section-smbaser
        =⟨ ap (_▹ is-section-smbaser) $
           ap (↓-ap-out= (fst ∘ P)
                         (∧-fmap f (⊙idf B))
                         (smgluer b)
                         (∧-fmap-smgluer-β-∙ b)) $
           apd-section-helper ⟩
      ↓-ap-out= (fst ∘ P)
                (∧-fmap f (⊙idf B))
                (smgluer b)
                (∧-fmap-smgluer-β-∙ b)
                ((s-f a₀ b ◃ transp-over (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (d (smin a₀ b))) ∙ᵈ
                 section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀)) ▹
      is-section-smbaser
        =⟨ cpac₂
             (fst ∘ P)
             (∧-fmap f (⊙idf B))
             (smgluer b)
             (smgluer b₀)
             d
             (ap (λ a' → smin a' b) (snd f))
             (ap (λ a' → smin a' b₀) (snd f))
             (smgluer b)
             (smgluer b₀)
             (∧-fmap-smgluer-β-∙' b)
             (∧-fmap-smgluer-β-∙' b₀)
             (s-a₀' b₀)
             (s-f a₀ b) ⟩
      s-f a₀ b ◃
      apd d (smgluer b) =∎
      where
      apd-section-helper :
        apd section (ap (λ a' → smin a' b) (snd f) ∙ ∧-norm-r b)
        ==
        (s-f a₀ b ◃ transp-over (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (d (smin a₀ b))) ∙ᵈ
        section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀)
      apd-section-helper =
        apd section (ap (λ a' → smin a' b) (snd f) ∙ ∧-norm-r b)
          =⟨ apd-∙ section (ap (λ a' → smin a' b) (snd f)) (∧-norm-r b) ⟩
        apd section (ap (λ a' → smin a' b) (snd f)) ∙ᵈ
        apd section (∧-norm-r b)
          =⟨ ap2 _∙ᵈ_
                 (apd-∘''' section (λ a' → smin a' b) (snd f))
                 (apd-∙ section (smgluer b) (! (smgluer b₀))) ⟩
        ↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)) ∙ᵈ
        apd section (smgluer b) ∙ᵈ apd section (! (smgluer b₀))
          =⟨ ap (↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)) ∙ᵈ_) $
             ap2 _∙ᵈ_
                  (Section.smgluer-β b)
                  (apd-! section (smgluer b₀) ∙
                  ap !ᵈ (Section.smgluer-β b₀)) ⟩
        ↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)) ∙ᵈ
        section-smgluer b ∙ᵈ !ᵈ (section-smgluer b₀)
          =⟨ custom-assoc (fst ∘ P)
               (↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)))
               (! (to-transp (↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)))))
               (ap (transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f))) (s-f a₀ b))
               (section-smgluer' b)
               (!ᵈ (section-smgluer b₀)) ⟩
        ((↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)) ▹
        ! (to-transp (↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f))))) ▹
        ap (transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f))) (s-f a₀ b)) ∙ᵈ
        section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀)
          =⟨ ap (λ u → (u ▹ ap (transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f))) (s-f a₀ b)) ∙ᵈ
                       section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀)) $
             to-transp-over (fst ∘ P) $
             ↓-ap-in (fst ∘ P) (λ a' → smin a' b) (apd (λ a' → s a' b) (snd f)) ⟩
        (transp-over (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (s (fst f a₀) b) ▹
        ap (transport (fst ∘ P) (ap (λ a' → smin a' b) (snd f))) (s-f a₀ b)) ∙ᵈ
        section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀)
          =⟨ ! $ ap (_∙ᵈ section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀)) $
             transp-over-naturality (fst ∘ P)
               (ap (λ a' → smin a' b) (snd f))
               (s-f a₀ b) ⟩
        (s-f a₀ b ◃ transp-over (fst ∘ P) (ap (λ a' → smin a' b) (snd f)) (d (smin a₀ b))) ∙ᵈ
        section-smgluer' b ∙ᵈ !ᵈ (section-smgluer b₀) =∎

    is-section : section ∘ ∧-fmap f (⊙idf B) ∼ d
    is-section =
      Smash-PathOver-elim
        {P = λ ab → fst (P (∧-fmap f (⊙idf B) ab))}
        (section ∘ ∧-fmap f (⊙idf B))
        d
        s-f
        is-section-smbasel
        is-section-smbaser
        is-section-smgluel
        is-section-smgluer

  {- Proposition 4.3.2 in Guillaume Brunerie's thesis -}
  ∧-fmap-conn-l : has-conn-fibers (n +2+ m) (∧-fmap f (⊙idf B))
  ∧-fmap-conn-l = conn-in (λ P → ConnIn.section P , ConnIn.is-section P)

private
  ∧-swap-conn : ∀ {i} {j} (X : Ptd i) (Y : Ptd j) (n : ℕ₋₂)
    → has-conn-fibers n (∧-swap X Y)
  ∧-swap-conn X Y n yx =
    Trunc-preserves-level {n = -2} n $
    equiv-is-contr-map (∧-swap-is-equiv X Y) yx

∧-fmap-conn-r : ∀ {i} {j} {k}
  (A : Ptd i) {B : Ptd j} {B' : Ptd k} (g : B ⊙→ B')
  {k l : ℕ₋₂}
  → is-connected (S k) (de⊙ A)
  → has-conn-fibers l (fst g)
  → has-conn-fibers (k +2+ l) (∧-fmap (⊙idf A) g)
∧-fmap-conn-r A {B} {B'} g {k} {l} A-is-Sk-conn g-is-l-conn =
  transport
    (has-conn-fibers (k +2+ l))
    (λ= (∧-swap-fmap (⊙idf A) g)) $
  ∘-conn (∧-swap A B)
         (∧-swap B' A ∘ ∧-fmap g (⊙idf A))
         (∧-swap-conn A B _) $
  ∘-conn (∧-fmap g (⊙idf A))
         (∧-swap B' A)
         (∧-fmap-conn-l g A g-is-l-conn A-is-Sk-conn)
         (∧-swap-conn B' A _)

private
  ∘-conn' : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
    {n m : ℕ₋₂} (g : B → C) (f : A → B)
    → has-conn-fibers m g
    → has-conn-fibers n f
    → has-conn-fibers (minT n m) (g ∘ f)
  ∘-conn' {n = n} {m = m} g f g-conn f-conn =
    ∘-conn f g
      (λ b → connected-≤T (minT≤l n m) {{f-conn b}})
      (λ c → connected-≤T (minT≤r n m) {{g-conn c}})

{- Proposition 4.3.5 in Guillaume Brunerie's thesis -}
∧-fmap-conn : ∀ {i i' j j'}
  {A : Ptd i} {A' : Ptd i'} (f : A ⊙→ A')
  {B : Ptd j} {B' : Ptd j'} (g : B ⊙→ B')
  {m n k l : ℕ₋₂}
  → is-connected (S k) (de⊙ A')
  → is-connected (S n) (de⊙ B)
  → has-conn-fibers m (fst f)
  → has-conn-fibers l (fst g)
  → has-conn-fibers (minT (n +2+ m) (k +2+ l)) (∧-fmap f g)
∧-fmap-conn {A = A} {A'} f {B} {B'} g {m} {n} {k} {l}
            A'-is-Sk-conn B-is-Sn-conn f-is-m-conn g-is-l-conn =
  transport (has-conn-fibers (minT (n +2+ m) (k +2+ l))) p $
  ∘-conn' (∧-fmap (⊙idf A') g)
          (∧-fmap f (⊙idf B))
          (∧-fmap-conn-r A' g A'-is-Sk-conn g-is-l-conn)
          (∧-fmap-conn-l f B f-is-m-conn B-is-Sn-conn)
  where
  p : ∧-fmap (⊙idf A') g ∘ ∧-fmap f (⊙idf B) == ∧-fmap f g
  p =
    ∧-fmap (⊙idf A') g ∘ ∧-fmap f (⊙idf B)
      =⟨ ! (λ= (∧-fmap-comp f (⊙idf A') (⊙idf B) g)) ⟩
    ∧-fmap (⊙idf A' ⊙∘ f) (g ⊙∘ ⊙idf B)
      =⟨ ap (λ h → ∧-fmap h g) (⊙λ= (⊙∘-unit-l f)) ⟩
    ∧-fmap f g =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda