Symmetries in Displayed Type Theory

Examples

axiom A0 : Type

axiom A01 : Type^(d) A0
axiom A10 : Type^(d) A0
axiom A11 : Type^(dd) A0 A01 A10

axiom A100 : Type^(d) A0
axiom A101 : Type^(dd) A0 A01 A100
axiom A110 : Type^(dd) A0 A10 A100
axiom A111 : Type^(ddd) A0 A01 A10 A11 A100 A101 A110

echo A111^(123)
echo A111^(132)
echo A111^(213)
echo A111^(231)
echo A111^(312)
echo A111^(321)

A111

Type⁽ᵈᵈᵈ⁾ A0 A01 A10 A11 A100 A101 A110

A111⁽¹³²⁾

Type⁽ᵈᵈᵈ⁾ A0 A01 A100 A101 A10 A11 (sym A110)

A111⁽²¹³⁾

Type⁽ᵈᵈᵈ⁾ A0 A10 A01 (sym A11) A100 A110 A101

A111⁽²³¹⁾

Type⁽ᵈᵈᵈ⁾ A0 A10 A100 A110 A01 (sym A11) (sym A101)

A111⁽³¹²⁾

Type⁽ᵈᵈᵈ⁾ A0 A100 A01 (sym A101) A10 (sym A110) A11

A111⁽³²¹⁾

Type⁽ᵈᵈᵈ⁾ A0 A100 A10 (sym A110) A01 (sym A101) (sym A11)