Skip to content

Commit

Permalink
a bit of category theory
Browse files Browse the repository at this point in the history
  • Loading branch information
@forked-from-1kasper
forked-from-1kasper committed Dec 28, 2023
1 parent c5fdb13 commit 375dd7b
Show file tree
Hide file tree
Showing 2 changed files with 119 additions and 92 deletions.
53 changes: 28 additions & 25 deletions GroundZero/Types/Category.lean
View file
Original file line number Diff line number Diff line change
@@ -1,54 +1,57 @@
import GroundZero.Types.Precategory

open GroundZero.Types.Precategory (idtoiso)
open GroundZero.Types.Equiv
open GroundZero.Structures

namespace GroundZero.Types
universe u v

hott definition Category (A : Type u) :=
Σ (𝒞 : Precategory A), Π a b, biinv (@Precategory.idtoiso A 𝒞 a b)
hott definition Category :=
Σ (A : Precategory), Π a b, biinv (@idtoiso A a b)

namespace Category
variable {A : Type u} (𝒞 : Category A)
variable (A : Category)

hott abbreviation hom := 𝒞.1.hom
hott abbreviation obj := A.1.obj
hott abbreviation hom := A.1.hom

hott definition set : Π (x y : A), hset (hom 𝒞 x y) := 𝒞.1.set
hott definition set : Π (x y : A.obj), hset (hom A x y) := A.1.set

attribute [irreducible] set

hott abbreviation id : Π {a : A}, hom 𝒞 a a := 𝒞.1.id
hott abbreviation id : Π {a : A.obj}, hom A a a := A.1.id

hott abbreviation comp {A : Type u} {𝒞 : Category A} {a b c : A}
(f : hom 𝒞 b c) (g : hom 𝒞 a b) : hom 𝒞 a c :=
𝒞.1.comp f g
hott abbreviation comp {A : Category} {a b c : A.obj}
(f : hom A b c) (g : hom A a b) : hom A a c :=
A.1.com f g

local infix:60 " ∘ " => comp

hott abbreviation idLeft : Π {a b : A} (f : hom 𝒞 a b), f = id 𝒞 ∘ f := 𝒞.1.idLeft
hott abbreviation idRight : Π {a b : A} (f : hom 𝒞 a b), f = f ∘ id 𝒞 := 𝒞.1.idRight
hott abbreviation assoc : Π {a b c d : A} (f : hom 𝒞 a b) (g : hom 𝒞 b c) (h : hom 𝒞 c d), h ∘ (g ∘ f) = (h ∘ g) ∘ f := 𝒞.1.assoc
hott abbreviation lu : Π {a b : A.obj} (f : hom A a b), id A ∘ f = f := A.1.lu
hott abbreviation ru : Π {a b : A.obj} (f : hom A a b), f ∘ id A = f := A.1.ru
hott abbreviation assoc : Π {a b c d : A.obj} (f : hom A a b) (g : hom A b c) (h : hom A c d), h ∘ (g ∘ f) = (h ∘ g) ∘ f := A.1.assoc

hott abbreviation iso (a b : A) := Precategory.iso 𝒞.1 a b
hott abbreviation iso (a b : A.obj) := Precategory.iso A.1 a b

hott abbreviation idtoiso {a b : A} : a = b → iso 𝒞 a b :=
Precategory.idtoiso 𝒞.1
hott abbreviation idtoiso {a b : A.obj} : a = b → iso A a b :=
Precategory.idtoiso A.1

hott definition univalence {a b : A} : (a = b) ≃ (iso 𝒞 a b) :=
⟨idtoiso 𝒞, 𝒞.snd a b⟩
hott definition univalence {a b : A.obj} : (a = b) ≃ (iso A a b) :=
⟨idtoiso A, A.snd a b⟩

hott definition ua {a b : A} : iso 𝒞 a b → a = b :=
(univalence 𝒞).left
hott definition ua {a b : A.obj} : iso A a b → a = b :=
(univalence A).left

hott definition uaβrule₁ {a b : A} (φ : iso 𝒞 a b) : idtoiso 𝒞 (ua 𝒞 φ) = φ :=
(univalence 𝒞).forwardLeft φ
hott definition uaβrule₁ {a b : A.obj} (φ : iso A a b) : idtoiso A (ua A φ) = φ :=
(univalence A).forwardLeft φ

