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

Rename ident to isIdentity

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 12:49:41 +01:00
parent 5cbc409770
commit 6446435a49
9 changed files with 55 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -91,13 +91,13 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
issSet = setSig {sA = C.arrowIsSet} {sB = λ x → D.arrowIsSet}
ident' : IsIdentity :𝟙:
ident'
= Σ≡ (fst C.ident) (fst D.ident)
, Σ≡ (snd C.ident) (snd D.ident)
= Σ≡ (fst C.isIdentity) (fst D.isIdentity)
, Σ≡ (snd C.isIdentity) (snd D.isIdentity)
postulate univalent : Univalence.Univalent :rawProduct: ident'
instance
:isCategory: : IsCategory :rawProduct:
IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative
IsCategory.ident :isCategory: = ident'
IsCategory.isIdentity :isCategory: = ident'
IsCategory.arrowIsSet :isCategory: = issSet
IsCategory.univalent :isCategory: = univalent
@ -107,13 +107,13 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
proj₁ : Catt [ :product: , ℂ ]
proj₁ = record
{ raw = record { func* = fst ; func→ = fst }
; isFunctor = record { ident = refl ; distrib = refl }
; isFunctor = record { isIdentity = refl ; distrib = refl }
}
proj₂ : Catt [ :product: , 𝔻 ]
proj₂ = record
{ raw = record { func* = snd ; func→ = snd }
; isFunctor = record { ident = refl ; distrib = refl }
; isFunctor = record { isIdentity = refl ; distrib = refl }
}
module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where
@ -124,7 +124,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
; func→ = λ x → func→ x₁ x , func→ x₂ x
}
; isFunctor = record
{ ident = Σ≡ x₁.ident x₂.ident
{ isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity
; distrib = Σ≡ x₁.distrib x₂.distrib
}
}
@ -230,7 +230,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
-- NaturalTransformation F G × ℂ .Arrow A B
-- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
-- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity)
-- where
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
-- Unfortunately the equational version has some ambigous arguments.
@ -239,8 +239,8 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
:func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
:func→: {c} {c} (identityNat F , 𝟙 ℂ) ≡⟨⟩
𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.ident ⟩
func→ F (𝟙 ℂ) ≡⟨ F.ident ⟩
𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩
func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩
𝟙 𝔻 ∎
where
open module 𝔻 = Category 𝔻
@ -313,7 +313,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
; func→ = λ {dom} {cod} → :func→: {dom} {cod}
}
; isFunctor = record
{ ident = λ {o} → :ident: {o}
{ isIdentity = λ {o} → :ident: {o}
; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y}
}
}

6
src/Cat/Categories/Fam.agda
View file

@ -29,8 +29,8 @@ module _ (ℓa ℓb : Level) where
isAssociative = Σ≡ refl refl
module _ {A B : Obj'} {f : Arr A B} where
ident : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
ident = (Σ≡ refl refl) , Σ≡ refl refl
isIdentity : B ⟨ f ∘ one ⟩ ≡ f × B ⟨ one {B} ∘ f ⟩ ≡ f
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
@ -45,7 +45,7 @@ module _ (ℓa ℓb : Level) where
isCategory : IsCategory RawFam
isCategory = record
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
; ident = λ {A} {B} {f} → ident {A} {B} {f = f}
; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
; arrowIsSet = {!!}
; univalent = {!!}
}

2
src/Cat/Categories/Free.agda
View file

@ -58,7 +58,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
RawIsCategoryFree : IsCategory RawFree
RawIsCategoryFree = record
{ isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}}
; ident = ident-r , ident-l
; isIdentity = ident-r , ident-l
; arrowIsSet = {!!}
; univalent = {!!}
}

10
src/Cat/Categories/Fun.agda
View file

@ -60,8 +60,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩
𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
@ -143,10 +143,10 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
eq-r C = begin
𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.ident ⟩
𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.isIdentity ⟩
f' C ∎
eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
eq-l C = proj₂ 𝔻.ident
eq-l C = proj₂ 𝔻.isIdentity
ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
ident-r = lemSig allNatural _ _ (funExt eq-r)
ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
@ -169,7 +169,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
:isCategory: : IsCategory RawFun
:isCategory: = record
{ isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
; ident = λ {A B} → :ident: {A} {B}
; isIdentity = λ {A B} → :ident: {A} {B}
; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
; univalent = {!!}
}

