wip: Day convolution

src/1Lab/Extensionality.agda

@@ -149,12 +149,30 @@ Extensional-Π ⦃ sb ⦄ .reflᵉ f x = reflᵉ sb (f x)
 Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path h = funext λ i → sb .idsᵉ .to-path (h i)
 Extensional-Π ⦃ sb ⦄ .idsᵉ .to-path-over h = funextP λ i → sb .idsᵉ .to-path-over (h i)
 
+Extensional-Π'
+  : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'}
+  → ⦃ sb : ∀ {x} → Extensional (B x) ℓr ⦄
+  → Extensional ({x : A} → B x) (ℓ ⊔ ℓr)
+Extensional-Π' ⦃ sb ⦄ .Pathᵉ f g = ∀ {x} → Pathᵉ sb (f {x}) (g {x})
+Extensional-Π' ⦃ sb ⦄ .reflᵉ f = reflᵉ sb f
+Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path h i {x} = sb .idsᵉ .to-path (h {x}) i
+Extensional-Π' ⦃ sb ⦄ .idsᵉ .to-path-over h i {x} = sb .idsᵉ .to-path-over (h {x}) i
+
 Extensional-→
   : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
   → ⦃ sb : Extensional B ℓr ⦄
   → Extensional (A → B) (ℓ ⊔ ℓr)
 Extensional-→ ⦃ sb ⦄ = Extensional-Π ⦃ λ {_} → sb ⦄
 
+Extensional-uncurry
+  : ∀ {ℓ ℓ' ℓ'' ℓr} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''}
+  → ⦃ sb : Extensional ((x : A) → B x → C) ℓr ⦄
+  → Extensional (Σ A B → C) ℓr
+Extensional-uncurry ⦃ sb ⦄ .Pathᵉ f g = sb .Pathᵉ (curry f) (curry g)
+Extensional-uncurry ⦃ sb ⦄ .reflᵉ f = sb .reflᵉ (curry f)
+Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path h i (a , b) = sb .idsᵉ .to-path h i a b
+Extensional-uncurry ⦃ sb = sb ⦄ .idsᵉ .to-path-over h = sb .idsᵉ .to-path-over h
+
 Extensional-×
   : ∀ {ℓ ℓ' ℓr ℓs} {A : Type ℓ} {B : Type ℓ'}
   → ⦃ sa : Extensional A ℓr ⦄
@@ -175,11 +193,21 @@ instance
     → Extensionality (A → B)
   extensionality-fun = record { lemma = quote Extensional-→ }
 
+  extensionality-uncurry
+    : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : Type ℓ''}
+    → Extensionality (Σ A B → C)
+  extensionality-uncurry = record { lemma = quote Extensional-uncurry }
+
   extensionality-Π
     : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
     → Extensionality ((x : A) → B x)
   extensionality-Π = record { lemma = quote Extensional-Π }
 
+  extensionality-Π'
+    : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
+    → Extensionality ({x : A} → B x)
+  extensionality-Π' = record { lemma = quote Extensional-Π' }
+
   extensionality-×
     : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
     → Extensionality (A × B)

src/1Lab/Underlying.agda

@@ -127,3 +127,10 @@ instance
   Funlike-Fun = record
     { _#_ = _$_
     }
+
+-- Generalised "sections" (e.g. of a presheaf) notation.
+_ʻ_
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''}
+  → ⦃ _ : Funlike F ⦄ {a : A} {b : B} ⦃ _ : Underlying ⌞ b ⌟ ⦄
+  → F a b → ⌞ a ⌟ → Type _
+F ʻ x = ⌞ F # x ⌟

src/Algebra/Group/Ab/Abelianisation.lagda.md

@@ -222,5 +222,5 @@ make-free-abelian {ℓ} = go where
   go .universal f .preserves .is-group-hom.pres-⋆ =
     Coeq-elim-prop₂ (λ _ _ → hlevel!) λ _ _ → f .preserves .is-group-hom.pres-⋆ _ _
   go .commutes f = trivial!
-  go .unique p = ext (Coeq-elim-prop (λ _ → hlevel!) (λ x → p #ₚ x))
+  go .unique p = ext (p #ₚ_)
 ```

src/Algebra/Group/Subgroup.lagda.md

@@ -578,8 +578,8 @@ predicate $\rm{inc}(x) = \rm{inc}(0)$ recovers the subgroup $H$; And
     from .hom (x , p) = x , quot (subst (_∈ H) (sym idr ∙ ap (_ ⋆_) (sym inv-unit)) p)
     from .preserves .is-group-hom.pres-⋆ _ _ = Σ-prop-path (λ _ → squash _ _) refl
 
-    il = ext λ x → Σ-prop-path (λ _ → H _ .is-tr) refl
-    ir = ext λ x → Σ-prop-path (λ _ → squash _ _) refl
+    il = ext λ x x∈H → Σ-prop-path! refl
+    ir = ext λ x x∈H → Σ-prop-path! refl
 ```
 
 To show that these are equal as subgroups of $G$, we must show that the

src/Cat/Base.lagda.md

@@ -5,6 +5,7 @@ open import 1Lab.Reflection.Record
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel.Universe
 open import 1Lab.Extensionality
+open import 1Lab.Underlying
 open import 1Lab.Rewrite
 open import 1Lab.HLevel
 open import 1Lab.Equiv
@@ -605,5 +606,11 @@ instance
     → Extensionality (F => G)
   extensionality-natural-transformation = record
     { lemma = quote Extensional-natural-transformation }
+
+  Underlying-Precategory : ∀ {o ℓ} → Underlying (Precategory o ℓ)
+  Underlying-Precategory = record { ⌞_⌟ = Precategory.Ob }
+
+  Funlike-Functor : ∀ {o ℓ o' ℓ'} → Funlike (Functor {o} {ℓ} {o'} {ℓ'})
+  Funlike-Functor = record { _#_ = Functor.F₀ }
 ```
 -->

src/Cat/CartesianClosed/Instances/PSh.agda

@@ -78,7 +78,7 @@ module _ {o ℓ κ} {C : Precategory o ℓ} where
     pb .p₁ .is-natural _ _ _ = refl
     pb .p₂ .η x (a , b , _) = b
     pb .p₂ .is-natural _ _ _ = refl
-    pb .has-is-pb .square = ext λ _ (_ , _ , p) → p
+    pb .has-is-pb .square = ext λ _ _ _ p → p
     pb .has-is-pb .universal path .η idx arg = _ , _ , (path ηₚ idx $ₚ arg)
     pb .has-is-pb .universal {p₁' = p₁'} {p₂'} path .is-natural x y f =
       funext λ x → pb-path (happly (p₁' .is-natural _ _ _) _) (happly (p₂' .is-natural _ _ _) _)
@@ -197,9 +197,9 @@ module _ {κ} {C : Precategory κ κ} where
         F .F₁ f nt .η i (g , x) = nt .η i (f C.∘ g , x)
         F .F₁ f nt .is-natural x y g = funext λ o →
           ap (nt .η y) (Σ-pathp (C.assoc _ _ _) refl) ∙ happly (nt .is-natural _ _ _) _
-        F .F-id = ext λ f i (g , x) →
+        F .F-id = ext λ f i g x →
           ap (f .η i) (Σ-pathp (C.idl _) refl)
-        F .F-∘ f g = ext λ h i (j , x) →
+        F .F-∘ f g = ext λ h i j x →
           ap (h .η i) (Σ-pathp (sym (C.assoc _ _ _)) refl)
 
       func : Functor (PSh κ C) (PSh κ C)
@@ -217,13 +217,13 @@ module _ {κ} {C : Precategory κ κ} where
           funext λ _ → Σ-pathp (happly (x .F-∘ _ _) _) refl
       adj .unit .η x .is-natural _ _ _ = funext λ _ → Nat-path λ _ → funext λ _ →
         Σ-pathp (sym (happly (x .F-∘ _ _) _)) refl
-      adj .unit .is-natural x y f = ext λ _ _ _ _ → sym (f .is-natural _ _ _ $ₚ _) , refl
+      adj .unit .is-natural x y f = ext λ _ _ _ _ _ → sym (f .is-natural _ _ _ $ₚ _) , refl
       adj .counit .η _ .η _ x = x .fst .η _ (C.id , x .snd)
       adj .counit .η _ .is-natural x y f = funext λ h →
         ap (h .fst .η _) (Σ-pathp C.id-comm refl) ∙ happly (h .fst .is-natural _ _ _) _
       adj .counit .is-natural x y f = Nat-path λ x → refl
-      adj .zig {A} = ext λ x _ → happly (F-id A) _ , refl
-      adj .zag {A} = ext λ _ x i (f , g) j → x .η i (C.idr f j , g)
+      adj .zig {A} = ext λ x _ _ → happly (F-id A) _ , refl
+      adj .zag {A} = ext λ _ x i f g j → x .η i (C.idr f j , g)
 
     cc : Cartesian-closed (PSh κ C) (PSh-products {C = C}) (PSh-terminal {C = C})
     cc = product-adjoint→cartesian-closed (PSh κ C)

src/Cat/Diagram/Coend/Sets.lagda.md

@@ -75,7 +75,6 @@ taken the right coequaliser.
 ```agda
   Set-coend : Coend F
   Set-coend = coend where
-
     universal-cowedge : Cowedge F
     universal-cowedge .nadir = el! (Coeq dimapl dimapr)
     universal-cowedge .ψ X Fxx = inc (X , Fxx)
@@ -88,15 +87,16 @@ project out the bundled up object from the coend and feed that
 to the family associated to the cowedge `W`.
 
 ```agda
+    factoring : (W : Cowedge F) → Coeq dimapl dimapr → ⌞ W .nadir ⌟
+    factoring W (inc (o , x)) = W .ψ o x
+    factoring W (glue (X , Y , f , Fxy) i) = W .extranatural f i Fxy
+    factoring W (squash x y p q i j) = W .nadir .is-tr (factoring W x) (factoring W y) (λ i → factoring W (p i)) (λ i → factoring W (q i)) i j
+
     coend : Coend F
     coend .cowedge = universal-cowedge
-    coend .factor W =
-      Coeq-rec hlevel! (λ ∫F → W .ψ (∫F .fst) (∫F .snd)) λ where
-        (X , Y , f , Fxy) → happly (W .extranatural f) Fxy
+    coend .factor W = factoring W
     coend .commutes = refl
-    coend .unique {W = W} p =
-      funext $ Coeq-elim hlevel! (λ ∫F → happly p (∫F .snd)) λ where
-        (X , Y , f , Fxy) → is-set→squarep (λ _ _ → is-tr (W .nadir)) _ _ _ _
+    coend .unique {W = W} p = ext λ X x → p #ₚ x
 ```
 
 This construction is actually functorial! Given any functor
@@ -118,14 +118,6 @@ module _ {o ℓ} {𝒞 : Precategory o ℓ} where
         (ap (λ ϕ → inc (X , ϕ)) $ happly (α .is-natural (X , Y) (X , X) (id , f)) Fxy) ··
         glue (X , Y , f , α .η (X , Y) Fxy) ··
         (sym $ ap (λ ϕ → inc (Y , ϕ)) $ happly (α .is-natural (X , Y) (Y , Y) (f , id)) Fxy)
-  Coends .F-id =
-    funext $ Coeq-elim
-      (λ _ → hlevel!)
-      (λ _ → refl)
-      (λ _ → is-set→squarep (λ _ _ → squash) _ _ _ _)
-  Coends .F-∘ f g =
-    funext $ Coeq-elim
-      (λ _ → hlevel!)
-      (λ _ → refl)
-      (λ _ → is-set→squarep (λ _ _ → squash) _ _ _ _)
+  Coends .F-id = trivial!
+  Coends .F-∘ f g = trivial!
 ```

src/Cat/Displayed/Doctrine/Logic.lagda.md

@@ -6,7 +6,7 @@ open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
 open import Cat.Diagram.Product
 open import Cat.Displayed.Base
-open import Cat.Prelude
+open import Cat.Prelude hiding (_ʻ_)
 
 import Cat.Displayed.Reasoning as Disp
 import Cat.Reasoning as Cat

src/Cat/Instances/Sets/CartesianClosed.lagda.md

@@ -52,9 +52,9 @@ module _ {A B : Set ℓ} (func : ∣ A ∣ → ∣ B ∣) where
 
 <!--
 ```agda
-  Sets-Π .F-id = ext λ x → Σ-pathp refl
+  Sets-Π .F-id = ext λ x y → Σ-pathp refl
     (funext λ x → Σ-pathp refl (A .is-tr _ _ _ _))
-  Sets-Π .F-∘ f g = ext λ x → Σ-pathp refl
+  Sets-Π .F-∘ f g = ext λ x y → Σ-pathp refl
     (funext λ x → Σ-pathp refl (A .is-tr _ _ _ _))
 ```
 -->

src/Cat/Instances/Slice.lagda.md

@@ -567,11 +567,7 @@ dependent function is automatically a natural transformation.
 <!--
 ```agda
     linv : is-left-inverse (F₁ Total-space) from
-    linv x = ext λ y → Σ-path (sym (happly (x .commutes) _))
-      ( sym (transport-∙ (ap (∣_∣ ⊙ G .F₀) (happly (x .commutes) y))
-                    (sym (ap (∣_∣ ⊙ G .F₀) (happly (x .commutes) y))) _)
-      ·· ap₂ transport (∙-invr (ap (∣_∣ ⊙ G .F₀) (happly (x .commutes) y))) refl
-      ·· transport-refl _)
+    linv x = ext λ y s → Σ-pathp (sym (x .commutes $ₚ _)) (to-pathp⁻ refl)
 ```
 -->
 

src/Cat/Instances/Slice/Presheaf.lagda.md

@@ -153,7 +153,7 @@ without comment.
 
     rinv : is-right-inverse inv (F₁ slice→total)
     rinv nt = ext λ where
-      o (z , p) → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _)
+      o z p → Σ-prop-path (λ _ → P.₀ _ .is-tr _ _)
         (λ i → nt .η (elem (o .ob) (p i)) (z , (λ j → p (i ∧ j))) .fst)
 
     linv : is-left-inverse inv (F₁ slice→total)