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

module Definition.Conversion.Conversion where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.RedSteps
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Stability
open import Definition.Conversion.Soundness
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Reduction

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Conversion of algorithmic equality.
  convConv↑Term : ∀ {t u A B Γ Δ}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ A ≡ B
                → Γ ⊢ t [conv↑] u ∷ A
                → Δ ⊢ t [conv↑] u ∷ B
  convConv↑Term Γ≡Δ A≡B ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    let _ , ⊢B = syntacticEq A≡B
        B′ , whnfB′ , D′ = whNorm ⊢B
        B₁≡B′ = trans (sym (subset* D)) (trans A≡B (subset* (red D′)))
    in  [↑]ₜ B′ t′ u′ (stabilityRed* Γ≡Δ (red D′))
             (stabilityRed*Term Γ≡Δ (conv* d B₁≡B′))
             (stabilityRed*Term Γ≡Δ (conv* d′ B₁≡B′)) whnfB′ whnft′ whnfu′
             (convConv↓Term Γ≡Δ B₁≡B′ whnfB′ t<>u)

  -- Conversion of algorithmic equality with terms and types in WHNF.
  convConv↓Term : ∀ {t u A B Γ Δ}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ A ≡ B
                → Whnf B
                → Γ ⊢ t [conv↓] u ∷ A
                → Δ ⊢ t [conv↓] u ∷ B
  convConv↓Term Γ≡Δ A≡B whnfB (ℕ-ins x) rewrite ℕ≡A A≡B whnfB =
    ℕ-ins (stability~↓ Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (Empty-ins x) rewrite Empty≡A A≡B whnfB =
    Empty-ins (stability~↓ Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (Unit-ins x) rewrite Unit≡A A≡B whnfB =
    Unit-ins (stability~↓ Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (ne-ins t u x x₁) with ne≡A x A≡B whnfB
  convConv↓Term Γ≡Δ A≡B whnfB (ne-ins t u x x₁) | B , neB , PE.refl =
    ne-ins (stabilityTerm Γ≡Δ (conv t A≡B)) (stabilityTerm Γ≡Δ (conv u A≡B))
           neB (stability~↓ Γ≡Δ x₁)
  convConv↓Term Γ≡Δ A≡B whnfB (univ x x₁ x₂) rewrite U≡A A≡B =
    univ (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁) (stabilityConv↓ Γ≡Δ x₂)
  convConv↓Term Γ≡Δ A≡B whnfB (zero-refl x) rewrite ℕ≡A A≡B whnfB =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  zero-refl ⊢Δ
  convConv↓Term Γ≡Δ A≡B whnfB (suc-cong x) rewrite ℕ≡A A≡B whnfB =
    suc-cong (stabilityConv↑Term Γ≡Δ x)
  convConv↓Term Γ≡Δ A≡B whnfB (η-eq x₁ x₂ y y₁ x₃) with Π≡A A≡B whnfB
  convConv↓Term Γ≡Δ A≡B whnfB (η-eq x₁ x₂ y y₁ x₃) | F′ , G′ , PE.refl =
    let F≡F′ , G≡G′ = injectivity A≡B
    in  η-eq (stabilityTerm Γ≡Δ (conv x₁ A≡B))
             (stabilityTerm Γ≡Δ (conv x₂ A≡B)) y y₁
             (convConv↑Term (Γ≡Δ ∙ F≡F′) G≡G′ x₃)
  convConv↓Term Γ≡Δ A≡B whnfB (Σ-η ⊢p ⊢r pProd rProd fstConv sndConv)
    with Σ≡A A≡B whnfB
  ... | F , G , PE.refl =
    let F≡ , G≡ = Σ-injectivity A≡B
        ⊢F = proj₁ (syntacticEq F≡)
        ⊢G = proj₁ (syntacticEq G≡)
        ⊢fst = fstⱼ ⊢F ⊢G ⊢p
    in  Σ-η (stabilityTerm Γ≡Δ (conv ⊢p A≡B))
            (stabilityTerm Γ≡Δ (conv ⊢r A≡B))
            pProd
            rProd
            (convConv↑Term Γ≡Δ F≡ fstConv)
            (convConv↑Term Γ≡Δ (substTypeEq G≡ (refl ⊢fst)) sndConv)
  convConv↓Term Γ≡Δ A≡B whnfB (η-unit [t] [u] tUnit uUnit) rewrite Unit≡A A≡B whnfB =
    let [t] = stabilityTerm Γ≡Δ [t]
        [u] = stabilityTerm Γ≡Δ [u]
    in  η-unit [t] [u] tUnit uUnit

-- Conversion of algorithmic equality with the same context.
convConvTerm : ∀ {t u A B Γ}
              → Γ ⊢ t [conv↑] u ∷ A
              → Γ ⊢ A ≡ B
              → Γ ⊢ t [conv↑] u ∷ B
convConvTerm t<>u A≡B = convConv↑Term (reflConEq (wfEq A≡B)) A≡B t<>u


text:
module z05-00-internal-verification where

open import bool
open import eq
open import nat
open import nat-thms
open import product
open import sum

{-
------------------------------------------------------------------------------
so far: EXTERNAL VERIFICATION
- written programs (e.g., 'length')
- proved properties (e.g., 'length-reverse')

This style of verification in type theory is called external verification
- proofs are external to programs
- proofs are distinct artifacts about some pre-existing programs

INTERNAL VERIFICATION

write functions with semantically expressive types
write datatypes that put restrictions on data
may require embedding proofs in code

------------------------------------------------------------------------------
-- p 99 VECTORS - length of vector included in type : vector is INDEXED by its length

-- vector.agda
-}
data 𝕍 {ℓ} (A : Set ℓ) : ℕ → Set ℓ where
  []   : 𝕍 A 0
  _::_ : {n : ℕ} (x : A) (xs : 𝕍 A n) → 𝕍 A (suc n)

-- compare to list (overloaded constructors OK)
data L {ℓ} (A : Set ℓ) :     Set ℓ where
  []   : L A
  _::_ :         (x : A) (xs : L A)   → L A

infixr 6 _::_ _++𝕍_

-- p 101

[_]𝕍 : ∀ {ℓ} {A : Set ℓ} → A → 𝕍 A 1
[ x ]𝕍 = x :: []

-- type level addition on length
_++𝕍_ : ∀ {ℓ} {A : Set ℓ}{n m : ℕ} → 𝕍 A n → 𝕍 A m → 𝕍 A (n + m)
[]        ++𝕍 ys = ys
(x :: xs) ++𝕍 ys = x :: xs ++𝕍 ys

-- p 102

-- no 'nil' list corner case
head𝕍 : ∀ {ℓ} {A : Set ℓ} {n : ℕ} → 𝕍 A (suc n) → A
head𝕍 (x :: _) = x

-- type level subtraction
tail𝕍 : ∀ {ℓ} {A : Set ℓ} {n : ℕ} → 𝕍 A n → 𝕍 A (pred n)
tail𝕍       []  = []
tail𝕍 (_ :: xs) = xs

-- p 103

-- length preserving (for lists, length preservation is separate proof)
map𝕍 : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {n : ℕ} → (A → B) → 𝕍 A n → 𝕍 B n
map𝕍 f       []  = []
map𝕍 f (x :: xs) = f x :: map𝕍 f xs

-- p 104

-- takes a vector of length m
-- each element is vector of length n
-- concats into single vector of length m * n
concat𝕍 : ∀{ℓ} {A : Set ℓ} {n m : ℕ} → 𝕍 (𝕍 A n) m → 𝕍 A (m * n)
concat𝕍       []  = []
concat𝕍 (x :: xs) = x ++𝕍 (concat𝕍 xs)

--  p 104

-- no need for maybe result as in lists by requiring n < m
nth𝕍 : ∀ {ℓ} {A : Set ℓ} {m : ℕ}
  → (n : ℕ)
  → n < m ≡ tt
  → 𝕍 A m
  → A
nth𝕍      0   _ (x :: _) = x
-- Proof p (that index is less than length of vector) reused in recursive call.
-- index is suc n
-- length of list is suc m, for implicit m
-- Agda implicitly introduces .m with suc .m
-- p proves suc n < suc m ≡ tt
-- def/eq to n < m ≡ tt
-- so p has correct type to make the recursive call
nth𝕍 (suc n)  p (_ :: xs) = nth𝕍 n p xs
-- us absurd pattern for the proof in last two cases
-- length of list is zero, so no index can be smaller than that length
-- must case-split on the index so Agda can the absurdity
-- because the definition of _<_ splits on both inputs
-- - returns ff separately for when the first input is is 0 and the second is 0
-- - and  for the first input being suc n and second is 0
nth𝕍 (suc n) ()       []
nth𝕍      0  ()       []

-- p 105

repeat𝕍 : ∀ {ℓ} {A : Set ℓ} → (a : A) (n : ℕ) → 𝕍 A n
repeat𝕍 a      0  = []
repeat𝕍 a (suc n) = a :: (repeat𝕍 a n)

{-
------------------------------------------------------------------------------
-- p 106 BRAUN TREES : balanced binary heaps

either empty or
node consisting of some data x and a left and a right subtree

data may be stored so that x is smaller than all data in left and right subtrees
if such an ordering property is desired

BRAUN TREE PROPERTY (BTP) : crucial property : sizes of left and right trees:

for each node in the tree
- either size (left) = size ( right ) or
         size (left) = size ( right ) + 1

ensures depth of the trees is ≤ log₂(N), where N is the number of nodes

property maintained (via types) during insert

make the type A and ordering on that type be parameters of the module

braun-tree.adga
-}

module braun-tree {ℓ} (A : Set ℓ) (_<A_ : A → A → 𝔹) where

  -- index n is size (number of elements of type A) of the tree
  data braun-tree : (n : ℕ) → Set ℓ where
    bt-empty : braun-tree 0
    bt-node : ∀ {n m : ℕ}
      → A
      → braun-tree n
      → braun-tree m
      → n ≡ m ∨ n ≡ suc m        -- 'v' defined in sum.agda for disjunction of two types
      → braun-tree (suc (n + m))

{- -- p 107
sum.agda

-- types A and B, possibly at different levels, accounted via ⊔ in return type
-- ⊔ part of Agda’s primitive level system : imported from Agda.Primitive module in level.agda
-- use this in code that intended to be run
data _⊎_ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where
  inj₁ : (x : A) → A ⊎ B -- built from an A
  inj₂ : (y : B) → A ⊎ B -- built from an B

-- use this to represent a logical proposition
_∨_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
_∨_ = _⊎_

NO SEMANTIC DIFFERENCE - just different notation to help understanding code
-}

  {-
  --------------------------------------------------
  -- p 107-108 INSERTION
  -- this version keeps smaller (_<A_) elements closer to root when inserting
  -}

  -- type says given BT of size n, returns BT of size suc n
  bt-insert : ∀ {n : ℕ} → A → braun-tree n → braun-tree (suc n)

  -- insert into empty
  -- Create node with element and empty subtrees (both with size 0).
  -- 4th arg to BT constructor is BTP proof
  -- - both 0 so 'refl'
  -- - wrap in inj₁ to say 0 ≡ 0 (not n ≡ suc n)
  bt-insert a bt-empty = bt-node a bt-empty bt-empty (inj₁ refl)

  -- insert info non empty: tree has left and right satisfying BTP
  -- left of size n; right of size m
  -- p is BTP proof
  -- inferred type of return is BT (suc (suc (n + m)))
  -- because type before insert is BT (suc (n + m)) - left plus node element plus right
  -- insert adds ONE, so BT (suc (suc (m + n)))
  bt-insert a (bt-node{n}{m} a' l r p)
    -- regardless of what happens, left and right will be swapped, so size sum will have m first

    -- do rewrite before case splitting on which disjunct of BTP holds (n ≡ m or n ≡ suc m)
    -- does not change structure of tree
    -- will change what proof is used for BTP for new node returned.

    -- case split via WITH on P

    -- could split on p directly in pattern for input BT,
    -- but here rewrite is factored to be done once

    -- could do WITH on an if_then_else_ term, to put the min of element being inserted (a)
    -- and element at current root (a') as 1st component pair (a1), max as 2nd (a2)
    -- want min (a1) to be data at root of new BT
    -- want to insert max (a2) recursively into right
    rewrite +comm n m
    with p | if a <A a' then (a , a') else (a' , a)

  -- inj₁ case
  -- case where p is inj₁ for NEW new pattern variable 'p'
  -- underscore in place of original proof/p
  -- because considering case where original is 'inj₁ p'

  -- p : n ≡ m
  -- so new node
  -- with smaller element a1 at root and then swapped left and update right
  -- has type 'inj₂ refl'

  -- BTP for new node is suc m ≡ n v suc m ≡ suc n
  -- because size of new left is suc m, since it is the updated version of old right
  -- case has proof n ≡ m
  -- rewrite with that proof changes that to suc m ≡ suc n
  -- 'inj 2 refl' proves it
  bt-insert a (bt-node{n}{m} a' l r _) | inj₁ p | (a1 , a2)
    rewrite p = (bt-node a1 (bt-insert a2 r) l (inj₂ refl))

  -- inj₂ case : n ≡ suc m
  -- so need proof suc m ≡ n v suc m ≡ suc n
  -- 'sym p' gives 'suc m ≡ n'
  -- wrap in 'inj₁'
  bt-insert a (bt-node{n}{m} a' l r _) | inj₂ p | (a1 , a2) =
                (bt-node a1 (bt-insert a2 r) l (inj₁ (sym p)))

  {-
  --------------------------------------------------
  -- p 110 REMOVE MIN ELEMENT
  -}

  -- input has at least one element; returns pair of element and a BT one smaller
  bt-remove-min : ∀ {p : ℕ} → braun-tree (suc p) → A × braun-tree p

  -- no need for case of empty input
  -- because size would be 0, but input is 'suc p'

  -- removing sole node; return data and bt-empty
  bt-remove-min (bt-node a bt-empty bt-empty u) = a , bt-empty

  -- next two equations for left is empty and right subtree is a node -- IMPOSSIBLE by BTP
  -- still need to handle both proves with absurd
  bt-remove-min (bt-node a bt-empty (bt-node _ _ _ _) (inj₁ ()))
  bt-remove-min (bt-node a bt-empty (bt-node _ _ _ _) (inj₂ ()))

  -- right empty, left node (implies left size is 1, but not needed)
  -- return data left
  -- need to confirm size relationships satisfied, because
  -- size of input  is suc (suc (n’ + m’) + 0)
  -- size of output is      suc (n’ + m’)
  -- use +0 to drop the '+ 0'
  bt-remove-min (bt-node a (bt-node{n’}{m’} a’ l’ r’ u’) bt-empty u)
    rewrite +0 (n’ + m’) = a , bt-node a’ l’ r’ u’

  -- left and right of input both nodes (not empty)
  -- return data input (the min data)
  -- reassemble output BT: remove min from left:
  bt-remove-min (bt-node a (bt-node a1 l1 r1 u1) (bt-node a2 l2 r2 u2) u)
    with bt-remove-min (bt-node a1 l1 r1 u1)
  -- then match on result of recursive call to bt-remove-min.
  -- produces min a1’ of left and updated left l’
  -- then WITH to pick smaller of a1’ (minimum of left) and a2, minimum of right
  -- similar to the bt-insert with an if_then_else_ term.
  bt-remove-min (bt-node a (bt-node a1 l1 r1 u1) (bt-node a2 l2 r2 u2) u) | a1’ , l’
    with if a1’ <A a2 then (a1’ , a2) else (a2 , a1’)

  -- p 113 first words TODO
  bt-remove-min (bt-node a (bt-node{n1}{m1} a1 l1 r1 u1) (bt-node{n2}{m2} _ l2 r2 u2) u)
    | _ , l’ | smaller , other
    rewrite +suc  (n1 + m1) (n2 + m2) |
            +comm (n1 + m1) (n2 + m2) = a , bt-node smaller (bt-node other l2 r2 u2) l’ (lem u)
    where lem : ∀ {x y}
              → suc x ≡ y ∨ suc x ≡ suc y
              →     y ≡ x ∨     y ≡ suc x
          lem (inj₁ p) = inj₂ (sym          p)
          lem (inj₂ p) = inj₁ (sym (suc-inj p))

{-
------------------------------------------------------------------------------
-- p 114 Sigma Types

Above expresses invariant properties of data using internally verified datatypes.

Any data constructed via the constructors are guaranteed to satisfy the property,
due to restrictions enforced by the constructors.

Different case: state that a property holds of an existing data type.

done using Σ-types (“sigma”)

similar to Cartesian product type A × B (elements of A × B are pairs (a, b))
- but generalization where type of 2nd element can depend on type of 1st
- aka "dependent product type" (though the notation comes from sum types, see below)

see nat-nonzero.agda : type for nonzero natural numbers:

-- a nat 'n' AND a proof 'iszero n ≡ ff'
ℕ⁺ : Set
ℕ⁺ = Σ ℕ (λ n → iszero n ≡ ff)

conceptually similar to Cartesian product : N × (iszero n ≡ ff)
- pair of number and equality proof
- in Cartesian product version, 'n' is free
- Σ-types enable referring to 1st of pair

see product.agda : def of Σ

parametrized by
- type A
- function B
  - input : type A
  - returns a type
- types can be at different levels
- Like sum types, Σ type is then at level ℓ ⊔ ℓ' (least upper bound of the two levels)
data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  _,_ : (a : A) → (b : B a) → Σ A B
                         ^
               B depends on

------------------------------------------------------------------------------
-- p 115 example: addition on nonzero nats
-}

open import nat-nonzero hiding (_+⁺_)

_+⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(zero         , ()) +⁺ n2 -- cannot happen, so uses absurd pattern
(1            , p1) +⁺ y = suc⁺ y
(suc (suc n1) , p1) +⁺ y = suc⁺ ((suc n1 , refl) +⁺ y) -- recursive call

{-
-- p 115 5.3.1 Why Sigma and Pi?

why Σ symbol for type of dependent pairs?
- because Σ-types generalize disjoint unions
- in math, a disjoint union is union of two sets
  - where elements are tagged to indicate from which set they have come
  - cardinality of A ⊎ B, is sum of cardinalities of A and B
    even if they have a nonempty intersection.
- This is where we get the notation for sum types in Figure 5.2.
- The disjoint union can be defined mathematically as
    ({0} × A) ∪ ({1} × B)
  - each element of union looks like (n, x)
    where if the tag n is 0, then x P A, and
          if         n is 1, then x P B.

------------------------------------------------------------------------------
-- p 116 Binary Search Trees

for some type A and an ordering relation on that type
values in left  subtree always ≤ value at node ℕ
values in right subtree always > value at node ℕ

see z05-01-bst-test.agda
    z05-01-bst.agda

-- p 117-120
TODO : read/understand discussion of
       bool-relations.agda
       relations.agda

------------------------------------------------------------------------------
-- p 123 Internal vs. External Verification

internal verification : datatypes defined with invariants; functions take proofs of preconditions
- Datatypes with essential invariants : enforce via internal
- Complex programs
  - doing external of complex will cause reasoning about complexity
    not relevant to property being proved
  - internal weaves proofs thru code and datatype

external verification : theorems about functions proved separately
- Algebraic Properties e.g., proving associativity
- Functions used in an internal verification's specification
  -- e.g., min/max used in bst - need to externally prove properties about min/max

------------------------------------------------------------------------------
-- p 126 Exercises

1. Nested vector type.
   Fill in the hole to define a type for matrices of nats
   where the type lists the dimensions of the matrix:
-}

-- inner vector is a row
_by_matrix : ℕ → ℕ → Set
rows by cols matrix = 𝕍 (𝕍 ℕ cols) rows

matrix-to-vec-vec : ∀ {rows cols : ℕ} → rows by cols matrix → 𝕍 (𝕍 ℕ cols) rows
matrix-to-vec-vec 𝕞 = 𝕞

-- 2a
zero-matrix : (rows cols : ℕ) → rows by cols matrix
zero-matrix rows cols = repeat𝕍 (repeat𝕍 0 cols) rows

_ : zero-matrix 2 3 ≡ (0 :: 0 :: 0 :: []) ::
                      (0 :: 0 :: 0 :: []) :: []
_ = refl

_ : zero-matrix 0 0 ≡ []
_ = refl
_ : zero-matrix 0 1 ≡ []
_ = refl
_ : zero-matrix 1 0 ≡ [] :: []
_ = refl
_ : zero-matrix 1 1 ≡ (0 :: []) :: []
_ = refl

-- 2b
matrix-elt : ∀ {rows cols : ℕ}
  → rows by cols matrix
  → (r : ℕ)
  → (c : ℕ)
  → r < rows ≡ tt
  → c < cols ≡ tt
  → ℕ
matrix-elt 𝕞 r c r<rows c<cols = nth𝕍 c c<cols (nth𝕍 r r<rows (matrix-to-vec-vec 𝕞))

-- 2c
diagonal-matrix : ℕ → (n : ℕ) → n by n matrix
diagonal-matrix d n = mkRows n n n
 where
  -- when constructing rows/cols
  -- - row/col param corresponds to row/col - rows/cols
  -- - e.g., for 2 x 3 matrix
  --   row param 2 corresponds 2 - 2 = 0

  mkElt  : ℕ → ℕ → ℕ
  mkElt i col = if i =ℕ col then d else zero

  mkCols : (ℕ → ℕ) → (cols : ℕ) → 𝕍 ℕ cols
  mkCols _     zero   = []
  mkCols f sc@(suc c) = f sc :: mkCols f c

  mkRows : ℕ → (rows : ℕ) → (cols : ℕ) → 𝕍 (𝕍 ℕ cols) rows
  mkRows _  zero   _ = []
  mkRows i (suc r) c = mkCols (mkElt i) c :: mkRows (i ∸ 1) r c

identity-matrix : (n : ℕ) → n by n matrix
identity-matrix = diagonal-matrix 1

idm5 : 5 by 5 matrix
idm5 = identity-matrix 5

_ : idm5 ≡ (1 :: 0 :: 0 :: 0 :: 0 :: []) ::
           (0 :: 1 :: 0 :: 0 :: 0 :: []) ::
           (0 :: 0 :: 1 :: 0 :: 0 :: []) ::
           (0 :: 0 :: 0 :: 1 :: 0 :: []) ::
           (0 :: 0 :: 0 :: 0 :: 1 :: []) :: []
_ = refl

_ : matrix-elt idm5 0 0 refl refl ≡ 1
_ = refl
_ : matrix-elt idm5 1 1 refl refl ≡ 1
_ = refl
_ : matrix-elt idm5 0 1 refl refl ≡ 0
_ = refl

-- 2d
-- BEGIN https://typeslogicscats.gitlab.io/posts/agda-matrix.lagda.html
prepend-column
  : ∀ {m n : ℕ}
  → 𝕍 ℕ n                    -- a column
  → n by     m matrix
  → n by suc m matrix        -- prepends the given column to the matrix
prepend-column      []           []  = []
prepend-column (x :: xs) (vec :: vecs) = (x :: vec) :: (prepend-column xs vecs)

-- inverse of prepend-column (NOT USED)
unprepend-column
  : ∀ {m n : ℕ}
  →            n by suc m matrix
  → (𝕍 ℕ n) × (n by     m matrix)
unprepend-column                     [] = ([] , [])
unprepend-column ((x :: vec) :: matrix) = let xs-vecs = unprepend-column matrix
                                in x :: fst xs-vecs , vec :: snd xs-vecs

fill-empty : (n : ℕ) → n by 0 matrix
fill-empty       0 = []
fill-empty (suc n) = [] :: fill-empty n

transpose : ∀ {i : ℕ} {j : ℕ} → i by j matrix → j by i matrix
transpose     {0} {j}           []  = fill-empty j
transpose {suc _} {_} (row :: rows) = prepend-column row (transpose rows)
-- END https://typeslogicscats.gitlab.io/posts/agda-matrix.lagda.html

ex2x3 : 2 by 3 matrix
ex2x3 = (1 :: 2 :: 3 :: []) ::
        (0 :: 6 :: 7 :: []) :: []

_ : transpose ex2x3 ≡ (1 :: 0 :: []) ::
                      (2 :: 6 :: []) ::
                      (3 :: 7 :: []) :: []
_ = refl

-- BEGIN https://www.cs.nott.ac.uk/~psztxa/g53cfr/solutions/ex02.agda
vreturn : {A : Set} {n : ℕ} → A → 𝕍 A n
vreturn {n = zero}  a = []
vreturn {n = suc m} a = a :: vreturn {n = m} a

vapp : {A B : Set} {n : ℕ} → 𝕍 (A → B) n → 𝕍 A n → 𝕍 B n
vapp      []       []  = []
vapp (f :: fs) (a :: as) = f a :: vapp fs as

transposeX : {m n : ℕ} → m by n matrix → n by m matrix
transposeX         []  = vreturn []
transposeX (as :: ass) = vapp (vapp (vreturn _::_ ) as) (transposeX ass)

_ : transposeX ex2x3 ≡ (1 :: 0 :: []) ::
                       (2 :: 6 :: []) ::
                       (3 :: 7 :: []) :: []
_ = refl
-- END https://www.cs.nott.ac.uk/~psztxa/g53cfr/solutions/ex02.agda

-- BEGIN HORRIBLE HACKY TRY
postulate
  yyy : (n : ℕ) → (rc : ℕ) → rc < n ≡ tt

xx : ∀ {x y : ℕ}
   → x =ℕ 0 ≡ ff
   → y =ℕ 0 ≡ ff
   → x ∸ y < x ≡ tt
xx {x} {suc y} x≠0 y≠0
  rewrite ∸< {x} {y} x≠0
  = refl

transpose' : ∀ {n m : ℕ} → n by m matrix → m by n matrix
transpose'             {0}       {m} _ = zero-matrix m 0
transpose'             {1}       {m} _ = zero-matrix m 1
transpose' n@{suc (suc _)}    {zero} 𝕞 = zero-matrix zero n
transpose' n@{suc (suc _)} m@{suc _} 𝕞 = mkRows m n
 where
  mkElt : (newRow : ℕ)
        → newRow =ℕ 0 ≡ ff
        → (newCol : ℕ)
        → newCol =ℕ 0 ≡ ff
        → ℕ
  mkElt newRow rp newCol cp =
    matrix-elt 𝕞 (n ∸ newCol)         (m ∸ newRow)
--                 (xx cp refl) (xx rp refl)
--              (yyy (n ∸ newCol) n) (yyy (m ∸ newRow) m)
                    {!!} {!!}

  mkCols : (∀ (new : ℕ) → new =ℕ 0 ≡ ff → ℕ) → (cols : ℕ) → 𝕍 ℕ cols
  mkCols _     zero   = []
  mkCols f sc@(suc c) = f sc refl :: mkCols f c

  mkRows : (rows : ℕ) → (cols : ℕ) → 𝕍 (𝕍 ℕ cols) rows
  mkRows     zero   _ = []
  mkRows sr@(suc r) c = mkCols (mkElt sr refl) c :: mkRows r c

_ : transpose' ex2x3 ≡ (1 :: 0 :: []) ::
                       (2 :: 6 :: []) ::
                       (3 :: 7 :: []) :: []
_ = refl
-- END HORRIBLE HACKY TRY

-- 2e
dotProduct𝕍 : ∀ {n : ℕ} → 𝕍 ℕ n → 𝕍 ℕ n → ℕ
dotProduct𝕍       []        []  = 0
dotProduct𝕍 (a :: as) (b :: bs) = a * b + (dotProduct𝕍 as bs)

_ : dotProduct𝕍 (1 :: 3 :: 5 :: []) (4 :: 2 :: 1 :: []) ≡ 15
_ = refl

foldr : ∀ {A B : Set} {n : ℕ} → (A → B → B) → B → 𝕍 A n → B
foldr f z       []  = z
foldr f z (x :: xs) = f x (foldr f z xs)

zipWith : ∀ {A B C : Set} {n : ℕ} → (A → B → C) → 𝕍 A n → 𝕍 B n → 𝕍 C n
zipWith _       []        []  = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

dotProduct𝕍' : ∀ {n : ℕ} → 𝕍 ℕ n → 𝕍 ℕ n → ℕ
dotProduct𝕍' as bs = foldr _+_ 0 (zipWith _*_ as bs)

_ : dotProduct𝕍' (1 :: 3 :: 5 :: []) (4 :: 2 :: 1 :: []) ≡ 15
_ = refl

-- 2f
matrix-* : ∀ {m n p : ℕ} → m by n matrix → n by p matrix → m by p matrix
matrix-* [] _ = []
matrix-* {m} {n} {p} (a :: as) bs =
  doRow {n} {p} a (transpose bs) :: matrix-* as bs
 where
  doRow : ∀ {n p : ℕ} → 𝕍 ℕ n → p by n matrix → 𝕍 ℕ p
  doRow a [] = []
  doRow {n} {p} a (b :: bs) = dotProduct𝕍 a b :: doRow a bs

ma : 2 by 3 matrix
ma = (2 :: 3 :: 4 :: []) ::
     (1 :: 0 :: 0 :: []) :: []
mb : 3 by 2 matrix
mb = (0 :: 1000 :: []) ::
     (1 ::  100 :: []) ::
     (0 ::   10 :: []) :: []

_ : matrix-* ma mb ≡ (3 :: 2340 :: []) ::
                     (0 :: 1000 :: []) :: []
_ = refl

identity-2 : 2 by 2 matrix
identity-2 = identity-matrix 2

some-mat : 2 by 2 matrix
some-mat =
  (1 :: 2 :: []) ::
  (3 :: 4 :: []) :: []

some-mat-trans : 2 by 2 matrix
some-mat-trans =
  (1 :: 3 :: []) ::
  (2 :: 4 :: []) :: []

_ : matrix-* some-mat identity-2 ≡ some-mat
_ = refl

_ : transpose some-mat ≡ some-mat-trans
_ = refl

left-mat : 2 by 3 matrix
left-mat =
  (1 :: 2 :: 3 :: []) ::
  (4 :: 5 :: 6 :: []) :: []

right-mat : 3 by 2 matrix
right-mat =
  ( 7 ::  8 :: []) ::
  ( 9 :: 10 :: []) ::
  (11 :: 12 :: []) :: []

product : 2 by 2 matrix
product =
  ( 58 ::  64 :: []) ::
  (139 :: 154 :: []) :: []

_ : matrix-* left-mat right-mat ≡ product
_ = refl

-- TODO https://www.cs.nott.ac.uk/~psztxa/g53cfr/solutions/ex02.agda

-- 3
-- from list.agda
data 𝕃 {ℓ} (A : Set ℓ) : Set ℓ where
  [] : 𝕃 A
  _::_ : (x : A) (xs : 𝕃 A) → 𝕃 A

-- from vector.agda
𝕍-to-𝕃 : ∀ {ℓ} {A : Set ℓ} {n : ℕ} → 𝕍 A n → 𝕃 A
𝕍-to-𝕃 [] = []
𝕍-to-𝕃 (x :: xs) = x :: (𝕍-to-𝕃 xs)

𝕃-to-𝕍 : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → Σ ℕ (λ n → 𝕍 A n)
𝕃-to-𝕍 [] = (0 , [])
𝕃-to-𝕍 (x :: xs) with 𝕃-to-𝕍 xs
... | (n , v) = (suc n , x :: v)

e3 : ∀ {ℓ} {A : Set ℓ} {n : ℕ}
   → (v : 𝕍 A n)
   → 𝕃-to-𝕍 (𝕍-to-𝕃 v) ≡ n , v
e3       [] = refl
e3 (x :: v) with e3 v
... | zz rewrite zz = refl

-- 4. fun takes V (A × B) n ; returns pair V A n and V B n
--    similar to Haskell unzip
unzip : ∀ {ℓ} {A B : Set ℓ} {n : ℕ}
      → 𝕍 (A × B) n
      → 𝕍 A n × 𝕍 B n
unzip       [] = [] , []
unzip ((a , b) :: v) =
  let rest = unzip v
   in a :: fst rest , b :: snd rest

_ : unzip ((1 , 10) :: (2 , 20) :: (3 , 30) :: []) ≡   ( 1 ::  2 ::  3 :: [])
                                                     , (10 :: 20 :: 30 :: [])
_ = refl

{- TODO
-- 5. Implement remove-min / remove-max functions for bst. type.
Using remove-min, define a general remove function
- finds first value isomorphic to given one
- returns bst without that value.
If node holding that value has two (non-leaf) nodes as left and right sub-trees,
then necessary to replace the removed element with its successor.
This is the minimum value in the right subtree.

-- 6. In list-merge-sort.agda : merge-sort using Braun trees.
State and prove theorems about merge-sort.
E.g., prove length of input list and length of returned sorted list are the same.
-}

ext: agda

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --erased-cubical #-}

-- Modules that use --cubical can be imported when --erased-cubical is
-- used.

open import Erased-cubical-Open-public.Cubical

-- However, re-exports from such modules, made using module
-- application, can only be used in erased contexts.

_ : Set
_ = A

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import Level

-- ⊥ is Initial

module Categories.Category.Instance.Zero where

open import Data.Empty using (⊥; ⊥-elim)
open import Function renaming (id to idf)

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Instance.Cats
import Categories.Object.Initial as Init

-- Unlike for ⊤ being Terminal, Agda can't deduce these, need to be explicit
module _ {o ℓ e : Level} where
  open Init (Cats o ℓ e)

  Zero : Category o ℓ e
  Zero = record
    { Obj       = Lift o ⊥
    ; _⇒_       = λ _ _ → Lift ℓ ⊥
    ; _≈_       = λ _ _ → Lift e ⊥
    ; id        = λ { { lift () } }
    ; _∘_       = λ a _ → a -- left-biased rather than strict
    ; assoc     = λ { {lift () } }
    ; sym-assoc = λ { {lift () } }
    ; identityˡ = λ { {()} }
    ; identityʳ = λ { {()} }
    ; identity² = λ { {()} }
    ; ∘-resp-≈  = λ { () }
    ; equiv     = record
      { refl = λ { {()} }
      ; sym = idf
      ; trans = λ a _ → a
      }
    }

  Zero-⊥ : Initial
  Zero-⊥ = record
    { ⊥ = Zero
    ; ! = record
      { F₀ = λ { (lift x) → ⊥-elim x }
      ; F₁ = λ { (lift ()) }
      ; identity = λ { {lift ()} }
      ; homomorphism = λ { {lift ()} }
      ; F-resp-≈ = λ { () }
      }
    ; !-unique = λ f → record
      { F⇒G = record { η = λ { () } ; commute = λ { () } ; sym-commute = λ { () } }
      ; F⇐G = record { η = λ { () } ; commute = λ { () } ; sym-commute = λ { () } }
      ; iso = λ { (lift ()) }
      }
    }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Issue113 where

module X where

  postulate D : Set

open X public

postulate x : D

-- Should give the proper error message, not __IMPOSSIBLE__ from Highlight.Generate
typeIncorrect : Set
typeIncorrect = Set1

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Data.Binary.Relations.Raw where

-- This module defines the "raw" relations on the binary types. In other words,
-- these relations are all functions which return either ⊤ or ⊥.
--
-- Each relation is generic of its strictness: if its first argument is O, it's a
-- strict relation (_<_); otherwise it's non-strict (_≤_).

open import Data.Binary.Bits
open import Data.Binary.Definitions
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary
open import Data.Bool.Properties using (T?)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Binary.Operations.Unary
open import Data.Binary.Operations.Addition

------------------------------------------------------------------------
-- Definition of relations

infix 4 ⟅_⟆_≺ᵇ_ ⟅_⟆_≺⁺_ ⟅_⟆_≺_

⟅_⟆_≺ᵇ_ : Bit → Bit → Bit → Bit
⟅ p ⟆ I ≺ᵇ q = q ∧ p
⟅ p ⟆ O ≺ᵇ q = p ∨ q

⟅_⟆_≺⁺_ : Bit → 𝔹⁺ → 𝔹⁺ → Set
⟅ p ⟆ 1ᵇ       ≺⁺ (y ∷ ys) = ⊤
⟅ p ⟆ 1ᵇ       ≺⁺ 1ᵇ = T p
⟅ p ⟆ (x ∷ xs) ≺⁺ 1ᵇ = ⊥
⟅ p ⟆ (x ∷ xs) ≺⁺ (y ∷ ys) = ⟅ ⟅ p ⟆ x ≺ᵇ y ⟆ xs ≺⁺ ys

⟅_⟆_≺_ : Bit → 𝔹 → 𝔹 → Set
⟅ p ⟆ 0ᵇ ≺ 0ᵇ = T p
⟅ p ⟆ 0ᵇ ≺ (0< _) = ⊤
⟅ p ⟆ 0< xs ≺ 0ᵇ = ⊥
⟅ p ⟆ 0< xs ≺ 0< ys = ⟅ p ⟆ xs ≺⁺ ys

------------------------------------------------------------------------
-- Properties

weaken⁺ : ∀ x xs ys → ⟅ x ⟆ xs ≺⁺ ys → ⟅ I ⟆ xs ≺⁺ ys
weaken⁺ x (O ∷ xs) 1ᵇ xs<ys = xs<ys
weaken⁺ x (O ∷ xs) (y ∷ ys) xs<ys = weaken⁺ (x ∨ y) xs ys xs<ys
weaken⁺ x (I ∷ xs) 1ᵇ xs<ys = xs<ys
weaken⁺ x (I ∷ xs) (O ∷ ys) xs<ys = xs<ys
weaken⁺ x (I ∷ xs) (I ∷ ys) xs<ys = weaken⁺ x xs ys xs<ys
weaken⁺ O 1ᵇ 1ᵇ xs<ys = tt
weaken⁺ O 1ᵇ (x ∷ xs) xs<ys = tt
weaken⁺ I 1ᵇ ys xs<ys = xs<ys

weaken : ∀ xs ys → ⟅ O ⟆ xs ≺ ys → ⟅ I ⟆ xs ≺ ys
weaken (0< xs) (0< ys) xs<ys = weaken⁺ O xs ys xs<ys
weaken (0< x) 0ᵇ xs<ys = xs<ys
weaken 0ᵇ (0< x) xs<ys = tt
weaken 0ᵇ 0ᵇ xs<ys = tt

≺⁺-trans : ∀ x y xs ys zs → ⟅ x ⟆ xs ≺⁺ ys → ⟅ y ⟆ ys ≺⁺ zs → ⟅ x ∧ y ⟆ xs ≺⁺ zs
≺⁺-trans c₁ c₂ 1ᵇ ys (x ∷ zs) xs<ys ys<zs = tt
≺⁺-trans c₁ c₂ (x ∷ xs) 1ᵇ 1ᵇ xs<ys ys<zs = xs<ys
≺⁺-trans c₁ c₂ (x ∷ xs) 1ᵇ (z ∷ zs) () ys<zs
≺⁺-trans c₁ c₂ (x ∷ xs) (y ∷ ys) 1ᵇ xs<ys ys<zs = ys<zs
≺⁺-trans O O 1ᵇ 1ᵇ 1ᵇ xs<ys ys<zs = ys<zs
≺⁺-trans O O 1ᵇ (x ∷ xs) 1ᵇ xs<ys ys<zs = ys<zs
≺⁺-trans O I 1ᵇ 1ᵇ 1ᵇ xs<ys ys<zs = xs<ys
≺⁺-trans O I 1ᵇ (x ∷ xs) 1ᵇ xs<ys ys<zs = ys<zs
≺⁺-trans I O 1ᵇ 1ᵇ 1ᵇ xs<ys ys<zs = ys<zs
≺⁺-trans I O 1ᵇ (x ∷ xs) 1ᵇ xs<ys ys<zs = ys<zs
≺⁺-trans I I 1ᵇ ys 1ᵇ xs<ys ys<zs = tt
≺⁺-trans I c₂ (I ∷ xs) (O ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans O (c₂ ∨ O) xs ys zs xs<ys ys<zs
≺⁺-trans I c₂ (I ∷ xs) (I ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans I O xs ys zs xs<ys ys<zs
≺⁺-trans O c₂ (I ∷ xs) (O ∷ ys) (I ∷ zs) xs<ys ys<zs = ≺⁺-trans O (c₂ ∨ I) xs ys zs xs<ys ys<zs
≺⁺-trans O c₂ (I ∷ xs) (I ∷ ys) (I ∷ zs) xs<ys ys<zs = ≺⁺-trans O c₂ xs ys zs xs<ys ys<zs
≺⁺-trans O c₂ (I ∷ xs) (O ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans O (c₂ ∨ O) xs ys zs xs<ys ys<zs
≺⁺-trans O c₂ (I ∷ xs) (I ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans O O xs ys zs xs<ys ys<zs
≺⁺-trans O c₂ (O ∷ xs) (y ∷ ys) (I ∷ zs) xs<ys ys<zs = weaken⁺ (y ∧ (⟅ c₂ ⟆ y ≺ᵇ I)) xs zs (≺⁺-trans y (⟅ c₂ ⟆ y ≺ᵇ I) xs ys zs xs<ys ys<zs)
≺⁺-trans O c₂ (O ∷ xs) (O ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans O (c₂ ∨ O) xs ys zs xs<ys ys<zs
≺⁺-trans O c₂ (O ∷ xs) (I ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans I O xs ys zs xs<ys ys<zs
≺⁺-trans I O (I ∷ xs) (O ∷ ys) (I ∷ zs) xs<ys ys<zs = ≺⁺-trans O I xs ys zs xs<ys ys<zs
≺⁺-trans I O (I ∷ xs) (I ∷ ys) (I ∷ zs) xs<ys ys<zs = ≺⁺-trans I O xs ys zs xs<ys ys<zs
≺⁺-trans I O (O ∷ xs) (y ∷ ys) (I ∷ zs) xs<ys ys<zs = weaken⁺ (⟅ O ⟆ y ≺ᵇ I) xs zs (≺⁺-trans I (⟅ O ⟆ y ≺ᵇ I) xs ys zs xs<ys ys<zs)
≺⁺-trans I O (O ∷ xs) (O ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans I O xs ys zs xs<ys ys<zs
≺⁺-trans I O (O ∷ xs) (I ∷ ys) (O ∷ zs) xs<ys ys<zs = ≺⁺-trans I O xs ys zs xs<ys ys<zs
≺⁺-trans I I (I ∷ xs) (O ∷ ys) (I ∷ zs) xs<ys ys<zs = weaken⁺ O xs zs (≺⁺-trans (O ∧ I) (⟅ I ⟆ O ≺ᵇ I) xs ys zs xs<ys ys<zs)
≺⁺-trans I I (I ∷ xs) (I ∷ ys) (I ∷ zs) xs<ys ys<zs = ≺⁺-trans (I ∧ I) (⟅ I ⟆ I ≺ᵇ I) xs ys zs xs<ys ys<zs
≺⁺-trans I I (O ∷ xs) (y ∷ ys) (z ∷ zs) xs<ys ys<zs = weaken⁺ (⟅ I ⟆ y ≺ᵇ z) xs zs (≺⁺-trans I (⟅ I ⟆ y ≺ᵇ z) xs ys zs xs<ys ys<zs)

≺-trans : ∀ x y xs ys zs → ⟅ x ⟆ xs ≺ ys → ⟅ y ⟆ ys ≺ zs → ⟅ x ∧ y ⟆ xs ≺ zs
≺-trans x y (0< x₁) (0< x₃) (0< x₂) xs<ys ys<zs = ≺⁺-trans x y x₁ x₃ x₂ xs<ys ys<zs
≺-trans x y (0< x₁) 0ᵇ (0< x₂) () ys<zs
≺-trans x y (0< x₁) (0< x₂) 0ᵇ xs<ys ys<zs = ys<zs
≺-trans x y (0< x₁) 0ᵇ 0ᵇ xs<ys ys<zs = xs<ys
≺-trans x y 0ᵇ ys (0< x₁) xs<ys ys<zs = tt
≺-trans x y 0ᵇ (0< x₁) 0ᵇ tt ()
≺-trans O O 0ᵇ 0ᵇ 0ᵇ xs<ys ys<zs = ys<zs
≺-trans O I 0ᵇ 0ᵇ 0ᵇ xs<ys ys<zs = xs<ys
≺-trans I O 0ᵇ 0ᵇ 0ᵇ xs<ys ys<zs = ys<zs
≺-trans I I 0ᵇ 0ᵇ 0ᵇ xs<ys ys<zs = tt

asym-≺⁺ : ∀ c xs ys → ⟅ c ⟆ ys ≺⁺ xs → ¬ ⟅ not c ⟆ xs ≺⁺ ys
asym-≺⁺ O 1ᵇ 1ᵇ ys<xs xs<ys = ys<xs
asym-≺⁺ O 1ᵇ (x ∷ xs) ys<xs xs<ys = ys<xs
asym-≺⁺ O (O ∷ xs) 1ᵇ ys<xs xs<ys = xs<ys
asym-≺⁺ O (O ∷ xs) (O ∷ ys) ys<xs xs<ys = asym-≺⁺ I ys xs xs<ys ys<xs
asym-≺⁺ O (O ∷ xs) (I ∷ ys) ys<xs xs<ys = asym-≺⁺ I ys xs xs<ys ys<xs
asym-≺⁺ O (I ∷ xs) 1ᵇ ys<xs xs<ys = xs<ys
asym-≺⁺ O (I ∷ xs) (O ∷ ys) ys<xs xs<ys = asym-≺⁺ O ys xs xs<ys ys<xs
asym-≺⁺ O (I ∷ xs) (I ∷ ys) ys<xs xs<ys = asym-≺⁺ I ys xs xs<ys ys<xs
asym-≺⁺ I 1ᵇ 1ᵇ ys<xs xs<ys = xs<ys
asym-≺⁺ I 1ᵇ (x ∷ xs) ys<xs xs<ys = ys<xs
asym-≺⁺ I (O ∷ xs) 1ᵇ ys<xs xs<ys = xs<ys
asym-≺⁺ I (O ∷ xs) (O ∷ ys) ys<xs xs<ys = asym-≺⁺ O ys xs xs<ys ys<xs
asym-≺⁺ I (O ∷ xs) (I ∷ ys) ys<xs xs<ys = asym-≺⁺ I ys xs xs<ys ys<xs
asym-≺⁺ I (I ∷ xs) 1ᵇ ys<xs xs<ys = xs<ys
asym-≺⁺ I (I ∷ xs) (O ∷ ys) ys<xs xs<ys = asym-≺⁺ O ys xs xs<ys ys<xs
asym-≺⁺ I (I ∷ xs) (I ∷ ys) ys<xs xs<ys = asym-≺⁺ O ys xs xs<ys ys<xs

asym-≺ : ∀ c xs ys → ⟅ c ⟆ ys ≺ xs → ¬ ⟅ not c ⟆ xs ≺ ys
asym-≺ c (0< xs) (0< ys) ys<xs xs<ys = asym-≺⁺ c xs ys ys<xs xs<ys
asym-≺ c (0< x) 0ᵇ ys<xs xs<ys = xs<ys
asym-≺ c 0ᵇ (0< x) ys<xs xs<ys = ys<xs
asym-≺ c 0ᵇ 0ᵇ ys<xs xs<ys = asym-≺⁺ c 1ᵇ 1ᵇ ys<xs xs<ys

pos-asym-≺⁺ : ∀ c xs ys → ¬ ⟅ c ⟆ ys ≺⁺ xs → ⟅ not c ⟆ xs ≺⁺ ys
pos-asym-≺⁺ c 1ᵇ (x ∷ ys) ys≺xs = tt
pos-asym-≺⁺ c (x ∷ xs) 1ᵇ ys≺xs = ys≺xs tt
pos-asym-≺⁺ c (I ∷ xs) (I ∷ ys) ys≺xs = pos-asym-≺⁺ c xs ys ys≺xs
pos-asym-≺⁺ O (O ∷ xs) (O ∷ ys) ys≺xs = pos-asym-≺⁺ O xs ys ys≺xs
pos-asym-≺⁺ I (O ∷ xs) (O ∷ ys) ys≺xs = pos-asym-≺⁺ I xs ys ys≺xs
pos-asym-≺⁺ O (O ∷ xs) (I ∷ ys) ys≺xs = pos-asym-≺⁺ O xs ys ys≺xs
pos-asym-≺⁺ I (O ∷ xs) (I ∷ ys) ys≺xs = pos-asym-≺⁺ O xs ys ys≺xs
pos-asym-≺⁺ O (I ∷ xs) (O ∷ ys) ys≺xs = pos-asym-≺⁺ I xs ys ys≺xs
pos-asym-≺⁺ I (I ∷ xs) (O ∷ ys) ys≺xs = pos-asym-≺⁺ I xs ys ys≺xs
pos-asym-≺⁺ O 1ᵇ 1ᵇ ys≺xs = tt
pos-asym-≺⁺ I 1ᵇ 1ᵇ ys≺xs = ys≺xs tt

pos-asym-≺ : ∀ c xs ys → ¬ ⟅ c ⟆ ys ≺ xs → ⟅ not c ⟆ xs ≺ ys
pos-asym-≺ c (0< xs) (0< ys) ys≮xs = pos-asym-≺⁺ c xs ys ys≮xs
pos-asym-≺ c (0< x) 0ᵇ ys≮xs = ys≮xs tt
pos-asym-≺ c 0ᵇ (0< x) ys≮xs = tt
pos-asym-≺ O 0ᵇ 0ᵇ ys≮xs = tt
pos-asym-≺ I 0ᵇ 0ᵇ ys≮xs = ys≮xs tt

≺⁺-antisym : ∀ c → Antisymmetric _≡_ ⟅ c ⟆_≺⁺_
≺⁺-antisym c {1ᵇ} {1ᵇ} xs<ys ys<xs = refl
≺⁺-antisym c {1ᵇ} {x ∷ ys} xs<ys ()
≺⁺-antisym c {x ∷ xs} {1ᵇ} () ys<xs
≺⁺-antisym c {O ∷ xs} {O ∷ ys} xs<ys ys<xs = cong (O ∷_) (≺⁺-antisym (c ∨ O) xs<ys ys<xs)
≺⁺-antisym c {O ∷ xs} {I ∷ ys} xs<ys ys<xs = ⊥-elim (asym-≺⁺ O xs ys ys<xs (weaken⁺ (c ∨ I) xs ys xs<ys))
≺⁺-antisym c {I ∷ xs} {O ∷ ys} xs<ys ys<xs = ⊥-elim (asym-≺⁺ O ys xs xs<ys (weaken⁺ (c ∨ I) ys xs ys<xs))
≺⁺-antisym c {I ∷ xs} {I ∷ ys} xs<ys ys<xs = cong (I ∷_) (≺⁺-antisym c xs<ys ys<xs)

≺-antisym : ∀ c → Antisymmetric _≡_ ⟅ c ⟆_≺_
≺-antisym c {0< x} {0< x₁} xs<ys ys<xs = cong 0<_ (≺⁺-antisym c xs<ys ys<xs)
≺-antisym c {0< x} {0ᵇ} () ys<xs
≺-antisym c {0ᵇ} {0< x} xs<ys ()
≺-antisym c {0ᵇ} {0ᵇ} xs<ys ys<xs = refl

≼-refl : ∀ xs → ⟅ I ⟆ xs ≺⁺ xs
≼-refl 1ᵇ = tt
≼-refl (O ∷ xs) = ≼-refl xs
≼-refl (I ∷ xs) = ≼-refl xs

≺⁺-inc⁺⁺ : ∀ x xs → ⟅ x ⟆ xs ≺⁺ inc⁺⁺ xs
≺⁺-inc⁺⁺ _ 1ᵇ = tt
≺⁺-inc⁺⁺ c (I ∷ xs) = ≺⁺-inc⁺⁺ O xs
≺⁺-inc⁺⁺ O (O ∷ xs) = ≼-refl xs
≺⁺-inc⁺⁺ I (O ∷ xs) = ≼-refl xs

≺⁺-add : ∀ ys xs c₁ c₂  → ⟅ c₁ ⟆ xs ≺⁺ add c₂ ys xs
≺⁺-add 1ᵇ 1ᵇ c₁ O = tt
≺⁺-add 1ᵇ 1ᵇ c₁ I = tt
≺⁺-add 1ᵇ (x ∷ xs) c₁ O = ≺⁺-inc⁺⁺ c₁ (x ∷ xs)
≺⁺-add 1ᵇ (x ∷ xs) c₁ I = ≺⁺-inc⁺⁺ (⟅ c₁ ⟆ x ≺ᵇ x) xs
≺⁺-add (y ∷ ys) (x ∷ xs) c₁ c₂ = ≺⁺-add ys xs (⟅ c₁ ⟆ x ≺ᵇ sumᵇ c₂ y x) (carryᵇ c₂ y x)
≺⁺-add (y ∷ ys) 1ᵇ c₁ I = tt
≺⁺-add (O ∷ ys) 1ᵇ c₁ O = tt
≺⁺-add (I ∷ ys) 1ᵇ c₁ O = tt

≺-add : ∀ ys xs → ⟅ I ⟆ xs ≺ ys + xs
≺-add (0< x) (0< x₁) = ≺⁺-add x x₁ I O
≺-add (0< x) 0ᵇ = tt
≺-add 0ᵇ (0< x) = ≼-refl x
≺-add 0ᵇ 0ᵇ = tt
------------------------------------------------------------------------
-- Decidability

infix 4 _!_≺⁺?_ _!_≺?_

_!_≺⁺?_ : ∀ x xs ys → Dec (⟅ x ⟆ xs ≺⁺ ys)
c ! 1ᵇ ≺⁺? x ∷ xs = yes tt
c ! 1ᵇ ≺⁺? 1ᵇ = T? c
c ! x ∷ xs ≺⁺? 1ᵇ = no (λ z → z)
c ! x ∷ xs ≺⁺? y ∷ ys = (⟅ c ⟆ x ≺ᵇ y) ! xs ≺⁺? ys

_!_≺?_ : ∀ x xs ys → Dec (⟅ x ⟆ xs ≺ ys)
c ! 0< xs ≺? 0< ys = c ! xs ≺⁺? ys
c ! 0< xs ≺? 0ᵇ = no (λ z → z)
c ! 0ᵇ ≺? 0< _ = yes tt
c ! 0ᵇ ≺? 0ᵇ = T? c

compare-≺ : ∀ c → Conn ⟅ c ⟆_≺_ ⟅ not c ⟆_≺_
compare-≺ c xs ys with c ! xs ≺? ys
compare-≺ c xs ys | yes p = inj₁ p
compare-≺ c xs ys | no ¬p = inj₂ (pos-asym-≺ c ys xs ¬p)

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


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

module Properties.Step where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess)
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.String using (primStringAppend)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
open import Luau.Syntax using (Block; Expr; nil; var; val; addr; bool; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; -; *; /; <; >; <=; >=; ==; ~=; ··; string)
open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOp₀; binOp₁; binOp₂; +; -; *; /; <; >; <=; >=; ==; ~=; ··; evalEqOp; evalNeqOp)
open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂; +; -; *; /; <; >; <=; >=; ··)
open import Luau.RuntimeType using (valueType; function; number)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Properties.Remember using (remember; _,_)
open import Utility.Bool using (not; _or_)

data BinOpStepResult v op w : Set where
  step : ∀ x → (v ⟦ op ⟧ w ⟶ x) → BinOpStepResult v op w
  error₁ : BinOpError op (valueType(v)) → BinOpStepResult v op w
  error₂ : BinOpError op (valueType(w)) → BinOpStepResult v op w

binOpStep : ∀ v op w → BinOpStepResult v op w
binOpStep nil + w = error₁ (+ (λ ()))
binOpStep (addr a) + w = error₁ (+ (λ ()))
binOpStep (number m) + nil = error₂ (+ (λ ()))
binOpStep (number m) + (addr a) = error₂ (+ (λ ()))
binOpStep (number m) + (number n) = step (number (primFloatPlus m n)) (+ m n)
binOpStep (number m) + (bool b) = error₂ (+ (λ ()))
binOpStep (number m) + (string x) = error₂ (+ (λ ()))
binOpStep (number m) - (string x) = error₂ (- (λ ()))
binOpStep (number m) * (string x) = error₂ (* (λ ()))
binOpStep (number m) / (string x) = error₂ (/ (λ ()))
binOpStep (number m) < (string x) = error₂ (< (λ ()))
binOpStep (number m) > (string x) = error₂ (> (λ ()))
binOpStep (number m) == (string x) = step (bool false) (== (number m) (string x))
binOpStep (number m) ~= (string x) = step (bool true) (~= (number m) (string x))
binOpStep (number m) <= (string x) = error₂ (<= (λ ()))
binOpStep (number m) >= (string x) = error₂ (>= (λ ()))
binOpStep (bool b) + w = error₁ (+ (λ ()))
binOpStep nil - w = error₁ (- (λ ()))
binOpStep (addr a) - w = error₁ (- (λ ()))
binOpStep (number x) - nil = error₂ (- (λ ()))
binOpStep (number x) - (addr a) = error₂ (- (λ ()))
binOpStep (number x) - (number n) = step (number (primFloatMinus x n)) (- x n)
binOpStep (number x) - (bool b) = error₂ (- (λ ()))
binOpStep (bool b) - w = error₁ (- (λ ()))
binOpStep nil * w = error₁ (* (λ ()))
binOpStep (addr a) * w = error₁ (* (λ ()))
binOpStep (number m) * nil = error₂ (* (λ ()))
binOpStep (number m) * (addr a) = error₂ (* (λ ()))
binOpStep (number m) * (number n) = step (number (primFloatDiv m n)) (* m n)
binOpStep (number m) * (bool b) = error₂ (* (λ ()))
binOpStep (bool b) * w = error₁ (* (λ ()))
binOpStep nil / w = error₁ (/ (λ ()))
binOpStep (addr a) / w = error₁ (/ (λ ()))
binOpStep (number m) / nil = error₂ (/ (λ ()))
binOpStep (number m) / (addr a) = error₂ (/ (λ ()))
binOpStep (number m) / (number n) = step (number (primFloatTimes m n)) (/ m n)
binOpStep (number m) / (bool b) = error₂ (/ (λ ()))
binOpStep (bool b) / w = error₁ (/ (λ ()))
binOpStep nil < w = error₁ (< (λ ()))
binOpStep (addr a) < w = error₁ (< (λ ()))
binOpStep (number m) < nil = error₂ (< (λ ()))
binOpStep (number m) < (addr a) = error₂ (< (λ ()))
binOpStep (number m) < (number n) = step (bool (primFloatLess m n)) (< m n)
binOpStep (number m) < (bool b) = error₂ (< (λ ()))
binOpStep (bool b) < w = error₁ (< (λ ()))
binOpStep nil > w = error₁ (> (λ ()))
binOpStep (addr a) > w = error₁ (> (λ ()))
binOpStep (number m) > nil = error₂ (> (λ ()))
binOpStep (number m) > (addr a) = error₂ (> (λ ()))
binOpStep (number m) > (number n) = step (bool (primFloatLess n m)) (> m n)
binOpStep (number m) > (bool b) = error₂ (> (λ ()))
binOpStep (bool b) > w = error₁ (> (λ ()))
binOpStep v == w = step (bool (evalEqOp v w)) (== v w)
binOpStep v ~= w = step (bool (evalNeqOp v w)) (~= v w)
binOpStep nil <= w = error₁ (<= (λ ()))
binOpStep (addr a) <= w = error₁ (<= (λ ()))
binOpStep (number m) <= nil = error₂ (<= (λ ()))
binOpStep (number m) <= (addr a) = error₂ (<= (λ ()))
binOpStep (number m) <= (number n) = step (bool (primFloatLess m n or primFloatEquality m n)) (<= m n)
binOpStep (number m) <= (bool b) = error₂ (<= (λ ()))
binOpStep (bool b) <= w = error₁ (<= (λ ()))
binOpStep nil >= w = error₁ (>= (λ ()))
binOpStep (addr a) >= w = error₁ (>= (λ ()))
binOpStep (number m) >= nil = error₂ (>= (λ ()))
binOpStep (number m) >= (addr a) = error₂ (>= (λ ()))
binOpStep (number m) >= (number n) = step (bool (primFloatLess n m or primFloatEquality m n)) (>= m n)
binOpStep (number m) >= (bool b) = error₂ (>= (λ ()))
binOpStep (bool b) >= w = error₁ (>= (λ ()))
binOpStep (string x) + w = error₁ (+ (λ ()))
binOpStep (string x) - w = error₁ (- (λ ()))
binOpStep (string x) * w = error₁ (* (λ ()))
binOpStep (string x) / w = error₁ (/ (λ ()))
binOpStep (string x) < w = error₁ (< (λ ()))
binOpStep (string x) > w = error₁ (> (λ ()))
binOpStep (string x) <= w = error₁ (<= (λ ()))
binOpStep (string x) >= w = error₁ (>= (λ ()))
binOpStep nil ·· y = error₁ (·· (λ ()))
binOpStep (addr x) ·· y = error₁ (BinOpError.·· (λ ()))
binOpStep (number x) ·· y = error₁ (BinOpError.·· (λ ()))
binOpStep (bool x) ·· y = error₁ (BinOpError.·· (λ ()))
binOpStep (string x) ·· nil = error₂ (·· (λ ()))
binOpStep (string x) ·· (addr y) = error₂ (·· (λ ()))
binOpStep (string x) ·· (number y) = error₂ (·· (λ ()))
binOpStep (string x) ·· (bool y) = error₂ (·· (λ ()))
binOpStep (string x) ·· (string y) = step (string (primStringAppend x y)) (·· x y)

data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set

data StepResultᴮ H B where
  step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
  return : ∀ v {B′} → (B ≡ (return (val v) ∙ B′)) → StepResultᴮ H B
  done : (B ≡ done) → StepResultᴮ H B
  error : (RuntimeErrorᴮ H B) → StepResultᴮ H B

data StepResultᴱ H M where
  step : ∀ H′ M′ → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → StepResultᴱ H M
  value : ∀ V → (M ≡ val V) → StepResultᴱ H M
  error : (RuntimeErrorᴱ H M) → StepResultᴱ H M

stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B

stepᴱ H (val v) = value v refl
stepᴱ H (var x) = error UnboundVariable
stepᴱ H (M $ N) with stepᴱ H M
stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
stepᴱ H (_ $ N) | value v refl with stepᴱ H N
stepᴱ H (_ $ N) | value v refl | step H′ N′ s = step H′ (val v $ N′) (app₂ v s)
stepᴱ H (_ $ _) | value (addr a) refl | value w refl with remember (H [ a ])
stepᴱ H (_ $ _) | value (addr a) refl | value w refl  | (nothing , p) = error (app₁ (SEGV p))
stepᴱ H (_ $ _) | value (addr a) refl | value w refl  | (just(function F is B end) , p) = step H (block (fun F) is B [ w / name (arg F) ]ᴮ end) (beta function F is B end w refl p)
stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ()))
stepᴱ H (_ $ _) | value (number m) refl | value w refl = error (FunctionMismatch (number m) w (λ ()))
stepᴱ H (_ $ _) | value (bool b) refl | value w refl = error (FunctionMismatch (bool b) w (λ ()))
stepᴱ H (_ $ _) | value (string x) refl | value w refl = error (FunctionMismatch (string x) w (λ ()))
stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
stepᴱ H (M $ N) | error E = error (app₁ E)
stepᴱ H (block b is B end) with stepᴮ H B
stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
stepᴱ H (block b is (return _ ∙ B′) end) | return v refl = step H (val v) (return v)
stepᴱ H (block b is done end) | done refl = step H (val nil) done
stepᴱ H (block b is B end) | error E = error (block E)
stepᴱ H (function F is C end) with alloc H (function F is C end)
stepᴱ H function F is C end | ok a H′ p = step H′ (val (addr a)) (function a p)
stepᴱ H (binexp M op N) with stepᴱ H M
stepᴱ H (binexp M op N) | step H′ M′ s = step H′ (binexp M′ op N) (binOp₁ s)
stepᴱ H (binexp M op N) | error E = error (bin₁ E)
stepᴱ H (binexp M op N) | value v refl with stepᴱ H N
stepᴱ H (binexp M op N) | value v refl | step H′ N′ s = step H′ (binexp (val v) op N′) (binOp₂ s)
stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E)
stepᴱ H (binexp M op N) | value v refl | value w refl with binOpStep v op w
stepᴱ H (binexp M op N) | value v refl | value w refl | step x p = step H (val x) (binOp₀ p)
stepᴱ H (binexp M op N) | value v refl | value w refl | error₁ E = error (BinOpMismatch₁ v w E)
stepᴱ H (binexp M op N) | value v refl | value w refl | error₂ E = error (BinOpMismatch₂ v w E)

stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / name (fun F) ]ᴮ) (function a p)
stepᴮ H (local x ← M ∙ B) with stepᴱ H M
stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
stepᴮ H (local x ← _ ∙ B) | value v refl = step H (B [ v / name x ]ᴮ) (subst v)
stepᴮ H (local x ← M ∙ B) | error E = error (local E)
stepᴮ H (return M ∙ B) with stepᴱ H M
stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
stepᴮ H (return _ ∙ B) | value V refl = return V refl
stepᴮ H (return M ∙ B) | error E = error (return E)
stepᴮ H done = done refl

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
-- Andreas, 2015-11-24, reported by Wolfram Kahl
{-# OPTIONS -v impossible:60 #-}
-- {-# OPTIONS -v tc.section:60 #-}
-- {-# OPTIONS -v scope:10 #-}
-- -- {-# OPTIONS -v tc.mod.apply:100 #-}

postulate N : Set

module A (O : Set) where

  record R : Set where
    field f : O

  module L where
    open R public

module B (P : Set) where

  module M (Q : Set) where
    -- private open module AQ = A Q public  -- Works, as module is named
    open A Q public  -- Did not work, as module is anonymous

  private open module MP = M P public
  -- OR: open MP public

open B
open L N

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --copatterns #-}
module InstantiatedRecordModuleNoCopattern where

module M (A : Set1) where

open M      -- underapplied open
open M Set  -- fully applied open

record R : Set2 where
  constructor inn
  field
    out : Set1

r : R
r = inn Set

open R r  -- fully applied open

bla = out

-- This is an ill-formed copattern:
-- field of instantiated record module is not a projection!!
wrong : R
out wrong = Set

-- InstantiatedRecordModuleNoCopattern.agda:23,1-16
-- Not a valid projection for a copattern: out
-- when checking that the clause out wrong = Set has type R


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

open import Relation.Binary using (Rel)

module Algebra.Structures.Field
  {a ℓ} {A : Set a}
  (_≈_ : Rel A ℓ)
  where

open import Algebra.Linear.Core

open import Relation.Nullary using (¬_)

open import Algebra.Structures _≈_
open import Algebra.FunctionProperties _≈_

open import Level using (_⊔_)

record NonZero (0# : A) : Set (a ⊔ ℓ) where
  field
    value    : A
    non-zero : ¬ (value ≈ 0#)

MultiplicativeInverse : ∀ (0# : A) -> Set (a ⊔ ℓ)
MultiplicativeInverse 0# = NonZero 0# → NonZero 0#

record IsField (_+_ _*_ : Op₂ A) (0# 1# : A) (-_ : Op₁ A) (_⁻¹ : MultiplicativeInverse 0#) : Set (a ⊔ ℓ) where
  field
    isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
    _⁻¹-involutive : ∀ (x : NonZero 0#) → NonZero.value ((x ⁻¹) ⁻¹) ≈ NonZero.value x
    _⁻¹-inverse  : ∀ (x : NonZero 0#) → ((NonZero.value x) * (NonZero.value (x ⁻¹))) ≈ 1#
    0#-not-1#    : ¬ (0# ≈ 1#)

  open IsCommutativeRing isCommutativeRing public

  open import Algebra.Properties.Ring (record { isRing = isRing }) public

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
{-# OPTIONS --without-K --exact-split #-}

module integers where

import rings-with-properties
open rings-with-properties public

--------------------------------------------------------------------------------

{- We give a self-contained proof that ℤ is the initial pointed type with an
   automorphism. -}

-- We first introduce the type of pointed types with an automorphism

UU-Pointed-Type-With-Aut :
  (l : Level) → UU (lsuc l)
UU-Pointed-Type-With-Aut l =
  Σ (UU l) (λ X → X × (X ≃ X))

-- Some trivial bureaucracy for the type of pointed types with an automorphism

type-Pointed-Type-With-Aut :
  {l : Level} → UU-Pointed-Type-With-Aut l → UU l
type-Pointed-Type-With-Aut X = pr1 X

point-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) → type-Pointed-Type-With-Aut X
point-Pointed-Type-With-Aut X = pr1 (pr2 X)

aut-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  type-Pointed-Type-With-Aut X ≃ type-Pointed-Type-With-Aut X
aut-Pointed-Type-With-Aut X = pr2 (pr2 X)

map-aut-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut X
map-aut-Pointed-Type-With-Aut X =
  map-equiv (aut-Pointed-Type-With-Aut X)

inv-map-aut-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut X
inv-map-aut-Pointed-Type-With-Aut X =
  inv-map-equiv (aut-Pointed-Type-With-Aut X)

issec-inv-map-aut-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  ((map-aut-Pointed-Type-With-Aut X) ∘ (inv-map-aut-Pointed-Type-With-Aut X))
  ~ id
issec-inv-map-aut-Pointed-Type-With-Aut X =
  issec-inv-map-equiv (aut-Pointed-Type-With-Aut X)

isretr-inv-map-aut-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  ((inv-map-aut-Pointed-Type-With-Aut X) ∘ (map-aut-Pointed-Type-With-Aut X))
  ~ id
isretr-inv-map-aut-Pointed-Type-With-Aut X =
  isretr-inv-map-equiv (aut-Pointed-Type-With-Aut X)

-- ℤ is a pointed type with an automorphism

ℤ-Pointed-Type-With-Aut : UU-Pointed-Type-With-Aut lzero
ℤ-Pointed-Type-With-Aut =
  pair ℤ (pair zero-ℤ equiv-succ-ℤ)

-- We introduce the type of morphisms of pointed types with an automorphism

hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} →
  UU-Pointed-Type-With-Aut l1 → UU-Pointed-Type-With-Aut l2 → UU (l1 ⊔ l2)
hom-Pointed-Type-With-Aut {l1} {l2} X Y =
  Σ ( type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut Y)
    ( λ f →
      Id (f (point-Pointed-Type-With-Aut X)) (point-Pointed-Type-With-Aut Y)
      ×
      ( ( f ∘ (map-aut-Pointed-Type-With-Aut X)) ~
        ( (map-aut-Pointed-Type-With-Aut Y) ∘ f)))

-- Some trivial bureaucracy about morphisms of pointed types with an
-- automorphism

map-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) → hom-Pointed-Type-With-Aut X Y →
  type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut Y
map-hom-Pointed-Type-With-Aut X Y f = pr1 f

preserves-point-map-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (f : hom-Pointed-Type-With-Aut X Y) →
  Id ( map-hom-Pointed-Type-With-Aut X Y f (point-Pointed-Type-With-Aut X))
     ( point-Pointed-Type-With-Aut Y)
preserves-point-map-hom-Pointed-Type-With-Aut X Y f = pr1 (pr2 f)

preserves-aut-map-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (f : hom-Pointed-Type-With-Aut X Y) →
  ( ( map-hom-Pointed-Type-With-Aut X Y f) ∘ (map-aut-Pointed-Type-With-Aut X))
    ~
  ( ( map-aut-Pointed-Type-With-Aut Y) ∘ (map-hom-Pointed-Type-With-Aut X Y f))
preserves-aut-map-hom-Pointed-Type-With-Aut X Y f = pr2 (pr2 f)

-- We characterize the identity type of hom-Pointed-Type-With-Aut

htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  UU (l1 ⊔ l2)
htpy-hom-Pointed-Type-With-Aut X Y h1 h2 =
  Σ ( map-hom-Pointed-Type-With-Aut X Y h1
      ~ map-hom-Pointed-Type-With-Aut X Y h2)
    ( λ H →
      ( Id ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1)
           ( ( H (point-Pointed-Type-With-Aut X)) ∙
             ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h2)))
      ×
      ( ( x : type-Pointed-Type-With-Aut X) →
        ( Id ( ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1 x) ∙
               ( ap (map-aut-Pointed-Type-With-Aut Y) (H x)))
             ( ( H (map-aut-Pointed-Type-With-Aut X x)) ∙
               ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h2 x)))))

refl-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (h : hom-Pointed-Type-With-Aut X Y) →
  htpy-hom-Pointed-Type-With-Aut X Y h h
refl-htpy-hom-Pointed-Type-With-Aut X Y h =
  pair refl-htpy (pair refl (λ x → right-unit))

htpy-hom-Pointed-Type-With-Aut-eq :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  Id h1 h2 → htpy-hom-Pointed-Type-With-Aut X Y h1 h2
htpy-hom-Pointed-Type-With-Aut-eq X Y h1 .h1 refl =
  refl-htpy-hom-Pointed-Type-With-Aut X Y h1

-- This is the meat of the characterization of the type of morphisms of pointed
-- types with an equivalence. The only hard part is feeding the families
-- explicitly to Agda over and over again, because Agda is apparently not that
-- good at figuring out what the correct family is.

is-contr-total-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (h1 : hom-Pointed-Type-With-Aut X Y) →
  is-contr
    ( Σ ( hom-Pointed-Type-With-Aut X Y)
        ( htpy-hom-Pointed-Type-With-Aut X Y h1))
is-contr-total-htpy-hom-Pointed-Type-With-Aut X Y h1 =
  is-contr-total-Eq-structure
    ( λ ( map-h2 : type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut Y)
        ( str-h2 : ( Id ( map-h2 (point-Pointed-Type-With-Aut X))
                        ( point-Pointed-Type-With-Aut Y)) ×
                   ( ( x : type-Pointed-Type-With-Aut X) →
                     Id ( map-h2 (map-aut-Pointed-Type-With-Aut X x))
                        ( map-aut-Pointed-Type-With-Aut Y (map-h2 x))))
        ( H : map-hom-Pointed-Type-With-Aut X Y h1 ~ map-h2)
      → ( Id ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1)
             ( ( H (point-Pointed-Type-With-Aut X)) ∙
               ( pr1 str-h2)))
        ×
        ( ( x : type-Pointed-Type-With-Aut X) →
          ( Id ( ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1 x) ∙
                 ( ap (map-aut-Pointed-Type-With-Aut Y) (H x)))
               ( ( H (map-aut-Pointed-Type-With-Aut X x)) ∙
                 ( pr2 str-h2 x)))))
    ( is-contr-total-htpy (map-hom-Pointed-Type-With-Aut X Y h1))
    ( pair (map-hom-Pointed-Type-With-Aut X Y h1) refl-htpy)
    ( is-contr-total-Eq-structure
      ( λ ( pt-h2 : Id ( map-hom-Pointed-Type-With-Aut X Y h1
                         ( point-Pointed-Type-With-Aut X))
                       ( point-Pointed-Type-With-Aut Y))
          ( aut-h2 : ( x : type-Pointed-Type-With-Aut X) →
                     Id ( map-hom-Pointed-Type-With-Aut X Y h1
                          ( map-aut-Pointed-Type-With-Aut X x))
                        ( map-aut-Pointed-Type-With-Aut Y
                          ( map-hom-Pointed-Type-With-Aut X Y h1 x)))
          ( α : Id ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1)
                   ( pt-h2))
        → ( ( x : type-Pointed-Type-With-Aut X) →
            Id ( ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1 x) ∙
                 ( refl))
               ( aut-h2 x)))
      ( is-contr-total-path
        ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1))
      ( pair (preserves-point-map-hom-Pointed-Type-With-Aut X Y h1) refl)
      ( is-contr-equiv'
        ( Σ ( ( x : type-Pointed-Type-With-Aut X) →
              Id ( map-hom-Pointed-Type-With-Aut X Y h1
                   ( map-aut-Pointed-Type-With-Aut X x))
                 ( map-aut-Pointed-Type-With-Aut Y
                   ( map-hom-Pointed-Type-With-Aut X Y h1 x)))
            ( λ aut-h2 →
              ( x : type-Pointed-Type-With-Aut X) →
              Id ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1 x)
                 ( aut-h2 x)))
        ( equiv-tot (equiv-htpy-concat htpy-right-unit))
        ( is-contr-total-htpy
          ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1))))

-- We complete the characterization of the identity type of the type of
-- morphisms of types with a point and an automorphism

is-equiv-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  is-equiv (htpy-hom-Pointed-Type-With-Aut-eq X Y h1 h2)
is-equiv-htpy-hom-Pointed-Type-With-Aut X Y h1 =
  fundamental-theorem-id h1
    ( refl-htpy-hom-Pointed-Type-With-Aut X Y h1)
    ( is-contr-total-htpy-hom-Pointed-Type-With-Aut X Y h1)
    ( htpy-hom-Pointed-Type-With-Aut-eq X Y h1)

eq-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : UU-Pointed-Type-With-Aut l1)
  (Y : UU-Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  htpy-hom-Pointed-Type-With-Aut X Y h1 h2 → Id h1 h2
eq-htpy-hom-Pointed-Type-With-Aut X Y h1 h2 =
  inv-is-equiv (is-equiv-htpy-hom-Pointed-Type-With-Aut X Y h1 h2)

-- We show that from ℤ there is a morphism of pointed types with automorphism
-- to any pointed type with automorphisms

map-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  ℤ → type-Pointed-Type-With-Aut X
map-initial-Pointed-Type-With-Aut X (inl zero-ℕ) =
  inv-map-aut-Pointed-Type-With-Aut X (point-Pointed-Type-With-Aut X)
map-initial-Pointed-Type-With-Aut X (inl (succ-ℕ k)) =
  inv-map-aut-Pointed-Type-With-Aut X
    ( map-initial-Pointed-Type-With-Aut X (inl k))
map-initial-Pointed-Type-With-Aut X (inr (inl star)) =
  point-Pointed-Type-With-Aut X
map-initial-Pointed-Type-With-Aut X (inr (inr zero-ℕ)) =
  map-aut-Pointed-Type-With-Aut X (point-Pointed-Type-With-Aut X)
map-initial-Pointed-Type-With-Aut X (inr (inr (succ-ℕ k))) =
  map-aut-Pointed-Type-With-Aut X
    ( map-initial-Pointed-Type-With-Aut X (inr (inr k)))

preserves-point-map-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  Id ( map-initial-Pointed-Type-With-Aut X zero-ℤ)
     ( point-Pointed-Type-With-Aut X)
preserves-point-map-initial-Pointed-Type-With-Aut X = refl

preserves-aut-map-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) (k : ℤ) →
  Id ( map-initial-Pointed-Type-With-Aut X (succ-ℤ k))
     ( map-aut-Pointed-Type-With-Aut X
       ( map-initial-Pointed-Type-With-Aut X k))
preserves-aut-map-initial-Pointed-Type-With-Aut X (inl zero-ℕ) =
  inv
    ( issec-inv-map-aut-Pointed-Type-With-Aut X (point-Pointed-Type-With-Aut X))
preserves-aut-map-initial-Pointed-Type-With-Aut X (inl (succ-ℕ k)) =
  inv
    ( issec-inv-map-aut-Pointed-Type-With-Aut X
      ( map-initial-Pointed-Type-With-Aut X (inl k)))
preserves-aut-map-initial-Pointed-Type-With-Aut X (inr (inl star)) =
  refl
preserves-aut-map-initial-Pointed-Type-With-Aut X (inr (inr zero-ℕ)) =
  refl
preserves-aut-map-initial-Pointed-Type-With-Aut X (inr (inr (succ-ℕ x))) =
  refl

hom-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X
hom-initial-Pointed-Type-With-Aut X =
  pair
    ( map-initial-Pointed-Type-With-Aut X)
    ( pair
      ( preserves-point-map-initial-Pointed-Type-With-Aut X)
      ( preserves-aut-map-initial-Pointed-Type-With-Aut X))

-- We now show that the morphism from ℤ to a pointed type with an automorphism
-- is unique, using our characterization of the identity type of the type of
-- morphisms of pointed types with an automorphism

htpy-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l)
  (h : hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X) →
  map-initial-Pointed-Type-With-Aut X ~
  map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X h
htpy-initial-Pointed-Type-With-Aut X h (inl zero-ℕ) =
  map-eq-transpose-equiv'
    ( aut-Pointed-Type-With-Aut X)
    ( ( inv
        ( preserves-point-map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut
          X h)) ∙
      ( preserves-aut-map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut
        X h neg-one-ℤ))
htpy-initial-Pointed-Type-With-Aut X h (inl (succ-ℕ k)) =
  map-eq-transpose-equiv'
    ( aut-Pointed-Type-With-Aut X)
    ( ( htpy-initial-Pointed-Type-With-Aut X h (inl k)) ∙
      ( preserves-aut-map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut
        X h (inl (succ-ℕ k))))
htpy-initial-Pointed-Type-With-Aut X h (inr (inl star)) =
  inv
    ( preserves-point-map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X h)
htpy-initial-Pointed-Type-With-Aut X h (inr (inr zero-ℕ)) =
  ( ap ( map-aut-Pointed-Type-With-Aut X)
       ( htpy-initial-Pointed-Type-With-Aut X h (inr (inl star)))) ∙
  ( inv
    ( preserves-aut-map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut
      X h (inr (inl star))))
htpy-initial-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k))) =
  ( ap ( map-aut-Pointed-Type-With-Aut X)
       ( htpy-initial-Pointed-Type-With-Aut X h (inr (inr k)))) ∙
  ( inv
    ( preserves-aut-map-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut
      X h (inr (inr k))))