2
src/Cat/Categories/Rel.agda
View file

@ -165,7 +165,7 @@ RawRel = record
RawIsCategoryRel : IsCategory RawRel
RawIsCategoryRel = record
{ isAssociative = funExt is-isAssociative
; ident = funExt ident-l , funExt ident-r
; isIdentity = funExt ident-l , funExt ident-r
; arrowIsSet = {!!}
; univalent = {!!}
}

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

@ -26,8 +26,8 @@ module _ (ℓ : Level) where
SetsIsCategory : IsCategory SetsRaw
isAssociative SetsIsCategory = refl
proj₁ (ident SetsIsCategory) = funExt λ _ → refl
proj₂ (ident SetsIsCategory) = funExt λ _ → refl
proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
univalent SetsIsCategory = {!!}
@ -98,7 +98,7 @@ module _ {ℓa ℓb : Level} where
; func→ = ℂ [_∘_]
}
; isFunctor = record
{ ident = funExt λ _ → proj₂ ident
{ isIdentity = funExt λ _ → proj₂ isIdentity
; distrib = funExt λ x → sym isAssociative
}
}
@ -113,7 +113,7 @@ module _ {ℓa ℓb : Level} where
; func→ = λ f g → ℂ [ g ∘ f ]
}
; isFunctor = record
{ ident = funExt λ x → proj₁ ident
{ isIdentity = funExt λ x → proj₁ isIdentity
; distrib = funExt λ x → isAssociative
}
}

36
src/Cat/Category.agda
View file

