Skip to content

Commit

Permalink
Clean category theory (#624)
Browse files Browse the repository at this point in the history 
* delete redundant file

* lots of cleaning (in particular make argument to id implicit)

* remove duplicate yoneda code
  • Loading branch information
@mortberg
mortberg authored Nov 19, 2021
1 parent 93d7f41 commit b0c2da6
Show file tree
Hide file tree
Showing 25 changed files with 202 additions and 370 deletions.
38 changes: 19 additions & 19 deletions Cubical/Categories/Adjoint.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,8 +68,8 @@ module UnitCounit where
⦃ isCatC : isCategory C ⦄ ⦃ isCatD : isCategory D ⦄
(η : 𝟙⟨ C ⟩ ⇒ (funcComp G F))
(ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩)
(Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id (F ⟅ c ⟆))
(Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id (G ⟅ d ⟆))
(Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id)
(Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id)
where

make⊣ : F ⊣ G
Expand Down Expand Up @@ -170,27 +170,27 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
-- ETA

-- trivial commutative diagram between identities in D
commInD : ∀ {x y} (f : C [ x , y ]) → (D .id _) ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _)
commInD : ∀ {x y} (f : C [ x , y ]) → D .id ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id
commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _)

sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _) ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _) ♭ ♯
sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ♭ ♯
sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _))

η' : 𝟙⟨ C ⟩ ⇒ G ∘F F
η' .N-ob x = (D .id _) ♭
η' .N-ob x = D .id ♭
η' .N-hom f = sym (fst (adjNat') (commInD f ∙ sharpen1 f))

-- EPSILON

-- trivial commutative diagram between identities in C
commInC : ∀ {x y} (g : D [ x , y ]) → (C .id _) ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ (C .id _)
commInC : ∀ {x y} (g : D [ x , y ]) → C .id ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ C .id
commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _)

sharpen2 : ∀ {x y} (g : D [ x , y ]) → (C .id _ ♯ ♭) ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ (C .id _) ⋆⟨ C ⟩ G ⟪ g ⟫
sharpen2 : ∀ {x y} (g : D [ x , y ]) → C .id ♯ ♭ ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ C .id ⋆⟨ C ⟩ G ⟪ g ⟫
sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _)

ε' : F ∘F G ⇒ 𝟙⟨ D ⟩
ε' .N-ob x = (C .id _) ♯
ε' .N-ob x = C .id ♯
ε' .N-hom g = sym (snd adjNat' (sharpen2 g ∙ commInC g))

-- DELTA 1
Expand All @@ -209,9 +209,9 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
→ (idTrans F) ⟦ c ⟧ ≡ (seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F) .N-ob c)
body c = (idTrans F) ⟦ c ⟧
≡⟨ refl ⟩
D .id _
D .id
≡⟨ sym (D .⋆IdL _) ⟩
D .id _ ⋆⟨ D ⟩ D .id _
D .id ⋆⟨ D ⟩ D .id
≡⟨ snd adjNat' (cong (λ v → (η' ⟦ c ⟧) ⋆⟨ C ⟩ v) (G .F-id)) ⟩
F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
≡⟨ sym (expL c) ⟩
Expand All @@ -226,16 +226,16 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
-- DELTA 2

body2 : ∀ (d)
→ seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧) ≡ C .id (G .F-ob d)
→ seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧) ≡ C .id
body2 d = seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧)
≡⟨ seqP≡seq {C = C} _ _ ⟩
((η' ∘ˡ G) ⟦ d ⟧) ⋆⟨ C ⟩ ((G ∘ʳ ε') ⟦ d ⟧)
≡⟨ refl ⟩
(η' ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ (G ⟪ ε' ⟦ d ⟧ ⟫)
≡⟨ fst adjNat' (cong (λ v → v ⋆⟨ D ⟩ (ε' ⟦ d ⟧)) (sym (F .F-id))) ⟩
C .id _ ⋆⟨ C ⟩ C .id _
C .id ⋆⟨ C ⟩ C .id
≡⟨ C .⋆IdL _ ⟩
C .id (G .F-ob d)
C .id
∎

