diff --git a/base/src/main/java/org/aya/lamett/syntax/Term.java b/base/src/main/java/org/aya/lamett/syntax/Term.java
index 1b0d433..1c4ea81 100644
--- a/base/src/main/java/org/aya/lamett/syntax/Term.java
+++ b/base/src/main/java/org/aya/lamett/syntax/Term.java
@@ -7,18 +7,22 @@
 import kala.tuple.Tuple2;
 import org.aya.lamett.tyck.Normalizer;
 import org.aya.lamett.tyck.Unification;
+import org.aya.lamett.tyck.Unifier;
 import org.aya.lamett.util.Distiller;
 import org.aya.lamett.util.LocalVar;
 import org.aya.lamett.util.Param;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Docile;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
+import java.util.function.Function;
+import java.util.function.Predicate;
 import java.util.function.UnaryOperator;
 
 public sealed interface Term extends Docile permits Cofib, Cofib.Eq, Term.App, Term.Coe, Term.ConCall, Term.DT, Term.DataCall,
   Term.Error, Term.Ext, Term.FnCall, Term.Hcom, Term.INeg, Term.InS, Term.Lam, Term.Lit, Term.OutS, Term.Pair, Term.PartEl,
-  Term.PartTy, Term.Path, Term.Proj, Term.Ref, Term.Sub {
+  Term.PartTy, Term.Path, Term.Proj, Term.Ref, Term.Sub, Term.Box, Term.Cap {
   @Override default @NotNull Doc toDoc() {
     return Distiller.term(this, Distiller.Prec.Free);
   }
@@ -33,7 +37,12 @@ public sealed interface Term extends Docile permits Cofib, Cofib.Eq, Term.App, T
   }
 
   record Error(@NotNull String msg) implements Term {}
-  record Ref(@NotNull LocalVar var) implements Term {}
+  record Ref(@NotNull LocalVar var) implements Term {
+    // For import static
+    public static @NotNull Term.Ref ref(@NotNull LocalVar var) {
+      return new Ref(var);
+    }
+  }
   record FnCall(@NotNull DefVar<Def.Fn> fn, @NotNull ImmutableSeq<Term> args) implements Term {}
   record DataCall(@NotNull DefVar<Def.Data> fn, @NotNull ImmutableSeq<Term> args) implements Term {}
   record ConCall(@NotNull DefVar<Def.Cons> fn, @NotNull ImmutableSeq<Term> args,
@@ -52,6 +61,12 @@ record Lam(@NotNull LocalVar x, @NotNull Term body) implements Term {
   static @NotNull Term mkLam(@NotNull SeqView<LocalVar> telescope, @NotNull Term body) {
     return telescope.foldRight(body, Lam::new);
   }
+
+  static @NotNull Term mkLam(@NotNull String name, @NotNull Function<LocalVar, Term> closeBody) {
+    var i = new LocalVar(name);
+    return new Lam(i, closeBody.apply(i));
+  }
+
   default @NotNull Term app(@NotNull Term... args) {
     var f = this;
     for (var a : args) f = f instanceof Lam lam ? lam.body.subst(lam.x, a) : new App(f, a);
@@ -129,6 +144,23 @@ record PartEl(@NotNull ImmutableSeq<Tuple2<Cofib.Conj, Term>> elems) implements
     public @NotNull PartEl map2(UnaryOperator<Term> f) {
       return new PartEl(elems.map(t -> Tuple.of(t.component1(), f.apply(t.component2()))));
     }
+
+    public @NotNull Cofib phi() {
+      return new Cofib(elems.map(Tuple2::component1));
+    }
+
+    /**
+     * Returns the first clause who makes simplifier happy.
+     *
+     * @param simplifier a simplifier, should confluent.
+     */
+    public @Nullable Tuple2<Cofib.Conj, Term> simplify(@NotNull Predicate<Cofib.Conj> simplifier) {
+      return elems.firstOrNull(pair -> simplifier.test(pair.component1()));
+    }
+
+    public @Nullable Tuple2<Cofib.Conj, Term> simplify(@NotNull Unifier unifier) {
+      return simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj)));
+    }
   }
 
 
@@ -196,6 +228,19 @@ record Hcom(@NotNull Term r, @NotNull Term s, @NotNull Term A, @NotNull Term phi
     return new Hcom(r, s, A.app(s), phi, mkPi(ImmutableSeq.of(new Param<>(i, Lit.I)), newEl));
   }
 
