Merge branch 'dev'

This commit is contained in:
Frederik Hanghøj Iversen 2018-01-21 19:24:13 +01:00
commit be4949180b
12 changed files with 380 additions and 220 deletions

2
Makefile Normal file
View file

@ -0,0 +1,2 @@
build: src/**.agda
agda src/Cat.agda

12
src/Cat.agda Normal file
View file

@ -0,0 +1,12 @@
module Cat where
import Cat.Categories.Sets
import Cat.Categories.Cat
import Cat.Categories.Rel
import Cat.Category.Pathy
import Cat.Category.Bij
import Cat.Category.Free
import Cat.Category.Properties
import Cat.Category
import Cat.Cubical
import Cat.Functor

View file

@ -1,55 +1,174 @@
{-# OPTIONS --cubical #-}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Category.Categories.Cat where
module Cat.Categories.Cat where
open import Agda.Primitive
open import Cubical
open import Function
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Category
open import Cat.Category
open import Cat.Functor
-- Tip from Andrea:
-- Use co-patterns - they help with showing more understandable types in goals.
lift-eq : {} {A B : Set } {a a' : A} {b b' : B} a a' b b' (a , b) (a' , b')
fst (lift-eq a b i) = a i
snd (lift-eq a b i) = b i
eqpair : {a b} {A : Set a} {B : Set b} {a a' : A} {b b' : B}
a a' b b' (a , b) (a' , b')
eqpair eqa eqb i = eqa i , eqb i
open Functor
open Category
module _ { ' : Level} {A B : Category '} where
lift-eq-functors : {f g : Functor A B}
(eq* : f .func* g .func*)
(eq→ : PathP (λ i {x y} A .Arrow x y B .Arrow (eq* i x) (eq* i y))
(f .func→) (g .func→))
-- → (eq→ : Functor.func→ f ≡ {!!}) -- Functor.func→ g)
-- Use PathP
-- directly to show heterogeneous equalities by using previous
-- equalities (i.e. continuous paths) to create new continuous paths.
(eqI : PathP (λ i {c : A .Object} eq→ i (A .𝟙 {c}) B .𝟙 {eq* i c})
(ident f) (ident g))
(eqD : PathP (λ i { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
eq→ i (A ._⊕_ a' a) B ._⊕_ (eq→ i a') (eq→ i a))
(distrib f) (distrib g))
f g
lift-eq-functors eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i }
-- The category of categories
module _ { ' : Level} where
private
_⊛_ = functor-comp
module _ {A B C D : Category {} {'}} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
assc : h (g f) (h g) f
assc = {!!}
module _ {A B C D : Category '} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
eq* : func* (h ∘f (g ∘f f)) func* ((h ∘f g) ∘f f)
eq* = refl
eq→ : PathP
(λ i {x y : A .Object} A .Arrow x y D .Arrow (eq* i x) (eq* i y))
(func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f))
eq→ = refl
id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D
id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D
postulate eqI : PathP
(λ i {c : A .Object} eq→ i (A .𝟙 {c}) D .𝟙 {eq* i c})
(ident ((h ∘f (g ∘f f))))
(ident ((h ∘f g) ∘f f))
postulate eqD : PathP (λ i { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
eq→ i (A ._⊕_ a' a) D ._⊕_ (eq→ i a') (eq→ i a))
(distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f))
-- eqD = {!!}
module _ {A B : Category {} {'}} where
lift-eq : (f g : Functor A B)
(eq* : Functor.func* f Functor.func* g)
-- TODO: Must transport here using the equality from above.
-- Reason:
-- func→ : Arrow A dom cod → Arrow B (func* dom) (func* cod)
-- func→₁ : Arrow A dom cod → Arrow B (func*₁ dom) (func*₁ cod)
-- In other words, func→ and func→₁ does not have the same type.
-- → Functor.func→ f ≡ Functor.func→ g
-- → Functor.ident f ≡ Functor.ident g
-- → Functor.distrib f ≡ Functor.distrib g
f g
lift-eq
(functor func* func→ idnt distrib)
(functor func*₁ func→₁ idnt₁ distrib₁)
eq-func* = {!!}
assc : h ∘f (g ∘f f) (h ∘f g) ∘f f
assc = lift-eq-functors eq* eq→ eqI eqD
module _ {A B : Category {} {'}} {f : Functor A B} where
idHere = identity {} {'} {A}
lem : (Functor.func* f) (Functor.func* idHere) Functor.func* f
module _ {A B : Category '} {f : Functor A B} where
lem : (func* f) (func* (identity {C = A})) func* f
lem = refl
ident-r : f identity f
ident-r = lift-eq (f identity) f refl
ident-l : identity f f
ident-l = {!!}
-- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
lemmm : PathP
(λ i
{x y : Object A} Arrow A x y Arrow B (func* f x) (func* f y))
(func→ (f ∘f identity)) (func→ f)
lemmm = refl
postulate lemz : PathP (λ i {c : A .Object} PathP (λ _ Arrow B (func* f c) (func* f c)) (func→ f (A .𝟙)) (B .𝟙))
(ident (f ∘f identity)) (ident f)
-- lemz = {!!}
postulate ident-r : f ∘f identity f
-- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!}
postulate ident-l : identity ∘f f f
-- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
CatCat : Category {lsuc ( ')} { '}
CatCat =
Cat : Category (lsuc ( ')) ( ')
Cat =
record
{ Object = Category {} {'}
{ Object = Category '
; Arrow = Functor
; 𝟙 = identity
; _⊕_ = functor-comp
; assoc = {!!}
; ident = ident-r , ident-l
; _⊕_ = _∘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
}
}
module _ { : Level} (C D : Category ) where
private
:Object: = C .Object × D .Object
:Arrow: : :Object: :Object: Set
:Arrow: (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
:𝟙: : {o : :Object:} :Arrow: o o
:𝟙: = C .𝟙 , D .𝟙
_:⊕:_ :
{a b c : :Object:}
:Arrow: b c
:Arrow: a b
:Arrow: a c
_:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) (C ._⊕_) bc∈C ab∈C , D ._⊕_ bc∈D ab∈D}
instance
:isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
:isCategory: = record
{ assoc = eqpair C.assoc D.assoc
; ident
= eqpair (fst C.ident) (fst D.ident)
, eqpair (snd C.ident) (snd D.ident)
}
where
open module C = IsCategory (C .isCategory)
open module D = IsCategory (D .isCategory)
:product: : Category
:product: = record
{ Object = :Object:
; Arrow = :Arrow:
; 𝟙 = :𝟙:
; _⊕_ = _:⊕:_
}
proj₁ : Arrow Cat :product: C
proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
proj₂ : Arrow Cat :product: D
proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
module _ {X : Object (Cat {} {})} (x₁ : Arrow Cat X C) (x₂ : Arrow Cat X D) where
open Functor
-- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D)
-- ident' {c = c} = lift-eq (ident x₁) (ident x₂)
x : Functor X :product:
x = record
{ func* = λ x (func* x₁) x , (func* x₂) x
; func→ = λ x func→ x₁ x , func→ x₂ x
; ident = lift-eq (ident x₁) (ident x₂)
; distrib = lift-eq (distrib x₁) (distrib x₂)
}
-- Need to "lift equality of functors"
-- If I want to do this like I do it for pairs it's gonna be a pain.
postulate isUniqL : (Cat proj₁) x x₁
-- isUniqL = lift-eq-functors refl refl {!!} {!!}
postulate isUniqR : (Cat proj₂) x x₂
-- isUniqR = lift-eq-functors refl refl {!!} {!!}
isUniq : (Cat proj₁) x x₁ × (Cat proj₂) x x₂
isUniq = isUniqL , isUniqR
uniq : ∃![ x ] ((Cat proj₁) x x₁ × (Cat proj₂) x x₂)
uniq = x , isUniq
instance
isProduct : IsProduct Cat proj₁ proj₂
isProduct = uniq
product : Product { = Cat} C D
product = record
{ obj = :product:
; proj₁ = proj₁
; proj₂ = proj₂
}

View file

@ -154,12 +154,11 @@ 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))
is-assoc = equivToPath equi
Rel : Category
Rel : Category (lsuc lzero) (lsuc lzero)
Rel = record
{ Object = Set
; Arrow = λ S R Subset (S × R)
; 𝟙 = λ {S} Diag S
; _⊕_ = λ {A B C} S R λ {( a , c ) Σ[ b B ] ( (a , b) R × (b , c) S )}
; assoc = funExt is-assoc
; ident = funExt ident-l , funExt ident-r
; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
}

View file

@ -9,44 +9,45 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Cat.Category
open import Cat.Functor
open Category
-- Sets are built-in to Agda. The set of all small sets is called Set.
Fun : { : Level} ( T U : Set ) Set
Fun T U = T U
Sets : { : Level} Category {lsuc } {}
Sets : { : Level} Category (lsuc )
Sets {} = record
{ Object = Set
; Arrow = λ T U Fun {} T U
; 𝟙 = λ x x
; _⊕_ = λ g f x g ( f x )
; assoc = refl
; ident = funExt (λ x refl) , funExt (λ x refl)
; Arrow = λ T U T U
; 𝟙 = id
; _⊕_ = _∘_
; isCategory = record { assoc = refl ; ident = funExt (λ _ refl) , funExt (λ _ refl) }
}
where
open import Function
Representable : { ' : Level} ( : Category {} {'}) Set ( lsuc ')
-- Covariant Presheaf
Representable : { ' : Level} ( : Category ') Set ( lsuc ')
Representable {' = '} = Functor (Sets {'})
representable : { ' : Level} { : Category {} {'}} Category.Object Representable
-- The "co-yoneda" embedding.
representable : { '} { : Category '} Category.Object Representable
representable { = } A = record
{ func* = λ B .Arrow A B
; func→ = λ f g f .⊕ g
; ident = funExt λ _ snd .ident
; distrib = funExt λ x sym .assoc
{ func* = λ B .Arrow A B
; func→ = ._⊕_
; ident = funExt λ _ snd ident
; distrib = funExt λ x sym assoc
}
where
open module = Category
open IsCategory ( .isCategory)
Presheaf : { ' : Level} ( : Category {} {'}) Set ( lsuc ')
-- Contravariant Presheaf
Presheaf : { '} ( : Category ') Set ( lsuc ')
Presheaf {' = '} = Functor (Opposite ) (Sets {'})
presheaf : { ' : Level} { : Category {} {'}} Category.Object (Opposite ) Presheaf
-- Alternate name: `yoneda`
presheaf : { ' : Level} { : Category '} Category.Object (Opposite ) Presheaf
presheaf { = } B = record
{ func* = λ A .Arrow A B
; func→ = λ f g g .⊕ f
; ident = funExt λ x fst .ident
; distrib = funExt λ x .assoc
{ func* = λ A .Arrow A B
; func→ = λ f g ._⊕_ g f
; ident = funExt λ x fst ident
; distrib = funExt λ x assoc
}
where
open module = Category
open IsCategory ( .isCategory)

View file

@ -4,139 +4,119 @@ module Cat.Category where
open import Agda.Primitive
open import Data.Unit.Base
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Data.Product renaming
( proj₁ to fst
; proj₂ to snd
; ∃! to ∃!≈
)
open import Data.Empty
open import Function
open import Cubical
postulate undefined : { : Level} {A : Set } A
∃! : {a b} {A : Set a}
(A Set b) Set (a b)
∃! = ∃!≈ _≡_
record Category { '} : Set (lsuc (' )) where
constructor category
∃!-syntax : {a b} {A : Set a} (A Set b) Set (a b)
∃!-syntax =
syntax ∃!-syntax (λ x B) = ∃![ x ] B
record IsCategory { ' : Level}
(Object : Set )
(Arrow : Object Object Set ')
(𝟙 : {o : Object} Arrow o o)
(_⊕_ : { a b c : Object } Arrow b c Arrow a b Arrow a c)
: Set (lsuc (' )) where
field
assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
h (g f) (h g) f
ident : {A B : Object} {f : Arrow A B}
f 𝟙 f × 𝟙 f f
-- open IsCategory public
record Category ( ' : Level) : Set (lsuc (' )) where
-- adding no-eta-equality can speed up type-checking.
no-eta-equality
field
Object : Set
Arrow : Object Object Set '
𝟙 : {o : Object} Arrow o o
_⊕_ : { a b c : Object } Arrow b c Arrow a b Arrow a c
assoc : { A B C D : Object } { f : Arrow A B } { g : Arrow B C } { h : Arrow C D }
h (g f) (h g) f
ident : { A B : Object } { f : Arrow A B }
f 𝟙 f × 𝟙 f f
{{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
infixl 45 _⊕_
domain : { a b : Object } Arrow a b Object
domain {a = a} _ = a
codomain : { a b : Object } Arrow a b Object
codomain {b = b} _ = b
open Category public
open Category
module _ { ' : Level} { : Category {} {'}} { A B : Object } where
private
open module = Category
_+_ = ._⊕_
module _ { ' : Level} { : Category '} where
module _ { A B : .Object } where
Isomorphism : (f : .Arrow A B) Set '
Isomorphism f = Σ[ g .Arrow B A ] ._⊕_ g f .𝟙 × ._⊕_ f g .𝟙
Isomorphism : (f : .Arrow A B) Set '
Isomorphism f = Σ[ g .Arrow B A ] g + f .𝟙 × f + g .𝟙
Epimorphism : {X : .Object } (f : .Arrow A B) Set '
Epimorphism {X} f = ( g₀ g₁ : .Arrow B X ) ._⊕_ g₀ f ._⊕_ g₁ f g₀ g₁
Epimorphism : {X : .Object } (f : .Arrow A B) Set '
Epimorphism {X} f = ( g₀ g₁ : .Arrow B X ) g₀ + f g₁ + f g₀ g₁
Monomorphism : {X : .Object} (f : .Arrow A B) Set '
Monomorphism {X} f = ( g₀ g₁ : .Arrow X A ) ._⊕_ f g₀ ._⊕_ f g₁ g₀ g₁
Monomorphism : {X : .Object} (f : .Arrow A B) Set '
Monomorphism {X} f = ( g₀ g₁ : .Arrow X A ) f + g₀ f + g₁ g₀ g₁
-- Isomorphism of objects
_≅_ : (A B : Object ) Set '
_≅_ A B = Σ[ f .Arrow A B ] (Isomorphism f)
iso-is-epi : {X} (f : .Arrow A B) Isomorphism f Epimorphism {X = X} f
-- Idea: Pre-compose with f- on both sides of the equality of eq to get
-- g₀ + f + f- ≡ g₁ + f + f-
-- which by left-inv reduces to the goal.
iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq =
trans (sym (fst .ident))
( trans (cong (_+_ g₀) (sym right-inv))
( trans .assoc
( trans (cong (λ x x + f-) eq)
( trans (sym .assoc)
( trans (cong (_+_ g₁) right-inv) (fst .ident))
)
)
)
)
module _ { ' : Level} ( : Category ') {A B obj : Object } where
IsProduct : (π₁ : Arrow obj A) (π₂ : Arrow obj B) Set ( ')
IsProduct π₁ π₂
= {X : .Object} (x₁ : .Arrow X A) (x₂ : .Arrow X B)
∃![ x ] ( ._⊕_ π₁ x x₁ × ._⊕_ π₂ x x₂)
iso-is-mono : {X} (f : .Arrow A B ) Isomorphism f Monomorphism {X = X} f
-- For the next goal we do something similar: Post-compose with f- and use
-- right-inv to get the goal.
iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq =
trans (sym (snd .ident))
( trans (cong (λ x x + g₀) (sym left-inv))
( trans (sym .assoc)
( trans (cong (_+_ f-) eq)
( trans .assoc
( trans (cong (λ x x + g₁) left-inv) (snd .ident)
)
)
)
)
)
-- Tip from Andrea; Consider this style for efficiency:
-- record IsProduct { ' : Level} ( : Category {} {'})
-- {A B obj : Object } (π₁ : Arrow obj A) (π₂ : Arrow obj B) : Set (') where
-- field
-- isProduct : ∀ {X : .Object} (x₁ : .Arrow X A) (x₂ : .Arrow X B)
-- → ∃![ x ] ( ._⊕_ π₁ x ≡ x₁ × . _⊕_ π₂ x ≡ x₂)
iso-is-epi-mono : {X} (f : .Arrow A B ) Isomorphism f Epimorphism {X = X} f × Monomorphism {X = X} f
iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso
record Product { ' : Level} { : Category '} (A B : .Object) : Set ( ') where
no-eta-equality
field
obj : .Object
proj₁ : .Arrow obj A
proj₂ : .Arrow obj B
{{isProduct}} : IsProduct proj₁ proj₂
{-
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 {!!}
-}
module _ { ' : Level} ( : Category ') where
Opposite : Category '
Opposite =
record
{ Object = .Object
; Arrow = flip ( .Arrow)
; 𝟙 = .𝟙
; _⊕_ = flip ( ._⊕_)
; isCategory = record { assoc = sym assoc ; ident = swap ident }
}
where
open IsCategory ( .isCategory)
-- Isomorphism of objects
_≅_ : { ' : Level } { : Category {} {'} } ( A B : Object ) Set '
_≅_ { = } A B = Σ[ f .Arrow A B ] (Isomorphism { = } f)
where
open module = Category
-- A consequence of no-eta-equality; `Opposite-is-involution` is no longer
-- definitional - i.e.; you must match on the fields:
--
-- Opposite-is-involution : ∀ { '} → {C : Category {} {'}} → Opposite (Opposite C) ≡ C
-- Object (Opposite-is-involution {C = C} i) = Object C
-- Arrow (Opposite-is-involution i) = {!!}
-- 𝟙 (Opposite-is-involution i) = {!!}
-- _⊕_ (Opposite-is-involution i) = {!!}
-- assoc (Opposite-is-involution i) = {!!}
-- ident (Opposite-is-involution i) = {!!}
Product : { : Level} ( C D : Category {} {} ) Category {} {}
Product C D =
record
{ Object = C.Object × D.Object
; Arrow = λ { (c , d) (c' , d')
let carr = C.Arrow c c'
darr = D.Arrow d d'
in carr × darr}
; 𝟙 = C.𝟙 , D.𝟙
; _⊕_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) bc∈C C.⊕ ab∈C , bc∈D D.⊕ ab∈D}
; assoc = eqpair C.assoc D.assoc
; ident =
let (Cl , Cr) = C.ident
(Dl , Dr) = D.ident
in eqpair Cl Dl , eqpair Cr Dr
}
where
open module C = Category C
open module D = Category D
-- Two pairs are equal if their components are equal.
eqpair : { : Level} { A : Set } { B : Set } { a a' : A } { b b' : B } a a' b b' (a , b) (a' , b')
eqpair {a = a} {b = b} eqa eqb = subst eqa (subst eqb (refl {x = (a , b)}))
Opposite : { '} Category {} {'} Category {} {'}
Opposite =
record
{ Object = .Object
; Arrow = λ A B .Arrow B A
; 𝟙 = .𝟙
; _⊕_ = λ g f f .⊕ g
; assoc = sym .assoc
; ident = swap .ident
}
where
open module = Category
Hom : { ' : Level} ( : Category {} {'}) (A B : Object ) Set '
Hom : { ' : Level} ( : Category ') (A B : Object ) Set '
Hom A B = Arrow A B
module _ { ' : Level} { : Category {} {'}} where
private
Obj = Object
Arr = Arrow
_+_ = _⊕_
HomFromArrow : (A : Obj) {B B' : Obj} (g : Arr B B')
module _ { ' : Level} { : Category '} where
HomFromArrow : (A : .Object) {B B' : .Object} (g : .Arrow B B')
Hom A B Hom A B'
HomFromArrow _A g = λ f g + f
HomFromArrow _A = _⊕_

View file

@ -1,6 +1,9 @@
{-# OPTIONS --cubical #-}
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Category.Bij where
open import Cubical.PathPrelude hiding ( Id )
open import Cubical.FromStdLib
module _ {A : Set} {a : A} {P : A Set} where
Q : A Set
@ -20,7 +23,7 @@ module _ {A : Set} {a : A} {P : A → Set} where
w x = {!!}
vw-bij : (a : P a) (w v) a a
vw-bij a = refl
vw-bij a = {!!}
-- tubij a with (t ∘ u) a
-- ... | q = {!!}

View file

@ -1,21 +1,20 @@
module Category.Free where
module Cat.Category.Free where
open import Agda.Primitive
open import Cubical.PathPrelude hiding (Path)
open import Data.Product
open import Category as C
open import Cat.Category as C
module _ { ' : Level} ( : Category {} {'}) where
module _ { ' : Level} ( : Category ') where
private
open module = Category
Obj = .Object
Path : ( a b : Obj ) Set
Path a b = undefined
postulate emptyPath : (o : Obj) Path o o
postulate concatenate : {a b c : Obj} Path b c Path a b Path a c
postulate
Path : ( a b : Obj ) Set '
emptyPath : (o : Obj) Path o o
concatenate : {a b c : Obj} Path b c Path a b Path a c
private
module _ {A B C D : Obj} {r : Path A B} {q : Path B C} {p : Path C D} where
@ -27,12 +26,11 @@ module _ { ' : Level} ( : Category {} {'}) where
ident-r : concatenate {A} {A} {B} p (emptyPath A) p
ident-l : concatenate {A} {B} {B} (emptyPath B) p p
Free : Category
Free : Category '
Free = record
{ Object = Obj
; Arrow = Path
; 𝟙 = λ {o} emptyPath o
; _⊕_ = λ {a b c} concatenate {a} {b} {c}
; assoc = p-assoc
; ident = ident-r , ident-l
; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
}

View file

@ -1,7 +1,8 @@
{-# OPTIONS --cubical #-}
module Category.Pathy where
module Cat.Category.Pathy where
open import Level
open import Cubical.PathPrelude
{-

View file

@ -2,22 +2,64 @@
module Cat.Category.Properties where
open import Agda.Primitive
open import Data.Product
open import Cubical.PathPrelude
open import Cat.Category
open import Cat.Functor
open import Cat.Categories.Sets
module _ { ' : Level} { : Category '} { A B : .Category.Object } {X : .Category.Object} (f : .Category.Arrow A B) where
open Category
open IsCategory (isCategory)
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₀ 𝟙 ≡⟨ cong (_⊕_ g₀) (sym right-inv)
g₀ (f f-) ≡⟨ assoc
(g₀ f) f- ≡⟨ cong (λ φ φ f-) eq
(g₁ f) f- ≡⟨ sym assoc
g₁ (f f-) ≡⟨ cong (_⊕_ g₁) right-inv
g₁ 𝟙 ≡⟨ proj₁ ident
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₀ ≡⟨ cong (λ φ φ g₀) (sym left-inv)
(f- f) g₀ ≡⟨ sym assoc
f- (f g₀) ≡⟨ cong (_⊕_ f-) eq
f- (f g₁) ≡⟨ assoc
(f- f) g₁ ≡⟨ cong (λ φ φ g₁) left-inv
𝟙 g₁ ≡⟨ proj₂ ident
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 {!!}
-}
module _ {a a' b b'} where
Exponential : Category {a} {a'} Category {b} {b'} Category {{!!}} {{!!}}
Exponential : Category a a' Category b b' Category {!!} {!!}
Exponential A B = record
{ Object = {!!}
; Arrow = {!!}
; 𝟙 = {!!}
; _⊕_ = {!!}
; assoc = {!!}
; ident = {!!}
; isCategory = {!!}
}
_⇑_ = Exponential
yoneda : { '} { : Category {} {'}} Functor (Sets (Opposite ))
yoneda : { '} { : Category '} Functor (Sets (Opposite ))
yoneda = {!!}

View file

@ -1,3 +1,4 @@
{-# OPTIONS --allow-unsolved-metas #-}
module Cat.Cubical where
open import Agda.Primitive
@ -9,8 +10,13 @@ open import Data.Empty
open import Cat.Category
-- See chapter 1 for a discussion on how presheaf categories are CwF's.
-- See section 6.8 in Huber's thesis for details on how to implement the
-- categorical version of CTT
module _ { ' : Level} (Ns : Set ) where
-- Σ is the "namespace"
-- Ns is the "namespace"
o = (lsuc lzero )
FiniteDecidableSubset : Set
@ -36,13 +42,12 @@ module _ { ' : Level} (Ns : Set ) where
Mor = Σ themap rules
-- The category of names and substitutions
: Category -- {o} {lsuc lzero ⊔ o}
: Category -- o (lsuc lzero ⊔ o)
= record
-- { Object = FiniteDecidableSubset
{ Object = Ns Bool
; Arrow = Mor
; 𝟙 = {!!}
; _⊕_ = {!!}
; assoc = {!!}
; ident = {!!}
; isCategory = ?
}

View file

@ -6,7 +6,7 @@ open import Function
open import Cat.Category
record Functor {c c' d d'} (C : Category {c} {c'}) (D : Category {d} {d'})
record Functor {c c' d d'} (C : Category c c') (D : Category d d')
: Set (c c' d d') where
private
open module C = Category C
@ -21,43 +21,41 @@ record Functor {c c' d d'} (C : Category {c} {c'}) (D : Catego
distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
func→ (a' C.⊕ a) func→ a' D.⊕ func→ a
module _ { ' : Level} {A B C : Category {} {'}} (F : Functor B C) (G : Functor A B) where
module _ { ' : Level} {A B C : Category '} (F : Functor B C) (G : Functor A B) where
open Functor
open Category
private
open module F = Functor F
open module G = Functor G
open module A = Category A
open module B = Category B
open module C = Category C
F* = F .func*
F→ = F .func→
G* = G .func*
G→ = G .func→
_A⊕_ = A ._⊕_
_B⊕_ = B ._⊕_
_C⊕_ = C ._⊕_
module _ {a0 a1 a2 : A .Object} {α0 : A .Arrow a0 a1} {α1 : A .Arrow a1 a2} where
F* = F.func*
F→ = F.func→
G* = G.func*
G→ = G.func→
module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
dist : (F→ G→) (α1 A.⊕ α0) (F→ G→) α1 C.⊕ (F→ G→) α0
dist : (F→ G→) (α1 A⊕ α0) (F→ G→) α1 C⊕ (F→ G→) α0
dist = begin
(F→ G→) (α1 A. α0) ≡⟨ refl
F→ (G→ (α1 A. α0)) ≡⟨ cong F→ G.distrib
F→ ((G→ α1) B. (G→ α0)) ≡⟨ F.distrib
(F→ G→) α1 C. (F→ G→) α0
(F→ G→) (α1 A⊕ α0) ≡⟨ refl
F→ (G→ (α1 A⊕ α0)) ≡⟨ cong F→ (G .distrib)
F→ ((G→ α1) B⊕ (G→ α0)) ≡⟨ F .distrib
(F→ G→) α1 C⊕ (F→ G→) α0
functor-comp : Functor A C
functor-comp =
_∘f_ : Functor A C
_∘f_ =
record
{ func* = F* G*
; func→ = F→ G→
; ident = begin
(F→ G→) (A.𝟙) ≡⟨ refl
F→ (G→ (A.𝟙)) ≡⟨ cong F→ G.ident
F→ (B.𝟙) ≡⟨ F.ident
C.𝟙
(F→ G→) (A .𝟙) ≡⟨ refl
F→ (G→ (A .𝟙)) ≡⟨ cong F→ (G .ident)
F→ (B .𝟙) ≡⟨ F .ident
C .𝟙
; distrib = dist
}
-- The identity functor
identity : { ' : Level} {C : Category {} {'}} Functor C C
-- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
identity : { '} {C : Category '} Functor C C
identity = record
{ func* = λ x x
; func→ = λ x x