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

Notes from Andrea and some stuff about products

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-01-21 00:21:25 +01:00
parent da10e63cc8
commit 5fd7dcae9d
5 changed files with 181 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,36 +10,57 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Cat.Category
open import Cat.Functor
-- 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
--lift-eq a b = λ i → a i , b i
open Functor
open Category
module _ {ℓ ℓ' : Level} {A B : Category {ℓ} {ℓ'}} where
lift-eq-functors : {f g : Functor A B}
→ (eq* : Functor.func* f ≡ Functor.func* g)
→ (eq→ : PathP (λ i → ∀ {x y} → Arrow A x y → Arrow B (eq* i x) (eq* i y))
(func→ f) (func→ g))
-- → (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 : 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 f g eq* x = {!!}
postulate assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
-- assc = lift-eq-functors refl refl {!refl!} λ i j → {!!}
module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
idHere = identity {ℓ} {ℓ'} {A}
lem : (Functor.func* f) ∘ (Functor.func* idHere) ≡ Functor.func* f
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 ⊛ identity) ≡ func→ f
lemmm : PathP
(λ i →
{x y : Object A} → Arrow A x y → Arrow B (func* f x) (func* f y))
(func→ (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 ⊛ identity)) (ident f)
-- lemz = {!!}
postulate ident-r : f ⊛ identity ≡ f
-- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!}
postulate ident-l : identity ⊛ f ≡ f
-- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
CatCat =
@ -48,6 +69,54 @@ module _ {ℓ ℓ' : Level} where
; Arrow = Functor
; 𝟙 = identity
; _⊕_ = functor-comp
; assoc = {!!}
-- What gives here? Why can I not name the variables directly?
; assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
; ident = ident-r , ident-l
}
module _ {ℓ : Level} (C D : Category {ℓ} {ℓ}) where
private
proj₁ : Arrow CatCat (catProduct C D) C
proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
proj₂ : Arrow CatCat (catProduct C D) D
proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
module _ {X : Object (CatCat {ℓ} {ℓ})} (x₁ : Arrow CatCat X C) (x₂ : Arrow CatCat 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 (catProduct C D)
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.
isUniqL : (CatCat ⊕ proj₁) x ≡ x₁
isUniqL = lift-eq-functors refl refl {!!} {!!}
isUniqR : (CatCat ⊕ proj₂) x ≡ x₂
isUniqR = lift-eq-functors refl refl {!!} {!!}
isUniq : (CatCat ⊕ proj₁) x ≡ x₁ × (CatCat ⊕ proj₂) x ≡ x₂
isUniq = isUniqL , isUniqR
uniq : ∃![ x ] ((CatCat ⊕ proj₁) x ≡ x₁ × (CatCat ⊕ proj₂) x ≡ x₂)
uniq = x , isUniq
instance
isProduct : IsProduct CatCat proj₁ proj₂
isProduct = uniq
product : Product {ℂ = CatCat} C D
product = record
{ obj = catProduct C D
; proj₁ = proj₁
; proj₂ = proj₂
}

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

@ -25,9 +25,11 @@ Sets {ℓ} = record
; ident = funExt (λ x → refl) , funExt (λ x → refl)
}
-- Covariant Presheaf
Representable : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
-- The "co-yoneda" embedding.
representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Representable ℂ
representable {ℂ = ℂ} A = record
{ func* = λ B → ℂ.Arrow A B
@ -38,9 +40,11 @@ representable {ℂ = ℂ} A = record
where
open module ℂ = Category ℂ
-- Contravariant Presheaf
Presheaf : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → Set (ℓ ⊔ lsuc ℓ')
Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
-- Alternate name: `yoneda`
presheaf : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
{ func* = λ A → ℂ.Arrow A B

109
src/Cat/Category.agda
View file

@ -4,15 +4,29 @@ 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
∃! : ∀ {a b} {A : Set a}
→ (A → Set b) → Set (a ⊔ b)
∃! = ∃!≈ _≡_
∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃!-syntax = ∃
syntax ∃!-syntax (λ x → B) = ∃![ x ] B
postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
constructor category
-- adding no-eta-equality can speed up type-checking.
no-eta-equality
field
Object : Set ℓ
Arrow : Object → Object → Set ℓ'
@ -36,7 +50,7 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w
_+_ = ℂ._⊕_
Isomorphism : (f : ℂ.Arrow A B) → Set ℓ'
Isomorphism f = Σ[ g ∈ ℂ.Arrow B A ] g + f ≡ ℂ.𝟙 × f + g ≡ ℂ.𝟙
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₁
@ -92,28 +106,55 @@ _≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ.Arrow A B ] (Isomorphism {ℂ = ℂ} f)
where
open module ℂ = Category ℂ
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
}
IsProduct : ∀ {ℓ ℓ'} (ℂ : Category {ℓ} {ℓ'}) {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
IsProduct ℂ {A = A} {B = B} π₁ π₂
= ∀ {X : ℂ.Object} (x₁ : ℂ.Arrow X A) (x₂ : ℂ.Arrow X B)
→ ∃![ x ] (π₁ ℂ.⊕ x ≡ x₁ × π₂ ℂ.⊕ x ≡ x₂)
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)}))
open module ℂ = Category ℂ
-- Consider this style for efficiency:
-- record R : Set where
-- field
-- isP : IsProduct {!!} {!!} {!!}
record Product {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} (A B : Category.Object ℂ) : Set (ℓ ⊔ ℓ') where
no-eta-equality
field
obj : Category.Object ℂ
proj₁ : Category.Arrow ℂ obj A
proj₂ : Category.Arrow ℂ obj B
{{isProduct}} : IsProduct ℂ proj₁ proj₂
mutual
catProduct : {ℓ : Level} → ( C D : Category {ℓ} {ℓ} ) → Category {ℓ} {ℓ}
catProduct C D =
record
{ Object = C.Object × D.Object
-- Why does "outlining with `arrowProduct` not work?
; Arrow = λ {(c , d) (c' , d') → Arrow C c c' × Arrow D d d'}
; 𝟙 = 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)}))
-- arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} → (Object C) × (Object D) → (Object C) × (Object D) → Set ℓ
-- arrowProduct = {!!}
-- Arrows in the product-category
arrowProduct : ∀ {ℓ} {C D : Category {ℓ} {ℓ}} (c d : Object (catProduct C D)) → Set ℓ
arrowProduct {C = C} {D = D} (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
Opposite : ∀ {ℓ ℓ'} → Category {ℓ} {ℓ'} → Category {ℓ} {ℓ'}
Opposite ℂ =
@ -128,15 +169,21 @@ Opposite ℂ =
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) = {!!}
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')
HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
→ Hom ℂ A B → Hom ℂ A B'
HomFromArrow _A g = λ f → g + f
HomFromArrow _A = _⊕_ ℂ

2
src/Cat/Category/Bij.agda
View file

@ -23,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 = ?
vw-bij a = {!!}
-- tubij a with (t ∘ u) a
-- ... | q = {!!}

7
src/Cat/Cubical.agda
View file

@ -10,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 ℓ