-- The following two steps become trivial if X is a set

coh-point-htpy-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l)
  (h : hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X) →
  Id ( preserves-point-map-initial-Pointed-Type-With-Aut X)
     ( ( htpy-initial-Pointed-Type-With-Aut X h zero-ℤ) ∙
       ( preserves-point-map-hom-Pointed-Type-With-Aut
         ℤ-Pointed-Type-With-Aut X h))
coh-point-htpy-initial-Pointed-Type-With-Aut X h =
  inv
    ( left-inv
      ( preserves-point-map-hom-Pointed-Type-With-Aut
        ℤ-Pointed-Type-With-Aut X h))

coh-aut-htpy-initial-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l)
  (h : hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X)
  (k : ℤ) →
  Id ( ( preserves-aut-map-initial-Pointed-Type-With-Aut X k) ∙
       ( ap ( map-aut-Pointed-Type-With-Aut X)
            ( htpy-initial-Pointed-Type-With-Aut X h k)))
     ( ( htpy-initial-Pointed-Type-With-Aut X h (succ-ℤ k)) ∙
       ( preserves-aut-map-hom-Pointed-Type-With-Aut
         ℤ-Pointed-Type-With-Aut X h k))
coh-aut-htpy-initial-Pointed-Type-With-Aut X h (inl zero-ℕ) =
  inv
    ( inv-con
      ( issec-inv-map-equiv
        ( aut-Pointed-Type-With-Aut X)
        ( point-Pointed-Type-With-Aut X))
      ( ( htpy-initial-Pointed-Type-With-Aut X h zero-ℤ) ∙
        ( preserves-aut-map-hom-Pointed-Type-With-Aut
          ℤ-Pointed-Type-With-Aut X h neg-one-ℤ))
      ( ap ( map-equiv (aut-Pointed-Type-With-Aut X))
           ( htpy-initial-Pointed-Type-With-Aut X h neg-one-ℤ))
      ( triangle-eq-transpose-equiv'
        ( aut-Pointed-Type-With-Aut X)
        ( ( inv
            ( preserves-point-map-hom-Pointed-Type-With-Aut
              ℤ-Pointed-Type-With-Aut X h)) ∙
          ( preserves-aut-map-hom-Pointed-Type-With-Aut
            ℤ-Pointed-Type-With-Aut X h neg-one-ℤ))))
