From 5fd7dcae9dbec409bbd3c2c16f653fb202e87261 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 21 Jan 2018 00:21:25 +0100 Subject: [PATCH] Notes from Andrea and some stuff about products --- src/Cat/Categories/Cat.agda | 115 ++++++++++++++++++++++++++++------- src/Cat/Categories/Sets.agda | 4 ++ src/Cat/Category.agda | 109 +++++++++++++++++++++++---------- src/Cat/Category/Bij.agda | 2 +- src/Cat/Cubical.agda | 7 ++- 5 files changed, 181 insertions(+), 56 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 1133eee..79aeb58 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -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₂ + } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index bd026dc..62c463e 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -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 diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index a30aee4..7d84df8 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -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 = _⊕_ ℂ diff --git a/src/Cat/Category/Bij.agda b/src/Cat/Category/Bij.agda index 0d55500..0892f55 100644 --- a/src/Cat/Category/Bij.agda +++ b/src/Cat/Category/Bij.agda @@ -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 = {!!} diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda index f5abda3..92f3d12 100644 --- a/src/Cat/Cubical.agda +++ b/src/Cat/Cubical.agda @@ -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 ℓ