fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Merge branch 'dev'

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 12:57:19 +01:00
parent 5b2681392c 002badd98d
commit c3b585d03b
12 changed files with 368 additions and 459 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
CHANGELOG.md
View file

@ -1,6 +1,23 @@
Changelog
=========
Version 1.2.0
-------------
This version is mainly a huge refactor.
I've renamed
* `distrib` to `isDistributive`
* `arrowIsSet` to `arrowsAreSets`
* `ident` to `isIdentity`
* `assoc` to `isAssociative`
And added "type-synonyms" for all of these. Their names should now match their
type. So e.g. `isDistributive` has type `IsDistributive`.
I've also changed how names are exported in `Functor` to be in line with
`Category`.
Version 1.1.0
-------------
In this version categories have been refactored - there's now a notion of a raw

325
src/Cat/Categories/Cat.agda
View file

@ -16,75 +16,22 @@ open import Cat.Category.Exponential
open import Cat.Equality
open Equality.Data.Product
open Functor
open IsFunctor
open Category hiding (_∘_)
open Functor using (func→ ; func*)
open Category using (Object ; 𝟙)
-- The category of categories
module _ (ℓ ℓ' : Level) where
private
module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
private
eq* : func* (H ∘f (G ∘f F)) ≡ func* ((H ∘f G) ∘f F)
eq* = refl
eq→ : PathP
(λ i → {A B : Object 𝔸} → 𝔸 [ A , B ] → 𝔻 [ eq* i A , eq* i B ])
(func→ (H ∘f (G ∘f F))) (func→ ((H ∘f G) ∘f F))
eq→ = refl
postulate
eqI
: (λ i → ∀ {A : Object 𝔸} → eq→ i (𝟙 𝔸 {A}) ≡ 𝟙 𝔻 {eq* i A})
[ (H ∘f (G ∘f F)) .isFunctor .ident
≡ ((H ∘f G) ∘f F) .isFunctor .ident
]
eqD
: (λ i → ∀ {A B C} {f : 𝔸 [ A , B ]} {g : 𝔸 [ B , C ]}
→ eq→ i (𝔸 [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
[ (H ∘f (G ∘f F)) .isFunctor .distrib
≡ ((H ∘f G) ∘f F) .isFunctor .distrib
]
assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F
assc = Functor≡ eq* eq→ (IsFunctor≡ eqI eqD)
assc = Functor≡ refl refl
module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
module _ where
private
eq* : (func* F) ∘ (func* (identity {C = ℂ})) ≡ func* F
eq* = refl
-- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
eq→ : PathP
(λ i →
{x y : Object ℂ} → Arrow ℂ x y → Arrow 𝔻 (func* F x) (func* F y))
(func→ (F ∘f identity)) (func→ F)
eq→ = refl
postulate
eqI-r
: (λ i → {c : Object ℂ} → (λ _ → 𝔻 [ func* F c , func* F c ])
[ func→ F (𝟙 ℂ) ≡ 𝟙 𝔻 ])
[(F ∘f identity) .isFunctor .ident ≡ F .isFunctor .ident ]
eqD-r : PathP
(λ i →
{A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} →
eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
ident-r : F ∘f identity ≡ F
ident-r = Functor≡ eq* eq→ (IsFunctor≡ eqI-r eqD-r)
module _ where
private
postulate
eq* : (identity ∘f F) .func* ≡ F .func*
eq→ : PathP
(λ i → {x y : Object ℂ} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
((identity ∘f F) .func→) (F .func→)
eqI : (λ i → ∀ {A : Object ℂ} → eq→ i (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {eq* i A})
[ ((identity ∘f F) .isFunctor .ident) ≡ (F .isFunctor .ident) ]
eqD : PathP (λ i → {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
→ eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
-- (λ z → eq* i z) (eq→ i)
ident-r = Functor≡ refl refl
ident-l : identity ∘f F ≡ F
ident-l = Functor≡ eq* eq→ λ i → record { ident = eqI i ; distrib = eqD i }
ident-l = Functor≡ refl refl
RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
RawCat =
@ -93,30 +40,34 @@ module _ (ℓ ℓ' : Level) where
; Arrow = Functor
; 𝟙 = identity
; _∘_ = _∘f_
-- What gives here? Why can I not name the variables directly?
-- ; isCategory = record
-- { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H}
-- ; ident = ident-r , ident-l
-- }
}
open IsCategory
instance
:isCategory: : IsCategory RawCat
assoc :isCategory: {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
ident :isCategory: = ident-r , ident-l
arrow-is-set :isCategory: = {!!}
univalent :isCategory: = {!!}
private
open RawCategory RawCat
isAssociative : IsAssociative
isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
-- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor.
ident' : IsIdentity identity
ident' = ident-r , ident-l
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of
-- categories. There does, however, exist a 2-category of 1-categories.
Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
raw Cat = RawCat
-- Because of the note above there is not category of categories.
Cat : (unprovable : IsCategory RawCat) → Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
Category.raw (Cat _) = RawCat
Category.isCategory (Cat unprovable) = unprovable
-- Category.raw Cat _ = RawCat
-- Category.isCategory Cat unprovable = unprovable
module _ {ℓ ℓ' : Level} where
-- The following to some extend depends on the category of categories being a
-- category. In some places it may not actually be needed, however.
module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
module _ (ℂ 𝔻 : Category ℓ ℓ') where
private
Catt = Cat ℓ ℓ'
Catt = Cat ℓ ℓ' unprovable
:Object: = Object ℂ × Object 𝔻
:Arrow: : :Object: → :Object: → Set ℓ'
:Arrow: (c , d) (c' , d') = Arrow ℂ c c' × Arrow 𝔻 d d'
:Arrow: (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
:𝟙: : {o : :Object:} → :Arrow: o o
:𝟙: = 𝟙 ℂ , 𝟙 𝔻
_:⊕:_ :
@ -131,70 +82,67 @@ module _ {ℓ ℓ' : Level} where
RawCategory.Arrow :rawProduct: = :Arrow:
RawCategory.𝟙 :rawProduct: = :𝟙:
RawCategory._∘_ :rawProduct: = _:⊕:_
open RawCategory :rawProduct:
module C = IsCategory (ℂ .isCategory)
module D = IsCategory (𝔻 .isCategory)
postulate
issSet : {A B : RawCategory.Object :rawProduct:} → isSet (RawCategory.Arrow :rawProduct: A B)
module C = Category ℂ
module D = Category 𝔻
open import Cubical.Sigma
issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B)
issSet = setSig {sA = C.arrowsAreSets} {sB = λ x → D.arrowsAreSets}
ident' : IsIdentity :𝟙:
ident'
= Σ≡ (fst C.isIdentity) (fst D.isIdentity)
, Σ≡ (snd C.isIdentity) (snd D.isIdentity)
postulate univalent : Univalence.Univalent :rawProduct: ident'
instance
:isCategory: : IsCategory :rawProduct:
-- :isCategory: = record
-- { assoc = Σ≡ C.assoc D.assoc
-- ; ident
-- = Σ≡ (fst C.ident) (fst D.ident)
-- , Σ≡ (snd C.ident) (snd D.ident)
-- ; arrow-is-set = issSet
-- ; univalent = {!!}
-- }
IsCategory.assoc :isCategory: = Σ≡ C.assoc D.assoc
IsCategory.ident :isCategory:
= Σ≡ (fst C.ident) (fst D.ident)
, Σ≡ (snd C.ident) (snd D.ident)
IsCategory.arrow-is-set :isCategory: = issSet
IsCategory.univalent :isCategory: = {!!}
IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative
IsCategory.isIdentity :isCategory: = ident'
IsCategory.arrowsAreSets :isCategory: = issSet
IsCategory.univalent :isCategory: = univalent
:product: : Category ℓ ℓ'
raw :product: = :rawProduct:
Category.raw :product: = :rawProduct:
proj₁ : Catt [ :product: , ℂ ]
proj₁ = record { func* = fst ; func→ = fst ; isFunctor = record { ident = refl ; distrib = refl } }
proj₁ = record
{ raw = record { func* = fst ; func→ = fst }
; isFunctor = record { isIdentity = refl ; isDistributive = refl }
}
proj₂ : Catt [ :product: , 𝔻 ]
proj₂ = record { func* = snd ; func→ = snd ; isFunctor = record { ident = refl ; distrib = refl } }
proj₂ = record
{ raw = record { func* = snd ; func→ = snd }
; isFunctor = record { isIdentity = refl ; isDistributive = refl }
}
module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where
open Functor
x : Functor X :product:
x = record
{ raw = record
{ func* = λ x → x₁ .func* x , x₂ .func* x
; func→ = λ x → func→ x₁ x , func→ x₂ x
}
; isFunctor = record
{ isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity
; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive
}
}
where
open module x₁ = Functor x₁
open module x₂ = Functor x₂
postulate x : Functor X :product:
-- x = record
-- { func* = λ x → x₁ .func* x , x₂ .func* x
-- ; func→ = λ x → func→ x₁ x , func→ x₂ x
-- ; isFunctor = record
-- { ident = Σ≡ x₁.ident x₂.ident
-- ; distrib = Σ≡ x₁.distrib x₂.distrib
-- }
-- }
-- where
-- open module x₁ = IsFunctor (x₁ .isFunctor)
-- open module x₂ = IsFunctor (x₂ .isFunctor)
isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
isUniqL = Functor≡ eq* eq→
where
eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
eq* = refl
eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
[ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
eq→ = refl
-- Turned into postulate after:
-- > commit e8215b2c051062c6301abc9b3f6ec67106259758 (HEAD -> dev, github/dev)
-- > Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
-- > Date: Mon Feb 5 14:59:53 2018 +0100
postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
-- isUniqL = Functor≡ eq* eq→ {!!}
-- where
-- eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
-- eq* = {!refl!}
-- eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
-- [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
-- eq→ = refl
-- postulate eqIsF : (Catt [ proj₁ ∘ x ]) .isFunctor ≡ x₁ .isFunctor
-- eqIsF = IsFunctor≡ {!refl!} {!!}
postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
-- isUniqR = Functor≡ refl refl {!!} {!!}
isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
isUniqR = Functor≡ refl refl
isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
isUniq = isUniqL , isUniqR
@ -203,36 +151,37 @@ module _ {ℓ ℓ' : Level} where
uniq = x , isUniq
instance
isProduct : IsProduct (Cat ℓ ℓ') proj₁ proj₂
isProduct : IsProduct Catt proj₁ proj₂
isProduct = uniq
product : Product {ℂ = (Cat ℓ ℓ')} ℂ 𝔻
product : Product {ℂ = Catt} ℂ 𝔻
product = record
{ obj = :product:
; proj₁ = proj₁
; proj₂ = proj₂
}
module _ {ℓ ℓ' : Level} where
module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
Catt = Cat ℓ ℓ' unprovable
instance
hasProducts : HasProducts (Cat ℓ ℓ')
hasProducts = record { product = product }
hasProducts : HasProducts Catt
hasProducts = record { product = product unprovable }
-- Basically proves that `Cat ℓ ℓ` is cartesian closed.
module _ (ℓ : Level) where
module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
private
open Data.Product
open import Cat.Categories.Fun
Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
Catℓ = Cat ℓ ℓ
Catℓ = Cat ℓ ℓ unprovable
module _ (ℂ 𝔻 : Category ℓ ℓ) where
private
:obj: : Object (Cat ℓ ℓ)
:obj: : Object Catℓ
:obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
:func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
:func*: (F , A) = F .func* A
:func*: (F , A) = func* F A
module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
private
@ -247,30 +196,30 @@ module _ (ℓ : Level) where
B = proj₂ cod
:func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
→ 𝔻 [ F .func* A , G .func* B ]
→ 𝔻 [ func* F A , func* G B ]
:func→: ((θ , θNat) , f) = result
where
θA : 𝔻 [ F .func* A , G .func* A ]
θA : 𝔻 [ func* F A , func* G A ]
θA = θ A
θB : 𝔻 [ F .func* B , G .func* B ]
θB : 𝔻 [ func* F B , func* G B ]
θB = θ B
F→f : 𝔻 [ F .func* A , F .func* B ]
F→f = F .func→ f
G→f : 𝔻 [ G .func* A , G .func* B ]
G→f = G .func→ f
l : 𝔻 [ F .func* A , G .func* B ]
F→f : 𝔻 [ func* F A , func* F B ]
F→f = func→ F f
G→f : 𝔻 [ func* G A , func* G B ]
G→f = func→ G f
l : 𝔻 [ func* F A , func* G B ]
l = 𝔻 [ θB ∘ F→f ]
r : 𝔻 [ F .func* A , G .func* B ]
r : 𝔻 [ func* F A , func* G B ]
r = 𝔻 [ G→f ∘ θA ]
-- There are two choices at this point,
-- but I suppose the whole point is that
-- by `θNat f` we have `l ≡ r`
-- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
-- lem = θNat f
result : 𝔻 [ F .func* A , G .func* B ]
result : 𝔻 [ func* F A , func* G B ]
result = l
_×p_ = product
_×p_ = product unprovable
module _ {c : Functor ℂ 𝔻 × Object ℂ} where
private
@ -281,21 +230,21 @@ module _ (ℓ : Level) where
-- NaturalTransformation F G × ℂ .Arrow A B
-- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
-- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity)
-- where
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
-- Unfortunately the equational version has some ambigous arguments.
:ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {o = proj₂ c}) ≡ 𝟙 𝔻
:ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
:ident: = begin
:func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
:func→: {c} {c} (identityNat F , 𝟙 ℂ) ≡⟨⟩
𝔻 [ identityTrans F C ∘ F .func→ (𝟙 ℂ)] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ F .func→ (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.ident ⟩
F .func→ (𝟙 ℂ) ≡⟨ F.ident ⟩
𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩
func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩
𝟙 𝔻 ∎
where
open module 𝔻 = IsCategory (𝔻 .isCategory)
open module F = IsFunctor (F .isFunctor)
open module 𝔻 = Category 𝔻
open module F = Functor F
module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where
F = F×A .proj₁
@ -330,48 +279,51 @@ module _ (ℓ : Level) where
ηθ = proj₁ ηθNT
ηθNat = proj₂ ηθNT
:distrib: :
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ]
≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ]
:distrib: = begin
𝔻 [ (ηθ C) ∘ F .func→ (ℂ [ g ∘ f ]) ]
:isDistributive: :
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ]
≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ]
:isDistributive: = begin
𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ]
≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
𝔻 [ H .func→ (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩
𝔻 [ 𝔻 [ H .func→ g ∘ H .func→ f ] ∘ (ηθ A) ]
≡⟨ sym assoc ⟩
𝔻 [ H .func→ g ∘ 𝔻 [ H .func→ f ∘ ηθ A ] ]
≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) assoc ⟩
𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ H .func→ f ∘ η A ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ η B ∘ G .func→ f ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (sym assoc) ⟩
𝔻 [ H .func→ g ∘ 𝔻 [ η B ∘ 𝔻 [ G .func→ f ∘ θ A ] ] ] ≡⟨ assoc ⟩
𝔻 [ 𝔻 [ H .func→ g ∘ η B ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G .func→ f ∘ θ A ] ]) (sym (ηNat g)) ⟩
𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ φ ]) (sym (θNat f)) ⟩
𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] ∎
𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ]
≡⟨ sym isAssociative ⟩
𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ]
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩
𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩
𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ]
≡⟨ isAssociative ⟩
𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩
𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩
𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎
where
open IsCategory (𝔻 .isCategory)
open module H = IsFunctor (H .isFunctor)
open Category 𝔻
module H = Functor H
:eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
:eval: = record
{ raw = record
{ func* = :func*:
; func→ = λ {dom} {cod} → :func→: {dom} {cod}
}
; isFunctor = record
{ ident = λ {o} → :ident: {o}
; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y}
{ isIdentity = λ {o} → :ident: {o}
; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y}
}
}
module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
open HasProducts (hasProducts {ℓ} {ℓ}) renaming (_|×|_ to parallelProduct)
open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct)
postulate
transpose : Functor 𝔸 :obj:
eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F
-- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
-- eq' : (Catℓ [ :eval: ∘
-- (record { product = product } HasProducts.|×| transpose)
@ -384,10 +336,11 @@ module _ (ℓ : Level) where
-- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
-- transpose , eq
:isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
:isExponential: = {!catTranspose!}
where
open HasProducts (hasProducts {ℓ} {ℓ}) using (_|×|_)
postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
-- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
-- :isExponential: = {!catTranspose!}
-- where
-- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_)
-- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F
-- :exponent: : Exponential (Cat ℓ ℓ) A B
@ -398,5 +351,5 @@ module _ (ℓ : Level) where
; isExponential = :isExponential:
}
hasExponentials : HasExponentials (Cat ℓ ℓ)
hasExponentials : HasExponentials Catℓ
hasExponentials = record { exponent = :exponent: }

14
src/Cat/Categories/Fam.agda
View file

@ -25,12 +25,12 @@ module _ (ℓa ℓb : Level) where
c ⟨ g ∘ f ⟩ = _∘_ {c = c} g f
module _ {A B C D : Obj'} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
assoc : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
assoc = Σ≡ refl refl
isAssociative : (D ⟨ h ∘ C ⟨ g ∘ f ⟩ ⟩) ≡ D ⟨ D ⟨ h ∘ g ⟩ ∘ f ⟩
isAssociative = Σ≡ refl refl
module _ {A B : Obj'} {f : Arr A B} where
ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
ident = (Σ≡ refl refl) , Σ≡ refl refl
isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
@ -44,9 +44,9 @@ module _ (ℓa ℓb : Level) where
instance
isCategory : IsCategory RawFam
isCategory = record
{ assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {D = D} {f} {g} {h}
; ident = λ {A} {B} {f} → ident {A} {B} {f = f}
; arrowIsSet = {!!}
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
; arrowsAreSets = {!!}
; univalent = {!!}
}

22
src/Cat/Categories/Free.agda
View file

@ -9,14 +9,6 @@ open import Cat.Category
open IsCategory
-- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
-- emptyPath : {a : A} → Path a a
-- concatenate : {a b c : A} → Path a b → Path b c → Path a b
-- import Data.List
-- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
-- P = {!Data.List.List ?!}
-- Generalized paths:
data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
empty : {a : A} → Path R a a
cons : {a b c : A} → R b c → Path R a b → Path R a c
@ -34,16 +26,16 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open Category ℂ
private
p-assoc : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D}
p-isAssociative : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D}
→ p ++ (q ++ r) ≡ (p ++ q) ++ r
p-assoc {r = r} {q} {empty} = refl
p-assoc {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
p-isAssociative {r = r} {q} {empty} = refl
p-isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin
cons x p ++ (q ++ r) ≡⟨ cong (cons x) lem ⟩
cons x ((p ++ q) ++ r) ≡⟨⟩
(cons x p ++ q) ++ r ∎
where
lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r)
lem = p-assoc {r = r} {q} {p}
lem = p-isAssociative {r = r} {q} {p}
ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p
ident-r {p = empty} = refl
@ -65,8 +57,8 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
}
RawIsCategoryFree : IsCategory RawFree
RawIsCategoryFree = record
{ assoc = λ { {f = f} {g} {h} → p-assoc {r = f} {g} {h}}
; ident = ident-r , ident-l
; arrowIsSet = {!!}
{ isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}}
; isIdentity = ident-r , ident-l
; arrowsAreSets = {!!}
; univalent = {!!}
}

40
src/Cat/Categories/Fun.agda
View file

@ -38,9 +38,6 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
-- naturalIsProp : ∀ θ → isProp (Natural θ)
-- naturalIsProp θ x y = {!funExt!}
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
NaturalTransformation = Σ Transformation Natural
@ -63,8 +60,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
@ -87,11 +84,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
𝔻 [ (θ ∘nt η) B ∘ F.func→ f ] ≡⟨⟩
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym assoc ⟩
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ assoc ⟩
𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩
𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩
𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎
where
@ -100,19 +97,17 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
NatComp = _:⊕:_
private
module _ {F G : Functor ℂ 𝔻} where
module 𝔻 = Category 𝔻
module _ {F G : Functor ℂ 𝔻} where
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j
IsSet' : {ℓ : Level} (A : Set ℓ) → Set ℓ
IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C) (λ l → q l C) i j
naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
naturalTransformationIsSets : isSet (NaturalTransformation F G)
naturalTransformationIsSets = sigPresSet transformationIsSet
@ -135,24 +130,23 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
_g⊕f_ = _:⊕:_ {A} {B} {C}
_h⊕g_ = _:⊕:_ {B} {C} {D}
:assoc: : L ≡ R
:assoc: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x → assoc))
:isAssociative: : L ≡ R
:isAssociative: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x → isAssociative))
where
open Category 𝔻
module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
private
module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
allNatural = naturalIsProp {F = A} {B}
f' = proj₁ f
module 𝔻Data = Category 𝔻
eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
eq-r C = begin
𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
𝔻 [ f' C ∘ 𝔻Data.𝟙 ] ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.isIdentity ⟩
f' C ∎
eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
eq-l C = proj₂ (𝔻.ident {A} {B})
eq-l C = proj₂ 𝔻.isIdentity
ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
ident-r = lemSig allNatural _ _ (funExt eq-r)
ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
@ -174,9 +168,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
instance
:isCategory: : IsCategory RawFun
:isCategory: = record
{ assoc = λ {A B C D} → :assoc: {A} {B} {C} {D}
; ident = λ {A B} → :ident: {A} {B}
; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
{ isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
; isIdentity = λ {A B} → :ident: {A} {B}
; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
; univalent = {!!}
}

12
src/Cat/Categories/Rel.agda
View file

@ -149,10 +149,10 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
equi = fwd Cubical.FromStdLib., isequiv
-- assocc : Q + (R + S) ≡ (Q + R) + S
is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
-- isAssociativec : Q + (R + S) ≡ (Q + R) + S
is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
is-assoc = equivToPath equi
is-isAssociative = equivToPath equi
RawRel : RawCategory (lsuc lzero) (lsuc lzero)
RawRel = record
@ -164,8 +164,8 @@ RawRel = record
RawIsCategoryRel : IsCategory RawRel
RawIsCategoryRel = record
{ assoc = funExt is-assoc
; ident = funExt ident-l , funExt ident-r
; arrowIsSet = {!!}
{ isAssociative = funExt is-isAssociative
; isIdentity = funExt ident-l , funExt ident-r
; arrowsAreSets = {!!}
; univalent = {!!}
}

20
src/Cat/Categories/Sets.agda
View file

@ -25,10 +25,10 @@ module _ (ℓ : Level) where
_∘_ SetsRaw = Function._∘′_
SetsIsCategory : IsCategory SetsRaw
assoc SetsIsCategory = refl
proj₁ (ident SetsIsCategory) = funExt λ _ → refl
proj₂ (ident SetsIsCategory) = funExt λ _ → refl
arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
isAssociative SetsIsCategory = refl
proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s
univalent SetsIsCategory = {!!}
𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
@ -94,12 +94,12 @@ module _ {ℓa ℓb : Level} where
representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
representable {ℂ = ℂ} A = record
{ raw = record
{ func* = λ B → ℂ [ A , B ] , arrowIsSet
{ func* = λ B → ℂ [ A , B ] , arrowsAreSets
; func→ = ℂ [_∘_]
}
; isFunctor = record
{ ident = funExt λ _ → proj₂ ident
; distrib = funExt λ x → sym assoc
{ isIdentity = funExt λ _ → proj₂ isIdentity
; isDistributive = funExt λ x → sym isAssociative
}
}
where
@ -109,12 +109,12 @@ module _ {ℓa ℓb : Level} where
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
{ raw = record
{ func* = λ A → ℂ [ A , B ] , arrowIsSet
{ func* = λ A → ℂ [ A , B ] , arrowsAreSets
; func→ = λ f g → ℂ [ g ∘ f ]
}
; isFunctor = record
{ ident = funExt λ x → proj₁ ident
; distrib = funExt λ x → assoc
{ isIdentity = funExt λ x → proj₁ isIdentity
; isDistributive = funExt λ x → isAssociative
}
}
where

74
src/Cat/Category.agda
View file

@ -49,6 +49,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
IsIdentity id = {A B : Object} {f : Arrow A B}
→ f ∘ id ≡ f × id ∘ f ≡ f
ArrowsAreSets : Set (ℓa ⊔ ℓb)
ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B)
IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
@ -80,9 +83,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
-- Univalence is indexed by a raw category as well as an identity proof.
module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
open RawCategory ℂ
module _ (ident : IsIdentity 𝟙) where
module _ (isIdentity : IsIdentity 𝟙) where
idIso : (A : Object) → A ≅ A
idIso A = 𝟙 , (𝟙 , ident)
idIso A = 𝟙 , (𝟙 , isIdentity)
-- Lemma 9.1.4 in [HoTT]
id-to-iso : (A B : Object) → A ≡ B → A ≅ B
@ -98,10 +101,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
open RawCategory ℂ
open Univalence ℂ public
field
assoc : IsAssociative
ident : IsIdentity 𝟙
arrowIsSet : ∀ {A B : Object} → isSet (Arrow A B)
univalent : Univalent ident
isAssociative : IsAssociative
isIdentity : IsIdentity 𝟙
arrowsAreSets : ArrowsAreSets
univalent : Univalent isIdentity
-- `IsCategory` is a mere proposition.
module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
@ -112,12 +115,12 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
open import Cubical.NType.Properties
propIsAssociative : isProp IsAssociative
propIsAssociative x y i = arrowIsSet _ _ x y i
propIsAssociative x y i = arrowsAreSets _ _ x y i
propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
propIsIdentity a b i
= arrowIsSet _ _ (fst a) (fst b) i
, arrowIsSet _ _ (snd a) (snd b) i
= arrowsAreSets _ _ (fst a) (fst b) i
, arrowsAreSets _ _ (snd a) (snd b) i
propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
propArrowIsSet a b i = isSetIsProp a b i
@ -126,9 +129,9 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
propIsInverseOf x y = λ i →
let
h : fst x ≡ fst y
h = arrowIsSet _ _ (fst x) (fst y)
h = arrowsAreSets _ _ (fst x) (fst y)
hh : snd x ≡ snd y
hh = arrowIsSet _ _ (snd x) (snd y)
hh = arrowsAreSets _ _ (snd x) (snd y)
in h i , hh i
module _ {A B : Object} {f : Arrow A B} where
@ -139,14 +142,14 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
open Cubical.NType.Properties
geq : g ≡ g'
geq = begin
g ≡⟨ sym (fst ident) ⟩
g ≡⟨ sym (fst isIdentity) ⟩
g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
g ∘ (f ∘ g') ≡⟨ assoc ⟩
g ∘ (f ∘ g') ≡⟨ isAssociative ⟩
(g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
𝟙 ∘ g' ≡⟨ snd ident ⟩
𝟙 ∘ g' ≡⟨ snd isIdentity ⟩
g' ∎
propUnivalent : isProp (Univalent ident)
propUnivalent : isProp (Univalent isIdentity)
propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
private
@ -159,23 +162,28 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
-- projections of `IsCategory` - I've arbitrarily chosed to use this
-- result from `x : IsCategory C`. I don't know which (if any) possibly
-- adverse effects this may have.
ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
ident = propIsIdentity x X.ident Y.ident
isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
done : x ≡ y
U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ] → (b : Univalent a) → Set _
U eqwal bbb = (λ i → Univalent (eqwal i)) [ X.univalent ≡ bbb ]
U : ∀ {a : IsIdentity 𝟙}
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
→ (b : Univalent a)
→ Set _
U eqwal bbb =
(λ i → Univalent (eqwal i))
[ X.univalent ≡ bbb ]
P : (y : IsIdentity 𝟙)
→ (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
P y eq = ∀ (b' : Univalent y) → U eq b'
helper : ∀ (b' : Univalent X.ident)
→ (λ _ → Univalent X.ident) [ X.univalent ≡ b' ]
helper : ∀ (b' : Univalent X.isIdentity)
→ (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
helper univ = propUnivalent x X.univalent univ
foo = pathJ P helper Y.ident ident
eqUni : U ident Y.univalent
foo = pathJ P helper Y.isIdentity isIdentity
eqUni : U isIdentity Y.univalent
eqUni = foo Y.univalent
IC.assoc (done i) = propIsAssociative x X.assoc Y.assoc i
IC.ident (done i) = ident i
IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
IC.isIdentity (done i) = isIdentity i
IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i
IC.univalent (done i) = eqUni i
propIsCategory : isProp (IsCategory C)
@ -208,9 +216,9 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
RawCategory._∘_ OpRaw = Function.flip _∘_
OpIsCategory : IsCategory OpRaw
IsCategory.assoc OpIsCategory = sym assoc
IsCategory.ident OpIsCategory = swap ident
IsCategory.arrowIsSet OpIsCategory = arrowIsSet
IsCategory.isAssociative OpIsCategory = sym isAssociative
IsCategory.isIdentity OpIsCategory = swap isIdentity
IsCategory.arrowsAreSets OpIsCategory = arrowsAreSets
IsCategory.univalent OpIsCategory = {!!}
Opposite : Category ℓa ℓb
@ -234,9 +242,9 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
open IsCategory
module IsCat = IsCategory (ℂ .isCategory)
rawIsCat : (i : I) → IsCategory (rawOp i)
assoc (rawIsCat i) = IsCat.assoc
ident (rawIsCat i) = IsCat.ident
arrowIsSet (rawIsCat i) = IsCat.arrowIsSet
isAssociative (rawIsCat i) = IsCat.isAssociative
isIdentity (rawIsCat i) = IsCat.isIdentity
arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets
univalent (rawIsCat i) = IsCat.univalent
Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ

1
src/Cat/Category/Exponential.agda
View file

@ -35,5 +35,6 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
transpose A f = proj₁ (isExponential A f)
record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
open Exponential public
field
exponent : (A B : Object ℂ) → Exponential ℂ A B

52
src/Cat/Category/Functor.agda
View file

@ -7,7 +7,7 @@ open import Function
open import Cat.Category
open Category hiding (_∘_ ; raw)
open Category hiding (_∘_ ; raw ; IsIdentity)
module _ {ℓc ℓc' ℓd ℓd'}
(ℂ : Category ℓc ℓc')
@ -23,42 +23,40 @@ module _ {ℓc ℓc' ℓd ℓd'}
func* : Object ℂ → Object 𝔻
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
record IsFunctor (F : RawFunctor) : 𝓤 where
open RawFunctor F
field
ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c}
distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
IsIdentity : Set _
IsIdentity = {A : Object ℂ} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A}
IsDistributive : Set _
IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
→ func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
record IsFunctor (F : RawFunctor) : 𝓤 where
open RawFunctor F public
field
isIdentity : IsIdentity
isDistributive : IsDistributive
record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
field
raw : RawFunctor
{{isFunctor}} : IsFunctor raw
private
module R = RawFunctor raw
open IsFunctor isFunctor public
func* : Object ℂ → Object 𝔻
func* = R.func*
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
func→ = R.func→
open IsFunctor
open Functor
module _
{ℓa ℓb : Level}
{ℂ 𝔻 : Category ℓa ℓb}
{F : RawFunctor ℂ 𝔻}
(F : RawFunctor ℂ 𝔻)
where
private
module 𝔻 = IsCategory (isCategory 𝔻)
propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record
{ ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
{ isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i
; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i
}
where
module isF0 = IsFunctor isF0
@ -77,7 +75,7 @@ module _
IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i)
IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻}
(\ F → propIsFunctor {F = F}) (\ i → F i)
(\ F → propIsFunctor F) (\ i → F i)
where
open import Cubical.NType.Properties using (lemPropF)
@ -108,8 +106,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
dist = begin
(F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩
F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (G .isFunctor .distrib)⟩
F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ F .isFunctor .distrib ⟩
F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (isDistributive G) ⟩
F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ isDistributive F ⟩
C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
_∘fr_ : RawFunctor A C
@ -118,12 +116,12 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
instance
isFunctor' : IsFunctor A C _∘fr_
isFunctor' = record
{ ident = begin
{ isIdentity = begin
(F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (G .isFunctor .ident)⟩
F→ (𝟙 B) ≡⟨ F .isFunctor .ident ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩
F→ (𝟙 B) ≡⟨ isIdentity F ⟩
𝟙 C ∎
; distrib = dist
; isDistributive = dist
}
_∘f_ : Functor A C
@ -137,7 +135,7 @@ identity = record
; func→ = λ x → x
}
; isFunctor = record
{ ident = refl
; distrib = refl
{ isIdentity = refl
; isDistributive = refl
}
}

133
src/Cat/Category/Properties.agda
View file

@ -17,106 +17,77 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object
iso-is-epi : Isomorphism f → Epimorphism {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym (proj₁ ident) ⟩
g₀ ≡⟨ sym (proj₁ isIdentity) ⟩
g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
g₀ ∘ (f ∘ f-) ≡⟨ assoc ⟩
g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩
(g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym assoc ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩
g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩
g₁ ∘ 𝟙 ≡⟨ proj₁ ident ⟩
g₁ ∘ 𝟙 ≡⟨ proj₁ isIdentity ⟩
g₁ ∎
iso-is-mono : Isomorphism f → Monomorphism {X = X} f
iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
begin
g₀ ≡⟨ sym (proj₂ ident) ⟩
g₀ ≡⟨ sym (proj₂ isIdentity) ⟩
𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym assoc ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
f- ∘ (f ∘ g₁) ≡⟨ assoc ⟩
f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
(f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
𝟙 ∘ g₁ ≡⟨ proj₂ ident ⟩
𝟙 ∘ g₁ ≡⟨ proj₂ isIdentity ⟩
g₁ ∎
iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso
{-
epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f)
epi-mono-is-not-iso f =
let k = f {!!} {!!} {!!} {!!}
in {!!}
-}
-- TODO: We want to avoid defining the yoneda embedding going through the
-- category of categories (since it doesn't exist).
open import Cat.Categories.Cat using (RawCat)
open import Cat.Category
open Category
open Functor
module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where
open import Cat.Categories.Fun
open import Cat.Categories.Sets
module Cat = Cat.Categories.Cat
open import Cat.Category.Exponential
open Functor
𝓢 = Sets ℓ
private
Catℓ : Category _ _
Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
prshf = presheaf {ℂ = ℂ}
module ℂ = Category ℂ
-- module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
-- {isSObj : isSet (ℂ .Object)}
-- {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where
-- -- open import Cat.Categories.Cat using (Cat)
-- open import Cat.Categories.Fun
-- open import Cat.Categories.Sets
-- -- module Cat = Cat.Categories.Cat
-- open import Cat.Category.Exponential
-- private
-- Catℓ = Cat ℓ ℓ
-- prshf = presheaf {ℂ = ℂ}
-- module ℂ = IsCategory (ℂ .isCategory)
_⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ
A ⇑ B = (exponent A B) .obj
where
open HasExponentials (Cat.hasExponentials ℓ unprovable)
-- -- Exp : Set (lsuc (lsuc ℓ))
-- -- Exp = Exponential (Cat (lsuc ℓ) ℓ)
-- -- Sets (Opposite ℂ)
module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
:func→: : NaturalTransformation (prshf A) (prshf B)
:func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
-- _⇑_ : (A B : Catℓ .Object) → Catℓ .Object
-- A ⇑ B = (exponent A B) .obj
-- where
-- open HasExponentials (Cat.hasExponentials ℓ)
module _ {c : Category.Object ℂ} where
eqTrans : (λ _ → Transformation (prshf c) (prshf c))
[ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
-- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
-- :func→: : NaturalTransformation (prshf A) (prshf B)
-- :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.assoc
open import Cubical.NType.Properties
open import Cat.Categories.Fun
:ident: : :func→: (ℂ.𝟙 {c}) ≡ Category.𝟙 Fun {A = prshf c}
:ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
where
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
-- module _ {c : ℂ .Object} where
-- eqTrans : (λ _ → Transformation (prshf c) (prshf c))
-- [ (λ _ x → ℂ [ ℂ .𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
-- eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
-- eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
-- [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
-- eqNat = λ i {A} {B} f →
-- let
-- open IsCategory (Sets .isCategory)
-- lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡
-- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
-- lemm = {!!}
-- lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ])
-- [ Sets [ eqTrans i B ∘ prshf c .func→ f ]
-- ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ]
-- lem
-- = isz2 _ _ lemm _ i
-- -- (Sets [ eqTrans i B ∘ prshf c .func→ f ])
-- -- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
-- -- lemm
-- -- _ i
-- in
-- lem
-- -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
-- -- let
-- -- k : ℂ [ {!!} , {!!} ]
-- -- k = ℂ[A,c]
-- -- in {!ℂ [ ? ∘ ? ]!}
-- :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
-- :ident: = Σ≡ eqTrans eqNat
-- yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
-- yoneda = record
-- { func* = prshf
-- ; func→ = :func→:
-- ; isFunctor = record
-- { ident = :ident:
-- ; distrib = {!!}
-- }
-- }
yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢})
yoneda = record
{ raw = record
{ func* = prshf
; func→ = :func→:
}
; isFunctor = record
{ isIdentity = :ident:
; isDistributive = {!!}
}
}

25
src/Cat/Equality.agda
View file

@ -20,28 +20,3 @@ module Equality where
Σ≡ : a ≡ b
proj₁ (Σ≡ i) = proj₁≡ i
proj₂ (Σ≡ i) = proj₂≡ i
-- Remark 2.7.1: This theorem:
--
-- (x , u) ≡ (x , v) → u ≡ v
--
-- does *not* hold! We can only conclude that there *exists* `p : x ≡ x`
-- such that
--
-- p* u ≡ v
-- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B)
-- thm sA sB (x , y) (x' , y') p q = res
-- where
-- x≡x'0 : x ≡ x'
-- x≡x'0 = λ i → proj₁ (p i)
-- x≡x'1 : x ≡ x'
-- x≡x'1 = λ i → proj₁ (q i)
-- someP : x ≡ x'
-- someP = {!!}
-- tricky : {!y!} ≡ y'
-- tricky = {!!}
-- -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ]
-- res' : ({!!} , {!!}) ≡ ({!!} , {!!})
-- res' = {!!}
-- res : p ≡ q
-- res i = {!res'!}