coh-aut-htpy-initial-Pointed-Type-With-Aut X h (inl (succ-ℕ k)) =
  inv
    ( inv-con
      ( issec-inv-map-equiv
        ( aut-Pointed-Type-With-Aut X)
        ( map-initial-Pointed-Type-With-Aut X (inl k)))
      ( ( htpy-initial-Pointed-Type-With-Aut X h (inl k)) ∙
        ( preserves-aut-map-hom-Pointed-Type-With-Aut
          ℤ-Pointed-Type-With-Aut X h (inl (succ-ℕ k))))
      ( ap ( map-equiv (aut-Pointed-Type-With-Aut X))
           ( htpy-initial-Pointed-Type-With-Aut X h (inl (succ-ℕ k))))
      ( triangle-eq-transpose-equiv'
        ( aut-Pointed-Type-With-Aut X)
        ( ( htpy-initial-Pointed-Type-With-Aut X h (inl k)) ∙
          ( preserves-aut-map-hom-Pointed-Type-With-Aut
            ℤ-Pointed-Type-With-Aut X h (inl (succ-ℕ k))))))
coh-aut-htpy-initial-Pointed-Type-With-Aut X h (inr (inl star)) =
  ( inv right-unit) ∙
  ( ( ap ( concat
           ( ap
             ( map-aut-Pointed-Type-With-Aut X)
             ( htpy-initial-Pointed-Type-With-Aut X h zero-ℤ))
           ( map-aut-Pointed-Type-With-Aut X
             ( map-hom-Pointed-Type-With-Aut
               ℤ-Pointed-Type-With-Aut X h zero-ℤ)))
         ( inv (left-inv
           ( preserves-aut-map-hom-Pointed-Type-With-Aut
             ℤ-Pointed-Type-With-Aut X h zero-ℤ)))) ∙
    ( inv
      ( assoc
        ( ap
          ( map-aut-Pointed-Type-With-Aut X)
          ( htpy-initial-Pointed-Type-With-Aut X h zero-ℤ))
        ( inv
          ( preserves-aut-map-hom-Pointed-Type-With-Aut
            ℤ-Pointed-Type-With-Aut X h zero-ℤ))
        ( preserves-aut-map-hom-Pointed-Type-With-Aut
          ℤ-Pointed-Type-With-Aut X h zero-ℤ))))
