text:
-- Some theorems about operations on non-deterministic values

module nondet-thms where

open import bool
open import bool-thms
open import nat
open import eq
open import nat-thms
open import functions
open import nondet

----------------------------------------------------------------------
-- Theorems about values contained in non-deterministic values:

-- A proof that x is value of the non-deterministic tree y:
-- either it is equal to a deterministic value (ndrefl)
-- or it is somewhere in the tree.
-- If it is in the tree then we need to construct both branches of the tree,
-- and a proof that x is in one of the branches
-- A consequence of this is that any proof that x ∈ y contains the path
-- to x in the tree.
--
-- Example:
-- hInCoin : H ∈ coin
-- hInCoin = left (Val H) (Val T) ndrefl
--
-- Since H is on the left side of coin, we use the left constructor
-- The branches of the tree are (Val H) and (Val T),
-- and since H is identically equal to H this completes the proof.
data _∈_ {A : Set} (x : A) : (y : ND A) → Set where
  ndrefl : x ∈ (Val x)
  left   : (l : ND A) → (r : ND A) → x ∈ l → x ∈ (l ?? r)
  right  : (l : ND A) → (r : ND A) → x ∈ r → x ∈ (l ?? r)

-- A basic inductive lemma that shows that ∈ is closed under function
-- application. That is, if x ∈ nx, then f x ∈ mapND f nx
--
-- Example:
-- ndCons : ... → xs ∈ nxs → (x :: xs) ∈ mapND (_::_ x) nxs
∈-apply : {A B : Set} → (f : A → B) → (x : A) → (nx : ND A)
        → x ∈ nx → (f x) ∈ (mapND f nx)
∈-apply f x (Val .x) ndrefl = ndrefl
∈-apply f x (l ?? r) (left  .l .r k) =
  left  (mapND f l) (mapND f r) (∈-apply f x l k)
∈-apply f x (l ?? r) (right .l .r k) =
  right (mapND f l) (mapND f r) (∈-apply f x r k)

----------------------------------------------------------------------
-- Theorems about 'mapND':

-- Combine two mapND applications into one:
mapND-mapND : ∀ {A B C : Set} → (f : B → C) (g : A → B) (xs : ND A)
            → mapND f (mapND g xs) ≡ mapND (f ∘ g) xs
mapND-mapND f g (Val x) = refl
mapND-mapND f g (t1 ?? t2)
  rewrite mapND-mapND f g t1 | mapND-mapND f g t2 = refl

----------------------------------------------------------------------
-- Theorems about 'always':

-- Extend validity of a function with a deterministic argument to validity of
-- the corresponding non-deterministic function:
always-mapND : ∀ {A : Set} → (p : A → 𝔹) (xs : ND A)
            → ((y : A) → p y ≡ tt)
            → always (mapND p xs) ≡ tt
always-mapND _ (Val y) prf = prf y
always-mapND p (t1 ?? t2) prf
  rewrite always-mapND p t1 prf
        | always-mapND p t2 prf = refl

-- Extend validity of a function with a deterministic argument to validity of
-- the corresponding non-deterministic function:
always-with-nd-arg : ∀ {A : Set} → (p : A → ND 𝔹) (xs : ND A)
               → ((y : A) → always (p y) ≡ tt)
               → always (with-nd-arg p xs) ≡ tt
always-with-nd-arg _ (Val y) prf = prf y
always-with-nd-arg p (t1 ?? t2) prf
  rewrite always-with-nd-arg p t1 prf
        | always-with-nd-arg p t2 prf = refl

-- Extend validity of a deterministic function to validity of
-- corresponding function with non-deterministic result:
always-toND : ∀ {A : Set} → (p : A → 𝔹) (x : A)
          → (p x) ≡ tt → always (toND p x) ≡ tt
always-toND _ _ p = p

-- Extend validity of a deterministic function to validity of
-- corresponding non-deterministic function:
always-det-to-nd : ∀ {A : Set} → (p : A → 𝔹)
          → ((y : A) → (p y) ≡ tt)
          → (xs : ND A) → always (det-to-nd p xs) ≡ tt
always-det-to-nd p u xs =
  always-with-nd-arg (toND p) xs (λ x → always-toND p x (u x))

----------------------------------------------------------------------
-- Theorems about 'satisfy':

-- A theorem like filter-map in functional programming:
satisfy-mapND : ∀ {A B : Set} → (f : A → B) (xs : ND A) (p : B → 𝔹)
             → (mapND f xs) satisfy p ≡ xs satisfy (p ∘ f)
satisfy-mapND _ (Val x) _ = refl
satisfy-mapND f (t1 ?? t2) p
 rewrite satisfy-mapND f t1 p
       | satisfy-mapND f t2 p = refl

-- Extend validity of function with deterministic argument to validity of
-- non-deterministic function:
satisfy-with-nd-arg : ∀ {A B : Set} → (p : B → 𝔹) (f : A → ND B) (xs : ND A)
               → ((y : A) → (f y) satisfy p ≡ tt)
               → (with-nd-arg f xs) satisfy p ≡ tt
satisfy-with-nd-arg _ _ (Val y) prf = prf y
satisfy-with-nd-arg p f (t1 ?? t2) prf
  rewrite satisfy-with-nd-arg p f t1 prf
        | satisfy-with-nd-arg p f t2 prf = refl

----------------------------------------------------------------------
-- Theorems about 'every':

mapNDval : ∀ (f : ℕ → ℕ) (v : ℕ) (x : ND ℕ) →
         every _=ℕ_ v x ≡ tt → every _=ℕ_ (f v) (mapND f x) ≡ tt
mapNDval f v (Val x) u rewrite =ℕ-to-≡ {v} {x} u | =ℕ-refl (f x) = refl
mapNDval f v (t1 ?? t2) u
  rewrite mapNDval f v t1 (&&-fst u)
        | mapNDval f v t2 (&&-snd {every _=ℕ_ v t1} {every _=ℕ_ v t2} u) = refl

----------------------------------------------------------------------
-- This theorms allows to weaken a predicate which is always satisfied:
weak-always-predicate : ∀ {A : Set} → (p p1 : A → 𝔹) (xs : ND A)
                → xs satisfy p ≡ tt
                → xs satisfy (λ x → p1 x || p x) ≡ tt
