diff --git a/base/src/main/java/org/aya/core/pat/PatMatcher.java b/base/src/main/java/org/aya/core/pat/PatMatcher.java
index 9653c1791c..5d77bb9281 100644
--- a/base/src/main/java/org/aya/core/pat/PatMatcher.java
+++ b/base/src/main/java/org/aya/core/pat/PatMatcher.java
@@ -123,7 +123,7 @@ private void solve(@NotNull Pat pat, @NotNull MetaPatTerm metaPat) throws Mismat
       // solve as pat
       metaPat.ref().solution().set(metalized);
     } else {
-      // a MetaPat that has solution <==> the solution
+      // a MetaPat that has a solution <==> the solution
       match(pat, todo.toTerm());
     }
   }
diff --git a/base/src/main/java/org/aya/core/serde/SerTerm.java b/base/src/main/java/org/aya/core/serde/SerTerm.java
index dbe4005d40..0cd92979b0 100644
--- a/base/src/main/java/org/aya/core/serde/SerTerm.java
+++ b/base/src/main/java/org/aya/core/serde/SerTerm.java
@@ -342,7 +342,7 @@ sealed interface SerShapedFn extends SerTerm permits SerTerm.IntegerOps {
       return (Term) deShape(state);
     }
 
-    @NotNull Shaped.Fn<Term> deShape(@NotNull DeState state);
+    @NotNull Shaped.Appliable<Term> deShape(@NotNull DeState state);
   }
 
   record IntegerOps(
@@ -351,7 +351,7 @@ record IntegerOps(
     @NotNull SerDef.SerShapeResult shapeResult,
     @NotNull SerTerm.Data dataCall) implements SerShapedFn {
     @Override
-    public @NotNull Shaped.Fn<Term> deShape(@NotNull DeState state) {
+    public @NotNull Shaped.Appliable<Term> deShape(@NotNull DeState state) {
       DefVar<? extends Def, ? extends TeleDecl<?>> ref = state.resolve(this.ref);
       // ref can be empty for now, perhaps it hasn't been de.
       var shapeRecog = shapeResult.de(state);
diff --git a/base/src/main/java/org/aya/core/serde/Serializer.java b/base/src/main/java/org/aya/core/serde/Serializer.java
index f99067c568..a68a6d319a 100644
--- a/base/src/main/java/org/aya/core/serde/Serializer.java
+++ b/base/src/main/java/org/aya/core/serde/Serializer.java
@@ -104,7 +104,7 @@ public record Serializer(@NotNull Serializer.State state) {
       case FnCall fnCall -> new SerTerm.Fn(
         state.def(fnCall.ref()),
         serializeCall(fnCall.ulift(), fnCall.args()));
-      case ShapedFnCall(Shaped.Fn<Term> head, int ulift, ImmutableSeq<Arg<Term>> args) -> new SerTerm.ShapedFn(
+      case ShapedFnCall(Shaped.Appliable<Term> head, int ulift, ImmutableSeq<Arg<Term>> args) -> new SerTerm.ShapedFn(
         serializeShapedFn(head), serializeCall(ulift, args)
       );
       case ProjTerm proj -> new SerTerm.Proj(serialize(proj.of()), proj.ix());
@@ -180,12 +180,12 @@ case PAppTerm(var of, var args, var cube) -> new SerTerm.PathApp(serialize(of),
       ImmutableMap.from(classCall.args().view().map((k, v) -> Tuple.of(state.def(k), serialize(v)))));
   }
 
-  private @NotNull SerTerm.SerShapedFn serializeShapedFn(@NotNull Shaped.Fn<Term> shapedFn) {
-    return switch (shapedFn) {
+  private @NotNull SerTerm.SerShapedFn serializeShapedFn(@NotNull Shaped.Appliable<Term> shapedAppliable) {
+    return switch (shapedAppliable) {
       case IntegerOpsTerm(var ref, var kind, var recog, var dataCall) -> new SerTerm.IntegerOps(
         state.def(ref), kind, SerDef.SerShapeResult.serialize(state, recog), (SerTerm.Data) serialize(dataCall)
       );
-      default -> throw new IllegalStateException("Unexpected value: " + shapedFn);
+      default -> throw new IllegalStateException("Unexpected value: " + shapedAppliable);
     };
   }
 
diff --git a/base/src/main/java/org/aya/core/term/IntegerOpsTerm.java b/base/src/main/java/org/aya/core/term/IntegerOpsTerm.java
index 7737d0dbc6..27514e1802 100644
--- a/base/src/main/java/org/aya/core/term/IntegerOpsTerm.java
+++ b/base/src/main/java/org/aya/core/term/IntegerOpsTerm.java
@@ -24,7 +24,7 @@ public record IntegerOpsTerm(
   @NotNull Kind kind,
   @NotNull ShapeRecognition paramRecog,
   @NotNull DataCall paramType
-) implements Shaped.Fn<Term>, Term {
+) implements Shaped.Appliable<Term>, Term {
   public IntegerOpsTerm {
     assert paramRecog.shape() == AyaShape.NAT_SHAPE;
 
@@ -100,13 +100,4 @@ public enum Kind implements Serializable {
       }
     };
   }
-
-  @Override
-  public boolean equals(Object obj) {
-    if (obj instanceof IntegerOpsTerm term) {
-      return this.ref == term.ref && this.kind == term.kind;
-    }
-
-    return false;
-  }
 }
diff --git a/base/src/main/java/org/aya/core/term/ShapedFnCall.java b/base/src/main/java/org/aya/core/term/ShapedFnCall.java
index 623d2c5010..b235d9ac92 100644
--- a/base/src/main/java/org/aya/core/term/ShapedFnCall.java
+++ b/base/src/main/java/org/aya/core/term/ShapedFnCall.java
@@ -21,7 +21,7 @@
  * @param args
  */
 public record ShapedFnCall(
-  @NotNull Shaped.Fn<Term> head,
+  @NotNull Shaped.Appliable<Term> head,
   @Override int ulift,
   @Override @NotNull ImmutableSeq<Arg<Term>> args
 ) implements Callable.Tele {
@@ -30,7 +30,7 @@ public record ShapedFnCall(
     return head.ref();
   }
 
-  private @NotNull ShapedFnCall update(@NotNull Shaped.Fn<Term> head, @NotNull ImmutableSeq<Arg<Term>> args) {
+  private @NotNull ShapedFnCall update(@NotNull Shaped.Appliable<Term> head, @NotNull ImmutableSeq<Arg<Term>> args) {
     return head == this.head && args.sameElements(this.args, true)
       ? this
       : new ShapedFnCall(head, ulift, args);
@@ -38,7 +38,7 @@ public record ShapedFnCall(
 
   @Override
   public @NotNull Term descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {
-    return update((Shaped.Fn<Term>) f.apply((Term) head), args.map(x -> x.descent(f)));
+    return update((Shaped.Appliable<Term>) f.apply((Term) head), args.map(x -> x.descent(f)));
   }
 
   /**
diff --git a/base/src/main/java/org/aya/generic/Shaped.java b/base/src/main/java/org/aya/generic/Shaped.java
index c591235010..c4ae854263 100644
--- a/base/src/main/java/org/aya/generic/Shaped.java
+++ b/base/src/main/java/org/aya/generic/Shaped.java
@@ -108,9 +108,22 @@ default <O extends AyaDocile> boolean compareUntyped(@NotNull Shaped.List<O> oth
     }
   }
 
-  interface Fn<T extends AyaDocile> extends Shaped<T> {
+  /**
+   * Something Shaped which is appliable, like
+   * {@link org.aya.core.def.FnDef}, {@link CtorDef}, and probably {@link org.aya.core.def.DataDef}
+   */
+  interface Appliable<T extends AyaDocile> extends Shaped<T> {
+    /**
+     * The underlying ref
+     */
     @NotNull DefVar<? extends Def, ? extends TeleDecl<?>> ref();
+
+    /**
+     * Applying arguments.
+     *
+     * @param args arguments
+     * @return null if failed
+     */
     @Nullable T apply(@NotNull ImmutableSeq<Arg<T>> args);
-    @Override boolean equals(Object obj);
   }
 }
diff --git a/base/src/main/java/org/aya/tyck/repr/ShapeFactory.java b/base/src/main/java/org/aya/tyck/repr/ShapeFactory.java
index d3205589b8..b156ea065b 100644
--- a/base/src/main/java/org/aya/tyck/repr/ShapeFactory.java
+++ b/base/src/main/java/org/aya/tyck/repr/ShapeFactory.java
@@ -20,7 +20,7 @@
 import org.jetbrains.annotations.Nullable;
 
 public final class ShapeFactory {
-  public static @Nullable Shaped.Fn<Term> ofCtor(
+  public static @Nullable Shaped.Appliable<Term> ofCtor(
     @NotNull DefVar<CtorDef, TeleDecl.DataCtor> ref,
     @NotNull AyaShape.Factory factory,
     @NotNull DataCall paramType
@@ -34,7 +34,7 @@ public final class ShapeFactory {
     return ofCtor(ref, paramRecog, paramType);
   }
 
-  public static @Nullable Shaped.Fn<Term> ofCtor(
+  public static @Nullable Shaped.Appliable<Term> ofCtor(
     @NotNull DefVar<CtorDef, TeleDecl.DataCtor> ref,
     @NotNull ShapeRecognition paramRecog,
     @NotNull DataCall paramType
@@ -54,7 +54,7 @@ public final class ShapeFactory {
     return null;
   }
 
-  public static @Nullable Shaped.Fn<Term> ofFn(
+  public static @Nullable Shaped.Appliable<Term> ofFn(
     @NotNull DefVar<FnDef, TeleDecl.FnDecl> ref,
     @NotNull ShapeRecognition recog,
     @NotNull AyaShape.Factory factory
diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
index 38723a4412..e58aa423ee 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -170,6 +170,11 @@ private boolean compareWHNF(Term lhs, Term preRhs, Sub lr, Sub rl, @NotNull Term
     return compare(whnf, rhsWhnf, lr, rl, type);
   }
 
+  /**
+   * Short path of comparing {@link Callable}
+   *
+   * @see #isCall(Term)
+   */
   private @Nullable Term compareApprox(@NotNull Term preLhs, @NotNull Term preRhs, Sub lr, Sub rl) {
     return switch (preLhs) {
       case FnCall lhs when preRhs instanceof FnCall rhs ->
@@ -180,7 +185,7 @@ private boolean compareWHNF(Term lhs, Term preRhs, Sub lr, Sub rl, @NotNull Term
         lhs.ref() != rhs.ref() ? null : visitCall(lhs, rhs, lr, rl, lhs.ref(), lhs.ulift());
       // TODO[h]: This also involves Con situations, is it bad?
       case ShapedFnCall lhs when preRhs instanceof ShapedFnCall rhs ->
-        (!lhs.head().equals(rhs.head())) ? null : visitCall(lhs, rhs, lr, rl, lhs.ref(), lhs.ulift());
+        lhs.ref() != rhs.ref() ? null : visitCall(lhs, rhs, lr, rl, lhs.ref(), lhs.ulift());
       default -> null;
     };
   }