+  /**
+   * <pre>
+   * Γ ⊢ {@param A}   : U
+   * Γ ⊢ {@param phi} : F
+   * Γ ⊢ {@param u}   : {@link PartTy} phi A
+   * -------------------------------------------
+   * Γ, phi ⊢ outPartial A phi u = hcom 0 1 phi (λ i. u) : A
+   * </pre>
+   */
+  static @NotNull Term outPartial(@NotNull Term A, @NotNull Term phi, @NotNull Term u) {
+    return new Hcom(Lit.Zero, Lit.One, A, phi, mkLam("i", $ -> u));
+  }
+
   /**
    * Generalized extension type.
    *
@@ -210,10 +255,59 @@ record Ext<F extends Restr>(@NotNull Term type, @NotNull F restr) implements Ter
   record Path(@NotNull ImmutableSeq<LocalVar> binders, @NotNull Ext<Restr.Cubical> ext) implements Term {
   }
 
+  /// region Cubical Subtype
+
   record Sub(@NotNull Term type, @NotNull Term partEl) implements Term {}
   record InS(@NotNull Term phi, @NotNull Term of) implements Term {}
   record OutS(@NotNull Term phi, @NotNull Term partEl, @NotNull Term of) implements Term {}
 
+  /// endregion Cubical Subtype
+
+  /// region HcompU
+
+  // Composition type in Kan.pdf, but there is already a class Hcom! So I use HcomU.
+  // record HcomU(
+  //   @NotNull Term r /* : I */,
+  //   @NotNull Term s /* : I */,
+  //   @NotNull LocalVar i /* : I*/,
+  //   // @NotNull Cofib φ, // come from PartEl
+  //   @NotNull PartEl A /* Partial (i = r \/ φ) code(U) // under i */
+  // ) implements Term {
+  // }
+
+  /**
+   * <pre>
+   * Γ ⊢ {@param r} {@param s} : I
+   * Γ ⊢ {@param phi} : F
+   * Γ ⊢ {@param A} : (i : I) → {@link PartTy} (i = r ∨ φ) U
+   * Γ ⊢ {@param eave} : Partial φ (A s)
+   * Γ ⊢ {@param floor} : A r | φ ↦ coe s r A eave
+   * outPartial (A s)
+   * ------------------------------- outS floor : A r
+   * Γ ⊢ box r s phi A eave floor : hcom r s U phi A
+   *                              | r = s ↦ outS (floor) : outPartial (A r)
+   * </pre>
+   */
+  record Box(
+    @NotNull Term r, @NotNull Term s,
+    @NotNull Term phi,
+    @NotNull Term A /* : (i : I) → Partial (i = r ∨ φ) U */,
+    // omit metalanguage-level `outPartial : (Partial ⊤ A) → A` below
+    @NotNull PartEl eave /* Partial φ (A s) */,
+    @NotNull Term floor /* : A r | φ ↦ coe s r A eave */
+  ) implements Term {
+  }
+
+  record Cap(
+    @NotNull Term r, @NotNull Term s,
+    @NotNull Term phi,
+    @NotNull Term A /* : (i : I) → Partial (i = r ∨ φ) U */,
+    @NotNull Term hcomU /* : hcom (r ~> s) U φ A */
+  ) implements Term {
+  }
+
+  /// endregion HcompU
+
   /** Let A be argument, then <code>A i -> A j</code> */
   static @NotNull Pi familyI2J(Term term, Term i, Term j) {
     return (Pi) mkPi(new App(term, i), new App(term, j));
diff --git a/base/src/main/java/org/aya/lamett/syntax/Type.java b/base/src/main/java/org/aya/lamett/syntax/Type.java
index 5820e20..504b28f 100644
--- a/base/src/main/java/org/aya/lamett/syntax/Type.java
+++ b/base/src/main/java/org/aya/lamett/syntax/Type.java
@@ -81,6 +81,17 @@ record Sub(
     }
   }
 
+  record HcomU(
+    @NotNull Term r, @NotNull Term s,
+    @NotNull LocalVar i,
+    @NotNull ImmutableSeq<Tuple2<Cofib.Conj, Type>> restrs // under i
+  ) implements Type {
+    @Override
+    public @NotNull Doc toDoc() {
+      return Doc.plain("HcomU");
+    }
+  }
+
   default @NotNull Type subst(@NotNull LocalVar x, @NotNull Term t) {
     return subst(MutableMap.of(x, t));
   }
