some housekeeping

1lab.agda-lib

@@ -9,3 +9,4 @@ flags:
   --postfix-projections
   -W noUnsupportedIndexedMatch
   --experimental-lazy-instances
+  --quote-metas

src/1Lab/Reflection.lagda.md

@@ -9,7 +9,7 @@ open import Data.String.Show
 open import Data.Bool.Base
 open import Data.List.Base
 open import Data.Dec.Base
-open import Data.Vec.Base
+open import Data.Vec.Base hiding (_++_)
 
 open import Meta.Append
 ```
@@ -394,21 +394,32 @@ extend-context* : ∀ {a} {A : Type a} → Telescope → TC A → TC A
 extend-context* [] a = a
 extend-context* ((nm , tm) ∷ xs) a = extend-context nm tm (extend-context* xs a)
 
+record New-meta : Type where
+  constructor meta
+  field
+    new-meta : Meta
+    new-term : Term
+    ⦃ neu ⦄ : Has-neutrals.neutral auto new-term
+
+new-meta' : Term → TC New-meta
+new-meta' ty = do
+  debugPrint "tactic.meta" 70 [ "new-meta'\n" , termErr ty ]
+  tm@(Term.meta mv _) ← check-type unknown ty
+    where what → do
+      debugPrint "tactic.meta" 70
+        [ "check-type unknown returns\n" , termErr what ]
+      typeError "impossible new-meta'"
+  debugPrint "tactic.meta" 70
+    [ "Created new meta\n  " , termErr tm , "\nof type\n  " , termErr ty ]
+  pure (meta mv tm)
+
 new-meta : Term → TC Term
 new-meta ty = do
   mv ← check-type unknown ty
   debugPrint "tactic.meta" 70
-    [ "Created new meta " , termErr mv , " of type " , termErr ty ]
+    [ "Created new meta\n  " , termErr mv , "\nof type\n  " , termErr ty ]
   pure mv
 
-new-meta' : Term → TC (Meta × Term)
-new-meta' ty = do
-  tm@(meta mv _) ← check-type unknown ty
-    where _ → typeError "impossible new-meta'"
-  debugPrint "tactic.meta" 70
-    [ "Created new meta " , termErr tm , " of type " , termErr tm ]
-  pure (mv , tm)
-
 block-on-meta : ∀ {a} {A : Type a} → Meta → TC A
 block-on-meta m = blockTC (blocker-meta m)
 
@@ -509,12 +520,16 @@ unapply-path' false red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) = d
   pure (just (domain , x , y))
 
 unapply-path' true tm = reduce tm >>= λ where
-  tm@(meta _ _) → do
-    (Tmv , T) ← new-meta' (pi (argN (quoteTerm I)) (abs "i" (def (quote Type) (unknown v∷ []))))
-    l ← new-meta (meta Tmv (quoteTerm i0 v∷ []))
-    r ← new-meta (meta Tmv (quoteTerm i1 v∷ []))
+  tm@(meta _ cx) → do
+    meta Tmv T ← new-meta' $ pi (argN (quoteTerm I))
+      (abs "i" (def (quote Type) (unknown v∷ [])))
+
+    meta lmv l ← new-meta' (T ##ₙ quoteTerm i0)
+    meta rmv r ← new-meta' (T ##ₙ quoteTerm i1)
+
     unify tm (def (quote PathP) (T v∷ l v∷ r v∷ []))
-    traverse wait-for-type (l ∷ r ∷ [])
+    blockTC {A = ⊤} (blocker-all (blocker-meta lmv ∷ blocker-meta rmv ∷ []))
+
     pure (just (T , l , r))
 
   red@(def (quote PathP) (T v∷ l v∷ r v∷ [])) → do

src/1Lab/Reflection/HLevel.agda

@@ -152,7 +152,7 @@ hlevel-proj A want goal = withNormalisation false do
   debugPrint "tactic.hlevel" 30 [ "H-Level: trying projections for term:\n  " , termErr (def head args), "\nwith head symbol ", nameErr head ]
 
   projection ← resetting do
-    (mv , _) ← new-meta' (def (quote hlevel-projection) (argN (lit (name head)) ∷ []))
+    meta mv _ ← new-meta' (def (quote hlevel-projection) (argN (lit (name head)) ∷ []))
     get-instances mv >>= λ where
       [] → typeError
         [ "H-Level: There are no hints for treating the name " , nameErr head , " as a projection.\n"

src/1Lab/Reflection/Marker.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import 1Lab.Reflection
 open import 1Lab.Path
 open import 1Lab.Type
@@ -16,32 +17,41 @@ module 1Lab.Reflection.Marker where
 ⌜ x ⌝ = x
 {-# NOINLINE ⌜_⌝ #-}
 
+-- A placeholder for terms that should be turned into metavariables when
+-- abstracting.
+-- This can be used with apd! to mark terms on which the type of a
+-- marker depends, as long as the path that ¿? replaces can be inferred
+-- from the type of the argument to apd!.
+¿? : ∀ {ℓ} {A : Type ℓ} {x : A} → A
+¿? {x = x} = x
+{-# NOINLINE ¿? #-}
+
 -- Abstract over the marked term(s). All marked terms refer to the same
 -- variable, so e.g.
 --
 --  abstract-marker (quoteTerm (f ⌜ x ⌝ (λ _ → ⌜ x ⌝)))
 --
 -- is (λ e → f e (λ _ → e)). The resulting term is open in precisely one
 -- variable: that variable is what substitutes the marked terms.
-abstract-marker : Term → Maybe Term
-abstract-marker = go 0 where
+abstract-marker : Nat → Term → Maybe Term
+abstract-marker base = go 0 where
   go  : Nat → Term → Maybe Term
   go* : Nat → List (Arg Term) → Maybe (List (Arg Term))
 
-  go k (var j args) = var j' <$> go* k args
-    where
-      j' : Nat
-      j' with j < k
-      ... | false = suc j
-      ... | true = j
+  go k (var j args) = var j' <$> go* k args where
+    j' : Nat
+    j' with j < k
+    ... | false = base + j
+    ... | true = j
   go k (con c args) = con c <$> go* k args
   go k (def f args) with f
   ... | quote ⌜_⌝ = pure (var k [])
-  -- ^ This is the one interesting case. Any application of the marker
+  -- ^ This is the first interesting case. Any application of the marker
   -- gets replaced with the 'k'th variable. Initially k = 0, so this is
   -- the variable bound by the lambda. But as we encounter further
   -- binders, we must increment this, since the marked term gets farther
   -- and farther away in the context.
+  ... | quote ¿? = pure unknown
   ... | x = def f <$> go* k args
   go k (lam v (abs x t)) = lam v ∘ abs x <$> go (suc k) t
   go k (pat-lam cs args) = nothing
@@ -88,9 +98,9 @@ private
   ap-worker : ∀ {ℓ} {A : Type ℓ} (x : A) → Term → TC ⊤
   ap-worker x goal = withNormalisation false do
     `x ← wait-for-type =<< quoteTC x