coh-aut-htpy-initial-Pointed-Type-With-Aut X h (inr (inr zero-ℕ)) =
  ( inv right-unit) ∙
  ( ( ap ( concat
           ( ap
             ( map-aut-Pointed-Type-With-Aut X)
             ( htpy-initial-Pointed-Type-With-Aut X h one-ℤ))
           ( map-aut-Pointed-Type-With-Aut X
             ( map-hom-Pointed-Type-With-Aut
               ℤ-Pointed-Type-With-Aut X h one-ℤ)))
         ( inv (left-inv
           ( preserves-aut-map-hom-Pointed-Type-With-Aut
             ℤ-Pointed-Type-With-Aut X h one-ℤ)))) ∙
    ( inv
      ( assoc
        ( ap
          ( map-aut-Pointed-Type-With-Aut X)
          ( htpy-initial-Pointed-Type-With-Aut X h one-ℤ))
        ( inv
          ( preserves-aut-map-hom-Pointed-Type-With-Aut
            ℤ-Pointed-Type-With-Aut X h one-ℤ))
        ( preserves-aut-map-hom-Pointed-Type-With-Aut
          ℤ-Pointed-Type-With-Aut X h one-ℤ))))
coh-aut-htpy-initial-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k))) =
  ( inv right-unit) ∙
  ( ( ap ( concat
           ( ap
             ( map-aut-Pointed-Type-With-Aut X)
             ( htpy-initial-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k)))))
           ( map-aut-Pointed-Type-With-Aut X
             ( map-hom-Pointed-Type-With-Aut
               ℤ-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k))))))
         ( inv (left-inv
           ( preserves-aut-map-hom-Pointed-Type-With-Aut
             ℤ-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k))))))) ∙
    ( inv
      ( assoc
        ( ap
          ( map-aut-Pointed-Type-With-Aut X)
          ( htpy-initial-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k)))))
        ( inv
          ( preserves-aut-map-hom-Pointed-Type-With-Aut
            ℤ-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k)))))
        ( preserves-aut-map-hom-Pointed-Type-With-Aut
          ℤ-Pointed-Type-With-Aut X h (inr (inr (succ-ℕ k)))))))

