Mercurial > hg > Members > kono > Proof > category

comparison src/Category/Constructions/Slice.agda @ 1111:73c72679421c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Oct 2023 17:00:17 +0900
parents 45de2b31bf02
children
comparison
equal deleted inserted replaced
1110:45de2b31bf02 1111:73c72679421c
1 {-# OPTIONS --universe-polymorphism #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 module Category.Constructions.Slice where 2 module Category.Constructions.Slice where
3 open import Category 3 open import Category
4 open import Level 4 open import Level
5 open import Relation.Binary 5 open import Relation.Binary
6 open import Relation.Binary.Core 6 open import Relation.Binary.Core
7 7 open import HomReasoning
8 import Relation.Binary.EqReasoning as EqR
9 8
10 record SliceObj {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) (O : Obj C) : Set (c₁ ⊔ c₂) where 9 record SliceObj {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) (O : Obj C) : Set (c₁ ⊔ c₂) where
11 constructor ⟦_⟧ 10 constructor ⟦_⟧
12 field 11 field
13 {X} : Obj C 12 {X} : Obj C
35 f = SliceObj.arrow f′ 34 f = SliceObj.arrow f′
36 g = SliceObj.arrow g′ 35 g = SliceObj.arrow g′
37 h = SliceObj.arrow h′ 36 h = SliceObj.arrow h′
38 module Cat = Category.Category C 37 module Cat = Category.Category C
39 open IsCategory Cat.isCategory 38 open IsCategory Cat.isCategory
40 open Cat 39 open Cat renaming ( _o_ to _*_ )
41 a₁ = _⟶_.arrow φ 40 a₁ = _⟶_.arrow φ
42 a₂ = _⟶_.arrow ψ 41 a₂ = _⟶_.arrow ψ
43 open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (refl to reflex) 42 open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (refl to reflex)
44 open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (sym to symm) 43 open IsEquivalence (Setoid.isEquivalence homsetoid) renaming (sym to symm)
45 open EqR homsetoid 44 open ≈-Reasoning C
46 φ-proof = _⟶_.proof φ 45 φ-proof = _⟶_.proof φ
47 ψ-proof : g ≈ h o a₂ 46 ψ-proof : C [ g ≈ C [ h o a₂ ] ]
48 ψ-proof = _⟶_.proof ψ 47 ψ-proof = _⟶_.proof ψ
49 48
50 _∼_ : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {F G : SliceObj C O} → Rel (F ⟶ G) _ 49 _∼_ : ∀{c₁ c₂ ℓ} {C : Category c₁ c₂ ℓ} {O : Obj C} {F G : SliceObj C O} → Rel (F ⟶ G) _
51 _∼_ {C = C} φ ψ = Category._≈_ C (_⟶_.arrow φ) (_⟶_.arrow ψ) 50 _∼_ {C = C} φ ψ = Category._≈_ C (_⟶_.arrow φ) (_⟶_.arrow ψ)
52 51