-    case abstract-marker `x of λ where
+    case abstract-marker 1 `x of λ where
       (just l) → do
-        debugPrint "1lab.marked-ap" 10
+        debugPrint "tactic.marked-ap" 10
           [ "original  " , termErr `x , "\n"
           , "abstracted" , termErr (lam visible (abs "x" l))
           ]
@@ -129,3 +139,93 @@ module _ {ℓ} {A : Type ℓ} {x y : A} {p : x ≡ y} {f : A → (A → A) → A
     r =
       f ⌜ y ⌝ (λ _ → ⌜ y ⌝) ≡˘⟨ ap¡ p ⟩
       f x (λ _ → x)         ∎
+
+private
+  -- In addition to supporting ¿? to mark explicit problematic
+  -- dependencies, we also remove all implicit arguments when
+  -- abstracting over the path.
+  censor  : Term → Term
+  censor* : List (Arg Term) → List (Arg Term)
+
+  censor (var x args)             = var x (censor* args)
+  censor (con c args)             = con c (censor* args)
+  censor (def f args)             = def f (censor* args)
+  censor (lam v (abs n tm))       = lam v (abs n (censor tm))
+  censor (pat-lam cs args)        = pat-lam cs (censor* args)
+  censor (pi (arg i x) (abs n y)) = pi (arg i (censor x)) (abs n (censor y))
+  censor (agda-sort s)            = agda-sort s
+  censor (lit l)                  = lit l
+  censor (meta m args)            = unknown
+  censor unknown                  = unknown
+
+  censor* [] = []
+  censor* (t v∷ ts) = censor t v∷ censor* ts
+  censor* (t h∷ ts) = censor* ts
+  censor* (t i∷ ts) = censor* ts
+
+  macro
+    apd-worker : ∀ {ℓ} {A : Type ℓ} → A → Term → Term → TC ⊤
+    apd-worker endpoint what goal = withNormalisation false do
+      `endpoint ← wait-for-type =<< quoteTC endpoint
+      case abstract-marker 2 (censor `endpoint) of λ where
+        (just l) → do
+          let fn = lam visible (abs "i" (lam visible (abs "x" l)))
+          debugPrint "tactic.marked-ap" 10
+            [ "original  " , termErr `endpoint , "\n"
+            , "abstracted" , termErr fn
+            ]
+          unify goal (def₀ (quote apd) ##ₙ fn ##ₙ what)
+        nothing → typeError [ "apd!: Failed to abstract over marker in term\n  " , termErr `endpoint ]
+
+  -- The entry point for apd! can't use tactic arguments to have the
+  -- elaborator propagate the endpoint; it's just too circular.
+  --
+  -- To prevent a performance blowup from quoting the entire type of the
+  -- goal, we take it apart by unifying against metavariables and
+  -- deferring to a different macro. The second macro application acts
+  -- like a "fence" for the blockTC primitive.
+  apd-wrapper : Bool → Term → Term → TC ⊤
+  apd-wrapper right what goal = do
+    meta Tmv T ← new-meta' $ pi (argN (quoteTerm I))
+      (abs "i" (def (quote Type) (unknown v∷ [])))
+
+    l ← new-meta (T ##ₙ quoteTerm i0)
+    r ← new-meta (T ##ₙ quoteTerm i1)
+
+    g' ← check-type goal (def₀ (quote PathP) ##ₙ T ##ₙ l ##ₙ r)
+
+    unify goal (def₀ (quote apd-worker) ##ₙ (if right then r else l) ##ₙ what)
+
+macro
+  -- Generalised apd. Automatically generates the function to apply to
+  -- by abstracting over any markers in the LEFT ENDPOINT of the path.
+  -- Use with _≡[]⟨_⟩_.
+  apd! : Term → Term → TC ⊤
+  apd! = apd-wrapper false
+
+  -- Generalised apd. Automatically generates the function to apply to
+  -- by abstracting over any markers in the RIGHT ENDPOINT of the path.
+  -- Use with _≡[]˘⟨_⟩_.
+  apd¡ : Term → Term → TC ⊤
+  apd¡ = apd-wrapper true
+
+module
+  _ {ℓ ℓ' ℓ''} {A : Type ℓ} {x y : A} {p : x ≡ y} {B : A → Type ℓ'}
+    {α : B x} {β : B y} (q : PathP (λ i → B (p i)) α β)
+    {C : (x : A) → B x → Type ℓ''}
+    (f : {x : A} (y : B x) → C x y)
+    (g : (x : A) (y : B x) → C x y)
+  where
+
+  -- test that needs 'censor'
+  _ : PathP (λ i → C (p i) (q i)) (f ⌜ α ⌝) (f β)
+  _ = apd! q
+
+  -- test that needs an explicit placeholder
+  _ : PathP (λ i → C (p i) (q i)) (g ¿? ⌜ α ⌝) (g y β)
+  _ = apd! q
+
+  -- test that the tactic works with goals.
+  -- this needs --quote-metas
+  _ : PathP (λ i → C (p i) (q i)) (f ⌜ α ⌝) (f β)
+  _ = apd! {!   !}

src/1Lab/Reflection/Regularity.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas -vtactic:10 #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 open import 1Lab.Reflection.HLevel
 open import 1Lab.Reflection.Subst
 open import 1Lab.Reflection

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

@@ -220,5 +220,5 @@ make-free-abelian G .fold {H} f .fst =
 make-free-abelian G .fold {H} f .snd .is-group-hom.pres-⋆ =
   elim! λ _ _ → f .snd .is-group-hom.pres-⋆ _ _
 make-free-abelian G .commute = ext λ _ → refl
-make-free-abelian G .unique f p = ext (p ·ₚ_)
+make-free-abelian G .unique f p = ext (sym p ·ₚ_)
 ```

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

@@ -85,5 +85,5 @@ limits][rapl]).
 
   Direct-sum-is-product .π₁∘⟨⟩ = ext λ _ → refl
   Direct-sum-is-product .π₂∘⟨⟩ = ext λ _ → refl
-  Direct-sum-is-product .unique p q = ext λ x → p ·ₚ x ,ₚ q ·ₚ x
+  Direct-sum-is-product .unique p q = ext λ x → sym p ·ₚ x ,ₚ sym q ·ₚ x
 ```

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

@@ -328,7 +328,6 @@ module _ {ℓ} {A B C : Abelian-group ℓ} where instance
       {f = λ h → curry-bilinear (Hom≃Bilinear.to h)}
       (λ {x} p → Hom≃Bilinear.injective (Equiv.injective (_ , curry-bilinear-is-equiv) p))
       ef
-  {-# OVERLAPS Extensional-tensor-hom #-}
 ```
 -->
 

src/Algebra/Group/Cat/FinitelyComplete.lagda.md

@@ -129,10 +129,9 @@ Direct-product-is-product {G} {H} = p where
   open is-product
   p : is-product _ _ _
   p .⟨_,_⟩ = factor
-  p .π₁∘⟨⟩ = Grp↪Sets-is-faithful refl
-  p .π₂∘⟨⟩ = Grp↪Sets-is-faithful refl
-  p .unique p q = Grp↪Sets-is-faithful (funext λ x →
-    ap₂ _,_ (happly (ap fst p) x) (happly (ap fst q) x))
+  p .π₁∘⟨⟩ = ext λ _ → refl
+  p .π₂∘⟨⟩ = ext λ _ → refl
+  p .unique p q = ext λ x i → p (~ i) .fst x , q (~ i) .fst x
 ```
 
 What sets the direct product of groups apart from (e.g.) the cartesian
@@ -145,12 +144,12 @@ a coproduct.
 inj₁ : G Groups.↪ Direct-product G H
 inj₁ {G} {H} .mor .fst x = x , H .snd .unit
 inj₁ {G} {H} .mor .snd .pres-⋆ x y = ap (_ ,_) (sym (H .snd .idl))
-inj₁ {G} {H} .monic g h x = Grp↪Sets-is-faithful (funext λ e i → (x i · e) .fst)
+inj₁ {G} {H} .monic g h x = ext λ e i → (x i · e) .fst
 
 inj₂ : H Groups.↪ Direct-product G H
 inj₂ {H} {G} .mor .fst x = G .snd .unit , x
 inj₂ {H} {G} .mor .snd .pres-⋆ x y = ap (_, _) (sym (G .snd .idl))
-inj₂ {H} {G} .monic g h x = Grp↪Sets-is-faithful (funext λ e i → (x i · e) .snd)
+inj₂ {H} {G} .monic g h x = ext λ e i → (x i · e) .snd
 ```
 
 ## Equalisers

src/Algebra/Group/Concrete/FinitelyComplete.lagda.md

@@ -63,7 +63,7 @@ ConcreteGroups-products X Y = prod where
   prod .has-is-product .π₁∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _)
   prod .has-is-product .π₂∘⟨⟩ = funext∙ (λ _ → refl) (∙-idr _)
   prod .has-is-product .unique {Q} {f} {g} {u} p1 p2 =
