Mercurial > hg > Members > kono > Proof > category

comparison src/Category/Cone.agda @ 1110:45de2b31bf02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1109:71049ed05151 1110:45de2b31bf02
1 {-# OPTIONS --cubical-compatible --irrelevant-projections #-}
2
3 import Category
4
5 module Category.Cone {c₁ c₂ ℓ} (C : Category.Category c₁ c₂ ℓ) where
6 open Category.Category C
7 open import Level
8 open import Relation.Binary
9 open import Relation.Binary.Core
10 open import Relation.Binary.PropositionalEquality hiding (isEquivalence)
11
12 record Diagram {c₁′ c₂′ ℓ′} (J : Category.Category c₁′ c₂′ ℓ′) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
13 field
14 type : Category.Functor J C
15 index : Set c₁′
16 index = Category.Category.Obj J
17 edge : index → index → Set c₂′
18 edge = Category.Category.Hom J
19
20 open Diagram
21
22 record Cone {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} (D : Diagram J) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
23 open Category.Functor (type D)
24 field
25 apex : Obj
26 proj : ∀ i → Hom apex (FObj i)
27 .isCone : ∀{i j : index D} {α : edge D i j } → proj j ≈ FMap α o proj i
28
29 record _-Cone⟶_ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} (C₁ : Cone D) (C₂ : Cone D)
30 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
31 -- private
32 open Cone
33 field
34 morphism : Hom (apex C₁) (apex C₂)
35 .isConeMorphism : ∀ {j} → proj C₁ j ≈ proj C₂ j o morphism
36
37 open Cone
38 open _-Cone⟶_
39
40 ConeId : ∀{c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} {C₁ : Cone D} → C₁ -Cone⟶ C₁
41 ConeId {C₁ = C₁} =
42 record { morphism = Id { apex C₁ } ; isConeMorphism = proof }
43 where
44 .proof : ∀ {j} → proj C₁ j ≈ proj C₁ j o Id
45 proof = ≈-sym identityR
46 where open Category.IsCategory isCategory
47 open IsEquivalence isEquivalence renaming (sym to ≈-sym)
48
49 open import HomReasoning
50
51 _∘_ : ∀ {c₁′ c₂′ ℓ′} {J : Category.Category c₁′ c₂′ ℓ′} {D : Diagram J} {C₁ C₂ C₃ : Cone D}
52 → C₂ -Cone⟶ C₃ → C₁ -Cone⟶ C₂ → C₁ -Cone⟶ C₃
53 _∘_ {_} {_} {_} {J} {D = D} {C₁} {C₂} {C₃} C₂toC₃ C₁toC₂ =
54 record { morphism = morph ; isConeMorphism = proof }
55 where
56 morph = morphism C₂toC₃ o morphism C₁toC₂
57 .proof : {j : index D} → proj C₁ j ≈ proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂)
58 proof {j} = begin
59 proj C₁ j ≈⟨ isConeMorphism C₁toC₂ ⟩
60 proj C₂ j o morphism C₁toC₂ ≈⟨ car (isConeMorphism C₂toC₃) ⟩
61 (proj C₃ j o morphism C₂toC₃) o morphism C₁toC₂ ≈↑⟨ assoc ⟩
62 proj C₃ j o (morphism C₂toC₃ o morphism C₁toC₂) ∎ where
63 open ≈-Reasoning C hiding (_o_ )
64
65 -- end