text:
{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.HITs.SetTruncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level
    A B C D : Type ℓ

rec : isSet B → (A → B) → ∥ A ∥₂ → B
rec Bset f ∣ x ∣₂ = f x
rec Bset f (squash₂ x y p q i j) =
  Bset _ _ (cong (rec Bset f) p) (cong (rec Bset f) q) i j

-- lemma 6.9.1 in HoTT book
elim : {B : ∥ A ∥₂ → Type ℓ}
       (Bset : (x : ∥ A ∥₂) → isSet (B x))
       (g : (a : A) → B (∣ a ∣₂))
       (x : ∥ A ∥₂) → B x
elim Bset g ∣ a ∣₂ = g a
elim Bset g (squash₂ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset _ _
    (cong (elim Bset g) p) (cong (elim Bset g) q) (squash₂ x y p q) i j

setTruncUniversal : isSet B → (∥ A ∥₂ → B) ≃ (A → B)
setTruncUniversal {B = B} Bset =
  isoToEquiv (iso (λ h x → h ∣ x ∣₂) (rec Bset) (λ _ → refl) rinv)
  where
  rinv : (f : ∥ A ∥₂ → B) → rec Bset (λ x → f ∣ x ∣₂) ≡ f
  rinv f i x =
    elim (λ x → isProp→isSet (Bset (rec Bset (λ x → f ∣ x ∣₂) x) (f x)))
         (λ _ → refl) x i

elim2 : {B : ∥ A ∥₂ → ∥ A ∥₂ → Type ℓ}
        (Bset : ((x y : ∥ A ∥₂) → isSet (B x y)))
        (g : (a b : A) → B ∣ a ∣₂ ∣ b ∣₂)
        (x y : ∥ A ∥₂) → B x y
elim2 Bset g = elim (λ _ → isSetΠ (λ _ → Bset _ _))
                    (λ a → elim (λ _ → Bset _ _) (g a))

elim3 : {B : (x y z : ∥ A ∥₂) → Type ℓ}
        (Bset : ((x y z : ∥ A ∥₂) → isSet (B x y z)))
        (g : (a b c : A) → B ∣ a ∣₂ ∣ b ∣₂ ∣ c ∣₂)
        (x y z : ∥ A ∥₂) → B x y z
elim3 Bset g = elim2 (λ _ _ → isSetΠ (λ _ → Bset _ _ _))
                     (λ a b → elim (λ _ → Bset _ _ _) (g a b))

setTruncIsSet : isSet ∥ A ∥₂
setTruncIsSet a b p q = squash₂ a b p q

setTruncIdempotent≃ : isSet A → ∥ A ∥₂ ≃ A
setTruncIdempotent≃ {A = A} hA = isoToEquiv f
  where
  f : Iso ∥ A ∥₂ A
  Iso.fun f = rec hA (idfun A)
  Iso.inv f x = ∣ x ∣₂
  Iso.rightInv f _ = refl
  Iso.leftInv f = elim (λ _ → isSet→isGroupoid setTruncIsSet _ _) (λ _ → refl)

setTruncIdempotent : isSet A → ∥ A ∥₂ ≡ A
setTruncIdempotent hA = ua (setTruncIdempotent≃ hA)

isContr→isContrSetTrunc : isContr A → isContr (∥ A ∥₂)
isContr→isContrSetTrunc contr = ∣ fst contr ∣₂
                                , elim (λ _ → isOfHLevelPath 2 (setTruncIsSet) _ _)
                                       λ a → cong ∣_∣₂ (snd contr a)

setTruncIso : Iso A B → Iso ∥ A ∥₂ ∥ B ∥₂
Iso.fun (setTruncIso is) = rec setTruncIsSet (λ x → ∣ Iso.fun is x ∣₂)
Iso.inv (setTruncIso is) = rec setTruncIsSet (λ x → ∣ Iso.inv is x ∣₂)
Iso.rightInv (setTruncIso is) =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ a → cong ∣_∣₂ (Iso.rightInv is a)
Iso.leftInv (setTruncIso is) =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ a → cong ∣_∣₂ (Iso.leftInv is a)

setSigmaIso : ∀ {ℓ} {B : A → Type ℓ} → Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
setSigmaIso {A = A} {B = B} = iso fun funinv sect retr
  where
  {- writing it out explicitly to avoid yellow highlighting -}
  fun : ∥ Σ A B ∥₂ → ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂
  fun = rec setTruncIsSet λ {(a , p) → ∣ a , ∣ p ∣₂ ∣₂}
  funinv : ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂ → ∥ Σ A B ∥₂
  funinv = rec setTruncIsSet (λ {(a , p) → rec setTruncIsSet (λ p → ∣ a , p ∣₂) p})
  sect : section fun funinv
  sect = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { (a , p) → elim {B = λ p → fun (funinv ∣ a , p ∣₂) ≡ ∣ a , p ∣₂}
              (λ p → isOfHLevelPath 2 setTruncIsSet _ _) (λ _ → refl) p }
  retr : retract fun funinv
  retr = elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
              λ { _ → refl }

sigmaElim : ∀ {ℓ ℓ'} {B : ∥ A ∥₂ → Type ℓ} {C : Σ ∥ A ∥₂ B  → Type ℓ'}
            (Bset : (x : Σ ∥ A ∥₂ B) → isSet (C x))
            (g : (a : A) (b : B ∣ a ∣₂) → C (∣ a ∣₂ , b))
            (x : Σ ∥ A ∥₂ B) → C x
sigmaElim {B = B} {C = C} set g (x , y) = elim {B = λ x → (y : B x) → C (x , y)}
                                               (λ _ → isOfHLevelΠ 2 λ _ → set (_ , _))
                                               g x y

sigmaProdElim : ∀ {ℓ ℓ'} {C : ∥ A ∥₂ × ∥ B ∥₂ → Type ℓ} {D : Σ (∥ A ∥₂ × ∥ B ∥₂) C  → Type ℓ'}
             (Bset : (x : Σ (∥ A ∥₂ × ∥ B ∥₂) C) → isSet (D x))
             (g : (a : A) (b : B) (c : C (∣ a ∣₂ , ∣ b ∣₂)) → D ((∣ a ∣₂ , ∣ b ∣₂) , c))
             (x : Σ (∥ A ∥₂ × ∥ B ∥₂) C) → D x
sigmaProdElim {B = B} {C = C} {D = D} set g ((x , y) , c) =
  elim {B = λ x → (y : ∥ B ∥₂) (c : C (x , y)) → D ((x , y) , c)}
       (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → set _)
       (λ x → elim (λ _ → isOfHLevelΠ 2 λ _ → set _)
                    λ y c → g x y c)
       x y c

prodElim : ∀ {ℓ} {C : ∥ A ∥₂ × ∥ B ∥₂ → Type ℓ}
        → ((x : ∥ A ∥₂ × ∥ B ∥₂) → isOfHLevel 2 (C x))
        → ((a : A) (b : B) → C (∣ a ∣₂ , ∣ b ∣₂))
        → (x : ∥ A ∥₂ × ∥ B ∥₂) → C x
prodElim {A = A} {B = B} {C = C} hlevel ind (a , b) = schonf a b
  where
  schonf : (a : ∥ A ∥₂) (b : ∥ B ∥₂) → C (a , b)
  schonf = elim (λ x → isOfHLevelΠ 2 λ y → hlevel (_ , _)) λ a → elim (λ x → hlevel (_ , _))
                 λ b → ind a b

prodElim2 : ∀ {ℓ} {E : (∥ A ∥₂ × ∥ B ∥₂) → (∥ C ∥₂ × ∥ D ∥₂) → Type ℓ}
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) (y : ∥ C ∥₂ × ∥ D ∥₂) → isOfHLevel 2 (E x y))
         → ((a : A) (b : B) (c : C) (d : D) → E (∣ a ∣₂ , ∣ b ∣₂) (∣ c ∣₂ , ∣ d ∣₂))
         → ((x : ∥ A ∥₂ × ∥ B ∥₂) (y : ∥ C ∥₂ × ∥ D ∥₂) → (E x y))
prodElim2 isset f = prodElim (λ _ → isOfHLevelΠ 2 λ _ → isset _ _)
                             λ a b → prodElim (λ _ → isset _ _)
                                     λ c d → f a b c d

setTruncOfProdIso :  Iso ∥ A × B ∥₂ (∥ A ∥₂ × ∥ B ∥₂)
Iso.fun setTruncOfProdIso = rec (isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet)) λ { (a , b) → ∣ a ∣₂ , ∣ b ∣₂ }
Iso.inv setTruncOfProdIso = prodElim (λ _ → setTruncIsSet) λ a b → ∣ a , b ∣₂
Iso.rightInv setTruncOfProdIso =
  prodElim (λ _ → isOfHLevelPath 2 (isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet)) _ _)
           λ _ _ → refl
