The intuitionistic negation example is so mind blowing. I can only wrap my head around it when I think about it in terms of functions and types:

    not : Type -> Type
    not P = P -> ⊥
    
    modus-ponens : P -> ((f : P -> Q) -> Q)
    modus-ponens p = λf. f p
    
    -- p implies not-not-p
    not-not : P -> ((f : P -> ⊥) -> ⊥)
    not-not p = λf. f p
    
    -- not-p implies not-not-not-p
    not-not-not : (P -> ⊥) -> (((P -> ⊥) -> ⊥) -> ⊥)
    not-not-not np = λf. f np

    -- not-not-not-p implies not-p
    not-p : (((P -> ⊥) -> ⊥) -> ⊥) -> (P -> ⊥)
    not-p nnnp = λp. nnnp (not-not p)

Now it all just turns into function application :)