Mercurial > hg > Members > kono > Proof > category
diff src/Category/Cone.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 07 Oct 2023 19:43:31 +0900 |
parents | |
children | 5620d4a85069 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Category/Cone.agda Sat Oct 07 19:43:31 2023 +0900 @@ -0,0 +1,65 @@ +{-# OPTIONS --cubical-compatible --irrelevant-projections #-} + +import Category + +module Category.Cone {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where +open Category.Category C +open import Level +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality hiding (isEquivalence) + +record Diagram {c₁′ c₂′ ℓ′} (J : Category.Category c₁′ c₂′ ℓ′) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + type : Category.Functor J C + index : Set c₁′ + index = Category.Category.Obj J + edge : index → index → Set c₂′ + edge = Category.Category.Hom J + +open Diagram + +record Cone {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} (D : Diagram J) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + open Category.Functor (type D) + field + apex : Obj + proj : ∀ i → Hom apex (FObj i) + .isCone : ∀{i j : index D} {α : edge D i j } → proj j ≈ FMap α o proj i + +record _-Cone⟶_ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} (C₁ : Cone D) (C₂ : Cone D) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + -- private + open Cone + field + morphism : Hom (apex C₁) (apex C₂) + .isConeMorphism : ∀ {j} → proj C₁ j ≈ proj C₂ j o morphism + +open Cone +open _-Cone⟶_ + +ConeId : ∀{c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} {C₁ : Cone D} → C₁ -Cone⟶ C₁ +ConeId {C₁ = C₁} = + record { morphism = Id { apex C₁ } ; isConeMorphism = proof } + where + .proof : ∀ {j} → proj C₁ j ≈ proj C₁ j o Id + proof = ≈-sym identityR + where open Category.IsCategory isCategory + open IsEquivalence isEquivalence renaming (sym to ≈-sym) + +open import HomReasoning + +_∘_ : ∀ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} {C₁ C₂ C₃ : Cone D} + → C₂ -Cone⟶ C₃ → C₁ -Cone⟶ C₂ → C₁ -Cone⟶ C₃ +_∘_ {_} {_} {_} {J} {D = D} {C₁} {C₂} {C₃} C₂toC₃ C₁toC₂ = + record { morphism = morph ; isConeMorphism = proof } + where + morph = morphism C₂toC₃ o morphism C₁toC₂ + .proof : {j : index D} → proj C₁ j ≈ proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) + proof {j} = begin + proj C₁ j ≈⟨ isConeMorphism C₁toC₂ ⟩ + proj C₂ j o morphism C₁toC₂ ≈⟨ car (isConeMorphism C₂toC₃) ⟩ + (proj C₃ j o morphism C₂toC₃) o morphism C₁toC₂ ≈↑⟨ assoc ⟩ + proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) ∎ where + open ≈-Reasoning C hiding (_o_ ) + +-- end