-    funext∙ (λ x → p1 ·ₚ x ,ₚ p2 ·ₚ x) (fix ◁ square)
+    sym $ funext∙ (λ x → p1 ·ₚ x ,ₚ p2 ·ₚ x) (fix ◁ square)
     where
       square : Square
         (p1 ·ₚ pt Q ,ₚ p2 ·ₚ pt Q) ((fst∙ ∘∙ u) .snd ,ₚ (snd∙ ∘∙ u) .snd)

src/Algebra/Group/Free.lagda.md

@@ -105,6 +105,28 @@ unquoteDef Free-elim-prop = make-elim-with (default-elim-visible into 1)
 
 </details>
 
+<!--
+```agda
+instance
+  Extensional-free-group-hom
+    : ∀ {ℓ ℓr} {A : Type ℓ} {G : Group ℓ}
+    → ⦃ ei : Extensional (A → ⌞ G ⌟) ℓr ⦄
+    → Extensional (Groups.Hom (Free-Group A) G) ℓr
+  Extensional-free-group-hom {G = G} ⦃ ei ⦄ =
+    injection→extensional! {f = λ g a → g · inc a}
+      (λ {g} {h} p →
+        let
+          module g = is-group-hom (g .snd)
+          module h = is-group-hom (h .snd)
+        in Grp↪Sets-is-faithful (funext (Free-elim-prop _ (λ _ → hlevel 1) (happly p)
+          (λ x p y q → g.pres-⋆ _ _ ∙∙ ap₂ G._⋆_ p q ∙∙ sym (h.pres-⋆ _ _))
+          (λ x p → g.pres-inv ∙∙ ap G._⁻¹ p ∙∙ sym h.pres-inv)
+          (g.pres-id ∙ sym h.pres-id))))
+      ei
+    where module G = Group-on (G .snd)
+```
+-->
+
 ## Universal property {defines=free-group}
 
 We now prove the universal property of `Free-group`{.Agda}, or, more