weak-always-predicate p p1 (Val x) u rewrite u | ||-tt (p1 x) = refl
weak-always-predicate p p1 (t1 ?? t2) u
  rewrite weak-always-predicate p p1 t1 (&&-fst u)
        | weak-always-predicate p p1 t2 (&&-snd {t1 satisfy p} {t2 satisfy p} u)
  = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


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

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Semigroup.Construct.Free {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Algebra.Semigroup

open import Cubical.Data.Empty.Polymorphic
open import Cubical.Data.Prod

open import Cubical.Relation.Binary.Reasoning.Equality

A = ⟨ Aˢ ⟩
isSetA = Aˢ .snd

------------------------------------------------------------------------
-- The direct free semigroup type

data FreeS′ : Type ℓ where
  inj : A → FreeS′
  _•_ : Op₂ FreeS′

  •-assoc : Associative _•_

  squash : isSet FreeS′

elim : ∀ {ℓ′} {B : FreeS′ → Type ℓ′} →
        (∀ x → isSet (B x)) →
        (∀ x → B (inj x)) →
        (op : ∀ x y → B x → B y → B (x • y)) →
        (∀ x y z (a : B x) (b : B y) (c : B z) → PathP (λ i → B (•-assoc x y z i)) (op _ _ (op _ _ a b) c) (op _ _ a (op _ _ b c))) →
        (x : FreeS′) → B x
elim isSetB f op assc (inj x) = f x
elim isSetB f op assc (x • y) = op x y (elim isSetB f op assc x) (elim isSetB f op assc y)
elim isSetB f op assc (•-assoc x y z i) = assc x y z (elim isSetB f op assc x) (elim isSetB f op assc y) (elim isSetB f op assc z) i
elim isSetB f op assc (squash x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 isSetB
    (elim isSetB f op assc x) (elim isSetB f op assc y)
    (cong (elim isSetB f op assc) p) (cong (elim isSetB f op assc) q) (squash x y p q) i j

------------------------------------------------------------------------
-- The simplified free semigroup type

infixl 5 _□
infixr 4 _∶_

data FreeS : Type ℓ where
  _□ : A → FreeS
  _∶_ : A → FreeS → FreeS

module FreeSPath where
  Cover : FreeS → FreeS → Type ℓ
  Cover (x □) (y □) = x ≡ y
  Cover (x □) (y ∶ ys) = ⊥
  Cover (x ∶ xs) (y □) = ⊥
  Cover (x ∶ xs) (y ∶ ys) = (x ≡ y) × Cover xs ys

  isPropCover : ∀ xs ys → isProp (Cover xs ys)
  isPropCover (x □) (y □) = isSetA x y
  isPropCover (x □) (y ∶ ys) = isProp⊥
  isPropCover (x ∶ xs) (y □) = isProp⊥
  isPropCover (x ∶ xs) (y ∶ ys) = isPropProd (isSetA x y) (isPropCover xs ys)

  reflCover : ∀ xs → Cover xs xs
  reflCover (x □)   = refl
  reflCover (x ∶ xs) = refl , reflCover xs

  encode : ∀ xs ys → xs ≡ ys → Cover xs ys
  encode xs _ = J (λ ys _ → Cover xs ys) (reflCover xs)

  encodeRefl : ∀ xs → encode xs xs refl ≡ reflCover xs
  encodeRefl xs = JRefl (λ ys _ → Cover xs ys) (reflCover xs)

  decode : ∀ xs ys → Cover xs ys → xs ≡ ys
  decode (x □) (y □) p = cong _□ p
  decode (x □) (y ∶ ys) ()
  decode (x ∶ xs) (y □) ()
  decode (x ∶ xs) (y ∶ ys) (p , q) = cong₂ _∶_ p (decode xs ys q)

  decodeRefl : ∀ xs → decode xs xs (reflCover xs) ≡ refl
  decodeRefl (x □)   = refl
  decodeRefl (x ∶ xs) = cong (cong₂ _∶_ refl) (decodeRefl xs)

  decodeEncode : ∀ xs ys → (p : xs ≡ ys) → decode xs ys (encode xs ys p) ≡ p
  decodeEncode xs _ =
    J (λ ys p → decode xs ys (encode xs ys p) ≡ p)
      (cong (decode xs xs) (encodeRefl xs) ∙ decodeRefl xs)

isSetFreeS : isSet FreeS
isSetFreeS x y =
  isOfHLevelRetract 1
    (FreeSPath.encode x y)
    (FreeSPath.decode x y)
    (FreeSPath.decodeEncode x y)
    (FreeSPath.isPropCover x y)

_++_ : Op₂ FreeS
(x □) ++ ys = x ∶ ys
(x ∶ xs) ++ ys = x ∶ xs ++ ys

++-assoc : Associative _++_
++-assoc (x □) ys zs = refl
++-assoc (x ∶ xs) ys zs = cong (x ∶_) (++-assoc xs ys zs)

------------------------------------------------------------------------
-- Proving the two types are equivalent

FreeS→FreeS′ : FreeS → FreeS′
FreeS→FreeS′ (x □)   = inj x
FreeS→FreeS′ (x ∶ xs) = inj x • FreeS→FreeS′ xs

FreeS′→FreeS : FreeS′ → FreeS
FreeS′→FreeS = elim (λ _ → isSetFreeS) _□ (λ _ _ → _++_) (λ _ _ _ → ++-assoc)

FreeS→FreeS′→FreeS : retract FreeS→FreeS′ FreeS′→FreeS
FreeS→FreeS′→FreeS (x □) = refl
FreeS→FreeS′→FreeS (x ∶ xs) = cong (x ∶_) (FreeS→FreeS′→FreeS xs)

++-hom : Homomorphic₂ FreeS→FreeS′ _++_ _•_
++-hom (x □)   ys = refl
++-hom (x ∶ xs) ys = cong (inj x •_) (++-hom xs ys) ∙ sym (•-assoc (inj x) (FreeS→FreeS′ xs) (FreeS→FreeS′ ys))

FreeS′→FreeS→FreeS′ : section FreeS→FreeS′ FreeS′→FreeS
FreeS′→FreeS→FreeS′ = elim (λ _ → isSet→isGroupoid squash _ _) (λ _ → refl) sectionOp (λ _ _ _ _ _ _ → isOfHLevelPathP' 0 (squash _ _) _ _ .fst)
  where
    sectionOp : ∀ x y → FreeS→FreeS′ (FreeS′→FreeS x) ≡ x →
                        FreeS→FreeS′ (FreeS′→FreeS y) ≡ y →
                        FreeS→FreeS′ (FreeS′→FreeS (x • y)) ≡ (x • y)
    sectionOp x y p q =
      FreeS→FreeS′ (FreeS′→FreeS (x • y))                           ≡⟨⟩
      FreeS→FreeS′ (FreeS′→FreeS x ++ FreeS′→FreeS y)               ≡⟨ ++-hom (FreeS′→FreeS x) (FreeS′→FreeS y) ⟩
      FreeS→FreeS′ (FreeS′→FreeS x) • FreeS→FreeS′ (FreeS′→FreeS y) ≡⟨ cong₂ _•_ p q ⟩
      x • y                                                         ∎

FreeS≃FreeS′ : FreeS ≃ FreeS′
FreeS≃FreeS′ = isoToEquiv (iso FreeS→FreeS′ FreeS′→FreeS FreeS′→FreeS→FreeS′ FreeS→FreeS′→FreeS)

FreeS≡FreeS′ : FreeS ≡ FreeS′
FreeS≡FreeS′ = ua FreeS≃FreeS′

------------------------------------------------------------------------
-- Semigroup Algebra

FreeS′-isSemigroup : IsSemigroup FreeS′ _•_
FreeS′-isSemigroup = record
  { isMagma = record { is-set = squash }
  ; assoc   = •-assoc
  }

FreeS-isSemigroup : IsSemigroup FreeS _++_
FreeS-isSemigroup = record
  { isMagma = record { is-set = isSetFreeS }
  ; assoc   = ++-assoc
  }

FreeSemigroup′ : Semigroup ℓ
FreeSemigroup′ = record { isSemigroup = FreeS′-isSemigroup }

FreeSemigroup : Semigroup ℓ
FreeSemigroup = record { isSemigroup = FreeS-isSemigroup }

EquivFreeS : SemigroupEquiv FreeSemigroup FreeSemigroup′
EquivFreeS = record
  { eq    = FreeS≃FreeS′
  ; isHom = ++-hom
  }

FreeSemigroup≡ : FreeSemigroup ≡ FreeSemigroup′
FreeSemigroup≡ = uaSemigroup EquivFreeS

ext: agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Data.Unit

module let-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

abstract
  e1 : let x = ⊤ in x
  e1 = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


text:
-----------------------------------------------------------------------
-- This file formalizes the proof that Dial₂(Sets) is a full linear  --
-- category.  See Lemma 12 of the paper.                             --
-----------------------------------------------------------------------
module FullLinCat where

open import prelude
open import Dial2Sets

-- Monoidal nat. trans. m⊤ : ⊤ → !⊤:
m⊤ : Hom I (!ₒ I)
m⊤ = id-set , (λ f → triv) , m⊤-cond
 where
  m⊤-cond : {u : ⊤} {l : 𝕃 ⊤} → ι u triv → all-pred (ι u) l
  m⊤-cond {triv}{[]} triv = triv
  m⊤-cond {triv}{triv :: l} triv = triv , m⊤-cond {triv}{l} triv

-- These diagrams can be found on page 23 of the report.
m⊤-diag₁ : _≡h_ {I}{ !ₒ (!ₒ I)}
  (comp {I} { !ₒ I} { !ₒ (!ₒ I)} m⊤ (!ₐ {I}{ !ₒ I} m⊤))
  (comp {I} { !ₒ I} { !ₒ (!ₒ I)} m⊤ (δ {I}))
m⊤-diag₁ = refl , refl

m⊤-diag₂ : _≡h_ {I}{I} (comp {I}{ !ₒ I}{I} m⊤ (ε {I})) (id {I})
m⊤-diag₂ = refl , ext-set aux
 where
  aux : {a : ⊤} → triv ≡ a
  aux {triv} = refl

-- The monoidal nat. trans. m : !A ⊗ !B → !(A ⊗ B):
h'₁ : {U V X Y : Set} → (((V → X) × (U → Y)) *) → (V → U → (X *))
h'₁ [] v u = []
h'₁ ((j₁ , j₂) :: js) v u = (j₁ v) :: h'₁ js v u

h'₁-append : ∀{U V X Y : Set}{l₁ l₂ : ((V → X) × (U → Y)) *}{v u}
  → (h'₁ l₁ v u) ++ (h'₁ l₂ v u) ≡ h'₁ (l₁ ++ l₂) v u
h'₁-append {l₁ = []} = refl
h'₁-append {l₁ = (j₁ , j₂) :: js}{l₂}{v}{u}
  rewrite h'₁-append {l₁ = js}{l₂}{v}{u} = refl

h₁ : {U V X Y : Set}
  → ((U × V)
  → (((V → X) × (U → Y)) *))
  → (V → U → (X *))
h₁ g v u = h'₁ (g (u , v)) v u

h'₂ : {U V X Y : Set}
  → (((V → X) × (U → Y)) *)
  → (U → V → (Y *))
h'₂ [] u v = []
h'₂ ((j₁ , j₂) :: js) u v = (j₂ u) :: h'₂ js u v

h'₂-append : ∀{U V X Y : Set}{l₁ l₂ : ((V → X) × (U → Y)) *}{v u}
  → (h'₂ l₁ v u) ++ (h'₂ l₂ v u) ≡ h'₂ (l₁ ++ l₂) v u
h'₂-append {l₁ = []} = refl
h'₂-append {l₁ = (j₁ , j₂) :: js}{l₂}{v}{u}
  rewrite h'₂-append {l₁ = js}{l₂}{v}{u} = refl

h₂ : {U V X Y : Set}
  → ((U × V)
  → (((V → X) × (U → Y)) *))
  → (U → V → (Y *))
h₂ g u v = h'₂ (g (u , v)) u v

m⊗ : {A B : Obj} → Hom ((!ₒ A) ⊗ₒ (!ₒ B)) (!ₒ (A ⊗ₒ B))
m⊗ {U , X , α} {V , Y , β} =
  id-set , (λ g → h₁ g , h₂ g) , (λ {u}{y} x → m⊗-cond {u}{y} x)
 where
  m⊗-cond : {u : Σ U (λ x → V)}
      {y : Σ U (λ x → V) → 𝕃 (Σ (V → X) (λ x → U → Y))} →
      ((λ u₁ f → all-pred (α u₁) (f u₁)) ⊗ᵣ
       (λ u₁ f → all-pred (β u₁) (f u₁)))
      u
      ((λ v u₁ → h'₁ (y (u₁ , v)) v u₁) ,
       (λ u₁ v → h'₂ (y (u₁ , v)) u₁ v)) →
      all-pred ((α ⊗ᵣ β) u) (y u)
  m⊗-cond {(u , v)}{g} (p₁ , p₂) = aux p₁ p₂
   where
    aux : ∀{l}
        → all-pred (α u) (h'₁ l v u)
        → all-pred (β v) (h'₂ l u v)
        → all-pred ((α ⊗ᵣ β) (u , v)) l
    aux {[]} p₁ p₂ = triv
    aux {(j₁ , j₂) :: js} (p₁ , p₂) (p₃ , p₄) = (p₁ , p₃) , aux {js} p₂ p₄

-- The following diagrams can be found on page 24 of the report.
m⊗-diag-A : ∀{A}
  → (m⊤ ⊗ₐ (id { !ₒ A})) ○ (m⊗ {I} {A} ○ !ₐ (λ⊗ {A})) ≡h λ⊗ { !ₒ A}
m⊗-diag-A {U , X , α} = ext-set (λ {a} → aux {a}) ,
                        ext-set (λ {g} → cong2 _,_ refl (ext-set (aux' {g})))
 where
  aux : {a : Σ ⊤ (λ x → U)}
    → snd (⟨ (λ x → x) , (λ x → x) ⟩ a) ≡ snd a
  aux {triv , u} = refl
  aux' : {g : U → X *} → {a : ⊤}
    → (λ v → h'₂ (map (λ x → (λ _ → triv) , (λ _ → x)) (g v)) a v) ≡ g
  aux' {g}{triv} = ext-set (λ {a} → aux'' {a}{g a})
   where
    aux'' : {a : U}{l : X *}
      → h'₂ (map (λ x → (λ _ → triv) , (λ _ → x)) l) triv a ≡ l
    aux'' {u}{[]} = refl
    aux'' {u}{x :: xs} rewrite aux'' {u}{xs} = refl

m⊗-diag-B : ∀{A}
  → ((id { !ₒ A}) ⊗ₐ m⊤) ○ (m⊗ {A} {I} ○ !ₐ (ρ⊗ {A})) ≡h ρ⊗ { !ₒ A}
m⊗-diag-B {U , X , α} =
  (ext-set (λ {a} → aux {a})) , ext-set (λ {g} → cong2 _,_ (ext-set aux') refl)
 where
   aux : {a : Σ U (λ x → ⊤)}
     → fst (⟨ (λ x → x) , (λ x → x) ⟩ a) ≡ fst a
   aux {u , triv} = refl
   aux' : {g : U → X *} → {a : ⊤}
     → (λ u → h'₁ (map (λ x → (λ x₁ → x) , (λ x₁ → triv)) (g u)) a u) ≡ g
   aux' {g}{triv} = ext-set (λ {u} →  aux'' {g u}{u})
    where
      aux'' : ∀{l : X *}{u : U}
        → h'₁ (map (λ x → (λ x₁ → x) , (λ x₁ → triv)) l) triv u ≡ l
      aux'' {[]}{u}  = refl
      aux'' {x :: xs}{u} rewrite aux'' {xs}{u} = refl

m⊗-diag-C : ∀{A B}
  → β⊗ { !ₒ A} { !ₒ B} ○ m⊗ {B} {A} ≡h (m⊗ {A}{B}) ○ (!ₐ (β⊗ {A}{B}))
m⊗-diag-C {U , X , α}{V , Y , β} =
          refl ,
          ext-set (λ {g} →
               cong2 _,_ (ext-set (λ {v} → ext-set (λ {u} → aux {g (v , u)}{u}{v})))
                         (ext-set (λ {u} → ext-set (λ {v} → aux' {g (v , u)}{u}{v}))))
 where
   aux : ∀{l : 𝕃 (Σ (U → Y) (λ x → V → X))}{u v}
     → h'₂ l v u ≡  h'₁ (map twist-× l) v u
   aux {[]} = refl
   aux {(j₁ , j₂) :: js} {u}{v} rewrite aux {js}{u}{v} = refl
   aux' : ∀{l : 𝕃 (Σ (U → Y) (λ x → V → X))}{u v}
     → h'₁ l u v ≡  h'₂ (map twist-× l) u v
   aux' {[]} = refl
   aux' {(j₁ , j₂) :: js} {u}{v} rewrite aux' {js}{u}{v} = refl

m⊗-diag-D : ∀{A B C : Obj}
  →  α⊗ { !ₒ A} { !ₒ B} { !ₒ C} ○ id { !ₒ A} ⊗ₐ m⊗ {B} {C} ○ m⊗ {A} {B ⊗ₒ C}
  ≡h ((m⊗ {A}{B}) ⊗ₐ (id { !ₒ C})) ○ (m⊗ {A ⊗ₒ B}{C}) ○ (!ₐ (α⊗ {A}{B}{C}))
m⊗-diag-D {U , X , α}{V , Y , β}{W , Z , γ} =
  ext-set aux  ,
  ext-set (λ {g} →
    cong2 _,_
          (ext-set
             (λ {w} → cong2 _,_
                            (ext-set
                               (λ {v} → ext-set
                                          (λ {u} → aux' {g (u , v , w)}{u}{v}{w})))
                            (ext-set (λ {u} → ext-set (λ {v} → aux'' {g (u , v , w)}{u}{v}{w})))))
          (ext-set (λ {a} → aux''' {a}{g})))
 where
  aux : {a : Σ (Σ U (λ x → V)) (λ x → W)}
    → ⟨ (λ x → x) , (λ x → x) ⟩ (lr-assoc-× a) ≡ lr-assoc-× (⟨ (λ x → x) , (λ x → x) ⟩ a)
  aux {((u , v) , w)} = refl
  aux' : ∀{l : 𝕃 (Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z)))}{u v w}
    → h'₁ l (v , w) u ≡ h'₁ (h'₁ (map (Fα {V}{W}{X}{Y}{U}{V}{Z}) l) w (u , v)) v u
  aux' {[]} = refl
  aux' {(j₁ , j₂) :: js}{u}{v}{w} rewrite aux' {js}{u}{v}{w} = refl
  aux'' : ∀{l : 𝕃 (Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z)))}{u v w}
    → h'₁ (h'₂ l u (v , w)) w v ≡ h'₂ (h'₁ (map (Fα {V}{W}{X}{Y}{U}{V}{Z}) l) w (u , v)) u v
  aux'' {[]} = refl
  aux'' {(j₁ , j₂) :: js}{u}{v}{w} with j₂ u
  ... | (j₃ , j₄) rewrite aux'' {js}{u}{v}{w} = refl
  aux''' : ∀{a : Σ U (λ x → V)}{g : Σ U (λ x → Σ V (λ x₁ → W)) →
    𝕃 (Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z)))} →
       (λ v →
          h'₂ (h'₂ (g (fst a , snd a , v)) (fst a) (snd a , v)) (snd a) v)
       ≡ (λ v → h'₂ (map (Fα {V}{W}{X}{Y}{U}{V}{Z}) (g (lr-assoc-× (a , v)))) a v)
  aux''' {u , v}{g} = ext-set (λ {w} → aux'''' {g (u , v , w)}{w})
   where
     aux'''' : ∀{l : 𝕃 (Σ (Σ V (λ x → W) → X) (λ x → U → Σ (W → Y) (λ x₁ → V → Z)))}{w : W}
       → h'₂ (h'₂ l u (v , w)) v w ≡ h'₂ (map (Fα {V}{W}{X}{Y}{U}{V}{Z}) l) (u , v) w
     aux'''' {[]} = refl
     aux'''' {(j₁ , j₂) :: js}{w} with j₂ u
     ... | (j₃ , j₄) rewrite aux'''' {js}{w} = refl

-- The following diagrams can be found on the bottom of page 26.
m⊗-diag-E : ∀{A B : Obj} → ε {A} ⊗ₐ ε {B} ≡h (m⊗ {A}{B}) ○ (ε {A ⊗ₒ B})
m⊗-diag-E {U , X , α}{V , Y , β} = ext-set aux , ext-set aux'
 where
  aux : {a : Σ U (λ x → V)} → ⟨ (λ x → x) , (λ x → x) ⟩ a ≡ a
  aux {u , v} = refl
  aux' : {a : Σ (V → X) (λ x → U → Y)}
    →   F⊗ {f = λ x → x} {λ x y → x :: []}{λ x → x} {λ x y → x :: []} a
      ≡ ((λ v u → h'₁ (a :: []) v u) , (λ u v → h'₂ (a :: []) u v))
  aux' {j₁ , j₂} = refl

m⊗-diag-F : ∀{A B : Obj}
  → δ {A} ⊗ₐ δ {B} ○ m⊗ { !ₒ A} { !ₒ B} ○ !ₐ (m⊗ {A} {B}) ≡h (m⊗ {A}{B}) ○ (δ {A ⊗ₒ B})
m⊗-diag-F {U , X , α}{V , Y , β} =
  ext-set aux , ext-set (λ {g} →
    cong2 _,_ (ext-set (λ {v} → ext-set (λ {u} → aux' {g (u , v)}{v}{u})))
              (ext-set (λ {u} → ext-set (λ {v} → aux'' {g (u , v)}{v}{u}))))
 where
   aux : {a : Σ U (λ x → V)} → ⟨ (λ x → x) , (λ x → x) ⟩ a ≡ a
   aux {u , v} = refl
   aux' : ∀{l : 𝕃 (Σ U (λ x → V)
     → 𝕃 (Σ (V → X) (λ x → U → Y)))}{v u}
     → foldr (λ f → _++_ (f u)) []
      (h'₁
       (map
        (λ g₁ →
           (λ v₁ u₁ → h'₁ (g₁ (u₁ , v₁)) v₁ u₁) ,
           (λ u₁ v₁ → h'₂ (g₁ (u₁ , v₁)) u₁ v₁))
        l)
       v u)
      ≡ h'₁ (foldr (λ f → _++_ (f (u , v))) [] l) v u
   aux' {[]} = refl
   aux' {j :: js}{v}{u} with j (u , v)
   ... | [] rewrite aux' {js}{v}{u} = refl
   ... | (j₁ , j₂) :: js' rewrite aux' {js}{v}{u}
     = cong2 {a = j₁ v} _::_ refl (h'₁-append {l₁ = js'})

   aux'' : ∀{l : 𝕃 (Σ U (λ x → V) → 𝕃 (Σ (V → X) (λ x → U → Y)))}{v u}
     → foldr (λ f → _++_ (f v)) []
      (h'₂
       (map
        (λ g₁ →
           (λ v₁ u₂ → h'₁ (g₁ (u₂ , v₁)) v₁ u₂) ,
           (λ u₂ v₁ → h'₂ (g₁ (u₂ , v₁)) u₂ v₁))
        l)
       u v)
      ≡ h'₂ (foldr (λ f → _++_ (f (u , v))) [] l) u v
   aux'' {[]} = refl
   aux'' {j :: js}{v}{u} with j (u , v)
   ... | [] = aux'' {js}
   ... | (j₁ , j₂) :: js' rewrite aux'' {js}{v}{u}
     = cong2 {a = j₂ u} _::_ refl (h'₂-append {l₁ = js'})

-- Now we show that whenever (!A , δ) is a free comonoid, then we have
-- distinguished nat. trans. e : !A → ⊤ and d : !A → !A ⊗ !A.  These
-- constructions and their diagrams can be found on page 27 of the
-- report.

e : {A : Obj} → Hom (!ₒ A) I
e {U , X , α} = (λ x → triv) , (λ x u → []) , (λ {u}{y} x → e-cond {u}{y} x)
 where
   e-cond : {u : U} {y : ⊤} → ⊤ → ι triv y
   e-cond {u}{triv} triv = triv

θ : ∀{U X : Set} → ((U → U → (X *)) × (U → U → (X *))) → U → X *
θ {U}{X} (f , g) u = (f u u) ++ (g u u)

d : {A : Obj} → Hom (!ₒ A) ((!ₒ A) ⊗ₒ (!ₒ A))
d {U , X , α} = (λ x → (x , x)) , θ , d-cond
 where
   d-cond : {u : U} {y : Σ (U → U → 𝕃 X) (λ x → U → U → 𝕃 X)} →
      all-pred (α u) (θ y u) →
      ((λ u₁ f → all-pred (α u₁) (f u₁)) ⊗ᵣ
       (λ u₁ f → all-pred (α u₁) (f u₁)))
      (u , u) y
   d-cond {u}{f , g} = aux
    where
      aux : ∀{l₁ l₂ : X *}
        → all-pred (α u) (l₁ ++ l₂)
        → ((all-pred (α u) l₁) × (all-pred (α u) l₂))
      aux {[]} p = triv , p
      aux {x :: xs} (p₁ , p₂) = (p₁ , fst (aux {xs} p₂)) , snd (aux {xs} p₂)

-- e must be a monoidal nat. trans.
e-diag-G : ∀{A B : Obj}{f : Hom A B} → !ₐ f ○ e {B} ≡h e {A}
e-diag-G {U , X , α}{V , Y , β}{(f , F , _)} = refl , refl

e-diag-H : _≡h_ {I}{I} (comp {I}{ !ₒ I}{I} m⊤ (e {I})) (id {I})
e-diag-H = ext-set aux , ext-set aux
 where
   aux : {a : ⊤} → triv ≡ a
   aux {triv} = refl

e-diag-I : ∀{A B : Obj} → m⊗ {A} {B} ○ e {A ⊗ₒ B} ≡h e {A} ⊗ₐ e {B} ○ λ⊗ {I}
e-diag-I {U , X , α}{V , Y , β} = (ext-set (λ {a} → aux {a})) , refl
 where
   aux : {a : Σ U (λ x → V)} → triv ≡ snd (⟨ (λ x → triv) , (λ x → triv) ⟩ a)
   aux {u , v} = refl

-- d must be a monoidal nat. trans.  The following diagrams can be
-- found on page 28 of the report.
d-diag-J : ∀{A B : Obj}{f : Hom A B} → !ₐ f ○ d {B} ≡h (d {A}) ○ ((!ₐ f) ⊗ₐ (!ₐ f))
d-diag-J {U , X , α}{V , Y , β}{f , F , _} = refl , ext-set (λ {a} → aux {a})
 where
   aux : {a : Σ (V → V → 𝕃 Y) (λ x → V → V → 𝕃 Y)}
     →   (λ u → map F (θ a (f u)))
       ≡ θ (F⊗ {f = f} {λ g u → map F (g (f u))} {f}
               {λ g u → map F (g (f u))} a)
   aux {j₁ , j₂} = ext-set (λ {u} → map-append F (j₁ (f u) (f u)) (j₂ (f u) (f u)))

d-diag-K : _≡h_ {I}{(!ₒ I) ⊗ₒ (!ₒ I)}
  (comp {I}{ !ₒ I}{(!ₒ I) ⊗ₒ (!ₒ I)} m⊤ (d {I}))
  (comp {I}{I ⊗ₒ I}{(!ₒ I) ⊗ₒ (!ₒ I)} (λ⁻¹⊗ {I}) (m⊤ ⊗ₐ m⊤))
d-diag-K = ext-set aux , ext-set (λ {a} → aux' {a})
 where
   aux : {a : ⊤} → (a , a) ≡ (triv , a)
   aux {triv} = refl
   aux' : {a : Σ (⊤ → ⊤ → 𝕃  ⊤) (λ x → ⊤ → ⊤ → 𝕃  ⊤)}
     →   triv
       ≡ (snd (F⊗ {f = λ x → x} {λ f → triv} {λ x → x} {λ f → triv} a) triv)
   aux' {j₁ , j₂} = refl

iso : {A B : Obj} → Hom (((!ₒ A) ⊗ₒ (!ₒ A)) ⊗ₒ ((!ₒ B) ⊗ₒ (!ₒ B)))
                        (((!ₒ A) ⊗ₒ (!ₒ B)) ⊗ₒ ((!ₒ A) ⊗ₒ (!ₒ B)))
iso {A}{B} =
    α⊗ {(!ₒ A)} {(!ₒ A)} {(!ₒ B) ⊗ₒ (!ₒ B)}
  ○ (id {(!ₒ A)} ⊗ₐ α⊗-inv {(!ₒ A)} {(!ₒ B)} {(!ₒ B)}
  ○ (id {(!ₒ A)} ⊗ₐ (β⊗ {(!ₒ A)} {(!ₒ B)} ⊗ₐ id {(!ₒ B)})
  ○ (id {(!ₒ A)} ⊗ₐ α⊗ {(!ₒ B)} {(!ₒ A)} {(!ₒ B)}
  ○ α⊗-inv {(!ₒ A)} {(!ₒ B)} {(!ₒ A) ⊗ₒ (!ₒ B)})))

d-diag-L : ∀{A B : Obj}
  → m⊗ {A} {B} ○ d {A ⊗ₒ B} ≡h ((d {A}) ⊗ₐ (d {B})) ○ (iso ○ ((m⊗ {A}{B}) ⊗ₐ (m⊗ {A}{B})))
d-diag-L {U , X , α}{V , Y , β} = ext-set aux , ext-set (λ {a} → aux' {a})
 where
   aux : {a : U × V}
     →   (a , a)
       ≡ ⟨ (λ x → x) , (λ x → x) ⟩
           (rl-assoc-×
             (⟨ (λ x → x) , lr-assoc-× ⟩
             (⟨ (λ x → x) , ⟨ twist-× , (λ x → x) ⟩ ⟩
             (⟨ (λ x → x) , rl-assoc-× ⟩
             (lr-assoc-× (⟨ (λ x → x , x) , (λ x → x , x) ⟩ a))))))
   aux {u , v} = refl
   -- The type of aux' is the fully expanded version of the following type:
   -- ((λ v u → h'₁ (θ a (u , v)) v u) , (λ u v → h'₂ (θ a (u , v)) u v))
   -- ≡ ((λ v u → fst (fst (F⊗ a) (u , v)) v u ++ fst (snd (F⊗ a) (u , v)) v u)
   --    ,
   --    (λ u u₁ → snd (fst (F⊗ a) (u , u₁)) u u₁ ++ snd (snd (F⊗ a) (u , u₁)) u u₁).
   -- Agda's type inference algorithm was having trouble inferring the annotations, and
   -- so we used Agda to generate the fully expanded version.
   aux' : {a
       : Σ {_} {_}
         (Σ {_} {_} U (λ x → V) →
          Σ {_} {_} U (λ x → V) →
          𝕃 {_}
          (Σ {_} {_} (V → X)
           (λ x → U → Y)))
         (λ x →
            Σ {_} {_} U (λ x₁ → V) →
            Σ {_} {_} U (λ x₁ → V) →
            𝕃 {_}
            (Σ {_} {_} (V → X)
             (λ x₁ → U → Y)))} →
      _≡_ {_}
      {Σ {_} {_}
       (V → U → 𝕃 {_} X)
       (λ x → U → V → 𝕃 {_} Y)}
      ((λ v u →
          h'₁ {U} {V} {X} {Y}
          (θ {Σ {_} {_} U (λ x → V)}
           {Σ {_} {_} (V → X)
            (λ x → U → Y)}
           a (u , v))
          v u)
       ,
       (λ u v →
          h'₂ {U} {V} {X} {Y}
          (θ {Σ {_} {_} U (λ x → V)}
           {Σ {_} {_} (V → X)
            (λ x → U → Y)}
           a (u , v))
          u v))
      ((λ v u →
          _++_ {_} {X}
          (fst {_} {_}
           {V → U → 𝕃 {_} X}
           {U → V → 𝕃 {_} Y}
           (fst {_} {_}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            (F⊗ {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {λ x → x}
             {λ g →
                (λ v₁ u₁ → h'₁ {U} {V} {X} {Y} (g (u₁ , v₁)) v₁ u₁) ,
                (λ u₁ v₁ → h'₂ {U} {V} {X} {Y} (g (u₁ , v₁)) u₁ v₁)}
             {λ x → x}
             {λ g →
                (λ v₁ u₁ → h'₁ {U} {V} {X} {Y} (g (u₁ , v₁)) v₁ u₁) ,
                (λ u₁ v₁ → h'₂ {U} {V} {X} {Y} (g (u₁ , v₁)) u₁ v₁)}
             a)
            (u , v))
           v u)
          (fst {_} {_}
           {V → U → 𝕃 {_} X}
           {U → V → 𝕃 {_} Y}
           (snd {_} {_}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            (F⊗ {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {λ x → x}
             {λ g →
                (λ v₁ u₁ → h'₁ {U} {V} {X} {Y} (g (u₁ , v₁)) v₁ u₁) ,
                (λ u₁ v₁ → h'₂ {U} {V} {X} {Y} (g (u₁ , v₁)) u₁ v₁)}
             {λ x → x}
             {λ g →
                (λ v₁ u₁ → h'₁ {U} {V} {X} {Y} (g (u₁ , v₁)) v₁ u₁) ,
                (λ u₁ v₁ → h'₂ {U} {V} {X} {Y} (g (u₁ , v₁)) u₁ v₁)}
             a)
            (u , v))
           v u))
       ,
       (λ u u₁ →
          _++_ {_} {Y}
          (snd {_} {_}
           {V → U → 𝕃 {_} X}
           {U → V → 𝕃 {_} Y}
           (fst {_} {_}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            (F⊗ {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {λ x → x}
             {λ g →
                (λ v u₂ → h'₁ {U} {V} {X} {Y} (g (u₂ , v)) v u₂) ,
                (λ u₂ v → h'₂ {U} {V} {X} {Y} (g (u₂ , v)) u₂ v)}
             {λ x → x}
             {λ g →
                (λ v u₂ → h'₁ {U} {V} {X} {Y} (g (u₂ , v)) v u₂) ,
                (λ u₂ v → h'₂ {U} {V} {X} {Y} (g (u₂ , v)) u₂ v)}
             a)
            (u , u₁))
           u u₁)
          (snd {_} {_}
           {V → U → 𝕃 {_} X}
           {U → V → 𝕃 {_} Y}
           (snd {_} {_}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            {Σ {_} {_} U (λ x → V) →
             Σ {_} {_}
             (V → U → 𝕃 {_} X)
             (λ x → U → V → 𝕃 {_} Y)}
            (F⊗ {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_} U (λ x → V) →
              𝕃 {_}
              (Σ {_} {_} (V → X)
               (λ x → U → Y))}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {Σ {_} {_} U (λ x → V)}
             {Σ {_} {_}
              (V → U → 𝕃 {_} X)
              (λ x → U → V → 𝕃 {_} Y)}
             {λ x → x}
             {λ g →
                (λ v u₂ → h'₁ {U} {V} {X} {Y} (g (u₂ , v)) v u₂) ,
                (λ u₂ v → h'₂ {U} {V} {X} {Y} (g (u₂ , v)) u₂ v)}
             {λ x → x}
             {λ g →
                (λ v u₂ → h'₁ {U} {V} {X} {Y} (g (u₂ , v)) v u₂) ,
                (λ u₂ v → h'₂ {U} {V} {X} {Y} (g (u₂ , v)) u₂ v)}
             a)
            (u , u₁))
           u u₁)))
   aux' {j₁ , j₂} =
     cong2
      {a = λ v u → h'₁ (j₁ (u , v) (u , v) ++ j₂ (u , v) (u , v)) v u}
      _,_ (ext-set
              (λ {v} → ext-set
                          (λ {u} → sym (h'₁-append
                                          {l₁ = j₁ (u , v) (u , v)}
                                          {l₂ = j₂ (u , v) (u , v)}{v}{u}))))
          (ext-set
              (λ {u} → (ext-set
                           (λ {v} → sym (h'₂-append
                                          {l₁ = j₁ (u , v) (u , v)}
                                          {l₂ = j₂ (u , v) (u , v)}{u}{v})))))

-- Show that (!A, d, e) is a commutative comonoid.  The following
-- diagrams can be found on page 29 of the report.
de-diag-M : ∀{A : Obj}
  → ρ⊗-inv {(!ₒ A)} ≡h (d {A}) ○ ((id {(!ₒ A)}) ⊗ₐ (e {A}))
de-diag-M {U , X , α} = refl , ext-set (λ {a} → aux {a})
 where
   aux : {a : Σ (⊤ → U → 𝕃 X) (λ x → U → ⊤)}
       →   (fst a triv)
         ≡ (θ (F⊗ {f = λ x → x} {λ x → x} {λ x → triv} {λ x u → []} a))
   aux {j₁ , j₂} = ext-set (λ {u} → sym (++[] (j₁ triv u)))

de-diag-N : ∀{A : Obj}
  → λ⁻¹⊗ {(!ₒ A)} ≡h (d {A}) ○ ((e {A}) ⊗ₐ (id {(!ₒ A)}))
de-diag-N {U , X , α} = refl , ext-set (λ {a} → aux {a})
 where
   aux : {a : Σ (U → ⊤) (λ x → ⊤ → U → 𝕃 X)} →
       _≡_ (snd a triv) (θ (F⊗ {f = λ x → triv}
                               {λ x u → []}
                               {λ x → x}
                               {λ x → x} a))
   aux {j₁ , j₂} = refl

de-diag-O : ∀{A : Obj}
  → d {A} ≡h (d {A}) ○ (β⊗ {(!ₒ A)}{(!ₒ A)})
de-diag-O {U , X , α} = refl , ext-set (λ {a} → aux {a})
 where
   aux : {a : Σ (U → U → 𝕃 X) (λ x → U → U → 𝕃 X)}
     → θ a ≡ θ (twist-× a)
   aux {j₁ , j₂} = ext-set (λ {u} → *-comm {l₁ = j₁ u u}{j₂ u u})

de-diag-P : ∀{A : Obj}
  →      (d {A})
       ○ (((d {A}) ⊗ₐ (id {(!ₒ A)}))
       ○ (α⊗ {(!ₒ A)}{(!ₒ A)}{(!ₒ A)}))
    ≡h (d {A}) ○ ((id {(!ₒ A)}) ⊗ₐ (d {A}))
de-diag-P {U , X , α} = refl , ext-set ((λ {a} → aux {a}))
 where
   aux : {a : Σ (Σ U (λ x → U) → U → 𝕃 X)
                    (λ x → U → Σ (U → U → 𝕃 X)
                (λ x₁ → U → U → 𝕃 X))}
     →   (θ (F⊗ {f = λ x → x , x} {θ {U} {X}} {λ x → x} {λ x → x}
                (Fα {U} {U} {U → 𝕃 X} {U → 𝕃 X} {U} {U} {U → 𝕃 X} a)))
       ≡ (θ (F⊗ {Σ U (λ x → U)} {U → 𝕃 X} {U}
                {Σ (U → U → 𝕃 X) (λ x → U → U → 𝕃 X)}
                {U} {U → 𝕃 X} {U} {U → 𝕃 X} {λ x → x}
                {λ x → x} {λ x → x , x} {θ} a))
   aux {x , y} = ext-set (λ {u} → aux')
    where
      aux' : ∀{u : U}
        →   (x (u , u) u ++ fst (y u) u u) ++ snd (y u) u u
          ≡ x (u , u) u ++ θ (y u) u
      aux' {u} with y u
      ... | j₁ , j₂ = ++-assoc (x (u , u) u) (j₁ u u) (j₂ u u)

-- The morphism e and d must be a coalgebra morphisms.  The following
-- diagram can be found on page 30 of the report.
e-diag-Q : ∀{A : Obj}
  → δ {A} ○ !ₐ (e {A}) ≡h (e {A}) ○ m⊤
e-diag-Q {U , X , α} =
  refl , ext-set (λ {a} → ext-set (λ {u} → aux {a triv}))
 where
   aux : ∀{l : ⊤ *}{u : U} → _≡_ {_} {𝕃 {_} X}
      (foldr {_} {_}
       {U → 𝕃 {_} X} {𝕃 {_} X}
       (λ f → _++_ {_} {X} (f u)) []
       (map {_} {_} {⊤}
        {U → 𝕃 {_} X} (λ x u₁ → []) l))
      []
   aux {[]} = refl
   aux {x :: l}{u} = aux {l}{u}

d-diag-R : ∀{A : Obj}
  → δ {A} ○ !ₐ (d {A}) ≡h (d {A}) ○ (((δ {A}) ⊗ₐ (δ {A})) ○ (m⊗ {(!ₒ A)}{(!ₒ A)}))
d-diag-R {U , X , α} = refl , ext-set (λ {a} → ext-set (λ {u} → aux {a (u , u)}{u}))
 where
   aux : ∀{l : 𝕃 (Σ (U → U → 𝕃 X) (λ x → U → U → 𝕃 X))}{u : U}
     →   foldr (λ f → _++_ (f u)) [] (map θ l)
       ≡ foldr (λ f → _++_ (f u)) [] (h'₁ l u u) ++
         foldr (λ f → _++_ (f u)) [] (h'₂ l u u)
   aux {[]} = refl
   aux {(j₁ , j₂) :: js}{u}
     rewrite
       ++-assoc (j₁ u u)
                (foldr (λ f → _++_ (f u)) [] (h'₁ js u u))
                (j₂ u u ++ foldr (λ f → _++_ (f u)) [] (h'₂ js u u))
     | sym (++-assoc (foldr (λ f → _++_ (f u)) [] (h'₁ js u u))
                     (j₂ u u)
                     (foldr (λ f → _++_ (f u)) [] (h'₂ js u u)))
     | *-comm {l₁ = foldr (λ f → _++_ (f u)) [] (h'₁ js u u)}{j₂ u u}
     | ++-assoc (j₂ u u)
                (foldr (λ f → _++_ (f u)) [] (h'₁ js u u))
                (foldr (λ f → _++_ (f u)) [] (h'₂ js u u))
     | sym (++-assoc (j₁ u u)
                     (j₂ u u)
                     (foldr (λ f → _++_ (f u)) [] (h'₁ js u u) ++
                      foldr (λ f → _++_ (f u)) [] (h'₂ js u u)))
     | aux {js}{u}
    = refl

-- The following diagrams can be found on page 31 of the report.
diag-S : ∀{A B : Obj}{f : Hom (!ₒ A) (!ₒ B)}
  → ((δ {A}) ○ (!ₐ f)) ≡h (f ○ (δ {B}))
  → f ○ (e {B}) ≡h e {A}
diag-S {U , X , _}{V , Y , _}{f , F , _} (p , p') =
  refl , ext-set (λ {a} → ext-set
                           (λ {u} → sym (congf2 {b = λ _ → []}
                                                {λ _ → []}{u}{u}
                                                p' refl refl)))

diag-T : ∀{A B : Obj}{f : Hom (!ₒ A) (!ₒ B)}
  → ((δ {A}) ○ (!ₐ f)) ≡h (f ○ (δ {B}))
  → f ○ d {B} ≡h (d {A}) ○ (f ⊗ₐ f)
diag-T {U , X , _}{V , Y , _}{f , F , _} (p , p') =
  refl , ext-set (λ {a} → aux {a})
 where
   aux : {a : Σ (V → V → 𝕃 Y) (λ x → V → V → 𝕃 Y)}
     → F (θ a) ≡ θ (F⊗ {f = f}{F}{f}{F} a)
   aux {j₁ , j₂} = ext-set (λ {u} → aux' {u})
     where
       aux'' : ∀{j₁ j₂ : V → V → 𝕃 Y}
         →   (λ u₁ → j₁ u₁ u₁ ++ j₂ u₁ u₁ ++ [])
           ≡ λ u₁ → j₁ u₁ u₁ ++ j₂ u₁ u₁
       aux'' {j₁}{j₂} =
         ext-set (λ {v} → cong2 {a = j₁ v v}
                                {j₁ v v}
                                {j₂ v v ++ []}
                                {j₂ v v}
                                _++_
                                refl
                                (++[] (j₂ v v)))
       aux' : ∀{u : U}
         →   F (λ u₁ → j₁ u₁ u₁ ++ j₂ u₁ u₁) u
           ≡ F (j₁ (f u)) u ++ F (j₂ (f u)) u
       aux' {u} with
         congf2 {b = λ x → j₁ x :: j₂ x :: []}
                {λ x → j₁ x :: j₂ x :: []}
                {u}{u}
                p' refl refl
       ... | p'' rewrite
           ++[] (F (j₂ (f u)) u)
         | aux'' {j₁}{j₂} = sym p''

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Nat
open import Prelude
open import List
open import core

-- erasure of cursor in the types and expressions is defined in the paper,
-- and in the core file, as a function on zexpressions. because of the
-- particular encoding of all the judgments as datatypes and the agda
-- semantics for pattern matching, it is sometimes also convenient to have
-- a judgemental form of erasure.
--
-- this file describes the obvious encoding of the view this function as a
-- jugement relating input and output as a datatype, and argues that this
-- encoding is correct by showing a isomorphism with the function. we also
-- show that as a correlary, the judgement is well moded at (∀, ∃!), which
-- is unsurprising if the jugement is written correctly.
--
-- taken together, these proofs allow us to move between the judgemental
-- form of erasure and the function form when it's convenient.
--
-- while we do not have it, the argument given here is sufficiently strong
-- to produce an equality between these things in a system with the
-- univalence axiom, as described in the homotopy type theory book and the
-- associated work done in agda.
module judgemental-erase where

  --cursor erasure for types, as written in the paper
  _◆t : τ̂ → τ̇
  ▹ t ◃ ◆t =  t
  (t1 ==>₁ t2) ◆t = (t1 ◆t) ==> t2
  (t1 ==>₂ t2) ◆t = t1 ==> (t2 ◆t)

  --cursor erasure for expressions, as written in the paper
  _◆e : ê → ė
  ▹ x ◃ ◆e       = x
  (e ·:₁ t) ◆e   = (e ◆e) ·: t
  (e ·:₂ t) ◆e   = e      ·: (t ◆t)
  ·λ x e ◆e      = ·λ x (e ◆e)
  (e1 ∘₁ e2) ◆e  = (e1 ◆e) ∘ e2
  (e1 ∘₂ e2) ◆e  = e1      ∘ (e2 ◆e)
  (e1 ·+₁ e2) ◆e = (e1 ◆e) ·+ e2
  (e1 ·+₂ e2) ◆e = e1      ·+ (e2 ◆e)
  ⦇⌜ e ⌟⦈ ◆e     = ⦇⌜ e ◆e ⌟⦈

  -- this pair of theorems moves from the judgmental form to the function form
  erase-t◆ : {t : τ̂} {tr : τ̇} → (erase-t t tr) → (t ◆t == tr)
  erase-t◆ ETTop       = refl
  erase-t◆ (ETArrL p)  = ap1 (λ x → x ==> _) (erase-t◆ p)
  erase-t◆ (ETArrR p)  = ap1 (λ x → _ ==> x) (erase-t◆ p)

  erase-e◆ : {e : ê} {er : ė} → (erase-e e er) → (e ◆e == er)
  erase-e◆ EETop       = refl
  erase-e◆ (EEAscL p)  with erase-e◆ p
  erase-e◆ (EEAscL p) | refl = refl -- ap1 (λ x → x ·: _)  (erase-e◆ p)
  erase-e◆ (EEAscR p)  = ap1 (λ x → _ ·: x)  (erase-t◆ p)
  erase-e◆ (EELam p)   = ap1 (λ e → ·λ _ e)  (erase-e◆ p)
  erase-e◆ (EEApL p)   = ap1 (λ x → x ∘ _)   (erase-e◆ p)
  erase-e◆ (EEApR p)   = ap1 (λ x → _ ∘ x)   (erase-e◆ p)
  erase-e◆ (EEPlusL p) = ap1 (λ x → x ·+ _)  (erase-e◆ p)
  erase-e◆ (EEPlusR p) = ap1 (λ x → _ ·+ x)  (erase-e◆ p)
  erase-e◆ (EENEHole p) = ap1 (λ x → ⦇⌜ x ⌟⦈) (erase-e◆ p)

  -- this pair of theorems moves back from judgmental form to the function form
  ◆erase-t : (t : τ̂) (tr : τ̇) → (t ◆t == tr) → (erase-t t tr)
  ◆erase-t ▹ x ◃ .x refl = ETTop
  ◆erase-t (t ==>₁ x) (.(t ◆t) ==> .x) refl with ◆erase-t t (t ◆t) refl
  ... | ih = ETArrL ih
  ◆erase-t (x ==>₂ t) (.x ==> .(t ◆t)) refl with ◆erase-t t (t ◆t) refl
  ... | ih = ETArrR ih

  ◆erase-e : (e : ê) (er : ė) → (e ◆e == er) → (erase-e e er)
  ◆erase-e ▹ x ◃ .x refl = EETop
  ◆erase-e (e ·:₁ x) .((e ◆e) ·: x) refl with ◆erase-e e (e ◆e) refl
  ... | ih = EEAscL ih
  ◆erase-e (x ·:₂ x₁) .(x ·: (x₁ ◆t)) refl = EEAscR (◆erase-t x₁ (x₁ ◆t) refl)
  ◆erase-e (·λ x e) .(·λ x (e ◆e)) refl = EELam (◆erase-e e (e ◆e) refl)
  ◆erase-e (e ∘₁ x) .((e ◆e) ∘ x) refl = EEApL (◆erase-e e (e ◆e) refl)
  ◆erase-e (x ∘₂ e) .(x ∘ (e ◆e)) refl = EEApR (◆erase-e e (e ◆e) refl)
  ◆erase-e (e ·+₁ x) .((e ◆e) ·+ x) refl = EEPlusL (◆erase-e e (e ◆e) refl)
  ◆erase-e (x ·+₂ e) .(x ·+ (e ◆e)) refl = EEPlusR (◆erase-e e (e ◆e) refl)
  ◆erase-e ⦇⌜ e ⌟⦈ .(⦇⌜ e ◆e ⌟⦈) refl = EENEHole (◆erase-e e (e ◆e) refl)

  -- jugemental erasure for both types and terms only has one proof for
  -- relating the a term to its non-judgemental erasure
  t-contr : (t : τ̂) → (x y : erase-t t (t ◆t)) → x == y
  t-contr ▹ x ◃ ETTop ETTop = refl
  t-contr (t ==>₁ x) (ETArrL y) (ETArrL z) = ap1 ETArrL (t-contr t y z)
  t-contr (x ==>₂ t) (ETArrR y) (ETArrR z) = ap1 ETArrR (t-contr t y z)

  e-contr : (e : ê) → (x y : erase-e e (e ◆e)) → x == y
  e-contr ▹ x ◃ EETop EETop = refl
  e-contr (e ·:₁ x) (EEAscL x₁) (EEAscL y) = ap1 EEAscL (e-contr e x₁ y)
  e-contr (x₁ ·:₂ x) (EEAscR x₂) (EEAscR x₃) = ap1 EEAscR (t-contr x x₂ x₃)
  e-contr (·λ x e) (EELam x₁) (EELam y) = ap1 EELam (e-contr e x₁ y)
  e-contr (e ∘₁ x) (EEApL x₁) (EEApL y) = ap1 EEApL (e-contr e x₁ y)
  e-contr (x ∘₂ e) (EEApR x₁) (EEApR y) = ap1 EEApR (e-contr e x₁ y)
  e-contr (e ·+₁ x) (EEPlusL x₁) (EEPlusL y) = ap1 EEPlusL (e-contr e x₁ y)
  e-contr (x ·+₂ e) (EEPlusR x₁) (EEPlusR y) = ap1 EEPlusR (e-contr e x₁ y)
  e-contr ⦇⌜ e ⌟⦈ (EENEHole x) (EENEHole y) = ap1 EENEHole (e-contr e x y)

  -- taken together, these four theorems demonstrate that both round-trips
  -- of the above functions are stable up to ==
  erase-trt1 : (t : τ̂) (tr : τ̇) → (x : t ◆t == tr) → (erase-t◆ (◆erase-t t tr x)) == x
  erase-trt1 ▹ x ◃ .x refl = refl
  erase-trt1 (t ==>₁ x) (.(t ◆t) ==> .x) refl with erase-t◆ (◆erase-t t (t ◆t) refl)
  erase-trt1 (t ==>₁ x) (.(t ◆t) ==> .x) refl | refl = refl
  erase-trt1 (x ==>₂ t) (.x ==> .(t ◆t)) refl with erase-t◆ (◆erase-t t (t ◆t) refl)
  erase-trt1 (x ==>₂ t) (.x ==> .(t ◆t)) refl | refl = refl

  erase-trt2 : (t : τ̂) (tr : τ̇) → (x : erase-t t tr) → ◆erase-t t tr (erase-t◆ x) == x
  erase-trt2 .(▹ tr ◃) tr ETTop = refl
  erase-trt2 _ _ (ETArrL ETTop) = refl
  erase-trt2 (t1 ==>₁ t2) _ (ETArrL x) with erase-t◆ x
  erase-trt2 (t1 ==>₁ t2) _ (ETArrL x) | refl = ap1 ETArrL (t-contr _ (◆erase-t t1 (t1 ◆t) refl) x)
  erase-trt2 (t1 ==>₂ t2) _ (ETArrR x) with erase-t◆ x
  erase-trt2 (t1 ==>₂ t2) _ (ETArrR x) | refl = ap1 ETArrR (t-contr _ (◆erase-t t2 (t2 ◆t) refl) x)

  erase-ert1 : (e : ê) (er : ė) → (x : e ◆e == er) → (erase-e◆ (◆erase-e e er x)) == x
  erase-ert1 ▹ x ◃ .x refl = refl
  erase-ert1 (e ·:₁ x) .((e ◆e) ·: x) refl with erase-e◆ (◆erase-e e (e ◆e) refl)
  erase-ert1 (e ·:₁ x) .((e ◆e) ·: x) refl | refl = refl
  erase-ert1 (x ·:₂ t) .(x ·: (t ◆t)) refl =  ap1 (λ a → ap1 (_·:_ x) a) (erase-trt1 t _ refl)
  erase-ert1 (·λ x e) .(·λ x (e ◆e)) refl = ap1 (λ a → ap1 (·λ x) a) (erase-ert1 e _ refl)
  erase-ert1 (e ∘₁ x) .((e ◆e) ∘ x) refl =  ap1 (λ a → ap1 (λ x₁ → x₁ ∘ x) a) (erase-ert1 e _ refl)
  erase-ert1 (x ∘₂ e) .(x ∘ (e ◆e)) refl = ap1 (λ a → ap1 (_∘_ x) a) (erase-ert1 e _ refl)
  erase-ert1 (e ·+₁ x) .((e ◆e) ·+ x) refl = ap1 (λ a → ap1 (λ x₁ → x₁ ·+ x) a) (erase-ert1 e _ refl)
  erase-ert1 (x ·+₂ e) .(x ·+ (e ◆e)) refl = ap1 (λ a → ap1 (_·+_ x) a) (erase-ert1 e _ refl)
  erase-ert1 ⦇⌜ e ⌟⦈ .(⦇⌜ e ◆e ⌟⦈) refl = ap1 (λ a → ap1 ⦇⌜_⌟⦈ a) (erase-ert1 e _ refl)

  erase-ert2 : (e : ê) (er : ė) → (b : erase-e e er) → ◆erase-e e er (erase-e◆ b) == b
  erase-ert2 .(▹ er ◃) er EETop = refl
  erase-ert2 (e ·:₁ x) _ (EEAscL b) with erase-e◆ b
  erase-ert2 (e ·:₁ x) _ (EEAscL b) | refl = ap1 EEAscL (e-contr _ (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e ·:₂ x) _ (EEAscR b) with erase-t◆ b
  erase-ert2 (e ·:₂ x) .(e ·: (x ◆t)) (EEAscR b) | refl = ap1 EEAscR (t-contr _ (◆erase-t x (x ◆t) refl) b)
  erase-ert2 (·λ x e) _ (EELam b) with erase-e◆ b
  erase-ert2 (·λ x e) .(·λ x (e ◆e)) (EELam b) | refl = ap1 EELam (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e ∘₁ x) _ (EEApL b) with erase-e◆ b
  erase-ert2 (e ∘₁ x) .((e ◆e) ∘ x) (EEApL b) | refl = ap1 EEApL (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e1 ∘₂ e) _ (EEApR b) with erase-e◆ b
  erase-ert2 (e1 ∘₂ e) .(e1 ∘ (e ◆e)) (EEApR b) | refl = ap1 EEApR (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e ·+₁ x) _ (EEPlusL b) with erase-e◆ b
  erase-ert2 (e ·+₁ x) .((e ◆e) ·+ x) (EEPlusL b) | refl = ap1 EEPlusL (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 (e1 ·+₂ e) _ (EEPlusR b) with erase-e◆ b
  erase-ert2 (e1 ·+₂ e) .(e1 ·+ (e ◆e)) (EEPlusR b) | refl = ap1 EEPlusR (e-contr e (◆erase-e e (e ◆e) refl) b)
  erase-ert2 ⦇⌜ e ⌟⦈ _ (EENEHole b) with erase-e◆ b
  erase-ert2 ⦇⌜ e ⌟⦈ .(⦇⌜ e ◆e ⌟⦈) (EENEHole b) | refl = ap1 EENEHole (e-contr e (◆erase-e e (e ◆e) refl) b)

  -- since both round trips are stable, these functions demonstrate
  -- isomorphisms between the jugemental and non-judgemental definitions of
  -- erasure
  erase-e-iso : (e : ê) (er : ė) → (e ◆e == er) ≃ (erase-e e er)
  erase-e-iso e er = (◆erase-e e er) , (erase-e◆ , erase-ert1 e er , erase-ert2 e er)

  erase-t-iso : (t : τ̂) (tr : τ̇) → (t ◆t == tr) ≃ (erase-t t tr)
  erase-t-iso t tr = (◆erase-t t tr) , (erase-t◆ , erase-trt1 t tr , erase-trt2 t tr)

  -- this isomorphism supplies the argument that the judgement has mode (∀,
  -- !∃), where uniqueness comes from erase-e◆.
  erase-e-mode : (e : ê) → Σ[ er ∈ ė ] (erase-e e er)
  erase-e-mode e = (e ◆e) , (◆erase-e e (e ◆e) refl)

  -- some translations and lemmas to move between the different
  -- forms. these are not needed to show that this is an ok encoding pair,
  -- but they are helpful when actually using it.

  -- even more specifically, the relation relates an expression to its
  -- functional erasure.
  rel◆t : (t : τ̂) → (erase-t t (t ◆t))
  rel◆t t = ◆erase-t t (t ◆t) refl

  rel◆ : (e : ê) → (erase-e e (e ◆e))
  rel◆ e = ◆erase-e e (e ◆e) refl

  lem-erase-synth : ∀{e e' Γ t} → erase-e e e' → Γ ⊢ e' => t → Γ ⊢ (e ◆e) => t
  lem-erase-synth er wt = tr (λ x → _ ⊢ x => _) (! (erase-e◆ er)) wt

  lem-erase-ana : ∀{e e' Γ t} → erase-e e e' → Γ ⊢ e' <= t → Γ ⊢ (e ◆e) <= t
  lem-erase-ana er wt = tr (λ x → _ ⊢ x <= _) (! (erase-e◆ er)) wt

  lem-synth-erase : ∀{Γ e t e' } → Γ ⊢ e ◆e => t → erase-e e e' → Γ ⊢ e' => t
  lem-synth-erase d1 d2 with erase-e◆ d2
  ... | refl = d1

  eraset-det : ∀{t t' t''} → erase-t t t' → erase-t t t'' → t' == t''
  eraset-det e1 e2 with erase-t◆ e1
  ... | refl = erase-t◆ e2

  erasee-det : ∀{e e' e''} → erase-e e e' → erase-e e e'' → e' == e''
  erasee-det e1 e2 with erase-e◆ e1
  ... | refl = erase-e◆ e2

  erase-in-hole : ∀ {e e'} → erase-e e e' → erase-e ⦇⌜ e ⌟⦈ ⦇⌜ e' ⌟⦈
  erase-in-hole (EENEHole er) = EENEHole (erase-in-hole er)
  erase-in-hole x = EENEHole x

  eq-er-trans : ∀{e e◆ e'} →
                    (e ◆e) == (e' ◆e) →
                    erase-e e e◆ →
                    erase-e e' e◆
  eq-er-trans {e} {e◆} {e'} eq er = tr (λ f → erase-e e' f) (erasee-det (◆erase-e e (e' ◆e) eq) er) (rel◆ e')

  eq-ert-trans : ∀{t t' t1 t2} →
                (t ◆t) == (t' ◆t) →
                erase-t t t1 →
                erase-t t' t2 →
                t1 == t2
  eq-ert-trans eq er1 er2 = ! (erase-t◆ er1) · (eq · (erase-t◆ er2))


text:
open import Relation.Binary hiding (_⇒_)
open import Level

module Relation.Unary.Monotone {c i}(pre : Preorder i c i) where

open Preorder pre renaming (Carrier to I; _∼_ to _≤_)
open import Relation.Unary
open import Data.Product hiding (map)
open import Data.List
open import Function

record Monotone {ℓ}(p : Pred I ℓ) : Set (i ⊔ ℓ) where
  field wk : ∀ {i j} → i ≤ j → p i → p j

open Monotone
open Monotone ⦃...⦄ public

∀≥[_] : ∀ {ℓ} → Pred I ℓ → Pred I (i ⊔ ℓ)
∀≥[ P ] i = ∀ {j} → i ≤ j → P j

∃≥[_] : ∀ {ℓ} → Pred I ℓ → Pred I (i ⊔ ℓ)
∃≥[ P ] i = ∃ λ j → i ≤ j × P j

infixr 4 _↗_
_↗_ : ∀ {ℓ} → Pred I ℓ → Pred I ℓ → Pred I (i ⊔ ℓ)
(P ↗ Q) = ∀≥[ P ⇒ Q ]

instance
  ∀≥-monotone : ∀ {ℓ}{P : Pred I ℓ} → Monotone ∀≥[ P ]
  wk ∀≥-monotone ext f ext' = f (trans ext ext')

  mono-∩ : ∀ {i j}{p : Pred I i}{q : Pred I j}
             ⦃ wp : Monotone p ⦄ ⦃ wq : Monotone q ⦄ → Monotone (p ∩ q)
  wk (mono-∩ ⦃ wp ⦄ ⦃ wq ⦄) ext (x , y) = (wk wp ext x , wk wq ext y)

  list-monotone : ∀ {B : Pred I i}⦃ wb : Monotone B ⦄ → Monotone (λ W → List (B W))
  wk (list-monotone ⦃ wₐ ⦄) ext v = map (wk wₐ ext) v

  open import Data.List.All as All
  all-monotone : ∀ {b i}{B : Set b}{xs : List B}{C : B → Pred I i}
                 ⦃ wₐ : ∀ x → Monotone (C x) ⦄ →
                 Monotone (λ ys → All (λ x → C x ys) xs)
  wk (all-monotone ⦃ wₐ ⦄) ext v = All.map (λ {a} y → wk (wₐ a) ext y) v

  open import Data.Vec using (Vec)
  open import Data.Vec.All as VAll
  vec-all-monotone : ∀ {b i n}{B : Set b}{xs : Vec B n}{C : B → Pred I i}
                 ⦃ wₐ : ∀ x → Monotone (C x) ⦄ →
                 Monotone (λ ys → VAll.All (λ x → C x ys) xs)
  wk (vec-all-monotone ⦃ wₐ ⦄) ext v = VAll.map (λ {a} y → wk (wₐ a) ext y) v

  ≤-mono : ∀ {i} → Monotone (_≤_ i)
  wk ≤-mono = flip trans

  open import Data.Maybe as Maybe
  maybe-monotone : ∀ {i}{P : Pred I i} ⦃ mono : Monotone P ⦄ → Monotone (λ W → Maybe (P W))
  wk (maybe-monotone ⦃ mono ⦄) ext mv = Maybe.map (wk mono ext) mv


text:
module AKS.Nat where

open import AKS.Nat.Base public
open import AKS.Nat.Properties public
open import AKS.Nat.WellFounded public
open import AKS.Nat.Divisibility public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A pointwise lifting of a relation to incorporate new extrema.
-------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Extrema

open import Relation.Binary

module Relation.Binary.Construct.Add.Extrema.Equality
  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Function using (_∘′_)
import Relation.Binary.Construct.Add.Infimum.Equality as AddInfimum
import Relation.Binary.Construct.Add.Supremum.Equality as AddSupremum
open import Relation.Nullary.Construct.Add.Extrema

-------------------------------------------------------------------------
-- Definition

private
  module Inf = AddInfimum _≈_
  module Sup = AddSupremum (Inf._≈₋_)

open Sup using () renaming (_≈⁺_ to _≈±_) public

-------------------------------------------------------------------------
-- Useful pattern synonyms

pattern ⊥±≈⊥± = Sup.[ Inf.⊥₋≈⊥₋ ]
pattern [_] p = Sup.[ Inf.[ p ] ]
pattern ⊤±≈⊤± = Sup.⊤⁺≈⊤⁺

-------------------------------------------------------------------------
-- Relational properties

[≈]-injective : ∀ {k l} → [ k ] ≈± [ l ] → k ≈ l
[≈]-injective = Inf.[≈]-injective ∘′ Sup.[≈]-injective

≈±-refl : Reflexive _≈_ → Reflexive _≈±_
≈±-refl = Sup.≈⁺-refl ∘′ Inf.≈₋-refl

≈±-sym : Symmetric _≈_ → Symmetric _≈±_
≈±-sym = Sup.≈⁺-sym ∘′ Inf.≈₋-sym

≈±-trans : Transitive _≈_ → Transitive _≈±_
≈±-trans = Sup.≈⁺-trans ∘′ Inf.≈₋-trans

≈±-dec : Decidable _≈_ → Decidable _≈±_
≈±-dec = Sup.≈⁺-dec ∘′ Inf.≈₋-dec

≈±-irrelevant : Irrelevant _≈_ → Irrelevant _≈±_
≈±-irrelevant = Sup.≈⁺-irrelevant ∘′ Inf.≈₋-irrelevant

≈±-substitutive : ∀ {ℓ} → Substitutive _≈_ ℓ → Substitutive _≈±_ ℓ
≈±-substitutive = Sup.≈⁺-substitutive ∘′ Inf.≈₋-substitutive

-------------------------------------------------------------------------
-- Structures

≈±-isEquivalence : IsEquivalence _≈_ → IsEquivalence _≈±_
≈±-isEquivalence = Sup.≈⁺-isEquivalence ∘′ Inf.≈₋-isEquivalence

≈±-isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence _≈±_
≈±-isDecEquivalence = Sup.≈⁺-isDecEquivalence ∘′ Inf.≈₋-isDecEquivalence


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

module Number.Operations where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Function.Base using (_$_)

open import Number.Postulates
open import Number.Base
open import Number.Coercions

open import Number.Operations.Specification
open import Number.Operations.Details
open import Number.Operations.Details using (_⁻¹; -_) public

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

-- infixl 6 _-_
infixl 7 _·_
infixl 6 _+_
infixl 4 _#_
infixl 4 _<_
infixl 4 _≤_

-- homogeneous operations

private
  _+ʰ_ : ∀{l p q} → Number (l , p) → Number (l , q) → Number (l , +-Positivityʰ l p q)
  _+ʰ_ {isNat    } x y = (num x +ⁿ num y) ,, (x +ʰⁿ y)
  _+ʰ_ {isInt    } x y = (num x +ᶻ num y) ,, (x +ʰᶻ y)
  _+ʰ_ {isRat    } x y = (num x +ᶠ num y) ,, (x +ʰᶠ y)
  _+ʰ_ {isReal   } x y = (num x +ʳ num y) ,, (x +ʰʳ y)
  _+ʰ_ {isComplex} x y = (num x +ᶜ num y) ,, (x +ʰᶜ y)

  _·ʰ_ : ∀{l p q} → Number (l , p) → Number (l , q) → Number (l , ·-Positivityʰ l p q)
  _·ʰ_ {isNat    } x y = (num x ·ⁿ num y) ,, (x ·ʰⁿ y)
  _·ʰ_ {isInt    } x y = (num x ·ᶻ num y) ,, (x ·ʰᶻ y)
  _·ʰ_ {isRat    } x y = (num x ·ᶠ num y) ,, (x ·ʰᶠ y)
  _·ʰ_ {isReal   } x y = (num x ·ʳ num y) ,, (x ·ʰʳ y)
  _·ʰ_ {isComplex} x y = (num x ·ᶜ num y) ,, (x ·ʰᶜ y)

  _<ʰ_ : ∀{L} → (x y : NumberKindInterpretation L) → Type (NumberKindProplevel L)
  _<ʰ_ {isNat}     x y = x <ⁿ y
  _<ʰ_ {isInt}     x y = x <ᶻ y
  _<ʰ_ {isRat}     x y = x <ᶠ y
  _<ʰ_ {isReal}    x y = x <ʳ y
  -- NOTE: this is some realization of a partial function, because `_<_` is defined on all numbers
  --       one might already anticipate that this breaks something in the future ...
  _<ʰ_ {isComplex} x y = {{p : ⊥}} → Lift ⊥

  _≤ʰ_ : ∀{L} → (x y : NumberKindInterpretation L) → Type (NumberKindProplevel L)
  _≤ʰ_ {isNat}     x y = x ≤ⁿ y
  _≤ʰ_ {isInt}     x y = x ≤ᶻ y
  _≤ʰ_ {isRat}     x y = x ≤ᶠ y
  _≤ʰ_ {isReal}    x y = x ≤ʳ y
  -- NOTE: this is some realization of a partial function, because `_≤_` is defined on all numbers
  --       one might already anticipate that this breaks something in the future ...
  _≤ʰ_ {isComplex} x y = {{p : ⊥}} → Lift ⊥

  _#ʰ_ : ∀{L} → (x y : NumberKindInterpretation L) → Type (NumberKindProplevel L)
  _#ʰ_ {isNat}     x y = x #ⁿ y
  _#ʰ_ {isInt}     x y = x #ᶻ y
  _#ʰ_ {isRat}     x y = x #ᶠ y
  _#ʰ_ {isReal}    x y = x #ʳ y
  _#ʰ_ {isComplex} x y = x #ᶜ y

{- NOTE: this creates a weird Number.L in the Have/Goal display

module _ {Lx Ly Px Py} (x : Number (Lx , Px)) (y : Number (Ly , Py)) where
  private L = maxₙₗ' Lx Ly
  _+_ : Number (L , +-Positivityʰ L (coerce-PositivityKind Lx L Px) (coerce-PositivityKind Ly L Py))
  _+_ =
    let (Lx≤L , Ly≤L) = max-implies-≤ₙₗ₂' Lx Ly
    in coerce Lx L Lx≤L x +ʰ coerce Ly L Ly≤L y
-}

-- inhomogeneous operations

_+_ : ∀{Lx Ly Px Py} → (x : Number (Lx , Px)) (y : Number (Ly , Py))
    → let L = maxₙₗ Lx Ly
      in Number (L , +-Positivityʰ L (coerce-PositivityKind Lx L Px) (coerce-PositivityKind Ly L Py))
_+_ {Lx} {Ly} {Px} {Py} x y =
  let L = maxₙₗ Lx Ly
      (Lx≤L , Ly≤L) = max-implies-≤ₙₗ₂ Lx Ly
  in coerce Lx L Lx≤L x +ʰ coerce Ly L Ly≤L y

_·_ : ∀{Lx Ly Px Py} → (x : Number (Lx , Px)) (y : Number (Ly , Py))
    → let L = maxₙₗ Lx Ly
      in Number (L , ·-Positivityʰ L (coerce-PositivityKind Lx L Px) (coerce-PositivityKind Ly L Py))
_·_ {Lx} {Ly} {Px} {Py} x y =
  let L = maxₙₗ Lx Ly
      (Lx≤L , Ly≤L) = max-implies-≤ₙₗ₂ Lx Ly
  in coerce Lx L Lx≤L x ·ʰ coerce Ly L Ly≤L y

_<_ : ∀{Lx Ly Px Py} → (x : Number (Lx , Px)) (y : Number (Ly , Py)) → Type (NumberKindProplevel (maxₙₗ Lx Ly))
_<_ {Lx} {Ly} {Px} {Py} x y =
  let L = maxₙₗ Lx Ly
      (Lx≤L , Ly≤L) = max-implies-≤ₙₗ₂ Lx Ly
  in num (coerce Lx L Lx≤L x) <ʰ num (coerce Ly L Ly≤L y)

_≤_ : ∀{Lx Ly Px Py} → (x : Number (Lx , Px)) (y : Number (Ly , Py)) → Type (NumberKindProplevel (maxₙₗ Lx Ly))
_≤_ {Lx} {Ly} {Px} {Py} x y =
  let L = maxₙₗ Lx Ly
      (Lx≤L , Ly≤L) = max-implies-≤ₙₗ₂ Lx Ly
  in num (coerce Lx L Lx≤L x) ≤ʰ num (coerce Ly L Ly≤L y)

_#_ : ∀{Lx Ly Px Py} → (x : Number (Lx , Px)) (y : Number (Ly , Py)) → Type (NumberKindProplevel (maxₙₗ Lx Ly))
_#_ {Lx} {Ly} {Px} {Py} x y =
  let L = maxₙₗ Lx Ly
      (Lx≤L , Ly≤L) = max-implies-≤ₙₗ₂ Lx Ly
  in num (coerce Lx L Lx≤L x) #ʰ num (coerce Ly L Ly≤L y)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

module Fragment.Extensions.CSemigroup.Monomial where

open import Fragment.Equational.Theory.Bundles

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Free Σ-magma hiding (_~_)
open import Fragment.Algebra.Homomorphism Σ-magma
open import Fragment.Algebra.Algebra Σ-magma
  using (Algebra; IsAlgebra; Interpretation; Congruence)
open import Fragment.Equational.Model Θ-csemigroup

open import Fragment.Setoid.Morphism using (_↝_)

open import Fragment.Extensions.CSemigroup.Nat

open import Data.Nat using (ℕ; zero; suc; _≟_)
open import Data.Fin using (Fin; #_; zero; suc; toℕ; fromℕ)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using ([]; _∷_)

open import Relation.Nullary using (yes ; no)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Relation.Binary using (Setoid; IsEquivalence)
import Relation.Binary.Reasoning.Setoid as Reasoning

data Monomial : ℕ → Set where
  leaf : ∀ {n} → ℕ⁺ → Monomial (suc n)
  skip : ∀ {n} → Monomial n → Monomial (suc n)
  cons : ∀ {n} → ℕ⁺ → Monomial n → Monomial (suc n)

lift : ∀ {n} → Monomial n → Monomial (suc n)
lift (leaf x)    = leaf x
lift (skip x)    = skip (lift x)
lift (cons x xs) = cons x (lift xs)

_⊗_ : ∀ {n} → Monomial n → Monomial n → Monomial n
leaf x    ⊗ leaf y    = leaf (x + y)
leaf x    ⊗ skip y    = cons x y
leaf x    ⊗ cons y ys = cons (x + y) ys
skip x    ⊗ leaf y    = cons y x
skip x    ⊗ skip y    = skip (x ⊗ y)
skip x    ⊗ cons y ys = cons y (x ⊗ ys)
cons x xs ⊗ leaf y    = cons (x + y) xs
cons x xs ⊗ skip y    = cons x (xs ⊗ y)
cons x xs ⊗ cons y ys = cons (x + y) (xs ⊗ ys)

⊗-cong : ∀ {n} {x y z w : Monomial n}
         → x ≡ y → z ≡ w → x ⊗ z ≡ y ⊗ w
⊗-cong = PE.cong₂ _⊗_

⊗-comm : ∀ {n} (x y : Monomial n) → x ⊗ y ≡ y ⊗ x
⊗-comm (leaf x)    (leaf y)    = PE.cong leaf (+-comm x y)
⊗-comm (leaf x)    (skip y)    = PE.refl
⊗-comm (leaf x)    (cons y ys) = PE.cong₂ cons (+-comm x y) PE.refl
⊗-comm (skip x)    (leaf y)    = PE.refl
⊗-comm (skip x)    (skip y)    = PE.cong skip (⊗-comm x y)
⊗-comm (skip x)    (cons y ys) = PE.cong (cons y) (⊗-comm x ys)
⊗-comm (cons x xs) (leaf y)    = PE.cong₂ cons (+-comm x y) PE.refl
⊗-comm (cons x xs) (skip y)    = PE.cong (cons x) (⊗-comm xs y)
⊗-comm (cons x xs) (cons y ys) = PE.cong₂ cons (+-comm x y) (⊗-comm xs ys)

⊗-assoc : ∀ {n} (x y z : Monomial n) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
⊗-assoc (leaf x)    (leaf y)    (leaf z)    = PE.cong leaf (+-assoc x y z)
⊗-assoc (leaf x)    (leaf y)    (skip z)    = PE.refl
⊗-assoc (leaf x)    (leaf y)    (cons z zs) = PE.cong₂ cons (+-assoc x y z) PE.refl
⊗-assoc (leaf x)    (skip y)    (leaf z)    = PE.refl
⊗-assoc (leaf x)    (skip y)    (skip z)    = PE.refl
⊗-assoc (leaf x)    (skip y)    (cons z zs) = PE.refl
⊗-assoc (leaf x)    (cons y ys) (leaf z)    = PE.cong₂ cons (+-assoc x y z) PE.refl
⊗-assoc (leaf x)    (cons y ys) (skip z)    = PE.refl
⊗-assoc (leaf x)    (cons y ys) (cons z zs) = PE.cong₂ cons (+-assoc x y z) PE.refl
⊗-assoc (skip x)    (leaf y)    (leaf z)    = PE.refl
⊗-assoc (skip x)    (leaf y)    (skip z)    = PE.refl
⊗-assoc (skip x)    (leaf y)    (cons z zs) = PE.refl
⊗-assoc (skip x)    (skip y)    (leaf z)    = PE.refl
⊗-assoc (skip x)    (skip y)    (skip z)    = PE.cong skip (⊗-assoc x y z)
⊗-assoc (skip x)    (skip y)    (cons z zs) = PE.cong (cons z) (⊗-assoc x y zs)
⊗-assoc (skip x)    (cons y ys) (leaf z)    = PE.refl
⊗-assoc (skip x)    (cons y ys) (skip z)    = PE.cong (cons y) (⊗-assoc x ys z)
⊗-assoc (skip x)    (cons y ys) (cons z zs) = PE.cong (cons (y + z)) (⊗-assoc x ys zs)
⊗-assoc (cons x xs) (leaf y)    (leaf z)    = PE.cong₂ cons (+-assoc x y z) PE.refl
⊗-assoc (cons x xs) (leaf y)    (skip z)    = PE.refl
⊗-assoc (cons x xs) (leaf y)    (cons z zs) = PE.cong₂ cons (+-assoc x y z) PE.refl
⊗-assoc (cons x xs) (skip y)    (leaf z)    = PE.refl
⊗-assoc (cons x xs) (skip y)    (skip z)    = PE.cong (cons x) (⊗-assoc xs y z)
⊗-assoc (cons x xs) (skip y)    (cons z zs) = PE.cong (cons (x + z)) (⊗-assoc xs y zs)
⊗-assoc (cons x xs) (cons y ys) (leaf z)    = PE.cong₂ cons (+-assoc x y z) PE.refl
⊗-assoc (cons x xs) (cons y ys) (skip z)    = PE.cong (cons (x + y)) (⊗-assoc xs ys z)
⊗-assoc (cons x xs) (cons y ys) (cons z zs) = PE.cong₂ cons (+-assoc x y z) (⊗-assoc xs ys zs)

module _ (n : ℕ) where

  private

    Monomial/≡ : Setoid _ _
    Monomial/≡ = PE.setoid (Monomial n)

    Monomial⟦_⟧ : Interpretation Monomial/≡
    Monomial⟦ • ⟧ (x ∷ y ∷ []) = x ⊗ y

    Monomial⟦_⟧-cong : Congruence Monomial/≡ Monomial⟦_⟧
    Monomial⟦ • ⟧-cong (p ∷ q ∷ []) = PE.cong₂ _⊗_ p q

    Monomial/≡-isAlgebra : IsAlgebra (Monomial/≡)
    Monomial/≡-isAlgebra = record { ⟦_⟧     = Monomial⟦_⟧
                                  ; ⟦⟧-cong = Monomial⟦_⟧-cong
                                  }

    Monomial/≡-algebra : Algebra
    Monomial/≡-algebra =
      record { ∥_∥/≈           = Monomial/≡
             ; ∥_∥/≈-isAlgebra = Monomial/≡-isAlgebra
             }

    Monomial/≡-models : Models Monomial/≡-algebra
    Monomial/≡-models comm θ  = ⊗-comm (θ (# 0)) (θ (# 1))
    Monomial/≡-models assoc θ = ⊗-assoc (θ (# 0)) (θ (# 1)) (θ (# 2))

    Monomial/≡-isModel : IsModel Monomial/≡
    Monomial/≡-isModel =
      record { isAlgebra = Monomial/≡-isAlgebra
             ; models    = Monomial/≡-models
             }

  J' : Model
  J' = record { ∥_∥/≈   = Monomial/≡
              ; isModel = Monomial/≡-isModel
              }

private

  module _ {n : ℕ} where

    open Setoid ∥ J n ∥/≈ using (_≈_)

    _·_ : ∥ J n ∥ → ∥ J n ∥ → ∥ J n ∥
    x · y = term • (x ∷ y ∷ [])

    ·-cong : ∀ {x y z w} → x ≈ y → z ≈ w → x · z ≈ y · w
    ·-cong p q = cong • (p ∷ q ∷ [])

    ·-comm : ∀ x y → x · y ≈ y · x
    ·-comm x y = axiom comm (env {A = ∥ J n ∥ₐ} (x ∷ y ∷ []))

    ·-assoc : ∀ x y z → (x · y) · z ≈ x · (y · z)
    ·-assoc x y z = axiom assoc (env {A = ∥ J n ∥ₐ} (x ∷ y ∷ z ∷ []))

  module _ (n : ℕ) where

    open Setoid ∥ J (suc n) ∥/≈ using (_≈_)

    exp : ℕ⁺ → ∥ J (suc n) ∥
    exp one     = atomise n
    exp (suc k) = atomise n · exp k

    exp-hom : ∀ {j k} → exp j · exp k ≈ exp (j + k)
    exp-hom {one}   {k} = refl
    exp-hom {suc j} {k} = begin
        (atomise n · exp j) · exp k
      ≈⟨ ·-assoc (atomise n) (exp j) (exp k) ⟩
        atomise n · (exp j · exp k)
      ≈⟨ ·-cong refl exp-hom ⟩
        atomise n · exp (j + k)
      ∎
      where open Reasoning ∥ J (suc n) ∥/≈

  ∣syn∣ : ∀ {n} → ∥ J' n ∥ → ∥ J n ∥
  ∣syn∣ {suc n} (leaf k)    = exp n k
  ∣syn∣ {suc n} (skip x)    = ∣ raise ∣ (∣syn∣ x)
  ∣syn∣ {suc n} (cons k xs) = exp n k · ∣ raise ∣ (∣syn∣ xs)

  ∣syn∣-cong : ∀ {n} → Congruent _≡_ ≈[ J n ] ∣syn∣
  ∣syn∣-cong {n} p = Setoid.reflexive ∥ J n ∥/≈ (PE.cong ∣syn∣ p)

  ∣syn∣⃗ : ∀ {n} → ∥ J' n ∥/≈ ↝ ∥ J n ∥/≈
  ∣syn∣⃗ {n} = record { ∣_∣      = ∣syn∣ {n}
                      ; ∣_∣-cong = ∣syn∣-cong {n}
                      }

  ∣syn∣-hom : ∀ {n} → Homomorphic ∥ J' n ∥ₐ ∥ J n ∥ₐ ∣syn∣
  ∣syn∣-hom {suc n} • (leaf x    ∷ leaf y    ∷ []) = exp-hom n
  ∣syn∣-hom {suc n} • (leaf x    ∷ skip y    ∷ []) = refl
  ∣syn∣-hom {suc n} • (leaf x    ∷ cons y ys ∷ []) = begin
      exp n x · (exp n y · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ sym (·-assoc (exp n x) (exp n y) _) ⟩
      (exp n x · exp n y) · ∣ raise ∣ (∣syn∣ ys)
    ≈⟨ ·-cong (exp-hom n) refl ⟩
      exp n (x + y) · ∣ raise ∣ (∣syn∣ ys)
    ∎
    where open Reasoning ∥ J (suc n) ∥/≈
  ∣syn∣-hom {suc n} • (skip x    ∷ leaf y    ∷ []) = ·-comm _ (exp n y)
  ∣syn∣-hom {suc n} • (skip x    ∷ skip y    ∷ []) = begin
      ∣ raise ∣ (∣syn∣ x) · ∣ raise ∣ (∣syn∣ y)
    ≈⟨ ∣ raise ∣-hom • (∣syn∣ x ∷ ∣syn∣ y ∷ []) ⟩
      ∣ raise ∣ (∣syn∣ x · ∣syn∣ y)
    ≈⟨ ∣ raise ∣-cong (∣syn∣-hom • (x ∷ y ∷ [])) ⟩
      ∣ raise ∣ (∣syn∣ (x ⊗ y))
    ∎
    where open Reasoning ∥ J (suc n) ∥/≈
  ∣syn∣-hom {suc n} • (skip x    ∷ cons y ys ∷ []) = begin
      ∣ raise ∣ (∣syn∣ x) · (exp n y · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ sym (·-assoc _ (exp n y) _) ⟩
      (∣ raise ∣ (∣syn∣ x) · exp n y) · ∣ raise ∣ (∣syn∣ ys)
    ≈⟨ ·-cong (·-comm _ (exp n y)) refl ⟩
      (exp n y · ∣ raise ∣ (∣syn∣ x)) · ∣ raise ∣ (∣syn∣ ys)
    ≈⟨ ·-assoc (exp n y) _ _ ⟩
      exp n y · (∣ raise ∣ (∣syn∣ x) · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ ·-cong refl (∣ raise ∣-hom • (∣syn∣ x ∷ ∣syn∣ ys ∷ [])) ⟩
      exp n y · ∣ raise ∣ (∣syn∣ x · ∣syn∣ ys)
    ≈⟨ ·-cong refl (∣ raise ∣-cong (∣syn∣-hom • (x ∷ ys ∷ []))) ⟩
      exp n y · ∣ raise ∣ (∣syn∣ (x ⊗ ys))
    ∎
    where open Reasoning ∥ J (suc n) ∥/≈
  ∣syn∣-hom {suc n} • (cons x xs ∷ leaf y    ∷ []) = begin
      (exp n x · ∣ raise ∣ (∣syn∣ xs)) · exp n y
    ≈⟨ ·-assoc (exp n x) _ (exp n y) ⟩
      exp n x · (∣ raise ∣ (∣syn∣ xs) · exp n y)
    ≈⟨ ·-cong refl (·-comm _ (exp n y)) ⟩
      exp n x · (exp n y · ∣ raise ∣ (∣syn∣ xs))
    ≈⟨ sym (·-assoc (exp n x) (exp n y) _) ⟩
      (exp n x · exp n y) · ∣ raise ∣ (∣syn∣ xs)
    ≈⟨ ·-cong (exp-hom n) refl ⟩
      exp n (x + y) · ∣ raise ∣ (∣syn∣ xs)
    ∎
    where open Reasoning ∥ J (suc n) ∥/≈
  ∣syn∣-hom {suc n} • (cons x xs ∷ skip y    ∷ []) = begin
      (exp n x · ∣ raise ∣ (∣syn∣ xs)) · ∣ raise ∣ (∣syn∣ y)
    ≈⟨ ·-assoc (exp n x) _ _ ⟩
      exp n x · (∣ raise ∣ (∣syn∣ xs) · ∣ raise ∣ (∣syn∣ y))
    ≈⟨ ·-cong refl (∣ raise ∣-hom • (∣syn∣ xs ∷ ∣syn∣ y ∷ [])) ⟩
      exp n x · ∣ raise ∣ (∣syn∣ xs · ∣syn∣ y)
    ≈⟨ ·-cong refl (∣ raise ∣-cong (∣syn∣-hom • (xs ∷ y ∷ []))) ⟩
      exp n x · ∣ raise ∣ (∣syn∣ (xs ⊗ y))
    ∎
    where open Reasoning ∥ J (suc n) ∥/≈
  ∣syn∣-hom {suc n} • (cons x xs ∷ cons y ys ∷ []) = begin
      (exp n x · ∣ raise ∣ (∣syn∣ xs)) · (exp n y · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ ·-assoc (exp n x) _ _ ⟩
      exp n x · (∣ raise ∣ (∣syn∣ xs) · (exp n y · ∣ raise ∣ (∣syn∣ ys)))
    ≈⟨ ·-cong refl (sym (·-assoc _ (exp n y) _)) ⟩
      exp n x · ((∣ raise ∣ (∣syn∣ xs) · exp n y) · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ ·-cong refl (·-cong (·-comm (∣ raise ∣ (∣syn∣ xs)) _) refl) ⟩
      exp n x · ((exp n y · ∣ raise ∣ (∣syn∣ xs)) · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ ·-cong refl (·-assoc (exp n y) _ _) ⟩
      exp n x · (exp n y · (∣ raise ∣ (∣syn∣ xs) · ∣ raise ∣ (∣syn∣ ys)))
    ≈⟨ sym (·-assoc (exp n x) (exp n y) _) ⟩
      (exp n x · exp n y) · (∣ raise ∣ (∣syn∣ xs) · ∣ raise ∣ (∣syn∣ ys))
    ≈⟨ ·-cong (exp-hom n) (∣ raise ∣-hom • (∣syn∣ xs ∷ ∣syn∣ ys ∷ [])) ⟩
      exp n (x + y) · ∣ raise ∣ (∣syn∣ xs · ∣syn∣ ys)
    ≈⟨ ·-cong refl (∣ raise ∣-cong (∣syn∣-hom • (xs ∷ ys ∷ []))) ⟩
      exp n (x + y) · ∣ raise ∣ (∣syn∣ (xs ⊗ ys))
    ∎
    where open Reasoning ∥ J (suc n) ∥/≈

syn : ∀ {n} → ∥ J' n ∥ₐ ⟿ ∥ J n ∥ₐ
syn = record { ∣_∣⃗    = ∣syn∣⃗
             ; ∣_∣-hom = ∣syn∣-hom
             }

private

  tab : ∀ {n} → Fin n → ∥ J' n ∥
  tab {suc zero}    zero    = leaf one
  tab {suc (suc n)} zero    = skip (tab {suc n} zero)
  tab {suc (suc n)} (suc k) = lift (tab {suc n} k)

norm : ∀ {n} → ∥ J n ∥ₐ ⟿ ∥ J' n ∥ₐ
norm {n} = interp (J' n) tab

private

  step-exp : ∀ {n} → (k : ℕ⁺)
             → ≈[ J (suc (suc n)) ] (exp (suc n) k)
                                    (∣ step ∣ (exp n k))
  step-exp one     = refl
  step-exp (suc k) = ·-cong refl (step-exp k)

  step-lift : ∀ {n} → (x : ∥ J' n ∥)
              → ≈[ J (suc n) ] (∣ syn ∣ (lift x))
                               (∣ step ∣ (∣ syn ∣ x))
  step-lift {suc n} (leaf x)    = step-exp x
  step-lift {suc n} (skip x)    = begin
      ∣ raise ∣ (∣ syn ∣ (lift x))
    ≈⟨ ∣ raise ∣-cong (step-lift x) ⟩
      ∣ raise ∣ (∣ step ∣ (∣ syn ∣ x))
    ≈⟨ sym (step-raise {x = ∣ syn ∣ x}) ⟩
      ∣ step ∣ (∣ raise ∣ (∣ syn ∣ x))
    ∎
    where open Reasoning ∥ J (suc (suc n)) ∥/≈
  step-lift {suc n} (cons x xs) = begin
      exp (suc n) x · ∣ raise ∣ (∣ syn ∣ (lift xs))
    ≈⟨ ·-cong refl (∣ raise ∣-cong (step-lift xs)) ⟩
      exp (suc n) x · ∣ raise ∣ (∣ step ∣ (∣ syn ∣ xs))
    ≈⟨ ·-cong (step-exp x) (sym (step-raise {x = ∣ syn ∣ xs})) ⟩
      ∣ step ∣ (exp n x) · ∣ step ∣ (∣ raise ∣ (∣ syn ∣ xs))
    ≈⟨ ∣ step ∣-hom • (exp n x ∷ (∣ raise ∣ (∣ syn ∣ xs)) ∷ []) ⟩
      ∣ step ∣ (exp n x · ∣ raise ∣ (∣ syn ∣ xs))
    ∎
    where open Reasoning ∥ J (suc (suc n)) ∥/≈

  syn-tab : ∀ {n} → (k : Fin n)
            → ≈[ J n ] (∣ syn ∣ (tab k)) (atom (dyn k))
  syn-tab {suc zero}    zero    = refl
  syn-tab {suc (suc n)} zero    = ∣ raise ∣-cong (syn-tab zero)
  syn-tab {suc (suc n)} (suc k) = begin
      ∣ syn ∣ (lift (tab {suc n} k))
    ≈⟨ step-lift (tab {suc n} k) ⟩
      ∣ step ∣ (∣ syn ∣ (tab {suc n} k))
    ≈⟨ ∣ step ∣-cong (syn-tab k) ⟩
      ∣ step ∣ (atom (dyn k))
    ∎
    where open Reasoning ∥ J (suc (suc n)) ∥/≈

syn⊙norm≗id : ∀ {n} → syn {n} ⊙ norm {n} ≗ id
syn⊙norm≗id {n} {atom (dyn k)}        = syn-tab k
syn⊙norm≗id {n} {term • (x ∷ y ∷ [])} = begin
    ∣ syn ∣ (∣ norm ∣ x ⊗ ∣ norm ∣ y)
  ≈⟨ sym (∣ syn ∣-hom • (∣ norm ∣ x ∷ ∣ norm ∣ y ∷ [])) ⟩
    ∣ syn ∣ (∣ norm ∣ x) · ∣ syn ∣ (∣ norm ∣ y)
  ≈⟨ ·-cong syn⊙norm≗id syn⊙norm≗id ⟩
    x · y
  ∎
  where open Reasoning ∥ J n ∥/≈

private

  tab-diag : ∀ n → tab {suc n} (fromℕ n) ≡ leaf one
  tab-diag zero    = PE.refl
  tab-diag (suc n) = PE.cong lift (tab-diag n)

  norm-exp : ∀ {n} (k : ℕ⁺) → ∣ norm ∣ (exp n k) ≡ leaf k
  norm-exp {n} one     = tab-diag n
  norm-exp {n} (suc k) = begin
      ∣ norm ∣ (atomise n · exp n k)
    ≈⟨ PE.sym (∣ norm ∣-hom • (atomise n ∷ exp n k ∷ [])) ⟩
      ∣ norm ∣ (atomise n) ⊗ ∣ norm ∣ (exp n k)
    ≈⟨ ⊗-cong (tab-diag n) (norm-exp k) ⟩
      leaf one ⊗ leaf k
    ∎
    where open Reasoning ∥ J' (suc n) ∥/≈

  tab-skip : ∀ {n} → (k : Fin n) → tab {suc n} (up k) ≡ skip (tab {n} k)
  tab-skip {suc zero}    zero    = PE.refl
  tab-skip {suc (suc n)} zero    = PE.refl
  tab-skip {suc (suc n)} (suc k) = PE.cong lift (tab-skip k)

  norm-raise : ∀ {n x} → ∣ norm {suc n} ∣ (∣ raise ∣ x) ≡ skip (∣ norm {n} ∣ x)
  norm-raise {n} {atom (dyn k)}        = tab-skip k
  norm-raise {n} {term • (x ∷ y ∷ [])} = begin
      ∣ norm ∣ (∣ raise ∣ (x · y))
    ≡⟨ ∣ norm ∣-cong (sym (∣ raise ∣-hom • (x ∷ y ∷ []))) ⟩
      ∣ norm ∣ (∣ raise ∣ x · ∣ raise ∣ y)
    ≡⟨ PE.sym (∣ norm ∣-hom • (∣ raise ∣ x ∷ ∣ raise ∣ y ∷ [])) ⟩
      ∣ norm ∣ (∣ raise ∣ x) ⊗ ∣ norm ∣ (∣ raise ∣ y)
    ≡⟨ ⊗-cong (norm-raise {x = x}) (norm-raise {x = y}) ⟩
      skip (∣ norm ∣ x ⊗ ∣ norm ∣ y)
    ≡⟨ PE.cong skip (∣ norm ∣-hom • (x ∷ y ∷ [])) ⟩
      skip (∣ norm ∣ (x · y))
    ∎
    where open PE.≡-Reasoning

norm⊙syn≗id : ∀ {n} → norm {n} ⊙ syn {n} ≗ id
norm⊙syn≗id {suc n} {leaf x} = norm-exp x
norm⊙syn≗id {suc n} {skip x} = begin
    ∣ norm ∣ (∣ raise ∣ (∣ syn ∣ x))
  ≈⟨ norm-raise {x = ∣ syn ∣ x} ⟩
    skip (∣ norm ∣ (∣ syn ∣ x))
  ≈⟨ PE.cong skip norm⊙syn≗id ⟩
    skip x
  ∎
  where open Reasoning ∥ J' (suc n) ∥/≈
norm⊙syn≗id {suc n} {cons x xs} = begin
    ∣ norm ∣ (exp n x · ∣ raise ∣ (∣ syn ∣ xs))
  ≈⟨ PE.sym (∣ norm ∣-hom • (exp n x ∷ ∣ raise ∣ (∣ syn ∣ xs) ∷ [])) ⟩
    ∣ norm ∣ (exp n x) ⊗ ∣ norm ∣ (∣ raise ∣ (∣ syn ∣ xs))
  ≈⟨ ⊗-cong (norm-exp x) (norm-raise {x = ∣ syn ∣ xs}) ⟩
    leaf x ⊗ skip (∣ norm ∣ (∣ syn ∣ xs))
  ≈⟨ ⊗-cong (PE.refl {x = leaf x}) (PE.cong skip (norm⊙syn≗id {x = xs})) ⟩
    leaf x ⊗ skip xs
  ∎
  where open Reasoning ∥ J' (suc n) ∥/≈

iso : ∀ {n} → ∥ J n ∥ₐ ≃ ∥ J' n ∥ₐ
iso = record { _⃗   = norm
             ; _⃖   = syn
             ; invˡ = norm⊙syn≗id
             ; invʳ = syn⊙norm≗id
             }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- Properties of (pre)additive categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Additive.Properties where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Categories.Additive.Base
open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' : Level

-- Some useful lemmas about preadditive categories
module PreaddCategoryTheory (C : PreaddCategory ℓ ℓ') where
  open PreaddCategory C

  -- Pure group theory lemmas
  +idl = λ {x y} → AbGroupStr.+IdL (homAbStr x y)
  +idr = λ {x y} → AbGroupStr.+IdR (homAbStr x y)
  +invl = λ {x y} → AbGroupStr.+InvL (homAbStr x y)
  +invr = λ {x y} → AbGroupStr.+InvR (homAbStr x y)
  +assoc = λ {x y} → AbGroupStr.+Assoc (homAbStr x y)
  +comm = λ {x y} → AbGroupStr.+Comm (homAbStr x y)

  -dist+ : {x y : ob} (f g : Hom[ x , y ]) →
      - (f + g) ≡ (- f) + (- g)
  -dist+ {x} {y} f g =
    let open GroupTheory (AbGroup→Group (Hom[ x , y ] , homAbStr x y)) in
      (invDistr _ _) ∙ (+comm _ _)

  +4assoc : {x y : ob} (a b c d : Hom[ x , y ]) →
      (a + b) + (c + d)  ≡  a + (b + c) + d
  +4assoc a b c d = sym (+assoc _ _ _) ∙ cong (a +_) (+assoc _ _ _)

  +4comm : {x y : ob} (a b c d : Hom[ x , y ]) →
      (a + b) + (c + d)  ≡  (a + c) + (b + d)
  +4comm a b c d = +4assoc _ _ _ _ ∙
      cong (λ u → a + (u + d)) (+comm _ _) ∙ sym (+4assoc _ _ _ _)

  -- Interaction of categorical & group structure
  ⋆0hl : ∀ {w x y} (f : Hom[ x , y ]) → 0h ⋆ f ≡ 0h {w}
  ⋆0hl f =
      0h ⋆ f                              ≡⟨ sym (+idr _) ⟩
      0h ⋆ f  +  0h                       ≡⟨ cong (0h ⋆ f +_) (sym (+invr _)) ⟩
      0h ⋆ f  +  (0h ⋆ f  -  0h ⋆ f)      ≡⟨ +assoc _ _ _ ⟩
      (0h ⋆ f  +  0h ⋆ f)  -  0h ⋆ f      ≡⟨ cong (_- 0h ⋆ f) (sym (⋆distr+ _ _ _)) ⟩
      (0h + 0h) ⋆ f  -  0h ⋆ f            ≡⟨ cong (λ a → a ⋆ f - 0h ⋆ f) (+idr _) ⟩
      0h ⋆ f  -  0h ⋆ f                   ≡⟨ +invr _ ⟩
      0h                                  ∎

  ⋆0hr : ∀ {x y z} (f : Hom[ x , y ]) → f ⋆ 0h ≡ 0h {x} {z}
  ⋆0hr f =
      f ⋆ 0h                              ≡⟨ sym (+idr _) ⟩
      f ⋆ 0h  +  0h                       ≡⟨ cong (f ⋆ 0h +_) (sym (+invr _)) ⟩
      f ⋆ 0h  +  (f ⋆ 0h  -  f ⋆ 0h)      ≡⟨ +assoc _ _ _ ⟩
      (f ⋆ 0h  +  f ⋆ 0h)  -  f ⋆ 0h      ≡⟨ cong (_- f ⋆ 0h) (sym (⋆distl+ _ _ _)) ⟩
      f ⋆ (0h + 0h)  -  f ⋆ 0h            ≡⟨ cong (λ a → f ⋆ a - f ⋆ 0h) (+idr _) ⟩
      f ⋆ 0h  -  f ⋆ 0h                   ≡⟨ +invr _ ⟩
      0h                                  ∎

  -distl⋆ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ])
    → (- f) ⋆ g ≡ - (f ⋆ g)
  -distl⋆ {x} {y} {z} f g =
    let open GroupTheory (AbGroup→Group (Hom[ x , z ] , homAbStr x z)) in
    invUniqueR (
      f ⋆ g + (- f) ⋆ g     ≡⟨ sym (⋆distr+ _ _ _) ⟩
      (f - f) ⋆ g           ≡⟨ cong (_⋆ g) (+invr _) ⟩
      0h ⋆ g                ≡⟨ ⋆0hl _ ⟩
      0h                    ∎
    )

  -distr⋆ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ])
    → f ⋆ (- g) ≡ - (f ⋆ g)
  -distr⋆ {x} {y} {z} f g =
    let open GroupTheory (AbGroup→Group (Hom[ x , z ] , homAbStr x z)) in
    invUniqueR (
      f ⋆ g + f ⋆ (- g)     ≡⟨ sym (⋆distl+ _ _ _) ⟩
      f ⋆ (g - g)           ≡⟨ cong (f ⋆_) (+invr _) ⟩
      f ⋆ 0h                ≡⟨ ⋆0hr _ ⟩
      0h                    ∎
    )

-- Matrix notation for morphisms  (x₁ ⊕ ⋯ ⊕ xₙ) → (y₁ ⊕ ⋯ ⊕ yₘ)
-- in an additive category
module MatrixNotation (A : AdditiveCategory ℓ ℓ') where
    open AdditiveCategory A
    open PreaddCategoryTheory preaddcat

    -- Polymorphic biproduct morphisms
    i₁ = λ {x y} → Biproduct.i₁ (biprod x y)
    i₂ = λ {x y} → Biproduct.i₂ (biprod x y)
    π₁ = λ {x y} → Biproduct.π₁ (biprod x y)
    π₂ = λ {x y} → Biproduct.π₂ (biprod x y)
    -- and axioms
    i₁⋆π₁ = λ {x y} → Biproduct.i₁⋆π₁ (biprod x y)
    i₁⋆π₂ = λ {x y} → Biproduct.i₁⋆π₂ (biprod x y)
    i₂⋆π₁ = λ {x y} → Biproduct.i₂⋆π₁ (biprod x y)
    i₂⋆π₂ = λ {x y} → Biproduct.i₂⋆π₂ (biprod x y)
    ∑π⋆i  = λ {x y} → Biproduct.∑π⋆i  (biprod x y)

    _∣_ : ∀ {x y y'} → Hom[ x , y ] → Hom[ x , y' ] → Hom[ x , y ⊕ y' ]
    f ∣ f' = (f ⋆ i₁) + (f' ⋆ i₂)
    infixr 5 _∣_

    _`_ : ∀ {y y' z} → Hom[ y , z ] → Hom[ y' , z ] → Hom[ y ⊕ y' , z ]
    g ` g' = (π₁ ⋆ g) + (π₂ ⋆ g')
    infixr 6 _`_

    -- Use the matrix notation like this:
    private module _ (x y : ob) (f : Hom[ x , y ]) where

      h : Hom[ x ⊕ x ⊕ x , y ⊕ y ⊕ y ⊕ y ]

      h =  f  ` - f `  0h   ∣
           0h `  0h `  f    ∣
           f  ` - f `  0h   ∣
           0h `  f  ` f + f

    -- Exchange law
    exchange : ∀ {x x' y y'} (a : Hom[ x , y ]) (b : Hom[ x' , y ])
            (c : Hom[ x , y' ]) (d : Hom[ x' , y' ]) →
        (a ` b ∣ c ` d)  ≡  (a ∣ c) ` (b ∣ d)

    exchange a b c d =
        (π₁ ⋆ a  +  π₂ ⋆ b) ⋆ i₁  +  (π₁ ⋆ c  +  π₂ ⋆ d) ⋆ i₂
                ≡⟨ cong₂ _+_ (⋆distr+ _ _ _) (⋆distr+ _ _ _) ⟩
        ((π₁ ⋆ a) ⋆ i₁  +  (π₂ ⋆ b) ⋆ i₁)  +  ((π₁ ⋆ c) ⋆ i₂  +  (π₂ ⋆ d) ⋆ i₂)
                ≡⟨ +4comm _ _ _ _ ⟩
        ((π₁ ⋆ a) ⋆ i₁  +  (π₁ ⋆ c) ⋆ i₂)  +  ((π₂ ⋆ b) ⋆ i₁  +  (π₂ ⋆ d) ⋆ i₂)
                ≡⟨ cong₂ _+_ (cong₂ _+_ (⋆Assoc _ _ _) (⋆Assoc _ _ _))
                            (cong₂ _+_ (⋆Assoc _ _ _) (⋆Assoc _ _ _)) ⟩
        (π₁ ⋆ (a ⋆ i₁)  +  π₁ ⋆ (c ⋆ i₂))  +  (π₂ ⋆ (b ⋆ i₁)  +  π₂ ⋆ (d ⋆ i₂))
                ≡⟨ sym (cong₂ _+_ (⋆distl+ _ _ _) (⋆distl+ _ _ _)) ⟩
        π₁ ⋆ (a ⋆ i₁  +  c ⋆ i₂)  +  π₂ ⋆ (b ⋆ i₁  +  d ⋆ i₂)
                ∎

    -- iₖ times a row
    module _ {x x' y : ob} (a : Hom[ x , y ]) (b : Hom[ x' , y ]) where

      i₁⋆row :  i₁ ⋆ (a ` b)  ≡  a
      i₁⋆row =
          i₁ ⋆ (π₁ ⋆ a  +  π₂ ⋆ b)
                  ≡⟨ ⋆distl+ _ _ _ ⟩
          i₁ ⋆ (π₁ ⋆ a)  +  i₁ ⋆ (π₂ ⋆ b)
                  ≡⟨ cong₂ _+_ (sym (⋆Assoc _ _ _)) (sym (⋆Assoc _ _ _)) ⟩
          (i₁ ⋆ π₁) ⋆ a  +  (i₁ ⋆ π₂) ⋆ b
                  ≡⟨ cong₂ (λ u v → u ⋆ a + v ⋆ b) i₁⋆π₁ i₁⋆π₂ ⟩
          id ⋆ a  +  0h ⋆ b
                  ≡⟨ cong₂ _+_ (⋆IdL _) (⋆0hl _) ⟩
          a  +  0h
                  ≡⟨ +idr _ ⟩
          a       ∎

      i₂⋆row :  i₂ ⋆ (a ` b)  ≡  b
      i₂⋆row =
          i₂ ⋆ (π₁ ⋆ a  +  π₂ ⋆ b)
                  ≡⟨ ⋆distl+ _ _ _ ⟩
          i₂ ⋆ (π₁ ⋆ a)  +  i₂ ⋆ (π₂ ⋆ b)
                  ≡⟨ cong₂ _+_ (sym (⋆Assoc _ _ _)) (sym (⋆Assoc _ _ _)) ⟩
          (i₂ ⋆ π₁) ⋆ a  +  (i₂ ⋆ π₂) ⋆ b
                  ≡⟨ cong₂ (λ u v → u ⋆ a + v ⋆ b) i₂⋆π₁ i₂⋆π₂ ⟩
          0h ⋆ a  +  id ⋆ b
                  ≡⟨ cong₂ _+_ (⋆0hl _) (⋆IdL _) ⟩
          0h  +  b
                  ≡⟨ +idl _ ⟩
          b       ∎

    -- A column times πₖ
    module _ {x y y' : ob} (a : Hom[ x , y ]) (b : Hom[ x , y' ]) where

      col⋆π₁ :  (a ∣ b) ⋆ π₁  ≡  a
      col⋆π₁ =
          (a ⋆ i₁  +  b ⋆ i₂) ⋆ π₁
                  ≡⟨ ⋆distr+ _ _ _ ⟩
          (a ⋆ i₁) ⋆ π₁  +  (b ⋆ i₂) ⋆ π₁
                  ≡⟨ cong₂ _+_ (⋆Assoc _ _ _) (⋆Assoc _ _ _) ⟩
          a ⋆ (i₁ ⋆ π₁)  +  b ⋆ (i₂ ⋆ π₁)
                  ≡⟨ cong₂ (λ u v → a ⋆ u + b ⋆ v) i₁⋆π₁ i₂⋆π₁ ⟩
          a ⋆ id  +  b ⋆ 0h
                  ≡⟨ cong₂ _+_ (⋆IdR _) (⋆0hr _) ⟩
          a  +  0h
                  ≡⟨ +idr _ ⟩
          a       ∎

      col⋆π₂ :  (a ∣ b) ⋆ π₂  ≡  b
      col⋆π₂ =
          (a ⋆ i₁  +  b ⋆ i₂) ⋆ π₂
                  ≡⟨ ⋆distr+ _ _ _ ⟩
          (a ⋆ i₁) ⋆ π₂  +  (b ⋆ i₂) ⋆ π₂
                  ≡⟨ cong₂ _+_ (⋆Assoc _ _ _) (⋆Assoc _ _ _) ⟩
          a ⋆ (i₁ ⋆ π₂)  +  b ⋆ (i₂ ⋆ π₂)
                  ≡⟨ cong₂ (λ u v → a ⋆ u + b ⋆ v) i₁⋆π₂ i₂⋆π₂ ⟩
          a ⋆ 0h  +  b ⋆ id
                  ≡⟨ cong₂ _+_ (⋆0hr _) (⋆IdR _) ⟩
          0h  +  b
                  ≡⟨ +idl _ ⟩
          b       ∎

    -- iₖ / πₖ times a diagonal matrix
    module _ {x x' y y'} (a : Hom[ x , y ]) (b : Hom[ x' , y' ]) where

      i₁⋆diag :  i₁ ⋆ (a ` 0h ∣ 0h ` b)  ≡  a ⋆ i₁
      i₁⋆diag =
          i₁ ⋆ (a ` 0h ∣ 0h ` b)          ≡⟨ cong (i₁ ⋆_) (exchange _ _ _ _) ⟩
          i₁ ⋆ ((a ∣ 0h) ` (0h ∣ b))      ≡⟨ i₁⋆row _ _ ⟩
          (a ∣ 0h)                        ≡⟨ cong (a ⋆ i₁ +_) (⋆0hl _) ⟩
          a ⋆ i₁  +  0h                   ≡⟨ +idr _ ⟩
          a ⋆ i₁                          ∎

      i₂⋆diag :  i₂ ⋆ (a ` 0h ∣ 0h ` b)  ≡  b ⋆ i₂
      i₂⋆diag =
          i₂ ⋆ (a ` 0h ∣ 0h ` b)          ≡⟨ cong (i₂ ⋆_) (exchange _ _ _ _) ⟩
          i₂ ⋆ ((a ∣ 0h) ` (0h ∣ b))      ≡⟨ i₂⋆row _ _ ⟩
          (0h ∣ b)                        ≡⟨ cong (_+ b ⋆ i₂) (⋆0hl _) ⟩
          0h  +  b ⋆ i₂                   ≡⟨ +idl _ ⟩
          b ⋆ i₂                          ∎

      diag⋆π₁ :  (a ` 0h ∣ 0h ` b) ⋆ π₁  ≡  π₁ ⋆ a
      diag⋆π₁ =
          (a ` 0h ∣ 0h ` b) ⋆ π₁      ≡⟨ col⋆π₁ _ _ ⟩
          a ` 0h                      ≡⟨ cong (π₁ ⋆ a +_) (⋆0hr _) ⟩
          π₁ ⋆ a  +  0h               ≡⟨ +idr _ ⟩
          π₁ ⋆ a                      ∎

      diag⋆π₂ :  (a ` 0h ∣ 0h ` b) ⋆ π₂  ≡  π₂ ⋆ b
      diag⋆π₂ =
          (a ` 0h ∣ 0h ` b) ⋆ π₂      ≡⟨ col⋆π₂ _ _ ⟩
          0h ` b                      ≡⟨ cong (_+ π₂ ⋆ b) (⋆0hr _) ⟩
          0h  +  π₂ ⋆ b               ≡⟨ +idl _ ⟩
          π₂ ⋆ b                      ∎

    -- Matrix addition
    addRow : ∀ {x y z}
        (f f' : Hom[ x , z ]) (g g' : Hom[ y , z ]) →
        (f ` g) + (f' ` g') ≡ (f + f') ` (g + g')

    addRow f f' g g' =
        (π₁ ⋆ f + π₂ ⋆ g) + (π₁ ⋆ f' + π₂ ⋆ g')
                ≡⟨ +4comm _ _ _ _ ⟩
        (π₁ ⋆ f + π₁ ⋆ f') + (π₂ ⋆ g + π₂ ⋆ g')
                ≡⟨ sym (cong₂ _+_ (⋆distl+ _ _ _) (⋆distl+ _ _ _)) ⟩
        π₁ ⋆ (f + f') + π₂ ⋆ (g + g')
                ∎

    addCol : ∀ {x y z}
        (f f' : Hom[ x , y ]) (g g' : Hom[ x , z ]) →
        (f ∣ g) + (f' ∣ g') ≡ (f + f') ∣ (g + g')

    addCol f f' g g' =
        (f ⋆ i₁ + g ⋆ i₂) + (f' ⋆ i₁ + g' ⋆ i₂)
                ≡⟨ +4comm _ _ _ _ ⟩
        (f ⋆ i₁ + f' ⋆ i₁) + (g ⋆ i₂ + g' ⋆ i₂)
                ≡⟨ sym (cong₂ _+_ (⋆distr+ _ _ _) (⋆distr+ _ _ _)) ⟩
        (f + f') ⋆ i₁ + (g + g') ⋆ i₂
                ∎

    private
      ⋆4assoc : ∀ {x y z w v} (a : Hom[ x , y ]) (b : Hom[ y , z ])
              (c : Hom[ z , w ]) (d : Hom[ w , v ]) →
          (a ⋆ b) ⋆ (c ⋆ d) ≡ a ⋆ (b ⋆ c) ⋆ d
      ⋆4assoc a b c d = (⋆Assoc _ _ _) ∙ cong (a ⋆_) (sym (⋆Assoc _ _ _))

      ⋆4assoc' : ∀ {x y z w v} (a : Hom[ x , y ]) (b : Hom[ y , z ])
              (c : Hom[ z , w ]) (d : Hom[ w , v ]) →
          (a ⋆ b) ⋆ (c ⋆ d) ≡ (a ⋆ (b ⋆ c)) ⋆ d
      ⋆4assoc' a b c d = sym (⋆Assoc _ _ _) ∙ cong (_⋆ d) (⋆Assoc _ _ _)

    -- Matrix multiplication
    innerProd : ∀ {x y₁ y₂ z} (f₁ : Hom[ x , y₁ ]) (g₁ : Hom[ y₁ , z ])
                              (f₂ : Hom[ x , y₂ ]) (g₂ : Hom[ y₂ , z ]) →
        (f₁ ∣ f₂) ⋆ (g₁ ` g₂) ≡ (f₁ ⋆ g₁) + (f₂ ⋆ g₂)

    innerProd f₁ g₁ f₂ g₂ =
        (f₁ ⋆ i₁ + f₂ ⋆ i₂) ⋆ (π₁ ⋆ g₁ + π₂ ⋆ g₂)
                ≡⟨ ⋆distr+ _ _ _ ⟩
        (f₁ ⋆ i₁) ⋆ (π₁ ⋆ g₁ + π₂ ⋆ g₂)  +  (f₂ ⋆ i₂) ⋆ (π₁ ⋆ g₁ + π₂ ⋆ g₂)
                ≡⟨ cong₂ _+_ (⋆distl+ _ _ _) (⋆distl+ _ _ _) ⟩
        ((f₁ ⋆ i₁) ⋆ (π₁ ⋆ g₁)  +  (f₁ ⋆ i₁) ⋆ (π₂ ⋆ g₂))
            +  (f₂ ⋆ i₂) ⋆ (π₁ ⋆ g₁)  +  (f₂ ⋆ i₂) ⋆ (π₂ ⋆ g₂)
                ≡⟨ cong₂ _+_ (cong₂ _+_ eq₁₁ eq₁₂) (cong₂ _+_ eq₂₁ eq₂₂) ⟩
        (f₁ ⋆ g₁  +  0h)  +  0h  +  f₂ ⋆ g₂
                ≡⟨ cong₂ _+_ (+idr _) (+idl _) ⟩
        (f₁ ⋆ g₁) + (f₂ ⋆ g₂)
                ∎
     where
      eq₁₁ = (f₁ ⋆ i₁) ⋆ (π₁ ⋆ g₁)      ≡⟨ ⋆4assoc _ _ _ _ ⟩
             f₁ ⋆ (i₁ ⋆ π₁) ⋆ g₁        ≡⟨ cong (λ u → _ ⋆ u ⋆ _) i₁⋆π₁ ⟩
             f₁ ⋆ id ⋆ g₁               ≡⟨ cong (f₁ ⋆_) (⋆IdL _) ⟩
             f₁ ⋆ g₁                    ∎

      eq₁₂ = (f₁ ⋆ i₁) ⋆ (π₂ ⋆ g₂)      ≡⟨ ⋆4assoc _ _ _ _ ⟩
             f₁ ⋆ (i₁ ⋆ π₂) ⋆ g₂        ≡⟨ cong (λ u → _ ⋆ u ⋆ _) i₁⋆π₂ ⟩
             f₁ ⋆ 0h ⋆ g₂               ≡⟨ cong (f₁ ⋆_) (⋆0hl _) ⟩
             f₁ ⋆ 0h                    ≡⟨ ⋆0hr _ ⟩
             0h                         ∎

      eq₂₁ = (f₂ ⋆ i₂) ⋆ (π₁ ⋆ g₁)      ≡⟨ ⋆4assoc _ _ _ _ ⟩
             f₂ ⋆ (i₂ ⋆ π₁) ⋆ g₁        ≡⟨ cong (λ u → _ ⋆ u ⋆ _) i₂⋆π₁ ⟩
             f₂ ⋆ 0h ⋆ g₁               ≡⟨ cong (f₂ ⋆_) (⋆0hl _) ⟩
             f₂ ⋆ 0h                    ≡⟨ ⋆0hr _ ⟩
             0h                         ∎

      eq₂₂ = (f₂ ⋆ i₂) ⋆ (π₂ ⋆ g₂)      ≡⟨ ⋆4assoc _ _ _ _ ⟩
             f₂ ⋆ (i₂ ⋆ π₂) ⋆ g₂        ≡⟨ cong (λ u → _ ⋆ u ⋆ _) i₂⋆π₂ ⟩
             f₂ ⋆ id ⋆ g₂               ≡⟨ cong (f₂ ⋆_) (⋆IdL _) ⟩
             f₂ ⋆ g₂                    ∎

    outerProd : ∀ {x₁ x₂ y z₁ z₂} (f₁ : Hom[ x₁ , y ]) (g₁ : Hom[ y , z₁ ])
                                  (f₂ : Hom[ x₂ , y ]) (g₂ : Hom[ y , z₂ ]) →

        (f₁ ` f₂) ⋆ (g₁ ∣ g₂)  ≡  f₁ ⋆ g₁ ` f₂ ⋆ g₁ ∣
                                  f₁ ⋆ g₂ ` f₂ ⋆ g₂

    outerProd {y = y} f₁ g₁ f₂ g₂ =
        (π₁ ⋆ f₁  +  π₂ ⋆ f₂) ⋆ (g₁ ⋆ i₁  +  g₂ ⋆ i₂)
                ≡⟨ ⋆distl+ _ _ _ ⟩
        (π₁ ⋆ f₁  +  π₂ ⋆ f₂) ⋆ (g₁ ⋆ i₁)  +  (π₁ ⋆ f₁  +  π₂ ⋆ f₂) ⋆ (g₂ ⋆ i₂)
                ≡⟨ cong₂ _+_ (eq g₁ i₁) (eq g₂ i₂) ⟩
           (π₁ ⋆ (f₁ ⋆ g₁)  +  π₂ ⋆ (f₂ ⋆ g₁)) ⋆ i₁
        +  (π₁ ⋆ (f₁ ⋆ g₂)  +  π₂ ⋆ (f₂ ⋆ g₂)) ⋆ i₂
                ∎
     where
      eq = λ {z w} (g : Hom[ y , z ]) (i : Hom[ z , w ]) →
        (π₁ ⋆ f₁  +  π₂ ⋆ f₂) ⋆ (g ⋆ i)
                ≡⟨ ⋆distr+ _ _ _ ⟩
        (π₁ ⋆ f₁) ⋆ (g ⋆ i)  +  (π₂ ⋆ f₂) ⋆ (g ⋆ i)
                ≡⟨ cong₂ _+_ (⋆4assoc' _ _ _ _) (⋆4assoc' _ _ _ _) ⟩
        (π₁ ⋆ (f₁ ⋆ g)) ⋆ i  +  (π₂ ⋆ (f₂ ⋆ g)) ⋆ i
                ≡⟨ sym (⋆distr+ _ _ _) ⟩
        (π₁ ⋆ (f₁ ⋆ g)  +  π₂ ⋆ (f₂ ⋆ g)) ⋆ i
                    ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.AlmostRing where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ)

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup

private
  variable
    ℓ : Level

record IsAlmostRing {R : Type ℓ}
                  (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor isalmostring

  field
    +IsMonoid : IsMonoid 0r _+_
    ·IsMonoid : IsMonoid 1r _·_
    +Comm : (x y : R) → x + y ≡ y + x
    ·Comm : (x y : R) → x · y ≡ y · x
    ·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
    ·DistL+ :  (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
    -Comm· : (x y : R) → - (x · y) ≡ (- x) · y
    -Dist+ : (x y : R) → - (x + y) ≡ (- x) + (- y)
    0LeftAnnihilates : (x : R) → 0r · x ≡ 0r
    0RightAnnihilates : (x : R) → x · 0r ≡ 0r

  open IsMonoid +IsMonoid public
    renaming
      ( assoc       to +Assoc
      ; identity    to +Identity
      ; lid         to +Lid
      ; rid         to +Rid
      ; isSemigroup to +IsSemigroup)

  open IsMonoid ·IsMonoid public
    renaming
      ( assoc       to ·Assoc
      ; identity    to ·Identity
      ; lid         to ·Lid
      ; rid         to ·Rid
      ; isSemigroup to ·IsSemigroup )
    hiding
      ( is-set ) -- We only want to export one proof of this

record AlmostRing : Type (ℓ-suc ℓ) where

  constructor almostring

  field
    Carrier : Type ℓ
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    isAlmostRing  : IsAlmostRing 0r 1r _+_ _·_ -_

  infixl 9 _^_
  infixl 8 _·_
  infixl 7 -_
  infixl 6 _+_
  infixl 6 _-_

  open IsAlmostRing isAlmostRing public

  _^_ : Carrier → ℕ → Carrier
  x ^ 0 = 1r
  x ^ ℕ.suc k = x · (x ^ k)

  _-_ : Carrier → Carrier → Carrier
  x - y = x + (- y)

-- Extractor for the carrier type
⟨_⟩ : AlmostRing → Type ℓ
⟨_⟩ = AlmostRing.Carrier

isSetAlmostRing : (R : AlmostRing {ℓ}) → isSet ⟨ R ⟩
isSetAlmostRing R = R .AlmostRing.isAlmostRing .IsAlmostRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

module Theory (R : AlmostRing {ℓ}) where
  open AlmostRing R

  0IsSelfinverse : - 0r ≡ 0r
  0IsSelfinverse = - 0r          ≡⟨ cong -_ (sym (·Lid 0r))  ⟩
                   - (1r · 0r)   ≡⟨ -Comm· 1r 0r ⟩
                   (- 1r) · 0r   ≡⟨ 0RightAnnihilates (- 1r) ⟩
                   0r ∎

  ·CommRight : (x y z : ⟨ R ⟩)
               → x · y · z ≡ x · z · y
  ·CommRight x y z = x · y · z   ≡⟨ sym (·Assoc _ _ _) ⟩
                     x · (y · z) ≡⟨ cong (λ u → x · u) (·Comm _ _) ⟩
                     x · (z · y) ≡⟨ ·Assoc _ _ _ ⟩
                     x · z · y ∎

  +ShufflePairs : (a b c d : ⟨ R ⟩)
                → (a + b) + (c + d) ≡ (a + c) + (b + d)
  +ShufflePairs a b c d =
    (a + b) + (c + d) ≡⟨ +Assoc _ _ _ ⟩
    ((a + b) + c) + d ≡⟨ cong (λ u → u + d) (sym (+Assoc _ _ _)) ⟩
    (a + (b + c)) + d ≡⟨ cong (λ u → (a + u) + d) (+Comm _ _) ⟩
    (a + (c + b)) + d ≡⟨ cong (λ u → u + d) (+Assoc _ _ _) ⟩
    ((a + c) + b) + d ≡⟨ sym (+Assoc _ _ _) ⟩
    (a + c) + (b + d) ∎

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:
-- Andreas, 2017-10-11, issue #2769

-- Patch https://github.com/agda/agda/commit/7fc73607703e0373beaf65ba05fb1911b6d84a5e
--
--   Re #2495: make mutual info safer by distinguishing Nothing and Just []
--
--   Nothing means: never computed.
--   Just [] means: computed, but non-recursive.
--
--   These two notions were conflated before.
--
-- introduced this regression because the projection-likeness check failed.

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v 10 #-}
-- {-# OPTIONS -v tc.signature:60 #-}
-- {-# OPTIONS -v tc.mod.apply:80 #-}
-- {-# OPTIONS -v tc.sig.param:90 #-}
-- {-# OPTIONS -v tc.display:100 #-}

module Issue2769 where

module M (_X : Set₁)
  where

  record R (_Y : Set₂) : Set₁ where
    field A : Set

  record S : Set₁ where
    field r : R Set₁
    module Rr = R r

ok : (s : M.S Set) → M.R.A (M.S.r s) -- M.S.Rr.A s
ok = {!!}  -- goal displayed as  (s : M.S Set) → M.R.A (M.S.r s)

module MSet = M Set

goal : (s : M.S Set) → M.R.A (M.S.r s) -- M.S.Rr.A s
goal = {!!}  -- WAS: goal displayed as  (s : MSet.S) → MSet.S.Rr.A

-- adding display form Issue2769.M.R.A --> Issue2769.MSet.S.Rr.A
-- Display {dfFreeVars = 1, dfPats = [Apply ru(Def Issue2769.M.S.r [Apply ru(Var 0 [])])], dfRHS = DTerm (Def Issue2769.MSet.S.Rr.A [])}

-- EXPECTED:
-- Should display goal 1 as
-- ?1 : (s : MSet.S) → M.R.A (MSet.S.r s)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Paths
import lib.types.Generic1HIT as Generic1HIT

module lib.types.Pushout {i j k} where

module _ where

  private
    data #Pushout-aux (d : Span {i} {j} {k}) : Type (lmax (lmax i j) k) where
      #left : Span.A d → #Pushout-aux d
      #right : Span.B d → #Pushout-aux d

    data #Pushout (d : Span) : Type (lmax (lmax i j) k) where
      #pushout : #Pushout-aux d → (Unit → Unit) → #Pushout d

  Pushout : (d : Span) → Type _
  Pushout d = #Pushout d

  left : {d : Span} → Span.A d → Pushout d
  left a = #pushout (#left a) _

  right : {d : Span} → Span.B d → Pushout d
  right b = #pushout (#right b) _

  postulate  -- HIT
    glue : {d : Span} → (c : Span.C d) → left (Span.f d c) == right (Span.g d c) :> Pushout d

  module PushoutElim {d : Span} {l} {P : Pushout d → Type l}
    (left* : (a : Span.A d) → P (left a))
    (right* : (b : Span.B d) → P (right b))
    (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c) [ P ↓ glue c ]) where

    f : Π (Pushout d) P
    f = f-aux phantom  where

      f-aux : Phantom glue* → Π (Pushout d) P
      f-aux phantom (#pushout (#left y) _) = left* y
      f-aux phantom (#pushout (#right y) _) = right* y

    postulate  -- HIT
      glue-β : (c : Span.C d) → apd f (glue c) == glue* c

open PushoutElim public using () renaming (f to Pushout-elim)

module PushoutRec {d : Span} {l} {D : Type l}
  (left* : Span.A d → D) (right* : Span.B d → D)
  (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c)) where

  private
    module M = PushoutElim left* right* (λ c → ↓-cst-in (glue* c))

  f : Pushout d → D
  f = M.f

  glue-β : (c : Span.C d) → ap f (glue c) == glue* c
  glue-β c = apd=cst-in {f = f} (M.glue-β c)

module PushoutGeneric {d : Span {i} {j} {k}} where

  open Span d renaming (f to g; g to h)

  open Generic1HIT (Coprod A B) C (inl ∘ g) (inr ∘ h) public

  module _ where

    module To = PushoutRec (cc ∘ inl) (cc ∘ inr) pp

    to : Pushout d → T
    to = To.f

    from-cc : Coprod A B → Pushout d
    from-cc (inl a) = left a
    from-cc (inr b) = right b

    module From = Rec from-cc glue

    from : T → Pushout d
    from = From.f

    abstract
      to-from : (x : T) → to (from x) == x
      to-from = elim to-from-cc to-from-pp where

        to-from-cc : (x : Coprod A B)
          → to (from (cc x)) == cc x
        to-from-cc (inl a) = idp
        to-from-cc (inr b) = idp

        to-from-pp :
          (c : C) → idp == idp [ (λ z → to (from z) == z) ↓ pp c ]
        to-from-pp c = ↓-∘=idf-in to from
          (ap to (ap from (pp c))   =⟨ From.pp-β c |in-ctx ap to ⟩
           ap to (glue c)           =⟨ To.glue-β c ⟩
           pp c ∎)

      from-to : (x : Pushout d) → from (to x) == x
      from-to = Pushout-elim (λ a → idp) (λ b → idp) (λ c → ↓-∘=idf-in from to
        (ap from (ap to (glue c))   =⟨ To.glue-β c |in-ctx ap from ⟩
         ap from (pp c)             =⟨ From.pp-β c ⟩
         glue c ∎))

  generic-pushout : Pushout d ≃ T
  generic-pushout = equiv to from to-from from-to

_⊔^[_]_/_ : (A : Type i) (C : Type k) (B : Type j)
  (fg : (C → A) × (C → B)) → Type (lmax (lmax i j) k)
A ⊔^[ C ] B  / (f , g) = Pushout (span A B C f g)

⊙Pushout : (d : ⊙Span {i} {j} {k}) → Ptd _
⊙Pushout d = ⊙[ Pushout (⊙span-out d) , left (snd (⊙Span.X d)) ]

module _ (d : ⊙Span {i} {j} {k}) where

  open ⊙Span d

  ⊙left : fst (X ⊙→ ⊙Pushout d)
  ⊙left = (left , idp)

  ⊙right : fst (Y ⊙→ ⊙Pushout d)
  ⊙right =
    (right , ap right (! (snd g)) ∙ ! (glue (snd Z)) ∙' ap left (snd f))

  ⊙glue : (⊙left ⊙∘ f) == (⊙right ⊙∘ g)
  ⊙glue = pair=
    (λ= glue)
    (↓-app=cst-in $
      ap left (snd f) ∙ idp
        =⟨ ∙-unit-r _ ⟩
      ap left (snd f)
        =⟨ lemma (glue (snd Z)) (ap right (snd g)) (ap left (snd f)) ⟩
      glue (snd Z) ∙ ap right (snd g)
      ∙ ! (ap right (snd g)) ∙ ! (glue (snd Z)) ∙' ap left (snd f)
        =⟨ !-ap right (snd g)
           |in-ctx (λ w → glue (snd Z) ∙ ap right (snd g) ∙ w
                          ∙ ! (glue (snd Z)) ∙' ap left (snd f)) ⟩
      glue (snd Z) ∙ ap right (snd g)
      ∙ ap right (! (snd g)) ∙ ! (glue (snd Z)) ∙' ap left (snd f)
        =⟨ ! (app=-β glue (snd Z))
           |in-ctx (λ w → w ∙ ap right (snd g) ∙ ap right (! (snd g))
                            ∙ ! (glue (snd Z)) ∙' ap left (snd f)) ⟩
      app= (λ= glue) (snd Z) ∙ ap right (snd g)
      ∙ ap right (! (snd g)) ∙ ! (glue (snd Z)) ∙' ap left (snd f) ∎)
    where
    lemma : ∀ {i} {A : Type i} {x y z w : A}
      (p : x == y) (q : y == z) (r : x == w)
      → r == p ∙ q ∙ ! q ∙ ! p ∙' r
    lemma idp idp idp = idp

⊙pushout-J : ∀ {l} (P : ⊙Span → Type l)
  → ({A : Type i} {B : Type j} (Z : Ptd k) (f : fst Z → A) (g : fst Z → B)
     → P (⊙span (A , f (snd Z)) (B , g (snd Z)) Z (f , idp) (g , idp)))
  → ((ps : ⊙Span) → P ps)
⊙pushout-J P t (⊙span (_ , ._) (_ , ._) Z (f , idp) (g , idp)) = t Z f g

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda