Merge pull request #431 from jacquescomeaux/master

Implement IsPullback suggestions

src/Categories/Category/CartesianClosed/Locally.agda

@@ -44,9 +44,9 @@ record Locally : Set (levelOfTerm C) where
     ; isPullback = record
       { commute         = p.commute
       ; universal       = λ {Z} {h i} eq → slicearr {h = p.universal eq} (pullʳ p.p₁∘universal≈h₁ ○ Slice⇒.△ h)
-      ; unique          = λ eq₁ eq₂ → p.unique eq₁ eq₂
       ; p₁∘universal≈h₁ = p.p₁∘universal≈h₁
       ; p₂∘universal≈h₂ = p.p₂∘universal≈h₂
+      ; unique-diagram  = p.unique-diagram
       }
     }
     where open HomReasoning
@@ -57,7 +57,7 @@ record Locally : Set (levelOfTerm C) where
           module f = Slice⇒ f
           module g = Slice⇒ g
           module p = P.Pullback (pullbacks f.h g.h) using (p₁; p₂; commute; universal;
-                                 p₁∘universal≈h₁; p₂∘universal≈h₂; unique)
+                                 p₁∘universal≈h₁; p₂∘universal≈h₂; unique-diagram)
           open MR C
 
           comm : Y.arr ∘ p.p₂ ≈ X.arr ∘ p.p₁

src/Categories/Category/Construction/Elements.agda

@@ -140,13 +140,13 @@ module Alternate-Pullback {C : Category (suc o) o o} (F : Functor C (Sets o)) wh
       ; homomorphism = Functor.homomorphism h₁
       ; F-resp-≈ = Functor.F-resp-≈ h₁
       }
+    ; p₁∘universal≈h₁ = {!!}
+    ; p₂∘universal≈h₂ = {!!}
     ; unique = λ πˡ∘i≃h₁ map∘i≃h₂ → record
       { F⇒G = record { η = λ X → {!!} ; commute = {!!} }
       ; F⇐G = record { η = {!!} ; commute = {!!} }
       ; iso = λ X → record { isoˡ = {!!} ; isoʳ = {!!} }
       }
-    ; p₁∘universal≈h₁ = {!!}
-    ; p₂∘universal≈h₂ = {!!}
     }
     where
     open NaturalTransformation

src/Categories/Category/Extensive/Properties/Distributive.agda

@@ -56,18 +56,20 @@ module Categories.Category.Extensive.Properties.Distributive {o ℓ e} (𝒞 : C
         pb g = record { p₁ = id ⁂ g ; p₂ = π₂ ; isPullback = record
           { commute = π₂∘⁂
           ; universal = λ {_} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩
-          ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (BP.unique (begin 
-              π₁ ∘ i              ≈˘⟨ identityˡ ⟩∘⟨refl ⟩ 
-              ((id ∘ π₁) ∘ i)     ≈˘⟨ pullˡ π₁∘⁂ ⟩
-              (π₁ ∘ (id ⁂ g) ∘ i) ≈⟨ refl⟩∘⟨ H1 ⟩
-              π₁ ∘ h₁             ∎) H2)
           ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → begin
               (id ⁂ g) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
               ⟨ id ∘ π₁ ∘ h₁ , g ∘ h₂ ⟩   ≈⟨ ⟨⟩-congʳ identityˡ ⟩
               ⟨ π₁ ∘ h₁ , g ∘ h₂ ⟩        ≈˘⟨ ⟨⟩-congˡ eq ⟩
               ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩       ≈⟨ g-η ⟩
               h₁                          ∎
           ; p₂∘universal≈h₂ = project₂
+          ; unique-diagram = λ {X} {h₁} {h₂} eq₁ eq₂ → BP.unique′ (begin
+              π₁ ∘ h₁            ≈⟨ pushˡ (introˡ refl) ⟩
+              id ∘ π₁ ∘ h₁       ≈⟨ extendʳ π₁∘⁂  ⟨
+              π₁ ∘ (id ⁂ g) ∘ h₁ ≈⟨ refl⟩∘⟨ eq₁ ⟩
+              π₁ ∘ (id ⁂ g) ∘ h₂ ≈⟨ extendʳ π₁∘⁂  ⟩
+              id ∘ π₁ ∘ h₂       ≈⟨ pullˡ (elimˡ refl) ⟩
+              π₁ ∘ h₂            ∎) eq₂
           } }
 
         -- by the diagram we get the canonical distributivity (iso-)morphism

src/Categories/Category/Instance/Properties/Setoids/Exact.agda

@@ -280,14 +280,14 @@ module _ ℓ where
     { regular   = Setoids-Regular
     ; quotient  = Quotient-Coequalizer
     ; effective = λ {X} E → record
-        { commute   = eqn _ (refl X) (refl X)
-        ; universal = λ { {Z}{h₁}{h₂} → universal E h₁ h₂ }
-        ; unique    = λ {Z}{h₁}{h₂}{u}{eq} eq₁ eq₂ {x} → Relation.relation (R E) u (universal E h₁ h₂ eq)
-            λ { zero {x}      → trans X eq₁ (sym X (x₁≈ eq))
-              ; (nzero _) {x} → trans X eq₂ (sym X (≈x₂ eq))
+        { commute         = eqn _ (refl X) (refl X)
+        ; universal       = λ {Z} {h₁} {h₂} → universal E h₁ h₂
+        ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq }
+        ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq }
+        ; unique-diagram  = λ {Z} {h₁} {h₂} eq₁ eq₂ → Relation.relation (R E) h₁ h₂
+            λ { zero      → eq₁
+              ; (nzero _) → eq₂
               }
-        ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq}
-        ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq}
         }
     }
       where

src/Categories/Category/Instance/Properties/Setoids/Extensive.agda

@@ -3,6 +3,7 @@
 module Categories.Category.Instance.Properties.Setoids.Extensive where
 
 open import Level using (Level)
+open import Data.Empty.Polymorphic using (⊥-elim)
 open import Data.Product using (_,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂; _⊎ₛ_; drop-inj₁; drop-inj₂)
@@ -46,9 +47,9 @@ Setoids-Extensive ℓ = record
            { to = λ z → conflict A B (eq {z})
            ; cong = λ {x} _ → conflict A B (eq {x})
            }
-        ; unique = λ {_} {_} {_} {_} {eq} _ _ {x} → conflict A B (eq {x})
         ; p₁∘universal≈h₁ = λ {_ _ _ eq x} → conflict A B (eq {x})
         ; p₂∘universal≈h₂ = λ {_ _ _ eq y} → conflict A B (eq {y})
+        ; unique-diagram = λ {X} {h} {i} eq₁ eq₂ {x} → ⊥-elim {ℓ} {ℓ} {λ ()} (h ⟨$⟩ x)
         }
    }
      where

src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda

@@ -58,9 +58,9 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
           }
         ; cong = < cong h₁ , cong h₂ >
         }
-      ; unique = λ eq₁ eq₂ → eq₁ , eq₂
       ; p₁∘universal≈h₁ = X.refl
       ; p₂∘universal≈h₂ = Y.refl
+      ; unique-diagram = λ eq₁ eq₂ {_} → eq₁ , eq₂
       }
     }
     where

src/Categories/Category/Slice/Properties.agda

@@ -27,15 +27,28 @@ module _ {A : C.Obj} where
   open C.Equiv
 
   product⇒pullback : ∀ {X Y : Obj} → Product (Slice A) X Y → Pullback C (arr X) (arr Y)