Δ₂' : PathP (λ i → NatTrans (F-rUnit {F = G} i) (F-lUnit {F = G} i))
Expand All @@ -251,20 +251,20 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor

-- helper functions for working with this Adjoint definition

δ₁ : ∀ {c} → (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧) ≡ D .id _
δ₁ : ∀ {c} → (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧) ≡ D .id
δ₁ {c} = (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧)
≡⟨ sym (seqP≡seq {C = D} _ _) ⟩
seqP {C = D} {p = refl} (F ⟪ η ⟦ c ⟧ ⟫) (ε ⟦ F ⟅ c ⟆ ⟧)
≡⟨ (λ j → (Δ₁ j) .N-ob c) ⟩
D .id _
D .id
∎

δ₂ : ∀ {d} → (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫) ≡ C .id _
δ₂ : ∀ {d} → (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫) ≡ C .id
δ₂ {d} = (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
≡⟨ sym (seqP≡seq {C = C} _ _) ⟩
seqP {C = C} {p = refl} (η ⟦ G ⟅ d ⟆ ⟧) (G ⟪ ε ⟦ d ⟧ ⟫)
≡⟨ (λ j → (Δ₂ j) .N-ob d) ⟩
C .id _
C .id
∎


Expand All @@ -287,7 +287,7 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
≡⟨ C .⋆Assoc _ _ _ ⟩
g ⋆⟨ C ⟩ (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
≡⟨ lPrecatWhisker {C = C} _ _ _ δ₂ ⟩
g ⋆⟨ C ⟩ C .id _
g ⋆⟨ C ⟩ C .id
≡⟨ C .⋆IdR _ ⟩
g
∎
Expand All @@ -307,7 +307,7 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
-- apply triangle identity
≡⟨ rPrecatWhisker {C = D} _ _ _ δ₁ ⟩
(D .id _) ⋆⟨ D ⟩ f
D .id ⋆⟨ D ⟩ f
≡⟨ D .⋆IdL _ ⟩
f
∎
Expand Down
4 changes: 0 additions & 4 deletions Cubical/Categories/Category.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,8 @@
- pathToIso : Turns a path between two objects into an isomorphism between them
- opposite categories
-}

{-# OPTIONS --safe #-}


module Cubical.Categories.Category where

open import Cubical.Categories.Category.Base public
Expand Down
40 changes: 14 additions & 26 deletions Cubical/Categories/Category/Base.agda
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
{-# OPTIONS --safe #-}


module Cubical.Categories.Category.Base where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
Expand All @@ -13,17 +10,15 @@ private
ℓ ℓ' : Level

-- Precategories

record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
-- no-eta-equality ; NOTE: need eta equality for `opop`
field
ob : Type ℓ
Hom[_,_] : ob → ob → Type ℓ'
id : ∀ x → Hom[ x , x ]
_⋆_ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
-- TODO: change these to implicit argument
⋆IdL : ∀ {x y : ob} (f : Hom[ x , y ]) → (id x) ⋆ f ≡ f
⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ (id y) ≡ f
id : ∀ {x} → Hom[ x , x ]
_⋆_ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
⋆IdL : ∀ {x y} (f : Hom[ x , y ]) → id ⋆ f ≡ f
⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f
⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ]) → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)

-- composition: alternative to diagramatic order
Expand All @@ -34,11 +29,10 @@ open Precategory


-- Helpful syntax/notation

