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