@@ -175,15 +197,7 @@ make-free-group S .free = Free-Group ⌞ S ⌟
 make-free-group S .unit = inc
 make-free-group S .fold = fold-free-group
 make-free-group S .commute = refl
-make-free-group S .unique {H} g p =
-  ext $ Free-elim-prop _ (λ _ → hlevel 1)
-    (p ·ₚ_)
-    (λ a p b q → g.pres-⋆ a b ∙ ap₂ H._⋆_ p q)
-    (λ a p → g.pres-inv ∙ ap H.inverse p)
-    g.pres-id
-  where
-    module H = Group-on (H .snd)
-    module g = is-group-hom (g .snd)
+make-free-group S .unique {H} g p = ext (sym p ·ₚ_)
 
 module Free-groups {ℓ} (S : Set ℓ) = Free-object (make-free-group S)
 ```

src/Algebra/Group/Free/Product.lagda.md

@@ -158,7 +158,7 @@ The universal property of the pushout is easy to verify.
   Groups-pushout .universal comm .snd .pres-⋆ _ _ = refl
   Groups-pushout .universal∘i₁ = ext λ _ → refl
   Groups-pushout .universal∘i₂ = ext λ _ → refl
-  Groups-pushout .unique {Q = Q} {colim' = u} comm₁ comm₂ = ext $
+  Groups-pushout .unique {Q = Q} {colim' = u} comm₁ comm₂ = sym $ ext $
     Amalgamated-elim-prop (λ _ → hlevel 1)
       (λ x p y q → u .snd .pres-⋆ x y ∙ ap₂ Q._⋆_ p q)
       (λ x p → pres-inv (u .snd) ∙ ap Q._⁻¹ p)

src/Algebra/Group/Free/Words.lagda.md

@@ -553,7 +553,7 @@ more case bashes. First, we'll show that a group homomorphism $g : F(A)
 letters.
 
 ```agda
-make-free-group .unique {Y} {f} g h = ext uniq where
+make-free-group .unique {Y} {f} g h = sym $ ext uniq where
   open fold {Y} f
   module g = is-group-hom (g .snd)
 

src/Algebra/Group/Instances/Integers.lagda.md

@@ -110,8 +110,8 @@ must lift it.
 This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$.
 
 ```agda
-    pow-unique : (g : Groups.Hom (Lift-group ℓ ℤ) G) → g · 1 ≡ x → g ≡ pow-hom
-    pow-unique g g1≡x = ext λ x → p x ∙ sym (q x) where
+    pow-unique : (g : Groups.Hom (Lift-group ℓ ℤ) G) → g · 1 ≡ x → pow-hom ≡ g
+    pow-unique g g1≡x = ext λ x → q x ∙ sym (p x) where
       pow' = ℤ.map-out unit ((_⋆ x) , ⋆-equivr x)
       p : ∀ x → g · lift x ≡ pow' x
       p = ℤ.map-out-unique (λ i → g · lift i) (pres-id (g .snd)) λ y →
@@ -126,7 +126,7 @@ This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$.
   open pow public
 
   pow-unique₂ : (g h : Groups.Hom (Lift-group ℓ ℤ) G) → g · 1 ≡ h · 1 → g ≡ h
-  pow-unique₂ g h p = pow-unique (g · 1) g refl ∙ sym (pow-unique (g · 1) h (sym p))
+  pow-unique₂ g h p = sym (pow-unique (g · 1) g refl) ∙ pow-unique (g · 1) h (sym p)
 ```
 
 <details>