diff --git a/base/src/main/java/org/aya/lamett/tyck/Elaborator.java b/base/src/main/java/org/aya/lamett/tyck/Elaborator.java
index 3671c09..25ee29b 100644
--- a/base/src/main/java/org/aya/lamett/tyck/Elaborator.java
+++ b/base/src/main/java/org/aya/lamett/tyck/Elaborator.java
@@ -19,7 +19,9 @@
 import java.util.function.Function;
 import java.util.function.Supplier;
 
+import static org.aya.lamett.syntax.Term.*;
 import static org.aya.lamett.tyck.Normalizer.rename;
+import static org.aya.lamett.syntax.Term.Ref.ref;
 
 public record Elaborator(
   @NotNull MutableMap<DefVar<?>, Def> sigma,
diff --git a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java
index 1648a3e..0f47b84 100644
--- a/base/src/main/java/org/aya/lamett/tyck/KanPDF.java
+++ b/base/src/main/java/org/aya/lamett/tyck/KanPDF.java
@@ -1,12 +1,18 @@
 package org.aya.lamett.tyck;
 
+import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableMap;
+import kala.tuple.Tuple;
+import org.aya.lamett.syntax.Cofib;
 import org.aya.lamett.syntax.Term;
 import org.aya.lamett.util.LocalVar;
 import org.jetbrains.annotations.NotNull;
 
+import java.util.function.BiFunction;
+import java.util.function.Function;
 import java.util.function.UnaryOperator;
 
+import static org.aya.lamett.syntax.Term.Ref.ref;
 import static org.aya.lamett.tyck.Normalizer.rename;
 
 public interface KanPDF {
@@ -75,4 +81,80 @@ static Term coeSigma(Term.Sigma sigma, LocalVar i, Term coeR, Term coeS) {
     var m1 = Term.com(hcomR, hcomS, comType, phi, i, partEl.map2(t -> t.proj(false)));
     return new Term.Pair(m0.apply(hcomS), m1);
   }
+
+  static @NotNull Term hcomHcomU(
+    // hcom
+    @NotNull Term hcomR, @NotNull Term hcomS,
+    @NotNull Term hcomPhi, @NotNull LocalVar hcomI, @NotNull Term.PartEl hcomU,
+    // hcomU
+    @NotNull Term hcomUr, @NotNull Term hcomUs,
+    @NotNull Term hcomUphi, @NotNull LocalVar hcomUi, @NotNull Term.PartEl hcomUA,
+    @NotNull Unifier unifier
+  ) {
+    var conjHcomPhi = Cofib.Conj.of(hcomPhi);
+    var conjHcomUphi = Cofib.Conj.of(hcomUphi);
+    var conjReqS = Cofib.Conj.of(new Cofib.Eq(hcomUr, hcomUs));
+
+    // hcom { r ~> s } (hcom { r' ~> s' } U ψ A) φ u =
+    // box { r' ~> s' } ?0 ?1 : hcom { r' ~> s' } U ψ A
+    //   where ψ ⊢ ?0 : A s'
+    //           ⊢ ?1 : A r' | ψ ↦ coe { s' ~> r' } A ?0
+
+    // r' = s' ∨ ψ , i : I ⊢ P := hcom { r ~> i } (A s') φ u : A s' | ψ ↦ u i
+    Function<Term, Term> P = i ->
+      new Term.Hcom(hcomR, i, hcomUA.subst(hcomUi, hcomUs), hcomPhi, new Term.Lam(hcomI, hcomU));
+
+    // ⊢ ?1 := hcom { r ~> s } (A r') (φ ∨ ψ ∨ r' = s')
+    //    (λ i. {| i = r ∨ φ ↦ ?2 ; ψ ↦ ?3 ; r' = s' ↦ ?4 |}
+    //    : A r'
+    //    | r = s ∨ φ ↦ ...
+    //    | ψ ↦ coe { s' ~> r' } A (P s')       (required by box)
+    //    | r' = s' ↦ ...
+
+    // i : I, i = r ∨ φ ⊢ ?2 := cap { r' <~ s' } ψ (u i)
+    BiFunction<Term, Cofib.Conj, Term> Q = (i, proof) -> {
+      var result = unifier.withCofibConj(proof, () -> {
+        var realU = hcomU.simplify(unifier);
+        assert realU != null : "φ ∧ ¬ φ";
+        return new Term.Cap(hcomUr, hcomUs, hcomUphi, hcomUA, realU.component2().subst(hcomI, i));
+      }, null);   // TODO: I am not sure !!
+      assert result != null : "i != r";
+      return result;
+    };
+
+    Function<Term, Term> Q0 = i -> Q.apply(i, Cofib.Conj.of(new Cofib.Eq(i, hcomR)));
+    Function<Term, Term> Q1 = i -> Q.apply(i, conjHcomPhi);
+
+    // i : I, ψ ⊢ ?3 := coe { s' ~> r' } A (P i)
+    Function<Term, Term> R = i -> {
+      var realA = hcomUA.simplify(unifier);
+      assert realA != null : "φ ∧ ¬ φ";
+      return new Term.Coe(hcomUs, hcomUr, realA.component2()).app(P.apply(i));
+    };
+
+    // i : I, r' = s' ⊢ ?4 := P i : A r'
+    Function<Term, Term> S = P;
+
+    Function<Term, Term.PartEl> T = i -> new Term.PartEl(ImmutableSeq.of(
+      Tuple.of(Cofib.Conj.of(new Cofib.Eq(i, hcomR)), Q0.apply(i)),
+      Tuple.of(conjHcomPhi, Q1.apply(i)),
+      Tuple.of(conjHcomUphi, R.apply(i)),
+      Tuple.of(conjReqS, S.apply(i))
+    ));
+
+    // (i : I) -> Partial (i = r ∨ φ ∨ ψ ∨ r' = s') (A r')
+    var termT = Term.mkLam("i", i -> T.apply(ref(i)));
+
+    var halfRealAr = ((Term.PartEl) hcomUA.subst(hcomUi, hcomUr))
+      .simplify(unifier);     // since `i : I ⊢ A : Partial (i = r' ∨ ψ) U`, we have a clause with cof `r' = r'`
+    assert halfRealAr != null : "φ ∧ ¬ φ";
+    var realAr = halfRealAr.component2();
+
+
+    return new Term.Box(hcomUr, hcomUs, hcomUphi, new Term.Lam(hcomUi, hcomUA),
+      new Term.PartEl(ImmutableSeq.of(Tuple.of(conjHcomUphi, P.apply(hcomUs)))),
+      new Term.Hcom(hcomR, hcomS, realAr,
+        Cofib.of(conjHcomPhi, conjHcomUphi, conjReqS),
+        termT));
+  }
 }
diff --git a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java
index 9b215b0..b6b0275 100644
--- a/base/src/main/java/org/aya/lamett/tyck/Normalizer.java
+++ b/base/src/main/java/org/aya/lamett/tyck/Normalizer.java
@@ -11,6 +11,8 @@
 
 import java.util.function.UnaryOperator;
 
+import static org.aya.lamett.syntax.Term.Ref.ref;
+
 
 public class Normalizer {
   private final @NotNull MutableMap<LocalVar, Term> rho;
@@ -51,6 +53,7 @@ public Type type(Type type) {
       case Type.Sigma sig -> new Type.Sigma(new Param<>(sig.param().x(), type(sig.param().type())), type(sig.cod()));
       case Type.PartTy partTy -> new Type.PartTy(type(partTy.underlying()), term(partTy.restrs()));
       case Type.Sub sub -> new Type.Sub(type(sub.underlying()), partEl(sub.restrs()));
+      case Type.HcomU(var r, var s, var i, var restr) -> new Type.HcomU(term(r), term(s), i, partEl(restr, this::type));
     };
   }
 
@@ -163,6 +166,65 @@ yield switch (A) {
         }
         yield new Term.OutS(outPhi, outPartEl, outOf);
       }