-  product⇒pullback p = record
+  product⇒pullback {X} p = record
     { p₁              = h π₁
     ; p₂              = h π₂
     ; isPullback = record
       { commute         = △ π₁ ○ ⟺ (△ π₂)
       ; universal       = λ eq → h ⟨ slicearr eq , slicearr refl ⟩
-      ; unique          = λ {_ _ _ _ eq} eq′ eq″ → ⟺ (unique {h = slicearr (pushˡ (⟺ (△ π₁)) ○ C.∘-resp-≈ʳ eq′ ○ eq)} eq′ eq″)
       ; p₁∘universal≈h₁ = project₁
       ; p₂∘universal≈h₂ = project₂
+      ; unique-diagram  = λ {D j i} eq₁ eq₂ →
+          let D′ : SliceObj A
+              D′ = sliceobj (arr A×B C.∘ i)
+              arr∘j≈arr∘i : arr A×B C.∘ j C.≈ arr A×B C.∘ i
+              arr∘j≈arr∘i = begin
+                arr A×B C.∘ j        ≈⟨ pushˡ (⟺ (△ π₁)) ⟩
+                arr X C.∘ h π₁ C.∘ j ≈⟨ refl⟩∘⟨ eq₁ ⟩
+                arr X C.∘ h π₁ C.∘ i ≈⟨ pullˡ (△ π₁) ⟩
+                arr A×B C.∘ i        ∎
+              j′ : D′ ⇒ A×B
+              j′ = slicearr {h = j} arr∘j≈arr∘i
+              i′ : D′ ⇒ A×B
+              i′ = slicearr {h = i} refl
+          in unique′ {h = j′} {i = i′} eq₁ eq₂
       }
     }
     where open Product (Slice A) p

src/Categories/Diagram/Duality.agda

@@ -80,9 +80,9 @@ coPullback⇒Pushout p = record
   ; i₂              = p₂
   ; commute         = commute
   ; universal       = universal
-  ; unique          = unique
   ; universal∘i₁≈h₁ = p₁∘universal≈h₁
   ; universal∘i₂≈h₂ = p₂∘universal≈h₂
+  ; unique-diagram  = unique-diagram
   }
   where open Pullback p
 
@@ -93,9 +93,9 @@ Pushout⇒coPullback p = record
   ; isPullback = record
     { commute         = commute
     ; universal       = universal
-    ; unique          = unique
     ; p₁∘universal≈h₁ = universal∘i₁≈h₁
     ; p₂∘universal≈h₂ = universal∘i₂≈h₂
+    ; unique-diagram  = unique-diagram
     }
   }
   where open Pushout p

src/Categories/Diagram/Pullback.agda

@@ -24,16 +24,21 @@ private
 -- Proof that a given square is a pullback
 record IsPullback {P : Obj} (p₁ : P ⇒ X) (p₂ : P ⇒ Y) (f : X ⇒ Z) (g : Y ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
   field
-    commute   : f ∘ p₁ ≈ g ∘ p₂
-    universal : ∀ {h₁ : A ⇒ X} {h₂ : A ⇒ Y} → f ∘ h₁ ≈ g ∘ h₂ → A ⇒ P
-    unique    : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
-                  p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ →
-                  i ≈ universal eq
-
-    p₁∘universal≈h₁  : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
-                         p₁ ∘ universal eq ≈ h₁
-    p₂∘universal≈h₂  : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
-                         p₂ ∘ universal eq ≈ h₂
+    commute         : f ∘ p₁ ≈ g ∘ p₂
+    universal       : ∀ {h₁ : A ⇒ X} {h₂ : A ⇒ Y} → f ∘ h₁ ≈ g ∘ h₂ → A ⇒ P
+    p₁∘universal≈h₁ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
+                        p₁ ∘ universal eq ≈ h₁
+    p₂∘universal≈h₂ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} →
+                        p₂ ∘ universal eq ≈ h₂
+    unique-diagram  : p₁ ∘ h ≈ p₁ ∘ i →
+                      p₂ ∘ h ≈ p₂ ∘ i →
+                      h ≈ i
+
+  unique : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} → p₁ ∘ i ≈ h₁ → p₂ ∘ i ≈ h₂ → i ≈ universal eq
+  unique p₁∘i≈h₁ p₂∘i≈h₂ =
+    unique-diagram
+      (p₁∘i≈h₁ ○ ⟺ p₁∘universal≈h₁)
+      (p₂∘i≈h₂ ○ ⟺ p₂∘universal≈h₂)
 
   unique′ : (eq eq′ : f ∘ h₁ ≈ g ∘ h₂) → universal eq ≈ universal eq′
   unique′ eq eq′ = unique p₁∘universal≈h₁ p₂∘universal≈h₂
