leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Compare commits

base: leonv:11107c67b82df8f79d7b163baf503e2eaef78cff
Branches Tags
leonv:main
leonv:Abgabe
..
compare: leonv:ac3b80c4f6b0f421bd419faf7f0cf66932aa874c
Branches Tags
leonv:main
leonv:Abgabe

No commits in common. "11107c67b82df8f79d7b163baf503e2eaef78cff" and "ac3b80c4f6b0f421bd419faf7f0cf66932aa874c" have entirely different histories.
11107c67b8 ... ac3b80c4f6

2 changed files with 22 additions and 104 deletions
Show stats Expand all files Collapse all files

23
src/Algebra/Elgot.lagda.md
View file

@ -139,6 +139,7 @@ Here we give a different Characterization and show that it is equal.
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩ [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩
(idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎ (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
-- TODO Proposition 41
#-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) # #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) #
#-Diamond {X} f = begin #-Diamond {X} f = begin
g # ≈⟨ introʳ inject₂ ⟩ g # ≈⟨ introʳ inject₂ ⟩
@ -152,8 +153,7 @@ Here we give a different Characterization and show that it is equal.
[ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ [ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ [ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ [ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ pullˡ (sym (#-Uniformity by-uni₂)) ⟩ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X} ≈⟨ {! !} ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₂ ≈⟨ (refl⟩∘⟨ (pullˡ inject₂ ○ (+₁∘i₂ ○ identityʳ))) ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X} ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X} ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩
[ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩
([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩ ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩
@ -167,24 +167,13 @@ Here we give a different Characterization and show that it is equal.
where where
g = (idC +₁ [ idC , idC ]) ∘ f g = (idC +₁ [ idC , idC ]) ∘ f
h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
by-uni₂ : (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]
by-uni₂ = begin
(idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₁ , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) ∘[] ⟩
[ i₁ , [ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₂ ∘ f ] ] ≈⟨ []-cong₂ refl ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂)) ⟩
[ i₁ , [ (idC ∘ idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ f ] ] ≈⟨ []-cong₂ refl ([]-cong₂ ((+₁-cong₂ identity² (pullˡ inject₂ ○ +₁∘i₁)) ⟩∘⟨refl) (∘[] ⟩∘⟨refl)) ⟩
[ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] ] ≈˘⟨ []-cong₂ refl ([]-cong₂ refl (pullˡ ∘[])) ⟩
[ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , i₂ ∘ h ] ] ≈˘⟨ []-cong₂ inject₁ ([]-cong₂ inject₂ identityʳ) ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₂ , (i₂ ∘ h) ∘ idC ] ] ≈˘⟨ []-cong₂ (pullˡ inject₁) []∘+₁ ⟩
[ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₁ ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ (i₂ +₁ idC) ] ≈˘⟨ ∘[] ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∎
by-uni₁ : (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈ g ∘ [ idC , idC ] by-uni₁ : (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈ g ∘ [ idC , idC ]
by-uni₁ = begin by-uni₁ = begin
(idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩ (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ idC , idC ]) ∘ (idC +₁ i₁) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩ [ (idC +₁ [ idC , idC ]) ∘ (idC +₁ i₁) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩
[ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩
[ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ [ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩
g ∘ [ idC , idC ] ∎ g ∘ [ idC , idC ] ∎
by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ] by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
by-fix = sym (begin by-fix = sym (begin
[ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩ [ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩

103
src/Monad/Instance/K/Instance/Maybe.lagda.md
View file

@ -10,17 +10,11 @@ open import Categories.Monad
open import Categories.Category.Monoidal.Instance.Setoids open import Categories.Category.Monoidal.Instance.Setoids
open import Categories.Category.Cocartesian open import Categories.Category.Cocartesian
open import Categories.Object.Terminal open import Categories.Object.Terminal
open import Function.Equality as SΠ renaming (id to idₛ) open import Function.Equality as SΠ renaming (id to ⟶-id)
import Categories.Morphism.Reasoning as MR import Categories.Morphism.Reasoning as MR
open import Relation.Binary open import Relation.Binary
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Sum.Function.Setoid
open import Data.Sum.Relation.Binary.Pointwise
open import Agda.Builtin.Unit using (tt) open import Agda.Builtin.Unit using (tt)
open import Data.Unit.Polymorphic using () renaming (⊤ to ⊤ₚ)
open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ₚ)
open import Categories.NaturalTransformation using (ntHelper)
open import Function.Base using (id)
``` ```
--> -->
@ -33,92 +27,27 @@ open Ambient ambient using ()
Assuming the axiom of choice, the maybe monad is an instance of K in the category of setoids. Assuming the axiom of choice, the maybe monad is an instance of K in the category of setoids.
```agda ```agda
module _ {c ℓ : Level} where module _ {c ℓ' : Level} where
data Maybe (A : Set c) : Set c where open Cocartesian (Setoids-Cocartesian {c} {c ⊔ ℓ'})
nothing : Maybe A open Terminal (terminal {c} {c ⊔ ℓ'})
just : A → Maybe A open MR (Setoids c (c ⊔ ℓ'))
open Category (Setoids c (c ⊔ ℓ'))
maybe-eq : ∀ (A : Setoid c ℓ) → Maybe (Setoid.Carrier A) → Maybe (Setoid.Carrier A) → Set ℓ open Equiv
maybe-eq _ nothing nothing = ⊤ₚ
maybe-eq _ nothing (just y) = ⊥ₚ
maybe-eq _ (just x) nothing = ⊥ₚ
maybe-eq A (just x) (just y) = Setoid._≈_ A x y
maybeSetoid : Setoid c ℓ → Setoid c ℓ maybe : Monad (Setoids c (c ⊔ ℓ'))
maybeSetoid A = record { Carrier = Maybe A.Carrier ; _≈_ = maybe-eq A ; isEquivalence = record { refl = λ {x} → refl' {x = x} ; sym = λ {x y} → sym' {x} {y} ; trans = λ {x y z} → trans' {x} {y} {z} } } maybe = record
where
module A = Setoid A
refl' : Reflexive (maybe-eq A)
refl' {nothing} = lift tt
refl' {just x} = IsEquivalence.refl A.isEquivalence
sym' : Symmetric (maybe-eq A)
sym' {nothing} {nothing} = id
sym' {nothing} {just y} = id
sym' {just x} {nothing} = id
sym' {just x} {just y} = IsEquivalence.sym A.isEquivalence
trans' : Transitive (maybe-eq A)
trans' {nothing} {nothing} {nothing} = λ _ → id
trans' {nothing} {nothing} {just z} = λ _ → id
trans' {nothing} {just y} {nothing} = λ _ _ → lift tt
trans' {nothing} {just y} {just z} = λ ()
trans' {just x} {nothing} {nothing} = λ ()
trans' {just x} {nothing} {just z} = λ ()
trans' {just x} {just y} {nothing} = λ _ → id
trans' {just x} {just y} {just z} = IsEquivalence.trans A.isEquivalence
maybeFun : ∀ {A B : Setoid c ℓ} → A ⟶ B → maybeSetoid A ⟶ maybeSetoid B
maybeFun {A} {B} f = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j }
where
app : Setoid.Carrier (maybeSetoid A) → Setoid.Carrier (maybeSetoid B)
app nothing = nothing
app (just x) = just (f ⟨$⟩ x)
cong' : ∀ (i j : Maybe (Setoid.Carrier A)) → maybe-eq A i j → maybe-eq B (app i) (app j)
cong' nothing nothing i≈j = i≈j
cong' (just _) (just _) i≈j = cong f i≈j
_≋_ : ∀ {A B : Setoid c ℓ} → A ⟶ B → A ⟶ B → Set (c ⊔ ℓ)
_≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
maybeFun-id : ∀ {A : Setoid c ℓ} → (maybeFun idₛ) ≋ idₛ {A = maybeSetoid A}
maybeFun-id {A} {nothing} {nothing} i≈j = i≈j
maybeFun-id {A} {just _} {just _} i≈j = i≈j
η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A
η A = record { _⟨$⟩_ = just ; cong = id }
μ : ∀ (A : Setoid c ℓ) → maybeSetoid (maybeSetoid A) ⟶ maybeSetoid A
μ A = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j }
where
app : Setoid.Carrier (maybeSetoid (maybeSetoid A)) → Setoid.Carrier (maybeSetoid A)
app nothing = nothing
app (just x) = x
cong' : ∀ (i j : Maybe (Maybe (Setoid.Carrier A))) → maybe-eq (maybeSetoid A) i j → maybe-eq A (app i) (app j)
cong' nothing nothing i≈j = i≈j
cong' (just i) (just j) i≈j = i≈j
maybeMonad : Monad (Setoids c ℓ)
maybeMonad = record
{ F = record { F = record
{ F₀ = maybeSetoid { F₀ = λ X → X + ⊤
; F₁ = maybeFun ; F₁ = λ {A} {B} f → f +₁ ⟶-id
; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y} ; identity = {! !}
; homomorphism = {! !} ; homomorphism = {! !}
; F-resp-≈ = {! !} ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → +₁-cong₂ f≈g ?
} }
; η = ntHelper (record ; η = {! !}
{ η = η ; μ = {! !}
; commute = {! !}
})
; μ = ntHelper (record
{ η = μ
; commute = {! !}
})
; assoc = {! !} ; assoc = {! !}
; sym-assoc = {! !} ; sym-assoc = {! !}
; identityˡ = {! !} ; identityˡ = {! !}
; identityʳ = {! !} ; identityʳ = {! !}
} }
``` ```