text:
module n2o.Network.Socket where

open import proto.IO
open import proto.Base

data SocketType : Set where
    NoSocketType : SocketType
    Stream     : SocketType
    Datagram   : SocketType
    Raw        : SocketType
    RDM        : SocketType
    SeqPacket  : SocketType

{-# COMPILE GHC SocketType = data Network.Socket.SocketType
                           ( NoSocketType
                           | Stream
                           | Datagram
                           | Raw
                           | RDM
                           | SeqPacket ) #-}

data SockFamily : Set where
    AF_UNSPEC           : SockFamily
    AF_UNIX             : SockFamily
    AF_INET             : SockFamily
    AF_INET6            : SockFamily
    AF_IMPLINK          : SockFamily
    AF_PUP              : SockFamily
    AF_CHAOS            : SockFamily
    AF_NS               : SockFamily
    AF_NBS              : SockFamily
    AF_ECMA             : SockFamily
    AF_DATAKIT          : SockFamily
    AF_CCITT            : SockFamily
    AF_SNA              : SockFamily
    AF_DECnet           : SockFamily
    AF_DLI              : SockFamily
    AF_LAT              : SockFamily
    AF_HYLINK           : SockFamily
    AF_APPLETALK        : SockFamily
    AF_ROUTE            : SockFamily
    AF_NETBIOS          : SockFamily
    AF_NIT              : SockFamily
    AF_EIE              : SockFamily
    AF_ISO              : SockFamily
    AF_OSI              : SockFamily
    AF_NETMAN           : SockFamily
    AF_X25              : SockFamily
    AF_AX25             : SockFamily
    AF_OSINET           : SockFamily
    AF_GOSSIP           : SockFamily
    AF_IPX              : SockFamily
    Pseudo_AF_XTP       : SockFamily
    AF_CTF              : SockFamily
    AF_WAN              : SockFamily
    AF_SDL              : SockFamily
    AF_NETWARE          : SockFamily
    AF_NDD              : SockFamily
    AF_INTF             : SockFamily
    AF_COIP             : SockFamily
    AF_CNT              : SockFamily
    Pseudo_AF_RTIP      : SockFamily
    Pseudo_AF_PIP       : SockFamily
    AF_SIP              : SockFamily
    AF_ISDN             : SockFamily
    Pseudo_AF_KEY       : SockFamily
    AF_NATM             : SockFamily
    AF_ARP              : SockFamily
    Pseudo_AF_HDRCMPLT  : SockFamily
    AF_ENCAP            : SockFamily
    AF_LINK             : SockFamily
    AF_RAW              : SockFamily
    AF_RIF              : SockFamily
    AF_NETROM           : SockFamily
    AF_BRIDGE           : SockFamily
    AF_ATMPVC           : SockFamily
    AF_ROSE             : SockFamily
    AF_NETBEUI          : SockFamily
    AF_SECURITY         : SockFamily
    AF_PACKET           : SockFamily
    AF_ASH              : SockFamily
    AF_ECONET           : SockFamily
    AF_ATMSVC           : SockFamily
    AF_IRDA             : SockFamily
    AF_PPPOX            : SockFamily
    AF_WANPIPE          : SockFamily
    AF_BLUETOOTH        : SockFamily
    AF_CAN              : SockFamily

{-# COMPILE GHC SockFamily = data Network.Socket.Family
                             ( AF_UNSPEC
                             | AF_UNIX
                             | AF_INET
                             | AF_INET6
                             | AF_IMPLINK
                             | AF_PUP
                             | AF_CHAOS
                             | AF_NS
                             | AF_NBS
                             | AF_ECMA
                             | AF_DATAKIT
                             | AF_CCITT
                             | AF_SNA
                             | AF_DECnet
                             | AF_DLI
                             | AF_LAT
                             | AF_HYLINK
                             | AF_APPLETALK
                             | AF_ROUTE
                             | AF_NETBIOS
                             | AF_NIT
                             | AF_802
                             | AF_ISO
                             | AF_OSI
                             | AF_NETMAN
                             | AF_X25
                             | AF_AX25
                             | AF_OSINET
                             | AF_GOSSIP
                             | AF_IPX
                             | Pseudo_AF_XTP
                             | AF_CTF
                             | AF_WAN
                             | AF_SDL
                             | AF_NETWARE
                             | AF_NDD
                             | AF_INTF
                             | AF_COIP
                             | AF_CNT
                             | Pseudo_AF_RTIP
                             | Pseudo_AF_PIP
                             | AF_SIP
                             | AF_ISDN
                             | Pseudo_AF_KEY
                             | AF_NATM
                             | AF_ARP
                             | Pseudo_AF_HDRCMPLT
                             | AF_ENCAP
                             | AF_LINK
                             | AF_RAW
                             | AF_RIF
                             | AF_NETROM
                             | AF_BRIDGE
                             | AF_ATMPVC
                             | AF_ROSE
                             | AF_NETBEUI
                             | AF_SECURITY
                             | AF_PACKET
                             | AF_ASH
                             | AF_ECONET
                             | AF_ATMSVC
                             | AF_IRDA
                             | AF_PPPOX
                             | AF_WANPIPE
                             | AF_BLUETOOTH
                             | AF_CAN ) #-}

data SocketOption : Set where
  Debug         : SocketOption
  ReuseAddr     : SocketOption
  Type          : SocketOption
  SoError       : SocketOption
  DontRoute     : SocketOption
  Broadcast     : SocketOption
  SendBuffer    : SocketOption
  RecvBuffer    : SocketOption
  KeepAlive     : SocketOption
  OOBInline     : SocketOption
  TimeToLive    : SocketOption
  MaxSegment    : SocketOption
  NoDelay       : SocketOption
  Cork          : SocketOption
  Linger        : SocketOption
  ReusePort     : SocketOption
  RecvLowWater  : SocketOption
  SendLowWater  : SocketOption
  RecvTimeOut   : SocketOption
  SendTimeOut   : SocketOption
  UseLoopBack   : SocketOption
  UserTimeout   : SocketOption
  IPv6Only      : SocketOption
  CustomSockOpt : ℤ × ℤ → SocketOption

{-
{-# COMPILE GHC SocketOption = data Network.Socket.SocketOption
                                ( Debug
                                | ReuseAddr
                                | Type
                                | SoError
                                | DontRoute
                                | Broadcast
                                | SendBuffer
                                | RecvBuffer
                                | KeepAlive
                                | OOBInline
                                | TimeToLive
                                | MaxSegment
                                | NoDelay
                                | Cork
                                | Linger
                                | ReusePort
                                | RecvLowWater
                                | SendLowWater
                                | RecvTimeOut
                                | SendTimeOut
                                | UseLoopBack
                                | UserTimeout
                                | IPv6Only
                                | CustomSockOpt ) #-}
-}

postulate
    Family : Set
    Socket : Set

{-# COMPILE GHC Family = type Network.Socket.Family #-}
{-# COMPILE GHC Socket = type Network.Socket.Socket #-}

ProtocolNumber : Set
ProtocolNumber = ℤ

data SocketStatus : Set where
  NotConnected      : SocketStatus
  Bound             : SocketStatus
  Listening         : SocketStatus
  Connected         : SocketStatus
  ConvertedToHandle : SocketStatus
  Closed            : SocketStatus

{-# COMPILE GHC SocketStatus = data Network.Socket.SocketStatus
  ( NotConnected
  | Bound
  | Listening
  | Connected
  | ConvertedToHandle
  | Closed ) #-}

-- data SockAddr where
--   SockAddrInet   : PortNumber → HostAddress → SockAddr
--   SockAddrInet6  : PortNumber → FlowInfo → HostAddress6 → ScopeID → SockAddr
--   SockAddrUnix   : String → SockAddr
--   SockAddrCan    : ℤ → SockAddr

-- record Socket : Set where
--     constructor MkSocket
--     field
--         sock     : ℤ
--         family   : Family
--         type     : SocketType
--         protonum : ProtocolNumber
--         status   : MVar SocketStatus
-- open Socket

-- {-# COMPILE GHC Socket = #-}

{-# FOREIGN GHC
  import Unsafe.Coerce
  import Foreign.C.Types
  import Network.Socket

  coeCInt :: Integer -> Foreign.C.Types.CInt
  coeCInt n = Unsafe.Coerce.unsafeCoerce (n :: Integer) :: Foreign.C.Types.CInt
#-}

postulate
    socket : SockFamily → SocketType → ProtocolNumber → IO Socket
    -- setSocketOption : Socket → SocketOption → ℤ → IO ⊤
    -- bind   : Socket → SockAddr → IO ⊤
    -- listen : Socket → ℤ → IO ⊤
    -- accept : Socket → IO (Socket × SockAddr)

{-# COMPILE GHC socket = \ f t n -> Network.Socket.socket f t (coeCInt n) #-}


text:
------------------------------------------------------------------------------
-- Testing the η-expansion
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Eta4 where

infix  7 _≡_
infixl 10 _*_

postulate
  D         : Set
  zero      : D
  _≡_       : D → D → Set
  _+_       : D → D → D
  lam       : (D → D) → D
  rec       : D → D → D → D
  *-helper₂ : D → D → D

-- We don't η-expand the definition of _*_ before the translation,
-- because we cannot translate the λ-abstraction generated from
-- *-helper₂ n to FOL terms.
_*_ : D → D → D
m * n = rec m zero (lam (*-helper₂ n))
{-# ATP definition _*_ #-}

postulate
  foo : ∀ n → n * n ≡ n * n
{-# ATP prove foo #-}

ext: agda

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- Instantiation of Contractive for streams
------------------------------------------------------------------------

-- Taken from the paper.

-- The definition of Eq has been changed slightly, as compared to the
-- paper. The paper uses
--   Eq = λ n xs ys → take n xs ≡ take n ys.
-- The reason for the change is that with the definition above
-- coherence does not say anything about the first element in limU s.
-- With the definition in the paper head (s 0), which is the first
-- element in limU s, does not have to be related to head (s n) for
-- any other n, and this makes it impossible to prove isLimitU.
-- (Unless I have missed something.)

module Contractive.Stream {A : Set} where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Contractive
open import Data.Nat
open import Data.Nat.Induction
open import Data.Nat.Properties
import Data.Vec as Vec
open Vec using (_∷_; [])
open import Function
open import Relation.Unary
open import Relation.Binary.PropositionalEquality

<′-isWellFoundedOrder : IsWellFoundedOrder _<′_
<′-isWellFoundedOrder = record
  { trans         = λ {i} {j} {k} i+1≤j j+1≤k → ≤⇒≤′ (begin
                       suc i  ≤⟨ ≤′⇒≤ (≤′-step i+1≤j) ⟩
                       suc j  ≤⟨ ≤′⇒≤ j+1≤k ⟩
                       k      ∎)
  ; isWellFounded = <′-wellFounded
  }
  where open ≤-Reasoning

ofe : OFE
ofe = record
  { Carrier            = ℕ
  ; Domain             = Stream A
  ; _<_                = _<′_
  ; isWellFoundedOrder = <′-isWellFoundedOrder
  ; Eq                 = λ n xs ys → take (suc n) xs ≡ take (suc n) ys
  ; isEquivalence      = λ _ → record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }

open OFE ofe

private

  limU : (ℕ → Stream A) → Stream A
  limU s = head (s 0) ∷ ♯ limU (tail ∘ s ∘ suc)

  η : ∀ {n} {xs : Stream A} → Eq n xs (head xs ∷ ♯ tail xs)
  η {xs = x ∷ xs} = refl

  step : ∀ s →
         IsCoherent {U} (lift s) →
         IsCoherent {U} (lift (tail ∘ s ∘ suc))
  step s coh {m} {n} _ _ m<n = begin
    take (suc m) (tail (s (suc m)))      ≡⟨ lem (s (suc m)) ⟩
    Vec.tail (take (2 + m) (s (1 + m)))  ≡⟨ cong Vec.tail $ coh {1 + m} {1 + n} _ _ (s≤′s m<n) ⟩
    Vec.tail (take (2 + m) (s (1 + n)))  ≡⟨ sym $ lem (s (suc n)) ⟩
    take (suc m) (tail (s (suc n)))      ∎
    where
    open ≡-Reasoning

    lem : ∀ {n} (xs : Stream A) →
          take n (tail xs) ≡ Vec.tail (take (1 + n) xs)
    lem (x ∷ xs) = refl

  isLimitU : ∀ s →
             IsCoherent {U} (lift s) →
             IsLimit {U} (lift s) (limU s)
  isLimitU s coh {zero}  _ = begin
    take 1 (s 0)     ≡⟨ η ⟩
    head (s 0) ∷ []  ∎
    where open ≡-Reasoning
  isLimitU s coh {suc n} _ = begin
    take (2 + n) (s (1 + n))                                 ≡⟨ η ⟩
    head (s (1 + n)) ∷ take (1 + n) ((tail ∘ s ∘ suc) n)     ≡⟨ cong₂ _∷_ lem₁ (isLimitU (tail ∘ s ∘ suc)
                                                                                (step s coh) {n} _) ⟩
    head (s 0)       ∷ take (1 + n) (limU (tail ∘ s ∘ suc))  ∎
    where
    open ≡-Reasoning

    lem₂ : ∀ {n} (xs ys : Stream A) →
           Eq n xs ys → head xs ≡ head ys
    lem₂ (x ∷ xs) (y ∷ ys) = cong Vec.head

    lem₁ : head (s (1 + n)) ≡ head (s 0)
    lem₁ = lem₂ _ _ $ sym $ coh {0} {suc n} _ _ (s≤′s z≤′n)

  lim↓ : A → ∀ n → (∀ n' → n' <′ n → Stream A) → Stream A
  lim↓ x zero    s = repeat x
  lim↓ x (suc n) s = s n ≤′-refl

  isLimit↓ : ∀ x n (s : Family (↓ n)) →
             IsCoherent s → IsLimit s (lim↓ x n s)
  isLimit↓ x zero    s coh ()
  isLimit↓ x (suc n) s coh ≤′-refl       = refl
  isLimit↓ x (suc n) s coh (≤′-step m<n) =
    coh (≤′-step m<n) ≤′-refl m<n

-- The paper implicitly assumes that A is non-empty.

cofe : A → COFE
cofe x = record
  { ofe      = ofe
  ; limU     = limU
  ; isLimitU = isLimitU _
  ; lim↓     = lim↓ x
  ; isLimit↓ = λ n {s} → isLimit↓ x n s
  }

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module MorePropAlgebra.Consequences where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Function.Base using (_∋_; _$_)
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax to infix  -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix  -4 ∃[∶]-syntax --
  ; ∀[∶]-syntax to infix  -4 ∀[∶]-syntax --
  ; ∀[]-syntax to infix  -4 ∀[]-syntax   --
  )
open import Cubical.HITs.PropositionalTruncation.Base -- ∣_∣
open import Cubical.HITs.PropositionalTruncation.Properties using (propTruncIsProp) renaming (elim to ∣∣-elim)

open import Utils
open import MoreLogic.Reasoning
open import MoreLogic.Definitions renaming
  ( _ᵗ⇒_ to infixr 0 _ᵗ⇒_
  ; ∀ᵖ[∶]-syntax to infix -4 ∀ᵖ[∶]-syntax
  ; ∀ᵖ〚∶〛-syntax to infix -4 ∀ᵖ〚∶〛-syntax
  ; ∀ᵖ!〚∶〛-syntax to infix -4 ∀ᵖ!〚∶〛-syntax
  ; ∀〚∶〛-syntax to infix -4 ∀〚∶〛-syntax
  )
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions

-- NOTE: hProps need to be explicit arguments (that is not a necessity, but we need to give them completely and not just their witnesses)
-- NOTE: I think one can make all `isProp` implementations `abstract` to save some compilation time
--         because we have `isPropIsProp` anyways
--       but for the logic part, it depends on how coslty
--         ⊔-elim, ⊥-elim, ⇒∶_⇐∶_, isoToPath, hProp≡, etc.
--       are and whether they could actually reduce some terms

module _ {ℓ ℓ' : Level} {A : Type ℓ} (R : hPropRel A A ℓ')
  (let _<_ = R)
  (let _≤_ = R)
  (let _#_ = R)
  where
  -- abstract
  irrefl+trans⇒asym    : [ isIrrefl  R ] → [ isTrans  R ] → [ isAsym  R ]
  irrefl+trans⇒asym'   : [ isIrrefl  R ] → [ isTrans  R ] → [ isAsym' R ]

  <-cotrans⇒≤-trans    : [ isCotrans _<_ ] → [ isTrans (λ x y → ¬(y < x)) ]
  connex⇒refl          : [ isConnex  _≤_ ] → [ isRefl _≤_ ]

  isIrrefl⇔isIrrefl'   :                              [ isIrrefl  _<_ ⇔ isIrrefl'  _<_ ]
  isIrrefl'⇔isIrrefl'' : (<-asym : [ isAsym  _<_ ]) → [ isIrrefl' _<_ ⇔ isIrrefl'' _<_ ]

  isAsym⇔isAsym'       :                              [ isAsym     R  ⇔ isAsym'                                    R           ]
  isTight⇔isTight'     :                              [ isTight    R  ⇔ isTight'                                   R           ]
  isTight'⇔isTight''   :                              [ isTight'   R  ⇔ isTight''                                  R           ]
  isTight'⇔isTight'''  :                              [ isTight'  _<_ ⇔ isTight''' (λ x y →                (x < y) ⊔  (y < x)) ]
  isTight''⇔isTight''' : (<-asym : [ isAsym  _<_ ]) → [ isTight'' _<_ ⇔ isTight''' (λ x y → [ <-asym x y ] (x < y) ⊎ᵖ (y < x)) ]
  isTight⇔isAntisym    :                              [ isTight   _<_ ⇔ isAntisym  (λ x y →                   ¬ (y < x))       ]

  strictlinearorder⇒strictpartialorder : [ isStrictLinearOrder _<_                   ⇒ isStrictPartialOrder _<_ ]
  linearorder⇒partialorder             : [ isLinearOrder       _≤_                   ⇒ isPartialOrder       _≤_ ]

  irrefl+trans⇒asym isIrrefl isTrans a b a<b b<a = isIrrefl _ (isTrans _ _ _ a<b b<a)

  irrefl+trans⇒asym' isIrrefl isTrans a b (a<b , b<a) = isIrrefl _ (isTrans _ _ _ a<b b<a)

  <-cotrans⇒≤-trans <-cotrans a b c ¬b<a ¬c<b c<a = ⊔-elim (c < b) (b < a) (λ _ → ⊥)
                                                     (λ c<b → ¬c<b c<b)
                                                     (λ b<a → ¬b<a b<a)
                                                     (<-cotrans _ _ c<a b)

  connex⇒refl is-connex a = case is-connex a a as a ≤ a ⊔ a ≤ a ⇒ a ≤ a of λ{ (inl p) → p ; (inr p) → p }

  isIrrefl⇔isIrrefl' .fst <-irrefl  a b a<b⊔b<a a≡b =
    substₚ (λ b → a < b ⊔ b < a ⇒ ⊥) a≡b
    (λ p → case p as R a a ⊔ R a a ⇒ ⊥ of λ{ (inl p) → <-irrefl _ p ; (inr p) → <-irrefl _ p })
    a<b⊔b<a
  isIrrefl⇔isIrrefl' .snd <-irrefl' x x<x = <-irrefl' x x (inlᵖ x<x) ∣ refl ∣

  isIrrefl'⇔isIrrefl'' <-asym .fst <-irrefl' a b (inl a<b) = <-irrefl'  a b (inlᵖ a<b)
  isIrrefl'⇔isIrrefl'' <-asym .fst <-irrefl' a b (inr b<a) = <-irrefl'  a b (inrᵖ b<a)
  isIrrefl'⇔isIrrefl'' <-asym .snd <-irrefl'' a b a<b⊎b<a = case a<b⊎b<a as a < b ⊔ b < a ⇒ ¬ a ≡ₚ b of λ
                                               { (inl a<b) → <-irrefl'' a b (inl a<b)
                                               ; (inr b<a) → <-irrefl'' a b (inr b<a) }

  isAsym⇔isAsym' .fst <-asym a b (a<b , b<a) = <-asym a b a<b b<a
  isAsym⇔isAsym' .snd <-asym a b = fst (¬-⊓-distrib (a < b) (b < a) (<-asym a b))

  isTight⇔isTight' .fst <-tightᵖ  a b ¬ᵗ[a<b⊔b<a]     = let (¬ᵗ[a<b] , ¬ᵗ[b<a]) = deMorgan₂ (a < b) (b < a) ¬ᵗ[a<b⊔b<a] in <-tightᵖ a b ¬ᵗ[a<b] ¬ᵗ[b<a]
  isTight⇔isTight' .snd <-tightᵖ' a b ¬ᵗ[a<b] ¬ᵗ[b<a] = <-tightᵖ' a b (deMorgan₂-back (a < b) (b < a) (¬ᵗ[a<b] , ¬ᵗ[b<a]))

  isTight'⇔isTight'' .fst <-tightᵖ'  a b ¬ᵗ[a<b⊎b<a] = <-tightᵖ'  a b (pathTo⇒ (∥¬A∥≡¬∥A∥ _) ∣ ¬ᵗ[a<b⊎b<a] ∣)
  isTight'⇔isTight'' .snd <-tightᵖ'' a b ¬ᵗ[a<b⊔b<a] = <-tightᵖ'' a b (λ [a<b⊎b<a] → ¬ᵗ[a<b⊔b<a] (⊎⇒⊔ (a < b) (b < a) [a<b⊎b<a]))

  isTight'⇔isTight''' .fst x = x
  isTight'⇔isTight''' .snd x = x

  isTight''⇔isTight''' <-asym .fst x = x
  isTight''⇔isTight''' <-asym .snd x = x

  isTight⇔isAntisym .fst <-tight   a b a≤b b≤a = <-tight   a b b≤a a≤b
  isTight⇔isAntisym .snd ≤-antisym a b b≤a a≤b = ≤-antisym a b a≤b b≤a

  strictlinearorder⇒strictpartialorder is-StrictLinearOrder = isstrictpartialorder is-irrefl is-trans is-cotrans where
    is-irrefl = IsStrictLinearOrder.is-irrefl is-StrictLinearOrder
    is-trans  = IsStrictLinearOrder.is-trans  is-StrictLinearOrder
    is-tricho = IsStrictLinearOrder.is-tricho is-StrictLinearOrder
    is-asym   = irrefl+trans⇒asym is-irrefl is-trans
    is-cotrans : [ isCotrans _<_ ]
    is-cotrans a b a<b x with is-tricho a x | is-tricho x b
    ... | inl (inl a<x) | q = inlᵖ a<x
    ... | inl (inr x<a) | inl (inl x<b) = inrᵖ x<b
    ... | inl (inr x<a) | inl (inr b<x) = ⊥-elim $ is-irrefl x (is-trans x b x (is-trans x a b x<a a<b) b<x)
    ... | inl (inr x<a) | inr      x≡b  = ⊥-elim $ is-asym a b a<b (substₚ (λ p → p < a) x≡b x<a)
    ... | inr      a≡x  | inl (inl x<b) = inrᵖ x<b
    ... | inr      a≡x  | inl (inr b<x) = ⊥-elim $ is-asym b x b<x (substₚ (λ p → p < b) a≡x a<b)
    ... | inr      a≡x  | inr      x≡b  = ⊥-elim $ is-irrefl b (substₚ (λ p → p < b) x≡b $ substₚ (λ p → p < b) a≡x a<b)

  linearorder⇒partialorder is-LinearOrder =
    let (islinearorder is-connex is-antisym is-trans) = is-LinearOrder
    in ispartialorder (connex⇒refl is-connex) is-antisym is-trans

  -- consequences on sets
  module _ (is-set : isSet A) where
    -- abstract
    isIrreflˢ''⇔isIrrefl''  : (is-asym : [ isAsym R ])    → [ isIrreflˢ'' R is-set ⇔ isIrrefl'' R ]
    isAntisymˢ⇔isAntisym    :                               [ isAntisymˢ  R is-set ⇔ isAntisym  R ]
    isAntisymˢ'⇔isAntisym'  :                               [ isAntisymˢ' R is-set ⇔ isAntisym' R ]
    isTightˢ⇔isTight        :                               [ isTightˢ    R is-set ⇔ isTight    R ]
    isTightˢ'⇔isTight'      :                               [ isTightˢ'   R is-set ⇔ isTight'   R ]
    isTightˢ''⇔isTight''    :                               [ isTightˢ''  R is-set ⇔ isTight''  R ]
    isTightˢ'''⇔isTight'''  :                               [ isTightˢ''' R is-set ⇔ isTight''' R ]
    isTightˢ'''⇔isAntisymˢ  : (is-asym : [ isAsym R ])    → [ isTightˢ''' (λ x y → [ is-asym x y ] (x < y) ⊎ᵖ (y < x)) is-set
                                                            ⇔ isAntisymˢ  (λ x y →                    ¬ (y < x)      ) is-set ]

    isTrichotomousˢ⇔isTrichotomous : (is-irrefl : [ isIrrefl'' R ]) → (is-irreflˢ : [ isIrreflˢ'' R is-set ]) → (is-asym : [ isAsym R ]) → [ isTrichotomousˢ R is-set is-irreflˢ is-asym ⇔ isTrichotomous R is-irrefl is-asym ]

    -- tricho⇒cotrans                       : (is-irrefl : [ isIrrefl'' R ]) → (is-asym : [ isAsym R ])
    --                                      → [ isTrichotomous      _<_ is-irrefl is-asym ⇒ isCotrans            _<_ ]

    isIrreflˢ''⇔isIrrefl'' <-asym .fst <-irreflˢ'' a b a<b a≡b = <-irreflˢ'' a b a<b (∣∣-elim (λ c → is-set a b) (λ x → x) a≡b)
    isIrreflˢ''⇔isIrrefl'' <-asym .snd <-irrefl''  a b a<b a≡b = <-irrefl''  a b a<b ∣ a≡b ∣

    isAntisymˢ⇔isAntisym .fst ≤-antisymˢ a b a≤b b≤a = ∣ ≤-antisymˢ a b a≤b b≤a ∣
    isAntisymˢ⇔isAntisym .snd ≤-antisym  a b a≤b b≤a = ∣∣-elim (λ c → is-set a b) (λ x → x) (≤-antisym  a b a≤b b≤a)

    isAntisymˢ'⇔isAntisym' .fst ≤-antisymˢ' a b a≤b ¬ᵗa≡b = ≤-antisymˢ' a b a≤b (λ  z  → ¬ᵗa≡b ∣ z ∣)
    isAntisymˢ'⇔isAntisym' .snd ≤-antisym'  a b a≤b ¬ᵗa≡b = ≤-antisym'  a b a≤b (λ ∣z∣ → ∣∣-elim {P = λ _ → ⊥⊥} (λ _ → isProp⊥) ¬ᵗa≡b ∣z∣)

    isTightˢ⇔isTight .fst <-tightˢ a b a<b b<a = ∣ <-tightˢ a b a<b b<a ∣
    isTightˢ⇔isTight .snd <-tightᵖ a b a<b b<a = ∣∣-elim (λ c → is-set a b) (λ x → x) (<-tightᵖ a b a<b b<a)

    isTightˢ'⇔isTight' .fst <-tightˢ' a b ¬ᵗ[a<b⊔b<a] = ∣ <-tightˢ' a b ¬ᵗ[a<b⊔b<a] ∣
    isTightˢ'⇔isTight' .snd <-tightᵖ' a b ¬ᵗ[a<b⊔b<a] = ∣∣-elim (λ c → is-set a b) (λ x → x) (<-tightᵖ' a b ¬ᵗ[a<b⊔b<a])

    isTightˢ''⇔isTight'' .fst <-tightˢ'' a b ¬ᵗ[a<b⊎b<a] = ∣ <-tightˢ'' a b ¬ᵗ[a<b⊎b<a] ∣
    isTightˢ''⇔isTight'' .snd <-tightᵖ'' a b ¬ᵗ[a<b⊎b<a] = ∣∣-elim (λ c → is-set a b) (λ x → x) (<-tightᵖ'' a b ¬ᵗ[a<b⊎b<a])

    isTightˢ'''⇔isTight''' .fst #-tightˢ''' a b ¬ᵗ[a#b] = ∣ #-tightˢ''' a b ¬ᵗ[a#b] ∣
    isTightˢ'''⇔isTight''' .snd #-tightᵖ''' a b ¬ᵗ[a#b] = ∣∣-elim (λ c → is-set a b) (λ x → x) (#-tightᵖ''' a b ¬ᵗ[a#b])

    isTightˢ'''⇔isAntisymˢ <-asym .fst #-tight a b a≤b b≤a = #-tight a b (deMorgan₂-back' (b≤a , a≤b))
    isTightˢ'''⇔isAntisymˢ <-asym .snd ≤-antisym a b ¬ᵗa#b = let (b≤a , a≤b) = deMorgan₂' ¬ᵗa#b in ≤-antisym a b a≤b b≤a

    isTrichotomousˢ⇔isTrichotomous <-irreflˢ <-irrefl <-asym .fst <-trichoˢ a b with <-trichoˢ a b
    ... | inl a<b⊎b<a = inl a<b⊎b<a
    ... | inr a≡b     = inr ∣ a≡b ∣
    isTrichotomousˢ⇔isTrichotomous <-irreflˢ <-irrefl <-asym .snd <-tricho  a b with <-tricho a b
    ... | inl a<b⊎b<a = inl a<b⊎b<a
    ... | inr a≡b     = inr (∣∣-elim (λ c → is-set a b) (λ x → x) a≡b)

-- for these pathes, `A` and `hProp.fst` need to be in the same universe to omit ugly lifting into `ℓ-max ℓ ℓ'`
--   although this would be possible to have (with lifting)
module _ {ℓ : Level} {A : Type ℓ} (_≤_ : hPropRel A A ℓ)
  (let R   = _≤_)
  (let _<_ = R) -- different semantics
  (let _≤_ = R) --
  (let _#_ = R) --
  where
  -- equivalence of "not apart" and "equal"
  [¬ᵗ#]⇔[≡]  : hProp ℓ
  [¬ᵗ#]⇔[≡]  = ∀[ a ] ∀[ b ] ¬ (a # b) ⇔ a ≡ₚ b
  [¬ᵗ#]⇔[≡]ᵗ : Type (ℓ-suc ℓ)
  [¬ᵗ#]⇔[≡]ᵗ = ∀ a b → (¬ᵗ [ a # b ]) ≡ (a ≡ b)

  -- double negation elimination over _≡_
  dne-over-≡ᵗ : Type (ℓ-suc ℓ)
  dne-over-≡ᵗ = ∀(a b : A) → (¬ᵗ ¬ᵗ (a ≡ b)) ≡ (a ≡ b)

  abstract
    irrefl+tight⇒[¬ᵗ#]⇔[≡] : [ isIrrefl  _#_ ] → [ isTight''' _#_ ] → [ [¬ᵗ#]⇔[≡] ]
    irrefl+tight⇒[¬ᵗ#]⇔[≡] #-irrefl #-tight a b .fst ¬ᵗ[a#b] = #-tight a b ¬ᵗ[a#b]
    irrefl+tight⇒[¬ᵗ#]⇔[≡] #-irrefl #-tight a b .snd a≡b a#b = #-irrefl b (substₚ (λ x → x # b) a≡b a#b)

    [¬ᵗ#]≡[≡]⇒dne-over-≡ : [¬ᵗ#]⇔[≡]ᵗ → dne-over-≡ᵗ
    [¬ᵗ#]≡[≡]⇒dne-over-≡ [¬ᵗ#]≡[≡] a b =
      (    ¬ᵗ ¬ᵗ ( a ≡ b ) ≡⟨ (λ i → ¬ᵗ ¬ᵗ [¬ᵗ#]≡[≡] a b (~ i)) ⟩
        ¬ᵗ ¬ᵗ ¬ᵗ [ a # b ] ≡⟨ ¬¬-involutiveᵗ [ a # b ] ⟩
              ¬ᵗ [ a # b ] ≡⟨ [¬ᵗ#]≡[≡] a b ⟩
                   a ≡ b   ∎)

  -- consequences on sets
  module _ (is-set : isSet A) where
    -- equivalence of "not apart" and "equal" on sets
    [¬ᵗ#]⇔[≡ˢ] = ∀[ a ] ∀[ b ]             ¬ (a # b) ⇔ [ is-set ] a ≡ˢ b

    -- double negation elimination over _≡_ on sets
    dne-over-≡ˢ  = ∀[ a ] ∀[ b ] ¬ ¬ ([ is-set ] a ≡ˢ b) ⇔ [ is-set ] a ≡ˢ b

    irrefl+tight⇒[¬ᵗ#]⇔[≡ˢ]   : [ isIrrefl  _#_ ] → [ isTightˢ''' _#_ is-set ] → [ [¬ᵗ#]⇔[≡ˢ] ]
    [¬ᵗ#]⇔[≡ˢ]⇒dne-over-≡ˢ    : [ [¬ᵗ#]⇔[≡ˢ] ]                                 → [ dne-over-≡ˢ ]
    irrefl+tight⇒dne-over-≡ˢ  : [ isIrrefl  _#_ ] → [ isTightˢ''' _#_ is-set ] → [ dne-over-≡ˢ ]
    irrefl+tight⇒[¬ᵗ#]≡[≡ˢ]   : [ isIrrefl  _#_ ] → [ isTightˢ''' _#_ is-set ] → ∀ a b → (¬ᵗ [ a # b ]) ≡ (a ≡ b)
    irrefl+tight⇒dne-over-≡ˢᵗ : [ isIrrefl  _#_ ] → [ isTightˢ''' _#_ is-set ] → ∀(a b : A) → (¬ᵗ ¬ᵗ (a ≡ b)) ≡ (a ≡ b)

    -- x ≤ y  ≡ ¬(y < x)
    -- x <' y ≡ ¬(y ≤ x) ≡ ¬¬(x < y)
    -- ¬¬(x < y) ⇔ (x < y) ??
    -- x ≤ y ⇔ ∀[ ε ] (y < ε) ⇒ (x < ε)

    -- https://en.wikipedia.org/wiki/Total_order
    -- We can work the other way and start by choosing < as a transitive trichotomous binary relation; then a total order ≤ can be defined in two equivalent ways:
    -- https://en.wikipedia.org/wiki/Weak_ordering#Strict_weak_orderings

    -- IsStrictLinearOrder _<_ ⇒ IsLinearOrder _≤_

    irrefl+tight⇒[¬ᵗ#]⇔[≡ˢ] #-irrefl #-tight a b .fst ¬ᵗ[a#b] = #-tight a b ¬ᵗ[a#b]
    irrefl+tight⇒[¬ᵗ#]⇔[≡ˢ] #-irrefl #-tight a b .snd a≡b a#b = #-irrefl b (subst (λ x → [ x # b ]) a≡b a#b)

    irrefl+tight⇒[¬ᵗ#]≡[≡ˢ] #-irrefl #-tight a b = isoToPath γ where
      γ : Iso _ _
      γ .Iso.fun      ¬ᵗ[a#b] = #-tight a b ¬ᵗ[a#b]
      γ .Iso.inv      a≡b a#b = #-irrefl b (subst (λ x → [ x # b ]) a≡b a#b)
      γ .Iso.rightInv f       = is-set a b _ f
      γ .Iso.leftInv  g       = isProp[] (¬ (a #  b)) _ g

    [¬ᵗ#]⇔[≡ˢ]⇒dne-over-≡ˢ [¬ᵗ#]⇔[≡ˢ] a b = snd ( -- this first proof works better with `_≡⟨_⟩_`
      -- ( ¬ ¬ ([ is-set ]     a ≡ˢ b)) ⇔⟨ (map-× (subst (λ p → fst p → snd p) (cong₂ _,_ {! ¬¬-introᵗ (a ≡ b)  !} {!   !})) {!   !} $ swap $ [¬ᵗ#]⇔[≡ˢ] a b) ⟩
      ( ¬ ¬ ([ is-set ]     a ≡ˢ b)) ⇔⟨ (map-× (λ z z₁ z₂ → z₂ (λ z₃ → z₁ (λ z₄ → z z₄ z₃))) (λ z z₁ z₂ → z₂ (z (λ z₃ → z₁ (λ z₄ → z₄ z₃)))) $ swap $ [¬ᵗ#]⇔[≡ˢ] a b) ⟩ -- how did Agsy find this out??
      ( ¬              ¬ ¬ (a #  b)) ⇔⟨ ¬¬-involutive (a # b) ⟩
      ( ¬                  (a #  b)) ⇔⟨ [¬ᵗ#]⇔[≡ˢ] a b ⟩
      (      [ is-set ]     a ≡ˢ b ) ∎ᵖ)

    irrefl+tight⇒dne-over-≡ˢ  #-irrefl #-tight = [¬ᵗ#]⇔[≡ˢ]⇒dne-over-≡ˢ (irrefl+tight⇒[¬ᵗ#]⇔[≡ˢ] #-irrefl #-tight)

    irrefl+tight⇒dne-over-≡ˢᵗ #-irrefl #-tight = [¬ᵗ#]≡[≡]⇒dne-over-≡   (irrefl+tight⇒[¬ᵗ#]≡[≡ˢ] #-irrefl #-tight)

module _ {ℓ : Level} {A : Type ℓ}  (is-set : isSet A) where

  nzinvˢ''+comm⇒invnzˢ : (0f 1f : A) (_·_ : A → A → A) → ∀{ℓ'} → (_#_ : hPropRel A A ℓ')
                       → [ isNonzeroInverseˢ'' is-set 0f 1f _·_ _#_ ⊓ isCommutativeˢ _·_ is-set
                         ⇒ isInverseNonzeroˢ   is-set 0f 1f _·_ _#_ ]
  nzinvˢ''+comm⇒invnzˢ 0f 1f _·_ _#_ (is-nzinv , ·-comm) x y x·y≡1 .fst = fst (is-nzinv x) ∣ y ,              x·y≡1 ∣
  nzinvˢ''+comm⇒invnzˢ 0f 1f _·_ _#_ (is-nzinv , ·-comm) x y x·y≡1 .snd = fst (is-nzinv y) ∣ x , ·-comm y x ∙ x·y≡1 ∣

module _ {ℓ ℓ'} {X : Type ℓ} {_<_ : hPropRel X X ℓ'} (<-SPO : [ isStrictPartialOrder  _<_ ])
  (let _#'_ : hPropRel X X ℓ'
       x #' y = (x < y) ⊔ (y < x)
       _≤'_ : hPropRel X X ℓ'
       x ≤' y = ¬ (y < x)
       (isstrictpartialorder <-irrefl <-trans <-cotrans) = <-SPO
  ) where
  abstract
    -- Lemma 4.1.7.
    -- Given a strict partial order < on a set X:
    -- 1. we have an apartness relation defined by
    --    x # y := (x < y) ∨ (y < x), and

    #'-isApartnessRel : [ isApartnessRel _#'_ ]
    #'-isApartnessRel .IsApartnessRel.is-irrefl a a#a =
      case a#a as a < a ⊔ a < a ⇒ ⊥ of λ where
        (inl a<a) → <-irrefl _ a<a
        (inr a<a) → <-irrefl _ a<a
    #'-isApartnessRel .IsApartnessRel.is-sym     a b p = pathTo⇒ (⊔-comm (a < b) (b < a)) p
    #'-isApartnessRel .IsApartnessRel.is-cotrans a b p =
      case p as a < b ⊔ b < a ⇒ ∀[ x ] (a #' x) ⊔ (x #' b) of λ where
        (inl a<b) x → case (<-cotrans _ _ a<b x) as a < x ⊔ x < b ⇒ (a #' x) ⊔ (x #' b) of λ where
          (inl a<x) → inlᵖ (inlᵖ a<x)
          (inr x<b) → inrᵖ (inlᵖ x<b)
        (inr b<a) x → case (<-cotrans _ _ b<a x) as b < x ⊔ x < a ⇒ (a #' x) ⊔ (x #' b) of λ where
          (inl b<x) → inrᵖ (inrᵖ b<x)
          (inr x<a) → inlᵖ (inrᵖ x<a)

    -- 2. we have a preorder defined by
    --    x ≤ y := ¬ᵗ(y < x).

    ≤'-isPreorder : [ isPreorder _≤'_ ]
    ≤'-isPreorder .IsPreorder.is-refl = <-irrefl
    ≤'-isPreorder .IsPreorder.is-trans a b c ¬ᵗb<a ¬ᵗc<b c<a =
         ⊔-elim (c < b) (b < a) (λ _ → ⊥)
         (λ c<b → ¬ᵗc<b c<b)
         (λ b<a → ¬ᵗb<a b<a)
         (<-cotrans _ _ c<a b)

module _ {ℓ ℓ'} {X : Type ℓ} {_<_ : hPropRel X X ℓ'} (<-SPO : [ isStrictPartialOrder  _<_ ]) (<-asym : [ isAsym _<_ ])
  (let _#''_ : hPropRel X X ℓ'
       x #'' y = [ <-asym x y ] (x < y) ⊎ᵖ (y < x)
       _≤'_ : hPropRel X X ℓ'
       x ≤' y = ¬ (y < x)
       (isstrictpartialorder <-irrefl <-trans <-cotrans) = <-SPO
  ) where
  abstract
    #''-isApartnessRel : [ isApartnessRel _#''_ ]
    #''-isApartnessRel .IsApartnessRel.is-irrefl a (inl a<a) = <-irrefl _ a<a
    #''-isApartnessRel .IsApartnessRel.is-irrefl a (inr a<a) = <-irrefl _ a<a
    #''-isApartnessRel .IsApartnessRel.is-sym     a b p = ⊎-swap p
    #''-isApartnessRel .IsApartnessRel.is-cotrans a b (inl a<b) x =
      case (<-cotrans _ _ a<b x) as a < x ⊔ x < b ⇒ (a #'' x) ⊔ (x #'' b) of λ where
        (inl a<x) → inlᵖ (inl a<x)
        (inr x<b) → inrᵖ (inl x<b)
    #''-isApartnessRel .IsApartnessRel.is-cotrans a b (inr b<a) x =
      case (<-cotrans _ _ b<a x) as b < x ⊔ x < a ⇒ (a #'' x) ⊔ (x #'' b) of λ where
        (inl b<x) → inrᵖ (inr b<x)
        (inr x<a) → inlᵖ (inr x<a)

module _ {ℓ ℓ'} {X : Type ℓ} {_<_ : hPropRel X X ℓ'} (<-SLO : [ isStrictLinearOrder  _<_ ])
  (let _≤'_ : hPropRel X X ℓ'
       x ≤' y = ¬ (y < x)
       (isstrictlinearorder <-irrefl <-trans <-tricho) = <-SLO

  ) where
  private
    <-cotrans : [ isCotrans _<_ ]
    <-cotrans = IsStrictPartialOrder.is-cotrans (strictlinearorder⇒strictpartialorder _<_ <-SLO)

  abstract
    ≤'-isLinearOrder : [ isLinearOrder _≤'_ ]
    IsLinearOrder.is-connex  ≤'-isLinearOrder a b with <-tricho a b
    ... | inl (inl a<b) = inlᵖ λ b<a → <-irrefl a $ <-trans a b a a<b b<a
    ... | inl (inr b<a) = inrᵖ λ a<b → <-irrefl a $ <-trans a b a a<b b<a
    ... | inr      a≡b  = inlᵖ λ b<a → <-irrefl b (substₚ (λ p → b < p) a≡b b<a)
    IsLinearOrder.is-antisym ≤'-isLinearOrder a b a≤b b≤a with <-tricho a b
    ... | inl (inl a<b) = ⊥-elim (b≤a a<b)
    ... | inl (inr b<a) = ⊥-elim (a≤b b<a)
    ... | inr      a≡b  = a≡b
    IsLinearOrder.is-trans   ≤'-isLinearOrder a b c a≤b b≤c c<a =
      let γ : [ ¬ (b < a ⊔ c < b) ]
          γ = deMorgan₂-back (b < a) (c < b) (a≤b , b≤c)
          κ : [ b < a ⊔ c < b ]
          κ = pathTo⇐ (⊔-comm (b < a) (c < b)) $ <-cotrans c a c<a b
      in γ κ

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Reflexivity {{eqrel : EqRelSet}} where

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation

open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

-- Reflexivity of reducible types.
reflEq : ∀ {l Γ A r} ([A] : Γ ⊩⟨ l ⟩ A ^ r) → Γ ⊩⟨ l ⟩ A ≡ A ^ r / [A]
reflEq (Uᵣ′ _ _ _ _ l< PE.refl D) = red D
reflEq (ℕᵣ D) = red D
reflEq (Emptyᵣ D) = red D
reflEq (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) =
  ne₌ _ [[ ⊢A , ⊢B , D ]] neK K≡K
reflEq (Πᵣ′ rF lF lG _ _ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) =
  Π₌ _ _ D A≡A
     (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
     (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a]))
reflEq (∃ᵣ′ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) =
  ∃₌ _ _ D A≡A
    (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
    (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a]))
reflEq {ι ¹} (emb X [A]) = reflEq [A]
reflEq {∞} (emb X [A]) = reflEq [A]

reflNatural-prop : ∀ {Γ n}
                 → Natural-prop Γ n
                 → [Natural]-prop Γ n n
reflNatural-prop (sucᵣ (ℕₜ n d t≡t prop)) =
  sucᵣ (ℕₜ₌ n n d d t≡t
            (reflNatural-prop prop))
reflNatural-prop zeroᵣ = zeroᵣ
reflNatural-prop (ne (neNfₜ neK ⊢k k≡k)) = ne (neNfₜ₌ neK neK k≡k)

reflEmpty-prop : ∀ {Γ n l}
                 → Empty-prop Γ n l
                 → [Empty]-prop Γ n n l
reflEmpty-prop (ne x) = ne x x

-- Reflexivity of reducible terms.
-- We proceed in a layered way because Agda does not understand our
-- recursions are well founded

reflEqTerm⁰ : ∀ {Γ A t r} ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ r)
           → Γ ⊩⟨ ι ⁰ ⟩ t ∷ A ^ r / [A]
           → Γ ⊩⟨ ι ⁰ ⟩ t ≡ t ∷ A ^ r / [A]
reflEqTerm⁰ (ℕᵣ D) (ℕₜ n [[ ⊢t , ⊢u , d ]] t≡t prop) =
  ℕₜ₌ n n [[ ⊢t , ⊢u , d ]] [[ ⊢t , ⊢u , d ]] t≡t
      (reflNatural-prop prop)
reflEqTerm⁰ (Emptyᵣ D) (Emptyₜ (ne x)) = Emptyₜ₌ (ne x x)
reflEqTerm⁰ {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ k d (neNfₜ neK₁ ⊢k k≡k)) =
  neₜ₌ k k d d (neNfₜ₌ neK₁ neK₁ k≡k)
reflEqTerm⁰ {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ d) = neₜ₌ d d
reflEqTerm⁰ {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ₌ f f d d funcF funcF f≡f
      (Πₜ f d funcF f≡f [f] [f]₁)
      (Πₜ f d funcF f≡f [f] [f]₁)
      (λ ρ ⊢Δ [a] → [f] ρ ⊢Δ [a] [a] (reflEqTerm⁰ ([F] ρ ⊢Δ) [a]))
reflEqTerm⁰ {r = [ % , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) X = X , X
reflEqTerm⁰ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) X = X , X

reflEqTerm¹ : ∀ {Γ A t r} ([A] : Γ ⊩⟨ ι ¹ ⟩ A ^ r)
           → Γ ⊩⟨ ι ¹ ⟩ t ∷ A ^ r / [A]
           → Γ ⊩⟨ ι ¹ ⟩ t ≡ t ∷ A ^ r / [A]
reflEqTerm¹ (Uᵣ (Uᵣ r ⁰ X PE.refl D)) (Uₜ A d typeA A≡A [A]) =
  Uₜ₌ (Uₜ A d typeA A≡A [A]) (Uₜ A d typeA A≡A [A])
    A≡A (λ [ρ] ⊢Δ → reflEq ([A] [ρ] ⊢Δ))
reflEqTerm¹ (Uᵣ (Uᵣ r ¹ () PE.refl D)) (Uₜ A d typeA A≡A [A])
reflEqTerm¹ (ℕᵣ D) (ℕₜ n [[ ⊢t , ⊢u , d ]] t≡t prop) =
  ℕₜ₌ n n [[ ⊢t , ⊢u , d ]] [[ ⊢t , ⊢u , d ]] t≡t
      (reflNatural-prop prop)
reflEqTerm¹ (Emptyᵣ D) (Emptyₜ (ne x)) = Emptyₜ₌ (ne x x)
reflEqTerm¹ {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ k d (neNfₜ neK₁ ⊢k k≡k)) =
  neₜ₌ k k d d (neNfₜ₌ neK₁ neK₁ k≡k)
reflEqTerm¹ {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ d) = neₜ₌ d d
reflEqTerm¹ {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ₌ f f d d funcF funcF f≡f
      (Πₜ f d funcF f≡f [f] [f]₁)
      (Πₜ f d funcF f≡f [f] [f]₁)
      (λ ρ ⊢Δ [a] → [f] ρ ⊢Δ [a] [a] (reflEqTerm¹ ([F] ρ ⊢Δ) [a]))
reflEqTerm¹ {r = [ % , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) X = X , X
reflEqTerm¹ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) X = X , X
reflEqTerm¹ (emb X [A]) = reflEqTerm⁰ [A]

reflEqTerm∞ : ∀ {Γ A t r} ([A] : Γ ⊩⟨ ∞ ⟩ A ^ r)
           → Γ ⊩⟨ ∞ ⟩ t ∷ A ^ r / [A]
           → Γ ⊩⟨ ∞ ⟩ t ≡ t ∷ A ^ r / [A]
reflEqTerm∞ (Uᵣ (Uᵣ r ⁰ X eq D)) (Uₜ A d typeA A≡A [A]) =
  Uₜ₌ (Uₜ A d typeA A≡A [A]) (Uₜ A d typeA A≡A [A]) A≡A (λ [ρ] ⊢Δ → reflEq ([A] [ρ] ⊢Δ))
reflEqTerm∞ (Uᵣ (Uᵣ r ¹ X eq D)) (Uₜ A d typeA A≡A [A]) =
  Uₜ₌ (Uₜ A d typeA A≡A [A]) (Uₜ A d typeA A≡A [A]) A≡A (λ [ρ] ⊢Δ → reflEq ([A] [ρ] ⊢Δ))
reflEqTerm∞ (ℕᵣ D) (ℕₜ n [[ ⊢t , ⊢u , d ]] t≡t prop) =
  ℕₜ₌ n n [[ ⊢t , ⊢u , d ]] [[ ⊢t , ⊢u , d ]] t≡t
      (reflNatural-prop prop)
reflEqTerm∞ (Emptyᵣ D) (Emptyₜ (ne x)) = Emptyₜ₌ (ne x x)
reflEqTerm∞ {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ k d (neNfₜ neK₁ ⊢k k≡k)) =
  neₜ₌ k k d d (neNfₜ₌ neK₁ neK₁ k≡k)
reflEqTerm∞ {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ d) = neₜ₌ d d
reflEqTerm∞ {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ₌ f f d d funcF funcF f≡f
      (Πₜ f d funcF f≡f [f] [f]₁)
      (Πₜ f d funcF f≡f [f] [f]₁)
      (λ ρ ⊢Δ [a] → [f] ρ ⊢Δ [a] [a] (reflEqTerm∞ ([F] ρ ⊢Δ) [a]))
reflEqTerm∞ {r = [ % , l ]} (Πᵣ′ rF lF lG F G _ _ D ⊢F ⊢G A≡A [F] [G] G-ext) X = X , X
reflEqTerm∞ (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) X = X , X
reflEqTerm∞ (emb X [A]) = reflEqTerm¹ [A]

reflEqTerm : ∀ {l Γ A t r} ([A] : Γ ⊩⟨ l ⟩ A ^ r)
           → Γ ⊩⟨ l ⟩ t ∷ A ^ r / [A]
           → Γ ⊩⟨ l ⟩ t ≡ t ∷ A ^ r / [A]
reflEqTerm {l = ι ⁰} [A] [t] = reflEqTerm⁰ [A] [t]
reflEqTerm {l = ι ¹} [A] [t] = reflEqTerm¹ [A] [t]
reflEqTerm {l = ∞} [A] [t] = reflEqTerm∞ [A] [t]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Diagram.Limit.Ran where

open import Level
open import Data.Product using (Σ)

open import Categories.Category
open import Categories.Category.Complete
import Categories.Category.Construction.Cones as ConesCat
open import Categories.Category.Construction.Comma
open import Categories.Category.Construction.Properties.Comma
open import Categories.Category.Instance.One using (One)
open import Categories.Diagram.Cone using (Cone; Cone⇒)
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Limit
open import Categories.Diagram.Limit.Properties
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.Functor.Construction.Constant
open import Categories.Kan
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≊_)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; module ≃; _ⓘˡ_)
open import Categories.Object.Terminal using (Terminal)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR

-- construct a Ran from a limit
module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″} {C : Category o′ ℓ′ e′} {D : Category o ℓ e} {E : Category o″ ℓ″ e″}
         (F : Functor C D) (X : Functor C E) (Com : Complete (o′ ⊔ ℓ) (ℓ′ ⊔ e) e′ E) where
  private
    module C = Category C
    module D = Category D
    module E = Category E
    module F = Functor F
    module X = Functor X
    open Limit using (limit; proj; apex; module terminal)
    open Cone using () renaming (commute to K-commute)
    open ConesCat.Cone⇒ using (arr) renaming (commute to ⇒-commute)
    open Mor E using (_≅_)

    G   : (d : D.Obj) → Functor (d ↙ F) E
    G d = X ∘F Cod {A = One} {B = C} {C = D} (const! d) F

    ⊤Gd : (d : D.Obj) → Limit (G d)
    ⊤Gd d = Com (G d)
    module ⊤Gd d = Limit (⊤Gd d) using (proj; limit; rep; rep-cone; apex; module terminal)

    f↙F : {Y Z : D.Obj} (f : Y D.⇒ Z) → Functor (Z ↙ F) (Y ↙ F)
    f↙F   =  along-natˡ′ F

    Gf≃ : {Y Z : D.Obj} (f : Y D.⇒ Z) → G Z ≃ G Y ∘F f↙F f
    Gf≃ f = record
      { F⇒G = record
        { η           = λ z/F →  let j = CommaObj.β z/F in X.₁ {j} C.id -- help inference a bit
        ; commute     = λ _ → [ X ]-resp-square id-comm-sym
        ; sym-commute = λ _ → [ X ]-resp-square id-comm
        }
      ; F⇐G = record
        { η       = λ _ → X.₁ C.id
        ; commute = λ _ → [ X ]-resp-square id-comm-sym
        ; sym-commute = λ _ → [ X ]-resp-square id-comm
        }
      ; iso = λ _ → record
        { isoˡ = [ X ]-resp-∘ C.identity² ○ X.identity
        ; isoʳ = [ X ]-resp-∘ C.identity² ○ X.identity
        }
      }
      where open MR C using (id-comm-sym; id-comm)
            open E.HomReasoning using (_○_)

    Compl : {Y Z : D.Obj} (f : Y D.⇒ Z) → Limit (G Y ∘F f↙F f)
    Compl {Y} f = Com (G Y ∘F f↙F f)

    limY⇒limZ∘ : {Y Z : D.Obj} (f : Y D.⇒ Z) →
        ConesCat.Cones (G Y ∘F f↙F f) [ F-map-Coneʳ (f↙F f) (limit (Com (G Y))) , limit (Compl f) ]
    limY⇒limZ∘ {Y} f = F⇒arr Com (f↙F f) (G Y)

    limZ∘≅limZ : {Y Z : D.Obj} (f : Y D.⇒ Z) → ⊤Gd.apex Z ≅ apex (Compl f)
    limZ∘≅limZ {Y} {Z} f = ≃⇒lim≅ (Gf≃ f) (⊤Gd Z) (Compl f)

  limit-is-ran : Ran F X
  limit-is-ran = record
    { R        = R
    ; ε        = ε
    ; δ        = δ
    ; δ-unique = λ {M γ} δ′ eq → δ-unique {M} {γ} δ′ eq
    ; commutes = commutes
    }
    where
    open MR E
    open E.HomReasoning
    module DH = D.HomReasoning

    R₀ : D.Obj → E.Obj
    R₀ = ⊤Gd.apex
    R₁ : ∀ {A B} → D [ A , B ] → E [ R₀ A , R₀ B ]
    R₁ {A} f = _≅_.to (limZ∘≅limZ f) E.∘ arr (limY⇒limZ∘ f)

    ↙⇒ : {Y Z : D.Obj} (K : CommaObj {A = One} {C} {D} (const Z) F) (f : Y D.⇒ Z) → CommaObj {A = One} {C} {D} (const Y) F
    ↙⇒ K f = record { β = CommaObj.β K; f = D.id D.∘ CommaObj.f K D.∘ f }

    proj-red : {Y Z : D.Obj} (K : CommaObj (const Z) F) (f : Y D.⇒ Z) → ⊤Gd.proj Z K E.∘ R₁ f E.≈ ⊤Gd.proj Y (↙⇒ K f)
    proj-red {Y} {Z} K f = begin
      ⊤Gd.proj Z K E.∘ R₁ f                                  ≈⟨ pullˡ (⇒-commute (≃⇒Cone⇒ (≃.sym (Gf≃ f)) (Compl f) (⊤Gd Z))) ⟩
      (X.₁ C.id E.∘ proj (Compl f) K) E.∘ arr (limY⇒limZ∘ f) ≈⟨ pullʳ (⇒-commute (limY⇒limZ∘ f)) ⟩
      X.₁ C.id E.∘ ⊤Gd.proj Y f/K                            ≈⟨ elimˡ X.identity ⟩
      ⊤Gd.proj Y f/K                                         ∎
      where
      f/K : CommaObj {A = One} {C} {D} (const Y) F
      f/K = ↙⇒ K f

    commaF : {d : D.Obj} {c : C.Obj} (f : d D.⇒ F.₀ c) → CommaObj {A = One} {C} {D} (const d) F
    commaF f = record { f = f }

    proj≈ : {d : D.Obj} {b : C.Obj} {f g : d D.⇒ F.₀ b} → f D.≈ g → ⊤Gd.proj d (commaF f) E.≈ ⊤Gd.proj d (commaF g)
    proj≈ {d} {b} {f} {g} eq = begin
      ⊤Gd.proj d (commaF f)              ≈⟨ introˡ X.identity ⟩
      X.₁ C.id E.∘ ⊤Gd.proj d (commaF f) ≈⟨ K-commute (⊤Gd.limit d) C⇒ ⟩
      ⊤Gd.proj d (commaF g)               ∎
      where
      C⇒ : Comma⇒ (commaF f) (commaF g)
      C⇒ = record
             { h = C.id
             ; commute = DH.begin
               F.₁ C.id D.∘ f   DH.≈⟨ D.∘-resp-≈ F.identity eq ⟩
               D.id D.∘ g       DH.≈⟨ MR.id-comm-sym D  ⟩
               g D.∘ D.id       DH.∎
              }

    ConesGd : {d : D.Obj} → Functor (Comma {A = One} (const d) F) E
    ConesGd {d} = X ∘F Cod {A = One} {B = C} {C = D} (const d) F

    R-identity : {d : D.Obj} → R₁ {d} D.id E.≈ E.id
    R-identity {d} = G.terminal.⊤-id ConeArr
        where
        open E
        module G = Limit (Com (G d))
        ConeArr : Cone⇒ (ConesGd {d}) G.limit G.limit
        ConeArr = record
          { arr = R₁ D.id
          ; commute = λ {Z} → begin
            G.proj Z ∘ R₁ D.id  ≈⟨ proj-red Z D.id ⟩
            G.proj (↙⇒ Z D.id) ≈⟨ proj≈ (D.Equiv.trans D.identityˡ D.identityʳ) ⟩
            G.proj Z            ∎
          }

    R-hom : {Y Z W : D.Obj} {f : D [ Y , Z ]} {g : D [ Z , W ]} → E [ R₁ (D [ g ∘ f ]) ≈ E [ R₁ g ∘ R₁ f ] ]
    R-hom {Y} {Z} {W} {f} {g} = terminal.!-unique₂ (⊤Gd W) {A = cc} {f = f⇒} {g = g⇒}
      where
      module ⊤GY = Cone (⊤Gd.limit Y)
      module H   = Functor (f↙F (g D.∘ f)) using (₀; ₁)
      open E
      cc : Cone (X ∘F Cod (const W) F)
      cc = record { N = ⊤GY.N; apex = record
        { ψ      =  λ K → ⊤GY.ψ (H.₀ K)
        ; commute = λ h → ⊤GY.commute (H.₁ h)
        } }
      f⇒ : Cone⇒ (ConesGd {W}) cc (⊤Gd.terminal.⊤ W)
      f⇒ = record
        { arr = R₁ (g D.∘ f)
        ; commute = λ {K} → proj-red K (g D.∘ f)
        }
      g⇒ : Cone⇒ (ConesGd {W}) cc (⊤Gd.terminal.⊤ W)
      g⇒ = record
        { arr = R₁ g ∘ R₁ f
        ; commute = λ {K} → begin
          ⊤Gd.proj W K ∘ R₁ g ∘ R₁ f        ≈⟨ pullˡ (proj-red K g) ⟩
          ⊤Gd.proj Z (↙⇒ K g) ∘ R₁ f       ≈⟨ proj-red (↙⇒ K g) f ⟩
          ⊤Gd.proj Y (↙⇒ (↙⇒ K g) f)     ≈⟨ proj≈ (D.Equiv.trans D.identityˡ (MR.assoc²' D)) ⟩
          ⊤Gd.proj Y (↙⇒ K (g D.∘ f))      ∎
        }

    R-resp-≈ : {Y Z : D.Obj} {f g : D [ Y , Z ]} → D [ f ≈ g ] → E [ R₁ f ≈ R₁ g ]
    R-resp-≈ {Y} {Z} {f} {g} f≈g = terminal.!-unique₂ (⊤Gd Z) {A = cc} {f = fc} {g = gc}
      where
      open E
      module ⊤GY = Cone (⊤Gd.limit Y)
      module H = Functor (f↙F f)
      cc : Cone (X ∘F Cod (const Z) F)
      cc = record { apex = record
            { ψ       = λ K → ⊤GY.ψ (H.F₀ K)
            ; commute = λ h → ⊤GY.commute (H.F₁ h)
            } }
      F-resp-≈-commute : ∀ {Y Z} {K : Category.Obj (Z ↙ F)} {f g : Y D.⇒ Z} → f D.≈ g →
                           ⊤Gd.proj Z K ∘ R₁ f ≈ ⊤Gd.proj Y (↙⇒ K g)
      F-resp-≈-commute {Y} {Z} {K} {f} {g} eq = begin
        ⊤Gd.proj Z K ∘ R₁ f   ≈⟨ proj-red K f ⟩
        ⊤Gd.proj Y (↙⇒ K f) ≈⟨ proj≈ (D.∘-resp-≈ʳ (D.∘-resp-≈ʳ eq)) ⟩
        ⊤Gd.proj Y (↙⇒ K g) ∎
      fc : Cone⇒ (ConesGd {Z}) cc (⊤Gd.terminal.⊤ Z)
      fc = record
        { arr     = R₁ f
        ; commute = λ {X} → F-resp-≈-commute {Y} {Z} {X} {f} {f} D.Equiv.refl
        }
      gc : Cone⇒ (ConesGd {Z}) cc (⊤Gd.terminal.⊤ Z)
      gc = record
        { arr = R₁ g
        ; commute = λ {X} → F-resp-≈-commute {Y} {Z} {X} {g} {f} (D.Equiv.sym f≈g)
        }

    R : Functor D E
    R = record
      { F₀           = R₀
      ; F₁           = R₁
      ; identity     = λ {d} → R-identity {d}
      ; homomorphism = λ {A B C} {f g} → R-hom {A} {B} {C} {f} {g}
      ; F-resp-≈     = λ {A B} {f g} → R-resp-≈ {A} {B} {f} {g}
      }

    ,Fc : (c : C.Obj) → CommaObj {A = One} {B = C} {C = D} (const (F.₀ c)) F
    ,Fc c = record { β = c ; f = D.id }

    ε : NaturalTransformation (R ∘F F) X
    ε = ntHelper record
      { η       = λ c → ⊤Gd.proj (F.F₀ c) record { f = D.id }
      ; commute = λ {Y Z} f → begin
        ⊤Gd.proj (F.F₀ Z) _ ∘ Functor.F₁ (R ∘F F) f ≈⟨ proj-red _ (F.F₁ f) ⟩
        ⊤Gd.proj (F.F₀ Y) _                         ≈˘⟨ K-commute {C = E} (⊤Gd.limit (F.F₀ Y)) record { h = f ; commute = D.Equiv.sym (D.Equiv.trans (D.∘-resp-≈ˡ D.identityˡ) (D.∘-resp-≈ˡ D.identityˡ)) } ⟩
        X.F₁ f ∘ ⊤Gd.proj (F.F₀ Y) _                ∎
      }
      where open E

{-
    ε : NaturalTransformation (R ∘F F) X
    ε = ntHelper record
      { η       = λ c → ⊤Gd.proj (F.₀ c) (,Fc c)
      ; commute = λ {Y Z} f → let module G = Limit (Com (G (F.₀ Y))) in begin
        ⊤Gd.proj (F.₀ Z) (,Fc Z) E.∘ Functor.F₁ (R ∘F F) f ≈⟨ proj-red (,Fc Z) (F.₁ f) ⟩
        G.proj (↙⇒ (,Fc Z) (F.₁ f))                       ≈˘⟨ K-commute {C = E} {J = Comma (const (F.₀ Y)) F} {F = ConesGd {F.₀ Y}}
                                                                         G.limit (,⇒ f) ⟩
        X.₁ f E.∘ G.proj (,Fc Y)                           ∎
      }
        where
        ,⇒ : {Y Z : C.Obj} (f : Y C.⇒ Z) → Comma⇒ (,Fc Y) (↙⇒ (,Fc Z) (F.₁ f))
        ,⇒ f = record
               { g = _
               ; h = f
               ; commute = DH.begin
                   F.₁ f D.∘ D.id                      DH.≈˘⟨ D.identityˡ DH.⟩∘⟨refl ⟩
                   ((D.id D.∘ F.₁ f) D.∘ D.id)         DH.≈˘⟨ D.identityˡ DH.⟩∘⟨refl ⟩
                    (D.id D.∘ D.id D.∘ F.₁ f) D.∘ D.id DH.∎
               }
-}
    δ-Cone : ∀ d (M : Functor D E) → NaturalTransformation (M ∘F F) X → Cone (G d)
    δ-Cone d M γ = record
      { apex = record
        { ψ       = λ K → γ.η (β K) E.∘ M.₁ (f K)
        ; commute = λ {Y Z} g → begin
          X.₁ (h g) E.∘ γ.η (β Y) E.∘ M.₁ (f Y)          ≈˘⟨ pushˡ (γ.commute (h g)) ⟩
          (γ.η (β Z) E.∘ M.₁ (F.₁ (h g))) E.∘ M.₁ (f Y)  ≈⟨  pullʳ ([ M ]-resp-∘ (D.Equiv.trans (commute g) D.identityʳ))  ⟩
          γ.η (β Z) E.∘ M.₁ (f Z)
            ∎
        }
      }
      where module M = Functor M
            module γ = NaturalTransformation γ
            open CommaObj
            open Comma⇒

    δ : (M : Functor D E) → NaturalTransformation (M ∘F F) X → NaturalTransformation M R
    δ M γ = record
      { η           = λ d → ⊤Gd.rep d (δ-Cone d M γ)
      ; commute     = λ {Y Z} f → terminal.!-unique₂ (⊤Gd Z) {cc f} {q⇒ f} {w⇒ f}
      ; sym-commute = λ {Y Z} f → terminal.!-unique₂ (⊤Gd Z) {cc f} {w⇒ f} {q⇒ f}
      }
      where module M        = Functor M
            module γ        = NaturalTransformation γ
            module δ-Cone d = Cone (δ-Cone d M γ)
            open CommaObj
            cc : {Y Z : D.Obj} → Y D.⇒ Z → Cone (X ∘F Cod (const Z) F)
            cc {_} {Z} f = record
                 { apex = record
                   { ψ       = λ W → δ-Cone.ψ Z W E.∘ M.F₁ f
                   ; commute = λ g → pullˡ (δ-Cone.commute Z g)
                   }
                 }
            q⇒ : {Y Z : D.Obj} → (f : Y D.⇒ Z) → Cone⇒ (ConesGd {Z}) (cc f) (⊤Gd.terminal.⊤ Z)
            q⇒ {Y} {Z} f = record
              { arr     = ⊤Gd.rep Z (δ-Cone Z M γ) E.∘ M.F₁ f
              ; commute = pullˡ (⇒-commute (⊤Gd.rep-cone Z (δ-Cone Z M γ)))
              }
            w⇒ : {Y Z : D.Obj} → (g : Y D.⇒ Z) → Cone⇒ (ConesGd {Z}) (cc g) (⊤Gd.terminal.⊤ Z)
            w⇒ {Y} {Z} g = record
              { arr     = R₁ g E.∘ ⊤Gd.rep Y (δ-Cone Y M γ)
              ; commute = λ {W} → begin
                ⊤Gd.proj Z W E.∘ R₁ g E.∘ ⊤Gd.rep Y (δ-Cone Y M γ)  ≈⟨ pullˡ (proj-red W g) ⟩
                ⊤Gd.proj Y (↙⇒ W g) E.∘ ⊤Gd.rep Y (δ-Cone Y M γ)  ≈⟨ ⇒-commute (⊤Gd.rep-cone Y (δ-Cone Y M γ)) ⟩
                γ.η (β W) E.∘ M.F₁ (D.id D.∘ f W D.∘ g)             ≈˘⟨ refl⟩∘⟨ [ M ]-resp-∘ ( D.Equiv.sym D.identityˡ ) ⟩
                γ.η (β W) E.∘ M.F₁ (f W) E.∘ M.F₁ g                 ≈⟨ E.sym-assoc ⟩
                (γ.η (β W) E.∘ M.F₁ (f W)) E.∘ M.F₁ g               ∎
              }

    δ-unique : ∀ {M : Functor D E} {γ : NaturalTransformation (M ∘F F) X}
                 (δ′ : NaturalTransformation M R) → γ ≊ ε ∘ᵥ δ′ ∘ʳ F → δ′ ≊ δ M γ
    δ-unique {M} {γ} δ′ eq {d} = ⟺ (⊤Gd.terminal.!-unique d C⇒)
      where
      module M = Functor M using (₁)
      module γ = NaturalTransformation γ using (η)
      module δ = NaturalTransformation δ′ using (η; commute)
      open CommaObj
      C⇒ : Cone⇒ (X ∘F Cod (const d) F) (δ-Cone d M γ) (terminal.⊤ (⊤Gd d))
      C⇒ = record
        { arr     = δ.η d
        ; commute = λ {W} → begin
          ⊤Gd.proj d W E.∘ δ.η d                                                   ≈˘⟨ proj≈ (D.Equiv.trans D.identityˡ D.identityˡ)  ⟩∘⟨refl ⟩
          ⊤Gd.proj d (↙⇒ (commaF D.id) (f W)) E.∘ δ.η d                          ≈˘⟨ pullˡ (proj-red (commaF D.id) (f W)) ⟩
          ⊤Gd.proj (F.₀ (β W)) (commaF D.id) E.∘ R₁ (f W) E.∘ δ.η d                ≈˘⟨ pullʳ (δ.commute (f W)) ⟩
          (⊤Gd.proj (F.₀ (β W)) (commaF D.id) E.∘ δ.η (F.₀ (β W))) E.∘ M.₁ (f W)   ≈˘⟨ eq ⟩∘⟨refl ⟩
          γ.η (β W) E.∘ M.₁ (f W)
            ∎
        }

    commutes : (M : Functor D E) (γ : NaturalTransformation (M ∘F F) X) → γ ≊ ε ∘ᵥ δ M γ ∘ʳ F
    commutes M γ {c} = begin
        η γ c                 ≈˘⟨ elimʳ M.identity ⟩
        η γ c E.∘ M.₁ D.id    ≈˘⟨ ⇒-commute (⊤Gd.rep-cone (F.₀ c) (δ-Cone (F.₀ c) M γ)) {,Fc c} ⟩
        η (ε ∘ᵥ δ M γ ∘ʳ F) c ∎
      where
      open NaturalTransformation
      module M  = Functor M using (₁; identity)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------------
-- Test case due to Agda new unifier
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Agda.NewUnifier where

infixl 7 _·_
infixr 5 _∷_
infix 4  _≡_

-- The universe of discourse/universal domain.
postulate D : Set

-- The identity type on the universe of discourse.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

postulate
  _·_  : D → D → D  -- FOTC application.

-- List constants.
postulate [] cons head tail null : D  -- FOTC partial lists.

-- Definitions
abstract
  _∷_  : D → D → D
  x ∷ xs = cons · x · xs

-- The FOTC lists type (inductive predicate for total lists).
data List : D → Set where
  lnil  : List []
  lcons : ∀ x {xs} → List xs → List (x ∷ xs)
{-# ATP axioms lnil lcons #-}

postulate
  _++_  : D → D → D
  ++-[] : ∀ ys → [] ++ ys            ≡ ys
  ++-∷  : ∀ x xs ys → (x ∷ xs) ++ ys ≡ x ∷ (xs ++ ys)
{-# ATP axioms ++-[] ++-∷ #-}

++-List : ∀ {xs ys} → List xs → List ys → List (xs ++ ys)
++-List {ys = ys} lnil Lys = prf
  where postulate prf : List ([] ++ ys)
        {-# ATP prove prf #-}

++-List {ys = ys} (lcons x {xs} Lxs) Lys = prf (++-List Lxs Lys)
  where postulate prf : List (xs ++ ys) → List ((x ∷ xs) ++ ys)
        {-# ATP prove prf #-}


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Monad.Relative where

open import Level

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; Endofunctor; _∘F_) renaming (id to idF)
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (_≃_)
open import Categories.NaturalTransformation.Equivalence
open NaturalIsomorphism

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C : Category o ℓ e
    D : Category o′ ℓ′ e′

record Monad {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (J : Functor C D) : Set (o ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private
    module C = Category C
    module D = Category D
    module J = Functor J
    open D using (_⇒_; _∘_; _≈_)
  field
    F₀ : C.Obj → D.Obj
    unit : {c : C.Obj} → J.₀ c ⇒ F₀ c
    extend : {x y : C.Obj} → (J.₀ x ⇒ F₀ y) → F₀ x ⇒ F₀ y
    identityʳ : {x y : C.Obj} { k : J.₀ x ⇒ F₀ y} → extend k ∘ unit ≈ k
    identityˡ : {x : C.Obj} → extend {x} unit ≈ D.id
    assoc : {x y z : C.Obj} {k : J.₀ x ⇒ F₀ y} {l : J.₀ y ⇒ F₀ z} → extend (extend l ∘ k) ≈ extend l ∘ extend k
    extend-≈ : {x y : C.Obj} {k h : J.₀ x ⇒ F₀ y} → k ≈ h → extend k ≈ extend h

-- From a Relative Monad, we can extract a functor
RMonad⇒Functor : {J : Functor C D} → Monad J → Functor C D
RMonad⇒Functor {C = C} {D = D} {J = J} r = record
  { F₀ = F₀
  ; F₁ = λ f → extend (unit ∘ J.₁ f)
  ; identity = identity′
  ; homomorphism = hom′
  ; F-resp-≈ = λ f≈g → extend-≈ (∘-resp-≈ʳ (J.F-resp-≈ f≈g))
  }
  where
  open Monad r
  module C = Category C
  module D = Category D
  module J = Functor J
  open Category D hiding (identityˡ; identityʳ; assoc)
  open HomReasoning
  open MR D
  identity′ : {c : C.Obj} → extend {c} (unit ∘ J.₁ C.id) ≈ id
  identity′ = begin
     extend (unit ∘ J.₁ C.id) ≈⟨ extend-≈ (elimʳ J.identity) ⟩
     extend unit              ≈⟨ identityˡ ⟩
     id                       ∎
  hom′ : {X Y Z : C.Obj} {f : X C.⇒ Y} {g : Y C.⇒ Z} →
      extend (unit ∘ J.₁ (g C.∘ f)) ≈ extend (unit ∘ J.₁ g) ∘ extend (unit ∘ J.F₁ f)
  hom′ {f = f} {g} = begin
    extend (unit ∘ J.₁ (g C.∘ f))                     ≈⟨ extend-≈ (pushʳ J.homomorphism) ⟩
    extend ((unit ∘ J.₁ g) ∘ J.₁ f)                   ≈⟨ extend-≈ (pushˡ (⟺ identityʳ)) ⟩
    extend (extend (unit ∘ J.₁ g) ∘ (unit ∘ J.F₁ f))  ≈⟨ assoc ⟩
    extend (unit ∘ J.₁ g) ∘ extend (unit ∘ J.F₁ f)    ∎