Welcome to setoid-hell and record-spaghetti This repository is an exploration into categories with families based on E-categories and some experiments with initiality. Written by Simon Huber in 2018.