@@ -44,16 +49,6 @@ record IsPullback {P : Obj} (p₁ : P ⇒ X) (p₂ : P ⇒ Y) (f : X ⇒ Z) (g :
   universal-resp-≈ : ∀ {eq : f ∘ h₁ ≈ g ∘ h₂} {eq′ : f ∘ i₁ ≈ g ∘ i₂} → h₁ ≈ i₁ → h₂ ≈ i₂ → universal eq ≈ universal eq′
   universal-resp-≈ h₁≈i₁ h₂≈i₂ = unique (p₁∘universal≈h₁ ○ h₁≈i₁) (p₂∘universal≈h₂ ○ h₂≈i₂)
 
-  unique-diagram : p₁ ∘ h ≈ p₁ ∘ i →
-                   p₂ ∘ h ≈ p₂ ∘ i →
-                   h ≈ i
-  unique-diagram {h = h} {i = i} eq₁ eq₂ = begin
-    h            ≈⟨ unique eq₁ eq₂ ⟩
-    universal eq ≈˘⟨ unique refl refl ⟩
-    i            ∎
-    where eq = extendʳ commute
-
-
 -- Pullback of two arrows with a common codomain
 record Pullback (f : X ⇒ Z) (g : Y ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
   field
@@ -95,9 +90,9 @@ swap p = record
   ; isPullback = record
     { commute          = ⟺ commute
     ; universal       = universal ● ⟺
-    ; unique          = flip unique
     ; p₁∘universal≈h₁ = p₂∘universal≈h₂
     ; p₂∘universal≈h₂ = p₁∘universal≈h₁
+    ; unique-diagram  = flip unique-diagram
     }
   }
   where open Pullback p
@@ -107,16 +102,18 @@ glue {h = h} p q = record
   { p₁              = q.p₁
   ; p₂              = p.p₂ ∘ q.p₂
   ; isPullback = record
-    { commute        = glue-square p.commute q.commute
+    { commute         = glue-square p.commute q.commute
     ; universal       = λ eq → q.universal (⟺ (p.p₁∘universal≈h₁ {eq = sym-assoc ○ eq}))
-    ; unique          = λ {_ h₁ h₂ i} eq eq′ →
-      q.unique eq (p.unique (begin
-        p.p₁ ∘ q.p₂ ∘ i ≈˘⟨ extendʳ q.commute ⟩
-        h ∘ q.p₁ ∘ i    ≈⟨ refl⟩∘⟨ eq ⟩
-        h ∘ h₁          ∎)
-                            (sym-assoc ○ eq′))
     ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁
     ; p₂∘universal≈h₂ = assoc ○ ∘-resp-≈ʳ q.p₂∘universal≈h₂ ○ p.p₂∘universal≈h₂
+    ; unique-diagram  = λ {_ j i} eq₁ eq₂ →
+        let eq′ : p.p₁ ∘ q.p₂ ∘ j ≈ p.p₁ ∘ q.p₂ ∘ i
+            eq′ = begin
+              p.p₁ ∘ q.p₂ ∘ j ≈⟨ extendʳ q.commute ⟨
+              h ∘ q.p₁ ∘ j    ≈⟨ refl⟩∘⟨ eq₁ ⟩
+              h ∘ q.p₁ ∘ i    ≈⟨ extendʳ q.commute ⟩
+              p.p₁ ∘ q.p₂ ∘ i ∎
+        in q.unique-diagram eq₁ (p.unique-diagram eq′ (sym-assoc ○ eq₂ ○ assoc))
     }
   }
   where module p = Pullback p
@@ -127,19 +124,23 @@ unglue {f = f} {g = g} {h = h} p q = record
   { p₁              = q.p₁
   ; p₂              = p₂′
   ; isPullback = record
-    { commute        = ⟺ p.p₁∘universal≈h₁
+    { commute         = ⟺ p.p₁∘universal≈h₁
     ; universal       = λ {_ h₁ h₂} eq → q.universal $ begin
       (f ∘ h) ∘ h₁      ≈⟨ pullʳ eq ⟩
       f ∘ p.p₁ ∘ h₂     ≈⟨ extendʳ p.commute ⟩
       g ∘ p.p₂ ∘ h₂     ∎
-    ; unique          = λ {_ h₁ h₂ i} eq eq′ → q.unique eq $ begin
-    q.p₂ ∘ i            ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩
-    p.p₂ ∘ p₂′ ∘ i      ≈⟨ refl⟩∘⟨ eq′ ⟩
-    p.p₂ ∘ h₂           ∎
     ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁
     ; p₂∘universal≈h₂ = λ {_ _ _ eq} →
       p.unique-diagram ((pullˡ p.p₁∘universal≈h₁) ○ pullʳ q.p₁∘universal≈h₁ ○ eq)
                        (pullˡ p.p₂∘universal≈h₂ ○ q.p₂∘universal≈h₂)
+    ; unique-diagram  = λ {_ j i} eq₁ eq₂ →
+        let eq′ : q.p₂ ∘ j ≈ q.p₂ ∘ i
+            eq′ = begin
+              q.p₂ ∘ j       ≈⟨ pushˡ (⟺ p.p₂∘universal≈h₂) ⟩
+              p.p₂ ∘ p₂′ ∘ j ≈⟨ refl⟩∘⟨ eq₂ ⟩
+              p.p₂ ∘ p₂′ ∘ i ≈⟨ pullˡ p.p₂∘universal≈h₂ ⟩
+              q.p₂ ∘ i ∎
+        in q.unique-diagram eq₁ eq′
     }
   }
   where module p = Pullback p
@@ -159,9 +160,10 @@ Product×Equalizer⇒Pullback {f = f} {g = g} p e = record
       f ∘ h₁                ≈⟨ eq ⟩
       g ∘ h₂                ≈˘⟨ pullʳ project₂ ⟩
       (g ∘ π₂) ∘ ⟨ h₁ , h₂ ⟩ ∎
-    ; unique          = λ eq eq′ → e.unique (p.unique (sym-assoc ○ eq) (sym-assoc ○ eq′))
     ; p₁∘universal≈h₁ = pullʳ (⟺ e.universal) ○ project₁
     ; p₂∘universal≈h₂ = pullʳ (⟺ e.universal) ○ project₂
+    ; unique-diagram  = λ eq₁ eq₂ →
+      e.unique-diagram (p.unique′ (sym-assoc ○ eq₁ ○ assoc) (sym-assoc ○ eq₂ ○ assoc))
     }
   }
   where module p = Product p
@@ -203,9 +205,9 @@ module _ (p : Pullback f g) where
     ; isPullback = record
       { commute         = ∘-resp-≈ˡ eq ○ commute ○ ⟺ (∘-resp-≈ˡ eq′)
       ; universal       = λ eq″ → universal (∘-resp-≈ˡ (⟺ eq) ○ eq″ ○ ∘-resp-≈ˡ eq′)
-      ; unique          = unique
       ; p₁∘universal≈h₁ = p₁∘universal≈h₁
       ; p₂∘universal≈h₂ = p₂∘universal≈h₂
+      ; unique-diagram  = unique-diagram
       }
     }