+      case Term.Box(var r, var s, var phi, var A, var eave, var floor) -> {
+        r = term(r);
+        s = term(s);
+        phi = term(phi);
+        A = term(A);
+        eave = (Term.PartEl) term(eave);
+        floor = term(floor);
+
+        // r = s
+        if (unifier.untyped(r, s)) yield floor;
+
+        // φ true
+        var branch = eave.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj)));
+        if (branch != null) yield branch.component2();    // FIXME: term(...) if we switch to whnf
+
+        // unique rule
+        if (floor instanceof Term.Cap cap && phi instanceof Cofib coffee) {
+          var mEave = eave;
+          var success = unifier.withCofib(coffee, () -> {
+            var realEave = mEave.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj)));
+            assert realEave != null : "φ ∧ ¬ φ";
+            return unifier.untyped(realEave.component2(), cap.hcomU());
+          }, true);
+          if (success) {
+            yield term(cap.hcomU());
+          }
+        }
+
+        yield new Term.Box(r, s, phi, A, eave, floor);
+      }
+      case Term.Cap(var r, var s, var phi, var A, var hcomU) -> {
+        r = term(r);
+        s = term(s);
+        phi = term(phi);
+        A = term(A);
+        hcomU = term(hcomU);
+
+        if (unifier.untyped(r, s)) yield hcomU;
+
+        var i = new LocalVar("i");
+        if (term(A.app(ref(i))) instanceof Term.PartEl wall
+          && phi instanceof Cofib coffee
+          && unifier.cofibIsTrue(coffee)) {
+          // since `A : (i : I) → Partial (i = r ∨ φ) U` and we are under `φ`
+          // We have `A i : Partial ⊤ U` for any i,
+          // and `realAi := outPartial (A i) : U`
+          var realAi = wall.simplify(conj -> unifier.cofibIsTrue(Cofib.of(conj)));
+          assert realAi != null : "φ ∧ ¬ φ";
+          // coe { s ~> r } A hcomU
+          yield term(new Term.Coe(s, r, new Term.Lam(i, realAi.component2())).app(hcomU));
+        }
+
+        if (hcomU instanceof Term.Box box) {
+          // computation rule
+          yield term(box.floor());
+        }
+
+        yield new Term.Cap(r, s, phi, A, hcomU);
+      }
     };
   }
 
