diff --git a/docs/design/generics/README.md b/docs/design/generics/README.md
index c49f321938105..2ada4467142de 100644
--- a/docs/design/generics/README.md
+++ b/docs/design/generics/README.md
@@ -16,5 +16,6 @@ feature of Carbon:
     direction.
 -   [Terminology](terminology.md) - A glossary establishing common terminology
     for describing the design.
--   ~~Detailed design~~ - not implemented yet
+-   [Detailed design](details.md) - In depth description of how generic type
+    parameters work.
 -   ~~Rejected alternatives~~ - not implemented yet
diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md
new file mode 100644
index 0000000000000..e62623168a918
--- /dev/null
+++ b/docs/design/generics/details.md
@@ -0,0 +1,1591 @@
+# Carbon deep dive: combined interfaces
+
+<!--
+Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+Exceptions. See /LICENSE for license information.
+SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+-->
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Overview](#overview)
+-   [Interfaces](#interfaces)
+-   [Implementing interfaces](#implementing-interfaces)
+    -   [Facet type](#facet-type)
+    -   [Implementing multiple interfaces](#implementing-multiple-interfaces)
+    -   [External impl](#external-impl)
+    -   [Qualified member names](#qualified-member-names)
+-   [Generics](#generics)
+    -   [Model](#model)
+-   [Interfaces recap](#interfaces-recap)
+-   [Type-of-types and facet types](#type-of-types-and-facet-types)
+-   [Structural interfaces](#structural-interfaces)
+    -   [Subtyping between type-of-types](#subtyping-between-type-of-types)
+-   [Combining interfaces by anding type-of-types](#combining-interfaces-by-anding-type-of-types)
+-   [Interface requiring other interfaces](#interface-requiring-other-interfaces)
+    -   [Interface extension](#interface-extension)
+        -   [`extends` and `impl` with structural interfaces](#extends-and-impl-with-structural-interfaces)
+        -   [Diamond dependency issue](#diamond-dependency-issue)
+    -   [Use case: overload resolution](#use-case-overload-resolution)
+-   [Type compatibility](#type-compatibility)
+-   [Future work](#future-work)
+    -   [Adapting types](#adapting-types)
+    -   [Associated constants](#associated-constants)
+    -   [Associated types](#associated-types)
+    -   [Parameterized interfaces](#parameterized-interfaces)
+        -   [Impl lookup](#impl-lookup)
+    -   [Constraints](#constraints)
+    -   [Conditional conformance](#conditional-conformance)
+    -   [Parameterized impls](#parameterized-impls)
+        -   [Lookup resolution and specialization](#lookup-resolution-and-specialization)
+    -   [Other constraints as type-of-types](#other-constraints-as-type-of-types)
+        -   [Sized types and type-of-types](#sized-types-and-type-of-types)
+    -   [Dynamic types](#dynamic-types)
+        -   [Runtime type parameters](#runtime-type-parameters)
+        -   [Runtime type fields](#runtime-type-fields)
+    -   [Abstract return types](#abstract-return-types)
+    -   [Interface defaults](#interface-defaults)
+    -   [Evolution](#evolution)
+    -   [Testing](#testing)
+    -   [Operator overloading](#operator-overloading)
+    -   [Impls with state](#impls-with-state)
+    -   [Generic associated types and higher-ranked types](#generic-associated-types-and-higher-ranked-types)
+        -   [Generic associated types](#generic-associated-types)
+        -   [Higher-ranked types](#higher-ranked-types)
+    -   [Field requirements](#field-requirements)
+    -   [Generic type specialization](#generic-type-specialization)
+    -   [Bridge for C++ customization points](#bridge-for-c-customization-points)
+    -   [Reverse generics for return types](#reverse-generics-for-return-types)
+    -   [Variadic arguments](#variadic-arguments)
+
+<!-- tocstop -->
+
+## Overview
+
+This document goes into the details of the design of generic type parameters.
+
+Imagine we want to write a function parameterized by a type argument. Maybe our
+function is `PrintToStdout` and let's say we want to operate on values that have
+a type for which we have an implementation of the `ConvertibleToString`
+interface. The `ConvertibleToString` interface has a `ToString` method returning
+a string. To do this, we give the `PrintToStdout` function two parameters: one
+is the value to print, let's call that `val`, the other is the type of that
+value, let's call that `T`. The type of `val` is `T`, what is the type of `T`?
+Well, since we want to let `T` be any type implementing the
+`ConvertibleToString` interface, we express that in the "interfaces are
+type-of-types" model by saying the type of `T` is `ConvertibleToString`.
+
+Since we can figure out `T` from the type of `val`, we don't need the caller to
+pass in `T` explicitly, so it can be an
+[deduced argument](terminology.md#deduced-parameter) (also see
+[deduced argument](overview.md#deduced-parameters) in the Generics overview
+doc). Basically, the user passes in a value for `val`, and the type of `val`
+determines `T`. `T` still gets passed into the function though, and it plays an
+important role -- it defines the implementation of the interface. We can think
+of the interface as defining a struct type whose members are function pointers,
+and an implementation of an interface as a value of that struct with actual
+function pointer values. So an implementation is a table of function pointers
+(one per function defined in the interface) that gets passed into a function as
+the type argument. For more on this, see [the model section](#model) below.
+
+In addition to function pointer members, interfaces can include any constants
+that belong to a type. For example, the
+[type's size](#sized-types-and-type-of-types) (represented by an integer
+constant member of the type) could be a member of an interface and its
+implementation. There are a few cases why we would include another interface
+implementation as a member:
+
+-   [associated types](#associated-types)
+-   [type parameters](#parameterized-interfaces)
+-   [interface requirements](#interface-requiring-other-interfaces)
+
+The function can decide whether that type argument is passed in
+[statically](terminology.md#static-dispatch-witness-table) (basically generating
+a separate function body for every different type passed in) by using the
+"generic argument" syntax (`:!`, see [the generics section](#generics) below) or
+[dynamically](terminology.md#dynamic-dispatch-witness-table) using the regular
+argument syntax (just a colon, `:`, see
+[the runtime type parameters section](#runtime-type-parameters) below). Either
+way, the interface contains enough information to
+[type and definition check](terminology.md#complete-definition-checking) the
+function body -- you can only call functions defined in the interface in the
+function body. Contrast this with making the type a template argument, where you
+could just use `Type` instead of an interface and it will work as long as the
+function is only called with types that allow the definition of the function to
+compile. The interface bound has other benefits:
+
+-   allows the compiler to deliver clearer error messages,
+-   documents expectations, and
+-   expresses that a type has certain semantics beyond what is captured in its
+    member function names and signatures.
+
+The last piece of the puzzle is how the caller of the function can produce a
+value with the right type. Let's say the user has a value of type `Song`, and of
+course songs have all sorts of functionality. If we want a `Song` to be printed
+using the `PrintToStdout` function, it needs to implement the
+`ConvertibleToString` interface. Note that we _don't_ say that `Song` is of type
+`ConvertibleToString` but instead that it has a "facet type". This means there
+is another type, called `Song as ConvertibleToString`, with the following
+properties:
+
+-   `Song as ConvertibleToString` has the same _data representation_ as `Song`.
+-   `Song as ConvertibleToString` is an implementation of the interface
+    `ConvertibleToString`. The functions of `Song as ConvertibleToString` are
+    just implementations of the names and signatures defined in the
+    `ConvertibleToString` interface, like `ToString`, and not the functions
+    defined on `Song` values.
+-   Carbon will implicitly cast values from type `Song` to type
+    `Song as ConvertibleToString` when calling a function that can only accept
+    types of type `ConvertibleToString`.
+-   In the normal case where the implementation of `ConvertibleToString` for
+    `Song` is not defined as `external`, every member of
+    `Song as ConvertibleToString` is also a member of `Song`. This includes
+    members of `ConvertibleToString` that are not explicitly named in the `impl`
+    definition but have defaults.
+-   You may access the `ToString` function for a `Song` value `w` by writing a
+    _qualified_ function call, like `w.(ConvertibleToString.ToString)()`. The
+    same effect may be achieved by casting, as in
+    `(w as (Song as ConvertibleToString)).ToString()`. This qualified syntax is
+    available whether or not the implementation is defined as `external`.
+-   If other interfaces are implemented for `Song`, they are also implemented
+    for `Song as ConvertibleToString`. The only thing that changes when casting
+    a `Song` `w` to `Song as ConvertibleToString` are the names that are
+    accessible without using the qualification syntax. A
+    `Song as ConvertibleToString` value can likewise be cast to a `Song`; a
+    `Song` acts just like another facet type for these purposes.
+
+We define these facet types (alternatively, interface implementations) either
+with the type, with the interface, or somewhere else where Carbon can be
+guaranteed to see when needed. For more on this, see
+[the implementing interfaces section](#implementing-interfaces) below.
+
+If `Song` doesn't implement an interface or we would like to use a different
+implementation of that interface, we can define another type that also has the
+same data representation as `Song` that has whatever different interface
+implementations we want. However, Carbon won't implicitly cast to that other
+type, the user will have to explicitly cast to that type in order to select
+those alternate implementations. For more on this, see
+[the adapting type section](#adapting-types) below.
+
+## Interfaces
+
+An [interface](terminology.md#interface), defines an API that a given type can
+implement. For example, an interface capturing a linear-algebra vector API might
+have two methods:
+
+```
+interface Vector {
+  // Here "Self" means "the type implementing this interface".
+  fn Add[me: Self](b: Self) -> Self;
+  fn Scale[me: Self](v: Double) -> Self;
+}
+```
+
+The syntax here is to match how the same members would be defined in a type.
+Each declaration in the interface defines an _associated item_ (same
+[terminology as Rust](https://doc.rust-lang.org/reference/items/associated-items.html)).
+In this example, `Vector` has two associated methods, `Add` and `Scale`.
+
+**References:** Method syntax for types was decided in
+[question-for-leads issue #494](https://github.com/carbon-language/carbon-lang/issues/494).
+
+An interface defines a type-of-type, that is a type whose values are types. The
+values of an interface are specifically
+[facet types](terminology.md#facet-type), by which we mean types that are
+declared as specifically implementing **exactly** this interface, and which
+provide definitions for all the functions (and other members) declared in the
+interface.
+
+## Implementing interfaces
+
+Carbon interfaces are ["nominal"](terminology.md#nominal-interfaces), which
+means that types explicitly describe how they implement interfaces. An
+["impl"](terminology.md#impls-implementations-of-interfaces) defines how one
+interface is implemented for a type. Every associated item is given a
+definition. Different types satisfying `Vector` can have different definitions
+for `Add` and `Scale`, so we say their definitions are _associated_ with what
+type is implementing `Vector`. The `impl` defines what is associated with the
+type for that interface.
+
+Impls may be defined inline inside the type definition:
+
+```
+class Point {
+  var x: Double;
+  var y: Double;
+  impl as Vector {
+    // In this scope, "Self" is an alias for "Point".
+    fn Add[me: Self](b: Self) -> Self {
+      return Point(.x = a.x + b.x, .y = a.y + b.y);
+    }
+    fn Scale[me: Self](v: Double) -> Self {
+      return Point(.x = a.x * v, .y = a.y * v);
+    }
+  }
+}
+```
+
+Interfaces that are implemented inline contribute to the type's API:
+
+```
+var p1: Point = (.x = 1.0, .y = 2.0);
+var p2: Point = (.x = 2.0, .y = 4.0);
+Assert(p1.Scale(2.0) == p2);
+Assert(p1.Add(p1) == p2);
+```
+
+**Comparison with other languages:** Rust defines implementations lexically
+outside of the `class` definition. This Carbon approach means that a type's API
+is described by declarations inside the `class` definition and doesn't change
+afterwards.
+
+**References:** This interface implementation syntax was accepted in
+[proposal #553](https://github.com/carbon-language/carbon-lang/pull/553). In
+particular, see
+[the alternatives considered](/proposals/p0553.md#interface-implementation-syntax).
+
+### Facet type
+
+The `impl` definition defines a [facet type](terminology.md#facet-type):
+`Point as Vector`. While the API of `Point` includes the two fields `x` and `y`
+along with the `Add` and `Scale` methods, the API of `Point as Vector` _only_
+has the `Add` and `Scale` methods of the `Vector` interface. The facet type
+`Point as Vector` is [compatible](terminology.md#compatible-types) with `Point`,
+meaning their data representations are the same, so we allow you to cast between
+the two freely:
+
+```
+var a: Point = (.x = 1.0, .y = 2.0);
+// `a` has `Add` and `Scale` methods:
+a.Add(a.Scale(2.0));
+
+// Cast from Point implicitly
+var b: Point as Vector = a;
+// `b` has `Add` and `Scale` methods:
+b.Add(b.Scale(2.0));
+
+// Will also implicitly cast when calling functions:
+fn F(c: Point as Vector, d: Point) {
+  d.Add(c.Scale(2.0));
+}
+F(a, b);
+
+// Explicit casts
+var z: Point as Vector = (a as (Point as Vector)).Scale(3.0);
+z.Add(b);
+var w: Point = z as Point;
+```
+
+These [casts](terminology.md#subtyping-and-casting) change which names are
+exposed in the type's API, but as much as possible we don't want the meaning of
+any given name to change. Instead we want these casts to simply change the
+subset of names that are visible.
+
+**Note:** In general the above is written assuming that casts are written
+"`a as T`" where `a` is a value and `T` is the type to cast to. When we write
+`Point as Vector`, the value `Point` is a type, and `Vector` is a type of a
+type, or a "type-of-type".
+
+**Note:** A type may implement any number of different interfaces, but may
+provide at most one implementation of any single interface. This makes the act
+of selecting an implementation of an interface for a type unambiguous throughout
+the whole program, so for example `Point as Vector` is well defined.
+
+We don't expect users to ordinarily name facet types explicitly in source code.
+Instead, values are implicitly cast to a facet type as part of calling a generic
+function, as described in the [Generics](#generics) section.
+
+### Implementing multiple interfaces
+
+To implement more than one interface when defining a type, simply include an
+`impl` block per interface.
+
+```
+class Point {
+  var x: Double;
+  var y: Double;
+  impl as Vector {
+    fn Add[me: Self](b: Self) -> Self { ... }
+    fn Scale[me: Self](v: Double) -> Self { ... }
+  }
+  impl as Drawable {
+    fn Draw[me: Self]() { ... }
+  }
+}
+```
+
+In this case, all the functions `Add`, `Scale`, and `Draw` end up a part of the
+API for `Point`. This means you can't implement two interfaces that have a name
+in common (unless you use an `external impl` for one or both, as described
+below).
+
+```
+class GameBoard {
+  impl as Drawable {
+    fn Draw[me: Self]() { ... }
+  }
+  impl as EndOfGame {
+    // Error: `GameBoard` has two methods named
+    // `Draw` with the same signature.
+    fn Draw[me: Self]() { ... }
+    fn Winner[me: Self](player: Int) { ... }
+  }
+}
+```
+
+**Open question:** Should we have some syntax for the case where you want both
+names to be given the same implementation? It seems like that might be a common
+case, but we won't really know if this is an important case until we get more
+experience.
+
+```
+class Player {
+  var name: String;
+  impl as Icon {
+    fn Name[me: Self]() -> String { return this.name; }
+    // ...
+  }
+  impl as GameUnit {
+    // Possible syntax for defining `GameUnit.Name` as
+    // the same as `Icon.Name`:
+    alias Name = Icon.Name;
+    // ...
+  }
+}
+```
+
+### External impl
+
+Interfaces may also be implemented for a type externally, by using the
+`external impl` construct which takes the name of an existing type:
+
+```
+class Point2 {
+  var x: Double;
+  var y: Double;
+}
+
+external impl Point2 as Vector {
+  // In this scope, "Self" is an alias for "Point2".
+  fn Add[me: Self](b: Self) -> Self {
+    return Point2(.x = a.x + b.x, .y = a.y + b.y);
+  }
+  fn Scale[me: Self](v: Double) -> Self {
+    return Point2(.x = a.x * v, .y = a.y * v);
+  }
+}
+```
+
+**References:** The external interface implementation syntax was decided in
+[proposal #553](https://github.com/carbon-language/carbon-lang/pull/553). In
+particular, see
+[the alternatives considered](/proposals/p0553.md#interface-implementation-syntax).
+
+The `external impl` statement is allowed to be defined in a different library
+from `Point2`, restricted by [the coherence/orphan rules](#impl-lookup) that
+ensure that the implementation of an interface won't change based on imports. In
+particular, the `external impl` statement is allowed in the library defining the
+interface (`Vector` in this case) in addition to the library that defines the
+type (`Point2` here). This (at least partially) addresses
+[the expression problem](https://eli.thegreenplace.net/2016/the-expression-problem-and-its-solutions).
+
+We don't want the API of `Point2` to change based on what is imported though. So
+the `external impl` statement does not add the interface's methods to the type.
+It would be particularly bad if two different libraries implemented interfaces
+with conflicting names both affected the API of a single type. The result is you
+can find all the names of direct (unqualified) members of a type in the
+definition of that type. The only thing that may be in another library is an
+`impl` of an interface.
+
+On the other hand, if we cast to the facet type, those methods do become
+visible:
+
+```
+var a: Point2 = (.x = 1.0, .y = 2.0);
+// `a` does *not* have `Add` and `Scale` methods:
+// Error: a.Add(a.Scale(2.0));
+
+// Cast from Point2 implicitly
+var b: Point2 as Vector = a;
+// `b` does have `Add` and `Scale` methods:
+b.Add(b.Scale(2.0));
+
+fn F(c: Point2 as Vector) {
+  // Can call `Add` and `Scale` on `c` even though we can't on `a`.
+  c.Add(c.Scale(2.0));
+}
+F(a);
+```
+
+You might intentionally use `external impl` to implement an interface for a type
+to avoid cluttering the API of that type, for example to avoid a name collision.
+A syntax for reusing method implementations allows us to do this selectively
+when needed:
+
+```
+class Point3 {
+  var x: Double;
+  var y: Double;
+  fn Add[me: Self](b: Self) -> Self {
+    return Point3(.x = a.x + b.x, .y = a.y + b.y);
+  }
+}
+
+external Point3 as Vector {
+  alias Add = Point3.Add;  // Syntax TBD
+  fn Scale[me: Self](v: Double) -> Self {
+    return Point3(.x = a.x * v, .y = a.y * v);
+  }
+}
+```
+
+With this definition, `Point3` includes `Add` in its API but not `Scale`, while
+`Point3 as Vector` includes both. This maintains the property that you can
+determine the API of a type by looking at its definition.
+
+**Rejected alternative:** We could allow types to have different APIs in
+different files based on explicit configuration in that file. For example, we
+could support a declaration that a given interface or a given method of an
+interface is "in scope" for a particular type in this file. With that
+declaration, the method could be called unqualified. This avoids most concerns
+arising from name collisions between interfaces. It has a few downsides though:
+
+-   It increases variability between files, since the same type will have
+    different APIs depending on these declarations. This makes it harder to
+    copy-paste code between files.
+-   It makes reading code harder, since you have to search the file for these
+    declarations that affect name lookup.
+
+**Comparison with other languages:** Both Rust and Swift support external
+implementation.
+[Swift's syntax](https://docs.swift.org/swift-book/LanguageGuide/Protocols.html#ID277)
+does this as an "extension" of the original type. In Rust, all implementations
+are external as in
+[this example](https://doc.rust-lang.org/rust-by-example/trait.html). Unlike
+Swift and Rust, we don't allow a type's API to be modified outside its
+definition. So in Carbon a type's API is consistent no matter what is imported,
+unlike Swift and Rust.
+
+### Qualified member names
+
+Given a value of type `Point2` and an interface `Vector` implemented for that
+type, you can access the methods from that interface using the member's
+_qualified name_, whether or not the implementation is done externally with an
+`external impl` statement:
+
+```
+var p1: Point2 = (.x = 1.0, .y = 2.0);
+var p2: Point2 = (.x = 2.0, .y = 4.0);
+Assert(p1.(Vector.Scale)(2.0) == p2);
+Assert(p1.(Vector.Add)(p1) == p2);
+```
+
+Note that the name in the parens is looked up in the containing scope, not in
+the names of members of `Point2`. So if there was another interface `Drawable`
+with method `Draw` defined in the `Plot` package also implemented for `Point2`,
+as in:
+
+```
+package Plot;
+import Points;
+
+interface Drawable {
+  fn Draw[me: Self]();
+}
+
+external impl Points.Point2 as Drawable { ... }
+```
+
+You could access `Draw` with a qualified name:
+
+```
+import Plot;
+import Points;
+
+var p: Points.Point2 = (.x = 1.0, .y = 2.0);
+p.(Plot.Drawable.Draw)();
+```
+
+**Comparison with other languages:** This is intended to be analogous to, in
+C++, adding `ClassName::` in front of a member name to disambiguate, such as
+[names defined in both a parent and child class](https://stackoverflow.com/questions/357307/how-to-call-a-parent-class-function-from-derived-class-function).
+
+## Generics
+
+Now let us write a function that can accept values of any type that has
+implemented the `Vector` interface:
+
+```
+fn AddAndScaleGeneric[T:! Vector](a: T, b: T, s: Double) -> T {
+  return a.Add(b).Scale(s);
+}
+var v: Point = AddAndScaleGeneric(a, w, 2.5);
+```
+
+Here `T` is a type whose type is `Vector`. The `:!` syntax means that `T` is a
+_[generic parameter](terminology.md#generic-versus-template-parameters)_, that
+is it must be known to the caller but we will only use the information present
+in the signature of the function to typecheck the body of `AddAndScaleGeneric`'s
+definition. In this case, we know that any value of type `T` implements the
+`Vector` interface and so has an `Add` and a `Scale` method.
+
+When we call `AddAndScaleGeneric`, we need to determine the value of `T` to use
+when passed values with type `Point`. Since `T` has type `Vector`, the compiler
+simply sets `T` to `Point as Vector`. This
+[cast](terminology.md#subtyping-and-casting)
+[erases](terminology.md#type-erasure) all of the API of `Point` and substitutes
+the api of `Vector`, without changing anything about the data representation. It
+acts like we called this non-generic function, found by setting `T` to
+`Point as Vector`:
+
+```
+fn AddAndScaleForPointAsVector(
+      a: Point as Vector, b: Point as Vector, s: Double)
+      -> Point as Vector {
+  return a.Add(b).Scale(s);
+}
+// May still be called with Point arguments, due to implicit casts.
+// Similarly the return value can be implicitly cast to a Point.
+var v2: Point = AddAndScaleForPointAsVector(a, w, 2.5);
+```
+
+Since `Point` implements `Vector` inline, `Point` also has definitions for `Add`
+and `Scale`:
+
+```
+fn AddAndScaleForPoint(a: Point, b: Point, s: Double) -> Point {
+  return a.Add(b).Scale(s);
+}
+
+AddAndScaleForPoint(a, w, 2.5);
+```
+
+However, for another type implementing `Vector` but out-of-line using an
+`external impl` statement, such as `Point2`, the situation is different:
+
+```
+fn AddAndScaleForPoint2(a: Point2, b: Point2, s: Double) -> Point2 {
+  // ERROR: `Point2` doesn't have `Add` or `Scale` methods.
+  return a.Add(b).Scale(s);
+}
+```
+
+Even though `Point2` doesn't have `Add` and `Scale` methods, it still implements
+`Vector` and so can still call `AddAndScaleGeneric`:
+
+```
+var a2: Point2 = (.x = 1.0, .y = 2.0);
+var w2: Point2 = (.x = 3.0, .y = 4.0);
+var v3: Point2 = AddAndScaleGeneric(a, w, 2.5);
+```
+
+**References:** The `:!` syntax was accepted in
+[proposal #676](https://github.com/carbon-language/carbon-lang/pull/676).
+
+### Model
+
+The underlying model here is interfaces are
+[type-of-types](terminology.md#type-of-type), in particular, the type of
+[facet types](terminology.md#facet-type):
+
+-   [Interfaces](#interfaces) are types of
+    [witness tables](terminology.md#witness-tables)
+-   Facet types (defined by [Impls](#implementing-interfaces)) are
+    [witness table](terminology.md#witness-tables) values
+-   The compiler rewrites functions with an implicit type argument
+    (`fn Foo[InterfaceName:! T](...)`) to have an actual argument with type
+    determined by the interface, and supplied at the callsite using a value
+    determined by the impl.
+
+For the example above, [the Vector interface](#interfaces) could be thought of
+defining a witness table type like:
+
+```
+class Vector {
+  // Self is the representation type, which is only
+  // known at compile time.
+  var Self:! Type;
+  // `fnty` is **placeholder** syntax for a "function type",
+  // so `Add` is a function that takes two `Self` parameters
+  // and returns a value of type `Self`.
+  var Add: fnty(a: Self, b: Self) -> Self;
+  var Scale: fnty(a: Self, v: Double) -> Self;
+}
+```
+
+The [impl of Vector for Point](#implementing-interfaces) would be a value of
+this type:
+
+```
+var VectorForPoint: Vector  = {
+    .Self = Point,
+    // `lambda` is **placeholder** syntax for defining a
+    // function value.
+    .Add = lambda(a: Point, b: Point) -> Point {
+      return Point(.x = a.x + b.x, .y = a.y + b.y);
+    },
+    .Scale = lambda(a: Point, v: Double) -> Point {
+      return Point(.x = a.x * v, .y = a.y * v);
+    },
+};
+```
+
+Finally we can define a generic function and call it, like
+[`AddAndScaleGeneric` from the "Generics" section](#generics) by making the
+witness table an explicit argument to the function:
+
+```
+fn AddAndScaleGeneric
+    (t:! Vector, a: t.Self, b: t.Self, s: Double) -> t.Self {
+  return t.Scale(t.Add(a, b), s);
+}
+// Point implements Vector.
+var v: Point = AddAndScaleGeneric(VectorForPoint, a, w, 2.5);
+```
+
+The rule is that generic arguments (declared using `:!`) are passed at compile
+time, so the actual value of the `t` argument here can be used to generate the
+code for `AddAndScaleGeneric`. So `AddAndScaleGeneric` is using a
+[static-dispatch witness table](terminology.md#static-dispatch-witness-table).
+
+## Interfaces recap
+
+Interfaces have a name and a definition.
+
+The definition of an interface consists of a set of declarations. Each
+declaration defines a requirement for any `impl` that is in turn a capability
+that consumers of that `impl` can rely on. Typically those declarations also
+have names, useful for both saying how the `impl` satisfies the requirement and
+accessing the capability.
+
+Interfaces are ["nominal"](terminology.md#nominal-interfaces), which means their
+name is significant. So two interfaces with the same body definition but
+different names are different, just like two classes with the same definition
+but different names are considered different types. For example, lets say we
+define another interface, say `LegoFish`, with the same `Add` and `Scale` method
+signatures. Implementing `Vector` would not imply an implementation of
+`LegoFish`, because the `impl` definition explicitly refers to the name
+`Vector`.
+
+An interface's name may be used in a few different contexts:
+
+-   to define [an `impl` for a type](#implementing-interfaces),
+-   as a namespace name in [a qualified name](#qualified-member-names), and
+-   as a [type-of-type](terminology.md#type-of-type) for
+    [a generic type parameter](#generics).
+
+While interfaces are examples of type-of-types, type-of-types are a more general
+concept, for which interfaces are a building block.
+
+## Type-of-types and facet types
+
+A [type-of-type](terminology.md#type-of-type) consists of a set of requirements
+and a set of names. Requirements are typically a set of interfaces that a type
+must satisfy (though other kinds of requirements are added below). The names are
+aliases for qualified names in those interfaces.
+
+An interface is one particularly simple example of a type-of-type. For example,
+`Vector` as a type-of-type has a set of requirements consisting of the single
+interface `Vector`. Its set of names consists of `Add` and `Scale` which are
+aliases for the corresponding qualified names inside `Vector` as a namespace.
+
+The requirements determine which types may be cast to a given type-of-type. The
+result of casting a type `T` to a type-of-type `I` (written `T as I`) is called
+a facet type, you might say a facet type `F` is the `I` facet of `T` if `F` is
+`T as I`. The API of `F` is determined by the set of names in the type-of-type.
+
+This general structure of type-of-types holds not just for interfaces, but
+others described in the rest of this document.
+
+## Structural interfaces
+
+If the nominal interfaces discussed above are the building blocks for
+type-of-types, [structural interfaces](terminology.md#structural-interfaces)
+describe how they may be composed together. Unlike nominal interfaces, the name
+of a structural interface is not a part of its value. Two different structural
+interfaces with the same definition are equivalent even if they have different
+names. This is because types don't explicitly specify which structural
+interfaces they implement, types automatically implement any structural
+interfaces they can satisfy.
+
+A structural interface definition can contain interface requirements using
+`impl` declarations and names using `alias` declarations. Note that this allows
+us to declare the aspects of a type-of-type directly.
+
+```
+structural interface VectorLegoFish {
+  // Interface implementation requirements
+  impl as Vector;
+  impl as LegoFish;
+  // Names
+  alias Scale = Vector.Scale;
+  alias VAdd = Vector.Add;
+  alias LFAdd = LegoFish.Add;
+}
+```
+
+We don't expect users do directly define many structural interfaces, but other
+constructs we do expect them to use will be defined in terms of them. For
+example, we can define the Carbon builtin `Type` as:
+
+```
+structural interface Type { }
+```
+
+That is, `Type` is the type-of-type with no requirements (so matches every
+type), and defines no names.
+
+```
+fn Identity[T:! Type](x: T) -> T {
+  // Can accept values of any type. But, since we no nothing about the
+  // type, we don't know about any operations on `x` inside this function.
+  return x;
+}
+
+var i: Int = Identity(3);
+var s: String = Identity("string");
+```
+
+**Aside:** We can define `auto` as syntactic sugar for `(template _:! Type)`.
+This definition allows you to use `auto` as the type for a local variable whose
+type can be statically determined by the compiler. It also allows you to use
+`auto` as the type of a function parameter, to mean "accepts a value of any
+type, and this function will be instantiated separately for every different
+type." This is consistent with the
+[use of `auto` in the C++20 Abbreviated function template feature](https://en.cppreference.com/w/cpp/language/function_template#Abbreviated_function_template).
+
+In general we should support the same kinds of declarations in a
+`structural interface` definitions as in an `interface`. Generally speaking
+declarations in one kind of interface make sense in the other, and there is an
+analogy between them. If an `interface` `I` has (non-`alias`) declarations `X`,
+`Y`, and `Z`, like so:
+
+```
+interface I {
+  X;
+  Y;
+  Z;
+}
+```
+
+(Here, `X` could be something like `fn F[me: Self]()`.)
+
+Then a type implementing `I` would have `impl as I` with definitions for `X`,
+`Y`, and `Z`, as in:
+
+```
+class ImplementsI {
+  // ...
+  impl as I {
+    X { ... }
+    Y { ... }
+    Z { ... }
+  }
+}
+```
+
+But the corresponding `structural interface`, `S`:
+
+```
+structural interface S {
+  X;
+  Y;
+  Z;
+}
+```
+
+would match any type with definitions for `X`, `Y`, and `Z` directly:
+
+```
+class ImplementsS {
+  // ...
+  X { ... }
+  Y { ... }
+  Z { ... }
+}
+```
+
+### Subtyping between type-of-types
+
+There is a subtyping relationship between type-of-types that allows you to call
+one generic function from another as long as you are calling a function with a
+subset of your requirements.
+
+Given a generic type `T` with type-of-type `I1`, it may be
+[implicitly cast](terminology.md#subtyping-and-casting) to a type-of-type `I2`,
+resulting in `T as I2`, as long as the requirements of `I1` are a superset of
+the requirements of `I2`. Further, given a value `x` of type `T`, it can be
+implicitly cast to `T as I2`. For example:
+
+```
+interface Printable { fn Print[me: Self](); }
+interface Renderable { fn Draw[me: Self](); }
+
+structural interface PrintAndRender {
+  impl as Printable;
+  impl as Renderable;
+}
+structural interface JustPrint {
+  impl as Printable;
+}
+
+fn PrintIt[T2:! JustPrint](x2: T2) {
+  x2.(Printable.Print)();
+}
+fn PrintDrawPrint[T1:! PrintAndRender](x1: T1) {
+  // x1 implements `Printable` and `Renderable`.
+  x1.(Printable.Print)();
+  x1.(Renderable.Draw)();
+  // Can call `PrintIt` since `T1` satisfies `JustPrint` since
+  // it implements `Printable` (in addition to `Renderable`).
+  // This calls `PrintIt` with `T2 == T1 as JustPrint` and
+  // `x2 == x1 as T2`.
+  PrintIt(x1);
+}
+```
+
+## Combining interfaces by anding type-of-types
+
+In order to support functions that require more than one interface to be
+implemented, we provide a combination operator on type-of-types, written `&`.
+This operator gives the type-of-type with the union of all the requirements and
+the union of the names minus any conflicts.
+
+```
+interface Printable {
+  fn Print[me: Self]();
+}
+interface Renderable {
+  fn Center[me: Self]() -> (Int, Int);
+  fn Draw[me: Self]();
+}
+
+// `Printable & Renderable` is syntactic sugar for this type-of-type:
+structural interface {
+  impl as Printable;
+  impl as Renderable;
+  alias Print = Printable.Print;
+  alias Center = Renderable.Center;
+  alias Draw = Renderable.Draw;
+}
+
+fn PrintThenDraw[T:! Printable & Renderable](x: T) {
+  // Can use methods of `Printable` or `Renderable` on `x` here.
+  x.Print();  // Same as `x.(Printable.Print)();`.
+  x.Draw();  // Same as `x.(Renderable.Draw)();`.
+}
+
+class Sprite {
+  // ...
+  impl as Printable {
+    fn Print[me: Self]() { ... }
+  }
+  impl as Renderable {
+    fn Center[me: Self]() -> (Int, Int) { ... }
+    fn Draw[me: Self]() { ... }
+  }
+}
+
+var s: Sprite = ...;
+PrintThenDraw(s);
+```
+
+Any conflicting names between the two types are replaced with a name that is an
+error to use.
+
+```
+interface Renderable {
+  fn Center[me: Self]() -> (Int, Int);
+  fn Draw[me: Self]();
+}
+interface EndOfGame {
+  fn Draw[me: Self]();
+  fn Winner[me: Self](player: Int);
+}
+// `Renderable & EndOfGame` is syntactic sugar for this type-of-type:
+structural interface {
+  impl as Renderable;
+  impl as EndOfGame;
+  alias Center = Renderable.Center;
+  // Open question: `forbidden`, `invalid`, or something else?
+  forbidden Draw
+    message "Ambiguous, use either `(Renderable.Draw)` or `(EndOfGame.Draw)`.";
+  alias Winner = EndOfGame.Winner;
+}
+```
+
+Conflicts can be resolved at the call site using
+[the qualified name syntax](#qualified-member-names), or by defining a
+structural interface explicitly and renaming the methods:
+
+```
+structural interface RenderableAndEndOfGame {
+  impl as Renderable;
+  impl as EndOfGame;
+  alias Center = Renderable.Center;
+  alias RenderableDraw = Renderable.Draw;
+  alias TieGame = EndOfGame.Draw;
+  alias Winner = EndOfGame.Winner;
+}
+
+fn RenderTieGame[T:! RenderableAndEndOfGame](x: T) {
+  // Calls Renderable.Draw()
+  x.RenderableDraw();
+  // Calls EndOfGame.Draw()
+  x.TieGame();
+}
+```
+
+Reserving the name when there is a conflict is part of resolving what happens
+when you combine more than two type-of-types. If `x` is forbidden in `A`, it is
+forbidden in `A & B`, whether or not `B` defines the name `x`. This makes `&`
+associative and commutative, and so it is well defined on sets of interfaces, or
+other type-of-types, independent of order.
+
+Note that we do _not_ consider two type-of-types using the same name to mean the
+same thing to be a conflict. For example, combining a type-of-type with itself
+gives itself, `MyTypeOfType & MyTypeOfType == MyTypeOfType`. Also, given two
+[interface extensions](#interface-extension) of a common base interface, the sum
+should not conflict on any names in the common base.
+
+**Rejected alternative:** Instead of using `&` as the combining operator, we
+considered using `+`,
+[like Rust](https://rust-lang.github.io/rfcs/0087-trait-bounds-with-plus.html).
+See [#531](https://github.com/carbon-language/carbon-lang/issues/531) for the
+discussion.
+
+**Future work:** We may want to define another operator on type-of-types for
+adding requirements to a type-of-type without affecting the names, and so avoid
+the possibility of name conflicts. Note this means the operation is not
+commutative. If we call this operator `[&]`, then `A [&] B` has the names of `A`
+and `B [&] A` has the names of `B`.
+
+```
+// `Printable [&] Renderable` is syntactic sugar for this type-of-type:
+structural interface {
+  impl as Printable;
+  impl as Renderable;
+  alias Print = Printable.Print;
+}
+
+// `Renderable [&] EndOfGame` is syntactic sugar for this type-of-type:
+structural interface {
+  impl as Renderable;
+  impl as EndOfGame;
+  alias Center = Renderable.Center;
+  alias Draw = Renderable.Draw;
+}
+```
+
+Note that all three expressions `A & B`, `A [&] B`, and `B [&] A` have the same
+requirements, and so you would be able to switch a function declaration between
+them without affecting callers.
+
+Nothing in this design depends on the `[&]` operator, and having both `&` and
+`[&]` might be confusing for users, so it makes sense to postpone implementing
+`[&]` until we have a demonstrated need. The `[&]` operator seems most useful
+for adding requirements for interfaces used for
+[operator overloading](#operator-overloading), where merely implementing the
+interface is enough to be able to use the operator to access the functionality.
+
+**Alternatives considered:** See
+[Carbon: Access to interface methods](https://docs.google.com/document/d/1u_i_s31OMI_apPur7WmVxcYq6MUXsG3oCiKwH893GRI/edit?usp=sharing&resourcekey=0-0lzSNebBMtUBi4lStL825g).
+
+**Comparison with other languages:** This `&` operation on interfaces works very
+similarly to Rust's `+` operation, with the main difference being how you
+[qualify names when there is a conflict](https://doc.rust-lang.org/rust-by-example/trait/disambiguating.html).
+
+## Interface requiring other interfaces
+
+Some interfaces will depend on other interfaces being implemented for the same
+type. For example, in C++,
+[the `Container` concept](https://en.cppreference.com/w/cpp/named_req/Container#Other_requirements)
+requires all containers to also satisfy the requirements of
+`DefaultConstructible`, `CopyConstructible`, `EqualityComparable`, and
+`Swappable`. This is already a capability for
+[type-of-types in general](#type-of-types-and-facet-types). For consistency we
+will use the same semantics and syntax as we do for
+[structural interfaces](#structural-interfaces):
+
+```
+interface Equatable { fn Equals[me: Self](that: Self) -> Bool; }
+
+interface Iterable {
+  fn Advance[addr me: Self*]() -> Bool;
+  impl as Equatable;
+}
+
+def DoAdvanceAndEquals[T:! Iterable](x: T) {
+  // `x` has type `T` that implements `Iterable`, and so has `Advance`.
+  x.Advance();
+  // `Iterable` requires an implementation of `Equatable`,
+  // so `T` also implements `Equatable`.
+  x.(Equatable.Equals)(x);
+}
+
+class Iota {
+  impl as Iterable { fn Advance[me: Self]() { ... } }
+  impl as Equatable { fn Equals[me: Self](that: Self) -> Bool { ... } }
+}
+var x: Iota;
+DoAdvanceAndEquals(x);
+```
+
+Like with structural interfaces, an interface implementation requirement doesn't
+by itself add any names to the interface, but again those can be added with
+`alias` declarations:
+
+```
+interface Hashable {
+  fn Hash[me: Self]() -> UInt64;
+  impl as Equatable;
+  alias Equals = Equatable.Equals;
+}
+
+def DoHashAndEquals[T:! Hashable](x: T) {
+  // Now both `Hash` and `Equals` are available directly:
+  x.Hash();
+  x.Equals(x);
+}
+```
+
+**Comparison with other languages:**
+[This feature is called "Supertraits" in Rust](https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#using-supertraits-to-require-one-traits-functionality-within-another-trait).
+
+### Interface extension
+
+When implementing an interface, we should allow implementing the aliased names
+as well. In the case of `Hashable` above, this includes all the members of
+`Equatable`, obviating the need to implement `Equatable` itself:
+
+```
+class Song {
+  impl as Hashable {
+    fn Hash[me: Self]() -> UInt64 { ... }
+    fn Equals[me: Self](that: Self) -> Bool { ... }
+  }
+}
+var y: Song;
+DoHashAndEquals(y);
+```
+
+This allows us to say that `Hashable`
+["extends"](terminology.md#extending-an-interface) `Equatable`, with some
+benefits:
+
+-   This allows `Equatable` to be an implementation detail of `Hashable`.
+-   This allows types implementing `Hashable` to implement all of its API in one
+    place.
+-   This reduces the boilerplate for types implementing `Hashable`.
+
+We expect this concept to be common enough to warrant dedicated syntax:
+
+```
+interface Equatable { fn Equals[me: Self](that: Self) -> Bool; }
+
+interface Hashable {
+  extends Equatable;
+  fn Hash[me: Self]() -> UInt64;
+}
+// is equivalent to the definition of Hashable from before:
+// interface Hashable {
+//   impl as Equatable;
+//   alias Equals = Equatable.Equals;
+//   fn Hash[me: Self]() -> UInt64;
+// }
+```
+
+No names in `Hashable` are allowed to conflict with names in `Equatable` (unless
+those names are marked as `upcoming` or `deprecated` as in
+[evolution future work](#evolution)). Hopefully this won't be a problem in
+practice, since interface extension is a very closely coupled relationship, but
+this may be something we will have to revisit in the future.
+
+Examples:
+
+-   The C++
+    [Boost.Graph library](https://www.boost.org/doc/libs/1_74_0/libs/graph/doc/)
+    [graph concepts](https://www.boost.org/doc/libs/1_74_0/libs/graph/doc/graph_concepts.html#fig:graph-concepts)
+    has many refining relationships between concepts.
+    [Carbon generics use case: graph library](https://docs.google.com/document/d/1xk0GLtpBl2OOnf3F_6Z-A3DtTt-r7wdOZ5wPipYUSO0/edit?usp=sharing&resourcekey=0-mBSmwn6b6jwbLaQw2WG6OA)
+    shows how those concepts might be translated into Carbon interfaces.
+-   The [C++ concepts](https://en.cppreference.com/w/cpp/named_req) for
+    containers, iterators, and concurrency include many requirement
+    relationships.
+-   Swift protocols, such as
+    [Collection](https://developer.apple.com/documentation/swift/collection).
+
+To write an interface extending multiple interfaces, use multiple `extends`
+declarations. For example, the
+[`BinaryInteger` protocol in Swift](https://developer.apple.com/documentation/swift/binaryinteger)
+inherits from `CustomStringConvertible`, `Hashable`, `Numeric`, and `Stridable`.
+The [`SetAlgeba` protocol](https://swiftdoc.org/v5.1/protocol/setalgebra/)
+extends `Equatable` and `ExpressibleByArrayLiteral`, which would be declared in
+Carbon:
+
+```
+interface SetAlgebra {
+  extends Equatable;
+  extends ExpressibleByArrayLiteral;
+}
+```
+
+**Alternative considered:** The `extends` declarations are in the body of the
+`interface` definition instead of the header so we can use
+[associated types (defined below)](#associated-types) also defined in the body
+in parameters or constraints of the interface being extended.
+
+```
+// A type can implement `ConvertibleTo` many times, using
+// different values of `T`.
+interface ConvertibleTo(T:! Type) { ... }
+
+// A type can only implement `PreferredConversion` once.
+interface PreferredConversion {
+  let AssociatedType: Type;
+  extends ConvertibleTo(AssociatedType);
+}
+```
+
+#### `extends` and `impl` with structural interfaces
+
+The `extends` declaration makes sense with the same meaning inside a
+[`structural interface`](#structural-interfaces), and so is also supported.
+
+```
+interface Media {
+  fn Play[me: Self]();
+}
+interface Job {
+  fn Run[me: Self]();
+}
+
+structural interface Combined {
+  extends Media;
+  extends Job;
+}
+```
+
+This definition of `Combined` is equivalent to requiring both the `Media` and
+`Job` interfaces being implemented, and aliases their methods.
+
+```
+// Equivalent
+structural interface Combined {
+  impl as Media;
+  alias Play = Media.Play;
+  impl as Job;
+  alias Run = Job.Run;
+}
+```
+
+Notice how `Combined` has aliases for all the methods in the interfaces it
+requires. That condition is sufficient to allow a type to `impl` the structural
+interface:
+
+```
+class Song {
+  impl as Combined {
+    fn Play[me: Self]() { ... }
+    fn Run[me: Self]() { ... }
+  }
+}
+```
+
+This is equivalent to implementing the required interfaces directly:
+
+```
+class Song {
+  impl as Media {
+    fn Play[me: Self]() { ... }
+  }
+  impl as Job {
+    fn Run[me: Self]() { ... }
+  }
+}
+```
+
+This is just like you get an implementation of `Equatable` by implementing
+`Hashable` when `Hashable` extends `Equatable`. This provides a tool useful for
+[evolution](#evolution).
+
+Conversely, an `interface` can extend a `structural interface`:
+
+```
+interface MovieCodec {
+  extends Combined;
+
+  fn Load[addr me: Self*](filename: String);
+}
+```
+
+This gives `MovieCodec` the same requirements and names as `Combined`, and so is
+equivalent to:
+
+```
+interface MovieCodec {
+  impl as Media;
+  alias Play = Media.Play;
+  impl as Job;
+  alias Run = Job.Run;
+
+  fn Load[addr me: Self*](filename: String);
+}
+```
+
+#### Diamond dependency issue
+
+Consider this set of interfaces, simplified from
+[this example generic graph library doc](https://docs.google.com/document/d/1xk0GLtpBl2OOnf3F_6Z-A3DtTt-r7wdOZ5wPipYUSO0/edit?resourcekey=0-mBSmwn6b6jwbLaQw2WG6OA#):
+
+```
+interface Graph {
+  fn Source[addr me: Self*](e: EdgeDescriptor) -> VertexDescriptor;
+  fn Target[addr me: Self*](e: EdgeDescriptor) -> VertexDescriptor;
+}
+
+interface IncidenceGraph {
+  extends Graph;
+  fn OutEdges[addr me: Self*](u: VertexDescriptor)
+    -> (EdgeIterator, EdgeIterator);
+}
+
+interface EdgeListGraph {
+  extends Graph;
+  fn Edges[addr me: Self*]() -> (EdgeIterator, EdgeIterator);
+}
+```
+
+We need to specify what happens when a graph type implements both
+`IncidenceGraph` and `EdgeListGraph`, since both interfaces extend the `Graph`
+interface.
+
+```
+class MyEdgeListIncidenceGraph {
+  impl as IncidenceGraph { ... }
+  impl as EdgeListGraph { ... }
+}
+```
+
+The rule is that we need one definition of each method of `Graph`. Each method
+though could be defined in the `impl` block of `IncidenceGraph`,
+`EdgeListGraph`, or `Graph`. These would all be valid:
+
+-   `IncidenceGraph` implements all methods of `Graph`, `EdgeListGraph`
+    implements none of them.
+
+```
+class MyEdgeListIncidenceGraph {
+  impl as IncidenceGraph {
+    fn Source[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+    fn Target[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+    fn OutEdges[addr me: Self*](u: VertexDescriptor)
+        -> (EdgeIterator, EdgeIterator) { ... }
+  }
+  impl as EdgeListGraph {
+    fn Edges[addr me: Self*]() -> (EdgeIterator, EdgeIterator) { ... }
+  }
+}
+```
+
+-   `IncidenceGraph` and `EdgeListGraph` implement all methods of `Graph`
+    between them, but with no overlap.
+
+```
+class MyEdgeListIncidenceGraph {
+  impl as IncidenceGraph {
+    fn Source[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+    fn OutEdges[addr me: Self*](u: VertexDescriptor)
+        -> (EdgeIterator, EdgeIterator) { ... }
+  }
+  impl as EdgeListGraph {
+    fn Target[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+    fn Edges[addr me: Self*]() -> (EdgeIterator, EdgeIterator) { ... }
+  }
+}
+```
+
+-   Explicitly implementing `Graph`.
+
+```
+class MyEdgeListIncidenceGraph {
+  impl as Graph {
+    fn Source[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+    fn Target[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+  }
+  impl as IncidenceGraph { ... }
+  impl as EdgeListGraph { ... }
+}
+```
+
+-   Implementing `Graph` externally.
+
+```
+class MyEdgeListIncidenceGraph {
+  impl as IncidenceGraph { ... }
+  impl as EdgeListGraph { ... }
+}
+external impl as Graph {
+  fn Source[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+  fn Target[me: Self](e: EdgeDescriptor) -> VertexDescriptor { ... }
+}
+```
+
+This last point means that there are situations where we can only detect a
+missing method definition by the end of the file. This doesn't delay other
+aspects of semantic checking, which will just assume that these methods will
+eventually be provided.
+
+### Use case: overload resolution
+
+Implementing an extended interface is an example of a more specific match for
+[lookup resolution](#lookup-resolution-and-specialization). For example, this
+could be used to provide different implementations of an algorithm depending on
+the capabilities of the iterator being passed in:
+
+```
+interface ForwardIntIterator {
+  fn Advance[addr me: Self*]();
+  fn Get[me: Self]() -> Int;
+}
+interface BidirectionalIntIterator {
+  extends ForwardIntIterator;
+  fn Back[addr me: Self*]();
+}
+interface RandomAccessIntIterator {
+  extends BidirectionalIntIterator;
+  fn Skip[addr me: Self*](offset: Int);
+  fn Difference[me: Self](that: Self) -> Int;
+}
+
+fn SearchInSortedList[IterT:! ForwardIntIterator]
+    (begin: IterT, end: IterT, needle: Int) -> Bool {
+  ... // does linear search
+}
+// Will prefer the following overload when it matches
+// since it is more specific.
+fn SearchInSortedList[IterT:! RandomAccessIntIterator]
+    (begin: IterT, end: IterT, needle: Int) -> Bool {
+  ... // does binary search
+}
+```
+
+This would be an example of the more general rule that an interface `A`
+requiring an implementation of interface `B` means `A` is more specific than
+`B`.
+
+## Type compatibility
+
+None of the casts between facet types change the implementation of any
+interfaces for a type. So the result of a cast does not depend on the sequence
+of casts you perform, just the original type and the final type-of-type. That
+is, these types will all be equal:
+
+-   `T as I`
+-   `(T as A) as I`
+-   `(((T as A) as B) as C) as I`
+
+Now consider a type with a generic type parameter, like a hash map type:
+
+```
+interface Hashable { ... }
+class HashMap(KeyT:! Hashable, ValueT:! Type) { ... }
+```
+
+If we write something like `HashMap(String, Int)` the type we actually get is:
+
+```
+HashMap(String as Hashable, Int as Type)
+```
+
+This is the same type we will get if we pass in some other facet types in, so
+all of these types are equal:
+
+-   `HashMap(String, Int)`
+-   `HashMap(String as Hashable, Int as Type)`
+-   `HashMap((String as Printable) as Hashable, Int)`
+-   `HashMap((String as Printable & Hashable) as Hashable, Int)`
+
+This means we don't generally need to worry about getting the wrong facet type
+as the argument for a generic type. This means we don't get type mismatches when
+calling functions as in this example, where the type parameters have different
+constraints than the type requires:
+
+```
+fn PrintValue
+    [KeyT:! Printable & Hashable, ValueT:! Printable]
+    (map: HashMap(KeyT, ValueT), key: KeyT) { ... }
+
+var m: HashMap(String, Int);
+PrintValue(m, "key");
+```
+
+## Future work
+
+### Adapting types
+
+Since interfaces may only be implemented for a type once, and we limit where
+implementations may be added to a type, there is a need to allow the user to
+switch the type of a value to access different interface implementations. See
+["adapting a type" in the terminology document](terminology.md#adapting-a-type).
+
+### Associated constants
+
+In addition to associated methods, we will allow other kinds of associated items
+associating values with types implementing an interface.
+
+### Associated types
+
+Associated types are associated constants that happen to be types. These are
+particularly interesting since they can be used in the signatures of associated
+methods or functions, to allow the signatures of methods to vary from
+implementation to implementation.
+
+### Parameterized interfaces
+
+Associated types don't change the fact that a type can only implement an
+interface at most once. If instead you want a family of related interfaces, each
+of which could be implemented for a given type, you could use parameterized
+interfaces instead.
+
+#### Impl lookup
+
+We will have rules limiting where interface implementations are defined for
+coherence.
+
+### Constraints
+
+We will need to be able to express constraints beyond "type implements these
+interfaces."
+
+### Conditional conformance
+
+[The problem](terminology.md#conditional-conformance) we are trying to solve
+here is expressing that we have an `impl` of some interface for some type, but
+only if some additional type restrictions are met.
+
+### Parameterized impls
+
+Also known as "blanket `impl`s", these are when you have an `impl` definition
+that is parameterized so it applies to more than a single type and interface
+combination.
+
+#### Lookup resolution and specialization
+
+For this to work, we need a rule that picks a single `impl` in the case where
+there are multiple `impl` definitions that match a particular type and interface
+combination.
+
+### Other constraints as type-of-types
+
+There are some constraints that we will naturally represent as named
+type-of-types that the user can specify.
+
+#### Sized types and type-of-types
+
+Like Rust, we may have types that have values whose size is only determined at
+runtime. Many functions may want to restrict to types with known size.
+
+### Dynamic types
+
+Generics provide enough structure to support runtime dispatch for values with
+types that vary at runtime, without giving up type safety. Both Rust and Swift
+have demonstrated the value of this feature.
+
+#### Runtime type parameters
+
+This feature is about allowing a function's type parameter to be passed in as a
+dynamic (non-generic) parameter. All values of that type would still be required
+to have the same type.
+
+#### Runtime type fields
+
+Instead of passing in a single type parameter to a function, we could store a
+type per value. This changes the data layout of the value, and so is a somewhat
+more invasive change. It also means that when a function operates on multiple
+values they could have different real types.
+
+### Abstract return types
+
+This lets you return am anonymous type implementing an interface from a
+function.
+[Rust has this feature](https://rust-lang.github.io/rfcs/1522-conservative-impl-trait.html).
+
+### Interface defaults
+
+Rust supports specifying defaults for
+[interface parameters](https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#default-generic-type-parameters-and-operator-overloading),
+[methods](https://doc.rust-lang.org/book/ch10-02-traits.html#default-implementations),
+[associated constants](https://doc.rust-lang.org/reference/items/associated-items.html#associated-constants-examples).
+We should support this too. It is helpful for evolution, as well as reducing
+boilerplate. Defaults address the gap between the minimum necessary for a type
+to provide the desired functionality of an interface and the breadth of API that
+user's desire.
+
+### Evolution
+
+There are a collection of use cases for making different changes to interfaces
+that are already in use. These should be addressed either by describing how they
+can be accomplished with existing generics features, or by adding features.
+
+In addition, evolution from (C++ or Carbon) templates to generics needs to be
+supported and made safe.
+
+### Testing
+
+The idea is that you would write tests alongside an interface that validate the
+expected behavior of any type implementing that interface.
+
+### Operator overloading
+
+We will need a story for defining how an operation is overloaded for a type by
+implementing an interface for that type.
+
+### Impls with state
+
+A feature we might consider where an `impl` itself can have state.
+
+### Generic associated types and higher-ranked types
+
+This would be some way to express the requirement that there is a way to go from
+a type to an implementation of an interface parameterized by that type.
+
+#### Generic associated types
+
+Generic associated types are about when this is a requirement of an interface.
+
+#### Higher-ranked types
+
+Higher-ranked types are used to represent this requirement in a function
+signature.
+
+### Field requirements
+
+We might want to allow interfaces to express the requirement that any
+implementing type has a particular field. This would be to match the
+expressivity of inheritance, which can express "all subtypes start with this
+list of fields."
+
+### Generic type specialization
+
+See [generic specialization](terminology.md#generic-specialization) for a
+description of what this might involve.
+
+### Bridge for C++ customization points
+
+See details in [the goals document](goals.md#bridge-for-c-customization-points).
+
+### Reverse generics for return types
+
+In Rust this is
+[return type of "`impl Trait`"](https://rust-lang.github.io/rfcs/1522-conservative-impl-trait.html).
+In Swift,
+[this feature is in discussion](https://forums.swift.org/t/improving-the-ui-of-generics/22814#heading--reverse-generics).
+Swift is considering spelling this `<V: Collection> V` or `some Collection`.
+
+### Variadic arguments
+
+Some facility for allowing a function to generically take a variable number of
+arguments.
diff --git a/proposals/README.md b/proposals/README.md
index 616c294ac55dd..2a4bce6d06ac9 100644
--- a/proposals/README.md
+++ b/proposals/README.md
@@ -58,6 +58,7 @@ request:
 -   [0524 - Generics overview](p0524.md)
 -   [0538 - `return` with no argument](p0538.md)
 -   [0540 - Remove `Void`](p0540.md)
+-   [0553 - Generics details part 1](p0553.md)
 -   [0555 - Operator precedence](p0555.md)
 -   [0601 - Operator tokens](p0601.md)
 -   [0618 - var ordering](p0618.md)
diff --git a/proposals/p0553.md b/proposals/p0553.md
new file mode 100644
index 0000000000000..f010e3215745d
--- /dev/null
+++ b/proposals/p0553.md
@@ -0,0 +1,205 @@
+# Generics details part 1
+
+<!--
+Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+Exceptions. See /LICENSE for license information.
+SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+-->
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/553)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Rationale based on Carbon's goals](#rationale-based-on-carbons-goals)
+-   [Alternatives considered](#alternatives-considered)
+    -   [Interface implementation syntax](#interface-implementation-syntax)
+        -   [`for` instead of `as` in external `impl`](#for-instead-of-as-in-external-impl)
+        -   [No `as` for inline `impl`](#no-as-for-inline-impl)
+        -   [No `external` for external `impl`](#no-external-for-external-impl)
+        -   [Out-of-line impl](#out-of-line-impl)
+        -   [`extend` blocks](#extend-blocks)
+    -   [Others](#others)
+
+<!-- tocstop -->
+
+## Problem
+
+We want to Carbon to have a high quality generics feature that achieves the
+goals set out in [#24](https://github.com/carbon-language/carbon-lang/pull/24).
+This is too big to land in a single proposal. This proposal goes into the
+details of the core of the feature, and provides an outline covering future
+work. It covers:
+
+-   interfaces
+-   implementing interfaces for types
+-   resolving name conflicts
+-   facet types
+-   type-types as the way of describing type variables
+-   structural interfaces
+-   combining interfaces
+-   interface requirements and extension
+-   type compatibility
+
+## Background
+
+This is a follow on to these previous generics proposals:
+
+-   [Generics goals #24](https://github.com/carbon-language/carbon-lang/pull/24)
+-   [Generics terminology #447](https://github.com/carbon-language/carbon-lang/pull/447)
+-   [Generics overview #524](https://github.com/carbon-language/carbon-lang/pull/524)
+
+The content for this proposal was extracted from a larger
+[Generics combined draft proposal](https://github.com/carbon-language/carbon-lang/pull/36).
+
+## Proposal
+
+This is a proposal to add
+[this detailed design document](/docs/design/generics/details.md).
+
+## Rationale based on Carbon's goals
+
+Much of this rationale was captured in the
+[Generics goals proposal](https://github.com/carbon-language/carbon-lang/pull/24).
+
+## Alternatives considered
+
+### Interface implementation syntax
+
+The interface implementation syntax was decided in
+[question-for-leads issue #575](https://github.com/carbon-language/carbon-lang/issues/575).
+
+```
+struct Song {
+  // data and methods ...
+  impl as Printable {
+    method (me: Self) Print() { ... }
+  }
+}
+external impl Song as Comparable { ... }
+```
+
+This proposal includes additional discussion and additional alternatives.
+
+#### `for` instead of `as` in external `impl`
+
+In this option, the interface name comes before the type name.
+
+```
+struct Song { ... }
+external impl Comparable for Song { ... }
+```
+
+Advantage:
+
+-   This ordering used by Rust.
+
+Disadvantages:
+
+-   We prefer the type name before the interface name (using `as`), since having
+    the type first and outer is consistent with those implemented in `struct`
+    declarations. It also seems more natural to express the parameters to the
+    interface in terms of the parameters and associated items of the type than
+    the other way around.
+-   The `Song as Comparable` phrase is the name of the facet type that is being
+    implemented.
+
+#### No `as` for inline `impl`
+
+```
+struct Song {
+  // data and methods ...
+  impl Printable {
+    method (me: Self) Print() { ... }
+  }
+}
+```
+
+Advantage:
+
+-   More concise, so less to read and write.
+
+Disadvantage:
+
+-   Less consistent with the `external impl` syntax.
+-   Less consistent with the planned inline conditional impl syntax.
+
+#### No `external` for external `impl`
+
+```
+struct Song { ... }
+impl Song as Comparable { ... }
+```
+
+Advantage:
+
+-   More concise, so less to read and write.
+
+Disadvantages:
+
+-   Less explicit that the the methods of this impl definition are not
+    contributing to unqualified API of the type.
+-   This kind of implementation is naturally referred to as "external",
+    especially when contrasting with "inline impl".
+
+#### Out-of-line impl
+
+We considered an out-of-line syntax for declaring and defining interface `impl`
+blocks, to be consistent with the `external impl` declarations. For example:
+
+```
+struct Song { ... }
+impl Printable for Song { ... }
+external impl Comparable for Song { ... }
+```
+
+The main advantage of this syntax was that it was uniform across many cases,
+including [conditional conformance](details.md#conditional-conformance). It
+wasn't ideal across a number of dimensions though.
+
+-   It repeated the type name which was redundant and verbose
+-   It could affect the API of the type outside of the type definition.
+
+#### `extend` blocks
+
+Instead of the `external impl` statement, we considered putting all external
+implementations in an `expand` block.
+
+```
+struct Song {
+  impl Printable { ... }
+}
+expand Song {
+  impl Comparable { ... }
+}
+```
+
+Advantages:
+
+-   This option is most similar to the
+    [approach used by Swift](https://docs.swift.org/swift-book/LanguageGuide/Protocols.html#ID277).
+-   Easier to copy-paste an `impl` between a `struct` definition and an `expand`
+    block.
+
+The `expand` approach had some disadvantages:
+
+-   Implementations were indented more than the `external impl` approach.
+-   Extra ceremony in the case of only implementing one type for an interface.
+    This case is expected to be common since external implementations will most
+    often be defined with the interface.
+-   When implementing multiple interfaces in a single `expand` block, the name
+    of the type being expanded could be far from the `impl` declaration and hard
+    to find.
+
+We originally used `extend` instead of `expand` but that collided with using
+`extends` for interface extension and derived classes.
+
+### Others
+
+Other alternatives considered will be in a future proposal. Some of them can be
+seen in a rough form in
+[#36](https://github.com/carbon-language/carbon-lang/pull/36).