Iso.leftInv setTruncOfProdIso =
  elim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ {(a , b) → refl}

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
{-# OPTIONS --cubical --safe --no-import-sorts #-}

module Cubical.HITs.Delooping.Two.Properties where

open import Cubical.Functions.Involution

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.Data.Bool
open import Cubical.Data.Empty
open import Cubical.Data.Unit

open import Cubical.HITs.Delooping.Two.Base
open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ : Level

module Embed where
  isSetIsPropDep : isOfHLevelDep {ℓ' = ℓ} 1 isSet
  isSetIsPropDep = isOfHLevel→isOfHLevelDep 1 (λ _ → isPropIsSet)

  notSet : PathP (λ i → isSet (notEq i)) isSetBool isSetBool
  notSet = isSetIsPropDep isSetBool isSetBool notEq

  notNot² : Square notEq refl refl notEq
  notNot² = involPath² notnot

  notNotSet
    : SquareP (λ i j → isSet (notNot² i j)) notSet refl refl notSet
  notNotSet = isPropDep→isSetDep'
                isSetIsPropDep
                (involPath² notnot)
                notSet refl refl notSet

  Code : Bℤ₂ → hSet ℓ-zero
  Code = Elim.rec
    (Bool , isSetBool)
    (λ i → notEq i , notSet i)
    (λ i j → λ where
      .fst → notNot² i j
      .snd → notNotSet i j)
    (isOfHLevelTypeOfHLevel 2)

  El : Bℤ₂ → Type₀
  El b = Code b .fst

module BINARY where
  open import Cubical.Data.FinSet.Binary.Large

  sem : Bℤ₂ → Binary _
  sem = Elim.rec Base Loop Loop² isGroupoidBinary

  loop? : Bool → base ≡ base
  loop? false = refl
  loop?  true = loop

  Loop²-coh : (a b c : Bool) → Type₀
  Loop²-coh false false false = Unit
  Loop²-coh false  true  true = Unit
  Loop²-coh  true false  true = Unit
  Loop²-coh  true  true false = Unit
  Loop²-coh     _     _     _ = ⊥

  rf : Bool ≡ Bool → Bool
  rf P = transport P false

  Loop²-coh-lemma₀
    : ∀(p q r : Bool)
    → r ⊕ p ≡ q
    → Loop²-coh p q r
  Loop²-coh-lemma₀ false false false sq = _
  Loop²-coh-lemma₀ false  true  true sq = _
  Loop²-coh-lemma₀  true false  true sq = _
  Loop²-coh-lemma₀  true  true false sq = _
  Loop²-coh-lemma₀ false  true false = false≢true
  Loop²-coh-lemma₀ false false  true = true≢false
  Loop²-coh-lemma₀  true false false = true≢false
  Loop²-coh-lemma₀  true  true  true = false≢true

  Loop²-coh-lemma
    : ∀(P Q R : Bool ≡ Bool)
    → Square P Q refl R
    → Loop²-coh (rf P) (rf Q) (rf R)
  Loop²-coh-lemma P Q R sq = Loop²-coh-lemma₀ p q r eqn
    where
    p = rf P
    q = rf Q
    r = rf R

    open BoolReflection

    cmp : P ∙ R ≡ Q
    cmp i j
      = hcomp (λ k → λ where
            (i = i0) → compPath-filler P R k j
            (i = i1) → Q j
            (j = i0) → Bool
            (j = i1) → R (i ∨ k))
          (sq i j)

    rcmp : ⊕-Path (r ⊕ p) ≡ ⊕-Path q
    rcmp = ⊕-Path (r ⊕ p)
             ≡[ i ]⟨ ⊕-comp p r (~ i) ⟩
           ⊕-Path p ∙ ⊕-Path r
             ≡[ i ]⟨ ⊕-complete P (~ i) ∙ ⊕-complete R (~ i) ⟩
           P ∙ R
             ≡⟨ cmp ⟩
           Q
             ≡⟨ ⊕-complete Q ⟩
           ⊕-Path q ∎
    open Iso
    eqn : r ⊕ p ≡ q
    eqn = transport (λ i →
              reflectIso .leftInv (r ⊕ p) i ≡ reflectIso .leftInv q i)
            (cong (reflectIso .inv) rcmp)

  loop²?
    : ∀ p q r → Loop²-coh p q r
    → Square (loop? p) (loop? q) refl (loop? r)
  loop²? false false false _ = refl
  loop²? false  true  true _ = λ i j → loop (i ∧ j)
  loop²?  true false  true _ = loop²
  loop²?  true  true false _ = refl

  module _ (B : Type₀) where
    based : (P : Bool ≃ B) → Bℤ₂
    based _ = base

    pull₀ : (P Q : Bool ≃ B) → Bool ≡ Bool
    pull₀ P Q i
      = hcomp (λ k → λ where
            (i = i0) → ua P (~ k)
            (i = i1) → ua Q (~ k))
          B

    pull₁ : (P Q : Bool ≃ B) → Square (ua P) (ua Q) (pull₀ P Q) refl
    pull₁ P Q i j
      = hcomp (λ k → λ where
            (i = i0) → ua P (~ k ∨ j)
            (i = i1) → ua Q (~ k ∨ j)
            (j = i1) → B)
          B

    pull₂
      : (P Q R : Bool ≃ B)
      → Square (pull₀ P Q) (pull₀ P R) refl (pull₀ Q R)
    pull₂ P Q R i j
      = hcomp (λ k → λ where
            (j = i0) → ua P (~ k)
            (i = i0) (j = i1) → ua Q (~ k)
            (i = i1) (j = i1) → ua R (~ k))
          B

    pull₃
      : (P Q R : Bool ≃ B)
      → Cube (pull₁ P Q) (pull₁ P R)
            (λ _ → ua P)  (pull₁ Q R)
            (pull₂ P Q R) (λ _ _ → B)
    pull₃ P Q R i j k
      = hcomp (λ τ → λ where
            (j = i0) → ua P (~ τ ∨ k)
            (i = i0) (j = i1) → ua Q (~ τ ∨ k)
            (i = i1) (j = i1) → ua R (~ τ ∨ k)
            (k = i1) → B)
          B

    looped : (P Q : Bool ≃ B) → based P ≡ based Q
    looped P Q = loop? b
      where
      b : Bool
      b = rf (pull₀ P Q)

    looped²
      : (P Q R : Bool ≃ B)
      → Square (looped P Q) (looped P R) refl (looped Q R)
    looped² P Q R = loop²? pq pr qr pqr
      where
      pq = rf (pull₀ P Q)
      pr = rf (pull₀ P R)
      qr = rf (pull₀ Q R)

      pqr : Loop²-coh pq pr qr
      pqr = Loop²-coh-lemma (pull₀ P Q) (pull₀ P R) (pull₀ Q R) (pull₂ P Q R)

  syn : Binary _ → Bℤ₂
  syn (B , tP) = rec→Gpd trunc (based B) 3k tP
    where
    open 3-Constant
    3k : 3-Constant (based B)
    3k .link = looped B
    3k .coh₁ = looped² B

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
----------------------------------------------------------------------
-- A monad with partiality and failure
----------------------------------------------------------------------

module PartialityAndFailure where

open import Category.Monad
open import Codata.Musical.Notation
open import Category.Monad.Partiality as Partiality using (_⊥)
open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe)
open import Data.Maybe.Categorical as MaybeC using ()
open import Level using (_⊔_)
open import Function
open import Relation.Binary as B hiding (Rel)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Danielsson's partiality-and-failure monad.

-- The definitions below are slightly modified versions of those given
-- in the code accompanying Danielsson's ICFP'12 paper "Operational
-- Semantics Using the Partiality Monad".  The original version along
-- with additional explanations can be found at
--
--   http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.html

_?⊥ : ∀ {a} → Set a → Set a
A ?⊥ = Maybe A ⊥

monad : ∀ {f} → RawMonad {f = f} (_⊥ ∘ Maybe)
monad = MaybeC.monadT Partiality.monad

private module M {f} = RawMonad (monad {f})

-- Re-export constructors and kinds of relations.
open Partiality public
  using (now; later; Kind; OtherKind; geq; weak; strong; other)

-- Failure.
private
  -- This module encapsulates fail so we can define/overload it as a
  -- constructor of _?⊥P and RelP in the Workaround and
  -- AlternativeEquality modules below.  Its definitions will be
  -- re-exported at the global scope later.
  module Failure {a} where

    fail : ∀ {A : Set a} → A ?⊥
    fail = now nothing

    infix 7 _or-fail

    _or-fail : ∀ {A B : Set a} → (A → B ?⊥) → Maybe A → B ?⊥
    f or-fail = maybe f fail

------------------------------------------------------------------------
-- Equality/ordering

-- The default equality for the partiality monad (bisimilarity)
-- specialized to include failure and with the underlying equality
-- fixed to "syntactic" equality (_≡_).

module Equality {a} {A : Set a} where
  open M using (_>>=_)
  private module E = Partiality.Equality (_≡_ {A = Maybe A})
  open E public using (now; later; laterʳ; laterˡ)

  infix 4 _≅_ _≳_ _≲_ _≈_

  -- The three relations specialized to include failure and with the
  -- underlying equality fixed to "syntactic" equality (_≡_).
  Rel : Kind → A ?⊥ → A ?⊥ → Set _
  Rel k x y = E.Rel k x y

  _≅_ = Rel strong
  _≳_ = Rel (other geq)
  _≲_ = flip _≳_
  _≈_ = Rel (other weak)

  fail : ∀ {k} → Rel k (Failure.fail) (Failure.fail)
  fail = now P.refl

------------------------------------------------------------------------
-- The (specialized) relations are equivalences or partial orders
-- for the chosen underlying "syntactic" equality (_≡_)

module Equivalence {a} {A : Set a} where
  open Partiality.Equivalence {A = Maybe A} {_∼_ = _≡_} public

-- Equational reasoning with the underlying equality fixed to
-- "syntactic" equality (_≡_).
module Reasoning {a} {A : Set a} where
  open Partiality.Reasoning (P.isEquivalence {A = Maybe A}) public

------------------------------------------------------------------------
-- Laws related to bind

module _ {a} {A B : Set a} where
  open Failure
  open Equality
  open M using (_>>=_)

  infixl 1 _>>=-cong_

  -- Bind preserves all the relations.
  _>>=-cong_ : ∀ {k} {x₁ x₂} {f₁ f₂ : A → B ?⊥} →
               Rel k x₁ x₂ → (∀ x → Rel k (f₁ x) (f₂ x)) →
               Rel k (x₁ >>= f₁) (x₂ >>= f₂)
  _>>=-cong_ {k} {f₁ = f₁} {f₂} x₁≈x₂ f₁≈f₂ =
    x₁≈x₂ Partiality.>>=-cong helper
    where
      helper : ∀ {x y} → x ≡ y → Rel k ((f₁ or-fail) x) ((f₂ or-fail) y)
      helper {x = nothing} P.refl = now P.refl
      helper {x = just x}  P.refl = f₁≈f₂ x

------------------------------------------------------------------------
-- Productivity checker workaround

-- Just like the partiality monad, the partiality-and-fail monad
-- suffers from the limitations of guarded coinduction.  Luckily there
-- is a (limited) workaround for this problem, namely to extend the
-- datatype _?⊥ with a _>>=_ constructor, yielding an embedded
-- language _?⊥P (of _?⊥ "programs") which internalizes the monadic
-- bind operation.  When writing corecursive functions in _?⊥P, one
-- may use _>>=_ without guarding it with other constructors.  By
-- interpreting the resulting programs in _?⊥, one recovers the
-- desired corecursive function.  For details, see e.g. Danielsson's
-- PAR'10 paper "Beating the Productivity Checker Using Embedded
-- Languages".

module Workaround {a} where
  private module W = Partiality.Workaround {a}

  infixl 1 _>>=_

  -- The language of _?⊥ "programs" internalizing _>>=_.
  data _?⊥P : Set a → Set (Level.suc a) where
    return : ∀ {A}   (x : A)                     → A ?⊥P
    later  : ∀ {A}   (x : ∞ (A ?⊥P))             → A ?⊥P
    fail   : ∀ {A}                               → A ?⊥P
    _>>=_  : ∀ {A B} (x : A ?⊥P) (f : A → B ?⊥P) → B ?⊥P

  private

    mutual

      -- Translation of _?⊥ programs to _⊥ programs.
      ⟦_⟧P′ : ∀ {A} → A ?⊥P → (Maybe A) W.⊥P
      ⟦ return x          ⟧P′ = W.now (just x)
      ⟦ later x           ⟧P′ = W.later (♯ ⟦ (♭ x) ⟧P′)
      ⟦ fail              ⟧P′ = W.now nothing
      ⟦ _>>=_ {A} {B} x f ⟧P′ = ⟦ x ⟧P′ W.>>= ⟦>>=⟧-helper f

      ⟦>>=⟧-helper : ∀ {A B : Set a} → (A → B ?⊥P) → Maybe A → (Maybe B) W.⊥P
      ⟦>>=⟧-helper f (just y) = ⟦ f y ⟧P′
      ⟦>>=⟧-helper _ nothing  = W.now nothing

  -- Interpretation of _?⊥ programs in _?⊥.
  ⟦_⟧P : ∀ {A} → A ?⊥P → A ?⊥
  ⟦_⟧P = W.⟦_⟧P ∘ ⟦_⟧P′

  -- The definitions above make sense. ⟦_⟧P is homomorphic with
  -- respect to now, later, fail and _>>=_.
  module Correct where
    open Equality {a} hiding (fail)
    open Reasoning {a}
    private
      module F      = Failure {a}
      module PM {f} = RawMonad (Partiality.monad {f})

    return-hom : ∀ {A} (x : A) → ⟦ return x ⟧P ≅ M.return x
    return-hom x = M.return x ∎

    later-hom : ∀ {A} (x : ∞ (A ?⊥P)) → ⟦ later x ⟧P ≅ later (♯ ⟦ ♭ x ⟧P)
    later-hom x = later (♯ (⟦ ♭ x ⟧P ∎) )

    fail-hom : ∀ {A} → ⟦ fail {A} ⟧P ≅ F.fail {A}
    fail-hom {A} = F.fail {A} ∎

    >>=-hom : ∀ {A B} (x : A ?⊥P) (f : A → B ?⊥P) →
              ⟦ x >>= f ⟧P ≅ (⟦ x ⟧P M.>>= λ y → ⟦ f y ⟧P)
    >>=-hom {A} {B} x f =
        W.⟦ ⟦ x ⟧P′ W.>>= (⟦>>=⟧-helper f) ⟧P
      ≅⟨ W.Correct.>>=-hom ⟦ x ⟧P′ _ ⟩
        (⟦ x ⟧P PM.>>= λ y → W.⟦ ⟦>>=⟧-helper f y ⟧P)
      ≅⟨ (⟦ x ⟧P ∎) Partiality.≡->>=-cong helper ⟩
        (⟦ x ⟧P PM.>>= maybe (⟦_⟧P ∘ f) F.fail)
      ∎
      where
        helper : ∀ y → W.⟦ ⟦>>=⟧-helper f y ⟧P ≅ maybe (⟦_⟧P ∘ f) F.fail y
        helper (just y) = ⟦ f y ⟧P ∎
        helper nothing  = F.fail ∎

------------------------------------------------------------------------
-- An alternative, but equivalent, formulation of equality/ordering

-- This version of equality works around some limitations of guarded
-- corecursion and is therefore easier to use in corecursive proofs.
-- However, it does not admit unrestricted use of transitivity.  For a
-- discussion of the technique and the related issues, see e.g.
--
--  * "Operational Semantics Using the Partiality Monad", Danielsson,
--    ICFP'12
--
--  * "Beating the Productivity Checker Using Embedded Languages",
--    Danielsson, PAR'10
--
--  * "Subtyping, Declaratively -- An Exercise in Mixed Induction and
--    Coinduction", Danielsson and Altenkirch, MPC'10
--
-- All of the above can be found at
--   http://www.cse.chalmers.se/~nad/publications/

module AlternativeEquality {a} where
  open Equality {a} hiding (fail)
  private
    open module F = Failure {a} hiding (fail)
    module AE = Partiality.AlternativeEquality {a}

  mutual
    -- Proof "programs" with the underlying equality fixed to
    -- "syntactic" equality (_≡_) and extended to include failure.

    infix  4 _≅P_ _≳P_ _≈P_
    infix  3 _∎
    infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≳⟨_⟩≅_ _≳⟨_⟩≈_ _≈⟨_⟩≅_ _≈⟨_⟩≲_
    infixl 1 _>>=_

    _≅P_ : ∀ {A} → B.Rel (A ?⊥) _
    _≅P_ = RelP strong

    _≳P_ : ∀ {A} → B.Rel (A ?⊥) _
    _≳P_ = RelP (other geq)

    _≈P_ : ∀ {A} → B.Rel (A ?⊥) _
    _≈P_ = RelP (other weak)

    data RelP {A : Set a} : Kind → B.Rel (A ?⊥) (Level.suc a) where

      -- Congruences.

      return : ∀ {k x y} (x≡y : x ≡ y) →
               RelP k (M.return x) (M.return y)
      later  : ∀ {k x y} (x∼y : ∞ (RelP k (♭ x) (♭ y))) →
               RelP k (later x) (later y)
      fail   : ∀ {k} → RelP k (F.fail) (F.fail)
      _>>=_  : ∀ {B : Set a} {k x₁ x₂} {f₁ f₂ : B → A ?⊥} →
               let open M in
               (x₁≡x₂ : RelP k x₁ x₂)
               (f₁∼f₂ : ∀ x → RelP k (f₁ x) (f₂ x)) →
               RelP k (x₁ >>= f₁) (x₂ >>= f₂)

      -- Ordering/weak equality.

      laterʳ : ∀ {x y} (x≈y : RelP (other weak) x (♭ y)) →
               RelP (other weak) x (later y)
      laterˡ : ∀ {k x y} (x∼y : RelP (other k) (♭ x) y) →
               RelP (other k) (later x) y

      -- Equational reasoning. Note that including full transitivity
      -- for weak equality would make _≈P_ trivial; a similar problem
      -- applies to _≳P_ (never ≳P return x would be
      -- provable). Instead the definition of RelP includes limited
      -- notions of transitivity, similar to weak bisimulation up-to
      -- various things.

      _∎      : ∀ {k} x → RelP k x x
      sym     : ∀ {k x y} {eq : Partiality.Equality k} (x∼y : RelP k x y) →
                RelP k y x
      _≡⟨_⟩_  : ∀ {k} x {y z} (x≡y : x ≡ y)  (y∼z : RelP k y z) → RelP k x z
      _≅⟨_⟩_  : ∀ {k} x {y z} (x≅y : x ≅P y) (y∼z : RelP k y z) → RelP k x z
      _≳⟨_⟩_  : ∀     x {y z} (x≳y : x ≳  y) (y≳z : y ≳P z) → x ≳P z
      _≳⟨_⟩≅_ : ∀     x {y z} (x≳y : x ≳P y) (y≅z : y ≅P z) → x ≳P z
      _≳⟨_⟩≈_ : ∀     x {y z} (x≳y : x ≳P y) (y≈z : y ≈P z) → x ≈P z
      _≈⟨_⟩≅_ : ∀     x {y z} (x≈y : x ≈P y) (y≅z : y ≅P z) → x ≈P z
      _≈⟨_⟩≲_ : ∀     x {y z} (x≈y : x ≈P y) (y≲z : z ≳P y) → x ≈P z

      -- If any of the following transitivity-like rules were added to
      -- RelP, then RelP and Rel would no longer be equivalent:
      --
      --   x ≳P y → y ≳P z → x ≳P z
      --   x ≳P y → y ≳  z → x ≳P z
      --   x ≲P y → y ≈P z → x ≈P z
      --   x ≈P y → y ≳P z → x ≈P z
      --   x ≲  y → y ≈P z → x ≈P z
      --   x ≈P y → y ≳  z → x ≈P z
      --   x ≈P y → y ≈P z → x ≈P z
      --   x ≈P y → y ≈  z → x ≈P z
      --   x ≈  y → y ≈P z → x ≈P z
      --
      -- The reason is that any of these rules would make it possible
      -- to derive that never and now x are related.

  -- RelP is complete with respect to Rel.
  complete : ∀ {A k} {x y : A ?⊥} → Rel k x y → RelP k x y
  complete {x = now (just x)} {now (just .x)} (now P.refl) = return P.refl
  complete {x = now (just x)} {now nothing}   (now ())
  complete {x = now nothing}  {now (just _)}  (now ())
  complete {x = now nothing}  {now nothing}   (now P.refl) = fail
  complete (later  x∼y) = later (♯ complete (♭ x∼y))
  complete (laterʳ x≈y) = laterʳ  (complete    x≈y)
  complete (laterˡ x∼y) = laterˡ  (complete    x∼y)

  private
    AE-RelP : ∀ {A : Set a} → Kind → B.Rel (A ?⊥) _
    AE-RelP {A} = AE.RelP (P.setoid (Maybe A))

    -- RelP is sound with respect to the alternative equality of the
    -- partiality monad.
    sound′ : ∀ {A k} {x y : A ?⊥} → RelP k x y → AE-RelP k x y
    sound′ (return x≡y)      = AE.now (P.cong just x≡y)
    sound′ (later x∼y)       = AE.later (♯ sound′ (♭ x∼y))
    sound′ fail              = AE.now P.refl
    sound′ {A} {k} (_>>=_ {B} {f₁ = f₁} {f₂} x f₁∼f₂) =
      sound′ x AE.>>= helper
      where
        helper : ∀ {x y} → x ≡ y → AE-RelP k ((f₁ or-fail) x) ((f₂ or-fail) y)
        helper {x = nothing} P.refl = AE.now P.refl
        helper {x = just x}  P.refl = sound′ (f₁∼f₂ x)
    sound′ (laterʳ x)        = AE.laterʳ (sound′ x)
    sound′ (laterˡ x)        = AE.laterˡ (sound′ x)
    sound′ (x ∎)             = x AE.∎
    sound′ (sym {eq = eq} x) = AE.sym {eq = eq} (sound′ x)
    sound′ (x ≡⟨ x≡y ⟩ y≡z)  = AE._≡⟨_⟩_  x x≡y          (sound′ y≡z)
    sound′ (x ≅⟨ x≅y ⟩ y≅z)  = AE._≅⟨_⟩_  x (sound′ x≅y) (sound′ y≅z)
    sound′ (x ≳⟨ x≳y ⟩ y≳z)  = AE._≳⟨_⟩_  x x≳y          (sound′ y≳z)
    sound′ (x ≳⟨ x≳y ⟩≅ y≅z) = AE._≳⟨_⟩≅_ x (sound′ x≳y) (sound′ y≅z)
    sound′ (x ≳⟨ x≳y ⟩≈ y≈z) = AE._≳⟨_⟩≈_ x (sound′ x≳y) (sound′ y≈z)
    sound′ (x ≈⟨ x≈y ⟩≅ y≅z) = AE._≈⟨_⟩≅_ x (sound′ x≈y) (sound′ y≅z)
    sound′ (x ≈⟨ x≈y ⟩≲ y≲z) = AE._≈⟨_⟩≲_ x (sound′ x≈y) (sound′ y≲z)

  -- RelP is sound with respect to Rel.
  sound : ∀ {A k} {x y : A ?⊥} → RelP k x y → Rel k x y
  sound = AE.sound ∘ sound′

open Failure public

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflexive closures
------------------------------------------------------------------------

module Data.ReflexiveClosure where

open import Data.Unit
open import Level
open import Relation.Binary
open import Relation.Binary.Simple

------------------------------------------------------------------------
-- Reflexive closure

data Refl {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  [_]  : ∀ {x y} (x∼y : x ∼ y) → Refl _∼_ x y
  refl : Reflexive (Refl _∼_)

-- Map.

map : ∀ {a a′ ℓ ℓ′} {A : Set a} {A′ : Set a′}
        {_R_ : Rel A ℓ} {_R′_ : Rel A′ ℓ′} {f : A → A′} →
      _R_ =[ f ]⇒ _R′_ → Refl _R_ =[ f ]⇒ Refl _R′_
map R⇒R′ [ xRy ] = [ R⇒R′ xRy ]
map R⇒R′ refl    = refl

-- The reflexive closure has no effect on reflexive relations.

drop-refl : ∀ {a ℓ} {A : Set a} {_R_ : Rel A ℓ} →
            Reflexive _R_ → Refl _R_ ⇒ _R_
drop-refl rfl [ x∼y ] = x∼y
drop-refl rfl refl    = rfl

------------------------------------------------------------------------
-- Example: Maybe

module Maybe where

  Maybe : ∀ {ℓ} → Set ℓ → Set ℓ
  Maybe A = Refl (Const A) tt tt

  nothing : ∀ {a} {A : Set a} → Maybe A
  nothing = refl

  just : ∀ {a} {A : Set a} → A → Maybe A
  just = [_]


text:
{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-}

{-
  Kan extension of a functor C → D to a functor PreShv C ℓ → PreShv D ℓ left or right adjoint to
  precomposition.
-}

module Cubical.Categories.Presheaf.KanExtension where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Functions.FunExtEquiv

open import Cubical.HITs.SetQuotients

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Adjoint
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Instances.Sets

{-
  Left Kan extension of a functor C → D to a functor PreShv C ℓ → PreShv D ℓ left adjoint to precomposition.
-}

module Lan {ℓC ℓC' ℓD ℓD'} ℓS
  {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'}
  (F : Functor C D)
  where

  open Functor
  open NatTrans

  private
    module C = Precategory C
    module D = Precategory D

    {-
      We want the category SET ℓ we're mapping into to be large enough that the coend will take presheaves
      Cᵒᵖ → Set ℓ to presheaves Dᵒᵖ → Set ℓ, otherwise we get no adjunction with precomposition.
      So we must have ℓC,ℓC',ℓD' ≤ ℓ; the parameter ℓS allows ℓ to be larger than their maximum.
    -}
    ℓ = ℓ-max (ℓ-max (ℓ-max ℓC ℓC') ℓD') ℓS

  module _ (G : Functor (C ^op) (SET ℓ)) where

    -- Definition of the coend

    module _ (d : D.ob) where

      Raw : Type ℓ
      Raw = Σ[ c ∈ C.ob ] Σ[ g ∈ D.Hom[ d , F ⟅ c ⟆ ] ] G .F-ob c .fst

      data _≈_ : (u v : Raw) → Type ℓ where
        shift : {c c' : C.ob} (g : D.Hom[ d , F ⟅ c ⟆ ]) (f : C.Hom[ c , c' ]) (a : (G ⟅ c' ⟆) .fst)
          → (c' , (g D.⋆ F ⟪ f ⟫) , a) ≈ (c , g , (G ⟪ f ⟫) a)

      Quo = Raw / _≈_

    pattern shift/ g f a i = eq/ _ _ (shift g f a) i

    -- Action of Quo on arrows in D

    mapR : {d d' : D.ob} (h : D.Hom[ d' , d ]) → Quo d → Quo d'
    mapR h [ c , g , a ] = [ c , h D.⋆ g , a ]
    mapR h (shift/ g f a i) =
      hcomp
        (λ j → λ
          { (i = i0) → [ _ , D.⋆Assoc h g (F ⟪ f ⟫) j , a ]
          ; (i = i1) → [ _ , h D.⋆ g , (G ⟪ f ⟫) a ]
          })
        (shift/ (h D.⋆ g) f a i)
    mapR h (squash/ t u p q i j) =
      squash/ (mapR h t) (mapR h u) (cong (mapR h) p) (cong (mapR h) q) i j

    mapRId : (d : D.ob) → mapR (D.id d) ≡ (idfun _)
    mapRId d =
      funExt (elimProp (λ _ → squash/ _ _) (λ (c , g , a) i → [ c , D.⋆IdL g i , a ]))

    mapR∘ : {d d' d'' : D.ob}
      (h' : D.Hom[ d'' , d' ]) (h : D.Hom[ d' , d ])
      → mapR (h' D.⋆ h) ≡ mapR h' ∘ mapR h
    mapR∘ h' h =
      funExt (elimProp (λ _ → squash/ _ _) (λ (c , g , a) i → [ c , D.⋆Assoc h' h g i , a ]))

  LanOb : Functor (C ^op) (SET ℓ) → Functor (D ^op) (SET _)
  LanOb G .F-ob d .fst = Quo G d
  LanOb G .F-ob d .snd = squash/
  LanOb G .F-hom = mapR G
  LanOb G .F-id {d} = mapRId G d
  LanOb G .F-seq h h' = mapR∘ G h' h

  -- Action of Quo on arrows in Cᵒᵖ → Set

  module _ {G G' : Functor (C ^op) (SET ℓ)} (α : NatTrans G G') where

    mapL : (d : D.ob) → Quo G d → Quo G' d
    mapL d [ c , g , a ] = [ c , g , α .N-ob c a ]
    mapL d (shift/ g f a i) =
      hcomp
        (λ j → λ
          { (i = i0) → [ _ , (g D.⋆ F ⟪ f ⟫) , α .N-ob _ a ]
          ; (i = i1) → [ _ , g , funExt⁻ (α .N-hom f) a (~ j) ]
          })
        (shift/ g f ((α ⟦ _ ⟧) a) i)
    mapL d (squash/ t u p q i j) =
      squash/ (mapL d t) (mapL d u) (cong (mapL d) p) (cong (mapL d) q) i j

    mapLR : {d d' : D.ob} (h : D.Hom[ d' , d ])
      → mapL d' ∘ mapR G h ≡ mapR G' h ∘ mapL d
    mapLR h = funExt (elimProp (λ _ → squash/ _ _) (λ _ → refl))

  mapLId : (G : Functor (C ^op) (SET ℓ))
    (d : D.ob) → mapL (idTrans G) d ≡ idfun (Quo G d)
  mapLId G d = funExt (elimProp (λ _ → squash/ _ _) (λ _ → refl))

  mapL∘ : {G G' G'' : Functor (C ^op) (SET ℓ)}
    (β : NatTrans G' G'') (α : NatTrans G G')
    (d : D.ob) → mapL (seqTrans α β) d ≡ mapL β d ∘ mapL α d
  mapL∘ β α d = funExt (elimProp (λ _ → squash/ _ _) (λ _ → refl))

  LanHom : {G G' : Functor (C ^op) (SET ℓ)}
    → NatTrans G G' → NatTrans (LanOb G) (LanOb G')
  LanHom α .N-ob = mapL α
  LanHom α .N-hom = mapLR α

  -- Definition of the left Kan extension functor

  Lan : Functor (FUNCTOR (C ^op) (SET ℓ)) (FUNCTOR (D ^op) (SET ℓ))
  Lan .F-ob = LanOb
  Lan .F-hom = LanHom
  Lan .F-id {G} = makeNatTransPath (funExt (mapLId G))
  Lan .F-seq α β = makeNatTransPath (funExt (mapL∘ β α))

  -- Adjunction between the left Kan extension and precomposition

  private
    F* = precomposeF (SET ℓ) (F ^opF)

  open UnitCounit

  η : 𝟙⟨ FUNCTOR (C ^op) (SET ℓ) ⟩ ⇒ funcComp F* Lan
  η .N-ob G .N-ob c a = [ c , D.id _ , a ]
  η .N-ob G .N-hom {c'} {c} f =
    funExt λ a →
    [ c , D.id _ , (G ⟪ f ⟫) a ]
      ≡⟨ sym (shift/ (D.id _) f a) ⟩
    [ c' , ((D.id _) D.⋆ F ⟪ f ⟫) , a ]
      ≡[ i ]⟨ [ c' , lem i , a ] ⟩
    [ c' , (F ⟪ f ⟫ D.⋆ (D.id _)) , a ]
    ∎
    where
    lem : (D.id _) D.⋆ F ⟪ f ⟫ ≡ F ⟪ f ⟫ D.⋆ (D.id _)
    lem = D.⋆IdL (F ⟪ f ⟫) ∙ sym (D.⋆IdR (F ⟪ f ⟫))
  η .N-hom f = makeNatTransPath refl

  ε : funcComp Lan F* ⇒ 𝟙⟨ FUNCTOR (D ^op) (SET ℓ) ⟩
  ε .N-ob H .N-ob d =
    elim
      (λ _ → (H ⟅ d ⟆) .snd)
      (λ (c , g , a) → (H ⟪ g ⟫) a)
      (λ {_ _ (shift g f a) i → H .F-seq (F ⟪ f ⟫) g i a})
  ε .N-ob H .N-hom g' =
    funExt (elimProp (λ _ → (H ⟅ _ ⟆) .snd _ _) (λ (c , g , a) → funExt⁻ (H .F-seq g g') a))
  ε .N-hom {H} {H'} α =
    makeNatTransPath
      (funExt₂ λ d →
         elimProp (λ _ → (H' ⟅ _ ⟆) .snd _ _)
          (λ (c , g , a) → sym (funExt⁻ (α .N-hom g) a)))

  Δ₁ : ∀ G → seqTrans (Lan ⟪ η ⟦ G ⟧ ⟫) (ε ⟦ Lan ⟅ G ⟆ ⟧) ≡ idTrans _
  Δ₁ G =
    makeNatTransPath
      (funExt₂ λ d →
        elimProp (λ _ → squash/ _ _)
          (λ (c , g , a) →
            [ c , g D.⋆ D.id _ , a ]
              ≡[ i ]⟨ [ c , (g D.⋆ F .F-id (~ i)) , a ] ⟩
            [ c , g D.⋆ (F ⟪ C.id _ ⟫) , a ]
              ≡⟨ shift/ g (C.id _) a ⟩
            [ c , g , (G ⟪ C.id _ ⟫) a ]
              ≡[ i ]⟨ [ c , g , G .F-id i a ] ⟩
            [ c , g , a ]
            ∎))

  Δ₂ : ∀ H → seqTrans (η ⟦ F* ⟅ H ⟆ ⟧) (F* ⟪ ε ⟦ H ⟧ ⟫) ≡ idTrans _
  Δ₂ H = makeNatTransPath (funExt λ c → H .F-id)

  adj : Lan ⊣ F*
  adj = make⊣ η ε Δ₁ Δ₂

{-
  Right Kan extension of a functor C → D to a functor PreShv C ℓ → PreShv D ℓ right adjoint to precomposition.
-}

module Ran {ℓC ℓC' ℓD ℓD'} ℓS
  {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'}
  (F : Functor C D)
  where

  open Functor
  open NatTrans

  private
    module C = Precategory C
    module D = Precategory D

    {-
      We want the category SET ℓ we're mapping into to be large enough that the coend will take presheaves
      Cᵒᵖ → Set ℓ to presheaves Dᵒᵖ → Set ℓ, otherwise we get no adjunction with precomposition.
      So we must have ℓC,ℓC',ℓD' ≤ ℓ; the parameter ℓS allows ℓ to be larger than their maximum.
    -}
    ℓ = ℓ-max (ℓ-max (ℓ-max ℓC ℓC') ℓD') ℓS

  module _ (G : Functor (C ^op) (SET ℓ)) where

    -- Definition of the end

    record End (d : D.ob) : Type ℓ where
      field
        fun : (c : C.ob) (g : D.Hom[ F ⟅ c ⟆ , d ]) → G .F-ob c .fst
        coh : {c c' : C.ob} (f : C.Hom[ c , c' ]) (g : D.Hom[ F ⟅ c' ⟆ , d ])
          → fun c (F ⟪ f ⟫ ⋆⟨ D ⟩ g) ≡ (G ⟪ f ⟫) (fun c' g)

    open End

    end≡ : {d : D.ob} {x x' : End d} → (∀ c g → x .fun c g ≡ x' .fun c g) → x ≡ x'
    end≡ h i .fun c g = h c g i
    end≡ {_} {x} {x'} h i .coh f g =
      isSet→isSet' (G .F-ob _ .snd)
        (x .coh f g)
        (x' .coh f g)
        (h _ (F ⟪ f ⟫ ⋆⟨ D ⟩ g))
        (cong (G ⟪ f ⟫) (h _ g))
        i

    -- Action of End on arrows in D

    mapR : {d d' : D.ob} (h : D.Hom[ d' , d ]) → End d → End d'
    mapR h x .fun c g = x .fun c (g ⋆⟨ D ⟩ h)
    mapR h x .coh f g = cong (x .fun _) (D.⋆Assoc (F ⟪ f ⟫) g h) ∙ x .coh f (g ⋆⟨ D ⟩ h)

    mapRId : (d : D.ob) → mapR (D.id d) ≡ (idfun _)
    mapRId h = funExt λ x → end≡ λ c g → cong (x .fun c) (D.⋆IdR g)

    mapR∘ : {d d' d'' : D.ob}
      (h' : D.Hom[ d'' , d' ]) (h : D.Hom[ d' , d ])
      → mapR (h' D.⋆ h) ≡ mapR h' ∘ mapR h
    mapR∘ h' h = funExt λ x → end≡ λ c g → cong (x .fun c) (sym (D.⋆Assoc g h' h))

  open End

  RanOb : Functor (C ^op) (SET ℓ) → Functor (D ^op) (SET _)
  RanOb G .F-ob d .fst = End G d
  RanOb G .F-ob d .snd =
    -- We use that End is equivalent to a Σ-type to prove its HLevel more easily
    isOfHLevelRetract 2
      {B =
        Σ[ z ∈ ((c : C.ob) (g : D.Hom[ F ⟅ c ⟆ , d ]) → G .F-ob c .fst) ]
        ({c c' : C.ob} (f : C.Hom[ c , c' ]) (g : D.Hom[ F ⟅ c' ⟆ , d ])
          → z c (F ⟪ f ⟫ ⋆⟨ D ⟩ g) ≡ (G ⟪ f ⟫) (z c' g))
      }
      (λ x → λ where .fst → x .fun; .snd → x .coh)
      (λ σ → λ where .fun → σ .fst; .coh → σ .snd)
      (λ _ → refl)
      (isSetΣ
        (isSetΠ2 λ _ _ → G .F-ob _ .snd)
        (λ _ → isProp→isSet
          (isPropImplicitΠ λ _ → isPropImplicitΠ λ _ → isPropΠ2 λ _ _ → G .F-ob _ .snd _ _)))
  RanOb G .F-hom = mapR G
  RanOb G .F-id {d} = mapRId G d
  RanOb G .F-seq h h' = mapR∘ G h' h

  -- Action of End on arrows in Cᵒᵖ → Set

  module _ {G G' : Functor (C ^op) (SET ℓ)} (α : NatTrans G G') where

    mapL : (d : D.ob) → End G d → End G' d
    mapL d x .fun c g = (α ⟦ c ⟧) (x .fun c g)
    mapL d x .coh f g =
      cong (α ⟦ _ ⟧) (x .coh f g)
      ∙ funExt⁻ (α .N-hom f) (x .fun _ g)

    mapLR : {d d' : D.ob} (h : D.Hom[ d' , d ])
      → mapL d' ∘ mapR G h ≡ mapR G' h ∘ mapL d
    mapLR h = funExt λ _ → end≡ _ λ _ _ → refl

  mapLId : (G : Functor (C ^op) (SET ℓ))
    (d : D.ob) → mapL (idTrans G) d ≡ idfun (End G d)
  mapLId G d = funExt λ _ → end≡ _ λ _ _ → refl

  mapL∘ : {G G' G'' : Functor (C ^op) (SET ℓ)}
    (β : NatTrans G' G'') (α : NatTrans G G')
    (d : D.ob) → mapL (seqTrans α β) d ≡ mapL β d ∘ mapL α d
  mapL∘ β α d = funExt λ _ → end≡ _ λ _ _ → refl

  RanHom : {G G' : Functor (C ^op) (SET ℓ)}
    → NatTrans G G' → NatTrans (RanOb G) (RanOb G')
  RanHom α .N-ob = mapL α
  RanHom α .N-hom = mapLR α

  -- Definition of the right Kan extension functor

  Ran : Functor (FUNCTOR (C ^op) (SET ℓ)) (FUNCTOR (D ^op) (SET ℓ))
  Ran .F-ob = RanOb
  Ran .F-hom = RanHom
  Ran .F-id {G} = makeNatTransPath (funExt (mapLId G))
  Ran .F-seq α β = makeNatTransPath (funExt (mapL∘ β α))

  -- Adjunction between precomposition and right Kan extension

  private
    F* = precomposeF (SET ℓ) (F ^opF)

  open UnitCounit

  η : 𝟙⟨ FUNCTOR (D ^op) (SET ℓ) ⟩ ⇒ (funcComp Ran F*)
  η .N-ob G .N-ob d a .fun c g = (G ⟪ g ⟫) a
  η .N-ob G .N-ob d a .coh f g = funExt⁻ (G .F-seq g (F ⟪ f ⟫)) a
  η .N-ob G .N-hom h = funExt λ a → end≡ _ λ c g → sym (funExt⁻ (G .F-seq h g) a)
  η .N-hom {G} {G'} α =
    makeNatTransPath (funExt₂ λ d a → end≡ _ λ c g → sym (funExt⁻ (α .N-hom g) a))

  ε : funcComp F* Ran ⇒ 𝟙⟨ FUNCTOR (C ^op) (SET ℓ) ⟩
  ε .N-ob H .N-ob c x = x .fun c (D.id _)
  ε .N-ob H .N-hom {c} {c'} g =
    funExt λ x →
    cong (x .fun c') (D.⋆IdL _ ∙ sym (D.⋆IdR _)) ∙ x .coh g (D.id _)
  ε .N-hom {H} {H'} α = makeNatTransPath refl

  Δ₁ : ∀ G → seqTrans (F* ⟪ η ⟦ G ⟧ ⟫) (ε ⟦ F* ⟅ G ⟆ ⟧) ≡ idTrans _
  Δ₁ G = makeNatTransPath (funExt₂ λ c a → funExt⁻ (G .F-id) a)

  Δ₂ : ∀ H → seqTrans (η ⟦ Ran ⟅ H ⟆ ⟧) (Ran ⟪ ε ⟦ H ⟧ ⟫) ≡ idTrans _
  Δ₂ H = makeNatTransPath (funExt₂ λ c x → end≡ _ λ c' g → cong (x .fun c') (D.⋆IdL g))

  adj : F* ⊣ Ran
  adj = make⊣ η ε Δ₁ Δ₂

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-
Problem #758
same as problem 757 but rewritten with only expressions of first-order logic
Given premises:
     (all A)(all B)((subset A B) <-> (all x)((mem x A) -> (mem x B)))    justification = 1.0
     (all A)(all B)(some intAB)(IsInt A B intAB)    justification = 1.0
     (all A)(all B)(all intAB)((IsInt A B intAB) <-> (all x)((mem x intAB) <-> ((mem x A) & (mem x B))))    justification = 1.0
     (all A)(all B)((mapsF A B) <-> ((all x)((mem x A) -> (some y)((mem y B) & (F x y))) & (all x)(all y)(all z)(((mem x A) & ((mem y A) & (mem z A))) -> (((F x y) & (F x z)) -> (same y z)))))    justification = 1.0
     (all A)(all x)(all y)((same x y) -> ((mem x A) -> (mem y A)))    justification = 1.0
     (all x)(same x x)    justification = 1.0
     (all x)(all y)((same x y) <-> (same y x))    justification = 1.0
     (all x)(all y)(all z)(((same x y) & (same y z)) -> (same x z))    justification = 1.0
     (all A)(all B)((equal A B) <-> ((subset A B) & (subset B A)))    justification = 1.0
     (all A)(all B)(some invFBA)(IsInvF B A invFBA)    justification = 1.0
     (all A)(all B)(all invFBA)((IsInvF B A invFBA) <-> (all x)((mem x invFBA) <-> ((mem x A) & (some y)((mem y B) & (F x y)))))    justification = 1.0
Ultimate epistemic interests:
     (all A)(all B)(all X)(all Y)(((mapsF A B) & ((subset X B) & (subset Y B))) -> (some intXY)((IsInt X Y intXY) & (some invFIntXYA)((IsInvF intXY A invFIntXYA) & (some invFXA)((IsInvF X A invFXA) & (some invFYA)((IsInvF Y A invFYA) & (some intInvFXAInvFYA)((IsInt invFXA invFYA intInvFXAInvFYA) & (equal invFIntXYA intInvFXAInvFYA)))))))    interest = 1.0
-}

_↔_ : Set → Set → Set
p ↔ q = p → q

postulate
  U : Set
  subset : U → U → Set
--  subsetMembership : ∀ {A} {B} →


text:
{-

Set quotients:

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.SetQuotients.Properties where

open import Cubical.HITs.SetQuotients.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Univalence

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Base

open import Cubical.HITs.TypeQuotients as TypeQuot using (_/ₜ_ ; [_] ; eq/)
open import Cubical.HITs.PropositionalTruncation as PropTrunc using (∥_∥ ; ∣_∣ ; squash)
open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂ ; ∣_∣₂ ; squash₂
                                                              ; setTruncIsSet)

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    R : A → A → Type ℓ
    B : A / R → Type ℓ
    C : A / R → A / R → Type ℓ
    D : A / R → A / R → A / R → Type ℓ

elimEq/ : (Bprop : (x : A / R ) → isProp (B x))
          {x y : A / R}
          (eq : x ≡ y)
          (bx : B x)
          (by : B y) →
          PathP (λ i → B (eq i)) bx by
elimEq/ {B = B} Bprop {x = x} =
  J (λ y eq → ∀ bx by → PathP (λ i → B (eq i)) bx by) (λ bx by → Bprop x bx by)

elimProp : ((x : A / R ) → isProp (B x))
         → ((a : A) → B ( [ a ]))
         → (x : A / R)
         → B x
elimProp Bprop f [ x ] = f x
elimProp Bprop f (squash/ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 (λ x → isProp→isSet (Bprop x))
    (g x) (g y) (cong g p) (cong g q) (squash/ x y p q) i j
    where
    g = elimProp Bprop f
elimProp Bprop f (eq/ a b r i) = elimEq/ Bprop (eq/ a b r) (f a) (f b) i

elimProp2 : ((x y : A / R ) → isProp (C x y))
          → ((a b : A) → C [ a ] [ b ])
          → (x y : A / R)
          → C x y
elimProp2 Cprop f = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                             (λ x → elimProp (λ y → Cprop [ x ] y) (f x))

elimProp3 : ((x y z : A / R ) → isProp (D x y z))
          → ((a b c : A) → D [ a ] [ b ] [ c ])
          → (x y z : A / R)
          → D x y z
elimProp3 Dprop f = elimProp (λ x → isPropΠ2 (λ y z → Dprop x y z))
                             (λ x → elimProp2 (λ y z → Dprop [ x ] y z) (f x))

-- lemma 6.10.2 in hott book
[]surjective : (x : A / R) → ∃[ a ∈ A ] [ a ] ≡ x
[]surjective = elimProp (λ x → squash) (λ a → ∣ a , refl ∣)

elim : {B : A / R → Type ℓ}
     → ((x : A / R) → isSet (B x))
     → (f : (a : A) → (B [ a ]))
     → ((a b : A) (r : R a b) → PathP (λ i → B (eq/ a b r i)) (f a) (f b))
     → (x : A / R)
     → B x
elim Bset f feq [ a ] = f a
elim Bset f feq (eq/ a b r i) = feq a b r i
elim Bset f feq (squash/ x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 Bset
              (g x) (g y) (cong g p) (cong g q) (squash/ x y p q) i j
    where
      g = elim Bset f feq

rec : {B : Type ℓ}
      (Bset : isSet B)
      (f : A → B)
      (feq : (a b : A) (r : R a b) → f a ≡ f b)
    → A / R → B
rec Bset f feq [ a ] = f a
rec Bset f feq (eq/ a b r i) = feq a b r i
rec Bset f feq (squash/ x y p q i j) = Bset (g x) (g y) (cong g p) (cong g q) i j
  where
  g = rec Bset f feq

rec2 : {B : Type ℓ} (Bset : isSet B)
       (f : A → A → B) (feql : (a b c : A) (r : R a b) → f a c ≡ f b c)
                       (feqr : (a b c : A) (r : R b c) → f a b ≡ f a c)
    → A / R → A / R → B
rec2 Bset f feql feqr = rec (isSetΠ (λ _ → Bset))
                            (λ a → rec Bset (f a) (feqr a))
                            (λ a b r → funExt (elimProp (λ _ → Bset _ _)
                                              (λ c → feql a b c r)))

-- the recursor for maps into groupoids:
-- i.e. for any type A with a binary relation R and groupoid B,
-- we can construct a map A / R → B from a map A → B satisfying the conditions
-- (i)   ∀ (a b : A) → R a b → f a ≡ f b
-- (ii)  ∀ (a b : A) → isProp (f a ≡ f b)

-- We start by proving that we can recover the set-quotient
-- by set-truncating the (non-truncated type quotient)
typeQuotSetTruncIso : Iso (A / R) ∥ A /ₜ R ∥₂
Iso.fun typeQuotSetTruncIso = rec setTruncIsSet (λ a → ∣ [ a ] ∣₂)
                                                 λ a b r → cong ∣_∣₂ (eq/ a b r)
Iso.inv typeQuotSetTruncIso = SetTrunc.rec squash/ (TypeQuot.rec [_] eq/)
Iso.rightInv typeQuotSetTruncIso = SetTrunc.elim (λ _ → isProp→isSet (squash₂ _ _))
                                  (TypeQuot.elimProp (λ _ → squash₂ _ _) λ _ → refl)
Iso.leftInv typeQuotSetTruncIso = elimProp (λ _ → squash/ _ _) λ _ → refl

module rec→Gpd {A : Type ℓ} {R : A → A → Type ℓ'} {B : Type ℓ''} (Bgpd : isGroupoid B)
               (f : A → B)
               (feq : ∀ (a b : A) → R a b → f a ≡ f b)
               (fprop : ∀ (a b : A) → isProp (f a ≡ f b)) where

 fun : A / R → B
 fun = f₁ ∘ f₂
  where
  f₁ : ∥ A /ₜ R ∥₂ → B
  f₁ = SetTrunc.rec→Gpd.fun Bgpd f/ congF/Const
   where
   f/ : A /ₜ R → B
   f/ = TypeQuot.rec f feq
   congF/Const : (a b : A /ₜ R) (p q : a ≡ b) → cong f/ p ≡ cong f/ q
   congF/Const = TypeQuot.elimProp2 (λ _ _ → isPropΠ2 λ _ _ → Bgpd _ _ _ _)
                                     λ a b p q → fprop a b (cong f/ p) (cong f/ q)

  f₂ : A / R → ∥ A /ₜ R ∥₂
  f₂ = Iso.fun typeQuotSetTruncIso

setQuotUniversalIso : {B : Type ℓ} (Bset : isSet B)
                    → Iso (A / R → B) (Σ[ f ∈ (A → B) ] ((a b : A) → R a b → f a ≡ f b))
Iso.fun (setQuotUniversalIso Bset) g = (λ a → g [ a ]) , λ a b r i → g (eq/ a b r i)
Iso.inv (setQuotUniversalIso Bset) h = elim (λ x → Bset) (fst h) (snd h)
Iso.rightInv (setQuotUniversalIso Bset) h = refl
Iso.leftInv (setQuotUniversalIso Bset) g =
 funExt (λ x → PropTrunc.elim (λ sur → Bset (out (intro g) x) (g x))
        (λ sur → cong (out (intro g)) (sym (snd sur)) ∙ (cong g (snd sur))) ([]surjective x))
     where
     intro = Iso.fun (setQuotUniversalIso Bset)
     out = Iso.inv (setQuotUniversalIso Bset)

setQuotUniversal : {B : Type ℓ} (Bset : isSet B) →
                   (A / R → B) ≃ (Σ[ f ∈ (A → B) ] ((a b : A) → R a b → f a ≡ f b))
setQuotUniversal Bset = isoToEquiv (setQuotUniversalIso Bset)

open BinaryRelation

-- characterisation of binary functions/operations on set-quotients
setQuotUniversal2Iso : {B : Type ℓ} (Bset : isSet B) → isRefl R
                 → Iso (A / R → A / R → B)
                       (Σ[ _∗_ ∈ (A → A → B) ] ((a a' b b' : A) → R a a' → R b b' → a ∗ b ≡ a' ∗ b'))
Iso.fun (setQuotUniversal2Iso {A = A} {R = R} {B = B} Bset isReflR) _∗/_ = _∗_ , h
   where
   _∗_ = λ a b → [ a ] ∗/ [ b ]
   h : (a a' b b' : A) → R a a' → R b b' → a ∗ b ≡ a' ∗ b'
   h a a' b b' ra rb = cong (_∗/ [ b ]) (eq/ _ _ ra) ∙ cong ([ a' ] ∗/_) (eq/ _ _ rb)
Iso.inv (setQuotUniversal2Iso {A = A} {R = R} {B = B} Bset isReflR) (_∗_ , h) =
   rec2 Bset _∗_ hleft hright
        where
        hleft : ∀ a b c → R a b → (a ∗ c) ≡ (b ∗ c)
        hleft _ _ c r = h _ _ _ _ r (isReflR c)
        hright : ∀ a b c → R b c → (a ∗ b) ≡ (a ∗ c)
        hright a _ _ r = h _ _ _ _ (isReflR a) r
Iso.rightInv (setQuotUniversal2Iso {A = A} {R = R} {B = B} Bset isReflR) (_∗_ , h) =
   Σ≡Prop (λ _ → isPropΠ4 λ _ _ _ _ → isPropΠ2 λ _ _ → Bset _ _) refl
Iso.leftInv (setQuotUniversal2Iso {A = A} {R = R} {B = B} Bset isReflR) _∗/_ =
   funExt₂ (elimProp2 (λ _ _ → Bset _ _) λ _ _ → refl)

setQuotUniversal2 : {B : Type ℓ} (Bset : isSet B) → isRefl R
                  → (A / R → A / R → B)
                  ≃ (Σ[ _∗_ ∈ (A → A → B) ] ((a a' b b' : A) → R a a' → R b b' → a ∗ b ≡ a' ∗ b'))
setQuotUniversal2 Bset isReflR = isoToEquiv (setQuotUniversal2Iso Bset isReflR)

-- corollary for binary operations
-- TODO: prove truncated inverse for effective relations
setQuotBinOp : isRefl R
             → (_∗_ : A → A → A)
             → (∀ a a' b b' → R a a' → R b b' → R (a ∗ b) (a' ∗ b'))
             → (A / R → A / R → A / R)
setQuotBinOp isReflR _∗_ h = Iso.inv (setQuotUniversal2Iso squash/ isReflR)
                             ((λ a b → [ a ∗ b ]) , λ _ _ _ _ ra rb → eq/ _ _ (h _ _ _ _ ra rb))

setQuotSymmBinOp : isRefl R → isTrans R
                 → (_∗_ : A → A → A)
                 → (∀ a b → a ∗ b ≡ b ∗ a)
                 → (∀ a a' b → R a a' → R (a ∗ b) (a' ∗ b))
                 → (A / R → A / R → A / R)
setQuotSymmBinOp {A = A} {R = R} isReflR isTransR _∗_ ∗-symm h = setQuotBinOp isReflR _∗_ h'
  where
  h' : ∀ a a' b b' → R a a' → R b b' → R (a ∗ b) (a' ∗ b')
  h' a a' b b' ra rb = isTransR _ _ _ (h a a' b ra)
                               (transport (λ i → R (∗-symm b a' i) (∗-symm b' a' i)) (h b b' a' rb))

effective : (Rprop : isPropValued R) (Requiv : isEquivRel R) (a b : A) → [ a ] ≡ [ b ] → R a b
effective {A = A} {R = R} Rprop (equivRel R/refl R/sym R/trans) a b p = transport aa≡ab (R/refl _)
  where
    helper : A / R → hProp _
    helper =
      rec isSetHProp (λ c → (R a c , Rprop a c))
                     (λ c d cd → Σ≡Prop (λ _ → isPropIsProp)
                                        (hPropExt (Rprop a c) (Rprop a d)
                                                  (λ ac → R/trans _ _ _ ac cd) (λ ad → R/trans _ _ _ ad (R/sym _ _ cd))))

    aa≡ab : R a a ≡ R a b
    aa≡ab i = helper (p i) .fst

isEquivRel→effectiveIso : isPropValued R → isEquivRel R → (a b : A) → Iso ([ a ] ≡ [ b ]) (R a b)
Iso.fun (isEquivRel→effectiveIso {R = R} Rprop Req a b) = effective Rprop Req a b
Iso.inv (isEquivRel→effectiveIso {R = R} Rprop Req a b) = eq/ a b
Iso.rightInv (isEquivRel→effectiveIso {R = R} Rprop Req a b) _ = Rprop a b _ _
Iso.leftInv (isEquivRel→effectiveIso {R = R} Rprop Req a b) _ = squash/ _ _ _ _

isEquivRel→isEffective : isPropValued R → isEquivRel R → isEffective R
isEquivRel→isEffective Rprop Req a b = isoToIsEquiv (invIso (isEquivRel→effectiveIso Rprop Req a b))

discreteSetQuotients : Discrete A → isPropValued R → isEquivRel R → (∀ a₀ a₁ → Dec (R a₀ a₁)) → Discrete (A / R)
discreteSetQuotients {A = A} {R = R} Adis Rprop Req Rdec =
  elim (λ a₀ → isSetΠ (λ a₁ → isProp→isSet (isPropDec (squash/ a₀ a₁))))
    discreteSetQuotients' discreteSetQuotients'-eq
  where
    discreteSetQuotients' : (a : A) (y : A / R) → Dec ([ a ] ≡ y)
    discreteSetQuotients' a₀ = elim (λ a₁ → isProp→isSet (isPropDec (squash/ [ a₀ ] a₁))) dis dis-eq
      where
        dis : (a₁ : A) → Dec ([ a₀ ] ≡ [ a₁ ])
        dis a₁ with Rdec a₀ a₁
        ... | (yes p) = yes (eq/ a₀ a₁ p)
        ... | (no ¬p) = no λ eq → ¬p (effective Rprop Req a₀ a₁ eq )

        dis-eq : (a b : A) (r : R a b) →
          PathP (λ i → Dec ([ a₀ ] ≡ eq/ a b r i)) (dis a) (dis b)
        dis-eq a b ab = J (λ b ab → ∀ k → PathP (λ i → Dec ([ a₀ ] ≡ ab i)) (dis a) k)
                          (λ k → isPropDec (squash/ _ _) _  _) (eq/ a b ab) (dis b)

    discreteSetQuotients'-eq : (a b : A) (r : R a b) →
      PathP (λ i → (y : A / R) → Dec (eq/ a b r i ≡ y))
            (discreteSetQuotients' a) (discreteSetQuotients' b)
    discreteSetQuotients'-eq a b ab =
      J (λ b ab → ∀ k → PathP (λ i → (y : A / R) → Dec (ab i ≡ y))
                              (discreteSetQuotients' a) k)
        (λ k → funExt (λ x → isPropDec (squash/ _ _) _ _)) (eq/ a b ab) (discreteSetQuotients' b)

-- Quotienting by the truncated relation is equivalent to quotienting by untruncated relation
truncRelIso : Iso (A / R) (A / (λ a b → ∥ R a b ∥))
Iso.fun truncRelIso = rec squash/ [_] λ _ _ r → eq/ _ _ ∣ r ∣
Iso.inv truncRelIso = rec squash/ [_] λ _ _ → PropTrunc.rec (squash/ _ _) λ r → eq/ _ _ r
Iso.rightInv truncRelIso = elimProp (λ _ → squash/ _ _) λ _ → refl
Iso.leftInv truncRelIso = elimProp (λ _ → squash/ _ _) λ _ → refl

truncRelEquiv : A / R ≃ A / (λ a b → ∥ R a b ∥)
truncRelEquiv = isoToEquiv truncRelIso

-- Using this we can obtain a useful characterization of
-- path-types for equivalence relations (not prop-valued)
-- and their quotients

isEquivRel→TruncIso : isEquivRel R → (a b : A) → Iso ([ a ] ≡ [ b ])  ∥ R a b ∥
isEquivRel→TruncIso {A = A} {R = R} Req a b = compIso (isProp→Iso (squash/ _ _) (squash/ _ _)
                                   (cong (Iso.fun truncRelIso)) (cong (Iso.inv truncRelIso)))
                      (isEquivRel→effectiveIso  (λ _ _ → PropTrunc.propTruncIsProp) ∥R∥eq a b)
 where
 open isEquivRel
 ∥R∥eq : isEquivRel  λ a b → ∥ R a b ∥
 reflexive ∥R∥eq a = ∣ reflexive Req a ∣
 symmetric ∥R∥eq a b = PropTrunc.map (symmetric Req a b)
 transitive ∥R∥eq a b c = PropTrunc.map2 (transitive Req a b c)


text:
module bool-thms2 where

open import bool
open import eq
open import product
open import sum

ff-imp : ∀ (b : 𝔹) → (ff imp b) ≡ tt
ff-imp ff = refl
ff-imp tt = refl

imp-tt : ∀ (b : 𝔹) → (b imp tt) ≡ tt
imp-tt ff = refl
imp-tt tt = refl

imp-ff : ∀ (b : 𝔹) → (b imp ff) ≡ ~ b
imp-ff tt = refl
imp-ff ff = refl

tt-imp : ∀ (b : 𝔹) → (tt imp b) ≡ b
tt-imp tt = refl
tt-imp ff = refl

&&-tt : ∀ (b : 𝔹) → b && tt ≡ b
&&-tt tt = refl
&&-tt ff = refl

||-ff : ∀ (b : 𝔹) → b || ff ≡ b
||-ff tt = refl
||-ff ff = refl

&&-contra : ∀ (b : 𝔹) → b && ~ b ≡ ff
&&-contra ff = refl
&&-contra tt = refl

&&-comm : ∀ (b1 b2 : 𝔹) → b1 && b2 ≡ b2 && b1
&&-comm ff ff = refl
&&-comm ff tt = refl
&&-comm tt ff = refl
&&-comm tt tt = refl

||-comm : ∀ (b1 b2 : 𝔹) → b1 || b2 ≡ b2 || b1
||-comm ff ff = refl
||-comm ff tt = refl
||-comm tt ff = refl
||-comm tt tt = refl

&&-assoc : ∀ (b1 b2 b3 : 𝔹) → b1 && (b2 && b3) ≡ (b1 && b2) && b3
&&-assoc ff _ _ = refl
&&-assoc tt _ _ = refl

||-assoc : ∀ (b1 b2 b3 : 𝔹) → b1 || (b2 || b3) ≡ (b1 || b2) || b3
||-assoc tt _ _ = refl
||-assoc ff _ _ = refl

~-over-&& : ∀ (b1 b2 : 𝔹) → ~ ( b1 && b2 ) ≡ (~ b1 || ~ b2)
~-over-&& tt _ = refl
~-over-&& ff _ = refl

~-over-|| : ∀ (b1 b2 : 𝔹) → ~ ( b1 || b2 ) ≡ (~ b1 && ~ b2)
~-over-|| tt _ = refl
~-over-|| ff _ = refl

&&-over-||-l : ∀ (a b c : 𝔹) → a && (b || c) ≡ (a && b) || (a && c)
&&-over-||-l tt _ _ = refl
&&-over-||-l ff _ _ = refl

&&-over-||-r : ∀ (a b c : 𝔹) → (a || b) && c ≡ (a && c) || (b && c)
&&-over-||-r tt tt tt = refl
&&-over-||-r tt tt ff = refl
&&-over-||-r tt ff tt = refl
&&-over-||-r tt ff ff = refl
&&-over-||-r ff tt tt = refl
&&-over-||-r ff tt ff = refl
&&-over-||-r ff ff tt = refl
&&-over-||-r ff ff ff = refl

||-over-&&-l : ∀ (a b c : 𝔹) → a || (b && c) ≡ (a || b) && (a || c)
||-over-&&-l tt _ _ = refl
||-over-&&-l ff _ _ = refl

||-over-&&-r : ∀ (a b c : 𝔹) → (a && b) || c ≡ (a || c) && (b || c)
||-over-&&-r tt _ _ = refl
||-over-&&-r ff _ ff = refl
||-over-&&-r ff tt tt = refl
||-over-&&-r ff ff tt = refl

&&-cong₁ : ∀ {b1 b1' b2 : 𝔹} → b1 ≡ b1' → b1 && b2 ≡ b1' && b2
&&-cong₁ refl = refl

&&-cong₂ : ∀ {b1 b2 b2' : 𝔹} → b2 ≡ b2' → b1 && b2 ≡ b1 && b2'
&&-cong₂ refl = refl

&&-intro : ∀ {b1 b2 : 𝔹} → b1 ≡ tt → b2 ≡ tt → b1 && b2 ≡ tt
&&-intro{tt}{tt} _ _ = refl
&&-intro{tt}{ff} _ ()
&&-intro{ff}{tt} () _
&&-intro{ff}{ff} () _

||-intro1 : ∀ {b1 b2 : 𝔹} → b1 ≡ tt → b1 || b2 ≡ tt
||-intro1 {tt} p = refl
||-intro1 {ff} ()

&&-elim : ∀ {b1 b2 : 𝔹} → b1 && b2 ≡ tt → b1 ≡ tt ∧ b2 ≡ tt
&&-elim{tt}{tt} _ = refl , refl
&&-elim{ff}{_} ()
&&-elim{tt}{ff} ()

&&-elim1 : ∀ {b1 b2 : 𝔹} → b1 && b2 ≡ tt → b1 ≡ tt
&&-elim1 p with &&-elim p
&&-elim1 _ | p , _ = p

&&-elim2 : ∀ {b1 b2 : 𝔹} → b1 && b2 ≡ tt → b2 ≡ tt
&&-elim2{b1} p with &&-elim{b1} p
&&-elim2 _ | _ , p = p

||-elim : ∀ {b1 b2 : 𝔹} → b1 || b2 ≡ tt → b1 ≡ tt ∨ b2 ≡ tt
||-elim {tt} refl = inj₁ refl
||-elim {ff} refl = inj₂ refl

~-cong : ∀ {b b' : 𝔹} → b ≡ b' → ~ b ≡ ~ b'
~-cong refl = refl

ite-cong₁ : ∀{ℓ}{A : Set ℓ} {b b' : 𝔹}(x y : A) → b ≡ b' → (if b then x else y) ≡ (if b' then x else y)
ite-cong₁ x y refl = refl

ite-cong₂ : ∀{ℓ}{A : Set ℓ} (b : 𝔹){x x' : A}(y : A) → x ≡ x' → (if b then x else y) ≡ (if b then x' else y)
ite-cong₂ b y refl = refl

ite-cong₃ : ∀{ℓ}{A : Set ℓ} (b : 𝔹)(x : A){y y' : A} → y ≡ y' → (if b then x else y) ≡ (if b then x else y')
ite-cong₃ b x refl = refl

&&-split : ∀ {b b' : 𝔹} → b || b' ≡ ff → b ≡ ff ⊎ b' ≡ ff
&&-split {tt} ()
&&-split {ff}{tt} ()
&&-split {ff}{ff} p = inj₁ refl

-----------------------------------
-- Theorems about imp
-----------------------------------
imp-same : ∀ (b : 𝔹) → (b imp b) ≡ tt
imp-same ff = refl
imp-same tt = refl

imp-to-|| : ∀ (b1 b2 : 𝔹) → (b1 imp b2) ≡ (~ b1 || b2)
imp-to-|| ff _ = refl
imp-to-|| tt _ = refl

imp-mp : ∀ {b b' : 𝔹} → (b imp b') ≡ tt → b ≡ tt → b' ≡ tt
imp-mp {tt} {tt} p refl = refl
imp-mp {ff} {ff} p q = q
imp-mp {tt} {ff} p q = p
imp-mp {ff} {tt} p q = refl

imp-antisymm : ∀ {b1 b2 : 𝔹} → (b1 imp b2) ≡ tt → (b2 imp b1) ≡ tt → b1 ≡ b2
imp-antisymm{tt}{tt} p q = refl
imp-antisymm{tt}{ff} () q
imp-antisymm{ff}{tt} p ()
imp-antisymm{ff}{ff} p q = refl

-----------------------------------
-- Theorems about xor
-----------------------------------
ff-xor : ∀ (b : 𝔹) → ff xor b ≡ b
ff-xor tt = refl
ff-xor ff = refl

tt-xor : ∀ (b : 𝔹) → tt xor b ≡ ~ b
tt-xor tt = refl
tt-xor ff = refl

~-xor-distrb : ∀ (a b : 𝔹) → ~ (a xor b) ≡ ~ a xor b
~-xor-distrb tt tt = refl
~-xor-distrb tt ff = refl
~-xor-distrb ff tt = refl
~-xor-distrb ff ff = refl

xor-distrib-&& : ∀ (x y : 𝔹) → x xor (y && x) ≡ ~ y && x
xor-distrib-&& tt tt = refl
xor-distrib-&& tt ff = refl
xor-distrib-&& ff tt = refl
xor-distrib-&& ff ff = refl

xor~hop : ∀ (a b : 𝔹) → ~ a xor b ≡ a xor ~ b
xor~hop tt tt = refl
xor~hop tt ff = refl
xor~hop ff tt = refl
xor~hop ff ff = refl

xor-comm : ∀ (b1 b2 : 𝔹) → b1 xor b2 ≡ b2 xor b1
xor-comm tt tt = refl
xor-comm tt ff = refl
xor-comm ff tt = refl
xor-comm ff ff = refl

xor-assoc : (b1 b2 b3 : 𝔹) → b1 xor (b2 xor b3) ≡ (b1 xor b2) xor b3
xor-assoc tt tt tt = refl
xor-assoc tt tt ff = refl
xor-assoc tt ff tt = refl
xor-assoc tt ff ff = refl
xor-assoc ff tt tt = refl
xor-assoc ff tt ff = refl
xor-assoc ff ff tt = refl
xor-assoc ff ff ff = refl

xor-anti-idem : (b : 𝔹) → b xor b ≡ ff
xor-anti-idem tt = refl
xor-anti-idem ff = refl

xor-≡ : {b1 b2 : 𝔹} → b1 xor b2 ≡ ff → b1 ≡ b2
xor-≡ {tt} {tt} p = refl
xor-≡ {tt} {ff} ()
xor-≡ {ff} {tt} ()
xor-≡ {ff} {ff} p = refl

-----------------------------------
-- Theorems about nor, nand
-----------------------------------

nor-not : ∀ (b : 𝔹) → b nor b ≡ ~ b
nor-not tt = refl
nor-not ff = refl

nor-or : ∀ (b1 b2 : 𝔹) → (b1 nor b2) nor (b1 nor b2) ≡ b1 || b2
nor-or tt b2 = refl
nor-or ff tt = refl
nor-or ff ff = refl

nor-and : ∀ (b1 b2 : 𝔹) → (b1 nor b1) nor (b2 nor b2) ≡ b1 && b2
nor-and tt tt = refl
nor-and tt ff = refl
nor-and ff b2 = refl

nor-comm : ∀ (b1 b2 : 𝔹) → b1 nor b2 ≡ b2 nor b1
nor-comm tt tt = refl
nor-comm tt ff = refl
nor-comm ff tt = refl
nor-comm ff ff = refl

nand-comm : ∀ (b1 b2 : 𝔹) → b1 nand b2 ≡ b2 nand b1
nand-comm tt tt = refl
nand-comm tt ff = refl
nand-comm ff tt = refl
nand-comm ff ff = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Prelude
open import Data.Nat using (_≤?_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Vec using (Vec; _∷_; [])

open import RW.Language.RTerm
open import RW.Language.FinTerm
open import RW.Language.RTermUtils
open import RW.Utils.Monads

module RW.Language.GoalGuesser (maxH : ℕ) where

  open Monad {{...}}

  ----------------
  -- Housekeeping

  private
    cast-RBinApp : {A B : Set} → (A → B) → RBinApp A → RBinApp B
    cast-RBinApp f (n , a , b) = n , replace-A (ovar ∘ f) a , replace-A (ovar ∘ f) b

    RBinApp02⊥ : RBinApp (Fin zero) → RBinApp ⊥
    RBinApp02⊥ = cast-RBinApp (λ ())

    symmetric : {A : Set} → RBinApp A → RBinApp A
    symmetric (n , a , b) = n , b , a

  -----------------
  -- Term subsitution

  -- Given a RBinApp representing a type (t₁ ▵ t₂), will return a
  -- non-deterministic substitution of t₂ for t₁ in a given goal g.
  -- If no substitution could be performed, the empty list will be returned.
  _[_] : {A : Set}{{eqA : Eq A}} → RTerm A → RTerm A × RTerm A → NonDet (RTerm A)
  g [ ty1 , ty2 ] = map p2 (filter p1 (substRTermAux g ty1 ty2))
    where
      -- Non-deterministic term substitution. Possibly empty substitution.
      -- Since we're only interested in the situations where a single substitution is performed,
      -- we also return a boolean flag indicating whether or not we already had a substitution.
      substRTermAux : {A : Set}{{ eqA : Eq A }} → RTerm A → RTerm A → RTerm A → NonDet (Bool × RTerm A)
      substRTermAux {A} {{eqA}} t m n with t ≟-RTerm m
      ...| yes _ = return (true , n)
      ...| no  _ = substStep t m n
        where
          mutual
            substStep : RTerm A → RTerm A → RTerm A → NonDet (Bool × RTerm A)
            substStep (ovar x) _ _ = return (false , ovar x)
            substStep (ivar n) _ _ = return (false , ivar n)
            substStep (rlit l) _ _ = return (false , rlit l)
            substStep (rlam t) m n = substRTermAux t m n >>= return ∘ (λ p → p1 p , rlam (p2 p))
            substStep (rapp a as) m n = substStep* as m n >>= return ∘ (λ p → p1 p , rapp a (p2 p))

            -- For the list scenario, in the inductive step, we need to substitute m for n in x,
            -- and return either the result of such substitution or the result of substituting
            -- m for n recursively in la. Do not forget that _++_ is mplus for the list monad.
            substStep* : List (RTerm A) → RTerm A → RTerm A → NonDet (Bool × List (RTerm A))
            substStep* [] _ _         = return (false , [])
            substStep* (x ∷ la) m n
              = substRTermAux x m n >>= λ x' → return (p1 x' , (p2 x' ∷ la))
                                            ++ (substStep* la m n >>= return ∘ (λ p → p1 p , x ∷ p2 p))

  -- Given a term and a type ty with n variables, will search for n subterms of t
  -- in a non-deterministic fashion, and will instantiate them as parameters to ty.
  {-# TERMINATING #-}
  apply : {n : ℕ} → RTerm ⊥ → RBinApp (Fin n) → NonDet (RTerm ⊥)
  -- If we have no more variables to instantiate on our type,
  -- we can proceed to substitute.
  apply {n = zero} g (_ , ty1 , ty2)
    = g [ Fin2RTerm⊥ ty1 , Fin2RTerm⊥ ty2 ]

  -- If not, we simply call with a recursively smaller n
  apply {n = suc n} g t = inst g t >>= apply g
    where
      -- Easy way of discarding the last variable of a Fin n.
      -- Mainly, we map Fin (1 + n) to 1 + Fin n.
      thin : {n : ℕ} → Fin (suc n) → Maybe (Fin n)
      thin {zero} _       = nothing
      thin {suc n} fz     = just fz
      thin {suc n} (fs x) with thin x
      ...| nothing = nothing
      ...| just x' = just (fs x')

      -- Given a closed term t, returns a substitution σ defined
      -- by σ(n+1) = t, σ(k, k ≤ n) = var k.
      ▵_ : {n : ℕ} → RTerm ⊥ → Fin (suc n) → RTerm (Fin n)
      ▵_ {n} t x with thin x
      ...| nothing = replace-A (λ ()) t
      ...| just x' = ovar x'

      {-# TERMINATING #-}
      mk-inst-f : {n : ℕ} → RTerm ⊥ → NonDet (Fin (suc n) → RTerm (Fin n))
      mk-inst-f (ovar ())
      mk-inst-f (ivar n) = return (▵ (ivar n))
      mk-inst-f (rlit l) = return (▵ (rlit l))
      mk-inst-f (rlam t) with height (rlam t) ≤? maxH
      ...| yes _ = return (▵ (rlam t)) ++ mk-inst-f t
      ...| no  _ = mk-inst-f t
      mk-inst-f (rapp n ts) with height (rapp n ts) ≤? maxH
      ...| yes _ = return (▵ (rapp n ts)) ++ concat (mapM mk-inst-f ts)
      ...| no  _ = concat (mapM mk-inst-f ts)

      -- Given a term t and a type with (n+1) variables, instantiate the last variable
      -- from the type with a non-deterministic subterm of t, returns the resulting type.
      inst : {n : ℕ} → RTerm ⊥ → RBinApp (Fin (suc n)) → NonDet (RBinApp (Fin n))
      inst {n} t (r , ty1 , ty2) = mk-inst-f {n} t >>= λ f → return (r , replace-A f ty1 , replace-A f ty2)

  -- TODO: Use vectors instead of lists...

  -- Given a goal (a ▵ b) and a list of types L, try to find intermediate goals g₁⋯gₙ such
  -- that ∀n . tyₙ ∈ L ⇒ tyₙ : gₙ₋₁ → gₙ , where g₀ = a and gₖ = b.
  divideGoal : RBinApp ⊥ → List (Σ ℕ (RBinApp ∘ Fin)) → Maybe (List (RTerm ⊥))
  divideGoal (gh , g1 , g2) l = sfHead (filter chainIsValid (stepGoals g1 l))
    where
      chainIsValid : List (RTerm ⊥) → Bool
      chainIsValid [] = false
      chainIsValid (x ∷ []) with x ≟-RTerm g2
      ...| yes _ = true
      ...| no  _ = false
      chainIsValid (x ∷ l) = chainIsValid l

      sfHead : {A : Set} → List A → Maybe A
      sfHead [] = nothing
      sfHead (x ∷ _) = just x

      -- Given a list of types, will return a possible list of goals that
      -- could be discharged by those types.
      stepGoals : RTerm ⊥ → List (Σ ℕ (RBinApp ∘ Fin)) → NonDet (List (RTerm ⊥))
      stepGoals g []       = return (g ∷ [])
      stepGoals g ((nₜ , t) ∷ ts) = apply g t ++ apply g (symmetric t)
                                >>= (λ g' → stepGoals g' ts
                                >>= return ∘ (_∷_ g))

  module Test where

    goal : RTerm ⊥
    goal = rapp (rdef (quote _≡_))
      (rapp (rdef (quote _+_)) (ivar 0 ∷ ivar 1 ∷ []) ∷
       rapp (rdef (quote _+_))
       (ivar 0 ∷
        rapp (rdef (quote _+_)) (ivar 1 ∷ rapp (rcon (quote zero)) [] ∷ [])
        ∷ [])
       ∷ [])

    binGoal : RBinApp ⊥
    binGoal = rdef (quote _≡_)
            , rapp (rdef (quote _+_)) (ivar 0 ∷ ivar 1 ∷ [])
            , rapp (rdef (quote _+_)) (ivar 0 ∷ (rapp (rdef (quote _+_)) (ivar 1 ∷ (rapp (rcon (quote zero)) []) ∷ []) ∷ []))

    +-ri : RBinApp (Fin 1)
    +-ri = rdef (quote _≡_)
         , rapp (rdef (quote _+_)) (ovar fz ∷ rapp (rcon (quote zero)) [] ∷ [])
         , ovar fz

    +-a : RBinApp (Fin 3)
    +-a = rdef (quote _≡_)
        , rapp (rdef (quote _+_)) (rapp (rdef (quote _+_)) (ovar (fs $ fs fz) ∷ ovar (fs fz) ∷ []) ∷ ovar fz ∷ [])
        , rapp (rdef (quote _+_)) (ovar (fs $ fs fz) ∷ rapp (rdef (quote _+_)) (ovar (fs fz) ∷ ovar fz ∷ []) ∷ [])

    tylist : List (Σ ℕ (RBinApp ∘ Fin))
    tylist = (1 , +-ri) ∷ (3 , +-a) ∷ []

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
{-# OPTIONS --prop --rewriting #-}

module Examples.Sorting.Sequential where

open import Examples.Sorting.Sequential.Comparable

open import Calf costMonoid
open import Calf.Types.Nat
open import Calf.Types.List

open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
open import Data.Product using (_,_)

test/forward  = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ 10 ∷ 11 ∷ 12 ∷ 13 ∷ 14 ∷ 15 ∷ 16 ∷ []
test/backward = 16 ∷ 15 ∷ 14 ∷ 13 ∷ 12 ∷ 11 ∷ 10 ∷ 9 ∷ 8 ∷ 7 ∷ 6 ∷ 5 ∷ 4 ∷ 3 ∷ 2 ∷ 1 ∷ []
test/shuffled = 4 ∷ 8 ∷ 12 ∷ 16 ∷ 13 ∷ 3 ∷ 5 ∷ 14 ∷ 9 ∷ 6 ∷ 7 ∷ 10 ∷ 11 ∷ 1 ∷ 2 ∷ 15 ∷ []

module Ex/InsertionSort where
  import Examples.Sorting.Sequential.InsertionSort NatComparable as Sort

  list' = list nat

  ex/insert : cmp (F list')
  ex/insert = Sort.insert 3 (1 ∷ 2 ∷ 4 ∷ [])

  ex/sort : cmp (F list')
  ex/sort = Sort.sort (1 ∷ 5 ∷ 3 ∷ 1 ∷ 2 ∷ [])

  ex/sort/forward : cmp (F list')
  ex/sort/forward = Sort.sort test/forward  -- cost: 15

  ex/sort/backward : cmp (F list')
  ex/sort/backward = Sort.sort test/backward  -- cost: 120

  ex/sort/shuffled : cmp (F list')
  ex/sort/shuffled = Sort.sort test/shuffled  -- cost: 76

module Ex/MergeSort where
  import Examples.Sorting.Sequential.MergeSort NatComparable as Sort

  list' = list nat

  ex/split : cmp (F Sort.pair)
  ex/split = Sort.split (6 ∷ 2 ∷ 8 ∷ 3 ∷ 1 ∷ 8 ∷ 5 ∷ [])

  ex/merge : cmp (F list')
  ex/merge = Sort.merge (2 ∷ 3 ∷ 6 ∷ 8 ∷ [] , 1 ∷ 5 ∷ 8 ∷ [])

  ex/sort : cmp (F list')
  ex/sort = Sort.sort (1 ∷ 5 ∷ 3 ∷ 1 ∷ 2 ∷ [])

  ex/sort/forward : cmp (F list')
  ex/sort/forward = Sort.sort test/forward  -- cost: 32

  ex/sort/backward : cmp (F list')
  ex/sort/backward = Sort.sort test/backward  -- cost: 32

  ex/sort/shuffled : cmp (F list')
  ex/sort/shuffled = Sort.sort test/shuffled  -- cost: 47

module SortEquivalence (M : Comparable) where
  open Comparable M
  open import Examples.Sorting.Sequential.Core M

  import Examples.Sorting.Sequential.InsertionSort M as ISort
  import Examples.Sorting.Sequential.MergeSort     M as MSort

  isort≡msort : ◯ (ISort.sort ≡ MSort.sort)
  isort≡msort = IsSort⇒≡ ISort.sort ISort.sort/correct MSort.sort MSort.sort/correct

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

-- From: On the Bright Side of Type Classes: Instances Arguments in
-- Agda (ICFP'11).

module InstanceArguments where

open import Data.Bool.Base
open import Data.Nat hiding ( equal ) renaming ( suc to succ )

-- Note: Agda doesn't have a primitive function primBoolEquality.
boolEq : Bool → Bool → Bool
boolEq true  true  = true
boolEq false false = true
{-# CATCHALL #-}
boolEq _     _     = false

natEq : ℕ → ℕ → Bool
natEq zero  zero         = true
natEq (succ m) (succ n)  = natEq m n
{-# CATCHALL #-}
natEq _     _            = false

record Eq (t : Set) : Set where
  field equal : t → t → Bool

instance
  eqInstanceBool : Eq Bool
  eqInstanceBool = record { equal = boolEq }

  eqInstanceℕ : Eq ℕ
  eqInstanceℕ = record { equal = natEq }

equal : {t : Set} → {{eqT : Eq t}} → t → t → Bool
equal {{eqT}} = Eq.equal eqT

test : Bool
test = equal 5 3 ∨ equal true false

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

open import AISEC.Utils
open import Data.Real as ℝ using (ℝ)
open import Data.List

module MyTestModule where

f : Tensor ℝ (1 ∷ []) → Tensor ℝ (1 ∷ [])
f = evaluate record
  { databasePath = DATABASE_PATH
  ; networkUUID  = NETWORK_UUID
  }

increasing : ∀ (x : Tensor ℝ (1 ∷ [])) → let y = f (x) in x 0 ℝ.≤ y 0
increasing = checkProperty record
  { databasePath = DATABASE_PATH
  ; propertyUUID = ????
  }

max_stars_repo_name: Yiergot/vehicle

max_issues_repo_name: Yiergot/vehicle

max_forks_repo_name: Yiergot/vehicle


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some specialised instances of the ring solver
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

-- Here, we provide proofs of homomorphism between the operations
-- defined on polynomials and those on the underlying ring.

module Tactic.RingSolver.Core.Polynomial.Homomorphism
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

-- The lemmas are the general-purpose proofs we reuse in each other section
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas         homo using (pow-cong) public

-- Proofs for each component of the polynomial
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition       homo using (⊞-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication homo using (⊠-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation       homo using (⊟-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation homo using (⊡-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants      homo using (κ-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables      homo using (ι-hom) public


text:
{-
This module contains
- the type of vertical composition operations
  that can be defined on a reflexive graph

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.VertComp where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Structures.Constant

open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.ReflGraph

open MorphismLemmas
open GroupLemmas

private
  variable
    ℓ ℓ' : Level

{-
-- The type of vertical composition operations
-- that can be defined over a reflexive graph 𝒢
--

-- we use the property isComposable instead of defining
-- a type of composable morphisms of G₁, because
-- otherwise it would be difficult to formulate
-- properties involving an odd number of composable morphisms
-- in a uniform and clean way.
-}
record VertComp (𝒢 : ReflGraph ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  no-eta-equality
  constructor vertcomp
  open ReflGraphNotation 𝒢
  open ReflGraphLemmas 𝒢

  -- the vertical composition operation with convenient syntax
  field
    vcomp : (g f : ⟨ G₁ ⟩) → isComposable g f → ⟨ G₁ ⟩
  syntax vcomp g f p = g ∘⟨ p ⟩ f

  field
    -- vcomp preserves source and target
    σ-∘ : (g f : ⟨ G₁ ⟩) (c : isComposable g f) → s (g ∘⟨ c ⟩ f) ≡ s f
    τ-∘ : (g f : ⟨ G₁ ⟩) (c : isComposable g f) → t (g ∘⟨ c ⟩ f) ≡ t g
    -- vcomp is a homomorphism, also known as interchange law
    isHom-∘ : (g f : ⟨ G₁ ⟩) (c : isComposable g f)
              (g' f' : ⟨ G₁ ⟩) (c' : isComposable g' f')
              (c'' : isComposable (g +₁ g') (f +₁ f'))
              → (g +₁ g') ∘⟨ c'' ⟩ (f +₁ f') ≡ (g ∘⟨ c ⟩ f) +₁ (g' ∘⟨ c' ⟩ f')
    -- vcomp is associative
    assoc-∘ : (h g f : ⟨ G₁ ⟩)
              (c-hg : isComposable h g)
              (c-gf  : isComposable g f)
              (c-h-gf : isComposable h (g ∘⟨ c-gf ⟩ f))
              (c-hg-f : isComposable (h ∘⟨ c-hg ⟩ g) f)
              → h ∘⟨ c-h-gf ⟩ (g ∘⟨ c-gf ⟩ f) ≡ (h ∘⟨ c-hg ⟩ g) ∘⟨ c-hg-f ⟩ f
    -- composing with identity arrows does nothing
    lid-∘ : (f : ⟨ G₁ ⟩) (c : isComposable (𝒾 (t f)) f)
            → 𝒾 (t f) ∘⟨ c ⟩ f ≡ f
    rid-∘ : (g : ⟨ G₁ ⟩) (c : isComposable g (𝒾 (s g))) → g ∘⟨ c ⟩ 𝒾 (s g) ≡ g

    -- alternative lid/rid definition, but taking paramter c is more flexible
    -- lid-∘ : (f : ⟨ G₁ ⟩) → 𝒾 (t f) ∘⟨ σι-≡-fun (t f) ⟩ f ≡ f
    -- assoc-∘ : (h g f : ⟨ G₁ ⟩) (c : isComposable h g) (c' : isComposable g f)
    --         → h ∘⟨ c ∙ sym (τ-∘ g f c') ⟩ (g ∘⟨ c' ⟩ f) ≡ (h ∘⟨ c ⟩ g) ∘⟨ σ-∘ h g c ∙ c' ⟩ f
               -- → h ∘⟨ c-hg ∙ sym (τ-∘ g f c-gf) ⟩ (g ∘⟨ c-gf ⟩ f)
               --  ≡ (h ∘⟨ c-hg ⟩ g) ∘⟨ σ-∘ h g c-hg ∙ c-gf ⟩ f

module _ {𝒢 : ReflGraph ℓ ℓ'} where
  open ReflGraphNotation 𝒢
  open ReflGraphLemmas 𝒢

  -- lemmas about a given vertical composition
  module _ (𝒞 : VertComp 𝒢) where

    open VertComp 𝒞

    -- These are all propositions, so we use abstract.
    -- Most of these lemmas are nontrivial, because we need to keep a
    -- proof of composability at hand.
    abstract
      -- if (g, f), and (g', f') are composable,
      -- then so is (g + g', f + f')
      +-c : (g f : ⟨ G₁ ⟩) (c : isComposable g f)
           (g' f' : ⟨ G₁ ⟩) (c' : isComposable g' f')
           → isComposable (g +₁ g') (f +₁ f')
      +-c g f c g' f' c' = σ .isHom g g'
                          ∙∙ cong (_+₀ s g') c
                          ∙∙ cong (t f +₀_) c'
                          ∙ sym (τ .isHom f f')

      -- if (g, f) is composable, and g ≡ g',
      -- then (g', f) is composable
      ∘-cong-l-c : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
                  {g' : ⟨ G₁ ⟩} (p : g ≡ g')
                  → isComposable g' f
      ∘-cong-l-c c p = cong s (sym p) ∙ c

      -- if (g, f) is composable, and f ≡ f',
      -- then (g, f') is composable
      ∘-cong-r-c : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
                  {f' : ⟨ G₁ ⟩} (p : f ≡ f')
                  → isComposable g f'
      ∘-cong-r-c c p = c ∙ cong t p

      -- if (g, f) are composable, and (g, f) ≡ (g', f'),
      -- then (g', f') is composable
      -- by combining the two lemmas above
      ∘-cong-c : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
                {g' f' : ⟨ G₁ ⟩} (p : g ≡ g') (q : f ≡ f')
                  → isComposable g' f'
      ∘-cong-c c p q = ∘-cong-l-c c p ∙ cong t q

      -- if (g, f) is composable, and g ≡ g',
      -- then g ∘ f ≡ g' ∘ f
      ∘-cong-l : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
                {g' : ⟨ G₁ ⟩} (p : g ≡ g')
                → g ∘⟨ c ⟩ f ≡ g' ∘⟨ ∘-cong-l-c c p ⟩ f
      ∘-cong-l {g = g} {f = f} c {g'} p = cong₂ (λ h d → h ∘⟨ d ⟩ f)
                                               p
                                               (toPathP (isPropIsComposable g'
                                                                            f
                                                                            (transp (λ i → isComposable (p i) f) i0 c)
                                                                            (∘-cong-l-c c p)))

      -- if (g, f) is composable, and f ≡ f',
      -- then g ∘ f ≡ g ∘ f'
      ∘-cong-r : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
                {f' : ⟨ G₁ ⟩} (p : f ≡ f')
                → g ∘⟨ c ⟩ f ≡ g ∘⟨ ∘-cong-r-c c p ⟩ f'
      ∘-cong-r {g = g} c {f'} p = cong₂ (λ h d → g ∘⟨ d ⟩ h)
                                  p
                                  (toPathP (isPropIsComposable g
                                                               f'
                                                               (transp (λ i → isComposable g (p i)) i0 c)
                                                               (∘-cong-r-c c p)))

      -- if (g, f) are composable, and (g, f) ≡ (g', f'),
      -- then g ∘ f ≡ g' ∘ f'
      ∘-cong : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
                {g' f' : ⟨ G₁ ⟩} (p : g ≡ g') (q : f ≡ f')
                → g ∘⟨ c ⟩ f ≡ g' ∘⟨ ∘-cong-c c p q ⟩ f'
      ∘-cong c p q = ∘-cong-l c p
                    ∙ ∘-cong-r (∘-cong-l-c c p) q

      -- an alternate version of lid-∘
      -- where a composable g is assumed and ι (σ g)
      -- instead of ι (τ f) is used
      ∘-lid' : {g f : ⟨ G₁ ⟩} (c : isComposable g f)
              (c' : isComposable (𝒾s g) f)
              → (𝒾s g) ∘⟨ c' ⟩ f ≡ f
      ∘-lid' {g} {f} c c' = (𝒾s g) ∘⟨ c' ⟩ f
                               ≡⟨ ∘-cong-l c' (cong 𝒾 c) ⟩
                           𝒾t f ∘⟨ ∘-cong-l-c c' (cong 𝒾 c) ⟩ f
                               ≡⟨ lid-∘ f (∘-cong-l-c c' (cong 𝒾 c)) ⟩
                           f ∎

      -- Fundamental theorem:
      -- Any vertical composition is necessarily of the form
      -- g ∘⟨ _ ⟩ f  ≡ g - ι (σ g) + f
      -- This implies contractibility of VertComp 𝒢
      VertComp→+₁ : (g f : ⟨ G₁ ⟩) (c : isComposable g f)
                   → g ∘⟨ c ⟩ f ≡ (g -₁ 𝒾s g) +₁ f
      VertComp→+₁ g f c = g ∘⟨ c ⟩ f
                           ≡⟨ ∘-cong c
                                     (sym (rId₁ g) ∙ cong (g +₁_) (sym (lCancel₁ isg)))
                                     (sym (lId₁ f) ∙ cong (_+₁ f) (sym (rCancel₁ isg))) ⟩
                         (g +₁ (-isg +₁ isg)) ∘⟨ c₁ ⟩ ((isg -₁ isg) +₁ f)
                           ≡⟨ ∘-cong-l c₁ (assoc₁ g -isg isg) ⟩
                         ((g -₁ isg) +₁ isg) ∘⟨ c₂ ⟩ ((isg -₁ isg) +₁ f)
                           ≡⟨ isHom-∘ (g -₁ isg) (isg -₁ isg) c₄
                                      isg f c₃
                                      c₂ ⟩
                         ((g +₁ -isg) ∘⟨ c₄ ⟩ (isg +₁ -isg)) +₁ (isg ∘⟨ c₃ ⟩ f)
                           ≡⟨ cong (_+₁ (isg ∘⟨ c₃ ⟩ f))
                                   (isHom-∘ g isg c₅ -isg -isg c₆ c₄) ⟩
                         ((g ∘⟨ c₅ ⟩ isg) +₁ (-isg ∘⟨ c₆ ⟩ -isg)) +₁ (isg ∘⟨ c₃ ⟩ f)
                           ≡⟨ cong (λ z → (z +₁ (-isg ∘⟨ c₆ ⟩ -isg)) +₁ (isg ∘⟨ c₃ ⟩ f))
                                    (rid-∘ g (isComp-g-isg g)) ⟩
                         (g +₁ (-isg ∘⟨ c₆ ⟩ -isg)) +₁ (isg ∘⟨ c₃ ⟩ f)
                           ≡⟨ cong ((g +₁ (-isg ∘⟨ c₆ ⟩ -isg)) +₁_)
                                   (∘-lid' c c₃) ⟩
                         (g +₁ (-isg ∘⟨ c₆ ⟩ -isg)) +₁ f
                           ≡⟨ cong (λ z → (g +₁ z) +₁ f)
                                   (-isg ∘⟨ c₆ ⟩ -isg
                                     ≡⟨ ∘-cong-r c₆
                                                 -- prove that is(-isg)≡-isg
                                                 (sym (cong 𝒾s (sym (mapInv ι (s g)))
                                                      ∙∙ cong 𝒾 (σι-≡-fun (-₀ s g))
                                                      ∙∙ mapInv ι (s g))) ⟩
                                   -isg ∘⟨ c₈ ⟩ (𝒾s -isg)
                                     ≡⟨ rid-∘ -isg c₈ ⟩
                                   -isg ∎) ⟩
                         (g -₁ isg) +₁ f ∎
                         where
                           -- abbreviations to reduce the amount of parentheses
                           isg = 𝒾s g
                           -isg = -₁ isg
                           itf = 𝒾t f
                           -- composability proofs,
                           -- none of which are really interesting.
                           c₁ : isComposable (g +₁ (-isg +₁ isg)) ((isg -₁ isg) +₁ f)
                           c₁ = ∘-cong-c c
                                         (sym (rId₁ g) ∙ cong (g +₁_) (sym (lCancel₁ isg)))
                                         (sym (lId₁ f) ∙ cong (_+₁ f) (sym (rCancel₁ isg)))
                           c₂ : isComposable ((g -₁ isg) +₁ isg) ((isg -₁ isg) +₁ f)
                           c₂ = ∘-cong-l-c c₁ (assoc₁ g -isg isg)
                           c₃ : isComposable isg f
                           c₃ = σι-≡-fun (s g) ∙ c
                           c₄ : isComposable (g -₁ isg) (isg -₁ isg)
                           c₄ = s (g -₁ isg)
                                  ≡⟨ σ-g--isg g ⟩
                                0₀
                                  ≡⟨ sym (cong t (rCancel₁ isg) ∙ mapId τ) ⟩
                                t (isg -₁ isg) ∎
                           c₅ : isComposable g isg
                           c₅ = isComp-g-isg g
                           c₆ : isComposable -isg -isg
                           c₆ = s -isg
                                  ≡⟨ mapInv σ isg ⟩
                                -₀ (s isg)
                                  ≡⟨ cong -₀_ (σι-≡-fun (s g)) ⟩
                                -₀ (s g)
                                  ≡⟨ cong -₀_ (sym (τι-≡-fun (s g))) ⟩
                                -₀ (t isg)
                                  ≡⟨ sym (mapInv τ isg) ⟩
                                t -isg ∎
                           c₈ : isComposable -isg (𝒾s -isg)
                           c₈ = ∘-cong-r-c c₆
                                           (sym (cong 𝒾s (sym (mapInv ι (s g)))
                                             ∙∙ cong 𝒾 (σι-≡-fun (-₀ s g))
                                             ∙∙ mapInv ι (s g)))

      -- properties of the interchange law
      IC2 : (g g' f : ⟨ G₁ ⟩) (c-gf : isComposable g f)
           →  (g' +₁ (-is g' -₁ is g)) +₁ f ≡ (-is g +₁ f) +₁ (g' -₁ is g')
      IC2 g g' f c-gf =
       (g' +₁ (-isg' +₁ -isg)) +₁ f
         ≡⟨ cong ((g' +₁ (-isg' +₁ -isg)) +₁_)
                 (sym (rCancel-rId G₁ f f') ∙ assoc₁ f f' -f') ⟩
       (g' +₁ (-isg' +₁ -isg)) +₁ ((f +₁ f') -₁ f')
         ≡⟨ assoc₁ (g' +₁ (-isg' +₁ -isg)) (f +₁ f') (-₁ f') ⟩
       ((g' +₁ (-isg' +₁ -isg)) +₁ (f +₁ f')) -₁ f'
         ≡⟨ cong (_-₁ f')
            (sym (lCancel-lId G₁ g _)) ⟩
       ((-g +₁ g) +₁ ((g' +₁ (-isg' +₁ -isg)) +₁ (f +₁ f'))) -₁ f'
         ≡⟨ cong (_-₁ f')
                 (sym (assoc₁ -g g _)) ⟩
       (-g +₁ (g +₁ ((g' +₁ (-isg' +₁ -isg)) +₁ (f +₁ f')))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ z) -₁ f')
                 (assoc₁ g _ (f +₁ f')) ⟩
       (-g +₁ ((g +₁ (g' +₁ (-isg' +₁ -isg))) +₁ (f +₁ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ (z +₁ (f +₁ f'))) -₁ f')
                 (assoc₁ g g' (-isg' -₁ isg)) ⟩
       (-g +₁ (((g +₁ g') +₁ (-isg' +₁ -isg)) +₁ (f +₁ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ z) -₁ f')
                 (sym q) ⟩
       (-g +₁ ((g +₁ g') ∘⟨ c-gf'+ ⟩ (f +₁ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ z) -₁ f')
                 (isHom-∘ g f c-gf
                          g' f' c-gf'
                          c-gf'+) ⟩
       (-g +₁ ((g ∘⟨ c-gf ⟩ f) +₁ (g' ∘⟨ c-gf' ⟩ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ ((g ∘⟨ c-gf ⟩ f) +₁ z)) -₁ f')
                 (VertComp→+₁ g' f' c-gf') ⟩
       (-g +₁ ((g ∘⟨ c-gf ⟩ f) +₁ ((g' -₁ isg') +₁ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ (z +₁ ((g' -₁ isg') +₁ f'))) -₁ f')
                 (VertComp→+₁ g f c-gf) ⟩
       (-g +₁ (((g -₁ isg) +₁ f) +₁ ((g' -₁ isg') +₁ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ (z +₁ ((g' -₁ isg') +₁ f'))) -₁ f')
                 (sym (assoc₁ g -isg f)) ⟩
       (-g +₁ ((g +₁ (-isg +₁ f)) +₁ ((g' -₁ isg') +₁ f'))) -₁ f'
         ≡⟨ cong (λ z → (-g +₁ z) -₁ f')
                 (sym (assoc₁ g (-isg +₁ f) _)) ⟩
       (-g +₁ (g +₁ ((-isg +₁ f) +₁ ((g' -₁ isg') +₁ f')))) -₁ f'
         ≡⟨ cong (_-₁ f')
                 (assoc₁ -g g _) ⟩
       ((-g +₁ g) +₁ ((-isg +₁ f) +₁ ((g' -₁ isg') +₁ f'))) -₁ f'
         ≡⟨ cong (_-₁ f')
            (lCancel-lId G₁ g _) ⟩
       ((-isg +₁ f) +₁ ((g' -₁ isg') +₁ f')) -₁ f'
         ≡⟨ sym (assoc₁ (-isg +₁ f) _ -f') ⟩
       (-isg +₁ f) +₁ (((g' -₁ isg') +₁ f') -₁ f')
         ≡⟨ cong ((-isg +₁ f) +₁_)
                 (sym (assoc₁ (g' -₁ isg') f' -f')) ⟩
       (-isg +₁ f) +₁ ((g' -₁ isg') +₁ (f' -₁ f'))
         ≡⟨ cong ((-isg +₁ f) +₁_ )
                 (rCancel-rId G₁ (g' -₁ isg') f') ⟩
       (-isg +₁ f) +₁ (g' -₁ isg') ∎
       where
         -- abbreviations to reduce the number of parentheses
         -g = -₁ g
         isg = 𝒾s g
         isg' = 𝒾s g'
         -isg = -₁ isg
         -isg' = -₁ isg'
         f' = isg'
         -f' = -₁ f'
         -- composability proofs
         c-gf' = isComp-g-isg g'
         c-gf'+ = +-c g f c-gf g' f' c-gf'
         --
         q = (g +₁ g') ∘⟨ c-gf'+ ⟩ (f +₁ f')
               ≡⟨ VertComp→+₁ (g +₁ g') (f +₁ f') c-gf'+ ⟩
             ((g +₁ g') -₁ (𝒾s (g +₁ g'))) +₁ (f +₁ f')
               ≡⟨ cong (λ z → ((g +₁ g') -₁ z) +₁ (f +₁ f'))
                       (ι∘σ .isHom g g') ⟩
             ((g +₁ g') -₁ (isg +₁ isg')) +₁ (f +₁ f')
               ≡⟨ cong (λ z → ((g +₁ g') +₁ z) +₁ (f +₁ f'))
                       (invDistr G₁ isg isg') ⟩
             ((g +₁ g') +₁ (-isg' +₁ -isg)) +₁ (f +₁ f') ∎

      IC3 : (g g' f : ⟨ G₁ ⟩) (c-gf : isComposable g f)
            → (-₁ f) +₁ ((is g +₁ is g') -₁ g') ≡ (is g' -₁ g') +₁ ((-₁ f) +₁ is g)
      IC3 g g' f c-gf =
        -f +₁ ((isg +₁ isg') -₁ g')
          ≡⟨ cong (λ z → -f +₁ ((isg +₁ z) -₁ g'))
                  (sym (invInvo G₁ isg')) ⟩
        -f +₁ ((isg -₁ -isg') -₁ g')
          ≡⟨ cong (λ z → -f +₁ ((z -₁ -isg') -₁ g'))
                  (sym (invInvo G₁ isg)) ⟩
        -f +₁ (((-₁ -isg) -₁ -isg') -₁ g')
          ≡⟨ cong (λ z → -f +₁ (z -₁ g'))
                  (sym (invDistr G₁ -isg' -isg)) ⟩
        -f +₁ ((-₁ (-isg' +₁ -isg)) -₁ g')
          ≡⟨ cong (λ z → -f +₁ z)
                  (sym (invDistr G₁ g' (-isg' +₁ -isg))) ⟩
        -f -₁ (g' +₁ (-isg' +₁ -isg))
          ≡⟨ sym (invDistr G₁ _ f) ⟩
        -₁ ((g' +₁ (-isg' +₁ -isg)) +₁ f)
          ≡⟨ cong -₁_
                  (IC2 g g' f c-gf) ⟩
        -₁ ((-isg +₁ f) +₁ (g' -₁ isg'))
          ≡⟨ invDistr G₁ (-isg +₁ f) (g' -₁ isg') ⟩
        (-₁ (g' -₁ isg')) +₁ (-₁ (-isg +₁ f))
          ≡⟨ cong ((-₁ (g' -₁ isg')) +₁_)
                  (invDistr G₁ -isg f) ⟩
        (-₁ (g' -₁ isg')) +₁ (-f -₁ -isg)
          ≡⟨ cong (_+₁ (-f -₁ -isg))
                  (invDistr G₁ g' -isg') ⟩
        ((-₁ -isg') -₁ g') +₁ (-f -₁ -isg)
          ≡⟨ cong (λ z → (z -₁ g') +₁ (-f -₁ -isg))
                  (invInvo G₁ isg') ⟩
        (isg' -₁ g') +₁ (-f -₁ -isg)
          ≡⟨ cong (λ z → (isg' -₁ g') +₁ (-f +₁ z))
                  (invInvo G₁ isg) ⟩
        (isg' -₁ g') +₁ (-f +₁ isg) ∎
        where
          -f = -₁ f
          -g = -₁ g
          isg = 𝒾s g
          isg' = 𝒾s g'
          -isg = -₁ isg
          -isg' = -₁ isg'

      IC4 : (g g' f : ⟨ G₁ ⟩) (c-gf : isComposable g f)
            → f +₁ (((-is g) -₁ (is g')) +₁ g') ≡ ((-is g') +₁ g') +₁ (f -₁ (is g))
      IC4 g g' f c-gf =
        f +₁ ((-isg -₁ isg') +₁ g')
          ≡⟨ cong (λ z → f +₁ ((-isg -₁ isg') +₁ z))
                  (sym (invInvo G₁ g')) ⟩
        (f +₁ ((-isg -₁ isg') -₁ -g'))
          ≡⟨ cong (λ z → f +₁ ((-isg +₁ z) -₁ -g'))
                  (sym (mapInv ι∘σ g')) ⟩
        f +₁ ((-isg +₁ (is- g')) -₁ -g')
          ≡⟨ cong (λ z → f +₁ ((z +₁ (is- g')) -₁ -g'))
                  (sym (mapInv ι∘σ g)) ⟩
        f +₁ (((is- g) +₁ (is- g')) -₁ -g')
          ≡⟨ cong (_+₁ ((is- g +₁ is- g') -₁ -g'))
                  (sym (invInvo G₁ f)) ⟩
        (-₁ -f) +₁ (((is- g) +₁ (is- g')) -₁ -g')
          ≡⟨ IC3 -g -g' -f c--gf ⟩
        ((is- g') -₁ -g') +₁ ((-₁ -f) +₁ (is- g))
          ≡⟨ cong (λ z → (z -₁ -g') +₁ ((-₁ -f) +₁ (is- g)))
                  (mapInv ι∘σ g') ⟩
        (-isg' -₁ -g') +₁ ((-₁ -f) +₁ (is- g))
          ≡⟨ cong (λ z → (-isg' +₁ z) +₁ ((-₁ -f) +₁ (is- g)))
                  (invInvo G₁ g') ⟩
        (-isg' +₁ g') +₁ ((-₁ -f) +₁ (is- g))
          ≡⟨ cong (λ z → (-isg' +₁ g') +₁ (z +₁ (is- g)))
                  (invInvo G₁ f) ⟩
        (-isg' +₁ g') +₁ (f +₁ (is- g))
          ≡⟨ cong (λ z → (-isg' +₁ g') +₁ (f +₁ z))
                  (mapInv ι∘σ g) ⟩
        (-isg' +₁ g') +₁ (f -₁ isg) ∎
        where
          -f = -₁ f
          -g = -₁ g
          -g' = -₁ g'
          isg = 𝒾s g
          isg' = 𝒾s g'
          -isg = -₁ isg
          -isg' = -₁ isg'
          c--gf = s -g
                    ≡⟨ mapInv σ g ⟩
                  -₀ (s g)
                    ≡⟨ cong -₀_ c-gf ⟩
                  -₀ (t f)
                    ≡⟨ sym (mapInv τ f) ⟩
                  t -f ∎
      -- g = itf
      IC5 : (g' f : ⟨ G₁ ⟩)
            → f +₁ (((-it f) -₁ (is g')) +₁ g') ≡ ((-is g') +₁ g') +₁ (f -₁ (it f))
      IC5 g' f =
        f +₁ ((-itf -₁ isg') +₁ g')
          ≡⟨ cong (λ z → f +₁ (((-₁ (𝒾 z)) -₁ isg') +₁ g'))
                  (sym c-gf) ⟩
        f +₁ ((-isg -₁ isg') +₁ g')
          ≡⟨ IC4 g g' f c-gf ⟩
        (-isg' +₁ g') +₁ (f -₁ isg)
          ≡⟨ cong (λ z → (-isg' +₁ g') +₁ (f -₁ (𝒾 z)))
                  c-gf ⟩
        (-isg' +₁ g') +₁ (f -₁ itf) ∎
        where
          -f = -₁ f
          -itf = -it f
          itf = it f
          g = it f
          -g = -₁ g
          -g' = -₁ g'
          isg = 𝒾s g
          isg' = 𝒾s g'
          -isg = -₁ isg
          -isg' = -₁ isg'
          c-gf : isComposable g f
          c-gf = isComp-itf-f f

  open VertComp

  -- the record VertComp has no eta equality, so this can be used to
  -- construct paths between vertical compositions
  η-VertComp : (𝒱 : VertComp 𝒢) → vertcomp (vcomp 𝒱) (σ-∘ 𝒱) (τ-∘ 𝒱) (isHom-∘ 𝒱) (assoc-∘ 𝒱) (lid-∘ 𝒱) (rid-∘ 𝒱) ≡ 𝒱
  vcomp (η-VertComp 𝒱 i) = vcomp 𝒱
  σ-∘ (η-VertComp 𝒱 i) = σ-∘ 𝒱
  τ-∘ (η-VertComp 𝒱 i) = τ-∘ 𝒱
  isHom-∘ (η-VertComp 𝒱 i) = isHom-∘ 𝒱
  assoc-∘ (η-VertComp 𝒱 i) = assoc-∘ 𝒱
  lid-∘(η-VertComp 𝒱 i) = lid-∘ 𝒱
  rid-∘ (η-VertComp 𝒱 i) = rid-∘ 𝒱

  -- this is just a helper for the module below
  module _ (𝒞 𝒞' : VertComp 𝒢) where
    p∘ : vcomp 𝒞 ≡ vcomp 𝒞'
    p∘ = funExt₃ (λ g f c → VertComp→+₁ 𝒞 g f c ∙ sym (VertComp→+₁ 𝒞' g f c))

    pσ : PathP (λ j → (g f : ⟨ G₁ ⟩) (c : isComposable g f) → s (p∘ j g f c) ≡ s f) (σ-∘ 𝒞) (σ-∘ 𝒞')
    pσ = isProp→PathP (λ i → isPropΠ3 (λ g f c → set₀ (s (p∘ i g f c)) (s f))) (σ-∘ 𝒞) (σ-∘ 𝒞')

    passoc : PathP (λ i → (h g f : ⟨ G₁ ⟩)
                          (c-hg : isComposable h g)
                          (c-gf : isComposable g f)
                          (c-h-gf : isComposable h (p∘ i g f c-gf))
                          (c-hg-f : isComposable (p∘ i h g c-hg) f) →
                          p∘ i h (p∘ i g f c-gf) c-h-gf ≡ p∘ i (p∘ i h g c-hg) f c-hg-f) (assoc-∘ 𝒞) (assoc-∘ 𝒞')
    passoc = isProp→PathP (λ j → isPropΠ4 (λ h g f c-hg → isPropΠ3 (λ c-gf c-h-gf c-hg-f → set₁ (p∘ j h (p∘ j g f c-gf) c-h-gf) (p∘ j (p∘ j h g c-hg) f c-hg-f)))) (assoc-∘ 𝒞) (assoc-∘ 𝒞')
    -- (p∘ j h (p∘ j g f c-gf) c-h-gf ≡ p∘ j (p∘ j h g c-hg) f c-hg-f)

-- proof that there is at most one vertical composition on a reflexive graph
module _ (𝒢 : ReflGraph ℓ ℓ') where
  open ReflGraphNotation 𝒢
  open ReflGraphLemmas 𝒢
  open VertComp
  isPropVertComp : isProp (VertComp 𝒢)
  vcomp (isPropVertComp 𝒞 𝒞' i) = funExt₃ (λ g f c → VertComp→+₁ 𝒞 g f c ∙ sym (VertComp→+₁ 𝒞' g f c)) i
  -- σ-∘ (isPropVertComp 𝒞 𝒞' i) = funExt₃ P i
  σ-∘ (isPropVertComp 𝒞 𝒞' i) = pσ 𝒞 𝒞' i
    where
      P : (g f : ⟨ G₁ ⟩) (c : isComposable g f)
          → PathP (λ j → s (vcomp (isPropVertComp 𝒞 𝒞' j) g f c) ≡ s f)
                  (σ-∘ 𝒞 g f c)
                  (σ-∘ 𝒞' g f c)
      P g f c = isProp→PathP (λ j → set₀ (s (vcomp (isPropVertComp 𝒞 𝒞' j) g f c)) (s f)) (σ-∘ 𝒞 g f c) (σ-∘ 𝒞' g f c)
  τ-∘ (isPropVertComp 𝒞 𝒞' i) = funExt₃ P i
    where
      P : (g f : ⟨ G₁ ⟩) (c : isComposable g f) → PathP (λ j → t (vcomp (isPropVertComp 𝒞 𝒞' j) g f c) ≡ t g) (τ-∘ 𝒞 g f c) (τ-∘ 𝒞' g f c)
      P g f c = isProp→PathP (λ j → set₀ (t (vcomp (isPropVertComp 𝒞 𝒞' j) g f c)) (t g)) (τ-∘ 𝒞 g f c) (τ-∘ 𝒞' g f c)
  isHom-∘ (isPropVertComp 𝒞 𝒞' i) = funExt₃ (λ g f c → funExt₃ (λ g' f' c' → funExt (λ c+ → P g f c g' f' c' c+))) i
    where
      P : (g f : ⟨ G₁ ⟩) (c : isComposable g f)
          (g' f' : ⟨ G₁ ⟩) (c' : isComposable g' f')
          (c+ : isComposable (g +₁ g') (f +₁ f'))
          → PathP (λ j → vcomp (isPropVertComp 𝒞 𝒞' j) (g +₁ g') (f +₁ f') c+
                         ≡ (vcomp (isPropVertComp 𝒞 𝒞' j) g f c) +₁ (vcomp (isPropVertComp 𝒞 𝒞' j) g' f' c'))
                  (isHom-∘ 𝒞 g f c g' f' c' c+)
                  (isHom-∘ 𝒞' g f c g' f' c' c+)
      P g f c g' f' c' c+ = isProp→PathP (λ j → set₁ (vcomp (isPropVertComp 𝒞 𝒞' j) (g +₁ g') (f +₁ f') c+)
                                                     ((vcomp (isPropVertComp 𝒞 𝒞' j) g f c) +₁ (vcomp (isPropVertComp 𝒞 𝒞' j) g' f' c')))
                                         (isHom-∘ 𝒞 g f c g' f' c' c+)
                                         (isHom-∘ 𝒞' g f c g' f' c' c+)
  assoc-∘ (isPropVertComp 𝒞 𝒞' i) = passoc 𝒞 𝒞' i
  lid-∘ (isPropVertComp 𝒞 𝒞' i) = funExt₂ P i
    where
      P : (f : ⟨ G₁ ⟩) (c : isComposable (𝒾 (t f)) f)
          → PathP (λ j → vcomp (isPropVertComp 𝒞 𝒞' j) (𝒾 (t f)) f c ≡ f) (lid-∘ 𝒞 f c) (lid-∘ 𝒞' f c)
      P f c = isProp→PathP (λ j → set₁ (vcomp (isPropVertComp 𝒞 𝒞' j) (𝒾 (t f)) f c) f) (lid-∘ 𝒞 f c) (lid-∘ 𝒞' f c)
  rid-∘ (isPropVertComp 𝒞 𝒞' i) = funExt₂ P i
    where
      P : (g : ⟨ G₁ ⟩) (c : isComposable g (𝒾 (s g)))
          → PathP (λ j → vcomp (isPropVertComp 𝒞 𝒞' j) g (𝒾 (s g)) c ≡ g) (rid-∘ 𝒞 g c) (rid-∘ 𝒞' g c)
      P g c = isProp→PathP (λ j → set₁ (vcomp (isPropVertComp 𝒞 𝒞' j) g (𝒾 (s g)) c) g) (rid-∘ 𝒞 g c) (rid-∘ 𝒞' g c)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module FFI.Data.String where

import Agda.Builtin.String

String = Agda.Builtin.String.String

infixr 5 _++_
_++_ = Agda.Builtin.String.primStringAppend

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text: -- Dummy file.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Numeral.Natural.Prime.Proofs.Product where

import      Lvl
open import Data.Either as Either using ()
open import Functional
open import Lang.Instance
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Oper
open import Numeral.Natural.Prime
open import Numeral.Natural.Relation.Divisibility.Proofs.Product
open import Sets.PredicateSet renaming (_≡_ to _≡ₛ_)
open import Type

private variable a b : ℕ

-- The prime factors of a product is the prime factors of its factors.
product-primeFactors : PrimeFactor(a ⋅ b) ≡ₛ (PrimeFactor(a) ∪ PrimeFactor(b))
product-primeFactors = [↔]-intro l r where
  l : PrimeFactor(a ⋅ b) ⊇ (PrimeFactor(a) ∪ PrimeFactor(b))
  l{a}{b}{x} (Either.Left  intro) = intro ⦃ factor = divides-with-[⋅] {x}{a}{b} ([∨]-introₗ infer) ⦄
  l{a}{b}{x} (Either.Right intro) = intro ⦃ factor = divides-with-[⋅] {x}{a}{b} ([∨]-introᵣ infer) ⦄

  r : PrimeFactor(a ⋅ b) ⊆ (PrimeFactor(a) ∪ PrimeFactor(b))
  r{a}{b}{x} intro = Either.map (p ↦ intro ⦃ factor = p ⦄) (p ↦ intro ⦃ factor = p ⦄) (prime-divides-of-[⋅] {x}{a}{b} infer infer)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Nat
open import Prelude
open import core
open import contexts

module typ-dec where
  lemma-arr-l : ∀{t1 t2 t4} → t1 ==> t2 == t1 ==> t4 → t2 == t4
  lemma-arr-l refl = refl

  lemma-arr-r : ∀{t1 t2 t3} → t1 ==> t2 == t3 ==> t2 → t1 == t3
  lemma-arr-r refl = refl

  lemma-arr-b : ∀{t1 t2 t3 t4} → t1 ==> t2 == t3 ==> t4 → t1 == t3
  lemma-arr-b refl = refl

  lemma-prod-l : ∀{t1 t2 t4} → t1 ⊗ t2 == t1 ⊗ t4 → t2 == t4
  lemma-prod-l refl = refl

  lemma-prod-r : ∀{t1 t2 t3} → t1 ⊗ t2 == t3 ⊗ t2 → t1 == t3
  lemma-prod-r refl = refl

  lemma-prod-b : ∀{t1 t2 t3 t4} → t1 ⊗ t2 == t3 ⊗ t4 → t1 == t3
  lemma-prod-b refl = refl

  -- types are decidable
  typ-dec : dec typ
  typ-dec b b = Inl refl
  typ-dec b ⦇·⦈ = Inr (λ ())
  typ-dec b (t2 ==> t3) = Inr (λ ())
  typ-dec ⦇·⦈ b = Inr (λ ())
  typ-dec ⦇·⦈ ⦇·⦈ = Inl refl
  typ-dec ⦇·⦈ (t2 ==> t3) = Inr (λ ())
  typ-dec (t1 ==> t2) b = Inr (λ ())
  typ-dec (t1 ==> t2) ⦇·⦈ = Inr (λ ())
  typ-dec (t1 ==> t2) (t3 ==> t4) with typ-dec t1 t3 | typ-dec t2 t4
  typ-dec (t1 ==> t2) (.t1 ==> .t2) | Inl refl | Inl refl = Inl refl
  typ-dec (t1 ==> t2) (.t1 ==> t4)  | Inl refl | Inr x₁   = Inr (λ x → x₁ (lemma-arr-l x))
  typ-dec (t1 ==> t2) (t3 ==> .t2)  | Inr x    | Inl refl = Inr (λ x₁ → x (lemma-arr-r x₁))
  typ-dec (t1 ==> t2) (t3 ==> t4)   | Inr x    | Inr x₁   = Inr (λ x₂ → x (lemma-arr-b x₂))
  typ-dec b (t2 ⊗ t3) = Inr (λ ())
  typ-dec ⦇·⦈ (t2 ⊗ t3) = Inr (λ ())
  typ-dec (t1 ==> t2) (t3 ⊗ t4) = Inr (λ ())
  typ-dec (t1 ⊗ t2) b = Inr (λ ())
  typ-dec (t1 ⊗ t2) ⦇·⦈ = Inr (λ ())
  typ-dec (t1 ⊗ t2) (t3 ==> t4) = Inr (λ ())
  typ-dec (t1 ⊗ t2) (t3 ⊗ t4) with typ-dec t1 t3 | typ-dec t2 t4
  typ-dec (t1 ⊗ t2) (.t1 ⊗ .t2) | Inl refl | Inl refl = Inl refl
  typ-dec (t1 ⊗ t2) (.t1 ⊗ t4)  | Inl refl | Inr x₁   = Inr (λ x → x₁ (lemma-prod-l x))
  typ-dec (t1 ⊗ t2) (t3 ⊗ .t2)  | Inr x    | Inl refl = Inr (λ x' → x (lemma-prod-r x'))
  typ-dec (t1 ⊗ t2) (t3 ⊗ t4)   | Inr x    | Inr x₁   = Inr (λ x' → x (lemma-prod-b x'))

  -- if an arrow is disequal, it disagrees in the first or second argument
  ne-factor : ∀{τ1 τ2 τ3 τ4} → (τ1 ==> τ2) ≠ (τ3 ==> τ4) → (τ1 ≠ τ3) + (τ2 ≠ τ4)
  ne-factor {τ1} {τ2} {τ3} {τ4} ne with typ-dec τ1 τ3 | typ-dec τ2 τ4
  ne-factor ne | Inl refl | Inl refl = Inl (λ x → ne refl)
  ne-factor ne | Inl x | Inr x₁ = Inr x₁
  ne-factor ne | Inr x | Inl x₁ = Inl x
  ne-factor ne | Inr x | Inr x₁ = Inl x

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda