Classical logic encoded as a fragment in Cubical Agda
Classical propositional calculus is encoded within (regular) Agda in Logic/Classical/Base.agda and then extended into variant equivalent operators in Logic/Classical/Properties.agda. Axioms from Mathematical Logic: A First Course, by JW Robbin are proven, showing that the encoded fragment is indeed classical logic. Robbin's inductive decidable semantics are also encoded. Cubical compatibility is maintained throughout the propositional calculus fragment.
The encoding involves wrapping terms and operators in double-negatives, which ensure that classical terms are propositions in the sense of being isProp. This is given the alias ISTRUE so that "ISTRUE A" means "A is classically true". A classical excluded middle follows for this fragment, essentially the Godel fragment. Logic/LawOfTheExcludedMiddle.agda also presents the definition of the law of the excluded middle in terms that can be used either axiomatically or as an argument to a function. But the preferred approach here is to do no such thing and rely on the encoding, called here "Classical In Constructive" logic. Issues pertaining to decidability are discussed in the comments. Since the ISTRUE wrapper ensures the property that everything in sight is isProp, this means that bijections entail isomorphisms. When the levels are the same, such isomorphisms entail Cubical equality via the library function isoToPath. This means we can be more systematic about making substitutions between equivalent terms and operators as in 'paper' classical logic, meaning the classical operators defined in (regular) Agda can be substituted for equivalent terms and operators via the Cubical machinery. Since we are mixing (regular) and Cubical Agda, Conversions.agda provides some support code for mixing the two variants of Agda.
This use of Cubical Agda is essential in Logic/Classical/Predicates.agda where the program is, in very short order, extended to classical predicate caluclus. This simply involves using the builtin constructive ∀ and the classical ∃ A B = ISTRUE (Σ A B). It turns out nicely that (¬ ∀ ¬) is cubically equal to ∃, and that the constructive definition of ∀ is also the classical definition - providing we wrap all terms in sight in the 'outer classical' ISTRUE wrapper. 'Outer classical' simply refers to the fact that within such a wrapped term there may be constructive components not so wrapped. The classical predicate calculus can therefore be used as a generalisation of 'paper' classical logic per se. Indeed, constructive logic is simply a generalisation, an extension, of classical logic.
Here is the definition of Outer Classical (using cubical equality):
data OuterClassical (A : Set ℓ) : Set (ℓ-suc ℓ) where
invariant : ((ISTRUE A) ≡ A) -> OuterClassical A
A few necessary axioms from S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951) are proven in Logic/Classical/Axiomatisation.agda to show that we have indeed coded a classical predicate calculus inside the constructive logic of Cubical Agda. It is kept as minimal as possible, meaning that it is not necessary to show the propositional calculus axioms again, nor any extensions which pertain more to how the type theory is used, as in Kleene's number theory axioms - this all devolves to type theory, and is not the topic of this work.
A classical equality is given as the wrapped ISTRUE (A ≡ B). Types of course have replaced sets, though we could use the machinery of sigma types to emulate the logic of set theory, albeit with provisos not explored here. It turns out (Logic/Classical/Predicates.agda) that the full function extensionality of classical mathematics does not follow from the constructive function extensionality given by Cubical Agda. Whilst this is interesting, it isn't classical logic as such that is the cause. It is due to the fact that Cubical Agda's function extensionality is natively constructive, not because its logic is. We can have classical logic inside a constructive type theory without adding new axioms, and with the Cubical machinery quite conveniently so in terms of making substitutions, but not necessarily classical function extensionality, at least not in important cases like when the codomain of the functions involved are constructive reals. This is because there is no decidable equality in such cases. Classical mathematics seems to add some extra axiom here, perhaps even by way of confusion. Analogously, something similar will also be the case for bisimilarity of infinite streams. This gives us some insight into constructive mathematics, in particular when dealing with reals, and, most interestingly, the relationship between classical and constructive mathematics: the difference does not really lie in the logic; constructive logic is but a generalisation and extension of classical logic!