hott definition uaβrule₂ {a b : A} (φ : a = b) : ua 𝒞 (idtoiso 𝒞 φ) = φ :=
(univalence 𝒞).leftForward φ
hott definition uaβrule₂ {a b : A.obj} (φ : a = b) : ua A (idtoiso A φ) = φ :=
(univalence A).leftForward φ

hott definition Mor {A : Type u} (𝒞 : Category A) := Σ (x y : A), hom 𝒞 x y
hott definition Mor (A : Category) := Σ (x y : A.obj), hom A x y

hott definition twoOutOfThree {a b c : A} (g : hom 𝒞 b c) (f : hom 𝒞 a b) (K : Π (x y : A), hom 𝒞 x y → Type v) :=
hott definition twoOutOfThree {a b c : A.obj} (g : hom A b c) (f : hom A a b) (K : Π (x y : A.obj), hom A x y → Type v) :=
(K a b f → K b c g → K a c (g ∘ f)) × (K a c (g ∘ f) → K b c g → K a b f) × (K a b f → K a c (g ∘ f) → K b c g)
end Category

Expand Down
158 changes: 91 additions & 67 deletions GroundZero/Types/Precategory.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,107 +10,131 @@ open GroundZero.Theorems
namespace GroundZero.Types
universe u v

structure Precategory (A : Type u) :=
(hom : A → A → Type v)
(set : Π (x y : A), hset (hom x y))
(id {a : A} : hom a a)
(comp {a b c : A} : hom b c → hom a b → hom a c)
(idLeft {a b : A} : Π (f : hom a b), f = comp id f)
(idRight {a b : A} : Π (f : hom a b), f = comp f id)
(assoc {a b c d : A} : Π (f : hom a b) (g : hom b c) (h : hom c d), comp h (comp g f) = comp (comp h g) f)
record Precategory : Type (max u v + 1) :=
(obj : Type u)
(hom : obj → obj → Type v)
(set : Π (x y : obj), hset (hom x y))
(id : Π {a : obj}, hom a a)
(com : Π {a b c : obj}, hom b c → hom a b → hom a c)
(lu : Π {a b : obj} (f : hom a b), com id f = f)
(ru : Π {a b : obj} (f : hom a b), com f id = f)
(assoc : Π {a b c d : obj} (f : hom a b) (g : hom b c) (h : hom c d), com h (com g f) = com (com h g) f)

section
variable (A : Type u) (𝒞 : Precategory A)
variable (A : Precategory)

instance : Reflexive 𝒞.hom := ⟨λ _, 𝒞.id⟩
instance : Transitive 𝒞.hom := ⟨λ _ _ _ p q, 𝒞.comp q p⟩
instance : Reflexive A.hom := ⟨λ _, A.id⟩
instance : Transitive A.hom := ⟨λ _ _ _ p q, A.com q p⟩
end

namespace Precategory
hott definition compose {A : Type u} {𝒞 : Precategory A} {a b c : A}
(g : hom 𝒞 b c) (f : hom 𝒞 a b) : hom 𝒞 a c :=
𝒞.comp g f
hott abbreviation compose {A : Precategory} {a b c : A.obj} (g : hom A b c) (f : hom A a b) : hom A a c :=
A.com g f

local infix:60 " ∘ " => compose

hott definition hasInv {A : Type u} (𝒞 : Precategory A) {a b : A} (f : hom 𝒞 a b) :=
Σ (g : hom 𝒞 b a), (f ∘ g = id 𝒞) × (g ∘ f = id 𝒞)
hott definition hasInv(A : Precategory) {a b : A.obj} (f : hom A a b) :=
Σ (g : hom A b a), (f ∘ g = id A) × (g ∘ f = id A)

hott definition iso {A : Type u} (𝒞 : Precategory A) (a b : A) :=
Σ (f : hom 𝒞 a b), hasInv 𝒞 f
hott definition iso (A : Precategory) (a b : A.obj) :=
Σ (f : hom A a b), hasInv A f

hott definition idiso {A : Type u} (𝒞 : Precategory A) {a : A} : iso 𝒞 a a :=
let p : id 𝒞 = id 𝒞 ∘ id 𝒞 := idLeft 𝒞 (@id A 𝒞 a);
⟨id 𝒞, ⟨id 𝒞, (p⁻¹, p⁻¹)⟩⟩
hott definition idiso (A : Precategory) {a : A.obj} : iso A a a :=
⟨id A, ⟨id A, (lu A (id A), lu A (id A))⟩⟩

