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 ∣₁))