is-initial-ℤ-Pointed-Type-With-Aut :
  {l : Level} (X : UU-Pointed-Type-With-Aut l) →
  is-contr (hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X)
is-initial-ℤ-Pointed-Type-With-Aut X =
  pair
    ( hom-initial-Pointed-Type-With-Aut X)
    ( λ h →
      eq-htpy-hom-Pointed-Type-With-Aut ℤ-Pointed-Type-With-Aut X
        ( hom-initial-Pointed-Type-With-Aut X)
        ( h)
        ( pair
          ( htpy-initial-Pointed-Type-With-Aut X h)
          ( pair
            ( coh-point-htpy-initial-Pointed-Type-With-Aut X h)
            ( coh-aut-htpy-initial-Pointed-Type-With-Aut X h))))

--------------------------------------------------------------------------------

{- We exhibit ℤ as an abelian group, and as a ring. -}

add-ℤ-Semi-Group : Semi-Group lzero
add-ℤ-Semi-Group = pair ℤ-Set (pair add-ℤ associative-add-ℤ)

is-unital-add-ℤ-Semi-Group : is-unital add-ℤ-Semi-Group
is-unital-add-ℤ-Semi-Group = pair zero-ℤ (pair left-unit-law-add-ℤ right-unit-law-add-ℤ)