@@ -194,18 +256,29 @@ yield switch (A) {
           cofib = cofib.conj(cofib1);
           continue;
         }
-        default -> {}
+        default -> {
+        }
       }
       cofib = cofib.conj(Cofib.from(atom));
     }
     return cofib;
   }
 
-  private @NotNull ImmutableSeq<Tuple2<Cofib.Conj, Term>> partEl(@NotNull ImmutableSeq<Tuple2<Cofib.Conj, Term>> elems) {
+  private @NotNull <T> ImmutableSeq<Tuple2<Cofib.Conj, T>> partEl(
+    @NotNull ImmutableSeq<Tuple2<Cofib.Conj, T>> elems,
+    @NotNull UnaryOperator<T> checker
+  ) {
     return elems.flatMap(tup ->
-      term(tup.component1()).conjs().map(conj -> Tuple.of(conj, term(tup.component2()))));
+      term(tup.component1()).conjs().map(conj -> Tuple.of(conj, checker.apply(tup.component2()))));
+  }
+
+  private @NotNull ImmutableSeq<Tuple2<Cofib.Conj, Term>> partEl(
+    @NotNull ImmutableSeq<Tuple2<Cofib.Conj, Term>> elems
+  ) {
+    return partEl(elems, this::term);
   }
 
+
   public @NotNull Normalizer derive() {
     return new Normalizer(MutableMap.from(rho), unification.derive());
   }
@@ -233,8 +306,7 @@ public Term term(Term term) {
         case Cofib.Eq eq -> new Cofib.Eq(term(eq.lhs()), term(eq.rhs()));
         case Term.INeg t -> new Term.INeg(term(t));
         case Term.PartTy(var cof, var ty) -> new Term.PartTy(term(cof), term(ty));
-        case Term.PartEl(var elems) ->
-          new Term.PartEl(elems.map(tup -> Tuple.of(term(tup.component1()), term(tup.component2()))));
+        case Term.PartEl partEl -> partEl(partEl);
         case Term.Error error -> error;
         case Term.Coe(var r, var s, var A) -> new Term.Coe(term(r), term(s), term(A));
         case Term.Hcom(var r, var s, var A, var f, var partial) ->
@@ -244,6 +316,10 @@ public Term term(Term term) {
         case Term.Sub(var A, var partEl) -> new Term.Sub(term(A), term(partEl));
         case Term.InS(var phi, var of) -> new Term.InS(term(phi), term(of));
         case Term.OutS(var phi, var partEl, var of) -> new Term.OutS(term(phi), term(partEl), term(of));
+        case Term.Box(var r, var s, var phi, var A, var eave, var floor) ->
+          new Term.Box(term(r), term(s), term(phi), term(A), partEl(eave), term(floor));
+        case Term.Cap(var r, var s, var phi, var A, var hcom) ->
+          new Term.Cap(term(r), term(s), term(phi), term(A), term(hcom));
       };
     }
 
@@ -251,6 +327,14 @@ public Term term(Term term) {
       return new Term.Ext<>(term(ext.type()), (F) ext.restr().map(this::term, this::term));
     }
 
+    // avoiding explicitly casting
+    public @NotNull Term.PartEl partEl(@NotNull Term.PartEl partEl) {
+      return new Term.PartEl(
+        partEl.elems().map(tup ->
+          Tuple.of(term(tup.component1()), term(tup.component2())))
+      );
+    }
+
     public @NotNull Cofib.Conj term(@NotNull Cofib.Conj conj) {
       return new Cofib.Conj(conj.atoms().map(this::term));
     }
