A friendly and relaxed place for online discussions about anything related to homotopy type theory. We discuss both formal and informal approaches, and we work with Coq, Agda, Cubical TT, and other systems.