add-ℤ-Monoid : Monoid lzero
add-ℤ-Monoid = pair add-ℤ-Semi-Group is-unital-add-ℤ-Semi-Group

has-inverses-add-ℤ-Monoid : is-group' add-ℤ-Semi-Group is-unital-add-ℤ-Semi-Group
has-inverses-add-ℤ-Monoid = pair neg-ℤ (pair left-inverse-law-add-ℤ right-inverse-law-add-ℤ)

is-group-add-ℤ-Semi-Group : is-group add-ℤ-Semi-Group
is-group-add-ℤ-Semi-Group = pair is-unital-add-ℤ-Semi-Group has-inverses-add-ℤ-Monoid

ℤ-Group : Group lzero
ℤ-Group = pair add-ℤ-Semi-Group is-group-add-ℤ-Semi-Group

ℤ-Ab : Ab lzero
ℤ-Ab = pair ℤ-Group commutative-add-ℤ

has-mul-ℤ-Ab : has-mul-Ab ℤ-Ab
has-mul-ℤ-Ab =
  pair
    ( pair mul-ℤ associative-mul-ℤ)
    ( pair
      ( pair one-ℤ (pair left-unit-law-mul-ℤ right-unit-law-mul-ℤ))
      ( pair left-distributive-mul-add-ℤ right-distributive-mul-add-ℤ))

ℤ-Ring : Ring lzero
ℤ-Ring = pair ℤ-Ab has-mul-ℤ-Ab

ℤ-Comm-Ring : Comm-Ring lzero
ℤ-Comm-Ring = pair ℤ-Ring commutative-mul-ℤ

mul-ℤ-Semi-Group : Semi-Group lzero
mul-ℤ-Semi-Group = pair ℤ-Set (pair mul-ℤ associative-mul-ℤ)

mul-ℤ-Monoid : Monoid lzero
mul-ℤ-Monoid =
  pair
    ( mul-ℤ-Semi-Group)
    ( pair one-ℤ (pair left-unit-law-mul-ℤ right-unit-law-mul-ℤ))

--------------------------------------------------------------------------------

{- We characterize the identity type of ℤ. -}

Eq-ℤ : ℤ → ℤ → UU lzero
Eq-ℤ (inl x) (inl y) = Eq-ℕ x y
Eq-ℤ (inl x) (inr y) = empty
Eq-ℤ (inr x) (inl x₁) = empty
Eq-ℤ (inr (inl x)) (inr (inl y)) = unit
Eq-ℤ (inr (inl x)) (inr (inr y)) = empty
Eq-ℤ (inr (inr x)) (inr (inl y)) = empty
Eq-ℤ (inr (inr x)) (inr (inr y)) = Eq-ℕ x y

is-prop-Eq-ℤ :
  (x y : ℤ) → is-prop (Eq-ℤ x y)
is-prop-Eq-ℤ (inl x) (inl y) = is-prop-Eq-ℕ x y
is-prop-Eq-ℤ (inl x) (inr y) = is-prop-empty
is-prop-Eq-ℤ (inr x) (inl x₁) = is-prop-empty
is-prop-Eq-ℤ (inr (inl x)) (inr (inl y)) = is-prop-unit
is-prop-Eq-ℤ (inr (inl x)) (inr (inr y)) = is-prop-empty
is-prop-Eq-ℤ (inr (inr x)) (inr (inl y)) = is-prop-empty
is-prop-Eq-ℤ (inr (inr x)) (inr (inr y)) = is-prop-Eq-ℕ x y

refl-Eq-ℤ :
  (x : ℤ) → Eq-ℤ x x
refl-Eq-ℤ (inl x) = refl-Eq-ℕ x
refl-Eq-ℤ (inr (inl x)) = star
refl-Eq-ℤ (inr (inr x)) = refl-Eq-ℕ x

Eq-ℤ-eq :
  {x y : ℤ} → Id x y → Eq-ℤ x y
Eq-ℤ-eq {x} {.x} refl = refl-Eq-ℤ x

contraction-total-Eq-ℤ :
  (x : ℤ) (y : Σ ℤ (Eq-ℤ x)) → Id (pair x (refl-Eq-ℤ x)) y
contraction-total-Eq-ℤ (inl x) (pair (inl y) e) =
  eq-pair
    ( ap inl (eq-Eq-ℕ x y e))
    ( is-prop'-is-prop
      ( is-prop-Eq-ℕ x y)
      ( tr
        ( Eq-ℤ (inl x))
        ( ap inl (eq-Eq-ℕ x y e))
        ( refl-Eq-ℤ (inl x)))
      ( e))