@ -83,9 +83,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
-- Univalence is indexed by a raw category as well as an identity proof.
module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
open RawCategory ℂ
module _ (ident : IsIdentity 𝟙) where
module _ (isIdentity : IsIdentity 𝟙) where
idIso : (A : Object) → A ≅ A
idIso A = 𝟙 , (𝟙 , ident)
idIso A = 𝟙 , (𝟙 , isIdentity)
-- Lemma 9.1.4 in [HoTT]
id-to-iso : (A B : Object) → A ≡ B → A ≅ B
@ -102,9 +102,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
open Univalence ℂ public
field
isAssociative : IsAssociative
ident : IsIdentity 𝟙
isIdentity : IsIdentity 𝟙
arrowIsSet : ArrowsAreSets
univalent : Univalent ident
univalent : Univalent isIdentity
-- `IsCategory` is a mere proposition.
module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
@ -142,14 +142,14 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
open Cubical.NType.Properties
geq : g ≡ g'
geq = begin
g ≡⟨ sym (fst ident) ⟩
g ≡⟨ sym (fst isIdentity) ⟩
g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
g ∘ (f ∘ g') ≡⟨ isAssociative ⟩
(g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
𝟙 ∘ g' ≡⟨ snd ident ⟩
𝟙 ∘ g' ≡⟨ snd isIdentity ⟩
g' ∎
propUnivalent : isProp (Univalent ident)
propUnivalent : isProp (Univalent isIdentity)
propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i
private
@ -162,27 +162,27 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
-- projections of `IsCategory` - I've arbitrarily chosed to use this
-- result from `x : IsCategory C`. I don't know which (if any) possibly
-- adverse effects this may have.
ident : (λ _ → IsIdentity 𝟙) [ X.ident ≡ Y.ident ]
ident = propIsIdentity x X.ident Y.ident
isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
isIdentity = propIsIdentity x X.isIdentity Y.isIdentity
done : x ≡ y
U : ∀ {a : IsIdentity 𝟙}
→ (λ _ → IsIdentity 𝟙) [ X.ident ≡ a ]
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
→ (b : Univalent a)
→ Set _
U eqwal bbb =
(λ i → Univalent (eqwal i))
[ X.univalent ≡ bbb ]
P : (y : IsIdentity 𝟙)
→ (λ _ → IsIdentity 𝟙) [ X.ident ≡ y ] → Set _
→ (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
P y eq = ∀ (b' : Univalent y) → U eq b'
helper : ∀ (b' : Univalent X.ident)
→ (λ _ → Univalent X.ident) [ X.univalent ≡ b' ]
helper : ∀ (b' : Univalent X.isIdentity)
→ (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
helper univ = propUnivalent x X.univalent univ
foo = pathJ P helper Y.ident ident
eqUni : U ident Y.univalent
foo = pathJ P helper Y.isIdentity isIdentity
eqUni : U isIdentity Y.univalent
eqUni = foo Y.univalent
IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
IC.ident (done i) = ident i
IC.isIdentity (done i) = isIdentity i
IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
IC.univalent (done i) = eqUni i
@ -217,7 +217,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
OpIsCategory : IsCategory OpRaw
IsCategory.isAssociative OpIsCategory = sym isAssociative
IsCategory.ident OpIsCategory = swap ident
IsCategory.isIdentity OpIsCategory = swap isIdentity
IsCategory.arrowIsSet OpIsCategory = arrowIsSet
IsCategory.univalent OpIsCategory = {!!}
@ -243,7 +243,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
module IsCat = IsCategory (ℂ .isCategory)
rawIsCat : (i : I) → IsCategory (rawOp i)
isAssociative (rawIsCat i) = IsCat.isAssociative
ident (rawIsCat i) = IsCat.ident
isIdentity (rawIsCat i) = IsCat.isIdentity
arrowIsSet (rawIsCat i) = IsCat.arrowIsSet
univalent (rawIsCat i) = IsCat.univalent

12
src/Cat/Category/Functor.agda
View file

@ -33,7 +33,7 @@ module _ {ℓc ℓc' ℓd ℓd'}
record IsFunctor (F : RawFunctor) : 𝓤 where
open RawFunctor F public
field
ident : IsIdentity
isIdentity : IsIdentity
distrib : IsDistributive
record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
@ -55,7 +55,7 @@ module _
propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record
{ ident = 𝔻.arrowIsSet _ _ isF0.ident isF1.ident i
{ isIdentity = 𝔻.arrowIsSet _ _ isF0.isIdentity isF1.isIdentity i
; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
}
where
@ -116,10 +116,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
instance
isFunctor' : IsFunctor A C _∘fr_
isFunctor' = record
{ ident = begin
{ isIdentity = begin
(F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (ident G)⟩
F→ (𝟙 B) ≡⟨ ident F ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩
F→ (𝟙 B) ≡⟨ isIdentity F ⟩
𝟙 C ∎
; distrib = dist
}
@ -135,7 +135,7 @@ identity = record
; func→ = λ x → x
}
; isFunctor = record
{ ident = refl
{ isIdentity = refl
; distrib = refl
}
}

14
src/Cat/Category/Properties.agda
View file

@ -17,25 +17,25 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object
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₀ ≡⟨ sym (proj₁ isIdentity) ⟩
g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩
(g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩
g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩
g₁ ∘ 𝟙 ≡⟨ proj₁ ident ⟩
g₁ ∘ 𝟙 ≡⟨ proj₁ isIdentity ⟩
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₀ ≡⟨ sym (proj₂ isIdentity) ⟩
𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
(f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
𝟙 ∘ g₁ ≡⟨ proj₂ ident ⟩
𝟙 ∘ g₁ ≡⟨ proj₂ isIdentity ⟩
g₁ ∎
iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
@ -70,7 +70,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
module _ {c : Category.Object ℂ} where
eqTrans : (λ _ → Transformation (prshf c) (prshf c))
[ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂
eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
open import Cubical.NType.Properties
open import Cat.Categories.Fun
@ -78,7 +78,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
:ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
where
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
eq = funExt λ A → funExt λ B → proj₂ ℂ.ident
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢})
yoneda = record
@ -87,7 +87,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
; func→ = :func→:
}
; isFunctor = record
{ ident = :ident:
{ isIdentity = :ident:
; distrib = {!!}
}
}