diff --git a/base/src/main/java/org/aya/lamett/tyck/Unifier.java b/base/src/main/java/org/aya/lamett/tyck/Unifier.java
index e1198bf..7cb1f6b 100644
--- a/base/src/main/java/org/aya/lamett/tyck/Unifier.java
+++ b/base/src/main/java/org/aya/lamett/tyck/Unifier.java
@@ -104,6 +104,7 @@ && untypedInner(ldt.param().type(), rdt.param().type())
       case Term.INeg(var ll) when r instanceof Term.INeg(var rr) -> untypedInner(ll, rr);
       case Term.Coe(var r1, var s1, var A1) when r instanceof Term.Coe(var r2, var s2, var A2) ->
         untypedInner(r1, r2) && untypedInner(s1, s2) && untypedInner(A1, A2);
+      case Term.Hcom hcom -> throw new UnsupportedOperationException();
       default -> false;
     };
     if (!happy && data == null) data = new FailureData(l, r);
@@ -111,7 +112,7 @@ && untypedInner(ldt.param().type(), rdt.param().type())
     return happy;
   }
 
-  boolean cofibIsTrue(@NotNull Cofib cofib) {
+  public boolean cofibIsTrue(@NotNull Cofib cofib) {
     return cofib.conjs().anyMatch(conj -> conj.atoms().allMatch(atom -> switch (atom) {
       case Cofib.Eq eq -> untyped(eq.lhs(), eq.rhs());
       case Term.Ref(var ref) -> unification.cofibVars.contains(ref);
diff --git a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java
index 2565666..6946b87 100644
--- a/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java
+++ b/base/src/main/java/org/aya/lamett/tyck/WeaklyTarski.java
@@ -1,9 +1,11 @@
 package org.aya.lamett.tyck;
 
 import org.aya.lamett.syntax.Cofib;
+import kala.tuple.Tuple;
 import org.aya.lamett.syntax.Keyword;
 import org.aya.lamett.syntax.Term;
 import org.aya.lamett.syntax.Type;
+import org.aya.lamett.util.LocalVar;
 import org.aya.lamett.util.Param;
 import org.jetbrains.annotations.NotNull;
 
@@ -25,6 +27,17 @@ public record WeaklyTarski(@NotNull Normalizer n) {
       case Term.PartTy(var c, var type) when c instanceof Cofib cofib -> new Type.PartTy(el(type), n.term(cofib));
       case Term.Sub(var A, var p) when p instanceof Term.PartEl partEl ->
         new Type.Sub(el(A), partEl.elems());
+      // composition type
+      case Term.Hcom hcom when hcom.A() instanceof Term.Lit tyLit && tyLit.keyword() == Keyword.U -> {
+        // hcom is wellTyped, then hcom.u has type `I -> Partial U (i = r ∨ φ) {| ... |}`
+        // constructing `Partial Type (i = r ∨ φ) {| ... |}` from hcom.u under our `i`
+        var i = new LocalVar("i");
+        var inner = n.term(hcom.u().app(new Term.Ref(i)));
+        if (inner instanceof Term.PartEl partEl) {
+          var tyInner = partEl.elems().map(x -> Tuple.of(x.component1(), el(x.component2())));
+          yield new Type.HcomU(hcom.r(), hcom.s(), i, tyInner);
+        } else yield new Type.El(hcom);
+      }
       case Term misc -> new Type.El(misc);
     };
   }
diff --git a/base/src/main/java/org/aya/lamett/util/Distiller.java b/base/src/main/java/org/aya/lamett/util/Distiller.java
index eba21b5..56e7460 100644
--- a/base/src/main/java/org/aya/lamett/util/Distiller.java
+++ b/base/src/main/java/org/aya/lamett/util/Distiller.java
@@ -160,6 +160,8 @@ enum Prec {
       case Term.Sub(Term A, Term partEl) -> call(envPrec, "Sub", A, Doc.plain("φ"), partEl);
       case Term.InS(var phi, var of) -> insideOut(envPrec, phi, of, "inS");
       case Term.OutS(var phi, var partEl, var of) -> insideOut(envPrec, phi, of, "outS");
+      case Term.Box box -> throw new UnsupportedOperationException("TODO");
+      case Term.Cap cap -> throw new UnsupportedOperationException("TODO");
     };
   }