mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
minor fixes
This commit is contained in:
parent
64a1f120d0
commit
a0f370b000
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
4 changed files with 4 additions and 358 deletions
4
Makefile
4
Makefile
|
|
@ -1,7 +1,7 @@
|
|||
.PHONY: all clean
|
||||
|
||||
all: Everything.agda
|
||||
agda --html --html-dir=out Everything.agda --html-highlight=auto
|
||||
agda --html --html-dir=out Everything.agda --html-highlight=auto -i.
|
||||
pandoc out/MonadK.md -s -c Agda.css -o out/MonadK.html
|
||||
pandoc out/ElgotAlgebra.md -s -c Agda.css -o out/ElgotAlgebra.html
|
||||
|
||||
|
|
@ -14,4 +14,4 @@ open:
|
|||
firefox out/ElgotAlgebra.html
|
||||
|
||||
Everything.agda:
|
||||
git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda
|
||||
git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda
|
||||
|
|
@ -1,3 +1,3 @@
|
|||
name: bsc
|
||||
include: .
|
||||
include: src/
|
||||
depend: standard-library agda-categories
|
||||
|
|
@ -1,3 +1,4 @@
|
|||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
open import Level
|
||||
|
||||
open import Categories.Category.Cocartesian using (Cocartesian)
|
||||
|
|
|
|||
|
|
@ -1,355 +0,0 @@
|
|||
{-# OPTIONS --cubical --safe #-}
|
||||
|
||||
open import Level using (Level) renaming (suc to ℓ-suc)
|
||||
open import Function using (id; _∘_; _$_)
|
||||
open import Data.Product using (_×_; Σ; _,_; ∃-syntax; proj₁; proj₂)
|
||||
|
||||
open import CubicalIdentity using (_≡_; sym; trans; refl; cong; cong2; subst; subst-app)
|
||||
open CubicalIdentity.≡-Reasoning
|
||||
|
||||
open import Category
|
||||
open import Co-Cartesian
|
||||
open import Functor
|
||||
|
||||
--*
|
||||
{-
|
||||
This module introduces the notion of Elgot iteration in a category.
|
||||
-}
|
||||
--*
|
||||
|
||||
module ElgotIteration {ℓ : Level} {Ob : Set (ℓ-suc ℓ)} {C : Category Ob} (CoC : Co-Cartesian C) where
|
||||
|
||||
open Co-Cartesian.Co-Cartesian CoC renaming (_⊎_ to _+_)
|
||||
|
||||
module †-axioms (_† : ∀ {X Y : Obj} → (X ➔ Y + X) → (X ➔ Y)) where
|
||||
|
||||
-- Fixpoint
|
||||
Fix : Set (ℓ-suc ℓ)
|
||||
Fix = ∀ {X Y : Obj} {f : X ➔ Y + X}
|
||||
→ [ idm , f † ] ⊚ f ≡ f †
|
||||
|
||||
-- Naturality
|
||||
Nat : Set (ℓ-suc ℓ)
|
||||
Nat = ∀ {X Y Z : Obj} {f : X ➔ Y + X} {g : Y ➔ Z}
|
||||
→ ((g ⊕ idm) ⊚ f) † ≡ g ⊚ f †
|
||||
|
||||
-- Dinaturality
|
||||
Din : Set (ℓ-suc ℓ)
|
||||
Din = ∀ {X Y Z : Obj} {g : X ➔ Y + Z} {h : Z ➔ Y + X}
|
||||
→ ([ inl , h ] ⊚ g) † ≡ [ idm , ([ inl , g ] ⊚ h) † ] ⊚ g
|
||||
|
||||
-- Codiagonal
|
||||
Cod : Set (ℓ-suc ℓ)
|
||||
Cod = ∀ {X Y : Obj} {f : X ➔ (Y + X) + X}
|
||||
→ ([ idm , inr ] ⊚ f) † ≡ f † †
|
||||
|
||||
module _ {D : Category Ob} {CoC-D : Co-Cartesian D}
|
||||
{F : Functor D C id} (J : CoC-Functor CoC-D CoC F) where
|
||||
|
||||
open Co-Cartesian.Co-Cartesian CoC-D
|
||||
using () renaming (_➔_ to _➔′_; idm to idm′; _⊕_ to _⊕′_)
|
||||
open Functor.CoC-Functor J
|
||||
|
||||
Uni : Set (ℓ-suc ℓ)
|
||||
Uni = ∀ {X Y Z : Obj} {f : X ➔ Y + X} {g : Z ➔ Y + Z} {h : Z ➔′ X}
|
||||
→ f ⊚ (fmap h) ≡ (idm ⊕ fmap h) ⊚ g → f † ⊚ (fmap h) ≡ g †
|
||||
|
||||
open †-axioms
|
||||
|
||||
record ElgotIteration : Set (ℓ-suc ℓ) where
|
||||
|
||||
field
|
||||
_† : ∀ {X Y : Obj} → (X ➔ Y + X) → (X ➔ Y)
|
||||
fix : Fix _†
|
||||
|
||||
record ConwayIteration (It : ElgotIteration) : Set (ℓ-suc ℓ) where
|
||||
open ElgotIteration It public
|
||||
|
||||
field
|
||||
-- Naturality
|
||||
nat : Nat _†
|
||||
|
||||
-- Dinaturality
|
||||
din : Din _†
|
||||
|
||||
-- Codiagonal
|
||||
cod : Cod _†
|
||||
|
||||
record TotalUniConway (It : ElgotIteration) {D : Category Ob} {CoC-D : Co-Cartesian D}
|
||||
{F : Functor D C id} (J : CoC-Functor CoC-D CoC F) : Set (ℓ-suc ℓ) where
|
||||
|
||||
-- added uniformity, removed dinaturality;
|
||||
-- the latter is derivable, which is shown below
|
||||
open ElgotIteration It public
|
||||
|
||||
field
|
||||
-- Naturality
|
||||
nat : Nat _†
|
||||
|
||||
-- Codiagonal
|
||||
cod : Cod _†
|
||||
|
||||
-- Uniformity
|
||||
uni : Uni _† J
|
||||
|
||||
open Co-Cartesian.Co-Cartesian CoC-D
|
||||
using () renaming (inl to inl′; inr to inr′
|
||||
; _⊚_ to _⊚′_; idm to idm′; _➔_ to _➔′_
|
||||
; _⊎_ to _+′_ ; _⊕_ to _⊕′_; [_,_] to [_,_]′)
|
||||
|
||||
open CoC-Functor J
|
||||
|
||||
-- some coherence properties of injections,
|
||||
-- using the fact that J is identical on objects
|
||||
fmap-⊎F-inl : ∀ {X Y : Obj} → fmap (⊎F→ {X} {Y} (X ➔′_) inl′) ≡ inl
|
||||
fmap-⊎F-inl{X}{Y} = trans (sym $ subst-app (X ➔′_) {B₂ = X ➔_} (λ _ → fmap) ⊎F) $ sym inlF
|
||||
|
||||
fmap-⊎F-inr : ∀ {X Y : Obj} → fmap (⊎F→ {X} {Y} (Y ➔′_) inr′) ≡ inr
|
||||
fmap-⊎F-inr{X}{Y} = trans (sym $ subst-app (Y ➔′_) {B₂ = Y ➔_} (λ _ → fmap) ⊎F) $ sym inrF
|
||||
|
||||
-- an instance of uniformity for inl
|
||||
†-inl : ∀ {X Y Z : Obj} {f : (X + Z) ➔ Y + (X + Z)} {g : X ➔ Y + X}
|
||||
→ f ⊚ inl ≡ (idm ⊕ inl) ⊚ g → f † ⊚ inl ≡ g †
|
||||
†-inl {X} {Y} {Z} {f = f} {g = g} p =
|
||||
begin
|
||||
f † ⊚ inl
|
||||
≡˘⟨ cong (_⊚_ (f †)) fmap-⊎F-inl ⟩
|
||||
f † ⊚ fmap (⊎F→ (X ➔′_) inl′)
|
||||
≡⟨ uni p′ ⟩
|
||||
g †
|
||||
∎
|
||||
where
|
||||
p′ : f ⊚ fmap (⊎F→ (X ➔′_) inl′) ≡ (idm ⊕ fmap (⊎F→ (X ➔′_) inl′)) ⊚ g
|
||||
p′ = trans (cong (_⊚_ f) fmap-⊎F-inl) (trans p (cong (λ w → (idm ⊕ w) ⊚ g) $ sym fmap-⊎F-inl))
|
||||
|
||||
-- an instance of uniformity for inr
|
||||
†-inr : ∀ {X Y Z : Obj} {f : (Z + X) ➔ Y + (Z + X)} {g : X ➔ Y + X}
|
||||
→ f ⊚ inr ≡ (idm ⊕ inr) ⊚ g → f † ⊚ inr ≡ g †
|
||||
†-inr {X} {Y} {Z} {f = f} {g = g} p =
|
||||
begin
|
||||
f † ⊚ inr
|
||||
≡˘⟨ cong (_⊚_ (f †)) fmap-⊎F-inr ⟩
|
||||
f † ⊚ fmap (⊎F→ (X ➔′_) inr′)
|
||||
≡⟨ uni p′ ⟩
|
||||
g †
|
||||
∎
|
||||
where
|
||||
p′ : f ⊚ fmap (⊎F→ (X ➔′_) inr′) ≡ (idm ⊕ fmap (⊎F→ (X ➔′_) inr′)) ⊚ g
|
||||
p′ = trans (cong (_⊚_ f) fmap-⊎F-inr) $ trans p (cong (λ w → (idm ⊕ w) ⊚ g) (sym fmap-⊎F-inr))
|
||||
|
||||
-- an instance of uniformity for swap
|
||||
†-swap : ∀ {X Y Z : Obj} {f : (X + Y) ➔ Z + (X + Y)}
|
||||
→ f † ⊚ swap ≡ ((idm ⊕ swap) ⊚ (f ⊚ swap)) †
|
||||
|
||||
†-swap {X} {Y} {Z} {f = f} =
|
||||
begin
|
||||
f † ⊚ swap
|
||||
≡˘⟨ ⊚-cong₂ fmap-swap′ ⟩
|
||||
f † ⊚ (fmap swap′)
|
||||
≡⟨
|
||||
uni (trans (sym ⊚-unitˡ) $ trans
|
||||
(⊚-cong₁ $ trans (trans (sym [inl,inr]) $
|
||||
([]-destruct
|
||||
(trans (sym ⊚-unitʳ) $ ⊚-cong₂ $ sym ⊚-unitˡ)
|
||||
(trans (sym ⊚-unitʳ) $ ⊚-cong₂ $ trans (sym swap-swap) $
|
||||
⊚-cong (sym fmap-swap′) (sym fmap-swap′))
|
||||
))
|
||||
(sym ⊕-⊕)) $ sym ⊚-assoc)
|
||||
⟩
|
||||
((idm ⊕ fmap swap′) ⊚ (f ⊚ fmap swap′)) †
|
||||
≡⟨ cong2 (λ w w′ → ((idm ⊕ w) ⊚ (f ⊚ w′)) †) fmap-swap′ fmap-swap′ ⟩
|
||||
((idm ⊕ swap) ⊚ (f ⊚ swap)) †
|
||||
∎
|
||||
where
|
||||
swap′ : ∀ {X Y : Obj} → X + Y ➔′ Y + X
|
||||
swap′ {X} {Y} = ⊎F→ ((X + Y) ➔′_) (⊎F→ (_➔′ Y +′ X) [ inr′ , inl′ ]′)
|
||||
|
||||
fmap-swap′ : ∀ {X Y : Obj} → fmap (swap′{X}{Y}) ≡ swap{X}{Y}
|
||||
fmap-swap′{X}{Y} =
|
||||
begin
|
||||
fmap (swap′{X}{Y})
|
||||
≡˘⟨ subst-app ((X + Y) ➔′_) {B₂ = (X + Y) ➔_} (λ _ → fmap) ⊎F ⟩
|
||||
⊎F→ (X + Y ➔_) (fmap (⊎F→ (_➔′ Y +′ X) [ inr′ , inl′ ]′))
|
||||
≡˘⟨ cong (⊎F→ (X + Y ➔_)) (subst-app (_➔′ Y +′ X) {B₂ = _➔ Y +′ X} (λ _ → fmap) ⊎F) ⟩
|
||||
⊎F→ (X + Y ➔_) (⊎F→ (_➔ Y +′ X) (fmap [ inr′ , inl′ ]′))
|
||||
≡˘⟨ cong (⊎F→ (X + Y ➔_)) []F ⟩
|
||||
⊎F→ (X + Y ➔_) ([ fmap inr′ , fmap inl′ ])
|
||||
≡˘⟨ ⊎-destruct (trans []-inl (⊎F→⊚ h inl)) (trans []-inr (⊎F→⊚ h inr)) ⟩
|
||||
[ ⊎F→ (_➔_ X) (h ⊚ inl) , ⊎F→ (_➔_ Y) (h ⊚ inr) ]
|
||||
≡⟨
|
||||
[]-destruct
|
||||
(trans (cong (⊎F→ (_➔_ X)) []-inl) $ sym inrF)
|
||||
(trans (cong (⊎F→ (_➔_ Y)) []-inr) $ sym inlF)
|
||||
⟩
|
||||
[ inr , inl ]
|
||||
∎
|
||||
where h = [ fmap inr′ , fmap inl′ ]
|
||||
|
||||
bekić : ∀ {X Y Z : Obj} {f : X ➔ (Y + X) + Z} {g : Z ➔ (Y + X) + Z}
|
||||
→ [([ idm , g † ] ⊚ f)† , [ idm , ([ idm , g † ] ⊚ f)† ] ⊚ g † ]
|
||||
≡ ([ idm ⊕ inl , inr ⊚ inr ] ⊚ [ f , g ]) †
|
||||
|
||||
bekić {f = f} {g = g} =
|
||||
begin
|
||||
[ ([ idm , g † ] ⊚ f) † , [ idm , ([ idm , g † ] ⊚ f) † ] ⊚ g † ]
|
||||
-- using bekić₁
|
||||
≡⟨ bekić₁ ⟩
|
||||
([ (idm ⊕ inl) ⊚ ([ idm , g † ] ⊚ f) , (idm ⊕ inl) ⊚ g † ] †)
|
||||
≡⟨ cong _† $ []-cong₁ ⊚-assoc ⟩
|
||||
([ ((idm ⊕ inl) ⊚ [ idm , g † ]) ⊚ f , (idm ⊕ inl) ⊚ g † ] †)
|
||||
≡⟨ cong _† $ []-cong₁ $ trans (⊚-cong₁ ⊚-distrib-[]) $ ⊚-cong₁ $ []-cong₁ ⊚-unitʳ ⟩
|
||||
[ [ idm ⊕ inl , (idm ⊕ inl) ⊚ g † ] ⊚ f , (idm ⊕ inl) ⊚ g † ] †
|
||||
≡˘⟨ cong _† $ []-cong₁ $ ⊚-cong₁ $ trans []-⊕ ([]-destruct ⊚-unitˡ ⊚-unitʳ) ⟩
|
||||
[ ([ idm , (idm ⊕ inl) ⊚ g † ] ⊚ ((idm ⊕ inl) ⊕ idm)) ⊚ f , (idm ⊕ inl) ⊚ g † ] †
|
||||
≡˘⟨ cong _† $ []-cong₁ $ ⊚-assoc ⟩
|
||||
[ [ idm , (idm ⊕ inl) ⊚ g † ] ⊚ (((idm ⊕ inl) ⊕ idm) ⊚ f) , (idm ⊕ inl) ⊚ g † ] †
|
||||
-- using naturality
|
||||
≡⟨ cong _† $ []-destruct (⊚-cong₁ $ []-cong₂ $ sym nat) (sym nat) ⟩
|
||||
[ [ idm , (((idm ⊕ inl) ⊕ idm) ⊚ g) † ] ⊚ (((idm ⊕ inl) ⊕ idm) ⊚ f) , (((idm ⊕ inl) ⊕ idm) ⊚ g) † ] †
|
||||
-- using bekić₂
|
||||
≡⟨ cong _† $ trans bekić₂ $ cong _† $ sym ⊚-distrib-[] ⟩
|
||||
((idm ⊕ inr) ⊚ [ ((idm ⊕ inl) ⊕ idm) ⊚ f , ((idm ⊕ inl) ⊕ idm) ⊚ g ]) † †
|
||||
≡⟨ cong (_† ∘ _†) $ ⊚-cong₂ $ sym ⊚-distrib-[] ⟩
|
||||
((idm ⊕ inr) ⊚ (((idm ⊕ inl) ⊕ idm) ⊚ [ f , g ])) † †
|
||||
≡⟨ cong (_† ∘ _†) $ trans ⊚-assoc $ ⊚-cong₁ $ trans ⊕-⊕ $
|
||||
[]-destruct (⊚-cong₂ ⊚-unitˡ) (⊚-cong₂ ⊚-unitʳ) ⟩
|
||||
(((idm ⊕ inl) ⊕ inr) ⊚ [ f , g ]) † †
|
||||
-- using codiagonal
|
||||
≡˘⟨ cod ⟩
|
||||
([ idm , inr ] ⊚ (((idm ⊕ inl) ⊕ inr) ⊚ [ f , g ])) †
|
||||
≡⟨ cong _† ⊚-assoc ⟩
|
||||
(([ idm , inr ] ⊚ ((idm ⊕ inl) ⊕ inr)) ⊚ [ f , g ]) †
|
||||
≡⟨ cong _† $ ⊚-cong₁ $ trans []-⊕ $ []-cong₁ ⊚-unitˡ ⟩
|
||||
([(idm ⊕ inl) , inr ⊚ inr ] ⊚ [ f , g ]) †
|
||||
∎
|
||||
|
||||
where
|
||||
|
||||
-- one instance of the Bekić law
|
||||
bekić₁ : ∀ {X Y Z : Obj} {f : X ➔ Y + X}{g : Z ➔ Y + X}
|
||||
→ [ f † , [ idm , f † ] ⊚ g ] ≡ [ (idm ⊕ inl) ⊚ f , (idm ⊕ inl) ⊚ g ] †
|
||||
|
||||
bekić₁ {f = f} {g = g} =
|
||||
begin
|
||||
[ f † , [ idm , f † ] ⊚ g ]
|
||||
≡˘⟨ []-destruct (†-inl []-inl) $ ⊚-cong₁ $ []-cong₂ $ †-inl []-inl ⟩
|
||||
[ h † ⊚ inl , [ idm , h † ⊚ inl ] ⊚ g ]
|
||||
≡˘⟨ []-cong₂ $ ⊚-cong₁ $ []-cong₁ $ ⊚-unitʳ ⟩
|
||||
[ h † ⊚ inl , [ idm ⊚ idm , h † ⊚ inl ] ⊚ g ]
|
||||
≡˘⟨ []-cong₂ $ ⊚-cong₁ $ []-⊕ ⟩
|
||||
[ h † ⊚ inl , ([ idm , h † ] ⊚ (idm ⊕ inl)) ⊚ g ]
|
||||
≡˘⟨ []-cong₂ $ ⊚-assoc ⟩
|
||||
[ h † ⊚ inl , [ idm , h † ] ⊚ ((idm ⊕ inl) ⊚ g) ]
|
||||
≡˘⟨ []-cong₂ $ ⊚-cong₂ $ []-inr ⟩
|
||||
[ h † ⊚ inl , [ idm , h † ] ⊚ (h ⊚ inr) ]
|
||||
≡⟨ []-cong₂ $ ⊚-assoc ⟩
|
||||
[ h † ⊚ inl , ([ idm , h † ] ⊚ h) ⊚ inr ]
|
||||
≡⟨ []-cong₂ $ ⊚-cong₁ $ fix ⟩
|
||||
[ h † ⊚ inl , h † ⊚ inr ]
|
||||
≡˘⟨ ⊚-distrib-[] ⟩
|
||||
h † ⊚ [ inl , inr ]
|
||||
≡⟨ ⊚-cong₂ [inl,inr] ⟩
|
||||
h † ⊚ idm
|
||||
≡⟨ ⊚-unitʳ ⟩
|
||||
h †
|
||||
∎
|
||||
where h = [ (idm ⊕ inl) ⊚ f , (idm ⊕ inl) ⊚ g ]
|
||||
|
||||
-- another instance of the Bekić law
|
||||
bekić₂ : ∀ {X Y Z : Obj} {f : X ➔ Y + X} {g : Z ➔ Y + X}
|
||||
→ [ [ idm , f † ] ⊚ g , f † ] ≡ [ (idm ⊕ inr) ⊚ g , (idm ⊕ inr) ⊚ f ] †
|
||||
bekić₂ {f = f} {g = g} =
|
||||
begin
|
||||
[ [ idm , f † ] ⊚ g , f † ]
|
||||
≡˘⟨ []-destruct (⊚-cong₁ $ []-cong₂ $ †-inr []-inr) (†-inr []-inr) ⟩
|
||||
[ [ idm , h † ⊚ inr ] ⊚ g , h † ⊚ inr ]
|
||||
≡˘⟨ []-cong₁ $ ⊚-cong₁ $ []-cong₁ $ ⊚-unitʳ ⟩
|
||||
[ [ idm ⊚ idm , h † ⊚ inr ] ⊚ g , h † ⊚ inr ]
|
||||
≡˘⟨ []-cong₁ $ ⊚-cong₁ $ []-⊕ ⟩
|
||||
[ ([ idm , h † ] ⊚ (idm ⊕ inr)) ⊚ g , h † ⊚ inr ]
|
||||
≡˘⟨ []-cong₁ $ ⊚-assoc ⟩
|
||||
[ [ idm , h † ] ⊚ ((idm ⊕ inr) ⊚ g) , h † ⊚ inr ]
|
||||
≡˘⟨ []-cong₁ $ ⊚-cong₂ $ []-inl ⟩
|
||||
[ [ idm , h † ] ⊚ (h ⊚ inl) , h † ⊚ inr ]
|
||||
≡⟨ []-cong₁ $ ⊚-assoc ⟩
|
||||
[ ([ idm , h † ] ⊚ h) ⊚ inl , h † ⊚ inr ]
|
||||
≡⟨ []-cong₁ $ ⊚-cong₁ $ fix ⟩
|
||||
[ h † ⊚ inl , h † ⊚ inr ]
|
||||
≡˘⟨ ⊚-distrib-[] ⟩
|
||||
h † ⊚ [ inl , inr ]
|
||||
≡⟨ ⊚-cong₂ [inl,inr] ⟩
|
||||
h † ⊚ idm
|
||||
≡⟨ ⊚-unitʳ ⟩
|
||||
h †
|
||||
∎
|
||||
where h = [ (idm ⊕ inr) ⊚ g , (idm ⊕ inr) ⊚ f ]
|
||||
|
||||
-- Dinaturality
|
||||
din : Din _†
|
||||
din {g = g} {h = h} =
|
||||
begin
|
||||
([ inl , h ] ⊚ g) †
|
||||
≡˘⟨ []-inl ⟩
|
||||
[([ inl , h ] ⊚ g) † , [ idm , ([ inl , h ] ⊚ g) † ] ⊚ h ] ⊚ inl
|
||||
≡˘⟨ ⊚-cong₁ helper₁ ⟩
|
||||
[ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † ⊚ inl
|
||||
≡⟨ trans (⊚-cong₁ (sym helper₂)) (trans (sym ⊚-assoc) (⊚-cong₂ []-inl)) ⟩
|
||||
[ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † ⊚ inr
|
||||
-- using fix
|
||||
≡⟨ trans (⊚-cong₁ (sym fix)) (trans (sym ⊚-assoc) (trans (⊚-cong₂ []-inr) ⊚-assoc)) ⟩
|
||||
([ idm , [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † ] ⊚ (idm ⊕ inl)) ⊚ g
|
||||
≡⟨ ⊚-cong₁ (trans []-⊕ ([]-cong₁ ⊚-unitˡ)) ⟩
|
||||
[ idm , [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] † ⊚ inl ] ⊚ g
|
||||
≡⟨ trans (cong (λ w → [ idm , w ⊚ inl ] ⊚ g) helper₁) (cong (λ w → [ idm , w ] ⊚ g) []-inl) ⟩
|
||||
[ idm , ([ inl , g ] ⊚ h) † ] ⊚ g
|
||||
∎
|
||||
where
|
||||
helper₁ : ∀ {X Y Z : Obj} {g : X ➔ Y + Z} {h : Z ➔ Y + X} →
|
||||
[ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † ≡ [([ inl , h ] ⊚ g) † , [ idm , ([ inl , h ] ⊚ g) † ] ⊚ h ]
|
||||
helper₁{X}{Y}{Z}{g = g}{h = h} =
|
||||
begin
|
||||
[ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] †
|
||||
≡˘⟨ cong _† $ []-cong₁ $ ⊚-cong₁ $ []-destruct []-inl ⊚-unitʳ ⟩
|
||||
([ [ (idm ⊕ inl) ⊚ inl , (inr ⊚ inr) ⊚ idm ] ⊚ g , (idm ⊕ inl) ⊚ h ] †)
|
||||
≡˘⟨ cong _† $ trans ⊚-distrib-[] $
|
||||
[]-destruct
|
||||
(trans ⊚-assoc $ ⊚-cong₁ []-⊕)
|
||||
(trans ⊚-assoc $ ⊚-cong₁ []-inl) ⟩
|
||||
(([ idm ⊕ inl , inr ⊚ inr ] ⊚ [ (inl ⊕ idm) ⊚ g , inl ⊚ h ]) †)
|
||||
≡˘⟨ bekić{f = (inl ⊕ idm) ⊚ g}{g = inl ⊚ h} ⟩
|
||||
[ ([ idm , (inl ⊚ h) † ] ⊚ ((inl ⊕ idm) ⊚ g))† ,
|
||||
[ idm , ([ idm , (inl ⊚ h) † ] ⊚ ((inl ⊕ idm) ⊚ g))† ] ⊚ ((inl ⊚ h) †) ]
|
||||
≡⟨ cong2 (λ w₁ w₂ → [ w₁ † , [ idm , w₂ † ] ⊚ ((inl ⊚ h) †) ])
|
||||
(trans ⊚-assoc $ cong (_⊚ g) $ trans []-⊕ $ []-destruct ⊚-unitˡ ⊚-unitʳ)
|
||||
(trans ⊚-assoc $ cong (_⊚ g) $ trans []-⊕ $ []-destruct ⊚-unitˡ ⊚-unitʳ) ⟩
|
||||
[ ([ inl , (inl ⊚ h) † ] ⊚ g) † , [ idm , ([ inl , (inl ⊚ h) † ] ⊚ g) † ] ⊚ ((inl ⊚ h) †) ]
|
||||
≡⟨ []-destruct
|
||||
(cong _† $ ⊚-cong₁ $ []-cong₂ inl-h†)
|
||||
(cong2 (λ w₁ w₂ → [ idm , ([ inl , w₁ ] ⊚ g) † ] ⊚ w₂) inl-h† inl-h†) ⟩
|
||||
[([ inl , h ] ⊚ g) † , [ idm , ([ inl , h ] ⊚ g)† ] ⊚ h ]
|
||||
∎
|
||||
where
|
||||
inl-h† : (inl ⊚ h) † ≡ h
|
||||
inl-h† = trans (sym fix) $ trans ⊚-assoc $ trans (⊚-cong₁ []-inl) ⊚-unitˡ
|
||||
|
||||
helper₂ : ∀ {X Y Z : Obj} {g : X ➔ Y + Z} {h : Z ➔ Y + X} →
|
||||
[ (idm ⊕ inr) ⊚ g , (idm ⊕ inl) ⊚ h ] † ⊚ swap ≡ [ (idm ⊕ inr) ⊚ h , (idm ⊕ inl) ⊚ g ] †
|
||||
helper₂ = trans †-swap $
|
||||
cong _† $ trans (⊚-cong₂ []-swap) (trans ⊚-distrib-[] $ []-destruct
|
||||
(trans ⊚-assoc $ ⊚-cong₁ $ trans ⊕-⊕ $ []-destruct (⊚-cong₂ ⊚-unitˡ) $ ⊚-cong₂ []-inl)
|
||||
(trans ⊚-assoc $ ⊚-cong₁ $ trans ⊕-⊕ $ []-destruct (⊚-cong₂ ⊚-unitˡ) $ ⊚-cong₂ []-inr))
|
||||
|
||||
|
||||
module _ (It : ElgotIteration) {D : Category Ob} {CoC-D : Co-Cartesian D}
|
||||
{F : Functor D C id} (J : CoC-Functor CoC-D CoC F) where
|
||||
|
||||
TotalUniConway→ConwayIteration : TotalUniConway It J → ConwayIteration It
|
||||
TotalUniConway→ConwayIteration TC =
|
||||
record {
|
||||
nat = nat ;
|
||||
din = din ;
|
||||
cod = cod
|
||||
}
|
||||
|
||||
where
|
||||
open TotalUniConway TC
|
||||
Loading…
Reference in a new issue