instance {A : Type u} (𝒞 : Precategory A) : Reflexive (iso 𝒞) := ⟨@idiso _ 𝒞⟩
instance (A : Precategory) : Reflexive (iso A) := ⟨@idiso A⟩

hott definition idtoiso {A : Type u} (𝒞 : Precategory A)
{a b : A} (p : a = b) : iso 𝒞 a b :=
hott definition idtoiso (A : Precategory) {a b : A.obj} (p : a = b) : iso A a b :=
begin induction p; reflexivity end

hott definition invProp {A : Type u} (𝒞 : Precategory A)
{a b : A} (f : hom 𝒞 a b) : prop (hasInv 𝒞 f) :=
hott definition invProp (A : Precategory) {a b : A.obj} (f : hom A a b) : prop (hasInv A f) :=
begin
intro ⟨g', (H₁, H₂)⟩ ⟨g, (G₁, G₂)⟩;
fapply Sigma.prod; apply calc
g' = id 𝒞 ∘ g' : idLeft _ _
g' = id A ∘ g' : (lu _ _)⁻¹
... = (g ∘ f) ∘ g' : ap (compose · g') G₂⁻¹
... = g ∘ (f ∘ g') : (assoc _ _ _ _)⁻¹
... = g ∘ id 𝒞 : ap (compose g) H₁
... = g : (idRight _ _)⁻¹;
... = g ∘ id A : ap (compose g) H₁
... = g : ru _ _;
apply productProp <;> apply set
end

hott definition op {A : Type u} (𝒞 : Precategory A) : Precategory A :=
{ hom := λ a b, hom 𝒞 b a,
set := λ a b, set 𝒞 b a,
id := 𝒞.id,
comp := λ p q, 𝒞.comp q p,
idLeft := λ p, 𝒞.idRight p,
idRight := λ p, 𝒞.idLeft p,
assoc := λ f g h, (𝒞.assoc h g f)⁻¹ }

hott definition Path (A : Type u) (H : groupoid A) : Precategory A :=
{ hom := @Id A,
set := H,
id := idp _,
comp := λ p q, q ⬝ p,
idRight := λ p, (Id.lid p)⁻¹,
idLeft := λ p, (Id.rid p)⁻¹,
assoc := λ f g h, (Id.assoc f g h)⁻¹ }

hott definition univalent {A : Type u} (𝒞 : Precategory A) :=
Π a b, biinv (@Precategory.idtoiso A 𝒞 a b)

hott definition isGroupoidIfUnivalent {A : Type u} (𝒞 : Precategory A) : univalent 𝒞 → groupoid A :=
hott definition op (A : Precategory) : Precategory :=
⟨A.obj, λ a b, hom A b a, λ a b, set A b a, id A,
λ p q, A.com q p, λ p, A.ru p, λ p, A.lu p, λ f g h, (A.assoc h g f)⁻¹⟩

hott definition Path (A : Type u) (H : groupoid A) : Precategory :=
⟨A, Id, H, idp _, λ p q, q ⬝ p, Id.rid, Id.lid, λ f g h, (Id.assoc f g h)⁻¹⟩

hott definition univalent (A : Precategory) :=
Π a b, biinv (@idtoiso A a b)

hott definition isGroupoidIfUnivalent (A : Precategory) : univalent A → groupoid A.obj :=
begin
intros H a b; change hset (a = b); apply hsetRespectsEquiv;
symmetry; existsi idtoiso 𝒞; apply H; apply hsetRespectsSigma;
apply 𝒞.set; intro; apply propIsSet; apply invProp
symmetry; existsi idtoiso A; apply H; apply hsetRespectsSigma;
apply A.set; intro; apply propIsSet; apply invProp
end

record Functor (A B : Precategory) :=
(apo : A.obj → B.obj)
(apf : Π {a b : A.obj}, hom A a b → hom B (apo a) (apo b))
(apid : Π (a : A.obj), apf (@id A a) = id B)
(apcom : Π {a b c : A.obj} (f : hom A b c) (g : hom A a b), apf (f ∘ g) = apf f ∘ apf g)

instance (A B : Precategory) : CoeFun (Functor A B) (λ _, A.obj → B.obj) := ⟨Functor.apo⟩

section
variable {A B : Precategory} (F : Functor A B)

hott definition isFaithful := Π a b, injective (@Functor.apf A B F a b)
hott definition isFull := Π a b, surjective (@Functor.apf A B F a b)
end

section
variable {A B C : Precategory}

hott definition Functor.com (F : Functor B C) (G : Functor A B) : Functor A C :=
⟨F.apo ∘ G.apo, F.apf ∘ G.apf, λ x, ap F.apf (G.apid x) ⬝ F.apid (G x),
λ f g, ap F.apf (G.apcom f g) ⬝ F.apcom (G.apf f) (G.apf g)⟩
end

hott definition Functor {A : Type u} {B : Type v} (𝒞 : Precategory A) (𝒟 : Precategory B) :=
Σ (F : A → B) (G : Π a b, 𝒞.hom a b → 𝒟.hom (F a) (F b)),
(Π a, G a a 𝒞.id = 𝒟.id) × (Π a b c f g, G a c (𝒞.comp f g) = 𝒟.comp (G b c f) (G a b g))
record Natural {A B : Precategory} (F G : Functor A B) :=
(com : Π x, hom B (F x) (G x))
(nat : Π {a b : A.obj} (f : hom A a b), com b ∘ F.apf f = G.apf f ∘ com a)

section
variable (A B : Precategory) (F G : Functor A B)
instance : CoeFun (Natural F G) (λ _, Π x, hom B (F x) (G x)) := ⟨Natural.com⟩
end

section
variable {A : Type u} {B : Type v} {𝒞 : Precategory A} {𝒟 : Precategory B} (F : Functor 𝒞 𝒟)
variable {A B : Precategory}

hott definition idn (F : Functor A B) : Natural F F :=
⟨λ _, id B, λ f, lu B (F.apf f) ⬝ (ru B (F.apf f))⁻¹⟩

hott definition isFaithful := Π a b, injective (F.2.1 a b)
hott definition isFull := Π a b, surjective (F.2.1 a b)
hott definition Natural.vert {F G H : Functor A B} (ε : Natural G H) (η : Natural F G) : Natural F H :=
⟨λ x, ε x ∘ η x, λ {a b} f, (assoc B _ _ _)⁻¹ ⬝ ap (B.com (ε b)) (η.nat f) ⬝ assoc B _ _ _ ⬝
ap (B.com · (η a)) (ε.nat f) ⬝ (assoc B _ _ _)⁻¹⟩
end

hott definition Natural {A : Type u} {B : Type v} {𝒞 : Precategory A} {𝒟 : Precategory B} (F G : Functor 𝒞 𝒟) :=
Σ (η : Π x, hom 𝒟 (F.1 x) (G.1 x)), Π (a b : A) (f : hom 𝒞 a b), η b ∘ F.2.1 a b f = G.2.1 a b f ∘ η a
section
variable {A B C : Precategory} {F₁ F₂ : Functor B C} {G₁ G₂ : Functor A B}

hott definition Natural.horiz (ε : Natural F₁ F₂) (η : Natural G₁ G₂) : Natural (F₁.com G₁) (F₂.com G₂) :=
⟨λ x, ε (G₂ x) ∘ F₁.apf (η x), λ f, ap (C.com · _) (ε.nat _) ⬝ (assoc C _ _ _)⁻¹ ⬝ ap (C.com _ ·) (ε.nat _) ⬝
assoc C _ _ _ ⬝ ap (C.com · _) ((F₂.apcom _ _)⁻¹ ⬝ ap F₂.apf (η.nat _) ⬝
F₂.apcom _ _) ⬝ (assoc C _ _ _)⁻¹ ⬝ ap (C.com _) (ε.nat _)⁻¹⟩
end

hott definition isProduct {A : Type u} (𝒞 : Precategory A) (a b c : A) :=
Σ (i : hom 𝒞 c a) (j : hom 𝒞 c b),
∀ (x : A) (f₁ : hom 𝒞 x a) (f₂ : hom 𝒞 x b),
contr (Σ (f : hom 𝒞 x c), i ∘ f = f₁ × j ∘ f = f₂)
hott definition isProduct (A : Precategory) (a b c : A.obj) :=
Σ (i : hom A c a) (j : hom A c b),
∀ (x : A.obj) (f₁ : hom A x a) (f₂ : hom A x b),
contr (Σ (f : hom A x c), i ∘ f = f₁ × j ∘ f = f₂)

hott definition isCoproduct {A : Type u} (𝒞 : Precategory A) (a b c : A) :=
isProduct (op 𝒞) a b c
hott definition isCoproduct (A : Precategory) (a b c : A.obj) :=
isProduct (op A) a b c
end Precategory

end GroundZero.Types

0 comments on commit 375dd7b

Please sign in to comment.