_[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ'
_[_,_] = Hom[_,_]

-- needed to define this in order to be able to make the subsequence syntax declaration
-- Needed to define this in order to be able to make the subsequence syntax declaration
seq' : ∀ (C : Precategory ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
seq' = _⋆_

Expand All @@ -54,46 +48,42 @@ syntax comp' C g f = g ∘⟨ C ⟩ f


-- Categories

record isCategory (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
field
isSetHom : ∀ {x y} → isSet (C [ x , y ])

-- Isomorphisms and paths in precategories

record CatIso {C : Precategory ℓ ℓ'} (x y : C .Precategory.ob) : Type ℓ' where
record CatIso {C : Precategory ℓ ℓ'} (x y : C .ob) : Type ℓ' where
constructor catiso
field
mor : C [ x , y ]
inv : C [ y , x ]
sec : inv ⋆⟨ C ⟩ mor ≡ C .id y
ret : mor ⋆⟨ C ⟩ inv ≡ C .id x
sec : inv ⋆⟨ C ⟩ mor ≡ C .id
ret : mor ⋆⟨ C ⟩ inv ≡ C .id


pathToIso : {C : Precategory ℓ ℓ'} (x y : C .ob) (p : x ≡ y) → CatIso {C = C} x y
pathToIso {C = C} x y p = J (λ z _ → CatIso x z) (catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)) p
pathToIso : {C : Precategory ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso {C = C} x y
pathToIso {C = C} p = J (λ z _ → CatIso _ z) (catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx)) p
where
idx = C .id x
idx = C .id

-- Univalent Categories

record isUnivalent (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
field
univ : (x y : C .ob) → isEquiv (pathToIso {C = C} x y)
univ : (x y : C .ob) → isEquiv (pathToIso {C = C} {x = x} {y = y})

-- package up the univalence equivalence
univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso x y)
univEquiv x y = (pathToIso {C = C} x y) , (univ x y)
univEquiv x y = pathToIso , univ x y

-- The function extracting paths from category-theoretic isomorphisms.
CatIsoToPath : {x y : C .ob} (p : CatIso x y) → x ≡ y
CatIsoToPath {x = x} {y = y} p =
equivFun (invEquiv (univEquiv x y)) p

open isUnivalent public

-- Opposite Categories

-- Opposite category
_^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
(C ^op) .ob = C .ob
(C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
Expand All @@ -102,5 +92,3 @@ _^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
(C ^op) .⋆IdL = C .⋆IdR
(C ^op) .⋆IdR = C .⋆IdL
(C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)

open isCategory public
29 changes: 14 additions & 15 deletions Cubical/Categories/Category/Properties.agda
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
{-# OPTIONS --safe #-}


module Cubical.Categories.Category.Properties where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category.Base hiding (isSetHom)

open import Cubical.Categories.Category.Base

open Precategory

Expand All @@ -32,36 +30,37 @@ module _ {C : Precategory ℓ ℓ'} ⦃ isC : isCategory C ⦄ where
isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom {y = a})



-- opposite of opposite is definitionally equal to itself
involutiveOp : ∀ {C : Precategory ℓ ℓ'} → (C ^op) ^op ≡ C
involutiveOp : ∀ {C : Precategory ℓ ℓ'} → C ^op ^op ≡ C
involutiveOp = refl

module _ {C : Precategory ℓ ℓ'} where
-- Other useful operations on categories

-- whisker the parallel morphisms g and g' with f
lPrecatWhisker : {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g') → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g'
lPrecatWhisker : {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g')
→ f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g'
lPrecatWhisker f _ _ p = cong (_⋆_ C f) p

rPrecatWhisker : {x y z : C .ob} (f f' : C [ x , y ]) (g : C [ y , z ]) (p : f ≡ f') → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g
rPrecatWhisker : {x y z : C .ob} (f f' : C [ x , y ]) (g : C [ y , z ]) (p : f ≡ f')
→ f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g
rPrecatWhisker _ _ g p = cong (λ v → v ⋆⟨ C ⟩ g) p

-- working with equal objects
idP : ∀ {x x'} {p : x ≡ x'} → C [ x , x' ]
idP {x = x} {x'} {p} = subst (λ v → C [ x , v ]) p (C .id x)
idP {x} {x'} {p} = subst (λ v → C [ x , v ]) p (C .id)

-- heterogeneous seq
seqP : ∀ {x y y' z} {p : y ≡ y'}
→ (f : C [ x , y ]) (g : C [ y' , z ])
→ C [ x , z ]
seqP {x = x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g)
seqP {x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g)

-- also heterogeneous seq, but substituting on the left
seqP' : ∀ {x y y' z} {p : y ≡ y'}
→ (f : C [ x , y ]) (g : C [ y' , z ])
→ C [ x , z ]
seqP' {x = x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g
→ (f : C [ x , y ]) (g : C [ y' , z ])
→ C [ x , z ]
seqP' {x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g

-- show that they're equal
seqP≡seqP' : ∀ {x y y' z} {p : y ≡ y'}
Expand All @@ -74,8 +73,8 @@ module _ {C : Precategory ℓ ℓ'} where

-- seqP is equal to normal seq when y ≡ y'
seqP≡seq : ∀ {x y z}
→ (f : C [ x , y ]) (g : C [ y , z ])
→ seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g
→ (f : C [ x , y ]) (g : C [ y , z ])
→ seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g
seqP≡seq {y = y} {z} f g i = f ⋆⟨ C ⟩ toPathP {A = λ _ → C [ y , z ]} {x = g} refl (~ i)


Expand Down
20 changes: 10 additions & 10 deletions Cubical/Categories/Constructions/Elements.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ infix 50 ∫_
(∫ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
-- morphisms are f : c → c' which take x to x'
(∫ F) .Hom[_,_] (c , x) (c' , x') = Σ[ f ∈ C [ c , c' ] ] x' ≡ (F ⟪ f ⟫) x
(∫ F) .id (c , x) = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
(∫ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
(∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
= (f ⋆⟨ C ⟩ g) , (x₂
≡⟨ q ⟩
Expand All @@ -49,16 +49,16 @@ infix 50 ∫_
cIdL = C .⋆IdL f

-- proof from composition with id
p' : x' ≡ (F ⟪ C .id c ⋆⟨ C ⟩ f ⟫) x
p' = snd ((∫ F) ._⋆_ ((∫ F) .id o) f')
p' : x' ≡ (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x
p' = snd ((∫ F) ._⋆_ ((∫ F) .id) f')
(∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
= (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' x' ((F ⟪ a ⟫) x)) p' p cIdR i
where
cIdR = C .⋆IdR f
isS' = getIsSet F c'

p' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id c' ⟫) x
p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id o1))
p' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x
p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id))
(∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
= (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ x₃ ((F ⟪ a ⟫) x)) p1 p2 cAssoc i
where
Expand All @@ -78,7 +78,7 @@ infix 50 ∫_
(∫ᴾ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
-- morphisms are f : c → c' which take x to x'
(∫ᴾ F) .Hom[_,_] (c , x) (c' , x') = Σ[ f ∈ C [ c , c' ] ] x ≡ (F ⟪ f ⟫) x'
(∫ᴾ F) .id (c , x) = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
(∫ᴾ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
(∫ᴾ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
= (f ⋆⟨ C ⟩ g) , (x
≡⟨ p ⟩
Expand All @@ -96,16 +96,16 @@ infix 50 ∫_
cIdL = C .⋆IdL f

-- proof from composition with id
p' : x ≡ (F ⟪ C .id c ⋆⟨ C ⟩ f ⟫) x'
p' = snd ((∫ᴾ F) ._⋆_ ((∫ᴾ F) .id o) f')
p' : x ≡ (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x'
p' = snd ((∫ᴾ F) ._⋆_ ((∫ᴾ F) .id) f')
(∫ᴾ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
= (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x')) p' p cIdR i
where
cIdR = C .⋆IdR f
isS = getIsSet F c

p' : x ≡ (F ⟪ f ⋆⟨ C ⟩ C .id c' ⟫) x'
p' = snd ((∫ᴾ F) ._⋆_ f' ((∫ᴾ F) .id o1))
p' : x ≡ (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x'
p' = snd ((∫ᴾ F) ._⋆_ f' ((∫ᴾ F) .id))
(∫ᴾ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
= (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x₃)) p1 p2 cAssoc i
where
Expand Down
Loading

0 comments on commit b0c2da6

Please sign in to comment.