From f524f9948178ed68112771099615f90bb43fe2d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 15 Nov 2017 20:45:35 +0100 Subject: [PATCH 1/6] Finish proof of left and right identity --- src/Category/Rel.agda | 41 +++++++++++++++++------------------------ 1 file changed, 17 insertions(+), 24 deletions(-) diff --git a/src/Category/Rel.agda b/src/Category/Rel.agda index 2091558..8ac7869 100644 --- a/src/Category/Rel.agda +++ b/src/Category/Rel.agda @@ -67,33 +67,23 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where → (a , b) ∈ S backwards (a' , (a=a' , a'b∈S)) = subst (sym a=a') a'b∈S - isbijective : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x + fwd-bwd : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x -- isbijective x = pathJ (λ y x₁ → (backwards ∘ forwards) x ≡ x) {!!} {!!} {!!} - isbijective x = pathJprop (λ y _ → y) x + fwd-bwd x = pathJprop (λ y _ → y) x - postulate - back-fwd : (x : Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) + bwd-fwd : (x : Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) → (forwards ∘ backwards) x ≡ x - -- back-fwd (a , (p , ab∈S)) - -- = =-ind (λ x y p → {!(forwards ∘ backwards) x ≡ x!}) {!!} {!!} {!!} p - -- = pathJprop (λ y _ → snd (snd y)) ab∈S - -- has type P x refl where P is the first argument -{- + -- bwd-fwd (y , a≡y , z) = ? + bwd-fwd (a' , a≡y , z) = pathJ lem0 lem1 a' a≡y z + where + lem0 = (λ a'' a≡a'' → ∀ a''b∈S → (forwards ∘ backwards) (a'' , a≡a'' , a''b∈S) ≡ (a'' , a≡a'' , a''b∈S)) + lem1 = (λ z₁ → cong (\ z → a , refl , z) (pathJprop (\ y _ → y) z₁)) -module _ {ℓ ℓ'} {A : Set ℓ} {x : A} - (P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where - pathJ : (y : A) → (p : x ≡ y) → P y p - pathJ _ p = transp (λ i → uncurry P (contrSingl p i)) d - - pathJprop : pathJ _ refl ≡ d - pathJprop i = primComp (λ _ → P x refl) i (λ {j (i = i1) → d}) d --} isequiv : isEquiv (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ((a , b) ∈ S) backwards --- isequiv ab∈S = (forwards ab∈S , sym (isbijective ab∈S)) , λ y → fiberhelp y - isequiv y = gradLemma backwards forwards isbijective back-fwd y + isequiv y = gradLemma backwards forwards fwd-bwd bwd-fwd y equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≃ (a , b) ∈ S @@ -113,18 +103,21 @@ module _ {ℓ ℓ'} {A : Set ℓ} {x : A} → (a , b) ∈ S backwards (b' , (ab'∈S , b'=b)) = subst b'=b ab'∈S - isbijective : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x - isbijective x = pathJprop (λ y _ → y) x + bwd-fwd : (x : (a , b) ∈ S) → (backwards ∘ forwards) x ≡ x + bwd-fwd x = pathJprop (λ y _ → y) x fwd-bwd : (x : Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) → (forwards ∘ backwards) x ≡ x - fwd-bwd (b , (ab∈S , refl)) = pathJprop (λ y _ → fst (snd y)) ab∈S + fwd-bwd (b' , (ab'∈S , b'≡b)) = pathJ lem0 lem1 b' (sym b'≡b) ab'∈S + where + lem0 = (λ b'' b≡b'' → (ab''∈S : (a , b'') ∈ S) → (forwards ∘ backwards) (b'' , ab''∈S , sym b≡b'') ≡ (b'' , ab''∈S , sym b≡b'')) + lem1 = (λ ab''∈S → cong (λ φ → b , φ , refl) (pathJprop (λ y _ → y) ab''∈S)) isequiv : isEquiv (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ((a , b) ∈ S) backwards - isequiv ab∈S = gradLemma backwards forwards isbijective fwd-bwd ab∈S + isequiv ab∈S = gradLemma backwards forwards bwd-fwd fwd-bwd ab∈S equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≃ ab ∈ S @@ -153,7 +146,7 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where RepFunctor = record { F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B - ; f = λ { {c' = c'} f g → HomFromArrow {ℂ = {!𝕊et-as-Cat!}} c' g} + ; f = λ { {c' = c'} f g → {!HomFromArrow {ℂ = } c' g!}} ; ident = {!!} ; distrib = {!!} } From fa5d380ee2183c0ca706951427a407f80d401f16 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 15 Nov 2017 21:49:50 +0100 Subject: [PATCH 2/6] Finnish the proof of the category of relations --- src/Category/Rel.agda | 41 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) diff --git a/src/Category/Rel.agda b/src/Category/Rel.agda index 8ac7869..7624da9 100644 --- a/src/Category/Rel.agda +++ b/src/Category/Rel.agda @@ -127,13 +127,52 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where ≡ ab ∈ S ident-r = equivToPath equi +module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset (C × D)} (ad : A × D) where + private + a : A + a = fst ad + d : D + d = snd ad + + Q⊕⟨R⊕S⟩ : Set + Q⊕⟨R⊕S⟩ = Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q + ⟨Q⊕R⟩⊕S : Set + ⟨Q⊕R⟩⊕S = Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q) + + fwd : Q⊕⟨R⊕S⟩ → ⟨Q⊕R⟩⊕S + fwd (c , (b , (ab∈S , bc∈R)) , cd∈Q) = b , (ab∈S , (c , (bc∈R , cd∈Q))) + + bwd : ⟨Q⊕R⟩⊕S → Q⊕⟨R⊕S⟩ + bwd (b , (ab∈S , (c , (bc∈R , cd∈Q)))) = c , (b , ab∈S , bc∈R) , cd∈Q + + fwd-bwd : (x : ⟨Q⊕R⟩⊕S) → (fwd ∘ bwd) x ≡ x + fwd-bwd x = refl + + bwd-fwd : (x : Q⊕⟨R⊕S⟩) → (bwd ∘ fwd) x ≡ x + bwd-fwd x = refl + + isequiv : isEquiv + (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) + (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) + fwd + isequiv = gradLemma fwd bwd fwd-bwd bwd-fwd + + equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) + ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) + equi = fwd , isequiv + + -- assocc : Q + (R + S) ≡ (Q + R) + S + assocc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) + ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) + assocc = equivToPath equi + Rel-as-Cat : Category Rel-as-Cat = record { Object = Set ; Arrow = λ S R → Subset (S × R) ; 𝟙 = λ {S} → Diag S ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} - ; assoc = {!!} + ; assoc = funExt assocc ; ident = funExt ident-l , funExt ident-r } From 6ca9368891f8a4da36753b40efa77ef14c5efd74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 15 Nov 2017 21:51:10 +0100 Subject: [PATCH 3/6] Add the category of sets --- src/Category/Sets.agda | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/Category/Sets.agda diff --git a/src/Category/Sets.agda b/src/Category/Sets.agda new file mode 100644 index 0000000..fb2c332 --- /dev/null +++ b/src/Category/Sets.agda @@ -0,0 +1,34 @@ +module Category.Sets where + +open import Cubical.PathPrelude +open import Agda.Primitive +open import Category + +-- Sets are built-in to Agda. The set of all small sets is called Set. + +Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ +Fun T U = T → U + +Sets : {ℓ : Level} → Category {lsuc ℓ} {ℓ} +Sets {ℓ} = record + { Object = Set ℓ + ; Arrow = λ T U → Fun {ℓ} T U + ; 𝟙 = λ x → x + ; _⊕_ = λ g f x → g ( f x ) + ; assoc = refl + ; ident = funExt (λ x → refl) , funExt (λ x → refl) + } + +module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where + private + C-Obj = Object ℂ + _+_ = Arrow ℂ + + RepFunctor : Functor ℂ Sets + RepFunctor = + record + { F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B + ; f = λ { {c' = c'} f g → {!HomFromArrow {ℂ = } c' g!}} + ; ident = {!!} + ; distrib = {!!} + } From 43cc73c6a8ef6976dfba55ca663452a49335a31a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 15 Nov 2017 21:51:41 +0100 Subject: [PATCH 4/6] Rename the category of relations --- src/Category/Rel.agda | 33 ++------------------------------- 1 file changed, 2 insertions(+), 31 deletions(-) diff --git a/src/Category/Rel.agda b/src/Category/Rel.agda index 7624da9..42ed17e 100644 --- a/src/Category/Rel.agda +++ b/src/Category/Rel.agda @@ -7,21 +7,6 @@ open import Cubical.GradLemma open import Agda.Primitive open import Category --- Sets are built-in to Agda. The set of all small sets is called Set. - -Fun : {ℓ : Level} → ( T U : Set ℓ ) → Set ℓ -Fun T U = T → U - -𝕊et-as-Cat : {ℓ : Level} → Category {lsuc ℓ} {ℓ} -𝕊et-as-Cat {ℓ} = record - { Object = Set ℓ - ; Arrow = λ T U → Fun {ℓ} T U - ; 𝟙 = λ x → x - ; _⊕_ = λ g f x → g ( f x ) - ; assoc = refl - ; ident = funExt (λ x → refl) , funExt (λ x → refl) - } - -- Subsets are predicates over some type. Subset : {ℓ : Level} → ( A : Set ℓ ) → Set (ℓ ⊔ lsuc lzero) Subset A = A → Set @@ -166,8 +151,8 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) assocc = equivToPath equi -Rel-as-Cat : Category -Rel-as-Cat = record +Rel : Category +Rel = record { Object = Set ; Arrow = λ S R → Subset (S × R) ; 𝟙 = λ {S} → Diag S @@ -175,17 +160,3 @@ Rel-as-Cat = record ; assoc = funExt assocc ; ident = funExt ident-l , funExt ident-r } - -module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where - private - C-Obj = Object ℂ - _+_ = Arrow ℂ - - RepFunctor : Functor ℂ 𝕊et-as-Cat - RepFunctor = - record - { F = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B - ; f = λ { {c' = c'} f g → {!HomFromArrow {ℂ = } c' g!}} - ; ident = {!!} - ; distrib = {!!} - } From 11f5b89b103bdaf945cc5a287b32f1ab2aa09903 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 15 Nov 2017 21:59:00 +0100 Subject: [PATCH 5/6] Rename some variables --- src/Category/Rel.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Category/Rel.agda b/src/Category/Rel.agda index 42ed17e..e9bbdc4 100644 --- a/src/Category/Rel.agda +++ b/src/Category/Rel.agda @@ -22,7 +22,7 @@ Subset A = A → Set -- syntax subset P = ⦃ a ∈ A | P a ⦄ -- syntax subset-syntax A (λ a → B) = ⟨ a foo A ∣ B ⟩ --- Membership is function applicatiom. +-- Membership is (dependent) function applicatiom. _∈_ : {ℓ : Level} {A : Set ℓ} → A → Subset A → Set s ∈ S = S s @@ -30,7 +30,7 @@ infixl 45 _∈_ -- The diagnoal of a set is a synonym for equality. Diag : ∀ S → Subset (S × S) -Diag S (s₀ , s₁) = s₀ ≡ s₁ +Diag S (x , y) = x ≡ y -- Diag S = subset (S × S) (λ {(p , q) → p ≡ q}) -- Diag S = ⟨ ? foo ? ∣ ? ⟩ -- Diag S (s₀ , s₁) = ⦃ (s₀ , s₁) ∈ S | s₀ ≡ s₁ ⦄ @@ -147,9 +147,9 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset equi = fwd , isequiv -- assocc : Q + (R + S) ≡ (Q + R) + S - assocc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) + is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) - assocc = equivToPath equi + is-assoc = equivToPath equi Rel : Category Rel = record @@ -157,6 +157,6 @@ Rel = record ; Arrow = λ S R → Subset (S × R) ; 𝟙 = λ {S} → Diag S ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} - ; assoc = funExt assocc + ; assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r } From 1d040e5391d71f27869d6c33c698ce4ca49a42a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 15 Nov 2017 22:56:04 +0100 Subject: [PATCH 6/6] Use bot from stdlib --- src/Category.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Category.agda b/src/Category.agda index ef5c2c4..d1aa814 100644 --- a/src/Category.agda +++ b/src/Category.agda @@ -6,6 +6,7 @@ open import Agda.Primitive open import Data.Unit.Base open import Data.Product open import Cubical.PathPrelude +open import Data.Empty postulate undefined : {ℓ : Level} → {A : Set ℓ} → A @@ -115,8 +116,6 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } w iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso -data ⊥ : Set where - ¬_ : {ℓ : Level} → Set ℓ → Set ℓ ¬ A = A → ⊥