Not so secret

Agda-report.agda

module PSet3 where

record TermStructure : Set₁ where
  field
    Term : Set

module QPER (TS TS' : TermStructure) where
  open TermStructure TS
  open TermStructure TS'
    renaming (Term to Term')

  record QPER : Set₁ where
    field
      R : (M : Term) (M' : Term') → Set
      zzc : {M N : Term} {M' N' : Term'} → R M M' → R N N' → R N M' → R M N'
  open QPER public

  variable
    X Y : QPER

  record QPERClosedTerm (Y : QPER) : Set where
    field
      M : Term
      M' : Term'
      law : R Y M M'

  _~_ : (tM tN : QPERClosedTerm Y) → Set
  _~_ {Y} tM tN = R Y (QPERClosedTerm.M tN) (QPERClosedTerm.M' tM)

  ~-trans : (Y : QPER) (tM tN tP : QPERClosedTerm Y) → (tM ~ tN) → (tN ~ tP) → (tM ~ tP)
  ~-trans Y tM tN tP h h' = {!   !}