text:
module Text.Greek.Script.Unicode where

open import Text.Greek.Script

-- U+0390 - U+03CE
ΐ : Token -- U+0390 GREEK SMALL LETTER IOTA WITH DIALYTIKA AND TONOS
ΐ = with-accent-diaeresis ι′ lower (acute ι-vowel) ι-diaeresis
Α : Token -- U+0391 GREEK CAPITAL LETTER ALPHA
Α = unmarked α′ upper
Β : Token -- U+0392 GREEK CAPITAL LETTER BETA
Β = unmarked β′ upper
Γ : Token -- U+0393 GREEK CAPITAL LETTER GAMMA
Γ = unmarked γ′ upper
Δ : Token -- U+0394 GREEK CAPITAL LETTER DELTA
Δ = unmarked δ′ upper
Ε : Token -- U+0395 GREEK CAPITAL LETTER EPSILON
Ε = unmarked ε′ upper
Ζ : Token -- U+0396 GREEK CAPITAL LETTER ZETA
Ζ = unmarked ζ′ upper
Η : Token -- U+0397 GREEK CAPITAL LETTER ETA
Η = unmarked η′ upper
Θ : Token -- U+0398 GREEK CAPITAL LETTER THETA
Θ = unmarked θ′ upper
Ι : Token -- U+0399 GREEK CAPITAL LETTER IOTA
Ι = unmarked ι′ upper
Κ : Token -- U+039A GREEK CAPITAL LETTER KAPPA
Κ = unmarked κ′ upper
Λ : Token -- U+039B GREEK CAPITAL LETTER LAMDA
Λ = unmarked λ′ upper
Μ : Token -- U+039C GREEK CAPITAL LETTER MU
Μ = unmarked μ′ upper
Ν : Token -- U+039D GREEK CAPITAL LETTER NU
Ν = unmarked ν′ upper
Ξ : Token -- U+039E GREEK CAPITAL LETTER XI
Ξ = unmarked ξ′ upper
Ο : Token -- U+039F GREEK CAPITAL LETTER OMICRON
Ο = unmarked ο′ upper
Π : Token -- U+03A0 GREEK CAPITAL LETTER PI
Π = unmarked π′ upper
Ρ : Token -- U+03A1 GREEK CAPITAL LETTER RHO
Ρ = unmarked ρ′ upper
                  -- U+03A2 <reserved>
Σ : Token -- U+03A3 GREEK CAPITAL LETTER SIGMA
Σ = unmarked σ′ upper
Τ : Token -- U+03A4 GREEK CAPITAL LETTER TAU
Τ = unmarked τ′ upper
Υ : Token -- U+03A5 GREEK CAPITAL LETTER UPSILON
Υ = unmarked υ′ upper
Φ : Token -- U+03A6 GREEK CAPITAL LETTER PHI
Φ = unmarked φ′ upper
Χ : Token -- U+03A7 GREEK CAPITAL LETTER CHI
Χ = unmarked χ′ upper
Ψ : Token -- U+03A8 GREEK CAPITAL LETTER PSI
Ψ = unmarked ψ′ upper
Ω : Token -- U+03A9 GREEK CAPITAL LETTER OMEGA
Ω = unmarked ω′ upper
Ϊ : Token -- U+03AA GREEK CAPITAL LETTER IOTA WITH DIALYTIKA
Ϊ = with-diaeresis ι′ upper ι-diaeresis
Ϋ : Token -- U+03AB GREEK CAPITAL LETTER UPSILON WITH DIALYTIKA
Ϋ = with-diaeresis υ′ upper υ-diaeresis
ά : Token -- U+03AC GREEK SMALL LETTER ALPHA WITH TONOS
ά = with-accent α′ lower (acute α-vowel)
έ : Token -- U+03AD GREEK SMALL LETTER EPSILON WITH TONOS
έ = with-accent ε′ lower (acute ε-vowel)
ή : Token -- U+03AE GREEK SMALL LETTER ETA WITH TONOS
ή = with-accent η′ lower (acute η-vowel)
ί : Token -- U+03AF GREEK SMALL LETTER IOTA WITH TONOS
ί = with-accent ι′ lower (acute ι-vowel)
ΰ : Token -- U+03B0 GREEK SMALL LETTER UPSILON WITH DIALYTIKA AND TONOS
ΰ = with-accent-diaeresis υ′ lower (acute υ-vowel) υ-diaeresis
α : Token -- U+03B1 GREEK SMALL LETTER ALPHA
α = unmarked α′ lower
β : Token -- U+03B2 GREEK SMALL LETTER BETA
β = unmarked β′ lower
γ : Token -- U+03B3 GREEK SMALL LETTER GAMMA
γ = unmarked γ′ lower
δ : Token -- U+03B4 GREEK SMALL LETTER DELTA
δ = unmarked δ′ lower
ε : Token -- U+03B5 GREEK SMALL LETTER EPSILON
ε = unmarked ε′ lower
ζ : Token -- U+03B6 GREEK SMALL LETTER ZETA
ζ = unmarked ζ′ lower
η : Token -- U+03B7 GREEK SMALL LETTER ETA
η = unmarked η′ lower
θ : Token -- U+03B8 GREEK SMALL LETTER THETA
θ = unmarked θ′ lower
ι : Token -- U+03B9 GREEK SMALL LETTER IOTA
ι = unmarked ι′ lower
κ : Token -- U+03BA GREEK SMALL LETTER KAPPA
κ = unmarked κ′ lower
∙λ : Token -- U+03BB GREEK SMALL LETTER LAMDA
∙λ = unmarked λ′ lower
μ : Token -- U+03BC GREEK SMALL LETTER MU
μ = unmarked μ′ lower
ν : Token -- U+03BD GREEK SMALL LETTER NU
ν = unmarked ν′ lower
ξ : Token -- U+03BE GREEK SMALL LETTER XI
ξ = unmarked ξ′ lower
ο : Token -- U+03BF GREEK SMALL LETTER OMICRON
ο = unmarked ο′ lower
π : Token -- U+03C0 GREEK SMALL LETTER PI
π = unmarked π′ lower
ρ : Token -- U+03C1 GREEK SMALL LETTER RHO
ρ = unmarked ρ′ lower
ς : Token -- U+03C2 GREEK SMALL LETTER FINAL SIGMA
ς = final σ′ lower σ-final
σ : Token -- U+03C3 GREEK SMALL LETTER SIGMA
σ = unmarked σ′ lower
τ : Token -- U+03C4 GREEK SMALL LETTER TAU
τ = unmarked τ′ lower
υ : Token -- U+03C5 GREEK SMALL LETTER UPSILON
υ = unmarked υ′ lower
φ : Token -- U+03C6 GREEK SMALL LETTER PHI
φ = unmarked φ′ lower
χ : Token -- U+03C7 GREEK SMALL LETTER CHI
χ = unmarked χ′ lower
ψ : Token -- U+03C8 GREEK SMALL LETTER PSI
ψ = unmarked ψ′ lower
ω : Token -- U+03C9 GREEK SMALL LETTER OMEGA
ω = unmarked ω′ lower
ϊ : Token -- U+03CA GREEK SMALL LETTER IOTA WITH DIALYTIKA
ϊ = with-diaeresis ι′ lower ι-diaeresis
ϋ : Token -- U+03CB GREEK SMALL LETTER UPSILON WITH DIALYTIKA
ϋ = with-diaeresis υ′ lower υ-diaeresis
ό : Token -- U+03CC GREEK SMALL LETTER OMICRON WITH TONOS
ό = with-accent ο′ lower (acute ο-vowel)
ύ : Token -- U+03CD GREEK SMALL LETTER UPSILON WITH TONOS
ύ = with-accent υ′ lower (acute υ-vowel)
ώ : Token -- U+03CE GREEK SMALL LETTER OMEGA WITH TONOS
ώ = with-accent ω′ lower (acute ω-vowel)

-- U+1F00 - U+1FFF
ἀ : Token -- U+1F00  ἀ GREEK SMALL LETTER ALPHA WITH PSILI
ἀ = with-breathing α′ lower (smooth α-smooth)
ἁ : Token -- U+1F01  ἁ GREEK SMALL LETTER ALPHA WITH DASIA
ἁ = with-breathing α′ lower (rough α-rough)
ἂ : Token -- U+1F02  ἂ GREEK SMALL LETTER ALPHA WITH PSILI AND VARIA
ἂ = with-accent-breathing α′ lower (grave α-vowel) (smooth α-smooth)
ἃ : Token -- U+1F03  ἃ GREEK SMALL LETTER ALPHA WITH DASIA AND VARIA
ἃ = with-accent-breathing α′ lower (grave α-vowel) (rough α-rough)
ἄ : Token -- U+1F04  ἄ GREEK SMALL LETTER ALPHA WITH PSILI AND OXIA
ἄ = with-accent-breathing α′ lower (acute α-vowel) (smooth α-smooth)
ἅ : Token -- U+1F05  ἅ GREEK SMALL LETTER ALPHA WITH DASIA AND OXIA
ἅ = with-accent-breathing α′ lower (acute α-vowel) (rough α-rough)
ἆ : Token -- U+1F06  ἆ GREEK SMALL LETTER ALPHA WITH PSILI AND PERISPOMENI
ἆ = with-accent-breathing α′ lower (circumflex α-long-vowel) (smooth α-smooth)
ἇ : Token -- U+1F07  ἇ GREEK SMALL LETTER ALPHA WITH DASIA AND PERISPOMENI
ἇ = with-accent-breathing α′ lower (circumflex α-long-vowel) (rough α-rough)
Ἀ : Token -- U+1F08  Ἀ GREEK CAPITAL LETTER ALPHA WITH PSILI
Ἀ = with-breathing α′ upper (smooth Α-smooth)
Ἁ : Token -- U+1F09  Ἁ GREEK CAPITAL LETTER ALPHA WITH DASIA
Ἁ = with-breathing α′ upper (rough α-rough)
Ἂ : Token -- U+1F0A  Ἂ GREEK CAPITAL LETTER ALPHA WITH PSILI AND VARIA
Ἂ = with-accent-breathing α′ upper (grave α-vowel) (smooth Α-smooth)
Ἃ : Token -- U+1F0B  Ἃ GREEK CAPITAL LETTER ALPHA WITH DASIA AND VARIA
Ἃ = with-accent-breathing α′ upper (grave α-vowel) (rough α-rough)
Ἄ : Token -- U+1F0C  Ἄ GREEK CAPITAL LETTER ALPHA WITH PSILI AND OXIA
Ἄ = with-accent-breathing α′ upper (acute α-vowel) (smooth Α-smooth)
Ἅ : Token -- U+1F0D  Ἅ GREEK CAPITAL LETTER ALPHA WITH DASIA AND OXIA
Ἅ = with-accent-breathing α′ upper (acute α-vowel) (rough α-rough)
Ἆ : Token -- U+1F0E  Ἆ GREEK CAPITAL LETTER ALPHA WITH PSILI AND PERISPOMENI
Ἆ = with-accent-breathing α′ upper (circumflex α-long-vowel) (smooth Α-smooth)
Ἇ : Token -- U+1F0F  Ἇ GREEK CAPITAL LETTER ALPHA WITH DASIA AND PERISPOMENI
Ἇ = with-accent-breathing α′ upper (circumflex α-long-vowel) (rough α-rough)
ἐ : Token -- U+1F10  ἐ GREEK SMALL LETTER EPSILON WITH PSILI
ἐ = with-breathing ε′ lower (smooth ε-smooth)
ἑ : Token -- U+1F11  ἑ GREEK SMALL LETTER EPSILON WITH DASIA
ἑ = with-breathing ε′ lower (rough ε-rough)
ἒ : Token -- U+1F12  ἒ GREEK SMALL LETTER EPSILON WITH PSILI AND VARIA
ἒ = with-accent-breathing ε′ lower (grave ε-vowel) (smooth ε-smooth)
ἓ : Token -- U+1F13  ἓ GREEK SMALL LETTER EPSILON WITH DASIA AND VARIA
ἓ = with-accent-breathing ε′ lower (grave ε-vowel) (rough ε-rough)
ἔ : Token -- U+1F14  ἔ GREEK SMALL LETTER EPSILON WITH PSILI AND OXIA
ἔ = with-accent-breathing ε′ lower (acute ε-vowel) (smooth ε-smooth)
ἕ : Token -- U+1F15  ἕ GREEK SMALL LETTER EPSILON WITH DASIA AND OXIA
ἕ = with-accent-breathing ε′ lower (acute ε-vowel) (rough ε-rough)
-- U+1F16
-- U+1F17
Ἐ : Token -- U+1F18  Ἐ GREEK CAPITAL LETTER EPSILON WITH PSILI
Ἐ = with-breathing ε′ upper (smooth Ε-smooth)
Ἑ : Token -- U+1F19  Ἑ GREEK CAPITAL LETTER EPSILON WITH DASIA
Ἑ = with-breathing ε′ upper (rough ε-rough)
Ἒ : Token -- U+1F1A  Ἒ GREEK CAPITAL LETTER EPSILON WITH PSILI AND VARIA
Ἒ = with-accent-breathing ε′ upper (grave ε-vowel) (smooth Ε-smooth)
Ἓ : Token -- U+1F1B  Ἓ GREEK CAPITAL LETTER EPSILON WITH DASIA AND VARIA
Ἓ = with-accent-breathing ε′ upper (grave ε-vowel) (rough ε-rough)
Ἔ : Token -- U+1F1C  Ἔ GREEK CAPITAL LETTER EPSILON WITH PSILI AND OXIA
Ἔ = with-accent-breathing ε′ upper (acute ε-vowel) (smooth Ε-smooth)
Ἕ : Token -- U+1F1D  Ἕ GREEK CAPITAL LETTER EPSILON WITH DASIA AND OXIA
Ἕ = with-accent-breathing ε′ upper (acute ε-vowel) (rough ε-rough)
-- U+1F1E
-- U+1F1F
ἠ : Token -- U+1F20  ἠ GREEK SMALL LETTER ETA WITH PSILI
ἠ = with-breathing η′ lower (smooth η-smooth)
ἡ : Token -- U+1F21  ἡ GREEK SMALL LETTER ETA WITH DASIA
ἡ = with-breathing η′ lower (rough η-rough)
ἢ : Token -- U+1F22  ἢ GREEK SMALL LETTER ETA WITH PSILI AND VARIA
ἢ = with-accent-breathing η′ lower (grave η-vowel) (smooth η-smooth)
ἣ : Token -- U+1F23  ἣ GREEK SMALL LETTER ETA WITH DASIA AND VARIA
ἣ = with-accent-breathing η′ lower (grave η-vowel) (rough η-rough)
ἤ : Token -- U+1F24  ἤ GREEK SMALL LETTER ETA WITH PSILI AND OXIA
ἤ = with-accent-breathing η′ lower (acute η-vowel) (smooth η-smooth)
ἥ : Token -- U+1F25  ἥ GREEK SMALL LETTER ETA WITH DASIA AND OXIA
ἥ = with-accent-breathing η′ lower (acute η-vowel) (rough η-rough)
ἦ : Token -- U+1F26  ἦ GREEK SMALL LETTER ETA WITH PSILI AND PERISPOMENI
ἦ = with-accent-breathing η′ lower (circumflex η-long-vowel) (smooth η-smooth)
ἧ : Token -- U+1F27  ἧ GREEK SMALL LETTER ETA WITH DASIA AND PERISPOMENI
ἧ = with-accent-breathing η′ lower (circumflex η-long-vowel) (rough η-rough)
Ἠ : Token -- U+1F28  Ἠ GREEK CAPITAL LETTER ETA WITH PSILI
Ἠ = with-breathing η′ upper (smooth Η-smooth)
Ἡ : Token -- U+1F29  Ἡ GREEK CAPITAL LETTER ETA WITH DASIA
Ἡ = with-breathing η′ upper (rough η-rough)
Ἢ : Token -- U+1F2A  Ἢ GREEK CAPITAL LETTER ETA WITH PSILI AND VARIA
Ἢ = with-accent-breathing η′ upper (grave η-vowel) (smooth Η-smooth)
Ἣ : Token -- U+1F2B  Ἣ GREEK CAPITAL LETTER ETA WITH DASIA AND VARIA
Ἣ = with-accent-breathing η′ upper (grave η-vowel) (rough η-rough)
Ἤ : Token -- U+1F2C  Ἤ GREEK CAPITAL LETTER ETA WITH PSILI AND OXIA
Ἤ = with-accent-breathing η′ upper (acute η-vowel) (smooth Η-smooth)
Ἥ : Token -- U+1F2D  Ἥ GREEK CAPITAL LETTER ETA WITH DASIA AND OXIA
Ἥ = with-accent-breathing η′ upper (acute η-vowel) (rough η-rough)
Ἦ : Token -- U+1F2E  Ἦ GREEK CAPITAL LETTER ETA WITH PSILI AND PERISPOMENI
Ἦ = with-accent-breathing η′ upper (circumflex η-long-vowel) (smooth Η-smooth)
Ἧ : Token -- U+1F2F  Ἧ GREEK CAPITAL LETTER ETA WITH DASIA AND PERISPOMENI
Ἧ = with-accent-breathing η′ upper (circumflex η-long-vowel) (rough η-rough)
ἰ : Token -- U+1F30  ἰ GREEK SMALL LETTER IOTA WITH PSILI
ἰ = with-breathing ι′ lower (smooth ι-smooth)
ἱ : Token -- U+1F31  ἱ GREEK SMALL LETTER IOTA WITH DASIA
ἱ = with-breathing ι′ lower (rough ι-rough)
ἲ : Token -- U+1F32  ἲ GREEK SMALL LETTER IOTA WITH PSILI AND VARIA
ἲ = with-accent-breathing ι′ lower (grave ι-vowel) (smooth ι-smooth)
ἳ : Token -- U+1F33  ἳ GREEK SMALL LETTER IOTA WITH DASIA AND VARIA
ἳ = with-accent-breathing ι′ lower (grave ι-vowel) (rough ι-rough)
ἴ : Token -- U+1F34  ἴ GREEK SMALL LETTER IOTA WITH PSILI AND OXIA
ἴ = with-accent-breathing ι′ lower (acute ι-vowel) (smooth ι-smooth)
ἵ : Token -- U+1F35  ἵ GREEK SMALL LETTER IOTA WITH DASIA AND OXIA
ἵ = with-accent-breathing ι′ lower (acute ι-vowel) (rough ι-rough)
ἶ : Token -- U+1F36  ἶ GREEK SMALL LETTER IOTA WITH PSILI AND PERISPOMENI
ἶ = with-accent-breathing ι′ lower (circumflex ι-long-vowel) (smooth ι-smooth)
ἷ : Token -- U+1F37  ἷ GREEK SMALL LETTER IOTA WITH DASIA AND PERISPOMENI
ἷ = with-accent-breathing ι′ lower (circumflex ι-long-vowel) (rough ι-rough)
Ἰ : Token -- U+1F38  Ἰ GREEK CAPITAL LETTER IOTA WITH PSILI
Ἰ = with-breathing ι′ upper (smooth Ι-smooth)
Ἱ : Token -- U+1F39  Ἱ GREEK CAPITAL LETTER IOTA WITH DASIA
Ἱ = with-breathing ι′ upper (rough ι-rough)
Ἲ : Token -- U+1F3A  Ἲ GREEK CAPITAL LETTER IOTA WITH PSILI AND VARIA
Ἲ = with-accent-breathing ι′ upper (grave ι-vowel) (smooth Ι-smooth)
Ἳ : Token -- U+1F3B  Ἳ GREEK CAPITAL LETTER IOTA WITH DASIA AND VARIA
Ἳ = with-accent-breathing ι′ upper (grave ι-vowel) (rough ι-rough)
Ἴ : Token -- U+1F3C  Ἴ GREEK CAPITAL LETTER IOTA WITH PSILI AND OXIA
Ἴ = with-accent-breathing ι′ upper (acute ι-vowel) (smooth Ι-smooth)
Ἵ : Token -- U+1F3D  Ἵ GREEK CAPITAL LETTER IOTA WITH DASIA AND OXIA
Ἵ = with-accent-breathing ι′ upper (acute ι-vowel) (rough ι-rough)
Ἶ : Token -- U+1F3E  Ἶ GREEK CAPITAL LETTER IOTA WITH PSILI AND PERISPOMENI
Ἶ = with-accent-breathing ι′ upper (circumflex ι-long-vowel) (smooth Ι-smooth)
Ἷ : Token -- U+1F3F  Ἷ GREEK CAPITAL LETTER IOTA WITH DASIA AND PERISPOMENI
Ἷ = with-accent-breathing ι′ upper (circumflex ι-long-vowel) (rough ι-rough)
ὀ : Token -- U+1F40  ὀ GREEK SMALL LETTER OMICRON WITH PSILI
ὀ = with-breathing ο′ lower (smooth ο-smooth)
ὁ : Token -- U+1F41  ὁ GREEK SMALL LETTER OMICRON WITH DASIA
ὁ = with-breathing ο′ lower (rough ο-rough)
ὂ : Token -- U+1F42  ὂ GREEK SMALL LETTER OMICRON WITH PSILI AND VARIA
ὂ = with-accent-breathing ο′ lower (grave ο-vowel) (smooth ο-smooth)
ὃ : Token -- U+1F43  ὃ GREEK SMALL LETTER OMICRON WITH DASIA AND VARIA
ὃ = with-accent-breathing ο′ lower (grave ο-vowel) (rough ο-rough)
ὄ : Token -- U+1F44  ὄ GREEK SMALL LETTER OMICRON WITH PSILI AND OXIA
ὄ = with-accent-breathing ο′ lower (acute ο-vowel) (smooth ο-smooth)
ὅ : Token -- U+1F45  ὅ GREEK SMALL LETTER OMICRON WITH DASIA AND OXIA
ὅ = with-accent-breathing ο′ lower (acute ο-vowel) (rough ο-rough)
-- U+1F46
-- U+1F47
Ὀ : Token -- U+1F48  Ὀ GREEK CAPITAL LETTER OMICRON WITH PSILI
Ὀ = with-breathing ο′ upper (smooth Ο-smooth)
Ὁ : Token -- U+1F49  Ὁ GREEK CAPITAL LETTER OMICRON WITH DASIA
Ὁ = with-breathing ο′ upper (rough ο-rough)
Ὂ : Token -- U+1F4A  Ὂ GREEK CAPITAL LETTER OMICRON WITH PSILI AND VARIA
Ὂ = with-accent-breathing ο′ upper (grave ο-vowel) (smooth Ο-smooth)
Ὃ : Token -- U+1F4B  Ὃ GREEK CAPITAL LETTER OMICRON WITH DASIA AND VARIA
Ὃ = with-accent-breathing ο′ upper (grave ο-vowel) (rough ο-rough)
Ὄ : Token -- U+1F4C  Ὄ GREEK CAPITAL LETTER OMICRON WITH PSILI AND OXIA
Ὄ = with-accent-breathing ο′ upper (acute ο-vowel) (smooth Ο-smooth)
Ὅ : Token -- U+1F4D  Ὅ GREEK CAPITAL LETTER OMICRON WITH DASIA AND OXIA
Ὅ = with-accent-breathing ο′ upper (acute ο-vowel) (rough ο-rough)
-- U+1F4E
-- U+1F4F
ὐ : Token -- U+1F50  ὐ GREEK SMALL LETTER UPSILON WITH PSILI
ὐ = with-breathing υ′ lower (smooth υ-smooth)
ὑ : Token -- U+1F51  ὑ GREEK SMALL LETTER UPSILON WITH DASIA
ὑ = with-breathing υ′ lower (rough υ-rough)
ὒ : Token -- U+1F52  ὒ GREEK SMALL LETTER UPSILON WITH PSILI AND VARIA
ὒ = with-accent-breathing υ′ lower (grave υ-vowel) (smooth υ-smooth)
ὓ : Token -- U+1F53  ὓ GREEK SMALL LETTER UPSILON WITH DASIA AND VARIA
ὓ = with-accent-breathing υ′ lower (grave υ-vowel) (rough υ-rough)
ὔ : Token -- U+1F54  ὔ GREEK SMALL LETTER UPSILON WITH PSILI AND OXIA
ὔ = with-accent-breathing υ′ lower (acute υ-vowel) (smooth υ-smooth)
ὕ : Token -- U+1F55  ὕ GREEK SMALL LETTER UPSILON WITH DASIA AND OXIA
ὕ = with-accent-breathing υ′ lower (acute υ-vowel) (rough υ-rough)
ὖ : Token -- U+1F56  ὖ GREEK SMALL LETTER UPSILON WITH PSILI AND PERISPOMENI
ὖ = with-accent-breathing υ′ lower (circumflex υ-long-vowel) (smooth υ-smooth)
ὗ : Token -- U+1F57  ὗ GREEK SMALL LETTER UPSILON WITH DASIA AND PERISPOMENI
ὗ = with-accent-breathing υ′ lower (circumflex υ-long-vowel) (rough υ-rough)
-- U+1F58
Ὑ : Token -- U+1F59  Ὑ GREEK CAPITAL LETTER UPSILON WITH DASIA
Ὑ = with-breathing υ′ upper (rough υ-rough)
-- U+1F5A
Ὓ : Token -- U+1F5B  Ὓ GREEK CAPITAL LETTER UPSILON WITH DASIA AND VARIA
Ὓ = with-accent-breathing υ′ upper (grave υ-vowel) (rough υ-rough)
-- U+1F5C
Ὕ : Token -- U+1F5D  Ὕ GREEK CAPITAL LETTER UPSILON WITH DASIA AND OXIA
Ὕ = with-accent-breathing υ′ upper (acute υ-vowel) (rough υ-rough)
-- U+1F5E
Ὗ : Token -- U+1F5F  Ὗ GREEK CAPITAL LETTER UPSILON WITH DASIA AND PERISPOMENI
Ὗ = with-accent-breathing υ′ upper (circumflex υ-long-vowel) (rough υ-rough)
ὠ : Token -- U+1F60  ὠ GREEK SMALL LETTER OMEGA WITH PSILI
ὠ = with-breathing ω′ lower (smooth ω-smooth)
ὡ : Token -- U+1F61  ὡ GREEK SMALL LETTER OMEGA WITH DASIA
ὡ = with-breathing ω′ lower (rough ω-rough)
ὢ : Token -- U+1F62  ὢ GREEK SMALL LETTER OMEGA WITH PSILI AND VARIA
ὢ = with-accent-breathing ω′ lower (grave ω-vowel) (smooth ω-smooth)
ὣ : Token -- U+1F63  ὣ GREEK SMALL LETTER OMEGA WITH DASIA AND VARIA
ὣ = with-accent-breathing ω′ lower (grave ω-vowel) (rough ω-rough)
ὤ : Token -- U+1F64  ὤ GREEK SMALL LETTER OMEGA WITH PSILI AND OXIA
ὤ = with-accent-breathing ω′ lower (acute ω-vowel) (smooth ω-smooth)
ὥ : Token -- U+1F65  ὥ GREEK SMALL LETTER OMEGA WITH DASIA AND OXIA
ὥ = with-accent-breathing ω′ lower (acute ω-vowel) (rough ω-rough)
ὦ : Token -- U+1F66  ὦ GREEK SMALL LETTER OMEGA WITH PSILI AND PERISPOMENI
ὦ = with-accent-breathing ω′ lower (circumflex ω-long-vowel) (smooth ω-smooth)
ὧ : Token -- U+1F67  ὧ GREEK SMALL LETTER OMEGA WITH DASIA AND PERISPOMENI
ὧ = with-accent-breathing ω′ lower (circumflex ω-long-vowel) (rough ω-rough)
Ὠ : Token -- U+1F68  Ὠ GREEK CAPITAL LETTER OMEGA WITH PSILI
Ὠ = with-breathing ω′ upper (smooth Ω-smooth)
Ὡ : Token -- U+1F69  Ὡ GREEK CAPITAL LETTER OMEGA WITH DASIA
Ὡ = with-breathing ω′ upper (rough ω-rough)
Ὢ : Token -- U+1F6A  Ὢ GREEK CAPITAL LETTER OMEGA WITH PSILI AND VARIA
Ὢ = with-accent-breathing ω′ upper (grave ω-vowel) (smooth Ω-smooth)
Ὣ : Token -- U+1F6B  Ὣ GREEK CAPITAL LETTER OMEGA WITH DASIA AND VARIA
Ὣ = with-accent-breathing ω′ upper (grave ω-vowel) (rough ω-rough)
Ὤ : Token -- U+1F6C  Ὤ GREEK CAPITAL LETTER OMEGA WITH PSILI AND OXIA
Ὤ = with-accent-breathing ω′ upper (acute ω-vowel) (smooth Ω-smooth)
Ὥ : Token -- U+1F6D  Ὥ GREEK CAPITAL LETTER OMEGA WITH DASIA AND OXIA
Ὥ = with-accent-breathing ω′ upper (acute ω-vowel) (rough ω-rough)
Ὦ : Token -- U+1F6E  Ὦ GREEK CAPITAL LETTER OMEGA WITH PSILI AND PERISPOMENI
Ὦ = with-accent-breathing ω′ upper (circumflex ω-long-vowel) (smooth Ω-smooth)
Ὧ : Token -- U+1F6F  Ὧ GREEK CAPITAL LETTER OMEGA WITH DASIA AND PERISPOMENI
Ὧ = with-accent-breathing ω′ upper (circumflex ω-long-vowel) (rough ω-rough)
ὰ : Token -- U+1F70  ὰ GREEK SMALL LETTER ALPHA WITH VARIA
ὰ = with-accent α′ lower (grave α-vowel)
ά : Token -- U+1F71  ά GREEK SMALL LETTER ALPHA WITH OXIA
ά = with-accent α′ lower (acute α-vowel)
ὲ : Token -- U+1F72  ὲ GREEK SMALL LETTER EPSILON WITH VARIA
ὲ = with-accent ε′ lower (grave ε-vowel)
έ : Token -- U+1F73  έ GREEK SMALL LETTER EPSILON WITH OXIA
έ = with-accent ε′ lower (acute ε-vowel)
ὴ : Token -- U+1F74  ὴ GREEK SMALL LETTER ETA WITH VARIA
ὴ = with-accent η′ lower (grave η-vowel)
ή : Token -- U+1F75  ή GREEK SMALL LETTER ETA WITH OXIA
ή = with-accent η′ lower (acute η-vowel)
ὶ : Token -- U+1F76  ὶ GREEK SMALL LETTER IOTA WITH VARIA
ὶ = with-accent ι′ lower (grave ι-vowel)
ί : Token -- U+1F77  ί GREEK SMALL LETTER IOTA WITH OXIA
ί = with-accent ι′ lower (acute ι-vowel)
ὸ : Token -- U+1F78  ὸ GREEK SMALL LETTER OMICRON WITH VARIA
ὸ = with-accent ο′ lower (grave ο-vowel)
ό : Token -- U+1F79  ό GREEK SMALL LETTER OMICRON WITH OXIA
ό = with-accent ο′ lower (acute ο-vowel)
ὺ : Token -- U+1F7A  ὺ GREEK SMALL LETTER UPSILON WITH VARIA
ὺ = with-accent υ′ lower (grave υ-vowel)
ύ : Token -- U+1F7B  ύ GREEK SMALL LETTER UPSILON WITH OXIA
ύ = with-accent υ′ lower (acute υ-vowel)
ὼ : Token -- U+1F7C  ὼ GREEK SMALL LETTER OMEGA WITH VARIA
ὼ = with-accent ω′ lower (grave ω-vowel)
ώ : Token -- U+1F7D  ώ GREEK SMALL LETTER OMEGA WITH OXIA
ώ = with-accent ω′ lower (acute ω-vowel)
-- U+1F7E
-- U+1F7F
ᾀ : Token -- U+1F80  ᾀ GREEK SMALL LETTER ALPHA WITH PSILI AND YPOGEGRAMMENI
ᾀ = with-breathing-iota α′ lower (smooth α-smooth) α-iota-subscript
ᾁ : Token -- U+1F81  ᾁ GREEK SMALL LETTER ALPHA WITH DASIA AND YPOGEGRAMMENI
ᾁ = with-breathing-iota α′ lower (rough α-rough) α-iota-subscript
ᾂ : Token -- U+1F82  ᾂ GREEK SMALL LETTER ALPHA WITH PSILI AND VARIA AND YPOGEGRAMMENI
ᾂ = with-accent-breathing-iota α′ lower (grave α-vowel) (smooth α-smooth) α-iota-subscript
ᾃ : Token -- U+1F83  ᾃ GREEK SMALL LETTER ALPHA WITH DASIA AND VARIA AND YPOGEGRAMMENI
ᾃ = with-accent-breathing-iota α′ lower (grave α-vowel) (rough α-rough) α-iota-subscript
ᾄ : Token -- U+1F84  ᾄ GREEK SMALL LETTER ALPHA WITH PSILI AND OXIA AND YPOGEGRAMMENI
ᾄ = with-accent-breathing-iota α′ lower (acute α-vowel) (smooth α-smooth) α-iota-subscript
ᾅ : Token -- U+1F85  ᾅ GREEK SMALL LETTER ALPHA WITH DASIA AND OXIA AND YPOGEGRAMMENI
ᾅ = with-accent-breathing-iota α′ lower (acute α-vowel) (rough α-rough) α-iota-subscript
ᾆ : Token -- U+1F86  ᾆ GREEK SMALL LETTER ALPHA WITH PSILI AND PERISPOMENI AND YPOGEGRAMMENI
ᾆ = with-accent-breathing-iota α′ lower (circumflex α-long-vowel) (smooth α-smooth) α-iota-subscript
ᾇ : Token -- U+1F87  ᾇ GREEK SMALL LETTER ALPHA WITH DASIA AND PERISPOMENI AND YPOGEGRAMMENI
ᾇ = with-accent-breathing-iota α′ lower (circumflex α-long-vowel) (rough α-rough) α-iota-subscript
ᾈ : Token -- U+1F88  ᾈ GREEK CAPITAL LETTER ALPHA WITH PSILI AND PROSGEGRAMMENI
ᾈ = with-breathing-iota α′ upper (smooth Α-smooth) α-iota-subscript
ᾉ : Token -- U+1F89  ᾉ GREEK CAPITAL LETTER ALPHA WITH DASIA AND PROSGEGRAMMENI
ᾉ = with-breathing-iota α′ upper (rough α-rough) α-iota-subscript
ᾊ : Token -- U+1F8A  ᾊ GREEK CAPITAL LETTER ALPHA WITH PSILI AND VARIA AND PROSGEGRAMMENI
ᾊ = with-accent-breathing-iota α′ upper (grave α-vowel) (smooth Α-smooth) α-iota-subscript
ᾋ : Token -- U+1F8B  ᾋ GREEK CAPITAL LETTER ALPHA WITH DASIA AND VARIA AND PROSGEGRAMMENI
ᾋ = with-accent-breathing-iota α′ upper (grave α-vowel) (rough α-rough) α-iota-subscript
ᾌ : Token -- U+1F8C  ᾌ GREEK CAPITAL LETTER ALPHA WITH PSILI AND OXIA AND PROSGEGRAMMENI
ᾌ = with-accent-breathing-iota α′ upper (acute α-vowel) (smooth Α-smooth) α-iota-subscript
ᾍ : Token -- U+1F8D  ᾍ GREEK CAPITAL LETTER ALPHA WITH DASIA AND OXIA AND PROSGEGRAMMENI
ᾍ = with-accent-breathing-iota α′ upper (acute α-vowel) (rough α-rough) α-iota-subscript
ᾎ : Token -- U+1F8E  ᾎ GREEK CAPITAL LETTER ALPHA WITH PSILI AND PERISPOMENI AND PROSGEGRAMMENI
ᾎ = with-accent-breathing-iota α′ upper (circumflex α-long-vowel) (smooth Α-smooth) α-iota-subscript
ᾏ : Token -- U+1F8F  ᾏ GREEK CAPITAL LETTER ALPHA WITH DASIA AND PERISPOMENI AND PROSGEGRAMMENI
ᾏ = with-accent-breathing-iota α′ upper (circumflex α-long-vowel) (rough α-rough) α-iota-subscript
ᾐ : Token -- U+1F90  ᾐ GREEK SMALL LETTER ETA WITH PSILI AND YPOGEGRAMMENI
ᾐ = with-breathing-iota η′ lower (smooth η-smooth) η-iota-subscript
ᾑ : Token -- U+1F91  ᾑ GREEK SMALL LETTER ETA WITH DASIA AND YPOGEGRAMMENI
ᾑ = with-breathing-iota η′ lower (rough η-rough) η-iota-subscript
ᾒ : Token -- U+1F92  ᾒ GREEK SMALL LETTER ETA WITH PSILI AND VARIA AND YPOGEGRAMMENI
ᾒ = with-accent-breathing-iota η′ lower (grave η-vowel) (smooth η-smooth) η-iota-subscript
ᾓ : Token -- U+1F93  ᾓ GREEK SMALL LETTER ETA WITH DASIA AND VARIA AND YPOGEGRAMMENI
ᾓ = with-accent-breathing-iota η′ lower (grave η-vowel) (rough η-rough) η-iota-subscript
ᾔ : Token -- U+1F94  ᾔ GREEK SMALL LETTER ETA WITH PSILI AND OXIA AND YPOGEGRAMMENI
ᾔ = with-accent-breathing-iota η′ lower (acute η-vowel) (smooth η-smooth) η-iota-subscript
ᾕ : Token -- U+1F95  ᾕ GREEK SMALL LETTER ETA WITH DASIA AND OXIA AND YPOGEGRAMMENI
ᾕ = with-accent-breathing-iota η′ lower (acute η-vowel) (rough η-rough) η-iota-subscript
ᾖ : Token -- U+1F96  ᾖ GREEK SMALL LETTER ETA WITH PSILI AND PERISPOMENI AND YPOGEGRAMMENI
ᾖ = with-accent-breathing-iota η′ lower (circumflex η-long-vowel) (smooth η-smooth) η-iota-subscript
ᾗ : Token -- U+1F97  ᾗ GREEK SMALL LETTER ETA WITH DASIA AND PERISPOMENI AND YPOGEGRAMMENI
ᾗ = with-accent-breathing-iota η′ lower (circumflex η-long-vowel) (rough η-rough) η-iota-subscript
ᾘ : Token -- U+1F98  ᾘ GREEK CAPITAL LETTER ETA WITH PSILI AND PROSGEGRAMMENI
ᾘ = with-breathing-iota η′ upper (smooth Η-smooth) η-iota-subscript
ᾙ : Token -- U+1F99  ᾙ GREEK CAPITAL LETTER ETA WITH DASIA AND PROSGEGRAMMENI
ᾙ = with-breathing-iota η′ upper (rough η-rough) η-iota-subscript
ᾚ : Token -- U+1F9A  ᾚ GREEK CAPITAL LETTER ETA WITH PSILI AND VARIA AND PROSGEGRAMMENI
ᾚ = with-accent-breathing-iota η′ upper (grave η-vowel) (smooth Η-smooth) η-iota-subscript
ᾛ : Token -- U+1F9B  ᾛ GREEK CAPITAL LETTER ETA WITH DASIA AND VARIA AND PROSGEGRAMMENI
ᾛ = with-accent-breathing-iota η′ upper (grave η-vowel) (rough η-rough) η-iota-subscript
ᾜ : Token -- U+1F9C  ᾜ GREEK CAPITAL LETTER ETA WITH PSILI AND OXIA AND PROSGEGRAMMENI
ᾜ = with-accent-breathing-iota η′ upper (acute η-vowel) (smooth Η-smooth) η-iota-subscript
ᾝ : Token -- U+1F9D  ᾝ GREEK CAPITAL LETTER ETA WITH DASIA AND OXIA AND PROSGEGRAMMENI
ᾝ = with-accent-breathing-iota η′ upper (acute η-vowel) (rough η-rough) η-iota-subscript
ᾞ : Token -- U+1F9E  ᾞ GREEK CAPITAL LETTER ETA WITH PSILI AND PERISPOMENI AND PROSGEGRAMMENI
ᾞ = with-accent-breathing-iota η′ upper (circumflex η-long-vowel) (smooth Η-smooth) η-iota-subscript
ᾟ : Token -- U+1F9F  ᾟ GREEK CAPITAL LETTER ETA WITH DASIA AND PERISPOMENI AND PROSGEGRAMMENI
ᾟ = with-accent-breathing-iota η′ upper (circumflex η-long-vowel) (rough η-rough) η-iota-subscript
ᾠ : Token -- U+1FA0  ᾠ GREEK SMALL LETTER OMEGA WITH PSILI AND YPOGEGRAMMENI
ᾠ = with-breathing-iota ω′ lower (smooth ω-smooth) ω-iota-subscript
ᾡ : Token -- U+1FA1  ᾡ GREEK SMALL LETTER OMEGA WITH DASIA AND YPOGEGRAMMENI
ᾡ = with-breathing-iota ω′ lower (rough ω-rough) ω-iota-subscript
ᾢ : Token -- U+1FA2  ᾢ GREEK SMALL LETTER OMEGA WITH PSILI AND VARIA AND YPOGEGRAMMENI
ᾢ = with-accent-breathing-iota ω′ lower (grave ω-vowel) (smooth ω-smooth) ω-iota-subscript
ᾣ : Token -- U+1FA3  ᾣ GREEK SMALL LETTER OMEGA WITH DASIA AND VARIA AND YPOGEGRAMMENI
ᾣ = with-accent-breathing-iota ω′ lower (grave ω-vowel) (rough ω-rough) ω-iota-subscript
ᾤ : Token -- U+1FA4  ᾤ GREEK SMALL LETTER OMEGA WITH PSILI AND OXIA AND YPOGEGRAMMENI
ᾤ = with-accent-breathing-iota ω′ lower (acute ω-vowel) (smooth ω-smooth) ω-iota-subscript
ᾥ : Token -- U+1FA5  ᾥ GREEK SMALL LETTER OMEGA WITH DASIA AND OXIA AND YPOGEGRAMMENI
ᾥ = with-accent-breathing-iota ω′ lower (acute ω-vowel) (rough ω-rough) ω-iota-subscript
ᾦ : Token -- U+1FA6  ᾦ GREEK SMALL LETTER OMEGA WITH PSILI AND PERISPOMENI AND YPOGEGRAMMENI
ᾦ = with-accent-breathing-iota ω′ lower (circumflex ω-long-vowel) (smooth ω-smooth) ω-iota-subscript
ᾧ : Token -- U+1FA7  ᾧ GREEK SMALL LETTER OMEGA WITH DASIA AND PERISPOMENI AND YPOGEGRAMMENI
ᾧ = with-accent-breathing-iota ω′ lower (circumflex ω-long-vowel) (rough ω-rough) ω-iota-subscript
ᾨ : Token -- U+1FA8  ᾨ GREEK CAPITAL LETTER OMEGA WITH PSILI AND PROSGEGRAMMENI
ᾨ = with-breathing-iota ω′ upper (smooth Ω-smooth) ω-iota-subscript
ᾩ : Token -- U+1FA9  ᾩ GREEK CAPITAL LETTER OMEGA WITH DASIA AND PROSGEGRAMMENI
ᾩ = with-breathing-iota ω′ upper (rough ω-rough) ω-iota-subscript
ᾪ : Token -- U+1FAA  ᾪ GREEK CAPITAL LETTER OMEGA WITH PSILI AND VARIA AND PROSGEGRAMMENI
ᾪ = with-accent-breathing-iota ω′ upper (grave ω-vowel) (smooth Ω-smooth) ω-iota-subscript
ᾫ : Token -- U+1FAB  ᾫ GREEK CAPITAL LETTER OMEGA WITH DASIA AND VARIA AND PROSGEGRAMMENI
ᾫ = with-accent-breathing-iota ω′ upper (grave ω-vowel) (rough ω-rough) ω-iota-subscript
ᾬ : Token -- U+1FAC  ᾬ GREEK CAPITAL LETTER OMEGA WITH PSILI AND OXIA AND PROSGEGRAMMENI
ᾬ = with-accent-breathing-iota ω′ upper (acute ω-vowel) (smooth Ω-smooth) ω-iota-subscript
ᾭ : Token -- U+1FAD  ᾭ GREEK CAPITAL LETTER OMEGA WITH DASIA AND OXIA AND PROSGEGRAMMENI
ᾭ = with-accent-breathing-iota ω′ upper (acute ω-vowel) (rough ω-rough) ω-iota-subscript
ᾮ : Token -- U+1FAE  ᾮ GREEK CAPITAL LETTER OMEGA WITH PSILI AND PERISPOMENI AND PROSGEGRAMMENI
ᾮ = with-accent-breathing-iota ω′ upper (circumflex ω-long-vowel) (smooth Ω-smooth) ω-iota-subscript
ᾯ : Token -- U+1FAF  ᾯ GREEK CAPITAL LETTER OMEGA WITH DASIA AND PERISPOMENI AND PROSGEGRAMMENI
ᾯ = with-accent-breathing-iota ω′ upper (circumflex ω-long-vowel) (rough ω-rough) ω-iota-subscript
-- U+1FB0 ᾰ GREEK SMALL LETTER ALPHA WITH VRACHY
-- U+1FB1 ᾱ GREEK SMALL LETTER ALPHA WITH MACRON
ᾲ : Token -- U+1FB2  ᾲ GREEK SMALL LETTER ALPHA WITH VARIA AND YPOGEGRAMMENI
ᾲ = with-accent-iota α′ lower (grave α-vowel) α-iota-subscript
ᾳ : Token -- U+1FB3  ᾳ GREEK SMALL LETTER ALPHA WITH YPOGEGRAMMENI
ᾳ = with-iota α′ lower α-iota-subscript
ᾴ : Token -- U+1FB4  ᾴ GREEK SMALL LETTER ALPHA WITH OXIA AND YPOGEGRAMMENI
ᾴ = with-accent-iota α′ lower (acute α-vowel) α-iota-subscript
-- U+1FB5
ᾶ : Token -- U+1FB6  ᾶ GREEK SMALL LETTER ALPHA WITH PERISPOMENI
ᾶ = with-accent α′ lower (circumflex α-long-vowel)
ᾷ : Token -- U+1FB7  ᾷ GREEK SMALL LETTER ALPHA WITH PERISPOMENI AND YPOGEGRAMMENI
ᾷ = with-accent-iota α′ lower (circumflex α-long-vowel) α-iota-subscript
-- U+1FB8 Ᾰ GREEK CAPITAL LETTER ALPHA WITH VRACHY
-- U+1FB9 Ᾱ GREEK CAPITAL LETTER ALPHA WITH MACRON
Ὰ : Token -- U+1FBA  Ὰ GREEK CAPITAL LETTER ALPHA WITH VARIA
Ὰ = with-accent α′ upper (grave α-vowel)
Ά : Token -- U+1FBB  Ά GREEK CAPITAL LETTER ALPHA WITH OXIA
Ά = with-accent α′ upper (acute α-vowel)
ᾼ : Token -- U+1FBC  ᾼ GREEK CAPITAL LETTER ALPHA WITH PROSGEGRAMMENI
ᾼ = with-iota α′ upper α-iota-subscript
-- U+1FBD  ᾽  GREEK KORONIS
-- U+1FBE  ι  GREEK PROSGEGRAMMENI
-- U+1FBF  ᾿  GREEK PSILI
-- U+1FC0  ῀  GREEK PERISPOMENI
-- U+1FC1  ῁  GREEK DIALYTIKA AND PERISPOMENI
ῂ : Token -- U+1FC2  ῂ GREEK SMALL LETTER ETA WITH VARIA AND YPOGEGRAMMENI accent (circumflex α-long-vowel)
ῂ = with-accent-iota η′ lower (grave η-vowel) η-iota-subscript
ῃ : Token -- U+1FC3  ῃ GREEK SMALL LETTER ETA WITH YPOGEGRAMMENI
ῃ = with-iota η′ lower η-iota-subscript
ῄ : Token -- U+1FC4  ῄ GREEK SMALL LETTER ETA WITH OXIA AND YPOGEGRAMMENI
ῄ = with-accent-iota η′ lower (acute η-vowel) η-iota-subscript
-- U+1FC5
ῆ : Token -- U+1FC6  ῆ GREEK SMALL LETTER ETA WITH PERISPOMENI
ῆ = with-accent η′ lower (circumflex η-long-vowel)
ῇ : Token -- U+1FC7  ῇ GREEK SMALL LETTER ETA WITH PERISPOMENI AND YPOGEGRAMMENI
ῇ = with-accent-iota η′ lower (circumflex η-long-vowel) η-iota-subscript
Ὲ : Token -- U+1FC8  Ὲ GREEK CAPITAL LETTER EPSILON WITH VARIA
Ὲ = with-accent ε′ upper (grave ε-vowel)
Έ : Token -- U+1FC9  Έ GREEK CAPITAL LETTER EPSILON WITH OXIA
Έ = with-accent ε′ upper (acute ε-vowel)
Ὴ : Token -- U+1FCA  Ὴ GREEK CAPITAL LETTER ETA WITH VARIA
Ὴ = with-accent η′ upper (grave η-vowel)
Ή : Token -- U+1FCB  Ή GREEK CAPITAL LETTER ETA WITH OXIA
Ή = with-accent η′ upper (acute η-vowel)
ῌ : Token -- U+1FCC  ῌ GREEK CAPITAL LETTER ETA WITH PROSGEGRAMMENI
ῌ = with-iota η′ upper η-iota-subscript
-- U+1FCD  ῍ GREEK PSILI AND VARIA
-- U+1FCE  ῎ GREEK PSILI AND OXIA
-- U+1FCF  ῏ GREEK PSILI AND PERISPOMENI
-- U+1FD0  ῐ GREEK SMALL LETTER IOTA WITH VRACHY
-- U+1FD1  ῑ GREEK SMALL LETTER IOTA WITH MACRON
ῒ : Token -- U+1FD2  ῒ GREEK SMALL LETTER IOTA WITH DIALYTIKA AND VARIA
ῒ = with-accent-diaeresis ι′ lower (grave ι-vowel) ι-diaeresis
ΐ : Token -- U+1FD3  ΐ GREEK SMALL LETTER IOTA WITH DIALYTIKA AND OXIA
ΐ = with-accent-diaeresis ι′ lower (acute ι-vowel) ι-diaeresis
-- U+1FD4
-- U+1FD5
ῖ : Token -- U+1FD6  ῖ GREEK SMALL LETTER IOTA WITH PERISPOMENI
ῖ = with-accent ι′ lower (circumflex ι-long-vowel)
ῗ : Token -- U+1FD7  ῗ GREEK SMALL LETTER IOTA WITH DIALYTIKA AND PERISPOMENI
ῗ = with-accent-diaeresis ι′ lower (circumflex ι-long-vowel) ι-diaeresis
-- U+1FD8 Ῐ GREEK CAPITAL LETTER IOTA WITH VRACHY
-- U+1FD9 Ῑ GREEK CAPITAL LETTER IOTA WITH MACRON
Ὶ : Token -- U+1FDA  Ὶ GREEK CAPITAL LETTER IOTA WITH VARIA
Ὶ = with-accent ι′ upper (grave ι-vowel)
Ί : Token -- U+1FDB  Ί GREEK CAPITAL LETTER IOTA WITH OXIA
Ί = with-accent ι′ upper (acute ι-vowel)
-- U+1FDC
-- U+1FDD  ῝ GREEK DASIA AND VARIA
-- U+1FDE  ῞ GREEK DASIA AND OXIA
-- U+1FDF  ῟ GREEK DASIA AND PERISPOMENI
-- U+1FE0 ῠ GREEK SMALL LETTER UPSILON WITH VRACHY
-- U+1FE1 ῡ GREEK SMALL LETTER UPSILON WITH MACRON
ῢ : Token -- U+1FE2  ῢ GREEK SMALL LETTER UPSILON WITH DIALYTIKA AND VARIA
ῢ = with-accent-diaeresis υ′ lower (grave υ-vowel) υ-diaeresis
ΰ : Token -- U+1FE3  ΰ GREEK SMALL LETTER UPSILON WITH DIALYTIKA AND OXIA
ΰ = with-accent-diaeresis υ′ lower (acute υ-vowel) υ-diaeresis
ῤ : Token -- U+1FE4 ῤ GREEK SMALL LETTER RHO WITH PSILI
ῤ = with-breathing ρ′ lower (smooth ρ-smooth)
ῥ : Token -- U+1FE5 ῥ GREEK SMALL LETTER RHO WITH DASIA
ῥ = with-breathing ρ′ lower (rough ρ-rough)
ῦ : Token -- U+1FE6  ῦ GREEK SMALL LETTER UPSILON WITH PERISPOMENI
ῦ = with-accent υ′ lower (circumflex υ-long-vowel)
ῧ : Token -- U+1FE7  ῧ GREEK SMALL LETTER UPSILON WITH DIALYTIKA AND PERISPOMENI
ῧ = with-accent-diaeresis υ′ lower (circumflex υ-long-vowel) υ-diaeresis
-- U+1FE8 Ῠ GREEK CAPITAL LETTER UPSILON WITH VRACHY
-- U+1FE9 Ῡ GREEK CAPITAL LETTER UPSILON WITH MACRON
Ὺ : Token -- U+1FEA  Ὺ GREEK CAPITAL LETTER UPSILON WITH VARIA
Ὺ = with-accent υ′ upper (grave υ-vowel)
Ύ : Token -- U+1FEB  Ύ GREEK CAPITAL LETTER UPSILON WITH OXIA
Ύ = with-accent υ′ upper (acute υ-vowel)
Ῥ : Token -- U+1FEC Ῥ GREEK CAPITAL LETTER RHO WITH DASIA
Ῥ = with-breathing ρ′ upper (rough ρ-rough)
-- U+1FED  ῭ GREEK DIALYTIKA AND VARIA
-- U+1FEE  ΅ GREEK DIALYTIKA AND OXIA
-- U+1FEF  ` GREEK VARIA
-- U+1FF0
-- U+1FF1
ῲ : Token -- U+1FF2  ῲ GREEK SMALL LETTER OMEGA WITH VARIA AND YPOGEGRAMMENI
ῲ = with-accent-iota ω′ lower (grave ω-vowel) ω-iota-subscript
ῳ : Token -- U+1FF3  ῳ GREEK SMALL LETTER OMEGA WITH YPOGEGRAMMENI
ῳ = with-iota ω′ lower ω-iota-subscript
ῴ : Token -- U+1FF4  ῴ GREEK SMALL LETTER OMEGA WITH OXIA AND YPOGEGRAMMENI
ῴ = with-accent-iota ω′ lower (acute ω-vowel) ω-iota-subscript
-- U+1FF5
ῶ : Token -- U+1FF6  ῶ GREEK SMALL LETTER OMEGA WITH PERISPOMENI
ῶ = with-accent ω′ lower (circumflex ω-long-vowel)
ῷ : Token -- U+1FF7  ῷ GREEK SMALL LETTER OMEGA WITH PERISPOMENI AND YPOGEGRAMMENI
ῷ = with-accent-iota ω′ lower (circumflex ω-long-vowel) ω-iota-subscript
Ὸ : Token -- U+1FF8  Ὸ GREEK CAPITAL LETTER OMICRON WITH VARIA
Ὸ = with-accent ο′ upper (grave ο-vowel)
Ό : Token -- U+1FF9  Ό GREEK CAPITAL LETTER OMICRON WITH OXIA
Ό = with-accent ο′ upper (acute ο-vowel)
Ὼ : Token -- U+1FFA  Ὼ GREEK CAPITAL LETTER OMEGA WITH VARIA
Ὼ = with-accent ω′ upper (grave ω-vowel)
Ώ : Token -- U+1FFB  Ώ GREEK CAPITAL LETTER OMEGA WITH OXIA
Ώ = with-accent ω′ upper (acute ω-vowel)
ῼ : Token -- U+1FFC  ῼ GREEK CAPITAL LETTER OMEGA WITH PROSGEGRAMMENI
ῼ = with-iota ω′ upper ω-iota-subscript
-- U+1FFD  ´ GREEK OXIA
-- U+1FFE  ῾ GREEK DASIA
-- U+1FFF

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Numbers.Naturals.Semiring -- for length
open import Lists.Lists
open import Functions.Definition
--open import Groups.Actions

module Groups.FinitePermutations where

allInsertions : {a : _} {A : Set a} (x : A) (l : List A) → List (List A)
allInsertions x [] = [ x ] :: []
allInsertions x (y :: l) = (x :: (y :: l)) :: (map (λ i → y :: i) (allInsertions x l))

permutations : {a : _} {A : Set a} (l : List A) → List (List A)
permutations [] = [ [] ]
permutations (x :: l) = flatten (map (allInsertions x) (permutations l))

factorial : ℕ → ℕ
factorial zero = 1
factorial (succ n) = (succ n) *N factorial n

factCheck : factorial 5 ≡ 120
factCheck = refl

allInsertionsLength : {a : _} {A : Set a} (x : A) (l : List A) → length (allInsertions x l) ≡ succ (length l)
allInsertionsLength x [] = refl
allInsertionsLength x (y :: l) = applyEquality succ (transitivity (equalityCommutative (lengthMap (allInsertions x l) {f = y ::_})) (allInsertionsLength x l))

allInsertionsLength' : {a : _} {A : Set a} (x : A) (l : List A) → allTrue (λ i → length i ≡ succ (length l)) (allInsertions x l)
allInsertionsLength' x [] = refl ,, record {}
allInsertionsLength' x (y :: l) with allInsertionsLength' x l
... | bl = refl ,, allTrueMap (λ i → length i ≡ succ (succ (length l))) (y ::_) (allInsertions x l) (allTrueExtension (λ z → length z ≡ succ (length l)) ((λ i → length i ≡ succ (succ (length l))) ∘ (y ::_)) (allInsertions x l) (λ {x} → λ p → applyEquality succ p) bl)

permutationsCheck : permutations (3 :: 4 :: []) ≡ (3 :: 4 :: []) :: (4 :: 3 :: []) :: []
permutationsCheck = refl

permsAllSameLength : {a : _} {A : Set a} (l : List A) → allTrue (λ i → length i ≡ length l) (permutations l)
permsAllSameLength [] = refl ,, record {}
permsAllSameLength (x :: l) with permsAllSameLength l
... | bl = allTrueFlatten (λ i → length i ≡ succ (length l)) (map (allInsertions x) (permutations l)) (allTrueMap (allTrue (λ i → length i ≡ succ (length l))) (allInsertions x) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (allTrue (λ i → length i ≡ succ (length l)) ∘ allInsertions x) (permutations l) lemma bl))
  where
    lemma : {m : List _} → (lenM=lenL : length m ≡ length l) → allTrue (λ i → length i ≡ succ (length l)) (allInsertions x m)
    lemma {m} lm=ll rewrite equalityCommutative lm=ll = allInsertionsLength' x m

allTrueEqual : {a b : _} {A : Set a} {B : Set b} (f : A → B) (equalTo : B) (l : List A) → allTrue (λ i → f i ≡ equalTo) l → map f l ≡ replicate (length l) equalTo
allTrueEqual f equalTo [] pr = refl
allTrueEqual f equalTo (x :: l) (fst ,, snd) rewrite fst | allTrueEqual f equalTo l snd = refl

totalReplicate : (l len : ℕ) → fold _+N_ 0 (replicate len l) ≡ l *N len
totalReplicate l zero rewrite multiplicationNIsCommutative l 0 = refl
totalReplicate l (succ len) rewrite totalReplicate l len | multiplicationNIsCommutative l (succ len) = applyEquality (l +N_) (multiplicationNIsCommutative l len)

permsLen : {a : _} {A : Set a} (l : List A) → length (permutations l) ≡ factorial (length l)
permsLen [] = refl
permsLen (x :: l) = transitivity (lengthFlatten (map (allInsertions x) (permutations l))) (transitivity (applyEquality (fold _+N_ 0) (mapMap (permutations l))) (transitivity (applyEquality (fold _+N_ 0) (mapExtension (permutations l) (length ∘ allInsertions x) (succ ∘ length) λ {y} → allInsertionsLength x y)) (transitivity (applyEquality (fold _+N_ 0) lemma) (transitivity (totalReplicate (succ (length l)) (length (permutations l))) ans))))
  where
    lemma : map (λ a → succ (length a)) (permutations l) ≡ replicate (length (permutations l)) (succ (length l))
    lemma = allTrueEqual (λ a → succ (length a)) (succ (length l)) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (λ i → succ (length i) ≡ succ (length l)) (permutations l) (λ pr → applyEquality succ pr) (permsAllSameLength l))
    ans : length (permutations l) +N length l *N length (permutations l) ≡ factorial (length l) +N length l *N factorial (length l)
    ans rewrite permsLen l = refl

--act : GroupAction (symmetricGroup (symmetricSetoid (reflSetoid (FinSet n))))
--act = ?

{- TODO: show that symmetricGroup acts in the obvious way on permutations FinSet
listElements : {a : _} {A : Set a} (l : List A) → Set
listElements [] = False
listElements (x :: l) = True || listElements l

listElement : {a : _} {A : Set a} {l : List A} (elt : listElements l) → A
listElement {l = []} ()
listElement {l = x :: l} (inl record {}) = x
listElement {l = x :: l} (inr elt) = listElement {l = l} elt

backwardRange : ℕ → List ℕ
backwardRange zero = []
backwardRange (succ n) = n :: backwardRange n

backwardRangeLength : {n : ℕ} → length (backwardRange n) ≡ n
backwardRangeLength {zero} = refl
backwardRangeLength {succ n} rewrite backwardRangeLength {n} = refl

applyPermutation : {n : ℕ} → (f : FinSet n → FinSet n) → listElements (permutations (backwardRange n)) → listElements (permutations (backwardRange n))
applyPermutation {zero} f (inl record {}) = inl (record {})
applyPermutation {zero} f (inr ())
applyPermutation {succ n} f elt = {!!}

finitePermutations : (n : ℕ) → SetoidToSet (symmetricSetoid (reflSetoid (FinSet n))) (listElements (permutations (backwardRange n)))
SetoidToSet.project (finitePermutations n) (sym {f} fBij) = {!!}
SetoidToSet.wellDefined (finitePermutations n) = {!!}
SetoidToSet.surj (finitePermutations n) = {!!}
SetoidToSet.inj (finitePermutations n) = {!!}

-}

ext: agda


text:
{-# OPTIONS --safe #-}
module RevRev where

open import Relation.Binary.PropositionalEquality
open import Data.List
open import Data.List.Properties

rev : ∀ {ℓ} {A : Set ℓ} → List A → List A
rev [] = []
rev (x ∷ xs) = rev xs ++ x ∷ []

lemma : ∀ {ℓ} {A : Set ℓ} (a b : List A) → rev (a ++ b) ≡ rev b ++ rev a
lemma [] b rewrite ++-identityʳ (rev b) = refl
lemma (x ∷ a) b rewrite lemma a b | ++-assoc (rev b) (rev a) (x ∷ []) = refl

revrevid : ∀ {ℓ} {A : Set ℓ} (a : List A) → rev (rev a) ≡ a
revrevid [] = refl
revrevid (x ∷ a) rewrite lemma (rev a) (x ∷ []) | revrevid a = refl

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
------------------------------------------------------------------------
-- Some properties about subsets
------------------------------------------------------------------------

module Data.Fin.Subset.Props where

open import Data.Nat
open import Data.Vec hiding (_∈_)
open import Data.Empty
open import Data.Function
open import Data.Fin
open import Data.Fin.Subset
open import Data.Product
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Constructor mangling

drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p
drop-there (there x∈p) = x∈p

drop-∷-⊆ : ∀ {n s₁ s₂} {p₁ p₂ : Subset n} → s₁ ∷ p₁ ⊆ s₂ ∷ p₂ → p₁ ⊆ p₂
drop-∷-⊆ p₁s₁⊆p₂s₂ x∈p₁ = drop-there $ p₁s₁⊆p₂s₂ (there x∈p₁)

drop-∷-Empty : ∀ {n s} {p : Subset n} → Empty (s ∷ p) → Empty p
drop-∷-Empty ¬¬∅ (x , x∈p) = ¬¬∅ (suc x , there x∈p)

------------------------------------------------------------------------
-- More interesting properties

allInside : ∀ {n} (x : Fin n) → x ∈ all inside
allInside zero    = here
allInside (suc x) = there (allInside x)

allOutside : ∀ {n} (x : Fin n) → x ∉ all outside
allOutside zero    ()
allOutside (suc x) (there x∈) = allOutside x x∈

⊆⊇⟶≡ : ∀ {n} {p₁ p₂ : Subset n} →
       p₁ ⊆ p₂ → p₂ ⊆ p₁ → p₁ ≡ p₂
⊆⊇⟶≡ = helper _ _
  where
  helper : ∀ {n} (p₁ p₂ : Subset n) →
           p₁ ⊆ p₂ → p₂ ⊆ p₁ → p₁ ≡ p₂
  helper []            []             _   _   = refl
  helper (s₁ ∷ p₁)     (s₂ ∷ p₂)      ₁⊆₂ ₂⊆₁ with ⊆⊇⟶≡ (drop-∷-⊆ ₁⊆₂)
                                                        (drop-∷-⊆ ₂⊆₁)
  helper (outside ∷ p) (outside ∷ .p) ₁⊆₂ ₂⊆₁ | refl = refl
  helper (inside  ∷ p) (inside  ∷ .p) ₁⊆₂ ₂⊆₁ | refl = refl
  helper (outside ∷ p) (inside  ∷ .p) ₁⊆₂ ₂⊆₁ | refl with ₂⊆₁ here
  ...                                                | ()
  helper (inside  ∷ p) (outside ∷ .p) ₁⊆₂ ₂⊆₁ | refl with ₁⊆₂ here
  ...                                                | ()

∅⟶allOutside : ∀ {n} {p : Subset n} →
               Empty p → p ≡ all outside
∅⟶allOutside {p = []}     ¬¬∅ = refl
∅⟶allOutside {p = s ∷ ps} ¬¬∅ with ∅⟶allOutside (drop-∷-Empty ¬¬∅)
∅⟶allOutside {p = outside ∷ .(all outside)} ¬¬∅ | refl = refl
∅⟶allOutside {p = inside  ∷ .(all outside)} ¬¬∅ | refl =
  ⊥-elim (¬¬∅ (zero , here))

max_issues_repo_name: larrytheliquid/Lemmachine


text:
postulate
  A B : Set
  f : @0 {{A}} → B

g : @0 {{A}} → B
g = f


text:
{-# OPTIONS --without-K #-}
module sets.nat.struct where

open import sum
open import equality
open import function
open import container.core
open import container.w
open import sets.empty
open import sets.unit
open import sets.nat.core
open import sets.fin
open import sets.vec.dependent
open import hott.level

ℕ-c : Container _ _ _
ℕ-c = record
  { I = ⊤
  ; A = λ _ → Fin 2
  ; B = ⊥ ∷∷ ⊤ ∷∷ ⟦⟧
  ; r = λ _ → tt }

open Container ℕ-c

ℕ-algebra-iso : (⊤ ⊎ ℕ) ≅ ℕ
ℕ-algebra-iso = record
  { to = λ { (inj₁ _) → zero ; (inj₂ n) → suc n }
  ; from = λ { zero → inj₁ tt ; (suc n) → inj₂ n }
  ; iso₁ = λ { (inj₁ _) → refl ; (inj₂ n) → refl }
  ; iso₂ = λ { zero → refl ; (suc n) → refl } }

private
  inℕ : F (λ _ → ℕ) tt → ℕ
  inℕ (zero , u) = 0
  inℕ (suc zero , u) = suc (u tt)
  inℕ (suc (suc ()) , u)

ℕ-struct-iso : ℕ ≅ W ℕ-c tt
ℕ-struct-iso = iso f g α β
  where
    f : ℕ → W ℕ-c tt
    f 0 = sup (zero) (λ ())
    f (suc n) = sup (suc zero) (λ _ → f n)

    g : W ℕ-c tt → ℕ
    g = fold ℕ-c (λ i → inℕ) tt

    α : (n : ℕ) → g (f n) ≡ n
    α zero = refl
    α (suc n) = ap suc (α n)

    β : (n : W ℕ-c tt) → f (g n) ≡ n
    β (sup zero u) = ap (sup zero) (funext λ ())
    β (sup (suc zero) u) = ap (sup (suc zero)) (funext (λ x → β (u tt)))
    β (sup (suc (suc ())) u)

private
  F-struct-iso : ∀ {i}(X : ⊤ → Set i) → F X tt ≅ (⊤ ⊎ X tt)
  F-struct-iso X = begin
      ( Σ (A tt) λ a → B a → X tt )
    ≅⟨ sym≅ (⊎-Σ-iso (λ a → B a → X tt)) ⟩
      ( (⊥ → X tt) ⊎ (⊤ → X tt) )
    ≅⟨ ⊎-ap-iso (contr-⊤-iso ⊥-initial) Π-left-unit ⟩
      ( ⊤ ⊎ X tt )
    ∎
    where open ≅-Reasoning

ℕ-initial : ∀ {i} (X : ℕ → Set i)
          → (x₀ : X 0)(f : ∀ n → X n → X (suc n))
          → contr ( Σ ((n : ℕ) → X n) λ x
                  → (x₀ ≡ x 0)
                  × (∀ n → f n (x n) ≡ x (suc n)) )
ℕ-initial X x₀ f = iso-level ℕ-alg-iso (W-section-contr ℕ-c 𝓧)
  where
    ψ : ∀ x → ((b : B (proj₁ x)) → X (proj₂ x b)) → X (inℕ x)
    ψ (zero , u) v = x₀
    ψ (suc zero , u) v = f (u tt) (v tt)
    ψ (suc (suc ()) , u) v

    P : ∀ i (n : W ℕ-c i) → Set _
    P i n = X (invert ℕ-struct-iso n)

    θ : ∀ i x → ((b : B (proj₁ x)) → P tt (proj₂ x b)) → P i (inW ℕ-c i x)
    θ i (a , u) v = ψ (a , invert ℕ-struct-iso ∘' u) v

    𝓧 : AlgFib ℕ-c _
    𝓧 = P , θ

    ℕ-alg-iso : AlgSection ℕ-c 𝓧 ≅
              ( Σ ((n : ℕ) → X n) λ x
              → (x₀ ≡ x 0)
              × (∀ n → f n (x n) ≡ x (suc n)) )
    ℕ-alg-iso = begin
        AlgSection ℕ-c 𝓧
      ≅⟨ ( Σ-ap-iso Π-left-unit λ g → iso≡ Π-left-unit) ⟩
        ( Σ ((w : W ℕ-c tt) → P tt w) λ g
        → ( _≡_ {A = (x : F (W ℕ-c) tt) → P tt (inW ℕ-c tt x)}
            (λ x → θ tt x (λ b → g (proj₂ x b)))
            (λ x → g (inW ℕ-c tt x)) ) )
      ≅⟨ sym≅ ( Σ-ap-iso (Π-ap-iso ℕ-struct-iso λ _ → refl≅) λ g
         → iso≡ (Π-ap-iso (sym≅ (F-ap-iso (λ i → sym≅ ℕ-struct-iso) tt)) λ x
                → refl≅ ) ) ⟩
        ( Σ ((n : ℕ) → X n) λ g
        → ( _≡_ {A = (x : F (λ _ → ℕ) tt) → X (inℕ x)}
            (λ x → ψ x (λ b → g (proj₂ x b)))
            (λ x → g (inℕ x)) ) )
      ≅⟨ ( Σ-ap-iso refl≅ λ g
         → iso≡ (Π-ap-iso (F-struct-iso (λ _ → ℕ)) λ _ → refl≅) ) ⟩
        ( let φ = invert (F-struct-iso (λ _ → ℕ))
        in Σ ((n : ℕ) → X n) λ g
        → ( _≡_ {A = (x : ⊤ ⊎ ℕ) → X (inℕ (φ x))}
            (λ x → ψ (φ x) (λ b → g (proj₂ (φ x) b)))
            (λ x → g (inℕ (φ x))) ) )
      ≅⟨ ( Σ-ap-iso refl≅ λ x → iso≡ ⊎-universal ) ⟩
        ( Σ ((n : ℕ) → X n) λ x
        → ( _≡_ {A = (⊤ → X 0) × ((n : ℕ) → X (suc n))}
            ((λ _ → x₀) , (λ n → f n (x n)))
            ((λ _ → x 0) , (λ n → x (suc n))) ) )
      ≅⟨ ( Σ-ap-iso refl≅ λ x → sym≅ ×-split-iso ) ⟩
        ( Σ ((n : ℕ) → X n) λ x
        → (_≡_ {A = ⊤ → X 0} (λ _ → x₀) (λ _ → x 0))
        × (_≡_ {A = (n : ℕ) → X (suc n)} (λ n → f n (x n)) (λ n → x (suc n))) )
      ≅⟨ ( Σ-ap-iso refl≅ λ x → ×-ap-iso (iso≡ Π-left-unit) (sym≅ strong-funext-iso) ) ⟩
        ( Σ ((n : ℕ) → X n) λ x
        → (x₀ ≡ x 0)
        × (∀ n → f n (x n) ≡ x (suc n)) )
      ∎
      where
        open ≅-Reasoning

ℕ-initial-simple : ∀ {i} {X : Set i} (x₀ : X)
                 → contr ( Σ (ℕ → X) λ x
                         → (x₀ ≡ x 0)
                         × (∀ n → x n ≡ x (suc n)) )
ℕ-initial-simple {X = X} x₀
  = ((λ _ → x₀) , refl , λ _ → refl)
  , (λ u → contr⇒prop (ℕ-initial (λ _ → X) x₀ (λ _ x → x)) _ u)

ℕ-elim-shift : ∀ {i}{X : ℕ → Set i}
             → ((n : ℕ) → X n)
             ≅ ( (X 0) × ((n : ℕ) → X (suc n)) )
ℕ-elim-shift {i}{X} = begin
    ((n : ℕ) → X n)
  ≅⟨ (Π-ap-iso (sym≅ ℕ-algebra-iso) λ _ → refl≅) ⟩
    ((n : ⊤ ⊎ ℕ) → X (apply ℕ-algebra-iso n))
  ≅⟨ ⊎-universal ⟩
    ((⊤ → X 0) × ((n : ℕ) → X (suc n)))
  ≅⟨ ×-ap-iso Π-left-unit refl≅ ⟩
    (X 0 × ((n : ℕ) → X (suc n)))
  ∎
  where
    open ≅-Reasoning

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Category.Functor.Lawful where
open import Agda.Primitive using (lsuc; _⊔_)
open import Category.Functor
open import Category.Applicative
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; module ≡-Reasoning; sym; cong)

record LawfulFunctorImp {l₁ l₂} {F : Set l₁ → Set l₂} (FFunc : RawFunctor F) : Set (lsuc l₁ ⊔ l₂) where
  open RawFunctor FFunc
  field
    <$>-identity : ∀ {a} {x : F a} → (id <$> x) ≡ x
    <$>-compose  : ∀ {a b c} {f : a → b} {g : b → c} {x : F a} → ((g ∘ f) <$> x) ≡ (g <$> (f <$> x))

module LawfulFunctor {l₁ l₂} {F : Set l₁ → Set l₂} {FFunc : RawFunctor F} (FLawful : LawfulFunctorImp FFunc) where
  open RawFunctor FFunc public
  open LawfulFunctorImp FLawful public

record LawfulApplicativeImp {l} {F : Set l → Set l} (FAppl : RawApplicative F) : Set (lsuc l) where
  open RawApplicative FAppl
  field
    ⊛-identity     : ∀ {A}     {u : F A}                                 → (pure id ⊛ u) ≡ u
    ⊛-homomorphism : ∀ {A B}   {u :    A → B } {v : A}                   → (pure u ⊛ pure v) ≡ pure (u v)
    ⊛-interchange  : ∀ {A B}   {u : F (A → B)} {v : A}                   → (u ⊛ pure v) ≡ (pure (λ uᵢ → uᵢ v) ⊛ u)
    ⊛-composition  : ∀ {A B C} {u : F (B → C)} {v : F (A → B)} {w : F A} → (pure (λ f g a → f (g a)) ⊛ u ⊛ v ⊛ w) ≡ (u ⊛ (v ⊛ w))
  open ≡-Reasoning
  private
    composelemma  : ∀ {a b c} {f : a → b} {g : b → c} {x : F a} → ((g ∘ f) <$> x) ≡ (g <$> (f <$> x))
    composelemma {_} {_} {_} {f} {g} {x} =
      pure (λ x₁ → g (f x₁)) ⊛ x ≡⟨ cong (_⊛ x) (sym ⊛-homomorphism) ⟩
      pure (λ f x → g (f x)) ⊛ pure f ⊛ x ≡⟨ cong ((_⊛ x) ∘ (_⊛ pure f)) (sym ⊛-homomorphism) ⟩
      pure (λ g f x → g (f x)) ⊛ pure g ⊛ pure f ⊛ x ≡⟨ ⊛-composition ⟩
      pure g ⊛ (pure f ⊛ x) ∎
  isLawfulFunctor : LawfulFunctorImp rawFunctor
  isLawfulFunctor = record
    { <$>-identity = ⊛-identity
    ; <$>-compose = composelemma
    }

module LawfulApplicative {l} {F : Set l → Set l} (FAppl : RawApplicative F) (FLawful : LawfulApplicativeImp FAppl) where
  open RawApplicative FAppl public
  open LawfulApplicativeImp FLawful public
  open LawfulFunctorImp isLawfulFunctor public

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
module Common.Equality where

open import Common.Level

infix 4 _≡_

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

subst : ∀ {a p}{A : Set a}(P : A → Set p){x y : A} → x ≡ y → P x → P y
subst P refl t = t

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unary relations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Relation.Unary where

open import Data.Empty
open import Data.Unit.Base using (⊤)
open import Data.Product
open import Data.Sum using (_⊎_; [_,_])
open import Function
open import Level
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

------------------------------------------------------------------------
-- Unary relations

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Pred A ℓ = A → Set ℓ

------------------------------------------------------------------------
-- Unary relations can be seen as sets
-- i.e. they can be seen as subsets of the universe of discourse.

module _ {a} {A : Set a} where

  ----------------------------------------------------------------------
  -- Special sets

  -- The empty set

  ∅ : Pred A zero
  ∅ = λ _ → ⊥

  -- The singleton set

  ｛_｝ : A → Pred A a
  ｛ x ｝ = x ≡_

  -- The universe

  U : Pred A zero
  U = λ _ → ⊤

  ----------------------------------------------------------------------
  -- Membership

  infix 4 _∈_ _∉_

  _∈_ : ∀ {ℓ} → A → Pred A ℓ → Set _
  x ∈ P = P x

  _∉_ : ∀ {ℓ} → A → Pred A ℓ → Set _
  x ∉ P = ¬ x ∈ P

  ----------------------------------------------------------------------
  -- Subsets

  infix 4 _⊆_ _⊇_ _⊈_ _⊉_ _⊂_ _⊃_ _⊄_ _⊅_

  _⊆_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

  _⊇_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊇ Q = Q ⊆ P

  _⊈_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊈ Q = ¬ (P ⊆ Q)

  _⊉_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊉ Q = ¬ (P ⊇ Q)

  _⊂_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊂ Q = P ⊆ Q × Q ⊈ P

  _⊃_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊃ Q = Q ⊂ P

  _⊄_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊄ Q = ¬ (P ⊂ Q)

  _⊅_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊅ Q = ¬ (P ⊃ Q)

  -- Dashed variants of _⊆_ for when 'x' can't be inferred from 'x ∈ P'.

  infix 4 _⊆′_ _⊇′_ _⊈′_ _⊉′_ _⊂′_ _⊃′_ _⊄′_ _⊅′_

  _⊆′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q

  _⊇′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  Q ⊇′ P = P ⊆′ Q

  _⊈′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊈′ Q = ¬ (P ⊆′ Q)

  _⊉′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊉′ Q = ¬ (P ⊇′ Q)

  _⊂′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊂′ Q = P ⊆′ Q × Q ⊈′ P

  _⊃′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊃′ Q = Q ⊂′ P

  _⊄′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊄′ Q = ¬ (P ⊂′ Q)

  _⊅′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ⊅′ Q = ¬ (P ⊃′ Q)

  ----------------------------------------------------------------------
  -- Properties of sets

  -- Emptiness

  Empty : ∀ {ℓ} → Pred A ℓ → Set _
  Empty P = ∀ x → x ∉ P

  -- Satisfiable

  Satisfiable : ∀ {ℓ} → Pred A ℓ → Set _
  Satisfiable P = ∃ λ x → x ∈ P

  -- Universality

  infix 10 Universal IUniversal
  Universal : ∀ {ℓ} → Pred A ℓ → Set _
  Universal P = ∀ x → x ∈ P

  IUniversal : ∀ {ℓ} → Pred A ℓ → Set _
  IUniversal P = ∀ {x} → x ∈ P

  syntax Universal  P = Π[ P ]
  syntax IUniversal P = ∀[ P ]

  -- Decidability

  Decidable : ∀ {ℓ} → Pred A ℓ → Set _
  Decidable P = ∀ x → Dec (P x)

  -- Irrelevance

  Irrelevant : ∀ {ℓ} → Pred A ℓ → Set _
  Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b

  ----------------------------------------------------------------------
  -- Operations on sets

  -- Set complement.

  ∁ : ∀ {ℓ} → Pred A ℓ → Pred A ℓ
  ∁ P = λ x → x ∉ P

  -- Positive version of non-disjointness, dual to inclusion.

  infix 4 _≬_

  _≬_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
  P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q

  -- Set union.

  infixr 6 _∪_

  _∪_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
  P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q

  -- Set intersection.

  infixr 7 _∩_

  _∩_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
  P ∩ Q = λ x → x ∈ P × x ∈ Q

  -- Implication.

  infixr 8 _⇒_

  _⇒_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
  P ⇒ Q = λ x → x ∈ P → x ∈ Q

  -- Infinitary union and intersection.

  infix 10 ⋃ ⋂

  ⋃ : ∀ {ℓ i} (I : Set i) → (I → Pred A ℓ) → Pred A _
  ⋃ I P = λ x → Σ[ i ∈ I ] P i x

  syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P

  ⋂ : ∀ {ℓ i} (I : Set i) → (I → Pred A ℓ) → Pred A _
  ⋂ I P = λ x → (i : I) → P i x

  syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P

-- Update.

infixr 9 _⊢_

_⊢_ : ∀ {a b} {A : Set a} {B : Set b} {ℓ} → (A → B) → Pred B ℓ → Pred A ℓ
f ⊢ P = λ x → P (f x)

------------------------------------------------------------------------
-- Unary relation combinators

infixr  2 _⟨×⟩_
infixr  2 _⟨⊙⟩_
infixr  1 _⟨⊎⟩_
infixr  0 _⟨→⟩_
infixl  9 _⟨·⟩_
infix  10 _~
infixr  9 _⟨∘⟩_
infixr  2 _//_ _\\_

_⟨×⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
        Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q

_⟨⊙⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
        Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q

_⟨⊎⟩_ : ∀ {a b ℓ} {A : Set a} {B : Set b} →
        Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
P ⟨⊎⟩ Q = [ P , Q ]

_⟨→⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
        Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
(P ⟨→⟩ Q) f = P ⊆ Q ∘ f

_⟨·⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
        (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
(P ⟨·⟩ Q) (p , f) = f p

-- Converse.

_~ : ∀ {a b ℓ} {A : Set a} {B : Set b} →
     Pred (A × B) ℓ → Pred (B × A) ℓ
P ~ = P ∘ swap

-- Composition.

_⟨∘⟩_ : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} →
        Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
(P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q

-- Post and pre-division.

_//_ : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} →
       Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
(P // Q) (x , y) = Q ∘ _,_ y ⊆ P ∘ _,_ x

_\\_ : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c} →
       Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
P \\ Q = (P ~ // Q ~) ~


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Sn.Base where

open import Cubical.HITs.Susp
open import Cubical.Foundations.Pointed
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne
open import Cubical.Data.Empty
open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool
open import Cubical.HITs.S1

S : ℕ₋₁ → Type₀
S neg1 = ⊥
S (ℕ→ℕ₋₁ n) = Susp (S (-1+ n))

S₊ : ℕ → Type₀
S₊ 0 = Bool
S₊ 1 = S¹
S₊ (suc (suc n)) = Susp (S₊ (suc n))

ptSn : (n : ℕ) → S₊ n
ptSn zero = true
ptSn (suc zero) = base
ptSn (suc (suc n)) = north

-- Pointed version
S₊∙ : (n : ℕ) → Pointed₀
S₊∙ n = (S₊ n) , ptSn n

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --cubical --safe #-}

module Data.List.Syntax where

open import Data.List
open import Prelude

open import Data.Vec.Sigma using () renaming (toList to [_]) public
open import Data.Vec.Sigma

[_][_] : ∀ n → Vec A n → List A
[ n ][ xs ] = toList {n = n} xs

-- record ListSyntax {a b} (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
--   field [_] : B → List A

-- open ListSyntax ⦃ ... ⦄ public

-- instance
--   cons : ⦃ _ : ListSyntax A B ⦄ →  ListSyntax A (A × B)
--   [_] ⦃ cons ⦄ (x , xs) = x ∷ [ xs ]

-- instance
--   sing : ListSyntax A A
--   [_] ⦃ sing ⦄ = _∷ []

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Data.Nat.DivMod.Properties where

open import Data.Nat
open ≤-Reasoning
open import Data.Nat.DivMod
open import Data.Nat.Etc
open import Data.Nat.Properties using (≰⇒>; m≤m+n)
open import Data.Nat.Properties.Simple using (+-right-identity; +-suc; +-assoc; +-comm; distribʳ-*-+)
open import Data.Fin using (Fin; toℕ; fromℕ; fromℕ≤; inject≤; inject₁)
    renaming (_+_ to _F+_; zero to Fzero; suc to Fsuc)
open import Data.Fin.Properties using (bounded)
open import Function
-- import Level

open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Nullary.Decidable using (True; False; toWitness)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; sym; trans; inspect)
open PropEq.≡-Reasoning
    renaming (begin_ to beginEq_; _≡⟨_⟩_ to _≡Eq⟨_⟩_; _∎ to _∎Eq)

ℕ-isDecTotalOrder   = DecTotalOrder.isDecTotalOrder decTotalOrder
ℕ-isTotalOrder      = IsDecTotalOrder.isTotalOrder ℕ-isDecTotalOrder
ℕ-isPartialOrder    = IsTotalOrder.isPartialOrder ℕ-isTotalOrder
ℕ-isPreorder        = IsPartialOrder.isPreorder ℕ-isPartialOrder
≤-refl      = IsPreorder.reflexive ℕ-isPreorder
≤-antisym   = IsPartialOrder.antisym ℕ-isPartialOrder
≤-total     = IsTotalOrder.total ℕ-isTotalOrder

lem-+-exchange : ∀ a b c d → (a + b) + (c + d) ≡ (a + c) + (b + d)
lem-+-exchange a b c d = beginEq
        (a + b) + (c + d)
    ≡Eq⟨ sym (+-assoc (a + b) c d) ⟩
        a + b + c + d
    ≡Eq⟨ cong (λ x → x + d) (+-assoc a b c) ⟩
        a + (b + c) + d
    ≡Eq⟨ cong (λ x → a + x + d) (+-comm b c) ⟩
        a + (c + b) + d
    ≡Eq⟨ cong (λ x → x + d) (sym (+-assoc a c b)) ⟩
        a + c + b + d
    ≡Eq⟨ +-assoc (a + c) b d ⟩
        (a + c) + (b + d)
    ∎Eq
{-
beginEq
    {!   !}
≡Eq⟨ {!   !} ⟩
    {!   !}
≡Eq⟨ {!   !} ⟩
    {!   !}
≡Eq⟨ {!   !} ⟩
    {!   !}
≡Eq⟨ {!   !} ⟩
    {!   !}
∎Eq
-}

record DM (dividend divisor : ℕ) : Set where
    constructor dm
    field
        q : ℕ
        r : Fin divisor
{-
_DM+_ : ∀ {b m n} → DM m b → DM n b → DM (m + n) b
_DM+_ {zero}          (dm q₀ ()) (dm q₁ ())
_DM+_ {suc b} (dm zero Fzero) (dm q₁ r₁) = dm q₁ Fzero
_DM+_ {suc n₁} (dm zero (Fsuc r₀)) (dm q₁ r₁) = {!   !}
_DM+_ {suc b} (dm (suc q₀) Fzero) (dm q₁ r₁) = {!   !}
_DM+_ {suc b} (dm (suc q₀) (Fsuc r₀)) (dm q₁ r₁) = {!   !}
-}
{-
_DivMod+_ : ∀ {b m n} → DivMod m b → DivMod n b → DivMod (m + n) b
_DivMod+_ {zero}          (result q₀       ()        prop₀) (result q₁ () prop₁)
_DivMod+_ {suc b} {m} {n} (result zero     Fzero     prop₀) (result q₁ r₁ prop₁) = result q₁ r₁ {! prop₁  !} -- (cong₂ _+_ prop₀ prop₁)
_DivMod+_ {suc b} {m} {n} (result zero     (Fsuc r₀) prop₀) (result q₁ r₁ prop₁) with ((toℕ (Fsuc r₀) + toℕ r₁) divMod (suc b))
_DivMod+_ {suc b} {m} {n} (result zero     (Fsuc r₀) prop₀) (result q₁ r₁ prop₁) | result zero rᵣ propᵣ =
    let q = q₁
        r = rᵣ
    in  result q r $
            beginEq
                m + n
            ≡Eq⟨ cong₂ _+_ prop₀ prop₁ ⟩
                suc (toℕ r₀ + zero + (toℕ r₁ + q₁ * suc b))
            ≡Eq⟨ lem-+-exchange (suc (toℕ r₀)) zero (toℕ r₁) (q₁ * suc b) ⟩
                suc (toℕ r₀ + toℕ r₁) + (q₁ * suc b)
            ≡Eq⟨ cong (λ x → x + q₁ * suc b) propᵣ ⟩
                toℕ rᵣ + zero + q₁ * suc b
            ≡Eq⟨ cong (λ x → x + q₁ * suc b) (+-right-identity (toℕ rᵣ)) ⟩
                toℕ rᵣ + q₁ * suc b
            ∎Eq
_DivMod+_ {suc b} {m} {n} (result zero     (Fsuc r₀) prop₀) (result q₁ r₁ prop₁) | result (suc qᵣ) rᵣ propᵣ =
    let q = suc qᵣ + q₁
        r = rᵣ
    in  result q r $
            beginEq
                m + n
            ≡Eq⟨ cong₂ _+_ prop₀ prop₁ ⟩
                suc (toℕ r₀) + zero + (toℕ r₁ + q₁ * suc b)
            ≡Eq⟨ lem-+-exchange (suc (toℕ r₀)) zero (toℕ r₁) (q₁ * suc b) ⟩
                suc (toℕ r₀) + toℕ r₁ + q₁ * suc b
            ≡Eq⟨ cong (λ x → x + q₁ * suc b) propᵣ ⟩
                toℕ rᵣ + suc qᵣ * suc b + q₁ * suc b
            ≡Eq⟨ +-assoc (toℕ rᵣ) (suc qᵣ * suc b) (q₁ * suc b) ⟩
                toℕ rᵣ + (suc qᵣ * suc b + q₁ * suc b)
            ≡Eq⟨ cong (λ x → toℕ rᵣ + x) (sym (distribʳ-*-+ (suc b) (suc qᵣ) q₁)) ⟩
                toℕ rᵣ + (suc qᵣ + q₁) * suc b
            ∎Eq
_DivMod+_ {suc b} {m} {n} (result (suc q₀) Fzero     prop₀) (result q₁ r₁ prop₁) = result (suc q₀ + q₁) r₁ $
    beginEq
        m + n
    ≡Eq⟨ cong₂ _+_ prop₀ prop₁ ⟩
        suc q₀ * suc b + (toℕ r₁ + q₁ * suc b)
    ≡Eq⟨ sym (+-assoc (suc (b + q₀ * suc b)) (toℕ r₁) (q₁ * suc b)) ⟩
        suc q₀ * suc b + toℕ r₁ + q₁ * suc b
    ≡Eq⟨ cong (λ x → x + q₁ * suc b) (+-comm (suc q₀ * suc b) (toℕ r₁)) ⟩
        toℕ r₁ + suc q₀ * suc b + q₁ * suc b
    ≡Eq⟨ +-assoc (toℕ r₁) (suc q₀ * suc b) (q₁ * suc b) ⟩
        toℕ r₁ + (suc q₀ * suc b + q₁ * suc b)
    ≡Eq⟨ cong (λ x → toℕ r₁ + x) (sym (distribʳ-*-+ (suc b) (suc q₀) q₁)) ⟩
        toℕ r₁ + (suc q₀ + q₁) * suc b
    ∎Eq
_DivMod+_ {suc b} {m} {n} (result (suc q₀) (Fsuc r₀) prop₀) (result q₁ r₁ prop₁) with ((toℕ (Fsuc r₀) + toℕ r₁) divMod (suc b))
_DivMod+_ {suc b} {m} {n} (result (suc q₀) (Fsuc r₀) prop₀) (result q₁ r₁ prop₁) | result zero     rᵣ propᵣ =
    let q = suc q₀ + q₁
        r = rᵣ
    in  result q r $
            beginEq
                m + n
            ≡Eq⟨ cong₂ _+_ prop₀ prop₁ ⟩
                (suc (toℕ r₀) + suc q₀ * suc b) + (toℕ r₁ + q₁ * suc b)
            ≡Eq⟨ lem-+-exchange (suc (toℕ r₀)) (suc (b + q₀ * suc b)) (toℕ r₁) (q₁ * suc b) ⟩
                (suc (toℕ r₀) + toℕ r₁) + (suc q₀ * suc b + q₁ * suc b)
            ≡Eq⟨ cong (λ x → (suc (toℕ r₀) + toℕ r₁) + x) (sym (distribʳ-*-+ (suc b) (suc q₀) q₁)) ⟩
                (suc (toℕ r₀) + toℕ r₁) + (suc q₀ + q₁) * suc b
            ≡Eq⟨ cong (λ x → x + suc (q₀ + q₁) * suc b) propᵣ ⟩
                toℕ rᵣ + zero + suc (b + (q₀ + q₁) * suc b)
            ≡Eq⟨ cong (λ x → x + suc (q₀ + q₁) * suc b) (+-right-identity (toℕ rᵣ)) ⟩
                toℕ rᵣ + suc (q₀ + q₁) * suc b
            ∎Eq
_DivMod+_ {suc b} {m} {n} (result (suc q₀) (Fsuc r₀) prop₀) (result q₁ r₁ prop₁) | result (suc qᵣ) rᵣ propᵣ =
    let q = suc qᵣ + (suc q₀ + q₁)
        r = rᵣ
    in  result q r $
            beginEq
                m + n
            ≡Eq⟨ cong₂ _+_ prop₀ prop₁ ⟩
                suc (toℕ r₀ + suc q₀ * suc b) + (toℕ r₁ + q₁ * suc b)
            ≡Eq⟨ lem-+-exchange (suc (toℕ r₀)) (suc (b + q₀ * suc b)) (toℕ r₁) (q₁ * suc b) ⟩
                suc (toℕ r₀) + toℕ r₁ + ((suc q₀) * suc b + q₁ * suc b)
            ≡Eq⟨ cong (λ x → suc (toℕ r₀) + toℕ r₁ + x) (sym (distribʳ-*-+ (suc b) (suc q₀) q₁)) ⟩
                suc (toℕ r₀) + toℕ r₁ + (suc q₀ + q₁) * suc b
            ≡Eq⟨ cong (λ x → x + (suc q₀ + q₁) * suc b) propᵣ ⟩
                toℕ rᵣ + suc qᵣ * suc b + (suc q₀ + q₁) * suc b
            ≡Eq⟨ +-assoc (toℕ rᵣ) (suc qᵣ * suc b) ((suc q₀ + q₁) * suc b) ⟩
                toℕ rᵣ + (suc qᵣ * suc b + (suc q₀ + q₁) * suc b)
            ≡Eq⟨ cong (λ x → toℕ rᵣ + x) (sym (distribʳ-*-+ (suc b) (suc qᵣ) (suc (q₀ + q₁)))) ⟩
                toℕ rᵣ + (suc qᵣ + (suc q₀ + q₁)) * suc b
            ∎Eq
-}
-- DivMod+-left-identity : ∀ {b n} → (x : DivMod n (suc b)) → _DivMod+_ {suc b} {0} {n} (result 0 Fzero refl) x ≡ x
-- DivMod+-left-identity {b} {n} (result q r prop) = {!   !}
{-
    beginEq
        _DivMod+_ {suc b} {m} {n} (result 0 Fzero p) (result q r prop)
    ≡Eq⟨ refl ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        result q r prop
    ∎Eq -- cong (result q r) {!   !} -- cong (result q r) refl
-}
{-
DivMod+-left-identity : ∀ {b m} → (x : DivMod m (suc b)) → (result 0 Fzero refl) DivMod+ x ≡ x
DivMod+-left-identity {b} {m} (result q r prop) with (toℕ Fzero + toℕ r) divMod (suc b)
DivMod+-left-identity {b} {m} (result q r prop) | result zero rᵣ propᵣ =
    -- propᵣ : toℕ r ≡ toℕ rᵣ + 0
    -- prop  :      m ≡ toℕ r  + q * suc b
    -- prop  :      m ≡ toℕ rᵣ + q * suc b
    -- trans (cong₂ _+_ refl prop) (trans (trans (cong (λ z → z + q * suc b) (sym (+-right-identity (toℕ r)))) (trans (+-assoc (toℕ r) zero (q * suc b)) refl)) (trans (cong₂ _+_ propᵣ refl) (trans (cong (λ z → z + q * suc b) (+-right-identity (toℕ rᵣ))) refl))))
    let prop' = beginEq
                m
            ≡Eq⟨ cong₂ _+_ refl prop ⟩
                toℕ r + q * suc b
            ≡Eq⟨ cong₂ _+_ propᵣ refl ⟩
                toℕ rᵣ + 0 + q * suc b
            ≡Eq⟨ cong₂ _+_ (+-right-identity (toℕ rᵣ)) refl ⟩
                toℕ rᵣ + q * suc b
            ∎Eq
    in  beginEq
            result q rᵣ prop'
        ≡Eq⟨ cong (λ x → result q x {! prop'  !}) (sym {! +-right-identity  !}) ⟩
            {!   !}
        ≡Eq⟨ {!   !} ⟩
            {!   !}
        ≡Eq⟨ {!   !} ⟩
            {!   !}
        ≡Eq⟨ {!   !} ⟩
            result q r prop
        ∎Eq
DivMod+-left-identity (result q r prop) | result (suc qᵣ) rᵣ propᵣ = {!   !}
-}
{-
DivMod+-left-identity : ∀ {b m} → (x : DivMod m (suc b)) → (result 0 Fzero refl) DivMod+ x ≡ x
DivMod+-left-identity {b} {m} (result q r prop) with (toℕ r) divMod (suc b)
DivMod+-left-identity {b} {m} (result q r prop) | result zero rᵣ propᵣ =
    beginEq
        result q rᵣ (beginEq
                m
            ≡Eq⟨ cong (λ z → z) prop ⟩
                toℕ r + q * suc b
            ≡Eq⟨ cong (λ z → z + q * suc b) (sym (+-right-identity (toℕ r))) ⟩
                (toℕ r + zero) + q * suc b
            ≡Eq⟨ cong (λ z → z + zero + q * suc b) propᵣ ⟩
                toℕ rᵣ + zero + zero + q * suc b
            ≡Eq⟨ cong (λ z → z + zero + q * suc b) (+-right-identity (toℕ rᵣ)) ⟩
                (toℕ rᵣ + zero) + q * suc b
            ≡Eq⟨ +-assoc (toℕ rᵣ) zero (q * suc b) ⟩
                toℕ rᵣ + q * suc b
            ∎Eq)
    ≡Eq⟨ {!   !} ⟩
        result q r prop
    ∎Eq
DivMod+-left-identity (result q r prop) | result (suc qᵣ) rᵣ propᵣ =
    beginEq
        (result 0 Fzero refl) DivMod+ {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!    !} ⟩
        {!    !}
    ≡Eq⟨ {!    !} ⟩
        result q r prop
    ∎Eq

DivMod+-left-identity : (b n : ℕ) → (≢0 : False (b ≟ 0)) → ((0 divMod b) {≢0}) DivMod+ ((n divMod b) {≢0}) ≡ ((n divMod b) {≢0})
DivMod+-left-identity zero n ()
DivMod+-left-identity (suc b) zero ≢0 = refl
DivMod+-left-identity (suc b) (suc n) ≢0 = {!   !}

divMod-hom : (b m n : ℕ) → (≢0 : False (b ≟ 0)) → ((m + n) divMod b) {≢0} ≡ ((m divMod b) {≢0}) DivMod+ ((n divMod b) {≢0})
divMod-hom zero    m n ()
divMod-hom (suc b) zero n ≢0 = {!   !}
divMod-hom (suc b) (suc m) n ≢0  = {!   !}

div-suc-mono : (n base : ℕ)  → (≢0 : False (base ≟ 0))
             → let _/base = λ x → (x div base) {≢0}
               in suc n /base ≥ n /base
div-suc-mono n       zero    ()
div-suc-mono zero    (suc b) ≢0 = z≤n
div-suc-mono (suc n) (suc b) ≢0 = {!   !}

-}

--  TODO: proof div monotone
postulate
    div-mono : (base : ℕ) → (≢0 : False (base ≟ 0))
             → let _/base = λ x → (x div base) {≢0}
               in  _/base Preserves _≤_ ⟶ _≤_
{-
n/n≡1 : ∀ n → (≢0 : False (n ≟ 0)) → (n div n) {≢0} ≡ 1
n/n≡1 zero ()
n/n≡1 (suc n) ≢0 with ((suc n) divMod (suc n)) {≢0} | inspect (λ w → ((suc n) divMod (suc n)) {w}) ≢0
n/n≡1 (suc n) ≢0 | result zero r prop | PropEq.[ eq ] =
    let prop' : suc n ≡ toℕ r
        prop' = trans prop (+-right-identity (toℕ r))
    in  contradiction (≤-refl prop') (>⇒≰ (bounded r))
n/n≡1 (suc n) ≢0 | result (suc zero) r prop | PropEq.[ eq ] = {!   !}
n/n≡1 (suc n) ≢0 | result (suc (suc q)) r prop | PropEq.[ eq ] =
    let prop' : suc n ≡ suc n + toℕ r + suc q * suc n
        prop' = beginEq
                suc n
            ≡Eq⟨ prop ⟩
                toℕ r + (suc n + suc (n + q * suc n))
            ≡Eq⟨ sym (+-assoc (toℕ r) (suc n) (suc (n + q * suc n))) ⟩
                toℕ r + suc n + suc (n + q * suc n)
            ≡Eq⟨ cong₂ _+_ (+-comm (toℕ r) (suc n)) refl ⟩
                suc (n + toℕ r + suc (n + q * suc n))
            ∎Eq
    in  contradiction (≤-refl prop') (>⇒≰ {!   !})

lem : ∀ m n → n ≤ m → (≢0 : False (n ≟ 0)) → (n div n) {≢0} ≤ (m div n) {≢0}
lem m zero n≤m ()
lem m (suc n) n≤m ≢0 = div-mono (suc n) {!   !} n≤m
-}
{-
div-mono : (base : ℕ) → (≢0 : False (base ≟ 0))
         → let _/base = λ x → (x div base) {≢0}
           in  _/base Preserves _≤_ ⟶ _≤_
div-mono zero () rel
div-mono (suc b) ≢0 z≤n = z≤n
div-mono (suc b) ≢0 (s≤s {x} {y} rel) with compare x y
div-mono (suc b) ≢0 (s≤s rel) | less m k with ((suc m) divMod (suc b)) {≢0}
                                            | inspect (λ w → ((suc m) divMod (suc b)) {w}) ≢0
                                            | ((suc (suc m + k)) divMod (suc b)) {≢0}
                                            | inspect (λ w → ((suc (suc m + k)) divMod (suc b)) {w}) ≢0
                                            | ((suc k) divMod (suc b)) {≢0}
                                            | inspect (λ w → ((suc k) divMod (suc b)) {w}) ≢0
div-mono (suc b) ≢0 (s≤s rel) | less m k | result q₀ r₀ prop₀ | PropEq.[ eq₀ ] | result q₁ r₁ prop₁ | PropEq.[ eq₁ ] | result q₂ r₂ prop₂ | PropEq.[ eq₂ ] =
    -- prop₀:      suc m      ≡ toℕ r₀ + qₒ * suc b
    -- prop₁: suc (suc m + k) ≡ toℕ r₁ + q₁ * suc b
    -- prop₂: suc          k  ≡ toℕ r₂ + q₂ * suc b
    begin
        q₀
    ≤⟨ {!   !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        q₁
    ∎
div-mono (suc b) ≢0 (s≤s rel) | equal m = ≤-refl refl
div-mono (suc b) ≢0 (s≤s rel) | greater m k = contradiction rel (>⇒≰ (s≤s (m≤m+n m k)))

div-mono (suc b) ≢0 (s≤s {x} {y} rel)   with (x divMod (suc b)) {≢0}
                                        | inspect (λ w → (x divMod (suc b)) {w}) ≢0
                                        | (y divMod (suc b)) {≢0}
                                        | inspect (λ w → (y divMod (suc b)) {w}) ≢0
div-mono (suc b) ≢0 (s≤s {x} {y} rel)   | result qx rx propx | PropEq.[ eqx ] | result qy ry propy | PropEq.[ eqy ] with  = {!   !}

    begin
        {!   !}
    <⟨ {!   !} ⟩
        {!   !}
    <⟨ {!   !} ⟩
        {!   !}
    ∎

    begin
        {!   !}
    ≤⟨ {!    !} ⟩
        {!    !}
    ≤⟨ {!    !} ⟩
        {!   !}
    ≤⟨ {!    !} ⟩
        {!   !}
    ≤⟨ {!    !} ⟩
        {!   !}
    ∎
    beginEq
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ≡Eq⟨ {!   !} ⟩
        {!   !}
    ∎Eq
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Relation.Binary.Core

module Heapsort.Impl2.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_ hiding (forget) renaming (flatten to flatten')
open import BBHeap.Compound _≤_
open import BBHeap.Drop _≤_ tot≤ trans≤
open import BBHeap.Drop.Properties _≤_ tot≤ trans≤
open import BBHeap.Heapify _≤_ tot≤ trans≤
open import BBHeap.Insert _≤_ tot≤ trans≤
open import BBHeap.Insert.Properties _≤_ tot≤ trans≤
open import BBHeap.Order _≤_
open import BBHeap.Order.Properties _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Heapsort.Impl2 _≤_ tot≤ trans≤
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import OList _≤_
open import Order.Total _≤_ tot≤

lemma-flatten-flatten' : {b : Bound}(h : BBHeap b)(accₕ : Acc h) → forget (flatten h accₕ) ∼ flatten' h
lemma-flatten-flatten' leaf _ = ∼[]
lemma-flatten-flatten' (left {l = l} {r = r} b≤x l⋘r) (acc rs) = ∼x /head /head (trans∼ (lemma-flatten-flatten' (drop⋘ b≤x l⋘r) (rs (drop⋘ b≤x l⋘r) (lemma-drop≤′ (cl b≤x l⋘r)))) (lemma-drop⋘∼ b≤x l⋘r))
lemma-flatten-flatten' (right {l = l} {r = r} b≤x l⋙r) (acc rs) = ∼x /head /head (trans∼ (lemma-flatten-flatten' (drop⋙ b≤x l⋙r) (rs (drop⋙ b≤x l⋙r) (lemma-drop≤′ (cr b≤x l⋙r)))) (lemma-drop⋙∼ b≤x l⋙r))

lemma-flatten'-flatten : {b : Bound}(h : BBHeap b)(accₕ : Acc h) → (flatten' h) ∼ (forget (flatten h accₕ))
lemma-flatten'-flatten h tₕ = sym∼ (lemma-flatten-flatten' h tₕ)

theorem-heapsort∼ : (xs : List A) → xs ∼ forget (heapsort xs)
theorem-heapsort∼ [] = ∼[]
theorem-heapsort∼ (x ∷ xs) =
                     let h = heapify xs ;
                          accₕ = ≺-wf h ;
                          hᵢ = insert lebx h ;
                          accₕᵢ = ≺-wf hᵢ ;
                          xs∼fh = theorem-heapsort∼ xs ;
                          fh∼f'h = lemma-flatten-flatten' h accₕ ;
                          xs∼f'h = trans∼ xs∼fh fh∼f'h ;
                          xxs∼xf'h = ∼x /head /head xs∼f'h ;
                          xf'h∼f'hᵢ = lemma-insert∼ lebx h ;
                          xxs∼f'hᵢ = trans∼ xxs∼xf'h xf'h∼f'hᵢ ;
                          f'hᵢ∼fhᵢ = lemma-flatten'-flatten hᵢ accₕᵢ
                      in trans∼ xxs∼f'hᵢ f'hᵢ∼fhᵢ

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Rec2 where

  open import Data.Nat
  open import Rec1

  x : ℕ
  x = 42

  z : ℕ
  z = y


text:
-- Following A CUBICAL TYPE THEORY FOR HIGHER INDUCTIVE TYPES
-- by Simon Huber at https://simhu.github.io/misc/hcomp.pdf
-- as closely as possible.

open import Cubical.Core.Primitives
open import Cubical.Core.Glue
import Agda.Builtin.Cubical.HCompU as HCompU
open HCompU using (primFaceForall)
open HCompU.Helpers using (refl)

private
  variable
    ℓ ℓ₁ : Level
    ℓ′ ℓ₁′ : I → Level

-- Section 2 : New Primitives

-- This is just a special case of transp where φ = i0. I include it as it
-- has a far simpler type.
transport : (A : ∀ i → Type (ℓ′ i)) → A i0 → A i1
transport A u₀ = transp A i0 u₀

transp' :
  (φ : I)
  {ℓ' : I → Level [ φ ↦ (λ _ → ℓ) ]}
  {a : PartialP φ (λ _ → Type ℓ)}
  (A : (i : I) → Type (outS (ℓ' i)) [ φ ↦ (λ { (φ = i1) → a 1=1 }) ])
  (u₀ : outS (A i0))
  → outS (A i1) [ φ ↦ (λ { (φ = i1) → u₀ }) ]
transp' φ A u₀ = inS (transp (λ i → outS (A i)) φ u₀)

transportFill :
  (A : ∀ i → Type (ℓ′ i))
  (u₀ : A i0)
  (i : I)
  → A i
transportFill A u₀ i = transp (λ j → A (i ∧ j)) (~ i) u₀

-- Note that I fix the universe of A to make the type simpler. From now on we
-- are going to do that for all code involving transp where φ is not just i0.
transpFill :
  (φ : I)
  {a : Partial φ (Type ℓ)}
  (A : I → Type ℓ [ φ ↦ a ])
  (u₀ : outS (A i0))
  (i : I)
  → outS (A i)
transpFill φ A u₀ i = transp (λ j → outS (A (i ∧ j))) (φ ∨ ~ i) u₀

forward :
  (A : ∀ i → Type (ℓ′ i))
  (r : I)
  (u : A r)
  → A i1
forward A r u = transp (λ i → A (i ∨ r)) r u

hcomp' :
  {A : Type ℓ}
  {φ : I}
  (u : ∀ i → Partial φ A)
  (u₀ : A [ φ ↦ u i0 ])
  → A [ φ ↦ u i1 ]
hcomp' u u₀ = inS (hcomp u (outS u₀))

module Comp
  (A : ∀ i → Type (ℓ′ i))
  {φ : I}
  (u : ∀ i → Partial φ (A i))
  (u₀ : A i0 [ φ ↦ u i0 ])
  where
  comp' : A i1 [ φ ↦ u i1 ]
  comp' =
    inS
      (hcomp
        (λ i o → forward A i (u i o))
        (forward A i0 (outS u₀)))

  compId : comp A {φ = φ} u (outS u₀) ≡ outS comp'
  compId = refl

-- Section 3 : Recursive definition of transport

data ℕ : Type where
  zero : ℕ
  suc : ℕ → ℕ

transpZeroId : (φ : I) → transp (λ _ → ℕ) φ zero ≡ zero
transpZeroId φ = refl

transpSucId : (φ : I) (u₀ : ℕ)
  → transp (λ _ → ℕ) φ (suc u₀) ≡ suc (transp (λ _ → ℕ) φ u₀)
transpSucId φ u₀ = refl

transpℕId : (φ : I) (u₀ : ℕ) → transp (λ _ → ℕ) φ u₀ ≡ u₀
transpℕId φ u₀ = refl

transportPathPId :
  (A : (i j : I) → Type (ℓ′ i))
  (v : (i : I) → A i i0)
  (w : (i : I) → A i i1)
  (u₀ : PathP (A i0) (v i0) (w i0))
  → transport (λ i → PathP (A i) (v i) (w i)) u₀
    ≡ λ j → comp
        (λ i → A i j)
        (λ i → λ
          { (j = i0) → v i
          ; (j = i1) → w i })
        (u₀ j)
transportPathPId A v w u₀ = refl

transpPathPId :
  (φ : I)
  {a : I → Partial φ (Type ℓ)}
  (A : (i j : I) → Type ℓ [ φ ↦ a j ])
  {vφ : PartialP φ (a i0)}
  (v : (i : I) → outS (A i i0) [ φ ↦ (λ { (φ = i1) → vφ 1=1 }) ])
  {wφ : PartialP φ (a i1)}
  (w : (i : I) → outS (A i i1) [ φ ↦ (λ { (φ = i1) → wφ 1=1 }) ])
  (u₀ : PathP (λ j → outS (A i0 j)) (outS (v i0)) (outS (w i0)))
  → transp (λ i → PathP (λ j → outS (A i j)) (outS (v i)) (outS (w i))) φ u₀
    ≡ λ j → comp
        (λ i → outS (A i j))
        (λ i → λ
          { (φ = i1) → u₀ j
          ; (j = i0) → outS (v i)
          ; (j = i1) → outS (w i) })
        (u₀ j)
transpPathPId φ A v w u₀ = refl

transportΣId :
  (A : ∀ i → Type (ℓ′ i))
  (B : ∀ i → A i → Type (ℓ₁′ i))
  (u₀ : Σ (A i0) (B i0))
  → transport (λ i → Σ (A i) (B i)) u₀
    ≡ (transport A (u₀ .fst) ,
      let v = transportFill A (u₀ .fst)
      in transport (λ i → B i (v i)) (u₀ .snd))
transportΣId A B u₀ = refl

transpΣId :
  (φ : I)
  {a : Partial φ (Type ℓ)}
  (A : I → Type ℓ [ φ ↦ a ])
  {b : Partial φ (Type ℓ₁)}
  (B : (i : I) → outS (A i) → Type ℓ₁ [ φ ↦ b ])
  (u₀ : Σ (outS (A i0)) (λ x → outS (B i0 x)))
  → transp (λ i → Σ (outS (A i)) (λ x → outS (B i x))) φ u₀
    ≡ (transp (λ i → outS (A i)) φ (u₀ .fst) ,
      let v = transpFill φ A (u₀ .fst)
      in transp (λ i → outS (B i (v i))) φ (u₀ .snd))
transpΣId φ A B u₀ = refl

transportΠId :
  (A : ∀ i → Type (ℓ′ i))
  (B : ∀ i → A i → Type (ℓ₁′ i))
  (u₀ : (x : A i0) → B i0 x)
  → transport (λ i → (x : A i) → B i x) u₀
    ≡ λ v →
      let
      w : (i : I) → A i
      w i = transportFill (λ j → A (~ j)) v (~ i)
      in
      transport (λ i → B i (w i)) (u₀ (w i0))
transportΠId A B u₀ = refl

transpΠId :
  (φ : I)
  {a : Partial φ (Type ℓ)}
  (A : I → Type ℓ [ φ ↦ a ])
  {b : Partial φ (Type ℓ₁)}
  (B : (i : I) → outS (A i) → Type ℓ₁ [ φ ↦ b ])
  (u₀ : ((x : outS (A i0))  → outS (B i0 x)))
  → transp (λ i → (x : outS (A i)) → outS (B i x)) φ u₀
    ≡ λ v →
      let
      w : (i : I) → outS (A i)
      w i = transpFill φ (λ j → (A (~ j))) v (~ i)
      in
      transp (λ i → outS (B i (w i))) φ (u₀ (w i0))
transpΠId φ A B u₀ = refl

transpUniverseId : (φ : I) (A : Type ℓ) → transp (λ _ → Type ℓ) φ A ≡ A
transpUniverseId φ A = refl

module TransportGlue
  (A : ∀ i → Type (ℓ′ i))
  (φ : I → I)
  (T : (i : I) → Partial (φ i) (Type (ℓ₁′ i)))
  (w : (i : I) → PartialP (φ i) (λ o → T i o ≃ A i))
  (u₀ : primGlue (A i0) (T i0) (w i0))
  where
  B : (i : I) → Type (ℓ₁′ i)
  B i = primGlue (A i) (T i) (w i)

  ∀φ : I
  ∀φ = primFaceForall φ

  t : (i : I) → PartialP ∀φ (λ { (∀φ = i1) → T i 1=1 })
  t i (∀φ = i1) = {!!}

  transportGlue : B i1
  transportGlue = {!!}

  transportGlueId : transport B u₀ ≡ transportGlue
  transportGlueId = {!!}

-- Section 4 : Recursive Definition of Homogeneous Composition

hcompZeroId : {φ : I} → hcomp (λ i → λ { (φ = i1) → zero }) zero ≡ zero
hcompZeroId = refl

hcompSucId :
  {φ : I}
  (u : I → Partial φ ℕ)
  (u₀ : ℕ [ φ ↦ u i0 ])
  → hcomp (λ i o → suc (u i o)) (suc (outS u₀)) ≡ suc (hcomp u (outS u₀))
hcompSucId u u₀ = refl

hcompPathPId :
  (A : I → Type ℓ)
  (v : A i0)
  (w : A i1)
  {φ : I}
  (u : I → Partial φ (PathP A v w))
  (u₀ : PathP A v w [ φ ↦ u i0 ])
  → hcomp u (outS u₀)
  ≡ λ j →
    hcomp
      (λ i → λ { (φ = i1) → u i 1=1 j ; (j = i0) → v ; (j = i1) → w })
      (outS u₀ j)
hcompPathPId A v w u u₀ = refl

hcompΣId :
  (A : Type ℓ)
  (B : (x : A) → Type ℓ₁)
  {φ : I}
  (u : I → Partial φ (Σ A B))
  (u₀ : Σ A B [ φ ↦ u i0 ])
  → hcomp u (outS u₀)
  ≡ let
    v : (i : I) → A
    -- should use hfill instead
    v = fill (λ _ → A) (λ i o → u i o .fst) (inS (outS u₀ .fst))
    in
    (v i1 ,
    comp (λ i → B (v i)) (λ i → λ { (φ = i1) → u i 1=1 .snd }) (outS u₀ .snd))
hcompΣId A B u u₀ = refl

hcompΠId :
  (A : Type ℓ)
  (B : (x : A) → Type ℓ₁)
  {φ : I}
  (u : I → Partial φ ((x : A) →  B x))
  (u₀ : ((x : A) →  B x) [ φ ↦ u i0 ])
  → hcomp u (outS u₀)
  ≡ λ v → hcomp (λ i o → u i o v) (outS u₀ v)
hcompΠId A B u u₀ = refl

-- Unfortunately  hcomp E (outS A) is not judgmentally equal to
-- outS (hcompUniverse E A) which I don't know why.
hcompUniverse :
  {φ : I}
  (E : I → Partial φ (Type ℓ))
  (A : Type ℓ [ φ ↦ E i0 ])
  → Type ℓ [ φ ↦ E i1 ]
hcompUniverse {φ = φ} E A =
  inS
    (primGlue
      (outS A)
      (E i1)
      (λ { (φ = i1) → lineToEquiv (λ i → E (~ i) 1=1) }))

module HcompGlue
  (A : Type ℓ)
  {φ : I}
  (T : Partial φ (Type ℓ₁))
  (w : PartialP φ (λ o → T o ≃ A))
  {ψ : I}
  (u : I → Partial ψ (primGlue A T w))
  (u₀ : primGlue A T w [ ψ ↦ u i0 ])
  where
  t : (i : I) → PartialP φ T
  t i (φ = i1) = hfill u u₀ i

  a₁ : A
  a₁ = hcomp (λ i → λ
    { (ψ = i1) → unglue φ (u i 1=1)
    ; (φ = i1) → w 1=1 .fst (t i 1=1) })
    (unglue φ (outS u₀))

  hcompGlue : primGlue A T w [ ψ ↦ u i1 ]
  hcompGlue = inS (glue (t i1) a₁)

  hcompGlueId : hcomp u (outS u₀) ≡ outS hcompGlue
  hcompGlueId = refl

max_stars_repo_name: howsiyu/hott-notes

max_issues_repo_name: howsiyu/hott-notes

max_forks_repo_name: howsiyu/hott-notes


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base

module HoTT.Identity where

open variables
private variable x y z w : A

-- Lemma 2.1.4
--  (i)
unitᵣ : {p : x == y} → p == p ∙ refl
unitᵣ {p = refl} = refl

unitₗ : {p : x == y} → p == refl ∙ p
unitₗ {p = refl} = refl

--  (ii)
invₗ : {p : x == y} → p ⁻¹ ∙ p == refl
invₗ {p = refl} = refl

invᵣ : {p : x == y} → p ∙ p ⁻¹ == refl
invᵣ {p = refl} = refl

--  (iv)
assoc : {p : x == y} {q : y == z} {r : z == w} →
        p ∙ (q ∙ r) == (p ∙ q) ∙ r
assoc {p = refl} {refl} {refl} = refl

invinv : {p : x == y} → p ⁻¹ ⁻¹ == p
invinv {p = refl} = refl

-- Whiskering
_∙ᵣ_ : {p q : x == y} (α : p == q) (r : y == z) → p ∙ r == q ∙ r
refl ∙ᵣ refl = refl
infixl 25 _∙ᵣ_

_∙ₗ_ : {r s : y == z} (q : x == y) (β : r == s) → q ∙ r == q ∙ s
refl ∙ₗ refl = refl
infixl 25 _∙ₗ_

-- Horizontal composition
_⋆_ : {p q : x == y} {r s : y == z} → (p == q) → (r == s) → p ∙ r == q ∙ s
refl ⋆ refl = refl

cancelᵣ : {p q : x == y} {r : y == z} (α : p ∙ r == q ∙ r) → p == q
cancelᵣ {r = refl} α = unitᵣ ∙ α ∙ unitᵣ ⁻¹

cancelₗ : {r s : y == z} {q : x == y} (β : q ∙ r == q ∙ s) → r == s
cancelₗ {q = refl} β = unitₗ ∙ β ∙ unitₗ ⁻¹

pivotᵣ : {p : x == y} {q : y == z} {r : x == z} → p ∙ q == r → p == r ∙ q ⁻¹
pivotᵣ {p = refl} {q = refl} α = α ∙ unitᵣ

pivotₗ : {p : x == y} {q : y == z} {r : x == z} → p ∙ q == r → q == p ⁻¹ ∙ r
pivotₗ {p = refl} {q = refl} α = α ∙ unitₗ

-- Lemma 2.2.2
--  (i)
ap-∙ : (f : A → B) (p : x == y) (q : y == z) → ap f (p ∙ q) == ap f p ∙ ap f q
ap-∙ _ refl refl = refl

--  (ii)
ap-inv : (f : A → B) (p : x == y) → ap f (p ⁻¹) == ap f p ⁻¹
ap-inv _ refl = refl

--  (iii)
ap-∘ : {C : 𝒰 i} (f : B → C) (g : A → B) (p : x == y) → ap (f ∘ g) p == ap f (ap g p)
ap-∘ _ _ refl = refl

--  (iv)
ap-id : (p : x == y) → ap id p == p
ap-id refl = refl

ap-const : (p : x == y) → ap (const B) p == refl
ap-const refl = refl

-- Lemma 2.3.5
transportconst : (p : x == y) → transport (const B) p ~ id
transportconst refl _ = refl

-- Lemma 2.3.9
transport-∙ : (P : A → 𝒰 i) (p : x == y) (q : y == z) →
              transport P (p ∙ q) ~ transport P q ∘ transport P p
transport-∙ P refl refl _ = refl

-- Lemma 2.3.10
transport-ap : (P : B → 𝒰 i) (f : A → B) {x y : A} (p : x == y) →
               transport P (ap f p) ~ transport (P ∘ f) p
transport-ap _ _ refl _ = refl

-- Lemma 2.3.11
transport-∘ : (f : {x : A} → P x → Q x) (p : x == y) →
              transport Q p ∘ f ~ f ∘ transport P p
transport-∘ _ refl _ = refl

module =-Reasoning {i} {A : 𝒰 i}
  where
  _=⟨_⟩_ : (x : A) {y z : A} → x == y → y == z → x == z
  x =⟨ p ⟩ q = p ∙ q
  infixr 2 _=⟨_⟩_

  _=⟨⟩_ : (x : A) {y : A} → x == y → x == y
  _ =⟨⟩ p = p
  infixr 2 _=⟨⟩_

  _∎ : (x : A) → x == x
  _ ∎ = refl
  infix 3 _∎

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott