open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Data.Unit
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Sum renaming (rec to sumRec)
open import Cubical.Data.Empty renaming (rec* to ⊥*rec)
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.Relation.Binary.Order.Preorder
open import Realizability.CombinatoryAlgebra
open import Realizability.ApplicativeStructure

module Realizability.Tripos.Prealgebra.Joins.Base {ℓ ℓ' ℓ''} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
open import Realizability.Tripos.Prealgebra.Predicate {ℓ' = ℓ'} {ℓ'' = ℓ''} ca
open import Realizability.Tripos.Prealgebra.Joins.Commutativity ca
open CombinatoryAlgebra ca
open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)

module _ (X : Type ℓ') (isSetX' : isSet X) (isNonTrivial : s ≡ k → ⊥) where
  PredicateX = Predicate X
  open Predicate
  open PredicateProperties X
  antiSym→x⊔z≤y⊔z' : ∀ x y z → x ≤ y → y ≤ x → (x ⊔ z) ≤ (y ⊔ z)
  antiSym→x⊔z≤y⊔z' x y z x≤y y≤x =
    do
      (x⊨y , x⊨yProves) ← x≤y
      let prover = ` Id ̇ (` pr₁ ̇ (# zero)) ̇ (` pair ̇ ` k ̇ (` x⊨y ̇ (` pr₂ ̇ (# zero)))) ̇ (` pair ̇ ` k' ̇ (` pr₂ ̇ (# zero)))
      return
        (λ* prover ,
          λ x' a a⊩x⊔zx' →
            equivFun
              (propTruncIdempotent≃
                ((y ⊔ z) .isPropValued x' (λ* prover ⨾ a)))
                (do
                  a⊩x⊔z ← a⊩x⊔zx'
                  return
                    ∣ sumRec
                      (λ { (pr₁⨾a≡k , pr₂⨾a⊩xx') →
                        inl
                          (((pr₁ ⨾ (λ* prover ⨾ a))
                             ≡⟨ cong (λ x → pr₁ ⨾ x) (λ*ComputationRule prover a) ⟩
                            (pr₁ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
                             ≡⟨ cong (λ x → (pr₁ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k ⟩
                            (pr₁ ⨾ (Id ⨾ k ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
                             ≡⟨ cong (λ x → pr₁ ⨾ x) (ifTrueThen _ _) ⟩
                            (pr₁ ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))))
                             ≡⟨ pr₁pxy≡x _ _ ⟩
                            (k)
                             ∎) ,
                             subst
                               (λ r → r ⊩ ∣ y ∣ x')
                               (sym
                                 (pr₂ ⨾ (λ* prover ⨾ a)
                                   ≡⟨ cong (λ x → pr₂ ⨾ x) (λ*ComputationRule prover a) ⟩
                                  pr₂ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
                                   ≡⟨ cong (λ x → (pr₂ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k ⟩
                                  pr₂ ⨾ (Id ⨾ k ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
                                   ≡⟨ cong (λ x → pr₂ ⨾ x) (ifTrueThen _ _) ⟩
                                  pr₂ ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a)))
                                   ≡⟨ pr₂pxy≡y _ _ ⟩
                                  x⊨y ⨾ (pr₂ ⨾ a)
                                   ∎))
                               (x⊨yProves x' (pr₂ ⨾ a) pr₂⨾a⊩xx')) })
                      (λ { (pr₁⨾a≡k' , pr₂a⊩zx') →
                        inr
                         ((((pr₁ ⨾ (λ* prover ⨾ a))
                             ≡⟨ cong (λ x → pr₁ ⨾ x) (λ*ComputationRule prover a) ⟩
                            (pr₁ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
                             ≡⟨ cong (λ x → (pr₁ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k' ⟩
                            (pr₁ ⨾ (Id ⨾ k' ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))
                             ≡⟨ cong (λ x → pr₁ ⨾ x) (ifFalseElse _ _) ⟩
                            (pr₁ ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
                             ≡⟨ pr₁pxy≡x _ _ ⟩
                            (k')
                             ∎)) ,
                               subst
                                 (λ r → r ⊩ ∣ z ∣ x')
                                 (sym
                                  ((pr₂ ⨾ (λ* prover ⨾ a)
                                   ≡⟨ cong (λ x → pr₂ ⨾ x) (λ*ComputationRule prover a) ⟩
                                  pr₂ ⨾ (Id ⨾ (pr₁ ⨾ a) ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
                                   ≡⟨ cong (λ x → (pr₂ ⨾ (Id ⨾ x ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))))) pr₁⨾a≡k' ⟩
                                  pr₂ ⨾ (Id ⨾ k' ⨾ (pair ⨾ k ⨾ (x⊨y ⨾ (pr₂ ⨾ a))) ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a)))
                                   ≡⟨ cong (λ x → pr₂ ⨾ x) (ifFalseElse _ _) ⟩
                                  pr₂ ⨾ (pair ⨾ k' ⨾ (pr₂ ⨾ a))
                                   ≡⟨ pr₂pxy≡y _ _ ⟩
                                  pr₂ ⨾ a
                                    ∎)))
                                 pr₂a⊩zx') })
                      a⊩x⊔z ∣₁))