Mercurial > hg > Members > kono > Proof > category

comparison src/Ch0101.agda @ 1124:f683d96fbc93 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2024 22:28:50 +0900
parents
children
comparison
equal deleted inserted replaced
1123:b6ab443f7a43 1124:f683d96fbc93
1 {-# OPTIONS --cubical-compatible --safe #-}
2
3 module Ch0101 where
4 open import Category
5 open import Category.Sets
6 open import Category.Rel
7 open import Level
8 open import Relation.Binary
9 open import Relation.Binary.Core
10
11 GObj : ∀{ℓ} → Set ℓ → RelObj ℓ
12 GObj a = a
13
14 data GMap {ℓ} {A B : Set ℓ} (f : A → B) (x : A) : B → Set (suc ℓ) where
15 Graph : GMap f x (f x)
16
17 GraphFunctor : ∀{ℓ} → Functor (Sets {ℓ}) (Rels {ℓ})
18 GraphFunctor {ℓ} = record { FObj = GObj
19 ; FMap = GMap
20 ; isFunctor = isFunctor
21 }
22 where
23 isFunctor : IsFunctor (Sets {ℓ}) (Rels {ℓ}) GObj GMap
24 isFunctor = record { ≈-cong = ≈-cong
25 ; identity = identity
26 ; distr = distr
27 }
28 where
29 ≈-cong : {A B : Set ℓ} → {φ ψ : A → B} → φ == ψ → GMap φ ≈ GMap ψ
30 ≈-cong {A} {B} {φ} {ψ} eq = exactly (λ g → ?) ?
31 identity : {A : Set ℓ} → GMap (λ x → x) ≈ RelId {A = A}
32 identity {A} = exactly lhs rhs
33 where
34 lhs : {i j : A} → GMap (λ x → x) i j → RelId i j
35 lhs {i} {.i} Graph = ReflRel
36 rhs : {i j : A} → RelId i j -> GMap (λ x → x) i j
37 rhs {i} {.i} ReflRel = Graph
38 distr : {A B C : Set ℓ} {φ : A → B} {ψ : B → C}
39 → (GMap (λ x → ψ ( φ x))) ≈ (GMap ψ ∘ GMap φ)
40 distr {A} {B} {C} {φ} {ψ} = exactly ? ? -- lhs rhs
41 -- where
42 -- lhs : {i : A} {k : C} → GMap (λ x → ψ ( φ x)) ≈ (GMap ψ ∘ GMap φ) i k → (GMap ψ ∘ GMap φ) i k
43 -- lhs {i} .{ψ (φ i)} Graph = Comp {a = Graph} {b = Graph}
44 -- rhs : {i : A} {k : C} → (GMap ψ ∘ GMap φ) i k → GMap (λ x → ψ ( φ x)) i k
45 -- rhs {i} .{ψ (φ i)} (Comp {a = Graph} {Graph}) = Graph
46
47 OpObj : ∀{ℓ} → RelObj ℓ → RelObj ℓ
48 OpObj x = x
49
50 data OpMap {ℓ} {A B : RelObj ℓ} (P : A -Rel⟶ B) (b : B) (a : A) : Set (suc ℓ) where
51 complement : P a b → OpMap P b a
52
53 ComplementFunctor : ∀{ℓ} → Functor (Category.op (Rels {ℓ})) (Rels {ℓ})
54 ComplementFunctor {ℓ} = record { FObj = OpObj
55 ; FMap = OpMap
56 ; isFunctor = isFunctor
57 }
58 where
59 isFunctor : IsFunctor (Category.op (Rels {ℓ})) (Rels {ℓ}) OpObj OpMap
60 isFunctor = record { ≈-cong = ≈-cong
61 ; identity = identity
62 ; distr = distr
63 }
64 where
65 ≈-cong : {A B : Set ℓ} {P Q : B -Rel⟶ A} → P ≈ Q → OpMap P ≈ OpMap Q
66 ≈-cong {A} {B} {P} {Q} (exactly P⇒Q Q⇒P) = exactly lhs rhs
67 where
68 lhs : {i : A} {j : B} → OpMap P i j → OpMap Q i j
69 lhs (complement Pji) = complement (P⇒Q Pji)
70 rhs : {i : A} {j : B} → OpMap Q i j → OpMap P i j
71 rhs (complement Qji) = complement (Q⇒P Qji)
72
73 identity : {A : Set ℓ} → OpMap (RelId {A = A}) ≈ RelId {A = OpObj A}
74 identity {A} = exactly lhs rhs
75 where
76 lhs : {i j : A} → OpMap RelId i j → RelId i j
77 lhs {i} .{i} (complement ReflRel) = ReflRel
78 rhs : {i j : A} → RelId i j → OpMap RelId i j
79 rhs {i} .{i} ReflRel = complement ReflRel
80
81 distr : {A B C : Set ℓ} {P : B -Rel⟶ A} {Q : C -Rel⟶ B} → OpMap (P ∘ Q) ≈ (OpMap Q ∘ OpMap P)
82 distr {A} {B} {C} {P} {Q} = exactly lhs rhs
83 where
84 lhs : {i : A} {k : C} → OpMap (P ∘ Q) i k → (OpMap Q ∘ OpMap P) i k
85 lhs {i} {k} (complement (Comp {a = Pjk} {Qij} ))= Comp {a = complement Qij} {b = complement Pjk}
86 rhs : {i : A} {k : C} → (OpMap Q ∘ OpMap P) i k → OpMap (P ∘ Q) i k
87 rhs {i} {k} (Comp {a = complement Qij} {b = complement Pjk}) = complement (Comp {a = Pjk} {Qij})