--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Ch0101.agda	Sun Jul 07 22:28:50 2024 +0900
@@ -0,0 +1,87 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Ch0101 where
+open import Category
+open import Category.Sets
+open import Category.Rel
+open import Level
+open import Relation.Binary
+open import Relation.Binary.Core
+
+GObj : ∀{ℓ} → Set ℓ → RelObj ℓ
+GObj a = a
+
+data GMap {ℓ} {A B : Set ℓ} (f : A → B) (x : A) : B → Set (suc ℓ) where
+  Graph : GMap f x (f x)
+
+GraphFunctor : ∀{ℓ} → Functor (Sets {ℓ}) (Rels {ℓ})
+GraphFunctor {ℓ} = record { FObj = GObj
+                          ; FMap = GMap
+                          ; isFunctor = isFunctor
+                          }
+  where
+    isFunctor : IsFunctor (Sets {ℓ}) (Rels {ℓ}) GObj GMap
+    isFunctor = record { ≈-cong = ≈-cong
+                       ; identity = identity
+                       ; distr = distr
+                       }
+      where
+        ≈-cong : {A B : Set ℓ} → {φ ψ : A →  B} → φ == ψ → GMap φ ≈ GMap ψ
+        ≈-cong {A} {B} {φ} {ψ} eq = exactly (λ g → ?) ?
+        identity : {A : Set ℓ} → GMap (λ x → x) ≈ RelId {A = A}
+        identity {A} = exactly lhs rhs
+          where
+            lhs : {i j : A} → GMap (λ x → x) i j → RelId i j
+            lhs {i} {.i} Graph = ReflRel
+            rhs : {i j : A} → RelId i j -> GMap (λ x → x) i j
+            rhs {i} {.i} ReflRel = Graph
+        distr : {A B C : Set ℓ} {φ : A →  B} {ψ : B →  C}
+              → (GMap (λ x → ψ ( φ x))) ≈ (GMap ψ ∘ GMap φ)
+        distr {A} {B} {C} {φ} {ψ} = exactly ? ? -- lhs rhs
+          -- where
+            -- lhs : {i : A} {k : C} → GMap (λ x → ψ ( φ x)) ≈ (GMap ψ ∘ GMap φ) i k → (GMap ψ ∘ GMap φ) i k
+            -- lhs {i} .{ψ (φ i)} Graph = Comp {a = Graph} {b = Graph}
+            -- rhs : {i : A} {k : C} → (GMap ψ ∘ GMap φ) i k → GMap (λ x → ψ ( φ x)) i k
+            -- rhs {i} .{ψ (φ i)} (Comp {a = Graph} {Graph}) = Graph
+
+OpObj : ∀{ℓ} → RelObj ℓ → RelObj ℓ
+OpObj x = x
+
+data  OpMap {ℓ} {A B : RelObj ℓ} (P : A -Rel⟶ B) (b : B) (a : A) : Set (suc ℓ) where
+  complement : P a b → OpMap P b a
+
+ComplementFunctor : ∀{ℓ} → Functor (Category.op (Rels {ℓ})) (Rels {ℓ})
+ComplementFunctor {ℓ} = record { FObj = OpObj
+                               ; FMap = OpMap
+                               ; isFunctor = isFunctor
+                               }
+  where
+    isFunctor : IsFunctor (Category.op (Rels {ℓ})) (Rels {ℓ}) OpObj OpMap
+    isFunctor = record { ≈-cong = ≈-cong
+                       ; identity = identity
+                       ; distr = distr
+                       }
+      where
+        ≈-cong : {A B : Set ℓ} {P Q : B -Rel⟶ A} → P ≈ Q → OpMap P ≈ OpMap Q
+        ≈-cong {A} {B} {P} {Q} (exactly P⇒Q Q⇒P) = exactly lhs rhs
+          where 
+            lhs : {i : A} {j : B} → OpMap P i j → OpMap Q i j
+            lhs (complement Pji) = complement (P⇒Q Pji)
+            rhs : {i : A} {j : B} → OpMap Q i j → OpMap P i j
+            rhs (complement Qji) = complement (Q⇒P Qji)
+
+        identity : {A : Set ℓ} → OpMap (RelId {A = A}) ≈ RelId {A = OpObj A}
+        identity {A} = exactly lhs rhs
+          where
+            lhs : {i j : A} → OpMap RelId i j → RelId i j
+            lhs {i} .{i} (complement ReflRel) = ReflRel
+            rhs : {i j : A} → RelId i j → OpMap RelId i j
+            rhs {i} .{i} ReflRel = complement ReflRel
+
+        distr : {A B C : Set ℓ} {P : B -Rel⟶ A} {Q : C -Rel⟶ B} → OpMap (P ∘ Q) ≈ (OpMap Q ∘ OpMap P)
+        distr {A} {B} {C} {P} {Q} = exactly lhs rhs
+          where
+            lhs : {i : A} {k : C} → OpMap (P ∘ Q) i k → (OpMap Q ∘ OpMap P) i k
+            lhs {i} {k} (complement (Comp {a = Pjk} {Qij} ))= Comp {a = complement Qij} {b = complement Pjk}
+            rhs : {i : A} {k : C} → (OpMap Q ∘ OpMap P) i k → OpMap (P ∘ Q) i k
+            rhs {i} {k} (Comp {a = complement Qij} {b = complement Pjk}) = complement (Comp {a = Pjk} {Qij})