# nLab complete loop graph

Contents

category theory

## In higher category theory

#### Graph theory

graph theory

graph

category of simple graphs

# Contents

## Definition

A complete loop graph is a loop graph? $G$ where between any two vertices $a:G$ and $b:G$ there is exactly one edge $p:a \to_G b$.

In the context of homotopy type theory, a complete loop graph is a type $G$ with a type family $\to_G$ such that the dependent type $a \to_G b$ is a contractible type for all elements $a:G$ and $b:G$.

A complete loop graph is univalent, a subsingleton, or a proposition if the canonical function

$idtoedge:(a =_G b) \to (a \to_G b)$

is an equivalence of types.