Post #2775977

@ncf@types.pl @jonmsterling@mathstodon.xyz @totbwf@types.pl @jeanas@mathstodon.xyz All of IR, II and HII types can be specified in terms of eliminators. The only relevant thing that's missing from literature is HII eliminators in cubical TTs.