contraction-total-Eq-ℤ (inr (inl star)) (pair (inr (inl star)) e) =
  eq-pair refl (is-prop'-is-prop is-prop-unit (refl-Eq-ℤ zero-ℤ) e)
contraction-total-Eq-ℤ (inr (inr x)) (pair (inr (inr y)) e) =
  eq-pair
    ( ap (inr ∘ inr) (eq-Eq-ℕ x y e))
    ( is-prop'-is-prop
      ( is-prop-Eq-ℕ x y)
      ( tr
        ( Eq-ℤ (inr (inr x)))
        ( ap (inr ∘ inr) (eq-Eq-ℕ x y e))
        ( refl-Eq-ℤ (inr (inr x))))
      ( e))

is-contr-total-Eq-ℤ :
  (x : ℤ) → is-contr (Σ ℤ (Eq-ℤ x))
is-contr-total-Eq-ℤ x =
  pair (pair x (refl-Eq-ℤ x)) (contraction-total-Eq-ℤ x)

is-equiv-Eq-ℤ-eq :
  (x y : ℤ) → is-equiv (Eq-ℤ-eq {x} {y})
is-equiv-Eq-ℤ-eq x =
  fundamental-theorem-id x
    ( refl-Eq-ℤ x)
    ( is-contr-total-Eq-ℤ x)
    ( λ y → Eq-ℤ-eq {x} {y})

eq-Eq-ℤ :
  {x y : ℤ} → Eq-ℤ x y → Id x y
eq-Eq-ℤ {x} {y} = inv-is-equiv (is-equiv-Eq-ℤ-eq x y)

--------------------------------------------------------------------------------

{- We prove some basic arithmetic properties of the integers. -}

--------------------------------------------------------------------------------

{- We show that addition from the left and from the right are both equivalences.
   We conclude that they are both injective maps. -}

is-emb-add-ℤ :
  (x : ℤ) → is-emb (add-ℤ x)
is-emb-add-ℤ x =
  is-emb-is-equiv (add-ℤ x) (is-equiv-add-ℤ x)

is-injective-add-ℤ :
  (x y z : ℤ) → Id (add-ℤ x y) (add-ℤ x z) → Id y z
is-injective-add-ℤ x y z = inv-is-equiv (is-emb-add-ℤ x y z)

is-emb-add-ℤ' :
  (y : ℤ) → is-emb (add-ℤ' y)
is-emb-add-ℤ' y = is-emb-is-equiv (add-ℤ' y) (is-equiv-add-ℤ' y)

is-injective-add-ℤ' :
  (y x w : ℤ) → Id (add-ℤ x y) (add-ℤ w y) → Id x w
is-injective-add-ℤ' y x w = inv-is-equiv (is-emb-add-ℤ' y x w)

--------------------------------------------------------------------------------

{- We show that multiplication by neg-one-ℤ is an equivalence. -}

is-emb-neg-ℤ : is-emb neg-ℤ
is-emb-neg-ℤ = is-emb-is-equiv neg-ℤ is-equiv-neg-ℤ

is-injective-neg-ℤ :
  (x y : ℤ) → Id (neg-ℤ x) (neg-ℤ y) → Id x y
is-injective-neg-ℤ x y = inv-is-equiv (is-emb-neg-ℤ x y)

--------------------------------------------------------------------------------

{- We show that if x = mul-ℤ x y for some non-zero integer x, then y = 1. -}

--------------------------------------------------------------------------------

{- We show that multiplication by a non-zero integer is an embedding. -}

{-
is-injective-mul-ℤ :
  (x y z : ℤ) → ¬ (Id zero-ℤ x) → Id (mul-ℤ x y) (mul-ℤ x z) → Id y z
is-injective-mul-ℤ (inl zero-ℕ) y z p q = is-injective-neg-ℤ y z q
is-injective-mul-ℤ (inl (succ-ℕ x)) y z p q = {!!}
is-injective-mul-ℤ (inr x) y z p q = {!x!}

neq-zero-mul-ℤ :
  (x y : ℤ) → ¬ (Id zero-ℤ x) → ¬ (Id zero-ℤ y) → ¬ (Id zero-ℤ (mul-ℤ x y))
neq-zero-mul-ℤ x y Hx Hy = {!!}
-}

--------------------------------------------------------------------------------

{- We prove some interchange laws and moves on iterated multiplications. -}

interchange-2-3-mul-ℤ :
  {a b c d : ℤ} →
  Id (mul-ℤ (mul-ℤ a b) (mul-ℤ c d)) (mul-ℤ (mul-ℤ a c) (mul-ℤ b d))
interchange-2-3-mul-ℤ {a} {b} {c} {d} =
  ( associative-mul-ℤ a b (mul-ℤ c d)) ∙
  ( ( ap ( mul-ℤ a)
         ( ( inv (associative-mul-ℤ b c d)) ∙
           ( ( ap (λ t → mul-ℤ t d) (commutative-mul-ℤ b c)) ∙
             ( associative-mul-ℤ c b d)))) ∙
    ( inv (associative-mul-ℤ a c (mul-ℤ b d))))

interchange-1-3-mul-ℤ :
  {a b c d : ℤ} →
  Id (mul-ℤ (mul-ℤ a b) (mul-ℤ c d)) (mul-ℤ (mul-ℤ c b) (mul-ℤ a d))
interchange-1-3-mul-ℤ {a} {b} {c} {d} =
  ( ap (λ t → mul-ℤ t (mul-ℤ c d)) (commutative-mul-ℤ a b)) ∙
  ( ( interchange-2-3-mul-ℤ {b}) ∙
    ( ap (λ t → mul-ℤ t (mul-ℤ a d)) (commutative-mul-ℤ b c)))

move-four-mul-ℤ :
  {a b c d : ℤ} →
  Id (mul-ℤ (mul-ℤ a b) (mul-ℤ c d)) (mul-ℤ (mul-ℤ a d) (mul-ℤ b c))
move-four-mul-ℤ {a} {b} {c} {d} =
   ( associative-mul-ℤ a b (mul-ℤ c d)) ∙
   ( ( ap ( mul-ℤ a)
          ( ( inv (associative-mul-ℤ b c d)) ∙
            ( commutative-mul-ℤ (mul-ℤ b c) d))) ∙
     ( inv (associative-mul-ℤ a d (mul-ℤ b c))))

move-five-mul-ℤ :
  {a b c d : ℤ} →
  Id (mul-ℤ (mul-ℤ a b) (mul-ℤ c d)) (mul-ℤ (mul-ℤ b c) (mul-ℤ a d))
move-five-mul-ℤ {a} {b} {c} {d} =
  ( interchange-2-3-mul-ℤ {a} {b} {c} {d}) ∙
  ( ( ap (λ t → mul-ℤ t (mul-ℤ b d)) (commutative-mul-ℤ a c)) ∙
    ( ( interchange-2-3-mul-ℤ {c}) ∙
      ( ap (λ t → mul-ℤ t (mul-ℤ a d)) (commutative-mul-ℤ c b))))

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


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

open import Cubical.Categories.Category
open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open Iso
open import Cubical.Foundations.HLevels
open Precategory
open import Cubical.Core.Glue
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport using (transpFill)

module Cubical.Categories.Constructions.Slice {ℓ ℓ' : Level} (C : Precategory ℓ ℓ') (c : C .ob) {{isC : isCategory C}} where

open import Cubical.Data.Sigma

-- just a helper to prevent redundency
TypeC : Type (ℓ-suc (ℓ-max ℓ ℓ'))
TypeC = Type (ℓ-max ℓ ℓ')

-- Components of a slice category

record SliceOb : TypeC where
  constructor sliceob
  field
    {S-ob} : C .ob
    S-arr : C [ S-ob , c ]

open SliceOb public

record SliceHom (a b : SliceOb) : Type ℓ' where
  constructor slicehom
  field
    S-hom : C [ S-ob a , S-ob b ]
    -- commutative diagram
    S-comm : S-hom ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a

open SliceHom public

-- Helpers for working with equality
-- can probably replace these by showing that SliceOb is isomorphic to Sigma and
-- that paths are isomorphic to Sigma? But sounds like that would need a lot of transp

SliceOb-≡-intro : ∀ {a b} {f g}
                 → (p : a ≡ b)
                 → PathP (λ i → C [ p i , c ]) f g
                 → sliceob {a} f ≡ sliceob {b} g
SliceOb-≡-intro p q = λ i → sliceob {p i} (q i)

module _ {xf yg : SliceOb} where
  private
    x = xf .S-ob
    f = xf .S-arr
    y = yg .S-ob
    g = yg .S-arr

  -- a path between slice objects is the "same" as a pair of paths between C obs and C arrows
  SOPathIsoPathΣ : Iso (xf ≡ yg) (Σ[ p ∈ x ≡ y ] PathP (λ i → C [ p i , c ]) f g)
  SOPathIsoPathΣ .fun p = (λ i → (p i) .S-ob) , (λ i → (p i) .S-arr)
  SOPathIsoPathΣ .inv (p , q) i = sliceob {p i} (q i)
  SOPathIsoPathΣ .rightInv _ = refl
  SOPathIsoPathΣ .leftInv _ = refl

  SOPath≃PathΣ = isoToEquiv SOPathIsoPathΣ

  SOPath≡PathΣ = ua (isoToEquiv SOPathIsoPathΣ)

-- intro and elim for working with SliceHom equalities (is there a better way to do this?)
SliceHom-≡-intro : ∀ {a b} {f g} {c₁} {c₂}
                → (p : f ≡ g)
                → PathP (λ i → (p i) ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a) c₁ c₂
                → slicehom f c₁ ≡ slicehom g c₂
SliceHom-≡-intro p q = λ i → slicehom (p i) (q i)

SliceHom-≡-elim : ∀ {a b} {f g} {c₁} {c₂}
                → slicehom f c₁ ≡ slicehom g c₂
                → Σ[ p ∈ f ≡ g ] PathP (λ i → (p i) ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a) c₁ c₂
SliceHom-≡-elim r = (λ i → S-hom (r i)) , λ i → S-comm (r i)

SliceHom-≡-intro' : ∀ {a b} {f g : C [ a .S-ob , b .S-ob ]} {c₁} {c₂}
                  → (p : f ≡ g)
                  → slicehom f c₁ ≡ slicehom g c₂
SliceHom-≡-intro' {a} {b} {f} {g} {c₁} {c₂} p i = slicehom (p i) (c₁≡c₂ i)
  where
    c₁≡c₂ : PathP (λ i → (p i) ⋆⟨ C ⟩ (b .S-arr) ≡ a .S-arr) c₁ c₂
    c₁≡c₂ = isOfHLevel→isOfHLevelDep 1 (λ _ → isC .isSetHom _ _) c₁ c₂ p

-- SliceHom is isomorphic to the Sigma type with the same components
SliceHom-Σ-Iso : ∀ {a b}
            → Iso (SliceHom a b) (Σ[ h ∈ C [ S-ob a , S-ob b ] ] h ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a)
SliceHom-Σ-Iso .fun (slicehom h c) = h , c
SliceHom-Σ-Iso .inv (h , c) = slicehom h c
SliceHom-Σ-Iso .rightInv = λ x → refl
SliceHom-Σ-Iso .leftInv = λ x → refl

-- Precategory definition

SliceCat : Precategory _ _
SliceCat .ob = SliceOb
SliceCat .Hom[_,_] = SliceHom
SliceCat .id (sliceob {x} f) = slicehom (C .id x) (C .⋆IdL _)
SliceCat ._⋆_ {sliceob j} {sliceob k} {sliceob l} (slicehom f p) (slicehom g p') =
  slicehom
    (f ⋆⟨ C ⟩ g)
    ( f ⋆⟨ C ⟩ g ⋆⟨ C ⟩ l
    ≡⟨ C .⋆Assoc _ _ _ ⟩
      f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ l)
    ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) p' ⟩
      f ⋆⟨ C ⟩ k
    ≡⟨ p ⟩
      j
    ∎)
SliceCat .⋆IdL (slicehom S-hom S-comm) =
  SliceHom-≡-intro (⋆IdL C _) (toPathP (isC .isSetHom _ _ _ _))
SliceCat .⋆IdR (slicehom S-hom S-comm) =
  SliceHom-≡-intro (⋆IdR C _) (toPathP (isC .isSetHom _ _ _ _))
SliceCat .⋆Assoc f g h =
  SliceHom-≡-intro (⋆Assoc C _ _ _) (toPathP (isC .isSetHom _ _ _ _))

-- SliceCat is a Category

instance
  isCatSlice : isCategory SliceCat
  isCatSlice .isSetHom {a} {b} (slicehom f c₁) (slicehom g c₂) p q = cong isoP p'≡q'
    where
      -- paths between SliceHoms are equivalent to the projection paths
      p' : Σ[ p ∈ f ≡ g ] PathP (λ i → (p i) ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a) c₁ c₂
      p' = SliceHom-≡-elim p
      q' : Σ[ p ∈ f ≡ g ] PathP (λ i → (p i) ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a) c₁ c₂
      q' = SliceHom-≡-elim q

      -- we want all paths between (dependent) paths of this type to be equal
      B = λ v → v ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a

      -- need the groupoidness for dependent paths
      homIsGroupoidDep : isOfHLevelDep 2 B
      homIsGroupoidDep = isOfHLevel→isOfHLevelDep 2 (λ v x y → isSet→isGroupoid (isC .isSetHom) _ _ x y)

      -- we first prove that the projected paths are equal
      p'≡q' : p' ≡ q'
      p'≡q' = ΣPathP ((isC .isSetHom _ _ _ _) , toPathP (homIsGroupoidDep _ _ _ _ _))

      -- and then we can use equivalence to lift these paths up
      -- to actual SliceHom paths
      isoP = λ g → cong (inv SliceHom-Σ-Iso) (fun (ΣPathIsoPathΣ) g)

-- SliceCat is univalent if C is univalent

module _ ⦃ isU : isUnivalent C ⦄ where
  open CatIso
  open Iso

  module _ { xf yg : SliceOb } where
    private
      x = xf .S-ob
      y = yg .S-ob

    -- names for the equivalences/isos

    pathIsoEquiv : (x ≡ y) ≃ (CatIso x y)
    pathIsoEquiv = univEquiv isU x y

    isoPathEquiv : (CatIso x y) ≃ (x ≡ y)
    isoPathEquiv = invEquiv pathIsoEquiv

    pToIIso' : Iso (x ≡ y) (CatIso x y)
    pToIIso' = equivToIso pathIsoEquiv

    -- the iso in SliceCat we're given induces an iso in C between x and y
    module _ ( cIso@(catiso kc lc s r) : CatIso {C = SliceCat} xf yg ) where
      extractIso' : CatIso {C = C} x y
      extractIso' .mor = kc .S-hom
      extractIso' .inv = lc .S-hom
      extractIso' .sec i = (s i) .S-hom
      extractIso' .ret i = (r i) .S-hom

  instance
    preservesUnivalenceSlice : isUnivalent SliceCat
    -- we prove the equivalence by going through Iso
    preservesUnivalenceSlice .univ xf@(sliceob {x} f) yg@(sliceob {y} g) = isoToIsEquiv sIso
      where
        -- this is just here because the type checker can't seem to infer xf and yg
        pToIIso : Iso (x ≡ y) (CatIso x y)
        pToIIso = pToIIso' {xf = xf} {yg}

        -- the meat of the proof
        sIso : Iso (xf ≡ yg) (CatIso xf yg)
        sIso .fun p = pathToIso xf yg p -- we use the normal pathToIso via path induction to get an isomorphism
        sIso .inv is@(catiso kc lc s r) = SliceOb-≡-intro x≡y (symP (sym (lc .S-comm) ◁ lf≡f))
          where
            -- we get a path between xf and yg by combining paths between
            -- x and y, and f and g
            -- 1. x≡y follows from univalence of C
            -- 2. f≡g is more tricky; by commutativity, we know that g ≡ l ⋆ f
              -- so we want l to be id; we get this by showing: id ≡ pathToIso x y x≡y ≡ l
              -- where the first step follows from path induction, and the second from univalence of C

            -- morphisms in C from kc and lc
            k = kc .S-hom
            l = lc .S-hom

            -- extract out the iso between x and y
            extractIso : CatIso {C = C} x y
            extractIso = extractIso' is

            -- and we can use univalence of C to get x ≡ y
            x≡y : x ≡ y
            x≡y = pToIIso .inv extractIso

            -- to show that f ≡ g, we show that l ≡ id
            -- by using C's isomorphism
            pToI≡id : PathP (λ i → C [ x≡y (~ i) , x ]) (pathToIso {C = C} x y x≡y .inv) (C .id x)
            pToI≡id = J (λ y p → PathP (λ i → C [ p (~ i) , x ]) (pathToIso {C = C} x y p .inv) (C .id x))
                        (λ j → JRefl pToIFam pToIBase j .inv)
                        x≡y
              where
                idx = C .id x
                pToIFam = (λ z _ → CatIso {C = C} x z)
                pToIBase = catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)

            l≡pToI : l ≡ pathToIso {C = C} x y x≡y .inv
            l≡pToI i = pToIIso .rightInv extractIso (~ i) .inv

            l≡id : PathP (λ i → C [ x≡y (~ i) , x ]) l (C .id x)
            l≡id = l≡pToI ◁ pToI≡id

            lf≡f : PathP (λ i → C [ x≡y (~ i) , c ]) (l ⋆⟨ C ⟩ f) f
            lf≡f = (λ i → (l≡id i) ⋆⟨ C ⟩ f) ▷ C .⋆IdL _

        sIso .rightInv is@(catiso kc lc s r) i = catiso (kc'≡kc i) (lc'≡lc i) (s'≡s i) (r'≡r i)
          -- we prove rightInv using a combination of univalence and the fact that homs are an h-set
          where
            kc' = (sIso .fun) (sIso .inv is) .mor
            lc' = (sIso .fun) (sIso .inv is) .inv
            k' = kc' .S-hom
            l' = lc' .S-hom
            k = kc .S-hom
            l = lc .S-hom

            extractIso : CatIso {C = C} x y
            extractIso = extractIso' is

            -- we do the equality component wise

            -- mor

            k'≡k : k' ≡ k
            k'≡k i = (pToIIso .rightInv extractIso) i .mor

            kcom'≡kcom : PathP (λ j → (k'≡k j) ⋆⟨ C ⟩ g ≡ f) (kc' .S-comm) (kc .S-comm)
            kcom'≡kcom = isSetHomP1 _ _ λ i → (k'≡k i) ⋆⟨ C ⟩ g

            kc'≡kc : kc' ≡ kc
            kc'≡kc i = slicehom (k'≡k i) (kcom'≡kcom i)

            -- inv

            l'≡l : l' ≡ l
            l'≡l i = (pToIIso .rightInv extractIso) i .inv

            lcom'≡lcom : PathP (λ j → (l'≡l j) ⋆⟨ C ⟩ f ≡ g) (lc' .S-comm) (lc .S-comm)
            lcom'≡lcom = isSetHomP1 _ _ λ i → (l'≡l i) ⋆⟨ C ⟩ f

            lc'≡lc : lc' ≡ lc
            lc'≡lc i = slicehom (l'≡l i) (lcom'≡lcom i)

            -- sec

            s' = (sIso .fun) (sIso .inv is) .sec
            s'≡s : PathP (λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i ≡ SliceCat .id _) s' s
            s'≡s = isSetHomP1 _ _ λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i

            -- ret

            r' = (sIso .fun) (sIso .inv is) .ret
            r'≡r : PathP (λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i ≡ SliceCat .id _) r' r
            r'≡r = isSetHomP1 _ _ λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i

        sIso .leftInv p = p'≡p
          -- to show that the round trip is equivalent to the identity
          -- we show that this is true for each component (S-ob, S-arr)
          -- and then combine
          -- specifically, we show that p'Ob≡pOb and p'Mor≡pMor
          -- and it follows that p'≡p
          where
            p' = (sIso .inv) (sIso .fun p)

            pOb : x ≡ y
            pOb i = (p i) .S-ob

            p'Ob : x ≡ y
            p'Ob i = (p' i) .S-ob

            pMor : PathP (λ i → C [ pOb i , c ]) f g
            pMor i = (p i) .S-arr

            p'Mor : PathP (λ i → C [ p'Ob i , c ]) f g
            p'Mor i = (p' i) .S-arr

            -- we first show that it's equivalent to use sIso first then extract, or to extract first than use pToIIso
            extractCom : extractIso' (sIso .fun p) ≡ pToIIso .fun pOb
            extractCom = J (λ yg' p̃ → extractIso' (pathToIso xf yg' p̃) ≡ pToIIso' {xf = xf} {yg'} .fun (λ i → (p̃ i) .S-ob))
                           (cong extractIso' (JRefl pToIFam' pToIBase') ∙ sym (JRefl pToIFam pToIBase))
                           p
               where
                 idx = C .id x
                 pToIFam = (λ z _ → CatIso {C = C} x z)
                 pToIBase = catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)

                 idxf = SliceCat .id xf
                 pToIFam' = (λ z _ → CatIso {C = SliceCat} xf z)
                 pToIBase' = catiso (SliceCat .id xf) idxf (SliceCat .⋆IdL idxf) (SliceCat .⋆IdL idxf)

            -- why does this not follow definitionally?
            -- from extractCom, we get that performing the roundtrip on pOb gives us back p'Ob
            ppp : p'Ob ≡ (pToIIso .inv) (pToIIso .fun pOb)
            ppp = cong (pToIIso .inv) extractCom

            -- apply univalence of C
            -- this gives us the first component that we want
            p'Ob≡pOb : p'Ob ≡ pOb
            p'Ob≡pOb = ppp ∙ pToIIso .leftInv pOb

            -- isSetHom gives us the second component, path between morphisms
            p'Mor≡pMor : PathP (λ j → PathP (λ i → C [ (p'Ob≡pOb j) i , c ]) f g) p'Mor pMor
            p'Mor≡pMor = isSetHomP2l _ _ p'Mor pMor p'Ob≡pOb

            -- we can use the above paths to show that p' ≡ p
            p'≡p : p' ≡ p
            p'≡p i = comp (λ i' → SOPath≡PathΣ {xf = xf} {yg} (~ i'))
                            (λ j → λ { (i = i0) → left (~ j) ; (i = i1) → right (~ j) })
                            (p'Σ≡pΣ i)
              where
                -- we break up p' and p into their constituent paths
                -- first via transport and then via our component definitions from before
                -- we show that p'ΣT ≡ p'Σ (and same for p) via univalence
                -- and p'Σ≡pΣ follows from our work from above
                p'ΣT : Σ[ p ∈ x ≡ y ] PathP (λ i → C [ p i , c ]) f g
                p'ΣT = transport SOPath≡PathΣ p'
                p'Σ : Σ[ p ∈ x ≡ y ] PathP (λ i → C [ p i , c ]) f g
                p'Σ = (p'Ob , p'Mor)

                pΣT : Σ[ p ∈ x ≡ y ] PathP (λ i → C [ p i , c ]) f g
                pΣT = transport SOPath≡PathΣ p
                pΣ : Σ[ p ∈ x ≡ y ] PathP (λ i → C [ p i , c ]) f g
                pΣ = (pOb , pMor)-- transport SOPathP≡PathPSO p

                -- using the computation rule to ua
                p'ΣT≡p'Σ : p'ΣT ≡ p'Σ
                p'ΣT≡p'Σ = uaβ SOPath≃PathΣ p'

                pΣT≡pΣ : pΣT ≡ pΣ
                pΣT≡pΣ = uaβ SOPath≃PathΣ p

                p'Σ≡pΣ : p'Σ ≡ pΣ
                p'Σ≡pΣ = ΣPathP (p'Ob≡pOb , p'Mor≡pMor)

                -- two sides of the square we're connecting
                left : PathP (λ i → SOPath≡PathΣ {xf = xf} {yg} i) p' p'Σ
                left = transport-filler SOPath≡PathΣ p' ▷ p'ΣT≡p'Σ

                right : PathP (λ i → SOPath≡PathΣ {xf = xf} {yg} i) p pΣ
                right = transport-filler SOPath≡PathΣ p ▷ pΣT≡pΣ

-- properties
-- TODO: move to own file

open isIsoC renaming (inv to invC)

-- make a slice isomorphism from just the hom
sliceIso : ∀ {a b} (f : C [ a .S-ob , b .S-ob ]) (c : (f ⋆⟨ C ⟩ b .S-arr) ≡ a .S-arr)
         → isIsoC {C = C} f
         → isIsoC {C = SliceCat} (slicehom f c)
sliceIso f c isof .invC = slicehom (isof .invC) (sym (invMoveL (isIso→areInv isof) c))
sliceIso f c isof .sec = SliceHom-≡-intro' (isof .sec)
sliceIso f c isof .ret = SliceHom-≡-intro' (isof .ret)

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:
module Reals where

  -- (a set with properties of) the reals
  data ℝ : Set where
    r0 : ℝ
    r1 : ℝ
    _+_ : ℝ → ℝ → ℝ

  -- equality
  data _==_ : ℝ → ℝ → Set where
    AXrefl== : ∀ {r} → r == r
    AXsymm== : ∀ {r s} → r == s → s == r
    AXtrans== : ∀ {r s t} → r == s → s == t → r == t
    AX+0 : ∀ {r} → (r + r0) == r
    AXsymm+ : ∀ {r s} → (r + s) == (s + r)
    AX+== : ∀ {r s t} → r == s → (r + t) == (s + t)

  THM0+ : {r : ℝ} → r == (r0 + r)
  THM0+ = AXsymm== (AXtrans== AXsymm+ AX+0)
  -- AXsymm+ AX+0   r0 + r == r + r0 and r + r0 == r
  -- AXtrans==      so r0 + r == r
  -- AXsymm==       so r == r0 + r

  THM0+alt : {r : ℝ} → r == (r0 + r)
  THM0+alt {r} = AXsymm== {r0 + r} {r} ((AXtrans== {r0 + r} {r + r0} {r}) (AXsymm+ {r0} {r}) (AX+0 {r}))

  -- strict partial ordering
  data _<_ : ℝ → ℝ → Set where
    AXtrans<<< : ∀ {r s t} → r < s → s < t → r < t
    AX<=< : ∀ {r s t} → r < s → s == t → r < t
    AX=<< : ∀ {r s t} → r == s → s < t → r < t
    AX0<1 : r0 < r1
    AX+<< : ∀ {r s t} → r < s → (r + t) < (s + t)

  THM<+1 : {r : ℝ} → r < (r + r1)
  THM<+1 = AX<=< (AX=<< THM0+ (AX+<< AX0<1)) AXsymm+
  -- AX0<1              0 < 1
  -- AX<+ %             so 0 + r < 1 + r
  -- AX=<< lem0+ %      so r < 1 + r
  -- AX<=< % AXsymm+    so r < r + 1

max_stars_repo_name: jjallaire/skylighting

max_issues_repo_name: jjallaire/skylighting

max_forks_repo_name: jjallaire/skylighting


text:
-- Andreas, 2017-01-21, issue #2423 overloading inherited projections

-- {-# OPTIONS -v tc.lhs.split:30 #-}
-- {-# OPTIONS -v tc.proj.amb:100 #-}
-- {-# OPTIONS -v tc.mod.apply:100 #-}

postulate
  A : Set

record R : Set where
  field f : A

record S : Set where
  field r : R
  open R r public
  -- The inherited projection (in the eyes of the scope checker) S.f
  -- is actually a composition of projections R.f ∘ S.r
  -- s .S.f = s .S.r .R.f

open S
open R

test : S → S
test s .f = s .f

-- Error WAS:
-- Cannot eliminate type S with pattern .f (did you supply too many arguments?)

-- NOW:
-- Cannot eliminate type  S  with projection  R.f

-- Shows the chosen disambiguation in error message.

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic structures
------------------------------------------------------------------------

module Algebra.Morphism where

open import Relation.Binary
open import Algebra
open import Algebra.FunctionProperties
import Algebra.Properties.Group as GroupP
open import Function
open import Data.Product
open import Level
import Relation.Binary.EqReasoning as EqR

------------------------------------------------------------------------
-- Basic definitions

module Definitions {f t ℓ}
                   (From : Set f) (To : Set t) (_≈_ : Rel To ℓ) where
  Morphism : Set _
  Morphism = From → To

  Homomorphic₀ : Morphism → From → To → Set _
  Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘

  Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set _
  Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ ∘ ⟦ x ⟧

  Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set _
  Homomorphic₂ ⟦_⟧ _∙_ _∘_ =
    ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)

------------------------------------------------------------------------
-- An example showing how a morphism type can be defined

-- Ring homomorphisms.

record _-Ring⟶_ {r₁ r₂ r₃ r₄}
                (From : Ring r₁ r₂) (To : Ring r₃ r₄) :
                Set (r₁ ⊔ r₂ ⊔ r₃ ⊔ r₄) where
  private
    module F = Ring From
    module T = Ring To
  open Definitions F.Carrier T.Carrier T._≈_

  field
    ⟦_⟧     : Morphism
    ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
    +-homo  : Homomorphic₂ ⟦_⟧ F._+_ T._+_
    *-homo  : Homomorphic₂ ⟦_⟧ F._*_ T._*_
    1-homo  : Homomorphic₀ ⟦_⟧ F.1#  T.1#

  open EqR T.setoid

  0-homo : Homomorphic₀ ⟦_⟧ F.0# T.0#
  0-homo =
    GroupP.left-identity-unique T.+-group ⟦ F.0# ⟧ ⟦ F.0# ⟧ (begin
      T._+_ ⟦ F.0# ⟧ ⟦ F.0# ⟧ ≈⟨ T.sym (+-homo F.0# F.0#) ⟩
      ⟦ F._+_ F.0# F.0# ⟧     ≈⟨ ⟦⟧-cong (proj₁ F.+-identity F.0#) ⟩
      ⟦ F.0# ⟧                ∎)

  -‿homo : Homomorphic₁ ⟦_⟧ F.-_ T.-_
  -‿homo x =
    GroupP.left-inverse-unique T.+-group ⟦ F.-_ x ⟧ ⟦ x ⟧ (begin
      T._+_ ⟦ F.-_ x ⟧ ⟦ x ⟧ ≈⟨ T.sym (+-homo (F.-_ x) x) ⟩
      ⟦ F._+_ (F.-_ x) x ⟧   ≈⟨ ⟦⟧-cong (proj₁ F.-‿inverse x) ⟩
      ⟦ F.0# ⟧               ≈⟨ 0-homo ⟩
      T.0#                   ∎)


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Nullification.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.PathSplitEquiv
open isPathSplitEquiv

isNull : ∀ {ℓ ℓ'} (S : Type ℓ) (A : Type ℓ') → Type (ℓ-max ℓ ℓ')
isNull S A = isPathSplitEquiv (const {A = A} {B = S})

data Null {ℓ ℓ'} (S : Type ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  ∣_∣ : A → Null S A
  -- the image of every map (S → Null S A) is contractible in Null S A
  hub   : (f : S → Null S A) → Null S A
  spoke : (f : S → Null S A) (s : S) → hub f ≡ f s
  -- the image of every map (S → x ≡ y) for x y : A is contractible in x ≡ y
  ≡hub   : ∀ {x y} (p : S → x ≡ y) → x ≡ y
  ≡spoke : ∀ {x y} (p : S → x ≡ y) (s : S) → ≡hub p ≡ p s

isNull-Null : ∀ {ℓ ℓ'} {S : Type ℓ} {A : Type ℓ'} → isNull S (Null S A)
fst (sec isNull-Null) f     = hub   f
snd (sec isNull-Null) f i s = spoke f s i
fst (secCong isNull-Null x y) p i     = ≡hub   (funExt⁻ p) i
snd (secCong isNull-Null x y) p i j s = ≡spoke (funExt⁻ p) s i j

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical